PaperlayerView exact revision on arXiv

Source-linked AI summary

FPScan: An Automated Constraint-Based Analyzer for Floating-Point Anomaly Detection

Julien Bortolussi, Dorra Ben Khalifa, Pierre-Loïc Garoche

arXiv:2609.07492v1cs.SEcs.NAmath.NA

TL;DR

Absorption and catastrophic cancellation can amplify rounding errors, yet relatively few tools explicitly address these pitfalls. FPScan combines static range analysis, order-of-magnitude constraints, and SMT solving to detect them. On FPBench, it proves 72% of cases impossible with 8% false positives, outperforming bitblasting and comparing favorably with FPChecker.

  • Problem

    Relatively little work has investigated systematic detection or exploitation of numerical pitfalls such as absorption and catastrophic cancellation, which can amplify rounding errors.

    Source: §I · p. 1

  • Method

    FPScan uses abstract interpretation to infer variable ranges and orders of magnitude, generates constraints for numerical pitfalls, and checks them with an SMT solver.

    Source: §I · p. 1

  • Results

    FPScan proves 72% of cases impossible with 8% false positives, outperforming bitblasting and comparing favorably with FPChecker.

    Source: §VI · p. 8

  • Takeaways & Limitations

    The approach can determine that a potential pitfall is impossible by checking whether its constraint is unsatisfiable.

    Source: C. Approximated Constraint-based… · p. 3, §VI · p. 8

Abstract

from arXiv · show

Writing error-free floating-point programs is a challenging task, especially for programmers who lack a strong background in numerical analysis and rounding-error propagation. State-of-the-art techniques typically aim to bound such errors using static or dynamic analysis. However, only a few tools explicitly address critical floating-point pitfalls such as absorption and catastrophic cancellation. These anomalies represent situations in which rounding errors are significantly amplified, causing the semantics of the finite-precision computation to deviate substantially from the real-number semantics. In this article, we present FPScan, a novel tool to formally define and detect both catastrophic cancellation and absorption in floating-point programs. Our approach starts with a custom static analyzer based on abstract interpretation to infer the order of magnitude of all program variables. This magnitude information is then used to build a set of first-order constraints that model error propagation and numerical precision within the program. Finally, we employ an off-the-shelf SMT solver to determine whether the program exhibits any of these critical numerical pitfalls. Experiments were conducted on FPBench, a well-known benchmark suite of floating-point programs, to evaluate the effectiveness of our tool. We also present a comparison with state-of-the-art tools regarding soundness and analysis time.

I. INTRODUCTION

FPScan targets absorption and catastrophic cancellation, floating-point pitfalls that amplify rounding errors and are difficult for developers to diagnose. It combines static analysis with constraint solving to detect these pitfalls, against a background of finite-precision representation and rounding.

I. INTRODUCTION

  • Relatively little work has examined systematic use of numerical pitfalls to help developers identify problematic computations or generate more accurate expressions.Developers without specialized numerical-analysis training often resort to inefficient, unreliable trial and error.Source: §I · p. 1
  • FPScan combines interval range analysis, order-of-magnitude reasoning, and SMT constraints to detect absorption and catastrophic cancellation; its evaluation includes FPBench comparisons with FPChecker and bitblasting.The article presents this as an efficient constraint-based method, including denormalized numbers.Source: §I · p. 1

II. BACKGROUND ON FLOATING-POINT ARITHMETIC

  • The introduction frames floating-point arithmetic as a standard way to approximate real-number computations, while the background section reviews its fundamentals and sources of numerical error.Finite, nonuniform representation is one reason some operations introduce significant numerical errors.Source: §II · p. 1, §I · p. 1

A. Floating-Point Numbers

  • Floating-point numbers use finite significands and bounded exponents; IEEE 754 formats differ in precision and exponent range, and normalization maximizes the significand.Numbers without a leading significand bit of one are denormalized.Source: A. Floating-Point Numbers · p. 2

B. Absorption and Catastrophic Cancellation in Floating-point Arithmetic

1) Absorption:

  • Adding a much larger number to a smaller one can make the smaller contribution similar to a rounding error, losing its information.In the binary32 example, adding 1 to 2^26 yields 2^26.Source: 1) Absorption · p. 2

2) Catastrophic Cancellation:

  • Subtracting nearby numbers with coincident leading bits can leave a much smaller result, magnifying errors in either operand.In the example, absorption makes z equal to 2^26, so subtracting x yields 0 instead of 1 and reveals the earlier pitfall.Source: 2) Catastrophic Cancellation · p. 2

III. CONSTRAINT-BASED DETECTION OF FLOATING-POINT ABSORPTION AND CATASTROPHIC CANCELLATION

