Skip to content

Commit 5bfb57d

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Extract CelZ3TypeConstraintGenerator from CelAstToZ3Translator
PiperOrigin-RevId: 1004241090
1 parent f6bc03e commit 5bfb57d

10 files changed

Lines changed: 485 additions & 400 deletions

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

Lines changed: 5 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
],
@@ -161,6 +164,7 @@ java_library(
161164
"CelZ3ExtensionalityAxioms.java",
162165
"CelZ3FunctionRegistry.java",
163166
"CelZ3OperatorTranslator.java",
167+
"CelZ3TypeConstraintGenerator.java",
164168
"TranslatedValue.java",
165169
],
166170
compatible_with = [],

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

Lines changed: 40 additions & 219 deletions
Large diffs are not rendered by default.

‎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+
}

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

Lines changed: 26 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -131,7 +131,7 @@ Optional<TranslatedValue> translateFunctionCall(
131131
typeGuards.add(mkTypeGuard(z3Args.get(i), overload.parameterTypes().get(i)));
132132
}
133133

134-
BoolExpr typeGuard = CelZ3TypeSystem.mkAndFlattened(ctx, typeGuards);
134+
BoolExpr typeGuard = CelZ3Exprs.mkAndFlattened(ctx, typeGuards);
135135
currentZ3Result = ctx.mkITE(typeGuard, evaluatedResult.z3Expr(), currentZ3Result);
136136
currentApprox =
137137
(BoolExpr) ctx.mkITE(typeGuard, evaluatedResult.isApproximate(), currentApprox);
@@ -144,7 +144,7 @@ Optional<TranslatedValue> translateFunctionCall(
144144
Operator op = opOpt.orElse(null);
145145
if (op == Operator.IN) {
146146
currentApprox =
147-
CelZ3TypeSystem.mkOrFlattened(
147+
CelZ3Exprs.mkOrFlattened(
148148
ctx, currentApprox, constrainInWitnessTypes(args.get(0), args.get(1), ast));
149149
} else if (op == Operator.OPTIONAL_SELECT) {
150150
// A chained optional select (e.g. `a.?b.?c`) selects from the value of an optional operand.
@@ -154,7 +154,7 @@ Optional<TranslatedValue> translateFunctionCall(
154154
typeSystem.isOptional(operand),
155155
typeSystem.getOptionalValue(typeSystem.getOptionalRef(operand)),
156156
operand);
157-
currentApprox = CelZ3TypeSystem.mkOrFlattened(ctx, currentApprox, isTruncatedMap(target));
157+
currentApprox = CelZ3Exprs.mkOrFlattened(ctx, currentApprox, isTruncatedMap(target));
158158
}
159159

160160
return Optional.of(
@@ -216,7 +216,7 @@ private BoolExpr constrainInWitnessTypes(
216216
typeConstraintGenerator.apply(lhs, ((MapType) rhsType).keyType())));
217217
return isTruncatedMap(rhs);
218218
}
219-
return CelZ3TypeSystem.mkOrFlattened(
219+
return CelZ3Exprs.mkOrFlattened(
220220
ctx, isTruncatedMap(rhs), mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv));
221221
}
222222

