模块化程序分析框架：共享信息的一阶逻辑自动化插件的应用

理论计算机科学电子笔记145（2006）131-150www.elsevier.com/locate/entcs使用交互分析插件纳撒尼尔·查尔顿1英国伦敦帝国理工学院南肯辛顿校区计算机系，邮编：SW7 2AZ摘要在本文中，我们提出了一个模块化的框架，程序分析，多个程序分析工具相结合，以利用每个特定的优势。这允许将每个核查任务所需的这些工具“插在一起”，并使新的分析易于整合。我们的框架使用具有传递闭包的一阶逻辑自动化插件之间的信息共享，其方式受到Cortesi等人的开放产品的启发。我们展示了如何使用我们的框架进行静态断言检查，通过调整Ball和Rajamani的过程间数据流分析。我们描述了我们的实现的原型检查器的Java的一个子集，它结合了谓词抽象，3值形状分析和可判定指针分析。我们通过一个例子证明了我们的方法可以提供的精度的增加。保留字：抽象，软件验证，开放产品1介绍状态模型检验是一种广泛使用的形式化验证方法，其中一种方法是创建某个系统行为的有限模型因为所有可达状态都被检查，模型检查提供了非常强的正确性保证。基于BDD的有效的国家[3]。模型检验的传统目标是控制系统和通信协议。1我是：纳撒尼尔。查尔斯·托恩@i mp eri al。联合王国1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.009132N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131但随着应用程序的规模和复杂性的不断增加，确保其可靠性的方法至关重要。因此，毫不奇怪，最近的工作已经探索了该技术在用Java等语言编写的无限状态软件中关键在于抽象的过程：从源程序中我们产生一个近似的抽象程序，它省略了原始程序的一些细节，但具有有限状态行为，因此可以进行模型检查。为了获得有意义的结果，我们坚持我们的抽象程序是原始程序的保守近似或模拟，即真实程序中的所有执行路径在抽象系统中都是可能的（可能更多）。这确保了在抽象系统上检查的安全属性抽象解释[6]提供了必要的理论框架来证明这种分析是正确的。以这种方式检查软件已经取得了一些成功：例如，可以验证设备驱动程序，垃圾收集器和实现数据结构的库。众所周知的抽象方法包括区间分析、预测抽象[2]、形状分析[16]、线性规划抽象和各种指针分析，例如[19]。但是，尽管这些方法中的每一种都能很好地用于特定类别的程序和属性，但它们都有因此，由普通程序员编写的“真正的”（应用程序）程序仍然问题是设计抽象方案是困难的：保留太多不相关的信息会导致高计算成本，但如果相关的事实被丢弃，就不可能验证所需的属性。贡献在本文中，我们提出了一个基于抽象的程序验证的模块化框架，其中多个程序分析工具相结合，以利用和放大每个特定的优势这允许分析的不同子集根据每个验证任务的要求“插入”在一起，并且易于集成新的理论上已知，由于每个分析产生的结果通常不是独立的，因此一次性使用它们可以给出比单独运行每个分析更精确但这些交互可能是微妙的，因此实现起来既困难又耗时。我们框架的一个关键方面是我们寻求自动利用这种交互：受Cortesi等人的开放产品[5]的启发，我们允许我们的插件使用具有传递闭包的一阶逻辑N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131133文件概要第二节简要介绍了我们工作的相关背景在第3节中，我们正式定义了我们的框架，并讨论了我们使用的过程间分析算法第4节描述了我们为Java的一个子集实现的原型类型断言检查器，它结合了三种技术的插件：谓词抽象，3值形状分析和可判定指针分析（分别如[2，16，19第5节跟踪我们的断言检查器在Java代码示例片段上的执行情况，展示了我们的方法可以提供的精度的提高2背景2.1摘要解释和核实抽象解释理论[6]是抽象的一般形式框架。它规定了抽象方案应该满足的条件，并提供了各种结果和算法，只要这些满足，就可以应用。考虑一个只有一个整数变量的程序程序在任何执行点的状态都是Z的元素，在任何特定程序点可达的可能状态集是完整格P（Z）的元素找到每个程序点的可达状态集需要迭代的最小固定点计算，但这可能永远不会终止，因为P（Z）是无限的。抽象解释告诉我们用有限（或有限高）格L近似P（Z），在那里我们将保证终止。一个这样的格是图1（左）中所示的符号抽象格L符号+ 0 −偶数奇数Fig. 1. 符号与奇偶抽象格其思想是元素{+，0，-}保留整数变量的符号，同时丢弃其确切值。图1右侧的奇偶晶格类似，只记录整数是偶数还是奇数。通过给出一个具体化函数γ，在这种情况下，一个L符号→P（Z）类型的函数，给抽象格的元素赋予了精确的含义γ（+）={n：n > 0}γ（0）={0}γ（T）= Zγ（−）={n：n 0}γ（）=134N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131从γ我们定义抽象函数α：P（Z）→ L符号，它将每个具体状态集映射到其最佳抽象表示。例如，α（{1， 2}）=+，但α（{0， 1， 2}）=T。诸如赋值之类的指令在具体状态空间上表达传递函数例如，传递函数f：Z→Z是这样的：hx：=x-1是f（n）=n−1。我们将抽象传递函数f#与each这样的f相关联，该抽象传递函数f#对矩阵e进行运算并模仿f的运算。对于x：=x-1，我们可以f#（+）=Tf#（0）=−f#（T）=Tf#（−）=−f#（）=这些抽象传递函数产生一个抽象转移系统，它（在nγ和f#s的适当安全条件下）是程序真实行为的一个自适应逼近现在，我们可以搜索抽象转换系统，寻找通向“坏”或错误状态的路径。在同等条件下-我们可以通过将每个断言转换为测试断言条件的代码来进行断言检查，并在断言失败时跳转到一个特殊的错误标签在看到了一般框架之后，我们现在考虑抽象方案的一些具体情况。2.2谓词抽象谓词抽象的思想是将具体的程序状态分组为等价类，这些等价类基于它们赋予有限的谓词。我们选择抽象谓词P1，. .. bn在哪里⎧如果为s，则为1 |= Pibi=00ifs $Pi位向量b1，...，bn是满足公式1.1的状态集合。 其中，如果bi= 1，则i是Pi，如果bi= 0，则i是Pi这样的公式称为单项式。这些之间的过渡抽象状态可以使用用于编程语言的最弱前提条件生成器和用于其中写入Φ i的逻辑的满足性检查器来计算因此，谓词抽象将模型检查与通过定理证明的验证相结合。SLAM[2]（现在是微软静态驱动验证器[ 18 ]的基础）和类似的BLAST [ 9 ]实现了C程序的谓词抽象。递归是通过构造每个过程的摘要来正确处理的，N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131135然后在所有呼叫站点之间共享这些工具在控制主导的程序（如设备驱动程序）上工作得很好，并且不需要用户提供不变量，但是当涉及到操纵链接数据结构（如链表和树）的程序时，这些工具是无效的为了有效地处理这样的结构，我们需要推理对象图中的可达性：例如，当将节点n众所周知，SLAM和BLAST所基于的一阶逻辑无法表达这些属性。在下一小节中，我们将研究一种描述对象图的方法，即使用具有可达性运算符的逻辑其他方法包括graph gram- mars [7]和使用明智选择的局部不变量和2.3描述对象图我们可以通过允许以下形式的传递闭包公式来TC[a，b][Φ（a，b）]（x，y）这是真的，只有当有一些有限的点序列开始于x和结束于y，这样，对于每个点a序列中的点b后，它满足Φ（a，b）。由此产生的逻辑称为具有传递闭包的一阶逻辑，或FO（TC）[22]。FO（TC）是理想的，因为它非常有表现力;我们可以编写如下条件：• 只有从x通过场可传递到达的对象才修改了它们的场（在这里和全文中，x0表示x的先前值）：select（g，o）select（go，o）→TC[a，b][select（f，a）=b]（x，o）虽然FO（TC）没有完整的证明过程，但最近的工作[15]表明，可以使用一阶定理证明器对FO（TC）进行有效的推理，方法是选择一组一阶公理，这些公理充分描述了传递闭包。或者，人们可以玩一个习惯的游戏，仔细地限制逻辑和/或模型类，希望找到一个逻辑，它是可判定的，但足够有表达力，是有价值的。已知多种具有可达性的可判定逻辑，例如• WS2S，本质上是一个弱的二阶树逻辑[11]，只能处理树型模型，具有很高的复杂性，但表达能力很强第2.4节中讨论的指针断言逻辑引擎（PALE）基于WS2S。• 树（DTC+[E]）[10]是FO（TC）的可判定基，其中e都不取单个二元关系符号E的传递闭包，它的主要优点是可以描述比树更一般的数据结构。136N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131• 保护固定点逻辑μGF[8]（包括模态μ-演算）也可以处理更一般的数据结构，但只能表达有限的可达性。这里没有探讨的一个问题是，在这些逻辑中，我们可以为程序语句导出最弱的先决条件，而在一些逻辑中我们不能。然而第三种方法是完全避免定理证明和决策过程，并采取基于模型的方法，使用3值模型来表示2值模型的集合这就是第1.1节中讨论的TVLA系统2.5工作。2.4苍白指针断言逻辑引擎（PALE）[19]用于验证操作图形类型数据结构的过程保持其一致性。图类型数据结构[19]由一些非循环树主干组成，这些主干由一些由数据类型不变式管理的行为良好的“额外”指针扩展带有指向最后一个节点的指针的链表是一种图形类型，就像二叉树一样，其中的叶子被串入循环列表。图类型存储可以方便地编码为树逻辑WS2S的模型PALE接受类似C语言的程序，忽略算术语句。程序员必须为所使用的每种类型提供循环不变式和特殊的图形类型声明，例如以下链表：类型Node ={ boolvalue;data next：Node;指针prev：Node[this^Node.next={prev}];}在这里，指针，由公式约束为“下一个”字段的逆PALE在WS2S中生成验证条件并将其发送到MONA工具[11] 用自动机来决定它们因此2.5TVLATVLA [16]，三值逻辑分析器，类似于PALE，因为它是一个用于跟踪对象图形形状的系统，抽象出数据字段，如整数。TVLA只给出近似结果，而PALE是完全精确的，但另一方面，它可以处理任意对象图N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131137并且可以推断循环不变量，从而不需要提供这些不变量TVLA将对象图视为具有一元和二元谓词的谓词逻辑的模型。解释域表示已分配对象的集合。对于每个（对象类型的）程序变量v，都有一个一元谓词V，它只在v所指向的对象处成立类似地，指针字段由二元谓词表示。下v图二.一个抽象堆，表示一个长度为3或更长的链表，v指向第一个或第二个元素，或空为了给出指令I的语义，我们为I改变的每个谓词提供更新规则这些规则在执行I之后根据谓词的值预先表达谓词的值，并且可以使用传递闭包。例如v：= u.f有更新规则V（o）=p（U（p）<$F（p，o））。抽象是通过转移到三值逻辑来实现的，在三值逻辑中，除了通常的真和假之外，还有一个额外的真值未知。在抽象状态中，如图2所示，谓词可以采用unknown值，如虚线所示。摘要节点用双圆绘制，表示一个或多个具体节点的整个组。图2中的抽象堆表示长度为3或更长的所有链表，在'head'，其中v指向第一个或第二个元素，或者为空。声音抽象传递函数自动获得简单地通过解释更新规则在三个真值，而不是两个。2.6抽象的组合器本节概述了关于定义和实现抽象组合（正确地称为产品）的研究。一般情况是有两个抽象格L1，L2，它们分别具有具体化函数γ1，γ2和抽象函数α1，α2.为了说明起见，我们考虑以下乘积：图1中的符号和奇偶校验格。最简单的积是直积，其中取所有对（a，b）∈A×B作为积格的元素。（a，b）的具体化简单地为γ1（a）<$γ2（b）。不幸的是，这可能会引入许多冗余元素。（odd， 0）是什么意思因为奇数和{0}的交集是空的，所以它的意思和（，）一样当一次只取一个分量时，后者更精确，所以我们想在看到（odd， 0）时使用它类似地，（T，0）应该减少到（even， 0）。头下下138N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131以这种方式去除冗余元素给出了期望的且表现良好的约简乘积[6]。如何构造约化积上的抽象传递函数？一种可能性是简单地逐点应用传递函数由A和B提供d，给定（a，b）<$→（f#（a），f#（b））。对于x：=x-1，我们1 2havef#（e ven）=oddandf#（0）=−，andndhence（even，0）›→（od d，−）.Th是1 2相当于（几乎）并行运行两个分析，没有交互作用他们之间然而，如果我们允许A和B合作互动，我们可以做得更好。逐点方法给出（even，+）<$→（odd，T）。 但我们知道如果整数n是偶数且n >0，则n≥2。因此，n−1必须是正的奇数，更精确的（even，+）<$→（odd，+）是可取的。这种合作是通过交叉的具体化，A和B之间的关系，即.Σ（a，b）›→α1（S），α2（S） 其中S=f（γ1（a）<$γ2（b））关键问题是如何开展这种合作。前面的定义并没有告诉我们如何去做直接实现传递函数是困难的和非模块化的：• 实现者必须具有所有格的结构的完整知识，其中通常可能存在n>0• 由各种格的元素编码的约束可能以微妙的方式相互作用，使得实现难以正确• 每次我们更改所用分析的组合时，都需要重新执行2.7开放式产品开放产品[5]试图自动和模块化地组合抽象，而简化产品则没有，同时仍然允许它们之间的合作其基本思想是允许抽象方案通过查询系统交换我们固定一个关于程序状态的查询集合Q。每个格L现在被赋予一个查询应答函数I：Q×L→ {true，unknown，false}，其中I（q，a）可以为真（分别为假），如果查询q为真（相应地，false）在由a表示的所有具体状态中，并且是未知的其他。抽象传递函数现在将另一个格提供的查询应答函数作为额外的参数，并且可以使用它N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131139term：：= var|int |Null|术语+术语|term − term|项×项|store（term，term，term）|store ( term, term, term )文字：：= term = term|term<术语|地图（术语）|C类（长期）|ClassC (term)Φ：：=文字|¬ Φ |Φ ∧ Φ |Φ ∨ Φ |Φ → Φ |Φ ↔ Φ|公司简介|公司简介| TC[a,b][Φ(a, b)](x, y)图三.用于交换信息的通用逻辑L以产生更精确的结果。开放产品已经应用于逻辑编程领域[5]，但似乎没有在其他地方。相关工作[12] 还描述了使用多个分析插件进行验证，在需要的地方应用每个插件，并使用公共逻辑在它们之间交换信息。然而，在[12]中，源程序的每个“模块”都只使用一个插件，并且交互只发生在模块边界，而不是每个指令。类似的主题也在[21，4]中找到。3用于验证我们现在描述我们的分析框架，它以模块化的方式组合分析，允许它们通过逻辑公式交换信息这使我们能够3.1普通逻辑我们首先定义公共逻辑，我们称之为L，用于插件交换信息。我们选择使用具有传递闭包的一阶逻辑或FO（TC），其语法如图3所示。逻辑是无类型的，在[14]的风格，其解释域包含：• 对象的地址，从无限集合地址• 特殊值null• 整数• 从addr到addr{null}的映射，用于表示类的字段140N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131通常的功能符号选择和存储提供了访问和更新地图。提供谓词来限制我们所谈论的定义域元素的集合：（x）和Map（x）分别意味着x是整数或一阶映射。对于程序中的每个类C，类C（a）声明a是类C的分配对象的地址。注意，FO（TC）中的be- cause函数是完全的，不适当的应用，例如，将算术运算符+应用于非整数参数确实会产生值。然而，关于这个值没有任何结论，量化器通常会使用谓词、Map和ClassC来保护。这种逻辑中的推理公理包括与选择和存储有关的标准公理。L的公式总是在状态对上-执行某些指令、方法调用或返回之前的状态，以及之后的状态。下标为0的变量表示较早的状态，普通变量表示较晚的状态。3.2插件接口本节解释了程序分析工具必须如何包装才能与我们的框架一起使用。每个插件都必须实现图4所示的接口。每个接口组件的非正式用途如下：• 数据类型T是插件使用的抽象值的类型。• （概念上的）具体化函数γ赋予抽象值以意义• 调用share（τ，i）要求插件共享一个L公式Φ，该公式在抽象状态τ所表示的所有具体状态中都是有效的（即Φ由t所蕴涵），并且在计算指令i的后继时可能对其他插件有用。• 调用succ（τ，i，Φ）计算程序可能达到的抽象状态集，通过在τ表示的具体状态中执行i并满足公式Φ。在实践中，Φ将是通过共享从其他插件收集的信息。• 函数shareC和succC用于处理方法调用，并采用实际参数列表而不是指令。• 从方法调用返回也同样被处理，除了必须提供两个抽象值而不是一个：一个描述被调用者近似地，返回后堆上的约束是从第一个开始的，而调用者局部变量上的约束是从第二个开始的N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131141（* 抽象值的数据类型 *）数据类型T（* 具体化函数-为抽象值赋予意义 *）（* 从未实际实现 *）funγ：T→P（状态）（* 在执行开始时获取可能的抽象状态 *）funinit：L→P（T）（*（*分享：T×Instr→L有趣的成功：T×Instr×L →P（T）（* 类似，但用于处理方法调用 *）C：T×Params→LC：T×Params×L →P（T）（* 同样类似，但用于处理方法返回 *）FunshareR：T×T→LFunsuccR：T×T×L →P（T）见图4。 分析插件从第二位开始。3.3示例插件：谓词抽象为了说明前面的小节，我们展示了如何将2.2节中提到的单项谓词抽象技术框架为插件。给定抽象谓词P1，.，Pn插件的抽象值的数据类型是TPA= 、∧i=1..n、i：每个具体化函数很简单;如果[−]]：L→P（State）给出了L-公式的语义，则γPA（γ 1）∧ Ψ n) =[Ψ 1∧... ∧Ψn]]定义份额也同样简单，因为TPA的元素已经是公式1.回想一下，公式是在成对的状态上的：那些在执行一个输入之前和之后的142N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131关于L：shareP A（2011年1月） . ∧Ψn,i)=Ψ1∧.. . [V\V0]单项式之间的转换像往常一样用满足性检查器计算。为了查看在由θ描述的状态下执行指令i是否可能使我们处于由Θ描述的状态，即，查看Θ 1是否为θ1. n∈succPA（101）伊莱恩， 我， Φ），我们检查满足性（2011年1月） . ∧Ψn)[V\V0]∧Post(i)∧Θ1∧.. . 联系我们公式Post（i）表示指令i的结果;例如，假设x和y是作用域中唯一的变量，后（x：= x +2）∧∧=x=x0+ 2∧y=y0(We当我们希望将其与等式区分开来时，将元等式写为=。逻辑，它仍然是书面的=）。对于方法调用，Post公式连接实际参数和形式参数。例如，如果由void m（int a，int b）声明的方法由m（x，10）调用，则Post公式将为a=x0b= 10。 注意，FO（TC）公式的可满足性是不可判定的。然而，我们仍然可以得到一个安全的分析，通过假设公式是sat-在我们无法证明的情况下是成立的。这意味着，当我们不能确定一个给定的过渡是否存在时，我们假设它存在。3.4过程间分析算法通过使用过程摘要的概念，我们能够分析带有递归方法调用的程序，而不需要用前置和后置条件来注释方法我们的算法是Ball和Rajamani在[1]中提出的用于布尔程序的Bebop模型检查器的算法的简单适应Bebop我们简单地将这些基于位向量的数据流事实和传递函数替换为基于插件的事实和传递函数。为了适应[1]的算法，我们必须提供：• 数据流事实的集合D• 对于每个指令i∈Instr，传递函数Transferi：D→P（D）• 对于条件或迭代语句上的每个保护Φ，两个转移函数TransferΦ，False，TransferΦ ， True：D→D（D），一个用于进入“true” 分 支 ， 一 个 用 于“false”分支。结构，调用或返回。由于单项式在执行指令之前保持，因此可以通过其编码“初始化”v 0来实现。N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131143类似的方法调用和返回的传递函数也是必要的;为了简洁起见，我们将不在这里讨论它们。我们“填写”这些要求如下。数据流事实是一个抽象值的元组，每个抽象值来自n个插件中的一个：D：= T1×T2×... × Tn为了计算元组（τ1，.，τn）在指令i下，我们首先在每个插件上调用share。这要求每个插件共享它可以描述i的执行的任何信息，并且我们形成所有结果然后我们在每个插件上调用succ，传递Φ作为参数，并从插件的各个后继者中获取所有可能的元组传递i（τ1，.，τm）：=j=1..nsuccj（τj，i，Φ），其中Φ：=πj=1.. Msharej（τj，i）以类似的方式，我们定义保护的传递函数：我们仅仅将保护或其否定与共享公式结合起来;跳过是没有效果的指令。转让五，T rue（τ1，.，τm）：=j=1..Msuccj（τj，skip，Φ）转让五，假（τ1，...，τm）：=j=1..Msuccj（τj，skip，Φ）3.5可靠性要求我们的插件进行的分析通常是近似的，但保守的，而不是精确的。每个插件必须满足什么条件才能使整体分析合理？这里我们只给出处理指令的条件;方法调用和返回的条件是类似的。假设我们要在抽象状态τ∈T中执行指令i。设fi是i的（具体）传递函数，s∈γ（τ）是τ所表示的任一具体状态。 第一个条件是，公式由插件导出的确实描述了i的执行：（s，fi（s））∈[[sharej（τ，i）]]（回想一下，公式是关于具体状态对的第二个条件是，如果从其他插件导入的公式正确，144N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131succ计算的新抽象状态保守地模拟了第一步：如果（s，fi（s））∈[[Φ]] 则fi（s）∈γj（succj（τ，i，Φ））4一种可插拔静态断言检查器我们已经实现了刚刚描述的框架作为Java子集的原型静态断言检查器断言检查器是可插入的，目前提供三个插件：谓词抽象，3值形状分析和可判定指针分析。在本节中，我们报告我们的实施情况。我们可以在以下意义上将我们的系统与高级语言的编译器进行比较：使用编译器而不是用汇编程序编程既没有增加原则上可以实现的算法的范围，也没有消除对人类洞察力的需要。它所做的是接管繁琐和容易出错的工作，如分配寄存器，从而允许用户专注于更高级别的关注点并实现更多。4.1编程语言我们的原型验证器包括一个通用的算法，用于解析和检查程序和一些分析插件，交换公式描述程序状态。为了简单起见，原型处理了Java的简化版本：主要遗漏了继承，多线程和异常。该语言的抽象语法如图5所示。使用L的公式，用户可以注释程序（大致以JML [13]的风格）。目前支持两种注释• 定义引入用户定义的谓词，用于注释，例如：//@ define successor（x，y）//@ by x>null y>nullselect（next，x）= y• 断言可以出现在任何预期语句的位置，并且要求当控制到达该位置时，给定的条件保持不变，例如。//@ assert x> null4.2实施分析插件目前有三个插件可用，它们都利用了现有的软件：谓词抽象：使用定理证明器[20]，这个插件提供了第3节中所述的谓词抽象一组可能的预测是从程序中猜测出来的，可以手动添加传递闭包用一阶公理处理，如[15]。N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131145program：：= classdecl*classdecl：：= classClassName{（字段decl|方法decl）*}类型：：= void|int |classNamefielddecl：：= typeFieldNamemethoddecl：：= type（static）？MethodName（（typeVarName）*）{ stmt*}参数：：= true|虚假|null|这|VarName|整数stmt：：=VarName=newClassName（）| VarName (. FieldName）？ =（simpleexpr |VarName。FieldName）| { stmt*}| if ( expr ) stmt (else stmt)?| while ( expr ) stmt| return (expr)?| (VarName =)? SystemName（param*）| (VarName =)? VarName。SystemName（param*）| (VarName =)? ClassName. SystemName（param*）简单表达式：：= true|虚假|null|这|VarName|整数| ! simpleexpr|−| × ||&&|||为|>>|<|=） select（data，y）， P2 ：= y /= P3=P3=选择（next，y） 假设当执行到达内部时，结构y =y.next唯一可能的数据流事实是对P1 ^ P2^P3，x下一个y(we将此堆称为h0）。首先，我们看看如果我们在不共享插件之间的信息的情况下计算后继会发生什么（这是通过传递True作为共享公式来实现的）。对于谓词抽象，我们得到：⎧ ⎫⎪ P1P2succcPA（P⎪⎨¬PPnext，True）=12017年12月27日P，1 2 3⎪ P1P2P3，⎪⎩¬P∧P∧¬P⎪⎭2 3对于TVLA，我们有succTVLA（h0，y = y.next，True）={h1，h2，h3}，其中堆h1，h2和h3是N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131147H1XyH2XyH3Xy因此，有12个后继元组，其中一些是不一致的，我们很快就会看到。另一方面，当启用共享时，分析器在每个插件上调用共享，导致共享信息Φ：共享TVLA（h0，y = y.next）∧=x0/=0共享PA（P1-P2-P3，y = y.next）∧=（P1<$P2<$P3）[V\V0]select（data0，x0）>select（data0，y0）=0/= select（next0，y0）/=select（data0，x0）>select（data0，y0）Φ=select（next，y）/=x0 0 0对succPA和succTVLA的调用现在包括Φ。尽管TVLA插件不能select（data0，x0）>select（data0，y0）x和y不能指向同一个对象，因此可以消除后继h1，留下succTVLA（h0，y = y.next，Φ）={h2，h3}.这留下了八个后继元组。然而，其中还有五个是不一致的，将在下一次共享迭代中被消除。例如，运行skipon（P1<$P2<$P3，h3），我们得到：148N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131共享PA（P1-P2-P3，跳过）select（data0，x0）>select（data0，y0）0/==select（next0，y0）共享TVLA（h0，skip）∧=x0/= 0 免费0Null ∧x0=y0select（data0，x0）>select（data0，y0）∧Φ =select（next0，y0）/=100万Null 免费0Null ∧x0=y0现在，用于谓词抽象的定理证明器检测到x0= y0和select（data0，x0）>select（data0，y0）之间的不一致，TVLA检测到select（data0，x0）> select（data0，y0）和堆h3之间的不一致。从而得到succPA（P1<$P2<$P3，skip，Φ）=0succTVLA（h3，skip，Φ）=0因此，如所期望的，转移跳跃（（P1<$P2<$P3，h3））=请注意，在这种情况下，两个插件都返回空的后继集，但情况并非总是如此;一个插件返回空后继集。6结论和今后的工作在本文中，我们描述了一个模块化的框架，通过交互分析插件，基于抽象的程序验证，并报告了一个原型系统的我们通过一个例子证明了我们的方法可以提高精度。在我们得出这对核查有用的结论之前，有两个关键问题需要探讨：N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131149• 效率：原型目前的速度相当慢，这阻碍了更大程序的实验。另一方面，到目前为止，几乎没有花费多少时间来使它更快，并且可以进行大量明显的优化。然而，一个更重要的问题是这种方法的基本效率一起运行分析但不交换公式应该不会比单独运行它们慢，事实上可能更快，因为其中一个工具排除的执行路径不需要被其他工具考虑。交换信息必然是更多的工作，但还有多少工作有待观察。• 使互动更加受需求驱动：目前分享公式的方式相当笨拙和随意。谓词抽象插件共享整个单项式，而TVLA插件则提供了简单的属性模板来共享。交互需要需求驱动，本着懒惰抽象的精神[9]，这样信息才能被发送到有用的地方。显然，这个问题与效率有关。确认我想感谢迈克尔·胡特为我们就这项工作进行了许多富有成效的讨论。引用[1] 球，T。 和S. K. Rajamani，Bebop：布尔程序，在：SPIN 2000会议记录，LNCS1885（2000），pp.113-130[2] 球 ， T 。 和 S.K. Rajamani ， Automatically validating temporal safety properties ofinterfaces，in：SPIN103-122.[3] Burch，J.R.，E. M. Clarke，K. L. McMillan，D. L.迪尔和L. J. Hwang，Symbolic modelchecking：1020states and beyond，Information and Computation98（1992），pp.142-170[4] 张，B.- Y. E.和K. R. M. Leino，Abstract interpretation with alien expressions and heapstructures，in：VMCAI147比163[5] Cortesi，A.，B. Le Charlier和P. Van Hentenryck，逻辑编程的抽象域组合：开放产品和通用模式构造，计算机编程科学38（2000），pp. 27比71[6] Cousot，P. and R. Cousot， Abstract Interpretation and Application to Logic Programs ，Journal of Logic Programming13（1992），pp. 103-179[7] Fra d et，P. 和D. L. M'etayer，Shapetypes，in：POPL27比39[8] Grêadel，E.和我。Walukiewicz，GuardedFixedPointLogic，in：Proceedingsof14hAnualIEEESymposium on Logic in Computer Science，Trento，1999，pp.45比54150N. Charlton/Electronic Notes in Theoretical Computer Science 145（2006）131[9] Henzinger，T.一、R.贾拉河Majumdar和G. Sutre，Lazy abstraction，in：Proceedings of the29th Annual Symposium on Principles of Programming Languages，ACM Press，2002，pp.pp. 58