Code Repair And Reverse Transformation Base On Boolean Program

Debugging is the process of finding the fault location in program and fixing it. In daily software development, this is a very critical process. The program debugging includes fault positioning and fixing. In the first step, we will locate the position of the specific fault. Then we fix it with some special methods. In re-cently years, for the code repairing problem, some scholars have proposed some automated code repairing methods. Andreas Griesmayer and some others pro-posed that fixing the faulty with a Boolean problem. Using predicate abstraction, we can map the infinite state system of C programs to a Boolean program finite state system. The predicate abstraction makes the programs size greatly reduced, and this is a great convenience for analyzing the reachability of the model’s dan-gerous state. According to this line of thinking, it was suggested that the control flow structure can be used for simulating the code’s running. It can build an error path in the Boolean program, which can get the repair of the Boolean pro-gram. Finally, we can get the repair of C program by using the repair of Boolean program and the relative mapping relations.Based on the methods mentioned above, we select Satabs to convert the C program to Boolean program. Through analyzing the principle of the counter-example guided abstraction refinement process, we simulate the error path again in C program to make sure it is also a specific path. And this also makes sure the correctness of the repairing result. When analyzing the method to get a repair for the program, we conclude that which kind of fault can be repaired with this method. Then we classify the different kind of fault and verify their repairable with some experiments.In addition, for the repair of the Boolean program results, if the program di-rectly on behalf of a Boolean variable represents C program expression meaning, can be considered the repair of the C program, but this is different from the minds of most people. This article first use SMT tool to judge the satisfiability of repair. The repair results can be expressed as a disjunctive normal form, each sub-type are conjunctive normal, the meaning of the proposition is the Boolean program’s variable represents the corresponding C program expressions. For disjunctive normal form, to judge each child can meet or not. Delete the ones which can’t meet. The use of linear programming methods can be used to remove the con-junct other formulas logical implication of the proposition, then get the effect of simplification.According to the method proposed in this paper, we designed an automat-ed C program repair process tools. In order to make the entire repair process be automated as much as possible, we use an existing fault localization method to determine the position of program errors. We use Satabs to convert C program to Boolean program. Using the TCAS test set to verify the repair of a particular type of error, the experimental results show that, after specify the type of error fixes inverse converted simplification, the repair results closer to the original program semantics.