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

module Language.QBE.Simulator.Concolic.Expression
  ( Concolic (..),
    hasSymbolic,
  )
where

import Control.DeepSeq (NFData, NFData1)
import Control.Exception (assert)
import Data.Functor ((<&>))
import Data.Maybe (fromMaybe)
import Data.Word (Word8)
import GHC.Generics (Generic, Generic1)
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.Simulator.Symbolic.Expression qualified as SE

data Concolic v
  = Concolic
  { forall v. Concolic v -> v
concrete :: v,
    forall v. Concolic v -> Maybe BitVector
symbolic :: Maybe SE.BitVector
  }
  deriving (Int -> Concolic v -> ShowS
[Concolic v] -> ShowS
Concolic v -> String
(Int -> Concolic v -> ShowS)
-> (Concolic v -> String)
-> ([Concolic v] -> ShowS)
-> Show (Concolic v)
forall v. Show v => Int -> Concolic v -> ShowS
forall v. Show v => [Concolic v] -> ShowS
forall v. Show v => Concolic v -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall v. Show v => Int -> Concolic v -> ShowS
showsPrec :: Int -> Concolic v -> ShowS
$cshow :: forall v. Show v => Concolic v -> String
show :: Concolic v -> String
$cshowList :: forall v. Show v => [Concolic v] -> ShowS
showList :: [Concolic v] -> ShowS
Show, (forall x. Concolic v -> Rep (Concolic v) x)
-> (forall x. Rep (Concolic v) x -> Concolic v)
-> Generic (Concolic v)
forall x. Rep (Concolic v) x -> Concolic v
forall x. Concolic v -> Rep (Concolic v) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall v x. Rep (Concolic v) x -> Concolic v
forall v x. Concolic v -> Rep (Concolic v) x
$cfrom :: forall v x. Concolic v -> Rep (Concolic v) x
from :: forall x. Concolic v -> Rep (Concolic v) x
$cto :: forall v x. Rep (Concolic v) x -> Concolic v
to :: forall x. Rep (Concolic v) x -> Concolic v
Generic, (forall a. Concolic a -> Rep1 Concolic a)
-> (forall a. Rep1 Concolic a -> Concolic a) -> Generic1 Concolic
forall a. Rep1 Concolic a -> Concolic a
forall a. Concolic a -> Rep1 Concolic a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall a. Concolic a -> Rep1 Concolic a
from1 :: forall a. Concolic a -> Rep1 Concolic a
$cto1 :: forall a. Rep1 Concolic a -> Concolic a
to1 :: forall a. Rep1 Concolic a -> Concolic a
Generic1)

instance (NFData a) => NFData (Concolic a)

instance NFData1 Concolic

hasSymbolic :: Concolic v -> Bool
hasSymbolic :: forall v. Concolic v -> Bool
hasSymbolic Concolic {symbolic :: forall v. Concolic v -> Maybe BitVector
symbolic = Just BitVector
_} = Bool
True
hasSymbolic Concolic v
_ = Bool
False

getSymbolicDef :: (v -> SE.BitVector) -> Concolic v -> SE.BitVector
getSymbolicDef :: forall v. (v -> BitVector) -> Concolic v -> BitVector
getSymbolicDef v -> BitVector
conc Concolic {concrete :: forall v. Concolic v -> v
concrete = v
c, symbolic :: forall v. Concolic v -> Maybe BitVector
symbolic = Maybe BitVector
s} =
  BitVector -> Maybe BitVector -> BitVector
forall a. a -> Maybe a -> a
fromMaybe (v -> BitVector
conc v
c) Maybe BitVector
s

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

instance MEM.Storable (Concolic D.RegVal) (Concolic Word8) where
  toBytes :: Concolic RegVal -> [Concolic Word8]
toBytes Concolic {concrete :: forall v. Concolic v -> v
concrete = RegVal
c, symbolic :: forall v. Concolic v -> Maybe BitVector
symbolic = Maybe BitVector
s} =
    let cbytes :: [Word8]
cbytes = RegVal -> [Word8]
forall valTy byteTy. Storable valTy byteTy => valTy -> [byteTy]
MEM.toBytes RegVal
c
        nbytes :: Int
