Fix overflow handlings for Uint, add more test cases around IntSort overflows

PiperOrigin-RevId: 952879660

Author: l46kok

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

@@ -16,6 +16,7 @@
 
 import com.google.common.collect.Lists;
 import com.google.common.collect.ObjectArrays;
+import com.google.common.primitives.UnsignedLongs;
 import com.google.errorprone.annotations.CanIgnoreReturnValue;
 import com.microsoft.z3.ArithExpr;
 import com.microsoft.z3.ArrayExpr;
@@ -300,9 +301,14 @@ public Expr<?> mkInt(long val) {
     return ctx.mkApp(intCons.ConstructorDecl(), ctx.mkInt(val));
   }
 
+  /** Creates a CelValue containing an unsigned integer from a string representation. */
+  public Expr<?> mkUint(String val) {
+    return ctx.mkApp(uintCons.ConstructorDecl(), ctx.mkInt(val));
+  }
+
   /** Creates a CelValue containing an unsigned integer. */
   public Expr<?> mkUint(long val) {
-    return ctx.mkApp(uintCons.ConstructorDecl(), ctx.mkInt(val));
+    return mkUint(UnsignedLongs.toString(val));
   }
 
   /** Creates a CelValue containing a double. */
@@ -859,10 +865,8 @@ public static BoolExpr mkNotFlattened(Context ctx, BoolExpr arg) {
     this.boolCons =
         ctx.mkConstructor(
             CONS_BOOL, IS_BOOL, new String[] {GET_BOOL}, new Sort[] {ctx.getBoolSort()}, null);
-    // Note: Z3's IntSort models unbounded mathematical integers. We do not currently use
-    // BitVecSort(64), which means CEL integer overflow semantics are not natively modeled,
-    // and bitwise operations are unsupported. We enforce 64-bit value bounds explicitly
-    // during variable constraint generation instead.
+    // We use Z3's IntSort instead of BitVecSort(64) for faster arithmetic solving without
+    // bit-blasting, explicitly enforcing 64-bit range bounds and overflow errors.
     this.intCons =
         ctx.mkConstructor(
             CONS_INT, IS_INT, new String[] {GET_INT}, new Sort[] {ctx.getIntSort()}, null);

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

@@ -84,6 +84,8 @@ public final class CelVerifierZ3ImplTest {
           .addMessageTypes(TestAllTypes.getDescriptor(), TestAllTypes.NestedMessage.getDescriptor())
           .addVar("x", SimpleType.INT)
           .addVar("u", SimpleType.UINT)
+          .addVar("u1", SimpleType.UINT)
+          .addVar("u2", SimpleType.UINT)
           .addVar("d", SimpleType.DOUBLE)
           .addVar("by", SimpleType.BYTES)
           .addVar("y", SimpleType.INT)
@@ -705,6 +707,10 @@ private enum IsAlwaysTrueTestCase {
     DYNAMIC_NUMERIC_EQUALITY_CROSS_TYPE_DYN_DOUBLE(
         "type(dyn_var) == double && dyn_var == 5.0 && dyn_var2 == 5.0 && type(dyn_var2) == double ?"
             + " dyn_var == dyn_var2 : true"),
+    INT64_BOUNDS_ALWAYS_TRUE("x <= 9223372036854775807 && x >= -9223372036854775808"),
+    UINT64_BOUNDS_ALWAYS_TRUE("u <= 18446744073709551615u && u >= 0u"),
+    MODULO_INT64_MIN_INT_BY_NEG_ONE_ALWAYS_ZERO(
+        "x == -9223372036854775808 && y == -1 ? x % y == 0 : true"),
     ;
 
     final String expr;
@@ -1203,7 +1209,44 @@ private enum IsAlwaysTrueViolationTestCase {
         "type(dyn_var) == int ? (dyn_var ? true : false) == (dyn_var ? true : false) : true",
         "Condition is not always true\\.",
         "Counterexample input:",
-        "dyn_var = int\\{\\}");
+        "dyn_var = int\\{\\}"),
+    ADD_INT64_OVERFLOW_FAILS_WITH_ERRORS(
+        "x > 0 && y > 0 ? x + y > x : true",
+        "Condition is not always true\\.",
+        "Counterexample input:",
+        "x = (1|9223372036854775807)",
+        "y = (1|9223372036854775807)"),
+    ADD_UINT64_OVERFLOW_FAILS_WITH_ERRORS(
+        "u1 > 0u && u2 > 0u ? u1 + u2 >= u1 : true",
+        "Condition is not always true\\.",
+        "Counterexample input:",
+        "u1 = (1u|18446744073709551615u)",
+        "u2 = (1u|18446744073709551615u)"),
+    SUBTRACT_INT64_UNDERFLOW_FAILS_WITH_ERRORS(
+        "x < 0 && y > 0 ? x - y < x : true",
+        "Condition is not always true\\.",
+        "Counterexample input:",
+        "x = (-2|9223372036854775807)",
+        "y = (-2|9223372036854775807)"),
+    MULTIPLY_INT64_OVERFLOW_FAILS_WITH_ERRORS(
+        "x > 1000000000 && y > 1000000000 ? x * y > 0 : true",
+        "Condition is not always true\\.",
+        "Counterexample input:",
+        "x = [0-9]+",
+        "y = [0-9]+"),
+    MULTIPLY_UINT64_OVERFLOW_FAILS_WITH_ERRORS(
+        "u1 > 1000000000u && u2 > 1000000000u ? u1 * u2 > 0u : true",
+        "Condition is not always true\\.",
+        "Counterexample input:",
+        "u1 = [0-9]+u",
+        "u2 = [0-9]+u"),
+    DIVIDE_INT64_OVERFLOW_MIN_INT_BY_NEG_ONE_FAILS_WITH_ERRORS(
+        "x == -9223372036854775808 && y == -1 ? x / y == -x : true",
+        "Condition is not always true\\.",
+        "Counterexample input:",
+        "x = -9223372036854775808",
+        "y = -1"),
+    ;
 
     final String expr;
     final ImmutableList<String> expectedFragments;