From 721350779255e4525d58f0548e23ad3231dd72de 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 | 148 ++++++++++++- .../dev/cel/verifier/CelVerifierZ3Impl.java | 29 ++- .../CelZ3CounterexampleGenerator.java | 31 ++- .../dev/cel/verifier/CelZ3TypeSystem.java | 35 ++- .../cel/verifier/axioms/OptionalAxioms.java | 2 + .../verifier/axioms/TypeConversionAxioms.java | 14 +- .../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 | 200 +++++++++++++++++- .../verifier/tools/CelVerifierReplTest.java | 2 +- .../verifier/tools/CelVerifierToolTest.java | 57 ++++- .../tools/VerificationOptionsTest.java | 30 ++- 15 files changed, 585 insertions(+), 51 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..6491a83a4 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -22,6 +22,7 @@ import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Context; import com.microsoft.z3.Expr; +import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; import com.microsoft.z3.Quantifier; @@ -82,6 +83,9 @@ final class CelAstToZ3Translator { private static final String EMPTY_LIST_PREFIX = "!empty_list"; private static final String EMPTY_MAP_PREFIX = "!empty_map"; private static final String NULL_VALUE_FIELD = "null_value"; + private static final String SECONDS_FIELD = "seconds"; + private static final long MAX_UINT32 = 0xFFFFFFFFL; + private static final int MIN_DURATION_NANOS = -999_999_999; private final Context ctx; private final CelZ3TypeSystem typeSystem; private final CelZ3OperatorTranslator operatorTranslator; @@ -401,6 +405,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 +527,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 +548,129 @@ 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(MAX_UINT32))); + } else if (typeName.equals(CelTypes.FLOAT_WRAPPER_MESSAGE)) { + FPExpr doubleVal = typeSystem.getDouble(currentVal); + FPExpr narrowedFloat = + ctx.mkFPToFP(ctx.mkFPRoundNearestTiesToEven(), doubleVal, ctx.mkFPSortSingle()); + FPExpr widenedDouble = + ctx.mkFPToFP(ctx.mkFPRoundNearestTiesToEven(), narrowedFloat, ctx.mkFPSortDouble()); + currentVal = typeSystem.wrapDouble(widenedDouble); + } + 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_FIELD)) { + secondsVal = ctx.mkITE(hasValue, unpackedVal, secondsVal); + } else { + nanosVal = ctx.mkITE(hasValue, unpackedVal, nanosVal); + } + entryTvs.add(entryTv); + } + + IntExpr seconds = typeSystem.getInt(secondsVal); + IntExpr nanos = typeSystem.getInt(nanosVal); + IntExpr totalNanos = + (IntExpr) + ctx.mkAdd(ctx.mkMul(seconds, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)), nanos); + + BoolExpr typeError = + ctx.mkOr(ctx.mkNot(typeSystem.isInt(secondsVal)), ctx.mkNot(typeSystem.isInt(nanosVal))); + BoolExpr rangeError; + if (isTimestamp) { + BoolExpr nanosOutOfRange = + ctx.mkOr( + ctx.mkLt(nanos, ctx.mkInt(0)), + ctx.mkGe(nanos, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND))); + rangeError = ctx.mkOr(nanosOutOfRange, typeSystem.checkTimestampOverflow(totalNanos)); + } else { + BoolExpr nanosOutOfRange = + ctx.mkOr( + ctx.mkLt(nanos, ctx.mkInt(MIN_DURATION_NANOS)), + ctx.mkGe(nanos, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND))); + 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)))); + rangeError = + ctx.mkOr(nanosOutOfRange, signMismatch, typeSystem.checkDurationOverflow(totalNanos)); + } + Expr wrapped = + isTimestamp ? typeSystem.wrapTimestamp(totalNanos) : typeSystem.wrapDuration(totalNanos); + Expr result = typeSystem.withRuntimeError(wrapped, typeError, rangeError); + return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, entryTvs); + } + private Expr getDefaultValueForType(CelType type) { if (type instanceof NullableType) { return typeSystem.mkNull(); @@ -1326,14 +1464,14 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { return typeSystem.isBytes(val); } if (type.equals(SimpleType.TIMESTAMP)) { - IntExpr seconds = typeSystem.getTimestamp(val); + IntExpr nanos = typeSystem.getTimestamp(val); return ctx.mkAnd( - typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(seconds))); + typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(nanos))); } if (type.equals(SimpleType.DURATION)) { - IntExpr seconds = typeSystem.getDuration(val); + IntExpr nanos = typeSystem.getDuration(val); return ctx.mkAnd( - typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(seconds))); + typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(nanos))); } if (type instanceof ListType) { 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/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index cef976608..22d7b8a42 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -23,6 +23,7 @@ import com.microsoft.z3.IntNum; import com.microsoft.z3.Model; import com.microsoft.z3.RatNum; +import java.math.BigInteger; import java.util.ArrayList; import java.util.HashSet; import java.util.LinkedHashSet; @@ -86,9 +87,9 @@ private static String formatExpr( if (decl.equals(typeSystem.intCons().ConstructorDecl())) { return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]); } else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) { - return "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")"; + return formatTimestamp(expr.getArgs()[0]); } else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) { - return "duration('" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "s')"; + return formatDuration(expr.getArgs()[0]); } else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) { return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u"; } else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) { @@ -154,6 +155,32 @@ private static String formatExpr( return expr.toString(); } + private static String formatTimestamp(Expr nanosExpr) { + BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger(); + BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND); + BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond); + BigInteger seconds = divRem[0]; + BigInteger nanos = divRem[1]; + if (nanos.signum() < 0) { + seconds = seconds.subtract(BigInteger.ONE); + nanos = nanos.add(nanosPerSecond); + } + if (nanos.equals(BigInteger.ZERO)) { + return "timestamp(" + seconds + ")"; + } + return "google.protobuf.Timestamp{seconds: " + seconds + ", nanos: " + nanos + "}"; + } + + private static String formatDuration(Expr nanosExpr) { + BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger(); + BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND); + BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond); + if (divRem[1].equals(BigInteger.ZERO)) { + return "duration('" + divRem[0] + "s')"; + } + return "duration('" + totalNanos + "ns')"; + } + private static String reconstructList( Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr listRef) { Expr lenExpr = diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index 666a5c0d4..2fa9965d6 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -35,6 +35,7 @@ import com.microsoft.z3.SeqSort; import com.microsoft.z3.Sort; import dev.cel.common.internal.ProtoTimeUtils; +import java.math.BigInteger; import java.util.ArrayList; import java.util.Arrays; import java.util.HashMap; @@ -56,6 +57,22 @@ @SuppressWarnings({"unchecked", "rawtypes", "AvoidObjectArrays"}) // Z3 Java API uses raw types. public final class CelZ3TypeSystem { + /** Number of nanoseconds per second. */ + public static final long NANOS_PER_SECOND = 1_000_000_000L; + + private static final long MAX_TIMESTAMP_NANOS_PART = 999_999_999L; + + private static final String MIN_TIMESTAMP_NANOS = + BigInteger.valueOf(ProtoTimeUtils.TIMESTAMP_SECONDS_MIN) + .multiply(BigInteger.valueOf(NANOS_PER_SECOND)) + .toString(); + + private static final String MAX_TIMESTAMP_NANOS = + BigInteger.valueOf(ProtoTimeUtils.TIMESTAMP_SECONDS_MAX) + .multiply(BigInteger.valueOf(NANOS_PER_SECOND)) + .add(BigInteger.valueOf(MAX_TIMESTAMP_NANOS_PART)) + .toString(); + private static final String TYPE_CEL_VALUE = "CelValue"; private static final String CONS_BOOL = "Bool"; private static final String IS_BOOL = "isBool"; @@ -777,18 +794,22 @@ public BoolExpr checkIntOverflow(ArithExpr result) { ctx.mkLt(result, ctx.mkInt(CelNumericBounds.MIN_INT64))); } - /** Checks if the given arithmetic expression overflows CEL Timestamp bounds. */ + /** + * Checks if the given nanosecond arithmetic expression overflows CEL Timestamp bounds + * ({@code [0001-01-01T00:00:00Z, 9999-12-31T23:59:59.999999999Z]}). + */ public BoolExpr checkTimestampOverflow(ArithExpr result) { return ctx.mkOr( - ctx.mkGt(result, ctx.mkInt(ProtoTimeUtils.TIMESTAMP_SECONDS_MAX)), - ctx.mkLt(result, ctx.mkInt(ProtoTimeUtils.TIMESTAMP_SECONDS_MIN))); + ctx.mkGt(result, ctx.mkInt(MAX_TIMESTAMP_NANOS)), + ctx.mkLt(result, ctx.mkInt(MIN_TIMESTAMP_NANOS))); } - /** Checks if the given arithmetic expression overflows CEL Duration bounds. */ + /** + * Checks if the given nanosecond arithmetic expression overflows CEL Duration bounds, which are + * confined to a signed 64-bit integer of nanoseconds (matching Go's {@code time.Duration}). + */ public BoolExpr checkDurationOverflow(ArithExpr result) { - return ctx.mkOr( - ctx.mkGt(result, ctx.mkInt(ProtoTimeUtils.DURATION_SECONDS_MAX)), - ctx.mkLt(result, ctx.mkInt(ProtoTimeUtils.DURATION_SECONDS_MIN))); + return checkIntOverflow(result); } /** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */ diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java index 49f2d7450..35f96b7ef 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java @@ -153,6 +153,8 @@ private static BoolExpr isZeroValue(Context ctx, CelZ3TypeSystem ts, Expr val ctx.mkAnd(ts.isInt(val), ctx.mkEq(ts.getInt(val), ctx.mkInt(0))), ctx.mkAnd(ts.isUint(val), ctx.mkEq(ts.getUint(val), ctx.mkInt(0))), ctx.mkAnd(ts.isDouble(val), ctx.mkFPIsZero((FPExpr) ts.getDouble(val))), + ctx.mkAnd(ts.isTimestamp(val), ctx.mkEq(ts.getTimestamp(val), ctx.mkInt(0))), + ctx.mkAnd(ts.isDuration(val), ctx.mkEq(ts.getDuration(val), ctx.mkInt(0))), ctx.mkAnd(ts.isString(val), ctx.mkEq(ts.getString(val), ctx.mkString(""))), ctx.mkAnd( ts.isBytes(val), ctx.mkEq(ctx.mkLength((SeqExpr) ts.getBytes(val)), ctx.mkInt(0))), diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java index 2064047fd..70f08f3f3 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java @@ -25,6 +25,7 @@ import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Conversions; import dev.cel.common.types.SimpleType; +import dev.cel.verifier.CelZ3TypeSystem; import java.util.Optional; /** Axiomatization for CEL's type conversion functions. */ @@ -52,7 +53,12 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.TIMESTAMP_TO_INT64.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> - Optional.of(typeSystem.wrapInt(typeSystem.getTimestamp(arg)))) + Optional.of( + typeSystem.wrapInt( + (IntExpr) + ctx.mkDiv( + typeSystem.getTimestamp(arg), + ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND))))) .build(); private static final CelZ3FunctionAxiom UINT_AXIOM = @@ -159,9 +165,11 @@ final class TypeConversionAxioms { Conversions.INT64_TO_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> { IntExpr intVal = typeSystem.getInt(arg); - BoolExpr overflow = typeSystem.checkTimestampOverflow(intVal); + IntExpr nanosVal = + (IntExpr) ctx.mkMul(intVal, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)); + BoolExpr overflow = typeSystem.checkTimestampOverflow(nanosVal); return Optional.of( - typeSystem.withRuntimeError(typeSystem.wrapTimestamp(intVal), overflow)); + typeSystem.withRuntimeError(typeSystem.wrapTimestamp(nanosVal), overflow)); }) .build(); 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..21c3c5812 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() { @@ -195,6 +194,15 @@ private enum IsSatisfiableTestCase { "size(nested_list) == 6 && dyn(nested_list[0]) == [1]", "nested_list = \\[\\[1\\]"), DYN_CONDITIONAL_EQUALITY_WITH_LONG_LIST_BRANCH( "size(int_list) == 6 && dyn(b ? [1] : int_list) == [1]", "b = true"), + TIMESTAMP_SUBSECOND_SATISFIABLE( + "ts == google.protobuf.Timestamp{seconds: 10, nanos: 500}", + "ts = google\\.protobuf\\.Timestamp\\{seconds: 10, nanos: 500\\}"), + TIMESTAMP_NEGATIVE_SUBSECOND_SATISFIABLE( + "ts == google.protobuf.Timestamp{seconds: -1, nanos: 500}", + "ts = google\\.protobuf\\.Timestamp\\{seconds: -1, nanos: 500\\}"), + DURATION_SUBSECOND_SATISFIABLE( + "dur == google.protobuf.Duration{seconds: 1, nanos: 500}", + "dur = duration\\('1000000500ns'\\)"), ; private final String expr; @@ -558,7 +566,13 @@ private enum IsAlwaysTrueTestCase { DURATION_LESS("(timestamp(150) - timestamp(100)) < (timestamp(200) - timestamp(100))"), TIMESTAMP_VARIABLE_TYPE("type(ts) == type(timestamp(0))"), DURATION_VARIABLE_TYPE("type(dur) == type(timestamp(1) - timestamp(0))"), - TIMESTAMP_VARIABLE_BOUNDS("ts >= timestamp(-62135596800) && ts <= timestamp(253402300799)"), + TIMESTAMP_VARIABLE_BOUNDS( + "ts >= timestamp(-62135596800) && ts <= google.protobuf.Timestamp{seconds: 253402300799," + + " nanos: 999999999}"), + TIMESTAMP_VARIABLE_SECONDS_BOUNDS("int(ts) >= -62135596800 && int(ts) <= 253402300799"), + DURATION_VARIABLE_BOUNDS( + "dur >= google.protobuf.Duration{seconds: -9223372036, nanos: -854775808} && dur <=" + + " google.protobuf.Duration{seconds: 9223372036, nanos: 854775807}"), CYCLIC_MACRO_SHADOWING_SAFETY("[1].all(x, [x].all(x, x == 1))"), TAUTOLOGY("x > 5 || x <= 5"), LIST_VARIABLE_CONSTRAINED("1 in int_list || !(1 in int_list)"), @@ -1908,7 +1922,8 @@ private enum EquivalenceTestCase { "[1, 2, 3].exists_one(x, x == 2)", "(1 == 2 ? 1 : 0) + (2 == 2 ? 1 : 0) + (3 == 2 ? 1 : 0) == 1"), TIMESTAMP_CONVERSION_OVERFLOW_EQUIVALENCE( - "timestamp(string_var) <= timestamp(253402300799)", + "timestamp(string_var) <= google.protobuf.Timestamp{seconds: 253402300799, nanos:" + + " 999999999}", "timestamp(string_var) == timestamp(string_var)"), TIMESTAMP_MATH_SUBTRACT_TS( "timestamp(900000) - timestamp(100)", "timestamp(899900) - timestamp(0)"), @@ -2159,6 +2174,128 @@ 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"), + WRAPPER_FLOAT_EXACT_MAX_VALUE( + "google.protobuf.FloatValue{value: 3.4028234663852886e38}", "3.4028234663852886e38"), + WRAPPER_FLOAT_EXACT_MIN_VALUE( + "google.protobuf.FloatValue{value: -3.4028234663852886e38}", "-3.4028234663852886e38"), + WRAPPER_FLOAT_PRECISION_LOSS_WIDENED( + "google.protobuf.FloatValue{value: 0.1}", "0.10000000149011612"), + WRAPPER_FLOAT_PRECISION_LOSS_NOT_EQUAL_ORIGINAL( + "google.protobuf.FloatValue{value: 0.1} == 0.1", "false"), + WRAPPER_FLOAT_IDEMPOTENT_LITERAL( + "google.protobuf.FloatValue{value: google.protobuf.FloatValue{value: 0.1}}", + "google.protobuf.FloatValue{value: 0.1}"), + WRAPPER_FLOAT_SYMBOLIC_EXACT_VALUE( + "d == 1.5 ? google.protobuf.FloatValue{value: d} == d : true", "true"), + WRAPPER_FLOAT_OVERFLOW_TO_POSITIVE_INFINITY( + "google.protobuf.FloatValue{value: 1.0e39} == 1.0e39", "false"), + WRAPPER_FLOAT_OVERFLOW_TO_NEGATIVE_INFINITY( + "google.protobuf.FloatValue{value: -1.0e39} == -1.0e39", "false"), + WRAPPER_FLOAT_UNDERFLOW_TO_ZERO("google.protobuf.FloatValue{value: 1.0e-46} == 0.0", "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}"), + TIMESTAMP_STRUCT_NANOS_ADD_DURATION( + "google.protobuf.Timestamp{seconds: 100, nanos: 500} + google.protobuf.Duration{nanos:" + + " 500}", + "google.protobuf.Timestamp{seconds: 100, nanos: 1000}"), + TIMESTAMP_STRUCT_NANOS_CARRY_SECOND( + "google.protobuf.Timestamp{seconds: 100, nanos: 600000000} +" + + " google.protobuf.Duration{nanos: 400000000}", + "timestamp(101)"), + TIMESTAMP_STRUCT_SUBTRACT_NANOS( + "google.protobuf.Timestamp{seconds: 10, nanos: 500} - timestamp(10)", + "google.protobuf.Duration{nanos: 500}"), + TIMESTAMP_STRUCT_TO_INT_TRUNCATES_POSITIVE_NANOS( + "int(google.protobuf.Timestamp{seconds: 100, nanos: 999999999})", "100"), + TIMESTAMP_STRUCT_TO_INT_FLOORS_NEGATIVE_SECONDS( + "int(google.protobuf.Timestamp{seconds: -1, nanos: 500000000})", "-1"), + DURATION_STRUCT_MAX_GO_DURATION_VALID( + "google.protobuf.Duration{seconds: 9223372036, nanos: 854775807} >" + + " google.protobuf.Duration{}", + "true"), + DURATION_STRUCT_MIN_GO_DURATION_VALID( + "google.protobuf.Duration{seconds: -9223372036, nanos: -854775808} <" + + " google.protobuf.Duration{}", + "true"), + TIMESTAMP_STRUCT_MIN_VALID( + "google.protobuf.Timestamp{seconds: -62135596800, nanos: 0}", "timestamp(-62135596800)"), + TIMESTAMP_STRUCT_MAX_VALID( + "google.protobuf.Timestamp{seconds: 253402300799, nanos: 999999999} >" + + " timestamp(253402300799)", + "true"), + DURATION_STRUCT_MIN_NANOS_VALID( + "google.protobuf.Duration{seconds: -1, nanos: -999999999} <" + + " google.protobuf.Duration{seconds: -1}", + "true"), + DURATION_STRUCT_MAX_NANOS_VALID( + "google.protobuf.Duration{seconds: 1, nanos: 999999999} >" + + " google.protobuf.Duration{seconds: 1}", + "true"), + DURATION_STRUCT_ZERO_SECONDS_NEGATIVE_NANOS_VALID( + "google.protobuf.Duration{seconds: 0, nanos: -1} < google.protobuf.Duration{}", "true"), + DURATION_STRUCT_NEGATIVE_SECONDS_ZERO_NANOS_VALID( + "google.protobuf.Duration{seconds: -1, nanos: 0} < google.protobuf.Duration{}", "true"), + OPTIONAL_OF_NON_ZERO_VALUE_TIMESTAMP_ZERO( + "optional.ofNonZeroValue(google.protobuf.Timestamp{})", "optional.none()"), + OPTIONAL_OF_NON_ZERO_VALUE_TIMESTAMP_NANOS( + "optional.ofNonZeroValue(google.protobuf.Timestamp{nanos: 1})", + "optional.of(google.protobuf.Timestamp{nanos: 1})"), + OPTIONAL_OF_NON_ZERO_VALUE_DURATION_ZERO( + "optional.ofNonZeroValue(google.protobuf.Duration{})", "optional.none()"), + OPTIONAL_OF_NON_ZERO_VALUE_DURATION_NANOS( + "optional.ofNonZeroValue(google.protobuf.Duration{nanos: 1})", + "optional.of(google.protobuf.Duration{nanos: 1})"), + 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 +2396,60 @@ 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_FLOAT_UNBOUNDED_OVERFLOW("google.protobuf.FloatValue{value: d}", "d"), + WRAPPER_FLOAT_PRECISION_LOSS_VIOLATION("google.protobuf.FloatValue{value: 0.1}", "0.1"), + WRAPPER_FLOAT_BOUNDED_VARIABLE_PRECISION_LOSS( + "d >= -3.4028234663852886e38 && d <= 3.4028234663852886e38 ?" + + " google.protobuf.FloatValue{value: d} == d : true", + "true"), + WRAPPER_FLOAT_DYN_NON_DOUBLE_FAILS( + "google.protobuf.FloatValue{value: dyn('bad')} == 0.0", "false"), + 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"), + 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}"), + TIMESTAMP_VARIABLE_NOT_BOUNDED_BY_WHOLE_SECONDS("ts <= timestamp(253402300799)", "true"), + TIMESTAMP_STRUCT_BELOW_MIN_FAILS( + "google.protobuf.Timestamp{seconds: -62135596801, nanos: 999999999} == timestamp(0)", + "false"), + TIMESTAMP_STRUCT_ABOVE_MAX_FAILS( + "google.protobuf.Timestamp{seconds: 253402300800, nanos: 0} == timestamp(0)", "false"), + DURATION_STRUCT_EXCEEDS_MAX_GO_DURATION_FAILS( + "google.protobuf.Duration{seconds: 9223372036, nanos: 854775808} ==" + + " google.protobuf.Duration{}", + "false"), + DURATION_STRUCT_EXCEEDS_MIN_GO_DURATION_FAILS( + "google.protobuf.Duration{seconds: -9223372036, nanos: -854775809} ==" + + " google.protobuf.Duration{}", + "false"), + TIMESTAMP_SUBTRACT_EXCEEDS_GO_DURATION_FAILS( + "(timestamp(253402300799) - timestamp(-62135596800)) == 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."); } }