From a5a92b5a6def20d00bb498875fda9d5958371e1c Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Wed, 21 Oct 2026 10:04:31 -0700 Subject: [PATCH] Expose the verifier's counterexamples as structured CelWitness values PiperOrigin-RevId: 1004026905 --- verifier/README.md | 5 +- .../main/java/dev/cel/verifier/BUILD.bazel | 5 + .../cel/verifier/CelAstToZ3Translator.java | 5 + .../cel/verifier/CelVerificationResult.java | 65 ++- .../dev/cel/verifier/CelVerifierZ3Impl.java | 71 +-- .../java/dev/cel/verifier/CelWitness.java | 52 ++ .../CelZ3CounterexampleGenerator.java | 453 +++++++++--------- .../cel/verifier/CelZ3TranslationContext.java | 8 +- .../verifier/CelPolicyVerifierImplTest.java | 4 +- .../cel/verifier/CelVerifierZ3ImplTest.java | 225 ++++++++- .../verifier/tools/CelVerifierReplTest.java | 2 +- 11 files changed, 599 insertions(+), 296 deletions(-) create mode 100644 verifier/src/main/java/dev/cel/verifier/CelWitness.java diff --git a/verifier/README.md b/verifier/README.md index d0c054485..7d9d7f899 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: @@ -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 6b498a162..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", ], ) @@ -186,10 +188,13 @@ 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", "//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/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/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 ceb5ae3d8..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.getTypeSystem(), - 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.getTypeSystem(), - 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.getTypeSystem(), - 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.getTypeSystem(), - 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.getTypeSystem(), - result.model, - /* isApproximate= */ false, - /* isCounterexample= */ true)) - : CelVerificationResult.verified( - "Condition is satisfiable." - + getCounterexampleString( - ctx, - translator.getTypeSystem(), - 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.getTypeSystem(), - result.model, - /* isApproximate= */ true, - /* isCounterexample= */ searchForCounterexample)); + extractWitness(ctx, translator, result.model), + /* isCounterexample= */ searchForCounterexample); case TRUNCATED: return CelVerificationResult.inconclusive( @@ -538,14 +502,13 @@ private CelAstToZ3Translator newTranslator(Context ctx, boolean parameterizeUnkn parameterizeUnknowns); } - private static String getCounterexampleString( - Context ctx, - CelZ3TypeSystem typeSystem, - Model model, - boolean isApproximate, - boolean isCounterexample) { + private CelWitness extractWitness(Context ctx, CelAstToZ3Translator translator, Model model) { return CelZ3CounterexampleGenerator.generate( - ctx, typeSystem, model, isApproximate, isCounterexample); + ctx, + translator.getTypeSystem(), + model, + 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 22d7b8a42..a5d796052 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -14,290 +14,306 @@ package dev.cel.verifier; -import com.google.common.base.Preconditions; +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; 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 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 org.jspecify.annotations.Nullable; +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 { 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; + private final int comprehensionUnrollLimit; - static String generate( + static CelWitness generate( Context ctx, CelZ3TypeSystem typeSystem, Model model, - 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))); - } + 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()); + } + + // 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; - if (bindings.isEmpty()) { - return isCounterexample - ? " (The expression fails unconditionally, regardless of input state)" - : " (The expression is satisfiable unconditionally, regardless of input state)"; + private static Value exact(Object runtimeValue, String display) { + return new Value(Optional.of(runtimeValue), display); } - String prefix; - if (isCounterexample) { - prefix = isApproximate ? " Potential counterexample input:" : " Counterexample input:"; - } else { - prefix = isApproximate ? " Potential satisfying input:" : " Satisfying input:"; + private static Value inexact(String display) { + return new Value(Optional.empty(), display); } - return prefix + String.join("", bindings); - } - private static String formatExpr( - Context ctx, CelZ3TypeSystem typeSystem, Model model, @Nullable Expr expr) { - Preconditions.checkState(expr != null, "Z3 failed to evaluate the expression natively."); + private Value(Optional runtimeValue, String display) { + this.runtimeValue = runtimeValue; + this.display = display; + } + } + private Value extract(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]); + 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 formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "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 formatExpr(ctx, typeSystem, model, expr.getArgs()[0]); + return Value.exact(args[0].isTrue(), args[0].toString()); + } else if (decl.equals(typeSystem.doubleCons().ConstructorDecl())) { + return extractDouble((FPNum) args[0]); } else if (decl.equals(typeSystem.stringCons().ConstructorDecl())) { - return expr.getArgs()[0].toString(); + return extractString(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 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); + 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 Value.inexact("timestamp(" + seconds + ")"); } - return doubleArg.toString(); + 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(); + 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 reconstructList(ctx, typeSystem, model, expr.getArgs()[0]); + return extractList(args[0]); } else if (decl.equals(typeSystem.mapCons().ConstructorDecl())) { - return reconstructMap(ctx, typeSystem, model, expr.getArgs()[0]); + return extractMap(args[0]); } else if (decl.equals(typeSystem.messageCons().ConstructorDecl())) { - return reconstructMessage(ctx, typeSystem, model, expr.getArgs()[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"; - } 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 Value.exact(NullValue.NULL_VALUE, "null"); } - return expr.toString(); + // Optional is the only remaining constructor. + if (!evaluate(typeSystem.optHasValue(args[0])).isTrue()) { + return Value.exact(Optional.empty(), "optional.none()"); + } + Value value = extract(evaluate(typeSystem.getOptionalValue(args[0]))); + return new Value( + value.runtimeValue.map(Optional::of), "optional.of(" + value.display + ")"); } - 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); - } - if (nanos.equals(BigInteger.ZERO)) { - return "timestamp(" + seconds + ")"; + private static boolean isInRange(BigInteger val, long min, long max) { + return val.compareTo(BigInteger.valueOf(min)) >= 0 + && val.compareTo(BigInteger.valueOf(max)) <= 0; + } + + private Value extractDouble(FPNum fpNum) { + if (fpNum.isNaN()) { + return Value.exact(Double.NaN, "double(\"NaN\")"); } - return "google.protobuf.Timestamp{seconds: " + seconds + ", nanos: " + nanos + "}"; + // Z3 doubles are IEEE 754 binary64, so their bits convert exactly. + double value = + Double.longBitsToDouble( + ((BitVecNum) ctx.mkFPToIEEEBV(fpNum).simplify()).getBigInteger().longValue()); + return Value.exact( + value, Double.isInfinite(value) ? "double(\"" + value + "\")" : Double.toString(value)); } - 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')"; + 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 "duration('" + totalNanos + "ns')"; + return Value.exact(isBytes ? CelByteString.copyFromUtf8(str) : str, display); } - 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); - 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)); + // 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++)); + } } - if (length > printLimit) { - elements.add("... (" + (length - printLimit) + " more elements)"); + return codePoints.build().toArray(); + } + + // 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 sb.append('"').toString(); + } - return "[" + String.join(", ", elements) + "]"; + 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 < 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); + } + String display = join("[", elements, length, "elements", "]"); + return isExact ? Value.exact(values.build(), display) : Value.inexact(display); } - 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 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 (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)) { + 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 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)); + 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); } - if (length > printLimit) { - entries.add("... (" + (length - printLimit) + " more 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(); - return "{" + String.join(", ", entries) + "}"; + String display = join("{", entries, length, "entries", "}"); + return isExact ? Value.exact(values.buildOrThrow(), display) : Value.inexact(display); } - 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) { + List shown = + new ArrayList<>(displayed.subList(0, Math.min(displayed.size(), MAX_ELEMENTS_TO_PRINT))); + if (length > MAX_ELEMENTS_TO_PRINT) { + shown.add("... (" + (length - MAX_ELEMENTS_TO_PRINT) + " more " + noun + ")"); + } + return prefix + String.join(", ", shown) + suffix; + } - String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", ""); + // TODO: Build message values. + private Value extractMessage(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() + ": " + extract(value).display); } } - return typeName + "{" + String.join(", ", entries) + "}"; + return Value.inexact(typeName + "{" + String.join(", ", entries) + "}"); } private static void extractKeys(Expr arrayExpr, Set> keys) { @@ -314,8 +330,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 +338,20 @@ 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, int comprehensionUnrollLimit) { + this.ctx = ctx; + this.typeSystem = typeSystem; + this.model = model; + this.comprehensionUnrollLimit = comprehensionUnrollLimit; } } 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..5dc66ecb7 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; @@ -81,6 +85,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) @@ -196,13 +201,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 +253,196 @@ 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_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.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 + 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 { + // 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); + + 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(); @@ -1064,6 +1268,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 @@ -1461,12 +1666,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 +1711,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 +1835,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 +2810,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(); }