Skip to content

Commit dbfe9ce

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Move CEL-agnostic Z3 expression helpers out of CelZ3TypeSystem
PiperOrigin-RevId: 1004241088
1 parent b6a64ff commit dbfe9ce

9 files changed

Lines changed: 246 additions & 216 deletions

File tree

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,10 @@ java_library(
112112

113113
java_library(
114114
name = "type_system",
115-
srcs = ["CelZ3TypeSystem.java"],
115+
srcs = [
116+
"CelZ3Exprs.java",
117+
"CelZ3TypeSystem.java",
118+
],
116119
compatible_with = [],
117120
tags = [
118121
],

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

Lines changed: 33 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ Set<BoolExpr> getTypeConstraints() {
112112
}
113113

114114
BoolExpr hasTruncation() {
115-
return CelZ3TypeSystem.mkOrFlattened(ctx, truncationConditions);
115+
return CelZ3Exprs.mkOrFlattened(ctx, truncationConditions);
116116
}
117117

118118
CelZ3TypeSystem getTypeSystem() {
@@ -806,7 +806,7 @@ private FieldAccess getMapAccess(Expr<?> operand, String field, BoolExpr typeGua
806806
BoolExpr presence =
807807
(BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), mapFieldZ3Str);
808808
Expr<?> value = ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), mapFieldZ3Str);
809-
constrainPresentValue(CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, presence), value);
809+
constrainPresentValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value);
810810
return new FieldAccess(presence, value);
811811
}
812812

@@ -816,7 +816,7 @@ private FieldAccess getMsgAccess(Expr<?> operand, String field, BoolExpr typeGua
816816
BoolExpr presence =
817817
(BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), msgFieldZ3Str);
818818
Expr<?> value = ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), msgFieldZ3Str);
819-
constrainPresentValue(CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, presence), value);
819+
constrainPresentValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value);
820820
return new FieldAccess(presence, value);
821821
}
822822

@@ -853,7 +853,7 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a
853853
FieldAccess msgAcc = getMsgAccess(operand, field, isMessage);
854854

855855
presenceResult =
856-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
856+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
857857
.addCase(isMessage, msgAcc.presence)
858858
.addCase(isMap, mapAcc.presence)
859859
.build(ctx.mkFalse());
@@ -863,7 +863,7 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a
863863
Expr<?> mapRead = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError());
864864

865865
valueResult =
866-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
866+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
867867
.addCase(isMessage, msgRead)
868868
.addCase(isMap, mapRead)
869869
.build(typeSystem.mkError());
@@ -1060,7 +1060,7 @@ private TranslatedValue translateComprehension(CelExpr celExpr, CelAbstractSynta
10601060
TranslatedValue resultTv =
10611061
withScope(
10621062
comp.accuVar(),
1063-
TranslatedValue.create(accu, typeSystem, CelZ3TypeSystem.mkOrFlattened(ctx, taints)),
1063+
TranslatedValue.create(accu, typeSystem, CelZ3Exprs.mkOrFlattened(ctx, taints)),
10641064
() -> translateExpr(comp.result(), ast));
10651065
Expr<?> result = resultTv.z3Expr();
10661066
return TranslatedValue.create(
@@ -1152,7 +1152,7 @@ private BoolExpr getBoundedMapBijection(
11521152
seqMap);
11531153
}
11541154
constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap)));
1155-
return CelZ3TypeSystem.mkAndFlattened(ctx, constraints);
1155+
return CelZ3Exprs.mkAndFlattened(ctx, constraints);
11561156
}
11571157

