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/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;