FPScan analyzes a program’s ranges, derives constraints for possible floating-point pitfalls, and checks their feasibility with an SMT solver. It uses integer order-of-magnitude quantities to represent values, precision, and rounding error.

III. CONSTRAINT-BASED DETECTION OF FLOATING-POINT ABSORPTION AND CATASTROPHIC CANCELLATION

  • FPScan infers bounds on variables and intermediate expressions, generates constraints for absorption and catastrophic cancellation, and checks each pitfall’s feasibility independently with an SMT solver.The analysis abstracts values and errors by their orders of magnitude, yielding integer constraints that are faster to solve.Source: §III · p. 2

A. Quantifying Magnitude, Precision, and Error

  • The section introduces ufp, ulp, and nsb to characterize a floating-point number’s magnitude, precision, and associated error.The number of significant bits can be negative when rounding error exceeds the value’s magnitude.Source: A. Quantifying Magnitude, Precision,… · p. 3
  • Ufp represents a number’s order of magnitude, with a special value specified for zero.The definition uses the minimum integer i such that 2^(i+1) exceeds the absolute value, and assigns emin − p + 1 when the value is zero.Source: A. Quantifying Magnitude, Precision,… · p. 3
  • Ulp denotes the exponent of the least significant bit and is defined to accommodate denormalized numbers.Its definition takes the maximum of ufp(x) − p + 1 and emin − p + 1.Source: A. Quantifying Magnitude, Precision,… · p. 3
  • Nsb counts bits whose weight exceeds the rounding error, so it can be negative when that error exceeds the value’s magnitude.The section introduces nsb as one of the quantities characterizing magnitude, precision, and associated error.Source: A. Quantifying Magnitude, Precision,… · p. 3

B. Concrete Program Semantics

The section defines concrete execution semantics for FPScan’s supported language, then abstracts program behavior with constraints over floating-point magnitudes and error. Interval bounds and sound over-approximation support this analysis, with bounded loops and shared real/FP control flow as scope limits.

B. Concrete Program Semantics

  • Loop conditions are unrolled only to a user-specified bound, and the analysis assumes real and floating-point executions take the same conditional path.Unbounded loops and unstable tests are left for future work.Source: B. Concrete Program Semantics · p. 3
  • FPScan’s concrete semantics maps machine states through statements, while its collecting semantics returns reachable states from a set of input states.The parser accepts arithmetic, mathematical functions, conditionals, and loops; loops must be bounded and are unrolled into nested conditionals.Source: B. Concrete Program Semantics · p. 3

1) Range analysis:

  • Interval analysis rejects programs that may overflow, produce NaNs, or divide by zero, then uses inferred intervals to bound variables’ ufp values.Those bounds feed the constraints used in the subsequent analysis.Source: 1) Range analysis · p. 4

2) Constraint generation:

  • Statement constraints are expressed using ufp, ulp, and nsb, so they omit operand signs and treat addition and subtraction uniformly.The constraint definitions cover arithmetic, functions, assignments, sequences, and branches.Source: 2) Constraint generation · p. 4
  • The abstract semantics is a sound over-approximation of concrete execution and must not omit any reachable machine state.The soundness argument uses structural induction over program constructs.Source: C. Approximated Constraint-based… · p. 3, 2) Constraint generation · p. 4
  • For addition, the abstract error bound combines operand-error bounds and the operation’s rounding error using the triangle inequality.The rounding-error term is bounded using ulp of the computed result.Source: 2) Constraint generation · p. 4

D. A Taxonomy of Floating-Point Pitfalls

The taxonomy formalizes absorption and catastrophic cancellation as conditions on addition and subtraction. It also notes a soundness boundary: the non-relational magnitude constraints can report spurious absorption in some cases.

D. A Taxonomy of Floating-Point Pitfalls

E. Detection of Floating-Point Pitfalls Using an SMT solver

FPScan encodes reachable machine states and pitfall conditions as constraints, then checks each potential pitfall independently with an SMT solver. Satisfiable constraints produce warnings, while unsatisfiable ones prove the corresponding case impossible.

E. Detection of Floating-Point Pitfalls Using an SMT solver

  • Each constraint combines a characterization of reachable machine states with conditions identifying states that exhibit a specific pitfall.FPScan generates one constraint for each pitfall that may occur in the program.Source: E. Detection of Floating-Point… · p. 5
  • In the example, Z3 proves absorption of x by y on Line 1 impossible, but reports a warning for absorption of y by x because its constraint is satisfiable.FPScan analyzes each case independently and applies the same procedure to catastrophic cancellation and Line 2.Source: E. Detection of Floating-Point… · p. 5
  • The example report contains three warnings across Lines 1 and 2, while the other three potential pitfalls are proven impossible.It is generated in less than 0.15 seconds; catastrophic cancellation cannot occur on Line 1.Source: E. Detection of Floating-Point… · p. 5, Figure 5 · p. 5
  • A Line 2 absorption report is spurious because non-relational constraints for ufp can admit states implying z is larger than x, which is impossible.The passage attributes this to the analysis being sound but incomplete.Source: E. Detection of Floating-Point… · p. 5

