From ed713ff58f5649da97910dadfd4849ffd92c4369 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 24 Nov 2023 16:11:37 +0000 Subject: [PATCH] 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 147b12991000..670e41668092 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 000000000000..66f8f98e29cc --- /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 000000000000..9efefbc7362d --- /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 043dafd0657a..df210afc6cf0 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();