Expose the verifier's counterexamples as structured CelWitness values

PiperOrigin-RevId: 1004026905

Author: l46kok

verifier/README.md

@@ -224,8 +224,8 @@ public class PolicyVerifierExample {
         System.out.println(result.message());
         // Output:
         // Equivalence violation detected. Counterexample input:
-        //   country = "a"
         //   role = "editor"
+        //   country = "a"
         //   port = 443
         break;
       case INCONCLUSIVE:
@@ -241,7 +241,8 @@ public class PolicyVerifierExample {
 When checking whether an expression is satisfiable using `isSatisfiable`, the
 verifier returns `VERIFIED` if there exists at least one input combination
 where the expression evaluates to `true`. Furthermore, `result.message()`
-provides concrete satisfying model assignments (witness/test case generation).
+provides concrete satisfying model assignments (witness/test case generation),
+and `result.witness()` exposes them as CEL runtime values.
 
 ```java
 import dev.cel.common.CelAbstractSyntaxTree;
@@ -370,14 +371,12 @@ public class InvariantsExample {
 
 ### Limitations
 
-*   **Unsupported Standard Functions (Uninterpreted Functions):** Not all
-    CEL standard library functions have SMT axioms defined yet. Unsupported
-    functions are treated as *uninterpreted functions* by Z3 (the solver
-    only guarantees that identical inputs yield identical outputs, but does
-    not understand the function's internal logic or return types).
-    Consequently, verifications that rely on the specific semantics of
-    these functions may return `VerificationStatus.INCONCLUSIVE`. Support for
-    more standard library functions will be added incrementally.
+*   **Uninterpreted Functions:** Custom functions, and standard library
+    functions that don't have SMT axioms yet, are treated as uninterpreted:
+    the solver only knows that identical inputs yield identical outputs.
+    Results that depend on their return values are `INCONCLUSIVE`, and a
+    `VERIFIED` result assumes they return a value of their declared type
+    rather than an error.
 
 ### Best Practices & Performance
 

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

@@ -15,6 +15,7 @@ java_library(
         "CelVerificationResult.java",
         "CelVerifier.java",
         "CelVerifierBuilder.java",
+        "CelWitness.java",
     ],
     tags = [
     ],
@@ -23,6 +24,7 @@ java_library(
         "//common:cel_ast",
         "//common/types:type_providers",
         "@maven//:com_google_errorprone_error_prone_annotations",
+        "@maven//:com_google_guava_guava",
     ],
 )
 
@@ -179,10 +181,13 @@ java_library(
         "//common/ast",
         "//common/ast:cel_block",
         "//common/internal:cel_descriptor_pools",
+        "//common/internal:proto_time_utils",
         "//common/internal:well_known_proto",
         "//common/types",
         "//common/types:cel_types",
         "//common/types:type_providers",
+        "//common/values",
+        "//common/values:cel_byte_string",
         "//optimizer",
         "//optimizer:optimization_exception",
         "//optimizer:optimizer_builder",

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

@@ -16,6 +16,7 @@
 
 import com.google.common.collect.ImmutableList;
 import com.google.common.collect.ImmutableSet;
+import com.google.common.collect.ImmutableSortedSet;
 import com.google.common.collect.Iterables;
 import com.microsoft.z3.ArithExpr;
 import com.microsoft.z3.ArrayExpr;
@@ -51,6 +52,7 @@
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.HashMap;
+import java.util.LinkedHashMap;
 import java.util.LinkedHashSet;
 import java.util.List;
 import java.util.Map;
@@ -82,6 +84,7 @@ final class CelAstToZ3Translator {
   private static final String EMPTY_MSG_REF_PREFIX = "!empty_msg_ref_";
   private static final String EMPTY_LIST_PREFIX = "!empty_list";
   private static final String EMPTY_MAP_PREFIX = "!empty_map";
+  private static final String FUNCTION_PREFIX = "!fn_";
   private static final String NULL_VALUE_FIELD = "null_value";
   private static final long MAX_UINT32 = 0xFFFFFFFFL;
   private final Context ctx;
@@ -114,6 +117,11 @@ CelZ3TypeSystem getTypeSystem() {
     return typeSystem;
   }
 
+  /** Returns the input variables, in order of first appearance. */
+  Set<Expr<?>> getInputVariables() {
+    return inputVariableTypes.keySet();
+  }
+
   /**
    * Returns a Z3 boolean expression asserting that the provided CEL value is a boolean and is true.
    */
@@ -820,21 +828,40 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
               Sort[] argSorts = new Sort[args.size()];
               Arrays.fill(argSorts, 0, args.size(), typeSystem.celValueSort());
               FuncDecl<?> funcDecl =
-                  typeSystem.internFuncDecl(functionName, argSorts, typeSystem.celValueSort());
+                  typeSystem.internFuncDecl(
+                      uninterpretedFunctionSymbol(exprId, ast),
+                      argSorts,
+                      typeSystem.celValueSort());
 
               Expr<?>[] exprArgs = args.stream().map(TranslatedValue::z3Expr).toArray(Expr[]::new);
               Expr<?> callRes = ctx.mkApp(funcDecl, exprArgs);
               typeConstraints.add(createTypeConstraint(callRes, exprId, ast));
               typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes)));
               typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes)));
 
-              boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN);
-              BoolExpr isApprox = ctx.mkBool(!isDynamic);
+              // The solver picks the result freely, so a model depending on it is never exact.
               return TranslatedValue.propagateStrict(
-                  ctx, typeSystem, functionName, callRes, Optional.of(expr), isApprox, args);
+                  ctx,
+                  typeSystem,
+                  functionName,
+                  callRes,
+                  Optional.of(expr),
+                  /* baseTaint= */ ctx.mkTrue(),
+                  args);
             });
   }
 
+  /**
+   * Returns the Z3 symbol for an uninterpreted call. Each set of candidate overloads gets its own
+   * symbol, since distinct overloads may have different implementations even on equal values (e.g.
+   * empty lists of different element types). The prefix keeps it apart from variables and internal
+   * symbols.
+   */
+  private static String uninterpretedFunctionSymbol(long exprId, CelAbstractSyntaxTree ast) {
+    ImmutableList<String> overloadIds = ast.getReferenceOrThrow(exprId).overloadIds();
+    return FUNCTION_PREFIX + String.join("|", ImmutableSortedSet.copyOf(overloadIds));
+  }
+
   /**
    * Whether a call may construct a container that embeds its args (e.g. list concatenation, map
    * insertion or optional.of). Indexing and conditionals return existing values instead, so
@@ -1556,7 +1583,7 @@ private Expr<?> mkParameterizedUnknown(CelExpr expr, CelAbstractSyntaxTree ast)
     this.comprehensionUnrollLimit = comprehensionUnrollLimit;
     this.typeSystem = new CelZ3TypeSystem(ctx, parameterizeUnknowns);
     this.typeConstraints = new LinkedHashSet<>();
-    this.inputVariableTypes = new HashMap<>();
+    this.inputVariableTypes = new LinkedHashMap<>();
     this.operatorTranslator =
         new CelZ3OperatorTranslator(
             ctx,

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

@@ -15,6 +15,8 @@
 package dev.cel.verifier;
 
 import com.google.auto.value.AutoValue;
+import java.util.Map;
+import java.util.Optional;
 
 /** Result object containing the outcome of a CEL AST verification check. */
 @AutoValue
@@ -43,6 +45,12 @@ public enum VerificationStatus {
    */
   public abstract String counterexample();
 
+  /**
+   * Returns the counterexample or satisfying input found by the solver, if any. Its variables are
+   * empty when the outcome doesn't depend on any input.
+   */
+  public abstract Optional<CelWitness> witness();
+
   /**
    * Returns a message detailing the outcome of the verification check, such as a counterexample
    * input, satisfying model assignments, or truncation reason. May be empty if status is VERIFIED
@@ -53,28 +61,65 @@ public String message() {
   }
 
   static CelVerificationResult verified() {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", "");
+    return create(VerificationStatus.VERIFIED, "");
   }
 
-  static CelVerificationResult verified(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, "");
+  static CelVerificationResult verified(String reason, CelWitness satisfyingInput) {
+    return create(
+        VerificationStatus.VERIFIED, reason, satisfyingInput, /* isCounterexample= */ false);
   }
 
   static CelVerificationResult failed(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, "");
+    return create(VerificationStatus.VIOLATED, reason);
   }
 
-  static CelVerificationResult failed(String reason, String counterexample) {
-    return new AutoValue_CelVerificationResult(
-        VerificationStatus.VIOLATED, reason, counterexample);
+  static CelVerificationResult failed(String reason, CelWitness counterexample) {
+    return create(
+        VerificationStatus.VIOLATED, reason, counterexample, /* isCounterexample= */ true);
   }
 
   static CelVerificationResult inconclusive(String reason) {
-    return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, "");
+    return create(VerificationStatus.INCONCLUSIVE, reason);
+  }
+
+  static CelVerificationResult inconclusive(
+      String reason, CelWitness witness, boolean isCounterexample) {
+    return create(VerificationStatus.INCONCLUSIVE, reason, witness, isCounterexample);
   }
 
-  static CelVerificationResult inconclusive(String reason, String counterexample) {
+  private static CelVerificationResult create(VerificationStatus status, String reason) {
+    return new AutoValue_CelVerificationResult(status, reason, "", Optional.empty());
+  }
+
+  private static CelVerificationResult create(
+      VerificationStatus status, String reason, CelWitness witness, boolean isCounterexample) {
     return new AutoValue_CelVerificationResult(
-        VerificationStatus.INCONCLUSIVE, reason, counterexample);
+        status,
+        reason,
+        describe(witness, status == VerificationStatus.INCONCLUSIVE, isCounterexample),
+        Optional.of(witness));
+  }
+
+  private static String describe(
+      CelWitness witness, boolean isApproximate, boolean isCounterexample) {
+    if (witness.variables().isEmpty()) {
+      return isCounterexample
+          ? " (The expression fails unconditionally, regardless of input state)"
+          : " (The expression is satisfiable unconditionally, regardless of input state)";
+    }
+
+    StringBuilder sb = new StringBuilder();
+    if (isCounterexample) {
+      sb.append(isApproximate ? " Potential counterexample input:" : " Counterexample input:");
+    } else {
+      sb.append(isApproximate ? " Potential satisfying input:" : " Satisfying input:");
+    }
+    for (Map.Entry<String, CelWitness.Variable> variable : witness.variables().entrySet()) {
+      sb.append("\n  ")
+          .append(variable.getKey())
+          .append(" = ")
+          .append(variable.getValue().displayValue());
+    }
+    return sb.toString();
   }
 }

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

@@ -255,23 +255,13 @@ public CelVerificationResult verifyEquivalence(
       switch (result.outcome) {
         case EXACT_MATCH:
           return CelVerificationResult.failed(
-              "Equivalence violation detected.",
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ false,
-                  /* isCounterexample= */ true));
+              "Equivalence violation detected.", extractWitness(ctx, translator, result.model));
         case APPROXIMATE_MATCH:
           return CelVerificationResult.inconclusive(
               "Inconclusive: a divergence may exist, but it depends on approximations, missing"
                   + " theories, or loop bounds.",
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ true,
-                  /* isCounterexample= */ true));
+              extractWitness(ctx, translator, result.model),
+              /* isCounterexample= */ true);
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
               "Inconclusive: expressions are equivalent within the current loop unroll limit, but"
@@ -342,22 +332,13 @@ CelVerificationResult verifyImplication(
         case EXACT_MATCH:
           return CelVerificationResult.failed(
               String.format("%s violation detected.", subjectName),
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ false,
-                  /* isCounterexample= */ true));
+              extractWitness(ctx, translator, result.model));
         case APPROXIMATE_MATCH:
           return CelVerificationResult.inconclusive(
               "Inconclusive: a counterexample may exist, but it depends on approximations, missing"
                   + " theories, or loop bounds.",
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ true,
-                  /* isCounterexample= */ true));
+              extractWitness(ctx, translator, result.model),
+              /* isCounterexample= */ true);
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
               String.format(
@@ -402,23 +383,10 @@ private CelVerificationResult checkSatisfiability(
 
       switch (result.outcome) {
         case EXACT_MATCH:
+          CelWitness witness = extractWitness(ctx, translator, result.model);
           return searchForCounterexample
-              ? CelVerificationResult.failed(
-                  "Condition is not always true.",
-                  getCounterexampleString(
-                      ctx,
-                      translator.getTypeSystem(),
-                      result.model,
-                      /* isApproximate= */ false,
-                      /* isCounterexample= */ true))
-              : CelVerificationResult.verified(
-                  "Condition is satisfiable."
-                      + getCounterexampleString(
-                          ctx,
-                          translator.getTypeSystem(),
-                          result.model,
-                          /* isApproximate= */ false,
-                          /* isCounterexample= */ false));
+              ? CelVerificationResult.failed("Condition is not always true.", witness)
+              : CelVerificationResult.verified("Condition is satisfiable.", witness);
 
         case APPROXIMATE_MATCH:
           String prefix =
@@ -429,12 +397,8 @@ private CelVerificationResult checkSatisfiability(
                       + " approximations, missing theories, or loop bounds.";
           return CelVerificationResult.inconclusive(
               prefix,
-              getCounterexampleString(
-                  ctx,
-                  translator.getTypeSystem(),
-                  result.model,
-                  /* isApproximate= */ true,
-                  /* isCounterexample= */ searchForCounterexample));
+              extractWitness(ctx, translator, result.model),
+              /* isCounterexample= */ searchForCounterexample);
 
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
@@ -537,14 +501,13 @@ private CelAstToZ3Translator newTranslator(Context ctx, boolean parameterizeUnkn
         parameterizeUnknowns);
   }
 
-  private static String getCounterexampleString(
-      Context ctx,
-      CelZ3TypeSystem typeSystem,
-      Model model,
-      boolean isApproximate,
-      boolean isCounterexample) {
+  private CelWitness extractWitness(Context ctx, CelAstToZ3Translator translator, Model model) {
     return CelZ3CounterexampleGenerator.generate(
-        ctx, typeSystem, model, isApproximate, isCounterexample);
+        ctx,
+        translator.getTypeSystem(),
+        model,
+        comprehensionUnrollLimit,
+        translator.getInputVariables());
   }
 
   private enum SolverOutcome {