From ca1978b469a028a7bc44f694658daddc654c4265 Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Wed, 30 Sep 2026 12:37:01 -0700 Subject: [PATCH] Fix soundness gaps for dyn-typed values in truncated containers PiperOrigin-RevId: 991155065 --- .../cel/verifier/CelAstToZ3Translator.java | 107 +++++++-- .../dev/cel/verifier/CelVerifierZ3Impl.java | 33 ++- .../cel/verifier/CelZ3OperatorTranslator.java | 220 ++++++++++++------ .../dev/cel/verifier/CelZ3TypeSystem.java | 73 +++--- .../dev/cel/verifier/TranslatedValue.java | 25 +- .../cel/verifier/CelVerifierZ3ImplTest.java | 218 +++++++++++++++-- 6 files changed, 508 insertions(+), 168 deletions(-) diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index f87f0023f..26b8d9a88 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -87,6 +87,7 @@ final class CelAstToZ3Translator { private final CelZ3OperatorTranslator operatorTranslator; private final Map symbolTable; private final Set typeConstraints; + private final Map, CelType> inputVariableTypes; private final ImmutableSet unknownIdentifiers; private final int comprehensionUnrollLimit; private final CelTypeProvider typeProvider; @@ -251,6 +252,7 @@ private TranslatedValue translateIdent(CelExpr celExpr, CelAbstractSyntaxTree as name, n -> { Expr v = ctx.mkConst(n, typeSystem.celValueSort()); + inputVariableTypes.put(v, type); // Variables at rest can never be pre-cooked Errors // Basically prevents error being a counterexample of var == var @@ -286,6 +288,7 @@ private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast // check to a trivial identity check (e.g., `list_ref_0 == list_ref_0`). if (listRef == null) { SeqExpr seq = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort())); + List> values = new ArrayList<>(); ImmutableList optionalIndices = createList.optionalIndices(); ImmutableList elements = createList.elements(); for (int i = 0; i < elements.size(); i++) { @@ -299,19 +302,23 @@ private TranslatedValue translateList(CelExpr celExpr, CelAbstractSyntaxTree ast elem = TranslatedValue.create(checkedValue, element, typeSystem, elem.isApproximate()); Expr optRef = typeSystem.getOptionalRef(elem.z3Expr()); + Expr value = typeSystem.getOptionalValue(optRef); seq = (SeqExpr) ctx.mkITE( typeSystem.optHasValue(optRef), - typeSystem.mkConcatSafe(seq, ctx.mkUnit(typeSystem.getOptionalValue(optRef))), + typeSystem.mkConcatSafe(seq, ctx.mkUnit(value)), seq); + values.add(value); } else { seq = typeSystem.mkConcatSafe(seq, ctx.mkUnit(elem.z3Expr())); + values.add(elem.z3Expr()); } elementsTv.add(elem); } listRef = typeSystem.mkListRefConst(LIST_REF_PREFIX); typeConstraints.add(ctx.mkEq(typeSystem.getSeq(listRef), seq)); + propagateTruncatedTypeConstraint(typeSystem.wrapList(listRef), values); Expr finalListRef = listRef; cacheKey.ifPresent(key -> listLiteralCache.put(key, finalListRef)); } @@ -329,6 +336,7 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast) Expr keysSeq = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort())); List elementsTv = new ArrayList<>(); + List> values = new ArrayList<>(); for (CelExpr.CelMap.Entry entryAst : createMap.entries()) { TranslatedValue keyTv = translateExpr(entryAst.key(), ast); @@ -350,6 +358,7 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast) finalValue = typeSystem.getOptionalValue(optRef); } elementsTv.add(valueTv); + values.add(finalValue); BoolExpr keyAlreadyPresent = (BoolExpr) ctx.mkSelect(mapPresence, key); BoolExpr shouldInsertKey = ctx.mkAnd(ctx.mkNot(keyAlreadyPresent), finalPresence); @@ -368,9 +377,25 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast) typeConstraints.add(ctx.mkEq(typeSystem.getMapKeys(mapRef), keysSeq)); Expr result = typeSystem.wrapMap(mapRef); + propagateTruncatedTypeConstraint(result, values); return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv); } + /** + * Marks {@code container} as having a truncated type constraint if any of {@code elements} has + * one, unless it is an error or unknown: those are shared terms that hold no elements. + */ + private void propagateTruncatedTypeConstraint(Expr container, Iterable> elements) { + BoolExpr hasTruncated = + ctx.mkOr( + typeSystem.isErrorOrUnknown(container), + typeSystem.hasTruncatedTypeConstraint(container)); + for (Expr element : elements) { + typeConstraints.add( + ctx.mkImplies(typeSystem.hasTruncatedTypeConstraint(element), hasTruncated)); + } + } + private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree ast) { CelExpr.CelStruct createStruct = celExpr.struct(); if (isJsonWkt(createStruct.messageName())) { @@ -673,8 +698,13 @@ private TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree a typeConstraints.add(createTypeConstraint(fieldAccess, exprId, ast)); - return TranslatedValue.propagateStrict( - ctx, typeSystem, fieldAccess, celExpr, ImmutableList.of(operandTv)); + TranslatedValue result = + TranslatedValue.propagateStrict( + ctx, typeSystem, fieldAccess, celExpr, ImmutableList.of(operandTv)); + // Map presence is only linked to the keys up to the unroll limit. + return operandType.kind() == CelKind.STRUCT + ? result + : result.withApproximation(operatorTranslator.isTruncatedMap(operand)); } private TranslatedValue translateBlock( @@ -710,7 +740,14 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { return operatorTranslator .translateFunctionCall(functionName, args, exprId, ast) - .map(tv -> TranslatedValue.create(tv.z3Expr(), expr, typeSystem, tv.isApproximate())) + .map( + tv -> { + if (mayEmbedArgs(functionName, ast.getTypeOrThrow(exprId))) { + propagateTruncatedTypeConstraint( + tv.z3Expr(), Iterables.transform(args, TranslatedValue::z3Expr)); + } + return TranslatedValue.create(tv.z3Expr(), expr, typeSystem, tv.isApproximate()); + }) .orElseGet( () -> { // Uninterpreted function @@ -732,6 +769,19 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { }); } + /** + * Whether a call may construct a container that embeds its args (e.g. list concatenation, map + * insertion or optional.of). Indexing and conditionals return existing values instead, so + * propagating to them would needlessly taint e.g. an element whenever its container has a + * truncated type constraint. + */ + private static boolean mayEmbedArgs(String functionName, CelType resultType) { + return (!CelZ3OperatorTranslator.isStaticallyKnown(resultType) + || !resultType.parameters().isEmpty()) + && !functionName.equals(Operator.INDEX.getFunction()) + && !functionName.equals(Operator.CONDITIONAL.getFunction()); + } + private T withScope(String varName, TranslatedValue value, Supplier action) { TranslatedValue prev = symbolTable.put(varName, value); try { @@ -856,7 +906,8 @@ private TranslatedValue translateDynamicComprehension( if (!isList && !isMap) { BoolExpr isRuntimeListOrMap = ctx.mkOr(typeSystem.isList(iterRange), typeSystem.isMap(iterRange)); - Expr result = ctx.mkITE(isRuntimeListOrMap, typeSystem.mkUnknown(), typeSystem.mkError()); + Expr result = + ctx.mkITE(isRuntimeListOrMap, mkParameterizedUnknown(celExpr, ast), typeSystem.mkError()); return TranslatedValue.create(result, celExpr, typeSystem, isRuntimeListOrMap); } @@ -1063,14 +1114,17 @@ private TranslatedValue unrollMapAndFilter( Expr iterRangeExpr = iterRangeTv.z3Expr(); BoolExpr rangeIsError = typeSystem.isError(iterRangeExpr); BoolExpr rangeIsUnknown = typeSystem.isUnknown(iterRangeExpr); - BoolExpr isNotError = ctx.mkNot(typeSystem.isError(resultTv.z3Expr())); - BoolExpr shouldYieldUnknown = ctx.mkAnd(isTruncated, isNotError); + // 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( - ctx.mkOr(rangeIsUnknown, shouldYieldUnknown), mkParameterizedUnknown(celExpr, ast)) + .addCase(isAbstracted, mkParameterizedUnknown(celExpr, ast)) .build(resultTv.z3Expr()); BoolExpr finalTaint = @@ -1078,7 +1132,8 @@ private TranslatedValue unrollMapAndFilter( ctx.mkITE( ctx.mkOr(rangeIsError, rangeIsUnknown), iterRangeTv.isApproximate(), - CelZ3TypeSystem.mkOrFlattened(ctx, resultTv.isApproximate(), shouldYieldUnknown)); + CelZ3TypeSystem.mkOrFlattened( + ctx, resultTv.isApproximate(), isTruncated, isConditionUnmodeled)); return TranslatedValue.create(finalResult, celExpr, typeSystem, finalTaint); } @@ -1200,6 +1255,11 @@ private static boolean isBooleanAccuInit(CelComprehension comp, boolean expected && 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()) @@ -1280,7 +1340,7 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { // 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]) + // typeConstraint(seq[i]). BoolExpr isList = typeSystem.isList(val); CelType elemType = ((ListType) type).elemType(); @@ -1290,6 +1350,13 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { 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); @@ -1323,6 +1390,14 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { 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); @@ -1400,7 +1475,8 @@ private Expr mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast) smtArgs.add(translateExpr(freeVar, ast).z3Expr()); } - return typeSystem.mkParameterizedUnknown(sig.staticHash(), smtArgs.build()); + return typeSystem.mkParameterizedUnknown( + "!trunc_" + Long.toHexString(sig.staticHash()), smtArgs.build()); } CelAstToZ3Translator( @@ -1408,17 +1484,20 @@ private Expr mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast) int comprehensionUnrollLimit, ImmutableSet unknownIdentifiers, CelZ3FunctionRegistry functionRegistry, - CelTypeProvider typeProvider) { + CelTypeProvider typeProvider, + boolean parameterizeUnknowns) { this.ctx = ctx; this.comprehensionUnrollLimit = comprehensionUnrollLimit; - this.typeSystem = new CelZ3TypeSystem(ctx); + 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<>(); diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index 2e957622c..85cd29a8e 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -192,16 +192,21 @@ public CelVerificationResult verifyEquivalence( // Fall back to original ASTs if canonicalization or re-typechecking fails } try (Context ctx = new Context(ImmutableMap.of("model", "true"))) { - CelAstToZ3Translator translator = - new CelAstToZ3Translator( - ctx, comprehensionUnrollLimit, unknownIdentifiers, functionRegistry, typeProvider); - translator.getTypeSystem().enableParameterizedUnknownPropagation(); + CelAstToZ3Translator translator = newTranslator(ctx, /* parameterizeUnknowns= */ true); TranslatedValue tvA = translator.translate(astA); TranslatedValue tvB = translator.translate(astB); BoolExpr divergenceCondition = ctx.mkNot(ctx.mkEq(tvA.z3Expr(), tvB.z3Expr())); - BoolExpr combinedTaint = ctx.mkOr(tvA.isApproximate(), tvB.isApproximate()); + // Parameterized unknowns are keyed on the operation producing them, whereas CEL identifies + // 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( + ctx, + tvA.isApproximate(), + tvB.isApproximate(), + ctx.mkAnd(tvA.isZ3Unknown(), tvB.isZ3Unknown())); Solver solver = newSolver(ctx); for (BoolExpr constraint : translator.getTypeConstraints()) { @@ -273,9 +278,7 @@ CelVerificationResult verifyImplication( } try (Context ctx = new Context(ImmutableMap.of("model", "true"))) { - CelAstToZ3Translator translator = - new CelAstToZ3Translator( - ctx, comprehensionUnrollLimit, unknownIdentifiers, functionRegistry, typeProvider); + CelAstToZ3Translator translator = newTranslator(ctx, /* parameterizeUnknowns= */ false); for (Map.Entry entry : boundSymbols.entrySet()) { TranslatedValue tv = translator.translate(entry.getValue()); @@ -350,9 +353,7 @@ CelVerificationResult verifyImplication( private CelVerificationResult checkSatisfiability( CelAbstractSyntaxTree ast, boolean searchForCounterexample) throws CelVerificationException { try (Context ctx = new Context(ImmutableMap.of("model", "true"))) { - CelAstToZ3Translator translator = - new CelAstToZ3Translator( - ctx, comprehensionUnrollLimit, unknownIdentifiers, functionRegistry, typeProvider); + CelAstToZ3Translator translator = newTranslator(ctx, /* parameterizeUnknowns= */ false); TranslatedValue tv = translator.translate(ast); BoolExpr condition = translator.isTrue(tv.z3Expr()); @@ -502,6 +503,16 @@ private Solver newSolver(Context ctx) { return solver; } + private CelAstToZ3Translator newTranslator(Context ctx, boolean parameterizeUnknowns) { + return new CelAstToZ3Translator( + ctx, + comprehensionUnrollLimit, + unknownIdentifiers, + functionRegistry, + typeProvider, + parameterizeUnknowns); + } + private static String getCounterexampleString( Context ctx, CelZ3TypeSystem typeSystem, diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index 1744b81d0..8d8c34aec 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -44,10 +44,12 @@ import dev.cel.verifier.axioms.CelZ3OverloadResult; import dev.cel.verifier.axioms.CelZ3OverloadTranslator; import java.util.ArrayList; +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. @@ -56,6 +58,7 @@ final class CelZ3OperatorTranslator { private final CelZ3TypeSystem typeSystem; private final Consumer constraintSink; private final BiFunction, CelType, BoolExpr> typeConstraintGenerator; + private final Function, CelType> guaranteedTypes; private final CelZ3FunctionRegistry functionRegistry; private final int comprehensionUnrollLimit; @@ -130,9 +133,20 @@ Optional translateFunctionCall( return opOpt.isPresent() ? Optional.of(resultChain) : Optional.empty(); } - if (opOpt.isPresent() && opOpt.get() == Operator.IN) { - constrainInWitnessTypes( - z3Args.get(0), z3Args.get(1), extractAstTypeOrDefault(args.get(1), ast)); + Operator op = opOpt.orElse(null); + if (op == Operator.IN) { + currentApprox = + CelZ3TypeSystem.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. + Expr operand = z3Args.get(0); + Expr target = + ctx.mkITE( + typeSystem.isOptional(operand), + typeSystem.getOptionalValue(typeSystem.getOptionalRef(operand)), + operand); + currentApprox = CelZ3TypeSystem.mkOrFlattened(ctx, currentApprox, isTruncatedMap(target)); } return Optional.of( @@ -143,14 +157,19 @@ Optional translateFunctionCall( } /** - * Constrains every value that {@code InAxiom} may find in {@code rhs} to the static element (or - * key) type. + * Constrains every value that {@code InAxiom} may find in {@code rhs} to its guaranteed element + * (or key) type, and returns the condition under which the result remains approximate. * *

Container type constraints are only unrolled up to the comprehension unroll limit, so - * without this, a match beyond it could be an ill-typed value (e.g. a string found in a list of - * ints). + * without this, a match beyond it could violate the element type (e.g. a string found in a list + * of ints). This cannot help when the element type is not guaranteed and concrete, nor with map + * presence, which is only linked to the keys up to that limit. */ - private void constrainInWitnessTypes(Expr lhs, Expr rhs, CelType rhsType) { + private BoolExpr constrainInWitnessTypes( + TranslatedValue lhsTv, TranslatedValue rhsTv, CelAbstractSyntaxTree ast) { + Expr lhs = lhsTv.z3Expr(); + Expr rhs = rhsTv.z3Expr(); + CelType rhsType = guaranteedType(rhsTv); if (rhsType instanceof ListType) { // IN_LIST probes lhs itself, its int/uint reinterpretation for cross-type numeric equality, // and every zero (0.0 == -0.0 == 0 == 0u). @@ -175,6 +194,10 @@ private void constrainInWitnessTypes(Expr lhs, Expr rhs, CelType rhsType) ctx.mkAnd(typeSystem.isList(rhs), structContains), typeConstraintGenerator.apply(cand, elemType))); } + // With a concrete element type, the constraints above cover any match in rhs. + return isConcrete(elemType) + ? mayObserveTruncatedTypeConstraint(ast, lhsTv) + : mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv); } else if (rhsType instanceof MapType) { // IN_MAP only probes the presence of lhs itself. ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(rhs)); @@ -183,7 +206,10 @@ private void constrainInWitnessTypes(Expr lhs, Expr rhs, CelType rhsType) ctx.mkImplies( ctx.mkAnd(typeSystem.isMap(rhs), inMap), typeConstraintGenerator.apply(lhs, ((MapType) rhsType).keyType()))); + return isTruncatedMap(rhs); } + return CelZ3TypeSystem.mkOrFlattened( + ctx, isTruncatedMap(rhs), mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv)); } private BoolExpr mkTypeGuard(Expr arg, CelType expectedType) { @@ -330,7 +356,11 @@ private TranslatedValue translateBinaryLogicalAndOr( BoolExpr hasMatch = isAnd ? ctx.mkOr(aFalse, bFalse) : ctx.mkOr(aTrue, bTrue); BoolExpr hasUnknown = ctx.mkOr(a.isZ3Unknown(), b.isZ3Unknown()); - BoolExpr hasError = ctx.mkOr(a.isZ3Error(), b.isZ3Error()); + // Non-boolean operands are no-overload errors. + BoolExpr hasError = + ctx.mkOr( + ctx.mkNot(ctx.mkOr(aIsBool, a.isZ3Unknown())), + ctx.mkNot(ctx.mkOr(bIsBool, b.isZ3Unknown()))); BoolExpr aMatch = isAnd ? aFalse : aTrue; BoolExpr bMatch = isAnd ? bFalse : bTrue; @@ -340,20 +370,10 @@ private TranslatedValue translateBinaryLogicalAndOr( ctx.mkAnd(aMatch, ctx.mkNot(a.isApproximate())), ctx.mkAnd(bMatch, ctx.mkNot(b.isApproximate()))); - BoolExpr hasSafeError = - ctx.mkOr( - ctx.mkAnd(a.isZ3Error(), ctx.mkNot(a.isApproximate())), - ctx.mkAnd(b.isZ3Error(), ctx.mkNot(b.isApproximate()))); - - BoolExpr hasSafeUnknown = - ctx.mkOr( - ctx.mkAnd(a.isZ3Unknown(), ctx.mkNot(a.isApproximate())), - ctx.mkAnd(b.isZ3Unknown(), ctx.mkNot(b.isApproximate()))); - String opName = isAnd ? Operator.LOGICAL_AND.getFunction() : Operator.LOGICAL_OR.getFunction(); Expr unknownResult = typeSystem.isParameterizingUnknowns() - ? typeSystem.mkPropagatedUnknown(opName, ImmutableList.of(a.z3Expr(), b.z3Expr())) + ? typeSystem.mkParameterizedUnknown(opName, ImmutableList.of(a.z3Expr(), b.z3Expr())) : ctx.mkITE(a.isZ3Unknown(), a.z3Expr(), b.z3Expr()); Expr resultZ3 = @@ -363,18 +383,13 @@ private TranslatedValue translateBinaryLogicalAndOr( .addCase(hasError, typeSystem.mkError()) .build(typeSystem.mkBool(isAnd)); - BoolExpr unknownTaint = - typeSystem.isParameterizingUnknowns() - ? ctx.mkOr(a.isApproximate(), b.isApproximate()) - : ctx.mkNot(hasSafeUnknown); - + // 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 = - (BoolExpr) - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase(hasMatch, ctx.mkNot(hasSafeMatch)) - .addCase(hasUnknown, unknownTaint) - .addCase(hasError, ctx.mkNot(hasSafeError)) - .build(ctx.mkOr(a.isApproximate(), b.isApproximate())); + CelZ3TypeSystem.mkAndFlattened( + ctx, + CelZ3TypeSystem.mkNotFlattened(ctx, hasSafeMatch), + CelZ3TypeSystem.mkOrFlattened(ctx, a.isApproximate(), b.isApproximate())); return TranslatedValue.create(resultZ3, typeSystem, resultTaint); } @@ -602,12 +617,20 @@ private boolean hasOptionalElements(TranslatedValue arg) { && !arg.celExpr().get().list().optionalIndices().isEmpty(); } + /** + * Unrolls equality against a list literal element-wise, adding each element equality's + * approximation to {@code taints}. The lists' own taints don't cover it, since numerically equal + * elements (e.g. {@code 1 == 1u}) needn't be equal terms. + */ private BoolExpr unrollListEquality( - TranslatedValue listA, TranslatedValue listB, CelAbstractSyntaxTree ast) { + TranslatedValue listA, + TranslatedValue listB, + CelAbstractSyntaxTree ast, + List taints) { CelExpr literalListAst = listA.isLiteral(ExprKind.Kind.LIST) ? listA.celExpr().get() : listB.celExpr().get(); - CelType type0 = extractAstTypeOrDefault(listA, ast); - CelType type1 = extractAstTypeOrDefault(listB, ast); + CelType type0 = guaranteedType(listA); + CelType type1 = guaranteedType(listB); SeqExpr seq0 = typeSystem.getSeq(typeSystem.getListRef(listA.z3Expr())); SeqExpr seq1 = typeSystem.getSeq(typeSystem.getListRef(listB.z3Expr())); @@ -638,6 +661,7 @@ private BoolExpr unrollListEquality( BoolExpr isTrue = ctx.mkAnd(isBool, (BoolExpr) typeSystem.unwrapBool(eqZ3)); equalities.add(isTrue); + taints.add(elemEquality.isApproximate()); } return CelZ3TypeSystem.mkAndFlattened(ctx, equalities); @@ -661,6 +685,8 @@ private TranslatedValue translateEquality( CelType type1 = extractAstTypeOrDefault(arg1, ast); BoolExpr equality; + List taints = new ArrayList<>(); + taints.add(mayObserveTruncatedTypeConstraint(ast, arg0, arg1)); if (isNumericType(type0) && isNumericType(type1)) { equality = getNumericEquality(arg0, arg1, ast); @@ -669,7 +695,7 @@ private TranslatedValue translateEquality( && (arg0.isLiteral(ExprKind.Kind.LIST) || arg1.isLiteral(ExprKind.Kind.LIST)) && !hasOptionalElements(arg0) && !hasOptionalElements(arg1)) { - equality = unrollListEquality(arg0, arg1, ast); + equality = unrollListEquality(arg0, arg1, ast, taints); } else if (isStaticallyKnown(type0) && isStaticallyKnown(type1)) { equality = typeSystem.getStructuralEquality(z3Arg0, z3Arg1); } else { @@ -685,7 +711,7 @@ private TranslatedValue translateEquality( (BoolExpr) ctx.mkITE( ctx.mkAnd(typeSystem.isList(z3Arg0), typeSystem.isList(z3Arg1)), - unrollListEquality(arg0, arg1, ast), + unrollListEquality(arg0, arg1, ast, taints), structuralEq); } @@ -705,7 +731,8 @@ private TranslatedValue translateEquality( Expr equalityExpr = typeSystem.wrapBool(equality); String opName = isEquals ? Operator.EQUALS.getFunction() : Operator.NOT_EQUALS.getFunction(); - return TranslatedValue.propagateStrict(ctx, typeSystem, opName, equalityExpr, arg0, arg1); + return TranslatedValue.propagateStrict(ctx, typeSystem, opName, equalityExpr, arg0, arg1) + .withApproximation(CelZ3TypeSystem.mkOrFlattened(ctx, taints)); } private Expr buildListIndex( @@ -908,6 +935,7 @@ private TranslatedValue translateIndex( TranslatedValue lhs = args.get(0); TranslatedValue rhs = args.get(1); CelType lhsType = extractAstTypeOrDefault(lhs, ast); + boolean isLhsTypeGuaranteed = lhsType.equals(guaranteedType(lhs)); Expr lhsTrans = lhs.z3Expr(); Expr rhsTrans = rhs.z3Expr(); @@ -929,8 +957,10 @@ private TranslatedValue translateIndex( } } - Expr actualValue = - buildAndConstrainIndex(lhsTrans, rhsTrans, lhsType, shouldEvaluate, isOptional); + TranslatedValue element = + buildAndConstrainIndex( + lhsTrans, rhsTrans, lhsType, isLhsTypeGuaranteed, shouldEvaluate, isOptional); + Expr actualValue = element.z3Expr(); if (isOptional) { actualValue = @@ -951,21 +981,22 @@ private TranslatedValue translateIndex( ctx.mkLt( typeSystem.getInt(rhsTrans), ctx.mkLength(typeSystem.getSeq(typeSystem.getListRef(lhsTrans))))); - BoolExpr isMapIndexTruncated = - ctx.mkAnd( - shouldEvaluate, - typeSystem.isMap(lhsTrans), - ctx.mkGt( - ctx.mkLength(typeSystem.getMapKeys(typeSystem.getMapRef(lhsTrans))), - ctx.mkInt(comprehensionUnrollLimit))); + BoolExpr isMapIndexTruncated = ctx.mkAnd(shouldEvaluate, isTruncatedMap(lhsTrans)); return TranslatedValue.propagateStrict(ctx, typeSystem, opName, actualValue, args) - .withApproximation(ctx.mkOr(isListIndexTruncated, isMapIndexTruncated)); + .withApproximation( + CelZ3TypeSystem.mkOrFlattened( + ctx, isListIndexTruncated, isMapIndexTruncated, element.isApproximate())); } - private Expr buildAndConstrainIndex( + /** + * Returns the element of {@code lhsTrans} at {@code rhsTrans}, which is approximate if it may not + * conform to a static element type that is not guaranteed. + */ + private TranslatedValue buildAndConstrainIndex( Expr lhsTrans, Expr rhsTrans, CelType lhsType, + boolean isLhsTypeGuaranteed, BoolExpr shouldEvaluate, boolean isOptional) { CelType expectedElemType = null; @@ -990,23 +1021,32 @@ private Expr buildAndConstrainIndex( } CelType finalType = isOptional ? OptionalType.create(expectedElemType) : expectedElemType; - - constraintSink.accept( - ctx.mkImplies( - ctx.mkAnd(shouldEvaluate, ctx.mkNot(typeSystem.isError(actualValue))), - typeConstraintGenerator.apply(actualValue, finalType))); - - return actualValue; + BoolExpr isDefined = ctx.mkAnd(shouldEvaluate, ctx.mkNot(typeSystem.isError(actualValue))); + BoolExpr typeConstraint = typeConstraintGenerator.apply(actualValue, finalType); + if (isLhsTypeGuaranteed) { + constraintSink.accept(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 + // string), so the element may not conform. + return TranslatedValue.create( + actualValue, + typeSystem, + CelZ3TypeSystem.mkAndFlattened( + ctx, isDefined, CelZ3TypeSystem.mkNotFlattened(ctx, typeConstraint))); } BoolExpr isListGuard = ctx.mkAnd(shouldEvaluate, typeSystem.isList(lhsTrans), typeSystem.isInt(rhsTrans)); BoolExpr isMapGuard = ctx.mkAnd(shouldEvaluate, typeSystem.isMap(lhsTrans)); - return CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional)) - .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional)) - .build(typeSystem.mkError()); + return TranslatedValue.create( + CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional)) + .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional)) + .build(typeSystem.mkError()), + typeSystem, + ctx.mkFalse()); } private TranslatedValue translateConditional( @@ -1026,7 +1066,7 @@ private TranslatedValue translateConditional( Expr unknownResult = typeSystem.isParameterizingUnknowns() - ? typeSystem.mkPropagatedUnknown( + ? typeSystem.mkParameterizedUnknown( Operator.CONDITIONAL.getFunction(), ImmutableList.of(cond.z3Expr(), trueBranch.z3Expr(), falseBranch.z3Expr())) : cond.z3Expr(); @@ -1040,16 +1080,11 @@ private TranslatedValue translateConditional( BoolExpr hasSafeError = ctx.mkAnd(hasError, ctx.mkNot(cond.isApproximate())); BoolExpr hasSafeUnknown = ctx.mkAnd(hasUnknown, ctx.mkNot(cond.isApproximate())); - BoolExpr unknownTaint = - typeSystem.isParameterizingUnknowns() - ? ctx.mkOr( - cond.isApproximate(), trueBranch.isApproximate(), falseBranch.isApproximate()) - : ctx.mkNot(hasSafeUnknown); BoolExpr resultTaint = (BoolExpr) CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase(hasUnknown, unknownTaint) + .addCase(hasUnknown, ctx.mkNot(hasSafeUnknown)) .addCase(hasError, ctx.mkNot(hasSafeError)) .addCase(condTrue, ctx.mkOr(cond.isApproximate(), trueBranch.isApproximate())) .build(ctx.mkOr(cond.isApproximate(), falseBranch.isApproximate())); @@ -1068,27 +1103,78 @@ private static CelType extractAstTypeOrDefault(TranslatedValue val, CelAbstractS return val.celExpr().map(node -> ast.getTypeOrThrow(node.id())).orElse(SimpleType.DYN); } - private static boolean isStaticallyKnown(CelType type) { + /** + * Returns the type that {@code val} is guaranteed to conform to at runtime: the declared type of + * an input variable, or else dyn. Global constraints may only be derived from guaranteed types: + * the type checker may narrow static types (e.g. {@code ['a'] + dyn_var} is typed list(string)), + * so constraints derived from those could exclude valid inputs. + */ + private CelType guaranteedType(TranslatedValue val) { + return guaranteedTypes.apply(val.z3Expr()); + } + + /** + * Whether {@code type} itself is neither dyn nor a type parameter. Unlike {@link #isConcrete}, + * its type parameters may still be (e.g. {@code list(dyn)}). + */ + static boolean isStaticallyKnown(CelType type) { CelKind kind = type.kind(); return !kind.isDyn() && !kind.isTypeParam(); } + /** Whether {@code type} and, recursively, its type parameters are statically known. */ + private static boolean isConcrete(CelType type) { + return isStaticallyKnown(type) + && type.parameters().stream().allMatch(CelZ3OperatorTranslator::isConcrete); + } + private static boolean isNumericType(CelType type) { CelKind kind = type.kind(); return kind == CelKind.INT || kind == CelKind.UINT || kind == CelKind.DOUBLE; } + /** + * Whether {@code val} is a map with more keys than the unroll limit, beyond which its presence is + * not linked to its keys. + */ + BoolExpr isTruncatedMap(Expr val) { + return ctx.mkAnd( + typeSystem.isMap(val), + ctx.mkGt( + ctx.mkLength(typeSystem.getMapKeys(typeSystem.getMapRef(val))), + ctx.mkInt(comprehensionUnrollLimit))); + } + + /** + * Whether observing {@code args} together may expose a value beyond a truncated type constraint + * in any of them. Type constraints at the point of observation rule this out only if every arg + * has a concrete static type (unlike e.g. {@code dyn(int_list)}). + */ + private BoolExpr mayObserveTruncatedTypeConstraint( + CelAbstractSyntaxTree ast, TranslatedValue... args) { + if (Arrays.stream(args).allMatch(arg -> isConcrete(extractAstTypeOrDefault(arg, ast)))) { + return ctx.mkFalse(); + } + return CelZ3TypeSystem.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; this.functionRegistry = functionRegistry; 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 b3d1c3538..666a5c0d4 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -131,6 +131,7 @@ public final class CelZ3TypeSystem { private static final String FUNC_MSG_VALUES = "msg_values"; private static final String FUNC_MSG_PRESENCE = "msg_presence"; private static final String FUNC_MSG_TYPE_NAME = "msg_type_name"; + private static final String FUNC_HAS_TRUNCATED_TYPE_CONSTRAINT = "!has_truncated_type_constraint"; private final Context ctx; private final Map> funcDeclCache; @@ -169,8 +170,9 @@ public final class CelZ3TypeSystem { private final FuncDecl msgValuesFunc; private final FuncDecl msgPresenceFunc; private final FuncDecl msgTypeNameFunc; + private final FuncDecl hasTruncatedTypeConstraintFunc; - private boolean propagateParameterizedUnknowns; + private final boolean parameterizeUnknowns; public Expr mkListRefConst(String prefix) { return ctx.mkFreshConst(prefix, listRefSort); @@ -454,44 +456,19 @@ private Expr mkUnknown(Expr unknownId) { return ctx.mkApp(unknownCons.ConstructorDecl(), unknownId); } - /** Creates a parameterized unknown representing a truncated comprehension. */ - Expr mkParameterizedUnknown(long staticHash, List> smtArgs) { - Sort[] domain = new Sort[smtArgs.size()]; - for (int i = 0; i < smtArgs.size(); i++) { - domain[i] = celValueSort(); - } - - String ufName = "!trunc_" + Long.toHexString(staticHash); - FuncDecl truncUf = internFuncDecl(ufName, domain, unknownIdSort); - - Expr uniqueUnknownId = - smtArgs.isEmpty() - ? ctx.mkConst(ufName, unknownIdSort) - : ctx.mkApp(truncUf, smtArgs.toArray(new Expr[0])); - - return mkUnknown(uniqueUnknownId); - } - - void enableParameterizedUnknownPropagation() { - this.propagateParameterizedUnknowns = true; - } - - boolean isParameterizingUnknowns() { - return propagateParameterizedUnknowns; - } - /** - * Creates a parameterized unknown representing an operation applied to one or more unknown - * values, preserving EUF congruence only when both the operation and all arguments match. - * - *

Only use this when {@link #isParameterizingUnknowns()} is true. Otherwise, verification only - * observes whether a value is unknown, not which unknown it is. + * Creates an unknown whose ID is the uninterpreted function {@code name} applied to {@code args}, + * so that EUF only equates unknowns produced by the same operation over the same arguments. */ - Expr mkPropagatedUnknown(String opName, List> allArgs) { - Sort[] domain = new Sort[allArgs.size()]; + Expr mkParameterizedUnknown(String name, List> args) { + Sort[] domain = new Sort[args.size()]; Arrays.fill(domain, celValueSort()); - FuncDecl propUf = internFuncDecl(opName, domain, unknownIdSort); - return mkUnknown(ctx.mkApp(propUf, allArgs.toArray(new Expr[0]))); + FuncDecl uf = internFuncDecl(name, domain, unknownIdSort); + return mkUnknown(ctx.mkApp(uf, args.toArray(new Expr[0]))); + } + + boolean isParameterizingUnknowns() { + return parameterizeUnknowns; } /** @@ -514,10 +491,11 @@ Expr propagateErrorAndUnknown( errors[i] = isError(checkArgs.get(i)); unknowns[i] = isUnknown(checkArgs.get(i)); } - // Only equivalence checks, which parameterize unknowns, can tell unknowns apart. The other - // checks only observe whether a value is unknown, so the generic unknown suffices for them. + // Equivalence checks compare unknowns, which may stand in for truncated values that differ, so + // they must not equate unknowns derived from different inputs. The other checks only observe + // whether a value is unknown, so the generic unknown suffices for them. Expr unknownResult = - propagateParameterizedUnknowns ? mkPropagatedUnknown(opName, allArgs) : mkUnknown(); + parameterizeUnknowns ? mkParameterizedUnknown(opName, allArgs) : mkUnknown(); BoolExpr hasError = ctx.mkOr(errors); BoolExpr hasUnknown = ctx.mkOr(unknowns); // Unknowns have higher precedence than error @@ -782,6 +760,16 @@ public Expr getMsgTypeName(Expr msgRef) { return ctx.mkApp(msgTypeNameFunc, msgRef); } + /** + * Whether {@code val} is, or was built from, a container whose type constraint was truncated at + * the unroll limit, so it may hold elements that do not conform to their static type. This is + * uninterpreted, but forced by the type constraints of containers longer than the limit, and + * propagated to containers built from them. + */ + BoolExpr hasTruncatedTypeConstraint(Expr val) { + return (BoolExpr) ctx.mkApp(hasTruncatedTypeConstraintFunc, val); + } + /** Checks if the given arithmetic expression overflows a 64-bit integer. */ public BoolExpr checkIntOverflow(ArithExpr result) { return ctx.mkOr( @@ -958,7 +946,7 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) { return ctx.mkNot(arg); } - CelZ3TypeSystem(Context ctx) { + CelZ3TypeSystem(Context ctx, boolean parameterizeUnknowns) { this.ctx = ctx; this.funcDeclCache = new HashMap<>(); this.boolCons = @@ -1099,6 +1087,9 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) { ctx.mkArraySort(ctx.getStringSort(), ctx.getBoolSort())); this.msgTypeNameFunc = ctx.mkFuncDecl(FUNC_MSG_TYPE_NAME, new Sort[] {this.messageRefSort}, ctx.getStringSort()); - this.propagateParameterizedUnknowns = false; + this.hasTruncatedTypeConstraintFunc = + ctx.mkFuncDecl( + FUNC_HAS_TRUNCATED_TYPE_CONSTRAINT, new Sort[] {this.celValueSort}, ctx.getBoolSort()); + this.parameterizeUnknowns = parameterizeUnknowns; } } diff --git a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java index f7aa95bdb..7172a6a4f 100644 --- a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java +++ b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java @@ -143,7 +143,8 @@ static TranslatedValue propagateStrict( List exactErrors = new ArrayList<>(); List exactUnknowns = new ArrayList<>(); List unknowns = new ArrayList<>(); - List argTaints = new ArrayList<>(args.size()); + List taints = new ArrayList<>(); + taints.add(baseTaint); List> nonConstZ3Args = new ArrayList<>(); List> allZ3Args = new ArrayList<>(args.size()); @@ -151,7 +152,7 @@ static TranslatedValue propagateStrict( Expr z3Expr = arg.z3Expr(); BoolExpr isApprox = arg.isApproximate(); allZ3Args.add(z3Expr); - argTaints.add(isApprox); + taints.add(isApprox); if (arg.isLiteral(ExprKind.Kind.CONSTANT)) { continue; } @@ -163,13 +164,10 @@ static TranslatedValue propagateStrict( unknowns.add(isUnknown); exactErrors.add(CelZ3TypeSystem.mkAndFlattened(ctx, isError, isExact)); - if (!ts.isParameterizingUnknowns()) { - exactUnknowns.add(CelZ3TypeSystem.mkAndFlattened(ctx, isUnknown, isExact)); - } + exactUnknowns.add(CelZ3TypeSystem.mkAndFlattened(ctx, isUnknown, isExact)); } - BoolExpr anyArgTaint = CelZ3TypeSystem.mkOrFlattened(ctx, argTaints); - BoolExpr anyTaint = CelZ3TypeSystem.mkOrFlattened(ctx, baseTaint, anyArgTaint); + BoolExpr anyTaint = CelZ3TypeSystem.mkOrFlattened(ctx, taints); if (nonConstZ3Args.isEmpty()) { return create(baseResult, celExpr, ts, anyTaint); } @@ -178,14 +176,8 @@ static TranslatedValue propagateStrict( ts.propagateErrorAndUnknown(opName, baseResult, nonConstZ3Args, allZ3Args); BoolExpr hasExactError = CelZ3TypeSystem.mkOrFlattened(ctx, exactErrors); + BoolExpr hasExactUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, exactUnknowns); BoolExpr hasUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, unknowns); - // A parameterized unknown is keyed on every argument, so it is only exact if no argument (not - // just the unknown one) is approximate. - BoolExpr hasExactUnknown = - ts.isParameterizingUnknowns() - ? CelZ3TypeSystem.mkAndFlattened( - ctx, hasUnknown, CelZ3TypeSystem.mkNotFlattened(ctx, anyArgTaint)) - : CelZ3TypeSystem.mkOrFlattened(ctx, exactUnknowns); BoolExpr isSafe = CelZ3TypeSystem.mkOrFlattened( @@ -219,8 +211,11 @@ private static String extractOpName(CelExpr expr) { mapSb.append('_').append(entry.optionalEntry()); } return mapSb.toString(); - default: + case LIST: return "LIST_" + expr.list().optionalIndices(); + default: + throw new IllegalArgumentException( + "Unexpected expression kind: " + expr.exprKind().getKind()); } } diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 51f3fa40f..d61607545 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -105,6 +105,8 @@ public final class CelVerifierZ3ImplTest { .addVar("nested_list_2", ListType.create(ListType.create(SimpleType.INT))) .addVar("dyn_list", ListType.create(SimpleType.DYN)) .addVar("dyn_map", MapType.create(SimpleType.DYN, SimpleType.DYN)) + .addVar("dyn_int_map", MapType.create(SimpleType.DYN, SimpleType.INT)) + .addVar("string_dyn_map", MapType.create(SimpleType.STRING, SimpleType.DYN)) .addVar("dyn_var", SimpleType.DYN) .addVar("dyn_var2", SimpleType.DYN) .addVar("opt_var", OptionalType.create(SimpleType.INT)) @@ -154,7 +156,8 @@ private enum IsSatisfiableTestCase { NULL_SATISFIABLE("unknown_var == null", "unknown_var = null"), DYNAMIC_VAR_NUMERIC_EQUALITY("dyn_var == 1 && dyn_var == 1.0", "dyn_var = 1"), DYNAMIC_VAR_NOT_IN_LIST( - "dyn_var == 1.5 && !(dyn_var in dyn_list) && size(dyn_list) > 5", "dyn_var = 1\\.5"), + "dyn_var == 1.5 && !(dyn_var in dyn_list) && size(dyn_list) == 6", "dyn_var = 1\\.5"), + DYNAMIC_LIST_EQUALITY_BEYOND_BMC_LIMIT("dyn_list == [1, 2, 3, 4, 5, 6]", "dyn_list = "), CROSS_NUMERIC_EQUALITY_INT_DYN_EXACT("1 == request", "request = 1"), MACRO_LIMIT("dyn_list.all(x, x == 1)", "Satisfying input:"), STRUCT_FIELD_MISSING_APPROXIMATE_SATISFIABLE("dyn_var.unknown_field", "dyn_var = "), @@ -184,12 +187,20 @@ private enum IsSatisfiableTestCase { INT_MAX_DOUBLE_EQUALITY( "dyn(request) == 9223372036854775808.0", "request = 9223372036854775[2-8]\\d+"), UINT_MAX_DOUBLE_EQUALITY("dyn(u) == 18446744073709551616.0", "u = 1844674407370955\\d+u"), + // The type checker narrows `int_list + dyn_var` to list(int), which must not constrain dyn_var. + IN_NARROWED_LIST_CONCATENATION("dyn('a') in (int_list + dyn_var)", "dyn_var = "), + // Indexing and conditionals return existing values, so they do not inherit truncated type + // constraints from their operands. + DYN_ELEMENT_OF_LONG_NESTED_LIST_EQUALITY( + "size(nested_list) == 6 && dyn(nested_list[0]) == [1]", "nested_list = \\[\\[1\\]"), + DYN_CONDITIONAL_EQUALITY_WITH_LONG_LIST_BRANCH( + "size(int_list) == 6 && dyn(b ? [1] : int_list) == [1]", "b = true"), ; - final String expr; - final ImmutableList expectedFragments; + private final String expr; + private final ImmutableList expectedFragments; - IsSatisfiableTestCase(String expr, String... expectedFragments) { + private IsSatisfiableTestCase(String expr, String... expectedFragments) { this.expr = expr; this.expectedFragments = ImmutableList.copyOf(expectedFragments); } @@ -353,11 +364,62 @@ private enum IsSatisfiableInconclusiveTestCase { APPROXIMATED_DOUBLE_TO_INT("int(1.5) == 1"), APPROXIMATED_INT_TO_STRING("string(123) == '123'"), APPROXIMATED_RANGE("int('123') > 100 && int('123') < 200"), - APPROXIMATED_BRANCHING("int('123') == 123 ? x > 5 : false"); + APPROXIMATED_BRANCHING("int('123') == 123 ? x > 5 : false"), + // Containers are only type-constrained up to the unroll limit, so observing one through dyn may + // expose an element beyond it that violates the static type. + BEYOND_BMC_LIMIT_DYN_LIST_LITERAL_EQUALITY( + "int_list == dyn([1, 2, 3, 4, 5, dyn('not_an_int')])"), + BEYOND_BMC_LIMIT_DYN_NESTED_LIST_LITERAL_EQUALITY( + "nested_list == dyn([[1, 2, 3, 4, 5, dyn('not_an_int')]])"), + // 1 == 1u holds without the inner lists being equal terms, so the flags aren't tied by EUF. + BEYOND_BMC_LIMIT_NESTED_LIST_CROSS_TYPE_LITERAL_EQUALITY( + "dyn(nested_list) == [[dyn(1u), 2, 3, 4, 5, dyn('not_an_int')]]"), + BEYOND_BMC_LIMIT_DYN_MAP_LITERAL_EQUALITY( + "string_int_map == dyn({'a': 1, 'b': 2, 'c': 3, 'd': 4, 'e': 5, 'f': dyn('not_an_int')})"), + BEYOND_BMC_LIMIT_DYN_NESTED_MAP_VALUE_EQUALITY( + "dyn(string_int_list_map) == {'a': [1, 2, 3, 4, 5, dyn('not_an_int')]}"), + BEYOND_BMC_LIMIT_DYN_LIST_LITERAL_ELEMENT_EQUALITY( + "dyn([int_list]) == [[1, 2, 3, 4, 5, dyn('not_an_int')]]"), + BEYOND_BMC_LIMIT_DYN_LIST_LITERAL_OPTIONAL_ELEMENT_EQUALITY( + "dyn([?optional.of(int_list)]) == [[1, 2, 3, 4, 5, dyn('not_an_int')]]"), + BEYOND_BMC_LIMIT_OPTIONAL_LIST_LITERAL_EQUALITY_WITH_DYN_LIST( + "size(int_list) == 6 && dyn([?optional.of(int_list)]) == dyn_list"), + BEYOND_BMC_LIMIT_DYN_MAP_LITERAL_VALUE_EQUALITY( + "dyn({'a': int_list}) == {'a': [1, 2, 3, 4, 5, dyn('not_an_int')]}"), + BEYOND_BMC_LIMIT_DYN_MAP_LITERAL_OPTIONAL_VALUE_EQUALITY( + "dyn({?'a': optional.of(int_list)}) == {'a': [1, 2, 3, 4, 5, dyn('not_an_int')]}"), + BEYOND_BMC_LIMIT_OPTIONAL_MAP_LITERAL_EQUALITY_WITH_DYN_MAP( + "size(int_list) == 6 && dyn({?'a': optional.of(int_list)}) == dyn_map"), + BEYOND_BMC_LIMIT_EQUALITY_WITH_DYN_LIST( + "int_list == dyn_list && size(dyn_list) == 6 && 'not_an_int' in dyn_list"), + BEYOND_BMC_LIMIT_IN_DYN_LIST("size(int_list) == 6 && dyn('not_an_int') in dyn(int_list)"), + BEYOND_BMC_LIMIT_DYN_IN_NESTED_LIST( + "size(nested_list) == 1 && dyn([1, 2, 3, 4, 5, dyn('not_an_int')]) in nested_list"), + BEYOND_BMC_LIMIT_IN_DYN_MAP("size(string_int_map) == 6 && dyn(1) in dyn(string_int_map)"), + BEYOND_BMC_LIMIT_IN_DYN_LIST_CONCATENATION("'a' in dyn(int_list + [1])"), + // A long map's type constraint is truncated even if only its key or its value type is known. + BEYOND_BMC_LIMIT_DYN_KEY_MAP_IN_LITERAL( + "dyn(dyn_int_map) in [{1: 1, 2: 2, 3: 3, 4: 4, 5: 5, 6: dyn('not_an_int')}]"), + BEYOND_BMC_LIMIT_DYN_VALUE_MAP_IN_LITERAL( + "dyn(string_dyn_map) in [{'a': 1, 'b': 2, 'c': 3, 'd': 4, 'e': 5, dyn(6): 6}]"), + // Map presence is only linked to the keys up to the unroll limit. + BEYOND_BMC_LIMIT_MAP_KEYS_IN( + "size(string_int_map) == 6 && ['a', 'b', 'c', 'd', 'e', 'f', 'g'].all(k, k in" + + " string_int_map)"), + BEYOND_BMC_LIMIT_MAP_KEYS_HAS( + "size(string_int_map) == 6 && has(string_int_map.a) && has(string_int_map.b) &&" + + " has(string_int_map.c) && has(string_int_map.d) && has(string_int_map.e) &&" + + " has(string_int_map.f) && has(string_int_map.g)"), + BEYOND_BMC_LIMIT_MAP_KEYS_OPTIONAL_SELECT( + "size(string_int_map) == 6 && string_int_map.?a.hasValue() &&" + + " string_int_map.?b.hasValue() && string_int_map.?c.hasValue() &&" + + " string_int_map.?d.hasValue() && string_int_map.?e.hasValue() &&" + + " string_int_map.?f.hasValue() && string_int_map.?g.hasValue()"), + ; - final String expr; + private final String expr; - IsSatisfiableInconclusiveTestCase(String expr) { + private IsSatisfiableInconclusiveTestCase(String expr) { this.expr = expr; } } @@ -454,11 +516,12 @@ private enum IsUnsatisfiableTestCase { BEYOND_BMC_LIMIT_UNCONSTRAINED_MAP_KEY_TYPE( "size(string_int_map) == 6 && dyn(1) in string_int_map"), LIST_INDEX_DYN_STRING_KEY("int_list[dyn('0')] == 1"), + NON_BOOL_LOGICAL_OPERAND("dyn(1) && true"), ; - final String expr; + private final String expr; - IsUnsatisfiableTestCase(String expr) { + private IsUnsatisfiableTestCase(String expr) { this.expr = expr; } } @@ -982,6 +1045,20 @@ public void isAlwaysTrue_withUnknownIdentifier_evaluatesToUnknown( assertThat(result.message()).contains("x = Unknown"); } + @Test + public void isAlwaysTrue_approximateOperandWithUnknown_inconclusive() throws Exception { + // The truncated `all` may really be false, which absorbs the unknown, so this is always true. + CelAbstractSyntaxTree ast = + CEL.compile("!(int_list.all(x, x > 0) && unknown_var) || int_list.all(x, x > 0)").getAst(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).addUnknownIdentifier("unknown_var").build(); + + CelVerificationResult result = verifier.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + assertThat(result.message()).contains("depends on approximations"); + } + @Test public void isAlwaysTrue_dynamicComprehensionNonBoolYieldsError() throws Exception { // Testing the path where a comprehension step successfully evaluates but yields a @@ -1100,6 +1177,42 @@ public void verifyEquivalence_unknownPrecedenceOverError() throws Exception { assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); } + private enum UnknownIdentifierEquivalenceTestCase { + // CEL identifies an unknown by its attributes, so both sides may yield the same unknown. + LOGICAL_AND_IDENTITY("a && true", "a"), + ADDITION_COMMUTATIVITY("x + 1", "1 + x"), + // An error is not final beyond the unroll limit: a later unknown step overrides it. + TRUNCATED_ERROR_THEN_UNKNOWN( + "int_list.transformList(i, v, i < 5 ? 1 / 0 : unknown_var)", + "int_list.transformList(i, v, 1 / 0)"), + ; + + private final String exprA; + private final String exprB; + + private UnknownIdentifierEquivalenceTestCase(String exprA, String exprB) { + this.exprA = exprA; + this.exprB = exprB; + } + } + + @Test + public void verifyEquivalence_withUnknownIdentifiers_inconclusive( + @TestParameter UnknownIdentifierEquivalenceTestCase testCase) throws Exception { + CelAbstractSyntaxTree astA = CEL.compile(testCase.exprA).getAst(); + CelAbstractSyntaxTree astB = CEL.compile(testCase.exprB).getAst(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL) + .addUnknownIdentifier("a") + .addUnknownIdentifier("x") + .addUnknownIdentifier("unknown_var") + .build(); + + CelVerificationResult result = verifier.verifyEquivalence(astA, astB); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + } + @Test public void verifyEquivalence_freeVariableIndicesDeduplicated() throws Exception { CelAbstractSyntaxTree astA = @@ -1572,12 +1685,35 @@ private enum IsAlwaysTrueViolationTestCase { "size(int_list) == 5 ? int_list[5] == 1 : true", "Condition is not always true\\.", "Counterexample input:"), + // The type checker narrows static types (e.g. `['guest'] + dyn_var` is typed list(string)), so + // those must not constrain inputs, even in subexpressions that are never evaluated. + NARROWED_LIST_IN_DOES_NOT_CONSTRAIN_INPUTS( + "dyn_var != [0] || (false && 'x' in (['guest'] + dyn_var))", + "Condition is not always true\\.", + "Counterexample input:", + "dyn_var = "), + NARROWED_LIST_INDEX_DOES_NOT_CONSTRAIN_INPUTS( + "dyn_var != [0] || (false && (['guest'] + dyn_var)[1] == 'x')", + "Condition is not always true\\.", + "Counterexample input:", + "dyn_var = "), + NARROWED_LIST_EQUALITY_DOES_NOT_CONSTRAIN_INPUTS( + "dyn_var != [1, 2, 3, 4, 5] ||" + + " (false && (['a'] + dyn_var) == ['a', 'b', 'c', 'd', 'e', 'f'])", + "Condition is not always true\\.", + "Counterexample input:", + "dyn_var = "), + NARROWED_ITERATION_VARIABLE_DOES_NOT_CONSTRAIN_INPUTS( + "dyn_int_map != {1: 1} || (false && [dyn_int_map, string_dyn_map].exists(m, dyn(1) in m))", + "Condition is not always true\\.", + "Counterexample input:", + "dyn_int_map = \\{1: 1\\}"), ; - final String expr; - final ImmutableList expectedFragments; + private final String expr; + private final ImmutableList expectedFragments; - IsAlwaysTrueViolationTestCase(String expr, String... expectedFragments) { + private IsAlwaysTrueViolationTestCase(String expr, String... expectedFragments) { this.expr = expr; this.expectedFragments = ImmutableList.copyOf(expectedFragments); } @@ -1642,11 +1778,14 @@ private enum IsInconclusiveTestCase { "x == y && y == port ? dyn_list.all(e, x == x) == dyn_list.all(e, y == port) : true"), LIST_INDEX_BEYOND_BMC_LIMIT("size(int_list) == 6 ? int_list[5] == 1 : true"), MAP_INDEX_BEYOND_BMC_LIMIT("size(string_int_map) == 6 ? string_int_map['a'] == 1 : true"), + // The approximate operand may really be false, which absorbs the error. + LOGICAL_AND_APPROXIMATE_OPERAND_WITH_ERROR( + "size(int_list) < 6 || !(dyn(int_list)[5] == 'x' && 1 / 0 == 1)"), ; - final String expr; + private final String expr; - IsInconclusiveTestCase(String expr) { + private IsInconclusiveTestCase(String expr) { this.expr = expr; } } @@ -1726,12 +1865,13 @@ private enum EquivalenceInconclusiveTestCase { STRUCT_DIFFERENT_DEFAULT_FIELDS_WITH_TRUNCATED_VALUE( "TestAllTypes{single_int64: int_list.all(i, v, i < 5) ? 0 : 1}", "TestAllTypes{single_sint64: int_list.all(i, v, i < 5) ? 0 : 1}"), - CHAINED_MAP_ALL_TRUE_INCONCLUSIVE("int_list.map(x, 1).all(v, v == 1)", "true"); + DYN_RANGE_DIFFERENT_COMPREHENSIONS("dyn_var.all(e, e > 0)", "dyn_var.all(e, e < 0)"), + CHAINED_MAP_ALL_TRUE("int_list.map(x, 1).all(v, v == 1)", "true"); - final String exprA; - final String exprB; + private final String exprA; + private final String exprB; - EquivalenceInconclusiveTestCase(String exprA, String exprB) { + private EquivalenceInconclusiveTestCase(String exprA, String exprB) { this.exprA = exprA; this.exprB = exprB; } @@ -2849,7 +2989,8 @@ public void getNumericEqualityWithConstant_skipsIntForDouble() throws Exception /* comprehensionUnrollLimit= */ 3, /* unknownIdentifiers= */ ImmutableSet.of(), /* functionRegistry= */ CelZ3FunctionRegistry.create(ImmutableList.of()), - /* typeProvider= */ CelVerifierZ3Impl.EMPTY_TYPE_PROVIDER); + /* typeProvider= */ CelVerifierZ3Impl.EMPTY_TYPE_PROVIDER, + /* parameterizeUnknowns= */ false); Expr result = translator.translate(ast).z3Expr(); String resultString = result.toString(); @@ -2870,7 +3011,8 @@ public void getNumericEqualityWithConstant_skipsDoubleForInt() throws Exception /* comprehensionUnrollLimit= */ 3, /* unknownIdentifiers= */ ImmutableSet.of(), /* functionRegistry= */ CelZ3FunctionRegistry.create(ImmutableList.of()), - /* typeProvider= */ CelVerifierZ3Impl.EMPTY_TYPE_PROVIDER); + /* typeProvider= */ CelVerifierZ3Impl.EMPTY_TYPE_PROVIDER, + /* parameterizeUnknowns= */ false); Expr result = translator.translate(ast).z3Expr(); String resultString = result.toString(); @@ -2979,6 +3121,42 @@ public void isAlwaysTrue_customComprehensionWithTrueAccuInit() throws Exception assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); } + @Test + public void isAlwaysTrue_customComprehensionWithLoopCondition_inconclusive() throws Exception { + // first_elem() stops folding once the accumulator is set, so it returns 1 for [1, 2]. The loop + // condition over a non-literal range is not modeled, so the verifier must not claim that the + // result is the last element. + Cel cel = + CelFactory.plannerCelBuilder() + .addVar("int_list", ListType.create(SimpleType.INT)) + .addMacros( + CelMacro.newReceiverMacro( + "first_elem", + 0, + (exprFactory, target, arguments) -> + Optional.of( + exprFactory.fold( + "x", + target, + "accu", + exprFactory.newIntLiteral(-1), + exprFactory.newGlobalCall( + Operator.EQUALS.getFunction(), + exprFactory.newIdentifier("accu"), + exprFactory.newIntLiteral(-1)), + exprFactory.newIdentifier("x"), + exprFactory.newIdentifier("accu"))))) + .build(); + CelAbstractSyntaxTree ast = + cel.compile("int_list == [1, 2] ? int_list.first_elem() == 2 : true").getAst(); + CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); + + CelVerificationResult result = verifier.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + assertThat(result.message()).contains("depends on approximations"); + } + @Test public void isSatisfiable_maskedByBmcButAlwaysFalse_returnsFailed() throws Exception { // The expression is false regardless of what the comprehension evaluates to.