[analyzer][WIP] A Python script to simplify the ExplodedGraph dumps

[Charusso]

Summary

Features:

• Hides duplicated information.
• The full information appears on mouse-hover event.
• Removes extra 'text' tags.

[Charusso]

Pre-alpha release as it is already too huge.

clang/tools/static-analyzer/exploded-graph-rewriter.py

200

Somehow we have to inject those special characters instead. At the moment HTML crashes with errors if they occur.

The spacing and the indentation is another story, I can handle it easily: just I have to inject the string from our representation.

[Charusso]

Example:

node-print-diff.svg6 MBDownload

[NoQ]

I asked you to publish this, but once i saw it, i realized that there are a lot more plans in my had that i already put into my work on this subject. I was imagining a data structure to manipulate graph dumps in more sophisticated manners, like filtering by state data or cutting out specific paths (the latter may be useful even for trimmed graphs), which i already have a more-or-less working sketch for. Therefore i'll ask you to let me in first to initiate this script, and later have you update it with your code.

A few high-level ideas anyway:

• This should go into utils rather than tools, because it's a utility for developers of Clang itself, not a user-facing tool.
• Python scripts in LLVM follow python coding guidelines, such as four spaces indentation.
• We'll have to use difflib or something like that for producing diffs because it's not that trivial. I think you're currently losing the information about when does something disappear from the state, which is often important, so i ideally hope to have a +/- diff-like print.

[Charusso]

clang/tools/static-analyzer/exploded-graph-rewriter.py

61

Solved by D62087.

[Charusso]

By https://github.com/llvm/llvm-project/commit/ee37e28fd1c670ecabea64a15b9cc8698ca62b86 which prevents build-bot and other developer build-break the JSON-support is final.

@NoQ, I am looking forward for that patch!

[Charusso]

It will continue its life as a sub-project of D62761.

clang/tools/static-analyzer/exploded-graph-rewriter.py

