{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# 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

-- Unqualified imports
import Control.DeepSeq (NFData)
import Data.Char (intToDigit)
import Data.List (genericLength)
import Data.Int (Int8, Int16, Int32, Int64)
import Data.Kind (Type)
import Data.Maybe (fromJust)
import Data.Word (Word8, Word16, Word32, Word64)
import Data.Parameterized ( NatRepr
                          , mkNatRepr
                          , natValue
                          , intValue
                          , addNat
                          , ShowF
                          , EqF(..)
                          , Hashable(..)
                          , Some(..)
                          , Pair(..)
                          )
import GHC.Generics (Generic)
import GHC.TypeLits (Nat, type(+), type(<=))
import Language.Haskell.TH.Lift (Lift)
import Numeric.Natural (Natural)
import Prelude hiding (abs, or, and, negate, concat, signum)
import System.Random.Stateful

----------------------------------------
-- Utility functions

-- | Check that a 'NatRepr' is representable as an 'Int'.
checkNatRepr :: NatRepr w -> a -> a
checkNatRepr :: forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr = forall a. Nat -> a -> a
checkNatural forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). NatRepr n -> Nat
natValue

-- | Check that a 'Natural' is representable as an 'Int'.
checkNatural :: Natural -> a -> a
checkNatural :: forall a. Nat -> a -> a
checkNatural Nat
n a
a = if Nat
n forall a. Ord a => a -> a -> Bool
> (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Int) :: Natural)
  then forall a. String -> [String] -> a
panic String
"Data.BitVector.Sized.Internal.checkNatural"
       [forall a. Show a => a -> String
show Nat
n forall a. [a] -> [a] -> [a]
++ String
" not representable as Int"]
  else a
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 :: Nat -> Int
fromNatural = forall a b. (Integral a, Num b) => a -> b
fromIntegral

----------------------------------------
-- BitVector data type definitions

-- | Bitvector datatype, parameterized by width.
newtype 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 ( forall (w :: Nat) x. Rep (BV w) x -> BV w
forall (w :: Nat) x. BV w -> Rep (BV w) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall (w :: Nat) x. Rep (BV w) x -> BV w
$cfrom :: forall (w :: Nat) x. BV w -> Rep (BV w) x
Generic
           , forall (w :: Nat). BV w -> ()
forall a. (a -> ()) -> NFData a
rnf :: BV w -> ()
$crnf :: forall (w :: Nat). BV w -> ()
NFData
           , Int -> BV w -> ShowS
forall (w :: Nat). Int -> BV w -> ShowS
forall (w :: Nat). [BV w] -> ShowS
forall (w :: Nat). BV w -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BV w] -> ShowS
$cshowList :: forall (w :: Nat). [BV w] -> ShowS
show :: BV w -> String
$cshow :: forall (w :: Nat). BV w -> String
showsPrec :: Int -> BV w -> ShowS
$cshowsPrec :: forall (w :: Nat). Int -> BV w -> ShowS
Show
           , ReadPrec [BV w]
ReadPrec (BV w)
ReadS [BV w]
forall (w :: Nat). ReadPrec [BV w]
forall (w :: Nat). ReadPrec (BV w)
forall (w :: Nat). Int -> ReadS (BV w)
forall (w :: Nat). ReadS [BV w]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [BV w]
$creadListPrec :: forall (w :: Nat). ReadPrec [BV w]
readPrec :: ReadPrec (BV w)
$creadPrec :: forall (w :: Nat). ReadPrec (BV w)
readList :: ReadS [BV w]
$creadList :: forall (w :: Nat). ReadS [BV w]
readsPrec :: Int -> ReadS (BV w)
$creadsPrec :: forall (w :: Nat). Int -> ReadS (BV w)
Read
           , BV w -> BV w -> Bool
forall (w :: Nat). BV w -> BV w -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BV w -> BV w -> Bool
$c/= :: forall (w :: Nat). BV w -> BV w -> Bool
== :: BV w -> BV w -> Bool
$c== :: forall (w :: Nat). BV w -> BV w -> Bool
Eq
           , BV w -> BV w -> Bool
BV w -> BV w -> Ordering
BV w -> BV w -> BV w
forall (w :: Nat). Eq (BV w)
forall (w :: Nat). BV w -> BV w -> Bool
forall (w :: Nat). BV w -> BV w -> Ordering
forall (w :: Nat). BV w -> BV w -> BV w
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: BV w -> BV w -> BV w
$cmin :: forall (w :: Nat). BV w -> BV w -> BV w
max :: BV w -> BV w -> BV w
$cmax :: forall (w :: Nat). BV w -> BV w -> BV w
>= :: BV w -> BV w -> Bool
$c>= :: forall (w :: Nat). BV w -> BV w -> Bool
> :: BV w -> BV w -> Bool
$c> :: forall (w :: Nat). BV w -> BV w -> Bool
<= :: BV w -> BV w -> Bool
$c<= :: forall (w :: Nat). BV w -> BV w -> Bool
< :: BV w -> BV w -> Bool
$c< :: forall (w :: Nat). BV w -> BV w -> Bool
compare :: BV w -> BV w -> Ordering
$ccompare :: forall (w :: Nat). BV w -> BV w -> Ordering
Ord -- ^ Uses an unsigned ordering, but 'ule' and 'ult' are
                 -- preferred. We provide this instance to allow the use of 'BV'
                 -- in situations where an arbitrary ordering is required (e.g.,
                 -- as the keys in a map)
           , forall (w :: Nat) (m :: * -> *). Quote m => BV w -> m Exp
forall (w :: Nat) (m :: * -> *). Quote m => BV w -> Code m (BV w)
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => BV w -> m Exp
forall (m :: * -> *). Quote m => BV w -> Code m (BV w)
liftTyped :: forall (m :: * -> *). Quote m => BV w -> Code m (BV w)
$cliftTyped :: forall (w :: Nat) (m :: * -> *). Quote m => BV w -> Code m (BV w)
lift :: forall (m :: * -> *). Quote m => BV w -> m Exp
$clift :: forall (w :: Nat) (m :: * -> *). Quote m => BV w -> m Exp
Lift)

instance ShowF BV

instance EqF BV where
  BV Integer
bv eqF :: forall (w :: Nat). BV w -> BV w -> Bool
`eqF` BV Integer
bv' = Integer
bv forall a. Eq a => a -> a -> Bool
== Integer
bv'

instance Hashable (BV w) where
  hashWithSalt :: Int -> BV w -> Int
