论文标题
FlowCFL：在存在可变数据的情况下基于类型的可及性分析的框架
FlowCFL: A Framework for Type-based Reachability Analysis in the Presence of Mutable Data
论文作者
论文摘要
可及性分析是具有各种应用的基本程序分析。我们提出FlowCFL，这是在存在可变数据的情况下基于类型的可及性分析的框架。有趣的是，FlowCFL的基本语义是CFL可得出的。 我们做出三项贡献。首先，我们定义了一种动态语义，该语义捕获了可达性分析中常用的流动概念。其次，我们在具有反边缘的图表上建立了CFL可得出的正确性（对于处理可变堆数据是必需的）。我们的方法结合了CFL的可涉及性能和参考不可超数性，以避免增加某些不可行的逆边缘，我们从经验上证明，避免这些边缘会导致精确改善。我们对正确性的正式描述也扩展到了这种情况。第三，我们提出了基于类型的可及性分析，并在某些CFL可得出的分析与基于类型的分析之间建立了等效性，从而证明了基于类型的分析的正确性。
Reachability analysis is a fundamental program analysis with a wide variety of applications. We present FlowCFL, a framework for type-based reachability analysis in the presence of mutable data. Interestingly, the underlying semantics of FlowCFL is CFL-reachability. We make three contributions. First, we define a dynamic semantics that captures the notion of flow commonly used in reachability analysis. Second, we establish correctness of CFL-reachability over graphs with inverse edges (inverse edges are necessary for the handling of mutable heap data). Our approach combines CFL-reachability with reference immutability to avoid the addition of certain infeasible inverse edges and we demonstrate empirically that avoiding those edges results in precision improvement. Our formal account of correctness extends to this case as well. Third, we present a type-based reachability analysis and establish equivalence between a certain CFL-reachability analysis and the type-based analysis, thus proving correctness of the type-based analysis.
