Skip to content

Commit 04050ab

Browse files
TristonianJonescopybara-github
TristonianJones
authored and
copybara-github
committed
Support protobuf Timestamp and Duration Well-Known Types with nanosecond precision in CelVerifier.
PiperOrigin-RevId: 1004169151
1 parent 1675f38 commit 04050ab

7 files changed

Lines changed: 353 additions & 21 deletions

File tree

‎verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java‎

Lines changed: 112 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
import com.google.common.collect.ImmutableList;
1818
import com.google.common.collect.ImmutableSet;
1919
import com.google.common.collect.Iterables;
20+
import com.google.common.collect.Streams;
2021
import com.microsoft.z3.ArithExpr;
2122
import com.microsoft.z3.ArrayExpr;
2223
import com.microsoft.z3.BoolExpr;
@@ -83,6 +84,8 @@ final class CelAstToZ3Translator {
8384
private static final String EMPTY_LIST_PREFIX = "!empty_list";
8485
private static final String EMPTY_MAP_PREFIX = "!empty_map";
8586
private static final String NULL_VALUE_FIELD = "null_value";
87+
private static final String SECONDS_FIELD = "seconds";
88+
private static final String NANOS_FIELD = "nanos";
8689
private static final long MAX_UINT32 = 0xFFFFFFFFL;
8790
private final Context ctx;
8891
private final CelZ3TypeSystem typeSystem;
@@ -406,7 +409,12 @@ private TranslatedValue translateStruct(CelExpr celExpr, CelAbstractSyntaxTree a
406409
if (CelTypes.isWrapperType(createStruct.messageName())) {
407410
return translateWrapperWktStruct(celExpr, createStruct, ast);
408411
}
409-
// TODO: Support google.protobuf.Timestamp and google.protobuf.Duration.
412+
if (createStruct.messageName().equals(CelTypes.TIMESTAMP_MESSAGE)) {
413+
return translateTimestampWktStruct(celExpr, createStruct, ast);
414+
}
415+
if (createStruct.messageName().equals(CelTypes.DURATION_MESSAGE)) {
416+
return translateDurationWktStruct(celExpr, createStruct, ast);
417+
}
410418

411419
// Bypass SMT when the struct is empty (return the cached SMT default pointer)
412420
if (createStruct.entries().isEmpty()) {
@@ -599,6 +607,105 @@ private TranslatedValue translateWrapperWktStruct(
599607
return TranslatedValue.propagateStrict(ctx, typeSystem, currentVal, celExpr, entryTvs);
600608
}
601609

610+
@FunctionalInterface
611+
private interface TimeWktValueFactory {
612+
Expr<?> create(IntExpr seconds, IntExpr nanos, IntExpr totalNanos);
613+
}
614+
615+
private TranslatedValue translateTimestampWktStruct(
616+
CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
617+
return translateTimeWktStruct(
618+
celExpr,
619+
createStruct,
620+
ast,
621+
/* minNanos= */ 0,
622+
(seconds, nanos, totalNanos) ->
623+
typeSystem.withRuntimeError(
624+
typeSystem.wrapTimestamp(totalNanos),
625+
typeSystem.checkTimestampOverflow(totalNanos)));
626+
}
627+
628+
private TranslatedValue translateDurationWktStruct(
629+
CelExpr celExpr, CelExpr.CelStruct createStruct, CelAbstractSyntaxTree ast) {
630+
return translateTimeWktStruct(
631+
celExpr,
632+
createStruct,
633+
ast,
634+
CelZ3TypeSystem.MIN_DURATION_NANOS,
635+
(seconds, nanos, totalNanos) -> {
636+
BoolExpr signMismatch =
637+
ctx.mkOr(
638+
ctx.mkAnd(ctx.mkGt(seconds, ctx.mkInt(0)), ctx.mkLt(nanos, ctx.mkInt(0))),
639+
ctx.mkAnd(ctx.mkLt(seconds, ctx.mkInt(0)), ctx.mkGt(nanos, ctx.mkInt(0))));
640+
return typeSystem.withRuntimeError(
641+
typeSystem.wrapDuration(totalNanos),
642+
signMismatch,
643+
typeSystem.checkDurationOverflow(totalNanos));
644+
});
645+
}
646+
647+
private TranslatedValue translateTimeWktStruct(
648+
CelExpr celExpr,
649+
CelExpr.CelStruct createStruct,
650+
CelAbstractSyntaxTree ast,
651+
int minNanos,
652+
TimeWktValueFactory valueFactory) {
653+
List<TranslatedValue> entryTvs = new ArrayList<>();
654+
Expr<?> secondsVal =
655+
resolveStructFieldValue(createStruct, SECONDS_FIELD, typeSystem.mkInt(0), ast, entryTvs);
656+
Expr<?> nanosVal =
657+
resolveStructFieldValue(createStruct, NANOS_FIELD, typeSystem.mkInt(0), ast, entryTvs);
658+
659+
IntExpr seconds = typeSystem.getInt(secondsVal);
660+
IntExpr nanos = typeSystem.getInt(nanosVal);
661+
IntExpr totalNanos =
662+
(IntExpr)
663+
ctx.mkAdd(ctx.mkMul(seconds, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)), nanos);
664+
665+
BoolExpr typeError =
666+
ctx.mkOr(ctx.mkNot(typeSystem.isInt(secondsVal)), ctx.mkNot(typeSystem.isInt(nanosVal)));
667+
BoolExpr nanosOutOfRange =
668+
ctx.mkOr(
669+
ctx.mkLt(nanos, ctx.mkInt(minNanos)),
670+
ctx.mkGe(nanos, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)));
671+
672+
Expr<?> result =
673+
typeSystem.withRuntimeError(
674+
valueFactory.create(seconds, nanos, totalNanos), typeError, nanosOutOfRange);
675+
return TranslatedValue.propagateStrict(ctx, typeSystem, result, celExpr, entryTvs);
676+
}
677+
678+
private Expr<?> resolveStructFieldValue(
679+
CelExpr.CelStruct createStruct,
680+
String fieldName,
681+
Expr<?> defaultValue,
682+
CelAbstractSyntaxTree ast,
683+
List<TranslatedValue> entryTvs) {
684+
return Streams.findLast(
685+
createStruct.entries().stream().filter(entry -> entry.fieldKey().equals(fieldName)))
686+
.<Expr<?>>map(
687+
entry -> {
688+
TranslatedValue entryTv = translateExpr(entry.value(), ast);
689+
Expr<?> val = entryTv.z3Expr();
690+
if (entry.optionalEntry()) {
691+
Expr<?> checkedVal =
692+
typeSystem.withRuntimeError(val, ctx.mkNot(typeSystem.isOptional(val)));
693+
entryTv =
694+
TranslatedValue.create(
695+
checkedVal, entry.value(), typeSystem, entryTv.isApproximate());
696+
Expr<?> optRef = typeSystem.getOptionalRef(checkedVal);
697+
val =
698+
ctx.mkITE(
699+
typeSystem.optHasValue(optRef),
700+
typeSystem.getOptionalValue(optRef),
701+
defaultValue);
702+
}
703+
entryTvs.add(entryTv);
704+
return val;
705+
})
706+
.orElse(defaultValue);
707+
}
708+
602709
private Expr<?> getDefaultValueForType(CelType type) {
603710
if (type instanceof NullableType) {
604711
return typeSystem.mkNull();
@@ -1392,14 +1499,14 @@ private BoolExpr createTypeConstraintForType(Expr<?> val, CelType type) {
13921499
return typeSystem.isBytes(val);
13931500
}
13941501
if (type.equals(SimpleType.TIMESTAMP)) {
1395-
IntExpr seconds = typeSystem.getTimestamp(val);
1502+
IntExpr nanos = typeSystem.getTimestamp(val);
13961503
return ctx.mkAnd(
1397-
typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(seconds)));
1504+
typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(nanos)));
13981505
}
13991506
if (type.equals(SimpleType.DURATION)) {
1400-
IntExpr seconds = typeSystem.getDuration(val);
1507+
IntExpr nanos = typeSystem.getDuration(val);
14011508
return ctx.mkAnd(
1402-
typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(seconds)));
1509+
typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(nanos)));
14031510
}
14041511

