Mark uninterpreted conversions with literals as approximate

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;
 

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

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",

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.

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())) {

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)