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

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_convert_side_effect.cpp

@@ -42,9 +42,20 @@ void goto_convertt::remove_assignment(
 {
   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 && 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,6 +124,12 @@ void goto_convertt::remove_assignment(
     rhs.type() = to_binary_expr(expr).op0().type();
     rhs.add_source_location() = expr.source_location();
 
+    if(result_is_used && 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();
@@ -128,7 +145,7 @@ void goto_convertt::remove_assignment(
   // revert assignment in the expression to its LHS
   if(result_is_used)
   {
-    exprt lhs = to_binary_expr(expr).op0();
+    exprt lhs = replacement_expr_opt.value_or(to_binary_expr(expr).op0());
     // assign_* statements can have an lhs operand with a different type than
     // that of the overall expression, because of integer promotion (which may
     // have introduced casts to the lhs).