Skip to content

Commit 06b3adc

Browse files
peterschrammelpeterschrammel
authored
Merge pull request #2077 from peterschrammel/stable-tmp-var-names
Prefix temporary variable names with function id
2 parents 47951ca + 0b3170d commit 06b3adc

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

46 files changed

+470
-258
lines changed

‎regression/cbmc/Quantifiers-not-exists/test.desc

+5-5
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ main.c
33

44
^\*\* Results:$
55
^\[main.assertion.1\] assertion a\[.*\]\[.*\] > 10: SUCCESS$
6-
^\[main.assertion.2\] assertion tmp_if_expr\$3: SUCCESS$
7-
^\[main.assertion.3\] assertion tmp_if_expr\$6: SUCCESS$
8-
^\[main.assertion.4\] assertion tmp_if_expr\$9: SUCCESS$
9-
^\[main.assertion.5\] assertion tmp_if_expr\$12: SUCCESS$
10-
^\[main.assertion.6\] assertion tmp_if_expr\$15: SUCCESS$
6+
^\[main.assertion.2\] assertion tmp_if_expr\$\d+: SUCCESS$
7+
^\[main.assertion.3\] assertion tmp_if_expr\$\d+: SUCCESS$
8+
^\[main.assertion.4\] assertion tmp_if_expr\$\d+: SUCCESS$
9+
^\[main.assertion.5\] assertion tmp_if_expr\$\d+: SUCCESS$
10+
^\[main.assertion.6\] assertion tmp_if_expr\$\d+: SUCCESS$
1111
^\*\* 0 of 6 failed
1212
^VERIFICATION SUCCESSFUL$
1313
^EXIT=0$

