diff --git a/verifier/README.md b/verifier/README.md index d0c054485..5d5a111f5 100644 --- a/verifier/README.md +++ b/verifier/README.md @@ -224,8 +224,8 @@ public class PolicyVerifierExample { System.out.println(result.message()); // Output: // Equivalence violation detected. Counterexample input: - // country = "a" // role = "editor" + // country = "a" // port = 443 break; case INCONCLUSIVE: diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index 6b498a162..a5362e4f7 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel @@ -186,6 +186,7 @@ java_library( "//common/ast", "//common/ast:cel_block", "//common/internal:cel_descriptor_pools", + "//common/internal:proto_time_utils", "//common/internal:well_known_proto", "//common/types", "//common/types:cel_types", diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 404ed9900..db344960b 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -92,6 +92,11 @@ CelZ3TypeSystem getTypeSystem() { return typeSystem; } + /** Returns the input variables, in order of first appearance. */ + Set> getInputVariables() { + return context.inputVariables(); + } + /** * Returns a Z3 boolean expression asserting that the provided CEL value is a boolean and is true. */ diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index ceb5ae3d8..1e791994f 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -259,7 +259,7 @@ public CelVerificationResult verifyEquivalence( "Equivalence violation detected.", getCounterexampleString( ctx, - translator.getTypeSystem(), + translator, result.model, /* isApproximate= */ false, /* isCounterexample= */ true)); @@ -269,7 +269,7 @@ public CelVerificationResult verifyEquivalence( + " theories, or loop bounds.", getCounterexampleString( ctx, - translator.getTypeSystem(), + translator, result.model, /* isApproximate= */ true, /* isCounterexample= */ true)); @@ -345,7 +345,7 @@ CelVerificationResult verifyImplication( String.format("%s violation detected.", subjectName), getCounterexampleString( ctx, - translator.getTypeSystem(), + translator, result.model, /* isApproximate= */ false, /* isCounterexample= */ true)); @@ -355,7 +355,7 @@ CelVerificationResult verifyImplication( + " theories, or loop bounds.", getCounterexampleString( ctx, - translator.getTypeSystem(), + translator, result.model, /* isApproximate= */ true, /* isCounterexample= */ true)); @@ -408,7 +408,7 @@ private CelVerificationResult checkSatisfiability( "Condition is not always true.", getCounterexampleString( ctx, - translator.getTypeSystem(), + translator, result.model, /* isApproximate= */ false, /* isCounterexample= */ true)) @@ -416,7 +416,7 @@ private CelVerificationResult checkSatisfiability( "Condition is satisfiable." + getCounterexampleString( ctx, - translator.getTypeSystem(), + translator, result.model, /* isApproximate= */ false, /* isCounterexample= */ false)); @@ -432,7 +432,7 @@ private CelVerificationResult checkSatisfiability( prefix, getCounterexampleString( ctx, - translator.getTypeSystem(), + translator, result.model, /* isApproximate= */ true, /* isCounterexample= */ searchForCounterexample)); @@ -540,12 +540,17 @@ private CelAstToZ3Translator newTranslator(Context ctx, boolean parameterizeUnkn private static String getCounterexampleString( Context ctx, - CelZ3TypeSystem typeSystem, + CelAstToZ3Translator translator, Model model, boolean isApproximate, boolean isCounterexample) { return CelZ3CounterexampleGenerator.generate( - ctx, typeSystem, model, isApproximate, isCounterexample); + ctx, + translator.getTypeSystem(), + model, + translator.getInputVariables(), + isApproximate, + isCounterexample); } private enum SolverOutcome { diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index 22d7b8a42..95fe6f461 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -14,286 +14,225 @@ package dev.cel.verifier; -import com.google.common.base.Preconditions; +import static java.nio.charset.StandardCharsets.UTF_8; + import com.microsoft.z3.ArrayExpr; +import com.microsoft.z3.BitVecNum; import com.microsoft.z3.Context; import com.microsoft.z3.Expr; import com.microsoft.z3.FPNum; import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntNum; import com.microsoft.z3.Model; -import com.microsoft.z3.RatNum; +import dev.cel.common.internal.ProtoTimeUtils; import java.math.BigInteger; +import java.time.Instant; import java.util.ArrayList; import java.util.HashSet; import java.util.LinkedHashSet; import java.util.List; import java.util.Set; -import org.jspecify.annotations.Nullable; +import java.util.stream.IntStream; /** Generates human-readable counterexample strings from Z3 models. */ @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types. final class CelZ3CounterexampleGenerator { private static final int MAX_ELEMENTS_TO_PRINT = 15; + private static final BigInteger NANOS_PER_SECOND = + BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND); - private CelZ3CounterexampleGenerator() {} + private final Context ctx; + private final CelZ3TypeSystem typeSystem; + private final Model model; static String generate( Context ctx, CelZ3TypeSystem typeSystem, Model model, + Set> inputs, boolean isApproximate, boolean isCounterexample) { - FuncDecl[] constDecls = model.getConstDecls(); - - List bindings = new ArrayList<>(); - for (FuncDecl decl : constDecls) { - String name = decl.getName().toString(); - // Filter out internal solver-generated Skolem constants (e.g., k!1, seq.empty!0). - // `!` is not a valid CEL identifier. - if (name.contains("!")) { - continue; - } - Expr constInterp = model.getConstInterp(decl); - if (constInterp != null) { - bindings.add( - String.format("\n %s = %s", name, formatExpr(ctx, typeSystem, model, constInterp))); - } - } - - if (bindings.isEmpty()) { + if (inputs.isEmpty()) { return isCounterexample ? " (The expression fails unconditionally, regardless of input state)" : " (The expression is satisfiable unconditionally, regardless of input state)"; } - String prefix; + CelZ3CounterexampleGenerator generator = + new CelZ3CounterexampleGenerator(ctx, typeSystem, model); + StringBuilder sb = new StringBuilder(); if (isCounterexample) { - prefix = isApproximate ? " Potential counterexample input:" : " Counterexample input:"; + sb.append(isApproximate ? " Potential counterexample input:" : " Counterexample input:"); } else { - prefix = isApproximate ? " Potential satisfying input:" : " Satisfying input:"; + sb.append(isApproximate ? " Potential satisfying input:" : " Satisfying input:"); + } + for (Expr input : inputs) { + sb.append("\n ") + .append(input.getFuncDecl().getName()) + .append(" = ") + .append(generator.format(generator.evaluate(input))); } - return prefix + String.join("", bindings); + return sb.toString(); } - private static String formatExpr( - Context ctx, CelZ3TypeSystem typeSystem, Model model, @Nullable Expr expr) { - Preconditions.checkState(expr != null, "Z3 failed to evaluate the expression natively."); - + // Formats a model value as a CEL literal where one exists. + private String format(Expr expr) { FuncDecl decl = expr.getFuncDecl(); + Expr[] args = expr.getArgs(); - // Handle CelType constructors wrapper unwrapping if (decl.equals(typeSystem.intCons().ConstructorDecl())) { - return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]); - } else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) { - return formatTimestamp(expr.getArgs()[0]); - } else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) { - return formatDuration(expr.getArgs()[0]); + return ((IntNum) args[0]).getBigInteger().toString(); } else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) { - return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u"; + return ((IntNum) args[0]).getBigInteger() + "u"; } else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) { - return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]); + return args[0].toString(); + } else if (decl.equals(typeSystem.doubleCons().ConstructorDecl())) { + return formatDouble((FPNum) args[0]); } else if (decl.equals(typeSystem.stringCons().ConstructorDecl())) { - return expr.getArgs()[0].toString(); + return formatString(args[0], /* isBytes= */ false); } else if (decl.equals(typeSystem.bytesCons().ConstructorDecl())) { - return "b" + expr.getArgs()[0]; - } else if (decl.equals(typeSystem.doubleCons().ConstructorDecl())) { - Expr doubleArg = expr.getArgs()[0]; - if (doubleArg instanceof FPNum) { - FPNum fpNum = (FPNum) doubleArg; - if (fpNum.isNaN()) { - return "NaN"; - } - if (fpNum.isInf()) { - return fpNum.isNegative() ? "-Infinity" : "Infinity"; - } - if (fpNum.isZero()) { - return fpNum.isNegative() ? "-0.0" : "0.0"; - } - Expr realExpr = ctx.mkFPToReal(fpNum).simplify(); - if (realExpr instanceof RatNum) { - RatNum ratNum = (RatNum) realExpr; - double val = - ratNum.getBigIntNumerator().doubleValue() - / ratNum.getBigIntDenominator().doubleValue(); - return Double.toString(val); - } + return formatString(args[0], /* isBytes= */ true); + } else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) { + BigInteger nanos = ((IntNum) args[0]).getBigInteger(); + BigInteger nanoAdjustment = nanos.mod(NANOS_PER_SECOND); + BigInteger seconds = nanos.subtract(nanoAdjustment).divide(NANOS_PER_SECOND); + if (!isInRange( + seconds, ProtoTimeUtils.TIMESTAMP_SECONDS_MIN, ProtoTimeUtils.TIMESTAMP_SECONDS_MAX)) { + // No CEL timestamp is out of range, so no literal exists; show the seconds. + return "timestamp(" + seconds + ")"; } - return doubleArg.toString(); + return "timestamp(\"" + + Instant.ofEpochSecond(seconds.longValue(), nanoAdjustment.longValue()) + + "\")"; + } else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) { + BigInteger nanos = ((IntNum) args[0]).getBigInteger(); + return nanos.remainder(NANOS_PER_SECOND).signum() == 0 + ? "duration(\"" + nanos.divide(NANOS_PER_SECOND) + "s\")" + : "duration(\"" + nanos + "ns\")"; } else if (decl.equals(typeSystem.listCons().ConstructorDecl())) { - return reconstructList(ctx, typeSystem, model, expr.getArgs()[0]); + return formatList(args[0]); } else if (decl.equals(typeSystem.mapCons().ConstructorDecl())) { - return reconstructMap(ctx, typeSystem, model, expr.getArgs()[0]); + return formatMap(args[0]); } else if (decl.equals(typeSystem.messageCons().ConstructorDecl())) { - return reconstructMessage(ctx, typeSystem, model, expr.getArgs()[0]); + return formatMessage(args[0]); } else if (decl.equals(typeSystem.errorCons().ConstructorDecl())) { return "Error"; } else if (decl.equals(typeSystem.unknownCons().ConstructorDecl())) { return "Unknown"; } else if (decl.equals(typeSystem.nullCons().ConstructorDecl())) { return "null"; - } else if (decl.equals(typeSystem.optionalCons().ConstructorDecl())) { - Expr optRef = expr.getArgs()[0]; - Expr hasValueExpr = - evaluateStrict( - model, - typeSystem.optHasValue(optRef), - String.format("Z3 failed to evaluate optHasValue natively for %s", optRef)); - if (hasValueExpr.isTrue()) { - Expr valueExpr = - evaluateStrict( - model, - typeSystem.getOptionalValue(optRef), - String.format("Z3 failed to evaluate optValue natively for %s", optRef)); - return "optional(" + formatExpr(ctx, typeSystem, model, valueExpr) + ")"; - } else if (hasValueExpr.isFalse()) { - return "optional.none()"; - } } - return expr.toString(); + // Optional is the only remaining constructor. + if (!evaluate(typeSystem.optHasValue(args[0])).isTrue()) { + return "optional.none()"; + } + return "optional.of(" + format(evaluate(typeSystem.getOptionalValue(args[0]))) + ")"; + } + + private static boolean isInRange(BigInteger val, long min, long max) { + return val.compareTo(BigInteger.valueOf(min)) >= 0 + && val.compareTo(BigInteger.valueOf(max)) <= 0; } - private static String formatTimestamp(Expr nanosExpr) { - BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger(); - BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND); - BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond); - BigInteger seconds = divRem[0]; - BigInteger nanos = divRem[1]; - if (nanos.signum() < 0) { - seconds = seconds.subtract(BigInteger.ONE); - nanos = nanos.add(nanosPerSecond); + private String formatDouble(FPNum fpNum) { + if (fpNum.isNaN()) { + return "double(\"NaN\")"; } - if (nanos.equals(BigInteger.ZERO)) { - return "timestamp(" + seconds + ")"; + // Z3 doubles are IEEE 754 binary64, so their bits convert exactly. + double value = + Double.longBitsToDouble( + ((BitVecNum) ctx.mkFPToIEEEBV(fpNum).simplify()).getBigInteger().longValue()); + return Double.isInfinite(value) ? "double(\"" + value + "\")" : Double.toString(value); + } + + private static String formatString(Expr arg, boolean isBytes) { + return quote(decodeZ3String(arg.getString()), isBytes); + } + + // Z3 escapes characters outside printable ASCII, and a backslash before 'u', as \\u{hex}. + private static int[] decodeZ3String(String encoded) { + IntStream.Builder codePoints = IntStream.builder(); + for (int i = 0; i < encoded.length(); ) { + if (encoded.startsWith("\\u{", i)) { + int end = encoded.indexOf('}', i); + codePoints.add(Integer.parseInt(encoded.substring(i + 3, end), 16)); + i = end + 1; + } else { + codePoints.add(encoded.charAt(i++)); + } } - return "google.protobuf.Timestamp{seconds: " + seconds + ", nanos: " + nanos + "}"; + return codePoints.build().toArray(); } - private static String formatDuration(Expr nanosExpr) { - BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger(); - BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND); - BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond); - if (divRem[1].equals(BigInteger.ZERO)) { - return "duration('" + divRem[0] + "s')"; + // Takes code points rather than a String, which would merge adjacent surrogates. + private static String quote(int[] codePoints, boolean isBytes) { + StringBuilder sb = new StringBuilder(isBytes ? "b\"" : "\""); + for (int codePoint : codePoints) { + if (codePoint == '"' || codePoint == '\\') { + sb.append('\\').appendCodePoint(codePoint); + } else if (isBytes && (codePoint < 0x20 || codePoint >= 0x7f)) { + // Bytes literals don't accept Unicode escapes, so write the character's UTF-8 bytes. + for (byte b : new String(Character.toChars(codePoint)).getBytes(UTF_8)) { + sb.append(String.format("\\x%02x", b & 0xff)); + } + } else if (Character.isISOControl(codePoint) + || Character.getType(codePoint) == Character.SURROGATE) { + // CEL rejects lone surrogates even when escaped, so those are shown, not evaluable. + sb.append(String.format("\\u%04x", codePoint)); + } else { + sb.appendCodePoint(codePoint); + } } - return "duration('" + totalNanos + "ns')"; + return sb.append('"').toString(); } - private static String reconstructList( - Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr listRef) { - Expr lenExpr = - evaluateStrict( - model, - ctx.mkLength(typeSystem.getSeq(listRef)), - String.format("Z3 failed to evaluate length for list %s", listRef)); - Preconditions.checkState( - lenExpr instanceof IntNum, "Expected IntNum length for list %s, got %s", listRef, lenExpr); - long length = ((IntNum) lenExpr).getInt64(); - int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT); + private String formatList(Expr listRef) { + long length = evaluateLength(ctx.mkLength(typeSystem.getSeq(listRef))); List elements = new ArrayList<>(); - for (int i = 0; i < printLimit; i++) { - Expr elem = - evaluateStrict( - model, - 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)); - } - if (length > printLimit) { - elements.add("... (" + (length - printLimit) + " more elements)"); + for (long i = 0; i < Math.min(length, MAX_ELEMENTS_TO_PRINT); i++) { + elements.add(format(evaluate(ctx.mkNth(typeSystem.getSeq(listRef), ctx.mkInt(i))))); } - - return "[" + String.join(", ", elements) + "]"; + return join("[", elements, length, "elements", "]"); } - private static String reconstructMap( - Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr mapRef) { - Expr lenExpr = - evaluateStrict( - model, - ctx.mkLength(typeSystem.getMapKeys(mapRef)), - String.format("Z3 failed to evaluate length for map %s", mapRef)); - Preconditions.checkState( - lenExpr instanceof IntNum, "Expected IntNum length for map %s, got %s", mapRef, lenExpr); - - long length = ((IntNum) lenExpr).getInt64(); - int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT); + private String formatMap(Expr mapRef) { + long length = evaluateLength(ctx.mkLength(typeSystem.getMapKeys(mapRef))); List entries = new ArrayList<>(); Set> seenKeys = new HashSet<>(); - for (int i = 0; i < printLimit; i++) { - Expr key = - evaluateStrict( - model, - ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i)), - String.format("Z3 failed to evaluate map key at index %d for map %s", i, mapRef)); - if (!seenKeys.add(key)) { + for (long i = 0; i < Math.min(length, MAX_ELEMENTS_TO_PRINT); i++) { + Expr key = evaluate(ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i))); + if (!seenKeys.add(key) + || !evaluate(ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), key)).isTrue()) { continue; } - Expr presence = - evaluateStrict( - model, - ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), key), - String.format( - "Z3 failed to evaluate map presence for key %s in map %s", key, mapRef)); - if (presence.isTrue()) { - Expr value = - evaluateStrict( - model, - 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, value)); - } - } - if (length > printLimit) { - entries.add("... (" + (length - printLimit) + " more entries)"); + Expr value = evaluate(ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), key)); + entries.add(format(key) + ": " + format(value)); } - - return "{" + String.join(", ", entries) + "}"; + return join("{", entries, length, "entries", "}"); } - private static String reconstructMessage( - Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr msgRef) { - Expr presenceArray = - evaluateStrict( - model, - typeSystem.getMsgPresence(msgRef), - String.format("Z3 failed to evaluate presence array natively for msg %s", msgRef)); - - Expr typeNameExpr = - evaluateStrict( - model, - typeSystem.getMsgTypeName(msgRef), - String.format("Z3 failed to evaluate type name natively for msg %s", msgRef)); + private static String join( + String prefix, List displayed, long length, String noun, String suffix) { + if (length > MAX_ELEMENTS_TO_PRINT) { + displayed.add("... (" + (length - MAX_ELEMENTS_TO_PRINT) + " more " + noun + ")"); + } + return prefix + String.join(", ", displayed) + suffix; + } - String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", ""); + private String formatMessage(Expr msgRef) { + Expr presenceArray = evaluate(typeSystem.getMsgPresence(msgRef)); + String typeName = evaluate(typeSystem.getMsgTypeName(msgRef)).getString(); Set> keys = new LinkedHashSet<>(); extractKeys(presenceArray, keys); List entries = new ArrayList<>(); for (Expr key : keys) { - Expr presence = - evaluateStrict( - model, - ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), key), - String.format( - "Z3 failed to evaluate msg presence for key %s in msg %s", key, msgRef)); - - if (presence.isTrue()) { - Expr value = - evaluateStrict( - model, - 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)); + if (evaluate(ctx.mkSelect((ArrayExpr) typeSystem.getMsgPresence(msgRef), key)).isTrue()) { + Expr value = evaluate(ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), key)); + entries.add(key.getString() + ": " + format(value)); } } @@ -314,8 +253,6 @@ private static void extractKeys(Expr arrayExpr, Set> keys) { if (declName.equals("store")) { Expr[] args = arrayExpr.getArgs(); - Preconditions.checkState( - args.length == 3, "Z3 store array operation must have exactly 3 arguments"); keys.add(args[1]); arrayExpr = args[0]; continue; @@ -324,13 +261,18 @@ private static void extractKeys(Expr arrayExpr, Set> keys) { } } - private static Expr evaluateStrict(Model model, Expr expr, String errorMessage) { - // There are no free variables remaining after the solver is ran, so the completion flag has - // no effect. - Expr evaluated = model.evaluate(expr, /* completion= */ true); - if (evaluated == null) { - throw new IllegalStateException(errorMessage); - } - return evaluated; + private long evaluateLength(Expr lengthExpr) { + return ((IntNum) evaluate(lengthExpr)).getInt64(); + } + + private Expr evaluate(Expr expr) { + // Model completion assigns a value to any input the model leaves unconstrained. + return model.evaluate(expr, /* completion= */ true); + } + + private CelZ3CounterexampleGenerator(Context ctx, CelZ3TypeSystem typeSystem, Model model) { + this.ctx = ctx; + this.typeSystem = typeSystem; + this.model = model; } } diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java index 4024e1ff5..70193017a 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TranslationContext.java @@ -22,6 +22,7 @@ import java.util.ArrayList; import java.util.Collections; import java.util.HashMap; +import java.util.LinkedHashMap; import java.util.LinkedHashSet; import java.util.List; import java.util.Map; @@ -76,6 +77,11 @@ void addInputVariable(Expr variable, CelType declaredType) { inputVariableTypes.put(variable, declaredType); } + /** Returns the input variables, in order of first appearance. */ + Set> inputVariables() { + return Collections.unmodifiableSet(inputVariableTypes.keySet()); + } + /** Returns the declared type of an input variable, or dyn for any other value. */ CelType guaranteedType(Expr value) { return inputVariableTypes.getOrDefault(value, SimpleType.DYN); @@ -135,7 +141,7 @@ T withScope(String varName, TranslatedValue value, Supplier action) { new CelZ3TypeConstraintGenerator(ctx, typeSystem, comprehensionUnrollLimit); this.comprehensionUnrollLimit = comprehensionUnrollLimit; this.constraints = new LinkedHashSet<>(); - this.inputVariableTypes = new HashMap<>(); + this.inputVariableTypes = new LinkedHashMap<>(); this.truncationConditions = new ArrayList<>(); this.symbolTable = new HashMap<>(); } diff --git a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java index 41af9ae8c..87db12f78 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java @@ -553,11 +553,11 @@ public void verifyInvariants_workloadAdmissionFlawed_violationsDetected() throws .isEqualTo( "Invariant 'universal_no_unapproved_privileged_prod' violation detected." + " Counterexample input:\n" + + " is_admin = true\n" + " is_owner = false\n" + " is_privileged = true\n" + " is_prod = true\n" - + " has_approval = false\n" - + " is_admin = true"); + + " has_approval = false"); } @Test diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index f8c747452..dd5254631 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -196,13 +196,22 @@ private enum IsSatisfiableTestCase { "size(int_list) == 6 && dyn(b ? [1] : int_list) == [1]", "b = true"), TIMESTAMP_SUBSECOND_SATISFIABLE( "ts == google.protobuf.Timestamp{seconds: 10, nanos: 500}", - "ts = google\\.protobuf\\.Timestamp\\{seconds: 10, nanos: 500\\}"), + "ts = timestamp\\(\"1970-01-01T00:00:10\\.000000500Z\"\\)"), TIMESTAMP_NEGATIVE_SUBSECOND_SATISFIABLE( "ts == google.protobuf.Timestamp{seconds: -1, nanos: 500}", - "ts = google\\.protobuf\\.Timestamp\\{seconds: -1, nanos: 500\\}"), + "ts = timestamp\\(\"1969-12-31T23:59:59\\.000000500Z\"\\)"), DURATION_SUBSECOND_SATISFIABLE( "dur == google.protobuf.Duration{seconds: 1, nanos: 500}", - "dur = duration\\('1000000500ns'\\)"), + "dur = duration\\(\"1000000500ns\"\\)"), + // Timestamps nested in dyn aren't range constrained, and RFC 3339 can't express these. + TIMESTAMP_ABOVE_RANGE_SATISFIABLE( + "type(dyn_var) == google.protobuf.Timestamp" + + " && dyn_var > google.protobuf.Timestamp{seconds: 253402300799, nanos: 999999999}", + "dyn_var = timestamp\\(\\d+\\)"), + TIMESTAMP_BELOW_RANGE_SATISFIABLE( + "type(dyn_var) == google.protobuf.Timestamp" + + " && dyn_var < google.protobuf.Timestamp{seconds: -62135596800}", + "dyn_var = timestamp\\(-\\d+\\)"), ; private final String expr; @@ -239,6 +248,87 @@ public void isSatisfiable_withVariable_returnsSatisfyingModel() throws Exception assertThat(result.message()).containsMatch("x = (?:[6-9]|[1-9]\\d+)"); } + private enum WitnessTestCase { + INT_MIN("x == -9223372036854775808", "x", "-9223372036854775808"), + INT_MAX("x == 9223372036854775807", "x", "9223372036854775807"), + UINT_MAX("u == 18446744073709551615u", "u", "18446744073709551615u"), + SUBNORMAL_DOUBLE("d == 4.9e-324", "d", "4.9E-324"), + POSITIVE_INFINITY("d > 1.7976931348623157e308", "d", "double(\"Infinity\")"), + NEGATIVE_INFINITY("d < -1.7976931348623157e308", "d", "double(\"-Infinity\")"), + BOOL("a", "a", "true"), + UNICODE_STRING("string_var == 'é'", "string_var", "\"é\""), + ESCAPED_STRING("string_var == '\"\\\\\\n\\x01'", "string_var", "\"\\\"\\\\\\u000a\\u0001\""), + ESCAPED_BYTES("by == b'a\\x01\"'", "by", "b\"a\\x01\\\"\""), + DEL_BYTES("by == b'\\x7f'", "by", "b\"\\x7f\""), + C1_CONTROL_STRING("string_var == '\\u0085'", "string_var", "\"\\u0085\""), + MIN_TIMESTAMP("ts == timestamp(-62135596800)", "ts", "timestamp(\"0001-01-01T00:00:00Z\")"), + MAX_TIMESTAMP( + "ts == google.protobuf.Timestamp{seconds: 253402300799, nanos: 999999999}", + "ts", + "timestamp(\"9999-12-31T23:59:59.999999999Z\")"), + SUBSECOND_TIMESTAMP( + "ts == google.protobuf.Timestamp{seconds: -1, nanos: 500}", + "ts", + "timestamp(\"1969-12-31T23:59:59.000000500Z\")"), + DURATION("timestamp(100) - timestamp(50) == dur", "dur", "duration(\"50s\")"), + SUBSECOND_DURATION( + "dur == google.protobuf.Duration{seconds: -1, nanos: -500}", + "dur", + "duration(\"-1000000500ns\")"), + NULL("dyn_var == null", "dyn_var", "null"), + EMPTY_LIST("int_list == []", "int_list", "[]"), + LIST_WITH_NULL("dyn_list == [true, null]", "dyn_list", "[true, null]"), + MAP("string_int_map == {'a': 1}", "string_int_map", "{\"a\": 1}"), + OPTIONAL("opt_var == optional.of(1)", "opt_var", "optional.of(1)"), + OPTIONAL_NONE("opt_var == optional.none()", "opt_var", "optional.none()"); + + private final String expr; + private final String variableName; + private final String expectedDisplayValue; + + WitnessTestCase(String expr, String variableName, String expectedDisplayValue) { + this.expr = expr; + this.variableName = variableName; + this.expectedDisplayValue = expectedDisplayValue; + } + } + + @Test + public void isSatisfiable_witnessDisplayedAsCelLiteral(@TestParameter WitnessTestCase testCase) + throws Exception { + CelAbstractSyntaxTree ast = CEL.compile(testCase.expr).getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.message().split("\n")) + .asList() + .contains(" " + testCase.variableName + " = " + testCase.expectedDisplayValue); + } + + @Test + public void isSatisfiable_listAtDisplayLimit_displaysAllElements() throws Exception { + CelAbstractSyntaxTree ast = + CEL.compile("int_list == [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.message()) + .endsWith("int_list = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]"); + } + + @Test + public void isSatisfiable_listPastDisplayLimit_elidesRemainingElements() throws Exception { + CelAbstractSyntaxTree ast = + CEL.compile("int_list == [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16]").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.message()) + .endsWith( + "int_list = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, ... (1 more" + + " elements)]"); + } + @Test public void isSatisfiable_mapNoContainerError_returnsSatisfyingModel() throws Exception { CelAbstractSyntaxTree ast = CEL.compile("string_int_map.size() == 1").getAst(); @@ -1461,12 +1551,12 @@ private enum IsAlwaysTrueViolationTestCase { "dur != dur", "Condition is not always true\\.", "Counterexample input:", - "dur = duration\\('-?\\d+s'\\)"), + "dur = duration\\(\"-?\\d+s\"\\)"), TIMESTAMP_VARIABLE_COUNTEREXAMPLE( "ts != ts", "Condition is not always true\\.", "Counterexample input:", - "ts = timestamp\\(-?\\d+\\)"), + "ts = timestamp\\(\"[^\"]+\"\\)"), UNINTERPRETED_CONVERSION_NULL_FAILS_WITH_ERRORS( "string(null) == string(null)", "Condition is not always true\\."), LAW_OF_EXCLUDED_MIDDLE_FAILS_WITH_ERRORS( @@ -1506,7 +1596,7 @@ private enum IsAlwaysTrueViolationTestCase { "opt_dyn_var.hasValue() ? type(opt_dyn_var.value()) == int : true", "Condition is not always true\\.", "Counterexample input:", - "opt_dyn_var = optional\\(Unknown\\)"), + "opt_dyn_var = optional\\.of\\(Unknown\\)"), OPTIONAL_ENTRY_DYN_VAR_TYPE_MISMATCH( "[?dyn_var] == [?dyn_var] ? true : true", "Condition is not always true\\.", @@ -1630,7 +1720,7 @@ private enum IsAlwaysTrueViolationTestCase { "request == request", "Condition is not always true\\.", "Counterexample input:", - "request = NaN"), + "request = double\\(\"NaN\"\\)"), CROSS_TYPE_NUMERIC_EQUALITY_APPROXIMATION_VIOLATION( "dyn_var == 1.0", "Condition is not always true\\.", @@ -2605,9 +2695,9 @@ private enum CounterexampleFormatTestCase { "role == \"user\"", ImmutableList.of("role = \"admin\"", "role = \"user\"")), DOUBLE("d == 1.5", "d == 2.5", ImmutableList.of("d = 1\\.5", "d = 2\\.5")), - DOUBLE_NAN("d != d", "false", ImmutableList.of("d = NaN")), - DOUBLE_INF("d == (1.0 / 0.0)", "false", ImmutableList.of("d = Infinity")), - DOUBLE_NEG_INF("d == (-1.0 / 0.0)", "false", ImmutableList.of("d = -Infinity")), + DOUBLE_NAN("d != d", "false", ImmutableList.of("d = double\\(\"NaN\"\\)")), + DOUBLE_INF("d == (1.0 / 0.0)", "false", ImmutableList.of("d = double\\(\"Infinity\"\\)")), + DOUBLE_NEG_INF("d == (-1.0 / 0.0)", "false", ImmutableList.of("d = double\\(\"-Infinity\"\\)")), DOUBLE_NEG_ZERO("d == 0.0 && 1.0 / d == (-1.0 / 0.0)", "false", ImmutableList.of("d = -0\\.0")), DOUBLE_POS_ZERO("d == 0.0 && 1.0 / d == (1.0 / 0.0)", "false", ImmutableList.of("d = 0\\.0")), UINT("u == 443u", "u == 80u", ImmutableList.of("u = 443u", "u = 80u")), diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java index 31e7ec5b8..31432ba3f 100644 --- a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java @@ -231,7 +231,7 @@ public void repl_durationSatisfyingInputFormat() throws Exception { runReplWithCommands(":var dur duration", "timestamp(100) - timestamp(50) == dur", ":quit"); assertThat(output[0]).contains("[VERIFIED]"); - assertThat(output[0]).contains("dur = duration('50s')"); + assertThat(output[0]).contains("dur = duration(\"50s\")"); assertThat(output[1]).isEmpty(); }