diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index bd455ab50..f25fdaea2 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel @@ -112,7 +112,10 @@ java_library( java_library( name = "type_system", - srcs = ["CelZ3TypeSystem.java"], + srcs = [ + "CelZ3Exprs.java", + "CelZ3TypeSystem.java", + ], compatible_with = [], tags = [ ], diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 913582ee4..e5fe3562a 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -112,7 +112,7 @@ Set getTypeConstraints() { } BoolExpr hasTruncation() { - return CelZ3TypeSystem.mkOrFlattened(ctx, truncationConditions); + return CelZ3Exprs.mkOrFlattened(ctx, truncationConditions); } CelZ3TypeSystem getTypeSystem() { @@ -806,7 +806,7 @@ private FieldAccess getMapAccess(Expr operand, String field, BoolExpr typeGua BoolExpr presence = (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), mapFieldZ3Str); Expr value = ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), mapFieldZ3Str); - constrainPresentValue(CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, presence), value); + constrainPresentValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value); return new FieldAccess(presence, value); } @@ -816,7 +816,7 @@ private FieldAccess getMsgAccess(Expr operand, String field, BoolExpr typeGua BoolExpr presence = (BoolExpr) ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), msgFieldZ3Str); Expr value = ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), msgFieldZ3Str); - constrainPresentValue(CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, presence), value); + constrainPresentValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value); return new FieldAccess(presence, value); } @@ -853,7 +853,7 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a FieldAccess msgAcc = getMsgAccess(operand, field, isMessage); presenceResult = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(isMessage, msgAcc.presence) .addCase(isMap, mapAcc.presence) .build(ctx.mkFalse()); @@ -863,7 +863,7 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a Expr mapRead = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError()); valueResult = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(isMessage, msgRead) .addCase(isMap, mapRead) .build(typeSystem.mkError()); @@ -1060,7 +1060,7 @@ private TranslatedValue translateComprehension(CelExpr celExpr, CelAbstractSynta TranslatedValue resultTv = withScope( comp.accuVar(), - TranslatedValue.create(accu, typeSystem, CelZ3TypeSystem.mkOrFlattened(ctx, taints)), + TranslatedValue.create(accu, typeSystem, CelZ3Exprs.mkOrFlattened(ctx, taints)), () -> translateExpr(comp.result(), ast)); Expr result = resultTv.z3Expr(); return TranslatedValue.create( @@ -1152,7 +1152,7 @@ private BoolExpr getBoundedMapBijection( seqMap); } constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap))); - return CelZ3TypeSystem.mkAndFlattened(ctx, constraints); + return CelZ3Exprs.mkAndFlattened(ctx, constraints); } private T withIterationScope( @@ -1301,8 +1301,7 @@ private TranslatedValue unrollMapAndFilter( TranslatedValue resultTv = withScope( comp.accuVar(), - TranslatedValue.create( - chainedAccu, typeSystem, CelZ3TypeSystem.mkOrFlattened(ctx, taints)), + TranslatedValue.create(chainedAccu, typeSystem, CelZ3Exprs.mkOrFlattened(ctx, taints)), () -> translateExpr(comp.result(), ast)); Expr iterRangeExpr = iterRangeTv.z3Expr(); @@ -1313,10 +1312,10 @@ private TranslatedValue unrollMapAndFilter( // result of any non-true condition, since the unrolled value ignores early exits. BoolExpr isConditionUnmodeled = ctx.mkBool(!isLiteralTrue(comp.loopCondition())); BoolExpr isAbstracted = - CelZ3TypeSystem.mkOrFlattened(ctx, rangeIsUnknown, isTruncated, isConditionUnmodeled); + CelZ3Exprs.mkOrFlattened(ctx, rangeIsUnknown, isTruncated, isConditionUnmodeled); // An error is not final when truncated: an unknown from a later iteration overrides it. Expr finalResult = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(rangeIsError, typeSystem.mkError()) .addCase(isAbstracted, mkParameterizedUnknown(celExpr, ast)) .build(resultTv.z3Expr()); @@ -1326,7 +1325,7 @@ private TranslatedValue unrollMapAndFilter( ctx.mkITE( ctx.mkOr(rangeIsError, rangeIsUnknown), iterRangeTv.isApproximate(), - CelZ3TypeSystem.mkOrFlattened( + CelZ3Exprs.mkOrFlattened( ctx, resultTv.isApproximate(), isTruncated, isConditionUnmodeled)); return TranslatedValue.create(finalResult, celExpr, typeSystem, finalTaint); @@ -1379,36 +1378,36 @@ private TranslatedValue reduceAllOrExists( BoolExpr isActive = iter.inBounds; - hasMatchList.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, isMatch)); - hasErrorList.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, isE)); - hasUnknownList.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, isU)); + hasMatchList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isMatch)); + hasErrorList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isE)); + hasUnknownList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isU)); hasSafeMatchList.add( - CelZ3TypeSystem.mkAndFlattened( - ctx, isActive, isMatch, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate()))); + CelZ3Exprs.mkAndFlattened( + ctx, isActive, isMatch, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate()))); hasSafeErrorList.add( - CelZ3TypeSystem.mkAndFlattened( - ctx, isActive, isE, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate()))); + CelZ3Exprs.mkAndFlattened( + ctx, isActive, isE, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate()))); hasSafeUnknownList.add( - CelZ3TypeSystem.mkAndFlattened( - ctx, isActive, isU, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate()))); - activeTaints.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, stepTv.isApproximate())); + CelZ3Exprs.mkAndFlattened( + ctx, isActive, isU, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate()))); + activeTaints.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, stepTv.isApproximate())); } - BoolExpr hasMatch = CelZ3TypeSystem.mkOrFlattened(ctx, hasMatchList); - BoolExpr hasError = CelZ3TypeSystem.mkOrFlattened(ctx, hasErrorList); - BoolExpr hasUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, hasUnknownList); + BoolExpr hasMatch = CelZ3Exprs.mkOrFlattened(ctx, hasMatchList); + BoolExpr hasError = CelZ3Exprs.mkOrFlattened(ctx, hasErrorList); + BoolExpr hasUnknown = CelZ3Exprs.mkOrFlattened(ctx, hasUnknownList); BoolExpr rangeIsError = typeSystem.isError(iterRangeTv.z3Expr()); BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeTv.z3Expr()); - BoolExpr hasSafeMatch = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeMatchList); - BoolExpr hasSafeError = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeErrorList); - BoolExpr hasSafeUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, hasSafeUnknownList); - BoolExpr anyActiveTaint = CelZ3TypeSystem.mkOrFlattened(ctx, activeTaints); + BoolExpr hasSafeMatch = CelZ3Exprs.mkOrFlattened(ctx, hasSafeMatchList); + BoolExpr hasSafeError = CelZ3Exprs.mkOrFlattened(ctx, hasSafeErrorList); + BoolExpr hasSafeUnknown = CelZ3Exprs.mkOrFlattened(ctx, hasSafeUnknownList); + BoolExpr anyActiveTaint = CelZ3Exprs.mkOrFlattened(ctx, activeTaints); Expr comprehensionUnknown = mkParameterizedUnknown(compExpr, ast); Expr result = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(rangeIsError, typeSystem.mkError()) .addCase(rangeIsUnknown, comprehensionUnknown) .addCase(hasMatch, typeSystem.mkBool(!isAll)) @@ -1416,13 +1415,12 @@ private TranslatedValue reduceAllOrExists( .addCase(hasError, typeSystem.mkError()) .build(typeSystem.mkBool(isAll)); - BoolExpr baseTaint = - CelZ3TypeSystem.mkOrFlattened(ctx, anyActiveTaint, iterRangeTv.isApproximate()); + BoolExpr baseTaint = CelZ3Exprs.mkOrFlattened(ctx, anyActiveTaint, iterRangeTv.isApproximate()); // Taint identically shadows the value flow's short-circuit control structure BoolExpr resultTaint = (BoolExpr) - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(ctx.mkOr(rangeIsError, rangeIsUnknown), iterRangeTv.isApproximate()) .addCase(hasMatch, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeMatch))) .addCase( @@ -1562,7 +1560,7 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint)); } - return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); + return CelZ3Exprs.mkAndFlattened(ctx, boundsAndTypes); } if (type instanceof MapType) { // Do NOT emit a for-all quantifier over map keys or values here. @@ -1614,7 +1612,7 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType))); } - return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); + return CelZ3Exprs.mkAndFlattened(ctx, boundsAndTypes); } if (type.kind() == CelKind.STRUCT) { return ctx.mkAnd( diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index c2a505216..ceb5ae3d8 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -227,7 +227,7 @@ public CelVerificationResult verifyEquivalence( // an unknown only by its attributes (e.g. `a && true` and `a` both yield unknown {a}). Two // distinct unknowns may thus still be equivalent. BoolExpr combinedTaint = - CelZ3TypeSystem.mkOrFlattened( + CelZ3Exprs.mkOrFlattened( ctx, tvA.isApproximate(), tvB.isApproximate(), @@ -318,7 +318,7 @@ CelVerificationResult verifyImplication( BoolExpr violationCondition = ctx.mkAnd(assumeCondition, ctx.mkNot(assertCondition)); BoolExpr combinedTaint = - CelZ3TypeSystem.mkOrFlattened(ctx, assumeTv.isApproximate(), assertTv.isApproximate()); + CelZ3Exprs.mkOrFlattened(ctx, assumeTv.isApproximate(), assertTv.isApproximate()); BoolExpr unknownCondition = ctx.mkOr( translator.getTypeSystem().isUnknown(assumeTv.z3Expr()), diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java b/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java new file mode 100644 index 000000000..b2b4d86dd --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3Exprs.java @@ -0,0 +1,160 @@ +// Copyright 2026 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// https://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +package dev.cel.verifier; + +import com.google.common.collect.Lists; +import com.google.errorprone.annotations.CanIgnoreReturnValue; +import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.Context; +import com.microsoft.z3.Expr; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; + +/** Helpers for building Z3 expressions that are independent of the CEL encoding. */ +public final class CelZ3Exprs { + + /** + * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs. + * + *

Returns {@code false} if the list is empty. + */ + public static BoolExpr mkOrFlattened(Context ctx, BoolExpr... args) { + return mkOrFlattened(ctx, Arrays.asList(args)); + } + + /** + * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs. + * + *

Returns {@code false} if the list is empty. + */ + public static BoolExpr mkOrFlattened(Context ctx, List args) { + // Pruning true/false constants in Java is significantly faster than building + // larger ASTs and letting Z3 process them natively. + List filteredArgs = new ArrayList<>(); + for (BoolExpr arg : args) { + if (arg.isTrue()) { + return ctx.mkTrue(); + } + if (!arg.isFalse()) { + filteredArgs.add(arg); + } + } + if (filteredArgs.isEmpty()) { + return ctx.mkFalse(); + } + if (filteredArgs.size() == 1) { + return filteredArgs.get(0); + } + return ctx.mkOr(filteredArgs.toArray(new BoolExpr[0])); + } + + /** + * Helper to construct a flattened logical AND expression to avoid deep left-leaning ASTs. + * + *

Returns {@code true} if the list is empty. + */ + public static BoolExpr mkAndFlattened(Context ctx, BoolExpr... args) { + return mkAndFlattened(ctx, Arrays.asList(args)); + } + + public static BoolExpr mkAndFlattened(Context ctx, List args) { + // Pruning true/false constants in Java is significantly faster than building + // larger ASTs and letting Z3 process them natively. + List filteredArgs = new ArrayList<>(); + for (BoolExpr arg : args) { + if (arg.isFalse()) { + return ctx.mkFalse(); + } + if (!arg.isTrue()) { + filteredArgs.add(arg); + } + } + if (filteredArgs.isEmpty()) { + return ctx.mkTrue(); + } + if (filteredArgs.size() == 1) { + return filteredArgs.get(0); + } + return ctx.mkAnd(filteredArgs.toArray(new BoolExpr[0])); + } + + /** Helper to construct a logical NOT expression while avoiding redundant NOT operations. */ + public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) { + if (arg.isTrue()) { + return ctx.mkFalse(); + } + if (arg.isFalse()) { + return ctx.mkTrue(); + } + return ctx.mkNot(arg); + } + + /** + * Helper to build a chain of nested ITE (If-Then-Else) conditions. + * + *

Conditions are evaluated in the order they are added. Branches with {@code isFalse()} + * conditions are skipped, and redundant {@code ITE(condition, X, X)} creations are omitted to + * avoid allocating dead AST paths in Z3. + */ + public static final class SwitchBuilder { + + private static final class SwitchCase { + private final BoolExpr condition; + private final Expr value; + + private SwitchCase(BoolExpr condition, Expr value) { + this.condition = condition; + this.value = value; + } + } + + private final Context ctx; + private final List cases; + + public static SwitchBuilder newBuilder(Context ctx) { + return new SwitchBuilder(ctx); + } + + @CanIgnoreReturnValue + public SwitchBuilder addCase(BoolExpr condition, Expr value) { + // Skip branches that can never be hit (e.g. `isFalse()` probes). + if (condition.isFalse()) { + return this; + } + cases.add(new SwitchCase(condition, value)); + return this; + } + + public Expr build(Expr defaultFallback) { + Expr result = defaultFallback; + for (SwitchCase c : Lists.reverse(cases)) { + // ITE(condition, X, X) simplifies to X; skip calling into native C++ Z3_mk_ite. + if (c.value.equals(result)) { + continue; + } + result = ctx.mkITE(c.condition, c.value, result); + } + return result; + } + + private SwitchBuilder(Context ctx) { + this.ctx = ctx; + this.cases = new ArrayList<>(); + } + } + + private CelZ3Exprs() {} +} diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index d4fd31962..eb4b7636e 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -131,7 +131,7 @@ Optional translateFunctionCall( typeGuards.add(mkTypeGuard(z3Args.get(i), overload.parameterTypes().get(i))); } - BoolExpr typeGuard = CelZ3TypeSystem.mkAndFlattened(ctx, typeGuards); + BoolExpr typeGuard = CelZ3Exprs.mkAndFlattened(ctx, typeGuards); currentZ3Result = ctx.mkITE(typeGuard, evaluatedResult.z3Expr(), currentZ3Result); currentApprox = (BoolExpr) ctx.mkITE(typeGuard, evaluatedResult.isApproximate(), currentApprox); @@ -144,7 +144,7 @@ Optional translateFunctionCall( Operator op = opOpt.orElse(null); if (op == Operator.IN) { currentApprox = - CelZ3TypeSystem.mkOrFlattened( + CelZ3Exprs.mkOrFlattened( ctx, currentApprox, constrainInWitnessTypes(args.get(0), args.get(1), ast)); } else if (op == Operator.OPTIONAL_SELECT) { // A chained optional select (e.g. `a.?b.?c`) selects from the value of an optional operand. @@ -154,7 +154,7 @@ Optional translateFunctionCall( typeSystem.isOptional(operand), typeSystem.getOptionalValue(typeSystem.getOptionalRef(operand)), operand); - currentApprox = CelZ3TypeSystem.mkOrFlattened(ctx, currentApprox, isTruncatedMap(target)); + currentApprox = CelZ3Exprs.mkOrFlattened(ctx, currentApprox, isTruncatedMap(target)); } return Optional.of( @@ -216,7 +216,7 @@ private BoolExpr constrainInWitnessTypes( typeConstraintGenerator.apply(lhs, ((MapType) rhsType).keyType()))); return isTruncatedMap(rhs); } - return CelZ3TypeSystem.mkOrFlattened( + return CelZ3Exprs.mkOrFlattened( ctx, isTruncatedMap(rhs), mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv)); } @@ -385,7 +385,7 @@ private TranslatedValue translateBinaryLogicalAndOr( : ctx.mkITE(a.isZ3Unknown(), a.z3Expr(), b.z3Expr()); Expr resultZ3 = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(hasMatch, typeSystem.mkBool(!isAnd)) .addCase(hasUnknown, unknownResult) .addCase(hasError, typeSystem.mkError()) @@ -394,10 +394,10 @@ private TranslatedValue translateBinaryLogicalAndOr( // An exact short-circuiting operand alone decides the result. Otherwise, an approximate operand // may really be the absorbing value (e.g. `unknown && false` is false). BoolExpr resultTaint = - CelZ3TypeSystem.mkAndFlattened( + CelZ3Exprs.mkAndFlattened( ctx, - CelZ3TypeSystem.mkNotFlattened(ctx, hasSafeMatch), - CelZ3TypeSystem.mkOrFlattened(ctx, a.isApproximate(), b.isApproximate())); + CelZ3Exprs.mkNotFlattened(ctx, hasSafeMatch), + CelZ3Exprs.mkOrFlattened(ctx, a.isApproximate(), b.isApproximate())); return TranslatedValue.create(resultZ3, typeSystem, resultTaint); } @@ -435,7 +435,7 @@ private TranslatedValue translateNegate(TranslatedValue arg, CelAbstractSyntaxTr typeSystem.wrapInt((IntExpr) intNeg), typeSystem.checkIntOverflow(intNeg)); Expr doubleResult = typeSystem.wrapDouble(ctx.mkFPNeg(typeSystem.getDouble(z3Expr))); result = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(typeSystem.isInt(z3Expr), intResult) .addCase(typeSystem.isDouble(z3Expr), doubleResult) .build(typeSystem.mkError()); @@ -498,7 +498,7 @@ private BoolExpr getNumericEqualityWithConstant( BoolExpr doubleEq = ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); return (BoolExpr) - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(typeSystem.isInt(symVal), intEq) .addCase(typeSystem.isUint(symVal), uintEq) .addCase(typeSystem.isDouble(symVal), doubleEq) @@ -610,7 +610,7 @@ private BoolExpr getDynamicNumericEquality(Expr z3Expr0, Expr z3Expr1) { ctx.mkLe(ctx.mkFPToReal(fpVal0), realVal1)); return (BoolExpr) - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(bothIntOrUint, ctx.mkEq(val0, val1)) .addCase( bothDouble, @@ -672,7 +672,7 @@ private BoolExpr unrollListEquality( taints.add(elemEquality.isApproximate()); } - return CelZ3TypeSystem.mkAndFlattened(ctx, equalities); + return CelZ3Exprs.mkAndFlattened(ctx, equalities); } private void constrainListElement(SeqExpr seq, IntExpr idx, Expr elem, CelType listType) { @@ -740,7 +740,7 @@ private TranslatedValue translateEquality( String opName = isEquals ? Operator.EQUALS.getFunction() : Operator.NOT_EQUALS.getFunction(); return TranslatedValue.propagateStrict(ctx, typeSystem, opName, equalityExpr, arg0, arg1) - .withApproximation(CelZ3TypeSystem.mkOrFlattened(ctx, taints)); + .withApproximation(CelZ3Exprs.mkOrFlattened(ctx, taints)); } private Expr buildListIndex( @@ -814,12 +814,12 @@ private ProbeResult createProbeResult( BoolExpr inMap2 = (BoolExpr) ctx.mkSelect(mapPresence, key2); Expr val2 = ctx.mkSelect(mapValues, key2); - BoolExpr condMap1 = CelZ3TypeSystem.mkAndFlattened(ctx, cond1, inMap1); - BoolExpr condMap2 = CelZ3TypeSystem.mkAndFlattened(ctx, cond2, inMap2); + BoolExpr condMap1 = CelZ3Exprs.mkAndFlattened(ctx, cond1, inMap1); + BoolExpr condMap2 = CelZ3Exprs.mkAndFlattened(ctx, cond2, inMap2); - BoolExpr altInMap = CelZ3TypeSystem.mkOrFlattened(ctx, inMapOrig, condMap1, condMap2); + BoolExpr altInMap = CelZ3Exprs.mkOrFlattened(ctx, inMapOrig, condMap1, condMap2); Expr altVal = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(inMapOrig, valOrig) .addCase(condMap1, val1) .addCase(condMap2, val2) @@ -912,14 +912,14 @@ private Expr buildMapIndex( BoolExpr finalInMap = (BoolExpr) - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(isInt, intProbe.altInMap) .addCase(isUint, uintProbe.altInMap) .addCase(isDouble, doubleProbe.altInMap) .build(inMapOrig); Expr finalVal = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(isInt, intProbe.altVal) .addCase(isUint, uintProbe.altVal) .addCase(isDouble, doubleProbe.altVal) @@ -992,7 +992,7 @@ private TranslatedValue translateIndex( BoolExpr isMapIndexTruncated = ctx.mkAnd(shouldEvaluate, isTruncatedMap(lhsTrans)); return TranslatedValue.propagateStrict(ctx, typeSystem, opName, actualValue, args) .withApproximation( - CelZ3TypeSystem.mkOrFlattened( + CelZ3Exprs.mkOrFlattened( ctx, isListIndexTruncated, isMapIndexTruncated, element.isApproximate())); } @@ -1040,8 +1040,8 @@ private TranslatedValue buildAndConstrainIndex( return TranslatedValue.create( actualValue, typeSystem, - CelZ3TypeSystem.mkAndFlattened( - ctx, isDefined, CelZ3TypeSystem.mkNotFlattened(ctx, typeConstraint))); + CelZ3Exprs.mkAndFlattened( + ctx, isDefined, CelZ3Exprs.mkNotFlattened(ctx, typeConstraint))); } BoolExpr isListGuard = @@ -1049,7 +1049,7 @@ private TranslatedValue buildAndConstrainIndex( BoolExpr isMapGuard = ctx.mkAnd(shouldEvaluate, typeSystem.isMap(lhsTrans)); return TranslatedValue.create( - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional)) .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional)) .build(typeSystem.mkError()), @@ -1080,7 +1080,7 @@ private TranslatedValue translateConditional( : cond.z3Expr(); Expr resultZ3 = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(hasUnknown, unknownResult) .addCase(hasError, typeSystem.mkError()) .addCase(condTrue, trueBranch.z3Expr()) @@ -1091,7 +1091,7 @@ private TranslatedValue translateConditional( BoolExpr resultTaint = (BoolExpr) - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(hasUnknown, ctx.mkNot(hasSafeUnknown)) .addCase(hasError, ctx.mkNot(hasSafeError)) .addCase(condTrue, ctx.mkOr(cond.isApproximate(), trueBranch.isApproximate())) @@ -1163,7 +1163,7 @@ private BoolExpr mayObserveTruncatedTypeConstraint( if (Arrays.stream(args).allMatch(arg -> isConcrete(extractAstTypeOrDefault(arg, ast)))) { return ctx.mkFalse(); } - return CelZ3TypeSystem.mkOrFlattened( + return CelZ3Exprs.mkOrFlattened( ctx, Arrays.stream(args) .map(arg -> typeSystem.hasTruncatedTypeConstraint(arg.z3Expr())) diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index 7defbc706..d164505c4 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -16,10 +16,8 @@ import com.google.auto.value.AutoValue; import com.google.common.collect.ImmutableList; -import com.google.common.collect.Lists; import com.google.common.collect.ObjectArrays; import com.google.common.primitives.UnsignedLongs; -import com.google.errorprone.annotations.CanIgnoreReturnValue; import com.microsoft.z3.ArithExpr; import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; @@ -35,7 +33,6 @@ import com.microsoft.z3.Sort; import dev.cel.common.internal.ProtoTimeUtils; import java.math.BigInteger; -import java.util.ArrayList; import java.util.Arrays; import java.util.HashMap; import java.util.List; @@ -404,7 +401,7 @@ public BoolExpr getStructuralEquality(Expr arg0, Expr arg1) { // For primitives, generic equality matches the direct Z3 datatype wrapper. BoolExpr genericEq = ctx.mkEq(arg0, arg1); return (BoolExpr) - SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(isListEq, seqEq) .addCase(isMapEq, mapEq) .addCase(isMsgEq, msgEq) @@ -489,7 +486,7 @@ Expr propagateErrorAndUnknown( BoolExpr hasError = ctx.mkOr(errors); BoolExpr hasUnknown = ctx.mkOr(unknowns); // Unknowns have higher precedence than error - return SwitchBuilder.newBuilder(ctx) + return CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(hasUnknown, unknownResult) .addCase(hasError, mkError()) .build(result); @@ -797,60 +794,6 @@ public SeqExpr mkConcatSafe(Expr arg1, Expr arg2) { return ctx.mkConcat((Expr>) arg1, (Expr>) arg2); } - /** - * Helper to build a chain of nested ITE (If-Then-Else) conditions. - * - *

Conditions are evaluated in the order they are added. Branches with {@code isFalse()} - * conditions are skipped, and redundant {@code ITE(condition, X, X)} creations are omitted to - * avoid allocating dead AST paths in Z3. - */ - public static final class SwitchBuilder { - - private static final class SwitchCase { - private final BoolExpr condition; - private final Expr value; - - private SwitchCase(BoolExpr condition, Expr value) { - this.condition = condition; - this.value = value; - } - } - - private final Context ctx; - private final List cases; - - public static SwitchBuilder newBuilder(Context ctx) { - return new SwitchBuilder(ctx); - } - - @CanIgnoreReturnValue - public SwitchBuilder addCase(BoolExpr condition, Expr value) { - // Skip branches that can never be hit (e.g. `isFalse()` probes). - if (condition.isFalse()) { - return this; - } - cases.add(new SwitchCase(condition, value)); - return this; - } - - public Expr build(Expr defaultFallback) { - Expr result = defaultFallback; - for (SwitchCase c : Lists.reverse(cases)) { - // ITE(condition, X, X) simplifies to X; skip calling into native C++ Z3_mk_ite. - if (c.value.equals(result)) { - continue; - } - result = ctx.mkITE(c.condition, c.value, result); - } - return result; - } - - private SwitchBuilder(Context ctx) { - this.ctx = ctx; - this.cases = new ArrayList<>(); - } - } - @AutoValue abstract static class FuncDeclKey { abstract String name(); @@ -864,82 +807,6 @@ private static FuncDeclKey create(String name, Sort[] domain, Sort range) { } } - /** - * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs. - * - *

Returns {@code false} if the list is empty. - */ - public static BoolExpr mkOrFlattened(Context ctx, BoolExpr... args) { - return mkOrFlattened(ctx, Arrays.asList(args)); - } - - /** - * Helper to construct a flattened logical OR expression to avoid deep left-leaning ASTs. - * - *

Returns {@code false} if the list is empty. - */ - public static BoolExpr mkOrFlattened(Context ctx, List args) { - // Pruning true/false constants in Java is significantly faster than building - // larger ASTs and letting Z3 process them natively. - List filteredArgs = new ArrayList<>(); - for (BoolExpr arg : args) { - if (arg.isTrue()) { - return ctx.mkTrue(); - } - if (!arg.isFalse()) { - filteredArgs.add(arg); - } - } - if (filteredArgs.isEmpty()) { - return ctx.mkFalse(); - } - if (filteredArgs.size() == 1) { - return filteredArgs.get(0); - } - return ctx.mkOr(filteredArgs.toArray(new BoolExpr[0])); - } - - /** - * Helper to construct a flattened logical AND expression to avoid deep left-leaning ASTs. - * - *

Returns {@code true} if the list is empty. - */ - public static BoolExpr mkAndFlattened(Context ctx, BoolExpr... args) { - return mkAndFlattened(ctx, Arrays.asList(args)); - } - - public static BoolExpr mkAndFlattened(Context ctx, List args) { - // Pruning true/false constants in Java is significantly faster than building - // larger ASTs and letting Z3 process them natively. - List filteredArgs = new ArrayList<>(); - for (BoolExpr arg : args) { - if (arg.isFalse()) { - return ctx.mkFalse(); - } - if (!arg.isTrue()) { - filteredArgs.add(arg); - } - } - if (filteredArgs.isEmpty()) { - return ctx.mkTrue(); - } - if (filteredArgs.size() == 1) { - return filteredArgs.get(0); - } - return ctx.mkAnd(filteredArgs.toArray(new BoolExpr[0])); - } - - /** Helper to construct a logical NOT expression while avoiding redundant NOT operations. */ - public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) { - if (arg.isTrue()) { - return ctx.mkFalse(); - } - if (arg.isFalse()) { - return ctx.mkTrue(); - } - return ctx.mkNot(arg); - } - CelZ3TypeSystem(Context ctx, boolean parameterizeUnknowns) { this.ctx = ctx; this.funcDeclCache = new HashMap<>(); diff --git a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java index 7172a6a4f..7ea52abc8 100644 --- a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java +++ b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java @@ -160,14 +160,14 @@ static TranslatedValue propagateStrict( BoolExpr isError = ts.isError(z3Expr); BoolExpr isUnknown = ts.isUnknown(z3Expr); - BoolExpr isExact = CelZ3TypeSystem.mkNotFlattened(ctx, isApprox); + BoolExpr isExact = CelZ3Exprs.mkNotFlattened(ctx, isApprox); unknowns.add(isUnknown); - exactErrors.add(CelZ3TypeSystem.mkAndFlattened(ctx, isError, isExact)); - exactUnknowns.add(CelZ3TypeSystem.mkAndFlattened(ctx, isUnknown, isExact)); + exactErrors.add(CelZ3Exprs.mkAndFlattened(ctx, isError, isExact)); + exactUnknowns.add(CelZ3Exprs.mkAndFlattened(ctx, isUnknown, isExact)); } - BoolExpr anyTaint = CelZ3TypeSystem.mkOrFlattened(ctx, taints); + BoolExpr anyTaint = CelZ3Exprs.mkOrFlattened(ctx, taints); if (nonConstZ3Args.isEmpty()) { return create(baseResult, celExpr, ts, anyTaint); } @@ -175,19 +175,19 @@ static TranslatedValue propagateStrict( Expr finalResult = ts.propagateErrorAndUnknown(opName, baseResult, nonConstZ3Args, allZ3Args); - BoolExpr hasExactError = CelZ3TypeSystem.mkOrFlattened(ctx, exactErrors); - BoolExpr hasExactUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, exactUnknowns); - BoolExpr hasUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, unknowns); + BoolExpr hasExactError = CelZ3Exprs.mkOrFlattened(ctx, exactErrors); + BoolExpr hasExactUnknown = CelZ3Exprs.mkOrFlattened(ctx, exactUnknowns); + BoolExpr hasUnknown = CelZ3Exprs.mkOrFlattened(ctx, unknowns); BoolExpr isSafe = - CelZ3TypeSystem.mkOrFlattened( + CelZ3Exprs.mkOrFlattened( ctx, hasExactUnknown, - CelZ3TypeSystem.mkAndFlattened( - ctx, hasExactError, CelZ3TypeSystem.mkNotFlattened(ctx, hasUnknown)), - CelZ3TypeSystem.mkNotFlattened(ctx, anyTaint)); + CelZ3Exprs.mkAndFlattened( + ctx, hasExactError, CelZ3Exprs.mkNotFlattened(ctx, hasUnknown)), + CelZ3Exprs.mkNotFlattened(ctx, anyTaint)); - return create(finalResult, celExpr, ts, CelZ3TypeSystem.mkNotFlattened(ctx, isSafe)); + return create(finalResult, celExpr, ts, CelZ3Exprs.mkNotFlattened(ctx, isSafe)); } /** @@ -228,7 +228,7 @@ TranslatedValue withApproximation(BoolExpr approxCondition) { z3Expr(), celExpr(), typeSystem(), - CelZ3TypeSystem.mkOrFlattened(typeSystem().ctx(), isApproximate(), approxCondition)); + CelZ3Exprs.mkOrFlattened(typeSystem().ctx(), isApproximate(), approxCondition)); } } diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java index 35f96b7ef..dd983d36b 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java @@ -33,6 +33,7 @@ import com.microsoft.z3.SeqExpr; import dev.cel.common.CelFunctionDecl; import dev.cel.common.CelOverloadDecl; +import dev.cel.verifier.CelZ3Exprs; import dev.cel.verifier.CelZ3TypeSystem; import java.util.Optional; @@ -107,7 +108,7 @@ final class OptionalAxioms { Expr mapRef = ts.getMapRef(actualOperand); Expr presence = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase( isMsg, ctx.mkSelect((ArrayExpr) ts.getMsgPresence(msgRef), msgFieldZ3Str)) @@ -117,7 +118,7 @@ final class OptionalAxioms { .build(ctx.mkFalse()); Expr value = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase( isMsg, ctx.mkSelect((ArrayExpr) ts.getMsgValues(msgRef), msgFieldZ3Str)) .addCase( @@ -129,7 +130,7 @@ final class OptionalAxioms { BoolExpr shouldEvaluate = (BoolExpr) ctx.mkITE(isOpt, hasValue, ctx.mkTrue()); sink.accept( ctx.mkImplies( - CelZ3TypeSystem.mkAndFlattened( + CelZ3Exprs.mkAndFlattened( ctx, shouldEvaluate, isValidTarget, (BoolExpr) presence), valNotError)); diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java index 0d8698518..baebfff60 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java @@ -22,6 +22,7 @@ import dev.cel.common.types.MapType; import dev.cel.common.types.OptionalType; import dev.cel.common.types.SimpleType; +import dev.cel.verifier.CelZ3Exprs; import dev.cel.verifier.CelZ3TypeSystem; import java.util.Optional; @@ -48,7 +49,7 @@ final class TypeAxiom { .build(); private static Expr getTypeExpression(Context ctx, CelZ3TypeSystem typeSystem, Expr val) { - return CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + return CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase( typeSystem.isStruct(val), typeSystem.wrapString(typeSystem.getMsgTypeName(typeSystem.getMessageRef(val))))