bv-sized 1.0.1 → 1.0.2
raw patch · 5 files changed
+331/−20 lines, 5 filesdep ~tastyPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: tasty
API changes (from Hackage documentation)
Files
- bv-sized.cabal +2/−2
- changelog.md +10/−0
- src/Data/BitVector/Sized.hs +2/−2
- src/Data/BitVector/Sized/Internal.hs +16/−16
- test/Main.hs +301/−0
bv-sized.cabal view
@@ -1,5 +1,5 @@ name: bv-sized-version: 1.0.1+version: 1.0.2 category: Bit Vectors synopsis: a bitvector datatype that is parameterized by the vector width description:@@ -45,7 +45,7 @@ bytestring, hedgehog, parameterized-utils,- tasty >= 1.2.3 && < 1.3,+ tasty >= 1.2.3 && < 1.4, tasty-hedgehog >= 1.0.0.2 && < 1.1 default-language: Haskell2010 ghc-options: -Wall -Wcompat
changelog.md view
@@ -1,5 +1,15 @@ # Changelog for [`bv-sized` package](http://hackage.haskell.org/package/bv-sized) +## 1.0.2 *August 2020*++* Allows tasty 1.3 for test suite+* Fixes bug in signedClamp function which made it possible to violate+ the nonnegative invariant on the internal representation of BVs+* Fixes divide by zero error in rotateL and rotateR+* Enhances test suite to test well-formedness of all operators that+ return a BV+* Fixes some documentation+ ## 1.0.1 *May 2020* This fixed a subtle bug in the test suite which occasionally caused a
src/Data/BitVector/Sized.hs view
@@ -43,6 +43,7 @@ , unsignedClamp, signedClamp , minUnsigned, maxUnsigned , minSigned, maxSigned+ , zero, one, width -- * Construction from fixed-width data types , bool , word8, word16, word32, word64@@ -62,7 +63,6 @@ , and, or, xor , complement , shl, lshr, ashr, rotateL, rotateR- , zero, one, width , bit, bit' , setBit, setBit' , clearBit, clearBit'@@ -108,7 +108,7 @@ import Prelude (Integer) -- | Get the underlying 'Integer' representation from a 'BV'. We--- guarantee that @(\\(BV.BV x) -> x) == BV.toUnsigned@.+-- guarantee that @(\\(BV.BV x) -> x) == BV.asUnsigned@. pattern BV :: Integer -> BV.BV w pattern BV x <- BV.BV x {-# COMPLETE BV #-}
src/Data/BitVector/Sized/Internal.hs view
@@ -178,6 +178,18 @@ -> Maybe (BV w) mkBVSigned w x = checkNatRepr w $ BV <$> signedToUnsigned w x +-- | 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 minimum unsigned value for bitvector with given width (always 0). minUnsigned :: NatRepr w -> BV w minUnsigned w = checkNatRepr w $ BV 0@@ -206,9 +218,9 @@ -- @-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)+ if | x < P.minSigned w -> mkBV' w (P.minSigned w) | x > P.maxSigned w -> BV (P.maxSigned w)- | otherwise -> BV x+ | otherwise -> mkBV' w x ---------------------------------------- -- Construction from fixed-width data types@@ -469,7 +481,7 @@ -- | Bitwise rotate left. rotateL :: NatRepr w -> BV w -> Natural -> BV w rotateL w bv rot' = leftChunk `or` rightChunk- where rot = rot' `mod` wNatural+ where rot = if wNatural == 0 then 0 else rot' `mod` wNatural leftChunk = shl w bv rot rightChunk = lshr w bv (wNatural - rot) wNatural = natValue w@@ -477,22 +489,10 @@ -- | Bitwise rotate right. rotateR :: NatRepr w -> BV w -> Natural -> BV w rotateR w bv rot' = leftChunk `or` rightChunk- where rot = rot' `mod` wNatural+ where rot = if wNatural == 0 then 0 else 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.
test/Main.hs view
@@ -2,6 +2,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} @@ -25,6 +26,7 @@ import Data.Parameterized.Some import Data.Parameterized.Pair import Data.Word+import Numeric.Natural ---------------------------------------- -- Utilities@@ -129,6 +131,43 @@ smallPosWidth :: Gen (Some NatRepr) smallPosWidth = mkNatRepr <$> (Gen.integral $ Range.linear 1 4) +data NatReprLte w where+ NatReprLte :: (i <= w) => NatRepr i -> NatReprLte w++deriving instance Show (NatReprLte w)++natReprLte :: NatRepr w -> Gen (NatReprLte w)+natReprLte w = do+ n <- Gen.integral $ Range.linear 0 (natValue w)+ Some i <- return $ mkNatRepr n+ Just LeqProof <- return $ i `testLeq` w+ return $ NatReprLte i++data NatReprLt w where+ NatReprLt :: (i+1 <= w) => NatRepr i -> NatReprLt w++deriving instance Show (NatReprLt w)++natReprLt :: NatRepr w -> Gen (NatReprLt w)+natReprLt w = do+ n <- Gen.integral $ Range.linear 0 (natValue w - 1)+ Some i <- return $ mkNatRepr n+ NatCaseLT LeqProof <- return $ i `testNatCases` w+ return $ NatReprLt i++data NatReprPosLt w where+ NatReprPosLt :: (1 <= i, i+1 <= w) => NatRepr i -> NatReprPosLt w++deriving instance Show (NatReprPosLt w)++natReprPosLt :: NatRepr w -> Gen (NatReprPosLt w)+natReprPosLt w = do+ n <- Gen.integral $ Range.linear 1 (natValue w - 1)+ Some i <- return $ mkNatRepr n+ NatCaseLT LeqProof <- return $ i `testNatCases` w+ Right LeqProof <- return $ isZeroOrGT1 i+ return $ NatReprPosLt i+ bytes :: Gen [Word8] bytes = Gen.list (Range.linear 0 16) $ Gen.word8 Range.linearBounded @@ -334,12 +373,274 @@ deserTest (BS.pack <$> bytes) ((*8) . BS.length) BV.bytestringLE BV.asBytestringLE ] +checkBounds :: MonadTest m => Integer -> NatRepr w -> m ()+checkBounds x w = do+ diff 0 (<=) x+ diff x (<=) (2 ^ natValue w)++wfCtor :: Gen (Some NatRepr)+ -- ^ generator for width+ -> (forall w . NatRepr w -> Integer -> Maybe (BV.BV w))+ -- ^ constructor+ -> Property+wfCtor genW ctor = property $ do+ Some w <- forAll genW+ x <- forAll (largeSigned w)++ case ctor w x of+ Just (BV.BV x') -> checkBounds x' w+ Nothing -> return ()++wfCtor' :: NatRepr w+ -- ^ fixed width of constructor+ -> (Integer -> BV.BV w)+ -- ^ embedding of integer into constructor arg+ -> Property+wfCtor' w ctor = property $ do+ x <- forAll (largeSigned w)++ let BV.BV x' = ctor x++ checkBounds x' w++wfUnary :: Gen (Some NatRepr)+ -- ^ generator for width+ -> (forall w . NatRepr w -> BV.BV w -> BV.BV w)+ -- ^ unary operator+ -> Property+wfUnary genW op = property $ do+ Some w <- forAll genW+ bv <- BV.mkBV w <$> forAll (unsigned w)++ let BV.BV x' = op w bv+ checkBounds x' w++wfUnaryMaybe :: Gen (Some NatRepr)+ -- ^ generator for width+ -> (forall w . NatRepr w -> BV.BV w -> Maybe (BV.BV w))+ -- ^ unary operator+ -> Property+wfUnaryMaybe genW op = property $ do+ Some w <- forAll genW+ bv <- BV.mkBV w <$> forAll (unsigned w)++ case op w bv of+ Just (BV.BV x') -> checkBounds x' w+ Nothing -> return ()++wfBinary :: Gen (Some NatRepr)+ -- ^ generator for width+ -> (forall w . NatRepr w -> BV.BV w -> BV.BV w -> BV.BV w)+ -- ^ binary operator+ -> Property+wfBinary genW op = property $ do+ Some w <- forAll genW+ bv1 <- BV.mkBV w <$> forAll (unsigned w)+ bv2 <- BV.mkBV w <$> forAll (unsigned w)++ let BV.BV x' = op w bv1 bv2+ checkBounds x' w++wfBinaryDiv :: Gen (Some NatRepr)+ -- ^ generator for width+ -> (forall w . NatRepr w -> BV.BV w -> BV.BV w -> BV.BV w)+ -- ^ binary division-like operator+ -> Property+wfBinaryDiv genW op = property $ do+ Some w <- forAll genW+ bv1 <- BV.mkBV w <$> forAll (unsigned w)+ bv2 <- BV.mkBV w <$> forAll (unsignedPos w)++ let BV.BV x' = op w bv1 bv2+ checkBounds x' w++wfBinaryN :: Gen (Some NatRepr)+ -- ^ generator for width+ -> (forall w . NatRepr w -> BV.BV w -> Natural -> BV.BV w)+ -- ^ binary operator with Natural arg+ -> Property+wfBinaryN genW op = property $ do+ Some w <- forAll genW+ bv <- BV.mkBV w <$> forAll (unsigned w)+ n <- fromInteger <$> forAll (largeUnsigned w)++ let BV.BV x' = op w bv n+ checkBounds x' w++wfBit :: Gen (Some NatRepr)+ -- ^ generator for width+ -> (forall w ix . ix+1 <= w => NatRepr w -> NatRepr ix -> BV.BV w -> BV.BV w)+ -- ^ bit twiddling function+ -> Property+wfBit genW f = property $ do+ Some w <- forAll genW+ bv <- BV.mkBV w <$> forAll (unsigned w)+ NatReprLt ix <- forAll (natReprLt w)++ let BV.BV x = f w ix bv+ checkBounds x w++wfBitN :: Gen (Some NatRepr)+ -- ^ generator for width+ -> (forall w . NatRepr w -> Natural -> BV.BV w -> BV.BV w)+ -- ^ bit twiddling function+ -> Property+wfBitN genW f = property $ do+ Some w <- forAll genW+ bv <- BV.mkBV w <$> forAll (unsigned w)+ n <- fromInteger <$> forAll (largeUnsigned w)++ let BV.BV x = f w n bv+ checkBounds x w++wellFormedTests :: TestTree+wellFormedTests = testGroup "well-formedness tests"+ [ testProperty "mkBV" $ wfCtor anyWidth (fmap Just . BV.mkBV)+ , testProperty "mkBVUnsigned" $ wfCtor anyWidth BV.mkBVUnsigned+ , testProperty "mkBVSigned" $ wfCtor anyPosWidth (forcePos BV.mkBVSigned)+ , testProperty "signedClamp" $ wfCtor anyPosWidth (fmap Just . forcePos BV.signedClamp)+ , testProperty "minUnsigned" $ wfCtor anyWidth (\w _ -> Just (BV.minUnsigned w))+ , testProperty "maxUnsigned" $ wfCtor anyWidth (\w _ -> Just (BV.maxUnsigned w))+ , testProperty "minSigned" $ wfCtor anyPosWidth (\w _ -> Just (forcePos BV.minSigned w))+ , testProperty "maxSigned" $ wfCtor anyPosWidth (\w _ -> Just (forcePos BV.maxSigned w))+ , testProperty "bool" $ wfCtor' knownNat (BV.bool . odd)+ , testProperty "word8" $ wfCtor' knownNat (BV.word8 . fromInteger)+ , testProperty "word16" $ wfCtor' knownNat (BV.word16 . fromInteger)+ , testProperty "word32" $ wfCtor' knownNat (BV.word32 . fromInteger)+ , testProperty "word64" $ wfCtor' knownNat (BV.word64 . fromInteger)+ , testProperty "int8" $ wfCtor' knownNat (BV.int8 . fromInteger)+ , testProperty "int16" $ wfCtor' knownNat (BV.int16 . fromInteger)+ , testProperty "int32" $ wfCtor' knownNat (BV.int32 . fromInteger)+ , testProperty "int64" $ wfCtor' knownNat (BV.int64 . fromInteger)+ , testProperty "and" $ wfBinary anyWidth (const BV.and)+ , testProperty "or" $ wfBinary anyWidth (const BV.or)+ , testProperty "xor" $ wfBinary anyWidth (const BV.xor)+ , testProperty "complement" $ wfUnary anyWidth BV.complement+ , testProperty "shl" $ wfBinaryN anyWidth BV.shl+ , testProperty "ashr" $ wfBinaryN anyPosWidth (forcePos BV.ashr)+ , testProperty "lshr" $ wfBinaryN anyWidth BV.lshr+ , testProperty "rotateL" $ wfBinaryN anyWidth BV.rotateL+ , testProperty "rotateR" $ wfBinaryN anyWidth BV.rotateR+ , testProperty "bit" $ property $ do+ Some w <- forAll anyPosWidth+ NatReprLt i <- forAll (natReprLt w)++ let BV.BV x = BV.bit w i+ checkBounds x w+ , testProperty "bit'" $ property $ do+ Some w <- forAll anyPosWidth+ n <- forAll $ Gen.integral $ Range.linear 0 (2 * natValue w)++ let BV.BV x = BV.bit' w n+ checkBounds x w+ , testProperty "setBit" $ wfBit anyPosWidth (const BV.setBit)+ , testProperty "setBit'" $ wfBitN anyPosWidth BV.setBit'+ , testProperty "clearBit" $ wfBit anyPosWidth BV.clearBit+ , testProperty "clearBit'" $ wfBitN anyPosWidth BV.clearBit'+ , testProperty "complementBit" $ wfBit anyPosWidth (const BV.complementBit)+ , testProperty "complementBit'" $ wfBitN anyPosWidth BV.complementBit'+ , testProperty "popCount" $ wfUnary anyWidth (const BV.popCount)+ , testProperty "ctz" $ wfUnary anyWidth BV.ctz+ , testProperty "clz" $ wfUnary anyWidth BV.clz+ , testProperty "truncBits" $ property $ do+ Some w <- forAll anyWidth+ bv <- BV.mkBV w <$> forAll (unsigned w)+ n <- forAll $ Gen.integral $ Range.linear 0 (2 * natValue w)++ let BV.BV x = BV.truncBits n bv+ checkBounds x w+ , testProperty "add" $ wfBinary anyWidth BV.add+ , testProperty "sub" $ wfBinary anyWidth BV.sub+ , testProperty "mul" $ wfBinary anyWidth BV.mul+ , testProperty "uquot" $ wfBinaryDiv anyPosWidth (const BV.uquot)+ , testProperty "urem" $ wfBinaryDiv anyPosWidth (const BV.urem)+ , testProperty "squot" $ wfBinaryDiv anyPosWidth (forcePos BV.squot)+ , testProperty "srem" $ wfBinaryDiv anyPosWidth (forcePos BV.srem)+ , testProperty "sdiv" $ wfBinaryDiv anyPosWidth (forcePos BV.sdiv)+ , testProperty "smod" $ wfBinaryDiv anyPosWidth (forcePos BV.smod)+ , testProperty "abs" $ wfUnary anyPosWidth (forcePos BV.abs)+ , testProperty "negate" $ wfUnary anyWidth BV.negate+ , testProperty "signBit" $ wfUnary anyPosWidth (forcePos BV.signBit)+ , testProperty "signum" $ wfUnary anyPosWidth (forcePos BV.signum)+ , testProperty "umin" $ wfBinary anyWidth (const BV.umin)+ , testProperty "umax" $ wfBinary anyWidth (const BV.umax)+ , testProperty "smin" $ wfBinary anyPosWidth (forcePos BV.smin)+ , testProperty "smax" $ wfBinary anyPosWidth (forcePos BV.smax)+ , testProperty "concat" $ property $ do+ Some w <- forAll anyWidth+ Some w' <- forAll anyWidth+ bv <- BV.mkBV w <$> forAll (unsigned w)+ bv' <- BV.mkBV w' <$> forAll (unsigned w')++ let BV.BV x = BV.concat w w' bv bv'+ checkBounds x (w `addNat` w')+ , testProperty "select" $ property $ do+ Some w <- forAll anyWidth+ bv <- BV.mkBV w <$> forAll (unsigned w)+ NatReprLte ix <- forAll (natReprLte w)+ Just LeqProof <- return $ ix `testLeq` w+ NatReprLte w' <- forAll (natReprLte (w `subNat` ix))+ Just LeqProof <- return $ (ix `addNat` w') `testLeq` w++ let BV.BV x = BV.select ix w' bv+ checkBounds x w'+ , testProperty "select'" $ property $ do+ Some w <- forAll anyWidth+ Some w' <- forAll anyWidth+ bv <- BV.mkBV w <$> forAll (unsigned w)+ n <- forAll $ Gen.integral $ Range.linear 0 (2 * natValue w)++ let BV.BV x = BV.select' n w' bv+ checkBounds x w'+ , testProperty "zext" $ property $ do+ Some w' <- forAll anyPosWidth+ NatReprLt w <- forAll (natReprLt w')+ bv <- BV.mkBV w <$> forAll (unsigned w)++ let BV.BV x = BV.zext w' bv+ checkBounds x w'+ , testProperty "sext" $ property $ do+ Some w' <- forAll anyWidthGT1+ NatReprPosLt w <- forAll (natReprPosLt w')+ bv <- BV.mkBV w <$> forAll (unsigned w)++ let BV.BV x = BV.sext w w' bv+ checkBounds x w'+ , testProperty "trunc" $ property $ do+ Some w <- forAll anyPosWidth+ NatReprLt w' <- forAll (natReprLt w)+ bv <- BV.mkBV w <$> forAll (unsigned w)++ let BV.BV x = BV.trunc w' bv+ checkBounds x w'+ , testProperty "trunc'" $ property $ do+ Some w <- forAll anyWidth+ Some w' <- forAll anyWidth+ bv <- BV.mkBV w <$> forAll (unsigned w)++ let BV.BV x = BV.trunc' w' bv+ checkBounds x w'+ , testProperty "mulWide" $ property $ do+ Some w <- forAll anyWidth+ Some w' <- forAll anyWidth+ bv <- BV.mkBV w <$> forAll (unsigned w)+ bv' <- BV.mkBV w' <$> forAll (unsigned w')++ let BV.BV x = BV.mulWide w w' bv bv'+ checkBounds x (w `addNat` w')+ , testProperty "succUnsigned" $ wfUnaryMaybe anyWidth BV.succUnsigned+ , testProperty "succSigned" $ wfUnaryMaybe anyPosWidth (forcePos BV.succUnsigned)+ , testProperty "predUnsigned" $ wfUnaryMaybe anyWidth BV.predUnsigned+ , testProperty "predSigned" $ wfUnaryMaybe anyPosWidth (forcePos BV.predUnsigned)+ ]+ tests :: TestTree tests = testGroup "bv-sized tests" [ arithHomTests , bitwiseHomTests , serdeTests , deserTests+ , wellFormedTests ] main :: IO ()