An efficient approach to computing fixpoints for complex program analysis
An efficient approach to computing fixpoints for complex program analysis
复制标题
一种计算复杂程序分析不动点的有效方法
DOI：
10.1145/181181.181308
复制
发表时间：
1994
期刊：
影响因子：
--
通讯作者：
W. Harrison
中科院分区：
文献类型：
--
作者：
Lilei Chen;W. Harrison
使用抽象解释的程序分析效率低下的主要来源来自以下事实：在分析过程中，大量环境（即问题状态）从节点传播到节点。我们称之为上下文投影的技术可以解决此问题，并在很大程度上可以缓解该问题，该技术向实际相关的部分投射了一个节点的输入上下文，并确定是否应基于预测的上下文对节点进行重新评估。该技术降低了评估的成本，并消除了不必要的评估。因此，计算固定点在一般晶格上的效率大大提高了。提出了一种特定方法，即可及性，以实现上下文投影的示例。使用可及性的实验结果表明，非常有说服力的加速度（超过八个较大的程序），证明了上下文投影的实际意义。
A chief source of inefficiency in program analysis using abstract interpretation comes from the fact that a large context (i.e., problem state) is propagated from node to node during the course of an analysis. This problem can be addressed and largely alleviated by a technique we call context projection, which projects an input context for a node to the portion that is actually relevant and determines whether the node should be reevaluated based on the projected context. This technique reduces the cost of an evaluation and eliminates unnecessary evaluations. Therefore, the efficiency of computing fixpoints over general lattices is greatly improved. A specific method, reachability, is presented as an example to accomplish context projection. Experimental results using reachability show very convincing speedups (more than eight for larger programs) that demonstrate the practical significance of context projection.