Remove renamedt from symex_targett interface

src/goto-symex/symex_builtin_functions.cpp

@@ -454,14 +454,13 @@ void goto_symext::symex_output(
   PRECONDITION(code.operands().size() >= 2);
   exprt id_arg = state.rename(code.op0(), ns).get();
 
-  std::list<renamedt<exprt, L2>> args;
+  std::list<exprt> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
     renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
-    if(symex_config.simplify_opt)
-      l2_arg.simplify(ns);
-    args.emplace_back(l2_arg);
+    args.emplace_back(l2_arg.get());
+    do_simplify(args.back());
   }
 
   const irep_idt output_id=get_string_argument(id_arg, ns);

src/goto-symex/symex_function_call.cpp

@@ -273,9 +273,11 @@ void goto_symext::symex_function_call_post_clean(
   }
 
   // read the arguments -- before the locality renaming
-  const std::vector<renamedt<exprt, L2>> renamed_arguments =
+  const std::vector<exprt> renamed_arguments =
     make_range(cleaned_arguments).map([&](const exprt &a) {
-      return state.rename(a, ns);
+      exprt arg = state.rename(a, ns).get();
+      do_simplify(arg);
+      return arg;
     });
 
   // we hide the call if the caller and callee are both hidden

src/goto-symex/symex_goto.cpp

@@ -238,9 +238,8 @@ void goto_symext::symex_goto(statet &state)
   renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
   renamed_guard = try_evaluate_pointer_comparisons(
     std::move(renamed_guard), state.value_set, language_mode, ns);
-  if(symex_config.simplify_opt)
-    renamed_guard.simplify(ns);
   new_guard = renamed_guard.get();
+  do_simplify(new_guard);
 
   if(new_guard.is_false())
   {
@@ -251,7 +250,7 @@ void goto_symext::symex_goto(statet &state)
     return; // nothing to do
   }
 
-  target.goto_instruction(state.guard.as_expr(), renamed_guard, state.source);
+  target.goto_instruction(state.guard.as_expr(), new_guard, state.source);
 
   DATA_INVARIANT(
     !instruction.targets.empty(), "goto should have at least one target");

src/goto-symex/symex_target.h

@@ -14,8 +14,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_program.h>
 
-#include "renamed.h"
-
 class ssa_exprt;
 
 /// The interface of the target _container_ for symbolic execution to record its
@@ -158,7 +156,7 @@ class symex_targett
   virtual void function_call(
     const exprt &guard,
     const irep_idt &function_id,
-    const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
+    const std::vector<exprt> &ssa_function_arguments,
     const sourcet &source,
     bool hidden) = 0;
 
@@ -192,7 +190,7 @@ class symex_targett
     const exprt &guard,
     const sourcet &source,
     const irep_idt &output_id,
-    const std::list<renamedt<exprt, L2>> &args) = 0;
+    const std::list<exprt> &args) = 0;
 
   /// Record formatted output.
   /// \param guard: Precondition for writing to the output
@@ -251,7 +249,7 @@ class symex_targett
   ///  goto instruction
   virtual void goto_instruction(
     const exprt &guard,
-    const renamedt<exprt, L2> &cond,
+    const exprt &cond,
     const sourcet &source) = 0;
 
   /// Record a _global_ constraint: there is no guard limiting its scope.

src/goto-symex/symex_target_equation.cpp

@@ -181,7 +181,7 @@
 void symex_target_equationt::function_call(
   const exprt &guard,
   const irep_idt &function_id,
-  const std::vector<renamedt<exprt, L2>> &function_arguments,
+  const std::vector<exprt> &function_arguments,
   const sourcet &source,
   const bool hidden)
 {
@@ -190,8 +190,7 @@
 
   SSA_step.guard = guard;
   SSA_step.called_function = function_id;
-  for(const auto &arg : function_arguments)
-    SSA_step.ssa_function_arguments.emplace_back(arg.get());
+  SSA_step.ssa_function_arguments = function_arguments;
   SSA_step.hidden = hidden;
 
   merge_ireps(SSA_step);
@@ -217,14 +216,13 @@
   const exprt &guard,
   const sourcet &source,
   const irep_idt &output_id,
-  const std::list<renamedt<exprt, L2>> &args)
+  const std::list<exprt> &args)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
   SSA_stept &SSA_step=SSA_steps.back();
 
   SSA_step.guard=guard;
-  for(const auto &arg : args)
-    SSA_step.io_args.emplace_back(arg.get());
+  SSA_step.io_args = args;
   SSA_step.io_id=output_id;
 
   merge_ireps(SSA_step);
@@ -299,14 +297,14 @@
 
 void symex_target_equationt::goto_instruction(
   const exprt &guard,
-  const renamedt<exprt, L2> &cond,
+  const exprt &cond,
   const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::GOTO);
   SSA_stept &SSA_step=SSA_steps.back();
 
   SSA_step.guard=guard;
-  SSA_step.cond_expr = cond.get();
+  SSA_step.cond_expr = cond;
 
   merge_ireps(SSA_step);
 }

src/goto-symex/symex_target_equation.h

@@ -82,7 +82,7 @@ class symex_target_equationt:public symex_targett
   virtual void function_call(
     const exprt &guard,
     const irep_idt &function_id,
-    const std::vector<renamedt<exprt, L2>> &ssa_function_arguments,
+    const std::vector<exprt> &ssa_function_arguments,
     const sourcet &source,
     bool hidden);
 
@@ -103,7 +103,7 @@ class symex_target_equationt:public symex_targett
     const exprt &guard,
     const sourcet &source,
     const irep_idt &output_id,
-    const std::list<renamedt<exprt, L2>> &args);
+    const std::list<exprt> &args);
 
   /// \copydoc symex_targett::output_fmt()
   virtual void output_fmt(
@@ -137,7 +137,7 @@ class symex_target_equationt:public symex_targett
   /// \copydoc symex_targett::goto_instruction()
   virtual void goto_instruction(
     const exprt &guard,
-    const renamedt<exprt, L2> &cond,
+    const exprt &cond,
     const sourcet &source);
 
   /// \copydoc symex_targett::constraint()