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

module Language.QBE.Simulator.Concolic.State
  ( Env (..),
    mkEnv,
    run,
    runPath,
    makeConcolic,
    ErrorState (..),
    ErrorPath (..),
    SimState (..),
  )
where

import Control.Exception (Exception, throwIO, try)
import Control.Monad.Error.Class (MonadError, catchError, throwError)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.Monad.State.Strict
  ( MonadState,
    StateT (StateT),
    evalStateT,
    get,
    gets,
    modify,
    runStateT,
  )
import Data.Map qualified as Map
import Data.Word (Word8)
import Language.QBE (Program)
import Language.QBE.Backend.Store qualified as ST
import Language.QBE.Backend.Tracer qualified as T
import Language.QBE.Simulator.Concolic.Expression qualified as CE
import Language.QBE.Simulator.Default.Expression qualified as DE
import Language.QBE.Simulator.Default.Funcs (lookupSimFunc)
import Language.QBE.Simulator.Default.State qualified as DS
import Language.QBE.Simulator.Error (EvalError (FuncArgsMismatch, TypingError))
import Language.QBE.Simulator.Expression qualified as E
import Language.QBE.Simulator.Memory qualified as MEM
import Language.QBE.Simulator.State
import Language.QBE.Simulator.Symbolic.Expression qualified as SE
import Language.QBE.Types qualified as QBE
import System.Random (initStdGen, mkStdGen)

data Env
  = Env
  { Env -> Env (Concolic RegVal) (Concolic Word8)
envBase :: DS.Env (CE.Concolic DE.RegVal) (CE.Concolic Word8),
    Env -> ExecTrace
envTracer :: T.ExecTrace,
    Env -> Store
envStore :: ST.Store
  }

mkEnv ::
  Program ->
  MEM.Address ->
  MEM.Size ->
  Maybe Int ->
  IO Env
mkEnv :: Program -> Word64 -> Word64 -> Maybe Int -> IO Env
mkEnv Program
prog Word64
memStart Word64
memSize Maybe Int
maySeed = do
  Env (Concolic RegVal) (Concolic Word8)
initEnv <- Program
-> Word64 -> Word64 -> IO (Env (Concolic RegVal) (Concolic Word8))
forall v b.
(Storable v b, ValueRepr v) =>
Program -> Word64 -> Word64 -> IO (Env v b)
DS.mkEnv Program
prog Word64
memStart Word64
memSize
  StdGen
randGen <-
    case Maybe Int
maySeed of
      Just Int
sd -> StdGen -> IO StdGen
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (StdGen -> IO StdGen) -> StdGen -> IO StdGen
forall a b. (a -> b) -> a -> b
$ Int -> StdGen
mkStdGen Int
sd
      Maybe Int
Nothing -> IO StdGen
forall (m :: * -> *). MonadIO m => m StdGen
initStdGen
  Env -> IO Env
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env -> IO Env) -> Env -> IO Env
forall a b. (a -> b) -> a -> b
$ Env (Concolic RegVal) (Concolic Word8) -> ExecTrace -> Store -> Env
Env Env (Concolic RegVal) (Concolic Word8)
initEnv ExecTrace
T.newExecTrace (StdGen -> Store
ST.empty StdGen
randGen)

liftState ::
  (DS.SimState (CE.Concolic DE.RegVal) (CE.Concolic Word8)) a ->
  SimState a
liftState :: forall a.
SimState (Concolic RegVal) (Concolic Word8) a -> SimState a
liftState (DS.SimState StateT (Env (Concolic RegVal) (Concolic Word8)) IO a
toLift) = do
  Env (Concolic RegVal) (Concolic Word8)
defEnv <- (Env -> Env (Concolic RegVal) (Concolic Word8))
-> SimState (Env (Concolic RegVal) (Concolic Word8))
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Env -> Env (Concolic RegVal) (Concolic Word8)
envBase

  -- XXX: Since 'toLift' is run in the DS.SimState monad, it would
  -- use its 'throwError' implementation here. We want to use the
  -- implementation of our t'SimState' though, hence we need to handle
  -- IO exceptions here.
  Either EvalError (a, Env (Concolic RegVal) (Concolic Word8))
