1#!/usr/bin/env python 2# 3#===- exploded-graph-rewriter.py - ExplodedGraph dump tool -----*- python -*--# 4# 5# Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. 6# See https://llvm.org/LICENSE.txt for license information. 7# SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception 8# 9#===-----------------------------------------------------------------------===# 10 11 12from __future__ import print_function 13 14import argparse 15import collections 16import difflib 17import json 18import logging 19import re 20 21 22# A helper function for finding the difference between two dictionaries. 23def diff_dicts(curr, prev): 24 removed = [k for k in prev if k not in curr or curr[k] != prev[k]] 25 added = [k for k in curr if k not in prev or curr[k] != prev[k]] 26 return (removed, added) 27 28 29# Represents any program state trait that is a dictionary of key-value pairs. 30class GenericMap(object): 31 def __init__(self, items): 32 self.generic_map = collections.OrderedDict(items) 33 34 def diff(self, prev): 35 return diff_dicts(self.generic_map, prev.generic_map) 36 37 def is_different(self, prev): 38 removed, added = self.diff(prev) 39 return len(removed) != 0 or len(added) != 0 40 41 42# A deserialized source location. 43class SourceLocation(object): 44 def __init__(self, json_loc): 45 super(SourceLocation, self).__init__() 46 self.line = json_loc['line'] 47 self.col = json_loc['column'] 48 self.filename = json_loc['filename'] \ 49 if 'filename' in json_loc else '(main file)' 50 51 52# A deserialized program point. 53class ProgramPoint(object): 54 def __init__(self, json_pp): 55 super(ProgramPoint, self).__init__() 56 self.kind = json_pp['kind'] 57 self.tag = json_pp['tag'] 58 if self.kind == 'Edge': 59 self.src_id = json_pp['src_id'] 60 self.dst_id = json_pp['dst_id'] 61 elif self.kind == 'Statement': 62 self.stmt_kind = json_pp['stmt_kind'] 63 self.stmt_point_kind = json_pp['stmt_point_kind'] 64 self.pointer = json_pp['pointer'] 65 self.pretty = json_pp['pretty'] 66 self.loc = SourceLocation(json_pp['location']) \ 67 if json_pp['location'] is not None else None 68 elif self.kind == 'BlockEntrance': 69 self.block_id = json_pp['block_id'] 70 71 72# A single expression acting as a key in a deserialized Environment. 73class EnvironmentBindingKey(object): 74 def __init__(self, json_ek): 75 super(EnvironmentBindingKey, self).__init__() 76 # CXXCtorInitializer is not a Stmt! 77 self.stmt_id = json_ek['stmt_id'] if 'stmt_id' in json_ek \ 78 else json_ek['init_id'] 79 self.pretty = json_ek['pretty'] 80 self.kind = json_ek['kind'] if 'kind' in json_ek else None 81 82 def _key(self): 83 return self.stmt_id 84 85 def __eq__(self, other): 86 return self._key() == other._key() 87 88 def __hash__(self): 89 return hash(self._key()) 90 91 92# Deserialized description of a location context. 93class LocationContext(object): 94 def __init__(self, json_frame): 95 super(LocationContext, self).__init__() 96 self.lctx_id = json_frame['lctx_id'] 97 self.caption = json_frame['location_context'] 98 self.decl = json_frame['calling'] 99 self.line = json_frame['call_line'] 100 101 def _key(self): 102 return self.lctx_id 103 104 def __eq__(self, other): 105 return self._key() == other._key() 106 107 def __hash__(self): 108 return hash(self._key()) 109 110 111# A group of deserialized Environment bindings that correspond to a specific 112# location context. 113class EnvironmentFrame(object): 114 def __init__(self, json_frame): 115 super(EnvironmentFrame, self).__init__() 116 self.location_context = LocationContext(json_frame) 117 self.bindings = collections.OrderedDict( 118 [(EnvironmentBindingKey(b), 119 b['value']) for b in json_frame['items']] 120 if json_frame['items'] is not None else []) 121 122 def diff_bindings(self, prev): 123 return diff_dicts(self.bindings, prev.bindings) 124 125 def is_different(self, prev): 126 removed, added = self.diff_bindings(prev) 127 return len(removed) != 0 or len(added) != 0 128 129 130# A deserialized Environment. This class can also hold other entities that 131# are similar to Environment, such as Objects Under Construction. 132class GenericEnvironment(object): 133 def __init__(self, json_e): 134 super(GenericEnvironment, self).__init__() 135 self.frames = [EnvironmentFrame(f) for f in json_e] 136 137 def diff_frames(self, prev): 138 # TODO: It's difficult to display a good diff when frame numbers shift. 139 if len(self.frames) != len(prev.frames): 140 return None 141 142 updated = [] 143 for i in range(len(self.frames)): 144 f = self.frames[i] 145 prev_f = prev.frames[i] 146 if f.location_context == prev_f.location_context: 147 if f.is_different(prev_f): 148 updated.append(i) 149 else: 150 # We have the whole frame replaced with another frame. 151 # TODO: Produce a nice diff. 152 return None 153 154 # TODO: Add support for added/removed. 155 return updated 156 157 def is_different(self, prev): 158 updated = self.diff_frames(prev) 159 return updated is None or len(updated) > 0 160 161 162# A single binding key in a deserialized RegionStore cluster. 163class StoreBindingKey(object): 164 def __init__(self, json_sk): 165 super(StoreBindingKey, self).__init__() 166 self.kind = json_sk['kind'] 167 self.offset = json_sk['offset'] 168 169 def _key(self): 170 return (self.kind, self.offset) 171 172 def __eq__(self, other): 173 return self._key() == other._key() 174 175 def __hash__(self): 176 return hash(self._key()) 177 178 179# A single cluster of the deserialized RegionStore. 180class StoreCluster(object): 181 def __init__(self, json_sc): 182 super(StoreCluster, self).__init__() 183 self.base_region = json_sc['cluster'] 184 self.bindings = collections.OrderedDict( 185 [(StoreBindingKey(b), b['value']) for b in json_sc['items']]) 186 187 def diff_bindings(self, prev): 188 return diff_dicts(self.bindings, prev.bindings) 189 190 def is_different(self, prev): 191 removed, added = self.diff_bindings(prev) 192 return len(removed) != 0 or len(added) != 0 193 194 195# A deserialized RegionStore. 196class Store(object): 197 def __init__(self, json_s): 198 super(Store, self).__init__() 199 self.ptr = json_s['pointer'] 200 self.clusters = collections.OrderedDict( 201 [(c['pointer'], StoreCluster(c)) for c in json_s['items']]) 202 203 def diff_clusters(self, prev): 204 removed = [k for k in prev.clusters if k not in self.clusters] 205 added = [k for k in self.clusters if k not in prev.clusters] 206 updated = [k for k in prev.clusters if k in self.clusters 207 and prev.clusters[k].is_different(self.clusters[k])] 208 return (removed, added, updated) 209 210 def is_different(self, prev): 211 removed, added, updated = self.diff_clusters(prev) 212 return len(removed) != 0 or len(added) != 0 or len(updated) != 0 213 214 215# Deserialized messages from a single checker in a single program state. 216# Basically a list of raw strings. 217class CheckerLines(object): 218 def __init__(self, json_lines): 219 super(CheckerLines, self).__init__() 220 self.lines = json_lines 221 222 def diff_lines(self, prev): 223 lines = difflib.ndiff(prev.lines, self.lines) 224 return [l.strip() for l in lines 225 if l.startswith('+') or l.startswith('-')] 226 227 def is_different(self, prev): 228 return len(self.diff_lines(prev)) > 0 229 230 231# Deserialized messages of all checkers, separated by checker. 232class CheckerMessages(object): 233 def __init__(self, json_m): 234 super(CheckerMessages, self).__init__() 235 self.items = collections.OrderedDict( 236 [(m['checker'], CheckerLines(m['messages'])) for m in json_m]) 237 238 def diff_messages(self, prev): 239 removed = [k for k in prev.items if k not in self.items] 240 added = [k for k in self.items if k not in prev.items] 241 updated = [k for k in prev.items if k in self.items 242 and prev.items[k].is_different(self.items[k])] 243 return (removed, added, updated) 244 245 def is_different(self, prev): 246 removed, added, updated = self.diff_messages(prev) 247 return len(removed) != 0 or len(added) != 0 or len(updated) != 0 248 249 250# A deserialized program state. 251class ProgramState(object): 252 def __init__(self, state_id, json_ps): 253 super(ProgramState, self).__init__() 254 logging.debug('Adding ProgramState ' + str(state_id)) 255 256 self.state_id = state_id 257 258 self.store = Store(json_ps['store']) \ 259 if json_ps['store'] is not None else None 260 261 self.environment = \ 262 GenericEnvironment(json_ps['environment']['items']) \ 263 if json_ps['environment'] is not None else None 264 265 self.constraints = GenericMap([ 266 (c['symbol'], c['range']) for c in json_ps['constraints'] 267 ]) if json_ps['constraints'] is not None else None 268 269 self.dynamic_types = GenericMap([ 270 (t['region'], '%s%s' % (t['dyn_type'], 271 ' (or a sub-class)' 272 if t['sub_classable'] else '')) 273 for t in json_ps['dynamic_types']]) \ 274 if json_ps['dynamic_types'] is not None else None 275 276 self.constructing_objects = \ 277 GenericEnvironment(json_ps['constructing_objects']) \ 278 if json_ps['constructing_objects'] is not None else None 279 280 self.checker_messages = CheckerMessages(json_ps['checker_messages']) \ 281 if json_ps['checker_messages'] is not None else None 282 283 284# A deserialized exploded graph node. Has a default constructor because it 285# may be referenced as part of an edge before its contents are deserialized, 286# and in this moment we already need a room for predecessors and successors. 287class ExplodedNode(object): 288 def __init__(self): 289 super(ExplodedNode, self).__init__() 290 self.predecessors = [] 291 self.successors = [] 292 293 def construct(self, node_id, json_node): 294 logging.debug('Adding ' + node_id) 295 self.node_id = json_node['node_id'] 296 self.ptr = json_node['pointer'] 297 self.points = [ProgramPoint(p) for p in json_node['program_points']] 298 self.state = ProgramState(json_node['state_id'], 299 json_node['program_state']) \ 300 if json_node['program_state'] is not None else None 301 302 assert self.node_name() == node_id 303 304 def node_name(self): 305 return 'Node' + self.ptr 306 307 308# A deserialized ExplodedGraph. Constructed by consuming a .dot file 309# line-by-line. 310class ExplodedGraph(object): 311 # Parse .dot files with regular expressions. 312 node_re = re.compile( 313 '^(Node0x[0-9a-f]*) \\[shape=record,.*label="{(.*)\\\\l}"\\];$') 314 edge_re = re.compile( 315 '^(Node0x[0-9a-f]*) -> (Node0x[0-9a-f]*);$') 316 317 def __init__(self): 318 super(ExplodedGraph, self).__init__() 319 self.nodes = collections.defaultdict(ExplodedNode) 320 self.root_id = None 321 self.incomplete_line = '' 322 323 def add_raw_line(self, raw_line): 324 if raw_line.startswith('//'): 325 return 326 327 # Allow line breaks by waiting for ';'. This is not valid in 328 # a .dot file, but it is useful for writing tests. 329 if len(raw_line) > 0 and raw_line[-1] != ';': 330 self.incomplete_line += raw_line 331 return 332 raw_line = self.incomplete_line + raw_line 333 self.incomplete_line = '' 334 335 # Apply regexps one by one to see if it's a node or an edge 336 # and extract contents if necessary. 337 logging.debug('Line: ' + raw_line) 338 result = self.edge_re.match(raw_line) 339 if result is not None: 340 logging.debug('Classified as edge line.') 341 pred = result.group(1) 342 succ = result.group(2) 343 self.nodes[pred].successors.append(succ) 344 self.nodes[succ].predecessors.append(pred) 345 return 346 result = self.node_re.match(raw_line) 347 if result is not None: 348 logging.debug('Classified as node line.') 349 node_id = result.group(1) 350 if len(self.nodes) == 0: 351 self.root_id = node_id 352 # Note: when writing tests you don't need to escape everything, 353 # even though in a valid dot file everything is escaped. 354 node_label = result.group(2).replace('\\l', '') \ 355 .replace(' ', '') \ 356 .replace('\\"', '"') \ 357 .replace('\\{', '{') \ 358 .replace('\\}', '}') \ 359 .replace('\\\\', '\\') \ 360 .replace('\\|', '|') \ 361 .replace('\\<', '\\\\<') \ 362 .replace('\\>', '\\\\>') \ 363 .rstrip(',') 364 logging.debug(node_label) 365 json_node = json.loads(node_label) 366 self.nodes[node_id].construct(node_id, json_node) 367 return 368 logging.debug('Skipping.') 369 370 371# A visitor that dumps the ExplodedGraph into a DOT file with fancy HTML-based 372# syntax highlighing. 373class DotDumpVisitor(object): 374 def __init__(self, do_diffs, dark_mode): 375 super(DotDumpVisitor, self).__init__() 376 self._do_diffs = do_diffs 377 self._dark_mode = dark_mode 378 379 @staticmethod 380 def _dump_raw(s): 381 print(s, end='') 382 383 @staticmethod 384 def _dump(s): 385 print(s.replace('&', '&') 386 .replace('{', '\\{') 387 .replace('}', '\\}') 388 .replace('\\<', '<') 389 .replace('\\>', '>') 390 .replace('\\l', '<br />') 391 .replace('|', '\\|'), end='') 392 393 @staticmethod 394 def _diff_plus_minus(is_added): 395 if is_added is None: 396 return '' 397 if is_added: 398 return '<font color="forestgreen">+</font>' 399 return '<font color="red">-</font>' 400 401 def visit_begin_graph(self, graph): 402 self._graph = graph 403 self._dump_raw('digraph "ExplodedGraph" {\n') 404 if self._dark_mode: 405 self._dump_raw('bgcolor="gray10";\n') 406 self._dump_raw('label="";\n') 407 408 def visit_program_point(self, p): 409 if p.kind in ['Edge', 'BlockEntrance', 'BlockExit']: 410 color = 'gold3' 411 elif p.kind in ['PreStmtPurgeDeadSymbols', 412 'PostStmtPurgeDeadSymbols']: 413 color = 'red' 414 elif p.kind in ['CallEnter', 'CallExitBegin', 'CallExitEnd']: 415 color = 'dodgerblue' if self._dark_mode else 'blue' 416 elif p.kind in ['Statement']: 417 color = 'cyan4' 418 else: 419 color = 'forestgreen' 420 421 if p.kind == 'Statement': 422 # This avoids pretty-printing huge statements such as CompoundStmt. 423 # Such statements show up only at [Pre|Post]StmtPurgeDeadSymbols 424 skip_pretty = 'PurgeDeadSymbols' in p.stmt_point_kind 425 stmt_color = 'cyan3' 426 if p.loc is not None: 427 self._dump('<tr><td align="left" width="0">' 428 '%s:<b>%s</b>:<b>%s</b>:</td>' 429 '<td align="left" width="0"><font color="%s">' 430 '%s</font></td>' 431 '<td align="left"><font color="%s">%s</font></td>' 432 '<td>%s</td></tr>' 433 % (p.loc.filename, p.loc.line, 434 p.loc.col, color, p.stmt_kind, 435 stmt_color, p.stmt_point_kind, 436 p.pretty if not skip_pretty else '')) 437 else: 438 self._dump('<tr><td align="left" width="0">' 439 '<i>Invalid Source Location</i>:</td>' 440 '<td align="left" width="0">' 441 '<font color="%s">%s</font></td>' 442 '<td align="left"><font color="%s">%s</font></td>' 443 '<td>%s</td></tr>' 444 % (color, p.stmt_kind, 445 stmt_color, p.stmt_point_kind, 446 p.pretty if not skip_pretty else '')) 447 elif p.kind == 'Edge': 448 self._dump('<tr><td width="0"></td>' 449 '<td align="left" width="0">' 450 '<font color="%s">%s</font></td><td align="left">' 451 '[B%d] -\\> [B%d]</td></tr>' 452 % (color, 'BlockEdge', p.src_id, p.dst_id)) 453 elif p.kind == 'BlockEntrance': 454 self._dump('<tr><td width="0"></td>' 455 '<td align="left" width="0">' 456 '<font color="%s">%s</font></td>' 457 '<td align="left">[B%d]</td></tr>' 458 % (color, p.kind, p.block_id)) 459 else: 460 # TODO: Print more stuff for other kinds of points. 461 self._dump('<tr><td width="0"></td>' 462 '<td align="left" width="0" colspan="2">' 463 '<font color="%s">%s</font></td></tr>' 464 % (color, p.kind)) 465 466 if p.tag is not None: 467 self._dump('<tr><td width="0"></td>' 468 '<td colspan="3" align="left">' 469 '<b>Tag: </b> <font color="crimson">' 470 '%s</font></td></tr>' % p.tag) 471 472 def visit_environment(self, e, prev_e=None): 473 self._dump('<table border="0">') 474 475 def dump_location_context(lc, is_added=None): 476 self._dump('<tr><td>%s</td>' 477 '<td align="left"><b>%s</b></td>' 478 '<td align="left" colspan="2">' 479 '<font color="gray60">%s </font>' 480 '%s</td></tr>' 481 % (self._diff_plus_minus(is_added), 482 lc.caption, lc.decl, 483 ('(line %s)' % lc.line) if lc.line is not None 484 else '')) 485 486 def dump_binding(f, b, is_added=None): 487 self._dump('<tr><td>%s</td>' 488 '<td align="left"><i>S%s</i></td>' 489 '%s' 490 '<td align="left">%s</td>' 491 '<td align="left">%s</td></tr>' 492 % (self._diff_plus_minus(is_added), 493 b.stmt_id, 494 '<td align="left"><font color="%s"><i>' 495 '%s</i></font></td>' % ( 496 'lavender' if self._dark_mode else 'darkgreen', 497 ('(%s)' % b.kind) if b.kind is not None else ' ' 498 ), 499 b.pretty, f.bindings[b])) 500 501 frames_updated = e.diff_frames(prev_e) if prev_e is not None else None 502 if frames_updated: 503 for i in frames_updated: 504 f = e.frames[i] 505 prev_f = prev_e.frames[i] 506 dump_location_context(f.location_context) 507 bindings_removed, bindings_added = f.diff_bindings(prev_f) 508 for b in bindings_removed: 509 dump_binding(prev_f, b, False) 510 for b in bindings_added: 511 dump_binding(f, b, True) 512 else: 513 for f in e.frames: 514 dump_location_context(f.location_context) 515 for b in f.bindings: 516 dump_binding(f, b) 517 518 self._dump('</table>') 519 520 def visit_environment_in_state(self, selector, title, s, prev_s=None): 521 e = getattr(s, selector) 522 prev_e = getattr(prev_s, selector) if prev_s is not None else None 523 if e is None and prev_e is None: 524 return 525 526 self._dump('<hr /><tr><td align="left"><b>%s: </b>' % title) 527 if e is None: 528 self._dump('<i> Nothing!</i>') 529 else: 530 if prev_e is not None: 531 if e.is_different(prev_e): 532 self._dump('</td></tr><tr><td align="left">') 533 self.visit_environment(e, prev_e) 534 else: 535 self._dump('<i> No changes!</i>') 536 else: 537 self._dump('</td></tr><tr><td align="left">') 538 self.visit_environment(e) 539 540 self._dump('</td></tr>') 541 542 def visit_store(self, s, prev_s=None): 543 self._dump('<table border="0">') 544 545 def dump_binding(s, c, b, is_added=None): 546 self._dump('<tr><td>%s</td>' 547 '<td align="left">%s</td>' 548 '<td align="left">%s</td>' 549 '<td align="left">%s</td>' 550 '<td align="left">%s</td></tr>' 551 % (self._diff_plus_minus(is_added), 552 s.clusters[c].base_region, b.offset, 553 '(<i>Default</i>)' if b.kind == 'Default' 554 else '', 555 s.clusters[c].bindings[b])) 556 557 if prev_s is not None: 558 clusters_removed, clusters_added, clusters_updated = \ 559 s.diff_clusters(prev_s) 560 for c in clusters_removed: 561 for b in prev_s.clusters[c].bindings: 562 dump_binding(prev_s, c, b, False) 563 for c in clusters_updated: 564 bindings_removed, bindings_added = \ 565 s.clusters[c].diff_bindings(prev_s.clusters[c]) 566 for b in bindings_removed: 567 dump_binding(prev_s, c, b, False) 568 for b in bindings_added: 569 dump_binding(s, c, b, True) 570 for c in clusters_added: 571 for b in s.clusters[c].bindings: 572 dump_binding(s, c, b, True) 573 else: 574 for c in s.clusters: 575 for b in s.clusters[c].bindings: 576 dump_binding(s, c, b) 577 578 self._dump('</table>') 579 580 def visit_store_in_state(self, s, prev_s=None): 581 st = s.store 582 prev_st = prev_s.store if prev_s is not None else None 583 if st is None and prev_st is None: 584 return 585 586 self._dump('<hr /><tr><td align="left"><b>Store: </b>') 587 if st is None: 588 self._dump('<i> Nothing!</i>') 589 else: 590 if prev_st is not None: 591 if s.store.is_different(prev_st): 592 self._dump('</td></tr><tr><td align="left">') 593 self.visit_store(st, prev_st) 594 else: 595 self._dump('<i> No changes!</i>') 596 else: 597 self._dump('</td></tr><tr><td align="left">') 598 self.visit_store(st) 599 self._dump('</td></tr>') 600 601 def visit_generic_map(self, m, prev_m=None): 602 self._dump('<table border="0">') 603 604 def dump_pair(m, k, is_added=None): 605 self._dump('<tr><td>%s</td>' 606 '<td align="left">%s</td>' 607 '<td align="left">%s</td></tr>' 608 % (self._diff_plus_minus(is_added), 609 k, m.generic_map[k])) 610 611 if prev_m is not None: 612 removed, added = m.diff(prev_m) 613 for k in removed: 614 dump_pair(prev_m, k, False) 615 for k in added: 616 dump_pair(m, k, True) 617 else: 618 for k in m.generic_map: 619 dump_pair(m, k, None) 620 621 self._dump('</table>') 622 623 def visit_generic_map_in_state(self, selector, title, s, prev_s=None): 624 m = getattr(s, selector) 625 prev_m = getattr(prev_s, selector) if prev_s is not None else None 626 if m is None and prev_m is None: 627 return 628 629 self._dump('<hr />') 630 self._dump('<tr><td align="left">' 631 '<b>%s: </b>' % title) 632 if m is None: 633 self._dump('<i> Nothing!</i>') 634 else: 635 if prev_m is not None: 636 if m.is_different(prev_m): 637 self._dump('</td></tr><tr><td align="left">') 638 self.visit_generic_map(m, prev_m) 639 else: 640 self._dump('<i> No changes!</i>') 641 else: 642 self._dump('</td></tr><tr><td align="left">') 643 self.visit_generic_map(m) 644 645 self._dump('</td></tr>') 646 647 def visit_checker_messages(self, m, prev_m=None): 648 self._dump('<table border="0">') 649 650 def dump_line(l, is_added=None): 651 self._dump('<tr><td>%s</td>' 652 '<td align="left">%s</td></tr>' 653 % (self._diff_plus_minus(is_added), l)) 654 655 def dump_chk(chk, is_added=None): 656 dump_line('<i>%s</i>:' % chk, is_added) 657 658 if prev_m is not None: 659 removed, added, updated = m.diff_messages(prev_m) 660 for chk in removed: 661 dump_chk(chk, False) 662 for l in prev_m.items[chk].lines: 663 dump_line(l, False) 664 for chk in updated: 665 dump_chk(chk) 666 for l in m.items[chk].diff_lines(prev_m.items[chk]): 667 dump_line(l[1:], l.startswith('+')) 668 for chk in added: 669 dump_chk(chk, True) 670 for l in m.items[chk].lines: 671 dump_line(l, True) 672 else: 673 for chk in m.items: 674 dump_chk(chk) 675 for l in m.items[chk].lines: 676 dump_line(l) 677 678 self._dump('</table>') 679 680 def visit_checker_messages_in_state(self, s, prev_s=None): 681 m = s.checker_messages 682 prev_m = prev_s.checker_messages if prev_s is not None else None 683 if m is None and prev_m is None: 684 return 685 686 self._dump('<hr />') 687 self._dump('<tr><td align="left">' 688 '<b>Checker State: </b>') 689 if m is None: 690 self._dump('<i> Nothing!</i>') 691 else: 692 if prev_m is not None: 693 if m.is_different(prev_m): 694 self._dump('</td></tr><tr><td align="left">') 695 self.visit_checker_messages(m, prev_m) 696 else: 697 self._dump('<i> No changes!</i>') 698 else: 699 self._dump('</td></tr><tr><td align="left">') 700 self.visit_checker_messages(m) 701 702 self._dump('</td></tr>') 703 704 def visit_state(self, s, prev_s): 705 self.visit_store_in_state(s, prev_s) 706 self.visit_environment_in_state('environment', 'Environment', 707 s, prev_s) 708 self.visit_generic_map_in_state('constraints', 'Ranges', 709 s, prev_s) 710 self.visit_generic_map_in_state('dynamic_types', 'Dynamic Types', 711 s, prev_s) 712 self.visit_environment_in_state('constructing_objects', 713 'Objects Under Construction', 714 s, prev_s) 715 self.visit_checker_messages_in_state(s, prev_s) 716 717 def visit_node(self, node): 718 self._dump('%s [shape=record,' 719 % (node.node_name())) 720 if self._dark_mode: 721 self._dump('color="white",fontcolor="gray80",') 722 self._dump('label=<<table border="0">') 723 724 self._dump('<tr><td bgcolor="%s"><b>Node %d (%s) - ' 725 'State %s</b></td></tr>' 726 % ("gray20" if self._dark_mode else "gray", 727 node.node_id, node.ptr, node.state.state_id 728 if node.state is not None else 'Unspecified')) 729 self._dump('<tr><td align="left" width="0">') 730 if len(node.points) > 1: 731 self._dump('<b>Program points:</b></td></tr>') 732 else: 733 self._dump('<b>Program point:</b></td></tr>') 734 self._dump('<tr><td align="left" width="0">' 735 '<table border="0" align="left" width="0">') 736 for p in node.points: 737 self.visit_program_point(p) 738 self._dump('</table></td></tr>') 739 740 if node.state is not None: 741 prev_s = None 742 # Do diffs only when we have a unique predecessor. 743 # Don't do diffs on the leaf nodes because they're 744 # the important ones. 745 if self._do_diffs and len(node.predecessors) == 1 \ 746 and len(node.successors) > 0: 747 prev_s = self._graph.nodes[node.predecessors[0]].state 748 self.visit_state(node.state, prev_s) 749 self._dump_raw('</table>>];\n') 750 751 def visit_edge(self, pred, succ): 752 self._dump_raw('%s -> %s%s;\n' % ( 753 pred.node_name(), succ.node_name(), 754 ' [color="white"]' if self._dark_mode else '' 755 )) 756 757 def visit_end_of_graph(self): 758 self._dump_raw('}\n') 759 760 761# A class that encapsulates traversal of the ExplodedGraph. Different explorer 762# kinds could potentially traverse specific sub-graphs. 763class Explorer(object): 764 def __init__(self): 765 super(Explorer, self).__init__() 766 767 def explore(self, graph, visitor): 768 visitor.visit_begin_graph(graph) 769 for node in sorted(graph.nodes): 770 logging.debug('Visiting ' + node) 771 visitor.visit_node(graph.nodes[node]) 772 for succ in sorted(graph.nodes[node].successors): 773 logging.debug('Visiting edge: %s -> %s ' % (node, succ)) 774 visitor.visit_edge(graph.nodes[node], graph.nodes[succ]) 775 visitor.visit_end_of_graph() 776 777 778def main(): 779 parser = argparse.ArgumentParser() 780 parser.add_argument('filename', type=str) 781 parser.add_argument('-v', '--verbose', action='store_const', 782 dest='loglevel', const=logging.DEBUG, 783 default=logging.WARNING, 784 help='enable info prints') 785 parser.add_argument('-d', '--diff', action='store_const', dest='diff', 786 const=True, default=False, 787 help='display differences between states') 788 parser.add_argument('--dark', action='store_const', dest='dark', 789 const=True, default=False, 790 help='dark mode') 791 args = parser.parse_args() 792 logging.basicConfig(level=args.loglevel) 793 794 graph = ExplodedGraph() 795 with open(args.filename) as fd: 796 for raw_line in fd: 797 raw_line = raw_line.strip() 798 graph.add_raw_line(raw_line) 799 800 explorer = Explorer() 801 visitor = DotDumpVisitor(args.diff, args.dark) 802 explorer.explore(graph, visitor) 803 804 805if __name__ == '__main__': 806 main() 807