基于后置条件的循环不变式自动生成方法

摘要

本发明公开了一种基于后置条件自动生成循环不变式的方法。首先依据循环语句的后置条件构造初始候选不变式，设计一个支持单层循环和双层循环的验证器，以验证循环不变式的有效性。然后运行程序生成高质量的样本数据集，利用循环程序的霍尔逻辑关系标注样本数据，采用KSVM方法学习不变式分类器。最后验证学习到的不变式分类器是否有效，若有效则表示生成的不变式分类器即为获得的循环不变式，否则迭代执行样本数据采用核支持向量机分类器学习，以获得可验证的循环不变式。本发明利用循环后置条件构造初始候选不变式，并在依据初始循环不变式构造的SVM分类器边界上选择分类样本，大大缩短了循环不变式生成时间，提高了可验证循环不变式的成功生成率。

说明书

技术领域

本发明属于软件工程、程序分析、软件安全和形式化验证技术领域，涉及一种循环不变式自动生成方法。

背景技术

循环不变式是程序在每次循环执行之前和循环结束时都应保持的性质，撰写一个程序的循环不变式可以帮助程序员深入理解程序的语义，也可以在程序断点检测出程序是否出现不合法的行为，为程序验证提供重要的可靠依据。然而，手工撰写循环不变式是一个非常耗时且具有挑战性的工作。此外，在程序验证时，并非所有的循环不变式都是可验证的(例如永真式)，只有能够通过程序验证的循环不变式才是一个可验证的不变式。因此，近几年，不少研究者们对自动生成循环不变式这一热点研究课题进行研究。目前，自动生成循环不变式的方法可分为静态方法和动态方法两大类。静态方法生成循环不变式时不需要运行循环程序，直接通过静态分析方法得到循环不变式，但该方法非常耗时且所得到的循环不变式的形式通常比较简单。动态方法则是通过执行循环程序计算循环不变式，可生成较形式复杂的循环不变式(例如，多项式循环不变式)，但因其与程序执行路径的覆盖率相关，容易生成一些假的循环不变式或冗余的不变式。为此，采用动态方法自动生成可验证的循环不变式问题，备受研究者的关注。目前，采用机器学习方法自动生成循环不变式的相关研究取得了一些研究成果，但大部分方法都基于随机生成的样本数据进行线性划分，容易出现因线性不可分的情况而导致无法生成循环不变式，也会因样本数据的随机性导致很难逼近循环不变式而导致生成循环不变式耗时较长。此外，目前循环不变式的自动生成主要停留在单层循环的程序结构，对嵌套循环的不变式自动生成研究很少。

发明内容

本发明所要解决的问题是为可执行的循环程序提供一种基于后置条件的自动循环不变式生成方法。本发明的目标：一是提高自动生成循环不变式的成功率，解决克服使用机器学习分类随机样本数据时，生成循环不变式成功率低的问题；二是缩短自动生成循环不变式所需要的时间，解决因样本数据的随机性导致很难逼近到有效循环不变式，从而使得自动生成循环不变式时间较长的问题；三是解决嵌套循环不变式的自动生成问题，以克服现有方法无法解决嵌套循环不变式自动生成的问题。

为此目的，本发明提供的基于后置条件自动生成循环不变式的方法，包括以下步骤，

步骤一，根据循环语句块构造初始候选不变式CanInv。在霍尔逻辑验证规则中，后置条件是循环不变式的弱化形式，该步骤借助这一逻辑关系，依据循环语句块的后置条件构造候选不变式CanInv。

步骤二，构造一个不变式验证器以验证候选不变式CanInv是否是有效的。若CanInv能通过程序验证，则该程序的可验证的循环不变式Inv已生成，即Inv＝CanInv。若CanInv不能通过验证，则得到反例数据，将其加入样本数据集，并执行步骤三。

步骤三，为更新步骤二中不能通过验证的候选循环不变式CanInv，生成样本数据集SD。

步骤四，标注步骤三中所生成的样本数据集SD，利用核支持向量机KSVM(KernelSupport Vector Machine)方法对这些标注过的样本数据集SD学习分类器；

