[analyzer] A Python script to prettify the ExplodedGraph dumps.

[NoQ]

Summary

That's my attempt on D62553 that i (just) promised.

Here's roughly how it looks:

Full dump of some random test file:

graph.svg207 KBDownload

The rough idea behind this script is that it deserializes JSON dumps into familiar python objects. Serializing them back into a pretty graph dump is only one of the possible use-cases; we can manipulate the deserialized graph by, say, hiding nodes that we aren't interested in.

This initial commit only supports Environment and Store and silently drops unsupported information; i'll hopefully follow up with more this week, most importantly ranges. As of today it's only a dot-to-dot converter, so @Charusso's SVG cleanup is not supported yet. Diffs are not supported yet; tomorrow i'll think a bit more how exactly do i want to implement them.

I wrote some tests but i'm not really sure they're worth it. I guess some corner-cases would be nice to document this way.

@Charusso, could you see if you can:

• Bring back stable IDs for nodes into JSON (not only pointers). They're very useful for debugging.
• See if your trick for reducing SVG size with text joining is even applicable to the dumps that i produce.
• Understand my code here :)

[NoQ]

Abstract away raw prints.

[NoQ]

Remove outdated comment.

[NoQ]

Use os.path.join for discovering the utility in tests.

[NoQ]

I wrote some tests but i'm not really sure they're worth it.

Mmm, on second thought, they probably won't work out of the box, because they might require installing python modules in order to work. I'm actually not sure if all machines have python3. I'll try but it'll most likely fail. I guess i could try excluding them from make check-all.

[Charusso]

Sorry for that much rewrite request but in a script language you have to name your stuff properly or you will be completely lost. I have not written a single Python class yet, but trust me.

I really like that DotDumpVisitor semantic, but it would be a lot better at SVG level. At the moment whatever style/table-data you insert it adds an extra text tag per styling which is quite inefficient.

