一种对源代码形式化验证方法

摘要

本发明提供一种对源代码形式化验证方法，包括输入生成器、符号执行器、规约生成器、规约匹配器、形式化验证规约库、规约学习器、规约筛选器、自然语言转换器、代码验证器、验证报告生成器，所述输入生成器将源代码作为输入，生成多个将变量和函数参数值随机化的代码文件，所述符号执行器用于读取上述代码文件，解析出文件集合，其中每个文件包含单个函数的输入状态、执行函数及输出状态。本方案通过规约生成器，将源代码进行自动化处理后生成原始规约，并通过模型学习手段，利用规约学习器对规约进行修正和补充，流程高度自动化，有效降低了开发和验证人员手动撰写形式规约的门槛，减少了形式语言学习和实施的成本，提高验证自动化程度。

权利要求

1.一种对源代码形式化验证方法，其特征在于：包括输入生成器、符号执行器、规约生成器、规约匹配器、形式化验证规约库、规约学习器、规约筛选器、自然语言转换器、代码验证器、验证报告生成器，所述输入生成器将源代码作为输入，生成多个将变量和函数参数值随机化的代码文件；

所述符号执行器用于读取上述代码文件，解析出文件集合，其中每个文件包含单个函数的输入状态、执行函数及输出状态；

所述规约生成器用于读取上述文件集合，生成每个函数对应的原始形式化规约；

所述规约匹配器接受原始规约集合后，从所述形式化验证规约库中调用符合上文生成的原始规约的形式化验证规约，并通过规约匹配器生成名称、性质相近的规约集合，用以扩充原始规约集合；

所述规约学习器将上述扩充后的规约集合输入，利用模型学习算法对规约集进行调整筛选，并输出调整后的规约；

所述规约筛选器将需求文档、接口文档通过自然语言转换器转换为规范文档后，和上文生成的规约集合一起传输至规约筛选器中，筛选出每一条函数最终对应的规约；

所述代码验证器用于对所有的源代码及其形式化规约进行形式化验证，验证是否相符，并通过所述验证报告生成器生成验证报告。

2.根据权利要求1所述的一种对源代码形式化验证方法，其特征在于：所述输入生成器用于接收验证所述源代码，对所述源代码进行分解，生成多个代码函数文件，每个所述代码文件均为一组可读的计算机语言指令。

3.根据权利要求2所述的一种对源代码形式化验证方法，其特征在于：所述符号执行器用于接受生成的代码文件，将所述代码文件解析出代码函数的集合，单个集合包含某一函数的输入状态、执行函数、及输出状态，将集合以文件方式打包后传输至模拟学习器中。

4.根据权利要求1所述的一种对源代码形式化验证方法，其特征在于：所述规约生成器用于函数的预处理，生成待验证函数列表，并对列表中的每个函数进行函数规约初始化，生成原始规约。

5.根据权利要求1所述的一种对源代码形式化验证方法，其特征在于：所述形式化验证规约库基于检测的形式化规约的集合，包括不同语言文法规则的形式化描述。

6.根据权利要求1所述的一种对源代码形式化验证方法，其特征在于：所述规约匹配器用于将上一步生成的原始规约与形式化规约库中的规约进行匹配，并生成不同类型的符合规约集合。

7.根据权利要求1所述的一种对源代码形式化验证方法，其特征在于：所述规约学习器用于接受规约集合，通过规约集合准确可靠地学习源代码，并自动生成源代码中每个函数对应的原始形式化规约。

8.根据权利要求1所述的一种对源代码形式化验证方法，其特征在于：所述自然语言转换器用于接收需求文档、接口文档等，将需求文档、接口文档转化为使用形式语言描述的需求规范文档、接口规范文档，并将规范文档传输至规约筛选器中。

9.根据权利要求1所述的一种对源代码形式化验证方法，其特征在于：所述规约筛选器是用于筛选、判断每一条函数对应的规约，并将集合传输到代码验证器中。

10.根据权利要求9所述的一种对源代码形式化验证方法，其特征在于：所述代码验证器用于验证所有函数及对应的规约是否相符。

说明书

一种对源代码形式化验证方法

技术领域

[0001] 本发明涉及形式化验证技术领域，具体为一种对源代码形式化验证方法。

背景技术

[0002] 软件正确性保障方法有三种技术，分别为：软件测试、代码分析、形式化验证，目前最常用的为形式化验证。

