Merge pull request #5860 from tautschnig/fixup-5857

fixup! Assignment side effects may require additional temporaries

Author: tautschnig

regression/cbmc/Sideeffects8/main.c

@@ -6,13 +6,30 @@ struct A
   struct A *p;
 };
 
+struct A *return_null()
+{
+  return NULL;
+}
+
 int main(void)
 {
   struct A x = {&x};
   struct A *r = x.p->p = NULL;
   assert(r == NULL);
 
+  struct A x2 = {&x2};
+  r = x2.p->p = return_null();
+  assert(r == NULL);
+
   struct A arr[2] = {arr, 0};
   r = arr[0].p->p += 1;
   assert(r == &arr[1]);
+
+  struct A arr2[2] = {arr2, 0};
+  r = ++(arr2[0].p->p);
+  assert(r == &arr2[1]);
+
+  struct A arr3[2] = {arr3, 0};
+  r = (arr3[0].p->p)++;
+  assert(r == &arr3[0]);
 }

src/goto-programs/goto_clean_expr.cpp

@@ -374,6 +374,16 @@ void goto_convertt::clean_expr(
         clean_expr(side_effect_assign.lhs(), dest, mode);
         exprt lhs = side_effect_assign.lhs();
 
+        const bool must_use_rhs = needs_cleaning(lhs);
+        if(must_use_rhs)
+        {
+          remove_function_call(
+            to_side_effect_expr_function_call(side_effect_assign.rhs()),
+            dest,
+            mode,
+            true);
+        }
+
         // turn into code
         code_assignt assignment;
         assignment.lhs()=lhs;
@@ -382,7 +392,7 @@ void goto_convertt::clean_expr(
         convert_assign(assignment, dest, mode);
 
         if(result_is_used)
-          expr.swap(lhs);
+          expr = must_use_rhs ? side_effect_assign.rhs() : lhs;
         else
           expr.make_nil();
         return;

src/goto-programs/goto_convert_class.h

@@ -114,6 +114,7 @@ class goto_convertt:public messaget
     side_effect_exprt &expr,
     goto_programt &dest,
     bool result_is_used,
+    bool address_taken,
     const irep_idt &mode);
   void remove_post(
     side_effect_exprt &expr,

src/goto-programs/goto_convert_side_effect.cpp

@@ -181,6 +181,7 @@ void goto_convertt::remove_pre(
   side_effect_exprt &expr,
   goto_programt &dest,
   bool result_is_used,
+  bool address_taken,
   const irep_idt &mode)
 {
   INVARIANT_WITH_DIAGNOSTICS(
@@ -234,16 +235,26 @@ void goto_convertt::remove_pre(
   rhs.add_to_operands(op, std::move(constant));
   rhs.type() = op.type();
 
+  const bool cannot_use_lhs =
+    result_is_used && !address_taken && needs_cleaning(op);
+  if(cannot_use_lhs)
+    make_temp_symbol(rhs, "pre", dest, mode);
+
   code_assignt assignment(op, rhs);
   assignment.add_source_location()=expr.find_source_location();
 
   convert(assignment, dest, mode);
 
   if(result_is_used)
   {
-    // revert to argument of pre-inc/pre-dec
-    exprt tmp = op;
-    expr.swap(tmp);
+    if(cannot_use_lhs)
+      expr.swap(rhs);
+    else
+    {
+      // revert to argument of pre-inc/pre-dec
+      exprt tmp = op;
+      expr.swap(tmp);
+    }
   }
   else
     expr.make_nil();
@@ -607,7 +618,7 @@ void goto_convertt::remove_side_effect(
     remove_post(expr, dest, mode, result_is_used);
   else if(statement==ID_preincrement ||
           statement==ID_predecrement)
-    remove_pre(expr, dest, result_is_used, mode);
+    remove_pre(expr, dest, result_is_used, address_taken, mode);
   else if(statement==ID_cpp_new ||
           statement==ID_cpp_new_array)
     remove_cpp_new(expr, dest, result_is_used);