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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Full Control-Flow Sensitivity for Definitional Interpreters

  • Kimball Germane

摘要

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.