hashWithSalt Int
salt (BV Integer
i) = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt Integer
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' :: forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w Integer
x = forall (w :: Nat). Integer -> BV w
BV (forall (w :: Nat). NatRepr w -> Integer -> Integer
P.toUnsigned NatRepr w
w Integer
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 :: forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w
w Integer
x = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w Integer
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 :: forall (w :: Nat). NatRepr w -> Integer -> Maybe Integer
checkUnsigned NatRepr w
w Integer
i = if Integer
i forall a. Ord a => a -> a -> Bool
< Integer
0 Bool -> Bool -> Bool
|| Integer
i forall a. Ord a => a -> a -> Bool
> forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w
  then forall a. Maybe a
Nothing
  else forall a. a -> Maybe a
Just Integer
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 :: forall (w :: Nat). NatRepr w -> Integer -> Maybe (BV w)
mkBVUnsigned NatRepr w
w Integer
x = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Integer -> BV w
BV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat). NatRepr w -> Integer -> Maybe Integer
checkUnsigned NatRepr w
w Integer
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 :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Integer -> Maybe Integer
signedToUnsigned NatRepr w
w Integer
i = if Integer
i forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.minSigned NatRepr w
w Bool -> Bool -> Bool
|| Integer
i forall a. Ord a => a -> a -> Bool
> forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.maxSigned NatRepr w
w
  then forall a. Maybe a
Nothing
  else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ if Integer
i forall a. Ord a => a -> a -> Bool
< Integer
0 then Integer
i forall a. Num a => a -> a -> a
+ forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w forall a. Num a => a -> a -> a
+ Integer
1 else Integer
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 :: forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> Maybe (BV w)
mkBVSigned NatRepr w
w Integer
x = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Integer -> BV w
BV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Integer -> Maybe Integer
signedToUnsigned NatRepr w
w Integer
x

-- | The zero bitvector of any width.
zero :: NatRepr w -> BV w
zero :: forall (w :: Nat). NatRepr w -> BV w
zero NatRepr w
w = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Integer -> BV w
BV Integer
0

-- | The bitvector with value 1, of any positive width.
one :: 1 <= w => NatRepr w -> BV w
one :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
one NatRepr w
w = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Integer -> BV w
BV Integer
1

-- | The bitvector whose value is its own width, of any width.
width :: NatRepr w -> BV w
width :: forall (w :: Nat). NatRepr w -> BV w
width NatRepr w
w = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Integer -> BV w
BV (forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w)

-- | The minimum unsigned value for bitvector with given width (always 0).
minUnsigned :: NatRepr w -> BV w
minUnsigned :: forall (w :: Nat). NatRepr w -> BV w
minUnsigned NatRepr w
w = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Integer -> BV w
BV Integer
0

-- | The maximum unsigned value for bitvector with given width.
maxUnsigned :: NatRepr w -> BV w
maxUnsigned :: forall (w :: Nat). NatRepr w -> BV w
maxUnsigned NatRepr w
w = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Integer -> BV w
BV (forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w)

-- | The minimum value for bitvector in two's complement with given width.
minSigned :: 1 <= w => NatRepr w -> BV w
minSigned :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
minSigned NatRepr w
w = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w
w (forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.minSigned NatRepr w
w)

-- | The maximum value for bitvector in two's complement with given width.
maxSigned :: 1 <= w => NatRepr w -> BV w
maxSigned :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
maxSigned NatRepr w
w = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Integer -> BV w
BV (forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.maxSigned NatRepr w
w)

-- | @unsignedClamp w i@ rounds @i@ to the nearest value between @0@
-- and @2^w - 1@ (inclusive).
unsignedClamp :: NatRepr w -> Integer -> BV w
unsignedClamp :: forall (w :: Nat). NatRepr w -> Integer -> BV w
unsignedClamp NatRepr w
w Integer
x = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$
  if | Integer
x forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). NatRepr w -> Integer
P.minUnsigned NatRepr w
w -> forall (w :: Nat). Integer -> BV w
BV (forall (w :: Nat). NatRepr w -> Integer
P.minUnsigned NatRepr w
w)
     | Integer
x forall a. Ord a => a -> a -> Bool
> forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w -> forall (w :: Nat). Integer -> BV w
BV (forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w)
     | Bool
otherwise -> forall (w :: Nat). Integer -> BV w
BV Integer
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 :: forall (w :: Nat). (1 <= w) => NatRepr w -> Integer -> BV w
signedClamp NatRepr w
w Integer
x = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$
  if | Integer
x forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.minSigned NatRepr w
w -> forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.minSigned NatRepr w
w)
     | Integer
x forall a. Ord a => a -> a -> Bool
> forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.maxSigned NatRepr w
w -> forall (w :: Nat). Integer -> BV w
BV (forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.maxSigned NatRepr w
w)
     | Bool
otherwise -> forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w Integer
x

----------------------------------------
-- Construction from fixed-width data types

-- | Construct a 'BV' from a 'Bool'.
bool :: Bool -> BV 1
bool :: Bool -> BV 1
bool Bool
True = forall (w :: Nat). Integer -> BV w
BV Integer
1
bool Bool
False = forall (w :: Nat). Integer -> BV w
BV Integer
0

-- | Construct a 'BV' from a 'Word8'.
word8 :: Word8 -> BV 8
word8 :: Word8 -> BV 8
word8 = forall (w :: Nat). Integer -> BV w
BV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

-- | Construct a 'BV' from a 'Word16'.
word16 :: Word16 -> BV 16
word16 :: Word16 -> BV 16
word16 = forall (w :: Nat). Integer -> BV w
BV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

-- | Construct a 'BV' from a 'Word32'.
word32 :: Word32 -> BV 32
word32 :: Word32 -> BV 32
word32 = forall (w :: Nat). Integer -> BV w
BV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

-- | Construct a 'BV' from a 'Word64'.
word64 :: Word64 -> BV 64
word64 :: Word64 -> BV 64
word64 = forall (w :: Nat). Integer -> BV w
BV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Integral a => a -> Integer
toInteger

-- | Construct a 'BV' from an 'Int8'.
int8 :: Int8 -> BV 8
int8 :: Int8 -> BV 8
int8 = Word8 -> BV 8
word8 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Int8 -> Word8)

-- | Construct a 'BV' from an 'Int16'.
int16 :: Int16 -> BV 16
int16 :: Int16 -> BV 16
int16 = Word16 -> BV 16
word16 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Int16 -> Word16)

-- | Construct a 'BV' from an 'Int32'.
int32 :: Int32 -> BV 32
int32 :: Int32 -> BV 32
int32 = Word32 -> BV 32
word32 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (Integral a, Num b) => a -> b
fromIntegral :: Int32 -> Word32)

-- | Construct a 'BV' from an 'Int64'.
int64 :: Int64 -> BV 64
int64 :: Int64 -> BV 64
int64 = Word64 -> BV 64
word64 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (Integral a, Num b) => a -> b
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 :: [Bool] -> Pair NatRepr BV
bitsBE [Bool]
bs = case Nat -> Some NatRepr
mkNatRepr (forall a. Num a => Integer -> a
fromInteger (forall i a. Num i => [a] -> i
genericLength [Bool]
bs)) of
  Some NatRepr x