[0003] 但形式化验证存在其学习成本较高的缺陷，对于每种编程语言都存在多种功能规约语言，导致功能规约的复用率低，即当一个新的软件中有类似功能的时候，无法直接使用之前写过的功能规约，也无法快速分析不同编程语言对于同一种实现的差别。

发明内容

[0004] （一）解决的技术问题

[0005] 针对现有技术的不足，本发明提供了一种对源代码形式化验证方法，解决了上述背景技术中提出的问题。

[0006] （二）技术方案

[0007] 为实现以上目的，本发明通过以下技术方案予以实现：一种对源代码形式化验证方法，包括输入生成器、符号执行器、规约生成器、规约匹配器、形式化验证规约库、规约学习器、规约筛选器、自然语言转换器、代码验证器、验证报告生成器，所述输入生成器将源代码作为输入，生成多个将变量和函数参数值随机化的代码文件，所述符号执行器用于读取上述代码文件，解析出文件集合，其中每个文件包含单个函数的输入状态、执行函数及输出状态，所述规约生成器用于读取上述文件集合，生成每个函数对应的原始形式化规约，所述规约匹配器接受原始规约集合后，从所述形式化验证规约库中调用符合上文生成的原始规约的形式化验证规约，并通过规约匹配器生成名称、性质相近的规约集合，用以扩充原始规约集合，所述规约学习器将上述扩充后的规约集合输入，利用模型学习算法对规约集进行调整筛选，并输出调整后的规约，所述规约筛选器将需求文档、接口文档通过自然语言转换器转换为规范文档后，和上文生成的规约集合一起传输至规约筛选器中，筛选出每一条函数最终对应的规约，所述代码验证器用于对所有的源代码及其形式化规约进行形式化验证，验证是否相符，并通过所述验证报告生成器生成验证报告。

[0008] 所述输入生成器用于接收验证所述源代码，对所述源代码进行分解，生成多个代码函数文件，每个所述代码文件均为一组可读的计算机语言指令。

[0009] 优选的，所述符号执行器用于接受生成的代码文件，将所述代码文件解析出代码函数的集合，单个集合包含某一函数的输入状态、执行函数、及输出状态，将集合以文件方式打包后传输至模拟学习器中。

[0010] 优选的，所述规约生成器用于函数的预处理，生成待验证函数列表，并对列表中的每个函数进行函数规约初始化，生成原始规约。

[0011] 优选的，所述形式化验证规约库基于检测的形式化规约的集合，包括不同语言文法规则的形式化描述。

[0012] 优选的，所述规约匹配器用于将上一步生成的原始规约与形式化规约库中的规约进行匹配，并生成不同类型的符合规约集合。

[0013] 优选的，所述规约学习器用于接受规约集合，通过规约集合准确可靠地学习源代码，并自动生成源代码中每个函数对应的原始形式化规约。

[0014] 优选的，所述自然语言转换器用于接收需求文档、接口文档等，将需求文档、接口文档转化为使用形式语言描述的需求规范文档、接口规范文档，并将规范文档传输至规约筛选器中。

[0015] 优选的，所述规约筛选器是用于筛选、判断每一条函数对应的规约，并将集合传输到代码验证器中。

[0016] 优选的，所述代码验证器用于验证所有函数及对应的规约是否相符。

[0017] （三）有益效果

[0018] 本发明提供了一种对源代码形式化验证方法。具备以下有益效果：

[0019] 1、本方案通过规约生成器，将源代码进行自动化处理后生成原始规约，并通过模型学习手段，利用规约学习器对规约进行修正和补充，流程高度自动化，有效降低了开发和验证人员手动撰写形式规约的门槛，减少了形式语言学习和实施的成本，提高验证自动化程度。

[0020] 2、本方案适用于多种编程语言，实现编程语言到形式化规约的转化，具有高度的普遍性。

附图说明

[0021] 图1为本发明中对源代码形式化验证方法的流程图；

[0022] 图2为规约学习器的学习流程框图。

具体实施方式

