Transformer方法的模块化和执行效率分析

可在www.sciencedirect.com在线获取理论计算机科学电子笔记307（2014）17-31www.elsevier.com/locate/entcs用Transformer计算不变量：实验可扩展性和准确性Vivien Maisonneuve1，Olivier Herzen2和François Irigoin3MINES ParisTech，法国摘要使用抽象解释，不变量通常通过迭代求解根据程序语句连接先决条件的方程组来获得。然而，也可以首先将语句抽象为transformer，然后使用transformer传播先决条件。第二种方法是模块化的，因为过程和循环可以一次性地抽象出来，避免了对调用图和所有控制流程图的迭代解析然而，基于多面体抽象域的Transformer方法会导致两个代价：在计算transformer时可能会损失一些不变的准确性，并且由于Transformer的维数是前置条件维数的两倍，执行时间可能会这篇文章的目的是1）衡量模块化方法的优点和缺点在执行时间和准确性方面，使用重要的示例和新开发的基准2）提出了一种新的减少精度损失的方法当计算变压器时，3）通过实验评估这种新技术的准确性，其他先前讨论的提供了ALICe测试用例和4）比较不同工具，ASPIC，ISL，PAGAI和PIPS的执行时间和准确性。我们的研究结果表明，在PIPS中使用的基于transformer的方法，一旦改进了transformer列表，在处理ALICe基准测试时与其他工具一样准确。 然而，当处理实际应用程序中的嵌套循环和过程调用时，它的模块化导致了更短的执行时间关键词：模型检测，抽象解释，静态程序分析，线性关系分析，自动不变量检测，循环不变量，Transformer，基准测试1介绍使用抽象解释，不变量通常通过迭代求解根据程序语句连接先决条件的方程组然而，也可以首先将语句抽象为状态转换器，然后使用这些转换器传播先决条件第二种方法是1 电子邮件：vivien. cri.mines-paristech.fr2电子邮件：olivier. cri.mines-paristech.fr3电子邮件：francois. cri.mines-paristech.frhttp://dx.doi.org/10.1016/j.entcs.2014.08.0031571-0661/© 2014 Elsevier B. V.保留所有权利。18诉Maisonneuve等人/理论计算机科学电子笔记307（2014）17模块化，因为过程和循环可以一次性地抽象出来，避免了对调用图和所有控制流程图的迭代解析然而，基于多面体抽象域[14，2]的Transformer方法会导致两种可能的惩罚：计算transformer时可能会丢失一些不变精度，并且执行时间可能会呈指数级增加，因为Transformer的维度是前提条件的两倍多面体运算符具有最坏情况下的指数复杂度，并且transformers必须处理每个变量的两个值，即前置条件中的值，即过去值，以及后置条件中的值，即新值，而前置条件仅需要当前值。本文的目的是：1）使用参数示例和新开发的用于循环不变式分析的基准套件ALICe [ 18 ]来测量模块化方法的优点及其在执行时间和精度方面的缺点，2）提出一种新技术，该技术用于减少计算循环不变式时的精度损失，即控制路径变换器，3）为了评估这种新技术和以前在[ 2 ]中讨论但未实现的旧技术的精度增益，提供ALICe测试用例; 4）使用前提条件传播或Transformer计算来比较不同工具的执行时间和精度。也就是说，我们比较了ASPIC[8]，这是一个基于加宽和加速的标准抽象解释（AI）工具，PAGAI[13]，一个基于SMT的AI工具，ISLSet库，ISL[24]，这是一个包含Presburger关系的传递闭包的库和PIPS[15，14]，这是一个使用多面体集合抽象转换器和先决条件的编译框架。比较是困难的，因为这些工具有不同的输入和输出语言，但这是由ALICe框架处理的本文中考虑的提高变换器方法精度的技术是沿不同控制路径计算变换器以将凸包运算推迟到前提条件传播阶段，基于先前计算的前提条件迭代计算新变换器[2]，利用幂等变换器[2]以及通过分裂和专门化控制节点[17]获得的控制虽然我们努力使这篇论文自成一体，但首先阅读[2]或遇到困难时可能会有所帮助。论文的提纲如下。由于基于transformer的方法不常见，我们在第2节中简要介绍它。然后，我们提出了第一组实验结果，以探索[2]（第3节）中提出的技术存在的准确性和执行时间问题。遇到的精度问题可以追溯到早期的凸壳运算，在第4节和第5节中详细介绍了几种旨在尽可能推迟它们的技术。最后，我们用ALICe（第6节）衡量这些改进的影响，并得出结论。诉Maisonneuve等人/理论计算机科学电子笔记307（2014）1719T（）voidfoo（floatx）{intn=0;while（1）if（x）if（n）n++;其他// T（）{0==-1}voidfoo（floatx）{// T（n）{n==0}intn=0;// T（n）{n#init==0}而（1）// T（n）{n =n#init+1}if（x）voidfoo（floatx）{//public void run（）{intn=0;// P（n）{n==0}而（1）// P（n）{0 =n，n =60}if（x）n=0;}// T（n）{n =60，n=n#init+1}if（n）// T（n）{n==n#init+1，n=60}n++;其他// T（n）{n==0，60 =n#init}n=0;}// P（n）{0 =n，n =60}if（n）// P（n）{0 =n，n =59}n++;其他// P（n）{n==60}n=0;}Fig. 1. 计数器的语句、变压器和先决条件（Halbwachs&等人））2用Transformers不变量通常通过沿着程序的控制路径传播前提条件来计算，直到为每个控制节点获得稳定的前提条件。为了避免无限传播，使用特殊的近似算子，例如加宽算子，以保证在有限步数内收敛相反，PIPS依赖于一个模块化的替代方法，使用一个可调变换器[15]，即。表示传递函数的多面体。图1显示了Halbwachs等人 [12]使用的反例的变换器和预条件基本状态的变压器包含许多方程，因为通常很少有变量被修改。这些方程是隐式的，而修改后的变量作为自变量列出。最后，使用#initsuccix来区分旧值和新值。2.1用PIPSPIPS中使用的算法假设调用图中没有循环，并按如下方式进行。首先，每个程序命令S，基本或复合语句或过程调用，由一个可调的变换器TransformerS，P过度近似，可能使用关于S的前提条件P的信息。这是一个自下而上的过程，在下面的段落中详细描述，因为当没有信息可用时，可以将默认值用于前置条件P。每个函数只分析一次，并且它的Transformer在每个调用站点重用。然后，使用转换器从程序起始点这种方法也可以用于非结构化程序：控制流程图要么变成等价的结构化图[1]，要么通过添加转换来近似和简化，要么使用分解成循环[5]进行分析PIPS使用的两阶段方法如下。我们假设电子指令已经变成了变压器，并显示如何控制结构得到处理。序列设xi，x′i和x′i′表示变量xi在不同状态下的值一20诉Maisonneuve等人/理论计算机科学电子笔记307（2014）17·⊔⊔∗选择“T或T“的结果T≤Tx， .. . ，x，x， . ，x11n消除“中间”值x“，...，x′′。 我们注意到这个操作T○T。21n1=（TT○Tc）（）<$（TF○T<$c）（）=（○（）一个连续的变压器序列（关于值） 在 T2 （ 关 于 值x′1′， . ，x′n′，x′1， . ，x′n），然后投影到x1， . ，xn，x′1， . ，x′n到一般情况下的凸多面体（两个凸多面体的并集不是凸多面体）。 最好的凸逼近是凸并T1T2. 这 通常是有损操作。Loop给定一个循环体的一个递归TransformerT，递归变换器T表示T的任何迭代次数的结果。它是由一个新的导数闭包算法计算[2]。出现的不精确性的两个主要来源是循环（）和并行路径（）的抽象。当多个控制路径出现在循环和嵌套循环中时，它们的影响会累积。请注意，纯自底向上的方法可能会被使用，也可能不会。由于转换器不是并发计算的，而是通过遍历AST计算的，因此可以立即使用一个Transformer的量程或一个测试的条件 例如，这解释了为什么条件n60出现在Transformer中 语句n++;。2.2不变量的生成不变量，也称为前提条件，使用在前一阶段计算的转换器从程序的初始状态向前传播。然而，当一些前置条件被直接重新计算用于复合语句时，准确性得到了提高。例如，条件if（c）TTelseTF的后置条件可以作为两个分支的后置条件的凸包PostPre Pre或者作为由条件Transformer变换的前置条件PostTTTcTFTc Pre来获得。 第一个方程以很小的代价提供了更准确的结果，因为无论如何都要计算分支后条件。3模块化和精确度： 实验结果PIPS是作为一个编译框架开发的，能够跨过程处理大型应用程序[21]。重要的是要检查变压器提供的模块化是否会导致预期的速度提高，并测量其对精度的负面影响程度。我们首先表明，PIPS在处理循环嵌套和过程调用时，相对于其他三个工具，ASPIC，ISL和PAGAI，在很短的时间内获得准确的结果。然后，我们回顾了以前的实验结果，这些结果表明，在处理以前发布的用于说明不变式生成算法的小测试用例时，缺乏准确性[18]。诉Maisonneuve等人/理论计算机科学电子笔记307（2014）17213.1使用的工具当处理状态转移关系时，传递闭包对于计算不变量[6，2]，检查循环终止或导出循环复杂性[11]，建立依赖约束或将凸数组区域从一个控制点移动到另一个控制点[16]是有用的。当处理依赖关系时，传递闭包对于优化或合成代码很有用[26，25，4]。很难比较为这些目标之一而设计的不同工具所使用的算法和算法，因为它们需要不同的输入并产生不兼容的输出。此外，输入的编码通常会影响分析。我们选择将PIPS与两个基于前提条件的标准抽象解释工具ASPIC[9，8]和PAGAI[13]以及Presburger等效库ISL[24，25]进行比较，因为它包含一个强大的传递闭包算法，最初设计用于计算数据依赖关系，优于[23]。ASPIC和ISL与PAGAI和PIPS不同，它们既不处理C的复杂性，也不处理它们的自动抽象。由于这些工具具有非常不同的结构和执行时间，因此我们直接报告ASPIC、ISL和PAGAI的时间命令报告的用户和IO时间之和，或者使用PIPS的transform和precondition通道的TIMINGS获得的时间。通过这种方式，PIPS的C解析部分被消除了，因为它适用于使用内部格式的ASPIC和ISL以及使用Clang进行解析的PAGAI，并且我们比较了可能被基于其他工具的新通道取代的PIPS此外，每个工具的执行时间的演变是完全相关和有趣的。基准测试在由四核Intel i7-2600处理器驱动的计算机上运行，该处理器的频率为3.40 GHz，具有16 GB内存，使用ASPIC版本3.3、ISL版本0.12.2、PAGAI版本14-04-07和PIPS修订版22 134。3.2循环嵌套对收敛性嵌套回路在科学代码中很常见，并且易于使用变压器进行分析然而，Halbwachs在[12]中使用了2D循环嵌套来显示加宽技术的改进。让我们考虑图2左边部分的代码，一个矩阵乘法。为了检查所有数组访问都是安全的，需要i，j和k上的不变量，这需要分析3D循环嵌套。为了理解工具的时间行为，我们测量了Transformer的执行每个循环都有一个 零 下 界 和 一 个 符 号 上 界 ， 对 于 （ i_k=0; i_k< b_k; i_k++ ） ， 循 环 体 是 空的，;。 没有关于循环上限b_k的信息：每个循环都可以进入或跳过。结果示于表1中。使用变换器或加速的工具的执行时间不是深度的一个线性函数，因为变量的数量增加的速度是深度的两倍，并且因为多面体算子以其指数最坏情况的复杂性而闻名但是，它不会增加得很快，特别是对于22诉Maisonneuve等人/理论计算机科学电子笔记307（2014）17intnums（intnums，intnums，浮点数A[l][m]，浮点数B[l][n]，int[n] nums（nums）{inti，j，k;for（i=0; i l; i++）{对于（j=0;j m; j++）{A[i][j]= 0.;对于（k=0; k n; k++）A[i][j] += B[i][k]*C[k][j];}}}intn，intp，int[n][n]，int [n]，int[n]，int [n]inti，j，k;for（i=0; i n; i++）对于（j=0; j n; j++）A[i][j]= B[i][j];对于（k=1; k p;k++）{intn [n];for（i=0; i n;i++）对于（j=0; j n; j++）T[i][j]= A[i][j];mm（n，n，n，A，T，B）;}}ISL0.0000.0100.0370.0830.3700.8531.1977.9275.713PAGAI0.0670.1870.4200.7971.3732.2603.6205.7809.643PIPS0.0040.0090.0150.0210.0300.0390.0530.0710.090表1具有不同深度的空嵌套for循环的不变分析时间（秒）main-12个内联主-23个内联主要-34个内联main-45个内联main-56个内联肉冻–––––ISL–––––PAGAI0.980 1.4171.383 5.6802.030 14.67730.00753.247PIPS0.048 0.0430.049 0.0630.048 0.0840.050 0.1080.051 0.127表2内联版本的过程间分析和过程内分析的时间（秒）当不使用内联时，函数中常见的嵌套深度3.3过程间分析或内联图2右边的代码是一个矩阵求幂mp，它在一个循环中包含一个对矩阵乘法mm的调用函数mp是从一个主函数调用的在内联之后，可以在过程间或过程内分析这些代码。表2包含主程序调用mp 1到5次的执行时间测量每次测量进行10次，并显示中位时间。代码要么在过程间进行分析，要么内联被调用者，这将调用站点的数量减少到零。当同一函数的多个调用点出现在被分析的程序中时，模块化变得越来越有用。此外，内联增加了循环嵌套深度，这对执行时间不利，如上一节所示。3.4使用ALICe在本节中，我们回顾了用ALICe获得的实验结果，并发表在[18]中。ALICe基准已开发用于评估鲁棒性，图二. 矩阵乘法和取幂：A=B×C和A=Bp深度肉冻1234567890.037 0.043 0.040 0.053 0.047 0.063诉Maisonneuve等人/理论计算机科学电子笔记307（2014）1723各种不变量生成工具的准确性。版本1.0支持三个工具，ASPIC，ISL和PIPS，并包含102个测试用例，这些测试用例来自处理循环不变式或终止的论文。它使用FAST格式作为中性参考格式，并为每个测试用例提供不同的编码无论编码如何，PIPS是三种工具中准确性较低的，有43个良好结果，而ASPIC为75个，ISL为63个。但是没有一个工具比另一个工具更好：对于每一个工具，至少有一个模型可以通过这个工具成功分析（参见图3）。此外，表3没有显示出生成的不变量的准确性的明确趋势，通过包含不变集来测量更仔细的分析表明，ISL在使用并发循环（单个控制点上的几个循环）编码的测试用例上执行得相对较好，而PIPS在这种情况下的结果特别差。另一方面，ISL在显示大型复杂控制结构的测试用例上可能会非常慢。最后，尽管取得了成功，但ASPIC在处理具有复杂公式的过渡方面面临更大的困难，它无法加速这种过渡。成功：78失败：24ISL12223911肉冻21PIPS图三. ALICe102测试用例的维恩图表3。不变包含3.5实验执行时间和精度在PIPS中实现的模块化方法，在使用函数调用和嵌套循环处理大型程序时，在准确性和执行时间方面是有效的[21]。然而，它缺乏准确性计算时，经常针对小transi-tion系统的不变量自动生成的文献。精度损失主要是由于在近似传递闭包之前在Transformer空间中执行凸包，但也观察到几个整数过凸包4Transformer计算我们提出了两个新的改进变压器为基础的分析。第一个处理并发循环，第二个处理整数上的循环4.1并发循环我们正在处理结构化代码。为每个循环体构建控制路径集。当发现测试或循环时，复制每个预先存在的控制路径，以考虑真分支和假分支，或循环入口和跳过。这不是递归地沿着分支或内部循环体执行的。因此，控制路径的总数最多为2k，其中k是循环体中语句（可能是复合语句）的数量ISLPIPS⊇5ASPIC ISL PIPS肉冻–3321–2354–24诉Maisonneuve等人/理论计算机科学电子笔记307（2014）17++CUP=CC≤≤=（）i 1i0ii=+正+ +∗P2=Ti（Tj（P0））P+=Ti+（P0）P3+=Ti+（Tj（C（P1）4.2回路中的控制路径变压器让我们假设一个循环包含几个控制路径，每个控制路径由它的变换器Ti定义。这样的循环在上面被称为并发循环循环前提条件，，可以被分解成一组前提条件，每个前提条件在可变次数的迭代之后获得，并通过凸壳算子被合并在一起，PP0 P2P+P3+ （1）P0是第一次进入循环的前提条件。P2是用不同的控制路径经过两次迭代后得到的。P对应于只有一个控制路径用于所有迭代的情况;它包括P1，第二次迭代的前提条件。最后，P3是对应于具有至少三次迭代和两个不同控制路径的所有较长控制路径ijii iji是过渡集的凸壳的传递闭包的过逼近，CT和P是一次迭代后的条件，TP。当使用PIPS中的默认公式PP0C P0时对于等式1，它们稍后在前提空间中执行，并且每个基本转换Ti被应用为最后一个转换。因此，由幂等变换带来的信息被保留。用于计算循环不变量的公式已经展开，以明确考虑多达三次迭代。可以将其推广到k步，其中项的数量呈指数增加。但我们缺乏证明这一发展的实验案例。[12]图1中的例子。重置为0是由一个Transformer抽象的，该transformer不能与抽象条件增量的Transformer准确合并，并且用[2]中给出然而，等式1提供了精确的循环不变量，0n 60，通过将它们、它们的传递闭包和初始循环预条件相结合，得到了一个新的循环预条件。4.3方程式1的动机公式1，结合P2，P和P3，被开发出来：(i) 将在Transformer空间中执行的尽可能多的凸包转换为在不变（前条件和后条件）空间中执行的凸包;例如，增量和减量的合并不会导致任何信息，而不管用于控制其执行的条件如何。(ii) C，C的传递闭包，相关变换的凸壳每个控制路径，往往是不精确的。信息，尤其是幂等诉Maisonneuve等人/理论计算机科学电子笔记307（2014）1725+○ =可以使用每个控制路径TransformerTi作为迭代的这可以推广到Ti。(iii) 在某些情况下，控制路径i可以跟随控制路径j，但j不能跟随i（T j T i）。通过考虑最后两种不同的迭代，排除了一些不可能的多迭代路径。4.4数字精度中间的计算可能会产生具有巨大系数的多面体，导致即使是64位整数也需要在凸包上进行算术运算，因为约束常数被凸包运算符转换为系数。最后，当过流发生时，一些约束可能会被丢弃，并且所得到的不变量比它应该的准确度低为了解决这个问题，我们为一些PIPS多面体运算符添加了GMP支持。这个看似纯粹实用的实现决策允许多面体算法的大幅简化，因为不再需要处理过流异常。事实证明，这对执行时间（现在快了大约6倍）以及基于Transformer和基于预条件的分析之间的比较都有积极的影响。5Transformer计算我们回顾了基于变压器的分析的几个改进它们可以直接应用于源代码，也可以应用于现有的分析。它们已经在[2，17]中发表，但它们仍然需要实施和实验。5.1基于节点分裂的将不变信息附加到控制节点。如果它们的数量增加，当使用多面体不变量时，可以找到更精确的不变量，因为全局不变量是节点不变量的析取。此外，程序的行为可以变得更容易分析，因为更少的弧可以加入分裂节点。然而，新节点的存在通常会增加分析时间，并且必须在精度和节点数量之间找到折衷Maisonneuve开发了一种拆分控制节点的方法[17]，只有在可以预期某些好处的情况下才拆分节点这种算法，fsmnodesplit，已经被实验证明和验证[17，18]，但没有集成到PIPS中，是改善PIPS结果的主要候选者，并观察其相对于通过分裂，合并或合并然后分裂节点获得的测试用例的不同等效编码的鲁棒性。它也适用于其他工具。5.2迭代分析有时可以通过第二次重新计算变压器来改进前提条件，使用第一组前提条件作为输入以限制其域和范围。26诉Maisonneuve等人/理论计算机科学电子笔记307（2014）17不= T（）=（（））Pn+Tn+1不∗voidfoo（intflag，floatx）{inti，j=1，a=0，b=0;if（flag）i=0;inti=1;while（x>0.）{1}a++;b +=（j-i）; i+= 2;if（i =0）j+=2;elsej++;}迭代1：while（x>0.）{1}// P（a，b，i，j）{2a==i，j =2a+1，a+1 =j}迭代2：while（x>0.）{1}// P（a，b，i，j）{2a==i，2a==j-1，0 =a，b =a}迭代3：if（flag）assert（a==b）;}while（x>0.）{1}// P（a，b，i，j）{a==b，2a==i，2a==j-1，0 =a}见图4。 例如，Dilig&al。：当flag！=时迭代获得的源代码和循环不变量0intmain（）函数{intx=0，new=0，old=1，y=0，z=0;while（x 10）{if（new==0）;其他z++;new = 1 - new;old = 1 -old;迭代1：while（x 10）{// P（new，old，x，y，z）{new+old==1，y+z==x，//0 =new，new =1，new =x，x =9，y =x，0 =y}}// P（new，old，x，y，z）{new+old==1，x==10，y+z==10，// 0 =new，new =1，new =y，y =new+9}迭代2：x++;}while（x 10）{if（new==1old==0|| new==0 &&old==1)printf("property verified\n");其他printf（“未找到属性\n”）;}// P（new，old，x，y，z）{new+old==1，new+x==2y，// new+z==y，0 =new，new =1，new =y，y =new+4}}// P（new，old，x，y，z）{new==0，old==1，x==10，y==5，==5}图五、周期性行为：循环不变式和后置条件如[2]中所解释的，transformers和前置条件之间的迭代关系由以下两个等式形式化，其中B代表循环体语句和延续条件，对于将语句转换为凸transformer的函数，P0表示任何状态，n为正数：Tn1B，PnPn，PnP0Tn中国（2）请注意，前面的前提条件（可以使用公式1更精确地计算）以两种不同的方式影响Transformer抽象函数是锐化的，并且所得到的Transformer的域也受到前面的前提条件Pn的限制。图4中的示例发表在[7]中。函数foo有两个不同的行为，这取决于flag的值，它在循环中使用了一个非随机条件，i%2==0。 依赖于形式参数的不同行为可以通过克隆函数来分离，并且当关于i的奇偶性的信息已知时，可以精确地分析模运算符返回的值。当flag不为零时，可以推导出a等于b。为了得到函数后置条件中的三个方程，transformers必须计算三次，因为每次前置条件都使语句的抽象更加精确。5.3周期性在科学计算中会出现周期性行为，例如，当两个子数组交换时，以避免每次在旧值的位置复制新值诉Maisonneuve等人/理论计算机科学电子笔记307（2014）1727=（） ○（）=（） ○（）publicint findDuplicate（intfindDuplicate）{while（x！（0）if（x）x--;elsex++;}}public int findDuplicate（intx）{while（x！（0）while（x！0&&x>0）x--;while（x！0 && x =0）x++;}}图第六章 While-if到while-while的 转换：Massé和Cook&等人的例子。步骤x，A[new][*]=f（A[old][*]），代价是仅仅交换索引。为了并行化这些程序（参见图5的第1列），编译器必须找到不变量new+old==1，然后在数据依赖性测试中使用该不变量以及连接方程new==old，以表明A[new][*]和A[old][*]指的是不同的位置集。正如[2]中所指出的，有不同的方式来编码交换，并且上述不变量可能或多或少容易生成。然而，不管编码如何，行为总是周期性的。如果将循环Transformer的传递闭包计算为其幂之一的函数，则可以保留更多信息[2]。例如，平方对幂等函数和周期为2的函数很有用T<$T 2<$T2<$，T +TT 2+TT2+。这可以推广到T的任何幂。由于还没有应用程序需要更大的周期性，我们目前在PIPS中的实现仅限于T2。最后请注意，迭代分析（见5.2节）改进了周期函数的不变量：找到了y和z之间的关系（见图5的第2列）。至于图4中的Dilig示例，在[2]中，迭代不仅与非多面体不变量有关，而且与多面体不变量有关，并且它们可能收敛。5.4While-If到While-While转换这种优化，将测试转换为while循环中的while循环，也在[2]中使用，并在扩展版本中证明是正确的[3]，但它尚未实现，既没有显式地使用程序转换，也没有隐式地计算循环不变量。事实上，除非使用控制路径变换器，否则其对于使用凸包来获得唯一环路Transformer可能具有有害效果。图6[20]中的例子显示了一旦内部测试变成一对while循环，证明循环终止是多么容易。6改进的实验评价尽管PIPS的设计目的不是分析学术论文中使用的循环不变量和终止的小测试用例，但使用它们来衡量上述改进的影响以及将PIPS与其他能够计算不变量的工具相此外，测试案例未解决28诉Maisonneuve等人/理论计算机科学电子笔记307（2014）17=∑FSMC肉冻ISL默认CPPIPSIA CP-IACP-IA-MP直接5497154824323成功时间7510.96335.5436.1697.84518.57219.673151.4分裂93487572224199成功时间7912.87243.0505.7726.85614.47519.077113.3合并5579153805187成功时间5916.77026.2406.2668.04418.56719.768225.9合并620638941成功70836379658082&分裂4549时间11.340.86.69.616.823.0222.2表4ALICe测试用例的直接、拆分、合并合并-拆分版本以及具有不同选项（控制路径转换器、迭代分析、MultiPrecision）的ASPIC、ISL和PIPS的成功率和执行时间FAST文件和fsm2c生成的C文件的行数大小在左侧显示。通过消除大于1 KB的文件和第一次PIPS通过，可以减小文件大小（控制简化）。 复制了ASPIC、ISL和PIPS[19]为方便起见，PIPS的执行时间不像[19]中那样测量是设计不变量生成新改进的良好起点6.1编码的影响和对ASPIC、ISL和PIPS的表4提供了ASPIC、ISL、PIPS基线和PIPS的ALICe基准[18]的四种不同编码的成功次数和总执行时间，其中一些改进在第5节中定义。正如预期的那样，对于ALICe版本1.0中的测试用例然而，使用控制路径Transformer集和有利的编码可以在每秒解决的测试用例数量方面提供出色的结果，并且未来的不变量生成基准可能会有不同的配置文件。请注意，表4中未显示的定期分析并没有改进ALICe中当前的任何测试用例。我们认为，这一基准应随着新案件的出现而定期提高;如有任何反馈，我们将不胜感激。还请注意，表4中的PIPS的执行时间与[18]中在[18]中，执行时间为：tWINGi∈ALICe时间（PIPS（fsm2c（情况i）这是所有测试用例的PIPS处理时间的总和，这些测试用例是由fsm2c转换成C语言的。这对PIPS非常不利，因为它的启动时间很长，因为许多传递（如解析）不是由其他工具执行的，因为FSM2C也有负面影响。为fsm2c选择的C编码意味着解析stdlib头、PIPS的过程间分析、大量无法访问的代码以及生成的代码大小的指数级增长。为了减少PIPS所产生的开销，我们消除了测试用例，不能再生在少于1000行，我们取代的功能编码的aleas的未解释的表达式，我们使用PIPS消除无法到达的语句，我们处理所有的测试用例在一个调用PIPS。正式的执行时间是现在：诉Maisonneuve等人/理论计算机科学电子笔记307（2014）1729=（（i∈ALICe测试时间PIPS PIPS替代品Csize（i）< 1000fsm2c（casei）这将PIPS执行时间减少了7到10倍6.2PIPS故障分析在102个测试用例中，ALICe基准测试包含9个涉及非Presburger不变量的测试用例，PIPS发现82个不变量 剩下11个案例需要进一步研究，即：halbwachs7、henry 、 metro 、 microsoftex2 、 microsoftex5 、 popeea 、 realheapsort 、realheapsort_step2、subway、synergy_bad和ticket（http://alice.cri.mines-paristech.fr）。ALICe基于FAST格式，用于从FAST控制流图生成结构化C的解析fsm2c可能会呈指数级增长，最高可达300 Kbps（metro，realheapsort，realheapsort_step2和subway至少）。当一些测试用例用C编写时，使用发布时的while循环，henry，halbwachs7和synergy_bad [10]的不变量由PIPS找到。案例microsoftex2在[11]中进行了分析，以检测循环终止。所需的信息不是不变量，而是一个Transformer，PIPS计算所需的Transformer。在[11]中还使用非凸变换器分析了Case microsoftex5。它包含两个嵌套的while循环，内部循环可能是也可能不是恒等函数。关于身份行为的信息不被PIPS保留，因为控制路径不是递归地沿着循环建立的，以保持它们的数量很小。该测试用例需要不同的算法来构建PIPS中的控制路径。Popeea [22，11]有一个非凸不变量，只能通过以下方法找到： 如果添加了新的控制点，则使用凸形工具。ALICe使用的解析法fsmnodesplit可能无法发现正确的节点拆分。 案件单[6] 很有趣，因为它很容易使不变量凸。然而，控制路径的数量很大，并且PIPS使用的凸包在while循环展开时会导致过度溢出该算法被描述为一个过渡系统，它可以在C中编码的方式是至关重要的PIPS分析。7结论我们提供了支持Transformer方法的实验结果。当分析具有许多函数和嵌套循环的大块代码时，相对于通常的基于前提传播的抽象解释方法，它具有时间效率。然而，正如我们在ALICe基准测试中所观察到的那样，小测试用例缺乏准确性。因此，我们提出了一种新的技术，控制路径transformers，并使用它来计算循环不变量，以及Transformer闭合和循环不变量生成的几个改进，包括使用多精度数，迭代分析，支持幂等和周期行为，以及输入重新编码。30诉Maisonneuve等人/理论计算机科学电子笔记307（2014）17这些改进，其中大部分在[2]中描述，已经在PIPS中实现，并针对ALICe基准的102个测试用例进行了测试。第6节中给出的结果表明，三项改进具有积极的效果，PIPS现在与ASPIC和ISL等更专业的工具一样准确。因此，尽管ALICe是非常有用的第一步，但开发一个用于研究循环不变量的通用基准，无论是否是一个循环不变量，仍然是一个悬而未决的问题。应该重新考虑为ALICe及其算法fsm2c所做的选择，以支持更大的测试用例和可伸缩性研究。例如，存储测试用例的C版本将是有用的，以便于添加新的用例，并简化PAGAI和PIPS等C分析器的使用。最后，ALICe中的一些测试用例没有被我们使用的三个工具中的任何一个处理有些不被PIPS处理，因为变换器或不变量不是凸的。仍然需要更多的工作来使用基于多面体的Transformer技术自动生成更多的不变量，同时避免从FAST文件生成C代码时或使用控制路径变换器和/或迭代地分析代码时的特别是票证算法，还有一般的控制重构，值得新的进步。确认我们感谢Paul Feautrier、Laure Gonnord和Sven Verdoolaege帮助我们使用他们各自的工具C2fsm、ASPIC和ISL。我们还要感谢Pierre Jouvelot和我们的三位审稿人非常仔细的阅读和出色的建议。引用[1] Ammarguellat，Z.，一种控制流归一化算法及其复杂性，IEEE软件工程学报18（1992），页.237-251。[2] Ancourt，C.，F. Coelho和F. Irigoin，A modular static analysis approach to a Clonne loop invariantsdetection（2010），pp. 3[3] Ancourt，C.，F. Coelho和F. Irigoin，A Modular Static Analysis Approach to A Clonne LoopInvariants Detection（extended version），Technical Report A-419，MINES ParisTech，CRI（2010）.[4] Bielecki，W.，K. Kraska和T. Klimek，参数化完美嵌套循环的依赖关系的联合的传递闭包，在：并行计算技术，2013年，pp。37-50.[5] Bourdoncle，F.， 毕业论文，巴黎综合理工学院（1992年）。[6] Bultan，T.，R. Gerber和W.Pugh，使用Presburger算法的无限状态系统的符号模型检查，在：计算机辅助验证，1997页。400-411[7] 迪利希岛T. 迪利希湾Li和K.麦克米兰，通过溯因推理归纳不变的生成，在：OOPSLA443-456[8] Feautrier，P.和L. Gonnord，用aspic和c2fsm加速C程序的不变式生成，电子。注意Theor。Comput.Sci. 267（2010），pp.三比十三[9] 贡诺德湖和N.Halbwachs，在线性关系分析中结合加宽和加速度，在：K. 易，主编，静态分析，计算机科学讲义4134，2006页。144-160诉Maisonneuve等人/理论计算机科学电子笔记307（2014）1731[10