[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

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@363898 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 82 insertions, 0 deletions

diff --git a/test/Analysis/exploded-graph-rewriter/store_diff.dot b/test/Analysis/exploded-graph-rewriter/store_diff.dot
new file mode 100644
index 0000000000..47ea9af014
--- /dev/null
+++ b/test/Analysis/exploded-graph-rewriter/store_diff.dot
@@ -0,0 +1,82 @@
+// RUN: %exploded_graph_rewriter -d %s | FileCheck %s
+
+// FIXME: Substitution doesn't seem to work on Windows.
+// UNSUPPORTED: system-windows
+
+Node0x1 [shape=record,label=
+ "{
+    { "node_id": 1,
+      "pointer": "0x1",
+      "state_id": 2,
+      "program_points": [],
+      "program_state": {
+        "environment": null,
+        "store": [
+          {
+            "cluster": "x",
+            "pointer": "0x3",
+            "items": [
+              {
+                "kind": "Default",
+                "offset": 0,
+                "value": "Undefined"
+              }
+            ]
+          }
+        ]
+      }
+    }
+\l}"];
+
+Node0x1 -> Node0x4;
+
+// CHECK: Node0x4 [
+// CHECK-SAME: <tr>
+// CHECK-SAME:   <td><font color="red">-</font></td>
+// CHECK-SAME:   <td align="left">x</td><td align="left">0</td>
+// CHECK-SAME:   <td align="left">(<i>Default</i>)</td>
+// CHECK-SAME:   <td align="left">Undefined</td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: <tr>
+// CHECK-SAME:   <td><font color="forestgreen">+</font></td>
+// CHECK-SAME:   <td align="left">x</td>
+// CHECK-SAME:   <td align="left">0</td>
+// CHECK-SAME:   <td align="left">(<i>Default</i>)</td>
+// CHECK-SAME:   <td align="left">Unknown</td>
+// CHECK-SAME: </tr>
+Node0x4 [shape=record,label=
+ "{
+    { "node_id": 4,
+      "pointer": "0x4",
+      "state_id": 5,
+      "program_points": [],
+      "program_state": {
+        "environment": null,
+        "store": [
+          {
+            "cluster": "x",
+            "pointer": "0x3",
+            "items": [
+              {
+                "kind": "Default",
+                "offset": 0,
+                "value": "Unknown"
+              }
+            ]
+          }
+        ]
+      }
+    }
+\l}"];
+
+Node0x4 -> Node0x6;
+
+Node0x6 [shape=record,label=
+ "{
+    { "node_id": 6,
+      "pointer": "0x6",
+      "state_id": 7,
+      "program_points": [],
+      "program_state": null
+    }
+\l}"];