14051512
if (type instanceof ListType) {

‎verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,10 +70,11 @@ public Optional<CelType> findType(String typeName) {
7070

7171
private static final ImmutableList<Descriptor> WELL_KNOWN_DESCRIPTORS =
7272
ImmutableList.of(
73-
// TODO: Support WellKnownProto.DURATION and WellKnownProto.TIMESTAMP.
73+
WellKnownProto.DURATION,
7474
WellKnownProto.JSON_LIST_VALUE,
7575
WellKnownProto.JSON_STRUCT_VALUE,
7676
WellKnownProto.JSON_VALUE,
77+
WellKnownProto.TIMESTAMP,
7778
WellKnownProto.FLOAT_VALUE,
7879
WellKnownProto.INT32_VALUE,
7980
WellKnownProto.INT64_VALUE,

‎verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java‎

Lines changed: 29 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@
2323
import com.microsoft.z3.IntNum;
2424
import com.microsoft.z3.Model;
2525
import com.microsoft.z3.RatNum;
26+
import java.math.BigInteger;
2627
import java.util.ArrayList;
2728
import java.util.HashSet;
2829
import java.util.LinkedHashSet;
@@ -86,9 +87,9 @@ private static String formatExpr(
8687
if (decl.equals(typeSystem.intCons().ConstructorDecl())) {
8788
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]);
8889
} else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) {
89-
return "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")";
90+
return formatTimestamp(expr.getArgs()[0]);
9091
} else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) {
91-
return "duration('" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "s')";
92+
return formatDuration(expr.getArgs()[0]);
9293
} else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) {
9394
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u";
9495
} else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) {
@@ -154,6 +155,32 @@ private static String formatExpr(
154155
return expr.toString();
155156
}
156157

158+
private static String formatTimestamp(Expr<?> nanosExpr) {
159+
BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger();
160+
BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND);
161+
BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond);
162+
BigInteger seconds = divRem[0];
163+
BigInteger nanos = divRem[1];
164+
if (nanos.signum() < 0) {
165+
seconds = seconds.subtract(BigInteger.ONE);
166+
nanos = nanos.add(nanosPerSecond);
167+
}
168+
if (nanos.equals(BigInteger.ZERO)) {
169+
return "timestamp(" + seconds + ")";
170+
}
171+
return "google.protobuf.Timestamp{seconds: " + seconds + ", nanos: " + nanos + "}";
172+
}
173+
174+
private static String formatDuration(Expr<?> nanosExpr) {
175+
BigInteger totalNanos = ((IntNum) nanosExpr).getBigInteger();
176+
BigInteger nanosPerSecond = BigInteger.valueOf(CelZ3TypeSystem.NANOS_PER_SECOND);
177+
BigInteger[] divRem = totalNanos.divideAndRemainder(nanosPerSecond);
178+
if (divRem[1].equals(BigInteger.ZERO)) {
179+
return "duration('" + divRem[0] + "s')";
180+
}
181+
return "duration('" + totalNanos + "ns')";
182+
}
183+
157184
private static String reconstructList(
158185
Context ctx, CelZ3TypeSystem typeSystem, Model model, Expr<?> listRef) {
159186
Expr<?> lenExpr =

‎verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java‎

Lines changed: 31 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@
3535
import com.microsoft.z3.SeqSort;
3636
import com.microsoft.z3.Sort;
3737
import dev.cel.common.internal.ProtoTimeUtils;
38+
import java.math.BigInteger;
3839
import java.util.ArrayList;
3940
import java.util.Arrays;
4041
import java.util.HashMap;
@@ -56,6 +57,25 @@
5657
@SuppressWarnings({"unchecked", "rawtypes", "AvoidObjectArrays"}) // Z3 Java API uses raw types.
5758
public final class CelZ3TypeSystem {
5859

60+
/** Number of nanoseconds per second. */
61+
public static final long NANOS_PER_SECOND = 1_000_000_000L;
62+
63+
/** Minimum valid nanosecond component for a protobuf Duration. */
64+
public static final int MIN_DURATION_NANOS = -999_999_999;
65+
66+
private static final long MAX_TIMESTAMP_NANOS_PART = 999_999_999L;
67+
68+
private static final String MIN_TIMESTAMP_NANOS =
69+
BigInteger.valueOf(ProtoTimeUtils.TIMESTAMP_SECONDS_MIN)
70+
.multiply(BigInteger.valueOf(NANOS_PER_SECOND))
71+
.toString();
72+
73+
private static final String MAX_TIMESTAMP_NANOS =
74+
BigInteger.valueOf(ProtoTimeUtils.TIMESTAMP_SECONDS_MAX)
75+
.multiply(BigInteger.valueOf(NANOS_PER_SECOND))
76+
.add(BigInteger.valueOf(MAX_TIMESTAMP_NANOS_PART))
77+
.toString();
78+
5979
private static final String TYPE_CEL_VALUE = "CelValue";
6080
private static final String CONS_BOOL = "Bool";
6181
private static final String IS_BOOL = "isBool";
@@ -777,18 +797,22 @@ public BoolExpr checkIntOverflow(ArithExpr result) {
777797
ctx.mkLt(result, ctx.mkInt(CelNumericBounds.MIN_INT64)));
778798
}
779799

780-
/** Checks if the given arithmetic expression overflows CEL Timestamp bounds. */
800+
/**
801+
* Checks if the given nanosecond arithmetic expression overflows CEL Timestamp bounds
802+
* ({@code [0001-01-01T00:00:00Z, 9999-12-31T23:59:59.999999999Z]}).
803+
*/
781804
public BoolExpr checkTimestampOverflow(ArithExpr result) {
782805
return ctx.mkOr(
783-
ctx.mkGt(result, ctx.mkInt(ProtoTimeUtils.TIMESTAMP_SECONDS_MAX)),
784-
ctx.mkLt(result, ctx.mkInt(ProtoTimeUtils.TIMESTAMP_SECONDS_MIN)));
806+
ctx.mkGt(result, ctx.mkInt(MAX_TIMESTAMP_NANOS)),
807+
ctx.mkLt(result, ctx.mkInt(MIN_TIMESTAMP_NANOS)));
785808
}
786809

