qute

A software analysis framework built around the QBE intermediate language

git clone https://git.8pit.net/qute.git

  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.Default.Expression qualified as DE
 30import Language.QBE.Simulator.Default.State
 31import Language.QBE.Simulator.Error
 32import Language.QBE.Simulator.Expression qualified as E
 33import Language.QBE.Simulator.Memory (addrOverlap)
 34import Language.QBE.Simulator.State
 35import Language.QBE.Types qualified as QBE
 36
 37-- | Execution of a 'QBE.Block' can either return (with an optional return
 38-- value) or it can jump to another 'QBE.Block' which will then be executed.
 39type BlockResult v = (Either (Maybe v) QBE.Block)
 40
 41------------------------------------------------------------------------
 42
 43execVolatile :: (Simulator m v) => QBE.VolatileInstr -> m ()
 44execVolatile (QBE.Store valTy valReg addrReg) = do
 45  -- Since byte and half are not first-class types in the IL, they are
 46  -- stored as words and have to be looked up as such.
 47  val <- case valTy of
 48    QBE.Byte -> lookupValue QBE.Word valReg
 49    QBE.HalfWord -> lookupValue QBE.Word valReg
 50    (QBE.Base bt) -> lookupValue bt valReg
 51
 52  addr <- lookupValue QBE.Long addrReg >>= toAddress
 53  writeMemory addr valTy val
 54execVolatile (QBE.Blit src dst toCopy) = do
 55  srcAddrVal <- lookupValue QBE.Long src
 56  dstAddrVal <- lookupValue QBE.Long dst
 57
 58  -- TODO: Check for invalid BLITs
 59  srcAddr <- toAddress srcAddrVal
 60  dstAddr <- toAddress dstAddrVal
 61  when (srcAddr /= dstAddr && addrOverlap srcAddr dstAddr toCopy) $
 62    throwError $
 63      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      -- Initially, the pointer stored in our representation of the “variable
 84      -- argument list” points one element beyond the argument list. This
 85      -- allows us to determine the element pointer in `vaarg` by always
 86      -- substracting the size of the requested element from the pointer.
 87      writeMemory ptr (QBE.Base QBE.Long) $
 88        E.fromLit (QBE.Base QBE.Long) (firstAddr + valSize)
 89    Nothing -> pure ()
 90execVolatile (QBE.DBGLoc {}) = pure ()
 91{-# INLINEABLE execVolatile #-}
 92
 93execBinaryTy ::
 94  (Simulator m v) =>
 95  QBE.BaseType ->
 96  (v -> v -> Maybe v) ->
 97  (QBE.BaseType, QBE.Value) ->
 98  (QBE.BaseType, QBE.Value) ->
 99  m v
100execBinaryTy retTy op (lty, lhs) (rty, rhs) = do
101  v1 <- lookupValue lty lhs
102  v2 <- lookupValue rty rhs
103  runBinary retTy op v1 v2
104
105execBinary ::
106  (Simulator m v) =>
107  QBE.BaseType ->
108  (v -> v -> Maybe v) ->
109  QBE.Value ->
110  QBE.Value ->
111  m v
112execBinary retTy op lhs rhs =
113  execBinaryTy retTy op (retTy, lhs) (retTy, rhs)
114{-# INLINE execBinary #-}
115
116execShift ::
117  (Simulator m v) =>
118  QBE.BaseType ->
119  (v -> v -> Maybe v) ->
120  QBE.Value ->
121  QBE.Value ->
122  m v
123execShift retTy op lhs amount =
124  execBinaryTy retTy op (retTy, lhs) (QBE.Word, amount)
125{-# INLINE execShift #-}
126
127-- | Execute a single 'QBE.Instr'. The 'QBE.BaseType' denotes the return value type.
128-- For example, as provided in the enclosing 'QBE.Assign'.
129execInstr :: (Simulator m v) => QBE.BaseType -> QBE.Instr -> m v
130execInstr retTy (QBE.Neg op) = do
131  v <- lookupValue retTy op
132  liftMaybe TypingError (E.neg v)
133execInstr retTy (QBE.Add lhs rhs) = execBinary retTy E.add lhs rhs
134execInstr retTy (QBE.Sub lhs rhs) = execBinary retTy E.sub lhs rhs
135execInstr retTy (QBE.Mul lhs rhs) = execBinary retTy E.mul lhs rhs
136execInstr retTy (QBE.Div lhs rhs) = execBinary retTy E.div lhs rhs
137execInstr retTy (QBE.Or lhs rhs) = execBinary retTy E.or lhs rhs
138execInstr retTy (QBE.Xor lhs rhs) = execBinary retTy E.xor lhs rhs
139execInstr retTy (QBE.And lhs rhs) = execBinary retTy E.and lhs rhs
140execInstr retTy (QBE.URem lhs rhs) = execBinary retTy E.urem lhs rhs
141execInstr retTy (QBE.Rem lhs rhs) = execBinary retTy E.srem lhs rhs
142execInstr retTy (QBE.UDiv lhs rhs) = execBinary retTy E.udiv lhs rhs
143execInstr retTy (QBE.Sar lhs rhs) = execShift retTy E.sar lhs rhs
144execInstr retTy (QBE.Shr lhs rhs) = execShift retTy E.shr lhs rhs
145execInstr retTy (QBE.Shl lhs rhs) = execShift retTy E.shl lhs rhs
146execInstr retTy (QBE.Load ty addrVal) = do
147  addr <- lookupValue QBE.Long addrVal >>= toAddress
148  val <- readMemory ty addr
149  subType retTy val
150execInstr QBE.Long (QBE.Alloc align sizeValue) = do
151  size <- lookupValue QBE.Long sizeValue
152  stackAlloc size (fromIntegral $ QBE.getSize align)
153execInstr _ QBE.Alloc {} = throwError InvalidAddressType
154execInstr retTy (QBE.CompareInt intArg cmpOp lhs rhs) = do
155  let cmpTy = QBE.i2BaseType intArg
156  v1 <- lookupValue cmpTy lhs
157  v2 <- lookupValue cmpTy rhs
158
159  let exprOp = E.compareIntExpr cmpOp
160  runBinary retTy exprOp v1 v2
161execInstr retTy (QBE.CompareFloat floatArg cmpOp lhs rhs) = do
162  let cmpTy = QBE.f2BaseType floatArg
163  v1 <- lookupValue cmpTy lhs
164  v2 <- lookupValue cmpTy rhs
165
166  let exprOp = E.compareFloatExpr cmpOp
167  runBinary retTy exprOp v1 v2
168-- exts is only valid with a double return type.
169execInstr QBE.Double (QBE.Ext QBE.ExtSingle value) = do
170  v <- lookupValue QBE.Single value
171  liftMaybe TypingError $ E.extendFloat v
172execInstr retTy (QBE.Ext extArg value) = do
173  v <- lookupValue QBE.Word value
174  let (isSigned, extTy) = QBE.toExtType extArg
175  liftMaybe
176    TypingError
177    (E.extract extTy v >>= E.extend (QBE.Base retTy) isSigned)
178execInstr QBE.Single (QBE.TruncDouble value) = do
179  v <- lookupValue QBE.Double value
180  liftMaybe TypingError $ E.truncFloat v
181-- truncd is only valid with a single return type.
182execInstr _ (QBE.TruncDouble _) = throwError TypingError
183execInstr retTy (QBE.Copy value) = lookupValue retTy value
184execInstr retTy (QBE.FloatToInt floatArg isSigned value) = do
185  v <- lookupValue (QBE.f2BaseType floatArg) value
186  liftMaybe TypingError $ E.floatToInt (QBE.Base retTy) isSigned v
187execInstr retTy (QBE.IntToFloat intArg isSigned value) = do
188  v <- lookupValue (QBE.i2BaseType intArg) value
189  liftMaybe TypingError $ E.intToFloat (QBE.Base retTy) isSigned v
190execInstr retTy (QBE.Cast value) = do
191  -- We must deduce the value type to use for lookup from
192  -- the return type as manadated by the cast type string.
193  let valueType =
194        case retTy of
195          QBE.Word -> QBE.Single
196          QBE.Long -> QBE.Double
197          QBE.Single -> QBE.Word
198          QBE.Double -> QBE.Long
199
200  -- TODO: Consider adding an explicit operation for casting
201  -- of floating points to the expression language abstraction.
202  v <- lookupValue valueType value
203  pure (E.fromLit (QBE.Base retTy) $ E.toWord64 v)
204execInstr retTy (QBE.VAArg argLst) = do
205  -- 'argsCtx' represents the “variable argument list”. Currently,
206  -- it is not modeled after a specific ABI but simply contains a
207  -- pointer to the previous argument. This pointer is updated by
208  -- each invocation of the `vaarg` instruction.
209  argsCtx <- lookupValue QBE.Long argLst >>= toAddress
210
211  prevPtr <- readMemory (QBE.LBase QBE.Long) argsCtx
212  let retTySize =
213        E.fromLit
214          (QBE.Base QBE.Long)
215          (fromIntegral $ QBE.baseTypeByteSize retTy)
216
217  -- Obtain current pointer by subtracting size from 'prevPtr'
218  -- and align the pointer down to the nearest aligned address.
219  ptrAligned <-
220    liftMaybe InvalidAddressType $
221      (prevPtr `E.sub` retTySize) >>= (`stackAlign` retTySize)
222
223  val <- toAddress ptrAligned >>= readMemory (QBE.LBase retTy)
224  writeMemory argsCtx (QBE.Base QBE.Long) ptrAligned
225  pure val
226{-# INLINEABLE execInstr #-}
227
228-- | Execute a 'QBE.Statement', usually a sequence of 'QBE.Instruction'.
229-- Therefore, this function iteratively calls 'execInstr' in the common case.
230execStmt :: (Simulator m v) => QBE.Statement -> m ()
231execStmt (QBE.Assign name ty inst) = do
232  newVal <- execInstr ty inst
233  modifyFrame (storeLocal name newVal)
234execStmt (QBE.Volatile v) = execVolatile v
235execStmt (QBE.Call ret toCall params) = do
236  function <- lookupFunc toCall
237  funcArgs <- lookupArgs params
238  -- Sanity chekcs on funcArgs are performed by execFunc.
239
240  mayRetVal <- case function of
241    SFuncDef funcDef -> execFunc funcDef funcArgs
242    SSimFunc simFunc -> simFunc funcArgs
243
244  case mayRetVal of
245    Nothing ->
246      -- XXX: Could also check funcDef for the return value.
247      if isNothing ret
248        then pure ()
249        else throwError FunctionReturnIgnored
250    Just retVal ->
251      case ret of
252        Nothing -> throwError AssignedVoidReturnValue
253        Just (ident, abity) -> do
254          let baseTy = QBE.abityToBase abity
255          subTyped <- subType baseTy retVal
256          modifyFrame (storeLocal ident subTyped)
257{-# INLINEABLE execStmt #-}
258
259execJump :: (Simulator m v) => QBE.JumpInstr -> m (BlockResult v)
260execJump QBE.Halt = throwError EncounteredHalt
261execJump (QBE.Jump ident) = do
262  blocks <- QBE.fBlock <$> (activeFrame <&> stkFunc)
263  case Map.lookup ident blocks of
264    Just bl -> pure $ Right bl
265    Nothing -> throwError (UnknownBlock ident)
266execJump (QBE.Jnz cond ifT ifF) = do
267  condValue <- lookupValue QBE.Word cond
268  condResult <- isTrue condValue
269  execJump $ QBE.Jump (if condResult then ifT else ifF)
270execJump (QBE.Return v) = do
271  func <- activeFrame <&> stkFunc
272  case QBE.fAbity func of
273    Just abity -> do
274      retVal <-
275        case v of
276          Nothing -> throwError InvalidReturnValue
277          Just x -> pure x
278      lookupValue (QBE.abityToBase abity) retVal <&> (Left . Just)
279    Nothing ->
280      if isNothing v
281        then pure (Left Nothing)
282        else throwError InvalidReturnValue
283{-# INLINEABLE execJump #-}
284
285execPhi :: (Simulator m v) => Maybe QBE.BlockIdent -> QBE.Phi -> m ()
286execPhi Nothing _ = throwError InvalidPhiPosition
287execPhi (Just prevIdent) (QBE.Phi name ty labels) =
288  case Map.lookup prevIdent labels of
289    Nothing -> throwError (UnknownBlock prevIdent)
290    Just v -> do
291      retVal <- lookupValue ty v
292      modifyFrame (storeLocal name retVal)
293{-# INLINEABLE execPhi #-}
294
295-- | Execute a BasicBlock, as represented by 'QBE.Block', by iteratively
296-- invoking 'execStmt'. If this isn't the first executed BasicBlock within a a
297-- 'QBE.Function', then the 'QBE.BlockIdent' of the previously executed
298-- BasicBlock should be provided. This is required to properly execute [phi
299-- instructions](https://c9x.me/compile/doc/il-v1.2.html#Phi).
300execBlock :: (Simulator m v) => Maybe QBE.BlockIdent -> QBE.Block -> m (BlockResult v)
301execBlock prevIdent block = do
302  mapM_ (execPhi prevIdent) (QBE.phi block)
303  mapM_ execStmt (QBE.stmt block)
304  execJump (QBE.term block)
305{-# INLINEABLE execBlock #-}
306
307execTilRet :: (Simulator m v) => Maybe QBE.BlockIdent -> QBE.Block -> m (BlockResult v)
308execTilRet prevIdent block = go prevIdent (Right block)
309  where
310    go _ retValue@(Left _) = pure retValue
311    go prevIdent' (Right nextBlock) =
312      execBlock prevIdent' nextBlock >>= go (Just $ QBE.label nextBlock)
313{-# INLINEABLE execTilRet #-}
314
315-- | Execute a 'QBE.FuncDef' until function return. If the function requires arguments to
316-- be passed to it, these must be provided as a list. Limited sanity checking is performed
317-- to ensure that the provided arguments match the declared function parameters. The return
318-- value of 'execFunc' is the return value of the executed 'QBE.FuncDef'. If the function
319-- has no return value, 'Nothing' is returned here.
320execFunc :: (Simulator m v) => QBE.FuncDef -> [v] -> m (Maybe v)
321execFunc func@(QBE.FuncDef {QBE.fParams = params}) args = do
322  -- Assumption: Variadic argument has been filtered from args (see lookupArgs).
323  let varIdxMay = elemIndex QBE.Variadic params
324      numNamed = fromMaybe (length args) varIdxMay
325      argsSane =
326        if isJust varIdxMay
327          then length args + 1 >= length params -- +1 for filtered '...'
328          else length params == length args
329  unless argsSane $
330    throwError (FuncArgsMismatch $ QBE.fName func)
331
332  -- Separate name and unnamed variadic arguments using 'numNamed'
333  -- and create a 'StackFrame' for 'func' that captures both.
334  let vars =
335        Map.fromList $
336          zip (map paramName $ take numNamed params) args
337  void $ newStackFrame func vars (drop numNamed args)
338
339  blockResult <- execTilRet Nothing (QBE.fEntry func) <* returnFromFunc
340  case blockResult of
341    Right _block -> throwError MissingFunctionReturn
342    Left maybeValue -> pure maybeValue
343  where
344    paramName :: QBE.FuncParam -> QBE.LocalIdent
345    paramName (QBE.Regular _ n) = n
346    paramName (QBE.Env n) = n
347    paramName QBE.Variadic = error "unreachable"
348{-# SPECIALIZE execFunc :: QBE.FuncDef -> [DE.RegVal] -> SimState DE.RegVal Word8 (Maybe DE.RegVal) #-}
349{-# INLINEABLE execFunc #-}