From 0b7891e7688bb10204adbb5541f5ba3cddc26496 Mon Sep 17 00:00:00 2001 From: Tristan Swadell Date: Fri, 16 Oct 2026 15:17:23 -0700 Subject: [PATCH] No public description PiperOrigin-RevId: 1001131887 --- .../main/java/dev/cel/verifier/BUILD.bazel | 3 + .../cel/verifier/CelAstToZ3Translator.java | 143 +++++++++++++++++- .../dev/cel/verifier/CelVerifierZ3Impl.java | 29 +++- .../java/dev/cel/verifier/tools/BUILD.bazel | 4 +- .../cel/verifier/tools/CelVerifierRepl.java | 2 +- .../verifier/tools/CelVerifierToolCore.java | 55 ++++--- .../verifier/tools/VerificationOptions.java | 24 ++- .../cel/verifier/CelVerifierZ3ImplTest.java | 88 ++++++++++- .../verifier/tools/CelVerifierReplTest.java | 2 +- .../verifier/tools/CelVerifierToolTest.java | 57 ++++++- .../tools/VerificationOptionsTest.java | 30 +++- 11 files changed, 403 insertions(+), 34 deletions(-) diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index 888af79a5..bd455ab50 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel @@ -178,6 +178,8 @@ java_library( "//common:operator", "//common/ast", "//common/ast:cel_block", + "//common/internal:cel_descriptor_pools", + "//common/internal:well_known_proto", "//common/types", "//common/types:cel_types", "//common/types:type_providers", @@ -187,6 +189,7 @@ java_library( "//verifier/axioms", "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:com_google_guava_guava", + "@maven//:com_google_protobuf_protobuf_java", "@maven//:org_jspecify_jspecify", "@maven//:tools_aqua_z3_turnkey", ], diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 26b8d9a88..8f0f5475c 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -401,6 +401,12 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a if (isJsonWkt(createStruct.messageName())) { return translateJsonWktStruct(celExpr, createStruct, ast); } + if (CelTypes.isWrapperType(createStruct.messageName())) { + return translateWrapperWktStruct(celExpr, createStruct, ast); + } + if (isTimeWkt(createStruct.messageName())) { + return translateTimeWktStruct(celExpr, createStruct, ast); + } // Bypass SMT when the struct is empty (return the cached SMT default pointer) if (createStruct.entries().isEmpty()) { @@ -517,7 +523,12 @@ private TranslatedValue translateJsonWktStruct( && entry.fieldKey().equals(NULL_VALUE_FIELD); if (entry.optionalEntry()) { - Expr optRef = typeSystem.getOptionalRef(finalVal); + Expr checkedVal = + typeSystem.withRuntimeError(finalVal, ctx.mkNot(typeSystem.isOptional(finalVal))); + entryTv = + TranslatedValue.create( + checkedVal, entry.value(), typeSystem, entryTv.isApproximate()); + Expr optRef = typeSystem.getOptionalRef(checkedVal); BoolExpr hasValue = typeSystem.optHasValue(optRef); Expr unpackedVal = typeSystem.getOptionalValue(optRef); @@ -533,6 +544,136 @@ private TranslatedValue translateJsonWktStruct( ctx, typeSystem, finalVal, celExpr, ImmutableList.of(entryTv)); } + private TranslatedValue translateWrapperWktStruct( + CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) { + String typeName = createStruct.messageName(); + CelType wrapperType = + CelTypes.getWellKnownCelType(typeName) + .orElseThrow( + () -> new IllegalArgumentException("Unexpected wrapper type: " + typeName)); + CelType targetType = ((NullableType) wrapperType).targetType(); + Expr currentVal = getDefaultValueForType(targetType); + + List entryTvs = new ArrayList<>(); + for (CelExpr.CelStruct.Entry entry : createStruct.entries()) { + TranslatedValue entryTv = translateExpr(entry.value(), ast); + Expr val = entryTv.z3Expr(); + if (entry.optionalEntry()) { + Expr checkedVal = + typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val))); + entryTv = + TranslatedValue.create( + checkedVal, entry.value(), typeSystem, entryTv.isApproximate()); + Expr optRef = typeSystem.getOptionalRef(checkedVal); + BoolExpr hasValue = typeSystem.optHasValue(optRef); + currentVal = ctx.mkITE(hasValue, typeSystem.getOptionalValue(optRef), currentVal); + } else { + currentVal = val; + } + entryTvs.add(entryTv); + } + BoolExpr validValue = createTypeConstraintForType(currentVal, targetType); + if (typeName.equals(CelTypes.INT32_WRAPPER_MESSAGE)) { + IntExpr intVal = typeSystem.getInt(currentVal); + validValue = + ctx.mkAnd( + validValue, + ctx.mkGe(intVal, ctx.mkInt(Integer.MIN_VALUE)), + ctx.mkLe(intVal, ctx.mkInt(Integer.MAX_VALUE))); + } else if (typeName.equals(CelTypes.UINT32_WRAPPER_MESSAGE)) { + IntExpr uintVal = typeSystem.getUint(currentVal); + validValue = + ctx.mkAnd( + validValue, + ctx.mkGe(uintVal, ctx.mkInt(0)), + ctx.mkLe(uintVal, ctx.mkInt(0xFFFFFFFFL))); + } + currentVal = typeSystem.withRuntimeError(currentVal, ctx.mkNot(validValue)); + return TranslatedValue.propagateStrict(ctx, typeSystem, currentVal, celExpr, entryTvs); + } + + private static boolean isTimeWkt(String messageName) { + return messageName.equals(CelTypes.TIMESTAMP_MESSAGE) + || messageName.equals(CelTypes.DURATION_MESSAGE); + } + + private TranslatedValue translateTimeWktStruct( + CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) { + boolean isTimestamp = createStruct.messageName().equals(CelTypes.TIMESTAMP_MESSAGE); + Expr secondsVal = typeSystem.mkInt(0); + Expr nanosVal = typeSystem.mkInt(0); + List entryTvs = new ArrayList<>(); + + for (CelExpr.CelStruct.Entry entry : createStruct.entries()) { + TranslatedValue entryTv = translateExpr(entry.value(), ast); + Expr val = entryTv.z3Expr(); + Expr unpackedVal = val; + BoolExpr hasValue = ctx.mkTrue(); + if (entry.optionalEntry()) { + Expr checkedVal = + typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val))); + entryTv = + TranslatedValue.create( + checkedVal, entry.value(), typeSystem, entryTv.isApproximate()); + Expr optRef = typeSystem.getOptionalRef(checkedVal); + hasValue = typeSystem.optHasValue(optRef); + unpackedVal = typeSystem.getOptionalValue(optRef); + } + if (entry.fieldKey().equals("seconds")) { + secondsVal = ctx.mkITE(hasValue, unpackedVal, secondsVal); + } else { + nanosVal = ctx.mkITE(hasValue, unpackedVal, nanosVal); + } + entryTvs.add(entryTv); + } + + IntExpr seconds = typeSystem.getInt(secondsVal); + BoolExpr secondsError = + ctx.mkOr( + ctx.mkNot(typeSystem.isInt(secondsVal)), + isTimestamp + ? typeSystem.checkTimestampOverflow(seconds) + : typeSystem.checkDurationOverflow(seconds)); + + IntExpr nanos = typeSystem.getInt(nanosVal); + BoolExpr nanosError; + if (isTimestamp) { + nanosError = + ctx.mkOr( + ctx.mkNot(typeSystem.isInt(nanosVal)), + ctx.mkLt(nanos, ctx.mkInt(0)), + ctx.mkGe(nanos, ctx.mkInt(1_000_000_000))); + } else { + BoolExpr nanosOutOfRange = + ctx.mkOr( + ctx.mkLt(nanos, ctx.mkInt(-999_999_999)), ctx.mkGe(nanos, ctx.mkInt(1_000_000_000))); + BoolExpr signMismatch = + ctx.mkOr( + ctx.mkAnd(ctx.mkGt(seconds, ctx.mkInt(0)), ctx.mkLt(nanos, ctx.mkInt(0))), + ctx.mkAnd(ctx.mkLt(seconds, ctx.mkInt(0)), ctx.mkGt(nanos, ctx.mkInt(0)))); + nanosError = ctx.mkOr(ctx.mkNot(typeSystem.isInt(nanosVal)), nanosOutOfRange, signMismatch); + } + BoolExpr nanosNonZero = ctx.mkNot(ctx.mkEq(nanos, ctx.mkInt(0))); + BoolExpr subSecondApprox = ctx.mkAnd(ctx.mkNot(nanosError), nanosNonZero); + FuncDecl subSecondOffset = + typeSystem.internFuncDecl( + createStruct.messageName() + "_subsecond", + new Sort[] {ctx.getIntSort(), ctx.getIntSort()}, + ctx.getIntSort()); + IntExpr subSecondTime = (IntExpr) ctx.mkApp(subSecondOffset, seconds, nanos); + IntExpr encodedTime = (IntExpr) ctx.mkITE(subSecondApprox, subSecondTime, seconds); + Expr wrapped = + isTimestamp ? typeSystem.wrapTimestamp(encodedTime) : typeSystem.wrapDuration(encodedTime); + Expr result = typeSystem.withRuntimeError(wrapped, secondsError, nanosError); + TranslatedValue strictResult = + TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, entryTvs); + return TranslatedValue.create( + strictResult.z3Expr(), + celExpr, + typeSystem, + CelZ3TypeSystem.mkOrFlattened(ctx, strictResult.isApproximate(), subSecondApprox)); + } + private Expr getDefaultValueForType(CelType type) { if (type instanceof NullableType) { return typeSystem.mkNull(); diff --git a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java index 85cd29a8e..c2a505216 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -16,6 +16,7 @@ import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.collect.ImmutableList.toImmutableList; import com.google.common.annotations.VisibleForTesting; import com.google.common.collect.ImmutableList; @@ -23,6 +24,7 @@ import com.google.common.collect.ImmutableSet; import com.google.errorprone.annotations.CanIgnoreReturnValue; import com.google.errorprone.annotations.Immutable; +import com.google.protobuf.Descriptors.Descriptor; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; import com.microsoft.z3.Model; @@ -32,6 +34,8 @@ import dev.cel.bundle.Cel; import dev.cel.bundle.CelFactory; import dev.cel.common.CelAbstractSyntaxTree; +import dev.cel.common.internal.DefaultDescriptorPool; +import dev.cel.common.internal.WellKnownProto; import dev.cel.common.types.CelType; import dev.cel.common.types.CelTypeProvider; import dev.cel.optimizer.CelOptimizationException; @@ -64,6 +68,26 @@ public Optional findType(String typeName) { } }; + private static final ImmutableList WELL_KNOWN_DESCRIPTORS = + ImmutableList.of( + WellKnownProto.DURATION, + WellKnownProto.JSON_LIST_VALUE, + WellKnownProto.JSON_STRUCT_VALUE, + WellKnownProto.JSON_VALUE, + WellKnownProto.TIMESTAMP, + WellKnownProto.FLOAT_VALUE, + WellKnownProto.INT32_VALUE, + WellKnownProto.INT64_VALUE, + WellKnownProto.STRING_VALUE, + WellKnownProto.BOOL_VALUE, + WellKnownProto.BYTES_VALUE, + WellKnownProto.DOUBLE_VALUE, + WellKnownProto.UINT32_VALUE, + WellKnownProto.UINT64_VALUE) + .stream() + .map(DefaultDescriptorPool::getWellKnownProtoDescriptor) + .collect(toImmutableList()); + private final Duration timeout; private final int comprehensionUnrollLimit; private final ImmutableSet unknownIdentifiers; @@ -74,7 +98,8 @@ public Optional findType(String typeName) { private final Cel cel; static Builder newBuilder() { - return new Builder(CelFactory.plannerCelBuilder().build()); + return new Builder( + CelFactory.plannerCelBuilder().addMessageTypes(WELL_KNOWN_DESCRIPTORS).build()); } static Builder newBuilder(Cel cel) { @@ -155,7 +180,7 @@ private Builder(Cel cel) { this.comprehensionUnrollLimit = 5; this.unknownIdentifiers = ImmutableSet.builder(); this.functionAxioms = ImmutableList.builder(); - this.typeProvider = EMPTY_TYPE_PROVIDER; + this.typeProvider = cel.getTypeProvider(); this.cel = cel; } } diff --git a/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel index 1d2c7569e..38ceed30a 100644 --- a/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/tools/BUILD.bazel @@ -45,10 +45,11 @@ java_library( "//common:cel_ast", "//common:compiler_common", "//common:options", + "//common/internal:cel_descriptor_pools", + "//common/internal:well_known_proto", "//common/types", "//common/types:cel_types", "//common/types:type_providers", - "//compiler", "//compiler:compiler_builder", "//extensions", "//parser:macro", @@ -64,6 +65,7 @@ java_library( "//verifier:verifier_factory", "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:com_google_guava_guava", + "@maven//:com_google_protobuf_protobuf_java", "@maven//:info_picocli_picocli", ], ) 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 82a93c3d7..ba700e728 100644 --- a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierRepl.java @@ -315,7 +315,7 @@ private static void printHelp(String topic, PrintStream out) { out.println(); out.println("Supported Types:"); out.println(" - Primitive types: int, uint, string, bool, double, bytes, dyn"); - out.println(" - Well-known types: timestamp, duration"); + out.println(" - Well-known types: timestamp, duration, google.protobuf.*"); 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)"); diff --git a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java index 51b7164e4..b75da7e62 100644 --- a/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java +++ b/verifier/src/main/java/dev/cel/verifier/tools/CelVerifierToolCore.java @@ -14,16 +14,20 @@ package dev.cel.verifier.tools; +import static com.google.common.collect.ImmutableList.toImmutableList; + +import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; +import com.google.protobuf.Descriptors.Descriptor; import dev.cel.bundle.Cel; import dev.cel.bundle.CelBuilder; import dev.cel.bundle.CelFactory; import dev.cel.common.CelAbstractSyntaxTree; import dev.cel.common.CelOptions; +import dev.cel.common.internal.DefaultDescriptorPool; +import dev.cel.common.internal.WellKnownProto; import dev.cel.common.types.CelType; import dev.cel.compiler.CelCompiler; -import dev.cel.compiler.CelCompilerBuilder; -import dev.cel.compiler.CelCompilerFactory; import dev.cel.extensions.CelExtensions; import dev.cel.parser.CelStandardMacro; import dev.cel.policy.CelPolicy; @@ -42,6 +46,26 @@ /** Core decoupled engine that executes formal verification operations. */ final class CelVerifierToolCore { + private static final ImmutableList WELL_KNOWN_DESCRIPTORS = + ImmutableList.of( + WellKnownProto.DURATION, + WellKnownProto.JSON_LIST_VALUE, + WellKnownProto.JSON_STRUCT_VALUE, + WellKnownProto.JSON_VALUE, + WellKnownProto.TIMESTAMP, + WellKnownProto.FLOAT_VALUE, + WellKnownProto.INT32_VALUE, + WellKnownProto.INT64_VALUE, + WellKnownProto.STRING_VALUE, + WellKnownProto.BOOL_VALUE, + WellKnownProto.BYTES_VALUE, + WellKnownProto.DOUBLE_VALUE, + WellKnownProto.UINT32_VALUE, + WellKnownProto.UINT64_VALUE) + .stream() + .map(DefaultDescriptorPool::getWellKnownProtoDescriptor) + .collect(toImmutableList()); + private CelVerifierToolCore() {} /** Checks if a single CEL expression is satisfiable. */ @@ -105,35 +129,24 @@ static CelVerificationResult verifyPolicyEquivalence( } static CelCompiler buildCompiler(Map variables) { - CelCompilerBuilder builder = - CelCompilerFactory.standardCelCompilerBuilder() - .setStandardMacros(CelStandardMacro.STANDARD_MACROS) - .addLibraries( - CelExtensions.bindings(), - CelExtensions.comprehensions(), - CelExtensions.encoders(CelOptions.DEFAULT), - CelExtensions.lists(), - CelExtensions.math(), - CelExtensions.optional(), - CelExtensions.protos(), - CelExtensions.regex(), - CelExtensions.sets(CelOptions.DEFAULT), - CelExtensions.strings()); - for (Map.Entry entry : variables.entrySet()) { - builder.addVar(entry.getKey(), entry.getValue()); - } - return builder.build(); + return buildCel(variables); } static Cel buildCel(Map variables) { CelBuilder celBuilder = CelFactory.plannerCelBuilder() .setStandardMacros(CelStandardMacro.STANDARD_MACROS) + .addMessageTypes(WELL_KNOWN_DESCRIPTORS) .addCompilerLibraries( - CelExtensions.optional(), CelExtensions.bindings(), + CelExtensions.comprehensions(), CelExtensions.encoders(CelOptions.DEFAULT), + CelExtensions.lists(), CelExtensions.math(), + CelExtensions.optional(), + CelExtensions.protos(), + CelExtensions.regex(), + CelExtensions.sets(CelOptions.DEFAULT), CelExtensions.strings()); for (Map.Entry entry : variables.entrySet()) { celBuilder.addVar(entry.getKey(), entry.getValue()); 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 6e61a182d..0789b1ff0 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.NullableType; import dev.cel.common.types.OptionalType; import dev.cel.common.types.SimpleType; import java.time.Duration; @@ -211,13 +212,34 @@ static CelType parseCelType(String typeStr) { case "duration": case "google.protobuf.duration": return SimpleType.DURATION; + case "google.protobuf.value": + return SimpleType.DYN; + case "google.protobuf.struct": + return MapType.create(SimpleType.STRING, SimpleType.DYN); + case "google.protobuf.listvalue": + return ListType.create(SimpleType.DYN); + case "google.protobuf.boolvalue": + return NullableType.create(SimpleType.BOOL); + case "google.protobuf.bytesvalue": + return NullableType.create(SimpleType.BYTES); + case "google.protobuf.doublevalue": + case "google.protobuf.floatvalue": + return NullableType.create(SimpleType.DOUBLE); + case "google.protobuf.int32value": + case "google.protobuf.int64value": + return NullableType.create(SimpleType.INT); + case "google.protobuf.uint32value": + case "google.protobuf.uint64value": + return NullableType.create(SimpleType.UINT); + case "google.protobuf.stringvalue": + return NullableType.create(SimpleType.STRING); 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, timestamp," - + " duration, list, map, optional."); + + " duration, google.protobuf.*, list, map, optional."); } } diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 553e39e29..7745b887a 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -132,8 +132,7 @@ public final class CelVerifierZ3ImplTest { TestAllTypes.getDescriptor(), TestAllTypes.NestedMessage.getDescriptor())) .build(); - private static final CelVerifier VERIFIER = - CelVerifierFactory.newVerifier(CEL).setTypeProvider(TYPE_PROVIDER).build(); + private static final CelVerifier VERIFIER = CelVerifierFactory.newVerifier(CEL).build(); @Before public void setUp() { @@ -1866,7 +1865,12 @@ private enum EquivalenceInconclusiveTestCase { "TestAllTypes{single_int64: int_list.all(i, v, i < 5) ? 0 : 1}", "TestAllTypes{single_sint64: int_list.all(i, v, i < 5) ? 0 : 1}"), DYN_RANGE_DIFFERENT_COMPREHENSIONS("dyn_var.all(e, e > 0)", "dyn_var.all(e, e < 0)"), - CHAINED_MAP_ALL_TRUE("int_list.map(x, 1).all(v, v == 1)", "true"); + CHAINED_MAP_ALL_TRUE("int_list.map(x, 1).all(v, v == 1)", "true"), + TIMESTAMP_STRUCT_NONZERO_NANOS( + "google.protobuf.Timestamp{seconds: 100, nanos: 500}", "timestamp(100)"), + DURATION_STRUCT_NONZERO_NANOS( + "google.protobuf.Duration{seconds: 100, nanos: 500}", + "google.protobuf.Duration{seconds: 100}"); private final String exprA; private final String exprB; @@ -2159,6 +2163,59 @@ private enum EquivalenceTestCase { JSON_VALUE_OPTIONAL_NULL_VALUE_NONE( "google.protobuf.Value{?null_value: optional.none()}", "null"), JSON_VALUE_OPTIONAL_NULL_VALUE_OF("google.protobuf.Value{?null_value: optional.of(0)}", "null"), + WRAPPER_INT64_VALUE("google.protobuf.Int64Value{value: 42}", "42"), + WRAPPER_INT64_EMPTY("google.protobuf.Int64Value{}", "0"), + WRAPPER_INT32_VALUE("google.protobuf.Int32Value{value: 42}", "42"), + WRAPPER_INT32_EMPTY("google.protobuf.Int32Value{}", "0"), + WRAPPER_UINT64_VALUE("google.protobuf.UInt64Value{value: 42u}", "42u"), + WRAPPER_UINT64_EMPTY("google.protobuf.UInt64Value{}", "0u"), + WRAPPER_UINT32_VALUE("google.protobuf.UInt32Value{value: 42u}", "42u"), + WRAPPER_UINT32_EMPTY("google.protobuf.UInt32Value{}", "0u"), + WRAPPER_DOUBLE_VALUE("google.protobuf.DoubleValue{value: 1.5}", "1.5"), + WRAPPER_DOUBLE_EMPTY("google.protobuf.DoubleValue{}", "0.0"), + WRAPPER_FLOAT_VALUE("google.protobuf.FloatValue{value: 1.5}", "1.5"), + WRAPPER_FLOAT_EMPTY("google.protobuf.FloatValue{}", "0.0"), + WRAPPER_BOOL_VALUE("google.protobuf.BoolValue{value: true}", "true"), + WRAPPER_BOOL_EMPTY("google.protobuf.BoolValue{}", "false"), + WRAPPER_STRING_VALUE("google.protobuf.StringValue{value: 'hello'}", "'hello'"), + WRAPPER_STRING_EMPTY("google.protobuf.StringValue{}", "''"), + WRAPPER_BYTES_VALUE("google.protobuf.BytesValue{value: b'abc'}", "b'abc'"), + WRAPPER_BYTES_EMPTY("google.protobuf.BytesValue{}", "b''"), + WRAPPER_INT64_OPTIONAL_NONE("google.protobuf.Int64Value{?value: optional.none()}", "0"), + WRAPPER_INT64_OPTIONAL_OF("google.protobuf.Int64Value{?value: optional.of(7)}", "7"), + WRAPPER_INT64_VARIABLE("google.protobuf.Int64Value{value: x}", "x"), + WRAPPER_INT32_BOUNDED_VARIABLE( + "x >= -2147483648 && x <= 2147483647 ? google.protobuf.Int32Value{value: x} == x : true", + "true"), + WRAPPER_UINT32_BOUNDED_VARIABLE( + "u <= 4294967295u ? google.protobuf.UInt32Value{value: u} == u : true", "true"), + TIMESTAMP_STRUCT_EMPTY("google.protobuf.Timestamp{}", "timestamp(0)"), + TIMESTAMP_STRUCT_SECONDS("google.protobuf.Timestamp{seconds: 100}", "timestamp(100)"), + TIMESTAMP_STRUCT_SECONDS_AND_ZERO_NANOS( + "google.protobuf.Timestamp{seconds: 100, nanos: 0}", "timestamp(100)"), + TIMESTAMP_STRUCT_VARIABLE("google.protobuf.Timestamp{seconds: x}", "timestamp(x)"), + TIMESTAMP_STRUCT_OPTIONAL_NONE( + "google.protobuf.Timestamp{?seconds: optional.none()}", "timestamp(0)"), + TIMESTAMP_STRUCT_OPTIONAL_OF( + "google.protobuf.Timestamp{?seconds: optional.of(100)}", "timestamp(100)"), + TIMESTAMP_STRUCT_OPTIONAL_NANOS_NONE( + "google.protobuf.Timestamp{seconds: 100, ?nanos: optional.none()}", "timestamp(100)"), + DURATION_STRUCT_EMPTY("google.protobuf.Duration{}", "timestamp(0) - timestamp(0)"), + DURATION_STRUCT_SECONDS( + "google.protobuf.Duration{seconds: 100}", "timestamp(200) - timestamp(100)"), + DURATION_STRUCT_SECONDS_AND_ZERO_NANOS( + "google.protobuf.Duration{seconds: 100, nanos: 0}", "timestamp(200) - timestamp(100)"), + DURATION_STRUCT_OPTIONAL_NONE( + "google.protobuf.Duration{?seconds: optional.none()}", "google.protobuf.Duration{}"), + DURATION_STRUCT_OPTIONAL_OF( + "google.protobuf.Duration{?seconds: optional.of(50)}", + "google.protobuf.Duration{seconds: 50}"), + JSON_VALUE_OPTIONAL_DYN_NON_OPTIONAL_ERROR( + "google.protobuf.Value{?string_value: dyn('hello')} == null", "1 / 0 == 1"), + WRAPPER_OPTIONAL_DYN_NON_OPTIONAL_ERROR( + "google.protobuf.Int64Value{?value: dyn(42)} == 0", "1 / 0 == 1"), + TIMESTAMP_STRUCT_OPTIONAL_DYN_NON_OPTIONAL_ERROR( + "google.protobuf.Timestamp{?seconds: dyn(100)} == timestamp(0)", "1 / 0 == 1"), OPTIONAL_INDEX_LIST_UNWRAPPING("optional.of([1, 2, 3])[?0]", "optional.of(1)"), OPTIONAL_INDEX_MAP_UNWRAPPING("optional.of({'a': 1})[?'a']", "optional.of(1)"), OPTIONAL_INDEX_UNWRAPPING_NONE("optional.none()[?0]", "optional.none()"), @@ -2259,7 +2316,30 @@ private enum EquivalenceViolationTestCase { "TestAllTypes{single_int64_wrapper: 0}.?single_int64_wrapper", "optional.none()"), OPTIONAL_DYNAMIC_TARGET_TYPE_MISMATCH("dyn_var.?a == optional.none()", "false"), OPTIONAL_NESTED_NONE_VS_MISSING( - "{'a': optional.none()}.?a.orValue(optional.of(1))", "optional.of(1)"); + "{'a': optional.none()}.?a.orValue(optional.of(1))", "optional.of(1)"), + WRAPPER_INT32_UNBOUNDED_OVERFLOW("google.protobuf.Int32Value{value: x}", "x"), + WRAPPER_UINT32_UNBOUNDED_OVERFLOW("google.protobuf.UInt32Value{value: u}", "u"), + WRAPPER_INT64_DYN_NULL_FAILS("google.protobuf.Int64Value{value: dyn(null)} == null", "true"), + TIMESTAMP_STRUCT_DYN_NON_INT_FAILS( + "google.protobuf.Timestamp{seconds: dyn('bad')} == timestamp(0)", "false"), + TIMESTAMP_STRUCT_NANOS_DYN_NON_INT_FAILS( + "google.protobuf.Timestamp{seconds: 0, nanos: dyn('bad')} == timestamp(0)", "false"), + TIMESTAMP_STRUCT_NANOS_NEGATIVE_FAILS( + "google.protobuf.Timestamp{seconds: 0, nanos: -1} == timestamp(0)", "false"), + TIMESTAMP_STRUCT_NANOS_TOO_LARGE_FAILS( + "google.protobuf.Timestamp{seconds: 0, nanos: 1000000000} == timestamp(0)", "false"), + DURATION_STRUCT_SECONDS_OVERFLOW_FAILS( + "google.protobuf.Duration{seconds: 315576000001} == google.protobuf.Duration{}", "false"), + DURATION_STRUCT_NANOS_TOO_SMALL_FAILS( + "google.protobuf.Duration{seconds: 0, nanos: -1000000000} == google.protobuf.Duration{}", + "false"), + DURATION_STRUCT_NANOS_TOO_LARGE_FAILS( + "google.protobuf.Duration{seconds: 0, nanos: 1000000000} == google.protobuf.Duration{}", + "false"), + DURATION_STRUCT_SIGN_MISMATCH_POS_NEG_FAILS( + "google.protobuf.Duration{seconds: 1, nanos: -1} == google.protobuf.Duration{}", "false"), + DURATION_STRUCT_SIGN_MISMATCH_NEG_POS_FAILS( + "google.protobuf.Duration{seconds: -1, nanos: 1} == google.protobuf.Duration{}", "false"); final String exprA; final String exprB; 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 cbe5fffd5..896972dd4 100644 --- a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierReplTest.java @@ -84,7 +84,7 @@ 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("Well-known types: timestamp, duration, google.protobuf.*"); assertThat(output[0]).contains("Optional types: optional"); assertThat(output[0]).contains("Protobuf types: coming soon"); } 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 2d01e7a0f..900ce82ae 100644 --- a/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java +++ b/verifier/src/test/java/dev/cel/verifier/tools/CelVerifierToolTest.java @@ -223,7 +223,7 @@ public void parseVariables_unsupportedType_throws() { .hasMessageThat() .contains( "Supported types: int, uint, string, bool, double, bytes, dyn, timestamp," - + " duration, list, map, optional."); + + " duration, google.protobuf.*, list, map, optional."); } @Test @@ -328,6 +328,61 @@ public void verifyEquivalence_canonicalizedMapComprehension() throws Exception { assertThat(result.status()).isEqualTo(VerificationStatus.VERIFIED); } + @Test + public void verifyEquivalence_wellKnownTypesSupportedByDefault() throws Exception { + VerificationOptions options = + VerificationOptions.builder().setTimeout(Duration.ofSeconds(5)).build(); + ImmutableMap vars = + VerificationOptions.parseVariables( + Arrays.asList("x:int", "w:google.protobuf.Int64Value", "s:google.protobuf.Struct")); + + assertThat( + CelVerifierToolCore.verifyEquivalence( + "google.protobuf.Struct{fields: {'a': google.protobuf.Value{number_value: 1.0}," + + " ?'b': optional.none()}}", + "{'a': 1.0}", + vars, + options) + .status()) + .isEqualTo(VerificationStatus.VERIFIED); + assertThat( + CelVerifierToolCore.verifyEquivalence( + "google.protobuf.ListValue{values: [google.protobuf.Value{string_value: 'x'}]}", + "['x']", + vars, + options) + .status()) + .isEqualTo(VerificationStatus.VERIFIED); + assertThat( + CelVerifierToolCore.verifyEquivalence( + "google.protobuf.Int64Value{value: x} == x" + + " && google.protobuf.Int64Value{} == 0" + + " && google.protobuf.StringValue{value: 'hi'} == 'hi'", + "true", + vars, + options) + .status()) + .isEqualTo(VerificationStatus.VERIFIED); + assertThat( + CelVerifierToolCore.verifyEquivalence( + "google.protobuf.Timestamp{seconds: 100} == timestamp(100)" + + " && google.protobuf.Duration{seconds: 50}" + + " == timestamp(150) - timestamp(100)", + "true", + vars, + options) + .status()) + .isEqualTo(VerificationStatus.VERIFIED); + assertThat( + CelVerifierToolCore.verifyEquivalence( + "w == null || w == google.protobuf.Int64Value{value: w}", + "true", + vars, + options) + .status()) + .isEqualTo(VerificationStatus.VERIFIED); + } + @Test public void verifyPolicyInvariants_success() throws Exception { String yamlPolicy = 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 e52868ea0..1a8512b93 100644 --- a/verifier/src/test/java/dev/cel/verifier/tools/VerificationOptionsTest.java +++ b/verifier/src/test/java/dev/cel/verifier/tools/VerificationOptionsTest.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.NullableType; import dev.cel.common.types.OptionalType; import dev.cel.common.types.SimpleType; import dev.cel.verifier.tools.VerificationOptions.OutputFormat; @@ -123,6 +124,33 @@ public void parseCelType_timestampAndDuration() { .isEqualTo(SimpleType.DURATION); } + @Test + public void parseCelType_wellKnownTypes() { + assertThat(VerificationOptions.parseCelType("google.protobuf.Value")).isEqualTo(SimpleType.DYN); + assertThat(VerificationOptions.parseCelType("google.protobuf.Struct")) + .isEqualTo(MapType.create(SimpleType.STRING, SimpleType.DYN)); + assertThat(VerificationOptions.parseCelType("google.protobuf.ListValue")) + .isEqualTo(ListType.create(SimpleType.DYN)); + assertThat(VerificationOptions.parseCelType("google.protobuf.BoolValue")) + .isEqualTo(NullableType.create(SimpleType.BOOL)); + assertThat(VerificationOptions.parseCelType("google.protobuf.BytesValue")) + .isEqualTo(NullableType.create(SimpleType.BYTES)); + assertThat(VerificationOptions.parseCelType("google.protobuf.DoubleValue")) + .isEqualTo(NullableType.create(SimpleType.DOUBLE)); + assertThat(VerificationOptions.parseCelType("google.protobuf.FloatValue")) + .isEqualTo(NullableType.create(SimpleType.DOUBLE)); + assertThat(VerificationOptions.parseCelType("google.protobuf.Int32Value")) + .isEqualTo(NullableType.create(SimpleType.INT)); + assertThat(VerificationOptions.parseCelType("google.protobuf.Int64Value")) + .isEqualTo(NullableType.create(SimpleType.INT)); + assertThat(VerificationOptions.parseCelType("google.protobuf.UInt32Value")) + .isEqualTo(NullableType.create(SimpleType.UINT)); + assertThat(VerificationOptions.parseCelType("google.protobuf.UInt64Value")) + .isEqualTo(NullableType.create(SimpleType.UINT)); + assertThat(VerificationOptions.parseCelType("google.protobuf.StringValue")) + .isEqualTo(NullableType.create(SimpleType.STRING)); + } + @Test public void parseCelType_optionalTypes() { assertThat(VerificationOptions.parseCelType("optional")) @@ -174,6 +202,6 @@ public void parseVariables_unsupportedType_throwsException() { .hasMessageThat() .contains( "Supported types: int, uint, string, bool, double, bytes, dyn, timestamp," - + " duration, list, map, optional."); + + " duration, google.protobuf.*, list, map, optional."); } }