Merge pull request #4369 from smowton/smowton/cleanup/split-source-and-state

Split out goto_statet::source

Author: smowton

src/goto-checker/symex_bmc.cpp

@@ -93,12 +93,15 @@ void symex_bmct::symex_step(
   }
 }
 
-void symex_bmct::merge_goto(goto_statet &&goto_state, statet &state)
+void symex_bmct::merge_goto(
+  const symex_targett::sourcet &prev_source,
+  goto_statet &&goto_state,
+  statet &state)
 {
-  const goto_programt::const_targett prev_pc = goto_state.source.pc;
+  const goto_programt::const_targett prev_pc = prev_source.pc;
   const guardt prev_guard = goto_state.guard;
 
-  goto_symext::merge_goto(std::move(goto_state), state);
+  goto_symext::merge_goto(prev_source, std::move(goto_state), state);
 
   PRECONDITION(prev_pc->is_goto());
   if(

src/goto-checker/symex_bmc.h

@@ -95,7 +95,10 @@ class symex_bmct : public goto_symext
   void symex_step(const get_goto_functiont &get_goto_function, statet &state)
     override;
 
-  void merge_goto(goto_statet &&goto_state, statet &state) override;
+  void merge_goto(
+    const symex_targett::sourcet &source,
+    goto_statet &&goto_state,
+    statet &state) override;
 
   bool should_stop_unwind(
     const symex_targett::sourcet &source,

src/goto-symex/frame.h

@@ -13,12 +13,14 @@ Author: Romain Brenguier, [email protected]
 #define CPROVER_GOTO_SYMEX_FRAME_H
 
 #include "goto_state.h"
+#include "symex_target.h"
 
 /// Stack frames -- these are used for function calls and for exceptions
 struct framet
 {
   // gotos
-  using goto_state_listt = std::list<goto_statet>;
+  using goto_state_listt =
+    std::list<std::pair<symex_targett::sourcet, goto_statet>>;
 
   // function calls
   irep_idt function_identifier;

src/goto-symex/goto_state.h

@@ -17,7 +17,6 @@ Author: Romain Brenguier, [email protected]
 #include <pointer-analysis/value_set.h>
 
 #include "renaming_level.h"
-#include "symex_target_equation.h"
 
 /// Container for data that varies per program point, e.g. the constant
 /// propagator state, when state needs to branch. This is copied out of
@@ -41,8 +40,6 @@ class goto_statet
   // of the condition of the if).
   guardt guard;
 
-  symex_targett::sourcet source;
-
   // Map L1 names to (L2) constants. Values will be evicted from this map
   // when they become non-constant. This is used to propagate values that have
   // been worked out to only have one possible value.
@@ -60,10 +57,8 @@ class goto_statet
   /// Constructors
   explicit goto_statet(const class goto_symex_statet &s);
 
-  goto_statet(
-    const symex_targett::sourcet &_source,
-    guard_managert &guard_manager)
-    : guard(true_exprt(), guard_manager), source(_source)
+  explicit goto_statet(guard_managert &guard_manager)
+    : guard(true_exprt(), guard_manager)
   {
   }
 };

src/goto-symex/goto_symex.h

@@ -336,9 +336,13 @@ class goto_symext
   /// Merge a single branch, the symbolic state of which is held in \p
   /// goto_state, into the current overall symbolic state. \p goto_state is no
   /// longer expected to be valid afterwards.
+  /// \param source: source associated with the incoming \p goto_state
   /// \param goto_state: A state to be merged into this location
   /// \param state: Symbolic execution state to be updated
-  virtual void merge_goto(goto_statet &&goto_state, statet &state);
+  virtual void merge_goto(
+    const symex_targett::sourcet &source,
+    goto_statet &&goto_state,
+    statet &state);
 
   /// Merge the SSA assignments from goto_state into dest_state
   /// \param goto_state: A state to be merged into this location

src/goto-symex/goto_symex_state.cpp

@@ -32,7 +32,8 @@ static void get_l1_name(exprt &expr);
 goto_symex_statet::goto_symex_statet(
   const symex_targett::sourcet &_source,
   guard_managert &manager)
-  : goto_statet(_source, manager),
+  : goto_statet(manager),
+    source(_source),
     guard_manager(manager),
     symex_target(nullptr),
     record_events(true),

src/goto-symex/goto_symex_state.h

@@ -54,6 +54,8 @@ class goto_symex_statet final : public goto_statet
     symex_target = target;
   }
 
+  symex_targett::sourcet source;
+
   /// contains symbols that are minted during symbolic execution, such as
   /// dynamically created objects etc. The names in this table are needed
   /// for error traces even after symbolic execution has finished.
@@ -219,7 +221,6 @@ inline goto_statet::goto_statet(const class goto_symex_statet &s)
     level2(s.level2),
     value_set(s.value_set),
     guard(s.guard),
-    source(s.source),
     propagation(s.propagation),
     atomic_section_id(s.atomic_section_id)
 {

src/goto-symex/symex_goto.cpp

@@ -210,7 +210,7 @@ void goto_symext::symex_goto(statet &state)
   // merge_gotos when we visit new_state_pc
   framet::goto_state_listt &goto_state_list =
     state.call_stack().top().goto_state_map[new_state_pc];
-  goto_state_list.emplace_back(state);
+  goto_state_list.emplace_back(state.source, state);
 
   symex_transition(state, state_pc, backward);
 
@@ -270,7 +270,7 @@ void goto_symext::symex_goto(statet &state)
     }
     else
     {
-      goto_statet &new_state = goto_state_list.back();
+      goto_statet &new_state = goto_state_list.back().second;
       if(!backward)
       {
         new_state.guard.add(guard_expr);
@@ -300,13 +300,18 @@ void goto_symext::merge_gotos(statet &state)
 
   for(auto list_it = state_list.rbegin(); list_it != state_list.rend();
       ++list_it)
-    merge_goto(std::move(*list_it), state);
+  {
+    merge_goto(list_it->first, std::move(list_it->second), state);
+  }
 
   // clean up to save some memory
   frame.goto_state_map.erase(state_map_it);
 }
 
-void goto_symext::merge_goto(goto_statet &&goto_state, statet &state)
+void goto_symext::merge_goto(
+  const symex_targett::sourcet &,
+  goto_statet &&goto_state,
+  statet &state)
 {
   // check atomic section
   if(state.atomic_section_id != goto_state.atomic_section_id)