------------------------------------------------------------------------
-- |
-- 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 :: SWord sym -> String
show (DBV SymBV sym w
bv) = forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (e :: BaseType -> Type) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W.printSymExpr SymBV sym w
bv
  show SWord sym
ZBV      = String
"0:[0]"

-------------------------------------------------------------

-- | Return the signed value if this is a constant bitvector
bvAsSignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
bvAsSignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
bvAsSignedInteger SWord sym
ZBV = forall a. a -> Maybe a
Just Integer
0
bvAsSignedInteger (DBV (SymBV sym w
bv :: SymBV sym w)) =
  forall (w :: Natural). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
W.asBV SymBV sym w
bv

-- | Return the unsigned value if this is a constant bitvector
bvAsUnsignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
bvAsUnsignedInteger :: forall sym. IsExprBuilder sym => SWord sym -> Maybe Integer
bvAsUnsignedInteger SWord sym
ZBV = forall a. a -> Maybe a
Just Integer
0
bvAsUnsignedInteger (DBV (SymBV sym w
bv :: SymBV sym w)) =
  forall (w :: Natural). BV w -> Integer
BV.asUnsigned forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> Maybe (BV w)
W.asBV SymBV sym w
bv


unsignedBVBounds :: forall sym. IsExprBuilder sym => SWord sym -> Maybe (Integer, Integer)
unsignedBVBounds :: forall sym.
IsExprBuilder sym =>
SWord sym -> Maybe (Integer, Integer)
unsignedBVBounds SWord sym
ZBV = forall a. a -> Maybe a
Just (Integer
0, Integer
0)
unsignedBVBounds (DBV SymBV sym w
bv) = forall (e :: BaseType -> Type) (w :: Natural).
(IsExpr e, 1 <= w) =>
e (BaseBVType w) -> Maybe (Integer, Integer)
W.unsignedBVBounds SymBV sym w
bv

signedBVBounds :: forall sym. IsExprBuilder sym => SWord sym -> Maybe (Integer, Integer)
signedBVBounds :: forall sym.
IsExprBuilder sym =>
SWord sym -> Maybe (Integer, Integer)
signedBVBounds SWord sym
ZBV = forall a. a -> Maybe a
Just (Integer
0, Integer
0)
signedBVBounds (DBV SymBV sym w
bv) = forall (e :: BaseType -> Type) (w :: Natural).
(IsExpr e, 1 <= w) =>
e (BaseBVType w) -> Maybe (Integer, Integer)
W.signedBVBounds SymBV sym w
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 :: forall sym width.
(Show width, Integral width, IsExprBuilder sym) =>
sym -> SymInteger sym -> width -> IO (SWord sym)
integerToBV sym
sym SymInteger sym
i width
w
  | Just (Some NatRepr x
wr) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat width
w
  , Just LeqProof 1 x
LeqProof  <- forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
wr
  = forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymInteger sym -> NatRepr w -> IO (SymBV sym w)
W.integerToBV sym
sym SymInteger sym
i NatRepr x
wr
  | Integer
0 forall a. Eq a => a -> a -> Bool
== forall a. Integral a => a -> Integer
toInteger width
w
  = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall sym. SWord sym
ZBV
  | Bool
otherwise
  = forall a. HasCallStack => String -> [String] -> a
panic String
"integerToBV" [String
"invalid bit-width", forall a. Show a => a -> String
show width
w]

-- | Interpret the bit-vector as an unsigned integer
bvToInteger :: forall sym. (IsExprBuilder sym) =>
  sym -> SWord sym -> IO (SymInteger sym)
bvToInteger :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> IO (SymInteger sym)
bvToInteger sym
sym SWord sym
ZBV      = forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W.intLit sym
sym Integer
0
bvToInteger sym
sym (DBV SymBV sym w
bv) = forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
W.bvToInteger sym
sym SymBV sym w
bv

-- | Interpret the bit-vector as a signed integer
sbvToInteger :: forall sym. (IsExprBuilder sym) =>
  sym -> SWord sym -> IO (SymInteger sym)
sbvToInteger :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> IO (SymInteger sym)
sbvToInteger sym
sym SWord sym
ZBV      = forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W.intLit sym
sym Integer
0
sbvToInteger sym
sym (DBV SymBV sym w
bv) = forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymInteger sym)
W.sbvToInteger sym
sym SymBV sym w
bv


