抽象域的字典和数组内容分析及静态推理技术

吴晓晖可在www.sciencedirect.com在线获取理论计算机科学电子笔记287（2012）53-64www.elsevier.com/locate/entcs字典和数组Jandrzej Fulara1，2华沙大学信息学院摘要我们提出了一个通用的抽象域的字典和数组内容的分析。我们的技术是参数化的标量，字典键和字典值的抽象。 它可以用各种现有的域来实例化，包括非数值域（例如用于分析字符串变量属性的域）。它足够强大，可以表达容器内容和标量之间的关系分析是全自动的。 容器根据键的属性进行分区，通过底层的密钥抽象。 分析的精度和成本是可定制的，并取决于键、字典元素和标量变量的抽象的选择我们展示的例子中，该技术是用来推理数组以及字符串键字典。该方法也进行了实验评估。保留字：摘要释义，摘要领域，词典内容分析像字典和数组这样的集合是非常重要的程序构建块，因此静态分析技术应该能够推断出这些容器的内容。我们的目标是通过抽象解释为静态分析中的任意字典和数组建模提供一个通用的解决方案[2]。该技术应该是全自动的，并且应该能够调整其精度/成本比。不仅可以用数值抽象域[9，13，15]来实例化该技术，还可以用其他类型的域来实例化该技术，例如用于字符串分析的域[8]。抽象解释我们使用抽象解释的经典定义[2]。 一个抽象域是一个元组A=A，a，a，αa，γa，δa，oa 表示该被抽象状态集，满足，连接，抽象，具体化，传递函数和扩展。我们还需要一个投影·↓v（称为变量消去），一个对偶算子·↑v（变量引入）和一个遗忘算子·v。1这项工作得到了波兰科学和高等教育部的部分支持，拨款N206 4931382 电子邮件地址：fulara@mimuw.edu.pl1571-0661 © 2012 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.09.00654J. Fulara/Electronic Notes in Theoretical Computer Science 287（2012）53∈∈×⟨ H H ⟩ ⟨ H HH H⊥⊥H∈∈ ∈∈记法我们分析的程序，操作一组标量变量变量Var（与值在一些集V）和字典Varc。字典键和元素分别属于集合K和E。一个具体的程序状态是一对（ρ，τ）∈（Var→V）×（Varc→（K-E））.我们考虑的唯一字典语句是更新T[v1]<$v2和T[v1]<$c，读v2<$T[v1]和布尔谓词φ（T[v1]，v2），其中T ∈Varc，v1，v2∈Var和c∈E。大纲第1节介绍了一个表示单个字典的结构。在第2节中，我们展示了如何使用它来构建一个抽象域。第3节给出了域的示例。第4节描述了一个实验。第5节概述了相关工作。我们在第6节结束。证明和额外的例子可以在这项工作的扩展版本中找到[8]。1字典的表示我们将字典TVarc建模为一组抽象段。 每一个抽象段代表一组（具体的）键和相应的字典元素。设K和V是两个抽象域（具有载波K，K，K 和五，V，v ）.一个抽象段是一个对（k，v）KV，其中k模拟一组混凝土keys（连同它们与标量的关系）并且被称为抽象键，而v抽象字典元素（以及它们与标量的关系）并且被称为抽象值。 字典抽象是乘积的一个（受限）幂集K ×V[3]。让我们引入一些辅助术语。在格<$A，Ha，Ha，Ta<$，a∈A中，空，如果a=<$a;a∈A与b∈A重叠，当aHab <$a。我们现在定义一个格D、d，D ，其中Dfinn（KV）和每个d D满足以下附加良构性条件：(i) 对于（k1，v1）∈d 且（k2，v2）∈d 或者（k1，v1）=（k2，v2）或者k1Hkk2=k，(ii) 对于（k，v）∈d，k <$k，v <$v.第一个条件是，每两个抽象段表示不相交的具体元素集合。第二个条件禁止抽象段具有空的抽象键或抽象值。抽象段（k，v）表示字典的一个空片段，而（k，v）表示一组不能初始化为任何值的元素。这样的抽象片段在我们的表示中是对于每个（具体）字典d：K-E，由抽象字典d表示对于每个键n Dom（d），存在抽象段（k，v）d，使得n和d（n）分别由k和v认识并加入我们dbofa，bD由获得的抽象片段组成 作为来自a和b的一些重叠段的逐点相交：{（kaHkkb，vaHvvb）|（ka，va）∈a，（kb，vb）∈b，kaHkkb=/<$k，vaHvvb<$v}.J. Fulara/Electronic Notes in Theoretical Computer Science 287（2012）5355∪H∈引理1.1交算子定义良好，即aHdb∈ D。加入Adb of a，bD应该表示由a或b抽象的所有具体字典，因此可以尝试将其定义为并集a b。然而，以这种方式定义的join可能违反第一个良构性条件。我们现在展示如何避免这个问题，即将任意一组抽象键转换成一组，其中没有两个键重叠。这个想法是识别重叠键的组，并用其最小上限替换每个组设A是完备格，Ha是A的有限子集，S是A的有限子集.定义1.2我们说一个非空集合的有限族X ={X1，X2，...，Xk}，其中每个Xi∈ S，是S的不相交划分，i ∈：• X是S的分区（即，S=X且Xi<$Xj=<$（对于i /=j），• 对任意yXi，Xj∈X，其中i=fj，有（.aXi）Ha（.aXj）=a.S的不相交划分总是存在的-如果S=X，则X= X，否则可以取X{S}。 如果S有多个不相交的分区，那么我们对S的分区X感兴趣，它不执行任何不必要的分组：定义1.3我们说S的一个不相交划分C是最小的，如果对于S的任何不相交划分X，它保持<$C∈C<$X∈XC <$X。直观地说，最小不相交划分将S的这些必须在S的每个不相交划分中分组在一起的元素分组（放入相同的Xi中）。引理1.4 S的最小不相交划分存在且唯一定义。我们使用最小不相交划分的概念将任意c∈ P_fin（K×V）变换为抽象字典d∈D。令S表示“非空”抽象段（k，v）∈ c的抽象键S. K|（k，v）∈c，k/= k，v<$v<$.设C表示S的最小不相交划分。我们定义一个不相交的规范化函数dNorm：Pfinn（K×V）→D为：d N或m（c）。（。kkj，.vvj）|{k1， . ，km}∈C，（kj，vj）∈c， j∈{1， . ，m}m。JJ这个标准化可以在O（|C|3）时间，包括计算最小不相交划分C的现在连接aHdb可以定义为正规化的联合ab，即aHdbdNorm（ab）。定理1.5集合D在H d下形成格 Hd。加宽加宽保留第一个参数中与第二个参数中的每个段不相交的所有段，用它们在K和V中的加宽替换重叠段，并用（Tk，w）替换第二个参数中与第一个参数中的所有段不相交的每个段（l，w）[8]。56J. Fulara/Electronic Notes in Theoretical Computer Science 287（2012）53∈∈--∪HH∈∈→∈∈ZH H联系我们a1，d1，i1oc a2，d2，i2.2域我们现在利用上面定义的格来定义一个抽象域。每个字典的内容将使用上面定义的D，d，d过度近似。在抽象段（k，v）中，k和v分别是具体元素的键及其可能值的过近似集。如果一个键根本没有被抽象，那么对应的元素就不能被初始化。抽象密钥在集合Varvk上的抽象域K内建模，其中vk是用于表示密钥值的人工密钥变量类似地，使用集合Varvv上的抽象域V来表示抽象值，其中vv是表示字典元素的值的值跟踪变量在这种方法中，可以表达标量和键以及标量和字典元素之间的关系格D（K，V）可以用来过度近似字典的内容，但它没有给出关于哪些元素必须初始化的任何信息。我们通过将每个字典也与用于过度近似未初始化的字典元素的D（K，Bool）的元素相关联来解决这个问题一个segment（k，True）意味着由k抽象的键上的元素可以是未初始化的。 如果某个键没有被任何段抽象，那么这个键处的元素必须被初始化。由于False是布尔值网格的底部，因此段（l，False）将自动删除。状态的标量部分被抽象在变量Var集合上的某个抽象域A中。我们还需要域A和K之间的转换函数κA→K和κK→A，以及A和V之间的转换函数κA→V和κV→A。现在我们可以定义域C=αC，Hc，Hc，γc，αc，δc，oc. 抽象状态集C由CA×（Var c→D（K，V））×（Var c→D（K，Bool））给出。 一个抽象状态记为（a，d，i）∈C。域操作meetc和joinc是逐点定义的。 加宽的oc是以一种懒惰的方式定义的，因为当标量的抽象状态a ∈A稳定时，字典修改应该变得稳定：（）（a1oaa2，d1Hdd2，i1Hdi2）ifa1oaa2/ =a1（a1oaa2，d1od2，i1odi2）否则。具体化标量的具体化是使用标量域A中的具体化γ a来定义的。 让我们考虑一个标量变量的具体赋值ρ：VarV，一个字典T Var c。和一个具体的关键nK.如果存在抽象段（k，True）i（T）使得n被k抽象，则T[n]可以是未初始化的。如果存在一个抽象段（l，w）d（T）使得n被l抽象，那么T[n]可以有一些被w抽象的值。 如果既不存在（k，True）i（T）也不存在（l，w）d（T）使得n被k或l抽象，则T [n]既不能初始化也不能非初始化，因此对于标量的赋值ρ，不存在字典的赋值τ：Var c→（K-E）。根据这些观察，我们定义了一个谓词I（ρ，T，n，i），对于ρ：Var→V，J. Fulara/Electronic Notes in Theoretical Computer Science 287（2012）5357..Σ.- 是的 Σ∈∈← ∈∈∈←DJλT.dNorm{（δk（I，k），δv（I，v））|（k，v）∈d（T）}IJλT.dNorm{（δk（I，k），True）|（k，True）∈i（T）}δc I，（a，d，i）δa（I，a），dJ，iJ图1.一、标量指令I的传递函数TVarc，nK和抽象状态i的初始化部分，当且仅当T[n]可以是未初始化的：I（ρ，T，n，i）真惠<$（k，True）∈i（T）<$σ∈γk（k）σ|Var=ρ，σ（vk）=n.（1）类似地，我们定义一个谓词V（ρ，T，n，m，d），其中ρ：Var→V，T∈Varc，n ∈K，当T[n]可以等于m时，m ∈E成立：V（ρ，T，n，m，d）真惠<$（k，v）∈d（T）<$σk∈ γk（k）<$σv∈ γv（v）σk|Var = σv|Var = ρ，σk（vk）= n，σv（vv）=m. (2)这允许我们将具体化γc（（a，d，i））定义为：，（ρ，τ）|ρ∈γa（a），<$T∈Va rc<$n∈K. n/∈D_m（τ（T））与I（ρ，T，n，i）. n∈Do m（τ（T））和V（ρ，T，n，τ（T）（n），d）n，.2.1传递函数我们提供了标量和字典语句的传递函数 我们举例说明定义，其中所有A，K和V都被选为Z值的区间域。为了清楚起见，在每个抽象段中，我们只显示关键和值跟踪变量vk和vv的值。标量语句抽象键和抽象值为标量变量的关系建模，因此标量语句不仅在标量域A中解释，而且在所有容器的所有抽象段中解释，如图1所示。当标量变量被修改时，它与抽象键和抽象字典元素的所有关系都被更新。字典语句T ←new dict创建一个空字典：δc。T←newdic t，（a，d，i）. a，d[T→k]，i∈T→{（Tk，Tru e）}∈ k.我们现在继续使用字典读取v2T[v1]，其中TVarc和v1，v2Var（参见图2）。直观地，我们从d（T）中检索所有抽象段（可能不止一个），其键与访问T[v1]的键重叠形式上，我们通过将人工密钥变量vk添加到a，分配vkv1并将结果转换到域K58J. Fulara/Electronic Notes in Theoretical Computer Science 287（2012）53来计算kK，即kκAK（δa（vkv1，av ））.我们取键与k重叠的所有抽象段（l，w）d（T）中的所有值的连接，即vv{w|（l，w）∈ d（T），lHkk/=k}，将v转换回定义域A，赋值v2← vv并消除特殊值跟踪变量vv。最后，我们使J. Fulara/Electronic Notes in Theoretical Computer Science 287（2012）5359..- 是的Σ.Σ.Σ¬Sk¬∈←∈∀⇒∈联系我们.ΣK κA→Kδa（v k←v1，a↑vk）vv w|（l，w）∈ d（T），k Hkl/=kaJδa（v2<$vv，κV→A（v）Ha↑vv）（，dJ，iJ）（a，d，i）<$v2δcv2← T [v1]，（a，d，i）（aJ↓vv，dJ，iJ）图二. v2←T[v1]的转移规则kκA→K.δa（vk<$v1，a↑vk）<$。vκA→V.δa（vv←v2，a↑vv）xdNorm d（T）<${（k，v）}δcT[v1]←v2，（a，d，i）（a，d[T<$→x]，i）图三. 弱更新T[v1]←v2（k）所有抽象段中v2的旧值每当访问的键可能未初始化时，即{1|（l，True）∈ i（T），kHkl/=k} /=.例2.1假设v1∈Var，a（v1）=[1，4]，T ∈Varc被建模为：d（T）={（[0， 2]，[-2，1]），（[3， 5]，[4， 4]），（[6， 9]，[2， 7]）}且i（T）={（[8，∞]，True）}。的读v2← T [v1]得到a（v2）=[−2，4]。我们定义弱和强字典更新。只有当标量的每一个赋值最多有一个更新的键的可能值时，才我们通过定义域K上的以下一元谓词S来形式化它：S（k）=真惠<$σ1，σ2∈γk（k）（σ1|Var = σ2|Var = σ1（vk）= σ2（vk））。这个定义不太实用，因此我们要求域K配备一个域特定谓词Sk，它蕴涵S，即kKSk（k） S（k）。 如果Sk（k）=True，那么我们说k是单例。让我们考虑更新T[v1]v2. 我们计算抽象密钥kK 就像在阅读中一样类似地，我们得到抽象值vV。如果k不是单元素（即Sk（k）），则弱更新被执行为de-在图3中找到。我们将新的抽象段（k，v）添加到d（T）并计算dNorm（d（T）（k，v））。初始化信息不会改变。如果k是单例，则可以执行强更新。容器d（T）可能已经包含描述更新的元素的抽象段（l，w），即k Hklk。 新值应该只分配给修改后的元素，所有与由L抽象的键相关联的其它元素应保持不变。我们需要将l拆分成更小的键的集合k，m1，m2，. 它们一起表示与L相同的具体键。我们说一个函数f：K×K→ P（K）是一个抽象键l ∈K关于一个单元素k ∈K的分解，如果：• <$m1，m2∈<$（l，k）<${k}m1• k/∈N（l，k），m2m1Hkm2=k，• γk（k）<$ m∈<$（l，k）γk（m）=γk（l）.定义k（l，k）必须与定义域K一起给出。我们定义一个运算：D（K，V）×（K×V）-D（K，V），使得d（k，v）60J. Fulara/Electronic Notes in Theoretical Computer Science 287（2012）53.- 是的Σ.- 是的Sk.Σ（vt，vf）πv.φ（vv，v2）， vxtd（T）±（k，vt） xfd（T）±（k，vf）D （k，v）. d。（l，w）|（l，w）∈d，l Hkk/= lk<$k<$k. （k，v）Sk（kKκA→Kδa（vk<$v1，a↑vk）vκA→Vδa（vv<$v2，a↑vv）xd（T）±（k，v）yi（T）±（k，假）δcT [v1] ←v2，（a，d，i）a，d [T <$→x]，i [T <$→y]见图4。 强更新T[v1]←v2kκA→K.δa（vk<$v1，a↑v<$k）<$v.v.W|（l，w）∈d（T），kHkl/=kHk（k）δcφ（T[v1]，v2），（a，d，i）（a，d[T<$→xt]，i），（a，d[T<$→xf]，i）图五. 布尔谓词φ（T[v1]，v2）在d中覆盖由k抽象的键处的元素：- 是的（m，w）|（l，w）∈d，l Hkk操作d （k，v）的定义仅当k是单例。k，m ∈ k（l，k）<$。设k和v与弱更新中的一样，设k是单例。强更新在d（T）中覆盖与抽象键k相关联的旧值，并在i（T）中标记由k抽象的键处的元素必须被初始化（参见图4）。强更新只会忘记更新元素的旧值（根据分解的定义），并将其替换为一个过度近似插入的具体值的抽象值。例2.2[弱更新]考虑与例2.1中相同的容器T ∈Varc和标量v1∈Var，外加一个标量v2∈Var使得a（v2）=[8， 8]。更新T[v1]← v2给出d（T）={（[0， 5]，[-2，8]），（[6， 9]，[2， 7]）}。例2.3[强更新]考虑标量v1，v2∈Var，使得a（v1）=[2， 2]且a（v2）=[7， 7]，容器T ∈Varc，其中d（T）={（[0， 5]，[1， 3]）}，i（T）={（[0，∞]，True）}。强更新T[v1]← v2修改T，使得d（T）={（[0， 1]，[1， 3]），（[2， 2]，[7， 7]），（[3， 5]，[1， 3]）}。它还标记更新的元素必须初始化，设置i（T）={（[0， 1]，True），（[3，∞]，True）}。布尔谓词布尔谓词（出现在条件语句中）可以对标量变量和字典访问进行操作，例如φ（T[v1]，v2）。我们限制T[v1]的可能值，如图5所示。令k表示访问T[v1]的抽象键，v是对应的抽象值。如果k是单例，则我们根据φ（vv，v2）限制v例2.4考虑v1，v2∈Var使得a（v1）=[4， 4]且a（v2）=[0， 0]且T ∈Varc使得d（T）={（[0， 4]，[-2，5]）}。一个测试T[v1]≤v2评估为两个绝对状态（cTrue，cFalse），其中d（T）由{（[0， 3]，[−2， 5]），（[4， 4]，[−2，0]）}给出[001 pdf 1st-31 files]和{（[0， 3]，[-2，5]），（[4， 4]，[1， 5]）}。J. Fulara/Electronic Notes in Theoretical Computer Science 287（2012）5361≤ ∈∈≤ ∈∈联系我们联系我们→ P × {≤}←∈≤≤←联系我们联系我们∅≤←←←← ←←←←←3示例我们提出的例子中，域是用来推理数组和字符串键字典。3.1数组分析让我们讨论图6（a）中的部分数组初始化。我们的分析发现，在这个代码片段之后，T的第一个j个元素被初始化。在这个例子中，我们使用一个非常简单的关系域的上界B [8]，其中抽象状态集B是一个映射Var（Var<、）. 直观地说，对于每个变量x，我们保持变量集大于x（带有一个额外的指示器，以确定不等式是否严格）。我们 通过 固定A=B（ Var） ，K=B（ Var ） 来 实例 化 域Cvk） 和V=B（Varvv）。下面我们不写所有的界限显式。相反，对于每个抽象键k，我们只显示键变量vk的约束。如果（x，D）k（vk），我们写“Dx“。 如果（vk，D）k（y），则我们写为如果（���，）k（vk），（vk，）k（ ），则我们使用快捷方式“=“ 。 对于每个抽象值v，我们只显示了具有值跟踪变量v v的约束。我们还假设在Var中有一个特殊的变量v0等于0。[0语句T ←new array（n）创建一个新数组，其索引范围为，n）。 注意，在这个程序点j = 0和T.length = n，因此未初始化的数组元素的索引l的范围可以写为v0= jlj}，真）}。1：在“b”处2：重复3：setattr（obj，at，6）1：x0，j0，Tnew array（n）2：whilex ndo3：x x+14：如果φ（x），则5：T[j]x，j j+16：结束，如果7：结束while（a）4：at+5：untilrandom（）=False6：ifrandom（）=Truethen7：obj.x 88：其他9：obj.x10：如果结束11：打印对象b -112：打印对象bcc -113：打印对象x -1（b）第（1）款图第六章部分数组初始化（6（a））和动态添加属性（6（b））62J. Fulara/Electronic Notes in Theoretical Computer Science 287（2012）53→ P {}在语句j←j+1之后，d（T）和i（T）等于{（{ j}，True，.最后，在j←j+1之后，我们得到d（T）和i（T）等于：{（{

下载后可阅读完整内容，剩余1页未读，立即下载