1{-# LANGUAGE BangPatterns #-} 2{-# LANGUAGE DataKinds #-} 3{-# LANGUAGE DeriveGeneric #-} 4{-# LANGUAGE DeriveLift #-} 5{-# LANGUAGE GADTs #-} 6{-# LANGUAGE KindSignatures #-} 7{-# LANGUAGE MultiWayIf #-} 8{-# LANGUAGE PatternSynonyms #-} 9{-# LANGUAGE ScopedTypeVariables #-} 10{-# LANGUAGE TemplateHaskell #-} 11{-# LANGUAGE TypeApplications #-} 12{-# LANGUAGE TypeOperators #-} 13 14{-| 15Module : Data.BitVector.Sized.Internal 16Copyright : (c) Galois Inc. 2018 17License : BSD-3 18Maintainer : benselfridge@galois.com 19Stability : experimental 20Portability : portable 21 22Internal hidden module containing all definitions for the 'BV' type. 23-} 24 25module Data.BitVector.Sized.Internal where 26 27import Data.BitVector.Sized.Panic (panic) 28 29-- Qualified imports 30import qualified Data.Bits as B 31import qualified Data.Bits.Bitwise as B 32import qualified Data.ByteString as BS 33import qualified Numeric as N 34import qualified Data.Parameterized.NatRepr as P 35import qualified Prelude as Prelude 36 37-- Unqualified imports 38import Data.Char (intToDigit) 39import Data.List (genericLength) 40import Data.Int 41import Data.Kind (Type) 42import Data.Maybe (fromJust) 43import Data.Word 44import Data.Parameterized ( NatRepr 45 , mkNatRepr 46 , natValue 47 , intValue 48 , addNat 49 , ShowF 50 , EqF(..) 51 , Hashable(..) 52 , Some(..) 53 , Pair(..) 54 ) 55import GHC.Generics 56import GHC.TypeLits 57import Language.Haskell.TH.Lift (Lift) 58import Numeric.Natural 59import Prelude hiding (abs, or, and, negate, concat, signum) 60 61---------------------------------------- 62-- Utility functions 63 64-- | Check that a 'NatRepr' is representable as an 'Int'. 65checkNatRepr :: NatRepr w -> a -> a 66checkNatRepr = checkNatural . natValue 67 68-- | Check that a 'Natural' is representable as an 'Int'. 69checkNatural :: Natural -> a -> a 70checkNatural n a = if n > (fromIntegral (maxBound :: Int) :: Natural) 71 then panic "Data.BitVector.Sized.Internal.checkNatural" 72 [show n ++ " not representable as Int"] 73 else a 74 75 76-- | Unsafe coercion from @Natural@ to @Int@. We mostly use this to 77-- interact with operations from "Data.Bits". This should only be 78-- called when we already know the input @Natural@ is small enough, 79-- e.g., because we previously called @checkNatural@. 80fromNatural :: Natural -> Int 81fromNatural = fromIntegral 82 83---------------------------------------- 84-- BitVector data type definitions 85 86-- | Bitvector datatype, parameterized by width. 87data BV (w :: Nat) :: Type where 88 -- | We store the value as an 'Integer' rather than a 'Natural', 89 -- since many of the operations on bitvectors rely on a two's 90 -- complement representation. However, an invariant on the value is 91 -- that it must always be positive. 92 -- 93 -- Secondly, we maintain the invariant that any constructed BV value 94 -- has a width whose value is representable in a Haskell @Int@. 95 BV :: Integer -> BV w 96 97 deriving ( Generic 98 , Show 99 , Read 100 , Eq 101 , Ord -- ^ Uses an unsigned ordering, but 'ule' and 'ult' are 102 -- preferred. We provide this instance to allow the use of 'BV' 103 -- in situations where an arbitrary ordering is required (e.g., 104 -- as the keys in a map) 105 , Lift) 106 107instance ShowF BV 108 109instance EqF BV where 110 BV bv `eqF` BV bv' = bv == bv' 111 112instance Hashable (BV w) where 113 hashWithSalt salt (BV i) = hashWithSalt salt i 114 115---------------------------------------- 116-- BV construction 117-- | Internal function for masking the input integer *without* 118-- checking that the width is representable as an 'Int'. We use this 119-- instead of 'mkBV' whenever we already have some guarantee that the 120-- width is legal. 121mkBV' :: NatRepr w -> Integer -> BV w 122mkBV' w x = BV (P.toUnsigned w x) 123 124-- | Construct a bitvector with a particular width, where the width is 125-- provided as an explicit `NatRepr` argument. The input 'Integer', 126-- whether positive or negative, is silently truncated to fit into the 127-- number of bits demanded by the return type. The width cannot be 128-- arbitrarily large; it must be representable as an 'Int'. 129-- 130-- >>> mkBV (knownNat @4) 10 131-- BV 10 132-- >>> mkBV (knownNat @2) 10 133-- BV 2 134-- >>> mkBV (knownNat @4) (-2) 135-- BV 14 136mkBV :: NatRepr w 137 -- ^ Desired bitvector width 138 -> Integer 139 -- ^ Integer value to truncate to bitvector width 140 -> BV w 141mkBV w x = checkNatRepr w $ mkBV' w x 142 143-- | Return 'Nothing' if the unsigned 'Integer' does not fit in the 144-- required number of bits, otherwise return the input. 145checkUnsigned :: NatRepr w 146 -> Integer 147 -> Maybe Integer 148checkUnsigned w i = if i < 0 || i > P.maxUnsigned w 149 then Nothing 150 else Just i 151 152-- | Like 'mkBV', but returns 'Nothing' if unsigned input integer cannot be 153-- represented in @w@ bits. 154mkBVUnsigned :: NatRepr w 155 -- ^ Desired bitvector width 156 -> Integer 157 -- ^ Integer value 158 -> Maybe (BV w) 159mkBVUnsigned w x = checkNatRepr w $ BV <$> checkUnsigned w x 160 161-- | Return 'Nothing if the signed 'Integer' does not fit in the 162-- required number of bits, otherwise return an unsigned positive 163-- integer that fits in @w@ bits. 164signedToUnsigned :: 1 <= w => NatRepr w 165 -- ^ Width of output 166 -> Integer 167 -> Maybe Integer 168signedToUnsigned w i = if i < P.minSigned w || i > P.maxSigned w 169 then Nothing 170 else Just $ if i < 0 then i + P.maxUnsigned w + 1 else i 171 172-- | Like 'mkBV', but returns 'Nothing' if signed input integer cannot 173-- be represented in @w@ bits. 174mkBVSigned :: 1 <= w => NatRepr w 175 -- ^ Desired bitvector width 176 -> Integer 177 -- ^ Integer value 178 -> Maybe (BV w) 179mkBVSigned w x = checkNatRepr w $ BV <$> signedToUnsigned w x 180 181-- | The zero bitvector of any width. 182zero :: NatRepr w -> BV w 183zero w = checkNatRepr w $ BV 0 184 185-- | The bitvector with value 1, of any positive width. 186one :: 1 <= w => NatRepr w -> BV w 187one w = checkNatRepr w $ BV 1 188 189-- | The bitvector whose value is its own width, of any width. 190width :: NatRepr w -> BV w 191width w = checkNatRepr w $ BV (intValue w) 192 193-- | The minimum unsigned value for bitvector with given width (always 0). 194minUnsigned :: NatRepr w -> BV w 195minUnsigned w = checkNatRepr w $ BV 0 196 197-- | The maximum unsigned value for bitvector with given width. 198maxUnsigned :: NatRepr w -> BV w 199maxUnsigned w = checkNatRepr w $ BV (P.maxUnsigned w) 200 201-- | The minimum value for bitvector in two's complement with given width. 202minSigned :: 1 <= w => NatRepr w -> BV w 203minSigned w = mkBV w (P.minSigned w) 204 205-- | The maximum value for bitvector in two's complement with given width. 206maxSigned :: 1 <= w => NatRepr w -> BV w 207maxSigned w = checkNatRepr w $ BV (P.maxSigned w) 208 209-- | @unsignedClamp w i@ rounds @i@ to the nearest value between @0@ 210-- and @2^w - 1@ (inclusive). 211unsignedClamp :: NatRepr w -> Integer -> BV w 212unsignedClamp w x = checkNatRepr w $ 213 if | x < P.minUnsigned w -> BV (P.minUnsigned w) 214 | x > P.maxUnsigned w -> BV (P.maxUnsigned w) 215 | otherwise -> BV x 216 217-- | @signedClamp w i@ rounds @i@ to the nearest value between 218-- @-2^(w-1)@ and @2^(w-1) - 1@ (inclusive). 219signedClamp :: 1 <= w => NatRepr w -> Integer -> BV w 220signedClamp w x = checkNatRepr w $ 221 if | x < P.minSigned w -> mkBV' w (P.minSigned w) 222 | x > P.maxSigned w -> BV (P.maxSigned w) 223 | otherwise -> mkBV' w x 224 225---------------------------------------- 226-- Construction from fixed-width data types 227 228-- | Construct a 'BV' from a 'Bool'. 229bool :: Bool -> BV 1 230bool True = BV 1 231bool False = BV 0 232 233-- | Construct a 'BV' from a 'Word8'. 234word8 :: Word8 -> BV 8 235word8 = BV . toInteger 236 237-- | Construct a 'BV' from a 'Word16'. 238word16 :: Word16 -> BV 16 239word16 = BV . toInteger 240 241-- | Construct a 'BV' from a 'Word32'. 242word32 :: Word32 -> BV 32 243word32 = BV . toInteger 244 245-- | Construct a 'BV' from a 'Word64'. 246word64 :: Word64 -> BV 64 247word64 = BV . toInteger 248 249-- | Construct a 'BV' from an 'Int8'. 250int8 :: Int8 -> BV 8 251int8 = word8 . (fromIntegral :: Int8 -> Word8) 252 253-- | Construct a 'BV' from an 'Int16'. 254int16 :: Int16 -> BV 16 255int16 = word16 . (fromIntegral :: Int16 -> Word16) 256 257-- | Construct a 'BV' from an 'Int32'. 258int32 :: Int32 -> BV 32 259int32 = word32 . (fromIntegral :: Int32 -> Word32) 260 261-- | Construct a 'BV' from an 'Int64'. 262int64 :: Int64 -> BV 64 263int64 = word64 . (fromIntegral :: Int64 -> Word64) 264 265-- | Construct a 'BV' from a list of bits, in big endian order (bits 266-- with lower value index in the list are mapped to higher order bits 267-- in the output bitvector). Return the resulting 'BV' along with its 268-- width. 269-- 270-- >>> case bitsBE [True, False] of p -> (fstPair p, sndPair p) 271-- (2,BV 2) 272bitsBE :: [Bool] -> Pair NatRepr BV 273bitsBE bs = case mkNatRepr (fromInteger (genericLength bs)) of 274 Some w -> checkNatRepr w $ Pair w (BV (B.fromListBE bs)) 275 276-- | Construct a 'BV' from a list of bits, in little endian order 277-- (bits with lower value index in the list are mapped to lower order 278-- bits in the output bitvector). Return the resulting 'BV' along 279-- with its width. 280-- 281-- >>> case bitsLE [True, False] of p -> (fstPair p, sndPair p) 282-- (2,BV 1) 283bitsLE :: [Bool] -> Pair NatRepr BV 284bitsLE bs = case mkNatRepr (fromInteger (genericLength bs)) of 285 Some w -> checkNatRepr w $ Pair w (BV (B.fromListLE bs)) 286 287-- | Convert a 'ByteString' (big-endian) of length @n@ to an 'Integer' 288-- with @8*n@ bits. This function uses a balanced binary fold to 289-- achieve /O(n log n)/ total memory allocation and run-time, in 290-- contrast to the /O(n^2)/ that would be required by a naive 291-- left-fold. 292bytestringToIntegerBE :: BS.ByteString -> Integer 293bytestringToIntegerBE bs 294 | l == 0 = 0 295 | l == 1 = toInteger (BS.head bs) 296 | otherwise = x1 `B.shiftL` (l2 * 8) B..|. x2 297 where 298 l = BS.length bs 299 l1 = l `div` 2 300 l2 = l - l1 301 (bs1, bs2) = BS.splitAt l1 bs 302 x1 = bytestringToIntegerBE bs1 303 x2 = bytestringToIntegerBE bs2 304 305bytestringToIntegerLE :: BS.ByteString -> Integer 306bytestringToIntegerLE bs 307 | l == 0 = 0 308 | l == 1 = toInteger (BS.head bs) 309 | otherwise = x2 `B.shiftL` (l1 * 8) B..|. x1 310 where 311 l = BS.length bs 312 l1 = l `div` 2 313 (bs1, bs2) = BS.splitAt l1 bs 314 x1 = bytestringToIntegerLE bs1 315 x2 = bytestringToIntegerLE bs2 316 317-- | Construct a 'BV' from a big-endian bytestring. 318-- 319-- >>> case bytestringBE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p) 320-- (24,BV 257) 321bytestringBE :: BS.ByteString -> Pair NatRepr BV 322bytestringBE bs = case mkNatRepr (8*fromIntegral (BS.length bs)) of 323 Some w -> checkNatRepr w $ Pair w (BV (bytestringToIntegerBE bs)) 324 325-- | Construct a 'BV' from a little-endian bytestring. 326-- 327-- >>> case bytestringLE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p) 328-- (24,BV 65792) 329bytestringLE :: BS.ByteString -> Pair NatRepr BV 330bytestringLE bs = case mkNatRepr (8*fromIntegral (BS.length bs)) of 331 Some w -> checkNatRepr w $ Pair w (BV (bytestringToIntegerLE bs)) 332 333-- | Construct a 'BV' from a list of bytes, in big endian order (bytes 334-- with lower value index in the list are mapped to higher order bytes 335-- in the output bitvector). 336-- 337-- >>> case bytesBE [0, 1, 1] of p -> (fstPair p, sndPair p) 338-- (24,BV 257) 339bytesBE :: [Word8] -> Pair NatRepr BV 340bytesBE = bytestringBE . BS.pack 341 342-- | Construct a 'BV' from a list of bytes, in little endian order 343-- (bytes with lower value index in the list are mapped to lower 344-- order bytes in the output bitvector). 345-- 346-- >>> case bytesLE [0, 1, 1] of p -> (fstPair p, sndPair p) 347-- (24,BV 65792) 348bytesLE :: [Word8] -> Pair NatRepr BV 349bytesLE = bytestringLE . BS.pack 350 351---------------------------------------- 352-- BitVector -> Integer functions 353 354-- | Unsigned interpretation of a bitvector as a positive Integer. 355asUnsigned :: BV w -> Integer 356asUnsigned (BV x) = x 357 358-- | Signed interpretation of a bitvector as an Integer. 359asSigned :: (1 <= w) => NatRepr w -> BV w -> Integer 360asSigned w (BV x) = 361 -- NB, fromNatural is OK here because we maintain the invariant that 362 -- any existing BV value has a representable width 363 let wInt = fromNatural (natValue w) in 364 if B.testBit x (wInt - 1) 365 then x - B.bit wInt 366 else x 367 368-- | Unsigned interpretation of a bitvector as a Natural. 369asNatural :: BV w -> Natural 370asNatural = (fromInteger :: Integer -> Natural) . asUnsigned 371 372-- | Convert a bitvector to a list of bits, in big endian order 373-- (higher order bits in the bitvector are mapped to lower indices in 374-- the output list). 375-- 376-- >>> asBitsBE (knownNat @5) (mkBV knownNat 0b1101) 377-- [False,True,True,False,True] 378asBitsBE :: NatRepr w -> BV w -> [Bool] 379asBitsBE w bv = [ testBit' i bv | i <- fromInteger <$> [wi - 1, wi - 2 .. 0] ] 380 where wi = intValue w 381 382-- | Convert a bitvector to a list of bits, in little endian order 383-- (lower order bits in the bitvector are mapped to lower indices in 384-- the output list). 385-- 386-- >>> asBitsLE (knownNat @5) (mkBV knownNat 0b1101) 387-- [True,False,True,True,False] 388asBitsLE :: NatRepr w -> BV w -> [Bool] 389asBitsLE w bv = [ testBit' i bv | i <- fromInteger <$> [0 .. wi - 1] ] 390 where wi = intValue w 391 392integerToBytesBE :: Natural 393 -- ^ number of bytes 394 -> Integer 395 -> [Word8] 396integerToBytesBE n x = 397 [ fromIntegral (x `B.shiftR` (8*ix)) | ix <- [ni-1, ni-2 .. 0] ] 398 where ni = fromIntegral n 399 400integerToBytesLE :: Natural 401 -- ^ number of bytes 402 -> Integer 403 -> [Word8] 404integerToBytesLE n x = 405 [ fromIntegral (x `B.shiftR` (8*ix)) | ix <- [0 .. ni-1] ] 406 where ni = fromIntegral n 407 408-- | Convert a bitvector to a list of bytes, in big endian order 409-- (higher order bytes in the bitvector are mapped to lower indices in 410-- the output list). Return 'Nothing' if the width is not a multiple 411-- of 8. 412-- 413-- >>> asBytesBE (knownNat @32) (mkBV knownNat 0xaabbccdd) 414-- Just [170,187,204,221] 415asBytesBE :: NatRepr w -> BV w -> Maybe [Word8] 416asBytesBE w (BV x) 417 | natValue w `mod` 8 == 0 = Just $ integerToBytesBE (natValue w `div` 8) x 418 | otherwise = Nothing 419 420-- | Convert a bitvector to a list of bytes, in little endian order 421-- (lower order bytes in the bitvector are mapped to lower indices in 422-- the output list). Return 'Nothing' if the width is not a multiple 423-- of 8. 424-- 425-- >>> asBytesLE (knownNat @32) (mkBV knownNat 0xaabbccdd) 426-- Just [221,204,187,170] 427asBytesLE :: NatRepr w -> BV w -> Maybe [Word8] 428asBytesLE w (BV x) 429 | natValue w `mod` 8 == 0 = Just $ integerToBytesLE (natValue w `div` 8) x 430 | otherwise = Nothing 431 432-- | 'asBytesBE', but for bytestrings. 433asBytestringBE :: NatRepr w -> BV w -> Maybe BS.ByteString 434asBytestringBE w bv = BS.pack <$> asBytesBE w bv 435 436-- | 'asBytesLE', but for bytestrings. 437asBytestringLE :: NatRepr w -> BV w -> Maybe BS.ByteString 438asBytestringLE w bv = BS.pack <$> asBytesLE w bv 439 440---------------------------------------- 441-- BV w operations (fixed width) 442 443-- | Bitwise and. 444and :: BV w -> BV w -> BV w 445and (BV x) (BV y) = BV (x B..&. y) 446 447-- | Bitwise or. 448or :: BV w -> BV w -> BV w 449or (BV x) (BV y) = BV (x B..|. y) 450 451-- | Bitwise xor. 452xor :: BV w -> BV w -> BV w 453xor (BV x) (BV y) = BV (x `B.xor` y) 454 455-- | Bitwise complement (flip every bit). 456complement :: NatRepr w -> BV w -> BV w 457complement w (BV x) = mkBV' w (B.complement x) 458 459 460-- | Clamp shift amounts to the word width and 461-- coerce to an @Int@ 462shiftAmount :: NatRepr w -> Natural -> Int 463shiftAmount w shf = fromNatural (min (natValue w) shf) 464 465-- | Left shift by positive 'Natural'. 466shl :: NatRepr w -> BV w -> Natural -> BV w 467shl w (BV x) shf = mkBV' w (x `B.shiftL` shiftAmount w shf) 468 469-- | Right arithmetic shift by positive 'Natural'. 470ashr :: (1 <= w) => NatRepr w -> BV w -> Natural -> BV w 471ashr w bv shf = mkBV' w (asSigned w bv `B.shiftR` shiftAmount w shf) 472 473-- | Right logical shift by positive 'Natural'. 474lshr :: NatRepr w -> BV w -> Natural -> BV w 475lshr w (BV x) shf = 476 -- Shift right (logical by default since the value is positive). No 477 -- need to truncate bits, since the result is guaranteed to occupy 478 -- no more bits than the input. 479 BV (x `B.shiftR` shiftAmount w shf) 480 481-- | Bitwise rotate left. 482rotateL :: NatRepr w -> BV w -> Natural -> BV w 483rotateL w bv rot' = leftChunk `or` rightChunk 484 where rot = if wNatural == 0 then 0 else rot' `mod` wNatural 485 leftChunk = shl w bv rot 486 rightChunk = lshr w bv (wNatural - rot) 487 wNatural = natValue w 488 489-- | Bitwise rotate right. 490rotateR :: NatRepr w -> BV w -> Natural -> BV w 491rotateR w bv rot' = leftChunk `or` rightChunk 492 where rot = if wNatural == 0 then 0 else rot' `mod` wNatural 493 rightChunk = lshr w bv rot 494 leftChunk = shl w bv (wNatural - rot) 495 wNatural = natValue w 496 497-- | The 'BV' that has a particular bit set, and is 0 everywhere 498-- else. 499bit :: ix+1 <= w 500 => NatRepr w 501 -- ^ Desired output width 502 -> NatRepr ix 503 -- ^ Index of bit to set 504 -> BV w 505bit w ix = 506 checkNatRepr w $ 507 -- NB fromNatural is OK here because of the (ix+1<w) constraint 508 BV (B.bit (fromNatural (natValue ix))) 509 510-- | Like 'bit', but without the requirement that the index bit refers 511-- to an actual bit in the output 'BV'. If it is out of range, just 512-- silently return the zero bitvector. 513bit' :: NatRepr w 514 -- ^ Desired output width 515 -> Natural 516 -- ^ Index of bit to set 517 -> BV w 518bit' w ix 519 | ix < natValue w = checkNatRepr w $ mkBV' w (B.bit (fromNatural ix)) 520 | otherwise = zero w 521 522-- | @setBit bv ix@ is the same as @or bv (bit knownNat ix)@. 523setBit :: ix+1 <= w 524 => NatRepr ix 525 -- ^ Index of bit to set 526 -> BV w 527 -- ^ Original bitvector 528 -> BV w 529setBit ix bv = 530 -- NB, fromNatural is OK because of the (ix+1 <= w) constraint 531 or bv (BV (B.bit (fromNatural (natValue ix)))) 532 533-- | Like 'setBit', but without the requirement that the index bit 534-- refers to an actual bit in the input 'BV'. If it is out of range, 535-- just silently return the original input. 536setBit' :: NatRepr w 537 -- ^ Desired output width 538 -> Natural 539 -- ^ Index of bit to set 540 -> BV w 541 -- ^ Original bitvector 542 -> BV w 543setBit' w ix bv 544 | ix < natValue w = or bv (BV (B.bit (fromNatural ix))) 545 | otherwise = bv 546 547-- | @clearBit w bv ix@ is the same as @and bv (complement (bit w ix))@. 548clearBit :: ix+1 <= w 549 => NatRepr w 550 -- ^ Desired output width 551 -> NatRepr ix 552 -- ^ Index of bit to clear 553 -> BV w 554 -- ^ Original bitvector 555 -> BV w 556clearBit w ix bv = 557 -- NB, fromNatural is OK because of the (ix+1<=w) constraint 558 and bv (complement w (BV (B.bit (fromNatural (natValue ix))))) 559 560 561-- | Like 'clearBit', but without the requirement that the index bit 562-- refers to an actual bit in the input 'BV'. If it is out of range, 563-- just silently return the original input. 564clearBit' :: NatRepr w 565 -- ^ Desired output width 566 -> Natural 567 -- ^ Index of bit to clear 568 -> BV w 569 -- ^ Original bitvector 570 -> BV w 571clearBit' w ix bv 572 | ix < natValue w = and bv (complement w (BV (B.bit (fromNatural ix)))) 573 | otherwise = bv 574 575-- | @complementBit bv ix@ is the same as @xor bv (bit knownNat ix)@. 576complementBit :: ix+1 <= w 577 => NatRepr ix 578 -- ^ Index of bit to flip 579 -> BV w 580 -- ^ Original bitvector 581 -> BV w 582complementBit ix bv = 583 -- NB, fromNatural is OK because of (ix+1 <= w) constraint 584 xor bv (BV (B.bit (fromNatural (natValue ix)))) 585 586-- | Like 'complementBit', but without the requirement that the index 587-- bit refers to an actual bit in the input 'BV'. If it is out of 588-- range, just silently return the original input. 589complementBit' :: NatRepr w 590 -- ^ Desired output width 591 -> Natural 592 -- ^ Index of bit to flip 593 -> BV w 594 -- ^ Original bitvector 595 -> BV w 596complementBit' w ix bv 597 | ix < natValue w = xor bv (BV (B.bit (fromNatural ix))) 598 | otherwise = bv 599 600-- | Test if a particular bit is set. 601testBit :: ix+1 <= w => NatRepr ix -> BV w -> Bool 602testBit ix (BV x) = B.testBit x (fromNatural (natValue ix)) 603 604-- | Like 'testBit', but takes a 'Natural' for the bit index. If the 605-- index is out of bounds, return 'False'. 606testBit' :: Natural -> BV w -> Bool 607testBit' ix (BV x) 608 -- NB, If the index is larger than the maximum representable 'Int', 609 -- this function should be 'False' by construction of 'BV'. 610 | ix > fromIntegral (maxBound :: Int) = False 611 | otherwise = B.testBit x (fromNatural ix) 612 613-- | Get the number of 1 bits in a 'BV'. 614popCount :: BV w -> BV w 615popCount (BV x) = BV (toInteger (B.popCount x)) 616 617-- | Count trailing zeros in a 'BV'. 618ctz :: NatRepr w -> BV w -> BV w 619ctz w (BV x) = BV (go 0) 620 where go !i | i < intValue w && 621 B.testBit x (fromInteger i) == False = go (i+1) 622 | otherwise = i 623 624-- | Count leading zeros in a 'BV'. 625clz :: NatRepr w -> BV w -> BV w 626clz w (BV x) = BV (go 0) 627 where go !i | i < intValue w && 628 B.testBit x (fromInteger (intValue w - i - 1)) == False = 629 go (i+1) 630 | otherwise = i 631 632-- | Truncate a bitvector to a particular width given at runtime, 633-- while keeping the type-level width constant. 634truncBits :: Natural -> BV w -> BV w 635truncBits b (BV x) = checkNatural b $ BV (x B..&. (B.bit (fromNatural b) - 1)) 636 637---------------------------------------- 638-- BV w arithmetic operations (fixed width) 639 640-- | Bitvector add. 641add :: NatRepr w -> BV w -> BV w -> BV w 642add w (BV x) (BV y) = mkBV' w (x+y) 643 644-- | Bitvector subtract. 645sub :: NatRepr w -> BV w -> BV w -> BV w 646sub w (BV x) (BV y) = mkBV' w (x-y) 647 648-- | Bitvector multiply. 649mul :: NatRepr w -> BV w -> BV w -> BV w 650mul w (BV x) (BV y) = mkBV' w (x*y) 651 652-- | Bitvector division (unsigned). Rounds to zero. Division by zero 653-- yields a runtime error. 654uquot :: BV w -> BV w -> BV w 655uquot (BV x) (BV y) = BV (x `quot` y) 656 657-- | Bitvector remainder after division (unsigned), when rounded to 658-- zero. Division by zero yields a runtime error. 659urem :: BV w -> BV w -> BV w 660urem (BV x) (BV y) = BV (x `rem` y) 661 662-- | 'uquot' and 'urem' returned as a pair. 663uquotRem :: BV w -> BV w -> (BV w, BV w) 664uquotRem bv1 bv2 = (uquot bv1 bv2, urem bv1 bv2) 665 666-- | Bitvector division (signed). Rounds to zero. Division by zero 667-- yields a runtime error. 668squot :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w 669squot w bv1 bv2 = mkBV' w (x `quot` y) 670 where x = asSigned w bv1 671 y = asSigned w bv2 672 673-- | Bitvector remainder after division (signed), when rounded to 674-- zero. Division by zero yields a runtime error. 675srem :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w 676srem w bv1 bv2 = mkBV' w (x `rem` y) 677 where x = asSigned w bv1 678 y = asSigned w bv2 679 680-- | 'squot' and 'srem' returned as a pair. 681squotRem :: (1 <= w) => NatRepr w -> BV w -> BV w -> (BV w, BV w) 682squotRem w bv1 bv2 = (squot w bv1 bv2, srem w bv1 bv2) 683 684-- | Bitvector division (signed). Rounds to negative infinity. Division 685-- by zero yields a runtime error. 686sdiv :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w 687sdiv w bv1 bv2 = mkBV' w (x `div` y) 688 where x = asSigned w bv1 689 y = asSigned w bv2 690 691-- | Bitvector remainder after division (signed), when rounded to 692-- negative infinity. Division by zero yields a runtime error. 693smod :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w 694smod w bv1 bv2 = mkBV' w (x `mod` y) 695 where x = asSigned w bv1 696 y = asSigned w bv2 697 698-- | 'sdiv' and 'smod' returned as a pair. 699sdivMod :: (1 <= w) => NatRepr w -> BV w -> BV w -> (BV w, BV w) 700sdivMod w bv1 bv2 = (sdiv w bv1 bv2, smod w bv1 bv2) 701 702-- | Bitvector absolute value. Returns the 2's complement 703-- magnitude of the bitvector. 704abs :: (1 <= w) => NatRepr w -> BV w -> BV w 705abs w bv = mkBV' w (Prelude.abs (asSigned w bv)) 706 707-- | 2's complement bitvector negation. 708negate :: NatRepr w -> BV w -> BV w 709negate w (BV x) = mkBV' w (-x) 710 711-- | Get the sign bit as a 'BV'. 712signBit :: 1 <= w => NatRepr w -> BV w -> BV w 713signBit w bv@(BV _) = lshr w bv (natValue w - 1) `and` BV 1 714 715-- | Return 1 if positive, -1 if negative, and 0 if 0. 716signum :: 1 <= w => NatRepr w -> BV w -> BV w 717signum w bv = mkBV' w (Prelude.signum (asSigned w bv)) 718 719-- | Signed less than. 720slt :: (1 <= w) => NatRepr w -> BV w -> BV w -> Bool 721slt w bv1 bv2 = asSigned w bv1 < asSigned w bv2 722 723-- | Signed less than or equal. 724sle :: (1 <= w) => NatRepr w -> BV w -> BV w -> Bool 725sle w bv1 bv2 = asSigned w bv1 <= asSigned w bv2 726 727-- | Unsigned less than. 728ult :: BV w -> BV w -> Bool 729ult bv1 bv2 = asUnsigned bv1 < asUnsigned bv2 730 731-- | Unsigned less than or equal. 732ule :: BV w -> BV w -> Bool 733ule bv1 bv2 = asUnsigned bv1 <= asUnsigned bv2 734 735-- | Unsigned minimum of two bitvectors. 736umin :: BV w -> BV w -> BV w 737umin (BV x) (BV y) = if x < y then BV x else BV y 738 739-- | Unsigned maximum of two bitvectors. 740umax :: BV w -> BV w -> BV w 741umax (BV x) (BV y) = if x < y then BV y else BV x 742 743-- | Signed minimum of two bitvectors. 744smin :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w 745smin w bv1 bv2 = if asSigned w bv1 < asSigned w bv2 then bv1 else bv2 746 747-- | Signed maximum of two bitvectors. 748smax :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w 749smax w bv1 bv2 = if asSigned w bv1 < asSigned w bv2 then bv2 else bv1 750 751---------------------------------------- 752-- Width-changing operations 753 754-- | Concatenate two bitvectors. The first argument gets placed in the 755-- higher order bits. 756-- 757-- >>> concat knownNat (mkBV (knownNat @3) 0b001) (mkBV (knownNat @2) 0b10) 758-- BV 6 759-- >>> :type it 760-- it :: BV 5 761concat :: NatRepr w 762 -- ^ Width of higher-order bits 763 -> NatRepr w' 764 -- ^ Width of lower-order bits 765 -> BV w 766 -- ^ Higher-order bits 767 -> BV w' 768 -- ^ Lower-order bits 769 -> BV (w+w') 770concat w w' (BV hi) (BV lo) = checkNatRepr (w `addNat` w') $ 771 BV ((hi `B.shiftL` (fromNatural (natValue w'))) B..|. lo) 772 773-- | Slice out a smaller bitvector from a larger one. 774-- 775-- >>> select (knownNat @4) (knownNat @1) (mkBV (knownNat @12) 0b110010100110) 776-- BV 3 777-- >>> :type it 778-- it :: BV 4 779select :: ix + w' <= w 780 => NatRepr ix 781 -- ^ Index to start selecting from 782 -> NatRepr w' 783 -- ^ Desired output width 784 -> BV w 785 -- ^ Bitvector to select from 786 -> BV w' 787select ix w' (BV x) = mkBV' w' xShf 788 -- NB fromNatural is OK because of (ix + w' <= w) constraint 789 where xShf = x `B.shiftR` (fromNatural (natValue ix)) 790 791-- | Like 'select', but takes a 'Natural' as the index to start 792-- selecting from. Neither the index nor the output width is checked 793-- to ensure the resulting 'BV' lies entirely within the bounds of the 794-- original bitvector. Any bits "selected" from beyond the bounds of 795-- the input bitvector will be 0. 796-- 797-- >>> select' (knownNat @4) 9 (mkBV (knownNat @12) 0b110010100110) 798-- BV 6 799-- >>> :type it 800-- it :: BV 4 801select' :: Natural 802 -- ^ Index to start selecting from 803 -> NatRepr w' 804 -- ^ Desired output width 805 -> BV w 806 -- ^ Bitvector to select from 807 -> BV w' 808select' ix w' (BV x) 809 | toInteger ix < toInteger (maxBound :: Int) = mkBV w' (x `B.shiftR` (fromNatural ix)) 810 | otherwise = zero w' 811 812-- | Zero-extend a bitvector to one of strictly greater width. 813-- 814-- >>> zext (knownNat @8) (mkBV (knownNat @4) 0b1101) 815-- BV 13 816-- >>> :type it 817-- it :: BV 8 818zext :: w + 1 <= w' 819 => NatRepr w' 820 -- ^ Desired output width 821 -> BV w 822 -- ^ Bitvector to extend 823 -> BV w' 824zext w (BV x) = checkNatRepr w $ BV x 825 826-- | Sign-extend a bitvector to one of strictly greater width. 827sext :: (1 <= w, w + 1 <= w') 828 => NatRepr w 829 -- ^ Width of input bitvector 830 -> NatRepr w' 831 -- ^ Desired output width 832 -> BV w 833 -- ^ Bitvector to extend 834 -> BV w' 835sext w w' bv = mkBV w' (asSigned w bv) 836 837-- | Truncate a bitvector to one of strictly smaller width. 838trunc :: w' + 1 <= w 839 => NatRepr w' 840 -- ^ Desired output width 841 -> BV w 842 -- ^ Bitvector to truncate 843 -> BV w' 844trunc w' (BV x) = mkBV' w' x 845 846-- | Like 'trunc', but allows the input width to be greater than or 847-- equal to the output width, in which case it just performs a zero 848-- extension. 849trunc' :: NatRepr w' 850 -- ^ Desired output width 851 -> BV w 852 -- ^ Bitvector to truncate 853 -> BV w' 854trunc' w' (BV x) = mkBV w' x 855 856-- | Wide multiply of two bitvectors. 857mulWide :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w+w') 858mulWide w w' (BV x) (BV y) = checkNatRepr (w `addNat` w') $ BV (x*y) 859 860---------------------------------------- 861-- Enum functions 862 863-- | Unsigned successor. @succUnsigned w (maxUnsigned w)@ returns 'Nothing'. 864succUnsigned :: NatRepr w -> BV w -> Maybe (BV w) 865succUnsigned w (BV x) = 866 if x == P.maxUnsigned w 867 then Nothing 868 else Just (BV (x+1)) 869 870-- | Signed successor. @succSigned w (maxSigned w)@ returns 'Nothing'. 871succSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w) 872succSigned w (BV x) = 873 if x == P.maxSigned w 874 then Nothing 875 else Just (mkBV' w (x+1)) 876 877-- | Unsigned predecessor. @predUnsigned w zero@ returns 'Nothing'. 878predUnsigned :: NatRepr w -> BV w -> Maybe (BV w) 879predUnsigned w (BV x) = 880 if x == P.minUnsigned w 881 then Nothing 882 else Just (BV (x-1)) 883 884-- | Signed predecessor. @predSigned w (minSigned w)@ returns 'Nothing'. 885predSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w) 886predSigned w bv@(BV x) = 887 if bv == minSigned w 888 then Nothing 889 else Just (mkBV' w (x-1)) 890 891-- | List of all unsigned bitvectors from a lower to an upper bound, 892-- inclusive. 893enumFromToUnsigned :: BV w 894 -- ^ Lower bound 895 -> BV w 896 -- ^ Upper bound 897 -> [BV w] 898enumFromToUnsigned bv1 bv2 = BV <$> [asUnsigned bv1 .. asUnsigned bv2] 899 900-- | List of all signed bitvectors from a lower to an upper bound, 901-- inclusive. 902enumFromToSigned :: 1 <= w => NatRepr w 903 -> BV w 904 -- ^ Lower bound 905 -> BV w 906 -- ^ Upper bound 907 -> [BV w] 908enumFromToSigned w bv1 bv2 = (BV . fromJust . signedToUnsigned w) <$> [asSigned w bv1 .. asSigned w bv2] 909 910---------------------------------------- 911-- Pretty printing 912 913-- | Pretty print in hex 914ppHex :: NatRepr w -> BV w -> String 915ppHex w (BV x) = "0x" ++ N.showHex x "" ++ ":" ++ ppWidth w 916 917-- | Pretty print in binary 918ppBin :: NatRepr w -> BV w -> String 919ppBin w (BV x) = "0b" ++ N.showIntAtBase 2 intToDigit x "" ++ ":" ++ ppWidth w 920 921-- | Pretty print in octal 922ppOct :: NatRepr w -> BV w -> String 923ppOct w (BV x) = "0o" ++ N.showOct x "" ++ ":" ++ ppWidth w 924 925-- | Pretty print in decimal 926ppDec :: NatRepr w -> BV w -> String 927ppDec w (BV x) = show x ++ ":" ++ ppWidth w 928 929ppWidth :: NatRepr w -> String 930ppWidth w = "[" ++ show (natValue w) ++ "]" 931