diff --git a/verifier/BUILD.bazel b/verifier/BUILD.bazel index ef1316ca2..8eda9a3f0 100644 --- a/verifier/BUILD.bazel +++ b/verifier/BUILD.bazel @@ -35,6 +35,13 @@ java_library( exports = ["//verifier/src/main/java/dev/cel/verifier:policy_verifier_factory"], ) +java_library( + name = "policy_verifier_impl", + compatible_with = [], + visibility = [":verifier_internal"], + exports = ["//verifier/src/main/java/dev/cel/verifier:policy_verifier_impl"], +) + java_library( name = "verifier_factory", compatible_with = [], diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index 3396b6df4..2f0f95fd1 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel @@ -11,6 +11,9 @@ package( java_library( name = "verifier", srcs = [ + "CelCounterexample.java", + "CelPolicyDiagnostic.java", + "CelPolicyEquivalenceDiagnostic.java", "CelVerificationException.java", "CelVerificationResult.java", "CelVerifier.java", @@ -21,8 +24,13 @@ java_library( deps = [ "//:auto_value", "//common:cel_ast", + "//common:compiler_common", + "//common:source", + "//common:source_location", "//common/types:type_providers", "@maven//:com_google_errorprone_error_prone_annotations", + "@maven//:com_google_guava_guava", + "@maven//:org_jspecify_jspecify", ], ) @@ -76,7 +84,10 @@ java_library( java_library( name = "policy_verifier_impl", - srcs = ["CelPolicyVerifierImpl.java"], + srcs = [ + "CelPolicyPathTracer.java", + "CelPolicyVerifierImpl.java", + ], compatible_with = [], tags = [ ], @@ -88,11 +99,14 @@ java_library( "//common:cel_ast", "//common:cel_source", "//common:compiler_common", + "//common:source_location", "//common/formats:value_string", "//policy", "//policy:compiled_rule", "//policy:compiler", + "//policy:source", "//policy:validation_exception", + "//runtime:evaluation_exception", "@maven//:com_google_guava_guava", ], ) @@ -153,6 +167,7 @@ java_library( java_library( name = "z3_impl", srcs = [ + "CegarRefiner.java", "CelAstAlphaHasher.java", "CelAstToZ3Translator.java", "CelVerifierZ3Impl.java", @@ -180,9 +195,12 @@ java_library( "//common/types", "//common/types:cel_types", "//common/types:type_providers", + "//common/values:cel_byte_string", + "//common/values:cel_value_provider", "//optimizer", "//optimizer:optimization_exception", "//optimizer:optimizer_builder", + "//runtime:evaluation_exception", "//verifier/axioms", "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:com_google_guava_guava", diff --git a/verifier/src/main/java/dev/cel/verifier/CegarRefiner.java b/verifier/src/main/java/dev/cel/verifier/CegarRefiner.java new file mode 100644 index 000000000..31fd301d3 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CegarRefiner.java @@ -0,0 +1,137 @@ +// 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.common.base.Preconditions; +import com.google.common.collect.ImmutableMap; +import com.google.errorprone.annotations.Immutable; +import dev.cel.bundle.Cel; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.runtime.CelEvaluationException; +import java.util.HashMap; +import java.util.Map; +import java.util.Objects; +import java.util.Optional; + +/** + * Evaluates candidate counterexample models against the concrete CEL runtime to confirm or refute + * potential violations (CEGAR refinement loop). + */ +@Immutable +final class CegarRefiner { + + @Immutable + static final class CegarOutcome { + private final boolean isViolation; + private final Optional evaluationErrorMessage; + + static CegarOutcome violation() { + return new CegarOutcome(true, Optional.empty()); + } + + static CegarOutcome spurious() { + return new CegarOutcome(false, Optional.empty()); + } + + static CegarOutcome evaluationError(String errorMessage) { + return new CegarOutcome(false, Optional.of(errorMessage)); + } + + private CegarOutcome(boolean isViolation, Optional evaluationErrorMessage) { + this.isViolation = isViolation; + this.evaluationErrorMessage = evaluationErrorMessage; + } + + boolean isViolation() { + return isViolation; + } + + Optional evaluationErrorMessage() { + return evaluationErrorMessage; + } + } + + private final Cel cel; + + CegarRefiner(Cel cel) { + this.cel = Preconditions.checkNotNull(cel); + } + + CegarOutcome refineEquivalence( + CelAbstractSyntaxTree astA, CelAbstractSyntaxTree astB, CelCounterexample model) { + if (model.isSatisfyingInput()) { + return CegarOutcome.spurious(); + } + try { + ImmutableMap evalContext = model.toEvaluationContext(); + Object resA = cel.createProgram(astA).eval(evalContext); + Object resB = cel.createProgram(astB).eval(evalContext); + // If concrete evaluation produces identical results, the candidate SMT divergence was an + // artifact of abstraction (spurious). Otherwise, concrete outputs diverge (violation). + return Objects.equals(resA, resB) ? CegarOutcome.spurious() : CegarOutcome.violation(); + } catch (CelEvaluationException e) { + return CegarOutcome.evaluationError(e.getMessage()); + } + } + + CegarOutcome refineSatisfiability( + CelAbstractSyntaxTree ast, boolean searchForCounterexample, CelCounterexample model) { + if (searchForCounterexample ? model.isSatisfyingInput() : !model.isSatisfyingInput()) { + return CegarOutcome.spurious(); + } + try { + ImmutableMap evalContext = model.toEvaluationContext(); + Object res = cel.createProgram(ast).eval(evalContext); + boolean isEvaluationTrue = Objects.equals(res, true); + // For universal truth (searchForCounterexample=true), evaluating to true refutes the + // candidate counterexample (spurious). For satisfiability search + // (searchForCounterexample=false), + // evaluating to true confirms the candidate satisfying model (violation). + boolean isSpurious = searchForCounterexample == isEvaluationTrue; + return isSpurious ? CegarOutcome.spurious() : CegarOutcome.violation(); + } catch (CelEvaluationException e) { + return CegarOutcome.evaluationError(e.getMessage()); + } + } + + CegarOutcome refineImplication( + CelAbstractSyntaxTree assumeAst, + CelAbstractSyntaxTree assertAst, + Map boundSymbols, + CelCounterexample model) { + if (model.isSatisfyingInput()) { + return CegarOutcome.spurious(); + } + try { + Map evalContext = new HashMap<>(model.toEvaluationContext()); + for (Map.Entry entry : boundSymbols.entrySet()) { + Object boundVal = cel.createProgram(entry.getValue()).eval(evalContext); + evalContext.put(entry.getKey(), boundVal); + } + Object assumeVal = cel.createProgram(assumeAst).eval(evalContext); + if (Objects.equals(assumeVal, true)) { + Object assertVal = cel.createProgram(assertAst).eval(evalContext); + // If the premise holds and the conclusion evaluates to true, the candidate counterexample + // is refuted (spurious). If the conclusion fails under true premise, implication is + // violated. + return Objects.equals(assertVal, true) ? CegarOutcome.spurious() : CegarOutcome.violation(); + } + // The candidate input did not satisfy the premise, so it cannot serve as a counterexample. + return CegarOutcome.spurious(); + } catch (CelEvaluationException e) { + return CegarOutcome.evaluationError(e.getMessage()); + } + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index ba63e9693..51955c12c 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -610,7 +610,7 @@ private FieldAccess getMapAccess(Expr operand, String field, BoolExpr typeGua typeConstraints.add( ctx.mkImplies( CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, (BoolExpr) presence), valNotError)); - if (unknownIdentifiers.isEmpty()) { + if (!unknownIdentifiers.contains(field)) { BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(value)); typeConstraints.add( ctx.mkImplies( @@ -630,7 +630,7 @@ private FieldAccess getMsgAccess(Expr operand, String field, BoolExpr typeGua typeConstraints.add( ctx.mkImplies( CelZ3TypeSystem.mkAndFlattened(ctx, typeGuard, (BoolExpr) presence), valNotError)); - if (unknownIdentifiers.isEmpty()) { + if (!unknownIdentifiers.contains(field)) { BoolExpr valNotUnknown = ctx.mkNot(typeSystem.isUnknown(value)); typeConstraints.add( ctx.mkImplies( diff --git a/verifier/src/main/java/dev/cel/verifier/CelCounterexample.java b/verifier/src/main/java/dev/cel/verifier/CelCounterexample.java new file mode 100644 index 000000000..5908406b1 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CelCounterexample.java @@ -0,0 +1,99 @@ +// 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 com.google.errorprone.annotations.Immutable; +import dev.cel.common.types.CelType; +import java.util.Map; +import java.util.Optional; +import org.jspecify.annotations.Nullable; + +/** Encapsulates a structured variable assignment model produced by formal verification. */ +@AutoValue +@AutoValue.CopyAnnotations +@Immutable +public abstract class CelCounterexample { + + /** Represents a single variable binding within a counterexample. */ + @AutoValue + @AutoValue.CopyAnnotations + @Immutable + @SuppressWarnings("Immutable") // Values are deeply immutable. + public abstract static class Binding { + /** Returns the name of the variable. */ + public abstract String name(); + + /** Returns the inferred CEL type of the variable. */ + public abstract CelType type(); + + /** + * Returns the native Java representation of the value (e.g., Long, Boolean, String, Instant, + * Duration, ImmutableList, ImmutableMap, Message, etc.), or empty if unassigned or unavailable. + */ + public abstract Optional nativeValue(); + + /** + * Returns the CEL literal representation of the value (e.g., "80", "\"admin\"", "true", "[1, + * 2]"). + */ + public abstract String celString(); + + public static Binding of( + String name, CelType type, @Nullable Object nativeValue, String celString) { + return new AutoValue_CelCounterexample_Binding( + name, type, Optional.ofNullable(nativeValue), celString); + } + } + + /** Returns all variable bindings keyed by variable name. */ + public abstract ImmutableMap bindings(); + + /** Returns true if this counterexample was derived from an approximate solver model. */ + public abstract boolean isApproximate(); + + /** Returns true if this model represents a satisfying assignment rather than a counterexample. */ + public abstract boolean isSatisfyingInput(); + + /** Returns the formatted display string representation. */ + public abstract String toDisplayString(); + + /** Looks up a variable binding by name. */ + public Optional get(String variableName) { + return Optional.ofNullable(bindings().get(variableName)); + } + + /** + * Returns a native Java variable map suitable for evaluating expressions in CelRuntime (e.g., + * Cel.createProgram().eval(toEvaluationContext())). + */ + public ImmutableMap toEvaluationContext() { + ImmutableMap.Builder builder = ImmutableMap.builder(); + for (Binding binding : bindings().values()) { + binding.nativeValue().ifPresent(value -> builder.put(binding.name(), value)); + } + return builder.buildOrThrow(); + } + + public static CelCounterexample create( + Map bindings, + boolean isApproximate, + boolean isSatisfyingInput, + String toDisplayString) { + return new AutoValue_CelCounterexample( + ImmutableMap.copyOf(bindings), isApproximate, isSatisfyingInput, toDisplayString); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/CelPolicyDiagnostic.java b/verifier/src/main/java/dev/cel/verifier/CelPolicyDiagnostic.java new file mode 100644 index 000000000..02a9423f9 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CelPolicyDiagnostic.java @@ -0,0 +1,68 @@ +// 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.errorprone.annotations.Immutable; +import dev.cel.common.CelIssue; +import dev.cel.common.CelSourceLocation; +import dev.cel.common.Source; +import java.util.Optional; + +/** Source-located explanation of a policy invariant violation. */ +@AutoValue +@AutoValue.CopyAnnotations +@Immutable +public abstract class CelPolicyDiagnostic { + + /** Returns the ID of the invariant that failed verification. */ + public abstract String invariantId(); + + /** Returns the name or ID of the offending rule if defined in the policy, or empty. */ + public abstract Optional offendingRuleName(); + + /** Returns the 0-based index of the policy match rule that fired. */ + public abstract int offendingRuleIndex(); + + /** + * Returns the underlying {@link CelIssue} containing location and formatted error explanation. + */ + public abstract CelIssue issue(); + + /** Formats a visual source code snippet highlighting the offending YAML rule. */ + public String toDisplayString(Source source) { + return issue().toDisplayString(source); + } + + static CelPolicyDiagnostic create( + String invariantId, + Optional ruleName, + int ruleIndex, + long yamlNodeId, + CelSourceLocation location, + String explanation) { + return new AutoValue_CelPolicyDiagnostic( + invariantId, ruleName, ruleIndex, CelIssue.formatError(yamlNodeId, location, explanation)); + } + + static CelPolicyDiagnostic create( + String invariantId, + int ruleIndex, + long yamlNodeId, + CelSourceLocation location, + String explanation) { + return create(invariantId, Optional.empty(), ruleIndex, yamlNodeId, location, explanation); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/CelPolicyEquivalenceDiagnostic.java b/verifier/src/main/java/dev/cel/verifier/CelPolicyEquivalenceDiagnostic.java new file mode 100644 index 000000000..794dda8aa --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CelPolicyEquivalenceDiagnostic.java @@ -0,0 +1,114 @@ +// 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.ImmutableList; +import com.google.errorprone.annotations.Immutable; +import dev.cel.common.CelIssue; +import dev.cel.common.CelSourceLocation; +import dev.cel.common.Source; +import java.util.Optional; + +/** Dual-source diagnostic pinpointing why two policies produced conflicting outputs. */ +@AutoValue +@AutoValue.CopyAnnotations +@Immutable +public abstract class CelPolicyEquivalenceDiagnostic { + + /** Represents the firing branch attribution for a single policy in an equivalence comparison. */ + @AutoValue + @AutoValue.CopyAnnotations + @Immutable + public abstract static class PolicyBranchAttribution { + /** Returns the name of the policy. */ + public abstract String policyName(); + + /** Returns the name or ID of the matching rule if defined in the policy, or empty. */ + public abstract Optional ruleName(); + + /** Returns the 0-based index of the matching rule that fired. */ + public abstract int ruleIndex(); + + /** Returns the evaluated output value string produced by this rule branch. */ + public abstract String evaluatedOutput(); + + /** Returns the underlying {@link CelIssue} containing location and match attribution. */ + public abstract CelIssue issue(); + + /** Formats a visual source code snippet highlighting the matching YAML rule. */ + public String toDisplayString(Source source) { + return issue().toDisplayString(source); + } + + static PolicyBranchAttribution create( + String policyName, + Optional ruleName, + int ruleIndex, + long matchNodeId, + CelSourceLocation location, + String evaluatedOutput) { + String ruleIdentifier = + ruleName.isPresent() + ? String.format("rule '%s'", ruleName.get()) + : String.format("match[%d]", ruleIndex); + String message = + String.format( + "Policy '%s' %s matched and evaluated to output: %s", + policyName, ruleIdentifier, evaluatedOutput); + CelIssue issue = CelIssue.formatError(matchNodeId, location, message); + return new AutoValue_CelPolicyEquivalenceDiagnostic_PolicyBranchAttribution( + policyName, ruleName, ruleIndex, evaluatedOutput, issue); + } + + static PolicyBranchAttribution create( + String policyName, + int ruleIndex, + long matchNodeId, + CelSourceLocation location, + String evaluatedOutput) { + return create( + policyName, Optional.empty(), ruleIndex, matchNodeId, location, evaluatedOutput); + } + } + + /** Returns the firing branch attribution for Policy A. */ + public abstract PolicyBranchAttribution policyABranch(); + + /** Returns the firing branch attribution for Policy B. */ + public abstract PolicyBranchAttribution policyBBranch(); + + /** Returns both issues for diagnostic inspection. */ + public ImmutableList toCelIssues() { + return ImmutableList.of(policyABranch().issue(), policyBBranch().issue()); + } + + /** + * Formats a side-by-side snippet display highlighting the diverging branches in both policies. + */ + public String toDisplayString(Source sourceA, Source sourceB) { + return String.format( + "Equivalence Divergence Detected:\n [Policy A: %s]\n%s\n\n [Policy B: %s]\n%s", + policyABranch().policyName(), + policyABranch().toDisplayString(sourceA), + policyBBranch().policyName(), + policyBBranch().toDisplayString(sourceB)); + } + + static CelPolicyEquivalenceDiagnostic of( + PolicyBranchAttribution branchA, PolicyBranchAttribution branchB) { + return new AutoValue_CelPolicyEquivalenceDiagnostic(branchA, branchB); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/CelPolicyPathTracer.java b/verifier/src/main/java/dev/cel/verifier/CelPolicyPathTracer.java new file mode 100644 index 000000000..cfb8d72bf --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CelPolicyPathTracer.java @@ -0,0 +1,191 @@ +// 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 dev.cel.common.CelSourceLocation; +import dev.cel.common.formats.ValueString; +import dev.cel.policy.CelCompiledRule; +import dev.cel.policy.CelCompiledRule.CelCompiledMatch; +import dev.cel.policy.CelCompiledRule.CelCompiledVariable; +import dev.cel.policy.CelPolicy; +import dev.cel.policy.CelPolicySource; +import dev.cel.runtime.CelEvaluationException; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Objects; +import java.util.Optional; + +/** Traces which rule branches matched and evaluated under a concrete counterexample assignment. */ +final class CelPolicyPathTracer { + + /** Encapsulates the trace outcome of a single firing rule match. */ + static final class MatchTrace { + final int ruleIndex; + final Optional ruleName; + final long sourceId; + final CelSourceLocation location; + final Object evaluatedOutput; + + MatchTrace( + int ruleIndex, + Optional ruleName, + long sourceId, + CelSourceLocation location, + Object evaluatedOutput) { + this.ruleIndex = ruleIndex; + this.ruleName = ruleName; + this.sourceId = sourceId; + this.location = location; + this.evaluatedOutput = evaluatedOutput; + } + } + + /** Traces the policy execution graph to determine the firing rule match under the given model. */ + static Optional traceMatchingBranch( + CelPolicy policy, CelCompiledRule compiledRule, CelCounterexample counterexample) { + CelPolicySource policySource = policy.policySource(); + Map evalContext = new HashMap<>(counterexample.toEvaluationContext()); + + // Populate compiled variables in the evaluation context + for (CelCompiledVariable var : compiledRule.variables()) { + try { + Object val = compiledRule.cel().createProgram(var.ast()).eval(evalContext); + evalContext.put(var.name(), val); + evalContext.put(var.celVarDecl().name(), val); + } catch (CelEvaluationException e) { + // Variable evaluation failed under this counterexample model. + // Safe and necessary to ignore. + } + } + + return traceRule(compiledRule, evalContext, policySource); + } + + private static Optional traceRule( + CelCompiledRule compiledRule, Map evalContext, CelPolicySource policySource) { + if (compiledRule.semantic() == CelPolicy.EvaluationSemantic.AGGREGATE) { + return traceAggregateRule(compiledRule, evalContext, policySource); + } + + Optional ruleName = compiledRule.ruleId().map(ValueString::value); + MatchTrace firstConditionErrorTrace = null; + + for (int i = 0; i < compiledRule.matches().size(); i++) { + CelCompiledMatch match = compiledRule.matches().get(i); + boolean conditionMatched; + try { + Object condVal = compiledRule.cel().createProgram(match.condition()).eval(evalContext); + conditionMatched = Objects.equals(condVal, true); + } catch (CelEvaluationException e) { + // A condition that encounters an evaluation error does not evaluate to boolean true. + // Record as fallback trace in case no subsequent branch matches. + conditionMatched = false; + if (firstConditionErrorTrace == null) { + long sourceId = match.sourceId(); + CelSourceLocation location = computeLocation(sourceId, policySource); + Object outputVal = ""; + firstConditionErrorTrace = new MatchTrace(i, ruleName, sourceId, location, outputVal); + } + } + + if (conditionMatched) { + if (match.result().kind() == CelCompiledMatch.Result.Kind.OUTPUT) { + Object outputVal; + try { + outputVal = + compiledRule.cel().createProgram(match.result().output().ast()).eval(evalContext); + } catch (CelEvaluationException e) { + outputVal = ""; + } + long sourceId = + match.sourceId() != 0 ? match.sourceId() : match.result().output().sourceId(); + CelSourceLocation location = computeLocation(sourceId, policySource); + return Optional.of(new MatchTrace(i, ruleName, sourceId, location, outputVal)); + } else if (match.result().kind() == CelCompiledMatch.Result.Kind.RULE) { + Optional nestedTrace = + traceRule(match.result().rule(), evalContext, policySource); + if (nestedTrace.isPresent()) { + return nestedTrace; + } + } + } + } + + return Optional.ofNullable(firstConditionErrorTrace); + } + + private static Optional traceAggregateRule( + CelCompiledRule compiledRule, Map evalContext, CelPolicySource policySource) { + List outputs = new ArrayList<>(); + MatchTrace firstTrace = null; + MatchTrace firstConditionErrorTrace = null; + Optional ruleName = compiledRule.ruleId().map(ValueString::value); + + for (int i = 0; i < compiledRule.matches().size(); i++) { + CelCompiledMatch match = compiledRule.matches().get(i); + boolean conditionMatched; + try { + Object condVal = compiledRule.cel().createProgram(match.condition()).eval(evalContext); + conditionMatched = Objects.equals(condVal, true); + } catch (CelEvaluationException e) { + // An evaluation error does not evaluate to boolean true, contributing nothing to the list. + conditionMatched = false; + if (firstConditionErrorTrace == null) { + long sourceId = match.sourceId(); + CelSourceLocation location = computeLocation(sourceId, policySource); + Object outputVal = ""; + firstConditionErrorTrace = new MatchTrace(i, ruleName, sourceId, location, outputVal); + } + } + + if (conditionMatched && match.result().kind() == CelCompiledMatch.Result.Kind.OUTPUT) { + if (firstTrace == null) { + long sourceId = + match.sourceId() != 0 ? match.sourceId() : match.result().output().sourceId(); + CelSourceLocation location = computeLocation(sourceId, policySource); + firstTrace = new MatchTrace(i, ruleName, sourceId, location, outputs); + } + try { + Object outputVal = + compiledRule.cel().createProgram(match.result().output().ast()).eval(evalContext); + outputs.add(outputVal); + } catch (CelEvaluationException e) { + outputs.add(""); + } + } + } + + if (firstTrace != null) { + return Optional.of(firstTrace); + } + + return Optional.ofNullable(firstConditionErrorTrace); + } + + static CelSourceLocation computeLocation(long sourceId, CelPolicySource policySource) { + if (sourceId == 0) { + return CelSourceLocation.NONE; + } + int offset = Optional.ofNullable(policySource.getPositionsMap().get(sourceId)).orElse(-1); + if (offset == -1) { + return CelSourceLocation.NONE; + } + return policySource.getOffsetLocation(offset).orElse(CelSourceLocation.NONE); + } + + private CelPolicyPathTracer() {} +} diff --git a/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifierImpl.java b/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifierImpl.java index 96473c16f..63c94474d 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifierImpl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelPolicyVerifierImpl.java @@ -28,6 +28,9 @@ import dev.cel.policy.CelPolicy; import dev.cel.policy.CelPolicyCompiler; import dev.cel.policy.CelPolicyValidationException; +import dev.cel.verifier.CelPolicyEquivalenceDiagnostic.PolicyBranchAttribution; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import java.util.Optional; /** Implementation of CelPolicyVerifier using a CelVerifier. */ final class CelPolicyVerifierImpl implements CelPolicyVerifier { @@ -66,7 +69,42 @@ public CelVerificationResult verifyEquivalence(CelPolicy policyA, CelPolicy poli throws CelPolicyValidationException, CelVerificationException { CelAbstractSyntaxTree astA = compiler.compile(policyA); CelAbstractSyntaxTree astB = compiler.compile(policyB); - return astVerifier.verifyEquivalence(astA, astB); + CelVerificationResult result = astVerifier.verifyEquivalence(astA, astB); + if (result.status() == VerificationStatus.VIOLATED + && result.counterexampleModel().isPresent()) { + CelCounterexample model = result.counterexampleModel().get(); + CelCompiledRule compiledRuleA = compiler.compileRule(policyA); + CelCompiledRule compiledRuleB = compiler.compileRule(policyB); + + Optional traceA = + CelPolicyPathTracer.traceMatchingBranch(policyA, compiledRuleA, model); + Optional traceB = + CelPolicyPathTracer.traceMatchingBranch(policyB, compiledRuleB, model); + + if (traceA.isPresent() && traceB.isPresent()) { + PolicyBranchAttribution branchA = + PolicyBranchAttribution.create( + policyA.name().value(), + traceA.get().ruleName, + traceA.get().ruleIndex, + traceA.get().sourceId, + traceA.get().location, + String.valueOf(traceA.get().evaluatedOutput)); + PolicyBranchAttribution branchB = + PolicyBranchAttribution.create( + policyB.name().value(), + traceB.get().ruleName, + traceB.get().ruleIndex, + traceB.get().sourceId, + traceB.get().location, + String.valueOf(traceB.get().evaluatedOutput)); + + CelPolicyEquivalenceDiagnostic equivDiag = + CelPolicyEquivalenceDiagnostic.of(branchA, branchB); + result = result.toBuilder().setPolicyEquivalenceDiagnostic(equivDiag).build(); + } + } + return result; } @Override @@ -153,6 +191,42 @@ public ImmutableMap verifyInvariants(CelPolicy po assertAst, boundSymbols, String.format("Invariant '%s'", invariantId)); + + if (result.status() == VerificationStatus.VIOLATED + && result.counterexampleModel().isPresent()) { + Optional matchTrace = + CelPolicyPathTracer.traceMatchingBranch( + policy, compiledRule, result.counterexampleModel().get()); + if (matchTrace.isPresent()) { + CelPolicyPathTracer.MatchTrace trace = matchTrace.get(); + String ruleIdentifier = + trace.ruleName.isPresent() + ? String.format("rule '%s'", trace.ruleName.get()) + : String.format("match[%d]", trace.ruleIndex); + String outputStr = String.valueOf(trace.evaluatedOutput); + String explanation; + if (outputStr.startsWith(" counterexampleModel(); + + /** Returns the source-located policy invariant diagnostic, if applicable. */ + public abstract Optional policyDiagnostic(); + + /** Returns the dual-source policy equivalence diagnostic, if applicable. */ + public abstract Optional policyEquivalenceDiagnostic(); + /** * 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 @@ -52,29 +61,84 @@ public String message() { return reason() + counterexample(); } + abstract Builder toBuilder(); + + static Builder builder() { + return new AutoValue_CelVerificationResult.Builder() + .setReason("") + .setCounterexample("") + .setCounterexampleModel(Optional.empty()) + .setPolicyDiagnostic(Optional.empty()) + .setPolicyEquivalenceDiagnostic(Optional.empty()); + } + + /** Builder for {@link CelVerificationResult}. */ + @AutoValue.Builder + abstract static class Builder { + abstract Builder setStatus(VerificationStatus status); + + abstract Builder setReason(String reason); + + abstract Builder setCounterexample(String counterexample); + + abstract Builder setCounterexampleModel(Optional counterexampleModel); + + Builder setCounterexampleModel(CelCounterexample counterexampleModel) { + return setCounterexampleModel(Optional.of(counterexampleModel)); + } + + abstract Builder setPolicyDiagnostic(Optional diagnostic); + + Builder setPolicyDiagnostic(CelPolicyDiagnostic diagnostic) { + return setPolicyDiagnostic(Optional.of(diagnostic)); + } + + abstract Builder setPolicyEquivalenceDiagnostic( + Optional diagnostic); + + Builder setPolicyEquivalenceDiagnostic(CelPolicyEquivalenceDiagnostic diagnostic) { + return setPolicyEquivalenceDiagnostic(Optional.of(diagnostic)); + } + + abstract CelVerificationResult build(); + } + static CelVerificationResult verified() { - return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, "", ""); + return builder().setStatus(VerificationStatus.VERIFIED).build(); } - static CelVerificationResult verified(String reason) { - return new AutoValue_CelVerificationResult(VerificationStatus.VERIFIED, reason, ""); + static CelVerificationResult verified(String reason, CelCounterexample counterexample) { + return builder() + .setStatus(VerificationStatus.VERIFIED) + .setReason(reason) + .setCounterexample(counterexample.toDisplayString()) + .setCounterexampleModel(counterexample) + .build(); } static CelVerificationResult failed(String reason) { - return new AutoValue_CelVerificationResult(VerificationStatus.VIOLATED, reason, ""); + return builder().setStatus(VerificationStatus.VIOLATED).setReason(reason).build(); } - static CelVerificationResult failed(String reason, String counterexample) { - return new AutoValue_CelVerificationResult( - VerificationStatus.VIOLATED, reason, counterexample); + static CelVerificationResult failed(String reason, CelCounterexample counterexample) { + return builder() + .setStatus(VerificationStatus.VIOLATED) + .setReason(reason) + .setCounterexample(counterexample.toDisplayString()) + .setCounterexampleModel(counterexample) + .build(); } static CelVerificationResult inconclusive(String reason) { - return new AutoValue_CelVerificationResult(VerificationStatus.INCONCLUSIVE, reason, ""); + return builder().setStatus(VerificationStatus.INCONCLUSIVE).setReason(reason).build(); } - static CelVerificationResult inconclusive(String reason, String counterexample) { - return new AutoValue_CelVerificationResult( - VerificationStatus.INCONCLUSIVE, reason, counterexample); + static CelVerificationResult inconclusive(String reason, CelCounterexample counterexample) { + return builder() + .setStatus(VerificationStatus.INCONCLUSIVE) + .setReason(reason) + .setCounterexample(counterexample.toDisplayString()) + .setCounterexampleModel(counterexample) + .build(); } } diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierBuilder.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierBuilder.java index c49bb4343..c45fa3edd 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierBuilder.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierBuilder.java @@ -82,6 +82,23 @@ public interface CelVerifierBuilder { @CanIgnoreReturnValue CelVerifierBuilder setComprehensionUnrollLimit(int unrollLimit); + /** + * Enables or disables Counterexample-Guided Abstraction Refinement (CEGAR). + * + *

When enabled, if the SMT solver returns an approximate model (e.g., due to unmodeled custom + * functions, approximations, or bounded loops), the candidate inputs are validated using concrete + * {@link dev.cel.bundle.Cel} program execution. If concrete evaluation confirms an invariant + * violation or equivalence divergence, the result is upgraded from {@code INCONCLUSIVE} to {@code + * VIOLATED}. + * + *

Note: This option requires an execution-ready CEL environment where any + * custom functions referenced in the policy have registered runtime {@link + * dev.cel.runtime.CelFunctionBinding} implementations. In declaration-only environments (e.g., + * static linters without runtime bindings), this should remain disabled. + */ + @CanIgnoreReturnValue + CelVerifierBuilder setEnableCegarRefinement(boolean enableCegarRefinement); + /** Builds the {@link CelVerifier} instance. */ CelVerifier build(); } diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index 04f3d3476..cae908b3d 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -32,6 +32,7 @@ import dev.cel.common.CelAbstractSyntaxTree; import dev.cel.common.types.CelType; import dev.cel.common.types.CelTypeProvider; +import dev.cel.common.values.CelValueProvider; import dev.cel.optimizer.CelOptimizationException; import dev.cel.optimizer.CelOptimizer; import dev.cel.optimizer.CelOptimizerFactory; @@ -69,10 +70,13 @@ public Optional findType(String typeName) { private final ImmutableSet unknownIdentifiers; private final CelZ3FunctionRegistry functionRegistry; private final CelTypeProvider typeProvider; + private final boolean enableCegarRefinement; @SuppressWarnings("Immutable") // Cel environment is immutable, just not marked as such private final Cel cel; + private final CegarRefiner cegarRefiner; + static Builder newBuilder() { return new Builder(CelFactory.plannerCelBuilder().build()); } @@ -88,6 +92,7 @@ static final class Builder implements CelVerifierBuilder { private final ImmutableList.Builder functionAxioms; private final Cel cel; private CelTypeProvider typeProvider; + private boolean enableCegarRefinement; private Builder(Cel cel) { this.timeout = Duration.ofSeconds(10); @@ -96,6 +101,7 @@ private Builder(Cel cel) { this.functionAxioms = ImmutableList.builder(); this.typeProvider = EMPTY_TYPE_PROVIDER; this.cel = cel; + this.enableCegarRefinement = false; } @Override @@ -130,6 +136,13 @@ public CelVerifierBuilder setComprehensionUnrollLimit(int unrollLimit) { return this; } + @Override + @CanIgnoreReturnValue + public CelVerifierBuilder setEnableCegarRefinement(boolean enableCegarRefinement) { + this.enableCegarRefinement = enableCegarRefinement; + return this; + } + @CanIgnoreReturnValue Builder addFunctionAxioms(CelZ3FunctionAxiom... axioms) { return addFunctionAxioms(Arrays.asList(axioms)); @@ -156,7 +169,8 @@ public CelVerifier build() { unknownIdentifiers.build(), registry, typeProvider, - cel); + cel, + enableCegarRefinement); } } @@ -222,37 +236,53 @@ public CelVerificationResult verifyEquivalence( translator, /* checkTruncation= */ false); + CelValueProvider valueProvider = cel.toCelBuilder().valueProvider(); switch (result.outcome) { case EXACT_MATCH: - return CelVerificationResult.failed( - "Equivalence violation detected.", - getCounterexampleString( + CelCounterexample exactCe = + CelZ3CounterexampleGenerator.extract( ctx, translator.getTypeSystem(), + valueProvider, result.model, /* isApproximate= */ false, - /* isCounterexample= */ true)); + /* isSatisfyingInput= */ false); + return CelVerificationResult.failed("Equivalence violation detected.", exactCe); case APPROXIMATE_MATCH: - return CelVerificationResult.inconclusive( - "Inconclusive: a divergence may exist, but it depends on approximations, missing" - + " theories, or loop bounds.", - getCounterexampleString( + CelCounterexample approxCe = + CelZ3CounterexampleGenerator.extract( ctx, translator.getTypeSystem(), + valueProvider, result.model, /* isApproximate= */ true, - /* isCounterexample= */ true)); - case TRUNCATED: + /* isSatisfyingInput= */ false); + if (enableCegarRefinement) { + CegarRefiner.CegarOutcome cegar = cegarRefiner.refineEquivalence(astA, astB, approxCe); + if (cegar.isViolation()) { + return CelVerificationResult.failed("Equivalence violation detected.", approxCe); + } + if (cegar.evaluationErrorMessage().isPresent()) { + return CelVerificationResult.inconclusive( + "Inconclusive: a divergence may exist, but concrete evaluation produced an error:" + + " " + + cegar.evaluationErrorMessage().get(), + approxCe); + } + } return CelVerificationResult.inconclusive( - "Inconclusive: expressions are equivalent within the current loop unroll limit, but" - + " may diverge for larger collections."); + "Inconclusive: a divergence may exist, but it depends on approximations, missing" + + " theories, or loop bounds.", + approxCe); case NO_MATCH: return CelVerificationResult.verified(); case SOLVER_UNKNOWN: return CelVerificationResult.inconclusive( "Inconclusive: the solver returned unknown status (" + result.reason + ")."); + default: + throw new AssertionError( + "Unexpected or unreachable verification outcome: " + result.outcome); } - throw new AssertionError("Unknown verification outcome: " + result.outcome); } } @@ -312,26 +342,48 @@ CelVerificationResult verifyImplication( translator, /* checkTruncation= */ true); + CelValueProvider valueProvider = cel.toCelBuilder().valueProvider(); switch (result.outcome) { case EXACT_MATCH: - return CelVerificationResult.failed( - String.format("%s violation detected.", subjectName), - getCounterexampleString( + CelCounterexample exactCe = + CelZ3CounterexampleGenerator.extract( ctx, translator.getTypeSystem(), + valueProvider, result.model, /* isApproximate= */ false, - /* isCounterexample= */ true)); + /* isSatisfyingInput= */ false); + return CelVerificationResult.failed( + String.format("%s violation detected.", subjectName), exactCe); case APPROXIMATE_MATCH: - return CelVerificationResult.inconclusive( - "Inconclusive: a counterexample may exist, but it depends on approximations, missing" - + " theories, or loop bounds.", - getCounterexampleString( + CelCounterexample approxCe = + CelZ3CounterexampleGenerator.extract( ctx, translator.getTypeSystem(), + valueProvider, result.model, /* isApproximate= */ true, - /* isCounterexample= */ true)); + /* isSatisfyingInput= */ false); + if (enableCegarRefinement) { + CegarRefiner.CegarOutcome cegar = + cegarRefiner.refineImplication(assumeAst, assertAst, boundSymbols, approxCe); + if (cegar.isViolation()) { + return CelVerificationResult.failed( + String.format("%s violation detected.", subjectName), approxCe); + } + if (cegar.evaluationErrorMessage().isPresent()) { + return CelVerificationResult.inconclusive( + String.format( + "Inconclusive: %s violation candidate found, but concrete evaluation produced" + + " an error: %s", + subjectName, cegar.evaluationErrorMessage().get()), + approxCe); + } + } + return CelVerificationResult.inconclusive( + "Inconclusive: a counterexample may exist, but it depends on approximations, missing" + + " theories, or loop bounds.", + approxCe); case TRUNCATED: return CelVerificationResult.inconclusive( String.format( @@ -376,41 +428,56 @@ private CelVerificationResult checkSatisfiability( translator, /* checkTruncation= */ true); + CelValueProvider valueProvider = cel.toCelBuilder().valueProvider(); switch (result.outcome) { case EXACT_MATCH: + CelCounterexample exactCe = + CelZ3CounterexampleGenerator.extract( + ctx, + translator.getTypeSystem(), + valueProvider, + result.model, + /* isApproximate= */ false, + /* isSatisfyingInput= */ !searchForCounterexample); 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.", exactCe) + : CelVerificationResult.verified("Condition is satisfiable.", exactCe); case APPROXIMATE_MATCH: + CelCounterexample approxCe = + CelZ3CounterexampleGenerator.extract( + ctx, + translator.getTypeSystem(), + valueProvider, + result.model, + /* isApproximate= */ true, + /* isSatisfyingInput= */ !searchForCounterexample); + if (enableCegarRefinement) { + CegarRefiner.CegarOutcome cegar = + cegarRefiner.refineSatisfiability(ast, searchForCounterexample, approxCe); + if (cegar.isViolation()) { + return searchForCounterexample + ? CelVerificationResult.failed("Condition is not always true.", approxCe) + : CelVerificationResult.verified("Condition is satisfiable.", approxCe); + } + if (cegar.evaluationErrorMessage().isPresent()) { + return CelVerificationResult.inconclusive( + (searchForCounterexample + ? "Inconclusive: property may not be always true, but concrete evaluation" + + " produced an error: " + : "Inconclusive: condition may be satisfiable, but concrete evaluation" + + " produced an error: ") + + cegar.evaluationErrorMessage().get(), + approxCe); + } + } String prefix = searchForCounterexample ? "Inconclusive: a counterexample may exist, but it depends on approximations," + " missing theories, or loop bounds." : "Inconclusive: a satisfying model may exist, but it depends on" + " approximations, missing theories, or loop bounds."; - return CelVerificationResult.inconclusive( - prefix, - getCounterexampleString( - ctx, - translator.getTypeSystem(), - result.model, - /* isApproximate= */ true, - /* isCounterexample= */ searchForCounterexample)); + return CelVerificationResult.inconclusive(prefix, approxCe); case TRUNCATED: return CelVerificationResult.inconclusive( @@ -503,29 +570,22 @@ private Solver newSolver(Context ctx) { return solver; } - private static String getCounterexampleString( - Context ctx, - CelZ3TypeSystem typeSystem, - Model model, - boolean isApproximate, - boolean isCounterexample) { - return CelZ3CounterexampleGenerator.generate( - ctx, typeSystem, model, isApproximate, isCounterexample); - } - CelVerifierZ3Impl( Duration timeout, int comprehensionUnrollLimit, ImmutableSet unknownIdentifiers, CelZ3FunctionRegistry functionRegistry, CelTypeProvider typeProvider, - Cel cel) { + Cel cel, + boolean enableCegarRefinement) { this.timeout = timeout; this.comprehensionUnrollLimit = comprehensionUnrollLimit; this.unknownIdentifiers = unknownIdentifiers; this.functionRegistry = functionRegistry; this.typeProvider = typeProvider; this.cel = cel; + this.enableCegarRefinement = enableCegarRefinement; + this.cegarRefiner = new CegarRefiner(cel); } 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 cef976608..27e231bdb 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -15,6 +15,9 @@ package dev.cel.verifier; import com.google.common.base.Preconditions; +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.Context; import com.microsoft.z3.Expr; @@ -23,14 +26,25 @@ import com.microsoft.z3.IntNum; import com.microsoft.z3.Model; import com.microsoft.z3.RatNum; +import dev.cel.common.types.CelType; +import dev.cel.common.types.ListType; +import dev.cel.common.types.MapType; +import dev.cel.common.types.OptionalType; +import dev.cel.common.types.SimpleType; +import dev.cel.common.types.StructTypeReference; +import dev.cel.common.values.CelByteString; +import dev.cel.common.values.CelValueProvider; +import java.time.Duration; +import java.time.Instant; import java.util.ArrayList; 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; -/** Generates human-readable counterexample strings from Z3 models. */ +/** Generates structured counterexamples and human-readable strings from Z3 models. */ @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types. final class CelZ3CounterexampleGenerator { @@ -38,15 +52,18 @@ final class CelZ3CounterexampleGenerator { private CelZ3CounterexampleGenerator() {} - static String generate( + static CelCounterexample extract( Context ctx, CelZ3TypeSystem typeSystem, + CelValueProvider valueProvider, Model model, boolean isApproximate, - boolean isCounterexample) { + boolean isSatisfyingInput) { FuncDecl[] constDecls = model.getConstDecls(); - List bindings = new ArrayList<>(); + ImmutableMap.Builder bindingsBuilder = + ImmutableMap.builder(); + List bindingStrings = 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). @@ -56,106 +73,189 @@ static String generate( } Expr constInterp = model.getConstInterp(decl); if (constInterp != null) { - bindings.add( - String.format("\n %s = %s", name, formatExpr(ctx, typeSystem, model, constInterp))); + ExtractedNode node = extractNode(ctx, typeSystem, valueProvider, model, constInterp); + bindingsBuilder.put( + name, CelCounterexample.Binding.of(name, node.type, node.nativeValue, node.celString)); + bindingStrings.add(String.format("\n %s = %s", name, node.celString)); } } + ImmutableMap bindings = bindingsBuilder.buildOrThrow(); + + String displayString; if (bindings.isEmpty()) { - return isCounterexample - ? " (The expression fails unconditionally, regardless of input state)" - : " (The expression is satisfiable unconditionally, regardless of input state)"; + displayString = + isSatisfyingInput + ? " (The expression is satisfiable unconditionally, regardless of input state)" + : " (The expression fails unconditionally, regardless of input state)"; + } else { + String prefix; + if (isSatisfyingInput) { + prefix = isApproximate ? " Potential satisfying input:" : " Satisfying input:"; + } else { + prefix = isApproximate ? " Potential counterexample input:" : " Counterexample input:"; + } + displayString = prefix + String.join("", bindingStrings); } - String prefix; - if (isCounterexample) { - prefix = isApproximate ? " Potential counterexample input:" : " Counterexample input:"; - } else { - prefix = isApproximate ? " Potential satisfying input:" : " Satisfying input:"; + return CelCounterexample.create(bindings, isApproximate, isSatisfyingInput, displayString); + } + + static final class ExtractedNode { + final CelType type; + final @Nullable Object nativeValue; + final String celString; + + ExtractedNode(CelType type, @Nullable Object nativeValue, String celString) { + this.type = type; + this.nativeValue = nativeValue; + this.celString = celString; } - 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."); - - FuncDecl decl = expr.getFuncDecl(); - - // 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 "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")"; - } else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) { - return "duration('" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "s')"; - } else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) { - return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u"; - } else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) { - return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]); - } else if (decl.equals(typeSystem.stringCons().ConstructorDecl())) { - return expr.getArgs()[0].toString(); - } 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); - } + static ExtractedNode extractNode( + Context ctx, + CelZ3TypeSystem typeSystem, + CelValueProvider valueProvider, + Model model, + Expr expr) { + Preconditions.checkNotNull(expr, "Z3 failed to evaluate the expression natively."); + + if (expr.getArgs().length == 0) { + String consName = expr.getFuncDecl().getName().toString(); + if (consName.equals(CelZ3TypeSystem.CONS_NULL)) { + return new ExtractedNode(SimpleType.NULL_TYPE, null, "null"); } - return doubleArg.toString(); - } else if (decl.equals(typeSystem.listCons().ConstructorDecl())) { - return reconstructList(ctx, typeSystem, model, expr.getArgs()[0]); - } else if (decl.equals(typeSystem.mapCons().ConstructorDecl())) { - return reconstructMap(ctx, typeSystem, model, expr.getArgs()[0]); - } else if (decl.equals(typeSystem.messageCons().ConstructorDecl())) { - return reconstructMessage(ctx, typeSystem, model, expr.getArgs()[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()"; + if (consName.equals(CelZ3TypeSystem.CONS_ERROR)) { + return new ExtractedNode(SimpleType.ERROR, null, "Error"); + } + if (expr.isString()) { + String raw = expr.toString(); + return new ExtractedNode(SimpleType.STRING, unquoteZ3String(raw), raw); + } + if (expr.isTrue() || expr.isFalse()) { + boolean val = expr.isTrue(); + return new ExtractedNode(SimpleType.BOOL, val, Boolean.toString(val)); } + if (expr instanceof IntNum) { + long val = ((IntNum) expr).getInt64(); + return new ExtractedNode(SimpleType.INT, val, Long.toString(val)); + } + if (expr instanceof FPNum || expr instanceof RatNum) { + return decodeDouble(ctx, expr); + } + return new ExtractedNode(SimpleType.DYN, null, expr.toString()); + } + + String consName = expr.getFuncDecl().getName().toString(); + switch (consName) { + case CelZ3TypeSystem.CONS_INT: + long intVal = ((IntNum) expr.getArgs()[0]).getBigInteger().longValue(); + return new ExtractedNode(SimpleType.INT, intVal, Long.toString(intVal)); + case CelZ3TypeSystem.CONS_UINT: + UnsignedLong uVal = UnsignedLong.valueOf(((IntNum) expr.getArgs()[0]).getBigInteger()); + return new ExtractedNode(SimpleType.UINT, uVal, uVal + "u"); + case CelZ3TypeSystem.CONS_BOOL: + boolean boolVal = expr.getArgs()[0].isTrue(); + return new ExtractedNode(SimpleType.BOOL, boolVal, Boolean.toString(boolVal)); + case CelZ3TypeSystem.CONS_STRING: + String strVal = expr.getArgs()[0].toString(); + return new ExtractedNode(SimpleType.STRING, unquoteZ3String(strVal), strVal); + case CelZ3TypeSystem.CONS_BYTES: + String byteVal = expr.getArgs()[0].toString(); + return new ExtractedNode( + SimpleType.BYTES, CelByteString.copyFromUtf8(unquoteZ3String(byteVal)), "b" + byteVal); + case CelZ3TypeSystem.CONS_DOUBLE: + return decodeDouble(ctx, expr.getArgs()[0]); + case CelZ3TypeSystem.CONS_TIMESTAMP: + long tsSeconds = ((IntNum) expr.getArgs()[0]).getBigInteger().longValue(); + return new ExtractedNode( + SimpleType.TIMESTAMP, Instant.ofEpochSecond(tsSeconds), "timestamp(" + tsSeconds + ")"); + case CelZ3TypeSystem.CONS_DURATION: + long durSeconds = ((IntNum) expr.getArgs()[0]).getBigInteger().longValue(); + return new ExtractedNode( + SimpleType.DURATION, Duration.ofSeconds(durSeconds), "duration('" + durSeconds + "s')"); + case CelZ3TypeSystem.CONS_LIST: + return reconstructList(ctx, typeSystem, valueProvider, model, expr.getArgs()[0]); + case CelZ3TypeSystem.CONS_MAP: + return reconstructMap(ctx, typeSystem, valueProvider, model, expr.getArgs()[0]); + case CelZ3TypeSystem.CONS_MESSAGE: + return reconstructMessage(ctx, typeSystem, valueProvider, model, expr.getArgs()[0]); + case CelZ3TypeSystem.CONS_OPTIONAL: + return decodeOptional(ctx, typeSystem, valueProvider, model, expr.getArgs()[0]); + case CelZ3TypeSystem.CONS_UNKNOWN: + return new ExtractedNode(SimpleType.DYN, null, "Unknown"); + default: + return new ExtractedNode(SimpleType.DYN, null, expr.toString()); } + } - return expr.toString(); + static String unquoteZ3String(String raw) { + if (raw.startsWith("\"") && raw.endsWith("\"") && raw.length() >= 2) { + return raw.substring(1, raw.length() - 1).replace("\"\"", "\""); + } + return raw; } - private static String reconstructList( - Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr listRef) { + static ExtractedNode decodeDouble(Context ctx, Expr doubleArg) { + if (doubleArg instanceof FPNum) { + FPNum fpNum = (FPNum) doubleArg; + if (fpNum.isNaN()) { + return new ExtractedNode(SimpleType.DOUBLE, Double.NaN, "NaN"); + } + if (fpNum.isInf()) { + double val = fpNum.isNegative() ? Double.NEGATIVE_INFINITY : Double.POSITIVE_INFINITY; + return new ExtractedNode( + SimpleType.DOUBLE, val, fpNum.isNegative() ? "-Infinity" : "Infinity"); + } + if (fpNum.isZero()) { + double val = fpNum.isNegative() ? -0.0 : 0.0; + return new ExtractedNode(SimpleType.DOUBLE, val, 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 new ExtractedNode(SimpleType.DOUBLE, val, Double.toString(val)); + } + } + return new ExtractedNode(SimpleType.DOUBLE, null, doubleArg.toString()); + } + + static ExtractedNode decodeOptional( + Context ctx, + CelZ3TypeSystem typeSystem, + CelValueProvider valueProvider, + Model model, + Expr optRef) { + 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)); + ExtractedNode valueNode = extractNode(ctx, typeSystem, valueProvider, model, valueExpr); + return new ExtractedNode( + OptionalType.create(valueNode.type), + Optional.ofNullable(valueNode.nativeValue), + "optional(" + valueNode.celString + ")"); + } + return new ExtractedNode( + OptionalType.create(SimpleType.DYN), Optional.empty(), "optional.none()"); + } + + private static ExtractedNode reconstructList( + Context ctx, + CelZ3TypeSystem typeSystem, + CelValueProvider valueProvider, + Model model, + Expr listRef) { Expr lenExpr = evaluateStrict( model, @@ -164,26 +264,43 @@ private static String reconstructList( 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++) { + int printLimit = (int) Math.min(length, MAX_ELEMENTS_TO_PRINT); + List elementStrings = new ArrayList<>(); + ImmutableList.Builder nativeElements = ImmutableList.builder(); + CelType elemType = SimpleType.DYN; + for (int i = 0; i < length; 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)); + ExtractedNode elemNode = extractNode(ctx, typeSystem, valueProvider, model, elem); + if (elemNode.nativeValue != null) { + nativeElements.add(elemNode.nativeValue); + } + if (i < printLimit) { + elementStrings.add(elemNode.celString); + } + elemType = elemNode.type; } if (length > printLimit) { - elements.add("... (" + (length - printLimit) + " more elements)"); + elementStrings.add("... (" + (length - printLimit) + " more elements)"); } - return "[" + String.join(", ", elements) + "]"; + ImmutableList builtList = nativeElements.build(); + Object adaptedList = valueProvider.celValueConverter().toRuntimeValue(builtList); + + return new ExtractedNode( + ListType.create(elemType), adaptedList, "[" + String.join(", ", elementStrings) + "]"); } - private static String reconstructMap( - Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr mapRef) { + static ExtractedNode reconstructMap( + Context ctx, + CelZ3TypeSystem typeSystem, + CelValueProvider valueProvider, + Model model, + Expr mapRef) { Expr lenExpr = evaluateStrict( model, @@ -194,9 +311,12 @@ private static String reconstructMap( long length = ((IntNum) lenExpr).getInt64(); int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT); - List entries = new ArrayList<>(); + List entryStrings = new ArrayList<>(); + ImmutableMap.Builder nativeMap = ImmutableMap.builder(); Set> seenKeys = new HashSet<>(); - for (int i = 0; i < printLimit; i++) { + CelType keyType = SimpleType.DYN; + CelType valType = SimpleType.DYN; + for (int i = 0; i < length; i++) { Expr key = evaluateStrict( model, @@ -217,21 +337,35 @@ private static String reconstructMap( 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)); + ExtractedNode keyNode = extractNode(ctx, typeSystem, valueProvider, model, key); + ExtractedNode valNode = extractNode(ctx, typeSystem, valueProvider, model, value); + if (keyNode.nativeValue != null && valNode.nativeValue != null) { + nativeMap.put(keyNode.nativeValue, valNode.nativeValue); + } + if (entryStrings.size() < printLimit) { + entryStrings.add(keyNode.celString + ": " + valNode.celString); + } + keyType = keyNode.type; + valType = valNode.type; } } if (length > printLimit) { - entries.add("... (" + (length - printLimit) + " more entries)"); + entryStrings.add("... (" + (length - printLimit) + " more entries)"); } - return "{" + String.join(", ", entries) + "}"; + ImmutableMap builtMap = nativeMap.buildOrThrow(); + Object adaptedMap = valueProvider.celValueConverter().toRuntimeValue(builtMap); + + return new ExtractedNode( + MapType.create(keyType, valType), adaptedMap, "{" + String.join(", ", entryStrings) + "}"); } - private static String reconstructMessage( - Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr msgRef) { + static ExtractedNode reconstructMessage( + Context ctx, + CelZ3TypeSystem typeSystem, + CelValueProvider valueProvider, + Model model, + Expr msgRef) { Expr presenceArray = evaluateStrict( model, @@ -244,12 +378,16 @@ private static String reconstructMessage( typeSystem.getMsgTypeName(msgRef), String.format("Z3 failed to evaluate type name natively for msg %s", msgRef)); - String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", ""); + String typeName = + extractNode(ctx, typeSystem, valueProvider, model, typeNameExpr) + .celString + .replace("\"", ""); Set> keys = new LinkedHashSet<>(); extractKeys(presenceArray, keys); - List entries = new ArrayList<>(); + List entryStrings = new ArrayList<>(); + ImmutableMap.Builder fieldMap = ImmutableMap.builder(); for (Expr key : keys) { Expr presence = evaluateStrict( @@ -265,12 +403,35 @@ private static String reconstructMessage( ctx.mkSelect((ArrayExpr) typeSystem.getMsgValues(msgRef), key), String.format("Z3 failed to evaluate msg value for key %s in msg %s", key, msgRef)); - String fieldName = formatExpr(ctx, typeSystem, model, key).replace("\"", ""); - entries.add(fieldName + ": " + formatExpr(ctx, typeSystem, model, value)); + String fieldName = + extractNode(ctx, typeSystem, valueProvider, model, key).celString.replace("\"", ""); + ExtractedNode valNode = extractNode(ctx, typeSystem, valueProvider, model, value); + if (valNode.nativeValue != null) { + fieldMap.put(fieldName, valNode.nativeValue); + } + entryStrings.add(fieldName + ": " + valNode.celString); + } + } + + ImmutableMap builtFieldMap = fieldMap.buildOrThrow(); + Object nativeVal = null; + try { + Optional structVal = valueProvider.newValue(typeName, builtFieldMap); + if (structVal.isPresent()) { + nativeVal = valueProvider.celValueConverter().maybeUnwrap(structVal.get()); } + } catch (IllegalArgumentException | UnsupportedOperationException e) { + // Z3 solver may assign values to non-existent field names for unconstrained message sorts. + nativeVal = null; + } + if (nativeVal == null) { + nativeVal = builtFieldMap; } - return typeName + "{" + String.join(", ", entries) + "}"; + return new ExtractedNode( + StructTypeReference.create(typeName), + nativeVal, + typeName + "{" + String.join(", ", entryStrings) + "}"); } private static void extractKeys(Expr arrayExpr, Set> keys) { diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index dc19a8d3a..d5404d3ab 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -56,50 +56,50 @@ public final class CelZ3TypeSystem { private static final String TYPE_CEL_VALUE = "CelValue"; - private static final String CONS_BOOL = "Bool"; + static final String CONS_BOOL = "Bool"; private static final String IS_BOOL = "isBool"; private static final String GET_BOOL = "getBool"; - private static final String CONS_INT = "Int"; + static final String CONS_INT = "Int"; private static final String IS_INT = "isInt"; private static final String GET_INT = "getInt"; - private static final String CONS_UINT = "Uint"; + static final String CONS_UINT = "Uint"; private static final String IS_UINT = "isUint"; private static final String GET_UINT = "getUint"; - private static final String CONS_DOUBLE = "Double"; + static final String CONS_DOUBLE = "Double"; private static final String IS_DOUBLE = "isDouble"; private static final String GET_DOUBLE = "getDouble"; - private static final String CONS_STRING = "String"; + static final String CONS_STRING = "String"; private static final String IS_STRING = "isString"; private static final String GET_STRING = "getString"; - private static final String CONS_BYTES = "Bytes"; + static final String CONS_BYTES = "Bytes"; private static final String IS_BYTES = "isBytes"; private static final String GET_BYTES = "getBytes"; - private static final String CONS_TIMESTAMP = "Timestamp"; + static final String CONS_TIMESTAMP = "Timestamp"; private static final String IS_TIMESTAMP = "isTimestamp"; private static final String GET_TIMESTAMP = "getTimestamp"; - private static final String CONS_DURATION = "Duration"; + static final String CONS_DURATION = "Duration"; private static final String IS_DURATION = "isDuration"; private static final String GET_DURATION = "getDuration"; - private static final String CONS_ERROR = "CelError"; + static final String CONS_ERROR = "CelError"; private static final String IS_ERROR = "isError"; - private static final String CONS_UNKNOWN = "CelUnknown"; + static final String CONS_UNKNOWN = "CelUnknown"; private static final String IS_UNKNOWN = "isUnknown"; private static final String GET_UNKNOWN = "getUnknownId"; private static final String GENERIC_UNKNOWN_ID = "!generic_unknown"; - private static final String CONS_NULL = "CelNull"; + static final String CONS_NULL = "CelNull"; private static final String IS_NULL = "isNull"; - private static final String CONS_OPTIONAL = "Optional"; + static final String CONS_OPTIONAL = "Optional"; private static final String IS_OPTIONAL = "isOptional"; private static final String SORT_OPTIONAL_REF = "OptionalRef"; @@ -108,13 +108,13 @@ public final class CelZ3TypeSystem { private static final String FUNC_OPT_OF_REF = "!optionalOfRef"; private static final String SORT_LIST_REF = "ListRef"; - private static final String CONS_LIST = "List"; + static final String CONS_LIST = "List"; private static final String IS_LIST = "isList"; private static final String GET_LIST_REF = "getListRef"; private static final String FUNC_AS_SEQ = "as_seq"; private static final String SORT_MAP_REF = "MapRef"; - private static final String CONS_MAP = "Map"; + static final String CONS_MAP = "Map"; private static final String IS_MAP = "isMap"; private static final String GET_MAP_REF = "getMapRef"; @@ -123,7 +123,7 @@ public final class CelZ3TypeSystem { private static final String FUNC_MAP_PRESENCE = "map_presence"; private static final String SORT_MESSAGE_REF = "MessageRef"; - private static final String CONS_MESSAGE = "Message"; + static final String CONS_MESSAGE = "Message"; private static final String IS_MESSAGE = "isMessage"; private static final String GET_MESSAGE_REF = "getMessageRef"; @@ -216,6 +216,7 @@ public Expr mkMessageRefConst(String prefix) { return ctx.mkFreshConst(prefix, messageRefSort); } + /** * Interns and retrieves a Z3 function declaration by name and signature. * diff --git a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel index 55b9c24be..d75bfb827 100644 --- a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel @@ -23,10 +23,14 @@ java_library( "//common:mutable_ast", "//common:operator", "//common:options", + "//common:source_location", "//common/ast", "//common/ast:mutable_expr", "//common/types", "//common/types:message_type_provider", + "//common/types:type_providers", + "//common/values:cel_byte_string", + "//common/values:cel_value_provider", "//compiler:compiler_builder", "//extensions", "//extensions:optional_library", @@ -43,6 +47,8 @@ java_library( "//policy:parser", "//policy:parser_factory", "//policy:validation_exception", + "//runtime:evaluation_exception", + "//runtime:function_binding", "@bazel_tools//tools/java/runfiles", "@maven//:junit_junit", "@maven//:com_google_testparameterinjector_test_parameter_injector", @@ -53,6 +59,7 @@ java_library( "//verifier:numeric_bounds", "//verifier:policy_verifier", "//verifier:policy_verifier_factory", + "//verifier:policy_verifier_impl", "//verifier:type_system", "//verifier:verifier_factory", "//verifier:z3_impl", diff --git a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java index 5a9eaea02..35eadf1d8 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelPolicyVerifierImplTest.java @@ -27,10 +27,12 @@ import dev.cel.common.CelFunctionDecl; import dev.cel.common.CelOptions; import dev.cel.common.CelOverloadDecl; +import dev.cel.common.CelSourceLocation; import dev.cel.common.types.SimpleType; import dev.cel.common.types.StructTypeReference; import dev.cel.expr.conformance.proto3.TestAllTypes; import dev.cel.extensions.CelExtensions; +import dev.cel.extensions.CelOptionalLibrary; import dev.cel.optimizer.CelOptimizer; import dev.cel.optimizer.CelOptimizerFactory; import dev.cel.optimizer.optimizers.SubexpressionOptimizer; @@ -62,7 +64,7 @@ public final class CelPolicyVerifierImplTest { .enableHeterogeneousNumericComparisons(true) .build()) .setStandardMacros(CelStandardMacro.STANDARD_MACROS) - .addCompilerLibraries(CelExtensions.bindings()) + .addCompilerLibraries(CelExtensions.bindings(), CelOptionalLibrary.INSTANCE) .addMessageTypes(TestAllTypes.getDescriptor()) .addVar("x", SimpleType.INT) .addVar("y", SimpleType.INT) @@ -80,7 +82,7 @@ public final class CelPolicyVerifierImplTest { private static final CelPolicyCompiler POLICY_COMPILER = CelPolicyCompilerFactory.newPolicyCompiler(CEL).build(); - private static final CelVerifier AST_VERIFIER = CelVerifierFactory.newVerifier().build(); + private static final CelVerifier AST_VERIFIER = CelVerifierFactory.newVerifier(CEL).build(); private static final CelPolicyVerifier VERIFIER = CelPolicyVerifierFactory.newVerifier(POLICY_COMPILER, AST_VERIFIER).build(); @@ -697,4 +699,687 @@ public void verifyInvariants_boundedSymbolWithApproximation_returnsInconclusive( assertThat(results).containsKey("check_approx"); assertThat(results.get("check_approx").status()).isEqualTo(VerificationStatus.INCONCLUSIVE); } + + @Test + public void verifyInvariants_violation_populatesPolicyDiagnosticWithSnippet() throws Exception { + String yamlPolicy = + "name: secure_access_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: 'port == 80'\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: always_secure\n" + + " assert:\n" + + " - 'rule.result == false'\n"; + CelPolicy policy = PARSER.parse(yamlPolicy); + + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("always_secure"); + CelVerificationResult result = results.get("always_secure"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + + CelPolicyDiagnostic diagnostic = result.policyDiagnostic().get(); + assertThat(diagnostic.invariantId()).isEqualTo("always_secure"); + assertThat(diagnostic.offendingRuleIndex()).isEqualTo(0); + assertThat(diagnostic.issue().getSourceLocation().getLine()).isEqualTo(4); + assertThat(diagnostic.issue().getMessage()) + .isEqualTo( + "Invariant 'always_secure' violated because match[0] matched and evaluated to output:" + + " true"); + + String snippet = diagnostic.toDisplayString(policy.policySource()); + assertThat(snippet).contains("ERROR: :4:7:"); + assertThat(snippet).contains("- condition: 'port == 80'"); + } + + @Test + public void verifyInvariants_shadowedRuleViolation_tracesFiringBranch() throws Exception { + String yamlPolicy = + "name: shadowed_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: 'role == \"admin\"'\n" + + " output: 'false'\n" + + " - condition: 'port == 22'\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: require_port_22_true\n" + + " assume:\n" + + " - 'port == 22'\n" + + " assert:\n" + + " - 'rule.result == true'\n"; + CelPolicy policy = PARSER.parse(yamlPolicy); + + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("require_port_22_true"); + CelVerificationResult result = results.get("require_port_22_true"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + + CelPolicyDiagnostic diagnostic = result.policyDiagnostic().get(); + // Rule 0 fires first under role == "admin" and port == 22, shadowing Rule 1 + assertThat(diagnostic.offendingRuleIndex()).isEqualTo(0); + assertThat(diagnostic.issue().getSourceLocation().getLine()).isEqualTo(4); + } + + @Test + public void verifyInvariants_nestedRuleViolation_tracesNestedLocation() throws Exception { + String yamlPolicy = + "name: nested_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: 'country == \"US\"'\n" + + " rule:\n" + + " match:\n" + + " - condition: 'port == 80'\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: us_port_never_true\n" + + " assume:\n" + + " - 'country == \"US\"'\n" + + " assert:\n" + + " - 'rule.result == false'\n"; + CelPolicy policy = PARSER.parse(yamlPolicy); + + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("us_port_never_true"); + CelVerificationResult result = results.get("us_port_never_true"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + + CelPolicyDiagnostic diagnostic = result.policyDiagnostic().get(); + assertThat(diagnostic.issue().getSourceLocation().getLine()).isEqualTo(7); + } + + @Test + public void verifyInvariants_aggregatePolicy_tracesMatchingBranches() throws Exception { + String yamlPolicy = + "name: aggregate_policy\n" + + "rule:\n" + + " aggregate:\n" + + " - condition: 'port == 80'\n" + + " output: '\"allow\"'\n" + + " - condition: 'role == \"guest\"'\n" + + " output: '\"log\"'\n" + + "verification:\n" + + " invariants:\n" + + " - id: no_log_when_allow\n" + + " assume:\n" + + " - 'port == 80'\n" + + " assert:\n" + + " - '!(\"log\" in rule.result)'\n"; + CelPolicy policy = PARSER.parse(yamlPolicy); + + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("no_log_when_allow"); + CelVerificationResult result = results.get("no_log_when_allow"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + + CelPolicyDiagnostic diagnostic = result.policyDiagnostic().get(); + assertThat(diagnostic.offendingRuleIndex()).isEqualTo(0); + assertThat(diagnostic.issue().getMessage()) + .contains("because match[0] matched and evaluated to output: [allow, log]"); + assertThat(result.counterexampleModel()).isPresent(); + assertThat(result.counterexampleModel().get().bindings().get("port").celString()) + .isEqualTo("80"); + assertThat(result.counterexampleModel().get().bindings().get("role").celString()) + .isEqualTo("\"guest\""); + } + + @Test + public void verifyInvariants_namedAggregatePolicy_diagnosticIncludesRuleNameAndAggregatedOutputs() + throws Exception { + String yamlPolicy = + "name: named_aggregate_policy\n" + + "rule:\n" + + " id: egress_rules\n" + + " aggregate:\n" + + " - condition: 'port == 80'\n" + + " output: '\"allow\"'\n" + + " - condition: 'role == \"guest\"'\n" + + " output: '\"rate_limit\"'\n" + + "verification:\n" + + " invariants:\n" + + " - id: no_rate_limit_on_http\n" + + " assume:\n" + + " - 'port == 80'\n" + + " assert:\n" + + " - '!(\"rate_limit\" in rule.result)'\n"; + CelPolicy policy = PARSER.parse(yamlPolicy); + + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("no_rate_limit_on_http"); + CelVerificationResult result = results.get("no_rate_limit_on_http"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + + CelPolicyDiagnostic diagnostic = result.policyDiagnostic().get(); + assertThat(diagnostic.offendingRuleName()).hasValue("egress_rules"); + assertThat(diagnostic.offendingRuleIndex()).isEqualTo(0); + assertThat(diagnostic.issue().getMessage()) + .contains( + "because rule 'egress_rules' matched and evaluated to output: [allow, rate_limit]"); + + String snippet = diagnostic.toDisplayString(policy.policySource()); + assertThat(snippet).contains("ERROR: :5:7:"); + assertThat(snippet).contains("- condition: 'port == 80'"); + } + + @Test + public void verifyInvariants_aggregatePolicy_noMatchingBranches_omitsDiagnostic() + throws Exception { + String yamlPolicy = + "name: empty_aggregate_policy\n" + + "rule:\n" + + " aggregate:\n" + + " - condition: 'port == 80'\n" + + " output: '\"allow\"'\n" + + "verification:\n" + + " invariants:\n" + + " - id: must_match_something\n" + + " assume:\n" + + " - 'port == 443'\n" + + " assert:\n" + + " - 'size(rule.result) > 0'\n"; + CelPolicy policy = PARSER.parse(yamlPolicy); + + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("must_match_something"); + CelVerificationResult result = results.get("must_match_something"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isEmpty(); + } + + @Test + public void verifyEquivalence_divergence_populatesDualSourceDiagnostic() throws Exception { + String yamlPolicyA = + "name: workload_v1\n" + + "rule:\n" + + " match:\n" + + " - condition: 'port == 80 && role == \"admin\"'\n" + + " output: 'true'\n" + + " - output: 'false'\n"; + String yamlPolicyB = + "name: workload_v2\n" + + "rule:\n" + + " match:\n" + + " - condition: 'port == 80'\n" + + " output: 'false'\n" + + " - output: 'true'\n"; + + CelPolicy policyA = PARSER.parse(yamlPolicyA); + CelPolicy policyB = PARSER.parse(yamlPolicyB); + + CelVerificationResult result = VERIFIER.verifyEquivalence(policyA, policyB); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyEquivalenceDiagnostic()).isPresent(); + + CelPolicyEquivalenceDiagnostic equivDiag = result.policyEquivalenceDiagnostic().get(); + assertThat(equivDiag.policyABranch().policyName()).isEqualTo("workload_v1"); + assertThat(equivDiag.policyABranch().issue().getSourceLocation().getLine()).isAtLeast(4); + + assertThat(equivDiag.policyBBranch().policyName()).isEqualTo("workload_v2"); + assertThat(equivDiag.policyBBranch().issue().getSourceLocation().getLine()).isAtLeast(4); + assertThat(equivDiag.policyABranch().evaluatedOutput()) + .isNotEqualTo(equivDiag.policyBBranch().evaluatedOutput()); + + String display = equivDiag.toDisplayString(policyA.policySource(), policyB.policySource()); + assertThat(display).contains("[Policy A: workload_v1]"); + assertThat(display).contains("[Policy B: workload_v2]"); + } + + @Test + public void verifyEquivalence_ruleOrderDivergence_tracesDifferentRuleIndices() throws Exception { + String yamlPolicyA = + "name: order_v1\n" + + "rule:\n" + + " match:\n" + + " - condition: 'role == \"admin\"'\n" + + " output: '\"ADMIN\"'\n" + + " - condition: 'port == 80'\n" + + " output: '\"HTTP\"'\n" + + " - output: '\"UNKNOWN\"'\n"; + String yamlPolicyB = + "name: order_v2\n" + + "rule:\n" + + " match:\n" + + " - condition: 'port == 80'\n" + + " output: '\"HTTP\"'\n" + + " - condition: 'role == \"admin\"'\n" + + " output: '\"ADMIN\"'\n" + + " - output: '\"UNKNOWN\"'\n"; + + CelPolicy policyA = PARSER.parse(yamlPolicyA); + CelPolicy policyB = PARSER.parse(yamlPolicyB); + + CelVerificationResult result = VERIFIER.verifyEquivalence(policyA, policyB); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyEquivalenceDiagnostic()).isPresent(); + + CelPolicyEquivalenceDiagnostic equivDiag = result.policyEquivalenceDiagnostic().get(); + // Under role == "admin" && port == 80: Policy A fires rule 0, Policy B fires rule 0 (with + // different outputs) + assertThat(equivDiag.policyABranch().evaluatedOutput()).isEqualTo("ADMIN"); + assertThat(equivDiag.policyBBranch().evaluatedOutput()).isEqualTo("HTTP"); + } + + @Test + public void verifyInvariants_namedRule_diagnosticIncludesRuleName() throws Exception { + String yamlPolicy = + "name: named_rule_policy\n" + + "rule:\n" + + " id: authz_gate\n" + + " match:\n" + + " - condition: 'port == 80'\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: always_deny\n" + + " assert:\n" + + " - 'rule.result == false'\n"; + + CelPolicy policy = PARSER.parse(yamlPolicy); + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("always_deny"); + CelVerificationResult result = results.get("always_deny"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + + CelPolicyDiagnostic diagnostic = result.policyDiagnostic().get(); + assertThat(diagnostic.offendingRuleName()).hasValue("authz_gate"); + assertThat(diagnostic.offendingRuleIndex()).isEqualTo(0); + assertThat(diagnostic.issue().getMessage()) + .contains("because rule 'authz_gate' matched and evaluated to output: true"); + } + + @Test + public void verifyEquivalence_namedRules_diagnosticIncludesRuleNames() throws Exception { + String yamlPolicyA = + "name: named_v1\n" + + "rule:\n" + + " id: v1_gate\n" + + " match:\n" + + " - condition: 'port == 80'\n" + + " output: 'true'\n" + + " - output: 'false'\n"; + String yamlPolicyB = + "name: named_v2\n" + + "rule:\n" + + " id: v2_gate\n" + + " match:\n" + + " - condition: 'port == 80'\n" + + " output: 'false'\n" + + " - output: 'true'\n"; + + CelPolicy policyA = PARSER.parse(yamlPolicyA); + CelPolicy policyB = PARSER.parse(yamlPolicyB); + + CelVerificationResult result = VERIFIER.verifyEquivalence(policyA, policyB); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyEquivalenceDiagnostic()).isPresent(); + + CelPolicyEquivalenceDiagnostic equivDiag = result.policyEquivalenceDiagnostic().get(); + assertThat(equivDiag.policyABranch().ruleName()).hasValue("v1_gate"); + assertThat(equivDiag.policyBBranch().ruleName()).hasValue("v2_gate"); + assertThat(equivDiag.toCelIssues()).hasSize(2); + } + + @Test + public void verifyInvariants_ruleWithVariables_tracesWithVariableResolution() throws Exception { + String yamlPolicy = + "name: var_policy\n" + + "rule:\n" + + " variables:\n" + + " - is_http: 'port == 80'\n" + + " match:\n" + + " - condition: 'variables.is_http'\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: never_http\n" + + " assume:\n" + + " - 'port == 80'\n" + + " assert:\n" + + " - 'rule.result == false'\n"; + + CelPolicy policy = PARSER.parse(yamlPolicy); + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("never_http"); + CelVerificationResult result = results.get("never_http"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + assertThat(result.policyDiagnostic().get().offendingRuleIndex()).isEqualTo(0); + assertThat(result.policyDiagnostic().get().issue().getMessage()) + .contains("matched and evaluated to output: true"); + } + + @Test + public void verifyInvariants_outputEvaluationError_diagnosticCapturesErrorString() + throws Exception { + String yamlPolicy = + "name: error_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: 'port == 80'\n" + + " output: '10 / (port - 80)'\n" + + " - output: '0'\n" + + "verification:\n" + + " invariants:\n" + + " - id: never_error\n" + + " assume:\n" + + " - 'port == 80'\n" + + " assert:\n" + + " - 'rule.result == 0'\n"; + + CelPolicy policy = PARSER.parse(yamlPolicy); + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("never_error"); + CelVerificationResult result = results.get("never_error"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + assertThat(result.policyDiagnostic().get().issue().getMessage()).contains(" policyVerifier.verifyInvariants(policy)); + } + + @Test + public void verifyInvariants_conditionEvaluationError_fallsThroughToNextRule() throws Exception { + String yamlPolicy = + "name: cond_error_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: '10 / port == 1'\n" // Division by zero when port == 0 + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: never_true_on_zero\n" + + " assume:\n" + + " - 'port == 0'\n" + + " assert:\n" + + " - 'rule.result == true'\n"; + + CelPolicy policy = PARSER.parse(yamlPolicy); + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("never_true_on_zero"); + CelVerificationResult result = results.get("never_true_on_zero"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + // Rule 0 errored on evaluation, so Rule 1 (index 1) fired with false + assertThat(result.policyDiagnostic().get().offendingRuleIndex()).isEqualTo(1); + } + + @Test + public void verifyInvariants_variableEvaluationError_fallsThroughGracefully() throws Exception { + String yamlPolicy = + "name: var_error_policy\n" + + "rule:\n" + + " variables:\n" + + " - err_var: '10 / port'\n" + + " match:\n" + + " - condition: 'port == 80'\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: deny_on_zero\n" + + " assume:\n" + + " - 'port == 80'\n" + + " assert:\n" + + " - 'rule.result == false'\n"; + + CelPolicy policy = PARSER.parse(yamlPolicy); + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("deny_on_zero"); + CelVerificationResult result = results.get("deny_on_zero"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + assertThat(result.policyDiagnostic().get().offendingRuleIndex()).isEqualTo(0); + } + + @Test + public void verifyInvariants_nestedRuleFallthrough_continuesOuterRules() throws Exception { + String yamlPolicy = + "name: nested_fallthrough_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: 'port == 80'\n" + + " rule:\n" + + " match:\n" + + " - condition: 'role == \"admin\"'\n" + + " output: '\"ADMIN\"'\n" + + " - output: '\"FALLTHROUGH\"'\n" + + "verification:\n" + + " invariants:\n" + + " - id: port_443_never_fallthrough\n" + + " assume:\n" + + " - 'port == 443'\n" + + " assert:\n" + + " - 'rule.result != optional.of(\"FALLTHROUGH\")'\n"; + + CelPolicy policy = PARSER.parse(yamlPolicy); + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("port_443_never_fallthrough"); + CelVerificationResult result = results.get("port_443_never_fallthrough"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + assertThat(result.policyDiagnostic().get().offendingRuleIndex()).isEqualTo(1); + assertThat(result.policyDiagnostic().get().issue().getMessage()) + .contains("output: FALLTHROUGH"); + } + + @Test + public void verifyInvariants_aggregateOutputEvaluationError_capturesErrorInAggregateList() + throws Exception { + String yamlPolicy = + "name: aggregate_error_policy\n" + + "rule:\n" + + " aggregate:\n" + + " - condition: 'port == 0'\n" + + " output: '10 / port'\n" + + "verification:\n" + + " invariants:\n" + + " - id: never_error\n" + + " assume:\n" + + " - 'port == 0'\n" + + " assert:\n" + + " - 'size(rule.result) == 0'\n"; + + CelPolicy policy = PARSER.parse(yamlPolicy); + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("never_error"); + CelVerificationResult result = results.get("never_error"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + assertThat(result.policyDiagnostic().get().issue().getMessage()).contains(" results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("no_second_on_zero"); + CelVerificationResult result = results.get("no_second_on_zero"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + assertThat(result.policyDiagnostic().get().issue().getMessage()).contains("[second]"); + } + + @Test + public void verifyInvariants_firstMatchConditionError_fallsThroughToFiringMatch() + throws Exception { + String yamlPolicy = + "name: first_match_cond_error_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: '10 / port == 1'\n" // Division by zero when port == 0 + + " output: '\"first\"'\n" + + " - condition: 'port == 0'\n" + + " output: '\"second\"'\n" + + " - output: '\"fallback\"'\n" + + "verification:\n" + + " invariants:\n" + + " - id: no_second_on_zero\n" + + " assume:\n" + + " - 'port == 0'\n" + + " assert:\n" + + " - 'rule.result != \"second\"'\n"; + + CelPolicy policy = PARSER.parse(yamlPolicy); + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("no_second_on_zero"); + CelVerificationResult result = results.get("no_second_on_zero"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + // Primary match (match[1]) matched, so it attributes to match[1] rather than condition error + assertThat(result.policyDiagnostic().get().offendingRuleIndex()).isEqualTo(1); + assertThat(result.policyDiagnostic().get().issue().getMessage()).contains("second"); + } + + @Test + public void + verifyInvariants_conditionEvaluationError_noSubsequentMatch_attributesToErroredCondition() + throws Exception { + String yamlPolicy = + "name: cond_error_no_match_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: '10 / port == 1'\n" // Division by zero when port == 0 + + " output: '\"first\"'\n" + + "verification:\n" + + " invariants:\n" + + " - id: must_match_something\n" + + " assume:\n" + + " - 'port == 0'\n" + + " assert:\n" + + " - 'rule.result == optional.of(\"first\")'\n"; + + CelPolicy policy = PARSER.parse(yamlPolicy); + ImmutableMap results = VERIFIER.verifyInvariants(policy); + + assertThat(results).containsKey("must_match_something"); + CelVerificationResult result = results.get("must_match_something"); + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.policyDiagnostic()).isPresent(); + // No subsequent match fires, so diagnostic pinpoints match[0] condition failure + assertThat(result.policyDiagnostic().get().offendingRuleIndex()).isEqualTo(0); + assertThat(result.policyDiagnostic().get().issue().getMessage()).contains(" "hash_" + s)) + .addVar("token", SimpleType.STRING) + .build(); + + CelAbstractSyntaxTree ast = + cel.compile("token == 'admin' ? customHash(token) != 'hash_admin' : true").getAst(); + + // Pure SMT verifier without CEGAR returns INCONCLUSIVE + CelVerifier verifierWithoutCegar = CelVerifierFactory.newVerifier(cel).build(); + CelVerificationResult resultWithoutCegar = verifierWithoutCegar.isAlwaysTrue(ast); + assertThat(resultWithoutCegar.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + + // Verifier with CEGAR refinement enabled evaluates candidate model concretely and proves + // violation + CelVerifier verifierWithCegar = + CelVerifierFactory.newVerifier(cel).setEnableCegarRefinement(true).build(); + CelVerificationResult resultWithCegar = verifierWithCegar.isAlwaysTrue(ast); + assertThat(resultWithCegar.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(resultWithCegar.counterexampleModel()).isPresent(); + assertThat(resultWithCegar.counterexampleModel().get().get("token")) + .hasValue(Binding.of("token", SimpleType.STRING, "admin", "\"admin\"")); + } + + @Test + public void cegarRefinement_equivalence_upgradesInconclusiveToViolated() throws Exception { + CelFunctionDecl customHash = + CelFunctionDecl.newFunctionDeclaration( + "customHash", + CelOverloadDecl.newGlobalOverload( + "customHash_string", SimpleType.STRING, SimpleType.STRING)); + Cel cel = + CelFactory.plannerCelBuilder() + .addFunctionDeclarations(customHash) + .addFunctionBindings( + CelFunctionBinding.from( + "customHash_string", String.class, (String s) -> "hash_" + s)) + .addVar("token", SimpleType.STRING) + .build(); + + CelAbstractSyntaxTree astA = + cel.compile("token == 'admin' && customHash(token) == 'hash_admin'").getAst(); + CelAbstractSyntaxTree astB = cel.compile("false").getAst(); + + // Pure SMT verifier without CEGAR returns INCONCLUSIVE because customHash is unmodeled + CelVerifier verifierWithoutCegar = CelVerifierFactory.newVerifier(cel).build(); + CelVerificationResult resultWithoutCegar = verifierWithoutCegar.verifyEquivalence(astA, astB); + assertThat(resultWithoutCegar.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + + // Verifier with CEGAR refinement enabled evaluates candidate model concretely and proves + // divergence + CelVerifier verifierWithCegar = + CelVerifierFactory.newVerifier(cel).setEnableCegarRefinement(true).build(); + CelVerificationResult resultWithCegar = verifierWithCegar.verifyEquivalence(astA, astB); + assertThat(resultWithCegar.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(resultWithCegar.counterexampleModel()).isPresent(); + assertThat(resultWithCegar.counterexampleModel().get().get("token")) + .hasValue(Binding.of("token", SimpleType.STRING, "admin", "\"admin\"")); + } + + @Test + public void cegarRefinement_implication_upgradesInconclusiveToViolated() throws Exception { + CelFunctionDecl customHash = + CelFunctionDecl.newFunctionDeclaration( + "customHash", + CelOverloadDecl.newGlobalOverload( + "customHash_string", SimpleType.STRING, SimpleType.STRING)); + Cel cel = + CelFactory.plannerCelBuilder() + .addFunctionDeclarations(customHash) + .addFunctionBindings( + CelFunctionBinding.from( + "customHash_string", String.class, (String s) -> "hash_" + s)) + .addVar("token", SimpleType.STRING) + .build(); + + CelAbstractSyntaxTree assumeAst = cel.compile("token == 'admin'").getAst(); + CelAbstractSyntaxTree assertAst = cel.compile("customHash(token) != 'hash_admin'").getAst(); + + // Pure SMT verifier without CEGAR returns INCONCLUSIVE + CelVerifierZ3Impl verifierWithoutCegar = + (CelVerifierZ3Impl) CelVerifierFactory.newVerifier(cel).build(); + CelVerificationResult resultWithoutCegar = + verifierWithoutCegar.verifyImplication( + assumeAst, assertAst, ImmutableMap.of(), "Condition"); + assertThat(resultWithoutCegar.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + + // Verifier with CEGAR refinement enabled evaluates candidate model concretely and proves + // violation + CelVerifierZ3Impl verifierWithCegar = + (CelVerifierZ3Impl) + CelVerifierFactory.newVerifier(cel).setEnableCegarRefinement(true).build(); + CelVerificationResult resultWithCegar = + verifierWithCegar.verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Condition"); + assertThat(resultWithCegar.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(resultWithCegar.counterexampleModel()).isPresent(); + assertThat(resultWithCegar.counterexampleModel().get().get("token")) + .hasValue(Binding.of("token", SimpleType.STRING, "admin", "\"admin\"")); + } + + @Test + public void cegarRefinement_implication_spuriousCounterexample_remainsInconclusive() + throws Exception { + CelFunctionDecl customHash = + CelFunctionDecl.newFunctionDeclaration( + "customHash", + CelOverloadDecl.newGlobalOverload( + "customHash_string", SimpleType.STRING, SimpleType.STRING)); + Cel cel = + CelFactory.plannerCelBuilder() + .addFunctionDeclarations(customHash) + .addFunctionBindings( + CelFunctionBinding.from( + "customHash_string", String.class, (String s) -> "hash_" + s)) + .addVar("token", SimpleType.STRING) + .build(); + + // The implication token == 'admin' ==> customHash(token) == 'hash_admin' is mathematically + // true. + // Pure SMT without customHash theory finds a spurious counterexample model, which CEGAR + // refutes. + CelAbstractSyntaxTree assumeAst = cel.compile("token == 'admin'").getAst(); + CelAbstractSyntaxTree assertAst = cel.compile("customHash(token) == 'hash_admin'").getAst(); + + CelVerifierZ3Impl verifierWithCegar = + (CelVerifierZ3Impl) + CelVerifierFactory.newVerifier(cel).setEnableCegarRefinement(true).build(); + CelVerificationResult result = + verifierWithCegar.verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Condition"); + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + } + + @Test + public void cegarRefinement_equivalence_spuriousCounterexample_remainsInconclusive() + throws Exception { + CelFunctionDecl customHash = + CelFunctionDecl.newFunctionDeclaration( + "customHash", + CelOverloadDecl.newGlobalOverload( + "customHash_string", SimpleType.STRING, SimpleType.STRING)); + Cel cel = + CelFactory.plannerCelBuilder() + .addFunctionDeclarations(customHash) + .addFunctionBindings( + CelFunctionBinding.from( + "customHash_string", String.class, (String s) -> "hash_" + s)) + .addVar("token", SimpleType.STRING) + .build(); + + // customHash(token) == 'hash_admin' and token == 'admin' are semantically equivalent. + // Pure SMT finds a spurious divergence model, which CEGAR refutes upon concrete evaluation. + CelAbstractSyntaxTree astA = cel.compile("customHash(token) == 'hash_admin'").getAst(); + CelAbstractSyntaxTree astB = cel.compile("token == 'admin'").getAst(); + + CelVerifier verifierWithCegar = + CelVerifierFactory.newVerifier(cel).setEnableCegarRefinement(true).build(); + CelVerificationResult result = verifierWithCegar.verifyEquivalence(astA, astB); + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + } + + @Test + public void cegarRefinement_equivalence_evaluationException_returnsInconclusiveWithErrorMessage() + throws Exception { + CelFunctionDecl customFailing = + CelFunctionDecl.newFunctionDeclaration( + "customFailing", + CelOverloadDecl.newGlobalOverload( + "customFailing_string", SimpleType.STRING, SimpleType.STRING)); + Cel cel = + CelFactory.plannerCelBuilder() + .addFunctionDeclarations(customFailing) + .addFunctionBindings( + CelFunctionBinding.from( + "customFailing_string", + String.class, + (String s) -> { + throw new CelEvaluationException("Custom runtime failure for " + s); + })) + .addVar("token", SimpleType.STRING) + .build(); + + CelAbstractSyntaxTree astA = cel.compile("customFailing(token) == 'expected'").getAst(); + CelAbstractSyntaxTree astB = cel.compile("token == 'expected'").getAst(); + + CelVerifier verifierWithCegar = + CelVerifierFactory.newVerifier(cel).setEnableCegarRefinement(true).build(); + CelVerificationResult result = verifierWithCegar.verifyEquivalence(astA, astB); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + assertThat(result.message()).contains("concrete evaluation produced an error:"); + assertThat(result.message()).contains("Custom runtime failure"); + assertThat(result.counterexampleModel()).isPresent(); + } + + @Test + public void cegarRefinement_isAlwaysTrue_evaluationException_returnsInconclusiveWithErrorMessage() + throws Exception { + CelFunctionDecl customFailing = + CelFunctionDecl.newFunctionDeclaration( + "customFailing", + CelOverloadDecl.newGlobalOverload( + "customFailing_string", SimpleType.STRING, SimpleType.STRING)); + Cel cel = + CelFactory.plannerCelBuilder() + .addFunctionDeclarations(customFailing) + .addFunctionBindings( + CelFunctionBinding.from( + "customFailing_string", + String.class, + (String s) -> { + throw new CelEvaluationException("Custom runtime failure for " + s); + })) + .addVar("token", SimpleType.STRING) + .build(); + + CelAbstractSyntaxTree ast = cel.compile("customFailing(token) == 'expected'").getAst(); + + CelVerifier verifierWithCegar = + CelVerifierFactory.newVerifier(cel).setEnableCegarRefinement(true).build(); + CelVerificationResult result = verifierWithCegar.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + assertThat(result.message()).contains("concrete evaluation produced an error:"); + assertThat(result.message()).contains("Custom runtime failure"); + assertThat(result.counterexampleModel()).isPresent(); + } + + @Test + public void cegarRefinement_protoMessage_upgradesInconclusiveToViolated() throws Exception { + CelFunctionDecl customHash = + CelFunctionDecl.newFunctionDeclaration( + "customHash", + CelOverloadDecl.newGlobalOverload( + "customHash_string", SimpleType.STRING, SimpleType.STRING)); + Cel cel = + CelFactory.plannerCelBuilder() + .setContainer(CelContainer.ofName("cel.expr.conformance.proto3")) + .addMessageTypes(TestAllTypes.getDescriptor()) + .setTypeProvider(TYPE_PROVIDER) + .addFunctionDeclarations(customHash) + .addFunctionBindings( + CelFunctionBinding.from( + "customHash_string", String.class, (String s) -> "hash_" + s)) + .addVar("msg", StructTypeReference.create(TestAllTypes.getDescriptor().getFullName())) + .build(); + + CelAbstractSyntaxTree ast = + cel.compile( + "msg == TestAllTypes{single_string: 'admin'} ? customHash(msg.single_string) !=" + + " 'hash_admin' : true") + .getAst(); + + CelVerifier verifierWithCegar = + CelVerifierFactory.newVerifier(cel) + .setTypeProvider(TYPE_PROVIDER) + .setEnableCegarRefinement(true) + .build(); + CelVerificationResult resultWithCegar = verifierWithCegar.isAlwaysTrue(ast); + assertWithMessage(resultWithCegar.message()) + .that(resultWithCegar.status()) + .isEqualTo(VerificationStatus.VIOLATED); + assertThat(resultWithCegar.counterexampleModel()).isPresent(); + CelCounterexample ce = resultWithCegar.counterexampleModel().get(); + assertThat(ce.get("msg")).isPresent(); + assertThat(ce.get("msg").get().nativeValue().orElse(null)).isInstanceOf(TestAllTypes.class); + TestAllTypes proto = (TestAllTypes) ce.get("msg").get().nativeValue().get(); + assertThat(proto.getSingleString()).isEqualTo("admin"); + } + + @Test + public void cegarRefinement_implication_evaluationException_returnsInconclusiveWithErrorMessage() + throws Exception { + CelFunctionDecl customFailing = + CelFunctionDecl.newFunctionDeclaration( + "customFailing", + CelOverloadDecl.newGlobalOverload( + "customFailing_string", SimpleType.STRING, SimpleType.STRING)); + Cel cel = + CelFactory.plannerCelBuilder() + .addFunctionDeclarations(customFailing) + .addFunctionBindings( + CelFunctionBinding.from( + "customFailing_string", + String.class, + (String s) -> { + throw new CelEvaluationException("Implication runtime failure for " + s); + })) + .addVar("token", SimpleType.STRING) + .build(); + + CelAbstractSyntaxTree assumeAst = cel.compile("token == 'admin'").getAst(); + CelAbstractSyntaxTree assertAst = cel.compile("customFailing(token) != 'expected'").getAst(); + + CelVerifierZ3Impl verifierWithCegar = + (CelVerifierZ3Impl) + CelVerifierFactory.newVerifier(cel).setEnableCegarRefinement(true).build(); + CelVerificationResult result = + verifierWithCegar.verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Condition"); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + assertThat(result.message()).contains("concrete evaluation produced an error:"); + assertThat(result.message()).contains("Implication runtime failure for admin"); + assertThat(result.counterexampleModel()).isPresent(); + } + + @Test + public void cegarRefinement_implication_withBoundSymbols_evaluatesBoundSymbolsInRefinement() + throws Exception { + CelFunctionDecl customHash = + CelFunctionDecl.newFunctionDeclaration( + "customHash", + CelOverloadDecl.newGlobalOverload( + "customHash_string", SimpleType.STRING, SimpleType.STRING)); + Cel cel = + CelFactory.plannerCelBuilder() + .addFunctionDeclarations(customHash) + .addFunctionBindings( + CelFunctionBinding.from( + "customHash_string", String.class, (String s) -> "hash_" + s)) + .addVar("token", SimpleType.STRING) + .addVar("computed", SimpleType.STRING) + .build(); + + CelAbstractSyntaxTree assumeAst = cel.compile("token == 'admin'").getAst(); + CelAbstractSyntaxTree assertAst = cel.compile("computed != 'hash_admin'").getAst(); + CelAbstractSyntaxTree boundExpr = cel.compile("customHash(token)").getAst(); + ImmutableMap boundSymbols = + ImmutableMap.of("computed", boundExpr); + + CelVerifierZ3Impl verifierWithCegar = + (CelVerifierZ3Impl) + CelVerifierFactory.newVerifier(cel).setEnableCegarRefinement(true).build(); + CelVerificationResult result = + verifierWithCegar.verifyImplication(assumeAst, assertAst, boundSymbols, "BoundCondition"); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.counterexampleModel()).isPresent(); + assertThat(result.counterexampleModel().get().get("token")) + .hasValue(Binding.of("token", SimpleType.STRING, "admin", "\"admin\"")); + } + + @Test + public void cegarRefinement_zeroArityFunction_isViolation() throws Exception { + CelFunctionDecl zeroArityFn = + CelFunctionDecl.newFunctionDeclaration( + "customConstant", + CelOverloadDecl.newGlobalOverload("customConstant_void", SimpleType.DYN)); + Cel cel = + CelFactory.plannerCelBuilder() + .addFunctionDeclarations(zeroArityFn) + .addFunctionBindings( + CelFunctionBinding.from("customConstant_void", ImmutableList.of(), unused -> 42L)) + .build(); + + CelAbstractSyntaxTree ast = cel.compile("customConstant() == 1").getAst(); + CelVerifier verifierWithCegar = + CelVerifierFactory.newVerifier(cel).setEnableCegarRefinement(true).build(); + + CelVerificationResult result = verifierWithCegar.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + } +} diff --git a/verifier/src/test/java/dev/cel/verifier/CelZ3CounterexampleGeneratorTest.java b/verifier/src/test/java/dev/cel/verifier/CelZ3CounterexampleGeneratorTest.java new file mode 100644 index 000000000..233ca46ed --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/CelZ3CounterexampleGeneratorTest.java @@ -0,0 +1,871 @@ +// 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 static com.google.common.truth.Truth.assertThat; + +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import com.google.common.primitives.UnsignedLong; +import com.google.testing.junit.testparameterinjector.TestParameterInjector; +// import com.google.testing.testsize.MediumTest; +import com.microsoft.z3.ArrayExpr; +import com.microsoft.z3.Context; +import com.microsoft.z3.Expr; +import com.microsoft.z3.FuncDecl; +import com.microsoft.z3.Model; +import com.microsoft.z3.Solver; +import com.microsoft.z3.Sort; +import com.microsoft.z3.Status; +import com.microsoft.z3.UninterpretedSort; +import dev.cel.bundle.Cel; +import dev.cel.bundle.CelFactory; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.CelContainer; +import dev.cel.common.types.CelTypeProvider; +import dev.cel.common.types.ListType; +import dev.cel.common.types.MapType; +import dev.cel.common.types.OptionalType; +import dev.cel.common.types.ProtoMessageTypeProvider; +import dev.cel.common.types.SimpleType; +import dev.cel.common.types.StructTypeReference; +import dev.cel.common.values.CelByteString; +import dev.cel.common.values.CelValueProvider; +import dev.cel.expr.conformance.proto3.TestAllTypes; +import dev.cel.extensions.CelOptionalLibrary; +import dev.cel.verifier.CelCounterexample.Binding; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import java.time.Duration; +import java.time.Instant; +import java.util.Optional; +import org.junit.Test; +import org.junit.runner.RunWith; + +// @MediumTest +@RunWith(TestParameterInjector.class) +public final class CelZ3CounterexampleGeneratorTest { + + private static final CelTypeProvider TYPE_PROVIDER = + ProtoMessageTypeProvider.newBuilder() + .addDescriptors(ImmutableList.of(TestAllTypes.getDescriptor())) + .build(); + + @Test + public void structuredCounterexample_primitiveTypes() throws Exception { + Cel cel = + CelFactory.plannerCelBuilder() + .addVar("i", SimpleType.INT) + .addVar("u", SimpleType.UINT) + .addVar("d", SimpleType.DOUBLE) + .addVar("b", SimpleType.BOOL) + .addVar("s", SimpleType.STRING) + .addVar("bytes_val", SimpleType.BYTES) + .addVar("ts", SimpleType.TIMESTAMP) + .addVar("dur", SimpleType.DURATION) + .build(); + CelAbstractSyntaxTree ast = + cel.compile( + "i == -42 && u == 100u && d == 3.14 && b == true && s == 'admin' && bytes_val ==" + + " b'foo' && ts == timestamp(1767225600) && dur == (timestamp(10) -" + + " timestamp(0))") + .getAst(); + + CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); + CelVerificationResult result = verifier.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.counterexampleModel()).isPresent(); + CelCounterexample ce = result.counterexampleModel().get(); + + assertThat(ce.get("i")).hasValue(Binding.of("i", SimpleType.INT, -42L, "-42")); + assertThat(ce.get("u")) + .hasValue(Binding.of("u", SimpleType.UINT, UnsignedLong.fromLongBits(100), "100u")); + assertThat(ce.get("d")).hasValue(Binding.of("d", SimpleType.DOUBLE, 3.14, "3.14")); + assertThat(ce.get("b")).hasValue(Binding.of("b", SimpleType.BOOL, true, "true")); + assertThat(ce.get("s")).hasValue(Binding.of("s", SimpleType.STRING, "admin", "\"admin\"")); + assertThat(ce.get("bytes_val")) + .hasValue( + Binding.of( + "bytes_val", SimpleType.BYTES, CelByteString.copyFromUtf8("foo"), "b\"foo\"")); + assertThat(ce.get("ts")) + .hasValue( + Binding.of( + "ts", + SimpleType.TIMESTAMP, + Instant.ofEpochSecond(1767225600), + "timestamp(1767225600)")); + assertThat(ce.get("dur")) + .hasValue( + Binding.of("dur", SimpleType.DURATION, Duration.ofSeconds(10), "duration('10s')")); + + // Test direct evaluation context with CelRuntime + ImmutableMap evalContext = ce.toEvaluationContext(); + Object evalResult = cel.createProgram(ast).eval(evalContext); + assertThat(evalResult).isEqualTo(true); + } + + @Test + public void structuredCounterexample_collectionTypes() throws Exception { + Cel cel = + CelFactory.plannerCelBuilder() + .addVar("l", ListType.create(SimpleType.INT)) + .addVar("m", MapType.create(SimpleType.STRING, SimpleType.INT)) + .build(); + CelAbstractSyntaxTree ast = + cel.compile("l == [1, 2, 3] && m == {'key1': 10, 'key2': 20}").getAst(); + + CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); + CelVerificationResult result = verifier.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.counterexampleModel()).isPresent(); + CelCounterexample ce = result.counterexampleModel().get(); + + assertThat(ce.get("l")) + .hasValue( + Binding.of( + "l", ListType.create(SimpleType.INT), ImmutableList.of(1L, 2L, 3L), "[1, 2, 3]")); + assertThat(ce.get("m")) + .hasValue( + Binding.of( + "m", + MapType.create(SimpleType.STRING, SimpleType.INT), + ImmutableMap.of("key1", 10L, "key2", 20L), + "{\"key1\": 10, \"key2\": 20}")); + + // Test evaluation context execution + Object evalResult = cel.createProgram(ast).eval(ce.toEvaluationContext()); + assertThat(evalResult).isEqualTo(true); + } + + @Test + public void structuredCounterexample_optionalTypes() throws Exception { + Cel cel = + CelFactory.plannerCelBuilder() + .addCompilerLibraries(CelOptionalLibrary.INSTANCE) + .addRuntimeLibraries(CelOptionalLibrary.INSTANCE) + .addVar("opt_val", OptionalType.create(SimpleType.INT)) + .addVar("opt_empty", OptionalType.create(SimpleType.INT)) + .build(); + CelAbstractSyntaxTree ast = + cel.compile("opt_val == optional.of(42) && opt_empty == optional.none()").getAst(); + + CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); + CelVerificationResult result = verifier.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.counterexampleModel()).isPresent(); + CelCounterexample ce = result.counterexampleModel().get(); + + assertThat(ce.get("opt_val")) + .hasValue( + Binding.of( + "opt_val", OptionalType.create(SimpleType.INT), Optional.of(42L), "optional(42)")); + assertThat(ce.get("opt_empty")) + .hasValue( + Binding.of( + "opt_empty", + OptionalType.create(SimpleType.DYN), + Optional.empty(), + "optional.none()")); + } + + @Test + public void structuredCounterexample_protoMessage() throws Exception { + Cel cel = + CelFactory.plannerCelBuilder() + .setContainer(CelContainer.ofName("cel.expr.conformance.proto3")) + .addMessageTypes(TestAllTypes.getDescriptor()) + .setTypeProvider(TYPE_PROVIDER) + .addVar("msg", StructTypeReference.create(TestAllTypes.getDescriptor().getFullName())) + .build(); + CelAbstractSyntaxTree ast = + cel.compile("msg == TestAllTypes{single_int32: 80, single_string: 'admin'}").getAst(); + + CelVerifier verifier = + CelVerifierFactory.newVerifier(cel).setTypeProvider(TYPE_PROVIDER).build(); + CelVerificationResult result = verifier.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.counterexampleModel()).isPresent(); + CelCounterexample ce = result.counterexampleModel().get(); + TestAllTypes expectedProto = + TestAllTypes.newBuilder().setSingleInt32(80).setSingleString("admin").build(); + assertThat(ce.get("msg")) + .hasValue( + Binding.of( + "msg", + StructTypeReference.create("cel.expr.conformance.proto3.TestAllTypes"), + expectedProto, + "cel.expr.conformance.proto3.TestAllTypes{single_string: \"admin\", single_int32:" + + " 80}")); + assertThat(cel.createProgram(ast).eval(ce.toEvaluationContext())).isEqualTo(true); + } + + @Test + public void structuredCounterexample_stringEdgeCases() throws Exception { + Cel cel = + CelFactory.plannerCelBuilder() + .addVar("s_empty", SimpleType.STRING) + .addVar("s_quote", SimpleType.STRING) + .addVar("s_single", SimpleType.STRING) + .build(); + CelAbstractSyntaxTree ast = + cel.compile("s_empty == '' && s_quote == '\"' && s_single == 'a'").getAst(); + + CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); + CelVerificationResult result = verifier.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.counterexampleModel()).isPresent(); + CelCounterexample ce = result.counterexampleModel().get(); + + assertThat(ce.get("s_empty")).hasValue(Binding.of("s_empty", SimpleType.STRING, "", "\"\"")); + assertThat(ce.get("s_single")) + .hasValue(Binding.of("s_single", SimpleType.STRING, "a", "\"a\"")); + assertThat(ce.get("s_quote")) + .hasValue(Binding.of("s_quote", SimpleType.STRING, "\"", "\"\"\"\"")); + } + + @Test + public void structuredCounterexample_doubleValues() throws Exception { + Cel cel = + CelFactory.plannerCelBuilder() + .addVar("d_pi", SimpleType.DOUBLE) + .addVar("d_val", SimpleType.DOUBLE) + .build(); + CelAbstractSyntaxTree ast = cel.compile("d_pi == 3.14159 && d_val == 2.5").getAst(); + + CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); + CelVerificationResult result = verifier.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.counterexampleModel()).isPresent(); + CelCounterexample ce = result.counterexampleModel().get(); + + assertThat(ce.get("d_pi")).hasValue(Binding.of("d_pi", SimpleType.DOUBLE, 3.14159, "3.14159")); + assertThat(ce.get("d_val")).hasValue(Binding.of("d_val", SimpleType.DOUBLE, 2.5, "2.5")); + } + + @Test + public void structuredCounterexample_listTruncation_printsEllipsis() throws Exception { + Cel cel = + CelFactory.plannerCelBuilder().addVar("l_long", ListType.create(SimpleType.INT)).build(); + CelAbstractSyntaxTree ast = + cel.compile( + "l_long == [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19]") + .getAst(); + + CelVerifier verifier = + CelVerifierFactory.newVerifier(cel).setComprehensionUnrollLimit(25).build(); + CelVerificationResult result = verifier.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.counterexampleModel()).isPresent(); + CelCounterexample ce = result.counterexampleModel().get(); + + assertThat(ce.get("l_long").map(Binding::celString)) + .hasValue("[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, ... (5 more elements)]"); + assertThat(ce.get("l_long").flatMap(Binding::nativeValue)) + .hasValue( + ImmutableList.of( + 0L, 1L, 2L, 3L, 4L, 5L, 6L, 7L, 8L, 9L, 10L, 11L, 12L, 13L, 14L, 15L, 16L, 17L, 18L, + 19L)); + } + + @Test + public void structuredCounterexample_mapWithDifferentKeyTypes() throws Exception { + Cel cel = + CelFactory.plannerCelBuilder() + .addVar("m_int", MapType.create(SimpleType.INT, SimpleType.STRING)) + .addVar("m_uint", MapType.create(SimpleType.UINT, SimpleType.BOOL)) + .addVar("m_bool", MapType.create(SimpleType.BOOL, SimpleType.INT)) + .build(); + CelAbstractSyntaxTree ast = + cel.compile( + "m_int == {1: 'one', 2: 'two'} && m_uint == {10u: true, 20u: false} && m_bool ==" + + " {true: 100, false: 200}") + .getAst(); + + CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); + CelVerificationResult result = verifier.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.counterexampleModel()).isPresent(); + CelCounterexample ce = result.counterexampleModel().get(); + + assertThat(ce.get("m_int").flatMap(Binding::nativeValue)) + .hasValue(ImmutableMap.of(1L, "one", 2L, "two")); + assertThat(ce.get("m_uint").flatMap(Binding::nativeValue)) + .hasValue( + ImmutableMap.of( + UnsignedLong.fromLongBits(10), true, UnsignedLong.fromLongBits(20), false)); + assertThat(ce.get("m_bool").flatMap(Binding::nativeValue)) + .hasValue(ImmutableMap.of(true, 100L, false, 200L)); + assertThat(cel.createProgram(ast).eval(ce.toEvaluationContext())).isEqualTo(true); + } + + @Test + public void structuredCounterexample_nullType() throws Exception { + Cel cel = CelFactory.plannerCelBuilder().addVar("n", SimpleType.NULL_TYPE).build(); + CelAbstractSyntaxTree ast = cel.compile("n == null").getAst(); + + CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); + CelVerificationResult result = verifier.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.counterexampleModel()).isPresent(); + CelCounterexample ce = result.counterexampleModel().get(); + + assertThat(ce.get("n")).hasValue(Binding.of("n", SimpleType.NULL_TYPE, null, "null")); + } + + @Test + public void structuredCounterexample_unconditionalSatisfiableAndFailing() throws Exception { + Cel cel = CelFactory.plannerCelBuilder().build(); + + CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); + + // Satisfiable without any variable inputs + CelVerificationResult satResult = verifier.isSatisfiable(cel.compile("true").getAst()); + assertThat(satResult.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(satResult.message()) + .contains("The expression is satisfiable unconditionally, regardless of input state"); + + // Unconditional violation without any variable inputs + CelVerificationResult failResult = verifier.isAlwaysTrue(cel.compile("false").getAst()); + assertThat(failResult.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(failResult.message()) + .contains("The expression fails unconditionally, regardless of input state"); + } + + @Test + public void cegarRefinement_tryCegarRefinement_mismatchedOrSpuriousModel_returnsSpurious() + throws Exception { + Cel cel = CelFactory.plannerCelBuilder().addVar("x", SimpleType.INT).build(); + CegarRefiner refiner = new CegarRefiner(cel); + + CelAbstractSyntaxTree astA = cel.compile("x == 1").getAst(); + CelAbstractSyntaxTree astB = cel.compile("x == 2").getAst(); + CelAbstractSyntaxTree astFailing = cel.compile("x != 1").getAst(); + CelAbstractSyntaxTree astPassing = cel.compile("x == 1").getAst(); + + CelCounterexample satisfyingModel = + CelCounterexample.create( + ImmutableMap.of("x", Binding.of("x", SimpleType.INT, 1L, "1")), + /* isApproximate= */ false, + /* isSatisfyingInput= */ true, + ""); + CelCounterexample counterexampleModel = + CelCounterexample.create( + ImmutableMap.of("x", Binding.of("x", SimpleType.INT, 1L, "1")), + /* isApproximate= */ false, + /* isSatisfyingInput= */ false, + ""); + + assertThat(refiner.refineEquivalence(astA, astB, satisfyingModel).isViolation()).isFalse(); + + // Mismatched satisfying flag returns spurious + assertThat( + refiner + .refineSatisfiability( + astFailing, /* searchForCounterexample= */ true, satisfyingModel) + .isViolation()) + .isFalse(); + assertThat( + refiner + .refineSatisfiability( + astPassing, /* searchForCounterexample= */ false, counterexampleModel) + .isViolation()) + .isFalse(); + + // Passing AST evaluated against candidate counterexample (x=1 -> 1==1 is true) refutes the + // counterexample as spurious + assertThat( + refiner + .refineSatisfiability( + astPassing, /* searchForCounterexample= */ true, counterexampleModel) + .isViolation()) + .isFalse(); + + // Failing AST evaluated against candidate counterexample (x=1 -> 1!=1 is false) confirms + // violation + assertThat( + refiner + .refineSatisfiability( + astFailing, /* searchForCounterexample= */ true, counterexampleModel) + .isViolation()) + .isTrue(); + + assertThat( + refiner.refineImplication(astA, astB, ImmutableMap.of(), satisfyingModel).isViolation()) + .isFalse(); + } + + @Test + public void cegarRefinement_refineImplication_premiseFails_returnsSpurious() throws Exception { + Cel cel = CelFactory.plannerCelBuilder().addVar("x", SimpleType.INT).build(); + CegarRefiner refiner = new CegarRefiner(cel); + + CelAbstractSyntaxTree assumeAst = cel.compile("x > 5").getAst(); + CelAbstractSyntaxTree assertAst = cel.compile("x > 3").getAst(); + + // Candidate model does not satisfy the assumption (x=1 -> x > 5 is false). + // Premise did not hold, so the model cannot serve as a counterexample. + CelCounterexample premiseFailsModel = + CelCounterexample.create( + ImmutableMap.of("x", Binding.of("x", SimpleType.INT, 1L, "1")), + /* isApproximate= */ false, + /* isSatisfyingInput= */ false, + ""); + assertThat( + refiner + .refineImplication(assumeAst, assertAst, ImmutableMap.of(), premiseFailsModel) + .isViolation()) + .isFalse(); + } + + @Test + public void cegarRefinement_refineImplication_premiseAndAssertionHold_returnsSpurious() + throws Exception { + Cel cel = CelFactory.plannerCelBuilder().addVar("x", SimpleType.INT).build(); + CegarRefiner refiner = new CegarRefiner(cel); + + CelAbstractSyntaxTree assumeAst = cel.compile("x > 5").getAst(); + CelAbstractSyntaxTree assertAst = cel.compile("x > 3").getAst(); + + // Candidate model satisfies assumption and assertion (x=10 -> x > 5 is true, x > 3 is true). + // Candidate counterexample is refuted (spurious). + CelCounterexample bothHoldModel = + CelCounterexample.create( + ImmutableMap.of("x", Binding.of("x", SimpleType.INT, 10L, "10")), + /* isApproximate= */ false, + /* isSatisfyingInput= */ false, + ""); + assertThat( + refiner + .refineImplication(assumeAst, assertAst, ImmutableMap.of(), bothHoldModel) + .isViolation()) + .isFalse(); + } + + @Test + public void cegarRefinement_refineImplication_premiseHoldsAndAssertionFails_returnsViolation() + throws Exception { + Cel cel = CelFactory.plannerCelBuilder().addVar("x", SimpleType.INT).build(); + CegarRefiner refiner = new CegarRefiner(cel); + + CelAbstractSyntaxTree assumeAst = cel.compile("x > 5").getAst(); + CelAbstractSyntaxTree assertFailingAst = cel.compile("x < 0").getAst(); + + // Candidate model satisfies assumption but violates assertion (x=10 -> x > 5 is true, x < 0 is + // false). Valid counterexample confirmed. + CelCounterexample violationModel = + CelCounterexample.create( + ImmutableMap.of("x", Binding.of("x", SimpleType.INT, 10L, "10")), + /* isApproximate= */ false, + /* isSatisfyingInput= */ false, + ""); + assertThat( + refiner + .refineImplication(assumeAst, assertFailingAst, ImmutableMap.of(), violationModel) + .isViolation()) + .isTrue(); + } + + @Test + public void cegarRefinement_refineImplication_withBoundSymbols_returnsViolation() + throws Exception { + Cel cel = + CelFactory.plannerCelBuilder() + .addVar("x", SimpleType.INT) + .addVar("y", SimpleType.INT) + .build(); + CegarRefiner refiner = new CegarRefiner(cel); + + // Implication with boundSymbols: y := x + 1, assume y > 5, assert y > 10. + // x=5 -> y=6 (y > 5 is true, y > 10 is false) -> violation. + CelAbstractSyntaxTree boundSymbolAst = cel.compile("x + 1").getAst(); + CelAbstractSyntaxTree boundAssumeAst = cel.compile("y > 5").getAst(); + CelAbstractSyntaxTree boundAssertAst = cel.compile("y > 10").getAst(); + CelCounterexample boundSymbolModel = + CelCounterexample.create( + ImmutableMap.of("x", Binding.of("x", SimpleType.INT, 5L, "5")), + /* isApproximate= */ false, + /* isSatisfyingInput= */ false, + ""); + assertThat( + refiner + .refineImplication( + boundAssumeAst, + boundAssertAst, + ImmutableMap.of("y", boundSymbolAst), + boundSymbolModel) + .isViolation()) + .isTrue(); + } + + @Test + // Generic Z3 ArrayExpr and mkStore APIs use raw ArraySort types in Java bindings. + @SuppressWarnings({"unchecked", "rawtypes"}) + public void reconstructMap_truncation_limitsPrintedEntries() { + Cel cel = CelFactory.plannerCelBuilder().build(); + CelValueProvider valueProvider = cel.toCelBuilder().valueProvider(); + + try (Context ctx = new Context()) { + CelZ3TypeSystem typeSystem = new CelZ3TypeSystem(ctx); + Expr mapRef = typeSystem.mkMapRefConst("test_map"); + + // Construct a sequence of 18 keys (0 to 17) and presence/values arrays + Expr keysSeq = ctx.mkEmptySeq(ctx.mkSeqSort(typeSystem.celValueSort())); + ArrayExpr presenceArray = ctx.mkConstArray(typeSystem.celValueSort(), ctx.mkFalse()); + ArrayExpr valuesArray = ctx.mkConstArray(typeSystem.celValueSort(), typeSystem.mkNull()); + + for (int i = 0; i < 18; i++) { + Expr key = typeSystem.mkInt(i); + Expr val = typeSystem.mkInt(i * 10); + keysSeq = typeSystem.mkConcatSafe(keysSeq, ctx.mkUnit(key)); + presenceArray = ctx.mkStore(presenceArray, key, ctx.mkTrue()); + valuesArray = ctx.mkStore(valuesArray, key, val); + } + + Solver solver = ctx.mkSolver(); + solver.add(ctx.mkEq(typeSystem.getMapKeys(mapRef), keysSeq)); + solver.add(ctx.mkEq(typeSystem.getMapPresence(mapRef), presenceArray)); + solver.add(ctx.mkEq(typeSystem.getMapValues(mapRef), valuesArray)); + solver.check(); + Model model = solver.getModel(); + + CelZ3CounterexampleGenerator.ExtractedNode node = + CelZ3CounterexampleGenerator.reconstructMap( + ctx, typeSystem, valueProvider, model, mapRef); + + assertThat(node.celString).contains("... (3 more entries)"); + assertThat(node.celString).contains("0: 0"); + assertThat(node.celString).contains("14: 140"); + // Key 15, 16, 17 must NOT be in the string preview + assertThat(node.celString).doesNotContain("15: 150"); + assertThat(node.celString).doesNotContain("16: 160"); + assertThat(node.celString).doesNotContain("17: 170"); + + // Full native map still contains all 18 entries + assertThat((ImmutableMap) node.nativeValue).hasSize(18); + } + } + + @Test + public void structuredCounterexample_rawZ3Terms_extractsDirectly() { + Cel cel = CelFactory.plannerCelBuilder().build(); + CelValueProvider valueProvider = cel.toCelBuilder().valueProvider(); + + try (Context ctx = new Context()) { + CelZ3TypeSystem typeSystem = new CelZ3TypeSystem(ctx); + Solver solver = ctx.mkSolver(); + + // Create constants for raw Z3 terms + Expr rawInt = ctx.mkConst("raw_int", ctx.getIntSort()); + Expr rawString = ctx.mkConst("raw_str", ctx.getStringSort()); + Expr rawBool = ctx.mkConst("raw_bool", ctx.getBoolSort()); + Expr rawFp = ctx.mkConst("raw_fp", ctx.mkFPSortDouble()); + Expr rawFpNaN = ctx.mkConst("raw_fp_nan", ctx.mkFPSortDouble()); + Expr rawFpPosInf = ctx.mkConst("raw_fp_pos_inf", ctx.mkFPSortDouble()); + Expr rawFpNegInf = ctx.mkConst("raw_fp_neg_inf", ctx.mkFPSortDouble()); + Expr rawFpNegZero = ctx.mkConst("raw_fp_neg_zero", ctx.mkFPSortDouble()); + Expr rawNull = ctx.mkConst("raw_null", typeSystem.celValueSort()); + Expr rawError = ctx.mkConst("raw_error", typeSystem.celValueSort()); + Expr rawUnknown = ctx.mkConst("raw_unknown", typeSystem.celValueSort()); + Expr skolemVar = ctx.mkConst("k!123", ctx.getIntSort()); + + solver.add(ctx.mkEq(rawInt, ctx.mkInt(999))); + solver.add(ctx.mkEq(rawString, ctx.mkString("hello \"world\""))); + solver.add(ctx.mkEq(rawBool, ctx.mkTrue())); + solver.add(ctx.mkEq(rawFp, ctx.mkFP(2.5, ctx.mkFPSortDouble()))); + solver.add(ctx.mkEq(rawFpNaN, ctx.mkFPNaN(ctx.mkFPSortDouble()))); + solver.add(ctx.mkEq(rawFpPosInf, ctx.mkFPInf(ctx.mkFPSortDouble(), false))); + solver.add(ctx.mkEq(rawFpNegInf, ctx.mkFPInf(ctx.mkFPSortDouble(), true))); + solver.add(ctx.mkEq(rawFpNegZero, ctx.mkFPZero(ctx.mkFPSortDouble(), true))); + solver.add(ctx.mkEq(rawNull, typeSystem.mkNull())); + solver.add(ctx.mkEq(rawError, typeSystem.mkError())); + solver.add(ctx.mkEq(rawUnknown, typeSystem.mkUnknown())); + solver.add(ctx.mkEq(skolemVar, ctx.mkInt(1))); + + Status status = solver.check(); + assertThat(status).isEqualTo(Status.SATISFIABLE); + + Model model = solver.getModel(); + + // Test CelZ3CounterexampleGenerator.extract + CelCounterexample ce = + CelZ3CounterexampleGenerator.extract( + ctx, + typeSystem, + valueProvider, + model, + /* isApproximate= */ false, + /* isSatisfyingInput= */ true); + + // Verify skolem constant is filtered out + assertThat(ce.get("k!123")).isEmpty(); + + // Verify raw int + assertThat(ce.get("raw_int")).hasValue(Binding.of("raw_int", SimpleType.INT, 999L, "999")); + + // Verify raw string with escaped quotes unquoted + assertThat(ce.get("raw_str")) + .hasValue( + Binding.of( + "raw_str", SimpleType.STRING, "hello \"world\"", "\"hello \"\"world\"\"\"")); + + // Verify raw bool + assertThat(ce.get("raw_bool")) + .hasValue(Binding.of("raw_bool", SimpleType.BOOL, true, "true")); + + // Verify raw double (FPNum) + assertThat(ce.get("raw_fp")).hasValue(Binding.of("raw_fp", SimpleType.DOUBLE, 2.5, "2.5")); + + // Verify double special values: NaN, +Inf, -Inf, -0.0 + Binding nanBinding = ce.get("raw_fp_nan").get(); + assertThat(nanBinding.type()).isEqualTo(SimpleType.DOUBLE); + assertThat(((Double) nanBinding.nativeValue().get()).isNaN()).isTrue(); + assertThat(nanBinding.celString()).isEqualTo("NaN"); + + assertThat(ce.get("raw_fp_pos_inf").flatMap(Binding::nativeValue)) + .hasValue(Double.POSITIVE_INFINITY); + assertThat(ce.get("raw_fp_pos_inf").map(Binding::celString)).hasValue("Infinity"); + + assertThat(ce.get("raw_fp_neg_inf").flatMap(Binding::nativeValue)) + .hasValue(Double.NEGATIVE_INFINITY); + assertThat(ce.get("raw_fp_neg_inf").map(Binding::celString)).hasValue("-Infinity"); + + assertThat(ce.get("raw_fp_neg_zero").flatMap(Binding::nativeValue)).hasValue(-0.0); + assertThat(ce.get("raw_fp_neg_zero").map(Binding::celString)).hasValue("-0.0"); + + // Verify null, error, unknown + assertThat(ce.get("raw_null")) + .hasValue(Binding.of("raw_null", SimpleType.NULL_TYPE, null, "null")); + + assertThat(ce.get("raw_error")) + .hasValue(Binding.of("raw_error", SimpleType.ERROR, null, "Error")); + + assertThat(ce.get("raw_unknown")) + .hasValue(Binding.of("raw_unknown", SimpleType.DYN, null, "Unknown")); + } + } + + @Test + public void directExtractNode_uninterpretedSorts_returnsDynFallback() { + Cel cel = CelFactory.plannerCelBuilder().build(); + CelValueProvider valueProvider = cel.toCelBuilder().valueProvider(); + + try (Context ctx = new Context()) { + CelZ3TypeSystem typeSystem = new CelZ3TypeSystem(ctx); + UninterpretedSort customSort = ctx.mkUninterpretedSort("CustomSort"); + Expr customConst = ctx.mkConst("custom_val", customSort); + + Solver solver = ctx.mkSolver(); + solver.check(); + Model model = solver.getModel(); + + CelZ3CounterexampleGenerator.ExtractedNode node = + CelZ3CounterexampleGenerator.extractNode( + ctx, typeSystem, valueProvider, model, customConst); + assertThat(node.type).isEqualTo(SimpleType.DYN); + assertThat(node.nativeValue).isNull(); + assertThat(node.celString).isEqualTo("custom_val"); + } + } + + @Test + public void unquoteZ3String_edgeCases() { + assertThat(CelZ3CounterexampleGenerator.unquoteZ3String("unquoted")).isEqualTo("unquoted"); + assertThat(CelZ3CounterexampleGenerator.unquoteZ3String("")).isEmpty(); + assertThat(CelZ3CounterexampleGenerator.unquoteZ3String("\"")).isEqualTo("\""); + assertThat(CelZ3CounterexampleGenerator.unquoteZ3String("\"\"")).isEmpty(); + assertThat(CelZ3CounterexampleGenerator.unquoteZ3String("\"hello\"")).isEqualTo("hello"); + assertThat(CelZ3CounterexampleGenerator.unquoteZ3String("\"hello \"\"world\"\"\"")) + .isEqualTo("hello \"world\""); + } + + @Test + public void decodeDouble_nonFpNum_returnsFallback() { + try (Context ctx = new Context()) { + Expr uninterpretedDouble = ctx.mkConst("unresolved_double", ctx.mkFPSortDouble()); + CelZ3CounterexampleGenerator.ExtractedNode node = + CelZ3CounterexampleGenerator.decodeDouble(ctx, uninterpretedDouble); + assertThat(node.type).isEqualTo(SimpleType.DOUBLE); + assertThat(node.nativeValue).isNull(); + assertThat(node.celString).isEqualTo("unresolved_double"); + } + } + + @Test + public void decodeOptional_noneRef_returnsNone() { + Cel cel = CelFactory.plannerCelBuilder().build(); + CelValueProvider valueProvider = cel.toCelBuilder().valueProvider(); + + try (Context ctx = new Context()) { + CelZ3TypeSystem typeSystem = new CelZ3TypeSystem(ctx); + Expr optRef = typeSystem.mkNoneOptionalRef(); + Solver solver = ctx.mkSolver(); + solver.check(); + Model model = solver.getModel(); + + CelZ3CounterexampleGenerator.ExtractedNode node = + CelZ3CounterexampleGenerator.decodeOptional( + ctx, typeSystem, valueProvider, model, optRef); + assertThat(node.type).isEqualTo(OptionalType.create(SimpleType.DYN)); + assertThat((Optional) node.nativeValue).isEmpty(); + assertThat(node.celString).isEqualTo("optional.none()"); + } + } + + @Test + public void structuredCounterexample_displayPrefixes() { + Cel cel = CelFactory.plannerCelBuilder().build(); + CelValueProvider valueProvider = cel.toCelBuilder().valueProvider(); + + try (Context ctx = new Context()) { + CelZ3TypeSystem typeSystem = new CelZ3TypeSystem(ctx); + Solver solver = ctx.mkSolver(); + Expr x = ctx.mkConst("x", ctx.getIntSort()); + solver.add(ctx.mkEq(x, ctx.mkInt(1))); + solver.check(); + Model model = solver.getModel(); + + CelCounterexample exactSat = + CelZ3CounterexampleGenerator.extract( + ctx, + typeSystem, + valueProvider, + model, + /* isApproximate= */ false, + /* isSatisfyingInput= */ true); + assertThat(exactSat.toDisplayString()).startsWith(" Satisfying input:\n x = 1"); + + CelCounterexample approxSat = + CelZ3CounterexampleGenerator.extract( + ctx, + typeSystem, + valueProvider, + model, + /* isApproximate= */ true, + /* isSatisfyingInput= */ true); + assertThat(approxSat.toDisplayString()).startsWith(" Potential satisfying input:\n x = 1"); + + CelCounterexample exactCounter = + CelZ3CounterexampleGenerator.extract( + ctx, + typeSystem, + valueProvider, + model, + /* isApproximate= */ false, + /* isSatisfyingInput= */ false); + assertThat(exactCounter.toDisplayString()).startsWith(" Counterexample input:\n x = 1"); + + CelCounterexample approxCounter = + CelZ3CounterexampleGenerator.extract( + ctx, + typeSystem, + valueProvider, + model, + /* isApproximate= */ true, + /* isSatisfyingInput= */ false); + assertThat(approxCounter.toDisplayString()) + .startsWith(" Potential counterexample input:\n x = 1"); + } + } + + @Test + public void extractNode_celUnknown_returnsUnknownNode() { + Cel cel = CelFactory.plannerCelBuilder().build(); + CelValueProvider valueProvider = cel.toCelBuilder().valueProvider(); + + try (Context ctx = new Context()) { + CelZ3TypeSystem typeSystem = new CelZ3TypeSystem(ctx); + Expr unknownVal = typeSystem.mkUnknown(); + Solver solver = ctx.mkSolver(); + solver.check(); + Model model = solver.getModel(); + + CelZ3CounterexampleGenerator.ExtractedNode node = + CelZ3CounterexampleGenerator.extractNode( + ctx, typeSystem, valueProvider, model, unknownVal); + assertThat(node.type).isEqualTo(SimpleType.DYN); + assertThat(node.nativeValue).isNull(); + assertThat(node.celString).isEqualTo("Unknown"); + } + } + + @Test + public void extractNode_unrecognizedConstructor_returnsFallbackDynNode() { + Cel cel = CelFactory.plannerCelBuilder().build(); + CelValueProvider valueProvider = cel.toCelBuilder().valueProvider(); + + try (Context ctx = new Context()) { + CelZ3TypeSystem typeSystem = new CelZ3TypeSystem(ctx); + UninterpretedSort customSort = ctx.mkUninterpretedSort("CustomSort"); + FuncDecl customCons = + ctx.mkFuncDecl("CustomCons", new Sort[] {typeSystem.celValueSort()}, customSort); + Expr customTerm = ctx.mkApp(customCons, typeSystem.mkInt(42)); + Solver solver = ctx.mkSolver(); + solver.check(); + Model model = solver.getModel(); + + CelZ3CounterexampleGenerator.ExtractedNode node = + CelZ3CounterexampleGenerator.extractNode( + ctx, typeSystem, valueProvider, model, customTerm); + assertThat(node.type).isEqualTo(SimpleType.DYN); + assertThat(node.nativeValue).isNull(); + assertThat(node.celString).contains("CustomCons"); + } + } + + @Test + // Generic Z3 ArrayExpr and mkStore APIs use raw ArraySort types in Java bindings. + @SuppressWarnings({"unchecked", "rawtypes"}) + public void reconstructMessage_unregisteredType_fallsBackToFieldMap() { + Cel cel = CelFactory.plannerCelBuilder().build(); + CelValueProvider valueProvider = cel.toCelBuilder().valueProvider(); + + try (Context ctx = new Context()) { + CelZ3TypeSystem typeSystem = new CelZ3TypeSystem(ctx); + Expr msgRef = typeSystem.mkMessageRefConst("test_msg"); + + Expr fieldKey = ctx.mkString("field_a"); + Expr fieldValue = typeSystem.mkInt(100); + + ArrayExpr presenceArray = ctx.mkConstArray(ctx.getStringSort(), ctx.mkFalse()); + presenceArray = ctx.mkStore(presenceArray, fieldKey, ctx.mkTrue()); + + ArrayExpr valuesArray = ctx.mkConstArray(ctx.getStringSort(), typeSystem.mkNull()); + valuesArray = ctx.mkStore(valuesArray, fieldKey, fieldValue); + + Solver solver = ctx.mkSolver(); + solver.add(ctx.mkEq(typeSystem.getMsgTypeName(msgRef), ctx.mkString("custom.DynamicStruct"))); + solver.add(ctx.mkEq(typeSystem.getMsgPresence(msgRef), presenceArray)); + solver.add(ctx.mkEq(typeSystem.getMsgValues(msgRef), valuesArray)); + solver.check(); + Model model = solver.getModel(); + + CelZ3CounterexampleGenerator.ExtractedNode node = + CelZ3CounterexampleGenerator.reconstructMessage( + ctx, typeSystem, valueProvider, model, msgRef); + + assertThat(node.type).isEqualTo(StructTypeReference.create("custom.DynamicStruct")); + assertThat(node.nativeValue).isEqualTo(ImmutableMap.of("field_a", 100L)); + assertThat(node.celString).isEqualTo("custom.DynamicStruct{field_a: 100}"); + } + } +}