This is an archive of the discontinued LLVM Phabricator instance.

Differential D104917

[Analyzer] Extend exploded-graph-rewriter to support eq and diseq classes
Needs ReviewPublic

Authored by martong on Jun 25 2021, 7:26 AM.

Details

Reviewers
steakhal
vsavchenko
NoQ
Szelethus

Diff Detail

Unit TestsFailed

TimeTest
160 msx64 debian > Clang.Analysis/exploded-graph-rewriter::dynamic_types.cpp
120 msx64 debian > Clang.Analysis/exploded-graph-rewriter::escapes.c
140 msx64 debian > Clang.Analysis/exploded-graph-rewriter::initializers_under_construction.cpp
160 msx64 debian > Clang.Analysis/exploded-graph-rewriter::l_name_starts_with_l.cpp
140 msx64 debian > Clang.Analysis/exploded-graph-rewriter::macros.c
View Full Test Results (13 Failed)

Event Timeline

martong created this revision.Jun 25 2021, 7:26 AM
Herald added subscribers: manas, ASDenysPetrov, gamesh411 and 10 others. · View Herald TranscriptJun 25 2021, 7:26 AM
martong requested review of this revision.Jun 25 2021, 7:26 AM
Herald added a project: Restricted Project. · View Herald TranscriptJun 25 2021, 7:26 AM
Herald added a subscriber: cfe-commits. · View Herald Transcript
martong mentioned this in D103967: [Analyzer][solver] Add dump methods for (dis)equality classes..Jun 25 2021, 7:28 AM
martong added a parent revision: D103967: [Analyzer][solver] Add dump methods for (dis)equality classes..
vsavchenko added a comment.Jun 25 2021, 7:37 AM

LGTM, but I'm not really an expert in exploded-graph-rewriter. I think @NoQ should take a look.

clang/utils/analyzer/exploded-graph-rewriter.py
299

I believe that enumerate is more idiomatic for Python in situations like this.

Harbormaster completed remote builds in B110996: Diff 354493.Jun 25 2021, 8:09 AM
NoQ added a comment.Jun 28 2021, 11:29 AM

Yay, great, thanks!

Can you add a test as well? We have a few in test/Analysis/exploded-graph-rewriter/ where we test parts of the emitted html.

Do you happen to have a screenshot of how it looks?

NoQ added a comment.Jun 28 2021, 12:51 PM

We have a few in test/Analysis/exploded-graph-rewriter/ where we test parts of the emitted html.

And they're now failing on the pre-merge buildbots. So i guess updating existing tests would already be nice.

martong updated this revision to Diff 356751.Jul 6 2021, 9:12 AM
  • Rebase on top of the newest version of the dependent patch
  • Draw borders for the table of the disequality info
  • Add tests
Herald added a reviewer: Szelethus. · View Herald TranscriptJul 6 2021, 9:12 AM
martong added a comment.Jul 6 2021, 9:14 AM
In D104917#2845181, @NoQ wrote:

We have a few in test/Analysis/exploded-graph-rewriter/ where we test parts of the emitted html.

And they're now failing on the pre-merge buildbots. So i guess updating existing tests would already be nice.

Yeah, just updated the tests. Plus I added some new tests for the Eq/DisEq info.

martong added a comment.Jul 6 2021, 9:20 AM

Do you happen to have a screenshot of how it looks?

Yes! :)


I've added borders to the tables in the Disequality Info section, because the default rendering makes it hard to notice if there are multiple disequivalent classes attached to one class (see the second pics).

Harbormaster completed remote builds in B112637: Diff 356751.Jul 6 2021, 9:57 AM
NoQ added a comment.Jul 6 2021, 5:24 PM

WDYT about the following format:

Equality constraints:
reg_$0<a> == reg_$1<b>
          == reg_$2<c>

Disequality constraints:
reg_$0<a> != reg_$3<d>,
          != reg_$4<e>

Comma is a bit hard to notice but otherwise kinda nicely readable?

martong added a comment.Jul 14 2021, 8:07 AM
In D104917#2860923, @NoQ wrote:

WDYT about the following format:

Equality constraints:
reg_$0<a> == reg_$1<b>
          == reg_$2<c>

Disequality constraints:
reg_$0<a> != reg_$3<d>,
          != reg_$4<e>

Comma is a bit hard to notice but otherwise kinda nicely readable?

IMHO this format would be confusing if you have two SVals that include comparison operators:
E.g. SVal1 (reg_$1<int b>) == (reg_$2<int c>) and SVal2 (reg_$0<int a>) != 42. They might be in the same equivalence class, that would result this format:

