Merge pull request #7270 from tautschnig/bugfixes/bitfield-side-effect

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

Author: kroening

regression/cbmc/Bitfields4/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdint.h>
+
+struct S0
+{
+  signed int f1 : 2;
+};
+
+int main(int argc, char *argv[])
+{
+  struct S0 l_4590 = {1};
+  uint32_t g_307 = ++l_4590.f1;
+  assert(g_307 == 4294967294u);
+
+  l_4590 = (struct S0){1};
+  uint32_t g_308 = l_4590.f1 += 1;
+  assert(g_308 == 4294967294u);
+
+  uint32_t g_309 = l_4590.f1 = 62378u;
+  assert(g_309 == 4294967294u);
+}

regression/cbmc/Bitfields4/test.desc

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

src/ansi-c/expr2c.cpp

@@ -1834,8 +1834,12 @@ std::string expr2ct::convert_constant(
   {
     const auto width = to_bitvector_type(type).get_width();
 
-    mp_integer int_value =
-      bvrep2integer(value, width, type.id() == ID_signedbv);
+    mp_integer int_value = bvrep2integer(
+      value,
+      width,
+      type.id() == ID_signedbv ||
+        (type.id() == ID_c_bit_field &&
+         to_c_bit_field_type(type).underlying_type().id() == ID_signedbv));
 
     const irep_idt &c_type =
       type.id() == ID_c_bit_field

src/goto-programs/goto_clean_expr.cpp

@@ -392,12 +392,12 @@ void goto_convertt::clean_expr(
         exprt new_lhs = skip_typecast(lhs);
         exprt new_rhs = typecast_exprt::conditional_cast(
           side_effect_assign.rhs(), new_lhs.type());
-        code_assignt assignment(std::move(new_lhs), std::move(new_rhs));
+        code_assignt assignment(std::move(new_lhs), new_rhs);
         assignment.add_source_location()=expr.source_location();
         convert_assign(assignment, dest, mode);
 
         if(result_is_used)
-          expr = must_use_rhs ? side_effect_assign.rhs() : lhs;
+          expr = must_use_rhs ? new_rhs : lhs;
         else
           expr.make_nil();
         return;

src/goto-programs/goto_convert_side_effect.cpp

@@ -49,6 +49,7 @@ void goto_convertt::remove_assignment(
   if(statement==ID_assign)
   {
     auto &old_assignment = to_side_effect_expr_assign(expr);
+    exprt new_lhs = skip_typecast(old_assignment.lhs());
 
     if(
       result_is_used && !address_taken &&
@@ -57,10 +58,10 @@ void goto_convertt::remove_assignment(
       if(!old_assignment.rhs().is_constant())
         make_temp_symbol(old_assignment.rhs(), "assign", dest, mode);
 
-      replacement_expr_opt = old_assignment.rhs();
+      replacement_expr_opt =
+        typecast_exprt::conditional_cast(old_assignment.rhs(), new_lhs.type());
     }
 
-    exprt new_lhs = skip_typecast(old_assignment.lhs());
     exprt new_rhs =
       typecast_exprt::conditional_cast(old_assignment.rhs(), new_lhs.type());
     code_assignt new_assignment(std::move(new_lhs), std::move(new_rhs));
@@ -115,6 +116,7 @@ void goto_convertt::remove_assignment(
     }
 
     const binary_exprt &binary_expr = to_binary_expr(expr);
+    exprt new_lhs = skip_typecast(binary_expr.op0());
     const typet &op0_type = binary_expr.op0().type();
 
     PRECONDITION(
@@ -129,10 +131,10 @@ void goto_convertt::remove_assignment(
       assignment_lhs_needs_temporary(binary_expr.op0()))
     {
       make_temp_symbol(rhs, "assign", dest, mode);
-      replacement_expr_opt = rhs;
+      replacement_expr_opt =
+        typecast_exprt::conditional_cast(rhs, new_lhs.type());
     }
 
-    exprt new_lhs = skip_typecast(binary_expr.op0());
     rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type());
     rhs.add_source_location() = expr.source_location();
     code_assignt assignment(new_lhs, rhs);