-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
--
-- SPDX-License-Identifier: GPL-3.0-only

module Language.QBE.Simulator.Symbolic.Expression
  ( BitVector,
    fromByte,
    fromReg,
    toSExpr,
    symbolic,
    bitSize,
    toCond,
  )
where

import Control.DeepSeq (NFData)
import Control.Exception (assert)
import Data.Bits (shiftL, (.&.))
import Data.Word (Word64, Word8)
import GHC.Generics (Generic)
import Language.QBE.Simulator.Default.Expression qualified as D
import Language.QBE.Simulator.Expression qualified as E
import Language.QBE.Simulator.Memory qualified as MEM
import Language.QBE.Types qualified as QBE
import SimpleBV qualified as SMT

-- TODO: Floating point support.
newtype BitVector = BitVector SMT.SExpr
  deriving (Int -> BitVector -> ShowS
[BitVector] -> ShowS
BitVector -> String
(Int -> BitVector -> ShowS)
-> (BitVector -> String)
-> ([BitVector] -> ShowS)
-> Show BitVector
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BitVector -> ShowS
showsPrec :: Int -> BitVector -> ShowS
$cshow :: BitVector -> String
show :: BitVector -> String
$cshowList :: [BitVector] -> ShowS
showList :: [BitVector] -> ShowS
Show, BitVector -> BitVector -> Bool
(BitVector -> BitVector -> Bool)
-> (BitVector -> BitVector -> Bool) -> Eq BitVector
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BitVector -> BitVector -> Bool
== :: BitVector -> BitVector -> Bool
$c/= :: BitVector -> BitVector -> Bool
/= :: BitVector -> BitVector -> Bool
Eq, (forall x. BitVector -> Rep BitVector x)
-> (forall x. Rep BitVector x -> BitVector) -> Generic BitVector
forall x. Rep BitVector x -> BitVector
forall x. BitVector -> Rep BitVector x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. BitVector -> Rep BitVector x
from :: forall x. BitVector -> Rep BitVector x
$cto :: forall x. Rep BitVector x -> BitVector
to :: forall x. Rep BitVector x -> BitVector
Generic)

instance NFData BitVector

fromByte :: Word8 -> BitVector
fromByte :: Word8 -> BitVector
fromByte Word8
byte = SExpr -> BitVector
BitVector (Int -> Integer -> SExpr
SMT.bvLit Int
8 (Integer -> SExpr) -> Integer -> SExpr
forall a b. (a -> b) -> a -> b
$ Word8 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word8
byte)

fromReg :: D.RegVal -> BitVector
fromReg :: RegVal -> BitVector
fromReg (D.VByte Word8
v) = SExpr -> BitVector
BitVector (Int -> Integer -> SExpr
SMT.bvLit Int
8 (Integer -> SExpr) -> Integer -> SExpr
forall a b. (a -> b) -> a -> b
$ Word8 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word8
v)
fromReg (D.VHalf Word16
v) = SExpr -> BitVector
BitVector (Int -> Integer -> SExpr
SMT.bvLit Int
16 (Integer -> SExpr) -> Integer -> SExpr
forall a b. (a -> b) -> a -> b
$ Word16 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word16
v)
fromReg (D.VWord Word32
v) = SExpr -> BitVector
BitVector (Int -> Integer -> SExpr
SMT.bvLit Int
32 (Integer -> SExpr) -> Integer -> SExpr
forall a b. (a -> b) -> a -> b
$ Word32 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word32
v)
fromReg (D.VLong Word64
v) = SExpr -> BitVector
BitVector (Int -> Integer -> SExpr
SMT.bvLit Int
64 (Integer -> SExpr) -> Integer -> SExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
v)
fromReg (D.VSingle Float
_) = String -> BitVector
forall a. HasCallStack => String -> a
error String
"symbolic floats not supported"
fromReg (D.VDouble Double
_) = String -> BitVector
forall a. HasCallStack => String -> a
error String
"symbolic doubles not supported"

toSExpr :: BitVector -> SMT.SExpr
toSExpr :: BitVector -> SExpr
toSExpr (BitVector SExpr
s) = SExpr
s

