Skip to content

Commit 5740e77

Browse files
haoNoQhaoNoQ
committed
[analyzer] exploded-graph-rewriter: Implement a --diff mode.
In this mode the tool would avoid duplicating the contents of the program state on every node, replacing them with a diff-like dump of changes that happened on that node. This is useful because most of the time we only interested in whether the effect of the statement was modeled correctly. A diffed graph would also be much faster to load and navigate, being much smaller than the original graph. The diffs are computed "semantically" as opposed to plain text diffs. I.e., the diff algorithm is hand-crafted separately for every state trait, taking the underlying data structures into account. This is especially nice for Environment because textual diffs would have been terrible. On the other hand, it requires some boilerplate to implement. Differential Revision: https://reviews.llvm.org/D62761 llvm-svn: 363898
1 parent b50d167 commit 5740e77

File tree

5 files changed

+411
-62
lines changed

5 files changed

+411
-62
lines changed

‎clang/test/Analysis/exploded-graph-rewriter/environment_diff.dot‎

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
// RUN: %exploded_graph_rewriter -d %s | FileCheck %s
2+
3+
// FIXME: Substitution doesn't seem to work on Windows.
4+
// UNSUPPORTED: system-windows
5+
6+
// No diffs on the first node, nothing to check.
7+
Node0x1 [shape=record,label=
8+
"{
9+
{ "node_id": 1,
10+
"pointer": "0x1",
11+
"state_id": 2,
12+
"program_points": [],
13+
"program_state": {
14+
"store": null,
15+
"environment": [
16+
{
17+
"location_context": "#0 Call",
18+
"lctx_id": 3,
19+
"calling": "foo",
20+
"call_line": 4,
21+
"items": [
22+
{
23+
"stmt_id": 5,
24+
"pretty": "bar()",
25+
"value": "Unknown"
26+
}
27+
]
28+
}
29+
]
30+
}
31+
}
32+
\l}"];
33+
34+
Node0x1 -> Node0x6;
35+
36+
// CHECK: Node0x6 [
37+
// CHECK-SAME: <tr>
38+
// CHECK-SAME: <td><font color="red">-</font></td>
39+
// CHECK-SAME: <td align="left"><i>S5</i></td>
40+
// CHECK-SAME: <td align="left">bar()</td>
41+
// CHECK-SAME: <td align="left">Unknown</td>
42+
// CHECK-SAME: </tr>
43+
// CHECK-SAME: <tr>
44+
// CHECK-SAME: <td><font color="forestgreen">+</font></td>
45+
// CHECK-SAME: <td align="left"><i>S9</i></td>
46+
// CHECK-SAME: <td align="left">baz()</td>
47+
// CHECK-SAME: <td align="left">Undefined</td>
48+
// CHECK-SAME: </tr>
49+
Node0x6 [shape=record,label=
50+
"{
51+
{ "node_id": 6,
52+
"pointer": "0x6",
53+
"state_id": 7,
54+
"program_points": [],
55+
"program_state": {
56+
"store": null,
57+
"environment": [
58+
{
59+
"location_context": "#0 Call",
60+
"lctx_id": 3,
61+
"calling": "foo",
62+
"call_line": 4,
63+
"items": [
64+
{
65+
"stmt_id": 9,
66+
"pretty": "baz()",
67+
"value": "Undefined"
68+
}
69+
]
70+
}
71+
]
72+
}
73+
}
74+
\l}"];
75+
76+
Node0x6 -> Node0x9;
77+
// Make sure that the last node in the path is not diffed.
78+
// CHECK: Node0x9 [
79+
// CHECK-SAME: <tr>
80+
// CHECK-SAME: <td></td>
81+
// CHECK-SAME: <td align="left"><i>S9</i></td>
82+
// CHECK-SAME: <td align="left">baz()</td>
83+
// CHECK-SAME: <td align="left">Undefined</td>
84+
// CHECK-SAME: </tr>
85+
Node0x9 [shape=record,label=
86+
"{
87+
{ "node_id": 9,
88+
"pointer": "0x9",
89+
"state_id": 7,
90+
"program_points": [],
91+
"program_state": {
92+
"store": null,
93+
"environment": [
94+
{
95+
"location_context": "#0 Call",
96+
"lctx_id": 3,
97+
"calling": "foo",
98+
"call_line": 4,
99+
"items": [
100+
{
101+
"stmt_id": 9,
102+
"pretty": "baz()",
103+
"value": "Undefined"
104+
}
105+
]
106+
}
107+
]
108+
}
109+
}
110+
\l}"];

