bv 0.3.0 → 0.4.0

raw patch · 4 files changed

+220/−41 lines, 4 filesdep +ghc-primdep +integer-gmpPVP ok

version bump matches the API change (PVP)

Dependencies added: ghc-prim, integer-gmp

API changes (from Hackage documentation)

Files

• LICENSE +1/−1
• bv.cabal +13/−7
• src/Data/BitVector.hs +142/−28
• test/Properties.hs +64/−5

@@ -1,4 +1,4 @@-Copyright (c) 2012-2014, Iago Abal+Copyright (c) 2012-2016, Iago Abal  All rights reserved. 

@@ -1,15 +1,15 @@  Name:                bv-Version:             0.3.0+Version:             0.4.0 Synopsis:            Bit-vector arithmetic library-Description:         Bit-vectors implemented as a wrapper over integers.+Description:         Bit-vectors implemented as a thin wrapper over integers. Homepage:            http://bitbucket.org/iago/bv-haskell Bug-reports:         http://bitbucket.org/iago/bv-haskell/issues License:             BSD3 License-file:        LICENSE Author:              Iago Abal <mail@iagoabal.eu> Maintainer:          Iago Abal <mail@iagoabal.eu>-Copyright:           2012-2014 Iago Abal+Copyright:           2012-2016 Iago Abal Category:            Data, Bit Vectors Build-type:          Simple Cabal-version:       >=1.6@@ -18,8 +18,12 @@   type:     mercurial   location: https://bitbucket.org/iago/bv-haskell +Flag gmp+     Description: Using Integer GMP backend.+     Default: True+ Flag test-     Description: Build the test suite, including an executable to run it.+     Description: Build the test suite, and an executable to run it.      Default: False      Manual: True @@ -27,10 +31,12 @@   Exposed-modules:     Data.BitVector   -- Other-modules:   Hs-Source-Dirs:      src-  ghc-options:         -Wall+  ghc-options:         -Wall -O2   Extensions:          CPP-  Other-Extensions:    BangPatterns, DeriveDataTypeable+  Other-Extensions:    BangPatterns, DeriveDataTypeable, MagicHash   Build-depends:       base >=4.6 && <5+  if impl(ghc) && flag(gmp)+    Build-depends: integer-gmp, ghc-prim  Executable bv-tester   if flag(test)@@ -46,5 +52,5 @@   Hs-Source-Dirs:      src, test   ghc-options:         -Wall   Extensions:          CPP-  Other-Extensions:    BangPatterns, DeriveDataTypeable+  Other-Extensions:    BangPatterns, DeriveDataTypeable, MagicHash 

