quebex

  1-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel <soeren+git@soeren-tempel.net>
  2--
  3-- SPDX-License-Identifier: GPL-3.0-only
  4
  5module Language.QBE.Simulator.Concolic.State
  6  ( Env (..),
  7    mkEnv,
  8    run,
  9    runPath,
 10    makeConcolic,
 11    ErrorState (..),
 12    ErrorPath (..),
 13    SimState (..),
 14  )
 15where
 16
 17import Control.Exception (Exception, throwIO, try)
 18import Control.Monad.Error.Class (MonadError, catchError, throwError)
 19import Control.Monad.IO.Class (MonadIO, liftIO)
 20import Control.Monad.State.Strict
 21  ( MonadState,
 22    StateT (StateT),
 23    evalStateT,
 24    get,
 25    gets,
 26    modify,
 27    runStateT,
 28  )
 29import Data.Map qualified as Map
 30import Data.Word (Word8)
 31import Language.QBE (Program)
 32import Language.QBE.Backend.Store qualified as ST
 33import Language.QBE.Backend.Tracer qualified as T
 34import Language.QBE.Simulator.Concolic.Expression qualified as CE
 35import Language.QBE.Simulator.Default.Expression qualified as DE
 36import Language.QBE.Simulator.Default.Funcs (lookupSimFunc)
 37import Language.QBE.Simulator.Default.State qualified as DS
 38import Language.QBE.Simulator.Error (EvalError (FuncArgsMismatch, TypingError))
 39import Language.QBE.Simulator.Expression qualified as E
 40import Language.QBE.Simulator.Memory qualified as MEM
 41import Language.QBE.Simulator.State
 42import Language.QBE.Simulator.Symbolic.Expression qualified as SE
 43import Language.QBE.Types qualified as QBE
 44import System.Random (initStdGen, mkStdGen)
 45
 46data Env
 47  = Env
 48  { envBase :: DS.Env (CE.Concolic DE.RegVal) (CE.Concolic Word8),
 49    envTracer :: T.ExecTrace,
 50    envStore :: ST.Store
 51  }
 52
 53mkEnv ::
 54  Program ->
 55  MEM.Address ->
 56  MEM.Size ->
 57  Maybe Int ->
 58  IO Env
 59mkEnv prog memStart memSize maySeed = do
 60  initEnv <- DS.mkEnv prog memStart memSize
 61  randGen <-
 62    case maySeed of
 63      Just sd -> pure $ mkStdGen sd
 64      Nothing -> initStdGen
 65  pure $ Env initEnv T.newExecTrace (ST.empty randGen)
 66
 67liftState ::
 68  (DS.SimState (CE.Concolic DE.RegVal) (CE.Concolic Word8)) a ->
 69  SimState a
 70liftState (DS.SimState toLift) = do
 71  defEnv <- gets envBase
 72
 73  -- XXX: Since 'toLift' is run in the DS.SimState monad, it would
 74  -- use its 'throwError' implementation here. We want to use the
 75  -- implementation of our 'SimState' though, hence we need to handle
 76  -- IO exceptions here.
 77  result <- liftIO $ try (runStateT toLift defEnv)
 78  case result of
 79    Left (e :: EvalError) -> throwError e
 80    Right (a, s) -> do
 81      modify (\ps -> ps {envBase = s})
 82      pure a
 83
 84makeConcolic :: String -> QBE.ExtType -> SimState (CE.Concolic DE.RegVal)
 85makeConcolic name ty = do
 86  st <- gets envStore
 87  let (ns, cv) = ST.getConcolic st name ty
 88  modify (\e -> e {envStore = ns})
 89  pure cv
 90
 91modifyTracer :: (MonadState Env m) => (T.ExecTrace -> T.ExecTrace) -> m ()
 92modifyTracer f =
 93  modify (\s@Env {envTracer = t} -> s {envTracer = f t})
 94
 95makeSymbolicArray ::
 96  QBE.GlobalIdent ->
 97  [CE.Concolic DE.RegVal] ->
 98  SimState (Maybe (CE.Concolic DE.RegVal))
 99makeSymbolicArray _ [arrayPtr, numElem, elemSize, namePtr] = do
