From dbe6455944ec676a77fb3483defb0ad7bada0781 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 14 Dec 2023 17:58:24 +0000 Subject: [PATCH 1/2] Dump-C: do not produce c_bit_field declarations goto-program conversion may introduce temporaries of c_bit_field type. These, however, are not permitted outside structs in C. Instead, change their types to their underlying types and use a bit mask to fix up initial values. --- src/goto-instrument/goto_program2code.cpp | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index 1590716b179..d69a4bb2fbc 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_program2code.h" #include +#include #include #include #include @@ -1435,6 +1436,19 @@ void goto_program2codet::cleanup_code( if(code.op0().type().id()==ID_array) cleanup_expr(to_array_type(code.op0().type()).size(), true); + else if(code.op0().type().id() == ID_c_bit_field) + { + c_bit_field_typet original_type = to_c_bit_field_type(code.op0().type()); + bitvector_typet bv_type = + to_bitvector_type(original_type.underlying_type()); + code.op0().type() = bv_type; + if(code.operands().size() == 2) + { + exprt bit_mask = + from_integer(power(2, original_type.get_width()) - 1, bv_type); + code.op1() = bitand_exprt{code.op1(), bit_mask}; + } + } add_local_types(code.op0().type()); From 16c0cbe0cab29720e2b5965da9b891d88429b658 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 24 Nov 2023 16:11:37 +0000 Subject: [PATCH 2/2] Assignments to bit-fields yield results of bit-field type Do not pre-emptively cast side effects over bit-fields to the underlying type. sizeof just has a very peculiar semantics, which is discussed in https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2958.htm. Issue was found by CSmith (test generated with random seed 1700653858). --- regression/cbmc/Bitfields1/main.c | 6 +++- regression/cbmc/Bitfields5/main.c | 36 +++++++++++++++++++++ regression/cbmc/Bitfields5/test.desc | 8 +++++ src/ansi-c/c_typecheck_expr.cpp | 48 ++++++++++++++++++++++++---- 4 files changed, 90 insertions(+), 8 deletions(-) create mode 100644 regression/cbmc/Bitfields5/main.c create mode 100644 regression/cbmc/Bitfields5/test.desc diff --git a/regression/cbmc/Bitfields1/main.c b/regression/cbmc/Bitfields1/main.c index 147b1299100..670e4166809 100644 --- a/regression/cbmc/Bitfields1/main.c +++ b/regression/cbmc/Bitfields1/main.c @@ -51,9 +51,13 @@ int main() { bf.d=2; assert(bf.d==1); - // assignments have the underlying type + // assignments have the underlying type, except for GCC assert(sizeof(bf.d=1)==sizeof(_Bool)); +#if defined(__GNUC__) && !defined(__INTEL_COMPILER) && !defined(__clang__) + assert(sizeof(bf.a += 1) == 1); +#else assert(sizeof(bf.a += 1) == sizeof(unsigned long)); +#endif bf.Type=IntelCacheTrace; diff --git a/regression/cbmc/Bitfields5/main.c b/regression/cbmc/Bitfields5/main.c new file mode 100644 index 00000000000..66f8f98e29c --- /dev/null +++ b/regression/cbmc/Bitfields5/main.c @@ -0,0 +1,36 @@ +#include +#include + +struct S0 +{ + unsigned f2 : CHAR_BIT + 1; + int x; +}; + +#ifdef _MSC_VER +# define _Static_assert static_assert +#endif + +int main() +{ + struct S0 g = {0}; + // All compilers in compiler explorer appear to agree that comma and + // assignment expressions over bit-fields permit the use of sizeof. With GCC, + // the result is the declared width (rounded to bytes), all others use the + // size of the underlying type. + // https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2958.htm + // for a discussion that this isn't actually specified (while being a + // sizeof/typeof peculiarity) +#if defined(__GNUC__) && !defined(__INTEL_COMPILER) && !defined(__clang__) +# define WIDTH 2 +#else +# define WIDTH sizeof(unsigned) +#endif + _Static_assert(sizeof(++g.f2) == WIDTH, ""); + _Static_assert(sizeof(0, g.f2) == WIDTH, ""); + _Static_assert(sizeof(g.f2 = g.f2) == WIDTH, ""); + if(g.f2 <= -1) + assert(0); + if((g.f2 = g.f2) <= -1) + assert(0); +} diff --git a/regression/cbmc/Bitfields5/test.desc b/regression/cbmc/Bitfields5/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/Bitfields5/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 043dafd0657..df210afc6cf 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -970,9 +970,39 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr) if(type.id()==ID_c_bit_field) { - error().source_location = expr.source_location(); - error() << "sizeof cannot be applied to bit fields" << eom; - throw 0; + // only comma or side-effect expressions are permitted + const exprt &op = skip_typecast(to_unary_expr(as_const(expr)).op()); + if(op.id() == ID_comma || op.id() == ID_side_effect) + { + const c_bit_field_typet &bf_type = to_c_bit_field_type(type); + if(config.ansi_c.mode == configt::ansi_ct::flavourt::GCC) + { + new_expr = from_integer( + (bf_type.get_width() + config.ansi_c.char_width - 1) / + config.ansi_c.char_width, + size_type()); + } + else + { + auto size_of_opt = size_of_expr(bf_type.underlying_type(), *this); + + if(!size_of_opt.has_value()) + { + error().source_location = expr.source_location(); + error() << "type has no size: " + << to_string(bf_type.underlying_type()) << eom; + throw 0; + } + + new_expr = size_of_opt.value(); + } + } + else + { + error().source_location = expr.source_location(); + error() << "sizeof cannot be applied to bit fields" << eom; + throw 0; + } } else if(type.id() == ID_bool) { @@ -1876,8 +1906,11 @@ void c_typecheck_baset::typecheck_expr_side_effect(side_effect_exprt &expr) { // promote to underlying type typet underlying_type = to_c_bit_field_type(type0).underlying_type(); + typet type_before{type0}; to_unary_expr(expr).op() = typecast_exprt(op0, underlying_type); expr.type()=underlying_type; + typecast_exprt result{expr, type_before}; + expr.swap(result); } else if(type0.id() == ID_bool || type0.id() == ID_c_bool) { @@ -4345,10 +4378,11 @@ void c_typecheck_baset::typecheck_side_effect_assignment( } // Add a cast to the underlying type for bit fields. - // In particular, sizeof(s.f=1) works for bit fields. - if(op0.type().id()==ID_c_bit_field) - op0 = - typecast_exprt(op0, to_c_bit_field_type(op0.type()).underlying_type()); + if(op0.type() != op1.type() && op0.type().id() == ID_c_bit_field) + { + op1 = + typecast_exprt{op1, to_c_bit_field_type(op0.type()).underlying_type()}; + } const typet o_type0=op0.type(); const typet o_type1=op1.type();