步骤五，利用步骤四所生成的分类器更新候选不变式CanInv。若更新后的候选循环不变式CanInv无法通过验证，则执行步骤二进行下一轮循环，进行候选不变式CanInv的迭代更新。

上述步骤一中，所述的对循环语句块构造初始候选不变式CanInv，是将后置条件做等价线性变换或多项式不等式变换建立一个初始候选不变式。从逻辑学的角度来看，后置条件是循环不变式的弱化形式。这样做，对于循环不变式为后置条件的情况，可快速得到循环程序的有效循环不变式。否则，即对于循环不变式不是后置条件的情况，可利用机器学习方法快速得到其有效的循环不变式。

步骤二中，所述的构造一个循环不变式验证器验证候选不变式CanInv是否是可验证的，是指利用程序正确性验证逻辑规则，检验候选循环不变式是否是一个可验证的不变式，确保循环不变式的正确性。构造的不变式验证器，既可以用来验证单层循环不变式的有效性，也可以用来验证嵌套循环不变式的有效性。

其中，单层循环的候选不变式验证是采用反证法进行验证，其验证规则如下：

嵌套循环的候选不变式验证是利用各层循环不变式的约束进行验证，以两层嵌套循环为例，其验证规则如下：

P→Inv， (1)

{Inv∧C}{Body1∧Inv

P

{Inv

其中，P

步骤二中，所述的若候选循环不变式不能通过验证，则得到反例数据，是指利用可满足性理论的求解技术计算出不能通过有效性验证的循环不变式的反例数据，并采集这些反列数据作为分类样本数据，作为下一轮更新候选循环不变式的依据。

步骤三中，所述的生成样本数据集SD，包括(1)在步骤二中生成的候选不变式的边界上选取的样本数据；(2)依据循环前置条件P生成满足P和不满足P的样本数据，以及将满足P的样本数据作为循环输入，运行循环语句所得到的新样本数据；(3)步骤二中所生成的反例数据。这样，采集的样本数据集SD既包含正例样本数据，又包含反例样本数据，可提高数据样本的分类结果的有效性，即获得有效的候选循环不变式。

步骤四中，所述标注所生成的样本数据集SD，是指依据程序验证规则中程序的前置条件、后置条件和循环体，将步骤三所生成的数据集SD标注为三类：正样本数据、反例样本数据和不确定的样本数据。

步骤四中，所述的核支持向量机KSVM方法是一种支持径向基核函数、线性核函数、高斯函数等核函数的多核分类算法，以解决复杂数据样本的分类问题，从而获得形式多样的候选循环不变式，如多项式形式的循环不变式。

步骤五中，所述的利用步骤四所生成的KSVM分类器更新候选不变式CanInv，是将步骤四中所学习到的KSVM分类器作为新的候选不变式，并继续返回步骤二中验证其有效性，以判断该候选不变式是否为可验证的循环不变式，从而决定是否需要进行下一轮求解。

与现有技术相比，本发明的有益效果：

1.本发明提供的基于后置条件的自动生成循环不变式方法，依据后置条件与循环不变式的逻辑推理关系，将后置条件进行等价变换构造初始候选不变式，能直接获得有效的循环不变式或快速逼近循环不变式，大大缩短了循环不变式的自动生成时间。

2.当初始候选不变式不是可验证的循环不变式时，本发明在初始候选不变式所构建的分类器分界边界上选择样本数据，以提高样本数据集的质量，对复杂的非决定性循环程序能提高其循环不变式生成的成功率。

3.本发明解决了嵌套循环的不变式自动生成问题，为嵌套循环不变式的自动生成提供了一种有效的方法。

附图说明

图1为本发明所述基于机器学习生成循环不变式的流程图。

具体实施方式

下面结合附图对本发明进行详细说明。

本发明提出一种基于后置条件自动生成可验证的循环不变式的方法，主要目的是：(1)自动生成可验证的、形式丰富的循环不变式；(2)缩短循环不变式的自动生成时间，提高自动生成循环不变式的成功率；(3)解决单层循环和嵌套循环的不变式自动生成问题。

本发明所述基于后置条件自动生成循环不变式的过程如图1所示，其具体实施过程如下：

第一步，利用生成的循环语句的后置条件，和其与循环不变式的逻辑推理关系，构造循环语句块的初始候选不变式CanInv。

第二步，构造一个不变式验证器，验证候选不变式CanInv是否是可验证的。该验证器既可以验证单层循环语句，也可以验证嵌套循环语句。验证过程是首先构造验证规则，然后将待验证程序和验证规则输入到SMT(Satisfiability modulo theories，可满足性模理论)求解器中自动完成。其中，对单层循环的候选不变式的验证是采用反证法进行，具体验证规则如下：

嵌套循环的候选不变式验证是利用各层循环不变式的约束进行验证，采用分层验证方法进行实现，以两层嵌套循环为例，验证规则如下：

P→Inv， (4)

{Inv∧C}{Body1∧Inv

P

{Inv

其中，P

第三步，生成的样本数据集SD由三种类型的数据构成：(1)在步骤二中生成的候选不变式的边界上选取的样本数据；(2)依据循环前置条件P生成满足P和不满足P的样本数据，以及将满足P的样本数据作为循环输入，运行循环语句所得到的新样本数据；(3)步骤二中所生成的反例数据。

第四步，标注样本数据集SD，利用核支持向量机KSVM(Kernel Support VectorMachine)算法对这些标注过的样本数据集SD进行分类，并以获得可用于更新候选循环不变式的分类器。

第五步，利用步骤四所生成的分类器更新候选不变式CanInv，并执行步骤二。

现对基于后置条件生成循环不变式所涉及的算法进行相应介绍。

循环不变式的自动生成算法

输入：循环前置条件P，循环条件C，循环体Body和循环后置条件Q

输出：循环不变式Inv

Step1:对后置条件做线性变换或多项式等价变换，构造初始候选不变式CanInv；

Step2:通过循环条件C和循环体Body，构造循环程序所涉及的变量集合V；

Step3:验证CanInv是否是可验证的。如果是可验证的，则跳转到Step5；如果不是可验证的，采集循环程序执行时所产生的反例数据，执行Step4；

Step4:更新候选不变式CanInv，具体操作如下：

1.将候选不变式CanInv作为KSVM分类器clf；

2.依据变量集合V和前置条件P生成满足P和不满足P的样本数据，将其加入到样本数据集SD中。

3.基于所生成的样本数据，再次执行循环程序，收集程序运行过程中所产生的样本数据，并将其加入到样本数据集SD中。

4.将Step3中采集的反例数据加入到样本数据集SD中；

5.在分类器clf的边界上选择样本数据，并将其加入到数据集SD中；

6.利用样本数据集SD学习新的KSVM分类器，并将学习到的分类器作为新的候选不变式CanInv，并跳转到Step3。

Step5:输出循环不变式Inv＝CanInv。

为了便于本领域的普通技术人员实施本发明，现对本发明的实施做如下说明。

使用本发明所提供的方法能够为包含循环语句的计算机程序(如C程序)自动生成有效的循环不变式，要求程序由前置条件、后置条件和循环语句组成。使用时，如果是带分支的循环程序，其生成循环不变式的自动生成过程是：首先，按照路径分析法将多分支循环分解为多条执行路径，然后针对每条执行路径按照上述使用核支持向量机的方法分别生成循环不变式，最后将所生成的循环不变式组成循环不变式的析取式，即可获得多分支循环程序的不变式。使用时，如果是嵌套循环，将内层循环语句块和外层循环语句块当作独立的循环语句块，首先按照单层循环的不变式生成方法生成外层循环的候选循环不变式CanInv，然后按照单层循环的不变式生成方法生成内层循环的循环不变式CanInv

以上所述实施方法表达了本发明的几种实施方式，其描述较为具体和详细，但并不能因此而理解为对本发明范围的限制。应当指出的是，对于本领域的普通技术人员来说，在不脱离本发明构思的前提下，还可以做出若干变形和改进，这些也属于本发明保护范围。