bv-sized 0.3.0 → 0.4.0

raw patch · 6 files changed

+184/−43 lines, 6 filesdep +mtlPVP ok

version bump matches the API change (PVP)

Dependencies added: mtl

API changes (from Hackage documentation)

Files

• README.md +18/−5
• bv-sized.cabal +3/−1
• changelog.md +23/−20
• src/Data/BitVector/Sized.hs +8/−9
• src/Data/BitVector/Sized/App.hs +125/−0
• src/Data/BitVector/Sized/BitLayout.hs +7/−8

@@ -1,8 +1,21 @@ # bv-sized -This library defines a BitVector datatype that is parameterized by the vector-width.+## Overview -It is especially useful in applications where the length of every individual bit-vector will be known at compile time. Supports width-changing operations like-truncation, signed/unsigned extension, and extraction/bit slicing.+This library defines a `BitVector` datatype that is parameterized by the vector width.++## Additional features++### BitLayout++We also provides a module called `BitLayout`, which is handy for defining mappings+from smaller `BitVector`s into larger ones. This module is particularly useful when+defining encodings in an instruction set.++### App++To aid in building expression languages over `BitVector`s, we provide a module called+App, which supports combining expressions over `BitVector`s using the `BitVector`+operations and evaluating said expressions. It can be used in a pure context or in+conjunction with a state monad. This module was inspired by the `App` type in+[macaw](https://github.com/GaloisInc/macaw), Galois's binary analysis framework.

@@ -1,5 +1,5 @@ name:                bv-sized-version:             0.3.0+version:             0.4.0 category:            Bit Vectors synopsis:            a BitVector datatype that is parameterized by the vector width description:@@ -17,10 +17,12 @@  library   exposed-modules:     Data.BitVector.Sized+                     , Data.BitVector.Sized.App                      , Data.BitVector.Sized.BitLayout   build-depends:       base >= 4.7 && < 5                      , containers >= 0.5.11 && < 0.6                      , lens >= 4 && < 5+                     , mtl >= 2 && < 3                      , parameterized-utils                      , prettyclass >= 1.0 && < 2.0                      , random >= 1.1 && < 1.2

@@ -1,31 +1,34 @@ # Changelog for [`bv-sized` package](http://hackage.haskell.org/package/bv-sized) -## 0.1.0.0 *March 2018*-  * First release+## 0.4.0 *April 2018*+  * Added App module for BitVector expression languages and evaluation -## 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+## 0.3.0 *April 2018*+  * fixed bug with bvShiftR, it was doing a left shift!+  * Division now rounds to zero for negative integers, bvDiv -> bvQuot+  * added Ix instance for BitVector w+  * added bv0, zero-width vector+  * bvConcatMany, bvGetBytesU (conversion to/from list of bytes) -## 0.1.1.1 *March 2018*-  * added BitLayout+## 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.)  ## 0.2 *March 2018*   * 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.)+## 0.1.1.1 *March 2018*+  * added BitLayout -## 0.3.0 *April 2018*-  * fixed bug with bvShiftR, it was doing a left shift!-  * Division now rounds to zero for negative integers, bvDiv -> bvQuot-  * added Ix instance for BitVector w-  * added bv0, zero-width vector-  * bvConcatMany, bvGetBytesU (conversion to/from list of bytes)+## 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++## 0.1.0.0 *March 2018*+  * First release

@@ -2,7 +2,6 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeOperators #-}  {-|@@ -99,9 +98,9 @@  -- | Signed interpretation of a bit vector as an Integer. bvIntegerS :: BitVector w -> Integer-bvIntegerS bv = case bvTestBit bv (width - 1) of-  True  -> bvIntegerU bv - (1 `shiftL` width)-  False -> bvIntegerU bv+bvIntegerS bv = if bvTestBit bv (width - 1)+                then bvIntegerU bv - (1 `shiftL` width)+                else bvIntegerU bv   where width = bvWidth bv  ----------------------------------------@@ -151,7 +150,7 @@ -- | Bitwise rotate. bvRotate :: BitVector w -> Int -> BitVector w bvRotate bv rot' = leftChunk `bvOr` rightChunk-  where rot = rot' `mod` (bvWidth bv)+  where rot = rot' `mod` bvWidth bv         leftChunk = bvShift bv rot         rightChunk = bvShift bv (rot - bvWidth bv) @@ -222,7 +221,7 @@  -- | Get the sign bit as a 'BitVector'. bvSignum :: BitVector w -> BitVector w-bvSignum bv@(BV wRepr _) = (bvShift bv (1 - width)) `bvAnd` (BV wRepr 0x1)+bvSignum bv@(BV wRepr _) = bvShift bv (1 - width) `bvAnd` BV wRepr 0x1   where width = fromIntegral (natValue wRepr)  -- | Signed less than.@@ -387,9 +386,9 @@  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+    if natValue wRepr == natValue wRepr' && x == y+    then Just (unsafeCoerce (Refl :: a :~: a))+    else Nothing  instance KnownNat w => Bits (BitVector w) where   (.&.)        = bvAnd

