From 2e11fef1da2d29267e9c935d85d83d07e16adcfa Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 25 May 2017 19:59:11 +0100 Subject: [PATCH] the c_types now have stronger C++ types --- src/ansi-c/ansi_c_convert_type.cpp | 41 ++++-- src/ansi-c/c_typecheck_type.cpp | 67 ++++++--- src/util/c_types.cpp | 217 ++++++++++++++--------------- src/util/c_types.h | 58 ++++---- 4 files changed, 216 insertions(+), 167 deletions(-) diff --git a/src/ansi-c/ansi_c_convert_type.cpp b/src/ansi-c/ansi_c_convert_type.cpp index d4777888b7e..62ff07f127e 100644 --- a/src/ansi-c/ansi_c_convert_type.cpp +++ b/src/ansi-c/ansi_c_convert_type.cpp @@ -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 { diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index 805293f7f0f..f4e3d6e397f 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/src/ansi-c/c_typecheck_type.cpp @@ -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(); diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp index 5719bb22ffe..9f87d854194 100644 --- a/src/util/c_types.cpp +++ b/src/util/c_types.cpp @@ -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 , 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 , 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); + result.set(ID_C_c_type, ID_long_double); - return result; + 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; } diff --git a/src/util/c_types.h b/src/util/c_types.h index 08acf393bab..5886c10584d 100644 --- a/src/util/c_types.h +++ b/src/util/c_types.h @@ -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" - -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(); +#include "std_types.h" + +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".