diff --git a/common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java b/common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java index a6e98c571..124f9dbe1 100644 --- a/common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java +++ b/common/src/main/java/dev/cel/common/internal/ProtoTimeUtils.java @@ -18,7 +18,6 @@ import static com.google.common.math.LongMath.checkedMultiply; import static com.google.common.math.LongMath.checkedSubtract; -import com.google.common.annotations.VisibleForTesting; import com.google.common.base.Strings; import com.google.errorprone.annotations.CanIgnoreReturnValue; import com.google.protobuf.Duration; @@ -50,15 +49,11 @@ public final class ProtoTimeUtils { // Timestamp for "0001-01-01T00:00:00Z" - @VisibleForTesting - static final long TIMESTAMP_SECONDS_MIN = -62135596800L; + public static final long TIMESTAMP_SECONDS_MIN = -62135596800L; // Timestamp for "9999-12-31T23:59:59Z" - @VisibleForTesting - static final long TIMESTAMP_SECONDS_MAX = 253402300799L; - @VisibleForTesting - static final long DURATION_SECONDS_MIN = -315576000000L; - @VisibleForTesting - static final long DURATION_SECONDS_MAX = 315576000000L; + public static final long TIMESTAMP_SECONDS_MAX = 253402300799L; + public static final long DURATION_SECONDS_MIN = -315576000000L; + public static final long DURATION_SECONDS_MAX = 315576000000L; private static final int MILLIS_PER_SECOND = 1000; diff --git a/verifier/README.md b/verifier/README.md index db797a283..f286a4d6f 100644 --- a/verifier/README.md +++ b/verifier/README.md @@ -400,7 +400,7 @@ public class InvariantsExample { ### Timeouts -SMT solving is NP-complete and can theoretically stop responding or take an +SMT solving is NP-hard and can theoretically stop responding or take an exponential amount of time for complex formulas. The verifier uses a default timeout of 10 seconds. It is recommended to configure this to a reasonable duration for your specific use case using diff --git a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel index b9ac88687..4ca9794cc 100644 --- a/verifier/src/main/java/dev/cel/verifier/BUILD.bazel +++ b/verifier/src/main/java/dev/cel/verifier/BUILD.bazel @@ -98,6 +98,7 @@ java_library( tags = [ ], deps = [ + "//common/internal:proto_time_utils", "@maven//:com_google_errorprone_error_prone_annotations", "@maven//:com_google_guava_guava", "@maven//:tools_aqua_z3_turnkey", diff --git a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java index 8c0239efd..e3bb1bfaf 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java @@ -533,6 +533,12 @@ private Expr getDefaultValueForType(CelType type) { if (type.equals(SimpleType.UINT)) { return typeSystem.mkUint(0); } + if (type.equals(SimpleType.TIMESTAMP)) { + return typeSystem.wrapTimestamp(ctx.mkInt(0)); + } + if (type.equals(SimpleType.DURATION)) { + return typeSystem.wrapDuration(ctx.mkInt(0)); + } if (type instanceof ListType) { if (emptyListCache == null) { emptyListCache = typeSystem.mkListRefConst(EMPTY_LIST_PREFIX); @@ -735,8 +741,10 @@ private TranslatedValue translateCall(CelExpr expr, CelAbstractSyntaxTree ast) { typeConstraints.add(ctx.mkNot(typeSystem.isUnknown(callRes))); typeConstraints.add(ctx.mkNot(typeSystem.isError(callRes))); + boolean isDynamic = ast.getType(exprId).map(SimpleType.DYN::equals).orElse(true); + BoolExpr isApprox = ctx.mkBool(!isDynamic); return TranslatedValue.propagateStrict( - ctx, typeSystem, callRes, Optional.of(expr), ctx.mkTrue(), args); + ctx, typeSystem, callRes, Optional.of(expr), isApprox, args); }); } @@ -1269,6 +1277,17 @@ private BoolExpr createTypeConstraintForType(Expr val, CelType type) { if (type.equals(SimpleType.BYTES)) { return (BoolExpr) ctx.mkApp(typeSystem.bytesCons().getTesterDecl(), val); } + if (type.equals(SimpleType.TIMESTAMP)) { + IntExpr seconds = typeSystem.getTimestamp(val); + return ctx.mkAnd( + typeSystem.isTimestamp(val), ctx.mkNot(typeSystem.checkTimestampOverflow(seconds))); + } + if (type.equals(SimpleType.DURATION)) { + IntExpr seconds = typeSystem.getDuration(val); + return ctx.mkAnd( + typeSystem.isDuration(val), ctx.mkNot(typeSystem.checkDurationOverflow(seconds))); + } + if (type instanceof ListType) { // Lists are explicitly bounded (sequence theory). We're safe in using for-all quantifiers // here. diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java index f7d47635f..2355d36bf 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3CounterexampleGenerator.java @@ -82,6 +82,10 @@ private static String formatExpr( // Handle CelType constructors wrapper unwrapping 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]) + ")"; + } else if (decl.equals(typeSystem.durationCons().ConstructorDecl())) { + return "duration(" + formatExpr(ctx, typeSystem, model, 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())) { diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java index effa91c2b..3051fbd87 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3OperatorTranslator.java @@ -148,11 +148,11 @@ private BoolExpr mkTypeGuard(Expr arg, CelType expectedType) { // These match everything structurally type-wise, although we might refine this later. return ctx.mkTrue(); case INT: + return typeSystem.isInt(arg); case TIMESTAMP: + return typeSystem.isTimestamp(arg); case DURATION: - // Safe to map int, timestamp, and duration to IntSort because CEL's static checker prevents - // invalid cross-type usage and their operator axioms translate to identical Z3 ASTs. - return typeSystem.isInt(arg); + return typeSystem.isDuration(arg); case UINT: return typeSystem.isUint(arg); case DOUBLE: @@ -386,7 +386,7 @@ private BoolExpr getNumericEqualityWithConstant( ? ctx.mkEq(typeSystem.getUint(symVal), ctx.mkInt(uintVal)) : ctx.mkFalse(); } else if (symType.kind() == CelKind.DOUBLE) { - return ctx.mkFPEq((FPExpr) typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); + return ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); } } @@ -396,8 +396,7 @@ private BoolExpr getNumericEqualityWithConstant( (uintVal != null) ? ctx.mkEq(typeSystem.getUint(symVal), ctx.mkInt(uintVal)) : ctx.mkFalse(); - BoolExpr doubleEq = - ctx.mkFPEq((FPExpr) typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); + BoolExpr doubleEq = ctx.mkFPEq(typeSystem.getDouble(symVal), typeSystem.mkFpDouble(doubleVal)); return (BoolExpr) CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) @@ -435,18 +434,17 @@ private BoolExpr getStaticallyKnownNumericEquality( case UINT: return ctx.mkEq(typeSystem.getUint(z3Expr0), typeSystem.getUint(z3Expr1)); case DOUBLE: - return ctx.mkFPEq( - (FPExpr) typeSystem.getDouble(z3Expr0), (FPExpr) typeSystem.getDouble(z3Expr1)); + return ctx.mkFPEq(typeSystem.getDouble(z3Expr0), typeSystem.getDouble(z3Expr1)); default: return ctx.mkFalse(); } } private BoolExpr mkIsFiniteDouble(Expr z3Expr) { - Expr fpVal = typeSystem.getDouble(z3Expr); + FPExpr fpVal = typeSystem.getDouble(z3Expr); return ctx.mkAnd( typeSystem.isDouble(z3Expr), - ctx.mkNot(ctx.mkOr(ctx.mkFPIsNaN((FPExpr) fpVal), ctx.mkFPIsInfinite((FPExpr) fpVal)))); + ctx.mkNot(ctx.mkOr(ctx.mkFPIsNaN(fpVal), ctx.mkFPIsInfinite(fpVal)))); } private BoolExpr getDynamicNumericEquality(Expr z3Expr0, Expr z3Expr1) { @@ -475,25 +473,28 @@ private BoolExpr getDynamicNumericEquality(Expr z3Expr0, Expr z3Expr1) { BoolExpr isIntOrUintAndDouble = ctx.mkAnd(isIntOrUint0, typeSystem.isDouble(z3Expr1)); BoolExpr isDoubleAndIntOrUint = ctx.mkAnd(typeSystem.isDouble(z3Expr0), isIntOrUint1); - Expr fpVal1 = typeSystem.getDouble(z3Expr1); + FPExpr fpVal1 = typeSystem.getDouble(z3Expr1); + ArithExpr realVal0 = ctx.mkInt2Real(val0); BoolExpr intDoubleEq = ctx.mkAnd( mkIsFiniteDouble(z3Expr1), - ctx.mkEq(ctx.mkInt2Real(val0), ctx.mkFPToReal((FPExpr) fpVal1))); + ctx.mkLe(realVal0, ctx.mkFPToReal(fpVal1)), + ctx.mkLe(ctx.mkFPToReal(fpVal1), realVal0)); - Expr fpVal0 = typeSystem.getDouble(z3Expr0); + FPExpr fpVal0 = typeSystem.getDouble(z3Expr0); + ArithExpr realVal1 = ctx.mkInt2Real(val1); BoolExpr doubleIntEq = ctx.mkAnd( mkIsFiniteDouble(z3Expr0), - ctx.mkEq(ctx.mkFPToReal((FPExpr) fpVal0), ctx.mkInt2Real(val1))); + ctx.mkLe(realVal1, ctx.mkFPToReal(fpVal0)), + ctx.mkLe(ctx.mkFPToReal(fpVal0), realVal1)); return (BoolExpr) CelZ3TypeSystem.SwitchBuilder.newBuilder(ctx) .addCase(bothIntOrUint, ctx.mkEq(val0, val1)) .addCase( bothDouble, - ctx.mkFPEq( - (FPExpr) typeSystem.getDouble(z3Expr0), (FPExpr) typeSystem.getDouble(z3Expr1))) + ctx.mkFPEq(typeSystem.getDouble(z3Expr0), typeSystem.getDouble(z3Expr1))) .addCase(isIntOrUintAndDouble, intDoubleEq) .addCase(isDoubleAndIntOrUint, doubleIntEq) .build(ctx.mkFalse()); @@ -593,7 +594,8 @@ private TranslatedValue translateEquality( // because X == X is a tautology (or propagates errors/unknowns exactly). if (z3Arg0.equals(z3Arg1)) { Expr finalResult = typeSystem.propagateErrorAndUnknown(equalityExpr, z3Arg0); - return TranslatedValue.create(finalResult, typeSystem, ctx.mkFalse()); + return TranslatedValue.create( + finalResult, typeSystem, ctx.mkOr(arg0.isApproximate(), arg1.isApproximate())); } return TranslatedValue.propagateStrict(ctx, typeSystem, equalityExpr, arg0, arg1) diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index af1a4688b..e9a1872c9 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -26,11 +26,13 @@ import com.microsoft.z3.DatatypeSort; import com.microsoft.z3.Expr; import com.microsoft.z3.FPExpr; +import com.microsoft.z3.FPNum; import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; import com.microsoft.z3.SeqExpr; import com.microsoft.z3.SeqSort; import com.microsoft.z3.Sort; +import dev.cel.common.internal.ProtoTimeUtils; import java.util.ArrayList; import java.util.Arrays; import java.util.Collection; @@ -82,6 +84,14 @@ public final class CelZ3TypeSystem { private static final String IS_BYTES = "isBytes"; private static final String GET_BYTES = "getBytes"; + private static final String CONS_TIMESTAMP = "Timestamp"; + private static final String IS_TIMESTAMP = "isTimestamp"; + private static final String GET_TIMESTAMP = "getTimestamp"; + + private static final String CONS_DURATION = "Duration"; + private static final String IS_DURATION = "isDuration"; + private static final String GET_DURATION = "getDuration"; + private static final String CONS_ERROR = "CelError"; private static final String IS_ERROR = "isError"; @@ -170,6 +180,8 @@ public int hashCode() { private final Constructor doubleCons; private final Constructor stringCons; private final Constructor bytesCons; + private final Constructor timestampCons; + private final Constructor durationCons; private final Constructor errorCons; private final Constructor unknownCons; private final Constructor nullCons; @@ -233,34 +245,71 @@ public Sort listRefSort() { return listRefSort; } - Constructor boolCons() { + public Constructor boolCons() { return boolCons; } - Constructor intCons() { + public Constructor intCons() { return intCons; } - Constructor uintCons() { + public Constructor uintCons() { return uintCons; } - Constructor doubleCons() { + public Constructor doubleCons() { return doubleCons; } - Constructor stringCons() { + public Constructor stringCons() { return stringCons; } - Constructor bytesCons() { + public Constructor bytesCons() { return bytesCons; } + public Constructor timestampCons() { + return timestampCons; + } + + public Constructor durationCons() { + return durationCons; + } + Constructor optionalCons() { return optionalCons; } + /** + * Checks if the given CelValue expression represents a statically known primitive constant. + * + *

This is useful for determining whether an uninterpreted function's result should be treated + * as an approximation. If the argument is a known constant, any resulting error is an + * approximation (e.g., parsing a literal string). If it's a variable, the error is an exact + * runtime failure. + */ + public boolean isPrimitiveConstant(Expr expr) { + if (!expr.isApp()) { + return false; + } + FuncDecl decl = expr.getFuncDecl(); + if (decl.equals(stringCons.ConstructorDecl()) || decl.equals(bytesCons.ConstructorDecl())) { + return expr.getArgs()[0].isString(); + } else if (decl.equals(intCons.ConstructorDecl()) + || decl.equals(uintCons.ConstructorDecl()) + || decl.equals(timestampCons.ConstructorDecl()) + || decl.equals(durationCons.ConstructorDecl())) { + return expr.getArgs()[0].isNumeral(); + } else if (decl.equals(doubleCons.ConstructorDecl())) { + return expr.getArgs()[0] instanceof FPNum; + } else if (decl.equals(boolCons.ConstructorDecl())) { + Expr inner = expr.getArgs()[0]; + return inner.isTrue() || inner.isFalse(); + } + return false; + } + /** Creates a CelValue containing a boolean. */ public Expr mkBool(boolean val) { return ctx.mkApp(boolCons.ConstructorDecl(), ctx.mkBool(val)); @@ -296,6 +345,16 @@ public Expr wrapBytes(Expr expr) { return ctx.mkApp(bytesCons.ConstructorDecl(), expr); } + /** Wraps a Z3 integer expression into a timestamp CelValue. */ + public Expr wrapTimestamp(IntExpr expr) { + return ctx.mkApp(timestampCons.ConstructorDecl(), expr); + } + + /** Wraps a Z3 integer expression into a duration CelValue. */ + public Expr wrapDuration(IntExpr expr) { + return ctx.mkApp(durationCons.ConstructorDecl(), expr); + } + /** Creates a CelValue containing an integer. */ public Expr mkInt(long val) { return ctx.mkApp(intCons.ConstructorDecl(), ctx.mkInt(val)); @@ -326,8 +385,8 @@ public BoolExpr isDouble(Expr val) { } /** Extracts the double reference from a double CelValue. */ - public Expr getDouble(Expr val) { - return ctx.mkApp(doubleCons.getAccessorDecls()[0], val); + public FPExpr getDouble(Expr val) { + return (FPExpr) ctx.mkApp(doubleCons.getAccessorDecls()[0], val); } /** @@ -372,7 +431,7 @@ public BoolExpr getStructuralEquality(Expr arg0, Expr arg1) { // Doubles must be compared using native floating-point equality to follow IEEE-754. // Z3's structural mkEq evaluates NaN == NaN as true and 0.0 == -0.0 as false. BoolExpr isDoubleEq = ctx.mkAnd(isDouble(arg0), isDouble(arg1)); - BoolExpr doubleEq = ctx.mkFPEq((FPExpr) getDouble(arg0), (FPExpr) getDouble(arg1)); + BoolExpr doubleEq = ctx.mkFPEq(getDouble(arg0), getDouble(arg1)); // For primitives, generic equality matches the direct Z3 datatype wrapper. BoolExpr genericEq = ctx.mkEq(arg0, arg1); @@ -409,10 +468,14 @@ public Expr mkNull() { return ctx.mkConst(nullCons.ConstructorDecl()); } - Constructor errorCons() { + public Constructor errorCons() { return errorCons; } + public Constructor nullCons() { + return nullCons; + } + /** Creates a CelValue representing an unknown value. */ public Expr mkUnknown() { return mkUnknown(ctx.mkConst(GENERIC_UNKNOWN_ID, unknownIdSort)); @@ -498,7 +561,7 @@ public Expr withRuntimeError( return ctx.mkITE(condition, mkError(), result); } - Constructor unknownCons() { + public Constructor unknownCons() { return unknownCons; } @@ -582,6 +645,26 @@ public IntExpr getUint(Expr val) { return (IntExpr) ctx.mkApp(uintCons.getAccessorDecls()[0], val); } + /** Checks if the given CelValue is a timestamp. */ + public BoolExpr isTimestamp(Expr val) { + return (BoolExpr) ctx.mkApp(timestampCons.getTesterDecl(), val); + } + + /** Extracts the integer expression from a timestamp CelValue. */ + public IntExpr getTimestamp(Expr val) { + return (IntExpr) ctx.mkApp(timestampCons.getAccessorDecls()[0], val); + } + + /** Checks if the given CelValue is a duration. */ + public BoolExpr isDuration(Expr val) { + return (BoolExpr) ctx.mkApp(durationCons.getTesterDecl(), val); + } + + /** Extracts the integer expression from a duration CelValue. */ + public IntExpr getDuration(Expr val) { + return (IntExpr) ctx.mkApp(durationCons.getAccessorDecls()[0], val); + } + /** Checks if the given CelValue is a string. */ public BoolExpr isString(Expr val) { return (BoolExpr) ctx.mkApp(stringCons.getTesterDecl(), val); @@ -719,6 +802,20 @@ public BoolExpr checkIntOverflow(ArithExpr result) { return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_INT64)), ctx.mkLt(result, ctx.mkInt(MIN_INT64))); } + /** Checks if the given arithmetic expression overflows CEL Timestamp bounds. */ + 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))); + } + + /** Checks if the given arithmetic expression overflows CEL Duration bounds. */ + 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))); + } + /** Checks if the given arithmetic expression overflows a 64-bit unsigned integer. */ public BoolExpr checkUintOverflow(ArithExpr result) { return ctx.mkOr(ctx.mkGt(result, ctx.mkInt(MAX_UINT64)), ctx.mkLt(result, ctx.mkInt(0))); @@ -890,6 +987,20 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) { this.bytesCons = ctx.mkConstructor( CONS_BYTES, IS_BYTES, new String[] {GET_BYTES}, new Sort[] {ctx.getStringSort()}, null); + this.timestampCons = + ctx.mkConstructor( + CONS_TIMESTAMP, + IS_TIMESTAMP, + new String[] {GET_TIMESTAMP}, + new Sort[] {ctx.getIntSort()}, + null); + this.durationCons = + ctx.mkConstructor( + CONS_DURATION, + IS_DURATION, + new String[] {GET_DURATION}, + new Sort[] {ctx.getIntSort()}, + null); this.errorCons = ctx.mkConstructor(CONS_ERROR, IS_ERROR, null, null, null); this.unknownIdSort = ctx.mkUninterpretedSort("UnknownId"); @@ -936,6 +1047,8 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) { this.doubleCons, this.stringCons, this.bytesCons, + this.timestampCons, + this.durationCons, this.errorCons, this.unknownCons, this.optionalCons, diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/AddAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/AddAxiom.java index 072f75088..bff6b1edb 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/AddAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/AddAxiom.java @@ -14,30 +14,67 @@ package dev.cel.verifier.axioms; +import com.microsoft.z3.ArithExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Expr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.FuncDecl; import com.microsoft.z3.IntExpr; import com.microsoft.z3.SeqExpr; import com.microsoft.z3.Sort; import dev.cel.checker.CelStandardDeclarations.StandardFunction; +import dev.cel.verifier.CelZ3TypeSystem; import java.util.Optional; +import java.util.function.BiFunction; /** Axiomatization for CEL's addition operator (+). */ final class AddAxiom { + @SuppressWarnings("Immutable") // Actually immutable -- BiFunction just isn't annotated as such. + private static CelZ3FunctionAxiom.BinaryTranslator createAddTranslator( + BiFunction, IntExpr> getLeft, + BiFunction, IntExpr> getRight, + BiFunction> wrapResult, + BiFunction, BoolExpr> overflowChecker) { + return (ctx, ts, sink, l, r) -> { + IntExpr a1 = getLeft.apply(ts, l); + IntExpr a2 = getRight.apply(ts, r); + ArithExpr addition = ctx.mkAdd(a1, a2); + Expr result = wrapResult.apply(ts, (IntExpr) addition); + BoolExpr overflow = overflowChecker.apply(ts, addition); + return Optional.of(ts.withRuntimeError(result, overflow)); + }; + } + static final CelZ3FunctionAxiom INSTANCE = CelZ3FunctionAxiom.newBuilder(StandardFunction.ADD.functionDecl()) .addBinaryOverloadTranslator( StandardFunction.Overload.Arithmetic.ADD_INT64.celOverloadDecl(), - (ctx, ts, sink, l, r) -> { - IntExpr a1 = ts.getInt(l); - IntExpr a2 = ts.getInt(r); - Expr result = ts.wrapInt((IntExpr) ctx.mkAdd(a1, a2)); - BoolExpr overflow = ts.checkIntOverflow(ctx.mkAdd(a1, a2)); - return Optional.of(ts.withRuntimeError(result, overflow)); - }) + createAddTranslator( + CelZ3TypeSystem::getInt, + CelZ3TypeSystem::getInt, + CelZ3TypeSystem::wrapInt, + CelZ3TypeSystem::checkIntOverflow)) + .addBinaryOverloadTranslator( + StandardFunction.Overload.Arithmetic.ADD_TIMESTAMP_DURATION.celOverloadDecl(), + createAddTranslator( + CelZ3TypeSystem::getTimestamp, + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::wrapTimestamp, + CelZ3TypeSystem::checkTimestampOverflow)) + .addBinaryOverloadTranslator( + StandardFunction.Overload.Arithmetic.ADD_DURATION_TIMESTAMP.celOverloadDecl(), + createAddTranslator( + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::getTimestamp, + CelZ3TypeSystem::wrapTimestamp, + CelZ3TypeSystem::checkTimestampOverflow)) + .addBinaryOverloadTranslator( + StandardFunction.Overload.Arithmetic.ADD_DURATION_DURATION.celOverloadDecl(), + createAddTranslator( + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::wrapDuration, + CelZ3TypeSystem::checkDurationOverflow)) .addBinaryOverloadTranslator( StandardFunction.Overload.Arithmetic.ADD_UINT64.celOverloadDecl(), (ctx, ts, sink, l, r) -> { @@ -53,9 +90,7 @@ final class AddAxiom { Optional.of( ts.wrapDouble( ctx.mkFPAdd( - ctx.mkFPRoundNearestTiesToEven(), - (FPExpr) ts.getDouble(l), - (FPExpr) ts.getDouble(r))))) + ctx.mkFPRoundNearestTiesToEven(), ts.getDouble(l), ts.getDouble(r))))) .addBinaryOverloadTranslator( StandardFunction.Overload.Arithmetic.ADD_STRING.celOverloadDecl(), (ctx, ts, sink, l, r) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/CelZ3FunctionAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/CelZ3FunctionAxiom.java index 2d1129618..06d797d4d 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/CelZ3FunctionAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/CelZ3FunctionAxiom.java @@ -110,8 +110,7 @@ public Builder addUnaryOverloadTranslator( Expr val = res.get(); BoolExpr approx = argApproximations.get(0); if (isApproximated) { - BoolExpr isErrorOrUnknown = ctx.mkOr(ts.isError(val), ts.isUnknown(val)); - approx = (BoolExpr) ctx.mkITE(isErrorOrUnknown, approx, ctx.mkTrue()); + approx = (BoolExpr) ctx.mkITE(ts.isUnknown(val), approx, ctx.mkTrue()); } return Optional.of(CelZ3OverloadResult.create(val, approx)); }; diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java index 527ef70ad..292b86135 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterAxiom.java @@ -32,33 +32,25 @@ final class GreaterAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGt( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkGt(typeSystem.getInt(lhs), typeSystem.getInt(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGt( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkGt(typeSystem.getTimestamp(lhs), typeSystem.getTimestamp(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_DURATION.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGt( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkGt(typeSystem.getDuration(lhs), typeSystem.getDuration(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGt( - (ArithExpr) typeSystem.getUint(lhs), - (ArithExpr) typeSystem.getUint(rhs))))) + ctx.mkGt(typeSystem.getUint(lhs), typeSystem.getUint(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java index ec3ffa69a..4be0c23e2 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/GreaterEqualsAxiom.java @@ -32,33 +32,25 @@ final class GreaterEqualsAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGe( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkGe(typeSystem.getInt(lhs), typeSystem.getInt(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGe( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkGe(typeSystem.getTimestamp(lhs), typeSystem.getTimestamp(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_DURATION.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGe( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkGe(typeSystem.getDuration(lhs), typeSystem.getDuration(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkGe( - (ArithExpr) typeSystem.getUint(lhs), - (ArithExpr) typeSystem.getUint(rhs))))) + ctx.mkGe(typeSystem.getUint(lhs), typeSystem.getUint(rhs))))) .addBinaryOverloadTranslator( Comparison.GREATER_EQUALS_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java index 429aee284..e09484f28 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessAxiom.java @@ -32,33 +32,25 @@ final class LessAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLt( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkLt(typeSystem.getInt(lhs), typeSystem.getInt(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLt( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkLt(typeSystem.getTimestamp(lhs), typeSystem.getTimestamp(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_DURATION.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLt( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkLt(typeSystem.getDuration(lhs), typeSystem.getDuration(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLt( - (ArithExpr) typeSystem.getUint(lhs), - (ArithExpr) typeSystem.getUint(rhs))))) + ctx.mkLt(typeSystem.getUint(lhs), typeSystem.getUint(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java index 5099850dd..e27b47631 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/LessEqualsAxiom.java @@ -32,33 +32,25 @@ final class LessEqualsAxiom { (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLe( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkLe(typeSystem.getInt(lhs), typeSystem.getInt(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLe( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkLe(typeSystem.getTimestamp(lhs), typeSystem.getTimestamp(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_DURATION.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLe( - (ArithExpr) typeSystem.getInt(lhs), - (ArithExpr) typeSystem.getInt(rhs))))) + ctx.mkLe(typeSystem.getDuration(lhs), typeSystem.getDuration(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_UINT64.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> Optional.of( typeSystem.wrapBool( - ctx.mkLe( - (ArithExpr) typeSystem.getUint(lhs), - (ArithExpr) typeSystem.getUint(rhs))))) + ctx.mkLe(typeSystem.getUint(lhs), typeSystem.getUint(rhs))))) .addBinaryOverloadTranslator( Comparison.LESS_EQUALS_DOUBLE.celOverloadDecl(), (ctx, typeSystem, constraintSink, lhs, rhs) -> diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/SubtractAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/SubtractAxiom.java index bd0ecf882..3bedacf8c 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/SubtractAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/SubtractAxiom.java @@ -14,27 +14,64 @@ package dev.cel.verifier.axioms; +import com.microsoft.z3.ArithExpr; import com.microsoft.z3.BoolExpr; import com.microsoft.z3.Expr; -import com.microsoft.z3.FPExpr; import com.microsoft.z3.IntExpr; import dev.cel.checker.CelStandardDeclarations.StandardFunction; +import dev.cel.verifier.CelZ3TypeSystem; import java.util.Optional; +import java.util.function.BiFunction; /** Axiomatization for CEL's subtraction operator (-). */ final class SubtractAxiom { + @SuppressWarnings("Immutable") // Actually immutable -- BiFunction just isn't annotated as such. + private static CelZ3FunctionAxiom.BinaryTranslator createSubtractTranslator( + BiFunction, IntExpr> getLeft, + BiFunction, IntExpr> getRight, + BiFunction> wrapResult, + BiFunction, BoolExpr> overflowChecker) { + return (ctx, ts, sink, l, r) -> { + IntExpr a1 = getLeft.apply(ts, l); + IntExpr a2 = getRight.apply(ts, r); + ArithExpr subtraction = ctx.mkSub(a1, a2); + Expr result = wrapResult.apply(ts, (IntExpr) subtraction); + BoolExpr overflow = overflowChecker.apply(ts, subtraction); + return Optional.of(ts.withRuntimeError(result, overflow)); + }; + } + static final CelZ3FunctionAxiom INSTANCE = CelZ3FunctionAxiom.newBuilder(StandardFunction.SUBTRACT.functionDecl()) .addBinaryOverloadTranslator( StandardFunction.Overload.Arithmetic.SUBTRACT_INT64.celOverloadDecl(), - (ctx, ts, sink, l, r) -> { - IntExpr a1 = ts.getInt(l); - IntExpr a2 = ts.getInt(r); - Expr result = ts.wrapInt((IntExpr) ctx.mkSub(a1, a2)); - BoolExpr overflow = ts.checkIntOverflow(ctx.mkSub(a1, a2)); - return Optional.of(ts.withRuntimeError(result, overflow)); - }) + createSubtractTranslator( + CelZ3TypeSystem::getInt, + CelZ3TypeSystem::getInt, + CelZ3TypeSystem::wrapInt, + CelZ3TypeSystem::checkIntOverflow)) + .addBinaryOverloadTranslator( + StandardFunction.Overload.Arithmetic.SUBTRACT_TIMESTAMP_TIMESTAMP.celOverloadDecl(), + createSubtractTranslator( + CelZ3TypeSystem::getTimestamp, + CelZ3TypeSystem::getTimestamp, + CelZ3TypeSystem::wrapDuration, + CelZ3TypeSystem::checkDurationOverflow)) + .addBinaryOverloadTranslator( + StandardFunction.Overload.Arithmetic.SUBTRACT_TIMESTAMP_DURATION.celOverloadDecl(), + createSubtractTranslator( + CelZ3TypeSystem::getTimestamp, + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::wrapTimestamp, + CelZ3TypeSystem::checkTimestampOverflow)) + .addBinaryOverloadTranslator( + StandardFunction.Overload.Arithmetic.SUBTRACT_DURATION_DURATION.celOverloadDecl(), + createSubtractTranslator( + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::getDuration, + CelZ3TypeSystem::wrapDuration, + CelZ3TypeSystem::checkDurationOverflow)) .addBinaryOverloadTranslator( StandardFunction.Overload.Arithmetic.SUBTRACT_UINT64.celOverloadDecl(), (ctx, ts, sink, l, r) -> { @@ -50,9 +87,7 @@ final class SubtractAxiom { Optional.of( ts.wrapDouble( ctx.mkFPSub( - ctx.mkFPRoundNearestTiesToEven(), - (FPExpr) ts.getDouble(l), - (FPExpr) ts.getDouble(r))))) + ctx.mkFPRoundNearestTiesToEven(), ts.getDouble(l), ts.getDouble(r))))) .build(); private SubtractAxiom() {} diff --git a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java index fc4757686..9c49ef958 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeAxiom.java @@ -61,6 +61,8 @@ private static Expr getTypeExpression(Context ctx, CelZ3TypeSystem typeSystem typeSystem.wrapString(typeSystem.getMsgTypeName(typeSystem.getMessageRef(val)))) .addCase(typeSystem.isOptional(val), typeSystem.mkString(OptionalType.NAME)) .addCase(typeSystem.isNull(val), typeSystem.mkString(SimpleType.NULL_TYPE.name())) + .addCase(typeSystem.isTimestamp(val), typeSystem.mkString(SimpleType.TIMESTAMP.name())) + .addCase(typeSystem.isDuration(val), typeSystem.mkString(SimpleType.DURATION.name())) .addCase(typeSystem.isMap(val), typeSystem.mkString(TYPE_NAME_MAP)) .addCase(typeSystem.isList(val), typeSystem.mkString(TYPE_NAME_LIST)) .addCase(typeSystem.isBytes(val), typeSystem.mkString(SimpleType.BYTES.name())) 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 94bdf0651..8cd844214 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 com.microsoft.z3.Sort; import dev.cel.checker.CelStandardDeclarations.StandardFunction; import dev.cel.checker.CelStandardDeclarations.StandardFunction.Overload.Conversions; +import dev.cel.common.types.SimpleType; import java.util.Optional; /** Axiomatization for CEL's type conversion functions. */ @@ -43,18 +44,16 @@ final class TypeConversionAxioms { return Optional.of( typeSystem.withRuntimeError(typeSystem.wrapInt(uintVal), outOfBounds)); }) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.DOUBLE_TO_INT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.DOUBLE_TO_INT64), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.DOUBLE_TO_INT64)) + .addOverloadTranslator( Conversions.STRING_TO_INT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_INT64), - true) + createUninterpretedConversion(Conversions.STRING_TO_INT64)) .addUnaryOverloadTranslator( Conversions.TIMESTAMP_TO_INT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.TIMESTAMP_TO_INT64), - true) + (ctx, typeSystem, sink, arg) -> + Optional.of(typeSystem.wrapInt(typeSystem.getTimestamp(arg)))) .build(); private static final CelZ3FunctionAxiom UINT_AXIOM = @@ -70,14 +69,12 @@ final class TypeConversionAxioms { return Optional.of( typeSystem.withRuntimeError(typeSystem.wrapUint(intVal), outOfBounds)); }) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.DOUBLE_TO_UINT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.DOUBLE_TO_UINT64), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.DOUBLE_TO_UINT64)) + .addOverloadTranslator( Conversions.STRING_TO_UINT64.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_UINT64), - true) + createUninterpretedConversion(Conversions.STRING_TO_UINT64)) .build(); private static final CelZ3FunctionAxiom DOUBLE_AXIOM = @@ -85,15 +82,13 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.DOUBLE_TO_DOUBLE.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.INT64_TO_DOUBLE.celOverloadDecl(), - createUninterpretedConversion(Conversions.INT64_TO_DOUBLE), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.INT64_TO_DOUBLE)) + .addOverloadTranslator( Conversions.UINT64_TO_DOUBLE.celOverloadDecl(), - createUninterpretedConversion(Conversions.UINT64_TO_DOUBLE), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.UINT64_TO_DOUBLE)) + .addOverloadTranslator( Conversions.STRING_TO_DOUBLE.celOverloadDecl(), createUninterpretedConversion(Conversions.STRING_TO_DOUBLE)) .build(); @@ -103,34 +98,27 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.STRING_TO_STRING.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.INT64_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.INT64_TO_STRING), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.INT64_TO_STRING)) + .addOverloadTranslator( Conversions.UINT64_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.UINT64_TO_STRING), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.UINT64_TO_STRING)) + .addOverloadTranslator( Conversions.DOUBLE_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.DOUBLE_TO_STRING), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.DOUBLE_TO_STRING)) + .addOverloadTranslator( Conversions.BOOL_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.BOOL_TO_STRING), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.BOOL_TO_STRING)) + .addOverloadTranslator( Conversions.BYTES_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.BYTES_TO_STRING), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.BYTES_TO_STRING)) + .addOverloadTranslator( Conversions.TIMESTAMP_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.TIMESTAMP_TO_STRING), - true) - .addUnaryOverloadTranslator( + createUninterpretedConversion(Conversions.TIMESTAMP_TO_STRING)) + .addOverloadTranslator( Conversions.DURATION_TO_STRING.celOverloadDecl(), - createUninterpretedConversion(Conversions.DURATION_TO_STRING), - true) + createUninterpretedConversion(Conversions.DURATION_TO_STRING)) .build(); private static final CelZ3FunctionAxiom BYTES_AXIOM = @@ -138,10 +126,9 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.BYTES_TO_BYTES.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.STRING_TO_BYTES.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_BYTES), - true) + createUninterpretedConversion(Conversions.STRING_TO_BYTES)) .build(); private static final CelZ3FunctionAxiom DYN_AXIOM = @@ -156,10 +143,9 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.DURATION_TO_DURATION.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.STRING_TO_DURATION.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_DURATION), - true) + createUninterpretedConversion(Conversions.STRING_TO_DURATION)) .build(); private static final CelZ3FunctionAxiom TIMESTAMP_AXIOM = @@ -167,14 +153,17 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.TIMESTAMP_TO_TIMESTAMP.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.STRING_TO_TIMESTAMP.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_TIMESTAMP), - true) + createUninterpretedConversion(Conversions.STRING_TO_TIMESTAMP)) .addUnaryOverloadTranslator( Conversions.INT64_TO_TIMESTAMP.celOverloadDecl(), - createUninterpretedConversion(Conversions.INT64_TO_TIMESTAMP), - true) + (ctx, typeSystem, sink, arg) -> { + IntExpr intVal = typeSystem.getInt(arg); + BoolExpr overflow = typeSystem.checkTimestampOverflow(intVal); + return Optional.of( + typeSystem.withRuntimeError(typeSystem.wrapTimestamp(intVal), overflow)); + }) .build(); private static final CelZ3FunctionAxiom BOOL_AXIOM = @@ -182,10 +171,9 @@ final class TypeConversionAxioms { .addUnaryOverloadTranslator( Conversions.BOOL_TO_BOOL.celOverloadDecl(), (ctx, typeSystem, sink, arg) -> Optional.of(arg)) - .addUnaryOverloadTranslator( + .addOverloadTranslator( Conversions.STRING_TO_BOOL.celOverloadDecl(), - createUninterpretedConversion(Conversions.STRING_TO_BOOL), - true) + createUninterpretedConversion(Conversions.STRING_TO_BOOL)) .build(); static final ImmutableList ALL_AXIOMS = @@ -200,9 +188,11 @@ final class TypeConversionAxioms { TIMESTAMP_AXIOM, BOOL_AXIOM); - private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion( - Conversions conversion) { - return (ctx, typeSystem, sink, arg) -> { + private static CelZ3OverloadTranslator createUninterpretedConversion(Conversions conversion) { + return (ctx, typeSystem, sink, unwrappedArgs, argApproximations) -> { + Expr arg = unwrappedArgs.get(0); + BoolExpr baseApprox = argApproximations.get(0); + FuncDecl funcDecl = typeSystem.internFuncDecl( conversion.celOverloadDecl().overloadId(), @@ -212,32 +202,63 @@ private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion( switch (conversion.celOverloadDecl().resultType().kind()) { case INT: + sink.accept(ctx.mkOr(typeSystem.isInt(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( + typeSystem.isInt(res), + ctx.mkNot(typeSystem.checkIntOverflow(typeSystem.getInt(res))))); + break; case TIMESTAMP: + sink.accept(ctx.mkOr(typeSystem.isTimestamp(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( + typeSystem.isTimestamp(res), + ctx.mkNot(typeSystem.checkTimestampOverflow(typeSystem.getTimestamp(res))))); + break; case DURATION: - sink.accept(typeSystem.isInt(res)); - sink.accept(ctx.mkNot(typeSystem.checkIntOverflow(typeSystem.getInt(res)))); + sink.accept(ctx.mkOr(typeSystem.isDuration(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( + typeSystem.isDuration(res), + ctx.mkNot(typeSystem.checkDurationOverflow(typeSystem.getDuration(res))))); break; case UINT: - sink.accept(typeSystem.isUint(res)); - sink.accept(ctx.mkNot(typeSystem.checkUintOverflow(typeSystem.getUint(res)))); + sink.accept(ctx.mkOr(typeSystem.isUint(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( + typeSystem.isUint(res), + ctx.mkNot(typeSystem.checkUintOverflow(typeSystem.getUint(res))))); break; case DOUBLE: - sink.accept(typeSystem.isDouble(res)); - sink.accept(ctx.mkNot(ctx.mkFPIsNaN((FPExpr) typeSystem.getDouble(res)))); + sink.accept(ctx.mkOr(typeSystem.isDouble(res), typeSystem.isError(res))); + sink.accept( + ctx.mkImplies( + typeSystem.isDouble(res), + ctx.mkNot(ctx.mkFPIsNaN((FPExpr) typeSystem.getDouble(res))))); break; case STRING: - sink.accept(typeSystem.isString(res)); + sink.accept(ctx.mkOr(typeSystem.isString(res), typeSystem.isError(res))); break; case BYTES: - sink.accept(typeSystem.isBytes(res)); + sink.accept(ctx.mkOr(typeSystem.isBytes(res), typeSystem.isError(res))); break; case BOOL: - sink.accept(typeSystem.isBool(res)); + sink.accept(ctx.mkOr(typeSystem.isBool(res), typeSystem.isError(res))); break; default: - break; + throw new IllegalArgumentException( + "Unsupported uninterpreted conversion result type: " + + conversion.celOverloadDecl().resultType()); } - return Optional.of(res); + + boolean isArgConstant = typeSystem.isPrimitiveConstant(arg); + boolean isStringParseConversion = + conversion.celOverloadDecl().parameterTypes().get(0).equals(SimpleType.STRING); + + BoolExpr finalApprox = + (!isArgConstant && isStringParseConversion) ? baseApprox : ctx.mkTrue(); + + return Optional.of(CelZ3OverloadResult.create(res, finalApprox)); }; } diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 59a5e8438..5a7ad7093 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -93,7 +93,10 @@ public final class CelVerifierZ3ImplTest { .addVar("b", SimpleType.BOOL) .addVar("role", SimpleType.STRING) .addVar("country", SimpleType.STRING) + .addVar("string_var", SimpleType.STRING) .addVar("port", SimpleType.INT) + .addVar("dur", SimpleType.DURATION) + .addVar("ts", SimpleType.TIMESTAMP) .addVar("request", SimpleType.DYN) .addVar("unknown_var", SimpleType.DYN) .addVar("int_list", ListType.create(SimpleType.INT)) @@ -151,8 +154,6 @@ private enum IsSatisfiableTestCase { NULL_SATISFIABLE("unknown_var == null"), DYNAMIC_VAR_NUMERIC_EQUALITY("dyn_var == 1 && dyn_var == 1.0"), DYNAMIC_VAR_NOT_IN_LIST("dyn_var == 1.5 && !(dyn_var in dyn_list) && size(dyn_list) > 5"), - TIMESTAMP_EQUALITY_TAUTOLOGY( - "timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"), CROSS_NUMERIC_EQUALITY_INT_DYN_EXACT("1 == request"), MACRO_LIMIT("dyn_list.all(x, x == 1)"), STRUCT_FIELD_MISSING_APPROXIMATE_SATISFIABLE("dyn_var.unknown_field"), @@ -288,7 +289,9 @@ private enum IsUnsatisfiableTestCase { TYPE_CONVERSION_UNSATISFIABLE_DOUBLE_TO_STRING("type(string(1.5)) == int"), EMPTY_MAP_SIZE_NOT_ZERO("size({}) != 0"), TIMESTAMP_INEQUALITY_CONTRADICTION( - "timestamp('2023-01-01T00:00:00Z') != timestamp('2023-01-01T00:00:00Z')"); + "timestamp('2023-01-01T00:00:00Z') != timestamp('2023-01-01T00:00:00Z')"), + TYPE_TIMESTAMP_NOT_INT("type(timestamp('1970-01-01T00:00:00Z')) == int"), + DYN_INT_NOT_DURATION("dyn(1) == dyn(duration('1s'))"); final String expr; @@ -321,6 +324,15 @@ public void isSatisfiable_timeout_throwsException() throws Exception { private enum IsAlwaysTrueTestCase { LOGICAL_OR_CONSTANTS("true || false"), + TIMESTAMP_GREATER_EQUALS("timestamp(200) >= timestamp(100)"), + DURATION_GREATER_EQUALS( + "(timestamp(200) - timestamp(100)) >= (timestamp(150) - timestamp(100))"), + DURATION_GREATER("(timestamp(200) - timestamp(100)) > (timestamp(150) - timestamp(100))"), + TIMESTAMP_LESS("timestamp(100) < timestamp(200)"), + 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)"), 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)"), @@ -655,29 +667,7 @@ private enum IsAlwaysTrueTestCase { TYPE_CONVERSION_DYN_IDENTITY("dyn(1) == 1"), TYPE_CONVERSION_UINT_TO_INT("int(1u) == 1"), TYPE_CONVERSION_INT_TO_UINT("uint(1) == 1u"), - TYPE_CONVERSION_INT_FROM_DOUBLE("int(1.0) == int(1.0)"), - TYPE_CONVERSION_INT_FROM_STRING("int('1') == int('1')"), - TYPE_CONVERSION_INT_FROM_TIMESTAMP( - "int(timestamp('1970-01-01T00:00:00Z')) == int(timestamp('1970-01-01T00:00:00Z'))"), - TYPE_CONVERSION_UINT_FROM_DOUBLE("uint(1.0) == uint(1.0)"), - TYPE_CONVERSION_UINT_FROM_STRING("uint('1') == uint('1')"), - TYPE_CONVERSION_DOUBLE_FROM_INT("double(1) == double(1)"), - TYPE_CONVERSION_DOUBLE_FROM_UINT("double(1u) == double(1u)"), - TYPE_CONVERSION_DOUBLE_FROM_STRING("double('1.0') == double('1.0')"), - TYPE_CONVERSION_STRING_FROM_INT("string(1) == string(1)"), - TYPE_CONVERSION_STRING_FROM_UINT("string(1u) == string(1u)"), - TYPE_CONVERSION_STRING_FROM_DOUBLE("string(1.0) == string(1.0)"), - TYPE_CONVERSION_STRING_FROM_BOOL("string(true) == string(true)"), - TYPE_CONVERSION_STRING_FROM_BYTES("string(b'foo') == string(b'foo')"), - TYPE_CONVERSION_STRING_FROM_TIMESTAMP( - "string(timestamp('1970-01-01T00:00:00Z')) == string(timestamp('1970-01-01T00:00:00Z'))"), - TYPE_CONVERSION_STRING_FROM_DURATION("string(duration('1s')) == string(duration('1s'))"), - TYPE_CONVERSION_BYTES_FROM_STRING("bytes('foo') == bytes('foo')"), - TYPE_CONVERSION_DURATION_FROM_STRING("duration('1s') == duration('1s')"), - TYPE_CONVERSION_TIMESTAMP_FROM_STRING( - "timestamp('1970-01-01T00:00:00Z') == timestamp('1970-01-01T00:00:00Z')"), TYPE_CONVERSION_TIMESTAMP_FROM_INT("timestamp(1) == timestamp(1)"), - TYPE_CONVERSION_BOOL_FROM_STRING("bool('true') == bool('true')"), TYPE_CONVERSION_INT_TO_UINT_ZERO("uint(0) == 0u"), TYPE_AXIOM_OPTIONAL("type(optional.of(1)) == optional_type"), @@ -954,7 +944,11 @@ private enum UnconditionalErrorTestCase { COLLECTION_ERROR("{'a': 1 / 0} == {'a': 1 / 0}"), LIST_ERROR("[1 / 0] == [1 / 0]"), STRICT_LITERAL_ERROR("{'a': 1/0}.exists(k, k == 'a') == {'a': 1/0}.exists(k, k == 'a')"), - STRICT_LITERAL_ERROR_KEY("{1/0: 'a'}.exists(k, k == 1) == {1/0: 'a'}.exists(k, k == 1)"); + STRICT_LITERAL_ERROR_KEY("{1/0: 'a'}.exists(k, k == 1) == {1/0: 'a'}.exists(k, k == 1)"), + TIMESTAMP_INT_CONVERSION_OUT_OF_BOUNDS( + "timestamp(999999999999999) == timestamp(999999999999999)"), + TIMESTAMP_INT_CONVERSION_UNDERFLOW( + "timestamp(-999999999999999) == timestamp(-999999999999999)"); final String expr; @@ -1075,6 +1069,58 @@ public void verifyEquivalence_infinityConstants_notEquivalent() throws Exception private enum IsAlwaysTrueViolationTestCase { NOT_ALWAYS_TRUE( "x > 5", "Condition is not always true\\.", "Counterexample input:", "x = -?\\d+"), + UNINTERPRETED_CONVERSION_CAN_ERROR_INT( + "int(request) == int(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_UINT( + "uint(request) == uint(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_DOUBLE( + "double(request) == double(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_TIMESTAMP( + "timestamp(request) == timestamp(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_BOOL( + "bool(request) == bool(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_STRING( + "string(request) == string(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_BYTES( + "bytes(request) == bytes(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + UNINTERPRETED_CONVERSION_CAN_ERROR_DURATION( + "duration(request) == duration(request)", + "Condition is not always true\\.", + "Counterexample input:", + "request = .*"), + DURATION_VARIABLE_COUNTEREXAMPLE( + "dur != dur", + "Condition is not always true\\.", + "Counterexample input:", + "dur = duration\\(-?\\d+\\)"), + TIMESTAMP_VARIABLE_COUNTEREXAMPLE( + "ts != ts", + "Condition is not always true\\.", + "Counterexample input:", + "ts = timestamp\\(-?\\d+\\)"), + UNINTERPRETED_CONVERSION_NULL_FAILS_WITH_ERRORS( + "string(null) == string(null)", "Condition is not always true\\."), LAW_OF_EXCLUDED_MIDDLE_FAILS_WITH_ERRORS( "(1 / 0 == 5) || !(1 / 0 == 5)", "Condition is not always true\\."), INTEGER_OVERFLOW_FAILS_WITH_ERRORS( @@ -1087,6 +1133,12 @@ private enum IsAlwaysTrueViolationTestCase { "Condition is not always true\\.", "Counterexample input:", "u = \\d+u?"), + CROSS_TYPE_DYNAMIC_EQUALITY_NOT_ALWAYS_UNEQUAL_INT_DOUBLE( + "!(request == unknown_var && type(request) == int && type(unknown_var) == double)", + "Condition is not always true\\.", + "Counterexample input:", + "unknown_var = -?\\d+\\.\\d+", + "request = -?\\d+"), NEGATE_MIN_INT_FAILS_WITH_ERRORS( "-(-x) == x", "Condition is not always true\\.", "Counterexample input:", "x = -?\\d+"), HETEROGENEOUS_ARITHMETIC_FAILS("dyn(1) + 1u == 2u", "Condition is not always true\\."), @@ -1102,12 +1154,6 @@ private enum IsAlwaysTrueViolationTestCase { "Counterexample input:", "x = -?\\d+", "u = \\d+u?"), - CROSS_TYPE_DYNAMIC_EQUALITY_NOT_ALWAYS_UNEQUAL_INT_DOUBLE( - "!(request == unknown_var && type(request) == int && type(unknown_var) == double)", - "Condition is not always true\\.", - "Counterexample input:", - "unknown_var = -?\\d+\\.\\d+", - "request = -?\\d+"), OPTIONAL_DYN_VAR_HAS_VALUE_NOT_IMPLIES_INT( "opt_dyn_var.hasValue() ? type(opt_dyn_var.value()) == int : true", "Condition is not always true\\.", @@ -1117,18 +1163,18 @@ private enum IsAlwaysTrueViolationTestCase { "[?dyn_var] == [?dyn_var] ? true : true", "Condition is not always true\\.", "Counterexample input:", - "dyn_var = b\"![01]!\""), + "dyn_var = .*"), OPTIONAL_MAP_ENTRY_DYN_VAR_TYPE_MISMATCH( "{?1: dyn_var} == {?1: dyn_var} ? true : true", "Condition is not always true\\.", "Counterexample input:", - "dyn_var = b\"![01]!\""), + "dyn_var = .*"), OPTIONAL_STRUCT_ENTRY_DYN_VAR_TYPE_MISMATCH( "cel.expr.conformance.proto3.TestAllTypes{?single_int32: dyn_var} ==" + " cel.expr.conformance.proto3.TestAllTypes{?single_int32: dyn_var} ? true : true", "Condition is not always true\\.", "Counterexample input:", - "dyn_var = b\"(!0!|i)\""), + "dyn_var = .*"), OPTIONAL_NONE_COUNTEREXAMPLE( "opt_dyn_var.hasValue()", "Condition is not always true\\.", @@ -1235,7 +1281,7 @@ private enum IsAlwaysTrueViolationTestCase { "dyn_var == 1.0", "Condition is not always true\\.", "Counterexample input:", - "dyn_var = b\"![01]!\""), + "dyn_var = .*"), DYNAMIC_NOT_TYPE_MISMATCH( "!dyn_var", "Condition is not always true\\.", @@ -1245,7 +1291,7 @@ private enum IsAlwaysTrueViolationTestCase { "dyn_var ? true : false", "Condition is not always true\\.", "Counterexample input:", - "dyn_var = b\"![01]!\""), + "dyn_var = .*"), DYNAMIC_NOT_TYPE_MISMATCH_SURVIVOR( "type(dyn_var) == int ? (!dyn_var == !dyn_var) : true", "Condition is not always true\\.", @@ -1292,6 +1338,22 @@ private enum IsAlwaysTrueViolationTestCase { "Counterexample input:", "x = -9223372036854775808", "y = -1"), + UNINTERPRETED_CONVERSION_CAN_ERROR_INT_FROM_STRING( + "int(string_var) == int(string_var)", + "Condition is not always true\\.", + "Counterexample input:"), + UNINTERPRETED_CONVERSION_CAN_ERROR_TIMESTAMP_FROM_STRING( + "timestamp(string_var) == timestamp(string_var)", + "Condition is not always true\\.", + "Counterexample input:"), + UNINTERPRETED_CONVERSION_CAN_ERROR_DURATION_FROM_STRING( + "duration(string_var) == duration(string_var)", + "Condition is not always true\\.", + "Counterexample input:"), + UNINTERPRETED_CONVERSION_CAN_ERROR_BOOL_FROM_STRING( + "bool(string_var) == bool(string_var)", + "Condition is not always true\\.", + "Counterexample input:"), ; final String expr; @@ -1317,6 +1379,17 @@ public void isAlwaysTrue_violation_returnsFalse( } private enum IsInconclusiveTestCase { + // TODO: Implement RFC 3339 spec in conversion + TIMESTAMP_STRING_CONVERSION_VALID( + "timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"), + DURATION_STRING_CONVERSION_VALID("duration('100s') == duration('100s')"), + BOOL_STRING_UNINTERPRETED("bool('true') == true"), + TIMESTAMP_ADD_DURATION_OVERFLOW("timestamp(253402300799) + duration('100s') > timestamp(0)"), + DYNAMIC_EQUALITY_TIMESTAMP_INT_COLLISION( + "type(dyn_var) == int && dyn_var == 0 ? dyn_var != timestamp('1970-01-01T00:00:00Z') :" + + " true"), + // TODO: Implement RFC 3339 spec in conversion + TIMESTAMP_BOUNDS_VALID("timestamp('2023-01-01T00:00:00Z') <= timestamp(253402300799)"), UNINTERPRETED_FUNCTION("request.matches('^[a-z]+$')"), INT_STRING_UNINTERPRETED("int('123') == 123"), LIST_WITH_APPROXIMATE_ELEMENT("[request.matches('a')]"), @@ -1398,7 +1471,18 @@ private enum EquivalenceInconclusiveTestCase { "size(int_list) == 6 ? int_list.map(x, 2.0) : [1.0]"), TRUNCATION_DIVERGENCE_DIFFERENT_BYTES( "size(int_list) == 6 ? int_list.map(x, b'a') : [b'a']", - "size(int_list) == 6 ? int_list.map(x, b'b') : [b'a']"); + "size(int_list) == 6 ? int_list.map(x, b'b') : [b'a']"), + TIMESTAMP_MATH_ADD_DUR_TS("timestamp(100) + duration('100s')", "timestamp(200)"), + TIMESTAMP_MATH_ADD_TS_DUR("duration('100s') + timestamp(100)", "timestamp(200)"), + TIMESTAMP_MATH_SUBTRACT_DUR("timestamp(900000) - duration('100s')", "timestamp(899900)"), + DURATION_MATH_ADD_DUR_DUR("duration('100s') + duration('200s')", "duration('300s')"), + DURATION_MATH_SUBTRACT_DUR_DUR("duration('300s') - duration('100s')", "duration('200s')"), + DURATION_MATH_ASSOCIATIVITY( + "(duration('10s') + duration('20s')) + duration('30s')", + "duration('10s') + (duration('20s') + duration('30s'))"), + TIMESTAMP_DURATION_MATH_ASSOCIATIVITY( + "(timestamp(10) + duration('20s')) + duration('30s')", + "timestamp(10) + (duration('20s') + duration('30s'))"); final String exprA; final String exprB; @@ -1421,6 +1505,7 @@ public void verifyEquivalence_inconclusive( } private enum EquivalenceTestCase { + STRUCT_UNSET_TIMESTAMP_DEFAULT("TestAllTypes{}.single_timestamp", "timestamp(0)"), TRUNCATION_STRICT_PROPAGATION_EQUIVALENT( "size(int_list) == 6 ? size(int_list.filter(x, x > 2)) : 0", "size(int_list) == 6 ? size(int_list.filter(y, y > 2)) : 0"), @@ -1438,6 +1523,12 @@ private enum EquivalenceTestCase { MACRO_EXISTS_ONE_EQUIVALENT( "[1, 2, 3].exists_one(x, x == 2)", "(1 == 2 ? 1 : 0) + (2 == 2 ? 1 : 0) + (3 == 2 ? 1 : 0) == 1"), + TIMESTAMP_MATH_SUBTRACT_TS( + "timestamp(900000) - timestamp(100)", "timestamp(899900) - timestamp(0)"), + TIMESTAMP_MATH_COMMUTATIVITY( + "duration('10s') + timestamp(50)", "timestamp(50) + duration('10s')"), + DURATION_MATH_COMMUTATIVITY( + "duration('10s') + duration('20s')", "duration('20s') + duration('10s')"), MACRO_MAP_EQUIVALENT("{1: true, 2: true, 3: true}.all(k, k > 0)", "1 > 0 && 2 > 0 && 3 > 0"), MACRO_BIND_EQUIVALENT("cel.bind(x, 10, x > 0)", "10 > 0"), NESTED_MACRO(