Maintain nondet and dynamic counters across symex instances

Use the path storage, which maintains state across different symex
instantiations. While at it, also make the counters std::size_t as using limited
bitwidth is not a meaningful optimisation here.

Author: tautschnig

regression/cbmc/Bitfields3/paths.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--pointer-check --bounds-check --paths lifo
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

scripts/delete_failing_smt2_solver_tests

@@ -4,6 +4,7 @@ cd regression/cbmc
 rm Anonymous_Struct3/test.desc
 rm Array_operations1/test.desc
 rm Bitfields3/test.desc
+rm Bitfields3/paths.desc
 rm Empty_struct1/test.desc
 rm Endianness4/test.desc
 rm Endianness6/test.desc

src/goto-symex/auto_objects.cpp

@@ -18,12 +18,11 @@ Author: Daniel Kroening, [email protected]
 
 exprt goto_symext::make_auto_object(const typet &type, statet &state)
 {
-  dynamic_counter++;
-
   // produce auto-object symbol
   symbolt symbol;
 
-  symbol.base_name="auto_object"+std::to_string(dynamic_counter);
+  symbol.base_name =
+    "auto_object" + std::to_string(++path_storage.dynamic_counter);
   symbol.name="symex::"+id2string(symbol.base_name);
   symbol.is_lvalue=true;
   symbol.type=type;

src/goto-symex/goto_symex.cpp

@@ -13,16 +13,13 @@ 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)
 {
   if(symex_config.simplify_opt)
     simplify(expr, ns);
 }
 
-nondet_symbol_exprt build_symex_nondet(typet &type, unsigned &nondet_count)
+nondet_symbol_exprt build_symex_nondet(typet &type, std::size_t &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

@@ -408,9 +408,6 @@ class goto_symext
   virtual void symex_input(statet &, const codet &);
   virtual void symex_output(statet &, const codet &);
 
-  static unsigned nondet_count;
-  static unsigned dynamic_counter;
-
   void rewrite_quantifiers(exprt &, statet &);
 
   path_storaget &path_storage;
@@ -463,7 +460,7 @@ class goto_symext
   }
 };
 
-nondet_symbol_exprt build_symex_nondet(typet &type, unsigned &nondet_count);
+nondet_symbol_exprt build_symex_nondet(typet &type, std::size_t &nondet_count);
 
 void symex_transition(goto_symext::statet &state);
 

src/goto-symex/path_storage.h

@@ -85,6 +85,10 @@ class path_storaget
     return size() == 0;
   };
 
+  /// Counters for nondet and dynamic objects, which require unique names
+  std::size_t nondet_count;
+  std::size_t dynamic_counter;
+
 private:
   // Derived classes should override these methods, allowing the base class to
   // enforce preconditions.

src/goto-symex/symex_builtin_functions.cpp

@@ -52,7 +52,7 @@ void goto_symext::symex_allocate(
   if(lhs.is_nil())
     return; // ignore
 
-  dynamic_counter++;
+  const std::size_t dynamic_counter = ++path_storage.dynamic_counter;
 
   exprt size=code.op0();
   optionalt<typet> object_type;
@@ -178,7 +178,8 @@ void goto_symext::symex_allocate(
   }
   else
   {
-    const exprt nondet = build_symex_nondet(*object_type, nondet_count);
+    const exprt nondet =
+      build_symex_nondet(*object_type, path_storage.nondet_count);
     const code_assignt assignment(value_symbol.symbol_expr(), nondet);
     symex_assign(state, assignment);
   }
@@ -396,9 +397,8 @@ void goto_symext::symex_cpp_new(
     (code.get(ID_statement) == ID_cpp_new_array ||
      code.get(ID_statement) == ID_java_new_array_data);
 
-  dynamic_counter++;
-
-  const std::string count_string(std::to_string(dynamic_counter));
+  const std::string count_string(
+    std::to_string(++path_storage.dynamic_counter));
 
   // value
   symbolt symbol;

src/goto-symex/symex_clean_expr.cpp

@@ -160,7 +160,7 @@ static void adjust_byte_extract_rec(exprt &expr, const namespacet &ns)
   }
 }
 
-static void replace_nondet(exprt &expr, unsigned &nondet_count)
+static void replace_nondet(exprt &expr, std::size_t &nondet_count)
 {
   if(expr.id() == ID_side_effect && expr.get(ID_statement) == ID_nondet)
   {
@@ -181,7 +181,7 @@ void goto_symext::clean_expr(
   statet &state,
   const bool write)
 {
-  replace_nondet(expr, nondet_count);
+  replace_nondet(expr, path_storage.nondet_count);
   dereference(expr, state, write);
 
   // make sure all remaining byte extract operations use the root