Relatively Complete Pushdown Analysis of Escape Continuations
Escape continuations are weaker than full, first-class continuations but nevertheless can express many common control operators. Although language and compiler designs profitably leverage escape continuations, all previous approaches to analyze them statically in a higher-order setting have been ad hoc or imprecise. We present MCCFA2, a generalization of CFA2 that analyzes them with pushdown precision in their most-general form. In particular, the summarization algorithm of MCCFA2 is both sound and complete with respect to a conservative extension of CFA2’s abstract semantics. We also sketch an integration into our framework of Vardoulakis and Shivers’ technique to handle first-class continuations that offers the full precision of MCCFA2 to uses of them as mere escape continuations.
Sun 13 JanDisplayed time zone: Belfast change
16:00 - 17:30 | Abstract Interpretation (2)VMCAI at Sala III Chair(s): Mihaela Sighireanu IRIF, University Paris Diderot and CNRS, France | ||
16:00 30mTalk | Demand Control-Flow Analysis VMCAI Kimball Germane University of Utah, Jay McCarthy University of Massachusetts Lowell, Michael D. Adams University of Utah, Matthew Might University of Alabama at Birmingham | Harvard Medical School | ||
16:30 30mTalk | Effect-driven Flow Analysis VMCAI Jens Nicolay Vrije Universiteit Brussel, Belgium, Quentin Stiévenart Vrije Universiteit Brussel, Belgium, Wolfgang De Meuter Vrije Universiteit Brussel, Coen De Roover Vrije Universiteit Brussel | ||
17:00 30mTalk | Relatively Complete Pushdown Analysis of Escape Continuations VMCAI Kimball Germane University of Utah, Matthew Might University of Alabama at Birmingham | Harvard Medical School |