bv 0.3.0 → 0.5
raw patch · 6 files changed
Files
- CHANGES.md +76/−0
- LICENSE +1/−1
- README.md +61/−0
- bv.cabal +39/−14
- src/Data/BitVector.hs +211/−50
- test/Properties.hs +80/−6
+ CHANGES.md view
@@ -0,0 +1,76 @@++0.5.0+=====++Note that changes in `fromInteger` and `toInteger` implementations break backwards compatibility.+I hope this will not cause major problems, let me know otherwise.++* Make _bv_ with compatible with GHC 8.4.1 (_base_ 4.11). Thanks to Kosyrev Serge!+* Define `toInteger` as `int` rather than `nat`.+* Make `fromInteger` consistent and always encode in two's complement, also positive integers.+* As a result of the two previous changes, now `toInteger . fromInteger == id`, as it should be.+* Add `Read BV` instance (based on `Text.Read`, so GHC-only).+* Fix a few bugs in the non-GMP implementation. (Fortunately, GMP is the default.)+* Remove upper bounds on testing dependencies.++0.4.1+=====++Another maintenance release:++* Fix compilation error with GHC 8.0.1.+* Add `check-bounds' flag so the user decides whether to perform bounds checking.++0.4.0+=====++This is a maintenance release, but it introduces changes to the API that required a new major version.+In summary, I have fixed a few bugs, optimized a few functions, and added a few more properties (tests).+Apart from that, and the usual clean up, there are also a handful of new API functions that I judged useful.++For performance reasons, this release introduces GMP specific optimizations.+The GMP-based backend is automatically used if available, unless _-f -gmp_ is specified.++Dependencies+-----------++Only if the library is compiled with _-fgmp_ (it will, by default, if possible):++* Depend on the _ghc-prim_ package, the GHC's internal representation of primitive types.+* Depend on the _integer-gmp_ package, the Haskell bindings for GNU's GMP library.+* Use _MagicHash_ extension to work with unboxed machine integers.++Interface+---------++* Added _bitVecs_ (list of bit-vector literals).+* Added _@:_ (indexing of multiple bits).+* Added _pow_ as an optimized exponentiation function.+* Fixed _bitVec_ (value must fit bit-with).+* Fixed _negate_ (wrong on zero bit-vector).+* Define _and_ and _or_ for the case of an empty list.+* Declared Monoid instance for bit-vector (monoid under concanetation).+* Define _join_ for the case of an empty list (it must be equivalent to _mconcat_).+* Optimized when using the GMP backend: _fromBits_, _fromInteger_, and _lg2_.+* Remove uninteresting _maxNat_ function from export list.++0.3.0+=====++This is a maintenance release, but it introduces changes to the API that required a new major version.++Dependencies+-----------++* Increase base version to 4.6.+* Support base 4.7 (new methods were added to the _Bits_ type-class).+* Use of _CPP_ extension for conditional compilation.++Interface+---------++* Replace assertions by errors when checking preconditions of exported functions.+* Use proper names for functions and encourage qualified import, names ended with underscore are now deprecated.+* Add _lsb1_ function to complement _msb1_.+* Tweak code and documentation.+
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2012-2014, Iago Abal+Copyright (c) 2012-2016, Iago Abal All rights reserved.
+ README.md view
@@ -0,0 +1,61 @@+A library for bit-vector arithmetic in Haskell+=========================================++Bit-vectors are represented as a pair of a _size_ and a _value_,+where sizes are of type _Int_ and values are _Integer_.+Operations on bit-vectors are translated into operations on integers.+Remarkably, most operations taking two or more bit-vectors, will+perform zero-padding to adjust the size of the input bit-vectors+when needed (eg. when adding bit-vectors of different sizes).+Indexing operators don't do this, to avoid masking _out of bounds_+errors.++Other libraries+-------------++There exist many Haskell libraries to handle bit-vectors, but to the+best of my knowledge _bv_ is the only one that adequately supports+bit-vector arithmetic.++If you do not need bit-vector arithmetic, then you may consider using+any of these other libraries, which could offer more compact and +efficient implementations of bit arrays.++Importing and name clashes+-----------------------++Many exported functions name-clash with Prelude functions, it is+therefore recommended to do a qualified import:++ import Data.BitVector ( BV )+ import qualified Data.BitVector as BV++Running the test suite+--------------------++If you wish to run the test suite simply:++ cabal configure -ftest+ cabal build++Then run:++ dist/build/bv-tester/bv-tester++Performance+----------++**Tip:** For best performance compile with _-fgmp_.++**Tip:** If you are brave enough, compile with _-f -check-bounds_ (disables index bounds checking).++The _BV_ datatype is simply a pair of an _Int_, to represent the+_size_, and an arbitrary-precision _Integer_, to represent the+_value_ of a bit-vector.+Both fields are strict, and we instruct GHC to unbox strict fields.+Further, we ask GHC to inline virtually all bit-vector operations.+When inlined, GHC should be able to remove any overhead associated+with the _BV_ data type, and unbox bit-vector sizes.+Performance should depend mostly on the _Integer_ data type+implementation.+
bv.cabal view
@@ -1,50 +1,75 @@ Name: bv-Version: 0.3.0+Version: 0.5 Synopsis: Bit-vector arithmetic library-Description: Bit-vectors implemented as a wrapper over integers.-Homepage: http://bitbucket.org/iago/bv-haskell-Bug-reports: http://bitbucket.org/iago/bv-haskell/issues+Description: Bit-vectors implemented as a thin wrapper over integers.+Homepage: https://github.com/iagoabal/haskell-bv+Bug-reports: https://github.com/iagoabal/haskell-bv/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 +Extra-source-files: README.md CHANGES.md+ source-repository head- type: mercurial- location: https://bitbucket.org/iago/bv-haskell+ type: git+ location: https://github.com/iagoabal/haskell-bv.git +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 +Flag check-bounds+ Description: Bounds checking.+ Default: True+ Manual: True++Flag dev+ Description: Development options.+ Default: False+ Manual: True+ Library Exposed-modules: Data.BitVector -- Other-modules: Hs-Source-Dirs: src- ghc-options: -Wall+ if flag(check-bounds)+ cpp-options: -DCHECK_BOUNDS+ ghc-options: -Wall -O2+ if flag(dev)+ ghc-options: -Werror 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 >=0.5.1,+ ghc-prim Executable bv-tester if flag(test) Buildable: True Build-depends: base >=4.6 && <5,- QuickCheck >=2.4 && < 2.7,- test-framework-quickcheck2 ==0.3.*,- test-framework-th ==0.2.*+ QuickCheck >=2.4,+ test-framework-quickcheck2 >=0.3,+ test-framework-th >=0.2 else Buildable: False Main-Is: Properties.hs Hs-Source-Dirs: src, test ghc-options: -Wall+ if flag(dev)+ ghc-options: -Werror Extensions: CPP- Other-Extensions: BangPatterns, DeriveDataTypeable+ Other-Extensions: BangPatterns, DeriveDataTypeable, MagicHash
src/Data/BitVector.hs view
@@ -3,9 +3,15 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE DeriveDataTypeable #-} +-- NOTE: defined(MIN_VERSION_integer_gmp) == package configured with -fgmp++#if defined(MIN_VERSION_integer_gmp)+{-# 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>@@ -19,7 +25,7 @@ -- * Bit-vectors are interpreted as unsigned integers -- (i.e. natural numbers) except for some specific /signed/ operations. ----- * Most operations are in some way /size-polymorphic/ and, if required, +-- * Most operations are in some way /size-polymorphic/ and, if required, -- will perform padding to adjust the size of input bit-vectors. -- -- For documentation purposes we will write @[n]k@ to denote a bit-vector@@ -31,7 +37,9 @@ , size, width , nat, uint, int -- * Creation+ , nil , bitVec+ , bitVecs , ones, zeros -- * Test , isNat@@ -43,15 +51,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,33 +86,41 @@ , showBin , showOct , showHex- -- * Utilities- , maxNat- , integerWidth ) where +import Control.Monad ( Monad(..), when ) import Control.Exception ( assert ) import Data.Bits-import Data.Bool ( Bool(..), otherwise, (&&))+import Data.Bool ( Bool(..), otherwise, (&&), (||)) 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+#ifdef __GLASGOW_HASKELL__+import qualified Text.Read as R+#endif import Data.Typeable ( Typeable ) +#if defined(MIN_VERSION_integer_gmp)+import qualified GHC.Integer.Logarithms as I+import GHC.Prim ( (+#) )+import GHC.Types ( Int(..) )+#else+import Data.Int ( Int )+#endif+ import Prelude ( Char , Eq(..) , Enum(..), Num(..)- , Integral(..), Int, Integer+ , Integral(..), Integer , Maybe(..) , Real(..)+#if MIN_VERSION_base(4,11,0)+ , Semigroup(..)+#endif , Show(..), String , const , error@@ -114,6 +132,7 @@ ) {-# DEPRECATED foldl_, foldr_, reverse_, replicate_, and_, or_, group_, not_ "Use corresponding versions without underscore" #-}+{-# DEPRECATED cat "Use (#) or append instead" #-} ---------------------------------------------------------------------- --- Bit-vectors@@ -154,9 +173,40 @@ instance Show BV where show (BV n a) = "[" ++ show n ++ "]" ++ show a +#ifdef __GLASGOW_HASKELL__+instance R.Read BV where+ readPrec = do+ R.Punc "[" <- R.lexP+ n <- R.step R.readPrec+ when (n < 0) R.pfail+ R.Punc "]" <- R.lexP+ a <- R.step R.readPrec+ when (a < 0) R.pfail+ return (bitVec (n::Int) (a::Integer))+#endif+ ----------------------------------------------------------------------+--- Safety checking & Errors++checkBounds :: Bool+#if CHECK_BOUNDS+checkBounds = True+#else+checkBounds = False+#endif++check :: Bool -> Bool+check c = checkBounds && c+{-# INLINE check #-}++---------------------------------------------------------------------- --- 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 +218,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 +273,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 +343,7 @@ ---------------------------------------------------------------------- --- Indexing -infixl 9 @., @@, !.+infixl 9 @., @@, @:, !. -- | Bit indexing. --@@ -285,8 +355,8 @@ -- >>> [4]2 @. 1 -- True (@.) :: Integral ix => BV -> ix -> Bool-(BV n a) @. i | 0 <= i' && i' < n = testBit a i'- | otherwise = error "Data.BitVector.(@.): index of out bounds"+(BV n a) @. i | check(i' < 0 || n <= i') = error "Data.BitVector.(@.): index of out bounds"+ | otherwise = testBit a i' where i' = fromIntegral i {-# INLINE (@.) #-} @@ -302,8 +372,8 @@ -- >>> [4]7 @@ (3,1) -- [3]3 (@@) :: Integral ix => BV -> (ix,ix) -> BV-(BV _ a) @@ (j,i) | 0 <= i && i <= j = BV m $ (a `shiftR` i') `mod` 2^m- | otherwise = error "Data.BitVector.(@@): invalid range"+(BV _ a) @@ (j,i) | check(i < 0 || j < i) = error "Data.BitVector.(@@): invalid range"+ | otherwise = BV m $ (a `shiftR` i') `mod` 2^m where i' = fromIntegral i m = fromIntegral $ j - i + 1 {-# INLINE (@@) #-}@@ -313,6 +383,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+ | check(i' < 0 || n <= i') = error "Data.BitVector.(@:): index out of bounds"+ | otherwise = testBit a i'+ where i' = fromIntegral i+{-# INLINE (@:) #-}+ -- | Reverse bit-indexing. -- -- Index starting from the most significant bit.@@ -322,8 +406,8 @@ -- >>> [3]3 !. 0 -- False (!.) :: Integral ix => BV -> ix -> Bool-(BV n a) !. i | 0 <= i' && i' < n = testBit a (n-i'-1)- | otherwise = error "Data.BitVector.(!.): index out of bounds"+(BV n a) !. i | check(i' < 0 || n <= i') = error "Data.BitVector.(!.): index out of bounds"+ | otherwise = testBit a (n-i'-1) where i' = fromIntegral i {-# INLINE (!.) #-} @@ -331,8 +415,8 @@ -- -- @least m u == u \@\@ (m-1,0)@ least :: Integral ix => ix -> BV -> BV-least m (BV _ a) | m' < 1 = error "Data.BitVector.least: non-positive index"- | otherwise = BV m' $ a `mod` 2^m+least m (BV _ a) | check(m' < 1) = error "Data.BitVector.least: non-positive index"+ | otherwise = BV m' $ a `mod` 2^m where m' = fromIntegral m {-# INLINE least #-} @@ -340,9 +424,9 @@ -- -- @most m u == u \@\@ (n-1,n-m)@ most :: Integral ix => ix -> BV -> BV-most m (BV n a) | m' < 1 = error "Data.BitVector.most: non-positive index"- | m' > n = error "Data.BitVector.most: index out of bounds"- | otherwise = BV m' $ a `shiftR` (n-m')+most m (BV n a) | check(m' < 1) = error "Data.BitVector.most: non-positive index"+ | check(m' > n) = error "Data.BitVector.most: index out of bounds"+ | otherwise = BV m' $ a `shiftR` (n-m') where m' = fromIntegral m {-# INLINE most #-} @@ -396,13 +480,21 @@ instance Num BV where (BV n1 a) + (BV n2 b) = BV n $ (a + b) `mod` 2^n where n = max n1 n2+ {-# 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- fromInteger i = bitVec (integerWidth i) i+ {-# INLINE signum #-}+ fromInteger !i = bitVec n i+ where !n = if i >= 0 then integerWidth i + 1 else integerWidth i+ {-# INLINE fromInteger #-} -- | Bit-vector 'signum' as an 'Integral'. signumI :: Integral a => BV -> a@@ -420,9 +512,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- toInteger = nat+ {-# INLINE divMod #-}+ toInteger = int+ {-# 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 +556,15 @@ lg2 :: BV -> BV lg2 (BV _ 0) = error "Data.BitVector.lg2: zero bit-vector" lg2 (BV n 1) = BV n 0-lg2 (BV n a) = BV n $ toInteger $ integerWidth (a-1)+#if defined(MIN_VERSION_integer_gmp)+lg2 (BV n a) = BV n (toInteger a')+ where a' = I# (I.integerLog2# a)+#else+lg2 (BV n a) = BV n $ go 0 1+ where go !k !b | b == a = k+ | b > a = k-1+ | otherwise = go (k+1) (2*b)+#endif {-# INLINE lg2 #-} ----------------------------------------------------------------------@@ -459,13 +573,37 @@ 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 #-}+ mconcat = join+ {-# INLINE mconcat #-}+#if !MIN_VERSION_base(4,11,0)+ mappend = (#)+ {-# INLINE mappend #-}+#else++instance Semigroup BV where+ (<>) = (#)+ {-# INLINE (<>) #-}+#endif+ -- | Logical extension. -- -- >>> zeroExtend 3 [1]1@@ -535,9 +673,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 +685,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@@ -558,8 +700,8 @@ -- >>> split 3 [4]15 -- [[2]0,[2]3,[2]3] split :: Integral times => times -> BV -> [BV]-split k (BV n a) | k > 0 = List.map (BV s) $ splitInteger s k' a- | otherwise = error "Data.BitVector.split: non-positive splits"+split k (BV n a) | k <= 0 = error "Data.BitVector.split: non-positive splits"+ | otherwise = List.map (BV s) $ splitInteger s k' a where k' = fromIntegral k (q,r) = divMod n k' s = q + signum r@@ -570,8 +712,8 @@ -- >>> group 3 [4]15 -- [[3]1,[3]7] group, group_ :: Integral size => size -> BV -> [BV]-group s (BV n a) | s > 0 = List.map (BV s') $ splitInteger s' k a- | otherwise = error "Data.BitVector.group: non-positive size"+group s (BV n a) | s <= 0 = error "Data.BitVector.group: non-positive size"+ | otherwise = List.map (BV s') $ splitInteger s' k a where s' = fromIntegral s (q,r) = divMod n s' k = q + signum r@@ -588,12 +730,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 +746,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 +772,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 +785,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 +794,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 +882,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,21 +938,27 @@ --- 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 #-} -- | Minimum width of a bit-vector to represent a given integer number. ----- >>> integerWith 4+-- >>> integerWidth 4 -- 3 ----- >>> integerWith (-4)+-- >>> integerWidth (-4) -- 4 integerWidth :: Integer -> Int+#if defined(MIN_VERSION_integer_gmp) integerWidth !n+ | n >= 0 = I# (I.integerLog2# n +# 1#)+ | otherwise = I# (I.integerLog2# (-n) +# 2#)+#else+integerWidth !n | n >= 0 = go 1 1 | otherwise = 1 + integerWidth (abs n) where go !k !k_max | k_max >= n = k | otherwise = go (k+1) (2*k_max+1)+#endif {-# INLINE integerWidth #-}
test/Properties.hs view
@@ -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,14 +87,26 @@ -- * 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++-- * fromInteger+ prop_bv_nat :: Integer -> Property prop_bv_nat i = i >= 0 ==> nat(fromInteger i) == i -prop_bv_neg :: Integer -> Property-prop_bv_neg i = i < 0 ==> int(fromInteger i) == i+prop_bv_id :: Integer -> Bool+prop_bv_id i = toInteger (fromInteger i :: BV) == i -- * 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 +122,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 +172,24 @@ 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++-- * Logarithm++prop_lg2 :: BV -> Property+prop_lg2 a = a /= 0 ==>+ let b = lg2 a in+ 2^(nat b) <= nat a+ && nat a < 2^(nat b + 1)+ -- * Not prop_not_id :: BV -> Bool@@ -176,8 +224,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 +234,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@@ -197,3 +267,7 @@ prop_group_join_id a = forallDivisorOf (size a) $ \n -> BV.join (BV.group n a) ==. a +-- * Show & Read++prop_show_read_id :: BV -> Bool+prop_show_read_id a = read (show a) ==. a