symbolic :: String -> QBE.ExtType -> BitVector
symbolic :: String -> ExtType -> BitVector
symbolic String
name ExtType
ty = SExpr -> BitVector
BitVector (String -> Int -> SExpr
SMT.const String
name (Int -> SExpr) -> Int -> SExpr
forall a b. (a -> b) -> a -> b
$ ExtType -> Int
QBE.extTypeBitSize ExtType
ty)

bitSize :: BitVector -> Int
bitSize :: BitVector -> Int
bitSize = SExpr -> Int
SMT.width (SExpr -> Int) -> (BitVector -> SExpr) -> BitVector -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector -> SExpr
toSExpr

-- In the QBE a condition (see `jnz`) is true if the Word value is not zero.
toCond :: Bool -> BitVector -> SMT.SExpr
toCond :: Bool -> BitVector -> SExpr
toCond Bool
isTrue BitVector
bv =
  -- Equality is only defined for Words.
  Bool -> SExpr -> SExpr
forall a. HasCallStack => Bool -> a -> a
assert (BitVector -> Int
bitSize BitVector
bv Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== BaseType -> Int
QBE.baseTypeBitSize BaseType
QBE.Word) (SExpr -> SExpr) -> SExpr -> SExpr
forall a b. (a -> b) -> a -> b
$
    let zeroSExpr :: SExpr
zeroSExpr = BitVector -> SExpr
toSExpr (RegVal -> BitVector
fromReg (RegVal -> BitVector) -> RegVal -> BitVector
forall a b. (a -> b) -> a -> b
$ ExtType -> Word64 -> RegVal
forall v. ValueRepr v => ExtType -> Word64 -> v
E.fromLit (BaseType -> ExtType
QBE.Base BaseType
QBE.Word) Word64
0)
     in SExpr -> SExpr -> SExpr
toCond' (BitVector -> SExpr
toSExpr BitVector
bv) SExpr
zeroSExpr
  where
    toCond' :: SExpr -> SExpr -> SExpr
toCond' SExpr
lhs SExpr
rhs
      | Bool
isTrue = SExpr -> SExpr
SMT.not (SExpr -> SExpr -> SExpr
SMT.eq SExpr
lhs SExpr
rhs) -- /= 0
      | Bool
otherwise = SExpr -> SExpr -> SExpr
SMT.eq SExpr
lhs SExpr
rhs -- == 0

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

instance MEM.Storable BitVector BitVector where
  toBytes :: BitVector -> [BitVector]
toBytes (BitVector SExpr
s) =
    Bool -> [BitVector] -> [BitVector]
forall a. HasCallStack => Bool -> a -> a
assert (Integer
size Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`mod` Integer
8 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0) ([BitVector] -> [BitVector]) -> [BitVector] -> [BitVector]
forall a b. (a -> b) -> a -> b
$
      (Int -> BitVector) -> [Int] -> [BitVector]
forall a b. (a -> b) -> [a] -> [b]
map (SExpr -> BitVector
BitVector (SExpr -> BitVector) -> (Int -> SExpr) -> Int -> BitVector
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SExpr -> Int -> SExpr
nthByte SExpr
s) [Int
1 .. Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
size Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
8]
    where
      size :: Integer
      size :: Integer
size = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ SExpr -> Int
SMT.width SExpr
s

      nthByte :: SMT.SExpr -> Int -> SMT.SExpr
      nthByte :: SExpr -> Int -> SExpr
nthByte SExpr
expr Int
n = SExpr -> Int -> Int -> SExpr
SMT.extract SExpr
expr ((Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
8) Int
8

  fromBytes :: LoadType -> [BitVector] -> Maybe BitVector
fromBytes LoadType
_ [] = Maybe BitVector
forall a. Maybe a
Nothing
  fromBytes LoadType
ty bytes :: [BitVector]
bytes@(BitVector SExpr
s : [BitVector]
xs) =
    if [BitVector] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BitVector]
bytes Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (LoadType -> Word64
QBE.loadByteSize LoadType
ty)
      then Maybe BitVector