-- | Get the width of a bitvector
bvWidth :: forall sym. SWord sym -> Integer
bvWidth :: forall sym. SWord sym -> Integer
bvWidth (DBV SymBV sym w
x) = forall a. Num a => Integer -> a
fromInteger (forall (n :: Natural). NatRepr n -> Integer
intValue (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x))
bvWidth SWord sym
ZBV = Integer
0

-- | Create a bitvector with the given width and value
bvLit :: forall sym. IsExprBuilder sym =>
  sym -> Integer -> Integer -> IO (SWord sym)
bvLit :: forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
_ Integer
w Integer
_
  | Integer
w forall a. Eq a => a -> a -> Bool
== Integer
0
  = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall sym. SWord sym
ZBV
bvLit sym
sym Integer
w Integer
dat
  | Just (Some NatRepr x
rw) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
w
  , Just LeqProof 1 x
LeqProof <- forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
rw
  = forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W.bvLit sym
sym NatRepr x
rw (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
rw Integer
dat)
  | Bool
otherwise
  = forall a. HasCallStack => String -> [String] -> a
panic String
"bvLit" [String
"size of bitvector is < 0 or >= maxInt", forall a. Show a => a -> String
show Integer
w]


freshBV :: forall sym. IsSymExprBuilder sym =>
  sym -> W.SolverSymbol -> Integer -> IO (SWord sym)
freshBV :: forall sym.
IsSymExprBuilder sym =>
sym -> SolverSymbol -> Integer -> IO (SWord sym)
freshBV sym
sym SolverSymbol
nm Integer
w
  | Integer
w forall a. Eq a => a -> a -> Bool
== Integer
0
  = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall sym. SWord sym
ZBV

  | Just (Some NatRepr x
rw) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
w
  , Just LeqProof 1 x
LeqProof <- forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
rw
  = forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
W.freshConstant sym
sym SolverSymbol
nm (forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W.BaseBVRepr NatRepr x
rw)

  | Bool
otherwise
  = forall a. HasCallStack => String -> [String] -> a
panic String
"freshBV" [String
"size of bitvector is < 0 or >= maxInt", forall a. Show a => a -> String
show Integer
w]


bvFill :: forall sym. IsExprBuilder sym =>
  sym -> Integer -> Pred sym -> IO (SWord sym)
bvFill :: forall sym.
IsExprBuilder sym =>
sym -> Integer -> Pred sym -> IO (SWord sym)
bvFill sym
sym Integer
w Pred sym
p
  | Integer
w forall a. Eq a => a -> a -> Bool
== Integer
0
  = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall sym. SWord sym
ZBV

  | Just (Some NatRepr x
rw) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
w
  , Just LeqProof 1 x
LeqProof <- forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
rw
  = forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> Pred sym -> IO (SymBV sym w)
W.bvFill sym
sym NatRepr x
rw Pred sym
p

  | Bool
otherwise
  = forall a. HasCallStack => String -> [String] -> a
