symex: source is not optional

src/goto-instrument/accelerate/scratch_program.cpp

@@ -35,8 +35,10 @@ bool scratch_programt::check_sat(bool do_slice)
   output(ns, "scratch", std::cout);
 #endif
 
+  symex_state = util_make_unique<goto_symex_statet>(
+    symex_targett::sourcet(goto_functionst::entry_point(), *this));
   symex.symex_with_state(
-    symex_state,
+    *symex_state,
     [this](const irep_idt &key) -> const goto_functionst::goto_functiont & {
       return functions.function_map.at(key);
     },
@@ -69,7 +71,7 @@ exprt scratch_programt::eval(const exprt &e)
 {
   exprt ssa=e;
 
-  symex_state.rename(ssa, ns);
+  symex_state->rename(ssa, ns);
 
   return checker->get(ssa);
 }

src/goto-instrument/accelerate/scratch_program.h

@@ -74,7 +74,7 @@ class scratch_programt:public goto_programt
   bool constant_propagation;
 
 protected:
-  goto_symex_statet symex_state;
+  std::unique_ptr<goto_symex_statet> symex_state;
   goto_functionst functions;
   symbol_tablet &symbol_table;
   symbol_tablet symex_symbol_table;

src/goto-symex/goto_symex.h

@@ -149,28 +149,12 @@ class goto_symext
 protected:
   const symex_configt symex_config;
 
-  /// Initialise the symbolic execution and the given state with <code>pc</code>
-  /// as entry point.
-  /// \param state: Symex state to initialise.
-  /// \param get_goto_function: producer for GOTO functions
-  /// \param function_identifier: The function in which the instructions are
-  /// \param pc: first instruction to symex
-  /// \param limit: final instruction, which itself will not
-  ///   be symexed.
-  void initialize_entry_point(
-    statet &state,
-    const get_goto_functiont &get_goto_function,
-    const irep_idt &function_identifier,
-    goto_programt::const_targett pc,
-    goto_programt::const_targett limit);
-
   /// Initialize the symbolic execution and the given state with
   /// the beginning of the entry point function.
   /// \param get_goto_function: producer for GOTO functions
-  /// \param state: Symex state to initialize.
-  void initialize_entry_point_state(
-    const get_goto_functiont &get_goto_function,
-    statet &state);
+  /// \return Initialized symex state.
+  std::unique_ptr<statet>
+  initialize_entry_point_state(const get_goto_functiont &get_goto_function);
 
   /// Invokes symex_step and verifies whether additional threads can be
   /// executed.

src/goto-symex/goto_symex_state.cpp

@@ -27,8 +27,8 @@ Author: Daniel Kroening, [email protected]
 
 static void get_l1_name(exprt &expr);
 
-goto_symex_statet::goto_symex_statet()
-  : symex_target(nullptr), record_events(true), dirty()
+goto_symex_statet::goto_symex_statet(const symex_targett::sourcet &_source)
+  : goto_statet(_source), symex_target(nullptr), record_events(true), dirty()
 {
   threads.resize(1);
   new_frame();
@@ -782,11 +782,8 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
       ++stackit)
   {
     const auto &frame = *stackit;
-    if(frame.calling_location.is_set)
-    {
-      out << frame.calling_location.function_id << " "
-          << frame.calling_location.pc->location_number << "\n";
-    }
+    out << frame.calling_location.function_id << " "
+        << frame.calling_location.pc->location_number << "\n";
   }
 }
 

src/goto-symex/goto_symex_state.h

@@ -72,8 +72,11 @@ class goto_statet
   unsigned total_vccs = 0;
   unsigned remaining_vccs = 0;
 
+  /// Constructors
   explicit goto_statet(const class goto_symex_statet &s);
-  goto_statet() = default;
+  explicit goto_statet(const symex_targett::sourcet &_source) : source(_source)
+  {
+  }
 };
 
 // stack frames -- these are used for function calls and
