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.Catch (throwM)
 8import Control.Monad.IO.Class (liftIO)
 9import Control.Monad.State (MonadState, StateT, gets, modify, runStateT)
10import Data.Word (Word8)
11import Language.QBE (Program, globalFuncs)
12import Language.QBE.Backend.Tracer qualified as T
13import Language.QBE.Simulator.Concolic.Expression qualified as CE
14import Language.QBE.Simulator.Default.Expression qualified as DE
15import Language.QBE.Simulator.Default.State qualified as DS
16import Language.QBE.Simulator.Error (EvalError (TypingError))
17import Language.QBE.Simulator.Expression qualified as E
18import Language.QBE.Simulator.State
19import Language.QBE.Simulator.Symbolic.Expression qualified as SE
20
21data Env
22  = Env
23  { envBase :: DS.Env (CE.Concolic DE.RegVal) (CE.Concolic Word8),
24    envTracer :: T.ExecTrace
25  }
26
27liftState ::
28  (DS.SimState (CE.Concolic DE.RegVal) (CE.Concolic Word8)) a ->
29  (StateT Env IO) a
30liftState toLift = do
31  defEnv <- gets envBase
32  (a, s) <- liftIO $ runStateT toLift defEnv
33  modify (\ps -> ps {envBase = s})
34  pure a
35
36modifyTracer :: (MonadState Env m) => (T.ExecTrace -> T.ExecTrace) -> m ()
37modifyTracer f =
38  modify (\s@Env {envTracer = t} -> s {envTracer = f t})
39
40instance Simulator (StateT Env IO) (CE.Concolic DE.RegVal) where
41  isTrue value = do
42    let condResult = E.toWord64 (CE.concrete value) /= 0
43    case CE.symbolic value of
44      Nothing -> pure condResult
45      Just sexpr -> do
46        -- Track the taken branch in the tracer.
47        let branch = T.newBranch sexpr
48        modifyTracer (\t -> T.appendBranch t condResult branch)
49
50        pure condResult
51
52  -- Implements address concretization as a memory model.
53  toAddress CE.Concolic {CE.concrete = cv, CE.symbolic = svMaybe} =
54    case svMaybe of
55      Just sv ->
56        case sv `E.eq` SE.fromReg cv of
57          Just c -> do
58            modifyTracer (`T.appendCons` c)
59            pure $ E.toWord64 cv
60          Nothing -> throwM TypingError
61      Nothing -> pure $ E.toWord64 cv
62
63  lookupGlobal = liftState . lookupGlobal
64  findFunc = liftState . findFunc
65
66  activeFrame = liftState activeFrame
67  pushStackFrame = liftState . pushStackFrame
68  popStackFrame = liftState popStackFrame
69  getSP = liftState getSP
70  setSP = liftState . setSP
71
72  writeMemory a t v = liftState (writeMemory a t v)
73  readMemory t a = liftState (readMemory t a)
74
75------------------------------------------------------------------------
76
77run :: Program -> StateT Env IO a -> IO T.ExecTrace
78run prog state = do
79  initEnv' <- liftIO $ DS.mkEnv (globalFuncs prog) 0x0 128 -- TODO
80  fst <$> runStateT (state >> gets envTracer) (Env initEnv' T.newExecTrace)