fix: !(x < y) is rewritten to y <= x even for floats - #1156
Draft
fabiomadge wants to merge 3 commits into
Draft
fabiomadge wants to merge 3 commits into
fabiomadge wants to merge 3 commits into
Conversation
This was referenced Aug 31, 2026
Expr.Not turned a negated order relation into the reverse relation for every type. That is only valid where the order is total: on floats every IEEE comparison is false when an operand is NaN, so "!(a < b)" holds of a NaN while "b <= a" does not. Equality is unaffected, since Boogie's == on floats is bit identity and therefore total. The type is not always available where Expr.Not is called: the parser negates the guard of an "if" or a "while" while it is still building an implementation's blocks. Such a negation is now left alone, and Program.Typecheck asks Expr.Not again once the types are in place, so an integer guard is still reversed and a float's is not. That also stops Boogie reporting a type error against the reversed operator it synthesised rather than the one the program contains.
A negation the parser built for the "!" operator never went through Expr.Not, so Constraint saw shapes it had no case for and learned nothing from them. It now pushes the negation inwards with the same rewriting Expr.Not applies everywhere else, which by then has the types it needs. Expr.Not declines to reverse an order relation on a float, so a result that is still a negation is one there is nothing to learn from.
fabiomadge
force-pushed
the
fix/negated-float-comparison
branch
from
September 20, 2026 15:50
a639f9d to
d3416a8
Compare
Contributor
|
@fabiomadge : Is it possible to solve the problem by avoiding any attempt to rewrite negations until the type is determined (and known not to be float)? That seems simpler at a first glance. |
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.
Expr.Notturned a negated order relation into the reverse relation for every type. That is valid onlywhere the order is total: every IEEE comparison is false when an operand is NaN, so
!(a < b)holds of aNaN while
b <= adoes not.No flags → 1 verified, 0 errors. The
elsebranch is reachable with a NaN, where the assertion isfalse.
Fix.
Expr.Notleaves an order relation alone unless the operand's type is known and not float. Itusually is not known, and cannot be made so: the guard is negated from the
Implementationconstructor,which flattens the structured statements while parsing, before any identifier is resolved. So no
reordering inside resolution can supply a type, and
Program.ReverseGuardNegationsasks again once typesexist. The second commit has
IntervalDomain.Constraintpush a hand-written!through the same helper,which it never did.
Scope. Equality is untouched,
==on floats being bit identity and so total. Inference gets sharperwhere the domain can now read a negation:
aitest1/ineq.bplinfersi == 10where it inferred0 <= i && i < 11. Two printed forms change.roundingmodes/InvalidOperators.bplloses four phantom typeerrors, which named operators the program does not contain.
inline/test4.bplkeeps an unreversed guard,because a
-printof the program as parsed runs before resolution while the blocks already exist, so thereversal cannot reach it.
Not addressed. The pass finds guards by
{:partition}, which a user may write; such an assume gets thesame rewriting, semantics-preserving but visible through
/print.One of six.
TryPushNegationsetsTypeandTypeParametersindependently, which matters once #1155lands: it types comparisons at construction, and a node with a type but no type parameters crashes
MonomorphizationDuplicator.