We could use "foreignObject" (somehow) and apply pure HTML tables or I could use my <tspan> idea instead (https://developer.mozilla.org/en-US/docs/Web/SVG/Element/tspan). I recommend the latter as it is better than a fixed table.

With the current representation it would be difficult to apply every styling to tspans. I think it also would be difficult to use your Explorer idea as we are talking about modificating the SVG dynamically.

In D62638#1522357, @NoQ wrote:

I wrote some tests but i'm not really sure they're worth it.

Mmm, on second thought, they probably won't work out of the box, because they might require installing python modules in order to work. I'm actually not sure if all machines have python3. I'll try but it'll most likely fail. I guess i could try excluding them from make check-all.

It would be cool to introduce something like check-scripts.

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

5 ↗

(On Diff #202094)

I think it is not that cool variable name. I would use the appropiate name of the object instead of the generic json name.

12 ↗

(On Diff #202094)

json -> loc

22 ↗

(On Diff #202094)

json -> program_point and so on...

33 ↗

(On Diff #202094)

What about just loc?

124 ↗

(On Diff #202094)

What about predecessors and successors? It is the proper name in the Static Analyzer world.

126 ↗

(On Diff #202094)

• set_json() -> set() the given node
• json -> node

151 ↗

(On Diff #202094)

nodes -> graph

184 ↗

(On Diff #202094)

raw_json -> node_string which will be a raw JSON after loads().

191 ↗

(On Diff #202094)

I have removed the trailing , from the end yesterday so rstrip(',') is not needed.

It would be cool to name the result[], like: pred_id = result[1] and succ_id = result[2] or current/previous ID, or something like that.

I also would put the regexes into a function and you could write:
pred_id, succ_id = parse_edge() or something more simpler.

What is result[0] btw? That confused me a little-bit.

233 ↗

(On Diff #202094)

It would be cool to put it into a "switch-statement" (https://stackoverflow.com/questions/60208/replacements-for-switch-statement-in-python).

237 ↗

(On Diff #202094)

I think tables are left aligned by default, so you could remove your left alignments.

326 ↗

(On Diff #202094)

I would create a table-builder class to reduce the repetition and for better readability what is going on. Also you could avoid balign typo.

Then may each class could have its own pretty-print method like LLVM does.

[NoQ]

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

326 ↗

(On Diff #202094)

balign is a thing in the graphviz dialect of html (https://www.graphviz.org/doc/info/shapes.html)

(not sure i still need this in the current incarnation of the script, given that we've removed those whole-decl pretty-prints in D62495)

[NoQ]

Fxd!

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

151 ↗

(On Diff #202094)

Mm, why would i have a field called "graph" in an object called "graph".

191 ↗

(On Diff #202094)

pred_id, succ_id = parse_edge()

Not really, i'd also have to return whether the match was successful, which kinda makes it as bad as before.

What is result[0] btw? That confused me a little-bit.

That's the entire match. https://docs.python.org/3/library/re.html#match-objects

233 ↗

(On Diff #202094)

I don't want to list the same color many times for each key that maps into it.

237 ↗

(On Diff #202094)

Unfortunately in GraphViz they're centered by default.

[NoQ]

Also switched to python2 because it seems to be the default. The differences are minimal.

[Charusso]

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

151 ↗

(On Diff #202094)

Because we are constructing the graph object and it would be still much better than LLVM's fancy Graph TheGraph; logic. I am okay with a bunch of nodes, just those are the graph itself.

191 ↗

(On Diff #202094)

I see, just I am that newbie. Thanks!

237 ↗

(On Diff #202094)

Well, that is unfortunate.

[Charusso]

In D62638#1525823, @NoQ wrote:

Also switched to python2 because it seems to be the default. The differences are minimal.

What about the state of the patch itself? Planned stuff WIP, could I take it to SVGify, or?

[NoQ]

In D62638#1525843, @Charusso wrote:

In D62638#1525823, @NoQ wrote:

Also switched to python2 because it seems to be the default. The differences are minimal.

What about the state of the patch itself? Planned stuff WIP, could I take it to SVGify, or?

The format would look roughly the same from now on, but i'll add more prints for other state traits and may slightly rearrange fields around, also diffs which would be simply extra +/- fields in the tables that otherwise look the same. I guess you should wait until i commit this revision and we at least figure out what's the situation with buildbots and tests.

[NoQ]

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

191 ↗

(On Diff #202094)

I have removed the trailing , from the end yesterday so rstrip(',') is not needed.

It still seems to be there for all nodes except the last node.

[Charusso]

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

191 ↗

(On Diff #202094)

Hm, that is why your testing idea is so cool, I am nearly sure I have removed it.

[NoQ]

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

191 ↗

(On Diff #202094)

*politely refuses to take credit for inventing test-driven development*

[NoQ]

Rebase.

[Charusso]

Let us see those tests!

[NoQ]

I disabled tests on Windows for now (rC362343 -> rC362347), but other than that the tests are working well, there was nothing to worry about.

[krytarowski]

This commit breaks the NetBSD buildbot node.

http://lab.llvm.org:8011/builders/netbsd-amd64/builds/20359

The problem is that this patch hardcodes python specific binary name, while it has to be detected dynamically or ideally passed from CMake. Afair lit has a knowledge of too.

​#!/usr/bin/env python # <- unportable form

On NetBSD with pkgsrc this can be python2.7, but the name is not fixed.

Plase correct this.

[Charusso]

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

1

# something else then
#
#==- exploded-graph-rewriter.py - Simplifies the ExplodedGraph -*- python -*-==#
#
# Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
# See https://llvm.org/LICENSE.txt for license information.
# SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
#
#===------------------------------------------------------------------------===#

Whoops!

[NoQ]

Thanks!! Will fix as soon as i get to my desktop.

[NoQ]

In D62638#1529170, @krytarowski wrote:

This commit breaks the NetBSD buildbot node.

rC362574.

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

1

rC362575.

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

+// RUN: %exploded_graph_rewriter %s | FileCheck %s
+
+Node0x1 [shape=record,label=
+ "{{ "node_id": 1, "pointer": "0x1",
+     "program_state": null, "program_points": []}\l}"];
+
+// CHECK: Node0x1 -> Node0x2;
+Node0x1 -> Node0x2;
+
+Node0x2 [shape=record,label=
+ "{{ "node_id": 2, "pointer": "0x2",
+     "program_state": null, "program_points": []}\l}"];

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

+// RUN: %exploded_graph_rewriter %s | FileCheck %s
+
+digraph "Exploded Graph" {
+  label="Exploded Graph";
+}
+
+// CHECK:      digraph "ExplodedGraph" {
+// CHECK-NEXT:   label="";
+// CHECK-NEXT: }

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

+// RUN: %exploded_graph_rewriter %s | FileCheck %s
+
+// CHECK: <b>Environment: </b>
+// CHECK-SAME: <table border="0">
+// CHECK-SAME:   <tr>
+// CHECK-SAME:     <td align="left">
+// CHECK-SAME:       <b>#0 Call</b>
+// CHECK-SAME:     </td>
+// CHECK-SAME:     <td align="left">
+// CHECK-SAME:       <font color="grey60">foo </font>(line 4)
+// CHECK-SAME:     </td>
+// CHECK-SAME:   </tr>
+// CHECK-SAME:   <tr>
+// CHECK-SAME:     <td align="left">
+// CHECK-SAME:       <i>S5</i>
+// CHECK-SAME:     </td>
+// CHECK-SAME:     <td align="left">
+// CHECK-SAME:       bar()
+// CHECK-SAME:     </td>
+// CHECK-SAME:     <td align="left">
+// CHECK-SAME:       Unknown
+// CHECK-SAME:     </td>
+// CHECK-SAME:   </tr>
+// CHECK-SAME: </table>
+Node0x1 [shape=record,label=
+ "{
+    { "node_id": 1,
+      "pointer": "0x1",
+      "state_id": 2,
+      "program_points": [],
+      "program_state": {
+        "store": null,
+        "environment": [
+          {
+            "location_context": "#0 Call",
+            "lctx_id": 3,
+            "calling": "foo",
+            "call_line": 4,
+            "items": [
+              {
+                "stmt_id": 5,
+                "pretty": "bar()",
+                "value": "Unknown"
+              }
+            ]
+          }
+        ]
+      }
+    }
+\l}"];

cfe/trunk/test/Analysis/exploded-graph-rewriter/lit.local.cfg

+import lit.util
+import lit.formats
+import os
+
+use_lit_shell = os.environ.get("LIT_USE_INTERNAL_SHELL")
+config.test_format = lit.formats.ShTest(use_lit_shell == "0")
+
+config.substitutions.append(('%exploded_graph_rewriter',
+                             lit.util.which('exploded-graph-rewriter.py',
+                                            os.path.join(config.clang_src_dir,
+                                                         'utils', 'analyzer'))))
+
+config.suffixes = ['.dot']

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

+// RUN: %exploded_graph_rewriter %s | FileCheck %s
+
+// CHECK: <b>Program point:</b>
+// CHECK-SAME: <table border="0" align="left" width="0">
+// CHECK-SAME:   <tr>
+// CHECK-SAME:     <td width="0">
+// CHECK-SAME:       -
+// CHECK-SAME:     </td>
+// CHECK-SAME:     <td align="left" width="0">
+// CHECK-SAME:       <font color="gold3">Edge</font>
+// CHECK-SAME:     </td>
+// CHECK-SAME:     <td align="left">
+// CHECK-SAME:     [B0] -&gt; [B1]
+// CHECK-SAME:     </td>
+// CHECK-SAME:   </tr>
+// CHECK-SAME: </table>
+Node0x1 [shape=record,label=
+ "{
+    { "node_id": 1, "pointer": "0x1",
+      "program_state": null, "program_points": [
+      {
+        "kind": "Edge",
+        "src_id": 0,
+        "dst_id": 1,
+        "terminator": null,
+        "term_kind": null,
+        "tag": null }
+    ]}
+\l}"];
+
+// CHECK-NEXT: <b>Program point:</b>
+// CHECK-SAME: <table border="0" align="left" width="0">
+// CHECK-SAME:   <tr>
+// CHECK-SAME:     <td align="left" width="0">
+// CHECK-SAME:       (main file):<b>4</b>:<b>5</b>:
+// CHECK-SAME:     </td>
+// CHECK-SAME:     <td align="left" width="0">
+// CHECK-SAME:       <font color="cyan3">DeclRefExpr</font>
+// CHECK-SAME:     </td>
+// CHECK-SAME:     <td>x</td>
+// CHECK-SAME:   </tr>
+// CHECK-SAME: </table>
+Node0x2 [shape=record,label=
+ "{
+    { "node_id": 2, "pointer": "0x2",
+      "program_state": null, "program_points": [
+      {
+        "kind": "Statement",
+        "stmt_kind": "DeclRefExpr",
+        "stmd_id": 3,
+        "pointer": "0x3",
+        "pretty": "x",
+        "location": {
+          "line": 4,
+          "column": 5
+        },
+        "tag": null
+      }
+    ]}
+\l}"];

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

+// RUN: %exploded_graph_rewriter %s | FileCheck %s
+
+// CHECK: <b>Store: </b>
+// CHECK-SAME: <table border="0">
+// CHECK-SAME:   <tr>
+// CHECK-SAME:     <td align="left">
+// CHECK-SAME:       x
+// CHECK-SAME:     </td>
+// CHECK-SAME:     <td align="left">
+// CHECK-SAME:       0
+// CHECK-SAME:     </td>
+// CHECK-SAME:     <td align="left">
+// CHECK-SAME:       (<i>Default</i>)
+// CHECK-SAME:     </td>
+// CHECK-SAME:     <td align="left">
+// CHECK-SAME:       Undefined
+// CHECK-SAME:     </td>
+// CHECK-SAME:   </tr>
+// CHECK-SAME: </table>
+Node0x1 [shape=record,label=
+ "{
+    { "node_id": 1,
+      "pointer": "0x1",
+      "state_id": 2,
+      "program_points": [],
+      "program_state": {
+        "environment": null,
+        "store": [
+          {
+            "cluster": "x",
+            "items": [
+              {
+                "kind": "Default",
+                "offset": 0,
+                "value": "Undefined"
+              }
+            ]
+          }
+        ]
+      }
+    }
+\l}"];

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

+#!/usr/bin/env python
+
+from __future__ import print_function
+
+import argparse
+import collections
+import json
+import logging
+import re
+
+
+# A deserialized source location.
+class SourceLocation(object):
+    def __init__(self, json_loc):
+        super(SourceLocation, self).__init__()
+        self.line = json_loc['line']
+        self.col = json_loc['column']
+        self.filename = json_loc['filename'] \
+            if 'filename' in json_loc else '(main file)'
+
+
+# A deserialized program point.
+class ProgramPoint(object):
+    def __init__(self, json_pp):
+        super(ProgramPoint, self).__init__()
+        self.kind = json_pp['kind']
+        self.tag = json_pp['tag']
+        if self.kind == 'Edge':
+            self.src_id = json_pp['src_id']
+            self.dst_id = json_pp['dst_id']
+        elif self.kind == 'Statement':
+            self.stmt_kind = json_pp['stmt_kind']
+            self.pointer = json_pp['pointer']
+            self.pretty = json_pp['pretty']
+            self.loc = SourceLocation(json_pp['location']) \
+                if json_pp['location'] is not None else None
+        elif self.kind == 'BlockEntrance':
+            self.block_id = json_pp['block_id']
+
+
+# A value of a single expression in a deserialized Environment.
+class EnvironmentBinding(object):
+    def __init__(self, json_eb):
+        super(EnvironmentBinding, self).__init__()
+        self.stmt_id = json_eb['stmt_id']
+        self.pretty = json_eb['pretty']
+        self.value = json_eb['value']
+
+
+# Deserialized description of a location context.
+class LocationContext(object):
+    def __init__(self, json_frame):
+        super(LocationContext, self).__init__()
+        self.lctx_id = json_frame['lctx_id']
+        self.caption = json_frame['location_context']
+        self.decl = json_frame['calling']
+        self.line = json_frame['call_line']
+
+
+# A group of deserialized Environment bindings that correspond to a specific
+# location context.
+class EnvironmentFrame(object):
+    def __init__(self, json_frame):
+        super(EnvironmentFrame, self).__init__()
+        self.location_context = LocationContext(json_frame)
+        self.bindings = [EnvironmentBinding(b) for b in json_frame['items']] \
+            if json_frame['items'] is not None else []
+
+
+# A deserialized Environment.
+class Environment(object):
+    def __init__(self, json_e):
+        super(Environment, self).__init__()
+        self.frames = [EnvironmentFrame(f) for f in json_e]
+
+
+# A single binding in a deserialized RegionStore cluster.
+class StoreBinding(object):
+    def __init__(self, json_sb):
+        super(StoreBinding, self).__init__()
+        self.kind = json_sb['kind']
+        self.offset = json_sb['offset']
+        self.value = json_sb['value']
+
+
+# A single cluster of the deserialized RegionStore.
+class StoreCluster(object):
+    def __init__(self, json_sc):
+        super(StoreCluster, self).__init__()
+        self.base_region = json_sc['cluster']
+        self.bindings = [StoreBinding(b) for b in json_sc['items']]
+
+
+# A deserialized RegionStore.
+class Store(object):
+    def __init__(self, json_s):
+        super(Store, self).__init__()
+        self.clusters = [StoreCluster(c) for c in json_s]
+
+
+# A deserialized program state.
+class ProgramState(object):
+    def __init__(self, state_id, json_ps):
+        super(ProgramState, self).__init__()
+        logging.debug('Adding ProgramState ' + str(state_id))
+
+        self.state_id = state_id
+        self.store = Store(json_ps['store']) \
+            if json_ps['store'] is not None else None
+        self.environment = Environment(json_ps['environment']) \
+            if json_ps['environment'] is not None else None
+        # TODO: Objects under construction.
+        # TODO: Constraint ranges.
+        # TODO: Dynamic types of objects.
+        # TODO: Checker messages.
+
+
+# A deserialized exploded graph node. Has a default constructor because it
+# may be referenced as part of an edge before its contents are deserialized,
+# and in this moment we already need a room for predecessors and successors.
+class ExplodedNode(object):
+    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.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):
+        return 'Node' + self.ptr
+
+
+# A deserialized ExplodedGraph. Constructed by consuming a .dot file
+# line-by-line.
+class ExplodedGraph(object):
+    # Parse .dot files with regular expressions.
+    node_re = re.compile(
+        '^(Node0x[0-9a-f]*) \\[shape=record,.*label="{(.*)\\\\l}"\\];$')
+    edge_re = re.compile(
+        '^(Node0x[0-9a-f]*) -> (Node0x[0-9a-f]*);$')
+
+    def __init__(self):
+        super(ExplodedGraph, self).__init__()
+        self.nodes = collections.defaultdict(ExplodedNode)
+        self.root_id = None
+        self.incomplete_line = ''
+
+    def add_raw_line(self, raw_line):
+        if raw_line.startswith('//'):
+            return
+
+        # Allow line breaks by waiting for ';'. This is not valid in
+        # a .dot file, but it is useful for writing tests.
+        if len(raw_line) > 0 and raw_line[-1] != ';':
+            self.incomplete_line += raw_line
+            return
+        raw_line = self.incomplete_line + raw_line
+        self.incomplete_line = ''
+
+        # Apply regexps one by one to see if it's a node or an edge
+        # and extract contents if necessary.
+        logging.debug('Line: ' + raw_line)
+        result = self.edge_re.match(raw_line)
+        if result is not None:
+            logging.debug('Classified as edge line.')
+            pred = result.group(1)
+            succ = result.group(2)
+            self.nodes[pred].successors.append(succ)
+            self.nodes[succ].predecessors.append(pred)
+            return
+        result = self.node_re.match(raw_line)
+        if result is not None:
+            logging.debug('Classified as node line.')
+            node_id = result.group(1)
+            if len(self.nodes) == 0:
+                self.root_id = node_id
+            # Note: when writing tests you don't need to escape everything,
+            # even though in a valid dot file everything is escaped.
+            node_label = result.group(2).replace('\\l', '') \
+                                        .replace(' ', '') \
+                                        .replace('\\"', '"') \
+                                        .replace('\\{', '{') \
+                                        .replace('\\}', '}') \
+                                        .replace('\\<', '\\\\<') \
+                                        .replace('\\>', '\\\\>') \
+                                        .rstrip(',')
+            logging.debug(node_label)
+            json_node = json.loads(node_label)
+            self.nodes[node_id].construct(node_id, json_node)
+            return
+        logging.debug('Skipping.')
+
+
+# A visitor that dumps the ExplodedGraph into a DOT file with fancy HTML-based
+# syntax highlighing.
+class DotDumpVisitor(object):
+    def __init__(self):
+        super(DotDumpVisitor, self).__init__()
+
+    @staticmethod
+    def _dump_raw(s):
+        print(s, end='')
+
+    @staticmethod
+    def _dump(s):
+        print(s.replace('&', '&amp;')
+               .replace('{', '\\{')
+               .replace('}', '\\}')
+               .replace('\\<', '&lt;')
+               .replace('\\>', '&gt;')
+               .replace('\\l', '<br />')
+               .replace('|', ''), end='')
+
+    def visit_begin_graph(self, graph):
+        self._graph = graph
+        self._dump_raw('digraph "ExplodedGraph" {\n')
+        self._dump_raw('label="";\n')
+
+    def visit_program_point(self, p):
+        if p.kind in ['Edge', 'BlockEntrance', 'BlockExit']:
+            color = 'gold3'
+        elif p.kind in ['PreStmtPurgeDeadSymbols',
+                        'PostStmtPurgeDeadSymbols']:
+            color = 'red'
+        elif p.kind in ['CallEnter', 'CallExitBegin', 'CallExitEnd']:
+            color = 'blue'
+        elif p.kind in ['Statement']:
+            color = 'cyan3'
+        else:
+            color = 'forestgreen'
+
+        if p.kind == 'Statement':
+            if p.loc is not None:
+                self._dump('<tr><td align="left" width="0">'
+                           '%s:<b>%s</b>:<b>%s</b>:</td>'
+                           '<td align="left" width="0"><font color="%s">'
+                           '%s</font></td><td>%s</td></tr>'
+                           % (p.loc.filename, p.loc.line,
+                              p.loc.col, color, p.stmt_kind, p.pretty))
+            else:
+                self._dump('<tr><td align="left" width="0">'
+                           '<i>Invalid Source Location</i>:</td>'
+                           '<td align="left" width="0">'
+                           '<font color="%s">%s</font></td><td>%s</td></tr>'
+                           % (color, p.stmt_kind, p.pretty))
+        elif p.kind == 'Edge':
+            self._dump('<tr><td width="0">-</td>'
+                       '<td align="left" width="0">'
+                       '<font color="%s">%s</font></td><td align="left">'
+                       '[B%d] -\\> [B%d]</td></tr>'
+                       % (color, p.kind, p.src_id, p.dst_id))
+        else:
+            # TODO: Print more stuff for other kinds of points.
+            self._dump('<tr><td width="0">-</td>'
+                       '<td align="left" width="0" colspan="2">'
+                       '<font color="%s">%s</font></td></tr>'
+                       % (color, p.kind))
+
+    def visit_environment(self, e):
+        self._dump('<table border="0">')
+
+        for f in e.frames:
+            self._dump('<tr><td align="left"><b>%s</b></td>'
+                       '<td align="left"><font color="grey60">%s </font>'
+                       '%s</td></tr>'
+                       % (f.location_context.caption,
+                          f.location_context.decl,
+                          ('(line %s)' % f.location_context.line)
+                          if f.location_context.line is not None else ''))
+            for b in f.bindings:
+                self._dump('<tr><td align="left"><i>S%s</i></td>'
+                           '<td align="left">%s</td>'
+                           '<td align="left">%s</td></tr>'
+                           % (b.stmt_id, b.pretty, b.value))
+
+        self._dump('</table>')
+
+    def visit_store(self, s):
+        self._dump('<table border="0">')
+
+        for c in s.clusters:
+            for b in c.bindings:
+                self._dump('<tr><td align="left">%s</td>'
+                           '<td align="left">%s</td>'
+                           '<td align="left">%s</td>'
+                           '<td align="left">%s</td></tr>'
+                           % (c.base_region, b.offset,
+                              '(<i>Default</i>)' if b.kind == 'Default'
+                              else '',
+                              b.value))
+
+        self._dump('</table>')
+
+    def visit_state(self, s):
+        self._dump('<tr><td align="left">'
+                   '<b>Store: </b>')
+        if s.store is None:
+            self._dump('<i> Nothing!</i>')
+        else:
+            self._dump('</td></tr>'
+                       '<tr><td align="left">')
+            self.visit_store(s.store)
+
+        self._dump('</td></tr><hr />'
+                   '<tr><td align="left">'
+                   '<b>Environment: </b>')
+        if s.environment is None:
+            self._dump('<i> Nothing!</i>')
+        else:
+            self._dump('</td></tr>'
+                       '<tr><td align="left">')
+            self.visit_environment(s.environment)
+
+        self._dump('</td></tr>')
+
+    def visit_node(self, node):
+        self._dump('%s [shape=record,label=<<table border="0">'
+                   % (node.node_name()))
+
+        self._dump('<tr><td bgcolor="grey"><b>Node %d (%s) - '
+                   'State %s</b></td></tr>'
+                   % (node.node_id, node.ptr, node.state.state_id
+                      if node.state is not None else 'Unspecified'))
+        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:
+            self.visit_program_point(p)
+        self._dump('</table></td></tr>')
+
+        if node.state is not None:
+            self._dump('<hr />')
+            self.visit_state(node.state)
+        self._dump_raw('</table>>];\n')
+
+    def visit_edge(self, pred, succ):
+        self._dump_raw('%s -> %s;\n' % (pred.node_name(), succ.node_name()))
+
+    def visit_end_of_graph(self):
+        self._dump_raw('}\n')
+
+
+# A class that encapsulates traversal of the ExplodedGraph. Different explorer
+# kinds could potentially traverse specific sub-graphs.
+class Explorer(object):
+    def __init__(self):
+        super(Explorer, self).__init__()
+
+    def explore(self, graph, visitor):
+        visitor.visit_begin_graph(graph)
+        for node in sorted(graph.nodes):
+            logging.debug('Visiting ' + node)
+            visitor.visit_node(graph.nodes[node])
+            for succ in sorted(graph.nodes[node].successors):
+                logging.debug('Visiting edge: %s -> %s ' % (node, succ))
+                visitor.visit_edge(graph.nodes[node], graph.nodes[succ])
+        visitor.visit_end_of_graph()
+
+
+def main():
+    parser = argparse.ArgumentParser()
+    parser.add_argument('filename', type=str)
+    parser.add_argument('-d', '--debug', action='store_const', dest='loglevel',
+                        const=logging.DEBUG, default=logging.WARNING,
+                        help='enable debug prints')
+    parser.add_argument('-v', '--verbose', action='store_const',
+                        dest='loglevel', const=logging.INFO,
+                        default=logging.WARNING,
+                        help='enable info prints')
+    args = parser.parse_args()
+    logging.basicConfig(level=args.loglevel)
+
+    graph = ExplodedGraph()
+    with open(args.filename) as fd:
+        for raw_line in fd:
+            raw_line = raw_line.strip()
+            graph.add_raw_line(raw_line)
+
+    explorer = Explorer()
+    visitor = DotDumpVisitor()
+    explorer.explore(graph, visitor)
+
+
+if __name__ == '__main__':
+    main()