result <- IO (Either EvalError (a, Env (Concolic RegVal) (Concolic Word8)))
-> SimState
     (Either EvalError (a, Env (Concolic RegVal) (Concolic Word8)))
forall a. IO a -> SimState a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Either EvalError (a, Env (Concolic RegVal) (Concolic Word8)))
 -> SimState
      (Either EvalError (a, Env (Concolic RegVal) (Concolic Word8))))
-> IO
     (Either EvalError (a, Env (Concolic RegVal) (Concolic Word8)))
-> SimState
     (Either EvalError (a, Env (Concolic RegVal) (Concolic Word8)))
forall a b. (a -> b) -> a -> b
$ IO (a, Env (Concolic RegVal) (Concolic Word8))
-> IO
     (Either EvalError (a, Env (Concolic RegVal) (Concolic Word8)))
forall e a. Exception e => IO a -> IO (Either e a)
try (StateT (Env (Concolic RegVal) (Concolic Word8)) IO a
-> Env (Concolic RegVal) (Concolic Word8)
-> IO (a, Env (Concolic RegVal) (Concolic Word8))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT (Env (Concolic RegVal) (Concolic Word8)) IO a
toLift Env (Concolic RegVal) (Concolic Word8)
defEnv)
  case Either EvalError (a, Env (Concolic RegVal) (Concolic Word8))
result of
    Left (EvalError
e :: EvalError) -> EvalError -> SimState a
forall a. EvalError -> SimState a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError EvalError
e
    Right (a
a, Env (Concolic RegVal) (Concolic Word8)
s) -> do
      (Env -> Env) -> SimState ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\Env
ps -> Env
ps {envBase = s})
      a -> SimState a
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a

makeConcolic :: String -> QBE.ExtType -> SimState (CE.Concolic DE.RegVal)
makeConcolic :: String -> ExtType -> SimState (Concolic RegVal)
makeConcolic String
name ExtType
ty = do
  Store
st <- (Env -> Store) -> SimState Store
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Env -> Store
envStore
  let (Store
ns, Concolic RegVal
cv) = Store -> String -> ExtType -> (Store, Concolic RegVal)
ST.getConcolic Store
st String
name ExtType
ty
  (Env -> Env) -> SimState ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\Env
e -> Env
e {envStore = ns})
  Concolic RegVal -> SimState (Concolic RegVal)
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Concolic RegVal
cv

modifyTracer :: (MonadState Env m) => (T.ExecTrace -> T.ExecTrace) -> m ()
modifyTracer :: forall (m :: * -> *).
MonadState Env m =>
(ExecTrace -> ExecTrace) -> m ()
modifyTracer ExecTrace -> ExecTrace
f =
  (Env -> Env) -> m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (\s :: Env
s@Env {envTracer :: Env -> ExecTrace
envTracer = ExecTrace
t} -> Env
s {envTracer = f t})

makeSymbolicArray ::
  QBE.GlobalIdent ->
  [CE.Concolic DE.RegVal] ->
  SimState (Maybe (CE.Concolic DE.RegVal))
makeSymbolicArray :: GlobalIdent
-> [Concolic RegVal] -> SimState (Maybe (Concolic RegVal))
makeSymbolicArray GlobalIdent
_ [Concolic RegVal
arrayPtr, Concolic RegVal
numElem, Concolic RegVal
elemSize, Concolic RegVal
namePtr] = do
  String
name <- [Concolic RegVal] -> String
forall v. ValueRepr v => [v] -> String
E.toString ([Concolic RegVal] -> String)
-> SimState [Concolic RegVal] -> SimState String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Concolic RegVal -> SimState Word64
forall (m :: * -> *) v. Simulator m v => v -> m Word64
toAddress Concolic RegVal
namePtr SimState Word64
-> (Word64 -> SimState [Concolic RegVal])
-> SimState [Concolic RegVal]
forall a b. SimState a -> (a -> SimState b) -> SimState b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Word64 -> SimState [Concolic RegVal]
forall (m :: * -> *) v. Simulator m v => Word64 -> m [v]
readNullArray)
  ExtType