Equality constraints:
(reg_$1<int b>) == (reg_$2<int c>) == (reg_$0<int a>) != 42

Well, ... I know the current table with the borders looks a bit rough and ugly, but I think the information is displayed in an obvious way and can be interpreted unambiguously.

NoQ added a comment.Jul 14 2021, 10:01 AM

We could color the special ==/!= 50% gray and/or replace it with a non-programming symbol such as ≃ and ≄.

Revision Contents

PathSize
clang/
test/
Analysis/
exploded-graph-rewriter/
2 lines
6 lines
4 lines
10 lines
83 lines
138 lines
2 lines
6 lines
53 lines
equivalence_classes_diff.dot
constraints_diff.dot
51 lines
2 lines
4 lines
2 lines
utils/
analyzer/
55 lines

Diff 356751

clang/test/Analysis/exploded-graph-rewriter/checker_messages.dot

Show All 16 Lines "{
"terminator": null, "term_kind": null, "terminator": null, "term_kind": null,
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"store": null, "store": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"environment": null, "environment": null,
"checker_messages": [ "checker_messages": [
{ "checker": "alpha.core.FooChecker", "messages": [ { "checker": "alpha.core.FooChecker", "messages": [
"Foo stuff:", "Foo stuff:",
"Foo: Bar" "Foo: Bar"
]} ]}
] ]
} }
} }
\l}"]; \l}"];

clang/test/Analysis/exploded-graph-rewriter/checker_messages_diff.dot

