diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp index 9d3797a7247..6150b91f240 100644 --- a/src/goto-symex/symex_builtin_functions.cpp +++ b/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> args; + std::list args; for(std::size_t i=1; i 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); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 6fdf9f4ff5e..bc316977499 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/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> renamed_arguments = + const std::vector 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 diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 404f04fec72..7cf2d28c4de 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -238,9 +238,8 @@ void goto_symext::symex_goto(statet &state) renamedt 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"); diff --git a/src/goto-symex/symex_target.h b/src/goto-symex/symex_target.h index 209bc6de49e..0ef20a59bca 100644 --- a/src/goto-symex/symex_target.h +++ b/src/goto-symex/symex_target.h @@ -14,8 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include -#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> &ssa_function_arguments, + const std::vector &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> &args) = 0; + const std::list &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 &cond, + const exprt &cond, const sourcet &source) = 0; /// Record a _global_ constraint: there is no guard limiting its scope. diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 0bb35155e01..5e469e730d4 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -181,7 +181,7 @@ void symex_target_equationt::location( void symex_target_equationt::function_call( const exprt &guard, const irep_idt &function_id, - const std::vector> &function_arguments, + const std::vector &function_arguments, const sourcet &source, const bool hidden) { @@ -190,8 +190,7 @@ void symex_target_equationt::function_call( 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 @@ void symex_target_equationt::output( const exprt &guard, const sourcet &source, const irep_idt &output_id, - const std::list> &args) + const std::list &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::assertion( void symex_target_equationt::goto_instruction( const exprt &guard, - const renamedt &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); } diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h index b10a922b113..ef2f1056a3c 100644 --- a/src/goto-symex/symex_target_equation.h +++ b/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> &ssa_function_arguments, + const std::vector &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> &args); + const std::list &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 &cond, + const exprt &cond, const sourcet &source); /// \copydoc symex_targett::constraint()