From 623cde5a038699376118c754cd46e11b38497bb8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Sat, 22 Oct 2022 21:13:59 +0000 Subject: [PATCH] Assignments to bit-fields yield results of bit-field type Do not use the type of the assignment expression (which is the underlying type) to store the result. Also fixes C pretty-printing of bit-field typed constants. Issue was found by CSmith (test generated with random seed 1665747314). --- regression/cbmc/Bitfields4/main.c | 21 +++++++++++++++++++ regression/cbmc/Bitfields4/test.desc | 8 +++++++ src/ansi-c/expr2c.cpp | 8 +++++-- src/goto-programs/goto_clean_expr.cpp | 4 ++-- .../goto_convert_side_effect.cpp | 10 +++++---- 5 files changed, 43 insertions(+), 8 deletions(-) create mode 100644 regression/cbmc/Bitfields4/main.c create mode 100644 regression/cbmc/Bitfields4/test.desc diff --git a/regression/cbmc/Bitfields4/main.c b/regression/cbmc/Bitfields4/main.c new file mode 100644 index 00000000000..2e7b4e33fa6 --- /dev/null +++ b/regression/cbmc/Bitfields4/main.c @@ -0,0 +1,21 @@ +#include +#include + +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); +} diff --git a/regression/cbmc/Bitfields4/test.desc b/regression/cbmc/Bitfields4/test.desc new file mode 100644 index 00000000000..9efefbc7362 --- /dev/null +++ b/regression/cbmc/Bitfields4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index d1e94046fef..cfc485b64cc 100644 --- a/src/ansi-c/expr2c.cpp +++ b/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 diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index 810302a27b6..16efaf32baa 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/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; diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index 0dc0ec40beb..db75e788cf4 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/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);