高级源代码到目标代码的转换验证方法

2网址：http://www.elsevier.nl/locate/entcs/volume65.html页面VOC：一个优化翻译器的翻译验证器1;2Lenore Zuck3 Amir Pnueli4 Yi Fang3 Benjamin Goldberg3摘要在工业界和学术界，人们越来越意识到正式证明系统安全关键组件的正确性的关键作用。大多数形式化验证方法都是针对给定的规范来验证系统的高级表示的正确性。然而，如果希望从这样的验证中推断出在实际目标架构上运行的代码的正确性，则必须证明高级表示在较低级别上正确地实现。也就是说，必须验证从高级源代码表示到目标代码的转换的正确性，该转换通常由编译器（或者在源代码表示的情况下由代码生成器）执行。 是一种规范，而不是一种编程语言）。正式验证一个全边缘优化编译器，因为人们会验证任何其他大型程序，是不可行的，由于其规模，正在进行的演变和修改，并可能，专有的考虑。本文所采用的翻译验证方法是一种新的方法，它可以替代一般的翻译人员和编译人员的验证。根据翻译验证方法，而不是验证编译器本身，构造一个验证工具，在编译器的每次运行之后，正式确认在该运行中产生的目标代码是源程序的正确翻译本文提出了一种优化编译器的翻译验证方法我们区分结构保持优化和结构修改优化，对于结构保持优化，我们基于计算归纳在源代码和目标代码之间建立模拟关系，对于结构修改优化，我们开发专门的“元规则”。本文还描述了双氢-64|一个原型翻译验证器，自动产生验证条件的SGI Pro-64编译器的全局优化。1 本 研 究 部 分 得 到 了 NSF 资 助 CCR-0098299 、 ONR 资 助 N 00014 - 99-1-0131 和Minerva Center for Veri cation of Reactive Systems（英特尔的礼物）以及德国-以色列科 学 研 究 与 发 展 基 金 会 （ German- Israel Foundation for Scienti c Research andDevelopment）的资助。2 电子邮件：fzuck，amir，yifa ng，go ld be rg g @c s。n你。埃杜乌3 纽约大学计算机科学系4 魏茨曼科学c 2002年由Elsevier Science B出版。诉 在CC BY-NC-ND许可下开放访问。31介绍在工业界和学术界，人们越来越意识到正式证明系统安全关键部分的正确性的关键作用。大多数验证方法处理系统的高级规范。然而，如果要证明高级规范在较低级别上正确实现，则需要验证执行翻译的编译器。由于目标体系结构的复杂性和可重构性以及编译器中使用的复杂分析和优化算法，现代优化编译器的正确性是具有挑战性的。正式验证一个全边优化编译器，就像验证任何其他大型程序一样，是不可行的，这是由于它的大小、随时间的演变以及可能的专有考虑。翻译验证是一种新的方法，它可以替代一般的译者验证，特别是编译者的验证。根据翻译验证方法，而不是验证编译器本身，构造一个验证工具，在编译器每次运行后，正式确认产生的目标代码是源程序的正确翻译新的微处理器体系结构类别的引入，例如以Intel IA-64体系结构为例的EPIC类别，将更重的责任放在优化编译器上。这是由于预期静态编译时依赖性分析和指令调度可以利用并行级并行，以便与其他架构（例如超标量机器类）竞争，其中依赖性被确定，并且指令在运行时由硬件重新排序。 因此，开发了一系列新的复杂优化，并将其纳入编译器中，例如针对EPIC架构先前的工作（[PSS98a]）开发了一种用于翻译验证的工具，cvt，它能够在大约10分钟内自动验证涉及大约10，000行源代码的翻译。这个工具的成功关键取决于一些简化的假设，这些假设将源和目标限制在具有单个外部循环的程序中，并假设了非常有限的优化集。其他方法[Nec00，RM00]考虑了限制较少的语言的翻译验证，例如允许嵌套循环。他们还考虑了一系列更广泛的优化。然而，那里提出的方法仅限于结构保持优化，不能直接处理更积极的优化，如循环分布和循环平铺，这是更先进的优化编译器中使用的。我们的最终目标是开发一种方法，用于高级优化编译器的翻译验证，重点是EPIC目标编译器，以及此类编译器的积极优化特性。4我们的方法将处理大量的优化，为广泛的编译器实现全自动认证，确保在诸如安全关键系统和编译成硅的领域中的编译器的极高水平的置信度，其中正确性是最重要的关注。在本文中，我们发展了正确翻译的理论，并描述了翻译标准64|我们的原型翻译验证器，自动产生验证条件的SGI Pro-64编译器的全局优化。正确翻译理论对目标程序是源程序的正确翻译这一概念提供了精确的定义，并提供了形式上建立这种关系的方法。我们区分结构保持优化，承认一个明确的映射目标程序中的控制点在源程序中的相应控制点。大多数高级优化都属于此类。对于这样的转换，我们采用众所周知的方法，模拟两个目标控制点之间的执行相应的源执行。一类更具挑战性的优化并不能保证这种对应性，对于这类优化，我们开发了专门的方法，称为元规则。属于这类的典型优化是循环分布和融合、循环平铺和循环交换。我们预计这项工作的副产品之一是制定一个面向验证的仪器，这将指导未来编译器的作者如何将适当的额外输出纳入优化模块，这将使验证简单明了。这将导致自证明编译器的构造理论。我们的翻译验证器PSS 98 a-64为SGI Pro-64编译器生成的代码生成验证条件（VC），这些代码稍后可以发送给cvt[PSS 98 a]进行验证。产生的验证条件严格遵循我们的理论：首先建立64个控制点，然后建立控制和数据抽象以及程序注释，并在此基础上建立VC。1.1相关工作这里的工作是[PSS98a]中工作的扩展，我们打算在这里研究的验证工具的实现中使用那里开发的工具。[Nec00]中的工作涵盖了我们工作的一些重要方面。首先，它将源程序从单循环程序扩展到具有任意嵌套循环结构的C程序。另一个重要的特征是，该方法根本不需要编译器插装，并且应用各种逻辑来恢复和识别所执行的优化以及相关联的元素映射。[Nec00]中明显的主要限制是，正如报告中描述的单一证明方法所暗示的那样，它只能应用于结构保持优化。相比之下，我们的工作也可以应用于结构修改优化，例如5与积极的循环优化相关的问题，积极的循环优化是现代体系结构优化的主要组成部分，尽管我们在本文中不讨论它。另一个相关的工作是[RM00]，它提出了一种类似的翻译验证方法，其中一个重要的贡献是能够处理源程序中的指针。然而，那里提出的方法假设编译器的完整插装，这在这里或[Nec00]中没有假设。[Nec97]和[NL98]中报道的相关性较弱，它们并不旨在建立翻译的完全正确性，而只是对某些“安全”属性感兴趣。然而，那里描述的程序分析技术与重新生成的自动生成非常相关元映射和辅助不变量。1.2优化翻译器翻译验证的一般策略编译器接收用某种高级语言编写的源程序，将其翻译成中间表示（IR），然后对程序应用一系列优化，从经典的与架构无关的全局优化开始，然后是与架构相关的优化，例如寄存器分配和指令调度。通常，这些优化在几个通道中执行（在某些编译器中多达15个），其中每个通道应用某种类型的优化。翻译验证为每个这样的优化遍次的正确性提供证明，其中成功的验证导致证明脚本确认，并且不成功的验证导致反例。建立目标和源代码之间正确对应关系的一般方法是基于RENMENT的，并通过仿真证明。根据这种方法，我们建立了一个元素映射，指示相关的源变量如何对应于目标变量或表达式。然后，证明被分解为一组验证条件（也称为证明义务），每个条件都声明目标执行的一段对应于源执行的一段。在某些情况下，证明义务本身是无效的，然后有必要引入辅助不变量，这些不变量在程序中的选定点上可证明成立。证明义务在辅助不变量的假设下是有效的。一般来说，我们的策略是首先使用转换系统（TS）的形式主义给源语言和目标语言目标代码T是源代码S的正确实现的概念是一种补充，说明T的每次计算都对应于S的某个计算，并具有相应变量的匹配值在图1中，我们以完成映射图的形式呈现了重新执行的过程6S：源语义上午（南）优化编译器T：目标映射语义映射验证Sem（T）Fig. 1. 第一千零六十八章圆满完成如果只进行少量优化，或者根本不进行优化（大多数编译器支持的调试模式），则目标代码对源程序的依赖性证明被简化为一组自动生成的验证条件（证明义务）的有效性证明，这些验证条件是一阶逻辑中的蕴涵。 对于这种简单的情况，所需要的是建立这些验证条件的有效性。在（现实的）假设下，只有限制优化应用于算术表达式，证明义务是一个限制形式的一阶逻辑，所谓的方程公式，使用未解释的函数来表示所有的算术运算。最近的工作（[PRSS99]）表明，建立一个工具来检查这些公式的有效性是可行的。这个工具是基于nding小域实例化的方程公式，然后使用基于BDD的表示来检查有效性。当优化开关打开时，使用可以自动生成的验证条件不再有效。验证工具将需要额外的信息，这些信息指定在当前翻译中应用了哪些优化转换。这些额外的信息可以由编译器提供，也可以由我们计划开发的一组语法和分析技术推断出来。我们的研究的一个主要组成部分是优化编译器提供程序注释的仪器。这些注释将由验证工具处理，以在选定的控制点处形成不变断言。验证条件将被这些不变量扩充2模型在这一节中，我们简要地描述了中间代码，我们假设它是优化编译器的输入和输出语言，以及我们的形式化模型的转换系统模型。2.1中间代码中间代码是一个三地址代码。它由一个ow图描述，这是一个三地址代码的图形表示中的每个节点ow图表示一个基本块，即总是完整执行且不包含分支的语句序列，而边7代表着控制的力量。示例1考虑图2中的C程序及其由SGI Pro-64翻译成中间代码的过程。程序在r中计算两个数组的元素乘积的总和，指针的初始地址分别是sender和weight。数组的最后一个元素是在end sender。void three（float *r，float*s，float *w，float* e）{寄存器浮点 * 接收器，*weight，*sender，*end_sender; receiver= r;sender=s;weight= w;end_sender=e;for（; sender<= end_sender;）* 接收器+=（*sender++）*（*weight++）}B 0接收方- r发送方-s权重-wend_sender-eB1 WHILE （发送者<=end_sender）B2块.t264-发送器发送器-.t264+4.t265-重量重量- .t265+4[接收器]- [接收器]+[.t264] *[.t265]端块B4返回图二.一个C程序及其中间代码图2中的程序流程图由初始块B0、端子块B4和内部块B1和B2组成，B0通向B1，B1通向B2和B4，B2通向B1。为了说明的简单性，我们假设变量和内存位置不相交。在我们工作的这个阶段，我们忽略了别名。变迁系统为了呈现源代码和中间代码的形式语义，我们引入了转换系统TS，它是[PSS98b]转换系统的一个变体。转换系统S =hV; O;; i是一个状态机，由以下部分组成：V是一组状态变量，O V一组可观察变量，初始条件，其表征所述系统的初始状态，以及一种过渡关系，将一个国家与其可能的继承者联系起来。变量是类型化的，并且TS的状态是变量的类型一致的解释。对于状态s和变量x 2 V，我们用s[x]表示s赋予x的值。 正如我们对基本块的讨论一样，转换关系指的是变量的未引发版本和引发版本，其中引发版本指的是变量在后继状态中的值，而变量的未引发版本指的是它们在转换前状态中的值。 我们，例如，转换关系may包括|y0 =y+1“表示8变量y在后继状态中的值比其在旧（转换前）状态中的值大1。可观察变量是我们关心的变量。当比较两个系统时，我们将要求两个系统中的可观测变量匹配。我们要求所有由程序打印其值的变量都被标识为可观察变量。如果需要的话，我们还可以在可观测量中包括一组选定过程的外部过程调用的历史。TS的计算是状态的最大nite或nite序列，：s 0; s 1;：;从满足初始条件的状态开始，即，s0 j= ，并且每两个连续状态通过过渡关系相关联，即hsi; si+1 i j=对于每个i，0i +1 j j5.示例2我们将图2中的中间代码翻译成TS。集合包括可观测量r、s、w、e和[r]，局部变量receiver、sender、weight、end sender，以及临时变量.t264和.t265。我们还在V中包含控制变量（程序计数器），它指向要执行的下一个状态。的取值范围为fB 0;B1;B2;B4 g。初始条件，由：= B0给出，表明程序从10开始（即，bl ock）B 0. 作为观察变量，我们认为O=fr;s;w;e g。转移关系可以表示为四个析取的析取=01_12_21_14，其中ij描述了从Bi到Bj的所有可能的移动，而不通过中间块。例如，在一个示例中，21是：（=1）^（：t2640 =sender r）^（sender r0 =：t26 40 +4）^（：t2650 =weight t）^（0个 =2）^（weight t0 =：t265+4）^（[接收器]0 =[接收器] +[：t264]0 [：t265]0）当描述一个过渡关系时，我们采用的惯例是只提及其值发生变化的变量，而其他变量则保持不变。程序的计算从B0开始，然后（由01）引导到B1，然后，它可以循环到B2（通过12）并返回到B1（通过21）几次，然后导致（通过14）到B4，在那里它终止。每个块达到的状态由分配给变量的值从中间代码到TS的转换很简单;因此我们假设这里处理的所有代码都是由TS描述的。TS的比较与修正让PS =hVS;OS;S;Si和PT =hVT;OT;T;Tib两个TS，它们分别被称为源TS和目标TS。如果P-S的可观测量之间存在一一对应，则这两个系统称为可比较的 和PT的那些。为了简化符号，我们用yX2OS表示 x2OT 两个系统中相应的观测值。我们认为PT 是5j j，长度 ，是中的状态数. 当是黑夜，它的长度是！.9不SPS的C或Recttranslation（保留） 如果它们具有可比性，T T T夜间（即， 终止）P - 计算：0;：;m，有一个夜晚公司简介PS-计算：0; ： ： ：;k，证明对于每个x 2 0 T，sm[x]=sk[X]。因此，我们的目标是提供一个自动化系统，(or反驳），给定的目标代码实现给定的源代码，其中两者都表示为TS。3VOC：结构保持变换考虑源TSPS =hVS;OS;S;Si和目标TSPT =hVT;OT;T;Ti具有可比性。 设CP是源节点的割点集，即， 一个集合，包括初始和终端块（节点）和至少一个节点，从每个chl oop，并类似地让C PT是在目标中设置的切割点。对于CPS中的每两个字符i和j（分别）CPT）such有一条简单的路径S T在源中的Bi和Bj之间（分别地，目标），让ij（resp.（ij）描述块Bi和块Bj之间的过渡关系。令pc表示CPS中的10个阳离子，并且表示10个阳离子CPT。为了证明PT 是PS的正确翻译 对于PT 不会改变PS的结构 在一个主要的方式，我们介绍，在图。3、规则Vali date的proo。 该规则是对计算归纳法（[Flo67]）的一种解释，该方法提供了一种证明方法来验证一个程序是否与另一个程序相关。这是通过建立从目标到源位置的控制映射，从源到目标变量的数据抽象映射，并证明它们在目标程序的每一步都被保留来实现的需要注意的是，为了保证Python可以处理较小的结构变化，例如，当目标中的赋值发生在源中的对应物之前时，循环不变代码运动。设计这样一个证明规则实际上是一个困难的问题{当前版本的证明规则继承了一系列合理的证明规则，但未能处理一些常见的优化。这个版本的Python已经成功地处理了许多例子，我们相信它可以处理所有不涉及主要结构修改的优化（如各种循环优化）。本文第（1）部分中的控制抽象是标准的Floyd控制映射。 第（2）部分中的变量注释是编译器通过对数据流的分析而期望提供的程序注释。直观地说，它们的作用是在基本块之间传递信息数据抽象部分（3）是标准类Flooret数据抽象的一个变体。 两差异是我们允许是局部的，并且包括警卫（PI S）。允许局部的动机是为了适应这种情况，例如在死代码消除中，源变量在目标中没有对应关系。允许包含保护的动机是为了适应例如在循环不变代码运动中发生的情况，其中在执行的某些点，源变量没有10S0(i) 建立控制抽象：CPT ！CP映射每个值将目标控制变量PC转换为源控制变量的相应值。控制抽象应该将目标的初始和终端块映射到源头为了定义，可能必须向CPS添加一些附加点。(ii) 对于每个基本块Bi，形成可以仅引用具体（目标）变量的不变量'i(iii) 建立数据抽象：（p1！v1=E1）^^（p n！vn=En）赋值给源状态变量vi2VS fg在目标状态变量上的表达式E i，以（目标）布尔表达式p i为条件。注意，对于同一个变量，可能包含多个子句。(iv) 对于每个基本块Bi和Bj，使得在PT的控制图中有一条从Bi到Bj的的t0Cij：'i ^^ij！9VSS0：㈠;（j）^^'j：(v) 确定所有生成的验证条件的有效性图3.第三章。证据规则在目标上的对应，而在其他点上它们是一致的。因此，保护描述了可以使用目标变量来定义源变量的条件。验证条件断言，在从Bi到Bj的每个（目标）转换处，如果断言“i”和数据抽象在转换之前保持，并且转换发生，则在转换之后存在反映源中的对应转换的新源变量，而数据抽象和断言“j”保持在新状态中。因此，'i被用作蕴涵C ij的前提。作为回报，验证器也必须在转换后确定'j保持不变。因此，我们不相信仪表编译器提供的注释，但作为验证的一部分，我们确信所提出的断言确实是归纳的，并且无论何时访问都有效由于断言只提到目标变量，它们的有效性应该完全取决于目标代码。在大多数情况下，可以很容易地从代码中实现原始源变量，6.我们假设变迁所描述的路径是简单的。11验证条件（iv）中的存在量化可以被消除，因为蕴涵q！9x0：（x0=E）^r与蕴涵式q^（x0 =E）！ R. 然而，情况可能并非总是如此，我们不得不离开（4）中的存在主义量化。在[PZP00]中，我们证明了一个定理，说明证明规则的一个变体是合理的。这个证明也适用于规则的这个版本，我们在这里省略它。在下一节中，我们将介绍SGIPro-64 {这是一个目前正在纽约大学开发的工具，用于为SGI Pro-64编译器编译的程序自动生成验证条件（VC）。通过voc-64生成的VC的验证可通过cvt执行，cvt是为Sacres项目开发的[PRSS 99]。cvt不能处理的部分可以由其他定理证明器处理。目前，我们一直在使用STeP[MAB +94]，并正在探索可以提供类似功能的其他软件包。在我们描述P2P-64及其功能之前，我们在这里给出一个由P2P生成的P2P应用程序的示 例。为了可读性，这里的输出是“人工辅助的”，但本质上是由工具产生在下一节中，我们将更详细地描述该工具。3.1一个应用实例这个例子是使用第4节中描述的<$-64导出的。 这里我们简单介绍一些示例输出。 考虑经过一系列优化后的图2的程序：复制传播，死代码消除，控制流图优化（循环反转）和寄存器变量识别。一个简化版本的代码，其中我们重命名了一些变量，是在图。四、 注释（'2，表示为phi2）由编译器提供（参见第4节）。B 0发送者- s重量-w如果！（s< = e）GOTO B4 B1.t266<-[r].t267-e+4B2{phi2：（.t267 =e+（weight= sender-（.t266= [r]）}&&.t271-发送器发送器-.t271+4.t270-重量见图4。注释优化程序为了验证程序，我们使用控制映射=f0 7！0; 27！二;六七！4G和数据抽象：：（SENDER=sender）^（RECEIVER=r）^（WEIGHT=weight）^（S=s）^（ENDSENDER=e）^（R=r）^（W=w）^（E=e）^（[RECEIVER] =[r]）重量- .t270+4.t266- .t266+ [.t271] *[.t270][r]- .t266IF（sender！ .t267）转到B2四、&&B3GOTO B5s+ w）B4.t266-[r]B6返回12021^（结束发送R0 =e0）^（S0 =s0）^（R0 =r0）^（W0 =w0）^（E0 =e0）其中大写字母表示源（抽象）变量，小写字母表示它们的目标（具体）对应物。在简化（包括删除存在性量化器）之后，我们得到从B2到B2的跃迁的VC C22为：TS0 0C22：：'2^22^22 ！^'2不哪里22是由：（pc=2）^（：t2660 =：t266 +[发送者][权重]）^（：t2700 =重量）^（：t2710 =发送者）^（发送者0=发送者+4）^（权重=权重+4）B@^（[r]0 =：t 266 +[sende r][sende r]）^（sender+46=：t267）^（p c0 =2）CAS和22是由：（=2）^（0 =2）^（[接收R]0 =[接收R] +[发送R][称重T]）^（重量T0 =权重+4）^（发送器+ 4结束发送R）^（发送R0 =SENDER+4）我们还拥有：（发送R0 =sender0）^（RECEIVE R0 =r0）^（重量T0 =weight0）！和'0 ：（：t2670 =e0 +4）^（权重0=发送方0s0 +w0）^（：t2660 =[r0]0）其他验证条件的构造类似。它们都很容易被证实。4VOC-64：SGI Pro-64在这一节中，我们给出了一个概述，并显示了一些样本输出，作为产生的源程序的图2和它的目标图4的BASIC-64代码、手册（草案）和示例可以在www.example.com中找到http://www.cs.nyu.edu/validation/tvoc。4.1图1 -64的部件说明解 析 器 （ wh.cxx 和 wh. h ） 。 SGI Pro-64 （ 简 称 SGI ） 的 中 间 语 言 是WHIRL。在每一轮优化之后，编译器输出ASCII格式的WHIRL代码，该代码可以被解析器读取并翻译回图形表示。切割点集（ts more.cxx）。START-64计算源和目标的割点集CP SET，如下所示。割点集包括初始和终止块。每当遇到循环时，如果循环中存在一个块，该块包含赋值语句，或者只有通向循环内部块的输出边，则包括第一个这样的块0：！13IJ在cutpoint set中。如果不存在这样的块，则循环的第一块包括在割点集中。初始和终止区组也包括在临界点集中。对于上一节的示例，RST-64计算源的截断点集f0;2;4 g，目标的截断点集f0;2;6 g。路径（ts more.cxx）。CP-64计算每个源和目标的路径集CP PATHS。该集合包括适当CP集合中两点之间的所有简单路径（和循环），即，不包含CP SET中任何其他点作为中间点的路径。对于我们的示例，对于源，NT-64的计算结果是CPPATHS = fB0！ B1！ B2; B2！ B1！ B2; B0！ B1！ B4;B2！ B1！ B4 g对于每条路径Bi！CP路径中的Bj，则Bj-64计算ij，该ij是没有控制信息（即隐式）的ij。输出为源的Ps（i，j）和目标的Pt（i，j），其由适当变量和分支条件上的一组等式组成。 因此x是Px（i，j）中各项的合取，加上= i ^0 =j.例如，对于Ps（0，2）π-64， 产生：（接收器' = R）（发送器' = S）（权重' = W）（结束_发送器' = E）（S = E）I nvaria nts（ts.cxx）. 对于每个基本块Bi，i_v_c-64计算的不变量集由两种类型的不变量组成，其源是可达定义的不变量和其源是循环归纳变量的不变量。前者帮助EJB-64处理优化，如复制传播和代码移动，后者帮助EJB-64处理优化，如强度降低。计算第一类不变量.形式y的y-定义d： f（x 1;：：;x n）在从Bj到Bi的路径上可用，如果d是y在Bj中的最后一个定义，并且从Bj到Bi的每条路径都不包含y;x 1;：：;x n的（重新）定义。形式y =f（x 1;：;x n）的断言在Bi处是不变量，如果Bi处所有可用的y-定义都是形式y：=f（x 1;：;x n）。对于割点集中的每一个点，ESTA-64计算不变量的集合。检测这种不变量类似于在计算到达定义时计算x点计算第二类不变量：对于初始值分别为i0和j0的每个循环归纳变量i和j，并且在每次迭代中分别递增c1和j递增c2，计算不变量j=c2=c1i+（j0i0c2=c1）数据抽象（ts more.cxx）。编译器为我们提供了每个目标变量的数据映射，这些目标变量在源代码中有对应的变量。对于存储器访问，a[e]被解释为[&a+size]，并且[Ei]=[ej]对于任何E i = e j成立。对于一个非参数源变量V，V = v只有在V和v都被初始化后才成立。也就是说，如果v的定义出现在目标代码中，并且没有V的定义出现在源代码中的对应块中，则我们得出结论，循环不变代码的提升已经发生，并且V = v14i;jIJJn在这一点上并不成立。对于参数，我们将V = v作为前提条件。因此，在我们的示例中，我们在数据抽象中获得了（pc2f0;2;6 g）！（[R]=[r]）和（pc2f2;6 g）！（[SENDE R]=[sender]）。Control Mapping（ts more.cxx）<$-64将目标的每个初始和终端位置映射到源的初始和终端位置。目标循环到源循环的映射是使用编译器提供的信息来完成的，并且目标循环的每个切割点被映射到对应的源循环的切割点。在我们的例子中，α-64产生f 0-> 0，2-> 2，6 -> 4 g。验证条件的生成VC的构造通常很简单。然而，一个有趣的情况是，当有多个路径连接源和目标中的两个切割点时假设割点集包括Bi和Bj。进一步假设从Bi到Bj有m条不同的路径，每条路径对T贡献一个析取Pk，并且从（Bi）到（Bj）有n条不同的路径，每条路径对T贡献一个析取Q`，S（i）;（j）. 然后， VC-64生成m个 VC C k，k = 1;：; m，每个VC的形式如下：“我^^Pk！9VS：W`=1Q`^^'0.5关于循环展开的一个示意性的循环展开是在图。5（假设nc> 1.）那里L1：i=1L2：B（i）; i=i+1;如果（i =n）转到L2第三层：=）L1：i=1L2：B（i）; B（i+1）;. ;B（i+c-1）;i=i+c;如果（i+c-1<= n）转到L2 L3：如果（i>n）转到L5L4：B（i）;i=i+1;如果（i =n）转到L4 L5：图五. 循环展开有几种处理循环展开的策略一种是设计一个直接处理它的Meta规则（见下一节）.另一种方法是将循环展开视为一种特殊情况，即用大小为c的瓦片平铺一个n 1数组，然后展开最里面的循环。 第三种方法，我们在这里追求的，是考虑循环展开作为一个结构保持转换，并应用于它。因此，对于目标中两个截点之间的简单路径，将其对应的执行返回源，并检查两条路径的分支条件是否一致。我们展示了C代码及其翻译的方法，如图所示。六、0015S6！C代码[100];void unroll（int n）{整数i;对于（i=0; i n;i++）a[i]=i;}源代码（IR）B0i<-0B1 WHILE（in）B2 [a +i*8]-i i-i+1B3返回目标B0IF！（01！（I = i））和不变量'0：t'5：（t1=8i+a）^（in）^（（ni）mod 3= 0）'6：（t1= 8i+a）^（（ni）mod3= 0）例如，对于C56='5不^^56S！9V0 ：S^0 “0”，其中不遵照图5的r-h-s的程序。 生成的56：（pc=5）^（pc0 =6）^i0 =i+3）^（t10 =t1 +24）^（[t1]0 （i）^（[t1 +8]0 =i+1）^（[t1 +16]0 =i+2）^（i+ 3n）S对于23：[8I+A]0 =I）^（[8（I+2） +&A]0 =I+2）^（[8（I+1）+&A]0 =I+1）^（=2）^（I0 =I+3）^（I+ 1

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