Generate satisfiable model for isSatisfiable

PiperOrigin-RevId: 951064191

Author: l46kok

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

@@ -34,15 +34,20 @@ public enum VerificationStatus {
   public abstract VerificationStatus status();
 
   /**
-   * Returns a message detailing why the verification failed or was inconclusive (e.g., the
-   * counterexample input or truncation reason). Empty if status is VERIFIED.
+   * 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
+   * and no model inputs apply (e.g., when verifying isAlwaysTrue without counterexamples).
    */
   public abstract String message();
 
   static CelVerificationResult verified() {
     return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "");
   }
 
+  static CelVerificationResult verified(String message) {
+    return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, message);
+  }
+
   static CelVerificationResult failed(String message) {
     return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, message);
   }

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

@@ -22,7 +22,9 @@
 public interface CelVerifier {
 
   /**
-   * Returns verified if there is at least one input combination where the AST evaluates to true.
+   * Returns verified if there is at least one input combination where the AST evaluates to true. If
+   * the expression is satisfiable and depends on input variables, the result message will contain a
+   * satisfying model (witness) with concrete variable assignments.
    *
    * @param ast The input expression to verify. Must be a type-checked AST.
    */

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

@@ -192,13 +192,21 @@ public CelVerificationResult verifyEquivalence(
           return CelVerificationResult.failed(
               "Equivalence violation detected."
                   + getCounterexampleString(
-                      ctx, translator.getTypeSystem(), result.model, /* isApproximate= */ false));
+                      ctx,
+                      translator.getTypeSystem(),
+                      result.model,
+                      /* isApproximate= */ false,
+                      /* isCounterexample= */ true));
         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));
+                      ctx,
+                      translator.getTypeSystem(),
+                      result.model,
+                      /* isApproximate= */ true,
+                      /* isCounterexample= */ true));
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
               "Inconclusive: expressions are equivalent within the current loop unroll limit, but"
@@ -250,8 +258,16 @@ private CelVerificationResult checkSatisfiability(
                           ctx,
                           translator.getTypeSystem(),
                           result.model,
-                          /* isApproximate= */ false))
-              : CelVerificationResult.verified();
+                          /* isApproximate= */ false,
+                          /* isCounterexample= */ true))
+              : CelVerificationResult.verified(
+                  "Condition is satisfiable."
+                      + getCounterexampleString(
+                          ctx,
+                          translator.getTypeSystem(),
+                          result.model,
+                          /* isApproximate= */ false,
+                          /* isCounterexample= */ false));
 
         case APPROXIMATE_MATCH:
           String prefix =
@@ -263,7 +279,11 @@ private CelVerificationResult checkSatisfiability(
           return CelVerificationResult.inconclusive(
               prefix
                   + getCounterexampleString(
-                      ctx, translator.getTypeSystem(), result.model, /* isApproximate= */ true));
+                      ctx,
+                      translator.getTypeSystem(),
+                      result.model,
+                      /* isApproximate= */ true,
+                      /* isCounterexample= */ searchForCounterexample));
 
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
@@ -357,8 +377,13 @@ private Solver newSolver(Context ctx) {
   }
 
   private static String getCounterexampleString(
-      Context ctx, CelZ3TypeSystem typeSystem, Model model, boolean isApproximate) {
-    return CelZ3CounterexampleGenerator.generate(ctx, typeSystem, model, isApproximate);
+      Context ctx,
+      CelZ3TypeSystem typeSystem,
+      Model model,
+      boolean isApproximate,
+      boolean isCounterexample) {
+    return CelZ3CounterexampleGenerator.generate(
+        ctx, typeSystem, model, isApproximate, isCounterexample);
   }
 
   CelVerifierZ3Impl(

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

@@ -36,7 +36,11 @@ final class CelZ3CounterexampleGenerator {
   private CelZ3CounterexampleGenerator() {}
 
   static String generate(
-      Context ctx, CelZ3TypeSystem typeSystem, Model model, boolean isApproximate) {
+      Context ctx,
+      CelZ3TypeSystem typeSystem,
+      Model model,
+      boolean isApproximate,
+      boolean isCounterexample) {
     FuncDecl[] constDecls = model.getConstDecls();
 
     List<String> bindings = new ArrayList<>();
@@ -55,10 +59,17 @@ static String generate(
     }
 
     if (bindings.isEmpty()) {
-      return " (The expression fails unconditionally, regardless of input state)";
+      return isCounterexample
+          ? " (The expression fails unconditionally, regardless of input state)"
+          : " (The expression is satisfiable unconditionally, regardless of input state)";
     }
 
-    String prefix = isApproximate ? " Potential counterexample input:" : " Counterexample input:";
+    String prefix;
+    if (isCounterexample) {
+      prefix = isApproximate ? " Potential counterexample input:" : " Counterexample input:";
+    } else {
+      prefix = isApproximate ? " Potential satisfying input:" : " Satisfying input:";
+    }
     return prefix + String.join("", bindings);
   }
 
@@ -228,6 +239,9 @@ private static void extractKeys(Expr<?> arrayExpr, List<Expr<?>> keys) {
       if (++iterations > 100_000) {
         throw new IllegalStateException("Exceeded maximum number of extractKeys iterations.");
       }
+      if (!arrayExpr.isApp()) {
+        break;
+      }
       FuncDecl<?> decl = arrayExpr.getFuncDecl();
       String declName = decl.getName().toString();
 

verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java

@@ -172,6 +172,43 @@ public void isSatisfiable_success(@TestParameter IsSatisfiableTestCase testCase)
     assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED);
   }
 
+  @Test
+  public void isSatisfiable_withVariable_returnsSatisfyingModel() throws Exception {
+    CelAbstractSyntaxTree ast = CEL.compile("x > 5").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()).containsMatch("x = (?:[6-9]|[1-9]\\d+)");
+  }
+
+  @Test
+  public void isSatisfiable_unconditional_returnsUnconditionalMessage() throws Exception {
+    CelAbstractSyntaxTree ast = CEL.compile("1 + 1 == 2").getAst();
+
+    CelVerificationResult result = VERIFIER.isSatisfiable(ast);
+
+    assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED);
+    assertThat(result.message())
+        .isEqualTo(
+            "Condition is satisfiable. (The expression is satisfiable unconditionally, regardless"
+                + " of input state)");
+  }
+
+  @Test
+  public void isSatisfiable_approximate_returnsPotentialSatisfyingInput() throws Exception {
+    CelAbstractSyntaxTree ast = CEL.compile("int('123') == 123 ? x > 5 : false").getAst();
+
+    CelVerificationResult result = VERIFIER.isSatisfiable(ast);
+
+    assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
+    assertThat(result.message()).contains("Inconclusive: a satisfying model may exist");
+    assertThat(result.message()).contains("Potential satisfying input:");
+    assertThat(result.message()).containsMatch("x = (?:[6-9]|[1-9]\\d+)");
+  }
+
   private enum IsSatisfiableInconclusiveTestCase {
     MASKED_BY_BMC("int_list == [1, 2, 3, 4, 5, 6] ? int_list.exists(x, x == 42) : false"),
     MASKED_BY_BMC_ALL("int_list == [1, 2, 3, 4, 5, 6] ? int_list.all(x, x > 0) : false"),