qute

  1-- SPDX-FileCopyrightText: 2025-2026 Sören Tempel <soeren+git@soeren-tempel.net>
  2--
  3-- SPDX-License-Identifier: GPL-3.0-only
  4
  5-- | This module describes the semantics of the [QBE](https://c9x.me/compile/)
  6-- intermediate representation using an abstract 'Simulator' monad.
  7-- Specifically, it abstractly describes the semantics of QBE's control-flow
  8-- constructs (such as functions, statements, and blocks) and instructions
  9-- using the primitives of this monad. The semantics can then be concretely
 10-- instantiated (refer to the instance of the 'Simulator' monad). This idea
 11-- is inspired by the paper [Flexible Instruction-Set Semantics via Abstract Monads]
 12-- (https://dl.acm.org/doi/10.1145/3607833).
 13module Language.QBE.Simulator
 14  ( BlockResult,
 15    execInstr,
 16    execStmt,
 17    execBlock,
 18    execFunc,
 19  )
 20where
 21
 22import Control.Monad (unless, void, when)
 23import Control.Monad.Error.Class (throwError)
 24import Data.Functor ((<&>))
 25import Data.List (elemIndex, uncons)
 26import Data.Map qualified as Map
 27import Data.Maybe (fromMaybe, isJust, isNothing)
 28import Data.Word (Word8)
 29import Language.QBE.Simulator.ABI.C (writeVAList)
 30import Language.QBE.Simulator.Default.Expression qualified as DE
 31import Language.QBE.Simulator.Default.State
 32import Language.QBE.Simulator.Error
 33import Language.QBE.Simulator.Expression qualified as E
 34import Language.QBE.Simulator.Memory (addrOverlap)
 35import Language.QBE.Simulator.State
 36import Language.QBE.Types qualified as QBE
 37
 38-- | Execution of a 'QBE.Block' can either return (with an optional return
 39-- value) or it can jump to another 'QBE.Block' which will then be executed.
 40type BlockResult v = (Either (Maybe v) QBE.Block)
 41
 42------------------------------------------------------------------------
 43
 44execVolatile :: (Simulator m v) => QBE.VolatileInstr -> m ()
 45execVolatile (QBE.Store valTy valReg addrReg) = do
 46  -- Since byte and half are not first-class types in the IL, they are
 47  -- stored as words and have to be looked up as such.
 48  val <- case valTy of
 49    QBE.Byte -> lookupValue QBE.Word valReg
 50    QBE.HalfWord -> lookupValue QBE.Word valReg
 51    (QBE.Base bt) -> lookupValue bt valReg
 52
 53  addr <- lookupValue QBE.Long addrReg >>= toAddress
 54  writeMemory addr valTy val
 55execVolatile (QBE.Blit src dst toCopy) = do
 56  srcAddrVal <- lookupValue QBE.Long src
 57  dstAddrVal <- lookupValue QBE.Long dst
 58
 59  -- TODO: Check for invalid BLITs
 60  srcAddr <- toAddress srcAddrVal
 61  dstAddr <- toAddress dstAddrVal
 62  when (srcAddr /= dstAddr && addrOverlap srcAddr dstAddr toCopy) $
 63    throwError (OverlappingBlit srcAddr dstAddr)
 64
 65  -- Somehow allow specialization of memory copies, e.g. for qute-symex.
 66  when (toCopy > 0) $
 67    mapM_
 68      ( \off -> do
 69          srcByte <- readMemory (QBE.LSubWord QBE.UnsignedByte) (srcAddr + off)
 70          writeMemory (dstAddr + off) QBE.Byte srcByte
 71      )
 72      [0 .. toCopy - 1]
 73execVolatile (QBE.VAStart val) = do
 74  ptr <- lookupValue QBE.Long val >>= toAddress
 75  stk <- activeFrame
 76
 77  addrs <- mapM (\v -> (v,) <$> stackSpill v) (stkVarArgs stk)
 78  case uncons addrs of
 79    Just ((firstValue, firstAddr), _) -> do
 80      let valType = E.getType firstValue
 81          valSize = fromIntegral $ QBE.extTypeByteSize valType
 82
 83      -- The pointer stored in our representation of the `overflow_arg_area` of
 84      -- `va_list` points one element beyond the argument list. This allows us
 85      -- to determine the element pointer in `vaarg` by always substracting the
 86      -- size of the requested element from the pointer.
 87      --
 88      -- TODO: This is incompatible with the x86 System V ABI, which requires
 89      -- `overflow_arg_area` to be „initialized with the address of the first
 90      -- argument passed on the stack“. However, we can't do that because
 91      -- `stackSpill` places elements from low→high addresses on the stack and
 92      -- the x86 System V ABI assumes they are instead stored from high→low.
 93      let overflowPtr = firstAddr + valSize
 94      writeVAList ptr overflowPtr
 95    Nothing -> writeVAList ptr 0
 96execVolatile (QBE.DBGLoc {}) = pure ()
 97{-# INLINEABLE execVolatile #-}
 98
 99execBinaryTy ::
100  (Simulator m v) =>
101  QBE.BaseType ->
102  (v -> v -> Maybe v) ->
103  (QBE.BaseType, QBE.Value) ->
104  (QBE.BaseType, QBE.Value) ->
105  m v
106execBinaryTy retTy op (lty, lhs) (rty, rhs) = do
107  v1 <- lookupValue lty lhs
108  v2 <- lookupValue rty rhs
109  runBinary retTy op v1 v2
110
111execBinary ::
112  (Simulator m v) =>
113  QBE.BaseType ->
114  (v -> v -> Maybe v) ->
115  QBE.Value ->
116  QBE.Value ->
117  m v
118execBinary retTy op lhs rhs =
119  execBinaryTy retTy op (retTy, lhs) (retTy, rhs)
120{-# INLINE execBinary #-}
121
122execShift ::
123  (Simulator m v) =>
124  QBE.BaseType ->
125  (v -> v -> Maybe v) ->
126  QBE.Value ->
127  QBE.Value ->
128  m v
129execShift retTy op lhs amount =
130  execBinaryTy retTy op (retTy, lhs) (QBE.Word, amount)
131{-# INLINE execShift #-}
132
133-- | Execute a single 'QBE.Instr'. The 'QBE.BaseType' denotes the return value type.
134-- For example, as provided in the enclosing 'QBE.Assign'.
135execInstr :: (Simulator m v) => QBE.BaseType -> QBE.Instr -> m v
136execInstr retTy (QBE.Neg op) = do
137  v <- lookupValue retTy op
138  liftMaybe TypingError (E.neg v)
139execInstr retTy (QBE.Add lhs rhs) = execBinary retTy E.add lhs rhs
140execInstr retTy (QBE.Sub lhs rhs) = execBinary retTy E.sub lhs rhs
141execInstr retTy (QBE.Mul lhs rhs) = execBinary retTy E.mul lhs rhs
142execInstr retTy (QBE.Div lhs rhs) = execBinary retTy E.div lhs rhs
143execInstr retTy (QBE.Or lhs rhs) = execBinary retTy E.or lhs rhs
144execInstr retTy (QBE.Xor lhs rhs) = execBinary retTy E.xor lhs rhs
145execInstr retTy (QBE.And lhs rhs) = execBinary retTy E.and lhs rhs
146execInstr retTy (QBE.URem lhs rhs) = execBinary retTy E.urem lhs rhs
147execInstr retTy (QBE.Rem lhs rhs) = execBinary retTy E.srem lhs rhs
148execInstr retTy (QBE.UDiv lhs rhs) = execBinary retTy E.udiv lhs rhs
149execInstr retTy (QBE.Sar lhs rhs) = execShift retTy E.sar lhs rhs
150execInstr retTy (QBE.Shr lhs rhs) = execShift retTy E.shr lhs rhs
151execInstr retTy (QBE.Shl lhs rhs) = execShift retTy E.shl lhs rhs
152execInstr retTy (QBE.Load ty addrVal) = do
153  addr <- lookupValue QBE.Long addrVal >>= toAddress
154  val <- readMemory ty addr
155  subType retTy val
156execInstr QBE.Long (QBE.Alloc align sizeValue) = do
157  size <- lookupValue QBE.Long sizeValue
158  stackAlloc size (fromIntegral $ QBE.getSize align)
159execInstr _ QBE.Alloc {} = throwError InvalidAddressType
160execInstr retTy (QBE.CompareInt intArg cmpOp lhs rhs) = do
161  let cmpTy = QBE.i2BaseType intArg
162  v1 <- lookupValue cmpTy lhs
163  v2 <- lookupValue cmpTy rhs
164
165  let exprOp = E.compareIntExpr cmpOp
166  runBinary retTy exprOp v1 v2
167execInstr retTy (QBE.CompareFloat floatArg cmpOp lhs rhs) = do
168  let cmpTy = QBE.f2BaseType floatArg
169  v1 <- lookupValue cmpTy lhs
170  v2 <- lookupValue cmpTy rhs
171
172  let exprOp = E.compareFloatExpr cmpOp
173  runBinary retTy exprOp v1 v2
174-- exts is only valid with a double return type.
175execInstr QBE.Double (QBE.Ext QBE.ExtSingle value) = do
176  v <- lookupValue QBE.Single value
177  liftMaybe TypingError $ E.extendFloat v
178execInstr retTy (QBE.Ext extArg value) = do
179  v <- lookupValue QBE.Word value
180  let (isSigned, extTy) = QBE.toExtType extArg
181  liftMaybe
182    TypingError
183    (E.extract extTy v >>= E.extend (QBE.Base retTy) isSigned)
184execInstr QBE.Single (QBE.TruncDouble value) = do
185  v <- lookupValue QBE.Double value
186  liftMaybe TypingError $ E.truncFloat v
187-- truncd is only valid with a single return type.
188execInstr _ (QBE.TruncDouble _) = throwError TypingError
189execInstr retTy (QBE.Copy value) = lookupValue retTy value
190execInstr retTy (QBE.FloatToInt floatArg isSigned value) = do
191  v <- lookupValue (QBE.f2BaseType floatArg) value
192  liftMaybe TypingError $ E.floatToInt (QBE.Base retTy) isSigned v
193execInstr retTy (QBE.IntToFloat intArg isSigned value) = do
194  v <- lookupValue (QBE.i2BaseType intArg) value
195  liftMaybe TypingError $ E.intToFloat (QBE.Base retTy) isSigned v
196execInstr retTy (QBE.Cast value) = do
197  -- We must deduce the value type to use for lookup from
198  -- the return type as manadated by the cast type string.
199  let valueType =
200        case retTy of
201          QBE.Word -> QBE.Single
202          QBE.Long -> QBE.Double
203          QBE.Single -> QBE.Word
204          QBE.Double -> QBE.Long
205
206  -- TODO: Consider adding an explicit operation for casting
207  -- of floating points to the expression language abstraction.
208  v <- lookupValue valueType value
209  pure (E.fromLit (QBE.Base retTy) $ E.toWord64 v)
210execInstr retTy (QBE.VAArg argLst) = do
211  -- 'argsCtx' represents a `va_list` with the memory layout as
212  -- defined in the x86 System V ABI. Below, we extract the
213  -- `overflow_arg_area` pointer. The value of this pointer is
214  -- currently not aligned with the System V ABI. As such, the
215  -- implementation of `vaarg` is also incompatible with the
216  -- description of the `va_arg` macro in the System V ABI.
217  --
218  -- See the `vastart` implementation for more information.
219  argsCtx <- lookupValue QBE.Long argLst >>= toAddress
220  let overflowArgArea = argsCtx + 8
221
222  prevPtr <- readMemory (QBE.LBase QBE.Long) overflowArgArea
223  let retTySize =
224        E.fromLit
225          (QBE.Base QBE.Long)
226          (fromIntegral $ QBE.baseTypeByteSize retTy)
227
228  -- Obtain current pointer by subtracting size from 'prevPtr'
229  -- and align the pointer down to the nearest aligned address.
230  ptrAligned <-
231    liftMaybe InvalidAddressType $
232      (prevPtr `E.sub` retTySize) >>= (`stackAlign` retTySize)
233
234  val <- toAddress ptrAligned >>= readMemory (QBE.LBase retTy)
235  writeMemory overflowArgArea (QBE.Base QBE.Long) ptrAligned
236  pure val
237{-# INLINEABLE execInstr #-}
238
239-- | Execute a 'QBE.Statement', usually a sequence of 'QBE.Instruction'.
240-- Therefore, this function iteratively calls 'execInstr' in the common case.
241execStmt :: (Simulator m v) => QBE.Statement -> m ()
242execStmt (QBE.Assign name ty inst) = do
243  newVal <- execInstr ty inst
244  modifyFrame (storeLocal name newVal)
245execStmt (QBE.Volatile v) = execVolatile v
246execStmt (QBE.Call ret toCall params) = do
247  function <- lookupFunc toCall
248  funcArgs <- lookupArgs params
249  -- Sanity chekcs on funcArgs are performed by execFunc.
250
251  mayRetVal <- case function of
252    SFuncDef funcDef -> execFunc funcDef funcArgs
253    SSimFunc simFunc -> simFunc funcArgs
254
255  case mayRetVal of
256    Nothing ->
257      -- XXX: Could also check funcDef for the return value.
258      if isNothing ret
259        then pure ()
260        else throwError FunctionReturnIgnored
261    Just retVal ->
262      case ret of
263        Nothing -> throwError AssignedVoidReturnValue
264        Just (ident, abity) -> do
265          let baseTy = QBE.abityToBase abity
266          subTyped <- subType baseTy retVal
267          modifyFrame (storeLocal ident subTyped)
268{-# INLINEABLE execStmt #-}
269
270execJump :: (Simulator m v) => QBE.JumpInstr -> m (BlockResult v)
271execJump QBE.Halt = throwError EncounteredHalt
272execJump (QBE.Jump ident) = do
273  blocks <- QBE.fBlock <$> (activeFrame <&> stkFunc)
274  case Map.lookup ident blocks of
275    Just bl -> pure $ Right bl
276    Nothing -> throwError (UnknownBlock ident)
277execJump (QBE.Jnz cond ifT ifF) = do
278  condValue <- lookupValue QBE.Word cond
279  condResult <- isTrue condValue
280  execJump $ QBE.Jump (if condResult then ifT else ifF)
281execJump (QBE.Return v) = do
282  func <- activeFrame <&> stkFunc
283  case QBE.fAbity func of
284    Just abity -> do
285      retVal <-
286        case v of
287          Nothing -> throwError InvalidReturnValue
288          Just x -> pure x
289      lookupValue (QBE.abityToBase abity) retVal <&> (Left . Just)
290    Nothing ->
291      if isNothing v
292        then pure (Left Nothing)
293        else throwError InvalidReturnValue
294{-# INLINEABLE execJump #-}
295
296execPhi :: (Simulator m v) => Maybe QBE.BlockIdent -> QBE.Phi -> m ()
297execPhi Nothing _ = throwError InvalidPhiPosition
298execPhi (Just prevIdent) (QBE.Phi name ty labels) =
299  case Map.lookup prevIdent labels of
300    Nothing -> throwError (UnknownBlock prevIdent)
301    Just v -> do
302      retVal <- lookupValue ty v
303      modifyFrame (storeLocal name retVal)
304{-# INLINEABLE execPhi #-}
305
306-- | Execute a BasicBlock, as represented by 'QBE.Block', by iteratively
307-- invoking 'execStmt'. If this isn't the first executed BasicBlock within a a
308-- 'QBE.Function', then the 'QBE.BlockIdent' of the previously executed
309-- BasicBlock should be provided. This is required to properly execute [phi
310-- instructions](https://c9x.me/compile/doc/il-v1.2.html#Phi).
311execBlock :: (Simulator m v) => Maybe QBE.BlockIdent -> QBE.Block -> m (BlockResult v)
312execBlock prevIdent block = do
313  mapM_ (execPhi prevIdent) (QBE.phi block)
314  mapM_ execStmt (QBE.stmt block)
315  execJump (QBE.term block)
316{-# INLINEABLE execBlock #-}
317
318execTilRet :: (Simulator m v) => Maybe QBE.BlockIdent -> QBE.Block -> m (BlockResult v)
319execTilRet prevIdent block = go prevIdent (Right block)
320  where
321    go _ retValue@(Left _) = pure retValue
322    go prevIdent' (Right nextBlock) =
323      execBlock prevIdent' nextBlock >>= go (Just $ QBE.label nextBlock)
324{-# INLINEABLE execTilRet #-}
325
326-- | Execute a 'QBE.FuncDef' until function return. If the function requires arguments to
327-- be passed to it, these must be provided as a list. Limited sanity checking is performed
328-- to ensure that the provided arguments match the declared function parameters. The return
329-- value of 'execFunc' is the return value of the executed 'QBE.FuncDef'. If the function
330-- has no return value, 'Nothing' is returned here.
331execFunc :: (Simulator m v) => QBE.FuncDef -> [v] -> m (Maybe v)
332execFunc func@(QBE.FuncDef {QBE.fParams = params}) args = do
333  -- Assumption: Variadic argument has been filtered from args (see lookupArgs).
334  let varIdxMay = elemIndex QBE.Variadic params
335      numNamed = fromMaybe (length args) varIdxMay
336      argsSane =
337        if isJust varIdxMay
338          then length args + 1 >= length params -- +1 for filtered '...'
339          else length params == length args
340  unless argsSane $
341    throwError (FuncArgsMismatch $ QBE.fName func)
342
343  -- Separate name and unnamed variadic arguments using 'numNamed'
344  -- and create a 'StackFrame' for 'func' that captures both.
345  let vars =
346        Map.fromList $
347          zip (map paramName $ take numNamed params) args
348  void $ newStackFrame func vars (drop numNamed args)
349
350  blockResult <- execTilRet Nothing (QBE.fEntry func) <* returnFromFunc
351  case blockResult of
352    Right _block -> throwError MissingFunctionReturn
353    Left maybeValue -> pure maybeValue
354  where
355    paramName :: QBE.FuncParam -> QBE.LocalIdent
356    paramName (QBE.Regular _ n) = n
357    paramName (QBE.Env n) = n
358    paramName QBE.Variadic = error "unreachable"
359{-# SPECIALIZE execFunc :: QBE.FuncDef -> [DE.RegVal] -> SimState DE.RegVal Word8 (Maybe DE.RegVal) #-}
360{-# INLINEABLE execFunc #-}