panic String
"bvFill" [String
"size of bitvector is < 0 or >= maxInt", forall a. Show a => a -> String
show Integer
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 :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> Integer -> IO (Pred sym)
bvAtBE sym
sym (DBV SymBV sym w
bv) Integer
i = do
  let w :: Natural
w   = forall (n :: Natural). NatRepr n -> Natural
natValue (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv)
  let idx :: Natural
idx = Natural
w forall a. Num a => a -> a -> a
- Natural
1 forall a. Num a => a -> a -> a
- forall a. Num a => Integer -> a
fromInteger Integer
i
  forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Natural -> SymBV sym w -> IO (Pred sym)
W.testBitBV sym
sym Natural
idx SymBV sym w
bv
bvAtBE sym
_ SWord sym
ZBV Integer
_ = forall a. HasCallStack => String -> [String] -> a
panic String
"bvAtBE" [String
"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 :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> Integer -> IO (Pred sym)
bvAtLE sym
sym (DBV SymBV sym w
bv) Integer
i =
  forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Natural -> SymBV sym w -> IO (Pred sym)
W.testBitBV sym
sym (forall a. Num a => Integer -> a
fromInteger Integer
i) SymBV sym w
bv
bvAtLE sym
_ SWord sym
ZBV Integer
_ = forall a. HasCallStack => String -> [String] -> a
panic String
"bvAtLE" [String
"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 :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> Integer -> Pred sym -> IO (SWord sym)
bvSetBE sym
_ SWord sym
ZBV Integer
_ Pred sym
_ = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall sym. SWord sym
ZBV
bvSetBE sym
sym (DBV SymBV sym w
bv) Integer
i Pred sym
b =
  do let w :: Natural
w = forall (n :: Natural). NatRepr n -> Natural
natValue (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv)
     let idx :: Natural
idx = Natural
w forall a. Num a => a -> a -> a
- Natural
1 forall a. Num a => a -> a -> a
- forall a. Num a => Integer -> a
fromInteger Integer
i
     forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> Natural -> Pred sym -> IO (SymBV sym w)
W.bvSet sym
sym SymBV sym w
bv Natural
idx Pred sym
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 :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> Integer -> Pred sym -> IO (SWord sym)
bvSetLE sym
_ SWord sym
ZBV Integer
_ Pred sym
_ = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall sym. SWord sym
ZBV
bvSetLE sym
sym (DBV SymBV sym w
bv) Integer
i Pred sym
b =
  forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> Natural -> Pred sym -> IO (SymBV sym w)
W.bvSet sym
sym SymBV sym w
bv (forall a. Num a => Integer -> a
fromInteger Integer
i) Pred sym
b


-- | Concatenate two bitvectors.
bvJoin  :: forall sym. IsExprBuilder sym => sym
  -> SWord sym
  -- ^ most significant bits
  -> SWord sym
  -- ^ least significant bits
  -> IO (SWord sym)
bvJoin :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvJoin sym
_ SWord sym
x SWord sym
ZBV = forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
x
bvJoin sym
_ SWord sym
ZBV SWord sym
x = forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
x
bvJoin sym
sym (DBV SymBV sym w
bv1) (DBV SymBV sym w
bv2)
  | LeqProof 1 (w + w)
LeqProof <- forall (m :: Natural) (n :: Natural) (p :: Natural -> Type)
       (q :: Natural -> Type).
(1 <= m, 1 <= n) =>
p m -> q n -> LeqProof 1 (m + n)
leqAddPos (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv1) (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv2)
  = forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (v :: Natural).
(IsExprBuilder sym, 1 <= u, 1 <= v) =>
sym -> SymBV sym u -> SymBV sym v -> IO (SymBV sym (u + v))
W.bvConcat sym
sym SymBV sym w
bv1 SymBV sym w
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 :: forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
bvSliceBE sym
_ Integer
_m Integer
0 SWord sym
_  = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure forall sym. SWord sym
ZBV
bvSliceBE sym
sym Integer
m Integer
n (DBV SymBV sym w
bv)
  | Just (Some NatRepr x
nr) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
n,
    Just LeqProof 1 x
LeqProof  <- forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
nr,
    Just (Some NatRepr x
mr) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
m,
    let wr :: NatRepr w
wr = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv,
    Just LeqProof (x + x) w
LeqProof <- forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr x
mr NatRepr x
nr)  NatRepr w
wr,
    let idx :: NatRepr (w - (x + x))
idx = forall (n :: Natural) (m :: Natural).
(n <= m) =>
NatRepr m -> NatRepr n -> NatRepr (m - n)
subNat NatRepr w
wr (forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr x
mr NatRepr x
nr),
    Just LeqProof ((w - (x + x)) + x) w
LeqProof <- forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr (w - (x + x))
idx NatRepr x
nr) NatRepr w
wr
  = forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (idx :: Natural) (n :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
W.bvSelect sym
sym NatRepr (w - (x + x))
idx NatRepr x
nr SymBV sym w
bv
  | Bool
otherwise
  = forall a. HasCallStack => String -> [String] -> a
panic String
"bvSliceBE"
      [String
"invalid arguments to slice: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
m forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n
        forall a. [a] -> [a] -> [a]
++ String
" from vector of length " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv)]
bvSliceBE sym
_ Integer
m Integer
n SWord sym
ZBV
  = forall a. HasCallStack => String -> [String] -> a
panic String
"bvSliceBE"
      [String
"invalid arguments to slice: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
m forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n
        forall a. [a] -> [a] -> [a]
++ String
" 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 :: forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
bvSliceLE sym
_ Integer
_m Integer
0 SWord sym
_  = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall sym. SWord sym
ZBV
bvSliceLE sym
sym Integer
m Integer
n (DBV SymBV sym w
bv)
  | Just (Some NatRepr x
nr) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
n,
    Just LeqProof 1 x
LeqProof  <- forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
nr,
    Just (Some NatRepr x
mr) <- forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
m,
    let wr :: NatRepr w
wr = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv,
    Just LeqProof (x + x) w
LeqProof <- forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr x
mr NatRepr x
nr) NatRepr w
wr
  = forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (idx :: Natural) (n :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= n, (idx + n) <= w) =>
sym -> NatRepr idx -> NatRepr n -> SymBV sym w -> IO (SymBV sym n)
W.bvSelect sym
sym NatRepr x
mr NatRepr x
nr SymBV sym w
bv

  | Bool
otherwise
  = forall a. HasCallStack => String -> [String] -> a
panic String
"bvSliceLE"
      [String
"invalid arguments to slice: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
m forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n
        forall a. [a] -> [a] -> [a]
++ String
" from vector of length " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv)]
bvSliceLE sym
_ Integer
m Integer
n SWord sym
ZBV
  = forall a. HasCallStack => String -> [String] -> a