@@ -3,9 +3,13 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE DeriveDataTypeable #-} +#if MIN_VERSION_integer_gmp(0,5,1)+{-# LANGUAGE MagicHash #-}+#endif+ -- | -- Module    : Data.BitVector--- Copyright : (c) 2012-2014 Iago Abal+-- Copyright : (c) 2012-2016 Iago Abal --             (c) 2012-2013 HASLab & University of Minho -- License   : BSD3 -- Maintainer: Iago Abal <mail@iagoabal.eu>@@ -31,7 +35,9 @@   , size, width   , nat, uint, int     -- * Creation+  , nil   , bitVec+  , bitVecs   , ones, zeros     -- * Test   , isNat@@ -43,15 +49,17 @@     -- * Indexing   , (@.), index   , (@@), extract+  , (@:)   , (!.)   , least, most   , msb, lsb, msb1, lsb1   -- * Arithmetic   , signumI+  , pow   , sdiv, srem, smod   , lg2   -- * List-like operations-  , (#), cat+  , (#), cat, append, concat   , zeroExtend, signExtend   , foldl, foldl_   , foldr, foldr_@@ -76,9 +84,6 @@   , showBin   , showOct   , showHex-  -- * Utilities-  , maxNat-  , integerWidth   ) where  import           Control.Exception ( assert )@@ -88,19 +93,21 @@ import qualified Data.Bool as Bool import           Data.Data ( Data ) import qualified Data.List as List-  ( foldr, foldl1'-  , length-  , map-  , maximum-  )+import           Data.Monoid ( Monoid(..) ) import           Data.Ord import           Data.Typeable ( Typeable ) +#if MIN_VERSION_integer_gmp(0,5,1)+import qualified GHC.Integer.Logarithms as I+import           GHC.Prim ( (+#) )+import           GHC.Types ( Int(..) )+#endif+ import           Prelude   ( Char   , Eq(..)   , Enum(..), Num(..)-  , Integral(..), Int, Integer+  , Integral(..), Integer   , Maybe(..)   , Real(..)   , Show(..), String@@ -114,6 +121,7 @@   )  {-# DEPRECATED foldl_, foldr_, reverse_, replicate_, and_, or_, group_, not_ "Use corresponding versions without underscore" #-}+{-# DEPRECATED cat "Use (#) or append instead" #-}  ---------------------------------------------------------------------- --- Bit-vectors@@ -157,6 +165,11 @@ ---------------------------------------------------------------------- --- Construction +-- | The /empty/ bit-vector, ie. @[0]0@.+nil :: BV+nil = BV 0 0+{-# INLINE nil #-}+ -- | Create a bit-vector given a size and an integer value. -- -- >>> bitVec 4 3@@ -168,10 +181,28 @@ -- [4]15 bitVec :: Integral a => Int -> a -> BV bitVec n a | n < 0     = error "Data.BitVector.bitVec: negative size"-           | a >= 0    = BV n $ fromIntegral a-           | otherwise = negate $ BV n $ fromIntegral (-a)+           | a >= 0    = BV n (a' `mod` 2^n)+           | otherwise = negate $ BV n ((-a') `mod` 2^n)+  where a' = fromIntegral a {-# INLINE bitVec #-} +-- | List of bit-vector literals of the same size+--+-- When a list of integer literals is interpreted as a list of bit-vectors,+-- 'fromInteger' is applied to each element invidually:+--+-- >>> [1,3,5] :: [BV]+-- [ [1]1, [2]3, [3]5 ]+--+-- Sometimes we want to specify a list of bit-vectors literals of the same+-- size, and for that we can use 'bitVects':+--+-- >>> bitVecs 3 [1,3,5]+-- [ [3]1, [3]3, [3]5 ]+bitVecs :: Integral a => Int -> [a] -> [BV]+bitVecs = List.map . bitVec+{-# INLINE bitVecs #-}+ -- | Create a mask of ones. ones :: Int -> BV ones n | n < 0     = error "Data.BitVector.ones: negative size"@@ -205,9 +236,11 @@  instance Eq BV where   (BV _ a) == (BV _ b) = a == b+  {-# INLINE (==) #-}  instance Ord BV where   compare = comparing nat+  {-# INLINE compare #-}  -- | Fixed-size equality. --@@ -273,7 +306,7 @@ ---------------------------------------------------------------------- --- Indexing -infixl 9 @., @@, !.+infixl 9 @., @@, @:, !.  -- | Bit indexing. --@@ -313,6 +346,20 @@ extract j i = (@@ (j,i)) {-# INLINE extract #-} +-- | Bit list indexing.+--+-- prop> u @: is ==. fromBits $ List.map (u @.) is+(@:) :: Integral ix => BV -> [ix] -> BV+(BV n a) @: is = fromBits $ List.map testBitAux is+  -- NB: Failing _late_ (the bounds check is done by 'testBitAux') avoids+  -- duplicating calls to 'fromIntegral' **and** this code should allow GHC+  -- to fuse 'fodlr' (from inlining 'frombits') with 'map'.+  where testBitAux i+          | i' >= 0 && i' < n = testBit a i'+          | otherwise = error "Data.BitVector.(@:): index out of bounds"+          where i' = fromIntegral i+{-# INLINE (@:) #-}+ -- | Reverse bit-indexing. -- -- Index starting from the most significant bit.@@ -396,13 +443,26 @@ instance Num BV where   (BV n1 a) + (BV n2 b) = BV n $ (a + b) `mod` 2^n     where n = max n1 n2+  {-# INLINE (+) #-}+  {-# INLINE (-) #-}   (BV n1 a) * (BV n2 b) = BV n $ (a * b) `mod` 2^n     where n = max n1 n2-  negate (BV n a) = BV n $ 2^n - a+  {-# INLINE (*) #-}+  negate u@(BV _ 0) = u+  negate   (BV n a) = BV n $ 2^n - a+  {-# INLINE negate #-}   abs u | msb u     = negate u         | otherwise = u+  {-# INLINE abs #-}   signum u = bitVec 2 $ signum $ int u+  {-# INLINE signum #-}+#if MIN_VERSION_integer_gmp(0,5,1)+  fromInteger i = bitVec n i+    where n = I# (I.integerLog2# i +# 1#)+#else   fromInteger i = bitVec (integerWidth i) i+#endif+  {-# INLINE fromInteger #-}  -- | Bit-vector 'signum' as an 'Integral'. signumI :: Integral a => BV -> a@@ -420,9 +480,23 @@   quotRem (BV n1 a) (BV n2 b) = (BV n q,BV n r)     where n = max n1 n2           (q,r) = quotRem a b+  {-# INLINE quotRem #-}   divMod = quotRem+  {-# INLINE divMod #-}   toInteger = nat+  {-# INLINE toInteger #-} +-- | Bit-vector exponentiation.+--+-- @pow [n]k e@ computes @k@ raised to @e@ modulo @n@.+--+-- This is faster than Haskell's (^) operator because it performs+-- modulo division just once. Besides, @a^0 == [1]0@ !!!+pow :: Integral exp => BV -> exp -> BV+pow (BV n a) e = BV n (a^e `mod` m)+  where m = 2^n+{-# INLINE pow #-}+ -- | 2's complement signed division. sdiv :: BV -> BV -> BV sdiv u@(BV n1 _) v@(BV n2 _) = bitVec n q@@ -450,7 +524,12 @@ lg2 :: BV -> BV lg2 (BV _ 0) = error "Data.BitVector.lg2: zero bit-vector" lg2 (BV n 1) = BV n 0+#if MIN_VERSION_integer_gmp(0,5,1)+lg2 (BV n a) = BV n (toInteger a')+  where a' = I# (I.integerLog2# a)+#else lg2 (BV n a) = BV n $ toInteger $ integerWidth (a-1)+#endif {-# INLINE lg2 #-}  ----------------------------------------------------------------------@@ -459,13 +538,29 @@ infixr 5 #  -- | Concatenation of two bit-vectors.-(#), cat :: BV -> BV -> BV+(#), cat, append :: BV -> BV -> BV (BV n a) # (BV m b) = BV (n + m) ((a `shiftL` m) + b) {-# INLINE (#) #-}  cat = (#) {-# INLINE cat #-} +append = (#)+{-# INLINE append #-}++-- | An alias for 'join'.+concat :: [BV] -> BV+concat = join++-- This is the most sensible monoid instance until we have size types!+instance Monoid BV where+  mempty  = nil+  {-# INLINE mempty #-}+  mappend = (#)+  {-# INLINE mappend #-}+  mconcat = join+  {-# INLINE mconcat #-}+ -- | Logical extension. -- -- >>> zeroExtend 3 [1]1@@ -535,9 +630,11 @@  -- | Conjunction. ----- @and == foldr1 (.&.)@+-- Essentially, @and == foldr1 (.&.)@.+--+-- Returns @[1]1@ if the input list is empty. and, and_ :: [BV] -> BV-and [] = error "Data.BitVector.and: empty list"+and [] = ones 1 and ws = BV n' $ List.foldl1' (.&.) $ List.map nat ws   where n' = List.maximum $ List.map size ws and_ = and@@ -545,9 +642,11 @@  -- | Disjunction. ----- @or == foldr1 (.|.)@+-- Essentially, @or == foldr1 (.|.)@.+--+-- Returns @[1]0@ if the input list is empty. or, or_ :: [BV] -> BV-or [] = error "Data.BitVector.or: empty list"+or [] = zeros 1 or ws = BV n' $ List.foldl1' (.|.) $ List.map nat ws   where n' = List.maximum $ List.map size ws or_ = or@@ -588,12 +687,12 @@                 a' = a `shiftR` n' {-# INLINE splitInteger #-} --- | Concatenate a list of bit-vectors.+-- | Concatenate a (possibly empty) list of bit-vectors. -- -- >>> join [[2]3,[2]2] -- [4]14 join :: [BV] -> BV-join = List.foldl1' (#)+join = List.foldl' (#) nil {-# INLINE join #-}  ----------------------------------------------------------------------@@ -604,17 +703,24 @@ instance Bits BV where   (BV n1 a) .&. (BV n2 b) = BV n $ a .&. b     where n = max n1 n2+  {-# INLINE (.&.) #-}   (BV n1 a) .|. (BV n2 b) = BV n $ a .|. b     where n = max n1 n2+  {-# INLINE (.|.) #-}   (BV n1 a) `xor` (BV n2 b) = BV n $ a `xor` b     where n = max n1 n2+  {-# INLINE xor #-}   complement (BV n a) = BV n $ 2^n - 1 - a+  {-# INLINE complement #-} #if MIN_VERSION_base(4,7,0)   zeroBits = BV 1 0+  {-# INLINE zeroBits #-} #endif   bit i = BV (i+1) (2^i)+  {-# INLINE bit #-}   testBit (BV n a) i | i < n     = testBit a i                      | otherwise = False+  {-# INLINE testBit #-}   bitSize = undefined #if MIN_VERSION_base(4,7,0)   bitSizeMaybe = const Nothing@@ -623,9 +729,11 @@   shiftL (BV n a) k     | k > n     = BV n 0     | otherwise = BV n $ shiftL a k `mod` 2^n+  {-# INLINE shiftL #-}   shiftR (BV n a) k     | k > n     = BV n 0     | otherwise = BV n $ shiftR a k+  {-# INLINE shiftR #-}   rotateL bv       0 = bv   rotateL (BV n a) k     | k == n    = BV n a@@ -634,6 +742,7 @@     where s = n - k           l = a `shiftR` s           h = (a `shiftL` k) `mod` 2^n+  {-# INLINE rotateL #-}   rotateR bv       0 = bv   rotateR (BV n a) k     | k == n    = BV n a@@ -642,7 +751,9 @@     where s = n - k           l = a `shiftR` k           h = (a `shiftL` s) `mod` 2^n+  {-# INLINE rotateR #-}   popCount (BV _ a) = assert (a >= 0) $ popCount a+  {-# INLINE popCount #-}  -- | An alias for 'complement'. not, not_ :: BV -> BV@@ -728,11 +839,12 @@ -- >>> fromBits [False, False, True] -- [3]1 fromBits :: [Bool] -> BV-fromBits bs = BV n $ snd $ List.foldr go (1,0) bs-  where n = List.length bs-        go b (!v,!acc) | b         = (v',acc+v)-                       | otherwise = (v',acc)-          where v' = 2*v+fromBits bs =+  let (n,k) = List.foldr go (0,0) bs in+  BV n k+  -- NB: 'setBit' is a GMP function, faster than regular addition.+  where go b (!i,!v) | b         = (i+1,setBit v i)+                     | otherwise = (i+1,v) {-# INLINE fromBits #-}  -- | Create a big-endian list of bits from a bit-vector.@@ -783,10 +895,11 @@ --- Utilities  -- | Greatest natural number representable with /n/ bits.-maxNat :: (Integral a, Integral b) => a -> b+maxNat :: Integral size => size -> Integer maxNat n = 2^n - 1 {-# INLINE maxNat #-} +#ifndef MIN_VERSION_integer_gmp -- | Minimum width of a bit-vector to represent a given integer number. -- -- >>> integerWith 4@@ -801,3 +914,4 @@   where go !k !k_max | k_max >= n = k                      | otherwise  = go (k+1) (2*k_max+1) {-# INLINE integerWidth #-}+#endif

