→→可在www.sciencedirect.com在线获取理论计算机科学电子笔记287（2012）29-40www.elsevier.com/locate/entcs基于XML的八角形Eva Beckschulze，Stefan Kowalewski，1，2德国亚琛工业大学嵌入式软件实验室JoürgBrauer3Veri Fied Systems InternationalGmbH德国不来梅摘要基于XML的本地化是一个两步过程。 首先，确定在过程中访问的抽象存储器位置的集合。然后，在随后的固定点迭代中，相应过程的输入被减少到那些确实被访问的变量，从而节省时间和内存。 的本文的主题是基于访问的八角形抽象域的本地化。对于经常出现的场景，只有一个八角形约束中的两个变量包含在一个过程的访问集中，有各种机会如何实现本地化。本文提出了三种不同的方法，如何处理这样的约束。尽管应用于抽象状态空间的子集，但这些方法中的两种保持精度，即，抽象的状态空间和不进行定位的情况保留字：局部化，八角形域，过程间分析1介绍抽象解释的关键思想[4]是系统地从程序的复杂、具体的语义中 给定分别描述具体值和抽象描述的具体和抽象域C和D，抽象解释的关键思想是模拟每个具体操作f：C的执行C在程序中使用抽象模拟g：DD. 以来具体语义可以表示为方程组，计算相应的抽象语义相当于定点迭代，直到结果稳定。1 支持DFG EXC 89。2电子邮件：beckschulze，kowalewski@embedded.rwth-aachen.de3电子邮件：brauer@verified.de1571-0661 © 2012 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.09.00430E. Beckschulze等人/理论计算机科学电子笔记287（2012）29∈∈1.1定点迭代在抽象解释中设计固定点计算时，效率是一个非常重要的问题。当然，所选择的抽象域强烈地限制了收敛到固定点所需的迭代次数。然而，与所选择的抽象领域无关，效率低下通常源于另外两个因素：• 由于抽象操作g将输入上的抽象状态d D转换为抽象输出dJD，因此每个dJ（或其变体）从程序中的每个位置传播到其后继者。如果一个程序构成了一个很大的数字，变量的状态，每个状态都相当大，需要大量的内存。• 为了检测固定点，需要将新计算的状态与前一次迭代中获得的状态进行比较。在最坏的情况下，固定点检测相当于比较两个完整的状态，这可能是显着的大小。最近，因此有越来越多的兴趣在本地化的抽象解释，技术是基于限制状态的子集，这是足够的计算在给定的上下文中的声音抽象的想法，基于在相应的上下文中本地1.2通过本地化提高性能基于内存的定位[8]是一个两步过程：首先，使用高效的对内存不敏感的预分析保守地估计代码块中访问的内存位置。第二，运行实际分析，将代码块的输入状态简化较小的状态可以提高固定点计算的性能。上面讨论的问题此外，较小的输入状态降低了必要的迭代次数，因为如果只有抽象状态的那些部分在过程中未被访问，则不需要对过程在[8]中，基于访问的本地化被应用于非关系区间域。对于每个抽象元素的二次内存成本和某些操作的三次时间成本，效率在八边形域中也是一个很大的问题[7]。然而，与间隔相比，八边形的关系性质需要不同的技术来避免精度损失。在本文中，我们讨论了三种不同的方法来访问为基础的定位八角形，其中两个不招致精度损失1.3捐款概要本文具体提供了以下对八边形抽象域的基于访问的本地化的贡献• 我们讨论了三种不同的策略，以确定这些限制，可能是相关的上下文中。• 我们在一个单一的框架内正式这些策略，并提供了一个最优性标准。• 我们提出了一个实验评估，比较两者，运行时和E. Beckschulze等人/理论计算机科学电子笔记287（2012）2931∈± ±≤± ±∞1次 intpublicvoid run（）{2if（... ）的第一个字符。三......4g（）;（五）6其他七...8h（）;（9）10}11空隙public voidrun（）12x++;13}141516空隙public voidrun（）0=0;18}Fig. 1. 示例C程序这些方法对于一组用C编写的基准测试的精度。这些捐款的列报结构如下。第二节首先通过一个实例介绍了不同的本地化策略然后，在第3节中，我们引入了局部化中约束的意义的形式概念。这一概念完善了经典的基于访问的依赖性观点。不同的本地化策略，然后正式在第4节，实验证据之前，在第4节。五、最后，本文总结了Sect.6和一个结论节。第七章2样例区间分析与八边形分析的关键区别。局部化是这样一个事实，即前者传播非关系区间，而后者传播将一个变量与另一个变量相关联的约束。为了说明这一重要差异及其对本地化的影响，我们讨论图1中的示例。我们假设预分析确定了函数中访问的变量集，表示为Acc。假设此步骤产生以下集合：Acc（f）={x，y}，Acc（g）=Acc（h）={x}已经表明，考虑到这种形式的访问信息[8]的函数g的基于区间的分析需要仅考虑x以收敛到合理的过近似。同样，将h的输入状态限制在描述x的区间内也是足够的。变量y在这些函数中不被访问;其对应的间隔在g之前（分别为f）因此与分析g（resp.h）的情况。2.1三角形集和八角形使用八边形，状态由形式为v1v2c的约束的合取组成，其中v1和v2是程序变量，cZ是常数值。在剩余部分中，我们假设所有变量都是整数，尽管我们的结果同样适用于实值或有理八边形。为了使演示更容易理解，我们将示例限制为几个约束，并假设对于所有未指定的约束，v1v2=特别是，我们不推导出所有的隐式约束，而是在Sect中单独处理它们3 .第三章。假设调用点g的输入状态（图4中的第4（1）由32E. Beckschulze等人/理论计算机科学电子笔记287（2012）29≤≤∈≤∈/∈≤≤≤≤{}/∈± ±≤≤{}∈≤ ≤∈≤八角形：（x≤ 4）（y≤ 0）（x+y≤ 2）显然，不需要将约束（y 0）的y的界限转移到g因为y不在g内被访问。 通过对比，由于x Acc（g），我们传播 （x个 4)变成g. 因此，对于约束（x（4）情况与因为八边形没有规定x和y之间的关系然而，对于xAcc（g）和yAcc（g），不清楚如何处理涉及x和y两者的约束。当然，有不同的可能策略来处理这种情况，我们在下面概述了其中的三个。2.2八边形投影到集合上使用这种策略，只有那些八边形约束v1v2c满足v1，v2Acc（g）被传播到g中。 因此，由于YAcc（g），约束x+ y 2）被删除。然而，在g中增加x需要更新所有涉及x的约束。然而，如果在该位置处不存在约束（x+ y 2），则x和y之间的关系的更新丢失。因此，对可靠性的追求迫使我们在分析g之后删除约束（x+假设调用点h的输入状态相同，删除约束不会导致信息丢失，因为赋值x = 0使（x+y2）无效对于g，该方法在图中举例说明2（a）.2.3传递依赖约束现在假设所有涉及x的约束-这里是（x +y 2）-也被转移到g（cp）中。图2（b））。在这种情况下，精度是以较大的输入状态为代价来维持的，并且分析就像在没有局部化的情况下执行一样继续进行。事实上，到目前为止讨论的两种策略都突出了关系域基于访问的本地化的不令人满意的方面.使用第一种方法，所有涉及不包含在相应函数的访问集中的变量的关系约束都被消除，从而将八边形分析的精度降低到区间的精度相比之下，如果存在许多这样的依赖关系，那么将表现出依赖关系的约束转移到访问的变量只会使输入空间的大小略微减小通过引入松弛变量，可以在两种方法之间找到一个实用的中间地带，我们将在下文中讨论。2.4Slack变量在下文中，假设g的输入上的八边形状态由与n个附加约束x + y i配对的（x 4）组成，c i为inN.表示这个八角形O. 注意，我们仍然有Acc（g）=X . 对于每个vAcc（g），我们引入一个新鲜松弛变量v松弛，用v松弛替换o中的v，并用（v松弛−v≤0）（v松弛− v≤0）增加八边形，相当于v=v松弛。因此，我们得到一个（E. Beckschulze等人/理论计算机科学电子笔记287（2012）2933i=1·||||≤ ∧≤−± ±∞- ≤ −≤变换的八边形或松弛定义为：〇slack=（xslack≤4）（x松弛+yi≤ci）<$（x− xslack≤ 0）<$（xslack−x ≤0）在这一点上，我们将减少的松弛传播到涉及Acc（g）和g中的对应松弛变量的约束上。这种构造的关键思想是只将那些包含在其访问集中的变量传播到函数中，但使用松弛变量来跟踪这些变量的更改。因此，传播到g的八边形范围超过2个Acc（g）变量。由于Acc（g）与变量的总数相比通常很小（并且可以使用旁路等技术进一步减少[10]），因此这种方法显着减少了八边形的大小。将x以g递增，得到修改后的八边形：（x≤ 5）<$（x− xslack≤ 1）<$（xslack−x ≤−1）这个八边形是在g（cp）之后的分析的输出。 图2（c））。 将此结果与o结合会产生一个八边形，该八边形隐式地将g的输出上的x与y 1，...，yn到x松弛。因此，剩下的步骤是使用存在量化从联合八边形中消除x松弛，从而使x和y之间的隐式关系为1，...，yn explicit，给出：n（x 5）（x+ yici+ 1）i=1消除可以作为闭包来实现[3]。重要的是要认识到，如果x被分配一个完全不相关的值，如图1中的h，则该方法也有效。1.一、我们称之为基于访问的方法，因为传输的输入状态直接来自访问信息。考虑到依赖性，我们将第二种方法命名为基于依赖性的方法。在最后一种方法中，xslack被用作将x与其输入值相关联的锚。因此，我们将这种方法称为锚定。3依赖性和重要性在最后一节中，我们假设对于未指定的约束，vivj=。然而，在实践中，通常很少有约束是无界的，因为传递函数要求通过闭合相应的八边形来使所有隐式约束显式化。这是使用修改的Floor-Warshall算法来完成的，该算法迭代地检查所有约束vjvkc和vk vi d是否c+d小于先前为vjvi计算的上限[7]。事实上，众所周知，封闭的八边形通常包含大量的冗余约束（cp。图3（a））。使用基于依赖的本地化，所有依赖于被调用函数的访问集中的变量的约束都被传递给被调用方。因此，基础八边形中的冗余约束在冗余依赖约束中表现出来，34E. Beckschulze等人/理论计算机科学电子笔记287（2012）29我⎪⎩⎪⎨x≤4，y≤0，x+y≤2x≤4，y≤0，x+y≤2x+y≤2x≤4，x+yi≤cix松弛−x≤0x−x松弛≤0y≤0调用gx≤4y≤0调用gx≤4调用gx≤4x松弛+yi≤ci返回x≤5返回x≤5返回x≤5x≤5x≤5x+y≤3x≤5x−x松弛≤1y≤0y≤0x+y≤3x+yi ≤c+ 1x松弛−x≤−1（一）（b）第（1）款（c）第（1）款图二.调用g时转移的约束：（a）仅考虑访问集，（b）也转移依赖约束，（c）引入松弛变量。也被传递给被调用方，即使它们对于分析的输出来说可能是无关紧要的。因此，我们通过显著性来细化依赖的概念，以便减少所涉及的约束的数量在文献[6]中提出了一种消除差分界矩阵（DBM）中冗余的算法，并在文献[1]中适用于八边形域中使用的相干DBM然而，在我们的例子中，冗余只对访问的变量有阻碍作用。为了确定一个约束是否是重要的，它需要确定一个约束是否比通过组合区间获得的约束更严格直观地说，如果一个约束切割了由区间定义的矩形，则它是有意义的，如图11所示。3（b）;这里，x+y小于x和y.在下文中，令V={v1，...，表示程序变量的集合。我们解释八边形o ={σ1，...，σ m}作为形式为σ i=（λ i，1·v i，1+ λ i，2·v i，2≤ c i）的m个线性约束的集合，其中v i，1，v i，2∈ V，λ i，1，λ i，2∈ {0，−1，1}，且c i∈Z。此外，我们假设o是闭的，并定义：定义3.1（依赖约束）令Acc（g）表示被调用方g的访问集。设o表示输入上的八边形然后，g依赖于约束σ i∈ oi <${vi，1，vi，2} <$Acc（g）/=<$。定义3.2（显著约束）对于每个v∈V，设vl和vu表示v的边界，其特征为o。一个约束σi∈o称为有效i<$λi，1·β（vi，1，λi，1）+λi，2·β（vi，2，λi，2）>ci。映射β：（V×Z）→Z定义为：β（v，λ）=λvl ：λ=−1vu：λ= 1从现在开始，我们将o中对f有意义的约束集称为 签名f（o）。在不考虑重要性的情况下，依赖性是一个纯粹的语法标准，用于确定八边形约束是否与被调用方相关。通过考虑重要性，传递给被调用方的约束取决于八角形抽象的状态直观地说，如果一个八边形约束是依赖的并且是重要的，那么它会使用基于依赖性的策略传播到被调用方Gx++;Gx++;Gx++;E. Beckschulze等人/理论计算机科学电子笔记287（2012）2935∪--∪--YXYX(a)（b）第（1）款图3.第三章。（a）对角约束并不比区间界限更精确（b）制约因素X+ Y ≤ c通过灰色三角形减少解空间。4形式化模型原则上，分析一个具体的过程f服从一个八边形输入状态o，相当于将f的抽象对应物f#应用于o。分析的输出是t husf#（o）=oout t。 显然，f#可以被设计为构成f的所有操作的抽象对应物的组合。本地化通过将f#应用于o的子状态来改进这种方法，该子状态（通常）严格小于o。本节正式讨论我们的本地化方法，并提供正确性和最优性标准的参数，以保持精度。4.1分类约束为了检测所有的依赖关系，我们要求八边形输入o到f是闭合的。 如前所述，让Acc（f）是在f中直接或传递访问的变量集。基于Acc（f），输入o=σ1，.，σ m到f被划分为三个不相交的 设置，取决于约束是否相关、是否被忽略或是否可以被丢弃。虽然后两组独立于本地化策略，但相关约束的定义区分了不同的本地化方法• Relevantf（o）表示在计算f时o中相关的约束集合。每种方法的正式定义见下文各段。• 未确定的f（o）由o=σ1，.中的约束组成，σ m是由对f的调用所不确定的，因此在从被调用者返回时仍然有效，即，单约束f（o）={σ ∈ o |vars（σ）<$Acc（f）=}。• 丢弃f（o）描述了o中剩余的约束，这些约束可以被丢弃，因为它们要么是冗余的，要么在返回后会过时形式上，我们得到丢弃f（o）={σ∈o\（相关f（o）<$不相关f（o））}。这些约束集合相对于f划分o，即， o =不确定的f（o）相关的f（o）丢弃f（o）。此外，如果f #表示f的抽象Transformer，则f#的输出o服从o被定义为（cp. 图4）：oout=Una certaintedf（o）f#（Relevantf（o））关于局部化分析的精度，我们陈述以下结果：36E. Beckschulze等人/理论计算机科学电子笔记287（2012）29∪FFF{∈|}Discardf（o）放弃约束O调用f相关性tf（o）未检出f（o）返回oout=未检测f（o）f#（Relevantf（o））f#（Relevantf（o））图四、应用于给定八边形o输入的调用站点的本地化示意图命题4.1当Una ectedf（o）f#（Relevantf（o））与f#（o）一致，局部化保持了原始分析的精确性。在这种背景下，我们现在正式研究不同的本地化方法，特别是相关性的定义。4.2基于XML的本地化使用基于访问的本地化分析f需要将所有与在f中访问的变量相关的八边形约束传播到f中。因此，我们将相关约束集定义为RelevantAcc（o）=σ ovars（σ）Acc（f），并获得关于精度的直接结果：推论4.2一个sv圆盘，其中f（o）≠Si gf（o）=Σ。然后又道：f#（o）=Una ectedf（o）f#（RelevantAcc（o））直观的，基于访问的八角形定位是最佳的，如果所有具有重要依赖关系的变量都在f中重新定义。4.3基于依赖关系的本地化为了避免基于访问的本地化固有的精度损失，我们在相关性的定义中考虑了重要的约束相关Dep（o）={σ∈o|vars（σ）σ∈Sigf（o）}这种构造需要仅丢弃冗余约束。然而，这些约束可以通过关闭f的分析的输出而分别被重新建立和更新，并且因此保持精度。命题4.3基于依赖性的定位是最佳的。4.4使用搜索引擎进行对于这种方法，我们首先确定引入副本（锚）的变量集。要做到这一点，定义出现在FE. Beckschulze等人/理论计算机科学电子笔记287（2012）2937∈∩.F⎪⎩（五）∈Acc（f）v/∈vars（σ））我Jσ∈o重大制约因素如下：sigVarsf（o）=σ∈Sigf（o）vars（σ）使用上面的集合，我们通过将sigVarsf（o）限制为在f的访问集合中找到的那些变量来获得要锚定的变量集合。 对于每个变量vsigVarsf（o） Acc（f），因此我们引入松弛（或锚定）变量v松弛， 辅助约束vslack=v，以给出：oslack=o<$v∈sigVarsf（o）<$Acc（f）（（v−vslack≤0）<$（vslack−v≤0））为了确保相同的约束对vslack和v有效，我们计算增广系统的强闭包。分区应用于增强的输入状态：关联函数An c（oslac k）=εεσ∈oslack。vi，vj∈vars（σ）：vi，vj∈Acc（f）<$通过观察基于锚点的定位精度与基于依赖关系的方法的精度相同，我们总结了对不同定位策略的阐述命题4.4基于锚点的定位是最佳的。5实验我们在Java中实现了不同的八角形本地化策略。我们的框架提供了一个八边形域中的一个对上下文敏感的抽象解释我们分析的基准测试由许多程序组成，例如，实现排序算法或执行整数运算。没有本地化，即，考虑到程序中所有点的所有变量，我们的分析器在几分钟后就会耗尽内存，消耗大约1GB的RAM。局部化的总体结果见表1。1.一、其中，Acc指的是基于访问的方法，Dep指的是基于依赖关系的方法，Anc指的是锚定。除了运行时，我们还确定了在分析过程中发现的不同过程上下文的数量，用于表示八边形约束的DBM的平均大小，约束的总数以及重要约束的部分。有趣的是，与Acc相比，使用Dep和Anc跟踪过程调用的变量数量仅略多。然而，使用Dep和Anc的过程间分析更精确。与Oh等人[8]报告的结果类似，我们观察到定位减少了必要的程序重新分析的数量。 这是因为它通常情况下，只有八边形中的约束会发生不相关的变化用于分析被呼叫者。分析的不同上下文的数量越少，38E. Beckschulze等人/理论计算机科学电子笔记287（2012）29方法运行时#context矩阵尺寸#约束标志. 约束ACC26 S13718.715678980.63%DEP36 S21123,5510312111.21%ANC34 S13220.616254590.67%表1本地化的结果表明基于访问的本地化和锚定受益于本地化的输入状态。通过比较，基于因变量的依赖性方法具有更大的输入状态，并且程序需要比使用其他策略之一更频繁地跟踪。我们实验的一个值得注意的副产品是语义上重要的约束的总体数量很少这一结果证实了Bagnara等人的观察结果[1]，他们指出（封闭的）八角形系统的大部分通常是冗余的。因此，基于语义依赖的本地化导致比基于句法基础确定依赖的标准更少的约束。6相关工作早期的本地化方法主要集中在可达性上，这是一个比考虑访问集粗糙得多的标准，在有效性方面有预期的缺点。 关于这一领域相关工作的调查，我们参考[8]，在引入基于访问的本地化的上下文中进行了全面的讨论。作者[8]还将局部化扩展到过程边界的区间 任意代码块。对于八边形域，也可以使用相同的技术来调整这种方法。独立于所选择的数值域，基于访问的本地化的效率取决于这样一个事实，即通常全局变量不必要地被携带在许多节点上，直到它们最终在调用树的深处的子例程中被访问。最重要的是，程序中访问的所有全局变量都被认为是main函数的输入状态。在[10]中，引入旁路的概念以减轻这种效应。其思想是绕过变量的抽象值传递调用过程，而不是通过过程体传播它们。这种针对区间域实现的思想也可以转移到八边形域。然而，由于八边形的关系性质在每个调用站点，需要派生所有隐式约束，以便将更新的约束和依赖关系传播给被调用方。其他相关的工作可以在处理复杂抽象域的大型抽象状态的工作中找到。 只有少数变量可以相互关联的变量包装是一种使关系域在内存消耗和分析时间方面可行的方法[5]。对于八边形抽象域，八边形包装[7]，即，基于程序中的可观察依赖性来例如，if语句中的控制变量将被分配给包含在相应的then块（和else块）中访问的变量的包，因为存在直接依赖关系E. Beckschulze等人/理论计算机科学电子笔记287（2012）2939这些变量之间八角形包装已成功地集成到静态分析器中，从而将内存消耗减少到合理的数量，同时仍然实现令人满意的精度[2]。使用局部化来减少抽象状态的大小可以被看作是与八边形包装正交的方法。这两种方法都减少了内存消耗和计算成本。通过比较，我们的方法保证了最大的精度，而八边形包装不，因为不是所有的约束。在[11]中，Venet和Brat报告说，基于语法标准静态确定的变量包他们考虑了使用DBMs进行涉及指针变量和数组索引的分析的问题。然后，解引用的评估基于基址和操作集，两者的值都是从抽象状态中提取的。他们的解决方案是在分析过程中，每当一个操作导致与不同DBMs相关联的变量之间的新关系时，这样，所有关系都是以永久重组DBM为代价的。此外，该过程不包括本地化，使得许多约束不必要地沿着许多路径传播。[9]中提出的稀疏分析框架应用了一种更严格的本地化形式，它基于（近似）数据依赖性（类似于def-use-chains）而不是控制流。设计稀疏分析的关键在于为特定的抽象域选择适当的近似定义集和使用集。对于稀疏关系分析，定义集和使用集由如上所述的预分析确定的包组成。确定本地化和大小缩减的两个步骤，它们的过程在我们的方法的执行顺序中有所不同：[9]中的稀疏关系分析从确定提供小八边形的八边形包装开始。随后，数据依赖性方面的本地化应用于包。作为对比，我们从本地化变量开始，然后基于数据依赖性减少八边形的大小虽然这两种方法都在朝着更有效的方向发展，但它们在接受信息丢失方面存在分歧7结论在本文中，我们重新讨论了基于访问的本地化，并确定了仅使用访问集或变量之间的语法依赖关系的方法的缺点。即使基于访问的本地化已被证明是精确的间隔，（弱）关系域，如八边形施加不同的需求的本地化策略，以捕捉暴露的关系，而不传播太多的冗余约束。因此，我们提供了一种基于依赖性的技术，该技术基于重要约束的概念。锚定方法又是基于用辅助（松弛或锚定）变量来增强输入状态以跟踪过程的输入和输出上的值之间的差异40E. Beckschulze等人/理论计算机科学电子笔记287（2012）29引用[1] 巴尼亚拉河P. Hill和E. Za Zanella，Weakly-Relational Approach for Numeric Abstractions：ImprovedAlgorithms and Proofs of Correctness，Formal Methods in System Design35（2009），pp. 279-323[2] 布朗切特，B.， P. 库索河Cousot，J. 费雷特湖 Mau borgne，A. 我的天。 Monniaux和X. Ri val，大型安全关键软件的静态分析器，PLDI（2003），第100页。196-207.[3] Bozga，M.，C. Girlea和R. Iosif，Ite ratingOctagon s，in：TACAS，LNCS 5505（2009），pp. 337-351[4] Cousot，P. and R. Cousot，Abstract Interpretation：A Unified Lattice Model for Static Analysis ofPrograms by Construction or Approximation of Fixpoints，POPL，1977，pp.238-252。[5] Cousot，P.，R. Cousot和L.Mauborgne，一个可扩展的分段决策树抽象域，在：时间验证，纪念阿米尔Pnueli（2010年），pp。72比95[6] Larsen，K.，F. Larsson，P. Pettersson和W. Yi，实时系统的有效验证：紧凑的数据结构和状态空间约简，RTSS（1997），pp.14比24[7] 我的儿子，八边形Abst ractDomai n，Higher-OrderandSymBolicComputation19（2006），pp. 31比100[8] 哦，H.，L. Brutschy和K. Yi，Access Analysis-based Tight Localization of Abstract Memories，in：VMCAI，LNCS6538（2011），pp. 356-370。[9] 哦，H.，K.休，W。李，W。Lee和K. Yi，类C语言稀疏全局分析的设计和实现，PLDI（2012）。[10] 哦，H。和K. Yi，基于网络的本地化与路由，在：APLAS，LNCS7078（2011），pp. 50比65[11] Venet，A.和G. Brat，Precise and Efficient static array bound checking for large embedded Cprograms，PLDI（2004），pp. 231-242.
我的内容管理
展开
