[BUG] Float conversion to bitvector
Closed this issue · 1 comments
SjRNMzU commented
Python 3.8, Debian Sid, latest version of claripy installed via pip.
The following IPython shell recreates the bug:
In [44]: arg
Out[44]: <FP32 FPV(0xe10, FLOAT)>
In [45]: arg.to_bv()
---------------------------------------------------------------------------
ClaripyOperationError Traceback (most recent call last)
~/enigma/src/classes/analysis_engine.py in <module>
----> 1 arg.to_bv()
/usr/local/lib/python3.8/dist-packages/claripy/ast/fp.py in to_bv(self)
46
47 def to_bv(self):
---> 48 return self.raw_to_bv()
49
50 def val_to_bv(self, size, signed=True, rm=None):
/usr/local/lib/python3.8/dist-packages/claripy/ast/fp.py in raw_to_bv(self)
43 :return: A BV AST whose bit-pattern is the same as this FP
44 """
---> 45 return fpToIEEEBV(self)
46
47 def to_bv(self):
/usr/local/lib/python3.8/dist-packages/claripy/operations.py in _op(*args)
65 args, kwargs = preprocessors[name](*args, **kwargs)
66
---> 67 return return_type(name, fixed_args, **kwargs)
68
69 _op.calc_length = calc_length
/usr/local/lib/python3.8/dist-packages/claripy/ast/base.py in __new__(cls, op, args, add_variables, hash, **kwargs)
151 for eb in eager_backends:
152 try:
--> 153 r = operations._handle_annotations(eb._abstract(eb.call(op, args)), args)
154 if r is not None:
155 return r
/usr/local/lib/python3.8/dist-packages/claripy/backends/__init__.py in call(self, op, args)
236 :return: A backend object representing the result.
237 """
--> 238 converted = self.convert_list(args)
239 return self._call(op, converted)
240
/usr/local/lib/python3.8/dist-packages/claripy/backends/__init__.py in convert_list(self, args)
224
225 def convert_list(self, args):
--> 226 return [ a if isinstance(a, numbers.Number) else self.convert(a) for a in args ]
227
228 #
/usr/local/lib/python3.8/dist-packages/claripy/backends/__init__.py in <listcomp>(.0)
224
225 def convert_list(self, args):
--> 226 return [ a if isinstance(a, numbers.Number) else self.convert(a) for a in args ]
227
228 #
/usr/local/lib/python3.8/dist-packages/claripy/backends/backend_concrete.py in convert(self, expr)
81 if type(expr) is Bool and expr.op == "BoolV":
82 return expr.args[0]
---> 83 return super().convert(expr)
84
85 def _If(self, b, t, f): #pylint:disable=no-self-use,unused-argument
/usr/local/lib/python3.8/dist-packages/claripy/backends/__init__.py in convert(self, expr)
194
195 try:
--> 196 r = self._call(ast.op, args)
197 except BackendUnsupportedError:
198 r = self.default_op(ast)
/usr/local/lib/python3.8/dist-packages/claripy/backends/__init__.py in _call(self, op, args)
248 if op in self._op_raw:
249 # the raw ops don't get the model, cause, for example, Z3 stuff can't take it
--> 250 obj = self._op_raw[op](*args)
251 elif not op.startswith("__"):
252 l.debug("backend has no operation %s", op)
/usr/local/lib/python3.8/dist-packages/claripy/backends/backend_concrete.py in FPV(op, sort)
47 @staticmethod
48 def FPV(op, sort):
---> 49 return fp.FPV(op, sort)
50
51 @staticmethod
/usr/local/lib/python3.8/dist-packages/claripy/fp.py in __init__(self, value, sort)
107 def __init__(self, value, sort):
108 if not isinstance(value, float) or sort not in {FSORT_FLOAT, FSORT_DOUBLE}:
--> 109 raise ClaripyOperationError("FPV needs a sort (FSORT_FLOAT or FSORT_DOUBLE) and a float value")
110
111 self.value = value
ClaripyOperationError: FPV needs a sort (FSORT_FLOAT or FSORT_DOUBLE) and a float value
rhelmot commented
Fixed. The problem was that typechecking was performed too late. Now int arguments to FPV will be coerced to floats.