diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index cef976608..ebc53b3db 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -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() {} @@ -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))); } } @@ -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())) { @@ -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())) { @@ -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()"; } @@ -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, @@ -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)"); @@ -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, @@ -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) { @@ -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, @@ -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> keys = new LinkedHashSet<>(); extractKeys(presenceArray, keys); @@ -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)); } } diff --git a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java index 5a9eaea02..b0611b634 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java @@ -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