@@ -124,7 +127,7 @@ struct framet
 class goto_symex_statet final : public goto_statet
 {
 public:
-  goto_symex_statet();
+  explicit goto_symex_statet(const symex_targett::sourcet &);
   ~goto_symex_statet();
 
   /// \brief Fake "copy constructor" that initializes the `symex_target` member

src/goto-symex/symex_function_call.cpp

@@ -326,7 +326,6 @@ void goto_symext::symex_function_call_code(
   frame.loop_iterations[identifier].is_recursion=true;
   frame.loop_iterations[identifier].count++;
 
-  state.source.is_set=true;
   state.source.function_id = identifier;
   symex_transition(state, goto_function.body.instructions.begin(), false);
 }

src/goto-symex/symex_main.cpp

@@ -159,34 +159,6 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
   }
 }
 
-void goto_symext::initialize_entry_point(
-  statet &state,
-  const get_goto_functiont &get_goto_function,
-  const irep_idt &function_id,
-  const goto_programt::const_targett pc,
-  const goto_programt::const_targett limit)
-{
-  PRECONDITION(!state.threads.empty());
-  PRECONDITION(!state.call_stack().empty());
-  state.source = symex_targett::sourcet(function_id, pc);
-  state.top().end_of_function=limit;
-  state.top().calling_location.pc=state.top().end_of_function;
-  state.symex_target=⌖
-
-  const goto_functiont &entry_point_function = get_goto_function(function_id);
-
-  state.top().hidden_function = entry_point_function.is_hidden();
-
-  auto emplace_safe_pointers_result =
-    state.safe_pointers.emplace(function_id, local_safe_pointerst{ns});
-  if(emplace_safe_pointers_result.second)
-    emplace_safe_pointers_result.first->second(entry_point_function.body);
-
-  state.dirty.populate_dirty_for_function(function_id, entry_point_function);
-
-  symex_transition(state, state.source.pc, false);
-}
-
 static void
 switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
 {
@@ -305,50 +277,69 @@ void goto_symext::resume_symex_from_saved_state(
       new_symbol_table);
 }
 
-void goto_symext::initialize_entry_point_state(
-  const get_goto_functiont &get_goto_function,
-  statet &state)
+std::unique_ptr<goto_symext::statet> goto_symext::initialize_entry_point_state(
+  const get_goto_functiont &get_goto_function)
 {
+  const irep_idt entry_point_id = goto_functionst::entry_point();
+
   const goto_functionst::goto_functiont *start_function;
   try
   {
-    start_function = &get_goto_function(goto_functionst::entry_point());
+    start_function = &get_goto_function(entry_point_id);
   }
   catch(const std::out_of_range &)
   {
     throw unsupported_operation_exceptiont("the program has no entry point");
   }
 
-  state.run_validation_checks = symex_config.run_validation_checks;
+  // create and prepare the state
+  auto state = util_make_unique<statet>(
+    symex_targett::sourcet(entry_point_id, start_function->body));
+  CHECK_RETURN(!state->threads.empty());
+  CHECK_RETURN(!state->call_stack().empty());
+
+  goto_programt::const_targett limit =
+    std::prev(start_function->body.instructions.end());
+  state->top().end_of_function = limit;
+  state->top().calling_location.pc = state->top().end_of_function;
+  state->top().hidden_function = start_function->is_hidden();
+
+  state->symex_target = &target;
+
+  state->run_validation_checks = symex_config.run_validation_checks;
 
-  initialize_entry_point(
-    state,
-    get_goto_function,
-    goto_functionst::entry_point(),
-    start_function->body.instructions.begin(),
-    std::prev(start_function->body.instructions.end()));
+  // initialize support analyses
+  auto emplace_safe_pointers_result =
+    state->safe_pointers.emplace(entry_point_id, local_safe_pointerst{ns});
+  if(emplace_safe_pointers_result.second)
+    emplace_safe_pointers_result.first->second(start_function->body);
+
+  state->dirty.populate_dirty_for_function(entry_point_id, *start_function);
+
+  // make the first step onto the instruction pointed to by the initial program
+  // counter
+  symex_transition(*state, state->source.pc, false);
+
+  return state;
 }
 
 void goto_symext::symex_from_entry_point_of(
   const get_goto_functiont &get_goto_function,
   symbol_tablet &new_symbol_table)
 {
-  statet state;
-  initialize_entry_point_state(get_goto_function, state);
+  auto state = initialize_entry_point_state(get_goto_function);
 
-  symex_with_state(
-    state, get_goto_function, new_symbol_table);
+  symex_with_state(*state, get_goto_function, new_symbol_table);
 }
 
 void goto_symext::initialize_path_storage_from_entry_point_of(
   const get_goto_functiont &get_goto_function,
   symbol_tablet &new_symbol_table)
 {
-  statet state;
-  initialize_entry_point_state(get_goto_function, state);
+  auto state = initialize_entry_point_state(get_goto_function);
 
-  path_storaget::patht entry_point_start(target, state);
-  entry_point_start.state.saved_target = state.source.pc;
+  path_storaget::patht entry_point_start(target, *state);
+  entry_point_start.state.saved_target = state->source.pc;
   entry_point_start.state.has_saved_next_instruction = true;
 
   path_storage.push(entry_point_start);

src/goto-symex/symex_target.h

@@ -39,14 +39,9 @@ class symex_targett
     // The program counter is an iterator which indicates where the execution
     // is in its program sequence
     goto_programt::const_targett pc;
-    bool is_set;
-
-    sourcet() : thread_nr(0), function_id(irep_idt()), is_set(false)
-    {
-    }
 
     sourcet(const irep_idt &_function_id, goto_programt::const_targett _pc)
-      : thread_nr(0), function_id(_function_id), pc(_pc), is_set(true)
+      : thread_nr(0), function_id(_function_id), pc(_pc)
     {
     }
 
@@ -55,8 +50,7 @@ class symex_targett
       const goto_programt &_goto_program)
       : thread_nr(0),
         function_id(_function_id),