@@ -6,7 +6,7 @@ {-# LANGUAGE TupleSections     #-}  -- |--- Copyright : (c) 2012-2014 Iago Abal+-- Copyright : (c) 2012-2016 Iago Abal --             (c) 2012-2013 HASLab & University of Minho -- License   : BSD3 -- Maintainer: Iago Abal <mail@iagoabal.eu>@@ -15,6 +15,7 @@ module Main where  import Data.BitVector as BV+import Data.List as List  import Control.Applicative ( (<$>), (<*>) ) @@ -32,6 +33,9 @@ c_MAX_SIZE :: Int c_MAX_SIZE = 8192 +c_SMALL_NAT :: Int+c_SMALL_NAT = 128+ data BV2 = BV2 !BV !BV     deriving (Eq,Show) @@ -41,8 +45,15 @@ divides :: Integral a => a -> a -> Bool divides k n = n `mod` k == 0 +aNat :: Gen Int+aNat = abs <$> arbitrary++aSmallNat, anExp :: Gen Int+aSmallNat = min c_SMALL_NAT <$> aNat+anExp = aSmallNat+ gSize :: Gen Int-gSize = min c_MAX_SIZE . (+1) . abs <$> arbitrary+gSize = min c_MAX_SIZE . (+1) <$> aNat  gBV :: Int -> Gen BV gBV sz = bitVec sz <$> choose (0::Integer,2^sz-1)@@ -76,6 +87,12 @@  -- * bitVec +prop_bv_any :: Integer -> Property+prop_bv_any i = forAll gSize $ \n ->+  let u = bitVec n i in+  let a = nat u in+  a >= 0 && a < 2^n+ prop_bv_nat :: Integer -> Property prop_bv_nat i = i >= 0 ==> nat(fromInteger i) == i @@ -84,6 +101,10 @@  -- * Indexing +prop_mult_index :: BV -> Property+prop_mult_index a = forAll (listOf (gIndex a)) $ \is ->+  a @: is ==. fromBits (List.map (a @.) is)+ prop_rev_index :: BV -> Property prop_rev_index a = forallIndexOf a $ \i -> a !. i == a @. (size(a)-i-1) @@ -99,6 +120,13 @@ prop_neg_id :: BV -> Bool prop_neg_id a = -(-a) ==. a +prop_neg_int :: Integer -> Property+prop_neg_int i = forAll gSize $ \n ->+  let u = bitVec n i in+  if nat u == 2^(n-1) -- only the msb is set, ie 1000...0+  then int u == -2^(n-1) && int (-u) == int u -- overflow!+  else int (-u) == -(int u)+ prop_abs_id :: BV -> Bool prop_abs_id a = abs(abs(a)) ==. abs(a) @@ -142,6 +170,16 @@ prop_smod_is_rem a b =   isNat a && isPos b ==> a `smod` b ==. a `rem` b +-- * Exponentiation++prop_exp_zero :: BV -> Bool+prop_exp_zero a =+  pow a (0::Int) ==. bitVec (size a) (1::Int)++prop_exp_spec :: BV -> Property+prop_exp_spec a = forAll anExp $ \e ->+  e /= 0 ==> pow a e ==. a^e+ -- * Not  prop_not_id :: BV -> Bool@@ -176,8 +214,7 @@  prop_shr_div :: BV -> Property prop_shr_div a = forallIndex1Of a $ \i ->-                   a `shiftR` i == a `div` bitVec n ((2::Integer)^i)-  where n = size a+                   a `shiftR` i == a `div` fromInteger((2::Integer)^i)  -- * Rotate @@ -187,6 +224,29 @@ prop_ror_id :: BV -> Bool prop_ror_id a = a `rotateR` (size a) ==. a +-- * Concat++prop_concat_id :: BV -> Bool+prop_concat_id a = nil # a ==. a && a # nil ==. a++prop_concat_assoc :: BV -> BV -> BV -> Bool+prop_concat_assoc a b c = (a # b) # c ==. a # (b # c)++prop_concat_join :: [BV] -> Bool+prop_concat_join us = join us ==. List.foldr (#) nil us++-- * Bit extension++prop_zero_extend :: BV -> Property+prop_zero_extend a = forAll aNat $ \d ->+  let a' = zeroExtend d a in+  a' == a && size a' - size a == d++prop_sign_extend :: BV -> Property+prop_sign_extend a = forAll aSmallNat $ \d ->+  let a' = signExtend d a in+  int a' == int a && size a' - size a == d+ -- * Split & group  prop_split_join_id :: BV -> Property@@ -196,4 +256,3 @@ prop_group_join_id :: BV -> Property prop_group_join_id a = forallDivisorOf (size a) $ \n ->   BV.join (BV.group n a) ==. a-