Skip to content

Commit e6a922c

Browse files
smowtonsmowton
authored
Merge pull request diffblue#415 from diffblue/CBMC_merge_2018-05-15
Cbmc merge 2018-05-15
2 parents 023d0ce + 384992c commit e6a922c

File tree

17 files changed

+304
-41
lines changed

17 files changed

+304
-41
lines changed

‎cbmc/regression/cbmc-java/phi-merge_uninitialized_values/PhiMergeUninitialized.class

1.46 KB
Binary file not shown.

‎cbmc/regression/cbmc-java/phi-merge_uninitialized_values/PhiMergeUninitialized.java

+54
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
public class PhiMergeUninitialized {
2+
3+
public int dynamicAllocationUninitialized(Boolean trigger) {
4+
5+
Ephemeral obj;
6+
if (trigger) {
7+
obj = new Ephemeral(42);
8+
} else {
9+
obj = new Aetherial(20);
10+
}
11+
12+
assert obj.val == 20;
13+
return obj.val;
14+
}
15+
16+
private Ephemeral field;
17+
18+
public int fieldUninitialized(Boolean trigger) {
19+
if (trigger) {
20+
field = new Ephemeral(42);
21+
}
22+
23+
assert field.val == 42;
24+
return field.val;
25+
}
26+
27+
private static Ephemeral staticField;
28+
29+
public int staticFieldUninitialized(Boolean trigger) {
30+
if (trigger) {
31+
staticField = new Ephemeral(42);
32+
} else {
33+
staticField = new Aetherial(76);
34+
}
35+
36+
assert staticField.val == 76;
37+
return staticField.val;
38+
}
39+
40+
class Ephemeral {
41+
Ephemeral(int value) {
42+
val = value;
43+
}
44+
45+
int val;
46+
}
47+
48+
class Aetherial extends Ephemeral {
49+
Aetherial(int value) {
50+
super(value);
51+
}
52+
}
53+
}
54+