11581158
private <T> T withIterationScope(
@@ -1301,8 +1301,7 @@ private TranslatedValue unrollMapAndFilter(
13011301
TranslatedValue resultTv =
13021302
withScope(
13031303
comp.accuVar(),
1304-
TranslatedValue.create(
1305-
chainedAccu, typeSystem, CelZ3TypeSystem.mkOrFlattened(ctx, taints)),
1304+
TranslatedValue.create(chainedAccu, typeSystem, CelZ3Exprs.mkOrFlattened(ctx, taints)),
13061305
() -> translateExpr(comp.result(), ast));
13071306

13081307
Expr<?> iterRangeExpr = iterRangeTv.z3Expr();
@@ -1313,10 +1312,10 @@ private TranslatedValue unrollMapAndFilter(
13131312
// result of any non-true condition, since the unrolled value ignores early exits.
13141313
BoolExpr isConditionUnmodeled = ctx.mkBool(!isLiteralTrue(comp.loopCondition()));
13151314
BoolExpr isAbstracted =
1316-
CelZ3TypeSystem.mkOrFlattened(ctx, rangeIsUnknown, isTruncated, isConditionUnmodeled);
1315+
CelZ3Exprs.mkOrFlattened(ctx, rangeIsUnknown, isTruncated, isConditionUnmodeled);
13171316
// An error is not final when truncated: an unknown from a later iteration overrides it.
13181317
Expr<?> finalResult =
1319-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
1318+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
13201319
.addCase(rangeIsError, typeSystem.mkError())
13211320
.addCase(isAbstracted, mkParameterizedUnknown(celExpr, ast))
13221321
.build(resultTv.z3Expr());
@@ -1326,7 +1325,7 @@ private TranslatedValue unrollMapAndFilter(
13261325
ctx.mkITE(
13271326
ctx.mkOr(rangeIsError, rangeIsUnknown),
13281327
iterRangeTv.isApproximate(),
1329-
CelZ3TypeSystem.mkOrFlattened(
1328+
CelZ3Exprs.mkOrFlattened(
13301329
ctx, resultTv.isApproximate(), isTruncated, isConditionUnmodeled));
13311330

13321331
return TranslatedValue.create(finalResult, celExpr, typeSystem, finalTaint);
@@ -1379,50 +1378,49 @@ private TranslatedValue reduceAllOrExists(
13791378

13801379
BoolExpr isActive = iter.inBounds;
13811380

1382-
hasMatchList.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, isMatch));
1383-
hasErrorList.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, isE));
1384-
hasUnknownList.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, isU));
1381+
hasMatchList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isMatch));
1382+
hasErrorList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isE));
1383+
hasUnknownList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isU));
13851384

13861385
hasSafeMatchList.add(
1387-
CelZ3TypeSystem.mkAndFlattened(
1388-
ctx, isActive, isMatch, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate())));
1386+
CelZ3Exprs.mkAndFlattened(
1387+
ctx, isActive, isMatch, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate())));
13891388
hasSafeErrorList.add(
1390-
CelZ3TypeSystem.mkAndFlattened(
1391-
ctx, isActive, isE, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate())));
1389+
CelZ3Exprs.mkAndFlattened(
1390+
ctx, isActive, isE, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate())));
13921391
hasSafeUnknownList.add(
1393-
CelZ3TypeSystem.mkAndFlattened(
1394-
ctx, isActive, isU, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate())));
1395-
activeTaints.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, stepTv.isApproximate()));
1392+
CelZ3Exprs.mkAndFlattened(
1393+
ctx, isActive, isU, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate())));
1394+
activeTaints.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, stepTv.isApproximate()));
13961395
}
13971396

1398-
BoolExpr hasMatch = CelZ3TypeSystem.mkOrFlattened(ctx, hasMatchList);
1399-
BoolExpr hasError = CelZ3TypeSystem.mkOrFlattened(ctx, hasErrorList);
1400-
BoolExpr hasUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, hasUnknownList);
1397+
BoolExpr hasMatch = CelZ3Exprs.mkOrFlattened(ctx, hasMatchList);
1398+
BoolExpr hasError = CelZ3Exprs.mkOrFlattened(ctx, hasErrorList);
1399+
BoolExpr hasUnknown = CelZ3Exprs.mkOrFlattened(ctx, hasUnknownList);
14011400
BoolExpr rangeIsError = typeSystem.isError(iterRangeTv.z3Expr());
14021401
BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeTv.z3Expr());
14031402

1404-
BoolExpr hasSafeMatch = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeMatchList);
1405-
BoolExpr hasSafeError = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeErrorList);
1406-
BoolExpr hasSafeUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeUnknownList);
1407-
BoolExpr anyActiveTaint = CelZ3TypeSystem.mkOrFlattened(ctx, activeTaints);
1403+
BoolExpr hasSafeMatch = CelZ3Exprs.mkOrFlattened(ctx, hasSafeMatchList);
1404+
BoolExpr hasSafeError = CelZ3Exprs.mkOrFlattened(ctx, hasSafeErrorList);
1405+
BoolExpr hasSafeUnknown = CelZ3Exprs.mkOrFlattened(ctx, hasSafeUnknownList);
1406+
BoolExpr anyActiveTaint = CelZ3Exprs.mkOrFlattened(ctx, activeTaints);
14081407