+#!/usr/bin/env python
+#
+#==- 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
+#
+#===------------------------------------------------------------------------===#
+
+import argparse
+import json
+import sys
+import subprocess
+import os.path
+
+
+def main():
+  node_parts = ['program_points', 'program_state', 'store', 'environment',
+                'constraints', 'dynamic_types', 'constructing_objects',
+                'checker_messages']
+
+  # Store which parts of the node we would show if they are not empty.
+  node_parts_dot = []
+  for node_part in node_parts:
+    node_parts_dot.append('\\"' + node_part + '\\"')
+
+  # Store what we would adjust with a title.
+  node_parts_svg = node_parts[2:]
+
+  parser = argparse.ArgumentParser(description='Simplifies the ExplodedGraph.')
+  parser.add_argument('-d', '--dot', help='path for the DOT file')
+  args = parser.parse_args()
+  
+  dot_file_full_path = args.dot;
+  dot_file_path, dot_file_name = os.path.split(dot_file_full_path)
+  svg_file_full_path = dot_file_path + '/' + dot_file_name[0:-4] + '-full.svg'
+
+
+  #===----------------------------------------------------------------------===#
+  # Build the JSON graph from the DOT file.
+  #===----------------------------------------------------------------------===#
+
+  graph = {}
+  dot_lines = []
+  with open(dot_file_full_path) as dot_instream:
+    for raw_line in dot_instream:
+      line = raw_line.lstrip('\t').rstrip('\n')
+      dot_lines.append(line)
+
+      # Node - e.g. 'Node0x31f39c0 [shape=record,label="{\{ JSON stuff \}\l}"];'
+      if (is_dot_node(line)):
+        node_id = str_between(line, 'Node', ' [shape=record')
+        label = get_label(line)
+        label = (label.replace('\\"', '"').replace('\\\\', '\\')
+                      .replace('\\{', '{').replace('\\}', '}')
+                      .replace('\\<', '<').replace('\\>', '>')
+                      .replace('&nbsp;', '').replace('\l', '')
+                      .replace('\|', '|'))
+
+        graph[node_id] = json.loads(label.rstrip(',')) # FIXME: remove ','.
+        graph[node_id]['successors'] = []
+        graph[node_id]['predecessors'] = []
+
+      # Edge - e.g. 'Node0x31f39c0 -> Node0x31f3a40;'
+      if (line.startswith('Node') and ' -> ' in line):
+        pred_id = str_between(line, 'Node', ' -> ')
+        succ_id = str_between(line, ' -> Node', ';')
+        graph[pred_id]['successors'].append(str(succ_id))
+
+  # Make the graph bidirectional.
+  for node_id, node in graph.items():
+    for succ_id in node['successors']:
+      graph[succ_id]['predecessors'].append(str(node_id))
+
+
+  #===----------------------------------------------------------------------===#
+  # Simplification of the DOT file.
+  #===----------------------------------------------------------------------===#
+
+  # Simplify each node by removing duplicated informations.
+  dot_simplified = []
+  previous_label_lines = None
+  for line in dot_lines:
+    # If it is not a node just append it.
+    if (not is_dot_node(line)):
+      dot_simplified.append(line)
+      continue
+
+    # Initialize the lines of the previous node.
+    current_label_lines = get_label(line).split('\\l')
+    if (previous_label_lines is None):
+      previous_label_lines = current_label_lines
+      dot_simplified.append(line)
+      continue
+
+    # Add the start of the node.
+    node_start = line[0 : line.find('{')]
+    dot_simplified.append(node_start)
+    for label_line in current_label_lines:
+      # Concatenate new information into the current label.
+      if (label_line not in previous_label_lines):
+        dot_simplified[-1] += label_line + '\l'
+
+      # Also concatenate the parts of the node.
+      for node_part in node_parts_dot:
+        if (node_part in label_line):
+          dot_simplified[-1] += label_line + '\l'
+          break
+
+    # Add the end of the node.
+    dot_simplified[-1] += '}"];'
+
+    previous_label_lines = current_label_lines
+
+
+  #===----------------------------------------------------------------------===#
+  # Write out the simplified DOT.
+  #===----------------------------------------------------------------------===#
+ 
+  dot_diff_path = dot_file_full_path[0:-4] + '-diff.dot'
+  with open(dot_diff_path, 'w') as dot_outstream:
+    for line in dot_simplified:
+      dot_outstream.write('%s\n' % line)
+  
+  # Parse it to an SVG file.
+  subprocess.call(["dot", "-Tsvg", dot_diff_path, "-o", svg_file_full_path])
+
+
+  #===----------------------------------------------------------------------===#
+  # Simplification of the SVG file.
+  #===----------------------------------------------------------------------===#
+
+  # Simplify each node to contain only one 'text' element.
+  svg_simplified = []
+  base_x = 0.0
+  is_node_read = False
+  with open(svg_file_full_path) as svg_instream:
+    for raw_line in svg_instream:
+      line = raw_line.rstrip('\n').replace('&quot;', '\"').replace('\0xc2', '')
+    
+      # If we have ended with reading a node add the ending tag of 'text'.
+      if (is_node_read and line.startswith('</g>')):
+        is_node_read = False
+        svg_simplified.append('</text>')
+
+      # If we do not read a node just append the text.
+      if (not is_svg_node(line)):
+        svg_simplified.append(line)
+        continue
+
+      # Node -  Store the 'x' position of the first 'text' and drop its end tag.
+      # After the first 'text' added replace other 'text' tags with 'tspan' tags
+      # and also replace the spaces with better 'x' positioning.
+      if (not is_node_read):
+        svg_simplified.append(line[0 : line.find('</text>')])
+        is_node_read = True
+        base_x = float(str_between(line, ' x="', '" y='))
+      else:
+        # 'x' is based on the count of spaces, 'y' is relative to its parent.
+        x_offset = line.decode('utf-8').count(u'\xa0') * 4.5
+        new_line = ('<tspan x="' + str(base_x + x_offset) + '" dy="1em">' +
+                    get_text(line) + '</tspan>')
+        svg_simplified.append(new_line)
+
+
+  #===----------------------------------------------------------------------===#
+  # For each part of each node add everything what we know as titles.
+  #===----------------------------------------------------------------------===#
+  
+  svg_titles = []
+  node = None
+  for line in svg_simplified:
+    if (not is_svg_node(line)):
+      svg_titles.append(line)
+      continue
+
+    tspan = get_tspan(line)
+    if ('\"node_id\":' in tspan):
+      node = graph[str_between(tspan, '\"node_id\": "', '\",')]
+
+    # Check whether we have encountered a part of the node.
+    # TODO: Put character-finding to 'str_between'
+    key = tspan[tspan.find('\"') + 1 : tspan.rfind('\"')]
+    if (key not in node_parts_svg):
+      svg_titles.append(line)
+      continue
+
+    # TODO: This is broken as hell.
+    value = node['program_state'][key]
+    # If the current part is not empty add a title to it. Otherwise drop it.
+    if (value is not None):
+      new_line = line[0 : line.find('</tspan>')]
+      new_line += ('<title>' +
+                   json.dumps(value, indent = 2).replace('\"', '&quot;')
+                                                .replace('&', '&amp;')
+                                                .replace('<', '&lt;')
+                                                .replace('>', '&gt;') +
+                   '</title></tspan>')
+      svg_titles.append(new_line)
+
+
+  #===----------------------------------------------------------------------===#
+  # Write out the graph.
+  #===----------------------------------------------------------------------===#
+ 
+  with open(dot_file_full_path[0:-4] + '-diff.svg', 'w') as svg_outstream:
+    for line in svg_titles:
+      svg_outstream.write('%s\n' % line)
+
+
+#===------------------------------------------------------------------------===#
+# Helper functions.
+#===------------------------------------------------------------------------===#
+
+def is_svg_node(line):
+  return (line.startswith('<text text-anchor="start"') or
+          line.startswith('<tspan '))
+
+def is_dot_node(line):
+  return line.startswith('Node') and ' -> ' not in line
+
+def get_label(line):
+  return line[line.find('{') + 1 : -4];
+
+def get_tspan(line):
+  return str_between(line, '">', '</tspan>')
+
+def get_text(line):
+  return str_between(line, '">', '</text>').decode('utf-8').replace(u'\xa0', '')
+
+def str_between(line, before_str, after_str):
+  return line[line.find(before_str) + len(before_str) : line.find(after_str)]
+
+if __name__ == '__main__':
+  main()