Ensure goto_symex_statet::source is always set

sourcet contains an interator, and the interface explicitly allows it to be
uninitialised.  However, most parts of the code base access source.pc
without checking.

Author: Daniel Kroening

src/goto-instrument/accelerate/scratch_program.cpp

@@ -35,7 +35,9 @@ bool scratch_programt::check_sat(bool do_slice)
   output(ns, "scratch", std::cout);
 #endif
 
-  symex.symex_with_state(symex_state, functions, symex_symbol_table);
+  symex_state = util_make_unique<goto_symex_statet>(
+    symex_targett::sourcet(goto_functionst::entry_point(), *this));
+  symex.symex_with_state(*symex_state, functions, symex_symbol_table);
 
   if(do_slice)
   {
@@ -64,7 +66,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_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();
@@ -724,11 +724,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
@@ -141,7 +144,6 @@ class goto_symex_statet final : public goto_statet
   /// for error traces even after symbolic execution has finished.
   symbol_tablet symbol_table;
 
-  symex_targett::sourcet source;
   symex_target_equationt *symex_target;
 
   // we remember all L1 renamings

src/goto-symex/symex_function_call.cpp

@@ -321,7 +321,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

@@ -339,7 +339,8 @@ void goto_symext::symex_from_entry_point_of(
     throw unsupported_operation_exceptiont("the program has no entry point");
   }
 
-  statet state;
+  statet state(symex_targett::sourcet(
+    goto_functionst::entry_point(), start_function->body));
 
   state.run_validation_checks = symex_config.run_validation_checks;
 

src/goto-symex/symex_target_equation.cpp

@@ -697,15 +697,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)
   {
@@ -798,15 +795,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)
   {