Use get_fresh_aux_symbol to construct dynamic objects

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/StringBuilderConstructors01/test-no-arg-fail.desc

@@ -4,9 +4,9 @@ StringBuilderConstructors01
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-dynamic_object2=\{\s*\}
+dynamic_object\$0=\{\s*\}
 --
 ^warning: ignoring
 --
-The check for dynamic_object2 is to make sure the array is created empty and
+The check for dynamic_object\$0 is to make sure the array is created empty and
 is not given arbitrary content before its final assignment.

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/array-cell-sensitivity1/test-max-array-size-10.desc

@@ -1,17 +1,17 @@
 CORE
 Test
 --function Test.main --show-vcc --max-field-sensitivity-array-size 10
-symex_dynamic::dynamic_2_array#2\[\[0\]\] =
-symex_dynamic::dynamic_2_array#2\[\[1\]\] =
-symex_dynamic::dynamic_2_array#2\[\[2\]\] =
-symex_dynamic::dynamic_2_array#2\[\[3\]\] =
-symex_dynamic::dynamic_2_array#2\[\[4\]\] =
-symex_dynamic::dynamic_2_array#2\[\[5\]\] =
-symex_dynamic::dynamic_2_array#2\[\[6\]\] =
-symex_dynamic::dynamic_2_array#2\[\[7\]\] =
-symex_dynamic::dynamic_2_array#2\[\[8\]\] =
-symex_dynamic::dynamic_2_array#2\[\[9\]\] =
-symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
+symex_dynamic::dynamic_array#2\[\[0\]\] =
+symex_dynamic::dynamic_array#2\[\[1\]\] =
+symex_dynamic::dynamic_array#2\[\[2\]\] =
+symex_dynamic::dynamic_array#2\[\[3\]\] =
+symex_dynamic::dynamic_array#2\[\[4\]\] =
+symex_dynamic::dynamic_array#2\[\[5\]\] =
+symex_dynamic::dynamic_array#2\[\[6\]\] =
+symex_dynamic::dynamic_array#2\[\[7\]\] =
+symex_dynamic::dynamic_array#2\[\[8\]\] =
+symex_dynamic::dynamic_array#2\[\[9\]\] =
+symex_dynamic::dynamic_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
 ^EXIT=0$
 ^SIGNAL=0$
 --

jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc

@@ -3,9 +3,9 @@ Test
 --function Test.main --show-vcc --max-field-sensitivity-array-size 9
 ^EXIT=0$
 ^SIGNAL=0$
-symex_dynamic::dynamic_2_array#[0-9]\[1\]
+symex_dynamic::dynamic_array#[0-9]\[1\]
 --
-symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\]
+symex_dynamic::dynamic_array#[0-9]\[\[[0-9]\]\]
 --
 This checks that field sensitvity is not applied to an array of size 10
-when the max is set to 9.
+when the max is set to 9.

jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc

@@ -3,9 +3,9 @@ Test
 --function Test.main --show-vcc --no-array-field-sensitivity
 ^EXIT=0$
 ^SIGNAL=0$
-symex_dynamic::dynamic_2_array#[0-9]\[1\]
+symex_dynamic::dynamic_array#[0-9]\[1\]
 --
-symex_dynamic::dynamic_2_array#[0-9]\[\[[0-9]\]\]
+symex_dynamic::dynamic_array#[0-9]\[\[[0-9]\]\]
 --
 This checks that field sensitvity is not applied to arrays when
-no-array-field-sensitivity is used.
+no-array-field-sensitivity is used.

jbmc/regression/jbmc/array-cell-sensitivity1/test.desc

@@ -1,21 +1,21 @@
 CORE
 Test
 --function Test.main --show-vcc
-symex_dynamic::dynamic_2_array#2\[\[0\]\] =
-symex_dynamic::dynamic_2_array#2\[\[1\]\] =
-symex_dynamic::dynamic_2_array#2\[\[2\]\] =
-symex_dynamic::dynamic_2_array#2\[\[3\]\] =
-symex_dynamic::dynamic_2_array#2\[\[4\]\] =
-symex_dynamic::dynamic_2_array#2\[\[5\]\] =
-symex_dynamic::dynamic_2_array#2\[\[6\]\] =
-symex_dynamic::dynamic_2_array#2\[\[7\]\] =
-symex_dynamic::dynamic_2_array#2\[\[8\]\] =
-symex_dynamic::dynamic_2_array#2\[\[9\]\] =
-symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
+symex_dynamic::dynamic_array#2\[\[0\]\] =
+symex_dynamic::dynamic_array#2\[\[1\]\] =
+symex_dynamic::dynamic_array#2\[\[2\]\] =
+symex_dynamic::dynamic_array#2\[\[3\]\] =
+symex_dynamic::dynamic_array#2\[\[4\]\] =
+symex_dynamic::dynamic_array#2\[\[5\]\] =
+symex_dynamic::dynamic_array#2\[\[6\]\] =
+symex_dynamic::dynamic_array#2\[\[7\]\] =
+symex_dynamic::dynamic_array#2\[\[8\]\] =
+symex_dynamic::dynamic_array#2\[\[9\]\] =
+symex_dynamic::dynamic_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
 ^EXIT=0$
 ^SIGNAL=0$
 --
