From a59f36b3a016e9479223b54e119603559213bba2 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 23 Feb 2021 07:41:32 +0000 Subject: [PATCH] Assignment side effects may require additional temporaries An assignment may invalidate pointers used in the left-hand side. In case the result of the assignment is used, we therefore cannot re-use the left-hand side to represent the result. Instead, introduce temporaries as needed to store the right-hand side value, and use the temporary to represent the result. Fixes: #5857 --- regression/cbmc/Sideeffects8/main.c | 18 ++++++++++ regression/cbmc/Sideeffects8/test.desc | 12 +++++++ src/goto-programs/goto_clean_expr.cpp | 5 +-- src/goto-programs/goto_convert_class.h | 4 ++- .../goto_convert_side_effect.cpp | 34 ++++++++++++++++--- 5 files changed, 66 insertions(+), 7 deletions(-) create mode 100644 regression/cbmc/Sideeffects8/main.c create mode 100644 regression/cbmc/Sideeffects8/test.desc diff --git a/regression/cbmc/Sideeffects8/main.c b/regression/cbmc/Sideeffects8/main.c new file mode 100644 index 00000000000..2e0734b9471 --- /dev/null +++ b/regression/cbmc/Sideeffects8/main.c @@ -0,0 +1,18 @@ +#include +#include + +struct A +{ + struct A *p; +}; + +int main(void) +{ + struct A x = {&x}; + struct A *r = x.p->p = NULL; + assert(r == NULL); + + struct A arr[2] = {arr, 0}; + r = arr[0].p->p += 1; + assert(r == &arr[1]); +} diff --git a/regression/cbmc/Sideeffects8/test.desc b/regression/cbmc/Sideeffects8/test.desc new file mode 100644 index 00000000000..565f30cc839 --- /dev/null +++ b/regression/cbmc/Sideeffects8/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--pointer-check +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +Invariant check failed +^warning: ignoring +-- +Assignments can affect dereferences occuring with the LHS, and thus may require +introducing temporaries. diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp index 3a023894d39..3539d1e76b3 100644 --- a/src/goto-programs/goto_clean_expr.cpp +++ b/src/goto-programs/goto_clean_expr.cpp @@ -409,7 +409,8 @@ void goto_convertt::clean_expr( if(expr.id()==ID_side_effect) { - remove_side_effect(to_side_effect_expr(expr), dest, mode, result_is_used); + remove_side_effect( + to_side_effect_expr(expr), dest, mode, result_is_used, false); } else if(expr.id()==ID_compound_literal) { @@ -482,7 +483,7 @@ void goto_convertt::clean_expr_address_of( } else if(expr.id() == ID_side_effect) { - remove_side_effect(to_side_effect_expr(expr), dest, mode, true); + remove_side_effect(to_side_effect_expr(expr), dest, mode, true, true); } else Forall_operands(it, expr) diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h index 1bf726288a8..e85132e9a05 100644 --- a/src/goto-programs/goto_convert_class.h +++ b/src/goto-programs/goto_convert_class.h @@ -102,11 +102,13 @@ class goto_convertt:public messaget side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, - bool result_is_used); + bool result_is_used, + bool address_taken); void remove_assignment( side_effect_exprt &expr, goto_programt &dest, bool result_is_used, + bool address_taken, const irep_idt &mode); void remove_pre( side_effect_exprt &expr, diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index fe72f3531ae..68f54e1e6a8 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -38,13 +38,25 @@ void goto_convertt::remove_assignment( side_effect_exprt &expr, goto_programt &dest, bool result_is_used, + bool address_taken, const irep_idt &mode) { const irep_idt statement=expr.get_statement(); + optionalt replacement_expr_opt; + if(statement==ID_assign) { auto &old_assignment = to_side_effect_expr_assign(expr); + + if(result_is_used && !address_taken && needs_cleaning(old_assignment.lhs())) + { + if(!old_assignment.rhs().is_constant()) + make_temp_symbol(old_assignment.rhs(), "assign", dest, mode); + + replacement_expr_opt = old_assignment.rhs(); + } + exprt new_lhs = skip_typecast(old_assignment.lhs()); exprt new_rhs = typecast_exprt::conditional_cast(old_assignment.rhs(), new_lhs.type()); @@ -113,10 +125,17 @@ void goto_convertt::remove_assignment( rhs.type() = to_binary_expr(expr).op0().type(); rhs.add_source_location() = expr.source_location(); + if( + result_is_used && !address_taken && + needs_cleaning(to_binary_expr(expr).op0())) + { + make_temp_symbol(rhs, "assign", dest, mode); + replacement_expr_opt = rhs; + } + exprt new_lhs = skip_typecast(to_binary_expr(expr).op0()); rhs = typecast_exprt::conditional_cast(rhs, new_lhs.type()); rhs.add_source_location() = expr.source_location(); - code_assignt assignment(new_lhs, rhs); assignment.add_source_location()=expr.source_location(); @@ -126,7 +145,13 @@ void goto_convertt::remove_assignment( UNREACHABLE; // revert assignment in the expression to its LHS - if(result_is_used) + if(replacement_expr_opt.has_value()) + { + exprt new_lhs = + typecast_exprt::conditional_cast(*replacement_expr_opt, expr.type()); + expr.swap(new_lhs); + } + else if(result_is_used) { exprt lhs = to_binary_expr(expr).op0(); // assign_* statements can have an lhs operand with a different type than @@ -556,7 +581,8 @@ void goto_convertt::remove_side_effect( side_effect_exprt &expr, goto_programt &dest, const irep_idt &mode, - bool result_is_used) + bool result_is_used, + bool address_taken) { const irep_idt &statement=expr.get_statement(); @@ -575,7 +601,7 @@ void goto_convertt::remove_side_effect( statement==ID_assign_ashr || statement==ID_assign_shl || statement==ID_assign_mod) - remove_assignment(expr, dest, result_is_used, mode); + remove_assignment(expr, dest, result_is_used, address_taken, mode); else if(statement==ID_postincrement || statement==ID_postdecrement) remove_post(expr, dest, mode, result_is_used);