Merge pull request #5858 from tautschnig/fix-5857

Assignment side effects may require additional temporaries

Author: tautschnig

regression/cbmc/Sideeffects8/main.c

@@ -0,0 +1,18 @@
+#include <assert.h>
+#include <stdlib.h>
+
+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]);
+}

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.

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)

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,

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<exprt> 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);