diff --git a/verifier/BUILD.bazel b/verifier/BUILD.bazel index cc2f01810..9ec441ed4 100644 --- a/verifier/BUILD.bazel +++ b/verifier/BUILD.bazel @@ -41,6 +41,13 @@ java_library( exports = ["//verifier/src/main/java/dev/cel/verifier:verifier_factory"], ) +java_library( + name = "numeric_bounds", + compatible_with = [], + visibility = [":verifier_internal"], + exports = ["//verifier/src/main/java/dev/cel/verifier:numeric_bounds"], +) + java_library( name = "type_system", compatible_with = [], diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index 4ca9794cc..ab341fba2 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel @@ -91,6 +91,19 @@ java_library( ], ) +java_library( + name = "numeric_bounds", + srcs = ["CelNumericBounds.java"], + compatible_with = [], + tags = [ + ], + deps = [ + "//:auto_value", + "//common/annotations", + "@maven//:com_google_guava_guava", + ], +) + java_library( name = "type_system", srcs = ["CelZ3TypeSystem.java"], @@ -98,6 +111,7 @@ java_library( tags = [ ], deps = [ + ":numeric_bounds", "//common/internal:proto_time_utils", "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:com_google_guava_guava", @@ -121,6 +135,7 @@ java_library( tags = [ ], deps = [ + ":numeric_bounds", ":type_system", ":verifier", "//:auto_value", diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java b/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java index c0491085f..a7e2be8b7 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java @@ -24,7 +24,9 @@ import dev.cel.common.ast.CelConstant; import dev.cel.common.ast.CelExpr; import java.util.ArrayList; +import java.util.HashMap; import java.util.List; +import java.util.Map; import org.jspecify.annotations.Nullable; /** @@ -83,16 +85,11 @@ private static void hashAst(CelExpr expr, @Nullable Scope scope, HasherContext c context.hasher.putByte((byte) 0); // 0 = bound context.hasher.putInt(bIdx); } else { - int fIdx = -1; - for (int i = 0; i < context.freeVars.size(); i++) { - if (context.freeVars.get(i).ident().name().equals(name)) { - fIdx = i; - break; - } - } - if (fIdx == -1) { + Integer fIdx = context.freeVarIndices.get(name); + if (fIdx == null) { context.freeVars.add(expr); fIdx = context.freeVars.size() - 1; + context.freeVarIndices.put(name, fIdx); } context.hasher.putByte((byte) 1); // 1 = free context.hasher.putInt(fIdx); @@ -100,12 +97,10 @@ private static void hashAst(CelExpr expr, @Nullable Scope scope, HasherContext c break; case SELECT: hashAst(expr.select().operand(), scope, context); - context.hasher.putInt(expr.select().field().length()); context.hasher.putString(expr.select().field(), UTF_8); context.hasher.putBoolean(expr.select().testOnly()); break; case CALL: - context.hasher.putInt(expr.call().function().length()); context.hasher.putString(expr.call().function(), UTF_8); context.hasher.putBoolean(expr.call().target().isPresent()); if (expr.call().target().isPresent()) { @@ -210,6 +205,7 @@ private static void hashConstant(CelConstant constant, HasherContext context) { private static final class HasherContext { final Hasher hasher; + final Map freeVarIndices = new HashMap<>(); final List freeVars = new ArrayList<>(); HasherContext(HashFunction hashFunction) { diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index e253b27ad..3964d68a1 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -1228,7 +1228,7 @@ private BoolExpr createTypeConstraint(Expr val, long exprId, CelAbstractSynta .orElseThrow( () -> new IllegalArgumentException("Type not found for expr ID: " + exprId)); BoolExpr typeConstraint = createTypeConstraintForType(val, type); - return ctx.mkOr(typeSystem.isError(val), typeSystem.isUnknown(val), typeConstraint); + return ctx.mkOr(typeSystem.isErrorOrUnknown(val), typeConstraint); } private BoolExpr createTypeConstraintForType(Expr val, CelType type) { @@ -1257,15 +1257,15 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { Expr unwrapped = ctx.mkApp(typeSystem.intCons().getAccessorDecls()[0], val); return ctx.mkAnd( ctx.mkApp(typeSystem.intCons().getTesterDecl(), val), - ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MIN_INT64)), - ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MAX_INT64))); + ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MIN_INT64)), + ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MAX_INT64))); } if (type.equals(SimpleType.UINT)) { Expr unwrapped = ctx.mkApp(typeSystem.uintCons().getAccessorDecls()[0], val); return ctx.mkAnd( ctx.mkApp(typeSystem.uintCons().getTesterDecl(), val), ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(0)), - ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MAX_UINT64))); + ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MAX_UINT64))); } if (type.equals(SimpleType.DOUBLE)) { return (BoolExpr) ctx.mkApp(typeSystem.doubleCons().getTesterDecl(), val); @@ -1351,7 +1351,10 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { BoolExpr validEntry = ctx.mkAnd(validIndex, presence); Expr mapVal = ctx.mkSelect(mapValues, key); - BoolExpr valNotError = ctx.mkNot(typeSystem.isError(mapVal)); + BoolExpr valNotError = + unknownIdentifiers.isEmpty() + ? ctx.mkNot(typeSystem.isErrorOrUnknown(mapVal)) + : ctx.mkNot(typeSystem.isError(mapVal)); boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError)); boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType))); } @@ -1409,6 +1412,12 @@ private Optional toCacheKey(CelExpr expr) { case CONSTANT: return Optional.of(expr.constant()); case LIST: + if (!expr.list().optionalIndices().isEmpty()) { + // Do not cache lists with optional elements. Optional elements conditionally alter + // sequence length and presence via ITE branches at runtime; caching would collide + // [1, 2] with [?1, 2] and freeze conditional evaluations to a static reference. + return Optional.empty(); + } ImmutableList.Builder builder = ImmutableList.builder(); for (CelExpr elem : expr.list().elements()) { Optional elemKey = toCacheKey(elem); diff --git a/verifier/src/main/java/dev/cel/verifier/CelNumericBounds.java b/verifier/src/main/java/dev/cel/verifier/CelNumericBounds.java new file mode 100644 index 000000000..8d2184c72 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CelNumericBounds.java @@ -0,0 +1,105 @@ +// Copyright 2026 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// https://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +package dev.cel.verifier; + +import com.google.auto.value.AutoValue; +import com.google.common.primitives.UnsignedLong; +import dev.cel.common.annotations.Internal; +import java.util.Optional; + +/** + * Utility for computing matching integer and unsigned integer ranges for IEEE-754 double-precision + * floating-point constants in Z3 verification. + */ +@Internal +public final class CelNumericBounds { + + /** Minimum representable signed 64-bit integer string. */ + public static final String MIN_INT64 = "-9223372036854775808"; + + /** Maximum representable signed 64-bit integer string. */ + public static final String MAX_INT64 = "9223372036854775807"; + + /** Maximum representable unsigned 64-bit integer string. */ + public static final String MAX_UINT64 = "18446744073709551615"; + + private static final double TWO_TO_63 = Math.scalb(1.0, 63); + private static final double TWO_TO_64 = Math.scalb(1.0, 64); + + @AutoValue + abstract static class IntRange { + abstract long min(); + + abstract long max(); + + static IntRange of(long min, long max) { + return new AutoValue_CelNumericBounds_IntRange(min, max); + } + } + + @AutoValue + abstract static class UintRange { + abstract String min(); + + abstract String max(); + + static UintRange of(String min, String max) { + return new AutoValue_CelNumericBounds_UintRange(min, max); + } + } + + private static boolean isMathematicalInteger(double vDouble) { + return Double.isFinite(vDouble) && vDouble == Math.rint(vDouble); + } + + static Optional getMatchingIntRange(double vDouble) { + if (!isMathematicalInteger(vDouble) || vDouble < -TWO_TO_63 || vDouble > TWO_TO_63) { + return Optional.empty(); + } + long minL = (long) vDouble; + while (minL > Long.MIN_VALUE && (double) (minL - 1) == vDouble) { + minL--; + } + long maxL = (long) vDouble; + while (maxL < Long.MAX_VALUE && (double) (maxL + 1) == vDouble) { + maxL++; + } + return Optional.of(IntRange.of(minL, maxL)); + } + + static Optional getMatchingUintRange(double vDouble) { + if (!isMathematicalInteger(vDouble) || vDouble < 0 || vDouble > TWO_TO_64) { + return Optional.empty(); + } + // XOR with Long.MIN_VALUE (0x8000000000000000L) flips bit 63 to 1, encoding unsigned values + // >= 2^63 into Java's two's-complement signed long representation. + long uBits = + vDouble < TWO_TO_63 ? (long) vDouble : (long) (vDouble - TWO_TO_63) ^ Long.MIN_VALUE; + UnsignedLong uVal = UnsignedLong.fromLongBits(uBits); + UnsignedLong minU = uVal; + while (!minU.equals(UnsignedLong.ZERO) + && minU.minus(UnsignedLong.ONE).doubleValue() == vDouble) { + minU = minU.minus(UnsignedLong.ONE); + } + UnsignedLong maxU = uVal; + while (!maxU.equals(UnsignedLong.MAX_VALUE) + && maxU.plus(UnsignedLong.ONE).doubleValue() == vDouble) { + maxU = maxU.plus(UnsignedLong.ONE); + } + return Optional.of(UintRange.of(minU.toString(), maxU.toString())); + } + + private CelNumericBounds() {} +} diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index 104e224a6..6e5c519fe 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -24,14 +24,17 @@ import com.microsoft.z3.Model; import com.microsoft.z3.RatNum; import java.util.ArrayList; +import java.util.HashSet; +import java.util.LinkedHashSet; import java.util.List; +import java.util.Set; import org.jspecify.annotations.Nullable; /** Generates human-readable counterexample strings from Z3 models. */ @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types. final class CelZ3CounterexampleGenerator { - private static final int MAX_LIST_ELEMENTS_TO_PRINT = 15; + private static final int MAX_ELEMENTS_TO_PRINT = 15; private CelZ3CounterexampleGenerator() {} @@ -158,8 +161,10 @@ private static String reconstructList( model, ctx.mkLength(typeSystem.getSeq(listRef)), String.format("Z3 failed to evaluate length for list %s", listRef)); - int length = ((IntNum) lenExpr).getInt(); - int printLimit = Math.min(length, MAX_LIST_ELEMENTS_TO_PRINT); + Preconditions.checkState( + lenExpr instanceof IntNum, "Expected IntNum length for list %s, got %s", listRef, lenExpr); + long length = ((IntNum) lenExpr).getInt64(); + int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT); List elements = new ArrayList<>(); for (int i = 0; i < printLimit; i++) { Expr elem = @@ -179,36 +184,33 @@ private static String reconstructList( private static String reconstructMap( Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr mapRef) { - List> keys = new ArrayList<>(); Expr lenExpr = evaluateStrict( model, ctx.mkLength(typeSystem.getMapKeys(mapRef)), String.format("Z3 failed to evaluate length for map %s", mapRef)); - if (lenExpr instanceof IntNum) { - int length = ((IntNum) lenExpr).getInt(); - int printLimit = Math.min(length, 100); - for (int i = 0; i < printLimit; i++) { - Expr elem = - evaluateStrict( - model, - ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i)), - String.format("Z3 failed to evaluate map key at index %d for map %s", i, mapRef)); - if (!keys.contains(elem)) { - keys.add(elem); - } - } - } + Preconditions.checkState( + lenExpr instanceof IntNum, "Expected IntNum length for map %s, got %s", mapRef, lenExpr); + long length = ((IntNum) lenExpr).getInt64(); + int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT); List entries = new ArrayList<>(); - for (Expr key : keys) { + Set> seenKeys = new HashSet<>(); + for (int i = 0; i < printLimit; i++) { + Expr key = + evaluateStrict( + model, + ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i)), + String.format("Z3 failed to evaluate map key at index %d for map %s", i, mapRef)); + if (!seenKeys.add(key)) { + continue; + } Expr presence = evaluateStrict( model, ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), key), String.format( "Z3 failed to evaluate map presence for key %s in map %s", key, mapRef)); - if (presence.isTrue()) { Expr value = evaluateStrict( @@ -221,6 +223,9 @@ private static String reconstructMap( + formatExpr(ctx, typeSystem, model, value)); } } + if (length > printLimit) { + entries.add("... (" + (length - printLimit) + " more entries)"); + } return "{" + String.join(", ", entries) + "}"; } @@ -241,7 +246,7 @@ private static String reconstructMessage( String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", ""); - List> keys = new ArrayList<>(); + Set> keys = new LinkedHashSet<>(); extractKeys(presenceArray, keys); List entries = new ArrayList<>(); @@ -268,7 +273,7 @@ private static String reconstructMessage( return typeName + "{" + String.join(", ", entries) + "}"; } - private static void extractKeys(Expr arrayExpr, List> keys) { + private static void extractKeys(Expr arrayExpr, Set> keys) { int iterations = 0; while (true) { if (++iterations > 100_000) { @@ -284,9 +289,7 @@ private static void extractKeys(Expr arrayExpr, List> keys) { Expr[] args = arrayExpr.getArgs(); Preconditions.checkState( args.length == 3, "Z3 store array operation must have exactly 3 arguments"); - if (!keys.contains(args[1])) { - keys.add(args[1]); - } + keys.add(args[1]); arrayExpr = args[0]; continue; } diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3ExtensionalityAxioms.java b/verifier/src/main/java/dev/cel/verifier/CelZ3ExtensionalityAxioms.java index 2303abcaf..be1ec1475 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3ExtensionalityAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3ExtensionalityAxioms.java @@ -79,7 +79,8 @@ private static void addListAxioms( Sort listRefSort = typeSystem.listRefSort(); Sort seqSort = ctx.mkSeqSort(typeSystem.celValueSort()); - FuncDecl mkListRef = ctx.mkFuncDecl(FUNC_MK_LIST_REF, new Sort[] {seqSort}, listRefSort); + FuncDecl mkListRef = + typeSystem.internFuncDecl(FUNC_MK_LIST_REF, new Sort[] {seqSort}, listRefSort); for (Expr ref : refs) { if (isAppOf(ref, FUNC_MK_LIST_REF)) { @@ -109,7 +110,8 @@ private static void addMapAxioms( Sort presenceSort = ctx.mkArraySort(typeSystem.celValueSort(), ctx.getBoolSort()); FuncDecl mkMapRef = - ctx.mkFuncDecl(FUNC_MK_MAP_REF, new Sort[] {valuesSort, presenceSort}, mapRefSort); + typeSystem.internFuncDecl( + FUNC_MK_MAP_REF, new Sort[] {valuesSort, presenceSort}, mapRefSort); for (Expr ref : refs) { if (isAppOf(ref, FUNC_MK_MAP_REF)) { @@ -141,7 +143,7 @@ private static void addMessageAxioms( Sort presenceSort = ctx.mkArraySort(ctx.getStringSort(), ctx.getBoolSort()); FuncDecl mkMsgRef = - ctx.mkFuncDecl( + typeSystem.internFuncDecl( FUNC_MK_MSG_REF, new Sort[] {typeNameSort, valuesSort, presenceSort}, msgRefSort); for (Expr ref : refs) { diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index 3051fbd87..bd5c8874e 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -43,7 +43,6 @@ import dev.cel.common.types.SimpleType; import dev.cel.verifier.axioms.CelZ3OverloadResult; import dev.cel.verifier.axioms.CelZ3OverloadTranslator; -import java.math.BigDecimal; import java.util.ArrayList; import java.util.List; import java.util.Optional; @@ -224,6 +223,8 @@ private TranslatedValue translateOperatorCall( return translateLogicalAndOr(args, false); case LOGICAL_NOT: return translateLogicalNot(args, ast); + case NEGATE: + return translateNegate(args.get(0), ast); case EQUALS: return translateEquality(args.get(0), args.get(1), ast, /* isEquals= */ true); case NOT_EQUALS: @@ -237,7 +238,6 @@ private TranslatedValue translateOperatorCall( case MULTIPLY: case DIVIDE: case MODULO: - case NEGATE: case IN: // Indicates a type-mismatch in an operator that's not handled // by our axioms @@ -330,72 +330,84 @@ private TranslatedValue translateLogicalNot( return TranslatedValue.propagateStrict(ctx, typeSystem, baseResult, args); } + private TranslatedValue translateNegate(TranslatedValue arg, CelAbstractSyntaxTree ast) { + CelType type = extractAstTypeOrDefault(arg, ast); + Expr z3Expr = arg.z3Expr(); + + Expr result; + if (type.equals(SimpleType.INT)) { + ArithExpr intNeg = ctx.mkUnaryMinus(typeSystem.getInt(z3Expr)); + result = + typeSystem.withRuntimeError( + typeSystem.wrapInt((IntExpr) intNeg), typeSystem.checkIntOverflow(intNeg)); + } else if (type.equals(SimpleType.DOUBLE)) { + result = typeSystem.wrapDouble(ctx.mkFPNeg(typeSystem.getDouble(z3Expr))); + } else { + ArithExpr intNeg = ctx.mkUnaryMinus(typeSystem.getInt(z3Expr)); + Expr intResult = + typeSystem.withRuntimeError( + typeSystem.wrapInt((IntExpr) intNeg), typeSystem.checkIntOverflow(intNeg)); + Expr doubleResult = typeSystem.wrapDouble(ctx.mkFPNeg(typeSystem.getDouble(z3Expr))); + result = + CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + .addCase(typeSystem.isInt(z3Expr), intResult) + .addCase(typeSystem.isDouble(z3Expr), doubleResult) + .build(typeSystem.mkError()); + } + return TranslatedValue.propagateStrict(ctx, typeSystem, result, arg); + } + private BoolExpr isNumeric(Expr arg) { return ctx.mkOr(typeSystem.isInt(arg), typeSystem.isUint(arg), typeSystem.isDouble(arg)); } private BoolExpr getNumericEqualityWithConstant( Expr symVal, CelConstant constant, CelType symType) { - Long intVal = null; - String uintVal = null; + Optional intRange = Optional.empty(); + Optional uintRange = Optional.empty(); double doubleVal; switch (constant.getKind()) { case INT64_VALUE: long vInt = constant.int64Value(); - intVal = vInt; - // Z3's infinite precision automatically evaluates `uint == -1` to false, - // but pruning it here keeps the formula smaller. + intRange = Optional.of(CelNumericBounds.IntRange.of(vInt, vInt)); if (vInt >= 0) { - uintVal = Long.toString(vInt); + uintRange = + Optional.of(CelNumericBounds.UintRange.of(Long.toString(vInt), Long.toString(vInt))); } doubleVal = (double) vInt; break; case UINT64_VALUE: long vUint = constant.uint64Value().longValue(); if (vUint >= 0) { - intVal = vUint; + intRange = Optional.of(CelNumericBounds.IntRange.of(vUint, vUint)); } - uintVal = constant.uint64Value().toString(); + String uStr = constant.uint64Value().toString(); + uintRange = Optional.of(CelNumericBounds.UintRange.of(uStr, uStr)); doubleVal = constant.uint64Value().doubleValue(); break; case DOUBLE_VALUE: double vDouble = constant.doubleValue(); doubleVal = vDouble; - if (vDouble == Math.floor(vDouble) && !Double.isInfinite(vDouble)) { - if (vDouble >= Long.MIN_VALUE && vDouble <= Long.MAX_VALUE) { - intVal = (long) vDouble; - } - if (vDouble >= 0 && vDouble <= Double.parseDouble(CelZ3TypeSystem.MAX_UINT64)) { - uintVal = BigDecimal.valueOf(vDouble).toBigInteger().toString(); - } - } + intRange = CelNumericBounds.getMatchingIntRange(vDouble); + uintRange = CelNumericBounds.getMatchingUintRange(vDouble); break; default: throw new IllegalArgumentException( "Unexpected numeric constant kind: " + constant.getKind()); } - if (isStaticallyKnown(symType)) { if (symType.kind() == CelKind.INT) { - return (intVal != null) - ? ctx.mkEq(typeSystem.getInt(symVal), ctx.mkInt(intVal)) - : ctx.mkFalse(); + return buildIntRangeExpr(intRange, typeSystem.getInt(symVal)); } else if (symType.kind() == CelKind.UINT) { - return (uintVal != null) - ? ctx.mkEq(typeSystem.getUint(symVal), ctx.mkInt(uintVal)) - : ctx.mkFalse(); + return buildUintRangeExpr(uintRange, typeSystem.getUint(symVal)); } else if (symType.kind() == CelKind.DOUBLE) { return ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); } } - BoolExpr intEq = - (intVal != null) ? ctx.mkEq(typeSystem.getInt(symVal), ctx.mkInt(intVal)) : ctx.mkFalse(); - BoolExpr uintEq = - (uintVal != null) - ? ctx.mkEq(typeSystem.getUint(symVal), ctx.mkInt(uintVal)) - : ctx.mkFalse(); + BoolExpr intEq = buildIntRangeExpr(intRange, typeSystem.getInt(symVal)); + BoolExpr uintEq = buildUintRangeExpr(uintRange, typeSystem.getUint(symVal)); BoolExpr doubleEq = ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); return (BoolExpr) @@ -406,6 +418,27 @@ private BoolExpr getNumericEqualityWithConstant( .build(ctx.mkFalse()); } + private BoolExpr buildIntRangeExpr(Optional rangeOpt, IntExpr symInt) { + return rangeOpt + .map(range -> buildIntRangeExpr(range.min(), range.max(), symInt)) + .orElseGet(ctx::mkFalse); + } + + private BoolExpr buildIntRangeExpr(long min, long max, IntExpr symInt) { + return ctx.mkAnd(ctx.mkGe(symInt, ctx.mkInt(min)), ctx.mkLe(symInt, ctx.mkInt(max))); + } + + private BoolExpr buildUintRangeExpr( + Optional rangeOpt, IntExpr symUint) { + return rangeOpt + .map(range -> buildUintRangeExpr(range.min(), range.max(), symUint)) + .orElseGet(ctx::mkFalse); + } + + private BoolExpr buildUintRangeExpr(String min, String max, IntExpr symUint) { + return ctx.mkAnd(ctx.mkGe(symUint, ctx.mkInt(min)), ctx.mkLe(symUint, ctx.mkInt(max))); + } + private BoolExpr getNumericEquality( TranslatedValue arg0, TranslatedValue arg1, CelAbstractSyntaxTree ast) { if (arg0.isNumericConstant()) { @@ -418,7 +451,7 @@ private BoolExpr getNumericEquality( CelType type0 = extractAstTypeOrDefault(arg0, ast); CelType type1 = extractAstTypeOrDefault(arg1, ast); - if (isStaticallyKnown(type0) && isStaticallyKnown(type1)) { + if (isStaticallyKnown(type0) && isStaticallyKnown(type1) && type0.kind() == type1.kind()) { return getStaticallyKnownNumericEquality(arg0.z3Expr(), type0, arg1.z3Expr()); } @@ -733,7 +766,7 @@ private Expr buildMapIndex( // Uint probes IntExpr rawUint = (IntExpr) ctx.mkITE(isUint, typeSystem.getUint(rhsTrans), ctx.mkInt(0)); - BoolExpr uintHasInt = ctx.mkLe(rawUint, ctx.mkInt(CelZ3TypeSystem.MAX_INT64)); + BoolExpr uintHasInt = ctx.mkLe(rawUint, ctx.mkInt(CelNumericBounds.MAX_INT64)); Expr uintIntKey = typeSystem.wrapInt(rawUint); BoolExpr uintHasDouble = hasExactDouble ? isUint : ctx.mkFalse(); diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index 1c1435e3b..dc19a8d3a 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -55,10 +55,6 @@ @SuppressWarnings({"unchecked", "rawtypes", "AvoidObjectArrays"}) // Z3 Java API uses raw types. public final class CelZ3TypeSystem { - public static final String MIN_INT64 = "-9223372036854775808"; - public static final String MAX_INT64 = "9223372036854775807"; - public static final String MAX_UINT64 = "18446744073709551615"; - private static final String TYPE_CEL_VALUE = "CelValue"; private static final String CONS_BOOL = "Bool"; private static final String IS_BOOL = "isBool"; @@ -357,7 +353,7 @@ public Expr wrapDuration(IntExpr expr) { /** Creates a CelValue containing an integer. */ public Expr mkInt(long val) { - return ctx.mkApp(intCons.ConstructorDecl(), ctx.mkInt(val)); + return ctx.mkApp(intCons.ConstructorDecl(), ctx.mkInt(Long.toString(val))); } /** Creates a CelValue containing an unsigned integer from a string representation. */ @@ -575,6 +571,11 @@ public BoolExpr isUnknown(Expr val) { return (BoolExpr) ctx.mkApp(unknownCons.getTesterDecl(), val); } + /** Checks if the given CelValue is either an error or an unknown value. */ + public BoolExpr isErrorOrUnknown(Expr val) { + return ctx.mkOr(isError(val), isUnknown(val)); + } + /** Checks if the given CelValue is a boolean. */ public BoolExpr isBool(Expr val) { return (BoolExpr) ctx.mkApp(boolCons.getTesterDecl(), val); @@ -804,7 +805,9 @@ public Expr getMsgTypeName(Expr msgRef) { /** Checks if the given arithmetic expression overflows a 64-bit integer. */ public BoolExpr checkIntOverflow(ArithExpr result) { - return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_INT64)), ctx.mkLt(result, ctx.mkInt(MIN_INT64))); + return ctx.mkOr( + ctx.mkGt(result, ctx.mkInt(CelNumericBounds.MAX_INT64)), + ctx.mkLt(result, ctx.mkInt(CelNumericBounds.MIN_INT64))); } /** Checks if the given arithmetic expression overflows CEL Timestamp bounds. */ @@ -823,7 +826,8 @@ public BoolExpr checkDurationOverflow(ArithExpr result) { /** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */ public BoolExpr checkUintOverflow(ArithExpr result) { - return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_UINT64)), ctx.mkLt(result, ctx.mkInt(0))); + return ctx.mkOr( + ctx.mkGt(result, ctx.mkInt(CelNumericBounds.MAX_UINT64)), ctx.mkLt(result, ctx.mkInt(0))); } /** Safely concatenates two Z3 sequences. */ diff --git a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java index 032c9dcdc..506f0bbc7 100644 --- a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java +++ b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java @@ -144,7 +144,6 @@ static TranslatedValue propagateStrict( Collection args) { List exactErrors = new ArrayList<>(); List exactUnknowns = new ArrayList<>(); - List errors = new ArrayList<>(); List unknowns = new ArrayList<>(); List taints = new ArrayList<>(); taints.add(baseTaint); @@ -164,7 +163,6 @@ static TranslatedValue propagateStrict( BoolExpr isError = ts.isError(z3Expr); BoolExpr isUnknown = ts.isUnknown(z3Expr); - errors.add(isError); unknowns.add(isUnknown); exactErrors.add( @@ -180,17 +178,18 @@ static TranslatedValue propagateStrict( return create(baseResult, celExpr, ts, anyTaint); } + List> z3Args = new ArrayList<>(); + for (TranslatedValue arg : argsList) { + if (!arg.isLiteral(ExprKind.Kind.CONSTANT)) { + z3Args.add(arg.z3Expr()); + } + } + Expr finalResult = ts.propagateErrorAndUnknown(baseResult, z3Args); + BoolExpr hasExactError = CelZ3TypeSystem.mkOrFlattened(ctx, exactErrors); BoolExpr hasExactUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, exactUnknowns); - BoolExpr hasError = CelZ3TypeSystem.mkOrFlattened(ctx, errors); BoolExpr hasUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, unknowns); - Expr finalResult = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase(hasUnknown, ts.mkUnknown()) - .addCase(hasError, ts.mkError()) - .build(baseResult); - BoolExpr isSafe = CelZ3TypeSystem.mkOrFlattened( ctx, diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel index 02752c10e..c397f1b45 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel @@ -22,6 +22,7 @@ java_library( "//common/types", "//extensions:comprehensions", "//extensions:optional_library", + "//verifier:numeric_bounds", "//verifier:type_system", "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:com_google_guava_guava", diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java index 9c49ef958..61e941258 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java @@ -47,7 +47,7 @@ final class TypeAxiom { // Custom approximation logic for type(): it is only approximate if the argument // is approximate AND the argument is an Error or Unknown. - BoolExpr isErrOrUnk = ctx.mkOr(typeSystem.isError(val), typeSystem.isUnknown(val)); + BoolExpr isErrOrUnk = typeSystem.isErrorOrUnknown(val); BoolExpr typeApprox = ctx.mkAnd(argApprox, isErrOrUnk); return Optional.of(CelZ3OverloadResult.create(result, typeApprox)); diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java index f4dba5afc..2064047fd 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java @@ -14,7 +14,7 @@ package dev.cel.verifier.axioms; -import static dev.cel.verifier.CelZ3TypeSystem.MAX_INT64; +import static dev.cel.verifier.CelNumericBounds.MAX_INT64; import com.google.common.collect.ImmutableList; import com.microsoft.z3.BoolExpr; diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java index 25354480a..94348ff15 100644 --- a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java @@ -50,7 +50,11 @@ static int runInteractiveRepl() { BufferedReader fallbackReader = null; try { Terminal terminal = TerminalBuilder.builder().system(true).build(); - lineReader = LineReaderBuilder.builder().terminal(terminal).build(); + lineReader = + LineReaderBuilder.builder() + .terminal(terminal) + .option(LineReader.Option.DISABLE_EVENT_EXPANSION, true) + .build(); } catch (Exception e) { fallbackReader = new BufferedReader(new InputStreamReader(System.in, UTF_8)); } diff --git a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel index 6bf44cafd..f1669c486 100644 --- a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel @@ -47,13 +47,13 @@ java_library( "//:java_truth", "@maven//:tools_aqua_z3_turnkey", "//verifier", + "//verifier:numeric_bounds", "//verifier:policy_verifier", "//verifier:policy_verifier_factory", "//verifier:type_system", "//verifier:verifier_factory", "//verifier:z3_impl", "//verifier/axioms", - "//verifier/tools", "@cel_spec//proto/cel/expr/conformance/proto3:test_all_types_java_proto", "@maven//:com_google_guava_guava", ], diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 696a21387..cea14e910 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -139,25 +139,25 @@ public void setUp() { } private enum IsSatisfiableTestCase { - SATISFIABLE("x > 5"), - DYNAMIC_ARITHMETIC("request == 1 && request + 2 == 3"), - DYNAMIC_ARITHMETIC_UNARY("request == 1 && -request == -1"), - GREATER_DOUBLE("d > 1.5"), - LESS_EQUALS_UINT64("u <= 5u"), - LESS_EQUALS_DOUBLE("d <= 5.5"), - LESS_EQUALS_STRING("role <= 'admin'"), - LESS_EQUALS_BYTES("by <= b'bytes'"), - GREATER_STRING("role > 'admin'"), - GREATER_BYTES("by > b'bytes'"), - DYNAMIC_LIST_COMPREHENSION_EXISTS("int_list.exists(x, x > 5)"), - DYNAMIC_MAP_COMPREHENSION_EXISTS("string_int_map.exists(k, k == 'test')"), - NULL_SATISFIABLE("unknown_var == null"), - DYNAMIC_VAR_NUMERIC_EQUALITY("dyn_var == 1 && dyn_var == 1.0"), - DYNAMIC_VAR_NOT_IN_LIST("dyn_var == 1.5 && !(dyn_var in dyn_list) && size(dyn_list) > 5"), - CROSS_NUMERIC_EQUALITY_INT_DYN_EXACT("1 == request"), - MACRO_LIMIT("dyn_list.all(x, x == 1)"), - STRUCT_FIELD_MISSING_APPROXIMATE_SATISFIABLE("dyn_var.unknown_field"), - NULLABLE_INT_SATISFIABLE("nullable_int == 123"), + SATISFIABLE("x > 5", "x = (?:[6-9]|[1-9]\\d+)"), + DYNAMIC_ARITHMETIC("request == 1 && request + 2 == 3", "request = 1"), + DYNAMIC_ARITHMETIC_UNARY("request == 1 && -request == -1", "request = 1"), + GREATER_DOUBLE("d > 1.5", "d = "), + LESS_EQUALS_UINT64("u <= 5u", "u = [0-5]u"), + LESS_EQUALS_DOUBLE("d <= 5.5", "d = "), + LESS_EQUALS_STRING("role <= 'admin'", "role = "), + LESS_EQUALS_BYTES("by <= b'bytes'", "by = "), + GREATER_STRING("role > 'admin'", "role = "), + GREATER_BYTES("by > b'bytes'", "by = "), + DYNAMIC_LIST_COMPREHENSION_EXISTS("int_list.exists(x, x > 5)", "int_list = "), + 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"), + DYNAMIC_VAR_NOT_IN_LIST( + "dyn_var == 1.5 && !(dyn_var in dyn_list) && size(dyn_list) > 5", "dyn_var = 1\\.5"), + CROSS_NUMERIC_EQUALITY_INT_DYN_EXACT("1 == request", "request = 1"), + MACRO_LIMIT("dyn_list.all(x, x == 1)", "Satisfying input:"), + STRUCT_FIELD_MISSING_APPROXIMATE_SATISFIABLE("dyn_var.unknown_field", "dyn_var = "), MAP_INDEX_SATISFIABLE("string_int_map['alice'] > 0", "\"alice\": [1-9]\\d*"), MAP_SIZE_GREATER_THAN_ONE_WITH_KEY( "string_int_map.size() > 1 && string_int_map['foo'] == 42", @@ -165,6 +165,25 @@ private enum IsSatisfiableTestCase { MAP_SIZE_GREATER_THAN_ONE_WITH_LIST_ELEMENT( "string_int_map.size() > 1 && string_int_map['a'] == int_list[0] && int_list.size() == 1", "string_int_map = \\{[^}]*,[^}]*\\}"), + DISTINCT_TRUNCATED_COMPREHENSIONS( + "dyn_list.all(x, x == 1) != dyn_list.all(x, x == 2)", "dyn_list = "), + DISTINCT_TRUNCATED_COMPREHENSIONS_FREE_VARS( + "dyn_list.all(e, x == x) != dyn_list.all(e, x == y)", "dyn_list = "), + DISTINCT_TRUNCATED_COMPREHENSIONS_STRUCTS( + "dyn_list.all(e, e == TestAllTypes{single_int64: 1}) !=" + + " dyn_list.all(e, e == TestAllTypes{single_int32: 1})", + "dyn_list = "), + DISTINCT_TRUNCATED_COMPREHENSIONS_STRUCT_MESSAGE_NAMES( + "dyn_list.all(e, e == TestAllTypes{single_int64: 1}) !=" + + " dyn_list.all(e, e == TestAllTypes.NestedMessage{bb: 1})", + "dyn_list = "), + MAP_SIZE_GREATER_THAN_CONSTRAINED_KEYS( + "string_int_map.size() == 5 && string_int_map['a'] == 10", "\"a\": 10"), + INT_MIN_DOUBLE_EQUALITY( + "dyn(request) == -9223372036854775808.0", "request = -9223372036854775[2-8]\\d+"), + INT_MAX_DOUBLE_EQUALITY( + "dyn(request) == 9223372036854775808.0", "request = 9223372036854775[2-8]\\d+"), + UINT_MAX_DOUBLE_EQUALITY("dyn(u) == 18446744073709551616.0", "u = 1844674407370955\\d+u"), ; final String expr; @@ -259,6 +278,18 @@ public void counterexample_nullValueFormattedAsNull() throws Exception { assertThat(result.message()).contains("request = null"); } + @Test + public void counterexample_mapFormattedCorrectly() throws Exception { + CelAbstractSyntaxTree ast = + CEL.compile("string_int_map.size() == 2 && string_int_map['a'] == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).containsMatch("string_int_map = \\{[^}]*,[^}]*\\}"); + assertThat(result.message()).contains("\"a\": 1"); + } + private enum CounterexampleNeverErrorTestCase { DYN_LIST_REFLEXIVITY("dyn_list.size() == 1 ? dyn_list[0] == dyn_list[0] : true"), DYN_MAP_REFLEXIVITY("dyn_map.size() == 1 ? dyn_map[1] == dyn_map[1] : true"), @@ -400,6 +431,15 @@ private enum IsUnsatisfiableTestCase { + " string_int_map.size() == 2"), EMPTY_MAP_KEY_LOOKUP("string_int_map['a'] > 100 && string_int_map.size() == 0"), EMPTY_MAP_DYNAMIC_KEY_LOOKUP("string_int_map[string_var] == 100 && string_int_map.size() == 0"), + INT_NON_INTEGER_DOUBLE_EQUALITY("dyn(x) == 1.5"), + INT_OUT_OF_BOUNDS_POS_DOUBLE_EQUALITY("dyn(x) == 9223372036854777856.0"), + INT_OUT_OF_BOUNDS_NEG_DOUBLE_EQUALITY("dyn(x) == -9223372036854777856.0"), + UINT_NEGATIVE_DOUBLE_EQUALITY("dyn(u) == -1.0"), + UINT_NON_INTEGER_DOUBLE_EQUALITY("dyn(u) == 1.5"), + UINT_OUT_OF_BOUNDS_POS_DOUBLE_EQUALITY("dyn(u) == 18446744073709555712.0"), + INT_OUT_OF_BOUNDS_LARGE_DOUBLE_EQUALITY("dyn(x) == 1e100"), + INT_OUT_OF_BOUNDS_LARGE_NEG_DOUBLE_EQUALITY("dyn(x) == -1e100"), + UINT_OUT_OF_BOUNDS_LARGE_DOUBLE_EQUALITY("dyn(u) == 1e100"), ; final String expr; @@ -518,7 +558,7 @@ private enum IsAlwaysTrueTestCase { "{'a': x, 'b': y}.all(z, {'a': x, 'b': y}.exists(z, z == 'a' || z == 'b'))"), MAP_LITERAL_VARIABLE_VALUE("{'a': x}['a'] == x"), HETEROGENEOUS_LARGE_UINT_INT_VARIABLE_NEQ( - "unknown_var == " + CelZ3TypeSystem.MAX_UINT64 + "u ? unknown_var != -1 : true"), + "unknown_var == " + CelNumericBounds.MAX_UINT64 + "u ? unknown_var != -1 : true"), MAP_LITERAL_VARIABLE_KEY("x != y ? {x: 1, y: 2}[x] == 1 : true"), MAP_MACRO_LIST_RETURN("{'a': 1, 'b': 2}.map(x, x + 'a') == ['aa', 'ba']"), MAP_LITERAL_NESTED_LIST("{'a': [1, 2]} == {'a': [1, 2]}"), @@ -695,12 +735,27 @@ private enum IsAlwaysTrueTestCase { "unknown_var == 9223372036854775807 ? unknown_var != 1e100 : true"), HETEROGENEOUS_MAX_EXACT_INT("dyn(9007199254740992) == 9007199254740992.0"), HETEROGENEOUS_MIN_EXACT_INT("dyn(-9007199254740992) == -9007199254740992.0"), - HETEROGENEOUS_INT_PRECISION_LOSS_POS("dyn(9007199254740993) != 9007199254740992.0"), - HETEROGENEOUS_INT_PRECISION_LOSS_NEG("dyn(-9007199254740993) != -9007199254740992.0"), - HETEROGENEOUS_UINT_PRECISION_LOSS("dyn(9007199254740993u) != 9007199254740992.0"), + HETEROGENEOUS_INT_PRECISION_LOSS_POS("dyn(9007199254740993) == 9007199254740992.0"), + HETEROGENEOUS_INT_PRECISION_LOSS_NEG("dyn(-9007199254740993) == -9007199254740992.0"), + HETEROGENEOUS_UINT_PRECISION_LOSS("dyn(9007199254740993u) == 9007199254740992.0"), HETEROGENEOUS_LONG_MAX_VS_DOUBLE("dyn(9223372036854775807) == 9223372036854775808.0"), - HETEROGENEOUS_LONG_MIN_VS_DOUBLE("dyn(-9223372036854775808) == -9223372036854775808.0"), - HETEROGENEOUS_UINT_MAX_VS_DOUBLE("dyn(18446744073709551615u) != 18446744073709551616.0"), + HETEROGENEOUS_STATIC_INT_DOUBLE_EQ("dyn(1) == 1.0"), + HETEROGENEOUS_STATIC_UINT_DOUBLE_EQ("dyn(1u) == 1.0"), + HETEROGENEOUS_STATIC_INT_UINT_EQ("dyn(1) == 1u"), + HETEROGENEOUS_LONG_MIN_VS_DOUBLE( + "dyn_var == -9223372036854775808.0 ? dyn_var == -9223372036854775808.0 : true"), + HETEROGENEOUS_UINT_MAX_VS_DOUBLE("dyn(18446744073709551615u) == 18446744073709551616.0"), + HETEROGENEOUS_UINT_OVERFLOW_VS_DOUBLE("dyn_var == 1e100 ? type(dyn_var) != uint : true"), + HETEROGENEOUS_UINT_NEG_VS_DOUBLE("dyn_var == -1.0 ? type(dyn_var) != uint : true"), + HETEROGENEOUS_INT_OVERFLOW_VS_DOUBLE("dyn_var == 1e100 ? type(dyn_var) != int : true"), + HETEROGENEOUS_INT_UNDERFLOW_VS_DOUBLE( + "dyn_var == -9223372036854777856.0 ? type(dyn_var) != int : true"), + HETEROGENEOUS_INT_NON_INTEGER_DOUBLE_INEQUALITY("dyn(x) != 1.5"), + HETEROGENEOUS_INT_OUT_OF_BOUNDS_POS_DOUBLE_INEQUALITY("dyn(x) != 9223372036854777856.0"), + HETEROGENEOUS_INT_OUT_OF_BOUNDS_NEG_DOUBLE_INEQUALITY("dyn(x) != -9223372036854777856.0"), + HETEROGENEOUS_UINT_NON_INTEGER_DOUBLE_INEQUALITY("dyn(u) != 1.5"), + HETEROGENEOUS_UINT_OUT_OF_BOUNDS_POS_DOUBLE_INEQUALITY("dyn(u) != 18446744073709555712.0"), + HETEROGENEOUS_UINT_OUT_OF_BOUNDS_NEG_DOUBLE_INEQUALITY("dyn(u) != -1.0"), HETEROGENEOUS_DYNAMIC_PRECISION( "type(dyn_var) == int && type(dyn_var2) == double && dyn_var == 9007199254740993 &&" + " dyn_var2 == 9007199254740992.0 ? dyn_var != dyn_var2 : true"), @@ -727,6 +782,8 @@ private enum IsAlwaysTrueTestCase { DYNAMIC_LIST_RESOLVES_CORRELATED_NESTING( "int_list == [1, 2] && int_list_2 == [2, 3] ? int_list.exists(x, int_list_2.exists(y, x" + " == y)) : true"), + DYNAMIC_LIST_ELEMENT_NEVER_ERROR( + "size(dyn_list) > 0 ? (dyn_list[0] == 1 || dyn_list[0] != 1) : true"), DYNAMIC_MAP_EXISTS( "string_int_map == {'a': 1, 'b': 2} ? string_int_map.exists(k, string_int_map[k] == 2)" + " : true"), @@ -859,6 +916,15 @@ private enum IsAlwaysTrueTestCase { DYNAMIC_VAR_TYPE_IDENTITY("type(dyn_var) == type(dyn_var)"), DYNAMIC_MAP_KEY_COMPREHENSION_TYPE_IDENTITY( "size(dyn_map) > 0 && size(dyn_map) <= 5 ? dyn_map.all(k, type(k) == type(k)) : true"), + DYNAMIC_MAP_VALUE_NOT_ERROR( + "size(dyn_map) == 1 && 1 in dyn_map ? dyn_map.all(k, v, v == 1 || v != 1) : true"), + MAP_KEY_TYPE_CONSTRAINT( + "size(string_int_map) > 0 && size(string_int_map) <= 5 ?" + + " string_int_map.all(k, type(k) == string) : true"), + MAP_VALUE_TYPE_CONSTRAINT( + "size(string_int_map) > 0 && size(string_int_map) <= 5 ?" + + " string_int_map.all(k, v, v >= -9223372036854775808 &&" + + " v <= 9223372036854775807) : true"), ; final String expr; @@ -1011,6 +1077,18 @@ public void verifyEquivalence_unknownPrecedenceOverError() throws Exception { assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); } + @Test + public void verifyEquivalence_freeVariableIndicesDeduplicated() throws Exception { + CelAbstractSyntaxTree astA = + CEL.compile("x == y && y == port ? dyn_list.all(e, x == x) : false").getAst(); + CelAbstractSyntaxTree astB = + CEL.compile("x == y && y == port ? dyn_list.all(e, y == port) : false").getAst(); + + CelVerificationResult result = VERIFIER.verifyEquivalence(astA, astB); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + } + @Test public void isSatisfiable_approximateIterRangeInMap_inconclusive() throws Exception { Cel celWithCustomFunc = @@ -1532,7 +1610,10 @@ private enum IsInconclusiveTestCase { COMPREHENSION_NULL_CONSTANT("size(int_list) == 6 ? size(int_list.map(x, null)) == 6 : true"), COMPREHENSION_UINT_CONSTANT("size(int_list) == 6 ? size(int_list.map(x, 1u)) == 6 : true"), COMPREHENSION_DOUBLE_CONSTANT("size(int_list) == 6 ? size(int_list.map(x, 1.0)) == 6 : true"), - COMPREHENSION_BYTES_CONSTANT("size(int_list) == 6 ? size(int_list.map(x, b'abc')) == 6 : true"); + COMPREHENSION_BYTES_CONSTANT("size(int_list) == 6 ? size(int_list.map(x, b'abc')) == 6 : true"), + COMPREHENSION_FREE_VAR_INDEX_DEDUPLICATION( + "x == y && y == port ? dyn_list.all(e, x == x) == dyn_list.all(e, y == port) : true"), + ; final String expr; @@ -1891,7 +1972,16 @@ private enum EquivalenceTestCase { OPTIONAL_INDEX_LIST_UNWRAPPING("optional.of([1, 2, 3])[?0]", "optional.of(1)"), OPTIONAL_INDEX_MAP_UNWRAPPING("optional.of({'a': 1})[?'a']", "optional.of(1)"), OPTIONAL_INDEX_UNWRAPPING_NONE("optional.none()[?0]", "optional.none()"), - INT_IN_LIST_IDENTITY_EQUIVALENT("x in [1, 2, x]", "true"); + INT_IN_LIST_IDENTITY_EQUIVALENT("x in [1, 2, x]", "true"), + HETEROGENEOUS_INT_NON_INTEGER_DOUBLE_EQUIVALENCE("dyn(x) == 1.5", "false"), + HETEROGENEOUS_INT_OUT_OF_BOUNDS_DOUBLE_EQUIVALENCE("dyn(x) == 9223372036854777856.0", "false"), + HETEROGENEOUS_UINT_NON_INTEGER_DOUBLE_EQUIVALENCE("dyn(u) == 1.5", "false"), + HETEROGENEOUS_UINT_OUT_OF_BOUNDS_DOUBLE_EQUIVALENCE( + "dyn(u) == 18446744073709555712.0", "false"), + HETEROGENEOUS_UINT_NEGATIVE_DOUBLE_EQUIVALENCE("dyn(u) == -1.0", "false"), + HETEROGENEOUS_UINT_ZERO_DOUBLE_EQUIVALENCE("dyn(u) == 0.0", "u == 0u"), + DYNAMIC_LIST_ELEMENT_NEVER_ERROR_EQUIVALENCE( + "size(dyn_list) > 0 ? (dyn_list[0] == 1 || dyn_list[0] != 1) : true", "true"); private final String exprA; private final String exprB; @@ -2737,6 +2827,50 @@ public void isAlwaysTrue_largeListCounterexample_truncatesOutput() throws Except assertThat(result.message()).contains("... (5 more elements)"); } + @Test + public void isAlwaysTrue_largeMapCounterexample_truncatesOutput() throws Exception { + Cel cel = + CelFactory.plannerCelBuilder() + .addVar("large_map", MapType.create(SimpleType.INT, SimpleType.INT)) + .build(); + StringBuilder mapLiteral = new StringBuilder("{"); + for (int i = 0; i < 20; i++) { + mapLiteral.append(i).append(": 1"); + if (i < 19) { + mapLiteral.append(", "); + } + } + mapLiteral.append("}"); + + CelAbstractSyntaxTree ast = cel.compile("!(large_map == " + mapLiteral + ")").getAst(); + CelVerifier verifier = + CelVerifierFactory.newVerifier().setTimeout(Duration.ofSeconds(10)).build(); + + CelVerificationResult result = verifier.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.message()).contains("... (5 more entries)"); + } + + @Test + public void counterexample_messageTwoFieldsFormatted() throws Exception { + Cel cel = + CelFactory.plannerCelBuilder() + .setContainer(CelContainer.ofName("cel.expr.conformance.proto3")) + .addMessageTypes(TestAllTypes.getDescriptor()) + .addVar("msg", StructTypeReference.create("cel.expr.conformance.proto3.TestAllTypes")) + .setTypeProvider(TYPE_PROVIDER) + .build(); + CelAbstractSyntaxTree ast = + cel.compile("!(msg == TestAllTypes{single_int32: 1, single_int64: 2})").getAst(); + + CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.message()).contains("single_int32: 1"); + assertThat(result.message()).contains("single_int64: 2"); + } + @Test public void isAlwaysTrue_customComprehensionWithTrueAccuInit() throws Exception { Cel cel = diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java index 52124c6ed..5b289c39a 100644 --- a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java @@ -168,6 +168,12 @@ public void repl_equivQueries() throws Exception { assertThat(output[1]).contains("Equivalence query format: equiv <=> "); } + @Test + public void repl_equivDoubleNegation() throws Exception { + String[] output = runReplWithCommands(":var x int", "equiv !!(x == 10) <=> (x == 10)", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + } + @Test public void repl_unknownCommandsAndErrors() throws Exception { String[] output =