diff --git a/BUILD.bazel b/BUILD.bazel index 024908625..d2bf2124b 100644 --- a/BUILD.bazel +++ b/BUILD.bazel @@ -95,6 +95,14 @@ java_library( ], ) +java_library( + name = "java_jline", + exports = [ + "@maven//:org_jline_jline_reader", + "@maven//:org_jline_jline_terminal", + ], +) + default_java_toolchain( name = "repository_default_toolchain", configuration = DEFAULT_TOOLCHAIN_CONFIGURATION, diff --git a/MODULE.bazel b/MODULE.bazel index ce9c67fde..3dcf8b0e5 100644 --- a/MODULE.bazel +++ b/MODULE.bazel @@ -95,6 +95,8 @@ maven.install( "info.picocli:picocli:4.7.7", "org.antlr:antlr4-runtime:4.13.2", "org.freemarker:freemarker:2.3.34", + "org.jline:jline-reader:3.26.1", + "org.jline:jline-terminal:3.26.1", "org.jspecify:jspecify:1.0.0", "org.threeten:threeten-extra:1.8.0", "org.yaml:snakeyaml:2.5", diff --git a/verifier/BUILD.bazel b/verifier/BUILD.bazel index cc2f01810..ef1316ca2 100644 --- a/verifier/BUILD.bazel +++ b/verifier/BUILD.bazel @@ -41,6 +41,13 @@ java_library( exports = ["//verifier/src/main/java/dev/cel/verifier:verifier_factory"], ) +java_library( + name = "numeric_bounds", + compatible_with = [], + visibility = [":verifier_internal"], + exports = ["//verifier/src/main/java/dev/cel/verifier:numeric_bounds"], +) + java_library( name = "type_system", compatible_with = [], @@ -54,3 +61,10 @@ java_library( visibility = [":verifier_internal"], exports = ["//verifier/src/main/java/dev/cel/verifier:z3_impl"], ) + +java_library( + name = "canonicalization_optimizer", + compatible_with = [], + visibility = [":verifier_internal"], + exports = ["//verifier/src/main/java/dev/cel/verifier:canonicalization_optimizer"], +) diff --git a/verifier/README.md b/verifier/README.md index f286a4d6f..bd9979390 100644 --- a/verifier/README.md +++ b/verifier/README.md @@ -433,3 +433,7 @@ What this means for verification: default unless you have a specific need and bounded inputs. --- + +## Tools & CLI + +For command-line verification and interactive execution, see the [CLI Tool documentation](tools/README.md). diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index 4ca9794cc..a0de7948a 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel @@ -35,6 +35,12 @@ java_library( deps = [ ":verifier", ":z3_impl", + "//bundle:cel", + "//checker:checker_builder", + "//compiler", + "//compiler:compiler_builder", + "//parser:parser_builder", + "//runtime", ], ) @@ -91,6 +97,19 @@ java_library( ], ) +java_library( + name = "numeric_bounds", + srcs = ["CelNumericBounds.java"], + compatible_with = [], + tags = [ + ], + deps = [ + "//:auto_value", + "//common/annotations", + "@maven//:com_google_guava_guava", + ], +) + java_library( name = "type_system", srcs = ["CelZ3TypeSystem.java"], @@ -98,6 +117,7 @@ java_library( tags = [ ], deps = [ + ":numeric_bounds", "//common/internal:proto_time_utils", "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:com_google_guava_guava", @@ -105,6 +125,29 @@ java_library( ], ) +java_library( + name = "canonicalization_optimizer", + srcs = ["CanonicalizationOptimizer.java"], + tags = [ + ], + deps = [ + "//:auto_value", + "//bundle:cel", + "//common:cel_ast", + "//common:mutable_ast", + "//common:mutable_source", + "//common:operator", + "//common/ast", + "//common/ast:mutable_expr", + "//common/navigation:common", + "//common/navigation:mutable_navigation", + "//common/values:cel_byte_string", + "//optimizer:ast_optimizer", + "//optimizer:mutable_ast", + "@maven//:com_google_guava_guava", + ], +) + java_library( name = "z3_impl", srcs = [ @@ -121,9 +164,12 @@ java_library( tags = [ ], deps = [ + ":canonicalization_optimizer", + ":numeric_bounds", ":type_system", ":verifier", "//:auto_value", + "//bundle:cel", "//common:cel_ast", "//common:compiler_common", "//common:operator", @@ -132,6 +178,9 @@ java_library( "//common/types", "//common/types:cel_types", "//common/types:type_providers", + "//optimizer", + "//optimizer:optimization_exception", + "//optimizer:optimizer_builder", "//verifier/axioms", "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:com_google_guava_guava", diff --git a/verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java b/verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java new file mode 100644 index 000000000..025bfd056 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java @@ -0,0 +1,674 @@ +// 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.collect.ImmutableList.toImmutableList; + +import com.google.auto.value.AutoValue; +import com.google.common.collect.ComparisonChain; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.Iterables; +import dev.cel.bundle.Cel; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.CelMutableAst; +import dev.cel.common.CelMutableSource; +import dev.cel.common.Operator; +import dev.cel.common.ast.CelConstant; +import dev.cel.common.ast.CelExpr.ExprKind.Kind; +import dev.cel.common.ast.CelMutableExpr; +import dev.cel.common.ast.CelMutableExpr.CelMutableCall; +import dev.cel.common.ast.CelMutableExpr.CelMutableComprehension; +import dev.cel.common.ast.CelMutableExpr.CelMutableMap; +import dev.cel.common.ast.CelMutableExpr.CelMutableSelect; +import dev.cel.common.ast.CelMutableExpr.CelMutableStruct; +import dev.cel.common.navigation.CelNavigableMutableAst; +import dev.cel.common.navigation.CelNavigableMutableExpr; +import dev.cel.common.navigation.TraversalOrder; +import dev.cel.common.values.CelByteString; +import dev.cel.optimizer.AstMutator; +import dev.cel.optimizer.CelAstOptimizer; +import java.util.ArrayList; +import java.util.Comparator; +import java.util.HashMap; +import java.util.Iterator; +import java.util.List; +import java.util.Map; +import java.util.Optional; + +/** + * Standalone AST canonicalization pass that normalizes commutative operator ordering and De Morgan + * quantifier/logical identities. + * + *

This optimizer performs: + * + *

+ * + *

Caveat: This is a structural normalizer intended for comparison purposes (such as + * formal equivalence verification) and as a pre-processor for helping other optimizers (such as + * Common Subexpression Elimination). It is not a runtime cost optimizer; lexicographical ordering + * of calls or Negation Normal Form expansions are not designed to optimize runtime execution or + * short-circuit latency. + */ +final class CanonicalizationOptimizer implements CelAstOptimizer { + + private final CanonicalizationOptions canonicalizationOptions; + + private static final Comparator EXPR_COMPARATOR = + new Comparator() { + @Override + public int compare(CelMutableExpr e1, CelMutableExpr e2) { + int kindCmp = + Integer.compare(getKindPriority(e1.getKind()), getKindPriority(e2.getKind())); + if (kindCmp != 0) { + return kindCmp; + } + switch (e1.getKind()) { + case CONSTANT: + return compareConstants(e1.constant(), e2.constant()); + case IDENT: + return e1.ident().name().compareTo(e2.ident().name()); + case SELECT: + return compareSelect(e1.select(), e2.select()); + case CALL: + return compareCall(e1.call(), e2.call()); + case LIST: + return compareList(e1.list().elements(), e2.list().elements()); + case MAP: + return compareMap(e1.map(), e2.map()); + case STRUCT: + return compareStruct(e1.struct(), e2.struct()); + case COMPREHENSION: + return compareComprehension(e1.comprehension(), e2.comprehension()); + case NOT_SET: + return 0; + default: + throw new UnsupportedOperationException( + "Unsupported expression kind: " + e1.getKind()); + } + } + + private int compareConstants(CelConstant c1, CelConstant c2) { + int constKindCmp = c1.getKind().name().compareTo(c2.getKind().name()); + if (constKindCmp != 0) { + return constKindCmp; + } + switch (c1.getKind()) { + case NULL_VALUE: + case NOT_SET: + return 0; + case BOOLEAN_VALUE: + return Boolean.compare(c1.booleanValue(), c2.booleanValue()); + case INT64_VALUE: + return Long.compare(c1.int64Value(), c2.int64Value()); + case UINT64_VALUE: + return c1.uint64Value().compareTo(c2.uint64Value()); + case DOUBLE_VALUE: + return Double.compare(c1.doubleValue(), c2.doubleValue()); + case STRING_VALUE: + return c1.stringValue().compareTo(c2.stringValue()); + case BYTES_VALUE: + return CelByteString.unsignedLexicographicalComparator() + .compare(c1.bytesValue(), c2.bytesValue()); + default: + throw new UnsupportedOperationException("Unsupported constant kind: " + c1.getKind()); + } + } + + private int compareSelect(CelMutableSelect s1, CelMutableSelect s2) { + return ComparisonChain.start() + .compare(s1.operand(), s2.operand(), this) + .compare(s1.field(), s2.field()) + .compareFalseFirst(s1.testOnly(), s2.testOnly()) + .result(); + } + + private int compareCall(CelMutableCall c1, CelMutableCall c2) { + int fnCmp = c1.function().compareTo(c2.function()); + if (fnCmp != 0) { + return fnCmp; + } + boolean hasT1 = c1.target().isPresent(); + boolean hasT2 = c2.target().isPresent(); + if (hasT1 != hasT2) { + return Boolean.compare(hasT1, hasT2); + } + if (hasT1) { + int tCmp = compare(c1.target().get(), c2.target().get()); + if (tCmp != 0) { + return tCmp; + } + } + return compareList(c1.args(), c2.args()); + } + + private int compareMap(CelMutableMap m1, CelMutableMap m2) { + int mapSizeCmp = Integer.compare(m1.entries().size(), m2.entries().size()); + if (mapSizeCmp != 0) { + return mapSizeCmp; + } + Iterator it2 = m2.entries().iterator(); + for (CelMutableMap.Entry entry1 : m1.entries()) { + CelMutableMap.Entry entry2 = it2.next(); + int cmp = + ComparisonChain.start() + .compare(entry1.key(), entry2.key(), this) + .compare(entry1.value(), entry2.value(), this) + .result(); + if (cmp != 0) { + return cmp; + } + } + return 0; + } + + private int compareStruct(CelMutableStruct s1, CelMutableStruct s2) { + int msgCmp = s1.messageName().compareTo(s2.messageName()); + if (msgCmp != 0) { + return msgCmp; + } + int structSizeCmp = Integer.compare(s1.entries().size(), s2.entries().size()); + if (structSizeCmp != 0) { + return structSizeCmp; + } + Iterator it2 = s2.entries().iterator(); + for (CelMutableStruct.Entry entry1 : s1.entries()) { + CelMutableStruct.Entry entry2 = it2.next(); + int cmp = + ComparisonChain.start() + .compare(entry1.fieldKey(), entry2.fieldKey()) + .compare(entry1.value(), entry2.value(), this) + .result(); + if (cmp != 0) { + return cmp; + } + } + return 0; + } + + private int compareComprehension( + CelMutableComprehension c1, CelMutableComprehension c2) { + return ComparisonChain.start() + .compare(c1.iterVar(), c2.iterVar()) + .compare(c1.iterVar2(), c2.iterVar2()) + .compare(c1.accuVar(), c2.accuVar()) + .compare(c1.iterRange(), c2.iterRange(), this) + .compare(c1.accuInit(), c2.accuInit(), this) + .compare(c1.loopCondition(), c2.loopCondition(), this) + .compare(c1.loopStep(), c2.loopStep(), this) + .compare(c1.result(), c2.result(), this) + .result(); + } + + private int compareList(List l1, List l2) { + int sizeCmp = Integer.compare(l1.size(), l2.size()); + if (sizeCmp != 0) { + return sizeCmp; + } + Iterator it2 = l2.iterator(); + for (CelMutableExpr elem1 : l1) { + int cmp = compare(elem1, it2.next()); + if (cmp != 0) { + return cmp; + } + } + return 0; + } + + private int getKindPriority(Kind kind) { + switch (kind) { + case IDENT: + return 1; + case SELECT: + return 2; + case CALL: + return 3; + case LIST: + return 4; + case MAP: + return 5; + case STRUCT: + return 6; + case COMPREHENSION: + return 7; + case CONSTANT: + return 8; + default: + return 99; + } + } + }; + + /** + * Returns a new instance of canonicalization optimizer configured with the provided {@link + * CanonicalizationOptions}. + */ + static CanonicalizationOptimizer newInstance( + CanonicalizationOptions canonicalizationOptions) { + return new CanonicalizationOptimizer(canonicalizationOptions); + } + + @Override + public OptimizationResult optimize(CelAbstractSyntaxTree ast, Cel cel) { + CelMutableAst mutableAst = CelMutableAst.fromCelAst(ast); + mutableAst = runCanonicalizationLoop(mutableAst); + for (Map.Entry entry : + new HashMap<>(mutableAst.source().getMacroCalls()).entrySet()) { + CelMutableExpr canonicalMacro = canonicalize(entry.getValue()); + mutableAst.source().addMacroCalls(entry.getKey(), canonicalMacro); + } + CelAbstractSyntaxTree optimizedAst = + AstMutator.newInstance(canonicalizationOptions.maxIterationLimit()) + .renumberIdsConsecutively(mutableAst) + .toParsedAst(); + return OptimizationResult.create(optimizedAst); + } + + /** Canonicalizes a single CelMutableExpr subtree. */ + private CelMutableExpr canonicalize(CelMutableExpr root) { + CelMutableAst mutableAst = CelMutableAst.of(root, CelMutableSource.newInstance()); + mutableAst = runCanonicalizationLoop(mutableAst); + return mutableAst.expr(); + } + + private CelMutableAst runCanonicalizationLoop(CelMutableAst mutableAst) { + AstMutator astMutator = AstMutator.newInstance(canonicalizationOptions.maxIterationLimit()); + int iterCount = 0; + boolean continueCanonicalizing = true; + while (continueCanonicalizing) { + if (iterCount >= canonicalizationOptions.maxIterationLimit()) { + throw new IllegalStateException( + "Max iteration count reached in CanonicalizationOptimizer."); + } + iterCount++; + continueCanonicalizing = false; + ImmutableList candidateExprs = + CelNavigableMutableAst.fromAst(mutableAst) + .getRoot() + .allNodes(TraversalOrder.POST_ORDER) + .filter(CanonicalizationOptimizer::canCanonicalize) + .collect(toImmutableList()); + for (CelNavigableMutableExpr candidate : candidateExprs) { + iterCount++; + Optional newExpr = maybeCanonicalize(mutableAst, candidate); + if (newExpr.isPresent()) { + continueCanonicalizing = true; + mutableAst = astMutator.replaceSubtree(mutableAst, newExpr.get(), candidate.id()); + break; + } + } + } + return mutableAst; + } + + private static boolean canCanonicalize(CelNavigableMutableExpr navigable) { + CelMutableExpr expr = navigable.expr(); + return isCallWithArgCount(expr, Operator.LOGICAL_AND.getFunction(), 2) + || isCallWithArgCount(expr, Operator.LOGICAL_OR.getFunction(), 2) + || isCallWithArgCount(expr, Operator.EQUALS.getFunction(), 2) + || isCallWithArgCount(expr, Operator.NOT_EQUALS.getFunction(), 2) + || isCallWithArgCount(expr, Operator.LOGICAL_NOT.getFunction(), 1); + } + + private static boolean isComprehensionAccuVar(CelNavigableMutableExpr expr) { + return expr.allNodes() + .filter(node -> node.getKind().equals(Kind.IDENT)) + .anyMatch( + identNode -> { + String identName = identNode.expr().ident().name(); + CelNavigableMutableExpr curr = identNode; + Optional maybeParent = curr.parent(); + while (maybeParent.isPresent()) { + CelNavigableMutableExpr parent = maybeParent.get(); + if (parent.getKind().equals(Kind.COMPREHENSION)) { + CelMutableComprehension compre = parent.expr().comprehension(); + if (compre.accuVar().equals(identName) + && curr.id() != compre.iterRange().id() + && curr.id() != compre.accuInit().id()) { + return true; + } + } + curr = parent; + maybeParent = parent.parent(); + } + return false; + }); + } + + private static Optional maybeCanonicalize( + CelMutableAst mutableAst, CelNavigableMutableExpr navigableExpr) { + CelMutableExpr expr = navigableExpr.expr(); + if (expr.getKind() != Kind.CALL) { + return Optional.empty(); + } + CelMutableCall call = expr.call(); + String functionName = call.function(); + List args = call.args(); + + if ((functionName.equals(Operator.LOGICAL_AND.getFunction()) + || functionName.equals(Operator.LOGICAL_OR.getFunction())) + && args.size() == 2) { + List navigableOperands = + flattenNavigableOperands(navigableExpr, functionName); + if (navigableOperands.stream().anyMatch(CanonicalizationOptimizer::isComprehensionAccuVar)) { + return Optional.empty(); + } + List operands = new ArrayList<>(); + for (CelNavigableMutableExpr navOp : navigableOperands) { + operands.add(navOp.expr()); + } + operands.sort(EXPR_COMPARATOR); + List uniqueSorted = new ArrayList<>(); + for (CelMutableExpr op : operands) { + if (uniqueSorted.isEmpty() + || EXPR_COMPARATOR.compare(op, Iterables.getLast(uniqueSorted)) != 0) { + uniqueSorted.add(op); + } + } + CelMutableExpr rebuilt = uniqueSorted.get(0); + for (int i = 1; i < uniqueSorted.size(); i++) { + rebuilt = + CelMutableExpr.ofCall( + expr.id(), CelMutableCall.create(functionName, rebuilt, uniqueSorted.get(i))); + } + if (EXPR_COMPARATOR.compare(rebuilt, expr) == 0) { + return Optional.empty(); + } + return Optional.of(rebuilt); + } + + if ((functionName.equals(Operator.EQUALS.getFunction()) + || functionName.equals(Operator.NOT_EQUALS.getFunction())) + && args.size() == 2) { + CelMutableExpr arg0 = args.get(0); + CelMutableExpr arg1 = args.get(1); + if (EXPR_COMPARATOR.compare(arg0, arg1) > 0) { + return Optional.of( + CelMutableExpr.ofCall(expr.id(), CelMutableCall.create(functionName, arg1, arg0))); + } + return Optional.empty(); + } + + if (functionName.equals(Operator.LOGICAL_NOT.getFunction()) && args.size() == 1) { + CelMutableExpr target = args.get(0); + if (isCallWithArgCount(target, Operator.LOGICAL_NOT.getFunction(), 1)) { + return Optional.of(target.call().args().get(0)); + } + if (isCallWithArgCount(target, Operator.LOGICAL_AND.getFunction(), 2)) { + List subArgs = target.call().args(); + return Optional.of( + CelMutableExpr.ofCall( + expr.id(), + CelMutableCall.create( + Operator.LOGICAL_OR.getFunction(), + negate(subArgs.get(0)), + negate(subArgs.get(1))))); + } + if (isCallWithArgCount(target, Operator.LOGICAL_OR.getFunction(), 2)) { + List subArgs = target.call().args(); + return Optional.of( + CelMutableExpr.ofCall( + expr.id(), + CelMutableCall.create( + Operator.LOGICAL_AND.getFunction(), + negate(subArgs.get(0)), + negate(subArgs.get(1))))); + } + if (isCallWithArgCount(target, Operator.EQUALS.getFunction(), 2)) { + List subArgs = target.call().args(); + return Optional.of( + CelMutableExpr.ofCall( + expr.id(), + CelMutableCall.create( + Operator.NOT_EQUALS.getFunction(), subArgs.get(0), subArgs.get(1)))); + } + if (isCallWithArgCount(target, Operator.NOT_EQUALS.getFunction(), 2)) { + List subArgs = target.call().args(); + return Optional.of( + CelMutableExpr.ofCall( + expr.id(), + CelMutableCall.create( + Operator.EQUALS.getFunction(), subArgs.get(0), subArgs.get(1)))); + } + if (target.getKind() == Kind.COMPREHENSION) { + CelMutableComprehension comp = target.comprehension(); + if (isExistsMacro(mutableAst, target.id(), comp)) { + return negateComprehension(mutableAst, target.id(), comp, true); + } else if (isAllMacro(mutableAst, target.id(), comp)) { + return negateComprehension(mutableAst, target.id(), comp, false); + } + } + } + + return Optional.empty(); + } + + private static Optional negateComprehension( + CelMutableAst mutableAst, long compId, CelMutableComprehension comp, boolean isExists) { + CelMutableCall stepCall = comp.loopStep().call(); + CelMutableExpr predicate = getPredicateFromLoopStep(stepCall); + CelMutableExpr newLoopStep = + CelMutableExpr.ofCall( + comp.loopStep().id(), + CelMutableCall.create( + (isExists ? Operator.LOGICAL_AND : Operator.LOGICAL_OR).getFunction(), + CelMutableExpr.ofIdent(comp.accuVar()), + negate(predicate))); + CelMutableExpr newAccuInit = CelMutableExpr.ofConstant(CelConstant.ofValue(isExists)); + CelMutableExpr newLoopCondition = + CelMutableExpr.ofCall( + comp.loopCondition().id(), + CelMutableCall.create( + Operator.NOT_STRICTLY_FALSE.getFunction(), + isExists + ? CelMutableExpr.ofIdent(comp.accuVar()) + : negate(CelMutableExpr.ofIdent(comp.accuVar())))); + CelMutableComprehension newComp = + CelMutableComprehension.create( + comp.iterVar(), + comp.iterVar2(), + comp.iterRange(), + comp.accuVar(), + newAccuInit, + newLoopCondition, + newLoopStep, + comp.result()); + updateMacroCallForQuantifier( + mutableAst, compId, (isExists ? Operator.ALL : Operator.EXISTS).getFunction()); + return Optional.of(CelMutableExpr.ofComprehension(compId, newComp)); + } + + private static CelMutableExpr negate(CelMutableExpr expr) { + return CelMutableExpr.ofCall( + expr.id(), CelMutableCall.create(Operator.LOGICAL_NOT.getFunction(), expr)); + } + + private static void updateMacroCallForQuantifier( + CelMutableAst mutableAst, long compId, String newFunctionName) { + if (!mutableAst.source().getMacroCalls().containsKey(compId)) { + return; + } + CelMutableExpr macroCall = mutableAst.source().getMacroCalls().get(compId); + if (macroCall.getKind() != Kind.CALL) { + throw new IllegalStateException( + "Expected macro call to be of kind CALL, but got: " + macroCall.getKind()); + } + CelMutableCall call = macroCall.call(); + if (call.args().size() < 2) { + throw new IllegalStateException( + "Expected macro call to have at least 2 arguments, but got: " + call.args().size()); + } + CelMutableExpr predicateArg = Iterables.getLast(call.args()); + CelMutableExpr notPredicate; + if (isCallWithArgCount(predicateArg, Operator.LOGICAL_NOT.getFunction(), 1)) { + notPredicate = predicateArg.call().args().get(0); + } else { + notPredicate = + CelMutableExpr.ofCall( + 0, CelMutableCall.create(Operator.LOGICAL_NOT.getFunction(), predicateArg)); + } + List newArgs = new ArrayList<>(call.args()); + newArgs.set(newArgs.size() - 1, notPredicate); + CelMutableCall newCall = + call.target().isPresent() + ? CelMutableCall.create(call.target().get(), newFunctionName, newArgs) + : CelMutableCall.create(newFunctionName, newArgs); + mutableAst.source().addMacroCalls(compId, CelMutableExpr.ofCall(macroCall.id(), newCall)); + } + + private static List flattenNavigableOperands( + CelNavigableMutableExpr expr, String functionName) { + List result = new ArrayList<>(); + flattenNavigableOperandsRec(expr, functionName, result); + return result; + } + + private static void flattenNavigableOperandsRec( + CelNavigableMutableExpr expr, String functionName, List result) { + if (expr.getKind() == Kind.CALL + && expr.expr().call().function().equals(functionName) + && expr.expr().call().args().size() == 2) { + ImmutableList children = expr.children().collect(toImmutableList()); + if (children.size() == 2) { + flattenNavigableOperandsRec(children.get(0), functionName, result); + flattenNavigableOperandsRec(children.get(1), functionName, result); + return; + } + } + result.add(expr); + } + + private static CelMutableExpr getPredicateFromLoopStep(CelMutableCall stepCall) { + return stepCall.args().get(1); + } + + private static boolean isExistsMacro( + CelMutableAst mutableAst, long compId, CelMutableComprehension comp) { + return isStandardMacroCall(mutableAst, compId, Operator.EXISTS.getFunction()) + && isBooleanAccuInit(comp, false) + && isNotStrictlyFalseLoopCondition(comp, true) + && isLoopStepWithAccuVar(comp, Operator.LOGICAL_OR.getFunction()); + } + + private static boolean isAllMacro( + CelMutableAst mutableAst, long compId, CelMutableComprehension comp) { + return isStandardMacroCall(mutableAst, compId, Operator.ALL.getFunction()) + && isBooleanAccuInit(comp, true) + && isNotStrictlyFalseLoopCondition(comp, false) + && isLoopStepWithAccuVar(comp, Operator.LOGICAL_AND.getFunction()); + } + + private static boolean isStandardMacroCall( + CelMutableAst mutableAst, long compId, String expectedMacroFunction) { + if (!mutableAst.source().getMacroCalls().containsKey(compId)) { + return true; + } + CelMutableExpr macroCall = mutableAst.source().getMacroCalls().get(compId); + return macroCall.getKind() == Kind.CALL + && macroCall.call().function().equals(expectedMacroFunction); + } + + private static boolean isBooleanAccuInit(CelMutableComprehension comp, boolean expectedValue) { + return comp.accuInit().getKind() == Kind.CONSTANT + && comp.accuInit().constant().getKind() == CelConstant.Kind.BOOLEAN_VALUE + && comp.accuInit().constant().booleanValue() == expectedValue; + } + + private static boolean isNotStrictlyFalseLoopCondition( + CelMutableComprehension comp, boolean expectNot) { + if (comp.loopCondition().getKind() != Kind.CALL) { + throw new IllegalStateException( + "Expected comprehension loopCondition to be a CALL, but got: " + + comp.loopCondition().getKind()); + } + CelMutableCall call = comp.loopCondition().call(); + if (!call.function().equals(Operator.NOT_STRICTLY_FALSE.getFunction()) + && !call.function().equals(Operator.OLD_NOT_STRICTLY_FALSE.getFunction())) { + throw new IllegalStateException( + "Expected comprehension loopCondition to be @not_strictly_false, but got: " + + call.function()); + } + if (call.args().size() != 1) { + throw new IllegalStateException( + "Expected @not_strictly_false to have exactly 1 argument, but got: " + + call.args().size()); + } + CelMutableExpr arg = call.args().get(0); + if (expectNot) { + if (!isCallWithArgCount(arg, Operator.LOGICAL_NOT.getFunction(), 1)) { + return false; + } + arg = arg.call().args().get(0); + } + return isIdent(arg, comp.accuVar()); + } + + private static boolean isLoopStepWithAccuVar( + CelMutableComprehension comp, String expectedFunction) { + if (!isCallWithArgCount(comp.loopStep(), expectedFunction, 2)) { + return false; + } + List args = comp.loopStep().call().args(); + return isIdent(args.get(0), comp.accuVar()) || isIdent(args.get(1), comp.accuVar()); + } + + private static boolean isIdent(CelMutableExpr expr, String name) { + return expr.getKind() == Kind.IDENT && expr.ident().name().equals(name); + } + + private static boolean isCallWithArgCount( + CelMutableExpr expr, String functionName, int argCount) { + return expr.getKind() == Kind.CALL + && expr.call().function().equals(functionName) + && expr.call().args().size() == argCount; + } + + /** Options to configure how Canonicalization behaves. */ + @AutoValue + abstract static class CanonicalizationOptions { + abstract int maxIterationLimit(); + + /** Builder for configuring the {@link CanonicalizationOptions}. */ + @AutoValue.Builder + abstract static class Builder { + + /** + * Limit the number of iterations while performing canonicalization. An exception is thrown if + * the iteration count exceeds the set value. + */ + abstract Builder maxIterationLimit(int value); + + abstract CanonicalizationOptions build(); + + Builder() {} + } + + /** Returns a new options builder with recommended defaults pre-configured. */ + static Builder newBuilder() { + return new AutoValue_CanonicalizationOptimizer_CanonicalizationOptions.Builder() + .maxIterationLimit(500); + } + + CanonicalizationOptions() {} + } + + private CanonicalizationOptimizer(CanonicalizationOptions canonicalizationOptions) { + this.canonicalizationOptions = canonicalizationOptions; + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java b/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java index c0491085f..a7e2be8b7 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstAlphaHasher.java @@ -24,7 +24,9 @@ import dev.cel.common.ast.CelConstant; import dev.cel.common.ast.CelExpr; import java.util.ArrayList; +import java.util.HashMap; import java.util.List; +import java.util.Map; import org.jspecify.annotations.Nullable; /** @@ -83,16 +85,11 @@ private static void hashAst(CelExpr expr, @Nullable Scope scope, HasherContext c context.hasher.putByte((byte) 0); // 0 = bound context.hasher.putInt(bIdx); } else { - int fIdx = -1; - for (int i = 0; i < context.freeVars.size(); i++) { - if (context.freeVars.get(i).ident().name().equals(name)) { - fIdx = i; - break; - } - } - if (fIdx == -1) { + Integer fIdx = context.freeVarIndices.get(name); + if (fIdx == null) { context.freeVars.add(expr); fIdx = context.freeVars.size() - 1; + context.freeVarIndices.put(name, fIdx); } context.hasher.putByte((byte) 1); // 1 = free context.hasher.putInt(fIdx); @@ -100,12 +97,10 @@ private static void hashAst(CelExpr expr, @Nullable Scope scope, HasherContext c break; case SELECT: hashAst(expr.select().operand(), scope, context); - context.hasher.putInt(expr.select().field().length()); context.hasher.putString(expr.select().field(), UTF_8); context.hasher.putBoolean(expr.select().testOnly()); break; case CALL: - context.hasher.putInt(expr.call().function().length()); context.hasher.putString(expr.call().function(), UTF_8); context.hasher.putBoolean(expr.call().target().isPresent()); if (expr.call().target().isPresent()) { @@ -210,6 +205,7 @@ private static void hashConstant(CelConstant constant, HasherContext context) { private static final class HasherContext { final Hasher hasher; + final Map freeVarIndices = new HashMap<>(); final List freeVars = new ArrayList<>(); HasherContext(HashFunction hashFunction) { diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index e3bb1bfaf..3964d68a1 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -741,7 +741,7 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes))); typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes))); - boolean isDynamic = ast.getType(exprId).map(SimpleType.DYN::equals).orElse(true); + boolean isDynamic = ast.getTypeOrThrow(exprId).equals(SimpleType.DYN); BoolExpr isApprox = ctx.mkBool(!isDynamic); return TranslatedValue.propagateStrict( ctx, typeSystem, callRes, Optional.of(expr), isApprox, args); @@ -877,10 +877,6 @@ private TranslatedValue translateDynamicComprehension( ArrayExpr mapPresence = isMap ? (ArrayExpr) typeSystem.getMapPresence(typeSystem.getMapRef(iterRange)) : null; - if (isMap) { - applyBoundedMapBijection(mapPresence, seq, lengthExpr); - } - BoolExpr isTruncated = ctx.mkGt(lengthExpr, ctx.mkInt(comprehensionUnrollLimit)); truncationConditions.add(isTruncated); @@ -893,14 +889,15 @@ private TranslatedValue translateDynamicComprehension( } } - private void applyBoundedMapBijection( + private BoolExpr getBoundedMapBijection( ArrayExpr mapPresence, SeqExpr seq, ArithExpr lengthExpr) { + List constraints = new ArrayList<>(); for (int i = 0; i < comprehensionUnrollLimit; i++) { for (int j = i + 1; j < comprehensionUnrollLimit; j++) { BoolExpr validPair = ctx.mkLt(ctx.mkInt(j), lengthExpr); BoolExpr notEqual = ctx.mkNot(ctx.mkEq(ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkNth(seq, ctx.mkInt(j)))); - typeConstraints.add(ctx.mkImplies(validPair, notEqual)); + constraints.add(ctx.mkImplies(validPair, notEqual)); } } @@ -915,7 +912,8 @@ private void applyBoundedMapBijection( ctx.mkStore(seqMap, ctx.mkNth(seq, ctx.mkInt(i)), ctx.mkTrue()), seqMap); } - typeConstraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap))); + constraints.add(ctx.mkImplies(isNotTruncated, ctx.mkEq(mapPresence, seqMap))); + return CelZ3TypeSystem.mkAndFlattened(ctx, constraints); } private TranslatedValue[] evaluateLoopCondAndStep( @@ -1230,7 +1228,7 @@ private BoolExpr createTypeConstraint(Expr val, long exprId, CelAbstractSynta .orElseThrow( () -> new IllegalArgumentException("Type not found for expr ID: " + exprId)); BoolExpr typeConstraint = createTypeConstraintForType(val, type); - return ctx.mkOr(typeSystem.isError(val), typeSystem.isUnknown(val), typeConstraint); + return ctx.mkOr(typeSystem.isErrorOrUnknown(val), typeConstraint); } private BoolExpr createTypeConstraintForType(Expr val, CelType type) { @@ -1247,9 +1245,10 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { } Expr optRef = typeSystem.getOptionalRef(val); BoolExpr hasValue = typeSystem.optHasValue(optRef); - BoolExpr valConstraint = - createTypeConstraintForType(typeSystem.getOptionalValue(optRef), paramType); - return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, valConstraint)); + Expr optVal = typeSystem.getOptionalValue(optRef); + BoolExpr optValNotError = ctx.mkNot(typeSystem.isError(optVal)); + BoolExpr valConstraint = createTypeConstraintForType(optVal, paramType); + return ctx.mkAnd(isOpt, ctx.mkImplies(hasValue, ctx.mkAnd(optValNotError, valConstraint))); } if (type.equals(SimpleType.BOOL)) { return (BoolExpr) ctx.mkApp(typeSystem.boolCons().getTesterDecl(), val); @@ -1258,15 +1257,15 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { Expr unwrapped = ctx.mkApp(typeSystem.intCons().getAccessorDecls()[0], val); return ctx.mkAnd( ctx.mkApp(typeSystem.intCons().getTesterDecl(), val), - ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MIN_INT64)), - ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MAX_INT64))); + ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MIN_INT64)), + ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MAX_INT64))); } if (type.equals(SimpleType.UINT)) { Expr unwrapped = ctx.mkApp(typeSystem.uintCons().getAccessorDecls()[0], val); return ctx.mkAnd( ctx.mkApp(typeSystem.uintCons().getTesterDecl(), val), ctx.mkGe((ArithExpr) unwrapped, ctx.mkInt(0)), - ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelZ3TypeSystem.MAX_UINT64))); + ctx.mkLe((ArithExpr) unwrapped, ctx.mkInt(CelNumericBounds.MAX_UINT64))); } if (type.equals(SimpleType.DOUBLE)) { return (BoolExpr) ctx.mkApp(typeSystem.doubleCons().getTesterDecl(), val); @@ -1289,15 +1288,13 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { } if (type instanceof ListType) { - // Lists are explicitly bounded (sequence theory). We're safe in using for-all quantifiers - // here. + // Constrain list elements using bounded unrolling up to comprehensionUnrollLimit rather + // than Z3 forall quantifiers to prevent MBQI quantifier instantiation loops. + // Assert: isList(val) ∧ for all unrolled 0 <= i < length: ¬isError(seq[i]) ∧ + // typeConstraint(seq[i]) BoolExpr isList = typeSystem.isList(val); CelType elemType = ((ListType) type).elemType(); - if (elemType.equals(SimpleType.DYN)) { - return isList; - } - // isList(val) ∧ ∀i. (0 <= i < length) ⇒ elemType(seq[i]) Expr listRef = typeSystem.getListRef(val); SeqExpr seq = typeSystem.getSeq(listRef); Expr length = ctx.mkLength(seq); @@ -1307,20 +1304,62 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { for (int i = 0; i < comprehensionUnrollLimit; i++) { IntExpr idx = ctx.mkInt(i); Expr elem = ctx.mkNth(seq, idx); - BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType); BoolExpr validIndex = ctx.mkLt(idx, length); + // Assert ¬isError(elem) as a domain invariant so Z3 never synthesizes an Error element in + // list(dyn). For concrete types, this is already implied by createTypeConstraintForType. + boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkNot(typeSystem.isError(elem)))); + BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType); boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint)); - BoolExpr outOfBounds = ctx.mkGe(idx, length); - boundsAndTypes.add(ctx.mkImplies(outOfBounds, ctx.mkEq(elem, typeSystem.mkUnknown()))); } return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); } if (type instanceof MapType) { - // Do NOT emit a for-all quantifier over map keys here. - // Doing so forces MBQI into an infinite loop. Structural equivalence of dynamic keys is - // naturally constrained by the primitive key assertions in getStructuralEquality(). - return typeSystem.isMap(val); + // Do NOT emit a for-all quantifier over map keys or values here. + // Doing so forces MBQI into an infinite loop. Instead, constrain keys and values using + // bounded unrolling over the key sequence up to comprehensionUnrollLimit. + // Assert: isMap(val) ∧ for all unrolled 0 <= i < length: isPrimitiveKey(key) ∧ ¬isError(key) + // ∧ (presence(key) ⇒ ¬isError(val) ∧ typeConstraint(val)) + BoolExpr isMap = typeSystem.isMap(val); + MapType mapType = (MapType) type; + CelType keyType = mapType.keyType(); + CelType valType = mapType.valueType(); + + Expr mapRef = typeSystem.getMapRef(val); + SeqExpr seq = typeSystem.getMapKeys(mapRef); + Expr length = ctx.mkLength(seq); + ArrayExpr mapValues = (ArrayExpr) typeSystem.getMapValues(mapRef); + ArrayExpr mapPresence = (ArrayExpr) typeSystem.getMapPresence(mapRef); + + List boundsAndTypes = new ArrayList<>(); + boundsAndTypes.add(isMap); + boundsAndTypes.add(getBoundedMapBijection(mapPresence, seq, (ArithExpr) length)); + + for (int i = 0; i < comprehensionUnrollLimit; i++) { + IntExpr idx = ctx.mkInt(i); + Expr key = ctx.mkNth(seq, idx); + BoolExpr validIndex = ctx.mkLt(idx, length); + + BoolExpr isKeyPrim = typeSystem.isPrimitiveKey(key); + BoolExpr keyNotError = ctx.mkNot(typeSystem.isError(key)); + // Assert isKeyPrim ∧ ¬isError(key) so Z3 never synthesizes a non-primitive or Error key in + // map(dyn, ...). For concrete map types, this is already implied by keyType constraints. + boundsAndTypes.add(ctx.mkImplies(validIndex, ctx.mkAnd(isKeyPrim, keyNotError))); + boundsAndTypes.add(ctx.mkImplies(validIndex, createTypeConstraintForType(key, keyType))); + + BoolExpr presence = (BoolExpr) ctx.mkSelect(mapPresence, key); + BoolExpr validEntry = ctx.mkAnd(validIndex, presence); + + Expr mapVal = ctx.mkSelect(mapValues, key); + BoolExpr valNotError = + unknownIdentifiers.isEmpty() + ? ctx.mkNot(typeSystem.isErrorOrUnknown(mapVal)) + : ctx.mkNot(typeSystem.isError(mapVal)); + boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError)); + boundsAndTypes.add(ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType))); + } + + return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); } if (type.kind() == CelKind.STRUCT) { return ctx.mkAnd( @@ -1373,6 +1412,12 @@ private Optional toCacheKey(CelExpr expr) { case CONSTANT: return Optional.of(expr.constant()); case LIST: + if (!expr.list().optionalIndices().isEmpty()) { + // Do not cache lists with optional elements. Optional elements conditionally alter + // sequence length and presence via ITE branches at runtime; caching would collide + // [1, 2] with [?1, 2] and freeze conditional evaluations to a static reference. + return Optional.empty(); + } ImmutableList.Builder builder = ImmutableList.builder(); for (CelExpr elem : expr.list().elements()) { Optional elemKey = toCacheKey(elem); diff --git a/verifier/src/main/java/dev/cel/verifier/CelNumericBounds.java b/verifier/src/main/java/dev/cel/verifier/CelNumericBounds.java new file mode 100644 index 000000000..8d2184c72 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/CelNumericBounds.java @@ -0,0 +1,105 @@ +// 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.primitives.UnsignedLong; +import dev.cel.common.annotations.Internal; +import java.util.Optional; + +/** + * Utility for computing matching integer and unsigned integer ranges for IEEE-754 double-precision + * floating-point constants in Z3 verification. + */ +@Internal +public final class CelNumericBounds { + + /** Minimum representable signed 64-bit integer string. */ + public static final String MIN_INT64 = "-9223372036854775808"; + + /** Maximum representable signed 64-bit integer string. */ + public static final String MAX_INT64 = "9223372036854775807"; + + /** Maximum representable unsigned 64-bit integer string. */ + public static final String MAX_UINT64 = "18446744073709551615"; + + private static final double TWO_TO_63 = Math.scalb(1.0, 63); + private static final double TWO_TO_64 = Math.scalb(1.0, 64); + + @AutoValue + abstract static class IntRange { + abstract long min(); + + abstract long max(); + + static IntRange of(long min, long max) { + return new AutoValue_CelNumericBounds_IntRange(min, max); + } + } + + @AutoValue + abstract static class UintRange { + abstract String min(); + + abstract String max(); + + static UintRange of(String min, String max) { + return new AutoValue_CelNumericBounds_UintRange(min, max); + } + } + + private static boolean isMathematicalInteger(double vDouble) { + return Double.isFinite(vDouble) && vDouble == Math.rint(vDouble); + } + + static Optional getMatchingIntRange(double vDouble) { + if (!isMathematicalInteger(vDouble) || vDouble < -TWO_TO_63 || vDouble > TWO_TO_63) { + return Optional.empty(); + } + long minL = (long) vDouble; + while (minL > Long.MIN_VALUE && (double) (minL - 1) == vDouble) { + minL--; + } + long maxL = (long) vDouble; + while (maxL < Long.MAX_VALUE && (double) (maxL + 1) == vDouble) { + maxL++; + } + return Optional.of(IntRange.of(minL, maxL)); + } + + static Optional getMatchingUintRange(double vDouble) { + if (!isMathematicalInteger(vDouble) || vDouble < 0 || vDouble > TWO_TO_64) { + return Optional.empty(); + } + // XOR with Long.MIN_VALUE (0x8000000000000000L) flips bit 63 to 1, encoding unsigned values + // >= 2^63 into Java's two's-complement signed long representation. + long uBits = + vDouble < TWO_TO_63 ? (long) vDouble : (long) (vDouble - TWO_TO_63) ^ Long.MIN_VALUE; + UnsignedLong uVal = UnsignedLong.fromLongBits(uBits); + UnsignedLong minU = uVal; + while (!minU.equals(UnsignedLong.ZERO) + && minU.minus(UnsignedLong.ONE).doubleValue() == vDouble) { + minU = minU.minus(UnsignedLong.ONE); + } + UnsignedLong maxU = uVal; + while (!maxU.equals(UnsignedLong.MAX_VALUE) + && maxU.plus(UnsignedLong.ONE).doubleValue() == vDouble) { + maxU = maxU.plus(UnsignedLong.ONE); + } + return Optional.of(UintRange.of(minU.toString(), maxU.toString())); + } + + private CelNumericBounds() {} +} diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierFactory.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierFactory.java index da48ec484..d761428d6 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierFactory.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierFactory.java @@ -14,14 +14,43 @@ package dev.cel.verifier; +import dev.cel.bundle.Cel; +import dev.cel.bundle.CelFactory; +import dev.cel.checker.CelChecker; +import dev.cel.compiler.CelCompiler; +import dev.cel.compiler.CelCompilerFactory; +import dev.cel.parser.CelParser; +import dev.cel.runtime.CelRuntime; /** Factory class for producing AST verifiers using Z3. */ public final class CelVerifierFactory { - /** Create a builder for configuring a {@link CelVerifier}. */ + /** + * Create a builder for configuring a {@link CelVerifier}. + * + * @deprecated Prefer passing a {@link Cel} environment using {@link #newVerifier(Cel)} to enable + * canonicalization and expression re-typechecking during verification. + */ + @Deprecated public static CelVerifierBuilder newVerifier() { return CelVerifierZ3Impl.newBuilder(); } + /** Create a builder for configuring a {@link CelVerifier} with a CEL environment. */ + public static CelVerifierBuilder newVerifier(Cel cel) { + return CelVerifierZ3Impl.newBuilder(cel); + } + + /** Create a builder for configuring a {@link CelVerifier} with a CEL environment. */ + public static CelVerifierBuilder newVerifier(CelCompiler celCompiler, CelRuntime celRuntime) { + return newVerifier(CelFactory.combine(celCompiler, celRuntime)); + } + + /** Create a builder for configuring a {@link CelVerifier} with a CEL environment. */ + public static CelVerifierBuilder newVerifier( + CelParser celParser, CelChecker celChecker, CelRuntime celRuntime) { + return newVerifier(CelCompilerFactory.combine(celParser, celChecker), celRuntime); + } + private CelVerifierFactory() {} } diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index 510d88ec0..62b104afa 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -27,9 +27,14 @@ import com.microsoft.z3.Params; import com.microsoft.z3.Solver; import com.microsoft.z3.Status; +import dev.cel.bundle.Cel; +import dev.cel.bundle.CelFactory; import dev.cel.common.CelAbstractSyntaxTree; import dev.cel.common.types.CelType; import dev.cel.common.types.CelTypeProvider; +import dev.cel.optimizer.CelOptimizationException; +import dev.cel.optimizer.CelOptimizer; +import dev.cel.optimizer.CelOptimizerFactory; import dev.cel.verifier.axioms.CelZ3FunctionAxiom; import dev.cel.verifier.axioms.CelZ3StandardAxioms; import java.time.Duration; @@ -59,14 +64,25 @@ public Optional findType(String typeName) { } }; + private static final CanonicalizationOptimizer CANONICALIZATION_OPTIMIZER = + CanonicalizationOptimizer.newInstance( + CanonicalizationOptimizer.CanonicalizationOptions.newBuilder().build()); + private final Duration timeout; private final int comprehensionUnrollLimit; private final ImmutableSet unknownIdentifiers; private final CelZ3FunctionRegistry functionRegistry; private final CelTypeProvider typeProvider; + @SuppressWarnings("Immutable") // Cel environment is immutable, just not marked as such + private final Cel cel; + static Builder newBuilder() { - return new Builder(); + return new Builder(CelFactory.plannerCelBuilder().build()); + } + + static Builder newBuilder(Cel cel) { + return new Builder(Preconditions.checkNotNull(cel)); } static final class Builder implements CelVerifierBuilder { @@ -74,14 +90,16 @@ static final class Builder implements CelVerifierBuilder { private int comprehensionUnrollLimit; private final ImmutableSet.Builder unknownIdentifiers; private final ImmutableList.Builder functionAxioms; + private final Cel cel; private CelTypeProvider typeProvider; - private Builder() { + private Builder(Cel cel) { this.timeout = Duration.ofSeconds(10); this.comprehensionUnrollLimit = 5; this.unknownIdentifiers = ImmutableSet.builder(); this.functionAxioms = ImmutableList.builder(); this.typeProvider = EMPTY_TYPE_PROVIDER; + this.cel = cel; } @Override @@ -137,7 +155,12 @@ public CelVerifier build() { CelZ3FunctionRegistry registry = CelZ3FunctionRegistry.create(allFunctionAxioms); return new CelVerifierZ3Impl( - timeout, comprehensionUnrollLimit, unknownIdentifiers.build(), registry, typeProvider); + timeout, + comprehensionUnrollLimit, + unknownIdentifiers.build(), + registry, + typeProvider, + cel); } } @@ -160,6 +183,18 @@ public CelVerificationResult verifyEquivalence( CelAbstractSyntaxTree astA, CelAbstractSyntaxTree astB) throws CelVerificationException { Preconditions.checkArgument(astA.isChecked(), "astA must be type-checked."); Preconditions.checkArgument(astB.isChecked(), "astB must be type-checked."); + CelOptimizer optimizer = + CelOptimizerFactory.standardCelOptimizerBuilder(cel) + .addAstOptimizers( + CanonicalizationOptimizer.newInstance( + CanonicalizationOptimizer.CanonicalizationOptions.newBuilder().build())) + .build(); + try { + astA = optimizer.optimize(astA); + astB = optimizer.optimize(astB); + } catch (CelOptimizationException e) { + // Fall back to original ASTs if canonicalization or re-typechecking fails + } try (Context ctx = new Context(ImmutableMap.of("model", "true"))) { CelAstToZ3Translator translator = new CelAstToZ3Translator( @@ -303,8 +338,10 @@ CelVerificationResult verifyImplication( /* isCounterexample= */ true)); case TRUNCATED: return CelVerificationResult.inconclusive( - String.format("Inconclusive: %s holds within the current loop unroll limit, but" - + " may be violated for larger collections.", subjectName.toLowerCase(Locale.US))); + String.format( + "Inconclusive: %s holds within the current loop unroll limit, but" + + " may be violated for larger collections.", + subjectName.toLowerCase(Locale.US))); case NO_MATCH: return CelVerificationResult.verified(); case SOLVER_UNKNOWN: @@ -485,12 +522,14 @@ private static String getCounterexampleString( int comprehensionUnrollLimit, ImmutableSet unknownIdentifiers, CelZ3FunctionRegistry functionRegistry, - CelTypeProvider typeProvider) { + CelTypeProvider typeProvider, + Cel cel) { this.timeout = timeout; this.comprehensionUnrollLimit = comprehensionUnrollLimit; this.unknownIdentifiers = unknownIdentifiers; this.functionRegistry = functionRegistry; this.typeProvider = typeProvider; + this.cel = 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 2355d36bf..6e5c519fe 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -24,14 +24,17 @@ import com.microsoft.z3.Model; import com.microsoft.z3.RatNum; import java.util.ArrayList; +import java.util.HashSet; +import java.util.LinkedHashSet; import java.util.List; +import java.util.Set; import org.jspecify.annotations.Nullable; /** Generates human-readable counterexample strings from Z3 models. */ @SuppressWarnings({"unchecked", "rawtypes"}) // Z3 Java API uses raw types. final class CelZ3CounterexampleGenerator { - private static final int MAX_LIST_ELEMENTS_TO_PRINT = 15; + private static final int MAX_ELEMENTS_TO_PRINT = 15; private CelZ3CounterexampleGenerator() {} @@ -127,6 +130,8 @@ private static String formatExpr( 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 = @@ -156,8 +161,10 @@ private static String reconstructList( model, ctx.mkLength(typeSystem.getSeq(listRef)), String.format("Z3 failed to evaluate length for list %s", listRef)); - int length = ((IntNum) lenExpr).getInt(); - int printLimit = Math.min(length, MAX_LIST_ELEMENTS_TO_PRINT); + Preconditions.checkState( + lenExpr instanceof IntNum, "Expected IntNum length for list %s, got %s", listRef, lenExpr); + long length = ((IntNum) lenExpr).getInt64(); + int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT); List elements = new ArrayList<>(); for (int i = 0; i < printLimit; i++) { Expr elem = @@ -177,24 +184,33 @@ private static String reconstructList( private static String reconstructMap( Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr mapRef) { - Expr presenceArray = + Expr lenExpr = evaluateStrict( model, - typeSystem.getMapPresence(mapRef), - String.format("Z3 failed to evaluate presence array natively for map %s", mapRef)); - - List> keys = new ArrayList<>(); - extractKeys(presenceArray, keys); + ctx.mkLength(typeSystem.getMapKeys(mapRef)), + String.format("Z3 failed to evaluate length for map %s", mapRef)); + Preconditions.checkState( + lenExpr instanceof IntNum, "Expected IntNum length for map %s, got %s", mapRef, lenExpr); + long length = ((IntNum) lenExpr).getInt64(); + int printLimit = (int) Math.min(length, (long) MAX_ELEMENTS_TO_PRINT); List entries = new ArrayList<>(); - for (Expr key : keys) { + Set> seenKeys = new HashSet<>(); + for (int i = 0; i < printLimit; i++) { + Expr key = + evaluateStrict( + model, + ctx.mkNth(typeSystem.getMapKeys(mapRef), ctx.mkInt(i)), + String.format("Z3 failed to evaluate map key at index %d for map %s", i, mapRef)); + if (!seenKeys.add(key)) { + continue; + } Expr presence = evaluateStrict( model, ctx.mkSelect((ArrayExpr) typeSystem.getMapPresence(mapRef), key), String.format( "Z3 failed to evaluate map presence for key %s in map %s", key, mapRef)); - if (presence.isTrue()) { Expr value = evaluateStrict( @@ -207,17 +223,20 @@ private static String reconstructMap( + formatExpr(ctx, typeSystem, model, value)); } } + if (length > printLimit) { + entries.add("... (" + (length - printLimit) + " more entries)"); + } return "{" + String.join(", ", entries) + "}"; } private static String reconstructMessage( Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr msgRef) { - Expr valuesArray = + Expr presenceArray = evaluateStrict( model, - typeSystem.getMsgValues(msgRef), - String.format("Z3 failed to evaluate values array natively for msg %s", msgRef)); + typeSystem.getMsgPresence(msgRef), + String.format("Z3 failed to evaluate presence array natively for msg %s", msgRef)); Expr typeNameExpr = evaluateStrict( @@ -227,8 +246,8 @@ private static String reconstructMessage( String typeName = formatExpr(ctx, typeSystem, model, typeNameExpr).replace("\"", ""); - List> keys = new ArrayList<>(); - extractKeys(valuesArray, keys); + Set> keys = new LinkedHashSet<>(); + extractKeys(presenceArray, keys); List entries = new ArrayList<>(); for (Expr key : keys) { @@ -254,7 +273,7 @@ private static String reconstructMessage( return typeName + "{" + String.join(", ", entries) + "}"; } - private static void extractKeys(Expr arrayExpr, List> keys) { + private static void extractKeys(Expr arrayExpr, Set> keys) { int iterations = 0; while (true) { if (++iterations > 100_000) { @@ -266,16 +285,15 @@ private static void extractKeys(Expr arrayExpr, List> keys) { FuncDecl decl = arrayExpr.getFuncDecl(); String declName = decl.getName().toString(); - if (!declName.equals("store")) { - break; + if (declName.equals("store")) { + Expr[] args = arrayExpr.getArgs(); + Preconditions.checkState( + args.length == 3, "Z3 store array operation must have exactly 3 arguments"); + keys.add(args[1]); + arrayExpr = args[0]; + continue; } - - Expr[] args = arrayExpr.getArgs(); - Preconditions.checkState( - args.length == 3, "Z3 store array operation must have exactly 3 arguments"); - keys.add(args[1]); - - arrayExpr = args[0]; + break; } } diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3ExtensionalityAxioms.java b/verifier/src/main/java/dev/cel/verifier/CelZ3ExtensionalityAxioms.java index 2303abcaf..be1ec1475 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3ExtensionalityAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3ExtensionalityAxioms.java @@ -79,7 +79,8 @@ private static void addListAxioms( Sort listRefSort = typeSystem.listRefSort(); Sort seqSort = ctx.mkSeqSort(typeSystem.celValueSort()); - FuncDecl mkListRef = ctx.mkFuncDecl(FUNC_MK_LIST_REF, new Sort[] {seqSort}, listRefSort); + FuncDecl mkListRef = + typeSystem.internFuncDecl(FUNC_MK_LIST_REF, new Sort[] {seqSort}, listRefSort); for (Expr ref : refs) { if (isAppOf(ref, FUNC_MK_LIST_REF)) { @@ -109,7 +110,8 @@ private static void addMapAxioms( Sort presenceSort = ctx.mkArraySort(typeSystem.celValueSort(), ctx.getBoolSort()); FuncDecl mkMapRef = - ctx.mkFuncDecl(FUNC_MK_MAP_REF, new Sort[] {valuesSort, presenceSort}, mapRefSort); + typeSystem.internFuncDecl( + FUNC_MK_MAP_REF, new Sort[] {valuesSort, presenceSort}, mapRefSort); for (Expr ref : refs) { if (isAppOf(ref, FUNC_MK_MAP_REF)) { @@ -141,7 +143,7 @@ private static void addMessageAxioms( Sort presenceSort = ctx.mkArraySort(ctx.getStringSort(), ctx.getBoolSort()); FuncDecl mkMsgRef = - ctx.mkFuncDecl( + typeSystem.internFuncDecl( FUNC_MK_MSG_REF, new Sort[] {typeNameSort, valuesSort, presenceSort}, msgRefSort); for (Expr ref : refs) { diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index 3051fbd87..bd5c8874e 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -43,7 +43,6 @@ import dev.cel.common.types.SimpleType; import dev.cel.verifier.axioms.CelZ3OverloadResult; import dev.cel.verifier.axioms.CelZ3OverloadTranslator; -import java.math.BigDecimal; import java.util.ArrayList; import java.util.List; import java.util.Optional; @@ -224,6 +223,8 @@ private TranslatedValue translateOperatorCall( return translateLogicalAndOr(args, false); case LOGICAL_NOT: return translateLogicalNot(args, ast); + case NEGATE: + return translateNegate(args.get(0), ast); case EQUALS: return translateEquality(args.get(0), args.get(1), ast, /* isEquals= */ true); case NOT_EQUALS: @@ -237,7 +238,6 @@ private TranslatedValue translateOperatorCall( case MULTIPLY: case DIVIDE: case MODULO: - case NEGATE: case IN: // Indicates a type-mismatch in an operator that's not handled // by our axioms @@ -330,72 +330,84 @@ private TranslatedValue translateLogicalNot( return TranslatedValue.propagateStrict(ctx, typeSystem, baseResult, args); } + private TranslatedValue translateNegate(TranslatedValue arg, CelAbstractSyntaxTree ast) { + CelType type = extractAstTypeOrDefault(arg, ast); + Expr z3Expr = arg.z3Expr(); + + Expr result; + if (type.equals(SimpleType.INT)) { + ArithExpr intNeg = ctx.mkUnaryMinus(typeSystem.getInt(z3Expr)); + result = + typeSystem.withRuntimeError( + typeSystem.wrapInt((IntExpr) intNeg), typeSystem.checkIntOverflow(intNeg)); + } else if (type.equals(SimpleType.DOUBLE)) { + result = typeSystem.wrapDouble(ctx.mkFPNeg(typeSystem.getDouble(z3Expr))); + } else { + ArithExpr intNeg = ctx.mkUnaryMinus(typeSystem.getInt(z3Expr)); + Expr intResult = + typeSystem.withRuntimeError( + typeSystem.wrapInt((IntExpr) intNeg), typeSystem.checkIntOverflow(intNeg)); + Expr doubleResult = typeSystem.wrapDouble(ctx.mkFPNeg(typeSystem.getDouble(z3Expr))); + result = + CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) + .addCase(typeSystem.isInt(z3Expr), intResult) + .addCase(typeSystem.isDouble(z3Expr), doubleResult) + .build(typeSystem.mkError()); + } + return TranslatedValue.propagateStrict(ctx, typeSystem, result, arg); + } + private BoolExpr isNumeric(Expr arg) { return ctx.mkOr(typeSystem.isInt(arg), typeSystem.isUint(arg), typeSystem.isDouble(arg)); } private BoolExpr getNumericEqualityWithConstant( Expr symVal, CelConstant constant, CelType symType) { - Long intVal = null; - String uintVal = null; + Optional intRange = Optional.empty(); + Optional uintRange = Optional.empty(); double doubleVal; switch (constant.getKind()) { case INT64_VALUE: long vInt = constant.int64Value(); - intVal = vInt; - // Z3's infinite precision automatically evaluates `uint == -1` to false, - // but pruning it here keeps the formula smaller. + intRange = Optional.of(CelNumericBounds.IntRange.of(vInt, vInt)); if (vInt >= 0) { - uintVal = Long.toString(vInt); + uintRange = + Optional.of(CelNumericBounds.UintRange.of(Long.toString(vInt), Long.toString(vInt))); } doubleVal = (double) vInt; break; case UINT64_VALUE: long vUint = constant.uint64Value().longValue(); if (vUint >= 0) { - intVal = vUint; + intRange = Optional.of(CelNumericBounds.IntRange.of(vUint, vUint)); } - uintVal = constant.uint64Value().toString(); + String uStr = constant.uint64Value().toString(); + uintRange = Optional.of(CelNumericBounds.UintRange.of(uStr, uStr)); doubleVal = constant.uint64Value().doubleValue(); break; case DOUBLE_VALUE: double vDouble = constant.doubleValue(); doubleVal = vDouble; - if (vDouble == Math.floor(vDouble) && !Double.isInfinite(vDouble)) { - if (vDouble >= Long.MIN_VALUE && vDouble <= Long.MAX_VALUE) { - intVal = (long) vDouble; - } - if (vDouble >= 0 && vDouble <= Double.parseDouble(CelZ3TypeSystem.MAX_UINT64)) { - uintVal = BigDecimal.valueOf(vDouble).toBigInteger().toString(); - } - } + intRange = CelNumericBounds.getMatchingIntRange(vDouble); + uintRange = CelNumericBounds.getMatchingUintRange(vDouble); break; default: throw new IllegalArgumentException( "Unexpected numeric constant kind: " + constant.getKind()); } - if (isStaticallyKnown(symType)) { if (symType.kind() == CelKind.INT) { - return (intVal != null) - ? ctx.mkEq(typeSystem.getInt(symVal), ctx.mkInt(intVal)) - : ctx.mkFalse(); + return buildIntRangeExpr(intRange, typeSystem.getInt(symVal)); } else if (symType.kind() == CelKind.UINT) { - return (uintVal != null) - ? ctx.mkEq(typeSystem.getUint(symVal), ctx.mkInt(uintVal)) - : ctx.mkFalse(); + return buildUintRangeExpr(uintRange, typeSystem.getUint(symVal)); } else if (symType.kind() == CelKind.DOUBLE) { return ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); } } - BoolExpr intEq = - (intVal != null) ? ctx.mkEq(typeSystem.getInt(symVal), ctx.mkInt(intVal)) : ctx.mkFalse(); - BoolExpr uintEq = - (uintVal != null) - ? ctx.mkEq(typeSystem.getUint(symVal), ctx.mkInt(uintVal)) - : ctx.mkFalse(); + BoolExpr intEq = buildIntRangeExpr(intRange, typeSystem.getInt(symVal)); + BoolExpr uintEq = buildUintRangeExpr(uintRange, typeSystem.getUint(symVal)); BoolExpr doubleEq = ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); return (BoolExpr) @@ -406,6 +418,27 @@ private BoolExpr getNumericEqualityWithConstant( .build(ctx.mkFalse()); } + private BoolExpr buildIntRangeExpr(Optional rangeOpt, IntExpr symInt) { + return rangeOpt + .map(range -> buildIntRangeExpr(range.min(), range.max(), symInt)) + .orElseGet(ctx::mkFalse); + } + + private BoolExpr buildIntRangeExpr(long min, long max, IntExpr symInt) { + return ctx.mkAnd(ctx.mkGe(symInt, ctx.mkInt(min)), ctx.mkLe(symInt, ctx.mkInt(max))); + } + + private BoolExpr buildUintRangeExpr( + Optional rangeOpt, IntExpr symUint) { + return rangeOpt + .map(range -> buildUintRangeExpr(range.min(), range.max(), symUint)) + .orElseGet(ctx::mkFalse); + } + + private BoolExpr buildUintRangeExpr(String min, String max, IntExpr symUint) { + return ctx.mkAnd(ctx.mkGe(symUint, ctx.mkInt(min)), ctx.mkLe(symUint, ctx.mkInt(max))); + } + private BoolExpr getNumericEquality( TranslatedValue arg0, TranslatedValue arg1, CelAbstractSyntaxTree ast) { if (arg0.isNumericConstant()) { @@ -418,7 +451,7 @@ private BoolExpr getNumericEquality( CelType type0 = extractAstTypeOrDefault(arg0, ast); CelType type1 = extractAstTypeOrDefault(arg1, ast); - if (isStaticallyKnown(type0) && isStaticallyKnown(type1)) { + if (isStaticallyKnown(type0) && isStaticallyKnown(type1) && type0.kind() == type1.kind()) { return getStaticallyKnownNumericEquality(arg0.z3Expr(), type0, arg1.z3Expr()); } @@ -733,7 +766,7 @@ private Expr buildMapIndex( // Uint probes IntExpr rawUint = (IntExpr) ctx.mkITE(isUint, typeSystem.getUint(rhsTrans), ctx.mkInt(0)); - BoolExpr uintHasInt = ctx.mkLe(rawUint, ctx.mkInt(CelZ3TypeSystem.MAX_INT64)); + BoolExpr uintHasInt = ctx.mkLe(rawUint, ctx.mkInt(CelNumericBounds.MAX_INT64)); Expr uintIntKey = typeSystem.wrapInt(rawUint); BoolExpr uintHasDouble = hasExactDouble ? isUint : ctx.mkFalse(); diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index e9a1872c9..dc19a8d3a 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -55,10 +55,6 @@ @SuppressWarnings({"unchecked", "rawtypes", "AvoidObjectArrays"}) // Z3 Java API uses raw types. public final class CelZ3TypeSystem { - public static final String MIN_INT64 = "-9223372036854775808"; - public static final String MAX_INT64 = "9223372036854775807"; - public static final String MAX_UINT64 = "18446744073709551615"; - private static final String TYPE_CEL_VALUE = "CelValue"; private static final String CONS_BOOL = "Bool"; private static final String IS_BOOL = "isBool"; @@ -357,7 +353,7 @@ public Expr wrapDuration(IntExpr expr) { /** Creates a CelValue containing an integer. */ public Expr mkInt(long val) { - return ctx.mkApp(intCons.ConstructorDecl(), ctx.mkInt(val)); + return ctx.mkApp(intCons.ConstructorDecl(), ctx.mkInt(Long.toString(val))); } /** Creates a CelValue containing an unsigned integer from a string representation. */ @@ -575,6 +571,11 @@ public BoolExpr isUnknown(Expr val) { return (BoolExpr) ctx.mkApp(unknownCons.getTesterDecl(), val); } + /** Checks if the given CelValue is either an error or an unknown value. */ + public BoolExpr isErrorOrUnknown(Expr val) { + return ctx.mkOr(isError(val), isUnknown(val)); + } + /** Checks if the given CelValue is a boolean. */ public BoolExpr isBool(Expr val) { return (BoolExpr) ctx.mkApp(boolCons.getTesterDecl(), val); @@ -685,6 +686,11 @@ public Expr getBytes(Expr val) { return ctx.mkApp(bytesCons.getAccessorDecls()[0], val); } + /** Checks if the given CelValue is a valid primitive map key type. */ + public BoolExpr isPrimitiveKey(Expr val) { + return ctx.mkOr(isBool(val), isInt(val), isUint(val), isString(val), isBytes(val)); + } + /** Checks if the given CelValue is a struct (message). */ public BoolExpr isStruct(Expr val) { return isMessage(val); @@ -799,7 +805,9 @@ public Expr getMsgTypeName(Expr msgRef) { /** Checks if the given arithmetic expression overflows a 64-bit integer. */ public BoolExpr checkIntOverflow(ArithExpr result) { - return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_INT64)), ctx.mkLt(result, ctx.mkInt(MIN_INT64))); + return ctx.mkOr( + ctx.mkGt(result, ctx.mkInt(CelNumericBounds.MAX_INT64)), + ctx.mkLt(result, ctx.mkInt(CelNumericBounds.MIN_INT64))); } /** Checks if the given arithmetic expression overflows CEL Timestamp bounds. */ @@ -818,7 +826,8 @@ public BoolExpr checkDurationOverflow(ArithExpr result) { /** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */ public BoolExpr checkUintOverflow(ArithExpr result) { - return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_UINT64)), ctx.mkLt(result, ctx.mkInt(0))); + return ctx.mkOr( + ctx.mkGt(result, ctx.mkInt(CelNumericBounds.MAX_UINT64)), ctx.mkLt(result, ctx.mkInt(0))); } /** Safely concatenates two Z3 sequences. */ diff --git a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java index 032c9dcdc..506f0bbc7 100644 --- a/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java +++ b/verifier/src/main/java/dev/cel/verifier/TranslatedValue.java @@ -144,7 +144,6 @@ static TranslatedValue propagateStrict( Collection args) { List exactErrors = new ArrayList<>(); List exactUnknowns = new ArrayList<>(); - List errors = new ArrayList<>(); List unknowns = new ArrayList<>(); List taints = new ArrayList<>(); taints.add(baseTaint); @@ -164,7 +163,6 @@ static TranslatedValue propagateStrict( BoolExpr isError = ts.isError(z3Expr); BoolExpr isUnknown = ts.isUnknown(z3Expr); - errors.add(isError); unknowns.add(isUnknown); exactErrors.add( @@ -180,17 +178,18 @@ static TranslatedValue propagateStrict( return create(baseResult, celExpr, ts, anyTaint); } + List> z3Args = new ArrayList<>(); + for (TranslatedValue arg : argsList) { + if (!arg.isLiteral(ExprKind.Kind.CONSTANT)) { + z3Args.add(arg.z3Expr()); + } + } + Expr finalResult = ts.propagateErrorAndUnknown(baseResult, z3Args); + BoolExpr hasExactError = CelZ3TypeSystem.mkOrFlattened(ctx, exactErrors); BoolExpr hasExactUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, exactUnknowns); - BoolExpr hasError = CelZ3TypeSystem.mkOrFlattened(ctx, errors); BoolExpr hasUnknown = CelZ3TypeSystem.mkOrFlattened(ctx, unknowns); - Expr finalResult = - CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) - .addCase(hasUnknown, ts.mkUnknown()) - .addCase(hasError, ts.mkError()) - .build(baseResult); - BoolExpr isSafe = CelZ3TypeSystem.mkOrFlattened( ctx, diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel index 02752c10e..c397f1b45 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/axioms/BUILD.bazel @@ -22,6 +22,7 @@ java_library( "//common/types", "//extensions:comprehensions", "//extensions:optional_library", + "//verifier:numeric_bounds", "//verifier:type_system", "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:com_google_guava_guava", diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java index 292b86135..2ccb1543a 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java @@ -15,7 +15,6 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -56,9 +55,7 @@ final class GreaterAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkFPGt( - (FPExpr) typeSystem.getDouble(lhs), - (FPExpr) typeSystem.getDouble(rhs))))) + ctx.mkFPGt(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_STRING.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -82,7 +79,7 @@ final class GreaterAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLtReal( ctx, - (FPExpr) typeSystem.getDouble(rhs), + typeSystem.getDouble(rhs), ctx.mkInt2Real(typeSystem.getInt(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_UINT64_DOUBLE.celOverloadDecl(), @@ -91,7 +88,7 @@ final class GreaterAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLtReal( ctx, - (FPExpr) typeSystem.getDouble(rhs), + typeSystem.getDouble(rhs), ctx.mkInt2Real(typeSystem.getUint(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_DOUBLE_INT64.celOverloadDecl(), @@ -101,7 +98,7 @@ final class GreaterAxiom { AxiomHelpers.mkRealLtFp( ctx, ctx.mkInt2Real(typeSystem.getInt(rhs)), - (FPExpr) typeSystem.getDouble(lhs))))) + typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_DOUBLE_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -110,7 +107,7 @@ final class GreaterAxiom { AxiomHelpers.mkRealLtFp( ctx, ctx.mkInt2Real(typeSystem.getUint(rhs)), - (FPExpr) typeSystem.getDouble(lhs))))) + typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_INT64_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java index 4be0c23e2..d71f0f248 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java @@ -15,7 +15,6 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -56,9 +55,7 @@ final class GreaterEqualsAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkFPGEq( - (FPExpr) typeSystem.getDouble(lhs), - (FPExpr) typeSystem.getDouble(rhs))))) + ctx.mkFPGEq(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_STRING.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -82,7 +79,7 @@ final class GreaterEqualsAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLeReal( ctx, - (FPExpr) typeSystem.getDouble(rhs), + typeSystem.getDouble(rhs), ctx.mkInt2Real(typeSystem.getInt(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_UINT64_DOUBLE.celOverloadDecl(), @@ -91,7 +88,7 @@ final class GreaterEqualsAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLeReal( ctx, - (FPExpr) typeSystem.getDouble(rhs), + typeSystem.getDouble(rhs), ctx.mkInt2Real(typeSystem.getUint(lhs)))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_DOUBLE_INT64.celOverloadDecl(), @@ -101,7 +98,7 @@ final class GreaterEqualsAxiom { AxiomHelpers.mkRealLeFp( ctx, ctx.mkInt2Real(typeSystem.getInt(rhs)), - (FPExpr) typeSystem.getDouble(lhs))))) + typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_DOUBLE_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -110,7 +107,7 @@ final class GreaterEqualsAxiom { AxiomHelpers.mkRealLeFp( ctx, ctx.mkInt2Real(typeSystem.getUint(rhs)), - (FPExpr) typeSystem.getDouble(lhs))))) + typeSystem.getDouble(lhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_INT64_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java index e09484f28..31b1d3a21 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java @@ -15,7 +15,6 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -56,9 +55,7 @@ final class LessAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkFPLt( - (FPExpr) typeSystem.getDouble(lhs), - (FPExpr) typeSystem.getDouble(rhs))))) + ctx.mkFPLt(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_STRING.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -83,7 +80,7 @@ final class LessAxiom { AxiomHelpers.mkRealLtFp( ctx, ctx.mkInt2Real(typeSystem.getInt(lhs)), - (FPExpr) typeSystem.getDouble(rhs))))) + typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_UINT64_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -92,7 +89,7 @@ final class LessAxiom { AxiomHelpers.mkRealLtFp( ctx, ctx.mkInt2Real(typeSystem.getUint(lhs)), - (FPExpr) typeSystem.getDouble(rhs))))) + typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_DOUBLE_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -100,7 +97,7 @@ final class LessAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLtReal( ctx, - (FPExpr) typeSystem.getDouble(lhs), + typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getInt(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_DOUBLE_UINT64.celOverloadDecl(), @@ -109,7 +106,7 @@ final class LessAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLtReal( ctx, - (FPExpr) typeSystem.getDouble(lhs), + typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getUint(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_INT64_UINT64.celOverloadDecl(), diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java index e27b47631..c2466cf1b 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java @@ -15,7 +15,6 @@ package dev.cel.verifier.axioms; import com.microsoft.z3.ArithExpr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.SeqExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Comparison; @@ -56,9 +55,7 @@ final class LessEqualsAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkFPLEq( - (FPExpr) typeSystem.getDouble(lhs), - (FPExpr) typeSystem.getDouble(rhs))))) + ctx.mkFPLEq(typeSystem.getDouble(lhs), typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_STRING.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -83,7 +80,7 @@ final class LessEqualsAxiom { AxiomHelpers.mkRealLeFp( ctx, ctx.mkInt2Real(typeSystem.getInt(lhs)), - (FPExpr) typeSystem.getDouble(rhs))))) + typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_UINT64_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -92,7 +89,7 @@ final class LessEqualsAxiom { AxiomHelpers.mkRealLeFp( ctx, ctx.mkInt2Real(typeSystem.getUint(lhs)), - (FPExpr) typeSystem.getDouble(rhs))))) + typeSystem.getDouble(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_DOUBLE_INT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> @@ -100,7 +97,7 @@ final class LessEqualsAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLeReal( ctx, - (FPExpr) typeSystem.getDouble(lhs), + typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getInt(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_DOUBLE_UINT64.celOverloadDecl(), @@ -109,7 +106,7 @@ final class LessEqualsAxiom { typeSystem.wrapBool( AxiomHelpers.mkFpLeReal( ctx, - (FPExpr) typeSystem.getDouble(lhs), + typeSystem.getDouble(lhs), ctx.mkInt2Real(typeSystem.getUint(rhs)))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_INT64_UINT64.celOverloadDecl(), diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java index 9c49ef958..61e941258 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java @@ -47,7 +47,7 @@ final class TypeAxiom { // Custom approximation logic for type(): it is only approximate if the argument // is approximate AND the argument is an Error or Unknown. - BoolExpr isErrOrUnk = ctx.mkOr(typeSystem.isError(val), typeSystem.isUnknown(val)); + BoolExpr isErrOrUnk = typeSystem.isErrorOrUnknown(val); BoolExpr typeApprox = ctx.mkAnd(argApprox, isErrOrUnk); return Optional.of(CelZ3OverloadResult.create(result, typeApprox)); diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java index 8cd844214..2064047fd 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java @@ -14,12 +14,11 @@ package dev.cel.verifier.axioms; -import static dev.cel.verifier.CelZ3TypeSystem.MAX_INT64; +import static dev.cel.verifier.CelNumericBounds.MAX_INT64; import com.google.common.collect.ImmutableList; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Expr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; import com.microsoft.z3.Sort; @@ -233,8 +232,7 @@ private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions sink.accept(ctx.mkOr(typeSystem.isDouble(res), typeSystem.isError(res))); sink.accept( ctx.mkImplies( - typeSystem.isDouble(res), - ctx.mkNot(ctx.mkFPIsNaN((FPExpr) typeSystem.getDouble(res))))); + typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res))))); break; case STRING: sink.accept(ctx.mkOr(typeSystem.isString(res), typeSystem.isError(res))); diff --git a/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel new file mode 100644 index 000000000..28ce776cb --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel @@ -0,0 +1,80 @@ +load("@rules_java//java:defs.bzl", "java_binary", "java_library") +load("//publish:cel_version.bzl", "CEL_VERSION") + +package( + default_applicable_licenses = [ + "//:license", + ], + default_visibility = [ + "//verifier:__subpackages__", + ], +) + +genrule( + name = "generate_version", + outs = ["CelVersion.java"], + cmd = """cat << 'EOF' > $@ +package dev.cel.verifier.tools; + +final class CelVersion { + static final String VERSION = "%s"; + + private CelVersion() {} +} +EOF +""" % CEL_VERSION, +) + +java_library( + name = "tools_lib", + srcs = [ + "CelVerifierRepl.java", + "CelVerifierTool.java", + "CelVerifierToolCore.java", + "FormatUtils.java", + "VerificationOptions.java", + ":generate_version", + ], + tags = [ + "alt_dep=//verifier/tools", + ], + deps = [ + "//:java_jline", + "//bundle:cel", + "//common:cel_ast", + "//common:compiler_common", + "//common:options", + "//common/types", + "//common/types:cel_types", + "//common/types:type_providers", + "//compiler", + "//compiler:compiler_builder", + "//extensions", + "//parser:macro", + "//policy", + "//policy:compiler", + "//policy:compiler_factory", + "//policy:parser", + "//policy:parser_factory", + "//policy:validation_exception", + "//verifier", + "//verifier:policy_verifier", + "//verifier:policy_verifier_factory", + "//verifier:verifier_factory", + "@maven//:com_google_errorprone_error_prone_annotations", + "@maven//:com_google_guava_guava", + "@maven//:info_picocli_picocli", + ], +) + +java_binary( + name = "cel_verifier_tool", + jvm_flags = ["-Dz3.skipLibraryLoad=true"], + main_class = "dev.cel.verifier.tools.CelVerifierTool", + tags = [ + "alt_dep=//verifier/tools:cel_verifier_tool", + ], + runtime_deps = [ + ":tools_lib", + ], +) diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java new file mode 100644 index 000000000..94348ff15 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java @@ -0,0 +1,439 @@ +// 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.tools; + +import static java.nio.charset.StandardCharsets.UTF_8; + +import com.google.common.base.Ascii; +import com.google.common.collect.ImmutableList; +import dev.cel.common.CelValidationException; +import dev.cel.common.types.CelType; +import dev.cel.common.types.CelTypes; +import dev.cel.policy.CelPolicyValidationException; +import dev.cel.verifier.CelVerificationResult; +import java.io.BufferedReader; +import java.io.InputStreamReader; +import java.io.PrintStream; +import java.time.Duration; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Locale; +import java.util.Map; +import java.util.Optional; +import org.jline.reader.EndOfFileException; +import org.jline.reader.LineReader; +import org.jline.reader.LineReaderBuilder; +import org.jline.reader.UserInterruptException; +import org.jline.terminal.Terminal; +import org.jline.terminal.TerminalBuilder; + +/** Interactive REPL shell for CEL formal verification. */ +final class CelVerifierRepl { + + private CelVerifierRepl() {} + + static int runInteractiveRepl() { + LineReader lineReader = null; + BufferedReader fallbackReader = null; + try { + Terminal terminal = TerminalBuilder.builder().system(true).build(); + lineReader = + LineReaderBuilder.builder() + .terminal(terminal) + .option(LineReader.Option.DISABLE_EVENT_EXPANSION, true) + .build(); + } catch (Exception e) { + fallbackReader = new BufferedReader(new InputStreamReader(System.in, UTF_8)); + } + return runReplInternal(lineReader, fallbackReader, System.out, System.err); + } + + static int runRepl(BufferedReader reader, PrintStream out, PrintStream err) { + return runReplInternal(null, reader, out, err); + } + + private static int runReplInternal( + LineReader lineReader, BufferedReader fallbackReader, PrintStream out, PrintStream err) { + out.println("============================================================"); + out.println(" CEL Verification REPL"); + out.println(" Type :help for commands, :quit to exit."); + out.println("============================================================"); + + Map sessionVars = new HashMap<>(); + List unknownIdentifiers = new ArrayList<>(); + int timeoutSeconds = 10; + int unrollLimit = 5; + + String prompt = FormatUtils.ANSI_CYAN + "cel-verifier> " + FormatUtils.ANSI_RESET; + + while (true) { + String line; + try { + if (lineReader != null) { + line = lineReader.readLine(prompt); + } else if (fallbackReader != null) { + out.print(prompt); + out.flush(); + line = fallbackReader.readLine(); + if (line == null) { + break; // EOF + } + } else { + break; + } + } catch (UserInterruptException | EndOfFileException e) { + out.println("Goodbye!"); + break; + } catch (Exception e) { + err.println("Error reading input: " + e.getMessage()); + break; + } + + line = line.trim(); + if (line.isEmpty()) { + continue; + } + + if (line.startsWith(":")) { + if (Ascii.equalsIgnoreCase(line, ":quit") || Ascii.equalsIgnoreCase(line, ":exit")) { + out.println("Goodbye!"); + break; + } + + Optional helpArg = extractCommandArg(line, ":help"); + if (helpArg.isPresent()) { + printHelp(helpArg.get(), out); + continue; + } + + if (Ascii.equalsIgnoreCase(line, ":vars")) { + printVars(sessionVars, unknownIdentifiers, timeoutSeconds, unrollLimit, out); + continue; + } + + if (Ascii.equalsIgnoreCase(line, ":clear")) { + sessionVars.clear(); + unknownIdentifiers.clear(); + out.println("Session state reset."); + continue; + } + + Optional varArg = extractCommandArg(line, ":var"); + if (varArg.isPresent()) { + String arg = varArg.get(); + if (arg.isEmpty()) { + err.println( + "Usage: :var (e.g. :var role string, :var scores map)"); + } else { + handleVarCommand(arg, sessionVars, out, err); + } + continue; + } + + Optional unknownArg = extractCommandArg(line, ":unknown"); + if (unknownArg.isPresent()) { + String arg = unknownArg.get(); + if (arg.isEmpty()) { + err.println("Usage: :unknown "); + } else { + unknownIdentifiers.add(arg); + out.println("Added unknown identifier: '" + arg + "'"); + } + continue; + } + + Optional timeoutArg = extractCommandArg(line, ":timeout"); + if (timeoutArg.isPresent()) { + String arg = timeoutArg.get(); + if (arg.isEmpty()) { + err.println("Usage: :timeout "); + } else { + try { + int t = Integer.parseInt(arg); + if (t <= 0) { + err.println("Timeout must be a positive integer."); + } else { + timeoutSeconds = t; + out.println("Timeout set to " + timeoutSeconds + "s."); + } + } catch (NumberFormatException e) { + err.println("Invalid timeout value."); + } + } + continue; + } + + Optional unrollArg = extractCommandArg(line, ":unroll"); + if (unrollArg.isPresent()) { + String arg = unrollArg.get(); + if (arg.isEmpty()) { + err.println("Usage: :unroll "); + } else { + try { + int u = Integer.parseInt(arg); + if (u < 0) { + err.println("Unroll limit must be non-negative."); + } else { + unrollLimit = u; + out.println("Comprehension unroll limit set to " + unrollLimit + "."); + } + } catch (NumberFormatException e) { + err.println("Invalid unroll limit value."); + } + } + continue; + } + + err.println("Unknown command: " + line + ". Type :help for commands."); + continue; + } + + // Handle queries + VerificationOptions options = + VerificationOptions.builder() + .setTimeout(Duration.ofSeconds(timeoutSeconds)) + .setComprehensionUnrollLimit(unrollLimit) + .setUnknownIdentifiers(unknownIdentifiers) + .build(); + + try { + Optional satArg = extractCommandArg(line, "sat"); + Optional validArg = extractCommandArg(line, "valid"); + Optional equivArg = extractCommandArg(line, "equiv"); + + if (satArg.isPresent()) { + String arg = satArg.get(); + if (arg.isEmpty()) { + err.println("Usage: sat "); + } else { + CelVerificationResult res = + CelVerifierToolCore.checkSatisfiable(arg, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } else if (validArg.isPresent()) { + String arg = validArg.get(); + if (arg.isEmpty()) { + err.println("Usage: valid "); + } else { + CelVerificationResult res = CelVerifierToolCore.checkValid(arg, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } else if (equivArg.isPresent()) { + String arg = equivArg.get(); + ImmutableList parts = splitEquivQuery(arg); + if (parts.size() != 2 || parts.get(0).isEmpty() || parts.get(1).isEmpty()) { + err.println("Equivalence query format: equiv <=> "); + } else { + String exprA = parts.get(0).trim(); + String exprB = parts.get(1).trim(); + CelVerificationResult res = + CelVerifierToolCore.verifyEquivalence(exprA, exprB, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } else { + // Default: treat as sat query + CelVerificationResult res = + CelVerifierToolCore.checkSatisfiable(line, sessionVars, options); + out.println(FormatUtils.formatTextResult(res)); + } + } catch (CelValidationException e) { + err.println( + FormatUtils.ANSI_RED + + "Compilation error:\n" + + e.getMessage() + + FormatUtils.ANSI_RESET); + } catch (CelPolicyValidationException e) { + err.println( + FormatUtils.ANSI_RED + + "Policy compilation error:\n" + + e.getMessage() + + FormatUtils.ANSI_RESET); + } catch (Exception e) { + err.println( + FormatUtils.ANSI_RED + + "Verification failed: " + + e.getMessage() + + FormatUtils.ANSI_RESET); + } + } + return 0; + } + + private static void handleVarCommand( + String arg, Map sessionVars, PrintStream out, PrintStream err) { + String[] parts = arg.split("\\s+", 2); + if (parts.length != 2) { + err.println("Usage: :var (e.g. :var role string, :var scores map)"); + return; + } + String name = parts[0].trim(); + String typeStr = parts[1].trim(); + try { + CelType type = VerificationOptions.parseCelType(typeStr); + sessionVars.put(name, type); + out.println("Variable declared: " + name + " : " + CelTypes.format(type)); + } catch (IllegalArgumentException e) { + err.println(e.getMessage()); + } + } + + private static void printVars( + Map sessionVars, + List unknowns, + int timeoutSeconds, + int unrollLimit, + PrintStream out) { + out.println("--- Session State ---"); + out.println("Timeout: " + timeoutSeconds + "s | Unroll limit: " + unrollLimit); + out.println("Unknowns: " + (unknowns.isEmpty() ? "none" : unknowns)); + out.println("Variables (" + sessionVars.size() + "):"); + for (Map.Entry entry : sessionVars.entrySet()) { + out.println(" " + entry.getKey() + " : " + CelTypes.format(entry.getValue())); + } + } + + private static void printHelp(String topic, PrintStream out) { + String t = topic.toLowerCase(Locale.US).replace(":", "").trim(); + switch (t) { + case "var": + case "vars": + out.println("Command: :var "); + out.println("Declares a variable in the REPL session with a specific type."); + out.println(); + out.println("Supported Types:"); + out.println(" - Primitive types: int, uint, string, bool, double, bytes"); + out.println(" - List types: list (e.g., list, list)"); + out.println(" - Map types: map (e.g., map, map)"); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :var role string"); + out.println(" cel-verifier> :var port int"); + out.println(" cel-verifier> :var scores map"); + out.println(" cel-verifier> :var tags list"); + break; + case "unknown": + out.println("Command: :unknown "); + out.println( + "Marks an identifier path as 'Unknown' during verification (partial evaluation)."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :unknown request.headers"); + out.println(" cel-verifier> :unknown request.auth.claims"); + break; + case "timeout": + out.println("Command: :timeout "); + out.println("Configures the Z3 solver soft timeout duration in seconds (default: 10s)."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :timeout 5"); + break; + case "unroll": + out.println("Command: :unroll "); + out.println("Configures the BMC loop unroll limit for comprehensions (default: 5)."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> :unroll 3"); + break; + case "sat": + out.println("Query: sat "); + out.println( + "Checks if a CEL expression can evaluate to true for any possible input assignments."); + out.println("If satisfiable, outputs concrete satisfying witness values."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> sat role == 'editor' && port > 1024"); + out.println(" cel-verifier> sat scores['alice'] > 90"); + break; + case "valid": + out.println("Query: valid "); + out.println( + "Proves whether a CEL expression evaluates to true for ALL possible input" + + " assignments."); + out.println("If invalid, outputs a counterexample showing inputs causing it to fail."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> valid x > 10 || x <= 10"); + break; + case "equiv": + out.println("Query: equiv <=> "); + out.println( + "Proves whether two CEL expressions are semantically identical for all inputs."); + out.println( + "If not equivalent, outputs a counterexample showing inputs where they diverge."); + out.println(); + out.println("Use '<=>' as the recommended separator between expressions."); + out.println(); + out.println("Examples:"); + out.println(" cel-verifier> equiv x > 10 <=> 10 < x"); + out.println(" cel-verifier> equiv (a && b) || (a && c) <=> a && (b || c)"); + out.println( + " cel-verifier> equiv string_int_map == {'a': 1, 'b': 2} ? string_int_map.all(k, k ==" + + " 'a') : true <=> string_int_map == {'a': 1, 'b': 2} ? string_int_map.all(k, k ==" + + " 'a') : true"); + break; + default: + out.println("REPL Commands:"); + out.println( + " :var Declare variable (e.g. :var role string, :var m" + + " map)"); + out.println(" :unknown Mark identifier as unknown"); + out.println(" :timeout Set solver timeout (default: 10s)"); + out.println(" :unroll Set comprehension unroll limit (default: 5)"); + out.println(" :vars List session variables & options"); + out.println(" :clear Reset session state"); + out.println( + " :help [command] Display help message or specific command details"); + out.println(" :quit Exit REPL"); + out.println(); + out.println("Verification Queries:"); + out.println(" sat Check satisfiability"); + out.println(" valid Check validity (always true)"); + out.println(" equiv <=> Prove logical equivalence"); + out.println(" Check satisfiability (default)"); + out.println(); + out.println( + "Type ':help ' (e.g. ':help var', ':help sat') for detailed usage and" + + " examples."); + break; + } + } + + private static ImmutableList splitEquivQuery(String rest) { + if (rest == null || rest.trim().isEmpty()) { + return ImmutableList.of(); + } + String input = rest.trim(); + if (input.contains(" <=> ")) { + return ImmutableList.copyOf(input.split(" <=> ", 2)); + } + if (input.contains("<=>")) { + return ImmutableList.copyOf(input.split("<=>", 2)); + } + return ImmutableList.of(); + } + + private static Optional extractCommandArg(String line, String prefix) { + if (Ascii.equalsIgnoreCase(line, prefix)) { + return Optional.of(""); + } + String prefixLower = Ascii.toLowerCase(prefix); + String lineLower = Ascii.toLowerCase(line); + if (lineLower.startsWith(prefixLower + " ") || lineLower.startsWith(prefixLower + "\t")) { + return Optional.of(line.substring(prefix.length()).trim()); + } + return Optional.empty(); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java new file mode 100644 index 000000000..963e966eb --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java @@ -0,0 +1,313 @@ +// 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.tools; + +import com.google.common.collect.ImmutableMap; +import dev.cel.common.CelValidationException; +import dev.cel.common.types.CelType; +import dev.cel.policy.CelPolicyValidationException; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import dev.cel.verifier.tools.VerificationOptions.OutputFormat; +import java.io.File; +import java.io.OutputStreamWriter; +import java.io.PrintWriter; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.time.Duration; +import java.util.ArrayList; +import java.util.List; +import java.util.Locale; +import java.util.concurrent.Callable; +import picocli.CommandLine; +import picocli.CommandLine.Command; +import picocli.CommandLine.IVersionProvider; +import picocli.CommandLine.Model.CommandSpec; +import picocli.CommandLine.Option; +import picocli.CommandLine.Spec; + +/** Main Picocli entrypoint for the CEL Formal Verification CLI. */ +@Command( + name = "cel-verifier", + mixinStandardHelpOptions = true, + versionProvider = CelVerifierTool.VersionProvider.class, + description = "CEL-Java Formal Verification CLI & REPL Tool", + subcommands = { + CelVerifierTool.CheckSatCommand.class, + CelVerifierTool.CheckValidCommand.class, + CelVerifierTool.VerifyEquivCommand.class, + CelVerifierTool.VerifyPolicyCommand.class, + CelVerifierTool.ReplCommand.class + }) +public final class CelVerifierTool implements Runnable { + + static final int EXIT_CODE_VERIFIED = 0; + static final int EXIT_CODE_VIOLATED = 1; + static final int EXIT_CODE_INCONCLUSIVE = 2; + static final int EXIT_CODE_ERROR = 3; + + static final class VersionProvider implements IVersionProvider { + @Override + public String[] getVersion() { + return new String[] {"cel-verifier " + CelVersion.VERSION}; + } + } + + @Spec private CommandSpec spec; + + @Override + public void run() { + spec.commandLine().usage(spec.commandLine().getOut()); + } + + /** Options shared across all verification commands. */ + abstract static class BaseVerificationCommand implements Callable { + + @Spec private CommandSpec spec; + + PrintWriter out() { + return spec != null + ? spec.commandLine().getOut() + : new PrintWriter(new OutputStreamWriter(System.out, StandardCharsets.UTF_8), true); + } + + PrintWriter err() { + return spec != null + ? spec.commandLine().getErr() + : new PrintWriter(new OutputStreamWriter(System.err, StandardCharsets.UTF_8), true); + } + + @Option( + names = {"--var", "-v"}, + description = + "Declared variable in 'name:type' format (e.g., --var role:string --var port:int)") + List variables = new ArrayList<>(); + + @Option( + names = {"--unknown", "-u"}, + description = + "Identifier to permit evaluating to Unknown (e.g., --unknown request.headers)") + List unknownIdentifiers = new ArrayList<>(); + + @Option( + names = {"--timeout"}, + description = "Solver timeout in seconds (default: 10)") + int timeoutSeconds = (int) VerificationOptions.DEFAULT_TIMEOUT.getSeconds(); + + @Option( + names = {"--unroll-limit"}, + description = "Comprehension unroll limit for BMC (default: 5)") + int comprehensionUnrollLimit = VerificationOptions.DEFAULT_COMPREHENSION_UNROLL_LIMIT; + + @Option( + names = {"--output_format", "-fmt"}, + description = "Output format: TEXT or JSON (default: TEXT)") + String outputFormatStr = VerificationOptions.DEFAULT_OUTPUT_FORMAT.name(); + + @FunctionalInterface + protected interface CommandAction { + int execute(VerificationOptions options, ImmutableMap vars) throws Exception; + } + + protected int executeCommand(CommandAction action) { + return executeCommand("Verification error", action); + } + + protected int executeCommand(String errorPrefix, CommandAction action) { + try { + VerificationOptions options = getOptions(); + ImmutableMap vars = VerificationOptions.parseVariables(variables); + return action.execute(options, vars); + } catch (CelValidationException e) { + err().println("Compilation error:\n" + e.getMessage()); + return EXIT_CODE_ERROR; + } catch (CelPolicyValidationException e) { + err().println("Policy compilation error:\n" + e.getMessage()); + return EXIT_CODE_ERROR; + } catch (Exception e) { + err().println(errorPrefix + ": " + e.getMessage()); + return EXIT_CODE_ERROR; + } + } + + protected VerificationOptions getOptions() { + OutputFormat format = OutputFormat.TEXT; + try { + format = OutputFormat.valueOf(outputFormatStr.toUpperCase(Locale.US)); + } catch (IllegalArgumentException e) { + err().println("Invalid output format '" + outputFormatStr + "'. Defaulting to TEXT."); + } + return VerificationOptions.builder() + .setTimeout(Duration.ofSeconds(timeoutSeconds)) + .setComprehensionUnrollLimit(comprehensionUnrollLimit) + .setUnknownIdentifiers(unknownIdentifiers) + .setOutputFormat(format) + .build(); + } + + protected int handleSingleResult(CelVerificationResult result, OutputFormat format) { + if (format == OutputFormat.JSON) { + out().println(FormatUtils.formatJsonResult(result)); + } else { + out().println(FormatUtils.formatTextResult(result)); + } + + if (result.status() == VerificationStatus.VERIFIED) { + return EXIT_CODE_VERIFIED; + } else if (result.status() == VerificationStatus.VIOLATED) { + return EXIT_CODE_VIOLATED; + } else { + return EXIT_CODE_INCONCLUSIVE; + } + } + } + + /** Base command for commands operating on a single CEL expression. */ + abstract static class SingleExpressionCommand extends BaseVerificationCommand { + @Option( + names = {"--expr", "-e"}, + required = true, + description = "CEL expression string to verify") + String expression = ""; + } + + @Command( + name = "check-sat", + description = "Verify satisfiability of a CEL expression & generate witness model") + static class CheckSatCommand extends SingleExpressionCommand { + + @Override + public Integer call() { + return executeCommand( + (options, vars) -> + handleSingleResult( + CelVerifierToolCore.checkSatisfiable(expression, vars, options), + options.getOutputFormat())); + } + } + + @Command( + name = "check-valid", + description = "Verify validity (isAlwaysTrue) of a CEL expression & generate counterexample") + static class CheckValidCommand extends SingleExpressionCommand { + + @Override + public Integer call() { + return executeCommand( + (options, vars) -> + handleSingleResult( + CelVerifierToolCore.checkValid(expression, vars, options), + options.getOutputFormat())); + } + } + + @Command( + name = "verify-equiv", + description = "Prove logical equivalence between two CEL expressions") + static class VerifyEquivCommand extends BaseVerificationCommand { + + @Option( + names = {"--expr1"}, + required = true, + description = "First CEL expression") + String expressionA = ""; + + @Option( + names = {"--expr2"}, + required = true, + description = "Second CEL expression") + String expressionB = ""; + + @Override + public Integer call() { + return executeCommand( + (options, vars) -> + handleSingleResult( + CelVerifierToolCore.verifyEquivalence(expressionA, expressionB, vars, options), + options.getOutputFormat())); + } + } + + @Command( + name = "verify-policy", + description = "Verify policy invariants defined in a YAML policy file") + static class VerifyPolicyCommand extends BaseVerificationCommand { + + @Option( + names = {"--file", "-f"}, + required = true, + description = "Path to policy YAML file") + String filePath = ""; + + @Override + public Integer call() { + return executeCommand( + "Policy verification error", + (options, vars) -> { + File file = new File(filePath); + if (!file.exists()) { + err().println("File not found: " + filePath); + return EXIT_CODE_ERROR; + } + String yamlContent = + new String(Files.readAllBytes(file.toPath()), StandardCharsets.UTF_8); + + ImmutableMap results = + CelVerifierToolCore.verifyPolicyInvariants(yamlContent, vars, options); + + if (options.getOutputFormat() == OutputFormat.JSON) { + out().println(FormatUtils.formatJsonPolicyResults(file.getName(), results)); + } else { + out().println(FormatUtils.formatTextPolicyResults(file.getName(), results)); + } + + return getPolicyExitCode(results); + }); + } + + private static int getPolicyExitCode(ImmutableMap results) { + boolean anyViolated = false; + boolean anyInconclusive = false; + for (CelVerificationResult res : results.values()) { + if (res.status() == VerificationStatus.VIOLATED) { + anyViolated = true; + } else if (res.status() == VerificationStatus.INCONCLUSIVE) { + anyInconclusive = true; + } + } + + if (anyViolated) { + return EXIT_CODE_VIOLATED; + } else if (anyInconclusive) { + return EXIT_CODE_INCONCLUSIVE; + } + return EXIT_CODE_VERIFIED; + } + } + + @Command(name = "repl", description = "Launch interactive CEL Formal Verification REPL shell") + static class ReplCommand implements Callable { + + @Override + public Integer call() { + return CelVerifierRepl.runInteractiveRepl(); + } + } + + public static void main(String[] args) { + int exitCode = new CommandLine(new CelVerifierTool()).execute(args); + System.exit(exitCode); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java new file mode 100644 index 000000000..51b7164e4 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java @@ -0,0 +1,165 @@ +// 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.tools; + +import com.google.common.collect.ImmutableMap; +import dev.cel.bundle.Cel; +import dev.cel.bundle.CelBuilder; +import dev.cel.bundle.CelFactory; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.CelOptions; +import dev.cel.common.types.CelType; +import dev.cel.compiler.CelCompiler; +import dev.cel.compiler.CelCompilerBuilder; +import dev.cel.compiler.CelCompilerFactory; +import dev.cel.extensions.CelExtensions; +import dev.cel.parser.CelStandardMacro; +import dev.cel.policy.CelPolicy; +import dev.cel.policy.CelPolicyCompiler; +import dev.cel.policy.CelPolicyCompilerFactory; +import dev.cel.policy.CelPolicyParser; +import dev.cel.policy.CelPolicyParserFactory; +import dev.cel.verifier.CelPolicyVerifier; +import dev.cel.verifier.CelPolicyVerifierFactory; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerifier; +import dev.cel.verifier.CelVerifierBuilder; +import dev.cel.verifier.CelVerifierFactory; +import java.util.Map; + +/** Core decoupled engine that executes formal verification operations. */ +final class CelVerifierToolCore { + + private CelVerifierToolCore() {} + + /** Checks if a single CEL expression is satisfiable. */ + static CelVerificationResult checkSatisfiable( + String expression, Map variables, VerificationOptions options) + throws Exception { + CelCompiler compiler = buildCompiler(variables); + CelAbstractSyntaxTree ast = compiler.compile(expression).getAst(); + CelVerifier verifier = buildVerifier(variables, options); + return verifier.isSatisfiable(ast); + } + + /** Checks if a single CEL expression is valid (always true). */ + static CelVerificationResult checkValid( + String expression, Map variables, VerificationOptions options) + throws Exception { + CelCompiler compiler = buildCompiler(variables); + CelAbstractSyntaxTree ast = compiler.compile(expression).getAst(); + CelVerifier verifier = buildVerifier(variables, options); + return verifier.isAlwaysTrue(ast); + } + + /** Proves logical equivalence between two CEL expressions. */ + static CelVerificationResult verifyEquivalence( + String expressionA, + String expressionB, + Map variables, + VerificationOptions options) + throws Exception { + CelCompiler compiler = buildCompiler(variables); + CelAbstractSyntaxTree astA = compiler.compile(expressionA).getAst(); + CelAbstractSyntaxTree astB = compiler.compile(expressionB).getAst(); + CelVerifier verifier = buildVerifier(variables, options); + return verifier.verifyEquivalence(astA, astB); + } + + /** Verifies custom invariants in a YAML policy content string. */ + static ImmutableMap verifyPolicyInvariants( + String yamlContent, Map variables, VerificationOptions options) + throws Exception { + CelPolicyParser parser = CelPolicyParserFactory.newYamlParserBuilder().build(); + CelPolicy policy = parser.parse(yamlContent); + + CelPolicyVerifier policyVerifier = buildPolicyVerifier(variables, options); + return policyVerifier.verifyInvariants(policy); + } + + /** Verifies equivalence between two YAML policy content strings. */ + static CelVerificationResult verifyPolicyEquivalence( + String yamlContentA, + String yamlContentB, + Map variables, + VerificationOptions options) + throws Exception { + CelPolicyParser parser = CelPolicyParserFactory.newYamlParserBuilder().build(); + CelPolicy policyA = parser.parse(yamlContentA); + CelPolicy policyB = parser.parse(yamlContentB); + + CelPolicyVerifier policyVerifier = buildPolicyVerifier(variables, options); + return policyVerifier.verifyEquivalence(policyA, policyB); + } + + static CelCompiler buildCompiler(Map variables) { + CelCompilerBuilder builder = + CelCompilerFactory.standardCelCompilerBuilder() + .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .addLibraries( + CelExtensions.bindings(), + CelExtensions.comprehensions(), + CelExtensions.encoders(CelOptions.DEFAULT), + CelExtensions.lists(), + CelExtensions.math(), + CelExtensions.optional(), + CelExtensions.protos(), + CelExtensions.regex(), + CelExtensions.sets(CelOptions.DEFAULT), + CelExtensions.strings()); + for (Map.Entry entry : variables.entrySet()) { + builder.addVar(entry.getKey(), entry.getValue()); + } + return builder.build(); + } + + static Cel buildCel(Map variables) { + CelBuilder celBuilder = + CelFactory.plannerCelBuilder() + .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .addCompilerLibraries( + CelExtensions.optional(), + CelExtensions.bindings(), + CelExtensions.encoders(CelOptions.DEFAULT), + CelExtensions.math(), + CelExtensions.strings()); + for (Map.Entry entry : variables.entrySet()) { + celBuilder.addVar(entry.getKey(), entry.getValue()); + } + return celBuilder.build(); + } + + static CelVerifier buildVerifier(Map variables, VerificationOptions options) { + CelVerifierBuilder builder = + CelVerifierFactory.newVerifier(buildCel(variables)) + .setTimeout(options.getTimeout()) + .setComprehensionUnrollLimit(options.getComprehensionUnrollLimit()); + + for (String unknown : options.getUnknownIdentifiers()) { + builder.addUnknownIdentifier(unknown); + } + return builder.build(); + } + + private static CelPolicyVerifier buildPolicyVerifier( + Map variables, VerificationOptions options) { + Cel celBundle = buildCel(variables); + CelPolicyCompiler policyCompiler = + CelPolicyCompilerFactory.newPolicyCompiler(celBundle).build(); + CelVerifier astVerifier = buildVerifier(variables, options); + + return CelPolicyVerifierFactory.newVerifier(policyCompiler, astVerifier).build(); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java b/verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java new file mode 100644 index 000000000..62d9889ad --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java @@ -0,0 +1,173 @@ +// 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.tools; + +import com.google.common.collect.ImmutableMap; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import java.util.Map; + +/** Utilities for formatting verification output (ANSI text & JSON). */ +final class FormatUtils { + + // ANSI Escape Codes for formatting text + static final String ANSI_RESET = "\u001B[0m"; + static final String ANSI_BOLD = "\u001B[1m"; + static final String ANSI_GREEN = "\u001B[32m"; + static final String ANSI_RED = "\u001B[31m"; + static final String ANSI_YELLOW = "\u001B[33m"; + static final String ANSI_CYAN = "\u001B[36m"; + + private FormatUtils() {} + + /** Formats a single CelVerificationResult for human-readable console display with ANSI color. */ + static String formatTextResult(CelVerificationResult result) { + StringBuilder sb = new StringBuilder(); + String statusColor = getStatusColor(result.status()); + sb.append(statusColor) + .append(ANSI_BOLD) + .append("[") + .append(result.status()) + .append("]") + .append(ANSI_RESET); + + if (!result.message().isEmpty()) { + sb.append(" ").append(result.message()); + } + + return sb.toString(); + } + + /** Formats policy invariant verification results for human-readable console display. */ + static String formatTextPolicyResults( + String policyName, ImmutableMap results) { + StringBuilder sb = new StringBuilder(); + sb.append(ANSI_BOLD) + .append("Policy Invariant Verification for '") + .append(policyName) + .append("':\n") + .append(ANSI_RESET); + + for (Map.Entry entry : results.entrySet()) { + String id = entry.getKey(); + CelVerificationResult result = entry.getValue(); + String symbol = result.status() == VerificationStatus.VERIFIED ? "✓" : "✗"; + String color = getStatusColor(result.status()); + + sb.append(" ") + .append(color) + .append(symbol) + .append(" Invariant '") + .append(id) + .append("': ") + .append(result.status()) + .append(ANSI_RESET); + + if (!result.message().isEmpty()) { + sb.append("\n ").append(result.message().replace("\n", "\n ")); + } + sb.append("\n"); + } + return sb.toString().trim(); + } + + /** Formats a single CelVerificationResult as structured JSON. */ + static String formatJsonResult(CelVerificationResult result) { + StringBuilder sb = new StringBuilder(); + sb.append("{\n"); + sb.append(" \"status\": \"").append(result.status()).append("\",\n"); + sb.append(" \"message\": \"").append(escapeJson(result.message())).append("\"\n"); + sb.append("}"); + return sb.toString(); + } + + /** Formats policy invariant verification results as structured JSON. */ + static String formatJsonPolicyResults( + String policyName, ImmutableMap results) { + StringBuilder sb = new StringBuilder(); + sb.append("{\n"); + sb.append(" \"policyName\": \"").append(escapeJson(policyName)).append("\",\n"); + sb.append(" \"invariants\": [\n"); + + int count = 0; + for (Map.Entry entry : results.entrySet()) { + count++; + String id = entry.getKey(); + CelVerificationResult res = entry.getValue(); + sb.append(" {\n"); + sb.append(" \"id\": \"").append(escapeJson(id)).append("\",\n"); + sb.append(" \"status\": \"").append(res.status()).append("\",\n"); + sb.append(" \"message\": \"").append(escapeJson(res.message())).append("\"\n"); + sb.append(" }").append(count < results.size() ? "," : "").append("\n"); + } + + sb.append(" ]\n"); + sb.append("}"); + return sb.toString(); + } + + private static String getStatusColor(VerificationStatus status) { + switch (status) { + case VERIFIED: + return ANSI_GREEN; + case VIOLATED: + return ANSI_RED; + case INCONCLUSIVE: + return ANSI_YELLOW; + } + return ANSI_RESET; + } + + static String escapeJson(String input) { + if (input == null) { + return ""; + } + StringBuilder sb = new StringBuilder(input.length() + 16); + for (int i = 0; i < input.length(); i++) { + char c = input.charAt(i); + switch (c) { + case '\\': + sb.append("\\\\"); + break; + case '"': + sb.append("\\\""); + break; + case '\b': + sb.append("\\b"); + break; + case '\f': + sb.append("\\f"); + break; + case '\n': + sb.append("\\n"); + break; + case '\r': + sb.append("\\r"); + break; + case '\t': + sb.append("\\t"); + break; + default: + if (c < 0x20) { + sb.append(String.format("\\u%04x", (int) c)); + } else { + sb.append(c); + } + break; + } + } + return sb.toString(); + } +} diff --git a/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java new file mode 100644 index 000000000..f2b3bf742 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java @@ -0,0 +1,223 @@ +// 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.tools; + +import com.google.common.base.Preconditions; +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import com.google.errorprone.annotations.CanIgnoreReturnValue; +import dev.cel.common.types.CelType; +import dev.cel.common.types.ListType; +import dev.cel.common.types.MapType; +import dev.cel.common.types.SimpleType; +import java.time.Duration; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Locale; +import java.util.Map; + +/** Configuration options for CEL verification CLI operations. */ +final class VerificationOptions { + + /** Output format for verification CLI results. */ + enum OutputFormat { + TEXT, + JSON + } + + static final Duration DEFAULT_TIMEOUT = Duration.ofSeconds(10); + static final int DEFAULT_COMPREHENSION_UNROLL_LIMIT = 5; + static final OutputFormat DEFAULT_OUTPUT_FORMAT = OutputFormat.TEXT; + + private final Duration timeout; + private final int comprehensionUnrollLimit; + private final ImmutableList unknownIdentifiers; + private final OutputFormat outputFormat; + + Duration getTimeout() { + return timeout; + } + + int getComprehensionUnrollLimit() { + return comprehensionUnrollLimit; + } + + ImmutableList getUnknownIdentifiers() { + return unknownIdentifiers; + } + + OutputFormat getOutputFormat() { + return outputFormat; + } + + static Builder builder() { + return new Builder(); + } + + /** A builder for {@link VerificationOptions}. */ + static final class Builder { + private Duration timeout = DEFAULT_TIMEOUT; + private int comprehensionUnrollLimit = DEFAULT_COMPREHENSION_UNROLL_LIMIT; + private ImmutableList unknownIdentifiers = ImmutableList.of(); + private OutputFormat outputFormat = DEFAULT_OUTPUT_FORMAT; + + @CanIgnoreReturnValue + Builder setTimeout(Duration timeout) { + this.timeout = Preconditions.checkNotNull(timeout); + return this; + } + + @CanIgnoreReturnValue + Builder setComprehensionUnrollLimit(int unrollLimit) { + Preconditions.checkArgument(unrollLimit >= 0, "unrollLimit must be non-negative"); + this.comprehensionUnrollLimit = unrollLimit; + return this; + } + + @CanIgnoreReturnValue + Builder setUnknownIdentifiers(List unknownIdentifiers) { + this.unknownIdentifiers = ImmutableList.copyOf(unknownIdentifiers); + return this; + } + + @CanIgnoreReturnValue + Builder setOutputFormat(OutputFormat outputFormat) { + this.outputFormat = Preconditions.checkNotNull(outputFormat); + return this; + } + + VerificationOptions build() { + return new VerificationOptions( + timeout, comprehensionUnrollLimit, unknownIdentifiers, outputFormat); + } + } + + private VerificationOptions( + Duration timeout, + int comprehensionUnrollLimit, + ImmutableList unknownIdentifiers, + OutputFormat outputFormat) { + this.timeout = timeout; + this.comprehensionUnrollLimit = comprehensionUnrollLimit; + this.unknownIdentifiers = unknownIdentifiers; + this.outputFormat = outputFormat; + } + + /** + * Helper utility to parse CLI variable definitions formatted as "name:type" (e.g. "x:int", + * "role:string", "is_admin:bool"). + */ + static ImmutableMap parseVariables(List varSpecs) { + if (varSpecs == null || varSpecs.isEmpty()) { + return ImmutableMap.of(); + } + Map vars = new HashMap<>(); + for (String varSpec : varSpecs) { + Preconditions.checkNotNull(varSpec, "Variable specification cannot be null."); + String[] parts = varSpec.split(":", 2); + if (parts.length != 2) { + throw new IllegalArgumentException( + "Invalid variable specification: '" + + varSpec + + "'. Expected format 'name:type' (e.g., 'x:int')."); + } + String name = parts[0].trim(); + if (name.isEmpty()) { + throw new IllegalArgumentException( + "Invalid variable specification: '" + varSpec + "'. Variable name cannot be empty."); + } + String typeStr = parts[1].trim().toLowerCase(Locale.US); + CelType type = parseCelType(typeStr); + vars.put(name, type); + } + return ImmutableMap.copyOf(vars); + } + + static CelType parseCelType(String typeStr) { + Preconditions.checkNotNull(typeStr, "Type string cannot be null."); + String str = typeStr.trim().toLowerCase(Locale.US); + + if (str.startsWith("list<") && str.endsWith(">")) { + String inner = str.substring(5, str.length() - 1).trim(); + CelType elemType = parseCelType(inner); + return ListType.create(elemType); + } + + if (str.startsWith("map<") && str.endsWith(">")) { + String inner = str.substring(4, str.length() - 1).trim(); + List parts = splitGenericArgs(inner); + if (parts.size() != 2) { + throw new IllegalArgumentException( + "Invalid map type format: '" + + typeStr + + "'. Expected format 'map' (e.g., 'map')."); + } + CelType keyType = parseCelType(parts.get(0)); + CelType valueType = parseCelType(parts.get(1)); + return MapType.create(keyType, valueType); + } + + switch (str) { + case "int": + return SimpleType.INT; + case "uint": + return SimpleType.UINT; + case "string": + return SimpleType.STRING; + case "bool": + case "boolean": + return SimpleType.BOOL; + case "double": + case "float": + return SimpleType.DOUBLE; + case "bytes": + return SimpleType.BYTES; + case "dyn": + return SimpleType.DYN; + default: + throw new IllegalArgumentException( + "Unsupported type for CLI variable declaration: '" + + typeStr + + "'. Supported types: int, uint, string, bool, double, bytes, dyn, list, map."); + } + } + + private static List splitGenericArgs(String inner) { + List result = new ArrayList<>(); + int depth = 0; + StringBuilder current = new StringBuilder(); + for (int i = 0; i < inner.length(); i++) { + char c = inner.charAt(i); + if (c == '<') { + depth++; + current.append(c); + } else if (c == '>') { + depth--; + current.append(c); + } else if (c == ',' && depth == 0) { + result.add(current.toString().trim()); + current.setLength(0); + } else { + current.append(c); + } + } + if (current.length() > 0) { + result.add(current.toString().trim()); + } + return result; + } +} diff --git a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel index 9e7f0ed15..89a01c610 100644 --- a/verifier/src/test/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/test/java/dev/cel/verifier/BUILD.bazel @@ -9,7 +9,7 @@ java_library( name = "tests", testonly = True, srcs = glob( - ["**/*.java"], + ["*.java"], ), compatible_with = [], data = [ @@ -20,9 +20,12 @@ java_library( "//common:cel_ast", "//common:compiler_common", "//common:container", + "//common:mutable_ast", "//common:operator", "//common:options", "//common/ast", + "//common/ast:mutable_expr", + "//common/navigation:mutable_navigation", "//common/types", "//common/types:message_type_provider", "//compiler:compiler_builder", @@ -47,6 +50,8 @@ java_library( "//:java_truth", "@maven//:tools_aqua_z3_turnkey", "//verifier", + "//verifier:canonicalization_optimizer", + "//verifier:numeric_bounds", "//verifier:policy_verifier", "//verifier:policy_verifier_factory", "//verifier:type_system", @@ -60,7 +65,7 @@ java_library( junit4_test_suites( name = "test_suites", - shard_count = 4, + shard_count = 8, sizes = [ "small", "medium", diff --git a/verifier/src/test/java/dev/cel/verifier/CanonicalizationOptimizerTest.java b/verifier/src/test/java/dev/cel/verifier/CanonicalizationOptimizerTest.java new file mode 100644 index 000000000..d526186e5 --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/CanonicalizationOptimizerTest.java @@ -0,0 +1,566 @@ +// 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 static org.junit.Assert.assertThrows; + +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import com.google.testing.junit.testparameterinjector.TestParameter; +import com.google.testing.junit.testparameterinjector.TestParameterInjector; +import dev.cel.bundle.Cel; +import dev.cel.bundle.CelFactory; +import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.CelContainer; +import dev.cel.common.CelMutableAst; +import dev.cel.common.CelOptions; +import dev.cel.common.ast.CelMutableExpr; +import dev.cel.common.ast.CelMutableExpr.CelMutableCall; +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.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.parser.CelStandardMacro; +import dev.cel.parser.CelUnparser; +import dev.cel.parser.CelUnparserFactory; +import dev.cel.verifier.CanonicalizationOptimizer.CanonicalizationOptions; +import org.junit.Test; +import org.junit.runner.RunWith; + +@RunWith(TestParameterInjector.class) +public class CanonicalizationOptimizerTest { + + private static final Cel CEL = + CelFactory.plannerCelBuilder() + .setContainer(CelContainer.ofName("cel.expr.conformance.proto3")) + .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .setOptions( + CelOptions.current() + .populateMacroCalls(true) + .enableHeterogeneousNumericComparisons(true) + .build()) + .addMessageTypes(TestAllTypes.getDescriptor()) + .addCompilerLibraries( + CelExtensions.comprehensions(), CelExtensions.bindings(), CelOptionalLibrary.INSTANCE) + .addRuntimeLibraries(CelExtensions.comprehensions(), CelOptionalLibrary.INSTANCE) + // Abstract DYN variables for alphabetical ordering and precedence tests + .addVar("dyn_a", SimpleType.DYN) + .addVar("dyn_b", SimpleType.DYN) + .addVar("dyn_c", SimpleType.DYN) + .addVar("dyn_d", SimpleType.DYN) + // Explicit Primitive typed variables + .addVar("bool_var", SimpleType.BOOL) + .addVar("bool_var2", SimpleType.BOOL) + .addVar("int_var", SimpleType.INT) + .addVar("int_var2", SimpleType.INT) + .addVar("uint_var", SimpleType.UINT) + .addVar("uint_var2", SimpleType.UINT) + .addVar("double_var", SimpleType.DOUBLE) + .addVar("double_var2", SimpleType.DOUBLE) + .addVar("string_var", SimpleType.STRING) + .addVar("string_var2", SimpleType.STRING) + .addVar("bytes_var", SimpleType.BYTES) + .addVar("bytes_var2", SimpleType.BYTES) + .addVar("duration_var", SimpleType.DURATION) + .addVar("timestamp_var", SimpleType.TIMESTAMP) + .addVar("null_var", SimpleType.NULL_TYPE) + // Collection variables + .addVar("int_list", ListType.create(SimpleType.INT)) + .addVar("string_list", ListType.create(SimpleType.STRING)) + .addVar("bool_list", ListType.create(SimpleType.BOOL)) + .addVar("nested_list", ListType.create(ListType.create(SimpleType.INT))) + .addVar("opt_list", ListType.create(OptionalType.create(SimpleType.INT))) + .addVar("string_int_map", MapType.create(SimpleType.STRING, SimpleType.INT)) + .addVar("int_string_map", MapType.create(SimpleType.INT, SimpleType.STRING)) + .addVar( + "nested_map", + MapType.create(SimpleType.STRING, MapType.create(SimpleType.STRING, SimpleType.INT))) + .addVar("list_map", ListType.create(MapType.create(SimpleType.STRING, SimpleType.INT))) + .addVar("int_list_map", MapType.create(SimpleType.INT, ListType.create(SimpleType.INT))) + // Struct / proto message variables + .addVar("msg", StructTypeReference.create(TestAllTypes.getDescriptor().getFullName())) + .addVar("msg2", StructTypeReference.create(TestAllTypes.getDescriptor().getFullName())) + .build(); + + private static final CelOptimizer OPTIMIZER = + CelOptimizerFactory.standardCelOptimizerBuilder(CEL) + .addAstOptimizers( + CanonicalizationOptimizer.newInstance( + CanonicalizationOptions.newBuilder().build())) + .build(); + + private static final CelUnparser UNPARSER = CelUnparserFactory.newUnparser(); + + private enum CanonicalizationTestCase { + // Commutative Logical Operators (&&, ||) across Simple Types + COMMUTATIVE_AND_BOOL( + "bool_var == true && bool_var2 == false", "bool_var == true && bool_var2 == false"), + COMMUTATIVE_AND_INT("int_var == 2 && int_var2 == 1", "int_var == 2 && int_var2 == 1"), + COMMUTATIVE_AND_UINT( + "uint_var == 20u && uint_var2 == 10u", "uint_var == 20u && uint_var2 == 10u"), + COMMUTATIVE_AND_DOUBLE( + "double_var == 3.14 && double_var2 == 1.41", "double_var == 3.14 && double_var2 == 1.41"), + COMMUTATIVE_AND_STRING( + "string_var == 'foo' && string_var2 == 'bar'", + "string_var == \"foo\" && string_var2 == \"bar\""), + COMMUTATIVE_AND_BYTES( + "bytes_var == b'foo' && bytes_var2 == b'bar'", + "bytes_var == b\"\\146\\157\\157\" && bytes_var2 == b\"\\142\\141\\162\""), + COMMUTATIVE_AND_NULL("null_var == null && dyn_a == null", "dyn_a == null && null_var == null"), + COMMUTATIVE_AND_MULTI_OPERAND( + "string_var == 'c' && string_var == 'a' && string_var == 'b'", + "string_var == \"a\" && string_var == \"b\" && string_var == \"c\""), + COMMUTATIVE_OR_MULTI_OPERAND( + "int_var == 30 || int_var == 10 || int_var == 20", + "int_var == 10 || int_var == 20 || int_var == 30"), + COMMUTATIVE_AND_DEDUPLICATION("int_var == 1 && int_var == 1", "int_var == 1"), + COMMUTATIVE_OR_DEDUPLICATION("string_var == 'a' || string_var == 'a'", "string_var == \"a\""), + COMMUTATIVE_AND_MIXED_TYPES( + "string_var == 'foo' && int_var == 1", "int_var == 1 && string_var == \"foo\""), + COMMUTATIVE_OR_MIXED_TYPES( + "bool_var == true || int_var == 1", "bool_var == true || int_var == 1"), + LIST_DIFFERENT_SIZES_EQUALITY("[1, 2] == [1]", "[1] == [1, 2]"), + ONE_ARG_CALL_WITH_LOGICAL_OPERANDS( + "type(bool_var == true && bool_var2 == false)", + "type(bool_var == true && bool_var2 == false)"), + COMMUTATIVE_AND_DURATION_TIMESTAMP( + "timestamp_var == timestamp('2026-01-01T00:00:00Z') && duration_var == duration('10s')", + "duration_var == duration(\"10s\") && timestamp_var ==" + + " timestamp(\"2026-01-01T00:00:00Z\")"), + COMMUTATIVE_AND_NESTED_LOGIC( + "(dyn_b || dyn_a) && (dyn_d || dyn_c)", "(dyn_a || dyn_b) && (dyn_c || dyn_d)"), + + // Symmetric Equality (==) and Inequality (!=) across Types + SYMMETRIC_EQUALS_BOOL("true == bool_var", "bool_var == true"), + SYMMETRIC_NOT_EQUALS_BOOL("false != bool_var", "bool_var != false"), + SYMMETRIC_EQUALS_INT("42 == int_var", "int_var == 42"), + SYMMETRIC_NOT_EQUALS_INT("0 != int_var", "int_var != 0"), + SYMMETRIC_EQUALS_UINT("100u == uint_var", "uint_var == 100u"), + SYMMETRIC_NOT_EQUALS_UINT("0u != uint_var", "uint_var != 0u"), + SYMMETRIC_EQUALS_DOUBLE("3.14159 == double_var", "double_var == 3.14159"), + SYMMETRIC_NOT_EQUALS_DOUBLE("0.0 != double_var", "double_var != 0.0"), + SYMMETRIC_EQUALS_STRING("'hello' == string_var", "string_var == \"hello\""), + SYMMETRIC_NOT_EQUALS_STRING("'' != string_var", "string_var != \"\""), + SYMMETRIC_EQUALS_BYTES("b'abc' == bytes_var", "bytes_var == b\"\\141\\142\\143\""), + SYMMETRIC_NOT_EQUALS_BYTES("b'' != bytes_var", "bytes_var != b\"\""), + SYMMETRIC_EQUALS_IDENT_ORDERING("dyn_c == dyn_a", "dyn_a == dyn_c"), + SYMMETRIC_EQUALS_CALL_VS_IDENT("size(int_list) == int_var", "int_var == size(int_list)"), + SYMMETRIC_EQUALS_SELECT_VS_IDENT("msg.single_int64 == dyn_a", "dyn_a == msg.single_int64"), + SYMMETRIC_EQUALS_GLOBAL_VS_MEMBER_CALL( + "int_list.size() == size(int_list)", "size(int_list) == int_list.size()"), + COMMUTATIVE_AND_GLOBAL_VS_MEMBER_CALL( + "int_list.size() == 1 && size(int_list) == 1", + "size(int_list) == 1 && int_list.size() == 1"), + + // De Morgan Transformations on Logical NOT (!) + DE_MORGAN_DOUBLE_NEGATION("!!bool_var", "bool_var"), + DE_MORGAN_QUADRUPLE_NEGATION("!!!!(int_var == 1)", "int_var == 1"), + DE_MORGAN_AND_TYPED( + "!(int_var == 1 && string_var == 'foo')", "int_var != 1 || string_var != \"foo\""), + DE_MORGAN_OR_TYPED( + "!(int_var == 1 || string_var == 'foo')", "int_var != 1 && string_var != \"foo\""), + DE_MORGAN_EQUALS_TYPED("!(int_var == 1)", "int_var != 1"), + DE_MORGAN_NOT_EQUALS_TYPED("!(int_var != 1)", "int_var == 1"), + DE_MORGAN_NESTED_AND_OR( + "!((dyn_a && dyn_b) || (dyn_c && dyn_d))", "(!dyn_a || !dyn_b) && (!dyn_c || !dyn_d)"), + DE_MORGAN_NESTED_OR_AND( + "!((dyn_a || dyn_b) && (dyn_c || dyn_d))", "!dyn_a && !dyn_b || !dyn_c && !dyn_d"), + DE_MORGAN_MIXED_TYPES( + "!(bool_var == true && double_var == 1.0)", "bool_var != true || double_var != 1.0"), + DE_MORGAN_ALL_NEGATED_PREDICATE("!int_list.all(e, !(e == 1))", "e == 1"), + DE_MORGAN_EXISTS_NEGATED_PREDICATE("!int_list.exists(e, !(e == 1))", "e == 1"), + DE_MORGAN_ALL_NEGATED_VAR_PREDICATE("!int_list.all(e, !bool_var)", "int_list.exists(e, bool_var)"), + DE_MORGAN_EXISTS_NEGATED_VAR_PREDICATE("!int_list.exists(e, !bool_var)", "int_list.all(e, bool_var)"), + DE_MORGAN_RELATIONAL_UNCHANGED("!(int_var > 5)", "!(int_var > 5)"), + DE_MORGAN_EXISTS_TYPED("!int_list.exists(e, e == 1)", "e != 1"), + DE_MORGAN_ALL_TYPED("!int_list.all(e, e == 1)", "e != 1"), + DE_MORGAN_EXISTS_COMPLEX_PREDICATE( + "!int_list.exists(e, !(e == 1 && e == 2))", "e == 1 && e == 2"), + DE_MORGAN_ALL_COMPLEX_PREDICATE("!int_list.all(e, !(e == 1 || e == 2))", "e == 1 || e == 2"), + DE_MORGAN_BOOL_VARIABLES("!(bool_var && bool_var2)", "!bool_var || !bool_var2"), + + // Extension Coverage - Optionals & Optional Indexing/Fields + OPTIONAL_OF_EQUALITY_SYMMETRY( + "optional.of(dyn_b) == optional.of(dyn_a)", "optional.of(dyn_a) == optional.of(dyn_b)"), + OPTIONAL_NONE_EQUALITY_SYMMETRY( + "optional.of(dyn_a) == optional.none()", "optional.none() == optional.of(dyn_a)"), + OPTIONAL_OF_NON_ZERO_VALUE_SYMMETRY( + "optional.ofNonZeroValue(dyn_b) == optional.ofNonZeroValue(dyn_a)", + "optional.ofNonZeroValue(dyn_a) == optional.ofNonZeroValue(dyn_b)"), + OPTIONAL_FIELD_SELECT_EQUALITY( + "msg.?single_int64 == optional.of(1)", "msg.?single_int64 == optional.of(1)"), + OPTIONAL_FIELD_SELECT_INEQUALITY( + "msg.?single_string != optional.none()", "msg.?single_string != optional.none()"), + OPTIONAL_FIELD_SELECT_OR_VALUE_EQUALITY( + "msg.?single_int64.orValue(0) == int_var", "int_var == msg.?single_int64.orValue(0)"), + OPTIONAL_LIST_ELEMENT_EQUALITY( + "[?optional.of(1)] == [?optional.of(int_var)]", + "[?optional.of(int_var)] == [?optional.of(1)]"), + OPTIONAL_MAP_ENTRY_EQUALITY( + "{?'key': optional.of(1)} == {?'key': optional.of(int_var)}", + "{?\"key\": optional.of(int_var)} == {?\"key\": optional.of(1)}"), + DE_MORGAN_OPTIONAL_EQUALITY( + "!(optional.of(dyn_a) == optional.of(dyn_b))", "optional.of(dyn_a) != optional.of(dyn_b)"), + DE_MORGAN_OPTIONAL_INEQUALITY( + "!(optional.of(dyn_a) != optional.none())", "optional.none() == optional.of(dyn_a)"), + COMMUTATIVE_AND_OPTIONAL_HAS_VALUE( + "optional.of(dyn_b).hasValue() && optional.of(dyn_a).hasValue()", + "optional.of(dyn_a).hasValue() && optional.of(dyn_b).hasValue()"), + COMMUTATIVE_OR_OPTIONAL_HAS_VALUE( + "optional.of(dyn_b).hasValue() || optional.of(dyn_a).hasValue()", + "optional.of(dyn_a).hasValue() || optional.of(dyn_b).hasValue()"), + COMMUTATIVE_AND_OPTIONAL_FIELD_SELECT( + "msg.?single_string.hasValue() && msg.?single_int64.hasValue()", + "msg.?single_int64.hasValue() && msg.?single_string.hasValue()"), + COMMUTATIVE_OR_OPTIONAL_FIELD_SELECT( + "msg.?single_string.hasValue() || msg.?single_int64.hasValue()", + "msg.?single_int64.hasValue() || msg.?single_string.hasValue()"), + DE_MORGAN_OPTIONAL_HAS_VALUE_AND( + "!(optional.of(dyn_a).hasValue() && optional.of(dyn_b).hasValue())", + "!optional.of(dyn_a).hasValue() || !optional.of(dyn_b).hasValue()"), + DE_MORGAN_OPTIONAL_HAS_VALUE_OR( + "!(optional.of(dyn_a).hasValue() || optional.of(dyn_b).hasValue())", + "!optional.of(dyn_a).hasValue() && !optional.of(dyn_b).hasValue()"), + OPTIONAL_IN_EXISTS_COMPREHENSION( + "!opt_list.exists(x, !(x.hasValue() && x.value() == 1))", "x.value() == 1 && x.hasValue()"), + OPTIONAL_IN_ALL_COMPREHENSION( + "!opt_list.all(x, !(x.hasValue() || x.value() == 1))", "x.value() == 1 || x.hasValue()"), + OPTIONAL_FIELD_CHAINING_EQUALITY( + "msg.?single_nested_message.?bb == optional.of(42)", + "msg.?single_nested_message.?bb == optional.of(42)"), + OPTIONAL_MAP_INDEXING_EQUALITY( + "string_int_map.?foo == optional.of(1)", "string_int_map.?foo == optional.of(1)"), + + // Extension Coverage - Two-Variable Comprehensions + DE_MORGAN_2VAR_EXISTS_MAP( + "!string_int_map.exists(k, v, k == 'foo' && v == 1)", "k != \"foo\" || v != 1"), + DE_MORGAN_2VAR_ALL_MAP( + "!string_int_map.all(k, v, !(k == 'foo' || v == 1))", "k == \"foo\" || v == 1"), + DE_MORGAN_2VAR_EXISTS_NEGATED_PREDICATE( + "!string_int_map.exists(k, v, !(v > 0 && k == 'foo'))", "k == \"foo\" && v > 0"), + DE_MORGAN_2VAR_ALL_NEGATED_PREDICATE( + "!string_int_map.all(k, v, !(v > 0 || k == 'foo'))", "k == \"foo\" || v > 0"), + TWO_VAR_EXISTS_COMMUTATIVE_AND( + "string_int_map.exists(k, v, v == 1 && k == 'foo')", + "string_int_map.exists(k, v, k == \"foo\" && v == 1)"), + TWO_VAR_ALL_COMMUTATIVE_OR( + "string_int_map.all(k, v, v == 1 || k == 'foo')", + "string_int_map.all(k, v, k == \"foo\" || v == 1)"), + TWO_VAR_EXISTS_SYMMETRIC_EQUALITY( + "string_int_map.exists(k, v, v == 1)", "string_int_map.exists(k, v, v == 1)"), + TWO_VAR_ALL_SYMMETRIC_INEQUALITY( + "string_int_map.all(k, v, v != 0)", "string_int_map.all(k, v, v != 0)"), + TWO_VAR_EXISTS_INT_STRING_MAP( + "int_string_map.exists(k, v, v == 'bar' && k == 1)", + "int_string_map.exists(k, v, k == 1 && v == \"bar\")"), + TWO_VAR_ALL_INT_STRING_MAP( + "!int_string_map.all(k, v, k == 1 || v == 'bar')", "k != 1 && v != \"bar\""), + TWO_VAR_EXISTS_LIST_INDEX_VALUE( + "!int_list.exists(i, v, i == 0 && v == 100)", "i != 0 || v != 100"), + TWO_VAR_ALL_LIST_INDEX_VALUE( + "!int_list.all(i, v, !(i == 0 || v == 100))", "i == 0 || v == 100"), + TWO_VAR_EXISTS_LIST_COMMUTATIVE_AND( + "int_list.exists(i, v, v == 100 && i == 0)", "int_list.exists(i, v, i == 0 && v == 100)"), + TWO_VAR_ALL_LIST_COMMUTATIVE_OR( + "int_list.all(i, v, v == 100 || i == 0)", "int_list.all(i, v, i == 0 || v == 100)"), + TWO_VAR_NESTED_COMPREHENSIONS( + "string_int_map.exists(k, v, k == 'foo' && int_list.all(i, e, e == v && i == 0))", + "string_int_map.exists(k, v, k == \"foo\" && int_list.all(i, e, e == v && i == 0))"), + DE_MORGAN_2VAR_NESTED_COMPREHENSIONS( + "string_int_map.exists(k, v, k == 'foo' && !int_list.exists(i, e, e == v))", + "string_int_map.exists(k, v, k == \"foo\" && e != v)"), + TWO_VAR_COMPREHENSION_WITH_OPTIONALS( + "!string_int_map.exists(k, v, optional.of(v).hasValue() && k == 'foo')", + "!optional.of(v).hasValue() || k != \"foo\""), + TWO_VAR_COMPREHENSION_STRUCT_FIELDS( + "!string_int_map.exists(k, v, !(k == msg.single_string && v == msg.single_int64))", + "k == msg.single_string && v == msg.single_int64"), + TWO_VAR_COMPREHENSION_DEDUPLICATION( + "string_int_map.exists(k, v, k == 'foo' && k == 'foo')", + "string_int_map.exists(k, v, k == \"foo\")"), + TWO_VAR_COMPREHENSION_DE_MORGAN_INEQUALITY( + "!string_int_map.exists(k, v, !(k != 'foo' && v != 1))", "k != \"foo\" && v != 1"), + + // Extension Coverage - cel.bind Macro + CEL_BIND_COMMUTATIVE_AND( + "cel.bind(x, int_var + 10, 1 == x && 2 == int_var2)", + "cel.bind(x, int_var + 10, int_var2 == 2 && x == 1)"), + CEL_BIND_COMMUTATIVE_OR( + "cel.bind(x, int_var + 10, 1 == x || 2 == int_var2)", + "cel.bind(x, int_var + 10, int_var2 == 2 || x == 1)"), + CEL_BIND_SYMMETRIC_EQUALITY( + "cel.bind(x, int_var + 10, 20 == x)", "cel.bind(x, int_var + 10, x == 20)"), + CEL_BIND_NESTED( + "cel.bind(x, int_var + 10, cel.bind(y, int_var2 + 20, 2 == y && 1 == x))", + "cel.bind(x, int_var + 10, cel.bind(y, int_var2 + 20, x == 1 && y == 2))"), + CEL_BIND_DE_MORGAN( + "cel.bind(x, int_var == 1, !(2 == int_var2 && x == true))", + "cel.bind(x, int_var == 1, int_var2 != 2 || x != true)"), + + // Nested Lists, Maps, and Structs + NESTED_LIST_EQUALITY_SYMMETRY( + "[[2, 1], [4, 3]] == [[1, 2], [3, 4]]", "[[1, 2], [3, 4]] == [[2, 1], [4, 3]]"), + NESTED_LIST_INEQUALITY_SYMMETRY("[[2, 1]] != [[1, 2]]", "[[1, 2]] != [[2, 1]]"), + LIST_ELEMENT_ORDERING_EQUALITY("int_list == [3, 2, 1]", "int_list == [3, 2, 1]"), + MAP_EQUALITY_ORDERING( + "string_int_map == {'b': 2, 'a': 1}", "string_int_map == {\"b\": 2, \"a\": 1}"), + MAP_DIFFERENT_SIZES_EQUALITY( + "{'b': 2, 'a': 1} == {'a': 1}", "{\"a\": 1} == {\"b\": 2, \"a\": 1}"), + COMMUTATIVE_AND_MAP_DIFFERENT_SIZES( + "string_int_map == {'a': 1, 'b': 2} && string_int_map == {'a': 1}", + "string_int_map == {\"a\": 1} && string_int_map == {\"a\": 1, \"b\": 2}"), + NESTED_MAP_EQUALITY( + "nested_map == {'b': {'d': 4, 'c': 3}, 'a': {'y': 2, 'x': 1}}", + "nested_map == {\"b\": {\"d\": 4, \"c\": 3}, \"a\": {\"y\": 2, \"x\": 1}}"), + LIST_OF_MAPS_EQUALITY( + "list_map == [{'y': 2, 'x': 1}, {'d': 4, 'c': 3}]", + "list_map == [{\"y\": 2, \"x\": 1}, {\"d\": 4, \"c\": 3}]"), + MAP_OF_LISTS_EQUALITY( + "int_list_map == {1: [2, 1], 2: [4, 3]}", "int_list_map == {1: [2, 1], 2: [4, 3]}"), + STRUCT_EQUALITY_ORDERING( + "msg == TestAllTypes{single_int64: 10, single_string: 'foo'}", + "msg == cel.expr.conformance.proto3.TestAllTypes{single_int64: 10, single_string:" + + " \"foo\"}"), + NESTED_STRUCT_EQUALITY( + "msg == TestAllTypes{single_nested_message: TestAllTypes.NestedMessage{bb: 42}}", + "msg == cel.expr.conformance.proto3.TestAllTypes{single_nested_message:" + + " cel.expr.conformance.proto3.TestAllTypes.NestedMessage{bb: 42}}"), + STRUCT_INEQUALITY( + "msg != TestAllTypes{single_int64: 0}", + "msg != cel.expr.conformance.proto3.TestAllTypes{single_int64: 0}"), + STRUCT_DIFFERENT_ENTRY_COUNTS_ORDERING( + "TestAllTypes{single_int64: 10, single_string: 'foo'} == TestAllTypes{single_int64: 10}", + "cel.expr.conformance.proto3.TestAllTypes{single_int64: 10} ==" + + " cel.expr.conformance.proto3.TestAllTypes{single_int64: 10, single_string: \"foo\"}"), + STRUCT_DIFFERENT_FIELD_VALUES_ORDERING( + "TestAllTypes{single_int64: 20} == TestAllTypes{single_int64: 10}", + "cel.expr.conformance.proto3.TestAllTypes{single_int64: 10} ==" + + " cel.expr.conformance.proto3.TestAllTypes{single_int64: 20}"), + DE_MORGAN_STRUCT_EQUALITY( + "!(msg == TestAllTypes{single_int64: 10})", + "msg != cel.expr.conformance.proto3.TestAllTypes{single_int64: 10}"), + DE_MORGAN_STRUCT_INEQUALITY( + "!(msg != TestAllTypes{single_int64: 10})", + "msg == cel.expr.conformance.proto3.TestAllTypes{single_int64: 10}"), + COMMUTATIVE_AND_STRUCT_FIELDS( + "msg.single_string == 'foo' && msg.single_int64 == 10", + "msg.single_int64 == 10 && msg.single_string == \"foo\""), + COMMUTATIVE_OR_STRUCT_FIELDS( + "msg.single_int64 == 20 || msg.single_int64 == 10", + "msg.single_int64 == 10 || msg.single_int64 == 20"), + DE_MORGAN_STRUCT_FIELDS_AND( + "!(msg.single_int64 == 10 && msg.single_string == 'foo')", + "msg.single_int64 != 10 || msg.single_string != \"foo\""), + DE_MORGAN_STRUCT_FIELDS_OR( + "!(msg.single_int64 == 10 || msg.single_int64 == 20)", + "msg.single_int64 != 10 && msg.single_int64 != 20"), + STRUCT_SELECT_ORDERING("msg.single_int64 == int_var", "int_var == msg.single_int64"), + NESTED_STRUCT_SELECT_ORDERING( + "msg.single_nested_message.bb == int_var", "int_var == msg.single_nested_message.bb"), + MAP_LOOKUP_IN_LOGICAL_EXPR( + "string_int_map['foo'] == 1 && string_int_map['bar'] == 2", + "string_int_map[\"bar\"] == 2 && string_int_map[\"foo\"] == 1"), + LIST_INDEX_IN_LOGICAL_EXPR( + "int_list[1] == 20 && int_list[0] == 10", "int_list[0] == 10 && int_list[1] == 20"), + COMPREHENSIONS_IN_LIST_LITERALS( + "[int_list.exists(e, e == 2), int_list.exists(e, e == 1)] == [true, false]", + "[int_list.exists(e, e == 2), int_list.exists(e, e == 1)] == [true, false]"), + COMPREHENSIONS_IN_MAP_LITERALS( + "{'b': int_list.all(e, e > 0), 'a': int_list.exists(e, e == 1)} == {'a': true, 'b': false}", + "{\"a\": true, \"b\": false} == {\"b\": int_list.all(e, e > 0), \"a\": int_list.exists(e, e" + + " == 1)}"), + COMPREHENSIONS_IN_STRUCT_FIELDS( + "TestAllTypes{single_int64: int_list[0]} == msg", + "msg == cel.expr.conformance.proto3.TestAllTypes{single_int64: int_list[0]}"), + NESTED_COMPREHENSIONS_IN_STRUCT_FIELDS( + "!int_list.exists(x, TestAllTypes{single_int64: x} == msg)", + "msg != cel.expr.conformance.proto3.TestAllTypes{single_int64: x}"), + DE_MORGAN_COLLECTION_LITERAL_EQUALITY("!([2, 1] == [1, 2])", "[1, 2] != [2, 1]"), + + // Cross-Type & Heterogeneous Comparisons + HETEROGENEOUS_INT_UINT_AND("int_var == 1 && uint_var == 1u", "int_var == 1 && uint_var == 1u"), + HETEROGENEOUS_INT_DOUBLE_OR( + "int_var == 1 || double_var == 1.0", "double_var == 1.0 || int_var == 1"), + HETEROGENEOUS_UINT_DOUBLE_EQUALITY( + "uint_var == 10u && double_var == 10.0", "double_var == 10.0 && uint_var == 10u"), + CROSS_TYPE_DURATION_TIMESTAMP_AND( + "timestamp_var == timestamp('2026-01-01T00:00:00Z') && duration_var == duration('10s')", + "duration_var == duration(\"10s\") && timestamp_var ==" + + " timestamp(\"2026-01-01T00:00:00Z\")"), + CROSS_TYPE_STRING_BYTES_OR( + "string_var == 'foo' || bytes_var == b'foo'", + "bytes_var == b\"\\146\\157\\157\" || string_var == \"foo\""), + NULL_VS_PRIMITIVE_EQUALITY("dyn_a == null", "dyn_a == null"), + NULL_VS_MESSAGE_EQUALITY("msg == null", "msg == null"), + NULL_VS_OPTIONAL_EQUALITY("optional.of(int_var) == null", "optional.of(int_var) == null"), + CROSS_TYPE_COMMUTATIVE_CHAIN( + "string_var == 'a' && double_var == 1.0 && int_var == 1 && bool_var == true", + "bool_var == true && double_var == 1.0 && int_var == 1 && string_var == \"a\""), + DE_MORGAN_CROSS_TYPE_CHAIN( + "!(string_var == 'a' && double_var == 1.0 && int_var == 1)", + "double_var != 1.0 || int_var != 1 || string_var != \"a\""), + HETEROGENEOUS_NUMERIC_DE_MORGAN( + "!(int_var != 1 || uint_var != 1u || double_var != 1.0)", + "double_var == 1.0 && int_var == 1 && uint_var == 1u"), + CROSS_TYPE_IN_2VAR_COMPREHENSION( + "!string_int_map.exists(k, v, !(int_var == 1 && double_var == 1.0))", + "double_var == 1.0 && int_var == 1"), + CROSS_TYPE_IN_LIST_COMPREHENSION( + "!int_list.exists(e, !(uint_var == 1u || double_var == 1.0))", + "double_var == 1.0 || uint_var == 1u"), + MIXED_SELECT_AND_CALLS_ACROSS_TYPES( + "msg.single_int64 == size(int_list) && msg.single_string == string(int_var)", + "msg.single_int64 == size(int_list) && msg.single_string == string(int_var)"), + DE_MORGAN_MIXED_SELECT_AND_CALLS( + "!(msg.single_int64 == size(int_list) && msg.single_string == 'foo')", + "msg.single_int64 != size(int_list) || msg.single_string != \"foo\""), + + // Edge Cases, Invariants, Non-Canonicalizable Expressions, and Precedence + RELATIONAL_OPERATORS_UNCHANGED("int_var < 10 && int_var > 5", "int_var < 10 && int_var > 5"), + DE_MORGAN_RELATIONAL_OPERATORS("!(int_var < 10)", "!(int_var < 10)"), + TERNARY_OPERATOR_UNCHANGED_COND( + "bool_var ? int_var == 1 : int_var == 2", "bool_var ? (int_var == 1) : (int_var == 2)"), + DE_MORGAN_TERNARY_OPERATOR( + "!(bool_var ? int_var == 1 : int_var == 2)", + "!(bool_var ? (int_var == 1) : (int_var == 2))"), + IN_OPERATOR_WITH_COMMUTATIVE_AND( + "int_var in int_list && bool_var == true", "int_var in int_list && bool_var == true"), + DE_MORGAN_IN_OPERATOR("!(int_var in int_list)", "!(int_var in int_list)"), + COMPREHENSION_ACCU_VAR_NOT_REORDERED( + "int_list.exists(e, e == 1 && e == 2)", "int_list.exists(e, e == 1 && e == 2)"), + COMPLEX_NESTED_DE_MORGAN_PRECEDENCE( + "!(dyn_a && dyn_b || dyn_c && dyn_d)", "(!dyn_a || !dyn_b) && (!dyn_c || !dyn_d)"), + COMPLEX_NESTED_DE_MORGAN_OR_AND( + "!((dyn_a || dyn_b) && (dyn_c || dyn_d))", "!dyn_a && !dyn_b || !dyn_c && !dyn_d"), + TRIPLE_AND_DEDUPLICATION("int_var == 1 && int_var == 1 && int_var == 1", "int_var == 1"), + TRIPLE_OR_DEDUPLICATION( + "string_var == 'x' || string_var == 'x' || string_var == 'x'", "string_var == \"x\""), + EMPTY_STRING_ZERO_CONSTANT_COMPARISONS( + "string_var == '' && int_var == 0 && bool_var == false", + "bool_var == false && int_var == 0 && string_var == \"\""), + IDENT_COMPARISON_SYMMETRY( + "dyn_b == dyn_a && dyn_d == dyn_c", "dyn_a == dyn_b && dyn_c == dyn_d"), + IDENT_INEQUALITY_SYMMETRY( + "dyn_b != dyn_a || dyn_d != dyn_c", "dyn_a != dyn_b || dyn_c != dyn_d"), + IDENT_SAME_NAME_DIFFERENT_OPERATORS( + "dyn_a != dyn_b && dyn_a == dyn_b", "dyn_a != dyn_b && dyn_a == dyn_b"); + + private final String input; + private final String expected; + + CanonicalizationTestCase(String input, String expected) { + this.input = input; + this.expected = expected; + } + } + + @Test + public void optimize_success(@TestParameter CanonicalizationTestCase testCase) throws Exception { + CelAbstractSyntaxTree ast = CEL.compile(testCase.input).getAst(); + CelAbstractSyntaxTree optimizedAst = OPTIMIZER.optimize(ast); + + String unparsed = UNPARSER.unparse(optimizedAst); + assertThat(unparsed).isEqualTo(testCase.expected); + } + + @Test + public void optimize_maxIterationLimitReached_throwsException() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("dyn_b == dyn_a && dyn_d == dyn_c").getAst(); + CanonicalizationOptimizer optimizer = + CanonicalizationOptimizer.newInstance( + CanonicalizationOptions.newBuilder().maxIterationLimit(1).build()); + + IllegalStateException e = + assertThrows(IllegalStateException.class, () -> optimizer.optimize(ast, CEL)); + assertThat(e).hasMessageThat().contains("Max iteration count reached."); + } + + @Test + public void optimize_deMorganAll_evaluatesCorrectly() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("!int_list.all(e, e == 1)").getAst(); + CelAbstractSyntaxTree optimizedAst = OPTIMIZER.optimize(ast); + + boolean result = + (boolean) + CEL.createProgram(optimizedAst) + .eval(ImmutableMap.of("int_list", ImmutableList.of(1, 2))); + assertThat(result).isTrue(); + } + + @Test + public void optimize_deMorganExists_evaluatesCorrectly() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("!int_list.exists(e, e == 1)").getAst(); + CelAbstractSyntaxTree optimizedAst = OPTIMIZER.optimize(ast); + + boolean result = + (boolean) + CEL.createProgram(optimizedAst) + .eval(ImmutableMap.of("int_list", ImmutableList.of(1, 2))); + assertThat(result).isFalse(); + } + + @Test + public void optimize_deMorganAll_negatedPredicate_evaluatesCorrectly() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("!int_list.all(e, !(e == 1))").getAst(); + CelAbstractSyntaxTree optimizedAst = OPTIMIZER.optimize(ast); + + boolean result = + (boolean) + CEL.createProgram(optimizedAst) + .eval(ImmutableMap.of("int_list", ImmutableList.of(1, 2))); + assertThat(result).isTrue(); + } + + @Test + public void optimize_deMorganExists_negatedPredicate_evaluatesCorrectly() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("!int_list.exists(e, !(e == 1))").getAst(); + CelAbstractSyntaxTree optimizedAst = OPTIMIZER.optimize(ast); + + boolean result = + (boolean) + CEL.createProgram(optimizedAst) + .eval(ImmutableMap.of("int_list", ImmutableList.of(1, 2))); + assertThat(result).isFalse(); + } + + @Test + public void optimize_customMacroWithExistsStructure_notCanonicalized() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("!int_list.exists(e, e == 1)").getAst(); + CelMutableAst mutableAst = CelMutableAst.fromCelAst(ast); + long macroKey = mutableAst.source().getMacroCalls().keySet().iterator().next(); + CelMutableExpr existingMacro = mutableAst.source().getMacroCalls().get(macroKey); + CelMutableCall customCall = + CelMutableCall.create( + existingMacro.call().target().get(), + "my_custom_exists", + existingMacro.call().args()); + mutableAst + .source() + .addMacroCalls(macroKey, CelMutableExpr.ofCall(existingMacro.id(), customCall)); + + CelAbstractSyntaxTree optimizedAst = + CanonicalizationOptimizer.newInstance(CanonicalizationOptions.newBuilder().build()) + .optimize(mutableAst.toParsedAst(), CEL) + .optimizedAst(); + assertThat(UNPARSER.unparse(optimizedAst)).isEqualTo("!int_list.my_custom_exists(e, e == 1)"); + } +} diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 1a41ef743..d7724ac91 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -131,7 +131,7 @@ public final class CelVerifierZ3ImplTest { .build(); private static final CelVerifier VERIFIER = - CelVerifierFactory.newVerifier().setTypeProvider(TYPE_PROVIDER).build(); + CelVerifierFactory.newVerifier(CEL).setTypeProvider(TYPE_PROVIDER).build(); @Before public void setUp() { @@ -139,30 +139,59 @@ public void setUp() { } private enum IsSatisfiableTestCase { - SATISFIABLE("x > 5"), - DYNAMIC_ARITHMETIC("request == 1 && request + 2 == 3"), - DYNAMIC_ARITHMETIC_UNARY("request == 1 && -request == -1"), - GREATER_DOUBLE("d > 1.5"), - LESS_EQUALS_UINT64("u <= 5u"), - LESS_EQUALS_DOUBLE("d <= 5.5"), - LESS_EQUALS_STRING("role <= 'admin'"), - LESS_EQUALS_BYTES("by <= b'bytes'"), - GREATER_STRING("role > 'admin'"), - GREATER_BYTES("by > b'bytes'"), - DYNAMIC_LIST_COMPREHENSION_EXISTS("int_list.exists(x, x > 5)"), - DYNAMIC_MAP_COMPREHENSION_EXISTS("string_int_map.exists(k, k == 'test')"), - NULL_SATISFIABLE("unknown_var == null"), - DYNAMIC_VAR_NUMERIC_EQUALITY("dyn_var == 1 && dyn_var == 1.0"), - DYNAMIC_VAR_NOT_IN_LIST("dyn_var == 1.5 && !(dyn_var in dyn_list) && size(dyn_list) > 5"), - CROSS_NUMERIC_EQUALITY_INT_DYN_EXACT("1 == request"), - MACRO_LIMIT("dyn_list.all(x, x == 1)"), - STRUCT_FIELD_MISSING_APPROXIMATE_SATISFIABLE("dyn_var.unknown_field"), - NULLABLE_INT_SATISFIABLE("nullable_int == 123"); + SATISFIABLE("x > 5", "x = (?:[6-9]|[1-9]\\d+)"), + DYNAMIC_ARITHMETIC("request == 1 && request + 2 == 3", "request = 1"), + DYNAMIC_ARITHMETIC_UNARY("request == 1 && -request == -1", "request = 1"), + GREATER_DOUBLE("d > 1.5", "d = "), + LESS_EQUALS_UINT64("u <= 5u", "u = [0-5]u"), + LESS_EQUALS_DOUBLE("d <= 5.5", "d = "), + LESS_EQUALS_STRING("role <= 'admin'", "role = "), + LESS_EQUALS_BYTES("by <= b'bytes'", "by = "), + GREATER_STRING("role > 'admin'", "role = "), + GREATER_BYTES("by > b'bytes'", "by = "), + DYNAMIC_LIST_COMPREHENSION_EXISTS("int_list.exists(x, x > 5)", "int_list = "), + DYNAMIC_MAP_COMPREHENSION_EXISTS("string_int_map.exists(k, k == 'test')", "string_int_map = "), + NULL_SATISFIABLE("unknown_var == null", "unknown_var = null"), + DYNAMIC_VAR_NUMERIC_EQUALITY("dyn_var == 1 && dyn_var == 1.0", "dyn_var = 1"), + DYNAMIC_VAR_NOT_IN_LIST( + "dyn_var == 1.5 && !(dyn_var in dyn_list) && size(dyn_list) > 5", "dyn_var = 1\\.5"), + CROSS_NUMERIC_EQUALITY_INT_DYN_EXACT("1 == request", "request = 1"), + MACRO_LIMIT("dyn_list.all(x, x == 1)", "Satisfying input:"), + STRUCT_FIELD_MISSING_APPROXIMATE_SATISFIABLE("dyn_var.unknown_field", "dyn_var = "), + MAP_INDEX_SATISFIABLE("string_int_map['alice'] > 0", "\"alice\": [1-9]\\d*"), + MAP_SIZE_GREATER_THAN_ONE_WITH_KEY( + "string_int_map.size() > 1 && string_int_map['foo'] == 42", + "string_int_map = \\{[^}]*,[^}]*\\}"), + MAP_SIZE_GREATER_THAN_ONE_WITH_LIST_ELEMENT( + "string_int_map.size() > 1 && string_int_map['a'] == int_list[0] && int_list.size() == 1", + "string_int_map = \\{[^}]*,[^}]*\\}"), + DISTINCT_TRUNCATED_COMPREHENSIONS( + "dyn_list.all(x, x == 1) != dyn_list.all(x, x == 2)", "dyn_list = "), + DISTINCT_TRUNCATED_COMPREHENSIONS_FREE_VARS( + "dyn_list.all(e, x == x) != dyn_list.all(e, x == y)", "dyn_list = "), + DISTINCT_TRUNCATED_COMPREHENSIONS_STRUCTS( + "dyn_list.all(e, e == TestAllTypes{single_int64: 1}) !=" + + " dyn_list.all(e, e == TestAllTypes{single_int32: 1})", + "dyn_list = "), + DISTINCT_TRUNCATED_COMPREHENSIONS_STRUCT_MESSAGE_NAMES( + "dyn_list.all(e, e == TestAllTypes{single_int64: 1}) !=" + + " dyn_list.all(e, e == TestAllTypes.NestedMessage{bb: 1})", + "dyn_list = "), + MAP_SIZE_GREATER_THAN_CONSTRAINED_KEYS( + "string_int_map.size() == 5 && string_int_map['a'] == 10", "\"a\": 10"), + INT_MIN_DOUBLE_EQUALITY( + "dyn(request) == -9223372036854775808.0", "request = -9223372036854775[2-8]\\d+"), + INT_MAX_DOUBLE_EQUALITY( + "dyn(request) == 9223372036854775808.0", "request = 9223372036854775[2-8]\\d+"), + UINT_MAX_DOUBLE_EQUALITY("dyn(u) == 18446744073709551616.0", "u = 1844674407370955\\d+u"), + ; final String expr; + final ImmutableList expectedFragments; - IsSatisfiableTestCase(String expr) { + IsSatisfiableTestCase(String expr, String... expectedFragments) { this.expr = expr; + this.expectedFragments = ImmutableList.copyOf(expectedFragments); } } @@ -183,6 +212,9 @@ public void isSatisfiable_success(@TestParameter IsSatisfiableTestCase testCase) CelVerificationResult result = VERIFIER.isSatisfiable(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + for (String fragment : testCase.expectedFragments) { + assertThat(result.message()).containsMatch(fragment); + } } @Test @@ -197,6 +229,93 @@ public void isSatisfiable_withVariable_returnsSatisfyingModel() throws Exception assertThat(result.message()).containsMatch("x = (?:[6-9]|[1-9]\\d+)"); } + @Test + public void isSatisfiable_mapNoContainerError_returnsSatisfyingModel() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("string_int_map.size() == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("Condition is satisfiable."); + assertThat(result.message()).contains("Satisfying input:"); + assertThat(result.message()).contains("string_int_map = {"); + assertThat(result.message()).doesNotContain("Error"); + } + + @Test + public void isSatisfiable_listNoContainerError_returnsSatisfyingModel() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("dyn_list.size() == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("Condition is satisfiable."); + assertThat(result.message()).contains("Satisfying input:"); + assertThat(result.message()).contains("dyn_list = ["); + assertThat(result.message()).doesNotContain("Error"); + } + + @Test + public void isSatisfiable_dynMapNoContainerError_returnsSatisfyingModel() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("dyn_map.size() == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("Condition is satisfiable."); + assertThat(result.message()).contains("Satisfying input:"); + assertThat(result.message()).contains("dyn_map = {"); + assertThat(result.message()).doesNotContain("Error"); + } + + @Test + public void counterexample_nullValueFormattedAsNull() throws Exception { + CelAbstractSyntaxTree ast = CEL.compile("unknown_var == 3u && request == null").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("request = null"); + } + + @Test + public void counterexample_mapFormattedCorrectly() throws Exception { + CelAbstractSyntaxTree ast = + CEL.compile("string_int_map.size() == 2 && string_int_map['a'] == 1").getAst(); + + CelVerificationResult result = VERIFIER.isSatisfiable(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).containsMatch("string_int_map = \\{[^}]*,[^}]*\\}"); + assertThat(result.message()).contains("\"a\": 1"); + } + + private enum CounterexampleNeverErrorTestCase { + DYN_LIST_REFLEXIVITY("dyn_list.size() == 1 ? dyn_list[0] == dyn_list[0] : true"), + DYN_MAP_REFLEXIVITY("dyn_map.size() == 1 ? dyn_map[1] == dyn_map[1] : true"), + DYN_LIST_ELEMENT("size(dyn_list) == 1 && dyn_list[0] == 'impossible_value'"), + DYN_MAP_VALUE("size(dyn_map) == 1 && dyn_map['a'] == 'impossible_value'"), + STRUCT_FIELD_VALUE("test_all_types.single_int64 == 12345 && false"), + ; + + final String expr; + + CounterexampleNeverErrorTestCase(String expr) { + this.expr = expr; + } + } + + @Test + public void isAlwaysTrue_counterexampleNeverContainsError( + @TestParameter CounterexampleNeverErrorTestCase testCase) throws Exception { + CelAbstractSyntaxTree ast = CEL.compile(testCase.expr).getAst(); + + CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.message()).doesNotContain("Error"); + } + @Test public void isSatisfiable_unconditional_returnsUnconditionalMessage() throws Exception { CelAbstractSyntaxTree ast = CEL.compile("1 + 1 == 2").getAst(); @@ -261,7 +380,7 @@ public void isSatisfiable_maskedByBmcNested_inconclusive() throws Exception { CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); CelVerifier customVerifier = - CelVerifierFactory.newVerifier() + CelVerifierFactory.newVerifier(CEL) .setComprehensionUnrollLimit(3) .setTypeProvider(TYPE_PROVIDER) .build(); @@ -276,7 +395,8 @@ public void isSatisfiable_comprehensionZeroUnrollLimit_inconclusive() throws Exc String expr = "int_list == [1] ? int_list.exists(x, x == 1) : false"; CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build(); CelVerificationResult result = verifier.isSatisfiable(ast); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); @@ -291,7 +411,37 @@ private enum IsUnsatisfiableTestCase { TIMESTAMP_INEQUALITY_CONTRADICTION( "timestamp('2023-01-01T00:00:00Z') != timestamp('2023-01-01T00:00:00Z')"), TYPE_TIMESTAMP_NOT_INT("type(timestamp('1970-01-01T00:00:00Z')) == int"), - DYN_INT_NOT_DURATION("dyn(1) == dyn(duration('1s'))"); + DYN_INT_NOT_DURATION("dyn(1) == dyn(duration('1s'))"), + DYNAMIC_MAP_DUPLICATE_KEYS_CONTRADICTION( + "size(string_int_map) == 2 && string_int_map.all(k, k == 'a')"), + EMPTY_MAP_WITH_KEY_IN("string_int_map.size() == 0 && 'foo' in string_int_map"), + KEY_IN_EMPTY_MAP("('x' in string_int_map) && string_int_map.size() == 0"), + EMPTY_MAP_AND_LIST_WITH_KEY_IN( + "int_list.size() == string_int_map.size() && int_list.size() == 0 && 'a' in" + + " string_int_map"), + MAP_SIZE_ONE_TWO_KEYS( + "string_int_map.size() == 1 && string_int_map['a'] == 1 && string_int_map['b'] == 2"), + MAP_SIZE_LESS_THAN_TWO_TWO_KEYS( + "string_int_map['foo'] == 10 && string_int_map['bar'] == 20 && string_int_map.size() < 2"), + MAP_SIZE_ONE_SUM_TWO_KEYS( + "string_int_map['a'] + string_int_map['b'] == 10 && string_int_map.size() == 1"), + MAP_SIZE_ONE_TWO_EQUAL_KEYS( + "string_int_map.size() == 1 && string_int_map['foo'] == 10 && string_int_map['bar'] == 10"), + MAP_SIZE_TWO_THREE_KEYS( + "string_int_map['k1'] == 1 && string_int_map['k2'] == 2 && string_int_map['k3'] == 3 &&" + + " string_int_map.size() == 2"), + EMPTY_MAP_KEY_LOOKUP("string_int_map['a'] > 100 && string_int_map.size() == 0"), + EMPTY_MAP_DYNAMIC_KEY_LOOKUP("string_int_map[string_var] == 100 && string_int_map.size() == 0"), + INT_NON_INTEGER_DOUBLE_EQUALITY("dyn(x) == 1.5"), + INT_OUT_OF_BOUNDS_POS_DOUBLE_EQUALITY("dyn(x) == 9223372036854777856.0"), + INT_OUT_OF_BOUNDS_NEG_DOUBLE_EQUALITY("dyn(x) == -9223372036854777856.0"), + UINT_NEGATIVE_DOUBLE_EQUALITY("dyn(u) == -1.0"), + UINT_NON_INTEGER_DOUBLE_EQUALITY("dyn(u) == 1.5"), + UINT_OUT_OF_BOUNDS_POS_DOUBLE_EQUALITY("dyn(u) == 18446744073709555712.0"), + INT_OUT_OF_BOUNDS_LARGE_DOUBLE_EQUALITY("dyn(x) == 1e100"), + INT_OUT_OF_BOUNDS_LARGE_NEG_DOUBLE_EQUALITY("dyn(x) == -1e100"), + UINT_OUT_OF_BOUNDS_LARGE_DOUBLE_EQUALITY("dyn(u) == 1e100"), + ; final String expr; @@ -409,7 +559,7 @@ private enum IsAlwaysTrueTestCase { "{'a': x, 'b': y}.all(z, {'a': x, 'b': y}.exists(z, z == 'a' || z == 'b'))"), MAP_LITERAL_VARIABLE_VALUE("{'a': x}['a'] == x"), HETEROGENEOUS_LARGE_UINT_INT_VARIABLE_NEQ( - "unknown_var == " + CelZ3TypeSystem.MAX_UINT64 + "u ? unknown_var != -1 : true"), + "unknown_var == " + CelNumericBounds.MAX_UINT64 + "u ? unknown_var != -1 : true"), MAP_LITERAL_VARIABLE_KEY("x != y ? {x: 1, y: 2}[x] == 1 : true"), MAP_MACRO_LIST_RETURN("{'a': 1, 'b': 2}.map(x, x + 'a') == ['aa', 'ba']"), MAP_LITERAL_NESTED_LIST("{'a': [1, 2]} == {'a': [1, 2]}"), @@ -586,12 +736,27 @@ private enum IsAlwaysTrueTestCase { "unknown_var == 9223372036854775807 ? unknown_var != 1e100 : true"), HETEROGENEOUS_MAX_EXACT_INT("dyn(9007199254740992) == 9007199254740992.0"), HETEROGENEOUS_MIN_EXACT_INT("dyn(-9007199254740992) == -9007199254740992.0"), - HETEROGENEOUS_INT_PRECISION_LOSS_POS("dyn(9007199254740993) != 9007199254740992.0"), - HETEROGENEOUS_INT_PRECISION_LOSS_NEG("dyn(-9007199254740993) != -9007199254740992.0"), - HETEROGENEOUS_UINT_PRECISION_LOSS("dyn(9007199254740993u) != 9007199254740992.0"), + HETEROGENEOUS_INT_PRECISION_LOSS_POS("dyn(9007199254740993) == 9007199254740992.0"), + HETEROGENEOUS_INT_PRECISION_LOSS_NEG("dyn(-9007199254740993) == -9007199254740992.0"), + HETEROGENEOUS_UINT_PRECISION_LOSS("dyn(9007199254740993u) == 9007199254740992.0"), HETEROGENEOUS_LONG_MAX_VS_DOUBLE("dyn(9223372036854775807) == 9223372036854775808.0"), - HETEROGENEOUS_LONG_MIN_VS_DOUBLE("dyn(-9223372036854775808) == -9223372036854775808.0"), - HETEROGENEOUS_UINT_MAX_VS_DOUBLE("dyn(18446744073709551615u) != 18446744073709551616.0"), + HETEROGENEOUS_STATIC_INT_DOUBLE_EQ("dyn(1) == 1.0"), + HETEROGENEOUS_STATIC_UINT_DOUBLE_EQ("dyn(1u) == 1.0"), + HETEROGENEOUS_STATIC_INT_UINT_EQ("dyn(1) == 1u"), + HETEROGENEOUS_LONG_MIN_VS_DOUBLE( + "dyn_var == -9223372036854775808.0 ? dyn_var == -9223372036854775808.0 : true"), + HETEROGENEOUS_UINT_MAX_VS_DOUBLE("dyn(18446744073709551615u) == 18446744073709551616.0"), + HETEROGENEOUS_UINT_OVERFLOW_VS_DOUBLE("dyn_var == 1e100 ? type(dyn_var) != uint : true"), + HETEROGENEOUS_UINT_NEG_VS_DOUBLE("dyn_var == -1.0 ? type(dyn_var) != uint : true"), + HETEROGENEOUS_INT_OVERFLOW_VS_DOUBLE("dyn_var == 1e100 ? type(dyn_var) != int : true"), + HETEROGENEOUS_INT_UNDERFLOW_VS_DOUBLE( + "dyn_var == -9223372036854777856.0 ? type(dyn_var) != int : true"), + HETEROGENEOUS_INT_NON_INTEGER_DOUBLE_INEQUALITY("dyn(x) != 1.5"), + HETEROGENEOUS_INT_OUT_OF_BOUNDS_POS_DOUBLE_INEQUALITY("dyn(x) != 9223372036854777856.0"), + HETEROGENEOUS_INT_OUT_OF_BOUNDS_NEG_DOUBLE_INEQUALITY("dyn(x) != -9223372036854777856.0"), + HETEROGENEOUS_UINT_NON_INTEGER_DOUBLE_INEQUALITY("dyn(u) != 1.5"), + HETEROGENEOUS_UINT_OUT_OF_BOUNDS_POS_DOUBLE_INEQUALITY("dyn(u) != 18446744073709555712.0"), + HETEROGENEOUS_UINT_OUT_OF_BOUNDS_NEG_DOUBLE_INEQUALITY("dyn(u) != -1.0"), HETEROGENEOUS_DYNAMIC_PRECISION( "type(dyn_var) == int && type(dyn_var2) == double && dyn_var == 9007199254740993 &&" + " dyn_var2 == 9007199254740992.0 ? dyn_var != dyn_var2 : true"), @@ -618,6 +783,8 @@ private enum IsAlwaysTrueTestCase { DYNAMIC_LIST_RESOLVES_CORRELATED_NESTING( "int_list == [1, 2] && int_list_2 == [2, 3] ? int_list.exists(x, int_list_2.exists(y, x" + " == y)) : true"), + DYNAMIC_LIST_ELEMENT_NEVER_ERROR( + "size(dyn_list) > 0 ? (dyn_list[0] == 1 || dyn_list[0] != 1) : true"), DYNAMIC_MAP_EXISTS( "string_int_map == {'a': 1, 'b': 2} ? string_int_map.exists(k, string_int_map[k] == 2)" + " : true"), @@ -747,6 +914,18 @@ private enum IsAlwaysTrueTestCase { UINT64_BOUNDS_ALWAYS_TRUE("u <= 18446744073709551615u && u >= 0u"), MODULO_INT64_MIN_INT_BY_NEG_ONE_ALWAYS_ZERO( "x == -9223372036854775808 && y == -1 ? x % y == 0 : true"), + DYNAMIC_VAR_TYPE_IDENTITY("type(dyn_var) == type(dyn_var)"), + DYNAMIC_MAP_KEY_COMPREHENSION_TYPE_IDENTITY( + "size(dyn_map) > 0 && size(dyn_map) <= 5 ? dyn_map.all(k, type(k) == type(k)) : true"), + DYNAMIC_MAP_VALUE_NOT_ERROR( + "size(dyn_map) == 1 && 1 in dyn_map ? dyn_map.all(k, v, v == 1 || v != 1) : true"), + MAP_KEY_TYPE_CONSTRAINT( + "size(string_int_map) > 0 && size(string_int_map) <= 5 ?" + + " string_int_map.all(k, type(k) == string) : true"), + MAP_VALUE_TYPE_CONSTRAINT( + "size(string_int_map) > 0 && size(string_int_map) <= 5 ?" + + " string_int_map.all(k, v, v >= -9223372036854775808 &&" + + " v <= 9223372036854775807) : true"), ; final String expr; @@ -778,7 +957,7 @@ public void isAlwaysTrue_withUnknownIdentifier_evaluatesToUnknown( CelAbstractSyntaxTree ast = CEL.compile(expression).getAst(); CelVerifier verifierWithUnknown = - CelVerifierFactory.newVerifier().addUnknownIdentifier("x").build(); + CelVerifierFactory.newVerifier(CEL).addUnknownIdentifier("x").build(); // 'x == x' is not a tautology if it can be unknown // i.e: CelUnknown == CelUnknown is unknown. @@ -800,7 +979,10 @@ public void isAlwaysTrue_dynamicComprehensionNonBoolYieldsError() throws Excepti + " dyn_list.all(x, x.not_a_bool) == false) : true"; CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); CelVerificationResult result = - CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(1).build().isAlwaysTrue(ast); + CelVerifierFactory.newVerifier(CEL) + .setComprehensionUnrollLimit(1) + .build() + .isAlwaysTrue(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); assertThat(result.message()) @@ -814,7 +996,8 @@ public void isAlwaysTrue_comprehensionExceedsMaxIterations_returnsUnknown() thro String expr = "int_list == [1, 2, 3] ? int_list.all(x, x > 0) : true"; CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(2).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(2).build(); CelVerificationResult verifiedValue = verifier.isAlwaysTrue(ast); // Truncated loops return Unknown, which negates to Unknown. @@ -831,7 +1014,8 @@ public void isAlwaysTrue_comprehensionZeroUnrollLimit_emptyList() throws Excepti String expr = "int_list == [] ? int_list.all(x, x > 0) : true"; CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build(); CelVerificationResult verifiedValue = verifier.isAlwaysTrue(ast); assertThat(verifiedValue.status()).isEqualTo(VerificationStatus.VERIFIED); @@ -889,7 +1073,9 @@ public void verifyEquivalence_unknownPrecedenceOverError() throws Exception { CelAbstractSyntaxTree astB = celWithCustomFunc.compile("1 / 0").getAst(); CelVerifier verifier = - CelVerifierFactory.newVerifier().addUnknownIdentifier("unknown_var").build(); + CelVerifierFactory.newVerifier(celWithCustomFunc) + .addUnknownIdentifier("unknown_var") + .build(); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); @@ -899,6 +1085,18 @@ public void verifyEquivalence_unknownPrecedenceOverError() throws Exception { assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); } + @Test + public void verifyEquivalence_freeVariableIndicesDeduplicated() throws Exception { + CelAbstractSyntaxTree astA = + CEL.compile("x == y && y == port ? dyn_list.all(e, x == x) : false").getAst(); + CelAbstractSyntaxTree astB = + CEL.compile("x == y && y == port ? dyn_list.all(e, y == port) : false").getAst(); + + CelVerificationResult result = VERIFIER.verifyEquivalence(astA, astB); + + assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); + } + @Test public void isSatisfiable_approximateIterRangeInMap_inconclusive() throws Exception { Cel celWithCustomFunc = @@ -1266,7 +1464,7 @@ private enum IsAlwaysTrueViolationTestCase { + "? dyn_map[1 + 1] == [] : true", "Condition is not always true\\.", "Counterexample input:", - "dyn_map = \\{\\}"), + "dyn_map = \\{.*\\}"), DYNAMIC_MAP_COMPREHENSION_NESTED_EQUALITY_VIOLATION( "cel.bind(r, request, r.l == [[1], [2], [3], [4], [5]] && r.m == {1: [1], 2: [2]," + " 3: [3]} ? r.l.all(x, r.m.exists(k, r.m[k] == x)) : true)", @@ -1420,7 +1618,10 @@ private enum IsInconclusiveTestCase { COMPREHENSION_NULL_CONSTANT("size(int_list) == 6 ? size(int_list.map(x, null)) == 6 : true"), COMPREHENSION_UINT_CONSTANT("size(int_list) == 6 ? size(int_list.map(x, 1u)) == 6 : true"), COMPREHENSION_DOUBLE_CONSTANT("size(int_list) == 6 ? size(int_list.map(x, 1.0)) == 6 : true"), - COMPREHENSION_BYTES_CONSTANT("size(int_list) == 6 ? size(int_list.map(x, b'abc')) == 6 : true"); + COMPREHENSION_BYTES_CONSTANT("size(int_list) == 6 ? size(int_list.map(x, b'abc')) == 6 : true"), + COMPREHENSION_FREE_VAR_INDEX_DEDUPLICATION( + "x == y && y == port ? dyn_list.all(e, x == x) == dyn_list.all(e, y == port) : true"), + ; final String expr; @@ -1524,6 +1725,9 @@ private enum EquivalenceTestCase { MACRO_EXISTS_ONE_EQUIVALENT( "[1, 2, 3].exists_one(x, x == 2)", "(1 == 2 ? 1 : 0) + (2 == 2 ? 1 : 0) + (3 == 2 ? 1 : 0) == 1"), + TIMESTAMP_CONVERSION_OVERFLOW_EQUIVALENCE( + "timestamp(string_var) <= timestamp(253402300799)", + "timestamp(string_var) == timestamp(string_var)"), TIMESTAMP_MATH_SUBTRACT_TS( "timestamp(900000) - timestamp(100)", "timestamp(899900) - timestamp(0)"), TIMESTAMP_MATH_COMMUTATIVITY( @@ -1776,7 +1980,27 @@ private enum EquivalenceTestCase { OPTIONAL_INDEX_LIST_UNWRAPPING("optional.of([1, 2, 3])[?0]", "optional.of(1)"), OPTIONAL_INDEX_MAP_UNWRAPPING("optional.of({'a': 1})[?'a']", "optional.of(1)"), OPTIONAL_INDEX_UNWRAPPING_NONE("optional.none()[?0]", "optional.none()"), - INT_IN_LIST_IDENTITY_EQUIVALENT("x in [1, 2, x]", "true"); + INT_IN_LIST_IDENTITY_EQUIVALENT("x in [1, 2, x]", "true"), + HETEROGENEOUS_INT_NON_INTEGER_DOUBLE_EQUIVALENCE("dyn(x) == 1.5", "false"), + HETEROGENEOUS_INT_OUT_OF_BOUNDS_DOUBLE_EQUIVALENCE("dyn(x) == 9223372036854777856.0", "false"), + HETEROGENEOUS_UINT_NON_INTEGER_DOUBLE_EQUIVALENCE("dyn(u) == 1.5", "false"), + HETEROGENEOUS_UINT_OUT_OF_BOUNDS_DOUBLE_EQUIVALENCE( + "dyn(u) == 18446744073709555712.0", "false"), + HETEROGENEOUS_UINT_NEGATIVE_DOUBLE_EQUIVALENCE("dyn(u) == -1.0", "false"), + HETEROGENEOUS_UINT_ZERO_DOUBLE_EQUIVALENCE("dyn(u) == 0.0", "u == 0u"), + DYNAMIC_LIST_ELEMENT_NEVER_ERROR_EQUIVALENCE( + "size(dyn_list) > 0 ? (dyn_list[0] == 1 || dyn_list[0] != 1) : true", "true"), + CANONICALIZE_MAP_TWO_VAR_PREDICATE_ORDER( + "string_int_map.exists(k, v, k == 'foo' && v == 1)", + "string_int_map.exists(k, v, v == 1 && k == 'foo')"), + CANONICALIZE_MAP_TWO_VAR_ALPHA_RENAME( + "string_int_map.exists(k, v, k == 'foo' && v == 1)", + "string_int_map.exists(key, val, key == 'foo' && val == 1)"), + CANONICALIZE_MAP_TWO_VAR_DE_MORGAN( + "!string_int_map.exists(k, v, !(v > 0))", "string_int_map.all(k, v, v > 0)"), + CANONICALIZE_LIST_PREDICATE_ORDER( + "int_list.all(e, e > 0 && e < 100)", "int_list.all(e, e < 100 && e > 0)"), + CANONICALIZE_LIST_ALPHA_RENAME("int_list.all(e, e > 0)", "int_list.all(elem, elem > 0)"); private final String exprA; private final String exprB; @@ -2162,7 +2386,7 @@ public void verifyEquivalence_functionError_equivalent() throws Exception { @Test @SuppressWarnings("GoodTime-ApiWithNumericTimeUnit") // Test only public void setTimeout_invalidDuration_throws(@TestParameter({"0", "-1"}) long timeoutSeconds) { - CelVerifierBuilder builder = CelVerifierFactory.newVerifier(); + CelVerifierBuilder builder = CelVerifierFactory.newVerifier(CEL); IllegalArgumentException exception = assertThrows( IllegalArgumentException.class, @@ -2181,9 +2405,6 @@ public void isSatisfiable_divisionByZero_failsInCelWithErrors() throws Exception @Test public void isSatisfiable_timeoutReached_throwsCelVerificationException() throws Exception { - CelVerifier timeoutVerifier = - CelVerifierFactory.newVerifier().setTimeout(Duration.ofMillis(1)).build(); - Cel customCel = CelFactory.plannerCelBuilder() .addVar("d1", SimpleType.DOUBLE) @@ -2191,6 +2412,8 @@ public void isSatisfiable_timeoutReached_throwsCelVerificationException() throws .addVar("d3", SimpleType.DOUBLE) .addVar("d4", SimpleType.DOUBLE) .build(); + CelVerifier timeoutVerifier = + CelVerifierFactory.newVerifier(customCel).setTimeout(Duration.ofMillis(1)).build(); // An overly complex double multiplication to guarantee Z3 FPA theory solver timeouts. CelAbstractSyntaxTree ast = @@ -2614,7 +2837,7 @@ public void isAlwaysTrue_largeListCounterexample_truncatesOutput() throws Except CelAbstractSyntaxTree ast = cel.compile("!(large_list == " + listLiteral + ")").getAst(); CelVerifier verifier = - CelVerifierFactory.newVerifier().setTimeout(Duration.ofSeconds(10)).build(); + CelVerifierFactory.newVerifier(cel).setTimeout(Duration.ofSeconds(10)).build(); CelVerificationResult result = verifier.isAlwaysTrue(ast); @@ -2622,6 +2845,50 @@ public void isAlwaysTrue_largeListCounterexample_truncatesOutput() throws Except assertThat(result.message()).contains("... (5 more elements)"); } + @Test + public void isAlwaysTrue_largeMapCounterexample_truncatesOutput() throws Exception { + Cel cel = + CelFactory.plannerCelBuilder() + .addVar("large_map", MapType.create(SimpleType.INT, SimpleType.INT)) + .build(); + StringBuilder mapLiteral = new StringBuilder("{"); + for (int i = 0; i < 20; i++) { + mapLiteral.append(i).append(": 1"); + if (i < 19) { + mapLiteral.append(", "); + } + } + mapLiteral.append("}"); + + CelAbstractSyntaxTree ast = cel.compile("!(large_map == " + mapLiteral + ")").getAst(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(cel).setTimeout(Duration.ofSeconds(10)).build(); + + CelVerificationResult result = verifier.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.message()).contains("... (5 more entries)"); + } + + @Test + public void counterexample_messageTwoFieldsFormatted() throws Exception { + Cel cel = + CelFactory.plannerCelBuilder() + .setContainer(CelContainer.ofName("cel.expr.conformance.proto3")) + .addMessageTypes(TestAllTypes.getDescriptor()) + .addVar("msg", StructTypeReference.create("cel.expr.conformance.proto3.TestAllTypes")) + .setTypeProvider(TYPE_PROVIDER) + .build(); + CelAbstractSyntaxTree ast = + cel.compile("!(msg == TestAllTypes{single_int32: 1, single_int64: 2})").getAst(); + + CelVerificationResult result = VERIFIER.isAlwaysTrue(ast); + + assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); + assertThat(result.message()).contains("single_int32: 1"); + assertThat(result.message()).contains("single_int64: 2"); + } + @Test public void isAlwaysTrue_customComprehensionWithTrueAccuInit() throws Exception { Cel cel = @@ -2646,7 +2913,7 @@ public void isAlwaysTrue_customComprehensionWithTrueAccuInit() throws Exception .build(); CelAbstractSyntaxTree ast = cel.compile("dyn_list == [1, 2] ? dyn_list.custom_fold(x) == true : true").getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().build(); + CelVerifier verifier = CelVerifierFactory.newVerifier(cel).build(); CelVerificationResult result = verifier.isAlwaysTrue(ast); @@ -2661,7 +2928,8 @@ public void isSatisfiable_maskedByBmcButAlwaysFalse_returnsFailed() throws Excep String expr = "int_list == [1, 2, 3, 4] ? int_list.exists(x, x == 42) && false : false"; CelAbstractSyntaxTree ast = CEL.compile(expr).getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(3).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(3).build(); CelVerificationResult result = verifier.isSatisfiable(ast); assertThat(result.status()).isEqualTo(VerificationStatus.VIOLATED); @@ -2676,7 +2944,8 @@ public void verifyEquivalence_maskedByBmcButAlwaysEqual_returnsVerified() throws CelAbstractSyntaxTree astA = CEL.compile(exprA).getAst(); CelAbstractSyntaxTree astB = CEL.compile(exprB).getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(3).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(3).build(); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); @@ -2703,7 +2972,8 @@ public void verifyEquivalence_zeroUnrollLimit_returnsInconclusive( CelAbstractSyntaxTree astA = CEL.compile(testCase.exprA).getAst(); CelAbstractSyntaxTree astB = CEL.compile(testCase.exprB).getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(0).build(); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); @@ -2752,7 +3022,8 @@ public void verifyEquivalence_comprehensionScopeShadowing_returnsInconclusive() CelAbstractSyntaxTree astA = customCel.compile("dyn_list.my_macro_1(true)").getAst(); CelAbstractSyntaxTree astB = customCel.compile("dyn_list.my_macro_2(true)").getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(customCel).setComprehensionUnrollLimit(0).build(); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); @@ -2796,7 +3067,8 @@ public void verifyEquivalence_comprehensionResultScopeIsolation_returnsInconclus CelAbstractSyntaxTree astB = customCel.compile("cel.bind(x, 20, dyn_list.my_macro(1))").getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(0).build(); + CelVerifier verifier = + CelVerifierFactory.newVerifier(customCel).setComprehensionUnrollLimit(0).build(); CelVerificationResult result = verifier.verifyEquivalence(astA, astB); assertThat(result.status()).isEqualTo(VerificationStatus.INCONCLUSIVE); @@ -2804,9 +3076,6 @@ public void verifyEquivalence_comprehensionResultScopeIsolation_returnsInconclus @Test public void verifyEquivalence_timeoutReached_throwsCelVerificationException() throws Exception { - CelVerifier timeoutVerifier = - CelVerifierFactory.newVerifier().setTimeout(Duration.ofMillis(1)).build(); - Cel customCel = CelFactory.plannerCelBuilder() .addVar("d1", SimpleType.DOUBLE) @@ -2815,6 +3084,9 @@ public void verifyEquivalence_timeoutReached_throwsCelVerificationException() th .addVar("d4", SimpleType.DOUBLE) .build(); + CelVerifier timeoutVerifier = + CelVerifierFactory.newVerifier(customCel).setTimeout(Duration.ofMillis(1)).build(); + CelAbstractSyntaxTree astA = customCel .compile( @@ -2836,7 +3108,7 @@ public void verifyImplication_loopExceedsLimit_returnsTruncatedInconclusive() th CelAbstractSyntaxTree assertAst = CEL.compile("int_list.all(x, x > 0)").getAst(); CelVerifier verifier = - CelVerifierFactory.newVerifier().setComprehensionUnrollLimit(2).build(); + CelVerifierFactory.newVerifier(CEL).setComprehensionUnrollLimit(2).build(); CelVerificationResult result = ((CelVerifierZ3Impl) verifier) .verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Implication"); @@ -2853,10 +3125,11 @@ public void verifyImplication_symbolicNan_crossNumericComparisonReturnsFalse() t // Assertion: x < d is false when d is NaN CelAbstractSyntaxTree assertAst = CEL.compile("!(x < d)").getAst(); - CelVerifier verifier = CelVerifierFactory.newVerifier().build(); + CelVerifier verifier = CelVerifierFactory.newVerifier(CEL).build(); CelVerificationResult result = ((CelVerifierZ3Impl) verifier) .verifyImplication(assumeAst, assertAst, ImmutableMap.of(), "Implication"); assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); } } + diff --git a/verifier/src/test/java/dev/cel/verifier/tools/BUILD.bazel b/verifier/src/test/java/dev/cel/verifier/tools/BUILD.bazel new file mode 100644 index 000000000..6077e4950 --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/BUILD.bazel @@ -0,0 +1,31 @@ +load("@rules_java//java:defs.bzl", "java_library") +load("//:testing.bzl", "junit4_test_suites") + +package( + default_applicable_licenses = ["//:license"], +) + +java_library( + name = "tests", + testonly = True, + srcs = glob(["*.java"]), + deps = [ + "//:java_truth", + "//common/types", + "//common/types:type_providers", + "//verifier", + "//verifier/tools", + "@maven//:com_google_guava_guava", + "@maven//:info_picocli_picocli", + "@maven//:junit_junit", + ], +) + +junit4_test_suites( + name = "test_suites", + sizes = [ + "small", + ], + src_dir = "src/test/java", + deps = [":tests"], +) diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java new file mode 100644 index 000000000..88cd62b88 --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java @@ -0,0 +1,208 @@ +// 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.tools; + +import static com.google.common.truth.Truth.assertThat; +import static java.nio.charset.StandardCharsets.UTF_8; + +import java.io.BufferedReader; +import java.io.ByteArrayOutputStream; +import java.io.PrintStream; +import java.io.StringReader; +import org.junit.Before; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.JUnit4; + +@RunWith(JUnit4.class) +public final class CelVerifierReplTest { + + @Before + public void setUp() { + System.setProperty("z3.skipLibraryLoad", "true"); + } + + @SuppressWarnings({"PreferCharsetOverload", "JdkObsolete"}) + private String[] runReplWithCommands(String... commands) throws Exception { + String input = String.join("\n", commands) + "\n"; + BufferedReader reader = new BufferedReader(new StringReader(input)); + ByteArrayOutputStream outStream = new ByteArrayOutputStream(); + ByteArrayOutputStream errStream = new ByteArrayOutputStream(); + PrintStream out = new PrintStream(outStream, true, UTF_8.name()); + PrintStream err = new PrintStream(errStream, true, UTF_8.name()); + + CelVerifierRepl.runRepl(reader, out, err); + + return new String[] { + new String(outStream.toByteArray(), UTF_8), new String(errStream.toByteArray(), UTF_8) + }; + } + + @Test + public void repl_quitAndExit() throws Exception { + String[] output1 = runReplWithCommands(":quit"); + assertThat(output1[0]).contains("Goodbye!"); + + String[] output2 = runReplWithCommands(":exit"); + assertThat(output2[0]).contains("Goodbye!"); + } + + @Test + public void repl_helpCommands() throws Exception { + String[] output = + runReplWithCommands( + ":help", + ":help var", + ":help unknown", + ":help timeout", + ":help unroll", + ":help sat", + ":help valid", + ":help equiv", + ":help non_existent_topic", + ":quit"); + assertThat(output[0]).contains("REPL Commands:"); + assertThat(output[0]).contains("Command: :var "); + assertThat(output[0]).contains("Command: :unknown "); + assertThat(output[0]).contains("Command: :timeout "); + assertThat(output[0]).contains("Command: :unroll "); + assertThat(output[0]).contains("Query: sat "); + assertThat(output[0]).contains("Query: valid "); + assertThat(output[0]).contains("Query: equiv <=> "); + } + + @Test + public void repl_varDeclarations() throws Exception { + String[] output = + runReplWithCommands( + ":var role string", + ":var port int", + ":var scores map", + ":var tags list", + ":vars", + ":quit"); + assertThat(output[0]).contains("Variable declared: role : string"); + assertThat(output[0]).contains("Variable declared: port : int"); + assertThat(output[0]).contains("Variable declared: scores : map(string, int)"); + assertThat(output[0]).contains("Variable declared: tags : list(string)"); + assertThat(output[0]).contains("Variables (4):"); + } + + @Test + public void repl_unknownIdentifiers() throws Exception { + String[] output = + runReplWithCommands(":unknown request.headers", ":unknown request.auth", ":vars", ":quit"); + assertThat(output[0]).contains("Added unknown identifier: 'request.headers'"); + assertThat(output[0]).contains("Added unknown identifier: 'request.auth'"); + assertThat(output[0]).contains("Unknowns: [request.headers, request.auth]"); + } + + @Test + public void repl_timeoutConfiguration() throws Exception { + String[] output = + runReplWithCommands( + ":timeout 15", ":vars", ":timeout -5", ":timeout abc", ":timeout", ":quit"); + assertThat(output[0]).contains("Timeout set to 15s."); + assertThat(output[0]).contains("Timeout: 15s"); + assertThat(output[1]).contains("Timeout must be a positive integer."); + assertThat(output[1]).contains("Invalid timeout value."); + assertThat(output[1]).contains("Usage: :timeout "); + } + + @Test + public void repl_unrollConfiguration() throws Exception { + String[] output = + runReplWithCommands(":unroll 10", ":vars", ":unroll -1", ":unroll xyz", ":unroll", ":quit"); + assertThat(output[0]).contains("Comprehension unroll limit set to 10."); + assertThat(output[0]).contains("Unroll limit: 10"); + assertThat(output[1]).contains("Unroll limit must be non-negative."); + assertThat(output[1]).contains("Invalid unroll limit value."); + assertThat(output[1]).contains("Usage: :unroll "); + } + + @Test + public void repl_sessionStateAndClear() throws Exception { + String[] output = + runReplWithCommands( + ":var role string", ":unknown req.headers", ":vars", ":clear", ":vars", ":quit"); + assertThat(output[0]).contains("Variables (1):"); + assertThat(output[0]).contains("Session state reset."); + assertThat(output[0]).contains("Variables (0):"); + assertThat(output[0]).contains("Unknowns: none"); + } + + @Test + public void repl_satQueries() throws Exception { + String[] output = + runReplWithCommands(":var port int", "sat port > 1024", "port > 1024", "sat", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[1]).contains("Usage: sat "); + } + + @Test + public void repl_validQueries() throws Exception { + String[] output = + runReplWithCommands(":var x int", "valid x > 0 || x <= 0", "valid x > 0", "valid", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[0]).contains("[VIOLATED]"); + assertThat(output[1]).contains("Usage: valid "); + } + + @Test + public void repl_equivQueries() throws Exception { + String[] output = + runReplWithCommands(":var x int", "equiv x > 10 <=> 10 < x", "equiv x > 10", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[1]).contains("Equivalence query format: equiv <=> "); + } + + @Test + public void repl_equivDoubleNegation() throws Exception { + String[] output = runReplWithCommands(":var x int", "equiv !!(x == 10) <=> (x == 10)", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + } + + @Test + public void repl_equivCanonicalization() throws Exception { + String[] output = + runReplWithCommands( + ":var map_string_int map", + ":var int_list list", + "equiv map_string_int.exists(k, v, k == 'foo' && v == 1) <=> map_string_int.exists(k," + + " v, v == 1 && k == 'foo')", + "equiv int_list.all(e, e > 0) <=> int_list.all(elem, elem > 0)", + ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[1]).isEmpty(); + } + + @Test + public void repl_unknownCommandsAndErrors() throws Exception { + String[] output = + runReplWithCommands( + ":unknowncommand", + ":var", + ":var invalid_spec", + ":var x foo_type", + ":unknown", + "invalid + + syntax", + ":quit"); + assertThat(output[1]).contains("Unknown command: :unknowncommand"); + assertThat(output[1]).contains("Usage: :var "); + assertThat(output[1]).contains("Unsupported type"); + assertThat(output[1]).contains("Usage: :unknown "); + assertThat(output[1]).contains("Compilation error"); + } +} diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java new file mode 100644 index 000000000..e3b2a21a6 --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java @@ -0,0 +1,604 @@ +// 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.tools; + +import static com.google.common.truth.Truth.assertThat; +import static org.junit.Assert.assertThrows; + +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import dev.cel.common.types.CelType; +import dev.cel.common.types.ListType; +import dev.cel.common.types.MapType; +import dev.cel.common.types.SimpleType; +import dev.cel.verifier.CelVerificationResult; +import dev.cel.verifier.CelVerificationResult.VerificationStatus; +import java.io.File; +import java.io.PrintWriter; +import java.io.StringWriter; +import java.nio.charset.StandardCharsets; +import java.nio.file.Files; +import java.time.Duration; +import java.util.Arrays; +import org.junit.Before; +import org.junit.Rule; +import org.junit.Test; +import org.junit.rules.TemporaryFolder; +import org.junit.runner.RunWith; +import org.junit.runners.JUnit4; +import picocli.CommandLine; + +@RunWith(JUnit4.class) +public final class CelVerifierToolTest { + + @Rule public TemporaryFolder tempFolder = new TemporaryFolder(); + + @Before + public void setUp() { + System.setProperty("z3.skipLibraryLoad", "true"); + } + + private String executeToolWithOutput(String... args) { + StringWriter out = new StringWriter(); + PrintWriter pw = new PrintWriter(out); + CommandLine cmd = new CommandLine(new CelVerifierTool()); + cmd.setOut(pw); + cmd.setErr(pw); + cmd.execute(args); + return out.toString(); + } + + @Test + public void celVerifierTool_checkSat_jsonOutputFormat() { + String output = + executeToolWithOutput( + "check-sat", "--expr", "x > 0", "--var", "x:int", "--output_format", "json"); + assertThat(output).startsWith("{\n"); + assertThat(output).contains("\"status\": \"VERIFIED\""); + assertThat(output).contains("satisfiable"); + assertThat(output.trim()).endsWith("}"); + } + + @Test + public void celVerifierTool_checkSat_textOutputFormat() { + String output = + executeToolWithOutput("check-sat", "--expr", "x > 0", "--var", "x:int", "-fmt", "text"); + assertThat(output).contains("[VERIFIED]"); + assertThat(output).contains("satisfiable"); + } + + @Test + public void celVerifierTool_checkSat_withDynVariable() { + String output = + executeToolWithOutput( + "check-sat", "--expr", "x == 'hello'", "--var", "x:dyn", "-fmt", "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_checkSat_withUnknownOption() { + String output = + executeToolWithOutput( + "check-sat", + "--expr", + "request.headers != null", + "--var", + "request:map", + "-u", + "request.headers", + "-fmt", + "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_checkSat_withTimeoutAndUnrollLimit() { + String output = + executeToolWithOutput( + "check-sat", + "--expr", + "[1, 2, 3].all(x, x > 0)", + "--timeout", + "5", + "--unroll-limit", + "5", + "-fmt", + "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_verifyPolicy_fileNotFound() { + String output = executeToolWithOutput("verify-policy", "--file", "non_existent_policy.yaml"); + assertThat(output).contains("File not found: non_existent_policy.yaml"); + } + + @Test + public void parseVariables_success() { + ImmutableMap vars = + VerificationOptions.parseVariables( + Arrays.asList( + "x:int", + "role:string", + "is_admin:bool", + "tags:list", + "scores:map")); + assertThat(vars).containsEntry("x", SimpleType.INT); + assertThat(vars).containsEntry("role", SimpleType.STRING); + assertThat(vars).containsEntry("is_admin", SimpleType.BOOL); + assertThat(vars).containsEntry("tags", ListType.create(SimpleType.STRING)); + assertThat(vars).containsEntry("scores", MapType.create(SimpleType.STRING, SimpleType.INT)); + } + + @Test + public void parseVariables_allTypesIncludingDyn() { + ImmutableMap vars = + VerificationOptions.parseVariables( + Arrays.asList( + "u:uint", + "d:double", + "fl:float", + "b:bytes", + "dyn_val:dyn", + "flag:boolean", + "nested_list:list", + "nested_map:map")); + assertThat(vars).containsEntry("u", SimpleType.UINT); + assertThat(vars).containsEntry("d", SimpleType.DOUBLE); + assertThat(vars).containsEntry("fl", SimpleType.DOUBLE); + assertThat(vars).containsEntry("b", SimpleType.BYTES); + assertThat(vars).containsEntry("dyn_val", SimpleType.DYN); + assertThat(vars).containsEntry("flag", SimpleType.BOOL); + assertThat(vars).containsEntry("nested_list", ListType.create(SimpleType.DYN)); + assertThat(vars).containsEntry("nested_map", MapType.create(SimpleType.STRING, SimpleType.DYN)); + } + + @Test + public void parseVariables_invalidFormat_throws() { + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList("x_no_colon"))); + } + + @Test + public void parseVariables_unsupportedType_throws() { + IllegalArgumentException ex = + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList("x:foo_bar"))); + assertThat(ex) + .hasMessageThat() + .contains("Supported types: int, uint, string, bool, double, bytes, dyn"); + } + + @Test + public void parseVariables_invalidMapFormat_throws() { + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList("x:map"))); + } + + @Test + public void parseVariables_emptyOrNull_returnsEmptyMap() { + assertThat(VerificationOptions.parseVariables(null)).isEmpty(); + assertThat(VerificationOptions.parseVariables(ImmutableList.of())).isEmpty(); + } + + @Test + public void parseVariables_nestedTypes() { + ImmutableMap vars = + VerificationOptions.parseVariables( + Arrays.asList( + "nested_map:map>", + "nested_list_map:map>")); + assertThat(vars) + .containsEntry( + "nested_map", + MapType.create(SimpleType.STRING, MapType.create(SimpleType.STRING, SimpleType.INT))); + assertThat(vars) + .containsEntry( + "nested_list_map", MapType.create(SimpleType.STRING, ListType.create(SimpleType.INT))); + } + + @Test + public void parseVariables_emptyString_throws() { + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList(""))); + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(Arrays.asList(" "))); + } + + @Test + public void parseVariables_nullElement_throws() { + assertThrows( + NullPointerException.class, + () -> VerificationOptions.parseVariables(Arrays.asList((String) null))); + } + + @Test + public void checkSatisfiable_satisfiable() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = + ImmutableMap.of("role", SimpleType.STRING, "port", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable("role == 'editor' && port > 1024", vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + assertThat(result.message()).contains("satisfiable"); + } + + @Test + public void checkValid_valid() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("x", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.checkValid("x > 10 || x <= 10", vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void verifyEquivalence_equivalent() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("x", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.verifyEquivalence("x > 10", "10 < x", vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void verifyEquivalence_canonicalizedMapComprehension() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = + ImmutableMap.of("map_string_int", MapType.create(SimpleType.STRING, SimpleType.INT)); + + CelVerificationResult result = + CelVerifierToolCore.verifyEquivalence( + "map_string_int.exists(k, v, k == 'foo' && v == 1)", + "map_string_int.exists(k, v, v == 1 && k == 'foo')", + vars, + options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void verifyPolicyInvariants_success() 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: port_check\n" + + " assert:\n" + + " - port == 80 || port != 80\n"; + + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("port", SimpleType.INT); + + ImmutableMap results = + CelVerifierToolCore.verifyPolicyInvariants(yamlPolicy, vars, options); + + assertThat(results).containsKey("port_check"); + assertThat(results.get("port_check").status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void verifyPolicyEquivalence_equivalent() throws Exception { + String policyA = + "name: policy_a\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n"; + + String policyB = + "name: policy_b\n" + + "rule:\n" + + " match:\n" + + " - condition: 80 == port\n" + + " output: 'true'\n" + + " - output: 'false'\n"; + + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = ImmutableMap.of("port", SimpleType.INT); + + CelVerificationResult result = + CelVerifierToolCore.verifyPolicyEquivalence(policyA, policyB, vars, options); + + assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); + } + + @Test + public void formatTextPolicyResults_verifiedAndViolated() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult verifiedRes = + CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + CelVerificationResult violatedRes = + CelVerifierToolCore.checkValid("x > 0", ImmutableMap.of("x", SimpleType.INT), options); + + ImmutableMap results = + ImmutableMap.of("inv_1", verifiedRes, "inv_2", violatedRes); + + String text = FormatUtils.formatTextPolicyResults("test_policy", results); + assertThat(text).contains("Policy Invariant Verification for 'test_policy':"); + assertThat(text).contains("✓ Invariant 'inv_1': VERIFIED"); + assertThat(text).contains("✗ Invariant 'inv_2': VIOLATED"); + } + + @Test + public void formatJsonPolicyResults_structuredJson() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + + ImmutableMap results = ImmutableMap.of("inv_1", result); + + String json = FormatUtils.formatJsonPolicyResults("my_policy", results); + assertThat(json).startsWith("{\n"); + assertThat(json).contains("\"policyName\": \"my_policy\""); + assertThat(json).contains("\"id\": \"inv_1\""); + assertThat(json).contains("\"status\": \"VERIFIED\""); + assertThat(json).endsWith("}"); + } + + @Test + public void celVerifierTool_verifyPolicy_success() throws Exception { + File policyFile = tempFolder.newFile("test_policy.yaml"); + String yamlContent = + "name: test_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: port_check\n" + + " assert:\n" + + " - port == 80 || port != 80\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + String output = + executeToolWithOutput( + "verify-policy", + "--file", + policyFile.getAbsolutePath(), + "--var", + "port:int", + "-fmt", + "json"); + + assertThat(output).contains("\"policyName\": \"test_policy.yaml\""); + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_verifyPolicy_violated() throws Exception { + File policyFile = tempFolder.newFile("violated_policy.yaml"); + String yamlContent = + "name: violated_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: invalid_check\n" + + " assert:\n" + + " - port > 1024\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", policyFile.getAbsolutePath(), "--var", "port:int"); + + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VIOLATED); + } + + @Test + public void celVerifierTool_verifyPolicy_multipleInvariants_oneViolated() throws Exception { + File policyFile = tempFolder.newFile("multi_invariant_policy.yaml"); + String yamlContent = + "name: multi_invariant_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: valid_check\n" + + " assert:\n" + + " - port == 80 || port != 80\n" + + " - id: invalid_check\n" + + " assert:\n" + + " - port > 1024\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", policyFile.getAbsolutePath(), "--var", "port:int"); + + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VIOLATED); + } + + @Test + public void celVerifierTool_verifyPolicy_multipleInvariants_allVerified() throws Exception { + File policyFile = tempFolder.newFile("multi_verified_policy.yaml"); + String yamlContent = + "name: multi_verified_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: check_1\n" + + " assert:\n" + + " - port == 80 || port != 80\n" + + " - id: check_2\n" + + " assert:\n" + + " - port > 0 || port <= 0\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", policyFile.getAbsolutePath(), "--var", "port:int"); + + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VERIFIED); + } + + @Test + public void formatUtils_jsonResult() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + String json = FormatUtils.formatJsonResult(result); + assertThat(json).contains("\"status\": \"VERIFIED\""); + assertThat(json).contains("satisfiable"); + } + + @Test + public void celVerifierTool_checkSat_verified() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("check-sat", "--expr", "x > 0", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VERIFIED); + } + + @Test + public void celVerifierTool_checkValid_violated() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("check-valid", "--expr", "x > 0", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VIOLATED); + } + + @Test + public void celVerifierTool_verifyEquiv_verified() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-equiv", "--expr1", "x > 10", "--expr2", "10 < x", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VERIFIED); + } + + @Test + public void celVerifierTool_checkSat_compilationError() { + String output = + executeToolWithOutput("check-sat", "--expr", "invalid + + syntax", "--var", "x:int"); + assertThat(output).contains("Compilation error"); + } + + @Test + public void celVerifierTool_checkValid_withUnknownOption_violated() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("check-valid", "--expr", "x == x", "--var", "x:int", "-u", "x"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VIOLATED); + } + + @Test + public void celVerifierTool_checkValid_inconclusive() { + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("check-valid", "--expr", "int('123') == 123"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_INCONCLUSIVE); + } + + @Test + public void celVerifierTool_verifyPolicy_inconclusive() throws Exception { + File policyFile = tempFolder.newFile("inconclusive_policy.yaml"); + String yamlContent = + "name: inconclusive_policy\n" + + "rule:\n" + + " match:\n" + + " - condition: port == 80\n" + + " output: 'true'\n" + + " - output: 'false'\n" + + "verification:\n" + + " invariants:\n" + + " - id: approx_check\n" + + " assert:\n" + + " - int('123') == 123\n"; + Files.write(policyFile.toPath(), yamlContent.getBytes(StandardCharsets.UTF_8)); + + int exitCode = + new CommandLine(new CelVerifierTool()) + .execute("verify-policy", "--file", policyFile.getAbsolutePath(), "--var", "port:int"); + + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_INCONCLUSIVE); + } + + @Test + public void celVerifierTool_invalidOutputFormat_defaultsToText() { + String output = + executeToolWithOutput( + "check-sat", "--expr", "x > 0", "--var", "x:int", "-fmt", "invalid_fmt"); + assertThat(output).contains("[VERIFIED]"); + } + + @Test + public void formatTextPolicyResults_inconclusive() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult res = + CelVerifierToolCore.checkValid("int('123') == 123", ImmutableMap.of(), options); + + String text = FormatUtils.formatTextPolicyResults("test_policy", ImmutableMap.of("inv_1", res)); + assertThat(text).contains("Invariant 'inv_1': INCONCLUSIVE"); + } + + @Test + public void formatJson_escapesSpecialCharacters() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + CelVerificationResult res = + CelVerifierToolCore.checkValid("int('123') == 123", ImmutableMap.of(), options); + String json = + FormatUtils.formatJsonPolicyResults( + "policy_with_\"quote\"\nand_newline", ImmutableMap.of("inv\ttab", res)); + assertThat(json).contains("policy_with_\\\"quote\\\"\\nand_newline"); + assertThat(json).contains("inv\\ttab"); + } + + @Test + public void celVerifierTool_version() { + int exitCode = new CommandLine(new CelVerifierTool()).execute("--version"); + assertThat(exitCode).isEqualTo(0); + } +} diff --git a/verifier/src/test/java/dev/cel/verifier/tools/FormatUtilsTest.java b/verifier/src/test/java/dev/cel/verifier/tools/FormatUtilsTest.java new file mode 100644 index 000000000..1ab1cbc8a --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/FormatUtilsTest.java @@ -0,0 +1,118 @@ +// 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.tools; + +import static com.google.common.truth.Truth.assertThat; + +import com.google.common.collect.ImmutableMap; +import dev.cel.common.types.SimpleType; +import dev.cel.verifier.CelVerificationResult; +import org.junit.Before; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.JUnit4; + +@RunWith(JUnit4.class) +public final class FormatUtilsTest { + + @Before + public void setUp() { + System.setProperty("z3.skipLibraryLoad", "true"); + } + + @Test + public void formatJsonResult_verified() throws Exception { + VerificationOptions options = VerificationOptions.builder().build(); + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + + String json = FormatUtils.formatJsonResult(result); + + assertThat(json) + .isEqualTo( + "{\n" + + " \"status\": \"VERIFIED\",\n" + + " \"message\": \"Condition is satisfiable. (The expression is satisfiable" + + " unconditionally, regardless of input state)\"\n" + + "}"); + } + + @Test + public void formatJsonResult_violated() throws Exception { + VerificationOptions options = VerificationOptions.builder().build(); + CelVerificationResult result = + CelVerifierToolCore.checkValid("x > 0", ImmutableMap.of("x", SimpleType.INT), options); + + String json = FormatUtils.formatJsonResult(result); + + assertThat(json) + .startsWith( + "{\n \"status\": \"VIOLATED\",\n \"message\": \"Condition is not always true."); + assertThat(json).endsWith("\"\n}"); + } + + @Test + public void formatJsonPolicyResults_multipleInvariants() throws Exception { + VerificationOptions options = VerificationOptions.builder().build(); + CelVerificationResult verified = + CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + CelVerificationResult inconclusive = + CelVerifierToolCore.checkValid("int('123') == 123", ImmutableMap.of(), options); + ImmutableMap results = + ImmutableMap.of("inv_1", verified, "inv_2", inconclusive); + + String json = FormatUtils.formatJsonPolicyResults("my_policy", results); + + assertThat(json).startsWith("{\n \"policyName\": \"my_policy\",\n \"invariants\": [\n"); + assertThat(json).contains(" {\n \"id\": \"inv_1\",\n \"status\": \"VERIFIED\""); + assertThat(json).contains(" },\n {\n \"id\": \"inv_2\","); + assertThat(json) + .contains(" {\n \"id\": \"inv_2\",\n \"status\": \"INCONCLUSIVE\""); + assertThat(json).endsWith(" }\n ]\n}"); + } + + @Test + public void formatTextResults_verified() throws Exception { + VerificationOptions options = VerificationOptions.builder().build(); + CelVerificationResult result = + CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + + String text = FormatUtils.formatTextResult(result); + + assertThat(text).contains("[VERIFIED]"); + } + + @Test + public void formatTextPolicyResults_inconclusive() throws Exception { + VerificationOptions options = VerificationOptions.builder().build(); + CelVerificationResult result = + CelVerifierToolCore.checkValid("int('123') == 123", ImmutableMap.of(), options); + ImmutableMap results = ImmutableMap.of("inv_1", result); + + String text = FormatUtils.formatTextPolicyResults("test_policy", results); + + assertThat(text).contains("Policy Invariant Verification for 'test_policy':"); + assertThat(text).contains("Invariant 'inv_1': INCONCLUSIVE"); + } + + @Test + public void escapeJson_escapesControlCharactersAndQuotes() { + String input = "Hello \"world\"\nLine 2\t\u0000\u001b"; + + String escaped = FormatUtils.escapeJson(input); + + assertThat(escaped).isEqualTo("Hello \\\"world\\\"\\nLine 2\\t\\u0000\\u001b"); + } +} diff --git a/verifier/src/test/java/dev/cel/verifier/tools/VerificationOptionsTest.java b/verifier/src/test/java/dev/cel/verifier/tools/VerificationOptionsTest.java new file mode 100644 index 000000000..28aac751a --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/VerificationOptionsTest.java @@ -0,0 +1,103 @@ +// 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.tools; + +import static com.google.common.truth.Truth.assertThat; +import static org.junit.Assert.assertThrows; + +import com.google.common.collect.ImmutableList; +import com.google.common.collect.ImmutableMap; +import dev.cel.common.types.CelType; +import dev.cel.common.types.SimpleType; +import dev.cel.verifier.tools.VerificationOptions.OutputFormat; +import java.time.Duration; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.JUnit4; + +@RunWith(JUnit4.class) +public final class VerificationOptionsTest { + + @Test + public void defaultOptions() { + VerificationOptions options = VerificationOptions.builder().build(); + + assertThat(options.getTimeout()).isEqualTo(VerificationOptions.DEFAULT_TIMEOUT); + assertThat(options.getComprehensionUnrollLimit()) + .isEqualTo(VerificationOptions.DEFAULT_COMPREHENSION_UNROLL_LIMIT); + assertThat(options.getUnknownIdentifiers()).isEmpty(); + assertThat(options.getOutputFormat()).isEqualTo(VerificationOptions.DEFAULT_OUTPUT_FORMAT); + } + + @Test + public void customOptions_allFieldsSet() { + VerificationOptions options = + VerificationOptions.builder() + .setTimeout(Duration.ofSeconds(25)) + .setComprehensionUnrollLimit(12) + .setUnknownIdentifiers(ImmutableList.of("req.auth", "req.headers")) + .setOutputFormat(OutputFormat.JSON) + .build(); + + assertThat(options.getTimeout()).isEqualTo(Duration.ofSeconds(25)); + assertThat(options.getComprehensionUnrollLimit()).isEqualTo(12); + assertThat(options.getUnknownIdentifiers()) + .containsExactly("req.auth", "req.headers") + .inOrder(); + assertThat(options.getOutputFormat()).isEqualTo(OutputFormat.JSON); + } + + @Test + public void setTimeout_null_throwsException() { + VerificationOptions.Builder builder = VerificationOptions.builder(); + assertThrows(NullPointerException.class, () -> builder.setTimeout(null)); + } + + @Test + public void setComprehensionUnrollLimit_negative_throwsException() { + VerificationOptions.Builder builder = VerificationOptions.builder(); + assertThrows(IllegalArgumentException.class, () -> builder.setComprehensionUnrollLimit(-1)); + } + + @Test + public void setOutputFormat_null_throwsException() { + VerificationOptions.Builder builder = VerificationOptions.builder(); + assertThrows(NullPointerException.class, () -> builder.setOutputFormat(null)); + } + + @Test + public void parseVariables_validSpecs() { + ImmutableMap vars = + VerificationOptions.parseVariables(ImmutableList.of("x:int", "name:string", "flag:bool")); + + assertThat(vars) + .containsExactly( + "x", SimpleType.INT, + "name", SimpleType.STRING, + "flag", SimpleType.BOOL); + } + + @Test + public void parseVariables_nullOrEmpty_returnsEmptyMap() { + assertThat(VerificationOptions.parseVariables(null)).isEmpty(); + assertThat(VerificationOptions.parseVariables(ImmutableList.of())).isEmpty(); + } + + @Test + public void parseVariables_invalidSpec_throwsException() { + ImmutableList specs = ImmutableList.of("invalid_spec_without_colon"); + assertThrows(IllegalArgumentException.class, () -> VerificationOptions.parseVariables(specs)); + } +} diff --git a/verifier/tools/BUILD.bazel b/verifier/tools/BUILD.bazel new file mode 100644 index 000000000..a547c15b2 --- /dev/null +++ b/verifier/tools/BUILD.bazel @@ -0,0 +1,19 @@ +package( + default_applicable_licenses = ["//:license"], + default_visibility = ["//verifier:verifier_internal"], +) + +alias( + name = "tools", + actual = "//verifier/src/main/java/dev/cel/verifier/tools:tools_lib", +) + +alias( + name = "tools_lib", + actual = "//verifier/src/main/java/dev/cel/verifier/tools:tools_lib", +) + +alias( + name = "cel_verifier_tool", + actual = "//verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool", +) diff --git a/verifier/tools/README.md b/verifier/tools/README.md new file mode 100644 index 000000000..398cbad74 --- /dev/null +++ b/verifier/tools/README.md @@ -0,0 +1,191 @@ +# CEL Java Verifier CLI & Interactive REPL Tool + +The CEL Java Verifier comes with a command-line tool (`cel-verifier`) and an +interactive REPL shell for testing satisfiability, validity, equivalence, +and policy invariants without writing Java code. + +## Running the CLI Tool + +### Running via Bazel + +```bash +# Run CLI verification commands +bazel run //verifier/tools:cel_verifier_tool -- \ + check-sat \ + --expr "role == 'editor' && port > 1024" \ + --var "role:string" \ + --var "port:int" + +# Run with JSON output format for CI/CD integrations +bazel run //verifier/tools:cel_verifier_tool -- \ + check-sat \ + --expr "role == 'editor'" \ + --var "role:string" \ + --output_format=json + +# Launch interactive REPL shell +bazel run //verifier/tools:cel_verifier_tool -- repl +``` + +### Running via Maven Central + +> **Note:** Executable binaries and Maven packages (`dev.cel:cel-verifier`) +> will be published to Maven Central in an upcoming release. + +## CLI Commands + +* `check-sat --expr "..."`: Verifies satisfiability of an expression and + prints witness inputs if satisfiable. +* `check-valid --expr "..."`: Proves validity (`isAlwaysTrue`) and prints + a counterexample if invalid. +* `verify-equiv --expr1 "..." --expr2 "..."`: Proves logical equivalence + between two CEL expressions. +* `verify-policy --file policy.yaml`: Verifies policy invariants defined + in a YAML policy file. +* `repl`: Enters interactive verification shell mode. + +## Command Options + +The verification commands (`check-sat`, `check-valid`, `verify-equiv`, +`verify-policy`) accept the following options: + +### Variable Declarations (`--var`, `-v`) + +Declare variables in `name:type` format. Multiple variables can be declared by +repeating the `--var` option. + +Supported types: + +* Primitive types: `int`, `uint`, `string`, `bool`, `double`, `bytes`, `dyn` +* List types: `list` (e.g., `--var "tags:list"`) +* Map types: `map` (e.g., `--var "scores:map"`) + +Examples: +```bash +--var "role:string" --var "port:int" --var "tags:list" +``` + +### Unknown Identifiers (`--unknown`, `-u`) + +Permit specific identifiers or attributes (e.g., `request.headers`) to +evaluate to `Unknown` during verification: + +```bash +--unknown "request.headers" --unknown "auth.credentials" +``` + +### Solver Timeout (`--timeout`) + +Set maximum Z3 SMT solver timeout in seconds (default: `10`): + +```bash +--timeout 15 +``` + +### Comprehension Unroll Limit (`--unroll-limit`) + +Set bounded unroll limit for comprehensions and loop macros like `.all()` and +`.exists()` (default: `5`): + +```bash +--unroll-limit 10 +``` + +### Output Format (`--output_format`, `-fmt`) + +Set CLI output format (`TEXT` or `JSON`, default: `TEXT`): + +```bash +--output_format json +``` + +## Exit Codes + +* `0`: Verification succeeded / condition verified. +* `1`: Violation or counterexample found. +* `2`: Inconclusive result (solver unknown or timeout). +* `3`: Error (syntax compilation error, missing file, or execution error). + +## Interactive REPL Shell + +The REPL shell provides an interactive, stateful environment to execute CEL +formal verification queries without re-declaring variables or re-running CLI +parameters for every query. + +### Launching the REPL + +```bash +bazel run //verifier/tools:cel_verifier_tool -- repl +``` + +### REPL Commands + +| Command | Description | Example | +|---|---|---| +| `:var ` | Declare a variable in session state | `:var role string` | +| `:unknown ` | Mark identifier as Unknown | `:unknown request.headers` | +| `:timeout ` | Set Z3 solver timeout in seconds (default: 10s) | `:timeout 5` | +| `:unroll ` | Set comprehension unroll limit (default: 5) | `:unroll 3` | +| `:vars` | Display declared session variables & config | `:vars` | +| `:clear` | Reset session state (clears variables & unknowns) | `:clear` | +| `:help [cmd]` | Display built-in help or command details | `:help var` | +| `:quit` / `:exit` | Exit the interactive REPL shell | `:quit` | + +### Verification Queries in REPL + +* **Satisfiability (`sat ` or ``):** Checks if the expression + can evaluate to `true` for any assignment of session variables. Outputs + satisfying witness inputs if satisfiable. +* **Validity (`valid `):** Proves whether the expression evaluates + to `true` for ALL possible variable assignments. Outputs a counterexample + if invalid. +* **Equivalence (`equiv <=> `):** Proves whether two + expressions are logically identical across all inputs. Outputs a + counterexample if not equivalent. + +### Example REPL Session + +```text +============================================================ + CEL Verification REPL + Type :help for commands, :quit to exit. +============================================================ +cel-verifier> :var port int +Variable declared: port : int + +cel-verifier> sat role == 'admin' && port > 1024 + +cel-verifier> :var role string +Variable declared: role : string + +cel-verifier> sat role == 'admin' && port > 1024 +[VERIFIED] Condition is satisfiable. Satisfying input: + role = "admin" + port = 1025 + +cel-verifier> valid port > 0 || port <= 0 +[VERIFIED] + +cel-verifier> valid port > 1024 +[VIOLATED] Condition is violated. Counterexample input: + port = 0 + +cel-verifier> equiv port > 10 <=> 10 < port +[VERIFIED] + +cel-verifier> :vars +--- Session State --- +Timeout: 10s | Unroll limit: 5 +Unknowns: none +Variables (2): + role : string + port : int + +cel-verifier> :quit +Goodbye! +``` + +> **Note:** Inline help is built into the REPL shell. Type `:help` or +> `:help ` (e.g. `:help var`, `:help equiv`) at any prompt for +> detailed usage instructions and examples. +