quebex

 1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
 2--
 3-- SPDX-License-Identifier: GPL-3.0-only
 4
 5module Language.QBE.Simulator.Concolic.State (run) where
 6
 7import Control.Monad.IO.Class (liftIO)
 8import Control.Monad.State (StateT, gets, modify, runStateT)
 9import Data.Word (Word8)
10import Language.QBE (Program, globalFuncs)
11import Language.QBE.Backend.Tracer qualified as T
12import Language.QBE.Simulator.Concolic.Expression qualified as CE
13import Language.QBE.Simulator.Default.Expression qualified as DE
14import Language.QBE.Simulator.Default.State qualified as DS
15import Language.QBE.Simulator.State
16
17data Env
18  = Env
19  { envBase :: DS.Env (CE.Concolic DE.RegVal) (CE.Concolic Word8),
20    envTracer :: T.ExecTrace
21  }
22
23liftState ::
24  (DS.SimState (CE.Concolic DE.RegVal) (CE.Concolic Word8)) a ->
25  (StateT Env IO) a
26liftState toLift = do
27  defEnv <- gets envBase
28  (a, s) <- liftIO $ runStateT toLift defEnv
29  modify (\ps -> ps {envBase = s})
30  pure a
31
32instance Simulator (StateT Env IO) (CE.Concolic DE.RegVal) where
33  condBranch CE.Concolic {CE.symbolic = Just sexpr} condResult = do
34    let branch = T.newBranch sexpr
35    modify
36      ( \s@Env {envTracer = t} ->
37          s {envTracer = T.appendBranch t condResult branch}
38      )
39  condBranch _ _ = pure ()
40
41  lookupGlobal = liftState . lookupGlobal
42  findFunc = liftState . findFunc
43
44  activeFrame = liftState activeFrame
45  pushStackFrame = liftState . pushStackFrame
46  popStackFrame = liftState popStackFrame
47  getSP = liftState getSP
48  setSP = liftState . setSP
49
50  writeMemory a t v = liftState (writeMemory a t v)
51  readMemory t a = liftState (readMemory t a)
52
53------------------------------------------------------------------------
54
55run :: Program -> StateT Env IO a -> IO T.ExecTrace
56run prog state = do
57  initEnv' <- liftIO $ DS.mkEnv (globalFuncs prog) 0x0 128 -- TODO
58  fst <$> runStateT (state >> gets envTracer) (Env initEnv' T.newExecTrace)