BackendZ3: Bypass integer string conversion limit.

claripy/backends/backend_z3.py

@@ -38,6 +38,7 @@
 # pylint:disable=unidiomatic-typecheck
 
 ALL_Z3_CONTEXTS = weakref.WeakSet()
+INT_STRING_CHUNK_SIZE: int | None = None  # will be updated later if we are on CPython 3.11+
 
 
 def handle_sigint(signals, frametype):
@@ -97,6 +98,82 @@ def _add_memory_pressure(p):
         __pypy__.add_memory_pressure(p)
 
 
+def int_to_str_unlimited(v: int) -> str:
+    """
+    Convert an integer to a decimal string, without any size limit.
+
+    :param v: The integer to convert.
+    :return: The string.
+    """
+
+    if INT_STRING_CHUNK_SIZE is None:
+        return str(v)
+
+    if v == 0:
+        return "0"
+
+    MOD = 10**INT_STRING_CHUNK_SIZE
+    v_str = ""
+    if v < 0:
+        is_negative = True
+        v = -v
+    else:
+        is_negative = False
+    while v > 0:
+        v_chunk = str(v % MOD)
+        v //= MOD
+        if v > 0:
+            v_chunk = v_chunk.zfill(INT_STRING_CHUNK_SIZE)
+        v_str = v_chunk + v_str
+    return v_str if not is_negative else "-" + v_str
+
+
+def Z3_to_int_str(val):
+    # we will monkey-patch Z3 and replace Z3._to_int_str with this version, which is free of integer size limits.
+
+    if isinstance(val, float):
+        return str(int(val))
+    if isinstance(val, bool):
+        return "1" if val else "0"
+    return int_to_str_unlimited(val)
+
+
+if hasattr(sys, "get_int_max_str_digits"):
+    # CPython 3.11+
+    # monkey-patch Z3 so that it can accept long integers
+    z3.z3._to_int_str = Z3_to_int_str
+    # update INT_STRING_CHUNK_SIZE
+    INT_STRING_CHUNK_SIZE = sys.get_int_max_str_digits()
+
+
+def str_to_int_unlimited(s: str) -> int:
+    """
+    Convert a decimal string to an integer, without any size limit.
+
+    :param s: The string to convert.
+    :return: The integer.
+    """
+    if INT_STRING_CHUNK_SIZE is None:
+        return int(s)
+
+    if not s:
+        return int(s)  # an exception will be raised, which is intentional
+
+    v = 0
+    if s[0] == "-":
+        is_negative = True
+        s = s[1:]
+    else:
+        is_negative = False
+
+    for i in range(0, len(s), INT_STRING_CHUNK_SIZE):
+        start = i
+        end = min(i + INT_STRING_CHUNK_SIZE, len(s))
+        v *= 10 ** (end - start)
+        v += int(s[start:end], 10)
+    return v if not is_negative else -v
+
+
 #
 # Some global variables
 #
@@ -457,7 +534,7 @@ def _abstract_internal(self, ctx, ast, split_on=None):
             bv_size = z3.Z3_get_bv_sort_size(ctx, z3_sort)
             if z3.Z3_get_numeral_uint64(ctx, ast, self._c_uint64_p):
                 return claripy.BVV(self._c_uint64_p.contents.value, bv_size)
-            bv_num = int(z3.Z3_get_numeral_string(ctx, ast))
+            bv_num = str_to_int_unlimited(z3.Z3_get_numeral_string(ctx, ast))
             return claripy.BVV(bv_num, bv_size)
         if op_name in ("FPVal", "MinusZero", "MinusInf", "PlusZero", "PlusInf", "NaN"):
             ebits = z3.Z3_fpa_get_ebits(ctx, z3_sort)
@@ -608,7 +685,7 @@ def _abstract_to_primitive(self, ctx, ast):
     def _abstract_bv_val(self, ctx, ast):
         if z3.Z3_get_numeral_uint64(ctx, ast, self._c_uint64_p):
             return self._c_uint64_p.contents.value
-        return int(z3.Z3_get_numeral_string(ctx, ast))
+        return str_to_int_unlimited(z3.Z3_get_numeral_string(ctx, ast))
 
     @staticmethod
     def _abstract_fp_val(ctx, ast, op_name):

tests/test_z3.py

@@ -1,6 +1,7 @@
 # pylint: disable=missing-class-docstring,no-self-use
 from __future__ import annotations
 
+import sys
 import unittest
 
 import claripy
@@ -35,6 +36,57 @@ def test_extrema(self):
             assert z.min(x, solver=s, extra_constraints=(x >= i,)) == i
             assert z.max(x, solver=s, extra_constraints=(x >= i,)) == range_[1]
 
+    def test_str2int(self):
+        """
+        Test the str_to_int_unlimited function.
+        """
+
+        s2i = claripy.backends.backend_z3.str_to_int_unlimited
+        CHUNK_SIZE = sys.get_int_max_str_digits() if hasattr(sys, "get_int_max_str_digits") else 640
+
+        assert s2i("0") == 0
+        assert s2i("1337") == 1337
+        assert s2i("1337133713371337") == 1337133713371337
+        assert s2i("1" + "0" * 639) == 10**639
+        assert s2i("1" + "0" * 640) == 10**640
+        assert s2i("1" + "0" * 641) == 10**641
+        assert s2i("1" + "0" * 640 + "1") == 10**641 + 1
+        assert s2i("1" + "0" * 8192) == 10**8192
+
+        assert s2i("1" + "0" * (CHUNK_SIZE - 1)) == 10 ** (CHUNK_SIZE - 1)
+        assert s2i("1" + "0" * CHUNK_SIZE) == 10**CHUNK_SIZE
+        assert s2i("1" + "0" * (CHUNK_SIZE + 1)) == 10 ** (CHUNK_SIZE + 1)
+
+        assert s2i("-0") == 0
+        assert s2i("-1") == -1
+        assert s2i("-1" + "0" * CHUNK_SIZE) == -(10**CHUNK_SIZE)
+
+    def test_int2str(self):
+        """
+        Test the int_to_str_unlimited function.
+        """
+
+        i2s = claripy.backends.backend_z3.int_to_str_unlimited
+        CHUNK_SIZE = sys.get_int_max_str_digits() if hasattr(sys, "get_int_max_str_digits") else 640
+
+        assert i2s(0) == "0"
+        assert i2s(-1) == "-1"
+        assert i2s(1337) == "1337"
+        assert i2s(10**8192) == "1" + "0" * 8192
+        assert i2s(10**CHUNK_SIZE) == "1" + "0" * CHUNK_SIZE
+
+    def test_get_long_strings(self):
+        # Python 3.11 introduced limits in decimal-to-int conversion. we bypass it by using the str_to_int_unlimited
+        # method.
+        z3 = claripy.backends.backend_z3
+
+        s = claripy.backends.z3.solver()
+        backend = z3.BackendZ3()
+        x = claripy.BVS("x", 16385 * 8)
+        backend.add(s, [x == 10**16384])
+        d = backend.eval(x, 1, solver=s)
+        assert d == [10**16384]
+
 
 if __name__ == "__main__":
     unittest.main()