From 02ae00af7fc2418a71b6c717e4e16f3fa0836d9a Mon Sep 17 00:00:00 2001 From: Sokwhan Huh Date: Thu, 16 Jul 2026 10:53:36 -0700 Subject: [PATCH] Support cross-type numeric equality in verifier PiperOrigin-RevId: 949058814 --- verifier/README.md | 10 - .../cel/verifier/CelAstToZ3Translator.java | 2 +- .../cel/verifier/CelZ3OperatorTranslator.java | 289 ++++++++++++++---- .../dev/cel/verifier/CelZ3TypeSystem.java | 4 - .../dev/cel/verifier/axioms/TypeAxiom.java | 33 +- .../verifier/axioms/TypeConversionAxioms.java | 3 +- .../verifier/CelPolicyVerifierImplTest.java | 2 +- .../cel/verifier/CelVerifierZ3ImplTest.java | 60 +++- 8 files changed, 286 insertions(+), 117 deletions(-) diff --git a/verifier/README.md b/verifier/README.md index a5889d5db..c10ce06eb 100644 --- a/verifier/README.md +++ b/verifier/README.md @@ -229,16 +229,6 @@ public class PolicyVerifierExample { ### Limitations -* **Cross-Type Numeric Comparisons:** - * **Equality (`==`, `!=`):** Equality comparisons between different - numeric types (e.g., `int` vs `double` or `uint` vs `double`) are - currently not supported and will evaluate to `false` during - verification, even if they have the same mathematical value (e.g., - `dyn(1) == dyn(1.0)` is false). Note that `int` vs `uint` equality *is* - supported. - * **Relational Operators (`<`, `>`, `<=`, `>=`):** Cross-type relational - comparisons are fully supported mathematically across all numeric - combinations (`int`, `uint`, and `double`). * **Unsupported Standard Functions (Uninterpreted Functions):** Not all CEL standard library functions have SMT axioms defined yet. Unsupported functions are treated as *uninterpreted functions* by Z3 (the solver diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 0562af693..54049a1b5 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -564,7 +564,7 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a typeConstraints.add(createTypeConstraint(fieldAccess, exprId, ast)); return TranslatedValue.propagateStrict( - ctx, typeSystem, fieldAccess, celExpr, Arrays.asList(operandTv)); + ctx, typeSystem, fieldAccess, celExpr, ImmutableList.of(operandTv)); } private TranslatedValue translateBlock( diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index e2df87b2a..17cd860f8 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -23,7 +23,9 @@ import com.microsoft.z3.Context; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; +import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; +import com.microsoft.z3.IntNum; import com.microsoft.z3.SeqExpr; import dev.cel.common.CelAbstractSyntaxTree; import dev.cel.common.CelFunctionDecl; @@ -223,9 +225,9 @@ private TranslatedValue translateOperatorCall( case LOGICAL_NOT: return translateLogicalNot(args, ast); case EQUALS: - return translateEquals(args.get(0), args.get(1), ast); + return translateEquality(args.get(0), args.get(1), ast, /* isNotEquals= */ false); case NOT_EQUALS: - return translateNotEquals(args.get(0), args.get(1), ast); + return translateEquality(args.get(0), args.get(1), ast, /* isNotEquals= */ true); case LESS: case GREATER: case LESS_EQUALS: @@ -422,9 +424,7 @@ private BoolExpr getNumericEquality( return getDynamicNumericEquality(arg0.z3Expr(), arg1.z3Expr()); } - /** - * Evaluates numeric equality when types are statically known. - */ + /** Evaluates numeric equality when types are statically known. */ private BoolExpr getStaticallyKnownNumericEquality( Expr z3Expr0, CelType type0, Expr z3Expr1) { switch (type0.kind()) { @@ -440,22 +440,51 @@ private BoolExpr getStaticallyKnownNumericEquality( } } + private BoolExpr mkIsFiniteDouble(Expr z3Expr) { + Expr fpVal = typeSystem.getDouble(z3Expr); + return ctx.mkAnd( + typeSystem.isDouble(z3Expr), + ctx.mkNot(ctx.mkOr(ctx.mkFPIsNaN((FPExpr) fpVal), ctx.mkFPIsInfinite((FPExpr) fpVal)))); + } + private BoolExpr getDynamicNumericEquality(Expr z3Expr0, Expr z3Expr1) { BoolExpr isIntOrUint0 = ctx.mkOr(typeSystem.isInt(z3Expr0), typeSystem.isUint(z3Expr0)); BoolExpr isIntOrUint1 = ctx.mkOr(typeSystem.isInt(z3Expr1), typeSystem.isUint(z3Expr1)); BoolExpr bothIntOrUint = ctx.mkAnd(isIntOrUint0, isIntOrUint1); + // Fall back to 0 if the expression is neither an INT nor a UINT. + // This prevents Z3 from evaluating getUint() on a DOUBLE, which causes the OSS solver to enter + // an incomplete state. IntExpr val0 = (IntExpr) ctx.mkITE( - typeSystem.isInt(z3Expr0), typeSystem.getInt(z3Expr0), typeSystem.getUint(z3Expr0)); + typeSystem.isInt(z3Expr0), + typeSystem.getInt(z3Expr0), + ctx.mkITE(typeSystem.isUint(z3Expr0), typeSystem.getUint(z3Expr0), ctx.mkInt(0))); IntExpr val1 = (IntExpr) ctx.mkITE( - typeSystem.isInt(z3Expr1), typeSystem.getInt(z3Expr1), typeSystem.getUint(z3Expr1)); + typeSystem.isInt(z3Expr1), + typeSystem.getInt(z3Expr1), + ctx.mkITE(typeSystem.isUint(z3Expr1), typeSystem.getUint(z3Expr1), ctx.mkInt(0))); BoolExpr bothDouble = ctx.mkAnd(typeSystem.isDouble(z3Expr0), typeSystem.isDouble(z3Expr1)); + BoolExpr isIntOrUintAndDouble = ctx.mkAnd(isIntOrUint0, typeSystem.isDouble(z3Expr1)); + BoolExpr isDoubleAndIntOrUint = ctx.mkAnd(typeSystem.isDouble(z3Expr0), isIntOrUint1); + + Expr fpVal1 = typeSystem.getDouble(z3Expr1); + BoolExpr intDoubleEq = + ctx.mkAnd( + mkIsFiniteDouble(z3Expr1), + ctx.mkEq(ctx.mkInt2Real(val0), ctx.mkFPToReal((FPExpr) fpVal1))); + + Expr fpVal0 = typeSystem.getDouble(z3Expr0); + BoolExpr doubleIntEq = + ctx.mkAnd( + mkIsFiniteDouble(z3Expr0), + ctx.mkEq(ctx.mkFPToReal((FPExpr) fpVal0), ctx.mkInt2Real(val1))); + return (BoolExpr) CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) .addCase(bothIntOrUint, ctx.mkEq(val0, val1)) @@ -463,6 +492,8 @@ private BoolExpr getDynamicNumericEquality(Expr z3Expr0, Expr z3Expr1) { bothDouble, ctx.mkFPEq( (FPExpr) typeSystem.getDouble(z3Expr0), (FPExpr) typeSystem.getDouble(z3Expr1))) + .addCase(isIntOrUintAndDouble, intDoubleEq) + .addCase(isDoubleAndIntOrUint, doubleIntEq) .build(ctx.mkFalse()); } @@ -487,7 +518,7 @@ private BoolExpr unrollListEquality( TranslatedValue elemB = TranslatedValue.create(elem1, listB.listElementAt(i), typeSystem, listB.isApproximate()); - TranslatedValue elemEquality = translateEquals(elemA, elemB, ast); + TranslatedValue elemEquality = translateEquality(elemA, elemB, ast, /* isNotEquals= */ false); Expr eqZ3 = elemEquality.z3Expr(); BoolExpr isBool = typeSystem.isBool(eqZ3); @@ -504,10 +535,8 @@ private TranslatedValue translateEquality( Expr z3Arg0 = arg0.z3Expr(); Expr z3Arg1 = arg1.z3Expr(); - CelType type0 = - arg0.celExpr().map(node -> ast.getTypeOrThrow(node.id())).orElse(SimpleType.DYN); - CelType type1 = - arg1.celExpr().map(node -> ast.getTypeOrThrow(node.id())).orElse(SimpleType.DYN); + CelType type0 = extractAstTypeOrDefault(arg0, ast); + CelType type1 = extractAstTypeOrDefault(arg1, ast); BoolExpr equality; @@ -520,7 +549,8 @@ private TranslatedValue translateEquality( } else if (isStaticallyKnown(type0) && isStaticallyKnown(type1)) { equality = typeSystem.getStructuralEquality(z3Arg0, z3Arg1); } else { - BoolExpr bothNumeric = ctx.mkAnd(isNumeric(z3Arg0), isNumeric(z3Arg1)); + boolean canBeNumeric0 = type0.kind() == CelKind.DYN || isNumericType(type0); + boolean canBeNumeric1 = type1.kind() == CelKind.DYN || isNumericType(type1); // Check if one side is an explicit LIST that we can unroll BoolExpr structuralEq = typeSystem.getStructuralEquality(z3Arg0, z3Arg1); @@ -533,8 +563,13 @@ private TranslatedValue translateEquality( structuralEq); } - equality = - (BoolExpr) ctx.mkITE(bothNumeric, getNumericEquality(arg0, arg1, ast), structuralEq); + if (canBeNumeric0 && canBeNumeric1) { + BoolExpr bothNumeric = ctx.mkAnd(isNumeric(z3Arg0), isNumeric(z3Arg1)); + equality = + (BoolExpr) ctx.mkITE(bothNumeric, getNumericEquality(arg0, arg1, ast), structuralEq); + } else { + equality = structuralEq; + } } if (isNotEquals) { @@ -550,42 +585,16 @@ private TranslatedValue translateEquality( return TranslatedValue.create(finalResult, typeSystem, ctx.mkFalse()); } - BoolExpr bothIntOrUint = - ctx.mkAnd( - ctx.mkOr(typeSystem.isInt(z3Arg0), typeSystem.isUint(z3Arg0)), - ctx.mkOr(typeSystem.isInt(z3Arg1), typeSystem.isUint(z3Arg1))); - BoolExpr bothDouble = ctx.mkAnd(typeSystem.isDouble(z3Arg0), typeSystem.isDouble(z3Arg1)); - BoolExpr bothNumeric = ctx.mkAnd(isNumeric(z3Arg0), isNumeric(z3Arg1)); - BoolExpr sameNumericType = ctx.mkOr(bothIntOrUint, bothDouble); - - // crossNumeric equality is only an approximation if we rely on getDynamicNumericEquality. - // getNumericEqualityWithConstant is exact because it evaluates heterogeneous numeric equality - // accurately. - BoolExpr crossNumeric; - if (arg0.isNumericConstant() || arg1.isNumericConstant()) { - crossNumeric = ctx.mkFalse(); - } else { - crossNumeric = ctx.mkAnd(bothNumeric, ctx.mkNot(sameNumericType)); - } - return TranslatedValue.propagateStrict(ctx, typeSystem, equalityExpr, arg0, arg1) - .withApproximation(crossNumeric); - } - - private TranslatedValue translateEquals( - TranslatedValue arg0, TranslatedValue arg1, CelAbstractSyntaxTree ast) { - return translateEquality(arg0, arg1, ast, false); - } - - private TranslatedValue translateNotEquals( - TranslatedValue arg0, TranslatedValue arg1, CelAbstractSyntaxTree ast) { - return translateEquality(arg0, arg1, ast, true); + // Mathematically redundant, but needed to prevent exponentially branching Z3 logic tree of + // mkOr tracking exact unknowns and errors + .withApproximation(ctx.mkFalse()); } - private Expr buildListIndex(Expr lhsTrans, Expr rhsTrans) { + private Expr buildListIndex(Expr lhsTrans, Expr rhsTrans, BoolExpr typeGuard) { Expr listRef = typeSystem.getListRef(lhsTrans); SeqExpr seq = typeSystem.getSeq(listRef); - Expr index = ctx.mkApp(typeSystem.intCons().getAccessorDecls()[0], rhsTrans); + Expr index = typeSystem.getInt(rhsTrans); BoolExpr inBounds = ctx.mkAnd( ctx.mkGe((ArithExpr) index, ctx.mkInt(0)), @@ -593,30 +602,186 @@ private Expr buildListIndex(Expr lhsTrans, Expr rhsTrans) { Expr val = ctx.mkNth(seq, (ArithExpr) index); BoolExpr valNotError = ctx.mkNot(ctx.mkEq(val, typeSystem.mkError())); - constraintSink.accept(ctx.mkImplies(inBounds, valNotError)); + constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, inBounds), valNotError)); if (!allowUnknowns) { BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(val)); - constraintSink.accept(ctx.mkImplies(inBounds, valNotUnknown)); + constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, inBounds), valNotUnknown)); } return ctx.mkITE(inBounds, val, typeSystem.mkError()); } - private Expr buildMapIndex(Expr lhsTrans, Expr rhsTrans) { + private Optional extractIntNumSafe(Expr expr) { + Expr simplified = expr.simplify(); + + if (!simplified.isApp()) { + return Optional.empty(); + } + + FuncDecl decl = simplified.getFuncDecl(); + if (decl.equals(typeSystem.intCons().ConstructorDecl()) + || decl.equals(typeSystem.uintCons().ConstructorDecl())) { + return Optional.of(simplified.getArgs()[0]) + .filter(IntNum.class::isInstance) + .map(IntNum.class::cast) + .map(IntNum::getInt64); + } + + return Optional.empty(); + } + + private static final class ProbeResult { + final BoolExpr altInMap; + final Expr altVal; + + ProbeResult(BoolExpr altInMap, Expr altVal) { + this.altInMap = altInMap; + this.altVal = altVal; + } + } + + private ProbeResult createProbeResult( + BoolExpr inMapOrig, + Expr valOrig, + BoolExpr cond1, + Expr key1, + BoolExpr cond2, + Expr key2, + ArrayExpr mapPresence, + ArrayExpr mapValues) { + BoolExpr inMap1 = (BoolExpr) ctx.mkSelect(mapPresence, key1); + Expr val1 = ctx.mkSelect(mapValues, key1); + BoolExpr inMap2 = (BoolExpr) ctx.mkSelect(mapPresence, key2); + Expr val2 = ctx.mkSelect(mapValues, key2); + + BoolExpr altInMap = ctx.mkOr(inMapOrig, ctx.mkAnd(cond1, inMap1), ctx.mkAnd(cond2, inMap2)); + Expr altVal = + ctx.mkITE( + inMapOrig, + valOrig, + ctx.mkITE( + ctx.mkAnd(cond1, inMap1), + val1, + ctx.mkITE(ctx.mkAnd(cond2, inMap2), val2, valOrig))); + + return new ProbeResult(altInMap, altVal); + } + + private Expr buildMapIndex(Expr lhsTrans, Expr rhsTrans, BoolExpr typeGuard) { Expr mapRef = typeSystem.getMapRef(lhsTrans); ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef); ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef); - BoolExpr inMap = (BoolExpr) ctx.mkSelect(mapPresence, rhsTrans); - Expr val = ctx.mkSelect(mapValues, rhsTrans); - BoolExpr valNotError = ctx.mkNot(ctx.mkEq(val, typeSystem.mkError())); - constraintSink.accept(ctx.mkImplies(inMap, valNotError)); + BoolExpr inMapOrig = (BoolExpr) ctx.mkSelect(mapPresence, rhsTrans); + Expr valOrig = ctx.mkSelect(mapValues, rhsTrans); + + BoolExpr isInt = typeSystem.isInt(rhsTrans); + BoolExpr isUint = typeSystem.isUint(rhsTrans); + BoolExpr isDouble = typeSystem.isDouble(rhsTrans); + + // Int probes + IntExpr rawInt = (IntExpr) ctx.mkITE(isInt, typeSystem.getInt(rhsTrans), ctx.mkInt(0)); + BoolExpr intHasUint = ctx.mkGe(rawInt, ctx.mkInt(0)); + Expr intUintKey = typeSystem.wrapUint(rawInt); + + FPExpr intFp; + BoolExpr intHasDouble; + Optional intNum = extractIntNumSafe(rhsTrans); + if (intNum.isPresent()) { + double d = (double) intNum.get(); + intFp = typeSystem.mkFpDouble(d); + intHasDouble = isInt; + } else { + intFp = typeSystem.mkFpDouble(0.0); + intHasDouble = ctx.mkFalse(); + } + Expr intDoubleKey = typeSystem.wrapDouble(intFp); + ProbeResult intProbe = + createProbeResult( + inMapOrig, + valOrig, + intHasUint, + intUintKey, + intHasDouble, + intDoubleKey, + mapPresence, + mapValues); + + // Uint probes + IntExpr rawUint = (IntExpr) ctx.mkITE(isUint, typeSystem.getUint(rhsTrans), ctx.mkInt(0)); + BoolExpr uintHasInt = ctx.mkLe(rawUint, ctx.mkInt(CelZ3TypeSystem.MAX_INT64)); + Expr uintIntKey = typeSystem.wrapInt(rawUint); + + FPExpr uintFp; + BoolExpr uintHasDouble; + Optional uintNum = extractIntNumSafe(rhsTrans); + if (uintNum.isPresent()) { + double d = (double) uintNum.get(); + uintFp = typeSystem.mkFpDouble(d); + uintHasDouble = isUint; + } else { + uintFp = typeSystem.mkFpDouble(0.0); + uintHasDouble = ctx.mkFalse(); + } + Expr uintDoubleKey = typeSystem.wrapDouble(uintFp); + ProbeResult uintProbe = + createProbeResult( + inMapOrig, + valOrig, + uintHasInt, + uintIntKey, + uintHasDouble, + uintDoubleKey, + mapPresence, + mapValues); + + // Double probes + FPExpr dVal = + (FPExpr) + (Expr) ctx.mkITE(isDouble, typeSystem.getDouble(rhsTrans), typeSystem.mkFpDouble(0.0)); + IntExpr dInt = ctx.mkReal2Int(ctx.mkFPToReal(dVal)); + BoolExpr doubleIsExact = + ctx.mkAnd( + isDouble, + ctx.mkNot(ctx.mkOr(ctx.mkFPIsNaN(dVal), ctx.mkFPIsInfinite(dVal))), + ctx.mkEq(ctx.mkInt2Real(dInt), ctx.mkFPToReal(dVal))); + Expr doubleIntKey = typeSystem.wrapInt(dInt); + Expr doubleUintKey = typeSystem.wrapUint(dInt); + BoolExpr doubleHasUint = ctx.mkAnd(doubleIsExact, ctx.mkGe(dInt, ctx.mkInt(0))); + ProbeResult doubleProbe = + createProbeResult( + inMapOrig, + valOrig, + doubleIsExact, + doubleIntKey, + doubleHasUint, + doubleUintKey, + mapPresence, + mapValues); + + BoolExpr finalInMap = + (BoolExpr) + CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + .addCase(isInt, intProbe.altInMap) + .addCase(isUint, uintProbe.altInMap) + .addCase(isDouble, doubleProbe.altInMap) + .build(inMapOrig); + + Expr finalVal = + CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + .addCase(isInt, intProbe.altVal) + .addCase(isUint, uintProbe.altVal) + .addCase(isDouble, doubleProbe.altVal) + .build(valOrig); + + BoolExpr valNotError = ctx.mkNot(ctx.mkEq(finalVal, typeSystem.mkError())); + constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, finalInMap), valNotError)); if (!allowUnknowns) { - BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(val)); - constraintSink.accept(ctx.mkImplies(inMap, valNotUnknown)); + BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(finalVal)); + constraintSink.accept(ctx.mkImplies(ctx.mkAnd(typeGuard, finalInMap), valNotUnknown)); } - return ctx.mkITE(inMap, val, typeSystem.mkError()); + return ctx.mkITE(finalInMap, finalVal, typeSystem.mkError()); } private TranslatedValue translateIndex(List args, CelAbstractSyntaxTree ast) { @@ -630,24 +795,24 @@ private TranslatedValue translateIndex(List args, CelAbstractSy Expr actualValue; if (lhsType.kind() == CelKind.LIST && rhsType.kind() == CelKind.INT) { - actualValue = buildListIndex(lhsTrans, rhsTrans); + actualValue = buildListIndex(lhsTrans, rhsTrans, ctx.mkTrue()); constraintSink.accept( ctx.mkImplies( ctx.mkNot(typeSystem.isError(actualValue)), typeConstraintGenerator.apply(actualValue, ((ListType) lhsType).elemType()))); } else if (lhsType.kind() == CelKind.MAP) { - actualValue = buildMapIndex(lhsTrans, rhsTrans); + actualValue = buildMapIndex(lhsTrans, rhsTrans, ctx.mkTrue()); constraintSink.accept( ctx.mkImplies( ctx.mkNot(typeSystem.isError(actualValue)), typeConstraintGenerator.apply(actualValue, ((MapType) lhsType).valueType()))); } else { + BoolExpr isListGuard = ctx.mkAnd(typeSystem.isList(lhsTrans), typeSystem.isInt(rhsTrans)); + BoolExpr isMapGuard = typeSystem.isMap(lhsTrans); actualValue = CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase( - ctx.mkAnd(typeSystem.isList(lhsTrans), typeSystem.isInt(rhsTrans)), - buildListIndex(lhsTrans, rhsTrans)) - .addCase(typeSystem.isMap(lhsTrans), buildMapIndex(lhsTrans, rhsTrans)) + .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard)) + .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard)) .build(typeSystem.mkError()); } diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index 7bd6d0daf..c5eae2c76 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -769,10 +769,6 @@ private SwitchBuilder(Context ctx) { * *

Returns {@code false} if the list is empty. */ - public static BoolExpr mkOrFlattened(Context ctx, BoolExpr... args) { - return mkOrFlattened(ctx, Arrays.asList(args)); - } - public static BoolExpr mkOrFlattened(Context ctx, List args) { // Pruning true/false constants in Java is significantly faster than building // larger ASTs and letting Z3 process them natively. diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java index 5b7fdba3a..fc4757686 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java @@ -24,9 +24,7 @@ import dev.cel.common.types.OptionalType; import dev.cel.common.types.SimpleType; import dev.cel.verifier.CelZ3TypeSystem; -import java.util.List; import java.util.Optional; -import java.util.function.Consumer; /** Axiomatization for CEL's type() function. */ final class TypeAxiom { @@ -38,30 +36,21 @@ final class TypeAxiom { CelZ3FunctionAxiom.newBuilder(StandardFunction.TYPE.functionDecl()) .addOverloadTranslator( StandardFunction.Overload.InternalOperator.TYPE.celOverloadDecl(), - new CelZ3OverloadTranslator() { - @Override - public Optional translate( - Context ctx, - CelZ3TypeSystem typeSystem, - Consumer constraintSink, - List> unwrappedArgs, - List argApproximations) { - Preconditions.checkArgument(unwrappedArgs.size() == 1); - Preconditions.checkArgument(argApproximations.size() == 1); + (ctx, typeSystem, constraintSink, unwrappedArgs, argApproximations) -> { + Preconditions.checkArgument(unwrappedArgs.size() == 1); + Preconditions.checkArgument(argApproximations.size() == 1); - Expr val = unwrappedArgs.get(0); - BoolExpr argApprox = argApproximations.get(0); + Expr val = unwrappedArgs.get(0); + BoolExpr argApprox = argApproximations.get(0); - Expr result = getTypeExpression(ctx, typeSystem, val); + Expr result = getTypeExpression(ctx, typeSystem, val); - // Custom approximation logic for type(): it is only approximate if the argument - // is approximate AND the argument is an Error or Unknown. - BoolExpr isErrOrUnk = - ctx.mkOr(typeSystem.isError(val), typeSystem.isUnknown(val)); - BoolExpr typeApprox = ctx.mkAnd(argApprox, isErrOrUnk); + // Custom approximation logic for type(): it is only approximate if the argument + // is approximate AND the argument is an Error or Unknown. + BoolExpr isErrOrUnk = ctx.mkOr(typeSystem.isError(val), typeSystem.isUnknown(val)); + BoolExpr typeApprox = ctx.mkAnd(argApprox, isErrOrUnk); - return Optional.of(CelZ3OverloadResult.create(result, typeApprox)); - } + return Optional.of(CelZ3OverloadResult.create(result, typeApprox)); }) .build(); diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java index 741513daf..94bdf0651 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java @@ -95,8 +95,7 @@ final class TypeConversionAxioms { true) .addUnaryOverloadTranslator( Conversions.STRING_TO_DOUBLE.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_DOUBLE), - true) + createUninterpretedConversion(Conversions.STRING_TO_DOUBLE)) .build(); private static final CelZ3FunctionAxiom STRING_AXIOM = diff --git a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java index a5567c1f1..2bc500bde 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java @@ -277,7 +277,7 @@ public void verifyEquivalence_violation_throws() throws Exception { assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); assertThat(result.message()) .containsMatch( - "Equivalence violation detected\\. Counterexample input:\\n x = (6|7|8|9|10)"); + "Equivalence violation detected\\. Counterexample input:\\n {2}x = (6|7|8|9|10)"); } @Test diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 5c13cc8de..9592153ed 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -266,6 +266,7 @@ private enum IsAlwaysTrueTestCase { UINT_ARITHMETIC_ZERO("0u + 0u == 0u"), MAP_COMPREHENSION("{1: 2, 3: 4}.all(k, k > 0)"), NESTED_COMPREHENSIONS("[1, 2].all(x, [3, 4].all(y, x < y || y <= x))"), + CYCLIC_BIND_DOES_NOT_HANG("cel.bind(x, x, x) == x"), CEL_BIND_SHADOWING("cel.bind(x, 1, cel.bind(x, 2, x) + x) == 3"), CEL_BIND_TO_TRUE("cel.bind(x, true, !x) == false"), CEL_BIND_TO_FALSE("cel.bind(x, false, !x) == true"), @@ -460,7 +461,14 @@ private enum IsAlwaysTrueTestCase { HETEROGENEOUS_INT_UINT_GE("2 >= 1u"), HETEROGENEOUS_UINT_INT_GE("2u >= 1"), HETEROGENEOUS_INT_DOUBLE_PRECISION("9007199254740993 > 9007199254740992.0"), - CYCLIC_BIND_DOES_NOT_HANG("cel.bind(x, x, x) == x"), + HETEROGENEOUS_INT_EQ_DOUBLE( + "type(dyn_var) == int && type(dyn_var2) == double && dyn_var == 1 && dyn_var2 == 1.0 ?" + + " dyn_var == dyn_var2 : true"), + HETEROGENEOUS_INT_NEQ_DOUBLE( + "type(dyn_var) == int && type(dyn_var2) == double && dyn_var == 1 && dyn_var2 == 1.5 ?" + + " dyn_var != dyn_var2 : true"), + HETEROGENEOUS_INF_VS_INT("dyn_var == 9223372036854775807 ? dyn_var != 1.0 / 0.0 : true"), + HETEROGENEOUS_NAN_VS_INT("dyn_var == 1 ? dyn_var != 0.0 / 0.0 : true"), HETEROGENEOUS_INT_UINT_VARIABLE_EQ("unknown_var == 1u ? unknown_var == 1 : true"), HETEROGENEOUS_INT_UINT_VARIABLE_VARIABLE_EQ( "unknown_var == u && x == 1 && u == 1u ? unknown_var == x : true"), @@ -469,6 +477,32 @@ private enum IsAlwaysTrueTestCase { HETEROGENEOUS_INT_UINT_VARIABLE_NEQ("unknown_var == 2u ? unknown_var != 1 : true"), HETEROGENEOUS_DOUBLE_INT_OVERFLOW( "unknown_var == 9223372036854775807 ? unknown_var != 1e100 : true"), + HETEROGENEOUS_MAX_EXACT_INT("dyn(9007199254740992) == 9007199254740992.0"), + HETEROGENEOUS_MIN_EXACT_INT("dyn(-9007199254740992) == -9007199254740992.0"), + HETEROGENEOUS_INT_PRECISION_LOSS_POS("dyn(9007199254740993) != 9007199254740992.0"), + HETEROGENEOUS_INT_PRECISION_LOSS_NEG("dyn(-9007199254740993) != -9007199254740992.0"), + HETEROGENEOUS_UINT_PRECISION_LOSS("dyn(9007199254740993u) != 9007199254740992.0"), + HETEROGENEOUS_LONG_MAX_VS_DOUBLE("dyn(9223372036854775807) == 9223372036854775808.0"), + HETEROGENEOUS_LONG_MIN_VS_DOUBLE("dyn(-9223372036854775808) == -9223372036854775808.0"), + HETEROGENEOUS_UINT_MAX_VS_DOUBLE("dyn(18446744073709551615u) != 18446744073709551616.0"), + HETEROGENEOUS_DYNAMIC_PRECISION( + "type(dyn_var) == int && type(dyn_var2) == double && dyn_var == 9007199254740993 &&" + + " dyn_var2 == 9007199254740992.0 ? dyn_var != dyn_var2 : true"), + HETEROGENEOUS_DYNAMIC_TRANSITIVITY( + "type(dyn_var) == int && type(dyn_var2) == double && dyn_var == 1 && dyn_var2 == 1.0 ?" + + " dyn_var == dyn_var2 : true"), + HETEROGENEOUS_DYNAMIC_ZERO("type(dyn_var) == double && dyn_var == -0.0 ? dyn_var == 0 : true"), + HETEROGENEOUS_MAP_INT_KEY_DOUBLE_LOOKUP("{1: 'a'}[dyn(1.0)] == 'a'"), + HETEROGENEOUS_MAP_DOUBLE_KEY_INT_LOOKUP("{1.0: 'a'}[dyn(1)] == 'a'"), + HETEROGENEOUS_MAP_DOUBLE_KEY_UINT_LOOKUP("{1.0: 'a'}[dyn(1u)] == 'a'"), + HETEROGENEOUS_MAP_UINT_KEY_DOUBLE_LOOKUP("{1u: 'a'}[dyn(1.0)] == 'a'"), + HETEROGENEOUS_MAP_UINT_KEY_INT_LOOKUP_ZERO("{0u: 'a'}[dyn(0)] == 'a'"), + HETEROGENEOUS_MAP_UINT_KEY_DOUBLE_LOOKUP_ZERO("{0u: 'a'}[dyn(0.0)] == 'a'"), + HETEROGENEOUS_MAP_DOUBLE_KEY_UINT_LOOKUP_ZERO("{0.0: 'a'}[dyn(0u)] == 'a'"), + HETEROGENEOUS_MAP_INT_KEY_UINT_LOOKUP_ZERO("{0: 'a'}[dyn(0u)] == 'a'"), + HETEROGENEOUS_MAP_PRECISION_MISS( + "{9007199254740993: 'exact', 9007199254740992: 'rounded'}[dyn(9007199254740992.0)] ==" + + " 'rounded'"), DYNAMIC_LIST_RESOLVES_QUANTIFIER_LOOPS( "int_list == [1] ? !(int_list.all(x, int_list.exists(y, y == x + 1))) : true"), DYNAMIC_LIST_RESOLVES_PIGEONHOLE( @@ -493,10 +527,6 @@ private enum IsAlwaysTrueTestCase { "string_int_map == {'a': 1} ? string_int_map.map(k, k) == ['a'] : true"), UINT_SUBTRACT("3u - 2u == 1u"), DOUBLE_SUBTRACT("3.0 - 2.0 == 1.0"), - // TODO: Cross-type numeric equality evaluates to strictly false, causing this - // test's condition to become a tautology. - // CROSS_TYPE_DYNAMIC_EQUALITY_NOT_ALWAYS_UNEQUAL_INT_DOUBLE( - // "!(request == unknown_var && type(request) == int && type(unknown_var) == double)"), DYNAMIC_LIST_V2_ALL("int_list == [1, 2] ? int_list.all(i, v, v > 0 && i >= 0) : true"), DYNAMIC_LIST_V2_EXISTS("int_list == [1, 2] ? int_list.exists(i, v, i == 0 && v == 1) : true"), DYNAMIC_MAP_V2_ALL( @@ -838,8 +868,6 @@ public void verifyEquivalence_unconditionalError_failsVerification( + " input state)"); } - - @Test public void verifyEquivalence_dynamicMapEquality_enforcesExtensionalityOnPresentKeys() throws Exception { @@ -883,8 +911,6 @@ private enum MalformedAstTestCase { } } - - @Test public void isAlwaysTrue_malformedAst_throwsIllegalArgumentException( @TestParameter MalformedAstTestCase testCase) throws Exception { @@ -937,6 +963,10 @@ private enum IsAlwaysTrueViolationTestCase { "dyn(x) != dyn(u)", "Condition is not always true."), CROSS_TYPE_SYMBOLIC_EQUALITY_NOT_ALWAYS_UNEQUAL_UINT_INT( "dyn(u) != dyn(x)", "Condition is not always true."), + CROSS_TYPE_DYNAMIC_EQUALITY_NOT_ALWAYS_UNEQUAL_INT_DOUBLE( + "!(request == unknown_var && type(request) == int && type(unknown_var) == double)", + "Condition is not always true.", + "Counterexample input:"), DYNAMIC_MAP_ALL_VIOLATION( "string_int_map == {'a': 1, 'b': 2} ? string_int_map.all(k, k == 'a') : true", "Condition is not always true.", @@ -1404,8 +1434,8 @@ public void verifyEquivalence_violation_hasCounterexampleMessage() throws Except assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); String message = result.message(); assertThat(message).contains("Equivalence violation detected. Counterexample input:"); - assertThat(message).containsMatch(" x = -?\\d+"); - assertThat(message).containsMatch(" y = -?\\d+"); + assertThat(message).containsMatch(" {2}x = -?\\d+"); + assertThat(message).containsMatch(" {2}y = -?\\d+"); } @Test @@ -1420,7 +1450,6 @@ public void verifyEquivalence_divergesOnTernaryErrorSemantics() throws Exception assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); } - @Test public void verifyEquivalence_dynamicIndexingWithExplicitMap_hydratesMap() throws Exception { CelAbstractSyntaxTree astA = @@ -1433,7 +1462,7 @@ public void verifyEquivalence_dynamicIndexingWithExplicitMap_hydratesMap() throw assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); assertThat(result.message()).contains("string_int_list_map = {"); assertThat(result.message()).contains("\"a\": [1, 2]"); - assertThat(result.message()).containsMatch("\"b\": \\[3, [45]\\]"); + assertThat(result.message()).containsMatch("\"b\": \\[3, [45]]"); } @Test @@ -1605,7 +1634,8 @@ public void verifyEquivalence_counterexampleFormat( result .message() .matches( - "(?s).*Equivalence violation detected\\. Counterexample input:\n " + "(?s).*Equivalence violation detected\\. Counterexample input:\n" + + " {2}" + f + ".*")); assertWithMessage(result.message()).that(matched).isTrue(); @@ -1952,7 +1982,7 @@ public void addFunctionAxioms_duplicateFunctionNames_throwsException() throws Ex .addFunctionAxioms(ImmutableList.of(dummyAxiom1, dummyAxiom2)); IllegalArgumentException exception = - assertThrows(IllegalArgumentException.class, () -> builder.build()); + assertThrows(IllegalArgumentException.class, builder::build); assertThat(exception).hasMessageThat().contains("dummy_func"); }