一句话:用分离逻辑静态推理程序片段语义效果,无需测试用例即可修复指针安全缺陷并验证补丁正确性。
静态分析工具已能有效发现真实代码中的缺陷,但自动程序修复(APR)多依赖测试用例,难以适用于新发现或难以确定性测试的缺陷(如内存泄漏),且满足测试套件的补丁质量难以保证。本文提出一种基于分离逻辑的静态 APR 技术:对已有程序片段的语义效果进行推理,针对一般指针安全性质(资源泄漏、内存泄漏、空指针解引用)定位并修复故障;该过程自动把识别出的代码片段转换为源码级补丁,并针对所报告的缺陷验证补丁正确性。作者开展了迄今规模最大的、自动修复真实代码中未被发现缺陷的研究,在 11 个真实项目中正确修复了 55 个 bug,其中 11 个为先前未被发现的 bug。
Static analysis tools have demonstrated effectiveness at finding bugs in real world code. Such tools are increasingly widely adopted to improve software quality in practice. Automated Program Repair (APR) has the potential to further cut down on the cost of improving software quality. However, there is a disconnect between these effective bug-finding tools and APR. Recent advances in APR rely on test cases, making them inapplicable to newly discovered bugs or bugs difficult to test for deterministically (like memory leaks). Additionally, the quality of patches generated to satisfy a test suite is a key challenge. We address these challenges by adapting advances in practical static analysis and verification techniques to enable a new technique that finds and then accurately fixes real bugs without test cases. We present a new automated program repair technique using Separation Logic. At a high-level, our technique reasons over semantic effects of existing program fragments to fix faults related to general pointer safety properties: resource leaks, memory leaks, and null dereferences. The procedure automatically translates identified fragments into source-level patches, and verifies patch correctness with respect to reported faults. In this work we conduct the largest study of automatically fixing undiscovered bugs in real-world code to date. We demonstrate our approach by correctly fixing 55 bugs, including 11 previously undiscovered bugs, in 11 real-world projects.