Correctly pass BV length when abstracting UBV and SBV (#590)

claripy/backends/backend_z3.py

@@ -540,6 +540,12 @@ def _abstract_internal(self, ctx, ast, split_on=None):
             sort = FSort.from_params(ebits, sbits)
             val = self._abstract_fp_val(ctx, ast, op_name)
             return claripy.FPV(val, sort)
+        if op_name == "fpToUBV":
+            bv_size = z3.Z3_get_bv_sort_size(ctx, z3_sort)
+            return claripy.fpToUBV(*children, bv_size)
+        if op_name == "fpToSBV":
+            bv_size = z3.Z3_get_bv_sort_size(ctx, z3_sort)
+            return claripy.fpToSBV(*children, bv_size)
 
         if op_name == "UNINTERPRETED" and num_args == 0:  # symbolic value
             symbol_name = _z3_decl_name_str(ctx, decl)
@@ -577,11 +583,6 @@ def _abstract_internal(self, ctx, ast, split_on=None):
             sort = FSort.from_params(exp, mantissa)
             args = [*children, sort]
             append_children = False
-        elif op_name in ("fpToSBV", "fpToUBV"):
-            # uuuuuugggggghhhhhh
-            bv_size = z3.Z3_get_bv_sort_size(ctx, z3_sort)
-            args = [*children, bv_size]
-            append_children = False
         else:
             args = []
 

tests/test_z3.py

@@ -5,6 +5,8 @@
 import unittest
 
 import claripy
+from claripy import FPS, fpToSBV, fpToUBV
+from claripy.fp import RM
 
 
 class TestZ3(unittest.TestCase):
@@ -87,6 +89,28 @@ def test_get_long_strings(self):
         d = backend.eval(x, 1, solver=s)
         assert d == [10**16384]
 
+    def test_abstract_sbv(self):
+        """
+        Test abstracting fpToSBV
+        """
+
+        f = FPS("f", claripy.FSORT_FLOAT)
+        sbv = fpToSBV(RM.RM_NearestTiesEven, f, 32)
+
+        sbv2 = claripy.backends.z3.simplify(sbv)
+        assert sbv2.length == 32
+
+    def test_abstract_ubv(self):
+        """
+        Test abstracting fpToUBV
+        """
+
+        f = FPS("f", claripy.FSORT_FLOAT)
+        sbv = fpToUBV(RM.RM_NearestTiesEven, f, 32)
+
+        sbv2 = claripy.backends.z3.simplify(sbv)
+        assert sbv2.length == 32
+
 
 if __name__ == "__main__":
     unittest.main()