-symex_dynamic::dynamic_2_array#3\[\[[023456789]\]\] =
+symex_dynamic::dynamic_array#3\[\[[023456789]\]\] =
 --
 This checks that a write to a Java array with an unknown index uses a whole-array
 write followed by array-cell expansion, but one targeting a constant index uses

jbmc/regression/jbmc/array-cell-sensitivity2/test.desc

@@ -1,13 +1,13 @@
 CORE
 Test
 --function Test.main --show-vcc
-symex_dynamic::dynamic_object6#3\.\.data =
-symex_dynamic::dynamic_object3#3\.\.data =
+symex_dynamic::dynamic_object\$3#3\.\.data =
+symex_dynamic::dynamic_object\$1#3\.\.data =
 ^EXIT=0$
 ^SIGNAL=0$
 --
-symex_dynamic::dynamic_object6#3\.\.data = symex_dynamic::dynamic_object6#3\.data
-symex_dynamic::dynamic_object3#3\.\.data = symex_dynamic::dynamic_object3#3\.data
+symex_dynamic::dynamic_object\$3#3\.\.data = symex_dynamic::dynamic_object\$3#3\.data
+symex_dynamic::dynamic_object\$1#3\.\.data = symex_dynamic::dynamic_object\$1#3\.data
 --
 This checks that a write using a mix of field and array accessors uses a field-sensitive
 symbol (the data field of the possible ultimate target objects) rather than using

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

jbmc/regression/jbmc/throwing-function-return-value/test.desc

@@ -1,7 +1,7 @@
 CORE
 Test
 --function Test.main --show-vcc
-java::Test\.main:\(Z\)V::14::t1!0@1#\d+ = address_of\(symex_dynamic::dynamic_object\d+\)
+java::Test\.main:\(Z\)V::14::t1!0@1#\d+ = address_of\(symex_dynamic::dynamic_object\$1\)
 java::Test\.main:\(Z\)V::9::x!0@1#\d+ = java::Test\.main:\(Z\)V::9::x!0@1#\d+ \+ 5
 java::Test\.g:\(\)I#return_value!0#[0-9]+ = 5
 ^EXIT=0$

jbmc/regression/strings-smoke-tests/java_parseint/test4.desc

@@ -5,7 +5,7 @@ Test4
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* FAILURE$
 ^\[.*assertion.2\].* line 9.* FAILURE$
-dynamic_object2=\{ '5', '0' \}
-dynamic_object2=\{ 'X', 'Y', 'Z', 'W' \}
+dynamic_object\$0=\{ '5', '0' \}
+dynamic_object\$0=\{ 'X', 'Y', 'Z', 'W' \}
 --
 non equal types

jbmc/regression/strings-smoke-tests/java_parselong/test_other_branches_possible.desc

@@ -5,7 +5,7 @@ Test_other_branches_possible
 ^SIGNAL=0$
 ^\[.*assertion.1\].* line 6.* FAILURE$
 ^\[.*assertion.2\].* line 9.* FAILURE$
-dynamic_object2=\{ '5', '0' \}
-dynamic_object2=\{ 'X', 'Y', 'Z', 'W' \}
+dynamic_object\$0=\{ '5', '0' \}
+dynamic_object\$0=\{ 'X', 'Y', 'Z', 'W' \}
 --
 non equal types

regression/cbmc/array-cell-sensitivity5/test.desc

@@ -1,20 +1,20 @@
 CORE
 test.c
 --show-vcc
-symex_dynamic::dynamic_object1#2\[\[1\]\] =
-symex_dynamic::dynamic_object1#2\[\[2\]\] =
-symex_dynamic::dynamic_object1#2\[\[3\]\] =
-symex_dynamic::dynamic_object1#2\[\[4\]\] =
-symex_dynamic::dynamic_object1#2\[\[5\]\] =
-symex_dynamic::dynamic_object1#2\[\[6\]\] =
-symex_dynamic::dynamic_object1#2\[\[7\]\] =
-symex_dynamic::dynamic_object1#2\[\[8\]\] =
-symex_dynamic::dynamic_object1#2\[\[9\]\] =
-symex_dynamic::dynamic_object1#3\[\[1\]\] =
+symex_dynamic::dynamic_object#2\[\[1\]\] =
+symex_dynamic::dynamic_object#2\[\[2\]\] =
+symex_dynamic::dynamic_object#2\[\[3\]\] =
+symex_dynamic::dynamic_object#2\[\[4\]\] =
+symex_dynamic::dynamic_object#2\[\[5\]\] =
+symex_dynamic::dynamic_object#2\[\[6\]\] =
+symex_dynamic::dynamic_object#2\[\[7\]\] =
+symex_dynamic::dynamic_object#2\[\[8\]\] =
+symex_dynamic::dynamic_object#2\[\[9\]\] =
+symex_dynamic::dynamic_object#3\[\[1\]\] =
 ^EXIT=0$
 ^SIGNAL=0$
 --
