Use sys.get_int_max_str_digits() as the chunk size.

angr · Dec 4, 2024 · d406b26 · d406b26
1 parent 5289293
commit d406b26
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 7 deletions.
diff --git a/claripy/backends/backend_z3.py b/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):
@@ -105,11 +106,13 @@ def int_to_str_unlimited(v: int) -> str:
     :return: The string.
     """
 
+    if INT_STRING_CHUNK_SIZE is None:
+        return str(v)
+
     if v == 0:
         return "0"
 
-    CHUNK_SIZE = 640
-    MOD = 10**CHUNK_SIZE
+    MOD = 10**INT_STRING_CHUNK_SIZE
     v_str = ""
     if v < 0:
         is_negative = True
@@ -120,7 +123,7 @@ def int_to_str_unlimited(v: int) -> str:
         v_chunk = str(v % MOD)
         v //= MOD
         if v > 0:
-            v_chunk = v_chunk.zfill(CHUNK_SIZE)
+            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
 
@@ -139,6 +142,8 @@ def Z3_to_int_str(val):
     # 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:
@@ -148,20 +153,22 @@ def str_to_int_unlimited(s: str) -> int:
     :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
 
-    CHUNK_SIZE = 640
     v = 0
     if s[0] == "-":
         is_negative = True
         s = s[1:]
     else:
         is_negative = False
 
-    for i in range(0, len(s), CHUNK_SIZE):
+    for i in range(0, len(s), INT_STRING_CHUNK_SIZE):
         start = i
-        end = min(i + CHUNK_SIZE, len(s))
+        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

diff --git a/tests/test_z3.py b/tests/test_z3.py
@@ -2,6 +2,7 @@
 from __future__ import annotations
 
 import unittest
+import sys
 
 import claripy
 
@@ -41,6 +42,7 @@ def test_str2int(self):
         """
 
         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
@@ -51,21 +53,27 @@ def test_str2int(self):
         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" * 8192) == -(10**8192)
+        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