qute

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