------------------------------------------------------------------------
-- |
-- 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) = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> Doc Any -> String
forall a b. (a -> b) -> a -> b
$ SymBV sym w -> Doc Any
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 :: SWord sym -> Maybe Integer
bvAsSignedInteger SWord sym
ZBV = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
bvAsSignedInteger (DBV (bv :: SymBV sym w)) =
  NatRepr w -> BV w -> Integer
forall (w :: Nat). (1 <= w) => NatRepr w -> BV w -> Integer
BV.asSigned (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv) (BV w -> Integer) -> Maybe (BV w) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym w -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Nat).
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 :: SWord sym -> Maybe Integer
bvAsUnsignedInteger SWord sym
ZBV = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
bvAsUnsignedInteger (DBV (bv :: SymBV sym w)) =
  BV w -> Integer
forall (w :: Nat). BV w -> Integer
BV.asUnsigned (BV w -> Integer) -> Maybe (BV w) -> Maybe Integer
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> SymBV sym w -> Maybe (BV w)
forall (e :: BaseType -> Type) (w :: Nat).
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 :: SWord sym -> Maybe (Integer, Integer)
unsignedBVBounds SWord sym
ZBV = (Integer, Integer) -> Maybe (Integer, Integer)
forall a. a -> Maybe a
Just (Integer
0, Integer
0)
unsignedBVBounds (DBV SymBV sym w
bv) = SymBV sym w -> Maybe (Integer, Integer)
forall (e :: BaseType -> Type) (w :: Nat).
(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 :: SWord sym -> Maybe (Integer, Integer)
signedBVBounds SWord sym
ZBV = (Integer, Integer) -> Maybe (Integer, Integer)
forall a. a -> Maybe a
Just (Integer
0, Integer
0)
signedBVBounds (DBV SymBV sym w
bv) = SymBV sym w -> Maybe (Integer, Integer)
forall (e :: BaseType -> Type) (w :: Nat).
(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 :: sym -> SymInteger sym -> width -> IO (SWord sym)
integerToBV sym
sym SymInteger sym
i width
w
  | Just (Some NatRepr x
wr) <- width -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat width
w
  , Just LeqProof 1 x
LeqProof  <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
wr
  = SymExpr sym ('BaseBVType x) -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymExpr sym ('BaseBVType x) -> SWord sym)
-> IO (SymExpr sym ('BaseBVType x)) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymInteger sym -> NatRepr x -> IO (SymExpr sym ('BaseBVType x))
forall sym (w :: Nat).
(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 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== width -> Integer
forall a. Integral a => a -> Integer
toInteger width
w
  = SWord sym -> IO (SWord sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
forall sym. SWord sym
ZBV
  | Bool
otherwise
  = String -> [String] -> IO (SWord sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"integerToBV" [String
"invalid bit-width", width -> String
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 :: sym -> SWord sym -> IO (SymInteger sym)
bvToInteger sym
sym SWord sym
ZBV      = sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W.intLit sym
sym Integer
0
bvToInteger sym
sym (DBV SymBV sym w
bv) = sym -> SymBV sym w -> IO (SymInteger sym)
forall sym (w :: Nat).
(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 :: sym -> SWord sym -> IO (SymInteger sym)
sbvToInteger sym
sym SWord sym
ZBV      = sym -> Integer -> IO (SymInteger sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> IO (SymInteger sym)
W.intLit sym
sym Integer
0
sbvToInteger sym
sym (DBV SymBV sym w
bv) = sym -> SymBV sym w -> IO (SymInteger sym)
forall sym (w :: Nat).
(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 :: SWord sym -> Integer
bvWidth (DBV SymBV sym w
x) = Integer -> Integer
forall a. Num a => Integer -> a
fromInteger (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
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 :: sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
_ Integer
w Integer
_
  | Integer
w Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0
  = SWord sym -> IO (SWord sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
forall sym. SWord sym
ZBV
bvLit sym
sym Integer
w Integer
dat
  | Just (Some NatRepr x
rw) <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
w
  , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
rw
  = SymExpr sym ('BaseBVType x) -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymExpr sym ('BaseBVType x) -> SWord sym)
-> IO (SymExpr sym ('BaseBVType x)) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> NatRepr x -> BV x -> IO (SymExpr sym ('BaseBVType x))
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W.bvLit sym
sym NatRepr x
rw (NatRepr x -> Integer -> BV x
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV NatRepr x
rw Integer
dat)
  | Bool
otherwise
  = String -> [String] -> IO (SWord sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"bvLit" [String
"size of bitvector is < 0 or >= maxInt", Integer -> String
forall a. Show a => a -> String
show Integer
w]


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

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

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


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

  | Just (Some NatRepr x
rw) <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
w
  , Just LeqProof 1 x
LeqProof <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
rw
  = SymExpr sym ('BaseBVType x) -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymExpr sym ('BaseBVType x) -> SWord sym)
-> IO (SymExpr sym ('BaseBVType x)) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> NatRepr x -> Pred sym -> IO (SymExpr sym ('BaseBVType x))
forall sym (w :: Nat).
(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
  = String -> [String] -> IO (SWord sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"bvFill" [String
"size of bitvector is < 0 or >= maxInt", Integer -> String
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 :: sym -> SWord sym -> Integer -> IO (Pred sym)
bvAtBE sym
sym (DBV SymBV sym w
bv) Integer
i = do
  let w :: Natural
w   = NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv)
  let idx :: Natural
idx = Natural
w Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i
  sym -> Natural -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(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
_ = String -> [String] -> IO (Pred sym)
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 :: sym -> SWord sym -> Integer -> IO (Pred sym)
bvAtLE sym
sym (DBV SymBV sym w
bv) Integer
i =
  sym -> Natural -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Natural -> SymBV sym w -> IO (Pred sym)
W.testBitBV sym
sym (Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i) SymBV sym w
bv
bvAtLE sym
_ SWord sym
ZBV Integer
_ = String -> [String] -> IO (Pred sym)
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 :: sym -> SWord sym -> Integer -> Pred sym -> IO (SWord sym)
bvSetBE sym
_ SWord sym
ZBV Integer
_ Pred sym
_ = SWord sym -> IO (SWord sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
forall sym. SWord sym
ZBV
bvSetBE sym
sym (DBV SymBV sym w
bv) Integer
i Pred sym
b =
  do let w :: Natural
w = NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv)
     let idx :: Natural
idx = Natural
w Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
i
     SymBV sym w -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymBV sym w -> Natural -> Pred sym -> IO (SymBV sym w)
forall sym (w :: Nat).
(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 :: sym -> SWord sym -> Integer -> Pred sym -> IO (SWord sym)
bvSetLE sym
_ SWord sym
ZBV Integer
_ Pred sym
_ = SWord sym -> IO (SWord sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
forall sym. SWord sym
ZBV
bvSetLE sym
sym (DBV SymBV sym w
bv) Integer
i Pred sym
b =
  SymBV sym w -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymBV sym w -> Natural -> Pred sym -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> Natural -> Pred sym -> IO (SymBV sym w)
W.bvSet sym
sym SymBV sym w
bv (Integer -> Natural
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 :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvJoin sym
_ SWord sym
x SWord sym
ZBV = SWord sym -> IO (SWord sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
x
bvJoin sym
_ SWord sym
ZBV SWord sym
x = SWord sym -> IO (SWord sym)
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 <- NatRepr w -> NatRepr w -> LeqProof 1 (w + w)
forall (m :: Nat) (n :: Nat) (p :: Nat -> Type) (q :: Nat -> Type).
(1 <= m, 1 <= n) =>
p m -> q n -> LeqProof 1 (m + n)
leqAddPos (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv1) (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv2)
  = SymExpr sym ('BaseBVType (w + w)) -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymExpr sym ('BaseBVType (w + w)) -> SWord sym)
-> IO (SymExpr sym ('BaseBVType (w + w))) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> SymBV sym w
-> SymBV sym w
-> IO (SymExpr sym ('BaseBVType (w + w)))
forall sym (u :: Nat) (v :: Nat).
(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 (must be > 0)
  -> SWord sym -> IO (SWord sym)
bvSliceBE :: sym -> Integer -> Integer -> SWord sym -> IO (SWord sym)
bvSliceBE sym
sym Integer
m Integer
n (DBV SymBV sym w
bv)
  | Just (Some NatRepr x
nr) <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
n,
    Just LeqProof 1 x
LeqProof  <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
nr,
    Just (Some NatRepr x
mr) <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
m,
    let wr :: NatRepr w
wr = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv,
    Just LeqProof (x + x) w
LeqProof <- NatRepr (x + x) -> NatRepr w -> Maybe (LeqProof (x + x) w)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (NatRepr x -> NatRepr x -> NatRepr (x + x)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr x
mr NatRepr x
nr)  NatRepr w
wr,
    let idx :: NatRepr (w - (x + x))
idx = NatRepr w -> NatRepr (x + x) -> NatRepr (w - (x + x))
forall (n :: Nat) (m :: Nat).
(n <= m) =>
NatRepr m -> NatRepr n -> NatRepr (m - n)
subNat NatRepr w
wr (NatRepr x -> NatRepr x -> NatRepr (x + x)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr x
mr NatRepr x
nr),
    Just LeqProof ((w - (x + x)) + x) w
LeqProof <- NatRepr ((w - (x + x)) + x)
-> NatRepr w -> Maybe (LeqProof ((w - (x + x)) + x) w)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (NatRepr (w - (x + x)) -> NatRepr x -> NatRepr ((w - (x + x)) + x)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr (w - (x + x))
idx NatRepr x
nr) NatRepr w
wr
  = SymExpr sym ('BaseBVType x) -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymExpr sym ('BaseBVType x) -> SWord sym)
-> IO (SymExpr sym ('BaseBVType x)) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> NatRepr (w - (x + x))
-> NatRepr x
-> SymBV sym w
-> IO (SymExpr sym ('BaseBVType x))
forall sym (idx :: Nat) (n :: Nat) (w :: Nat).
(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
  = String -> [String] -> IO (SWord sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"bvSliceBE"
      [String
"invalid arguments to slice: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" from vector of length " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall a. Show a => a -> String
show (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv)]
bvSliceBE sym
_ Integer
_ Integer
_ SWord sym
ZBV = SWord sym -> IO (SWord sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
forall sym. SWord sym
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 -> Integer -> Integer -> SWord sym -> IO (SWord sym)
bvSliceLE sym
sym Integer
m Integer
n (DBV SymBV sym w
bv)
  | Just (Some NatRepr x
nr) <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
n,
    Just LeqProof 1 x
LeqProof  <- NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
nr,
    Just (Some NatRepr x
mr) <- Integer -> Maybe (Some NatRepr)
forall a. Integral a => a -> Maybe (Some NatRepr)
someNat Integer
m,
    let wr :: NatRepr w
wr = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv,
    Just LeqProof (x + x) w
LeqProof <- NatRepr (x + x) -> NatRepr w -> Maybe (LeqProof (x + x) w)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (NatRepr x -> NatRepr x -> NatRepr (x + x)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat NatRepr x
mr NatRepr x
nr) NatRepr w
wr
  = SymExpr sym ('BaseBVType x) -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymExpr sym ('BaseBVType x) -> SWord sym)
-> IO (SymExpr sym ('BaseBVType x)) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> NatRepr x
-> NatRepr x
-> SymBV sym w
-> IO (SymExpr sym ('BaseBVType x))
forall sym (idx :: Nat) (n :: Nat) (w :: Nat).
(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
  = String -> [String] -> IO (SWord sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"bvSliceLE"
      [String
"invalid arguments to slice: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
m String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" from vector of length " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NatRepr w -> String
forall a. Show a => a -> String
show (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv)]
bvSliceLE sym
_ Integer
_ Integer
_ SWord sym
ZBV = SWord sym -> IO (SWord sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
forall sym. SWord sym
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 -> 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 = SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x
    size :: Integer
    size :: Integer
size = NatRepr w -> Integer
forall (n :: Nat). 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 = sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W.bvLit sym
sym NatRepr w
w (NatRepr w -> Integer -> BV w
forall (w :: Nat). 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 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
size = do
           SymBV sym w
x' <- Integer -> IO (SymBV sym w)
lit (Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
i)
           SymExpr sym BaseBoolType
b' <- sym -> SymBV sym w -> SymBV sym w -> IO (SymExpr sym BaseBoolType)
forall sym (w :: Nat).
(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 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
           sym
-> SymExpr sym BaseBoolType
-> SymBV sym w
-> SymBV sym w
-> IO (SymBV sym w)
forall sym (w :: Nat).
(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 :: sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvIte sym
_ Pred sym
_ SWord sym
ZBV SWord sym
ZBV
  = SWord sym -> IO (SWord sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
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 <- BaseTypeRepr (BaseBVType w)
-> BaseTypeRepr (BaseBVType w)
-> Maybe (BaseBVType w :~: BaseBVType w)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (SymBV sym w -> BaseTypeRepr (BaseBVType w)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W.exprType SymBV sym w
bv1) (SymBV sym w -> BaseTypeRepr (BaseBVType w)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W.exprType SymBV sym w
bv2)
  = SymBV sym w -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> Pred sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(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
SymBV sym w
bv2
bvIte sym
_ Pred sym
_ SWord sym
x SWord sym
y
  = String -> [String] -> IO (SWord sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"bvIte" [String
"bit-vectors don't have same length", Integer -> String
forall a. Show a => a -> String
show (SWord sym -> Integer
forall sym. SWord sym -> Integer
bvWidth SWord sym
x), Integer -> String
forall a. Show a => a -> String
show (SWord sym -> Integer
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 :: sym -> SWord sym -> IO (Vector (Pred sym))
bvUnpackBE sym
_   SWord sym
ZBV = Vector (Pred sym) -> IO (Vector (Pred sym))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Vector (Pred sym)
forall a. Vector a
V.empty
bvUnpackBE sym
sym (DBV SymBV sym w
bv) = do
  let w :: Natural
      w :: Natural
w = NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv)
  Int -> (Int -> IO (Pred sym)) -> IO (Vector (Pred sym))
forall (m :: Type -> Type) a.
Monad m =>
Int -> (Int -> m a) -> m (Vector a)
V.generateM (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
w)
              (\Int
i -> sym -> Natural -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Natural -> SymBV sym w -> IO (Pred sym)
W.testBitBV sym
sym (Natural
w Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Natural
1 Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
- Int -> Natural
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 :: sym -> SWord sym -> IO (Vector (Pred sym))
bvUnpackLE sym
_   SWord sym
ZBV = Vector (Pred sym) -> IO (Vector (Pred sym))
forall (m :: Type -> Type) a. Monad m => a -> m a
return Vector (Pred sym)
forall a. Vector a
V.empty
bvUnpackLE sym
sym (DBV SymBV sym w
bv) = do
  let w :: Natural
      w :: Natural
w = NatRepr w -> Natural
forall (n :: Nat). NatRepr n -> Natural
natValue (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
bv)
  Int -> (Int -> IO (Pred sym)) -> IO (Vector (Pred sym))
forall (m :: Type -> Type) a.
Monad m =>
Int -> (Int -> m a) -> m (Vector a)
V.generateM (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
w)
              (\Int
i -> sym -> Natural -> SymBV sym w -> IO (Pred sym)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> Natural -> SymBV sym w -> IO (Pred sym)
W.testBitBV sym
sym (Int -> Natural
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 :: sym -> Vector (Pred sym) -> IO (SWord sym)
bvPackBE sym
sym Vector (Pred sym)
vec = do
  Vector (SWord sym)
vec' <- (Pred sym -> IO (SWord sym))
-> Vector (Pred sym) -> IO (Vector (SWord sym))
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 <- sym -> Integer -> Integer -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
sym Integer
1 Integer
1
                     SWord sym
v2 <- sym -> Integer -> Integer -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
sym Integer
1 Integer
0
                     sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
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
  (SWord sym -> SWord sym -> IO (SWord sym))
-> SWord sym -> Vector (SWord sym) -> IO (SWord sym)
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 -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvJoin sym
sym SWord sym
x SWord sym
y) SWord sym
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 :: sym -> Vector (Pred sym) -> IO (SWord sym)
bvPackLE sym
sym Vector (Pred sym)
vec = do
  Vector (SWord sym)
vec' <- (Pred sym -> IO (SWord sym))
-> Vector (Pred sym) -> IO (Vector (SWord sym))
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 <- sym -> Integer -> Integer -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
sym Integer
1 Integer
1
                     SWord sym
v2 <- sym -> Integer -> Integer -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
sym Integer
1 Integer
0
                     sym -> Pred sym -> SWord sym -> SWord sym -> IO (SWord sym)
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
  (SWord sym -> SWord sym -> IO (SWord sym))
-> SWord sym -> Vector (SWord sym) -> IO (SWord sym)
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 -> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvJoin sym
sym SWord sym
y SWord sym
x) SWord sym
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 (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> IO (SWord sym)
bvUn forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
f sym
sym (DBV SymBV sym w
bv) = SymBV sym w -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
f sym
sym SymBV sym w
bv
bvUn forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
_ sym
_  SWord sym
ZBV = SWord sym -> IO (SWord sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
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 (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvBin forall (w :: Nat).
(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 <- BaseTypeRepr (BaseBVType w)
-> BaseTypeRepr (BaseBVType w)
-> Maybe (BaseBVType w :~: BaseBVType w)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (SymBV sym w -> BaseTypeRepr (BaseBVType w)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W.exprType SymBV sym w
bv1) (SymBV sym w -> BaseTypeRepr (BaseBVType w)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W.exprType SymBV sym w
bv2)
  = SymBV sym w -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
f sym
sym SymBV sym w
bv1 SymBV sym w
SymBV sym w
bv2
bvBin forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
_ sym
_ SWord sym
ZBV SWord sym
ZBV
  = SWord sym -> IO (SWord sym)
forall (m :: Type -> Type) a. Monad m => a -> m a
return SWord sym
forall sym. SWord sym
ZBV
bvBin forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
_ sym
_ SWord sym
x SWord sym
y
  = String -> [String] -> IO (SWord sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"bvBin" [String
"bit-vectors don't have same length", Integer -> String
forall a. Show a => a -> String
show (SWord sym -> Integer
forall sym. SWord sym -> Integer
bvWidth SWord sym
x), Integer -> String
forall a. Show a => a -> String
show (SWord sym -> Integer
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 :: Bool
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
bvBinPred Bool
_ forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
f sym
sym x :: SWord sym
x@(DBV SymBV sym w
bv1) y :: SWord sym
y@(DBV SymBV sym w
bv2)
  | Just BaseBVType w :~: BaseBVType w
Refl <- BaseTypeRepr (BaseBVType w)
-> BaseTypeRepr (BaseBVType w)
-> Maybe (BaseBVType w :~: BaseBVType w)
forall k (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
testEquality (SymBV sym w -> BaseTypeRepr (BaseBVType w)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W.exprType SymBV sym w
bv1) (SymBV sym w -> BaseTypeRepr (BaseBVType w)
forall (e :: BaseType -> Type) (tp :: BaseType).
IsExpr e =>
e tp -> BaseTypeRepr tp
W.exprType SymBV sym w
bv2)
  = sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
f sym
sym SymBV sym w
bv1 SymBV sym w
SymBV sym w
bv2
  | Bool
otherwise
  = String -> [String] -> IO (Pred sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"bvBinPred" [String
"bit-vectors don't have same length", Integer -> String
forall a. Show a => a -> String
show (SWord sym -> Integer
forall sym. SWord sym -> Integer
bvWidth SWord sym
x), Integer -> String
forall a. Show a => a -> String
show (SWord sym -> Integer
forall sym. SWord sym -> Integer
bvWidth SWord sym
y)]
bvBinPred Bool
b forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
_ sym
sym SWord sym
ZBV SWord sym
ZBV
  = Pred sym -> IO (Pred sym)
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (sym -> Bool -> Pred sym
forall sym. IsExprBuilder sym => sym -> Bool -> Pred sym
W.backendPred sym
sym Bool
b)
bvBinPred Bool
_ forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
_ sym
_ SWord sym
x SWord sym
y
  = String -> [String] -> IO (Pred sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"bvBinPred" [String
"bit-vectors don't have same length", Integer -> String
forall a. Show a => a -> String
show (SWord sym -> Integer
forall sym. SWord sym -> Integer
bvWidth SWord sym
x), Integer -> String
forall a. Show a => a -> String
show (SWord sym -> Integer
forall sym. SWord sym -> Integer
bvWidth SWord sym
y)]

 -- Bitvector logical

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

-- | Bitwise logical and.
bvAnd :: SWordBin
bvAnd :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvAnd = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvAndBits

-- | Bitwise logical or.
bvOr :: SWordBin
bvOr :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvOr = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvOrBits

-- | Bitwise logical exclusive or.
bvXor :: SWordBin
bvXor :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvXor = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvXorBits

 -- Bitvector arithmetic

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

-- | Add two bitvectors.
bvAdd :: SWordBin
bvAdd :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvAdd = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvAdd

-- | Subtract one bitvector from another.
bvSub :: SWordBin
bvSub :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvSub = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvSub

-- | Multiply one bitvector by another.
bvMul :: SWordBin
bvMul :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvMul = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvMul


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

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

bvCountTrailingZeros :: SWordUn
bvCountTrailingZeros :: sym -> SWord sym -> IO (SWord sym)
bvCountTrailingZeros = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> IO (SWord sym)
bvUn forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(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 :: 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 -> String -> [String] -> IO (Pred sym)
forall a. HasCallStack => String -> [String] -> a
panic String
"bvForall" [SolverSymbolError -> String
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 <- NatRepr 1 -> NatRepr x -> Maybe (LeqProof 1 x)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> Maybe (LeqProof m n)
testLeq (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) NatRepr x
w ->
              do BoundVar sym (BaseBVType x)
i <- sym
-> SolverSymbol
-> BaseTypeRepr (BaseBVType x)
-> IO (BoundVar sym (BaseBVType x))
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> SolverSymbol -> BaseTypeRepr tp -> IO (BoundVar sym tp)
W.freshBoundVar sym
sym SolverSymbol
indexSymbol (BaseTypeRepr (BaseBVType x) -> IO (BoundVar sym (BaseBVType x)))
-> BaseTypeRepr (BaseBVType x) -> IO (BoundVar sym (BaseBVType x))
forall a b. (a -> b) -> a -> b
$ NatRepr x -> BaseTypeRepr (BaseBVType x)
forall (w :: Nat).
(1 <= w) =>
NatRepr w -> BaseTypeRepr (BaseBVType w)
W.BaseBVRepr NatRepr x
w
                 Pred sym
body <- SWord sym -> IO (Pred sym)
f (SWord sym -> IO (Pred sym))
-> (SymExpr sym (BaseBVType x) -> SWord sym)
-> SymExpr sym (BaseBVType x)
-> IO (Pred sym)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymExpr sym (BaseBVType x) -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymExpr sym (BaseBVType x) -> IO (Pred sym))
-> SymExpr sym (BaseBVType x) -> IO (Pred sym)
forall a b. (a -> b) -> a -> b
$ sym -> BoundVar sym (BaseBVType x) -> SymExpr sym (BaseBVType x)
forall sym (tp :: BaseType).
IsSymExprBuilder sym =>
sym -> BoundVar sym tp -> SymExpr sym tp
W.varExpr sym
sym BoundVar sym (BaseBVType x)
i
                 sym -> BoundVar sym (BaseBVType x) -> Pred sym -> IO (Pred sym)
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 SWord sym
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 :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvUDiv = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(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 :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvURem = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(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 :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvSDiv = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(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 :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvSRem = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
W.bvSrem

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

 -- Bitvector comparisons

-- | Return true if bitvectors are equal.
bvEq   :: PredBin
bvEq :: sym -> SWord sym -> SWord sym -> IO (Pred sym)
bvEq = Bool
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Nat).
    (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvEq

-- | Signed less-than-or-equal.
bvsle  :: PredBin
bvsle :: sym -> SWord sym -> SWord sym -> IO (Pred sym)
bvsle = Bool
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Nat).
    (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvSle

-- | Signed less-than.
bvslt  :: PredBin
bvslt :: sym -> SWord sym -> SWord sym -> IO (Pred sym)
bvslt = Bool
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Nat).
    (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvSlt

-- | Unsigned less-than-or-equal.
bvule  :: PredBin
bvule :: sym -> SWord sym -> SWord sym -> IO (Pred sym)
bvule = Bool
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Nat).
    (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvUle

-- | Unsigned less-than.
bvult  :: PredBin
bvult :: sym -> SWord sym -> SWord sym -> IO (Pred sym)
bvult = Bool
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Nat).
    (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvUlt

-- | Signed greater-than-or-equal.
bvsge  :: PredBin
bvsge :: sym -> SWord sym -> SWord sym -> IO (Pred sym)
bvsge = Bool
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Nat).
    (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvSge

-- | Signed greater-than.
bvsgt  :: PredBin
bvsgt :: sym -> SWord sym -> SWord sym -> IO (Pred sym)
bvsgt = Bool
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Nat).
    (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvSgt

-- | Unsigned greater-than-or-equal.
bvuge  :: PredBin
bvuge :: sym -> SWord sym -> SWord sym -> IO (Pred sym)
bvuge = Bool
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Nat).
    (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvUge

-- | Unsigned greater-than.
bvugt  :: PredBin
bvugt :: sym -> SWord sym -> SWord sym -> IO (Pred sym)
bvugt = Bool
-> (forall (w :: Nat).
    (1 <= w) =>
    sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym))
-> sym
-> SWord sym
-> SWord sym
-> IO (Pred sym)
forall sym.
IsExprBuilder sym =>
Bool
-> (forall (w :: Nat).
    (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
forall (w :: Nat).
(1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (Pred sym)
W.bvUgt

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

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

    -- y is shorter, zero extend
    NatGT NatRepr y
_diff ->
      do SymBV sym w
y' <- sym -> NatRepr w -> SymBV sym w -> IO (SymBV sym w)
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
W.bvZext sym
sym (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x) SymBV sym w
y
         SymBV sym w -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(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 <- sym -> NatRepr w -> BV w -> IO (SymBV sym w)
forall sym (w :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> NatRepr w -> BV w -> IO (SymBV sym w)
W.bvLit sym
sym (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
y) (NatRepr w -> Integer -> BV w
forall (w :: Nat). NatRepr w -> Integer -> BV w
BV.mkBV (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
y) (NatRepr w -> Integer
forall (n :: Nat). NatRepr n -> Integer
intValue (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x)))
         SymBV sym w
y' <- sym -> NatRepr w -> SymBV sym w -> IO (SymBV sym w)
forall sym (r :: Nat) (w :: Nat).
(IsExprBuilder sym, 1 <= r, (r + 1) <= w) =>
sym -> NatRepr r -> SymBV sym w -> IO (SymBV sym r)
W.bvTrunc sym
sym (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x) (SymBV sym w -> IO (SymBV sym w))
-> IO (SymBV sym w) -> IO (SymBV sym w)
forall (m :: Type -> Type) a b. Monad m => (a -> m b) -> m a -> m b
=<< sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall sym (w :: Nat).
(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
         SymBV sym w -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymBV sym w -> SWord sym) -> IO (SymBV sym w) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(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 :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvShl = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(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 :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvLshr = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(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 :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvAshr = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(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 :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvRol = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(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 :: sym -> SWord sym -> SWord sym -> IO (SWord sym)
bvRor = (forall (w :: Nat).
 (1 <= w) =>
 sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w))
-> sym -> SWord sym -> SWord sym -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
(forall (w :: Nat).
 (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 :: Nat).
(IsExprBuilder sym, 1 <= w) =>
sym -> SymBV sym w -> SymBV sym w -> IO (SymBV sym w)
forall (w :: Nat).
(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 :: 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 NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
nr of
        Maybe (LeqProof 1 x)
Nothing -> SWord sym -> IO (SWord sym)
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 -> sym -> Integer -> Integer -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
sym (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n) Integer
0
            DBV (x :: W.SymBV sym w) ->
              LeqProof (w + 1) (w + x)
-> (((w + 1) <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
forall (m :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (LeqProof w w -> LeqProof 1 x -> LeqProof (w + 1) (w + x)
forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 (NatRepr w -> LeqProof w w
forall (f :: Nat -> Type) (n :: Nat). f n -> LeqProof n n
leqRefl (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x)) LeqProof 1 x
lp :: LeqProof (w+1) (w+n)) ((((w + 1) <= (w + x)) => IO (SWord sym)) -> IO (SWord sym))
-> (((w + 1) <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
forall a b. (a -> b) -> a -> b
$
              LeqProof 1 (w + x)
-> ((1 <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
forall (m :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (LeqProof 1 w -> NatRepr x -> LeqProof 1 (w + x)
forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof NatRepr x
nr :: LeqProof 1 (w+n)) (((1 <= (w + x)) => IO (SWord sym)) -> IO (SWord sym))
-> ((1 <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
forall a b. (a -> b) -> a -> b
$
              SymExpr sym ('BaseBVType (w + x)) -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymExpr sym ('BaseBVType (w + x)) -> SWord sym)
-> IO (SymExpr sym ('BaseBVType (w + x))) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> NatRepr (w + x)
-> SymBV sym w
-> IO (SymExpr sym ('BaseBVType (w + x)))
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
W.bvZext sym
sym (NatRepr w -> NatRepr x -> NatRepr (w + x)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
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 :: 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 NatRepr x -> Maybe (LeqProof 1 x)
forall (n :: Nat). NatRepr n -> Maybe (LeqProof 1 n)
isPosNat NatRepr x
nr of
        Maybe (LeqProof 1 x)
Nothing -> SWord sym -> IO (SWord sym)
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 -> sym -> Integer -> Integer -> IO (SWord sym)
forall sym.
IsExprBuilder sym =>
sym -> Integer -> Integer -> IO (SWord sym)
bvLit sym
sym (Natural -> Integer
forall a. Integral a => a -> Integer
toInteger Natural
n) Integer
0
            DBV (x :: W.SymBV sym w) ->
              LeqProof (w + 1) (w + x)
-> (((w + 1) <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
forall (m :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (LeqProof w w -> LeqProof 1 x -> LeqProof (w + 1) (w + x)
forall (x_l :: Nat) (x_h :: Nat) (y_l :: Nat) (y_h :: Nat).
LeqProof x_l x_h
-> LeqProof y_l y_h -> LeqProof (x_l + y_l) (x_h + y_h)
leqAdd2 (NatRepr w -> LeqProof w w
forall (f :: Nat -> Type) (n :: Nat). f n -> LeqProof n n
leqRefl (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x)) LeqProof 1 x
lp :: LeqProof (w+1) (w+n)) ((((w + 1) <= (w + x)) => IO (SWord sym)) -> IO (SWord sym))
-> (((w + 1) <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
forall a b. (a -> b) -> a -> b
$
              LeqProof 1 (w + x)
-> ((1 <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
forall (m :: Nat) (n :: Nat) a.
LeqProof m n -> ((m <= n) => a) -> a
withLeqProof (LeqProof 1 w -> NatRepr x -> LeqProof 1 (w + x)
forall (f :: Nat -> Type) (m :: Nat) (n :: Nat) (p :: Nat).
LeqProof m n -> f p -> LeqProof m (n + p)
leqAdd LeqProof 1 w
forall (m :: Nat) (n :: Nat). (m <= n) => LeqProof m n
LeqProof NatRepr x
nr :: LeqProof 1 (w+n)) (((1 <= (w + x)) => IO (SWord sym)) -> IO (SWord sym))
-> ((1 <= (w + x)) => IO (SWord sym)) -> IO (SWord sym)
forall a b. (a -> b) -> a -> b
$
              SymExpr sym ('BaseBVType (w + x)) -> SWord sym
forall sym (w :: Nat).
(IsExpr (SymExpr sym), 1 <= w) =>
SymBV sym w -> SWord sym
DBV (SymExpr sym ('BaseBVType (w + x)) -> SWord sym)
-> IO (SymExpr sym ('BaseBVType (w + x))) -> IO (SWord sym)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> sym
-> NatRepr (w + x)
-> SymBV sym w
-> IO (SymExpr sym ('BaseBVType (w + x)))
forall sym (u :: Nat) (r :: Nat).
(IsExprBuilder sym, 1 <= u, (u + 1) <= r) =>
sym -> NatRepr r -> SymBV sym u -> IO (SymBV sym r)
W.bvSext sym
sym (NatRepr w -> NatRepr x -> NatRepr (w + x)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (SymBV sym w -> NatRepr w
forall (e :: BaseType -> Type) (w :: Nat).
IsExpr e =>
e (BaseBVType w) -> NatRepr w
W.bvWidth SymBV sym w
x) NatRepr x
nr) SymBV sym w
x