100  name <- E.toString <$> (toAddress namePtr >>= readNullArray)
101  vlty <- case E.toWord64 elemSize of
102    1 -> pure QBE.Byte
103    2 -> pure QBE.HalfWord
104    4 -> pure (QBE.Base QBE.Word)
105    8 -> pure (QBE.Base QBE.Long)
106    _ -> throwError TypingError
107
108  values <-
109    mapM
110      (\n -> makeConcolic (name ++ show n) vlty)
111      [1 .. E.toWord64 numElem]
112
113  arrayAddr <- toAddress arrayPtr
114  liftState (DS.SimState $ DS.storeValues arrayAddr values) >> pure Nothing
115makeSymbolicArray ident _ = throwError $ FuncArgsMismatch ident
116
117findSimFunc :: QBE.GlobalIdent -> Maybe ([CE.Concolic DE.RegVal] -> SimState (Maybe (CE.Concolic DE.RegVal)))
118findSimFunc i@(QBE.GlobalIdent "quebex_make_symbolic") = Just (makeSymbolicArray i)
119findSimFunc ident = lookupSimFunc ident
120
121------------------------------------------------------------------------
122
123-- | State of the concolic executor with which an error was triggered
124-- in the application code, which can be reproduced using this state.
125data ErrorState
126  = ErrorState
127  { errTracer :: T.ExecTrace,
128    errStore :: ST.Store
129  }
130
131-- | Exception thrown upon encountered an 'ErrorState'.
132data ErrorPath
133  = ErrorPath
134  { pathInput :: ErrorState,
135    pathError :: EvalError
136  }
137
138instance Exception ErrorPath
139
140instance Show ErrorPath where
141  show (ErrorPath _ err) = show err
142
143------------------------------------------------------------------------
144
145newtype SimState a = SimState {unSimState :: StateT Env IO a}
146  deriving (Functor, Applicative, Monad, MonadIO)
147
148deriving instance MonadState Env SimState
149
150-- Implements 'MonadError' in 'SimState' via 'IOException's. On throw,
151-- it also returns the relevant executor state by encapsulting it in
152-- an 'ErrorPath'.
153--
154-- See also: The instance for 'DS.SimState'.
155instance MonadError EvalError SimState where
156  throwError err = do
157    Env {envTracer = t, envStore = s} <- get
158    liftIO $ throwIO (ErrorPath (ErrorState t s) err)
159
160  catchError (SimState st) handler =
161    SimState $ DS.unliftCatch st (unSimState . handler)
162
163------------------------------------------------------------------------
164
165instance Simulator SimState (CE.Concolic DE.RegVal) where
166  isTrue value = do
167    let condResult = E.toWord64 (CE.concrete value) /= 0
168    case CE.symbolic value of
169      Nothing -> pure condResult
170      Just sexpr -> do
171        -- Track the taken branch in the tracer.
172        let branch = T.newBranch sexpr
173        modifyTracer (\t -> T.appendBranch t condResult branch)
174
175        pure condResult
176
177  -- Implements address concretization as a memory model.
178  toAddress CE.Concolic {CE.concrete = cv, CE.symbolic = svMaybe} =
179    case svMaybe of
180      Just sv ->
181        case sv `E.eq` SE.fromReg cv of
182          Just c -> do
183            modifyTracer (`T.appendCons` c)
184            pure $ E.toWord64 cv
185          Nothing -> throwError TypingError
186      Nothing -> pure $ E.toWord64 cv
187
188  findFunc ident = do
189    funcs <- gets (DS.envFuncs . envBase)
190    pure $ case Map.lookup ident funcs of
191      Just x -> Just $ SFuncDef x
192      Nothing -> SSimFunc <$> findSimFunc ident
193  findFuncByAddr addr = do
194    fptrs <- gets (DS.envFuncAddrs . envBase)
195    case Map.lookup addr fptrs of
196      Just fn -> findFunc fn
197      Nothing -> pure Nothing
198
199  lookupSymbol = liftState . lookupSymbol
200  activeFrame = liftState activeFrame
201  pushStackFrame = liftState . pushStackFrame
202  popStackFrame = liftState popStackFrame
203  getSP = liftState getSP
204  setSP = liftState . setSP
205
206  writeMemory a t v = liftState (writeMemory a t v)
207  readMemory t a = liftState (readMemory t a)
208
209------------------------------------------------------------------------
210
211runPath :: SimState a -> SimState (T.ExecTrace, ST.Store)
212runPath state = do
213  _ <- state
214  t <- gets envTracer
215  s <- gets envStore
216  pure (t, s)
217
218run :: Env -> SimState a -> IO (T.ExecTrace, ST.Store)
219run env state = evalStateT (unSimState $ runPath state) env