Skip to content

Commit aa0e58b

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Add CLI for Verifier
PiperOrigin-RevId: 956259271
1 parent ecc7a55 commit aa0e58b

13 files changed

Lines changed: 1904 additions & 1 deletion

File tree

‎verifier/README.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -433,3 +433,7 @@ What this means for verification:
433433
default unless you have a specific need and bounded inputs.
434434

435435
---
436+
437+
## Tools & CLI
438+
439+
For command-line verification and interactive execution, see the [CLI Tool documentation](tools/README.md).

‎verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel‎

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,77 @@
1+
load("@rules_java//java:defs.bzl", "java_binary", "java_library")
2+
load("//publish:cel_version.bzl", "CEL_VERSION")
3+
4+
package(
5+
default_applicable_licenses = [
6+
"//:license",
7+
],
8+
default_visibility = [
9+
"//verifier:__subpackages__",
10+
],
11+
)
12+
13+
genrule(
14+
name = "generate_version",
15+
outs = ["CelVersion.java"],
16+
cmd = """cat << 'EOF' > $@
17+
package dev.cel.verifier.tools;
18+
19+
final class CelVersion {
20+
static final String VERSION = "%s";
21+
22+
private CelVersion() {}
23+
}
24+
EOF
25+
""" % CEL_VERSION,
26+
)
27+
28+
java_library(
29+
name = "tools_lib",
30+
srcs = [
31+
"CelVerifierTool.java",
32+
"CelVerifierToolCore.java",
33+
"FormatUtils.java",
34+
"VerificationOptions.java",
35+
":generate_version",
36+
],
37+
tags = [
38+
"alt_dep=//verifier/tools",
39+
],
40+
deps = [
41+
"//bundle:cel",
42+
"//common:cel_ast",
43+
"//common:compiler_common",
44+
"//common:options",
45+
"//common/types",
46+
"//common/types:type_providers",
47+
"//compiler",
48+
"//compiler:compiler_builder",
49+
"//extensions",
50+
"//parser:macro",
51+
"//policy",
52+
"//policy:compiler",
53+
"//policy:compiler_factory",
54+
"//policy:parser",
55+
"//policy:parser_factory",
56+
"//policy:validation_exception",
57+
"//verifier",
58+
"//verifier:policy_verifier",
59+
"//verifier:policy_verifier_factory",
60+
"//verifier:verifier_factory",
61+
"@maven//:com_google_errorprone_error_prone_annotations",
62+
"@maven//:com_google_guava_guava",
63+
"@maven//:info_picocli_picocli",
64+
],
65+
)
66+
67+
java_binary(
68+
name = "cel_verifier_tool",
69+
jvm_flags = ["-Dz3.skipLibraryLoad=true"],
70+
main_class = "dev.cel.verifier.tools.CelVerifierTool",
71+
tags = [
72+
"alt_dep=//verifier/tools:cel_verifier_tool",
73+
],
74+
runtime_deps = [
75+
":tools_lib",
76+
],
77+
)

‎verifier/src/main/java/dev/cel/verifier/tools/CelVerifierTool.java‎

