[analyzer] exploded-graph-rewriter: Implement bug nodes and sink nodes.

[NoQ]

Summary

Add a label to nodes that have a bug report attached or on which the analysis was generally interrupted.

Fix printing has_report and implement printing is_sink in the graph dumper.

[NoQ]

[Charusso]

I have removed that is_sink business because we have an actual graph, not just a huge painting, so you could mark whether it is sink by it has zero successors. I like the idea about refactoring that crazy code, thanks!

[NoQ]

Sink node is not the same thing as "zero successors". A sink node is a node in which termination was explictly requested as part of modeling, which is usually nice to know. A non-sink node may have no successors because it ran out of statements to execute (i.e., the analysis finishes successfully).

P.S. I don't have many more plans on implementing more prints in the exploded-graph-rewriter. I have plans to implement different Explorers (which would only visit a part of the graph). You should now be unblocked to take a look at the SVG stuff that you had (but pls keep it at a lower priority than the immediate GSoC stuff).

[Charusso]

In D64110#1567505, @NoQ wrote:

A non-sink node may have no successors because it ran out of statements to execute (i.e., the analysis finishes successfully).

Ah, of course, sorry.

P.S. I don't have many more plans on implementing more prints in the exploded-graph-rewriter. I have plans to implement different Explorers (which would only visit a part of the graph). You should now be unblocked to take a look at the SVG stuff that you had (but pls keep it at a lower priority than the immediate GSoC stuff).

Thanks for your huge amount of work! "Hold my beer."

[NoQ]

Fix the dump_egraph.c test (whoops).

[NoQ]

clang/lib/StaticAnalyzer/Core/ExprEngine.cpp

3009–3010 ↗

(On Diff #207687)

The fix in test/Analysis/dump_egraph.c is related to this change. Previously multiple nodes in the dump were marked as "has_report": true and the CHECK directives were in a wrong order but went unnoticed.

cfe/trunk/lib/StaticAnalyzer/Core/ExprEngine.cpp

static bool nodeHasBugReport(const ExplodedNode *N) {
     BugReporter &BR = static_cast<ExprEngine &>(
       N->getState()->getStateManager().getOwningEngine()).getBugReporter();
 
     const auto EQClasses =
         llvm::make_range(BR.EQClasses_begin(), BR.EQClasses_end());
 
     for (const auto &EQ : EQClasses) {
       for (const BugReport &Report : EQ) {
-        if (Report.getErrorNode()->getState() == N->getState())
+        if (Report.getErrorNode()->getState() == N->getState() &&
+            Report.getErrorNode()->getLocation() == N->getLocation())
           return true;
       }
     }
     return false;
   }
 
   /// \p PreCallback: callback before break.
   /// \p PostCallback: callback after break.
while (true) {
         break;
       PostCallback(OtherNode);
 
       OtherNode = *OtherNode->succ_begin();
     }
     return false;
   }
 
-  static std::string getNodeAttributes(const ExplodedNode *N,
-                                       ExplodedGraph *) {
-    SmallVector<StringRef, 10> Out;
-    auto Noop = [](const ExplodedNode*){};
-    if (traverseHiddenNodes(N, Noop, Noop, &nodeHasBugReport)) {
-      Out.push_back("style=filled");
-      Out.push_back("fillcolor=red");
-    }
-
-    if (traverseHiddenNodes(N, Noop, Noop,
-                            [](const ExplodedNode *C) { return C->isSink(); }))
-      Out.push_back("color=blue");
-    return llvm::join(Out, ",");
-  }
-
   static bool isNodeHidden(const ExplodedNode *N) {
     return N->isTrivial();
   }
 
   static std::string getNodeLabel(const ExplodedNode *N, ExplodedGraph *G){
     std::string Buf;
     llvm::raw_string_ostream Out(Buf);
 
     const bool IsDot = true;
     const unsigned int Space = 1;
     ProgramStateRef State = N->getState();
 
+    auto Noop = [](const ExplodedNode*){};
+    bool HasReport = traverseHiddenNodes(
+        N, Noop, Noop, &nodeHasBugReport);
+    bool IsSink = traverseHiddenNodes(
+        N, Noop, Noop, [](const ExplodedNode *N) { return N->isSink(); });
+
     Out << "{ \"node_id\": " << N->getID(G) << ", \"pointer\": \""
         << (const void *)N << "\", \"state_id\": " << State->getID()
-        << ", \"has_report\": " << (nodeHasBugReport(N) ? "true" : "false")
+        << ", \"has_report\": " << (HasReport ? "true" : "false")
+        << ", \"is_sink\": " << (IsSink ? "true" : "false")
         << ",\\l";
 
     Indent(Out, Space, IsDot) << "\"program_points\": [\\l";
 
     // Dump program point for all the previously skipped nodes.
     traverseHiddenNodes(
         N,
         [&](const ExplodedNode *OtherNode) {

cfe/trunk/test/Analysis/dump_egraph.c

int foo() {
 
   return *x + *y;
 }
 
 // CHECK: \"program_points\": [\l    \{ \"kind\": \"Edge\", \"src_id\": 2, \"dst_id\": 1, \"terminator\": null, \"term_kind\": null, \"tag\": null \}\l  ],\l  \"program_state\": null
 
 // CHECK: \"program_points\": [\l    \{ \"kind\": \"BlockEntrance\", \"block_id\": 1
 
-// CHECK: \"has_report\": true
 
 // CHECK: \"pretty\": \"*x\", \"location\": \{ \"line\": 18, \"column\": 10, \"file\": \"{{(.+)}}dump_egraph.c\" \}
 
 // CHECK: \"pretty\": \"'\\\\x13'\"
 
+// CHECK: \"has_report\": true

cfe/trunk/test/Analysis/exploded-graph-rewriter/checker_messages.dot

 // RUN: %exploded_graph_rewriter %s | FileCheck %s
 
 // FIXME: Substitution doesn't seem to work on Windows.
 // UNSUPPORTED: system-windows
 
 // CHECK: <b>Checker State: </b>
 // CHECK-SAME: <td align="left"><i>alpha.core.FooChecker</i>:</td>
 // CHECK-SAME: <td align="left">Foo stuff:</td>
 // CHECK-SAME: <td align="left">Foo: Bar</td>
 Node0x1 [shape=record,label=
  "{
     { "node_id": 1,
       "pointer": "0x1",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 2,
       "program_points": [],
       "program_state": {
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "environment": null,

cfe/trunk/test/Analysis/exploded-graph-rewriter/checker_messages_diff.dot

 // 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",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 2,
       "program_points": [],
       "program_state": {
         "environment": null,
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,

 // CHECK-SAME: <tr>
 // CHECK-SAME:   <td><font color="forestgreen">+</font></td>
 // CHECK-SAME:   <td align="left">Dunno, some other message.</td>
 // CHECK-SAME: </tr>
 Node0x4 [shape=record,label=
  "{
     { "node_id": 4,
       "pointer": "0x4",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 5,
       "program_points": [],
       "program_state": {
         "environment": null,
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,

 \l}"];
 
 Node0x4 -> Node0x6;
 
 Node0x6 [shape=record,label=
  "{
     { "node_id": 6,
       "pointer": "0x6",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 7,
       "program_points": [],
       "program_state": null
     }
 \l}"];

cfe/trunk/test/Analysis/exploded-graph-rewriter/constraints.dot

 // 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",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 2,
       "program_points": [],
       "program_state": {
         "store": null,
         "environment": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,
         "constraints": [
           { "symbol": "reg_$0<x>", "range": "{ [0, 0] }" }
         ]
       }
     }
 \l}"];

cfe/trunk/test/Analysis/exploded-graph-rewriter/constraints_diff.dot

 // 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",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 2,
       "program_points": [],
       "program_state": {
         "store": null,
         "environment": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,

 // 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",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 4,
       "program_points": [],
       "program_state": {
         "store": null,
         "environment": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,
         "constraints": [
           { "symbol": "reg_$0<x>", "range": "{ [0, 5] }" }
         ]
       }
     }
 \l}"];
 
 Node0x3 -> Node0x5;
 
 Node0x5 [shape=record,label=
  "{
     { "node_id": 5,
       "pointer": "0x5",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 6,
       "program_points": [],
       "program_state": {
         "store": null,
         "environment": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null
       }
     }
 \l}"];

cfe/trunk/test/Analysis/exploded-graph-rewriter/edge.dot

 // RUN: %exploded_graph_rewriter %s | FileCheck %s -check-prefix=LIGHT
 // RUN: %exploded_graph_rewriter --dark %s | FileCheck %s -check-prefixes=DARK
 
 // FIXME: Substitution doesn't seem to work on Windows.
 // UNSUPPORTED: system-windows
 
 Node0x1 [shape=record,label=
- "{{ "node_id": 1, "pointer": "0x1",
+ "{{ "node_id": 1, "pointer": "0x1", "has_report": false, "is_sink": false,
      "program_state": null, "program_points": []}\l}"];
 
 // LIGHT: Node0x1 -> Node0x2;
 // DARK:  Node0x1 -> Node0x2 [color="white"];
 Node0x1 -> Node0x2;
 
 Node0x2 [shape=record,label=
- "{{ "node_id": 2, "pointer": "0x2",
+ "{{ "node_id": 2, "pointer": "0x2", "has_report": false, "is_sink": false,
      "program_state": null, "program_points": []}\l}"];

cfe/trunk/test/Analysis/exploded-graph-rewriter/environment.dot

 // CHECK-SAME:       Unknown
 // CHECK-SAME:     </td>
 // CHECK-SAME:   </tr>
 // CHECK-SAME: </table>
 Node0x1 [shape=record,label=
  "{
     { "node_id": 1,
       "pointer": "0x1",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 2,
       "program_points": [],
       "program_state": {
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,

cfe/trunk/test/Analysis/exploded-graph-rewriter/environment_diff.dot

 // RUN: %exploded_graph_rewriter -d %s | FileCheck %s
 
 // FIXME: Substitution doesn't seem to work on Windows.
 // UNSUPPORTED: system-windows
 
 // No diffs on the first node, nothing to check.
 Node0x1 [shape=record,label=
  "{
     { "node_id": 1,
       "pointer": "0x1",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 2,
       "program_points": [],
       "program_state": {
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,

 // CHECK-SAME:   <td align="left"><i>S9</i></td>
 // CHECK-SAME:   <td align="left">baz()</td>
 // CHECK-SAME:   <td align="left">Undefined</td>
 // CHECK-SAME: </tr>
 Node0x6 [shape=record,label=
  "{
     { "node_id": 6,
       "pointer": "0x6",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 7,
       "program_points": [],
       "program_state": {
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,

 // CHECK-SAME:   <td align="left"><i>S9</i></td>
 // CHECK-SAME:   <td align="left">baz()</td>
 // CHECK-SAME:   <td align="left">Undefined</td>
 // CHECK-SAME: </tr>
 Node0x9 [shape=record,label=
  "{
     { "node_id": 9,
       "pointer": "0x9",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 7,
       "program_points": [],
       "program_state": {
         "store": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,

cfe/trunk/test/Analysis/exploded-graph-rewriter/node_labels.dot

 // CHECK-SAME:   <tr>
 // LIGHT-SAME:     <td bgcolor="gray">
 // DARK-SAME:      <td bgcolor="gray20">
 // CHECK-SAME:       <b>Node 1 (0x1) - State Unspecified</b>
 // CHECK-SAME:     </td>
 // CHECK-SAME:   </tr>
 Node0x1 [shape=record,label=
  "{
-    { "node_id": 1, "pointer": "0x1",
+    { "node_id": 1, "pointer": "0x1", "has_report": false, "is_sink": false,
+      "program_state": null,
+      "program_points": []
+    }
+\l}"];
+
+// CHECK: Node0x2 [
+// CHECK-SAME: <tr><td>
+// CHECK-SAME:   <font color="red"><b>Bug Report Attached</b></font>
+// CHECK-SAME: </td></tr>
+// CHECK-SAME: <tr><td>
+// CHECK-SAME:   <font color="cornflowerblue"><b>Sink Node</b></font>
+// CHECK-SAME: </td></tr>
+Node0x2 [shape=record,label=
+ "{
+    { "node_id": 2, "pointer": "0x2", "has_report": true, "is_sink": true,
       "program_state": null,
       "program_points": []
     }
 \l}"];

cfe/trunk/test/Analysis/exploded-graph-rewriter/program_points.dot

 // CHECK-SAME:     </td>
 // CHECK-SAME:     <td align="left">
 // CHECK-SAME:     [B1]
 // CHECK-SAME:     </td>
 // CHECK-SAME:   </tr>
 // CHECK-SAME: </table>
 Node0x1 [shape=record,label=
  "{
-    { "node_id": 1, "pointer": "0x1",
+    { "node_id": 1, "pointer": "0x1", "has_report": false, "is_sink": false,
       "program_state": null, "program_points": [
       {
         "kind": "Edge",
         "src_id": 0,
         "dst_id": 1,
         "terminator": null,
         "term_kind": null,
         "tag": null

 // CHECK-SAME:     <td colspan="3" align="left">
 // CHECK-SAME:       <b>Tag: </b>
 // CHECK-SAME:       <font color="crimson">ExprEngine : Clean Node</font>
 // CHECK-SAME:     </td>
 // CHECK-SAME:   </tr>
 // CHECK-SAME: </table>
 Node0x2 [shape=record,label=
  "{
-    { "node_id": 2, "pointer": "0x2",
+    { "node_id": 2, "pointer": "0x2", "has_report": false, "is_sink": false,
       "program_state": null, "program_points": [
       {
         "kind": "Statement",
         "stmt_kind": "DeclRefExpr",
         "stmt_point_kind": "PreStmt",
         "stmd_id": 3,
         "pointer": "0x3",
         "pretty": "x",
         "location": {
           "line": 4,
           "column": 5
         },
         "tag": "ExprEngine : Clean Node"
       }
     ]}
 \l}"];
 
 // Test collapsing large pretty prints with braces.
 
 // CHECK-NEXT: <b>Program point:</b>
 // CHECK-SAME: <td>\{ ... \}</td>
 Node0x3 [shape=record,label=
  "{
-    { "node_id": 3, "pointer": "0x3",
+    { "node_id": 3, "pointer": "0x3", "has_report": false, "is_sink": false,
       "program_state": null, "program_points": [
       {
         "kind": "Statement",
         "stmt_kind": "CompoundStmt",
         "stmt_point_kind": "PostStmt",
         "stmd_id": 6,
         "pointer": "0x6",
         "pretty": "{ very very very very very very long pretty print }",
         "location": {
           "line": 7,
           "column": 8
         },
         "tag": "ExprEngine : Clean Node"
       }
     ]}
 \l}"];

cfe/trunk/test/Analysis/exploded-graph-rewriter/store.dot

 // CHECK-SAME:       Undefined
 // CHECK-SAME:     </td>
 // CHECK-SAME:   </tr>
 // CHECK-SAME: </table>
 Node0x1 [shape=record,label=
  "{
     { "node_id": 1,
       "pointer": "0x1",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 2,
       "program_points": [],
       "program_state": {
         "environment": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,

cfe/trunk/test/Analysis/exploded-graph-rewriter/store_diff.dot

 // 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",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 2,
       "program_points": [],
       "program_state": {
         "environment": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,

 // 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",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 5,
       "program_points": [],
       "program_state": {
         "environment": null,
         "constraints": null,
         "dynamic_types": null,
         "constructing_objects": null,
         "checker_messages": null,

 \l}"];
 
 Node0x4 -> Node0x6;
 
 Node0x6 [shape=record,label=
  "{
     { "node_id": 6,
       "pointer": "0x6",
+      "has_report": false,
+      "is_sink": false,
       "state_id": 7,
       "program_points": [],
       "program_state": null
     }
 \l}"];

cfe/trunk/utils/analyzer/exploded-graph-rewriter.py

def __init__(self):
         super(ExplodedNode, self).__init__()
         self.predecessors = []
         self.successors = []
 
     def construct(self, node_id, json_node):
         logging.debug('Adding ' + node_id)
         self.node_id = json_node['node_id']
         self.ptr = json_node['pointer']
+        self.has_report = json_node['has_report']
+        self.is_sink = json_node['is_sink']
         self.points = [ProgramPoint(p) for p in json_node['program_points']]
         self.state = ProgramState(json_node['state_id'],
                                   json_node['program_state']) \
             if json_node['program_state'] is not None else None
 
         assert self.node_name() == node_id
 
     def node_name(self):
def visit_node(self, node):
             self._dump('color="white",fontcolor="gray80",')
         self._dump('label=<<table border="0">')
 
         self._dump('<tr><td bgcolor="%s"><b>Node %d (%s) - '
                    'State %s</b></td></tr>'
                    % ("gray20" if self._dark_mode else "gray",
                       node.node_id, node.ptr, node.state.state_id
                       if node.state is not None else 'Unspecified'))
+        if node.has_report:
+            self._dump('<tr><td><font color="red"><b>Bug Report Attached'
+                       '</b></font></td></tr>')
+        if node.is_sink:
+            self._dump('<tr><td><font color="cornflowerblue"><b>Sink Node'
+                       '</b></font></td></tr>')
         self._dump('<tr><td align="left" width="0">')
         if len(node.points) > 1:
             self._dump('<b>Program points:</b></td></tr>')
         else:
             self._dump('<b>Program point:</b></td></tr>')
         self._dump('<tr><td align="left" width="0">'
                    '<table border="0" align="left" width="0">')
         for p in node.points: