Full Control-Flow Sensitivity for Definitional Interpreters
Static analyzers can exhibit a variety of control-flow sensitivities, including path and flow sensitivity. Darais et al. provide an account of these sensitivities rooted in “control properties of the interpreter” for static analyzers that model program behavior as a finite-state transition system. In the meantime, many static analyzer frameworks—particularly those for higher-order languages—have migrated to more sophisticated and precise pushdown models which admit evaluation summaries. It is not immediately clear how to realize the full spectrum of path and flow sensitivity in a summary-based setting which, like that of Darais et al., is rooted in the control properties of the interpreter and therefore independent of all other aspects of the analyzer formulation. We present a framework which achieves precisely this. We also provide a caching algorithm which performs summarization and demonstrate the framework on an abstract definitional interpreter. Altogether, we show how to achieve the full range of path and flow sensitivities, even at once, within a single abstract definitional interpreter-based analysis, completely independent of other aspects of its formulation.
Sun 20 OctDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:30 | Types, Control-flow and trace partitioningSAS at San Gabriel Chair(s): Michele Pasqua University of Verona | ||
11:00 30mFull-paper | BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code SAS Ian Smith Trail of Bits Pre-print | ||
11:30 30mFull-paper | Full Control-Flow Sensitivity for Definitional Interpreters SAS Kimball Germane Brigham Young University Pre-print | ||
12:00 30mFull-paper | Trace Partitioning as an Optimization Problem SAS Charles Babu M CEA-List, Matthieu Lemerre Université Paris-Saclay - CEA LIST, Sébastien Bardin CEA LIST, University Paris-Saclay, Jean-Yves Marion LORIA Pre-print |