Merge pull request #4595 from romainbrenguier/clean-up/field-sensitivity

field_sensitivityt::apply does not take a reference

Author: tautschnig

src/goto-symex/field_sensitivity.cpp

@@ -18,37 +18,37 @@ Author: Michael Tautschnig
 
 // #define ENABLE_ARRAY_FIELD_SENSITIVITY
 
-void field_sensitivityt::apply(
+exprt field_sensitivityt::apply(
   const namespacet &ns,
   goto_symex_statet &state,
-  exprt &expr,
+  exprt expr,
   bool write) const
 {
   if(!run_apply)
-    return;
+    return expr;
 
   if(expr.id() != ID_address_of)
   {
     Forall_operands(it, expr)
-      apply(ns, state, *it, write);
+      *it = apply(ns, state, std::move(*it), write);
   }
 
   if(expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol) && !write)
   {
-    expr = get_fields(ns, state, to_ssa_expr(expr));
+    return get_fields(ns, state, to_ssa_expr(expr));
   }
   else if(
     !write && expr.id() == ID_member &&
     to_member_expr(expr).struct_op().id() == ID_struct)
   {
-    simplify(expr, ns);
+    return simplify_expr(std::move(expr), ns);
   }
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(
     !write && expr.id() == ID_index &&
     to_index_expr(expr).array().id() == ID_array)
   {
-    simplify(expr, ns);
+    return simplify_expr(std::move(expr), ns);
   }
 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
   else if(expr.id() == ID_member)
@@ -73,9 +73,9 @@ void field_sensitivityt::apply(
       member.struct_op() = tmp.get_original_expr();
       tmp.set_expression(member);
       if(was_l2)
-        expr = state.rename(tmp, ns).get();
+        return state.rename(std::move(tmp), ns).get();
       else
-        expr.swap(tmp);
+        return std::move(tmp);
     }
   }
 #ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
@@ -102,12 +102,13 @@ void field_sensitivityt::apply(
       index.array() = tmp.get_original_expr();
       tmp.set_expression(index);
       if(was_l2)
-        expr = state.rename(tmp, ns).get();
+        return state.rename(std::move(tmp), ns).get();
       else
-        expr.swap(tmp);
+        return std::move(tmp);
     }
   }
 #endif // ENABLE_ARRAY_FIELD_SENSITIVITY
+  return expr;
 }
 
 exprt field_sensitivityt::get_fields(
@@ -187,8 +188,7 @@ void field_sensitivityt::field_assignments(
   symex_targett &target,
   bool allow_pointer_unsoundness)
 {
-  exprt lhs_fs = lhs;
-  apply(ns, state, lhs_fs, false);
+  const exprt lhs_fs = apply(ns, state, lhs, false);
 
   bool run_apply_bak = run_apply;
   run_apply = false;

src/goto-symex/field_sensitivity.h

@@ -45,11 +45,11 @@ class field_sensitivityt
   /// existing member or index expressions into symbols are performed.
   /// \param ns: a namespace to resolve type symbols/tag types
   /// \param [in,out] state: symbolic execution state
-  /// \param [in,out] expr: an expression to be (recursively) transformed - this
-  ///   parameter is both input and output.
+  /// \param expr: an expression to be (recursively) transformed.
   /// \param write: set to true if the expression is to be used as an lvalue.
-  void
-  apply(const namespacet &ns, goto_symex_statet &state, exprt &expr, bool write)
+  /// \return the transformed expression
+  exprt
+  apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write)
     const;
 
   /// Compute an expression representing the individual components of a

src/goto-symex/goto_symex_state.cpp

@@ -337,7 +337,7 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
       "if_exprt");
 
     if(level == L2)
-      field_sensitivity.apply(ns, *this, expr, false);
+      expr = field_sensitivity.apply(ns, *this, std::move(expr), false);
 
     return renamedt<exprt, level>{std::move(expr)};
   }

src/goto-symex/symex_assign.cpp

@@ -271,7 +271,8 @@ static void rewrite_with_to_field_symbols(
         with_expr.new_value().type());
     }
 
-    state.field_sensitivity.apply(ns, state, field_sensitive_lhs, true);
+    field_sensitive_lhs = state.field_sensitivity.apply(
+      ns, state, std::move(field_sensitive_lhs), true);
 
     if(field_sensitive_lhs.id() != ID_symbol)
       break;
@@ -392,8 +393,8 @@ void goto_symext::symex_assign_from_struct(
   for(std::size_t i = 0; i < components.size(); ++i)
   {
     const auto &comp = components[i];
-    exprt lhs_field = member_exprt(lhs, comp.get_name(), comp.type());
-    state.field_sensitivity.apply(ns, state, lhs_field, true);
+    const exprt lhs_field = state.field_sensitivity.apply(
+      ns, state, member_exprt{lhs, comp.get_name(), comp.type()}, true);
     INVARIANT(
       lhs_field.id() == ID_symbol,
       "member of symbol should be susceptible to field-sensitivity");

src/goto-symex/symex_dereference.cpp

@@ -244,7 +244,7 @@ void goto_symext::dereference_rec(exprt &expr, statet &state, bool write)
 
     // ...and may have introduced a member-of-symbol construct with a
     // corresponding SSA symbol:
-    state.field_sensitivity.apply(ns, state, expr, write);
+    expr = state.field_sensitivity.apply(ns, state, std::move(expr), write);
   }
   else if(
     expr.id() == ID_index && to_index_expr(expr).array().id() == ID_member &&
@@ -359,8 +359,8 @@ void goto_symext::dereference(exprt &expr, statet &state, bool write)
   // from different frames. Would be enough to rename
   // symbols whose address is taken.
   PRECONDITION(!state.call_stack().empty());
-  exprt l1_expr = state.rename<L1>(expr, ns).get();
-  state.field_sensitivity.apply(ns, state, l1_expr, write);
+  exprt l1_expr = state.field_sensitivity.apply(
+    ns, state, state.rename<L1>(expr, ns).get(), write);
 
   // start the recursion!
   dereference_rec(l1_expr, state, write);
@@ -394,5 +394,5 @@ void goto_symext::dereference(exprt &expr, statet &state, bool write)
       "simplify re-introduced dereferencing");
   }
 
-  state.field_sensitivity.apply(ns, state, expr, write);
+  expr = state.field_sensitivity.apply(ns, state, std::move(expr), write);
 }