FpGuard: Static-Analysis Guided Domain Exclusions for Robust Floating-Point Error Analysis

Estimating worst-case rounding errors is a crucial step in floating-point program analysis and verification. Successful static analysis tools in this area are based on symbolic automatic differentiation (to compute the error expressions) followed by maximizing these error expressions on the input domain. Unfortunately, this process has not been robustly supported in existing state of the art tools like Satire which scales to millions of operators. The main problem these tools run into is singularities in the maximization phase as the error expressions tend to infinity. By employing floating-point program synthesis, we discover the extent of this defect in Satire and then resort to a series of techniques that "guard" the input domain through constraints that avoid the singularities. We conduct the first study of this problem in this domain, and propose a set of novel solutions that makes Satire more robust, with our techniques being general enough to be applicable to other similar tools in this area. The new tool FpGuard produces tighter bounds, fewer crashes, runs faster and provides domain constraints to avoid singularities.