Interactive Visualization of Abstract Machines for Static Analysis 📊

We present an approach for interactively visualizing static analyses built using the abstracting abstract machines (AAM) methodology—a process that yields a static program analysis by abstract interpretation of an abstract machine. The resulting analysis is a state graph of all possible machine states—with paths through this graph encoding possible executions of the program—combined with a model of the heap. To understand or audit the results of such an analysis (e.g., for debugging or improving the analysis) can become a laborious process of stepping from state to state, building an intuition for each, while considering valid executions that are missing and spurious executions that are included. Finding states relevant to some program property, on its own, can involve writing a custom predicate to match such states at the REPL. In this paper, we explore an approach to concisely visualizing AAM-based analyses of Scheme programs by decomposing the analysis into its functional components and displaying nested graphs for inter- and intra-procedural control flow. We allow interactive visualization in that the user can focus on specific functions or lines of code to discover if they’re reachable, in what contexts, atop what stacks, and with what values bound to variables in scope, in terms of states in an abstract abstract machine. Presenter: Kyle Headly Authors: Kyle Headly, Clark Ren Paper: https://thomas.gilray.org/pdf/viz-aam.pdf Presented at the Scheme workshop 2019: https://icfp19.sigplan.org/home/scheme-2019, part of ICFP'19: icfp19.sigplan.org