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
  6  ( Env (..),
  7    mkEnv,
  8    run,
  9    runPath,
 10    makeConcolic,
 11  )
 12where
 13
 14import Control.Monad.Catch (throwM)
 15import Control.Monad.IO.Class (liftIO)
 16import Control.Monad.State (MonadState, StateT, gets, modify, runStateT)
 17import Data.Map qualified as Map
 18import Data.Word (Word8)
 19import Language.QBE (Program)
 20import Language.QBE.Backend.Store qualified as ST
 21import Language.QBE.Backend.Tracer qualified as T
 22import Language.QBE.Simulator.Concolic.Expression qualified as CE
 23import Language.QBE.Simulator.Default.Expression qualified as DE
 24import Language.QBE.Simulator.Default.Funcs (lookupSimFunc)
 25import Language.QBE.Simulator.Default.State qualified as DS
 26import Language.QBE.Simulator.Error (EvalError (FuncArgsMismatch, TypingError))
 27import Language.QBE.Simulator.Expression qualified as E
 28import Language.QBE.Simulator.Memory qualified as MEM
 29import Language.QBE.Simulator.State
 30import Language.QBE.Simulator.Symbolic.Expression qualified as SE
 31import Language.QBE.Types qualified as QBE
 32import System.Random (initStdGen, mkStdGen)
 33
 34data Env
 35  = Env
 36  { envBase :: DS.Env (CE.Concolic DE.RegVal) (CE.Concolic Word8),
 37    envTracer :: T.ExecTrace,
 38    envStore :: ST.Store
 39  }
 40
 41mkEnv ::
 42  Program ->
 43  MEM.Address ->
 44  MEM.Size ->
 45  Maybe Int ->
 46  IO Env
 47mkEnv prog memStart memSize maySeed = do
 48  initEnv <- DS.mkEnv prog memStart memSize
 49  randGen <-
 50    case maySeed of
 51      Just sd -> pure $ mkStdGen sd
 52      Nothing -> initStdGen
 53  pure $ Env initEnv T.newExecTrace (ST.empty randGen)
 54
 55liftState ::
 56  (DS.SimState (CE.Concolic DE.RegVal) (CE.Concolic Word8)) a ->
 57  (StateT Env IO) a
 58liftState toLift = do
 59  defEnv <- gets envBase
 60  (a, s) <- liftIO $ runStateT toLift defEnv
 61  modify (\ps -> ps {envBase = s})
 62  pure a
 63
 64makeConcolic :: String -> QBE.ExtType -> StateT Env IO (CE.Concolic DE.RegVal)
 65makeConcolic name ty = do
 66  st <- gets envStore
 67  let (ns, cv) = ST.getConcolic st name ty
 68  modify (\e -> e {envStore = ns})
 69  pure cv
 70
 71modifyTracer :: (MonadState Env m) => (T.ExecTrace -> T.ExecTrace) -> m ()
 72modifyTracer f =
 73  modify (\s@Env {envTracer = t} -> s {envTracer = f t})
 74
 75makeSymbolicArray ::
 76  QBE.GlobalIdent ->
 77  [CE.Concolic DE.RegVal] ->
 78  StateT Env IO (Maybe (CE.Concolic DE.RegVal))
 79makeSymbolicArray _ [arrayPtr, numElem, elemSize, namePtr] = do
 80  name <- E.toString <$> (toAddress namePtr >>= readNullArray)
 81  vlty <- case E.toWord64 elemSize of
 82    1 -> pure QBE.Byte
 83    2 -> pure QBE.HalfWord
 84    4 -> pure (QBE.Base QBE.Word)
 85    8 -> pure (QBE.Base QBE.Long)
 86    _ -> throwM TypingError
 87
 88  values <-
 89    mapM
 90      (\n -> makeConcolic (name ++ show n) vlty)
 91      [1 .. E.toWord64 numElem]
 92
 93  arrayAddr <- toAddress arrayPtr
 94  liftState (DS.storeValues arrayAddr values) >> pure Nothing
 95makeSymbolicArray ident _ = throwM $ FuncArgsMismatch ident
 96
 97findSimFunc :: QBE.GlobalIdent -> Maybe ([CE.Concolic DE.RegVal] -> (StateT Env IO) (Maybe (CE.Concolic DE.RegVal)))
 98findSimFunc i@(QBE.GlobalIdent "quebex_make_symbolic") = Just (makeSymbolicArray i)
 99findSimFunc ident = lookupSimFunc ident
100
101instance Simulator (StateT Env IO) (CE.Concolic DE.RegVal) where
102  isTrue value = do
103    let condResult = E.toWord64 (CE.concrete value) /= 0
104    case CE.symbolic value of
105      Nothing -> pure condResult
106      Just sexpr -> do
107        -- Track the taken branch in the tracer.
108        let branch = T.newBranch sexpr
109        modifyTracer (\t -> T.appendBranch t condResult branch)
110
111        pure condResult
112
113  -- Implements address concretization as a memory model.
114  toAddress CE.Concolic {CE.concrete = cv, CE.symbolic = svMaybe} =
115    case svMaybe of
116      Just sv ->
117        case sv `E.eq` SE.fromReg cv of
118          Just c -> do
119            modifyTracer (`T.appendCons` c)
120            pure $ E.toWord64 cv
121          Nothing -> throwM TypingError
122      Nothing -> pure $ E.toWord64 cv
123
124  findFunc ident = do
125    funcs <- gets (DS.envFuncs . envBase)
126    pure $ case Map.lookup ident funcs of
127      Just x -> Just $ SFuncDef x
128      Nothing -> SSimFunc <$> findSimFunc ident
129  findFuncByAddr addr = do
130    fptrs <- gets (DS.envFuncAddrs . envBase)
131    case Map.lookup addr fptrs of
132      Just fn -> findFunc fn
133      Nothing -> pure Nothing
134
135  lookupSymbol = liftState . lookupSymbol
136  activeFrame = liftState activeFrame
137  pushStackFrame = liftState . pushStackFrame
138  popStackFrame = liftState popStackFrame
139  getSP = liftState getSP
140  setSP = liftState . setSP
141
142  writeMemory a t v = liftState (writeMemory a t v)
143  readMemory t a = liftState (readMemory t a)
144
145------------------------------------------------------------------------
146
147runPath :: StateT Env IO a -> StateT Env IO (T.ExecTrace, ST.Store)
148runPath state = do
149  _ <- state
150  t <- gets envTracer
151  s <- gets envStore
152  pure (t, s)
153
154run :: Env -> StateT Env IO a -> IO (T.ExecTrace, ST.Store)
155run env state = fst <$> runStateT (runPath state) env