w -> forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr x
w forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k -> *) (tp :: k) (b :: k -> *).
a tp -> b tp -> Pair a b
Pair NatRepr x
w (forall (w :: Nat). Integer -> BV w
BV (forall b. Bits b => [Bool] -> b
B.fromListBE [Bool]
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 :: [Bool] -> Pair NatRepr BV
bitsLE [Bool]
bs = case Nat -> Some NatRepr
mkNatRepr (forall a. Num a => Integer -> a
fromInteger (forall i a. Num i => [a] -> i
genericLength [Bool]
bs)) of
  Some NatRepr x
w -> forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr x
w forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k -> *) (tp :: k) (b :: k -> *).
a tp -> b tp -> Pair a b
Pair NatRepr x
w (forall (w :: Nat). Integer -> BV w
BV (forall b. Bits b => [Bool] -> b
B.fromListLE [Bool]
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 :: ByteString -> Integer
bytestringToIntegerBE ByteString
bs
  | Int
l forall a. Eq a => a -> a -> Bool
== Int
0 = Integer
0
  | Int
l forall a. Eq a => a -> a -> Bool
== Int
1 = forall a. Integral a => a -> Integer
toInteger (HasCallStack => ByteString -> Word8
BS.head ByteString
bs)
  | Bool
otherwise = Integer
x1 forall a. Bits a => a -> Int -> a
`B.shiftL` (Int
l2 forall a. Num a => a -> a -> a
* Int
8) forall a. Bits a => a -> a -> a
B..|. Integer
x2
  where
    l :: Int
l = ByteString -> Int
BS.length ByteString
bs
    l1 :: Int
l1 = Int
l forall a. Integral a => a -> a -> a
`div` Int
2
    l2 :: Int
l2 = Int
l forall a. Num a => a -> a -> a
- Int
l1
    (ByteString
bs1, ByteString
bs2) = Int -> ByteString -> (ByteString, ByteString)
BS.splitAt Int
l1 ByteString
bs
    x1 :: Integer
x1 = ByteString -> Integer
bytestringToIntegerBE ByteString
bs1
    x2 :: Integer
x2 = ByteString -> Integer
bytestringToIntegerBE ByteString
bs2

bytestringToIntegerLE :: BS.ByteString -> Integer
bytestringToIntegerLE :: ByteString -> Integer
bytestringToIntegerLE ByteString
bs
  | Int
l forall a. Eq a => a -> a -> Bool
== Int
0 = Integer
0
  | Int
l forall a. Eq a => a -> a -> Bool
== Int
1 = forall a. Integral a => a -> Integer
toInteger (HasCallStack => ByteString -> Word8
BS.head ByteString
bs)
  | Bool
otherwise = Integer
x2 forall a. Bits a => a -> Int -> a
`B.shiftL` (Int
l1 forall a. Num a => a -> a -> a
* Int
8) forall a. Bits a => a -> a -> a
B..|. Integer
x1
  where
    l :: Int
l = ByteString -> Int
BS.length ByteString
bs
    l1 :: Int
l1 = Int
l forall a. Integral a => a -> a -> a
`div` Int
2
    (ByteString
bs1, ByteString
bs2) = Int -> ByteString -> (ByteString, ByteString)
BS.splitAt Int
l1 ByteString
bs
    x1 :: Integer
x1 = ByteString -> Integer
bytestringToIntegerLE ByteString
bs1
    x2 :: Integer
x2 = ByteString -> Integer
bytestringToIntegerLE ByteString
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 :: ByteString -> Pair NatRepr BV
bytestringBE ByteString
bs = case Nat -> Some NatRepr
mkNatRepr (Nat
8forall a. Num a => a -> a -> a
*forall a b. (Integral a, Num b) => a -> b
fromIntegral (ByteString -> Int
BS.length ByteString
bs)) of
  Some NatRepr x
w -> forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr x
w forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k -> *) (tp :: k) (b :: k -> *).
a tp -> b tp -> Pair a b
Pair NatRepr x
w (forall (w :: Nat). Integer -> BV w
BV (ByteString -> Integer
bytestringToIntegerBE ByteString
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 :: ByteString -> Pair NatRepr BV
bytestringLE ByteString
bs = case Nat -> Some NatRepr
mkNatRepr (Nat
8forall a. Num a => a -> a -> a
*forall a b. (Integral a, Num b) => a -> b
fromIntegral (ByteString -> Int
BS.length ByteString
bs)) of
  Some NatRepr x
w -> forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr x
w forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k -> *) (tp :: k) (b :: k -> *).
a tp -> b tp -> Pair a b
Pair NatRepr x
w (forall (w :: Nat). Integer -> BV w
BV (ByteString -> Integer
bytestringToIntegerLE ByteString
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 :: [Word8] -> Pair NatRepr BV
bytesBE = ByteString -> Pair NatRepr BV
bytestringBE forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
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 :: [Word8] -> Pair NatRepr BV
bytesLE = ByteString -> Pair NatRepr BV
bytestringLE forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Word8] -> ByteString
BS.pack

----------------------------------------
-- BitVector -> Integer functions

-- | Unsigned interpretation of a bitvector as a positive Integer.
asUnsigned :: BV w -> Integer
asUnsigned :: forall (w :: Nat). BV w -> Integer
asUnsigned (BV Integer
x) = Integer
x

-- | Signed interpretation of a bitvector as an Integer.
asSigned :: (1 <= w) => NatRepr w -> BV w -> Integer
asSigned :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w (BV Integer
x) =
  -- NB, fromNatural is OK here because we maintain the invariant that
  --  any existing BV value has a representable width
  let wInt :: Int
wInt = Nat -> Int
fromNatural (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w) in
  if forall a. Bits a => a -> Int -> Bool
B.testBit Integer
x (Int
wInt forall a. Num a => a -> a -> a
- Int
1)
  then Integer
x forall a. Num a => a -> a -> a
- forall a. Bits a => Int -> a
B.bit Int
wInt
  else Integer
x

-- | Unsigned interpretation of a bitvector as a Natural.
asNatural :: BV w -> Natural
asNatural :: forall (w :: Nat). BV w -> Nat
asNatural = (forall a. Num a => Integer -> a
fromInteger :: Integer -> Natural) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Nat). BV w -> Integer
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 :: forall (w :: Nat). NatRepr w -> BV w -> [Bool]
asBitsBE NatRepr w
w BV w
bv = [ forall (w :: Nat). Nat -> BV w -> Bool
testBit' Nat
i BV w
bv | Nat
i <- forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
wi forall a. Num a => a -> a -> a
- Integer
1, Integer
wi forall a. Num a => a -> a -> a
- Integer
2 .. Integer
0] ]
  where wi :: Integer
wi = forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
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 :: forall (w :: Nat). NatRepr w -> BV w -> [Bool]
asBitsLE NatRepr w
w BV w
bv = [ forall (w :: Nat). Nat -> BV w -> Bool
testBit' Nat
i BV w
bv | Nat
i <- forall a. Num a => Integer -> a
fromInteger forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Integer
0 .. Integer
wi forall a. Num a => a -> a -> a
- Integer
1] ]
  where wi :: Integer
wi = forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w

integerToBytesBE :: Natural
                 -- ^ number of bytes
                 -> Integer
                 -> [Word8]
integerToBytesBE :: Nat -> Integer -> [Word8]
integerToBytesBE Nat
n Integer
x =
  [ forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
x forall a. Bits a => a -> Int -> a
`B.shiftR` (Int
8forall a. Num a => a -> a -> a
*Int
ix)) | Int
ix <- [Int
niforall a. Num a => a -> a -> a
-Int
1, Int
niforall a. Num a => a -> a -> a
-Int
2 .. Int
0] ]
  where ni :: Int