-symex_dynamic::dynamic_object1#[3-9]\[[0-9]+\]
+symex_dynamic::dynamic_object#[3-9]\[[0-9]+\]
 --
 This checks that a write with a non-constant index leads to a whole-array
 operation followed by expansion into individual array cells, while a write with

regression/cbmc/array-cell-sensitivity6/test.desc

@@ -1,20 +1,20 @@
 CORE
 test.c
 --show-vcc
-symex_dynamic::dynamic_object1#2\[\[1\]\] =
-symex_dynamic::dynamic_object1#2\[\[2\]\] =
-symex_dynamic::dynamic_object1#2\[\[3\]\] =
-symex_dynamic::dynamic_object1#2\[\[4\]\] =
-symex_dynamic::dynamic_object1#2\[\[5\]\] =
-symex_dynamic::dynamic_object1#2\[\[6\]\] =
-symex_dynamic::dynamic_object1#2\[\[7\]\] =
-symex_dynamic::dynamic_object1#2\[\[8\]\] =
-symex_dynamic::dynamic_object1#2\[\[9\]\] =
-symex_dynamic::dynamic_object1#3\[\[1\]\] =
+symex_dynamic::dynamic_object#2\[\[1\]\] =
+symex_dynamic::dynamic_object#2\[\[2\]\] =
+symex_dynamic::dynamic_object#2\[\[3\]\] =
+symex_dynamic::dynamic_object#2\[\[4\]\] =
+symex_dynamic::dynamic_object#2\[\[5\]\] =
+symex_dynamic::dynamic_object#2\[\[6\]\] =
+symex_dynamic::dynamic_object#2\[\[7\]\] =
+symex_dynamic::dynamic_object#2\[\[8\]\] =
+symex_dynamic::dynamic_object#2\[\[9\]\] =
+symex_dynamic::dynamic_object#3\[\[1\]\] =
 ^EXIT=0$
 ^SIGNAL=0$
 --
-symex_dynamic::dynamic_object1#[3-9]\[[0-9]+\]
+symex_dynamic::dynamic_object#[3-9]\[[0-9]+\]
 --
 This checks that a write with a non-constant index leads to a whole-array
 operation followed by expansion into individual array cells, while a write with

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc

@@ -1,8 +1,8 @@
 CORE
 double_deref_with_pointer_arithmetic.c
 --show-vcc
-^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
-^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
+^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object#3\[\[0\]\], symex_dynamic::dynamic_object#3\[\[1\]\] \}\[cast\(mod\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
+^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object\$[01]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object\$[01]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc

@@ -1,7 +1,7 @@
 CORE
 double_deref_with_pointer_arithmetic_single_alias.c
 --show-vcc
-\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object2\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)
+\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object\$0\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)
 ^EXIT=0$
 ^SIGNAL=0$
 --

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/ansi-c/expr2c.cpp

@@ -1648,7 +1648,7 @@ std::string expr2ct::convert_symbol(const exprt &src)
     dest=id2string(entry->second);
 
     #if 0
-    if(has_prefix(id2string(id), SYMEX_DYNAMIC_PREFIX "dynamic_object"))
+    if(has_prefix(id2string(id), SYMEX_DYNAMIC_PREFIX "::dynamic_object"))
     {
       if(sizeof_nesting++ == 0)
         dest+=" /*"+convert(src.type());

src/goto-instrument/race_check.cpp

@@ -130,7 +130,7 @@ static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
     identifier == "stdout" || identifier == "stderr" ||
     identifier == "sys_nerr" ||
     has_prefix(id2string(identifier), "symex::invalid_object") ||
-    has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "dynamic_object"))
+    has_prefix(id2string(identifier), SYMEX_DYNAMIC_PREFIX "::dynamic_object"))
     return false; // no race check
 
   const symbolt &symbol=ns.lookup(identifier);

src/goto-programs/graphml_witness.cpp

@@ -459,9 +459,9 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         }
         else if(
           !contains_symbol_prefix(
-            it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
+            it->full_lhs_value, SYMEX_DYNAMIC_PREFIX "::dynamic_object") &&
           !contains_symbol_prefix(
-            it->full_lhs, SYMEX_DYNAMIC_PREFIX "dynamic_object") &&
+            it->full_lhs, SYMEX_DYNAMIC_PREFIX "::dynamic_object") &&
           lhs_id.find("thread") == std::string::npos &&
           lhs_id.find("mutex") == std::string::npos &&
           (!it->full_lhs_value.is_constant() ||

src/goto-symex/auto_objects.cpp

@@ -9,29 +9,28 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Symbolic Execution of ANSI-C
 
-#include "goto_symex.h"
-
+#include <util/fresh_symbol.h>
 #include <util/pointer_expr.h>
 #include <util/prefix.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 
+#include "goto_symex.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)
@@ -85,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