@@ -0,0 +1,125 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE Rank2Types #-}+{-# LANGUAGE TypeOperators #-}++{-|+Module      : Data.BitVector.Sized.App+Copyright   : (c) Benjamin Selfridge, 2018+                  Galois Inc.+License     : None (yet)+Maintainer  : benselfridge@galois.com+Stability   : experimental+Portability : portable++This module exports a type, 'BVApp', to aid in building expression languages over+'BitVector's. Let @expr :: Nat -> *@ be some ADT of /expressions/ that yield+'BitVector's when evaluated. Then, given one or more values of type @expr w@+(i.e. one or more of these evaluatable expressions), 'BVApp' provides the various+constructors necessary for creating compound expressions involving pure 'BitVector'+operations. The @expr@ type can (and often will) include a constructor of type @BVApp+expr w -> expr w@ in order to create a recursive expression language.++In addition to the 'BVApp' type, we provide an evaluator which, given a function+mapping values of type @expr w@ to 'BitVector's, will evaluate the compound+'BVApp' expressions.+-}++module Data.BitVector.Sized.App+  ( BVApp(..)+  , evalBVApp+  , evalBVAppM+  ) where++import Control.Monad.Identity+import Data.BitVector.Sized+import Data.Parameterized+import Foreign.Marshal.Utils (fromBool)+import GHC.TypeLits++-- | Represents the application of a 'BitVector' operation to one or more+-- subexpressions.+data BVApp (expr :: Nat -> *) (w :: Nat) where+  -- Literal BitVector+  LitBVApp :: BitVector w -> BVApp expr w++  -- Bitwise operations+  AndApp :: !(expr w) -> !(expr w) -> BVApp expr w+  OrApp  :: !(expr w) -> !(expr w) -> BVApp expr w+  XorApp :: !(expr w) -> !(expr w) -> BVApp expr w+  NotApp :: !(expr w) -> BVApp expr w++  -- Shifts+  SllApp :: !(expr w) -> !(expr w) -> BVApp expr w+  SrlApp :: !(expr w) -> !(expr w) -> BVApp expr w+  SraApp :: !(expr w) -> !(expr w) -> BVApp expr w++  -- Arithmetic operations+  AddApp   :: !(expr w) -> !(expr w) -> BVApp expr w+  SubApp   :: !(expr w) -> !(expr w) -> BVApp expr w+  MulSApp  :: !(expr w) -> !(expr w) -> BVApp expr (w+w)+  MulUApp  :: !(expr w) -> !(expr w) -> BVApp expr (w+w)+  MulSUApp :: !(expr w) -> !(expr w) -> BVApp expr (w+w)+  DivUApp  :: !(expr w) -> !(expr w) -> BVApp expr w+  DivSApp  :: !(expr w) -> !(expr w) -> BVApp expr w+  RemUApp  :: !(expr w) -> !(expr w) -> BVApp expr w+  RemSApp  :: !(expr w) -> !(expr w) -> BVApp expr w++  -- Comparisons+  EqApp  :: !(expr w) -> !(expr w) -> BVApp expr 1+  LtuApp :: !(expr w) -> !(expr w) -> BVApp expr 1+  LtsApp :: !(expr w) -> !(expr w) -> BVApp expr 1++  -- Width-changing+  ZExtApp    :: NatRepr w' -> !(expr w) -> BVApp expr w'+  SExtApp    :: NatRepr w' -> !(expr w) -> BVApp expr w'+  ExtractApp :: NatRepr w' -> Int -> !(expr w) -> BVApp expr w'+  ConcatApp  :: !(expr w) -> !(expr w') -> BVApp expr (w+w')++  -- Other operations+  IteApp :: !(expr 1) -> !(expr w) -> !(expr w) -> BVApp expr w++-- | Evaluate a 'BVApp' given a monadic evaluation function for the parameterized type @expr@.+evalBVAppM :: Monad m+           => (forall w' . expr w' -> m (BitVector w')) -- ^ expression evaluator+           -> BVApp expr w                              -- ^ application+           -> m (BitVector w)+evalBVAppM _ (LitBVApp bv) = return bv+evalBVAppM eval (AndApp e1 e2) = bvAnd <$> eval e1 <*> eval e2+evalBVAppM eval (OrApp  e1 e2) = bvOr  <$> eval e1 <*> eval e2+evalBVAppM eval (XorApp e1 e2) = bvXor <$> eval e1 <*> eval e2+evalBVAppM eval (NotApp e)     = bvComplement <$> eval e+evalBVAppM eval (AddApp e1 e2) = bvAdd <$> eval e1 <*> eval e2+evalBVAppM eval (SubApp e1 e2) = bvAdd <$> eval e1 <*> (bvNegate <$> eval e2)+evalBVAppM eval (SllApp e1 e2) = bvShiftL  <$> eval e1 <*> (fromIntegral . bvIntegerU <$> eval e2)+evalBVAppM eval (SrlApp e1 e2) = bvShiftRL <$> eval e1 <*> (fromIntegral . bvIntegerU <$> eval e2)+evalBVAppM eval (SraApp e1 e2) = bvShiftRA <$> eval e1 <*> (fromIntegral . bvIntegerU <$> eval e2)+evalBVAppM eval (MulSApp  e1 e2) = bvMulFS  <$> eval e1 <*> eval e2+evalBVAppM eval (MulUApp  e1 e2) = bvMulFU  <$> eval e1 <*> eval e2+evalBVAppM eval (MulSUApp e1 e2) = bvMulFSU <$> eval e1 <*> eval e2+evalBVAppM eval (DivSApp  e1 e2) = bvQuotS  <$> eval e1 <*> eval e2+evalBVAppM eval (DivUApp  e1 e2) = bvQuotU  <$> eval e1 <*> eval e2+evalBVAppM eval (RemSApp  e1 e2) = bvRemS   <$> eval e1 <*> eval e2+evalBVAppM eval (RemUApp  e1 e2) = bvRemU   <$> eval e1 <*> eval e2+evalBVAppM eval (EqApp  e1 e2) = fromBool <$> ((==)  <$> eval e1 <*> eval e2)+evalBVAppM eval (LtuApp e1 e2) = fromBool <$> (bvLTU <$> eval e1 <*> eval e2)+evalBVAppM eval (LtsApp e1 e2) = fromBool <$> (bvLTS <$> eval e1 <*> eval e2)+evalBVAppM eval (ZExtApp wRepr e) = bvZextWithRepr wRepr <$> eval e+evalBVAppM eval (SExtApp wRepr e) = bvSextWithRepr wRepr <$> eval e+evalBVAppM eval (ExtractApp wRepr base e) = bvExtractWithRepr wRepr base <$> eval e+evalBVAppM eval (ConcatApp e1 e2) = do+  e1Val <- eval e1+  e2Val <- eval e2+  return $ e1Val `bvConcat` e2Val+evalBVAppM eval (IteApp eTest eT eF) = do+  testVal <- eval eTest+  tVal <- eval eT+  fVal <- eval eF+  return $ if testVal == 1 then tVal else fVal++-- | Evaluate a 'BVApp' given a pure evaluation function for the parameterized type @expr@.+evalBVApp :: (forall w' . expr w' -> BitVector w') -- ^ expression evaluator+          -> BVApp expr w                          -- ^ application+          -> BitVector w+evalBVApp eval bvApp = runIdentity $ evalBVAppM (return . eval) bvApp

