Interactive Abstract Interpretation with Demanded Summarization

We consider the problem of making expressive, interactive static analyzers compositional. Such a technique could help bring the power of server-based static analyses to integrated development environments (IDEs), updating their results live as the code is modified. Compositionality is key for this scenario, as it enables reuse of already-computed analysis results for unmodified code. Previous techniques for interactive static analysis either lack compositionality, cannot express arbitrary abstract domains, or are not from-scratch consistent. We present demanded summarization, the first algorithm for incremental compositional analysis in arbitrary abstract domains that guarantees from-scratch consistency. Our approach analyzes individual procedures using a recent technique for demanded analysis, computing summaries on demand for procedure calls. A dynamically updated summary dependency graph enables precise result invalidation after program edits, and the algorithm is carefully designed to guarantee from-scratch-consistent results after edits, even in the presence of recursion and in arbitrary abstract domains. We formalize our technique and prove soundness, termination, and from-scratch consistency. An experimental evaluation of a prototype implementation on synthetic and real-world program edits provides evidence for the feasibility of this theoretical framework, showing potential for major performance benefits over non-demanded compositional analyses.

我们考虑的问题，表达，交互式静态分析器组成。这样的技术可以帮助将基于服务器的静态分析的力量带到集成开发环境（IDE）中，并在代码修改时实时更新其结果。组合性是此场景的关键，因为它支持为未修改的代码重用已计算的分析结果。以前的交互式静态分析技术要么缺乏组合性，不能表达任意的抽象域，要么不是从头开始一致的。我们提出了要求的总结，第一个算法的增量成分分析在任意的抽象域，保证从头开始的一致性。我们的方法分析了个别程序，使用最近的技术要求分析，计算程序调用的需求摘要。动态更新的摘要依赖图可以在程序编辑后实现精确的结果无效，并且该算法经过精心设计，即使在递归和任意抽象域中，也可以在编辑后保证从头开始一致的结果。我们正式我们的技术和证明的合理性，终止，从零开始的一致性。合成和现实世界的程序编辑的原型实现的实验评估提供了这种理论框架的可行性的证据，表现出潜在的主要性能优势，在非必需的成分分析。