goto-convert: introduce assignment_lhs_needs_temporary

This introduces goto_convertt::assignment_lhs_needs_temporary, to be used
instead of needs_cleaning when determining whether to introduce a temporary
for the value of an assignment expression, compound assignment expression,
or pre- or post-increment or decrement operator.

This allows weakening the condition computed by needs_cleaning.

Author: kroening

src/goto-programs/goto_clean_expr.cpp

@@ -384,7 +384,7 @@ 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);
+        const bool must_use_rhs = assignment_lhs_needs_temporary(lhs);
         if(must_use_rhs)
         {
           remove_function_call(

src/goto-programs/goto_convert_class.h

@@ -89,6 +89,15 @@ class goto_convertt:public messaget
 
   static bool needs_cleaning(const exprt &expr);
 
+  // Do we need to introduce a temporary for the value of an assignment
+  // to the given lhs? E.g., a[i] needs a temporary as its value may change
+  // when i is changed; likewise, *p needs a temporary as its value may change
+  // when p is changed.
+  static bool assignment_lhs_needs_temporary(const exprt &lhs)
+  {
+    return lhs.id() != ID_symbol;
+  }
+
   void make_temp_symbol(
     exprt &expr,
     const std::string &suffix,

src/goto-programs/goto_convert_side_effect.cpp

@@ -50,7 +50,9 @@ void goto_convertt::remove_assignment(
   {
     auto &old_assignment = to_side_effect_expr_assign(expr);
 
-    if(result_is_used && !address_taken && needs_cleaning(old_assignment.lhs()))
+    if(
+      result_is_used && !address_taken &&
+      assignment_lhs_needs_temporary(old_assignment.lhs()))
     {
       if(!old_assignment.rhs().is_constant())
         make_temp_symbol(old_assignment.rhs(), "assign", dest, mode);
@@ -122,7 +124,9 @@ void goto_convertt::remove_assignment(
     exprt rhs = binary_exprt{binary_expr.op0(), new_id, binary_expr.op1()};
     rhs.add_source_location() = expr.source_location();
 
-    if(result_is_used && !address_taken && needs_cleaning(binary_expr.op0()))
+    if(
+      result_is_used && !address_taken &&
+      assignment_lhs_needs_temporary(binary_expr.op0()))
     {
       make_temp_symbol(rhs, "assign", dest, mode);
       replacement_expr_opt = rhs;
@@ -237,7 +241,7 @@ void goto_convertt::remove_pre(
   }
 
   const bool cannot_use_lhs =
-    result_is_used && !address_taken && needs_cleaning(lhs);
+    result_is_used && !address_taken && assignment_lhs_needs_temporary(lhs);
   if(cannot_use_lhs)
     make_temp_symbol(rhs, "pre", dest, mode);