vlty <- case Concolic RegVal -> Word64
forall v. ValueRepr v => v -> Word64
E.toWord64 Concolic RegVal
elemSize of
    Word64
1 -> ExtType -> SimState ExtType
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ExtType
QBE.Byte
    Word64
2 -> ExtType -> SimState ExtType
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ExtType
QBE.HalfWord
    Word64
4 -> ExtType -> SimState ExtType
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BaseType -> ExtType
QBE.Base BaseType
QBE.Word)
    Word64
8 -> ExtType -> SimState ExtType
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (BaseType -> ExtType
QBE.Base BaseType
QBE.Long)
    Word64
_ -> EvalError -> SimState ExtType
forall a. EvalError -> SimState a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError EvalError
TypingError

  [Concolic RegVal]
values <-
    (Word64 -> SimState (Concolic RegVal))
-> [Word64] -> SimState [Concolic RegVal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM
      (\Word64
n -> String -> ExtType -> SimState (Concolic RegVal)
makeConcolic (String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. Show a => a -> String
show Word64
n) ExtType
vlty)
      [Word64
1 .. Concolic RegVal -> Word64
forall v. ValueRepr v => v -> Word64
E.toWord64 Concolic RegVal
numElem]

  Word64
arrayAddr <- Concolic RegVal -> SimState Word64
forall (m :: * -> *) v. Simulator m v => v -> m Word64
toAddress Concolic RegVal
arrayPtr
  SimState (Concolic RegVal) (Concolic Word8) Word64
-> SimState Word64
forall a.
SimState (Concolic RegVal) (Concolic Word8) a -> SimState a
liftState (StateT (Env (Concolic RegVal) (Concolic Word8)) IO Word64
-> SimState (Concolic RegVal) (Concolic Word8) Word64
forall v b a. StateT (Env v b) IO a -> SimState v b a
DS.SimState (StateT (Env (Concolic RegVal) (Concolic Word8)) IO Word64
 -> SimState (Concolic RegVal) (Concolic Word8) Word64)
-> StateT (Env (Concolic RegVal) (Concolic Word8)) IO Word64
-> SimState (Concolic RegVal) (Concolic Word8) Word64
forall a b. (a -> b) -> a -> b
$ Word64
-> [Concolic RegVal]
-> StateT (Env (Concolic RegVal) (Concolic Word8)) IO Word64
forall v b.
Storable v b =>
Word64 -> [v] -> StateT (Env v b) IO Word64
DS.storeValues Word64
arrayAddr [Concolic RegVal]
values) SimState Word64
-> SimState (Maybe (Concolic RegVal))
-> SimState (Maybe (Concolic RegVal))
forall a b. SimState a -> SimState b -> SimState b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (Concolic RegVal) -> SimState (Maybe (Concolic RegVal))
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Concolic RegVal)
forall a. Maybe a
Nothing
makeSymbolicArray GlobalIdent
ident [Concolic RegVal]
_ = EvalError -> SimState (Maybe (Concolic RegVal))
forall a. EvalError -> SimState a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (EvalError -> SimState (Maybe (Concolic RegVal)))
-> EvalError -> SimState (Maybe (Concolic RegVal))
forall a b. (a -> b) -> a -> b
$ GlobalIdent -> EvalError
FuncArgsMismatch GlobalIdent
ident