@@ -64,7 +64,7 @@  -- | Construct a 'Chunk' in a context where the chunk width is known at compile time. chunk :: KnownNat w => Int -> Chunk w-chunk start = Chunk knownNat start+chunk = Chunk knownNat  deriving instance Show (Chunk w) @@ -176,13 +176,13 @@   noOverlaps chk (toList chunks)  noOverlaps :: Chunk r -> [Some Chunk] -> Bool-noOverlaps chk chks = all (chunksDontOverlap (Some chk)) chks+noOverlaps chk = all (chunksDontOverlap (Some chk))  chunksDontOverlap :: Some Chunk -> Some Chunk -> Bool chunksDontOverlap (Some (Chunk chunkRepr1 start1)) (Some (Chunk chunkRepr2 start2)) =-  case start1 <= start2 of-    True  -> start1 + chunkWidth1 <= start2-    False -> start2 + chunkWidth2 <= start1+  if start1 <= start2+  then start1 + chunkWidth1 <= start2+  else start2 + chunkWidth2 <= start1   where chunkWidth1 = fromIntegral (natValue chunkRepr1)         chunkWidth2 = fromIntegral (natValue chunkRepr2) @@ -212,7 +212,7 @@        -> BitVector s   -- ^ The smaller vector to be injected        -> BitVector t inject (BitLayout tRepr _ chunks) tVec sVec =-  (bvOrAtAll tRepr (toList chunks) sVec) `bvOr` tVec+  bvOrAtAll tRepr (toList chunks) sVec `bvOr` tVec  -- First, extract the appropriate bits as a BitVector t, where the relevant bits -- start at the LSB of the vector (so, mask and shiftL). Then, truncate to a@@ -241,8 +241,7 @@ extract :: BitLayout t s -- ^ The layout         -> BitVector t   -- ^ The larger vector to extract from         -> BitVector s-extract (BitLayout _ sRepr chunks) tVec =-  extractAll sRepr 0 (toList chunks) tVec+extract (BitLayout _ sRepr chunks) = extractAll sRepr 0 (toList chunks)  -- | Lens for bit layout. layoutLens :: BitLayout t s -> Simple Lens (BitVector t) (BitVector s)