‎regression/cbmc/Quantifiers-two-dimension-array/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ main.c
66
^\[main.assertion.2\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
77
^\[main.assertion.3\] assertion a\[.*\]\[.*\] == 1: SUCCESS$
88
^\[main.assertion.4\] assertion a\[.*\]\[.*\] == 2: SUCCESS$
9-
^\[main.assertion.5\] assertion tmp_if_expr\$3: SUCCESS$
9+
^\[main.assertion.5\] assertion tmp_if_expr\$\d+: SUCCESS$
1010
^\*\* 0 of 5 failed
1111
^VERIFICATION SUCCESSFUL$
1212
^EXIT=0$

‎regression/cbmc/Quantifiers-type/test.desc

+2-2
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ CORE
22
main.c
33

44
^\*\* Results:$
5-
^\[main.assertion.1\] assertion tmp_if_expr\$1: FAILURE$
6-
^\[main.assertion.2\] assertion tmp_if_expr\$2: SUCCESS$
5+
^\[main.assertion.1\] assertion tmp_if_expr(\$\d+)?: FAILURE$
6+
^\[main.assertion.2\] assertion tmp_if_expr\$\d+: SUCCESS$
77
^\*\* 1 of 2 failed
88
^VERIFICATION FAILED$
99
^EXIT=10$

‎regression/cbmc/pointer-function-parameters-2/test.desc

+4-4
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ main.c
33
--function fun --cover branch
44
^\*\* 7 of 7 covered \(100.0%\)$
55
^Test suite:$
6-
^a=\(\(signed int \*\*\)NULL\), tmp\$\d+=[^,]*, tmp\$\d+=[^,]*$
7-
^a=&tmp\$\d+!0, tmp\$\d+=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
8-
^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$
9-
^a=&tmp\$\d+!0, tmp\$\d+=&tmp\$\d+!0, tmp\$\d+=4$
6+
^a=\(\(signed int \*\*\)NULL\), tmp(\$\d+)?=[^,]*, tmp(\$\d+)?=[^,]*$
7+
^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$
8+
^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp\$\d+!0, tmp(\$\d+)?=(-[0-9]+|[012356789][0-9]*|4[0-9]+)$
9+
^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$
1010
^EXIT=0$
1111
^SIGNAL=0$
1212
--

‎regression/cbmc/pointer-function-parameters/test.desc

+3-3
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ main.c
33
--function fun --cover branch
44
^\*\* 5 of 5 covered \(100\.0%\)$
55
^Test suite:$
6-
^a=\(\(signed int \*\)NULL\), tmp\$\d+=[^,]*$
7-
^a=&tmp\$\d+!0, tmp\$\d+=4$
8-
^a=&tmp\$\d+!0, tmp\$\d+=([012356789][0-9]*|4[0-9]+)$
6+
^a=\(\(signed int \*\)NULL\), tmp(\$\d+)?=[^,]*$
7+
^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=4$
8+
^a=&tmp(\$\d+)?!0, tmp(\$\d+)?=([012356789][0-9]*|4[0-9]+)$
99
^EXIT=0$
1010
^SIGNAL=0$
1111
--

‎regression/goto-diff/java-tmp-vars-array/new.jar

662 Bytes
Binary file not shown.

‎regression/goto-diff/java-tmp-vars-array/new/Test.java

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
public class Test {
2+
public int[] f00(int[] x) {
3+
int[] y = new int[x.length];
4+
return y;
5+
}
6+
7+
public int[] f01(int[] z) {
8+
int[] w = new int[z.length];
9+
return w;
10+
}
11+
}

‎regression/goto-diff/java-tmp-vars-array/old.jar

668 Bytes
Binary file not shown.

‎regression/goto-diff/java-tmp-vars-array/old/Test.java

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
public class Test {
2+
public int[] f00(int[] x) {
3+
int[] y = x;
4+
return y;
5+
}
6+
7+
public int[] f01(int[] z) {
8+
int[] w = new int[z.length];
9+
return w;
10+
}
11+
}

‎regression/goto-diff/java-tmp-vars-array/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
new.jar
3+
old.jar
4+
// Enable multi-line checking
5+
activate-multi-line-match
6+
EXIT=0
7+
SIGNAL=0
8+
new functions:\nmodified functions:\n Test\.java: java::Test\.f00:\(\[I\)\[I\ndeleted functions:
9+
--
10+
^warning: ignoring

‎regression/goto-diff/java-tmp-vars-inc/new.jar

657 Bytes
Binary file not shown.

‎regression/goto-diff/java-tmp-vars-inc/new/Test.java

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
public class Test {
2+
public int f00(int x) {
3+
int y = x++;
4+
return y;
5+
}
6+
7+
public int f01(int z) {
8+
int w = z++;
9+
return w;
10+
}
11+
}

‎regression/goto-diff/java-tmp-vars-inc/old.jar

666 Bytes
Binary file not shown.

‎regression/goto-diff/java-tmp-vars-inc/old/Test.java

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
public class Test {
2+
public int f00(int x) {
3+
int y = x;
4+
return y;
5+
}
6+
7+
public int f01(int z) {
8+
int w = z++;
9+
return w;
10+
}
11+
}

‎regression/goto-diff/java-tmp-vars-inc/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
new.jar
3+
old.jar
4+
// Enable multi-line checking
5+
activate-multi-line-match
6+
EXIT=0
7+
SIGNAL=0
8+
new functions:\nmodified functions:\n Test\.java: java::Test\.f00:\(I\)I\ndeleted functions:
9+
--
10+
^warning: ignoring

‎regression/goto-diff/java-tmp-vars-new/new.jar

1.26 KB
Binary file not shown.

‎regression/goto-diff/java-tmp-vars-new/new/Test.java

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
class B {
2+
void foo() {}
3+
}
4+
5+
class A {
6+
B b = new B();
7+
}
8+
9+
public class Test {
10+
public A f00(A x) {
11+
return org.cprover.CProver.nondetWithoutNull();
12+
}
13+
14+
public A f01(A z) {
15+
return org.cprover.CProver.nondetWithoutNull();
16+
}
17+
}

‎regression/goto-diff/java-tmp-vars-new/old.jar

1.26 KB
Binary file not shown.

‎regression/goto-diff/java-tmp-vars-new/old/Test.java

+17
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
class B {
2+
void foo() {}
3+
}
4+
5+
class A {
6+
B b = new B();
7+
}
8+
9+
public class Test {
10+
public A f00(A x) {
11+
return x;
12+
}
13+
14+
public A f01(A z) {
15+
return org.cprover.CProver.nondetWithoutNull();
16+
}
17+
}

‎regression/goto-diff/java-tmp-vars-new/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
new.jar
3+
old.jar
4+
// Enable multi-line checking
5+
activate-multi-line-match
6+
EXIT=0
7+
SIGNAL=0
8+
new functions:\nmodified functions:\n Test\.java: java::Test\.f00:\(LA;\)LA;\ndeleted functions:
9+
--
10+
^warning: ignoring

‎regression/goto-diff/java-tmp-vars-string/new.jar

752 Bytes
Binary file not shown.

‎regression/goto-diff/java-tmp-vars-string/new/Test.java

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
public class Test {
2+
public String f00(String x) {
3+
String y = x + "abc";
4+
return y;
5+
}
6+
7+
public String f01(String z) {
8+
String w = z + "abc";
9+
return w;
10+
}
11+
}

‎regression/goto-diff/java-tmp-vars-string/old.jar

757 Bytes
Binary file not shown.

‎regression/goto-diff/java-tmp-vars-string/old/Test.java

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
public class Test {
2+
public String f00(String x) {
3+
String y = x;
4+
return y;
5+
}
6+
7+
public String f01(String z) {
8+
String w = z + "abc";
9+
return w;
10+
}
11+
}

‎regression/goto-diff/java-tmp-vars-string/test.desc

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
new.jar
3+
old.jar
4+
// Enable multi-line checking
5+
activate-multi-line-match
6+
EXIT=0
7+
SIGNAL=0
8+
new functions:\nmodified functions:\n Test\.java: java::Test\.f00:\(Ljava/lang/String;\)Ljava/lang/String;\ndeleted functions:
9+
--
10+
^warning: ignoring

‎src/ansi-c/c_nondet_symbol_factory.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -43,8 +43,8 @@ static const symbolt &c_new_tmp_symbol(
4343
const bool static_lifetime,
4444
const std::string &prefix="tmp")
4545
{
46-
symbolt &tmp_symbol=
47-
get_fresh_aux_symbol(type, "", prefix, loc, ID_C, symbol_table);
46+
symbolt &tmp_symbol = get_fresh_aux_symbol(
47+
type, id2string(loc.get_function()), prefix, loc, ID_C, symbol_table);
4848
tmp_symbol.is_static_lifetime=static_lifetime;
4949

5050
return tmp_symbol;

‎src/goto-instrument/code_contracts.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -250,7 +250,7 @@ const symbolt &code_contractst::new_tmp_symbol(
250250
{
251251
return get_fresh_aux_symbol(
252252
type,
253-
"",
253+
id2string(source_location.get_function()),
254254
"tmp_cc",
255255
source_location,
256256
irep_idt(),

‎src/goto-programs/convert_nondet.cpp

+6-1
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Author: Reuben Thomas, [email protected]
1717
#include <java_bytecode/java_object_factory.h> // gen_nondet_init
1818

1919
#include <util/irep_ids.h>
20+
#include <util/fresh_symbol.h>
2021

2122
#include <memory>
2223

@@ -135,11 +136,13 @@ void convert_nondet(
135136
message_handlert &message_handler,
136137
const object_factory_parameterst &object_factory_parameters)
137138
{
139+
object_factory_parameterst parameters = object_factory_parameters;
140+
parameters.function_id = function.get_function_id();
138141
convert_nondet(
139142
function.get_goto_function().body,
140143
function.get_symbol_table(),
141144
message_handler,
142-
object_factory_parameters);
145+
parameters);
143146

144147
function.compute_location_numbers();
145148
}
@@ -158,6 +161,8 @@ void convert_nondet(
158161

159162
if(symbol.mode==ID_java)
160163
{
164+
object_factory_parameterst parameters = object_factory_parameters;
165+
parameters.function_id = f_it.first;
161166
convert_nondet(
162167
f_it.second.body,
163168
symbol_table,

‎src/goto-programs/goto_convert_class.h

-2
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,6 @@ class goto_convertt:public messaget
3434
messaget(_message_handler),
3535
symbol_table(_symbol_table),
3636
ns(_symbol_table),
37-
temporary_counter(0),
3837
tmp_symbol_prefix("goto_convertt")
3938
{
4039
}
@@ -46,7 +45,6 @@ class goto_convertt:public messaget
4645
protected:
4746
symbol_table_baset &symbol_table;
4847
namespacet ns;
49-
unsigned temporary_counter;
5048
std::string tmp_symbol_prefix;
5149

5250
void goto_convert_rec(const codet &code, goto_programt &dest);

‎src/goto-programs/goto_convert_functions.cpp

-2
Original file line numberDiff line numberDiff line change
@@ -147,8 +147,6 @@ void goto_convert_functionst::convert_function(
147147

148148
// make tmp variables local to function
149149
tmp_symbol_prefix=id2string(symbol.name)+"::$tmp::";
150-
temporary_counter=0;
151-
reset_temporary_counter();
152150

153151
f.type=to_code_type(symbol.type);
154152

‎src/goto-programs/goto_convert_side_effect.cpp

+6-3
Original file line numberDiff line numberDiff line change
@@ -379,14 +379,15 @@ void goto_convertt::remove_function_call(
379379

380380
new_base_name+='_';
381381
new_base_name+=id2string(symbol.base_name);
382-
new_base_name+="$"+std::to_string(++temporary_counter);
382+
new_base_name += "$0";
383383

384384
new_symbol.base_name=new_base_name;
385385
new_symbol.mode=symbol.mode;
386386
}
387387

388388
new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
389389

390+
// ensure that the name is unique
390391
new_name(new_symbol);
391392

392393
{
@@ -429,10 +430,11 @@ void goto_convertt::remove_cpp_new(
429430

430431
auxiliary_symbolt new_symbol;
431432

432-
new_symbol.base_name="new_ptr$"+std::to_string(++temporary_counter);
433+
new_symbol.base_name = "new_ptr$0";
433434
new_symbol.type=expr.type();
434435
new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
435436

437+
// ensure that the name is unique
436438
new_name(new_symbol);
437439

438440
code_declt decl;
@@ -480,11 +482,12 @@ void goto_convertt::remove_malloc(
480482
{
481483
auxiliary_symbolt new_symbol;
482484

483-
new_symbol.base_name="malloc_value$"+std::to_string(++temporary_counter);
485+
new_symbol.base_name = "malloc_value$0";
484486
new_symbol.type=expr.type();
485487
new_symbol.name=tmp_symbol_prefix+id2string(new_symbol.base_name);
486488
new_symbol.location=expr.source_location();
487489

490+
// ensure that the name is unique
488491
new_name(new_symbol);
489492

490493
code_declt decl;

‎src/goto-programs/remove_function_pointers.cpp

+7-8
Original file line numberDiff line numberDiff line change
@@ -233,14 +233,13 @@ void remove_function_pointerst::fix_return_type(
233233
code_type.return_type(), ns))
234234
return;
235235

236-
symbolt &tmp_symbol=
237-
get_fresh_aux_symbol(
238-
code_type.return_type(),
239-
"remove_function_pointers",
240-
"tmp_return_val",
241-
function_call.source_location(),
242-
irep_idt(),
243-
symbol_table);
236+
symbolt &tmp_symbol = get_fresh_aux_symbol(
237+
code_type.return_type(),
238+
id2string(function_call.source_location().get_function()),
239+
"tmp_return_val",
240+
function_call.source_location(),
241+
irep_idt(),
242+
symbol_table);
244243

245244
symbol_exprt tmp_symbol_expr;
246245
tmp_symbol_expr.type()=tmp_symbol.type;

‎src/goto-programs/remove_instanceof.cpp

+7-8
Original file line numberDiff line numberDiff line change
@@ -106,14 +106,13 @@ std::size_t remove_instanceoft::lower_instanceof(
106106
symbol_typet jlo=to_symbol_type(java_lang_object_type().subtype());
107107
exprt object_clsid=get_class_identifier_field(check_ptr, jlo, ns);
108108

109-
symbolt &newsym=
110-
get_fresh_aux_symbol(
111-
object_clsid.type(),
112-
"instanceof_tmp",
113-
"instanceof_tmp",
114-
source_locationt(),
115-
ID_java,
116-
symbol_table);
109+
symbolt &newsym = get_fresh_aux_symbol(
110+
object_clsid.type(),
111+
id2string(this_inst->function),
112+
"instanceof_tmp",
113+
source_locationt(),
114+
ID_java,
115+
symbol_table);
117116

118117
auto newinst=goto_program.insert_after(this_inst);
119118
newinst->make_assignment();

0 commit comments

Comments
 (0)