Permalink
Browse files

BV: Enforcing positive values in BV Numbers.

  • Loading branch information...
marcogario committed Apr 28, 2015
1 parent 5d015d6 commit a5210b0bbbe52bc0918dfbb7b25dfb95208f541b
Showing with 23 additions and 19 deletions.
  1. +2 −6 pysmt/fnode.py
  2. +5 −0 pysmt/formula.py
  3. +5 −9 pysmt/simplifier.py
  4. +10 −3 pysmt/test/test_bv.py
  5. +1 −1 run_tests.sh
View
@@ -333,16 +333,12 @@ def constant_value(self):
return self._content.payload
def bv_unsigned_value(self):
+ # TODO: We currently support only unsigned bitvectors
value = self.constant_value()
- if value < 0:
- return value + (2 << self.bv_width())
return value
def bv_bin_str(self, reverse=False):
- if self.constant_value() >= 0:
- fstr = '{0:0%db}' % self.bv_width()
- else:
- fstr = '{0:1%db}' % self.bv_width()
+ fstr = '{0:0%db}' % self.bv_width()
bitstr = fstr.format(self.constant_value())
if reverse:
bitstr = bitstr[::-1]
View
@@ -516,6 +516,11 @@ def BV(self, value, width=None):
raise ValueError("Need to specify a width for the constant")
if is_integer(value):
+ if value < 0:
+ raise ValueError("Cannot specify a negative value: %d" % value)
+ if value >= 2**width:
+ raise ValueError("Cannot express %d in %d bits" % (value, width))
+
n = self.create_node(node_type=op.BV_CONSTANT,
args=tuple(),
payload=(value, width))
View
@@ -406,7 +406,8 @@ def walk_bv_not(self, formula, args):
def walk_bv_neg(self, formula, args):
if args[0].is_bv_constant():
- res = - args[0].constant_value()
+ res = 2**formula.bv_width() - args[0].constant_value()
+ res = res % 2**formula.bv_width()
return self.manager.BV(res, width=formula.bv_width())
return self.walk_identity(formula, args)
@@ -425,24 +426,21 @@ def walk_bv_xor(self, formula, args):
def walk_bv_add(self, formula, args):
if args[0].is_bv_constant() and args[1].is_bv_constant:
res = args[0].constant_value() + args[1].constant_value()
+ res = res % 2**formula.bv_width()
return self.manager.BV(res, width=formula.bv_width())
return self.walk_identity(formula, args)
def walk_bv_mul(self, formula, args):
if args[0].is_bv_constant() and args[1].is_bv_constant:
res = args[0].constant_value() * args[1].constant_value()
+ res = res % 2**formula.bv_width()
return self.manager.BV(res, width=formula.bv_width())
return self.walk_identity(formula, args)
def walk_bv_udiv(self, formula, args):
if args[0].is_bv_constant() and args[1].is_bv_constant:
res = args[0].bv_unsigned_value() / args[1].bv_unsigned_value()
- return self.manager.BV(res, width=formula.bv_width())
- return self.walk_identity(formula, args)
-
- def walk_bv_udiv(self, formula, args):
- if args[0].is_bv_constant() and args[1].is_bv_constant:
- res = args[0].bv_unsigned_value() / args[1].bv_unsigned_value()
+ res = res% 2**formula.bv_width()
return self.manager.BV(res, width=formula.bv_width())
return self.walk_identity(formula, args)
@@ -510,6 +508,4 @@ def walk_bv_zext(self, formula, args):
return self.manager.BV(res, width=formula.bv_width())
return self.walk_identity(formula, args)
-
-
# EOC Simplifier
View
@@ -44,19 +44,26 @@ def test_bv(self):
self.assertEqual(one, mgr.BVOne(32))
self.assertEqual(zero, mgr.BVZero(32))
+ with self.assertRaises(ValueError):
+ # Negative numbers are not supported
+ BV(-1, 10)
+ with self.assertRaises(ValueError):
+ # Number should fit in the width
+ BV(10, 2)
+
# Variables
b128 = Symbol("b", BV128) # BV1, BV8 etc. are defined in pysmt.typing
b32 = Symbol("b32", BV32)
hexample = BV(0x10, 32)
- s_one = BV(-1, 32)
+ #s_one = BV(-1, 32)
bcustom = Symbol("bc", BVType(42))
self.assertIsNotNone(hexample)
self.assertIsNotNone(bcustom)
- self.assertIsNotNone(s_one)
+ #self.assertIsNotNone(s_one)
self.assertEqual(bcustom.bv_width(), 42)
self.assertEqual(hexample.constant_value(), 16)
- self.assertEqual(str(s_one), "-1_32")
+ #self.assertEqual(str(s_one), "-1_32")
not_zero32 = mgr.BVNot(zero)
not_b128 = mgr.BVNot(b128)
View
@@ -18,7 +18,7 @@
#
export NOSE_PROCESSES=4
-export NOSE_PROCESS_TIMEOUT=180
+export NOSE_PROCESS_TIMEOUT=240
export PYTHONDONTWRITEBYTECODE=True
# Skip slow tests (-A "not slow")

0 comments on commit a5210b0

Please sign in to comment.