diff --git a/verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java b/verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java index 5e2a0a8ec..11a78fcbe 100644 --- a/verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java +++ b/verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java @@ -476,7 +476,11 @@ private static int compareIdent(String name1, String name2, CanonicalizationScop if (bIdx2 >= 0) { return 1; // Free variable comes after bound variable } - return name1.compareTo(name2); + return stripLeadingDot(name1).compareTo(stripLeadingDot(name2)); + } + + private static String stripLeadingDot(String name) { + return name.startsWith(".") ? name.substring(1) : name; } private int compareSelect(CelMutableSelect s1, CelMutableSelect s2) { diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java b/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java index 31a7e3b2a..f518caf99 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java @@ -21,8 +21,10 @@ import com.google.common.hash.HashFunction; import com.google.common.hash.Hasher; import com.google.common.hash.Hashing; +import dev.cel.common.CelAbstractSyntaxTree; import dev.cel.common.ast.CelConstant; import dev.cel.common.ast.CelExpr; +import dev.cel.common.ast.CelReference; import java.util.ArrayList; import java.util.HashMap; import java.util.List; @@ -65,14 +67,21 @@ static AlphaSignature create(long staticHash, ImmutableList freeVariabl } } - static AlphaSignature computeSignature(CelExpr expr) { - HasherContext context = new HasherContext(HASH_FUNCTION); + static AlphaSignature computeSignature(CelExpr expr, CelAbstractSyntaxTree ast) { + HasherContext context = new HasherContext(HASH_FUNCTION, ast); hashAst(expr, /* scope= */ null, context); return AlphaSignature.create( context.hasher.hash().asLong(), ImmutableList.copyOf(context.freeVars)); } private static void hashAst(CelExpr expr, @Nullable Scope scope, HasherContext context) { + CelConstant refValue = + context.ast.getReference(expr.id()).flatMap(CelReference::value).orElse(null); + if (refValue != null) { + context.hasher.putString(CelExpr.ExprKind.Kind.CONSTANT.name(), UTF_8); + hashConstant(refValue, context); + return; + } context.hasher.putString(expr.exprKind().getKind().name(), UTF_8); switch (expr.exprKind().getKind()) { case CONSTANT: @@ -85,11 +94,12 @@ private static void hashAst(CelExpr expr, @Nullable Scope scope, HasherContext c context.hasher.putByte((byte) 0); // 0 = bound context.hasher.putInt(bIdx); } else { - Integer fIdx = context.freeVarIndices.get(name); + String freeName = name.startsWith(".") ? name.substring(1) : name; + Integer fIdx = context.freeVarIndices.get(freeName); if (fIdx == null) { context.freeVars.add(expr); fIdx = context.freeVars.size() - 1; - context.freeVarIndices.put(name, fIdx); + context.freeVarIndices.put(freeName, fIdx); } context.hasher.putByte((byte) 1); // 1 = free context.hasher.putInt(fIdx); @@ -205,11 +215,13 @@ private static void hashConstant(CelConstant constant, HasherContext context) { private static final class HasherContext { final Hasher hasher; + final CelAbstractSyntaxTree ast; final Map freeVarIndices = new HashMap<>(); final List freeVars = new ArrayList<>(); - HasherContext(HashFunction hashFunction) { + HasherContext(HashFunction hashFunction, CelAbstractSyntaxTree ast) { this.hasher = hashFunction.newHasher(); + this.ast = ast; } } diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index db344960b..7cada2186 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -33,6 +33,7 @@ import dev.cel.common.ast.CelExpr; import dev.cel.common.ast.CelExpr.CelList; import dev.cel.common.ast.CelExpr.ExprKind; +import dev.cel.common.ast.CelReference; import dev.cel.common.types.CelKind; import dev.cel.common.types.CelType; import dev.cel.common.types.CelTypeProvider; @@ -223,6 +224,10 @@ private TranslatedValue translateConstant(CelExpr celExpr) { private TranslatedValue translateIdent(CelExpr celExpr, CelAbstractSyntaxTree ast) { CelExpr.CelIdent ident = celExpr.ident(); long exprId = celExpr.id(); + CelConstant refValue = ast.getReference(exprId).flatMap(CelReference::value).orElse(null); + if (refValue != null) { + return translateConstant(CelExpr.ofConstant(exprId, refValue)); + } String name = ident.name(); CelType type = ast.getTypeOrThrow(exprId); if (type instanceof TypeType) { @@ -244,7 +249,7 @@ private TranslatedValue translateIdent(CelExpr celExpr, CelAbstractSyntaxTree as context.addConstraint(ctx.mkNot(typeSystem.isError(v))); BoolExpr constraint = typeConstraintGenerator.createTypeConstraint(v, exprId, ast); - if (unknownIdentifiers.contains(name)) { + if (unknownIdentifiers.contains(n)) { context.addConstraint(ctx.mkOr(typeSystem.isUnknown(v), constraint)); } else { context.addConstraint(ctx.mkNot(typeSystem.isUnknown(v))); diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java index df34f00aa..79bcd0e42 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java @@ -508,7 +508,7 @@ private IterationElement(Expr keyOrIndex, Expr value) { } private Expr mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast) { - CelAstAlphaHasher.AlphaSignature sig = CelAstAlphaHasher.computeSignature(expr); + CelAstAlphaHasher.AlphaSignature sig = CelAstAlphaHasher.computeSignature(expr, ast); ImmutableList.Builder> smtArgs = ImmutableList.builder(); for (CelExpr freeVar : sig.freeVariables()) { diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java index 70193017a..8e52da1b9 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java @@ -42,6 +42,7 @@ final class CelZ3TranslationContext { private final Map, CelType> inputVariableTypes; private final List truncationConditions; private final Map symbolTable; + private final Map localScope; Context ctx() { return ctx; @@ -108,28 +109,32 @@ BoolExpr hasTruncation() { } void bindSymbol(String name, TranslatedValue value) { - symbolTable.put(name, value); + localScope.put(name, value); } Optional lookupSymbol(String name) { - return Optional.ofNullable(symbolTable.get(name)); + return Optional.ofNullable(localScope.get(name)); } TranslatedValue computeSymbolIfAbsent( - String name, Function mappingFunction) { - return symbolTable.computeIfAbsent(name, mappingFunction); + String rawName, Function mappingFunction) { + if (!rawName.startsWith(".") && localScope.containsKey(rawName)) { + return localScope.get(rawName); + } + return symbolTable.computeIfAbsent( + rawName.startsWith(".") ? rawName.substring(1) : rawName, mappingFunction); } /** Binds {@code varName} to {@code value} while running {@code action}, then restores it. */ T withScope(String varName, TranslatedValue value, Supplier action) { - TranslatedValue prev = symbolTable.put(varName, value); + TranslatedValue prev = localScope.put(varName, value); try { return action.get(); } finally { if (prev != null) { - symbolTable.put(varName, prev); + localScope.put(varName, prev); } else { - symbolTable.remove(varName); + localScope.remove(varName); } } } @@ -144,5 +149,6 @@ T withScope(String varName, TranslatedValue value, Supplier action) { this.inputVariableTypes = new LinkedHashMap<>(); this.truncationConditions = new ArrayList<>(); this.symbolTable = new HashMap<>(); + this.localScope = new HashMap<>(); } } diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index dd5254631..4438b4245 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -36,6 +36,7 @@ import dev.cel.common.CelFunctionDecl; import dev.cel.common.CelOptions; import dev.cel.common.CelOverloadDecl; +import dev.cel.common.CelVarDecl; import dev.cel.common.Operator; import dev.cel.common.ast.CelConstant; import dev.cel.common.ast.CelExpr; @@ -613,6 +614,8 @@ private enum IsUnsatisfiableTestCase { "size(string_int_map) == 6 && dyn(1) in string_int_map"), LIST_INDEX_DYN_STRING_KEY("int_list[dyn('0')] == 1"), NON_BOOL_LOGICAL_OPERAND("dyn(1) && true"), + ENUM_CONSTANTS_DISTINCT("TestAllTypes.NestedEnum.FOO == TestAllTypes.NestedEnum.BAR"), + LEADING_DOT_GLOBAL_DISAMBIGUATION_CONTRADICTION("x == 5 && [1, 2].all(x, x > .x)"), ; private final String expr; @@ -1114,6 +1117,9 @@ private enum IsAlwaysTrueTestCase { "size(string_int_map) > 0 && size(string_int_map) <= 5 ?" + " string_int_map.all(k, v, v >= -9223372036854775808 &&" + " v <= 9223372036854775807) : true"), + ENUM_CONSTANT_EQUALITY("TestAllTypes.NestedEnum.BAR == 1"), + ENUM_CONSTANT_INEQUALITY("TestAllTypes.NestedEnum.FOO != TestAllTypes.NestedEnum.BAR"), + LEADING_DOT_GLOBAL_DISAMBIGUATION_IN_COMPREHENSION("x == 0 ? [1, 2].all(x, x > .x) : true"), ; final String expr; @@ -2452,7 +2458,19 @@ private enum EquivalenceTestCase { + " && z_key == 'foo')"), CANONICALIZE_CEL_BIND_ALPHA_RENAME_PREDICATE_ORDER( "cel.bind(a, x + 10, cel.bind(b, x + 20, 2 == b && 1 == a))", - "cel.bind(c, x + 10, cel.bind(d, x + 20, c == 1 && d == 2))"); + "cel.bind(c, x + 10, cel.bind(d, x + 20, c == 1 && d == 2))"), + ENUM_FIELD_COMPARE_VS_INT_LITERAL( + "test_all_types.single_nested_enum == TestAllTypes.NestedEnum.BAR", + "test_all_types.single_nested_enum == 1"), + LEADING_DOT_GLOBAL_DISAMBIGUATION("[1, 2].all(x, x > .x) && x == 0", "x == 0"), + TRUNCATED_COMPREHENSION_ENUM_VS_INT_LITERAL( + "dyn_list.all(e, e == TestAllTypes.NestedEnum.BAR)", "dyn_list.all(e, e == 1)"), + TRUNCATED_COMPREHENSION_LEADING_DOT_VS_UNSHADOWED( + "int_list.all(y, (.y == x) && y > 0 && [1].all(x, .x > 0 && .y > 0))", + "int_list.all(z, (y == x) && z > 0 && [1].all(w, x > 0 && y > 0))"), + TRUNCATED_COMPREHENSION_SHADOWED_CEL_BIND( + "cel.bind(x, x + 1, int_list.all(e, e > x && a))", + "cel.bind(x, x + 1, int_list.all(v, a && v > x))"); private final String exprA; private final String exprB; @@ -3593,8 +3611,8 @@ private enum EquivalenceZeroUnrollLimitTestCase { DIFFERENT_CONSTANTS("dyn_list.exists(i, i == 1)", "dyn_list.exists(i, i == 2)"), DIFFERENT_VARIABLES("dyn_list.exists(i, i == x)", "dyn_list.exists(i, i == y)"); - final String exprA; - final String exprB; + private final String exprA; + private final String exprB; EquivalenceZeroUnrollLimitTestCase(String exprA, String exprB) { this.exprA = exprA; @@ -3607,9 +3625,9 @@ public void verifyEquivalence_zeroUnrollLimit_returnsInconclusive( @TestParameter EquivalenceZeroUnrollLimitTestCase testCase) throws Exception { CelAbstractSyntaxTree astA = CEL.compile(testCase.exprA).getAst(); CelAbstractSyntaxTree astB = CEL.compile(testCase.exprB).getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build(); + CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); @@ -3632,8 +3650,8 @@ private enum EquivalenceZeroUnrollLimitVerifiedTestCase { "string_int_map.exists(z_key, a_val, int_list.all(idx, elem, idx == 0 && elem == a_val)" + " && z_key == 'foo')"); - final String exprA; - final String exprB; + private final String exprA; + private final String exprB; EquivalenceZeroUnrollLimitVerifiedTestCase(String exprA, String exprB) { this.exprA = exprA; @@ -3646,9 +3664,9 @@ public void verifyEquivalence_zeroUnrollLimit_twoVarComprehensions_returnsVerifi @TestParameter EquivalenceZeroUnrollLimitVerifiedTestCase testCase) throws Exception { CelAbstractSyntaxTree astA = CEL.compile(testCase.exprA).getAst(); CelAbstractSyntaxTree astB = CEL.compile(testCase.exprB).getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build(); + CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertWithMessage(result.message()) @@ -3673,7 +3691,6 @@ public void verifyEquivalence_comprehensionScopeShadowing_returnsInconclusive() exprFactory.newBoolLiteral(true), /* step= */ exprFactory.newIdentifier("x"), /* result= */ exprFactory.newIdentifier("x")))); - CelMacro macro2 = CelMacro.newReceiverMacro( "my_macro_2", @@ -3689,18 +3706,16 @@ public void verifyEquivalence_comprehensionScopeShadowing_returnsInconclusive() exprFactory.newBoolLiteral(true), /* step= */ exprFactory.newIdentifier("y"), /* result= */ exprFactory.newIdentifier("x")))); - Cel customCel = CelFactory.plannerCelBuilder() .addVar("dyn_list", ListType.create(SimpleType.DYN)) .addMacros(macro1, macro2) .build(); - CelAbstractSyntaxTree astA = customCel.compile("dyn_list.my_macro_1(true)").getAst(); CelAbstractSyntaxTree astB = customCel.compile("dyn_list.my_macro_2(true)").getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier(customCel).setComprehensionUnrollLimit(0).build(); + CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); @@ -3730,7 +3745,6 @@ public void verifyEquivalence_comprehensionResultScopeIsolation_returnsInconclus exprFactory.newIntLiteral(0L)), exprFactory.newIntLiteral(0L), exprFactory.newIdentifier("x"))))); - Cel customCel = CelFactory.plannerCelBuilder() .addVar("dyn_list", ListType.create(SimpleType.DYN)) @@ -3738,14 +3752,13 @@ public void verifyEquivalence_comprehensionResultScopeIsolation_returnsInconclus .addMacros(macro) .addCompilerLibraries(CelExtensions.bindings()) .build(); - CelAbstractSyntaxTree astA = customCel.compile("cel.bind(x, 10, dyn_list.my_macro(1))").getAst(); CelAbstractSyntaxTree astB = customCel.compile("cel.bind(x, 20, dyn_list.my_macro(1))").getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier(customCel).setComprehensionUnrollLimit(0).build(); + CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); @@ -3760,10 +3773,8 @@ public void verifyEquivalence_timeoutReached_throwsCelVerificationException() th .addVar("d3", SimpleType.DOUBLE) .addVar("d4", SimpleType.DOUBLE) .build(); - CelVerifier timeoutVerifier = CelVerifierFactory.newVerifier(customCel).setTimeout(Duration.ofMillis(1)).build(); - CelAbstractSyntaxTree astA = customCel .compile( @@ -3775,6 +3786,7 @@ public void verifyEquivalence_timeoutReached_throwsCelVerificationException() th CelVerificationException e = assertThrows( CelVerificationException.class, () -> timeoutVerifier.verifyEquivalence(astA, astB)); + assertThat(e).hasMessageThat().containsMatch("timeout|canceled"); } @@ -3783,9 +3795,9 @@ public void verifyImplication_loopExceedsLimit_returnsTruncatedInconclusive() th CelAbstractSyntaxTree assumeAst = CEL.compile("size(int_list) <= 2 && int_list[0] > 0 && int_list[1] > 0").getAst(); CelAbstractSyntaxTree assertAst = CEL.compile("int_list.all(x, x > 0)").getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(2).build(); + CelVerificationResult result = ((CelVerifierZ3Impl) verifier) .verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Implication"); @@ -3801,12 +3813,38 @@ public void verifyImplication_symbolicNan_crossNumericComparisonReturnsFalse() t 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(CEL).build(); + CelVerificationResult result = ((CelVerifierZ3Impl) verifier) .verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Implication"); + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); } + + @Test + public void isAlwaysTrue_constantVarDecl_verified() throws Exception { + Cel celWithConstVar = + CelFactory.plannerCelBuilder() + .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .addVarDeclarations( + CelVarDecl.newBuilder() + .setName("CONST_INT") + .setType(SimpleType.INT) + .setConstant(CelConstant.ofValue(42L)) + .build()) + .build(); + CelVerifier verifier = CelVerifierFactory.newVerifier(celWithConstVar).build(); + CelAbstractSyntaxTree ast = + celWithConstVar + .compile("CONST_INT == 42 && [1, 2].all(x, .CONST_INT == 42 && x > 0)") + .getAst(); + + CelVerificationResult result = verifier.isAlwaysTrue(ast); + + assertWithMessage(result.message()) + .that(result.status()) + .isEqualTo(VerificationStatus.VERIFIED); + } }