nbytes = [Word8] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Word8]
cbytes
        sbytes :: [Maybe BitVector]
sbytes = [Maybe BitVector]
-> (BitVector -> [Maybe BitVector])
-> Maybe BitVector
-> [Maybe BitVector]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Int -> Maybe BitVector -> [Maybe BitVector]
forall a. Int -> a -> [a]
replicate Int
nbytes Maybe BitVector
forall a. Maybe a
Nothing) ((BitVector -> Maybe BitVector) -> [BitVector] -> [Maybe BitVector]
forall a b. (a -> b) -> [a] -> [b]
map BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just ([BitVector] -> [Maybe BitVector])
-> (BitVector -> [BitVector]) -> BitVector -> [Maybe BitVector]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector -> [BitVector]
forall valTy byteTy. Storable valTy byteTy => valTy -> [byteTy]
MEM.toBytes) Maybe BitVector
s
     in Bool -> [Concolic Word8] -> [Concolic Word8]
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (Int
nbytes Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Maybe BitVector] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Maybe BitVector]
sbytes) ([Concolic Word8] -> [Concolic Word8])
-> [Concolic Word8] -> [Concolic Word8]
forall a b. (a -> b) -> a -> b
$
          (Word8 -> Maybe BitVector -> Concolic Word8)
-> [Word8] -> [Maybe BitVector] -> [Concolic Word8]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Word8 -> Maybe BitVector -> Concolic Word8
forall v. v -> Maybe BitVector -> Concolic v
Concolic [Word8]
cbytes [Maybe BitVector]
sbytes

  fromBytes :: LoadType -> [Concolic Word8] -> Maybe (Concolic RegVal)
fromBytes LoadType
ty [Concolic Word8]
bytes =
    do
      let conBytes :: [Word8]
conBytes = (Concolic Word8 -> Word8) -> [Concolic Word8] -> [Word8]
forall a b. (a -> b) -> [a] -> [b]
map Concolic Word8 -> Word8
forall v. Concolic v -> v
concrete [Concolic Word8]
bytes
      RegVal
con <- LoadType -> [Word8] -> Maybe RegVal
forall valTy byteTy.
Storable valTy byteTy =>
LoadType -> [byteTy] -> Maybe valTy
MEM.fromBytes LoadType
ty [Word8]
conBytes

      let mkConcolic :: Maybe BitVector -> Concolic RegVal
mkConcolic = RegVal -> Maybe BitVector -> Concolic RegVal
forall v. v -> Maybe BitVector -> Concolic v
Concolic RegVal
con
      if (Concolic Word8 -> Bool) -> [Concolic Word8] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Concolic Word8 -> Bool
forall v. Concolic v -> Bool
hasSymbolic [Concolic Word8]
bytes
        then do
          let symBVs :: [BitVector]
symBVs = (Concolic Word8 -> BitVector) -> [Concolic Word8] -> [BitVector]
forall a b. (a -> b) -> [a] -> [b]
map ((Word8 -> BitVector) -> Concolic Word8 -> BitVector
forall v. (v -> BitVector) -> Concolic v -> BitVector
getSymbolicDef Word8 -> BitVector
SE.fromByte) [Concolic Word8]
bytes
          LoadType -> [BitVector] -> Maybe BitVector
forall valTy byteTy.
Storable valTy byteTy =>
LoadType -> [byteTy] -> Maybe valTy
MEM.fromBytes LoadType
ty [BitVector]
symBVs Maybe BitVector
-> (BitVector -> Concolic RegVal) -> Maybe (Concolic RegVal)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Maybe BitVector -> Concolic RegVal
mkConcolic (Maybe BitVector -> Concolic RegVal)
-> (BitVector -> Maybe BitVector) -> BitVector -> Concolic RegVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just
        else Concolic RegVal -> Maybe (Concolic RegVal)
forall a. a -> Maybe a
Just (Concolic RegVal -> Maybe (Concolic RegVal))
-> Concolic RegVal -> Maybe (Concolic RegVal)
forall a b. (a -> b) -> a -> b
$ Maybe BitVector -> Concolic RegVal
mkConcolic Maybe BitVector
forall a. Maybe a
Nothing

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

