Merge pull request #29 from GaloisInc/fix-bvdomain

Fix bugs in abstract bitvector domain operations `sdiv` and `srem`.

Author: brianhuffman

what4/doc/bvdomain.cry

@@ -74,14 +74,15 @@ sbounds a = (lo - delta, hi - delta)
     delta = reverse 1
     (lo, hi) = ubounds (interval (a.lo + delta) a.sz)
 
-/** Least and greatest nonzero values in a domain, according to the
-unsigned ordering. */
+/** Nonzero signed values in a domain with the least and greatest
+reciprocals. Note that this coincides with the greatest and least
+nonzero values using the unsigned ordering. */
 rbounds : {n} (fin n, n >= 1) => BVDom n -> ([n], [n])
 rbounds a =
-  if a.lo == 0 then (1, a_hi) else
-  if a_hi == 0 then (a.lo, ~0) else
-  if a_hi < a.lo then (1, ~0) else
-  (a.lo, a_hi)
+  if a.lo == 0 then (a_hi, 1) else
+  if a_hi == 0 then (-1, a.lo) else
+  if a_hi < a.lo then (-1, 1) else
+  (a_hi, a.lo)
   where a_hi = a.lo + a.sz
 
 overlap : {n} (fin n) => BVDom n -> BVDom n -> Bit
@@ -203,14 +204,15 @@ urem a b =
     (ql, rl) = (al / bh', al % bh')
     (qh, rh) = (ah / bl', ah % bl')
 
-// The first argument is a signed interval, but the second argument is
-// an unsigned interval: The arguments should satisfy 'al <=$ ah'
-// (signed) and 'bl <= bh' (unsigned).
+// The first argument is an ordinary signed interval, but the second
+// argument is a reciprocal interval: The arguments should satisfy 'al
+// <=$ ah' (signed) and '1/bl <= 1/bh' (signed), or equivalently, 'bh
+// <= bl' (unsigned).
 sdivRange : {n} (fin n, n >= 1) => ([n], [n]) -> ([n], [n]) -> ([1+n], [1+n])
 sdivRange (al, ah) (bl, bh) = (ql, qh)
   where
-    (ql1, qh1) = shrinkRange (al, ah) bl
-    (ql2, qh2) = shrinkRange (al, ah) bh
+    (ql1, qh1) = shrinkRange (al, ah) bh
+    (ql2, qh2) = shrinkRange (al, ah) bl
     ql = smin ql1 ql2
     qh = smax qh1 qh2
 

what4/src/What4/Utils/BVDomain.hs

@@ -469,29 +469,33 @@ urem a b
     (ql, rl) = al `divMod` max 1 bh -- assume that division by 0 does not happen
     (qh, rh) = ah `divMod` max 1 bl -- assume that division by 0 does not happen
 
--- | Least and greatest nonzero values in a domain, according to the
--- unsigned ordering.
-rbounds :: BVDomain w -> (Integer, Integer)
-rbounds a =
+-- | Pairs of nonzero integers @(lo, hi)@ such that @1\/lo <= 1\/hi@.
+-- This pair represents the set of all nonzero integers @x@ such that
+-- @1\/lo <= 1\/x <= 1\/hi@.
+data ReciprocalRange = ReciprocalRange Integer Integer
+
+-- | Nonzero signed values in a domain with the least and greatest
+-- reciprocals.
+rbounds :: (1 <= w) => NatRepr w -> BVDomain w -> ReciprocalRange
+rbounds w a =
   case a of
-    BVDAny mask -> (1, mask)
+    BVDAny _ -> ReciprocalRange (-1) 1
     BVDInterval mask al aw
-      | ah > mask + 1 -> (1, mask)
-      | otherwise     -> (max 1 al, min mask aw)
-      where ah = al + aw
+      | ah > mask + 1 -> ReciprocalRange (-1) 1
+      | otherwise     -> ReciprocalRange (signed (min mask ah)) (signed (max 1 al))
+      where
+        ah = al + aw
+        signed x = if x < halfRange w then x else x - (mask + 1)
 
 -- | Interval arithmetic for integer division (rounding towards 0).
--- The argument ranges @(al, ah)@ and @(bl, bh)@ should satisfy @al <=
--- ah@ and @1\/bl >= 1\/bh@. That is, if @bl@ and @bh@ have the same
--- sign, then we require @bl <= bh@, but if they have opposite signs
--- then we require @bl > bh@. Given @a@ and @b@ with @al <= a <= ah@
--- and @1\/bl >= 1\/b >= 1/bh@, @sdivRange (al, ah) (bl, bh)@ returns
--- @(ql, qh)@ such that @ql <= a `quot` b <= qh@.
-sdivRange :: (Integer, Integer) -> (Integer, Integer) -> (Integer, Integer)
-sdivRange (al, ah) (bl, bh) = (ql, qh)
+-- Given @a@ and @b@ with @al <= a <= ah@ and @1\/bl <= 1\/b <= 1/bh@,
+-- @sdivRange (al, ah) (ReciprocalRange bl bh)@ returns @(ql, qh)@
+-- such that @ql <= a `quot` b <= qh@.
+sdivRange :: (Integer, Integer) -> ReciprocalRange -> (Integer, Integer)
+sdivRange (al, ah) (ReciprocalRange bl bh) = (ql, qh)
   where
-    (ql1, qh1) = scaleDownRange (al, ah) bl
-    (ql2, qh2) = scaleDownRange (al, ah) bh
+    (ql1, qh1) = scaleDownRange (al, ah) bh
+    (ql2, qh2) = scaleDownRange (al, ah) bl
     ql = min ql1 ql2
     qh = max qh1 qh2
 
@@ -507,7 +511,7 @@ sdiv :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
 sdiv w a b = interval mask ql (qh - ql)
   where
     mask = bvdMask a
-    (ql, qh) = sdivRange (sbounds w a) (sbounds w b)
+    (ql, qh) = sdivRange (sbounds w a) (rbounds w b)
 
 srem :: (1 <= w) => NatRepr w -> BVDomain w -> BVDomain w -> BVDomain w
 srem w a b =
@@ -524,7 +528,7 @@ srem w a b =
     mask = bvdMask a
     (al, ah) = sbounds w a
     (bl, bh) = sbounds w b
-    (ql, qh) = sdivRange (al, ah) (rbounds b)
+    (ql, qh) = sdivRange (al, ah) (rbounds w b)
     rl = if al < 0 then min (bl+1) (-bh+1) else 0
     rh = if ah > 0 then max (-bl-1) (bh-1) else 0
     aw = ah - al