Skip to content

Fp smt #36

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
cdonovick wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Fp smt #36

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
42b6f20
Add z3 fp vector
cdonovick May 20, 2019
025a22c
lots of tests
cdonovick Jun 7, 2019
7ddd3a2
Bug fixes, more testing
cdonovick Jun 12, 2019
8ee18bb
Bug fixes
cdonovick Jun 12, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions hwtypes/__init__.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,3 +6,4 @@
from .fp_vector_abc import *
from .fp_vector import *
from .modifiers import *
from .z3_fp_vector import *
111 changes: 58 additions & 53 deletions hwtypes/fp_vector.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
}

def _coerce(T : tp.Type['FPVector'], val : tp.Any) -> 'FPVector':
if not isinstance(val, FPVector):
if not isinstance(val, T):
return T(val)
elif type(val).binding != T.binding:
raise TypeError('Inconsistent FP type')
Expand All @@ -42,58 +42,60 @@ def wrapped(self : 'FPVector', *args, **kwargs):
class FPVector(AbstractFPVector):
@set_context
def __init__(self, value):
# Because for some reason gmpy2.mpfr is a function and not a type
if isinstance(value, type(gmpy2.mpfr(0))):
#need to specify precision because mpfr will use the input
#precision not the context precision when constructing from mpfr
value = gmpy2.mpfr(value, self._ctx_.precision)
elif isinstance(value, FPVector):
value = gmpy2.mpfr(value._value, self._ctx_.precision)
elif isinstance(value, (int, float, type(gmpy2.mpz(0)), type(gmpy2.mpq(0)))):
value = gmpy2.mpfr(value)
elif isinstance(value, str):
try:
#Handles '0.5'
value = gmpy2.mpfr(value)
except ValueError:

with gmpy2.local_context(self._ctx_):
# Because for some reason gmpy2.mpfr is a function and not a type
if isinstance(value, type(gmpy2.mpfr(0))):
#need to specify precision because mpfr will use the input
#precision not the context precision when constructing from mpfr
value = gmpy2.mpfr(value, precision=self._ctx_.precision)
elif isinstance(value, FPVector):
value = gmpy2.mpfr(value._value, precision=self._ctx_.precision)
elif isinstance(value, (int, float, type(gmpy2.mpz(0)), type(gmpy2.mpq(0)))):
value = gmpy2.mpfr(value, precision=self._ctx_.precision)
elif isinstance(value, str):
try:
#Handles '1/2'
value = gmpy2.mpfr(gmpy2.mpq(value))
#Handles '0.5'
value = gmpy2.mpfr(value, precision=self._ctx_.precision)
except ValueError:
raise ValueError('Invalid string')
elif hasattr(value, '__float__'):
value = gmpy2.mpfr(float(value))
elif hasattr(value, '__int__'):
value = gmpy2.mpfr(int(value))
else:
try:
#if gmpy2 doesn't complain I wont
value = gmpy2.mpfr(value)
except TypeError:
raise TypeError(f"Can't construct FPVector from {type(value)}")

if gmpy2.is_nan(value) and not type(self).ieee_compliance:
if gmpy2.is_signed(value):
self._value = gmpy2.mpfr('-inf')
try:
#Handles '1/2'
value = gmpy2.mpfr(gmpy2.mpq(value), precision=self._ctx_.precision)
except ValueError:
raise ValueError('Invalid string')
elif hasattr(value, '__float__'):
value = gmpy2.mpfr(float(value), precision=self._ctx_.precision)
elif hasattr(value, '__int__'):
value = gmpy2.mpfr(int(value), precision=self._ctx_.precision)
else:
self._value = gmpy2.mpfr('inf')
try:
#if gmpy2 doesn't complain I wont
value = gmpy2.mpfr(value, precision=self._ctx_.precision)
except TypeError:
raise TypeError(f"Can't construct FPVector from {type(value)}")


else:
self._value = value

if not type(self).ieee_compliance:
if self.fp_is_subnormal():
if self.fp_is_positive():
self._value = gmpy2.mpfr('+0', precision=self._ctx_.precision)
else:
self._value = gmpy2.mpfr('-0', precision=self._ctx_.precision)
elif self.fp_is_NaN():
self._value = gmpy2.mpfr('inf', precision=self._ctx_.precision)




@classmethod
def __init_subclass__(cls, **kwargs):
if cls.is_bound:
if cls.ieee_compliance:
precision=cls.mantissa_size+1
emax=1<<(cls.exponent_size - 1)
emin=4-emax-precision
subnormalize=True
else:
precision=cls.mantissa_size+1
emax=1<<(cls.exponent_size - 1)
emin=3-emax
subnormalize=False
precision=cls.mantissa_size+1
emax=1<<(cls.exponent_size - 1)
emin=4-emax-precision
subnormalize=True