unaryOp ::
  (D.RegVal -> Maybe D.RegVal) ->
  (SE.BitVector -> Maybe SE.BitVector) ->
  Concolic D.RegVal ->
  Maybe (Concolic D.RegVal)
unaryOp :: (RegVal -> Maybe RegVal)
-> (BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Maybe (Concolic RegVal)
unaryOp RegVal -> Maybe RegVal
fnCon BitVector -> Maybe BitVector
fnSym Concolic {concrete :: forall v. Concolic v -> v
concrete = RegVal
c, symbolic :: forall v. Concolic v -> Maybe BitVector
symbolic = Maybe BitVector
s} = do
  RegVal
c' <- RegVal -> Maybe RegVal
fnCon RegVal
c
  let con :: Maybe BitVector -> Concolic RegVal
con = RegVal -> Maybe BitVector -> Concolic RegVal
forall v. v -> Maybe BitVector -> Concolic v
Concolic RegVal
c'
  case Maybe BitVector
s of
    Just BitVector
s' -> BitVector -> Maybe BitVector
fnSym BitVector
s' Maybe BitVector
-> (BitVector -> Concolic RegVal) -> Maybe (Concolic RegVal)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Maybe BitVector -> Concolic RegVal
con (Maybe BitVector -> Concolic RegVal)
-> (BitVector -> Maybe BitVector) -> BitVector -> Concolic RegVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just
    Maybe BitVector
Nothing -> Concolic RegVal -> Maybe (Concolic RegVal)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Concolic RegVal -> Maybe (Concolic RegVal))
-> Concolic RegVal -> Maybe (Concolic RegVal)
forall a b. (a -> b) -> a -> b
$ Maybe BitVector -> Concolic RegVal
con Maybe BitVector
forall a. Maybe a
Nothing

binaryOp ::
  (D.RegVal -> D.RegVal -> Maybe D.RegVal) ->
  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->
  Concolic D.RegVal ->
  Concolic D.RegVal ->
  Maybe (Concolic D.RegVal)
binaryOp :: (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
fnCon BitVector -> BitVector -> Maybe BitVector
fnSym Concolic RegVal
lhs Concolic RegVal
rhs =
  do
    RegVal
c <- Concolic RegVal -> RegVal
forall v. Concolic v -> v
concrete Concolic RegVal
lhs RegVal -> RegVal -> Maybe RegVal
`fnCon` Concolic RegVal -> RegVal
forall v. Concolic v -> v
concrete Concolic RegVal
rhs
    if Concolic RegVal -> Bool
forall v. Concolic v -> Bool
hasSymbolic Concolic RegVal
lhs Bool -> Bool -> Bool
|| Concolic RegVal -> Bool
forall v. Concolic v -> Bool
hasSymbolic Concolic RegVal
rhs
      then
        let lhsS :: BitVector
lhsS = (RegVal -> BitVector) -> Concolic RegVal -> BitVector
forall v. (v -> BitVector) -> Concolic v -> BitVector
getSymbolicDef RegVal -> BitVector
SE.fromReg Concolic RegVal
lhs
            rhsS :: BitVector
rhsS = (RegVal -> BitVector) -> Concolic RegVal -> BitVector
forall v. (v -> BitVector) -> Concolic v -> BitVector
getSymbolicDef RegVal -> BitVector
SE.fromReg Concolic RegVal
rhs
         in (BitVector
lhsS BitVector -> BitVector -> Maybe BitVector
`fnSym` BitVector
rhsS) Maybe BitVector
-> (BitVector -> Concolic RegVal) -> Maybe (Concolic RegVal)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> RegVal -> Maybe BitVector -> Concolic RegVal
forall v. v -> Maybe BitVector -> Concolic v
Concolic RegVal
c (Maybe BitVector -> Concolic RegVal)
-> (BitVector -> Maybe BitVector) -> BitVector -> Concolic RegVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BitVector -> Maybe BitVector
forall a. a -> Maybe a
Just
      else Concolic RegVal -> Maybe (Concolic RegVal)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Concolic RegVal -> Maybe (Concolic RegVal))
-> Concolic RegVal -> Maybe (Concolic RegVal)
forall a b. (a -> b) -> a -> b
$ RegVal -> Maybe BitVector -> Concolic RegVal
forall v. v -> Maybe BitVector -> Concolic v
Concolic RegVal
c Maybe BitVector
forall a. Maybe a
Nothing

