content: ------------------------------------------------------------------------
  -- |
  -- Module      : What4.SWord
  -- Description : Dynamically-sized bitvector values
  -- Copyright   : Galois, Inc. 2018-2020
  -- License     : BSD3
  -- Maintainer  : rdockins@galois.com
  -- Stability   : experimental
  -- Portability : non-portable (language extensions)
  --
  -- A wrapper for What4 bitvectors so that the width is not tracked
  -- statically.
  ------------------------------------------------------------------------
  
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveTraversable #-}
  {-# LANGUAGE DeriveFoldable #-}
  {-# LANGUAGE DeriveFunctor #-}
  {-# LANGUAGE DoAndIfThenElse #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE PatternGuards #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE PartialTypeSignatures #-}
  
  module What4.SWord
    ( SWord(..)
    , bvAsSignedInteger
    , bvAsUnsignedInteger
    , integerToBV
    , bvToInteger
    , sbvToInteger
    , freshBV
    , bvWidth
    , bvLit
    , bvFill
    , bvAtBE
    , bvAtLE
    , bvSetBE
    , bvSetLE
    , bvSliceBE
    , bvSliceLE
    , bvJoin
    , bvIte
    , bvPackBE
    , bvPackLE
    , bvUnpackBE
    , bvUnpackLE
    , bvForall
    , unsignedBVBounds
    , signedBVBounds
  
      -- * Logic operations
    , bvNot
    , bvAnd
    , bvOr
    , bvXor
  
      -- * Arithmetic operations
    , bvNeg
    , bvAdd
    , bvSub
    , bvMul
    , bvUDiv
    , bvURem
    , bvSDiv
    , bvSRem
  
      -- * Comparison operations
    , bvEq
    , bvsle
    , bvslt
    , bvule
    , bvult
    , bvsge
    , bvsgt
    , bvuge
    , bvugt
    , bvIsNonzero
  
      -- * bit-counting operations
    , bvPopcount
    , bvCountLeadingZeros
    , bvCountTrailingZeros
    , bvLg2
  
      -- * Shift and rotates
    , bvShl
    , bvLshr
    , bvAshr
    , bvRol
    , bvRor
  
      -- * Zero- and sign-extend
    , bvZext
    , bvSext
    ) where
  
  
  import           Data.Vector (Vector)
  import qualified Data.Vector as V
  import           Numeric.Natural
  
  import           GHC.TypeNats
  
  import qualified Data.BitVector.Sized as BV
  import           Data.Parameterized.NatRepr
  import           Data.Parameterized.Some(Some(..))
  
  import           What4.Interface(SymBV,Pred,SymInteger,IsExpr,SymExpr,IsExprBuilder,IsSymExprBuilder)
  import qualified What4.Interface as W
  import           What4.Panic (panic)
  
  -------------------------------------------------------------
  --
  -- | A What4 symbolic bitvector where the size does not appear in the type
  data SWord sym where
  
    DBV :: (IsExpr (SymExpr sym), 1<=w) => SymBV sym w -> SWord sym
    -- a bit-vector with positive length
  
    ZBV :: SWord sym
    -- a zero-length bit vector. i.e. 0
  
  
  instance Show (SWord sym) where
    show (DBV bv) = show $ W.printSymExpr bv
    show ZBV      = "0:[0]"
  
  -------------------------------------------------------------
  
  -- | Return the signed value if this is a constant bitvector
  bvAsSignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
  bvAsSignedInteger ZBV = Just 0
  bvAsSignedInteger (DBV (bv :: SymBV sym w)) =
    BV.asSigned (W.bvWidth bv) <$> W.asBV bv
  
  -- | Return the unsigned value if this is a constant bitvector
  bvAsUnsignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
  bvAsUnsignedInteger ZBV = Just 0
  bvAsUnsignedInteger (DBV (bv :: SymBV sym w)) =
    BV.asUnsigned <$> W.asBV bv
  
  
  unsignedBVBounds :: forall sym. IsExprBuilder sym => SWord sym -> Maybe (Integer, Integer)
  unsignedBVBounds ZBV = Just (0, 0)
  unsignedBVBounds (DBV bv) = W.unsignedBVBounds bv
  
  signedBVBounds :: forall sym. IsExprBuilder sym => SWord sym -> Maybe (Integer, Integer)
  signedBVBounds ZBV = Just (0, 0)
  signedBVBounds (DBV bv) = W.signedBVBounds bv
  
  
  -- | Convert an integer to an unsigned bitvector.
  --   The input value is reduced modulo 2^w.
  integerToBV :: forall sym width. (Show width, Integral width, IsExprBuilder sym) =>
    sym ->  SymInteger sym -> width -> IO (SWord sym)
  integerToBV sym i w
    | Just (Some wr) <- someNat w
    , Just LeqProof  <- isPosNat wr
    = DBV <$> W.integerToBV sym i wr
    | 0 == toInteger w
    = return ZBV
    | otherwise
    = panic "integerToBV" ["invalid bit-width", show w]
  
  -- | Interpret the bit-vector as an unsigned integer
  bvToInteger :: forall sym. (IsExprBuilder sym) =>
    sym -> SWord sym -> IO (SymInteger sym)
  bvToInteger sym ZBV      = W.intLit sym 0
  bvToInteger sym (DBV bv) = W.bvToInteger sym bv
  
  -- | Interpret the bit-vector as a signed integer
  sbvToInteger :: forall sym. (IsExprBuilder sym) =>
    sym -> SWord sym -> IO (SymInteger sym)
  sbvToInteger sym ZBV      = W.intLit sym 0
  sbvToInteger sym (DBV bv) = W.sbvToInteger sym bv
  
  
  -- | Get the width of a bitvector
  bvWidth :: forall sym. SWord sym -> Integer
  bvWidth (DBV x) = fromInteger (intValue (W.bvWidth x))
  bvWidth ZBV = 0
  
  -- | Create a bitvector with the given width and value
  bvLit :: forall sym. IsExprBuilder sym =>
    sym -> Integer -> Integer -> IO (SWord sym)
  bvLit _ w _
    | w == 0
    = return ZBV
  bvLit sym w dat
    | Just (Some rw) <- someNat w
    , Just LeqProof <- isPosNat rw
    = DBV <$> W.bvLit sym rw (BV.mkBV rw dat)
    | otherwise
    = panic "bvLit" ["size of bitvector is < 0 or >= maxInt", show w]
  
  
  freshBV :: forall sym. IsSymExprBuilder sym =>
    sym -> W.SolverSymbol -> Integer -> IO (SWord sym)
  freshBV sym nm w
    | w == 0
    = return ZBV
  
    | Just (Some rw) <- someNat w
    , Just LeqProof <- isPosNat rw
    = DBV <$> W.freshConstant sym nm (W.BaseBVRepr rw)
  
    | otherwise
    = panic "freshBV" ["size of bitvector is < 0 or >= maxInt", show w]
  
  
  bvFill :: forall sym. IsExprBuilder sym =>
    sym -> Integer -> Pred sym -> IO (SWord sym)
  bvFill sym w p
    | w == 0
    = return ZBV
  
    | Just (Some rw) <- someNat w
    , Just LeqProof <- isPosNat rw
    = DBV <$> W.bvFill sym rw p
  
    | otherwise
    = panic "bvFill" ["size of bitvector is < 0 or >= maxInt", show w]
  
  
  -- | Returns true if the corresponding bit in the bitvector is set.
  --   NOTE bits are numbered in big-endian ordering, meaning the
  --   most-significant bit is bit 0
  bvAtBE :: forall sym.
    IsExprBuilder sym =>
    sym ->
    SWord sym ->
    Integer {- ^ Index of bit (0 is the most significant bit) -} ->
    IO (Pred sym)
  bvAtBE sym (DBV bv) i = do
    let w   = natValue (W.bvWidth bv)
    let idx = w - 1 - fromInteger i
    W.testBitBV sym idx bv
  bvAtBE _ ZBV _ = panic "bvAtBE" ["cannot index into empty bitvector"]
  
  -- | Returns true if the corresponding bit in the bitvector is set.
  --   NOTE bits are numbered in little-endian ordering, meaning the
  --   least-significant bit is bit 0
  bvAtLE :: forall sym.
    IsExprBuilder sym =>
    sym ->
    SWord sym ->
    Integer {- ^ Index of bit (0 is the most significant bit) -} ->
    IO (Pred sym)
  bvAtLE sym (DBV bv) i =
    W.testBitBV sym (fromInteger i) bv
  bvAtLE _ ZBV _ = panic "bvAtLE" ["cannot index into empty bitvector"]
  
  -- | Set the numbered bit in the given bitvector to the given
  --   bit value.
  --   NOTE bits are numbered in big-endian ordering, meaning the
  --   most-significant bit is bit 0
  bvSetBE :: forall sym.
    IsExprBuilder sym =>
    sym ->
    SWord sym ->
    Integer {- ^ Index of bit (0 is the most significant bit) -} ->
    Pred sym ->
    IO (SWord sym)
  bvSetBE _ ZBV _ _ = return ZBV
  bvSetBE sym (DBV bv) i b =
    do let w = natValue (W.bvWidth bv)
       let idx = w - 1 - fromInteger i
       DBV <$> W.bvSet sym bv idx b
  
  -- | Set the numbered bit in the given bitvector to the given
  --   bit value.
  --   NOTE bits are numbered in big-endian ordering, meaning the
  --   most-significant bit is bit 0
  bvSetLE :: forall sym.
    IsExprBuilder sym =>
    sym ->
    SWord sym ->
    Integer {- ^ Index of bit (0 is the most significant bit) -} ->
    Pred sym ->
    IO (SWord sym)
  bvSetLE _ ZBV _ _ = return ZBV
  bvSetLE sym (DBV bv) i b =
    DBV <$> W.bvSet sym bv (fromInteger i) b
  
  
  -- | Concatenate two bitvectors.
  bvJoin  :: forall sym. IsExprBuilder sym => sym
    -> SWord sym
    -- ^ most significant bits
    -> SWord sym
    -- ^ least significant bits
    -> IO (SWord sym)
  bvJoin _ x ZBV = return x
  bvJoin _ ZBV x = return x
  bvJoin sym (DBV bv1) (DBV bv2)
    | LeqProof <- leqAddPos (W.bvWidth bv1) (W.bvWidth bv2)
    = DBV <$> W.bvConcat sym bv1 bv2
  
  -- | Select a subsequence from a bitvector, with bits
  --   numbered in Big Endian order (most significant bit is 0).
  --   This fails if idx + n is >= w
  bvSliceBE :: forall sym. IsExprBuilder sym => sym
    -> Integer
    -- ^ Starting index, from 0 as most significant bit
    -> Integer
    -- ^ Number of bits to take
    -> SWord sym
    -> IO (SWord sym)
  bvSliceBE _ _m 0 _  = pure ZBV
  bvSliceBE sym m n (DBV bv)
    | Just (Some nr) <- someNat n,
      Just LeqProof  <- isPosNat nr,
      Just (Some mr) <- someNat m,
      let wr = W.bvWidth bv,
      Just LeqProof <- testLeq (addNat mr nr)  wr,
      let idx = subNat wr (addNat mr nr),
      Just LeqProof <- testLeq (addNat idx nr) wr
    = DBV <$> W.bvSelect sym idx nr bv
    | otherwise
    = panic "bvSliceBE"
        ["invalid arguments to slice: " ++ show m ++ " " ++ show n
          ++ " from vector of length " ++ show (W.bvWidth bv)]
  bvSliceBE _ m n ZBV
    = panic "bvSliceBE"
        ["invalid arguments to slice: " ++ show m ++ " " ++ show n
          ++ " from vector of length 0"]
  
  
  -- | Select a subsequence from a bitvector, with bits
  --   numbered in Little Endian order (least significant bit is 0).
  --   This fails if idx + n is >= w
  bvSliceLE :: forall sym. IsExprBuilder sym => sym
    -> Integer
    -- ^ Starting index, from 0 as most significant bit
    -> Integer
    -- ^ Number of bits to take
    -> SWord sym
    -> IO (SWord sym)
  bvSliceLE _ _m 0 _  = return ZBV
  bvSliceLE sym m n (DBV bv)
    | Just (Some nr) <- someNat n,
      Just LeqProof  <- isPosNat nr,
      Just (Some mr) <- someNat m,
      let wr = W.bvWidth bv,
      Just LeqProof <- testLeq (addNat mr nr) wr
    = DBV <$> W.bvSelect sym mr nr bv
  
    | otherwise
    = panic "bvSliceLE"
        ["invalid arguments to slice: " ++ show m ++ " " ++ show n
          ++ " from vector of length " ++ show (W.bvWidth bv)]
  bvSliceLE _ m n ZBV
    = panic "bvSliceLE"
        ["invalid arguments to slice: " ++ show m ++ " " ++ show n
          ++ " from vector of length 0"]
  
  
  -- | Ceiling (log_2 x)
  -- adapted from saw-core-sbv/src/Verifier/SAW/Simulator/SBV.hs
  w_bvLg2 :: forall sym w. (IsExprBuilder sym, 1 <= w) =>
     sym -> SymBV sym w -> IO (SymBV sym w)
  w_bvLg2 sym x = go 0
    where
      w = W.bvWidth x
      size :: Integer
      size = intValue w
      lit :: Integer -> IO (SymBV sym w)
      -- BGS: This change could lead to some inefficency
      lit n = W.bvLit sym w (BV.mkBV w n)
      go :: Integer -> IO (SymBV sym w)
      go i | i < size = do
             x' <- lit (2 ^ i)
             b' <- W.bvUle sym x x'
             th <- lit i
             el <- go (i + 1)
             W.bvIte sym b' th el
           | otherwise    = lit i
  
  -- | If-then-else applied to bitvectors.
  bvIte :: forall sym. IsExprBuilder sym =>
    sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
  bvIte _ _ ZBV ZBV
    = return ZBV
  bvIte sym p (DBV bv1) (DBV bv2)
    | Just Refl <- testEquality (W.exprType bv1) (W.exprType bv2)
    = DBV <$> W.bvIte sym p bv1 bv2
  bvIte _ _ x y
    = panic "bvIte" ["bit-vectors don't have same length", show (bvWidth x), show (bvWidth y)]
  
  
  ----------------------------------------------------------------------
  -- Convert to/from Vectors
  ----------------------------------------------------------------------
  
  -- | Explode a bitvector into a vector of booleans in Big Endian
  --   order (most significant bit first)
  bvUnpackBE :: forall sym. IsExprBuilder sym =>
    sym -> SWord sym -> IO (Vector (Pred sym))
  bvUnpackBE _   ZBV = return V.empty
  bvUnpackBE sym (DBV bv) = do
    let w :: Natural
        w = natValue (W.bvWidth bv)
    V.generateM (fromIntegral w)
                (\i -> W.testBitBV sym (w - 1 - fromIntegral i) bv)
  
  
  -- | Explode a bitvector into a vector of booleans in Little Endian
  --   order (least significant bit first)
  bvUnpackLE :: forall sym. IsExprBuilder sym =>
    sym -> SWord sym -> IO (Vector (Pred sym))
  bvUnpackLE _   ZBV = return V.empty
  bvUnpackLE sym (DBV bv) = do
    let w :: Natural
        w = natValue (W.bvWidth bv)
    V.generateM (fromIntegral w)
                (\i -> W.testBitBV sym (fromIntegral i) bv)
  
  
  -- | convert a vector of booleans to a bitvector.  The input
  --   are used in Big Endian order (most significant bit first)
  bvPackBE :: forall sym. (W.IsExpr (W.SymExpr sym), IsExprBuilder sym) =>
    sym -> Vector (Pred sym) -> IO (SWord sym)
  bvPackBE sym vec = do
    vec' <- V.mapM (\p -> do
                       v1 <- bvLit sym 1 1
                       v2 <- bvLit sym 1 0
                       bvIte sym p v1 v2) vec
    V.foldM (\x y -> bvJoin sym x y) ZBV vec'
  
  
  -- | convert a vector of booleans to a bitvector.  The inputs
  --   are used in Little Endian order (least significant bit first)
  bvPackLE :: forall sym. (W.IsExpr (W.SymExpr sym), IsExprBuilder sym) =>
    sym -> Vector (Pred sym) -> IO (SWord sym)
  bvPackLE sym vec = do
    vec' <- V.mapM (\p -> do
                       v1 <- bvLit sym 1 1
                       v2 <- bvLit sym 1 0
                       bvIte sym p v1 v2) vec
    V.foldM (\x y -> bvJoin sym y x) ZBV vec'
  
  
  
  
  ----------------------------------------------------------------------
  -- Generic wrapper for unary operators
  ----------------------------------------------------------------------
  
  -- | Type of unary operation on bitvectors
  type SWordUn =
    forall sym. IsExprBuilder sym =>
    sym -> SWord sym -> IO (SWord sym)
  
  -- | Convert a unary operation on length indexed bvs to a unary operation
  -- on `SWord`
  bvUn ::  forall sym. IsExprBuilder sym =>
     (forall w. 1 <= w => sym -> SymBV sym w -> IO (SymBV sym w)) ->
     sym -> SWord sym -> IO (SWord sym)
  bvUn f sym (DBV bv) = DBV <$> f sym bv
  bvUn _ _  ZBV = return ZBV
  
  ----------------------------------------------------------------------
  -- Generic wrapper for binary operators that take two words
  -- of the same length
  ----------------------------------------------------------------------
  
  -- | type of binary operation that returns a bitvector
  type SWordBin =
    forall sym. IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
  -- | type of binary operation that returns a boolean
  type PredBin =
    forall sym. IsExprBuilder sym =>
    sym -> SWord sym -> SWord sym -> IO (Pred sym)
  
  
  -- | convert binary operations that return bitvectors
  bvBin  :: forall sym. IsExprBuilder sym =>
    (forall w. 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)) ->
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
  bvBin f sym (DBV bv1) (DBV bv2)
    | Just Refl <- testEquality (W.exprType bv1) (W.exprType bv2)
    = DBV <$> f sym bv1 bv2
  bvBin _ _ ZBV ZBV
    = return ZBV
  bvBin _ _ x y
    = panic "bvBin" ["bit-vectors don't have same length", show (bvWidth x), show (bvWidth y)]
  
  
  -- | convert binary operations that return booleans (Pred)
  bvBinPred  :: forall sym. IsExprBuilder sym =>
    Bool {- ^ answer to give on 0-width bitvectors -} ->
    (forall w. 1 <= w => sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)) ->
    sym -> SWord sym -> SWord sym -> IO (Pred sym)
  bvBinPred _ f sym (DBV bv1) (DBV bv2)
    | Just Refl <- testEquality (W.exprType bv1) (W.exprType bv2)
    = f sym bv1 bv2
  bvBinPred b _ sym ZBV ZBV
    = pure (W.backendPred sym b)
  bvBinPred _ _ _ x y
    = panic "bvBinPred" ["bit-vectors don't have same length", show (bvWidth x), show (bvWidth y)]
  
   -- Bitvector logical
  
  -- | Bitwise complement
  bvNot :: SWordUn
  bvNot = bvUn W.bvNotBits
  
  -- | Bitwise logical and.
  bvAnd :: SWordBin
  bvAnd = bvBin W.bvAndBits
  
  -- | Bitwise logical or.
  bvOr :: SWordBin
  bvOr = bvBin W.bvOrBits
  
  -- | Bitwise logical exclusive or.
  bvXor :: SWordBin
  bvXor = bvBin W.bvXorBits
  
   -- Bitvector arithmetic
  
  -- | 2's complement negation.
  bvNeg :: SWordUn
  bvNeg = bvUn W.bvNeg
  
  -- | Add two bitvectors.
  bvAdd :: SWordBin
  bvAdd = bvBin W.bvAdd
  
  -- | Subtract one bitvector from another.
  bvSub :: SWordBin
  bvSub = bvBin W.bvSub
  
  -- | Multiply one bitvector by another.
  bvMul :: SWordBin
  bvMul = bvBin W.bvMul
  
  
  bvPopcount :: SWordUn
  bvPopcount = bvUn W.bvPopcount
  
  bvCountLeadingZeros :: SWordUn
  bvCountLeadingZeros = bvUn W.bvCountLeadingZeros
  
  bvCountTrailingZeros :: SWordUn
  bvCountTrailingZeros = bvUn W.bvCountTrailingZeros
  
  bvForall :: W.IsSymExprBuilder sym =>
    sym -> Natural -> (SWord sym -> IO (Pred sym)) -> IO (Pred sym)
  bvForall sym n f =
    case W.userSymbol "i" of
      Left err -> panic "bvForall" [show err]
      Right indexSymbol ->
        case mkNatRepr n of
          Some w
            | Just LeqProof <- testLeq (knownNat @1) w ->
                do i <- W.freshBoundVar sym indexSymbol $ W.BaseBVRepr w
                   body <- f . DBV $ W.varExpr sym i
                   W.forallPred sym i body
            | otherwise -> f ZBV
  
  -- | Unsigned bitvector division.
  --
  --   The result is undefined when @y@ is zero,
  --   but is otherwise equal to @floor( x / y )@.
  bvUDiv :: SWordBin
  bvUDiv = bvBin W.bvUdiv
  
  
  -- | Unsigned bitvector remainder.
  --
  --   The result is undefined when @y@ is zero,
  --   but is otherwise equal to @x - (bvUdiv x y) * y@.
  bvURem :: SWordBin
  bvURem = bvBin W.bvUrem
  
  -- | Signed bitvector division.  The result is truncated to zero.
  --
  --   The result of @bvSdiv x y@ is undefined when @y@ is zero,
  --   but is equal to @floor(x/y)@ when @x@ and @y@ have the same sign,
  --   and equal to @ceiling(x/y)@ when @x@ and @y@ have opposite signs.
  --
  --   NOTE! However, that there is a corner case when dividing @MIN_INT@ by
  --   @-1@, in which case an overflow condition occurs, and the result is instead
  --   @MIN_INT@.
  bvSDiv :: SWordBin
  bvSDiv = bvBin W.bvSdiv
  
  -- | Signed bitvector remainder.
  --
  --   The result of @bvSrem x y@ is undefined when @y@ is zero, but is
  --   otherwise equal to @x - (bvSdiv x y) * y@.
  bvSRem :: SWordBin
  bvSRem = bvBin W.bvSrem
  
  bvLg2 :: SWordUn
  bvLg2 = bvUn w_bvLg2
  
   -- Bitvector comparisons
  
  -- | Return true if bitvectors are equal.
  bvEq   :: PredBin
  bvEq = bvBinPred True W.bvEq
  
  -- | Signed less-than-or-equal.
  bvsle  :: PredBin
  bvsle = bvBinPred True W.bvSle
  
  -- | Signed less-than.
  bvslt  :: PredBin
  bvslt = bvBinPred False W.bvSlt
  
  -- | Unsigned less-than-or-equal.
  bvule  :: PredBin
  bvule = bvBinPred True W.bvUle
  
  -- | Unsigned less-than.
  bvult  :: PredBin
  bvult = bvBinPred False W.bvUlt
  
  -- | Signed greater-than-or-equal.
  bvsge  :: PredBin
  bvsge = bvBinPred True W.bvSge
  
  -- | Signed greater-than.
  bvsgt  :: PredBin
  bvsgt = bvBinPred False W.bvSgt
  
  -- | Unsigned greater-than-or-equal.
  bvuge  :: PredBin
  bvuge = bvBinPred True W.bvUge
  
  -- | Unsigned greater-than.
  bvugt  :: PredBin
  bvugt = bvBinPred False W.bvUgt
  
  bvIsNonzero :: IsExprBuilder sym => sym -> SWord sym -> IO (Pred sym)
  bvIsNonzero sym ZBV = return (W.falsePred sym)
  bvIsNonzero sym (DBV x) = W.bvIsNonzero sym x
  
  
  ----------------------------------------
  -- Bitvector shifts and rotates
  ----------------------------------------
  
  bvMin ::
    (IsExprBuilder sym, 1 <= w) =>
    sym ->
    W.SymBV sym w ->
    W.SymBV sym w ->
    IO (W.SymBV sym w)
  bvMin sym x y =
    do p <- W.bvUle sym x y
       W.bvIte sym p x y
  
  reduceShift ::
    IsExprBuilder sym =>
    (forall w. (1 <= w) => sym -> W.SymBV sym w -> W.SymBV sym w -> IO (W.SymBV sym w)) ->
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
  reduceShift _wop _sym ZBV _ = return ZBV
  reduceShift _wop _sym x ZBV = return x
  reduceShift wop sym (DBV x) (DBV y) =
    case compareNat (W.bvWidth x) (W.bvWidth y) of
  
      -- already the same size, apply the operation
      NatEQ -> DBV <$> wop sym x y
  
      -- y is shorter, zero extend
      NatGT _diff ->
        do y' <- W.bvZext sym (W.bvWidth x) y
           DBV <$> wop sym x y'
  
      -- y is longer, clamp to the width of x then truncate.
      -- Truncation is OK because the value will always fit after
      -- clamping.
      NatLT _diff ->
        do wx <- W.bvLit sym (W.bvWidth y) (BV.mkBV (W.bvWidth y) (intValue (W.bvWidth x)))
           y' <- W.bvTrunc sym (W.bvWidth x) =<< bvMin sym y wx
           DBV <$> wop sym x y'
  
  reduceRotate ::
    IsExprBuilder sym =>
    (forall w. (1 <= w) => sym -> W.SymBV sym w -> W.SymBV sym w -> IO (W.SymBV sym w)) ->
    sym -> SWord sym -> SWord sym -> IO (SWord sym)
  reduceRotate _wop _sym ZBV _ = return ZBV
  reduceRotate _wop _sym x ZBV = return x
  reduceRotate wop sym (DBV x) (DBV y) =
    case compareNat (W.bvWidth x) (W.bvWidth y) of
  
      -- already the same size, apply the operation
      NatEQ -> DBV <$> wop sym x y
  
      -- y is shorter, zero extend
      NatGT _diff ->
        do y' <- W.bvZext sym (W.bvWidth x) y
           DBV <$> wop sym x y'
  
      -- y is longer, reduce modulo the width of x, then truncate
      -- Truncation is OK because the value will always
      -- fit after modulo reduction
      NatLT _diff ->
        do wx <- W.bvLit sym (W.bvWidth y) (BV.mkBV (W.bvWidth y) (intValue (W.bvWidth x)))
           y' <- W.bvTrunc sym (W.bvWidth x) =<< W.bvUrem sym y wx
           DBV <$> wop sym x y'
  
  bvShl  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
  bvShl = reduceShift W.bvShl
  
  bvLshr  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
  bvLshr = reduceShift W.bvLshr
  
  bvAshr :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
  bvAshr = reduceShift W.bvAshr
  
  bvRol  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
  bvRol = reduceRotate W.bvRol
  
  bvRor  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
  bvRor = reduceRotate W.bvRor
  
  -- | Zero-extend a value, adding the specified number of bits.
  bvZext :: forall sym. IsExprBuilder sym => sym -> Natural -> SWord sym -> IO (SWord sym)
  bvZext sym n sw =
    case mkNatRepr n of
      Some (nr :: NatRepr n) ->
        case isPosNat nr of
          Nothing -> pure sw
          Just lp@LeqProof ->
            case sw of
              ZBV -> bvLit sym (toInteger n) 0
              DBV (x :: W.SymBV sym w) ->
                withLeqProof (leqAdd2 (leqRefl (W.bvWidth x)) lp :: LeqProof (w+1) (w+n)) $
                withLeqProof (leqAdd LeqProof nr :: LeqProof 1 (w+n)) $
                DBV <$> W.bvZext sym (addNat (W.bvWidth x) nr) x
  
  -- | Sign-extend a value, adding the specified number of bits.
  bvSext :: forall sym. IsExprBuilder sym => sym -> Natural -> SWord sym -> IO (SWord sym)
  bvSext sym n sw =
    case mkNatRepr n of
      Some (nr :: NatRepr n) ->
        case isPosNat nr of
          Nothing -> pure sw
          Just lp@LeqProof ->
            case sw of
              ZBV -> bvLit sym (toInteger n) 0
              DBV (x :: W.SymBV sym w) ->
                withLeqProof (leqAdd2 (leqRefl (W.bvWidth x)) lp :: LeqProof (w+1) (w+n)) $
                withLeqProof (leqAdd LeqProof nr :: LeqProof 1 (w+n)) $
                DBV <$> W.bvSext sym (addNat (W.bvWidth x) nr) x
  