findSimFunc :: QBE.GlobalIdent -> Maybe ([CE.Concolic DE.RegVal] -> SimState (Maybe (CE.Concolic DE.RegVal)))
findSimFunc :: GlobalIdent
-> Maybe ([Concolic RegVal] -> SimState (Maybe (Concolic RegVal)))
findSimFunc i :: GlobalIdent
i@(QBE.GlobalIdent String
"qute_make_symbolic") = ([Concolic RegVal] -> SimState (Maybe (Concolic RegVal)))
-> Maybe ([Concolic RegVal] -> SimState (Maybe (Concolic RegVal)))
forall a. a -> Maybe a
Just (GlobalIdent
-> [Concolic RegVal] -> SimState (Maybe (Concolic RegVal))
makeSymbolicArray GlobalIdent
i)
findSimFunc GlobalIdent
ident = GlobalIdent
-> Maybe ([Concolic RegVal] -> SimState (Maybe (Concolic RegVal)))
forall (m :: * -> *) v.
(MonadIO m, ValueRepr v, Simulator m v) =>
GlobalIdent -> Maybe ([v] -> m (Maybe v))
lookupSimFunc GlobalIdent
ident

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

-- | State of the concolic executor with which an error was triggered
-- in the application code, which can be reproduced using this state.
data ErrorState
  = ErrorState
  { ErrorState -> ExecTrace
errTracer :: T.ExecTrace,
    ErrorState -> Store
errStore :: ST.Store
  }

-- | Exception thrown upon encountered an t'ErrorState'.
data ErrorPath
  = ErrorPath
  { ErrorPath -> ErrorState
pathInput :: ErrorState,
    ErrorPath -> EvalError
pathError :: EvalError
  }

instance Exception ErrorPath

instance Show ErrorPath where
  show :: ErrorPath -> String
show (ErrorPath ErrorState
_ EvalError
err) = EvalError -> String
forall a. Show a => a -> String
show EvalError
err

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

newtype SimState a = SimState {forall a. SimState a -> StateT Env IO a
unSimState :: StateT Env IO a}
  deriving ((forall a b. (a -> b) -> SimState a -> SimState b)
-> (forall a b. a -> SimState b -> SimState a) -> Functor SimState
forall a b. a -> SimState b -> SimState a
forall a b. (a -> b) -> SimState a -> SimState b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> SimState a -> SimState b
fmap :: forall a b. (a -> b) -> SimState a -> SimState b
$c<$ :: forall a b. a -> SimState b -> SimState a
<$ :: forall a b. a -> SimState b -> SimState a
Functor, Functor SimState
Functor SimState =>
(forall a. a -> SimState a)
-> (forall a b. SimState (a -> b) -> SimState a -> SimState b)
-> (forall a b c.
    (a -> b -> c) -> SimState a -> SimState b -> SimState c)
-> (forall a b. SimState a -> SimState b -> SimState b)
-> (forall a b. SimState a -> SimState b -> SimState a)
-> Applicative SimState
forall a. a -> SimState a
forall a b. SimState a -> SimState b -> SimState a
forall a b. SimState a -> SimState b -> SimState b
forall a b. SimState (a -> b) -> SimState a -> SimState b
forall a b c.
(a -> b -> c) -> SimState a -> SimState b -> SimState c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> SimState a
pure :: forall a. a -> SimState a
$c<*> :: forall a b. SimState (a -> b) -> SimState a -> SimState b
<*> :: forall a b. SimState (a -> b) -> SimState a -> SimState b
$cliftA2 :: forall a b c.
(a -> b -> c) -> SimState a -> SimState b -> SimState c
liftA2 :: forall a b c.
(a -> b -> c) -> SimState a -> SimState b -> SimState c
$c*> :: forall a b. SimState a -> SimState b -> SimState b
*> :: forall a b. SimState a -> SimState b -> SimState b
$c<* :: forall a b. SimState a -> SimState b -> SimState a
<* :: forall a b. SimState a -> SimState b -> SimState a
Applicative, Applicative SimState
Applicative SimState =>
(forall a b. SimState a -> (a -> SimState b) -> SimState b)
-> (forall a b. SimState a -> SimState b -> SimState b)
-> (forall a. a -> SimState a)
-> Monad SimState
forall a. a -> SimState a
forall a b. SimState a -> SimState b -> SimState b
forall a b. SimState a -> (a -> SimState b) -> SimState b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b. SimState a -> (a -> SimState b) -> SimState b
>>= :: forall a b. SimState a -> (a -> SimState b) -> SimState b
$c>> :: forall a b. SimState a -> SimState b -> SimState b
>> :: forall a b. SimState a -> SimState b -> SimState b
$creturn :: forall a. a -> SimState a
return :: forall a. a -> SimState a
Monad, Monad SimState
Monad SimState =>
(forall a. IO a -> SimState a) -> MonadIO SimState
forall a. IO a -> SimState a
forall (m :: * -> *).
Monad m =>
(forall a. IO a -> m a) -> MonadIO m
$cliftIO :: forall a. IO a -> SimState a
liftIO :: forall a. IO a -> SimState a
MonadIO)

