qute

 1-- SPDX-FileCopyrightText: 2026 Sören Tempel <soeren+git@soeren-tempel.net>
 2--
 3-- SPDX-License-Identifier: GPL-3.0-only
 4
 5-- | This module provides utility functions for interfacing with C code.
 6module Language.QBE.Simulator.ABI.C
 7  ( charRepr,
 8    readString,
 9    readArray,
10    writeBuffer,
11    writeVAList,
12  )
13where
14
15import Control.Monad (foldM_)
16import Data.Word (Word64)
17import Language.QBE.Simulator.Expression qualified as E
18import Language.QBE.Simulator.Memory qualified as MEM
19import Language.QBE.Simulator.State (Simulator, readMemory, writeMemory)
20import Language.QBE.Types qualified as QBE
21
22-- | Representation of a @char@ in C.
23charRepr :: QBE.LoadType
24charRepr = QBE.LSubWord QBE.SignedByte
25
26-- | Read a null-terminated C string from memory at the given 'MEM.Address'.
27-- The return value is a list of 8-bit values.
28readString :: (Simulator m v) => MEM.Address -> m [v]
29readString addr = go addr []
30  where
31    go a acc = do
32      byte <- readMemory charRepr a
33      if E.toWord64 byte == 0
34        then pure acc
35        else go (a + 1) (acc ++ [byte])
36{-# INLINE readString #-}
37
38-- | Read an array of a fixed size, starting from a given 'MEM.Address'.
39-- The array is assumed to only store elements of the given 'QBE.LoadType'.
40readArray :: (Simulator m v) => MEM.Address -> QBE.LoadType -> Word64 -> m [v]
41readArray addr elemTy numElems =
42  mapM (\off -> readMemory elemTy (addr + off)) [0 .. numElems - 1]
43{-# INLINE readArray #-}
44
45-- | Write a list of values to a memory buffer located at the given 'MEM.Address'.
46writeBuffer :: (Simulator m v) => MEM.Address -> [v] -> m ()
47writeBuffer = foldM_ go
48  where
49    go lastAddr el = do
50      let elTy = E.getType el
51          elSize = fromIntegral $ QBE.extTypeByteSize elTy
52      writeMemory lastAddr elTy el
53      pure $ lastAddr + elSize
54{-# INLINE writeBuffer #-}
55
56-- | This writes the @overflow_arg_area@ of a @va_list@ in memory, as defined
57-- in the x86-64-ABI psABI.
58writeVAList :: (Simulator m v) => MEM.Address -> MEM.Address -> m ()
59writeVAList ptr overflowPtr = do
60  -- This is the layout of the `va_list` from the x86 System V ABI. It is
61  -- implemented in a way that it signals that all vaargs are on the stack.
62  --
63  -- See also <https://github.com/klee/klee/blob/v3.3/lib/Core/Executor.cpp#L1962-L1981>.
64  writeMemory ptr (QBE.Base QBE.Word) $
65    E.fromLit (QBE.Base QBE.Word) 48 -- gp_offset
66  writeMemory (ptr + 4) (QBE.Base QBE.Word) $
67    E.fromLit (QBE.Base QBE.Word) 176 -- fp_offset
68  writeMemory (ptr + 8) (QBE.Base QBE.Long) $
69    E.fromLit (QBE.Base QBE.Long) overflowPtr -- overflow_arg_area
70  writeMemory (ptr + 16) (QBE.Base QBE.Long) $
71    E.fromLit (QBE.Base QBE.Long) 0 -- reg_save_area
72{-# INLINE writeVAList #-}