Internal Changes

PiperOrigin-RevId: 949795380

Author: l46kok

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

@@ -141,14 +141,14 @@ public CelVerifier build() {
   public CelVerificationResult isSatisfiable(CelAbstractSyntaxTree ast)
       throws CelVerificationException {
     Preconditions.checkArgument(ast.isChecked(), "AST must be type-checked.");
-    return checkSatisfiability(ast, false);
+    return checkSatisfiability(ast, /* searchForCounterexample= */ false);
   }
 
   @Override
   public CelVerificationResult isAlwaysTrue(CelAbstractSyntaxTree ast)
       throws CelVerificationException {
     Preconditions.checkArgument(ast.isChecked(), "AST must be type-checked.");
-    return checkSatisfiability(ast, true);
+    return checkSatisfiability(ast, /* searchForCounterexample= */ true);
   }
 
   @Override
@@ -191,12 +191,14 @@ public CelVerificationResult verifyEquivalence(
         case EXACT_MATCH:
           return CelVerificationResult.failed(
               "Equivalence violation detected."
-                  + getCounterexampleString(ctx, translator.getTypeSystem(), result.model));
+                  + getCounterexampleString(
+                      ctx, translator.getTypeSystem(), result.model, /* isApproximate= */ false));
         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));
+                  + getCounterexampleString(
+                      ctx, translator.getTypeSystem(), result.model, /* isApproximate= */ true));
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
               "Inconclusive: expressions are equivalent within the current loop unroll limit, but"
@@ -244,7 +246,11 @@ private CelVerificationResult checkSatisfiability(
           return searchForCounterexample
               ? CelVerificationResult.failed(
                   "Condition is not always true."
-                      + getCounterexampleString(ctx, translator.getTypeSystem(), result.model))
+                      + getCounterexampleString(
+                          ctx,
+                          translator.getTypeSystem(),
+                          result.model,
+                          /* isApproximate= */ false))
               : CelVerificationResult.verified();
 
         case APPROXIMATE_MATCH:
@@ -255,7 +261,9 @@ private CelVerificationResult checkSatisfiability(
                   : "Inconclusive: a satisfying model may exist, but it depends on"
                       + " approximations, missing theories, or loop bounds.";
           return CelVerificationResult.inconclusive(
-              prefix + getCounterexampleString(ctx, translator.getTypeSystem(), result.model));
+              prefix
+                  + getCounterexampleString(
+                      ctx, translator.getTypeSystem(), result.model, /* isApproximate= */ true));
 
         case TRUNCATED:
           return CelVerificationResult.inconclusive(
@@ -349,8 +357,8 @@ private Solver newSolver(Context ctx) {
   }
 
   private static String getCounterexampleString(
-      Context ctx, CelZ3TypeSystem typeSystem, Model model) {
-    return CelZ3CounterexampleGenerator.generate(ctx, typeSystem, model);
+      Context ctx, CelZ3TypeSystem typeSystem, Model model, boolean isApproximate) {
+    return CelZ3CounterexampleGenerator.generate(ctx, typeSystem, model, isApproximate);
   }
 
   CelVerifierZ3Impl(

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

@@ -35,7 +35,8 @@ final class CelZ3CounterexampleGenerator {
 
   private CelZ3CounterexampleGenerator() {}
 
-  static String generate(Context ctx, CelZ3TypeSystem typeSystem, Model model) {
+  static String generate(
+      Context ctx, CelZ3TypeSystem typeSystem, Model model, boolean isApproximate) {
     FuncDecl[] constDecls = model.getConstDecls();
 
     List<String> bindings = new ArrayList<>();
@@ -57,7 +58,8 @@ static String generate(Context ctx, CelZ3TypeSystem typeSystem, Model model) {
       return " (The expression fails unconditionally, regardless of input state)";
     }
 
-    return " Counterexample input:" + String.join("", bindings);
+    String prefix = isApproximate ? " Potential counterexample input:" : " Counterexample input:";
+    return prefix + String.join("", bindings);
   }
 
   private static String formatExpr(

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

@@ -602,7 +602,8 @@ private enum IsAlwaysTrueTestCase {
         "'key' in string_int_map ? type(string_int_map['key']) == int : true"),
     LITERAL_LIST_INDEX("[1, 2][0] == 1"),
     NESTED_LIST_VARIABLES_EQUALITY(
-        "nested_list == [[1]] && nested_list_2 == [[1]] ? nested_list == nested_list_2 : true");
+        "nested_list == [[1]] && nested_list_2 == [[1]] ? nested_list == nested_list_2 : true"),
+    ;
 
     final String expr;
 
@@ -1124,6 +1125,17 @@ public void isAlwaysTrue_inconclusive(@TestParameter IsInconclusiveTestCase test
     assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
   }
 
+  @Test
+  public void isAlwaysTrue_inconclusive_containsPotentialCounterexample() throws Exception {
+    CelAbstractSyntaxTree ast = CEL.compile("request.matches('^[a-z]+$') == true").getAst();
+
+    CelVerificationResult result = VERIFIER.isAlwaysTrue(ast);
+
+    assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
+    assertThat(result.message())
+        .containsMatch("Potential counterexample input:\\n\\s*request = .*");
+  }
+
   private enum EquivalenceInconclusiveTestCase {
     MASKED_BY_BMC(
         "int_list == [1, 2, 3, 4, 5, 6] ? int_list.all(x, x > 0) : true",