Merge pull request #4018 from romainbrenguier/clean-up/goto-symex-state

Break goto_symex_state into more manageable bits

Author: tautschnig

src/goto-checker/symex_bmc.cpp

@@ -86,9 +86,7 @@ void symex_bmct::symex_step(
   }
 }
 
-void symex_bmct::merge_goto(
-  const statet::goto_statet &goto_state,
-  statet &state)
+void symex_bmct::merge_goto(const goto_statet &goto_state, statet &state)
 {
   const goto_programt::const_targett prev_pc = goto_state.source.pc;
   const guardt prev_guard = goto_state.guard;

src/goto-checker/symex_bmc.h

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

src/goto-symex/goto_symex.h

@@ -256,17 +256,11 @@ class goto_symext
   // gotos
   void merge_gotos(statet &);
 
-  virtual void merge_goto(
-    const statet::goto_statet &goto_state,
-    statet &);
+  virtual void merge_goto(const goto_statet &goto_state, statet &);
 
-  void merge_value_sets(
-    const statet::goto_statet &goto_state,
-    statet &dest);
+  void merge_value_sets(const goto_statet &goto_state, statet &dest);
 
-  void phi_function(
-    const statet::goto_statet &goto_state,
-    statet &);
+  void phi_function(const goto_statet &goto_state, statet &);
 
   // determine whether to unwind a loop -- true indicates abort,
   // with false we continue.

src/goto-symex/goto_symex_state.cpp

@@ -28,13 +28,7 @@ Author: Daniel Kroening, [email protected]
 static void get_l1_name(exprt &expr);
 
 goto_symex_statet::goto_symex_statet()
-  : depth(0),
-    symex_target(nullptr),
-    atomic_section_id(0),
-    total_vccs(0),
-    remaining_vccs(0),
-    record_events(true),
-    dirty()
+  : symex_target(nullptr), record_events(true), dirty()
 {
   threads.resize(1);
   new_frame();
@@ -697,42 +691,6 @@ void goto_symex_statet::rename(
     l1_type_entry.first->second=type;
 }
 
-void goto_symex_statet::get_original_name(exprt &expr) const
-{
-  get_original_name(expr.type());
-
-  if(expr.id()==ID_symbol &&
-     expr.get_bool(ID_C_SSA_symbol))
-    expr=to_ssa_expr(expr).get_original_expr();
-  else
-    Forall_operands(it, expr)
-      get_original_name(*it);
-}
-
-void goto_symex_statet::get_original_name(typet &type) const
-{
-  // rename all the symbols with their last known value
-
-  if(type.id()==ID_array)
-  {
-    auto &array_type = to_array_type(type);
-    get_original_name(array_type.subtype());
-    get_original_name(array_type.size());
-  }
-  else if(type.id() == ID_struct || type.id() == ID_union)
-  {
-    struct_union_typet &s_u_type=to_struct_union_type(type);
-    struct_union_typet::componentst &components=s_u_type.components();
-
-    for(auto &component : components)
-      get_original_name(component.type());
-  }
-  else if(type.id()==ID_pointer)
-  {
-    get_original_name(to_pointer_type(type).subtype());
-  }
-}
-
 static void get_l1_name(exprt &expr)
 {
   // do not reset the type !
@@ -777,7 +735,7 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
 /// Print the constant propagation map in a human-friendly format.
 /// This is primarily for use from the debugger; please don't delete me just
 /// because there aren't any current callers.
-void goto_symex_statet::output_propagation_map(std::ostream &out)
+void goto_statet::output_propagation_map(std::ostream &out)
 {
   for(const auto &name_value : propagation)
   {