From 2d1e4db37269c0466c3fce71f10ed45a80d0ef9f Mon Sep 17 00:00:00 2001 From: Sean Huh Date: Wed, 4 Nov 2026 15:10:21 -0800 Subject: [PATCH] Widen Z3 verifier duration bounds to match google.protobuf.Duration. PiperOrigin-RevId: 1014169905 --- .../CelZ3CounterexampleGenerator.java | 19 +++--- .../cel/verifier/CelZ3StructTranslator.java | 3 +- .../dev/cel/verifier/CelZ3TypeSystem.java | 34 +++++----- .../cel/verifier/CelVerifierZ3ImplTest.java | 65 ++++++++++++++----- 4 files changed, 78 insertions(+), 43 deletions(-) diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index 675432d79..bbcb16403 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -138,14 +138,17 @@ private Value extractValue(Expr expr) { Instant instant = Instant.ofEpochSecond(seconds.longValue(), nanoAdjustment.longValue()); return Value.exact(instant, "timestamp(\"" + instant + "\")"); } else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) { - BigInteger nanos = ((IntNum) args[0]).getBigInteger(); - String display = - nanos.remainder(NANOS_PER_SECOND).signum() == 0 - ? "duration(\"" + nanos.divide(NANOS_PER_SECOND) + "s\")" - : "duration(\"" + nanos + "ns\")"; - return isInRange(nanos, Long.MIN_VALUE, Long.MAX_VALUE) - ? Value.exact(Duration.ofNanos(nanos.longValue()), display) - : Value.inexact(display); + BigInteger[] parts = ((IntNum) args[0]).getBigInteger().divideAndRemainder(NANOS_PER_SECOND); + if (!isInRange( + parts[0], ProtoTimeUtils.DURATION_SECONDS_MIN, ProtoTimeUtils.DURATION_SECONDS_MAX)) { + // No CEL duration is out of range, so no literal exists; show the seconds. + return Value.inexact("duration(\"" + parts[0] + "s\")"); + } + long seconds = parts[0].longValue(); + int nanos = parts[1].intValue(); + return Value.exact( + Duration.ofSeconds(seconds, nanos), + "duration(\"" + ProtoTimeUtils.formatDuration(seconds, nanos) + "\")"); } else if (decl.equals(typeSystem.listCons().ConstructorDecl())) { return extractList(args[0]); } else if (decl.equals(typeSystem.mapCons().ConstructorDecl())) { diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java index c98877185..90b941a67 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3StructTranslator.java @@ -25,6 +25,7 @@ import com.microsoft.z3.IntExpr; import dev.cel.common.CelAbstractSyntaxTree; import dev.cel.common.ast.CelExpr; +import dev.cel.common.internal.ProtoTimeUtils; import dev.cel.common.types.CelKind; import dev.cel.common.types.CelType; import dev.cel.common.types.CelTypeProvider; @@ -293,7 +294,7 @@ private TranslatedValue translateDurationWktStruct( celExpr, createStruct, ast, - CelZ3TypeSystem.MIN_DURATION_NANOS, + -ProtoTimeUtils.MAX_NANOS, (seconds, nanos, totalNanos) -> { BoolExpr signMismatch = ctx.mkOr( diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index d164505c4..1e92aed35 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -56,21 +56,14 @@ 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(); - + totalNanosString(ProtoTimeUtils.TIMESTAMP_SECONDS_MIN, 0); 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(); + totalNanosString(ProtoTimeUtils.TIMESTAMP_SECONDS_MAX, ProtoTimeUtils.MAX_NANOS); + private static final String MIN_TOTAL_DURATION_NANOS = + totalNanosString(ProtoTimeUtils.DURATION_SECONDS_MIN, -ProtoTimeUtils.MAX_NANOS); + private static final String MAX_TOTAL_DURATION_NANOS = + totalNanosString(ProtoTimeUtils.DURATION_SECONDS_MAX, ProtoTimeUtils.MAX_NANOS); private static final String TYPE_CEL_VALUE = "CelValue"; private static final String CONS_BOOL = "Bool"; @@ -775,11 +768,13 @@ public BoolExpr checkTimestampOverflow(ArithExpr result) { } /** - * 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}). + * Checks if the given nanosecond arithmetic expression overflows CEL Duration bounds ({@code + * [-315576000000.999999999s, 315576000000.999999999s]}). */ public BoolExpr checkDurationOverflow(ArithExpr result) { - return checkIntOverflow(result); + return ctx.mkOr( + ctx.mkGt(result, ctx.mkInt(MAX_TOTAL_DURATION_NANOS)), + ctx.mkLt(result, ctx.mkInt(MIN_TOTAL_DURATION_NANOS))); } /** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */ @@ -794,6 +789,13 @@ public SeqExpr mkConcatSafe(Expr arg1, Expr arg2) { return ctx.mkConcat((Expr>) arg1, (Expr>) arg2); } + private static String totalNanosString(long seconds, int nanos) { + return BigInteger.valueOf(seconds) + .multiply(BigInteger.valueOf(NANOS_PER_SECOND)) + .add(BigInteger.valueOf(nanos)) + .toString(); + } + @AutoValue abstract static class FuncDeclKey { abstract String name(); diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index e6d0b97a3..722f808f6 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -208,8 +208,8 @@ private enum IsSatisfiableTestCase { "ts = timestamp\\(\"1969-12-31T23:59:59\\.000000500Z\"\\)"), DURATION_SUBSECOND_SATISFIABLE( "dur == google.protobuf.Duration{seconds: 1, nanos: 500}", - "dur = duration\\(\"1000000500ns\"\\)"), - // Timestamps nested in dyn aren't range constrained, and RFC 3339 can't express these. + "dur = duration\\(\"1\\.000000500s\"\\)"), + // Timestamps and durations nested in dyn aren't range constrained. TIMESTAMP_ABOVE_RANGE_SATISFIABLE( "type(dyn_var) == google.protobuf.Timestamp" + " && dyn_var > google.protobuf.Timestamp{seconds: 253402300799, nanos: 999999999}", @@ -218,6 +218,14 @@ private enum IsSatisfiableTestCase { "type(dyn_var) == google.protobuf.Timestamp" + " && dyn_var < google.protobuf.Timestamp{seconds: -62135596800}", "dyn_var = timestamp\\(-\\d+\\)"), + DURATION_ABOVE_RANGE_SATISFIABLE( + "type(dyn_var) == google.protobuf.Duration" + + " && dyn_var > google.protobuf.Duration{seconds: 315576000000, nanos: 999999999}", + "dyn_var = duration\\(\"\\d+s\"\\)"), + DURATION_BELOW_RANGE_SATISFIABLE( + "type(dyn_var) == google.protobuf.Duration" + + " && dyn_var < google.protobuf.Duration{seconds: -315576000000, nanos: -999999999}", + "dyn_var = duration\\(\"-\\d+s\"\\)"), ; private final String expr; @@ -280,7 +288,17 @@ private enum WitnessTestCase { SUBSECOND_DURATION( "dur == google.protobuf.Duration{seconds: -1, nanos: -500}", "dur", - "duration(\"-1000000500ns\")"), + "duration(\"-1.000000500s\")"), + NEGATIVE_SUBSECOND_DURATION( + "dur == google.protobuf.Duration{nanos: -500}", "dur", "duration(\"-0.000000500s\")"), + MIN_DURATION( + "dur == google.protobuf.Duration{seconds: -315576000000, nanos: -999999999}", + "dur", + "duration(\"-315576000000.999999999s\")"), + MAX_DURATION( + "dur == google.protobuf.Duration{seconds: 315576000000, nanos: 999999999}", + "dur", + "duration(\"315576000000.999999999s\")"), NULL("dyn_var == null", "dyn_var", "null"), EMPTY_LIST("int_list == []", "int_list", "[]"), LIST_WITH_NULL("dyn_list == [true, null]", "dyn_list", "[true, null]"), @@ -324,6 +342,14 @@ private enum InexactWitnessTestCase { "type(dyn_var) == google.protobuf.Timestamp" + " && dyn_var > google.protobuf.Timestamp{seconds: 253402300799, nanos: 999999999}", "dyn_var"), + DURATION_ABOVE_MAX( + "type(dyn_var) == google.protobuf.Duration" + + " && dyn_var > google.protobuf.Duration{seconds: 315576000000, nanos: 999999999}", + "dyn_var"), + DURATION_BELOW_MIN( + "type(dyn_var) == google.protobuf.Duration" + + " && dyn_var < google.protobuf.Duration{seconds: -315576000000, nanos: -999999999}", + "dyn_var"), SURROGATE_STRING( "size(string_var) == 1 && string_var > '\\ud7ff' && string_var < '\\ue000'", "string_var"), NON_ASCII_BYTES("by == b'\\xc3\\xa9'", "by"), @@ -780,8 +806,8 @@ private enum IsAlwaysTrueTestCase { + " 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}"), + "dur >= google.protobuf.Duration{seconds: -315576000000, nanos: -999999999} && dur <=" + + " google.protobuf.Duration{seconds: 315576000000, nanos: 999999999}"), 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)"), @@ -2491,14 +2517,18 @@ private enum EquivalenceTestCase { "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} >" + DURATION_STRUCT_MAX_VALID( + "google.protobuf.Duration{seconds: 315576000000, nanos: 999999999} >" + " google.protobuf.Duration{}", "true"), - DURATION_STRUCT_MIN_GO_DURATION_VALID( - "google.protobuf.Duration{seconds: -9223372036, nanos: -854775808} <" + DURATION_STRUCT_MIN_VALID( + "google.protobuf.Duration{seconds: -315576000000, nanos: -999999999} <" + " google.protobuf.Duration{}", "true"), + TIMESTAMP_SUBTRACT_MAX_RANGE_VALID( + "(timestamp(253402300799) - timestamp(-62135596800)) ==" + + " google.protobuf.Duration{seconds: 315537897599}", + "true"), TIMESTAMP_STRUCT_MIN_VALID( "google.protobuf.Timestamp{seconds: -62135596800, nanos: 0}", "timestamp(-62135596800)"), TIMESTAMP_STRUCT_MAX_VALID( @@ -2692,16 +2722,15 @@ private enum EquivalenceViolationTestCase { "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{}", + DURATION_STRUCT_SECONDS_UNDERFLOW_FAILS( + "google.protobuf.Duration{seconds: -315576000001} == google.protobuf.Duration{}", "false"), + DURATION_ADD_EXCEEDS_MAX_FAILS( + "(google.protobuf.Duration{seconds: 315576000000, nanos: 999999999} +" + + " google.protobuf.Duration{nanos: 1}) == google.protobuf.Duration{}", "false"), - TIMESTAMP_SUBTRACT_EXCEEDS_GO_DURATION_FAILS( - "(timestamp(253402300799) - timestamp(-62135596800)) == google.protobuf.Duration{}", + DURATION_SUBTRACT_EXCEEDS_MIN_FAILS( + "(google.protobuf.Duration{seconds: -315576000000, nanos: -999999999} -" + + " google.protobuf.Duration{nanos: 1}) == google.protobuf.Duration{}", "false"); final String exprA;