panic String
"bvSliceLE"
      [String
"invalid arguments to slice: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
m forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
n
        forall a. [a] -> [a] -> [a]
++ String
" 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 :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
w_bvLg2 sym
sym SymBV sym w
x = Integer -> IO (SymBV sym w)
go Integer
0
  where
    w :: NatRepr w
w = forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x
    size :: Integer
    size :: Integer
size = forall (n :: Natural). NatRepr n -> Integer
intValue NatRepr w
w
    lit :: Integer -> IO (SymBV sym w)
    -- BGS: This change could lead to some inefficency
    lit :: Integer -> IO (SymBV sym w)
lit Integer
n = forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W.bvLit sym
sym NatRepr w
w (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr w
w Integer
n)
    go :: Integer -> IO (SymBV sym w)
    go :: Integer -> IO (SymBV sym w)
go Integer
i | Integer
i forall a. Ord a => a -> a -> Bool
< Integer
size = do
           SymBV sym w
x' <- Integer -> IO (SymBV sym w)
lit (Integer
2 forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
i)
           SymExpr sym BaseBoolType
b' <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvUle sym
sym SymBV sym w
x SymBV sym w
x'
           SymBV sym w
th <- Integer -> IO (SymBV sym w)
lit Integer
i
           SymBV sym w
el <- Integer -> IO (SymBV sym w)
go (Integer
i forall a. Num a => a -> a -> a
+ Integer
1)
           forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvIte sym
sym SymExpr sym BaseBoolType
b' SymBV sym w
th SymBV sym w
el
         | Bool
otherwise    = Integer -> IO (SymBV sym w)
lit Integer
i

-- | If-then-else applied to bitvectors.
bvIte :: forall sym. IsExprBuilder sym =>
  sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvIte :: forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvIte sym
_ Pred sym
_ SWord sym
ZBV SWord sym
ZBV
  = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall sym. SWord sym
ZBV
bvIte sym
sym Pred sym
p (DBV SymBV sym w
bv1) (DBV SymBV sym w
bv2)
  | Just BaseBVType w :~: BaseBVType w
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W.exprType SymBV sym w
bv1) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W.exprType SymBV sym w
bv2)
  = forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvIte sym
sym Pred sym
p SymBV sym w
bv1 SymBV sym w
bv2
bvIte sym
_ Pred sym
_ SWord sym
x SWord sym
y
  = forall a. HasCallStack => String -> [String] -> a