ctx = gmpy2.context(
precision=precision,
Expand Down Expand Up @@ -135,7 +137,7 @@ def __init_subclass__(cls, **kwargs):


def __repr__(self):
return f'{self._value}'
return f"{type(self)}({self._value.__format__('b')})"

@set_context
def fp_abs(self) -> 'FPVector':
Expand Down Expand Up @@ -229,7 +231,6 @@ def fp_is_normal(self) -> Bit:
def fp_is_subnormal(self) -> Bit:
bv = self.reinterpret_as_bv()
if (bv[type(self).mantissa_size:-1] == 0) & ~self.fp_is_zero():
assert type(self).ieee_compliance
return Bit(True)
else:
return Bit(False)
Expand Down Expand Up @@ -381,15 +382,19 @@ def __float__(self):

@classmethod
@set_context
def random(cls, allow_inf=True) -> 'FPVector':
def random(cls, allow_inf=True, allow_nan=True) -> 'FPVector':
bias = (1 << (cls.exponent_size - 1)) - 1
sign = random.choice([-1, 1])
mantissa = gmpy2.mpfr_random(gmpy2.random_state()) + 1
if allow_inf:
sign = random.choice([-1, 1])
mantissa = gmpy2.mpfr_random(gmpy2.random_state()) + 1
exp = random.randint(1-bias, bias+1)
return cls(mantissa*sign*(gmpy2.mpfr(2)**gmpy2.mpfr(exp)))
else:
sign = random.choice([-1, 1])
mantissa = gmpy2.mpfr_random(gmpy2.random_state()) + 1
exp = random.randint(1-bias, bias)
return cls(mantissa*sign*(gmpy2.mpfr(2)**gmpy2.mpfr(exp)))
v = cls(mantissa*sign*(gmpy2.mpfr(2)**gmpy2.mpfr(exp)))
while ((not allow_inf) and v.fp_is_infinite()) or ((not allow_nan) and v.fp_is_NaN()):
if allow_inf:
exp = random.randint(1-bias, bias+1)
else:
exp = random.randint(1-bias, bias)
v = cls(mantissa*sign*(gmpy2.mpfr(2)**gmpy2.mpfr(exp)))
return v
2 changes: 1 addition & 1 deletion hwtypes/fp_vector_abc.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -206,4 +206,4 @@ def reinterpret_as_bv(self) -> AbstractBitVector: pass

@classmethod
@abstractmethod
def reinterpret_from_bv(self, value: AbstractBitVector) -> 'AbstractFPVector': pass
def reinterpret_from_bv(cls, value: AbstractBitVector) -> 'AbstractFPVector': pass
28 changes: 8 additions & 20 deletions hwtypes/z3_bit_vector.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,9 @@ def __init__(self, value=SMYBOLIC, *, name=AUTOMATIC):
name = _gen_name()
_name_table[name] = self

if isinstance(value, z3.ExprRef):
value = z3.simplify(value)

if value is SMYBOLIC:
self._value = z3.Bool(name)
elif isinstance(value, z3.BoolRef):
Expand Down Expand Up @@ -149,7 +152,6 @@ def ite(self, t_branch, f_branch):

T = type(t_branch)


return T(z3.If(self.value, t_branch.value, f_branch.value))

def _coerce(T : tp.Type['z3BitVector'], val : tp.Any) -> 'z3BitVector':
Expand Down Expand Up @@ -195,6 +197,9 @@ def __init__(self, value=SMYBOLIC, *, name=AUTOMATIC):
_name_table[name] = self
self._name = name

if isinstance(value, z3.ExprRef):
value = z3.simplify(value)

T = z3.BitVecSort(self.size)

if value is SMYBOLIC:
Expand Down Expand Up @@ -489,8 +494,6 @@ def bvsrem(self, other):
__le__ = bvule
__lt__ = bvult



@int_cast
def repeat(self, n):
return type(self)(z3.RepeatBitVec(n, self.value))
Expand All @@ -510,23 +513,8 @@ def zext(self, ext):
raise ValueError()
return type(self).unsized_t[self.size + ext](z3.ZeroExt(ext, self.value))

# Used in testing
# def bits(self):
# return [(self >> i) & 1 for i in range(self.size)]
#
# def __int__(self):
# return self.as_uint()
#
# def as_uint(self):
# return self._value.as_long()
#
# def as_sint(self):
# return self._value.as_signed_long()
#
# @classmethod
# def random(cls, width):
# return cls.unsized_t[width](random.randint(0, (1 << width) - 1))
#
def __repr__(self):
return f'{type(self)}({self._value})'

class z3NumVector(z3BitVector):
pass
Expand Down
Loading