From 2a08d7861ec1da1b4a3e3adc8114c56463f50b8e Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Tue, 28 Jul 2026 15:56:36 -0700 Subject: [PATCH] Fix floating point comparisons involving infinity/NaN for cross-type numeric comparisons PiperOrigin-RevId: 955519324 --- .../dev/cel/verifier/axioms/AxiomHelpers.java | 48 ++++++++++++++++++ .../dev/cel/verifier/axioms/GreaterAxiom.java | 28 ++++++----- .../verifier/axioms/GreaterEqualsAxiom.java | 28 ++++++----- .../dev/cel/verifier/axioms/LessAxiom.java | 20 +++++--- .../cel/verifier/axioms/LessEqualsAxiom.java | 20 +++++--- .../cel/verifier/CelVerifierZ3ImplTest.java | 50 +++++++++++++++++++ 6 files changed, 154 insertions(+), 40 deletions(-) diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/AxiomHelpers.java b/verifier/src/main/java/dev/cel/verifier/axioms/AxiomHelpers.java index a249b4fe9..c7b101e21 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/AxiomHelpers.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/AxiomHelpers.java @@ -16,7 +16,9 @@ import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; +import com.microsoft.z3.FPExpr; import com.microsoft.z3.IntExpr; +import com.microsoft.z3.RealExpr; /** Helper methods for Z3 axioms operations. */ final class AxiomHelpers { @@ -47,5 +49,51 @@ static IntExpr mkTruncatedMod(Context ctx, IntExpr a, IntExpr b) { return (IntExpr) ctx.mkSub(a, ctx.mkMul(mkTruncatedDiv(ctx, a, b), b)); } + /** + * Safe comparison between a Z3 Real (from int/uint) and a Z3 FloatingPoint (double) for {@code + * <}. + */ + static BoolExpr mkRealLtFp(Context ctx, RealExpr real, FPExpr fp) { + return mkSafeFpComparison(ctx, fp, isPosInf(ctx, fp), ctx.mkLt(real, ctx.mkFPToReal(fp))); + } + + /** + * Safe comparison between a Z3 FloatingPoint (double) and a Z3 Real (from int/uint) for {@code + * <}. + */ + static BoolExpr mkFpLtReal(Context ctx, FPExpr fp, RealExpr real) { + return mkSafeFpComparison(ctx, fp, isNegInf(ctx, fp), ctx.mkLt(ctx.mkFPToReal(fp), real)); + } + + /** + * Safe comparison between a Z3 Real (from int/uint) and a Z3 FloatingPoint (double) for {@code + * <=}. + */ + static BoolExpr mkRealLeFp(Context ctx, RealExpr real, FPExpr fp) { + return mkSafeFpComparison(ctx, fp, isPosInf(ctx, fp), ctx.mkLe(real, ctx.mkFPToReal(fp))); + } + + /** + * Safe comparison between a Z3 FloatingPoint (double) and a Z3 Real (from int/uint) for {@code + * <=}. + */ + static BoolExpr mkFpLeReal(Context ctx, FPExpr fp, RealExpr real) { + return mkSafeFpComparison(ctx, fp, isNegInf(ctx, fp), ctx.mkLe(ctx.mkFPToReal(fp), real)); + } + + private static BoolExpr isPosInf(Context ctx, FPExpr fp) { + return ctx.mkAnd(ctx.mkFPIsInfinite(fp), ctx.mkFPIsPositive(fp)); + } + + private static BoolExpr isNegInf(Context ctx, FPExpr fp) { + return ctx.mkAnd(ctx.mkFPIsInfinite(fp), ctx.mkFPIsNegative(fp)); + } + + private static BoolExpr mkSafeFpComparison( + Context ctx, FPExpr fp, BoolExpr infCondition, BoolExpr finiteComparison) { + BoolExpr isFinite = ctx.mkNot(ctx.mkOr(ctx.mkFPIsNaN(fp), ctx.mkFPIsInfinite(fp))); + return ctx.mkOr(infCondition, ctx.mkAnd(isFinite, finiteComparison)); + } + private AxiomHelpers() {} } diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java index 2dce5c8e6..527ef70ad 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java @@ -88,33 +88,37 @@ final class GreaterAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGt( - ctx.mkInt2Real(typeSystem.getInt(lhs)), - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(rhs)))))) + AxiomHelpers.mkFpLtReal( + ctx, + (FPExpr) typeSystem.getDouble(rhs), + ctx.mkInt2Real(typeSystem.getInt(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_UINT64_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGt( - ctx.mkInt2Real(typeSystem.getUint(lhs)), - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(rhs)))))) + AxiomHelpers.mkFpLtReal( + ctx, + (FPExpr) typeSystem.getDouble(rhs), + ctx.mkInt2Real(typeSystem.getUint(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_DOUBLE_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGt( - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(lhs)), - ctx.mkInt2Real(typeSystem.getInt(rhs)))))) + AxiomHelpers.mkRealLtFp( + ctx, + ctx.mkInt2Real(typeSystem.getInt(rhs)), + (FPExpr) typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_DOUBLE_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGt( - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(lhs)), - ctx.mkInt2Real(typeSystem.getUint(rhs)))))) + AxiomHelpers.mkRealLtFp( + ctx, + ctx.mkInt2Real(typeSystem.getUint(rhs)), + (FPExpr) typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_INT64_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java index b3c401aa7..ec3ffa69a 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java @@ -88,33 +88,37 @@ final class GreaterEqualsAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGe( - ctx.mkInt2Real(typeSystem.getInt(lhs)), - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(rhs)))))) + AxiomHelpers.mkFpLeReal( + ctx, + (FPExpr) typeSystem.getDouble(rhs), + ctx.mkInt2Real(typeSystem.getInt(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_UINT64_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGe( - ctx.mkInt2Real(typeSystem.getUint(lhs)), - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(rhs)))))) + AxiomHelpers.mkFpLeReal( + ctx, + (FPExpr) typeSystem.getDouble(rhs), + ctx.mkInt2Real(typeSystem.getUint(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_DOUBLE_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGe( - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(lhs)), - ctx.mkInt2Real(typeSystem.getInt(rhs)))))) + AxiomHelpers.mkRealLeFp( + ctx, + ctx.mkInt2Real(typeSystem.getInt(rhs)), + (FPExpr) typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_DOUBLE_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGe( - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(lhs)), - ctx.mkInt2Real(typeSystem.getUint(rhs)))))) + AxiomHelpers.mkRealLeFp( + ctx, + ctx.mkInt2Real(typeSystem.getUint(rhs)), + (FPExpr) typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_INT64_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java index 9c34709d0..429aee284 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java @@ -88,32 +88,36 @@ final class LessAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLt( + AxiomHelpers.mkRealLtFp( + ctx, ctx.mkInt2Real(typeSystem.getInt(lhs)), - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(rhs)))))) + (FPExpr) typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_UINT64_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLt( + AxiomHelpers.mkRealLtFp( + ctx, ctx.mkInt2Real(typeSystem.getUint(lhs)), - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(rhs)))))) + (FPExpr) typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_DOUBLE_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLt( - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(lhs)), + AxiomHelpers.mkFpLtReal( + ctx, + (FPExpr) typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getInt(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_DOUBLE_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLt( - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(lhs)), + AxiomHelpers.mkFpLtReal( + ctx, + (FPExpr) typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getUint(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_INT64_UINT64.celOverloadDecl(), diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java index 750961515..5099850dd 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java @@ -88,32 +88,36 @@ final class LessEqualsAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLe( + AxiomHelpers.mkRealLeFp( + ctx, ctx.mkInt2Real(typeSystem.getInt(lhs)), - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(rhs)))))) + (FPExpr) typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_UINT64_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLe( + AxiomHelpers.mkRealLeFp( + ctx, ctx.mkInt2Real(typeSystem.getUint(lhs)), - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(rhs)))))) + (FPExpr) typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_DOUBLE_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLe( - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(lhs)), + AxiomHelpers.mkFpLeReal( + ctx, + (FPExpr) typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getInt(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_DOUBLE_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLe( - ctx.mkFPToReal((FPExpr) typeSystem.getDouble(lhs)), + AxiomHelpers.mkFpLeReal( + ctx, + (FPExpr) typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getUint(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_INT64_UINT64.celOverloadDecl(), diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 2b41408d7..59a5e8438 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -498,6 +498,34 @@ private enum IsAlwaysTrueTestCase { IEEE_754_NEG_ZERO_IN_LIST("-0.0 in [0.0]"), IEEE_754_POS_ZERO_IN_LIST("0.0 in [-0.0]"), IEEE_754_NAN_IN_LIST_FALSE("!((0.0/0.0) in [1.0, (0.0/0.0)])"), + CROSS_TYPE_NUMERIC_LESS_NAN_INT_FALSE("!(x < (0.0 / 0.0))"), + CROSS_TYPE_NUMERIC_LESS_INT_NAN_FALSE("!((0.0 / 0.0) < x)"), + CROSS_TYPE_NUMERIC_LESS_EQUALS_NAN_INT_FALSE("!(x <= (0.0 / 0.0))"), + CROSS_TYPE_NUMERIC_GREATER_NAN_INT_FALSE("!(x > (0.0 / 0.0))"), + CROSS_TYPE_NUMERIC_GREATER_EQUALS_NAN_INT_FALSE("!(x >= (0.0 / 0.0))"), + CROSS_TYPE_NUMERIC_LESS_NAN_UINT_FALSE("!(u < (0.0 / 0.0))"), + CROSS_TYPE_NUMERIC_LESS_UINT_NAN_FALSE("!((0.0 / 0.0) < u)"), + CROSS_TYPE_NUMERIC_LESS_EQUALS_NAN_UINT_FALSE("!(u <= (0.0 / 0.0))"), + CROSS_TYPE_NUMERIC_GREATER_NAN_UINT_FALSE("!(u > (0.0 / 0.0))"), + CROSS_TYPE_NUMERIC_GREATER_EQUALS_NAN_UINT_FALSE("!(u >= (0.0 / 0.0))"), + CROSS_TYPE_NUMERIC_LESS_POS_INF_INT("x < (1.0 / 0.0)"), + CROSS_TYPE_NUMERIC_LESS_EQUALS_POS_INF_INT("x <= (1.0 / 0.0)"), + CROSS_TYPE_NUMERIC_GREATER_POS_INF_INT_FALSE("!(x > (1.0 / 0.0))"), + CROSS_TYPE_NUMERIC_GREATER_EQUALS_POS_INF_INT_FALSE("!(x >= (1.0 / 0.0))"), + CROSS_TYPE_NUMERIC_GREATER_POS_INF_DOUBLE_INT("(1.0 / 0.0) > x"), + CROSS_TYPE_NUMERIC_GREATER_EQUALS_POS_INF_DOUBLE_INT("(1.0 / 0.0) >= x"), + CROSS_TYPE_NUMERIC_LESS_POS_INF_DOUBLE_INT_FALSE("!((1.0 / 0.0) < x)"), + CROSS_TYPE_NUMERIC_LESS_EQUALS_POS_INF_DOUBLE_INT_FALSE("!((1.0 / 0.0) <= x)"), + CROSS_TYPE_NUMERIC_GREATER_NEG_INF_INT("x > (-1.0 / 0.0)"), + CROSS_TYPE_NUMERIC_GREATER_EQUALS_NEG_INF_INT("x >= (-1.0 / 0.0)"), + CROSS_TYPE_NUMERIC_LESS_NEG_INF_INT_FALSE("!(x < (-1.0 / 0.0))"), + CROSS_TYPE_NUMERIC_LESS_EQUALS_NEG_INF_INT_FALSE("!(x <= (-1.0 / 0.0))"), + CROSS_TYPE_NUMERIC_LESS_NEG_INF_DOUBLE_INT("(-1.0 / 0.0) < x"), + CROSS_TYPE_NUMERIC_LESS_EQUALS_NEG_INF_DOUBLE_INT("(-1.0 / 0.0) <= x"), + CROSS_TYPE_NUMERIC_LESS_POS_INF_UINT("u < (1.0 / 0.0)"), + CROSS_TYPE_NUMERIC_LESS_EQUALS_POS_INF_UINT("u <= (1.0 / 0.0)"), + CROSS_TYPE_NUMERIC_GREATER_NEG_INF_UINT("u > (-1.0 / 0.0)"), + CROSS_TYPE_NUMERIC_GREATER_EQUALS_NEG_INF_UINT("u >= (-1.0 / 0.0)"), STRING_IN_LIST("'b' in ['a', 'b', 'c']"), INT_IN_MAP("1 in {1: 2}"), MAP_MISSING_KEY("!(3 in {1: 'a', 2: 'b'})"), @@ -1426,6 +1454,14 @@ private enum EquivalenceTestCase { CROSS_TYPE_NUMERIC_EQUALITY_INT_DOUBLE("request == 1.0", "request == 1"), CROSS_TYPE_NUMERIC_EQUALITY_UINT_DOUBLE("request == 1u", "request == 1.0"), CROSS_TYPE_NUMERIC_EQUALITY_INT_UINT("request == 1", "request == 1u"), + CROSS_TYPE_NUMERIC_NAN_LESS_INT("x < (0.0 / 0.0)", "false"), + CROSS_TYPE_NUMERIC_NAN_LESS_UINT("u < (0.0 / 0.0)", "false"), + CROSS_TYPE_NUMERIC_NAN_GREATER_INT("x > (0.0 / 0.0)", "false"), + CROSS_TYPE_NUMERIC_NAN_GREATER_UINT("u > (0.0 / 0.0)", "false"), + CROSS_TYPE_NUMERIC_POS_INF_GREATER_INT("(1.0 / 0.0) > x", "true"), + CROSS_TYPE_NUMERIC_POS_INF_LESS_INT("x < (1.0 / 0.0)", "true"), + CROSS_TYPE_NUMERIC_NEG_INF_GREATER_INT("x > (-1.0 / 0.0)", "true"), + CROSS_TYPE_NUMERIC_NEG_INF_LESS_INT("(-1.0 / 0.0) < x", "true"), STATIC_DOUBLE_EQUALITY("d + 1.0 == d + 1.0", "d == d"), MAP_FIELD_SELECT("string_int_map.my_field > 0", "string_int_map['my_field'] > 0"), HETEROGENEOUS_LIST_SIZES_SAFE_FALSE("!([1, 2] == [1, 2, 3])", "true"), @@ -2715,4 +2751,18 @@ public void verifyImplication_loopExceedsLimit_returnsTruncatedInconclusive() th assertThat(result.message()) .contains("implication holds within the current loop unroll limit"); } + + @Test + public void verifyImplication_symbolicNan_crossNumericComparisonReturnsFalse() throws Exception { + // Assumption: d is NaN (d != d) + CelAbstractSyntaxTree assumeAst = CEL.compile("d != d").getAst(); + // Assertion: x < d is false when d is NaN + CelAbstractSyntaxTree assertAst = CEL.compile("!(x < d)").getAst(); + + CelVerifier verifier = CelVerifierFactory.newVerifier().build(); + CelVerificationResult result = + ((CelVerifierZ3Impl) verifier) + .verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Implication"); + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } }