Merge pull request #4381 from romainbrenguier/clean-up/ssa_step

romainbrenguier · web-flow · commit 410f50eb3094 · 2019-03-14T10:54:21.000Z
Move SSA_stept definition to its own header file
diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/src/goto-checker/goto_symex_fault_localizer.cpp
@@ -46,8 +46,7 @@ operator()(const irep_idt &failed_property_id)
   return fault_location;
 }
 
-const symex_target_equationt::SSA_stept &
-goto_symex_fault_localizert::collect_guards(
+const SSA_stept &goto_symex_fault_localizert::collect_guards(
   const irep_idt &failed_property_id,
   localization_pointst &localization_points,
   fault_location_infot &fault_location)
@@ -74,7 +73,7 @@ goto_symex_fault_localizert::collect_guards(
 }
 
 bool goto_symex_fault_localizert::check(
-  const symex_target_equationt::SSA_stept &failed_step,
+  const SSA_stept &failed_step,
   const localization_pointst &localization_points,
   const localization_points_valuet &value)
 {
@@ -116,7 +115,7 @@ void goto_symex_fault_localizert::update_scores(
 }
 
 void goto_symex_fault_localizert::localize_linear(
-  const symex_target_equationt::SSA_stept &failed_step,
+  const SSA_stept &failed_step,
   const localization_pointst &localization_points)
 {
   localization_points_valuet v(localization_points.size(), tvt::unknown());
diff --git a/src/goto-checker/goto_symex_fault_localizer.h b/src/goto-checker/goto_symex_fault_localizer.h
@@ -44,24 +44,23 @@ class goto_symex_fault_localizert
   /// Collects the guards as \p localization_points up to \p failed_property_id
   /// and initializes fault_location_info, and returns the SSA step of
   /// the failed property
-  const symex_target_equationt::SSA_stept &collect_guards(
+  const SSA_stept &collect_guards(
     const irep_idt &failed_property_id,
     localization_pointst &localization_points,
     fault_location_infot &fault_location);
 
   // specify a localization point combination to check
   typedef std::vector<tvt> localization_points_valuet;
   bool check(
-    const symex_target_equationt::SSA_stept &failed_step,
+    const SSA_stept &failed_step,
     const localization_pointst &,
     const localization_points_valuet &);
 
   void update_scores(const localization_pointst &);
 
   // localization method: flip each point
-  void localize_linear(
-    const symex_target_equationt::SSA_stept &failed_step,
-    const localization_pointst &);
+  void
+  localize_linear(const SSA_stept &failed_step, const localization_pointst &);
 };
 
 #endif // CPROVER_GOTO_CHECKER_GOTO_SYMEX_FAULT_LOCALIZER_H
diff --git a/src/goto-symex/Makefile b/src/goto-symex/Makefile
@@ -15,6 +15,7 @@ SRC = auto_objects.cpp \
       show_program.cpp \
       show_vcc.cpp \
       slice.cpp \
+      ssa_step.cpp \
       symex_assign.cpp \
       symex_atomic_section.cpp \
       symex_builtin_functions.cpp \
diff --git a/src/goto-symex/README.md b/src/goto-symex/README.md
@@ -48,7 +48,7 @@ digraph G {
 \subsection symex-overview Overview
 
 The \ref bmct class gets a reference to an \ref symex_target_equationt
-"equation" (initially, an empty list of \ref symex_target_equationt::SSA_stept
+"equation" (initially, an empty list of \ref SSA_stept
 "single-static assignment steps") and a goto-program from the frontend.
 The \ref bmct creates a goto_symext to symbolically execute the
 goto-program, thereby filling the equation, which can then be passed
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
@@ -134,7 +134,7 @@ static void set_internal_dynamic_object(
 /// set internal for variables assignments related to dynamic_object and CPROVER
 /// internal functions (e.g., __CPROVER_initialize)
 static void update_internal_field(
-  const symex_target_equationt::SSA_stept &SSA_step,
+  const SSA_stept &SSA_step,
   goto_trace_stept &goto_trace_step,
   const namespacet &ns)
 {
@@ -201,7 +201,7 @@ void build_goto_trace(
       last_step_to_keep = it;
     }
 
-    const symex_target_equationt::SSA_stept &SSA_step=*it;
+    const SSA_stept &SSA_step = *it;
 
     if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
       continue;
diff --git a/src/goto-symex/equation_conversion_exceptions.h b/src/goto-symex/equation_conversion_exceptions.h
@@ -16,14 +16,14 @@ Author: Diffblue Ltd.
 
 #include <util/format_expr.h>
 
-#include "symex_target_equation.h"
+#include "ssa_step.h"
 
 class equation_conversion_exceptiont : public std::runtime_error
 {
 public:
   equation_conversion_exceptiont(
     const std::string &message,
-    const symex_target_equationt::SSA_stept &step)
+    const SSA_stept &step)
     : runtime_error(message), step(step)
   {
     std::ostringstream error_msg;
@@ -40,7 +40,7 @@ class equation_conversion_exceptiont : public std::runtime_error
   }
 
 private:
-  symex_target_equationt::SSA_stept step;
+  SSA_stept step;
   std::string error_message;
 };
 
diff --git a/src/goto-symex/partial_order_concurrency.cpp b/src/goto-symex/partial_order_concurrency.cpp
@@ -58,7 +58,7 @@ void partial_order_concurrencyt::add_init_writes(
     {
       init_steps.emplace_back(
         e_it->source, goto_trace_stept::typet::SHARED_WRITE);
-      symex_target_equationt::SSA_stept &SSA_step=init_steps.back();
+      SSA_stept &SSA_step = init_steps.back();
 
       SSA_step.guard=true_exprt();
       // no SSA L2 index, thus nondet value
diff --git a/src/goto-symex/partial_order_concurrency.h b/src/goto-symex/partial_order_concurrency.h
@@ -25,7 +25,7 @@ class partial_order_concurrencyt:public messaget
   explicit partial_order_concurrencyt(const namespacet &_ns);
   virtual ~partial_order_concurrencyt();
 
-  typedef symex_target_equationt::SSA_stept eventt;
+  typedef SSA_stept eventt;
   typedef symex_target_equationt::SSA_stepst eventst;
   typedef eventst::const_iterator event_it;
 
diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
@@ -22,19 +22,16 @@ class postconditiont
   postconditiont(
     const namespacet &_ns,
     const value_sett &_value_set,
-    const symex_target_equationt::SSA_stept &_SSA_step,
-    const goto_symex_statet &_s):
-    ns(_ns),
-    value_set(_value_set),
-    SSA_step(_SSA_step),
-    s(_s)
+    const SSA_stept &_SSA_step,
+    const goto_symex_statet &_s)
+    : ns(_ns), value_set(_value_set), SSA_step(_SSA_step), s(_s)
   {
   }
 
 protected:
   const namespacet &ns;
   const value_sett &value_set;
-  const symex_target_equationt::SSA_stept &SSA_step;
+  const SSA_stept &SSA_step;
   const goto_symex_statet &s;
 
 public:
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
@@ -25,21 +25,21 @@ class preconditiont
     const namespacet &_ns,
     value_setst &_value_sets,
     const goto_programt::const_targett _target,
-    const symex_target_equationt::SSA_stept &_SSA_step,
-    const goto_symex_statet &_s):
-    ns(_ns),
-    value_sets(_value_sets),
-    target(_target),
-    SSA_step(_SSA_step),
-    s(_s)
+    const SSA_stept &_SSA_step,
+    const goto_symex_statet &_s)
+    : ns(_ns),
+      value_sets(_value_sets),
+      target(_target),
+      SSA_step(_SSA_step),
+      s(_s)
   {
   }
 
 protected:
   const namespacet &ns;
   value_setst &value_sets;
   const goto_programt::const_targett target;
-  const symex_target_equationt::SSA_stept &SSA_step;
+  const SSA_stept &SSA_step;
   const goto_symex_statet &s;
   void compute_rec(exprt &dest);
 
diff --git a/src/goto-symex/show_program.cpp b/src/goto-symex/show_program.cpp
@@ -24,7 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \param count: Step number, incremented after output
 static void show_step(
   const namespacet &ns,
-  const symex_target_equationt::SSA_stept &step,
+  const SSA_stept &step,
   const std::string &annotation,
   std::size_t &count)
 {
diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp
@@ -51,7 +51,7 @@ void symex_slicet::slice(symex_target_equationt &equation)
     slice(*it);
 }
 
-void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step)
+void symex_slicet::slice(SSA_stept &SSA_step)
 {
   get_symbols(SSA_step.guard);
 
@@ -109,8 +109,7 @@ void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step)
   }
 }
 
-void symex_slicet::slice_assignment(
-  symex_target_equationt::SSA_stept &SSA_step)
+void symex_slicet::slice_assignment(SSA_stept &SSA_step)
 {
   PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);
   const irep_idt &id=SSA_step.ssa_lhs.get_identifier();
@@ -124,8 +123,7 @@ void symex_slicet::slice_assignment(
     get_symbols(SSA_step.ssa_rhs);
 }
 
-void symex_slicet::slice_decl(
-  symex_target_equationt::SSA_stept &SSA_step)
+void symex_slicet::slice_decl(SSA_stept &SSA_step)
 {
   const irep_idt &id = to_symbol_expr(SSA_step.ssa_lhs).get_identifier();
 
@@ -152,7 +150,7 @@ void symex_slicet::collect_open_variables(
       it!=equation.SSA_steps.end();
       it++)
   {
-    const symex_target_equationt::SSA_stept &SSA_step=*it;
+    const SSA_stept &SSA_step = *it;
 
     get_symbols(SSA_step.guard);
 
diff --git a/src/goto-symex/ssa_step.cpp b/src/goto-symex/ssa_step.cpp
diff --git a/src/goto-symex/ssa_step.h b/src/goto-symex/ssa_step.h
diff --git a/src/goto-symex/symex_slice_class.h b/src/goto-symex/symex_slice_class.h
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h

Original file line number	Diff line number	Diff line change
`@@ -46,8 +46,7 @@ operator()(const irep_idt &failed_property_id)`
`46`	`46`	`return fault_location;`
`47`	`47`	`}`
`48`	`48`
`49`		`-const symex_target_equationt::SSA_stept &`
`50`		`-goto_symex_fault_localizert::collect_guards(`
	`49`	`+const SSA_stept &goto_symex_fault_localizert::collect_guards(`
`51`	`50`	`const irep_idt &failed_property_id,`
`52`	`51`	`localization_pointst &localization_points,`
`53`	`52`	`fault_location_infot &fault_location)`
`@@ -74,7 +73,7 @@ goto_symex_fault_localizert::collect_guards(`
`74`	`73`	`}`
`75`	`74`
`76`	`75`	`bool goto_symex_fault_localizert::check(`
`77`		`- const symex_target_equationt::SSA_stept &failed_step,`
	`76`	`+ const SSA_stept &failed_step,`
`78`	`77`	`const localization_pointst &localization_points,`
`79`	`78`	`const localization_points_valuet &value)`
`80`	`79`	`{`
`@@ -116,7 +115,7 @@ void goto_symex_fault_localizert::update_scores(`
`116`	`115`	`}`
`117`	`116`
`118`	`117`	`void goto_symex_fault_localizert::localize_linear(`
`119`		`- const symex_target_equationt::SSA_stept &failed_step,`
	`118`	`+ const SSA_stept &failed_step,`
`120`	`119`	`const localization_pointst &localization_points)`
`121`	`120`	`{`
`122`	`121`	`localization_points_valuet v(localization_points.size(), tvt::unknown());`
Original file line number	Diff line number	Diff line change
`@@ -58,7 +58,7 @@ void partial_order_concurrencyt::add_init_writes(`
`58`	`58`	`{`
`59`	`59`	`init_steps.emplace_back(`
`60`	`60`	`e_it->source, goto_trace_stept::typet::SHARED_WRITE);`
`61`		`- symex_target_equationt::SSA_stept &SSA_step=init_steps.back();`
	`61`	`+ SSA_stept &SSA_step = init_steps.back();`
`62`	`62`
`63`	`63`	`SSA_step.guard=true_exprt();`
`64`	`64`	`// no SSA L2 index, thus nondet value`
Original file line number	Diff line number	Diff line change
`@@ -24,7 +24,7 @@ Author: Daniel Kroening, [email protected]`
`24`	`24`	`/// \param count: Step number, incremented after output`
`25`	`25`	`static void show_step(`
`26`	`26`	`const namespacet &ns,`
`27`		`- const symex_target_equationt::SSA_stept &step,`
	`27`	`+ const SSA_stept &step,`
`28`	`28`	`const std::string &annotation,`
`29`	`29`	`std::size_t &count)`
`30`	`30`	`{`
Original file line number	Diff line number	Diff line change
`@@ -51,7 +51,7 @@ void symex_slicet::slice(symex_target_equationt &equation)`
`51`	`51`	`slice(*it);`
`52`	`52`	`}`
`53`	`53`
`54`		`-void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step)`
	`54`	`+void symex_slicet::slice(SSA_stept &SSA_step)`
`55`	`55`	`{`
`56`	`56`	`get_symbols(SSA_step.guard);`
`57`	`57`
`@@ -109,8 +109,7 @@ void symex_slicet::slice(symex_target_equationt::SSA_stept &SSA_step)`
`109`	`109`	`}`
`110`	`110`	`}`
`111`	`111`
`112`		`-void symex_slicet::slice_assignment(`
`113`		`- symex_target_equationt::SSA_stept &SSA_step)`
	`112`	`+void symex_slicet::slice_assignment(SSA_stept &SSA_step)`
`114`	`113`	`{`
`115`	`114`	`PRECONDITION(SSA_step.ssa_lhs.id() == ID_symbol);`
`116`	`115`	`const irep_idt &id=SSA_step.ssa_lhs.get_identifier();`
`@@ -124,8 +123,7 @@ void symex_slicet::slice_assignment(`
`124`	`123`	`get_symbols(SSA_step.ssa_rhs);`
`125`	`124`	`}`
`126`	`125`
`127`		`-void symex_slicet::slice_decl(`
`128`		`- symex_target_equationt::SSA_stept &SSA_step)`
	`126`	`+void symex_slicet::slice_decl(SSA_stept &SSA_step)`
`129`	`127`	`{`
`130`	`128`	`const irep_idt &id = to_symbol_expr(SSA_step.ssa_lhs).get_identifier();`
`131`	`129`
`@@ -152,7 +150,7 @@ void symex_slicet::collect_open_variables(`
`152`	`150`	`it!=equation.SSA_steps.end();`
`153`	`151`	`it++)`
`154`	`152`	`{`
`155`		`- const symex_target_equationt::SSA_stept &SSA_step=*it;`
	`153`	`+ const SSA_stept &SSA_step = *it;`
`156`	`154`
`157`	`155`	`get_symbols(SSA_step.guard);`
`158`	`156`