From 9b7aabbe0af3c4e66fe9333b206c746e6214dc91 Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Thu, 6 Aug 2026 12:04:34 -0700 Subject: [PATCH] Add timestamp, duration and optional types to CEL Verifier CLI PiperOrigin-RevId: 960433430 --- .../CelZ3CounterexampleGenerator.java | 2 +- .../cel/verifier/tools/CelVerifierRepl.java | 12 +++- .../verifier/tools/VerificationOptions.java | 36 ++++++++-- .../cel/verifier/CelVerifierZ3ImplTest.java | 2 +- .../verifier/tools/CelVerifierReplTest.java | 63 +++++++++++++++- .../verifier/tools/CelVerifierToolTest.java | 68 ++++++++++++++++-- .../tools/VerificationOptionsTest.java | 71 ++++++++++++++++++- verifier/tools/README.md | 5 +- 8 files changed, 237 insertions(+), 22 deletions(-) diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index 6e5c519fe..cef976608 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -88,7 +88,7 @@ private static String formatExpr( } else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) { return "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")"; } else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) { - return "duration(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")"; + return "duration('" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "s')"; } else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) { return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u"; } else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) { diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java index 94348ff15..82a93c3d7 100644 --- a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java @@ -314,15 +314,21 @@ private static void printHelp(String topic, PrintStream out) { out.println("Declares a variable in the REPL session with a specific type."); out.println(); out.println("Supported Types:"); - out.println(" - Primitive types: int, uint, string, bool, double, bytes"); - out.println(" - List types: list (e.g., list, list)"); - out.println(" - Map types: map (e.g., map, map)"); + out.println(" - Primitive types: int, uint, string, bool, double, bytes, dyn"); + out.println(" - Well-known types: timestamp, duration"); + out.println(" - List types: list (e.g., list, list)"); + out.println(" - Map types: map (e.g., map, map)"); + out.println(" - Optional types: optional (e.g., optional, optional)"); + out.println(" - Protobuf types: coming soon"); out.println(); out.println("Examples:"); out.println(" cel-verifier> :var role string"); out.println(" cel-verifier> :var port int"); out.println(" cel-verifier> :var scores map"); out.println(" cel-verifier> :var tags list"); + out.println(" cel-verifier> :var created_at timestamp"); + out.println(" cel-verifier> :var timeout duration"); + out.println(" cel-verifier> :var opt_flag optional"); break; case "unknown": out.println("Command: :unknown "); diff --git a/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java index f2b3bf742..32a5763f5 100644 --- a/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java +++ b/verifier/src/main/java/dev/cel/verifier/tools/VerificationOptions.java @@ -21,6 +21,7 @@ import dev.cel.common.types.CelType; import dev.cel.common.types.ListType; import dev.cel.common.types.MapType; +import dev.cel.common.types.OptionalType; import dev.cel.common.types.SimpleType; import java.time.Duration; import java.util.ArrayList; @@ -150,13 +151,15 @@ static CelType parseCelType(String typeStr) { Preconditions.checkNotNull(typeStr, "Type string cannot be null."); String str = typeStr.trim().toLowerCase(Locale.US); - if (str.startsWith("list<") && str.endsWith(">")) { + if ((str.startsWith("list<") && str.endsWith(">")) + || (str.startsWith("list(") && str.endsWith(")"))) { String inner = str.substring(5, str.length() - 1).trim(); CelType elemType = parseCelType(inner); return ListType.create(elemType); } - if (str.startsWith("map<") && str.endsWith(">")) { + if ((str.startsWith("map<") && str.endsWith(">")) + || (str.startsWith("map(") && str.endsWith(")"))) { String inner = str.substring(4, str.length() - 1).trim(); List parts = splitGenericArgs(inner); if (parts.size() != 2) { @@ -170,6 +173,20 @@ static CelType parseCelType(String typeStr) { return MapType.create(keyType, valueType); } + if ((str.startsWith("optional<") && str.endsWith(">")) + || (str.startsWith("optional(") && str.endsWith(")"))) { + String inner = str.substring(9, str.length() - 1).trim(); + CelType elemType = parseCelType(inner); + return OptionalType.create(elemType); + } + + if ((str.startsWith("optional_type<") && str.endsWith(">")) + || (str.startsWith("optional_type(") && str.endsWith(")"))) { + String inner = str.substring(14, str.length() - 1).trim(); + CelType elemType = parseCelType(inner); + return OptionalType.create(elemType); + } + switch (str) { case "int": return SimpleType.INT; @@ -187,12 +204,19 @@ static CelType parseCelType(String typeStr) { return SimpleType.BYTES; case "dyn": return SimpleType.DYN; + case "timestamp": + case "google.protobuf.timestamp": + return SimpleType.TIMESTAMP; + case "duration": + case "google.protobuf.duration": + return SimpleType.DURATION; default: + // TODO: Support protobuf message types (coming soon). throw new IllegalArgumentException( "Unsupported type for CLI variable declaration: '" + typeStr - + "'. Supported types: int, uint, string, bool, double, bytes, dyn, list, map."); + + "'. Supported types: int, uint, string, bool, double, bytes, dyn, timestamp," + + " duration, list, map, optional."); } } @@ -202,10 +226,10 @@ private static List splitGenericArgs(String inner) { StringBuilder current = new StringBuilder(); for (int i = 0; i < inner.length(); i++) { char c = inner.charAt(i); - if (c == '<') { + if (c == '<' || c == '(') { depth++; current.append(c); - } else if (c == '>') { + } else if (c == '>' || c == ')') { depth--; current.append(c); } else if (c == ',' && depth == 0) { diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index d7724ac91..003256e0c 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -1312,7 +1312,7 @@ private enum IsAlwaysTrueViolationTestCase { "dur != dur", "Condition is not always true\\.", "Counterexample input:", - "dur = duration\\(-?\\d+\\)"), + "dur = duration\\('-?\\d+s'\\)"), TIMESTAMP_VARIABLE_COUNTEREXAMPLE( "ts != ts", "Condition is not always true\\.", diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java index 88cd62b88..cbe5fffd5 100644 --- a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java @@ -53,9 +53,11 @@ private String[] runReplWithCommands(String... commands) throws Exception { @Test public void repl_quitAndExit() throws Exception { String[] output1 = runReplWithCommands(":quit"); + assertThat(output1[0]).contains("Goodbye!"); String[] output2 = runReplWithCommands(":exit"); + assertThat(output2[0]).contains("Goodbye!"); } @@ -73,6 +75,7 @@ public void repl_helpCommands() throws Exception { ":help equiv", ":help non_existent_topic", ":quit"); + assertThat(output[0]).contains("REPL Commands:"); assertThat(output[0]).contains("Command: :var "); assertThat(output[0]).contains("Command: :unknown "); @@ -81,6 +84,9 @@ public void repl_helpCommands() throws Exception { assertThat(output[0]).contains("Query: sat "); assertThat(output[0]).contains("Query: valid "); assertThat(output[0]).contains("Query: equiv <=> "); + assertThat(output[0]).contains("Well-known types: timestamp, duration"); + assertThat(output[0]).contains("Optional types: optional"); + assertThat(output[0]).contains("Protobuf types: coming soon"); } @Test @@ -91,19 +97,27 @@ public void repl_varDeclarations() throws Exception { ":var port int", ":var scores map", ":var tags list", + ":var created_at timestamp", + ":var timeout duration", + ":var opt_user optional", ":vars", ":quit"); + assertThat(output[0]).contains("Variable declared: role : string"); assertThat(output[0]).contains("Variable declared: port : int"); assertThat(output[0]).contains("Variable declared: scores : map(string, int)"); assertThat(output[0]).contains("Variable declared: tags : list(string)"); - assertThat(output[0]).contains("Variables (4):"); + assertThat(output[0]).contains("Variable declared: created_at : google.protobuf.Timestamp"); + assertThat(output[0]).contains("Variable declared: timeout : google.protobuf.Duration"); + assertThat(output[0]).contains("Variable declared: opt_user : optional_type(string)"); + assertThat(output[0]).contains("Variables (7):"); } @Test public void repl_unknownIdentifiers() throws Exception { String[] output = runReplWithCommands(":unknown request.headers", ":unknown request.auth", ":vars", ":quit"); + assertThat(output[0]).contains("Added unknown identifier: 'request.headers'"); assertThat(output[0]).contains("Added unknown identifier: 'request.auth'"); assertThat(output[0]).contains("Unknowns: [request.headers, request.auth]"); @@ -114,6 +128,7 @@ public void repl_timeoutConfiguration() throws Exception { String[] output = runReplWithCommands( ":timeout 15", ":vars", ":timeout -5", ":timeout abc", ":timeout", ":quit"); + assertThat(output[0]).contains("Timeout set to 15s."); assertThat(output[0]).contains("Timeout: 15s"); assertThat(output[1]).contains("Timeout must be a positive integer."); @@ -125,6 +140,7 @@ public void repl_timeoutConfiguration() throws Exception { public void repl_unrollConfiguration() throws Exception { String[] output = runReplWithCommands(":unroll 10", ":vars", ":unroll -1", ":unroll xyz", ":unroll", ":quit"); + assertThat(output[0]).contains("Comprehension unroll limit set to 10."); assertThat(output[0]).contains("Unroll limit: 10"); assertThat(output[1]).contains("Unroll limit must be non-negative."); @@ -137,6 +153,7 @@ public void repl_sessionStateAndClear() throws Exception { String[] output = runReplWithCommands( ":var role string", ":unknown req.headers", ":vars", ":clear", ":vars", ":quit"); + assertThat(output[0]).contains("Variables (1):"); assertThat(output[0]).contains("Session state reset."); assertThat(output[0]).contains("Variables (0):"); @@ -147,6 +164,7 @@ public void repl_sessionStateAndClear() throws Exception { public void repl_satQueries() throws Exception { String[] output = runReplWithCommands(":var port int", "sat port > 1024", "port > 1024", "sat", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); assertThat(output[1]).contains("Usage: sat "); } @@ -155,6 +173,7 @@ public void repl_satQueries() throws Exception { public void repl_validQueries() throws Exception { String[] output = runReplWithCommands(":var x int", "valid x > 0 || x <= 0", "valid x > 0", "valid", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); assertThat(output[0]).contains("[VIOLATED]"); assertThat(output[1]).contains("Usage: valid "); @@ -164,6 +183,7 @@ public void repl_validQueries() throws Exception { public void repl_equivQueries() throws Exception { String[] output = runReplWithCommands(":var x int", "equiv x > 10 <=> 10 < x", "equiv x > 10", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); assertThat(output[1]).contains("Equivalence query format: equiv <=> "); } @@ -171,6 +191,7 @@ public void repl_equivQueries() throws Exception { @Test public void repl_equivDoubleNegation() throws Exception { String[] output = runReplWithCommands(":var x int", "equiv !!(x == 10) <=> (x == 10)", ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); } @@ -184,6 +205,45 @@ public void repl_equivCanonicalization() throws Exception { + " v, v == 1 && k == 'foo')", "equiv int_list.all(e, e > 0) <=> int_list.all(elem, elem > 0)", ":quit"); + + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[1]).isEmpty(); + } + + @Test + public void repl_timestampAndDurationQueries() throws Exception { + String[] output = + runReplWithCommands( + ":var t timestamp", + ":var d duration", + "sat t > timestamp(1000)", + "sat d > duration('60s')", + "sat t + d > timestamp(2000)", + ":quit"); + + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[1]).isEmpty(); + } + + @Test + public void repl_durationSatisfyingInputFormat() throws Exception { + String[] output = + runReplWithCommands(":var dur duration", "timestamp(100) - timestamp(50) == dur", ":quit"); + + assertThat(output[0]).contains("[VERIFIED]"); + assertThat(output[0]).contains("dur = duration('50s')"); + assertThat(output[1]).isEmpty(); + } + + @Test + public void repl_optionalQueries() throws Exception { + String[] output = + runReplWithCommands( + ":var opt_val optional", + "sat opt_val.hasValue() && opt_val.value() > 100", + "sat !opt_val.hasValue()", + ":quit"); + assertThat(output[0]).contains("[VERIFIED]"); assertThat(output[1]).isEmpty(); } @@ -199,6 +259,7 @@ public void repl_unknownCommandsAndErrors() throws Exception { ":unknown", "invalid + + syntax", ":quit"); + assertThat(output[1]).contains("Unknown command: :unknowncommand"); assertThat(output[1]).contains("Usage: :var "); assertThat(output[1]).contains("Unsupported type"); diff --git a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java index e3b2a21a6..2d01e7a0f 100644 --- a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java @@ -22,6 +22,7 @@ import dev.cel.common.types.CelType; import dev.cel.common.types.ListType; import dev.cel.common.types.MapType; +import dev.cel.common.types.OptionalType; import dev.cel.common.types.SimpleType; import dev.cel.verifier.CelVerificationResult; import dev.cel.verifier.CelVerificationResult.VerificationStatus; @@ -65,6 +66,7 @@ public void celVerifierTool_checkSat_jsonOutputFormat() { String output = executeToolWithOutput( "check-sat", "--expr", "x > 0", "--var", "x:int", "--output_format", "json"); + assertThat(output).startsWith("{\n"); assertThat(output).contains("\"status\": \"VERIFIED\""); assertThat(output).contains("satisfiable"); @@ -75,6 +77,7 @@ public void celVerifierTool_checkSat_jsonOutputFormat() { public void celVerifierTool_checkSat_textOutputFormat() { String output = executeToolWithOutput("check-sat", "--expr", "x > 0", "--var", "x:int", "-fmt", "text"); + assertThat(output).contains("[VERIFIED]"); assertThat(output).contains("satisfiable"); } @@ -84,6 +87,7 @@ public void celVerifierTool_checkSat_withDynVariable() { String output = executeToolWithOutput( "check-sat", "--expr", "x == 'hello'", "--var", "x:dyn", "-fmt", "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); } @@ -100,6 +104,7 @@ public void celVerifierTool_checkSat_withUnknownOption() { "request.headers", "-fmt", "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); } @@ -116,12 +121,33 @@ public void celVerifierTool_checkSat_withTimeoutAndUnrollLimit() { "5", "-fmt", "json"); + + assertThat(output).contains("\"status\": \"VERIFIED\""); + } + + @Test + public void celVerifierTool_checkSat_withTimestampDurationAndOptional() { + String output = + executeToolWithOutput( + "check-sat", + "--expr", + "t + d > timestamp(1000) && opt.hasValue()", + "--var", + "t:timestamp", + "--var", + "d:duration", + "--var", + "opt:optional", + "-fmt", + "json"); + assertThat(output).contains("\"status\": \"VERIFIED\""); } @Test public void celVerifierTool_verifyPolicy_fileNotFound() { String output = executeToolWithOutput("verify-policy", "--file", "non_existent_policy.yaml"); + assertThat(output).contains("File not found: non_existent_policy.yaml"); } @@ -134,12 +160,19 @@ public void parseVariables_success() { "role:string", "is_admin:bool", "tags:list", - "scores:map")); + "scores:map", + "created_at:timestamp", + "timeout:duration", + "opt_user:optional")); + assertThat(vars).containsEntry("x", SimpleType.INT); assertThat(vars).containsEntry("role", SimpleType.STRING); assertThat(vars).containsEntry("is_admin", SimpleType.BOOL); assertThat(vars).containsEntry("tags", ListType.create(SimpleType.STRING)); assertThat(vars).containsEntry("scores", MapType.create(SimpleType.STRING, SimpleType.INT)); + assertThat(vars).containsEntry("created_at", SimpleType.TIMESTAMP); + assertThat(vars).containsEntry("timeout", SimpleType.DURATION); + assertThat(vars).containsEntry("opt_user", OptionalType.create(SimpleType.STRING)); } @Test @@ -153,14 +186,21 @@ public void parseVariables_allTypesIncludingDyn() { "b:bytes", "dyn_val:dyn", "flag:boolean", + "t:google.protobuf.timestamp", + "dur:google.protobuf.duration", + "opt:optional", "nested_list:list", "nested_map:map")); + assertThat(vars).containsEntry("u", SimpleType.UINT); assertThat(vars).containsEntry("d", SimpleType.DOUBLE); assertThat(vars).containsEntry("fl", SimpleType.DOUBLE); assertThat(vars).containsEntry("b", SimpleType.BYTES); assertThat(vars).containsEntry("dyn_val", SimpleType.DYN); assertThat(vars).containsEntry("flag", SimpleType.BOOL); + assertThat(vars).containsEntry("t", SimpleType.TIMESTAMP); + assertThat(vars).containsEntry("dur", SimpleType.DURATION); + assertThat(vars).containsEntry("opt", OptionalType.create(SimpleType.INT)); assertThat(vars).containsEntry("nested_list", ListType.create(SimpleType.DYN)); assertThat(vars).containsEntry("nested_map", MapType.create(SimpleType.STRING, SimpleType.DYN)); } @@ -178,9 +218,12 @@ public void parseVariables_unsupportedType_throws() { assertThrows( IllegalArgumentException.class, () -> VerificationOptions.parseVariables(Arrays.asList("x:foo_bar"))); + assertThat(ex) .hasMessageThat() - .contains("Supported types: int, uint, string, bool, double, bytes, dyn"); + .contains( + "Supported types: int, uint, string, bool, double, bytes, dyn, timestamp," + + " duration, list, map, optional."); } @Test @@ -203,6 +246,7 @@ public void parseVariables_nestedTypes() { Arrays.asList( "nested_map:map>", "nested_list_map:map>")); + assertThat(vars) .containsEntry( "nested_map", @@ -298,7 +342,6 @@ public void verifyPolicyInvariants_success() throws Exception { + " - id: port_check\n" + " assert:\n" + " - port == 80 || port != 80\n"; - VerificationOptions options = VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); ImmutableMap vars = ImmutableMap.of("port", SimpleType.INT); @@ -319,7 +362,6 @@ public void verifyPolicyEquivalence_equivalent() throws Exception { + " - condition: port == 80\n" + " output: 'true'\n" + " - output: 'false'\n"; - String policyB = "name: policy_b\n" + "rule:\n" @@ -327,7 +369,6 @@ public void verifyPolicyEquivalence_equivalent() throws Exception { + " - condition: 80 == port\n" + " output: 'true'\n" + " - output: 'false'\n"; - VerificationOptions options = VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); ImmutableMap vars = ImmutableMap.of("port", SimpleType.INT); @@ -346,11 +387,11 @@ public void formatTextPolicyResults_verifiedAndViolated() throws Exception { CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); CelVerificationResult violatedRes = CelVerifierToolCore.checkValid("x > 0", ImmutableMap.of("x", SimpleType.INT), options); - ImmutableMap results = ImmutableMap.of("inv_1", verifiedRes, "inv_2", violatedRes); String text = FormatUtils.formatTextPolicyResults("test_policy", results); + assertThat(text).contains("Policy Invariant Verification for 'test_policy':"); assertThat(text).contains("✓ Invariant 'inv_1': VERIFIED"); assertThat(text).contains("✗ Invariant 'inv_2': VIOLATED"); @@ -362,10 +403,10 @@ public void formatJsonPolicyResults_structuredJson() throws Exception { VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); CelVerificationResult result = CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); - ImmutableMap results = ImmutableMap.of("inv_1", result); String json = FormatUtils.formatJsonPolicyResults("my_policy", results); + assertThat(json).startsWith("{\n"); assertThat(json).contains("\"policyName\": \"my_policy\""); assertThat(json).contains("\"id\": \"inv_1\""); @@ -488,7 +529,9 @@ public void formatUtils_jsonResult() throws Exception { VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); CelVerificationResult result = CelVerifierToolCore.checkSatisfiable("true", ImmutableMap.of(), options); + String json = FormatUtils.formatJsonResult(result); + assertThat(json).contains("\"status\": \"VERIFIED\""); assertThat(json).contains("satisfiable"); } @@ -498,6 +541,7 @@ public void celVerifierTool_checkSat_verified() { int exitCode = new CommandLine(new CelVerifierTool()) .execute("check-sat", "--expr", "x > 0", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VERIFIED); } @@ -506,6 +550,7 @@ public void celVerifierTool_checkValid_violated() { int exitCode = new CommandLine(new CelVerifierTool()) .execute("check-valid", "--expr", "x > 0", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VIOLATED); } @@ -514,6 +559,7 @@ public void celVerifierTool_verifyEquiv_verified() { int exitCode = new CommandLine(new CelVerifierTool()) .execute("verify-equiv", "--expr1", "x > 10", "--expr2", "10 < x", "--var", "x:int"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VERIFIED); } @@ -521,6 +567,7 @@ public void celVerifierTool_verifyEquiv_verified() { public void celVerifierTool_checkSat_compilationError() { String output = executeToolWithOutput("check-sat", "--expr", "invalid + + syntax", "--var", "x:int"); + assertThat(output).contains("Compilation error"); } @@ -529,6 +576,7 @@ public void celVerifierTool_checkValid_withUnknownOption_violated() { int exitCode = new CommandLine(new CelVerifierTool()) .execute("check-valid", "--expr", "x == x", "--var", "x:int", "-u", "x"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_VIOLATED); } @@ -537,6 +585,7 @@ public void celVerifierTool_checkValid_inconclusive() { int exitCode = new CommandLine(new CelVerifierTool()) .execute("check-valid", "--expr", "int('123') == 123"); + assertThat(exitCode).isEqualTo(CelVerifierTool.EXIT_CODE_INCONCLUSIVE); } @@ -569,6 +618,7 @@ public void celVerifierTool_invalidOutputFormat_defaultsToText() { String output = executeToolWithOutput( "check-sat", "--expr", "x > 0", "--var", "x:int", "-fmt", "invalid_fmt"); + assertThat(output).contains("[VERIFIED]"); } @@ -580,6 +630,7 @@ public void formatTextPolicyResults_inconclusive() throws Exception { CelVerifierToolCore.checkValid("int('123') == 123", ImmutableMap.of(), options); String text = FormatUtils.formatTextPolicyResults("test_policy", ImmutableMap.of("inv_1", res)); + assertThat(text).contains("Invariant 'inv_1': INCONCLUSIVE"); } @@ -589,9 +640,11 @@ public void formatJson_escapesSpecialCharacters() throws Exception { VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); CelVerificationResult res = CelVerifierToolCore.checkValid("int('123') == 123", ImmutableMap.of(), options); + String json = FormatUtils.formatJsonPolicyResults( "policy_with_\"quote\"\nand_newline", ImmutableMap.of("inv\ttab", res)); + assertThat(json).contains("policy_with_\\\"quote\\\"\\nand_newline"); assertThat(json).contains("inv\\ttab"); } @@ -599,6 +652,7 @@ public void formatJson_escapesSpecialCharacters() throws Exception { @Test public void celVerifierTool_version() { int exitCode = new CommandLine(new CelVerifierTool()).execute("--version"); + assertThat(exitCode).isEqualTo(0); } } diff --git a/verifier/src/test/java/dev/cel/verifier/tools/VerificationOptionsTest.java b/verifier/src/test/java/dev/cel/verifier/tools/VerificationOptionsTest.java index 28aac751a..98e5bcb4e 100644 --- a/verifier/src/test/java/dev/cel/verifier/tools/VerificationOptionsTest.java +++ b/verifier/src/test/java/dev/cel/verifier/tools/VerificationOptionsTest.java @@ -20,6 +20,9 @@ import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import dev.cel.common.types.CelType; +import dev.cel.common.types.ListType; +import dev.cel.common.types.MapType; +import dev.cel.common.types.OptionalType; import dev.cel.common.types.SimpleType; import dev.cel.verifier.tools.VerificationOptions.OutputFormat; import java.time.Duration; @@ -62,31 +65,80 @@ public void customOptions_allFieldsSet() { @Test public void setTimeout_null_throwsException() { VerificationOptions.Builder builder = VerificationOptions.builder(); + assertThrows(NullPointerException.class, () -> builder.setTimeout(null)); } @Test public void setComprehensionUnrollLimit_negative_throwsException() { VerificationOptions.Builder builder = VerificationOptions.builder(); + assertThrows(IllegalArgumentException.class, () -> builder.setComprehensionUnrollLimit(-1)); } @Test public void setOutputFormat_null_throwsException() { VerificationOptions.Builder builder = VerificationOptions.builder(); + assertThrows(NullPointerException.class, () -> builder.setOutputFormat(null)); } @Test public void parseVariables_validSpecs() { ImmutableMap vars = - VerificationOptions.parseVariables(ImmutableList.of("x:int", "name:string", "flag:bool")); + VerificationOptions.parseVariables( + ImmutableList.of( + "x:int", + "name:string", + "flag:bool", + "created_at:timestamp", + "timeout:duration", + "opt_user:optional", + "opt_list:optional>", + "opt_map:optional>")); assertThat(vars) .containsExactly( "x", SimpleType.INT, "name", SimpleType.STRING, - "flag", SimpleType.BOOL); + "flag", SimpleType.BOOL, + "created_at", SimpleType.TIMESTAMP, + "timeout", SimpleType.DURATION, + "opt_user", OptionalType.create(SimpleType.STRING), + "opt_list", OptionalType.create(ListType.create(SimpleType.INT)), + "opt_map", OptionalType.create(MapType.create(SimpleType.STRING, SimpleType.INT))); + } + + @Test + public void parseCelType_timestampAndDuration() { + assertThat(VerificationOptions.parseCelType("timestamp")).isEqualTo(SimpleType.TIMESTAMP); + assertThat(VerificationOptions.parseCelType("google.protobuf.timestamp")) + .isEqualTo(SimpleType.TIMESTAMP); + assertThat(VerificationOptions.parseCelType("google.protobuf.Timestamp")) + .isEqualTo(SimpleType.TIMESTAMP); + assertThat(VerificationOptions.parseCelType("duration")).isEqualTo(SimpleType.DURATION); + assertThat(VerificationOptions.parseCelType("google.protobuf.duration")) + .isEqualTo(SimpleType.DURATION); + assertThat(VerificationOptions.parseCelType("google.protobuf.Duration")) + .isEqualTo(SimpleType.DURATION); + } + + @Test + public void parseCelType_optionalTypes() { + assertThat(VerificationOptions.parseCelType("optional")) + .isEqualTo(OptionalType.create(SimpleType.INT)); + assertThat(VerificationOptions.parseCelType("optional")) + .isEqualTo(OptionalType.create(SimpleType.STRING)); + assertThat(VerificationOptions.parseCelType("optional(double)")) + .isEqualTo(OptionalType.create(SimpleType.DOUBLE)); + assertThat(VerificationOptions.parseCelType("optional_type")) + .isEqualTo(OptionalType.create(SimpleType.BOOL)); + assertThat(VerificationOptions.parseCelType("optional_type(bytes)")) + .isEqualTo(OptionalType.create(SimpleType.BYTES)); + assertThat(VerificationOptions.parseCelType("optional>")) + .isEqualTo(OptionalType.create(OptionalType.create(SimpleType.INT))); + assertThat(VerificationOptions.parseCelType("map>")) + .isEqualTo(MapType.create(SimpleType.STRING, OptionalType.create(SimpleType.INT))); } @Test @@ -98,6 +150,21 @@ public void parseVariables_nullOrEmpty_returnsEmptyMap() { @Test public void parseVariables_invalidSpec_throwsException() { ImmutableList specs = ImmutableList.of("invalid_spec_without_colon"); + assertThrows(IllegalArgumentException.class, () -> VerificationOptions.parseVariables(specs)); } + + @Test + public void parseVariables_unsupportedType_throwsException() { + ImmutableList specs = ImmutableList.of("x:unknown_type"); + + IllegalArgumentException ex = + assertThrows( + IllegalArgumentException.class, () -> VerificationOptions.parseVariables(specs)); + assertThat(ex) + .hasMessageThat() + .contains( + "Supported types: int, uint, string, bool, double, bytes, dyn, timestamp," + + " duration, list, map, optional."); + } } diff --git a/verifier/tools/README.md b/verifier/tools/README.md index b34422b27..09b83ad70 100644 --- a/verifier/tools/README.md +++ b/verifier/tools/README.md @@ -66,12 +66,15 @@ repeating the `--var` option. Supported types: * Primitive types: `int`, `uint`, `string`, `bool`, `double`, `bytes`, `dyn` +* Well-known types: `timestamp`, `duration` * List types: `list` (e.g., `--var "tags:list"`) * Map types: `map` (e.g., `--var "scores:map"`) +* Optional types: `optional` (e.g., `--var "opt_flag:optional"`) +* Protobuf types: Coming soon Examples: ```bash ---var "role:string" --var "port:int" --var "tags:list" +--var "role:string" --var "port:int" --var "tags:list" --var "created_at:timestamp" --var "opt_flag:optional" ``` ### Unknown Identifiers (`--unknown`, `-u`)