Skip to content

Compare lists and maps that aren't literals, and in on lists with CEL equality #1463

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
copybara-service merged 1 commit into from
Nov 13, 2026
Merged

Compare lists and maps that aren't literals, and in on lists with CEL equality #1463

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 0 additions & 7 deletions verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -107,13 +107,6 @@ Set<Expr<?>> getInputVariables() {
return context.inputVariables();
}

/**
* Returns a Z3 boolean expression asserting that the provided CEL value is a boolean and is true.
*/
BoolExpr isTrue(Expr<?> celValue) {
return ctx.mkAnd(typeSystem.isBool(celValue), (BoolExpr) typeSystem.unwrapBool(celValue));
}

/**
* Binds an identifier name in the symbol table to an already-translated value. Used to bind
* reserved policy symbols such as 'rule.result' to the composed policy graph.
Expand Down
6 changes: 3 additions & 3 deletions verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -273,8 +273,8 @@ CelVerificationResult verifyImplication(
TranslatedValue assumeTv = translator.translate(assumeAst);
TranslatedValue assertTv = translator.translate(assertAst);

BoolExpr assumeCondition = translator.isTrue(assumeTv.z3Expr());
BoolExpr assertCondition = translator.isTrue(assertTv.z3Expr());
BoolExpr assumeCondition = translator.getTypeSystem().isTrue(assumeTv.z3Expr());
BoolExpr assertCondition = translator.getTypeSystem().isTrue(assertTv.z3Expr());
BoolExpr violationCondition = ctx.mkAnd(assumeCondition, ctx.mkNot(assertCondition));

BoolExpr combinedTaint =
Expand Down Expand Up @@ -305,7 +305,7 @@ private CelVerificationResult checkSatisfiability(
CelAstToZ3Translator translator = newTranslator(ctx, /* parameterizeUnknowns= */ false);

TranslatedValue tv = translator.translate(ast);
BoolExpr isTrue = translator.isTrue(tv.z3Expr());
BoolExpr isTrue = translator.getTypeSystem().isTrue(tv.z3Expr());
if (searchForCounterexample) {
return search(
ctx,
Expand Down
Loading
Loading