deriving instance MonadState Env SimState

-- Implements 'MonadError' in t'SimState' via 'IOException's. On throw,
-- it also returns the relevant executor state by encapsulting it in
-- an 'ErrorPath'.
--
-- See also: The instance for 'DS.SimState'.
instance MonadError EvalError SimState where
  throwError :: forall a. EvalError -> SimState a
throwError EvalError
err = do
    Env {envTracer :: Env -> ExecTrace
envTracer = ExecTrace
t, envStore :: Env -> Store
envStore = Store
s} <- SimState Env
forall s (m :: * -> *). MonadState s m => m s
get
    IO a -> SimState a
forall a. IO a -> SimState a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> SimState a) -> IO a -> SimState a
forall a b. (a -> b) -> a -> b
$ ErrorPath -> IO a
forall e a. Exception e => e -> IO a
throwIO (ErrorState -> EvalError -> ErrorPath
ErrorPath (ExecTrace -> Store -> ErrorState
ErrorState ExecTrace
t Store
s) EvalError
err)

  catchError :: forall a. SimState a -> (EvalError -> SimState a) -> SimState a
catchError (SimState StateT Env IO a
st) EvalError -> SimState a
handler =
    StateT Env IO a -> SimState a
forall a. StateT Env IO a -> SimState a
SimState (StateT Env IO a -> SimState a) -> StateT Env IO a -> SimState a
forall a b. (a -> b) -> a -> b
$ StateT Env IO a
-> (EvalError -> StateT Env IO a) -> StateT Env IO a
forall t s a.
Exception t =>
StateT s IO a -> (t -> StateT s IO a) -> StateT s IO a
DS.unliftCatch StateT Env IO a
st (SimState a -> StateT Env IO a
forall a. SimState a -> StateT Env IO a
unSimState (SimState a -> StateT Env IO a)
-> (EvalError -> SimState a) -> EvalError -> StateT Env IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvalError -> SimState a
handler)

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

instance Simulator SimState (CE.Concolic DE.RegVal) where
  isTrue :: Concolic RegVal -> SimState Bool
isTrue Concolic RegVal
value = do
    let condResult :: Bool
condResult = RegVal -> Word64
forall v. ValueRepr v => v -> Word64
E.toWord64 (Concolic RegVal -> RegVal
forall v. Concolic v -> v
CE.concrete Concolic RegVal
value) Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
/= Word64
0
    case Concolic RegVal -> Maybe BitVector
forall v. Concolic v -> Maybe BitVector
CE.symbolic Concolic RegVal
value of
      Maybe BitVector
Nothing -> Bool -> SimState Bool
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
condResult
      Just BitVector
sexpr -> do
        -- Track the taken branch in the tracer.
        let branch :: Branch
branch = BitVector -> Branch
T.newBranch BitVector
sexpr
        (ExecTrace -> ExecTrace) -> SimState ()
forall (m :: * -> *).
MonadState Env m =>
(ExecTrace -> ExecTrace) -> m ()
modifyTracer (\ExecTrace
t -> ExecTrace -> Bool -> Branch -> ExecTrace
T.appendBranch ExecTrace
t Bool
condResult Branch
branch)

        Bool -> SimState Bool
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
condResult

  -- Implements address concretization as a memory model.
  toAddress :: Concolic RegVal -> SimState Word64
toAddress CE.Concolic {concrete :: forall v. Concolic v -> v
CE.concrete = RegVal
cv, symbolic :: forall v. Concolic v -> Maybe BitVector
CE.symbolic = Maybe BitVector
svMaybe} =
    case Maybe BitVector