‎cbmc/regression/cbmc-java/phi-merge_uninitialized_values/field.desc

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
PhiMergeUninitialized.class
3+
--function PhiMergeUninitialized.fieldUninitialized --show-vcc
4+
activate-multi-line-match
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^.*:\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\)
9+
^.*\?\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\s+:
10+
--
11+
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12+
statement:
13+
14+
(guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
15+
16+
Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

‎cbmc/regression/cbmc-java/phi-merge_uninitialized_values/local.desc

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
PhiMergeUninitialized.class
3+
--function PhiMergeUninitialized.dynamicAllocationUninitialized --show-vcc
4+
activate-multi-line-match
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^.*:\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\)
9+
^.*\?\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\s+:
10+
--
11+
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12+
statement:
13+
14+
(guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
15+
16+
Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

‎cbmc/regression/cbmc-java/phi-merge_uninitialized_values/static_field.desc

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
PhiMergeUninitialized.class
3+
--function PhiMergeUninitialized.staticFieldUninitialized --show-vcc
4+
activate-multi-line-match
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^.*:\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\)
9+
^.*\?\s+(dynamic_object|new_tmp)[0-9]+(@[0-9]+)?#0\s+:
10+
--
11+
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12+
statement:
13+
14+
(guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
15+
16+
Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

‎cbmc/regression/cbmc/phi-merge_uninitialized_values/dynamic.desc

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
test.c
3+
--function dynamicAllocationUninitialized --show-vcc
4+
activate-multi-line-match
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^.*:\s+dynamic_object[0-9]+(@[0-9]+)?#0\)
9+
^.*\?\s+dynamic_object[0-9]+(@[0-9]+)?#0\s+:
10+
--
11+
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12+
statement:
13+
14+
(guard ? dynamic_object2@3#1 : dynamic_object3@3#0)
15+
16+
Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

‎cbmc/regression/cbmc/phi-merge_uninitialized_values/global.desc

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
test.c
3+
--function globalUninitialized --show-vcc
4+
activate-multi-line-match
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^.*:\s+global(@[0-9]+)?#0\)
9+
^.*\?\s+global(@[0-9]+)?#0\s+:
10+
--
11+
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12+
statement:
13+
14+
(guard ? global#1 : global#0)
15+
16+
Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

‎cbmc/regression/cbmc/phi-merge_uninitialized_values/local.desc

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
test.c
3+
--function localUninitialized --show-vcc
4+
activate-multi-line-match
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^.*:\s+local(@[0-9]+)?#0\)
9+
^.*\?\s+local(@[0-9]+)?#0\s+:
10+
--
11+
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12+
statement:
13+
14+
(guard ? local#1 : local#0)
15+
16+
Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

‎cbmc/regression/cbmc/phi-merge_uninitialized_values/static_local.desc

+16
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
test.c
3+
--function staticLocalUninitialized --show-vcc
4+
activate-multi-line-match
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^.*:\s+staticLocal(@[0-9]+)?#0\)
9+
^.*\?\s+staticLocal(@[0-9]+)?#0\s+:
10+
--
11+
These regexes are making sure that a variable of generation 0 dosen't appear in a phi merge, so the below
12+
statement:
13+
14+
(guard ? staticLocal#1 : dynamic_object#0)
15+
16+
Should not appear. First regex deals with when the gen zero is the latter position, second when it's in the former.

‎cbmc/regression/cbmc/phi-merge_uninitialized_values/test.c

+56
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,56 @@
1+
#include <assert.h>
2+
#include <stdlib.h>
3+
4+
void dynamicAllocationUninitialized(int trigger)
5+
{
6+
int *obj;
7+
if(trigger)
8+
{
9+
obj = (int *)malloc(sizeof(int));
10+
*obj = 42;
11+
}
12+
else
13+
{
14+
obj = (int *)malloc(sizeof(int));
15+
*obj = 76;
16+
}
17+
18+
assert(*obj == 42);
19+
}
20+
21+
int global;
22+
void globalUninitialized(int trigger)
23+
{
24+
if(trigger)
25+
{
26+
global = 44;
27+
}
28+
else
29+
{
30+
global = 20;
31+
}
32+
33+
assert(global == 44);
34+
}
35+
36+
void staticLocalUninitialized(int trigger)
37+
{
38+
static int staticLocal;
39+
if(trigger)
40+
{
41+
staticLocal = 43;
42+
}
43+
44+
assert(staticLocal == 43);
45+
}
46+
47+
void localUninitialized(int trigger)
48+
{
49+
int local;
50+
if(trigger)
51+
{
52+
local = 24;
53+
}
54+
55+
assert(local == 24);
56+
}

‎cbmc/regression/test.pl

+1-1
Original file line numberDiff line numberDiff line change
@@ -174,7 +174,7 @@ ($$$$$$$$$)
174174
binmode $fh;
175175
my $whole_file = <$fh>;
176176
$whole_file =~ s/\r\n/\n/g;
177-
my $is_match = $whole_file =~ /$result/;
177+
my $is_match = $whole_file =~ /$result/m;
178178
$r = ($included ? !$is_match : $is_match);
179179
}
180180
else

‎cbmc/scripts/glucose-syrup-patch

+30
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,36 @@ diff -rupNw glucose-syrup/core/SolverTypes.h glucose-syrup-patched/core/SolverTy
4343

4444
friend class ClauseAllocator;
4545

46+
diff -rupNw glucose-syrup/mtl/Clone.h glucose-syrup-patched/mtl/Clone.h
47+
--- glucose-syrup/mtl/Clone.h 2014-10-03 11:10:22.000000000 +0200
48+
+++ glucose-syrup-patched/mtl/Clone.h 2018-05-10 12:35:25.150491249 +0200
49+
@@ -8,6 +8,6 @@ namespace Glucose {
50+
public:
51+
virtual Clone* clone() const = 0;
52+
};
53+
-};
54+
+}
55+
56+
#endif
57+
\ No newline at end of file
58+
diff -rupNw glucose-syrup/mtl/Clone.h~ glucose-syrup-patched/mtl/Clone.h~
59+
--- glucose-syrup/mtl/Clone.h~ 1970-01-01 01:00:00.000000000 +0100
60+
+++ glucose-syrup-patched/mtl/Clone.h~ 2018-04-21 16:58:22.950005391 +0200
61+
@@ -0,0 +1,13 @@
62+
+#ifndef Glucose_Clone_h
63+
+#define Glucose_Clone_h
64+
+
65+
+
66+
+namespace Glucose {
67+
+
68+
+ class Clone {
69+
+ public:
70+
+ virtual Clone* clone() const = 0;
71+
+ };
72+
+};
73+
+
74+
+#endif
75+
\ No newline at end of file
4676
diff -rupNw glucose-syrup/mtl/IntTypes.h glucose-syrup-patched/mtl/IntTypes.h
4777
--- glucose-syrup/mtl/IntTypes.h 2014-10-03 11:10:22.000000000 +0200
4878
+++ glucose-syrup-patched/mtl/IntTypes.h 2018-04-21 16:58:22.950005391 +0200

‎cbmc/src/goto-programs/goto_trace.cpp

+23-38
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ Author: Daniel Kroening
1717
#include <ostream>
1818

1919
#include <util/arith_tools.h>
20+
#include <util/format_expr.h>
2021
#include <util/symbol.h>
2122

2223
#include <ansi-c/printf_formatter.h>
@@ -61,61 +62,45 @@ void goto_trace_stept::output(
6162
UNREACHABLE;
6263
}
6364

64-
if(type==typet::ASSERT || type==typet::ASSUME || type==typet::GOTO)
65+
if(is_assert() || is_assume() || is_goto())
6566
out << " (" << cond_value << ")";
67+
else if(is_function_call() || is_function_return())
68+
out << ' ' << identifier;
6669

6770
if(hidden)
6871
out << " hidden";
6972

70-
out << "\n";
73+
out << '\n';
74+
75+
if(is_assignment())
76+
{
77+
out << " " << format(full_lhs)
78+
<< " = " << format(full_lhs_value)
79+
<< '\n';
80+
}
7181

7282
if(!pc->source_location.is_nil())
73-
out << pc->source_location << "\n";
74-
75-
if(pc->is_goto())
76-
out << "GOTO ";
77-
else if(pc->is_assume())
78-
out << "ASSUME ";
79-
else if(pc->is_assert())
80-
out << "ASSERT ";
81-
else if(pc->is_dead())
82-
out << "DEAD ";
83-
else if(pc->is_other())
84-
out << "OTHER ";
85-
else if(pc->is_assign())
86-
out << "ASSIGN ";
87-
else if(pc->is_decl())
88-
out << "DECL ";
89-
else if(pc->is_function_call())
90-
out << "CALL ";
91-
else
92-
out << "(?) ";
83+
out << pc->source_location << '\n';
9384

94-
out << "\n";
85+
out << pc->type << '\n';
9586

96-
if((pc->is_other() && lhs_object.is_not_nil()) || pc->is_assign())
97-
{
98-
irep_idt identifier=lhs_object.get_object_name();
99-
out << " " << from_expr(ns, identifier, lhs_object.get_original_expr())
100-
<< " = " << from_expr(ns, identifier, lhs_object_value)
101-
<< "\n";
102-
}
103-
else if(pc->is_assert())
87+
if(pc->is_assert())
10488
{
10589
if(!cond_value)
10690
{
107-
out << "Violated property:" << "\n";
91+
out << "Violated property:" << '\n';
10892
if(pc->source_location.is_nil())
109-
out << " " << pc->source_location << "\n";
93+
out << " " << pc->source_location << '\n';
11094

111-
if(comment!="")
112-
out << " " << comment << "\n";
113-
out << " " << from_expr(ns, pc->function, pc->guard) << "\n";
114-
out << "\n";
95+
if(!comment.empty())
96+
out << " " << comment << '\n';
97+
98+
out << " " << format(pc->guard) << '\n';
99+
out << '\n';
115100
}
116101
}
117102

118-
out << "\n";
103+
out << '\n';
119104
}
120105

121106
std::string trace_value_binary(

‎cbmc/src/goto-symex/goto_symex.cpp

+8-2
Original file line numberDiff line numberDiff line change
@@ -22,13 +22,19 @@ void goto_symext::do_simplify(exprt &expr)
2222
simplify(expr, ns);
2323
}
2424

25+
nondet_symbol_exprt goto_symext::build_symex_nondet(typet &type)
26+
{
27+
irep_idt identifier = "symex::nondet" + std::to_string(nondet_count++);
28+
nondet_symbol_exprt new_expr(identifier, type);
29+
return new_expr;
30+
}
31+
2532
void goto_symext::replace_nondet(exprt &expr)
2633
{
2734
if(expr.id()==ID_side_effect &&
2835
expr.get(ID_statement)==ID_nondet)
2936
{
30-
irep_idt identifier="symex::nondet"+std::to_string(nondet_count++);
31-
nondet_symbol_exprt new_expr(identifier, expr.type());
37+
nondet_symbol_exprt new_expr = build_symex_nondet(expr.type());
3238
new_expr.add_source_location()=expr.source_location();
3339
expr.swap(new_expr);
3440
}

0 commit comments

Comments
 (0)