Skip to content

Commit 3613047

Browse files
l46kokcopybara-github
l46kok
authored and
copybara-github
committed
Add axioms for timestamps and durations
PiperOrigin-RevId: 955537654
1 parent 2a08d78 commit 3613047

4 files changed

Lines changed: 86 additions & 4 deletions

File tree

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,6 +38,33 @@ final class AddAxiom {
3838
BoolExpr overflow = ts.checkIntOverflow(ctx.mkAdd(a1, a2));
3939
return Optional.of(ts.withRuntimeError(result, overflow));
4040
})
41+
.addBinaryOverloadTranslator(
42+
StandardFunction.Overload.Arithmetic.ADD_TIMESTAMP_DURATION.celOverloadDecl(),
43+
(ctx, ts, sink, l, r) -> {
44+
IntExpr a1 = ts.getInt(l);
45+
IntExpr a2 = ts.getInt(r);
46+
Expr<?> result = ts.wrapInt((IntExpr) ctx.mkAdd(a1, a2));
47+
BoolExpr overflow = ts.checkIntOverflow(ctx.mkAdd(a1, a2));
48+
return Optional.of(ts.withRuntimeError(result, overflow));
49+
})
50+
.addBinaryOverloadTranslator(
51+
StandardFunction.Overload.Arithmetic.ADD_DURATION_TIMESTAMP.celOverloadDecl(),
52+
(ctx, ts, sink, l, r) -> {
53+
IntExpr a1 = ts.getInt(l);
54+
IntExpr a2 = ts.getInt(r);
55+
Expr<?> result = ts.wrapInt((IntExpr) ctx.mkAdd(a1, a2));
56+
BoolExpr overflow = ts.checkIntOverflow(ctx.mkAdd(a1, a2));
57+
return Optional.of(ts.withRuntimeError(result, overflow));
58+
})
59+
.addBinaryOverloadTranslator(
60+
StandardFunction.Overload.Arithmetic.ADD_DURATION_DURATION.celOverloadDecl(),
61+
(ctx, ts, sink, l, r) -> {
62+
IntExpr a1 = ts.getInt(l);
63+
IntExpr a2 = ts.getInt(r);
64+
Expr<?> result = ts.wrapInt((IntExpr) ctx.mkAdd(a1, a2));
65+
BoolExpr overflow = ts.checkIntOverflow(ctx.mkAdd(a1, a2));
66+
return Optional.of(ts.withRuntimeError(result, overflow));
67+
})
4168
.addBinaryOverloadTranslator(
4269
StandardFunction.Overload.Arithmetic.ADD_UINT64.celOverloadDecl(),
4370
(ctx, ts, sink, l, r) -> {

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,33 @@ final class SubtractAxiom {
3535
BoolExpr overflow = ts.checkIntOverflow(ctx.mkSub(a1, a2));
3636
return Optional.of(ts.withRuntimeError(result, overflow));
3737
})
38+
.addBinaryOverloadTranslator(
39+
StandardFunction.Overload.Arithmetic.SUBTRACT_TIMESTAMP_TIMESTAMP.celOverloadDecl(),
40+
(ctx, ts, sink, l, r) -> {
41+
IntExpr a1 = ts.getInt(l);
42+
IntExpr a2 = ts.getInt(r);
43+
Expr<?> result = ts.wrapInt((IntExpr) ctx.mkSub(a1, a2));
44+
BoolExpr overflow = ts.checkIntOverflow(ctx.mkSub(a1, a2));
45+
return Optional.of(ts.withRuntimeError(result, overflow));
46+
})
47+
.addBinaryOverloadTranslator(
48+
StandardFunction.Overload.Arithmetic.SUBTRACT_TIMESTAMP_DURATION.celOverloadDecl(),
49+
(ctx, ts, sink, l, r) -> {
50+
IntExpr a1 = ts.getInt(l);
51+
IntExpr a2 = ts.getInt(r);
52+
Expr<?> result = ts.wrapInt((IntExpr) ctx.mkSub(a1, a2));
53+
BoolExpr overflow = ts.checkIntOverflow(ctx.mkSub(a1, a2));
54+
return Optional.of(ts.withRuntimeError(result, overflow));
55+
})
56+
.addBinaryOverloadTranslator(
57+
StandardFunction.Overload.Arithmetic.SUBTRACT_DURATION_DURATION.celOverloadDecl(),
58+
(ctx, ts, sink, l, r) -> {
59+
IntExpr a1 = ts.getInt(l);
60+
IntExpr a2 = ts.getInt(r);
61+
Expr<?> result = ts.wrapInt((IntExpr) ctx.mkSub(a1, a2));
62+
BoolExpr overflow = ts.checkIntOverflow(ctx.mkSub(a1, a2));
63+
return Optional.of(ts.withRuntimeError(result, overflow));
64+
})
3865
.addBinaryOverloadTranslator(
3966
StandardFunction.Overload.Arithmetic.SUBTRACT_UINT64.celOverloadDecl(),
4067
(ctx, ts, sink, l, r) -> {

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

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -53,8 +53,7 @@ final class TypeConversionAxioms {
5353
true)
5454
.addUnaryOverloadTranslator(
5555
Conversions.TIMESTAMP_TO_INT64.celOverloadDecl(),
56-
createUninterpretedConversion(Conversions.TIMESTAMP_TO_INT64),
57-
true)
56+
(ctx, typeSystem, sink, arg) -> Optional.of(arg))
5857
.build();
5958

6059
private static final CelZ3FunctionAxiom UINT_AXIOM =
@@ -173,8 +172,7 @@ final class TypeConversionAxioms {
173172
true)
174173
.addUnaryOverloadTranslator(
175174
Conversions.INT64_TO_TIMESTAMP.celOverloadDecl(),
176-
createUninterpretedConversion(Conversions.INT64_TO_TIMESTAMP),
177-
true)
175+
(ctx, typeSystem, sink, arg) -> Optional.of(arg))
178176
.build();
179177

180178
private static final CelZ3FunctionAxiom BOOL_AXIOM =

‎verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1438,6 +1438,36 @@ private enum EquivalenceTestCase {
14381438
MACRO_EXISTS_ONE_EQUIVALENT(
14391439
"[1, 2, 3].exists_one(x, x == 2)",
14401440
"(1 == 2 ? 1 : 0) + (2 == 2 ? 1 : 0) + (3 == 2 ? 1 : 0) == 1"),
1441+
TIMESTAMP_MATH_SUBTRACT_TS(
1442+
"timestamp(900000) - timestamp(100)",
1443+
"timestamp(899900) - timestamp(0)"),
1444+
TIMESTAMP_MATH_ADD_DUR_TS(
1445+
"timestamp(100) + duration('100s')",
1446+
"timestamp(200)"),
1447+
TIMESTAMP_MATH_ADD_TS_DUR(
1448+
"duration('100s') + timestamp(100)",
1449+
"timestamp(200)"),
1450+
TIMESTAMP_MATH_SUBTRACT_DUR(
1451+
"timestamp(900000) - duration('100s')",
1452+
"timestamp(899900)"),
1453+
DURATION_MATH_ADD_DUR_DUR(
1454+
"duration('100s') + duration('200s')",
1455+
"duration('300s')"),
1456+
DURATION_MATH_SUBTRACT_DUR_DUR(
1457+
"duration('300s') - duration('100s')",
1458+
"duration('200s')"),
1459+
TIMESTAMP_MATH_COMMUTATIVITY(
1460+
"duration('10s') + timestamp(50)",
1461+
"timestamp(50) + duration('10s')"),
1462+
DURATION_MATH_COMMUTATIVITY(
1463+
"duration('10s') + duration('20s')",
1464+
"duration('20s') + duration('10s')"),
1465+
DURATION_MATH_ASSOCIATIVITY(
1466+
"(duration('10s') + duration('20s')) + duration('30s')",
1467+
"duration('10s') + (duration('20s') + duration('30s'))"),
1468+
TIMESTAMP_DURATION_MATH_ASSOCIATIVITY(
1469+
"(timestamp(10) + duration('20s')) + duration('30s')",
1470+
"timestamp(10) + (duration('20s') + duration('30s'))"),
14411471
MACRO_MAP_EQUIVALENT("{1: true, 2: true, 3: true}.all(k, k > 0)", "1 > 0 && 2 > 0 && 3 > 0"),
14421472
MACRO_BIND_EQUIVALENT("cel.bind(x, 10, x > 0)", "10 > 0"),
14431473
NESTED_MACRO(

0 commit comments

Comments
 (0)