Oracle-free repair synthesis for floating-point programs
Daming Zou, GU Yu-chen, Yuanfeng Shi, MingZhe Wang, Yingfei Xiong, Zhendong Su · Proceedings of the ACM on Programming Languages · 2022
The floating-point representation provides widely-used data types (such as “float” and “double”) for modern numerical software. Numerical errors are inherent due to floating-point’s approximate nature, and pose an important, well-known challenge. It is nontrivial to fix/repair numerical code to reduce numerical errors — it requires eithernumerical expertise(for manual fixing) or high-precisionoracles(for automatic repair); both are difficult requirements. To tackle this challenge, this paper introduces aprincipled dynamic approachthat isfully automatedandoracle-freefor effectively repairing floating-point errors. The key of our approach is the novel notion ofmicro-structurethat characterizes structural patterns of floating-point errors. We leverage micro-structures’ statistical information on floating-point errors to effectively guide repair synthesis and validation. Compared with existing state-of-the-art repair approaches, our work is fully automatic and has the distinctive benefit of not relying on the difficult to obtain high-precision oracles. Evaluation results on 36 commonly-used numerical programs show that our approach is highly efficient and effective: (1) it is able to synthesize repairs instantaneously, and (2) versus the original programs, the repaired programs have orders of magnitude smaller floating-point errors, while having faster runtime performance.