Skip to content

Commit 064ec2f

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Make invariant violation messages policy-specific
PiperOrigin-RevId: 953023510
1 parent db6432f commit 064ec2f

5 files changed

Lines changed: 95 additions & 53 deletions

File tree

‎verifier/README.md‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -353,7 +353,7 @@ public class InvariantsExample {
353353
System.out.println("Invariant violated!");
354354
System.out.println(result.message());
355355
// Output:
356-
// Implication violation detected. Counterexample input:
356+
// Invariant 'always_secure' violation detected. Counterexample input:
357357
// port = 80
358358
break;
359359
case INCONCLUSIVE:

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

Lines changed: 19 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -145,10 +145,28 @@ public ImmutableMap<String, CelVerificationResult> verifyInvariants(CelPolicy po
145145
throw new UnsupportedOperationException(
146146
"Invariants verification requires Z3 verifier implementation.");
147147
}
148+
String invariantId = invariant.invariantId().value();
148149
CelVerificationResult result =
149150
((CelVerifierZ3Impl) astVerifier)
150151
.verifyImplication(assumeAst, assertAst, boundSymbols);
151-
resultsBuilder.put(invariant.invariantId().value(), result);
152+
if (result.status() == CelVerificationResult.VerificationStatus.VIOLATED) {
153+
String newReason =
154+
result.reason().replaceFirst(
155+
"^Implication", String.format("Invariant '%s'", invariantId));
156+
result =
157+
result.counterexample().isPresent()
158+
? CelVerificationResult.failed(newReason, result.counterexample().get())
159+
: CelVerificationResult.failed(newReason);
160+
} else if (result.status() == CelVerificationResult.VerificationStatus.INCONCLUSIVE) {
161+
String newReason =
162+
result.reason().replaceFirst(
163+
"^Inconclusive: implication", String.format("Inconclusive: invariant '%s'", invariantId));
164+
result =
165+
result.counterexample().isPresent()
166+
? CelVerificationResult.inconclusive(newReason, result.counterexample().get())
167+
: CelVerificationResult.inconclusive(newReason);
168+
}
169+
resultsBuilder.put(invariantId, result);
152170
}
153171

154172
return resultsBuilder.buildOrThrow();

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

Lines changed: 31 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
package dev.cel.verifier;
1616

1717
import com.google.auto.value.AutoValue;
18+
import java.util.Optional;
1819

1920
/** Result object containing the outcome of a CEL AST verification check. */
2021
@AutoValue
@@ -33,26 +34,48 @@ public enum VerificationStatus {
3334
/** Returns the status of the verification check. */
3435
public abstract VerificationStatus status();
3536

37+
/**
38+
* Returns the primary reason for the verification outcome.
39+
*/
40+
public abstract String reason();
41+
42+
/**
43+
* Returns a detailed counterexample or satisfying model assignment, if one was found.
44+
*/
45+
public abstract Optional<String> counterexample();
46+
3647
/**
3748
* Returns a message detailing the outcome of the verification check, such as a counterexample
3849
* input, satisfying model assignments, or truncation reason. May be empty if status is VERIFIED
3950
* and no model inputs apply (e.g., when verifying isAlwaysTrue without counterexamples).
4051
*/
41-
public abstract String message();
52+
public String message() {
53+
return reason() + counterexample().orElse("");
54+
}
4255

4356
static CelVerificationResult verified() {
44-
return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "");
57+
return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", Optional.empty());
58+
}
59+
60+
static CelVerificationResult verified(String reason) {
61+
return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, Optional.empty());
62+
}
63+
64+
static CelVerificationResult failed(String reason) {
65+
return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, Optional.empty());
4566
}
4667

47-
static CelVerificationResult verified(String message) {
48-
return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, message);
68+
static CelVerificationResult failed(String reason, String counterexample) {
69+
return new AutoValue_CelVerificationResult(
70+
VerificationStatus.VIOLATED, reason, Optional.of(counterexample));
4971
}
5072

51-
static CelVerificationResult failed(String message) {
52-
return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, message);
73+
static CelVerificationResult inconclusive(String reason) {
74+
return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, Optional.empty());
5375
}
5476

55-
static CelVerificationResult inconclusive(String message) {
56-
return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, message);
77+
static CelVerificationResult inconclusive(String reason, String counterexample) {
78+
return new AutoValue_CelVerificationResult(
79+
VerificationStatus.INCONCLUSIVE, reason, Optional.of(counterexample));
5780
}
5881
}

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