IV. EXPERIMENTAL EVALUATION

The evaluation tests FPScan on an FPBench subset for detection accuracy and runtime relative to bitblasting and FPChecker. FPScan proves many potential pitfalls impossible without false negatives, while FPChecker’s sampling misses cancellations on some programs.

IV. EXPERIMENTAL EVALUATION

  • The evaluation asks how well ufp, ulp, and nsb abstraction detects pitfalls and how FPScan’s constraint-solving runtime compares with existing tools.The research questions are evaluated on the FPBench benchmark suite.Source: §IV · p. 5

B. RQ1: Soundness Validation and Completeness Evaluation.

  • For most programs, FPScan’s detected cancellations closely match all occurring cancellations; FPChecker misses cancellations on some programs due to its sampling strategy.Figure 6 separates FPScan’s detected and proven-impossible cancellations from FPChecker’s detected and missed occurring cancellations; robust cross-program sampling is left for future work.Source: Figure 6 · p. 6, B. RQ1: Soundness Validation and… · p. 6

A. Experimental Setup

  • The evaluation uses 58 of FPBench’s 130 binary32 programs with interval-based preconditions, of which 41 are compatible with bitblasting.Bitblasting supplies a sound and complete ground truth for decidable theories but is too computationally expensive for large-scale practical use; its cancellation criterion is stricter than FPScan’s and may underestimate FPScan completeness. FPChecker is sampled at 1000 points per input interval and is compared only for cancellation detection because it does not detect absorption.Source: A. Experimental Setup · p. 6

B. RQ1: Soundness Validation and Completeness Evaluation.

  • Across 665 checked cases, FPScan proves 482 (72%) impossible; it is sound by construction, so its false-negative counts are zero and every pitfall it proves impossible is indeed impossible.Source: B. RQ1: Soundness Validation and… · p. 6
  • Only 14 of 183 reported pitfalls (8%) are false positives, and 36 of 41 benchmark analyses contain none.The abstraction can include unreachable machine states, preventing FPScan from proving that some non-occurring pitfalls are impossible.Source: B. RQ1: Soundness Validation and… · p. 6
  • For programs shown in bold, FPScan’s detected cancellations and FPChecker’s detected cancellations exactly match, with the tools providing complementary information.In these cases, FPScan proves some cancellations impossible while FPChecker guarantees others are possible through a counterexample.Source: B. RQ1: Soundness Validation and… · p. 7

C. RQ2 Execution Time Evaluation

FPScan combines static analysis and constraint solving to detect floating-point pitfalls, with evaluation reporting precision and execution-time comparisons. The related-work discussion contrasts its scope and constraints with dynamic and static alternatives.

C. RQ2 Execution Time Evaluation

  • FPScan was comparable to FPChecker and significantly faster than bitblasting on the evaluated benchmarks.Figure 7 compares execution times for 58 FPBench benchmarks, ordered by bitblasting time, on a logarithmic scale; some bitblasting times are unavailable because of timeouts or unsupported operations.Source: C. RQ2 Execution Time Evaluation · p. 7

V. RELATED WORK

  • Unlike precision tuning for a target output precision, FPScan uses a different constraint set, including nsb and refined error propagation, and tests pitfall constraints for unsatisfiability.The related-work discussion also says its ufp and ulp constraint formalization extends to denormalized numbers.Source: A. ufp, ulp, and nsb constraint-based… · p. 7

B. Detection of Floating-Point Pitfalls

  • Dynamic techniques target cancellations rather than absorptions and are not sound without exploring the entire input space, whereas FPScan reasons soundly over all executions for both pitfalls.The paper notes that fully exploring the input space is generally infeasible in practice.Source: B. Detection of Floating-Point Pitfalls · p. 8
  • FPScan supports denormalized values, sound loop analysis up to a user-specified unrolling bound, and rounding-error-aware cancellation detection; direct comparison with Lopes et al. was unavailable.The authors could not compare directly because the other tool was not freely available.Source: B. Detection of Floating-Point Pitfalls · p. 8

