Add CLI for Verifier

PiperOrigin-RevId: 956259271

Author: l46kok

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).

verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

@@ -1247,9 +1247,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);
@@ -1289,15 +1290,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 +1306,69 @@ 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);
-        boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint));
-        BoolExpr outOfBounds = ctx.mkGe(idx, length);
-        boundsAndTypes.add(ctx.mkImplies(outOfBounds, ctx.mkEq(elem, typeSystem.mkUnknown())));
+        // 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))));
+        // Short-circuit DYN element types to prevent generating redundant validIndex ⇒ TRUE
+        // clauses.
+        if (!elemType.equals(SimpleType.DYN)) {
+          BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType);
+          boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint));
+        }
       }
 
       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<BoolExpr> boundsAndTypes = new ArrayList<>();
+      boundsAndTypes.add(isMap);
+
+      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)));
+        // Short-circuit DYN key types to prevent generating redundant validIndex ⇒ TRUE clauses.
+        if (!keyType.equals(SimpleType.DYN)) {
+          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 = ctx.mkNot(typeSystem.isError(mapVal));
+        boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError));
+        // Short-circuit DYN value types to prevent generating redundant validEntry ⇒ TRUE clauses.
+        if (!valType.equals(SimpleType.DYN)) {
+          boundsAndTypes.add(
+              ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType)));
+        }
+      }
+
+      return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes);
     }
     if (type.kind() == CelKind.STRUCT) {
       return ctx.mkAnd(

verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java

@@ -127,6 +127,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 =

verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java

@@ -685,6 +685,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);

verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel

@@ -0,0 +1,77 @@
+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 = [
+        "CelVerifierTool.java",
+        "CelVerifierToolCore.java",
+        "FormatUtils.java",
+        "VerificationOptions.java",
+        ":generate_version",
+    ],
+    tags = [
+        "alt_dep=//verifier/tools",
+    ],
+    deps = [
+        "//bundle:cel",
+        "//common:cel_ast",
+        "//common:compiler_common",
+        "//common:options",
+        "//common/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",
+    ],
+)