Cleanup fmod vs IEEE remainder#7885
Open
tautschnig wants to merge 18 commits into
Open
Conversation
Collaborator
tautschnig
commented
Sep 12, 2023
tautschnig
commented
- Add tests for both the C and Java front-end.
- Make sure we support both variants of the modulus operator on floating-point values in the back-ends: the SMT back-end only supported remainder (and only for FPA mode), the propositional back-end did not distinguish between fmod and IEEE remainder.
- Each commit message has a non-empty body, explaining why the change was made.
- Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
- n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
- Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
- n/a My commit message includes data points confirming performance improvements (if claimed).
- My PR is restricted to a single feature or bugfix.
- n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.
tautschnig
force-pushed
the
cleanup/floatbv-mod-rem
branch
2 times, most recently
from
2c2733f to
a7d2d63
Compare
Collaborator
Author
|
Asking for help from @martin-cs: the remaining issue is that we need an ability to round-to-integer ( |
tautschnig
force-pushed
the
cleanup/floatbv-mod-rem
branch
from
a7d2d63 to
49c66f4
Compare
tautschnig
force-pushed
the
cleanup/floatbv-mod-rem
branch
from
49c66f4 to
f007d82
Compare
tautschnig
force-pushed
the
cleanup/floatbv-mod-rem
branch
from
f007d82 to
82f5832
Compare
tautschnig
requested review from
TGWDB,
jimgrundy,
kroening,
martin-cs and
remi-delmas-3000
as code owners
There was a problem hiding this comment.
Pull request overview
This PR improves CBMC/JBMC’s handling of floating-point modulus/remainder by distinguishing C/Java “fmod-style” remainder from IEEE-754 remainder, and introduces an FMA primitive to support a more precise IEEE remainder encoding across backends.
Changes:
- Add
floatbv_fmaexpression support plus a propositional (boolbv) implementation and SMT2-FPA conversion. - Rework floating-point mod/rem encodings: boolbv now selects RTZ vs RN-even based on
floatbv_modvsfloatbv_rem; SMT2 gainsfloatbv_modconversion. - Add/enable regression and unit tests for C and Java front-ends, plus a Coq proof artifact for the FMA-based remainder argument.
Reviewed changes
Copilot reviewed 48 out of 49 changed files in this pull request and generated 7 comments.
Show a summary per file
| File | Description |
|---|---|
| unit/solvers/floatbv/float_utils.cpp | Adds SAT-level unit tests for FMA behavior. |
| src/util/irep_ids.def | Introduces ID_floatbv_fma. |
| src/util/floatbv_expr.h | Adds floatbv_fma_exprt node type. |
| src/solvers/smt2_incremental/convert_expr_to_smt.cpp | Touches (still-disabled) dispatch for floatbv mod/rem in incremental SMT2. |
| src/solvers/smt2/smt2_conv.h | Declares SMT2 conversions for floatbv mod and fma. |
| src/solvers/smt2/smt2_conv.cpp | Implements SMT2 conversions for floatbv mod and fma; updates symbol finding. |
| src/solvers/floatbv/float_utils.h | Adds float_utilst::fma API. |
| src/solvers/floatbv/float_utils.cpp | Implements propositional FMA and reworks float_utilst::rem encoding. |
| src/solvers/floatbv/float_bv.h | Adds word-level mod/rem APIs. |
| src/solvers/floatbv/float_bv.cpp | Implements float_bvt::mod and float_bvt::rem. |
| src/solvers/flattening/boolbv_floatbv_mod_rem.cpp | Selects rounding mode (RTZ vs RN-even) based on expr id. |
| src/solvers/flattening/boolbv_floatbv_fma.cpp | New boolbv conversion for floatbv_fma. |
| src/solvers/flattening/boolbv.h | Declares convert_floatbv_fma. |
| src/solvers/flattening/boolbv.cpp | Dispatches ID_floatbv_fma to the new conversion. |
| src/goto-programs/adjust_float_expressions.cpp | Marks floatbv mod/rem/fma as already-adjusted expressions. |
| src/ansi-c/library/math.c | Replaces fma/remainder wrappers to call __CPROVER_* builtins. |
| src/ansi-c/expr2c.cpp | Adds pretty-printing hooks for floatbv_fma and floatbv_mod. |
| src/ansi-c/cprover_builtin_headers.h | Declares __CPROVER_fma/fmaf/fmal. |
| src/ansi-c/c_typecheck_expr.cpp | Typechecks __CPROVER_fma* into floatbv_fma_exprt. |
| regression/cbmc-library/remainder*/** | Converts prior KNOWNBUG tests to CORE and adds new edge/tie tests plus a bench. |
| regression/cbmc-library/fmod*/** | Converts prior KNOWNBUG tests to CORE and adds concrete assertions. |
| regression/cbmc-library/fma/* | Adds a CORE regression for fmaf semantics. |
| regression/cbmc-library/__sort_of_CPROVER_remainder*/* | Removes obsolete placeholder regressions. |
| jbmc/regression/jbmc/farith2/* | Adds a CORE regression for Java floating %. |
| doc/proofs/fma_remainder.v | Adds Coq proof artifact for representability/rounding claims. |
| doc/proofs/check_proof.sh | Adds helper script to run the Coq proof check. |
| .clang-format-ignore | Excludes the Coq proof file from clang-format. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
tautschnig
force-pushed
the
cleanup/floatbv-mod-rem
branch
5 times, most recently
from
7d350f2 to
1fbb488
Compare
kroening
reviewed
Apr 3, 2026
kroening
reviewed
Apr 3, 2026
kroening
reviewed
Apr 3, 2026
kroening
reviewed
Apr 3, 2026
tautschnig
force-pushed
the
cleanup/floatbv-mod-rem
branch
from
3580205 to
099b6df
Compare
bv_utilst::unsigned_divider always allocated fresh variables for the quotient and remainder, with a quotient*divisor + rem == dividend multiplier constraint, even when both operands are constant. The result was therefore never a constant literal, so a constant division feeding a later multiply produced a (hard) variable*variable multiplier instead of folding away. Add a fast path: when both operands are constant (and the divisor is non-zero), compute the quotient and remainder directly as constants. Division by zero falls through to the existing nondeterministic encoding, so semantics are unchanged. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
cleanup/floatbv-mod-rem
branch
3 times, most recently
from
82728cd to
64f5de4
Compare
The existing ID_floatbv_rem was used for both fmod and IEEE remainder, but these have different semantics (truncation vs round-to-nearest-even). Add ID_floatbv_mod for fmod, keeping ID_floatbv_rem for IEEE remainder. Update adjust_float_expressions to recognize the new ID, expr2c to display it, and the incremental SMT2 back-end. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Replace the old __sort_of_CPROVER_remainder helper functions (which used extended precision as a workaround) with direct calls to __CPROVER_fmod and __CPROVER_remainder built-ins. These lower to ID_floatbv_mod and ID_floatbv_rem respectively, which are handled natively by the solvers. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
The propositional back-end crashed on IEEE remainder because to_signed_integer has a precondition requiring round-to-zero, but remainder uses round-to-even. Fix: use round_to_integral instead of to_signed_integer. The round_to_integral function respects the current rounding mode (ROUND_TO_ZERO for fmod, ROUND_TO_EVEN for IEEE remainder). Set the rounding mode correctly in boolbv_floatbv_mod_rem based on whether the expression is ID_floatbv_mod or ID_floatbv_rem. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
SMT2 with FPA theory: add convert_floatbv_mod using fp.roundToIntegral with roundTowardZero for fmod. IEEE remainder already used fp.rem. SMT2 without FPA theory (float_bvt): add mod() and rem() methods that compute x - round_to_integer(x/y) * y with appropriate rounding. Use _Float16 in the regression test for faster SMT solving. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Verify concrete values and add float-overflow-check and nan-check. Mark fmodl as THOROUGH due to long double divider size The integer significand divider for long double (80-bit, e=15) is 32834 bits wide, causing the test to take ~15 minutes. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Verify concrete values and add float-overflow-check and nan-check. Mark remainderl as THOROUGH due to long double divider size The integer significand divider for long double is 32834 bits wide, causing the test to take ~4 minutes. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Test remainder with inputs where fp division rounds the quotient across an integer boundary. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Test IEEE 754 tie-breaking behavior when quotient is near n+0.5. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Test the Java % operator on doubles, which uses fmod semantics. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
SMT-LIB tests: - fp-rem-nonstandard/fp-rem1: fp.rem(3.0, 2.0) correctness (KNOWNBUG) - fp-rem-nonstandard/fp-rem-nonstandard1: fp.rem on non-standard sort - Tests from Z3 issues z3#2381 and z3#6553 (correctness, KNOWNBUG) C test: - Float-rem1: remainderf(3.0f, 2.0f) (KNOWNBUG) Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Replace the extended-precision approach with FMA-based comparison for
the IEEE remainder correction step. FMA computes x - n*y with a single
rounding (the product n*y is exact internally), which provides a much
stronger soundness argument than the extended-precision approach.
Soundness proof sketch (included as comments in the code):
(a) The tentative n from round_to_integral(fp_div(x,y)) is off by at
most 1 from the correct n_correct.
(b) fma(-n_correct, y, x) = R_correct exactly, because IEEE 754
specifies that the remainder is exactly representable.
(c) fma(-n_wrong, y, x) = round(R_wrong). Since |R_wrong| >= |y|/2
and |R_correct| <= |y|/2, the gap |R_wrong| - |R_correct| >= ulp(y),
which exceeds the FMA rounding error of 1/2 ulp(R_wrong).
(d) In the true tie case (|R_correct| == |y|/2), both FMA results are
exact and equal in magnitude. The rint-chosen even n is kept, which
is correct per IEEE 754 tie-breaking.
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Add __CPROVER_fmodf16, __CPROVER_remainderf16, __CPROVER_fmaf16 declarations and typechecker support. This enables verification of floating-point remainder on _Float16, where the integer significand division produces a manageable formula (~16K variables vs ~194K for float). Add a CORE regression test that verifies |remainder(x,y)| <= |y|/2 for ALL finite _Float16 inputs (completes in ~3s with MiniSat). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Add a Coq/Flocq proof (doc/proofs/fma_remainder.v) that machine-checks correctness properties of the FMA-based IEEE remainder algorithm. Fully proved (zero admits, Coq 8.18 + Flocq): remainder_format: x - n*y is exactly representable in FLX format when |x - n*y| <= |y|/2 (both exponent orderings). fma_remainder_exact: round(x - n*y) = x - n*y, so FMA returns the exact remainder without rounding. comparison_step: the wrong candidate (n +/- 1) has strictly larger |remainder| than the correct one in exact arithmetic. Add nearest_int_small, fmod_then_remainder, and rounding_preserves_remainder_comparison. Move comparison_step out of the FMA_Remainder section. Remove dead comments. Add nearest_integer_from_ratio_lt for ey > ex case. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Port core theorems using native int type with div/rem and real_zpow for integer exponents. All proved with zero mk_thm. Update check_proof.sh to verify both Coq and HOL Light. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Add a CI workflow that triggers when float implementation or proof files change. It verifies: 1. Coq proofs compile (zero admits) 2. HOL Light proofs pass (zero mk_thm) 3. _Float16 exhaustive tests pass (linking proofs to implementation) Add _Float16 tests for specific proved properties: - special_cases: fmod(inf,y)=NaN, fmod(x,0)=NaN, etc. - fmod_bound: |fmod(x,y)| < |y| for all finite inputs Add cross-reference comments in float_utilst::rem mapping each proof theorem to its corresponding _Float16 test. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Replace the try-all-three FMA approach (n, n+1, n-1) with a simpler conditional subtract: compare 2*|fmod| against |y| and correct by ±y when |fmod| > |y|/2, with tie-breaking by quotient parity. This eliminates the div + round_to_integral + 3 FMA calls in float_utils.cpp, and the n±1 multiply + subtract chain in float_bv.cpp, replacing them with a single comparison and one FMA (float_utils) or add/sub (float_bv). Performance (_Float16 remainder property, exhaustive): Before: 4.6s, 85KB SMT2 After: 0.4s, 66KB SMT2 (11x faster, 23% smaller) Performance (float remainderf, fully symbolic): Before: >10 min timeout, 402K vars, 1.98M clauses, 86KB SMT2 After: 17s, 383K vars, 1.89M clauses, 64KB SMT2 Re-enable the float remainderf benchmark (bench.desc) as CORE now that it completes in ~17s. Add Coq proofs (conditional_subtract_closer, no_subtract_when_small, tie_case_equal_abs) and HOL Light proofs (CONDITIONAL_SUBTRACT_CLOSER, NO_SUBTRACT_WHEN_SMALL, TIE_CASE_EQUAL_ABS) confirming the conditional subtract gives the correct IEEE remainder in all cases. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
float_bvt::mod/rem computed fmod as x - trunc(x/y)*y with the quotient truncated to a fixed (type-width) integer. When floor(x/y) exceeds that width it wraps around, giving a wrong result -- e.g. fmod(2048, 2^-5) (quotient 2^16) returned 2048 instead of 0, and the property |fmod(x,y)| < |y| failed for _Float16 under the bit-vector SMT encoding. Replace it with integer-significand arithmetic (align the significands, take a single integer remainder), which is correct for arbitrarily large exponent differences, mirroring float_utilst::rem. mod and rem now share a fmod_via_significand helper; rem keeps the conditional-subtract Step 2 for the IEEE round-to-nearest correction. Adds regression/cbmc-library/remainderf/large_quotient.c demonstrating the bug/fix on the default boolbv path, plus *-z3.desc tests that run the remainderf checks against the float_bvt bit-vector path via cbmc --z3 (the exhaustive _Float16/fmod_bound ones tagged THOROUGH). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
cleanup/floatbv-mod-rem
branch
from
64f5de4 to
71495d3
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.