Name what the verifier approximates in inconclusive results

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

@@ -23,6 +23,7 @@
 import com.microsoft.z3.Context;
 import com.microsoft.z3.Expr;
 import com.microsoft.z3.FuncDecl;
+import com.microsoft.z3.Model;
 import com.microsoft.z3.Quantifier;
 import com.microsoft.z3.SeqExpr;
 import com.microsoft.z3.Sort;
@@ -89,6 +90,14 @@ BoolExpr hasTruncation() {
     return context.hasTruncation();
   }
 
+  ImmutableList<String> approximationSources(Model model, BoolExpr taint) {
+    return context.approximationSources(model, taint);
+  }
+
+  BoolExpr recordApproximation(String description, BoolExpr condition) {
+    return context.recordApproximation(description, condition);
+  }
+
   CelZ3TypeSystem getTypeSystem() {
     return typeSystem;
   }
@@ -450,7 +459,7 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) {
                   functionName,
                   callRes,
                   Optional.of(expr),
-                  /* baseTaint= */ ctx.mkTrue(),
+                  /* baseTaint= */ context.recordCallApproximation(functionName, ctx.mkTrue()),
                   args);
             });
   }

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

@@ -231,7 +231,9 @@ public CelVerificationResult verifyEquivalence(
               ctx,
               tvA.isApproximate(),
               tvB.isApproximate(),
-              ctx.mkAnd(tvA.isZ3Unknown(), tvB.isZ3Unknown()));
+              translator.recordApproximation(
+                  "unknown results, which are compared only by their origin",
+                  ctx.mkAnd(tvA.isZ3Unknown(), tvB.isZ3Unknown())));
 
       Solver solver = newSolver(ctx);
       for (BoolExpr constraint : translator.getTypeConstraints()) {
@@ -259,8 +261,7 @@ public CelVerificationResult verifyEquivalence(
               "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.",
+              inconclusiveReason("a divergence", translator, result.model, combinedTaint),
               extractWitness(ctx, translator, result.model),
               /* isCounterexample= */ true);
         case TRUNCATED:
@@ -336,8 +337,7 @@ CelVerificationResult verifyImplication(
               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.",
+              inconclusiveReason("a counterexample", translator, result.model, combinedTaint),
               extractWitness(ctx, translator, result.model),
               /* isCounterexample= */ true);
         case TRUNCATED:
@@ -390,14 +390,12 @@ private CelVerificationResult checkSatisfiability(
               : CelVerificationResult.verified("Condition is satisfiable.", witness);
 
         case APPROXIMATE_MATCH:
-          String prefix =
-              searchForCounterexample
-                  ? "Inconclusive: a counterexample may exist, but it depends on approximations,"
-                      + " missing theories, or loop bounds."
-                  : "Inconclusive: a satisfying model may exist, but it depends on"
-                      + " approximations, missing theories, or loop bounds.";
           return CelVerificationResult.inconclusive(
-              prefix,
+              inconclusiveReason(
+                  searchForCounterexample ? "a counterexample" : "a satisfying input",
+                  translator,
+                  result.model,
+                  tv.isApproximate()),
               extractWitness(ctx, translator, result.model),
               /* isCounterexample= */ searchForCounterexample);
 
@@ -502,6 +500,15 @@ private CelAstToZ3Translator newTranslator(Context ctx, boolean parameterizeUnkn
         parameterizeUnknowns);
   }
 
+  private static String inconclusiveReason(
+      String candidate, CelAstToZ3Translator translator, Model model, BoolExpr taint) {
+    ImmutableList<String> sources = translator.approximationSources(model, taint);
+    return "Inconclusive: "
+        + candidate
+        + " may exist, but it depends on what the verifier doesn't model exactly"
+        + (sources.isEmpty() ? "." : ": " + String.join(", ", sources) + ".");
+  }
+
   private CelWitness extractWitness(Context ctx, CelAstToZ3Translator translator, Model model) {
     return CelZ3CounterexampleGenerator.generate(
         ctx,

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

@@ -154,7 +154,9 @@ private TranslatedValue translateDynamicComprehension(
     boolean isMap = rangeType instanceof MapType;
     if (!isList && !isMap) {
       BoolExpr isRuntimeListOrMap =
-          ctx.mkOr(typeSystem.isList(iterRange), typeSystem.isMap(iterRange));
+          context.recordApproximation(
+              "comprehensions over `dyn` values",
+              ctx.mkOr(typeSystem.isList(iterRange), typeSystem.isMap(iterRange)));
       Expr<?> result =
           ctx.mkITE(isRuntimeListOrMap, mkParameterizedUnknown(celExpr, ast), typeSystem.mkError());
       return TranslatedValue.create(result, celExpr, typeSystem, isRuntimeListOrMap);
@@ -171,7 +173,8 @@ private TranslatedValue translateDynamicComprehension(
 
     BoolExpr isValidRange = isMap ? typeSystem.isMap(iterRange) : typeSystem.isList(iterRange);
     BoolExpr isTruncated =
-        ctx.mkAnd(isValidRange, ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit)));
+        context.recordUnrollLimitApproximation(
+            ctx.mkAnd(isValidRange, ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit))));
     context.addTruncationCondition(isTruncated);
 
     if (isAllMacro(comp) || isExistsMacro(comp)) {
@@ -338,7 +341,10 @@ private TranslatedValue unrollMapAndFilter(
 
     // TODO: Model the loop condition for custom macros; until then, abstract the
     // result of any non-true condition, since the unrolled value ignores early exits.
-    BoolExpr isConditionUnmodeled = ctx.mkBool(!isLiteralTrue(comp.loopCondition()));
+    BoolExpr isConditionUnmodeled =
+        context.recordApproximation(
+            "comprehensions with a loop condition",
+            ctx.mkBool(!isLiteralTrue(comp.loopCondition())));
     BoolExpr isAbstracted =
         CelZ3Exprs.mkOrFlattened(ctx, rangeIsUnknown, isTruncated, isConditionUnmodeled);
     // An error is not final when truncated: an unknown from a later iteration overrides it.

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

@@ -130,7 +130,12 @@ Optional<TranslatedValue> translateFunctionCall(
       BoolExpr typeGuard = CelZ3Exprs.mkAndFlattened(ctx, typeGuards);
       currentZ3Result = ctx.mkITE(typeGuard, evaluatedResult.z3Expr(), currentZ3Result);
       currentApprox =
-          (BoolExpr) ctx.mkITE(typeGuard, evaluatedResult.isApproximate(), currentApprox);
+          (BoolExpr)
+              ctx.mkITE(
+                  typeGuard,
+                  attributeApproximation(
+                      functionName, evaluatedResult.isApproximate(), argApproximations),
+                  currentApprox);
     }
 
     if (!matchedAny) {
@@ -160,6 +165,24 @@ Optional<TranslatedValue> translateFunctionCall(
             currentApprox));
   }
 
+  // Returns an overload's approximation with the part it adds itself recorded as a call
+  // approximation.
+  private BoolExpr attributeApproximation(
+      String functionName, BoolExpr approx, ImmutableList<BoolExpr> argApproximations) {
+    // A literal `true` can't be substituted without also replacing the overload's own `true`.
+    ImmutableList<BoolExpr> substitutable =
+        argApproximations.stream().filter(a -> !a.isTrue()).collect(toImmutableList());
+    // Approximations only grow with their arguments', so approx is equivalent to the overload's own
+    // part (its value with exact arguments) or approx under some approximate argument.
+    BoolExpr own =
+        context.recordCallApproximation(
+            functionName,
+            (BoolExpr) context.withoutApproximation(approx, substitutable).simplify());
+    BoolExpr inherited =
+        CelZ3Exprs.mkAndFlattened(ctx, approx, CelZ3Exprs.mkOrFlattened(ctx, argApproximations));
+    return CelZ3Exprs.mkOrFlattened(ctx, own, inherited);
+  }
+
   /**
    * Constrains every value that {@code InAxiom} may find in {@code rhs} to its guaranteed element
    * (or key) type, and returns the condition under which the result remains approximate.
@@ -339,7 +362,7 @@ private TranslatedValue translateOperatorCall(
         // For operators we haven't implemented cleanly, just wrap uninterpreted for now.
         return TranslatedValue.propagateStrict(
                 ctx, typeSystem, op.getFunction(), typeSystem.mkUnknown(), args)
-            .withApproximation(ctx.mkTrue());
+            .withApproximation(context.recordCallApproximation(op.getFunction(), ctx.mkTrue()));
     }
   }
 
@@ -977,14 +1000,15 @@ private TranslatedValue translateIndex(
     String opName =
         isOptional ? Operator.OPTIONAL_INDEX.getFunction() : Operator.INDEX.getFunction();
     BoolExpr isListIndexTruncated =
-        ctx.mkAnd(
-            shouldEvaluate,
-            typeSystem.isList(lhsTrans),
-            typeSystem.isInt(rhsTrans),
-            ctx.mkGe(typeSystem.getInt(rhsTrans), ctx.mkInt(comprehensionUnrollLimit)),
-            ctx.mkLt(
-                typeSystem.getInt(rhsTrans),
-                ctx.mkLength(typeSystem.getSeq(typeSystem.getListRef(lhsTrans)))));
+        context.recordUnrollLimitApproximation(
+            ctx.mkAnd(
+                shouldEvaluate,
+                typeSystem.isList(lhsTrans),
+                typeSystem.isInt(rhsTrans),
+                ctx.mkGe(typeSystem.getInt(rhsTrans), ctx.mkInt(comprehensionUnrollLimit)),
+                ctx.mkLt(
+                    typeSystem.getInt(rhsTrans),
+                    ctx.mkLength(typeSystem.getSeq(typeSystem.getListRef(lhsTrans))))));
     BoolExpr isMapIndexTruncated = ctx.mkAnd(shouldEvaluate, context.isTruncatedMap(lhsTrans));
     return TranslatedValue.propagateStrict(ctx, typeSystem, opName, actualValue, args)
         .withApproximation(
@@ -1148,11 +1172,12 @@ private BoolExpr mayObserveTruncatedTypeConstraint(
     if (Arrays.stream(args).allMatch(arg -> isConcrete(extractAstTypeOrDefault(arg, ast)))) {
       return ctx.mkFalse();
     }
-    return CelZ3Exprs.mkOrFlattened(
-        ctx,
-        Arrays.stream(args)
-            .map(arg -> typeSystem.hasTruncatedTypeConstraint(arg.z3Expr()))
-            .collect(toImmutableList()));
+    return context.recordUnrollLimitApproximation(
+        CelZ3Exprs.mkOrFlattened(
+            ctx,
+            Arrays.stream(args)
+                .map(arg -> typeSystem.hasTruncatedTypeConstraint(arg.z3Expr()))
+                .collect(toImmutableList())));
   }
 
   CelZ3OperatorTranslator(CelZ3TranslationContext context, CelZ3FunctionRegistry functionRegistry) {

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

@@ -14,12 +14,17 @@
 
 package dev.cel.verifier;
 
+import static com.google.common.collect.ImmutableList.toImmutableList;
+
+import com.google.common.collect.ImmutableList;
 import com.microsoft.z3.BoolExpr;
 import com.microsoft.z3.Context;
 import com.microsoft.z3.Expr;
+import com.microsoft.z3.Model;
 import dev.cel.common.types.CelType;
 import dev.cel.common.types.SimpleType;
 import java.util.ArrayList;
+import java.util.Arrays;
 import java.util.Collections;
 import java.util.HashMap;
 import java.util.LinkedHashMap;
@@ -41,6 +46,7 @@ final class CelZ3TranslationContext {
   private final Set<BoolExpr> constraints;
   private final Map<Expr<?>, CelType> inputVariableTypes;
   private final List<BoolExpr> truncationConditions;
+  private final Map<String, List<BoolExpr>> approximationTerms;
   private final Map<String, TranslatedValue> symbolTable;
   private final Map<String, TranslatedValue> localScope;
 
@@ -93,11 +99,65 @@ CelType guaranteedType(Expr<?> value) {
    * not linked to its keys.
    */
   BoolExpr isTruncatedMap(Expr<?> val) {
-    return ctx.mkAnd(
-        typeSystem.isMap(val),
-        ctx.mkGt(
-            ctx.mkLength(typeSystem.getMapKeys(typeSystem.getMapRef(val))),
-            ctx.mkInt(comprehensionUnrollLimit)));
+    return recordUnrollLimitApproximation(
+        ctx.mkAnd(
+            typeSystem.isMap(val),
+            ctx.mkGt(
+                ctx.mkLength(typeSystem.getMapKeys(typeSystem.getMapRef(val))),
+                ctx.mkInt(comprehensionUnrollLimit))));
+  }
+
+  /**
+   * Records {@code description} as a reason results are approximate where {@code condition} holds,
+   * and returns the term to use for {@code condition}, so that it can be told apart in a taint.
+   */
+  BoolExpr recordApproximation(String description, BoolExpr condition) {
+    BoolExpr term = condition;
+    if (condition.isTrue()) {
+      // A literal `true` is shared by every other unconditional approximation.
+      term = (BoolExpr) ctx.mkFreshConst("!approx", ctx.getBoolSort());
+      constraints.add(term);
+    }
+    approximationTerms.computeIfAbsent(description, k -> new ArrayList<>()).add(term);
+    return term;
+  }
+
+  BoolExpr recordUnrollLimitApproximation(BoolExpr condition) {
+    return recordApproximation(
+        "lists and maps longer than the unroll limit (" + comprehensionUnrollLimit + ")",
+        condition);
+  }
+
+  BoolExpr recordCallApproximation(String functionName, BoolExpr condition) {
+    return recordApproximation("calls to `" + functionName + "`", condition);
+  }
+
+  /**
+   * Returns the descriptions of the approximations that are enough on their own to make {@code
+   * taint} hold in {@code model}, which leaves out those in short-circuited operands or untaken
+   * branches.
+   */
+  ImmutableList<String> approximationSources(Model model, BoolExpr taint) {
+    return approximationTerms.keySet().stream()
+        .filter(description -> holds(model, withoutApproximation(taint, termsExcept(description))))
+        .collect(toImmutableList());
+  }
+
+  private ImmutableList<BoolExpr> termsExcept(String description) {
+    return approximationTerms.entrySet().stream()
+        .filter(source -> !source.getKey().equals(description))
+        .flatMap(source -> source.getValue().stream())
+        .collect(toImmutableList());
+  }
+
+  BoolExpr withoutApproximation(BoolExpr expr, List<BoolExpr> terms) {
+    BoolExpr[] falses = new BoolExpr[terms.size()];
+    Arrays.fill(falses, ctx.mkFalse());
+    return (BoolExpr) expr.substitute(terms.toArray(new BoolExpr[0]), falses);
+  }
+
+  private static boolean holds(Model model, BoolExpr condition) {
+    return model.evaluate(condition, /* completion= */ true).isTrue();
   }
 
   void addTruncationCondition(BoolExpr condition) {
@@ -148,6 +208,7 @@ <T> T withScope(String varName, TranslatedValue value, Supplier<T> action) {
     this.constraints = new LinkedHashSet<>();
     this.inputVariableTypes = new LinkedHashMap<>();
     this.truncationConditions = new ArrayList<>();
+    this.approximationTerms = new LinkedHashMap<>();
     this.symbolTable = new HashMap<>();
     this.localScope = new HashMap<>();
   }