ni = forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
n

integerToBytesLE :: Natural
                 -- ^ number of bytes
                 -> Integer
                 -> [Word8]
integerToBytesLE :: Nat -> Integer -> [Word8]
integerToBytesLE Nat
n Integer
x =
  [ forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer
x forall a. Bits a => a -> Int -> a
`B.shiftR` (Int
8forall a. Num a => a -> a -> a
*Int
ix)) | Int
ix <- [Int
0 .. Int
niforall a. Num a => a -> a -> a
-Int
1] ]
  where ni :: Int
ni = forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
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 :: forall (w :: Nat). NatRepr w -> BV w -> Maybe [Word8]
asBytesBE NatRepr w
w (BV Integer
x)
  | forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w forall a. Integral a => a -> a -> a
`mod` Nat
8 forall a. Eq a => a -> a -> Bool
== Nat
0 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Nat -> Integer -> [Word8]
integerToBytesBE (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w forall a. Integral a => a -> a -> a
`div` Nat
8) Integer
x
  | Bool
otherwise = forall a. Maybe a
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 :: forall (w :: Nat). NatRepr w -> BV w -> Maybe [Word8]
asBytesLE NatRepr w
w (BV Integer
x)
  | forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w forall a. Integral a => a -> a -> a
`mod` Nat
8 forall a. Eq a => a -> a -> Bool
== Nat
0 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Nat -> Integer -> [Word8]
integerToBytesLE (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w forall a. Integral a => a -> a -> a
`div` Nat
8) Integer
x
  | Bool
otherwise = forall a. Maybe a
Nothing

-- | 'asBytesBE', but for bytestrings.
asBytestringBE :: NatRepr w -> BV w -> Maybe BS.ByteString
asBytestringBE :: forall (w :: Nat). NatRepr w -> BV w -> Maybe ByteString
asBytestringBE NatRepr w
w BV w
bv = [Word8] -> ByteString
BS.pack forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat). NatRepr w -> BV w -> Maybe [Word8]
asBytesBE NatRepr w
w BV w
bv

-- | 'asBytesLE', but for bytestrings.
asBytestringLE :: NatRepr w -> BV w -> Maybe BS.ByteString
asBytestringLE :: forall (w :: Nat). NatRepr w -> BV w -> Maybe ByteString
asBytestringLE NatRepr w
w BV w
bv = [Word8] -> ByteString
BS.pack forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Nat). NatRepr w -> BV w -> Maybe [Word8]
asBytesLE NatRepr w
w BV w
bv

----------------------------------------
-- BV w operations (fixed width)

-- | Bitwise and.
and :: BV w -> BV w -> BV w
and :: forall (w :: Nat). BV w -> BV w -> BV w
and (BV Integer
x) (BV Integer
y) = forall (w :: Nat). Integer -> BV w
BV (Integer
x forall a. Bits a => a -> a -> a
B..&. Integer
y)

-- | Bitwise or.
or :: BV w -> BV w -> BV w
or :: forall (w :: Nat). BV w -> BV w -> BV w
or (BV Integer
x) (BV Integer
y) = forall (w :: Nat). Integer -> BV w
BV (Integer
x forall a. Bits a => a -> a -> a
B..|. Integer
y)

-- | Bitwise xor.
xor :: BV w -> BV w -> BV w
xor :: forall (w :: Nat). BV w -> BV w -> BV w
xor (BV Integer
x) (BV Integer
y) = forall (w :: Nat). Integer -> BV w
BV (Integer
x forall a. Bits a => a -> a -> a
`B.xor` Integer
y)

-- | Bitwise complement (flip every bit).
complement :: NatRepr w -> BV w -> BV w
complement :: forall (w :: Nat). NatRepr w -> BV w -> BV w
complement NatRepr w
w (BV Integer
x) = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (forall a. Bits a => a -> a
B.complement Integer
x)


-- | Clamp shift amounts to the word width and
--   coerce to an @Int@
shiftAmount :: NatRepr w -> Natural -> Int
shiftAmount :: forall (w :: Nat). NatRepr w -> Nat -> Int
shiftAmount NatRepr w
w Nat
shf = Nat -> Int
fromNatural (forall a. Ord a => a -> a -> a
min (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w) Nat
shf)

-- | Left shift by positive 'Natural'.
shl :: NatRepr w -> BV w -> Natural -> BV w
shl :: forall (w :: Nat). NatRepr w -> BV w -> Nat -> BV w
shl NatRepr w
w (BV Integer
x) Nat
shf = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
x forall a. Bits a => a -> Int -> a
`B.shiftL` forall (w :: Nat). NatRepr w -> Nat -> Int
shiftAmount NatRepr w
w Nat
shf)

-- | Right arithmetic shift by positive 'Natural'.
ashr :: (1 <= w) => NatRepr w -> BV w -> Natural -> BV w
ashr :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Nat -> BV w
ashr NatRepr w
w BV w
bv Nat
shf = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv forall a. Bits a => a -> Int -> a
`B.shiftR` forall (w :: Nat). NatRepr w -> Nat -> Int
shiftAmount NatRepr w
w Nat
shf)

-- | Right logical shift by positive 'Natural'.
lshr :: NatRepr w -> BV w -> Natural -> BV w
lshr :: forall (w :: Nat). NatRepr w -> BV w -> Nat -> BV w
lshr NatRepr w
w (BV Integer
x) Nat
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.
  forall (w :: Nat). Integer -> BV w
BV (Integer
x forall a. Bits a => a -> Int -> a
`B.shiftR` forall (w :: Nat). NatRepr w -> Nat -> Int
shiftAmount NatRepr w
w Nat
shf)

-- | Bitwise rotate left.
rotateL :: NatRepr w -> BV w -> Natural -> BV w
rotateL :: forall (w :: Nat). NatRepr w -> BV w -> Nat -> BV w
rotateL NatRepr w
w BV w
bv Nat
rot' = BV w
leftChunk forall (w :: Nat). BV w -> BV w -> BV w
`or` BV w
rightChunk
  where rot :: Nat
rot = if Nat
wNatural forall a. Eq a => a -> a -> Bool
== Nat
0 then Nat
0 else Nat
rot' forall a. Integral a => a -> a -> a
`mod` Nat
wNatural
        leftChunk :: BV w
leftChunk = forall (w :: Nat). NatRepr w -> BV w -> Nat -> BV w
shl NatRepr w
w BV w
bv Nat
rot
        rightChunk :: BV w
rightChunk = forall (w :: Nat). NatRepr w -> BV w -> Nat -> BV w
lshr NatRepr w
w BV w
bv (Nat
wNatural forall a. Num a => a -> a -> a
- Nat
rot)
        wNatural :: Nat
wNatural = forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w

-- | Bitwise rotate right.
rotateR :: NatRepr w -> BV w -> Natural -> BV w
rotateR :: forall (w :: Nat). NatRepr w -> BV w -> Nat -> BV w
rotateR NatRepr w
w BV w
bv Nat
rot' = BV w
leftChunk forall (w :: Nat). BV w -> BV w -> BV w
`or` BV w
rightChunk
  where rot :: Nat