Lines changed: 42 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -193,23 +193,23 @@ public CelVerificationResult verifyEquivalence(
193193
switch (result.outcome) {
194194
case EXACT_MATCH:
195195
return CelVerificationResult.failed(
196-
"Equivalence violation detected."
197-
+ getCounterexampleString(
198-
ctx,
199-
translator.getTypeSystem(),
200-
result.model,
201-
/* isApproximate= */ false,
202-
/* isCounterexample= */ true));
196+
"Equivalence violation detected.",
197+
getCounterexampleString(
198+
ctx,
199+
translator.getTypeSystem(),
200+
result.model,
201+
/* isApproximate= */ false,
202+
/* isCounterexample= */ true));
203203
case APPROXIMATE_MATCH:
204204
return CelVerificationResult.inconclusive(
205205
"Inconclusive: a divergence may exist, but it depends on approximations, missing"
206-
+ " theories, or loop bounds."
207-
+ getCounterexampleString(
208-
ctx,
209-
translator.getTypeSystem(),
210-
result.model,
211-
/* isApproximate= */ true,
212-
/* isCounterexample= */ true));
206+
+ " theories, or loop bounds.",
207+
getCounterexampleString(
208+
ctx,
209+
translator.getTypeSystem(),
210+
result.model,
211+
/* isApproximate= */ true,
212+
/* isCounterexample= */ true));
213213
case TRUNCATED:
214214
return CelVerificationResult.inconclusive(
215215
"Inconclusive: expressions are equivalent within the current loop unroll limit, but"
@@ -282,23 +282,23 @@ CelVerificationResult verifyImplication(
282282
switch (result.outcome) {
283283
case EXACT_MATCH:
284284
return CelVerificationResult.failed(
285-
"Implication violation detected."
286-
+ getCounterexampleString(
287-
ctx,
288-
translator.getTypeSystem(),
289-
result.model,
290-
/* isApproximate= */ false,
291-
/* isCounterexample= */ true));
285+
"Implication violation detected.",
286+
getCounterexampleString(
287+
ctx,
288+
translator.getTypeSystem(),
289+
result.model,
290+
/* isApproximate= */ false,
291+
/* isCounterexample= */ true));
292292
case APPROXIMATE_MATCH:
293293
return CelVerificationResult.inconclusive(
294294
"Inconclusive: a counterexample may exist, but it depends on approximations, missing"
295-
+ " theories, or loop bounds."
296-
+ getCounterexampleString(
297-
ctx,
298-
translator.getTypeSystem(),
299-
result.model,
300-
/* isApproximate= */ true,
301-
/* isCounterexample= */ true));
295+
+ " theories, or loop bounds.",
296+
getCounterexampleString(
297+
ctx,
298+
translator.getTypeSystem(),
299+
result.model,
300+
/* isApproximate= */ true,
301+
/* isCounterexample= */ true));
302302
case TRUNCATED:
303303
return CelVerificationResult.inconclusive(
304304
"Inconclusive: implication holds within the current loop unroll limit, but"
@@ -345,13 +345,13 @@ private CelVerificationResult checkSatisfiability(
345345
case EXACT_MATCH:
346346
return searchForCounterexample
347347
? CelVerificationResult.failed(
348-
"Condition is not always true."
349-
+ getCounterexampleString(
350-
ctx,
351-
translator.getTypeSystem(),
352-
result.model,
353-
/* isApproximate= */ false,
354-
/* isCounterexample= */ true))
348+
"Condition is not always true.",
349+
getCounterexampleString(
350+
ctx,
351+
translator.getTypeSystem(),
352+
result.model,
353+
/* isApproximate= */ false,
354+
/* isCounterexample= */ true))
355355
: CelVerificationResult.verified(
356356
"Condition is satisfiable."
357357
+ getCounterexampleString(
@@ -369,13 +369,13 @@ private CelVerificationResult checkSatisfiability(
369369
: "Inconclusive: a satisfying model may exist, but it depends on"
370370
+ " approximations, missing theories, or loop bounds.";
371371
return CelVerificationResult.inconclusive(
372-
prefix
373-
+ getCounterexampleString(
374-
ctx,
375-
translator.getTypeSystem(),
376-
result.model,
377-
/* isApproximate= */ true,
378-
/* isCounterexample= */ searchForCounterexample));
372+
prefix,
373+
getCounterexampleString(
374+
ctx,
375+
translator.getTypeSystem(),
376+
result.model,
377+
/* isApproximate= */ true,
378+
/* isCounterexample= */ searchForCounterexample));
379379

380380
case TRUNCATED:
381381
return CelVerificationResult.inconclusive(

‎verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -526,7 +526,8 @@ public void verifyInvariants_workloadAdmissionFlawed_violationsDetected() throws
526526
.isEqualTo(VerificationStatus.VIOLATED);
527527
assertThat(results.get("universal_no_unapproved_privileged_prod").message())
528528
.isEqualTo(
529-
"Implication violation detected. Counterexample input:\n"
529+
"Invariant 'universal_no_unapproved_privileged_prod' violation detected."
530+
+ " Counterexample input:\n"
530531
+ " is_owner = false\n"
531532
+ " is_privileged = true\n"
532533
+ " is_prod = true\n"

0 commit comments

Comments
 (0)