svMaybe of
      Just BitVector
sv ->
        case BitVector
sv BitVector -> BitVector -> Maybe BitVector
forall v. ValueRepr v => v -> v -> Maybe v
`E.eq` RegVal -> BitVector
SE.fromReg RegVal
cv of
          Just BitVector
c -> do
            (ExecTrace -> ExecTrace) -> SimState ()
forall (m :: * -> *).
MonadState Env m =>
(ExecTrace -> ExecTrace) -> m ()
modifyTracer (ExecTrace -> BitVector -> ExecTrace
`T.appendCons` BitVector
c)
            Word64 -> SimState Word64
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Word64 -> SimState Word64) -> Word64 -> SimState Word64
forall a b. (a -> b) -> a -> b
$ RegVal -> Word64
forall v. ValueRepr v => v -> Word64
E.toWord64 RegVal
cv
          Maybe BitVector
Nothing -> EvalError -> SimState Word64
forall a. EvalError -> SimState a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError EvalError
TypingError
      Maybe BitVector
Nothing -> Word64 -> SimState Word64
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Word64 -> SimState Word64) -> Word64 -> SimState Word64
forall a b. (a -> b) -> a -> b
$ RegVal -> Word64
forall v. ValueRepr v => v -> Word64
E.toWord64 RegVal
cv

  findFunc :: GlobalIdent
-> SimState (Maybe (SomeFunc SimState (Concolic RegVal)))
findFunc GlobalIdent
ident = do
    Map GlobalIdent FuncDef
funcs <- (Env -> Map GlobalIdent FuncDef)
-> SimState (Map GlobalIdent FuncDef)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Env (Concolic RegVal) (Concolic Word8) -> Map GlobalIdent FuncDef
forall v b. Env v b -> Map GlobalIdent FuncDef
DS.envFuncs (Env (Concolic RegVal) (Concolic Word8) -> Map GlobalIdent FuncDef)
-> (Env -> Env (Concolic RegVal) (Concolic Word8))
-> Env
-> Map GlobalIdent FuncDef
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Env (Concolic RegVal) (Concolic Word8)
envBase)
    Maybe (SomeFunc SimState (Concolic RegVal))
-> SimState (Maybe (SomeFunc SimState (Concolic RegVal)))
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (SomeFunc SimState (Concolic RegVal))
 -> SimState (Maybe (SomeFunc SimState (Concolic RegVal))))
-> Maybe (SomeFunc SimState (Concolic RegVal))
-> SimState (Maybe (SomeFunc SimState (Concolic RegVal)))
forall a b. (a -> b) -> a -> b
$ case GlobalIdent -> Map GlobalIdent FuncDef -> Maybe FuncDef
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup GlobalIdent
ident Map GlobalIdent FuncDef
funcs of
      Just FuncDef
x -> SomeFunc SimState (Concolic RegVal)
-> Maybe (SomeFunc SimState (Concolic RegVal))
forall a. a -> Maybe a
Just (SomeFunc SimState (Concolic RegVal)
 -> Maybe (SomeFunc SimState (Concolic RegVal)))
-> SomeFunc SimState (Concolic RegVal)
-> Maybe (SomeFunc SimState (Concolic RegVal))
forall a b. (a -> b) -> a -> b
$ FuncDef -> SomeFunc SimState (Concolic RegVal)
forall (m :: * -> *) v. FuncDef -> SomeFunc m v
SFuncDef FuncDef
x
      Maybe FuncDef
Nothing -> ([Concolic RegVal] -> SimState (Maybe (Concolic RegVal)))
-> SomeFunc SimState (Concolic RegVal)
forall (m :: * -> *) v. ([v] -> m (Maybe v)) -> SomeFunc m v
SSimFunc (([Concolic RegVal] -> SimState (Maybe (Concolic RegVal)))
 -> SomeFunc SimState (Concolic RegVal))
