Skip to content

Commit 689912b

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Refactor Canonicalization Optimizer
Granular nested classes for comparator, safety check, and NNF normalization has been introduced. No functional changes PiperOrigin-RevId: 960456441
1 parent d459cc9 commit 689912b

11 files changed

Lines changed: 814 additions & 443 deletions

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -145,6 +145,7 @@ java_library(
145145
"//optimizer:ast_optimizer",
146146
"//optimizer:mutable_ast",
147147
"@maven//:com_google_guava_guava",
148+
"@maven//:org_jspecify_jspecify",
148149
],
149150
)
150151

‎verifier/src/main/java/dev/cel/verifier/CanonicalizationOptimizer.java‎

Lines changed: 502 additions & 420 deletions
Large diffs are not rendered by default.

‎verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ private static String formatExpr(
8888
} else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) {
8989
return "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")";
9090
} else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) {
91-
return "duration(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")";
91+
return "duration('" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "s')";
9292
} else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) {
9393
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u";
9494
} else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) {

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

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -314,15 +314,21 @@ private static void printHelp(String topic, PrintStream out) {
314314
out.println("Declares a variable in the REPL session with a specific type.");
315315
out.println();
316316
out.println("Supported Types:");
317-
out.println(" - Primitive types: int, uint, string, bool, double, bytes");
318-
out.println(" - List types: list<T> (e.g., list<int>, list<string>)");
319-
out.println(" - Map types: map<K,V> (e.g., map<string,int>, map<string,string>)");
317+
out.println(" - Primitive types: int, uint, string, bool, double, bytes, dyn");
318+
out.println(" - Well-known types: timestamp, duration");
319+
out.println(" - List types: list<T> (e.g., list<int>, list<string>)");
320+
out.println(" - Map types: map<K,V> (e.g., map<string,int>, map<string,string>)");
321+
out.println(" - Optional types: optional<T> (e.g., optional<string>, optional<int>)");
322+
out.println(" - Protobuf types: coming soon");
320323
out.println();
321324
out.println("Examples:");
322325
out.println(" cel-verifier> :var role string");
323326
out.println(" cel-verifier> :var port int");
324327
out.println(" cel-verifier> :var scores map<string,int>");
325328
out.println(" cel-verifier> :var tags list<string>");
329+
out.println(" cel-verifier> :var created_at timestamp");
330+
out.println(" cel-verifier> :var timeout duration");
331+
out.println(" cel-verifier> :var opt_flag optional<bool>");
326332
break;
327333
case "unknown":
328334
out.println("Command: :unknown <identifier>");

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

Lines changed: 30 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@
2121
import dev.cel.common.types.CelType;
2222
import dev.cel.common.types.ListType;
2323
import dev.cel.common.types.MapType;
24+
import dev.cel.common.types.OptionalType;
2425
import dev.cel.common.types.SimpleType;
2526
import java.time.Duration;
2627
import java.util.ArrayList;
@@ -150,13 +151,15 @@ static CelType parseCelType(String typeStr) {
150151
Preconditions.checkNotNull(typeStr, "Type string cannot be null.");
151152
String str = typeStr.trim().toLowerCase(Locale.US);
152153

153-
if (str.startsWith("list<") && str.endsWith(">")) {
154+
if ((str.startsWith("list<") && str.endsWith(">"))
155+
|| (str.startsWith("list(") && str.endsWith(")"))) {
154156
String inner = str.substring(5, str.length() - 1).trim();
155157
CelType elemType = parseCelType(inner);
156158
return ListType.create(elemType);
157159
}
158160

159-
if (str.startsWith("map<") && str.endsWith(">")) {
161+
if ((str.startsWith("map<") && str.endsWith(">"))
162+
|| (str.startsWith("map(") && str.endsWith(")"))) {
160163
String inner = str.substring(4, str.length() - 1).trim();
161164
List<String> parts = splitGenericArgs(inner);
162165
if (parts.size() != 2) {
@@ -170,6 +173,20 @@ static CelType parseCelType(String typeStr) {
170173
return MapType.create(keyType, valueType);
171174
}
172175

176+
if ((str.startsWith("optional<") && str.endsWith(">"))
177+
|| (str.startsWith("optional(") && str.endsWith(")"))) {
178+
String inner = str.substring(9, str.length() - 1).trim();
179+
CelType elemType = parseCelType(inner);
180+
return OptionalType.create(elemType);
181+
}
182+
183+
if ((str.startsWith("optional_type<") && str.endsWith(">"))
184+
|| (str.startsWith("optional_type(") && str.endsWith(")"))) {
185+
String inner = str.substring(14, str.length() - 1).trim();
186+
CelType elemType = parseCelType(inner);
187+
return OptionalType.create(elemType);
188+
}
189+
173190
switch (str) {
174191
case "int":
175192
return SimpleType.INT;
@@ -187,12 +204,19 @@ static CelType parseCelType(String typeStr) {
187204
return SimpleType.BYTES;
188205
case "dyn":
189206
return SimpleType.DYN;
207+
case "timestamp":
208+
case "google.protobuf.timestamp":
209+
return SimpleType.TIMESTAMP;
210+
case "duration":
211+
case "google.protobuf.duration":
212+
return SimpleType.DURATION;
190213
default:
214+
// TODO: Support protobuf message types (coming soon).
191215
throw new IllegalArgumentException(
192216
"Unsupported type for CLI variable declaration: '"
193217
+ typeStr
194-
+ "'. Supported types: int, uint, string, bool, double, bytes, dyn, list<T>, map<K,"
195-
+ " V>.");
218+
+ "'. Supported types: int, uint, string, bool, double, bytes, dyn, timestamp,"
219+
+ " duration, list<T>, map<K, V>, optional<T>.");
196220
}
197221
}
198222

@@ -202,10 +226,10 @@ private static List<String> splitGenericArgs(String inner) {
202226
StringBuilder current = new StringBuilder();
203227
for (int i = 0; i < inner.length(); i++) {
204228
char c = inner.charAt(i);
205-
if (c == '<') {
229+
if (c == '<' || c == '(') {
206230
depth++;
207231
current.append(c);
208-
} else if (c == '>') {
232+
} else if (c == '>' || c == ')') {
209233
depth--;
210234
current.append(c);
211235
} else if (c == ',' && depth == 0) {

‎verifier/src/test/java/dev/cel/verifier/CanonicalizationOptimizerTest.java‎

Lines changed: 74 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@
2727
import dev.cel.common.CelContainer;
2828
import dev.cel.common.CelMutableAst;
2929
import dev.cel.common.CelOptions;
30+
import dev.cel.common.ast.CelExpr.ExprKind.Kind;
3031
import dev.cel.common.ast.CelMutableExpr;
3132
import dev.cel.common.ast.CelMutableExpr.CelMutableCall;
3233
import dev.cel.common.types.ListType;
@@ -464,7 +465,49 @@ private enum CanonicalizationTestCase {
464465
IDENT_INEQUALITY_SYMMETRY(
465466
"dyn_b != dyn_a || dyn_d != dyn_c", "dyn_a != dyn_b || dyn_c != dyn_d"),
466467
IDENT_SAME_NAME_DIFFERENT_OPERATORS(
467-
"dyn_a != dyn_b && dyn_a == dyn_b", "dyn_a != dyn_b && dyn_a == dyn_b");
468+
"dyn_a != dyn_b && dyn_a == dyn_b", "dyn_a != dyn_b && dyn_a == dyn_b"),
469+
470+
// Comprehension Sorting & Structure Comparison (iterRange, accuInit, loopStep, iterVar2)
471+
COMPREHENSIONS_DIFFERENT_ITER_RANGE_EQUALITY(
472+
"[2, 3].all(x, x > 0) == [1, 2].all(x, x > 0)",
473+
"[1, 2].all(x, x > 0) == [2, 3].all(x, x > 0)"),
474+
COMPREHENSIONS_DIFFERENT_ITER_RANGE_AND(
475+
"[2, 3].all(x, x > 0) && [1, 2].all(x, x > 0)",
476+
"[1, 2].all(x, x > 0) && [2, 3].all(x, x > 0)"),
477+
COMPREHENSIONS_DIFFERENT_PREDICATES_AND(
478+
"[1, 2].all(x, x > 10) && [1, 2].all(x, x > 0)",
479+
"[1, 2].all(x, x > 0) && [1, 2].all(x, x > 10)"),
480+
COMPREHENSIONS_EXISTS_VS_ALL_AND(
481+
"[1, 2].all(x, x == 1) && [1, 2].exists(x, x == 1)",
482+
"[1, 2].exists(x, x == 1) && [1, 2].all(x, x == 1)"),
483+
COMPREHENSIONS_ONE_VAR_VS_TWO_VAR_AND(
484+
"string_int_map.all(k, v, v > 0) && string_int_map.all(k, k == 'a')",
485+
"string_int_map.all(k, k == \"a\") && string_int_map.all(k, v, v > 0)"),
486+
487+
// Macro Scope Coverage (filter, map, exists_one, optMap, optFlatMap)
488+
FILTER_MACRO_PREDICATE_ORDER(
489+
"int_list.filter(x, x > 10 && x > 0)", "int_list.filter(x, x > 0 && x > 10)"),
490+
MAP_MACRO_PREDICATE_ORDER(
491+
"int_list.map(x, x == 2 && x == 1)", "int_list.map(x, x == 1 && x == 2)"),
492+
EXISTS_ONE_MACRO_PREDICATE_ORDER(
493+
"int_list.exists_one(x, x > 10 && x > 0)", "int_list.exists_one(x, x > 0 && x > 10)"),
494+
OPT_MAP_MACRO_PREDICATE_ORDER(
495+
"optional.of(int_var).optMap(x, x == 2 && x == 1)",
496+
"optional.of(int_var).optMap(x, x == 1 && x == 2)"),
497+
OPT_FLAT_MAP_MACRO_PREDICATE_ORDER(
498+
"optional.of(int_var).optFlatMap(x, optional.of(x == 2 && x == 1))",
499+
"optional.of(int_var).optFlatMap(x, optional.of(x == 1 && x == 2))"),
500+
501+
// Literal & Constant Comparator Branches
502+
CONST_UINT_SYMMETRIC_EQUALITY("20u == 10u", "10u == 20u"),
503+
CONST_DOUBLE_SYMMETRIC_EQUALITY("2.5 == 1.5", "1.5 == 2.5"),
504+
CONST_BYTES_SYMMETRIC_EQUALITY(
505+
"b'xyz' == b'abc'", "b\"\\141\\142\\143\" == b\"\\170\\171\\172\""),
506+
MAP_DIFFERENT_KEYS_EQUALITY("{'b': 1} == {'a': 1}", "{\"a\": 1} == {\"b\": 1}"),
507+
MAP_DIFFERENT_VALUES_EQUALITY("{'a': 2} == {'a': 1}", "{\"a\": 1} == {\"a\": 2}"),
508+
LIST_DIFFERENT_ELEMENTS_EQUALITY("[2, 1] == [1, 2]", "[1, 2] == [2, 1]"),
509+
SELECT_DIFFERENT_FIELDS_EQUALITY(
510+
"msg2.single_int64 == msg.single_int64", "msg.single_int64 == msg2.single_int64");
468511

469512
private final String input;
470513
private final String expected;
@@ -563,4 +606,34 @@ public void optimize_customMacroWithExistsStructure_notCanonicalized() throws Ex
563606
.optimizedAst();
564607
assertThat(UNPARSER.unparse(optimizedAst)).isEqualTo("!int_list.my_custom_exists(e, e == 1)");
565608
}
609+
610+
@Test
611+
public void optimize_comprehensionWithoutMacroCalls_deMorganSucceeds() throws Exception {
612+
CelAbstractSyntaxTree ast = CEL.compile("!int_list.exists(e, e == 1)").getAst();
613+
CelMutableAst mutableAst = CelMutableAst.fromCelAst(ast);
614+
mutableAst.source().getMacroCalls().clear();
615+
616+
CelAbstractSyntaxTree optimizedAst =
617+
CanonicalizationOptimizer.newInstance(CanonicalizationOptions.newBuilder().build())
618+
.optimize(mutableAst.toParsedAst(), CEL)
619+
.optimizedAst();
620+
assertThat(optimizedAst.getExpr().getKind()).isEqualTo(Kind.COMPREHENSION);
621+
assertThat(optimizedAst.getExpr().comprehension().accuInit().constant().booleanValue())
622+
.isTrue();
623+
}
624+
625+
@Test
626+
public void optimize_comprehensionAllWithoutMacroCalls_deMorganSucceeds() throws Exception {
627+
CelAbstractSyntaxTree ast = CEL.compile("!int_list.all(e, e == 1)").getAst();
628+
CelMutableAst mutableAst = CelMutableAst.fromCelAst(ast);
629+
mutableAst.source().getMacroCalls().clear();
630+
631+
CelAbstractSyntaxTree optimizedAst =
632+
CanonicalizationOptimizer.newInstance(CanonicalizationOptions.newBuilder().build())
633+
.optimize(mutableAst.toParsedAst(), CEL)
634+
.optimizedAst();
635+
assertThat(optimizedAst.getExpr().getKind()).isEqualTo(Kind.COMPREHENSION);
636+
assertThat(optimizedAst.getExpr().comprehension().accuInit().constant().booleanValue())
637+
.isFalse();
638+
}
566639
}

‎verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1312,7 +1312,7 @@ private enum IsAlwaysTrueViolationTestCase {
13121312
"dur != dur",
13131313
"Condition is not always true\\.",
13141314
"Counterexample input:",
1315-
"dur = duration\\(-?\\d+\\)"),
1315+
"dur = duration\\('-?\\d+s'\\)"),
13161316
TIMESTAMP_VARIABLE_COUNTEREXAMPLE(
13171317
"ts != ts",
13181318
"Condition is not always true\\.",

‎verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java‎

Lines changed: 62 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -53,9 +53,11 @@ private String[] runReplWithCommands(String... commands) throws Exception {
5353
@Test
5454
public void repl_quitAndExit() throws Exception {
5555
String[] output1 = runReplWithCommands(":quit");
56+
5657
assertThat(output1[0]).contains("Goodbye!");
5758

5859
String[] output2 = runReplWithCommands(":exit");
60+
5961
assertThat(output2[0]).contains("Goodbye!");
6062
}
6163

@@ -73,6 +75,7 @@ public void repl_helpCommands() throws Exception {
7375
":help equiv",
7476
":help non_existent_topic",
7577
":quit");
78+
7679
assertThat(output[0]).contains("REPL Commands:");
7780
assertThat(output[0]).contains("Command: :var <name> <type>");
7881
assertThat(output[0]).contains("Command: :unknown <identifier>");
@@ -81,6 +84,9 @@ public void repl_helpCommands() throws Exception {
8184
assertThat(output[0]).contains("Query: sat <expression>");
8285
assertThat(output[0]).contains("Query: valid <expression>");
8386
assertThat(output[0]).contains("Query: equiv <expression1> <=> <expression2>");
87+
assertThat(output[0]).contains("Well-known types: timestamp, duration");
88+
assertThat(output[0]).contains("Optional types: optional<T>");
89+
assertThat(output[0]).contains("Protobuf types: coming soon");
8490
}
8591

8692
@Test
@@ -91,19 +97,27 @@ public void repl_varDeclarations() throws Exception {
9197
":var port int",
9298
":var scores map<string,int>",
9399
":var tags list<string>",
100+
":var created_at timestamp",
101+
":var timeout duration",
102+
":var opt_user optional<string>",
94103
":vars",
95104
":quit");
105+
96106
assertThat(output[0]).contains("Variable declared: role : string");
97107
assertThat(output[0]).contains("Variable declared: port : int");
98108
assertThat(output[0]).contains("Variable declared: scores : map(string, int)");
99109
assertThat(output[0]).contains("Variable declared: tags : list(string)");
100-
assertThat(output[0]).contains("Variables (4):");
110+
assertThat(output[0]).contains("Variable declared: created_at : google.protobuf.Timestamp");
111+
assertThat(output[0]).contains("Variable declared: timeout : google.protobuf.Duration");
112+
assertThat(output[0]).contains("Variable declared: opt_user : optional_type(string)");
113+
assertThat(output[0]).contains("Variables (7):");
101114
}
102115

103116
@Test
104117
public void repl_unknownIdentifiers() throws Exception {
105118
String[] output =
106119
runReplWithCommands(":unknown request.headers", ":unknown request.auth", ":vars", ":quit");
120+
107121
assertThat(output[0]).contains("Added unknown identifier: 'request.headers'");
108122
assertThat(output[0]).contains("Added unknown identifier: 'request.auth'");
109123
assertThat(output[0]).contains("Unknowns: [request.headers, request.auth]");
@@ -114,6 +128,7 @@ public void repl_timeoutConfiguration() throws Exception {
114128
String[] output =
115129
runReplWithCommands(
116130
":timeout 15", ":vars", ":timeout -5", ":timeout abc", ":timeout", ":quit");
131+
117132
assertThat(output[0]).contains("Timeout set to 15s.");
118133
assertThat(output[0]).contains("Timeout: 15s");
119134
assertThat(output[1]).contains("Timeout must be a positive integer.");
@@ -125,6 +140,7 @@ public void repl_timeoutConfiguration() throws Exception {
125140
public void repl_unrollConfiguration() throws Exception {
126141
String[] output =
127142
runReplWithCommands(":unroll 10", ":vars", ":unroll -1", ":unroll xyz", ":unroll", ":quit");
143+
128144
assertThat(output[0]).contains("Comprehension unroll limit set to 10.");
129145
assertThat(output[0]).contains("Unroll limit: 10");
130146
assertThat(output[1]).contains("Unroll limit must be non-negative.");
@@ -137,6 +153,7 @@ public void repl_sessionStateAndClear() throws Exception {
137153
String[] output =
138154
runReplWithCommands(
139155
":var role string", ":unknown req.headers", ":vars", ":clear", ":vars", ":quit");
156+
140157
assertThat(output[0]).contains("Variables (1):");
141158
assertThat(output[0]).contains("Session state reset.");
142159
assertThat(output[0]).contains("Variables (0):");
@@ -147,6 +164,7 @@ public void repl_sessionStateAndClear() throws Exception {
147164
public void repl_satQueries() throws Exception {
148165
String[] output =
149166
runReplWithCommands(":var port int", "sat port > 1024", "port > 1024", "sat", ":quit");
167+
150168
assertThat(output[0]).contains("[VERIFIED]");
151169
assertThat(output[1]).contains("Usage: sat <expression>");
152170
}
@@ -155,6 +173,7 @@ public void repl_satQueries() throws Exception {
155173
public void repl_validQueries() throws Exception {
156174
String[] output =
157175
runReplWithCommands(":var x int", "valid x > 0 || x <= 0", "valid x > 0", "valid", ":quit");
176+
158177
assertThat(output[0]).contains("[VERIFIED]");
159178
assertThat(output[0]).contains("[VIOLATED]");
160179
assertThat(output[1]).contains("Usage: valid <expression>");
@@ -164,13 +183,15 @@ public void repl_validQueries() throws Exception {
164183
public void repl_equivQueries() throws Exception {
165184
String[] output =
166185
runReplWithCommands(":var x int", "equiv x > 10 <=> 10 < x", "equiv x > 10", ":quit");
186+
167187
assertThat(output[0]).contains("[VERIFIED]");
168188
assertThat(output[1]).contains("Equivalence query format: equiv <expr1> <=> <expr2>");
169189
}
170190

171191
@Test
172192
public void repl_equivDoubleNegation() throws Exception {
173193
String[] output = runReplWithCommands(":var x int", "equiv !!(x == 10) <=> (x == 10)", ":quit");
194+
174195
assertThat(output[0]).contains("[VERIFIED]");
175196
}
176197

@@ -184,6 +205,45 @@ public void repl_equivCanonicalization() throws Exception {
184205
+ " v, v == 1 && k == 'foo')",
185206
"equiv int_list.all(e, e > 0) <=> int_list.all(elem, elem > 0)",
186207
":quit");
208+
209+
assertThat(output[0]).contains("[VERIFIED]");
210+
assertThat(output[1]).isEmpty();
211+
}
212+
213+
@Test
214+
public void repl_timestampAndDurationQueries() throws Exception {
215+
String[] output =
216+
runReplWithCommands(
217+
":var t timestamp",
218+
":var d duration",
219+
"sat t > timestamp(1000)",
220+
"sat d > duration('60s')",
221+
"sat t + d > timestamp(2000)",
222+
":quit");
223+
224+
assertThat(output[0]).contains("[VERIFIED]");
225+
assertThat(output[1]).isEmpty();
226+
}
227+
228+
@Test
229+
public void repl_durationSatisfyingInputFormat() throws Exception {
230+
String[] output =
231+
runReplWithCommands(":var dur duration", "timestamp(100) - timestamp(50) == dur", ":quit");
232+
233+
assertThat(output[0]).contains("[VERIFIED]");
234+
assertThat(output[0]).contains("dur = duration('50s')");
235+
assertThat(output[1]).isEmpty();
236+
}
237+
238+
@Test
239+
public void repl_optionalQueries() throws Exception {
240+
String[] output =
241+
runReplWithCommands(
242+
":var opt_val optional<int>",
243+
"sat opt_val.hasValue() && opt_val.value() > 100",
244+
"sat !opt_val.hasValue()",
245+
":quit");
246+
187247
assertThat(output[0]).contains("[VERIFIED]");
188248
assertThat(output[1]).isEmpty();
189249
}
@@ -199,6 +259,7 @@ public void repl_unknownCommandsAndErrors() throws Exception {
199259
":unknown",
200260
"invalid + + syntax",
201261
":quit");
262+
202263
assertThat(output[1]).contains("Unknown command: :unknowncommand");
203264
assertThat(output[1]).contains("Usage: :var <name> <type>");
204265
assertThat(output[1]).contains("Unsupported type");

0 commit comments

Comments
 (0)