Show All 9 Lines "{
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"environment": null, "environment": null,
"store": null, "store": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": [ "checker_messages": [
{ "checker": "FooChecker", "messages": [ { "checker": "FooChecker", "messages": [
"Foo: Bar" "Foo: Bar"
]}, ]},
{ "checker": "BarChecker", "messages": [ { "checker": "BarChecker", "messages": [
"Bar: Foo" "Bar: Foo"
▲ Show 20 Lines • Show All 42 Lines • ▼ Show 20 Lines "{
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"environment": null, "environment": null,
"store": null, "store": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": [ "checker_messages": [
{ "checker": "FooChecker", "messages": [ { "checker": "FooChecker", "messages": [
"Foo: Bar", "Foo: Bar",
"Bar: Foo" "Bar: Foo"
]}, ]},
{ "checker": "DunnoWhateverSomeOtherChecker", "messages": [ { "checker": "DunnoWhateverSomeOtherChecker", "messages": [
Show All 23 Lines

clang/test/Analysis/exploded-graph-rewriter/constraints.dot

Show All 21 Lines "{
"program_state": { "program_state": {
"store": null, "store": null,
"environment": null, "environment": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null, "checker_messages": null,
"constraints": [ "constraints": [
{ "symbol": "reg_$0<x>", "range": "{ [0, 0] }" } { "symbol": "reg_$0<x>", "range": "{ [0, 0] }" }
] ],
"equivalence_classes": null,
"disequality_info": null
} }
} }
\l}"]; \l}"];

clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot

  • This file was copied to clang/test/Analysis/exploded-graph-rewriter/equivalence_classes_diff.dot.
Show All 14 Lines "{
"program_state": { "program_state": {
"store": null, "store": null,
"environment": null, "environment": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null, "checker_messages": null,
"constraints": [ "constraints": [
{ "symbol": "reg_$0<x>", "range": "{ [0, 10] }" } { "symbol": "reg_$0<x>", "range": "{ [0, 10] }" }
] ],
"equivalence_classes": null,
"disequality_info": null
} }
} }
\l}"]; \l}"];
Node0x1 -> Node0x3; Node0x1 -> Node0x3;
// CHECK: Node0x3 [ // CHECK: Node0x3 [
// CHECK-SAME: <tr> // CHECK-SAME: <tr>
Show All 21 Lines "{
"program_state": { "program_state": {
"store": null, "store": null,
"environment": null, "environment": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null, "checker_messages": null,
"constraints": [ "constraints": [
{ "symbol": "reg_$0<x>", "range": "{ [0, 5] }" } { "symbol": "reg_$0<x>", "range": "{ [0, 5] }" }
] ],
"equivalence_classes": null,
"disequality_info": null
} }
} }
\l}"]; \l}"];
Node0x3 -> Node0x5; Node0x3 -> Node0x5;
Node0x5 [shape=record,label= Node0x5 [shape=record,label=
"{ "{
{ {
"state_id": 6, "state_id": 6,
"program_points": [ "program_points": [
{ {
"kind": "BlockEntrance", "block_id": 1, "kind": "BlockEntrance", "block_id": 1,
"terminator": null, "term_kind": null, "terminator": null, "term_kind": null,
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"store": null, "store": null,
"environment": null, "environment": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null "checker_messages": null
} }
} }
\l}"]; \l}"];

clang/test/Analysis/exploded-graph-rewriter/disequality_info.dot

  • This file was added.
// 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}"];

clang/test/Analysis/exploded-graph-rewriter/disequality_info_diff.dot

  • This file was added.
// 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}"];

clang/test/Analysis/exploded-graph-rewriter/environment.dot

Show All 38 Lines "{
"terminator": null, "term_kind": null, "terminator": null, "term_kind": null,
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"store": null, "store": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null, "checker_messages": null,
"environment": { "environment": {
"pointer": "0x2", "pointer": "0x2",
"items": [ "items": [
{ {
"location_context": "#0 Call", "location_context": "#0 Call",
Show All 25 Lines

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

Show All 10 Lines "{
"terminator": null, "term_kind": null, "terminator": null, "term_kind": null,
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"store": null, "store": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null, "checker_messages": null,
"environment": { "environment": {
"pointer": "0x2", "pointer": "0x2",
"items": [ "items": [
{ {
"location_context": "#0 Call", "location_context": "#0 Call",
Show All 39 Lines "{
"terminator": null, "term_kind": null, "terminator": null, "term_kind": null,
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"store": null, "store": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null, "checker_messages": null,
"environment": { "environment": {
"pointer": "0x2", "pointer": "0x2",
"items": [ "items": [
{ {
"location_context": "#0 Call", "location_context": "#0 Call",
Show All 33 Lines "{
"terminator": null, "term_kind": null, "terminator": null, "term_kind": null,
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"store": null, "store": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null, "checker_messages": null,
"environment": { "environment": {
"pointer": "0x2", "pointer": "0x2",
"items": [ "items": [
{ {
"location_context": "#0 Call", "location_context": "#0 Call",
Show All 16 Lines

clang/test/Analysis/exploded-graph-rewriter/equivalence_classes.dot

  • This file was added.
// 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}"];

clang/test/Analysis/exploded-graph-rewriter/equivalence_classes_diff.dot

  • This file was copied from clang/test/Analysis/exploded-graph-rewriter/constraints_diff.dot.
Show All 12 Lines "{
} }
], ],
"program_state": { "program_state": {
"store": null, "store": null,
"environment": null, "environment": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null, "checker_messages": null,
"constraints": [ "constraints": null,
{ "symbol": "reg_$0<x>", "range": "{ [0, 10] }" } "equivalence_classes": [
] [ "reg_$0<int a>", "reg_$1<int b>" ],
[ "reg_$2<int c>", "reg_$3<int d>" ]
],
"disequality_info": null
} }
} }
\l}"]; \l}"];
Node0x1 -> Node0x3; Node0x1 -> Node0x3;
// CHECK: Node0x3 [ // CHECK: Node0x3 [
// CHECK-SAME: <tr> // CHECK-SAME: <tr>
// CHECK-SAME: <td><font color="red">-</font></td> // CHECK-SAME: <td><font color="red">-</font></td>
// CHECK-SAME: <td align="left">reg_$0<x></td> // CHECK-SAME: <td align="left">0</td>
// CHECK-SAME: <td align="left">\{ [0, 10] \}</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: <tr> // CHECK-SAME: <tr>
// CHECK-SAME: <td><font color="forestgreen">+</font></td> // CHECK-SAME: <td><font color="forestgreen">+</font></td>
// CHECK-SAME: <td align="left">reg_$0<x></td> // CHECK-SAME: <td align="left">0</td>
// CHECK-SAME: <td align="left">\{ [0, 5] \}</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> // CHECK-SAME: </tr>
Node0x3 [shape=record,label= Node0x3 [shape=record,label=
"{ "{
{ {
"state_id": 4, "state_id": 4,
"program_points": [ "program_points": [
{ {
"kind": "BlockEntrance", "block_id": 1, "kind": "BlockEntrance", "block_id": 1,
"terminator": null, "term_kind": null, "terminator": null, "term_kind": null,
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"store": null, "store": null,
"environment": null, "environment": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null, "checker_messages": null,
"constraints": [ "constraints": null,
{ "symbol": "reg_$0<x>", "range": "{ [0, 5] }" } "equivalence_classes": [
] [ "reg_$2<int e>", "reg_$3<int f>" ]
],
"disequality_info": null
} }
} }
\l}"]; \l}"];
Node0x3 -> Node0x5; Node0x3 -> Node0x5;
Node0x5 [shape=record,label= Node0x5 [shape=record,label=
"{ "{
{ {
"state_id": 6, "state_id": 6,
"program_points": [ "program_points": [
{ {
"kind": "BlockEntrance", "block_id": 1, "kind": "BlockEntrance", "block_id": 1,
"terminator": null, "term_kind": null, "terminator": null, "term_kind": null,
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"store": null, "store": null,
"environment": null, "environment": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null "checker_messages": null
} }
} }
\l}"]; \l}"];

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

Show All 26 Lines "{
"terminator": null, "term_kind": null, "terminator": null, "term_kind": null,
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"environment": null, "environment": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null, "checker_messages": null,
"store": { "store": {
"pointer": "0x2", "pointer": "0x2",
"items": [ "items": [
{ {
"cluster": "x", "cluster": "x",
Show All 14 Lines

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

Show All 12 Lines "{
"terminator": null, "term_kind": null, "terminator": null, "term_kind": null,
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"environment": null, "environment": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null, "checker_messages": null,
"store": { "store": {
"pointer": "0x2", "pointer": "0x2",
"items": [ "items": [
{ {
"cluster": "x", "cluster": "x",
Show All 38 Lines "{
"terminator": null, "term_kind": null, "terminator": null, "term_kind": null,
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"environment": null, "environment": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": null, "checker_messages": null,
"store": { "store": {
"pointer": "0x5", "pointer": "0x5",
"items": [ "items": [
{ {
"cluster": "x", "cluster": "x",
Show All 32 Lines

clang/test/Analysis/exploded-graph-rewriter/topology.dot

Show All 16 Lines "{
"terminator": null, "term_kind": null, "terminator": null, "term_kind": null,
"tag": null, "node_id": 1, "tag": null, "node_id": 1,
"has_report": 0, "is_sink": 0 "has_report": 0, "is_sink": 0
} }
], ],
"program_state": { "program_state": {
"environment": null, "environment": null,
"constraints": null, "constraints": null,
"equivalence_classes": null,
"disequality_info": null,
"dynamic_types": null, "dynamic_types": null,
"constructing_objects": null, "constructing_objects": null,
"checker_messages": [ "checker_messages": [
{ "checker": "foo", "messages": ["bar"] } { "checker": "foo", "messages": ["bar"] }
], ],
"store": null "store": null
} }
} }
\l}"]; \l}"];

clang/utils/analyzer/exploded-graph-rewriter.py

Show First 20 Lines • Show All 261 Lines • ▼ Show 20 Linesclass ProgramState:
def __init__(self, state_id, json_ps): def __init__(self, state_id, json_ps):
logging.debug('Adding ProgramState ' + str(state_id)) logging.debug('Adding ProgramState ' + str(state_id))
if json_ps is None: if json_ps is None:
json_ps = { json_ps = {
'store': None, 'store': None,
'environment': None, 'environment': None,
'constraints': None, 'constraints': None,
'equivalence_classes': None,
'disequality_info': None,
'dynamic_types': None, 'dynamic_types': None,
'constructing_objects': None, 'constructing_objects': None,
'checker_messages': None 'checker_messages': None
} }
self.state_id = state_id self.state_id = state_id
self.store = Store(json_ps['store']) \ self.store = Store(json_ps['store']) \
if json_ps['store'] is not None else None if json_ps['store'] is not None else None
self.environment = \ self.environment = \
GenericEnvironment(json_ps['environment']['items']) \ GenericEnvironment(json_ps['environment']['items']) \
if json_ps['environment'] is not None else None if json_ps['environment'] is not None else None
self.constraints = GenericMap([ self.constraints = GenericMap([
(c['symbol'], c['range']) for c in json_ps['constraints'] (c['symbol'], c['range']) for c in json_ps['constraints']
]) if json_ps['constraints'] is not None else None ]) 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))})
vsavchenkoUnsubmitted
Not Done
ReplyInline Actions

I believe that enumerate is more idiomatic for Python in situations like this.

vsavchenko: I believe that `enumerate` is more idiomatic for Python in situations like this.
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([ self.dynamic_types = GenericMap([
(t['region'], '%s%s' % (t['dyn_type'], (t['region'], '%s%s' % (t['dyn_type'],
' (or a sub-class)' ' (or a sub-class)'
if t['sub_classable'] else '')) if t['sub_classable'] else ''))
for t in json_ps['dynamic_types']]) \ for t in json_ps['dynamic_types']]) \
if json_ps['dynamic_types'] is not None else None if json_ps['dynamic_types'] is not None else None
self.constructing_objects = \ self.constructing_objects = \
▲ Show 20 Lines • Show All 381 Lines • ▼ Show 20 Lines def visit_store_in_state(self, s, prev_s=None):
self.visit_store(st, prev_st) self.visit_store(st, prev_st)
else: else:
self._dump('<i> No changes!</i>') self._dump('<i> No changes!</i>')
else: else:
self._dump('</td></tr><tr><td align="left">') self._dump('</td></tr><tr><td align="left">')
self.visit_store(st) self.visit_store(st)
self._dump('</td></tr>') self._dump('</td></tr>')
def visit_generic_map(self, m, prev_m=None): def visit_generic_map(self, m, prev_m=None, border=0):
self._dump('<table border="0">') self._dump('<table border="%s">' % (border))
def dump_pair(m, k, is_added=None): def dump_pair(m, k, is_added=None):
self._dump('<tr><td>%s</td>' self._dump('<tr><td>%s</td>'
'<td align="left">%s</td>' '<td align="left">%s</td>'
'<td align="left">%s</td></tr>' '<td align="left">%s</td></tr>'
% (self._diff_plus_minus(is_added), % (self._diff_plus_minus(is_added),
k, m.generic_map[k])) k, m.generic_map[k]))
if prev_m is not None: if prev_m is not None:
removed, added = m.diff(prev_m) removed, added = m.diff(prev_m)
for k in removed: for k in removed:
dump_pair(prev_m, k, False) dump_pair(prev_m, k, False)
for k in added: for k in added:
dump_pair(m, k, True) dump_pair(m, k, True)
else: else:
for k in m.generic_map: for k in m.generic_map:
dump_pair(m, k, None) dump_pair(m, k, None)
self._dump('</table>') 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) m = getattr(s, selector)
prev_m = getattr(prev_s, selector) if prev_s is not None else None prev_m = getattr(prev_s, selector) if prev_s is not None else None
if m is None and prev_m is None: if m is None and prev_m is None:
return return
self._dump('<hr />') self._dump('<hr />')
self._dump('<tr><td align="left">' self._dump('<tr><td align="left">'
'<b>%s: </b>' % title) '<b>%s: </b>' % title)
if m is None: if m is None:
self._dump('<i> Nothing!</i>') self._dump('<i> Nothing!</i>')
else: else:
if prev_m is not None: if prev_m is not None:
if m.is_different(prev_m): if m.is_different(prev_m):
self._dump('</td></tr><tr><td align="left">') self._dump('</td></tr><tr><td align="left">')
self.visit_generic_map(m, prev_m) self.visit_generic_map(m, prev_m, border)
else: else:
self._dump('<i> No changes!</i>') self._dump('<i> No changes!</i>')
else: else:
self._dump('</td></tr><tr><td align="left">') 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>') self._dump('</td></tr>')
def visit_checker_messages(self, m, prev_m=None): def visit_checker_messages(self, m, prev_m=None):
self._dump('<table border="0">') self._dump('<table border="0">')
def dump_line(l, is_added=None): def dump_line(l, is_added=None):
self._dump('<tr><td>%s</td>' self._dump('<tr><td>%s</td>'
▲ Show 20 Lines • Show All 50 Lines • ▼ Show 20 Lines def visit_checker_messages_in_state(self, s, prev_s=None):
self._dump('</td></tr>') self._dump('</td></tr>')
def visit_state(self, s, prev_s): def visit_state(self, s, prev_s):
self.visit_store_in_state(s, prev_s) self.visit_store_in_state(s, prev_s)
self.visit_environment_in_state('environment', 'Expressions', self.visit_environment_in_state('environment', 'Expressions',
s, prev_s) s, prev_s)
self.visit_generic_map_in_state('constraints', 'Ranges', self.visit_generic_map_in_state('constraints', 'Ranges',
s, prev_s) 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', self.visit_generic_map_in_state('dynamic_types', 'Dynamic Types',
s, prev_s) s, prev_s)
self.visit_environment_in_state('constructing_objects', self.visit_environment_in_state('constructing_objects',
'Objects Under Construction', 'Objects Under Construction',
s, prev_s) s, prev_s)
self.visit_checker_messages_in_state(s, prev_s) self.visit_checker_messages_in_state(s, prev_s)
def visit_node(self, node): def visit_node(self, node):
▲ Show 20 Lines • Show All 244 Lines • Show Last 20 Lines