------------------------------------------------------------------------
-- |
-- 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 (must be > 0)
  -> SWord sym -> IO (SWord sym)
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 _ _ _ ZBV = return ZBV

-- | 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 (must be > 0)
  -> SWord sym -> IO (SWord sym)
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 _ _ _ ZBV = return ZBV





-- | 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 x@(DBV bv1) y@(DBV bv2)
  | Just Refl <- testEquality (W.exprType bv1) (W.exprType bv2)
  = f sym bv1 bv2
  | otherwise
  = panic "bvBinPred" ["bit-vectors don't have same length", show (bvWidth x), show (bvWidth y)]
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
----------------------------------------

bvMax ::
  (IsExprBuilder sym, 1 <= w) =>
  sym ->
  W.SymBV sym w ->
  W.SymBV sym w ->
  IO (W.SymBV sym w)
bvMax sym x y =
  do p <- W.bvUge 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) =<< bvMax 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