martong updated this revision to Diff 356751.
martong added a comment.
Herald added a reviewer: Szelethus.
- Rebase on top of the newest version of the dependent patch
- Draw borders for the table of the disequality info
- Add tests
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D104917/new/
https://reviews.llvm.org/D104917
Files:
clang/test/Analysis/exploded-graph-rewriter/checker_messages.dot
clang/test/Analysis/exploded-graph-rewriter/checker_messages_diff.dot
clang/test/Analysis/exploded-graph-rewriter/constraints.dot
clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot
clang/test/Analysis/exploded-graph-rewriter/disequality_info.dot
clang/test/Analysis/exploded-graph-rewriter/disequality_info_diff.dot
clang/test/Analysis/exploded-graph-rewriter/environment.dot
clang/test/Analysis/exploded-graph-rewriter/environment_diff.dot
clang/test/Analysis/exploded-graph-rewriter/equivalence_classes.dot
clang/test/Analysis/exploded-graph-rewriter/equivalence_classes_diff.dot
clang/test/Analysis/exploded-graph-rewriter/store.dot
clang/test/Analysis/exploded-graph-rewriter/store_diff.dot
clang/test/Analysis/exploded-graph-rewriter/topology.dot
clang/utils/analyzer/exploded-graph-rewriter.py
Index: clang/utils/analyzer/exploded-graph-rewriter.py
===================================================================
--- clang/utils/analyzer/exploded-graph-rewriter.py
+++ clang/utils/analyzer/exploded-graph-rewriter.py
@@ -267,6 +267,8 @@
'store': None,
'environment': None,
'constraints': None,
+ 'equivalence_classes': None,
+ 'disequality_info': None,
'dynamic_types': None,
'constructing_objects': None,
'checker_messages': None
@@ -285,6 +287,43 @@
(c['symbol'], c['range']) for c in json_ps['constraints']
]) if json_ps['constraints'] is not None else None
+ # Each equivalence_class is represented as List[Str].
+ # json_ps['equivalence_classes']: List[List[Str]]
+ # Sort by the first element of each equivalence_class.
+ eq_classes = (
+ json_ps['equivalence_classes']
+ if json_ps['equivalence_classes']
+ else None
+ )
+ self.equivalence_classes = (
+ GenericMap({i: ", ".join(eq_classes[i]) for i in range(0, len(eq_classes))})
+ if eq_classes
+ else None
+ )
+
+ # Each equivalence_class is represented as List[Str].
+ # Disequality info is a mapping from an equivalence class to many
+ # equivalence classes:
+ # json_ps['disequality_info']: Dict[List[Str], List[List[Str]]]
+ def get_diseq_classes(classes):
+ """ Flatten List[List[Str]] to Str """
+ return (
+ "<table border='1'><tr><td>"
+ + "</td></tr><tr><td>".join([", ".join(cl) for cl in classes])
+ + "</td></tr></table>"
+ )
+
+ self.disequality_info = (
+ GenericMap(
+ {
+ ", ".join(c["class"]): get_diseq_classes(c["disequal_to"])
+ for c in json_ps["disequality_info"]
+ }
+ )
+ if json_ps["disequality_info"]
+ else None
+ )
+
self.dynamic_types = GenericMap([
(t['region'], '%s%s' % (t['dyn_type'],
' (or a sub-class)'
@@ -682,8 +721,8 @@
self.visit_store(st)
self._dump('</td></tr>')
- def visit_generic_map(self, m, prev_m=None):
- self._dump('<table border="0">')
+ def visit_generic_map(self, m, prev_m=None, border=0):
+ self._dump('<table border="%s">' % (border))
def dump_pair(m, k, is_added=None):
self._dump('<tr><td>%s</td>'
@@ -704,7 +743,7 @@
self._dump('</table>')
- def visit_generic_map_in_state(self, selector, title, s, prev_s=None):
+ def visit_generic_map_in_state(self, selector, title, s, prev_s=None, border=0):
m = getattr(s, selector)
prev_m = getattr(prev_s, selector) if prev_s is not None else None
if m is None and prev_m is None:
@@ -719,12 +758,12 @@
if prev_m is not None:
if m.is_different(prev_m):
self._dump('</td></tr><tr><td align="left">')
- self.visit_generic_map(m, prev_m)
+ self.visit_generic_map(m, prev_m, border)
else:
self._dump('<i> No changes!</i>')
else:
self._dump('</td></tr><tr><td align="left">')
- self.visit_generic_map(m)
+ self.visit_generic_map(m, prev_m=None, border=border)
self._dump('</td></tr>')
@@ -791,6 +830,12 @@
s, prev_s)
self.visit_generic_map_in_state('constraints', 'Ranges',
s, prev_s)
+ self.visit_generic_map_in_state('equivalence_classes',
+ 'Equivalence Classes',
+ s, prev_s)
+ self.visit_generic_map_in_state('disequality_info',
+ 'Disequality Info',
+ s, prev_s, border=1)
self.visit_generic_map_in_state('dynamic_types', 'Dynamic Types',
s, prev_s)
self.visit_environment_in_state('constructing_objects',
Index: clang/test/Analysis/exploded-graph-rewriter/topology.dot
===================================================================
--- clang/test/Analysis/exploded-graph-rewriter/topology.dot
+++ clang/test/Analysis/exploded-graph-rewriter/topology.dot
@@ -22,6 +22,8 @@
"program_state": {
"environment": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": [
Index: clang/test/Analysis/exploded-graph-rewriter/store_diff.dot
===================================================================
--- clang/test/Analysis/exploded-graph-rewriter/store_diff.dot
+++ clang/test/Analysis/exploded-graph-rewriter/store_diff.dot
@@ -18,6 +18,8 @@
"program_state": {
"environment": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": null,
@@ -72,6 +74,8 @@
"program_state": {
"environment": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": null,
Index: clang/test/Analysis/exploded-graph-rewriter/store.dot
===================================================================
--- clang/test/Analysis/exploded-graph-rewriter/store.dot
+++ clang/test/Analysis/exploded-graph-rewriter/store.dot
@@ -32,6 +32,8 @@
"program_state": {
"environment": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": null,
Index: clang/test/Analysis/exploded-graph-rewriter/equivalence_classes_diff.dot
===================================================================
--- clang/test/Analysis/exploded-graph-rewriter/equivalence_classes_diff.dot
+++ clang/test/Analysis/exploded-graph-rewriter/equivalence_classes_diff.dot
@@ -18,9 +18,12 @@
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": null,
- "constraints": [
- { "symbol": "reg_$0<x>", "range": "{ [0, 10] }" }
- ]
+ "constraints": null,
+ "equivalence_classes": [
+ [ "reg_$0<int a>", "reg_$1<int b>" ],
+ [ "reg_$2<int c>", "reg_$3<int d>" ]
+ ],
+ "disequality_info": null
}
}
\l}"];
@@ -29,14 +32,34 @@
// CHECK: Node0x3 [
// CHECK-SAME: <tr>
-// CHECK-SAME: <td><font color="red">-</font></td>
-// CHECK-SAME: <td align="left">reg_$0<x></td>
-// CHECK-SAME: <td align="left">\{ [0, 10] \}</td>
+// CHECK-SAME: <td><font color="red">-</font></td>
+// CHECK-SAME: <td align="left">0</td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: reg_$0
+// CHECK-SAME: <int a>
+// CHECK-SAME: , reg_$1
+// CHECK-SAME: <int b>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td><font color="red">-</font></td>
+// CHECK-SAME: <td align="left">1</td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: reg_$2
+// CHECK-SAME: <int c>
+// CHECK-SAME: , reg_$3
+// CHECK-SAME: <int d>
+// CHECK-SAME: </td>
// CHECK-SAME: </tr>
// CHECK-SAME: <tr>
-// CHECK-SAME: <td><font color="forestgreen">+</font></td>
-// CHECK-SAME: <td align="left">reg_$0<x></td>
-// CHECK-SAME: <td align="left">\{ [0, 5] \}</td>
+// CHECK-SAME: <td><font color="forestgreen">+</font></td>
+// CHECK-SAME: <td align="left">0</td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: reg_$2
+// CHECK-SAME: <int e>
+// CHECK-SAME: , reg_$3
+// CHECK-SAME: <int f>
+// CHECK-SAME: </td>
// CHECK-SAME: </tr>
Node0x3 [shape=record,label=
"{
@@ -56,9 +79,11 @@
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": null,
- "constraints": [
- { "symbol": "reg_$0<x>", "range": "{ [0, 5] }" }
- ]
+ "constraints": null,
+ "equivalence_classes": [
+ [ "reg_$2<int e>", "reg_$3<int f>" ]
+ ],
+ "disequality_info": null
}
}
\l}"];
@@ -81,6 +106,8 @@
"store": null,
"environment": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": null
Index: clang/test/Analysis/exploded-graph-rewriter/equivalence_classes.dot
===================================================================
--- /dev/null
+++ clang/test/Analysis/exploded-graph-rewriter/equivalence_classes.dot
@@ -0,0 +1,53 @@
+// RUN: %exploded_graph_rewriter %s | FileCheck %s
+
+// CHECK: <tr>
+// CHECK-SAME: <td align="left"><b>Equivalence Classes: </b></td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: <table border="0">
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td></td>
+// CHECK-SAME: <td align="left">0</td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: reg_$0<int a>, reg_$1<int b>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td></td>
+// CHECK-SAME: <td align="left">1</td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: reg_$2<int c>, reg_$3<int d>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: </table>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+
+Node0x1 [shape=record,label=
+ "{
+ {
+ "state_id": 2,
+ "program_points": [
+ {
+ "kind": "BlockEntrance", "block_id": 1,
+ "terminator": null, "term_kind": null,
+ "tag": null, "node_id": 1,
+ "has_report": 0, "is_sink": 0
+ }
+ ],
+ "program_state": {
+ "store": null,
+ "environment": null,
+ "dynamic_types": null,
+ "constructing_objects": null,
+ "checker_messages": null,
+ "constraints": null,
+ "equivalence_classes": [
+ [ "reg_$0<int a>", "reg_$1<int b>" ],
+ [ "reg_$2<int c>", "reg_$3<int d>" ]
+ ],
+ "disequality_info": null
+ }
+ }
+\l}"];
Index: clang/test/Analysis/exploded-graph-rewriter/environment_diff.dot
===================================================================
--- clang/test/Analysis/exploded-graph-rewriter/environment_diff.dot
+++ clang/test/Analysis/exploded-graph-rewriter/environment_diff.dot
@@ -16,6 +16,8 @@
"program_state": {
"store": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": null,
@@ -71,6 +73,8 @@
"program_state": {
"store": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": null,
@@ -120,6 +124,8 @@
"program_state": {
"store": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": null,
Index: clang/test/Analysis/exploded-graph-rewriter/environment.dot
===================================================================
--- clang/test/Analysis/exploded-graph-rewriter/environment.dot
+++ clang/test/Analysis/exploded-graph-rewriter/environment.dot
@@ -44,6 +44,8 @@
"program_state": {
"store": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": null,
Index: clang/test/Analysis/exploded-graph-rewriter/disequality_info_diff.dot
===================================================================
--- /dev/null
+++ clang/test/Analysis/exploded-graph-rewriter/disequality_info_diff.dot
@@ -0,0 +1,138 @@
+// RUN: %exploded_graph_rewriter -d %s | FileCheck %s
+
+Node0x1 [shape=record,label=
+ "{
+ {
+ "state_id": 2,
+ "program_points": [
+ {
+ "kind": "BlockEntrance", "block_id": 1,
+ "terminator": null, "term_kind": null,
+ "tag": null, "node_id": 1,
+ "has_report": 0, "is_sink": 0
+ }
+ ],
+ "program_state": {
+ "store": null,
+ "environment": null,
+ "dynamic_types": null,
+ "constructing_objects": null,
+ "checker_messages": null,
+ "constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": [
+ {
+ "class": [ "reg_$0<int a>" ],
+ "disequal_to": [
+ [ "(reg_$1<int b>) - 2" ],
+ [ "reg_$2<int c>" ]]
+ },
+ {
+ "class": [ "reg_$4<int d>" ],
+ "disequal_to": [
+ [ "reg_$5<int e>" ]]
+ }
+ ]
+ }
+ }
+\l}"];
+
+Node0x1 -> Node0x3;
+
+
+// CHECK: Node0x3 [
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td><font color="red">-</font></td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: reg_$4
+// CHECK-SAME: <int d>
+// CHECK-SAME: </td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: <table border='1'>
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td>
+// CHECK-SAME: reg_$5<int e>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: </table>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td><font color="forestgreen">+</font></td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: reg_$4
+// CHECK-SAME: <int d>
+// CHECK-SAME: </td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: <table border='1'>
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td>
+// CHECK-SAME: reg_$6<int f>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: </table>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+Node0x3 [shape=record,label=
+ "{
+ {
+ "state_id": 4,
+ "program_points": [
+ {
+ "kind": "BlockEntrance", "block_id": 1,
+ "terminator": null, "term_kind": null,
+ "tag": null, "node_id": 1,
+ "has_report": 0, "is_sink": 0
+ }
+ ],
+ "program_state": {
+ "store": null,
+ "environment": null,
+ "dynamic_types": null,
+ "constructing_objects": null,
+ "checker_messages": null,
+ "constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": [
+ {
+ "class": [ "reg_$0<int a>" ],
+ "disequal_to": [
+ [ "(reg_$1<int b>) - 2" ],
+ [ "reg_$2<int c>" ]]
+ },
+ {
+ "class": [ "reg_$4<int d>" ],
+ "disequal_to": [
+ [ "reg_$6<int f>" ]]
+ }
+ ]
+ }
+ }
+\l}"];
+
+Node0x3 -> Node0x5;
+
+Node0x5 [shape=record,label=
+ "{
+ {
+ "state_id": 6,
+ "program_points": [
+ {
+ "kind": "BlockEntrance", "block_id": 1,
+ "terminator": null, "term_kind": null,
+ "tag": null, "node_id": 1,
+ "has_report": 0, "is_sink": 0
+ }
+ ],
+ "program_state": {
+ "store": null,
+ "environment": null,
+ "constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
+ "dynamic_types": null,
+ "constructing_objects": null,
+ "checker_messages": null
+ }
+ }
+\l}"];
Index: clang/test/Analysis/exploded-graph-rewriter/disequality_info.dot
===================================================================
--- /dev/null
+++ clang/test/Analysis/exploded-graph-rewriter/disequality_info.dot
@@ -0,0 +1,83 @@
+// RUN: %exploded_graph_rewriter %s | FileCheck %s
+
+// CHECK: <tr>
+// CHECK-SAME: <td align="left"><b>Disequality Info: </b></td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: <table border="1">
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td></td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: reg_$0<int a>
+// CHECK-SAME: </td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: <table border='1'>
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td>
+// CHECK-SAME: (reg_$1<int b>) - 2
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td>
+// CHECK-SAME: reg_$2<int c>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: </table>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td></td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: reg_$4<int d>
+// CHECK-SAME: </td>
+// CHECK-SAME: <td align="left">
+// CHECK-SAME: <table border='1'>
+// CHECK-SAME: <tr>
+// CHECK-SAME: <td>
+// CHECK-SAME: reg_$5<int e>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: </table>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+// CHECK-SAME: </table>
+// CHECK-SAME: </td>
+// CHECK-SAME: </tr>
+
+Node0x1 [shape=record,label=
+ "{
+ {
+ "state_id": 2,
+ "program_points": [
+ {
+ "kind": "BlockEntrance", "block_id": 1,
+ "terminator": null, "term_kind": null,
+ "tag": null, "node_id": 1,
+ "has_report": 0, "is_sink": 0
+ }
+ ],
+ "program_state": {
+ "store": null,
+ "environment": null,
+ "dynamic_types": null,
+ "constructing_objects": null,
+ "checker_messages": null,
+ "constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": [
+ {
+ "class": [ "reg_$0<int a>" ],
+ "disequal_to": [
+ [ "(reg_$1<int b>) - 2" ],
+ [ "reg_$2<int c>" ]]
+ },
+ {
+ "class": [ "reg_$4<int d>" ],
+ "disequal_to": [
+ [ "reg_$5<int e>" ]]
+ }
+ ]
+ }
+ }
+\l}"];
Index: clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot
===================================================================
--- clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot
+++ clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot
@@ -20,7 +20,9 @@
"checker_messages": null,
"constraints": [
{ "symbol": "reg_$0<x>", "range": "{ [0, 10] }" }
- ]
+ ],
+ "equivalence_classes": null,
+ "disequality_info": null
}
}
\l}"];
@@ -58,7 +60,9 @@
"checker_messages": null,
"constraints": [
{ "symbol": "reg_$0<x>", "range": "{ [0, 5] }" }
- ]
+ ],
+ "equivalence_classes": null,
+ "disequality_info": null
}
}
\l}"];
@@ -81,6 +85,8 @@
"store": null,
"environment": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": null
Index: clang/test/Analysis/exploded-graph-rewriter/constraints.dot
===================================================================
--- clang/test/Analysis/exploded-graph-rewriter/constraints.dot
+++ clang/test/Analysis/exploded-graph-rewriter/constraints.dot
@@ -27,7 +27,9 @@
"checker_messages": null,
"constraints": [
{ "symbol": "reg_$0<x>", "range": "{ [0, 0] }" }
- ]
+ ],
+ "equivalence_classes": null,
+ "disequality_info": null
}
}
\l}"];
Index: clang/test/Analysis/exploded-graph-rewriter/checker_messages_diff.dot
===================================================================
--- clang/test/Analysis/exploded-graph-rewriter/checker_messages_diff.dot
+++ clang/test/Analysis/exploded-graph-rewriter/checker_messages_diff.dot
@@ -15,6 +15,10 @@
"environment": null,
"store": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": [
@@ -73,6 +77,8 @@
"environment": null,
"store": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"checker_messages": [
Index: clang/test/Analysis/exploded-graph-rewriter/checker_messages.dot
===================================================================
--- clang/test/Analysis/exploded-graph-rewriter/checker_messages.dot
+++ clang/test/Analysis/exploded-graph-rewriter/checker_messages.dot
@@ -22,6 +22,8 @@
"program_state": {
"store": null,
"constraints": null,
+ "equivalence_classes": null,
+ "disequality_info": null,
"dynamic_types": null,
"constructing_objects": null,
"environment": null,
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
