完善Coccinelle的控制流功能及测试

发布时间：2020-07-04 14:09

【摘要】：随着代码规模的增大和系统复杂性的增加,软件开发者意识到依靠人工的方式去维护软件系统、排除系统错误已经变得非常困难。形式化方法由于其正确性高、可自动化的特点,已经开始被应用于大型复杂的软件系统中。模型检验作为一种广泛采用的形式化方法,建立在对系统模型的抽象和对性质规约验证的基础之上,利用算法对模型的性质进行验证;模型检验技术不仅适用于系统开发前的安全性和可靠性验证,也适用于系统后期的维护工作。Coccinelle作为基于模型检验技术的代码搜索和转化工具,主要用于解决系统API库接口变化引发的并行演变。它利用描述语言SmPL描述代码模式,还可以在代码中搜索软件错误和漏洞,提升代码质量。SmPL能够理解C程序中的控制逻辑,因此可以精确地在大规模的程序中搜索C语言的代码块。目前SmPL支持条件语句、循环语句等不同控制结构的模式描述,但是缺少了对do-while循环结构的支持,这会限制SmPL的表达能力,影响程序匹配的准确性。本文针对Coccinelle中缺少的do-while循环结构进行了建模和公式设计。我们通过对C语言代码中的do-while循环结构进行建模,抽象为具有通用性的控制流图。在SmPL中,需要将do-while循环的控制结构转为CTL公式;通过对do-while的语法定义的补充,完成从代码到AST,再到CTL公式的转换过程,从而拓展SmPL的表意能力,完善了Coccinelle的控制流功能。本文的成果主要包括:1.我们对拓展后的Coccinelle进行了测试,包含了功能测试和性能测试,测试结果显示拓展后的Coccinelle可以正确地解析包含复合控制结构和嵌套结构下的do-while循环。2.我们利用拓展后的Coccinelle对Linux内核中的代码模式进行了调研,统计了Linux内核中do-while结构的数量和代码分布情况。还成功地对现实中一个具体的内核问题进行了验证,结果说明本文成果兼具正确性和实用性。
【学位授予单位】：兰州大学
【学位级别】：硕士
【学位授予年份】：2019
【分类号】：TP311.52
【图文】：

运行流程,源代码,硕士学位论文,补丁

大学硕士学位论文完善 Coccinelle 的控制流功能的补丁进行修改。occinelle 的实现原理分析上一节中，我们介绍了如何使用 Coccinelle 去匹配和搜索源代码细分析 Coccinelle 实现这一过程的原理。Coccinelle 每次执行以规则为执行单位。每个规则将对一个或者多个 C 源代码文件进行明了 Coccinelle 转换引擎执行的主要步骤。

函数,公式,递归,运算符

图 2-5 函数 SAT，该函数还调用了特化函数pre 、pre 、S TEU和S TAF在这个算法中，SAT 函数接收模型和公式Φ作为参数，递归地遍历在模型中标记满足对应公式的状态节点。递归地遍历公式时，通常最底层是原子命题。根据 SAT 函数，当公式中只有原子命题的情况时，它会标命题成立的状态节点，返回该状态集合。这个状态集合将作为函数 SAT 结果，会上一层 SAT 函数中执行其他运算符的计算。最后状态集合之间结果会作为最终满足公式Φ的输出。在图 2-3 中，Φ中会出现不同的运算符，主要有三类处理方式：第一类是直接返回结果，例如 T，⊥以及原子命题。第二类是递归地进行处理，例如∧，∨和运算符。第三类是调用函数pre 、pre 、S TEU和S TAF进行处理。对于第二类和第三类情况，算法通常会对公式进行一次预处理，因为辑中，可以用、∨来表示所有逻辑运算符；而在时序逻辑中，可以用 EX、AF 来表示所有时序运算符。公式 2-2 中包含了运算符的转换关系。

【相似文献】