[0023] 本发明实施例提供一种对源代码形式化验证方法，如图1所示，包括输入生成器、符号执行器、规约生成器、规约匹配器、形式化验证规约库、规约学习器、规约筛选器、自然语言转换器、代码验证器、验证报告生成器，输入生成器将源代码作为输入，生成多个将变量和函数参数值随机化的代码文件，符号执行器用于读取上述代码文件，解析出文件集合，其中每个文件包含单个函数的输入状态、执行函数及输出状态，规约生成器用于读取上述文件集合，生成每个函数对应的原始形式化规约，规约匹配器接受原始规约集合后，从形式化验证规约库中调用符合上文生成的原始规约的形式化验证规约，并通过规约匹配器生成名称、性质相近的规约集合， 用以扩充原始规约集合，规约学习器将上述扩充后的规约集合输入，利用模型学习算法对规约集进行调整筛选，并输出调整后的规约，规约筛选器将需求文档、接口文档通过自然语言转换器转换为规范文档后，和上文生成的规约集合一起传输至规约筛选器中，筛选出每一条函数最终对应的规约，代码验证器用于对所有的源代码及其形式化规约进行形式化验证，验证是否相符，并通过验证报告生成器生成验证报告。

[0024] 输入生成器用于接收验证源代码，对源代码进行分解，生成多个代码函数文件，暨将每个函数转化为使多个仅执行该函数的一个程序入口函数的代码文件，并调整全局变量及输入参数类型，并将生成的代码文件传输至符号执行器中，每个代码文件均为一组可读的计算机语言指令。

[0025] 符号执行器用于接受生成的代码文件，将代码文件解析出代码函数的集合，单个集合包含某一函数的输入状态、执行函数、及输出状态，将集合以文件方式打包后传输至模拟学习器中。

[0026] 规约生成器用于函数的预处理，生成待验证函数列表，并对列表中的每个函数进行函数规约初始化，生成原始规约。

[0027] 形式化验证规约库基于检测的形式化规约的集合，包括不同语言文法规则的形式化描述。

[0028] 规约匹配器用于将上一步生成的原始规约与形式化规约库中的规约进行匹配，并生成不同类型的符合规约集合。

[0029] 规约学习器用于接受规约集合，通过规约集合准确可靠地学习源代码，并自动生成源代码中每个函数对应的原始形式化规约。

[0030] 自然语言转换器用于接收需求文档、接口文档等，将需求文档、接口文档转化为使用形式语言描述的需求规范文档、接口规范文档，并将规范文档传输至规约筛选器中。

[0031] 规约筛选器是用于筛选、判断每一条函数对应的规约，并将集合传输到代码验证器中。

[0032] 代码验证器用于验证所有函数及对应的规约是否相符。

[0033] 通过建立形式化规则模型库，对源代码规约进行自动初始化匹配，并结合自然/半形式的需求和设计文档，校准形式规约，而后由形式化验证器对规约进行自动验证和报告生成。本发明通过下述技术方案实现：

[0034] 第一步，读取待验证的源代码文件，放入输入生成器中。源代码代码文件中的每个函数会被生成多个仅执行该函数的代码文件，生成后的文件会调整该代码文件中原先的全局变量为随机值，以及该函数的输入参数类型的随机值。

[0035] 具体来说，生成器接受源代码，采用BNF范式和其拓展EBNF方式描述编程语言语法，并且转化为语法树。根据语法树找到所有的函数定义语句，确定函数的名称、返回值类型、参数类型，以及调用该函数所需要的其他信息（例如：类名，包名等）。将源代码文件中的程序入口调用的代码块删除，替换为调用该函数的代码块。

[0036] 其中代码块应包含信息如下：返回变量与参数的构造、仅需初始化的返回变量、随机赋值的参数。其中函数调用指函数调用的返回值给到之前构造的返回变量中。

[0037] 第二步，将上文输出的代码文件放入符号执行器中，解析出源码函数文件集合（包含函数的输入状态、执行函数及输出状态）。符号执行即虚拟的执行，通过提前定义好的源代码语义，在抽象的程序状态中执行。程序的执行就是该程序状态变换的过程。其中，单个集合包的内容为：执行文件、执行函数标识（通常为函数名+执行文件的代码行数）、执行函数前的程序状态、执行函数后的程序状态（或在存在循环时，推导出的循环不变式）。

[0038] 第三步，将上述函数文件集合置入规约生成器中，生成源码中每个函数对应的原始形式化规约，包含前置条件和后置条件两部分。前后置条件的结构相近，均应该包含变元和变元的约束条件。变元的约束条件应该是一个返回值为布尔类型的一个表达式。

[0039] 规约生成器对源程序（函数集合）进行程序的预处理，获得不包含预处理指令内容的源程序，生成待验证函数列表，对上述列表中的每个函数进行下面相同的操作：

[0040] 1、函数规约初始化。

[0041] 1.获取该函数调用的全部全局变量：

[0042] a.获取源程序中的所有全局变量；

[0043] b.提取源程序中目标函数所有表达式中的操作变量；

