Skip to content

Commit 58d21ed

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

7 files changed

Lines changed: 105 additions & 67 deletions

File tree

‎verifier/BUILD.bazel‎

Lines changed: 17 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,25 @@ load("@rules_java//java:defs.bzl", "java_library")
22

33
package(
44
default_applicable_licenses = ["//:license"],
5-
default_visibility = ["//:internal"],
5+
default_visibility = [":verifier_allow_list"],
6+
)
7+
8+
VERIFIER_ALLOW_LIST = [
9+
"//...",
10+
]
11+
12+
package_group(
13+
name = "verifier_allow_list",
14+
packages = VERIFIER_ALLOW_LIST,
15+
)
16+
17+
package_group(
18+
name = "verifier_internal",
19+
packages = ["//verifier/..."],
620
)
721

822
java_library(
923
name = "verifier",
10-
visibility = [
11-
"//:internal",
12-
],
1324
exports = ["//verifier/src/main/java/dev/cel/verifier"],
1425
)
1526

@@ -27,22 +38,19 @@ java_library(
2738
java_library(
2839
name = "verifier_factory",
2940
compatible_with = [],
30-
visibility = [
31-
"//:internal",
32-
],
3341
exports = ["//verifier/src/main/java/dev/cel/verifier:verifier_factory"],
3442
)
3543

3644
java_library(
3745
name = "type_system",
3846
compatible_with = [],
39-
visibility = ["//:internal"],
47+
visibility = [":verifier_internal"],
4048
exports = ["//verifier/src/main/java/dev/cel/verifier:type_system"],
4149
)
4250

4351
java_library(
4452
name = "z3_impl",
4553
compatible_with = [],
46-
visibility = ["//:internal"],
54+
visibility = [":verifier_internal"],
4755
exports = ["//verifier/src/main/java/dev/cel/verifier:z3_impl"],
4856
)

‎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: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -145,10 +145,15 @@ 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)
150-
.verifyImplication(assumeAst, assertAst, boundSymbols);
151-
resultsBuilder.put(invariant.invariantId().value(), result);
151+
.verifyImplication(
152+
assumeAst,
153+
assertAst,
154+
boundSymbols,
155+
String.format("Invariant '%s'", invariantId));
156+
resultsBuilder.put(invariantId, result);
152157
}
153158

154159
return resultsBuilder.buildOrThrow();

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

Lines changed: 30 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -33,26 +33,48 @@ public enum VerificationStatus {
3333
/** Returns the status of the verification check. */
3434
public abstract VerificationStatus status();
3535

36+
/**
37+
* Returns the primary reason for the verification outcome.
38+
*/
39+
public abstract String reason();
40+
41+
/**
42+
* Returns a detailed counterexample or satisfying model assignment, if one was found.
43+
*/
44+
public abstract String counterexample();
45+
3646
/**
3747
* Returns a message detailing the outcome of the verification check, such as a counterexample
3848
* input, satisfying model assignments, or truncation reason. May be empty if status is VERIFIED
3949
* and no model inputs apply (e.g., when verifying isAlwaysTrue without counterexamples).
4050
*/
41-
public abstract String message();
51+
public String message() {
52+
return reason() + counterexample();
53+
}
4254

4355
static CelVerificationResult verified() {
44-
return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "");
56+
return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", "");
57+
}
58+
59+
static CelVerificationResult verified(String reason) {
60+
return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, "");
61+
}
62+
63+
static CelVerificationResult failed(String reason) {
64+
return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, "");
4565
}
4666

47-
static CelVerificationResult verified(String message) {
48-
return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, message);
67+
static CelVerificationResult failed(String reason, String counterexample) {
68+
return new AutoValue_CelVerificationResult(
69+
VerificationStatus.VIOLATED, reason, counterexample);
4970
}
5071

51-
static CelVerificationResult failed(String message) {
52-
return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, message);
72+
static CelVerificationResult inconclusive(String reason) {
73+
return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, "");
5374
}
5475

55-
static CelVerificationResult inconclusive(String message) {
56-
return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, message);
76+
static CelVerificationResult inconclusive(String reason, String counterexample) {
77+
return new AutoValue_CelVerificationResult(
78+
VerificationStatus.INCONCLUSIVE, reason, counterexample);
5779
}
5880
}

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

