diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 2e8711883..64cf80a99 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -17,6 +17,7 @@ import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; +import com.google.common.collect.Streams; import com.microsoft.z3.ArithExpr; import com.microsoft.z3.ArrayExpr; import com.microsoft.z3.BoolExpr; @@ -83,6 +84,8 @@ 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 String NANOS_FIELD = "nanos"; private static final long MAX_UINT32 = 0xFFFFFFFFL; private final Context ctx; private final CelZ3TypeSystem typeSystem; @@ -406,7 +409,12 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a if (CelTypes.isWrapperType(createStruct.messageName())) { return translateWrapperWktStruct(celExpr, createStruct, ast); } - // TODO: Support google.protobuf.Timestamp and google.protobuf.Duration. + if (createStruct.messageName().equals(CelTypes.TIMESTAMP_MESSAGE)) { + return translateTimestampWktStruct(celExpr, createStruct, ast); + } + if (createStruct.messageName().equals(CelTypes.DURATION_MESSAGE)) { + return translateDurationWktStruct(celExpr, createStruct, ast); + } // Bypass SMT when the struct is empty (return the cached SMT default pointer) if (createStruct.entries().isEmpty()) { @@ -599,6 +607,105 @@ private TranslatedValue translateWrapperWktStruct( return TranslatedValue.propagateStrict(ctx, typeSystem, currentVal, celExpr, entryTvs); } + @FunctionalInterface + private interface TimeWktValueFactory { + Expr create(IntExpr seconds, IntExpr nanos, IntExpr totalNanos); + } + + private TranslatedValue translateTimestampWktStruct( + CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) { + return translateTimeWktStruct( + celExpr, + createStruct, + ast, + /* minNanos= */ 0, + (seconds, nanos, totalNanos) -> + typeSystem.withRuntimeError( + typeSystem.wrapTimestamp(totalNanos), + typeSystem.checkTimestampOverflow(totalNanos))); + } + + private TranslatedValue translateDurationWktStruct( + CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) { + return translateTimeWktStruct( + celExpr, + createStruct, + ast, + CelZ3TypeSystem.MIN_DURATION_NANOS, + (seconds, nanos, totalNanos) -> { + 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)))); + return typeSystem.withRuntimeError( + typeSystem.wrapDuration(totalNanos), + signMismatch, + typeSystem.checkDurationOverflow(totalNanos)); + }); + } + + private TranslatedValue translateTimeWktStruct( + CelExpr celExpr, + CelExpr.CelStruct createStruct, + CelAbstractSyntaxTree ast, + int minNanos, + TimeWktValueFactory valueFactory) { + List entryTvs = new ArrayList<>(); + Expr secondsVal = + resolveStructFieldValue(createStruct, SECONDS_FIELD, typeSystem.mkInt(0), ast, entryTvs); + Expr nanosVal = + resolveStructFieldValue(createStruct, NANOS_FIELD, typeSystem.mkInt(0), ast, entryTvs); + + 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 nanosOutOfRange = + ctx.mkOr( + ctx.mkLt(nanos, ctx.mkInt(minNanos)), + ctx.mkGe(nanos, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND))); + + Expr result = + typeSystem.withRuntimeError( + valueFactory.create(seconds, nanos, totalNanos), typeError, nanosOutOfRange); + return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, entryTvs); + } + + private Expr resolveStructFieldValue( + CelExpr.CelStruct createStruct, + String fieldName, + Expr defaultValue, + CelAbstractSyntaxTree ast, + List entryTvs) { + return Streams.findLast( + createStruct.entries().stream().filter(entry -> entry.fieldKey().equals(fieldName))) + .>map( + entry -> { + 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); + val = + ctx.mkITE( + typeSystem.optHasValue(optRef), + typeSystem.getOptionalValue(optRef), + defaultValue); + } + entryTvs.add(entryTv); + return val; + }) + .orElse(defaultValue); + } + private Expr getDefaultValueForType(CelType type) { if (type instanceof NullableType) { return typeSystem.mkNull(); @@ -1392,14 +1499,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 439dd6c21..c2a505216 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java +++ b/verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java @@ -70,10 +70,11 @@ public Optional findType(String typeName) { private static final ImmutableList WELL_KNOWN_DESCRIPTORS = ImmutableList.of( - // TODO: Support WellKnownProto.DURATION and WellKnownProto.TIMESTAMP. + WellKnownProto.DURATION, WellKnownProto.JSON_LIST_VALUE, WellKnownProto.JSON_STRUCT_VALUE, WellKnownProto.JSON_VALUE, + WellKnownProto.TIMESTAMP, WellKnownProto.FLOAT_VALUE, WellKnownProto.INT32_VALUE, WellKnownProto.INT64_VALUE, 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..1a341f64d 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,25 @@ @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; + + /** Minimum valid nanosecond component for a protobuf Duration. */ + public static final int MIN_DURATION_NANOS = -999_999_999; + + 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 +797,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/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 7ac9e975b..c5bd7410a 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -194,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; @@ -557,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)"), @@ -1907,7 +1922,10 @@ 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(x) <= timestamp(253402300799)", "timestamp(x) == timestamp(x)"), + TIMESTAMP_STRING_CONVERSION_OVERFLOW_EQUIVALENCE( + "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)"), @@ -2202,10 +2220,106 @@ private enum EquivalenceTestCase { 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_DUPLICATE_SECONDS_LAST_WINS( + "google.protobuf.Timestamp{seconds: 10, 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_MIN_NANOS( + "int(google.protobuf.Timestamp{seconds: 100, nanos: 1})", "100"), + TIMESTAMP_STRUCT_TO_INT_TRUNCATES_POSITIVE_NANOS( + "int(google.protobuf.Timestamp{seconds: 100, nanos: 999999999})", "100"), + TIMESTAMP_STRUCT_TO_INT_POSITIVE_NANOS_ROLLOVER( + "int(google.protobuf.Timestamp{seconds: 100, nanos: 999999999} +" + + " google.protobuf.Duration{nanos: 1})", + "101"), + TIMESTAMP_STRUCT_TO_INT_NEGATIVE_SECONDS_ZERO_NANOS( + "int(google.protobuf.Timestamp{seconds: -1, nanos: 0})", "-1"), + TIMESTAMP_STRUCT_TO_INT_NEGATIVE_SECONDS_MIN_POSITIVE_NANOS( + "int(google.protobuf.Timestamp{seconds: -1, nanos: 1})", "-1"), + TIMESTAMP_STRUCT_TO_INT_FLOORS_NEGATIVE_SECONDS( + "int(google.protobuf.Timestamp{seconds: -1, nanos: 500000000})", "-1"), + TIMESTAMP_STRUCT_TO_INT_NEGATIVE_SECONDS_MAX_NANOS( + "int(google.protobuf.Timestamp{seconds: -1, nanos: 999999999})", "-1"), + TIMESTAMP_STRUCT_TO_INT_NEGATIVE_SECONDS_NANOS_ROLLOVER_TO_ZERO( + "int(google.protobuf.Timestamp{seconds: -1, nanos: 999999999} +" + + " google.protobuf.Duration{nanos: 1})", + "0"), + TIMESTAMP_STRUCT_TO_INT_ZERO_SECONDS_SUBTRACT_ONE_NANO_FLOORS_TO_NEGATIVE_ONE( + "int(google.protobuf.Timestamp{seconds: 0, nanos: 0} -" + + " google.protobuf.Duration{nanos: 1})", + "-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()"), @@ -2317,7 +2431,56 @@ private enum EquivalenceViolationTestCase { "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"); + 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_STRING_CONVERSION_NOT_BOUNDED_BY_WHOLE_SECONDS( + "timestamp(string_var) <= timestamp(253402300799)", + "timestamp(string_var) == timestamp(string_var)"), + TIMESTAMP_STRUCT_TO_INT_NEGATIVE_SECONDS_NEGATIVE_NANOS_FAILS( + "int(google.protobuf.Timestamp{seconds: -1, nanos: -1}) == -1", "false"), + TIMESTAMP_STRUCT_TO_INT_NEGATIVE_SECONDS_NANOS_TOO_LARGE_FAILS( + "int(google.protobuf.Timestamp{seconds: -1, nanos: 1000000000}) == 0", "false"), + 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;