diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 7cada2186..005289b83 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -76,7 +76,7 @@ final class CelAstToZ3Translator { private final CelZ3ComprehensionTranslator comprehensionTranslator; private final CelZ3StructTranslator structTranslator; private final ImmutableSet unknownIdentifiers; - private final Map> listLiteralCache; + private final Map, Expr> listLiteralCache; /** * Returns a set of Z3 boolean expressions representing type constraints for the translated AST. @@ -268,51 +268,49 @@ private TranslatedValue translateIdent(CelExpr celExpr, CelAbstractSyntaxTree as private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast) { CelList createList = celExpr.list(); - Optional cacheKey = toCacheKey(celExpr); List elementsTv = new ArrayList<>(); - Expr listRef = cacheKey.map(listLiteralCache::get).orElse(null); - - // Cache list literals containing only constants. If the same list literal appears multiple - // times (e.g., in equality checks like `[1, 2] == [1, 2]`), caching allows us to reuse the - // same Z3 constant. This avoids expensive sequence equality reasoning in Z3 by reducing the - // check to a trivial identity check (e.g., `list_ref_0 == list_ref_0`). - if (listRef == null) { - SeqExpr seq = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort())); - List> values = new ArrayList<>(); - ImmutableList optionalIndices = createList.optionalIndices(); - ImmutableList elements = createList.elements(); - for (int i = 0; i < elements.size(); i++) { - CelExpr element = elements.get(i); - TranslatedValue elem = translateExpr(element, ast); - - if (optionalIndices.contains(i)) { - Expr checkedValue = - typeSystem.withRuntimeError( - elem.z3Expr(), ctx.mkNot(typeSystem.isOptional(elem.z3Expr()))); - elem = TranslatedValue.create(checkedValue, element, typeSystem, elem.isApproximate()); - - Expr optRef = typeSystem.getOptionalRef(elem.z3Expr()); - Expr value = typeSystem.getOptionalValue(optRef); - seq = - (SeqExpr) - ctx.mkITE( - typeSystem.optHasValue(optRef), - typeSystem.mkConcatSafe(seq, ctx.mkUnit(value)), - seq); - values.add(value); - } else { - seq = typeSystem.mkConcatSafe(seq, ctx.mkUnit(elem.z3Expr())); - values.add(elem.z3Expr()); - } - elementsTv.add(elem); + SeqExpr seq = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort())); + List> values = new ArrayList<>(); + ImmutableList optionalIndices = createList.optionalIndices(); + ImmutableList elements = createList.elements(); + for (int i = 0; i < elements.size(); i++) { + CelExpr element = elements.get(i); + TranslatedValue elem = translateExpr(element, ast); + + if (optionalIndices.contains(i)) { + Expr checkedValue = + typeSystem.withRuntimeError( + elem.z3Expr(), ctx.mkNot(typeSystem.isOptional(elem.z3Expr()))); + elem = TranslatedValue.create(checkedValue, element, typeSystem, elem.isApproximate()); + + Expr optRef = typeSystem.getOptionalRef(elem.z3Expr()); + Expr value = typeSystem.getOptionalValue(optRef); + seq = + (SeqExpr) + ctx.mkITE( + typeSystem.optHasValue(optRef), + typeSystem.mkConcatSafe(seq, ctx.mkUnit(value)), + seq); + values.add(value); + } else { + seq = typeSystem.mkConcatSafe(seq, ctx.mkUnit(elem.z3Expr())); + values.add(elem.z3Expr()); } - listRef = typeSystem.mkListRefConst(LIST_REF_PREFIX); - context.addConstraint(ctx.mkEq(typeSystem.getSeq(listRef), seq)); - propagateTruncatedTypeConstraint(typeSystem.wrapList(listRef), values); - Expr finalListRef = listRef; - cacheKey.ifPresent(key -> listLiteralCache.put(key, finalListRef)); + elementsTv.add(elem); } + // Reuse the same Z3 ListRef whenever two list constructions yield the exact same sequence term + // (e.g., identical constant lists or identical unrolled map/filter step lists across ASTs). + Expr listRef = + listLiteralCache.computeIfAbsent( + seq, + s -> { + Expr ref = typeSystem.mkListRefConst(LIST_REF_PREFIX); + context.addConstraint(ctx.mkEq(typeSystem.getSeq(ref), s)); + propagateTruncatedTypeConstraint(typeSystem.wrapList(ref), values); + return ref; + }); + Expr result = typeSystem.wrapList(listRef); return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv); } @@ -481,31 +479,6 @@ private static boolean mayEmbedArgs(String functionName, CelType resultType) { && !functionName.equals(Operator.CONDITIONAL.getFunction()); } - private Optional toCacheKey(CelExpr expr) { - switch (expr.exprKind().getKind()) { - case CONSTANT: - return Optional.of(expr.constant()); - case LIST: - if (!expr.list().optionalIndices().isEmpty()) { - // Do not cache lists with optional elements. Optional elements conditionally alter - // sequence length and presence via ITE branches at runtime; caching would collide - // [1, 2] with [?1, 2] and freeze conditional evaluations to a static reference. - return Optional.empty(); - } - ImmutableList.Builder builder = ImmutableList.builder(); - for (CelExpr elem : expr.list().elements()) { - Optional elemKey = toCacheKey(elem); - if (!elemKey.isPresent()) { - return Optional.empty(); // Contains non-constants - } - builder.add(elemKey.get()); - } - return Optional.of(builder.build()); - default: - return Optional.empty(); - } - } - CelAstToZ3Translator( Context ctx, int comprehensionUnrollLimit, diff --git a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel index 55b9c24be..11477ee45 100644 --- a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel @@ -14,9 +14,11 @@ java_library( compatible_with = [], data = [ "//testing:policy_test_resources", + "@cel_policy//conformance:testdata", ], deps = [ "//bundle:cel", + "//bundle:environment_yaml_parser", "//common:cel_ast", "//common:compiler_common", "//common:container", @@ -25,6 +27,7 @@ java_library( "//common:options", "//common/ast", "//common/ast:mutable_expr", + "//common/resources/testdata/proto3:standalone_global_enum_java_proto", "//common/types", "//common/types:message_type_provider", "//compiler:compiler_builder", @@ -43,6 +46,8 @@ java_library( "//policy:parser", "//policy:parser_factory", "//policy:validation_exception", + "//policy/testing:k8s_test_tag_handler", + "//testing/protos:single_file_java_proto", "@bazel_tools//tools/java/runfiles", "@maven//:junit_junit", "@maven//:com_google_testparameterinjector_test_parameter_injector", diff --git a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java index 87db12f78..206316dd5 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java @@ -18,10 +18,12 @@ import static com.google.common.truth.Truth.assertWithMessage; import static org.junit.Assert.assertThrows; +import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import com.google.testing.junit.testparameterinjector.TestParameter; import com.google.testing.junit.testparameterinjector.TestParameterInjector; import dev.cel.bundle.Cel; +import dev.cel.bundle.CelEnvironmentYamlParser; import dev.cel.bundle.CelFactory; import dev.cel.common.CelAbstractSyntaxTree; import dev.cel.common.CelFunctionDecl; @@ -31,6 +33,7 @@ import dev.cel.common.types.StructTypeReference; import dev.cel.expr.conformance.proto3.TestAllTypes; import dev.cel.extensions.CelExtensions; +import dev.cel.extensions.CelOptionalLibrary; import dev.cel.optimizer.CelOptimizer; import dev.cel.optimizer.CelOptimizerFactory; import dev.cel.optimizer.optimizers.SubexpressionOptimizer; @@ -43,6 +46,9 @@ import dev.cel.policy.CelPolicyParser; import dev.cel.policy.CelPolicyParserFactory; import dev.cel.policy.CelPolicyValidationException; +import dev.cel.policy.testing.K8sTagHandler; +import dev.cel.testing.testdata.SingleFile; +import dev.cel.testing.testdata.proto3.StandaloneGlobalEnum; import dev.cel.verifier.CelVerificationResult.VerificationStatus; import org.junit.Before; import org.junit.Test; @@ -80,7 +86,7 @@ public final class CelPolicyVerifierImplTest { private static final CelPolicyCompiler POLICY_COMPILER = CelPolicyCompilerFactory.newPolicyCompiler(CEL).build(); - private static final CelVerifier AST_VERIFIER = CelVerifierFactory.newVerifier().build(); + private static final CelVerifier AST_VERIFIER = CelVerifierFactory.newVerifier(CEL).build(); private static final CelPolicyVerifier VERIFIER = CelPolicyVerifierFactory.newVerifier(POLICY_COMPILER, AST_VERIFIER).build(); @@ -722,4 +728,85 @@ public void verifyInvariants_boundedSymbolWithApproximation_returnsInconclusive( assertThat(results).containsKey("check_approx"); assertThat(results.get("check_approx").status()).isEqualTo(VerificationStatus.INCONCLUSIVE); } + + private enum ConformancePolicyTestCase { + AGGREGATE("aggregate"), + AGGREGATE_EXPLICIT_LIST_OUTPUT("aggregate_explicit_list_output"), + AGGREGATE_EXPLICIT_OPTIONAL_NONE("aggregate_explicit_optional_none"), + AGGREGATE_NESTED_EXPLICIT_LIST_DOUBLE_WRAPPING( + "aggregate_nested_explicit_list_double_wrapping"), + AGGREGATE_SHADOWED_VARIABLES("aggregate_shadowed_variables"), + CONTEXT_PB("context_pb"), + FIRST_MATCH_NESTED_AGGREGATE("first_match_nested_aggregate"), + K8S("k8s"), + LIMITS("limits"), + NESTED_RULE("nested_rule"), + NESTED_RULE2("nested_rule2"), + NESTED_RULE3("nested_rule3"), + NESTED_RULE4("nested_rule4"), + NESTED_RULE5("nested_rule5"), + NESTED_RULE6("nested_rule6"), + NESTED_RULE7("nested_rule7"), + NESTED_RULES_VARIABLE_SHADOWING("nested_rules_variable_shadowing"), + PB("pb"), + REQUIRED_LABELS("required_labels"), + RESTRICTED_DESTINATIONS("restricted_destinations"), + UNCONDITIONAL_RULES("unconditional_rules"), + UNNEST("unnest"), + VARIABLE_TYPE_PROPAGATION("variable_type_propagation"); + + private final String policyDir; + + ConformancePolicyTestCase(String policyDir) { + this.policyDir = policyDir; + } + } + + @Test + public void verifyEquivalence_conformancePolicies_unoptimizedVsOptimized( + @TestParameter ConformancePolicyTestCase testCase) throws Exception { + CelPolicyParser policyParser = + CelPolicyParserFactory.newYamlParserBuilder().addTagVisitor(new K8sTagHandler()).build(); + CelOptions options = + CelOptions.current() + .populateMacroCalls(true) + .enableHeterogeneousNumericComparisons(true) + .build(); + Cel baseCel = + CelFactory.plannerCelBuilder() + .setOptions(options) + .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .addCompilerLibraries(CelOptionalLibrary.INSTANCE, CelExtensions.bindings()) + .addRuntimeLibraries(CelOptionalLibrary.INSTANCE) + .addFileTypes(StandaloneGlobalEnum.getDescriptor().getFile()) + .addMessageTypes(TestAllTypes.getDescriptor(), SingleFile.getDescriptor()) + .build(); + String configYaml = + VerifierTestHelper.maybeLoadConformanceConfigYaml(testCase.policyDir).orElse(null); + Cel cel = + configYaml != null + ? CelEnvironmentYamlParser.newInstance().parse(configYaml).extend(baseCel, options) + : baseCel; + CelPolicy policy = + policyParser.parse(VerifierTestHelper.loadConformancePolicyYaml(testCase.policyDir)); + CelPolicyCompiler unoptimizedCompiler = CelPolicyCompilerFactory.newPolicyCompiler(cel).build(); + CelPolicyCompiler optimizedCompiler = + CelPolicyCompilerFactory.newPolicyCompiler(cel) + .setOptimizers( + ImmutableList.of( + SubexpressionOptimizer.newInstance( + SubexpressionOptimizerOptions.newBuilder() + .populateMacroCalls(true) + .build()))) + .build(); + CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); + + CelAbstractSyntaxTree unoptimizedAst = unoptimizedCompiler.compile(policy); + CelAbstractSyntaxTree optimizedAst = optimizedCompiler.compile(policy); + CelVerificationResult result = verifier.verifyEquivalence(unoptimizedAst, optimizedAst); + + assertWithMessage(result.message()) + .that(result.status()) + .isEqualTo(VerificationStatus.VERIFIED); + } } diff --git a/verifier/src/test/java/dev/cel/verifier/VerifierTestHelper.java b/verifier/src/test/java/dev/cel/verifier/VerifierTestHelper.java index b54d01d44..4f57ae1ba 100644 --- a/verifier/src/test/java/dev/cel/verifier/VerifierTestHelper.java +++ b/verifier/src/test/java/dev/cel/verifier/VerifierTestHelper.java @@ -22,28 +22,42 @@ import com.google.devtools.build.runfiles.Runfiles; import java.io.File; import java.io.IOException; +import java.util.Optional; /** Package-private class to assist with verifier testing and runfiles resolution. */ @AutoBazelRepository final class VerifierTestHelper { - private static final Runfiles runfiles = createRunfiles(); + private static final Runfiles RUNFILES = createRunfiles(); static String loadVerificationPolicyYaml(String filename) throws IOException { - String rlocationPath = - "cel_java/testing/src/test/resources/policy/verification/" + filename; - String resolvedPath = runfiles.rlocation(Ascii.toLowerCase(rlocationPath)); - if (resolvedPath == null) { - throw new IOException("Unmapped runfile path: " + rlocationPath); - } - File file = new File(resolvedPath); - if (!file.exists()) { - throw new IOException( - String.format( - "Runfile not found on disk at '%s' (unresolved path: '%s')", - resolvedPath, rlocationPath)); + return loadRunfile( + "cel_java/testing/src/test/resources/policy/verification/" + filename); + } + + static String loadConformancePolicyYaml(String policyDir) throws IOException { + return loadRunfile( + String.format( + "cel_policy/conformance/testdata/%s/policy.yaml", policyDir)); + } + + static Optional maybeLoadConformanceConfigYaml(String policyDir) throws IOException { + return maybeLoadRunfile( + String.format( + "cel_policy/conformance/testdata/%s/config.yaml", policyDir)); + } + + private static String loadRunfile(String rlocationPath) throws IOException { + return maybeLoadRunfile(rlocationPath) + .orElseThrow(() -> new IOException("Runfile not found: " + rlocationPath)); + } + + private static Optional maybeLoadRunfile(String rlocationPath) throws IOException { + String resolvedPath = RUNFILES.rlocation(Ascii.toLowerCase(rlocationPath)); + if (resolvedPath == null || !new File(resolvedPath).exists()) { + return Optional.empty(); } - return Files.asCharSource(file, UTF_8).read(); + return Optional.of(Files.asCharSource(new File(resolvedPath), UTF_8).read()); } private static Runfiles createRunfiles() {