Compositional Shape Analysis by Means of Bi-Abduction
Compositional Shape Analysis by Means of Bi-Abduction
复制标题
DOI：
10.1145/2049697.2049700
复制
发表时间：
2011-12-01
影响因子：
2.5
通讯作者：
Yang, Hongseok
中科院分区：
文献类型：
--
作者：
Calcagno, Cristiano;Distefano, Dino;Yang, Hongseok
可变数据结构的准确和有效处理是自动程序验证和分析中出色的问题领域之一。形状分析是一种程序分析的一种形式，试图推断程序中数据结构的描述，并证明这些结构没有被滥用或损坏。由于混叠的复杂性以及需要深入研究程序堆的需求，因此它是更具挑战性和昂贵的计划分析形式之一。本文描述了一种通过定义组成方法来增强形状分析的方法，其中每个过程都独立于呼叫者分析。分析算法使用限制性分离逻辑的限制片段，并将HOARE三元组的集合分配给每个过程；这些三元组提供了数据结构使用情况的过度评价。我们的方法带来了构成性的扩展潜力，处理不完整程序的能力，首次处理不精确的形状分析的能力。该分析基于绑架的广义形式（解释性假设的推断），我们称之为双性恋。双重侵蚀显示绑架是框架问题的一种反面：它共同侵入反框架（缺少状态的部分）和框架（状态的一部分不受操作触摸），并且是新分析算法的基础。我们已经实施了分析，并报告了有关较小程序的案例研究，以评估发现规格的质量和较大的代码库（例如SendMail，IMAP服务器，Linux分发），以说明我们从我们的组成方法。本文在证明程序和分析算法上做出了许多特定的技术贡献，但从某种意义上说，其更重要的贡献是整体：使用外观推断，解释和证明了如何进行自动化大量增加。
The accurate and efficient treatment of mutable data structures is one of the outstanding problem areas in automatic program verification and analysis. Shape analysis is a form of program analysis that attempts to infer descriptions of the data structures in a program, and to prove that these structures are not misused or corrupted. It is one of the more challenging and expensive forms of program analysis, due to the complexity of aliasing and the need to look arbitrarily deeply into the program heap. This article describes a method of boosting shape analyses by defining a compositional method, where each procedure is analyzed independently of its callers.The analysis algorithm uses a restricted fragment of separation logic, and assigns a collection of Hoare triples to each procedure; the triples provide an over-approximation of data structure usage. Our method brings the usual benefits of compositionality-increased potential to scale, ability to deal with incomplete programs, graceful way to deal with imprecision-to shape analysis, for the first time. The analysis rests on a generalized form of abduction (inference of explanatory hypotheses), which we call bi-abduction. Bi-abduction displays abduction as a kind of inverse to the frame problem: it jointly infers anti-frames (missing portions of state) and frames (portions of state not touched by an operation), and is the basis of a new analysis algorithm. We have implemented our analysis and we report case studies on smaller programs to evaluate the quality of discovered specifications, and larger code bases (e.g., sendmail, an imap server, a Linux distribution) to illustrate the level of automation and scalability that we obtain from our compositional method.This article makes number of specific technical contributions on proof procedures and analysis algorithms, but in a sense its more important contribution is holistic: the explanation and demonstration of how a massive increase in automation is possible using abductive inference.