Lines changed: 47 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@
3636
import java.util.ArrayList;
3737
import java.util.Arrays;
3838
import java.util.List;
39+
import java.util.Locale;
3940
import java.util.Map;
4041
import java.util.Optional;
4142
import org.jspecify.annotations.Nullable;
@@ -193,23 +194,23 @@ public CelVerificationResult verifyEquivalence(
193194
switch (result.outcome) {
194195
case EXACT_MATCH:
195196
return CelVerificationResult.failed(
196-
"Equivalence violation detected."
197-
+ getCounterexampleString(
198-
ctx,
199-
translator.getTypeSystem(),
200-
result.model,
201-
/* isApproximate= */ false,
202-
/* isCounterexample= */ true));
197+
"Equivalence violation detected.",
198+
getCounterexampleString(
199+
ctx,
200+
translator.getTypeSystem(),
201+
result.model,
202+
/* isApproximate= */ false,
203+
/* isCounterexample= */ true));
203204
case APPROXIMATE_MATCH:
204205
return CelVerificationResult.inconclusive(
205206
"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));
207+
+ " theories, or loop bounds.",
208+
getCounterexampleString(
209+
ctx,
210+
translator.getTypeSystem(),
211+
result.model,
212+
/* isApproximate= */ true,
213+
/* isCounterexample= */ true));
213214
case TRUNCATED:
214215
return CelVerificationResult.inconclusive(
215216
"Inconclusive: expressions are equivalent within the current loop unroll limit, but"
@@ -227,7 +228,8 @@ public CelVerificationResult verifyEquivalence(
227228
CelVerificationResult verifyImplication(
228229
CelAbstractSyntaxTree assumeAst,
229230
CelAbstractSyntaxTree assertAst,
230-
Map<String, CelAbstractSyntaxTree> boundSymbols)
231+
Map<String, CelAbstractSyntaxTree> boundSymbols,
232+
String subjectName)
231233
throws CelVerificationException {
232234
Preconditions.checkArgument(assumeAst.isChecked(), "assumeAst must be type-checked.");
233235
Preconditions.checkArgument(assertAst.isChecked(), "assertAst must be type-checked.");
@@ -282,27 +284,27 @@ CelVerificationResult verifyImplication(
282284
switch (result.outcome) {
283285
case EXACT_MATCH:
284286
return CelVerificationResult.failed(
285-
"Implication violation detected."
286-
+ getCounterexampleString(
287-
ctx,
288-
translator.getTypeSystem(),
289-
result.model,
290-
/* isApproximate= */ false,
291-
/* isCounterexample= */ true));
287+
String.format("%s violation detected.", subjectName),
288+
getCounterexampleString(
289+
ctx,
290+
translator.getTypeSystem(),
291+
result.model,
292+
/* isApproximate= */ false,
293+
/* isCounterexample= */ true));
292294
case APPROXIMATE_MATCH:
293295
return CelVerificationResult.inconclusive(
294296
"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));
297+
+ " theories, or loop bounds.",
298+
getCounterexampleString(
299+
ctx,
300+
translator.getTypeSystem(),
301+
result.model,
302+
/* isApproximate= */ true,
303+
/* isCounterexample= */ true));
302304
case TRUNCATED:
303305
return CelVerificationResult.inconclusive(
304-
"Inconclusive: implication holds within the current loop unroll limit, but"
305-
+ " may be violated for larger collections.");
306+
String.format("Inconclusive: %s holds within the current loop unroll limit, but"
307+
+ " may be violated for larger collections.", subjectName.toLowerCase(Locale.US)));
306308
case NO_MATCH:
307309
return CelVerificationResult.verified();
308310
case SOLVER_UNKNOWN:
@@ -345,13 +347,13 @@ private CelVerificationResult checkSatisfiability(
345347
case EXACT_MATCH:
346348
return searchForCounterexample
347349
? CelVerificationResult.failed(
348-
"Condition is not always true."
349-
+ getCounterexampleString(
350-
ctx,
351-
translator.getTypeSystem(),
352-
result.model,
353-
/* isApproximate= */ false,
354-
/* isCounterexample= */ true))
350+
"Condition is not always true.",
351+
getCounterexampleString(
352+
ctx,
353+
translator.getTypeSystem(),
354+
result.model,
355+
/* isApproximate= */ false,
356+
/* isCounterexample= */ true))
355357
: CelVerificationResult.verified(
356358
"Condition is satisfiable."
357359
+ getCounterexampleString(
@@ -369,13 +371,13 @@ private CelVerificationResult checkSatisfiability(
369371
: "Inconclusive: a satisfying model may exist, but it depends on"
370372
+ " approximations, missing theories, or loop bounds.";
371373
return CelVerificationResult.inconclusive(
372-
prefix
373-
+ getCounterexampleString(
374-
ctx,
375-
translator.getTypeSystem(),
376-
result.model,
377-
/* isApproximate= */ true,
378-
/* isCounterexample= */ searchForCounterexample));
374+
prefix,
375+
getCounterexampleString(
376+
ctx,
377+
translator.getTypeSystem(),
378+
result.model,
379+
/* isApproximate= */ true,
380+
/* isCounterexample= */ searchForCounterexample));
379381

380382
case TRUNCATED:
381383
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"

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2604,7 +2604,7 @@ public void verifyImplication_loopExceedsLimit_returnsTruncatedInconclusive() th
26042604
CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(2).build();
26052605
CelVerificationResult result =
26062606
((CelVerifierZ3Impl) verifier)
2607-
.verifyImplication(assumeAst, assertAst, ImmutableMap.of());
2607+
.verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Implication");
26082608

26092609
assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE);
26102610
assertThat(result.message())

0 commit comments

Comments
 (0)