forall a. Maybe a
Nothing
      else case (LoadType
ty, [BitVector]
bytes) of
        (QBE.LSubWord SubWordType
QBE.UnsignedByte, [BitVector
_]) ->
          BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just (SExpr -> BitVector
BitVector (Integer -> SExpr -> SExpr
SMT.zeroExtend Integer
24 SExpr
concated))
        (QBE.LSubWord SubWordType
QBE.SignedByte, [BitVector
_]) ->
          BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just (SExpr -> BitVector
BitVector (Integer -> SExpr -> SExpr
SMT.signExtend Integer
24 SExpr
concated))
        (QBE.LSubWord SubWordType
QBE.SignedHalf, [BitVector
_, BitVector
_]) ->
          BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just (SExpr -> BitVector
BitVector (Integer -> SExpr -> SExpr
SMT.signExtend Integer
16 SExpr
concated))
        (QBE.LSubWord SubWordType
QBE.UnsignedHalf, [BitVector
_, BitVector
_]) ->
          BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just (SExpr -> BitVector
BitVector (Integer -> SExpr -> SExpr
SMT.zeroExtend Integer
16 SExpr
concated))
        (QBE.LBase BaseType
QBE.Word, [BitVector
_, BitVector
_, BitVector
_, BitVector
_]) ->
          BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just (SExpr -> BitVector
BitVector SExpr
concated)
        (QBE.LBase BaseType
QBE.Long, [BitVector
_, BitVector
_, BitVector
_, BitVector
_, BitVector
_, BitVector
_, BitVector
_, BitVector
_]) ->
          BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just (SExpr -> BitVector
BitVector SExpr
concated)
        (QBE.LBase BaseType
QBE.Single, [BitVector
_, BitVector
_, BitVector
_, BitVector
_]) ->
          String -> Maybe BitVector
forall a. HasCallStack => String -> a
error String
"float loading not implemented"
        (QBE.LBase BaseType
QBE.Double, [BitVector
_, BitVector
_, BitVector
_, BitVector
_, BitVector
_, BitVector
_, BitVector
_, BitVector
_]) ->
          String -> Maybe BitVector
forall a. HasCallStack => String -> a
error String
"double loading not implemented"
        (LoadType, [BitVector])
_ -> Maybe BitVector
forall a. Maybe a
Nothing
    where
      concated :: SMT.SExpr
      concated :: SExpr
concated = (SExpr -> BitVector -> SExpr) -> SExpr -> [BitVector] -> SExpr
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl SExpr -> BitVector -> SExpr
concatBV SExpr
s [BitVector]
xs

      concatBV :: SMT.SExpr -> BitVector -> SMT.SExpr
      concatBV :: SExpr -> BitVector -> SExpr
concatBV SExpr
acc (BitVector SExpr
byte) =
        Bool -> SExpr -> SExpr
forall a. HasCallStack => Bool -> a -> a
assert (SExpr -> Int
SMT.width SExpr
byte Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
8) (SExpr -> SExpr) -> SExpr -> SExpr
forall a b. (a -> b) -> a -> b
$
          SExpr -> SExpr -> SExpr
SMT.concat SExpr
byte SExpr
acc

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

binaryOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector
binaryOp :: (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
op (BitVector SExpr
lhs) (BitVector SExpr
rhs)
  | SExpr -> Int
SMT.width SExpr
lhs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== SExpr -> Int
SMT.width SExpr
rhs = BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just (BitVector -> Maybe BitVector) -> BitVector -> Maybe BitVector
forall a b. (a -> b) -> a -> b
$ SExpr -> BitVector
BitVector (SExpr
lhs SExpr -> SExpr -> SExpr
`op` SExpr
rhs)
  | Bool
otherwise = Maybe BitVector
forall a. Maybe a
Nothing

-- TODO: Move this into the expression abstraction.
toShiftAmount :: Word64 -> BitVector -> Maybe BitVector
toShiftAmount :: Word64 -> BitVector -> Maybe BitVector
toShiftAmount Word64
size BitVector
amount = BitVector
amount BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
`E.urem` ExtType -> Word64 -> BitVector
forall v. ValueRepr v => ExtType -> Word64 -> v
E.fromLit (BaseType -> ExtType
QBE.Base BaseType
QBE.Word) Word64
size

shiftOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector
shiftOp :: (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
shiftOp SExpr -> SExpr -> SExpr
op BitVector
value amount :: BitVector
amount@(BitVector SExpr
SMT.Word) =
  case BitVector -> Int
bitSize BitVector
value of
    Int
32 -> Word64 -> BitVector -> Maybe BitVector
toShiftAmount Word64
32 BitVector
amount Maybe BitVector
-> (BitVector -> Maybe BitVector) -> Maybe BitVector
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
op BitVector
value
    Int
64 -> do
      BitVector
shiftAmount <- Word64 -> BitVector -> Maybe BitVector
toShiftAmount Word64
64 BitVector
amount
      ExtType -> Bool -> BitVector -> Maybe BitVector
forall v. ValueRepr v => ExtType -> Bool -> v -> Maybe v
E.extend (BaseType -> ExtType
QBE.Base BaseType
QBE.Long) Bool
False BitVector
shiftAmount Maybe BitVector
-> (BitVector -> Maybe BitVector) -> Maybe BitVector
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
op BitVector
value
    Int
_ -> Maybe BitVector
forall a. Maybe a
Nothing
shiftOp SExpr -> SExpr -> SExpr
_ BitVector
_ BitVector
_ = Maybe BitVector
forall a. Maybe a
Nothing -- Shift amount must always be a Word.

binaryBoolOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector
binaryBoolOp :: (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryBoolOp SExpr -> SExpr -> SExpr
op BitVector
lhs BitVector
rhs = do
  BitVector
bv <- (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
op BitVector
lhs BitVector
rhs
  BitVector -> Maybe BitVector
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (BitVector -> Maybe BitVector) -> BitVector -> Maybe BitVector
forall a b. (a -> b) -> a -> b
$ SExpr -> BitVector
BitVector (SExpr -> SExpr -> SExpr -> SExpr
SMT.ite (BitVector -> SExpr
toSExpr BitVector
bv) SExpr
trueValue SExpr
falseValue)
  where
    -- TODO: Declare these as constants.
    trueValue :: SMT.SExpr
    trueValue :: SExpr
trueValue = BitVector -> SExpr
toSExpr (BitVector -> SExpr) -> BitVector -> SExpr
forall a b. (a -> b) -> a -> b
$ ExtType -> Word64 -> BitVector
forall v. ValueRepr v => ExtType -> Word64 -> v
E.fromLit (BaseType -> ExtType
QBE.Base BaseType
QBE.Long) Word64
1

    falseValue :: SMT.SExpr
    falseValue :: SExpr
falseValue = BitVector -> SExpr
toSExpr (BitVector -> SExpr) -> BitVector -> SExpr
forall a b. (a -> b) -> a -> b
$ ExtType -> Word64 -> BitVector
forall v. ValueRepr v => ExtType -> Word64 -> v
E.fromLit (BaseType -> ExtType
QBE.Base BaseType
QBE.Long) Word64
0

instance E.ValueRepr BitVector where
  fromLit :: ExtType -> Word64 -> BitVector
fromLit ExtType
ty Word64
n =
    let size :: Int
size = ExtType -> Int
QBE.extTypeBitSize ExtType
ty
        mask :: Word64
mask = (Word64
1 Word64 -> Int -> Word64
forall a. Bits a => a -> Int -> a
`shiftL` Int
size) Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1
     in SExpr -> BitVector
BitVector (SExpr -> BitVector) -> SExpr -> BitVector
forall a b. (a -> b) -> a -> b
$ Int -> Integer -> SExpr
SMT.bvLit (Int -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
size) (Integer -> SExpr) -> Integer -> SExpr
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64
n Word64 -> Word64 -> Word64
forall a. Bits a => a -> a -> a
.&. Word64
mask)

  fromFloat :: Float -> BitVector
fromFloat = String -> Float -> BitVector
forall a. HasCallStack => String -> a
error String
"symbolic floats currently unsupported"
  fromDouble :: Double -> BitVector
fromDouble = String -> Double -> BitVector
forall a. HasCallStack => String -> a
error String
"symbolic doubles currently unsupported"

  -- XXX: This only works for constants values, but this is fine since we implement
  -- concolic execution and can obtain the address from the concrete value part.
  toWord64 :: BitVector -> Word64
toWord64 (BitVector SExpr
value) =
    case SExpr -> Value
SMT.sexprToVal SExpr
value of
      SMT.Bits Int
_ Integer
n -> Integer -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
      Value
_ -> String -> Word64
forall a. HasCallStack => String -> a
error String
"unrechable"

  getType :: BitVector -> ExtType
getType BitVector
v = case BitVector -> Int
bitSize BitVector
v of
    Int
08 -> ExtType
QBE.Byte
    Int
16 -> ExtType
QBE.HalfWord
    Int
32 -> BaseType -> ExtType
QBE.Base BaseType
QBE.Word
    Int
64 -> BaseType -> ExtType
QBE.Base BaseType
QBE.Long
    Int
_ -> String -> ExtType
forall a. HasCallStack => String -> a
error String
"unreachable"

  floatToInt :: ExtType -> Bool -> BitVector -> Maybe BitVector
floatToInt = String -> ExtType -> Bool -> BitVector -> Maybe BitVector
forall a. HasCallStack => String -> a
error String
"symbolic float conversion not supported"
  intToFloat :: ExtType -> Bool -> BitVector -> Maybe BitVector
intToFloat = String -> ExtType -> Bool -> BitVector -> Maybe BitVector
forall a. HasCallStack => String -> a
error String
"symbolic float conversion not supported"
  extendFloat :: BitVector -> Maybe BitVector
extendFloat = String -> BitVector -> Maybe BitVector
forall a. HasCallStack => String -> a
error String
"symbolic float extension not supported"
  truncFloat :: BitVector -> Maybe BitVector
truncFloat = String -> BitVector -> Maybe BitVector
forall a. HasCallStack => String -> a
error String
"symbolic float trunction not supported"

  extend :: ExtType -> Bool -> BitVector -> Maybe BitVector
extend ExtType
extTy Bool
isSigned val :: BitVector
val@(BitVector SExpr
s)
    | ExtType -> Int
QBE.extTypeBitSize ExtType
extTy Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= BitVector -> Int
bitSize BitVector
val = Maybe BitVector
forall a. Maybe a
Nothing
    | Bool
otherwise = BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just (BitVector -> Maybe BitVector) -> BitVector -> Maybe BitVector
forall a b. (a -> b) -> a -> b
$ SExpr -> BitVector
BitVector (Integer -> SExpr -> SExpr
extFunc Integer
targetSize SExpr
s)
    where
      targetSize :: Integer
      targetSize :: Integer
targetSize = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ ExtType -> Int
QBE.extTypeBitSize ExtType
extTy Int -> Int -> Int
forall a. Num a => a -> a -> a
- BitVector -> Int
bitSize BitVector
val

      extFunc :: Integer -> SMT.SExpr -> SMT.SExpr
      extFunc :: Integer -> SExpr -> SExpr
extFunc = if Bool
isSigned then Integer -> SExpr -> SExpr
SMT.signExtend else Integer -> SExpr -> SExpr
SMT.zeroExtend

  extract :: ExtType -> BitVector -> Maybe BitVector
extract ExtType
extTy val :: BitVector
val@(BitVector SExpr
s)
    | ExtType -> Int
QBE.extTypeBitSize ExtType
extTy Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> BitVector -> Int
bitSize BitVector
val = Maybe BitVector
forall a. Maybe a
Nothing
    | Bool
otherwise = BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just (BitVector -> Maybe BitVector) -> BitVector -> Maybe BitVector
forall a b. (a -> b) -> a -> b
$ SExpr -> BitVector
BitVector (SExpr -> Int -> Int -> SExpr
SMT.extract SExpr
s Int
0 (Int -> SExpr) -> Int -> SExpr
forall a b. (a -> b) -> a -> b
$ ExtType -> Int
QBE.extTypeBitSize ExtType
extTy)

  add :: BitVector -> BitVector -> Maybe BitVector
add = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
SMT.bvAdd
  sub :: BitVector -> BitVector -> Maybe BitVector
sub = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
SMT.bvSub
  mul :: BitVector -> BitVector -> Maybe BitVector
mul = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
SMT.bvMul
  div :: BitVector -> BitVector -> Maybe BitVector
div = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
SMT.bvSDiv
  or :: BitVector -> BitVector -> Maybe BitVector
or = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
SMT.bvOr
  xor :: BitVector -> BitVector -> Maybe BitVector
xor = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
SMT.bvXOr
  and :: BitVector -> BitVector -> Maybe BitVector
and = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
SMT.bvAnd
  urem :: BitVector -> BitVector -> Maybe BitVector
urem = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
SMT.bvURem
  srem :: BitVector -> BitVector -> Maybe BitVector
srem = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
SMT.bvSRem
  udiv :: BitVector -> BitVector -> Maybe BitVector
udiv = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryOp SExpr -> SExpr -> SExpr
SMT.bvUDiv

  neg :: BitVector -> Maybe BitVector
neg (BitVector SExpr
v) = BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just (BitVector -> Maybe BitVector) -> BitVector -> Maybe BitVector
forall a b. (a -> b) -> a -> b
$ SExpr -> BitVector
BitVector (SExpr -> SExpr
SMT.bvNeg SExpr
v)

  sar :: BitVector -> BitVector -> Maybe BitVector
sar = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
shiftOp SExpr -> SExpr -> SExpr
SMT.bvAShr
  shr :: BitVector -> BitVector -> Maybe BitVector
shr = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
shiftOp SExpr -> SExpr -> SExpr
SMT.bvLShr
  shl :: BitVector -> BitVector -> Maybe BitVector
shl = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
shiftOp SExpr -> SExpr -> SExpr
SMT.bvShl

  eq :: BitVector -> BitVector -> Maybe BitVector
eq = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryBoolOp SExpr -> SExpr -> SExpr
SMT.eq
  ne :: BitVector -> BitVector -> Maybe BitVector
ne = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryBoolOp (\SExpr
lhs SExpr
rhs -> SExpr -> SExpr
SMT.not (SExpr -> SExpr) -> SExpr -> SExpr
forall a b. (a -> b) -> a -> b
$ SExpr -> SExpr -> SExpr
SMT.eq SExpr
lhs SExpr
rhs)
  sle :: BitVector -> BitVector -> Maybe BitVector
sle = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryBoolOp SExpr -> SExpr -> SExpr
SMT.bvSLeq
  slt :: BitVector -> BitVector -> Maybe BitVector
slt = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryBoolOp SExpr -> SExpr -> SExpr
SMT.bvSLt
  sge :: BitVector -> BitVector -> Maybe BitVector
sge = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryBoolOp SExpr -> SExpr -> SExpr
SMT.bvSGeq
  sgt :: BitVector -> BitVector -> Maybe BitVector
sgt = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryBoolOp SExpr -> SExpr -> SExpr
SMT.bvSGt
  ule :: BitVector -> BitVector -> Maybe BitVector
ule = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryBoolOp SExpr -> SExpr -> SExpr
SMT.bvULeq
  ult :: BitVector -> BitVector -> Maybe BitVector
ult = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryBoolOp SExpr -> SExpr -> SExpr
SMT.bvULt
  uge :: BitVector -> BitVector -> Maybe BitVector
uge = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryBoolOp SExpr -> SExpr -> SExpr
SMT.bvUGeq
  ugt :: BitVector -> BitVector -> Maybe BitVector
ugt = (SExpr -> SExpr -> SExpr)
-> BitVector -> BitVector -> Maybe BitVector
binaryBoolOp SExpr -> SExpr -> SExpr
SMT.bvUGt

  ord :: BitVector -> BitVector -> Maybe BitVector
ord = String -> BitVector -> BitVector -> Maybe BitVector
forall a. HasCallStack => String -> a
error String
"symbolic ordered comparison not supported"
  unord :: BitVector -> BitVector -> Maybe BitVector
unord = String -> BitVector -> BitVector -> Maybe BitVector
forall a. HasCallStack => String -> a
error String
"symbolic unordered comparison not supported"