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
 63-- TODO: Use QBE.ExtType here
 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      [0 .. 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_symbolic_array") = 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
130  lookupSymbol = liftState . lookupSymbol
131  activeFrame = liftState activeFrame
132  pushStackFrame = liftState . pushStackFrame
133  popStackFrame = liftState popStackFrame
134  getSP = liftState getSP
135  setSP = liftState . setSP
136
137  writeMemory a t v = liftState (writeMemory a t v)
138  readMemory t a = liftState (readMemory t a)
139
140------------------------------------------------------------------------
141
142run :: Env -> StateT Env IO a -> IO (T.ExecTrace, ST.Store)
143run env state = fst <$> runStateT go env
144  where
145    go = do
146      _ <- state
147      t <- gets envTracer
148      s <- gets envStore
149      pure (t, s)