Skip to content

Commit 7ccae6e

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Deduplicate Z3 list references by sequence term and add policy conformance equivalence tests
PiperOrigin-RevId: 1010013088
1 parent e5bf206 commit 7ccae6e

4 files changed

Lines changed: 161 additions & 82 deletions

File tree

‎verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java‎

Lines changed: 40 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -76,7 +76,7 @@ final class CelAstToZ3Translator {
7676
private final CelZ3ComprehensionTranslator comprehensionTranslator;
7777
private final CelZ3StructTranslator structTranslator;
7878
private final ImmutableSet<String> unknownIdentifiers;
79-
private final Map<Object, Expr<?>> listLiteralCache;
79+
private final Map<SeqExpr<?>, Expr<?>> listLiteralCache;
8080

8181
/**
8282
* 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
268268

269269
private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast) {
270270
CelList createList = celExpr.list();
271-
Optional<Object> cacheKey = toCacheKey(celExpr);
272271
List<TranslatedValue> elementsTv = new ArrayList<>();
273-
Expr<?> listRef = cacheKey.map(listLiteralCache::get).orElse(null);
274-
275-
// Cache list literals containing only constants. If the same list literal appears multiple
276-
// times (e.g., in equality checks like `[1, 2] == [1, 2]`), caching allows us to reuse the
277-
// same Z3 constant. This avoids expensive sequence equality reasoning in Z3 by reducing the
278-
// check to a trivial identity check (e.g., `list_ref_0 == list_ref_0`).
279-
if (listRef == null) {
280-
SeqExpr seq = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()));
281-
List<Expr<?>> values = new ArrayList<>();
282-
ImmutableList<Integer> optionalIndices = createList.optionalIndices();
283-
ImmutableList<CelExpr> elements = createList.elements();
284-
for (int i = 0; i < elements.size(); i++) {
285-
CelExpr element = elements.get(i);
286-
TranslatedValue elem = translateExpr(element, ast);
287-
288-
if (optionalIndices.contains(i)) {
289-
Expr<?> checkedValue =
290-
typeSystem.withRuntimeError(
291-
elem.z3Expr(), ctx.mkNot(typeSystem.isOptional(elem.z3Expr())));
292-
elem = TranslatedValue.create(checkedValue, element, typeSystem, elem.isApproximate());
293-
294-
Expr<?> optRef = typeSystem.getOptionalRef(elem.z3Expr());
295-
Expr<?> value = typeSystem.getOptionalValue(optRef);
296-
seq =
297-
(SeqExpr)
298-
ctx.mkITE(
299-
typeSystem.optHasValue(optRef),
300-
typeSystem.mkConcatSafe(seq, ctx.mkUnit(value)),
301-
seq);
302-
values.add(value);
303-
} else {
304-
seq = typeSystem.mkConcatSafe(seq, ctx.mkUnit(elem.z3Expr()));
305-
values.add(elem.z3Expr());
306-
}
307-
elementsTv.add(elem);
272+
SeqExpr seq = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort()));
273+
List<Expr<?>> values = new ArrayList<>();
274+
ImmutableList<Integer> optionalIndices = createList.optionalIndices();
275+
ImmutableList<CelExpr> elements = createList.elements();
276+
for (int i = 0; i < elements.size(); i++) {
277+
CelExpr element = elements.get(i);
278+
TranslatedValue elem = translateExpr(element, ast);
279+
280+
if (optionalIndices.contains(i)) {
281+
Expr<?> checkedValue =
282+
typeSystem.withRuntimeError(
283+
elem.z3Expr(), ctx.mkNot(typeSystem.isOptional(elem.z3Expr())));
284+
elem = TranslatedValue.create(checkedValue, element, typeSystem, elem.isApproximate());
285+
286+
Expr<?> optRef = typeSystem.getOptionalRef(elem.z3Expr());
287+
Expr<?> value = typeSystem.getOptionalValue(optRef);
288+
seq =
289+
(SeqExpr)
290+
ctx.mkITE(
291+
typeSystem.optHasValue(optRef),
292+
typeSystem.mkConcatSafe(seq, ctx.mkUnit(value)),
293+
seq);
294+
values.add(value);
295+
} else {
296+
seq = typeSystem.mkConcatSafe(seq, ctx.mkUnit(elem.z3Expr()));
297+
values.add(elem.z3Expr());
308298
}
309-
listRef = typeSystem.mkListRefConst(LIST_REF_PREFIX);
310-
context.addConstraint(ctx.mkEq(typeSystem.getSeq(listRef), seq));
311-
propagateTruncatedTypeConstraint(typeSystem.wrapList(listRef), values);
312-
Expr<?> finalListRef = listRef;
313-
cacheKey.ifPresent(key -> listLiteralCache.put(key, finalListRef));
299+
elementsTv.add(elem);
314300
}
315301

302+
// Reuse the same Z3 ListRef whenever two list constructions yield the exact same sequence term
303+
// (e.g., identical constant lists or identical unrolled map/filter step lists across ASTs).
304+
Expr<?> listRef =
305+
listLiteralCache.computeIfAbsent(
306+
seq,
307+
s -> {
308+
Expr<?> ref = typeSystem.mkListRefConst(LIST_REF_PREFIX);
309+
context.addConstraint(ctx.mkEq(typeSystem.getSeq(ref), s));
310+
propagateTruncatedTypeConstraint(typeSystem.wrapList(ref), values);
311+
return ref;
312+
});
313+
316314
Expr<?> result = typeSystem.wrapList(listRef);
317315
return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv);
318316
}
@@ -481,31 +479,6 @@ private static boolean mayEmbedArgs(String functionName, CelType resultType) {
481479
&& !functionName.equals(Operator.CONDITIONAL.getFunction());
482480
}
483481

484-
private Optional<Object> toCacheKey(CelExpr expr) {
485-
switch (expr.exprKind().getKind()) {
486-
case CONSTANT:
487-
return Optional.of(expr.constant());
488-
case LIST:
489-
if (!expr.list().optionalIndices().isEmpty()) {
490-
// Do not cache lists with optional elements. Optional elements conditionally alter
491-
// sequence length and presence via ITE branches at runtime; caching would collide
492-
// [1, 2] with [?1, 2] and freeze conditional evaluations to a static reference.
493-
return Optional.empty();
494-
}
495-
ImmutableList.Builder<Object> builder = ImmutableList.builder();
496-
for (CelExpr elem : expr.list().elements()) {
497-
Optional<Object> elemKey = toCacheKey(elem);
498-
if (!elemKey.isPresent()) {
499-
return Optional.empty(); // Contains non-constants
500-
}
501-
builder.add(elemKey.get());
502-
}
503-
return Optional.of(builder.build());
504-
default:
505-
return Optional.empty();
506-
}
507-
}
508-
509482
CelAstToZ3Translator(
510483
Context ctx,
511484
int comprehensionUnrollLimit,

‎verifier/src/test/java/dev/cel/verifier/BUILD.bazel‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,9 +14,11 @@ java_library(
1414
compatible_with = [],
1515
data = [
1616
"//testing:policy_test_resources",
17+
"@cel_policy//conformance:testdata",
1718
],
1819
deps = [
1920
"//bundle:cel",
21+
"//bundle:environment_yaml_parser",
2022
"//common:cel_ast",
2123
"//common:compiler_common",
2224
"//common:container",
@@ -25,6 +27,7 @@ java_library(
2527
"//common:options",
2628
"//common/ast",
2729
"//common/ast:mutable_expr",
30+
"//common/resources/testdata/proto3:standalone_global_enum_java_proto",
2831
"//common/types",
2932
"//common/types:message_type_provider",
3033
"//compiler:compiler_builder",
@@ -43,6 +46,8 @@ java_library(
4346
"//policy:parser",
4447
"//policy:parser_factory",
4548
"//policy:validation_exception",
49+
"//policy/testing:k8s_test_tag_handler",
50+
"//testing/protos:single_file_java_proto",
4651
"@bazel_tools//tools/java/runfiles",
4752
"@maven//:junit_junit",
4853
"@maven//:com_google_testparameterinjector_test_parameter_injector",

‎verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java‎

Lines changed: 88 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -18,10 +18,12 @@
1818
import static com.google.common.truth.Truth.assertWithMessage;
1919
import static org.junit.Assert.assertThrows;
2020

21+
import com.google.common.collect.ImmutableList;
2122
import com.google.common.collect.ImmutableMap;
2223
import com.google.testing.junit.testparameterinjector.TestParameter;
2324
import com.google.testing.junit.testparameterinjector.TestParameterInjector;
2425
import dev.cel.bundle.Cel;
26+
import dev.cel.bundle.CelEnvironmentYamlParser;
2527
import dev.cel.bundle.CelFactory;
2628
import dev.cel.common.CelAbstractSyntaxTree;
2729
import dev.cel.common.CelFunctionDecl;
@@ -31,6 +33,7 @@
3133
import dev.cel.common.types.StructTypeReference;
3234
import dev.cel.expr.conformance.proto3.TestAllTypes;
3335
import dev.cel.extensions.CelExtensions;
36+
import dev.cel.extensions.CelOptionalLibrary;
3437
import dev.cel.optimizer.CelOptimizer;
3538
import dev.cel.optimizer.CelOptimizerFactory;
3639
import dev.cel.optimizer.optimizers.SubexpressionOptimizer;
@@ -43,6 +46,9 @@
4346
import dev.cel.policy.CelPolicyParser;
4447
import dev.cel.policy.CelPolicyParserFactory;
4548
import dev.cel.policy.CelPolicyValidationException;
49+
import dev.cel.policy.testing.K8sTagHandler;
50+
import dev.cel.testing.testdata.SingleFile;
51+
import dev.cel.testing.testdata.proto3.StandaloneGlobalEnum;
4652
import dev.cel.verifier.CelVerificationResult.VerificationStatus;
4753
import org.junit.Before;
4854
import org.junit.Test;
@@ -80,7 +86,7 @@ public final class CelPolicyVerifierImplTest {
8086
private static final CelPolicyCompiler POLICY_COMPILER =
8187
CelPolicyCompilerFactory.newPolicyCompiler(CEL).build();
8288

83-
private static final CelVerifier AST_VERIFIER = CelVerifierFactory.newVerifier().build();
89+
private static final CelVerifier AST_VERIFIER = CelVerifierFactory.newVerifier(CEL).build();
8490
private static final CelPolicyVerifier VERIFIER =
8591
CelPolicyVerifierFactory.newVerifier(POLICY_COMPILER, AST_VERIFIER).build();
8692

@@ -722,4 +728,85 @@ public void verifyInvariants_boundedSymbolWithApproximation_returnsInconclusive(
722728
assertThat(results).containsKey("check_approx");
723729
assertThat(results.get("check_approx").status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
724730
}
731+
732+
private enum ConformancePolicyTestCase {
733+
AGGREGATE("aggregate"),
734+
AGGREGATE_EXPLICIT_LIST_OUTPUT("aggregate_explicit_list_output"),
735+
AGGREGATE_EXPLICIT_OPTIONAL_NONE("aggregate_explicit_optional_none"),
736+
AGGREGATE_NESTED_EXPLICIT_LIST_DOUBLE_WRAPPING(
737+
"aggregate_nested_explicit_list_double_wrapping"),
738+
AGGREGATE_SHADOWED_VARIABLES("aggregate_shadowed_variables"),
739+
CONTEXT_PB("context_pb"),
740+
FIRST_MATCH_NESTED_AGGREGATE("first_match_nested_aggregate"),
741+
K8S("k8s"),
742+
LIMITS("limits"),
743+
NESTED_RULE("nested_rule"),
744+
NESTED_RULE2("nested_rule2"),
745+
NESTED_RULE3("nested_rule3"),
746+
NESTED_RULE4("nested_rule4"),
747+
NESTED_RULE5("nested_rule5"),
748+
NESTED_RULE6("nested_rule6"),
749+
NESTED_RULE7("nested_rule7"),
750+
NESTED_RULES_VARIABLE_SHADOWING("nested_rules_variable_shadowing"),
751+
PB("pb"),
752+
REQUIRED_LABELS("required_labels"),
753+
RESTRICTED_DESTINATIONS("restricted_destinations"),
754+
UNCONDITIONAL_RULES("unconditional_rules"),
755+
UNNEST("unnest"),
756+
VARIABLE_TYPE_PROPAGATION("variable_type_propagation");
757+
758+
private final String policyDir;
759+
760+
ConformancePolicyTestCase(String policyDir) {
761+
this.policyDir = policyDir;
762+
}
763+
}
764+
765+
@Test
766+
public void verifyEquivalence_conformancePolicies_unoptimizedVsOptimized(
767+
@TestParameter ConformancePolicyTestCase testCase) throws Exception {
768+
CelPolicyParser policyParser =
769+
CelPolicyParserFactory.newYamlParserBuilder().addTagVisitor(new K8sTagHandler()).build();
770+
CelOptions options =
771+
CelOptions.current()
772+
.populateMacroCalls(true)
773+
.enableHeterogeneousNumericComparisons(true)
774+
.build();
775+
Cel baseCel =
776+
CelFactory.plannerCelBuilder()
777+
.setOptions(options)
778+
.setStandardMacros(CelStandardMacro.STANDARD_MACROS)
779+
.addCompilerLibraries(CelOptionalLibrary.INSTANCE, CelExtensions.bindings())
780+
.addRuntimeLibraries(CelOptionalLibrary.INSTANCE)
781+
.addFileTypes(StandaloneGlobalEnum.getDescriptor().getFile())
782+
.addMessageTypes(TestAllTypes.getDescriptor(), SingleFile.getDescriptor())
783+
.build();
784+
String configYaml =
785+
VerifierTestHelper.maybeLoadConformanceConfigYaml(testCase.policyDir).orElse(null);
786+
Cel cel =
787+
configYaml != null
788+
? CelEnvironmentYamlParser.newInstance().parse(configYaml).extend(baseCel, options)
789+
: baseCel;
790+
CelPolicy policy =
791+
policyParser.parse(VerifierTestHelper.loadConformancePolicyYaml(testCase.policyDir));
792+
CelPolicyCompiler unoptimizedCompiler = CelPolicyCompilerFactory.newPolicyCompiler(cel).build();
793+
CelPolicyCompiler optimizedCompiler =
794+
CelPolicyCompilerFactory.newPolicyCompiler(cel)
795+
.setOptimizers(
796+
ImmutableList.of(
797+
SubexpressionOptimizer.newInstance(
798+
SubexpressionOptimizerOptions.newBuilder()
799+
.populateMacroCalls(true)
800+
.build())))
801+
.build();
802+
CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build();
803+
804+
CelAbstractSyntaxTree unoptimizedAst = unoptimizedCompiler.compile(policy);
805+
CelAbstractSyntaxTree optimizedAst = optimizedCompiler.compile(policy);
806+
CelVerificationResult result = verifier.verifyEquivalence(unoptimizedAst, optimizedAst);
807+
808+
assertWithMessage(result.message())
809+
.that(result.status())
810+
.isEqualTo(VerificationStatus.VERIFIED);
811+
}
725812
}

‎verifier/src/test/java/dev/cel/verifier/VerifierTestHelper.java‎

Lines changed: 28 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -22,28 +22,42 @@
2222
import com.google.devtools.build.runfiles.Runfiles;
2323
import java.io.File;
2424
import java.io.IOException;
25+
import java.util.Optional;
2526

2627
/** Package-private class to assist with verifier testing and runfiles resolution. */
2728
@AutoBazelRepository
2829
final class VerifierTestHelper {
2930

30-
private static final Runfiles runfiles = createRunfiles();
31+
private static final Runfiles RUNFILES = createRunfiles();
3132

3233
static String loadVerificationPolicyYaml(String filename) throws IOException {
33-
String rlocationPath =
34-
"cel_java/testing/src/test/resources/policy/verification/" + filename;
35-
String resolvedPath = runfiles.rlocation(Ascii.toLowerCase(rlocationPath));
36-
if (resolvedPath == null) {
37-
throw new IOException("Unmapped runfile path: " + rlocationPath);
38-
}
39-
File file = new File(resolvedPath);
40-
if (!file.exists()) {
41-
throw new IOException(
42-
String.format(
43-
"Runfile not found on disk at '%s' (unresolved path: '%s')",
44-
resolvedPath, rlocationPath));
34+
return loadRunfile(
35+
"cel_java/testing/src/test/resources/policy/verification/" + filename);
36+
}
37+
38+
static String loadConformancePolicyYaml(String policyDir) throws IOException {
39+
return loadRunfile(
40+
String.format(
41+
"cel_policy/conformance/testdata/%s/policy.yaml", policyDir));
42+
}
43+
44+
static Optional<String> maybeLoadConformanceConfigYaml(String policyDir) throws IOException {
45+
return maybeLoadRunfile(
46+
String.format(
47+
"cel_policy/conformance/testdata/%s/config.yaml", policyDir));
48+
}
49+
50+
private static String loadRunfile(String rlocationPath) throws IOException {
51+
return maybeLoadRunfile(rlocationPath)
52+
.orElseThrow(() -> new IOException("Runfile not found: " + rlocationPath));
53+
}
54+
55+
private static Optional<String> maybeLoadRunfile(String rlocationPath) throws IOException {
56+
String resolvedPath = RUNFILES.rlocation(Ascii.toLowerCase(rlocationPath));
57+
if (resolvedPath == null || !new File(resolvedPath).exists()) {
58+
return Optional.empty();
4559
}
46-
return Files.asCharSource(file, UTF_8).read();
60+
return Optional.of(Files.asCharSource(new File(resolvedPath), UTF_8).read());
4761
}
4862

4963
private static Runfiles createRunfiles() {

0 commit comments

Comments
 (0)