diff --git a/verifier/README.md b/verifier/README.md index 5d5a111f5..7d9d7f899 100644 --- a/verifier/README.md +++ b/verifier/README.md @@ -241,7 +241,8 @@ public class PolicyVerifierExample { When checking whether an expression is satisfiable using `isSatisfiable`, the verifier returns `VERIFIED` if there exists at least one input combination where the expression evaluates to `true`. Furthermore, `result.message()` -provides concrete satisfying model assignments (witness/test case generation). +provides concrete satisfying model assignments (witness/test case generation), +and `result.witness()` exposes them as CEL runtime values. ```java import dev.cel.common.CelAbstractSyntaxTree; diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index a5362e4f7..2d2549456 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel @@ -15,6 +15,7 @@ java_library( "CelVerificationResult.java", "CelVerifier.java", "CelVerifierBuilder.java", + "CelWitness.java", ], tags = [ ], @@ -23,6 +24,7 @@ java_library( "//common:cel_ast", "//common/types:type_providers", "@maven//:com_google_errorprone_error_prone_annotations", + "@maven//:com_google_guava_guava", ], ) @@ -191,6 +193,8 @@ java_library( "//common/types", "//common/types:cel_types", "//common/types:type_providers", + "//common/values", + "//common/values:cel_byte_string", "//optimizer", "//optimizer:optimization_exception", "//optimizer:optimizer_builder", diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java b/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java index 5a4c7ada6..f4c4a8123 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerificationResult.java @@ -15,6 +15,8 @@ package dev.cel.verifier; import com.google.auto.value.AutoValue; +import java.util.Map; +import java.util.Optional; /** Result object containing the outcome of a CEL AST verification check. */ @AutoValue @@ -43,6 +45,12 @@ public enum VerificationStatus { */ public abstract String counterexample(); + /** + * Returns the counterexample or satisfying input found by the solver, if any. Its variables are + * empty when the outcome doesn't depend on any input. + */ + public abstract Optional witness(); + /** * Returns a message detailing the outcome of the verification check, such as a counterexample * input, satisfying model assignments, or truncation reason. May be empty if status is VERIFIED @@ -53,28 +61,65 @@ public String message() { } static CelVerificationResult verified() { - return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", ""); + return create(VerificationStatus.VERIFIED, ""); } - static CelVerificationResult verified(String reason) { - return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, ""); + static CelVerificationResult verified(String reason, CelWitness satisfyingInput) { + return create( + VerificationStatus.VERIFIED, reason, satisfyingInput, /* isCounterexample= */ false); } static CelVerificationResult failed(String reason) { - return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, ""); + return create(VerificationStatus.VIOLATED, reason); } - static CelVerificationResult failed(String reason, String counterexample) { - return new AutoValue_CelVerificationResult( - VerificationStatus.VIOLATED, reason, counterexample); + static CelVerificationResult failed(String reason, CelWitness counterexample) { + return create( + VerificationStatus.VIOLATED, reason, counterexample, /* isCounterexample= */ true); } static CelVerificationResult inconclusive(String reason) { - return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, ""); + return create(VerificationStatus.INCONCLUSIVE, reason); + } + + static CelVerificationResult inconclusive( + String reason, CelWitness witness, boolean isCounterexample) { + return create(VerificationStatus.INCONCLUSIVE, reason, witness, isCounterexample); } - static CelVerificationResult inconclusive(String reason, String counterexample) { + private static CelVerificationResult create(VerificationStatus status, String reason) { + return new AutoValue_CelVerificationResult(status, reason, "", Optional.empty()); + } + + private static CelVerificationResult create( + VerificationStatus status, String reason, CelWitness witness, boolean isCounterexample) { return new AutoValue_CelVerificationResult( - VerificationStatus.INCONCLUSIVE, reason, counterexample); + status, + reason, + describe(witness, status == VerificationStatus.INCONCLUSIVE, isCounterexample), + Optional.of(witness)); + } + + private static String describe( + CelWitness witness, boolean isApproximate, boolean isCounterexample) { + if (witness.variables().isEmpty()) { + return isCounterexample + ? " (The expression fails unconditionally, regardless of input state)" + : " (The expression is satisfiable unconditionally, regardless of input state)"; + } + + StringBuilder sb = new StringBuilder(); + if (isCounterexample) { + sb.append(isApproximate ? " Potential counterexample input:" : " Counterexample input:"); + } else { + sb.append(isApproximate ? " Potential satisfying input:" : " Satisfying input:"); + } + for (Map.Entry variable : witness.variables().entrySet()) { + sb.append("\n ") + .append(variable.getKey()) + .append(" = ") + .append(variable.getValue().displayValue()); + } + return sb.toString(); } } diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index 1e791994f..131b3c24c 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -256,23 +256,13 @@ public CelVerificationResult verifyEquivalence( switch (result.outcome) { case EXACT_MATCH: return CelVerificationResult.failed( - "Equivalence violation detected.", - getCounterexampleString( - ctx, - translator, - result.model, - /* isApproximate= */ false, - /* isCounterexample= */ true)); + "Equivalence violation detected.", extractWitness(ctx, translator, result.model)); case APPROXIMATE_MATCH: return CelVerificationResult.inconclusive( "Inconclusive: a divergence may exist, but it depends on approximations, missing" + " theories, or loop bounds.", - getCounterexampleString( - ctx, - translator, - result.model, - /* isApproximate= */ true, - /* isCounterexample= */ true)); + extractWitness(ctx, translator, result.model), + /* isCounterexample= */ true); case TRUNCATED: return CelVerificationResult.inconclusive( "Inconclusive: expressions are equivalent within the current loop unroll limit, but" @@ -343,22 +333,13 @@ CelVerificationResult verifyImplication( case EXACT_MATCH: return CelVerificationResult.failed( String.format("%s violation detected.", subjectName), - getCounterexampleString( - ctx, - translator, - result.model, - /* isApproximate= */ false, - /* isCounterexample= */ true)); + extractWitness(ctx, translator, result.model)); case APPROXIMATE_MATCH: return CelVerificationResult.inconclusive( "Inconclusive: a counterexample may exist, but it depends on approximations, missing" + " theories, or loop bounds.", - getCounterexampleString( - ctx, - translator, - result.model, - /* isApproximate= */ true, - /* isCounterexample= */ true)); + extractWitness(ctx, translator, result.model), + /* isCounterexample= */ true); case TRUNCATED: return CelVerificationResult.inconclusive( String.format( @@ -403,23 +384,10 @@ private CelVerificationResult checkSatisfiability( switch (result.outcome) { case EXACT_MATCH: + CelWitness witness = extractWitness(ctx, translator, result.model); return searchForCounterexample - ? CelVerificationResult.failed( - "Condition is not always true.", - getCounterexampleString( - ctx, - translator, - result.model, - /* isApproximate= */ false, - /* isCounterexample= */ true)) - : CelVerificationResult.verified( - "Condition is satisfiable." - + getCounterexampleString( - ctx, - translator, - result.model, - /* isApproximate= */ false, - /* isCounterexample= */ false)); + ? CelVerificationResult.failed("Condition is not always true.", witness) + : CelVerificationResult.verified("Condition is satisfiable.", witness); case APPROXIMATE_MATCH: String prefix = @@ -430,12 +398,8 @@ private CelVerificationResult checkSatisfiability( + " approximations, missing theories, or loop bounds."; return CelVerificationResult.inconclusive( prefix, - getCounterexampleString( - ctx, - translator, - result.model, - /* isApproximate= */ true, - /* isCounterexample= */ searchForCounterexample)); + extractWitness(ctx, translator, result.model), + /* isCounterexample= */ searchForCounterexample); case TRUNCATED: return CelVerificationResult.inconclusive( @@ -538,19 +502,13 @@ private CelAstToZ3Translator newTranslator(Context ctx, boolean parameterizeUnkn parameterizeUnknowns); } - private static String getCounterexampleString( - Context ctx, - CelAstToZ3Translator translator, - Model model, - boolean isApproximate, - boolean isCounterexample) { + private CelWitness extractWitness(Context ctx, CelAstToZ3Translator translator, Model model) { return CelZ3CounterexampleGenerator.generate( ctx, translator.getTypeSystem(), model, - translator.getInputVariables(), - isApproximate, - isCounterexample); + comprehensionUnrollLimit, + translator.getInputVariables()); } private enum SolverOutcome { diff --git a/verifier/src/main/java/dev/cel/verifier/CelWitness.java b/verifier/src/main/java/dev/cel/verifier/CelWitness.java new file mode 100644 index 000000000..6dcc2eef6 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CelWitness.java @@ -0,0 +1,52 @@ +// Copyright 2026 Google LLC +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// https://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +package dev.cel.verifier; + +import com.google.auto.value.AutoValue; +import com.google.common.collect.ImmutableMap; +import java.util.Optional; + +/** An input assignment found by the solver: a counterexample or a satisfying input. */ +@AutoValue +public abstract class CelWitness { + + /** The value the solver assigned to one input variable. */ + @AutoValue + public abstract static class Variable { + + /** + * Returns the value in its CEL runtime representation ({@code Long}, {@code UnsignedLong}, + * {@code Double}, {@code Boolean}, {@code String}, {@code CelByteString}, {@code Instant}, + * {@code Duration}, {@code NullValue}, {@code ImmutableList}, {@code ImmutableMap} or {@code + * Optional}, nested accordingly), or empty if it has no exact runtime equivalent (e.g. an + * unknown). + */ + public abstract Optional value(); + + // The value as a CEL literal where one exists, for display. + abstract String displayValue(); + + static Variable create(Optional value, String displayValue) { + return new AutoValue_CelWitness_Variable(value, displayValue); + } + } + + /** Returns the variables keyed by name, in order of first appearance. */ + public abstract ImmutableMap variables(); + + static CelWitness create(ImmutableMap variables) { + return new AutoValue_CelWitness(variables); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index 571a005e5..675432d79 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -16,6 +16,9 @@ import static java.nio.charset.StandardCharsets.UTF_8; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import com.google.common.primitives.UnsignedLong; import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BitVecNum; import com.microsoft.z3.Context; @@ -25,16 +28,21 @@ import com.microsoft.z3.IntNum; import com.microsoft.z3.Model; import dev.cel.common.internal.ProtoTimeUtils; +import dev.cel.common.values.CelByteString; +import dev.cel.common.values.NullValue; import java.math.BigInteger; +import java.time.Duration; import java.time.Instant; import java.util.ArrayList; +import java.util.Arrays; import java.util.HashSet; import java.util.LinkedHashSet; import java.util.List; +import java.util.Optional; import java.util.Set; import java.util.stream.IntStream; -/** Generates human-readable counterexample strings from Z3 models. */ +/** Extracts {@link CelWitness}es from Z3 models. */ @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types. final class CelZ3CounterexampleGenerator { @@ -45,65 +53,79 @@ final class CelZ3CounterexampleGenerator { private final Context ctx; private final CelZ3TypeSystem typeSystem; private final Model model; + private final int comprehensionUnrollLimit; private final Set> valuesOnPath; - static String generate( + static CelWitness generate( Context ctx, CelZ3TypeSystem typeSystem, Model model, - Set> inputs, - boolean isApproximate, - boolean isCounterexample) { - if (inputs.isEmpty()) { - return isCounterexample - ? " (The expression fails unconditionally, regardless of input state)" - : " (The expression is satisfiable unconditionally, regardless of input state)"; + int comprehensionUnrollLimit, + Set> inputs) { + CelZ3CounterexampleGenerator generator = + new CelZ3CounterexampleGenerator(ctx, typeSystem, model, comprehensionUnrollLimit); + ImmutableMap.Builder variables = ImmutableMap.builder(); + for (Expr input : inputs) { + Value value = generator.extract(generator.evaluate(input)); + variables.put( + input.getFuncDecl().getName().toString(), + CelWitness.Variable.create(value.runtimeValue, value.display)); } + return CelWitness.create(variables.buildOrThrow()); + } - CelZ3CounterexampleGenerator generator = - new CelZ3CounterexampleGenerator(ctx, typeSystem, model); - StringBuilder sb = new StringBuilder(); - if (isCounterexample) { - sb.append(isApproximate ? " Potential counterexample input:" : " Counterexample input:"); - } else { - sb.append(isApproximate ? " Potential satisfying input:" : " Satisfying input:"); + // A model value's CEL runtime representation, if it has an exact one, and its display. + private static final class Value { + private final Optional runtimeValue; + private final String display; + + private static Value exact(Object runtimeValue, String display) { + return new Value(Optional.of(runtimeValue), display); } - for (Expr input : inputs) { - sb.append("\n ") - .append(input.getFuncDecl().getName()) - .append(" = ") - .append(generator.format(generator.evaluate(input))); + + private static Value inexact(String display) { + return new Value(Optional.empty(), display); + } + + private Value(Optional runtimeValue, String display) { + this.runtimeValue = runtimeValue; + this.display = display; } - return sb.toString(); } - // Formats a model value as a CEL literal where one exists. - private String format(Expr expr) { + private Value extract(Expr expr) { // Refs are uninterpreted, so Z3 may return a cyclic model (e.g. a map containing itself). if (!valuesOnPath.add(expr)) { - return ""; + return Value.inexact(""); } - String formatted = formatValue(expr); + Value value = extractValue(expr); valuesOnPath.remove(expr); - return formatted; + return value; } - private String formatValue(Expr expr) { + private Value extractValue(Expr expr) { FuncDecl decl = expr.getFuncDecl(); Expr[] args = expr.getArgs(); if (decl.equals(typeSystem.intCons().ConstructorDecl())) { - return ((IntNum) args[0]).getBigInteger().toString(); + BigInteger val = ((IntNum) args[0]).getBigInteger(); + return isInRange(val, Long.MIN_VALUE, Long.MAX_VALUE) + ? Value.exact(val.longValue(), val.toString()) + : Value.inexact(val.toString()); } else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) { - return ((IntNum) args[0]).getBigInteger() + "u"; + BigInteger val = ((IntNum) args[0]).getBigInteger(); + String display = val + "u"; + return val.signum() >= 0 && val.bitLength() <= 64 + ? Value.exact(UnsignedLong.valueOf(val), display) + : Value.inexact(display); } else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) { - return args[0].toString(); + return Value.exact(args[0].isTrue(), args[0].toString()); } else if (decl.equals(typeSystem.doubleCons().ConstructorDecl())) { - return formatDouble((FPNum) args[0]); + return extractDouble((FPNum) args[0]); } else if (decl.equals(typeSystem.stringCons().ConstructorDecl())) { - return formatString(args[0], /* isBytes= */ false); + return extractString(args[0], /* isBytes= */ false); } else if (decl.equals(typeSystem.bytesCons().ConstructorDecl())) { - return formatString(args[0], /* isBytes= */ true); + return extractString(args[0], /* isBytes= */ true); } else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) { BigInteger nanos = ((IntNum) args[0]).getBigInteger(); BigInteger nanoAdjustment = nanos.mod(NANOS_PER_SECOND); @@ -111,35 +133,40 @@ private String formatValue(Expr expr) { 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 Value.inexact("timestamp(" + seconds + ")"); } - return "timestamp(\"" - + Instant.ofEpochSecond(seconds.longValue(), nanoAdjustment.longValue()) - + "\")"; + Instant instant = Instant.ofEpochSecond(seconds.longValue(), nanoAdjustment.longValue()); + return Value.exact(instant, "timestamp(\"" + instant + "\")"); } 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\")"; + String display = + nanos.remainder(NANOS_PER_SECOND).signum() == 0 + ? "duration(\"" + nanos.divide(NANOS_PER_SECOND) + "s\")" + : "duration(\"" + nanos + "ns\")"; + return isInRange(nanos, Long.MIN_VALUE, Long.MAX_VALUE) + ? Value.exact(Duration.ofNanos(nanos.longValue()), display) + : Value.inexact(display); } else if (decl.equals(typeSystem.listCons().ConstructorDecl())) { - return formatList(args[0]); + return extractList(args[0]); } else if (decl.equals(typeSystem.mapCons().ConstructorDecl())) { - return formatMap(args[0]); + return extractMap(args[0]); } else if (decl.equals(typeSystem.messageCons().ConstructorDecl())) { - return formatMessage(args[0]); + return extractMessage(args[0]); } else if (decl.equals(typeSystem.errorCons().ConstructorDecl())) { - return "Error"; + return Value.inexact("Error"); } else if (decl.equals(typeSystem.unknownCons().ConstructorDecl())) { - return "Unknown"; + return Value.inexact("Unknown"); } else if (decl.equals(typeSystem.nullCons().ConstructorDecl())) { - return "null"; + return Value.exact(NullValue.NULL_VALUE, "null"); } // Optional is the only remaining constructor. if (!evaluate(typeSystem.optHasValue(args[0])).isTrue()) { - return "optional.none()"; + return Value.exact(Optional.empty(), "optional.none()"); } - return "optional.of(" + format(evaluate(typeSystem.getOptionalValue(args[0]))) + ")"; + Value value = extract(evaluate(typeSystem.getOptionalValue(args[0]))); + return new Value( + value.runtimeValue.map(Optional::of), "optional.of(" + value.display + ")"); } private static boolean isInRange(BigInteger val, long min, long max) { @@ -147,19 +174,34 @@ private static boolean isInRange(BigInteger val, long min, long max) { && val.compareTo(BigInteger.valueOf(max)) <= 0; } - private String formatDouble(FPNum fpNum) { + private Value extractDouble(FPNum fpNum) { if (fpNum.isNaN()) { - return "double(\"NaN\")"; + return Value.exact(Double.NaN, "double(\"NaN\")"); } // 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); + return Value.exact( + value, Double.isInfinite(value) ? "double(\"" + value + "\")" : Double.toString(value)); } - private static String formatString(Expr arg, boolean isBytes) { - return quote(decodeZ3String(arg.getString()), isBytes); + private static Value extractString(Expr arg, boolean isBytes) { + int[] codePoints = decodeZ3String(arg.getString()); + // Bytes are modeled as their UTF-8 decoding, which is lossy for non-ASCII bytes. Java merges + // adjacent surrogates into one code point, which would change the string's size. + boolean isExact = + Arrays.stream(codePoints) + .allMatch( + isBytes + ? c -> c < 0x80 + : c -> c < Character.MIN_SURROGATE || c > Character.MAX_SURROGATE); + String str = new String(codePoints, 0, codePoints.length); + String display = quote(codePoints, isBytes); + if (!isExact) { + return Value.inexact(display); + } + return Value.exact(isBytes ? CelByteString.copyFromUtf8(str) : str, display); } // Z3 escapes characters outside printable ASCII, and a backslash before 'u', as \\u{hex}. @@ -199,40 +241,75 @@ private static String quote(int[] codePoints, boolean isBytes) { return sb.append('"').toString(); } - private String formatList(Expr listRef) { + private Value extractList(Expr listRef) { long length = evaluateLength(ctx.mkLength(typeSystem.getSeq(listRef))); + // Elements past the unroll limit are unconstrained, so they may violate the declared type. + boolean isExact = length <= comprehensionUnrollLimit; + long limit = isExact ? length : Math.min(length, MAX_ELEMENTS_TO_PRINT); + ImmutableList.Builder values = ImmutableList.builder(); List elements = new ArrayList<>(); - 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))))); + for (long i = 0; i < limit; i++) { + Value elem = extract(evaluate(ctx.mkNth(typeSystem.getSeq(listRef), ctx.mkInt(i)))); + if (elem.runtimeValue.isPresent()) { + values.add(elem.runtimeValue.get()); + } else { + isExact = false; + } + elements.add(elem.display); } - return join("[", elements, length, "elements", "]"); + String display = join("[", elements, length, "elements", "]"); + return isExact ? Value.exact(values.build(), display) : Value.inexact(display); } - private String formatMap(Expr mapRef) { + private Value extractMap(Expr mapRef) { long length = evaluateLength(ctx.mkLength(typeSystem.getMapKeys(mapRef))); + // Entries past the unroll limit are unconstrained, so they may violate the declared type. + boolean isExact = length <= comprehensionUnrollLimit; + long limit = isExact ? length : Math.min(length, MAX_ELEMENTS_TO_PRINT); + ImmutableMap.Builder values = ImmutableMap.builder(); List entries = new ArrayList<>(); Set> seenKeys = new HashSet<>(); - for (long i = 0; i < Math.min(length, MAX_ELEMENTS_TO_PRINT); i++) { + ArrayExpr keySet = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse()); + for (long i = 0; i < limit; i++) { Expr key = evaluate(ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i))); + keySet = ctx.mkStore(keySet, key, ctx.mkTrue()); if (!seenKeys.add(key) || !evaluate(ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), key)).isTrue()) { continue; } - Expr value = evaluate(ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), key)); - entries.add(format(key) + ": " + format(value)); + Value keyValue = extract(key); + Value value = + extract(evaluate(ctx.mkSelect((ArrayExpr) typeSystem.getMapValues(mapRef), key))); + if (keyValue.runtimeValue.isPresent() && value.runtimeValue.isPresent()) { + values.put(keyValue.runtimeValue.get(), value.runtimeValue.get()); + } else { + isExact = false; + } + entries.add(keyValue.display + ": " + value.display); } - return join("{", entries, length, "entries", "}"); + // Maps nested in dyn values aren't constrained to be well formed: the size comes from the key + // sequence and membership from the presence array, so they must agree. + isExact = + isExact + && seenKeys.size() == length + && evaluate(ctx.mkEq(typeSystem.getMapPresence(mapRef), keySet)).isTrue(); + + String display = join("{", entries, length, "entries", "}"); + return isExact ? Value.exact(values.buildOrThrow(), display) : Value.inexact(display); } private static String join( String prefix, List displayed, long length, String noun, String suffix) { + List shown = + new ArrayList<>(displayed.subList(0, Math.min(displayed.size(), MAX_ELEMENTS_TO_PRINT))); if (length > MAX_ELEMENTS_TO_PRINT) { - displayed.add("... (" + (length - MAX_ELEMENTS_TO_PRINT) + " more " + noun + ")"); + shown.add("... (" + (length - MAX_ELEMENTS_TO_PRINT) + " more " + noun + ")"); } - return prefix + String.join(", ", displayed) + suffix; + return prefix + String.join(", ", shown) + suffix; } - private String formatMessage(Expr msgRef) { + // TODO: Build message values. + private Value extractMessage(Expr msgRef) { Expr presenceArray = evaluate(typeSystem.getMsgPresence(msgRef)); String typeName = evaluate(typeSystem.getMsgTypeName(msgRef)).getString(); @@ -243,11 +320,11 @@ private String formatMessage(Expr msgRef) { for (Expr key : keys) { 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)); + entries.add(key.getString() + ": " + extract(value).display); } } - return typeName + "{" + String.join(", ", entries) + "}"; + return Value.inexact(typeName + "{" + String.join(", ", entries) + "}"); } private static void extractKeys(Expr arrayExpr, Set> keys) { @@ -281,10 +358,12 @@ private Expr evaluate(Expr expr) { return model.evaluate(expr, /* completion= */ true); } - private CelZ3CounterexampleGenerator(Context ctx, CelZ3TypeSystem typeSystem, Model model) { + private CelZ3CounterexampleGenerator( + Context ctx, CelZ3TypeSystem typeSystem, Model model, int comprehensionUnrollLimit) { this.ctx = ctx; this.typeSystem = typeSystem; this.model = model; + this.comprehensionUnrollLimit = comprehensionUnrollLimit; this.valuesOnPath = new HashSet<>(); } } diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 4438b4245..e6d0b97a3 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -25,10 +25,14 @@ import com.google.testing.junit.testparameterinjector.TestParameter; import com.google.testing.junit.testparameterinjector.TestParameterInjector; // import com.google.testing.testsize.MediumTest; +import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; import com.microsoft.z3.Expr; import com.microsoft.z3.IntExpr; +import com.microsoft.z3.SeqExpr; +import com.microsoft.z3.Solver; +import com.microsoft.z3.Status; import dev.cel.bundle.Cel; import dev.cel.bundle.CelFactory; import dev.cel.common.CelAbstractSyntaxTree; @@ -82,6 +86,7 @@ public final class CelVerifierZ3ImplTest { .setContainer(CelContainer.ofName("cel.expr.conformance.proto3")) .addCompilerLibraries( CelExtensions.bindings(), CelOptionalLibrary.INSTANCE, CelExtensions.comprehensions()) + .addRuntimeLibraries(CelOptionalLibrary.INSTANCE) .addMessageTypes(TestAllTypes.getDescriptor(), TestAllTypes.NestedMessage.getDescriptor()) .addVar("x", SimpleType.INT) .addVar("u", SimpleType.UINT) @@ -295,15 +300,121 @@ private enum WitnessTestCase { } @Test - public void isSatisfiable_witnessDisplayedAsCelLiteral(@TestParameter WitnessTestCase testCase) - throws Exception { + public void isSatisfiable_witnessValueSatisfiesExpressionAndDisplayRoundTrips( + @TestParameter WitnessTestCase testCase) throws Exception { + CelAbstractSyntaxTree ast = CEL.compile(testCase.expr).getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + CelWitness.Variable variable = result.witness().get().variables().get(testCase.variableName); + assertThat(variable.displayValue()).isEqualTo(testCase.expectedDisplayValue); + ImmutableMap input = + ImmutableMap.of(testCase.variableName, variable.value().get()); + assertThat(CEL.createProgram(ast).eval(input)).isEqualTo(true); + CelAbstractSyntaxTree displayRoundTrip = + CEL.compile(testCase.variableName + " == " + variable.displayValue()).getAst(); + assertThat(CEL.createProgram(displayRoundTrip).eval(input)).isEqualTo(true); + } + + private enum InexactWitnessTestCase { + INT_OUT_OF_RANGE("type(dyn_var) == int && dyn_var > 9223372036854775807", "dyn_var"), + UINT_OUT_OF_RANGE("type(dyn_var) == uint && dyn_var > 18446744073709551615u", "dyn_var"), + NEGATIVE_UINT("type(dyn_var) == uint && dyn_var < 0u", "dyn_var"), + TIMESTAMP_OUT_OF_RANGE( + "type(dyn_var) == google.protobuf.Timestamp" + + " && dyn_var > google.protobuf.Timestamp{seconds: 253402300799, nanos: 999999999}", + "dyn_var"), + SURROGATE_STRING( + "size(string_var) == 1 && string_var > '\\ud7ff' && string_var < '\\ue000'", "string_var"), + NON_ASCII_BYTES("by == b'\\xc3\\xa9'", "by"), + LIST_PAST_UNROLL_LIMIT("size(int_list) == 6", "int_list"), + MAP_PAST_UNROLL_LIMIT("size(string_int_map) == 6", "string_int_map"), + LIST_WITH_INEXACT_ELEMENT( + "size(dyn_list) == 1 && type(dyn_list[0]) == int && dyn_list[0] > 9223372036854775807", + "dyn_list"), + MAP_WITH_INEXACT_KEY( + "size(dyn_int_map) == 1" + + " && dyn_int_map.exists(k, type(k) == int && k > 9223372036854775807)", + "dyn_int_map"), + MAP_WITH_INEXACT_VALUE( + "size(string_dyn_map) == 1 && type(string_dyn_map['a']) == int" + + " && string_dyn_map['a'] > 9223372036854775807", + "string_dyn_map"), + OPTIONAL_WITH_INEXACT_VALUE( + "opt_dyn_var.hasValue() && type(opt_dyn_var.value()) == int" + + " && opt_dyn_var.value() > 9223372036854775807", + "opt_dyn_var"); + + private final String expr; + private final String variableName; + + InexactWitnessTestCase(String expr, String variableName) { + this.expr = expr; + this.variableName = variableName; + } + } + + @Test + public void isSatisfiable_noExactRuntimeValue_witnessValueEmpty( + @TestParameter InexactWitnessTestCase 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); + assertThat(result.witness().get().variables().get(testCase.variableName).value()).isEmpty(); + } + + // A map value in the model, as its key sequence and its present keys. + private enum InexactMapTestCase { + DUPLICATE_KEY(ImmutableList.of("a", "a"), ImmutableList.of("a")), + ABSENT_KEY(ImmutableList.of("a", "b"), ImmutableList.of("a")), + PRESENT_KEY_NOT_IN_SEQUENCE(ImmutableList.of(), ImmutableList.of("a")), + // Entries past the unroll limit (5) may violate the declared type. + PAST_UNROLL_LIMIT( + ImmutableList.of("a", "b", "c", "d", "e", "f"), + ImmutableList.of("a", "b", "c", "d", "e", "f")); + + private final ImmutableList keySequence; + private final ImmutableList presentKeys; + + InexactMapTestCase(ImmutableList keySequence, ImmutableList presentKeys) { + this.keySequence = keySequence; + this.presentKeys = presentKeys; + } + } + + @Test + @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types. + public void generateWitness_mapWithoutExactValue_valueEmpty( + @TestParameter InexactMapTestCase testCase) { + try (Context ctx = new Context()) { + CelZ3TypeSystem typeSystem = new CelZ3TypeSystem(ctx, /* parameterizeUnknowns= */ false); + Expr map = ctx.mkConst("map", typeSystem.celValueSort()); + Expr mapRef = typeSystem.getMapRef(map); + SeqExpr keys = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort())); + for (String key : testCase.keySequence) { + keys = ctx.mkConcat(keys, ctx.mkUnit(typeSystem.mkString(key))); + } + ArrayExpr presence = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse()); + for (String key : testCase.presentKeys) { + presence = ctx.mkStore(presence, (Expr) typeSystem.mkString(key), ctx.mkTrue()); + } + Solver solver = ctx.mkSolver(); + solver.add(typeSystem.isMap(map)); + solver.add(ctx.mkEq(typeSystem.getMapKeys(mapRef), keys)); + solver.add(ctx.mkEq(typeSystem.getMapPresence(mapRef), presence)); + assertThat(solver.check()).isEqualTo(Status.SATISFIABLE); + + CelWitness witness = + CelZ3CounterexampleGenerator.generate( + ctx, + typeSystem, + solver.getModel(), + /* comprehensionUnrollLimit= */ 5, + ImmutableSet.of(map)); + + assertThat(witness.variables().get("map").value()).isEmpty(); + } } @Test @@ -319,10 +430,13 @@ public void isSatisfiable_listAtDisplayLimit_displaysAllElements() throws Except @Test public void isSatisfiable_listPastDisplayLimit_elidesRemainingElements() throws Exception { + // Within the unroll limit the whole list is extracted, so the display must still elide it. + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(16).build(); 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); + CelVerificationResult result = verifier.isSatisfiable(ast); assertThat(result.message()) .endsWith( @@ -1160,6 +1274,7 @@ public void isAlwaysTrue_withUnknownIdentifier_evaluatesToUnknown( assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); assertThat(result.message()).contains("x = Unknown"); + assertThat(result.witness().get().variables().get("x").value()).isEmpty(); } @Test