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..159a66a77 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); @@ -1269,6 +1275,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..59795c6c5 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()); diff --git a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java index af1a4688b..5c0b87fbe 100644 --- a/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java +++ b/verifier/src/main/java/dev/cel/verifier/CelZ3TypeSystem.java @@ -31,6 +31,7 @@ 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 +83,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 +179,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,30 +244,38 @@ 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; } @@ -296,6 +315,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 +355,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 +401,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 +438,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 +531,7 @@ public Expr withRuntimeError( return ctx.mkITE(condition, mkError(), result); } - Constructor unknownCons() { + public Constructor unknownCons() { return unknownCons; } @@ -582,6 +615,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 +772,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 +957,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 +1017,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..fabdd3d9b 100644 --- a/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java +++ b/verifier/src/main/java/dev/cel/verifier/axioms/TypeConversionAxioms.java @@ -19,7 +19,6 @@ import com.google.common.collect.ImmutableList; 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.Sort; @@ -53,8 +52,8 @@ final class TypeConversionAxioms { true) .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 = @@ -173,8 +172,12 @@ final class TypeConversionAxioms { true) .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 = @@ -212,18 +215,38 @@ private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion( switch (conversion.celOverloadDecl().resultType().kind()) { case INT: + BoolExpr intValid = + ctx.mkAnd( + typeSystem.isInt(res), + ctx.mkNot(typeSystem.checkIntOverflow(typeSystem.getInt(res)))); + sink.accept(intValid); + break; case TIMESTAMP: + BoolExpr timestampValid = + ctx.mkAnd( + typeSystem.isTimestamp(res), + ctx.mkNot(typeSystem.checkTimestampOverflow(typeSystem.getTimestamp(res)))); + sink.accept(timestampValid); + break; case DURATION: - sink.accept(typeSystem.isInt(res)); - sink.accept(ctx.mkNot(typeSystem.checkIntOverflow(typeSystem.getInt(res)))); + BoolExpr durationValid = + ctx.mkAnd( + typeSystem.isDuration(res), + ctx.mkNot(typeSystem.checkDurationOverflow(typeSystem.getDuration(res)))); + sink.accept(durationValid); break; case UINT: - sink.accept(typeSystem.isUint(res)); - sink.accept(ctx.mkNot(typeSystem.checkUintOverflow(typeSystem.getUint(res)))); + BoolExpr uintValid = + ctx.mkAnd( + typeSystem.isUint(res), + ctx.mkNot(typeSystem.checkUintOverflow(typeSystem.getUint(res)))); + sink.accept(uintValid); break; case DOUBLE: - sink.accept(typeSystem.isDouble(res)); - sink.accept(ctx.mkNot(ctx.mkFPIsNaN((FPExpr) typeSystem.getDouble(res)))); + BoolExpr doubleValid = + ctx.mkAnd( + typeSystem.isDouble(res), ctx.mkNot(ctx.mkFPIsNaN(typeSystem.getDouble(res)))); + sink.accept(doubleValid); break; case STRING: sink.accept(typeSystem.isString(res)); @@ -235,8 +258,11 @@ private static CelZ3FunctionAxiom.UnaryTranslator createUninterpretedConversion( sink.accept(typeSystem.isBool(res)); break; default: - break; + throw new IllegalArgumentException( + "Unsupported uninterpreted conversion result type: " + + conversion.celOverloadDecl().resultType()); } + return Optional.of(res); }; } diff --git a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java index 59a5e8438..a078beff7 100644 --- a/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java +++ b/verifier/src/test/java/dev/cel/verifier/CelVerifierZ3ImplTest.java @@ -94,6 +94,8 @@ public final class CelVerifierZ3ImplTest { .addVar("role", SimpleType.STRING) .addVar("country", 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)) @@ -288,7 +290,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 +325,22 @@ public void isSatisfiable_timeout_throwsException() throws Exception { private enum IsAlwaysTrueTestCase { LOGICAL_OR_CONSTANTS("true || false"), + DYNAMIC_EQUALITY_TIMESTAMP_INT_COLLISION( + "type(dyn_var) == int && dyn_var == 0 ? dyn_var != timestamp('1970-01-01T00:00:00Z') :" + + " true"), + TIMESTAMP_STRING_CONVERSION_VALID( + "timestamp('2023-01-01T00:00:00Z') == timestamp('2023-01-01T00:00:00Z')"), + DURATION_STRING_CONVERSION_VALID("duration('100s') == duration('100s')"), + TIMESTAMP_BOUNDS_VALID("timestamp('2023-01-01T00:00:00Z') <= timestamp(253402300799)"), + 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)"), @@ -954,7 +974,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 +1099,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 +1163,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 +1184,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 +1193,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 +1311,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 +1321,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\\.", @@ -1317,6 +1393,7 @@ public void isAlwaysTrue_violation_returnsFalse( } private enum IsInconclusiveTestCase { + TIMESTAMP_ADD_DURATION_OVERFLOW("timestamp(253402300799) + duration('100s') > timestamp(0)"), UNINTERPRETED_FUNCTION("request.matches('^[a-z]+$')"), INT_STRING_UNINTERPRETED("int('123') == 123"), LIST_WITH_APPROXIMATE_ELEMENT("[request.matches('a')]"), @@ -1398,7 +1475,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 +1509,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 +1527,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(