787-
/** Checks if the given arithmetic expression overflows CEL Duration bounds. */
810+
/**
811+
* Checks if the given nanosecond arithmetic expression overflows CEL Duration bounds, which are
812+
* confined to a signed 64-bit integer of nanoseconds (matching Go's {@code time.Duration}).
813+
*/
788814
public BoolExpr checkDurationOverflow(ArithExpr result) {
789-
return ctx.mkOr(
790-
ctx.mkGt(result, ctx.mkInt(ProtoTimeUtils.DURATION_SECONDS_MAX)),
791-
ctx.mkLt(result, ctx.mkInt(ProtoTimeUtils.DURATION_SECONDS_MIN)));
815+
return checkIntOverflow(result);
792816
}
793817

794818
/** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */

‎verifier/src/main/java/dev/cel/verifier/axioms/OptionalAxioms.java‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -153,6 +153,8 @@ private static BoolExpr isZeroValue(Context ctx, CelZ3TypeSystem ts, Expr<?> val
153153
ctx.mkAnd(ts.isInt(val), ctx.mkEq(ts.getInt(val), ctx.mkInt(0))),
154154
ctx.mkAnd(ts.isUint(val), ctx.mkEq(ts.getUint(val), ctx.mkInt(0))),
155155
ctx.mkAnd(ts.isDouble(val), ctx.mkFPIsZero((FPExpr) ts.getDouble(val))),
156+
ctx.mkAnd(ts.isTimestamp(val), ctx.mkEq(ts.getTimestamp(val), ctx.mkInt(0))),
157+
ctx.mkAnd(ts.isDuration(val), ctx.mkEq(ts.getDuration(val), ctx.mkInt(0))),
156158
ctx.mkAnd(ts.isString(val), ctx.mkEq(ts.getString(val), ctx.mkString(""))),
157159
ctx.mkAnd(
158160
ts.isBytes(val), ctx.mkEq(ctx.mkLength((SeqExpr) ts.getBytes(val)), ctx.mkInt(0))),

‎verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java‎

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@
2525
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
2626
import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Conversions;
2727
import dev.cel.common.types.SimpleType;
28+
import dev.cel.verifier.CelZ3TypeSystem;
2829
import java.util.Optional;
2930

3031
/** Axiomatization for CEL's type conversion functions. */
@@ -52,7 +53,12 @@ final class TypeConversionAxioms {
5253
.addUnaryOverloadTranslator(
5354
Conversions.TIMESTAMP_TO_INT64.celOverloadDecl(),
5455
(ctx, typeSystem, sink, arg) ->
55-
Optional.of(typeSystem.wrapInt(typeSystem.getTimestamp(arg))))
56+
Optional.of(
57+
typeSystem.wrapInt(
58+
(IntExpr)
59+
ctx.mkDiv(
60+
typeSystem.getTimestamp(arg),
61+
ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND)))))
5662
.build();
5763

5864
private static final CelZ3FunctionAxiom UINT_AXIOM =
@@ -159,9 +165,11 @@ final class TypeConversionAxioms {
159165
Conversions.INT64_TO_TIMESTAMP.celOverloadDecl(),
160166
(ctx, typeSystem, sink, arg) -> {
161167
IntExpr intVal = typeSystem.getInt(arg);
162-
BoolExpr overflow = typeSystem.checkTimestampOverflow(intVal);
168+
IntExpr nanosVal =
169+
(IntExpr) ctx.mkMul(intVal, ctx.mkInt(CelZ3TypeSystem.NANOS_PER_SECOND));
170+
BoolExpr overflow = typeSystem.checkTimestampOverflow(nanosVal);
163171
return Optional.of(
164-
typeSystem.withRuntimeError(typeSystem.wrapTimestamp(intVal), overflow));
172+
typeSystem.withRuntimeError(typeSystem.wrapTimestamp(nanosVal), overflow));
165173
})
166174
.build();
167175

0 commit comments

Comments
 (0)