-> Maybe ([Concolic RegVal] -> SimState (Maybe (Concolic RegVal)))
-> Maybe (SomeFunc SimState (Concolic RegVal))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> GlobalIdent
-> Maybe ([Concolic RegVal] -> SimState (Maybe (Concolic RegVal)))
findSimFunc GlobalIdent
ident
  findFuncByAddr :: Word64 -> SimState (Maybe (SomeFunc SimState (Concolic RegVal)))
findFuncByAddr Word64
addr = do
    Map Word64 GlobalIdent
fptrs <- (Env -> Map Word64 GlobalIdent)
-> SimState (Map Word64 GlobalIdent)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (Env (Concolic RegVal) (Concolic Word8) -> Map Word64 GlobalIdent
forall v b. Env v b -> Map Word64 GlobalIdent
DS.envFuncAddrs (Env (Concolic RegVal) (Concolic Word8) -> Map Word64 GlobalIdent)
-> (Env -> Env (Concolic RegVal) (Concolic Word8))
-> Env
-> Map Word64 GlobalIdent
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Env (Concolic RegVal) (Concolic Word8)
envBase)
    case Word64 -> Map Word64 GlobalIdent -> Maybe GlobalIdent
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Word64
addr Map Word64 GlobalIdent
fptrs of
      Just GlobalIdent
fn -> GlobalIdent
-> SimState (Maybe (SomeFunc SimState (Concolic RegVal)))
forall (m :: * -> *) v.
Simulator m v =>
GlobalIdent -> m (Maybe (SomeFunc m v))
findFunc GlobalIdent
fn
      Maybe GlobalIdent
Nothing -> Maybe (SomeFunc SimState (Concolic RegVal))
-> SimState (Maybe (SomeFunc SimState (Concolic RegVal)))
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (SomeFunc SimState (Concolic RegVal))
forall a. Maybe a
Nothing

  lookupSymbol :: GlobalIdent -> SimState (Maybe Word64)
lookupSymbol = SimState (Concolic RegVal) (Concolic Word8) (Maybe Word64)
-> SimState (Maybe Word64)
forall a.
SimState (Concolic RegVal) (Concolic Word8) a -> SimState a
liftState (SimState (Concolic RegVal) (Concolic Word8) (Maybe Word64)
 -> SimState (Maybe Word64))
-> (GlobalIdent
    -> SimState (Concolic RegVal) (Concolic Word8) (Maybe Word64))
-> GlobalIdent
-> SimState (Maybe Word64)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GlobalIdent
-> SimState (Concolic RegVal) (Concolic Word8) (Maybe Word64)
forall (m :: * -> *) v.
Simulator m v =>
GlobalIdent -> m (Maybe Word64)
lookupSymbol
  activeFrame :: SimState (StackFrame (Concolic RegVal))
activeFrame = SimState
  (Concolic RegVal) (Concolic Word8) (StackFrame (Concolic RegVal))
-> SimState (StackFrame (Concolic RegVal))
forall a.
SimState (Concolic RegVal) (Concolic Word8) a -> SimState a
liftState SimState
  (Concolic RegVal) (Concolic Word8) (StackFrame (Concolic RegVal))
forall (m :: * -> *) v. Simulator m v => m (StackFrame v)
activeFrame
  pushStackFrame :: StackFrame (Concolic RegVal) -> SimState ()
pushStackFrame = SimState (Concolic RegVal) (Concolic Word8) () -> SimState ()
forall a.
SimState (Concolic RegVal) (Concolic Word8) a -> SimState a
liftState (SimState (Concolic RegVal) (Concolic Word8) () -> SimState ())
-> (StackFrame (Concolic RegVal)
    -> SimState (Concolic RegVal) (Concolic Word8) ())
-> StackFrame (Concolic RegVal)
-> SimState ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StackFrame (Concolic RegVal)
-> SimState (Concolic RegVal) (Concolic Word8) ()
forall (m :: * -> *) v. Simulator m v => StackFrame v -> m ()
pushStackFrame
  popStackFrame :: SimState (StackFrame (Concolic RegVal))
popStackFrame = SimState
  (Concolic RegVal) (Concolic Word8) (StackFrame (Concolic RegVal))
