Use get_fresh_aux_symbol to construct dynamic objects

tautschnig · tautschnig · commit e51444e28e94 · 2022-12-01T16:08:00.000Z
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.
diff --git a/jbmc/regression/jbmc-generics/constant_propagation/test.desc b/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\.\.@java.lang.Object\.\.@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\.\.@java.lang.Object\.\.@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
 --
diff --git a/jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc b/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.
diff --git a/jbmc/regression/jbmc-strings/long_string/test_abort.desc b/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
diff --git a/jbmc/regression/jbmc/VarLengthArrayTrace1/test.desc b/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
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc b/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$
 --
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-9.desc b/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.
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test-no-array-field-sensitivity.desc b/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.
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity1/test.desc b/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
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity2/test.desc b/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
diff --git a/jbmc/regression/jbmc/json_trace3/test.desc b/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
diff --git a/jbmc/regression/jbmc/throwing-function-return-value/test.desc b/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$
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test4.desc b/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
diff --git a/jbmc/regression/strings-smoke-tests/java_parselong/test_other_branches_possible.desc b/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
diff --git a/regression/cbmc/array-cell-sensitivity5/test.desc b/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
diff --git a/regression/cbmc/array-cell-sensitivity6/test.desc b/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
diff --git a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc b/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$
 --
diff --git a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc b/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$
 --
diff --git a/regression/cbmc/trace-values/trace-values.desc b/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\)$
diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp
@@ -9,29 +9,28 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \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(
diff --git a/src/goto-symex/goto_symex.cpp b/src/goto-symex/goto_symex.cpp
@@ -29,8 +29,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <climits>
 
-unsigned goto_symext::dynamic_counter=0;
-
 void goto_symext::do_simplify(exprt &expr)
 {
   if(symex_config.simplify_opt)
diff --git a/src/goto-symex/goto_symex.h b/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
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
