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.