Skip to content

Update p4_symbolic expected outputs for z3 5.1.0. #1353

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
copybara-service wants to merge 1 commit into
base: main
Choose a base branch
from
Open

Update p4_symbolic expected outputs for z3 5.1.0. #1353

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
48 changes: 28 additions & 20 deletions verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@
final class CelZ3CounterexampleGenerator {

private static final int MAX_ELEMENTS_TO_PRINT = 15;
private static final int MAX_NESTING_DEPTH = 32;

private CelZ3CounterexampleGenerator() {}

Expand All @@ -57,7 +58,7 @@ static String generate(
Expr<?> constInterp = model.getConstInterp(decl);
if (constInterp != null) {
bindings.add(
String.format("\n %s = %s", name, formatExpr(ctx, typeSystem, model, constInterp)));
String.format("\n %s = %s", name, formatExpr(ctx, typeSystem, model, constInterp, 0)));
}
}

Expand All @@ -77,22 +78,29 @@ static String generate(
}

private static String formatExpr(
Context ctx, CelZ3TypeSystem typeSystem, Model model, @Nullable Expr<?> expr) {
Context ctx, CelZ3TypeSystem typeSystem, Model model, @Nullable Expr<?> expr, int depth) {
Preconditions.checkState(expr != null, "Z3 failed to evaluate the expression natively.");
// Models may contain self-referential values (e.g. a map whose value refers back to the map
// itself), so bound the nesting depth to avoid unbounded recursion.
if (depth > MAX_NESTING_DEPTH) {
return "...";
}

FuncDecl decl = expr.getFuncDecl();

// Handle CelType constructors wrapper unwrapping
if (decl.equals(typeSystem.intCons().ConstructorDecl())) {
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]);
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0], depth + 1);
} else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) {
return "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")";
return "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0], depth + 1) + ")";
} else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) {
return "duration('" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "s')";
return "duration('"
+ formatExpr(ctx, typeSystem, model, expr.getArgs()[0], depth + 1)
+ "s')";
} else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) {
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u";
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0], depth + 1) + "u";
} else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) {
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]);
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0], depth + 1);
} else if (decl.equals(typeSystem.stringCons().ConstructorDecl())) {
return expr.getArgs()[0].toString();
} else if (decl.equals(typeSystem.bytesCons().ConstructorDecl())) {
Expand Down Expand Up @@ -121,11 +129,11 @@ private static String formatExpr(
}
return doubleArg.toString();
} else if (decl.equals(typeSystem.listCons().ConstructorDecl())) {
return reconstructList(ctx, typeSystem, model, expr.getArgs()[0]);
return reconstructList(ctx, typeSystem, model, expr.getArgs()[0], depth + 1);
} else if (decl.equals(typeSystem.mapCons().ConstructorDecl())) {
return reconstructMap(ctx, typeSystem, model, expr.getArgs()[0]);
return reconstructMap(ctx, typeSystem, model, expr.getArgs()[0], depth + 1);
} else if (decl.equals(typeSystem.messageCons().ConstructorDecl())) {
return reconstructMessage(ctx, typeSystem, model, expr.getArgs()[0]);
return reconstructMessage(ctx, typeSystem, model, expr.getArgs()[0], depth + 1);
} else if (decl.equals(typeSystem.errorCons().ConstructorDecl())) {
return "Error";
} else if (decl.equals(typeSystem.unknownCons().ConstructorDecl())) {
Expand All @@ -145,7 +153,7 @@ private static String formatExpr(
model,
typeSystem.getOptionalValue(optRef),
String.format("Z3 failed to evaluate optValue natively for %s", optRef));
return "optional(" + formatExpr(ctx, typeSystem, model, valueExpr) + ")";
return "optional(" + formatExpr(ctx, typeSystem, model, valueExpr, depth + 1) + ")";
} else if (hasValueExpr.isFalse()) {
return "optional.none()";
}
Expand All @@ -155,7 +163,7 @@ private static String formatExpr(
}

