循环边界分析与协变变量的时态属性验证

可在www.sciencedirect.com在线获取理论计算机科学电子笔记289（2012）41-51www.elsevier.com/locate/entcs具有协变变量的循环的规范化MarianneDeMichiel1ArmelleBonenfant1HuguesCass'e1IRITUniversit'edeToulouseToulouse，France摘要时态属性验证对于确保关键实时系统的安全性至关重要。这种验证的一个主要组成部分是计算最坏情况执行时间（WCET），这反过来又需要确定循环边界。 虽然在这一领域已经进行了大量的工作，这类案件仍然是比较普遍的，没有得到解决。例如，据我们所知，没有快速的自动方法可以处理一个简单的二叉搜索查找的循环边界。本文提出了一种用算术-几何级数求解此类循环的方法，即用多变量算术和/或几何递增的循环。我们已经在我们的工具oRange中实现并试验了这种方法。关键词：时序分析，最坏情况执行时间，循环边界分析，抽象解释1引言关键的硬实时系统由必须在截止日期前完成的任务组成为了保证这一点，任务调度分析，这需要的知识，每个任务的WCET，进行。静态WCET分析是由一个时序分析工具，需要循环上限。这样的界限可以由开发者在程序中手动注释或通过自动评估来给出。自动方法更用户友好，更不容易出错，但没有自动方法的循环边界分析可以给出一个确切的答案，所有的循环。本文提出了一种新的方法来扩大可计算循环界的域与协变感应变量。我们专注于为边界（迭代次数）找到一个数值，而不是程序的终止[4]。WCET质量取决于找到的边界的质量。1电子邮件：{michiel，bonenfant，casse}@ irit.fr1571-0661 © 2012 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.11.00542M. De Pastel等人/理论计算机科学电子笔记289（2012）41几种方法已经在关于循环边界的循环流分析中进行了探索[2，1，7，11，14，5]。这些方法中的大多数使用抽象解释[6]来构建一个映射，该映射将变量与其值的抽象表示相关联。这允许在不同的程序点上给出安全的，但可能被高估的状态集。二进制searc h的一个经典例子是M é lardalen基准测试套件[ 3 ]的程序我所知的，只有一种方法，那就是在[14]和[9]中描述它然而，[14]使用二元紧缩的模型检查并将其扩展并嵌入到使用一套分析方法的更一般的方法作为一个整体的结果，它增加了计算复杂性证明或反证相关的时间界限的程序。SWEET [9]通过使用扩展每个循环迭代的抽象执行来解决循环边界。在这两种情况下，解决方案的通用性是以计算时间为代价的，有时是令人望而却步的。此外，这些工具获得循环边界值，并且不能在不同的调用上下文中实例化。在[12]中，74%的Müalardalenben chmark循环 被成功计算，但没有详细说明处理了哪些循环（特别是“bs. c“）。oRange [13]将基于C程序的循环绑定表达式与抽象解释相结合。对于循环Li，计算两种类型的循环边界：totali（程序的整个执行中的迭代总数）和maxii（每次循环启动的最大迭代次数）。分析过程分为三个步骤：1）对增量和循环边界表达式进行上下文无关的识别和规范化[8]，2）对totali和maxi符号表达式进行上下文相关的构造，最后3）计算最终的totali和maxi表达式和值。oRange支持多种条件类型（包括例如），最常见的归纳变量表达式（即包含+，-的表达式、×、/）和任何类型的C循环语句。复杂的控制流程语句（break、goto等）由程序的语义保持简化器处理表示.在[13]中可以找到oRange的完整描述。本文的组织如下：第2节是动机，第3节介绍了我们的方法，第3.5节描述了一些限制的方法，第4节是一个典型的例子，我们在第5节结束。2具有算术几何级数的在下面的程序中，函数oracle返回一个整数，可能是随机值：示例1：基本协方差虚空public void run（） {int i=0， j=10;while（ i j）{<如果（oracle（））i=（i+j）/2;否则j=（i+j）/2;}}M. De Pastel等人/理论计算机科学电子笔记289（2012）4143while循环的迭代次数取决于两个变量i和/或j，它们在选择的两个分支中分别被修改。由于这些变量都是条件归纳变量，所以称之为协变量，循环迭代界要求考察这些变量的协变。这种类型的循环称为协变。规范化的目标是得到一个循环，循环变量通过[0.最大值]递增1。这允许简化计算，特别是在嵌套循环的情况在oRange执行的初始分析中，如果两个或多个路径导致条件归纳变量的不同增量，则相关增量值近似为T（任何可能的增量），因为我们无法支持多个增量。 为了调查变量i和j如何演变，一个新的引入元变量X，使得X = j − i总结了循环条件下i和j的演变。X是一个临时变量，它允许处理常规归一化。 为了实现这一点，我们在每个包含i或j修改的块的末尾插入一个新的X赋值，以考虑i和j修改对X的影响。示例1的if指令现在变为：实施例2：引入X用于系列测定public void run（）{i=（ i+ j）/2;X=j-i;}其他j=（ i+ j）/2;X=j- i;}然后，分析X，并将oRange的变量重写算法应用于选择的then部分的赋值，产生Xn <$jn−1−（in−1+jn−1）/2=（jn−1−in−1）/2，即Xn=Xn−1/2。 else-部分的赋值也可以用同样的方法进行：Xn<$（in−1+jn−1）/2−in−1=（jn−1−in−1）/2，即Xn=Xn−1/2。最后，在这个特殊的例子中，X在每个bran ch上的形式可以结合起来，得到几何级数Xn=Xn−1/2。如果连接可以产生已知序列，则重写初始程序以嵌入X作为条件归纳变量（初始化，循环条件，主体增量），其边界表示整个循环边界的安全估计（如下所示）。示例3：循环的最终重写虚空public void run（） {inti=0，j=10，X;X =j-i;while（0< X && ij）{<如果（oracle（））i=（i+j）/2;否则 j=（i+j）/2;X = X/2;}}第一种方法是正确的（通过重命名是微不足道的），当归纳变量是重复的点值时。整数使事情变得有点棘手，因为除法和模的离散算术的特性。实际上，我们得到44M. De Pastel等人/理论计算机科学电子笔记289（2012）41我JI jX01，c是一个二元表达式exp=exp1opexp22，其中op∈{<，≤，≥，>}，且至少nx∈I，ny∈I，如x和y至少在b的两条不同路径上被修改，则x和y是协变变量。3.2条件及其诱导变量我们在这里展示如何确定循环体中执行的增量，以及如何检查它们是否可以被处理。我们目前的分析只支持一个简单的形式（exp = k0 + i∈[1. n]k i× x i）。设ki是变量xi∈LVE（exp）的系数ki在Z或R中这取决于比较运算符的类型。如果所有的k i都可以被求解，我们就可以找到循环变量的增量：X = i∈[1.. n]k i×x i.为了将协变变量的分析替换为X的分析，我们在代码中插入赋值X = i∈[1.. n]k i×x i到特定位置：在循环体之前和每个块之后修改x i。此外，条件c被替换为CJ= 0opX+k0c。这个定义允许处理X的界限，即使表现出对X的高估3.3增加量评价在这个探索步骤中，我们认为归纳变量的递增只在循环体中执行，而不是在被调用的函数中，也不是在内部循环体中。在实际执行中，我们认为，2exp=exp1op exp2当op∈ {>，≥}和exp=exp2op exp1当op∈ {<，≤}只有支持<或≤对照药物⎩46M. De Pastel等人/理论计算机科学电子笔记289（2012）41在后面的情况下，无法分析增量（尽管假设T为了缩短介绍，我们只介绍归纳变量按顺序或条件路径修改实际上，其他情况在实际执行中也有处理。抽象解释应用于指令序列和抽象存储σ，并导致新的抽象存储。 初始值为σ0=σ2。这些状态是按顺序计算的。设pl是最后一个被评估的程序点，σ pl是它的上下文。以σ pl为输入抽象存储器，对程序pi n t p j的下一个p i n tpj进行赋值，并将程序pintpl后的状态赋值给程序pi ntpj。结果是输出上下文σpl和X符号表达式。示例4：计算点位置while（. ）{//p0如果public voidrun（）{i=（ i+ j）/2;X=j-i;//p1}其他j=（ i+ j）/2;X=j-i;//p2}//p3}第一次求值，在p1中得到X<$ j-（i + j）/2。 第二个，在p2中得到X←（i +j）/2-i。本文根据X在p_t_j处的一般形式，给出了一个已知的形式X←q_jX+k_j_0为算术-几何级数[10]。如果qj≥0s，则我们将其密封。t. i∈[1.. n]kj=qj×kj，i. 如果我们没有找到合适的形式，则X被评估为T。3.3.1序列中的增量求值：updateJ设X=q1X+k10是X在序列中的第一次赋值，X=q2X+k20成为下一个。表2更新情况所得增量例如q1/=0，q2/=0X=q1×q2X+k10×q2+k20X= 3X+ 1，X=12X+ 6X= 4X+ 2 、q1=0，q2/=0X=k10×q2+k20×X= 1X= 6X= 4X+ 2、q1/=0，q2=0X=k20X= 4X+ 2X= 1X= 1* 当这个X值沿着路径传播时，如果它导致退出循环，则循环是有界的，否则循环可能永远不会终止。为了扩大oRange的应用范围，协方差系数q和k不仅是单个值，而且还可以是被标记为SET（q1，q2）3的集合，其中q1，q2是单个值。为了将这种表示应用于我们的算术-几何3oRange将集合限制为两个值，以避免复杂性爆炸。更大的集合被抽象为T。M. De Pastel等人/理论计算机科学电子笔记289（2012）4147系列，我们重新定义运算符（+，×.. .）对于表3中的SET，其中q1、q2是单个值。表3顺序运算符· ∈ {×，+}Q2SET（ f3，f4）年q1q1· q2SET，q1·f3，，q1·f4你好，SET（ f1，f2）SET，q2·f1，，q2·f2f1·f3，f1·f4，敏，设置为：f2· f3，f2· f4，最大值，f1·f3，f1·f4，最大值f2·f3，f2·f43.3.2连接J的增量求值在X中有两个表达式的情况下：连接的每一部分都有一个表达式，我们设置X=q1X+k10和X=q2X+k20作为两个要连接的X结果增量取决于四个下一个有序的情况，否则它是unfined（T）。joinJ使用表4中定义的compose操作。(i) 如果q1= 0并且如果这个X赋值是导致退出循环的赋值，则X=q2X+k20是默认增量。当执行if的第一个分支时，X的常数值给出循环条件在下一次迭代时为假，因此当总是执行第二个分支时，获得循环的最大迭代次数。或者循环条件为真，所以循环可能永远不会终止（分别为）。如果q2= 0是最后一次迭代的情况，则X=q1X+k10），否则它是unfined。(ii) 如果q1=q2= 1，那么它是一个经典的算术形式：如果k10×k20>0，则X的赋值结果是X=X+compose（k10，k20），否则它是unfined。(iii) 如果k10=k20= 0，则它是一个经典的几何形式：如果（q11 andq2 1）或（q1>1 andq2> 1），则X的赋值结果是X=X×compose（q1，q2），否则它是unfined的。<<(iv) 否则它是算术-几何形式，得到的增量是：如果（q11和q21和k100和k200）或（q1>1和q2>1和<<<0和k20>0）则级数有界于X=X×compose（q1，q2）+compose（k10，k20）否则为unfined。表4组成组成Q2SET（ f3，f4）年q1ifq1=q2thenq2elseSET（q1，q2）如果q1min（f3，f4）SET（q1，max（f3，f4））ifq1>max（f3，f4）SET（min（f3，f4），q1）elseSET（f3，f4）你好，SET（ f1，f2）ifq2min（f1，f2）SET（q2，max（f1，f2））ifq2>max（f1，f2）SET（min（f1，f2），q2）elseSET（f1，f2）f1，f3，f1，f4，敏，SETf2，f3，f2，f4，最大值，f1，f3，f1，f4，最大值f2，f3，f2，f448M. De Pastel等人/理论计算机科学电子笔记289（2012）41KK我们在示例5中应用增量求值。 当compare（）== 0时，X=i−1−i = 1，测试00）j=（i+j）/2-1;elsei=（i+j）/2 + 1;}}3.4算术几何形式我们考虑严格的递减或递增形式。其他的形式是不确定的。经典的算术或几何形式在这里不考虑（以前的情况）。我们想用数学结果把它转换成几何形式。为了做到这一点，我们用新的级数V代替X级数，其中Vn=Xn+c，c= −k10/（1−q1）。通过引入V赋值代替X赋值并根据V变量改变条件来如果这是不可能的（因为SET），有时我们可以近似形式X=q1X+k10通过边界算术（见下一个有序公式a）或几何级数。(i) 如果lower（q1）= 1，则如果lower（k10）> 0。0则X=X+k10 else unfined.Ex. X=X×SET（2，1）+1则有界X=X+1(ii) 如果upper（q1）= 1，则如果upper（k10）= <0。0则X=X+k10 else unfined.Ex. X=X×SET（1/ 2， 1）−1则有界X=X− 1(iii) 如果q1>1，则(a) 如果X >0，则X=q1X(b) 如果X0，则与前面的情况相同，循环边界为+1，因为如果X = 0，当k10为正时，循环也会增加(c) 否则未确定(iv) 如果00，则X=q1X(b) 如果X0，则与前面的情况相同，循环边界为+1，因为如果X = 0，当k10为负时，循环也会减少(c) 否则未确定定义：设q1∈C，q2∈C。 设lower（q1）（相应地lower（q2））=(i) 如果q1∈R，则如果q1(ii) 如果q1=SET（f1，f2），则min（f1，f2）（分别为max（f1，f2））M. De Pastel等人/理论计算机科学电子笔记289（2012）4149我Ji+ 1

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