Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
We propose a novel method to automatically repairing buggy heap-manipulating programs using constraint solving and deductive synthesis. Given an input program C and its formal specification in the form of a Hoare triple: {P} C {Q}, we use a separation-logic-based verifier to verify if program C is correct w.r.t. its specifications. If program C is found buggy, we then repair it in the following steps. First, we rely on the verification results to collect a list of suspicious statements of the buggy program. For each suspicious statement, we temporarily replace it with a template patch representing the desired statements. The template patch is also formally specified using a pair of unknown pre- and postcondition. Next, we use the verifier to analyze the temporarily patched program to collect constraints related to the pre- and postcondition of the template patch. Then, these constraints are solved by our constraint solving technique to discover the suitable specifications of the template patch. Subsequently, these specifications can be used to synthesize program statements of the template patch, consequently creating a candidate program. Finally, if the candidate program is validated, it is returned as the repaired program. We demonstrate the effectiveness of our approach by evaluating our implementation and a state-of-the-art approach on a benchmark of 231 buggy programs. The experiment results show that our tool successfully repairs 223 buggy programs and considerably outperforms the compared tool.
NEM is build on top of the HIP verification system and Songbird prover.
The details about the benchmark we use in our experiments is provided in Github.