From 43a8b01211e479a2978e15786d3d2786ffbbad95 Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Fri, 18 Dec 2015 18:28:58 -0500 Subject: [PATCH] feat(extra/depgraph): add dependency graph script --- extras/depgraph/README.md | 27 +++++ extras/depgraph/leandeps.py | 203 ++++++++++++++++++++++++++++++++++++ 2 files changed, 230 insertions(+) create mode 100644 extras/depgraph/README.md create mode 100644 extras/depgraph/leandeps.py diff --git a/extras/depgraph/README.md b/extras/depgraph/README.md new file mode 100644 index 000000000..8649fa4a1 --- /dev/null +++ b/extras/depgraph/README.md @@ -0,0 +1,27 @@ +Generating Dependency Graph +============================ + +Usage: + + leandeps.py [options] dir/file + +If argument is a directory, all source files below that directory will be included in the graph. + + - `-h`/`--help` : prints this message + - `-o `/`--output ` : saves the DOT output in the specified file + +If no output file is specified, `deps.gv` and `deps.gv.dot` is written to. + +You need the [graphviz python library][python-graphviz]. If you already have [pip][pip], you can do: + + pip install graphviz + +The resulting `deps.gv.dot` file can be run through [dot][graphviz] (and maybe tred first) from graphviz to produce, +e.g., an svg file. For example: + + tred deps.gv.dot > treddeps.dot + dot -Tsvg -O treddeps.dot + +[python-graphviz]: https://pypi.python.org/pypi/graphviz +[graphviz]: http://www.graphviz.org/ +[pip]: https://pip.readthedocs.org/en/stable/installing/#install-pip diff --git a/extras/depgraph/leandeps.py b/extras/depgraph/leandeps.py new file mode 100644 index 000000000..9dd6867cc --- /dev/null +++ b/extras/depgraph/leandeps.py @@ -0,0 +1,203 @@ +#!/usr/bin/env python +# -*- coding: utf-8 -*- +# +# Copyright (c) 2015 Microsoft Corporation. All rights reserved. +# Released under Apache 2.0 license as described in the file LICENSE. +# +# Authors: Soonho Kong, Leonardo de Moura, Ulrik Buchholtz + +# Python 2/3 compatibility +from __future__ import print_function + +import os +import sys +import getopt +import subprocess +import platform +import graphviz + +g_lean_exec_name = "lean" +if platform.system() == "Windows" or platform.system().startswith("MSYS"): + g_lean_exec_name = "lean.exe" + +if platform.system().startswith("MSYS"): + # In MSYS platform, realpath has a strange behavior. + # os.path.realpath("c:\a\b\c") => \:\a\b\c + g_leanutil_path = os.path.abspath(os.path.normpath(__file__)) +else: + g_leanutil_path = os.path.abspath(os.path.realpath(__file__)) + +g_lean_bin_dir = os.path.dirname(g_leanutil_path) + +g_lean_dir = os.path.dirname(g_lean_bin_dir) + +g_lean_path = os.path.join(g_lean_bin_dir, g_lean_exec_name) + +if not os.path.isfile(g_lean_path): + error("cannot find lean executable at " + os.path.abspath(g_lean_path)) + +class lean_exception(Exception): + def __init__(self, value): + self.value = value + def __str__(self): + return repr(self.value) + +def normalize_drive_name(name): + if platform.system() == "Windows": + drive, path = os.path.splitdrive(name) + if drive == None: + return name + else: + # Leo: return drive.lower() + path + return path + else: + return name + +def is_olean(fname): + return fname.endswith(".olean") + +def is_lean(fname): + return fname.endswith(".lean") + +def is_hlean(fname): + return fname.endswith(".hlean") + +LEAN_KIND=0 +HLEAN_KIND=1 +OLEAN_KIND=2 + +def get_lean_file_kind(fname): + if is_lean(fname): + return LEAN_KIND + elif is_hlean(fname): + return HLEAN_KIND + elif is_olean(fname): + return OLEAN_KIND + else: + raise lean_exception("unknown file kind: " + fname) + +def olean_to_lean(fname, kind): + if kind == LEAN_KIND: + return fname[:-5] + "lean" + elif kind == HLEAN_KIND: + return fname[:-5] + "hlean" + else: + raise lean_exception("unsupported file kind: " + kind) + +def lean_to_olean(fname): + if is_lean(fname): + return fname[:-4] + "olean" + elif is_hlean(fname): + return fname[:-5] + "olean" + else: + raise lean_exception("file '%s' is not a lean source file" % fname) + +def get_timestamp(fname): + try: + return os.path.getmtime(fname) + except OSError: + return 0 + +def is_uptodate(fname): + return get_timestamp(lean_to_olean(fname)) > get_timestamp(fname) + +def lean_direct_deps(lean_file): + deps = [] + proc = subprocess.Popen([g_lean_path, "--deps", lean_file], + stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + output = proc.communicate()[0].decode('utf-8').replace('\r\n', '\n') + if not proc.returncode == 0: + raise lean_exception(str(output)) + for olean_file in output.strip().splitlines(): + if olean_file: + deps.append(normalize_drive_name(os.path.abspath(olean_file))) + return deps + +def get_lean_prefixes(): + paths = [] + proc = subprocess.Popen([g_lean_path, "--path"], + stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + output = proc.communicate()[0].decode('utf-8').replace('\r\n', '\n') + if not proc.returncode == 0: + raise lean_exception(str(output)) + for p in output.rstrip().split(':'): + paths.append(os.path.normpath(os.path.abspath(p))) + proc = subprocess.Popen([g_lean_path, "--hlean", "--path"], + stdout=subprocess.PIPE, stderr=subprocess.STDOUT) + output = proc.communicate()[0].decode('utf-8').replace('\r\n', '\n') + if not proc.returncode == 0: + raise lean_exception(str(output)) + for p in output.rstrip().split(':'): + paths.append(os.path.normpath(os.path.abspath(p))) + return paths + +def lean_to_module(fname, prefixes): + root, ext = os.path.splitext(fname) + for prefix in prefixes: + if root.startswith(prefix): + root = root[len(prefix)+1:] + break + return root.replace(os.sep, '.') + +def lean_deps_core(lean_files, prefixes, visited, graph): + for lean_file in lean_files: + kind = get_lean_file_kind(lean_file) + if not lean_file in visited: + visited[lean_file] = True + graph.node(lean_to_module(lean_file, prefixes)) + for d in lean_direct_deps(lean_file): + d = os.path.normpath(os.path.abspath(str(d))) + if is_olean(d): + d = olean_to_lean(d, kind) + graph.edge(lean_to_module(lean_file, prefixes), lean_to_module(d, prefixes)) + lean_deps_core([d], prefixes, visited, graph) + +def lean_deps(lean_files, prefixes, oname): + visited = dict() + graph = graphviz.Digraph(name=oname,format='dot') + lean_deps_core(lean_files, prefixes, visited, graph) + graph.render() + +def usage(): + print('Usage: '+sys.argv[0]+' [options] dir/file') + print("\nIf argument is a directory, all source files below that directory") + print("will be included in the graph.") + print("\n -h/--help : prints this message") + print(" -o/--output file : saves the DOT output in the specified file") + print("If no output file is specified, deps.gv and deps.gv.dot is written to.") + +def main(argv): + oname = "deps" + try: + opts, args = getopt.getopt(argv, "ho:", ["help","output="]) + except getopt.GetoptError as err: + print(str(err)) + usage() + sys.exit(2) + for opt, arg in opts: + if opt in ("-h", "--help"): + usage() + sys.exit() + elif opt in ("-o", "--output"): + oname = arg + if len(args) != 1: + print(" Input argument required!") + usage() + sys.exit(2) + leanfiles = [] + prefixes = get_lean_prefixes() + if os.path.isdir(args[0]): + for root, dirs, files in os.walk(args[0]): + for name in files: + if is_lean(name) or is_hlean(name): + leanfiles.append(os.path.abspath(os.path.normpath(os.path.join(root, name)))) + prefixes.append(os.path.abspath(os.path.normpath(root))) + elif is_lean(args[0]) or is_hlean(args[0]): + leanfiles = [os.path.abspath(os.path.normpath(args[0]))] + else: + usage() + sys.exit(2) + lean_deps(leanfiles, prefixes, oname) + +if __name__ == "__main__": + main(sys.argv[1:]) \ No newline at end of file