bv 0.2.1 → 0.2.2
raw patch · 3 files changed
+248/−6 lines, 3 filesdep +QuickCheckdep +test-framework-quickcheck2dep +test-framework-thnew-component:exe:bv-tester
Dependencies added: QuickCheck, test-framework-quickcheck2, test-framework-th
Files
- Data/BitVector.hs +31/−4
- Properties.hs +198/−0
- bv.cabal +19/−2
Data/BitVector.hs view
@@ -4,8 +4,7 @@ -- | -- Module : Data.BitVector--- Copyright : (c) Iago Abal, 2012-2013--- (c) University of Minho, 2012+-- Copyright : (c) 2012-2013 Iago Abal, HASLab & University of Minho -- License : BSD3 -- Maintainer: Iago Abal <iago.abal@gmail.com> --@@ -28,6 +27,9 @@ -- * Creation , bitVec , ones, zeros+ -- * Test+ , isNat+ , isPos -- * Comparison , (==.), (/=.) , (<.), (<=.), (>.), (>=.)@@ -39,6 +41,7 @@ , least, most , msb, lsb, msb1 -- * Arithmetic+ , signumI , sdiv, srem, smod , lg2 -- * List-like operations@@ -139,7 +142,7 @@ bitVec :: Integral a => Int -> a -> BV bitVec n a | a >= 0 = BV n $ fromIntegral a | otherwise = negate $ BV n $ fromIntegral (-a)-{-# RULES "bitVec/Integer" bitVec = BV #-}+{-# SPECIALIZE bitVec :: Int -> Integer -> BV #-} {-# SPECIALIZE bitVec :: Int -> Int -> BV #-} {-# INLINE[1] bitVec #-} @@ -154,8 +157,22 @@ {-# INLINE zeros #-} ----------------------------------------------------------------------+--- Test++-- | Test if the signed value of a bit-vector is a natural number.+isNat :: BV -> Bool+isNat a = int(a) >= 0++-- | Test if the signed value of a bit-vector is a positive number.+isPos :: BV -> Bool+isPos a = int(a) > 0++---------------------------------------------------------------------- --- Comparison +infix 4 ==., /=., <., <=., >., >=.+infix 4 `slt`, `sle`, `sgt`, `sge`+ instance Eq BV where (BV _ a) == (BV _ b) = a == b @@ -225,6 +242,8 @@ ---------------------------------------------------------------------- --- Indexing +infixl 9 @., @@, !.+ -- | Bit indexing. -- -- @u \@. i@ stands for the /i/-th bit of /u/.@@ -339,9 +358,13 @@ negate (BV n a) = BV n $ 2^n - a abs u | msb u = negate u | otherwise = u- signum u = bitVec 2 $ int u+ signum u = bitVec 2 $ signum $ int u fromInteger i = bitVec (integerWidth i) i +-- | Bit-vector 'signum' as an 'Integral'.+signumI :: Integral a => BV -> a+signumI = fromInteger . signum . int+ instance Real BV where toRational = toRational . nat @@ -386,6 +409,8 @@ ---------------------------------------------------------------------- --- List-like operations +infixr 5 #+ -- | Concatenation of two bit-vectors. (#), cat :: BV -> BV -> BV (BV n a) # (BV m b) = BV (n + m) ((a `shiftL` m) + b)@@ -522,6 +547,8 @@ ---------------------------------------------------------------------- --- Bitwise operations++infixl 8 <<., `shl`, >>., `shr`, `ashr`, <<<., `rol`, >>>., `ror` instance Bits BV where (BV n1 a) .&. (BV n2 b) = BV n $ a .&. b
+ Properties.hs view
@@ -0,0 +1,198 @@+{-# OPTIONS_GHC -fno-warn-orphans #-}+++{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TupleSections #-}++-- |+-- Copyright : (c) 2012-2013 Iago Abal, HASLab & University of Minho+-- License : BSD3+-- Maintainer: Iago Abal <iago.abal@gmail.com>+--+-- QuickCheck properties for 'Data.BitVector'.+module Main where++import Data.BitVector++import Control.Applicative ( (<$>), (<*>) )++import Test.Framework.TH+import Test.Framework.Providers.QuickCheck2+import Test.QuickCheck.Arbitrary+import Test.QuickCheck.Property ( Property, Testable, forAll, (==>) )+import Test.QuickCheck.Gen++main :: IO ()+main = $(defaultMainGenerator)++-- * Generators++c_MAX_SIZE :: Int+c_MAX_SIZE = 8192++data BV2 = BV2 !BV !BV+ deriving (Eq,Show)++data BV3 = BV3 !BV !BV !BV+ deriving (Eq,Show)++divides :: Integral a => a -> a -> Bool+divides k n = n `mod` k == 0++gSize :: Gen Int+gSize = min c_MAX_SIZE . (+1) . abs <$> arbitrary++gBV :: Int -> Gen BV+gBV sz = bitVec sz <$> choose (0::Integer,2^sz-1)++gDivisor :: Int -> Gen Int+gDivisor n = suchThat (choose (1,n)) (`divides` n)++forallDivisorOf :: Testable prop => Int -> (Int -> prop) -> Property+forallDivisorOf n = forAll (gDivisor n)++gIndex :: BV -> Gen Int+gIndex a = choose (0,size(a)-1)++forallIndexOf :: Testable prop => BV -> (Int -> prop) -> Property+forallIndexOf a = forAll (gIndex a)++gIndex1 :: BV -> Gen Int+gIndex1 a = choose (1,size a)++forallIndex1Of :: Testable prop => BV -> (Int -> prop) -> Property+forallIndex1Of a = forAll (gIndex1 a)++instance Arbitrary BV where+ arbitrary = gBV =<< gSize++instance Arbitrary BV2 where+ arbitrary = gSize >>= \sz -> BV2 <$> gBV sz <*> gBV sz++instance Arbitrary BV3 where+ arbitrary = gSize >>= \sz -> BV3 <$> gBV sz <*> gBV sz <*> gBV sz++-- * bitVec++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++-- * Indexing++prop_rev_index :: BV -> Property+prop_rev_index a = forallIndexOf a $ \i -> a !. i == a @. (size(a)-i-1)++prop_least :: BV -> Property+prop_least a = forallIndex1Of a $ \m -> least m a ==. a@@(m-1,0)++prop_most :: BV -> Property+prop_most a = forallIndex1Of a $ \m -> most m a ==. a@@(n-1,n-m)+ where n = size a++-- * Negate++prop_neg_id :: BV -> Bool+prop_neg_id a = -(-a) ==. a++prop_abs_id :: BV -> Bool+prop_abs_id a = abs(abs(a)) ==. abs(a)++-- * Addition++prop_plus_right_id :: BV -> Bool+prop_plus_right_id a = a + zeros(size a) ==. a++prop_plus_comm :: BV -> BV -> Bool+prop_plus_comm a b = a + b ==. b + a++prop_plus_assoc :: BV3 -> Bool+prop_plus_assoc (BV3 a b c) = (a + b) + c ==. a + (b + c)++-- * Multiplication++prop_mult_comm :: BV -> BV -> Bool+prop_mult_comm a b = a * b ==. b * a++prop_mult_assoc :: BV3 -> Bool+prop_mult_assoc (BV3 a b c) = (a * b) * c ==. a * (b * c)++prop_mult_plus_distrib :: BV3 -> Bool+prop_mult_plus_distrib (BV3 a b c) = a * (b + c) ==. (a * b) + (a * c)++-- * Division++prop_div :: BV -> BV -> Property+prop_div a b = b /= 0 ==> a == q*b + r && r <= b+ where (q,r) = quotRem a b++prop_sdiv_is_div :: BV -> BV -> Property+prop_sdiv_is_div a b =+ isNat a && isPos b ==> a `sdiv` b ==. a `div` b++prop_srem_is_rem :: BV -> BV -> Property+prop_srem_is_rem a b =+ isNat a && isPos b ==> a `srem` b ==. a `rem` b++prop_smod_is_rem :: BV -> BV -> Property+prop_smod_is_rem a b =+ isNat a && isPos b ==> a `smod` b ==. a `rem` b++-- * Not++prop_not_id :: BV -> Bool+prop_not_id a = not_(not_ a) ==. a++-- * And++prop_and_comm :: BV -> BV -> Bool+prop_and_comm a b = a .&. b ==. b .&. a++prop_and_assoc :: BV3 -> Bool+prop_and_assoc (BV3 a b c) = (a .&. b) .&. c ==. a .&. (b .&. c)++-- * Shift++prop_shl_id :: BV -> Bool+prop_shl_id a = a `shiftL` 0 ==. a++prop_shl_0 :: BV -> Int -> Property+prop_shl_0 a i = i >= size a ==> a `shiftL` i == 0++prop_shl_mul :: BV -> Property+prop_shl_mul a = forallIndex1Of a $ \i ->+ a `shiftL` i == a * bitVec n ((2::Integer)^i)+ where n = size a++prop_shr_id :: BV -> Bool+prop_shr_id a = a `shiftR` 0 ==. a++prop_shr_0 :: BV -> Int -> Property+prop_shr_0 a i = i >= size a ==> a `shiftR` i == 0++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++-- * Rotate++prop_rol_id :: BV -> Bool+prop_rol_id a = a `rotateL` (size a) ==. a++prop_ror_id :: BV -> Bool+prop_ror_id a = a `rotateR` (size a) ==. a++-- * Split & group++prop_split_join_id :: BV -> Property+prop_split_join_id a = forallDivisorOf (size a) $ \n ->+ join (split n a) ==. a++prop_group_join_id :: BV -> Property+prop_group_join_id a = forallDivisorOf (size a) $ \n ->+ join (group_ n a) ==. a+
bv.cabal view
@@ -1,7 +1,7 @@ Name: bv-Version: 0.2.1-Synopsis: Bit-vectors library+Version: 0.2.2+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@@ -18,8 +18,25 @@ type: mercurial location: https://bitbucket.org/iago/bv-haskell +Flag test+ Description: Build the test suite, including an executable to run it.+ Default: False+ Library Exposed-modules: Data.BitVector -- Other-modules: ghc-options: -Wall Build-depends: base >=4.4 && <5++Executable bv-tester+ if flag(test)+ Buildable: True+ Build-depends: base >=4.4 && <5,+ QuickCheck >=2.4 && < 2.7,+ test-framework-quickcheck2 ==0.3.*,+ test-framework-th ==0.2.*+ else+ Buildable: False++ Main-Is: Properties.hs+ ghc-options: -Wall