From 17fdcb6ffb1652a0a2cdbd1775baf7fddad1dd5a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 25 May 2026 18:51:53 +0000 Subject: [PATCH] dump-c: sign-extend signed bit-field temporaries When goto-conversion lowers a chained assignment `outer = bf = expr` through a bit-field lvalue, it introduces a temporary symbol whose declared type is the bit-field type. `goto_program2code` rewrites that temporary's type to the bit-field's underlying integer type and previously masked the initialiser with `& ((1 << N) - 1)` to model the bit-field truncation. For unsigned bit-fields the AND-mask is enough, but for signed bit-fields the value of `bf = expr` is the value of `bf` after the assignment - i.e. the masked value sign-extended to the underlying type (per C11 6.5.16.1p3). Without the sign extension, the temporary held an unsigned-truncated value, so subsequent uses of it (here: the chained assignment to `outer`) observed the wrong value. The original program continued to verify correctly under CBMC, but the C code emitted by `--dump-c` no longer agreed with the source - which CSmith picks up as a checksum mismatch. Apply branchless sign extension `((v & mask) ^ sign_bit) - sign_bit` for the signed-and-narrower case. This expression stays within the bit-field's value range and so triggers neither signed overflow nor implementation-defined shift behaviour in the dumped C. Co-authored-by: Kiro --- .../dump-bitfield-chained-assign/main.c | 25 +++++++++++++++ .../dump-bitfield-chained-assign/test.desc | 15 +++++++++ src/goto-instrument/goto_program2code.cpp | 31 +++++++++++++++++-- 3 files changed, 68 insertions(+), 3 deletions(-) create mode 100644 regression/goto-instrument/dump-bitfield-chained-assign/main.c create mode 100644 regression/goto-instrument/dump-bitfield-chained-assign/test.desc diff --git a/regression/goto-instrument/dump-bitfield-chained-assign/main.c b/regression/goto-instrument/dump-bitfield-chained-assign/main.c new file mode 100644 index 00000000000..5d413897bef --- /dev/null +++ b/regression/goto-instrument/dump-bitfield-chained-assign/main.c @@ -0,0 +1,25 @@ +#include + +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; +} diff --git a/regression/goto-instrument/dump-bitfield-chained-assign/test.desc b/regression/goto-instrument/dump-bitfield-chained-assign/test.desc new file mode 100644 index 00000000000..4c0c3c2de24 --- /dev/null +++ b/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). diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index e5978ae1d5a..b3567614531 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/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}; + } } }