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,9 +3,9 @@ Test
 --function Test.main --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
-^\{-\d+\} symex_dynamic::dynamic_object1#2\.\.@Generic\.\[email protected]\.\.@class_identifier = "java::GenericSub"$
-^\{-\d+\} symex_dynamic::dynamic_object1#2\.\.@Generic\.\.key = NULL$
-^\{-\d+\} symex_dynamic::dynamic_object1#3\.\.@Generic\.\.x = 5$
+^\{-\d+\} symex_dynamic::dynamic_object#2\.\.@Generic\.\[email protected]\.\.@class_identifier = "java::GenericSub"$
+^\{-\d+\} symex_dynamic::dynamic_object#2\.\.@Generic\.\.key = NULL$
+^\{-\d+\} symex_dynamic::dynamic_object#3\.\.@Generic\.\.x = 5$
 --
 byte_extract_(big|little)_endian
 --

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

@@ -3,7 +3,7 @@ Test
 --function Test.checkAbort --trace --max-nondet-string-length 100000000
 ^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
 --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
 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

@@ -10,7 +10,7 @@ trace-values.c
 ^  my_nested\[0.*\].array\[1.*\]=4 .*$
 ^  my_nested\[1.*\].f=5 .*$
 ^  junk\$object=7 .*$
-^  dynamic_object1\[1.*\]=8 .*$
+^  dynamic_object\[1.*\]=8 .*$
 ^  my_nested\[1.*\](=\{ )?.f=0[ ,]
 ^  my_nested\[1.*\](=\{ .f=0, )?.array=\{ 0, 4, 0 \}
 ^  s\.f=42 \([0 ]+ 00101010\)$

src/goto-symex/auto_objects.cpp

@@ -19,20 +19,18 @@ 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.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)
@@ -86,7 +84,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.base_name), "symex::auto_object"))
         {
           // done already?
           if(!state.get_level2().current_names.has_key(

src/goto-symex/goto_symex.cpp

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

src/goto-symex/goto_symex.h

@@ -776,9 +776,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

@@ -56,8 +56,6 @@ void goto_symext::symex_allocate(
   if(lhs.is_nil())
     return; // ignore
 
-  dynamic_counter++;
-
   exprt size = to_binary_expr(code).op0();
   optionalt<typet> object_type;
   auto function_symbol = outer_symbol_table.lookup(state.source.function_id);
@@ -137,19 +135,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);
-
       auto array_size_rhs = array_size;
       array_size = size_symbol.symbol_expr();
 
@@ -158,17 +153,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(to_binary_expr(code).op1(), ns).get();
@@ -471,47 +466,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 =
       clean_expr(static_cast<const exprt &>(code.find(ID_size)), state, false);
-    symbol.type = array_typet(pointer_type.base_type(), size_arg);
+    type = array_typet(pointer_type.base_type(), size_arg);
   }
   else
-    symbol.type = pointer_type.base_type();
+    type = pointer_type.base_type();
 
-  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