replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Merge pull request #971 from diffblue/c-types-typing 

Make the c_types have stronger C++ types
This commit is contained in:
Michael Tautschnig 2017-05-26 08:20:59 +01:00 committed by GitHub
parent 3dbda9268f 2e11fef1da
commit 7f8efa0385
4 changed files with 216 additions and 167 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
src/ansi-c/ansi_c_convert_type.cpp
View File

@ -464,14 +464,25 @@ void ansi_c_convert_typet::write(typet &type)
}
if(int8_cnt)
type=is_signed?signed_char_type():unsigned_char_type();
if(is_signed)
type=signed_char_type();
else
type=unsigned_char_type();
else if(int16_cnt)
type=is_signed?signed_short_int_type():unsigned_short_int_type();
if(is_signed)
type=signed_short_int_type();
else
type=unsigned_short_int_type();
else if(int32_cnt)
type=is_signed?signed_int_type():unsigned_int_type();
if(is_signed)
type=signed_int_type();
else
type=unsigned_int_type();
else if(int64_cnt) // Visual Studio: equivalent to long long int
type=
is_signed?signed_long_long_int_type():unsigned_long_long_int_type();
if(is_signed)
type=signed_long_long_int_type();
else
type=unsigned_long_long_int_type();
else
assert(false);
}
@ -509,19 +520,31 @@ void ansi_c_convert_typet::write(typet &type)
throw 0;
}
type=is_signed?signed_short_int_type():unsigned_short_int_type();
if(is_signed)
type=signed_short_int_type();
else
type=unsigned_short_int_type();
}
else if(long_cnt==0)
{
type=is_signed?signed_int_type():unsigned_int_type();
if(is_signed)
type=signed_int_type();
else
type=unsigned_int_type();
}
else if(long_cnt==1)
{
type=is_signed?signed_long_int_type():unsigned_long_int_type();
if(is_signed)
type=signed_long_int_type();
else
type=unsigned_long_int_type();
}
else if(long_cnt==2)
{
type=is_signed?signed_long_long_int_type():unsigned_long_long_int_type();
if(is_signed)
type=signed_long_long_int_type();
else
type=unsigned_long_long_int_type();
}
else
{

67
src/ansi-c/c_typecheck_type.cpp
View File

@ -134,39 +134,74 @@ void c_typecheck_baset::typecheck_type(typet &type)
typet result;
if(mode=="__QI__") // 8 bits
result=is_signed?signed_char_type():unsigned_char_type();
if(is_signed)
result=signed_char_type();
else
result=unsigned_char_type();
else if(mode=="__byte__") // 8 bits
result=is_signed?signed_char_type():unsigned_char_type();
if(is_signed)
result=signed_char_type();
else
result=unsigned_char_type();
else if(mode=="__HI__") // 16 bits
result=is_signed?signed_short_int_type():unsigned_short_int_type();
if(is_signed)
result=signed_short_int_type();
else
result=unsigned_short_int_type();
else if(mode=="__SI__") // 32 bits
result=is_signed?signed_int_type():unsigned_int_type();
if(is_signed)
result=signed_int_type();
else
result=unsigned_int_type();
else if(mode=="__word__") // long int, we think
result=is_signed?signed_long_int_type():unsigned_long_int_type();
if(is_signed)
result=signed_long_int_type();
else
result=unsigned_long_int_type();
else if(mode=="__pointer__") // we think this is size_t/ssize_t
result=is_signed?signed_size_type():size_type();
if(is_signed)
result=signed_size_type();
else
result=size_type();
else if(mode=="__DI__") // 64 bits
{
if(config.ansi_c.long_int_width==64)
result=is_signed?signed_long_int_type():unsigned_long_int_type();
if(is_signed)
result=signed_long_int_type();
else
result=unsigned_long_int_type();
else
{
assert(config.ansi_c.long_long_int_width==64);
result=
is_signed?signed_long_long_int_type():unsigned_long_long_int_type();
if(is_signed)
result=signed_long_long_int_type();
else
result=unsigned_long_long_int_type();
}
}
else if(mode=="__TI__") // 128 bits
result=is_signed?gcc_signed_int128_type():gcc_unsigned_int128_type();
if(is_signed)
result=gcc_signed_int128_type();
else
result=gcc_unsigned_int128_type();
else if(mode=="__V2SI__") // vector of 2 ints, deprecated by gcc
result=
vector_typet(
is_signed?signed_int_type():unsigned_int_type(),
if(is_signed)
result=vector_typet(
signed_int_type(),
from_integer(2, size_type()));
else
result=vector_typet(
unsigned_int_type(),
from_integer(2, size_type()));
else if(mode=="__V4SI__") // vector of 4 ints, deprecated by gcc
result=
vector_typet(
is_signed?signed_int_type():unsigned_int_type(),
if(is_signed)
result=vector_typet(
signed_int_type(),
from_integer(4, size_type()));
else
result=vector_typet(
unsigned_int_type(),
from_integer(4, size_type()));
else // give up, just use subtype
result=type.subtype();

219
src/util/c_types.cpp
View File

@ -23,7 +23,7 @@ Function: index_type
\*******************************************************************/
typet index_type()
bitvector_typet index_type()
{
// same as signed size type
return signed_size_type();
@ -41,7 +41,7 @@ Function: enum_constant_type
\*******************************************************************/
typet enum_constant_type()
bitvector_typet enum_constant_type()
{
// usually same as 'int',
// but might be unsigned, or shorter than 'int'
@ -60,9 +60,9 @@ Function: signed_int_type
\*******************************************************************/
typet signed_int_type()
signedbv_typet signed_int_type()
{
typet result=signedbv_typet(config.ansi_c.int_width);
signedbv_typet result(config.ansi_c.int_width);
result.set(ID_C_c_type, ID_signed_int);
return result;
}
@ -79,9 +79,9 @@ Function: signed_short_int_type
\*******************************************************************/
typet signed_short_int_type()
signedbv_typet signed_short_int_type()
{
typet result=signedbv_typet(config.ansi_c.short_int_width);
signedbv_typet result(config.ansi_c.short_int_width);
result.set(ID_C_c_type, ID_signed_short_int);
return result;
}
@ -98,9 +98,9 @@ Function: unsigned_int_type
\*******************************************************************/
typet unsigned_int_type()
unsignedbv_typet unsigned_int_type()
{
typet result=unsignedbv_typet(config.ansi_c.int_width);
unsignedbv_typet result(config.ansi_c.int_width);
result.set(ID_C_c_type, ID_unsigned_int);
return result;
}
@ -117,9 +117,9 @@ Function: unsigned_short_int_type
\*******************************************************************/
typet unsigned_short_int_type()
unsignedbv_typet unsigned_short_int_type()
{
typet result=unsignedbv_typet(config.ansi_c.short_int_width);
unsignedbv_typet result(config.ansi_c.short_int_width);
result.set(ID_C_c_type, ID_unsigned_short_int);
return result;
}
@ -136,7 +136,7 @@ Function: size_type
\*******************************************************************/
typet size_type()
unsignedbv_typet size_type()
{
// The size type varies. This is unsigned int on some systems,
// and unsigned long int on others,
@ -164,7 +164,7 @@ Function: signed_size_type
\*******************************************************************/
typet signed_size_type()
signedbv_typet signed_size_type()
{
// we presume this is the same as pointer difference
return pointer_diff_type();
@ -182,9 +182,9 @@ Function: signed_long_int_type
\*******************************************************************/
typet signed_long_int_type()
signedbv_typet signed_long_int_type()
{
typet result=signedbv_typet(config.ansi_c.long_int_width);
signedbv_typet result(config.ansi_c.long_int_width);
result.set(ID_C_c_type, ID_signed_long_int);
return result;
}
@ -201,9 +201,9 @@ Function: signed_long_long_int_type
\*******************************************************************/
typet signed_long_long_int_type()
signedbv_typet signed_long_long_int_type()
{
typet result=signedbv_typet(config.ansi_c.long_long_int_width);
signedbv_typet result(config.ansi_c.long_long_int_width);
result.set(ID_C_c_type, ID_signed_long_long_int);
return result;
}
@ -220,9 +220,9 @@ Function: unsigned_long_int_type
\*******************************************************************/
typet unsigned_long_int_type()
unsignedbv_typet unsigned_long_int_type()
{
typet result=unsignedbv_typet(config.ansi_c.long_int_width);
unsignedbv_typet result(config.ansi_c.long_int_width);
result.set(ID_C_c_type, ID_unsigned_long_int);
return result;
}
@ -239,9 +239,9 @@ Function: unsigned_long_long_int_type
\*******************************************************************/
typet unsigned_long_long_int_type()
unsignedbv_typet unsigned_long_long_int_type()
{
typet result=unsignedbv_typet(config.ansi_c.long_long_int_width);
unsignedbv_typet result(config.ansi_c.long_long_int_width);
result.set(ID_C_c_type, ID_unsigned_long_long_int);
return result;
}
@ -276,23 +276,25 @@ Function: char_type
\*******************************************************************/
typet char_type()
bitvector_typet char_type()
{
typet result;
// this can be signed or unsigned, depending on the architecture
if(config.ansi_c.char_is_unsigned)
result=unsignedbv_typet(config.ansi_c.char_width);
else
result=signedbv_typet(config.ansi_c.char_width);
// There are 3 char types, i.e., this one is
// different from either signed char or unsigned char!
result.set(ID_C_c_type, ID_char);
return result;
if(config.ansi_c.char_is_unsigned)
{
unsignedbv_typet result(config.ansi_c.char_width);
result.set(ID_C_c_type, ID_char);
return result;
}
else
{
signedbv_typet result(config.ansi_c.char_width);
result.set(ID_C_c_type, ID_char);
return result;
}
}
/*******************************************************************\
@ -307,12 +309,10 @@ Function: unsigned_char_type
\*******************************************************************/
typet unsigned_char_type()
unsignedbv_typet unsigned_char_type()
{
typet result=unsignedbv_typet(config.ansi_c.char_width);
unsignedbv_typet result(config.ansi_c.char_width);
result.set(ID_C_c_type, ID_unsigned_char);
return result;
}
@ -328,12 +328,10 @@ Function: signed_char_type
\*******************************************************************/
typet signed_char_type()
signedbv_typet signed_char_type()
{
typet result=signedbv_typet(config.ansi_c.char_width);
signedbv_typet result(config.ansi_c.char_width);
result.set(ID_C_c_type, ID_signed_char);
return result;
}
@ -349,18 +347,20 @@ Function: wchar_t_type
\*******************************************************************/
typet wchar_t_type()
bitvector_typet wchar_t_type()
{
typet result;
if(config.ansi_c.wchar_t_is_unsigned)
result=unsignedbv_typet(config.ansi_c.wchar_t_width);
{
unsignedbv_typet result(config.ansi_c.wchar_t_width);
result.set(ID_C_c_type, ID_wchar_t);
return result;
}
else
result=signedbv_typet(config.ansi_c.wchar_t_width);
result.set(ID_C_c_type, ID_wchar_t);
return result;
{
signedbv_typet result(config.ansi_c.wchar_t_width);
result.set(ID_C_c_type, ID_wchar_t);
return result;
}
}
/*******************************************************************\
@ -375,17 +375,13 @@ Function: char16_t_type
\*******************************************************************/
typet char16_t_type()
unsignedbv_typet char16_t_type()
{
typet result;
// Types char16_t and char32_t denote distinct types with the same size,
// signedness, and alignment as uint_least16_t and uint_least32_t,
// respectively, in <stdint.h>, called the underlying types.
result=unsignedbv_typet(16);
unsignedbv_typet result(16);
result.set(ID_C_c_type, ID_char16_t);
return result;
}
@ -401,17 +397,13 @@ Function: char32_t_type
\*******************************************************************/
typet char32_t_type()
unsignedbv_typet char32_t_type()
{
typet result;
// Types char16_t and char32_t denote distinct types with the same size,
// signedness, and alignment as uint_least16_t and uint_least32_t,
// respectively, in <stdint.h>, called the underlying types.
result=unsignedbv_typet(32);
unsignedbv_typet result(32);
result.set(ID_C_c_type, ID_char32_t);
return result;
}
@ -427,23 +419,23 @@ Function: float_type
\*******************************************************************/
typet float_type()
bitvector_typet float_type()
{
typet result;
if(config.ansi_c.use_fixed_for_float)
{
fixedbv_typet tmp;
tmp.set_width(config.ansi_c.single_width);
tmp.set_integer_bits(config.ansi_c.single_width/2);
result=tmp;
fixedbv_typet result;
result.set_width(config.ansi_c.single_width);
result.set_integer_bits(config.ansi_c.single_width/2);
result.set(ID_C_c_type, ID_float);
return result;
}
else
result=ieee_float_spect::single_precision().to_type();
result.set(ID_C_c_type, ID_float);
return result;
{
floatbv_typet result=
ieee_float_spect::single_precision().to_type();
result.set(ID_C_c_type, ID_float);
return result;
}
}
/*******************************************************************\
@ -458,23 +450,23 @@ Function: double_type
\*******************************************************************/
typet double_type()
bitvector_typet double_type()
{
typet result;
if(config.ansi_c.use_fixed_for_float)
{
fixedbv_typet tmp;
tmp.set_width(config.ansi_c.double_width);
tmp.set_integer_bits(config.ansi_c.double_width/2);
result=tmp;
fixedbv_typet result;
result.set_width(config.ansi_c.double_width);
result.set_integer_bits(config.ansi_c.double_width/2);
result.set(ID_C_c_type, ID_double);
return result;
}
else
result=ieee_float_spect::double_precision().to_type();
result.set(ID_C_c_type, ID_double);
return result;
{
floatbv_typet result=
ieee_float_spect::double_precision().to_type();
result.set(ID_C_c_type, ID_double);
return result;
}
}
/*******************************************************************\
@ -489,19 +481,19 @@ Function: long_double_type
\*******************************************************************/
typet long_double_type()
bitvector_typet long_double_type()
{
typet result;
if(config.ansi_c.use_fixed_for_float)
{
fixedbv_typet tmp;
tmp.set_width(config.ansi_c.long_double_width);
tmp.set_integer_bits(config.ansi_c.long_double_width/2);
result=tmp;
fixedbv_typet result;
result.set_width(config.ansi_c.long_double_width);
result.set_integer_bits(config.ansi_c.long_double_width/2);
result.set(ID_C_c_type, ID_long_double);
return result;
}
else
{
floatbv_typet result;
if(config.ansi_c.long_double_width==128)
result=ieee_float_spect::quadruple_precision().to_type();
else if(config.ansi_c.long_double_width==64)
@ -520,11 +512,11 @@ typet long_double_type()
}
else
assert(false);
result.set(ID_C_c_type, ID_long_double);
return result;
}
result.set(ID_C_c_type, ID_long_double);
return result;
}
/*******************************************************************\
@ -539,26 +531,25 @@ Function: gcc_float128_type
\*******************************************************************/
typet gcc_float128_type()
bitvector_typet gcc_float128_type()
{
typet result;
// not same as long double!
if(config.ansi_c.use_fixed_for_float)
{
fixedbv_typet tmp;
tmp.set_width(128);
tmp.set_integer_bits(128/2);
result=tmp;
fixedbv_typet result;
result.set_width(128);
result.set_integer_bits(128/2);
result.set(ID_C_c_type, ID_gcc_float128);
return result;
}
else
{
result=ieee_float_spect::quadruple_precision().to_type();
floatbv_typet result=
ieee_float_spect::quadruple_precision().to_type();
result.set(ID_C_c_type, ID_gcc_float128);
return result;
}
// not same as long double!
result.set(ID_C_c_type, ID_gcc_float128);
return result;
}
/*******************************************************************\
@ -573,7 +564,7 @@ Function: pointer_diff_type
\*******************************************************************/
typet pointer_diff_type()
signedbv_typet pointer_diff_type()
{
// The pointer-diff type varies. This is signed int on some systems,
// and signed long int on others, and signed long long on say Windows.
@ -600,7 +591,7 @@ Function: pointer_type
\*******************************************************************/
typet pointer_type(const typet &subtype)
pointer_typet pointer_type(const typet &subtype)
{
return pointer_typet(subtype);
}
@ -617,7 +608,7 @@ Function: reference_type
\*******************************************************************/
typet reference_type(const typet &subtype)
reference_typet reference_type(const typet &subtype)
{
return reference_typet(subtype);
}
@ -651,9 +642,9 @@ Function: gcc_unsigned_int128_type
\*******************************************************************/
typet gcc_unsigned_int128_type()
unsignedbv_typet gcc_unsigned_int128_type()
{
typet result=unsignedbv_typet(128);
unsignedbv_typet result(128);
result.set(ID_C_c_type, ID_unsigned_int128);
return result;
}
@ -670,9 +661,9 @@ Function: gcc_signed_int128_type
\*******************************************************************/
typet gcc_signed_int128_type()
signedbv_typet gcc_signed_int128_type()
{
typet result=signedbv_typet(128);
signedbv_typet result(128);
result.set(ID_C_c_type, ID_signed_int128);
return result;
}

56
src/util/c_types.h
View File

@ -9,39 +9,39 @@ Author: Daniel Kroening, kroening@kroening.com
#ifndef CPROVER_UTIL_C_TYPES_H
#define CPROVER_UTIL_C_TYPES_H
#include "type.h"
#include "std_types.h"
typet index_type();
typet enum_constant_type();
typet signed_int_type();
typet unsigned_int_type();
typet signed_long_int_type();
typet signed_short_int_type();
typet unsigned_short_int_type();
typet signed_long_long_int_type();
typet unsigned_long_int_type();
typet unsigned_long_long_int_type();
bitvector_typet index_type();
bitvector_typet enum_constant_type();
signedbv_typet signed_int_type();
unsignedbv_typet unsigned_int_type();
signedbv_typet signed_long_int_type();
signedbv_typet signed_short_int_type();
unsignedbv_typet unsigned_short_int_type();
signedbv_typet signed_long_long_int_type();
unsignedbv_typet unsigned_long_int_type();
unsignedbv_typet unsigned_long_long_int_type();
typet c_bool_type();
typet char_type();
typet unsigned_char_type();
typet signed_char_type();
typet wchar_t_type();
typet char16_t_type();
typet char32_t_type();
typet float_type();
typet double_type();
typet long_double_type();
typet gcc_float128_type();
typet gcc_unsigned_int128_type();
typet gcc_signed_int128_type();
typet size_type();
typet signed_size_type();
typet pointer_diff_type();
typet pointer_type(const typet &);
bitvector_typet char_type();
unsignedbv_typet unsigned_char_type();
signedbv_typet signed_char_type();
bitvector_typet wchar_t_type();
unsignedbv_typet char16_t_type();
unsignedbv_typet char32_t_type();
bitvector_typet float_type();
bitvector_typet double_type();
bitvector_typet long_double_type();
bitvector_typet gcc_float128_type();
unsignedbv_typet gcc_unsigned_int128_type();
signedbv_typet gcc_signed_int128_type();
unsignedbv_typet size_type();
signedbv_typet signed_size_type();
signedbv_typet pointer_diff_type();
pointer_typet pointer_type(const typet &);
typet void_type();
// This is for Java and C++
typet reference_type(const typet &);
reference_typet reference_type(const typet &);
// Turns an ID_C_c_type into a string, e.g.,
// ID_signed_int gets "signed int".