instance E.ValueRepr (Concolic D.RegVal) where
  fromLit :: ExtType -> Word64 -> Concolic RegVal
fromLit ExtType
ty Word64
v = RegVal -> Maybe BitVector -> Concolic RegVal
forall v. v -> Maybe BitVector -> Concolic v
Concolic (ExtType -> Word64 -> RegVal
forall v. ValueRepr v => ExtType -> Word64 -> v
E.fromLit ExtType
ty Word64
v) Maybe BitVector
forall a. Maybe a
Nothing
  fromFloat :: Float -> Concolic RegVal
fromFloat Float
fl = RegVal -> Maybe BitVector -> Concolic RegVal
forall v. v -> Maybe BitVector -> Concolic v
Concolic (Float -> RegVal
forall v. ValueRepr v => Float -> v
E.fromFloat Float
fl) Maybe BitVector
forall a. Maybe a
Nothing
  fromDouble :: Double -> Concolic RegVal
fromDouble Double
d = RegVal -> Maybe BitVector -> Concolic RegVal
forall v. v -> Maybe BitVector -> Concolic v
Concolic (Double -> RegVal
forall v. ValueRepr v => Double -> v
E.fromDouble Double
d) Maybe BitVector
forall a. Maybe a
Nothing
  toWord64 :: Concolic RegVal -> Word64
toWord64 Concolic {concrete :: forall v. Concolic v -> v
concrete = RegVal
c} = RegVal -> Word64
forall v. ValueRepr v => v -> Word64
E.toWord64 RegVal
c
  getType :: Concolic RegVal -> ExtType
getType Concolic {concrete :: forall v. Concolic v -> v
concrete = RegVal
c} = RegVal -> ExtType
forall v. ValueRepr v => v -> ExtType
E.getType RegVal
c

  extend :: ExtType -> Bool -> Concolic RegVal -> Maybe (Concolic RegVal)
