fix: Abstract interpretation proves false assertions about floats - #1157
Draft
fabiomadge wants to merge 2 commits into
Draft
fabiomadge wants to merge 2 commits into
fabiomadge wants to merge 2 commits into
Conversation
This was referenced Aug 31, 2026
`NativeIntervalDomain` stores a variable's bounds as a pair of integers under
two conventions -- `Lo <= v < Hi` for an int, `Lo <= v <= Hi` for a real -- and
every site that picks between them tests `Type.IsReal`, which is false for a
float. Floats were stored with the real convention and read with the integer
one, so a float pinned to a literal, whose bounds are equal, was read as the
empty interval:
m := 1.0;
if (m == 1.0) { ... } // Meet -> hi <= lo -> bottom: the branch is dead
That made the then-branch of a float equality unreachable in the abstraction, so
a loop alternating a float between two values reported only one of them and
`-infer:j` proved a false assertion. Six further defects share the mismatch: an
equality emitted for a point interval, which `-0.0` fails because Boogie's `==`
on floats is bit identity; the half-open `-1` in `Add`; comparison folding under
the wrong convention; `Constraint`'s `Lt` tightening a float bound by one;
`ConstrainNeq` excluding a value that is not an endpoint; and NaN acquiring
bounds through arithmetic. A bound is also emitted as a literal of the
variable's own format, and `BigFloat.FromBigInt` throws rather than rounds when
the integer does not fit, so two shapes crashed outright.
An interval of integers cannot describe a float. Arithmetic rounds, overflows to
an infinity and produces NaN, so bounds computed from the operands' bounds need
not hold of the result; `-0.0` and `+0.0` have one value while `==` separates
them, so a one-point interval is not one point; and NaN is unordered, so no
bound holds of it. Rather than repair each site, this stops the domain modelling
floats at all: `PEVisitor.VisitLiteralExpr` no longer gives a float literal
integer bounds, and since `VisitIdentifierExpr` never read a float variable's
bounds either, no float expression has bounds and so no float variable is ever
constrained or assigned any. The float arms of `Node.ToExpr` and `NumberToExpr`
go with it.
WHAT THIS GIVES UP. Some of what the domain inferred about a float was sound,
and goes too: a two-sided range from `<=` assumes, which `Constraint`'s `Le`
case always handled correctly since it makes no +-1 adjustment; the floor and
ceiling brackets of a literal assignment, and their join across branches; and a
non-float value folded through a float comparison, such as
`x := if (1.5 <= 2.0) then 5 else 7`. Each needs a hand-written float literal in
a loop, and each rode on the machinery above, so none survives without it.
IT ORPHANS AN API ADDED FOR THIS CALL SITE. `BigFloat.TryFloorCeiling` and
`MaxFloorCeilingBits` were added in #1142 to keep the deleted call site from
overflowing on a wide exponent. They now have no production caller. They stay:
both are public, unit-tested, and a reasonable sibling to `FloorCeiling`. The
deletion is deliberate, not a merge accident.
This fixes the float-specific defects and one crash. It does not make `-infer:j`
sound: the same file still derives an upper bound from two lower bounds in
`Mul`, pins a value on division or mod by zero, trusts `{:identity}` against the
verification condition, and crashes on a null type in `ThresholdFinder`.
The tests are one mechanism per file, following the convention of the directory,
so that a regression names itself, and each of the seven wrongly verifies on
`master`. Two others cover what a consequence test cannot.
`IntervalNoFloatTracked.bpl` pins the property that makes the seven hold, by
printing what is inferred for a program that exercises every route to a float
bound -- a literal, a copy, an if-then-else, a comparison, a disequality,
arithmetic and a NaN -- and showing no element mentions a float. That catches a
re-admission of float tracking even where the re-admission is sound, which none
of the seven would. `IntervalStillInferred.bpl` is the other half: non-float
inference is unchanged in a program that mentions floats, and still proves
`0 <= j` from an inferred loop invariant.
fabiomadge
force-pushed
the
fix/interval-domain-no-floats
branch
from
September 20, 2026 15:50
c920def to
d9a4a97
Compare
shazqadeer
reviewed
Sep 20, 2026
| public class Node | ||
| { | ||
| public readonly Variable V; // variable has type bool or int | ||
| // Never of float type: see PEVisitor.VisitLiteralExpr for why, and the constructors, which say so |
Contributor
There was a problem hiding this comment.
This comment does not make any sense.
shazqadeer
reviewed
Sep 20, 2026
| // bounds (Update). A pair of integer bounds cannot describe a float at all, for the reasons set | ||
| // out on FloatType. | ||
|
|
||
| return node; |
Contributor
There was a problem hiding this comment.
Is this 'return node' happening for BigFloat type with other cases being considered above? If so, please add an assertion here to document.
| } | ||
|
|
||
| return e; | ||
| } |
Contributor
There was a problem hiding this comment.
Why are we deleting all this code for Real type? I thought we are focused on the Float type in this PR.
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
2 participants
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.
The interval domain describes a variable by a pair of integer bounds, and asked float literals for theirs.
A float has no such value to bound: arithmetic rounds and overflows, so bounds computed from the operands
need not hold of the result; the order ties
-0.0and+0.0where==separates them, so a one-pointinterval is not one point; and no bound at all holds of a NaN.
-infer:j→ 1 verified, 0 errors. Three flips leavemat 2.0. A float pinned to a literal has equalbounds, and
Meettests emptiness the way it does for an int, whereLo == Himeans empty — so thethen-branch was inferred unreachable.
Fix. The domain computes no bounds for a float: the
BigFloatcase inPEVisitor.VisitLiteralExprgoes, and with it the float arms of
Node.ToExprandNumberToExpr.ToExprkeeps the real arm where itwas and replaces the float one with an unreachable guard, which also makes the diff read the way it
behaves — the two arms had identical bodies, so deleting the float one rendered as deleting the real one.
Both
Nodeconstructors assert the invariant, and the literal fallthrough asserts that a float leaves thebounds cleared.
Scope. What is lost is any inference about a float. The domain already declines the one other type it
cannot describe — a bitvector is never tracked — so this brings floats into line with that. Of the ten
tests added, seven pin a consequence that used to be proved falsely, one an unhandled
ArgumentException,one that variables the domain can describe are still tracked in a program mentioning floats, and one the
property itself.
One of six; #1154 should land first, since a comment here cites it.