-> SimState (StackFrame (Concolic RegVal))
forall a.
SimState (Concolic RegVal) (Concolic Word8) a -> SimState a
liftState SimState
  (Concolic RegVal) (Concolic Word8) (StackFrame (Concolic RegVal))
forall (m :: * -> *) v. Simulator m v => m (StackFrame v)
popStackFrame
  getSP :: SimState (Concolic RegVal)
getSP = SimState (Concolic RegVal) (Concolic Word8) (Concolic RegVal)
-> SimState (Concolic RegVal)
forall a.
SimState (Concolic RegVal) (Concolic Word8) a -> SimState a
liftState SimState (Concolic RegVal) (Concolic Word8) (Concolic RegVal)
forall (m :: * -> *) v. Simulator m v => m v
getSP
  setSP :: Concolic RegVal -> SimState ()
setSP = SimState (Concolic RegVal) (Concolic Word8) () -> SimState ()
forall a.
SimState (Concolic RegVal) (Concolic Word8) a -> SimState a
liftState (SimState (Concolic RegVal) (Concolic Word8) () -> SimState ())
-> (Concolic RegVal
    -> SimState (Concolic RegVal) (Concolic Word8) ())
-> Concolic RegVal
-> SimState ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concolic RegVal -> SimState (Concolic RegVal) (Concolic Word8) ()
forall (m :: * -> *) v. Simulator m v => v -> m ()
setSP

  writeMemory :: Word64 -> ExtType -> Concolic RegVal -> SimState ()
writeMemory Word64
a ExtType
t Concolic RegVal
v = SimState (Concolic RegVal) (Concolic Word8) () -> SimState ()
forall a.
SimState (Concolic RegVal) (Concolic Word8) a -> SimState a
liftState (Word64
-> ExtType
-> Concolic RegVal
-> SimState (Concolic RegVal) (Concolic Word8) ()
forall (m :: * -> *) v.
Simulator m v =>
Word64 -> ExtType -> v -> m ()
writeMemory Word64
a ExtType
t Concolic RegVal
v)
  readMemory :: LoadType -> Word64 -> SimState (Concolic RegVal)
readMemory LoadType
t Word64
a = SimState (Concolic RegVal) (Concolic Word8) (Concolic RegVal)
-> SimState (Concolic RegVal)
forall a.
SimState (Concolic RegVal) (Concolic Word8) a -> SimState a
liftState (LoadType
-> Word64
-> SimState (Concolic RegVal) (Concolic Word8) (Concolic RegVal)
forall (m :: * -> *) v. Simulator m v => LoadType -> Word64 -> m v
readMemory LoadType
t Word64
a)

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

runPath :: SimState a -> SimState (T.ExecTrace, ST.Store)
runPath :: forall a. SimState a -> SimState (ExecTrace, Store)
runPath SimState a
state = do
  a
_ <- SimState a
state
  ExecTrace
t <- (Env -> ExecTrace) -> SimState ExecTrace
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Env -> ExecTrace
envTracer
  Store
s <- (Env -> Store) -> SimState Store
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets Env -> Store
envStore
  (ExecTrace, Store) -> SimState (ExecTrace, Store)
forall a. a -> SimState a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExecTrace
t, Store
s)

run :: Env -> SimState a -> IO (T.ExecTrace, ST.Store)
run :: forall a. Env -> SimState a -> IO (ExecTrace, Store)
run Env
env SimState a
state = StateT Env IO (ExecTrace, Store) -> Env -> IO (ExecTrace, Store)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (SimState (ExecTrace, Store) -> StateT Env IO (ExecTrace, Store)
forall a. SimState a -> StateT Env IO a
unSimState (SimState (ExecTrace, Store) -> StateT Env IO (ExecTrace, Store))
-> SimState (ExecTrace, Store) -> StateT Env IO (ExecTrace, Store)
forall a b. (a -> b) -> a -> b
$ SimState a -> SimState (ExecTrace, Store)
forall a. SimState a -> SimState (ExecTrace, Store)
runPath SimState a
state) Env
env