Towards Developing Effective Oracles to Reduce Patch Overfitting in Automated Program Repair

Patch overfitting is a well-known open challenge for automated program repair (APR), which results from having insufficient or incomplete specifications to validate the generated patches. We argue that part of the patch overfitting challenge is caused by not properly taking termination issues into account during patch validation. As such, our goal here is to improve the APR process by proposing a new approach that is dedicated to more complete patch correctness validation for APR. The paper is divided into two parts: In the first part, we study the correlation between the automated program repair problem and the program termination problem, demonstrating how a variety of program defects (e.g., violation of liveness properties, which causes the program to run indefinitely, and memory safety properties, which lead the program to crash) can be handled by fixing the termination of the program. In the second part, we present a novel patch validation approach that extends the standard test-based validation strategy by verifying two additional oracles: (i) oracle Oeb, which is an assertion-based oracle, obtained from developer-written bug reports and used to check the absence of erroneous behavior associated with the analyzed bug, and (ii) oracle <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\mathcal{O}_{halt}$</tex>, which is a halting oracle used to check the normal halting of the patched program. We demonstrate how to validate oracles <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$:\mathcal{O}_{eb}$</tex> and <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\mathcal{O}_{halt}$</tex> using contemporary termination provers and program verifiers. We also demonstrate how to effectively use the new validation oracles while taking into account the type of bug being repaired and the structure of the defected program.