Index: clang/tools/static-analyzer/exploded-graph-rewriter.py =================================================================== --- /dev/null +++ clang/tools/static-analyzer/exploded-graph-rewriter.py @@ -0,0 +1,236 @@ +#!/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(' ', '').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('"', '\"').replace('\0xc2', '') + + # If we have ended with reading a node add the ending tag of 'text'. + if (is_node_read and line.startswith('')): + is_node_read = False + svg_simplified.append('') + + # 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('')]) + 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 = ('' + + get_text(line) + '') + 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('')] + new_line += ('' + + json.dumps(value, indent = 2).replace('\"', '"') + .replace('&', '&') + .replace('<', '<') + .replace('>', '>') + + '') + 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(' ' not in line + +def get_label(line): + return line[line.find('{') + 1 : -4]; + +def get_tspan(line): + return str_between(line, '">', '') + +def get_text(line): + return str_between(line, '">', '').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()