VI. CONCLUSION

  • 72% of cases were proven impossible with 8% false positives, while FPScan outperformed bitblasting and compared favorably with FPChecker.The conclusion presents these as the experimental results for FPScan.Source: §VI · p. 8
  • Extending FPScan to mixed-precision programs remains future work.The conclusion also proposes using identified pitfalls to suggest guaranteed repairs.Source: §VI · p. 8

APPENDIX

The appendix proves the soundness of abstract addition and subtraction by bounding the propagated error and deriving a bound on the result’s number of significant bits.

A. Soundness of abstract addition/subtraction (cf. Def. 4)

  • The proof represents each real value as its floating-point value plus an error, then derives a bound on the result error from the input errors and operation rounding error.The addition rounding error is denoted e+.Source: A. Soundness of abstract… · p. 10
  • The bound on the result error uses the triangle inequality, bounds on input errors, and the operation’s rounding-error bound.The rounding error e+ is bounded using the ulp relation; the proof then bounds a sum of powers of two.Source: A. Soundness of abstract… · p. 10
  • Bounding the result error yields a bound on its ufp, which together with the stated relation gives the desired nsb bound.The appendix states that the equations used remain valid for zero and denormalized numbers.Source: A. Soundness of abstract… · p. 10, APPENDIX · p. 10

B. Soundness of abstract multiplication (cf. Def. 5)

The multiplication soundness proof bounds the result error from operand errors and multiplication rounding, then uses that bound to constrain the result’s number of significant bits.

B. Soundness of abstract multiplication (cf. Def. 5)

  • The proof expresses multiplication’s real result through floating-point operands, their errors, and the multiplication rounding error.It bounds the result error using the triangle inequality and bounds on operand magnitudes and errors.Source: B. Soundness of abstract… · p. 10
  • The proof bounds the operand magnitudes using their ufp values and combines powers-of-two bounds to bound the result error.The derivation uses a maximum exponent to bound a sum of four terms.Source: B. Soundness of abstract… · p. 11
  • The resulting error bound is used to bound the result’s nsb, completing the soundness argument for multiplication.The proof invokes the rounding-error relation for the multiplication rounding term.Source: B. Soundness of abstract… · pp. 10–11

C. Soundness of abstract division (cf. Def. 6)

The division soundness proof bounds the quotient error by bounding its numerator and controlling the denominator away from zero under a small-error condition.

C. Soundness of abstract division (cf. Def. 6)

  • The quotient error bound requires an upper bound on the numerator error term and a lower bound on the denominator.The proof identifies these as the two quantities needed to bound the quotient’s absolute error.Source: C. Soundness of abstract division (cf.… · p. 11
  • The analysis applies the denominator lower bound only when nsb(yv) > 1; otherwise, it applies no constraint.This condition expresses the proof’s small-error scenario, preventing the denominator expression from being too close to zero under the stated bound.Source: C. Soundness of abstract division (cf.… · p. 11
  • The numerator and denominator bounds are combined to bound the quotient error, which then supports the result’s nsb bound.The proof states that the division rounding error is denoted e÷ and uses the rounding-error relation for it.Source: C. Soundness of abstract division (cf.… · pp. 11–12

D. Soundness of abstract Cos, Sin, and Atan (cf. Def. 7)

For abstract cos, sin, and atan, the soundness argument bounds output error by combining a Taylor remainder with rounding error, yielding a bound on nsbσ(zv).

D. Soundness of abstract Cos, Sin, and Atan (cf. Def. 7)

E. Soundness of abstract Sqrt (cf. Def. 8)

For abstract sqrt, the soundness argument bounds output error by separating the propagated input-error contribution from operation rounding, then bounding the propagated contribution.

E. Soundness of abstract Sqrt (cf. Def. 8)

  • The analysis represents the real values x and z and their floating-point counterparts ˜x and ˜z through the machine state σ.The errors are defined as εx = x − ˜x and εz = z − ˜z.Source: E. Soundness of abstract Sqrt (cf.… · p. 12
  • The proof bounds the propagated sqrt error contribution Δ using its derivative with respect to x.It then combines the bound on Δ with a bound on the operation's rounding error e using ulp(˜z).Source: E. Soundness of abstract Sqrt (cf.… · p. 12
  • The operation's rounding error e is bounded using ulp(˜z), while the propagated error depends on εx.The proof uses these contributions to bound εz.Source: E. Soundness of abstract Sqrt (cf.… · p. 12
  • The proof converts the Eq. (58) power-of-two bound on |εz| into a bound on ufp(εz), then uses Eq. (59) with Def. 3 to conclude.The derivation uses Eq. (3) to bound ufp and Def. 3 to define nsb.Source: E. Soundness of abstract Sqrt (cf.… · p. 12
Loading 2609.07492v1…