clean_expr returns exprt and takes argument by copy

This makes the information flow clearer, avoid errors where a subtype of
exprt could be passed as argument and its id mutated to something
inconsistent with this subtype, and avoids having to make explicit
copies in the places where the function is called.

Author: romainbrenguier

src/goto-symex/goto_symex.h

@@ -305,7 +305,7 @@ class goto_symext
   /// \param expr: The expression to clean up
   /// \param state
   /// \param write
-  void clean_expr(exprt &expr, statet &state, bool write);
+  exprt clean_expr(exprt expr, statet &state, bool write);
 
   void trigger_auto_object(const exprt &, statet &);
   void initialize_auto_object(const exprt &, statet &);

src/goto-symex/symex_assign.cpp

@@ -27,14 +27,12 @@ Author: Daniel Kroening, [email protected]
 
 void goto_symext::symex_assign(statet &state, const code_assignt &code)
 {
-  exprt lhs=code.lhs();
-  exprt rhs=code.rhs();
+  exprt lhs = clean_expr(code.lhs(), state, true);
+  exprt rhs = clean_expr(code.rhs(), state, false);
 
   DATA_INVARIANT(
     lhs.type() == rhs.type(), "assignments must be type consistent");
 
-  clean_expr(lhs, state, true);
-  clean_expr(rhs, state, false);
 
   if(rhs.id()==ID_side_effect)
   {

src/goto-symex/symex_builtin_functions.cpp

@@ -290,7 +290,7 @@ void goto_symext::symex_va_start(
     state.symbol_table);
   va_array.value = array;
 
-  clean_expr(array, state, false);
+  array = clean_expr(std::move(array), state, false);
   array = state.rename(std::move(array), ns).get();
   do_simplify(array);
   symex_assign(state, code_assignt{va_array.symbol_expr(), std::move(array)});
@@ -446,8 +446,8 @@ void goto_symext::symex_cpp_new(
 
   if(do_array)
   {
-    exprt size_arg = static_cast<const exprt &>(code.find(ID_size));
-    clean_expr(size_arg, state, false);
+    exprt size_arg =
+      clean_expr(static_cast<const exprt &>(code.find(ID_size)), state, false);
     symbol.type = array_typet(pointer_type.subtype(), size_arg);
   }
   else

src/goto-symex/symex_clean_expr.cpp

@@ -173,8 +173,7 @@ replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
 
 void goto_symext::lift_let(statet &state, const let_exprt &let_expr)
 {
-  exprt let_value = let_expr.value();
-  clean_expr(let_value, state, false);
+  exprt let_value = clean_expr(let_expr.value(), state, false);
   let_value = state.rename(std::move(let_value), ns).get();
   do_simplify(let_value);
 
@@ -213,8 +212,8 @@ void goto_symext::lift_lets(statet &state, exprt &rhs)
   }
 }
 
-void goto_symext::clean_expr(
-  exprt &expr,
+exprt goto_symext::clean_expr(
+  exprt expr,
   statet &state,
   const bool write)
 {
@@ -227,4 +226,5 @@ void goto_symext::clean_expr(
   // lhs
   if(write)
     adjust_byte_extract_rec(expr, ns);
+  return expr;
 }

src/goto-symex/symex_function_call.cpp

@@ -134,8 +134,8 @@ void goto_symext::parameter_assignments(
         assignment_type =
           symex_targett::assignment_typet::VISIBLE_ACTUAL_PARAMETER;
 
-      clean_expr(lhs, state, true);
-      clean_expr(rhs, state, false);
+      lhs = to_symbol_expr(clean_expr(std::move(lhs), state, true));
+      rhs = clean_expr(std::move(rhs), state, false);
 
       exprt::operandst lhs_conditions;
       symex_assign_rec(
@@ -193,12 +193,12 @@ void goto_symext::symex_function_call_symbol(
   code_function_callt code = original_code;
 
   if(code.lhs().is_not_nil())
-    clean_expr(code.lhs(), state, true);
+    code.lhs() = clean_expr(std::move(code.lhs()), state, true);
 
-  clean_expr(code.function(), state, false);
+  code.function() = clean_expr(std::move(code.function()), state, false);
 
   Forall_expr(it, code.arguments())
-    clean_expr(*it, state, false);
+    *it = clean_expr(std::move(*it), state, false);
 
   target.location(state.guard.as_expr(), state.source);
 

src/goto-symex/symex_goto.cpp

@@ -69,8 +69,7 @@ void goto_symext::symex_goto(statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;
 
-  exprt new_guard = instruction.get_condition();
-  clean_expr(new_guard, state, false);
+  exprt new_guard = clean_expr(instruction.get_condition(), state, false);
 
   renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
   if(symex_config.simplify_opt)

src/goto-symex/symex_main.cpp

@@ -87,8 +87,7 @@ void goto_symext::symex_assert(
   const goto_programt::instructiont &instruction,
   statet &state)
 {
-  exprt condition = instruction.get_condition();
-  clean_expr(condition, state, false);
+  exprt condition = clean_expr(instruction.get_condition(), state, false);
 
   // First, push negations in and perhaps convert existential quantifiers into
   // universals:
@@ -131,9 +130,7 @@ void goto_symext::vcc(
 
 void goto_symext::symex_assume(statet &state, const exprt &cond)
 {
-  exprt simplified_cond=cond;
-
-  clean_expr(simplified_cond, state, false);
+  exprt simplified_cond = clean_expr(cond, state, false);
   simplified_cond = state.rename(std::move(simplified_cond), ns).get();
   do_simplify(simplified_cond);
 

src/goto-symex/symex_other.cpp

@@ -89,26 +89,22 @@ void goto_symext::symex_other(
   else if(statement==ID_cpp_delete ||
           statement=="cpp_delete[]")
   {
-    codet clean_code=code;
-    clean_expr(clean_code, state, false);
+    const codet clean_code = to_code(clean_expr(code, state, false));
     symex_cpp_delete(state, clean_code);
   }
   else if(statement==ID_printf)
   {
-    codet clean_code=code;
-    clean_expr(clean_code, state, false);
+    const codet clean_code = to_code(clean_expr(code, state, false));
     symex_printf(state, clean_code);
   }
   else if(statement==ID_input)
   {
-    codet clean_code(code);
-    clean_expr(clean_code, state, false);
+    const codet clean_code = to_code(clean_expr(code, state, false));
     symex_input(state, clean_code);
   }
   else if(statement==ID_output)
   {
-    codet clean_code(code);
-    clean_expr(clean_code, state, false);
+    const codet clean_code = to_code(clean_expr(code, state, false));
     symex_output(state, clean_code);
   }
   else if(statement==ID_decl)
@@ -138,10 +134,8 @@ void goto_symext::symex_other(
       "expected array_copy/array_replace statement to have two operands");
 
     // we need to add dereferencing for both operands
-    exprt dest_array(code.op0());
-    clean_expr(dest_array, state, false);
-    exprt src_array(code.op1());
-    clean_expr(src_array, state, false);
+    exprt dest_array = clean_expr(code.op0(), state, false);
+    exprt src_array = clean_expr(code.op1(), state, false);
 
     // obtain the actual arrays
     process_array_expr(state, dest_array);
@@ -190,15 +184,13 @@ void goto_symext::symex_other(
       "expected array_set statement to have two operands");
 
     // we need to add dereferencing for the first operand
-    exprt array_expr(code.op0());
-    clean_expr(array_expr, state, false);
+    exprt array_expr = clean_expr(code.op0(), state, false);
 
     // obtain the actual array(s)
     process_array_expr(state, array_expr);
 
     // prepare to build the array_of
-    exprt value = code.op1();
-    clean_expr(value, state, false);
+    exprt value = clean_expr(code.op1(), state, false);
 
     // we might have a memset-style update of a non-array type - convert to a
     // byte array
@@ -237,10 +229,8 @@ void goto_symext::symex_other(
       "expected array_equal statement to have three operands");
 
     // we need to add dereferencing for the first two
-    exprt array1(code.op0());
-    clean_expr(array1, state, false);
-    exprt array2(code.op1());
-    clean_expr(array2, state, false);
+    exprt array1 = clean_expr(code.op0(), state, false);
+    exprt array2 = clean_expr(code.op1(), state, false);
 
     // obtain the actual arrays
     process_array_expr(state, array1);
@@ -270,8 +260,7 @@ void goto_symext::symex_other(
       code.operands().size() == 1,
       "expected havoc_object statement to have one operand");
 
-    exprt object(code.op0());
-    clean_expr(object, state, false);
+    exprt object = clean_expr(code.op0(), state, false);
 
     process_array_expr(state, object);
     havoc_rec(state, guardt(true_exprt(), guard_manager), object);