【作者】 张灵；

【导师】 万海；

【作者基本信息】 中山大学 ， 软件工程， 2012， 硕士

【摘要】 调试是发现和减少计算机程序或电子硬件中的错误或缺陷的有序过程。程序调试过程包括错误定位和代码修复两个阶段。近年来在代码修复方面提出了一些方法可以相对容易地发现错误缺陷的原因。现有代码修复主要有基于形式化规范和基于测试用例两种方式。但实际应用中很难直接对具有控制流结构的坃程序的复杂数据和控制关系进行推理。布尔程序是跟坃程序一样具有常规的控制流结构的命令式语言，它的所有变量只有布尔类型。布尔程序的特性使以其作为坃程序修复过程中间语言来实现代码修复是一个值得研究的方法，现有研究中对布尔程序进行修复方面尚未实现完全自动化修复。本文在对布尔程序进行修复的方法上根据前人工作作了进一步的研究和改进。本文利用控制流结构对代码进行模拟运行构建出到达错误状态的错误路径以得到布尔修复。在构建错误路径时加入了更多的测试用例，使得能够覆盖的错误路径范围增大，因此对错误路径分析后找到的布尔修复的准确性更高。本文提出布尔程序修复的逆向转换方法，通过将得到的布尔程序修复逆向转换回坃程序的表达式，可以实现坃程序的整个修复过程完全自动化。得到布尔程序修复公式之后，首先根据在坃程序转换为布尔程序的过程中的变量映射关系将其转换为坃程序的表达式。转换之后对表达式的可满足性进行判断，当其可满足的时候才是坃程序的正确修复，可满足性判断问题可以归约到坓坍坔（可满足性模理论）问题。接着针对转换后坃程序的正确修复进行公式化简，将析取范式的修复通过修复子式内以及修复子式之间的关系进行化简得到有效最简的坃程序语句。根据本文改进的修复方法和提出的逆向转换方法，设计并实现了一个布尔程序修复逆向转换工具，该工具输入已知错误位置的坃程序，将其转换为布尔程序进行修复，再把布尔程序的修复结果转换为坃程序的表达式，输出一个修复后坃程序。本文采用了坔坃坁坓测试集来验证工具的正确性及有效性，实验结果显示该工具能够找到正确的修复结果且经过转换化简的修复结果贴近原程序的语义。更多还原

【Abstract】 Debugging is a methodical process of finding and reducing the number of bugs, or defects, in a computer program or a piece of electronic hardware. The debugging process includes two phases of fault location and code repair. A num-ber of methods in code repair make it easy to find the reason of errors or defects in recent years. There are mainly two ways of code repair methods which are formal specification-based and test cases based. It is difficult to reasoning the complex data structure and control relation in C program with control flow struc-ture. Boolean program is command language with control flow structure the same as C program. All variables of it are Boolean type. The feature of Boolean pro-gram makes it a worthwhile method in code repair as intermediate language. The existing work has yet to achieve the aim of fully automated repair the Boolean program.This dissertation do a further research base on previous work about repair of Boolean program. In this paper, we use control flow structure to simulate pro-gram running then construct the error paths which reach the error states to get a Boolean repair. We add more than one test case while constructing the error paths to make sure all the paths could be found so that accuracy of the repair is higher.This paper propose a method which could convert Boolean program’s repair to C program’s repair automatically. After obtaining the Boolean program’s repair formula, firstly the formula will be converted to C program’s expression accord-ing the map relations between C variables and Boolean variables. Secondly we determine whether the expression is satisfied. It is the right repair of C program if it is satisfied. The satisfiability judgment can reduce to the SMT (Satisfiability Modulo Theories) problem. The third we simplify the C program’s expression which is a disjunction formula then get the simplest C program statement.This dissertation design and implement a Boolean program reverse conver-sion tool based on the method propose in this paper. Input a C program with a known error into the tool, the program will be converted to a Boolean program and be repaired. Then the Boolean program’s repair will be reverse convert to C program’s expression. The tool will output a repaired C program at last. We use TCAS test suit to verify the accuracy and validity of the tool. The experiment results show that our tool can find the right repair results which are close to the semantics of the original program after reverse conversion and simplification.更多还原