Synthesizing Control-Flow Graph Generators from Operataional Semantics


Theoretically, given a complete semantics of a programming language, one should be able to automatically generate all desired tools. In this work, we take a first step towards that vision by automatically synthesizing many variants of control-flow graph generators from operational semantics, and prove a formal correspondence between the generated graphs and a language’s semantics. The first half of our approach is a new algorithm for converting a large class of small-step operational semantics to abstract machines. The second half builds a CFG generator by using “abstract rewriting” to automatically abstract the semantics of a language. The final step generates a graph describing the control flow of all instantiations of each node type, from which the tool generates concise code that can generate a CFG for any program. We implement this approach in a tool called Mandate, and show that it can generate many types of control-flow graph generators for two realistic languages drawn from compilers courses.

In submission
James Koppel
Ph. D. Candidate