dump-c: sign-extend signed bit-field temporaries

regression/goto-instrument/dump-bitfield-chained-assign/main.c

@@ -0,0 +1,25 @@
+#include <assert.h>
+
+struct S
+{
+  signed r : 2;
+};
+
+static int outer;
+static struct S s;
+
+int main(void)
+{
+  int v = 2;
+
+  // Per C11 6.5.16.1p3, the value of an assignment expression is the value of
+  // the left operand after the assignment. Storing 2 into a 2-bit signed
+  // bit-field yields -2 when read back, so both `outer` and `s.r` must equal
+  // -2 here.
+  outer = s.r = v;
+
+  assert(outer == -2);
+  assert((int)s.r == -2);
+
+  return 0;
+}

regression/goto-instrument/dump-bitfield-chained-assign/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+--dump-c
+VERIFICATION SUCCESSFUL
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This test must verify successfully also for the output generated using dump-c.
+A chained assignment `outer = bf = expr;` through a signed bit-field previously
+produced dump-c output that lost sign-extension semantics: the temporary
+holding the assignment value was masked but not sign-extended, so `outer`
+ended up with the unsigned-truncated value rather than the value of the
+bit-field after the assignment (per C11 6.5.16.1p3).

src/goto-instrument/goto_program2code.cpp

@@ -1444,9 +1444,34 @@ void goto_program2codet::cleanup_code(
       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};
+        const std::size_t bf_width = original_type.get_width();
+        exprt bit_mask = from_integer(power(2, bf_width) - 1, bv_type);
+        if(
+          bv_type.id() == ID_signedbv && bf_width >= 1 &&
+          bf_width < bv_type.get_width())
+        {
+          // For a signed bit-field that is narrower than its underlying type
+          // we need to sign-extend the stored value: writing to and reading
+          // back from such a bit-field yields a sign-extended value (per
+          // C11 6.5.16.1p3). Subsequent uses of this temporary - which we
+          // are about to give the underlying integer type - must therefore
+          // already observe the sign-extended value. We use the well-defined
+          // branchless sign-extension formula
+          //   ((v & mask) ^ sign_bit) - sign_bit
+          // where mask    = (1 << N) - 1
+          //       sign_bit = 1 << (N - 1)
+          // and N is the bit-field width. The intermediate result stays
+          // within the bit-field's value range, so this expression triggers
+          // neither signed overflow nor implementation-defined shifts.
+          const exprt sign_bit = from_integer(power(2, bf_width - 1), bv_type);
+          code.op1() = minus_exprt{
+            bitxor_exprt{bitand_exprt{code.op1(), bit_mask}, sign_bit},
+            sign_bit};
+        }
+        else
+        {
+          code.op1() = bitand_exprt{code.op1(), bit_mask};
+        }
       }
     }