Skip to content

Commit 3cb4b50

Browse files
maskri17copybara-github
maskri17
authored and
copybara-github
committed
Introduce cel_verifier_test Bazel macro for CEL verification.
PiperOrigin-RevId: 977944120
1 parent d88ea56 commit 3cb4b50

5 files changed

Lines changed: 273 additions & 0 deletions

File tree

‎verifier/tools/BUILD.bazel‎

Lines changed: 62 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,13 @@
1+
load("@bazel_skylib//:bzl_library.bzl", "bzl_library")
2+
load(":cel_verifier.bzl", "cel_verifier_test")
3+
14
package(
25
default_applicable_licenses = ["//:license"],
36
default_visibility = ["//verifier:verifier_internal"],
47
)
58

9+
exports_files(["run_verifier.sh"])
10+
611
alias(
712
name = "tools",
813
actual = "//verifier/src/main/java/dev/cel/verifier/tools:tools_lib",
@@ -17,3 +22,60 @@ alias(
1722
name = "cel_verifier_tool",
1823
actual = "//verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool",
1924
)
25+
26+
cel_verifier_test(
27+
name = "test_sat_simple_test",
28+
command = "check-sat",
29+
expected_status = [
30+
"VERIFIED",
31+
"INCONCLUSIVE",
32+
], # Pass if verified OR inconclusive
33+
expression = "x > 10",
34+
variables = {"x": "int"},
35+
)
36+
37+
cel_verifier_test(
38+
name = "test_sat_unsatisfiable_test",
39+
command = "check-sat",
40+
expected_status = ["VIOLATED"],
41+
expression = "x > 10 && x < 5",
42+
variables = {"x": "int"},
43+
)
44+
45+
cel_verifier_test(
46+
name = "test_equiv_simple_test",
47+
command = "verify-equiv",
48+
expression = "x > 10",
49+
expression_b = "10 < x",
50+
variables = {"x": "int"},
51+
)
52+
53+
cel_verifier_test(
54+
name = "test_policy_simple_test",
55+
command = "verify-policy",
56+
policy_file = "testdata/simple_policy.yaml",
57+
variables = {"role": "string"},
58+
)
59+
60+
cel_verifier_test(
61+
name = "test_equiv_negative_test",
62+
command = "verify-equiv",
63+
expected_status = ["VIOLATED"],
64+
expression = "x > 10",
65+
expression_b = "x < 5",
66+
variables = {"x": "int"},
67+
)
68+
69+
cel_verifier_test(
70+
name = "test_policy_violated_test",
71+
command = "verify-policy",
72+
expected_status = ["VIOLATED"],
73+
policy_file = "testdata/violated_policy.yaml",
74+
variables = {"role": "string"},
75+
)
76+
77+
bzl_library(
78+
name = "cel_verifier_bzl",
79+
srcs = ["cel_verifier.bzl"],
80+
visibility = ["//visibility:private"],
81+
)

‎verifier/tools/cel_verifier.bzl‎

Lines changed: 154 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
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+
"""Macros for CEL Formal Verifier."""
16+
17+
load("@rules_shell//shell:sh_test.bzl", "sh_test")
18+
load("@bazel_skylib//lib:shell.bzl", "shell")
19+
20+
# Mapping of friendly status names to CelVerifierTool exit codes
21+
_STATUS_TO_EXIT_CODE = {
22+
"VERIFIED": "0",
23+
"VIOLATED": "1",
24+
"INCONCLUSIVE": "2",
25+
"ERROR": "3",
26+
}
27+
28+
def _make_verifier_args(
29+
command,
30+
expression = None,
31+
expression_b = None,
32+
policy_file = None,
33+
variables = {},
34+
unknowns = [],
35+
timeout = 10,
36+
unroll_limit = 5):
37+
args = []
38+
srcs = []
39+
40+
if command not in ["check-sat", "check-valid", "verify-equiv", "verify-policy"]:
41+
fail("Unsupported command: " + command)
42+
43+
args.append(command)
44+
45+
if command in ["check-sat", "check-valid"]:
46+
if not expression:
47+
fail("expression is required for " + command)
48+
args.append("--expr")
49+
args.append(expression)
50+
elif command == "verify-equiv":
51+
if not expression or not expression_b:
52+
fail("expression and expression_b are required for verify-equiv")
53+
args.append("--expr1")
54+
args.append(expression)
55+
args.append("--expr2")
56+
args.append(expression_b)
57+
elif command == "verify-policy":
58+
if not policy_file:
59+
fail("policy_file is required for verify-policy")
60+
args.append("--file")
61+
args.append("$(rootpath %s)" % policy_file)
62+
srcs.append(policy_file)
63+
64+
for var_name, var_type in variables.items():
65+
args.append("--var")
66+
args.append("%s:%s" % (var_name, var_type))
67+
68+
for unknown in unknowns:
69+
args.append("--unknown")
70+
args.append(unknown)
71+
72+
args.append("--timeout")
73+
args.append(str(timeout))
74+
75+
args.append("--unroll-limit")
76+
args.append(str(unroll_limit))
77+
78+
args.append("--output_format")
79+
args.append("TEXT")
80+
81+
return args, srcs
82+
83+
def cel_verifier_test(
84+
name,
85+
command,
86+
expression = None,
87+
expression_b = None,
88+
policy_file = None,
89+
variables = {},
90+
unknowns = [],
91+
timeout = 10,
92+
unroll_limit = 5,
93+
expected_status = ["VERIFIED"],
94+
**kwargs):
95+
"""Verifies a CEL expression or policy via a test rule.
96+
97+
See //verifier/tools/README.md for more details on CLI commands and options.
98+
99+
Args:
100+
name: str name for the test
101+
command: str verification command. Supported commands:
102+
- 'check-sat': Verify satisfiability of a CEL expression & generate witness model.
103+
- 'check-valid': Verify validity (isAlwaysTrue) of a CEL expression & generate counterexample.
104+
- 'verify-equiv': Prove logical equivalence between two CEL expressions.
105+
- 'verify-policy': Verify policy invariants defined in a YAML policy file.
106+
expression: str CEL expression to verify (required for check-sat, check-valid, verify-equiv)
107+
expression_b: str second CEL expression for equivalence check (required for verify-equiv)
108+
policy_file: label of a YAML policy file to verify (required for verify-policy)
109+
variables: dict of var_name -> type_string (e.g., {"port": "int"})
110+
unknowns: list of str unknown identifiers
111+
timeout: int solver timeout in seconds (default 10)
112+
unroll_limit: int comprehension unroll limit (default 5)
113+
expected_status: list of str expected verification statuses (default ["VERIFIED"]).
114+
Supported statuses: 'VERIFIED', 'VIOLATED', 'INCONCLUSIVE', 'ERROR'.
115+
**kwargs: other standard Bazel attributes
116+
"""
117+
118+
args, srcs = _make_verifier_args(
119+
command = command,
120+
expression = expression,
121+
expression_b = expression_b,
122+
policy_file = policy_file,
123+
variables = variables,
124+
unknowns = unknowns,
125+
timeout = timeout,
126+
unroll_limit = unroll_limit,
127+
)
128+
129+
tags = kwargs.pop("tags", [])
130+
if "nomsan" not in tags:
131+
tags = tags + ["nomsan"]
132+
133+
allowed_codes = []
134+
for status in expected_status:
135+
if status not in _STATUS_TO_EXIT_CODE:
136+
fail("Unsupported status in expected_status: " + status)
137+
allowed_codes.append(_STATUS_TO_EXIT_CODE[status])
138+
139+
allowed_codes_str = ",".join(allowed_codes)
140+
141+
env = kwargs.pop("env", {})
142+
env["ALLOWED_EXIT_CODES"] = allowed_codes_str
143+
144+
sh_test(
145+
name = name,
146+
srcs = ["//verifier/tools:run_verifier.sh"],
147+
args = [shell.quote("$(rootpath //verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool)")] + [shell.quote(a) for a in args],
148+
data = [
149+
"//verifier/src/main/java/dev/cel/verifier/tools:cel_verifier_tool",
150+
] + srcs,
151+
tags = tags,
152+
env = env,
153+
**kwargs
154+
)

‎verifier/tools/run_verifier.sh‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
#!/bin/bash
2+
# Path: //third_party/java/cel/verifier/tools/run_verifier.sh
3+
#
4+
# This script is used by the cel_verifier_test macro to invoke the
5+
# underlying Java binary (CelVerifierTool) with the arguments passed to the macro.
6+
# It uses 'find' to locate the binary in the runfiles directory, which works
7+
# in both Google3 and Bazel environments.
8+
9+
die() {
10+
echo "ERROR: $*" >&2
11+
exit 1
12+
}
13+
14+
if [ -z "$1" ]; then
15+
die "Verifier binary path not provided as first argument."
16+
fi
17+
18+
VERIFIER_BINARY="$1"
19+
shift
20+
21+
# Execute the verifier binary with all passed arguments.
22+
"$VERIFIER_BINARY" "$@"
23+
ACTUAL_EXIT_CODE=$?
24+
25+
# Default to expecting 0 (VERIFIED) if env is not set
26+
ALLOWED_CODES=${ALLOWED_EXIT_CODES:-"0"}
27+
28+
# Check if the actual exit code is in the allowed list
29+
if [[ ",$ALLOWED_CODES," =~ ",$ACTUAL_EXIT_CODE," ]]; then
30+
echo "Verification finished with status code $ACTUAL_EXIT_CODE (Allowed: $ALLOWED_CODES)"
31+
exit 0
32+
else
33+
echo "ERROR: Verification finished with unexpected status code $ACTUAL_EXIT_CODE (Allowed: $ALLOWED_CODES)" >&2
34+
exit 1
35+
fi

‎verifier/tools/testdata/simple_policy.yaml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
name: simple_policy
2+
rule:
3+
match:
4+
- condition: role == 'admin'
5+
output: 'true'
6+
- output: 'false'
7+
verification:
8+
invariants:
9+
- id: admin_always_true
10+
assume: role == 'admin'
11+
assert: rule.result == true

‎verifier/tools/testdata/violated_policy.yaml‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
name: violated_policy
2+
rule:
3+
match:
4+
- condition: role == 'admin'
5+
output: 'true'
6+
- output: 'false'
7+
verification:
8+
invariants:
9+
- id: viewer_always_true
10+
assume: role == 'viewer'
11+
assert: rule.result == true

0 commit comments

Comments
 (0)