diff --git a/BUILD.bazel b/BUILD.bazel index 024908625..d2bf2124b 100644 --- a/BUILD.bazel +++ b/BUILD.bazel @@ -95,6 +95,14 @@ java_library( ], ) +java_library( + name = "java_jline", + exports = [ + "@maven//:org_jline_jline_reader", + "@maven//:org_jline_jline_terminal", + ], +) + default_java_toolchain( name = "repository_default_toolchain", configuration = DEFAULT_TOOLCHAIN_CONFIGURATION, diff --git a/MODULE.bazel b/MODULE.bazel index ce9c67fde..3dcf8b0e5 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -95,6 +95,8 @@ maven.install( "info.picocli:picocli:4.7.7", "org.antlr:antlr4-runtime:4.13.2", "org.freemarker:freemarker:2.3.34", + "org.jline:jline-reader:3.26.1", + "org.jline:jline-terminal:3.26.1", "org.jspecify:jspecify:1.0.0", "org.threeten:threeten-extra:1.8.0", "org.yaml:snakeyaml:2.5", 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/README.md b/verifier/README.md index f286a4d6f..bd9979390 100644 --- a/verifier/README.md +++ b/verifier/README.md @@ -433,3 +433,7 @@ What this means for verification: default unless you have a specific need and bounded inputs. --- + +## Tools & CLI + +For command-line verification and interactive execution, see the [CLI Tool documentation](tools/README.md). 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 e3bb1bfaf..3964d68a1 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -741,7 +741,7 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes))); typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes))); - boolean isDynamic = ast.getType(exprId).map(SimpleType.DYN::equals).orElse(true); + boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN); BoolExpr isApprox = ctx.mkBool(!isDynamic); return TranslatedValue.propagateStrict( ctx, typeSystem, callRes, Optional.of(expr), isApprox, args); @@ -877,10 +877,6 @@ private TranslatedValue translateDynamicComprehension( ArrayExpr mapPresence = isMap ? (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(iterRange)) : null; - if (isMap) { - applyBoundedMapBijection(mapPresence, seq, lengthExpr); - } - BoolExpr isTruncated = ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit)); truncationConditions.add(isTruncated); @@ -893,14 +889,15 @@ private TranslatedValue translateDynamicComprehension( } } - private void applyBoundedMapBijection( + private BoolExpr getBoundedMapBijection( ArrayExpr mapPresence, SeqExpr seq, ArithExpr lengthExpr) { + List constraints = new ArrayList<>(); for (int i = 0; i < comprehensionUnrollLimit; i++) { for (int j = i + 1; j < comprehensionUnrollLimit; j++) { BoolExpr validPair = ctx.mkLt(ctx.mkInt(j), lengthExpr); BoolExpr notEqual = ctx.mkNot(ctx.mkEq(ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkNth(seq, ctx.mkInt(j)))); - typeConstraints.add(ctx.mkImplies(validPair, notEqual)); + constraints.add(ctx.mkImplies(validPair, notEqual)); } } @@ -915,7 +912,8 @@ private void applyBoundedMapBijection( ctx.mkStore(seqMap, ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkTrue()), seqMap); } - typeConstraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap))); + constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap))); + return CelZ3TypeSystem.mkAndFlattened(ctx, constraints); } private TranslatedValue[] evaluateLoopCondAndStep( @@ -1230,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) { @@ -1247,9 +1245,10 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { } Expr optRef = typeSystem.getOptionalRef(val); BoolExpr hasValue = typeSystem.optHasValue(optRef); - BoolExpr valConstraint = - createTypeConstraintForType(typeSystem.getOptionalValue(optRef), paramType); - return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, valConstraint)); + Expr optVal = typeSystem.getOptionalValue(optRef); + BoolExpr optValNotError = ctx.mkNot(typeSystem.isError(optVal)); + BoolExpr valConstraint = createTypeConstraintForType(optVal, paramType); + return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, ctx.mkAnd(optValNotError, valConstraint))); } if (type.equals(SimpleType.BOOL)) { return (BoolExpr) ctx.mkApp(typeSystem.boolCons().getTesterDecl(), val); @@ -1258,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); @@ -1289,15 +1288,13 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { } if (type instanceof ListType) { - // Lists are explicitly bounded (sequence theory). We're safe in using for-all quantifiers - // here. + // Constrain list elements using bounded unrolling up to comprehensionUnrollLimit rather + // than Z3 forall quantifiers to prevent MBQI quantifier instantiation loops. + // Assert: isList(val) ∧ for all unrolled 0 <= i < length: ¬isError(seq[i]) ∧ + // typeConstraint(seq[i]) BoolExpr isList = typeSystem.isList(val); CelType elemType = ((ListType) type).elemType(); - if (elemType.equals(SimpleType.DYN)) { - return isList; - } - // isList(val) ∧ ∀i. (0 <= i < length) ⇒ elemType(seq[i]) Expr listRef = typeSystem.getListRef(val); SeqExpr seq = typeSystem.getSeq(listRef); Expr length = ctx.mkLength(seq); @@ -1307,20 +1304,62 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { for (int i = 0; i < comprehensionUnrollLimit; i++) { IntExpr idx = ctx.mkInt(i); Expr elem = ctx.mkNth(seq, idx); - BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType); BoolExpr validIndex = ctx.mkLt(idx, length); + // Assert ¬isError(elem) as a domain invariant so Z3 never synthesizes an Error element in + // list(dyn). For concrete types, this is already implied by createTypeConstraintForType. + boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkNot(typeSystem.isError(elem)))); + BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType); boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint)); - BoolExpr outOfBounds = ctx.mkGe(idx, length); - boundsAndTypes.add(ctx.mkImplies(outOfBounds, ctx.mkEq(elem, typeSystem.mkUnknown()))); } return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); } if (type instanceof MapType) { - // Do NOT emit a for-all quantifier over map keys here. - // Doing so forces MBQI into an infinite loop. Structural equivalence of dynamic keys is - // naturally constrained by the primitive key assertions in getStructuralEquality(). - return typeSystem.isMap(val); + // Do NOT emit a for-all quantifier over map keys or values here. + // Doing so forces MBQI into an infinite loop. Instead, constrain keys and values using + // bounded unrolling over the key sequence up to comprehensionUnrollLimit. + // Assert: isMap(val) ∧ for all unrolled 0 <= i < length: isPrimitiveKey(key) ∧ ¬isError(key) + // ∧ (presence(key) ⇒ ¬isError(val) ∧ typeConstraint(val)) + BoolExpr isMap = typeSystem.isMap(val); + MapType mapType = (MapType) type; + CelType keyType = mapType.keyType(); + CelType valType = mapType.valueType(); + + Expr mapRef = typeSystem.getMapRef(val); + SeqExpr seq = typeSystem.getMapKeys(mapRef); + Expr length = ctx.mkLength(seq); + ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef); + ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef); + + List boundsAndTypes = new ArrayList<>(); + boundsAndTypes.add(isMap); + boundsAndTypes.add(getBoundedMapBijection(mapPresence, seq, (ArithExpr) length)); + + for (int i = 0; i < comprehensionUnrollLimit; i++) { + IntExpr idx = ctx.mkInt(i); + Expr key = ctx.mkNth(seq, idx); + BoolExpr validIndex = ctx.mkLt(idx, length); + + BoolExpr isKeyPrim = typeSystem.isPrimitiveKey(key); + BoolExpr keyNotError = ctx.mkNot(typeSystem.isError(key)); + // Assert isKeyPrim ∧ ¬isError(key) so Z3 never synthesizes a non-primitive or Error key in + // map(dyn, ...). For concrete map types, this is already implied by keyType constraints. + boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkAnd(isKeyPrim, keyNotError))); + boundsAndTypes.add(ctx.mkImplies(validIndex, createTypeConstraintForType(key, keyType))); + + BoolExpr presence = (BoolExpr) ctx.mkSelect(mapPresence, key); + BoolExpr validEntry = ctx.mkAnd(validIndex, presence); + + Expr mapVal = ctx.mkSelect(mapValues, key); + 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))); + } + + return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); } if (type.kind() == CelKind.STRUCT) { return ctx.mkAnd( @@ -1373,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/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index 510d88ec0..90d7238c2 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -303,8 +303,10 @@ CelVerificationResult verifyImplication( /* isCounterexample= */ true)); case TRUNCATED: return CelVerificationResult.inconclusive( - String.format("Inconclusive: %s holds within the current loop unroll limit, but" - + " may be violated for larger collections.", subjectName.toLowerCase(Locale.US))); + String.format( + "Inconclusive: %s holds within the current loop unroll limit, but" + + " may be violated for larger collections.", + subjectName.toLowerCase(Locale.US))); case NO_MATCH: return CelVerificationResult.verified(); case SOLVER_UNKNOWN: diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index 2355d36bf..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() {} @@ -127,6 +130,8 @@ private static String formatExpr( return "Error"; } else if (decl.equals(typeSystem.unknownCons().ConstructorDecl())) { return "Unknown"; + } else if (decl.equals(typeSystem.nullCons().ConstructorDecl())) { + return "null"; } else if (decl.equals(typeSystem.optionalCons().ConstructorDecl())) { Expr optRef = expr.getArgs()[0]; Expr hasValueExpr = @@ -156,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 = @@ -177,24 +184,33 @@ private static String reconstructList( private static String reconstructMap( Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr mapRef) { - Expr presenceArray = + Expr lenExpr = evaluateStrict( model, - typeSystem.getMapPresence(mapRef), - String.format("Z3 failed to evaluate presence array natively for map %s", mapRef)); - - List> keys = new ArrayList<>(); - extractKeys(presenceArray, keys); + ctx.mkLength(typeSystem.getMapKeys(mapRef)), + String.format("Z3 failed to evaluate length for map %s", mapRef)); + 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( @@ -207,17 +223,20 @@ private static String reconstructMap( + formatExpr(ctx, typeSystem, model, value)); } } + if (length > printLimit) { + entries.add("... (" + (length - printLimit) + " more entries)"); + } return "{" + String.join(", ", entries) + "}"; } private static String reconstructMessage( Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr msgRef) { - Expr valuesArray = + Expr presenceArray = evaluateStrict( model, - typeSystem.getMsgValues(msgRef), - String.format("Z3 failed to evaluate values array natively for msg %s", msgRef)); + typeSystem.getMsgPresence(msgRef), + String.format("Z3 failed to evaluate presence array natively for msg %s", msgRef)); Expr typeNameExpr = evaluateStrict( @@ -227,8 +246,8 @@ private static String reconstructMessage( String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", ""); - List> keys = new ArrayList<>(); - extractKeys(valuesArray, keys); + Set> keys = new LinkedHashSet<>(); + extractKeys(presenceArray, keys); List entries = new ArrayList<>(); for (Expr key : keys) { @@ -254,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) { @@ -266,16 +285,15 @@ private static void extractKeys(Expr arrayExpr, List> keys) { FuncDecl decl = arrayExpr.getFuncDecl(); String declName = decl.getName().toString(); - if (!declName.equals("store")) { - break; + if (declName.equals("store")) { + Expr[] args = arrayExpr.getArgs(); + Preconditions.checkState( + args.length == 3, "Z3 store array operation must have exactly 3 arguments"); + keys.add(args[1]); + arrayExpr = args[0]; + continue; } - - Expr[] args = arrayExpr.getArgs(); - Preconditions.checkState( - args.length == 3, "Z3 store array operation must have exactly 3 arguments"); - keys.add(args[1]); - - arrayExpr = args[0]; + break; } } 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 e9a1872c9..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); @@ -685,6 +686,11 @@ public Expr getBytes(Expr val) { return ctx.mkApp(bytesCons.getAccessorDecls()[0], val); } + /** Checks if the given CelValue is a valid primitive map key type. */ + public BoolExpr isPrimitiveKey(Expr val) { + return ctx.mkOr(isBool(val), isInt(val), isUint(val), isString(val), isBytes(val)); + } + /** Checks if the given CelValue is a struct (message). */ public BoolExpr isStruct(Expr val) { return isMessage(val); @@ -799,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. */ @@ -818,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/GreaterAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java index 292b86135..2ccb1543a 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java @@ -15,7 +15,6 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -56,9 +55,7 @@ final class GreaterAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkFPGt( - (FPExpr) typeSystem.getDouble(lhs), - (FPExpr) typeSystem.getDouble(rhs))))) + ctx.mkFPGt(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_STRING.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -82,7 +79,7 @@ final class GreaterAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLtReal( ctx, - (FPExpr) typeSystem.getDouble(rhs), + typeSystem.getDouble(rhs), ctx.mkInt2Real(typeSystem.getInt(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_UINT64_DOUBLE.celOverloadDecl(), @@ -91,7 +88,7 @@ final class GreaterAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLtReal( ctx, - (FPExpr) typeSystem.getDouble(rhs), + typeSystem.getDouble(rhs), ctx.mkInt2Real(typeSystem.getUint(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_DOUBLE_INT64.celOverloadDecl(), @@ -101,7 +98,7 @@ final class GreaterAxiom { AxiomHelpers.mkRealLtFp( ctx, ctx.mkInt2Real(typeSystem.getInt(rhs)), - (FPExpr) typeSystem.getDouble(lhs))))) + typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_DOUBLE_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -110,7 +107,7 @@ final class GreaterAxiom { AxiomHelpers.mkRealLtFp( ctx, ctx.mkInt2Real(typeSystem.getUint(rhs)), - (FPExpr) typeSystem.getDouble(lhs))))) + typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_INT64_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java index 4be0c23e2..d71f0f248 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java @@ -15,7 +15,6 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -56,9 +55,7 @@ final class GreaterEqualsAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkFPGEq( - (FPExpr) typeSystem.getDouble(lhs), - (FPExpr) typeSystem.getDouble(rhs))))) + ctx.mkFPGEq(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_STRING.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -82,7 +79,7 @@ final class GreaterEqualsAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLeReal( ctx, - (FPExpr) typeSystem.getDouble(rhs), + typeSystem.getDouble(rhs), ctx.mkInt2Real(typeSystem.getInt(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_UINT64_DOUBLE.celOverloadDecl(), @@ -91,7 +88,7 @@ final class GreaterEqualsAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLeReal( ctx, - (FPExpr) typeSystem.getDouble(rhs), + typeSystem.getDouble(rhs), ctx.mkInt2Real(typeSystem.getUint(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_DOUBLE_INT64.celOverloadDecl(), @@ -101,7 +98,7 @@ final class GreaterEqualsAxiom { AxiomHelpers.mkRealLeFp( ctx, ctx.mkInt2Real(typeSystem.getInt(rhs)), - (FPExpr) typeSystem.getDouble(lhs))))) + typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_DOUBLE_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -110,7 +107,7 @@ final class GreaterEqualsAxiom { AxiomHelpers.mkRealLeFp( ctx, ctx.mkInt2Real(typeSystem.getUint(rhs)), - (FPExpr) typeSystem.getDouble(lhs))))) + typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_INT64_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java index e09484f28..31b1d3a21 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java @@ -15,7 +15,6 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -56,9 +55,7 @@ final class LessAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkFPLt( - (FPExpr) typeSystem.getDouble(lhs), - (FPExpr) typeSystem.getDouble(rhs))))) + ctx.mkFPLt(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_STRING.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -83,7 +80,7 @@ final class LessAxiom { AxiomHelpers.mkRealLtFp( ctx, ctx.mkInt2Real(typeSystem.getInt(lhs)), - (FPExpr) typeSystem.getDouble(rhs))))) + typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_UINT64_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -92,7 +89,7 @@ final class LessAxiom { AxiomHelpers.mkRealLtFp( ctx, ctx.mkInt2Real(typeSystem.getUint(lhs)), - (FPExpr) typeSystem.getDouble(rhs))))) + typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_DOUBLE_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -100,7 +97,7 @@ final class LessAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLtReal( ctx, - (FPExpr) typeSystem.getDouble(lhs), + typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getInt(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_DOUBLE_UINT64.celOverloadDecl(), @@ -109,7 +106,7 @@ final class LessAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLtReal( ctx, - (FPExpr) typeSystem.getDouble(lhs), + typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getUint(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_INT64_UINT64.celOverloadDecl(), diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java index e27b47631..c2466cf1b 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java @@ -15,7 +15,6 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -56,9 +55,7 @@ final class LessEqualsAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkFPLEq( - (FPExpr) typeSystem.getDouble(lhs), - (FPExpr) typeSystem.getDouble(rhs))))) + ctx.mkFPLEq(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_STRING.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -83,7 +80,7 @@ final class LessEqualsAxiom { AxiomHelpers.mkRealLeFp( ctx, ctx.mkInt2Real(typeSystem.getInt(lhs)), - (FPExpr) typeSystem.getDouble(rhs))))) + typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_UINT64_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -92,7 +89,7 @@ final class LessEqualsAxiom { AxiomHelpers.mkRealLeFp( ctx, ctx.mkInt2Real(typeSystem.getUint(lhs)), - (FPExpr) typeSystem.getDouble(rhs))))) + typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_DOUBLE_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -100,7 +97,7 @@ final class LessEqualsAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLeReal( ctx, - (FPExpr) typeSystem.getDouble(lhs), + typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getInt(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_DOUBLE_UINT64.celOverloadDecl(), @@ -109,7 +106,7 @@ final class LessEqualsAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLeReal( ctx, - (FPExpr) typeSystem.getDouble(lhs), + typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getUint(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_INT64_UINT64.celOverloadDecl(), 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 8cd844214..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,12 +14,11 @@ 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; import com.microsoft.z3.Expr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; import com.microsoft.z3.Sort; @@ -233,8 +232,7 @@ private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions sink.accept(ctx.mkOr(typeSystem.isDouble(res), typeSystem.isError(res))); sink.accept( ctx.mkImplies( - typeSystem.isDouble(res), - ctx.mkNot(ctx.mkFPIsNaN((FPExpr) typeSystem.getDouble(res))))); + typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res))))); break; case STRING: sink.accept(ctx.mkOr(typeSystem.isString(res), typeSystem.isError(res))); diff --git a/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel new file mode 100644 index 000000000..28ce776cb --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel @@ -0,0 +1,80 @@ +load("@rules_java//java:defs.bzl", "java_binary", "java_library") +load("//publish:cel_version.bzl", "CEL_VERSION") + +package( + default_applicable_licenses = [ + "//:license", + ], + default_visibility = [ + "//verifier:__subpackages__", + ], +) + +genrule( + name = "generate_version", + outs = ["CelVersion.java"], + cmd = """cat << 'EOF' > $@ +package dev.cel.verifier.tools; + +final class CelVersion { + static final String VERSION = "%s"; + + private CelVersion() {} +} +EOF +""" % CEL_VERSION, +) + +java_library( + name = "tools_lib", + srcs = [ + "CelVerifierRepl.java", + "CelVerifierTool.java", + "CelVerifierToolCore.java", + "FormatUtils.java", + "VerificationOptions.java", + ":generate_version", + ], + tags = [ + "alt_dep=//verifier/tools", + ], + deps = [ + "//:java_jline", + "//bundle:cel", + "//common:cel_ast", + "//common:compiler_common", + "//common:options", + "//common/types", + "//common/types:cel_types", + "//common/types:type_providers", + "//compiler", + "//compiler:compiler_builder", + "//extensions", + "//parser:macro", + "//policy", + "//policy:compiler", + "//policy:compiler_factory", + "//policy:parser", + "//policy:parser_factory", + "//policy:validation_exception", + "//verifier", + "//verifier:policy_verifier", + "//verifier:policy_verifier_factory", + "//verifier:verifier_factory", + "@maven//:com_google_errorprone_error_prone_annotations", + "@maven//:com_google_guava_guava", + "@maven//:info_picocli_picocli", + ], +) + +java_binary( + name = "cel_verifier_tool", + jvm_flags = ["-Dz3.skipLibraryLoad=true"], + main_class = "dev.cel.verifier.tools.CelVerifierTool", + tags = [ + "alt_dep=//verifier/tools:cel_verifier_tool", + ], + runtime_deps = [ + ":tools_lib", + ], +) diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java new file mode 100644 index 000000000..94348ff15 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java @@ -0,0 +1,439 @@ +// 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.tools; + +import static java.nio.charset.StandardCharsets.UTF_8; + +import com.google.common.base.Ascii; +import com.google.common.collect.ImmutableList; +import dev.cel.common.CelValidationException; +import dev.cel.common.types.CelType; +import dev.cel.common.types.CelTypes; +import dev.cel.policy.CelPolicyValidationException; +import dev.cel.verifier.CelVerificationResult; +import java.io.BufferedReader; +import java.io.InputStreamReader; +import java.io.PrintStream; +import java.time.Duration; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Locale; +import java.util.Map; +import java.util.Optional; +import org.jline.reader.EndOfFileException; +import org.jline.reader.LineReader; +import org.jline.reader.LineReaderBuilder; +import org.jline.reader.UserInterruptException; +import org.jline.terminal.Terminal; +import org.jline.terminal.TerminalBuilder; + +/** Interactive REPL shell for CEL formal verification. */ +final class CelVerifierRepl { + + private CelVerifierRepl() {} + + static int runInteractiveRepl() { + LineReader lineReader = null; + BufferedReader fallbackReader = null; + try { + Terminal terminal = TerminalBuilder.builder().system(true).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)); + } + return runReplInternal(lineReader, fallbackReader, System.out, System.err); + } + + static int runRepl(BufferedReader reader, PrintStream out, PrintStream err) { + return runReplInternal(null, reader, out, err); + } + + private static int runReplInternal( + LineReader lineReader, BufferedReader fallbackReader, PrintStream out, PrintStream err) { + out.println("============================================================"); + out.println(" CEL Verification REPL"); + out.println(" Type :help for commands, :quit to exit."); + out.println("============================================================"); + + Map sessionVars = new HashMap<>(); + List unknownIdentifiers = new ArrayList<>(); + int timeoutSeconds = 10; + int unrollLimit = 5; + + String prompt = FormatUtils.ANSI_CYAN + "cel-verifier> " + FormatUtils.ANSI_RESET; + + while (true) { + String line; + try { + if (lineReader != null) { + line = lineReader.readLine(prompt); + } else if (fallbackReader != null) { + out.print(prompt); + out.flush(); + line = fallbackReader.readLine(); + if (line == null) { + break; // EOF + } + } else { + break; + } + } catch (UserInterruptException | EndOfFileException e) { + out.println("Goodbye!"); + break; + } catch (Exception e) { + err.println("Error reading input: " + e.getMessage()); + break; + } + + line = line.trim(); + if (line.isEmpty()) { + continue; + } + + if (line.startsWith(":")) { + if (Ascii.equalsIgnoreCase(line, ":quit") || Ascii.equalsIgnoreCase(line, ":exit")) { + out.println("Goodbye!"); + break; + } + + Optional helpArg = extractCommandArg(line, ":help"); + if (helpArg.isPresent()) { + printHelp(helpArg.get(), out); + continue; + } + + if (Ascii.equalsIgnoreCase(line, ":vars")) { + printVars(sessionVars, unknownIdentifiers, timeoutSeconds, unrollLimit, out); + continue; + } + + if (Ascii.equalsIgnoreCase(line, ":clear")) { + sessionVars.clear(); + unknownIdentifiers.clear(); + out.println("Session state reset."); + continue; + } + + Optional varArg = extractCommandArg(line, ":var"); + if (varArg.isPresent()) { + String arg = varArg.get(); + if (arg.isEmpty()) { + err.println( + "Usage: :var (e.g. :var role string, :var scores map)"); + } else { + handleVarCommand(arg, sessionVars, out, err); + } + continue; + } + + Optional unknownArg = extractCommandArg(line, ":unknown"); + if (unknownArg.isPresent()) { + String arg = unknownArg.get(); + if (arg.isEmpty()) { + err.println("Usage: :unknown "); + } else { + unknownIdentifiers.add(arg); + out.println("Added unknown identifier: '" + arg + "'"); + } + continue; + } + + Optional timeoutArg = extractCommandArg(line, ":timeout"); + if (timeoutArg.isPresent()) { + String arg = timeoutArg.get(); + if (arg.isEmpty()) { + err.println("Usage: :timeout "); + } else { + try { + int t = Integer.parseInt(arg); + if (t <= 0) { + err.println("Timeout must be a positive integer."); + } else { + timeoutSeconds = t; + out.println("Timeout set to " + timeoutSeconds + "s."); + } + } catch (NumberFormatException e) { + err.println("Invalid timeout value."); + } + } + continue; + } + + Optional unrollArg = extractCommandArg(line, ":unroll"); + if (unrollArg.isPresent()) { + String arg = unrollArg.get(); + if (arg.isEmpty()) { + err.println("Usage: :unroll "); + } else { + try { + int u = Integer.parseInt(arg); + if (u < 0) { + err.println("Unroll limit must be non-negative."); + } else { + unrollLimit = u; + out.println("Comprehension unroll limit set to " + unrollLimit + "."); + } + } catch (NumberFormatException e) { + err.println("Invalid unroll limit value."); + } + } + continue; + } + + err.println("Unknown command: " + line + ". Type :help for commands."); + continue; + } + + // Handle queries + VerificationOptions options = + VerificationOptions.builder() + .setTimeout(Duration.ofSeconds(timeoutSeconds)) + .setComprehensionUnrollLimit(unrollLimit) + .setUnknownIdentifiers(unknownIdentifiers) + .build(); + + try { + Optional satArg = extractCommandArg(line, "sat"); + Optional validArg = extractCommandArg(line, "valid"); + Optional equivArg = extractCommandArg(line, "equiv"); + + if (satArg.isPresent()) { + String arg = satArg.get(); + if (arg.isEmpty()) { + err.println("Usage: sat "); + } else { + CelVerificationResult res = + CelVerifierToolCore.checkSatisfiable(arg, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } else if (validArg.isPresent()) { + String arg = validArg.get(); + if (arg.isEmpty()) { + err.println("Usage: valid "); + } else { + CelVerificationResult res = CelVerifierToolCore.checkValid(arg, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } else if (equivArg.isPresent()) { + String arg = equivArg.get(); + ImmutableList parts = splitEquivQuery(arg); + if (parts.size() != 2 || parts.get(0).isEmpty() || parts.get(1).isEmpty()) { + err.println("Equivalence query format: equiv <=> "); + } else { + String exprA = parts.get(0).trim(); + String exprB = parts.get(1).trim(); + CelVerificationResult res = + CelVerifierToolCore.verifyEquivalence(exprA, exprB, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } else { + // Default: treat as sat query + CelVerificationResult res = + CelVerifierToolCore.checkSatisfiable(line, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } catch (CelValidationException e) { + err.println( + FormatUtils.ANSI_RED + + "Compilation error:\n" + + e.getMessage() + + FormatUtils.ANSI_RESET); + } catch (CelPolicyValidationException e) { + err.println( + FormatUtils.ANSI_RED + + "Policy compilation error:\n" + + e.getMessage() + + FormatUtils.ANSI_RESET); + } catch (Exception e) { + err.println( + FormatUtils.ANSI_RED + + "Verification failed: " + + e.getMessage() + + FormatUtils.ANSI_RESET); + } + } + return 0; + } + + private static void handleVarCommand( + String arg, Map sessionVars, PrintStream out, PrintStream err) { + String[] parts = arg.split("\\s+", 2); + if (parts.length != 2) { + err.println("Usage: :var (e.g. :var role string, :var scores map)"); + return; + } + String name = parts[0].trim(); + String typeStr = parts[1].trim(); + try { + CelType type = VerificationOptions.parseCelType(typeStr); + sessionVars.put(name, type); + out.println("Variable declared: " + name + " : " + CelTypes.format(type)); + } catch (IllegalArgumentException e) { + err.println(e.getMessage()); + } + } + + private static void printVars( + Map sessionVars, + List unknowns, + int timeoutSeconds, + int unrollLimit, + PrintStream out) { + out.println("--- Session State ---"); + out.println("Timeout: " + timeoutSeconds + "s | Unroll limit: " + unrollLimit); + out.println("Unknowns: " + (unknowns.isEmpty() ? "none" : unknowns)); + out.println("Variables (" + sessionVars.size() + "):"); + for (Map.Entry entry : sessionVars.entrySet()) { + out.println(" " + entry.getKey() + " : " + CelTypes.format(entry.getValue())); + } + } + + private static void printHelp(String topic, PrintStream out) { + String t = topic.toLowerCase(Locale.US).replace(":", "").trim(); + switch (t) { + case "var": + case "vars": + out.println("Command: :var "); + out.println("Declares a variable in the REPL session with a specific type."); + out.println(); + out.println("Supported Types:"); + out.println(" - Primitive types: int, uint, string, bool, double, bytes"); + out.println(" - List types: list (e.g., list, list)"); + out.println(" - Map types: map (e.g., map, map)"); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :var role string"); + out.println(" cel-verifier> :var port int"); + out.println(" cel-verifier> :var scores map"); + out.println(" cel-verifier> :var tags list"); + break; + case "unknown": + out.println("Command: :unknown "); + out.println( + "Marks an identifier path as 'Unknown' during verification (partial evaluation)."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :unknown request.headers"); + out.println(" cel-verifier> :unknown request.auth.claims"); + break; + case "timeout": + out.println("Command: :timeout "); + out.println("Configures the Z3 solver soft timeout duration in seconds (default: 10s)."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :timeout 5"); + break; + case "unroll": + out.println("Command: :unroll "); + out.println("Configures the BMC loop unroll limit for comprehensions (default: 5)."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :unroll 3"); + break; + case "sat": + out.println("Query: sat "); + out.println( + "Checks if a CEL expression can evaluate to true for any possible input assignments."); + out.println("If satisfiable, outputs concrete satisfying witness values."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> sat role == 'editor' && port > 1024"); + out.println(" cel-verifier> sat scores['alice'] > 90"); + break; + case "valid": + out.println("Query: valid "); + out.println( + "Proves whether a CEL expression evaluates to true for ALL possible input" + + " assignments."); + out.println("If invalid, outputs a counterexample showing inputs causing it to fail."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> valid x > 10 || x <= 10"); + break; + case "equiv": + out.println("Query: equiv <=> "); + out.println( + "Proves whether two CEL expressions are semantically identical for all inputs."); + out.println( + "If not equivalent, outputs a counterexample showing inputs where they diverge."); + out.println(); + out.println("Use '<=>' as the recommended separator between expressions."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> equiv x > 10 <=> 10 < x"); + out.println(" cel-verifier> equiv (a && b) || (a && c) <=> a && (b || c)"); + out.println( + " cel-verifier> equiv string_int_map == {'a': 1, 'b': 2} ? string_int_map.all(k, k ==" + + " 'a') : true <=> string_int_map == {'a': 1, 'b': 2} ? string_int_map.all(k, k ==" + + " 'a') : true"); + break; + default: + out.println("REPL Commands:"); + out.println( + " :var Declare variable (e.g. :var role string, :var m" + + " map)"); + out.println(" :unknown Mark identifier as unknown"); + out.println(" :timeout Set solver timeout (default: 10s)"); + out.println(" :unroll Set comprehension unroll limit (default: 5)"); + out.println(" :vars List session variables & options"); + out.println(" :clear Reset session state"); + out.println( + " :help [command] Display help message or specific command details"); + out.println(" :quit Exit REPL"); + out.println(); + out.println("Verification Queries:"); + out.println(" sat Check satisfiability"); + out.println(" valid Check validity (always true)"); + out.println(" equiv <=> Prove logical equivalence"); + out.println(" Check satisfiability (default)"); + out.println(); + out.println( + "Type ':help ' (e.g. ':help var', ':help sat') for detailed usage and" + + " examples."); + break; + } + } + + private static ImmutableList splitEquivQuery(String rest) { + if (rest == null || rest.trim().isEmpty()) { + return ImmutableList.of(); + } + String input = rest.trim(); + if (input.contains(" <=> ")) { + return ImmutableList.copyOf(input.split(" <=> ", 2)); + } + if (input.contains("<=>")) { + return ImmutableList.copyOf(input.split("<=>", 2)); + } + return ImmutableList.of(); + } + + private static Optional extractCommandArg(String line, String prefix) { + if (Ascii.equalsIgnoreCase(line, prefix)) { + return Optional.of(""); + } + String prefixLower = Ascii.toLowerCase(prefix); + String lineLower = Ascii.toLowerCase(line); + if (lineLower.startsWith(prefixLower + " ") || lineLower.startsWith(prefixLower + "\t")) { + return Optional.of(line.substring(prefix.length()).trim()); + } + return Optional.empty(); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java new file mode 100644 index 000000000..963e966eb --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java @@ -0,0 +1,313 @@ +// 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.tools; + +import com.google.common.collect.ImmutableMap; +import dev.cel.common.CelValidationException; +import dev.cel.common.types.CelType; +import dev.cel.policy.CelPolicyValidationException; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import dev.cel.verifier.tools.VerificationOptions.OutputFormat; +import java.io.File; +import java.io.OutputStreamWriter; +import java.io.PrintWriter; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.time.Duration; +import java.util.ArrayList; +import java.util.List; +import java.util.Locale; +import java.util.concurrent.Callable; +import picocli.CommandLine; +import picocli.CommandLine.Command; +import picocli.CommandLine.IVersionProvider; +import picocli.CommandLine.Model.CommandSpec; +import picocli.CommandLine.Option; +import picocli.CommandLine.Spec; + +/** Main Picocli entrypoint for the CEL Formal Verification CLI. */ +@Command( + name = "cel-verifier", + mixinStandardHelpOptions = true, + versionProvider = CelVerifierTool.VersionProvider.class, + description = "CEL-Java Formal Verification CLI & REPL Tool", + subcommands = { + CelVerifierTool.CheckSatCommand.class, + CelVerifierTool.CheckValidCommand.class, + CelVerifierTool.VerifyEquivCommand.class, + CelVerifierTool.VerifyPolicyCommand.class, + CelVerifierTool.ReplCommand.class + }) +public final class CelVerifierTool implements Runnable { + + static final int EXIT_CODE_VERIFIED = 0; + static final int EXIT_CODE_VIOLATED = 1; + static final int EXIT_CODE_INCONCLUSIVE = 2; + static final int EXIT_CODE_ERROR = 3; + + static final class VersionProvider implements IVersionProvider { + @Override + public String[] getVersion() { + return new String[] {"cel-verifier " + CelVersion.VERSION}; + } + } + + @Spec private CommandSpec spec; + + @Override + public void run() { + spec.commandLine().usage(spec.commandLine().getOut()); + } + + /** Options shared across all verification commands. */ + abstract static class BaseVerificationCommand implements Callable { + + @Spec private CommandSpec spec; + + PrintWriter out() { + return spec != null + ? spec.commandLine().getOut() + : new PrintWriter(new OutputStreamWriter(System.out, StandardCharsets.UTF_8), true); + } + + PrintWriter err() { + return spec != null + ? spec.commandLine().getErr() + : new PrintWriter(new OutputStreamWriter(System.err, StandardCharsets.UTF_8), true); + } + + @Option( + names = {"--var", "-v"}, + description = + "Declared variable in 'name:type' format (e.g., --var role:string --var port:int)") + List variables = new ArrayList<>(); + + @Option( + names = {"--unknown", "-u"}, + description = + "Identifier to permit evaluating to Unknown (e.g., --unknown request.headers)") + List unknownIdentifiers = new ArrayList<>(); + + @Option( + names = {"--timeout"}, + description = "Solver timeout in seconds (default: 10)") + int timeoutSeconds = (int) VerificationOptions.DEFAULT_TIMEOUT.getSeconds(); + + @Option( + names = {"--unroll-limit"}, + description = "Comprehension unroll limit for BMC (default: 5)") + int comprehensionUnrollLimit = VerificationOptions.DEFAULT_COMPREHENSION_UNROLL_LIMIT; + + @Option( + names = {"--output_format", "-fmt"}, + description = "Output format: TEXT or JSON (default: TEXT)") + String outputFormatStr = VerificationOptions.DEFAULT_OUTPUT_FORMAT.name(); + + @FunctionalInterface + protected interface CommandAction { + int execute(VerificationOptions options, ImmutableMap vars) throws Exception; + } + + protected int executeCommand(CommandAction action) { + return executeCommand("Verification error", action); + } + + protected int executeCommand(String errorPrefix, CommandAction action) { + try { + VerificationOptions options = getOptions(); + ImmutableMap vars = VerificationOptions.parseVariables(variables); + return action.execute(options, vars); + } catch (CelValidationException e) { + err().println("Compilation error:\n" + e.getMessage()); + return EXIT_CODE_ERROR; + } catch (CelPolicyValidationException e) { + err().println("Policy compilation error:\n" + e.getMessage()); + return EXIT_CODE_ERROR; + } catch (Exception e) { + err().println(errorPrefix + ": " + e.getMessage()); + return EXIT_CODE_ERROR; + } + } + + protected VerificationOptions getOptions() { + OutputFormat format = OutputFormat.TEXT; + try { + format = OutputFormat.valueOf(outputFormatStr.toUpperCase(Locale.US)); + } catch (IllegalArgumentException e) { + err().println("Invalid output format '" + outputFormatStr + "'. Defaulting to TEXT."); + } + return VerificationOptions.builder() + .setTimeout(Duration.ofSeconds(timeoutSeconds)) + .setComprehensionUnrollLimit(comprehensionUnrollLimit) + .setUnknownIdentifiers(unknownIdentifiers) + .setOutputFormat(format) + .build(); + } + + protected int handleSingleResult(CelVerificationResult result, OutputFormat format) { + if (format == OutputFormat.JSON) { + out().println(FormatUtils.formatJsonResult(result)); + } else { + out().println(FormatUtils.formatTextResult(result)); + } + + if (result.status() == VerificationStatus.VERIFIED) { + return EXIT_CODE_VERIFIED; + } else if (result.status() == VerificationStatus.VIOLATED) { + return EXIT_CODE_VIOLATED; + } else { + return EXIT_CODE_INCONCLUSIVE; + } + } + } + + /** Base command for commands operating on a single CEL expression. */ + abstract static class SingleExpressionCommand extends BaseVerificationCommand { + @Option( + names = {"--expr", "-e"}, + required = true, + description = "CEL expression string to verify") + String expression = ""; + } + + @Command( + name = "check-sat", + description = "Verify satisfiability of a CEL expression & generate witness model") + static class CheckSatCommand extends SingleExpressionCommand { + + @Override + public Integer call() { + return executeCommand( + (options, vars) -> + handleSingleResult( + CelVerifierToolCore.checkSatisfiable(expression, vars, options), + options.getOutputFormat())); + } + } + + @Command( + name = "check-valid", + description = "Verify validity (isAlwaysTrue) of a CEL expression & generate counterexample") + static class CheckValidCommand extends SingleExpressionCommand { + + @Override + public Integer call() { + return executeCommand( + (options, vars) -> + handleSingleResult( + CelVerifierToolCore.checkValid(expression, vars, options), + options.getOutputFormat())); + } + } + + @Command( + name = "verify-equiv", + description = "Prove logical equivalence between two CEL expressions") + static class VerifyEquivCommand extends BaseVerificationCommand { + + @Option( + names = {"--expr1"}, + required = true, + description = "First CEL expression") + String expressionA = ""; + + @Option( + names = {"--expr2"}, + required = true, + description = "Second CEL expression") + String expressionB = ""; + + @Override + public Integer call() { + return executeCommand( + (options, vars) -> + handleSingleResult( + CelVerifierToolCore.verifyEquivalence(expressionA, expressionB, vars, options), + options.getOutputFormat())); + } + } + + @Command( + name = "verify-policy", + description = "Verify policy invariants defined in a YAML policy file") + static class VerifyPolicyCommand extends BaseVerificationCommand { + + @Option( + names = {"--file", "-f"}, + required = true, + description = "Path to policy YAML file") + String filePath = ""; + + @Override + public Integer call() { + return executeCommand( + "Policy verification error", + (options, vars) -> { + File file = new File(filePath); + if (!file.exists()) { + err().println("File not found: " + filePath); + return EXIT_CODE_ERROR; + } + String yamlContent = + new String(Files.readAllBytes(file.toPath()), StandardCharsets.UTF_8); + + ImmutableMap results = + CelVerifierToolCore.verifyPolicyInvariants(yamlContent, vars, options); + + if (options.getOutputFormat() == OutputFormat.JSON) { + out().println(FormatUtils.formatJsonPolicyResults(file.getName(), results)); + } else { + out().println(FormatUtils.formatTextPolicyResults(file.getName(), results)); + } + + return getPolicyExitCode(results); + }); + } + + private static int getPolicyExitCode(ImmutableMap results) { + boolean anyViolated = false; + boolean anyInconclusive = false; + for (CelVerificationResult res : results.values()) { + if (res.status() == VerificationStatus.VIOLATED) { + anyViolated = true; + } else if (res.status() == VerificationStatus.INCONCLUSIVE) { + anyInconclusive = true; + } + } + + if (anyViolated) { + return EXIT_CODE_VIOLATED; + } else if (anyInconclusive) { + return EXIT_CODE_INCONCLUSIVE; + } + return EXIT_CODE_VERIFIED; + } + } + + @Command(name = "repl", description = "Launch interactive CEL Formal Verification REPL shell") + static class ReplCommand implements Callable { + + @Override + public Integer call() { + return CelVerifierRepl.runInteractiveRepl(); + } + } + + public static void main(String[] args) { + int exitCode = new CommandLine(new CelVerifierTool()).execute(args); + System.exit(exitCode); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java new file mode 100644 index 000000000..75fa5b635 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java @@ -0,0 +1,165 @@ +// 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.tools; + +import com.google.common.collect.ImmutableMap; +import dev.cel.bundle.Cel; +import dev.cel.bundle.CelBuilder; +import dev.cel.bundle.CelFactory; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.CelOptions; +import dev.cel.common.types.CelType; +import dev.cel.compiler.CelCompiler; +import dev.cel.compiler.CelCompilerBuilder; +import dev.cel.compiler.CelCompilerFactory; +import dev.cel.extensions.CelExtensions; +import dev.cel.parser.CelStandardMacro; +import dev.cel.policy.CelPolicy; +import dev.cel.policy.CelPolicyCompiler; +import dev.cel.policy.CelPolicyCompilerFactory; +import dev.cel.policy.CelPolicyParser; +import dev.cel.policy.CelPolicyParserFactory; +import dev.cel.verifier.CelPolicyVerifier; +import dev.cel.verifier.CelPolicyVerifierFactory; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerifier; +import dev.cel.verifier.CelVerifierBuilder; +import dev.cel.verifier.CelVerifierFactory; +import java.util.Map; + +/** Core decoupled engine that executes formal verification operations. */ +final class CelVerifierToolCore { + + private CelVerifierToolCore() {} + + /** Checks if a single CEL expression is satisfiable. */ + static CelVerificationResult checkSatisfiable( + String expression, Map variables, VerificationOptions options) + throws Exception { + CelCompiler compiler = buildCompiler(variables); + CelAbstractSyntaxTree ast = compiler.compile(expression).getAst(); + CelVerifier verifier = buildVerifier(options); + return verifier.isSatisfiable(ast); + } + + /** Checks if a single CEL expression is valid (always true). */ + static CelVerificationResult checkValid( + String expression, Map variables, VerificationOptions options) + throws Exception { + CelCompiler compiler = buildCompiler(variables); + CelAbstractSyntaxTree ast = compiler.compile(expression).getAst(); + CelVerifier verifier = buildVerifier(options); + return verifier.isAlwaysTrue(ast); + } + + /** Proves logical equivalence between two CEL expressions. */ + static CelVerificationResult verifyEquivalence( + String expressionA, + String expressionB, + Map variables, + VerificationOptions options) + throws Exception { + CelCompiler compiler = buildCompiler(variables); + CelAbstractSyntaxTree astA = compiler.compile(expressionA).getAst(); + CelAbstractSyntaxTree astB = compiler.compile(expressionB).getAst(); + CelVerifier verifier = buildVerifier(options); + return verifier.verifyEquivalence(astA, astB); + } + + /** Verifies custom invariants in a YAML policy content string. */ + static ImmutableMap verifyPolicyInvariants( + String yamlContent, Map variables, VerificationOptions options) + throws Exception { + CelPolicyParser parser = CelPolicyParserFactory.newYamlParserBuilder().build(); + CelPolicy policy = parser.parse(yamlContent); + + CelPolicyVerifier policyVerifier = buildPolicyVerifier(variables, options); + return policyVerifier.verifyInvariants(policy); + } + + /** Verifies equivalence between two YAML policy content strings. */ + static CelVerificationResult verifyPolicyEquivalence( + String yamlContentA, + String yamlContentB, + Map variables, + VerificationOptions options) + throws Exception { + CelPolicyParser parser = CelPolicyParserFactory.newYamlParserBuilder().build(); + CelPolicy policyA = parser.parse(yamlContentA); + CelPolicy policyB = parser.parse(yamlContentB); + + CelPolicyVerifier policyVerifier = buildPolicyVerifier(variables, options); + return policyVerifier.verifyEquivalence(policyA, policyB); + } + + static CelCompiler buildCompiler(Map variables) { + CelCompilerBuilder builder = + CelCompilerFactory.standardCelCompilerBuilder() + .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .addLibraries( + CelExtensions.bindings(), + CelExtensions.comprehensions(), + CelExtensions.encoders(CelOptions.DEFAULT), + CelExtensions.lists(), + CelExtensions.math(), + CelExtensions.optional(), + CelExtensions.protos(), + CelExtensions.regex(), + CelExtensions.sets(CelOptions.DEFAULT), + CelExtensions.strings()); + if (variables != null) { + for (Map.Entry entry : variables.entrySet()) { + builder.addVar(entry.getKey(), entry.getValue()); + } + } + return builder.build(); + } + + static CelVerifier buildVerifier(VerificationOptions options) { + CelVerifierBuilder builder = + CelVerifierFactory.newVerifier() + .setTimeout(options.getTimeout()) + .setComprehensionUnrollLimit(options.getComprehensionUnrollLimit()); + + for (String unknown : options.getUnknownIdentifiers()) { + builder.addUnknownIdentifier(unknown); + } + return builder.build(); + } + + private static CelPolicyVerifier buildPolicyVerifier( + Map variables, VerificationOptions options) { + CelBuilder celBuilder = + CelFactory.plannerCelBuilder() + .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .addCompilerLibraries( + CelExtensions.optional(), + CelExtensions.bindings(), + CelExtensions.encoders(CelOptions.DEFAULT), + CelExtensions.math(), + CelExtensions.strings()); + if (variables != null) { + for (Map.Entry entry : variables.entrySet()) { + celBuilder.addVar(entry.getKey(), entry.getValue()); + } + } + Cel celBundle = celBuilder.build(); + CelPolicyCompiler policyCompiler = + CelPolicyCompilerFactory.newPolicyCompiler(celBundle).build(); + CelVerifier astVerifier = buildVerifier(options); + + return CelPolicyVerifierFactory.newVerifier(policyCompiler, astVerifier).build(); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java b/verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java new file mode 100644 index 000000000..d1666cd55 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java @@ -0,0 +1,146 @@ +// 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.tools; + +import com.google.common.collect.ImmutableMap; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import java.util.Map; + +/** Utilities for formatting verification output (ANSI text & JSON). */ +final class FormatUtils { + + // ANSI Escape Codes for formatting text + static final String ANSI_RESET = "\u001B[0m"; + static final String ANSI_BOLD = "\u001B[1m"; + static final String ANSI_GREEN = "\u001B[32m"; + static final String ANSI_RED = "\u001B[31m"; + static final String ANSI_YELLOW = "\u001B[33m"; + static final String ANSI_CYAN = "\u001B[36m"; + + private FormatUtils() {} + + /** Formats a single CelVerificationResult for human-readable console display with ANSI color. */ + static String formatTextResult(CelVerificationResult result) { + StringBuilder sb = new StringBuilder(); + String statusColor = getStatusColor(result.status()); + sb.append(statusColor) + .append(ANSI_BOLD) + .append("[") + .append(result.status()) + .append("]") + .append(ANSI_RESET); + + if (result.message() != null && !result.message().isEmpty()) { + sb.append(" ").append(result.message()); + } + + return sb.toString(); + } + + /** Formats policy invariant verification results for human-readable console display. */ + static String formatTextPolicyResults( + String policyName, ImmutableMap results) { + StringBuilder sb = new StringBuilder(); + sb.append(ANSI_BOLD) + .append("Policy Invariant Verification for '") + .append(policyName) + .append("':\n") + .append(ANSI_RESET); + + for (Map.Entry entry : results.entrySet()) { + String id = entry.getKey(); + CelVerificationResult result = entry.getValue(); + String symbol = result.status() == VerificationStatus.VERIFIED ? "✓" : "✗"; + String color = getStatusColor(result.status()); + + sb.append(" ") + .append(color) + .append(symbol) + .append(" Invariant '") + .append(id) + .append("': ") + .append(result.status()) + .append(ANSI_RESET); + + if (result.message() != null && !result.message().isEmpty()) { + sb.append("\n ").append(result.message().replace("\n", "\n ")); + } + sb.append("\n"); + } + return sb.toString().trim(); + } + + /** Formats a single CelVerificationResult as structured JSON. */ + static String formatJsonResult(CelVerificationResult result) { + StringBuilder sb = new StringBuilder(); + sb.append("{\n"); + sb.append(" \"status\": \"").append(result.status()).append("\",\n"); + sb.append(" \"message\": \"").append(escapeJson(result.message())).append("\"\n"); + sb.append("}"); + return sb.toString(); + } + + /** Formats policy invariant verification results as structured JSON. */ + static String formatJsonPolicyResults( + String policyName, ImmutableMap results) { + StringBuilder sb = new StringBuilder(); + sb.append("{\n"); + sb.append(" \"policyName\": \"").append(escapeJson(policyName)).append("\",\n"); + sb.append(" \"invariants\": [\n"); + + int count = 0; + for (Map.Entry entry : results.entrySet()) { + count++; + String id = entry.getKey(); + CelVerificationResult res = entry.getValue(); + sb.append(" {\n"); + sb.append(" \"id\": \"").append(escapeJson(id)).append("\",\n"); + sb.append(" \"status\": \"").append(res.status()).append("\",\n"); + sb.append(" \"message\": \"").append(escapeJson(res.message())).append("\"\n"); + sb.append(" }").append(count < results.size() ? "," : "").append("\n"); + } + + sb.append(" ]\n"); + sb.append("}"); + return sb.toString(); + } + + private static String getStatusColor(VerificationStatus status) { + switch (status) { + case VERIFIED: + return ANSI_GREEN; + case VIOLATED: + return ANSI_RED; + case INCONCLUSIVE: + return ANSI_YELLOW; + } + return ANSI_RESET; + } + + private static String escapeJson(String input) { + if (input == null) { + return ""; + } + return input + .replace("\\", "\\\\") + .replace("\"", "\\\"") + .replace("\b", "\\b") + .replace("\f", "\\f") + .replace("\n", "\\n") + .replace("\r", "\\r") + .replace("\t", "\\t"); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java new file mode 100644 index 000000000..f2b3bf742 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java @@ -0,0 +1,223 @@ +// 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.tools; + +import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import com.google.errorprone.annotations.CanIgnoreReturnValue; +import dev.cel.common.types.CelType; +import dev.cel.common.types.ListType; +import dev.cel.common.types.MapType; +import dev.cel.common.types.SimpleType; +import java.time.Duration; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Locale; +import java.util.Map; + +/** Configuration options for CEL verification CLI operations. */ +final class VerificationOptions { + + /** Output format for verification CLI results. */ + enum OutputFormat { + TEXT, + JSON + } + + static final Duration DEFAULT_TIMEOUT = Duration.ofSeconds(10); + static final int DEFAULT_COMPREHENSION_UNROLL_LIMIT = 5; + static final OutputFormat DEFAULT_OUTPUT_FORMAT = OutputFormat.TEXT; + + private final Duration timeout; + private final int comprehensionUnrollLimit; + private final ImmutableList unknownIdentifiers; + private final OutputFormat outputFormat; + + Duration getTimeout() { + return timeout; + } + + int getComprehensionUnrollLimit() { + return comprehensionUnrollLimit; + } + + ImmutableList getUnknownIdentifiers() { + return unknownIdentifiers; + } + + OutputFormat getOutputFormat() { + return outputFormat; + } + + static Builder builder() { + return new Builder(); + } + + /** A builder for {@link VerificationOptions}. */ + static final class Builder { + private Duration timeout = DEFAULT_TIMEOUT; + private int comprehensionUnrollLimit = DEFAULT_COMPREHENSION_UNROLL_LIMIT; + private ImmutableList unknownIdentifiers = ImmutableList.of(); + private OutputFormat outputFormat = DEFAULT_OUTPUT_FORMAT; + + @CanIgnoreReturnValue + Builder setTimeout(Duration timeout) { + this.timeout = Preconditions.checkNotNull(timeout); + return this; + } + + @CanIgnoreReturnValue + Builder setComprehensionUnrollLimit(int unrollLimit) { + Preconditions.checkArgument(unrollLimit >= 0, "unrollLimit must be non-negative"); + this.comprehensionUnrollLimit = unrollLimit; + return this; + } + + @CanIgnoreReturnValue + Builder setUnknownIdentifiers(List unknownIdentifiers) { + this.unknownIdentifiers = ImmutableList.copyOf(unknownIdentifiers); + return this; + } + + @CanIgnoreReturnValue + Builder setOutputFormat(OutputFormat outputFormat) { + this.outputFormat = Preconditions.checkNotNull(outputFormat); + return this; + } + + VerificationOptions build() { + return new VerificationOptions( + timeout, comprehensionUnrollLimit, unknownIdentifiers, outputFormat); + } + } + + private VerificationOptions( + Duration timeout, + int comprehensionUnrollLimit, + ImmutableList unknownIdentifiers, + OutputFormat outputFormat) { + this.timeout = timeout; + this.comprehensionUnrollLimit = comprehensionUnrollLimit; + this.unknownIdentifiers = unknownIdentifiers; + this.outputFormat = outputFormat; + } + + /** + * Helper utility to parse CLI variable definitions formatted as "name:type" (e.g. "x:int", + * "role:string", "is_admin:bool"). + */ + static ImmutableMap parseVariables(List varSpecs) { + if (varSpecs == null || varSpecs.isEmpty()) { + return ImmutableMap.of(); + } + Map vars = new HashMap<>(); + for (String varSpec : varSpecs) { + Preconditions.checkNotNull(varSpec, "Variable specification cannot be null."); + String[] parts = varSpec.split(":", 2); + if (parts.length != 2) { + throw new IllegalArgumentException( + "Invalid variable specification: '" + + varSpec + + "'. Expected format 'name:type' (e.g., 'x:int')."); + } + String name = parts[0].trim(); + if (name.isEmpty()) { + throw new IllegalArgumentException( + "Invalid variable specification: '" + varSpec + "'. Variable name cannot be empty."); + } + String typeStr = parts[1].trim().toLowerCase(Locale.US); + CelType type = parseCelType(typeStr); + vars.put(name, type); + } + return ImmutableMap.copyOf(vars); + } + + static CelType parseCelType(String typeStr) { + Preconditions.checkNotNull(typeStr, "Type string cannot be null."); + String str = typeStr.trim().toLowerCase(Locale.US); + + if (str.startsWith("list<") && str.endsWith(">")) { + String inner = str.substring(5, str.length() - 1).trim(); + CelType elemType = parseCelType(inner); + return ListType.create(elemType); + } + + if (str.startsWith("map<") && str.endsWith(">")) { + String inner = str.substring(4, str.length() - 1).trim(); + List parts = splitGenericArgs(inner); + if (parts.size() != 2) { + throw new IllegalArgumentException( + "Invalid map type format: '" + + typeStr + + "'. Expected format 'map' (e.g., 'map')."); + } + CelType keyType = parseCelType(parts.get(0)); + CelType valueType = parseCelType(parts.get(1)); + return MapType.create(keyType, valueType); + } + + switch (str) { + case "int": + return SimpleType.INT; + case "uint": + return SimpleType.UINT; + case "string": + return SimpleType.STRING; + case "bool": + case "boolean": + return SimpleType.BOOL; + case "double": + case "float": + return SimpleType.DOUBLE; + case "bytes": + return SimpleType.BYTES; + case "dyn": + return SimpleType.DYN; + default: + throw new IllegalArgumentException( + "Unsupported type for CLI variable declaration: '" + + typeStr + + "'. Supported types: int, uint, string, bool, double, bytes, dyn, list, map."); + } + } + + private static List splitGenericArgs(String inner) { + List result = new ArrayList<>(); + int depth = 0; + StringBuilder current = new StringBuilder(); + for (int i = 0; i < inner.length(); i++) { + char c = inner.charAt(i); + if (c == '<') { + depth++; + current.append(c); + } else if (c == '>') { + depth--; + current.append(c); + } else if (c == ',' && depth == 0) { + result.add(current.toString().trim()); + current.setLength(0); + } else { + current.append(c); + } + } + if (current.length() > 0) { + result.add(current.toString().trim()); + } + return result; + } +} diff --git a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel index 9e7f0ed15..f1669c486 100644 --- a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel @@ -9,7 +9,7 @@ java_library( name = "tests", testonly = True, srcs = glob( - ["**/*.java"], + ["*.java"], ), compatible_with = [], data = [ @@ -47,6 +47,7 @@ java_library( "//:java_truth", "@maven//:tools_aqua_z3_turnkey", "//verifier", + "//verifier:numeric_bounds", "//verifier:policy_verifier", "//verifier:policy_verifier_factory", "//verifier:type_system", @@ -60,7 +61,7 @@ java_library( junit4_test_suites( name = "test_suites", - shard_count = 4, + shard_count = 8, sizes = [ "small", "medium", diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index e8783af86..0492ff7ab 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -139,30 +139,59 @@ 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", + "string_int_map = \\{[^}]*,[^}]*\\}"), + 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; + final ImmutableList expectedFragments; - IsSatisfiableTestCase(String expr) { + IsSatisfiableTestCase(String expr, String... expectedFragments) { this.expr = expr; + this.expectedFragments = ImmutableList.copyOf(expectedFragments); } } @@ -183,6 +212,9 @@ public void isSatisfiable_success(@TestParameter IsSatisfiableTestCase testCase) CelVerificationResult result = VERIFIER.isSatisfiable(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + for (String fragment : testCase.expectedFragments) { + assertThat(result.message()).containsMatch(fragment); + } } @Test @@ -197,6 +229,93 @@ public void isSatisfiable_withVariable_returnsSatisfyingModel() throws Exception assertThat(result.message()).containsMatch("x = (?:[6-9]|[1-9]\\d+)"); } + @Test + public void isSatisfiable_mapNoContainerError_returnsSatisfyingModel() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("string_int_map.size() == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("Condition is satisfiable."); + assertThat(result.message()).contains("Satisfying input:"); + assertThat(result.message()).contains("string_int_map = {"); + assertThat(result.message()).doesNotContain("Error"); + } + + @Test + public void isSatisfiable_listNoContainerError_returnsSatisfyingModel() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("dyn_list.size() == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("Condition is satisfiable."); + assertThat(result.message()).contains("Satisfying input:"); + assertThat(result.message()).contains("dyn_list = ["); + assertThat(result.message()).doesNotContain("Error"); + } + + @Test + public void isSatisfiable_dynMapNoContainerError_returnsSatisfyingModel() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("dyn_map.size() == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("Condition is satisfiable."); + assertThat(result.message()).contains("Satisfying input:"); + assertThat(result.message()).contains("dyn_map = {"); + assertThat(result.message()).doesNotContain("Error"); + } + + @Test + public void counterexample_nullValueFormattedAsNull() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("unknown_var == 3u && request == null").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + 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"), + DYN_LIST_ELEMENT("size(dyn_list) == 1 && dyn_list[0] == 'impossible_value'"), + DYN_MAP_VALUE("size(dyn_map) == 1 && dyn_map['a'] == 'impossible_value'"), + STRUCT_FIELD_VALUE("test_all_types.single_int64 == 12345 && false"), + ; + + final String expr; + + CounterexampleNeverErrorTestCase(String expr) { + this.expr = expr; + } + } + + @Test + public void isAlwaysTrue_counterexampleNeverContainsError( + @TestParameter CounterexampleNeverErrorTestCase testCase) throws Exception { + CelAbstractSyntaxTree ast = CEL.compile(testCase.expr).getAst(); + + CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.message()).doesNotContain("Error"); + } + @Test public void isSatisfiable_unconditional_returnsUnconditionalMessage() throws Exception { CelAbstractSyntaxTree ast = CEL.compile("1 + 1 == 2").getAst(); @@ -291,7 +410,37 @@ private enum IsUnsatisfiableTestCase { 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"), - DYN_INT_NOT_DURATION("dyn(1) == dyn(duration('1s'))"); + DYN_INT_NOT_DURATION("dyn(1) == dyn(duration('1s'))"), + DYNAMIC_MAP_DUPLICATE_KEYS_CONTRADICTION( + "size(string_int_map) == 2 && string_int_map.all(k, k == 'a')"), + EMPTY_MAP_WITH_KEY_IN("string_int_map.size() == 0 && 'foo' in string_int_map"), + KEY_IN_EMPTY_MAP("('x' in string_int_map) && string_int_map.size() == 0"), + EMPTY_MAP_AND_LIST_WITH_KEY_IN( + "int_list.size() == string_int_map.size() && int_list.size() == 0 && 'a' in" + + " string_int_map"), + MAP_SIZE_ONE_TWO_KEYS( + "string_int_map.size() == 1 && string_int_map['a'] == 1 && string_int_map['b'] == 2"), + MAP_SIZE_LESS_THAN_TWO_TWO_KEYS( + "string_int_map['foo'] == 10 && string_int_map['bar'] == 20 && string_int_map.size() < 2"), + MAP_SIZE_ONE_SUM_TWO_KEYS( + "string_int_map['a'] + string_int_map['b'] == 10 && string_int_map.size() == 1"), + MAP_SIZE_ONE_TWO_EQUAL_KEYS( + "string_int_map.size() == 1 && string_int_map['foo'] == 10 && string_int_map['bar'] == 10"), + MAP_SIZE_TWO_THREE_KEYS( + "string_int_map['k1'] == 1 && string_int_map['k2'] == 2 && string_int_map['k3'] == 3 &&" + + " 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; @@ -409,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]}"), @@ -586,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"), @@ -618,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"), @@ -747,6 +913,18 @@ private enum IsAlwaysTrueTestCase { UINT64_BOUNDS_ALWAYS_TRUE("u <= 18446744073709551615u && u >= 0u"), MODULO_INT64_MIN_INT_BY_NEG_ONE_ALWAYS_ZERO( "x == -9223372036854775808 && y == -1 ? x % y == 0 : true"), + 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; @@ -899,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 = @@ -1266,7 +1456,7 @@ private enum IsAlwaysTrueViolationTestCase { + "? dyn_map[1 + 1] == [] : true", "Condition is not always true\\.", "Counterexample input:", - "dyn_map = \\{\\}"), + "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)", @@ -1420,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; @@ -1524,6 +1717,9 @@ private enum EquivalenceTestCase { MACRO_EXISTS_ONE_EQUIVALENT( "[1, 2, 3].exists_one(x, x == 2)", "(1 == 2 ? 1 : 0) + (2 == 2 ? 1 : 0) + (3 == 2 ? 1 : 0) == 1"), + TIMESTAMP_CONVERSION_OVERFLOW_EQUIVALENCE( + "timestamp(string_var) <= timestamp(253402300799)", + "timestamp(string_var) == timestamp(string_var)"), TIMESTAMP_MATH_SUBTRACT_TS( "timestamp(900000) - timestamp(100)", "timestamp(899900) - timestamp(0)"), TIMESTAMP_MATH_COMMUTATIVITY( @@ -1775,7 +1971,16 @@ private enum EquivalenceTestCase { JSON_VALUE_OPTIONAL_NULL_VALUE_OF("google.protobuf.Value{?null_value: optional.of(0)}", "null"), 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()"); + OPTIONAL_INDEX_UNWRAPPING_NONE("optional.none()[?0]", "optional.none()"), + 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; @@ -2620,6 +2825,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 = @@ -2858,3 +3107,4 @@ public void verifyImplication_symbolicNan_crossNumericComparisonReturnsFalse() t assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); } } + diff --git a/verifier/src/test/java/dev/cel/verifier/tools/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/tools/BUILD.bazel new file mode 100644 index 000000000..6077e4950 --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/BUILD.bazel @@ -0,0 +1,31 @@ +load("@rules_java//java:defs.bzl", "java_library") +load("//:testing.bzl", "junit4_test_suites") + +package( + default_applicable_licenses = ["//:license"], +) + +java_library( + name = "tests", + testonly = True, + srcs = glob(["*.java"]), + deps = [ + "//:java_truth", + "//common/types", + "//common/types:type_providers", + "//verifier", + "//verifier/tools", + "@maven//:com_google_guava_guava", + "@maven//:info_picocli_picocli", + "@maven//:junit_junit", + ], +) + +junit4_test_suites( + name = "test_suites", + sizes = [ + "small", + ], + src_dir = "src/test/java", + deps = [":tests"], +) diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java new file mode 100644 index 000000000..5b289c39a --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java @@ -0,0 +1,194 @@ +// 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.tools; + +import static com.google.common.truth.Truth.assertThat; +import static java.nio.charset.StandardCharsets.UTF_8; + +import java.io.BufferedReader; +import java.io.ByteArrayOutputStream; +import java.io.PrintStream; +import java.io.StringReader; +import org.junit.Before; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.JUnit4; + +@RunWith(JUnit4.class) +public final class CelVerifierReplTest { + + @Before + public void setUp() { + System.setProperty("z3.skipLibraryLoad", "true"); + } + + @SuppressWarnings({"PreferCharsetOverload", "JdkObsolete"}) + private String[] runReplWithCommands(String... commands) throws Exception { + String input = String.join("\n", commands) + "\n"; + BufferedReader reader = new BufferedReader(new StringReader(input)); + ByteArrayOutputStream outStream = new ByteArrayOutputStream(); + ByteArrayOutputStream errStream = new ByteArrayOutputStream(); + PrintStream out = new PrintStream(outStream, true, UTF_8.name()); + PrintStream err = new PrintStream(errStream, true, UTF_8.name()); + + CelVerifierRepl.runRepl(reader, out, err); + + return new String[] { + new String(outStream.toByteArray(), UTF_8), new String(errStream.toByteArray(), UTF_8) + }; + } + + @Test + public void repl_quitAndExit() throws Exception { + String[] output1 = runReplWithCommands(":quit"); + assertThat(output1[0]).contains("Goodbye!"); + + String[] output2 = runReplWithCommands(":exit"); + assertThat(output2[0]).contains("Goodbye!"); + } + + @Test + public void repl_helpCommands() throws Exception { + String[] output = + runReplWithCommands( + ":help", + ":help var", + ":help unknown", + ":help timeout", + ":help unroll", + ":help sat", + ":help valid", + ":help equiv", + ":help non_existent_topic", + ":quit"); + assertThat(output[0]).contains("REPL Commands:"); + assertThat(output[0]).contains("Command: :var "); + assertThat(output[0]).contains("Command: :unknown "); + assertThat(output[0]).contains("Command: :timeout "); + assertThat(output[0]).contains("Command: :unroll "); + assertThat(output[0]).contains("Query: sat "); + assertThat(output[0]).contains("Query: valid "); + assertThat(output[0]).contains("Query: equiv <=> "); + } + + @Test + public void repl_varDeclarations() throws Exception { + String[] output = + runReplWithCommands( + ":var role string", + ":var port int", + ":var scores map", + ":var tags list", + ":vars", + ":quit"); + assertThat(output[0]).contains("Variable declared: role : string"); + assertThat(output[0]).contains("Variable declared: port : int"); + assertThat(output[0]).contains("Variable declared: scores : map(string, int)"); + assertThat(output[0]).contains("Variable declared: tags : list(string)"); + assertThat(output[0]).contains("Variables (4):"); + } + + @Test + public void repl_unknownIdentifiers() throws Exception { + String[] output = + runReplWithCommands(":unknown request.headers", ":unknown request.auth", ":vars", ":quit"); + assertThat(output[0]).contains("Added unknown identifier: 'request.headers'"); + assertThat(output[0]).contains("Added unknown identifier: 'request.auth'"); + assertThat(output[0]).contains("Unknowns: [request.headers, request.auth]"); + } + + @Test + public void repl_timeoutConfiguration() throws Exception { + String[] output = + runReplWithCommands( + ":timeout 15", ":vars", ":timeout -5", ":timeout abc", ":timeout", ":quit"); + assertThat(output[0]).contains("Timeout set to 15s."); + assertThat(output[0]).contains("Timeout: 15s"); + assertThat(output[1]).contains("Timeout must be a positive integer."); + assertThat(output[1]).contains("Invalid timeout value."); + assertThat(output[1]).contains("Usage: :timeout "); + } + + @Test + public void repl_unrollConfiguration() throws Exception { + String[] output = + runReplWithCommands(":unroll 10", ":vars", ":unroll -1", ":unroll xyz", ":unroll", ":quit"); + assertThat(output[0]).contains("Comprehension unroll limit set to 10."); + assertThat(output[0]).contains("Unroll limit: 10"); + assertThat(output[1]).contains("Unroll limit must be non-negative."); + assertThat(output[1]).contains("Invalid unroll limit value."); + assertThat(output[1]).contains("Usage: :unroll "); + } + + @Test + public void repl_sessionStateAndClear() throws Exception { + String[] output = + runReplWithCommands( + ":var role string", ":unknown req.headers", ":vars", ":clear", ":vars", ":quit"); + assertThat(output[0]).contains("Variables (1):"); + assertThat(output[0]).contains("Session state reset."); + assertThat(output[0]).contains("Variables (0):"); + assertThat(output[0]).contains("Unknowns: none"); + } + + @Test + public void repl_satQueries() throws Exception { + String[] output = + runReplWithCommands(":var port int", "sat port > 1024", "port > 1024", "sat", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[1]).contains("Usage: sat "); + } + + @Test + public void repl_validQueries() throws Exception { + String[] output = + runReplWithCommands(":var x int", "valid x > 0 || x <= 0", "valid x > 0", "valid", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[0]).contains("[VIOLATED]"); + assertThat(output[1]).contains("Usage: valid "); + } + + @Test + public void repl_equivQueries() throws Exception { + String[] output = + runReplWithCommands(":var x int", "equiv x > 10 <=> 10 < x", "equiv x > 10", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + 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 = + runReplWithCommands( + ":unknowncommand", + ":var", + ":var invalid_spec", + ":var x foo_type", + ":unknown", + "invalid + + syntax", + ":quit"); + assertThat(output[1]).contains("Unknown command: :unknowncommand"); + assertThat(output[1]).contains("Usage: :var "); + assertThat(output[1]).contains("Unsupported type"); + assertThat(output[1]).contains("Usage: :unknown "); + assertThat(output[1]).contains("Compilation error"); + } +} diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java new file mode 100644 index 000000000..bfc794c28 --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java @@ -0,0 +1,578 @@ +// 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.tools; + +import static com.google.common.truth.Truth.assertThat; +import static org.junit.Assert.assertThrows; + +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import dev.cel.common.types.CelType; +import dev.cel.common.types.ListType; +import dev.cel.common.types.MapType; +import dev.cel.common.types.SimpleType; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import java.io.File; +import java.io.PrintWriter; +import java.io.StringWriter; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.time.Duration; +import java.util.Arrays; +import org.junit.Before; +import org.junit.Rule; +import org.junit.Test; +import org.junit.rules.TemporaryFolder; +import org.junit.runner.RunWith; +import org.junit.runners.JUnit4; +import picocli.CommandLine; + +@RunWith(JUnit4.class) +public final class CelVerifierToolTest { + + @Rule public TemporaryFolder tempFolder = new TemporaryFolder(); + + @Before + public void setUp() { + System.setProperty("z3.skipLibraryLoad", "true"); + } + + private String executeToolWithOutput(String... args) { + StringWriter out = new StringWriter(); + PrintWriter pw = new PrintWriter(out); + CommandLine cmd = new CommandLine(new CelVerifierTool()); + cmd.setOut(pw); + cmd.setErr(pw); + cmd.execute(args); + return out.toString(); + } + + @Test + public void celVerifierTool_checkSat_jsonOutputFormat() { + String output = + executeToolWithOutput( + "check-sat", "--expr", "x > 0", "--var", "x:int", "--output_format", "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); + assertThat(output).contains("satisfiable"); + } + + @Test + public void celVerifierTool_checkSat_textOutputFormat() { + String output = + executeToolWithOutput("check-sat", "--expr", "x > 0", "--var", "x:int", "-fmt", "text"); + assertThat(output).contains("[VERIFIED]"); + assertThat(output).contains("satisfiable"); + } + + @Test + public void celVerifierTool_checkSat_withDynVariable() { + String output = + executeToolWithOutput( + "check-sat", "--expr", "x == 'hello'", "--var", "x:dyn", "-fmt", "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_checkSat_withUnknownOption() { + String output = + executeToolWithOutput( + "check-sat", + "--expr", + "request.headers != null", + "--var", + "request:map", + "-u", + "request.headers", + "-fmt", + "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_checkSat_withTimeoutAndUnrollLimit() { + String output = + executeToolWithOutput( + "check-sat", + "--expr", + "[1, 2, 3].all(x, x > 0)", + "--timeout", + "5", + "--unroll-limit", + "5", + "-fmt", + "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_verifyPolicy_fileNotFound() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", "non_existent_policy.yaml"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_ERROR); + } + + @Test + public void parseVariables_success() { + ImmutableMap vars = + VerificationOptions.parseVariables( + Arrays.asList( + "x:int", + "role:string", + "is_admin:bool", + "tags:list", + "scores:map")); + assertThat(vars).containsEntry("x", SimpleType.INT); + assertThat(vars).containsEntry("role", SimpleType.STRING); + assertThat(vars).containsEntry("is_admin", SimpleType.BOOL); + assertThat(vars).containsEntry("tags", ListType.create(SimpleType.STRING)); + assertThat(vars).containsEntry("scores", MapType.create(SimpleType.STRING, SimpleType.INT)); + } + + @Test + public void parseVariables_allTypesIncludingDyn() { + ImmutableMap vars = + VerificationOptions.parseVariables( + Arrays.asList( + "u:uint", + "d:double", + "fl:float", + "b:bytes", + "dyn_val:dyn", + "flag:boolean", + "nested_list:list", + "nested_map:map")); + assertThat(vars).containsEntry("u", SimpleType.UINT); + assertThat(vars).containsEntry("d", SimpleType.DOUBLE); + assertThat(vars).containsEntry("fl", SimpleType.DOUBLE); + assertThat(vars).containsEntry("b", SimpleType.BYTES); + assertThat(vars).containsEntry("dyn_val", SimpleType.DYN); + assertThat(vars).containsEntry("flag", SimpleType.BOOL); + assertThat(vars).containsEntry("nested_list", ListType.create(SimpleType.DYN)); + assertThat(vars).containsEntry("nested_map", MapType.create(SimpleType.STRING, SimpleType.DYN)); + } + + @Test + public void parseVariables_invalidFormat_throws() { + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList("x_no_colon"))); + } + + @Test + public void parseVariables_unsupportedType_throws() { + IllegalArgumentException ex = + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList("x:foo_bar"))); + assertThat(ex) + .hasMessageThat() + .contains("Supported types: int, uint, string, bool, double, bytes, dyn"); + } + + @Test + public void parseVariables_invalidMapFormat_throws() { + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList("x:map"))); + } + + @Test + public void parseVariables_emptyOrNull_returnsEmptyMap() { + assertThat(VerificationOptions.parseVariables(null)).isEmpty(); + assertThat(VerificationOptions.parseVariables(ImmutableList.of())).isEmpty(); + } + + @Test + public void parseVariables_nestedTypes() { + ImmutableMap vars = + VerificationOptions.parseVariables( + Arrays.asList( + "nested_map:map>", + "nested_list_map:map>")); + assertThat(vars) + .containsEntry( + "nested_map", + MapType.create(SimpleType.STRING, MapType.create(SimpleType.STRING, SimpleType.INT))); + assertThat(vars) + .containsEntry( + "nested_list_map", MapType.create(SimpleType.STRING, ListType.create(SimpleType.INT))); + } + + @Test + public void parseVariables_emptyString_throws() { + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList(""))); + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList(" "))); + } + + @Test + public void parseVariables_nullElement_throws() { + assertThrows( + NullPointerException.class, + () -> VerificationOptions.parseVariables(Arrays.asList((String) null))); + } + + @Test + public void checkSatisfiable_satisfiable() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = + ImmutableMap.of("role", SimpleType.STRING, "port", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable("role == 'editor' && port > 1024", vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("satisfiable"); + } + + @Test + public void checkValid_valid() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("x", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.checkValid("x > 10 || x <= 10", vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void verifyEquivalence_equivalent() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("x", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.verifyEquivalence("x > 10", "10 < x", vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void verifyPolicyInvariants_success() throws Exception { + String yamlPolicy = + "name: secure_access_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: port_check\n" + + " assert:\n" + + " - port == 80 || port != 80\n"; + + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("port", SimpleType.INT); + + ImmutableMap results = + CelVerifierToolCore.verifyPolicyInvariants(yamlPolicy, vars, options); + + assertThat(results).containsKey("port_check"); + assertThat(results.get("port_check").status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void verifyPolicyEquivalence_equivalent() throws Exception { + String policyA = + "name: policy_a\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n"; + + String policyB = + "name: policy_b\n" + + "rule:\n" + + " match:\n" + + " - condition: 80 == port\n" + + " output: 'true'\n" + + " - output: 'false'\n"; + + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("port", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.verifyPolicyEquivalence(policyA, policyB, vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void formatTextPolicyResults_verifiedAndViolated() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult verifiedRes = + CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + CelVerificationResult violatedRes = + CelVerifierToolCore.checkValid("x > 0", ImmutableMap.of("x", SimpleType.INT), options); + + ImmutableMap results = + ImmutableMap.of("inv_1", verifiedRes, "inv_2", violatedRes); + + String text = FormatUtils.formatTextPolicyResults("test_policy", results); + assertThat(text).contains("Policy Invariant Verification for 'test_policy':"); + assertThat(text).contains("✓ Invariant 'inv_1': VERIFIED"); + assertThat(text).contains("✗ Invariant 'inv_2': VIOLATED"); + } + + @Test + public void formatJsonPolicyResults_structuredJson() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + + ImmutableMap results = ImmutableMap.of("inv_1", result); + + String json = FormatUtils.formatJsonPolicyResults("my_policy", results); + assertThat(json).contains("\"policyName\": \"my_policy\""); + assertThat(json).contains("\"id\": \"inv_1\""); + assertThat(json).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_verifyPolicy_success() throws Exception { + File policyFile = tempFolder.newFile("test_policy.yaml"); + String yamlContent = + "name: test_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: port_check\n" + + " assert:\n" + + " - port == 80 || port != 80\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + String output = + executeToolWithOutput( + "verify-policy", + "--file", + policyFile.getAbsolutePath(), + "--var", + "port:int", + "-fmt", + "json"); + + assertThat(output).contains("\"policyName\": \"test_policy.yaml\""); + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_verifyPolicy_violated() throws Exception { + File policyFile = tempFolder.newFile("violated_policy.yaml"); + String yamlContent = + "name: violated_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: invalid_check\n" + + " assert:\n" + + " - port > 1024\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", policyFile.getAbsolutePath(), "--var", "port:int"); + + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VIOLATED); + } + + @Test + public void celVerifierTool_verifyPolicy_multipleInvariants_oneViolated() throws Exception { + File policyFile = tempFolder.newFile("multi_invariant_policy.yaml"); + String yamlContent = + "name: multi_invariant_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: valid_check\n" + + " assert:\n" + + " - port == 80 || port != 80\n" + + " - id: invalid_check\n" + + " assert:\n" + + " - port > 1024\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", policyFile.getAbsolutePath(), "--var", "port:int"); + + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VIOLATED); + } + + @Test + public void celVerifierTool_verifyPolicy_multipleInvariants_allVerified() throws Exception { + File policyFile = tempFolder.newFile("multi_verified_policy.yaml"); + String yamlContent = + "name: multi_verified_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: check_1\n" + + " assert:\n" + + " - port == 80 || port != 80\n" + + " - id: check_2\n" + + " assert:\n" + + " - port > 0 || port <= 0\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", policyFile.getAbsolutePath(), "--var", "port:int"); + + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VERIFIED); + } + + @Test + public void formatUtils_jsonResult() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + String json = FormatUtils.formatJsonResult(result); + assertThat(json).contains("\"status\": \"VERIFIED\""); + assertThat(json).contains("satisfiable"); + } + + @Test + public void celVerifierTool_checkSat_verified() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("check-sat", "--expr", "x > 0", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VERIFIED); + } + + @Test + public void celVerifierTool_checkValid_violated() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("check-valid", "--expr", "x > 0", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VIOLATED); + } + + @Test + public void celVerifierTool_verifyEquiv_verified() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-equiv", "--expr1", "x > 10", "--expr2", "10 < x", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VERIFIED); + } + + @Test + public void celVerifierTool_checkSat_compilationError() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("check-sat", "--expr", "invalid + + syntax", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_ERROR); + } + + @Test + public void celVerifierTool_checkValid_inconclusive() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("check-valid", "--expr", "int('123') == 123"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_INCONCLUSIVE); + } + + @Test + public void celVerifierTool_verifyPolicy_inconclusive() throws Exception { + File policyFile = tempFolder.newFile("inconclusive_policy.yaml"); + String yamlContent = + "name: inconclusive_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: approx_check\n" + + " assert:\n" + + " - int('123') == 123\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", policyFile.getAbsolutePath(), "--var", "port:int"); + + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_INCONCLUSIVE); + } + + @Test + public void celVerifierTool_invalidOutputFormat_defaultsToText() { + String output = + executeToolWithOutput( + "check-sat", "--expr", "x > 0", "--var", "x:int", "-fmt", "invalid_fmt"); + assertThat(output).contains("[VERIFIED]"); + } + + @Test + public void formatTextPolicyResults_inconclusive() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult res = + CelVerifierToolCore.checkValid("int('123') == 123", ImmutableMap.of(), options); + + String text = FormatUtils.formatTextPolicyResults("test_policy", ImmutableMap.of("inv_1", res)); + assertThat(text).contains("Invariant 'inv_1': INCONCLUSIVE"); + } + + @Test + public void formatJson_escapesSpecialCharacters() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult res = + CelVerifierToolCore.checkValid("int('123') == 123", ImmutableMap.of(), options); + String json = + FormatUtils.formatJsonPolicyResults( + "policy_with_\"quote\"\nand_newline", ImmutableMap.of("inv\ttab", res)); + assertThat(json).contains("policy_with_\\\"quote\\\"\\nand_newline"); + assertThat(json).contains("inv\\ttab"); + } + + @Test + public void celVerifierTool_version() { + int exitCode = new CommandLine(new CelVerifierTool()).execute("--version"); + assertThat(exitCode).isEqualTo(0); + } +} diff --git a/verifier/tools/BUILD.bazel b/verifier/tools/BUILD.bazel new file mode 100644 index 000000000..a547c15b2 --- /dev/null +++ b/verifier/tools/BUILD.bazel @@ -0,0 +1,19 @@ +package( + default_applicable_licenses = ["//:license"], + default_visibility = ["//verifier:verifier_internal"], +) + +alias( + name = "tools", + actual = "//verifier/src/main/java/dev/cel/verifier/tools:tools_lib", +) + +alias( + name = "tools_lib", + actual = "//verifier/src/main/java/dev/cel/verifier/tools:tools_lib", +) + +alias( + name = "cel_verifier_tool", + actual = "//verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool", +) diff --git a/verifier/tools/README.md b/verifier/tools/README.md new file mode 100644 index 000000000..398cbad74 --- /dev/null +++ b/verifier/tools/README.md @@ -0,0 +1,191 @@ +# CEL Java Verifier CLI & Interactive REPL Tool + +The CEL Java Verifier comes with a command-line tool (`cel-verifier`) and an +interactive REPL shell for testing satisfiability, validity, equivalence, +and policy invariants without writing Java code. + +## Running the CLI Tool + +### Running via Bazel + +```bash +# Run CLI verification commands +bazel run //verifier/tools:cel_verifier_tool -- \ + check-sat \ + --expr "role == 'editor' && port > 1024" \ + --var "role:string" \ + --var "port:int" + +# Run with JSON output format for CI/CD integrations +bazel run //verifier/tools:cel_verifier_tool -- \ + check-sat \ + --expr "role == 'editor'" \ + --var "role:string" \ + --output_format=json + +# Launch interactive REPL shell +bazel run //verifier/tools:cel_verifier_tool -- repl +``` + +### Running via Maven Central + +> **Note:** Executable binaries and Maven packages (`dev.cel:cel-verifier`) +> will be published to Maven Central in an upcoming release. + +## CLI Commands + +* `check-sat --expr "..."`: Verifies satisfiability of an expression and + prints witness inputs if satisfiable. +* `check-valid --expr "..."`: Proves validity (`isAlwaysTrue`) and prints + a counterexample if invalid. +* `verify-equiv --expr1 "..." --expr2 "..."`: Proves logical equivalence + between two CEL expressions. +* `verify-policy --file policy.yaml`: Verifies policy invariants defined + in a YAML policy file. +* `repl`: Enters interactive verification shell mode. + +## Command Options + +The verification commands (`check-sat`, `check-valid`, `verify-equiv`, +`verify-policy`) accept the following options: + +### Variable Declarations (`--var`, `-v`) + +Declare variables in `name:type` format. Multiple variables can be declared by +repeating the `--var` option. + +Supported types: + +* Primitive types: `int`, `uint`, `string`, `bool`, `double`, `bytes`, `dyn` +* List types: `list` (e.g., `--var "tags:list"`) +* Map types: `map` (e.g., `--var "scores:map"`) + +Examples: +```bash +--var "role:string" --var "port:int" --var "tags:list" +``` + +### Unknown Identifiers (`--unknown`, `-u`) + +Permit specific identifiers or attributes (e.g., `request.headers`) to +evaluate to `Unknown` during verification: + +```bash +--unknown "request.headers" --unknown "auth.credentials" +``` + +### Solver Timeout (`--timeout`) + +Set maximum Z3 SMT solver timeout in seconds (default: `10`): + +```bash +--timeout 15 +``` + +### Comprehension Unroll Limit (`--unroll-limit`) + +Set bounded unroll limit for comprehensions and loop macros like `.all()` and +`.exists()` (default: `5`): + +```bash +--unroll-limit 10 +``` + +### Output Format (`--output_format`, `-fmt`) + +Set CLI output format (`TEXT` or `JSON`, default: `TEXT`): + +```bash +--output_format json +``` + +## Exit Codes + +* `0`: Verification succeeded / condition verified. +* `1`: Violation or counterexample found. +* `2`: Inconclusive result (solver unknown or timeout). +* `3`: Error (syntax compilation error, missing file, or execution error). + +## Interactive REPL Shell + +The REPL shell provides an interactive, stateful environment to execute CEL +formal verification queries without re-declaring variables or re-running CLI +parameters for every query. + +### Launching the REPL + +```bash +bazel run //verifier/tools:cel_verifier_tool -- repl +``` + +### REPL Commands + +| Command | Description | Example | +|---|---|---| +| `:var ` | Declare a variable in session state | `:var role string` | +| `:unknown ` | Mark identifier as Unknown | `:unknown request.headers` | +| `:timeout ` | Set Z3 solver timeout in seconds (default: 10s) | `:timeout 5` | +| `:unroll ` | Set comprehension unroll limit (default: 5) | `:unroll 3` | +| `:vars` | Display declared session variables & config | `:vars` | +| `:clear` | Reset session state (clears variables & unknowns) | `:clear` | +| `:help [cmd]` | Display built-in help or command details | `:help var` | +| `:quit` / `:exit` | Exit the interactive REPL shell | `:quit` | + +### Verification Queries in REPL + +* **Satisfiability (`sat ` or ``):** Checks if the expression + can evaluate to `true` for any assignment of session variables. Outputs + satisfying witness inputs if satisfiable. +* **Validity (`valid `):** Proves whether the expression evaluates + to `true` for ALL possible variable assignments. Outputs a counterexample + if invalid. +* **Equivalence (`equiv <=> `):** Proves whether two + expressions are logically identical across all inputs. Outputs a + counterexample if not equivalent. + +### Example REPL Session + +```text +============================================================ + CEL Verification REPL + Type :help for commands, :quit to exit. +============================================================ +cel-verifier> :var port int +Variable declared: port : int + +cel-verifier> sat role == 'admin' && port > 1024 + +cel-verifier> :var role string +Variable declared: role : string + +cel-verifier> sat role == 'admin' && port > 1024 +[VERIFIED] Condition is satisfiable. Satisfying input: + role = "admin" + port = 1025 + +cel-verifier> valid port > 0 || port <= 0 +[VERIFIED] + +cel-verifier> valid port > 1024 +[VIOLATED] Condition is violated. Counterexample input: + port = 0 + +cel-verifier> equiv port > 10 <=> 10 < port +[VERIFIED] + +cel-verifier> :vars +--- Session State --- +Timeout: 10s | Unroll limit: 5 +Unknowns: none +Variables (2): + role : string + port : int + +cel-verifier> :quit +Goodbye! +``` + +> **Note:** Inline help is built into the REPL shell. Type `:help` or +> `:help ` (e.g. `:help var`, `:help equiv`) at any prompt for +> detailed usage instructions and examples. +