Always use BV64 returns in string ops

claripy/ast/strings.py

@@ -167,7 +167,7 @@ def StringV(value, length: int | None = None, **kwargs):
 
 StrConcat = operations.op("StrConcat", String, String, calc_length=operations.str_concat_length_calc)
 StrSubstr = operations.op("StrSubstr", (BV, BV, String), String, calc_length=operations.substr_length_calc)
-StrLen = operations.op("StrLen", (String, int), BV, calc_length=operations.strlen_bv_size_calc)
+StrLen = operations.op("StrLen", (String), BV, calc_length=lambda *_: 64)
 StrReplace = operations.op(
     "StrReplace",
     (String, String, String),
@@ -178,8 +178,8 @@ def StringV(value, length: int | None = None, **kwargs):
 StrContains = operations.op("StrContains", (String, String), Bool)
 StrPrefixOf = operations.op("StrPrefixOf", (String, String), Bool)
 StrSuffixOf = operations.op("StrSuffixOf", (String, String), Bool)
-StrIndexOf = operations.op("StrIndexOf", (String, String, BV, int), BV, calc_length=operations.strindexof_bv_size_calc)
-StrToInt = operations.op("StrToInt", (String, int), BV, calc_length=operations.strtoint_bv_size_calc)
+StrIndexOf = operations.op("StrIndexOf", (String, String, BV), BV, calc_length=lambda *_: 64)
+StrToInt = operations.op("StrToInt", (String), BV, calc_length=lambda *_: 64)
 IntToStr = operations.op("IntToStr", (BV,), String, calc_length=operations.int_to_str_length_calc)
 StrIsDigit = operations.op("StrIsDigit", (String,), Bool)
 

claripy/backends/backend_z3.py

@@ -1231,8 +1231,8 @@ def _op_raw_StrSubstr(start_idx, count, initial_string):
 
     @staticmethod
     @condom
-    def _op_raw_StrLen(input_string, bitlength):
-        return z3.Int2BV(z3.Length(input_string), bitlength)
+    def _op_raw_StrLen(input_string):
+        return z3.Int2BV(z3.Length(input_string), 64)
 
     @staticmethod
     @condom
@@ -1256,13 +1256,13 @@ def _op_raw_StrSuffixOf(suffix, input_string):
 
     @staticmethod
     @condom
-    def _op_raw_StrIndexOf(string, pattern, start_idx, bitlength):
-        return z3.Int2BV(z3.IndexOf(string, pattern, z3.BV2Int(start_idx)), bitlength)
+    def _op_raw_StrIndexOf(string, pattern, start_idx):
+        return z3.Int2BV(z3.IndexOf(string, pattern, z3.BV2Int(start_idx)), 64)
 
     @staticmethod
     @condom
-    def _op_raw_StrToInt(input_string, bitlength):
-        return z3.Int2BV(z3.StrToInt(input_string), bitlength)
+    def _op_raw_StrToInt(input_string):
+        return z3.Int2BV(z3.StrToInt(input_string), 64)
 
     @staticmethod
     @condom

claripy/operations.py

@@ -212,18 +212,6 @@ def str_replace_length_calc(*args):
     return str_1.length - str_2.length + str_3.length
 
 
-def strlen_bv_size_calc(s, bitlength):  # pylint: disable=unused-argument
-    return bitlength
-
-
-def strindexof_bv_size_calc(s1, s2, start_idx, bitlength):  # pylint: disable=unused-argument
-    return bitlength
-
-
-def strtoint_bv_size_calc(s, bitlength):  # pylint: disable=unused-argument
-    return bitlength
-
-
 #
 # Operation lists
 #

claripy/strings.py

@@ -56,16 +56,15 @@ def StrReplace(initial_string, pattern_to_be_replaced, replacement_pattern):
     return StringV(new_value)
 
 
-def StrLen(input_string, bitlength):
+def StrLen(input_string):
     """
     Return length of the `input_string` in bytes.
 
     :param input_string:            the string we want to calculate the length
-    :param bitlength:               length of the bitvector representing the length of the string
 
     :return:                        bitvector holding the size of the string in bytes
     """
-    return BVV(len(input_string.value), bitlength)
+    return BVV(len(input_string.value), 64)
 
 
 def StrContains(input_string, substring):
@@ -105,41 +104,39 @@ def StrSuffixOf(suffix, input_string):
     return re.match(r".*" + suffix.value + "$", input_string.value) is not None
 
 
-def StrIndexOf(input_string, substring, startIndex, bitlength):
+def StrIndexOf(input_string, substring, startIndex):
     """
     Return the index of the first occurrence of `substring` at or after the `startIndex`, or -1 if
     it is not found.
 
     :param input_string:            the string we want to check
     :param substring:               the substring we want to find the index
     :param startIndex:              the index to start searching at
-    :param bitlength:               length of the bitvector representing the index of the substring
 
     :return BV:                     index of the substring or -1 in bitvector
     """
     try:
         s = input_string.value
         t = substring.value
         i = startIndex.value
-        return BVV(i + s[i:].index(t), bitlength)
+        return BVV(i + s[i:].index(t), 64)
     except ValueError:
-        return BVV(-1, bitlength)
+        return BVV(-1, 64)
 
 
-def StrToInt(input_string, bitlength):
+def StrToInt(input_string):
     """
     Return the integer representation of `input_string`.
 
     :param input_string:            the string we want to transform in an integer
-    :param bitlength:               length of the bitvector representing the index of the substring
 
     :return BV:                     bitvector of the integer resulting from the string or -1 in
                                     bitvector if the string cannot be transformed into an integer
     """
     try:
-        return BVV(int(input_string.value), bitlength)
+        return BVV(int(input_string.value), 64)
     except ValueError:
-        return BVV(-1, bitlength)
+        return BVV(-1, 64)
 
 
 def StrIsDigit(input_string):

tests/test_strings.py

@@ -100,7 +100,7 @@ def test_length(self):
         str_symb = claripy.StringS("symb_length", 12, explicit_name=True)
         solver = self.get_solver()
         # TODO: How do we want to deal with the size of a symbolic string?
-        solver.add(claripy.StrLen(str_symb, 32) == 14)
+        solver.add(claripy.StrLen(str_symb) == 14)
         self.assertTrue(solver.satisfiable())
 
         result = solver.eval(str_symb, 4 if KEEP_TEST_PERFORMANT else 100)
@@ -110,7 +110,7 @@ def test_length(self):
     def test_length_simplification(self):
         str_concrete = claripy.StringV("concrete")
         solver = self.get_solver()
-        solver.add(claripy.StrLen(str_concrete, 32) == 8)
+        solver.add(claripy.StrLen(str_concrete) == 8)
         self.assertTrue(solver.satisfiable())
 
         result = solver.eval(str_concrete, 2)
@@ -131,10 +131,10 @@ def test_or(self):
     def test_lt_etc(self):
         str_symb = claripy.StringS("Symb_2", 4)
         solver = self.get_solver()
-        c1 = claripy.StrLen(str_symb, 32) <= 4
-        c2 = claripy.StrLen(str_symb, 32) < 4
-        c3 = claripy.StrLen(str_symb, 32) >= 4
-        c4 = claripy.StrLen(str_symb, 32) > 4
+        c1 = claripy.StrLen(str_symb) <= 4
+        c2 = claripy.StrLen(str_symb) < 4
+        c3 = claripy.StrLen(str_symb) >= 4
+        c4 = claripy.StrLen(str_symb) > 4
         solver.add(c1)
         solver.add(c2)
         solver.add(c3)
@@ -245,7 +245,7 @@ def test_suffix_simplification(self):
 
     def test_index_of(self):
         str_symb = claripy.StringS("symb_suffix", 4, explicit_name=True)
-        res = claripy.StrIndexOf(str_symb, claripy.StringV("an"), 0, 32)
+        res = claripy.StrIndexOf(str_symb, claripy.StringV("an"), 0)
         solver = self.get_solver()
 
         target_idx = 4 if KEEP_TEST_PERFORMANT else 100
@@ -261,7 +261,7 @@ def test_index_of(self):
     def test_index_of_simplification(self):
         str_concrete = claripy.StringV("concrete")
         solver = self.get_solver()
-        res = claripy.StrIndexOf(str_concrete, claripy.StringV("rete"), 0, 32)
+        res = claripy.StrIndexOf(str_concrete, claripy.StringV("rete"), 0)
         target_idx = 4 if KEEP_TEST_PERFORMANT else 100
         solver.add(res == target_idx)
         self.assertTrue(solver.satisfiable())
@@ -277,7 +277,7 @@ def test_index_of_symbolic_start_idx(self):
 
         solver.add(start_idx > 32)
         solver.add(start_idx < 35)
-        res = claripy.StrIndexOf(str_symb, claripy.StringV("an"), start_idx, 32)
+        res = claripy.StrIndexOf(str_symb, claripy.StringV("an"), start_idx)
 
         solver.add(res != -1)
         solver.add(res < 38)
@@ -290,7 +290,7 @@ def test_index_of_symbolic_start_idx(self):
 
     def test_str_to_int(self):
         str_symb = claripy.StringS("symb_strtoint", 4, explicit_name=True)
-        res = claripy.StrToInt(str_symb, 32)
+        res = claripy.StrToInt(str_symb)
         solver = self.get_solver()
         target_num = 12 if KEEP_TEST_PERFORMANT else 100000
         solver.add(res == target_num)
@@ -305,7 +305,7 @@ def test_str_to_int_simplification(self):
 
         str_concrete = claripy.StringV(str(target_num))
         solver = self.get_solver()
-        res = claripy.StrToInt(str_concrete, 32)
+        res = claripy.StrToInt(str_concrete)
 
         solver.add(res == target_num)
         self.assertTrue(solver.satisfiable())