Revert "Replace nondet_count by a functor"

This reverts commit 8fb2902.

Nondet symbol names need to be unique across goto_symext instantiations.

Author: tautschnig

src/goto-symex/goto_symex.cpp

@@ -13,6 +13,7 @@ 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)
@@ -21,7 +22,7 @@ void goto_symext::do_simplify(exprt &expr)
     simplify(expr, ns);
 }
 
-nondet_symbol_exprt symex_nondet_generatort::operator()(typet &type)
+nondet_symbol_exprt build_symex_nondet(typet &type, unsigned &nondet_count)
 {
   irep_idt identifier = "symex::nondet" + std::to_string(nondet_count++);
   nondet_symbol_exprt new_expr(identifier, type);

src/goto-symex/goto_symex.h

@@ -38,16 +38,6 @@ 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;
-};
-
 /// Configuration of the symbolic execution
 struct symex_configt final
 {
@@ -418,7 +408,7 @@ class goto_symext
   virtual void symex_input(statet &, const codet &);
   virtual void symex_output(statet &, const codet &);
 
-  symex_nondet_generatort build_symex_nondet;
+  static unsigned nondet_count;
   static unsigned dynamic_counter;
 
   void rewrite_quantifiers(exprt &, statet &);
@@ -473,6 +463,8 @@ class goto_symext
   }
 };
 
+nondet_symbol_exprt build_symex_nondet(typet &type, unsigned &nondet_count);
+
 void symex_transition(goto_symext::statet &state);
 
 void symex_transition(

src/goto-symex/symex_builtin_functions.cpp

@@ -178,7 +178,7 @@ void goto_symext::symex_allocate(
   }
   else
   {
-    const exprt nondet = build_symex_nondet(*object_type);
+    const exprt nondet = build_symex_nondet(*object_type, nondet_count);
     const code_assignt assignment(value_symbol.symbol_expr(), nondet);
     symex_assign(state, assignment);
   }

src/goto-symex/symex_clean_expr.cpp

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