改进的不变式生成：验证优化代码正确性的新方法

理论计算机科学电子札记176（2007）21-35www.elsevier.com/locate/entcs改进的不变式生成T一方一号微软公司Redmond WA，美国丽诺尔·D Zuck扎克2，3美国伊利诺伊大学芝加哥分校计算机科学系摘要NYUT项目应用翻译验证的方法来验证优化的代码在语义上等同于未优化的代码，通过为优化编译器的每次运行建立，一组验证条件（VC），其有效性意味着优化运行的正确性。 核心是T-SP，它处理结构保持优化，即，不改变内部循环结构的优化。底层的证明规则，Val，其可靠性T-SP的基础上，要求，除其他事项外，在每个“切割点”的控制图的源和目标代码的生成不变量。TVOC-Pemploy的计算实现类似于通过简单的固定运算来获得不变量。在本文中，我们提出了另一种方法来计算不变量，这是基于简单的数据流分析技术。关键词：翻译验证，不变量生成，数据抽象，数据流分析.1介绍在工业界和学术界，人们越来越意识到正式证明系统安全关键部分的正确性的关键作用。大多数验证方法侧重于验证与需求相关的规范，以及与规范相关的高级代码。然而，如果要证明高级规范在低级代码中正确实现，则需要验证执行翻译的编译器验证正确性1电子邮件：yfang@microsoft.com2 电子邮件地址：lenore@cs.uic.edu3本研究部分得到了NSF基金CCR-0205571和SRC基金2004-TJ-1256的支持。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.06.01622Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）21由于目标体系结构的复杂性和可重新配置性，以及编译器中使用的复杂分析和优化算法，因此现代优化编译器的设计具有挑战性。正式验证一个全边缘优化编译器，因为人们会验证任何其他大型程序，是不可行的，由于其规模，随着时间的推移，并可能，专有的考虑。在[ 9 ]中引入的翻译验证方法提供了一种替代一般翻译器和特定编译器的验证方法：而不是验证编译器本身，而是构建一个验证工具，在编译器每次运行后，正式确认生成的目标代码是源程序的正确翻译。在过去的五年里，我们一直致力于开发一种优化编译器的全自动翻译验证方法（参见，例如，[14、15、3]）。该方法包括正确翻译的理论，以及一个工具套件，T，它为英特尔的ORC编译器执行翻译验证。该理论区分结构保持优化和结构修改优化，结构保持优化允许目标程序中的控制和数据值到源程序中的相应控制和数据值的清晰映射，结构修改优化不允许这种清晰映射。大多数高级优化都是结构预处理，服务.测试包括两个主要部分：处理结构t_SP保留变换，以及处理循环重新排序变换的T循环，其被简化为由T循环-SP处理的等价性检查。给定源代码（优化前）和目标代码（优化后），T-SP构造验证条件（VC），其有效性意味着两者之间的语义T-SP的理论基础是弗洛里亚诺风格的证明规则Val。证明规则Val不同于类似的证明规则，除了通常的数据和控制之外，映射，即在选定的控制点上构建基本块之间携带信息的不变量。生成的不变量的强度决定了工具的能力。在本文中，我们研究的不变量生成，Val呼吁，并提出了一种方法，以获得更强的不变量比在目前的实现，tation的TVOC-SP。 Currently（se e [3]），TVOC-Ppermrarna-v e f e ra- p e r a-peint计算以获得数据映射和不变量。我们的想法的要点是将输入到T的文本Whirl（[12]）转换为静态Single赋值（SSA）形式，并执行简单的数据分析，以获得数据映射和应用Val所需的不变量。我们还提供了一个更适合我们需求的Val版本。这里描述的技术得到了实施（见[7]），并且在几乎所有的情况下都产生了优于T细胞的结果。例本文的组织如下：在第2节中，我们提出了新版本的规则Val，并讨论它是如何从它的前辈不同。第三节是本文的核心部分，描述了一种新的不变量生成方法。在第4节中，我们描述了新的不变量生成所需要的数据映射的新计算。我们在第5节结束。Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）2123相关工作[9]中的工作开发了一个翻译验证工具，CVT，它可以在大约10分钟内自动验证大约10，000行源代码的翻译CVT的成功关键取决于一些简化的假设，这些假设将源和目标限制为具有单个外部循环的程序，并假设非常有限的优化集其他方法[8，11]考虑了比[9]中考虑的限制更少的语言的翻译验证，例如允许嵌套循环。他们还考虑了一套更广泛的优化措施。然而，那里提出的方法仅限于结构保持优化，并且不能直接处理涉及代码运动或循环重新排序变换的更积极的优化。本文所依据的正确翻译验证理论出现在，例如，[14]，[15]和[3]介绍了T工具套件。2总框架编译器接收用某种高级语言编写的源程序，将其翻译成中间表示（IR），然后对程序应用一系列优化-从经典的与体系结构无关的全局优化开始，然后是与体系结构相关的优化，中间代码是一个三地址代码。它由一个三地址代码的图形表示法-- 图来描述图中的每个节点表示一个基本块，即完整执行且不包含分支的语句序列图的边缘代表控制流程。为了表示源代码和中间代码的形式语义，我们引入了转换系统，TS，它转换系统S=πV，O，Θ，ρπ是一个状态机，由以下部分组成：• V是一组状态变量，• 一组可观测变量，• Θ是表征系统的初始状态的初始条件，以及• ρ是一种过渡关系，将一个状态与其可能的后继者联系起来。变量是类型化的，T的状态是变量的类型一致的解释。 对于状态s和变量x∈V，我们用s[x]表示s赋予x的值。转换关系指的是变量的未启动版本和启动版本，其中启动版本指的是而变量的未启动版本指的是它们在过渡前状态中的值因此，例如，转换关系可以包括24Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）21不S可观察变量是我们关心的变量，我们将每个I/O设备视为变量，每个I/O操作将元素删除/追加到相应的变量。如果需要的话，我们还可以在可观测量中包括一组选定过程的外部过程调用当比较两个系统时，我们将要求两个系统中的可观测变量匹配。TS的计算是状态σ的最大有限或无限序列：s0，s1，.，从满足初始条件的状态开始，使得每两个连续的状态通过转移关系相关联。 也就是说， s0|= Θ，且s i，s i+1| = ρ，对于每个i，0 ≤i +1 <|σ|四、如果初始条件的可观测部分唯一地决定了计算的其余部分，则过渡系统S被称为确定的也就是说，如果S有两个计算s0，s1，. 以及t0，t1，. 使得s0的可观测部分（可观测变量的值）与t0的可观测部分一致，则两个计算是相同的。我们限制我们的注意力确定性的过渡系统和程序，产生这样的系统。因此，为了简化演示，我们在这里不考虑其行为可能取决于程序在整个计算过程中读取的附加输入的程序。这是直接的理论和方法扩展到这样的中间输入驱动的程序。设P=<$V，O V，O，θ，ρ′和P=V，O，Θ，ρ′是两个T′T T T T T我们分别称之为源T和目标T这两个系统称为可比较的，如果存在一个一对一的对应之间的可观察量的PS和PT。 为了简化符号，我们用X∈ OS和x∈ OT表示这两个系统中相应的观测量。 源状态s被定义为与目标状态t相容，如果s和t在它们的可观测部分上一致。也就是说，对于每个x∈ OT，s[X] =t[x]。我们说PT是P S的一个正确的翻译（精化），如果它们是可比较的，并且对于每个σT：t0，t1，. PT和每个σS的计算 ：s0，s1，. P S的计算 使得s0与t0相容，σT为在终止的情况下，它们的最终状态是相容的。我们的目标是提供一种自动化的方法，该方法将确定（或反驳）给定的目标代码正确地实现了给定的源代码，其中两者都表示为T假设PS和PT是用某种中间语言给出的源程序和目标程序此外，我们假设PS和PT都是SSA形式的（[6]），这允许更强大的数据映射，不变量生成比那些允许非SSA形式的程序（[5，4]5）。将代码翻译成T因此，我们假设两个程序都是TS因此，我们用同一个名字来称呼IR程序和它们的T对于每个程序，我们计算一个割点集，即，一组控制点，包括入口点、出口点和至少一个控件每个循环的点源割点集用CP表示，目标割点表示为CP。 简单路径是控制切割点之间的路径，4|σ的长度是σ中的状态数。|, the length of σ, is the number of states in σ. 当σ无限大时，它的长度是ω。5Seeal s oipf-orc.sourceforge.net/ORC-documentation.htm.Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）2125(i)建立控制抽象κ：CPT→CPS，将目标的初始点和终点映射到源的初始点和终点(ii)对于CPT中的每个目标切割点i，形成可以仅引用目标变量的目标不变量cut（i(iii)对于CPS中的每个源割点i，形成可以仅引用源变量的源不变量S（i(iv)为CPT中的每个目标临界点i建立数据抽象α（i）：（v1=E1）···n（vn=En）对某些非控制源状态变量vk∈VS赋予一个表达式Ek目标状态变量。注意，允许α（i）是部分的，即，它可以不包含用于某些变量子句。要求对于每个可观测变量（其目标对应物是v）和每个端点t，α（t）具有子句V=E（V），其中E（V）是目标可观测变量上的表达式。(v)对于每个割点i和j，使得在PT的控制图中存在从i到j的简单路径，形成验证条件.不！Cij：<$T（i）<$$>S（κ（i））<$α（i）<$ρij→VS：ρκ（i），κ（j）JSJJJ（vi）确定所有生成的验证条件的有效性。Fig. 1. 证明规则Val中间切割点。图1中给出的证明规则Val描述了如何确定PT是PS的正确翻译。该规则要求计算从目标切割点到源切割点的控制映射，以及将（一些）源变量映射到目标变量上的表达式的数据映射。此外，在PS和PT的每个控制点处计算不变量。不变量允许在基本块之间携带信息，并为Val提供额外的边缘，这是其他验证技术所缺少的。这里提出的证明规则是一些规则的变体。前任（参见，例如，[15]）。在图1中，大写字母用于表示PS中的变量，小写字母用于表示PT中的变量。对于每个割点i和割点j，ρij描述了i和j之间的广义转移关系，即，类型τ（V，VJ）的断言，其中V是转换之前的变量，VJ是转换之后的变量例如，考虑图的左手侧的示例二、在那里，对于从位置1到位置2的广义转移，我们有：ρ12：（PC=1）<$（PCJ=2）<$（（B1=1<$NJ = 500）（B1= 1<$NJ = 0））压（V-{N1，N2，PC}）。 前两个1 2S合取是指程序计数器的值，即1在前，2在后，过渡期第二个合取词描述了两条路径可能发生的结果第三个合取指定转换保留所有源变量的值，但对于PC，N1和N2。26Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）21不变量（i）是它们的作用是在切割点之间传递信息。在步骤（5）中证明了它们的不变性。这个版本的Val和以前版本的Val之间的主要区别是：(i) 在以前的Val版本中，只提到了目标不变量。然而，在工具T中，源和目标不变量都被使用。从理论的角度来看，添加源不变量没有任何好处，因为目标在-变量与数据映射α一起可以捕获源不变量。然而，从实际的角度来看，直接计算源不变量更简单，这在这里是明确的。(ii) 该规则的先前版本中的数据抽象α包括引用目标变量的保护。在这里，我们选择一个更简单的形式，不包括警卫，但建立一个单独的数据映射为每个目标切割点（以适应代码运动），每个可能只涉及一个子集的源变量。这里的形式更弱，因为它（隐式地）只允许目标控制变量作为守卫，而不是目标变量上的任何谓词。然而，T的实现仅计算目标控制变量作为保护的数据抽象，因此我们在这里选择与工具对应的版本。(iii) 在[ 14 ]中讨论了验证条件C ij右侧的存在性量化。正如在[ 15 ]中指出的，这种存在性合取可以通过在蕴涵的左手边包括合取来消除Sρππ∈{来自κ（i）的简单路}S其中ρπ是对应于路径π的转移关系，因此替换有一个有限的（和小的）连接的存在的quantier。2.1应用Val：一个例子为了应用Val，翻译验证工具应该计算割点集、控制映射、简单路径、广义转换关系（对于简单路径）、不变量和数据抽象。有了以上内容，该工具就可以构造VC（在Val的步骤（5）中）并将它们发送给定理证明器。 我们保留了割点集的计算，控制抽象，简单路径，就像在当前的T-SP中一样（见[14，3]）。在那里，我们用包含在割点集中的基本块的第一个位置来标识每个割点。为了适应SSA形式，我们用包含在割点集中的基本块的φ-赋值（SSA形式）之后的第一个位置来标识每个割点第3节中我们描述了不变量的新计算，在第4节中，我们描述了数据抽象映射的新计算（它使用计算的不变量）。在本节中，我们将通过一个简单的例子来演示T-SP如何计算Val的其他成分，以及为什么它无法计算出好的不变量。Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）2127S考虑图2中描述稀疏条件常数传播的示例。第0章：B1←1;W1←1;Y1←0;一曰：if（1）N1←500;其他第九章：第十章：w1←1;t1←0;w3←φ（w1，w2）;第二章：N2←0;N3←φ（N1，N2）;十一：t3←φ（t1，t2）w2←w3+t3+3;第三章：W3←φ（W1，W2）;Y3←φ（Y1，Y2）;十二：t2←t3+2;如果（w2≤500），则转到10;第四章：如果（W3>N3）转到7;十三日：y1←t2/2;5：W2←W3+ 2<$Y3+3;Y2←Y3+1;6：goto 3;7：返回Y3;第八章：十四日：return1;(b) 目标(a) 源图二. 源和目标通过上述修改以适应SSA，T-SP计算：• CP不 目标切割点集由位置组成：9，这是第一个位置在初始块中，14是终端位置，11是循环体的基本块中的第一个非φ位置第11和12段）。类似地，CP（目标切割点集）由位置{0， 5， 8}组成。• 控制映射κ为{9<$→0，11<$→5，14 <$→8};28Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）21• 源代码中的简单路径是：{0→ 5， 5→ 5， 5→ 8， 0→ 8}目标中的简单路径是：{9→ 11， 11→ 11， 11→ 14}• PS中源路[5 → 5]的跃迁关系 是：（PC= 5）<$（PCJ= 5）<$（WJ=W3+Y2·2+ 3）<$（YJ=YJ+1）2 2 3<$（WJ=WJ）<$（YJ=YJ）<$（WJ≤N3）3 2 3 2 3VS−{PC，W2，W3，Y2，Y3}）Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）2129其中pres（V）是（vJ=v）的缩写v∈VT-SP通过取决于到达定义的固定点计算来计算不变量。对于这个代码，T-SP不能建立有效的验证条件，因为它不能在位置5生成不变量N3= 500。下一节中介绍的不变量计算可以平凡地检测这个不变量。3生成不变量不变量的生成是Val应用中最具挑战性的任务。 在这一节中，我们描述了一个新的不变式生成方法，在SSA形式的IR程序上操作。由于目前在T语言中实现的基于数据流的方法是纯语法的，而新方法也是语义的，我们相信它比基于数据流的方法更有效，并产生更多的信息。直观地说，Val中不变量的作用是在基本块之间携带信息。对于SSA形式的程序，这样的任务可以通过收集到达某些程序点的定义以及分支条件其可以稍后被馈送到具有某些算术能力的定理证明器中以揭示考虑图2（a）中的SSA程序。由于L1处if语句的分支条件总是求值为真，因此N3在L3处求值为常数值500。我们不是试图直接检测（N3= 500）作为L3的不变量，而是从L3回溯收集N3定义所依赖的数据流信息根据分支条件（B1= 1），N3被分配给N1的值或N2的值，因此我们得到（N3=N1（B1= 1））（1）作为L3的不变量。此外，由于L0支配L3，并且程序是SSA形式的，所以L0的定义在L3也成立。因此，我们得到（B1= 1）（W1= 1）（Y1= 0）（2）在L3处不变。Eq的连接。1和等式2表示所需值（N3= 500）。3.1SSA形式假设一个SSA形式的程序的控制流图（CFG）G，其循环都是具有单个入口位置的自然(IfG的某些我们将循环的入口节点表示为循环头。我们假设每个循环头都有一个从循环外部进入的边。(If这是不是这样的情况下，我们引入preheaders30Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）21我我循环的头部，使得先前从循环外部引导到头部中的所有边都引导到前头部中，并且存在从前头部到头部中的单个新边。因此，我们假设G是一个CFG，每个节点是一个基本块。 由于GG的节点和前向边定义了一个有向无环图（DAG），它在节点之间导出了一个偏序按照标准符号，给定两个节点x，y∈G，我们说x支配 y，如果从G的入口到y的每条路都经过x。我们说x是y的直接支配子，如果y的每个支配子要么是x，要么被x严格支配。节点y的直接支配者用idom（y）表示。对于一个节点y∈G，我们用Gidom（y）表示从G中去掉所有通向idom（y）的边，然后去掉所有没有到达y的节点和边而得到的图。对于一个节点x∈G，设assign（x）是x中的非φ-赋值集. 如果x不是循环头，我们定义：gen（x）=（v = exp）。（v：=exp）∈assign（x）表达式gen（x）描述了由x生成的不变量，而不管它的环境如何。对于具有直接后继者y的节点x，我们用cond（x，y）表示控制从x转移到y的条件。设x∈G是一个不是循环头的节点。 假设x有mxprede-cessors xJ，. ，xJ . 设V x表示由x中的φ -函数定义的变量集。1mx假设对于每个v∈Vx，φ函数在x中定义v为vtx（v）←φ（vtx（v），.，v tx（v））。0 1mx设x∈G现在是一个节点，它是一个循环头。显然，如果x是通过后边缘到达的，除了在φ函数之后表示的诱导变量的定义之外，还必须考虑关于它们的信息。在循环体中更新。 如果v x，.，vx是基本的感应变量，I K循环，其头部为x，其中每个归纳变量vx在进入循环之前初始化为bi，并在每次迭代时递增ci，我们定义：Kindu c（x）=v<$x≥0.（vx=bi+ci×v<$x）（3）i=1当我们的视频是一个新的视频。 I. e. ，v_x是一个零次迭代，并且induc（x）c在某个（可能是第0次）迭代中得到了归纳变量的值。循环.我们将回到处理问题（即，消除）3.2节中的存在变量。在图3中，我们描述了计算（x）中的断言的数据流方程，Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）2131我我out（x）对每个节点x∈G.前者是在所有φ-函数之后，在x的开始处的不变量，而后者是在x的结束处的不变量。对于任意x∈G，通过向前遍历由G的前边缘诱导的DAG，可以同时计算出不变量in（x）和out（x）.⎧n（x，G）n⎪⎪in（x，G）=cond（idom（x），x）⎪⎪⎨ out（idom（x），G）⎪⎛ ⎞Gidom（x）{\displaystyleGidom（x）}{\displaystyle Gidom（x）}mxi=1⎪∧我（vx我的=vx）v∈Vx⎩⎧t0（v）ti（v）否则out（x，G）=如果x∈G，则在（x，G）中⎩不然就真的。图三. 输入（x，G）和输出（x，G）的数据流方程定理3.1图3.1所计算的数据流方程. 3是健全的，即，在程序执行期间，对于cfgG中由节点x表示的每个基本块B，当程序到达B时（在φ函数之后），in（x，G）成立，并且每当程序退出B时，out（x，G）成立。证明大纲：证明是通过归纳的广度第 一搜索的G.基本情况用于入口节点。然后，我们得到了out的数据流方程，这是很平常的. 对于归纳步骤，我们区分循环头和非循环头。假设x是一个循环头。因为我们假设所有的循环都是自然的，所以控件要么从它的直接支配者要么从后边缘到达循环头。由于我们假设SSA形式，我们有在直接支配符的末尾的所有不变量，以及导致循环的条件，都成立。如果这是循环的第一个入口，那么induct（x）在平凡vx= 0的情况下成立。如果一个后边缘到达循环头，则induct（x）对于平凡的vx>0成立根据归纳假设，out（idom（x），G）是可靠的。因此，我们可以得出结论，in（x，G）是合理的。如果x不是一个循环头，那么x是通过它的一个前任xJ到达的，cond（xJ，x）保持不变。因此，in（x，G）的可靠性直接来自归纳假设。最后，无论x是否是循环头，gen（x）在块x执行后都有效。因此，out（x，G）是in（x，G）与gen（x）的合取。因为我们假设in（x，G）是可靠的，所以out（x，G）的可靠性随之而来。因此，从定理3.1可以得出，对于CFG的每个初始位置i，对应于G，我们可以取f（i）：in（x，G）作为在i处的不变量。⎪⎪32Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）21不不不注意，in（x，G）和out（x，G）是G诱导的DAG结构上的相互递归函数.因此，不需要定点计算来求解方程。事实上，x的祖先在G中的每个节点和边都是可访问的在计算in（x，G）和out（x，G）时只需要一次，因此计算的复杂度与G的大小成线性关系。3.2量化消除由于Val生成的VC在蕴涵的两边都有不变量，并且由于大多数定理证明者不接受存在公式作为结果，我们需要在不变量中消除这种量化。我们通过设置令人反感的存在主义量化器来实现这一点。在这个讨论中，我们只考虑目标不变量的情况。 源不变量的情况类似。Sup ppos e aVCCijt thhide hh 根据新版本生成算法，得出X是循环报头。让 假设在C ij的左手边有不变式T（i）。我们区分以下情况：j是循环的头，i在循环之外。因此，i和j之间的简单路径是对应于循环的第一个条目的路径。 在这种情况下，我们可以将索引值设置为0，并将索引值重新设置为具有h的J（j）的整数部分K（v i= b i）。i=1j是循环头，i在循环中。因此，i和j之间的简单路径表示为G的一个块。我们可以从先行项中“重新使用”v x的值，K（vi=bi+ci×（v<$x+1））i=1以前的案子都没有。因此，i和j之间的简单路径并不排除该inducible值的值，并且我们可以从先行项中“重新使用”v_x的值，因此K（vi=bi+ci×v<$x）i=13.3示例：不变量生成为了将上述方法应用于我们的运行示例中的目标程序，我们定义基本块B1={L9}，B2={L1 0，L1 1 1，L1 2}，B3={L1 3}，对于这些基本块，我们Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）2133有：gen（B1）：（t1= 0）（w1= 1）gen（B2）：（w2=w3+t3+ 3）n（t2=t3+2）cond（B1，B2）：truecond（B2，B3）：<$（w2≤500）该程序有一个循环{B2}，其中有一个归纳变量t3，它在循环之前被初始化为t1，并在每次迭代时递增2因此，我们有：感应器t（B2）=ΔvΔT。（t3=t1+2v<$T）求解图1的方程。3、我们得到：在（B1）中：trueout（B1）：（t1= 0）（w1= 1）在（B2）中 ：（t1=0）（w1=1）vT：（t3=t1+2vT）out（B2）：（t1=0）（w1=1）vT：（t3=t1+2vT）n（w2=w3+t3+ 3）n（t2=t3+2）在（B3）中 ：（t1=0）（w1=1）vT：（t3=t1+2vT）（w2≤500）因此我们可以得出结论：宾馆（9） ：trueT（11）：（t1=0）类似地，对于我们正在运行的示例中的源程序，我们可以计算：S（0）：trueS（5）：（N3= 500）∧∃vˆS:(Y3=Y1+vˆS)∧(W3≤N3)Sinc e vis 是这样一个循环的概念，而vist是它在目标中的概念，我们可以在v i s i s ind e（viS=viT）中定义一个函数，它允许我们将源和目标中的循环归纳变量联系起来。结合RNS（5）和RINT（11），我们得到t3= 2·Y3在目标截断点L11（及其对应的源截断点L5）处成立，这意味着在终止时可观测变量Y3和y134Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）214计算数据抽象数据抽象α为每个目标切割点映射等式的合取。每个等式都是U=EU的形式，其中U是源变量，EU是目标变量的表达式。在α（i）中包含合取式U=EU的含义是，当目标的控制在位置i中，并且因此源的控制在κ（i）中时，k（i）中的U的值是在目标处计算的EU的值。不变量越精确，α就越精确。在本节中，我们将描述如何在计算上述α的情况下计算α这里描述的算法假设给定了U=EU类型的一些初始等式集。在实践中，如果可以访问编译器的符号表（在ORC的情况下可以访问），或者通过“合理”的猜测，例如，通过假设源和目标中具有相同名称的变量相等，可以从编译器的符号表中获得这样的初始集。算法的正确性不依赖于初始集合的选择，特别是初始集合可能包含错误的等式。然而，它生成精确数据抽象的能力可能会受到初始集的影响。我们用Γ表示这个初始集合该算法如图4所示。对于每个割点i，该算法采用辅助γ（i），其是（来自U=EU的）等式的集合。在每一步中，γ（i）是假设在目标处于位置时保持的等式集合I. 最初，γ（i）是Γ本身。在每次迭代中，直到γ（i）稳定，违反不变量和转移关系的等式被删除。在每一步，α（i）是γ（i）中等式的合取等式U=EU被从γ（i）中移除，如果对于从j到i的某条简单路径，T SJ J<$T（j）<$<$S（κ（j））<$α（j）<$ρπ<$ρκ（j）κ（i）/→U=（EU）其中（EU）J是转换后EU的评估，即，其中每个变量都被替换为它的初始版本。请注意，当我们选择对应于目标路径π的目标转移函数时，我们将匹配源路径视为源的两个匹配π端点之间的任何路径。因此，如果有几个匹配的源路径，我们采取各自的转移关系的析取该过程可以看作是在格点（2Γ，λ）上进行的迭代正向数据流分析.可以通过从Γ开始并在每次迭代时在网格中递减值来求解γ的卷积函数，直到达到固定点。用定理证明器判定了γ与编译器优化中使用的迭代数据流分析不同，该过程对源程序和目标程序应用联合分析在我们运行的示例中，我们在数据抽象中获得，例如，α（9）：（W0=w0）<$（Y0=y0）α（11）：（W3=w3）α（14）：（W3=w2）（Y3=y1）Y. Fang，L.D.Zuck/Electronic Notes in Theoretical Computer Science 176（2007）2135V为每个目标切割点Iγ（i）：V=Γα（i）=重复E∈γ（i）{E}为每个目标切割点I对于每一条通向ij的简单路径π：=startpointofπγ（i）：=T SJ{E∈γ（i）：<$T（j）<$$>S（κ（j））<$α（j）<$ρ π<$ρκ（j）κ（i）→E}α（i）=E∈γ（i）E直到集稳定见图4。 数据抽象请注意，如果我们在算法开始时，Γ只包含形式为（U=u）的简单等式，那么在源不变量的帮助下，将捕获更复杂的数据映射例如，在一个示例中，表示α（i）：（X=x）<$（Y=y）<$（Z=x+y），可得到α（i）：（X=x）<$（Y=y）和<$S（κ（i））：（Z=X+Y）.5讨论与结论本文提出了一种基于SSA-from的计算不变量和数据映射的方法。该方法允许翻译验证的程序，超出了目前的权力的T恤。翻译到SSA形式和这里提出的新算法进行了实施和测试。B0： a1←1B0： a1←3b1←1B1： a3←φ（a1，a2）1←2B1： d3←φ（d1，d2）b3←φ（b1，b2）a3←φ（a1，a2）如果（a3mod2 = 0）转到B3B2： a4←a3+ 1f1←a3+d3g1←5b4←b3+ 1B2：a2←g1−d3d2←2如果（f1≤g1）到B1goto B4B3： a5←a3+ 3b5←b3+ 3B4： a2←φ（a4，a5）（一）b2←φ（b4，b5）如果（b2

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