private static String reconstructList(
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> listRef) {
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> listRef, int depth) {
Expr<?> lenExpr =
evaluateStrict(
model,
Expand All @@ -173,7 +181,7 @@ private static String reconstructList(
ctx.mkNth(typeSystem.getSeq(listRef), ctx.mkInt(i)),
String.format(
"Z3 failed to evaluate list element at index %d for list %s", i, listRef));
elements.add(formatExpr(ctx, typeSystem, model, elem));
elements.add(formatExpr(ctx, typeSystem, model, elem, depth + 1));
}
if (length > printLimit) {
elements.add("... (" + (length - printLimit) + " more elements)");
Expand All @@ -183,7 +191,7 @@ private static String reconstructList(
}

private static String reconstructMap(
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> mapRef) {
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> mapRef, int depth) {
Expr<?> lenExpr =
evaluateStrict(
model,
Expand Down Expand Up @@ -218,9 +226,9 @@ private static String reconstructMap(
ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), key),
String.format("Z3 failed to evaluate map value for key %s in map %s", key, mapRef));
entries.add(
formatExpr(ctx, typeSystem, model, key)
formatExpr(ctx, typeSystem, model, key, depth + 1)
+ ": "
+ formatExpr(ctx, typeSystem, model, value));
+ formatExpr(ctx, typeSystem, model, value, depth + 1));
}
}
if (length > printLimit) {
Expand All @@ -231,7 +239,7 @@ private static String reconstructMap(
}

private static String reconstructMessage(
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> msgRef) {
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> msgRef, int depth) {
Expr<?> presenceArray =
evaluateStrict(
model,
Expand All @@ -244,7 +252,7 @@ private static String reconstructMessage(
typeSystem.getMsgTypeName(msgRef),
String.format("Z3 failed to evaluate type name natively for msg %s", msgRef));

String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", "");
String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr, depth + 1).replace("\"", "");

Set<Expr<?>> keys = new LinkedHashSet<>();
extractKeys(presenceArray, keys);
Expand All @@ -265,8 +273,8 @@ private static String reconstructMessage(
ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), key),
String.format("Z3 failed to evaluate msg value for key %s in msg %s", key, msgRef));

String fieldName = formatExpr(ctx, typeSystem, model, key).replace("\"", "");
entries.add(fieldName + ": " + formatExpr(ctx, typeSystem, model, value));
String fieldName = formatExpr(ctx, typeSystem, model, key, depth + 1).replace("\"", "");
entries.add(fieldName + ": " + formatExpr(ctx, typeSystem, model, value, depth + 1));
}
}

Expand Down
27 changes: 19 additions & 8 deletions verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -524,15 +524,26 @@ public void verifyInvariants_workloadAdmissionFlawed_violationsDetected() throws
assertThat(results).containsKey("universal_no_unapproved_privileged_prod");
assertThat(results.get("universal_no_unapproved_privileged_prod").status())
.isEqualTo(VerificationStatus.VIOLATED);
// Both counterexamples are valid bypasses of the invariant; which one is reported depends on
// the Z3 version (4.x vs. 5.x) used to solve the constraints.
String adminBypassCounterexample =
"Invariant 'universal_no_unapproved_privileged_prod' violation detected."
+ " Counterexample input:\n"
+ " is_owner = false\n"
+ " is_privileged = true\n"
+ " is_prod = true\n"
+ " has_approval = false\n"
+ " is_admin = true";
String ownerBypassCounterexample =
"Invariant 'universal_no_unapproved_privileged_prod' violation detected."
+ " Counterexample input:\n"
+ " is_owner = true\n"
+ " is_prod = true\n"
+ " has_approval = false\n"
+ " is_privileged = true\n"
+ " is_admin = false";
assertThat(results.get("universal_no_unapproved_privileged_prod").message())
.isEqualTo(
"Invariant 'universal_no_unapproved_privileged_prod' violation detected."
+ " Counterexample input:\n"
+ " is_owner = false\n"
+ " is_privileged = true\n"
+ " is_prod = true\n"
+ " has_approval = false\n"
+ " is_admin = true");
.isAnyOf(adminBypassCounterexample, ownerBypassCounterexample);
}

@Test
Expand Down
Loading