[0044] c.删除不作为操作变量的全局变量，保存为该函数调用的全局变量列表。

[0045] 2.获取前置条件的变元：设置“目标函数参数”以及“该函数调用的全局变量”为变元。

[0046] 3.设置初始前置条件：

[0047] a.源程序的每个变元都应该存在一个类型；若是类型不确定，则通过调用该变元的表达式操作中其他的表达式确定类型，以及该函数被调处的变元类型；

[0048] b.每个变元都应该被约束为“未确定的类型值”且“被允许的类型值” 。

[0049] 4.获取后置条件的变元：设置“目标函数返回参数”以及“该函数调用的全局变量”为变元。

[0050] 5.设置初始后置条件：

[0051] a.源程序的每个变元都应该存在一个类型；若是类型不确定，则通过调用该变元的表达式操作中其他的表达式确定类型，以及该函数被调用处的变元类型；

[0052] b.每个变元都应该被约束为未确定及被允许的类型值,且之前符号执行的结果设置为「输入状态」蕴含「输出状态」。

[0053] 第四步，读取函数集合的原始规约集合，并从形式化验证规约库中调用符合上文生成的原始规约的形式化验证规约，并通过规约匹配器，在原始规约的基础上，通过形式化验证规约库，扩展生成文本匹配度高、存在前后置条件交集的规约集合。

[0054] 规约匹配器将首先按照函数名称，在规约库中匹配含义相近的规约名称；然后通过集合操作，找到名称相近规约（多个）、原始规约在前置条件和后置条件存在交集的规约。最后，将综合匹配度最高的规约集合和原始规约进行组合，进行最终输出。

[0055] 第五步，将上述中扩展后的规约集合、原始规约输入至规约学习器中，进行函数规约学习，并输出函数的规约。

[0056] 函数规约学习只学习不调用无功能规约函数的函数。如果一个函数内部有调用的函数还没有功能规约，则先学习该调用函数的功能规约。

[0057] 学习的目标是获得该函数的可能的函数规约。

[0058] 在一个实施例中，以下将学习器中的提问模块以学生指代，回答模块以老师指代，学习的过程是通过学生不断的询问和老师每次的回答，逐渐获得个更加准确的前置条件和后置条件的过程。

[0059] 如图2所示，具体步骤为：

[0060] 1.学生总是拿着前置条件和后置条件组合成函数规约去询问老师是否是这个函数的函数规约。

[0061] 2.老师通过程序验证器验证该规约，程序验证器是输入验证规约和源代码可以返回验证结果的装置，如果验证规约与源代码实现相符则返回真，若验证规约语言与源代码实现不相符则返回假：

[0062] a.若不相符，则返回反例。学生根据该反例删除掉该前后置条件中的这种情况，若是多次遇到错误，则构造包含这几次反例最小的集合进行删除，尝试多次后若是仍不相符，则返回到最近的相符的前置条件和后置条件。

[0063] b.若相符，则根据源代码中使用该函数的操作返回一个例子。学生根据该例子增加该前后置条件中的这种情况，若是多次遇到正确，则构造包含这几次例子最小的集合进增加。

[0064] 通过此种学习方式反复学习，直至源代码中每个函数生成对应的原始形式化规约集合。

[0065] 第六步，将需求文档、接口文档通过自然语言转换器转换为规范文档后，和上文生成的规约集合一起传输至规约筛选器中，筛选出每一条函数对应的规约。

[0066] 作为进入规约筛选阶段的另一个前置步骤，自然语言转换器从需求文档中提取需求名称，找到和原始规约名称含义相近的需求名称。对该需求名称对应的需求描述进行自然语言解析，将名词转化为自由变元，动词转化为函数。生成相应的ivl（如Boogie），随后将交集规约作为前后置条件进行验证。若通过则标志为可能需求，若没通过标记为小概率需求。接口文档也是相同的操作，不过是提取接口名称。在规约字段中增加需求名称和接口名称。

[0067] 第七步，选择所有的源代码及其形式化规约置入代码验证器中进行形式化验证，验证所有函数及对应的规约是否相符。

[0068] 第八步，验证报告生成器对验证结果进项报告，若相符，通过验证报告器生成验证报告。

[0069] 尽管已经示出和描述了本发明的实施例，对于本领域的普通技术人员而言，可以理解在不脱离本发明的原理和精神的情况下可以对这些实施例进行多种变化、修改、替换和变型，本发明的范围由所附权利要求及其等同物限定。