‎clang/test/Analysis/exploded-graph-rewriter/program_points.dot‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,6 @@
77
// CHECK-SAME: <table border="0" align="left" width="0">
88
// CHECK-SAME: <tr>
99
// CHECK-SAME: <td width="0">
10-
// CHECK-SAME: -
1110
// CHECK-SAME: </td>
1211
// CHECK-SAME: <td align="left" width="0">
1312
// CHECK-SAME: <font color="gold3">Edge</font>

‎clang/test/Analysis/exploded-graph-rewriter/store.dot‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@ Node0x1 [shape=record,label=
3131
"store": [
3232
{
3333
"cluster": "x",
34+
"pointer": "0x3",
3435
"items": [
3536
{
3637
"kind": "Default",

‎clang/test/Analysis/exploded-graph-rewriter/store_diff.dot‎

Lines changed: 82 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,82 @@
1+
// RUN: %exploded_graph_rewriter -d %s | FileCheck %s
2+
3+
// FIXME: Substitution doesn't seem to work on Windows.
4+
// UNSUPPORTED: system-windows
5+
6+
Node0x1 [shape=record,label=
7+
"{
8+
{ "node_id": 1,
9+
"pointer": "0x1",
10+
"state_id": 2,
11+
"program_points": [],
12+
"program_state": {
13+
"environment": null,
14+
"store": [
15+
{
16+
"cluster": "x",
17+
"pointer": "0x3",
18+
"items": [
19+
{
20+
"kind": "Default",
21+
"offset": 0,
22+
"value": "Undefined"
23+
}
24+
]
25+
}
26+
]
27+
}
28+
}
29+
\l}"];
30+
31+
Node0x1 -> Node0x4;
32+
33+
// CHECK: Node0x4 [
34+
// CHECK-SAME: <tr>
35+
// CHECK-SAME: <td><font color="red">-</font></td>
36+
// CHECK-SAME: <td align="left">x</td><td align="left">0</td>
37+
// CHECK-SAME: <td align="left">(<i>Default</i>)</td>
38+
// CHECK-SAME: <td align="left">Undefined</td>
39+
// CHECK-SAME: </tr>
40+
// CHECK-SAME: <tr>
41+
// CHECK-SAME: <td><font color="forestgreen">+</font></td>
42+
// CHECK-SAME: <td align="left">x</td>
43+
// CHECK-SAME: <td align="left">0</td>
44+
// CHECK-SAME: <td align="left">(<i>Default</i>)</td>
45+
// CHECK-SAME: <td align="left">Unknown</td>
46+
// CHECK-SAME: </tr>
47+
Node0x4 [shape=record,label=
48+
"{
49+
{ "node_id": 4,
50+
"pointer": "0x4",
51+
"state_id": 5,
52+
"program_points": [],
53+
"program_state": {
54+
"environment": null,
55+
"store": [
56+
{
57+
"cluster": "x",
58+
"pointer": "0x3",
59+
"items": [
60+
{
61+
"kind": "Default",
62+
"offset": 0,
63+
"value": "Unknown"
64+
}
65+
]
66+
}
67+
]
68+
}
69+
}
70+
\l}"];
71+
72+
Node0x4 -> Node0x6;
73+
74+
Node0x6 [shape=record,label=
75+
"{
76+
{ "node_id": 6,
77+
"pointer": "0x6",
78+
"state_id": 7,
79+
"program_points": [],
80+
"program_state": null
81+
}
82+
\l}"];

0 commit comments

Comments
 (0)