Skip to content

Commit 19bbb93

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Refactor Canonicalization Optimizer
No functional changes PiperOrigin-RevId: 960456441
1 parent d459cc9 commit 19bbb93

10 files changed

Lines changed: 952 additions & 442 deletions

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

Lines changed: 714 additions & 419 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: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -285,7 +285,7 @@ private enum CanonicalizationTestCase {
285285
"int_list.all(i, v, v == 100 || i == 0)", "int_list.all(i, v, i == 0 || v == 100)"),
286286
TWO_VAR_NESTED_COMPREHENSIONS(
287287
"string_int_map.exists(k, v, k == 'foo' && int_list.all(i, e, e == v && i == 0))",
288-
"string_int_map.exists(k, v, k == \"foo\" && int_list.all(i, e, e == v && i == 0))"),
288+
"string_int_map.exists(k, v, k == \"foo\" && int_list.all(i, e, i == 0 && e == v))"),
289289
DE_MORGAN_2VAR_NESTED_COMPREHENSIONS(
290290
"string_int_map.exists(k, v, k == 'foo' && !int_list.exists(i, e, e == v))",
291291
"string_int_map.exists(k, v, k == \"foo\" && e != v)"),

‎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)