14091408
Expr<?> comprehensionUnknown = mkParameterizedUnknown(compExpr, ast);
14101409
Expr<?> result =
1411-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
1410+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
14121411
.addCase(rangeIsError, typeSystem.mkError())
14131412
.addCase(rangeIsUnknown, comprehensionUnknown)
14141413
.addCase(hasMatch, typeSystem.mkBool(!isAll))
14151414
.addCase(ctx.mkOr(hasUnknown, isTruncated), comprehensionUnknown)
14161415
.addCase(hasError, typeSystem.mkError())
14171416
.build(typeSystem.mkBool(isAll));
14181417

1419-
BoolExpr baseTaint =
1420-
CelZ3TypeSystem.mkOrFlattened(ctx, anyActiveTaint, iterRangeTv.isApproximate());
1418+
BoolExpr baseTaint = CelZ3Exprs.mkOrFlattened(ctx, anyActiveTaint, iterRangeTv.isApproximate());
14211419

14221420
// Taint identically shadows the value flow's short-circuit control structure
14231421
BoolExpr resultTaint =
14241422
(BoolExpr)
1425-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
1423+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
14261424
.addCase(ctx.mkOr(rangeIsError, rangeIsUnknown), iterRangeTv.isApproximate())
14271425
.addCase(hasMatch, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeMatch)))
14281426
.addCase(
@@ -1562,7 +1560,7 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
15621560
boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint));
15631561
}
15641562

1565-
return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes);
1563+
return CelZ3Exprs.mkAndFlattened(ctx, boundsAndTypes);
15661564
}
15671565
if (type instanceof MapType) {
15681566
// Do NOT emit a for-all quantifier over map keys or values here.
@@ -1614,7 +1612,7 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
16141612
boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType)));
16151613
}
16161614

