Skip to content

Commit 6804ce7

Browse files
l46kokcopybara-github
authored andcommitted
Add a canonicalization pass to CEL verifier
PiperOrigin-RevId: 957797112
1 parent 989c8c5 commit 6804ce7

39 files changed

Lines changed: 4732 additions & 216 deletions

BUILD.bazel

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,14 @@ java_library(
9595
],
9696
)
9797

98+
java_library(
99+
name = "java_jline",
100+
exports = [
101+
"@maven//:org_jline_jline_reader",
102+
"@maven//:org_jline_jline_terminal",
103+
],
104+
)
105+
98106
default_java_toolchain(
99107
name = "repository_default_toolchain",
100108
configuration = DEFAULT_TOOLCHAIN_CONFIGURATION,

MODULE.bazel

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -95,6 +95,8 @@ maven.install(
9595
"info.picocli:picocli:4.7.7",
9696
"org.antlr:antlr4-runtime:4.13.2",
9797
"org.freemarker:freemarker:2.3.34",
98+
"org.jline:jline-reader:3.26.1",
99+
"org.jline:jline-terminal:3.26.1",
98100
"org.jspecify:jspecify:1.0.0",
99101
"org.threeten:threeten-extra:1.8.0",
100102
"org.yaml:snakeyaml:2.5",

verifier/BUILD.bazel

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -41,6 +41,13 @@ java_library(
4141
exports = ["//verifier/src/main/java/dev/cel/verifier:verifier_factory"],
4242
)
4343

44+
java_library(
45+
name = "numeric_bounds",
46+
compatible_with = [],
47+
visibility = [":verifier_internal"],
48+
exports = ["//verifier/src/main/java/dev/cel/verifier:numeric_bounds"],
49+
)
50+
4451
java_library(
4552
name = "type_system",
4653
compatible_with = [],
@@ -54,3 +61,10 @@ java_library(
5461
visibility = [":verifier_internal"],
5562
exports = ["//verifier/src/main/java/dev/cel/verifier:z3_impl"],
5663
)
64+
65+
java_library(
66+
name = "canonicalization_optimizer",
67+
compatible_with = [],
68+
visibility = [":verifier_internal"],
69+
exports = ["//verifier/src/main/java/dev/cel/verifier:canonicalization_optimizer"],
70+
)

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/BUILD.bazel

Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,12 @@ java_library(
3535
deps = [
3636
":verifier",
3737
":z3_impl",
38+
"//bundle:cel",
39+
"//checker:checker_builder",
40+
"//compiler",
41+
"//compiler:compiler_builder",
42+
"//parser:parser_builder",
43+
"//runtime",
3844
],
3945
)
4046

@@ -91,20 +97,57 @@ java_library(
9197
],
9298
)
9399

100+
java_library(
101+
name = "numeric_bounds",
102+
srcs = ["CelNumericBounds.java"],
103+
compatible_with = [],
104+
tags = [
105+
],
106+
deps = [
107+
"//:auto_value",
108+
"//common/annotations",
109+
"@maven//:com_google_guava_guava",
110+
],
111+
)
112+
94113
java_library(
95114
name = "type_system",
96115
srcs = ["CelZ3TypeSystem.java"],
97116
compatible_with = [],
98117
tags = [
99118
],
100119
deps = [
120+
":numeric_bounds",
101121
"//common/internal:proto_time_utils",
102122
"@maven//:com_google_errorprone_error_prone_annotations",
103123
"@maven//:com_google_guava_guava",
104124
"@maven//:tools_aqua_z3_turnkey",
105125
],
106126
)
107127

128+
java_library(
129+
name = "canonicalization_optimizer",
130+
srcs = ["CanonicalizationOptimizer.java"],
131+
tags = [
132+
],
133+
deps = [
134+
"//:auto_value",
135+
"//bundle:cel",
136+
"//common:cel_ast",
137+
"//common:mutable_ast",
138+
"//common:mutable_source",
139+
"//common:operator",
140+
"//common/ast",
141+
"//common/ast:mutable_expr",
142+
"//common/navigation:common",
143+
"//common/navigation:mutable_navigation",
144+
"//common/values:cel_byte_string",
145+
"//optimizer:ast_optimizer",
146+
"//optimizer:mutable_ast",
147+
"@maven//:com_google_guava_guava",
148+
],
149+
)
150+
108151
java_library(
109152
name = "z3_impl",
110153
srcs = [
@@ -121,9 +164,12 @@ java_library(
121164
tags = [
122165
],
123166
deps = [
167+
":canonicalization_optimizer",
168+
":numeric_bounds",
124169
":type_system",
125170
":verifier",
126171
"//:auto_value",
172+
"//bundle:cel",
127173
"//common:cel_ast",
128174
"//common:compiler_common",
129175
"//common:operator",
@@ -132,6 +178,9 @@ java_library(
132178
"//common/types",
133179
"//common/types:cel_types",
134180
"//common/types:type_providers",
181+
"//optimizer",
182+
"//optimizer:optimization_exception",
183+
"//optimizer:optimizer_builder",
135184
"//verifier/axioms",
136185
"@maven//:com_google_errorprone_error_prone_annotations",
137186
"@maven//:com_google_guava_guava",

0 commit comments

Comments
 (0)