extend ExtType
ty Bool
s = (RegVal -> Maybe RegVal)
-> (BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Maybe (Concolic RegVal)
unaryOp (ExtType -> Bool -> RegVal -> Maybe RegVal
forall v. ValueRepr v => ExtType -> Bool -> v -> Maybe v
E.extend ExtType
ty Bool
s) (ExtType -> Bool -> BitVector -> Maybe BitVector
forall v. ValueRepr v => ExtType -> Bool -> v -> Maybe v
E.extend ExtType
ty Bool
s)
  extract :: ExtType -> Concolic RegVal -> Maybe (Concolic RegVal)
extract ExtType
ty = (RegVal -> Maybe RegVal)
-> (BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Maybe (Concolic RegVal)
unaryOp (ExtType -> RegVal -> Maybe RegVal
forall v. ValueRepr v => ExtType -> v -> Maybe v
E.extract ExtType
ty) (ExtType -> BitVector -> Maybe BitVector
forall v. ValueRepr v => ExtType -> v -> Maybe v
E.extract ExtType
ty)

  -- TODO: Add constraint which enforces concrete value on
  -- symbolic part instead of silently discarding it. See
  -- the address concretization implementation for details.
  floatToInt :: ExtType -> Bool -> Concolic RegVal -> Maybe (Concolic RegVal)
floatToInt ExtType
ty Bool
s Concolic {concrete :: forall v. Concolic v -> v
concrete = RegVal
c} =
    (RegVal -> Maybe BitVector -> Concolic RegVal
forall v. v -> Maybe BitVector -> Concolic v
`Concolic` Maybe BitVector
forall a. Maybe a
Nothing) (RegVal -> Concolic RegVal)
-> Maybe RegVal -> Maybe (Concolic RegVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExtType -> Bool -> RegVal -> Maybe RegVal
forall v. ValueRepr v => ExtType -> Bool -> v -> Maybe v
E.floatToInt ExtType
ty Bool
s RegVal
c
  intToFloat :: ExtType -> Bool -> Concolic RegVal -> Maybe (Concolic RegVal)
intToFloat ExtType
ty Bool
s Concolic {concrete :: forall v. Concolic v -> v
concrete = RegVal
c} =
    (RegVal -> Maybe BitVector -> Concolic RegVal
forall v. v -> Maybe BitVector -> Concolic v
`Concolic` Maybe BitVector
forall a. Maybe a
Nothing) (RegVal -> Concolic RegVal)
-> Maybe RegVal -> Maybe (Concolic RegVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExtType -> Bool -> RegVal -> Maybe RegVal
forall v. ValueRepr v => ExtType -> Bool -> v -> Maybe v
E.intToFloat ExtType
ty Bool
s RegVal
c
  extendFloat :: Concolic RegVal -> Maybe (Concolic RegVal)
extendFloat Concolic {concrete :: forall v. Concolic v -> v
concrete = RegVal
c} =
    (RegVal -> Maybe BitVector -> Concolic RegVal
forall v. v -> Maybe BitVector -> Concolic v
`Concolic` Maybe BitVector
forall a. Maybe a
Nothing) (RegVal -> Concolic RegVal)
-> Maybe RegVal -> Maybe (Concolic RegVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> Maybe v
E.extendFloat RegVal
c
  truncFloat :: Concolic RegVal -> Maybe (Concolic RegVal)
truncFloat Concolic {concrete :: forall v. Concolic v -> v
concrete = RegVal
c} =
    (RegVal -> Maybe BitVector -> Concolic RegVal
forall v. v -> Maybe BitVector -> Concolic v
`Concolic` Maybe BitVector
forall a. Maybe a
Nothing) (RegVal -> Concolic RegVal)
-> Maybe RegVal -> Maybe (Concolic RegVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> Maybe v
E.truncFloat RegVal
c

  add :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
add = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.add BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.add
  sub :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
sub = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.sub BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.sub
  mul :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
mul = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.mul BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.mul
  div :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
div = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.div BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.div
  or :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
or = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.or BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.or
  xor :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
xor = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.xor BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.xor
  and :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
and = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.and BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.and
  urem :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
urem = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.urem BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.urem
  srem :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
srem = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.srem BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.srem
  udiv :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
udiv = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.udiv BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.udiv

  neg :: Concolic RegVal -> Maybe (Concolic RegVal)
neg = (RegVal -> Maybe RegVal)
-> (BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Maybe (Concolic RegVal)
unaryOp RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> Maybe v
E.neg BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> Maybe v
E.neg

  sar :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
sar = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.sar BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.sar
  shr :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
shr = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.shr BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.shr
  shl :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
shl = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.shl BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.shl

  eq :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
eq = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.eq BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.eq
  ne :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
ne = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.ne BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.ne
  sle :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
sle = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.sle BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.sle
  slt :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
slt = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.slt BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.slt
  sge :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
sge = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.sge BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.sge
  sgt :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
sgt = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.sgt BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.sgt
  ule :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
ule = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.ule BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.ule
  ult :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
ult = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.ult BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.ult
  uge :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
uge = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.uge BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.uge
  ugt :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
ugt = (RegVal -> RegVal -> Maybe RegVal)
-> (BitVector -> BitVector -> Maybe BitVector)
-> Concolic RegVal
-> Concolic RegVal
-> Maybe (Concolic RegVal)
binaryOp RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.ugt BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
E.ugt

  -- TODO: Add constraint which enforces concrete value on
  -- symbolic part instead of silently discarding it. See
  -- the address concretization implementation for details.
  ord :: Concolic RegVal -> Concolic RegVal -> Maybe (Concolic RegVal)
ord Concolic RegVal
lhs Concolic RegVal
rhs = (RegVal -> Maybe BitVector -> Concolic RegVal
forall v. v -> Maybe BitVector -> Concolic v
`Concolic` Maybe BitVector
forall a. Maybe a
Nothing) (RegVal -> Concolic RegVal)
-> Maybe RegVal -> Maybe (Concolic RegVal)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RegVal -> RegVal -> Maybe RegVal
forall v. ValueRepr v => v -> v -> Maybe v
E.ord (Concolic RegVal -> RegVal
forall v. Concolic v -> v
concrete Concolic RegVal
lhs) (Concolic RegVal -> RegVal
forall v. Concolic v -> v
concrete Concolic RegVal
rhs)