panic String
"bvIte" [String
"bit-vectors don't have same length", forall a. Show a => a -> String
show (forall sym. SWord sym -> Integer
bvWidth SWord sym
x), forall a. Show a => a -> String
show (forall sym. SWord sym -> Integer
bvWidth SWord sym
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 :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> IO (Vector (Pred sym))
bvUnpackBE sym
_   SWord sym
ZBV = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Vector a
V.empty
bvUnpackBE sym
sym (DBV SymBV sym w
bv) = do
  let w :: Natural
      w :: Natural
w = forall (n :: Natural). NatRepr n -> Natural
natValue (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv)
  forall (m :: Type -> Type) a.
Monad m =>
Int -> (Int -> m a) -> m (Vector a)
V.generateM (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
w)
              (\Int
i -> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Natural -> SymBV sym w -> IO (Pred sym)
W.testBitBV sym
sym (Natural
w forall a. Num a => a -> a -> a
- Natural
1 forall a. Num a => a -> a -> a
- forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i) SymBV sym w
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 :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> IO (Vector (Pred sym))
bvUnpackLE sym
_   SWord sym
ZBV = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a. Vector a
V.empty
bvUnpackLE sym
sym (DBV SymBV sym w
bv) = do
  let w :: Natural
      w :: Natural
w = forall (n :: Natural). NatRepr n -> Natural
natValue (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv)
  forall (m :: Type -> Type) a.
Monad m =>
Int -> (Int -> m a) -> m (Vector a)
V.generateM (forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
w)
              (\Int
i -> forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Natural -> SymBV sym w -> IO (Pred sym)
W.testBitBV sym
sym (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
i) SymBV sym w
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 :: forall sym.
(IsExpr (SymExpr sym), IsExprBuilder sym) =>
sym -> Vector (Pred sym) -> IO (SWord sym)
bvPackBE sym
sym Vector (Pred sym)
vec = do
  Vector (SWord sym)
vec' <- forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Vector a -> m (Vector b)
V.mapM (\Pred sym
p -> do
                     SWord sym
v1 <- forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
sym Integer
1 Integer
1
                     SWord sym
v2 <- forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
sym Integer
1 Integer
0
                     forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvIte sym
sym Pred sym
p SWord sym
v1 SWord sym
v2) Vector (Pred sym)
vec
  forall (m :: Type -> Type) a b.
Monad m =>
(a -> b -> m a) -> a -> Vector b -> m a
V.foldM (\SWord sym
x SWord sym
y -> forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvJoin sym
sym SWord sym
x SWord sym
y) forall sym. SWord sym
ZBV Vector (SWord sym)
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 :: forall sym.
(IsExpr (SymExpr sym), IsExprBuilder sym) =>
sym -> Vector (Pred sym) -> IO (SWord sym)
bvPackLE sym
sym Vector (Pred sym)
vec = do
  Vector (SWord sym)
vec' <- forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Vector a -> m (Vector b)
V.mapM (\Pred sym
p -> do
                     SWord sym
v1 <- forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
sym Integer
1 Integer
1
                     SWord sym
v2 <- forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
sym Integer
1 Integer
0
                     forall sym.
IsExprBuilder sym =>
sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvIte sym
sym Pred sym
p SWord sym
v1 SWord sym
v2) Vector (Pred sym)
vec
  forall (m :: Type -> Type) a b.
Monad m =>
(a -> b -> m a) -> a -> Vector b -> m a
V.foldM (\SWord sym
x SWord sym
y -> forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvJoin sym
sym SWord sym
y SWord sym
x) forall sym. SWord sym
ZBV Vector (SWord sym)
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 :: forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> IO (SWord sym)
bvUn forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
f sym
sym (DBV SymBV sym w
bv) = forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
f sym
sym SymBV sym w
bv
bvUn forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
_ sym
_  SWord sym
ZBV = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall sym. SWord sym
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 :: forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvBin forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
f sym
sym (DBV SymBV sym w
bv1) (DBV SymBV sym w
bv2)
  | Just BaseBVType w :~: BaseBVType w
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W.exprType SymBV sym w
bv1) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W.exprType SymBV sym w
bv2)
  = forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
f sym
sym SymBV sym w
bv1 SymBV sym w
bv2
bvBin forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
_ sym
_ SWord sym
ZBV SWord sym
ZBV
  = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall sym. SWord sym
ZBV
bvBin forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
_ sym
_ SWord sym
x SWord sym
y
  = forall a. HasCallStack => String -> [String] -> a
panic String
"bvBin" [String
"bit-vectors don't have same length", forall a. Show a => a -> String
show (forall sym. SWord sym -> Integer
bvWidth SWord sym
x), forall a. Show a => a -> String
show (forall sym. SWord sym -> Integer
bvWidth SWord sym
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 :: forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
bvBinPred Bool
_ forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
f sym
sym (DBV SymBV sym w
bv1) (DBV SymBV sym w
bv2)
  | Just BaseBVType w :~: BaseBVType w
Refl <- forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W.exprType SymBV sym w
bv1) (forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W.exprType SymBV sym w
bv2)
  = forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
f sym
sym SymBV sym w
bv1 SymBV sym w
bv2
bvBinPred Bool
b forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
_ sym
sym SWord sym
ZBV SWord sym
ZBV
  = forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
W.backendPred sym
sym Bool
b)
bvBinPred Bool
_ forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
_ sym
_ SWord sym
x SWord sym
y
  = forall a. HasCallStack => String -> [String] -> a
panic String
"bvBinPred" [String
"bit-vectors don't have same length", forall a. Show a => a -> String
show (forall sym. SWord sym -> Integer
bvWidth SWord sym
x), forall a. Show a => a -> String
show (forall sym. SWord sym -> Integer
bvWidth SWord sym
y)]

 -- Bitvector logical

-- | Bitwise complement
bvNot :: SWordUn
bvNot :: SWordUn
bvNot = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> IO (SWord sym)
bvUn forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W.bvNotBits

-- | Bitwise logical and.
bvAnd :: SWordBin
bvAnd :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvAnd = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvBin forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvAndBits

-- | Bitwise logical or.
bvOr :: SWordBin
bvOr :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvOr = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvBin forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvOrBits

-- | Bitwise logical exclusive or.
bvXor :: SWordBin
bvXor :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvXor = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvBin forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvXorBits

 -- Bitvector arithmetic

-- | 2's complement negation.
bvNeg :: SWordUn
bvNeg :: SWordUn
bvNeg = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> IO (SWord sym)
bvUn forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W.bvNeg

-- | Add two bitvectors.
bvAdd :: SWordBin
bvAdd :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvAdd = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvBin forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvAdd

-- | Subtract one bitvector from another.
bvSub :: SWordBin
bvSub :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvSub = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvBin forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvSub

-- | Multiply one bitvector by another.
bvMul :: SWordBin
bvMul :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvMul = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvBin forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvMul


bvPopcount :: SWordUn
bvPopcount :: SWordUn
bvPopcount = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> IO (SWord sym)
bvUn forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W.bvPopcount

bvCountLeadingZeros :: SWordUn
bvCountLeadingZeros :: SWordUn
bvCountLeadingZeros = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> IO (SWord sym)
bvUn forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W.bvCountLeadingZeros

bvCountTrailingZeros :: SWordUn
bvCountTrailingZeros :: SWordUn
bvCountTrailingZeros = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> IO (SWord sym)
bvUn forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
W.bvCountTrailingZeros

bvForall :: W.IsSymExprBuilder sym =>
  sym -> Natural -> (SWord sym -> IO (Pred sym)) -> IO (Pred sym)
bvForall :: forall sym.
IsSymExprBuilder sym =>
sym -> Natural -> (SWord sym -> IO (Pred sym)) -> IO (Pred sym)
bvForall sym
sym Natural
n SWord sym -> IO (Pred sym)
f =
  case String -> Either SolverSymbolError SolverSymbol
W.userSymbol String
"i" of
    Left SolverSymbolError
err -> forall a. HasCallStack => String -> [String] -> a
panic String
"bvForall" [forall a. Show a => a -> String
show SolverSymbolError
err]
    Right SolverSymbol
indexSymbol ->
      case Natural -> Some NatRepr
mkNatRepr Natural
n of
        Some NatRepr x
w
          | Just LeqProof 1 x
LeqProof <- forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (forall (n :: Natural). KnownNat n => NatRepr n
knownNat @1) NatRepr x
w ->
              do BoundVar sym ('BaseBVType x)
i <- forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
W.freshBoundVar sym
sym SolverSymbol
indexSymbol forall a b. (a -> b) -> a -> b
$ forall (w :: Natural).
(1 <= w) =>
NatRepr w -> BaseTypeRepr ('BaseBVType w)
W.BaseBVRepr NatRepr x
w
                 Pred sym
body <- SWord sym -> IO (Pred sym)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall a b. (a -> b) -> a -> b
$ forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> SymExpr sym tp
W.varExpr sym
sym BoundVar sym ('BaseBVType x)
i
                 forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> Pred sym -> IO (Pred sym)
W.forallPred sym
sym BoundVar sym ('BaseBVType x)
i Pred sym
body
          | Bool
otherwise -> SWord sym -> IO (Pred sym)
f forall sym. SWord sym
ZBV

-- | Unsigned bitvector division.
--
--   The result is undefined when @y@ is zero,
--   but is otherwise equal to @floor( x / y )@.
bvUDiv :: SWordBin
bvUDiv :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvUDiv = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvBin forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
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 :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvURem = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvBin forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
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 :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvSDiv = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvBin forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
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 :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvSRem = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvBin forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvSrem

bvLg2 :: SWordUn
bvLg2 :: SWordUn
bvLg2 = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> IO (SWord sym)
bvUn forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
w_bvLg2

 -- Bitvector comparisons

-- | Return true if bitvectors are equal.
bvEq   :: PredBin
bvEq :: PredBin
bvEq = forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
bvBinPred Bool
True forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvEq

-- | Signed less-than-or-equal.
bvsle  :: PredBin
bvsle :: PredBin
bvsle = forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
bvBinPred Bool
True forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvSle

-- | Signed less-than.
bvslt  :: PredBin
bvslt :: PredBin
bvslt = forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
bvBinPred Bool
False forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvSlt

-- | Unsigned less-than-or-equal.
bvule  :: PredBin
bvule :: PredBin
bvule = forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
bvBinPred Bool
True forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvUle

-- | Unsigned less-than.
bvult  :: PredBin
bvult :: PredBin
bvult = forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
bvBinPred Bool
False forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvUlt

-- | Signed greater-than-or-equal.
bvsge  :: PredBin
bvsge :: PredBin
bvsge = forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
bvBinPred Bool
True forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvSge

-- | Signed greater-than.
bvsgt  :: PredBin
bvsgt :: PredBin
bvsgt = forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
bvBinPred Bool
False forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvSgt

-- | Unsigned greater-than-or-equal.
bvuge  :: PredBin
bvuge :: PredBin
bvuge = forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
bvBinPred Bool
True forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvUge

-- | Unsigned greater-than.
bvugt  :: PredBin
bvugt :: PredBin
bvugt = forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Natural).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
bvBinPred Bool
False forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvUgt

bvIsNonzero :: IsExprBuilder sym => sym -> SWord sym -> IO (Pred sym)
bvIsNonzero :: forall sym. IsExprBuilder sym => sym -> SWord sym -> IO (Pred sym)
bvIsNonzero sym
sym SWord sym
ZBV = forall (m :: Type -> Type) a. Monad m => a -> m a
return (forall sym. IsExprBuilder sym => sym -> Pred sym
W.falsePred sym
sym)
bvIsNonzero sym
sym (DBV SymBV sym w
x) = forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (Pred sym)
W.bvIsNonzero sym
sym SymBV sym w
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 :: forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMin sym
sym SymBV sym w
x SymBV sym w
y =
  do SymExpr sym BaseBoolType
p <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvUle sym
sym SymBV sym w
x SymBV sym w
y
     forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvIte sym
sym SymExpr sym BaseBoolType
p SymBV sym w
x SymBV sym w
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 :: forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
reduceShift forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
_wop sym
_sym SWord sym
ZBV SWord sym
_ = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall sym. SWord sym
ZBV
reduceShift forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
_wop sym
_sym SWord sym
x SWord sym
ZBV = forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
x
reduceShift forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
wop sym
sym (DBV SymBV sym w
x) (DBV SymBV sym w
y) =
  case forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x) (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
y) of

    -- already the same size, apply the operation
    NatComparison w w
NatEQ -> forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
wop sym
sym SymBV sym w
x SymBV sym w
y

    -- y is shorter, zero extend
    NatGT NatRepr y
_diff ->
      do SymBV sym w
y' <- forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
W.bvZext sym
sym (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x) SymBV sym w
y
         forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
wop sym
sym SymBV sym w
x SymBV sym w
y'

    -- y is longer, clamp to the width of x then truncate.
    -- Truncation is OK because the value will always fit after
    -- clamping.
    NatLT NatRepr y
_diff ->
      do SymBV sym w
wx <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W.bvLit sym
sym (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
y) (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
y) (forall (n :: Natural). NatRepr n -> Integer
intValue (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x)))
         SymBV sym w
y' <- forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
W.bvTrunc sym
sym (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x) forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
bvMin sym
sym SymBV sym w
y SymBV sym w
wx
         forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
wop sym
sym SymBV sym w
x SymBV sym w
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 :: forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
reduceRotate forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
_wop sym
_sym SWord sym
ZBV SWord sym
_ = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall sym. SWord sym
ZBV
reduceRotate forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
_wop sym
_sym SWord sym
x SWord sym
ZBV = forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
x
reduceRotate forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
wop sym
sym (DBV SymBV sym w
x) (DBV SymBV sym w
y) =
  case forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatComparison m n
compareNat (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x) (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
y) of

    -- already the same size, apply the operation
    NatComparison w w
NatEQ -> forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
wop sym
sym SymBV sym w
x SymBV sym w
y

    -- y is shorter, zero extend
    NatGT NatRepr y
_diff ->
      do SymBV sym w
y' <- forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
W.bvZext sym
sym (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x) SymBV sym w
y
         forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
wop sym
sym SymBV sym w
x SymBV sym w
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 NatRepr y
_diff ->
      do SymBV sym w
wx <- forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W.bvLit sym
sym (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
y) (forall (w :: Natural). NatRepr w -> Integer -> BV w
BV.mkBV (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
y) (forall (n :: Natural). NatRepr n -> Integer
intValue (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x)))
         SymBV sym w
y' <- forall sym (r :: Natural) (w :: Natural).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
W.bvTrunc sym
sym (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x) forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvUrem sym
sym SymBV sym w
y SymBV sym w
wx
         forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (w :: Natural).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
wop sym
sym SymBV sym w
x SymBV sym w
y'

bvShl  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvShl :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvShl = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
reduceShift forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvShl

bvLshr  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvLshr :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvLshr = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
reduceShift forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvLshr

bvAshr :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvAshr :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvAshr = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
reduceShift forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvAshr

bvRol  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvRol :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvRol = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
reduceRotate forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvRol

bvRor  :: W.IsExprBuilder sym => sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvRor :: forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvRor = forall sym.
IsExprBuilder sym =>
(forall (w :: Natural).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
reduceRotate forall sym (w :: Natural).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
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 :: forall sym.
IsExprBuilder sym =>
sym -> Natural -> SWord sym -> IO (SWord sym)
bvZext sym
sym Natural
n SWord sym
sw =
  case Natural -> Some NatRepr
mkNatRepr Natural
n of
    Some (NatRepr x
nr :: NatRepr n) ->
      case forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
nr of
        Maybe (LeqProof 1 x)
Nothing -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SWord sym
sw
        Just lp :: LeqProof 1 x
lp@LeqProof 1 x
LeqProof ->
          case SWord sym
sw of
            SWord sym
ZBV -> forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
sym (forall a. Integral a => a -> Integer
toInteger Natural
n) Integer
0
            DBV (SymBV sym w
x :: W.SymBV sym w) ->
              forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
       (y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 (forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
leqRefl (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x)) LeqProof 1 x
lp :: LeqProof (w+1) (w+n)) forall a b. (a -> b) -> a -> b
$
              forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof NatRepr x
nr :: LeqProof 1 (w+n)) forall a b. (a -> b) -> a -> b
$
              forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
W.bvZext sym
sym (forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x) NatRepr x
nr) SymBV sym w
x

-- | Sign-extend a value, adding the specified number of bits.
bvSext :: forall sym. IsExprBuilder sym => sym -> Natural -> SWord sym -> IO (SWord sym)
bvSext :: forall sym.
IsExprBuilder sym =>
sym -> Natural -> SWord sym -> IO (SWord sym)
bvSext sym
sym Natural
n SWord sym
sw =
  case Natural -> Some NatRepr
mkNatRepr Natural
n of
    Some (NatRepr x
nr :: NatRepr n) ->
      case forall (n :: Natural). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
nr of
        Maybe (LeqProof 1 x)
Nothing -> forall (f :: Type -> Type) a. Applicative f => a -> f a
pure SWord sym
sw
        Just lp :: LeqProof 1 x
lp@LeqProof 1 x
LeqProof ->
          case SWord sym
sw of
            SWord sym
ZBV -> forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
sym (forall a. Integral a => a -> Integer
toInteger Natural
n) Integer
0
            DBV (SymBV sym w
x :: W.SymBV sym w) ->
              forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (forall (x_l :: Natural) (x_h :: Natural) (y_l :: Natural)
       (y_h :: Natural).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 (forall (f :: Natural -> Type) (n :: Natural). f n -> LeqProof n n
leqRefl (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x)) LeqProof 1 x
lp :: LeqProof (w+1) (w+n)) forall a b. (a -> b) -> a -> b
$
              forall (m :: Natural) (n :: Natural) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (forall (f :: Natural -> Type) (m :: Natural) (n :: Natural)
       (p :: Natural).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd forall (m :: Natural) (n :: Natural). (m <= n) => LeqProof m n
LeqProof NatRepr x
nr :: LeqProof 1 (w+n)) forall a b. (a -> b) -> a -> b
$
              forall sym (w :: Natural).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall sym (u :: Natural) (r :: Natural).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
W.bvSext sym
sym (forall (m :: Natural) (n :: Natural).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (forall (e :: BaseType -> Type) (w :: Natural).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x) NatRepr x
nr) SymBV sym w
x