Merge pull request #3433 from romainbrenguier/refactor/symex-nondet-count

Refactoring in symex, replace nondet_count by a functor

Author: romainbrenguier

src/goto-symex/goto_symex.cpp

@@ -13,7 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/simplify_expr.h>
 
-unsigned goto_symext::nondet_count=0;
 unsigned goto_symext::dynamic_counter=0;
 
 void goto_symext::do_simplify(exprt &expr)
@@ -22,23 +21,9 @@ void goto_symext::do_simplify(exprt &expr)
     simplify(expr, ns);
 }
 
-nondet_symbol_exprt goto_symext::build_symex_nondet(typet &type)
+nondet_symbol_exprt symex_nondet_generatort::operator()(typet &type)
 {
   irep_idt identifier = "symex::nondet" + std::to_string(nondet_count++);
   nondet_symbol_exprt new_expr(identifier, type);
   return new_expr;
 }
-
-void goto_symext::replace_nondet(exprt &expr)
-{
-  if(expr.id()==ID_side_effect &&
-     expr.get(ID_statement)==ID_nondet)
-  {
-    nondet_symbol_exprt new_expr = build_symex_nondet(expr.type());
-    new_expr.add_source_location()=expr.source_location();
-    expr.swap(new_expr);
-  }
-  else
-    Forall_operands(it, expr)
-      replace_nondet(*it);
-}

src/goto-symex/goto_symex.h

@@ -38,6 +38,16 @@ class namespacet;
 class side_effect_exprt;
 class typecast_exprt;
 
+/// Functor generating fresh nondet symbols
+class symex_nondet_generatort
+{
+public:
+  nondet_symbol_exprt operator()(typet &type);
+
+private:
+  unsigned nondet_count = 0;
+};
+
 /// \brief The main class for the forward symbolic simulator
 ///
 /// Higher-level architectural information on symbolic execution is
@@ -238,19 +248,6 @@ class goto_symext
 
   const irep_idt guard_identifier;
 
-  // symex
-  virtual void symex_transition(
-    statet &,
-    goto_programt::const_targett to,
-    bool is_backwards_goto);
-
-  virtual void symex_transition(statet &state)
-  {
-    goto_programt::const_targett next=state.source.pc;
-    ++next;
-    symex_transition(state, next, false);
-  }
-
   virtual void symex_goto(statet &);
   virtual void symex_start_thread(statet &);
   virtual void symex_atomic_begin(statet &);
@@ -333,8 +330,6 @@ class goto_symext
     statet &,
     const goto_functionst::goto_functiont &);
 
-  nondet_symbol_exprt build_symex_nondet(typet &type);
-
   // exceptions
   void symex_throw(statet &);
   void symex_catch(statet &);
@@ -414,10 +409,9 @@ class goto_symext
   virtual void symex_input(statet &, const codet &);
   virtual void symex_output(statet &, const codet &);
 
-  static unsigned nondet_count;
+  symex_nondet_generatort build_symex_nondet;
   static unsigned dynamic_counter;
 
-  void replace_nondet(exprt &);
   void rewrite_quantifiers(exprt &, statet &);
 
   path_storaget &path_storage;
@@ -465,4 +459,11 @@ class goto_symext
   }
 };
 
+void symex_transition(goto_symext::statet &state);
+
+void symex_transition(
+  goto_symext::statet &,
+  goto_programt::const_targett to,
+  bool is_backwards_goto);
+
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H

src/goto-symex/symex_clean_expr.cpp

@@ -135,12 +135,28 @@ static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
   }
 }
 
+static void
+replace_nondet(exprt &expr, symex_nondet_generatort &build_symex_nondet)
+{
+  if(expr.id() == ID_side_effect && expr.get(ID_statement) == ID_nondet)
+  {
+    nondet_symbol_exprt new_expr = build_symex_nondet(expr.type());
+    new_expr.add_source_location() = expr.source_location();
+    expr.swap(new_expr);
+  }
+  else
+  {
+    Forall_operands(it, expr)
+      replace_nondet(*it, build_symex_nondet);
+  }
+}
+
 void goto_symext::clean_expr(
   exprt &expr,
   statet &state,
   const bool write)
 {
-  replace_nondet(expr);
+  replace_nondet(expr, build_symex_nondet);
   dereference(expr, state, write);
 
   // make sure all remaining byte extract operations use the root

src/goto-symex/symex_main.cpp

@@ -22,8 +22,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <analyses/dirty.h>
 
-void goto_symext::symex_transition(
-  statet &state,
+void symex_transition(
+  goto_symext::statet &state,
   goto_programt::const_targett to,
   bool is_backwards_goto)
 {
@@ -34,7 +34,7 @@ void goto_symext::symex_transition(
     // 1. the transition from state.source.pc to "to" is not a backwards goto
     // or
     // 2. we are arriving from an outer loop
-    statet::framet &frame=state.top();
+    goto_symext::statet::framet &frame = state.top();
     const goto_programt::instructiont &instruction=*to;
     for(const auto &i_e : instruction.incoming_edges)
       if(i_e->is_goto() && i_e->is_backwards_goto() &&
@@ -46,6 +46,13 @@ void goto_symext::symex_transition(
   state.source.pc=to;
 }
 
+void symex_transition(goto_symext::statet &state)
+{
+  goto_programt::const_targett next = state.source.pc;
+  ++next;
+  symex_transition(state, next, false);
+}
+
 void goto_symext::vcc(
   const exprt &vcc_expr,
   const std::string &msg,