diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 00b04b199..5d6e8c9b2 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -41,6 +41,7 @@ import java.util.ArrayList; import java.util.Arrays; import java.util.HashMap; +import java.util.LinkedHashMap; import java.util.LinkedHashSet; import java.util.List; import java.util.Map; @@ -110,7 +111,7 @@ Set> getInputVariables() { * 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)); + return typeSystem.isTrue(celValue); } /** @@ -342,11 +343,33 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast) List elementsTv = new ArrayList<>(); List> values = new ArrayList<>(); + // Keys must be strings, ints, uints or bools, and can't equal an earlier key in the map. + List invalidKeys = new ArrayList<>(); + Map, BoolExpr> keysSoFar = new LinkedHashMap<>(); for (CelExpr.CelMap.Entry entryAst : createMap.entries()) { TranslatedValue keyTv = translateExpr(entryAst.key(), ast); Expr key = keyTv.z3Expr(); elementsTv.add(keyTv); + invalidKeys.add( + ctx.mkNot( + ctx.mkOr( + typeSystem.isString(key), + typeSystem.isInt(key), + typeSystem.isUint(key), + typeSystem.isBool(key)))); + for (CelZ3TypeSystem.EqualKey equalKey : typeSystem.equalKeys(key)) { + keysSoFar.forEach( + (earlierKey, isPresent) -> { + BoolExpr repeats = + ctx.mkAnd( + isPresent, equalKey.condition(), ctx.mkEq(earlierKey, equalKey.key())); + // Performance only: skips what distinct constant keys rule out. + if (!repeats.simplify().isFalse()) { + invalidKeys.add(repeats); + } + }); + } TranslatedValue valueTv = translateExpr(entryAst.value(), ast); Expr value = valueTv.z3Expr(); @@ -364,6 +387,7 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast) } elementsTv.add(valueTv); values.add(finalValue); + keysSoFar.merge(key, finalPresence, ctx::mkOr); BoolExpr keyAlreadyPresent = (BoolExpr) ctx.mkSelect(mapPresence, key); BoolExpr shouldInsertKey = ctx.mkAnd(ctx.mkNot(keyAlreadyPresent), finalPresence); @@ -381,7 +405,9 @@ private TranslatedValue translateMap(CelExpr celExpr, CelAbstractSyntaxTree ast) context.addConstraint(ctx.mkEq(typeSystem.getMapPresence(mapRef), mapPresence)); context.addConstraint(ctx.mkEq(typeSystem.getMapKeys(mapRef), keysSeq)); - Expr result = typeSystem.wrapMap(mapRef); + Expr result = + typeSystem.withRuntimeError( + typeSystem.wrapMap(mapRef), CelZ3Exprs.mkOrFlattened(ctx, invalidKeys)); propagateTruncatedTypeConstraint(result, values); return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, elementsTv); } diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index 3db4ec809..3c6d2dcb1 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; @@ -43,12 +45,16 @@ import dev.cel.verifier.axioms.CelZ3OverloadTranslator; import java.util.ArrayList; import java.util.Arrays; +import java.util.Comparator; import java.util.List; import java.util.Optional; /** 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 final Context ctx; private final CelZ3TypeSystem typeSystem; private final CelZ3TranslationContext context; @@ -142,9 +148,22 @@ 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)); + CelZ3Exprs.mkOrFlattened(ctx, currentApprox, constrainInWitnessTypes(lhs, list, ast)); + CelType exactListType = exactType(list, ast); + if (extractAstTypeOrDefault(list, ast).kind() != CelKind.MAP + && !(exactListType instanceof ListType + && isExact(exactType(lhs, ast), ((ListType) exactListType).elemType()))) { + List taints = new ArrayList<>(); + BoolExpr found = listMembership(lhs, list, currentZ3Result, ast, taints); + BoolExpr isList = typeSystem.isList(list.z3Expr()); + currentZ3Result = ctx.mkITE(isList, typeSystem.wrapBool(found), currentZ3Result); + currentApprox = + CelZ3Exprs.mkOrFlattened( + ctx, currentApprox, ctx.mkAnd(isList, CelZ3Exprs.mkOrFlattened(ctx, taints))); + } } 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); @@ -549,7 +568,10 @@ 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) { if (arg0.isNumericConstant()) { return getNumericEqualityWithConstant( arg1.z3Expr(), arg0.celExpr().get().constant(), extractAstTypeOrDefault(arg1, ast)); @@ -564,7 +586,8 @@ private BoolExpr getNumericEquality( return getStaticallyKnownNumericEquality(arg0.z3Expr(), type0, arg1.z3Expr()); } - return getDynamicNumericEquality(arg0.z3Expr(), arg1.z3Expr()); + return getDynamicNumericEquality( + arg0.z3Expr(), arg1.z3Expr(), taints, /* approximateIntDouble= */ false); } /** Evaluates numeric equality when types are statically known. */ @@ -582,7 +605,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 +632,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, + (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()); @@ -634,147 +669,137 @@ 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. - */ + // A literal with optional elements has as many as are present. + private boolean isFixedLengthListLiteral(TranslatedValue list) { + return list.isLiteral(ExprKind.Kind.LIST) && !hasOptionalElements(list); + } + + // 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))); + TranslatedValue literal = isLiteralA ? listA : listB; + int size = + isLiteral ? literal.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); + TranslatedValue elemB = listElement(listB, seq1, i, isLiteralB); if (i >= comprehensionUnrollLimit) { - constrainListElement(seq0, idx, elem0, type0); - constrainListElement(seq1, idx, elem1, type1); + constrainListElement(seq0, ctx.mkInt(i), elemA.z3Expr(), guaranteedType(listA)); + constrainListElement(seq1, ctx.mkInt(i), elemB.z3Expr(), guaranteedType(listB)); } - - 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()); + TranslatedValue elemEquality = translateElementEquality(elemA, elemB, ast, isLiteral); + // A literal's length is known. + BoolExpr inBounds = isLiteral ? ctx.mkTrue() : 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); } - // 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. + // 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) { + IntExpr idx = ctx.mkInt(i); + Expr elem = ctx.mkNth(seq, idx); + // A literal's elements are already CEL values (performance only). + if (!isLiteral) { + context.constrainValidValue( + ctx.mkAnd(typeSystem.isList(list.z3Expr()), ctx.mkLt(idx, ctx.mkLength(seq))), elem); + } + return TranslatedValue.create( + elem, + isLiteral ? list.listElementAt(i) : Optional.empty(), + typeSystem, + list.isApproximate()); + } + + // 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)); + } + 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()), + translateElementEquality( + 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); + 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 +830,163 @@ private BoolExpr mapEqualityAtLiteralKeys(TranslatedValue mapA, TranslatedValue return CelZ3Exprs.mkAndFlattened(ctx, equalities); } + // `in` on a list compares each element with lhs by CEL equality, unrolled up to the unroll limit + // unless the list is a literal. Past it, the list axiom (whose result is axiomResult) matches by + // terms, which is CEL equality for lhs that aren't lists, maps, messages or optionals, except + // across ints and doubles. + private BoolExpr listMembership( + TranslatedValue lhs, + TranslatedValue list, + Expr axiomResult, + 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 = + translateElementEquality(listElement(list, seq, i, isLiteral), lhs, ast, 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; + } + Expr z3Lhs = lhs.z3Expr(); + BoolExpr pastLimit = ctx.mkGt(length, ctx.mkInt(comprehensionUnrollLimit)); + BoolExpr isContainer = isContainer(z3Lhs); + found = + ctx.mkOr( + found, + CelZ3Exprs.mkAndFlattened( + ctx, pastLimit, ctx.mkNot(isContainer), typeSystem.isTrue(axiomResult))); + CelType listType = guaranteedType(list); + CelType elemType = + listType instanceof ListType ? ((ListType) listType).elemType() : SimpleType.DYN; + BoolExpr mayMissNumbers = + canBeNumeric(elemType) + ? ctx.mkOr( + typeSystem.isInt(z3Lhs), + typeSystem.isUint(z3Lhs), + ctx.mkAnd( + typeSystem.isDouble(z3Lhs), typeSystem.isIntegral(typeSystem.getDouble(z3Lhs)))) + : ctx.mkFalse(); + BoolExpr mayMissByTerms = isScalarType(elemType) ? ctx.mkFalse() : isContainer; + return approximateWhere( + FUNC_APPROX_IN, + context.recordUnrollLimitApproximation( + CelZ3Exprs.mkAndFlattened( + ctx, pastLimit, ctx.mkNot(found), ctx.mkOr(mayMissNumbers, mayMissByTerms))), + z3Lhs, + list.z3Expr(), + found, + taints); + } + + // Where the recorded approximation holds, the verifier doesn't model this relation between the + // two values, so the result there is an uninterpreted function of them. + private BoolExpr approximateWhere( + String name, + BoolExpr approximation, + Expr z3Expr0, + Expr z3Expr1, + BoolExpr exact, + List taints) { + taints.add(approximation); + Sort sort = typeSystem.celValueSort(); + FuncDecl relation = + typeSystem.internFuncDecl(name, new Sort[] {sort, sort}, ctx.getBoolSort()); + return (BoolExpr) + ctx.mkITE(approximation, (BoolExpr) ctx.mkApp(relation, z3Expr0, z3Expr1), exact); + } + + // Like approximateWhere, for CEL equality, which is symmetric. + private BoolExpr approximateEqualityWhere( + BoolExpr approximation, + Expr z3Expr0, + Expr z3Expr1, + BoolExpr exact, + List taints) { + ImmutableList> args = + ImmutableList.sortedCopyOf( + Comparator.>comparingInt(Expr::getId), Arrays.asList(z3Expr0, z3Expr1)); + return approximateWhere(FUNC_APPROX_EQ, approximation, args.get(0), args.get(1), 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); + } + + // CEL equality of values read out of lists or maps, which are typed dyn. Unless either is a + // literal (or a list or map literal's element), numbers compare numerically but approximately + // across ints and doubles, lists, maps, messages and optionals approximately, and the rest by + // their terms (performance only: unrolling or truncating every such comparison is slow). + private TranslatedValue translateElementEquality( + TranslatedValue arg0, TranslatedValue arg1, CelAbstractSyntaxTree ast, boolean isLiteral) { + if (isLiteral + || arg0.celExpr().filter(CelZ3OperatorTranslator::isContainerLiteral).isPresent() + || arg1.celExpr().filter(CelZ3OperatorTranslator::isContainerLiteral).isPresent()) { + return translateEquality(arg0, arg1, ast, /* isEquals= */ true); + } + Expr z3Arg0 = arg0.z3Expr(); + Expr z3Arg1 = arg1.z3Expr(); + List taints = new ArrayList<>(); + BoolExpr equality = + (BoolExpr) + ctx.mkITE( + ctx.mkAnd(isNumeric(z3Arg0), isNumeric(z3Arg1)), + // Only lhs of `in` may be a constant. + arg1.isNumericConstant() + ? getNumericEquality(arg0, arg1, ast, taints) + : getDynamicNumericEquality( + z3Arg0, z3Arg1, taints, /* approximateIntDouble= */ true), + approximateEqualityWhere( + context.recordApproximation( + "comparisons of lists, maps, messages or optionals read out of lists and" + + " maps", + CelZ3Exprs.mkOrFlattened( + ctx, + ctx.mkAnd(typeSystem.isList(z3Arg0), typeSystem.isList(z3Arg1)), + ctx.mkAnd(typeSystem.isMap(z3Arg0), typeSystem.isMap(z3Arg1)), + ctx.mkAnd(typeSystem.isMessage(z3Arg0), typeSystem.isMessage(z3Arg1)), + ctx.mkAnd( + typeSystem.isOptional(z3Arg0), typeSystem.isOptional(z3Arg1)))), + z3Arg0, + z3Arg1, + ctx.mkEq(z3Arg0, z3Arg1), + taints)); + return TranslatedValue.propagateStrict( + ctx, + typeSystem, + Operator.EQUALS.getFunction(), + typeSystem.wrapBool(equality), + arg0, + arg1) + .withApproximation(CelZ3Exprs.mkOrFlattened(ctx, taints)); + } + + private BoolExpr isContainer(Expr arg) { + return CelZ3Exprs.mkOrFlattened( + ctx, + typeSystem.isList(arg), + typeSystem.isMap(arg), + typeSystem.isMessage(arg), + typeSystem.isOptional(arg)); + } + private static boolean hasContainerLiteralValue(TranslatedValue map) { return map.celExpr().get().map().entries().stream() .anyMatch(e -> isContainerLiteral(e.value())); @@ -838,45 +1020,51 @@ private TranslatedValue translateEquality( 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); + equality = getNumericEquality(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) + isExact(type0, type1) ? mapEqualityAtLiteralKeys(arg0, arg1) : unrollMapEquality(arg0, arg1, ast, taints), typeSystem.getStructuralEquality(z3Arg0, z3Arg1)); - } else if (isStaticallyKnown(type0) && isStaticallyKnown(type1)) { - equality = typeSystem.getStructuralEquality(z3Arg0, z3Arg1); } 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 + // Lists and maps compare by CEL equality, unless their guaranteed types make it their terms'. BoolExpr structuralEq = typeSystem.getStructuralEquality(z3Arg0, z3Arg1); - if ((arg0.isLiteral(ExprKind.Kind.LIST) || arg1.isLiteral(ExprKind.Kind.LIST)) - && !hasOptionalElements(arg0) - && !hasOptionalElements(arg1)) { - structuralEq = - (BoolExpr) - ctx.mkITE( - ctx.mkAnd(typeSystem.isList(z3Arg0), typeSystem.isList(z3Arg1)), - unrollListEquality(arg0, arg1, ast, taints), - structuralEq); + if (!isExact(exactType(arg0, ast), exactType(arg1, ast))) { + BoolExpr bothLists = ctx.mkAnd(typeSystem.isList(z3Arg0), typeSystem.isList(z3Arg1)); + BoolExpr bothMaps = ctx.mkAnd(typeSystem.isMap(z3Arg0), typeSystem.isMap(z3Arg1)); + 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) { + structuralEq = + (BoolExpr) + ctx.mkITE(bothMaps, unrollMapEquality(arg0, arg1, ast, taints), structuralEq); + } else if (!isStaticallyKnown(type0) && !isStaticallyKnown(type1)) { + // Performance only: values read out of lists and maps are typed dyn, and unrolling every + // comparison of them is slow. A side with a known type isn't a list or map here, so + // approximating it too would only slow the solver down. + // 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); + } } - if (canBeNumeric0 && canBeNumeric1) { + if (canBeNumeric(type0) && canBeNumeric(type1)) { BoolExpr bothNumeric = ctx.mkAnd(isNumeric(z3Arg0), isNumeric(z3Arg1)); equality = - (BoolExpr) ctx.mkITE(bothNumeric, getNumericEquality(arg0, arg1, ast), structuralEq); + (BoolExpr) + ctx.mkITE(bothNumeric, getNumericEquality(arg0, arg1, ast, taints), structuralEq); } else { equality = structuralEq; } @@ -1134,6 +1322,36 @@ private static boolean isConcrete(CelType type) { && type.parameters().stream().allMatch(CelZ3OperatorTranslator::isConcrete); } + // Whether values of these types are equal exactly when their terms are. + private static boolean isExact(CelType type0, CelType type1) { + return type0.equals(type1) && hasStructuralEquality(type0); + } + + private static boolean isScalarType(CelType type) { + switch (type.kind()) { + case BOOL: + case BYTES: + case DOUBLE: + case DURATION: + case INT: + case NULL_TYPE: + case STRING: + case TIMESTAMP: + case UINT: + return true; + default: + return false; + } + } + + // The type val is guaranteed to have: a constant's, or else its declared type (static types may + // be narrowed, e.g. `['a'] + dyn_var` is a list(string)). + private CelType exactType(TranslatedValue val, CelAbstractSyntaxTree ast) { + return val.isLiteral(ExprKind.Kind.CONSTANT) + ? extractAstTypeOrDefault(val, ast) + : guaranteedType(val); + } + /** Whether values of {@code type} are equal exactly when their terms are. */ private static boolean hasStructuralEquality(CelType type) { switch (type.kind()) { @@ -1154,6 +1372,10 @@ private static boolean hasStructuralEquality(CelType type) { } } + private static boolean canBeNumeric(CelType type) { + return !isStaticallyKnown(type) || isNumericType(type); + } + private static boolean isNumericType(CelType type) { CelKind kind = type.kind(); return kind == CelKind.INT || kind == CelKind.UINT || kind == CelKind.DOUBLE; diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index b3ba7d4fe..4a57b4e82 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. */ + public 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); @@ -951,8 +956,8 @@ public BoolExpr doubleLeInt(FPExpr d, IntExpr n) { return ctx.mkAnd(ctx.mkNot(ctx.mkFPIsNaN(d)), ctx.mkNot(intLtDouble(n, d))); } - // Returns the double that holds the constant n exactly, if any. Comparing with it needs no - // truncation (performance only), and it's the double key equal to n. + // Performance only: a constant that a double holds exactly compares as that double, without the + // uninterpreted truncation. private Optional asExactDouble(IntExpr n) { Expr simplified = n.simplify(); if (!(simplified instanceof IntNum)) { diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 9853fb8d1..ae986bb25 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -349,7 +349,7 @@ private enum InexactWitnessTestCase { LIST_PAST_UNROLL_LIMIT("size(int_list) == 6", "int_list"), MAP_PAST_UNROLL_LIMIT("size(string_int_map) == 6", "string_int_map"), LIST_WITH_INEXACT_ELEMENT("dyn_list == [b'\\xc3\\xa9']", "dyn_list"), - MAP_WITH_INEXACT_KEY("dyn_int_map == {b'\\xc3\\xa9': 1}", "dyn_int_map"), + MAP_WITH_INEXACT_KEY("b'\\xc3\\xa9' in dyn_int_map", "dyn_int_map"), MAP_WITH_INEXACT_VALUE("string_dyn_map == {'a': b'\\xc3\\xa9'}", "string_dyn_map"), OPTIONAL_WITH_INEXACT_VALUE("opt_dyn_var == optional.of(b'\\xc3\\xa9')", "opt_dyn_var"); @@ -677,6 +677,12 @@ public void isSatisfiable_approximate_returnsPotentialSatisfyingInput() throws E } private enum IsSatisfiableInconclusiveTestCase { + // Ints compare with doubles read out of lists 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 +813,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 +899,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"), @@ -991,14 +993,12 @@ private enum IsAlwaysTrueTestCase { MAP_SIZE("size({'a': 1, 'b': 2}) == 2"), EMPTY_LIST_SIZE("size([]) == 0"), EMPTY_MAP_SIZE("size({}) == 0"), - MAP_LITERAL_DUPLICATE_KEYS("size({'a': 1, 'a': 2}) == 1"), LIST_CONCATENATION_SIZE("size(int_list + [1]) == size(int_list) + 1"), STRING_CONCATENATION_SIZE("size(role + 'a') == size(role) + 1"), BYTES_CONCATENATION_SIZE("size(by + b'a') == size(by) + 1"), LIST_SIZE_NON_NEGATIVE("size(int_list) >= 0"), STRING_SIZE_NON_NEGATIVE("size(role) >= 0"), MAP_SIZE_NON_NEGATIVE("size(string_int_map) >= 0"), - DYNAMIC_MAP_DUPLICATE_KEYS("!(x == y) || size({x: 1, y: 2}) == 1"), MEMBER_LIST_SIZE("[1, 2].size() == 2"), MEMBER_STRING_SIZE("'abc'.size() == 3"), MEMBER_BYTES_SIZE("b'abc'.size() == 3"), @@ -1067,7 +1067,6 @@ 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"), 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( @@ -1123,6 +1122,8 @@ private enum IsAlwaysTrueTestCase { DYN_MESSAGE_UNSET_ENUM_FIELD("dyn(TestAllTypes{}).standalone_enum == 0"), DYN_MESSAGE_SET_FIELD_TYPE("type(dyn(test_all_types).single_string) == string"), STRUCT_DEFAULT_ENUM_EQ_UNSET("TestAllTypes{standalone_enum: 0} == TestAllTypes{}"), + // An absent optional entry's key may repeat. + MAP_LITERAL_ABSENT_OPTIONAL_KEY_REPEATED("{?1: optional.none(), 1: 'b'}[1] == 'b'"), // Map keys and values compare by CEL equality: numerically across int, uint and double. MAP_LITERAL_EQ_ACROSS_NUMERIC_KEYS("dyn({1: 'a'}) == {1u: 'a'}"), MAP_LITERAL_EQ_ACROSS_NUMERIC_VALUES("dyn({'a': 1}) == {'a': 1.0}"), @@ -1145,6 +1146,23 @@ 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_PAST_UNROLL_LIMIT_BY_TERMS( + "(dyn_list == [0, 0, 0, 0, 0, 'a'] ? 'a' in dyn_list : true)" + + " && !(1.5 in [0, 0, 0, 0, 0] + [dyn(1)])"), + 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)" @@ -1881,6 +1899,22 @@ 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\"\\)"), + // 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\\."), + MAP_LITERAL_REPEATED_KEY("size({1: 'a', 1: 'b'}) == 1", "Condition is not always true\\."), + MAP_LITERAL_NUMERICALLY_REPEATED_KEY( + "size({1: 'a', 1u: 'b'}) == 2", "Condition is not always true\\."), + MAP_LITERAL_PRESENT_OPTIONAL_KEY_REPEATED( + "size({?1: optional.of('a'), 1: 'b'}) == 1", "Condition is not always true\\."), + MAP_LITERAL_VARIABLE_KEY_REPEATED( + "x == 1 ? size({x: 'a', 1u: 'b'}) == 2 : true", "Condition is not always true\\."), // The exact error wins over whether the empty list(dyn) field is set. STRUCT_EMPTY_LIST_DYN_FIELD_WITH_ERROR( "TestAllTypes{repeated_value: [], single_int64: 1 / 0} == TestAllTypes{}", @@ -2252,10 +2286,34 @@ 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"), + // Lists that aren't literals compare, and `in` matches across ints and doubles, 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_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] +" @@ -2346,6 +2404,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"), @@ -2571,8 +2648,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", @@ -2767,18 +2842,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}}",