Assignments to bit-fields yield results of bit-field type

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;
 

regression/cbmc/Bitfields5/main.c

@@ -0,0 +1,36 @@
+#include <assert.h>
+#include <limits.h>
+
+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);
+}

regression/cbmc/Bitfields5/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/ansi-c/c_typecheck_expr.cpp

@@ -970,9 +970,39 @@
 
   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 @@
     {
       // 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 @@
   }
 
   // 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();

src/goto-instrument/goto_program2code.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "goto_program2code.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/c_types.h>
 #include <util/expr_util.h>
 #include <util/ieee_float.h>
@@ -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());