ICFP 2022
Sun 11 - Fri 16 September 2022 Ljubljana, Slovenia
Wed 14 Sep 2022 10:50 - 11:10 at Linhart - Compilation Chair(s): Matija Pretnar

We develop the first theory of control-flow graphs from first principles, and use it to create an algorithm for automatically synthesizing many variants of control-flow graph generators from a language’s operational semantics. Our approach first introduces a new algorithm for converting a large class of small-step operational semantics to an abstract machine. It next uses a technique called “abstract rewriting” to automatically abstract the semantics of a language, which is used both to directly generate a CFG from a program (“interpreted mode”) and to generate standalone code, similar to a human-written CFG generator, for any program in a language. We show how the choice of two abstraction and projection parameters allow our approach to synthesize several families of CFG-generators useful for different kinds of tools. We prove the correspondence between the generated graphs and the original semantics. We provide and prove an algorithm for automatically proving the termination of interpreted-mode generators. In addition to our theoretical results, we have implemented this algorithm in a tool called Mandate, and show that it produces human-readable code on two medium-size languages with 60-80 rules, featuring nearly all intraprocedural control constructs common in modern languages. We then show these CFG-generators were sufficient to build two static analyses atop them. Our work is a promising step towards the grand vision of being able to synthesize all desired tools from the semantics of a programming language.

Wed 14 Sep

Displayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change

10:30 - 12:10
CompilationICFP Papers and Events at Linhart
Chair(s): Matija Pretnar University of Ljubljana, Slovenia
10:30
20m
Talk
Beyond Relooper: Recursive Translation of Unstructured Control Flow to Structured Control FlowFunctional Pearl
ICFP Papers and Events
Norman Ramsey Tufts University
DOI
10:50
20m
Talk
Automatically Deriving Control-Flow Graph Generators From Operational Semantics
ICFP Papers and Events
James Koppel Massachusetts Institute of Technology, USA, Jackson Kearl MIT, Armando Solar-Lezama Massachusetts Institute of Technology
DOI
11:10
20m
Talk
Analyzing Binding Extent in 3CPS
ICFP Papers and Events
Benjamin Quiring University of Maryland, Olin Shivers Northeastern University, USA, John Reppy University of Chicago, USA
DOI
11:30
20m
Talk
'do' Unchained: Embracing Local Imperativity in a Purely Functional LanguageFunctional Pearl
ICFP Papers and Events
Sebastian Ullrich Karlsruhe Institute of Technology, Leonardo de Moura Microsoft Research, n.n.
DOI
11:50
20m
Talk
ANF Preserves Dependent Types up to Extensional EqualityJFP Presentation
ICFP Papers and Events
Paulette Koronkevich University of British Columbia, Ramon Rakow University of British Columbia, Amal Ahmed Northeastern University, USA, William J. Bowman University of British Columbia