From a6835d2d777ccae70dc717284b0a2453f83bb9cb Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Fri, 13 Nov 2026 10:40:01 -0800 Subject: [PATCH] Select fields from and index optionals, and error on `.?` of undeclared fields PiperOrigin-RevId: 1021151594 --- .../cel/verifier/CelAstToZ3Translator.java | 18 +- .../dev/cel/verifier/CelVerifierZ3Impl.java | 6 +- .../cel/verifier/CelZ3OperatorTranslator.java | 651 +++++++++++------- .../cel/verifier/CelZ3StructTranslator.java | 76 +- .../cel/verifier/CelZ3TranslationContext.java | 8 + .../dev/cel/verifier/CelZ3TypeSystem.java | 5 + .../dev/cel/verifier/TranslatedValue.java | 2 + .../java/dev/cel/verifier/axioms/InAxiom.java | 80 +-- .../cel/verifier/axioms/OptionalAxioms.java | 60 -- .../cel/verifier/CelVerifierZ3ImplTest.java | 194 +++++- 10 files changed, 667 insertions(+), 433 deletions(-) diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index e3211e0f0..25496cc8c 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -14,6 +14,8 @@ package dev.cel.verifier; +import static com.google.common.base.Preconditions.checkArgument; + import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import com.google.common.collect.ImmutableSortedSet; @@ -107,13 +109,6 @@ Set> getInputVariables() { return context.inputVariables(); } - /** - * Returns a Z3 boolean expression asserting that the provided CEL value is a boolean and is true. - */ - BoolExpr isTrue(Expr celValue) { - return ctx.mkAnd(typeSystem.isBool(celValue), (BoolExpr) typeSystem.unwrapBool(celValue)); - } - /** * Binds an identifier name in the symbol table to an already-translated value. Used to bind * reserved policy symbols such as 'rule.result' to the composed policy graph. @@ -446,6 +441,15 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { long exprId = expr.id(); String functionName = call.function(); ImmutableList argsAst = call.args(); + if (functionName.equals(Operator.OPTIONAL_SELECT.getFunction())) { + checkArgument( + !call.target().isPresent() + && argsAst.size() == 2 + && argsAst.get(1).constantOrDefault().getKind() == CelConstant.Kind.STRING_VALUE, + "Malformed AST: operator %s expects an operand and a field name", + Operator.OPTIONAL_SELECT); + return structTranslator.translateSelect(expr, ast); + } List args = 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 767bf4bda..900821e92 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -273,8 +273,8 @@ CelVerificationResult verifyImplication( TranslatedValue assumeTv = translator.translate(assumeAst); TranslatedValue assertTv = translator.translate(assertAst); - BoolExpr assumeCondition = translator.isTrue(assumeTv.z3Expr()); - BoolExpr assertCondition = translator.isTrue(assertTv.z3Expr()); + BoolExpr assumeCondition = translator.getTypeSystem().isTrue(assumeTv.z3Expr()); + BoolExpr assertCondition = translator.getTypeSystem().isTrue(assertTv.z3Expr()); BoolExpr violationCondition = ctx.mkAnd(assumeCondition, ctx.mkNot(assertCondition)); BoolExpr combinedTaint = @@ -305,7 +305,7 @@ private CelVerificationResult checkSatisfiability( CelAstToZ3Translator translator = newTranslator(ctx, /* parameterizeUnknowns= */ false); TranslatedValue tv = translator.translate(ast); - BoolExpr isTrue = translator.isTrue(tv.z3Expr()); + BoolExpr isTrue = translator.getTypeSystem().isTrue(tv.z3Expr()); if (searchForCounterexample) { return search( ctx, diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index 3db4ec809..ab00dd028 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -23,8 +23,10 @@ import com.microsoft.z3.Context; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; +import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; import com.microsoft.z3.SeqExpr; +import com.microsoft.z3.Sort; import dev.cel.common.CelAbstractSyntaxTree; import dev.cel.common.CelFunctionDecl; import dev.cel.common.CelOverloadDecl; @@ -37,6 +39,7 @@ 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 dev.cel.verifier.axioms.CelZ3OverloadResult; @@ -49,6 +52,10 @@ /** Handles mapping CEL Operators to Z3 SMT logic. */ @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types. final class CelZ3OperatorTranslator { + private static final String FUNC_APPROX_EQ = "!approxEq"; + private static final String FUNC_APPROX_IN = "!approxIn"; + private static final MapType DYN_MAP = MapType.create(SimpleType.DYN, SimpleType.DYN); + private final Context ctx; private final CelZ3TypeSystem typeSystem; private final CelZ3TranslationContext context; @@ -142,18 +149,34 @@ Optional translateFunctionCall( Operator op = opOpt.orElse(null); if (op == Operator.IN) { + TranslatedValue lhs = args.get(0); + TranslatedValue list = args.get(1); currentApprox = - 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. - Expr operand = z3Args.get(0); - Expr target = - ctx.mkITE( - typeSystem.isOptional(operand), - typeSystem.getOptionalValue(typeSystem.getOptionalRef(operand)), - operand); - currentApprox = CelZ3Exprs.mkOrFlattened(ctx, currentApprox, context.isTruncatedMap(target)); + CelZ3Exprs.mkOrFlattened(ctx, currentApprox, constrainInWitnessTypes(lhs, list, ast)); + BoolExpr isList = typeSystem.isList(list.z3Expr()); + if (isExact(ListType.create(guaranteedType(lhs, ast)), guaranteedType(list, ast))) { + // IN_LIST matched by terms, but a miss may be past the unroll limit, where elements aren't + // constrained to the element type (e.g. `!(false in bool_list)` with a 6th element of 1). + ArithExpr length = ctx.mkLength(typeSystem.getSeq(typeSystem.getListRef(list.z3Expr()))); + currentApprox = + CelZ3Exprs.mkOrFlattened( + ctx, + currentApprox, + context.recordUnrollLimitApproximation( + CelZ3Exprs.mkAndFlattened( + ctx, + isList, + ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)), + ctx.mkNot(typeSystem.isTrue(currentZ3Result))))); + } else if (extractAstTypeOrDefault(list, ast).kind() != CelKind.MAP) { + // Performance only: maps never take the list overload. + List taints = new ArrayList<>(); + BoolExpr found = listMembership(lhs, list, ast, taints); + currentZ3Result = ctx.mkITE(isList, typeSystem.wrapBool(found), currentZ3Result); + currentApprox = + CelZ3Exprs.mkOrFlattened( + ctx, currentApprox, ctx.mkAnd(isList, CelZ3Exprs.mkOrFlattened(ctx, taints))); + } } return Optional.of( @@ -182,49 +205,17 @@ private BoolExpr attributeApproximation( } /** - * 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 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. + * Constrains keys that {@code InAxiom} may find in a declared map to its key type, and returns + * where the result stays approximate. */ 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). - IntExpr intVal = - (IntExpr) - ctx.mkITE(typeSystem.isInt(lhs), typeSystem.getInt(lhs), typeSystem.getUint(lhs)); - ImmutableList> candidates = - ImmutableList.of( - lhs, - typeSystem.wrapInt(intVal), - typeSystem.wrapUint(intVal), - typeSystem.mkDouble(0.0), - typeSystem.mkDouble(-0.0), - typeSystem.mkInt(0), - typeSystem.mkUint(0)); - CelType elemType = ((ListType) rhsType).elemType(); - SeqExpr seq = typeSystem.getSeq(typeSystem.getListRef(rhs)); - for (Expr cand : candidates) { - BoolExpr structContains = ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(cand)); - context.addConstraint( - ctx.mkImplies( - ctx.mkAnd(typeSystem.isList(rhs), structContains), - typeConstraintGenerator.createTypeConstraintForType(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 probes lhs and its numeric counterparts. + CelType rhsType = guaranteedType(rhsTv, ast); + if (rhsType instanceof MapType) { + // IN_MAP probes lhs and its numeric counterparts, which type constraints unrolled up to the + // limit don't cover (e.g. a string found in a map with int keys). ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(rhs)); for (CelZ3TypeSystem.EqualKey key : typeSystem.equalKeys(lhs)) { context.addConstraint( @@ -238,8 +229,14 @@ private BoolExpr constrainInWitnessTypes( } return context.isTruncatedMap(rhs); } - return CelZ3Exprs.mkOrFlattened( - ctx, context.isTruncatedMap(rhs), mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv)); + // On lists, IN_LIST is exact (lhs has the element type, which compares by terms), or else + // listMembership compares by CEL equality. + return ctx.mkAnd( + typeSystem.isMap(rhs), + CelZ3Exprs.mkOrFlattened( + ctx, + context.isTruncatedMap(rhs), + mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv))); } private BoolExpr mkTypeGuard(Expr arg, CelType expectedType) { @@ -333,9 +330,11 @@ private TranslatedValue translateOperatorCall( case NEGATE: return translateNegate(args.get(0), ast); case EQUALS: - return translateEquality(args.get(0), args.get(1), ast, /* isEquals= */ true); + return translateEquality( + args.get(0), args.get(1), ast, /* isEquals= */ true, /* shallow= */ false); case NOT_EQUALS: - return translateEquality(args.get(0), args.get(1), ast, /* isEquals= */ false); + return translateEquality( + args.get(0), args.get(1), ast, /* isEquals= */ false, /* shallow= */ false); case LESS: case GREATER: case LESS_EQUALS: @@ -351,9 +350,9 @@ private TranslatedValue translateOperatorCall( return TranslatedValue.propagateStrict( ctx, typeSystem, op.getFunction(), typeSystem.mkError(), args); case INDEX: - return translateIndex(args, ast, false); + return translateIndex(args, ast, /* isOptional= */ false); case OPTIONAL_INDEX: - return translateIndex(args, ast, true); + return translateIndex(args, ast, /* isOptional= */ true); case CONDITIONAL: return translateConditional(args, ast); case NOT_STRICTLY_FALSE: @@ -549,7 +548,11 @@ private BoolExpr buildUintRangeExpr(String min, String max, IntExpr symUint) { } private BoolExpr getNumericEquality( - TranslatedValue arg0, TranslatedValue arg1, CelAbstractSyntaxTree ast) { + TranslatedValue arg0, + TranslatedValue arg1, + CelAbstractSyntaxTree ast, + List taints, + boolean approximateIntDouble) { if (arg0.isNumericConstant()) { return getNumericEqualityWithConstant( arg1.z3Expr(), arg0.celExpr().get().constant(), extractAstTypeOrDefault(arg1, ast)); @@ -564,7 +567,7 @@ private BoolExpr getNumericEquality( return getStaticallyKnownNumericEquality(arg0.z3Expr(), type0, arg1.z3Expr()); } - return getDynamicNumericEquality(arg0.z3Expr(), arg1.z3Expr()); + return getDynamicNumericEquality(arg0.z3Expr(), arg1.z3Expr(), taints, approximateIntDouble); } /** Evaluates numeric equality when types are statically known. */ @@ -582,7 +585,8 @@ private BoolExpr getStaticallyKnownNumericEquality( } } - private BoolExpr getDynamicNumericEquality(Expr z3Expr0, Expr z3Expr1) { + private BoolExpr getDynamicNumericEquality( + Expr z3Expr0, Expr z3Expr1, List taints, boolean approximateIntDouble) { BoolExpr isIntOrUint0 = ctx.mkOr(typeSystem.isInt(z3Expr0), typeSystem.isUint(z3Expr0)); BoolExpr isIntOrUint1 = ctx.mkOr(typeSystem.isInt(z3Expr1), typeSystem.isUint(z3Expr1)); BoolExpr bothIntOrUint = ctx.mkAnd(isIntOrUint0, isIntOrUint1); @@ -608,16 +612,27 @@ private BoolExpr getDynamicNumericEquality(Expr z3Expr0, Expr z3Expr1) { BoolExpr isIntOrUintAndDouble = ctx.mkAnd(isIntOrUint0, typeSystem.isDouble(z3Expr1)); BoolExpr isDoubleAndIntOrUint = ctx.mkAnd(typeSystem.isDouble(z3Expr0), isIntOrUint1); - // Likewise fall back to 0.0, which the int/double comparisons never need to define. - FPExpr fpVal0 = guardedDouble(z3Expr0); - FPExpr fpVal1 = guardedDouble(z3Expr1); - - return (BoolExpr) + CelZ3Exprs.SwitchBuilder equality = CelZ3Exprs.SwitchBuilder.newBuilder(ctx) .addCase(bothIntOrUint, ctx.mkEq(val0, val1)) .addCase( bothDouble, - ctx.mkFPEq(typeSystem.getDouble(z3Expr0), typeSystem.getDouble(z3Expr1))) + ctx.mkFPEq(typeSystem.getDouble(z3Expr0), typeSystem.getDouble(z3Expr1))); + if (approximateIntDouble) { + return approximateEqualityWhere( + context.recordApproximation( + "comparisons of ints with doubles read out of lists and maps", + ctx.mkOr(isIntOrUintAndDouble, isDoubleAndIntOrUint)), + z3Expr0, + z3Expr1, + /* exact= */ (BoolExpr) equality.build(ctx.mkFalse()), + taints); + } + // Likewise fall back to 0.0, which the int/double comparisons never need to define. + FPExpr fpVal0 = guardedDouble(z3Expr0); + FPExpr fpVal1 = guardedDouble(z3Expr1); + return (BoolExpr) + equality .addCase(isIntOrUintAndDouble, typeSystem.intEqDouble(val0, fpVal1)) .addCase(isDoubleAndIntOrUint, typeSystem.intEqDouble(val1, fpVal0)) .build(ctx.mkFalse()); @@ -629,152 +644,154 @@ private FPExpr guardedDouble(Expr z3Expr) { typeSystem.isDouble(z3Expr), typeSystem.getDouble(z3Expr), typeSystem.mkFpDouble(0.0)); } - private boolean hasOptionalElements(TranslatedValue arg) { - return arg.isLiteral(ExprKind.Kind.LIST) - && !arg.celExpr().get().list().optionalIndices().isEmpty(); + // A literal with optional elements has as many elements as are present, so no fixed length. + private static boolean isFixedLengthListLiteral(TranslatedValue list) { + return list.isLiteral(ExprKind.Kind.LIST) + && list.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. - */ + // Unrolls list equality element-wise (up to the unroll limit unless either is a literal), adding + // each element equality's approximation to taints: numerically equal elements (e.g. 1 == 1u) + // needn't be equal terms. private BoolExpr unrollListEquality( TranslatedValue listA, TranslatedValue listB, CelAbstractSyntaxTree ast, List taints) { - CelExpr literalListAst = - listA.isLiteral(ExprKind.Kind.LIST) ? listA.celExpr().get() : listB.celExpr().get(); - CelType type0 = guaranteedType(listA); - CelType type1 = guaranteedType(listB); - + boolean isLiteralA = isFixedLengthListLiteral(listA); + boolean isLiteralB = isFixedLengthListLiteral(listB); + boolean isLiteral = isLiteralA || isLiteralB; SeqExpr seq0 = typeSystem.getSeq(typeSystem.getListRef(listA.z3Expr())); SeqExpr seq1 = typeSystem.getSeq(typeSystem.getListRef(listB.z3Expr())); + ArithExpr length = ctx.mkLength(seq0); List equalities = new ArrayList<>(); - equalities.add(ctx.mkEq(ctx.mkLength(seq0), ctx.mkLength(seq1))); - - int size = literalListAst.list().elements().size(); + equalities.add(ctx.mkEq(length, ctx.mkLength(seq1))); + int size = + isLiteral + ? (isLiteralA ? listA : listB).celExpr().get().list().elements().size() + : comprehensionUnrollLimit; + if (!isLiteral) { + equalities.add(approximatePastUnrollLimit(length, listA.z3Expr(), listB.z3Expr(), taints)); + } for (int i = 0; i < size; i++) { - IntExpr idx = ctx.mkInt(i); - Expr elem0 = ctx.mkNth(seq0, idx); - Expr elem1 = ctx.mkNth(seq1, idx); - // A literal's elements, and a concrete declared type's, are already CEL values (performance - // only). - if (!listA.isLiteral(ExprKind.Kind.LIST) && !hasConcreteElements(type0)) { - context.constrainValidValue( - ctx.mkAnd(typeSystem.isList(listA.z3Expr()), ctx.mkLt(idx, ctx.mkLength(seq0))), elem0); - } - if (!listB.isLiteral(ExprKind.Kind.LIST) && !hasConcreteElements(type1)) { - context.constrainValidValue( - ctx.mkAnd(typeSystem.isList(listB.z3Expr()), ctx.mkLt(idx, ctx.mkLength(seq1))), elem1); - } + TranslatedValue elemA = listElement(listA, seq0, i, isLiteralA, ast); + TranslatedValue elemB = listElement(listB, seq1, i, isLiteralB, ast); + TranslatedValue elemEquality = + translateEquality(elemA, elemB, ast, /* isEquals= */ true, /* shallow= */ !isLiteral); + BoolExpr inBounds = ctx.mkLt(ctx.mkInt(i), length); + equalities.add(ctx.mkImplies(inBounds, typeSystem.isTrue(elemEquality.z3Expr()))); + taints.add(ctx.mkAnd(inBounds, elemEquality.isApproximate())); + } + return CelZ3Exprs.mkAndFlattened(ctx, equalities); + } - if (i >= comprehensionUnrollLimit) { - constrainListElement(seq0, idx, elem0, type0); - constrainListElement(seq1, idx, elem1, type1); + // Element i of list, typed by the literal's element if list is a literal. + private TranslatedValue listElement( + TranslatedValue list, SeqExpr seq, int i, boolean isLiteral, CelAbstractSyntaxTree ast) { + Expr elem = ctx.mkNth(seq, ctx.mkInt(i)); + // A literal's elements are already CEL values (performance only). + if (!isLiteral) { + BoolExpr inBounds = ctx.mkLt(ctx.mkInt(i), ctx.mkLength(seq)); + context.constrainValidValue(ctx.mkAnd(typeSystem.isList(list.z3Expr()), inBounds), elem); + CelType listType = guaranteedType(list, ast); + // Type constraints are only unrolled up to the limit. + if (i >= comprehensionUnrollLimit && listType instanceof ListType) { + context.addConstraint( + ctx.mkImplies( + inBounds, + typeConstraintGenerator.createTypeConstraintForType( + elem, ((ListType) listType).elemType()))); } - - TranslatedValue elemA = - TranslatedValue.create(elem0, listA.listElementAt(i), typeSystem, listA.isApproximate()); - TranslatedValue elemB = - TranslatedValue.create(elem1, listB.listElementAt(i), typeSystem, listB.isApproximate()); - - TranslatedValue elemEquality = translateEquality(elemA, elemB, ast, /* isEquals= */ true); - Expr eqZ3 = elemEquality.z3Expr(); - - BoolExpr isBool = typeSystem.isBool(eqZ3); - BoolExpr isTrue = ctx.mkAnd(isBool, (BoolExpr) typeSystem.unwrapBool(eqZ3)); - - equalities.add(isTrue); - taints.add(elemEquality.isApproximate()); } - - return CelZ3Exprs.mkAndFlattened(ctx, equalities); + return TranslatedValue.create( + elem, + isLiteral ? list.listElementAt(i) : Optional.empty(), + typeSystem, + list.isApproximate()); } - // Unrolled over a map literal's keys: the other map has as many keys, each present and equal to - // a literal key, and an equal value for each literal key. + // Unrolled over a map literal's keys, or else mapA's up to the unroll limit: the other map has as + // many keys, and an equal key and value for each. private BoolExpr unrollMapEquality( TranslatedValue mapA, TranslatedValue mapB, CelAbstractSyntaxTree ast, List taints) { + boolean isLiteral = mapA.isLiteral(ExprKind.Kind.MAP) || mapB.isLiteral(ExprKind.Kind.MAP); // Prefer a literal whose values are list or map literals, which compare element-wise. - boolean isLiteralA = - mapA.isLiteral(ExprKind.Kind.MAP) - && !(mapB.isLiteral(ExprKind.Kind.MAP) - && hasContainerLiteralValue(mapB) - && !hasContainerLiteralValue(mapA)); - TranslatedValue literal = isLiteralA ? mapA : mapB; - Expr other = (isLiteralA ? mapB : mapA).z3Expr(); + boolean isMapA = + !mapB.isLiteral(ExprKind.Kind.MAP) + || (mapA.isLiteral(ExprKind.Kind.MAP) && !hasContainerLiteralValue(mapB)); + TranslatedValue map = isMapA ? mapA : mapB; + TranslatedValue otherMap = isMapA ? mapB : mapA; + Expr other = otherMap.z3Expr(); BoolExpr isOtherMap = typeSystem.isMap(other); - Expr literalRef = typeSystem.getMapRef(literal.z3Expr()); - SeqExpr keys = typeSystem.getMapKeys(literalRef); - ArrayExpr values = (ArrayExpr) typeSystem.getMapValues(literalRef); + Expr mapRef = typeSystem.getMapRef(map.z3Expr()); + SeqExpr keys = typeSystem.getMapKeys(mapRef); + ArrayExpr values = (ArrayExpr) typeSystem.getMapValues(mapRef); ArithExpr length = ctx.mkLength(keys); Expr otherRef = typeSystem.getMapRef(other); SeqExpr otherKeys = typeSystem.getMapKeys(otherRef); List equalities = new ArrayList<>(); equalities.add(ctx.mkEq(length, ctx.mkLength(otherKeys))); - ImmutableList entries = literal.celExpr().get().map().entries(); + ImmutableList entries = + isLiteral ? map.celExpr().get().map().entries() : ImmutableList.of(); // The keys are in entry order unless an optional entry is absent (repeated keys are errors). - boolean inEntryOrder = entries.stream().noneMatch(CelExpr.CelMap.Entry::optionalEntry); - for (int i = 0; i < entries.size(); i++) { + boolean inEntryOrder = + isLiteral && entries.stream().noneMatch(CelExpr.CelMap.Entry::optionalEntry); + int size = isLiteral ? entries.size() : comprehensionUnrollLimit; + if (!isLiteral) { + equalities.add(approximatePastUnrollLimit(length, map.z3Expr(), other, taints)); + // A map that isn't a literal or of a declared map type isn't otherwise known to be + // well-formed (distinct keys matching its presence, valid keys and values). + for (TranslatedValue operand : ImmutableList.of(mapA, mapB)) { + if (!(guaranteedType(operand, ast) instanceof MapType)) { + context.addConstraint( + ctx.mkImplies( + typeSystem.isMap(operand.z3Expr()), + typeConstraintGenerator.createTypeConstraintForType(operand.z3Expr(), DYN_MAP))); + } + } + } + for (int i = 0; i < size; i++) { BoolExpr inBounds = ctx.mkLt(ctx.mkInt(i), length); Expr key = ctx.mkNth(keys, ctx.mkInt(i)).simplify(); ImmutableList equalKeys = typeSystem.equalKeys(key); BoolExpr hasKey = typeSystem.hasEqualKey(other, equalKeys); Expr otherValue = typeSystem.valueAtEqualKey(other, equalKeys); context.constrainValidValue(ctx.mkAnd(isOtherMap, inBounds, hasKey), otherValue); - Expr value = ctx.mkSelect(values, key); - CelExpr valueAst = entries.get(i).value(); - boolean isValueLiteral = inEntryOrder && isContainerLiteral(valueAst); TranslatedValue valueEquality = translateEquality( - inEntryOrder - ? TranslatedValue.create(value, valueAst, typeSystem, literal.isApproximate()) - : TranslatedValue.create(value, typeSystem, literal.isApproximate()), - TranslatedValue.create(otherValue, typeSystem, ctx.mkFalse()), + TranslatedValue.create( + ctx.mkSelect(values, key), + inEntryOrder ? Optional.of(entries.get(i).value()) : Optional.empty(), + typeSystem, + map.isApproximate()), + TranslatedValue.create(otherValue, typeSystem, otherMap.isApproximate()), ast, - /* isEquals= */ true); + /* isEquals= */ true, + /* shallow= */ !isLiteral); taints.add(ctx.mkAnd(inBounds, valueEquality.isApproximate())); - if (!isValueLiteral) { - // TODO: Lists and maps compare by their terms unless one is a literal. - taints.add( - context.recordApproximation( - "comparisons of lists or maps nested in maps", - CelZ3Exprs.mkAndFlattened( - ctx, - isOtherMap, - inBounds, - hasKey, - ctx.mkOr( - ctx.mkAnd(typeSystem.isList(value), typeSystem.isList(otherValue)), - ctx.mkAnd(typeSystem.isMap(value), typeSystem.isMap(otherValue)))))); - } - Expr isEqual = valueEquality.z3Expr(); equalities.add( - ctx.mkImplies( - inBounds, - ctx.mkAnd( - hasKey, typeSystem.isBool(isEqual), (BoolExpr) typeSystem.unwrapBool(isEqual)))); + ctx.mkImplies(inBounds, ctx.mkAnd(hasKey, typeSystem.isTrue(valueEquality.z3Expr())))); } - // The other map's keys are exactly the present ones, so each equals a literal key: as many as - // the literal's, which are all present. - ArrayExpr presence = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse()); - for (int j = 0; j < entries.size(); j++) { - Expr otherKey = ctx.mkNth(otherKeys, ctx.mkInt(j)); - presence = - (ArrayExpr) - ctx.mkITE( - ctx.mkLt(ctx.mkInt(j), length), - ctx.mkStore(presence, otherKey, ctx.mkTrue()), - presence); + if (isLiteral) { + // The other map's keys are exactly the present ones, so each equals a literal key: as many + // as the literal's, which are all present. + ArrayExpr presence = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse()); + for (int j = 0; j < entries.size(); j++) { + Expr otherKey = ctx.mkNth(otherKeys, ctx.mkInt(j)); + presence = + (ArrayExpr) + ctx.mkITE( + ctx.mkLt(ctx.mkInt(j), length), + ctx.mkStore(presence, otherKey, ctx.mkTrue()), + presence); + } + equalities.add(ctx.mkEq(typeSystem.getMapPresence(otherRef), presence)); } - equalities.add(ctx.mkEq(typeSystem.getMapPresence(otherRef), presence)); return CelZ3Exprs.mkAndFlattened(ctx, equalities); } @@ -805,6 +822,101 @@ private BoolExpr mapEqualityAtLiteralKeys(TranslatedValue mapA, TranslatedValue return CelZ3Exprs.mkAndFlattened(ctx, equalities); } + // `in` on a list compares each element with lhs by CEL equality, unrolled over a literal's + // elements or else up to the unroll limit, past which a match is approximate. + private BoolExpr listMembership( + TranslatedValue lhs, TranslatedValue list, CelAbstractSyntaxTree ast, List taints) { + boolean isLiteral = isFixedLengthListLiteral(list); + SeqExpr seq = typeSystem.getSeq(typeSystem.getListRef(list.z3Expr())); + ArithExpr length = ctx.mkLength(seq); + List matches = new ArrayList<>(); + int size = isLiteral ? list.celExpr().get().list().elements().size() : comprehensionUnrollLimit; + for (int i = 0; i < size; i++) { + BoolExpr inBounds = ctx.mkLt(ctx.mkInt(i), length); + // The runtime compares each element with lhs, in that order. + TranslatedValue equality = + translateEquality( + listElement(list, seq, i, isLiteral, ast), + lhs, + ast, + /* isEquals= */ true, + /* shallow= */ !isLiteral); + matches.add(ctx.mkAnd(inBounds, typeSystem.isTrue(equality.z3Expr()))); + taints.add(ctx.mkAnd(inBounds, equality.isApproximate())); + } + BoolExpr found = CelZ3Exprs.mkOrFlattened(ctx, matches); + if (isLiteral) { + return found; + } + CelType listType = guaranteedType(list, ast); + CelType elemType = + listType instanceof ListType ? ((ListType) listType).elemType() : SimpleType.DYN; + return approximateWhere( + context.recordUnrollLimitApproximation( + CelZ3Exprs.mkAndFlattened( + ctx, + ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)), + ctx.mkNot(found), + mayEqualElement(lhs.z3Expr(), elemType))), + uninterpreted(FUNC_APPROX_IN, lhs.z3Expr(), list.z3Expr()), + found, + taints); + } + + // Whether lhs may equal an element of elemType: a number only across numeric types, and a list + // only another list (anything else conservatively). + private BoolExpr mayEqualElement(Expr lhs, CelType elemType) { + if (elemType instanceof NullableType) { + return ctx.mkTrue(); + } + if (isNumericType(elemType)) { + return isNumeric(lhs); + } + return elemType.kind() == CelKind.LIST ? typeSystem.isList(lhs) : ctx.mkTrue(); + } + + // Where the recorded approximation holds, the verifier doesn't model the result, so it's the + // given uninterpreted relation there. + private BoolExpr approximateWhere( + BoolExpr approximation, BoolExpr relation, BoolExpr exact, List taints) { + taints.add(approximation); + return (BoolExpr) ctx.mkITE(approximation, relation, exact); + } + + private BoolExpr uninterpreted(String name, Expr z3Expr0, Expr z3Expr1) { + Sort sort = typeSystem.celValueSort(); + FuncDecl relation = + typeSystem.internFuncDecl(name, new Sort[] {sort, sort}, ctx.getBoolSort()); + return (BoolExpr) ctx.mkApp(relation, z3Expr0, z3Expr1); + } + + // Like approximateWhere, for CEL equality, which is symmetric. + private BoolExpr approximateEqualityWhere( + BoolExpr approximation, + Expr z3Expr0, + Expr z3Expr1, + BoolExpr exact, + List taints) { + // Ordered by term id (in either direction) so that x == y and y == x share one application. + // Asserting both orders instead doubles the applications, which made nested comparisons slow. + boolean swap = z3Expr0.getId() > z3Expr1.getId(); + BoolExpr relation = + uninterpreted(FUNC_APPROX_EQ, swap ? z3Expr1 : z3Expr0, swap ? z3Expr0 : z3Expr1); + return approximateWhere(approximation, relation, exact, taints); + } + + // Lists and maps compared up to the unroll limit may differ past it. + private BoolExpr approximatePastUnrollLimit( + ArithExpr length, Expr z3Expr0, Expr z3Expr1, List taints) { + return approximateEqualityWhere( + context.recordUnrollLimitApproximation( + ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit))), + z3Expr0, + z3Expr1, + /* exact= */ ctx.mkTrue(), + taints); + } + private static boolean hasContainerLiteralValue(TranslatedValue map) { return map.celExpr().get().map().entries().stream() .anyMatch(e -> isContainerLiteral(e.value())); @@ -814,19 +926,20 @@ private static boolean isContainerLiteral(CelExpr expr) { return expr.getKind() == ExprKind.Kind.LIST || expr.getKind() == ExprKind.Kind.MAP; } - private void constrainListElement(SeqExpr seq, IntExpr idx, Expr elem, CelType listType) { - if (listType instanceof ListType) { - context.addConstraint( - ctx.mkImplies( - ctx.mkLt(idx, ctx.mkLength(seq)), - context - .typeConstraintGenerator() - .createTypeConstraintForType(elem, ((ListType) listType).elemType()))); - } + private static boolean isContainerLiteral(TranslatedValue val) { + return val.isLiteral(ExprKind.Kind.LIST) || val.isLiteral(ExprKind.Kind.MAP); } + // CEL equality. Values read out of lists and maps that aren't literals (shallow, unless either is + // a list or map literal) compare numbers numerically, but ints and doubles approximately, and + // lists, maps, messages and optionals approximately (performance only). private TranslatedValue translateEquality( - TranslatedValue arg0, TranslatedValue arg1, CelAbstractSyntaxTree ast, boolean isEquals) { + TranslatedValue arg0, + TranslatedValue arg1, + CelAbstractSyntaxTree ast, + boolean isEquals, + boolean shallow) { + boolean isShallow = shallow && !isContainerLiteral(arg0) && !isContainerLiteral(arg1); Expr z3Arg0 = arg0.z3Expr(); Expr z3Arg1 = arg1.z3Expr(); @@ -835,51 +948,69 @@ private TranslatedValue translateEquality( BoolExpr equality; List taints = new ArrayList<>(); - taints.add(mayObserveTruncatedTypeConstraint(ast, arg0, arg1)); + if (!isShallow) { + taints.add(mayObserveTruncatedTypeConstraint(ast, arg0, arg1)); + } if (isNumericType(type0) && isNumericType(type1)) { - equality = getNumericEquality(arg0, arg1, ast); - } else if (type0.kind() == CelKind.LIST - && type1.kind() == CelKind.LIST - && (arg0.isLiteral(ExprKind.Kind.LIST) || arg1.isLiteral(ExprKind.Kind.LIST)) - && !hasOptionalElements(arg0) - && !hasOptionalElements(arg1)) { - equality = unrollListEquality(arg0, arg1, ast, taints); - } else if (arg0.isLiteral(ExprKind.Kind.MAP) || arg1.isLiteral(ExprKind.Kind.MAP)) { - equality = - (BoolExpr) - ctx.mkITE( - ctx.mkAnd(typeSystem.isMap(z3Arg0), typeSystem.isMap(z3Arg1)), - type0.equals(type1) && hasStructuralEquality(type0) - ? mapEqualityAtLiteralKeys(arg0, arg1) - : unrollMapEquality(arg0, arg1, ast, taints), - typeSystem.getStructuralEquality(z3Arg0, z3Arg1)); - } else if (isStaticallyKnown(type0) && isStaticallyKnown(type1)) { - equality = typeSystem.getStructuralEquality(z3Arg0, z3Arg1); + equality = getNumericEquality(arg0, arg1, ast, taints, /* approximateIntDouble= */ false); } else { - boolean canBeNumeric0 = !isStaticallyKnown(type0) || isNumericType(type0); - boolean canBeNumeric1 = !isStaticallyKnown(type1) || isNumericType(type1); - - // Check if one side is an explicit LIST that we can unroll - BoolExpr structuralEq = typeSystem.getStructuralEquality(z3Arg0, z3Arg1); - if ((arg0.isLiteral(ExprKind.Kind.LIST) || arg1.isLiteral(ExprKind.Kind.LIST)) - && !hasOptionalElements(arg0) - && !hasOptionalElements(arg1)) { + BoolExpr bothLists = ctx.mkAnd(typeSystem.isList(z3Arg0), typeSystem.isList(z3Arg1)); + BoolExpr bothMaps = ctx.mkAnd(typeSystem.isMap(z3Arg0), typeSystem.isMap(z3Arg1)); + BoolExpr structuralEq; + if (isShallow) { structuralEq = - (BoolExpr) - ctx.mkITE( - ctx.mkAnd(typeSystem.isList(z3Arg0), typeSystem.isList(z3Arg1)), - unrollListEquality(arg0, arg1, ast, taints), - structuralEq); - } - - if (canBeNumeric0 && canBeNumeric1) { - BoolExpr bothNumeric = ctx.mkAnd(isNumeric(z3Arg0), isNumeric(z3Arg1)); - equality = - (BoolExpr) ctx.mkITE(bothNumeric, getNumericEquality(arg0, arg1, ast), structuralEq); + approximateEqualityWhere( + context.recordApproximation( + "comparisons of lists, maps, messages or optionals read out of lists and maps", + CelZ3Exprs.mkOrFlattened( + ctx, + bothLists, + bothMaps, + ctx.mkAnd(typeSystem.isMessage(z3Arg0), typeSystem.isMessage(z3Arg1)), + ctx.mkAnd(typeSystem.isOptional(z3Arg0), typeSystem.isOptional(z3Arg1)))), + z3Arg0, + z3Arg1, + /* exact= */ ctx.mkEq(z3Arg0, z3Arg1), + taints); } else { - equality = structuralEq; + // Lists and maps compare by CEL equality, unless their guaranteed types make it their + // terms'. + structuralEq = typeSystem.getStructuralEquality(z3Arg0, z3Arg1); + if (!isExact(guaranteedType(arg0, ast), guaranteedType(arg1, ast))) { + if (type0.kind() == CelKind.LIST || type1.kind() == CelKind.LIST) { + structuralEq = + (BoolExpr) + ctx.mkITE(bothLists, unrollListEquality(arg0, arg1, ast, taints), structuralEq); + } else if (type0.kind() == CelKind.MAP || type1.kind() == CelKind.MAP) { + BoolExpr mapEquality = + isExact(type0, type1) + && (arg0.isLiteral(ExprKind.Kind.MAP) || arg1.isLiteral(ExprKind.Kind.MAP)) + ? mapEqualityAtLiteralKeys(arg0, arg1) + : unrollMapEquality(arg0, arg1, ast, taints); + structuralEq = (BoolExpr) ctx.mkITE(bothMaps, mapEquality, structuralEq); + } else if (!isStaticallyKnown(type0) && !isStaticallyKnown(type1)) { + // Performance only: a side with a known type isn't a list or map here. + // TODO: Unless the type checker narrowed it, e.g. `(int_list + + // dyn_var)[0]`. + structuralEq = + approximateEqualityWhere( + context.recordApproximation( + "comparisons of lists or maps typed dyn", ctx.mkOr(bothLists, bothMaps)), + z3Arg0, + z3Arg1, + structuralEq, + taints); + } + } } + equality = + (BoolExpr) + ctx.mkITE( + ctx.mkAnd(isNumeric(z3Arg0), isNumeric(z3Arg1)), + getNumericEquality( + arg0, arg1, ast, taints, /* approximateIntDouble= */ isShallow), + structuralEq); } if (!isEquals) { @@ -894,7 +1025,7 @@ private TranslatedValue translateEquality( } private Expr buildListIndex( - Expr lhsTrans, Expr rhsTrans, BoolExpr typeGuard, boolean isOptional) { + Expr lhsTrans, Expr rhsTrans, BoolExpr typeGuard, BoolExpr returnOptional) { Expr listRef = typeSystem.getListRef(lhsTrans); SeqExpr seq = typeSystem.getSeq(listRef); Expr index = typeSystem.getInt(rhsTrans); @@ -903,37 +1034,43 @@ private Expr buildListIndex( ctx.mkGe((ArithExpr) index, ctx.mkInt(0)), ctx.mkLt((ArithExpr) index, ctx.mkLength(seq))); - return finishIndex(inBounds, ctx.mkNth(seq, (ArithExpr) index), typeGuard, isOptional); + return finishIndex(inBounds, ctx.mkNth(seq, (ArithExpr) index), typeGuard, returnOptional); } private Expr buildMapIndex( - Expr lhsTrans, Expr rhsTrans, BoolExpr typeGuard, boolean isOptional) { + Expr lhsTrans, Expr rhsTrans, BoolExpr typeGuard, BoolExpr returnOptional) { ImmutableList equalKeys = typeSystem.equalKeys(rhsTrans); return finishIndex( typeSystem.hasEqualKey(lhsTrans, equalKeys), typeSystem.valueAtEqualKey(lhsTrans, equalKeys), typeGuard, - isOptional); + returnOptional); } - // Returns val where found, or else an error (or an empty optional). - private Expr finishIndex(BoolExpr found, Expr val, BoolExpr typeGuard, boolean isOptional) { + // Returns val where found, or else an error, as an optional (empty if not found) where + // returnOptional holds. + private Expr finishIndex( + BoolExpr found, Expr val, BoolExpr typeGuard, BoolExpr returnOptional) { context.constrainValidValue(ctx.mkAnd(typeGuard, found), val); - if (isOptional) { - Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), val); - context.addConstraint(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val)); - context.addConstraint(typeSystem.optHasValue(resultOptRef)); - return ctx.mkITE(found, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone()); + Expr plain = ctx.mkITE(found, val, typeSystem.mkError()); + // Performance only: skips building an optional that isn't returned. + if (returnOptional.isFalse()) { + return plain; } - return ctx.mkITE(found, val, typeSystem.mkError()); + Expr optional = ctx.mkITE(found, context.mkOptionalOf(val), typeSystem.mkOptionalNone()); + return returnOptional.isTrue() ? optional : ctx.mkITE(returnOptional, optional, plain); } + /** + * Translates {@code lhs[rhs]}, or {@code lhs[?rhs]} if isOptional. An optional lhs is indexed + * optionally (e.g. {@code optional.of([])[0]} is {@code optional.none()}). + */ private TranslatedValue translateIndex( List args, CelAbstractSyntaxTree ast, boolean isOptional) { TranslatedValue lhs = args.get(0); TranslatedValue rhs = args.get(1); CelType lhsType = extractAstTypeOrDefault(lhs, ast); - boolean isLhsTypeGuaranteed = lhsType.equals(guaranteedType(lhs)); + boolean isLhsTypeGuaranteed = lhsType.equals(guaranteedType(lhs, ast)); Expr lhsTrans = lhs.z3Expr(); Expr rhsTrans = rhs.z3Expr(); @@ -941,8 +1078,10 @@ private TranslatedValue translateIndex( BoolExpr isLhsOpt = ctx.mkFalse(); BoolExpr lhsHasValue = ctx.mkFalse(); BoolExpr shouldEvaluate = ctx.mkTrue(); + BoolExpr returnOptional = isOptional ? ctx.mkTrue() : ctx.mkFalse(); - if (isOptional) { + // Performance only: an lhs of a known type other than optional isn't one. + if (lhsType instanceof OptionalType || !isStaticallyKnown(lhsType)) { isLhsOpt = typeSystem.isOptional(lhsTrans); Expr optRef = typeSystem.getOptionalRef(lhsTrans); lhsHasValue = typeSystem.optHasValue(optRef); @@ -952,21 +1091,24 @@ private TranslatedValue translateIndex( if (lhsType instanceof OptionalType) { lhsType = lhsType.parameters().get(0); + returnOptional = ctx.mkTrue(); + } else if (!isOptional) { + returnOptional = isLhsOpt; } } TranslatedValue element = buildAndConstrainIndex( - lhsTrans, rhsTrans, lhsType, isLhsTypeGuaranteed, shouldEvaluate, isOptional); - Expr actualValue = element.z3Expr(); - - if (isOptional) { - actualValue = - ctx.mkITE( - ctx.mkAnd(isLhsOpt, ctx.mkNot(lhsHasValue)), - typeSystem.mkOptionalNone(), - actualValue); - } + lhsTrans, rhsTrans, lhsType, isLhsTypeGuaranteed, shouldEvaluate, returnOptional); + // An empty optional gives an empty optional, unless no overload takes the index (e.g. a string + // indexing an optional list). + BoolExpr takesIndex = + lhsType.kind() == CelKind.LIST ? typeSystem.isInt(rhsTrans) : ctx.mkTrue(); + Expr actualValue = + ctx.mkITE( + CelZ3Exprs.mkAndFlattened(ctx, isLhsOpt, ctx.mkNot(lhsHasValue), takesIndex), + typeSystem.mkOptionalNone(), + element.z3Expr()); String opName = isOptional ? Operator.OPTIONAL_INDEX.getFunction() : Operator.INDEX.getFunction(); @@ -997,7 +1139,7 @@ private TranslatedValue buildAndConstrainIndex( CelType lhsType, boolean isLhsTypeGuaranteed, BoolExpr shouldEvaluate, - boolean isOptional) { + BoolExpr returnOptional) { CelType expectedElemType = null; if (lhsType.kind() == CelKind.LIST) { expectedElemType = ((ListType) lhsType).elemType(); @@ -1008,18 +1150,19 @@ private TranslatedValue buildAndConstrainIndex( if (expectedElemType != null) { Expr actualValue; if (lhsType.kind() == CelKind.MAP) { - actualValue = buildMapIndex(lhsTrans, rhsTrans, shouldEvaluate, isOptional); + actualValue = buildMapIndex(lhsTrans, rhsTrans, shouldEvaluate, returnOptional); } else { BoolExpr isIntIndex = typeSystem.isInt(rhsTrans); actualValue = ctx.mkITE( isIntIndex, buildListIndex( - lhsTrans, rhsTrans, ctx.mkAnd(shouldEvaluate, isIntIndex), isOptional), + lhsTrans, rhsTrans, ctx.mkAnd(shouldEvaluate, isIntIndex), returnOptional), typeSystem.mkError()); } - CelType finalType = isOptional ? OptionalType.create(expectedElemType) : expectedElemType; + CelType finalType = + returnOptional.isTrue() ? OptionalType.create(expectedElemType) : expectedElemType; BoolExpr isDefined = ctx.mkAnd(shouldEvaluate, ctx.mkNot(typeSystem.isError(actualValue))); BoolExpr typeConstraint = typeConstraintGenerator.createTypeConstraintForType(actualValue, finalType); @@ -1042,8 +1185,8 @@ private TranslatedValue buildAndConstrainIndex( return TranslatedValue.create( CelZ3Exprs.SwitchBuilder.newBuilder(ctx) - .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, isOptional)) - .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, isOptional)) + .addCase(isListGuard, buildListIndex(lhsTrans, rhsTrans, isListGuard, returnOptional)) + .addCase(isMapGuard, buildMapIndex(lhsTrans, rhsTrans, isMapGuard, returnOptional)) .build(typeSystem.mkError()), typeSystem, ctx.mkFalse()); @@ -1104,13 +1247,15 @@ private static CelType extractAstTypeOrDefault(TranslatedValue val, CelAbstractS } /** - * 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. + * Returns the type that {@code val} is guaranteed to conform to at runtime: a constant's, 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 context.guaranteedType(val.z3Expr()); + private CelType guaranteedType(TranslatedValue val, CelAbstractSyntaxTree ast) { + return val.isLiteral(ExprKind.Kind.CONSTANT) + ? extractAstTypeOrDefault(val, ast) + : context.guaranteedType(val.z3Expr()); } /** @@ -1134,6 +1279,10 @@ private static boolean isConcrete(CelType type) { && type.parameters().stream().allMatch(CelZ3OperatorTranslator::isConcrete); } + private static boolean isExact(CelType type0, CelType type1) { + return type0.equals(type1) && hasStructuralEquality(type0); + } + /** Whether values of {@code type} are equal exactly when their terms are. */ private static boolean hasStructuralEquality(CelType type) { switch (type.kind()) { diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java index 11cc36191..1db897f8a 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java @@ -26,6 +26,7 @@ import com.microsoft.z3.SeqExpr; import dev.cel.common.CelAbstractSyntaxTree; import dev.cel.common.ast.CelExpr; +import dev.cel.common.ast.CelExpr.ExprKind; import dev.cel.common.internal.ProtoTimeUtils; import dev.cel.common.types.CelKind; import dev.cel.common.types.CelType; @@ -536,13 +537,41 @@ private FieldAccess getMsgAccess(Expr operand, String field, BoolExpr typeGua return new FieldAccess(presence, value); } + /** + * Translates {@code e.f}, {@code has(e.f)} or {@code e.?f} (an optional of {@code e.f} if {@code + * has(e.f)}, else empty). + */ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) { - CelExpr.CelSelect select = celExpr.select(); + boolean isOptional = celExpr.getKind() == ExprKind.Kind.CALL; + CelExpr operandExpr = isOptional ? celExpr.call().args().get(0) : celExpr.select().operand(); + String field = + isOptional + ? celExpr.call().args().get(1).constant().stringValue() + : celExpr.select().field(); + boolean testOnly = !isOptional && celExpr.select().testOnly(); long exprId = celExpr.id(); - TranslatedValue operandTv = translateExpr(select.operand(), ast); + TranslatedValue operandTv = translateExpr(operandExpr, ast); Expr operand = operandTv.z3Expr(); - String field = select.field(); - CelType operandType = extractAstTypeOrDefault(ast, select.operand().id()); + CelType operandType = extractAstTypeOrDefault(ast, operandExpr.id()); + // Selecting from an optional selects from its value optionally (e.g. `optional.of({}).a` is + // `optional.none()`). Performance only: an operand of a known type other than optional isn't. + boolean mayBeOptional = + operandType instanceof OptionalType + || !CelZ3OperatorTranslator.isStaticallyKnown(operandType); + BoolExpr isOptionalOperand = ctx.mkFalse(); + BoolExpr hasValue = ctx.mkFalse(); + BoolExpr shouldEvaluate = ctx.mkTrue(); + if (mayBeOptional) { + Expr optRef = typeSystem.getOptionalRef(operand); + isOptionalOperand = typeSystem.isOptional(operand); + hasValue = typeSystem.optHasValue(optRef); + shouldEvaluate = (BoolExpr) ctx.mkITE(isOptionalOperand, hasValue, ctx.mkTrue()); + operand = ctx.mkITE(isOptionalOperand, typeSystem.getOptionalValue(optRef), operand); + } + if (operandType instanceof OptionalType) { + // Performance only: reads the value by its static type. + operandType = operandType.parameters().get(0); + } Expr presenceResult; Expr valueResult; @@ -550,11 +579,11 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) { BoolExpr presenceError = ctx.mkFalse(); if (operandType instanceof MapType) { - FieldAccess mapAcc = getMapAccess(operand, field, ctx.mkTrue()); + FieldAccess mapAcc = getMapAccess(operand, field, shouldEvaluate); presenceResult = mapAcc.presence; valueResult = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError()); } else if (operandType.kind() == CelKind.STRUCT) { - FieldAccess msgAcc = getMsgAccess(operand, field, ctx.mkTrue()); + FieldAccess msgAcc = getMsgAccess(operand, field, shouldEvaluate); presenceResult = msgAcc.presence; Expr defaultVal = getDefaultValueForType(extractAstTypeOrDefault(ast, exprId)); valueResult = ctx.mkITE(msgAcc.presence, msgAcc.value, defaultVal); @@ -563,8 +592,8 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) { BoolExpr isMap = typeSystem.isMap(operand); BoolExpr isMessage = typeSystem.isMessage(operand); - FieldAccess mapAcc = getMapAccess(operand, field, isMap); - FieldAccess msgAcc = getMsgAccess(operand, field, isMessage); + FieldAccess mapAcc = getMapAccess(operand, field, ctx.mkAnd(shouldEvaluate, isMap)); + FieldAccess msgAcc = getMsgAccess(operand, field, ctx.mkAnd(shouldEvaluate, isMessage)); presenceResult = CelZ3Exprs.SwitchBuilder.newBuilder(ctx) @@ -590,13 +619,13 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) { msgRead.addCase(isType, typeSystem.mkError()); continue; } - if (select.testOnly()) { + if (testOnly) { continue; } CelType fieldType = declared.get().type(); context.addConstraint( ctx.mkImplies( - ctx.mkAnd(isMessage, isType, msgAcc.presence), + ctx.mkAnd(shouldEvaluate, isMessage, isType, msgAcc.presence), typeConstraintGenerator.createTypeConstraintForType(msgAcc.value, fieldType))); msgRead.addCase( isType, ctx.mkITE(msgAcc.presence, msgAcc.value, getDefaultValueForType(fieldType))); @@ -605,7 +634,10 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) { unmodeledMessage = context.recordApproximation( "messages of types the type provider doesn't declare", - ctx.mkAnd(isMessage, ctx.mkNot(CelZ3Exprs.mkOrFlattened(ctx, isModeledType)))); + ctx.mkAnd( + shouldEvaluate, + isMessage, + ctx.mkNot(CelZ3Exprs.mkOrFlattened(ctx, isModeledType)))); Expr mapRead = ctx.mkITE(mapAcc.presence, mapAcc.value, typeSystem.mkError()); // Testing an undeclared field, or a field of something other than a map or message, errors. presenceError = @@ -622,10 +654,27 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) { .build(typeSystem.mkError()); } + // has(e.f), else e.f, or for e.?f and an optional e, an optional of e.f if has(e.f). Expr fieldAccess = - select.testOnly() + testOnly ? typeSystem.withRuntimeError(typeSystem.wrapBool(presenceResult), presenceError) : valueResult; + Expr chained = fieldAccess; + if (!testOnly && (isOptional || mayBeOptional)) { + chained = + ctx.mkITE( + presenceError, + typeSystem.mkError(), + ctx.mkITE( + (BoolExpr) presenceResult, + context.mkOptionalOf(valueResult), + typeSystem.mkOptionalNone())); + fieldAccess = isOptional ? chained : valueResult; + } + if (mayBeOptional) { + Expr empty = testOnly ? typeSystem.mkBool(false) : typeSystem.mkOptionalNone(); + fieldAccess = ctx.mkITE(isOptionalOperand, ctx.mkITE(hasValue, chained, empty), fieldAccess); + } context.addConstraint(typeConstraintGenerator.createTypeConstraint(fieldAccess, exprId, ast)); @@ -636,7 +685,8 @@ TranslatedValue translateSelect(CelExpr celExpr, CelAbstractSyntaxTree ast) { return operandType.kind() == CelKind.STRUCT ? result : result.withApproximation( - CelZ3Exprs.mkOrFlattened(ctx, context.isTruncatedMap(operand), unmodeledMessage)); + CelZ3Exprs.mkOrFlattened( + ctx, ctx.mkAnd(shouldEvaluate, context.isTruncatedMap(operand)), unmodeledMessage)); } private static CelType extractAstTypeOrDefault(CelAbstractSyntaxTree ast, long id) { diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java index fb6f7270d..05e6e307a 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java @@ -80,6 +80,14 @@ void constrainValidValue(BoolExpr guard, Expr value) { addConstraint(ctx.mkImplies(guard, typeSystem.isValidValue(value))); } + /** Returns an optional holding {@code value}. */ + Expr mkOptionalOf(Expr value) { + Expr optRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), value); + addConstraint(ctx.mkEq(typeSystem.getOptionalValue(optRef), value)); + addConstraint(typeSystem.optHasValue(optRef)); + return typeSystem.mkOptionalOf(optRef); + } + void addInputVariable(Expr variable, CelType declaredType) { inputVariableTypes.put(variable, declaredType); } diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index 1a9d262d0..f5fd569cc 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -360,6 +360,11 @@ public FPExpr mkFpDouble(double val) { return ctx.mkFP(val, ctx.mkFPSortDouble()); } + /** Whether the given CelValue is the bool true. */ + BoolExpr isTrue(Expr celValue) { + return ctx.mkAnd(isBool(celValue), (BoolExpr) unwrapBool(celValue)); + } + /** Checks if the given CelValue is a double. */ public BoolExpr isDouble(Expr val) { return (BoolExpr) ctx.mkApp(doubleCons.getTesterDecl(), val); diff --git a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java index 7ea52abc8..201739f66 100644 --- a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java +++ b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java @@ -199,6 +199,8 @@ private static String extractOpName(CelExpr expr) { switch (expr.exprKind().getKind()) { case SELECT: return "select_" + expr.select().field() + "_" + expr.select().testOnly(); + case CALL: // e.?f + return "optional_select_" + expr.call().args().get(1).constant().stringValue(); case STRUCT: StringBuilder structSb = new StringBuilder("struct_").append(expr.struct().messageName()); for (CelExpr.CelStruct.Entry entry : expr.struct().entries()) { diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/InAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/InAxiom.java index f24552dfe..5a745e39c 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/InAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/InAxiom.java @@ -14,88 +14,26 @@ package dev.cel.verifier.axioms; -import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Expr; -import com.microsoft.z3.FPExpr; -import com.microsoft.z3.IntExpr; -import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import java.util.Optional; /** Axiomatization for CEL's in operator/function (list and map overloads). */ @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types. -public final class InAxiom { +final class InAxiom { static final CelZ3FunctionAxiom INSTANCE = CelZ3FunctionAxiom.newBuilder(StandardFunction.IN.functionDecl()) + // Matches by terms, which is CEL equality when lhs has the list's element type and that + // type compares by terms; the operator translator compares other lists by CEL equality. .addBinaryOverloadTranslator( StandardFunction.Overload.InternalOperator.IN_LIST.celOverloadDecl(), - (ctx, typeSystem, constraintSink, lhsTrans, rhsTrans) -> { - Expr listRef = typeSystem.getListRef(rhsTrans); - SeqExpr seq = typeSystem.getSeq(listRef); - - BoolExpr structContains = ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(lhsTrans)); - - BoolExpr isDouble = typeSystem.isDouble(lhsTrans); - FPExpr fpVal = (FPExpr) typeSystem.getDouble(lhsTrans); - - BoolExpr isNaN = ctx.mkFPIsNaN(fpVal); - BoolExpr isDoubleZero = ctx.mkFPIsZero(fpVal); - - Expr posZeroCel = typeSystem.wrapDouble(typeSystem.mkFpDouble(0.0)); - Expr negZeroCel = typeSystem.wrapDouble(typeSystem.mkFpDouble(-0.0)); - Expr intZeroCel = typeSystem.wrapInt(ctx.mkInt(0)); - Expr uintZeroCel = typeSystem.wrapUint(ctx.mkInt(0)); - - // CEL follows IEEE-754 where 0.0 == -0.0, and cross-type equality means they also - // equal int 0 and uint 0. - BoolExpr containsAnyZero = - ctx.mkOr( - ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(posZeroCel)), - ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(negZeroCel)), - ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(intZeroCel)), - ctx.mkContains((Expr) seq, (Expr) ctx.mkUnit(uintZeroCel))); - - // CEL follows IEEE-754 where NaN != NaN. - BoolExpr doubleInList = - (BoolExpr) - ctx.mkITE( - isNaN, - ctx.mkFalse(), - ctx.mkITE(isDoubleZero, containsAnyZero, structContains)); - - BoolExpr isInt = typeSystem.isInt(lhsTrans); - BoolExpr isUint = typeSystem.isUint(lhsTrans); - BoolExpr isIntOrUint = ctx.mkOr(isInt, isUint); - - IntExpr intVal = - (IntExpr) - ctx.mkITE(isInt, typeSystem.getInt(lhsTrans), typeSystem.getUint(lhsTrans)); - BoolExpr isIntOrUintZero = ctx.mkEq(intVal, ctx.mkInt(0)); - - BoolExpr containsIntOrUint = - ctx.mkOr( - ctx.mkAnd( - ctx.mkNot(typeSystem.checkIntOverflow(intVal)), - ctx.mkContains( - (Expr) seq, (Expr) ctx.mkUnit(typeSystem.wrapInt(intVal)))), - ctx.mkAnd( - ctx.mkNot(typeSystem.checkUintOverflow(intVal)), - ctx.mkContains( - (Expr) seq, (Expr) ctx.mkUnit(typeSystem.wrapUint(intVal))))); - - BoolExpr intOrUintInList = - (BoolExpr) ctx.mkITE(isIntOrUintZero, containsAnyZero, containsIntOrUint); - - BoolExpr isMatch = - (BoolExpr) - ctx.mkITE( - isDouble, - doubleInList, - ctx.mkITE(isIntOrUint, intOrUintInList, structContains)); - - return Optional.of(typeSystem.wrapBool(isMatch)); - }) + (ctx, typeSystem, constraintSink, lhsTrans, rhsTrans) -> + Optional.of( + typeSystem.wrapBool( + ctx.mkContains( + (Expr) typeSystem.getSeq(typeSystem.getListRef(rhsTrans)), + (Expr) ctx.mkUnit(lhsTrans))))) .addBinaryOverloadTranslator( StandardFunction.Overload.InternalOperator.IN_MAP.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhsTrans, rhsTrans) -> 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 dd983d36b..748b6f6ca 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java @@ -20,12 +20,10 @@ import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_OF_NON_ZERO_VALUE; import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_OR; import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_OR_VALUE; -import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_SELECT; import static dev.cel.extensions.CelOptionalLibrary.OptionalDeclaration.OPTIONAL_VALUE; import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableList; -import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; import com.microsoft.z3.Expr; @@ -33,7 +31,6 @@ 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; @@ -88,63 +85,6 @@ final class OptionalAxioms { (ctx, ts, sink, val, other) -> { Expr optRef = ts.getOptionalRef(val); return Optional.of(ctx.mkITE(ts.optHasValue(optRef), val, other)); - }), - createBinaryAxiom( - OPTIONAL_SELECT, - (ctx, ts, sink, operand, field) -> { - Expr optRef = ts.getOptionalRef(operand); - BoolExpr isOpt = ts.isOptional(operand); - BoolExpr hasValue = ts.optHasValue(optRef); - Expr actualOperand = ctx.mkITE(isOpt, ts.getOptionalValue(optRef), operand); - - BoolExpr isMap = ts.isMap(actualOperand); - BoolExpr isMsg = ts.isMessage(actualOperand); - BoolExpr isValidTarget = ctx.mkOr(isMap, isMsg); - - Expr msgFieldZ3Str = ts.getString(field); - Expr mapFieldCelVal = field; - - Expr msgRef = ts.getMessageRef(actualOperand); - Expr mapRef = ts.getMapRef(actualOperand); - - Expr presence = - CelZ3Exprs.SwitchBuilder.newBuilder(ctx) - .addCase( - isMsg, - ctx.mkSelect((ArrayExpr) ts.getMsgPresence(msgRef), msgFieldZ3Str)) - .addCase( - isMap, - ctx.mkSelect((ArrayExpr) ts.getMapPresence(mapRef), mapFieldCelVal)) - .build(ctx.mkFalse()); - - Expr value = - CelZ3Exprs.SwitchBuilder.newBuilder(ctx) - .addCase( - isMsg, ctx.mkSelect((ArrayExpr) ts.getMsgValues(msgRef), msgFieldZ3Str)) - .addCase( - isMap, - ctx.mkSelect((ArrayExpr) ts.getMapValues(mapRef), mapFieldCelVal)) - .build(ts.mkError()); - - BoolExpr valNotError = ctx.mkNot(ctx.mkEq(value, ts.mkError())); - BoolExpr shouldEvaluate = (BoolExpr) ctx.mkITE(isOpt, hasValue, ctx.mkTrue()); - sink.accept( - ctx.mkImplies( - CelZ3Exprs.mkAndFlattened( - ctx, shouldEvaluate, isValidTarget, (BoolExpr) presence), - valNotError)); - - Expr resultOptRef = ctx.mkApp(ts.optionalOfRefFunc(), value); - sink.accept(ctx.mkEq(ts.getOptionalValue(resultOptRef), value)); - sink.accept(ts.optHasValue(resultOptRef)); - - Expr optionalResult = - ctx.mkITE( - (BoolExpr) presence, ts.mkOptionalOf(resultOptRef), ts.mkOptionalNone()); - - Expr result = ctx.mkITE(isValidTarget, optionalResult, ts.mkError()); - return Optional.of( - ctx.mkITE(ctx.mkAnd(isOpt, ctx.mkNot(hasValue)), ts.mkOptionalNone(), result)); })); private static BoolExpr isZeroValue(Context ctx, CelZ3TypeSystem ts, Expr val) { diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 8ab5fa1cf..d8eeaa921 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -118,6 +118,9 @@ public final class CelVerifierZ3ImplTest { .addVar("opt_var", OptionalType.create(SimpleType.INT)) .addVar("opt_dyn_var", OptionalType.create(SimpleType.DYN)) .addVar("nullable_int", NullableType.create(SimpleType.INT)) + .addVar("nullable_int_list", ListType.create(NullableType.create(SimpleType.INT))) + .addVar("bool_list", ListType.create(SimpleType.BOOL)) + .addVar("bool_list_2", ListType.create(SimpleType.BOOL)) .addVar("string_int_map", MapType.create(SimpleType.STRING, SimpleType.INT)) .addVar("bytes_val", SimpleType.BYTES) .addVar( @@ -177,8 +180,6 @@ private enum IsSatisfiableTestCase { "dyn_var == TestAllTypes{} && dyn_var.single_string == ''", "dyn_var = "), ANY_NUMERIC_EQUALITY( "test_all_types.single_any == 1 && 1.0 == test_all_types.single_any", "test_all_types = "), - DYNAMIC_VAR_NOT_IN_LIST( - "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:"), @@ -597,7 +598,18 @@ private enum ApproximationSourceTestCase { CUSTOM_COMPREHENSION_LOOP_CONDITION( "int_list == [1, 2] && int_list.first_elem() == 1", "comprehensions with a loop condition"), OPTIONAL_SELECT_WITH_AXIOM( - "(false && string_int_map.?k.hasValue()) || int(string_var) == 5", "calls to `int`"); + "(false && string_int_map.?k.hasValue()) || int(string_var) == 5", "calls to `int`"), + INT_DOUBLE_IN_LISTS( + "size(dyn_list) == 1 && size(dyn_var) == 1 && dyn_list[0] + 1 == 2" + + " && dyn_var[0] + 1.0 == 2.0 && dyn_list == dyn_var", + "comparisons of ints with doubles read out of lists and maps"), + LISTS_IN_LISTS( + "size(dyn_list) == 1 && size(dyn_var) == 1 && type(dyn_list[0]) == list" + + " && dyn_list == dyn_var", + "comparisons of lists, maps, messages or optionals read out of lists and maps"), + DYN_LIST_VARIABLES( + "size(dyn_var) == 1 && dyn_var[0] == 1 && dyn_var == dyn_var2", + "comparisons of lists or maps typed dyn"); private final String expr; private final String expectedSources; @@ -677,6 +689,19 @@ public void isSatisfiable_approximate_returnsPotentialSatisfyingInput() throws E } private enum IsSatisfiableInconclusiveTestCase { + // A list of nullable ints may hold null past the unroll limit. + NULL_IN_NULLABLE_LIST_PAST_UNROLL_LIMIT( + "size(nullable_int_list) == 6 && nullable_int_list[0] != null && nullable_int_list[1] !=" + + " null && nullable_int_list[2] != null && nullable_int_list[3] != null" + + " && nullable_int_list[4] != null && null in nullable_int_list"), + // `in` on a list that isn't a literal is approximate past the unroll limit. + DYNAMIC_VAR_NOT_IN_LIST("dyn_var == 1.5 && !(dyn_var in dyn_list) && size(dyn_list) == 6"), + // `in` compares an int with doubles read out of lists that aren't literals approximately. + DYN_IN_LIST_OUT_OF_RANGE_CROSS_TYPE_CANDIDATE( + "size(dyn_var + []) == 1" + + " && ((-1 in dyn_var && dyn_var != ([-1] + []))" + + " || (18446744073709551615u in dyn_var" + + " && dyn_var != ([18446744073709551615u] + [])))"), // Well-known types are never messages, and other message types may have the field. DYN_MESSAGE_FIELD_OF_UNKNOWN_TYPE("type(dyn_var) != map && dyn_var.type_url == ''"), MASKED_BY_BMC("int_list == [1, 2, 3, 4, 5, 6] ? int_list.exists(x, x == 42) : false"), @@ -807,7 +832,8 @@ private enum IsUnsatisfiableTestCase { TYPE_CONVERSION_UNSATISFIABLE_INT_TO_DOUBLE_NAN("double(x) != double(x)"), EMPTY_MAP_SIZE_NOT_ZERO("size({}) != 0"), // An int key never finds a double key of a host map. - INT_KEY_NOT_FOUND_BUT_LITERAL_FOUND("x == 1 && !(x in dyn_var) && 1 in dyn_var"), + INT_KEY_NOT_FOUND_BUT_LITERAL_FOUND( + "type(dyn_var) == map && x == 1 && !(x in dyn_var) && 1 in dyn_var"), TIMESTAMP_INEQUALITY_CONTRADICTION( "timestamp('2023-01-01T00:00:00Z') != timestamp('2023-01-01T00:00:00Z')"), TYPE_TIMESTAMP_NOT_INT("type(timestamp('1970-01-01T00:00:00Z')) == int"), @@ -892,11 +918,6 @@ private enum IsUnsatisfiableTestCase { "d == -9223372036854777856.0 && dyn_var == [d] && !(d in dyn_var)"), DYN_LIST_EQUALITY_OUT_OF_RANGE_RIGHT_ELEMENT( "d == -9223372036854777856.0 && [d] == dyn_var && !(d in dyn_var)"), - DYN_IN_LIST_OUT_OF_RANGE_CROSS_TYPE_CANDIDATE( - "size(dyn_var + []) == 1" - + " && ((-1 in dyn_var && dyn_var != ([-1] + []))" - + " || (18446744073709551615u in dyn_var" - + " && dyn_var != ([18446744073709551615u] + [])))"), DYN_OPTIONAL_OR_VALUE_OUT_OF_RANGE( "type(dyn_var.orValue(1u)) == uint && dyn_var.orValue(1u) < 0u"), ANY_NEGATIVE_UINT("type(test_all_types.single_any) == uint && test_all_types.single_any < 0u"), @@ -968,6 +989,9 @@ private enum IsAlwaysTrueTestCase { CYCLIC_MACRO_SHADOWING_SAFETY("[1].all(x, [x].all(x, x == 1))"), TAUTOLOGY("x > 5 || x <= 5"), LIST_VARIABLE_CONSTRAINED("1 in int_list || !(1 in int_list)"), + // Ints are found in int lists by their terms, past the unroll limit too. + INT_IN_INT_LIST_PAST_UNROLL_LIMIT( + "size(int_list) == 6 && int_list[5] == x ? x in int_list : true"), LIST_CONCATENATION("[1, 2, 3] == [1] + [2] + [3]"), LIST_CONTAINS_LIST("[1] in [[1]]"), UINT_MIN_RANGE("u >= 0u"), @@ -1065,7 +1089,10 @@ private enum IsAlwaysTrueTestCase { STATIC_NUMERIC_EQUALITY_INT("x == x"), STATIC_NUMERIC_EQUALITY_UINT("u == u"), DYNAMIC_MAP_EQUALITY("string_int_map == {'a': 1} || string_int_map != {'a': 1}"), - DYNAMIC_LIST_VARIABLE_EQUALITY("dyn_list == dyn_list"), + // A dyn map equal to a declared map has as many distinct keys. + DYN_MAP_EQUAL_TO_DECLARED_MAP_KEYS( + "string_int_map == {'a': 1, 'b': 2} && dyn_var == string_int_map" + + " ? 'b' in dyn_var && !('c' in dyn_var) : true"), DYNAMIC_LIST_COMPREHENSION_ALL_SHORT_CIRCUITS_ERROR( "dyn_list == [false, 1] ? (dyn_list.all(x, x) == false) : true"), DYNAMIC_LIST_COMPREHENSION_EXISTS_SHORT_CIRCUITS_ERROR( @@ -1145,6 +1172,20 @@ private enum IsAlwaysTrueTestCase { TYPED_MAP_EQ_LITERAL( "'a' in string_int_map && size(string_int_map) == 1 && string_int_map['a'] == 1 ?" + " string_int_map == {'a': 1} : true"), + // Lists and maps that aren't literals compare by CEL equality, and so does `in` on lists. + MAP_VARIABLES_EQ_ACROSS_NUMERIC_KEYS( + "dyn_map == {1: 'a'} && dyn_var == {1u: 'a'} ? dyn_map == dyn_var : true"), + IN_LIST_ACROSS_NUMERIC_ELEMENTS( + "dyn(1) in [dyn(1.0)] && dyn(1.0) in [dyn(1)] && dyn(1u) in [dyn(1.0)]"), + IN_LIST_ACROSS_NUMERIC_NESTED_ELEMENTS("[1] in [dyn([1.0])]"), + IN_LIST_AT_UNROLL_LIMIT( + "!(2 in [0, 0, 0, 0] + [dyn(1.0)]) && !(2 in [0, 0, 0, 0, 0, dyn(1.0)])"), + DYN_CONTAINER_EQUALITY_SYMMETRIC("(dyn(int_list) == dyn_var) == (dyn_var == dyn(int_list))"), + LIST_VARIABLES_EQ_WITHIN_LENGTH( + "size(int_list) == 1 && size(int_list_2) == 1 && int_list[0] == int_list_2[0] ?" + + " int_list + [] == int_list_2 : true"), + MAP_VARIABLES_NEQ_SIZE( + "dyn_map == {1: 'a'} && dyn_var == {1: 'a', 2: 'b'} ? dyn_map != dyn_var : true"), // Whether an empty list(dyn) field is set is the same in every literal. STRUCT_EMPTY_LIST_DYN_FIELD_PRESENCE_CONSISTENT( "has(TestAllTypes{list_value: []}.list_value)" @@ -1754,6 +1795,23 @@ private enum UnconditionalErrorTestCase { "dyn(TestAllTypes.NestedMessage{}).single_int64 == 0" + " || dyn(TestAllTypes.NestedMessage{}).single_int64 != 0"), MAP_MISSING_KEY("{'a': 1}['b'] == 0 || !({'a': 1}['b'] == 0)"), + OPTIONAL_SELECT_UNDECLARED_FIELD_OF_DYN_MESSAGE( + "dyn(TestAllTypes{}).?unknown_field.hasValue()" + + " || !dyn(TestAllTypes{}).?unknown_field.hasValue()"), + OPTIONAL_CHAINING_SELECT_UNDECLARED_FIELD( + "optional.of(dyn(TestAllTypes{})).unknown_field.hasValue()" + + " || !optional.of(dyn(TestAllTypes{})).unknown_field.hasValue()"), + // No overload indexes a list with a string, even an empty optional list. + OPTIONAL_LIST_INDEXED_BY_STRING( + "TestAllTypes{}.?repeated_int64[dyn('a')].hasValue()" + + " || !TestAllTypes{}.?repeated_int64[dyn('a')].hasValue()"), + OPTIONAL_LIST_OPTIONALLY_INDEXED_BY_STRING( + "TestAllTypes{}.?repeated_int64[?dyn('a')].hasValue()" + + " || !TestAllTypes{}.?repeated_int64[?dyn('a')].hasValue()"), + // A present optional's value must be a map or message to select from. + OPTIONAL_CHAINING_SELECT_FROM_NULL( + "{'null_key': dyn(null)}.?null_key.invalid.hasValue()" + + " || !{'null_key': dyn(null)}.?null_key.invalid.hasValue()"), COLLECTION_ERROR("{'a': 1 / 0} == {'a': 1 / 0}"), LIST_ERROR("[1 / 0] == [1 / 0]"), STRICT_LITERAL_ERROR("{'a': 1/0}.exists(k, k == 'a') == {'a': 1/0}.exists(k, k == 'a')"), @@ -1830,7 +1888,12 @@ private enum MalformedAstTestCase { Operator.LESS, ImmutableList.of( CelExpr.newBuilder().setId(2).setConstant(CelConstant.ofValue(1L)).build()), - "expects 2 arguments, got 1"); + "expects 2 arguments, got 1"), + OPTIONAL_SELECT( + Operator.OPTIONAL_SELECT, + ImmutableList.of( + CelExpr.newBuilder().setId(2).setConstant(CelConstant.ofValue(1L)).build()), + "expects an operand and a field name"); final Operator operator; final ImmutableList args; @@ -1881,6 +1944,17 @@ public void verifyEquivalence_infinityConstants_notEquivalent() throws Exception } private enum IsAlwaysTrueViolationTestCase { + // `[NaN]` differs from itself. + DYNAMIC_LIST_VARIABLE_EQUALITY("dyn_list == dyn_list", "dyn_list = \\[double\\(\"NaN\"\\)\\]"), + DYNAMIC_MAP_VARIABLE_EQUALITY( + "string_dyn_map == string_dyn_map", "Condition is not always true\\."), + // `[NaN]` is found nowhere, not even by its term. + IN_LIST_NAN_LIST("[d] in [[d]]", "d = double\\(\"NaN\"\\)"), + // The checker types the value string, but at runtime it's the int 1, which equals 1.0. + NARROWED_TYPE_NUMERIC_EQUALITY( + "dyn_var == optional.of(1) ? optional.ofNonZeroValue('').or(dyn_var).value() != dyn(1.0)" + + " : true", + "dyn_var = optional\\.of\\(1\\)"), // Map literal keys must be strings, ints, uints or bools, and can't repeat. MAP_LITERAL_DOUBLE_KEY("{1.0: 'a'}[dyn(1)] == 'a'", "Condition is not always true\\."), MAP_LITERAL_BYTES_KEY("size({b'a': 1}) == 1", "Condition is not always true\\."), @@ -2247,8 +2321,11 @@ public void isAlwaysTrue_dynamicMapComprehensionNestedEquality_violated() throws + " 3: [3]} ? r.l.all(x, r.m.exists(k, r.m[k] == x)) : true)") .getAst(); // A looser timeout than the default: comparing a dyn map with a literal admits every numeric - // representation of its keys and values, a state space that takes 5-15 s to explore locally. - CelVerifier verifier = withRuntimeOracle(CEL, b -> b.setTimeout(Duration.ofSeconds(20))); + // representation of its keys and values, a state space that takes 5-25 s to explore remotely + // (longer on GitHub runners). + // TODO: Restore 20 s once the slowdown since map literal key validation is + // recovered. + CelVerifier verifier = withRuntimeOracle(CEL, b -> b.setTimeout(Duration.ofSeconds(60))); CelVerificationResult result = verifier.isAlwaysTrue(ast); @@ -2262,10 +2339,42 @@ private enum IsInconclusiveTestCase { "int_list == [1, 0] ? int_list.exists(x, x == 1 ? int('5') == 5 : 1 / x == 1) : true"), // nested_list[5] is past the unroll limit, so it may not be a list. APPROXIMATE_DYN_RANGE("size(nested_list) == 6 ? dyn(nested_list)[5].all(e, e == e) : true"), - // A map literal's non-literal list value compares by its term. + // Ints compare with doubles read out of lists and maps that aren't literals approximately. + LIST_VARIABLES_ACROSS_NUMERIC_ELEMENTS( + "dyn_list == [1] && type(dyn_list[0]) == int && dyn_var == [1.0] && type(dyn_var[0]) ==" + + " double ? dyn_list != dyn_var : true"), + DYN_LISTS_PAIRWISE_EQUALITY( + "int_list == [1] && int_list_2 == [2] && dyn_var == [1.0] && type(dyn_var[0]) == double &&" + + " dyn_var2 == [2.0] && type(dyn_var2[0]) == double ? !(dyn(int_list) == dyn_var &&" + + " dyn(int_list_2) == dyn_var2 && dyn(int_list) != dyn_var2 && dyn(int_list_2) !=" + + " dyn_var) : true"), + MAP_LITERAL_VARIABLE_LIST_VALUE_NEQ( + "int_list == [1] && dyn_var == {'a': [1.0]} && type(dyn_var['a'][0]) == double ?" + + " {'a': dyn(int_list)} != dyn_var : true"), MAP_LITERAL_VARIABLE_LIST_VALUE( "int_list == [1] && dyn_list == [1.0] && dyn_var == {'a': dyn_list} ?" + " {'a': dyn(int_list)} == dyn_var : true"), + // Elements past the unroll limit aren't constrained to bool, so they may differ by their terms. + NOT_IN_BOOL_LIST_PAST_UNROLL_LIMIT( + "size(bool_list) == 6 && size(bool_list_2) == 6 && !(false in bool_list)" + + " && !(false in bool_list_2) ? bool_list == bool_list_2 : true"), + // An absent optional entry shifts the keys, so their values aren't typed by the entries. + MAP_LITERAL_ABSENT_OPTIONAL_ENTRY( + "dyn_var == {'b': [1], 'c': 0} ? {?'a': optional.none(), 'b': [1.0], 'c': 0} == dyn_var" + + " : true"), + // Lists that aren't literals compare, and `in` matches, only up to the unroll limit. + LIST_PAST_UNROLL_LIMIT_EQ("[0, 0, 0, 0, 0] + [dyn(1)] == [0, 0, 0, 0, 0] + [dyn(2)]"), + IN_LIST_PAST_UNROLL_LIMIT( + "x == 1 && u == 1u && d == 1.0 ? !(x in [0, 0, 0, 0, 0] + [dyn(1.0)]) || !(u in [0, 0, 0," + + " 0, 0] + [dyn(1.0)]) || !(d in [0, 0, 0, 0, 0] + [dyn(1)]) : true"), + IN_LIST_PAST_UNROLL_LIMIT_STRING("dyn_list == [0, 0, 0, 0, 0, 'a'] ? 'a' in dyn_list : true"), + IN_LIST_PAST_UNROLL_LIMIT_MISSING("x == 2 ? x in [0, 0, 0, 0, 0] + [dyn(1.0)] : true"), + IN_LIST_PAST_UNROLL_LIMIT_LIST( + "nested_list == [[0], [0], [0], [0], [0], [1]] ? !(dyn([1.0]) in nested_list) : true"), + LIST_PAST_UNROLL_LIMIT_NEQ("[0, 0, 0, 0, 0] + [dyn(1)] != [0, 0, 0, 0, 0] + [dyn(1)]"), + MAP_PAST_UNROLL_LIMIT_EQ( + "x == 1 ? (x == 1 ? {'a': 0, 'b': 0, 'c': 0, 'd': 0, 'e': 0, 'f': 1} : {}) == (x == 1 ?" + + " {'a': 0, 'b': 0, 'c': 0, 'd': 0, 'e': 0, 'f': 2} : {}) : true"), // Lists nested in map values past the unroll limit compare approximately. MAP_VALUE_LIST_PAST_UNROLL_LIMIT( "!(size(int_list) == 6 && {'k': [1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 1.5]} == {'k': [1.0] +" @@ -2356,6 +2465,25 @@ public void isAlwaysTrue_inconclusive_containsPotentialCounterexample() throws E } private enum EquivalenceInconclusiveTestCase { + // A list or map typed dyn holding NaN (e.g. `[NaN]`) differs from itself, so these do diverge, + // but lists and maps typed dyn on both sides compare approximately. + DYN_NAN_INPUT_AND_LITERAL("dyn_var != dyn_var ? 0.0 / 0.0 : dyn_var", "dyn_var"), + DYN_INDEXED_NAN_AND_LITERAL("dyn_var[0] != dyn_var[0] ? 0.0 / 0.0 : dyn_var[0]", "dyn_var[0]"), + DYN_OPTIONAL_NAN_AND_LITERAL( + "dyn_var.value() != dyn_var.value() ? 0.0 / 0.0 : dyn_var.value()", "dyn_var.value()"), + ANY_NAN_FIELD_AND_LITERAL( + "test_all_types.single_any != test_all_types.single_any" + + " ? 0.0 / 0.0 : test_all_types.single_any", + "test_all_types.single_any"), + // TODO: number_value set from an optional isn't checked to be a double, so it may + // be a list here. + DYN_OPTIONAL_JSON_NAN_AND_LITERAL( + "google.protobuf.Value{?number_value: dyn_var} != google.protobuf.Value{?number_value:" + + " dyn_var} ? 0.0 / 0.0 : google.protobuf.Value{?number_value: dyn_var}", + "google.protobuf.Value{?number_value: dyn_var}"), + // The lists nested in literals are compared element-wise up to the unroll limit. + NESTED_LIST_VARIABLE_EQUALITY( + "[int_list] == [int_list_2] ? int_list == int_list_2 : true", "true"), MASKED_BY_BMC( "int_list == [1, 2, 3, 4, 5, 6] ? int_list.all(x, x > 0) : true", "int_list == [1, 2, 3, 4, 5, 6] ? (int_list.all(x, x > 0) || size(int_list) == 6) : true"), @@ -2581,8 +2709,6 @@ private enum EquivalenceTestCase { GREATER_EQUALS("x >= y", "y <= x"), ADD("x + y", "y + x"), SUBTRACT("x - y == 5", "5 == x - y"), - NESTED_LIST_VARIABLE_EQUALITY( - "[int_list] == [int_list_2] ? int_list == int_list_2 : true", "true"), NESTED_SYMBOLIC_LIST_EXTENSIONALITY( "size(nested_list) >= 2 && nested_list[0] == nested_list[1] ? [nested_list[0]] ==" + " [nested_list[1]] : true", @@ -2707,6 +2833,30 @@ private enum EquivalenceTestCase { OPTIONAL_FIELD_SELECTION_MAP_COMPREHENSION( "{'a': 1, 'b': 2}.transformMap(k, v, v > 1, v).?b", "optional.of(2)"), OPTIONAL_FIELD_SELECTION_BINDER("cel.bind(m, {'a': 1}, m.?a)", "optional.of(1)"), + // Selecting from or indexing an optional does so optionally. + OPTIONAL_CHAINING_SELECT( + "optional.of({'c': {'index': 'goodbye'}}).c.index", "optional.of('goodbye')"), + OPTIONAL_CHAINING_SELECT_MISSING("optional.of({'c': {}}).c.missing", "optional.none()"), + OPTIONAL_CHAINING_SELECT_NONE("optional.none().c", "optional.none()"), + OPTIONAL_CHAINING_SELECT_OPTIONAL_VALUE( + "optional.of({'a': optional.of(1)}).a", "optional.of(optional.of(1))"), + OPTIONAL_CHAINING_HAS_PRESENT("has(optional.of({'c': 1}).c)", "true"), + OPTIONAL_CHAINING_HAS_ABSENT("has(optional.of({'c': 1}).d)", "false"), + OPTIONAL_CHAINING_HAS_NONE("has(optional.none().c)", "false"), + OPTIONAL_CHAINING_SELECT_PROTO3_ZERO( + "optional.of(TestAllTypes{single_int64: 0}).single_int64", "optional.none()"), + OPTIONAL_CHAINING_SELECT_UNSET_WRAPPER( + "optional.of(TestAllTypes{}).single_int64_wrapper", "optional.none()"), + OPTIONAL_CHAINING_INDEX("optional.of(['list-value'])[0]", "optional.of('list-value')"), + OPTIONAL_CHAINING_INDEX_MISSING("optional.of({'c': {}}).c['missing']", "optional.none()"), + OPTIONAL_CHAINING_INDEX_NONE("optional.none()[0]", "optional.none()"), + OPTIONAL_SELECT_THEN_INDEX( + "optional.of(TestAllTypes{repeated_string: ['foo']}).?repeated_string[0]", + "optional.of('foo')"), + OPTIONAL_CHAINING_DYN( + "dyn_var == optional.of({'a': [1]}) ? dyn_var.a[0] : optional.of(1)", "optional.of(1)"), + OPTIONAL_CHAINING_DYN_NONE( + "request == optional.none() ? request.l : optional.none()", "optional.none()"), JSON_VALUE_BOOL("google.protobuf.Value{bool_value: true}", "true"), JSON_VALUE_NUMBER("google.protobuf.Value{number_value: 1.0}", "1.0"), JSON_VALUE_NULL("google.protobuf.Value{null_value: 0}", "null"), @@ -2777,18 +2927,6 @@ private enum EquivalenceTestCase { WRAPPER_FLOAT_NAN("d != d ? google.protobuf.FloatValue{value: d} : 0.0", "d != d ? d : 0.0"), DOUBLE_NAN_ARITHMETIC("d != d ? d + 1.0 : 0.0", "d != d ? d : 0.0"), DOUBLE_NAN_INPUT_AND_LITERAL("d != d ? d : 0.0", "d != d ? 0.0 / 0.0 : 0.0"), - DYN_NAN_INPUT_AND_LITERAL("dyn_var != dyn_var ? 0.0 / 0.0 : dyn_var", "dyn_var"), - DYN_INDEXED_NAN_AND_LITERAL("dyn_var[0] != dyn_var[0] ? 0.0 / 0.0 : dyn_var[0]", "dyn_var[0]"), - DYN_OPTIONAL_JSON_NAN_AND_LITERAL( - "google.protobuf.Value{?number_value: dyn_var} != google.protobuf.Value{?number_value:" - + " dyn_var} ? 0.0 / 0.0 : google.protobuf.Value{?number_value: dyn_var}", - "google.protobuf.Value{?number_value: dyn_var}"), - DYN_OPTIONAL_NAN_AND_LITERAL( - "dyn_var.value() != dyn_var.value() ? 0.0 / 0.0 : dyn_var.value()", "dyn_var.value()"), - ANY_NAN_FIELD_AND_LITERAL( - "test_all_types.single_any != test_all_types.single_any" - + " ? 0.0 / 0.0 : test_all_types.single_any", - "test_all_types.single_any"), DOUBLE_NAN_IN_LIST("d != d ? [d] : []", "d != d ? [-d] : []"), WRAPPER_FLOAT_IDEMPOTENT_LITERAL( "google.protobuf.FloatValue{value: google.protobuf.FloatValue{value: 0.1}}",