rot = if Nat
wNatural forall a. Eq a => a -> a -> Bool
== Nat
0 then Nat
0 else Nat
rot' forall a. Integral a => a -> a -> a
`mod` Nat
wNatural
        rightChunk :: BV w
rightChunk = forall (w :: Nat). NatRepr w -> BV w -> Nat -> BV w
lshr NatRepr w
w BV w
bv Nat
rot
        leftChunk :: BV w
leftChunk = forall (w :: Nat). NatRepr w -> BV w -> Nat -> BV w
shl NatRepr w
w BV w
bv (Nat
wNatural forall a. Num a => a -> a -> a
- Nat
rot)
        wNatural :: Nat
wNatural = forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
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 :: forall (ix :: Nat) (w :: Nat).
((ix + 1) <= w) =>
NatRepr w -> NatRepr ix -> BV w
bit NatRepr w
w NatRepr ix
ix =
  forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$
    -- NB fromNatural is OK here because of the (ix+1<w) constraint
    forall (w :: Nat). Integer -> BV w
BV (forall a. Bits a => Int -> a
B.bit (Nat -> Int
fromNatural (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr ix
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' :: forall (w :: Nat). NatRepr w -> Nat -> BV w
bit' NatRepr w
w Nat
ix
  | Nat
ix forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (forall a. Bits a => Int -> a
B.bit (Nat -> Int
fromNatural Nat
ix))
  | Bool
otherwise = forall (w :: Nat). NatRepr w -> BV w
zero NatRepr w
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 :: forall (ix :: Nat) (w :: Nat).
((ix + 1) <= w) =>
NatRepr ix -> BV w -> BV w
setBit NatRepr ix
ix BV w
bv =
  -- NB, fromNatural is OK because of the (ix+1 <= w) constraint
  forall (w :: Nat). BV w -> BV w -> BV w
or BV w
bv (forall (w :: Nat). Integer -> BV w
BV (forall a. Bits a => Int -> a
B.bit (Nat -> Int
fromNatural (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr ix
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' :: forall (w :: Nat). NatRepr w -> Nat -> BV w -> BV w
setBit' NatRepr w
w Nat
ix BV w
bv
  | Nat
ix forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w = forall (w :: Nat). BV w -> BV w -> BV w
or BV w
bv (forall (w :: Nat). Integer -> BV w
BV (forall a. Bits a => Int -> a
B.bit (Nat -> Int
fromNatural Nat
ix)))
  | Bool
otherwise = BV w
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 :: forall (ix :: Nat) (w :: Nat).
((ix + 1) <= w) =>
NatRepr w -> NatRepr ix -> BV w -> BV w
clearBit NatRepr w
w NatRepr ix
ix BV w
bv =
  -- NB, fromNatural is OK because of the (ix+1<=w) constraint
  forall (w :: Nat). BV w -> BV w -> BV w
and BV w
bv (forall (w :: Nat). NatRepr w -> BV w -> BV w
complement NatRepr w
w (forall (w :: Nat). Integer -> BV w
BV (forall a. Bits a => Int -> a
B.bit (Nat -> Int
fromNatural (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr ix
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' :: forall (w :: Nat). NatRepr w -> Nat -> BV w -> BV w
clearBit' NatRepr w
w Nat
ix BV w
bv
  | Nat
ix forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w = forall (w :: Nat). BV w -> BV w -> BV w
and BV w
bv (forall (w :: Nat). NatRepr w -> BV w -> BV w
complement NatRepr w
w (forall (w :: Nat). Integer -> BV w
BV (forall a. Bits a => Int -> a
B.bit (Nat -> Int
fromNatural Nat
ix))))
  | Bool
otherwise = BV w
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 :: forall (ix :: Nat) (w :: Nat).
((ix + 1) <= w) =>
NatRepr ix -> BV w -> BV w
complementBit NatRepr ix
ix BV w
bv =
  -- NB, fromNatural is OK because of (ix+1 <= w) constraint
  forall (w :: Nat). BV w -> BV w -> BV w
xor BV w
bv (forall (w :: Nat). Integer -> BV w
BV (forall a. Bits a => Int -> a
B.bit (Nat -> Int
fromNatural (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr ix
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' :: forall (w :: Nat). NatRepr w -> Nat -> BV w -> BV w
complementBit' NatRepr w
w Nat
ix BV w
bv
  | Nat
ix forall a. Ord a => a -> a -> Bool
< forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w = forall (w :: Nat). BV w -> BV w -> BV w
xor BV w
bv (forall (w :: Nat). Integer -> BV w
BV (forall a. Bits a => Int -> a
B.bit (Nat -> Int
fromNatural Nat
ix)))
  | Bool
otherwise = BV w
bv

-- | Test if a particular bit is set.
testBit :: ix+1 <= w => NatRepr ix -> BV w -> Bool
testBit :: forall (ix :: Nat) (w :: Nat).
((ix + 1) <= w) =>
NatRepr ix -> BV w -> Bool
testBit NatRepr ix
ix (BV Integer
x) = forall a. Bits a => a -> Int -> Bool
B.testBit Integer
x (Nat -> Int
fromNatural (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr ix
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' :: forall (w :: Nat). Nat -> BV w -> Bool
testBit' Nat
ix (BV Integer
x)
  -- NB, If the index is larger than the maximum representable 'Int',
  -- this function should be 'False' by construction of 'BV'.
  | Nat
ix forall a. Ord a => a -> a -> Bool
> forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Int) = Bool
False
  | Bool
otherwise = forall a. Bits a => a -> Int -> Bool
B.testBit Integer
x (Nat -> Int
fromNatural Nat
ix)

-- | Get the number of 1 bits in a 'BV'.
popCount :: BV w -> BV w
popCount :: forall (w :: Nat). BV w -> BV w
popCount (BV Integer
x) = forall (w :: Nat). Integer -> BV w
BV (forall a. Integral a => a -> Integer
toInteger (forall a. Bits a => a -> Int
B.popCount Integer
x))

-- | Count trailing zeros in a 'BV'.
ctz :: NatRepr w -> BV w -> BV w
ctz :: forall (w :: Nat). NatRepr w -> BV w -> BV w
ctz NatRepr w
w (BV Integer
x) = forall (w :: Nat). Integer -> BV w
BV (Integer -> Integer
go Integer
0)
  where go :: Integer -> Integer
go !Integer
i | Integer
i forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w Bool -> Bool -> Bool
&&
                Bool -> Bool
not (forall a. Bits a => a -> Int -> Bool
B.testBit Integer
x (forall a. Num a => Integer -> a
fromInteger Integer
i)) = Integer -> Integer
go (Integer
iforall a. Num a => a -> a -> a
+Integer
1)
              | Bool
otherwise = Integer
i

-- | Count leading zeros in a 'BV'.
clz :: NatRepr w -> BV w -> BV w
clz :: forall (w :: Nat). NatRepr w -> BV w -> BV w
clz NatRepr w
w (BV Integer
x) = forall (w :: Nat). Integer -> BV w
BV (Integer -> Integer
go Integer
0)
 where go :: Integer -> Integer
go !Integer
i | Integer
i forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w Bool -> Bool -> Bool
&&
               Bool -> Bool
not (forall a. Bits a => a -> Int -> Bool
B.testBit Integer
x (forall a. Num a => Integer -> a
fromInteger (forall (w :: Nat). NatRepr w -> Integer
intValue NatRepr w
w forall a. Num a => a -> a -> a
- Integer
i forall a. Num a => a -> a -> a
- Integer
1))) =
                 Integer -> Integer
go (Integer
iforall a. Num a => a -> a -> a
+Integer
1)
             | Bool
otherwise = Integer
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 :: forall (w :: Nat). Nat -> BV w -> BV w
truncBits Nat
b (BV Integer
x) = forall a. Nat -> a -> a
checkNatural Nat
b forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Integer -> BV w
BV (Integer
x forall a. Bits a => a -> a -> a
B..&. (forall a. Bits a => Int -> a
B.bit (Nat -> Int
fromNatural Nat
b) forall a. Num a => a -> a -> a
- Integer
1))

----------------------------------------
-- BV w arithmetic operations (fixed width)

-- | Bitvector add.
add :: NatRepr w -> BV w -> BV w -> BV w
add :: forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
add NatRepr w
w (BV Integer
x) (BV Integer
y) = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
xforall a. Num a => a -> a -> a
+Integer
y)

-- | Bitvector subtract.
sub :: NatRepr w -> BV w -> BV w -> BV w
sub :: forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
sub NatRepr w
w (BV Integer
x) (BV Integer
y) = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
xforall a. Num a => a -> a -> a
-Integer
y)

-- | Bitvector multiply.
mul :: NatRepr w -> BV w -> BV w -> BV w
mul :: forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w
mul NatRepr w
w (BV Integer
x) (BV Integer
y) = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
xforall a. Num a => a -> a -> a
*Integer
y)

-- | Bitvector division (unsigned). Rounds to zero. Division by zero
-- yields a runtime error.
uquot :: BV w -> BV w -> BV w
uquot :: forall (w :: Nat). BV w -> BV w -> BV w
uquot (BV Integer
x) (BV Integer
y) = forall (w :: Nat). Integer -> BV w
BV (Integer
x forall a. Integral a => a -> a -> a
`quot` Integer
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 :: forall (w :: Nat). BV w -> BV w -> BV w
urem (BV Integer
x) (BV Integer
y) = forall (w :: Nat). Integer -> BV w
BV (Integer
x forall a. Integral a => a -> a -> a
`rem` Integer
y)

-- | 'uquot' and 'urem' returned as a pair.
uquotRem :: BV w -> BV w -> (BV w, BV w)
uquotRem :: forall (w :: Nat). BV w -> BV w -> (BV w, BV w)
uquotRem BV w
bv1 BV w
bv2 = (forall (w :: Nat). BV w -> BV w -> BV w
uquot BV w
bv1 BV w
bv2, forall (w :: Nat). BV w -> BV w -> BV w
urem BV w
bv1 BV w
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 :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
squot NatRepr w
w BV w
bv1 BV w
bv2 = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
x forall a. Integral a => a -> a -> a
`quot` Integer
y)
  where x :: Integer
x = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1
        y :: Integer
y = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV 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 :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
srem NatRepr w
w BV w
bv1 BV w
bv2 = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
x forall a. Integral a => a -> a -> a
`rem` Integer
y)
  where x :: Integer
x = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1
        y :: Integer
y = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2

-- | 'squot' and 'srem' returned as a pair.
squotRem :: (1 <= w) => NatRepr w -> BV w -> BV w -> (BV w, BV w)
squotRem :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> (BV w, BV w)
squotRem NatRepr w
w BV w
bv1 BV w
bv2 = (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
squot NatRepr w
w BV w
bv1 BV w
bv2, forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
srem NatRepr w
w BV w
bv1 BV w
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 :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
sdiv NatRepr w
w BV w
bv1 BV w
bv2 = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
x forall a. Integral a => a -> a -> a
`div` Integer
y)
  where x :: Integer
x = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1
        y :: Integer
y = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV 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 :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
smod NatRepr w
w BV w
bv1 BV w
bv2 = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
x forall a. Integral a => a -> a -> a
`mod` Integer
y)
  where x :: Integer
x = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1
        y :: Integer
y = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2

-- | 'sdiv' and 'smod' returned as a pair.
sdivMod :: (1 <= w) => NatRepr w -> BV w -> BV w -> (BV w, BV w)
sdivMod :: forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BV w -> BV w -> (BV w, BV w)
sdivMod NatRepr w
w BV w
bv1 BV w
bv2 = (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
sdiv NatRepr w
w BV w
bv1 BV w
bv2, forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
smod NatRepr w
w BV w
bv1 BV w
bv2)

-- | Bitvector absolute value.  Returns the 2's complement
--   magnitude of the bitvector.
abs :: (1 <= w) => NatRepr w -> BV w -> BV w
abs :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w
abs NatRepr w
w BV w
bv = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (forall a. Num a => a -> a
Prelude.abs (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv))

-- | 2's complement bitvector negation.
negate :: NatRepr w -> BV w -> BV w
negate :: forall (w :: Nat). NatRepr w -> BV w -> BV w
negate NatRepr w
w (BV Integer
x) = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (-Integer
x)

-- | Get the sign bit as a 'BV'.
signBit :: 1 <= w => NatRepr w -> BV w -> BV w
signBit :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w
signBit NatRepr w
w bv :: BV w
bv@(BV Integer
_) = forall (w :: Nat). NatRepr w -> BV w -> Nat -> BV w
lshr NatRepr w
w BV w
bv (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w forall a. Num a => a -> a -> a
- Nat
1) forall (w :: Nat). BV w -> BV w -> BV w
`and` forall (w :: Nat). Integer -> BV w
BV Integer
1

-- | Return 1 if positive, -1 if negative, and 0 if 0.
signum :: 1 <= w => NatRepr w -> BV w -> BV w
signum :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w
signum NatRepr w
w BV w
bv = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (forall a. Num a => a -> a
Prelude.signum (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv))

-- | Signed less than.
slt :: (1 <= w) => NatRepr w -> BV w -> BV w -> Bool
slt :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> Bool
slt NatRepr w
w BV w
bv1 BV w
bv2 = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1 forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2

-- | Signed less than or equal.
sle :: (1 <= w) => NatRepr w -> BV w -> BV w -> Bool
sle :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> Bool
sle NatRepr w
w BV w
bv1 BV w
bv2 = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1 forall a. Ord a => a -> a -> Bool
<= forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2

-- | Unsigned less than.
ult :: BV w -> BV w -> Bool
ult :: forall (w :: Nat). BV w -> BV w -> Bool
ult BV w
bv1 BV w
bv2 = forall (w :: Nat). BV w -> Integer
asUnsigned BV w
bv1 forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). BV w -> Integer
asUnsigned BV w
bv2

-- | Unsigned less than or equal.
ule :: BV w -> BV w -> Bool
ule :: forall (w :: Nat). BV w -> BV w -> Bool
ule BV w
bv1 BV w
bv2 = forall (w :: Nat). BV w -> Integer
asUnsigned BV w
bv1 forall a. Ord a => a -> a -> Bool
<= forall (w :: Nat). BV w -> Integer
asUnsigned BV w
bv2

-- | Unsigned minimum of two bitvectors.
umin :: BV w -> BV w -> BV w
umin :: forall (w :: Nat). BV w -> BV w -> BV w
umin (BV Integer
x) (BV Integer
y) = if Integer
x forall a. Ord a => a -> a -> Bool
< Integer
y then forall (w :: Nat). Integer -> BV w
BV Integer
x else forall (w :: Nat). Integer -> BV w
BV Integer
y

-- | Unsigned maximum of two bitvectors.
umax :: BV w -> BV w -> BV w
umax :: forall (w :: Nat). BV w -> BV w -> BV w
umax (BV Integer
x) (BV Integer
y) = if Integer
x forall a. Ord a => a -> a -> Bool
< Integer
y then forall (w :: Nat). Integer -> BV w
BV Integer
y else forall (w :: Nat). Integer -> BV w
BV Integer
x

-- | Signed minimum of two bitvectors.
smin :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
smin :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
smin NatRepr w
w BV w
bv1 BV w
bv2 = if forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1 forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2 then BV w
bv1 else BV w
bv2

-- | Signed maximum of two bitvectors.
smax :: (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
smax :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> BV w
smax NatRepr w
w BV w
bv1 BV w
bv2 = if forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1 forall a. Ord a => a -> a -> Bool
< forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2 then BV w
bv2 else BV w
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 :: forall (w :: Nat) (w' :: Nat).
NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
concat NatRepr w
w NatRepr w'
w' (BV Integer
hi) (BV Integer
lo) = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr (NatRepr w
w forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
`addNat` NatRepr w'
w') forall a b. (a -> b) -> a -> b
$
  forall (w :: Nat). Integer -> BV w
BV ((Integer
hi forall a. Bits a => a -> Int -> a
`B.shiftL` Nat -> Int
fromNatural (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w'
w')) forall a. Bits a => a -> a -> a
B..|. Integer
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 :: forall (ix :: Nat) (w' :: Nat) (w :: Nat).
((ix + w') <= w) =>
NatRepr ix -> NatRepr w' -> BV w -> BV w'
select NatRepr ix
ix NatRepr w'
w' (BV Integer
x) = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w'
w' Integer
xShf
  -- NB fromNatural is OK because of (ix + w' <= w) constraint
  where xShf :: Integer
xShf = Integer
x forall a. Bits a => a -> Int -> a
`B.shiftR` Nat -> Int
fromNatural (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr ix
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' :: forall (w' :: Nat) (w :: Nat). Nat -> NatRepr w' -> BV w -> BV w'
select' Nat
ix NatRepr w'
w' (BV Integer
x)
  | forall a. Integral a => a -> Integer
toInteger Nat
ix forall a. Ord a => a -> a -> Bool
< forall a. Integral a => a -> Integer
toInteger (forall a. Bounded a => a
maxBound :: Int) = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w'
w' (Integer
x forall a. Bits a => a -> Int -> a
`B.shiftR` Nat -> Int
fromNatural Nat
ix)
  | Bool
otherwise = forall (w :: Nat). NatRepr w -> BV w
zero NatRepr w'
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 :: forall (w :: Nat) (w' :: Nat).
((w + 1) <= w') =>
NatRepr w' -> BV w -> BV w'
zext NatRepr w'
w (BV Integer
x) = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr NatRepr w'
w forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Integer -> BV w
BV Integer
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 :: forall (w :: Nat) (w' :: Nat).
(1 <= w, (w + 1) <= w') =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
sext NatRepr w
w NatRepr w'
w' BV w
bv = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w'
w' (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV 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 :: forall (w' :: Nat) (w :: Nat).
((w' + 1) <= w) =>
NatRepr w' -> BV w -> BV w'
trunc NatRepr w'
w' (BV Integer
x) = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w'
w' Integer
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' :: forall (w' :: Nat) (w :: Nat). NatRepr w' -> BV w -> BV w'
trunc' NatRepr w'
w' (BV Integer
x) = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w'
w' Integer
x
{-# DEPRECATED trunc' "Use zresize instead" #-}

-- | Resizes a bitvector. If @w' > w@, perform a zero extension.
zresize :: NatRepr w'
        -- ^ Desired output width
        -> BV w
        -- ^ Bitvector to resize
        -> BV w'
zresize :: forall (w' :: Nat) (w :: Nat). NatRepr w' -> BV w -> BV w'
zresize NatRepr w'
w' (BV Integer
x) = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w'
w' Integer
x

-- | Resizes a bitvector. If @w' > w@, perform a signed extension.
sresize :: 1 <= w
        => NatRepr w
        -- ^ Width of input vector
        -> NatRepr w'
        -- ^ Desired output width
        -> BV w
        -- ^ Bitvector to resize
        -> BV w'
sresize :: forall (w :: Nat) (w' :: Nat).
(1 <= w) =>
NatRepr w -> NatRepr w' -> BV w -> BV w'
sresize NatRepr w
w NatRepr w'
w' BV w
bv = forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w'
w' (forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv)

-- | Wide multiply of two bitvectors.
mulWide :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w+w')
mulWide :: forall (w :: Nat) (w' :: Nat).
NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
mulWide NatRepr w
w NatRepr w'
w' (BV Integer
x) (BV Integer
y) = forall (w :: Nat) a. NatRepr w -> a -> a
checkNatRepr (NatRepr w
w forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
`addNat` NatRepr w'
w') forall a b. (a -> b) -> a -> b
$ forall (w :: Nat). Integer -> BV w
BV (Integer
xforall a. Num a => a -> a -> a
*Integer
y)

----------------------------------------
-- Enum functions

-- | Unsigned successor. @succUnsigned w (maxUnsigned w)@ returns 'Nothing'.
succUnsigned :: NatRepr w -> BV w -> Maybe (BV w)
succUnsigned :: forall (w :: Nat). NatRepr w -> BV w -> Maybe (BV w)
succUnsigned NatRepr w
w (BV Integer
x) =
  if Integer
x forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w
  then forall a. Maybe a
Nothing
  else forall a. a -> Maybe a
Just (forall (w :: Nat). Integer -> BV w
BV (Integer
xforall a. Num a => a -> a -> a
+Integer
1))

-- | Signed successor. @succSigned w (maxSigned w)@ returns 'Nothing'.
succSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w)
succSigned :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Maybe (BV w)
succSigned NatRepr w
w (BV Integer
x) =
  if Integer
x forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). (1 <= w) => NatRepr w -> Integer
P.maxSigned NatRepr w
w
  then forall a. Maybe a
Nothing
  else forall a. a -> Maybe a
Just (forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
xforall a. Num a => a -> a -> a
+Integer
1))

-- | Unsigned predecessor. @predUnsigned w zero@ returns 'Nothing'.
predUnsigned :: NatRepr w -> BV w -> Maybe (BV w)
predUnsigned :: forall (w :: Nat). NatRepr w -> BV w -> Maybe (BV w)
predUnsigned NatRepr w
w (BV Integer
x) =
  if Integer
x forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). NatRepr w -> Integer
P.minUnsigned NatRepr w
w
  then forall a. Maybe a
Nothing
  else forall a. a -> Maybe a
Just (forall (w :: Nat). Integer -> BV w
BV (Integer
xforall a. Num a => a -> a -> a
-Integer
1))

-- | Signed predecessor. @predSigned w (minSigned w)@ returns 'Nothing'.
predSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w)
predSigned :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Maybe (BV w)
predSigned NatRepr w
w bv :: BV w
bv@(BV Integer
x) =
  if BV w
bv forall a. Eq a => a -> a -> Bool
== forall (w :: Nat). (1 <= w) => NatRepr w -> BV w
minSigned NatRepr w
w
  then forall a. Maybe a
Nothing
  else forall a. a -> Maybe a
Just (forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV' NatRepr w
w (Integer
xforall a. Num a => a -> a -> a
-Integer
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 :: forall (w :: Nat). BV w -> BV w -> [BV w]
enumFromToUnsigned BV w
bv1 BV w
bv2 = forall (w :: Nat). Integer -> BV w
BV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [forall (w :: Nat). BV w -> Integer
asUnsigned BV w
bv1 .. forall (w :: Nat). BV w -> Integer
asUnsigned BV w
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 :: forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> BV w -> [BV w]
enumFromToSigned NatRepr w
w BV w
bv1 BV w
bv2 =
  forall (w :: Nat). Integer -> BV w
BV forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (w :: Nat).
(1 <= w) =>
NatRepr w -> Integer -> Maybe Integer
signedToUnsigned NatRepr w
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv1 .. forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
bv2]

----------------------------------------
-- Generating random bitvectors

-- | Generates a bitvector uniformly distributed over all possible values for a
-- given width. (See 'System.Random.Stateful.uniformM').
uniformM :: StatefulGen g m => NatRepr w -> g -> m (BV w)
uniformM :: forall g (m :: * -> *) (w :: Nat).
StatefulGen g m =>
NatRepr w -> g -> m (BV w)
uniformM NatRepr w
w g
g = forall (w :: Nat). Integer -> BV w
BV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a g (m :: * -> *).
(UniformRange a, StatefulGen g m) =>
(a, a) -> g -> m a
uniformRM (forall (w :: Nat). NatRepr w -> Integer
P.minUnsigned NatRepr w
w, forall (w :: Nat). NatRepr w -> Integer
P.maxUnsigned NatRepr w
w) g
g

-- | Generates a bitvector uniformly distributed over the provided range
-- (interpreted as a range of /unsigned/ bitvectors), which is interpreted as
-- inclusive in the lower and upper bound. (See
-- 'System.Random.Stateful.uniformRM').
uUniformRM :: StatefulGen g m => (BV w, BV w) -> g -> m (BV w)
uUniformRM :: forall g (m :: * -> *) (w :: Nat).
StatefulGen g m =>
(BV w, BV w) -> g -> m (BV w)
uUniformRM (BV w
lo, BV w
hi) g
g =
  let loI :: Integer
loI = forall (w :: Nat). BV w -> Integer
asUnsigned BV w
lo
      hiI :: Integer
hiI = forall (w :: Nat). BV w -> Integer
asUnsigned BV w
hi
  in forall (w :: Nat). Integer -> BV w
BV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a g (m :: * -> *).
(UniformRange a, StatefulGen g m) =>
(a, a) -> g -> m a
uniformRM (Integer
loI, Integer
hiI) g
g

-- | Generates a bitvector uniformly distributed over the provided range
-- (interpreted as a range of /signed/ bitvectors), which is interpreted as
-- inclusive in the lower and upper bound. (See
-- 'System.Random.Stateful.uniformRM').
sUniformRM :: (StatefulGen g m, 1 <= w) => NatRepr w -> (BV w, BV w) -> g -> m (BV w)
sUniformRM :: forall g (m :: * -> *) (w :: Nat).
(StatefulGen g m, 1 <= w) =>
NatRepr w -> (BV w, BV w) -> g -> m (BV w)
sUniformRM NatRepr w
w (BV w
lo, BV w
hi) g
g =
  let loI :: Integer
loI = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
lo
      hiI :: Integer
hiI = forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
asSigned NatRepr w
w BV w
hi
  in forall (w :: Nat). NatRepr w -> Integer -> BV w
mkBV NatRepr w
w forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a g (m :: * -> *).
(UniformRange a, StatefulGen g m) =>
(a, a) -> g -> m a
uniformRM (Integer
loI, Integer
hiI) g
g

----------------------------------------
-- Pretty printing

-- | Pretty print in hex
ppHex :: NatRepr w -> BV w -> String
ppHex :: forall (w :: Nat). NatRepr w -> BV w -> String
ppHex NatRepr w
w (BV Integer
x) = String
"0x" forall a. [a] -> [a] -> [a]
++ forall a. (Integral a, Show a) => a -> ShowS
N.showHex Integer
x String
"" forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ forall (w :: Nat). NatRepr w -> String
ppWidth NatRepr w
w

-- | Pretty print in binary
ppBin :: NatRepr w -> BV w -> String
ppBin :: forall (w :: Nat). NatRepr w -> BV w -> String
ppBin NatRepr w
w (BV Integer
x) = String
"0b" forall a. [a] -> [a] -> [a]
++ forall a. (Integral a, Show a) => a -> (Int -> Char) -> a -> ShowS
N.showIntAtBase Integer
2 Int -> Char
intToDigit Integer
x String
"" forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ forall (w :: Nat). NatRepr w -> String
ppWidth NatRepr w
w

-- | Pretty print in octal
ppOct :: NatRepr w -> BV w -> String
ppOct :: forall (w :: Nat). NatRepr w -> BV w -> String
ppOct NatRepr w
w (BV Integer
x) = String
"0o" forall a. [a] -> [a] -> [a]
++ forall a. (Integral a, Show a) => a -> ShowS
N.showOct Integer
x String
"" forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ forall (w :: Nat). NatRepr w -> String
ppWidth NatRepr w
w

-- | Pretty print in decimal
ppDec :: NatRepr w -> BV w -> String
ppDec :: forall (w :: Nat). NatRepr w -> BV w -> String
ppDec NatRepr w
w (BV Integer
x) = forall a. Show a => a -> String
show Integer
x forall a. [a] -> [a] -> [a]
++ String
":" forall a. [a] -> [a] -> [a]
++ forall (w :: Nat). NatRepr w -> String
ppWidth NatRepr w
w

ppWidth :: NatRepr w -> String
ppWidth :: forall (w :: Nat). NatRepr w -> String
ppWidth NatRepr w
w = String
"[" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (n :: Nat). NatRepr n -> Nat
natValue NatRepr w
w) forall a. [a] -> [a] -> [a]
++ String
"]"