diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index d056826e4..3db4ec809 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -23,9 +23,7 @@ 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.IntNum; import com.microsoft.z3.SeqExpr; import dev.cel.common.CelAbstractSyntaxTree; import dev.cel.common.CelFunctionDecl; @@ -226,15 +224,18 @@ private BoolExpr constrainInWitnessTypes( ? mayObserveTruncatedTypeConstraint(ast, lhsTv) : mayObserveTruncatedTypeConstraint(ast, lhsTv, rhsTv); } else if (rhsType instanceof MapType) { - // IN_MAP only probes the presence of lhs itself. + // IN_MAP probes lhs and its numeric counterparts. ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(rhs)); - BoolExpr inMap = (BoolExpr) ctx.mkSelect(mapPresence, lhs); - context.addConstraint( - ctx.mkImplies( - ctx.mkAnd(typeSystem.isMap(rhs), inMap), - context - .typeConstraintGenerator() - .createTypeConstraintForType(lhs, ((MapType) rhsType).keyType()))); + for (CelZ3TypeSystem.EqualKey key : typeSystem.equalKeys(lhs)) { + context.addConstraint( + ctx.mkImplies( + ctx.mkAnd( + typeSystem.isMap(rhs), + key.condition(), + (BoolExpr) ctx.mkSelect(mapPresence, key.key())), + typeConstraintGenerator.createTypeConstraintForType( + key.key(), ((MapType) rhsType).keyType()))); + } return context.isTruncatedMap(rhs); } return CelZ3Exprs.mkOrFlattened( @@ -693,6 +694,126 @@ private BoolExpr unrollListEquality( 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. + private BoolExpr unrollMapEquality( + TranslatedValue mapA, + TranslatedValue mapB, + CelAbstractSyntaxTree ast, + List taints) { + // 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(); + BoolExpr isOtherMap = typeSystem.isMap(other); + Expr literalRef = typeSystem.getMapRef(literal.z3Expr()); + SeqExpr keys = typeSystem.getMapKeys(literalRef); + ArrayExpr values = (ArrayExpr) typeSystem.getMapValues(literalRef); + 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(); + // 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++) { + 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()), + ast, + /* isEquals= */ true); + 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)))); + } + // 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)); + return CelZ3Exprs.mkAndFlattened(ctx, equalities); + } + + // Maps whose keys and values compare by their terms are equal when they have the same keys, and + // the same values at the literal's keys (performance only). + private BoolExpr mapEqualityAtLiteralKeys(TranslatedValue mapA, TranslatedValue mapB) { + boolean isLiteralA = mapA.isLiteral(ExprKind.Kind.MAP); + Expr literalRef = typeSystem.getMapRef((isLiteralA ? mapA : mapB).z3Expr()); + Expr otherRef = typeSystem.getMapRef((isLiteralA ? mapB : mapA).z3Expr()); + SeqExpr keys = typeSystem.getMapKeys(literalRef); + ArrayExpr values = (ArrayExpr) typeSystem.getMapValues(literalRef); + ArrayExpr otherValues = (ArrayExpr) typeSystem.getMapValues(otherRef); + List equalities = new ArrayList<>(); + // Same size and same keys. Past the unroll limit, a map's presence isn't tied to its keys, so + // matching presence alone doesn't rule out extra keys (e.g. a 6-key map equal to {'a': 1}). + equalities.add(ctx.mkEq(ctx.mkLength(keys), ctx.mkLength(typeSystem.getMapKeys(otherRef)))); + equalities.add( + ctx.mkEq(typeSystem.getMapPresence(literalRef), typeSystem.getMapPresence(otherRef))); + int size = (isLiteralA ? mapA : mapB).celExpr().get().map().entries().size(); + for (int i = 0; i < size; i++) { + Expr key = ctx.mkNth(keys, ctx.mkInt(i)); + equalities.add( + ctx.mkImplies( + ctx.mkLt(ctx.mkInt(i), ctx.mkLength(keys)), + typeSystem.getStructuralEquality( + ctx.mkSelect(values, key), ctx.mkSelect(otherValues, key)))); + } + return CelZ3Exprs.mkAndFlattened(ctx, equalities); + } + + private static boolean hasContainerLiteralValue(TranslatedValue map) { + return map.celExpr().get().map().entries().stream() + .anyMatch(e -> isContainerLiteral(e.value())); + } + + 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( @@ -724,6 +845,15 @@ private TranslatedValue translateEquality( && !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); } else { @@ -773,181 +903,29 @@ private Expr buildListIndex( ctx.mkGe((ArithExpr) index, ctx.mkInt(0)), ctx.mkLt((ArithExpr) index, ctx.mkLength(seq))); - Expr val = ctx.mkNth(seq, (ArithExpr) index); - context.constrainValidValue(ctx.mkAnd(typeGuard, inBounds), 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( - inBounds, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone()); - } - - return ctx.mkITE(inBounds, val, typeSystem.mkError()); - } - - private Optional extractIntNumSafe(Expr expr) { - Expr simplified = expr.simplify(); - - if (!simplified.isApp()) { - return Optional.empty(); - } - - FuncDecl decl = simplified.getFuncDecl(); - if (decl.equals(typeSystem.intCons().ConstructorDecl()) - || decl.equals(typeSystem.uintCons().ConstructorDecl())) { - return Optional.of(simplified.getArgs()[0]) - .filter(IntNum.class::isInstance) - .map(IntNum.class::cast) - .map(IntNum::getInt64); - } - - return Optional.empty(); - } - - private static final class ProbeResult { - private final BoolExpr altInMap; - private final Expr altVal; - - private ProbeResult(BoolExpr altInMap, Expr altVal) { - this.altInMap = altInMap; - this.altVal = altVal; - } - } - - private ProbeResult createProbeResult( - BoolExpr inMapOrig, - Expr valOrig, - BoolExpr cond1, - Expr key1, - BoolExpr cond2, - Expr key2, - ArrayExpr mapPresence, - ArrayExpr mapValues) { - BoolExpr inMap1 = (BoolExpr) ctx.mkSelect(mapPresence, key1); - Expr val1 = ctx.mkSelect(mapValues, key1); - BoolExpr inMap2 = (BoolExpr) ctx.mkSelect(mapPresence, key2); - Expr val2 = ctx.mkSelect(mapValues, key2); - - BoolExpr condMap1 = CelZ3Exprs.mkAndFlattened(ctx, cond1, inMap1); - BoolExpr condMap2 = CelZ3Exprs.mkAndFlattened(ctx, cond2, inMap2); - - BoolExpr altInMap = CelZ3Exprs.mkOrFlattened(ctx, inMapOrig, condMap1, condMap2); - Expr altVal = - CelZ3Exprs.SwitchBuilder.newBuilder(ctx) - .addCase(inMapOrig, valOrig) - .addCase(condMap1, val1) - .addCase(condMap2, val2) - .build(valOrig); - - return new ProbeResult(altInMap, altVal); + return finishIndex(inBounds, ctx.mkNth(seq, (ArithExpr) index), typeGuard, isOptional); } private Expr buildMapIndex( Expr lhsTrans, Expr rhsTrans, BoolExpr typeGuard, boolean isOptional) { - Expr mapRef = typeSystem.getMapRef(lhsTrans); - ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef); - ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef); - - BoolExpr inMapOrig = (BoolExpr) ctx.mkSelect(mapPresence, rhsTrans); - Expr valOrig = ctx.mkSelect(mapValues, rhsTrans); - - BoolExpr isInt = typeSystem.isInt(rhsTrans); - BoolExpr isUint = typeSystem.isUint(rhsTrans); - BoolExpr isDouble = typeSystem.isDouble(rhsTrans); - - // Common double key for both int and uint - FPExpr intUintFp; - Optional rhsNum = extractIntNumSafe(rhsTrans); - boolean hasExactDouble = rhsNum.isPresent(); - if (hasExactDouble) { - intUintFp = typeSystem.mkFpDouble((double) rhsNum.get()); - } else { - intUintFp = typeSystem.mkFpDouble(0.0); - } - Expr intUintDoubleKey = typeSystem.wrapDouble(intUintFp); - - // Int probes - IntExpr rawInt = (IntExpr) ctx.mkITE(isInt, typeSystem.getInt(rhsTrans), ctx.mkInt(0)); - BoolExpr intHasUint = ctx.mkGe(rawInt, ctx.mkInt(0)); - Expr intUintKey = typeSystem.wrapUint(rawInt); - - BoolExpr intHasDouble = hasExactDouble ? isInt : ctx.mkFalse(); - ProbeResult intProbe = - createProbeResult( - inMapOrig, - valOrig, - intHasUint, - intUintKey, - intHasDouble, - intUintDoubleKey, - mapPresence, - mapValues); - - // Uint probes - IntExpr rawUint = (IntExpr) ctx.mkITE(isUint, typeSystem.getUint(rhsTrans), ctx.mkInt(0)); - BoolExpr uintHasInt = ctx.mkLe(rawUint, ctx.mkInt(CelNumericBounds.MAX_INT64)); - Expr uintIntKey = typeSystem.wrapInt(rawUint); - - BoolExpr uintHasDouble = hasExactDouble ? isUint : ctx.mkFalse(); - ProbeResult uintProbe = - createProbeResult( - inMapOrig, - valOrig, - uintHasInt, - uintIntKey, - uintHasDouble, - intUintDoubleKey, - mapPresence, - mapValues); - - // Double probes - FPExpr dVal = guardedDouble(rhsTrans); - IntExpr dInt = typeSystem.truncateDouble(dVal); - BoolExpr doubleIsExact = typeSystem.isIntegral(dVal); - Expr doubleIntKey = typeSystem.wrapInt(dInt); - Expr doubleUintKey = typeSystem.wrapUint(dInt); - // TODO: -2^63 finds an int key here, but the spec doesn't say whether it should. - BoolExpr doubleHasInt = ctx.mkAnd(doubleIsExact, ctx.mkNot(typeSystem.checkIntOverflow(dInt))); - BoolExpr doubleHasUint = ctx.mkAnd(doubleIsExact, ctx.mkGe(dInt, ctx.mkInt(0))); - ProbeResult doubleProbe = - createProbeResult( - inMapOrig, - valOrig, - doubleHasInt, - doubleIntKey, - doubleHasUint, - doubleUintKey, - mapPresence, - mapValues); - - BoolExpr finalInMap = - (BoolExpr) - CelZ3Exprs.SwitchBuilder.newBuilder(ctx) - .addCase(isInt, intProbe.altInMap) - .addCase(isUint, uintProbe.altInMap) - .addCase(isDouble, doubleProbe.altInMap) - .build(inMapOrig); - - Expr finalVal = - CelZ3Exprs.SwitchBuilder.newBuilder(ctx) - .addCase(isInt, intProbe.altVal) - .addCase(isUint, uintProbe.altVal) - .addCase(isDouble, doubleProbe.altVal) - .build(valOrig); - - context.constrainValidValue(ctx.mkAnd(typeGuard, finalInMap), finalVal); + ImmutableList equalKeys = typeSystem.equalKeys(rhsTrans); + return finishIndex( + typeSystem.hasEqualKey(lhsTrans, equalKeys), + typeSystem.valueAtEqualKey(lhsTrans, equalKeys), + typeGuard, + isOptional); + } + // Returns val where found, or else an error (or an empty optional). + private Expr finishIndex(BoolExpr found, Expr val, BoolExpr typeGuard, boolean isOptional) { + context.constrainValidValue(ctx.mkAnd(typeGuard, found), val); if (isOptional) { - Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), finalVal); - context.addConstraint(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), finalVal)); + Expr resultOptRef = ctx.mkApp(typeSystem.optionalOfRefFunc(), val); + context.addConstraint(ctx.mkEq(typeSystem.getOptionalValue(resultOptRef), val)); context.addConstraint(typeSystem.optHasValue(resultOptRef)); - return ctx.mkITE( - finalInMap, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone()); + return ctx.mkITE(found, typeSystem.mkOptionalOf(resultOptRef), typeSystem.mkOptionalNone()); } - - return ctx.mkITE(finalInMap, finalVal, typeSystem.mkError()); + return ctx.mkITE(found, val, typeSystem.mkError()); } private TranslatedValue translateIndex( @@ -1156,6 +1134,26 @@ private static boolean isConcrete(CelType type) { && type.parameters().stream().allMatch(CelZ3OperatorTranslator::isConcrete); } + /** Whether values of {@code type} are equal exactly when their terms are. */ + private static boolean hasStructuralEquality(CelType type) { + switch (type.kind()) { + case BOOL: + case INT: + case UINT: + case STRING: + case BYTES: + case TIMESTAMP: + case DURATION: + return true; + case LIST: + case MAP: + return type.parameters().stream().allMatch(CelZ3OperatorTranslator::hasStructuralEquality); + default: + // Doubles (NaN, -0.0), dyn, messages and the rest compare by CEL equality. + return false; + } + } + 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 b0f05b68f..b3ba7d4fe 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -14,6 +14,8 @@ package dev.cel.verifier; +import static com.google.common.collect.ImmutableList.toImmutableList; + import com.google.auto.value.AutoValue; import com.google.common.collect.ImmutableList; import com.google.common.collect.ObjectArrays; @@ -47,6 +49,7 @@ import java.util.LinkedHashSet; import java.util.List; import java.util.Map; +import java.util.Optional; import java.util.Set; /** @@ -829,6 +832,70 @@ public BoolExpr isValidValue(Expr val) { return ctx.mkAnd(ctx.mkNot(isErrorOrUnknown(val)), isValidScalar(val)); } + /** + * Returns the keys a lookup of {@code key} in a map finds, as {@code RuntimeEquality.findInMap} + * does: {@code key} itself, and its numeric counterparts across int and uint. + */ + ImmutableList equalKeys(Expr key) { + ImmutableList.Builder keys = ImmutableList.builder(); + keys.add(EqualKey.create(key, ctx.mkTrue())); + BoolExpr isInt = isInt(key); + addEqualKey(keys, wrapUint(getInt(key)), ctx.mkAnd(isInt, ctx.mkGe(getInt(key), ctx.mkInt(0)))); + BoolExpr isUint = isUint(key); + addEqualKey( + keys, + wrapInt(getUint(key)), + ctx.mkAnd(isUint, ctx.mkLe(getUint(key), ctx.mkInt(CelNumericBounds.MAX_INT64)))); + // Performance only: a key that can't be a double needs no truncation. + BoolExpr isDouble = isDouble(key); + if (!isDouble.simplify().isFalse()) { + FPExpr d = (FPExpr) ctx.mkITE(isDouble, getDouble(key), mkFpDouble(0.0)); + IntExpr t = truncateDouble(d); + BoolExpr isIntegralDouble = ctx.mkAnd(isDouble, isIntegral(d)); + // TODO: -2^63 finds an int key here, but the spec doesn't say whether it should. + addEqualKey(keys, wrapInt(t), ctx.mkAnd(isIntegralDouble, ctx.mkNot(checkIntOverflow(t)))); + addEqualKey(keys, wrapUint(t), ctx.mkAnd(isIntegralDouble, ctx.mkGe(t, ctx.mkInt(0)))); + } + return keys.build(); + } + + // Performance only: skips the keys a constant key can't match, and folds the conditions it + // decides. + private void addEqualKey(ImmutableList.Builder keys, Expr key, BoolExpr condition) { + BoolExpr simplified = (BoolExpr) condition.simplify(); + if (!simplified.isFalse()) { + keys.add(EqualKey.create(key, simplified.isTrue() ? simplified : condition)); + } + } + + /** Returns whether {@code map} has a key equal to {@code key}. */ + public BoolExpr hasEqualKey(Expr map, Expr key) { + return hasEqualKey(map, equalKeys(key)); + } + + BoolExpr hasEqualKey(Expr map, ImmutableList equalKeys) { + ArrayExpr presence = (ArrayExpr) getMapPresence(getMapRef(map)); + return CelZ3Exprs.mkOrFlattened( + ctx, equalKeys.stream().map(k -> isPresent(presence, k)).collect(toImmutableList())); + } + + /** Returns the value of {@code map} at a key equal to one of {@code equalKeys}, if any. */ + Expr valueAtEqualKey(Expr map, ImmutableList equalKeys) { + Expr mapRef = getMapRef(map); + ArrayExpr presence = (ArrayExpr) getMapPresence(mapRef); + ArrayExpr values = (ArrayExpr) getMapValues(mapRef); + CelZ3Exprs.SwitchBuilder value = CelZ3Exprs.SwitchBuilder.newBuilder(ctx); + for (EqualKey k : equalKeys) { + value.addCase(isPresent(presence, k), ctx.mkSelect(values, k.key())); + } + return value.build(mkUnknown()); + } + + private BoolExpr isPresent(ArrayExpr presence, EqualKey k) { + return CelZ3Exprs.mkAndFlattened( + ctx, k.condition(), (BoolExpr) ctx.mkSelect(presence, k.key())); + } + /** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */ public BoolExpr checkUintOverflow(ArithExpr result) { return ctx.mkOr( @@ -845,6 +912,10 @@ BoolExpr intEqDouble(IntExpr n, FPExpr d) { /** Returns whether the integer {@code n} is less than the double {@code d}. */ public BoolExpr intLtDouble(IntExpr n, FPExpr d) { + Optional exact = asExactDouble(n); + if (exact.isPresent()) { + return ctx.mkFPLt(exact.get(), d); + } IntExpr t = truncateDouble(d); return ctx.mkOr( ctx.mkFPGEq(d, mkFpDouble(CelNumericBounds.TWO_TO_64)), @@ -857,6 +928,10 @@ public BoolExpr intLtDouble(IntExpr n, FPExpr d) { /** Returns whether the double {@code d} is less than the integer {@code n}. */ public BoolExpr doubleLtInt(FPExpr d, IntExpr n) { + Optional exact = asExactDouble(n); + if (exact.isPresent()) { + return ctx.mkFPLt(d, exact.get()); + } IntExpr t = truncateDouble(d); return ctx.mkOr( ctx.mkFPLEq(d, ctx.mkFPNeg(mkFpDouble(CelNumericBounds.TWO_TO_64))), @@ -876,6 +951,21 @@ 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. + private Optional asExactDouble(IntExpr n) { + Expr simplified = n.simplify(); + if (!(simplified instanceof IntNum)) { + return Optional.empty(); + } + BigInteger value = ((IntNum) simplified).getBigInteger(); + double d = value.doubleValue(); + return Double.isFinite(d) + && DoubleMath.roundToBigInteger(d, RoundingMode.UNNECESSARY).equals(value) + ? Optional.of(mkFpDouble(d)) + : Optional.empty(); + } + /** Returns whether {@code d} is an integer of magnitude below 2^64. */ BoolExpr isIntegral(FPExpr d) { return ctx.mkAnd(isBelowTwoTo64(d), ctx.mkNot(hasFraction(d))); @@ -962,6 +1052,18 @@ private static String totalNanosString(long seconds, int nanos) { .toString(); } + /** A key a map lookup may find, and when. */ + @AutoValue + abstract static class EqualKey { + abstract Expr key(); + + abstract BoolExpr condition(); + + static EqualKey create(Expr key, BoolExpr condition) { + return new AutoValue_CelZ3TypeSystem_EqualKey(key, condition); + } + } + @AutoValue abstract static class FuncDeclKey { abstract String name(); 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 56b2d366b..f24552dfe 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/InAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/InAxiom.java @@ -14,7 +14,6 @@ package dev.cel.verifier.axioms; -import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; @@ -99,14 +98,8 @@ public final class InAxiom { }) .addBinaryOverloadTranslator( StandardFunction.Overload.InternalOperator.IN_MAP.celOverloadDecl(), - (ctx, typeSystem, constraintSink, lhsTrans, rhsTrans) -> { - Expr mapRef = typeSystem.getMapRef(rhsTrans); - ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef); - - BoolExpr inMap = (BoolExpr) ctx.mkSelect(mapPresence, lhsTrans); - - return Optional.of(typeSystem.wrapBool(inMap)); - }) + (ctx, typeSystem, constraintSink, lhsTrans, rhsTrans) -> + Optional.of(typeSystem.wrapBool(typeSystem.hasEqualKey(rhsTrans, lhsTrans)))) .build(); private InAxiom() {} diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 383bb8ba0..9853fb8d1 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -169,6 +169,10 @@ private enum IsSatisfiableTestCase { DYNAMIC_MAP_COMPREHENSION_EXISTS("string_int_map.exists(k, k == 'test')", "string_int_map = "), NULL_SATISFIABLE("unknown_var == null", "unknown_var = null"), DYNAMIC_VAR_NUMERIC_EQUALITY("dyn_var == 1 && dyn_var == 1.0", "dyn_var = 1"), + // Map equality compares values numerically, so an int value equals 1u. + MAP_LITERAL_LEFT_EQ_TYPED_MAP_ACROSS_NUMERIC_VALUES( + "{'a': 1u} == string_dyn_map && type(string_dyn_map['a']) == int", + "string_dyn_map = \\{\"a\": 1\\}"), DYNAMIC_VAR_UNSET_MESSAGE_FIELD( "dyn_var == TestAllTypes{} && dyn_var.single_string == ''", "dyn_var = "), ANY_NUMERIC_EQUALITY( @@ -802,6 +806,8 @@ private enum IsUnsatisfiableTestCase { TYPE_CONVERSION_UNSATISFIABLE_DOUBLE_TO_STRING("type(string(1.5)) == int"), 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"), 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"), @@ -999,7 +1005,8 @@ private enum IsAlwaysTrueTestCase { MEMBER_MAP_SIZE("{'a': 1, 'b': 2}.size() == 2"), MAP_LOOKUP_EQUALITY("!(x == y) || {x: 1, 'b': 2}[x] == {y: 1, 'b': 2}[y]"), MAP_INSERT_SIZE( - "dyn_map == {'a': 1, 'b': 2} ? size(dyn_map.transformMap(k, v, v > 1, v * 2)) == 1 : true"), + "dyn_map == {'a': 1, 'b': 2} && type(dyn_map['b']) == int ?" + + " size(dyn_map.transformMap(k, v, v > 1, v * 2)) == 1 : true"), UNSET_MAP_FIELD_SIZE("TestAllTypes{}.map_int64_int64.size() == 0"), STRING_CONTAINS_SELF("role.contains(role)"), STRING_STARTS_WITH_SELF("role.startsWith(role)"), @@ -1116,6 +1123,28 @@ 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{}"), + // 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}"), + MAP_LITERAL_NAN_VALUE_NEQ("{'a': 0.0 / 0.0} != {'a': 0.0 / 0.0}"), + MAP_LITERAL_EQ_ACROSS_NUMERIC_LIST_VALUES("dyn({'a': [1]}) == {'a': [1.0]}"), + MAP_LITERAL_EQ_ACROSS_NUMERIC_MAP_VALUES("dyn({'a': {1: 'x'}}) == {'a': {1u: 'x'}}"), + MAP_LITERAL_LEFT_EQ_ACROSS_NUMERIC_KEYS("{1u: 'a'} == dyn({1: 'a'})"), + MAP_LITERAL_WITH_ABSENT_OPTIONAL_ENTRY_EQ("{?'b': optional.none(), 'a': 1} == dyn({'a': 1.0})"), + MAP_LITERAL_WITH_VARIABLE_KEY_EQ("x == 1 ? {x: 1} == dyn({1u: 1.0}) : true"), + MAP_LITERAL_SIZE_NEQ("dyn({1: 'a'}) != {1u: 'a', 2: 'b'}"), + MAP_VARIABLE_EQ_LITERAL_ACROSS_NUMERIC_VALUES( + "string_int_map == {'a': 1} ? dyn(string_int_map) == {'a': 1.0} : true"), + IN_MAP_NUMERIC_KEYS("dyn(1.0) in {1: 'a'} && dyn(1u) in {1: 'a'} && !(dyn(1.5) in {1: 'a'})"), + IN_TYPED_MAP_NUMERIC_KEYS("!(dyn(1.0) in string_int_map) && !(dyn(1u) in string_int_map)"), + MAP_LITERAL_SINGLE_VARIABLE_KEY_LIST_VALUE("x == 1 ? {x: [1]} == dyn({1: [1.0]}) : true"), + MAP_LITERALS_PREFER_LIST_LITERAL_VALUES( + "int_list == [1] ? {'a': dyn(int_list)} == {'a': [1.0]} : true"), + MAP_EQ_LITERAL_ABSENT_KEY("dyn_var == {'a': 1} ? !('b' in dyn_var) : true"), + MAP_EQ_LITERAL_VALID_VALUE("x == -1 && dyn_var == {'a': x} ? dyn_var == {'a': -1} : true"), + 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"), // 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)" @@ -1220,6 +1249,7 @@ private enum IsAlwaysTrueTestCase { HETEROGENEOUS_INT_UINT_GE("2 >= 1u"), HETEROGENEOUS_UINT_INT_GE("2u >= 1"), HETEROGENEOUS_INT_DOUBLE_PRECISION("9007199254740993 > 9007199254740992.0"), + HETEROGENEOUS_NEGATIVE_INT_DOUBLE_PRECISION("-9007199254740993 < -9007199254740992.0"), HETEROGENEOUS_INT_EQ_DOUBLE( "type(dyn_var) == int && type(dyn_var2) == double && dyn_var == 1 && dyn_var2 == 1.0 ?" + " dyn_var == dyn_var2 : true"), @@ -1275,12 +1305,9 @@ private enum IsAlwaysTrueTestCase { + " dyn_var == dyn_var2 : true"), HETEROGENEOUS_DYNAMIC_ZERO("type(dyn_var) == double && dyn_var == -0.0 ? dyn_var == 0 : true"), HETEROGENEOUS_MAP_INT_KEY_DOUBLE_LOOKUP("{1: 'a'}[dyn(1.0)] == 'a'"), - HETEROGENEOUS_MAP_DOUBLE_KEY_INT_LOOKUP("{1.0: 'a'}[dyn(1)] == 'a'"), - HETEROGENEOUS_MAP_DOUBLE_KEY_UINT_LOOKUP("{1.0: 'a'}[dyn(1u)] == 'a'"), HETEROGENEOUS_MAP_UINT_KEY_DOUBLE_LOOKUP("{1u: 'a'}[dyn(1.0)] == 'a'"), HETEROGENEOUS_MAP_UINT_KEY_INT_LOOKUP_ZERO("{0u: 'a'}[dyn(0)] == 'a'"), HETEROGENEOUS_MAP_UINT_KEY_DOUBLE_LOOKUP_ZERO("{0u: 'a'}[dyn(0.0)] == 'a'"), - HETEROGENEOUS_MAP_DOUBLE_KEY_UINT_LOOKUP_ZERO("{0.0: 'a'}[dyn(0u)] == 'a'"), HETEROGENEOUS_MAP_INT_KEY_UINT_LOOKUP_ZERO("{0: 'a'}[dyn(0u)] == 'a'"), HETEROGENEOUS_MAP_PRECISION_MISS( "{9007199254740993: 'exact', 9007199254740992: 'rounded'}[dyn(9007199254740992.0)] ==" @@ -1324,8 +1351,8 @@ private enum IsAlwaysTrueTestCase { LITERAL_MAP_TRANSFORM_MAP_V2_FILTER( "{'a': 1, 'b': 2}.transformMap(k, v, v > 1, v * 2) == {'b': 4}"), TWO_VAR_HETEROGENEOUS_MAP( - "dyn_map == {'a': 1, 1: 'b'} ? dyn_map.exists(k, v, type(k) == string && type(v) == int &&" - + " k == 'a' && v == 1) : true"), + "dyn_map == {'a': 1, 1: 'b'} && type(dyn_map['a']) == int ? dyn_map.exists(k, v, type(k)" + + " == string && type(v) == int && k == 'a' && v == 1) : true"), TYPE_AXIOM_BOOL("type(true) == bool"), NULLABLE_INT_IS_NULL_OR_INT("type(nullable_int) == int || type(nullable_int) == null_type"), TYPE_AXIOM_INT("type(1) == int"), @@ -1350,8 +1377,8 @@ private enum IsAlwaysTrueTestCase { TYPE_AXIOM_OPTIONAL("type(optional.of(1)) == optional_type"), TYPE_AXIOM_STRUCT("type(TestAllTypes{}) == type(TestAllTypes{})"), TWO_VAR_TRANSFORM_MAP_DYNAMIC( - "dyn_map == {'a': 1, 'b': 2} ? dyn_map.transformMap(k, v, v > 1, v * 2) == {'b': 4} :" - + " true"), + "dyn_map == {'a': 1, 'b': 2} && type(dyn_map['b']) == int ? dyn_map.transformMap(k, v, v >" + + " 1, v * 2) == {'b': 4} : true"), NULL_EQ_NULL("null == null"), NULL_NEQ_DYN("request == 1 ? request != null : true"), TYPE_AXIOM_NULL("type(null) == null_type"), @@ -1532,9 +1559,9 @@ public void isAlwaysTrue_dynamicComprehensionNonBoolYieldsError() throws Excepti assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); assertThat(result.message()) - .isEqualTo( - "Condition is not always true. Counterexample input:\n" - + " dyn_list = [{\"not_a_bool\": 123}]"); + .matches( + "Condition is not always true\\. Counterexample input:\n" + + " dyn_list = \\[\\{\"not_a_bool\": 123(u|\\.0)?\\}\\]"); } @Test @@ -2063,12 +2090,6 @@ private enum IsAlwaysTrueViolationTestCase { "Condition is not always true\\.", "Counterexample input:", "dyn_map = \\{.*\\}"), - DYNAMIC_MAP_COMPREHENSION_NESTED_EQUALITY_VIOLATION( - "cel.bind(r, request, r.l == [[1], [2], [3], [4], [5]] && r.m == {1: [1], 2: [2]," - + " 3: [3]} ? r.l.all(x, r.m.exists(k, r.m[k] == x)) : true)", - "Condition is not always true\\.", - "Counterexample input:", - "request = .*"), UNINTERPRETED_EQUALITY_VIOLATION( "request == request", "Condition is not always true\\.", @@ -2161,7 +2182,7 @@ private enum IsAlwaysTrueViolationTestCase { "dyn_int_map != {1: 1} || (false && [dyn_int_map, string_dyn_map].exists(m, dyn(1) in m))", "Condition is not always true\\.", "Counterexample input:", - "dyn_int_map = \\{1: 1\\}"), + "dyn_int_map = \\{1u?: 1\\}"), CROSS_TYPE_POSITIVE_INT_EQUALS_DOUBLE("!(dyn(x) == d && x > 0)", "x = [1-9]\\d*", "d = [1-9]"), CROSS_TYPE_NEGATIVE_DOUBLE_BETWEEN_INTS( "!(x < 0 && x < d && d < x + 1)", "d = -\\d+\\.\\d*[1-9]"), @@ -2190,12 +2211,55 @@ public void isAlwaysTrue_violation_returnsFalse( } } + @Test + public void isAlwaysTrue_dynValuesComparedWithIntConstant_verified( + @TestParameter({ + "dyn_map == {'a': 1, 'b': 2} ? dyn_map.all(k, v, k == 'a' || v > 1) : true", + "dyn_map == {'a': 1, 'b': 2} ? dyn_map.all(k, v, k == 'b' || v < 2) : true" + }) + String expression) + throws Exception { + CelAbstractSyntaxTree ast = CEL.compile(expression).getAst(); + // A tighter timeout than the default, so that removing the fast path for comparing doubles with + // exact integer constants fails as a performance regression (~0.3 s with it, 19-45 s without). + CelVerifier verifier = withRuntimeOracle(CEL, b -> b.setTimeout(Duration.ofSeconds(5))); + + CelVerificationResult result = verifier.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void isAlwaysTrue_dynamicMapComprehensionNestedEquality_violated() throws Exception { + CelAbstractSyntaxTree ast = + CEL.compile( + "cel.bind(r, request, r.l == [[1], [2], [3], [4], [5]] && r.m == {1: [1], 2: [2]," + + " 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))); + + CelVerificationResult result = verifier.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.message()).contains("request = "); + } + private enum IsInconclusiveTestCase { // int('5') == 5 is approximate and may really be true, which absorbs the 1 / 0 error. APPROXIMATE_MATCH_BEFORE_ERROR( "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. + 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 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] +" + + " dyn(int_list)})"), // TODO: Implement RFC 3339 spec in conversion TIMESTAMP_STRING_CONVERSION_VALID( "timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"),