diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,39 +1,12 @@ +[![Build Status](https://travis-ci.org/GaloisInc/bv-sized.svg?branch=master)](https://travis-ci.org/GaloisInc/bv-sized) + bv-sized - A Haskell library for manipulating width-parameterized bitvectors === copyright (c) Ben Selfridge, Galois Inc. 2018 -This library defines a `BitVector` datatype that is parameterized by the vector -width. - -Requirements -=== - -The following are a list of mandatory and secondary requirements for bv-sized. - -Mandatory Requirements -=== - -- Must support integer arithmetic on bitvectors of arbitrary width, assuming a - two's-complement representation. - -- Must support the construction of symbolic expressions involving bitvectors, - and evaluating those expressions in such a way that the "pure" bitvector - expression language can be embedded in a larger expression language. (See - Data.BitVector.Sized.App) - -- Declarative descriptions of bit encodings within an instruction word for the - purposes of ISA definitions and the like. (See Data.BitVector.Sized.BitLayout) - -Secondary Requirements -=== - -None. - -Current Status -=== - -The library is relatively stable and supports all the above requirements. +This library defines a bitvector datatype that is parameterized by the +vector width. Other information === 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.7.0 +version: 1.0.0 category: Bit Vectors synopsis: a BitVector datatype that is parameterized by the vector width description: @@ -16,34 +16,37 @@ cabal-version: >=1.10 extra-source-files: README.md +source-repository head + type: git + location: https://github.com/GaloisInc/bv-sized + library exposed-modules: Data.BitVector.Sized - , Data.BitVector.Sized.App - , Data.BitVector.Sized.BitLayout + Data.BitVector.Sized.Signed + Data.BitVector.Sized.Unsigned + Data.BitVector.Sized.Overflow other-modules: Data.BitVector.Sized.Internal - build-depends: base >= 4.7 && < 5 - , containers >= 0.5.10 && < 0.7 - , lens >= 4 && < 5 - , mtl >= 2 && < 3 - , parameterized-utils >= 2.0 && < 3 - , pretty - , random >= 1.1 && < 1.2 - , QuickCheck >= 2.11 && < 2.12 + Data.BitVector.Sized.Panic + build-depends: base >= 4.10 && <5, + bitwise >= 1.0.0 && < 1.1, + bytestring >= 0.10.10 && < 0.11, + panic >= 0.4.0 && < 0.5, + parameterized-utils >= 2.0.2 && < 2.1, + th-lift >= 0.8.1 && < 0.9 hs-source-dirs: src default-language: Haskell2010 ghc-options: -Wall -test-suite bv-tests - type: exitcode-stdio-1.0 - default-language: Haskell2010 - ghc-options: -Wall - main-is: Test.hs - other-modules: Data.BitVector.Sized - hs-source-dirs: test, src - build-depends: base >= 4.7 && < 5 - , bv-sized - , lens >= 4 && < 5 - , parameterized-utils - , pretty - , random >= 1.1 && < 1.2 - , QuickCheck >= 2.11 && < 2.12 +test-suite bv-sized-tests + type: exitcode-stdio-1.0 + hs-source-dirs: test + main-is: Main.hs + build-depends: base >= 4.7 && < 5, + bv-sized, + bytestring >= 0.10.10 && < 0.11, + hedgehog >= 1.0.2 && < 1.1, + parameterized-utils >= 2.0.2 && < 2.1, + tasty >= 1.2.3 && < 1.3, + tasty-hedgehog >= 1.0.0.2 && < 1.1 + default-language: Haskell2010 + ghc-options: -Wall -Wcompat diff --git a/changelog.md b/changelog.md --- a/changelog.md +++ b/changelog.md @@ -1,10 +1,37 @@ # Changelog for [`bv-sized` package](http://hackage.haskell.org/package/bv-sized) +## 1.0.0 *May 2020* + +This is a completely breaking change and it is completely incompatible +with any previous use for this library. + + * Bitvectors no longer track their own width. Every operations that + relies on runtime awareness of the width (for instance, + truncations) requires an expicit 'NatRepr' argument. + * Bitvectors do not support any typical instances you might hope for + (Num, Bits, etc.). This is because they are not interpreted by + default as signed or unsigned, so any class that requires such an + interpretation is not supported. We do provide wrapper types that + supply those instances when the bitvector width is known + (SignedBV/UnsignedBV). + * Every operation has been renamed. Most are pretty straightforward + (e.g. bvAdd ==> add). + * Several previously unsupported operations have been added + (e.g. count leading zeros, conversion to/from bit/bytestrings) + * The App and BitLayout modules have been removed entirely. Both are + potentially useful, but are out of date and probably should be in + a different package anyway. + * New modules + * Data.BitVector.Sized.{Signed,Unsigned}: wrappers for BV that + provide many instances + * Data.BitVector.Sized.Overflow: wrappers for operations that + provide overflow information as part of the output + ## 0.7.0 *April 2019* - * extractWithRepr now takes a NatRepr as an argument to specify the index, which it - always should have. - * Updated to recent parameterized-utils hackage release, which fixes the build - failures in the previous bv-sized release. + * extractWithRepr now takes a NatRepr as an argument to specify the + index, which it always should have. + * Updated to recent parameterized-utils hackage release, which fixes + the build failures in the previous bv-sized release. ## 0.6.0 *March 2019* * changed WithRepr functions to ' @@ -17,8 +44,9 @@ * fixed github URL ## 0.5.0 *August 2018* - * Added a lot of better support for the App module, including a type class for - embedding BVApp expressions along with associated smart constructors + * Added a lot of better support for the App module, including a type + class for embedding BVApp expressions along with associated smart + constructors ## 0.4.0 *April 2018* * Added App module for BitVector expression languages and evaluation @@ -33,8 +61,9 @@ ## 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.) + * 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 @@ -45,10 +74,11 @@ * added BitLayout ## 0.1.1.0 *March 2018* - * added functions `bvMulFS`/`bvMulFU` for full bitvector multiplication - without truncation + * 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 + * 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 @@ -9,47 +9,106 @@ Module : Data.BitVector.Sized Copyright : (c) Galois Inc. 2018 License : BSD-3 -Maintainer : benselfridge@galois.com +Maintainer : Ben Selfridge 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 defines a width-parameterized 'BV' type and various +associated operations. A @'BV' w@ is a newtype around an 'Integer', so +operations that require the width take an explicit @'NatRepr' w@ +argument. We explicitly do not allow widths that cannot be represented +as an 'Prelude.Int', as we appeal to the underlying 'Prelude.Num' and +'Data.Bits.Bits' instances on 'Integer' for the implementation of many +of the same operations (which, in turn, require those widths to be +'Prelude.Int's). + +We omit all typeclass instances that require compile-time knowledge of +bitvector width, or force a signed or unsigned intepretation. Those +instances can be recovered via the use of +'Data.BitVector.Sized.Signed.SignedBV' or +'Data.BitVector.Sized.Unsigned.UnsignedBV'. + +This module should be imported qualified, as many of the names clash +with those in Prelude or other base packages. -} module Data.BitVector.Sized - ( -- * BitVector type - BitVector, pattern BitVector - , bitVector, bitVector' - , bv0 - -- * Bitwise operations (width-preserving) - -- | These are alternative versions of some of the 'Data.Bits' functions where we - -- do not need to know the width at compile time. They are all width-preserving. - , bvAnd, bvOr, bvXor - , bvComplement - , bvShift, bvShiftL, bvShiftRA, bvShiftRL, bvRotate - , bvWidth - , bvTestBit - , bvPopCount - , bvTruncBits + ( -- * 'BV.BV' type + BV.BV, pattern BV + -- * 'NatRepr's (from parameterized-utils) + , NatRepr + , knownNat + -- * Constructors + , mkBV, mkBVUnsigned, mkBVSigned + , unsignedClamp, signedClamp + , minUnsigned, maxUnsigned + , minSigned, maxSigned + -- * Construction from fixed-width data types + , bool + , word8, word16, word32, word64 + , int8, int16, int32, int64 + , bitsBE, bitsLE + , bytesBE, bytesLE + , bytestringBE, bytestringLE + -- * Conversions to primitive types + , asSigned + , asUnsigned + , asNatural + , asBitsBE, asBitsLE + , asBytesBE, asBytesLE + , asBytestringBE, asBytestringLE + -- * Bits operations (width-preserving) + -- | 'BV' versions of the functions in @Data.Bits@. + , and, or, xor + , complement + , shl, lshr, ashr, rotateL, rotateR + , zero, one, width + , bit, bit' + , setBit, setBit' + , clearBit, clearBit' + , complementBit, complementBit' + , testBit, testBit' + , popCount + , ctz, clz + , truncBits -- * Arithmetic operations (width-preserving) - , bvAdd, bvMul - , bvQuotU, bvQuotS - , bvRemU, bvRemS - , bvAbs, bvNegate - , bvSignum - , bvLTS, bvLTU + , add, sub, mul + , uquot, squot, sdiv + , urem, srem, smod + , uquotRem, squotRem, sdivMod + , abs, negate + , signBit + , signum + , slt, sle, ult, ule + , umin, umax + , smin, smax -- * Variable-width operations -- | These are functions that involve bit vectors of different lengths. - , bvConcat, (<:>), bvConcatMany, bvConcatMany' - , bvExtract, bvExtract' - , bvZext, bvZext' - , bvSext, bvSext' - -- * Conversions to Integer - , bvIntegerU - , bvIntegerS - -- * Byte decomposition - , bvGetBytesU + , concat + , select, select' + , zext + , sext + , trunc, trunc' + , mulWide + -- * Enum operations + , succUnsigned, succSigned + , predUnsigned, predSigned + , enumFromToUnsigned, enumFromToSigned + -- * Pretty printing + , ppHex + , ppBin + , ppOct + , ppDec ) where -import Data.BitVector.Sized.Internal +import Data.BitVector.Sized.Internal hiding (BV(..)) +import qualified Data.BitVector.Sized.Internal as BV + +import Data.Parameterized.NatRepr (knownNat, NatRepr) +import Prelude (Integer) + +-- | Get the underlying 'Integer' representation from a 'BV'. We +-- guarantee that @(\\(BV.BV x) -> x) == BV.toUnsigned@. +pattern BV :: Integer -> BV.BV w +pattern BV x <- BV.BV x +{-# COMPLETE BV #-} diff --git a/src/Data/BitVector/Sized/App.hs b/src/Data/BitVector/Sized/App.hs deleted file mode 100644 --- a/src/Data/BitVector/Sized/App.hs +++ /dev/null @@ -1,369 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE Rank2Types #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeOperators #-} - -{-| -Module : Data.BitVector.Sized.App -Copyright : (c) Galois Inc. 2018 -License : BSD-3 -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 - , bvAppWidth - -- * Smart constructors - , BVExpr(..) - -- ** Bitwise - , andE - , orE - , xorE - , notE - -- ** Arithmetic - , addE - , subE - , mulE - , quotuE - , quotsE - , remuE - , remsE - , negateE - , absE - , signumE - , sllE - , srlE - , sraE - -- ** Comparison - , eqE - , ltuE - , ltsE - -- ** Width-changing - , zextE, zextE' - , sextE, sextE' - , extractE, extractE' - , concatE - -- ** Control - , iteE - ) where - -import Control.Monad.Identity -import Data.BitVector.Sized --- import Data.Bits -import Data.Parameterized -import Data.Parameterized.TH.GADT -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 - - -- Bitwise operations - AndApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - OrApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - XorApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - NotApp :: !(NatRepr w) -> !(expr w) -> BVApp expr w - - -- Shifts - SllApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - SrlApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - SraApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - - -- Arithmetic operations - AddApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - SubApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - MulApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - QuotUApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - QuotSApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - RemUApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - RemSApp :: !(NatRepr w) -> !(expr w) -> !(expr w) -> BVApp expr w - NegateApp :: !(NatRepr w) -> !(expr w) -> BVApp expr w - AbsApp :: !(NatRepr w) -> !(expr w) -> BVApp expr w - SignumApp :: !(NatRepr 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' -> NatRepr ix -> !(expr w) -> BVApp expr w' - ConcatApp :: !(NatRepr (w+w')) -> !(expr w) -> !(expr w') -> BVApp expr (w+w') - - -- Other operations - IteApp :: !(NatRepr w) -> !(expr 1) -> !(expr w) -> !(expr w) -> BVApp expr w - -bvAppWidth :: BVApp expr w -> NatRepr w -bvAppWidth (AndApp wRepr _ _) = wRepr -bvAppWidth (OrApp wRepr _ _) = wRepr -bvAppWidth (XorApp wRepr _ _) = wRepr -bvAppWidth (NotApp wRepr _) = wRepr - -bvAppWidth (SllApp wRepr _ _) = wRepr -bvAppWidth (SrlApp wRepr _ _) = wRepr -bvAppWidth (SraApp wRepr _ _) = wRepr - -bvAppWidth (AddApp wRepr _ _) = wRepr -bvAppWidth (SubApp wRepr _ _) = wRepr -bvAppWidth (MulApp wRepr _ _) = wRepr -bvAppWidth (QuotUApp wRepr _ _) = wRepr -bvAppWidth (QuotSApp wRepr _ _) = wRepr -bvAppWidth (RemUApp wRepr _ _) = wRepr -bvAppWidth (RemSApp wRepr _ _) = wRepr -bvAppWidth (NegateApp wRepr _) = wRepr -bvAppWidth (AbsApp wRepr _) = wRepr -bvAppWidth (SignumApp wRepr _) = wRepr - -bvAppWidth (EqApp _ _) = knownNat -bvAppWidth (LtuApp _ _) = knownNat -bvAppWidth (LtsApp _ _) = knownNat - -bvAppWidth (ZExtApp wRepr _) = wRepr -bvAppWidth (SExtApp wRepr _) = wRepr -bvAppWidth (ExtractApp wRepr _ _) = wRepr -bvAppWidth (ConcatApp wRepr _ _) = wRepr - -bvAppWidth (IteApp wRepr _ _ _) = wRepr - -$(return []) - -instance TestEquality expr => TestEquality (BVApp expr) where - testEquality = $(structuralTypeEquality [t|BVApp|] - [ (AnyType `TypeApp` AnyType, [|testEquality|]) ]) - -instance TestEquality expr => Eq (BVApp expr w) where - (==) = \x y -> isJust (testEquality x y) - -instance TestEquality expr => EqF (BVApp expr) where - eqF = (==) - -instance OrdF expr => OrdF (BVApp expr) where - compareF = $(structuralTypeOrd [t|BVApp|] - [ (AnyType `TypeApp` AnyType, [|compareF|]) ]) - -instance OrdF expr => Ord (BVApp expr w) where - compare a b = - case compareF a b of - LTF -> LT - EQF -> EQ - GTF -> GT - -instance FunctorFC BVApp where - fmapFC = fmapFCDefault - -instance FoldableFC BVApp where - foldMapFC = foldMapFCDefault - -instance TraversableFC BVApp where - traverseFC = $(structuralTraversal [t|BVApp|] []) - --- | 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 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 (MulApp _ e1 e2) = bvMul <$> eval e1 <*> eval e2 -evalBVAppM eval (QuotSApp _ e1 e2) = bvQuotS <$> eval e1 <*> eval e2 -evalBVAppM eval (QuotUApp _ 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 (NegateApp _ e) = bvNegate <$> eval e -evalBVAppM eval (AbsApp _ e) = bvAbs <$> eval e -evalBVAppM eval (SignumApp _ e) = bvSignum <$> eval e -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) = bvZext' wRepr <$> eval e -evalBVAppM eval (SExtApp wRepr e) = bvSext' wRepr <$> eval e -evalBVAppM eval (ExtractApp wRepr ixRepr e) = - bvExtract' wRepr (fromIntegral $ intValue ixRepr) <$> 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 - case testVal of - 1 -> eval eT - _ -> eval eF - --- | 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 - --- | Typeclass for embedding 'BVApp' constructors into larger expression types. -class BVExpr (expr :: Nat -> *) where - litBV :: BitVector w -> expr w - exprWidth :: expr w -> NatRepr w - appExpr :: BVApp expr w -> expr w - --- -- TODO: finish --- instance (BVExpr expr) => Num (BVApp expr w) where --- app1 + app2 = AddApp (appExpr app1) (appExpr app2) --- app1 * app2 = MulApp (appExpr app1) (appExpr app2) --- abs app = AbsApp (appExpr app) --- signum app = SignumApp (appExpr app) --- fromInteger = undefined --- negate app = NegateApp (appExpr app) --- app1 - app2 = SubApp (appExpr app1) (appExpr app2) - --- -- TODO: finish --- instance (KnownNat w, BVExpr expr, TestEquality expr) => Bits (BVApp expr w) where --- app1 .&. app2 = AndApp (appExpr app1) (appExpr app2) --- app1 .|. app2 = OrApp (appExpr app1) (appExpr app2) --- app1 `xor` app2 = XorApp (appExpr app1) (appExpr app2) --- complement app = NotApp (appExpr app) --- shiftL = undefined --- shiftR = undefined --- rotate = undefined --- bitSize = undefined --- bitSizeMaybe = undefined --- isSigned = undefined --- testBit = undefined --- bit = undefined --- popCount = undefined - --- | Bitwise and. -andE :: BVExpr expr => expr w -> expr w -> expr w -andE e1 e2 = appExpr (AndApp (exprWidth e1) e1 e2) - --- | Bitwise or. -orE :: BVExpr expr => expr w -> expr w -> expr w -orE e1 e2 = appExpr (OrApp (exprWidth e1) e1 e2) - --- | Bitwise xor. -xorE :: BVExpr expr => expr w -> expr w -> expr w -xorE e1 e2 = appExpr (XorApp (exprWidth e1) e1 e2) - --- | Bitwise not. -notE :: BVExpr expr => expr w -> expr w -notE e = appExpr (NotApp (exprWidth e) e) - --- | Add two expressions. -addE :: BVExpr expr => expr w -> expr w -> expr w -addE e1 e2 = appExpr (AddApp (exprWidth e1) e1 e2) - --- | Subtract the second expression from the first. -subE :: BVExpr expr => expr w -> expr w -> expr w -subE e1 e2 = appExpr (SubApp (exprWidth e1) e1 e2) - --- | Signed multiply two 'BitVector's, doubling the width of the result to hold all --- arithmetic overflow bits. -mulE :: BVExpr expr => expr w -> expr w -> expr w -mulE e1 e2 = appExpr (MulApp (exprWidth e1) e1 e2) - --- | Signed divide two 'BitVector's, rounding to zero. -quotsE :: BVExpr expr => expr w -> expr w -> expr w -quotsE e1 e2 = appExpr (QuotSApp (exprWidth e1) e1 e2) - --- | Unsigned divide two 'BitVector's, rounding to zero. -quotuE :: BVExpr expr => expr w -> expr w -> expr w -quotuE e1 e2 = appExpr (QuotUApp (exprWidth e1) e1 e2) - --- | Remainder after signed division of two 'BitVector's, when rounded to zero. -remsE :: BVExpr expr => expr w -> expr w -> expr w -remsE e1 e2 = appExpr (RemSApp (exprWidth e1) e1 e2) - --- | Remainder after unsigned division of two 'BitVector's, when rounded to zero. -remuE :: BVExpr expr => expr w -> expr w -> expr w -remuE e1 e2 = appExpr (RemUApp (exprWidth e1) e1 e2) - -negateE :: BVExpr expr => expr w -> expr w -negateE e = appExpr (NegateApp (exprWidth e) e) - -absE :: BVExpr expr => expr w -> expr w -absE e = appExpr (AbsApp (exprWidth e) e) - -signumE :: BVExpr expr => expr w -> expr w -signumE e = appExpr (SignumApp (exprWidth e) e) - --- | Left logical shift the first expression by the second. -sllE :: BVExpr expr => expr w -> expr w -> expr w -sllE e1 e2 = appExpr (SllApp (exprWidth e1) e1 e2) - --- | Left logical shift the first expression by the second. -srlE :: BVExpr expr => expr w -> expr w -> expr w -srlE e1 e2 = appExpr (SrlApp (exprWidth e1) e1 e2) - --- | Left logical shift the first expression by the second. -sraE :: BVExpr expr => expr w -> expr w -> expr w -sraE e1 e2 = appExpr (SraApp (exprWidth e1) e1 e2) - --- | Test for equality of two expressions. -eqE :: BVExpr expr => expr w -> expr w -> expr 1 -eqE e1 e2 = appExpr (EqApp e1 e2) - --- | Signed less than -ltsE :: BVExpr expr => expr w -> expr w -> expr 1 -ltsE e1 e2 = appExpr (LtsApp e1 e2) - --- | Unsigned less than -ltuE :: BVExpr expr => expr w -> expr w -> expr 1 -ltuE e1 e2 = appExpr (LtuApp e1 e2) - --- | Zero-extension -zextE :: (BVExpr expr, KnownNat w') => expr w -> expr w' -zextE e = appExpr (ZExtApp knownNat e) - --- | Zero-extension with an explicit width argument -zextE' :: BVExpr expr => NatRepr w' -> expr w -> expr w' -zextE' repr e = appExpr (ZExtApp repr e) - --- | Sign-extension -sextE :: (BVExpr expr, KnownNat w') => expr w -> expr w' -sextE e = appExpr (SExtApp knownNat e) - --- | Sign-extension with an explicit width argument -sextE' :: BVExpr expr => NatRepr w' -> expr w -> expr w' -sextE' repr e = appExpr (SExtApp repr e) - --- | Extract bits -extractE :: (BVExpr expr, KnownNat w') => NatRepr ix -> expr w -> expr w' -extractE ixRepr e = appExpr (ExtractApp knownNat ixRepr e) - --- | Extract bits with an explicit width argument -extractE' :: BVExpr expr => NatRepr w' -> NatRepr ix -> expr w -> expr w' -extractE' wRepr ixRepr e = appExpr (ExtractApp wRepr ixRepr e) - --- | Concatenation -concatE :: BVExpr expr => expr w -> expr w' -> expr (w+w') -concatE e1 e2 = appExpr (ConcatApp (exprWidth e1 `addNat` exprWidth e2) e1 e2) - --- | Conditional branch. -iteE :: BVExpr expr => expr 1 -> expr w -> expr w -> expr w -iteE t e1 e2 = appExpr (IteApp (exprWidth e1) t e1 e2) diff --git a/src/Data/BitVector/Sized/BitLayout.hs b/src/Data/BitVector/Sized/BitLayout.hs deleted file mode 100644 --- a/src/Data/BitVector/Sized/BitLayout.hs +++ /dev/null @@ -1,283 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeOperators #-} - -{-| -Module : Data.BitVector.Sized.BitLayout -Copyright : (c) Galois Inc. 2018 -License : BSD-3 -Maintainer : benselfridge@galois.com -Stability : experimental -Portability : portable - -This module defines a 'BitLayout' datatype which encodes a chunk-to-chunk mapping (no -overlaps) from a smaller bit vector into a larger one. 'BitLayout's are especially -useful for defining the encoding and decoding of opcodes/operands in an instruction. --} - -module Data.BitVector.Sized.BitLayout - ( -- * Chunk - Chunk(..) - , chunk - -- * BitLayout - , BitLayout - , empty, singleChunk, (<:) - , inject - , extract - -- * Lenses - , layoutLens, layoutsLens - -- * Utilities - , bitLayoutAssignmentList - ) where - -import Data.BitVector.Sized.Internal -import Data.Foldable -import qualified Data.Functor.Product as P -import Control.Lens (lens, Simple, Lens) -import Data.Parameterized -import Data.Parameterized.List -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 --- 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, --- preserving the order of the input bits. So an 5-bit input like @10011@ would map --- to some larger bit vector containing the input starting at position 2, like --- @000001001100@. --- --- Multiple 'Chunk's comprise a 'BitLayout'; see below. -data Chunk (w :: Nat) :: * where - Chunk :: NatRepr w -- width of range - -> Int -- index of range start - -> Chunk w - --- | Construct a 'Chunk' in a context where the chunk width is known at compile time. -chunk :: KnownNat w => Int -> Chunk w -chunk = Chunk knownNat - -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@. --- --- To construct a 'BitLayout', use the 'empty' constructor and the '<:' operator, --- 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 --- BitLayout 32 12 (fromList [Chunk 5 7,Chunk 7 25]) --- >>> :type it --- it :: BitLayout 32 12 --- --- In the above example @bitLayout@ defines a chunk-by-chunk mapping from a bit --- vector of width 12 to one of width 32. We imagine the input vector of width 12 --- listed like so: --- --- @ --- 0bAXXXXXBCXXXD --- |-----||---| --- 7 5 --- @ --- --- Here, bits @A@, @B@, @C@, and @D@ are just labeled as such to illustrate their --- place after the mapping. The @BitLayout 32 12@ defined above as the @layout@ --- variable would map that 12-bit vector to the following 32-bit vector: --- --- @ --- (Bit 25) (Bit 5) --- | | --- | | --- v v --- 0bAXXXXXB0000000000000CXXXD0000000 --- |-----| |---| --- 7 5 --- @ --- --- To use a 'BitLayout' to achieve a bidirectional mapping like the one described --- above, you can either use the 'Lens' interface or the functions 'inject' and --- 'extract', which give an explicit setter and getter, respectively. --- --- Example use of @inject@/@extract@: --- --- >>> let bl = (chunk 25 :: Chunk 7) <: (chunk 7 :: Chunk 5) <: (empty :: BitLayout 32 0) --- >>> let sVec = bitVector 0b111111100001 :: BitVector 12 --- >>> sVec --- 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 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 - --- | Construct a 'BitLayout' with one chunk. -singleChunk :: (KnownNat w, KnownNat w') => Int -> BitLayout w w' -singleChunk idx = chunk idx <: empty - --- TODO: Should this be in Maybe? --- | Add a 'Chunk' to a 'BitLayout'. If the 'Chunk' does not fit, either because the --- resulting 'BitLayout' would be too long or because it would overlap with a 'Chunk' --- that is already in the 'BitLayout', we throw an error. -(<:) :: Chunk r -- ^ chunk to add - -> BitLayout t s -- ^ layout we are adding the chunk to - -> BitLayout t (r + s) -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 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 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 chk (toList chunks) - -noOverlaps :: Chunk r -> [Some Chunk] -> Bool -noOverlaps chk = all (chunksDontOverlap (Some chk)) - -chunksDontOverlap :: Some Chunk -> Some Chunk -> Bool -chunksDontOverlap (Some (Chunk chunkRepr1 start1)) (Some (Chunk chunkRepr2 start2)) = - if start1 <= start2 - then start1 + chunkWidth1 <= start2 - else start2 + chunkWidth2 <= start1 - where chunkWidth1 = fromIntegral (natValue chunkRepr1) - chunkWidth2 = fromIntegral (natValue chunkRepr2) - --- | Given a starting position, insert (via "or") a smaller 'BitVector' @s@ with a larger --- 'BitVector' @t@ at that position. -bvOrAt :: Int - -> BitVector s - -> BitVector t - -> BitVector t -bvOrAt start sVec tVec@(BitVector tRepr _) = - (bvZext' tRepr sVec `bvShift` start) `bvOr` tVec - --- | Given a list of 'Chunk's, inject each chunk from a source 'BitVector' @s@ into a --- target 'BitVector' @t@. -bvOrAtAll :: NatRepr t - -> [Some Chunk] - -> BitVector s - -> BitVector t -bvOrAtAll tRepr [] _ = BV tRepr 0 -bvOrAtAll tRepr (Some (Chunk chunkRepr chunkStart) : chunks) sVec = - bvOrAt chunkStart (bvTruncBits sVec chunkWidth) (bvOrAtAll tRepr chunks (sVec `bvShift` (- chunkWidth))) - where chunkWidth = fromIntegral (natValue chunkRepr) - --- | Use a 'BitLayout' to inject a smaller vector into a larger one. -inject :: BitLayout t s -- ^ The layout - -> BitVector t -- ^ The larger vector to inject into - -> BitVector s -- ^ The smaller vector to be injected - -> BitVector t -inject (BitLayout tRepr _ chunks) tVec sVec = - 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 --- BitVector s, and shiftinto the starting position. -extractChunk :: NatRepr s -- ^ width of output - -> Int -- ^ where to place the chunk in the result - -> Some Chunk -- ^ location/width of chunk in the input - -> BitVector t -- ^ input vector - -> BitVector s -extractChunk sRepr sStart (Some (Chunk chunkRepr chunkStart)) tVec = - bvShift extractedChunk sStart - where extractedChunk = bvZext' sRepr (bvExtract' chunkRepr chunkStart tVec) - -extractAll :: NatRepr s -- ^ determines width of output vector - -> Int -- ^ current position in output vector - -> [Some Chunk] -- ^ list of remaining chunks to place in output vector - -> BitVector t -- ^ input vector - -> BitVector s -extractAll sRepr _ [] _ = BV sRepr 0 -extractAll sRepr outStart (chk@(Some (Chunk chunkRepr _)) : chunks) tVec = - extractChunk sRepr outStart chk tVec `bvOr` - extractAll sRepr (outStart + chunkWidth) chunks tVec - where chunkWidth = fromInteger (intValue chunkRepr) - --- | Use a 'BitLayout' to extract a smaller vector from a larger one. -extract :: BitLayout t s -- ^ The layout - -> BitVector t -- ^ The larger vector to extract from - -> BitVector s -extract (BitLayout _ sRepr chunks) = extractAll sRepr 0 (toList chunks) - --- | Lens for a 'BitLayout'. -layoutLens :: BitLayout t s -> Simple Lens (BitVector t) (BitVector s) -layoutLens layout = lens (extract layout) (inject layout) - --- | Lens for a parameterized 'List' of 'BitLayout's. -layoutsLens :: forall ws . List (BitLayout 32) ws -> Simple Lens (BitVector 32) (List BitVector ws) -layoutsLens layouts = lens - (\bv -> imap (const $ flip extract bv) layouts) - (\bv bvFlds -> ifoldr (\_ (P.Pair fld layout) bv' -> inject layout bv' fld) - bv - (izipWith (const P.Pair) bvFlds layouts)) - --- | From a `BitLayout`, get a list representing the position of each bit from the --- source to the target. The list --- --- @ --- [3,4,5,10,11,12,13] --- @ --- --- means that bit 0 of the source is placed in bit 3 of the target, bit 1 of the --- source is placed in bit 4 of the target, etc. - -bitLayoutAssignmentList :: BitLayout t s -> [Int] -bitLayoutAssignmentList (BitLayout _ _ someChunks) = reverse (bitLayoutAssignmentList' (toList someChunks)) - -bitLayoutAssignmentList' :: [Some Chunk] -> [Int] -bitLayoutAssignmentList' [] = [] -bitLayoutAssignmentList' (Some (Chunk wRepr start):rst) = - reverse [start..start+w-1] ++ bitLayoutAssignmentList' rst - where w = fromIntegral (natValue wRepr) diff --git a/src/Data/BitVector/Sized/Internal.hs b/src/Data/BitVector/Sized/Internal.hs --- a/src/Data/BitVector/Sized/Internal.hs +++ b/src/Data/BitVector/Sized/Internal.hs @@ -1,420 +1,922 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeOperators #-} - -{-| -Module : Data.BitVector.Sized -Copyright : (c) Galois Inc. 2018 -License : BSD-3 -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. --} - -module Data.BitVector.Sized.Internal where - -import Data.Bits -import Data.Ix -import Data.Parameterized -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 - --- | BitVector datatype, parameterized by width. -data BitVector (w :: Nat) :: * where - BV :: NatRepr w -> Integer -> BitVector w - --- | 'BitVector' can be treated as a constructor for pattern matching, but to build --- one you must use the smart constructor `bitVector`. -pattern BitVector :: NatRepr w -> Integer -> BitVector w -pattern BitVector wRepr x <- BV wRepr x -{-# COMPLETE BitVector #-} - --- | Construct a bit vector with a particular width, where the width is inferrable --- from the type context. The 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 --- >>> bitVector 0xA :: BitVector 2 --- 0x2 -bitVector :: (Integral a, KnownNat w) => a -> BitVector w -bitVector x = bitVector' knownNat x - --- | Like 'bitVector', but with an explict 'NatRepr'. -bitVector' :: Integral a => NatRepr w -> a -> BitVector w -bitVector' wRepr x = BV wRepr (truncBits width (fromIntegral x)) - where width = natValue wRepr - --- | The zero bitvector with width 0. -bv0 :: BitVector 0 -bv0 = bitVector (0 :: Integer) - ----------------------------------------- --- 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 bv = if bvTestBit bv (width - 1) - then bvIntegerU bv - (1 `shiftL` width) - else bvIntegerU bv - where width = bvWidth bv - ----------------------------------------- --- 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. Uses an arithmetic right shift. -bvShift :: BitVector w -> Int -> BitVector w -bvShift bv@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` shf)) - where width = natValue wRepr - x = bvIntegerS bv -- arithmetic right shift when negative - -toPos :: Int -> Int -toPos x | x < 0 = 0 -toPos x = x - --- | Left shift. -bvShiftL :: BitVector w -> Int -> BitVector w -bvShiftL bv shf = bvShift bv (toPos shf) - --- | Right arithmetic shift. -bvShiftRA :: BitVector w -> Int -> BitVector w -bvShiftRA bv shf = bvShift bv (- (toPos shf)) - --- | Right logical shift. -bvShiftRL :: BitVector w -> Int -> BitVector w -bvShiftRL bv@(BV wRepr _) shf = BV wRepr (truncBits width (x `shift` (- toPos shf))) - where width = natValue wRepr - x = bvIntegerU bv - --- | Bitwise rotate. -bvRotate :: BitVector w -> Int -> BitVector w -bvRotate bv rot' = leftChunk `bvOr` rightChunk - where rot = rot' `mod` bvWidth bv - leftChunk = bvShift bv rot - rightChunk = bvShift bv (rot - bvWidth bv) - --- | 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 division (unsigned). Rounds to zero. -bvQuotU :: BitVector w -> BitVector w -> BitVector w -bvQuotU (BV wRepr x) (BV _ y) = BV wRepr (x `quot` y) - --- | Bitwise division (signed). Rounds to zero (not negative infinity). -bvQuotS :: BitVector w -> BitVector w -> BitVector w -bvQuotS bv1@(BV wRepr _) bv2 = BV wRepr (truncBits width (x `quot` y)) - where x = bvIntegerS bv1 - y = bvIntegerS bv2 - width = natValue wRepr - --- | Bitwise remainder after division (unsigned), when rounded to zero. -bvRemU :: BitVector w -> BitVector w -> BitVector w -bvRemU (BV wRepr x) (BV _ y) = BV wRepr (x `rem` y) - --- | Bitwise remainder after division (signed), when rounded to zero (not negative --- infinity). -bvRemS :: BitVector w -> BitVector w -> BitVector w -bvRemS bv1@(BV wRepr _) bv2 = BV wRepr (truncBits width (x `rem` 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 - where width = natValue wRepr - x = bvIntegerS bv - 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 bv@(BV wRepr _) = bvShift bv (1 - width) `bvAnd` BV wRepr 0x1 - where width = fromIntegral (natValue wRepr) - --- | Signed less than. -bvLTS :: BitVector w -> BitVector w -> Bool -bvLTS bv1 bv2 = bvIntegerS bv1 < bvIntegerS bv2 - --- | Unsigned less than. -bvLTU :: BitVector w -> BitVector w -> Bool -bvLTU bv1 bv2 = bvIntegerU bv1 < bvIntegerU bv2 - ----------------------------------------- --- Width-changing operations - --- | Concatenate two bit vectors. --- --- >>> (0xAA :: BitVector 8) `bvConcat` (0xBCDEF0 :: BitVector 24) --- 0xaabcdef0 --- >>> :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 - -bvConcatSome :: Some BitVector -> Some BitVector -> Some BitVector -bvConcatSome (Some bv1) (Some bv2) = Some (bv2 <:> bv1) - --- | Concatenate a list of 'BitVector's into a 'BitVector' of arbitrary width. The ordering is little endian: --- --- >>> bvConcatMany [0xAA :: BitVector 8, 0xBB] :: BitVector 16 --- 0xbbaa --- >>> bvConcatMany [0xAA :: BitVector 8, 0xBB, 0xCC] :: BitVector 16 --- 0xbbaa --- --- If the sum of the widths of the input 'BitVector's exceeds the output width, we --- ignore the tail end of the list. -bvConcatMany :: KnownNat w' => [BitVector w] -> BitVector w' -bvConcatMany = bvConcatMany' knownNat - --- | 'bvConcatMany' with an explicit 'NatRepr'. -bvConcatMany' :: NatRepr w' -> [BitVector w] -> BitVector w' -bvConcatMany' wRepr bvs = - viewSome (bvZext' wRepr) $ foldl bvConcatSome (Some bv0) (Some <$> bvs) - -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 (0xAABCDEF0 :: BitVector 32) :: BitVector 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. -bvExtract :: forall w w' . (KnownNat w') - => Int - -> BitVector w - -> BitVector w' -bvExtract pos bv = bitVector xShf - where (BV _ xShf) = bvShift bv (- pos) - --- | Unconstrained variant of 'bvExtract' with an explicit 'NatRepr' argument. -bvExtract' :: NatRepr w' - -> Int - -> BitVector w - -> BitVector w' -bvExtract' repr pos bv = BV repr (truncBits width xShf) - where (BV _ xShf) = bvShift bv (- 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) = bitVector x - --- | Unconstrained variant of 'bvZext' with an explicit 'NatRepr' argument. -bvZext' :: NatRepr w' - -> BitVector w - -> BitVector w' -bvZext' 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 bv = bitVector (bvIntegerS bv) - --- | Unconstrained variant of 'bvSext' with an explicit 'NatRepr' argument. -bvSext' :: NatRepr w' - -> BitVector w - -> BitVector w' -bvSext' repr bv = BV repr (truncBits width (bvIntegerS bv)) - where width = natValue repr - ----------------------------------------- --- Byte decomposition - --- | Given a 'BitVector' of arbitrary length, decompose it into a list of bytes. Uses --- an unsigned interpretation of the input vector, so if you ask for more bytes that --- the 'BitVector' contains, you get zeros. The result is little-endian, so the first --- element of the list will be the least significant byte of the input vector. -bvGetBytesU :: Int -> BitVector w -> [BitVector 8] -bvGetBytesU n _ | n <= 0 = [] -bvGetBytesU n bv = bvExtract 0 bv : bvGetBytesU (n-1) (bvShiftRL bv 8) - ----------------------------------------- --- 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 - ----------------------------------------- --- Class instances -$(return []) - -instance Show (BitVector w) where - 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 - (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 OrdF BitVector where - (BV xRepr x) `compareF` (BV yRepr y) = - case xRepr `compareF` yRepr of - EQF -> fromOrdering (x `compare` y) - cmp -> cmp - -instance TestEquality BitVector where - testEquality (BV wRepr x) (BV wRepr' y) = - if natValue wRepr == natValue wRepr' && x == y - then Just (unsafeCoerce (Refl :: a :~: a)) - else 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 = bitVector . (bit :: Int -> Integer) - 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 = bitVector - negate = bvNegate - -instance KnownNat w => Enum (BitVector w) where - toEnum = bitVector - fromEnum = fromIntegral . bvIntegerU - -instance KnownNat w => Ix (BitVector w) where - range (lo, hi) = bitVector <$> [bvIntegerU lo .. bvIntegerU hi] - index (lo, hi) bv = index (bvIntegerU lo, bvIntegerU hi) (bvIntegerU bv) - inRange (lo, hi) bv = inRange (bvIntegerU lo, bvIntegerU hi) (bvIntegerU bv) - -instance KnownNat w => Bounded (BitVector w) where - minBound = bitVector (0 :: Integer) - maxBound = bitVector ((-1) :: Integer) - -instance KnownNat w => Arbitrary (BitVector w) where - arbitrary = choose (minBound, maxBound) - -instance KnownNat w => Random (BitVector w) where - randomR (bvLo, bvHi) gen = - let (x, gen') = randomR (bvIntegerU bvLo, bvIntegerU bvHi) gen - in (bitVector x, gen') - random gen = - let (x :: Integer, gen') = random gen - in (bitVector x, gen') - -prettyHex :: (Integral a, PrintfArg a, Show a) => a -> Integer -> String -prettyHex width val = printf format val width - where -- numDigits = (width+3) `quot` 4 - -- format = "0x%." ++ show numDigits ++ "x<%d>" - format = "0x%x<%d>" - -instance Pretty (BitVector w) where - -- | Pretty print a bit vector (shows its width) - pPrint (BV wRepr x) = text $ prettyHex (natValue wRepr) x +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveLift #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +{-| +Module : Data.BitVector.Sized.Internal +Copyright : (c) Galois Inc. 2018 +License : BSD-3 +Maintainer : benselfridge@galois.com +Stability : experimental +Portability : portable + +Internal hidden module containing all definitions for the 'BV' type. +-} + +module Data.BitVector.Sized.Internal where + +import Data.BitVector.Sized.Panic (panic) + +-- Qualified imports +import qualified Data.Bits as B +import qualified Data.Bits.Bitwise as B +import qualified Data.ByteString as BS +import qualified Numeric as N +import qualified Data.Parameterized.NatRepr as P +import qualified Prelude as Prelude + +-- Unqualified imports +import Data.Char (intToDigit) +import Data.List (genericLength) +import Data.Int +import Data.Kind (Type) +import Data.Maybe (fromJust) +import Data.Word +import Data.Parameterized ( NatRepr + , mkNatRepr + , natValue + , intValue + , addNat + , ShowF + , EqF(..) + , Hashable(..) + , Some(..) + , Pair(..) + ) +import GHC.Generics +import GHC.TypeLits +import Language.Haskell.TH.Lift (Lift) +import Numeric.Natural +import Prelude hiding (abs, or, and, negate, concat, signum) + +---------------------------------------- +-- Utility functions + +-- | Check that a 'NatRepr' is representable as an 'Int'. +checkNatRepr :: NatRepr w -> a -> a +checkNatRepr = checkNatural . natValue + +-- | Check that a 'Natural' is representable as an 'Int'. +checkNatural :: Natural -> a -> a +checkNatural n a = if n > (fromIntegral (maxBound :: Int) :: Natural) + then panic "Data.BitVector.Sized.Internal.checkNatural" + [show n ++ " not representable as Int"] + else a + + +-- | Unsafe coercion from @Natural@ to @Int@. We mostly use this to +-- interact with operations from "Data.Bits". This should only be +-- called when we already know the input @Natural@ is small enough, +-- e.g., because we previously called @checkNatural@. +fromNatural :: Natural -> Int +fromNatural = fromIntegral + +---------------------------------------- +-- BitVector data type definitions + +-- | Bitvector datatype, parameterized by width. +data BV (w :: Nat) :: Type where + -- | We store the value as an 'Integer' rather than a 'Natural', + -- since many of the operations on bitvectors rely on a two's + -- complement representation. However, an invariant on the value is + -- that it must always be positive. + -- + -- Secondly, we maintain the invariant that any constructed BV value + -- has a width whose value is representable in a Haskell @Int@. + BV :: Integer -> BV w + + deriving (Generic, Show, Read, Eq, Ord, Lift) + +instance ShowF BV + +instance EqF BV where + BV bv `eqF` BV bv' = bv == bv' + +instance Hashable (BV w) where + hashWithSalt salt (BV i) = hashWithSalt salt i + +---------------------------------------- +-- BV construction +-- | Internal function for masking the input integer *without* +-- checking that the width is representable as an 'Int'. We use this +-- instead of 'mkBV' whenever we already have some guarantee that the +-- width is legal. +mkBV' :: NatRepr w -> Integer -> BV w +mkBV' w x = BV (P.toUnsigned w x) + +-- | Construct a bitvector with a particular width, where the width is +-- provided as an explicit `NatRepr` argument. The input 'Integer', +-- whether positive or negative, is silently truncated to fit into the +-- number of bits demanded by the return type. The width cannot be +-- arbitrarily large; it must be representable as an 'Int'. +-- +-- >>> mkBV (knownNat @4) 10 +-- BV 10 +-- >>> mkBV (knownNat @2) 10 +-- BV 2 +-- >>> mkBV (knownNat @4) (-2) +-- BV 14 +mkBV :: NatRepr w + -- ^ Desired bitvector width + -> Integer + -- ^ Integer value to truncate to bitvector width + -> BV w +mkBV w x = checkNatRepr w $ mkBV' w x + +-- | Return 'Nothing' if the unsigned 'Integer' does not fit in the +-- required number of bits, otherwise return the input. +checkUnsigned :: NatRepr w + -> Integer + -> Maybe Integer +checkUnsigned w i = if i < 0 || i > P.maxUnsigned w + then Nothing + else Just i + +-- | Like 'mkBV', but returns 'Nothing' if unsigned input integer cannot be +-- represented in @w@ bits. +mkBVUnsigned :: NatRepr w + -- ^ Desired bitvector width + -> Integer + -- ^ Integer value + -> Maybe (BV w) +mkBVUnsigned w x = checkNatRepr w $ BV <$> checkUnsigned w x + +-- | Return 'Nothing if the signed 'Integer' does not fit in the +-- required number of bits, otherwise return an unsigned positive +-- integer that fits in @w@ bits. +signedToUnsigned :: 1 <= w => NatRepr w + -- ^ Width of output + -> Integer + -> Maybe Integer +signedToUnsigned w i = if i < P.minSigned w || i > P.maxSigned w + then Nothing + else Just $ if i < 0 then i + P.maxUnsigned w + 1 else i + +-- | Like 'mkBV', but returns 'Nothing' if signed input integer cannot +-- be represented in @w@ bits. +mkBVSigned :: 1 <= w => NatRepr w + -- ^ Desired bitvector width + -> Integer + -- ^ Integer value + -> Maybe (BV w) +mkBVSigned w x = checkNatRepr w $ BV <$> signedToUnsigned w x + +-- | The minimum unsigned value for bitvector with given width (always 0). +minUnsigned :: NatRepr w -> BV w +minUnsigned w = checkNatRepr w $ BV 0 + +-- | The maximum unsigned value for bitvector with given width. +maxUnsigned :: NatRepr w -> BV w +maxUnsigned w = checkNatRepr w $ BV (P.maxUnsigned w) + +-- | The minimum value for bitvector in two's complement with given width. +minSigned :: 1 <= w => NatRepr w -> BV w +minSigned w = mkBV w (P.minSigned w) + +-- | The maximum value for bitvector in two's complement with given width. +maxSigned :: 1 <= w => NatRepr w -> BV w +maxSigned w = checkNatRepr w $ BV (P.maxSigned w) + +-- | @unsignedClamp w i@ rounds @i@ to the nearest value between @0@ +-- and @2^w - 1@ (inclusive). +unsignedClamp :: NatRepr w -> Integer -> BV w +unsignedClamp w x = checkNatRepr w $ + if | x < P.minUnsigned w -> BV (P.minUnsigned w) + | x > P.maxUnsigned w -> BV (P.maxUnsigned w) + | otherwise -> BV x + +-- | @signedClamp w i@ rounds @i@ to the nearest value between +-- @-2^(w-1)@ and @2^(w-1) - 1@ (inclusive). +signedClamp :: 1 <= w => NatRepr w -> Integer -> BV w +signedClamp w x = checkNatRepr w $ + if | x < P.minSigned w -> BV (P.minSigned w) + | x > P.maxSigned w -> BV (P.maxSigned w) + | otherwise -> BV x + +---------------------------------------- +-- Construction from fixed-width data types + +-- | Construct a 'BV' from a 'Bool'. +bool :: Bool -> BV 1 +bool True = BV 1 +bool False = BV 0 + +-- | Construct a 'BV' from a 'Word8'. +word8 :: Word8 -> BV 8 +word8 = BV . toInteger + +-- | Construct a 'BV' from a 'Word16'. +word16 :: Word16 -> BV 16 +word16 = BV . toInteger + +-- | Construct a 'BV' from a 'Word32'. +word32 :: Word32 -> BV 32 +word32 = BV . toInteger + +-- | Construct a 'BV' from a 'Word64'. +word64 :: Word64 -> BV 64 +word64 = BV . toInteger + +-- | Construct a 'BV' from an 'Int8'. +int8 :: Int8 -> BV 8 +int8 = word8 . (fromIntegral :: Int8 -> Word8) + +-- | Construct a 'BV' from an 'Int16'. +int16 :: Int16 -> BV 16 +int16 = word16 . (fromIntegral :: Int16 -> Word16) + +-- | Construct a 'BV' from an 'Int32'. +int32 :: Int32 -> BV 32 +int32 = word32 . (fromIntegral :: Int32 -> Word32) + +-- | Construct a 'BV' from an 'Int64'. +int64 :: Int64 -> BV 64 +int64 = word64 . (fromIntegral :: Int64 -> Word64) + +-- | Construct a 'BV' from a list of bits, in big endian order (bits +-- with lower value index in the list are mapped to higher order bits +-- in the output bitvector). Return the resulting 'BV' along with its +-- width. +-- +-- >>> case bitsBE [True, False] of p -> (fstPair p, sndPair p) +-- (2,BV 2) +bitsBE :: [Bool] -> Pair NatRepr BV +bitsBE bs = case mkNatRepr (fromInteger (genericLength bs)) of + Some w -> checkNatRepr w $ Pair w (BV (B.fromListBE bs)) + +-- | Construct a 'BV' from a list of bits, in little endian order +-- (bits with lower value index in the list are mapped to lower order +-- bits in the output bitvector). Return the resulting 'BV' along +-- with its width. +-- +-- >>> case bitsLE [True, False] of p -> (fstPair p, sndPair p) +-- (2,BV 1) +bitsLE :: [Bool] -> Pair NatRepr BV +bitsLE bs = case mkNatRepr (fromInteger (genericLength bs)) of + Some w -> checkNatRepr w $ Pair w (BV (B.fromListLE bs)) + +-- | Convert a 'ByteString' (big-endian) of length @n@ to an 'Integer' +-- with @8*n@ bits. This function uses a balanced binary fold to +-- achieve /O(n log n)/ total memory allocation and run-time, in +-- contrast to the /O(n^2)/ that would be required by a naive +-- left-fold. +bytestringToIntegerBE :: BS.ByteString -> Integer +bytestringToIntegerBE bs + | l == 0 = 0 + | l == 1 = toInteger (BS.head bs) + | otherwise = x1 `B.shiftL` (l2 * 8) B..|. x2 + where + l = BS.length bs + l1 = l `div` 2 + l2 = l - l1 + (bs1, bs2) = BS.splitAt l1 bs + x1 = bytestringToIntegerBE bs1 + x2 = bytestringToIntegerBE bs2 + +bytestringToIntegerLE :: BS.ByteString -> Integer +bytestringToIntegerLE bs + | l == 0 = 0 + | l == 1 = toInteger (BS.head bs) + | otherwise = x2 `B.shiftL` (l1 * 8) B..|. x1 + where + l = BS.length bs + l1 = l `div` 2 + (bs1, bs2) = BS.splitAt l1 bs + x1 = bytestringToIntegerLE bs1 + x2 = bytestringToIntegerLE bs2 + +-- | Construct a 'BV' from a big-endian bytestring. +-- +-- >>> case bytestringBE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p) +-- (24,BV 257) +bytestringBE :: BS.ByteString -> Pair NatRepr BV +bytestringBE bs = case mkNatRepr (8*fromIntegral (BS.length bs)) of + Some w -> checkNatRepr w $ Pair w (BV (bytestringToIntegerBE bs)) + +-- | Construct a 'BV' from a little-endian bytestring. +-- +-- >>> case bytestringLE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p) +-- (24,BV 65792) +bytestringLE :: BS.ByteString -> Pair NatRepr BV +bytestringLE bs = case mkNatRepr (8*fromIntegral (BS.length bs)) of + Some w -> checkNatRepr w $ Pair w (BV (bytestringToIntegerLE bs)) + +-- | Construct a 'BV' from a list of bytes, in big endian order (bytes +-- with lower value index in the list are mapped to higher order bytes +-- in the output bitvector). +-- +-- >>> case bytesBE [0, 1, 1] of p -> (fstPair p, sndPair p) +-- (24,BV 257) +bytesBE :: [Word8] -> Pair NatRepr BV +bytesBE = bytestringBE . BS.pack + +-- | Construct a 'BV' from a list of bytes, in little endian order +-- (bytes with lower value index in the list are mapped to lower +-- order bytes in the output bitvector). +-- +-- >>> case bytesLE [0, 1, 1] of p -> (fstPair p, sndPair p) +-- (24,BV 65792) +bytesLE :: [Word8] -> Pair NatRepr BV +bytesLE = bytestringLE . BS.pack + +---------------------------------------- +-- BitVector -> Integer functions + +-- | Unsigned interpretation of a bitvector as a positive Integer. +asUnsigned :: BV w -> Integer +asUnsigned (BV x) = x + +-- | Signed interpretation of a bitvector as an Integer. +asSigned :: (1 <= w) => NatRepr w -> BV w -> Integer +asSigned w (BV x) = + -- NB, fromNatural is OK here because we maintain the invariant that + -- any existing BV value has a representable width + let wInt = fromNatural (natValue w) in + if B.testBit x (wInt - 1) + then x - B.bit wInt + else x + +-- | Unsigned interpretation of a bitvector as a Natural. +asNatural :: BV w -> Natural +asNatural = (fromInteger :: Integer -> Natural) . asUnsigned + +-- | Convert a bitvector to a list of bits, in big endian order +-- (higher order bits in the bitvector are mapped to lower indices in +-- the output list). +-- +-- >>> asBitsBE (knownNat @5) (mkBV knownNat 0b1101) +-- [False,True,True,False,True] +asBitsBE :: NatRepr w -> BV w -> [Bool] +asBitsBE w bv = [ testBit' i bv | i <- fromInteger <$> [wi - 1, wi - 2 .. 0] ] + where wi = intValue w + +-- | Convert a bitvector to a list of bits, in little endian order +-- (lower order bits in the bitvector are mapped to lower indices in +-- the output list). +-- +-- >>> asBitsLE (knownNat @5) (mkBV knownNat 0b1101) +-- [True,False,True,True,False] +asBitsLE :: NatRepr w -> BV w -> [Bool] +asBitsLE w bv = [ testBit' i bv | i <- fromInteger <$> [0 .. wi - 1] ] + where wi = intValue w + +integerToBytesBE :: Natural + -- ^ number of bytes + -> Integer + -> [Word8] +integerToBytesBE n x = + [ fromIntegral (x `B.shiftR` (8*ix)) | ix <- [ni-1, ni-2 .. 0] ] + where ni = fromIntegral n + +integerToBytesLE :: Natural + -- ^ number of bytes + -> Integer + -> [Word8] +integerToBytesLE n x = + [ fromIntegral (x `B.shiftR` (8*ix)) | ix <- [0 .. ni-1] ] + where ni = fromIntegral n + +-- | Convert a bitvector to a list of bytes, in big endian order +-- (higher order bytes in the bitvector are mapped to lower indices in +-- the output list). Return 'Nothing' if the width is not a multiple +-- of 8. +-- +-- >>> asBytesBE (knownNat @32) (mkBV knownNat 0xaabbccdd) +-- Just [170,187,204,221] +asBytesBE :: NatRepr w -> BV w -> Maybe [Word8] +asBytesBE w (BV x) + | natValue w `mod` 8 == 0 = Just $ integerToBytesBE (natValue w `div` 8) x + | otherwise = Nothing + +-- | Convert a bitvector to a list of bytes, in little endian order +-- (lower order bytes in the bitvector are mapped to lower indices in +-- the output list). Return 'Nothing' if the width is not a multiple +-- of 8. +-- +-- >>> asBytesLE (knownNat @32) (mkBV knownNat 0xaabbccdd) +-- Just [221,204,187,170] +asBytesLE :: NatRepr w -> BV w -> Maybe [Word8] +asBytesLE w (BV x) + | natValue w `mod` 8 == 0 = Just $ integerToBytesLE (natValue w `div` 8) x + | otherwise = Nothing + +-- | 'asBytesBE', but for bytestrings. +asBytestringBE :: NatRepr w -> BV w -> Maybe BS.ByteString +asBytestringBE w bv = BS.pack <$> asBytesBE w bv + +-- | 'asBytesLE', but for bytestrings. +asBytestringLE :: NatRepr w -> BV w -> Maybe BS.ByteString +asBytestringLE w bv = BS.pack <$> asBytesLE w bv + +---------------------------------------- +-- BV w operations (fixed width) + +-- | Bitwise and. +and :: BV w -> BV w -> BV w +and (BV x) (BV y) = BV (x B..&. y) + +-- | Bitwise or. +or :: BV w -> BV w -> BV w +or (BV x) (BV y) = BV (x B..|. y) + +-- | Bitwise xor. +xor :: BV w -> BV w -> BV w +xor (BV x) (BV y) = BV (x `B.xor` y) + +-- | Bitwise complement (flip every bit). +complement :: NatRepr w -> BV w -> BV w +complement w (BV x) = mkBV' w (B.complement x) + + +-- | Clamp shift amounts to the word width and +-- coerce to an @Int@ +shiftAmount :: NatRepr w -> Natural -> Int +shiftAmount w shf = fromNatural (min (natValue w) shf) + +-- | Left shift by positive 'Natural'. +shl :: NatRepr w -> BV w -> Natural -> BV w +shl w (BV x) shf = mkBV' w (x `B.shiftL` shiftAmount w shf) + +-- | Right arithmetic shift by positive 'Natural'. +ashr :: (1 <= w) => NatRepr w -> BV w -> Natural -> BV w +ashr w bv shf = mkBV' w (asSigned w bv `B.shiftR` shiftAmount w shf) + +-- | Right logical shift by positive 'Natural'. +lshr :: NatRepr w -> BV w -> Natural -> BV w +lshr w (BV x) shf = + -- Shift right (logical by default since the value is positive). No + -- need to truncate bits, since the result is guaranteed to occupy + -- no more bits than the input. + BV (x `B.shiftR` shiftAmount w shf) + +-- | Bitwise rotate left. +rotateL :: NatRepr w -> BV w -> Natural -> BV w +rotateL w bv rot' = leftChunk `or` rightChunk + where rot = rot' `mod` wNatural + leftChunk = shl w bv rot + rightChunk = lshr w bv (wNatural - rot) + wNatural = natValue w + +-- | Bitwise rotate right. +rotateR :: NatRepr w -> BV w -> Natural -> BV w +rotateR w bv rot' = leftChunk `or` rightChunk + where rot = rot' `mod` wNatural + rightChunk = lshr w bv rot + leftChunk = shl w bv (wNatural - rot) + wNatural = natValue w + +-- | The zero bitvector of any width. +zero :: NatRepr w -> BV w +zero w = checkNatRepr w $ BV 0 + +-- | The bitvector with value 1, of any positive width. +one :: 1 <= w => NatRepr w -> BV w +one w = checkNatRepr w $ BV 1 + +-- | The bitvector whose value is its own width, of any width. +width :: NatRepr w -> BV w +width w = checkNatRepr w $ BV (intValue w) + +-- | The 'BV' that has a particular bit set, and is 0 everywhere +-- else. +bit :: ix+1 <= w + => NatRepr w + -- ^ Desired output width + -> NatRepr ix + -- ^ Index of bit to set + -> BV w +bit w ix = + checkNatRepr w $ + -- NB fromNatural is OK here because of the (ix+1 Natural + -- ^ Index of bit to set + -> BV w +bit' w ix + | ix < natValue w = checkNatRepr w $ mkBV' w (B.bit (fromNatural ix)) + | otherwise = zero w + +-- | @setBit bv ix@ is the same as @or bv (bit knownNat ix)@. +setBit :: ix+1 <= w + => NatRepr ix + -- ^ Index of bit to set + -> BV w + -- ^ Original bitvector + -> BV w +setBit ix bv = + -- NB, fromNatural is OK because of the (ix+1 <= w) constraint + or bv (BV (B.bit (fromNatural (natValue ix)))) + +-- | Like 'setBit', but without the requirement that the index bit +-- refers to an actual bit in the input 'BV'. If it is out of range, +-- just silently return the original input. +setBit' :: NatRepr w + -- ^ Desired output width + -> Natural + -- ^ Index of bit to set + -> BV w + -- ^ Original bitvector + -> BV w +setBit' w ix bv + | ix < natValue w = or bv (BV (B.bit (fromNatural ix))) + | otherwise = bv + +-- | @clearBit w bv ix@ is the same as @and bv (complement (bit w ix))@. +clearBit :: ix+1 <= w + => NatRepr w + -- ^ Desired output width + -> NatRepr ix + -- ^ Index of bit to clear + -> BV w + -- ^ Original bitvector + -> BV w +clearBit w ix bv = + -- NB, fromNatural is OK because of the (ix+1<=w) constraint + and bv (complement w (BV (B.bit (fromNatural (natValue ix))))) + + +-- | Like 'clearBit', but without the requirement that the index bit +-- refers to an actual bit in the input 'BV'. If it is out of range, +-- just silently return the original input. +clearBit' :: NatRepr w + -- ^ Desired output width + -> Natural + -- ^ Index of bit to clear + -> BV w + -- ^ Original bitvector + -> BV w +clearBit' w ix bv + | ix < natValue w = and bv (complement w (BV (B.bit (fromNatural ix)))) + | otherwise = bv + +-- | @complementBit bv ix@ is the same as @xor bv (bit knownNat ix)@. +complementBit :: ix+1 <= w + => NatRepr ix + -- ^ Index of bit to flip + -> BV w + -- ^ Original bitvector + -> BV w +complementBit ix bv = + -- NB, fromNatural is OK because of (ix+1 <= w) constraint + xor bv (BV (B.bit (fromNatural (natValue ix)))) + +-- | Like 'complementBit', but without the requirement that the index +-- bit refers to an actual bit in the input 'BV'. If it is out of +-- range, just silently return the original input. +complementBit' :: NatRepr w + -- ^ Desired output width + -> Natural + -- ^ Index of bit to flip + -> BV w + -- ^ Original bitvector + -> BV w +complementBit' w ix bv + | ix < natValue w = xor bv (BV (B.bit (fromNatural ix))) + | otherwise = bv + +-- | Test if a particular bit is set. +testBit :: ix+1 <= w => NatRepr ix -> BV w -> Bool +testBit ix (BV x) = B.testBit x (fromNatural (natValue ix)) + +-- | Like 'testBit', but takes a 'Natural' for the bit index. If the +-- index is out of bounds, return 'False'. +testBit' :: Natural -> BV w -> Bool +testBit' ix (BV x) + -- NB, If the index is larger than the maximum representable 'Int', + -- this function should be 'False' by construction of 'BV'. + | ix > fromIntegral (maxBound :: Int) = False + | otherwise = B.testBit x (fromNatural ix) + +-- | Get the number of 1 bits in a 'BV'. +popCount :: BV w -> BV w +popCount (BV x) = BV (toInteger (B.popCount x)) + +-- | Count trailing zeros in a 'BV'. +ctz :: NatRepr w -> BV w -> BV w +ctz w (BV x) = BV (go 0) + where go !i | i < intValue w && + B.testBit x (fromInteger i) == False = go (i+1) + | otherwise = i + +-- | Count leading zeros in a 'BV'. +clz :: NatRepr w -> BV w -> BV w +clz w (BV x) = BV (go 0) + where go !i | i < intValue w && + B.testBit x (fromInteger (intValue w - i - 1)) == False = + go (i+1) + | otherwise = i + +-- | Truncate a bitvector to a particular width given at runtime, +-- while keeping the type-level width constant. +truncBits :: Natural -> BV w -> BV w +truncBits b (BV x) = checkNatural b $ BV (x B..&. (B.bit (fromNatural b) - 1)) + +---------------------------------------- +-- BV w arithmetic operations (fixed width) + +-- | Bitvector add. +add :: NatRepr w -> BV w -> BV w -> BV w +add w (BV x) (BV y) = mkBV' w (x+y) + +-- | Bitvector subtract. +sub :: NatRepr w -> BV w -> BV w -> BV w +sub w (BV x) (BV y) = mkBV' w (x-y) + +-- | Bitvector multiply. +mul :: NatRepr w -> BV w -> BV w -> BV w +mul w (BV x) (BV y) = mkBV' w (x*y) + +-- | Bitvector division (unsigned). Rounds to zero. Division by zero +-- yields a runtime error. +uquot :: BV w -> BV w -> BV w +uquot (BV x) (BV y) = BV (x `quot` y) + +-- | Bitvector remainder after division (unsigned), when rounded to +-- zero. Division by zero yields a runtime error. +urem :: BV w -> BV w -> BV w +urem (BV x) (BV y) = BV (x `rem` y) + +-- | 'uquot' and 'urem' returned as a pair. +uquotRem :: BV w -> BV w -> (BV w, BV w) +uquotRem bv1 bv2 = (uquot bv1 bv2, urem bv1 bv2) + +-- | Bitvector division (signed). Rounds to zero. Division by zero +-- yields a runtime error. +squot :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w +squot w bv1 bv2 = mkBV' w (x `quot` y) + where x = asSigned w bv1 + y = asSigned w bv2 + +-- | Bitvector remainder after division (signed), when rounded to +-- zero. Division by zero yields a runtime error. +srem :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w +srem w bv1 bv2 = mkBV' w (x `rem` y) + where x = asSigned w bv1 + y = asSigned w bv2 + +-- | 'squot' and 'srem' returned as a pair. +squotRem :: (1 <= w) => NatRepr w -> BV w -> BV w -> (BV w, BV w) +squotRem w bv1 bv2 = (squot w bv1 bv2, srem w bv1 bv2) + +-- | Bitvector division (signed). Rounds to negative infinity. Division +-- by zero yields a runtime error. +sdiv :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w +sdiv w bv1 bv2 = mkBV' w (x `div` y) + where x = asSigned w bv1 + y = asSigned w bv2 + +-- | Bitvector remainder after division (signed), when rounded to +-- negative infinity. Division by zero yields a runtime error. +smod :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w +smod w bv1 bv2 = mkBV' w (x `mod` y) + where x = asSigned w bv1 + y = asSigned w bv2 + +-- | 'sdiv' and 'smod' returned as a pair. +sdivMod :: (1 <= w) => NatRepr w -> BV w -> BV w -> (BV w, BV w) +sdivMod w bv1 bv2 = (sdiv w bv1 bv2, smod w bv1 bv2) + +-- | Bitvector absolute value. Returns the 2's complement +-- magnitude of the bitvector. +abs :: (1 <= w) => NatRepr w -> BV w -> BV w +abs w bv = mkBV' w (Prelude.abs (asSigned w bv)) + +-- | 2's complement bitvector negation. +negate :: NatRepr w -> BV w -> BV w +negate w (BV x) = mkBV' w (-x) + +-- | Get the sign bit as a 'BV'. +signBit :: 1 <= w => NatRepr w -> BV w -> BV w +signBit w bv@(BV _) = lshr w bv (natValue w - 1) `and` BV 1 + +-- | Return 1 if positive, -1 if negative, and 0 if 0. +signum :: 1 <= w => NatRepr w -> BV w -> BV w +signum w bv = mkBV' w (Prelude.signum (asSigned w bv)) + +-- | Signed less than. +slt :: (1 <= w) => NatRepr w -> BV w -> BV w -> Bool +slt w bv1 bv2 = asSigned w bv1 < asSigned w bv2 + +-- | Signed less than or equal. +sle :: (1 <= w) => NatRepr w -> BV w -> BV w -> Bool +sle w bv1 bv2 = asSigned w bv1 <= asSigned w bv2 + +-- | Unsigned less than. +ult :: BV w -> BV w -> Bool +ult bv1 bv2 = asUnsigned bv1 < asUnsigned bv2 + +-- | Unsigned less than or equal. +ule :: BV w -> BV w -> Bool +ule bv1 bv2 = asUnsigned bv1 <= asUnsigned bv2 + +-- | Unsigned minimum of two bitvectors. +umin :: BV w -> BV w -> BV w +umin (BV x) (BV y) = if x < y then BV x else BV y + +-- | Unsigned maximum of two bitvectors. +umax :: BV w -> BV w -> BV w +umax (BV x) (BV y) = if x < y then BV y else BV x + +-- | Signed minimum of two bitvectors. +smin :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w +smin w bv1 bv2 = if asSigned w bv1 < asSigned w bv2 then bv1 else bv2 + +-- | Signed maximum of two bitvectors. +smax :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w +smax w bv1 bv2 = if asSigned w bv1 < asSigned w bv2 then bv2 else bv1 + +---------------------------------------- +-- Width-changing operations + +-- | Concatenate two bitvectors. The first argument gets placed in the +-- higher order bits. +-- +-- >>> concat knownNat (mkBV (knownNat @3) 0b001) (mkBV (knownNat @2) 0b10) +-- BV 6 +-- >>> :type it +-- it :: BV 5 +concat :: NatRepr w + -- ^ Width of higher-order bits + -> NatRepr w' + -- ^ Width of lower-order bits + -> BV w + -- ^ Higher-order bits + -> BV w' + -- ^ Lower-order bits + -> BV (w+w') +concat w w' (BV hi) (BV lo) = checkNatRepr (w `addNat` w') $ + BV ((hi `B.shiftL` (fromNatural (natValue w'))) B..|. lo) + +-- | Slice out a smaller bitvector from a larger one. +-- +-- >>> select (knownNat @4) (knownNat @1) (mkBV (knownNat @12) 0b110010100110) +-- BV 3 +-- >>> :type it +-- it :: BV 4 +select :: ix + w' <= w + => NatRepr ix + -- ^ Index to start selecting from + -> NatRepr w' + -- ^ Desired output width + -> BV w + -- ^ Bitvector to select from + -> BV w' +select ix w' (BV x) = mkBV' w' xShf + -- NB fromNatural is OK because of (ix + w' <= w) constraint + where xShf = x `B.shiftR` (fromNatural (natValue ix)) + +-- | Like 'select', but takes a 'Natural' as the index to start +-- selecting from. Neither the index nor the output width is checked +-- to ensure the resulting 'BV' lies entirely within the bounds of the +-- original bitvector. Any bits "selected" from beyond the bounds of +-- the input bitvector will be 0. +-- +-- >>> select' (knownNat @4) 9 (mkBV (knownNat @12) 0b110010100110) +-- BV 6 +-- >>> :type it +-- it :: BV 4 +select' :: Natural + -- ^ Index to start selecting from + -> NatRepr w' + -- ^ Desired output width + -> BV w + -- ^ Bitvector to select from + -> BV w' +select' ix w' (BV x) + | toInteger ix < toInteger (maxBound :: Int) = mkBV w' (x `B.shiftR` (fromNatural ix)) + | otherwise = zero w' + +-- | Zero-extend a bitvector to one of strictly greater width. +-- +-- >>> zext (knownNat @8) (mkBV (knownNat @4) 0b1101) +-- BV 13 +-- >>> :type it +-- it :: BV 8 +zext :: w + 1 <= w' + => NatRepr w' + -- ^ Desired output width + -> BV w + -- ^ Bitvector to extend + -> BV w' +zext w (BV x) = checkNatRepr w $ BV x + +-- | Sign-extend a bitvector to one of strictly greater width. +sext :: (1 <= w, w + 1 <= w') + => NatRepr w + -- ^ Width of input bitvector + -> NatRepr w' + -- ^ Desired output width + -> BV w + -- ^ Bitvector to extend + -> BV w' +sext w w' bv = mkBV w' (asSigned w bv) + +-- | Truncate a bitvector to one of strictly smaller width. +trunc :: w' + 1 <= w + => NatRepr w' + -- ^ Desired output width + -> BV w + -- ^ Bitvector to truncate + -> BV w' +trunc w' (BV x) = mkBV' w' x + +-- | Like 'trunc', but allows the input width to be greater than or +-- equal to the output width, in which case it just performs a zero +-- extension. +trunc' :: NatRepr w' + -- ^ Desired output width + -> BV w + -- ^ Bitvector to truncate + -> BV w' +trunc' w' (BV x) = mkBV w' x + +-- | Wide multiply of two bitvectors. +mulWide :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w+w') +mulWide w w' (BV x) (BV y) = checkNatRepr (w `addNat` w') $ BV (x*y) + +---------------------------------------- +-- Enum functions + +-- | Unsigned successor. @succUnsigned w (maxUnsigned w)@ returns 'Nothing'. +succUnsigned :: NatRepr w -> BV w -> Maybe (BV w) +succUnsigned w (BV x) = + if x == P.maxUnsigned w + then Nothing + else Just (BV (x+1)) + +-- | Signed successor. @succSigned w (maxSigned w)@ returns 'Nothing'. +succSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w) +succSigned w (BV x) = + if x == P.maxSigned w + then Nothing + else Just (mkBV' w (x+1)) + +-- | Unsigned predecessor. @predUnsigned w zero@ returns 'Nothing'. +predUnsigned :: NatRepr w -> BV w -> Maybe (BV w) +predUnsigned w (BV x) = + if x == P.minUnsigned w + then Nothing + else Just (BV (x-1)) + +-- | Signed predecessor. @predSigned w (minSigned w)@ returns 'Nothing'. +predSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w) +predSigned w bv@(BV x) = + if bv == minSigned w + then Nothing + else Just (mkBV' w (x-1)) + +-- | List of all unsigned bitvectors from a lower to an upper bound, +-- inclusive. +enumFromToUnsigned :: BV w + -- ^ Lower bound + -> BV w + -- ^ Upper bound + -> [BV w] +enumFromToUnsigned bv1 bv2 = BV <$> [asUnsigned bv1 .. asUnsigned bv2] + +-- | List of all signed bitvectors from a lower to an upper bound, +-- inclusive. +enumFromToSigned :: 1 <= w => NatRepr w + -> BV w + -- ^ Lower bound + -> BV w + -- ^ Upper bound + -> [BV w] +enumFromToSigned w bv1 bv2 = (BV . fromJust . signedToUnsigned w) <$> [asSigned w bv1 .. asSigned w bv2] + +---------------------------------------- +-- Pretty printing + +-- | Pretty print in hex +ppHex :: NatRepr w -> BV w -> String +ppHex w (BV x) = "0x" ++ N.showHex x "" ++ ":" ++ ppWidth w + +-- | Pretty print in binary +ppBin :: NatRepr w -> BV w -> String +ppBin w (BV x) = "0b" ++ N.showIntAtBase 2 intToDigit x "" ++ ":" ++ ppWidth w + +-- | Pretty print in octal +ppOct :: NatRepr w -> BV w -> String +ppOct w (BV x) = "0o" ++ N.showOct x "" ++ ":" ++ ppWidth w + +-- | Pretty print in decimal +ppDec :: NatRepr w -> BV w -> String +ppDec w (BV x) = show x ++ ":" ++ ppWidth w + +ppWidth :: NatRepr w -> String +ppWidth w = "[" ++ show (natValue w) ++ "]" diff --git a/src/Data/BitVector/Sized/Overflow.hs b/src/Data/BitVector/Sized/Overflow.hs new file mode 100644 --- /dev/null +++ b/src/Data/BitVector/Sized/Overflow.hs @@ -0,0 +1,216 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeOperators #-} + +{-| +Module : Data.BitVector.Sized.Overflow +Copyright : (c) Galois Inc. 2020 +License : BSD-3 +Maintainer : Ben Selfridge +Stability : experimental +Portability : portable + +This module provides alternative definitions of certain bitvector +functions that might produce signed or unsigned overflow. Instead of +producing a pure value, these versions produce the same value along +with overflow flags. We only provide definitions for operators that +might actually overflow. + +-} + +module Data.BitVector.Sized.Overflow + ( Overflow(..) + , UnsignedOverflow(..) + , SignedOverflow(..) + , ofUnsigned + , ofSigned + , ofResult + -- * Overflowing bitwise operators + , shlOf + -- * Overflowing arithmetic operators + , addOf + , subOf + , mulOf + , squotOf + , sremOf + , sdivOf + , smodOf + ) where + +import qualified Data.Bits as B +import Numeric.Natural +import GHC.TypeLits + +import Data.Parameterized ( NatRepr ) +import qualified Data.Parameterized.NatRepr as P + +import Data.BitVector.Sized.Internal ( BV(..) + , mkBV' + , asUnsigned + , asSigned + , shiftAmount + ) + + +---------------------------------------- +-- Unsigned and signed overflow datatypes + +-- | Datatype representing the possibility of unsigned overflow. +data UnsignedOverflow = UnsignedOverflow + | NoUnsignedOverflow + deriving (Show, Eq) + +instance Semigroup UnsignedOverflow where + NoUnsignedOverflow <> NoUnsignedOverflow = NoUnsignedOverflow + _ <> _ = UnsignedOverflow + +instance Monoid UnsignedOverflow where + mempty = NoUnsignedOverflow + +-- | Datatype representing the possibility of signed overflow. +data SignedOverflow = SignedOverflow + | NoSignedOverflow + deriving (Show, Eq) + +instance Semigroup SignedOverflow where + NoSignedOverflow <> NoSignedOverflow = NoSignedOverflow + _ <> _ = SignedOverflow + +instance Monoid SignedOverflow where + mempty = NoSignedOverflow + +---------------------------------------- +-- Overflow wrapper +-- | A value annotated with overflow information. +data Overflow a = + Overflow UnsignedOverflow SignedOverflow a + deriving (Show, Eq) + +-- | Return 'True' if a computation caused unsigned overflow. +ofUnsigned :: Overflow a -> Bool +ofUnsigned (Overflow UnsignedOverflow _ _) = True +ofUnsigned _ = False + +-- | Return 'True' if a computation caused signed overflow. +ofSigned :: Overflow a -> Bool +ofSigned (Overflow _ SignedOverflow _) = True +ofSigned _ = False + +-- | Return the result of a computation. +ofResult :: Overflow a -> a +ofResult (Overflow _ _ res) = res + +instance Foldable Overflow where + foldMap f (Overflow _ _ a) = f a + +instance Traversable Overflow where + sequenceA (Overflow uof sof a) = Overflow uof sof <$> a + +instance Functor Overflow where + fmap f (Overflow uof sof a) = Overflow uof sof (f a) + +instance Applicative Overflow where + pure a = Overflow mempty mempty a + Overflow uof sof f <*> Overflow uof' sof' a = + Overflow (uof <> uof') (sof <> sof') (f a) + +-- | Monad for bitvector operations which might produce signed or +-- unsigned overflow. +instance Monad Overflow where + Overflow uof sof a >>= k = + let Overflow uof' sof' b = k a + in Overflow (uof <> uof') (sof <> sof') b + +getUof :: NatRepr w -> Integer -> UnsignedOverflow +getUof w x = if x < P.minUnsigned w || x > P.maxUnsigned w + then UnsignedOverflow + else NoUnsignedOverflow + +getSof :: NatRepr w -> Integer -> SignedOverflow +getSof w x = case P.isZeroOrGT1 w of + Left P.Refl -> NoSignedOverflow + Right P.LeqProof -> + if x < P.minSigned w || x > P.maxSigned w + then SignedOverflow + else NoSignedOverflow + +-- | This only works if the operation has equivalent signed and +-- unsigned interpretations on bitvectors. +liftBinary :: (1 <= w) => (Integer -> Integer -> Integer) + -> NatRepr w + -> BV w -> BV w -> Overflow (BV w) +liftBinary op w xv yv = + let ux = asUnsigned xv + uy = asUnsigned yv + sx = asSigned w xv + sy = asSigned w yv + + ures = ux `op` uy + sres = sx `op` sy + + uof = getUof w ures + sof = getSof w sres + in Overflow uof sof (mkBV' w ures) + +-- | Bitvector add. +addOf :: (1 <= w) => NatRepr w -> BV w -> BV w -> Overflow (BV w) +addOf = liftBinary (+) + +-- | Bitvector subtract. +subOf :: (1 <= w) => NatRepr w -> BV w -> BV w -> Overflow (BV w) +subOf = liftBinary (-) + +-- | Bitvector multiply. +mulOf :: (1 <= w) => NatRepr w -> BV w -> BV w -> Overflow (BV w) +mulOf = liftBinary (*) + +-- | Left shift by positive 'Natural'. +shlOf :: (1 <= w) => NatRepr w -> BV w -> Natural -> Overflow (BV w) +shlOf w xv shf = + let ux = asUnsigned xv + sx = asSigned w xv + ures = ux `B.shiftL` shiftAmount w shf + sres = sx `B.shiftL` shiftAmount w shf + uof = getUof w ures + sof = getSof w sres + in Overflow uof sof (mkBV' w ures) + +-- | Bitvector division (signed). Rounds to zero. Division by zero +-- yields a runtime error. +squotOf :: (1 <= w) => NatRepr w -> BV w -> BV w -> Overflow (BV w) +squotOf w bv1 bv2 = Overflow NoUnsignedOverflow sof (mkBV' w (x `quot` y)) + where x = asSigned w bv1 + y = asSigned w bv2 + sof = if (x == P.minSigned w && y == -1) + then SignedOverflow + else NoSignedOverflow + +-- | Bitvector remainder after division (signed), when rounded to +-- zero. Division by zero yields a runtime error. +sremOf :: (1 <= w) => NatRepr w -> BV w -> BV w -> Overflow (BV w) +sremOf w bv1 bv2 = Overflow NoUnsignedOverflow sof (mkBV' w (x `rem` y)) + where x = asSigned w bv1 + y = asSigned w bv2 + sof = if (x == P.minSigned w && y == -1) + then SignedOverflow + else NoSignedOverflow + +-- | Bitvector division (signed). Rounds to zero. Division by zero +-- yields a runtime error. +sdivOf :: (1 <= w) => NatRepr w -> BV w -> BV w -> Overflow (BV w) +sdivOf w bv1 bv2 = Overflow NoUnsignedOverflow sof (mkBV' w (x `div` y)) + where x = asSigned w bv1 + y = asSigned w bv2 + sof = if (x == P.minSigned w && y == -1) + then SignedOverflow + else NoSignedOverflow + +-- | Bitvector remainder after division (signed), when rounded to +-- zero. Division by zero yields a runtime error. +smodOf :: (1 <= w) => NatRepr w -> BV w -> BV w -> Overflow (BV w) +smodOf w bv1 bv2 = Overflow NoUnsignedOverflow sof (mkBV' w (x `mod` y)) + where x = asSigned w bv1 + y = asSigned w bv2 + sof = if (x == P.minSigned w && y == -1) + then SignedOverflow + else NoSignedOverflow diff --git a/src/Data/BitVector/Sized/Panic.hs b/src/Data/BitVector/Sized/Panic.hs new file mode 100644 --- /dev/null +++ b/src/Data/BitVector/Sized/Panic.hs @@ -0,0 +1,20 @@ +{-# LANGUAGE TemplateHaskell #-} + +module Data.BitVector.Sized.Panic + ( panic + ) where + +import Panic hiding (panic) +import qualified Panic + +data BVSized = BVSized + +panic :: String -> [String] -> a +panic = Panic.panic BVSized + +instance PanicComponent BVSized where + panicComponentName _ = "bv-sized" + panicComponentIssues _ = "https://github.com/GaloisInc/bv-sized/issues" + + {-# Noinline panicComponentRevision #-} + panicComponentRevision = $useGitRevision diff --git a/src/Data/BitVector/Sized/Signed.hs b/src/Data/BitVector/Sized/Signed.hs new file mode 100644 --- /dev/null +++ b/src/Data/BitVector/Sized/Signed.hs @@ -0,0 +1,128 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE MultiWayIf #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeApplications #-} + +{-| +Module : Data.BitVector.Sized.Signed +Copyright : (c) Galois Inc. 2018 +License : BSD-3 +Maintainer : benselfridge@galois.com +Stability : experimental +Portability : portable + +This module defines a wrapper around the 'BV' type, 'SignedBV', with +instances not provided by 'BV'. +-} + +module Data.BitVector.Sized.Signed + ( SignedBV(..) + , mkSignedBV + ) where + +import Data.BitVector.Sized (BV, mkBV) +import qualified Data.BitVector.Sized.Internal as BV +import Data.BitVector.Sized.Panic (panic) +import Data.Parameterized.NatRepr + +import Data.Bits (Bits(..), FiniteBits(..)) +import Data.Ix +import GHC.Generics +import GHC.TypeLits +import Numeric.Natural + +-- | Signed bit vector. +newtype SignedBV w = SignedBV (BV w) + deriving (Generic, Show, Read, Eq) + +-- | Convenience wrapper for 'BV.mkBV'. +mkSignedBV :: NatRepr w -> Integer -> SignedBV w +mkSignedBV w x = SignedBV (BV.mkBV w x) + +instance (KnownNat w, 1 <= w) => Ord (SignedBV w) where + SignedBV bv1 `compare` SignedBV bv2 = + if | bv1 == bv2 -> EQ + | BV.slt knownNat bv1 bv2 -> LT + | otherwise -> GT + +liftUnary :: (BV w -> BV w) + -> SignedBV w + -> SignedBV w +liftUnary op (SignedBV bv) = SignedBV (op bv) + +liftBinary :: (BV w -> BV w -> BV w) + -> SignedBV w + -> SignedBV w + -> SignedBV w +liftBinary op (SignedBV bv1) (SignedBV bv2) = SignedBV (op bv1 bv2) + +liftBinaryInt :: (BV w -> Natural -> BV w) + -> SignedBV w + -> Int + -> SignedBV w +liftBinaryInt op (SignedBV bv) i = SignedBV (op bv (intToNatural i)) + +intToNatural :: Int -> Natural +intToNatural = fromIntegral + +instance (KnownNat w, 1 <= w) => Bits (SignedBV w) where + (.&.) = liftBinary BV.and + (.|.) = liftBinary BV.or + xor = liftBinary BV.xor + complement = liftUnary (BV.complement knownNat) + shiftL = liftBinaryInt (BV.shl knownNat) + shiftR = liftBinaryInt (BV.ashr knownNat) + rotateL = liftBinaryInt (BV.rotateL knownNat) + rotateR = liftBinaryInt (BV.rotateR knownNat) + bitSize _ = widthVal (knownNat @w) + bitSizeMaybe _ = Just (widthVal (knownNat @w)) + isSigned = const True + testBit (SignedBV bv) ix = BV.testBit' (intToNatural ix) bv + bit = SignedBV . BV.bit' knownNat . intToNatural + popCount (SignedBV bv) = fromInteger (BV.asUnsigned (BV.popCount bv)) + +instance (KnownNat w, 1 <= w) => FiniteBits (SignedBV w) where + finiteBitSize _ = widthVal (knownNat @w) + countLeadingZeros (SignedBV bv) = fromInteger $ BV.asUnsigned $ BV.clz knownNat bv + countTrailingZeros (SignedBV bv) = fromInteger $ BV.asUnsigned $ BV.ctz knownNat bv + +instance (KnownNat w, 1 <= w) => Num (SignedBV w) where + (+) = liftBinary (BV.add knownNat) + (*) = liftBinary (BV.mul knownNat) + abs = liftUnary (BV.abs knownNat) + signum (SignedBV bv) = mkSignedBV knownNat $ signum $ BV.asSigned knownNat bv + fromInteger = SignedBV . mkBV knownNat + negate = liftUnary (BV.negate knownNat) + +instance (KnownNat w, 1 <= w) => Enum (SignedBV w) where + toEnum = SignedBV . mkBV knownNat . checkInt + where checkInt i | lo <= toInteger i && toInteger i <= hi = toInteger i + | otherwise = panic "Data.BitVector.Sized.Signed" + ["toEnum: bad argument"] + where lo = minSigned (knownNat @w) + hi = maxSigned (knownNat @w) + + fromEnum (SignedBV bv) = fromInteger (BV.asSigned (knownNat @w) bv) + +instance (KnownNat w, 1 <= w) => Ix (SignedBV w) where + range (SignedBV loBV, SignedBV hiBV) = + (SignedBV . mkBV knownNat) <$> + [BV.asSigned knownNat loBV .. BV.asSigned knownNat hiBV] + index (SignedBV loBV, SignedBV hiBV) (SignedBV ixBV) = + index ( BV.asSigned knownNat loBV + , BV.asSigned knownNat hiBV) + (BV.asSigned knownNat ixBV) + inRange (SignedBV loBV, SignedBV hiBV) (SignedBV ixBV) = + inRange ( BV.asSigned knownNat loBV + , BV.asSigned knownNat hiBV) + (BV.asSigned knownNat ixBV) + +instance (KnownNat w, 1 <= w) => Bounded (SignedBV w) where + minBound = SignedBV (BV.minSigned knownNat) + maxBound = SignedBV (BV.maxSigned knownNat) diff --git a/src/Data/BitVector/Sized/Unsigned.hs b/src/Data/BitVector/Sized/Unsigned.hs new file mode 100644 --- /dev/null +++ b/src/Data/BitVector/Sized/Unsigned.hs @@ -0,0 +1,120 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeApplications #-} + +{-| +Module : Data.BitVector.Sized.Unsigned +Copyright : (c) Galois Inc. 2018 +License : BSD-3 +Maintainer : benselfridge@galois.com +Stability : experimental +Portability : portable + +This module defines a wrapper around the 'BV' type, 'UnsignedBV', with +instances not provided by 'BV'. +-} + +module Data.BitVector.Sized.Unsigned + ( UnsignedBV(..) + , mkUnsignedBV + ) where + +import Data.BitVector.Sized.Internal (BV(..), mkBV) +import qualified Data.BitVector.Sized.Internal as BV +import Data.BitVector.Sized.Panic (panic) +import Data.Parameterized.NatRepr + +import Data.Bits (Bits(..), FiniteBits(..)) +import Data.Ix +import GHC.Generics +import GHC.TypeLits +import Numeric.Natural + +-- | Signed bit vector. +newtype UnsignedBV w = UnsignedBV { asBV :: BV w } + deriving (Generic, Show, Read, Eq, Ord) + +-- | Convenience wrapper for 'BV.mkBV'. +mkUnsignedBV :: NatRepr w -> Integer -> UnsignedBV w +mkUnsignedBV w x = UnsignedBV (BV.mkBV w x) + +liftUnary :: (BV w -> BV w) + -> UnsignedBV w + -> UnsignedBV w +liftUnary op (UnsignedBV bv) = UnsignedBV (op bv) + +liftBinary :: (BV w -> BV w -> BV w) + -> UnsignedBV w + -> UnsignedBV w + -> UnsignedBV w +liftBinary op (UnsignedBV bv1) (UnsignedBV bv2) = UnsignedBV (op bv1 bv2) + +liftBinaryInt :: (BV w -> Natural -> BV w) + -> UnsignedBV w + -> Int + -> UnsignedBV w +liftBinaryInt op (UnsignedBV bv) i = UnsignedBV (op bv (intToNatural i)) + +intToNatural :: Int -> Natural +intToNatural = fromIntegral + +instance KnownNat w => Bits (UnsignedBV w) where + (.&.) = liftBinary BV.and + (.|.) = liftBinary BV.or + xor = liftBinary BV.xor + complement = liftUnary (BV.complement knownNat) + shiftL = liftBinaryInt (BV.shl knownNat) + shiftR = liftBinaryInt (BV.lshr knownNat) + rotateL = liftBinaryInt (BV.rotateL knownNat) + rotateR = liftBinaryInt (BV.rotateR knownNat) + bitSize _ = widthVal (knownNat @w) + bitSizeMaybe _ = Just (widthVal (knownNat @w)) + isSigned = const False + testBit (UnsignedBV bv) ix = BV.testBit' (intToNatural ix) bv + bit = UnsignedBV . BV.bit' knownNat . intToNatural + popCount (UnsignedBV bv) = fromInteger (BV.asUnsigned (BV.popCount bv)) + +instance KnownNat w => FiniteBits (UnsignedBV w) where + finiteBitSize _ = widthVal (knownNat @w) + countLeadingZeros (UnsignedBV bv) = fromInteger $ BV.asUnsigned $ BV.clz knownNat bv + countTrailingZeros (UnsignedBV bv) = fromInteger $ BV.asUnsigned $ BV.ctz knownNat bv + +instance KnownNat w => Num (UnsignedBV w) where + (+) = liftBinary (BV.add knownNat) + (*) = liftBinary (BV.mul knownNat) + abs = id + signum (UnsignedBV bv) = UnsignedBV $ BV.BV $ signum $ BV.asUnsigned bv + fromInteger = UnsignedBV . mkBV knownNat + -- in this case, negate just means "additive inverse" + negate = liftUnary (BV.negate knownNat) + +instance KnownNat w => Enum (UnsignedBV w) where + toEnum = UnsignedBV . mkBV knownNat . checkInt + where checkInt i | 0 <= i && toInteger i <= (maxUnsigned (knownNat @w)) = toInteger i + | otherwise = panic "Data.BitVector.Sized.Unsigned" + ["toEnum: bad argument"] + + fromEnum (UnsignedBV bv) = fromInteger (BV.asUnsigned bv) + +instance KnownNat w => Ix (UnsignedBV w) where + range (UnsignedBV loBV, UnsignedBV hiBV) = + (UnsignedBV . mkBV knownNat) <$> + [BV.asUnsigned loBV .. BV.asUnsigned hiBV] + index (UnsignedBV loBV, UnsignedBV hiBV) (UnsignedBV ixBV) = + index ( BV.asUnsigned loBV, + BV.asUnsigned hiBV) + (BV.asUnsigned ixBV) + inRange (UnsignedBV loBV, UnsignedBV hiBV) (UnsignedBV ixBV) = + inRange ( BV.asUnsigned loBV + , BV.asUnsigned hiBV) + (BV.asUnsigned ixBV) + +instance KnownNat w => Bounded (UnsignedBV w) where + minBound = UnsignedBV (BV.minUnsigned knownNat) + maxBound = UnsignedBV (BV.maxUnsigned knownNat) diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -0,0 +1,319 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +module Main where + +-- Testing modules +import Hedgehog +import qualified Hedgehog.Gen as Gen +import qualified Hedgehog.Range as Range +import Test.Tasty +import Test.Tasty.Hedgehog + +-- Modules under test +import qualified Data.BitVector.Sized as BV + +-- Auxiliary modules +import qualified Data.ByteString as BS +import Data.Maybe (isJust, fromJust) +import Data.Parameterized.NatRepr +import Data.Parameterized.Some +import Data.Parameterized.Pair +import Data.Word + +---------------------------------------- +-- Utilities +forcePos :: (1 <= w => NatRepr w -> a) + -> NatRepr w -> a +forcePos f w = case isZeroOrGT1 w of + Left Refl -> error "Main.forcePos: encountered 0 nat" + Right LeqProof -> f w + +---------------------------------------- +-- Homomorphisms +un :: Show a + => Gen (Some NatRepr) + -- ^ generator for width + -> (forall w . NatRepr w -> a -> BV.BV w) + -- ^ morphism + -> (forall w . NatRepr w -> Gen a) + -- ^ generator for arg + -> (forall w . NatRepr w -> a -> a) + -- ^ unary operator on domain + -> (forall w . NatRepr w -> BV.BV w -> BV.BV w) + -- ^ unary operator on codomain + -> Property +un genW p gen aOp bOp = property $ do + Some w <- forAll genW + a <- forAll (gen w) + + p w (aOp w a) === bOp w (p w a) + +bin :: Show a + => Gen (Some NatRepr) + -- ^ generator for width + -> (forall w. NatRepr w -> a -> BV.BV w) + -- ^ morphism on domains + -> (forall w. NatRepr w -> Gen a) + -- ^ generator for first arg + -> (forall w. NatRepr w -> Gen a) + -- ^ generator for second arg + -> (forall w. NatRepr w -> a -> a -> a) + -- ^ binary operator on domain + -> (forall w. NatRepr w -> BV.BV w -> BV.BV w -> BV.BV w) + -- ^ binary operator on codomain + -> Property +bin genW p gen1 gen2 aOp bOp = property $ do + Some w <- forAll genW + a1 <- forAll (gen1 w) + a2 <- forAll (gen2 w) + + -- compute f (a1 `aOp` a2) + let a1_a2 = aOp w a1 a2 + let pa1_a2 = p w a1_a2 + + -- compute f (a1) `bOp` f (a2) + let pa1 = p w a1 + let pa2 = p w a2 + let pa1_pa2 = bOp w pa1 pa2 + + pa1_a2 === pa1_pa2 + +binPred :: Show a + => Gen (Some NatRepr) + -- ^ generator for width + -> (forall w. NatRepr w -> a -> BV.BV w) + -- ^ morphism on domains + -> (forall w . NatRepr w -> Gen a) + -- ^ generator for first arg + -> (forall w . NatRepr w -> Gen a) + -- ^ generator for second arg + -> (forall w . NatRepr w -> a -> a -> Bool) + -- ^ binary predicate on domain + -> (forall w . NatRepr w -> BV.BV w -> BV.BV w -> Bool) + -- ^ binary predicate on codomain + -> Property +binPred genW p gen1 gen2 aPred bPred = property $ do + Some w <- forAll genW + a1 <- forAll (gen1 w) + a2 <- forAll (gen2 w) + + let a1_a2 = aPred w a1 a2 + + let pa1 = p w a1 + let pa2 = p w a2 + let pa1_pa2 = bPred w pa1 pa2 + + a1_a2 === pa1_pa2 + +---------------------------------------- +-- Ranges + +anyWidth :: Gen (Some NatRepr) +anyWidth = mkNatRepr <$> (Gen.integral $ Range.linear 0 128) + +byteWidth :: Gen (Some NatRepr) +byteWidth = mkNatRepr <$> (8*) <$> (Gen.integral $ Range.linear 0 16) + +anyPosWidth :: Gen (Some NatRepr) +anyPosWidth = mkNatRepr <$> (Gen.integral $ Range.linear 1 128) + +anyWidthGT1 :: Gen (Some NatRepr) +anyWidthGT1 = mkNatRepr <$> (Gen.integral $ Range.linear 2 128) + +smallPosWidth :: Gen (Some NatRepr) +smallPosWidth = mkNatRepr <$> (Gen.integral $ Range.linear 1 4) + +bytes :: Gen [Word8] +bytes = Gen.list (Range.linear 0 16) $ Gen.word8 Range.linearBounded + +bits :: Gen [Bool] +bits = Gen.list (Range.linear 0 128) $ Gen.bool + +unsigned :: NatRepr w -> Gen Integer +unsigned w = Gen.integral $ Range.linear 0 (maxUnsigned w) + +unsignedPos :: NatRepr w -> Gen Integer +unsignedPos w = Gen.integral $ Range.linear 1 (maxUnsigned w) + +largeUnsigned :: NatRepr w -> Gen Integer +largeUnsigned w = Gen.integral $ Range.linear 0 (maxUnsigned w') + where w' = incNat w + +signed :: NatRepr w -> Gen Integer +signed w = case isZeroOrGT1 w of + Left Refl -> error "Main.signed: w = 0" + Right LeqProof -> Gen.integral $ Range.linearFrom 0 (minSigned w) (maxSigned w) + +signedPos :: NatRepr w -> Gen Integer +signedPos w = case isZeroOrGT1 w of + Left Refl -> error "Main.posBounded: w = 0" + Right LeqProof -> Gen.integral $ Range.linear 1 (maxSigned w) + +signedNeg :: NatRepr w -> Gen Integer +signedNeg w = case isZeroOrGT1 w of + Left Refl -> error "Main.posBounded: w = 0" + Right LeqProof -> Gen.integral $ Range.linearFrom (-1) (minSigned w) (-1) + +largeSigned :: NatRepr w -> Gen Integer +largeSigned w = Gen.integral $ Range.linearFrom 0 (- maxUnsigned w') (maxUnsigned w') + where w' = incNat w + +genPair :: Gen a -> Gen a -> Gen (a, a) +genPair gen gen' = do + a <- gen + a' <- gen' + return (a, a') + +---------------------------------------- +-- Tests + +arithHomTests :: TestTree +arithHomTests = testGroup "arithmetic homomorphisms tests" + [ testProperty "add" $ bin anyWidth BV.mkBV + largeSigned largeSigned + (const (+)) BV.add + , testProperty "sub" $ bin anyWidth BV.mkBV + largeSigned largeSigned + (const (-)) BV.sub + , testProperty "mul" $ bin anyWidth BV.mkBV + largeSigned largeSigned + (const (*)) BV.mul + , testProperty "uquot" $ bin anyPosWidth BV.mkBV + unsigned unsignedPos + (const quot) (const BV.uquot) + , testProperty "urem" $ bin anyPosWidth BV.mkBV + unsigned unsignedPos + (const rem) (const BV.urem) + , testProperty "squot-pos-denom" $ bin anyWidthGT1 BV.mkBV + signed signedPos + (const quot) (forcePos BV.squot) + , testProperty "squot-neg-denom" $ bin anyPosWidth BV.mkBV + signed signedNeg + (const quot) (forcePos BV.squot) + , testProperty "srem-pos-denom" $ bin anyPosWidth BV.mkBV + signed signedPos + (const rem) (forcePos BV.srem) + , testProperty "srem-neg-denom" $ bin anyPosWidth BV.mkBV + signed signedNeg + (const rem) (forcePos BV.srem) + , testProperty "sdiv-pos-denom" $ bin anyPosWidth BV.mkBV + signed signedPos + (const div) (forcePos BV.sdiv) + , testProperty "sdiv-neg-denom" $ bin anyPosWidth BV.mkBV + signed signedNeg + (const div) (forcePos BV.sdiv) + , testProperty "smod-pos-denom" $ bin anyPosWidth BV.mkBV + signed signedPos + (const mod) (forcePos BV.smod) + , testProperty "smod-neg-denom" $ bin anyPosWidth BV.mkBV + signed signedNeg + (const mod) (forcePos BV.smod) + , testProperty "abs" $ un anyPosWidth BV.mkBV + signed + (const abs) (forcePos BV.abs) + , testProperty "negate" $ un anyPosWidth BV.mkBV + largeSigned + (const negate) BV.negate + , testProperty "signBit" $ un anyPosWidth BV.mkBV + signed + (\_ a -> if a < 0 then 1 else 0) (forcePos BV.signBit) + , testProperty "slt" $ binPred anyPosWidth BV.mkBV + signed signed + (const (<)) (forcePos BV.slt) + , testProperty "sle" $ binPred anyPosWidth BV.mkBV + signed signed + (const (<=)) (forcePos BV.sle) + , testProperty "ult" $ binPred anyWidth BV.mkBV + unsigned unsigned + (const (<)) (const BV.ult) + , testProperty "ule" $ binPred anyWidth BV.mkBV + unsigned unsigned + (const (<=)) (const BV.ule) + , testProperty "umin" $ bin anyWidth BV.mkBV + unsigned unsigned + (const min) (const BV.umin) + , testProperty "umax" $ bin anyWidth BV.mkBV + unsigned unsigned + (const max) (const BV.umax) + ] + +serdeTest :: Gen (Some NatRepr) + -> (forall w . NatRepr w -> BV.BV w -> Maybe a) + -> (a -> Pair NatRepr BV.BV) + -> Property +serdeTest wGen ser de = property $ do + Some w <- forAll wGen + i <- forAll (largeUnsigned w) + let bv = BV.mkBV w i + + let a = ser w bv + assert (isJust a) + Pair w' bv' <- return $ de $ fromJust a + + assert (isJust (w' `testEquality` w)) + Just Refl <- return $ w' `testEquality` w + bv' === bv + +deserTest :: (Show a, Eq a) + => Gen a + -> (a -> Int) + -> (a -> Pair NatRepr BV.BV) + -> (forall w . NatRepr w -> BV.BV w -> Maybe a) + -> Property +deserTest genA lenA de ser = property $ do + a <- forAll genA + Some w' <- return $ mkNatRepr (fromIntegral (lenA a)) + + Pair w bv <- return $ de $ a + + assert (isJust (w' `testEquality` w)) + Just Refl <- return $ w' `testEquality` w + + ser w bv === Just a + +serdeTests :: TestTree +serdeTests = testGroup "serialization/deseriallization tests" + [ testProperty "bitsBE" $ + serdeTest anyWidth (\w bv -> Just (BV.asBitsBE w bv)) BV.bitsBE + , testProperty "bitsLE" $ + serdeTest anyWidth (\w bv -> Just (BV.asBitsLE w bv)) BV.bitsLE + , testProperty "bytesBE" $ + serdeTest byteWidth BV.asBytesBE BV.bytesBE + , testProperty "bytesLE" $ + serdeTest byteWidth BV.asBytesLE BV.bytesLE + , testProperty "bytestringBE" $ + serdeTest byteWidth BV.asBytestringBE BV.bytestringBE + , testProperty "bytestringLE" $ + serdeTest byteWidth BV.asBytestringLE BV.bytestringLE + ] + +deserTests :: TestTree +deserTests = testGroup "deserialization/serialization tests" + [ testProperty "asBitsBE" $ + deserTest bits length BV.bitsBE (\w bv -> Just (BV.asBitsBE w bv)) + , testProperty "asBitsLE" $ + deserTest bits length BV.bitsLE (\w bv -> Just (BV.asBitsLE w bv)) + , testProperty "asBytesBE" $ + deserTest bytes ((*8) . length) BV.bytesBE BV.asBytesBE + , testProperty "asBytesLE" $ + deserTest bytes ((*8) . length) BV.bytesLE BV.asBytesLE + , testProperty "asBytesBE" $ + deserTest (BS.pack <$> bytes) ((*8) . BS.length) BV.bytestringBE BV.asBytestringBE + , testProperty "asBytesLE" $ + deserTest (BS.pack <$> bytes) ((*8) . BS.length) BV.bytestringLE BV.asBytestringLE + ] + +tests :: TestTree +tests = testGroup "bv-sized tests" + [ arithHomTests + , serdeTests + , deserTests + ] + +main :: IO () +main = defaultMain tests diff --git a/test/Test.hs b/test/Test.hs deleted file mode 100644 --- a/test/Test.hs +++ /dev/null @@ -1,13 +0,0 @@ -{-# LANGUAGE DataKinds #-} - -module Main where - -import Test.QuickCheck - -import Data.BitVector.Sized - -main :: IO () -main = quickCheck bitVectorTest - -bitVectorTest :: BitVector 64 -> Bool -bitVectorTest bv = bitVector (bvIntegerS bv) == bv