Use get_fresh_aux_symbol to construct dynamic objects

This avoids use of a global variable and reuses central infrastructure instead
of repeated local work. Note that this changes the names of dynamic objects as
the suffix now includes a $ character, and need not have any suffix, as well as
moving the counter out of the middle of C++/Java dynamic_X_array objects.

Author: tautschnig

jbmc/regression/jbmc-generics/constant_propagation/test.desc

@@ -3,8 +3,8 @@ Test.class
 --function Test.main --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
-^\{-\d+\} symex_dynamic::dynamic_object1#3 = \{ \{ \{ "java::GenericSub" \}, NULL, 0 \} \}$
-^\{-\d+\} symex_dynamic::dynamic_object1#4 = \{ \{ \{ "java::GenericSub" \}, NULL, 5 \} \}$
+^\{-\d+\} symex_dynamic::dynamic_object#3 = \{ \{ \{ "java::GenericSub" \}, NULL, 0 \} \}$
+^\{-\d+\} symex_dynamic::dynamic_object#4 = \{ \{ \{ "java::GenericSub" \}, NULL, 5 \} \}$
 --
 byte_extract_(big|little)_endian
 --

jbmc/regression/jbmc-strings/long_string/test_abort.desc

@@ -3,7 +3,7 @@ Test.class
 --function Test.checkAbort --trace
 ^EXIT=10$
 ^SIGNAL=0$
-dynamic_object[0-9]*=\(assignment removed\)
+dynamic_object\$?[0-9]*=\(assignment removed\)
 --
 --
 This tests that the object does not appear in the trace, because concretizing

jbmc/regression/jbmc/VarLengthArrayTrace1/test.desc

@@ -3,7 +3,7 @@ VarLengthArrayTrace1.class
 --trace --function VarLengthArrayTrace1.main
 ^EXIT=10$
 ^SIGNAL=0$
-dynamic_3_array\[1.*\]=10
+dynamic_array\$?\d*\[1.*\]=10
 --
 ^warning: ignoring
 assignment removed

jbmc/regression/jbmc/json_trace3/test.desc

@@ -4,7 +4,7 @@ Test.class
 activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
-"lhs": "dynamic_object3\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "18",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "8"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
+"lhs": "dynamic_object\$?\d*\[1L?\]",\n *"mode": "java",\n *"sourceLocation": \{\n *"bytecodeIndex": "18",\n *"file": "Test\.java",\n *"function": "java::Test\.main:\(\[J\)V",\n *"line": "8"\n *\},\n *"stepType": "assignment",\n *"thread": 0,\n *"value": \{\n *"binary": "0000000000000000000000000000000000000000000000000000000000000001",\n *"data": "1L",\n *"name": "integer",\n *"type": "long",\n *"width": 64
 --
 "name": "unknown"
 ^warning: ignoring

regression/cbmc/trace-values/trace-values.desc

@@ -11,7 +11,7 @@ trace-values.c
 ^  my_nested\[1.*\].f=5 .*$
 ^  null\$object=6 .*$
 ^  junk\$object=7 .*$
-^  dynamic_object1\[1.*\]=8 .*$
+^  dynamic_object\[1.*\]=8 .*$
 ^  my_nested\[1.*\]=\{ .f=0, .array=\{ 0, 4, 0 \} \} .*$
 ^VERIFICATION FAILED$
 --

src/goto-symex/auto_objects.cpp

@@ -11,27 +11,26 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_symex.h"
 
-#include <util/prefix.h>
 #include <util/cprover_prefix.h>
-#include <util/symbol_table.h>
+#include <util/fresh_symbol.h>
+#include <util/prefix.h>
 #include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 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.name="symex::"+id2string(symbol.base_name);
-  symbol.is_lvalue=true;
-  symbol.type=type;
-  symbol.mode=ID_C;
-
-  state.symbol_table.add(symbol);
-
-  return symbol_exprt(symbol.name, symbol.type);
+  symbolt &symbol = get_fresh_aux_symbol(
+    type,
+    "symex",
+    "auto_object",
+    state.source.pc->source_location,
+    ID_C,
+    state.symbol_table);
+  symbol.is_thread_local = false;
+  symbol.is_file_local = false;
+
+  return symbol.symbol_expr();
 }
 
 void goto_symext::initialize_auto_object(const exprt &expr, statet &state)
@@ -88,7 +87,7 @@ void goto_symext::trigger_auto_object(const exprt &expr, statet &state)
       const symbolt &symbol=
         ns.lookup(obj_identifier);
 