Lines changed: 303 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,303 @@
1+
// Copyright 2026 Google LLC
2+
//
3+
// Licensed under the Apache License, Version 2.0 (the "License");
4+
// you may not use this file except in compliance with the License.
5+
// You may obtain a copy of the License at
6+
//
7+
// https://www.apache.org/licenses/LICENSE-2.0
8+
//
9+
// Unless required by applicable law or agreed to in writing, software
10+
// distributed under the License is distributed on an "AS IS" BASIS,
11+
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
12+
// See the License for the specific language governing permissions and
13+
// limitations under the License.
14+
15+
package dev.cel.verifier.tools;
16+
17+
import com.google.common.collect.ImmutableMap;
18+
import dev.cel.common.CelValidationException;
19+
import dev.cel.common.types.CelType;
20+
import dev.cel.policy.CelPolicyValidationException;
21+
import dev.cel.verifier.CelVerificationResult;
22+
import dev.cel.verifier.CelVerificationResult.VerificationStatus;
23+
import dev.cel.verifier.tools.VerificationOptions.OutputFormat;
24+
import java.io.File;
25+
import java.io.OutputStreamWriter;
26+
import java.io.PrintWriter;
27+
import java.nio.charset.StandardCharsets;
28+
import java.nio.file.Files;
29+
import java.time.Duration;
30+
import java.util.ArrayList;
31+
import java.util.List;
32+
import java.util.Locale;
33+
import java.util.concurrent.Callable;
34+
import picocli.CommandLine;
35+
import picocli.CommandLine.Command;
36+
import picocli.CommandLine.IVersionProvider;
37+
import picocli.CommandLine.Model.CommandSpec;
38+
import picocli.CommandLine.Option;
39+
import picocli.CommandLine.Spec;
40+
41+
/** Main Picocli entrypoint for the CEL Formal Verification CLI. */
42+
@Command(
43+
name = "cel-verifier",
44+
mixinStandardHelpOptions = true,
45+
versionProvider = CelVerifierTool.VersionProvider.class,
46+
description = "CEL-Java Formal Verification CLI Tool",
47+
subcommands = {
48+
CelVerifierTool.CheckSatCommand.class,
49+
CelVerifierTool.CheckValidCommand.class,
50+
CelVerifierTool.VerifyEquivCommand.class,
51+
CelVerifierTool.VerifyPolicyCommand.class
52+
})
53+
public final class CelVerifierTool implements Runnable {
54+
55+
static final int EXIT_CODE_VERIFIED = 0;
56+
static final int EXIT_CODE_VIOLATED = 1;
57+
static final int EXIT_CODE_INCONCLUSIVE = 2;
58+
static final int EXIT_CODE_ERROR = 3;
59+
60+
static final class VersionProvider implements IVersionProvider {
61+
@Override
62+
public String[] getVersion() {
63+
return new String[] {"cel-verifier " + CelVersion.VERSION};
64+
}
65+
}
66+
67+
@Spec private CommandSpec spec;
68+
69+
@Override
70+
public void run() {
71+
spec.commandLine().usage(spec.commandLine().getOut());
72+
}
73+
74+
/** Options shared across all verification commands. */
75+
abstract static class BaseVerificationCommand implements Callable<Integer> {
76+
77+
@Spec private CommandSpec spec;
78+
79+
PrintWriter out() {
80+
return spec != null
81+
? spec.commandLine().getOut()
82+
: new PrintWriter(new OutputStreamWriter(System.out, StandardCharsets.UTF_8), true);
83+
}
84+
85+
PrintWriter err() {
86+
return spec != null
87+
? spec.commandLine().getErr()
88+
: new PrintWriter(new OutputStreamWriter(System.err, StandardCharsets.UTF_8), true);
89+
}
90+
91+
@Option(
92+
names = {"--var", "-v"},
93+
description =
94+
"Declared variable in 'name:type' format (e.g., --var role:string --var port:int)")
95+
List<String> variables = new ArrayList<>();
96+
97+
@Option(
98+
names = {"--unknown", "-u"},
99+
description =
100+
"Identifier to permit evaluating to Unknown (e.g., --unknown request.headers)")
101+
List<String> unknownIdentifiers = new ArrayList<>();
102+
103+
@Option(
104+
names = {"--timeout"},
105+
description = "Solver timeout in seconds (default: 10)")
106+
int timeoutSeconds = (int) VerificationOptions.DEFAULT_TIMEOUT.getSeconds();
107+
108+
@Option(
109+
names = {"--unroll-limit"},
110+
description = "Comprehension unroll limit for BMC (default: 5)")
111+
int comprehensionUnrollLimit = VerificationOptions.DEFAULT_COMPREHENSION_UNROLL_LIMIT;
112+
113+
@Option(
114+
names = {"--output_format", "-fmt"},
115+
description = "Output format: TEXT or JSON (default: TEXT)")
116+
String outputFormatStr = VerificationOptions.DEFAULT_OUTPUT_FORMAT.name();
117+
118+
@FunctionalInterface
119+
protected interface CommandAction {
120+
int execute(VerificationOptions options, ImmutableMap<String, CelType> vars) throws Exception;
121+
}
122+
123+
protected int executeCommand(CommandAction action) {
124+
return executeCommand("Verification error", action);
125+
}
126+
127+
protected int executeCommand(String errorPrefix, CommandAction action) {
128+
try {
129+
VerificationOptions options = getOptions();
130+
ImmutableMap<String, CelType> vars = VerificationOptions.parseVariables(variables);
131+
return action.execute(options, vars);
132+
} catch (CelValidationException e) {
133+
err().println("Compilation error:\n" + e.getMessage());
134+
return EXIT_CODE_ERROR;
135+
} catch (CelPolicyValidationException e) {
136+
err().println("Policy compilation error:\n" + e.getMessage());
137+
return EXIT_CODE_ERROR;
138+
} catch (Exception e) {
139+
err().println(errorPrefix + ": " + e.getMessage());
140+
return EXIT_CODE_ERROR;
141+
}
142+
}
143+
144+
protected VerificationOptions getOptions() {
145+
OutputFormat format = OutputFormat.TEXT;
146+
try {
147+
format = OutputFormat.valueOf(outputFormatStr.toUpperCase(Locale.US));
148+
} catch (IllegalArgumentException e) {
149+
err().println("Invalid output format '" + outputFormatStr + "'. Defaulting to TEXT.");
150+
}
151+
return VerificationOptions.builder()
152+
.setTimeout(Duration.ofSeconds(timeoutSeconds))
153+
.setComprehensionUnrollLimit(comprehensionUnrollLimit)
154+
.setUnknownIdentifiers(unknownIdentifiers)
155+
.setOutputFormat(format)
156+
.build();
157+
}
158+
159+
protected int handleSingleResult(CelVerificationResult result, OutputFormat format) {
160+
if (format == OutputFormat.JSON) {
161+
out().println(FormatUtils.formatJsonResult(result));
162+
} else {
163+
out().println(FormatUtils.formatTextResult(result));
164+
}
165+
166+
if (result.status() == VerificationStatus.VERIFIED) {
167+
return EXIT_CODE_VERIFIED;
168+
} else if (result.status() == VerificationStatus.VIOLATED) {
169+
return EXIT_CODE_VIOLATED;
170+
} else {
171+
return EXIT_CODE_INCONCLUSIVE;
172+
}
173+
}
174+
}
175+
176+
/** Base command for commands operating on a single CEL expression. */
177+
abstract static class SingleExpressionCommand extends BaseVerificationCommand {
178+
@Option(
179+
names = {"--expr", "-e"},
180+
required = true,
181+
description = "CEL expression string to verify")
182+
String expression = "";
183+
}
184+
185+
@Command(
186+
name = "check-sat",
187+
description = "Verify satisfiability of a CEL expression & generate witness model")
188+
static class CheckSatCommand extends SingleExpressionCommand {
189+
190+
@Override
191+
public Integer call() {
192+
return executeCommand(
193+
(options, vars) ->
194+
handleSingleResult(
195+
CelVerifierToolCore.checkSatisfiable(expression, vars, options),
196+
options.getOutputFormat()));
197+
}
198+
}
199+
200+
@Command(
201+
name = "check-valid",
202+
description = "Verify validity (isAlwaysTrue) of a CEL expression & generate counterexample")
203+
static class CheckValidCommand extends SingleExpressionCommand {
204+
205+
@Override
206+
public Integer call() {
207+
return executeCommand(
208+
(options, vars) ->
209+
handleSingleResult(
210+
CelVerifierToolCore.checkValid(expression, vars, options),
211+
options.getOutputFormat()));
212+
}
213+
}
214+
215+
@Command(
216+
name = "verify-equiv",
217+
description = "Prove logical equivalence between two CEL expressions")
218+
static class VerifyEquivCommand extends BaseVerificationCommand {
219+
220+
@Option(
221+
names = {"--expr1"},
222+
required = true,
223+
description = "First CEL expression")
224+
String expressionA = "";
225+
226+
@Option(
227+
names = {"--expr2"},
228+
required = true,
229+
description = "Second CEL expression")
230+
String expressionB = "";
231+
232+
@Override
233+
public Integer call() {
234+
return executeCommand(
235+
(options, vars) ->
236+
handleSingleResult(
237+
CelVerifierToolCore.verifyEquivalence(expressionA, expressionB, vars, options),
238+
options.getOutputFormat()));
239+
}
240+
}
241+
242+
@Command(
243+
name = "verify-policy",
244+
description = "Verify policy invariants defined in a YAML policy file")
245+
static class VerifyPolicyCommand extends BaseVerificationCommand {
246+
247+
@Option(
248+
names = {"--file", "-f"},
249+
required = true,
250+
description = "Path to policy YAML file")
251+
String filePath = "";
252+
253+
@Override
254+
public Integer call() {
255+
return executeCommand(
256+
"Policy verification error",
257+
(options, vars) -> {
258+
File file = new File(filePath);
259+
if (!file.exists()) {
260+
err().println("File not found: " + filePath);
261+
return EXIT_CODE_ERROR;
262+
}
263+
String yamlContent =
264+
new String(Files.readAllBytes(file.toPath()), StandardCharsets.UTF_8);
265+
266+
ImmutableMap<String, CelVerificationResult> results =
267+
CelVerifierToolCore.verifyPolicyInvariants(yamlContent, vars, options);
268+
269+
if (options.getOutputFormat() == OutputFormat.JSON) {
270+
out().println(FormatUtils.formatJsonPolicyResults(file.getName(), results));
271+
} else {
272+
out().println(FormatUtils.formatTextPolicyResults(file.getName(), results));
273+
}
274+
275+
return getPolicyExitCode(results);
276+
});
277+
}
278+
279+
private static int getPolicyExitCode(ImmutableMap<String, CelVerificationResult> results) {
280+
boolean anyViolated = false;
281+
boolean anyInconclusive = false;
282+
for (CelVerificationResult res : results.values()) {
283+
if (res.status() == VerificationStatus.VIOLATED) {
284+
anyViolated = true;
285+
} else if (res.status() == VerificationStatus.INCONCLUSIVE) {
286+
anyInconclusive = true;
287+
}
288+
}
289+
290+
if (anyViolated) {
291+
return EXIT_CODE_VIOLATED;
292+
} else if (anyInconclusive) {
293+
return EXIT_CODE_INCONCLUSIVE;
294+
}
295+
return EXIT_CODE_VERIFIED;
296+
}
297+
}
298+
299+
public static void main(String[] args) {
300+
int exitCode = new CommandLine(new CelVerifierTool()).execute(args);
301+
System.exit(exitCode);
302+
}
303+
}

0 commit comments

Comments
 (0)