1617-
return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes);
1615+
return CelZ3Exprs.mkAndFlattened(ctx, boundsAndTypes);
16181616
}
16191617
if (type.kind() == CelKind.STRUCT) {
16201618
return ctx.mkAnd(

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -227,7 +227,7 @@ public CelVerificationResult verifyEquivalence(
227227
// an unknown only by its attributes (e.g. `a && true` and `a` both yield unknown {a}). Two
228228
// distinct unknowns may thus still be equivalent.
229229
BoolExpr combinedTaint =
230-
CelZ3TypeSystem.mkOrFlattened(
230+
CelZ3Exprs.mkOrFlattened(
231231
ctx,
232232
tvA.isApproximate(),
233233
tvB.isApproximate(),
@@ -318,7 +318,7 @@ CelVerificationResult verifyImplication(
318318
BoolExpr violationCondition = ctx.mkAnd(assumeCondition, ctx.mkNot(assertCondition));
319319

320320
BoolExpr combinedTaint =
321-
CelZ3TypeSystem.mkOrFlattened(ctx, assumeTv.isApproximate(), assertTv.isApproximate());
321+
CelZ3Exprs.mkOrFlattened(ctx, assumeTv.isApproximate(), assertTv.isApproximate());
322322
BoolExpr unknownCondition =
323323
ctx.mkOr(
324324
translator.getTypeSystem().isUnknown(assumeTv.z3Expr()),

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

Lines changed: 160 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,160 @@
1+
// Copyright 2026 Google LLC
2+
//
3+
// Licensed under the Apache License, Version 2.0 (the "License");
4+
// you may not use this file except in compliance with the License.
5+
// You may obtain a copy of the License at
6+
//
7+
// https://www.apache.org/licenses/LICENSE-2.0
8+
//
9+
// Unless required by applicable law or agreed to in writing, software
10+
// distributed under the License is distributed on an "AS IS" BASIS,
11+
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12+
// See the License for the specific language governing permissions and
13+
// limitations under the License.
14+
15+
package dev.cel.verifier;
16+
17+
import com.google.common.collect.Lists;
18+
import com.google.errorprone.annotations.CanIgnoreReturnValue;
19+
import com.microsoft.z3.BoolExpr;
20+
import com.microsoft.z3.Context;
21+
import com.microsoft.z3.Expr;
22+
import java.util.ArrayList;
23+
import java.util.Arrays;
24+
import java.util.List;
25+
26+
/** Helpers for building Z3 expressions that are independent of the CEL encoding. */
27+
public final class CelZ3Exprs {
28+
29+
/**
30+
* Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs.
31+
*
32+
* <p>Returns {@code false} if the list is empty.
33+
*/
34+
public static BoolExpr mkOrFlattened(Context ctx, BoolExpr... args) {
35+
return mkOrFlattened(ctx, Arrays.asList(args));
36+
}
37+
38+
/**
39+
* Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs.
40+
*
41+
* <p>Returns {@code false} if the list is empty.
42+
*/
43+
public static BoolExpr mkOrFlattened(Context ctx, List<BoolExpr> args) {
44+
// Pruning true/false constants in Java is significantly faster than building
45+
// larger ASTs and letting Z3 process them natively.
46+
List<BoolExpr> filteredArgs = new ArrayList<>();
47+
for (BoolExpr arg : args) {
48+
if (arg.isTrue()) {
49+
return ctx.mkTrue();
50+
}
51+
if (!arg.isFalse()) {
52+
filteredArgs.add(arg);
53+
}
54+
}
55+
if (filteredArgs.isEmpty()) {
56+
return ctx.mkFalse();
57+
}
58+
if (filteredArgs.size() == 1) {
59+
return filteredArgs.get(0);
60+
}
61+
return ctx.mkOr(filteredArgs.toArray(new BoolExpr[0]));
62+
}
63+
64+
/**
65+
* Helper to construct a flattened logical AND expression to avoid deep left-leaning ASTs.
66+
*
67+
* <p>Returns {@code true} if the list is empty.
68+
*/
69+
public static BoolExpr mkAndFlattened(Context ctx, BoolExpr... args) {
70+
return mkAndFlattened(ctx, Arrays.asList(args));
71+
}
72+
73+
public static BoolExpr mkAndFlattened(Context ctx, List<BoolExpr> args) {
74+
// Pruning true/false constants in Java is significantly faster than building
75+
// larger ASTs and letting Z3 process them natively.
76+
List<BoolExpr> filteredArgs = new ArrayList<>();
77+
for (BoolExpr arg : args) {
78+
if (arg.isFalse()) {
79+
return ctx.mkFalse();
80+
}
81+
if (!arg.isTrue()) {
82+
filteredArgs.add(arg);
83+
}
84+
}
85+
if (filteredArgs.isEmpty()) {
86+
return ctx.mkTrue();
87+
}
88+
if (filteredArgs.size() == 1) {
89+
return filteredArgs.get(0);
90+
}
91+
return ctx.mkAnd(filteredArgs.toArray(new BoolExpr[0]));
92+
}
93+
94+
/** Helper to construct a logical NOT expression while avoiding redundant NOT operations. */
95+
public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
96+
if (arg.isTrue()) {
97+
return ctx.mkFalse();
98+
}
99+
if (arg.isFalse()) {
100+
return ctx.mkTrue();
101+
}
102+
return ctx.mkNot(arg);
103+
}
104+
105+
/**
106+
* Helper to build a chain of nested ITE (If-Then-Else) conditions.
107+
*
108+
* <p>Conditions are evaluated in the order they are added. Branches with {@code isFalse()}
109+
* conditions are skipped, and redundant {@code ITE(condition, X, X)} creations are omitted to
110+
* avoid allocating dead AST paths in Z3.
111+
*/
112+
public static final class SwitchBuilder {
113+
114+
private static final class SwitchCase {
115+
private final BoolExpr condition;
116+
private final Expr<?> value;
117+
118+
private SwitchCase(BoolExpr condition, Expr<?> value) {
119+
this.condition = condition;
120+
this.value = value;
121+
}
122+
}
123+
124+
private final Context ctx;
125+
private final List<SwitchCase> cases;
126+
127+
public static SwitchBuilder newBuilder(Context ctx) {
128+
return new SwitchBuilder(ctx);
129+
}
130+
131+
@CanIgnoreReturnValue
132+
public SwitchBuilder addCase(BoolExpr condition, Expr<?> value) {
133+
// Skip branches that can never be hit (e.g. `isFalse()` probes).
134+
if (condition.isFalse()) {
135+
return this;
136+
}
137+
cases.add(new SwitchCase(condition, value));
138+
return this;
139+
}
140+
141+
public Expr<?> build(Expr<?> defaultFallback) {
142+
Expr<?> result = defaultFallback;
143+
for (SwitchCase c : Lists.reverse(cases)) {
144+
// ITE(condition, X, X) simplifies to X; skip calling into native C++ Z3_mk_ite.
145+
if (c.value.equals(result)) {
146+
continue;
147+
}
148+
result = ctx.mkITE(c.condition, c.value, result);
149+
}
150+
return result;
151+
}
152+
153+
private SwitchBuilder(Context ctx) {
154+
this.ctx = ctx;
155+
this.cases = new ArrayList<>();
156+
}
157+
}
158+
159+
private CelZ3Exprs() {}
160+
}

0 commit comments

Comments
 (0)