程序分析中的多面体模型与包装整数

可在www.sciencedirect.com在线获取理论计算机科学电子笔记288（2012）3-13www.elsevier.com/locate/entcs带包装整数的全有界多面体分析StefanBygde，BjornLisper1Müalardalen大学创新、设计与技术学院Vêsterédas，瑞典Niklas Holsti2Tidorum Ltd芬兰赫尔辛基摘要使用抽象解释的凸多面体分析是一种常见且强大的程序分析技术，用于发现程序中变量之间的线性关系。然而，执行多面体分析的经典方法并没有模拟这样一个事实，即值通常存储为固定大小的二进制字符串，并且在过流的情况下通常具有环绕语义。 在使用16位甚至8位处理器的嵌入式系统中，甚至可以有意地使用包装行为。因此，为了准确和正确地分析这种系统，必须对包装进行建模。我们提出了一种多面体分析的方法，该方法导出在所有维度上有界的多面体，从而提供包含有限个整数点的多面体。我们的方法使用了以前建议的包装技术多面体，但结合它在一个新的方式与有限的扩大，一个适当的位置扩大点和限制无界变量。我们展示了我们的方法如何有潜力显着提高精度相比，以前建议的包装方法。关键词：抽象解释，抽象域，数值域，凸多面体，加宽，过流1介绍程序分析的一个普遍和常用的应用是导出程序变量在程序中的每一点可以取的这通常使用抽象解释[3]和一些数值抽象域来获得可能值的近似值。已经开发了许多关系和非关系领域[3，5，6，11，4]，所有这些领域都有一个共同的假设，1电子邮件：{stefan.bygde，bjorn. lieu}@ mdh.se2电子邮件：niklas. tidorum.fi1571-0661 © 2012 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.10.0034S. Bygde等人/理论计算机科学电子笔记288（2012）3变量可以取任意整数值。然而，在实际程序中，值通常存储为固定大小的二进制字符串。细微错误的一个常见来源是过度溢出，这意味着计算结果太大，无法存储在给定大小的二进制字符串中。 一个过流可能会导致运行时错误，饱和 在整数类型的最大或最小可表示值处的结果，或一个环绕。在通用处理器中，回绕是处理超流的最常见方法。虽然回绕可能是某些错误的原因，但有意使用回绕并不罕见，特别是在字长较短的处理器上。不幸的是，在上述假设下的变量，大多数抽象的数值域得出不健全的结果，如果包装周围存在于一个程序。为了使分析结果听起来w.r.t.回绕有必要对所选域进行修改Sen和Srikant [13]提出了一种整数和同余整环的约化积的变形，它处理了过幂的特殊此外，他们还使用了一个关系分析的一个科隆等式。Gustafsson等人。[7]修改了区间域，使变量在其范围内有界，并通过使用更强大的区间值表示来处理环绕。 关系域更具挑战性。Muller-Olm和Seidl [12]提出了一种分析方法，可以推导出程序变量之间的所有a-lynne等式，这在环绕的情况下是安全的。Brauer和King [1]提出了一种方法来推导关系域的传递函数，并对八边形域这样做，同时通过使用SAT求解器来考虑环绕效应。最后，Simon和King [14]提出了一种使用多面体分析的方法（最初在[4]中提出），即使在存在环绕时也是合理的我们的工作建立在西蒙和国王的方法，使用经典的多面体分析。我们在本文中表明，直接使用Simon和King我们提出了一个多面体分析，推导出完全有界的多面体，是健全的包装周围的存在下，在程序中。我们的方法是基于包装多面体（使用[14]中的方法），有限加宽[9]，加宽的适当位置以及对变量施加边界的组合基于类型信息。 我们的方法的好处如下：• 与使用[14]中概述的方法和标准的抽象解释相比，精确度提高• 有界多面体对于依赖于多面体内部整数点的数量的分析特别有用（例如，[10]，[2]），因为有界多面体保证这个数是有限的。第2节包含了我们的方法，解释经典的多面体分析和包装的多面体。我们在第3节中展示了我们方法的一个激励性例子，以及它与其他方法的不同之处。在第4节中，我们详细介绍了有界多面体分析的方法。第5节讨论了我们的扩展方法，这是该方法的核心最后，我们在第6节结束。S. Bygde等人/理论计算机科学电子笔记288（2012）35⎧⎨{≥ ≤ −}2预赛2.1多面体域经典的凸多面体抽象域[4]用包含S中所有整数点的最小凸多面体α（S）抽象一个整数点的有限集合S<$Rn。凸多面体的有效实现需要对偶表示。一种表示是一组线性约束C;多面体P（C）则由R中所有满足C中约束的点组成。另一种表示是框架F，其是顶点V ={v0，.，vv−1}<$Rn，射线R ={r0，...，rr−1}<$Rn.框架的多面体P（F）表示其中Rn是顶点的凸组合加上线性组合的光线（允许无界多面体）。注意，我们用P来区分多面体和它的表示。在本文中，我们将建模整数值变量，因此我们将感兴趣的整数点内的多面体。因此，如果P是一个多面体，那么γ（P）<$Zn（即具体化函数）将表示P内的整数点。2.2有限变元为了正确地对可能环绕的变量进行建模，我们需要更具体地了解如何对变量进行建模。令X ={x0，.，x n-1}是程序变量的集合。 Ea chvariablexj与大小w j相关联，大小wj定义了可以使用多少位来存储变量（我们允许变量具有不同的大小）和类型，有符号（int）或无符号（uint）。我们将变量x的值域定义为返回一组约束的xj0，xj2wj1 ifxj isuintrange（xj）= n{xj≥ −2wj−1，xj≤ 2wj−1− 1}ifxjisint然后，我们定义一组变量V<$X的范围约束集RV为：RV= range（x）x∈V如果V是所有程序变量X的集合，我们简单地写R为RX。范围约束的集合形成多面体P（R）。2.3环绕式Simon和King [14]开发了一种方法，使多面体分析对具有环绕行为的有限大小整数是合理的。由于我们的方法是建立在这个方法的基础上的，这里介绍了基础知识将基本窗口B定义为范围约束多面体P（R）中的整数点的集合。设M：Z n→B定义为p0，p1，.，p n−1n →（p0 mod 2 w0，p1 mod 2 w1，.，p n-1 mod 2 wn-1），其中mod余数取为6S. Bygde等人/理论计算机科学电子笔记288（2012）3≤Fig. 1.左边的图片（a）显示了包装前的多面体。基本窗口由点划线正方形显示。多面体覆盖了基础窗口的一部分和三个相邻窗口的一部分。不同阴影三角形的网格显示了条件x0x1，作为x 0的8位无符号残差与x 1的8位有符号残差的有符号比较。多面体与此条件的三个组件相交，一个在基础窗口中，一个在右侧的下一个窗口中一个在基本窗口的下一个窗口中，一个在基本窗口的上一个窗口中。 右边（b），交叉点 的条件与展开的多面体被显示，转移到基础窗口，和他们的凸包，这是最终的包装多面体。有符号或无符号，取决于变量xj的类型。Simon和King这意味着对于任何多面体P，γSK（P）∈B。直观地说，γSK（P）可以看作是将Zn划分成一个矩形窗口网格，每个窗口的尺寸为2wj，取P与每个窗口的交点，并在每个坐标xj上将该交点移动到基窗口中所需的2wj的倍数。然后，γSK（P）是由P的这些移位的“残基片段”组成的马赛克注意，如果P不包含在B中，则γSK（P）中的点可能不形成凸多面体。常数的加法、减法和乘法可以像往常一样处理，因为这些运算与模剩余交换。然而，有限大小整数的算术不等式比较（<，≤，≥，>）不与模剩余交换。 因此，在应用约束时，有必要显式包裹多面体。 设c是一个约束，P是一个多面体，V∈X是一组变量。然后，非正式地，函数wrap（P，c，V）物理地执行前面提到的分割和移位，将c应用于每个片段并计算结果的凸包。然而，只有涉及V中变量的Zn的子空间被划分并被wrap（P，c，V）移位。在典型的使用中，V是线性约束c中涉及的变量的集合。这种包装如图1所示。实际上，只有当P有有限个残基片段时，换句话说，只有当约束中涉及的所有变量都在P中有界时，西蒙和金才计算应用于P的c的这种近似。否则，Simon和King丢弃P中关于这些变量的所有信息，并将条件c本身替换为这些变量的唯一约束S. Bygde等人/理论计算机科学电子笔记288（2012）37nnnn2图二. 给出了一个实例程序L.3动机和例证我们将程序建模为图2中所示的图，其中我们将图中的每条边q与凸多面体P（q）相关联。使用经典多面体分析[4]，图2中的程序L产生以下递归方程系统：Pn（0）=TPn（1）=Pn（0）[x→N]Pn（2）=Pn−1（2）<$（Pn（1）HPn−1（5））Pn（3）=Pn（2）H {x≤0}（1）Pn（4）=Pn（2）H {x≥1}Pn（5）=Pn（4）[x→x+1]假设L（图2中）在8位处理器上执行。设x和N是8位无符号整数变量。然后L终止，因为当255 + 1返回0时x绕回。因此，（1）将给出不合理的结果。这是因为经典的多面体域不对环绕进行建模。为了使结果合理，我们应用Simon和King对于边0、 1、 2和5的方程PSK等于Pn，但是对于边3和4，我们有：PSK（3）= wrap（Pn（2），{x≤0}，{x}）（2）PSK（4）= wrap（Pn（2），{x≥1}，{x}）（3）ITERn= 1n= 2PSK（0）nPSK（1）nPSK（2）nPSK（3）nPSK（4）nPSK（5）n不x=Nx=Nx= 0≤N≤ 2551≤x≤ 255≤N≤ 2552≤x≤ 256 0≤N≤ 255不X=N不x= 0≤N≤ 2551≤x≤ 255≤N≤ 2552≤x≤ 256 0≤N≤ 255表1使用包裹多面体迭代程序L迭代的结果如表1所示。多面体PSK（3）正确地暗示N必须在0到255的范围内。8S. Bygde等人/理论计算机科学电子笔记288（2012）3然而，在这个过程中，x和N之间的关系信息已经丢失。这是由于包装S. Bygde等人/理论计算机科学电子笔记288（2012）391nn4n2nnnn对于无界多面体PSK（2）=P（{x=N}），必须丢弃x和N之间的关系信息，才能进行合理安全的包装。虽然这是一个简单的例子，可以通过在程序开始时对x和N施加界限来避免，但无界多面体是常见的（由任何加宽，非线性分配或无界初始状态引起），显然使包裹算法失去了很多精度。这使我们设计了一个完全有界的多面体分析。我们的方法使用有限的加宽，以适当的方式放置加宽点，并使用类型信息绑定变量。为了说明这个想法，我们在这里概述了我们的方法是如何分析L的。我们的方法的方程如下：PBD（0）=P（R）PBD（1）=PBD（0）[x→N]PBD（2）=PBD（1）HPBD（5）PBD（3）= wrap（PBD（2），{x≤0}，{x}）n n n−1n nPBD（4）=PBD（4）<$R <${x≥1}wrap（PBD（2），{x≥1}，{x}）n n−1nPBD（5）=PBD（4）[x→x+1]其中R={ 0≤x≤ 255， 0≤N≤ 255}。PBD和PSK之间的差异可以在三个地方看到一是n n初始程序点PBD（0）根据变量的类型来限制变量。其次，加宽点已移至PBD（4），最后，加宽部分已被有限加宽部分取代（见第5.1节）。所有这些多面体都是完全有界的，所以我们可以只用顶点集来表示它们的框架这种表示法对我们的方法更方便。表2中显示的迭代使用了这种表示法。在这里，我们让第一个维度对应于x，第二个维度对应于N。注意，表示为顶点集合的R是{（0， 0），（0， 255），（255， 0），（255， 255）}。在这个例子中，我们的方法在稳定之前需要更多的迭代，但是这个结果，虽然仍然听起来w.r.t.环绕，比以前的方法更精确。特别地，注意在PBD（3）中，我们有x保持为零，但N可以是0到255之间的任何数字（可靠性），并且我们保持了PBD（2），PBD（4）和PBD（5）中x和N之间的有价值的关系，作为多面体4 4 4呈三角形。 PSK（2）、PSK（4）或2 2PSK（5）.4有界多面体分析在经典分析中，一个多面体在三种情况下会变成无界的：第一，在初始程序点，那里对程序变量一无所知。第二，任何非线性赋值都会丢弃关于变量的任何信息，使多面体在该变量的方向上没有边界。第三，加宽通常产生无界多面体。有界多面体有几个好处。首先，包装算法丢失了变量之间的所有关系信息，这些变量是无界的。如果一个多面体是有界的，这个信息不一定会丢失。第二，分析计算10S. Bygde等人/理论计算机科学电子笔记288（2012）3nnnITER12PBD（0）（0， 0），（0， 255），（255，0），（255， 255）（0， 0），（0， 255），（255，0），（255， 255）PBD（1）（0， 0），（255， 255）（0， 0），（255， 255）PBD（2）（0， 0），（255， 255）（0， 0），（255， 255），（2，1），（256， 255）PBD（3）（0， 0）（0， 0），（0， 255）PBD（4）（1， 1），（255， 255）（1， 1），（255， 255），（255， 1）PBD（5）（2， 1），（256， 255）（2， 1），（256， 255），（256， 1）ITER34PBD（0）（0， 0），（0， 255），（255，0），（255， 255）（0， 0），（0， 255），（255，0），（255， 255）PBD（1）（0， 0），（255， 255）（0， 0），（255， 255）PBD（2）（0， 0），（255， 255），（256， 255），（256， 1）（0， 0），（255， 255），（256，255），（256， 0）PBD（3）（0， 0），（0， 255）（0， 0），（0， 255）PBD（4）（1， 0），（1， 1），（255，255），（255， 0）（1， 0），（1， 1），（255，255），（255， 0）PBD（5）（2， 0），（2， 1），（256，255），（256， 0）（2， 0），（2， 1），（256，255），（256， 0）表2使用完全有界多面体对L进行迭代抽象解释。迭代显示为顶点集而不是约束。[10][12][13][14][15][16][17][18][19][ 14.1使多面体有界我们考虑每一种可能的方式，使一个多面体无界，并认为它是如何可能的健全和精确地使它有界。本节详细介绍了如何用PBD替换方程PSK。n n4.2入口点经典的多面体域使用无界多面体作为起始点，表示变量值未知。也就是说，如果pinit是初始程序点，则使用包裹的经典多面体域的初始方程为PSK（pinit）=T。但是，由于每个变量都与一个类型相关联，因此可以绑定它们。也就是说，在程序开始时，约束R全部保持。因此，我们定义PBD（pinit）=P（R）请注意，PBD（pinit）是合理的，比PSK（pinit）更精确。n n4.3非线性滤波器在多面体分析中，非线性赋值丢弃了关于赋值变量及其与其他变量的关系的所有信息 作为一个例子，让px：=？是紧接在非线性分配之后的边。则P_SK（p_x：=？）=πx（Pn（prev（px：=？其中πx是在x上的投影操作，在x方向上向框架添加一条线。函数prev（p）返回进入p离开的节点的边在赋值的情况下，它保证只有一个，所以我们在这种情况下稍微滥用了符号来引用prev函数返回的单个元素在非线性赋S. Bygde等人/理论计算机科学电子笔记288（2012）311值之后，由于与x有关的关系信息已经被丢弃，我们可以声明range（x）为真。因此，在本发明中，12S. Bygde等人/理论计算机科学电子笔记288（2012）3.nn我们定义：PBD（px：=？）= πx（P BD（prev（px：=？H P（range（x））同样，PBD（px：=？）是健全的，更精确的比PSK（px：=？）.n n4.4扩大对于一个包含循环的程序，需要加宽以确保终止。在经典的抽象解释中，加宽部分通常紧接着循环合并点之后插入。设p循环是紧接在循环合并节点之后的程序点（例如，程序L的边2）。然后，经典的多面体分析定义：Pn（ploop）=Pn−1（ploop）<$q∈prev（ploop）Pn−1（q）这通常会导致一个无界的多面体，因为加宽通常会删除约束。在这种情况下，应用任何范围约束对于回绕来说都是不合理的，因此我们必须采用另一种方法。5使加宽有界如前所述，标准的加宽操作通常会使多面体无界。然而，在有限加宽的帮助下，可能会使结果与某些有限约束相交我们的想法是以这样一种方式使用加宽，即总是可以将结果与完全有界的多面体相交5.1有限加宽在[9]中建议了有限的加宽。有限加宽的想法是有一组约束C，并定义有限加宽C如下：P<$CQ =（P <$Q）H {c ∈ C|P ± P（{c}）<$Q ± P（{c}）}也就是说，加宽的结果是C中的所有约束在P和Q中都成立。 可以表明，这是对任何约束集合C的加宽操作。集合C通常针对每个程序策略性地选择。我们的想法是使用一个程序的范围约束R作为有限加宽的集合C。我们的目标是能够与所有范围约束相交，使多面体完全有界。 为了避免不必要地包装变量加宽点不应放在环路合并点处5.2加宽点的位置在经典的多面体分析中，通常将加宽点放在环合并节点之后。但是，如果不进行包裹，通常会导致一个无界多面体（见表1）。我们的目标是将结果S. Bygde等人/理论计算机科学电子笔记288（2012）313n0nnnn0nnnn−1n并减少不必要的包装。为此，我们将扩展点放在无论如何都必须进行包装的条件句处我们这样做的方式，使我们仍然有正好一个扩大每个周期在图中。这意味着我们将取代PSK（ploop）= P SK（ploop）Pn−1（q）与n n−1PBD（ploop）= .q∈prev（ploop）PBD（q）n−1q∈prev（ploop）这是可能的，因为我们将在周期的其他地方放一个扩大点。设σ是涉及变量Xσ的线性不等式约束，设pσ是在循环3内紧接着条件的边。当使用Simon和KingPSK（p σ）= wrap（PSK（prev（pσ）），{σ}，X σ）其中X σ是σ中涉及的变量。我们将其替换为：PBD（pσ）=PBD（pσ）<$R <${σ}wrap（PBD（prev（pσ）），{σ}，X）（4）在每一个循环中都有一个条件。注意，我们使用X，所有程序变量的集合，而不是Xσ（然而，这可以改进，参见下面的讨论）。将扩展放在条件语句中可以避免不必要的包装，但不会影响方法的可靠性。我们将加宽与包装结合起来，并且我们使用程序变量R和条件本身σ的范围约束的有限加宽。既然有限的加宽就是加宽，既然我们在每个周期中都有加宽，这是一个合理而安全的做法，它仍然保证终止。此外，这总是导致一个完全有界的多面体，如下面的命题所示命题5.1设PBD（q）= P，对一个程序中的所有边q。设σ是线性约束，设C = R {σ}，并设PBD（p σ）由（4）定义。然后又道：PBD（pσ）± P（C）对于所有n> 0。此外，P BD（p σ）是一个完全有界的多面体，因为P（C）是。证据 首先，设Qn=PBD（pσ）且Rn= wrap（PBD（prev（pσ）），{σ}，X），因此我们有n−1nPBD（pσ）=Qn<$CRn我们将用n上的归纳法证明这个命题成立。设n= 1，则Q1= P BD（p σ）= P。包装操作符保证所有变量X都是14S. Bygde等人/理论计算机科学电子笔记288（2012）3[3]请注意，根据循环的形式，σ既可以是对应于假分支的条件，也可以是对应于真分支的条件;如果它是假分支，则简单地否定σ。S. Bygde等人/理论计算机科学电子笔记288（2012）315在各自的范围内。因此，对于所有的n > 0，有<$c∈ R：Rn±P（{c}）。我们也有Rn±P（{σ}），因为包装操作应用包装后的条件。现在我们有Q1CR1=CR1=R1H P（{c ∈ C|± P（{c}）=R1H P（{c ∈ C|± P（{c}）=R1H P（C）±P（C）其中最后一个方程来自于这样一个事实，即对于任何c，Rn±P（{c}）已经对任何c∈C成立。因此，该命题对于n= 1成立。现在假设Qn<$CRn±P（C）成立，则Q n+1<$CR n+1=（Q n+1<$R n+1）H {c ∈ C|Q n± P（{c}）<$R n± P（{c}）}归纳假设说，对于所有c ∈ C，Qn± P（{c}）和Rn± P（{c}），因此我们再次得到{c∈C|Q n± P（{c}）<$R n± P（{c}）}= C. 所以，（Q n+1<$R n+1）H {c∈C|Q n± P（{c}）<$R n± P（{c}）}=（Qn+1<$Rn+1）HP（C）±P（C）Q命题5.1证明了所有变量在加宽后都是有界的。这与前面的步骤一起确保多面体是有界的，每个多面体都有界的分析。最后，我们可以改进命题5.1中的集合X，只要观察到只有那些被加宽算子移除的约束中的变量才需要被包裹，因为它们是唯一被加宽算子包裹的变量。然而，我们使用X作为所有变量的集合来简化证明。6结论和今后的工作我们已经开发了一个分析，使用完全有界的凸多面体，这是健全的程序与环绕语义。这是通过在初始程序点和非线性赋值时对变量施加范围界限来实现的，在条件中包装多面体（如[14]），最后通过使用带有范围约束的有限加宽并将此加宽放置在条件中。我们认为，这种分析很可能比使用西蒙更精确以及金的标准抽象解释方法。这是因为他们的方法必须丢弃无界变量之间的任何关系信息，而我们的方法从不让任何变量无界。请注意，我们并没有指定在循环中的哪个条件句中应该放置加宽点。我们计划开发用于放置加宽点的方法，尽管我们预计最佳放置取决于程序。我们的方法正在实施，16S. Bygde等人/理论计算机科学电子笔记288（2012）3SWEET工具[8]执行控制流分析，以限制嵌入式实时程序的最坏情况我们计划评估程序的方法，并没有环绕。确认这项工作得到了欧盟FP7项目APARTS的支持，批准号为251413。引用[1] Brauer，J.和A. King，无量化消除的传递函数合成，在：G. Barthe，editor，ESOP，Lecture Notes inComputer Science6602（2011），pp.97比115[2] Bygde，S.，基于抽象解释和元素计数的静态WCET分析，Licentiate论文（2010）。URLhttp://www.mrtc.mdh.se/index.php?选择=出版物&ID=2144[3] 库 索 山 口 和 R.Cousot ， Abstract interpretation ： A unified lattice model for static analysis ofprograms by construction or approximation of fixpoints，POPL，1977，pp.238-252。[4] Cousot，P. and N.Halbwachs，自动发现程序变量之间的线性约束，在：POPL，1978年，pp. 84比96[5] Granger，P.，算术同余式的静态分析，见：国际计算机数学杂志，第30卷，1989年，第30页。165-190。[6] Granger，P.，程序变量之间线性同余等式的静态分析，在：关于代数和编程中的树的学术讨论会上的软件开发理论和实践的国际联合会议论文集（CAAP169-192.URLhttp://portal.acm.org/citation.cfm? 111310.111320[7] Gustafsson，J.，A. Ermedahl和B. Lisper，Towards a Challenge Analysis for Embedded System CPrograms ， in ： The 10th IEEE International Workshop on Object-Oriented Real-time DependencySystems（WORDS 05），2005。URLhttp://www.mrtc.mdh.se/index.php? choice=publications& id=0972[8] Gustafsson，J.， A. 埃尔梅达尔角 Sandberg和B. Lisper，循环边界的自动推导，使用抽象执行的WCET分析的不可行路径，在：Proc.27thIEEE Real-Time Systems Symposium（RTSS[9] Halbwachs，N.，同步程序中的延迟分析。Courcoubetis，编辑，CAV，Lecture Notes in ComputerScience697（1993），pp.333-346[10] Lisper ， B. ， 全 自 动 、 参 数 化 的 最 坏 情 况 执 行 时 间 分 析 ， 见 ： J. Gustafsson ， 编 辑 ， Proc. ThirdInternational Workshop on Worst-Case Execution Time（WCET）Analysis，2003，pp. 77比80URLhttp://www.mrtc.mdh.se/index.php? choice=publications& id=0629[11] 我的儿子， Octagonabst ract domain，HigherOrderSymbol. Comput. 19（2006），pp. 31比100[12]Müller-Olm，M. 和H. 王文，李文，李文，等. 程序. 浪 系统29（2007年）。URLhttp://doi.acm.org/10.1145/1275497.1275504[13] 森河和Y. N. Srikant，使用循环线性进展的抽象解释的可执行分析，在：第五届IEEE/ACM国际会议正式方法和模型的程序，MEMOCODE39比48网址http://dx.doi.org/10.1109/MEMCOD.2007.371251[14] Simon，A.和A. King，Taming the wrapping of integer arithmetic，in：Static Analysis，LectureNotes in Computer Science4634，Springer Berlin/Heidelberg，2007 pp.121-136