bv-sized 0.7.0 → 1.0.0

raw patch · 13 files changed

+1890/−1185 lines, 13 filesdep +bitwisedep +bytestringdep +hedgehogdep −QuickCheckdep −containersdep −lensdep ~basedep ~parameterized-utilsPVP ok

version bump matches the API change (PVP)

Dependencies added: bitwise, bytestring, hedgehog, panic, tasty, tasty-hedgehog, th-lift

Dependencies removed: QuickCheck, containers, lens, mtl, pretty, random

Dependency ranges changed: base, parameterized-utils

API changes (from Hackage documentation)

Files

• README.md +4/−31
• bv-sized.cabal +28/−25
• changelog.md +41/−11
• src/Data/BitVector/Sized.hs +92/−33
• src/Data/BitVector/Sized/App.hs +0/−369
• src/Data/BitVector/Sized/BitLayout.hs +0/−283
• src/Data/BitVector/Sized/Internal.hs +922/−420
• src/Data/BitVector/Sized/Overflow.hs +216/−0
• src/Data/BitVector/Sized/Panic.hs +20/−0
• src/Data/BitVector/Sized/Signed.hs +128/−0
• src/Data/BitVector/Sized/Unsigned.hs +120/−0
• test/Main.hs +319/−0
• test/Test.hs +0/−13

@@ -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 ===

@@ -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

@@ -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

@@ -9,47 +9,106 @@ Module      : Data.BitVector.Sized Copyright   : (c) Galois Inc. 2018 License     : BSD-3-Maintainer  : benselfridge@galois.com+Maintainer  : Ben Selfridge <benselfridge@galois.com> Stability   : experimental Portability : portable -This module defines a width-parameterized 'BitVector' type and various associated-operations that assume a 2's complement representation.+This module 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 #-}

@@ -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)

@@ -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)

@@ -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<w) constraint+    BV (B.bit (fromNatural (natValue ix)))++-- | Like 'bit', but without the requirement that the index bit refers+-- to an actual bit in the output 'BV'. If it is out of range, just+-- silently return the zero bitvector.+bit' :: NatRepr w+     -- ^ Desired output width+     -> 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) ++ "]"

@@ -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 <benselfridge@galois.com>+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

@@ -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

@@ -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)

@@ -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)

@@ -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

@@ -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