bv-sized 0.1.0.0 → 0.1.1.0
raw patch · 5 files changed
+331/−329 lines, 5 filesdep +containersdep +lensPVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies added: containers, lens
API changes (from Hackage documentation)
- Data.BitVector.Sized.Internal: (<:>) :: BitVector v -> BitVector w -> BitVector (v + w)
- Data.BitVector.Sized.Internal: [BV] :: NatRepr w -> Integer -> BitVector w
- Data.BitVector.Sized.Internal: bv :: KnownNat w => Integer -> BitVector w
- Data.BitVector.Sized.Internal: bvAbs :: BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvAdd :: BitVector w -> BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvAnd :: BitVector w -> BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvComplement :: BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvConcat :: BitVector v -> BitVector w -> BitVector (v + w)
- Data.BitVector.Sized.Internal: bvExtract :: forall w w'. (KnownNat w') => Int -> BitVector w -> BitVector w'
- Data.BitVector.Sized.Internal: bvExtractWithRepr :: NatRepr w' -> Int -> BitVector w -> BitVector w'
- Data.BitVector.Sized.Internal: bvIntegerS :: BitVector w -> Integer
- Data.BitVector.Sized.Internal: bvIntegerU :: BitVector w -> Integer
- Data.BitVector.Sized.Internal: bvMul :: BitVector w -> BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvNegate :: BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvOr :: BitVector w -> BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvPopCount :: BitVector w -> Int
- Data.BitVector.Sized.Internal: bvRotate :: BitVector w -> Int -> BitVector w
- Data.BitVector.Sized.Internal: bvSext :: forall w w'. KnownNat w' => BitVector w -> BitVector w'
- Data.BitVector.Sized.Internal: bvSextWithRepr :: NatRepr w' -> BitVector w -> BitVector w'
- Data.BitVector.Sized.Internal: bvShift :: BitVector w -> Int -> BitVector w
- Data.BitVector.Sized.Internal: bvSignum :: BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvTestBit :: BitVector w -> Int -> Bool
- Data.BitVector.Sized.Internal: bvWidth :: BitVector w -> Int
- Data.BitVector.Sized.Internal: bvXor :: BitVector w -> BitVector w -> BitVector w
- Data.BitVector.Sized.Internal: bvZext :: forall w w'. KnownNat w' => BitVector w -> BitVector w'
- Data.BitVector.Sized.Internal: bvZextWithRepr :: NatRepr w' -> BitVector w -> BitVector w'
- Data.BitVector.Sized.Internal: data BitVector (w :: Nat) :: *
- Data.BitVector.Sized.Internal: infixl 6 <:>
- Data.BitVector.Sized.Internal: instance Data.Parameterized.Classes.EqF Data.BitVector.Sized.Internal.BitVector
- Data.BitVector.Sized.Internal: instance Data.Parameterized.Classes.ShowF Data.BitVector.Sized.Internal.BitVector
- Data.BitVector.Sized.Internal: instance Data.Type.Equality.TestEquality Data.BitVector.Sized.Internal.BitVector
- Data.BitVector.Sized.Internal: instance GHC.Classes.Eq (Data.BitVector.Sized.Internal.BitVector w)
- Data.BitVector.Sized.Internal: instance GHC.Show.Show (Data.BitVector.Sized.Internal.BitVector w)
- Data.BitVector.Sized.Internal: instance GHC.TypeNats.KnownNat w => Data.Bits.Bits (Data.BitVector.Sized.Internal.BitVector w)
- Data.BitVector.Sized.Internal: instance GHC.TypeNats.KnownNat w => Data.Bits.FiniteBits (Data.BitVector.Sized.Internal.BitVector w)
- Data.BitVector.Sized.Internal: instance GHC.TypeNats.KnownNat w => GHC.Enum.Bounded (Data.BitVector.Sized.Internal.BitVector w)
- Data.BitVector.Sized.Internal: instance GHC.TypeNats.KnownNat w => GHC.Enum.Enum (Data.BitVector.Sized.Internal.BitVector w)
- Data.BitVector.Sized.Internal: instance GHC.TypeNats.KnownNat w => GHC.Num.Num (Data.BitVector.Sized.Internal.BitVector w)
+ Data.BitVector.Sized: [BV] :: NatRepr w -> Integer -> BitVector w
+ Data.BitVector.Sized: bvAbs :: BitVector w -> BitVector w
+ Data.BitVector.Sized: bvAdd :: BitVector w -> BitVector w -> BitVector w
+ Data.BitVector.Sized: bvAnd :: BitVector w -> BitVector w -> BitVector w
+ Data.BitVector.Sized: bvComplement :: BitVector w -> BitVector w
+ Data.BitVector.Sized: bvExtractWithRepr :: NatRepr w' -> Int -> BitVector w -> BitVector w'
+ Data.BitVector.Sized: bvMul :: BitVector w -> BitVector w -> BitVector w
+ Data.BitVector.Sized: bvMulFS :: BitVector w -> BitVector w' -> BitVector (w + w')
+ Data.BitVector.Sized: bvMulFU :: BitVector w -> BitVector w' -> BitVector (w + w')
+ Data.BitVector.Sized: bvNegate :: BitVector w -> BitVector w
+ Data.BitVector.Sized: bvOr :: BitVector w -> BitVector w -> BitVector w
+ Data.BitVector.Sized: bvPopCount :: BitVector w -> Int
+ Data.BitVector.Sized: bvRotate :: BitVector w -> Int -> BitVector w
+ Data.BitVector.Sized: bvSextWithRepr :: NatRepr w' -> BitVector w -> BitVector w'
+ Data.BitVector.Sized: bvShift :: BitVector w -> Int -> BitVector w
+ Data.BitVector.Sized: bvSignum :: BitVector w -> BitVector w
+ Data.BitVector.Sized: bvTestBit :: BitVector w -> Int -> Bool
+ Data.BitVector.Sized: bvTruncBits :: BitVector w -> Int -> BitVector w
+ Data.BitVector.Sized: bvWidth :: BitVector w -> Int
+ Data.BitVector.Sized: bvXor :: BitVector w -> BitVector w -> BitVector w
+ Data.BitVector.Sized: bvZextWithRepr :: NatRepr w' -> BitVector w -> BitVector w'
+ Data.BitVector.Sized: instance Data.Parameterized.Classes.EqF Data.BitVector.Sized.BitVector
+ Data.BitVector.Sized: instance Data.Parameterized.Classes.ShowF Data.BitVector.Sized.BitVector
+ Data.BitVector.Sized: instance Data.Type.Equality.TestEquality Data.BitVector.Sized.BitVector
+ Data.BitVector.Sized: instance GHC.Classes.Eq (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.Classes.Ord (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.Show.Show (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.TypeNats.KnownNat w => Data.Bits.Bits (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.TypeNats.KnownNat w => Data.Bits.FiniteBits (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.TypeNats.KnownNat w => GHC.Enum.Bounded (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.TypeNats.KnownNat w => GHC.Enum.Enum (Data.BitVector.Sized.BitVector w)
+ Data.BitVector.Sized: instance GHC.TypeNats.KnownNat w => GHC.Num.Num (Data.BitVector.Sized.BitVector w)
Files
- bv-sized.cabal +3/−2
- changelog.md +10/−0
- src/Data/BitVector/Sized.hs +316/−10
- src/Data/BitVector/Sized/Internal.hs +0/−317
- stack.yaml +2/−0
bv-sized.cabal view
@@ -1,5 +1,5 @@ name: bv-sized-version: 0.1.0.0+version: 0.1.1.0 category: Bit Vectors synopsis: a BitVector datatype that is parameterized by the vector width description:@@ -17,8 +17,9 @@ library exposed-modules: Data.BitVector.Sized- Data.BitVector.Sized.Internal build-depends: base >= 4.7 && < 5+ , containers >= 0.5.11 && < 0.6+ , lens >= 4 && < 5 , parameterized-utils hs-source-dirs: src default-language: Haskell2010
+ changelog.md view
@@ -0,0 +1,10 @@+# Changelog for [`bv-sized` package](http://hackage.haskell.org/package/bv-sized)++## 0.1.0.0 *March 2018*+ * First release++## 0.1.1.0 *March 2018*+ * added functions `bvMulFS`/`bvMulFU` for full bitvector multiplication+ without truncation+ * removed Internal module, now export all those functions in Data.BitVector.Sized+ * fixed the bv*WithRepr functions, which were not truncating the inputs properly
src/Data/BitVector/Sized.hs view
@@ -5,7 +5,7 @@ {-# LANGUAGE TypeOperators #-} {-|-Module : Data.BitVector.Sized+Module : Data.BitVector.Sized.Internal Copyright : (c) Benjamin Selfridge, 2018 Galois Inc. License : BSD3@@ -15,24 +15,330 @@ This module defines a width-parameterized 'BitVector' type and various associated operations that assume a 2's complement representation.--For more fine-grained access to the internals (including explicit 'Data.Parameterized.NatRepr's), see-'Data.BitVector.Sized.Internal'. -} module Data.BitVector.Sized ( -- * BitVector type- BitVector+ BitVector(..) , bv- -- * Bitwise operations (variable width)+ -- * Bitwise operations (width-preserving)+ -- | These are alternative versions of some of the 'Bits' functions where we do+ -- not need to know the width at compile time. They are all width-preserving.+ , bvAnd, bvOr, bvXor+ , bvComplement+ , bvShift, bvRotate+ , bvWidth+ , bvTestBit+ , bvPopCount+ , bvTruncBits+ -- * Arithmetic operations (width-preserving)+ , bvAdd, bvMul+ , bvAbs, bvNegate+ , bvSignum+ -- * Variable-width operations -- | These are functions that involve bit vectors of different lengths. , bvConcat, (<:>)- , bvExtract- , bvZext- , bvSext+ , bvExtract, bvExtractWithRepr+ , bvZext, bvZextWithRepr+ , bvSext, bvSextWithRepr+ , bvMulFU, bvMulFS -- * Conversions to Integer , bvIntegerU , bvIntegerS ) where -import Data.BitVector.Sized.Internal+import Data.Bits+import Data.Parameterized.Classes+import Data.Parameterized.NatRepr+import GHC.TypeLits+import Text.Printf+import Unsafe.Coerce (unsafeCoerce)+----------------------------------------+-- BitVector data type definitions++-- | BitVector datatype, parameterized by width.+data BitVector (w :: Nat) :: * where+ BV :: NatRepr w -> Integer -> BitVector w++-- | Construct a bit vector in a context where the width is inferrable from the type+-- context. The 'Integer' input (an unbounded data type, hence with an infinite-width+-- bit representation), whether positive or negative is silently truncated to fit+-- into the number of bits demanded by the return type.+--+-- >>> bv 0xA :: BitVector 4+-- 0xa<4>+-- >>> bv 0xA :: BitVector 3+-- 0x2<3>+-- >>> bv (-1) :: BitVector 8+-- 0xff<8>+-- >>> bv (-1) :: BitVector 32+-- 0xffffffff<32>++bv :: KnownNat w => Integer -> BitVector w+bv x = BV wRepr (truncBits width (fromIntegral x))+ where wRepr = knownNat+ width = natValue wRepr++----------------------------------------+-- BitVector -> Integer functions++-- | Unsigned interpretation of a bit vector as a (positive) Integer.+bvIntegerU :: BitVector w -> Integer+bvIntegerU (BV _ x) = x++-- | Signed interpretation of a bit vector as an Integer.+bvIntegerS :: BitVector w -> Integer+bvIntegerS bvec = case bvTestBit bvec (width - 1) of+ True -> bvIntegerU bvec - (1 `shiftL` width)+ False -> bvIntegerU bvec+ where width = bvWidth bvec++----------------------------------------+-- BitVector w operations (fixed width)++-- | Bitwise and.+bvAnd :: BitVector w -> BitVector w -> BitVector w+bvAnd (BV wRepr x) (BV _ y) = BV wRepr (x .&. y)++-- | Bitwise or.+bvOr :: BitVector w -> BitVector w -> BitVector w+bvOr (BV wRepr x) (BV _ y) = BV wRepr (x .|. y)++-- | Bitwise xor.+bvXor :: BitVector w -> BitVector w -> BitVector w+bvXor (BV wRepr x) (BV _ y) = BV wRepr (x `xor` y)++-- | Bitwise complement (flip every bit).+bvComplement :: BitVector w -> BitVector w+bvComplement (BV wRepr x) = BV wRepr (truncBits width (complement x))+ where width = natValue wRepr++-- | Bitwise shift.+bvShift :: BitVector w -> Int -> BitVector w+bvShift bvec@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` shf))+ where width = natValue wRepr+ x = bvIntegerS bvec -- arithmetic right shift when negative++-- | Bitwise rotate.+bvRotate :: BitVector w -> Int -> BitVector w+bvRotate bvec rot' = leftChunk `bvOr` rightChunk+ where rot = rot' `mod` (bvWidth bvec)+ leftChunk = bvShift bvec rot+ rightChunk = bvShift bvec (rot - bvWidth bvec)++-- | Get the width of a 'BitVector'.+bvWidth :: BitVector w -> Int+bvWidth (BV wRepr _) = fromIntegral (natValue wRepr)++-- | Test if a particular bit is set.+bvTestBit :: BitVector w -> Int -> Bool+bvTestBit (BV _ x) b = testBit x b++-- | Get the number of 1 bits in a 'BitVector'.+bvPopCount :: BitVector w -> Int+bvPopCount (BV _ x) = popCount x++-- | Truncate a bit vector to a particular width given at runtime, while keeping the+-- type-level width constant.+bvTruncBits :: BitVector w -> Int -> BitVector w+bvTruncBits (BV wRepr x) b = BV wRepr (truncBits b x)++----------------------------------------+-- BitVector w arithmetic operations (fixed width)++-- | Bitwise add.+bvAdd :: BitVector w -> BitVector w -> BitVector w+bvAdd (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x + y))+ where width = natValue wRepr++-- | Bitwise multiply.+bvMul :: BitVector w -> BitVector w -> BitVector w+bvMul (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x * y))+ where width = natValue wRepr++-- | Bitwise absolute value.+bvAbs :: BitVector w -> BitVector w+bvAbs bvec@(BV wRepr _) = BV wRepr abs_x+ where width = natValue wRepr+ x = bvIntegerS bvec+ abs_x = truncBits width (abs x) -- this is necessary++-- | Bitwise negation.+bvNegate :: BitVector w -> BitVector w+bvNegate (BV wRepr x) = BV wRepr (truncBits width (-x))+ where width = fromIntegral (natValue wRepr) :: Integer++-- | Get the sign bit as a 'BitVector'.+bvSignum :: BitVector w -> BitVector w+bvSignum bvec@(BV wRepr _) = (bvShift bvec (1 - width)) `bvAnd` (BV wRepr 0x1)+ where width = fromIntegral (natValue wRepr)++----------------------------------------+-- Width-changing operations++-- | Concatenate two bit vectors.+--+-- >>> (bv 0xAA :: BitVector 8) `bvConcat` (bv 0xBCDEF0 :: BitVector 24)+-- 0xaabcdef0<32>+-- >>> :type it+-- it :: BitVector 32+--+-- Note that the first argument gets placed in the higher-order bits. The above+-- example should be illustrative enough.+bvConcat :: BitVector v -> BitVector w -> BitVector (v+w)+bvConcat (BV hiWRepr hi) (BV loWRepr lo) =+ BV (hiWRepr `addNat` loWRepr) ((hi `shiftL` loWidth) .|. lo)+ where loWidth = fromIntegral (natValue loWRepr)++-- | Infix 'bvConcat'.+(<:>) :: BitVector v -> BitVector w -> BitVector (v+w)+(<:>) = bvConcat++infixl 6 <:>++-- | Slice out a smaller bit vector from a larger one. The lowest significant bit is+-- given explicitly as an argument of type 'Int', and the length of the slice is+-- inferred from a type-level context.+--+-- >>> bvExtract 12 (bv 0xAABCDEF0 :: BitVector 32) :: BitVector 8+-- 0xcd<8>+--+-- Note that 'bvExtract' does not do any bounds checking whatsoever; if you try and+-- extract bits that aren't present in the input, you will get 0's.+bvExtract :: forall w w' . (KnownNat w')+ => Int+ -> BitVector w+ -> BitVector w'+bvExtract pos bvec = bv xShf+ where (BV _ xShf) = bvShift bvec (- pos)++-- | Unconstrained variant of 'bvExtract' with an explicit 'NatRepr' argument.+bvExtractWithRepr :: NatRepr w'+ -> Int+ -> BitVector w+ -> BitVector w'+bvExtractWithRepr repr pos bvec = BV repr (truncBits width xShf)+ where (BV _ xShf) = bvShift bvec (- pos)+ width = natValue repr++-- | Zero-extend a vector to one of greater length. If given an input of greater+-- length than the output type, this performs a truncation.+bvZext :: forall w w' . KnownNat w'+ => BitVector w+ -> BitVector w'+bvZext (BV _ x) = bv x++-- | Unconstrained variant of 'bvZext' with an explicit 'NatRepr' argument.+bvZextWithRepr :: NatRepr w'+ -> BitVector w+ -> BitVector w'+bvZextWithRepr repr (BV _ x) = BV repr (truncBits width x)+ where width = natValue repr++-- | Sign-extend a vector to one of greater length. If given an input of greater+-- length than the output type, this performs a truncation.+bvSext :: forall w w' . KnownNat w'+ => BitVector w+ -> BitVector w'+bvSext bvec = bv (bvIntegerS bvec)++-- | Unconstrained variant of 'bvSext' with an explicit 'NatRepr' argument.+bvSextWithRepr :: NatRepr w'+ -> BitVector w+ -> BitVector w'+bvSextWithRepr repr bvec = BV repr (truncBits width (bvIntegerS bvec))+ where width = natValue repr++-- | Fully multiply two bit vectors as unsigned integers, returning a bit vector+-- whose length is equal to the sum of the inputs.+bvMulFU :: BitVector w -> BitVector w' -> BitVector (w+w')+bvMulFU (BV wRepr x) (BV wRepr' y) = BV (wRepr `addNat` wRepr') (x*y)++-- | Fully multiply two bit vectors as signed integers, returning a bit vector whose+-- length is equal to the sum of the inputs.+bvMulFS :: BitVector w -> BitVector w' -> BitVector (w+w')+bvMulFS bvec1@(BV wRepr _) bvec2@(BV wRepr' _) = BV prodRepr (truncBits width (x'*y'))+ where x' = bvIntegerS bvec1+ y' = bvIntegerS bvec2+ prodRepr = wRepr `addNat` wRepr'+ width = natValue prodRepr++----------------------------------------+-- Class instances++instance Show (BitVector w) where+ show (BV wRepr val) = prettyHex width val+ where width = natValue wRepr++instance ShowF BitVector++instance Eq (BitVector w) where+ (BV _ x) == (BV _ y) = x == y++instance EqF BitVector where+ (BV _ x) `eqF` (BV _ y) = x == y++instance Ord (BitVector w) where+ (BV _ x) `compare` (BV _ y) = x `compare` y++instance TestEquality BitVector where+ testEquality (BV wRepr x) (BV wRepr' y) =+ case natValue wRepr == natValue wRepr' && x == y of+ True -> Just (unsafeCoerce (Refl :: a :~: a))+ False -> Nothing++instance KnownNat w => Bits (BitVector w) where+ (.&.) = bvAnd+ (.|.) = bvOr+ xor = bvXor+ complement = bvComplement+ shift = bvShift+ rotate = bvRotate+ bitSize = bvWidth+ bitSizeMaybe = Just . bvWidth+ isSigned = const False+ testBit = bvTestBit+ bit = bv . bit+ popCount = bvPopCount++instance KnownNat w => FiniteBits (BitVector w) where+ finiteBitSize = bvWidth++instance KnownNat w => Num (BitVector w) where+ (+) = bvAdd+ (*) = bvMul+ abs = bvAbs+ signum = bvSignum+ fromInteger = bv+ negate = bvNegate++instance KnownNat w => Enum (BitVector w) where+ toEnum = bv . fromIntegral+ fromEnum = fromIntegral . bvIntegerU++instance KnownNat w => Bounded (BitVector w) where+ minBound = bv 0+ maxBound = bv (-1)++----------------------------------------+-- UTILITIES++----------------------------------------+-- Pretty Printing++-- | Print an integral value in hex with a leading "0x"+prettyHex :: (Integral a, PrintfArg a, Show a) => a -> Integer -> String+prettyHex width val = printf format val width+ where numDigits = (width+3) `div` 4+ format = "0x%." ++ show numDigits ++ "x<%d>"++----------------------------------------+-- Bits++-- | Mask for a specified number of lower bits.+lowMask :: (Integral a, Bits b) => a -> b+lowMask numBits = complement (complement zeroBits `shiftL` fromIntegral numBits)++-- | Truncate to a specified number of lower bits.+truncBits :: (Integral a, Bits b) => a -> b -> b+truncBits width b = b .&. lowMask width
− src/Data/BitVector/Sized/Internal.hs
@@ -1,317 +0,0 @@-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeOperators #-}--{-|-Module : Data.BitVector.Sized.Internal-Copyright : (c) Benjamin Selfridge, 2018- Galois Inc.-License : BSD3-Maintainer : benselfridge@galois.com-Stability : experimental-Portability : portable--This module defines a width-parameterized 'BitVector' type and various associated-operations that assume a 2's complement representation. This module exports more of-the internals of the type as well as several functions that operate on explicit-'NatRepr's instead of requiring a 'KnownNat' constraint.--}--module Data.BitVector.Sized.Internal- ( -- * BitVector type- BitVector(..)- , bv- -- * Bitwise operations (width-preserving)- -- | These are alternative versions of some of the 'Bits' functions where we do- -- not need to know the width at compile time. They are all width-preserving.- , bvAnd, bvOr, bvXor- , bvComplement- , bvShift, bvRotate- , bvWidth- , bvTestBit- , bvPopCount- -- * Arithmetic operations (width-preserving)- , bvAdd, bvMul- , bvAbs, bvNegate- , bvSignum- -- * Bitwise operations (variable width)- -- | These are functions that involve bit vectors of different lengths.- , bvConcat, (<:>)- , bvExtract, bvExtractWithRepr- , bvZext, bvZextWithRepr- , bvSext, bvSextWithRepr- -- * Conversions to Integer- , bvIntegerU- , bvIntegerS- ) where--import Data.Bits-import Data.Parameterized.Classes-import Data.Parameterized.NatRepr-import GHC.TypeLits-import Text.Printf-import Unsafe.Coerce (unsafeCoerce)-------------------------------------------- BitVector data type definitions---- | BitVector datatype, parameterized by width.-data BitVector (w :: Nat) :: * where- BV :: NatRepr w -> Integer -> BitVector w---- | Construct a bit vector in a context where the width is inferrable from the type--- context. The 'Integer' input (an unbounded data type, hence with an infinite-width--- bit representation), whether positive or negative is silently truncated to fit--- into the number of bits demanded by the return type.------ >>> bv 0xA :: BitVector 4--- 0xa<4>--- >>> bv 0xA :: BitVector 3--- 0x2<3>--- >>> bv (-1) :: BitVector 8--- 0xff<8>--- >>> bv (-1) :: BitVector 32--- 0xffffffff<32>--bv :: KnownNat w => Integer -> BitVector w-bv x = BV wRepr (truncBits width (fromIntegral x))- where wRepr = knownNat- width = natValue wRepr--------------------------------------------- BitVector -> Integer functions---- | Unsigned interpretation of a bit vector as a (positive) Integer.-bvIntegerU :: BitVector w -> Integer-bvIntegerU (BV _ x) = x---- | Signed interpretation of a bit vector as an Integer.-bvIntegerS :: BitVector w -> Integer-bvIntegerS bvec = case bvTestBit bvec (width - 1) of- True -> bvIntegerU bvec - (1 `shiftL` width)- False -> bvIntegerU bvec- where width = bvWidth bvec--------------------------------------------- BitVector w operations (fixed width)---- | Bitwise and.-bvAnd :: BitVector w -> BitVector w -> BitVector w-bvAnd (BV wRepr x) (BV _ y) = BV wRepr (x .&. y)---- | Bitwise or.-bvOr :: BitVector w -> BitVector w -> BitVector w-bvOr (BV wRepr x) (BV _ y) = BV wRepr (x .|. y)---- | Bitwise xor.-bvXor :: BitVector w -> BitVector w -> BitVector w-bvXor (BV wRepr x) (BV _ y) = BV wRepr (x `xor` y)---- | Bitwise complement (flip every bit).-bvComplement :: BitVector w -> BitVector w-bvComplement (BV wRepr x) = BV wRepr (truncBits width (complement x))- where width = natValue wRepr---- | Bitwise shift.-bvShift :: BitVector w -> Int -> BitVector w-bvShift bvec@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` shf))- where width = natValue wRepr- x = bvIntegerS bvec -- arithmetic right shift when negative---- | Bitwise rotate.-bvRotate :: BitVector w -> Int -> BitVector w-bvRotate bvec rot' = leftChunk `bvOr` rightChunk- where rot = rot' `mod` (bvWidth bvec)- leftChunk = bvShift bvec rot- rightChunk = bvShift bvec (rot - bvWidth bvec)---- | Get the width of a 'BitVector'.-bvWidth :: BitVector w -> Int-bvWidth (BV wRepr _) = fromIntegral (natValue wRepr)---- | Test if a particular bit is set.-bvTestBit :: BitVector w -> Int -> Bool-bvTestBit (BV _ x) b = testBit x b---- | Get the number of 1 bits in a 'BitVector'.-bvPopCount :: BitVector w -> Int-bvPopCount (BV _ x) = popCount x--------------------------------------------- BitVector w arithmetic operations (fixed width)---- | Bitwise add.-bvAdd :: BitVector w -> BitVector w -> BitVector w-bvAdd (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x + y))- where width = natValue wRepr---- | Bitwise multiply.-bvMul :: BitVector w -> BitVector w -> BitVector w-bvMul (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x * y))- where width = natValue wRepr---- | Bitwise absolute value.-bvAbs :: BitVector w -> BitVector w-bvAbs bvec@(BV wRepr _) = BV wRepr abs_x- where width = natValue wRepr- x = bvIntegerS bvec- abs_x = truncBits width (abs x) -- this is necessary---- | Bitwise negation.-bvNegate :: BitVector w -> BitVector w-bvNegate (BV wRepr x) = BV wRepr (truncBits width (-x))- where width = fromIntegral (natValue wRepr) :: Integer---- | Get the sign bit as a 'BitVector'.-bvSignum :: BitVector w -> BitVector w-bvSignum bvec@(BV wRepr _) = (bvShift bvec (1 - width)) `bvAnd` (BV wRepr 0x1)- where width = fromIntegral (natValue wRepr)--------------------------------------------- Width-changing operations---- | Concatenate two bit vectors.------ >>> (bv 0xAA :: BitVector 8) `bvConcat` (bv 0xBCDEF0 :: BitVector 24)--- 0xaabcdef0<32>------ Note that the first argument gets placed in the higher-order bits. The above--- example should be illustrative enough.-bvConcat :: BitVector v -> BitVector w -> BitVector (v+w)-bvConcat (BV hiWRepr hi) (BV loWRepr lo) =- BV (hiWRepr `addNat` loWRepr) ((hi `shiftL` loWidth) .|. lo)- where loWidth = fromIntegral (natValue loWRepr)---- | Infix 'bvConcat'.-(<:>) :: BitVector v -> BitVector w -> BitVector (v+w)-(<:>) = bvConcat--infixl 6 <:>---- | Slice out a smaller bit vector from a larger one. The lowest significant bit is--- given explicitly as an argument of type 'Int', and the length of the slice is--- inferred from a type-level context.------ >>> bvExtract 12 (bv 0xAABCDEF0 :: BitVector 32) :: BitVector 8--- 0xcd<8>------ Note that 'bvExtract' does not do any bounds checking whatsoever; if you try and--- extract bits that aren't present in the input, you will get 0's.-bvExtract :: forall w w' . (KnownNat w')- => Int- -> BitVector w- -> BitVector w'-bvExtract pos bvec = bv xShf- where (BV _ xShf) = bvShift bvec (- pos)---- | Unconstrained variant of 'bvExtract' with an explicit 'NatRepr' argument.-bvExtractWithRepr :: NatRepr w'- -> Int- -> BitVector w- -> BitVector w'-bvExtractWithRepr repr pos bvec = BV repr xShf- where (BV _ xShf) = bvShift bvec (- pos)---- | Zero-extend a vector to one of greater length. If given an input of greater--- length than the output type, this performs a truncation.-bvZext :: forall w w' . KnownNat w'- => BitVector w- -> BitVector w'-bvZext (BV _ x) = bv x---- | Unconstrained variant of 'bvZext' with an explicit 'NatRepr' argument.-bvZextWithRepr :: NatRepr w'- -> BitVector w- -> BitVector w'-bvZextWithRepr repr (BV _ x) = BV repr x---- | Sign-extend a vector to one of greater length. If given an input of greater--- length than the output type, this performs a truncation.-bvSext :: forall w w' . KnownNat w'- => BitVector w- -> BitVector w'-bvSext bvec = bv (bvIntegerS bvec)---- | Unconstrained variant of 'bvSext' with an explicit 'NatRepr' argument.-bvSextWithRepr :: NatRepr w'- -> BitVector w- -> BitVector w'-bvSextWithRepr repr bvec = BV repr (bvIntegerS bvec)--------------------------------------------- Class instances--instance Show (BitVector w) where- show (BV wRepr val) = prettyHex width val- where width = natValue wRepr--instance ShowF BitVector--instance Eq (BitVector w) where- (BV _ x) == (BV _ y) = x == y--instance EqF BitVector where- (BV _ x) `eqF` (BV _ y) = x == y--instance TestEquality BitVector where- testEquality (BV wRepr x) (BV wRepr' y) =- case natValue wRepr == natValue wRepr' && x == y of- True -> Just (unsafeCoerce (Refl :: a :~: a))- False -> Nothing--instance KnownNat w => Bits (BitVector w) where- (.&.) = bvAnd- (.|.) = bvOr- xor = bvXor- complement = bvComplement- shift = bvShift- rotate = bvRotate- bitSize = bvWidth- bitSizeMaybe = Just . bvWidth- isSigned = const False- testBit = bvTestBit- bit = bv . bit- popCount = bvPopCount--instance KnownNat w => FiniteBits (BitVector w) where- finiteBitSize = bvWidth--instance KnownNat w => Num (BitVector w) where- (+) = bvAdd- (*) = bvMul- abs = bvAbs- signum = bvSignum- fromInteger = bv- negate = bvNegate--instance KnownNat w => Enum (BitVector w) where- toEnum = bv . fromIntegral- fromEnum = fromIntegral . bvIntegerU--instance KnownNat w => Bounded (BitVector w) where- minBound = bv 0- maxBound = bv (-1)--------------------------------------------- UTILITIES--------------------------------------------- Pretty Printing---- | Print an integral value in hex with a leading "0x"-prettyHex :: (Integral a, PrintfArg a, Show a) => a -> Integer -> String-prettyHex width val = printf format val width- where numDigits = (width+3) `div` 4- format = "0x%." ++ show numDigits ++ "x<%d>"--------------------------------------------- Bits---- | Mask for a specified number of lower bits.-lowMask :: (Integral a, Bits b) => a -> b-lowMask numBits = complement (complement zeroBits `shiftL` fromIntegral numBits)---- | Truncate to a specified number of lower bits.-truncBits :: (Integral a, Bits b) => a -> b -> b-truncBits width b = b .&. lowMask width
stack.yaml view
@@ -4,4 +4,6 @@ - . extra-deps:+- containers-0.5.11.0+- lens-4.16 - parameterized-utils-1.0.0