Synthesis of Rigorous Floating-Point Predicates

A floating-point predicate is a routine that returns a boolean value based on a result of a floating-point computation. For example, in computational geometry floating-point predicates determine whether 3 points are collinear or which side of a line a point lies on. Due to floating-point round-off errors, implementing such predicates correctly, while maintaining good performance, requires both domain knowledge and deep understanding of the floating-point standard. Hence, it is usually done by experts that carefully craft them by relying on the floating-point round-off error model and complex mathematical derivations. This paper presents our automatic floating-point predicates synthesis method. Given an input predicate specified over reals, our method synthesizes the corresponding rigorous floating-point predicate by automatically deriving the expression that calculates the round-off error-bound of the input computation. We minimize the number of operations in the error-bound calculation, which is critical to maintain good performance, by judiciously reusing intermediate results, applying absolute-value inequalities, adjusting polynomial coefficients, and performing meta-heuristic grouping. We implemented the method in a prototype tool FPSyn. We evaluated FPSyn on 8 floating-point predicates, and showed that it synthesizes predicates whose performance is on par with optimized manually crafted implementations, while they outperform the straightforward interval arithmetic implementations.