From 4cd8411a5fa0c794077ed0a8ec5da074dc912ca4 Mon Sep 17 00:00:00 2001 From: Sokwhan Huh Date: Mon, 20 Jul 2026 14:46:20 -0700 Subject: [PATCH] Generate satisfiable model for isSatisfiable PiperOrigin-RevId: 951064191 --- .../cel/verifier/CelVerificationResult.java | 9 ++++- .../java/dev/cel/verifier/CelVerifier.java | 4 +- .../dev/cel/verifier/CelVerifierZ3Impl.java | 39 +++++++++++++++---- .../CelZ3CounterexampleGenerator.java | 20 ++++++++-- .../cel/verifier/CelVerifierZ3ImplTest.java | 37 ++++++++++++++++++ 5 files changed, 96 insertions(+), 13 deletions(-) diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java b/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java index b7510ccf0..f243537e1 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java @@ -34,8 +34,9 @@ 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(); @@ -43,6 +44,10 @@ 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); } diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifier.java b/verifier/src/main/java/dev/cel/verifier/CelVerifier.java index 7394886cb..32bffa1d3 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifier.java +++ b/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. */ diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index 35d847d1b..9d8b87e07 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/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( diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index 8dcc73435..5cea7468d 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/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 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> 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(); diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 898604808..f56c26cfc 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/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"),