From de04acf0f55a99ea4e7dc8a3d2b9260f8e2603c1 Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Wed, 29 Jul 2026 21:35:11 -0700 Subject: [PATCH] Add CLI for Verifier PiperOrigin-RevId: 956259271 --- verifier/README.md | 4 + .../cel/verifier/CelAstToZ3Translator.java | 82 ++- .../CelZ3CounterexampleGenerator.java | 2 + .../dev/cel/verifier/CelZ3TypeSystem.java | 5 + .../java/dev/cel/verifier/tools/BUILD.bazel | 77 +++ .../cel/verifier/tools/CelVerifierTool.java | 303 +++++++++ .../verifier/tools/CelVerifierToolCore.java | 161 +++++ .../dev/cel/verifier/tools/FormatUtils.java | 173 ++++++ .../verifier/tools/VerificationOptions.java | 219 +++++++ .../test/java/dev/cel/verifier/BUILD.bazel | 3 +- .../cel/verifier/CelVerifierZ3ImplTest.java | 77 +++ .../java/dev/cel/verifier/tools/BUILD.bazel | 31 + .../verifier/tools/CelVerifierToolTest.java | 587 ++++++++++++++++++ .../cel/verifier/tools/FormatUtilsTest.java | 117 ++++ .../tools/VerificationOptionsTest.java | 104 ++++ verifier/tools/BUILD.bazel | 19 + verifier/tools/README.md | 107 ++++ 17 files changed, 2053 insertions(+), 18 deletions(-) create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/FormatUtils.java create mode 100644 verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java create mode 100644 verifier/src/test/java/dev/cel/verifier/tools/BUILD.bazel create mode 100644 verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java create mode 100644 verifier/src/test/java/dev/cel/verifier/tools/FormatUtilsTest.java create mode 100644 verifier/src/test/java/dev/cel/verifier/tools/VerificationOptionsTest.java create mode 100644 verifier/tools/BUILD.bazel create mode 100644 verifier/tools/README.md 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/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index e3bb1bfaf..407f896a0 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -1247,9 +1247,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); @@ -1289,15 +1290,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 +1306,69 @@ 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); - boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint)); - BoolExpr outOfBounds = ctx.mkGe(idx, length); - boundsAndTypes.add(ctx.mkImplies(outOfBounds, ctx.mkEq(elem, typeSystem.mkUnknown()))); + // 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)))); + // Short-circuit DYN element types to prevent generating redundant validIndex ⇒ TRUE + // clauses. + if (!elemType.equals(SimpleType.DYN)) { + BoolExpr elemConstraint = createTypeConstraintForType(elem, elemType); + boundsAndTypes.add(ctx.mkImplies(validIndex, elemConstraint)); + } } 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); + + 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))); + // Short-circuit DYN key types to prevent generating redundant validIndex ⇒ TRUE clauses. + if (!keyType.equals(SimpleType.DYN)) { + 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 = ctx.mkNot(typeSystem.isError(mapVal)); + boundsAndTypes.add(ctx.mkImplies(validEntry, valNotError)); + // Short-circuit DYN value types to prevent generating redundant validEntry ⇒ TRUE clauses. + if (!valType.equals(SimpleType.DYN)) { + boundsAndTypes.add( + ctx.mkImplies(validEntry, createTypeConstraintForType(mapVal, valType))); + } + } + + return CelZ3TypeSystem.mkAndFlattened(ctx, boundsAndTypes); } if (type.kind() == CelKind.STRUCT) { return ctx.mkAnd( diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index 2355d36bf..f52886a42 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -127,6 +127,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 = diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index e9a1872c9..1c1435e3b 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -685,6 +685,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); 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..e4339f857 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel @@ -0,0 +1,77 @@ +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 = [ + "CelVerifierTool.java", + "CelVerifierToolCore.java", + "FormatUtils.java", + "VerificationOptions.java", + ":generate_version", + ], + tags = [ + "alt_dep=//verifier/tools", + ], + deps = [ + "//bundle:cel", + "//common:cel_ast", + "//common:compiler_common", + "//common:options", + "//common/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/CelVerifierTool.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java new file mode 100644 index 000000000..8289b9f77 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java @@ -0,0 +1,303 @@ +// 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 Tool", + subcommands = { + CelVerifierTool.CheckSatCommand.class, + CelVerifierTool.CheckValidCommand.class, + CelVerifierTool.VerifyEquivCommand.class, + CelVerifierTool.VerifyPolicyCommand.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; + } + } + + 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..89e842fb1 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java @@ -0,0 +1,161 @@ +// 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(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(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(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 CelVerifier buildVerifier(VerificationOptions options) { + CelVerifierBuilder builder = + CelVerifierFactory.newVerifier() + .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) { + 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()); + } + Cel celBundle = celBuilder.build(); + CelPolicyCompiler policyCompiler = + CelPolicyCompilerFactory.newPolicyCompiler(celBundle).build(); + CelVerifier astVerifier = buildVerifier(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..f25f6ab10 --- /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() != null && !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() != null && !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..91ec443a5 --- /dev/null +++ b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java @@ -0,0 +1,219 @@ +// 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(); + 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..de788ca5c 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 = [ @@ -53,6 +53,7 @@ java_library( "//verifier:verifier_factory", "//verifier:z3_impl", "//verifier/axioms", + "//verifier/tools", "@cel_spec//proto/cel/expr/conformance/proto3:test_all_types_java_proto", "@maven//:com_google_guava_guava", ], diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 1a41ef743..f230714b2 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -197,6 +197,80 @@ 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"); + } + + 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'"), + ; + + 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(); @@ -747,6 +821,9 @@ 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"), ; final String expr; 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/CelVerifierToolTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java new file mode 100644 index 000000000..383604aa0 --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java @@ -0,0 +1,587 @@ +// 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 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..7ed553bff --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/FormatUtilsTest.java @@ -0,0 +1,117 @@ +// 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 \"id\": \"inv_2\",\n \"status\": \"INCONCLUSIVE\""); + assertThat(json).endsWith(" ]\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..039c5eaa2 --- /dev/null +++ b/verifier/src/test/java/dev/cel/verifier/tools/VerificationOptionsTest.java @@ -0,0 +1,104 @@ +// 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() { + assertThrows(NullPointerException.class, () -> VerificationOptions.builder().setTimeout(null)); + } + + @Test + public void setComprehensionUnrollLimit_negative_throwsException() { + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.builder().setComprehensionUnrollLimit(-1)); + } + + @Test + public void setOutputFormat_null_throwsException() { + assertThrows( + NullPointerException.class, () -> VerificationOptions.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() { + assertThrows( + IllegalArgumentException.class, + () -> VerificationOptions.parseVariables(ImmutableList.of("invalid_spec_without_colon"))); + } +} 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..f2cfa2528 --- /dev/null +++ b/verifier/tools/README.md @@ -0,0 +1,107 @@ +# 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).