基于模式的动态链接数据结构程序验证方法

理论计算机科学电子笔记145（2006）113-130www.elsevier.com/locate/entcs基于模式的扩展线性链接数据结构MilanCeska，PavelErlebach，andTomasVojnar1FIT，BrnoUniversityofTechnology，Bozetechova2，CZ-61266，Brno，CzechRepublic摘要本文讨论动态链接数据结构程序的自动验证问题。特别是，使用基于模式的抽象的内存配置被认为是。在这种方法中，人们可以通过抽象出某些记忆模式相邻出现的确切数量来抽象记忆配置。本文通过提出一种全自动和高效的方法来检测要从手头的程序正在生成的内存配置中使用的内存模式，从而扩展了这一领域的最新技术。该方法的目标是操作广泛的扩展线性链接数据结构的程序，这些扩展线性链接数据结构具有线性骨架（可能是双向链接或循环的），在其顶部定义了某些附加指针，其涵盖了许多实际的动态数据结构（例如列表、双向链接列表、循环列表、具有尾/头指针的列表等）。 实验结果表明，该方法具有很强的竞争力，具有很大的扩展潜力。保留字：形式验证，程序分析，动态链接数据结构1引言处理指针和动态链接数据结构是计算机编程中最困难的部分之一，自然也是最容易出错的部分之一因此，非常希望为程序员提供自动工具，帮助他们在指针操作过程中发现错误或允许他们证明它们是正确的。因此，验证具有动态链接数据结构的程序是一个非常活跃的研究领域1 电子邮件：ceska@fit.vutbr.cz， erlebach@fit.vutbr.cz，vojnar@fit.vutbr.cz2由捷克赠款机构项目102/05/H 050、102/03/D211和102/04/0780支助。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.10.008M. Ceškaetal. /《理论与计算科学》145（2006）113114虽然在动态链接数据结构程序的验证领域已经取得了许多成果，但在通用性、自动化和已知方法的效率方面由于处理的是无界结构，这个问题当然是不可判定的。因此，寻求各种近似和/或半算法方法。由于要操作的对象通常是表示特定内存配置的不受限制的图，因此问题进一步复杂化在这项工作中，我们通过显着改进[14，15]中首次提出的方法（我们称之为基于模式的验证），为动态链接数据结构的程序验证研究做出了贡献。该方法是基于识别一些重复的模式，在所谓的形状图，代表内存配置和抽象的内存配置，通过不记得这种模式的确切数量的出现在[14，15]中，该方法的用户应该提供用于抽象的适当内存模式。在这里，我们提出了一种全自动检测记忆模式的技术，这使得整个方法完全自动化，因此我们可以称之为基于模式的自动验证。让我们补充一下，[14，15]将计数器附加到形状图的每个汇总节点。计数器计算隐藏在摘要节点后面然后可以使用对整数进行自动抽象的方法来保持关于这些计数器的值的某些信息我们在这里不考虑这种扩展，但它可以很容易地引入。我们的方法目前可以处理扩展的线性链接数据结构，我们指的是具有线性骨架（可能具有双向链接或闭合成循环）的动态链接数据结构，在线性骨架上可以添加两这意味着我们涵盖了广泛的非常实用的结构，如列表，双向链表，循环（双向链接）列表，可以扩展为经常使用的结构，如指向列表的第一个或最后一个元素的附加指针我们自动检测记忆模式的方法背后的基本直觉扩展线性结构的记忆模式必须有某种线性骨架（或主干）。这个骨架被所谓的入口节点和出口节点包围。当我们有几个相邻的-M. Ceškaetal. /《理论与计算科学》145（2006）113115在模式的所有状态中，第一个实例的出口节点成为另一个实例的入口节点，等等。因此，这些节点必须有一个平等的选择器环境（下一个指针）和平等的选择器路径的全球共享节点。这一事实可以在检测模式时加以利用我们目前通过为程序的每个控制点生成一组抽象形状图来处理所考虑的程序类，这些抽象形状图覆盖了此时可能获得的所有内存配置，并检测是否没有指针操作错误（如通过未定义指针或内存泄漏的引用）。然后，生成的抽象形状图可以用于检查程序的其他安全属性，例如反转链表的结果再次是链表，或者甚至是输入列表的反转。如果发现错误，我们的技术为我们提供了一个具体的错误跟踪。我们已经实现了一个原型的Prolog为基础的工具，并尝试了一些所描述的那种程序的方法。结果是非常令人鼓舞的，无论是从该方法的简单性（和进一步推广和改进的巨大潜力）的角度来看，以及从它的非常有竞争力的效率的角度来看相关工作。除了[14，15]启发了我们的工作，我们在这项工作中显着扩展，已经发表了许多其他作品，主题是动态链接数据结构程序的形式验证（或形状分析或别名Pale [10]的方法基于使用WS 1 S/WS 2S和Mona [9]来编码和处理指针操作。该方法可以处理一些我们目前无法处理的结构（如树及其扩展），尽管我们已经在扩展我们的方法，覆盖这些结构。然而，与我们的方法不同，Pale的方法对于非无循环代码来说并不是完全自动的，必须手动指定循环不变式，这可能并不容易。TVLA [11]使用三值逻辑来编码形状图。TVLA还可以处理一些比我们当前状态下的方法更一般的结构TVLA方法比Pale的方法更自动化，但仍然可能需要用户提供定义所使用的结构类的核心谓词和插装谓词（或[5]的后期方法中的模拟不变量），以使抽象足够精确。 直到最近，才出现了[8]一种自动生成一些插装谓词的方法。在[2]中提出了一种用一个选择器验证动态链接结构的全自动方法。本文基于抽象正则模型检验，给出了线性数据M. Ceškaetal. /《理论与计算科学》145（2006）113116结构使用合适的有限字母表上的单词进行编码。然后，配置集被有限自动机描述为正则语言，有限转换器用于编码指针操作程序语句，并通过重复应用计算可达集。一个特殊的抽象-检查-细化框架用于使该方法尽可能频繁地终止并使其高效。与这种方法相比，我们可以处理一些更一般的结构，如双向链表，带有附加指针的列表等。另一种有趣的全自动方法是[7]基于使用形状图和某种属性语法的组合。这种方法可以处理一些我们目前无法处理的结构（基于树）另一方面，我们也可以处理一些[7]的方法无法处理的结构（带有附加指针的双向链表等）。在[12]中，继[6，4]的早期工作之后，考虑了may-alias分析的特殊问题，并使用了基于自动机和约束的记忆May-alias分析也在[13]中被考虑，其中内存对象由与程序创建时的状态相关的特殊时间戳表示。在文献[1]中，引入了一种基于将存储器配置表示为自动机集合的具有Hoare类证明系统纸的计划。在下一节中，我们将描述一个操作动态链接数据结构的示例程序，该程序将在本文中用作运行在第3节中，我们提出了我们的方法来自动化的基于模式的验证。然后，在第4节中，我们介绍了我们使用该技术进行的实验结果最后，我们给出了一些结论和我们计划的未来工作的方法的扩展的轮廓。2运行示例在本文中，我们将使用带有指向尾元素的附加指针的双向链表结构作为运行示例。图2中描绘了这种列表的示例以及用伪C++语言编写的这种类型的列表的构造器。对于一个双向链表来说，拥有指向头元素和尾元素的额外指针可能更自然，这是我们在实验中考虑的一种情况，但是结构会变得太复杂而无法用于解释目的。让我们注意到，我们还通过假设new总是成功来简化它M. Ceškaetal. /《理论与计算科学》145（2006）113117intx =new;t=t;t−>n=NU LL;public voidrun（）{new;y−>n=x;x−>p=y;y−>t=t;x=y;}x−>p=NU LL;Fig. 1. 带尾指针3基于模式的自动验证内存配置包括许多动态分配的节点（内存对象），这些节点是程序中定义的各种数据结构（记录）的实例这些结构包括（非指针）数据字段，我们在这项工作中抽象出来，指针字段-选择器-将特定的内存对象链接在一起，形成一个列表，一个双向链表等特定的内存对象是可传递访问的程序通过指针变量指向其中一些在提取记忆结构时，我们寻找的是某种记忆模式的重复出现。由于我们假设使用基于线性骨架的扩展线性结构，因此我们提出由单个入口节点、单个出口节点、一组内部节点以及所谓的共享节点给出的模式。 共享节点有点类似于全局程序变量-它们可以通过某些选择器序列从任何其他节点访问内部节点只能在它们自己、入口和出口节点以及共享节点之间建立链接。通过用单个总结节点（加上未总结的最后一个退出节点）替换任意数量（大于或等于2）的所谓内存模式的相邻出现的入口、出口和内部节点（以及它们之间的适当链接），可以抽象出内存配置我们目前允许使用单一的内存模式一个generalisation的框架是留给我们未来的工作，让我们，但是，请注意，即使有一个单一的内存模式，我们已经能够处理许多有用的实际程序。在分析程序时，我们计算一组在每个程序点可达的抽象内存配置当验证一个过程，如列表反转，我们假设它是由一段代码作为前缀，不X不不不不pnpnpnpnpnM. Ceškaetal. /《理论与计算科学》145（2006）113118所考虑的输入结构的构造器，其具有非确定性地选择的长度。当我们在抽象内存配置上应用程序语句时，如果语句设置程序变量指向汇总节点，则可能需要至少部分地将其和其他作品一样，我们把部分具体化称为具体化操作。这种操作总是产生两种结构-在一种结构中，总结节点被记忆模式的两次出现所取代，在第二种结构中，我们获得了模式的一次具体出现和一个总结节点（对应于在总结节点后面隐藏了超过两次的模式然后在模式的具体化发生时执行该语句随后，通过在单个汇总节点后面隐藏任意数量（大于或等于两个）的相邻内存模式，从而抽象出所得到的内存配置这个操作在文献中又被称为总结操作。通过调用下面描述的findPattern函数来扩展上述过程，该函数试图在每个新出现的内存配置中识别内存模式，直到识别出某个模式之后，不再调用此函数，并在具体化和汇总过程中使用已识别的模式。如果没有找到模式（或者考虑了错误的模式），并且我们遇到一个大于某个预定值的内存结构，则该过程以“不知道”的答案停止类似地，当过程终止，并且给定的感兴趣的安全属性被破坏时，我们可以通过向后计算来测试消除所述限制的程序的概括是我们未来工作的主题。在本节的其余部分，我们首先形式化了内存配置和内存模式的概念，然后我们描述了用于自动检测内存模式的建议函数findPattern，最后，我们简要描述了物化和总结的算法。3.1形状图和形状模式让我们固定一个任意有限的选择器集合Sel和一个任意有限的程序指针变量集合Var。我们将抽象存储器配置表示为形状图SG=（N，E，PT，SM，λ），其中：（1）N是节点（存储器对象）的有限集合。 (2)EN×Sel×N是对内存对象之间的指针链接（边）进行编码的关系，<$n1，n2，n3∈N<$s∈Sel：（n1，s，n2）∈E<$（n1，s，n3）∈E<$n2=n3且M. Ceškaetal. /《理论与计算科学》145（2006）113119ESM × Sel × SM =。（3）PT：V ar→N表示哪些程序变量指向哪些节点（4）SM_N是存在于形状图中的一组摘要节点，在其后面隐藏了所使用的任意数量的出现的(5)最后，λ：E→ {entry，exit，multi，normal}指定节点之间的链接类型。我们需要<$n1，n2∈N <$s∈Sel <$e∈E：e =（n1，s，n2）<$λ（e）=正规惠{n1，n2}<$SM =<$且<$n1，n2∈N<$s∈Sel<$e∈E：e=（n1，s，n2）<$λ（e）∈ {entry，exit，multi}|=1。|= 1.两个摘要节点之间没有边。让我们补充一下，我们允许SM= Σ。然后，我们得到一个具体的内存配置作为一个特殊的情况下，一个抽象的没有使用抽象。的当描述概括过程时，进入、退出和多边的含义将变得清楚记忆模式被定义为5元组P=（PN，e，x，S，P E），其中：PN是模式的节点的有限集合。(2)e∈PN是其入口节点，格局 (3)x∈PN是出口节点，x e。 (4)S是一组共享的这样的节点，{e，x}S=。 (5) PEPN×Sel×PN是一组边描述模式的节点之间的指针链接出于技术原因，我们还使用了具有两个出口节点的内存模式概念的扩展扩展内存模式是一个5元组PE=（PN，e，X，S，P E）定义如上，直到X=PN是一个集合，使得|X| =2和{e}<$X = X<$S=<$。当必须检测给定内存配置中的模式时，我们检测扩展模式，然后拆分它在中间的一对两个扩展模式的检测在我们有来自单个节点的更多下一个指针的设置中是有利的（如在双向链表中），并且在没有任何附加信息的情况下，很难猜测结构的正确方向。这就是为什么我们将在两个（所有）方向上搜索。最后，对于给定的形状图SG=（N，E，PT，SM，λ）和给定的扩展记忆模式PE=（PN，e，X，S，PE），我们定义了一个函数matchSG，P：N→ {true，false}，该函数指定记忆模式是否适合形状当给定的根节点r∈N与入口节点e匹配时的图。（请参阅函数可以通过取X={x}用于非扩展内存模式。）如果存在映射f：N→PN，则函数返回true {undef}在形状图和图案的节点之间，使得下面的条件（1）、（2）和（3）成立：(1)f（r）=e<$$>m，n∈N：f（m）=f（n）<$f（m）=undef.条件（1）说明我们匹配r和e，当我们忽略到undef的映射时，函数是一个注入。M. Ceškaetal. /《理论与计算科学》145（2006）113120(2)m，n∈N(2.1)（a，s，b）∈PE<$a=f（m）<$b=f（n）<$(2.2)（m，s，n）∈E<$（m/∈SM<$a∈X）<$（n/∈SM<$b∈X）.条件（2）要求来自PE的所有边在SG中具有对应边。我们不允许将模式映射到摘要节点上。(3)m，n∈N(3.1)a=f（m）b=f（n）（（3.2.1）a=b=undef（3.2.2）（a/=<$b <<$（a，s，b）∈PE）（3.2.3）（aundefb=undef（（3.2.3.1）（a∈X<$$>c∈PN：（e，s，c）∈PE）<$（3.2.3.2）（a∈S）（3.2.3.3）（a=e<$$>x∈X <$c∈PN：（x，s，c）∈PE）（3.2.4）（a=uniformb/=uniformb）（3.2.4.1）（b∈X<$$>c∈PN：（c，s，e）∈PE）<$（3.2.4.2）（b∈S）（3.2.4.3）（b=e<$$>x∈X <$c∈PN：（c，s，x）∈PE）。条件（3）成立，如果来自E的每条边满足以下要求之一：它要么与模式（3.2.1）完全无关，要么在模式（3.2.2）中有一个对应物，要么是模式（3.2.3）的内部边缘，要么是模式（3.2.2）的外部边缘，要么是模式（3.2.4）的内部边缘。如果它引出模式，则必须有从e（3.2.3.1）引出的具有相同选择器的边。该条件仅针对输入为非扩展模式的情况引入如果它从一个共享节点（3.2.3.2）引出，我们不需要任何其他东西，因为我们对共享节点的周围环境不感兴趣如果它从e（3.2.3.3）引出，则一定有一条边具有从x引出的相同选择子。类似的条件适用于引入图案的边缘（3.2.4）。所描述的概念如图2所示在顶部有一个形状图（它是一个具体的形状图，即其中没有摘要节点），其中我们突出显示了与下面中间所示的扩展内存模式匹配的节点这个扩展的记忆模式可以被分割成两个M. Ceškaetal. /《理论与计算科学》145（2006）113121X1pepX2不不不SenX1不不SX不不不n不不不nnnn不 npppX1pepX2ppSnpnn n图二.一种匹配样本形状图的扩展记忆模式及其分裂为两个3.2记忆模式寻找记忆模式的策略是，我们逐步考虑给定形状图的每个节点n（注意，这个形状图是具体的-其中没有汇总节点，因为我们还没有找到任何模式，也没有应用任何抽象）作为入口节点的来源，并尝试识别以n为入口节点的记忆模式的边界（目前，我们认为函数f是模undef的单位元，因此根和入口节点变得相同）。识别边界意味着我们寻找与所选入口节点n具有相同周围边的出口节点，以及从入口节点和出口节点通过相同选择器路径可访问的共享节点随后，我们检查潜在模式是否在给定的形状图中具有重复的相邻出现。只有这样，它才被认为是一种有用的记忆模式。作为算法1呈现的函数findPattern实现了模式搜索的顶层。它迭代通过给定形状图的所有节点n，这些节点可从某个指针变量访问，并尝试使用下面讨论的算法中的findPatternFromEntry函数找到以n作为其入口节点的内存作为算法2呈现的函数findPatternFromEntry检查给定节点e的所有周围环境，并检查它们中的一些是否可能是内存模式。在下面描述的函数findCandidate中寻找看起来像潜在的扩展模式（即，扩展模式的候选）的对于候选扩展模式，我们放宽了有两个出口节点的条件，我们允许更多的出口节点。可以使用与e相邻的边的集合在线计算得到3. 函数findCandidate返回越来越大的环境，或NULLepX2不不SM. Ceškaetal. /《理论与计算科学》145（2006）113122算法1（用于检测存储器模式的顶级函数1findPattern（SG=（N，E，PT，SM，λ））{2V isited=0;3foreach（v∈V ar）{4n=PT（v）;5{n};6while（ToTry）{7从T oT ry中选择n1; T oT ry=T oT ry\{n 1};8if（n1∈/Visited）{9V isited=V isited{n1};10if（（P=findPatternFromEntry（SG，n1））/=NULL）11返回P;12ToT ry = T oT ry {a ∈ N |s：（n1，s，a）∈ E};13}//if（n1∈/Vited）14}//while（n1∈/Vited）15}//foreach（v∈V ar）16returnNULL;17个文件夹这意味着没有更多的候选项-在这种情况下，findPatternFromEntry失败，返回NULL。如果找到了某个候选模式，就对其进行测试（第8 - 11行），以真正产生一个有用的模式。我们要求，对于给定的，形状图和候选扩展模式。通过这种方式，通过尝试将扩展模式的入口节点与扩展模式的另一实例的出口节点进行匹配，我们测试在找到的候选者“之前”和“之后”是否存在模式的另一个如果是，则候选者被声称是有用的扩展模式。如果没有，我们将候选者的退出节点添加到集合F alseX中，以排除在未来找到相同的候选者并重复搜索。让我们也注意到，当它找到一个具有两个以上出口节点的候选扩展模式这样的候选扩展模式不符合我们对扩展模式的定义，并且表明遇到的结构可能不是线性的（当考虑可能未来的概念概括，我们可以，例如， 获得|X|= 3（对于二进制）树木等）。最后，如果找到一个有用的候选扩展模式，其中有两个出口节点满足我们对扩展模式的定义，那么它随后会被分割成一对“对称”模式，其中一个函数findCandidate（算法3）寻找给定节点e的最小周围，该给定节点e可以是扩展的存储器模式，其中e作为其入口节点，考虑到所有先前的不成功搜索。在findCandidate中检测候选扩展模式的关键步骤是检测模式的线性骨架周围的出口节点的adepts。当函数第一次被调用时，M. Ceškaetal. /《理论与计算科学》145（2006）113123算法2（搜索具有给定入口节点的模式1findPatternFromEntry（SG=（N，E，PT，SM，λ），e）{2false =false;3EntrySel = E（{e}×Sel×NN×Sel× {e}）;4while（（P=findCandidate（SG，e，FalseX，EntrySel））/=NULL）{5（PN，e，X，S，PE）=P;6returntrue;7foreach （x∈X）{8if（<$match（SG，P，x））{9int x=intx {x};10returnfalse;11}12}13if（ok）14如果（|异能者|> 2）15返回 NULL;//不是一个扩展模式。16int n = int n（P）;17}//while（（P = findCandidate（. ））18returnNULL;19}空）adeptsXAdepts设置为空（第2行）。然后，该函数为作为结果的一部分返回的出口节点（以及检测到的共享节点，内部节点和适当的边缘）找到至少两个adept，或者该函数失败并返回NU LL。如果找到了候选扩展模式，但未被接受，则再次调用findCandidate，并为出口节点F alseX给出一组adept，当寻找模式的另一个相邻出现时，对出口节点F alseX的正确匹配测试失败。然后，这些节点被从先前运行findCandidate时记住的exit节点的adepts集合中删除（第3行），并重复搜索，其中未失败的adepts被视为已经探索过（第5行）。当探索从给定入口节点e可到达的节点时，每个新发现的节点在第15- 24行被测试为出口节点的熟练者-只要它在之前的findCandidate调用中没有失败，并且是共享节点的熟练者（第26- 32行）。一个节点n1是否是出口节点的adept的测试包括检查它周围的边是否匹配围绕所选入口节点的那些。如果这个测试通过了，节点就会被添加到XAdepts集合中，然后重新开始搜索（直到记住XAdepts为止）--这一步的目的是让新添加的adepts更容易检测到共享如果没有发现节点n1这包括测试是否存在从某个exit adept到n1的选择器路径，该路径与从e到n1的路径具有相同的选择器，但不与后一路径共享任何节点。M. Ceškaetal. /《理论与计算科学》145（2006）113124算法3（搜索扩展记忆模式的候选者）1findCandidate（SG=（N，E，PT，SM，λ），e，FalseX，EntrySel）{2staticXAdepts = 0;//在调用之间保持定义。3XAdepts=XAdepts\FalseX;4{e};5Explored={e}个XAdepts;6 PE=0;7while（ToExplore）{8从ToExplore中选择n;9T oExplore=T oExplore\{n};10foreach（（a，sel，b）∈E使得a=n<$b=n）{11PE=PE <${（a，sel，b）};12if（a==n）n1=b;elsen1=a;13if（n1∈/Explored）{14Explored=Explored{n1};15if（n1∈/F alseX）{16foreach（es∈EntrySel）{17if（s∈Sel：（es=（e，s，e）<$（n1，s，n1）∈/E）<$当我们匹配一个出口节点和一个跟随的入口节点时，也会重复当发现n1是共享节点的adapt时，从适当的退出adapt到n1的路径的所有边和节点（除了退出节点）被添加到候选扩展模式。一个新发现的节点，不被认为是一个出口节点，也不被认为是一个共享节点的专家，只是添加到集合ToExplore，搜索继续从它的继任者。3.3总结和具体化我们现在简要地描述了概括和物化操作将用于我们的抽象形状图。正如我们已经说过的，summarisa- tion是一种抽象操作，它取代了内存中重复出现的18（<$nJ∈N：es=（e，s，nJ）<$$>nJJ∈N：（n1，s，nJJ））<$19（nJJ∈N：（nJJ，s，n1）20goto25; // n1不能是退出节点21}22{numerals}{numerals};23goto4;//用一个新的adept重新开始搜索24}/tif（n1∈/F alseX）25T oExplore=ToExplore {n1};26foreach（x∈XAdepts）{27如果（n =path（a，n1）∈SGn=path（a，n1））{28addSelectorsFrompath（a，n1）toPE;29addNodesFrompath（a，n1）\atoS;30T oExplore=T oExplore\{n1};31}32}//foreachx33}//ifn1∈/Explored34}//foreachedge35}//while（ToExplore/=）36如果（|XAdepts|（<二）37返回 NULL;38PN ={k，l∈N|s∈Sel：（k，s，l）∈ PE};39返回（PN，e，XAdepts，S，PE）;40}M. Ceškaetal. /《理论与计算科学》145（2006）113125模式，并且具体化是从给定的概要节点具体化存储器模式的具体出现的部分具体化，其随后可以由程序语句处理不幸的是，这些操作的完整和正式描述超出了本文的有限空间-它将出现在本文的完整版本中，我们也可以参考读者[15]，其中详细描述了类似的对于给定的形状图SG=（N，E，PT，SM，λ）和给定的记忆模式P=（PN，e，x，S，P，E），概括操作如下工作。我们遍历所有可从程序变量访问的节点，并且对于每个非汇总节点n1∈N，我们测试是否匹配SG，P（n1）=true，即当n匹配与入口节点。我们还检查了没有一个涉及的节点是由一些程序变量指向的-在总结之后，这将导致一种情况，即变量将指向我们想要排除的无限数量的节点。如果测试成功，我们将所有与模式匹配的节点（除了退出节点和共享节点）收集到一个集合ofnodestobecollapsedT oCollaps={n∈N|f（n） =p<$p∈/S<$p/= x}.我们进一步检查节点n2是否绑定到出口节点，即f（n2）=x，可以被用作另一次出现的开始。模式（即我们检查是否匹配SG，P（n2）=true）。如果是，我们再次注意要总结的适当节点，并重复整个过程，直到匹配SG，P返回true。如果n1是一个总结节点，我们定义匹配测试总是成功的，我们只需将n1添加到ToCollaps中，并将其退出作为进一步检查的入口。如果所描述的过程成功至少两次，则创建新的摘要节点sm新的摘要节点与形状图链接，如下所示。与原像相关的边（a，s1，f-1（e）），（f-1（e），s2，b）1 1第一概括存储器模式中的入口节点e（令fi表示在模式的第i次出现中使用的函数f）被与概要节点链接并具有类型条目的新边（a， s1，sm），（sm， s2，b）所取代。连接的边（a，s1，f−1（x）），（f−1（x），s2，b）K K- 最后概括的存储器模式的出口节点x的原像，以及该模式a、b中的其它节点被边（sm，s1，f-1（x））代替，−1k（fk（x），s2，sm）类型的exit。最后，将映射到某些共享节点s∈S的节点n与该模式中的其他节点通过某些选择器s都被sm和n之间的一条边替换，s，并具有多个类型。我们重复总结过程，直到有可能总结。为了优化案件的程序，当我们搜索M. Ceškaetal. /《理论与计算科学》145（2006）113126结构从它的结束（这可能是当前唯一的节点可访问的一些指针变量），我们也允许一个反向的方式链接一系列的occurrences的内存模式。然后，我们尝试将开始节点n1与模式的退出节点匹配，然后将模式的入口节点与模式的另一个出现的退出节点匹配，依此类推。现在让我们进行物化操作。当我们执行一个程序语句，使某个程序变量指向一个汇总节点（因此，实际上指向一个无限数量的具体节点），或者删除另一种类型的边时，就会使用这个操作。第一种情况的一个典型例子是使用一个语句y = x->n，其中x指向的节点的n-后继节点是一个汇总节点。另一种情况的典型示例是free（x），其中x指向的节点链接到汇总节点，这意味着适当的链接不能是正常边。最后一步的动机是保持形状图的规范形式，其中汇总节点总是被非汇总节点包围。具体化总是导致两个形状图-在其中一个中，总结节点完全被记忆模式的两个具体实例所取代;在第二个中，总结节点被保留，但在它之前或之后，我们添加了一个记忆模式的具体实例第一种情况模拟了这样一种情况，即汇总节点只覆盖了内存模式的两个实例，因此在其中一个实例被某个指针变量指向之后，就再也不可能进行汇总了。第二种情况对应于当存在隐藏在概要节点后面的模式的更多出现时的情况，并且因此概要节点可以在具体化中幸存。当从汇总节点中具体化内存模式的实例时，我们必须尊重汇总节点周围的入口/出口边的性质。当我们需要模式的新实例出现在入口边的方向时，它通过其出口与汇总节点链接节点，反之亦然。所描述的操作在图3中描绘。为了降低图形的复杂性，我们省略了尾指针。摘要节点被绘制为双圆，入口或出口类型的边缘被绘制为分别带有两条平行线或交叉线的箭头。在左边有一些具体的内存配置，它们都被抽象为同一个抽象内存配置（中间的那个然后，由于执行x = x->n和y = y->p语句，该配置右边显示了相应的内存配置对。M. Ceškaetal. /《理论与计算科学》145（2006）113127npnpnpn pn pn pn pnpnpxxxn nnXx = x np ppXyn nnp ppX y恩恩恩n pp ppX y公司简介y = y pn nnp ppyx y图三. 总结和具体化表1基于模式的自动验证的一些实验结果程序SLLSLL+tSLL+dDLLDLL+dDLL+htcSLL+dcDLL+d构造函数0.020.080.140.030.251.020.060.09getLast0.040.180.260.080.471.52––反向2.4510.235.706.7213.7851.156.0216.03insertFirst0.030.140.190.040.382.030.090.18删除0.200.980.770.441.476.290.681.33插入0.221.050.840.511.767.560.400.73deleteAll0.030.120.190.040.311.330.070.14搜索0.060.260.330.110.621.860.130.234个实验为了测试我们的方法的功能，我们实验了几个现实生活中的程序与各种扩展的线性链接结构。结果总结于表1中。SLL或DLL分别表示单链表或双链表。X+t或X+h分别表示带有指向尾部或头部的附加指针X+d表示具有附加数据节点的最后，cX表示循环结构。我们验证了不存在空值解引用和内存泄漏n pn pM. Ceškaetal. /《理论与计算科学》145（2006）113128在程序和结构的所有组合中。此外，我们验证了每个程序的一些特定功能（例如，deleteAll总是导致空结构，反向导致相同类型的结构，等等）。在所有情况下，感兴趣的过程都在结构的构造之前（表1中的构造函数行对应于仅检查结构的构造）。请注意，标有“-”的字段表1中所示的时间是从我们方法的基于SWI Prolog的原型实现中获得的五个测量时间的平均值。它们是在配备AMD Athlon 2GHz处理器的PC上获得的与其他验证方法相比，结果似乎非常令人鼓舞和具有竞争力（当我们考虑到尚未考虑该方法的优化时，甚至更多）。让我们简单地回到与其他结果相比在相对较高的时间内验证的相反这是因为我们使用了[3]中提出的技术来检查输出是否真的是给定输入列表的反转（而不仅仅是某个列表的反转为此，我们通过设置一个特殊的、新引入的变量head来标记列表中的第一个元素，然后以类似的方式用变量tail标记最后一个元素，并进一步任意选择中间的两个后续元素，将它们标记为第一个和第二个。（我们的技术还不支持存储在节点中的数据值，所以我们使用指针变量。然后我们检查输出是否以tail开头，以head结尾，并且包含一对second-first在循环结构中，当然不使用头部和尾部标记正如在[3]中所讨论的，这保证了结果列表实际上是输入的逆，并且没有添加，删除等。所描述的插装显著增加了可达抽象内存配置的数量，因此获得的时间有点高。5结论在本文中，我们考虑了[14，15]中首次提出的动态链接数据结构程序我们已经提出了一个显着的扩展方法的自动程序检测记忆模式时，抽象的内存配置，urations。通过这种方式，我们使该方法完全自动化。我们已经在一个原型工具中实现了该方法，并在一些扩展的线性链接数据结构和各种程序上显示了其适用性，M. Ceškaetal. /《理论与计算科学》145（2006）113129操纵他们。我们的实验结果从一个非常轻的重量原型-连同简单的原则的方法-似乎是非常令人鼓舞的，并oacerering进一步扩展和改进的巨大潜力在未来，我们首先计划以更可靠的方式实现该技术（包括指定要检查的属性的系统方式），并在更多的示例上进行测试。我们还计划扩展该技术，以处理不仅仅是一个单一的模式。此外，该方法应该扩展到不仅处理扩展的线性数据结构，而且处理树状和更一般的结构。该方法还应该扩展到能够处理存储在动态数据结构的节点中的一些此外，人们可以考虑扩展该方法以使用完整的抽象-检查-细化范式，即通过排除某些模式的使用，在发现一些虚假的反例后能够恢复最后，一个有趣且具有挑战性的问题是不仅要考虑安全性的验证，还要考虑活性，这是一个在大多数动态数据结构程序的验证技术中非常开放的领域引用[1] M. 博兹加河Iosif和Y.Lakhnech 无存储语义学和无存储逻辑。在PEPM'03的程序ACM Press，2003.[2] A. Bouajjani，P. Habermehl，P. Moro，and T.沃伊纳尔在常规模型检查中使用动态1-选择器链接结构的编译程序。在TACAS'05的Proc.施普林格，2005年。[3] A. Bouajjani，P. Habermehl，and T.沃伊纳尔抽象规则模型检查。在Proc. ofCAVSpringer，2004.[4] A. 德语指针的跨过程May-Mayer分析：超越k-极限。在PLDI'94的程序中ACM Press，1994.[5] N. Immerman，A. Rabinovich，T.代表，M. Sagiv和G.约什通过结构模拟进行验证。在CAV'04的程序Springer，2004.[6] HBM混蛋抽象存储结构。语言学。IFIP，1981年。[7] O. Lee，H. Yang和K.逸使用基于文法的形状分析自动验证指针程序。在ESOP'05的程序施普林格，2005年。[8] A. Loginov，T. Reps和M.萨吉夫通过归纳学习进行抽象细化。出现在2005年CAV'05的Proc.[9] N. Klarlund和A.莫勒Mona 版本 1.4用户手册BRICS，丹麦奥胡斯大学计算机科学系，2001年。[10] A. Møller和M.I. 施瓦茨巴赫 指针断言逻辑引擎。在Proc. PLDI '01，2001。另见2001年5月SIGPLAN第36（5）号通告M. Ceškaetal. /《理论与计算科学》145（2006）113130[11] S. Sagiv，T.W. Reps和R.威廉通过三值逻辑的参数形状分析。TOPLAS，24（3），2002.[12] A. 维内特无类型程序指针别名的自动分析。计算机程序设计科学，35（2），1999。[13] A.维内特 一种可扩展的嵌入式程序非均匀指针分析方法。在SAS'04的程序 施普林格，2005年。[14]T. Yavuz-Kahveci和T.布尔坦使用计数器自动验证并发链表。在SAS'02的Proc.施普林格，2002年。[15]T.亚武兹-卡维奇并发软件系统的规范和自动验证。PhD.论文，加州大学计算机科学系，圣巴巴拉，加利福尼亚州，美国，2