@@ -385,7 +385,7 @@ private TranslatedValue translateBinaryLogicalAndOr(
385385
: ctx.mkITE(a.isZ3Unknown(), a.z3Expr(), b.z3Expr());
386386

387387
Expr<?> resultZ3 =
388-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
388+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
389389
.addCase(hasMatch, typeSystem.mkBool(!isAnd))
390390
.addCase(hasUnknown, unknownResult)
391391
.addCase(hasError, typeSystem.mkError())
@@ -394,10 +394,10 @@ private TranslatedValue translateBinaryLogicalAndOr(
394394
// An exact short-circuiting operand alone decides the result. Otherwise, an approximate operand
395395
// may really be the absorbing value (e.g. `unknown && false` is false).
396396
BoolExpr resultTaint =
397-
CelZ3TypeSystem.mkAndFlattened(
397+
CelZ3Exprs.mkAndFlattened(
398398
ctx,
399-
CelZ3TypeSystem.mkNotFlattened(ctx, hasSafeMatch),
400-
CelZ3TypeSystem.mkOrFlattened(ctx, a.isApproximate(), b.isApproximate()));
399+
CelZ3Exprs.mkNotFlattened(ctx, hasSafeMatch),
400+
CelZ3Exprs.mkOrFlattened(ctx, a.isApproximate(), b.isApproximate()));
401401

402402
return TranslatedValue.create(resultZ3, typeSystem, resultTaint);
403403
}
@@ -435,7 +435,7 @@ private TranslatedValue translateNegate(TranslatedValue arg, CelAbstractSyntaxTr
435435
typeSystem.wrapInt((IntExpr) intNeg), typeSystem.checkIntOverflow(intNeg));
436436
Expr<?> doubleResult = typeSystem.wrapDouble(ctx.mkFPNeg(typeSystem.getDouble(z3Expr)));
437437
result =
438-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
438+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
439439
.addCase(typeSystem.isInt(z3Expr), intResult)
440440
.addCase(typeSystem.isDouble(z3Expr), doubleResult)
441441
.build(typeSystem.mkError());
@@ -498,7 +498,7 @@ private BoolExpr getNumericEqualityWithConstant(
498498
BoolExpr doubleEq = ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal));
499499

500500
return (BoolExpr)
501-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
501+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
502502
.addCase(typeSystem.isInt(symVal), intEq)
503503
.addCase(typeSystem.isUint(symVal), uintEq)
504504
.addCase(typeSystem.isDouble(symVal), doubleEq)
@@ -610,7 +610,7 @@ private BoolExpr getDynamicNumericEquality(Expr<?> z3Expr0, Expr<?> z3Expr1) {
610610
ctx.mkLe(ctx.mkFPToReal(fpVal0), realVal1));
611611

612612
return (BoolExpr)
613-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
613+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
614614
.addCase(bothIntOrUint, ctx.mkEq(val0, val1))
615615
.addCase(
616616
bothDouble,
@@ -672,7 +672,7 @@ private BoolExpr unrollListEquality(
672672
taints.add(elemEquality.isApproximate());
673673
}
674674

675-
return CelZ3TypeSystem.mkAndFlattened(ctx, equalities);
675+
return CelZ3Exprs.mkAndFlattened(ctx, equalities);
676676
}
677677

