diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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. diff --git a/bv-sized.cabal b/bv-sized.cabal --- a/bv-sized.cabal +++ b/bv-sized.cabal @@ -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 diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -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 diff --git a/src/Data/BitVector/Sized.hs b/src/Data/BitVector/Sized.hs --- a/src/Data/BitVector/Sized.hs +++ b/src/Data/BitVector/Sized.hs @@ -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 diff --git a/src/Data/BitVector/Sized/App.hs b/src/Data/BitVector/Sized/App.hs new file mode 100644 --- /dev/null +++ b/src/Data/BitVector/Sized/App.hs @@ -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 diff --git a/src/Data/BitVector/Sized/BitLayout.hs b/src/Data/BitVector/Sized/BitLayout.hs --- a/src/Data/BitVector/Sized/BitLayout.hs +++ b/src/Data/BitVector/Sized/BitLayout.hs @@ -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)