Skip to content

Commit

Permalink
[analyzer] exploded-graph-rewriter: Add support for range constraints.
Browse files Browse the repository at this point in the history
Diff support included.

A cheap solution is implemented that treats range constraints as
"some sort of key-value map", so it's going to be trivial
to add support for other such maps later, such as dynamic type info.

Differential Revision: https://reviews.llvm.org/D63685

llvm-svn: 364268
haoNoQ committed Jun 25, 2019
1 parent b9c94f9 commit beb85ad
Showing 7 changed files with 162 additions and 2 deletions.
27 changes: 27 additions & 0 deletions clang/test/Analysis/exploded-graph-rewriter/constraints.dot
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
// RUN: %exploded_graph_rewriter %s | FileCheck %s

// FIXME: Substitution doesn't seem to work on Windows.
// UNSUPPORTED: system-windows

// CHECK: <tr><td align="left"><b>Ranges: </b></td></tr>
// CHECK-SAME: <tr><td align="left"><table border="0">
// CHECK-SAME: <tr>
// CHECK-SAME: <td align="left">reg_$0<x></td>
// CHECK-SAME: <td align="left">\{ [0, 0] \}</td>
// CHECK-SAME: </tr>
// CHECK-SAME: </table></td></tr>
Node0x1 [shape=record,label=
"{
{ "node_id": 1,
"pointer": "0x1",
"state_id": 2,
"program_points": [],
"program_state": {
"store": null,
"environment": null,
"constraints": [
{ "symbol": "reg_$0<x>", "range": "{ [0, 0] }" }
]
}
}
\l}"];
65 changes: 65 additions & 0 deletions clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot
Original file line number Diff line number Diff line change
@@ -0,0 +1,65 @@
// 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": {
"store": null,
"environment": null,
"constraints": [
{ "symbol": "reg_$0<x>", "range": "{ [0, 10] }" }
]
}
}
\l}"];

Node0x1 -> Node0x3;

// 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: </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: </tr>
Node0x3 [shape=record,label=
"{
{ "node_id": 3,
"pointer": "0x3",
"state_id": 4,
"program_points": [],
"program_state": {
"store": null,
"environment": null,
"constraints": [
{ "symbol": "reg_$0<x>", "range": "{ [0, 5] }" }
]
}
}
\l}"];

Node0x3 -> Node0x5;

Node0x5 [shape=record,label=
"{
{ "node_id": 5,
"pointer": "0x5",
"state_id": 6,
"program_points": [],
"program_state": {
"store": null,
"environment": null,
"constraints": null
}
}
\l}"];
Original file line number Diff line number Diff line change
@@ -33,6 +33,7 @@ Node0x1 [shape=record,label=
"program_points": [],
"program_state": {
"store": null,
"constraints": null,
"environment": [
{
"location_context": "#0 Call",
Original file line number Diff line number Diff line change
@@ -12,6 +12,7 @@ Node0x1 [shape=record,label=
"program_points": [],
"program_state": {
"store": null,
"constraints": null,
"environment": [
{
"location_context": "#0 Call",
@@ -54,6 +55,7 @@ Node0x6 [shape=record,label=
"program_points": [],
"program_state": {
"store": null,
"constraints": null,
"environment": [
{
"location_context": "#0 Call",
@@ -90,6 +92,7 @@ Node0x9 [shape=record,label=
"program_points": [],
"program_state": {
"store": null,
"constraints": null,
"environment": [
{
"location_context": "#0 Call",
1 change: 1 addition & 0 deletions clang/test/Analysis/exploded-graph-rewriter/store.dot
Original file line number Diff line number Diff line change
@@ -28,6 +28,7 @@ Node0x1 [shape=record,label=
"program_points": [],
"program_state": {
"environment": null,
"constraints": null,
"store": [
{
"cluster": "x",
2 changes: 2 additions & 0 deletions clang/test/Analysis/exploded-graph-rewriter/store_diff.dot
Original file line number Diff line number Diff line change
@@ -11,6 +11,7 @@ Node0x1 [shape=record,label=
"program_points": [],
"program_state": {
"environment": null,
"constraints": null,
"store": [
{
"cluster": "x",
@@ -52,6 +53,7 @@ Node0x4 [shape=record,label=
"program_points": [],
"program_state": {
"environment": null,
"constraints": null,
"store": [
{
"cluster": "x",
65 changes: 63 additions & 2 deletions clang/utils/analyzer/exploded-graph-rewriter.py
Original file line number Diff line number Diff line change
@@ -25,6 +25,19 @@ def diff_dicts(curr, prev):
return (removed, added)


# Represents any program state trait that is a dictionary of key-value pairs.
class GenericMap(object):
def __init__(self, generic_map):
self.generic_map = generic_map

def diff(self, prev):
return diff_dicts(self.generic_map, prev.generic_map)

def is_different(self, prev):
removed, added = self.diff(prev)
return len(removed) != 0 or len(added) != 0


# A deserialized source location.
class SourceLocation(object):
def __init__(self, json_loc):
@@ -203,8 +216,10 @@ def __init__(self, state_id, json_ps):
if json_ps['store'] is not None else None
self.environment = Environment(json_ps['environment']) \
if json_ps['environment'] is not None else None
self.constraints = GenericMap(collections.OrderedDict([
(c['symbol'], c['range']) for c in json_ps['constraints']
])) if json_ps['constraints'] is not None else None
# TODO: Objects under construction.
# TODO: Constraint ranges.
# TODO: Dynamic types of objects.
# TODO: Checker messages.

@@ -479,11 +494,57 @@ def visit_store_in_state(self, s, prev_s=None):
else:
self._dump('</td></tr><tr><td align="left">')
self.visit_store(s.store)
self._dump('</td></tr><hr />')
self._dump('</td></tr>')

def visit_generic_map(self, m, prev_m=None):
self._dump('<table border="0">')

def dump_pair(m, k, is_added=None):
self._dump('<tr><td>%s</td>'
'<td align="left">%s</td>'
'<td align="left">%s</td></tr>'
% (self._diff_plus_minus(is_added),
k, m.generic_map[k]))

if prev_m is not None:
removed, added = m.diff(prev_m)
for k in removed:
dump_pair(prev_m, k, False)
for k in added:
dump_pair(m, k, True)
else:
for k in m.generic_map:
dump_pair(m, k, None)

self._dump('</table>')

def visit_generic_map_in_state(self, selector, s, prev_s=None):
self._dump('<tr><td align="left">'
'<b>Ranges: </b>')
m = getattr(s, selector)
if m is None:
self._dump('<i> Nothing!</i>')
else:
prev_m = None
if prev_s is not None:
prev_m = getattr(prev_s, selector)
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)
else:
self._dump('<i> No changes!</i>')
if prev_m is None:
self._dump('</td></tr><tr><td align="left">')
self.visit_generic_map(m)
self._dump('</td></tr>')

def visit_state(self, s, prev_s):
self.visit_store_in_state(s, prev_s)
self._dump('<hr />')
self.visit_environment_in_state(s, prev_s)
self._dump('<hr />')
self.visit_generic_map_in_state('constraints', s, prev_s)

def visit_node(self, node):
self._dump('%s [shape=record,label=<<table border="0">'

0 comments on commit beb85ad

Please sign in to comment.