-        pc(_goto_program.instructions.begin()),
-        is_set(true)
+        pc(_goto_program.instructions.begin())
     {
     }
   };

src/goto-symex/symex_target_equation.cpp

@@ -701,15 +701,12 @@ void symex_target_equationt::SSA_stept::output(
   const namespacet &ns,
   std::ostream &out) const
 {
-  if(source.is_set)
-  {
-    out << "Thread " << source.thread_nr;
+  out << "Thread " << source.thread_nr;
 
-    if(source.pc->source_location.is_not_nil())
-      out << " " << source.pc->source_location << '\n';
-    else
-      out << '\n';
-  }
+  if(source.pc->source_location.is_not_nil())
+    out << " " << source.pc->source_location << '\n';
+  else
+    out << '\n';
 
   switch(type)
   {
@@ -802,15 +799,12 @@ void symex_target_equationt::SSA_stept::output(
 
 void symex_target_equationt::SSA_stept::output(std::ostream &out) const
 {
-  if(source.is_set)
-  {
-    out << "Thread " << source.thread_nr;
+  out << "Thread " << source.thread_nr;
 
-    if(source.pc->source_location.is_not_nil())
-      out << " " << source.pc->source_location << '\n';
-    else
-      out << '\n';
-  }
+  if(source.pc->source_location.is_not_nil())
+    out << " " << source.pc->source_location << '\n';
+  else
+    out << '\n';
 
   switch(type)
   {

unit/goto-symex/ssa_equation.cpp

@@ -25,10 +25,12 @@ SCENARIO("Validation of well-formed SSA steps", "[core][goto-symex][validate]")
     fun_symbol.name = fun_name;
     symbol_exprt fun_foo(fun_name, code_type);
 
+    goto_programt goto_program;
+    goto_program.add_instruction(END_FUNCTION);
     symex_target_equationt equation;
-    symex_targett::sourcet empty_source;
+    symex_targett::sourcet at_end_function(fun_name, goto_program);
     equation.SSA_steps.emplace_back(
-      empty_source, goto_trace_stept::typet::FUNCTION_RETURN);
+      at_end_function, goto_trace_stept::typet::FUNCTION_RETURN);
     auto &step = equation.SSA_steps.back();
     step.called_function = fun_name;