Skip to content

Commit 3cccc68

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Structured counterexample and CEGAR
PiperOrigin-RevId: 965286727
1 parent 5cf3ab3 commit 3cccc68

12 files changed

Lines changed: 1847 additions & 199 deletions

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

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ package(
1111
java_library(
1212
name = "verifier",
1313
srcs = [
14+
"CelCounterexample.java",
1415
"CelVerificationException.java",
1516
"CelVerificationResult.java",
1617
"CelVerifier.java",
@@ -23,6 +24,8 @@ java_library(
2324
"//common:cel_ast",
2425
"//common/types:type_providers",
2526
"@maven//:com_google_errorprone_error_prone_annotations",
27+
"@maven//:com_google_guava_guava",
28+
"@maven//:org_jspecify_jspecify",
2629
],
2730
)
2831

@@ -153,6 +156,7 @@ java_library(
153156
java_library(
154157
name = "z3_impl",
155158
srcs = [
159+
"CegarRefiner.java",
156160
"CelAstAlphaHasher.java",
157161
"CelAstToZ3Translator.java",
158162
"CelVerifierZ3Impl.java",
@@ -180,9 +184,12 @@ java_library(
180184
"//common/types",
181185
"//common/types:cel_types",
182186
"//common/types:type_providers",
187+
"//common/values:cel_byte_string",
188+
"//common/values:cel_value_provider",
183189
"//optimizer",
184190
"//optimizer:optimization_exception",
185191
"//optimizer:optimizer_builder",
192+
"//runtime:evaluation_exception",
186193
"//verifier/axioms",
187194
"@maven//:com_google_errorprone_error_prone_annotations",
188195
"@maven//:com_google_guava_guava",

‎verifier/src/main/java/dev/cel/verifier/CegarRefiner.java‎

Lines changed: 137 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,137 @@
1+
// Copyright 2026 Google LLC
2+
//
3+
// Licensed under the Apache License, Version 2.0 (the "License");
4+
// you may not use this file except in compliance with the License.
5+
// You may obtain a copy of the License at
6+
//
7+
// https://www.apache.org/licenses/LICENSE-2.0
8+
//
9+
// Unless required by applicable law or agreed to in writing, software
10+
// distributed under the License is distributed on an "AS IS" BASIS,
11+
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12+
// See the License for the specific language governing permissions and
13+
// limitations under the License.
14+
15+
package dev.cel.verifier;
16+
17+
import com.google.common.base.Preconditions;
18+
import com.google.common.collect.ImmutableMap;
19+
import com.google.errorprone.annotations.Immutable;
20+
import dev.cel.bundle.Cel;
21+
import dev.cel.common.CelAbstractSyntaxTree;
22+
import dev.cel.runtime.CelEvaluationException;
23+
import java.util.HashMap;
24+
import java.util.Map;
25+
import java.util.Objects;
26+
import java.util.Optional;
27+
28+
/**
29+
* Evaluates candidate counterexample models against the concrete CEL runtime to confirm or refute
30+
* potential violations (CEGAR refinement loop).
31+
*/
32+
@Immutable
33+
final class CegarRefiner {
34+
35+
@Immutable
36+
static final class CegarOutcome {
37+
private final boolean isViolation;
38+
private final Optional<String> evaluationErrorMessage;
39+
40+
static CegarOutcome violation() {
41+
return new CegarOutcome(true, Optional.empty());
42+
}
43+
44+
static CegarOutcome spurious() {
45+
return new CegarOutcome(false, Optional.empty());
46+
}
47+
48+
static CegarOutcome evaluationError(String errorMessage) {
49+
return new CegarOutcome(false, Optional.of(errorMessage));
50+
}
51+
52+
private CegarOutcome(boolean isViolation, Optional<String> evaluationErrorMessage) {
53+
this.isViolation = isViolation;
54+
this.evaluationErrorMessage = evaluationErrorMessage;
55+
}
56+
57+
boolean isViolation() {
58+
return isViolation;
59+
}
60+
61+
Optional<String> evaluationErrorMessage() {
62+
return evaluationErrorMessage;
63+
}
64+
}
65+
66+
private final Cel cel;
67+
68+
CegarRefiner(Cel cel) {
69+
this.cel = Preconditions.checkNotNull(cel);
70+
}
71+
72+
CegarOutcome refineEquivalence(
73+
CelAbstractSyntaxTree astA, CelAbstractSyntaxTree astB, CelCounterexample model) {
74+
if (model.isSatisfyingInput()) {
75+
return CegarOutcome.spurious();
76+
}
77+
try {
78+
ImmutableMap<String, Object> evalContext = model.toEvaluationContext();
79+
Object resA = cel.createProgram(astA).eval(evalContext);
80+
Object resB = cel.createProgram(astB).eval(evalContext);
81+
// If concrete evaluation produces identical results, the candidate SMT divergence was an
82+
// artifact of abstraction (spurious). Otherwise, concrete outputs diverge (violation).
83+
return Objects.equals(resA, resB) ? CegarOutcome.spurious() : CegarOutcome.violation();
84+
} catch (CelEvaluationException e) {
85+
return CegarOutcome.evaluationError(e.getMessage());
86+
}
87+
}
88+
89+
CegarOutcome refineSatisfiability(
90+
CelAbstractSyntaxTree ast, boolean searchForCounterexample, CelCounterexample model) {
91+
if (searchForCounterexample ? model.isSatisfyingInput() : !model.isSatisfyingInput()) {
92+
return CegarOutcome.spurious();
93+
}
94+
try {
95+
ImmutableMap<String, Object> evalContext = model.toEvaluationContext();
96+
Object res = cel.createProgram(ast).eval(evalContext);
97+
boolean isEvaluationTrue = Objects.equals(res, true);
98+
// For universal truth (searchForCounterexample=true), evaluating to true refutes the
99+
// candidate counterexample (spurious). For satisfiability search
100+
// (searchForCounterexample=false),
101+
// evaluating to true confirms the candidate satisfying model (violation).
102+
boolean isSpurious = searchForCounterexample == isEvaluationTrue;
103+
return isSpurious ? CegarOutcome.spurious() : CegarOutcome.violation();
104+
} catch (CelEvaluationException e) {
105+
return CegarOutcome.evaluationError(e.getMessage());
106+
}
107+
}
108+
109+
CegarOutcome refineImplication(
110+
CelAbstractSyntaxTree assumeAst,
111+
CelAbstractSyntaxTree assertAst,
112+
Map<String, CelAbstractSyntaxTree> boundSymbols,
113+
CelCounterexample model) {
114+
if (model.isSatisfyingInput()) {
115+
return CegarOutcome.spurious();
116+
}
117+
try {
118+
Map<String, Object> evalContext = new HashMap<>(model.toEvaluationContext());
119+
for (Map.Entry<String, CelAbstractSyntaxTree> entry : boundSymbols.entrySet()) {
120+
Object boundVal = cel.createProgram(entry.getValue()).eval(evalContext);
121+
evalContext.put(entry.getKey(), boundVal);
122+
}
123+
Object assumeVal = cel.createProgram(assumeAst).eval(evalContext);
124+
if (Objects.equals(assumeVal, true)) {
125+
Object assertVal = cel.createProgram(assertAst).eval(evalContext);
126+
// If the premise holds and the conclusion evaluates to true, the candidate counterexample
127+
// is refuted (spurious). If the conclusion fails under true premise, implication is
128+
// violated.
129+
return Objects.equals(assertVal, true) ? CegarOutcome.spurious() : CegarOutcome.violation();
130+
}
131+
// The candidate input did not satisfy the premise, so it cannot serve as a counterexample.
132+
return CegarOutcome.spurious();
133+
} catch (CelEvaluationException e) {
134+
return CegarOutcome.evaluationError(e.getMessage());
135+
}
136+
}
137+
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -610,7 +610,7 @@ private FieldAccess getMapAccess(Expr<?> operand, String field, BoolExpr typeGua
610610
typeConstraints.add(
611611
ctx.mkImplies(
612612
CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, (BoolExpr) presence), valNotError));
613-
if (unknownIdentifiers.isEmpty()) {
613+
if (!unknownIdentifiers.contains(field)) {
614614
BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(value));
615615
typeConstraints.add(
616616
ctx.mkImplies(
@@ -630,7 +630,7 @@ private FieldAccess getMsgAccess(Expr<?> operand, String field, BoolExpr typeGua
630630
typeConstraints.add(
631631
ctx.mkImplies(
632632
CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, (BoolExpr) presence), valNotError));
633-
if (unknownIdentifiers.isEmpty()) {
633+
if (!unknownIdentifiers.contains(field)) {
634634
BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(value));
635635
typeConstraints.add(
636636
ctx.mkImplies(

‎verifier/src/main/java/dev/cel/verifier/CelCounterexample.java‎

Lines changed: 99 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,99 @@
1+
// Copyright 2026 Google LLC
2+
//
3+
// Licensed under the Apache License, Version 2.0 (the "License");
4+
// you may not use this file except in compliance with the License.
5+
// You may obtain a copy of the License at
6+
//
7+
// https://www.apache.org/licenses/LICENSE-2.0
8+
//
9+
// Unless required by applicable law or agreed to in writing, software
10+
// distributed under the License is distributed on an "AS IS" BASIS,
11+
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12+
// See the License for the specific language governing permissions and
13+
// limitations under the License.
14+
15+
package dev.cel.verifier;
16+
17+
import com.google.auto.value.AutoValue;
18+
import com.google.common.collect.ImmutableMap;
19+
import com.google.errorprone.annotations.Immutable;
20+
import dev.cel.common.types.CelType;
21+
import java.util.Map;
22+
import java.util.Optional;
23+
import org.jspecify.annotations.Nullable;
24+
25+
/** Encapsulates a structured variable assignment model produced by formal verification. */
26+
@AutoValue
27+
@AutoValue.CopyAnnotations
28+
@Immutable
29+
public abstract class CelCounterexample {
30+
31+
/** Represents a single variable binding within a counterexample. */
32+
@AutoValue
33+
@AutoValue.CopyAnnotations
34+
@Immutable
35+
@SuppressWarnings("Immutable") // Values are deeply immutable.
36+
public abstract static class Binding {
37+
/** Returns the name of the variable. */
38+
public abstract String name();
39+
40+
/** Returns the inferred CEL type of the variable. */
41+
public abstract CelType type();
42+
43+
/**
44+
* Returns the native Java representation of the value (e.g., Long, Boolean, String, Instant,
45+
* Duration, ImmutableList, ImmutableMap, Message, etc.), or empty if unassigned or unavailable.
46+
*/
47+
public abstract Optional<Object> nativeValue();
48+
49+
/**
50+
* Returns the CEL literal representation of the value (e.g., "80", "\"admin\"", "true", "[1,
51+
* 2]").
52+
*/
53+
public abstract String celString();
54+
55+
public static Binding of(
56+
String name, CelType type, @Nullable Object nativeValue, String celString) {
57+
return new AutoValue_CelCounterexample_Binding(
58+
name, type, Optional.ofNullable(nativeValue), celString);
59+
}
60+
}
61+
62+
/** Returns all variable bindings keyed by variable name. */
63+
public abstract ImmutableMap<String, Binding> bindings();
64+
65+
/** Returns true if this counterexample was derived from an approximate solver model. */
66+
public abstract boolean isApproximate();
67+
68+
/** Returns true if this model represents a satisfying assignment rather than a counterexample. */
69+
public abstract boolean isSatisfyingInput();
70+
71+
/** Returns the formatted display string representation. */
72+
public abstract String toDisplayString();
73+
74+
/** Looks up a variable binding by name. */
75+
public Optional<Binding> get(String variableName) {
76+
return Optional.ofNullable(bindings().get(variableName));
77+
}
78+
79+
/**
80+
* Returns a native Java variable map suitable for evaluating expressions in CelRuntime (e.g.,
81+
* Cel.createProgram().eval(toEvaluationContext())).
82+
*/
83+
public ImmutableMap<String, Object> toEvaluationContext() {
84+
ImmutableMap.Builder<String, Object> builder = ImmutableMap.builder();
85+
for (Binding binding : bindings().values()) {
86+
binding.nativeValue().ifPresent(value -> builder.put(binding.name(), value));
87+
}
88+
return builder.buildOrThrow();
89+
}
90+
91+
public static CelCounterexample create(
92+
Map<String, Binding> bindings,
93+
boolean isApproximate,
94+
boolean isSatisfyingInput,
95+
String toDisplayString) {
96+
return new AutoValue_CelCounterexample(
97+
ImmutableMap.copyOf(bindings), isApproximate, isSatisfyingInput, toDisplayString);
98+
}
99+
}

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

Lines changed: 29 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -15,9 +15,12 @@
1515
package dev.cel.verifier;
1616

1717
import com.google.auto.value.AutoValue;
18+
import com.google.errorprone.annotations.Immutable;
19+
import java.util.Optional;
1820

1921
/** Result object containing the outcome of a CEL AST verification check. */
2022
@AutoValue
23+
@Immutable
2124
public abstract class CelVerificationResult {
2225

2326
/** Represents the outcome of the verification process. */
@@ -38,11 +41,12 @@ public enum VerificationStatus {
3841
*/
3942
public abstract String reason();
4043

41-
/**
42-
* Returns a detailed counterexample or satisfying model assignment, if one was found.
43-
*/
44+
/** Returns a detailed counterexample or satisfying model assignment string, if one was found. */
4445
public abstract String counterexample();
4546

47+
/** Returns the structured counterexample or satisfying model assignment, if one was found. */
48+
public abstract Optional<CelCounterexample> counterexampleModel();
49+
4650
/**
4751
* Returns a message detailing the outcome of the verification check, such as a counterexample
4852
* input, satisfying model assignments, or truncation reason. May be empty if status is VERIFIED
@@ -53,28 +57,41 @@ public String message() {
5357
}
5458

5559
static CelVerificationResult verified() {
56-
return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", "");
60+
return new AutoValue_CelVerificationResult(
61+
VerificationStatus.VERIFIED, "", "", Optional.empty());
5762
}
5863

59-
static CelVerificationResult verified(String reason) {
60-
return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, "");
64+
static CelVerificationResult verified(String reason, CelCounterexample counterexample) {
65+
return new AutoValue_CelVerificationResult(
66+
VerificationStatus.VERIFIED,
67+
reason,
68+
counterexample.toDisplayString(),
69+
Optional.of(counterexample));
6170
}
6271

6372
static CelVerificationResult failed(String reason) {
64-
return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, "");
73+
return new AutoValue_CelVerificationResult(
74+
VerificationStatus.VIOLATED, reason, "", Optional.empty());
6575
}
6676

67-
static CelVerificationResult failed(String reason, String counterexample) {
77+
static CelVerificationResult failed(String reason, CelCounterexample counterexample) {
6878
return new AutoValue_CelVerificationResult(
69-
VerificationStatus.VIOLATED, reason, counterexample);
79+
VerificationStatus.VIOLATED,
80+
reason,
81+
counterexample.toDisplayString(),
82+
Optional.of(counterexample));
7083
}
7184

7285
static CelVerificationResult inconclusive(String reason) {
73-
return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, "");
86+
return new AutoValue_CelVerificationResult(
87+
VerificationStatus.INCONCLUSIVE, reason, "", Optional.empty());
7488
}
7589

76-
static CelVerificationResult inconclusive(String reason, String counterexample) {
90+
static CelVerificationResult inconclusive(String reason, CelCounterexample counterexample) {
7791
return new AutoValue_CelVerificationResult(
78-
VerificationStatus.INCONCLUSIVE, reason, counterexample);
92+
VerificationStatus.INCONCLUSIVE,
93+
reason,
94+
counterexample.toDisplayString(),
95+
Optional.of(counterexample));
7996
}
8097
}

‎verifier/src/main/java/dev/cel/verifier/CelVerifierBuilder.java‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,23 @@ public interface CelVerifierBuilder {
8282
@CanIgnoreReturnValue
8383
CelVerifierBuilder setComprehensionUnrollLimit(int unrollLimit);
8484

85+
/**
86+
* Enables or disables Counterexample-Guided Abstraction Refinement (CEGAR).
87+
*
88+
* <p>When enabled, if the SMT solver returns an approximate model (e.g., due to unmodeled custom
89+
* functions, approximations, or bounded loops), the candidate inputs are validated using concrete
90+
* {@link dev.cel.bundle.Cel} program execution. If concrete evaluation confirms an invariant
91+
* violation or equivalence divergence, the result is upgraded from {@code INCONCLUSIVE} to {@code
92+
* VIOLATED}.
93+
*
94+
* <p><strong>Note:</strong> This option requires an execution-ready CEL environment where any
95+
* custom functions referenced in the policy have registered runtime {@link
96+
* dev.cel.runtime.CelFunctionBinding} implementations. In declaration-only environments (e.g.,
97+
* static linters without runtime bindings), this should remain disabled.
98+
*/
99+
@CanIgnoreReturnValue
100+
CelVerifierBuilder setEnableCegarRefinement(boolean enableCegarRefinement);
101+
85102
/** Builds the {@link CelVerifier} instance. */
86103
CelVerifier build();
87104
}

0 commit comments

Comments
 (0)