bv-sized 0.2.0 → 0.2.1

raw patch · 5 files changed

+98/−57 lines, 5 filesdep +prettyclassPVP ok

version bump matches the API change (PVP)

Dependencies added: prettyclass

API changes (from Hackage documentation)

Files

• bv-sized.cabal +3/−1
• changelog.md +6/−0
• src/Data/BitVector/Sized.hs +48/−28
• src/Data/BitVector/Sized/BitLayout.hs +40/−28
• stack.yaml +1/−0

@@ -1,5 +1,5 @@ name:                bv-sized-version:             0.2.0+version:             0.2.1 category:            Bit Vectors synopsis:            a BitVector datatype that is parameterized by the vector width description:@@ -22,6 +22,7 @@                      , containers >= 0.5.11 && < 0.6                      , lens >= 4 && < 5                      , parameterized-utils+                     , prettyclass >= 1.0 && < 2.0                      , random >= 1.1 && < 1.2                      , QuickCheck >= 2.11 && < 2.12   hs-source-dirs:      src@@ -39,5 +40,6 @@                      , bv-sized                      , lens >= 4 && < 5                      , parameterized-utils+                     , prettyclass >= 1.0 && < 2.0                      , random >= 1.1 && < 1.2                      , QuickCheck >= 2.11 && < 2.12

@@ -16,3 +16,9 @@   * bv -> bitVector, so this is very much a breaking change   * bvShiftL, bvShiftRL, bvShiftRA   * bvLTU, bvLTS++## 0.2.1 *March 2018*+  * bvMulFSU+  * bvDivU, bvDivS+  * Added Read instance, fixed Show to be compatible. Using prettyclass for+    pretty printing. (I guess this is semi-breaking, but whatever.)

@@ -2,10 +2,11 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeOperators #-}  {-|-Module      : Data.BitVector.Sized.Internal+Module      : Data.BitVector.Sized Copyright   : (c) Benjamin Selfridge, 2018                   Galois Inc. License     : BSD3@@ -26,13 +27,13 @@     -- not need to know the width at compile time. They are all width-preserving.   , bvAnd, bvOr, bvXor   , bvComplement-  , bvShift, bvShiftL, bvShiftRA, bvShiftRL,  bvRotate+  , bvShift, bvShiftL, bvShiftRA, bvShiftRL, bvRotate   , bvWidth   , bvTestBit   , bvPopCount   , bvTruncBits     -- * Arithmetic operations (width-preserving)-  , bvAdd, bvMul+  , bvAdd, bvMul, bvDivU, bvDivS   , bvAbs, bvNegate   , bvSignum   , bvLTS, bvLTU@@ -42,7 +43,7 @@   , bvExtract, bvExtractWithRepr   , bvZext, bvZextWithRepr   , bvSext, bvSextWithRepr-  , bvMulFU, bvMulFS+  , bvMulFU, bvMulFS, bvMulFSU     -- * Conversions to Integer   , bvIntegerU   , bvIntegerS@@ -52,10 +53,13 @@ import Data.Parameterized.Classes import Data.Parameterized.NatRepr import GHC.TypeLits+import Numeric import System.Random import Test.QuickCheck (Arbitrary(..), choose)+import Text.PrettyPrint.HughesPJClass import Text.Printf import Unsafe.Coerce (unsafeCoerce)+ ---------------------------------------- -- BitVector data type definitions @@ -63,20 +67,15 @@ 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.+-- | Construct a bit vector with a particular width, 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. -- -- >>> bitVector 0xA :: BitVector 4--- 0xa<4>--- >>> 0xA :: BitVector 4--- >>> 0xA :: BitVector 3--- 0x2<3>--- >>> (-1) :: BitVector 8--- 0xff<8>--- >>> (-1) :: BitVector 32--- 0xffffffff<32>+-- 0xa+-- >>> :type it+-- it :: BitVector 4 bitVector :: KnownNat w => Integer -> BitVector w bitVector x = BV wRepr (truncBits width (fromIntegral x))   where wRepr = knownNat@@ -177,6 +176,17 @@ bvMul (BV wRepr x) (BV _ y) = BV wRepr (truncBits width (x * y))   where width = natValue wRepr +-- | Bitwise division (unsigned).+bvDivU :: BitVector w -> BitVector w -> BitVector w+bvDivU (BV wRepr x) (BV _ y) = BV wRepr (x `div` y)++-- | Bitwise division (signed).+bvDivS :: BitVector w -> BitVector w -> BitVector w+bvDivS bv1@(BV wRepr _) bv2 = BV wRepr (truncBits width (x `div` y))+  where x = bvIntegerS bv1+        y = bvIntegerS bv2+        width = natValue wRepr+ -- | Bitwise absolute value. bvAbs :: BitVector w -> BitVector w bvAbs bv@(BV wRepr _) = BV wRepr abs_x@@ -207,8 +217,8 @@  -- | Concatenate two bit vectors. ----- >>> (0xAA :: BitVector 8 `bvConcat` 0xBCDEF0 :: BitVector 24)--- 0xaabcdef0<32>+-- >>> (0xAA :: BitVector 8) `bvConcat` (0xBCDEF0 :: BitVector 24)+-- 0xaabcdef0 -- >>> :type it -- it :: BitVector 32 --@@ -230,7 +240,7 @@ -- inferred from a type-level context. -- -- >>> bvExtract 12 (0xAABCDEF0 :: BitVector 32) :: BitVector 8--- 0xcd<8>+-- 0xcd -- -- 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.@@ -292,13 +302,26 @@         prodRepr = wRepr `addNat` wRepr'         width = natValue prodRepr +-- | Fully multiply two bit vectors, treating the first as a signed integer and the+-- second as an unsigned integer, returning a bit vector whose length is equal to the+-- sum of the inputs.+bvMulFSU :: BitVector w -> BitVector w' -> BitVector (w+w')+bvMulFSU bv1@(BV wRepr _) bv2@(BV wRepr' _) = BV prodRepr (truncBits width (x'*y'))+  where x' = bvIntegerS bv1+        y' = bvIntegerU bv2+        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+  show (BV _ x) = "0x" ++ showHex x "" +instance KnownNat w => Read (BitVector w) where+  readsPrec s =+    (fmap . fmap) (\(a,s') -> (bitVector a, s')) (readsPrec s :: ReadS Integer)+ instance ShowF BitVector  instance Eq (BitVector w) where@@ -360,17 +383,14 @@     let (x, gen') = random gen     in (bitVector x, gen') -------------------------------------------- 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>"++instance Pretty (BitVector w) where+  -- | Pretty print a bit vector (shows its width)+  pPrint (BV wRepr x) = text $ prettyHex (natValue wRepr) x  ---------------------------------------- -- Bits

