八边形稀疏保持算法的性能与精确度的研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记331（2017）57-70www.elsevier.com/locate/entcs八边形的稀疏保持算法雅克-亨利·阿格丹MPI-SWS，Inria Paris摘要用于操纵八边形的已知算法不保持它们的稀疏性，通常导致二次或三次时间和空间复杂性，即使当它们都有界时变量之间的关系是未知的。在本文中，我们提出了新的算法，它使用和返回的八边形表示为弱封闭的差分界矩阵，保持其输入的稀疏性，并在其输入稀疏的情况下有更好的性能。我们证明，这些算法是精确的已知的。关键词：数值抽象域，八角抽象域，静态分析，静态分析器1引言为了捕捉程序的数值属性，静态分析器使用数值抽象域。 静态分析器中数值抽象域的选择是精确度、捕获复杂数值特性的能力和性能之间的折衷。 非关系抽象域，如区间[6]，非常有效，但相对不精确：它们不能表示程序变量之间的关系。另一方面，为了捕获程序变量之间的数值关系，可以将它们表示为线性不等式。这类关系数值抽象域是由线性抽象域构成的。线性抽象域对应于不同的精度与性能权衡：它们的范围从不太精确、有效的区域[13]、五边形[12]或八边形[13，14]到更精确、昂贵的区域，如子多面体[11]、八面体[5]、每个不等式两个变量[16]、zonotopes [15]或一般多面体[8]。特别是，八角形抽象域[13，14]准确地表示了程序中出现的许多它在静态分析社区中非常流行，这解释了为什么算法改进[3，1，17]和精度改进变体[4]会定期发布。1这项工作得到国家研究机构ANR-11-INSE-003的支持http://dx.doi.org/10.1016/j.entcs.2017.02.0041571-0661/© 2017作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。58J. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）正如Astrée [7]的设计者所报告的那样，其二次或三次性能仍然使其无法使用合理数量的变量。 实际上，通常用于表示八边形抽象值的数据结构，即，强闭差界矩阵的上界或下界已知，其变量的数量为二次型。一个常见的解决方案是使用变量包装[13，§8.4.2]，其中八角抽象域仅用于变量的小包。打包的缺点是不在同一个包中的变量之间没有关系存储。 已经引入了一种包装变体来减轻不精确性[2]，但仍然可能发生精度损失八边形的性能问题已经被研究过了：特别是，Singh等人。[17]提出了一种在其表示是稀疏的情况下优化的八边形抽象域的实现。但他们没有解决的事实，即它是密集的，只要区间界限是已知的许多变量，我们预计，由于这个原因，稀疏性是非常低的，在他们的实施。相反，在本文中，我们建议使用Octagon抽象域的新算法：这些算法工作在八边形的稀疏表示上，使得分析两个独立变量集的成本是成本之和两组变量的分析，独立进行。我们的算法具有与传统算法相同的精度。 我们的主要想法如下：为了确保所有操作的最佳精度，表示八边形、差分边界矩阵的数据结构通常保持强闭合：即，算法确保任何返回的差分边界矩阵是最佳抽象。然而，大多数情况下，强闭差分界矩阵是稠密的，因为必要的加强步骤。在本文中，我们提出了削弱保持不变的差界矩阵，并保持它们弱封闭，从而跳过加强步骤。弱闭有界矩阵不一定是稠密的，因此我们可以使用稀疏数据结构来表示它们。我们证明了某些算法在保持不变的情况下，可以在不损失精度的情况下对弱闭有界矩阵进行运算，并对其他运算给出了我们从§2中的初步定义开始。在§3中，我们描述并证明了我们的新算法的可靠性和相对精度 我们在§4中得出结论。2定义设V+是一个有限的变量集。 我们称一个从V~+到R的函数为一个正则的包络函数。常规环境表示程序的数值状态。八角形抽象域的作用是近似正则环境ρ的集合。为此，八边形的抽象域存储以下形式的一组不等式±ρ （ u ） ±ρ （ v ） ≤Cstuvu ， v∈V+（1）这对应于给出ρ值的和与差的界。更多-如果我们两次使用相同符号的相同变量，我们看到，使用这样的约束，我们可以表示环境值的区间约束[13]。J. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）59为了以统一的方式处理这些约束中所有不同的符号组合，我们引入了有符号变量的集合V±。有符号变量有两种类型：它们要么通常是V+的变量，在有符号变量的上下文中称为正变量，要么是它们的相反形式，负变量。我们给V±配上一个对合算子，将每个有符号变量v与它的对立面v相关联，使得v为正当且仅当v为负。正则环境通过取ρ（u）=−ρ（u）而规范地扩展到有符号变量。更一般地，我们将不规则环境定义为从V±到R的函数σ，并将规则环境集视为不规则环境集的子集。正则环境就是满足性质ρv，ρ（v）= −ρ（v）的非正则环境ρ。使用这种新的形式主义，形式（1）的八边形约束可以被看作是ρ值的离散度的上界，ρ是一个规则的环境：ρ（u）−ρ（v）≤Cstuv u，v∈V±（2）这有两个好处：首先，（1）允许的所有不同类型的约束都被分解为一种更简单的形式。其次，我们可以把这些约束看作是对不规则环境的约束，并进一步把它们约束为规则的：我们看到，对八角形抽象域的研究始于对一个更简单的抽象域的研究，在这个抽象域中只有变量的离散性是有界的。这种抽象域的约束集，称为潜在约束，在线性优化文献中得到了很好的研究，因为它对应于加权有向图中众所周知的最短路径问题。这样一组约束表示为差分边界矩阵：有界矩阵（DBM）是一个矩阵（B uv）（u，v）∈V2 的元素R{+∞}。的这些约束的含义由两个约束函数γpot和γoct给出，它们分别与DBM相关联，满足所有约束的不规则或规则环境的集合：γ pot（B）={σ：V±→ R |uv ∈ V±，σ（u）− σ（v）≤ B uv}（3）γ oct（B）={ρ ∈ γ pot（B）|<$u ∈ V±，ρ（u）= −ρ（u）}（4）例2.1考虑V+={x;y;z}是一组三个（位置ve）变量。有符号变量的集合是V±={x;x; y; y ;z; z}。 设A是DBM，使得对于所有其他条目，A xx= 1，A yy= 3，A yz= 1，并且A uv=+∞。集合γoct（A）包含所有环境ρ：V±→R，使得：• <$u∈V±，ρ（u）=−ρ（u）• ρ（x）≤1/ 2，−ρ（y）≤3/ 2且ρ（y）+ρ（z）≤1这种具体化被同化到一组n阶p：V+→R的p位置变量使得p（x）≤1/2，−p（y）≤3/2和p（y）+p（z）≤1。我们将DBM上的自然序关系表示为≤，定义如下：A≤B惠函uv∈V±，Auv≤Buv（560J. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017））J. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）61≤⊆≤≤{−}⊆下面的简单引理指出，这种顺序关系使γpot和γoct增加，这使得八角形抽象域2的比较算子成为一个很好的候选：引理2.2设A和B是两个DBM，使得A ≤ B。然后，我们有：γpot（A）γpot（B）γoct（A）γoct（B）对于任意非正则环境的非空集合S，存在一个极小的（在意义上）DBM来逼近它，即存在一个极小的DBMα（S）使得S γpot（α（S））. 这个属性直接从定义中得出 关于α：α（S）uv=supσ（u）σ（v）（6）σ∈S这个函数称为抽象函数。我们可以很容易地看到，α是一个递增函数。此外，α不仅返回γ pot的最佳抽象，而且返回γ oct的最佳抽象：如果集合S仅包含正则环境，我们可以看到α（S）也是最小DBM，使得Sγ oct（α（S））。事实上，很容易看出，定义了一个在DBMs上用底元素扩展的完全格，并且对（α，γpot）和（α，γoct）形成伽罗瓦连接。2.1闭包和强闭包许多DBM具有相同的具体化。这是一个问题，因为我们操作的抽象环境不一定是最精确的，这可能导致不精确。因此，通常，八角形抽象域的实现保持不变，即它只操纵这样的一个重要的事实是，我们可以使用它们包含的值来描述最好的抽象，并且我们有算法来计算它们。我们将这些特征与这些算法一起此外，我们给出了一个较弱的封闭性条件DBMs，这并不确保规范性，但允许更好的算法，而不损失精度。2.1.1最佳γ罐第一步是注意到规范DBM总是具有零对角值。此外，规范DBM应该总是验证三角不等式。我们称这种DBM为封闭 DBM：定义2.3[封闭DBM]封闭 DBM是验证以下两个属性的DBMB• Bv∈V±，Bvv= 0• uvw∈V±，Buw ≤Buv+Bvw2正如我们在§3.1中看到的，这不是我们在实现中用作比较运算符的顺序关系。Octagon abstractdomain的缩写。62J. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）∈.;B闭DBM是γpot的最佳抽象[13，定理3.3.6]。因此，封闭的DBM总是有非空的具体化。我们在这里不详细介绍用于检测DBM具体化的空性和计算闭包的算法：相反，我们请感兴趣的读者参考以前的工作[13，1]。例2.4例2.1中定义的DBMA的闭包α（γpot（A））包含以下附加的有限元素：• α（γpot（A））uu= 0• α（γ pot（A））yz= 4（对应于约束ρ（z）−ρ（y）≤4）。2.1.2γoct的最佳抽象现在我们将闭包的概念重新定义为γoct的标准型。很容易看出，对于任何正则环境的非空集合S，α（S）uv=α（S）vu。因此，γoct的规范DBM将验证相干性质：定义2.5[相干DBM] A DBMB是相干的，当：uv∈V±，Buv=Bvu此外，Buu（对于uV±）形式的矩阵元素对ρ的值施加了区间约束。这些区间约束可以结合起来，以约束ρ值的任何差异。 因此，γoct的标准型将验证以下强封闭性：定义2.6[强闭DBM] A DBMB是强闭的，当它是闭的和相干的，并且：Buv ≤Buu+Bvv2这个条件是充分必要的：强封闭性是γoct的典型DBM的特征.定理2.7设B是DBM。以下两个属性是等效的：(i) B是强闭的(ii) γoct（B）B=α（γoct（B））证据 参见，例如，[13，定理4.3.2和4.3.3]。Q通常[1]，为了计算强闭包，首先确保给定矩阵是相干的，然后计算闭包（即，γpot意义上的规范代表），最后，执行所谓的强化步骤3：定义2.8[加强]设B是DBM。 加强B，注意到S（B）的定义为：S（B）uv=minBuu+Bvv2紫外线[3]这实际上是Miné[13]最初描述的方法的改进。ΣJ. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）63下面的定理陈述了上面概述的强闭包算法的正确性，包括计算闭包，然后是加强：定理2.9设B是相干DBM，其中γoct（B）/=α（γoct（B））=S（α（γpot（B）- 是的然后又道：特别地，如果B是凝聚闭的，则S（B）是强闭的。证据 参见，例如，[10，定理8.2.7]。Q例2.10为了考虑例2.1中定义的DBM A的强闭包，我们首先需要使e itcohere nt：让A表示包含与A相同的元素的DBM，除了A=y=1。A的闭包包含以下附加的有限元素：• α（γpot（A））uu=0• α（γpot（A））zy=α（γpot（A））yz=4（对应于约束条件ρ（z）−ρ（y）≤4）• α（γpo t（A））zz=5（对应于约束tρ（z）≤5/2）。然后通过加强α（γpo t（A<$））得到强闭包α（γoc t（A<$））. 加强操作将创建以下新条目：• α（γoct（A））xy=α（γoct（A））yx=2• α（γoc t（A））xz=α（γoc t（A））zx=3。2.2弱封闭性通常，八角形抽象域的实现保持所有DBM强闭，以便在执行抽象操作时知道最大信息然而，这破坏了稀疏性：实际上，Buu形式的矩阵元素是变量的非关系区间界限：因为我们期望许多变量是有界的，所以加强步骤为许多DBM单元提供了有限界限，并且加强的DBM失去了大部分稀疏性。一般来说，DBM在变量的数量上具有二次大小，因此这种稀疏性的损失是昂贵的。以前尝试使用稀疏性来提高性能[17]，但没有观察到这种情况。我们相信，当使用这些实现时，DBMs很快变得密集，从而降低了稀疏算法的效率。在我们的算法中，我们建议跳过加强步骤：而不是保持所有被操纵的DBM都是强封闭的不变式，我们保持它们是弱封闭的不变式：定义2.11[弱闭DBM]设B是一个DBM。我们说B是弱闭的，当以下两个等价的陈述中的任何一个成立时：(i) B有零对角，S（B）是强闭的;(ii) B具有零对角，S（B）是相干的，并且：uvw，S（B）uw≤Buv+Bvw（7）64J. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）≤证据这 两个定义的等价性证明在[10，定义8.2.5]中。Q为了确保我们不会失去精度，我们将证明对于这些运算符中的每一个，它都以与使用相同的具体化来计算抽象值。通常的算法。等价地，我们证明了由我们的算子计算的抽象值的加强等于由通常的算子计算的加强参数的抽象值。弱闭DBM既不一定是强闭的，也不一定是闭的。然而，一个封闭的和连贯的DBM总是弱封闭的：这有助于我们从任意的八边形约束集合中轻松构建弱封闭的DBM例2.12根据例2.1的定义，α（γpo t（A））是闭的且相干的，因此是弱闭的。该DBM不包含与变量x和其他变量相关的条目这是稀疏性的一个改进闭包α（γoct（A））. 据我们所知，这次行动是不可能的如前所述，[17]。这个弱闭性的概念已经由Bagnara等人引入。[1，Ap-pennsylvania A]作为证明紧闭包算法正确性的中间概念（见§3.5）。据我们所知，使用弱封闭性作为操作稀疏DBMs的不变量是我们工作的原始结果。3关于有界矩阵的八边形的抽象域定义了几个操作差分边界矩阵的操作。它们包括格操作，如比较和连接，以及抽象传递函数，这些函数对程序中的状态变化在本节中，我们回顾了这些运算的标准定义，并给出了弱闭DBM上的新的稀疏保持定义所有这些算法都保持了DBM的稀疏性和弱封闭性，并且可以被证明与标准算法一样精确。更准确地说，我们声称，他们总是返回DBM的加强等于DBM，将已返回的传统算法。[10，8.2.7节]中详述的加宽操作的实现更加复杂，由于缺少空间而被省略。3.1比较为了在静态分析器中使用八边形，我们需要定义一个比较运算符，取两个DBM并返回一个布尔值。如果这个布尔值为真，那么我们保证第一个操作数的具体化包含在第二个操作数的具体化中。一个很好的候选者是DBM之间的自然顺序关系。它的可靠性由γoct的单调性保证。在八角形抽象域的通常实现中，DBM保持强闭，因此这个运算符实际上尽可能精确：当且仅当包含具体化时，它返回trueJ. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）65∈X锅Oct然而，在弱闭DBMs的设置中，该属性不成立。为了在仍然使用稀疏DBM的同时不损失精度，我们需要另一个比较运算符，当它们不需要右操作数时，它可以加强左操作数的边界：定义3.1[弱闭比较]设A和B是DBM。A和B的弱闭比较，记为A≤弱B，定义为：A≤B组A≤BAuu+AvvB ≤B弱UV UV2UVu，v∈V±Buv+∞也就是说，对于B上的每一个有限界，我们首先检查它是否直接被A中相应的界所蕴涵，然后尝试使用非关系界来蕴涵它。下面的定理指出，它实现了对具体化的比较，因此我们可以在稀疏上下文中使用它而不会失去精度：定理3.2设A是弱闭DBM，B是任意DBM。以下两个语句是等效的：(i) γoct（A）γoct（B）(ii) A≤弱B证据 参见，例如，[10，定理8.2.9]。Q3.2忘记变量Octagon抽象域提供的一个重要操作是forget。当给定一个DBM和一个变量v时，它返回另一个DBM，其中关于v的所有信息都被遗忘了。它的具体和抽象定义如下：定义3.3[具体遗忘]设xV+和S是正则环。我们定义：Foct（S）={σ +[x <$r; x <$−r] |σ ∈ S，r ∈ R}定义3.4[抽象遗忘](i) 设x ∈V±，B是DBM.我们定义Fx（B）DBM使得：如果u=v=x，X∞Fpot（B）uv=+否则，如果u=x或v=xUVUV否则(ii) 设x∈V+，B是DBM. 我们的定义：x x xFoct（B）= Fpot（ Fpot（B））这是来自八角形文献[13，定理3.6.1和4.4.2]的已知结果所以Fx适用于任何DBM时都是合理的。 此外，当应用于任何66J. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）OctOctOctOctOct∪∪≤∪±UV2UV2强闭DBM，它是精确的，并返回强闭DBM。对这些性质，我们为弱封闭性添加类似的性质，让我们使用Fx原样对于不损失精度的弱闭DBM：定理3.5LetB是一个弱的DBM且x∈V+. 我们有：（i）S（Fx（B））=Fx（S（B））(ii) Fx(iii) Fx （γoct（B））=γoct（Fx（B）弱闭（B））Oct证据 参见[10，定理8.2.11]。Q3.3加入DBM上的常用连接运算符是≤的最小上限运算符定义3.6[DBM最小上界]设A和B是两个DBM。DBMs上的最小上限可由下式定义：uv，（A<$B）uv= max{Auv;Buv}序关系和算子清楚地形成了一个上半格，因此伽罗瓦连接的通常性质保持不变，提供了关于该算子的可靠性和精度的通常结果：是可靠的，并且，如果给定强闭DBM，它返回近似具体并集的最佳强闭DBM。对于弱闭DBM，即使是合理的，它可能会失去精度时，适用于非强封闭DBMs。例如，弱闭DBMA表示关于正变量x和y的两个不等式：x+x≤1y+y≤0弱闭DBMB又表示以下两个不等式：x+x≤0y+y≤1不等式x+y≤1/2既不存在于A中，也不存在于B中，尽管它存在于S（A）和S（B）中。因此，A<$B包含不等式x+x≤1和y+y≤1，但不需要x+y≤1/2，而需要S（A）<$S（B）。这个例子背后的基本原理是，连接可以创建一些在一个或两个操作数中不存在的关系。我们的操作员必须考虑这个事实。然而，应该注意不要通过在矩阵中引入虚假的有限值来破坏操作数的稀疏性。弱闭DBMs的连接定义如下：定义3.7[八边形的弱闭连接]设A和B是两个弱闭的DBMs。 对于u，我们取v∈V ，B1/2=Buu+Bvv A1/2=Auu+Avv。 弱closed join的定义有两个步骤：J. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）67弱⎪（B弱- ≤∈CIBB如果 BvvA.A.vvBuvA）UV如果(ii) 设u，v∈V±. 我们定义：好 吧（A/50/2000）（A）B）、=MaxB）紫外线加里夫AB弱UV⎪⎩(A∪0uv机B）紫外线uu uu vv vv否则第一步可以通过迭代所有矩阵元素来计算，在A和B中不同。因此，第一步保留了稀疏性，并且仅对两个分支中不同的变量消耗计算时间。第二步可以通过首先在一个列表中收集所有的变量u，其中Auu Buu，并且在另一个列表中，所有的变量u，其中Buu Auu。通过在两个列表上迭代，我们可以有效地只修改满足给定条件的单元格应该注意的是，我们在第二步中只打破了需要打破的稀疏性，因为修改后的单元格对应于连接创建新关系信息的情况（如上面的例子）。下面的定理表明，这个修改后的连接运算符可以用于弱闭DBM，而不会失去精度或可靠性：定理3.8设A和B是两个弱闭DBM。我们有：(i)S（A<$weakB）=S（A）<$S（B）(ii) γoct（A<$weakB）=γoct（α（γoct（A）<$γoct（B）(iii) A弱B弱闭证据 参见[10，定理8.2.13]。Q3.4假设约束抽象域的一个重要操作是假设原语，它使用近似环境集合上的新假设来细化抽象域的内部状态。在本节中，我们只考虑这种操作是精确的情况，即，它不会导致任何近似。这些情况相当于假设ρ（x）ρ（y）C，对于CR和x，y两个变量。 为了为了处理任意的线性不等式，甚至任意的算术约束，需要为八角形域编写一些支持模块，将任意的约束转换为精确的约束。这样的支持模块是出于本文的范围：我们请读者参考[13]以了解更多细节。此外，注意≤B二分之一UV二分之一、68J. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）∈∈锅锅OctOctOct一弱≤弱Oct弱锅锅Oct弱假设与忘记的组合让我们模拟变量赋值4，因此我们在本文中不详细描述变量赋值。我们给出了两个版本的假设原语：一个适应于γpot，一个适应于γoct。我们首先给出这个操作的具体语义，这对于不规则和规则环境是相同的：定义3.9 [假设具体的约束条件]设CR，x，yV±和S是一系列不规则的环境。我们定义：A x−y≤C（S）={σ ∈ S |σ（x）− σ（y）≤ C}很容易看出，我们可以在DBMs中精确地反映这种操作。实际上，如果旧值大于新值，则可以更改与新约束对应的单元格。然而，这并不保持任何类型的封闭性，无论是正常封闭性，强封闭性还是弱封闭性。因此，在插入新约束时需要运行闭包算法。这些算法是昂贵的（即，立方复杂度），并且不利用输入矩阵已经几乎闭合的事实。为此，已经开发了具有二次复杂度的增量闭包算法。我们在这里给出了这些算法的一个稍微不同的介绍，作为Miné [13]最初给出的算法定义3.10[假设抽象的约束]设C∈R，B是DBM，x，y∈V±。(i) 我们定义Ax−y≤C（B）DBM，使得对于u，v∈V±：Ax−y≤C（B）uv= min{Buv;Bux+C+Byv}(ii) 如果x，y∈V+，则定义Ax−y≤C（B）且Ax−y≤C（B）为：Ax−y≤C（B）=Ay−x≤C（Ax−y≤C（B））Ax−y≤C（B）=S（Ax−y≤C（B））众所周知[10，定理8.2.14]，当应用于具有零对角线的DBM。当应用于强闭DBM B（0 ≤ C + Byx）时，结果是强闭的. 因此，假设原语在强闭设置中的实现首先检查是否0 ≤ C + B yx。如果是，则返回Ax−y≤C;否则返回。特别地，当应用于弱闭DBM时，x−y≤C是合理且精确的，因为弱闭DBM具有零对角线。 由于该操作员使用S，它破坏了稀疏性。使用弱闭DBM的优点在于，不再需要弱闭DBMs，S的设置：可以使用Ax−y≤C如果实现额外检查0 2C+Byy+Bxx，则按原样执行。下面的定理总结了这个结果，并证明了在稀疏DBM的上下文中使用这个传递函数而不损失精度：4然而，一个有效的实现将使用一个特定的、优化的实现来分配任务。J. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）69弱弱弱Oct2.定理3.11L∈C ∈R，B可表示为DBM，x，y∈V+。我们有：(i) 如果0≤ 2C+Byy+Bxx，则S（Ax−y≤C（B））=Ax−y≤C（S（B））弱(ii) γoct（Ax−y≤C（B））=Ax−y≤C（γoct（B））Oct(iii) 如果B是弱闭的，则下列语句等价：(i) Ax−y≤C（γoct（B））/=π(ii) 0 ≤Ax−y≤C（B）xx(iii) 0≤C+Byx和0≤2C+Byy+Bxx(iv) Ax-y≤C（B）是弱闭的。证据 参见，例如，[10，定理8.2.15]。Q3.5收紧Miné [13] and Bagnara et al.[1]研究八角形抽象域的情况，当所考虑的环境只取Z中的值时：与前面的部分相反，在这种情况下，强闭DBM并不都是规范的，因此需要使用修改的算法我们在这里解释弱闭集的使用与整数的情况是兼容为此，我们定义了不同的具体化函数γZ，具体化到整数环境：定义3.12[八边形的具体化]设B是DBM。我们定义：ZOct（B）={ρ∈γoc t（B）|<$u∈V+，ρ（u）∈Z}如果我们只考虑整数环境，最好的抽象具有稍微更强的特征。这样的DBM被称为紧密闭合的。我们还定义了弱紧闭DBM的概念，它是整数情况下弱闭定义3.13[紧闭包]设B是DBM。B是紧闭的（分别是弱紧闭的），当：• B是强闭的（弱闭的）• uv∈V±，Buv ∈Z• u∈V±，Buu∈Z紧闭DBM是整数环境的最佳抽象[10，定理8.2.17]。Bagnara等人[1，§6]给出了计算DBM紧闭包的有效算法。它包括在加强之前使用紧固操作。拧紧操作定义如下：定义3.14[收紧]设B是元素在Z中的DBM。我们定义T（B）是具有Z中的元素的DBM，使得对于u，v∈V±：T（B）uv =Buv−1，如果u=v且Buv为奇数Buv否则γ70J. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）下面的定理给出了紧缩运算的基本性质定理3.15设B是弱闭DBM，其元素在Z中。我们假设其中，0 ≤T（B）uu+T（B）uu. 则T（B）是弱紧闭的。证据 参见，例如，[10，定理8.2.18]。Q这个定理有两个结果。 首先，正如Bagnara等人所解释的那样。[1，§6]，它给出了一个计算紧闭包的有效算法：一个是计算输入矩阵的闭包，然后收紧它并最终加强它。其次，我们的稀疏算法在整数环境中使用时只需要很小的调整：而不是保持DBM弱闭，我们只需要在每次操作后收紧它们，使它们弱紧闭然而，请注意，收紧并没有解决混合环境的情况据我们所知，没有已知的有效闭包算法支持这种用例，即使在密集设置中也是如此4结论在本文中，我们提出了新的算法的八角形抽象域，它保持了八边形表示的稀疏性。这些算法与通常的算法一样精确，并且依赖于差界矩阵上的一个较弱的不变量，称为弱闭性。我们已经表明，这些算法可以用于在合理的或真实的环境，以及在整数环境的上下文中。我们在Verasco静态分析器的上下文中实现并正式验证了Coq中的这些算法[9，10，18]。这些新算法的使用提高了八角抽象域的性能至少一个数量级这些算法仍然有可能改进：特别是，我们认为在每个抽象运算之后尽可能地稀疏差界矩阵，同时仍然保持它们弱闭，这可能是有益的。实际上，抽象操作可以推断实际上可以从非关系边界推导出的差异边界矩阵中的边界，因此错过了稀疏性的机会。我们认为Bagnara等人提出的约简算法[1]可以适用于仅使用弱闭差界矩阵来计算约简差界矩阵。这将导致基于语义定义的更简单的加宽算法，如Bagnara等人所述[1，§4.2]。我们相信，这些新算法的实现在国家的最先进的静态分析仪，通过使用，例如，由辛格等人开发的框架[17]这是一个很大的进步。引用[1] 巴尼亚拉河P. M. Hill和E. Za Zananella，Weakly-Relational Shapes for Numeral Abstractions：Improved Algorithms and Proofs of Correctness，Formal Methods in System Design35（2009），pp.279-323J. - H. Escherdan/Electronic Notes in Theoretical Computer Science 331（2017）71[2]Bouaziz，M.，TreeKs：一个使数值抽象域可扩展的函子，在：NSAD，ENTCS287中（2012），pp. 41比52[3] Chawdhary，A.，E. Robbins和A. King，Simple and Efficient Algorithms for Octagons，in：APLAS，LNCS8858（2014），pp. 296-313[4] Chen，L.，中国地质大学，J. Liu，A.米内湾Kapur和J. Wang，用绝对值，在：SAS，LNCS8723（2014），pp.101-117[5] 克拉里索河和j.Cortadella，八面体抽象域，在：SAS，LNCS3148（2004），pp.312- 327[6] Cousot，P. and R. Cousot，Static determination of dynamic properties of programs，in：Proceedingsof the Second International Symposium on Programming（1976），pp.106-130[7] Cousot，P.，R. Cousot，J. Feret，L. Mauborgne，A. Miné和X.竞争对手，为什么astrée扩大规模？系统设计中的形式化方法35（2009），pp.229-264。[8] Cousot，P. and N. Halbwachs，自动发现程序变量之间的线性约束，在：POPL（1978），pp. 84比96[9] J.，V. Laporte，S.布雷齐，X。Leroy和D. Pichardie，一个正式验证的C静态分析器，在：POPL，ACM，2015，pp. 247-259[10] 1999年，H、 论文，巴黎狄德罗大学[11] 拉维龙河谷和F.Logozzo，Subpolyhedra：一种（更）可扩展的方法来推断线性不等式，在：VMCAI，LNCS5403（2009），pp.229-244。[12] 洛戈佐湾和M. Fähndrich，Pentagons：a weakly relational abstract domain for the efficient validationof array accesses，in：SAC，ACM，2008，pp. 184比188[13] Miné，A.， 毕业论文，巴黎综合理工学院（2004年）。[14] Miné，A.，八边形抽象域，HOSC19（2006），pp. 31比100[15] Putot，S.和E. Goubault，Static analysis of numerical algorithms，in：SAS，LNCS4134（2006），pp.18-34.[16] Simon，A.和A.King，The Two Variable per Inequality Abstract Domain，HOSC23（2010），pp.87比143[17] 辛格，G.，M. Püschel和M. Vechev，Making numerical program analysis fast，in：PLDI，ACM，2015，pp. 303-313[18] Verasco正式验证了C静态分析器，http://compcert.inria.fr/verasco/。