Skip to content

Commit 62b8f6d

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Add axioms for timestamps/durations arithmetic along with their type conversions
PiperOrigin-RevId: 955537654
1 parent 8bfc4c7 commit 62b8f6d

13 files changed

Lines changed: 256 additions & 53 deletions

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -533,6 +533,12 @@ private Expr<?> getDefaultValueForType(CelType type) {
533533
if (type.equals(SimpleType.UINT)) {
534534
return typeSystem.mkUint(0);
535535
}
536+
if (type.equals(SimpleType.TIMESTAMP)) {
537+
return typeSystem.wrapTimestamp(ctx.mkInt(0));
538+
}
539+
if (type.equals(SimpleType.DURATION)) {
540+
return typeSystem.wrapDuration(ctx.mkInt(0));
541+
}
536542
if (type instanceof ListType) {
537543
if (emptyListCache == null) {
538544
emptyListCache = typeSystem.mkListRefConst(EMPTY_LIST_PREFIX);

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,10 @@ private static String formatExpr(
8282
// Handle CelType constructors wrapper unwrapping
8383
if (decl.equals(typeSystem.intCons().ConstructorDecl())) {
8484
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]);
85+
} else if (decl.equals(typeSystem.timestampCons().ConstructorDecl())) {
86+
return "timestamp(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")";
87+
} else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) {
88+
return "duration(" + formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + ")";
8589
} else if (decl.equals(typeSystem.uintCons().ConstructorDecl())) {
8690
return formatExpr(ctx, typeSystem, model, expr.getArgs()[0]) + "u";
8791
} else if (decl.equals(typeSystem.boolCons().ConstructorDecl())) {

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -148,11 +148,11 @@ private BoolExpr mkTypeGuard(Expr<?> arg, CelType expectedType) {
148148
// These match everything structurally type-wise, although we might refine this later.
149149
return ctx.mkTrue();
150150
case INT:
151+
return typeSystem.isInt(arg);
151152
case TIMESTAMP:
153+
return typeSystem.isTimestamp(arg);
152154
case DURATION:
153-
// Safe to map int, timestamp, and duration to IntSort because CEL's static checker prevents
154-
// invalid cross-type usage and their operator axioms translate to identical Z3 ASTs.
155-
return typeSystem.isInt(arg);
155+
return typeSystem.isDuration(arg);
156156
case UINT:
157157
return typeSystem.isUint(arg);
158158
case DOUBLE:

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

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,14 @@ public final class CelZ3TypeSystem {
8282
private static final String IS_BYTES = "isBytes";
8383
private static final String GET_BYTES = "getBytes";
8484

85+
private static final String CONS_TIMESTAMP = "Timestamp";
86+
private static final String IS_TIMESTAMP = "isTimestamp";
87+
private static final String GET_TIMESTAMP = "getTimestamp";
88+
89+
private static final String CONS_DURATION = "Duration";
90+
private static final String IS_DURATION = "isDuration";
91+
private static final String GET_DURATION = "getDuration";
92+
8593
private static final String CONS_ERROR = "CelError";
8694
private static final String IS_ERROR = "isError";
8795

@@ -170,6 +178,8 @@ public int hashCode() {
170178
private final Constructor doubleCons;
171179
private final Constructor stringCons;
172180
private final Constructor bytesCons;
181+
private final Constructor timestampCons;
182+
private final Constructor durationCons;
173183
private final Constructor errorCons;
174184
private final Constructor unknownCons;
175185
private final Constructor nullCons;
@@ -257,6 +267,14 @@ Constructor bytesCons() {
257267
return bytesCons;
258268
}
259269

270+
Constructor timestampCons() {
271+
return timestampCons;
272+
}
273+
274+
Constructor durationCons() {
275+
return durationCons;
276+
}
277+
260278
Constructor optionalCons() {
261279
return optionalCons;
262280
}
@@ -296,6 +314,16 @@ public Expr<?> wrapBytes(Expr<?> expr) {
296314
return ctx.mkApp(bytesCons.ConstructorDecl(), expr);
297315
}
298316

317+
/** Wraps a Z3 integer expression into a timestamp CelValue. */
318+
public Expr<?> wrapTimestamp(IntExpr expr) {
319+
return ctx.mkApp(timestampCons.ConstructorDecl(), expr);
320+
}
321+
322+
/** Wraps a Z3 integer expression into a duration CelValue. */
323+
public Expr<?> wrapDuration(IntExpr expr) {
324+
return ctx.mkApp(durationCons.ConstructorDecl(), expr);
325+
}
326+
299327
/** Creates a CelValue containing an integer. */
300328
public Expr<?> mkInt(long val) {
301329
return ctx.mkApp(intCons.ConstructorDecl(), ctx.mkInt(val));
@@ -582,6 +610,26 @@ public IntExpr getUint(Expr<?> val) {
582610
return (IntExpr) ctx.mkApp(uintCons.getAccessorDecls()[0], val);
583611
}
584612

613+
/** Checks if the given CelValue is a timestamp. */
614+
public BoolExpr isTimestamp(Expr<?> val) {
615+
return (BoolExpr) ctx.mkApp(timestampCons.getTesterDecl(), val);
616+
}
617+
618+
/** Extracts the integer expression from a timestamp CelValue. */
619+
public IntExpr getTimestamp(Expr<?> val) {
620+
return (IntExpr) ctx.mkApp(timestampCons.getAccessorDecls()[0], val);
621+
}
622+
623+
/** Checks if the given CelValue is a duration. */
624+
public BoolExpr isDuration(Expr<?> val) {
625+
return (BoolExpr) ctx.mkApp(durationCons.getTesterDecl(), val);
626+
}
627+
628+
/** Extracts the integer expression from a duration CelValue. */
629+
public IntExpr getDuration(Expr<?> val) {
630+
return (IntExpr) ctx.mkApp(durationCons.getAccessorDecls()[0], val);
631+
}
632+
585633
/** Checks if the given CelValue is a string. */
586634
public BoolExpr isString(Expr<?> val) {
587635
return (BoolExpr) ctx.mkApp(stringCons.getTesterDecl(), val);
@@ -719,6 +767,19 @@ public BoolExpr checkIntOverflow(ArithExpr result) {
719767
return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_INT64)), ctx.mkLt(result, ctx.mkInt(MIN_INT64)));
720768
}
721769

770+
/** Checks if the given arithmetic expression overflows CEL Timestamp bounds. */
771+
public BoolExpr checkTimestampOverflow(ArithExpr result) {
772+
return ctx.mkOr(
773+
ctx.mkGt(result, ctx.mkInt(253402300799L)), // 9999-12-31T23:59:59Z
774+
ctx.mkLt(result, ctx.mkInt(-62135596800L))); // 0001-01-01T00:00:00Z
775+
}
776+
777+
/** Checks if the given arithmetic expression overflows CEL Duration bounds. */
778+
public BoolExpr checkDurationOverflow(ArithExpr result) {
779+
return ctx.mkOr(
780+
ctx.mkGt(result, ctx.mkInt(315576000000L)), ctx.mkLt(result, ctx.mkInt(-315576000000L)));
781+
}
782+
722783
/** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */
723784
public BoolExpr checkUintOverflow(ArithExpr result) {
724785
return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_UINT64)), ctx.mkLt(result, ctx.mkInt(0)));
@@ -890,6 +951,20 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
890951
this.bytesCons =
891952
ctx.mkConstructor(
892953
CONS_BYTES, IS_BYTES, new String[] {GET_BYTES}, new Sort[] {ctx.getStringSort()}, null);
954+
this.timestampCons =
955+
ctx.mkConstructor(
956+
CONS_TIMESTAMP,
957+
IS_TIMESTAMP,
958+
new String[] {GET_TIMESTAMP},
959+
new Sort[] {ctx.getIntSort()},
960+
null);
961+
this.durationCons =
962+
ctx.mkConstructor(
963+
CONS_DURATION,
964+
IS_DURATION,
965+
new String[] {GET_DURATION},
966+
new Sort[] {ctx.getIntSort()},
967+
null);
893968
this.errorCons = ctx.mkConstructor(CONS_ERROR, IS_ERROR, null, null, null);
894969

895970
this.unknownIdSort = ctx.mkUninterpretedSort("UnknownId");
@@ -936,6 +1011,8 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
9361011
this.doubleCons,
9371012
this.stringCons,
9381013
this.bytesCons,
1014+
this.timestampCons,
1015+
this.durationCons,
9391016
this.errorCons,
9401017
this.unknownCons,
9411018
this.optionalCons,

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

Lines changed: 45 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414

1515
package dev.cel.verifier.axioms;
1616

17+
import com.microsoft.z3.ArithExpr;
1718
import com.microsoft.z3.BoolExpr;
1819
import com.microsoft.z3.Expr;
1920
import com.microsoft.z3.FPExpr;
@@ -22,22 +23,59 @@
2223
import com.microsoft.z3.SeqExpr;
2324
import com.microsoft.z3.Sort;
2425
import dev.cel.checker.CelStandardDeclarations.StandardFunction;
26+
import dev.cel.verifier.CelZ3TypeSystem;
2527
import java.util.Optional;
28+
import java.util.function.BiFunction;
2629

2730
/** Axiomatization for CEL's addition operator (+). */
2831
final class AddAxiom {
2932

33+
@SuppressWarnings("Immutable") // Actually immutable -- BiFunction just isn't annotated as such.
34+
private static CelZ3FunctionAxiom.BinaryTranslator createAddTranslator(
35+
BiFunction<CelZ3TypeSystem, Expr<?>, IntExpr> getLeft,
36+
BiFunction<CelZ3TypeSystem, Expr<?>, IntExpr> getRight,
37+
BiFunction<CelZ3TypeSystem, IntExpr, Expr<?>> wrapResult,
38+
BiFunction<CelZ3TypeSystem, ArithExpr<?>, BoolExpr> overflowChecker) {
39+
return (ctx, ts, sink, l, r) -> {
40+
IntExpr a1 = getLeft.apply(ts, l);
41+
IntExpr a2 = getRight.apply(ts, r);
42+
ArithExpr<?> addition = ctx.mkAdd(a1, a2);
43+
Expr<?> result = wrapResult.apply(ts, (IntExpr) addition);
44+
BoolExpr overflow = overflowChecker.apply(ts, addition);
45+
return Optional.of(ts.withRuntimeError(result, overflow));
46+
};
47+
}
48+
3049
static final CelZ3FunctionAxiom INSTANCE =
3150
CelZ3FunctionAxiom.newBuilder(StandardFunction.ADD.functionDecl())
3251
.addBinaryOverloadTranslator(
3352
StandardFunction.Overload.Arithmetic.ADD_INT64.celOverloadDecl(),
34-
(ctx, ts, sink, l, r) -> {
35-
IntExpr a1 = ts.getInt(l);
36-
IntExpr a2 = ts.getInt(r);
37-
Expr<?> result = ts.wrapInt((IntExpr) ctx.mkAdd(a1, a2));
38-
BoolExpr overflow = ts.checkIntOverflow(ctx.mkAdd(a1, a2));
39-
return Optional.of(ts.withRuntimeError(result, overflow));
40-
})
53+
createAddTranslator(
54+
CelZ3TypeSystem::getInt,
55+
CelZ3TypeSystem::getInt,
56+
CelZ3TypeSystem::wrapInt,
57+
CelZ3TypeSystem::checkIntOverflow))
58+
.addBinaryOverloadTranslator(
59+
StandardFunction.Overload.Arithmetic.ADD_TIMESTAMP_DURATION.celOverloadDecl(),
60+
createAddTranslator(
61+
CelZ3TypeSystem::getTimestamp,
62+
CelZ3TypeSystem::getDuration,
63+
CelZ3TypeSystem::wrapTimestamp,
64+
CelZ3TypeSystem::checkTimestampOverflow))
65+
.addBinaryOverloadTranslator(
66+
StandardFunction.Overload.Arithmetic.ADD_DURATION_TIMESTAMP.celOverloadDecl(),
67+
createAddTranslator(
68+
CelZ3TypeSystem::getDuration,
69+
CelZ3TypeSystem::getTimestamp,
70+
CelZ3TypeSystem::wrapTimestamp,
71+
CelZ3TypeSystem::checkTimestampOverflow))
72+
.addBinaryOverloadTranslator(
73+
StandardFunction.Overload.Arithmetic.ADD_DURATION_DURATION.celOverloadDecl(),
74+
createAddTranslator(
75+
CelZ3TypeSystem::getDuration,
76+
CelZ3TypeSystem::getDuration,
77+
CelZ3TypeSystem::wrapDuration,
78+
CelZ3TypeSystem::checkDurationOverflow))
4179
.addBinaryOverloadTranslator(
4280
StandardFunction.Overload.Arithmetic.ADD_UINT64.celOverloadDecl(),
4381
(ctx, ts, sink, l, r) -> {

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -41,16 +41,16 @@ final class GreaterAxiom {
4141
Optional.of(
4242
typeSystem.wrapBool(
4343
ctx.mkGt(
44-
(ArithExpr) typeSystem.getInt(lhs),
45-
(ArithExpr) typeSystem.getInt(rhs)))))
44+
(ArithExpr) typeSystem.getTimestamp(lhs),
45+
(ArithExpr) typeSystem.getTimestamp(rhs)))))
4646
.addBinaryOverloadTranslator(
4747
Comparison.GREATER_DURATION.celOverloadDecl(),
4848
(ctx, typeSystem, constraintSink, lhs, rhs) ->
4949
Optional.of(
5050
typeSystem.wrapBool(
5151
ctx.mkGt(
52-
(ArithExpr) typeSystem.getInt(lhs),
53-
(ArithExpr) typeSystem.getInt(rhs)))))
52+
(ArithExpr) typeSystem.getDuration(lhs),
53+
(ArithExpr) typeSystem.getDuration(rhs)))))
5454
.addBinaryOverloadTranslator(
5555
Comparison.GREATER_UINT64.celOverloadDecl(),
5656
(ctx, typeSystem, constraintSink, lhs, rhs) ->

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -41,16 +41,16 @@ final class GreaterEqualsAxiom {
4141
Optional.of(
4242
typeSystem.wrapBool(
4343
ctx.mkGe(
44-
(ArithExpr) typeSystem.getInt(lhs),
45-
(ArithExpr) typeSystem.getInt(rhs)))))
44+
(ArithExpr) typeSystem.getTimestamp(lhs),
45+
(ArithExpr) typeSystem.getTimestamp(rhs)))))
4646
.addBinaryOverloadTranslator(
4747
Comparison.GREATER_EQUALS_DURATION.celOverloadDecl(),
4848
(ctx, typeSystem, constraintSink, lhs, rhs) ->
4949
Optional.of(
5050
typeSystem.wrapBool(
5151
ctx.mkGe(
52-
(ArithExpr) typeSystem.getInt(lhs),
53-
(ArithExpr) typeSystem.getInt(rhs)))))
52+
(ArithExpr) typeSystem.getDuration(lhs),
53+
(ArithExpr) typeSystem.getDuration(rhs)))))
5454
.addBinaryOverloadTranslator(
5555
Comparison.GREATER_EQUALS_UINT64.celOverloadDecl(),
5656
(ctx, typeSystem, constraintSink, lhs, rhs) ->

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -41,16 +41,16 @@ final class LessAxiom {
4141
Optional.of(
4242
typeSystem.wrapBool(
4343
ctx.mkLt(
44-
(ArithExpr) typeSystem.getInt(lhs),
45-
(ArithExpr) typeSystem.getInt(rhs)))))
44+
(ArithExpr) typeSystem.getTimestamp(lhs),
45+
(ArithExpr) typeSystem.getTimestamp(rhs)))))
4646
.addBinaryOverloadTranslator(
4747
Comparison.LESS_DURATION.celOverloadDecl(),
4848
(ctx, typeSystem, constraintSink, lhs, rhs) ->
4949
Optional.of(
5050
typeSystem.wrapBool(
5151
ctx.mkLt(
52-
(ArithExpr) typeSystem.getInt(lhs),
53-
(ArithExpr) typeSystem.getInt(rhs)))))
52+
(ArithExpr) typeSystem.getDuration(lhs),
53+
(ArithExpr) typeSystem.getDuration(rhs)))))
5454
.addBinaryOverloadTranslator(
5555
Comparison.LESS_UINT64.celOverloadDecl(),
5656
(ctx, typeSystem, constraintSink, lhs, rhs) ->

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -41,16 +41,16 @@ final class LessEqualsAxiom {
4141
Optional.of(
4242
typeSystem.wrapBool(
4343
ctx.mkLe(
44-
(ArithExpr) typeSystem.getInt(lhs),
45-
(ArithExpr) typeSystem.getInt(rhs)))))
44+
(ArithExpr) typeSystem.getTimestamp(lhs),
45+
(ArithExpr) typeSystem.getTimestamp(rhs)))))
4646
.addBinaryOverloadTranslator(
4747
Comparison.LESS_EQUALS_DURATION.celOverloadDecl(),
4848
(ctx, typeSystem, constraintSink, lhs, rhs) ->
4949
Optional.of(
5050
typeSystem.wrapBool(
5151
ctx.mkLe(
52-
(ArithExpr) typeSystem.getInt(lhs),
53-
(ArithExpr) typeSystem.getInt(rhs)))))
52+
(ArithExpr) typeSystem.getDuration(lhs),
53+
(ArithExpr) typeSystem.getDuration(rhs)))))
5454
.addBinaryOverloadTranslator(
5555
Comparison.LESS_EQUALS_UINT64.celOverloadDecl(),
5656
(ctx, typeSystem, constraintSink, lhs, rhs) ->

0 commit comments

Comments
 (0)