@@ -1,8 +1,10 @@ {-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeOperators #-}  {-|@@ -39,13 +41,14 @@ import qualified Data.Sequence as S import Data.Sequence (Seq) import GHC.TypeLits+import Text.PrettyPrint.HughesPJClass (Pretty(..), text)  -- | 'Chunk' type, parameterized by chunk width. The internal 'Int' is the -- position of the least significant bit of the chunk, and the type-level nat 'w' is -- the width of the chunk. -- -- >>> chunk 2 :: Chunk 5--- [2...6]+-- Chunk 5 2 -- -- Intuitively, the above chunk index captures the notion of /embedding/ a -- 'BitVector' @5@ (bit vector of width 5) into a larger 'BitVector' at index 2,@@ -63,16 +66,25 @@ chunk :: KnownNat w => Int -> Chunk w chunk start = Chunk knownNat start -instance Show (Chunk w) where-  show (Chunk wRepr start)-    | width > 0 =-      "[" ++ show (start + width - 1) ++ "..." ++ show start ++ "]"-    | otherwise = "[" ++ show start ++ "]"-    where width = fromIntegral (natValue wRepr)+deriving instance Show (Chunk w)  instance ShowF Chunk where   showF = show +instance Pretty (Chunk w) where+  pPrint (Chunk wRepr start)+    | width > 0 = text $+      "[" ++ show (start + width - 1) ++ "..." ++ show start ++ "]"+    | otherwise = text $ "[" ++ show start ++ "]"+    where width = fromIntegral (natValue wRepr)++instance Pretty (Some Chunk) where+  pPrint (Some (Chunk wRepr start))+    | width > 0 = text $+      "[" ++ show (start + width - 1) ++ "..." ++ show start ++ "]"+    | otherwise = text $ "[" ++ show start ++ "]"+    where width = fromIntegral (natValue wRepr)+ -- | BitLayout type, parameterized by target width and source width. @t@ is the -- target width, @s@ is the source width. @s@ should always be less than or equal to -- @t@.@@ -81,10 +93,10 @@ -- like so: -- -- >>> empty :: BitLayout 32 0--- []+-- BitLayout 32 0 (fromList []) -- >>> let layout = (chunk 25 :: Chunk 7) <: (chunk 7 :: Chunk 5) <: (empty :: BitLayout 32 0) -- >>> layout--- [[25...31],[7...11]]+-- BitLayout 32 12 (fromList [Chunk 5 7,Chunk 7 25]) -- >>> :type it -- it :: BitLayout 32 12 --@@ -119,22 +131,22 @@ -- Example use of @inject@/@extract@: -- -- >>> let bl = (chunk 25 :: Chunk 7) <: (chunk 7 :: Chunk 5) <: (empty :: BitLayout 32 0)--- >>> bl--- [[25...31],[7...11]]--- >>> let sVec = bv 0b111111100001 :: BitVector 12+-- >>> let sVec = bitVector 0b111111100001 :: BitVector 12 -- >>> sVec--- 0xfe1<12>--- >>> inject bl (bv 0) (bv 0b111111100001)--- 0xfe000080<32>--- >>> extract bl $ inject bl (bv 0) (bv 0b111111100001)--- 0xfe1<12>+-- 0xfe1+-- >>> inject bl (bitVector 0) (bitVector 0b111111100001)+-- 0xfe000080+-- >>> extract bl $ inject bl (bitVector 0) (bitVector 0b111111100001)+-- 0xfe1  data BitLayout (t :: Nat) (s :: Nat) :: * where   BitLayout :: NatRepr t -> NatRepr s -> Seq (Some Chunk) -> BitLayout t s -instance Show (BitLayout t s) where-  show (BitLayout _ _ cIdxs) = show (reverse $ toList cIdxs)+instance Pretty (BitLayout t s) where+  pPrint (BitLayout _ _ chks) = text $ show (pPrint <$> reverse $ toList chks) +deriving instance Show (BitLayout t s)+ -- | Construct an empty 'BitLayout'. empty :: KnownNat t => BitLayout t 0 empty = BitLayout knownNat knownNat S.empty@@ -146,25 +158,25 @@ (<:) :: Chunk r             -- ^ chunk to add      -> BitLayout t s       -- ^ layout we are adding the chunk to      -> BitLayout t (r + s)-cIdx@(Chunk rRepr _) <: bl@(BitLayout tRepr sRepr chunks) =-  if cIdx `chunkFits` bl-  then BitLayout tRepr (rRepr `addNat` sRepr) (chunks S.|> Some cIdx)+chk@(Chunk rRepr _) <: bl@(BitLayout tRepr sRepr chunks) =+  if chk `chunkFits` bl+  then BitLayout tRepr (rRepr `addNat` sRepr) (chunks S.|> Some chk)   else error $-       "chunk " ++ show cIdx ++ " does not fit in layout of size " +++       "chunk " ++ show chk ++ " does not fit in layout of size " ++        show (natValue tRepr) ++ ": " ++ show bl  -- TODO: check precedence (associativity is correct) infixr 6 <:  chunkFits :: Chunk r -> BitLayout t s -> Bool-chunkFits cIdx@(Chunk rRepr start) (BitLayout tRepr sRepr chunks) =+chunkFits chk@(Chunk rRepr start) (BitLayout tRepr sRepr chunks) =   (natValue rRepr + natValue sRepr <= natValue tRepr) && -- widths are ok   (fromIntegral start + natValue rRepr <= natValue tRepr) && -- chunk lies within the bit vector   (0 <= start) &&-  noOverlaps cIdx (toList chunks)+  noOverlaps chk (toList chunks)  noOverlaps :: Chunk r -> [Some Chunk] -> Bool-noOverlaps cIdx cIdxs = all (chunksDontOverlap (Some cIdx)) cIdxs+noOverlaps chk chks = all (chunksDontOverlap (Some chk)) chks  chunksDontOverlap :: Some Chunk -> Some Chunk -> Bool chunksDontOverlap (Some (Chunk chunkRepr1 start1)) (Some (Chunk chunkRepr2 start2)) =@@ -220,8 +232,8 @@            -> BitVector t     -- ^ input vector            -> BitVector s extractAll sRepr _ [] _ = BV sRepr 0-extractAll sRepr outStart (cIdx@(Some (Chunk chunkRepr _)) : chunks) tVec =-  extractChunk sRepr outStart cIdx tVec `bvOr`+extractAll sRepr outStart (chk@(Some (Chunk chunkRepr _)) : chunks) tVec =+  extractChunk sRepr outStart chk tVec `bvOr`   extractAll sRepr (outStart + chunkWidth) chunks tVec   where chunkWidth = fromInteger (natValue chunkRepr) 

@@ -7,5 +7,6 @@ - containers-0.5.11.0 - lens-4.16 - parameterized-utils-1.0.0+- prettyclass-1.0.0.0 - random-1.1 - QuickCheck-2.11.3