678678
private void constrainListElement(SeqExpr<?> seq, IntExpr idx, Expr<?> elem, CelType listType) {
@@ -740,7 +740,7 @@ private TranslatedValue translateEquality(
740740
String opName = isEquals ? Operator.EQUALS.getFunction() : Operator.NOT_EQUALS.getFunction();
741741

742742
return TranslatedValue.propagateStrict(ctx, typeSystem, opName, equalityExpr, arg0, arg1)
743-
.withApproximation(CelZ3TypeSystem.mkOrFlattened(ctx, taints));
743+
.withApproximation(CelZ3Exprs.mkOrFlattened(ctx, taints));
744744
}
745745

746746
private Expr<?> buildListIndex(
@@ -814,12 +814,12 @@ private ProbeResult createProbeResult(
814814
BoolExpr inMap2 = (BoolExpr) ctx.mkSelect(mapPresence, key2);
815815
Expr<?> val2 = ctx.mkSelect(mapValues, key2);
816816

817-
BoolExpr condMap1 = CelZ3TypeSystem.mkAndFlattened(ctx, cond1, inMap1);
818-
BoolExpr condMap2 = CelZ3TypeSystem.mkAndFlattened(ctx, cond2, inMap2);
817+
BoolExpr condMap1 = CelZ3Exprs.mkAndFlattened(ctx, cond1, inMap1);
818+
BoolExpr condMap2 = CelZ3Exprs.mkAndFlattened(ctx, cond2, inMap2);
819819

820-
BoolExpr altInMap = CelZ3TypeSystem.mkOrFlattened(ctx, inMapOrig, condMap1, condMap2);
820+
BoolExpr altInMap = CelZ3Exprs.mkOrFlattened(ctx, inMapOrig, condMap1, condMap2);
821821
Expr<?> altVal =
822-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
822+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
823823
.addCase(inMapOrig, valOrig)
824824
.addCase(condMap1, val1)
825825
.addCase(condMap2, val2)
@@ -912,14 +912,14 @@ private Expr<?> buildMapIndex(
912912

913913
BoolExpr finalInMap =
914914
(BoolExpr)
915-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
915+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
916916
.addCase(isInt, intProbe.altInMap)
917917
.addCase(isUint, uintProbe.altInMap)
918918
.addCase(isDouble, doubleProbe.altInMap)
919919
.build(inMapOrig);
920920

921921
Expr<?> finalVal =
922-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
922+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
923923
.addCase(isInt, intProbe.altVal)
924924
.addCase(isUint, uintProbe.altVal)
925925
.addCase(isDouble, doubleProbe.altVal)
@@ -992,7 +992,7 @@ private TranslatedValue translateIndex(
992992
BoolExpr isMapIndexTruncated = ctx.mkAnd(shouldEvaluate, isTruncatedMap(lhsTrans));
993993
return TranslatedValue.propagateStrict(ctx, typeSystem, opName, actualValue, args)
994994
.withApproximation(
995-
CelZ3TypeSystem.mkOrFlattened(
995+
CelZ3Exprs.mkOrFlattened(
996996
ctx, isListIndexTruncated, isMapIndexTruncated, element.isApproximate()));
997997
}
998998

@@ -1040,16 +1040,16 @@ private TranslatedValue buildAndConstrainIndex(
10401040
return TranslatedValue.create(
10411041
actualValue,
10421042
typeSystem,
1043-
CelZ3TypeSystem.mkAndFlattened(
1044-
ctx, isDefined, CelZ3TypeSystem.mkNotFlattened(ctx, typeConstraint)));
1043+
CelZ3Exprs.mkAndFlattened(
1044+
ctx, isDefined, CelZ3Exprs.mkNotFlattened(ctx, typeConstraint)));
10451045
}
10461046

10471047
BoolExpr isListGuard =
10481048
ctx.mkAnd(shouldEvaluate, typeSystem.isList(lhsTrans), typeSystem.isInt(rhsTrans));
10491049
BoolExpr isMapGuard = ctx.mkAnd(shouldEvaluate, typeSystem.isMap(lhsTrans));
10501050

10511051
return TranslatedValue.create(
1052-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
1052+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
10531053
.addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional))
10541054
.addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional))
10551055
.build(typeSystem.mkError()),
@@ -1080,7 +1080,7 @@ private TranslatedValue translateConditional(
10801080
: cond.z3Expr();
10811081

10821082
Expr<?> resultZ3 =
1083-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
1083+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
10841084
.addCase(hasUnknown, unknownResult)
10851085
.addCase(hasError, typeSystem.mkError())
10861086
.addCase(condTrue, trueBranch.z3Expr())
@@ -1091,7 +1091,7 @@ private TranslatedValue translateConditional(
10911091

10921092
BoolExpr resultTaint =
10931093
(BoolExpr)
1094-
CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx)
1094+
CelZ3Exprs.SwitchBuilder.newBuilder(ctx)
10951095
.addCase(hasUnknown, ctx.mkNot(hasSafeUnknown))
10961096
.addCase(hasError, ctx.mkNot(hasSafeError))
10971097
.addCase(condTrue, ctx.mkOr(cond.isApproximate(), trueBranch.isApproximate()))
@@ -1163,7 +1163,7 @@ private BoolExpr mayObserveTruncatedTypeConstraint(
11631163
if (Arrays.stream(args).allMatch(arg -> isConcrete(extractAstTypeOrDefault(arg, ast)))) {
11641164
return ctx.mkFalse();
11651165
}
1166-
return CelZ3TypeSystem.mkOrFlattened(
1166+
return CelZ3Exprs.mkOrFlattened(
11671167
ctx,
11681168
Arrays.stream(args)
11691169
.map(arg -> typeSystem.hasTruncatedTypeConstraint(arg.z3Expr()))

0 commit comments

Comments
 (0)