diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index bd455ab50..b8d62a4d4 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 = [ ], @@ -157,10 +160,13 @@ java_library( "CelAstAlphaHasher.java", "CelAstToZ3Translator.java", "CelVerifierZ3Impl.java", + "CelZ3ComprehensionTranslator.java", "CelZ3CounterexampleGenerator.java", "CelZ3ExtensionalityAxioms.java", "CelZ3FunctionRegistry.java", "CelZ3OperatorTranslator.java", + "CelZ3TranslationContext.java", + "CelZ3TypeConstraintGenerator.java", "TranslatedValue.java", ], compatible_with = [], diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 913582ee4..778aa88d7 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -19,7 +19,6 @@ import com.google.common.collect.ImmutableSortedSet; import com.google.common.collect.Iterables; import com.google.common.collect.Streams; -import com.microsoft.z3.ArithExpr; import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; @@ -35,7 +34,6 @@ import dev.cel.common.ast.CelBlock; import dev.cel.common.ast.CelConstant; import dev.cel.common.ast.CelExpr; -import dev.cel.common.ast.CelExpr.CelComprehension; import dev.cel.common.ast.CelExpr.CelList; import dev.cel.common.ast.CelExpr.ExprKind; import dev.cel.common.types.CelKind; @@ -58,7 +56,6 @@ import java.util.Map; import java.util.Optional; import java.util.Set; -import java.util.function.Supplier; /** * Internal translator from CEL AST to Z3 SMT expressions using a 4-valued logic tagged union. @@ -91,14 +88,12 @@ final class CelAstToZ3Translator { private static final long MAX_UINT32 = 0xFFFFFFFFL; private final Context ctx; private final CelZ3TypeSystem typeSystem; + private final CelZ3TranslationContext context; + private final CelZ3TypeConstraintGenerator typeConstraintGenerator; private final CelZ3OperatorTranslator operatorTranslator; - private final Map symbolTable; - private final Set typeConstraints; - private final Map, CelType> inputVariableTypes; + private final CelZ3ComprehensionTranslator comprehensionTranslator; private final ImmutableSet unknownIdentifiers; - private final int comprehensionUnrollLimit; private final CelTypeProvider typeProvider; - private final List truncationConditions; private final Map> emptyMessageCache; private final Map> listLiteralCache; private Expr emptyListCache; @@ -108,11 +103,11 @@ final class CelAstToZ3Translator { * Returns a set of Z3 boolean expressions representing type constraints for the translated AST. */ Set getTypeConstraints() { - return typeConstraints; + return context.constraints(); } BoolExpr hasTruncation() { - return CelZ3TypeSystem.mkOrFlattened(ctx, truncationConditions); + return context.hasTruncation(); } CelZ3TypeSystem getTypeSystem() { @@ -131,7 +126,7 @@ BoolExpr isTrue(Expr celValue) { * reserved policy symbols such as 'rule.result' to the composed policy graph. */ void bindSymbol(String varName, TranslatedValue value) { - symbolTable.put(varName, value); + context.bindSymbol(varName, value); } TranslatedValue translate(CelAbstractSyntaxTree ast) { @@ -148,13 +143,13 @@ TranslatedValue translate(CelAbstractSyntaxTree ast) { Set> mapRefs = new LinkedHashSet<>(); Set> msgRefs = new LinkedHashSet<>(); - for (Expr constraint : typeConstraints) { + for (Expr constraint : context.constraints()) { collectReferences(constraint, visited, listRefs, mapRefs, msgRefs); } collectReferences(result.z3Expr(), visited, listRefs, mapRefs, msgRefs); - this.typeConstraints.addAll( - CelZ3ExtensionalityAxioms.generateAxioms(ctx, typeSystem, listRefs, mapRefs, msgRefs)); + CelZ3ExtensionalityAxioms.generateAxioms(ctx, typeSystem, listRefs, mapRefs, msgRefs) + .forEach(context::addConstraint); return result; } @@ -205,7 +200,7 @@ private TranslatedValue translateExpr(CelExpr celExpr, CelAbstractSyntaxTree ast case STRUCT: return translateStruct(celExpr, ast); case COMPREHENSION: - return translateComprehension(celExpr, ast); + return comprehensionTranslator.translateComprehension(celExpr, ast); default: throw new IllegalArgumentException("Unsupported expression kind: " + kind); } @@ -255,22 +250,22 @@ private TranslatedValue translateIdent(CelExpr celExpr, CelAbstractSyntaxTree as } } TranslatedValue tv = - symbolTable.computeIfAbsent( + context.computeSymbolIfAbsent( name, n -> { Expr v = ctx.mkConst(n, typeSystem.celValueSort()); - inputVariableTypes.put(v, type); + context.addInputVariable(v, type); // Variables at rest can never be pre-cooked Errors // Basically prevents error being a counterexample of var == var - typeConstraints.add(ctx.mkNot(typeSystem.isError(v))); + context.addConstraint(ctx.mkNot(typeSystem.isError(v))); - BoolExpr constraint = createTypeConstraint(v, exprId, ast); + BoolExpr constraint = typeConstraintGenerator.createTypeConstraint(v, exprId, ast); if (unknownIdentifiers.contains(name)) { - typeConstraints.add(ctx.mkOr(typeSystem.isUnknown(v), constraint)); + context.addConstraint(ctx.mkOr(typeSystem.isUnknown(v), constraint)); } else { - typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(v))); - typeConstraints.add(constraint); + context.addConstraint(ctx.mkNot(typeSystem.isUnknown(v))); + context.addConstraint(constraint); } return TranslatedValue.create( @@ -324,7 +319,7 @@ private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast elementsTv.add(elem); } listRef = typeSystem.mkListRefConst(LIST_REF_PREFIX); - typeConstraints.add(ctx.mkEq(typeSystem.getSeq(listRef), seq)); + context.addConstraint(ctx.mkEq(typeSystem.getSeq(listRef), seq)); propagateTruncatedTypeConstraint(typeSystem.wrapList(listRef), values); Expr finalListRef = listRef; cacheKey.ifPresent(key -> listLiteralCache.put(key, finalListRef)); @@ -379,9 +374,9 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast) ctx.mkITE(finalPresence, ctx.mkStore(mapPresence, key, ctx.mkTrue()), mapPresence); } - typeConstraints.add(ctx.mkEq(typeSystem.getMapValues(mapRef), mapValues)); - typeConstraints.add(ctx.mkEq(typeSystem.getMapPresence(mapRef), mapPresence)); - typeConstraints.add(ctx.mkEq(typeSystem.getMapKeys(mapRef), keysSeq)); + context.addConstraint(ctx.mkEq(typeSystem.getMapValues(mapRef), mapValues)); + context.addConstraint(ctx.mkEq(typeSystem.getMapPresence(mapRef), mapPresence)); + context.addConstraint(ctx.mkEq(typeSystem.getMapKeys(mapRef), keysSeq)); Expr result = typeSystem.wrapMap(mapRef); propagateTruncatedTypeConstraint(result, values); @@ -398,7 +393,7 @@ private void propagateTruncatedTypeConstraint(Expr container, Iterable element : elements) { - typeConstraints.add( + context.addConstraint( ctx.mkImplies(typeSystem.hasTruncatedTypeConstraint(element), hasTruncated)); } } @@ -487,10 +482,10 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a ctx.mkITE(shouldBypass, msgPresence, ctx.mkStore(msgPresence, key, ctx.mkTrue())); } - typeConstraints.add( + context.addConstraint( ctx.mkEq(typeSystem.getMsgTypeName(msgRef), ctx.mkString(createStruct.messageName()))); - typeConstraints.add(ctx.mkEq(typeSystem.getMsgValues(msgRef), msgValues)); - typeConstraints.add(ctx.mkEq(typeSystem.getMsgPresence(msgRef), msgPresence)); + context.addConstraint(ctx.mkEq(typeSystem.getMsgValues(msgRef), msgValues)); + context.addConstraint(ctx.mkEq(typeSystem.getMsgPresence(msgRef), msgPresence)); Expr result = typeSystem.wrapMessage(msgRef); return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv); @@ -582,7 +577,8 @@ private TranslatedValue translateWrapperWktStruct( } entryTvs.add(entryTv); } - BoolExpr validValue = createTypeConstraintForType(currentVal, targetType); + BoolExpr validValue = + typeConstraintGenerator.createTypeConstraintForType(currentVal, targetType); if (typeName.equals(CelTypes.INT32_WRAPPER_MESSAGE)) { IntExpr intVal = typeSystem.getInt(currentVal); validValue = @@ -742,7 +738,7 @@ private Expr getDefaultValueForType(CelType type) { if (type instanceof ListType) { if (emptyListCache == null) { emptyListCache = typeSystem.mkListRefConst(EMPTY_LIST_PREFIX); - typeConstraints.add( + context.addConstraint( ctx.mkEq( typeSystem.getSeq(emptyListCache), ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort())))); @@ -752,15 +748,15 @@ private Expr getDefaultValueForType(CelType type) { if (type instanceof MapType) { if (emptyMapCache == null) { emptyMapCache = typeSystem.mkMapRefConst(EMPTY_MAP_PREFIX); - typeConstraints.add( + context.addConstraint( ctx.mkEq( typeSystem.getMapPresence(emptyMapCache), ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse()))); - typeConstraints.add( + context.addConstraint( ctx.mkEq( typeSystem.getMapValues(emptyMapCache), ctx.mkConstArray(typeSystem.celValueSort(), typeSystem.mkUnknown()))); - typeConstraints.add( + context.addConstraint( ctx.mkEq( typeSystem.getMapKeys(emptyMapCache), ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort())))); @@ -774,15 +770,15 @@ private Expr getDefaultValueForType(CelType type) { messageName, name -> { Expr ref = typeSystem.mkMessageRefConst(EMPTY_MSG_REF_PREFIX + name); - typeConstraints.add( + context.addConstraint( ctx.mkEq( typeSystem.getMsgPresence(ref), ctx.mkConstArray(ctx.getStringSort(), ctx.mkFalse()))); - typeConstraints.add( + context.addConstraint( ctx.mkEq( typeSystem.getMsgValues(ref), ctx.mkConstArray(ctx.getStringSort(), typeSystem.mkUnknown()))); - typeConstraints.add(ctx.mkEq(typeSystem.getMsgTypeName(ref), ctx.mkString(name))); + context.addConstraint(ctx.mkEq(typeSystem.getMsgTypeName(ref), ctx.mkString(name))); return ref; }); return typeSystem.wrapMessage(msgRef); @@ -806,7 +802,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); + context.constrainValidValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value); return new FieldAccess(presence, value); } @@ -816,14 +812,10 @@ 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); + context.constrainValidValue(CelZ3Exprs.mkAndFlattened(ctx, typeGuard, presence), value); return new FieldAccess(presence, value); } - private void constrainPresentValue(BoolExpr guard, Expr value) { - typeConstraints.add(ctx.mkImplies(guard, ctx.mkNot(typeSystem.isErrorOrUnknown(value)))); - } - private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) { CelExpr.CelSelect select = celExpr.select(); long exprId = celExpr.id(); @@ -853,7 +845,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 +855,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()); @@ -871,7 +863,7 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a Expr fieldAccess = select.testOnly() ? typeSystem.wrapBool(presenceResult) : valueResult; - typeConstraints.add(createTypeConstraint(fieldAccess, exprId, ast)); + context.addConstraint(typeConstraintGenerator.createTypeConstraint(fieldAccess, exprId, ast)); TranslatedValue result = TranslatedValue.propagateStrict( @@ -892,7 +884,7 @@ private TranslatedValue translateBlock( TranslatedValue subExprVal = translateExpr(subExprAst, ast); String varName = CelBlock.INDEX_PREFIX + currentIndex; - return withScope( + return context.withScope( varName, subExprVal, () -> translateBlock(boundExprs, currentIndex + 1, resultExpr, ast)); } @@ -936,9 +928,10 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { Expr[] exprArgs = args.stream().map(TranslatedValue::z3Expr).toArray(Expr[]::new); Expr callRes = ctx.mkApp(funcDecl, exprArgs); - typeConstraints.add(createTypeConstraint(callRes, exprId, ast)); - typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes))); - typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes))); + context.addConstraint( + typeConstraintGenerator.createTypeConstraint(callRes, exprId, ast)); + context.addConstraint(ctx.mkNot(typeSystem.isUnknown(callRes))); + context.addConstraint(ctx.mkNot(typeSystem.isError(callRes))); // The solver picks the result freely, so a model depending on it is never exact. return TranslatedValue.propagateStrict( @@ -976,666 +969,10 @@ private static boolean mayEmbedArgs(String functionName, CelType resultType) { && !functionName.equals(Operator.CONDITIONAL.getFunction()); } - private T withScope(String varName, TranslatedValue value, Supplier action) { - TranslatedValue prev = symbolTable.put(varName, value); - try { - return action.get(); - } finally { - if (prev != null) { - symbolTable.put(varName, prev); - } else { - symbolTable.remove(varName); - } - } - } - - private TranslatedValue translateComprehension(CelExpr celExpr, CelAbstractSyntaxTree ast) { - CelComprehension comp = celExpr.comprehension(); - CelExpr iterRangeExpr = comp.iterRange(); - if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.IDENT) { - TranslatedValue boundTv = symbolTable.get(iterRangeExpr.ident().name()); - if (boundTv != null) { - iterRangeExpr = boundTv.celExpr().orElse(iterRangeExpr); - } - } - List iterationElements = new ArrayList<>(); - List taints = new ArrayList<>(); - List> allRangeElems = new ArrayList<>(); - - // For statically known list/map literals, unroll them exactly. - if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.LIST - && iterRangeExpr.list().optionalIndices().isEmpty()) { - ImmutableList elements = iterRangeExpr.list().elements(); - for (int i = 0; i < elements.size(); i++) { - TranslatedValue valueTv = translateExpr(elements.get(i), ast); - Expr value = valueTv.z3Expr(); - taints.add(valueTv.isApproximate()); - iterationElements.add(new IterationElement(typeSystem.mkInt(i), value)); - allRangeElems.add(value); - } - } else if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.MAP - && iterRangeExpr.map().entries().stream().noneMatch(CelExpr.CelMap.Entry::optionalEntry)) { - for (CelExpr.CelMap.Entry entry : iterRangeExpr.map().entries()) { - TranslatedValue keyTv = translateExpr(entry.key(), ast); - Expr key = keyTv.z3Expr(); - taints.add(keyTv.isApproximate()); - TranslatedValue valueTv = translateExpr(entry.value(), ast); - Expr value = valueTv.z3Expr(); - taints.add(valueTv.isApproximate()); - iterationElements.add(new IterationElement(key, value)); - allRangeElems.add(key); - allRangeElems.add(value); - } - } else { - return translateDynamicComprehension(celExpr, ast); - } - - TranslatedValue accuTv = translateExpr(comp.accuInit(), ast); - Expr accu = accuTv.z3Expr(); - taints.add(accuTv.isApproximate()); - boolean isMap = iterRangeExpr.exprKind().getKind() == ExprKind.Kind.MAP; - boolean isTwoVar = !comp.iterVar2().isEmpty(); - - for (IterationElement iterElem : iterationElements) { - Expr currentAccu = accu; - accu = - withIterationScope( - comp, - iterElem.keyOrIndex, - iterElem.value, - currentAccu, - isMap, - isTwoVar, - () -> { - TranslatedValue condTv = translateExpr(comp.loopCondition(), ast); - TranslatedValue stepTv = translateExpr(comp.loopStep(), ast); - taints.add(stepTv.isApproximate()); - return ctx.mkITE( - (BoolExpr) typeSystem.unwrapBool(condTv.z3Expr()), - stepTv.z3Expr(), - currentAccu); - }); - } - - TranslatedValue resultTv = - withScope( - comp.accuVar(), - TranslatedValue.create(accu, typeSystem, CelZ3TypeSystem.mkOrFlattened(ctx, taints)), - () -> translateExpr(comp.result(), ast)); - Expr result = resultTv.z3Expr(); - return TranslatedValue.create( - typeSystem.propagateErrorAndUnknown( - "comprehension", - result, - allRangeElems, - ImmutableList.>builder().add(result).addAll(allRangeElems).build()), - celExpr, - typeSystem, - resultTv.isApproximate()); - } - private static CelType extractAstTypeOrDefault(CelAbstractSyntaxTree ast, long id) { return ast.getType(id).orElse(SimpleType.DYN); } - private static final class BoundedIteration { - private final BoolExpr inBounds; - private final TranslatedValue stepResult; - - private BoundedIteration(BoolExpr inBounds, TranslatedValue stepResult) { - this.inBounds = inBounds; - this.stepResult = stepResult; - } - } - - private TranslatedValue translateDynamicComprehension( - CelExpr celExpr, CelAbstractSyntaxTree ast) { - CelComprehension comp = celExpr.comprehension(); - TranslatedValue iterRangeTv = translateExpr(comp.iterRange(), ast); - Expr iterRange = iterRangeTv.z3Expr(); - CelType rangeType = extractAstTypeOrDefault(ast, comp.iterRange().id()); - - boolean isList = rangeType instanceof ListType; - boolean isMap = rangeType instanceof MapType; - if (!isList && !isMap) { - BoolExpr isRuntimeListOrMap = - ctx.mkOr(typeSystem.isList(iterRange), typeSystem.isMap(iterRange)); - Expr result = - ctx.mkITE(isRuntimeListOrMap, mkParameterizedUnknown(celExpr, ast), typeSystem.mkError()); - return TranslatedValue.create(result, celExpr, typeSystem, isRuntimeListOrMap); - } - - SeqExpr seq = - isMap - ? typeSystem.getMapKeys(typeSystem.getMapRef(iterRange)) - : typeSystem.getSeq(typeSystem.getListRef(iterRange)); - - ArithExpr lengthExpr = ctx.mkLength(seq); - ArrayExpr mapPresence = - isMap ? (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(iterRange)) : null; - - BoolExpr isValidRange = isMap ? typeSystem.isMap(iterRange) : typeSystem.isList(iterRange); - BoolExpr isTruncated = - ctx.mkAnd(isValidRange, ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit))); - truncationConditions.add(isTruncated); - - if (isAllMacro(comp) || isExistsMacro(comp)) { - return unrollAllAndExists( - celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv); - } else { - return unrollMapAndFilter( - celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv); - } - } - - private BoolExpr getBoundedMapBijection( - ArrayExpr mapPresence, SeqExpr seq, ArithExpr lengthExpr) { - List constraints = new ArrayList<>(); - for (int i = 0; i < comprehensionUnrollLimit; i++) { - for (int j = i + 1; j < comprehensionUnrollLimit; j++) { - BoolExpr validPair = ctx.mkLt(ctx.mkInt(j), lengthExpr); - BoolExpr notEqual = - ctx.mkNot(ctx.mkEq(ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkNth(seq, ctx.mkInt(j)))); - constraints.add(ctx.mkImplies(validPair, notEqual)); - } - } - - BoolExpr isNotTruncated = ctx.mkLe(lengthExpr, ctx.mkInt(comprehensionUnrollLimit)); - - ArrayExpr seqMap = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse()); - for (int i = 0; i < comprehensionUnrollLimit; i++) { - seqMap = - (ArrayExpr) - ctx.mkITE( - ctx.mkLt(ctx.mkInt(i), lengthExpr), - ctx.mkStore(seqMap, ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkTrue()), - seqMap); - } - constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap))); - return CelZ3TypeSystem.mkAndFlattened(ctx, constraints); - } - - private T withIterationScope( - CelComprehension comp, - Expr keyOrIndex, - Expr value, - Expr currentAccu, - boolean isMap, - boolean isTwoVar, - Supplier action) { - Supplier bindAccu = - () -> - withScope( - comp.accuVar(), - TranslatedValue.create(currentAccu, typeSystem, ctx.mkFalse()), - action); - - if (isTwoVar) { - return withScope( - comp.iterVar(), - TranslatedValue.create(keyOrIndex, typeSystem, ctx.mkFalse()), - () -> - withScope( - comp.iterVar2(), - TranslatedValue.create(value, typeSystem, ctx.mkFalse()), - bindAccu)); - } else { - Expr iterVal = isMap ? keyOrIndex : value; - return withScope( - comp.iterVar(), TranslatedValue.create(iterVal, typeSystem, ctx.mkFalse()), bindAccu); - } - } - - private IterationElement getIterationElement( - Expr xVal, IntExpr idx, Expr iterRange, boolean isMap, boolean isTwoVar) { - Expr keyOrIndex; - Expr value; - - if (isMap) { - keyOrIndex = xVal; - if (isTwoVar) { - Expr mapRef = typeSystem.getMapRef(iterRange); - ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef); - value = ctx.mkSelect(mapValues, keyOrIndex); - } else { - value = null; - } - } else { - if (isTwoVar) { - keyOrIndex = typeSystem.wrapInt(idx); - value = xVal; - } else { - keyOrIndex = null; - value = xVal; - } - } - return new IterationElement(keyOrIndex, value); - } - - private TranslatedValue unrollAllAndExists( - CelExpr celExpr, - CelAbstractSyntaxTree ast, - SeqExpr seq, - ArithExpr lengthExpr, - ArrayExpr mapPresence, - BoolExpr isTruncated, - TranslatedValue iterRangeTv) { - CelComprehension comp = celExpr.comprehension(); - List iterations = new ArrayList<>(); - TranslatedValue accuInitTv = translateExpr(comp.accuInit(), ast); - Expr accuInitExpr = accuInitTv.z3Expr(); - - boolean isMap = mapPresence != null; - boolean isTwoVar = !comp.iterVar2().isEmpty(); - - for (int i = 0; i < comprehensionUnrollLimit; i++) { - IntExpr idx = ctx.mkInt(i); - BoolExpr inBounds = ctx.mkLt(idx, lengthExpr); - Expr xVal = ctx.mkNth(seq, idx); - - constrainIterationElement(idx, lengthExpr, xVal, inBounds, mapPresence); - - IterationElement iterElem = - getIterationElement(xVal, idx, iterRangeTv.z3Expr(), isMap, isTwoVar); - - TranslatedValue stepTv = - withIterationScope( - comp, - iterElem.keyOrIndex, - iterElem.value, - accuInitExpr, - isMap, - isTwoVar, - () -> translateExpr(comp.loopStep(), ast)); - iterations.add(new BoundedIteration(inBounds, stepTv)); - } - - return reduceAllOrExists(iterations, isTruncated, iterRangeTv, isAllMacro(comp), celExpr, ast); - } - - private TranslatedValue unrollMapAndFilter( - CelExpr celExpr, - CelAbstractSyntaxTree ast, - SeqExpr seq, - ArithExpr lengthExpr, - ArrayExpr mapPresence, - BoolExpr isTruncated, - TranslatedValue iterRangeTv) { - CelComprehension comp = celExpr.comprehension(); - // For macros like map and filter, we must sequentially thread the accumulator through the loop - TranslatedValue chainedAccuTv = translateExpr(comp.accuInit(), ast); - Expr chainedAccu = chainedAccuTv.z3Expr(); - - boolean isMap = mapPresence != null; - boolean isTwoVar = !comp.iterVar2().isEmpty(); - - List taints = new ArrayList<>(); - taints.add(chainedAccuTv.isApproximate()); - taints.add(iterRangeTv.isApproximate()); - - for (int i = 0; i < comprehensionUnrollLimit; i++) { - IntExpr idx = ctx.mkInt(i); - BoolExpr inBounds = ctx.mkLt(idx, lengthExpr); - Expr xVal = ctx.mkNth(seq, idx); - - constrainIterationElement(idx, lengthExpr, xVal, inBounds, mapPresence); - - Expr currentAccu = chainedAccu; - IterationElement iterElem = - getIterationElement(xVal, idx, iterRangeTv.z3Expr(), isMap, isTwoVar); - - TranslatedValue stepTv = - withIterationScope( - comp, - iterElem.keyOrIndex, - iterElem.value, - currentAccu, - isMap, - isTwoVar, - () -> translateExpr(comp.loopStep(), ast)); - - taints.add(ctx.mkAnd(inBounds, stepTv.isApproximate())); - chainedAccu = ctx.mkITE(inBounds, stepTv.z3Expr(), currentAccu); - } - - TranslatedValue resultTv = - withScope( - comp.accuVar(), - TranslatedValue.create( - chainedAccu, typeSystem, CelZ3TypeSystem.mkOrFlattened(ctx, taints)), - () -> translateExpr(comp.result(), ast)); - - Expr iterRangeExpr = iterRangeTv.z3Expr(); - BoolExpr rangeIsError = typeSystem.isError(iterRangeExpr); - BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeExpr); - - // TODO: Model the loop condition for custom macros; until then, abstract the - // 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); - // An error is not final when truncated: an unknown from a later iteration overrides it. - Expr finalResult = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase(rangeIsError, typeSystem.mkError()) - .addCase(isAbstracted, mkParameterizedUnknown(celExpr, ast)) - .build(resultTv.z3Expr()); - - BoolExpr finalTaint = - (BoolExpr) - ctx.mkITE( - ctx.mkOr(rangeIsError, rangeIsUnknown), - iterRangeTv.isApproximate(), - CelZ3TypeSystem.mkOrFlattened( - ctx, resultTv.isApproximate(), isTruncated, isConditionUnmodeled)); - - return TranslatedValue.create(finalResult, celExpr, typeSystem, finalTaint); - } - - private void constrainIterationElement( - IntExpr idx, ArithExpr lengthExpr, Expr xVal, BoolExpr inBounds, ArrayExpr mapPresence) { - // Constrain out-of-bounds elements to prevent MBQI from infinitely instantiating list/map - // axioms - BoolExpr outOfBounds = ctx.mkGe(idx, lengthExpr); - typeConstraints.add(ctx.mkImplies(outOfBounds, ctx.mkEq(xVal, typeSystem.mkUnknown()))); - - // If we are iterating over a map, we can optionally bind the sequence elements - // to the map presence array to ensure the solver knows they correspond. - if (mapPresence != null) { - Expr selectExpr = ctx.mkSelect(mapPresence, xVal); - typeConstraints.add(ctx.mkImplies(inBounds, (BoolExpr) selectExpr)); - } - } - - private TranslatedValue reduceAllOrExists( - List iterations, - BoolExpr isTruncated, - TranslatedValue iterRangeTv, - boolean isAll, - CelExpr compExpr, - CelAbstractSyntaxTree ast) { - List hasMatchList = new ArrayList<>(); - List hasErrorList = new ArrayList<>(); - List hasUnknownList = new ArrayList<>(); - - List hasSafeMatchList = new ArrayList<>(); - List hasSafeErrorList = new ArrayList<>(); - List hasSafeUnknownList = new ArrayList<>(); - List activeTaints = new ArrayList<>(); - - for (BoundedIteration iter : iterations) { - TranslatedValue stepTv = iter.stepResult; - Expr step = stepTv.z3Expr(); - BoolExpr isBool = typeSystem.isBool(step); - BoolExpr unwrapStep = (BoolExpr) typeSystem.unwrapBool(step); - - // 'all' short-circuits on False, 'exists' short-circuits on True - BoolExpr matchCond = isAll ? ctx.mkNot(unwrapStep) : unwrapStep; - BoolExpr isMatch = ctx.mkAnd(isBool, matchCond); - - BoolExpr isU = typeSystem.isUnknown(step); - BoolExpr isE = - ctx.mkOr(typeSystem.isError(step), ctx.mkAnd(ctx.mkNot(isBool), ctx.mkNot(isU))); - - 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)); - - hasSafeMatchList.add( - CelZ3TypeSystem.mkAndFlattened( - ctx, isActive, isMatch, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate()))); - hasSafeErrorList.add( - CelZ3TypeSystem.mkAndFlattened( - ctx, isActive, isE, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate()))); - hasSafeUnknownList.add( - CelZ3TypeSystem.mkAndFlattened( - ctx, isActive, isU, CelZ3TypeSystem.mkNotFlattened(ctx, stepTv.isApproximate()))); - activeTaints.add(CelZ3TypeSystem.mkAndFlattened(ctx, isActive, stepTv.isApproximate())); - } - - BoolExpr hasMatch = CelZ3TypeSystem.mkOrFlattened(ctx, hasMatchList); - BoolExpr hasError = CelZ3TypeSystem.mkOrFlattened(ctx, hasErrorList); - BoolExpr hasUnknown = CelZ3TypeSystem.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); - - Expr comprehensionUnknown = mkParameterizedUnknown(compExpr, ast); - Expr result = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase(rangeIsError, typeSystem.mkError()) - .addCase(rangeIsUnknown, comprehensionUnknown) - .addCase(hasMatch, typeSystem.mkBool(!isAll)) - .addCase(ctx.mkOr(hasUnknown, isTruncated), comprehensionUnknown) - .addCase(hasError, typeSystem.mkError()) - .build(typeSystem.mkBool(isAll)); - - BoolExpr baseTaint = - CelZ3TypeSystem.mkOrFlattened(ctx, anyActiveTaint, iterRangeTv.isApproximate()); - - // Taint identically shadows the value flow's short-circuit control structure - BoolExpr resultTaint = - (BoolExpr) - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase(ctx.mkOr(rangeIsError, rangeIsUnknown), iterRangeTv.isApproximate()) - .addCase(hasMatch, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeMatch))) - .addCase( - ctx.mkOr(hasUnknown, isTruncated), - ctx.mkOr(iterRangeTv.isApproximate(), isTruncated, ctx.mkNot(hasSafeUnknown))) - .addCase(hasError, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeError))) - .build(baseTaint); - - return TranslatedValue.create(result, compExpr, typeSystem, resultTaint); - } - - private static boolean isAllMacro(CelComprehension comp) { - return isBooleanAccuInit(comp, true) - && isNotStrictlyFalseLoopCondition(comp, /* expectNot= */ false); - } - - private static boolean isExistsMacro(CelComprehension comp) { - return isBooleanAccuInit(comp, false) - && isNotStrictlyFalseLoopCondition(comp, /* expectNot= */ true); - } - - private static boolean isBooleanAccuInit(CelComprehension comp, boolean expectedValue) { - return comp.accuInit().constantOrDefault().getKind() == CelConstant.Kind.BOOLEAN_VALUE - && comp.accuInit().constant().booleanValue() == expectedValue; - } - - private static boolean isLiteralTrue(CelExpr expr) { - CelConstant constant = expr.constantOrDefault(); - return constant.getKind() == CelConstant.Kind.BOOLEAN_VALUE && constant.booleanValue(); - } - - private static boolean isNotStrictlyFalseLoopCondition(CelComprehension comp, boolean expectNot) { - CelExpr.CelCall call = comp.loopCondition().callOrDefault(); - if (!call.function().equals(Operator.NOT_STRICTLY_FALSE.getFunction()) - && !call.function().equals(Operator.OLD_NOT_STRICTLY_FALSE.getFunction())) { - return false; - } - CelExpr arg = call.args().get(0); - if (expectNot) { - CelExpr.CelCall notCall = arg.callOrDefault(); - if (!notCall.function().equals(Operator.LOGICAL_NOT.getFunction())) { - return false; - } - arg = notCall.args().get(0); - } - return arg.identOrDefault().name().equals(comp.accuVar()); - } - - private BoolExpr createTypeConstraint(Expr val, long exprId, CelAbstractSyntaxTree ast) { - CelType type = - ast.getType(exprId) - .orElseThrow( - () -> new IllegalArgumentException("Type not found for expr ID: " + exprId)); - BoolExpr typeConstraint = createTypeConstraintForType(val, type); - return ctx.mkOr(typeSystem.isErrorOrUnknown(val), typeConstraint); - } - - private BoolExpr createTypeConstraintForType(Expr val, CelType type) { - if (type instanceof NullableType) { - NullableType nullableType = (NullableType) type; - return ctx.mkOr( - typeSystem.isNull(val), createTypeConstraintForType(val, nullableType.targetType())); - } - if (type instanceof OptionalType) { - BoolExpr isOpt = typeSystem.isOptional(val); - CelType paramType = type.parameters().get(0); - if (paramType.kind().isDyn() || paramType.kind().isTypeParam()) { - return isOpt; - } - Expr optRef = typeSystem.getOptionalRef(val); - BoolExpr hasValue = typeSystem.optHasValue(optRef); - Expr optVal = typeSystem.getOptionalValue(optRef); - BoolExpr optValNotError = ctx.mkNot(typeSystem.isError(optVal)); - BoolExpr valConstraint = createTypeConstraintForType(optVal, paramType); - return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, ctx.mkAnd(optValNotError, valConstraint))); - } - if (type.equals(SimpleType.BOOL)) { - return typeSystem.isBool(val); - } - if (type.equals(SimpleType.INT)) { - IntExpr unwrapped = typeSystem.getInt(val); - return ctx.mkAnd(typeSystem.isInt(val), ctx.mkNot(typeSystem.checkIntOverflow(unwrapped))); - } - if (type.equals(SimpleType.UINT)) { - IntExpr unwrapped = typeSystem.getUint(val); - return ctx.mkAnd(typeSystem.isUint(val), ctx.mkNot(typeSystem.checkUintOverflow(unwrapped))); - } - if (type.equals(SimpleType.DOUBLE)) { - return typeSystem.isDouble(val); - } - if (type.equals(SimpleType.STRING)) { - return typeSystem.isString(val); - } - if (type.equals(SimpleType.BYTES)) { - return typeSystem.isBytes(val); - } - if (type.equals(SimpleType.TIMESTAMP)) { - IntExpr nanos = typeSystem.getTimestamp(val); - return ctx.mkAnd( - typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(nanos))); - } - if (type.equals(SimpleType.DURATION)) { - IntExpr nanos = typeSystem.getDuration(val); - return ctx.mkAnd( - typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(nanos))); - } - - if (type instanceof ListType) { - // Constrain list elements using bounded unrolling up to comprehensionUnrollLimit rather - // than Z3 forall quantifiers to prevent MBQI quantifier instantiation loops. - // Assert: isList(val) ∧ for all unrolled 0 <= i < length: ¬isError(seq[i]) ∧ - // typeConstraint(seq[i]). - BoolExpr isList = typeSystem.isList(val); - CelType elemType = ((ListType) type).elemType(); - - Expr listRef = typeSystem.getListRef(val); - SeqExpr seq = typeSystem.getSeq(listRef); - Expr length = ctx.mkLength(seq); - - List boundsAndTypes = new ArrayList<>(); - boundsAndTypes.add(isList); - // Elements beyond the limit are unconstrained, which only matters if elemType is known. - if (CelZ3OperatorTranslator.isStaticallyKnown(elemType)) { - boundsAndTypes.add( - ctx.mkImplies( - ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)), - typeSystem.hasTruncatedTypeConstraint(val))); - } - for (int i = 0; i < comprehensionUnrollLimit; i++) { - IntExpr idx = ctx.mkInt(i); - Expr elem = ctx.mkNth(seq, idx); - BoolExpr validIndex = ctx.mkLt(idx, length); - // Assert ¬isError(elem) as a domain invariant so Z3 never synthesizes an Error element in - // list(dyn). For concrete types, this is already implied by createTypeConstraintForType. - boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkNot(typeSystem.isError(elem)))); - BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType); - boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint)); - } - - return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); - } - if (type instanceof MapType) { - // Do NOT emit a for-all quantifier over map keys or values here. - // Doing so forces MBQI into an infinite loop. Instead, constrain keys and values using - // bounded unrolling over the key sequence up to comprehensionUnrollLimit. - // Assert: isMap(val) ∧ for all unrolled 0 <= i < length: isPrimitiveKey(key) ∧ ¬isError(key) - // ∧ (presence(key) ⇒ ¬isError(val) ∧ typeConstraint(val)) - BoolExpr isMap = typeSystem.isMap(val); - MapType mapType = (MapType) type; - CelType keyType = mapType.keyType(); - CelType valType = mapType.valueType(); - - Expr mapRef = typeSystem.getMapRef(val); - SeqExpr seq = typeSystem.getMapKeys(mapRef); - Expr length = ctx.mkLength(seq); - ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef); - ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef); - - List boundsAndTypes = new ArrayList<>(); - boundsAndTypes.add(isMap); - boundsAndTypes.add(getBoundedMapBijection(mapPresence, seq, (ArithExpr) length)); - // Entries beyond the limit are unconstrained, which matters if keyType or valType is known. - if (CelZ3OperatorTranslator.isStaticallyKnown(keyType) - || CelZ3OperatorTranslator.isStaticallyKnown(valType)) { - boundsAndTypes.add( - ctx.mkImplies( - ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)), - typeSystem.hasTruncatedTypeConstraint(val))); - } - - for (int i = 0; i < comprehensionUnrollLimit; i++) { - IntExpr idx = ctx.mkInt(i); - Expr key = ctx.mkNth(seq, idx); - BoolExpr validIndex = ctx.mkLt(idx, length); - - BoolExpr isKeyPrim = typeSystem.isPrimitiveKey(key); - BoolExpr keyNotError = ctx.mkNot(typeSystem.isError(key)); - // Assert isKeyPrim ∧ ¬isError(key) so Z3 never synthesizes a non-primitive or Error key in - // map(dyn, ...). For concrete map types, this is already implied by keyType constraints. - boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkAnd(isKeyPrim, keyNotError))); - boundsAndTypes.add(ctx.mkImplies(validIndex, createTypeConstraintForType(key, keyType))); - - BoolExpr presence = (BoolExpr) ctx.mkSelect(mapPresence, key); - BoolExpr validEntry = ctx.mkAnd(validIndex, presence); - - Expr mapVal = ctx.mkSelect(mapValues, key); - BoolExpr valNotError = ctx.mkNot(typeSystem.isErrorOrUnknown(mapVal)); - boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError)); - boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType))); - } - - return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); - } - if (type.kind() == CelKind.STRUCT) { - return ctx.mkAnd( - typeSystem.isMessage(val), - ctx.mkEq( - typeSystem.getMsgTypeName(typeSystem.getMessageRef(val)), ctx.mkString(type.name()))); - } - // Fallback: no type constraint - return ctx.mkTrue(); - } - - private static final class IterationElement { - private final Expr keyOrIndex; - private final Expr value; - - private IterationElement(Expr keyOrIndex, Expr value) { - this.keyOrIndex = keyOrIndex; - this.value = value; - } - } - private Optional toCacheKey(CelExpr expr) { switch (expr.exprKind().getKind()) { case CONSTANT: @@ -1661,18 +998,6 @@ private Optional toCacheKey(CelExpr expr) { } } - private Expr mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast) { - CelAstAlphaHasher.AlphaSignature sig = CelAstAlphaHasher.computeSignature(expr); - - ImmutableList.Builder> smtArgs = ImmutableList.builder(); - for (CelExpr freeVar : sig.freeVariables()) { - smtArgs.add(translateExpr(freeVar, ast).z3Expr()); - } - - return typeSystem.mkParameterizedUnknown( - "!trunc_" + Long.toHexString(sig.staticHash()), smtArgs.build()); - } - CelAstToZ3Translator( Context ctx, int comprehensionUnrollLimit, @@ -1681,24 +1006,14 @@ private Expr mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast) CelTypeProvider typeProvider, boolean parameterizeUnknowns) { this.ctx = ctx; - this.comprehensionUnrollLimit = comprehensionUnrollLimit; this.typeSystem = new CelZ3TypeSystem(ctx, parameterizeUnknowns); - this.typeConstraints = new LinkedHashSet<>(); - this.inputVariableTypes = new HashMap<>(); - this.operatorTranslator = - new CelZ3OperatorTranslator( - ctx, - typeSystem, - this.typeConstraints::add, - this::createTypeConstraintForType, - val -> inputVariableTypes.getOrDefault(val, SimpleType.DYN), - functionRegistry, - comprehensionUnrollLimit); - this.symbolTable = new HashMap<>(); + this.context = new CelZ3TranslationContext(ctx, typeSystem, comprehensionUnrollLimit); + this.typeConstraintGenerator = context.typeConstraintGenerator(); + this.operatorTranslator = new CelZ3OperatorTranslator(context, functionRegistry); + this.comprehensionTranslator = new CelZ3ComprehensionTranslator(context, this::translateExpr); this.unknownIdentifiers = unknownIdentifiers; this.emptyMessageCache = new HashMap<>(); this.listLiteralCache = new HashMap<>(); this.typeProvider = typeProvider; - this.truncationConditions = new ArrayList<>(); } } 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/CelZ3ComprehensionTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java new file mode 100644 index 000000000..df34f00aa --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3ComprehensionTranslator.java @@ -0,0 +1,535 @@ +// 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.ImmutableList; +import com.microsoft.z3.ArithExpr; +import com.microsoft.z3.ArrayExpr; +import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.Context; +import com.microsoft.z3.Expr; +import com.microsoft.z3.IntExpr; +import com.microsoft.z3.SeqExpr; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.Operator; +import dev.cel.common.ast.CelConstant; +import dev.cel.common.ast.CelExpr; +import dev.cel.common.ast.CelExpr.CelComprehension; +import dev.cel.common.ast.CelExpr.ExprKind; +import dev.cel.common.types.CelType; +import dev.cel.common.types.ListType; +import dev.cel.common.types.MapType; +import dev.cel.common.types.SimpleType; +import java.util.ArrayList; +import java.util.List; +import java.util.function.BiFunction; +import java.util.function.Supplier; + +/** Translates CEL comprehensions to Z3, unrolling them up to the comprehension unroll limit. */ +@SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types. +final class CelZ3ComprehensionTranslator { + + private final CelZ3TranslationContext context; + private final Context ctx; + private final CelZ3TypeSystem typeSystem; + private final int comprehensionUnrollLimit; + private final BiFunction exprTranslator; + + TranslatedValue translateComprehension(CelExpr celExpr, CelAbstractSyntaxTree ast) { + CelComprehension comp = celExpr.comprehension(); + CelExpr iterRangeExpr = comp.iterRange(); + if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.IDENT) { + iterRangeExpr = + context + .lookupSymbol(iterRangeExpr.ident().name()) + .flatMap(TranslatedValue::celExpr) + .orElse(iterRangeExpr); + } + List iterationElements = new ArrayList<>(); + List taints = new ArrayList<>(); + List> allRangeElems = new ArrayList<>(); + + // For statically known list/map literals, unroll them exactly. + if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.LIST + && iterRangeExpr.list().optionalIndices().isEmpty()) { + ImmutableList elements = iterRangeExpr.list().elements(); + for (int i = 0; i < elements.size(); i++) { + TranslatedValue valueTv = translateExpr(elements.get(i), ast); + Expr value = valueTv.z3Expr(); + taints.add(valueTv.isApproximate()); + iterationElements.add(new IterationElement(typeSystem.mkInt(i), value)); + allRangeElems.add(value); + } + } else if (iterRangeExpr.exprKind().getKind() == ExprKind.Kind.MAP + && iterRangeExpr.map().entries().stream().noneMatch(CelExpr.CelMap.Entry::optionalEntry)) { + for (CelExpr.CelMap.Entry entry : iterRangeExpr.map().entries()) { + TranslatedValue keyTv = translateExpr(entry.key(), ast); + Expr key = keyTv.z3Expr(); + taints.add(keyTv.isApproximate()); + TranslatedValue valueTv = translateExpr(entry.value(), ast); + Expr value = valueTv.z3Expr(); + taints.add(valueTv.isApproximate()); + iterationElements.add(new IterationElement(key, value)); + allRangeElems.add(key); + allRangeElems.add(value); + } + } else { + return translateDynamicComprehension(celExpr, ast); + } + + TranslatedValue accuTv = translateExpr(comp.accuInit(), ast); + Expr accu = accuTv.z3Expr(); + taints.add(accuTv.isApproximate()); + boolean isMap = iterRangeExpr.exprKind().getKind() == ExprKind.Kind.MAP; + boolean isTwoVar = !comp.iterVar2().isEmpty(); + + for (IterationElement iterElem : iterationElements) { + Expr currentAccu = accu; + accu = + withIterationScope( + comp, + iterElem.keyOrIndex, + iterElem.value, + currentAccu, + isMap, + isTwoVar, + () -> { + TranslatedValue condTv = translateExpr(comp.loopCondition(), ast); + TranslatedValue stepTv = translateExpr(comp.loopStep(), ast); + taints.add(stepTv.isApproximate()); + return ctx.mkITE( + (BoolExpr) typeSystem.unwrapBool(condTv.z3Expr()), + stepTv.z3Expr(), + currentAccu); + }); + } + + TranslatedValue resultTv = + context.withScope( + comp.accuVar(), + TranslatedValue.create(accu, typeSystem, CelZ3Exprs.mkOrFlattened(ctx, taints)), + () -> translateExpr(comp.result(), ast)); + Expr result = resultTv.z3Expr(); + return TranslatedValue.create( + typeSystem.propagateErrorAndUnknown( + "comprehension", + result, + allRangeElems, + ImmutableList.>builder().add(result).addAll(allRangeElems).build()), + celExpr, + typeSystem, + resultTv.isApproximate()); + } + + private static final class BoundedIteration { + private final BoolExpr inBounds; + private final TranslatedValue stepResult; + + private BoundedIteration(BoolExpr inBounds, TranslatedValue stepResult) { + this.inBounds = inBounds; + this.stepResult = stepResult; + } + } + + private TranslatedValue translateDynamicComprehension( + CelExpr celExpr, CelAbstractSyntaxTree ast) { + CelComprehension comp = celExpr.comprehension(); + TranslatedValue iterRangeTv = translateExpr(comp.iterRange(), ast); + Expr iterRange = iterRangeTv.z3Expr(); + CelType rangeType = ast.getType(comp.iterRange().id()).orElse(SimpleType.DYN); + + boolean isList = rangeType instanceof ListType; + boolean isMap = rangeType instanceof MapType; + if (!isList && !isMap) { + BoolExpr isRuntimeListOrMap = + ctx.mkOr(typeSystem.isList(iterRange), typeSystem.isMap(iterRange)); + Expr result = + ctx.mkITE(isRuntimeListOrMap, mkParameterizedUnknown(celExpr, ast), typeSystem.mkError()); + return TranslatedValue.create(result, celExpr, typeSystem, isRuntimeListOrMap); + } + + SeqExpr seq = + isMap + ? typeSystem.getMapKeys(typeSystem.getMapRef(iterRange)) + : typeSystem.getSeq(typeSystem.getListRef(iterRange)); + + ArithExpr lengthExpr = ctx.mkLength(seq); + ArrayExpr mapPresence = + isMap ? (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(iterRange)) : null; + + BoolExpr isValidRange = isMap ? typeSystem.isMap(iterRange) : typeSystem.isList(iterRange); + BoolExpr isTruncated = + ctx.mkAnd(isValidRange, ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit))); + context.addTruncationCondition(isTruncated); + + if (isAllMacro(comp) || isExistsMacro(comp)) { + return unrollAllAndExists( + celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv); + } else { + return unrollMapAndFilter( + celExpr, ast, seq, lengthExpr, mapPresence, isTruncated, iterRangeTv); + } + } + + private T withIterationScope( + CelComprehension comp, + Expr keyOrIndex, + Expr value, + Expr currentAccu, + boolean isMap, + boolean isTwoVar, + Supplier action) { + Supplier bindAccu = + () -> + context.withScope( + comp.accuVar(), + TranslatedValue.create(currentAccu, typeSystem, ctx.mkFalse()), + action); + + if (isTwoVar) { + return context.withScope( + comp.iterVar(), + TranslatedValue.create(keyOrIndex, typeSystem, ctx.mkFalse()), + () -> + context.withScope( + comp.iterVar2(), + TranslatedValue.create(value, typeSystem, ctx.mkFalse()), + bindAccu)); + } else { + Expr iterVal = isMap ? keyOrIndex : value; + return context.withScope( + comp.iterVar(), TranslatedValue.create(iterVal, typeSystem, ctx.mkFalse()), bindAccu); + } + } + + private IterationElement getIterationElement( + Expr xVal, IntExpr idx, Expr iterRange, boolean isMap, boolean isTwoVar) { + Expr keyOrIndex; + Expr value; + + if (isMap) { + keyOrIndex = xVal; + if (isTwoVar) { + Expr mapRef = typeSystem.getMapRef(iterRange); + ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef); + value = ctx.mkSelect(mapValues, keyOrIndex); + } else { + value = null; + } + } else { + if (isTwoVar) { + keyOrIndex = typeSystem.wrapInt(idx); + value = xVal; + } else { + keyOrIndex = null; + value = xVal; + } + } + return new IterationElement(keyOrIndex, value); + } + + private TranslatedValue unrollAllAndExists( + CelExpr celExpr, + CelAbstractSyntaxTree ast, + SeqExpr seq, + ArithExpr lengthExpr, + ArrayExpr mapPresence, + BoolExpr isTruncated, + TranslatedValue iterRangeTv) { + CelComprehension comp = celExpr.comprehension(); + List iterations = new ArrayList<>(); + TranslatedValue accuInitTv = translateExpr(comp.accuInit(), ast); + Expr accuInitExpr = accuInitTv.z3Expr(); + + boolean isMap = mapPresence != null; + boolean isTwoVar = !comp.iterVar2().isEmpty(); + + for (int i = 0; i < comprehensionUnrollLimit; i++) { + IntExpr idx = ctx.mkInt(i); + BoolExpr inBounds = ctx.mkLt(idx, lengthExpr); + Expr xVal = ctx.mkNth(seq, idx); + + constrainIterationElement(idx, lengthExpr, xVal, inBounds, mapPresence); + + IterationElement iterElem = + getIterationElement(xVal, idx, iterRangeTv.z3Expr(), isMap, isTwoVar); + + TranslatedValue stepTv = + withIterationScope( + comp, + iterElem.keyOrIndex, + iterElem.value, + accuInitExpr, + isMap, + isTwoVar, + () -> translateExpr(comp.loopStep(), ast)); + iterations.add(new BoundedIteration(inBounds, stepTv)); + } + + return reduceAllOrExists(iterations, isTruncated, iterRangeTv, isAllMacro(comp), celExpr, ast); + } + + private TranslatedValue unrollMapAndFilter( + CelExpr celExpr, + CelAbstractSyntaxTree ast, + SeqExpr seq, + ArithExpr lengthExpr, + ArrayExpr mapPresence, + BoolExpr isTruncated, + TranslatedValue iterRangeTv) { + CelComprehension comp = celExpr.comprehension(); + // For macros like map and filter, we must sequentially thread the accumulator through the loop + TranslatedValue chainedAccuTv = translateExpr(comp.accuInit(), ast); + Expr chainedAccu = chainedAccuTv.z3Expr(); + + boolean isMap = mapPresence != null; + boolean isTwoVar = !comp.iterVar2().isEmpty(); + + List taints = new ArrayList<>(); + taints.add(chainedAccuTv.isApproximate()); + taints.add(iterRangeTv.isApproximate()); + + for (int i = 0; i < comprehensionUnrollLimit; i++) { + IntExpr idx = ctx.mkInt(i); + BoolExpr inBounds = ctx.mkLt(idx, lengthExpr); + Expr xVal = ctx.mkNth(seq, idx); + + constrainIterationElement(idx, lengthExpr, xVal, inBounds, mapPresence); + + Expr currentAccu = chainedAccu; + IterationElement iterElem = + getIterationElement(xVal, idx, iterRangeTv.z3Expr(), isMap, isTwoVar); + + TranslatedValue stepTv = + withIterationScope( + comp, + iterElem.keyOrIndex, + iterElem.value, + currentAccu, + isMap, + isTwoVar, + () -> translateExpr(comp.loopStep(), ast)); + + taints.add(ctx.mkAnd(inBounds, stepTv.isApproximate())); + chainedAccu = ctx.mkITE(inBounds, stepTv.z3Expr(), currentAccu); + } + + TranslatedValue resultTv = + context.withScope( + comp.accuVar(), + TranslatedValue.create(chainedAccu, typeSystem, CelZ3Exprs.mkOrFlattened(ctx, taints)), + () -> translateExpr(comp.result(), ast)); + + Expr iterRangeExpr = iterRangeTv.z3Expr(); + BoolExpr rangeIsError = typeSystem.isError(iterRangeExpr); + BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeExpr); + + // TODO: Model the loop condition for custom macros; until then, abstract the + // result of any non-true condition, since the unrolled value ignores early exits. + BoolExpr isConditionUnmodeled = ctx.mkBool(!isLiteralTrue(comp.loopCondition())); + BoolExpr isAbstracted = + CelZ3Exprs.mkOrFlattened(ctx, rangeIsUnknown, isTruncated, isConditionUnmodeled); + // An error is not final when truncated: an unknown from a later iteration overrides it. + Expr finalResult = + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) + .addCase(rangeIsError, typeSystem.mkError()) + .addCase(isAbstracted, mkParameterizedUnknown(celExpr, ast)) + .build(resultTv.z3Expr()); + + BoolExpr finalTaint = + (BoolExpr) + ctx.mkITE( + ctx.mkOr(rangeIsError, rangeIsUnknown), + iterRangeTv.isApproximate(), + CelZ3Exprs.mkOrFlattened( + ctx, resultTv.isApproximate(), isTruncated, isConditionUnmodeled)); + + return TranslatedValue.create(finalResult, celExpr, typeSystem, finalTaint); + } + + private void constrainIterationElement( + IntExpr idx, ArithExpr lengthExpr, Expr xVal, BoolExpr inBounds, ArrayExpr mapPresence) { + // Constrain out-of-bounds elements to prevent MBQI from infinitely instantiating list/map + // axioms + BoolExpr outOfBounds = ctx.mkGe(idx, lengthExpr); + context.addConstraint(ctx.mkImplies(outOfBounds, ctx.mkEq(xVal, typeSystem.mkUnknown()))); + + // If we are iterating over a map, we can optionally bind the sequence elements + // to the map presence array to ensure the solver knows they correspond. + if (mapPresence != null) { + Expr selectExpr = ctx.mkSelect(mapPresence, xVal); + context.addConstraint(ctx.mkImplies(inBounds, (BoolExpr) selectExpr)); + } + } + + private TranslatedValue reduceAllOrExists( + List iterations, + BoolExpr isTruncated, + TranslatedValue iterRangeTv, + boolean isAll, + CelExpr compExpr, + CelAbstractSyntaxTree ast) { + List hasMatchList = new ArrayList<>(); + List hasErrorList = new ArrayList<>(); + List hasUnknownList = new ArrayList<>(); + + List hasSafeMatchList = new ArrayList<>(); + List hasSafeErrorList = new ArrayList<>(); + List hasSafeUnknownList = new ArrayList<>(); + List activeTaints = new ArrayList<>(); + + for (BoundedIteration iter : iterations) { + TranslatedValue stepTv = iter.stepResult; + Expr step = stepTv.z3Expr(); + BoolExpr isBool = typeSystem.isBool(step); + BoolExpr unwrapStep = (BoolExpr) typeSystem.unwrapBool(step); + + // 'all' short-circuits on False, 'exists' short-circuits on True + BoolExpr matchCond = isAll ? ctx.mkNot(unwrapStep) : unwrapStep; + BoolExpr isMatch = ctx.mkAnd(isBool, matchCond); + + BoolExpr isU = typeSystem.isUnknown(step); + BoolExpr isE = + ctx.mkOr(typeSystem.isError(step), ctx.mkAnd(ctx.mkNot(isBool), ctx.mkNot(isU))); + + BoolExpr isActive = iter.inBounds; + + hasMatchList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isMatch)); + hasErrorList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isE)); + hasUnknownList.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, isU)); + + hasSafeMatchList.add( + CelZ3Exprs.mkAndFlattened( + ctx, isActive, isMatch, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate()))); + hasSafeErrorList.add( + CelZ3Exprs.mkAndFlattened( + ctx, isActive, isE, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate()))); + hasSafeUnknownList.add( + CelZ3Exprs.mkAndFlattened( + ctx, isActive, isU, CelZ3Exprs.mkNotFlattened(ctx, stepTv.isApproximate()))); + activeTaints.add(CelZ3Exprs.mkAndFlattened(ctx, isActive, stepTv.isApproximate())); + } + + 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 = 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 = + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) + .addCase(rangeIsError, typeSystem.mkError()) + .addCase(rangeIsUnknown, comprehensionUnknown) + .addCase(hasMatch, typeSystem.mkBool(!isAll)) + .addCase(ctx.mkOr(hasUnknown, isTruncated), comprehensionUnknown) + .addCase(hasError, typeSystem.mkError()) + .build(typeSystem.mkBool(isAll)); + + BoolExpr baseTaint = CelZ3Exprs.mkOrFlattened(ctx, anyActiveTaint, iterRangeTv.isApproximate()); + + // Taint identically shadows the value flow's short-circuit control structure + BoolExpr resultTaint = + (BoolExpr) + CelZ3Exprs.SwitchBuilder.newBuilder(ctx) + .addCase(ctx.mkOr(rangeIsError, rangeIsUnknown), iterRangeTv.isApproximate()) + .addCase(hasMatch, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeMatch))) + .addCase( + ctx.mkOr(hasUnknown, isTruncated), + ctx.mkOr(iterRangeTv.isApproximate(), isTruncated, ctx.mkNot(hasSafeUnknown))) + .addCase(hasError, ctx.mkOr(iterRangeTv.isApproximate(), ctx.mkNot(hasSafeError))) + .build(baseTaint); + + return TranslatedValue.create(result, compExpr, typeSystem, resultTaint); + } + + private static boolean isAllMacro(CelComprehension comp) { + return isBooleanAccuInit(comp, true) + && isNotStrictlyFalseLoopCondition(comp, /* expectNot= */ false); + } + + private static boolean isExistsMacro(CelComprehension comp) { + return isBooleanAccuInit(comp, false) + && isNotStrictlyFalseLoopCondition(comp, /* expectNot= */ true); + } + + private static boolean isBooleanAccuInit(CelComprehension comp, boolean expectedValue) { + return comp.accuInit().constantOrDefault().getKind() == CelConstant.Kind.BOOLEAN_VALUE + && comp.accuInit().constant().booleanValue() == expectedValue; + } + + private static boolean isLiteralTrue(CelExpr expr) { + CelConstant constant = expr.constantOrDefault(); + return constant.getKind() == CelConstant.Kind.BOOLEAN_VALUE && constant.booleanValue(); + } + + private static boolean isNotStrictlyFalseLoopCondition(CelComprehension comp, boolean expectNot) { + CelExpr.CelCall call = comp.loopCondition().callOrDefault(); + if (!call.function().equals(Operator.NOT_STRICTLY_FALSE.getFunction()) + && !call.function().equals(Operator.OLD_NOT_STRICTLY_FALSE.getFunction())) { + return false; + } + CelExpr arg = call.args().get(0); + if (expectNot) { + CelExpr.CelCall notCall = arg.callOrDefault(); + if (!notCall.function().equals(Operator.LOGICAL_NOT.getFunction())) { + return false; + } + arg = notCall.args().get(0); + } + return arg.identOrDefault().name().equals(comp.accuVar()); + } + + private static final class IterationElement { + private final Expr keyOrIndex; + private final Expr value; + + private IterationElement(Expr keyOrIndex, Expr value) { + this.keyOrIndex = keyOrIndex; + this.value = value; + } + } + + private Expr mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast) { + CelAstAlphaHasher.AlphaSignature sig = CelAstAlphaHasher.computeSignature(expr); + + ImmutableList.Builder> smtArgs = ImmutableList.builder(); + for (CelExpr freeVar : sig.freeVariables()) { + smtArgs.add(translateExpr(freeVar, ast).z3Expr()); + } + + return typeSystem.mkParameterizedUnknown( + "!trunc_" + Long.toHexString(sig.staticHash()), smtArgs.build()); + } + + private TranslatedValue translateExpr(CelExpr expr, CelAbstractSyntaxTree ast) { + return exprTranslator.apply(expr, ast); + } + + CelZ3ComprehensionTranslator( + CelZ3TranslationContext context, + BiFunction exprTranslator) { + this.context = context; + this.ctx = context.ctx(); + this.typeSystem = context.typeSystem(); + this.comprehensionUnrollLimit = context.comprehensionUnrollLimit(); + this.exprTranslator = exprTranslator; + } +} 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..587f18f19 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -47,18 +47,14 @@ import java.util.Arrays; import java.util.List; import java.util.Optional; -import java.util.function.BiFunction; -import java.util.function.Consumer; -import java.util.function.Function; /** Handles mapping CEL Operators to Z3 SMT logic. */ @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types. final class CelZ3OperatorTranslator { private final Context ctx; private final CelZ3TypeSystem typeSystem; - private final Consumer constraintSink; - private final BiFunction, CelType, BoolExpr> typeConstraintGenerator; - private final Function, CelType> guaranteedTypes; + private final CelZ3TranslationContext context; + private final CelZ3TypeConstraintGenerator typeConstraintGenerator; private final CelZ3FunctionRegistry functionRegistry; private final int comprehensionUnrollLimit; @@ -117,7 +113,7 @@ Optional translateFunctionCall( } Optional evaluatedResultOpt = - translator.translate(ctx, typeSystem, constraintSink, z3Args, argApproximations); + translator.translate(ctx, typeSystem, context::addConstraint, z3Args, argApproximations); if (!evaluatedResultOpt.isPresent()) { continue; @@ -131,7 +127,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 +140,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 +150,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( @@ -197,10 +193,10 @@ private BoolExpr constrainInWitnessTypes( SeqExpr seq = typeSystem.getSeq(typeSystem.getListRef(rhs)); for (Expr cand : candidates) { BoolExpr structContains = ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(cand)); - constraintSink.accept( + context.addConstraint( ctx.mkImplies( ctx.mkAnd(typeSystem.isList(rhs), structContains), - typeConstraintGenerator.apply(cand, elemType))); + typeConstraintGenerator.createTypeConstraintForType(cand, elemType))); } // With a concrete element type, the constraints above cover any match in rhs. return isConcrete(elemType) @@ -210,13 +206,15 @@ private BoolExpr constrainInWitnessTypes( // IN_MAP only probes the presence of lhs itself. ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(rhs)); BoolExpr inMap = (BoolExpr) ctx.mkSelect(mapPresence, lhs); - constraintSink.accept( + context.addConstraint( ctx.mkImplies( ctx.mkAnd(typeSystem.isMap(rhs), inMap), - typeConstraintGenerator.apply(lhs, ((MapType) rhsType).keyType()))); + context + .typeConstraintGenerator() + .createTypeConstraintForType(lhs, ((MapType) rhsType).keyType()))); return isTruncatedMap(rhs); } - return CelZ3TypeSystem.mkOrFlattened( + return CelZ3Exprs.mkOrFlattened( ctx, isTruncatedMap(rhs), mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv)); } @@ -385,7 +383,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 +392,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 +433,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 +496,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 +608,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,15 +670,17 @@ 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) { if (listType instanceof ListType) { - constraintSink.accept( + context.addConstraint( ctx.mkImplies( ctx.mkLt(idx, ctx.mkLength(seq)), - typeConstraintGenerator.apply(elem, ((ListType) listType).elemType()))); + context + .typeConstraintGenerator() + .createTypeConstraintForType(elem, ((ListType) listType).elemType()))); } } @@ -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( @@ -754,12 +754,12 @@ private Expr buildListIndex( ctx.mkLt((ArithExpr) index, ctx.mkLength(seq))); Expr val = ctx.mkNth(seq, (ArithExpr) index); - constrainValidElement(ctx.mkAnd(typeGuard, inBounds), val); + context.constrainValidValue(ctx.mkAnd(typeGuard, inBounds), val); if (isOptional) { Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), val); - constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val)); - constraintSink.accept(typeSystem.optHasValue(resultOptRef)); + context.addConstraint(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val)); + context.addConstraint(typeSystem.optHasValue(resultOptRef)); return ctx.mkITE( inBounds, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone()); } @@ -767,10 +767,6 @@ private Expr buildListIndex( return ctx.mkITE(inBounds, val, typeSystem.mkError()); } - private void constrainValidElement(BoolExpr guard, Expr val) { - constraintSink.accept(ctx.mkImplies(guard, ctx.mkNot(typeSystem.isErrorOrUnknown(val)))); - } - private Optional extractIntNumSafe(Expr expr) { Expr simplified = expr.simplify(); @@ -814,12 +810,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,25 +908,25 @@ 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) .build(valOrig); - constrainValidElement(ctx.mkAnd(typeGuard, finalInMap), finalVal); + context.constrainValidValue(ctx.mkAnd(typeGuard, finalInMap), finalVal); if (isOptional) { Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), finalVal); - constraintSink.accept(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal)); - constraintSink.accept(typeSystem.optHasValue(resultOptRef)); + context.addConstraint(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal)); + context.addConstraint(typeSystem.optHasValue(resultOptRef)); return ctx.mkITE( finalInMap, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone()); } @@ -992,7 +988,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())); } @@ -1030,9 +1026,10 @@ private TranslatedValue buildAndConstrainIndex( CelType finalType = isOptional ? OptionalType.create(expectedElemType) : expectedElemType; BoolExpr isDefined = ctx.mkAnd(shouldEvaluate, ctx.mkNot(typeSystem.isError(actualValue))); - BoolExpr typeConstraint = typeConstraintGenerator.apply(actualValue, finalType); + BoolExpr typeConstraint = + typeConstraintGenerator.createTypeConstraintForType(actualValue, finalType); if (isLhsTypeGuaranteed) { - constraintSink.accept(ctx.mkImplies(isDefined, typeConstraint)); + context.addConstraint(ctx.mkImplies(isDefined, typeConstraint)); return TranslatedValue.create(actualValue, typeSystem, ctx.mkFalse()); } // The type checker may narrow other static types (e.g. `(['a'] + dyn_var)[1]` is typed @@ -1040,8 +1037,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 +1046,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 +1077,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 +1088,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())) @@ -1118,7 +1115,7 @@ private static CelType extractAstTypeOrDefault(TranslatedValue val, CelAbstractS * so constraints derived from those could exclude valid inputs. */ private CelType guaranteedType(TranslatedValue val) { - return guaranteedTypes.apply(val.z3Expr()); + return context.guaranteedType(val.z3Expr()); } /** @@ -1163,27 +1160,19 @@ 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())) .collect(toImmutableList())); } - CelZ3OperatorTranslator( - Context ctx, - CelZ3TypeSystem typeSystem, - Consumer constraintSink, - BiFunction, CelType, BoolExpr> typeConstraintGenerator, - Function, CelType> guaranteedTypes, - CelZ3FunctionRegistry functionRegistry, - int comprehensionUnrollLimit) { - this.ctx = ctx; - this.typeSystem = typeSystem; - this.constraintSink = constraintSink; - this.typeConstraintGenerator = typeConstraintGenerator; - this.guaranteedTypes = guaranteedTypes; + CelZ3OperatorTranslator(CelZ3TranslationContext context, CelZ3FunctionRegistry functionRegistry) { + this.ctx = context.ctx(); + this.typeSystem = context.typeSystem(); + this.context = context; + this.typeConstraintGenerator = context.typeConstraintGenerator(); this.functionRegistry = functionRegistry; - this.comprehensionUnrollLimit = comprehensionUnrollLimit; + this.comprehensionUnrollLimit = context.comprehensionUnrollLimit(); } } diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java new file mode 100644 index 000000000..b42c9f7de --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java @@ -0,0 +1,130 @@ +// 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.microsoft.z3.BoolExpr; +import com.microsoft.z3.Context; +import com.microsoft.z3.Expr; +import dev.cel.common.types.CelType; +import dev.cel.common.types.SimpleType; +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.LinkedHashSet; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.Set; +import java.util.function.Function; +import java.util.function.Supplier; + +/** State shared by the translators of a single verification query. */ +final class CelZ3TranslationContext { + + private final Context ctx; + private final CelZ3TypeSystem typeSystem; + private final CelZ3TypeConstraintGenerator typeConstraintGenerator; + private final int comprehensionUnrollLimit; + private final Set constraints; + private final Map, CelType> inputVariableTypes; + private final List truncationConditions; + private final Map symbolTable; + + Context ctx() { + return ctx; + } + + CelZ3TypeSystem typeSystem() { + return typeSystem; + } + + CelZ3TypeConstraintGenerator typeConstraintGenerator() { + return typeConstraintGenerator; + } + + int comprehensionUnrollLimit() { + return comprehensionUnrollLimit; + } + + /** Returns the constraints asserted so far, in insertion order. */ + Set constraints() { + return Collections.unmodifiableSet(constraints); + } + + void addConstraint(BoolExpr constraint) { + constraints.add(constraint); + } + + /** Constrains {@code value} to be neither an error nor unknown whenever {@code guard} holds. */ + void constrainValidValue(BoolExpr guard, Expr value) { + addConstraint(ctx.mkImplies(guard, ctx.mkNot(typeSystem.isErrorOrUnknown(value)))); + } + + void addInputVariable(Expr variable, CelType declaredType) { + inputVariableTypes.put(variable, declaredType); + } + + /** Returns the declared type of an input variable, or dyn for any other value. */ + CelType guaranteedType(Expr value) { + return inputVariableTypes.getOrDefault(value, SimpleType.DYN); + } + + void addTruncationCondition(BoolExpr condition) { + truncationConditions.add(condition); + } + + BoolExpr hasTruncation() { + return CelZ3Exprs.mkOrFlattened(ctx, truncationConditions); + } + + void bindSymbol(String name, TranslatedValue value) { + symbolTable.put(name, value); + } + + Optional lookupSymbol(String name) { + return Optional.ofNullable(symbolTable.get(name)); + } + + TranslatedValue computeSymbolIfAbsent( + String name, Function mappingFunction) { + return symbolTable.computeIfAbsent(name, mappingFunction); + } + + /** Binds {@code varName} to {@code value} while running {@code action}, then restores it. */ + T withScope(String varName, TranslatedValue value, Supplier action) { + TranslatedValue prev = symbolTable.put(varName, value); + try { + return action.get(); + } finally { + if (prev != null) { + symbolTable.put(varName, prev); + } else { + symbolTable.remove(varName); + } + } + } + + CelZ3TranslationContext(Context ctx, CelZ3TypeSystem typeSystem, int comprehensionUnrollLimit) { + this.ctx = ctx; + this.typeSystem = typeSystem; + this.typeConstraintGenerator = + new CelZ3TypeConstraintGenerator(ctx, typeSystem, comprehensionUnrollLimit); + this.comprehensionUnrollLimit = comprehensionUnrollLimit; + this.constraints = new LinkedHashSet<>(); + this.inputVariableTypes = new HashMap<>(); + this.truncationConditions = new ArrayList<>(); + this.symbolTable = new HashMap<>(); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeConstraintGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeConstraintGenerator.java new file mode 100644 index 000000000..1f6e86475 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeConstraintGenerator.java @@ -0,0 +1,231 @@ +// 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.microsoft.z3.ArithExpr; +import com.microsoft.z3.ArrayExpr; +import com.microsoft.z3.BoolExpr; +import com.microsoft.z3.Context; +import com.microsoft.z3.Expr; +import com.microsoft.z3.IntExpr; +import com.microsoft.z3.SeqExpr; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.types.CelKind; +import dev.cel.common.types.CelType; +import dev.cel.common.types.ListType; +import dev.cel.common.types.MapType; +import dev.cel.common.types.NullableType; +import dev.cel.common.types.OptionalType; +import dev.cel.common.types.SimpleType; +import java.util.ArrayList; +import java.util.List; + +/** Generates Z3 constraints restricting a value to the values of a CEL type. */ +@SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types. +final class CelZ3TypeConstraintGenerator { + + private final Context ctx; + private final CelZ3TypeSystem typeSystem; + private final int comprehensionUnrollLimit; + + BoolExpr createTypeConstraint(Expr val, long exprId, CelAbstractSyntaxTree ast) { + CelType type = + ast.getType(exprId) + .orElseThrow( + () -> new IllegalArgumentException("Type not found for expr ID: " + exprId)); + BoolExpr typeConstraint = createTypeConstraintForType(val, type); + return ctx.mkOr(typeSystem.isErrorOrUnknown(val), typeConstraint); + } + + BoolExpr createTypeConstraintForType(Expr val, CelType type) { + if (type instanceof NullableType) { + NullableType nullableType = (NullableType) type; + return ctx.mkOr( + typeSystem.isNull(val), createTypeConstraintForType(val, nullableType.targetType())); + } + if (type instanceof OptionalType) { + BoolExpr isOpt = typeSystem.isOptional(val); + CelType paramType = type.parameters().get(0); + if (!CelZ3OperatorTranslator.isStaticallyKnown(paramType)) { + return isOpt; + } + Expr optRef = typeSystem.getOptionalRef(val); + BoolExpr hasValue = typeSystem.optHasValue(optRef); + Expr optVal = typeSystem.getOptionalValue(optRef); + BoolExpr optValNotError = ctx.mkNot(typeSystem.isError(optVal)); + BoolExpr valConstraint = createTypeConstraintForType(optVal, paramType); + return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, ctx.mkAnd(optValNotError, valConstraint))); + } + if (type.equals(SimpleType.BOOL)) { + return typeSystem.isBool(val); + } + if (type.equals(SimpleType.INT)) { + IntExpr unwrapped = typeSystem.getInt(val); + return ctx.mkAnd(typeSystem.isInt(val), ctx.mkNot(typeSystem.checkIntOverflow(unwrapped))); + } + if (type.equals(SimpleType.UINT)) { + IntExpr unwrapped = typeSystem.getUint(val); + return ctx.mkAnd(typeSystem.isUint(val), ctx.mkNot(typeSystem.checkUintOverflow(unwrapped))); + } + if (type.equals(SimpleType.DOUBLE)) { + return typeSystem.isDouble(val); + } + if (type.equals(SimpleType.STRING)) { + return typeSystem.isString(val); + } + if (type.equals(SimpleType.BYTES)) { + return typeSystem.isBytes(val); + } + if (type.equals(SimpleType.TIMESTAMP)) { + IntExpr nanos = typeSystem.getTimestamp(val); + return ctx.mkAnd( + typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(nanos))); + } + if (type.equals(SimpleType.DURATION)) { + IntExpr nanos = typeSystem.getDuration(val); + return ctx.mkAnd( + typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(nanos))); + } + + if (type instanceof ListType) { + // Constrain list elements using bounded unrolling up to comprehensionUnrollLimit rather + // than Z3 forall quantifiers to prevent MBQI quantifier instantiation loops. + // Assert: isList(val) ∧ for all unrolled 0 <= i < length: ¬isError(seq[i]) ∧ + // typeConstraint(seq[i]). + BoolExpr isList = typeSystem.isList(val); + CelType elemType = ((ListType) type).elemType(); + + Expr listRef = typeSystem.getListRef(val); + SeqExpr seq = typeSystem.getSeq(listRef); + Expr length = ctx.mkLength(seq); + + List boundsAndTypes = new ArrayList<>(); + boundsAndTypes.add(isList); + // Elements beyond the limit are unconstrained, which only matters if elemType is known. + if (CelZ3OperatorTranslator.isStaticallyKnown(elemType)) { + boundsAndTypes.add( + ctx.mkImplies( + ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)), + typeSystem.hasTruncatedTypeConstraint(val))); + } + for (int i = 0; i < comprehensionUnrollLimit; i++) { + IntExpr idx = ctx.mkInt(i); + Expr elem = ctx.mkNth(seq, idx); + BoolExpr validIndex = ctx.mkLt(idx, length); + // Assert ¬isError(elem) as a domain invariant so Z3 never synthesizes an Error element in + // list(dyn). For concrete types, this is already implied by createTypeConstraintForType. + boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkNot(typeSystem.isError(elem)))); + BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType); + boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint)); + } + + return CelZ3Exprs.mkAndFlattened(ctx, boundsAndTypes); + } + if (type instanceof MapType) { + // Do NOT emit a for-all quantifier over map keys or values here. + // Doing so forces MBQI into an infinite loop. Instead, constrain keys and values using + // bounded unrolling over the key sequence up to comprehensionUnrollLimit. + // Assert: isMap(val) ∧ for all unrolled 0 <= i < length: isPrimitiveKey(key) ∧ ¬isError(key) + // ∧ (presence(key) ⇒ ¬isError(val) ∧ typeConstraint(val)) + BoolExpr isMap = typeSystem.isMap(val); + MapType mapType = (MapType) type; + CelType keyType = mapType.keyType(); + CelType valType = mapType.valueType(); + + Expr mapRef = typeSystem.getMapRef(val); + SeqExpr seq = typeSystem.getMapKeys(mapRef); + Expr length = ctx.mkLength(seq); + ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef); + ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef); + + List boundsAndTypes = new ArrayList<>(); + boundsAndTypes.add(isMap); + boundsAndTypes.add(getBoundedMapBijection(mapPresence, seq, (ArithExpr) length)); + // Entries beyond the limit are unconstrained, which matters if keyType or valType is known. + if (CelZ3OperatorTranslator.isStaticallyKnown(keyType) + || CelZ3OperatorTranslator.isStaticallyKnown(valType)) { + boundsAndTypes.add( + ctx.mkImplies( + ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)), + typeSystem.hasTruncatedTypeConstraint(val))); + } + + for (int i = 0; i < comprehensionUnrollLimit; i++) { + IntExpr idx = ctx.mkInt(i); + Expr key = ctx.mkNth(seq, idx); + BoolExpr validIndex = ctx.mkLt(idx, length); + + BoolExpr isKeyPrim = typeSystem.isPrimitiveKey(key); + BoolExpr keyNotError = ctx.mkNot(typeSystem.isError(key)); + // Assert isKeyPrim ∧ ¬isError(key) so Z3 never synthesizes a non-primitive or Error key in + // map(dyn, ...). For concrete map types, this is already implied by keyType constraints. + boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkAnd(isKeyPrim, keyNotError))); + boundsAndTypes.add(ctx.mkImplies(validIndex, createTypeConstraintForType(key, keyType))); + + BoolExpr presence = (BoolExpr) ctx.mkSelect(mapPresence, key); + BoolExpr validEntry = ctx.mkAnd(validIndex, presence); + + Expr mapVal = ctx.mkSelect(mapValues, key); + BoolExpr valNotError = ctx.mkNot(typeSystem.isErrorOrUnknown(mapVal)); + boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError)); + boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType))); + } + + return CelZ3Exprs.mkAndFlattened(ctx, boundsAndTypes); + } + if (type.kind() == CelKind.STRUCT) { + return ctx.mkAnd( + typeSystem.isMessage(val), + ctx.mkEq( + typeSystem.getMsgTypeName(typeSystem.getMessageRef(val)), ctx.mkString(type.name()))); + } + // Fallback: no type constraint + return ctx.mkTrue(); + } + + private BoolExpr getBoundedMapBijection( + ArrayExpr mapPresence, SeqExpr seq, ArithExpr lengthExpr) { + List constraints = new ArrayList<>(); + for (int i = 0; i < comprehensionUnrollLimit; i++) { + for (int j = i + 1; j < comprehensionUnrollLimit; j++) { + BoolExpr validPair = ctx.mkLt(ctx.mkInt(j), lengthExpr); + BoolExpr notEqual = + ctx.mkNot(ctx.mkEq(ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkNth(seq, ctx.mkInt(j)))); + constraints.add(ctx.mkImplies(validPair, notEqual)); + } + } + + BoolExpr isNotTruncated = ctx.mkLe(lengthExpr, ctx.mkInt(comprehensionUnrollLimit)); + + ArrayExpr seqMap = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse()); + for (int i = 0; i < comprehensionUnrollLimit; i++) { + seqMap = + (ArrayExpr) + ctx.mkITE( + ctx.mkLt(ctx.mkInt(i), lengthExpr), + ctx.mkStore(seqMap, ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkTrue()), + seqMap); + } + constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap))); + return CelZ3Exprs.mkAndFlattened(ctx, constraints); + } + + CelZ3TypeConstraintGenerator( + Context ctx, CelZ3TypeSystem typeSystem, int comprehensionUnrollLimit) { + this.ctx = ctx; + this.typeSystem = typeSystem; + this.comprehensionUnrollLimit = comprehensionUnrollLimit; + } +} 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))))