Arithmetic Strengthening for Shape Analysis
Arithmetic Strengthening for Shape Analysis
复制标题
形状分析的算术强化
DOI：
10.1007/978-3-540-74061-2_26
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
B. Cook
中科院分区：
文献类型：
--
作者：
Stephen Magill;Josh Berdine;E. Clarke;B. Cook
形状分析在其数值推理中通常是不精确的，而数值静态分析通常在很大程度上不知道程序堆的形状。本文提出了一种将基于分离逻辑的形状分析与任意算术分析相结合的惰性方法。当我们的形状分析报告了潜在的虚假反例时，该方法构建了一个纯算术程序，其轨迹过于近似于反例轨迹集。然后将该算法程序与算法分析相结合，构建了形状分析的精化算法。我们的方法旨在证明需要对堆进行综合推理和更有针对性的算术推理的性质。给定足够的前提条件，我们的技术可以自动证明程序的内存安全性，这些程序的无错误操作取决于形状、大小和整数不变量的组合。我们已经实现了我们的算法，并使用各种算术分析工具在许多常见的列表例程上对其进行了测试。
Shape analyses are often imprecise in their numerical reasoning, whereas numerical static analyses are often largely unaware of the shape of a program's heap. In this paper we propose a lazy method of combining a shape analysis based on separation logic with an arbitrary arithmetic analysis. When potentially spurious counterexamples are reported by our shape analysis, the method constructs a purely arithmetic program whose traces over-approximate the set of counterexample traces. It then uses this arithmetic program together with the arithmetic analysis to construct a refinement for the shape analysis. Our method is aimed at proving properties that require comprehensive reasoning about heaps together with more targeted arithmetic reasoning. Given a sufficient precondition, our technique can automatically prove memory safety of programs whose error-free operation depends on a combination of shape, size, and integer invariants. We have implemented our algorithm and tested it on a number of common list routines using a variety of arithmetic analysis tools for refinement.