-      if(has_prefix(id2string(symbol.base_name), "auto_object"))
+      if(has_prefix(id2string(symbol.name), "symex::auto_object"))
       {
         // done already?
         if(state.level2.current_names.find(ssa_expr.get_identifier())==

src/goto-symex/goto_symex.cpp

@@ -13,8 +13,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/simplify_expr.h>
 
-unsigned goto_symext::dynamic_counter=0;
-
 void goto_symext::do_simplify(exprt &expr)
 {
   if(symex_config.simplify_opt)

src/goto-symex/goto_symex.h

@@ -550,9 +550,6 @@ class goto_symext
   /// \param code: The cleaned up output instruction
   virtual void symex_output(statet &state, const codet &code);
 
-  /// A monotonically increasing index for each created dynamic object
-  static unsigned dynamic_counter;
-
   void rewrite_quantifiers(exprt &, statet &);
 
   /// \brief Symbolic execution paths to be resumed later

src/goto-symex/symex_builtin_functions.cpp

@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
+#include <util/fresh_symbol.h>
 #include <util/invariant_utils.h>
 #include <util/optional.h>
 #include <util/pointer_offset_size.h>
@@ -54,8 +55,6 @@ void goto_symext::symex_allocate(
   if(lhs.is_nil())
     return; // ignore
 
-  dynamic_counter++;
-
   exprt size=code.op0();
   optionalt<typet> object_type;
   auto function_symbol = outer_symbol_table.lookup(state.source.function_id);
@@ -132,19 +131,16 @@ void goto_symext::symex_allocate(
     {
       exprt &array_size = to_array_type(*object_type).size();
 
-      auxiliary_symbolt size_symbol;
-
-      size_symbol.base_name=
-        "dynamic_object_size"+std::to_string(dynamic_counter);
-      size_symbol.name =
-        SYMEX_DYNAMIC_PREFIX "::" + id2string(size_symbol.base_name);
-      size_symbol.type=tmp_size.type();
-      size_symbol.mode = mode;
+      symbolt &size_symbol = get_fresh_aux_symbol(
+        tmp_size.type(),
+        SYMEX_DYNAMIC_PREFIX,
+        "dynamic_object_size",
+        code.source_location(),
+        mode,
+        state.symbol_table);
       size_symbol.type.set(ID_C_constant, true);
       size_symbol.value = array_size;
 
-      state.symbol_table.add(size_symbol);
-
       code_assignt assignment(size_symbol.symbol_expr(), array_size);
       array_size = assignment.lhs();
 
@@ -153,17 +149,17 @@ void goto_symext::symex_allocate(
   }
 
   // value
-  symbolt value_symbol;
-
-  value_symbol.base_name="dynamic_object"+std::to_string(dynamic_counter);
-  value_symbol.name =
-    SYMEX_DYNAMIC_PREFIX "::" + id2string(value_symbol.base_name);
-  value_symbol.is_lvalue=true;
-  value_symbol.type = *object_type;
+  symbolt &value_symbol = get_fresh_aux_symbol(
+    *object_type,
+    SYMEX_DYNAMIC_PREFIX,
+    "dynamic_object",
+    code.source_location(),
+    mode,
+    state.symbol_table);
+  value_symbol.is_auxiliary = false;
+  value_symbol.is_thread_local = false;
+  value_symbol.is_file_local = false;
   value_symbol.type.set(ID_C_dynamic, true);
-  value_symbol.mode = mode;
-
-  state.symbol_table.add(value_symbol);
 
   // to allow constant propagation
   exprt zero_init = state.rename(code.op1(), ns);
@@ -383,47 +379,46 @@ void goto_symext::symex_cpp_new(
   const exprt &lhs,
   const side_effect_exprt &code)
 {
-  bool do_array;
-
-  PRECONDITION(code.type().id() == ID_pointer);
-
   const auto &pointer_type = to_pointer_type(code.type());
 
-  do_array =
+  const bool do_array =
     (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));
-
   // value
-  symbolt symbol;
-  symbol.base_name=
-    do_array?"dynamic_"+count_string+"_array":
-             "dynamic_"+count_string+"_value";
-  symbol.name = SYMEX_DYNAMIC_PREFIX "::" + id2string(symbol.base_name);
-  symbol.is_lvalue=true;
-  if(code.get(ID_statement)==ID_cpp_new_array ||
-     code.get(ID_statement)==ID_cpp_new)
-    symbol.mode=ID_cpp;
-  else if(code.get(ID_statement) == ID_java_new_array_data)
-    symbol.mode=ID_java;
-  else
-    INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code);
-
+  optionalt<typet> type;
   if(do_array)
   {
     exprt size_arg = static_cast<const exprt &>(code.find(ID_size));
     clean_expr(size_arg, state, false);
-    symbol.type = array_typet(pointer_type.subtype(), size_arg);
+    type = array_typet(pointer_type.subtype(), size_arg);
   }
   else
-    symbol.type = pointer_type.subtype();
+    type = pointer_type.subtype();
 
-  symbol.type.set(ID_C_dynamic, true);
+  irep_idt mode;
+  if(
+    code.get(ID_statement) == ID_cpp_new_array ||
+    code.get(ID_statement) == ID_cpp_new)
+  {
+    mode = ID_cpp;
+  }
+  else if(code.get(ID_statement) == ID_java_new_array_data)
+    mode = ID_java;
+  else
+    INVARIANT_WITH_IREP(false, "Unexpected side effect expression", code);
 
-  state.symbol_table.add(symbol);
+  symbolt &symbol = get_fresh_aux_symbol(
+    *type,
+    SYMEX_DYNAMIC_PREFIX,
+    (do_array ? "dynamic_array" : "dynamic_value"),
+    code.source_location(),
+    mode,
+    state.symbol_table);
+  symbol.is_auxiliary = false;
+  symbol.is_thread_local = false;
+  symbol.is_file_local = false;
+  symbol.type.set(ID_C_dynamic, true);
 
   // make symbol expression