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