qute

  1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
  2--
  3-- SPDX-License-Identifier: GPL-3.0-only
  4{-# LANGUAGE TemplateHaskell #-}
  5-- The code generated by template-haskell does not have type signatures.
  6{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
  7
  8-- | This module provides an implementation of the expression abstract from
  9-- 'Language.QBE.Simulator.Expression' which uses concrete fixed-width integer
 10-- values from "Data.Word" internally.
 11module Language.QBE.Simulator.Default.Expression
 12  ( RegVal (..),
 13    bitSize,
 14    fromBits,
 15  )
 16where
 17
 18import Control.Exception (assert)
 19import Data.Bits
 20  ( FiniteBits,
 21    finiteBitSize,
 22    shift,
 23    shiftR,
 24    unsafeShiftL,
 25    unsafeShiftR,
 26    xor,
 27    (.&.),
 28    (.|.),
 29  )
 30import Data.Int (Int16, Int32, Int64, Int8)
 31import Data.Word (Word16, Word32, Word64, Word8)
 32import GHC.Float
 33  ( castDoubleToWord64,
 34    castFloatToWord32,
 35    castWord32ToFloat,
 36    castWord64ToDouble,
 37    double2Float,
 38    float2Double,
 39  )
 40import Language.QBE.Simulator.Default.Generator (generateOperators)
 41import Language.QBE.Simulator.Expression qualified as E
 42import Language.QBE.Simulator.Memory qualified as MEM
 43import Language.QBE.Types qualified as QBE
 44
 45-- TODO: Can we just wrap base type here?
 46-- TODO: Do not export the constructors
 47data RegVal
 48  = VByte Word8
 49  | VHalf Word16
 50  | VWord Word32
 51  | VLong Word64
 52  | VSingle Float
 53  | VDouble Double
 54  deriving (Show, Eq)
 55
 56-- | Size of the value in bits.
 57bitSize :: RegVal -> Int
 58bitSize (VByte _) = 8
 59bitSize (VHalf _) = 16
 60bitSize (VWord _) = 32
 61bitSize (VLong _) = 64
 62bitSize (VSingle _) = 32
 63bitSize (VDouble _) = 64
 64
 65-- | Create a a 'RegVal' from an 'Integer' inferring the type from a given
 66-- amount of bits instead of requiring the user to provide a 'QBE.ExtType',
 67-- as required by 'Language.QBE.Simulator.Expression.fromLit'.
 68fromBits :: Int -> Integer -> Maybe RegVal
 69fromBits 08 = Just . VHalf . fromIntegral
 70fromBits 16 = Just . VHalf . fromIntegral
 71fromBits 32 = Just . VWord . fromIntegral
 72fromBits 64 = Just . VLong . fromIntegral
 73fromBits _ = const Nothing
 74
 75fromBool :: Bool -> RegVal
 76fromBool True = VLong 1
 77fromBool False = VLong 0
 78
 79------------------------------------------------------------------------
 80
 81shiftInstr ::
 82  (RegVal -> Word32 -> Maybe RegVal) ->
 83  RegVal ->
 84  RegVal ->
 85  Maybe RegVal
 86shiftInstr shiftOp val (VWord amount) = val `shiftOp` amount
 87shiftInstr _ _ _ = Nothing
 88
 89toShiftAmount :: Word32 -> Word32 -> Int
 90toShiftAmount valBitSize amount =
 91  -- From the QBE specification: "The shifting amount
 92  -- is taken modulo the size of the result type."
 93  let s = fromIntegral $ amount `mod` valBitSize
 94   in assert (s > 0) s
 95
 96shiftSar :: RegVal -> Word32 -> Maybe RegVal
 97shiftSar (VWord val) amount =
 98  (Just . VWord . fromIntegral) $
 99    (fromIntegral val :: Int32) `unsafeShiftR` toShiftAmount 32 amount
100shiftSar (VLong val) amount =
101  (Just . VLong . fromIntegral) $
102    (fromIntegral val :: Int64) `unsafeShiftR` toShiftAmount 64 amount
103shiftSar _ _ = Nothing
104
105shiftShr :: RegVal -> Word32 -> Maybe RegVal
106shiftShr (VWord val) amount =
107  (Just . VWord) $ val `unsafeShiftR` toShiftAmount 32 amount
108shiftShr (VLong val) amount =
109  (Just . VLong) $ val `unsafeShiftR` toShiftAmount 64 amount
110shiftShr _ _ = Nothing
111
112shiftShl :: RegVal -> Word32 -> Maybe RegVal
113shiftShl (VWord val) amount =
114  (Just . VWord) $ val `unsafeShiftL` toShiftAmount 32 amount
115shiftShl (VLong val) amount =
116  (Just . VLong) $ val `unsafeShiftL` toShiftAmount 64 amount
117shiftShl _ _ = Nothing
118
119------------------------------------------------------------------------
120
121regToBytes :: RegVal -> [Word8]
122regToBytes val =
123  let f w =
124        map
125          (\off -> fromIntegral $ shiftR w off .&. 0xff)
126          (take (bytesize w) $ iterate (+ 8) 0)
127   in case val of
128        (VByte v) -> [v]
129        (VWord v) -> f v
130        (VHalf v) -> f v
131        (VLong v) -> f v
132        (VSingle v) -> MEM.toBytes (VWord $ castFloatToWord32 v)
133        (VDouble v) -> MEM.toBytes (VLong $ castDoubleToWord64 v)
134  where
135    bytesize :: (FiniteBits a) => a -> Int
136    bytesize v = finiteBitSize v `div` 8
137
138regFromBytes :: QBE.LoadType -> [Word8] -> Maybe RegVal
139regFromBytes ty lst =
140  let f a =
141        foldl
142          (\acc (byte, idx) -> (fromIntegral byte `shift` (idx * 8)) .|. acc)
143          0
144          $ zip a [0 ..]
145   in case (ty, lst) of
146        (QBE.LSubWord QBE.UnsignedByte, [byte]) -> Just (VWord (fromIntegral byte))
147        (QBE.LSubWord QBE.SignedByte, [byte]) -> Just (VWord $ fromIntegral (fromIntegral byte :: Int8))
148        (QBE.LSubWord QBE.SignedHalf, bytes@[_, _]) -> Just (VWord $ fromIntegral (f bytes :: Int16))
149        (QBE.LSubWord QBE.UnsignedHalf, bytes@[_, _]) -> Just (VWord $ fromIntegral (f bytes :: Word16))
150        (QBE.LBase QBE.Word, bytes@[_, _, _, _]) -> Just (VWord $ f bytes)
151        (QBE.LBase QBE.Long, bytes@[_, _, _, _, _, _, _, _]) -> Just (VLong $ f bytes)
152        (QBE.LBase QBE.Single, bytes@[_, _, _, _]) ->
153          Just (VSingle $ castWord32ToFloat (f bytes))
154        (QBE.LBase QBE.Double, bytes@[_, _, _, _, _, _, _, _]) ->
155          Just (VDouble $ castWord64ToDouble (f bytes))
156        _ -> Nothing
157
158instance MEM.Storable RegVal Word8 where
159  toBytes = regToBytes
160  fromBytes = regFromBytes
161
162------------------------------------------------------------------------
163
164-- TODO: Insert the generated code directly into the instance declaration.
165generateOperators
166
167maxValue :: RegVal -> Maybe RegVal
168maxValue val =
169  let bitSiz = bitSize val
170      maxVal = (2 ^ bitSiz) - 1
171   in fromBits bitSiz maxVal
172
173withZeroDiv ::
174  Maybe RegVal ->
175  (RegVal -> RegVal -> Maybe RegVal) ->
176  RegVal ->
177  RegVal ->
178  Maybe RegVal
179withZeroDiv defVal op lhs rhs
180  | E.toWord64 rhs == 0 = defVal
181  | otherwise = op lhs rhs
182
183-- Signed division overflow occurs when the most-negative integer is divided by -1.
184withSDivOverflow ::
185  Maybe RegVal ->
186  (RegVal -> RegVal -> Maybe RegVal) ->
187  RegVal ->
188  RegVal ->
189  Maybe RegVal
190withSDivOverflow defVal op lhs rhs
191  | E.toWord64 lhs == mostNeg && E.toWord64 rhs == minusOne = defVal
192  | otherwise = op lhs rhs
193  where
194    numBits :: Int
195    numBits =
196      assert (bitSize lhs == bitSize rhs) $
197        bitSize lhs
198
199    minusOne :: Word64
200    minusOne = (2 ^ numBits) - 1
201
202    mostNeg :: Word64
203    mostNeg = 2 ^ (numBits - 1)
204
205-- We could also add support for unary operators to the generator. However,
206-- presently there is only one unary operator so it isn't worth it.
207neg' :: RegVal -> Maybe RegVal
208neg' (VWord v) = Just . VWord $ negate v
209neg' (VLong v) = Just . VLong $ negate v
210neg' (VSingle v) = Just . VSingle $ negate v
211neg' (VDouble v) = Just . VDouble $ negate v
212neg' _ = Nothing
213
214-- This can't be easily auto generated because the operation differs
215-- based on the type.
216div' :: RegVal -> RegVal -> Maybe RegVal
217div' (VWord lhs) (VWord rhs) =
218  (Just . VWord . fromIntegral) $
219    (fromIntegral lhs :: Int32) `quot` (fromIntegral rhs :: Int32)
220div' (VLong lhs) (VLong rhs) =
221  (Just . VLong . fromIntegral) $
222    (fromIntegral lhs :: Int64) `quot` (fromIntegral rhs :: Int64)
223div' (VSingle lhs) (VSingle rhs) = (Just . VSingle) $ lhs / rhs
224div' (VDouble lhs) (VDouble rhs) = (Just . VDouble) $ lhs / rhs
225div' _ _ = Nothing
226
227instance E.ValueRepr RegVal where
228  fromLit QBE.Byte n = VByte $ fromIntegral n
229  fromLit QBE.HalfWord n = VHalf $ fromIntegral n
230  fromLit (QBE.Base QBE.Long) n = VLong n
231  fromLit (QBE.Base QBE.Word) n = VWord $ fromIntegral n
232  fromLit (QBE.Base QBE.Single) n = VSingle $ castWord32ToFloat (fromIntegral n)
233  fromLit (QBE.Base QBE.Double) n = VDouble $ castWord64ToDouble n
234
235  toWord64 (VByte v) = fromIntegral v
236  toWord64 (VHalf v) = fromIntegral v
237  toWord64 (VWord v) = fromIntegral v
238  toWord64 (VLong v) = v
239  toWord64 (VSingle v) = fromIntegral $ castFloatToWord32 v
240  toWord64 (VDouble v) = castDoubleToWord64 v
241
242  fromFloat = VSingle
243  fromDouble = VDouble
244
245  -- stosi
246  floatToInt ty@(QBE.Base QBE.Word) True (VSingle v) =
247    Just $ E.fromLit ty (fromIntegral (truncate v :: Int32))
248  floatToInt ty@(QBE.Base QBE.Long) True (VSingle v) =
249    Just $ E.fromLit ty (fromIntegral (truncate v :: Int64))
250  -- stoui
251  floatToInt ty@(QBE.Base QBE.Word) False (VSingle v) =
252    Just $ E.fromLit ty (fromIntegral (truncate v :: Word32))
253  floatToInt ty@(QBE.Base QBE.Long) False (VSingle v) =
254    Just $ E.fromLit ty (truncate v :: Word64)
255  -- dtosi
256  floatToInt ty@(QBE.Base QBE.Word) True (VDouble v) =
257    Just $ E.fromLit ty (fromIntegral (truncate v :: Int32))
258  floatToInt ty@(QBE.Base QBE.Long) True (VDouble v) =
259    Just $ E.fromLit ty (fromIntegral (truncate v :: Int64))
260  -- dtoui
261  floatToInt ty@(QBE.Base QBE.Word) False (VDouble v) =
262    Just $ E.fromLit ty (fromIntegral (truncate v :: Word32))
263  floatToInt ty@(QBE.Base QBE.Long) False (VDouble v) =
264    Just $ E.fromLit ty (truncate v :: Word64)
265  -- rest
266  floatToInt _ _ _ = Nothing
267
268  -- swtof
269  intToFloat ty@(QBE.Base QBE.Single) True (VWord v) =
270    Just $ E.fromLit ty (fromIntegral (fromIntegral v :: Int32))
271  intToFloat ty@(QBE.Base QBE.Double) True (VWord v) =
272    Just $ E.fromLit ty (fromIntegral (fromIntegral v :: Int32))
273  -- uwtof
274  intToFloat ty@(QBE.Base QBE.Single) False (VWord v) =
275    Just $ E.fromLit ty (fromIntegral (fromIntegral v :: Word32))
276  intToFloat ty@(QBE.Base QBE.Double) False (VWord v) =
277    Just $ E.fromLit ty (fromIntegral (fromIntegral v :: Word32))
278  -- sltof
279  intToFloat ty@(QBE.Base QBE.Single) True (VLong v) =
280    Just $ E.fromLit ty (fromIntegral (fromIntegral v :: Int64))
281  intToFloat ty@(QBE.Base QBE.Double) True (VLong v) =
282    Just $ E.fromLit ty (fromIntegral (fromIntegral v :: Int64))
283  -- ultof
284  intToFloat ty@(QBE.Base QBE.Single) False (VLong v) =
285    Just $ E.fromLit ty (fromIntegral (fromIntegral v :: Word64))
286  intToFloat ty@(QBE.Base QBE.Double) False (VLong v) =
287    Just $ E.fromLit ty (fromIntegral (fromIntegral v :: Word64))
288  -- rest
289  intToFloat _ _ _ = Nothing
290
291  extendFloat (VSingle v) = Just $ VDouble (float2Double v)
292  extendFloat _ = Nothing
293
294  truncFloat (VDouble v) = Just $ VSingle (double2Float v)
295  truncFloat _ = Nothing
296
297  getType (VByte _) = QBE.Byte
298  getType (VHalf _) = QBE.HalfWord
299  getType (VWord _) = QBE.Base QBE.Word
300  getType (VLong _) = QBE.Base QBE.Long
301  getType (VSingle _) = QBE.Base QBE.Single
302  getType (VDouble _) = QBE.Base QBE.Double
303
304  -- TODO: Consider replacing Nothing cases with assert as this on the hot path.
305  extend extTy isSigned val
306    | QBE.extTypeBitSize extTy <= bitSize val = Nothing
307    | otherwise =
308        E.fromLit extTy
309          <$> case (isSigned, val) of
310            (True, VByte v) -> Just $ fromIntegral (fromIntegral v :: Int8)
311            (True, VHalf v) -> Just $ fromIntegral (fromIntegral v :: Int16)
312            (True, VWord v) -> Just $ fromIntegral (fromIntegral v :: Int32)
313            (True, VLong v) -> Just $ fromIntegral (fromIntegral v :: Int64)
314            (False, VByte v) -> Just $ fromIntegral (fromIntegral v :: Word8)
315            (False, VHalf v) -> Just $ fromIntegral (fromIntegral v :: Word16)
316            (False, VWord v) -> Just $ fromIntegral (fromIntegral v :: Word32)
317            (False, VLong v) -> Just $ fromIntegral (fromIntegral v :: Word64)
318            _ -> Nothing
319
320  -- TODO: Consider replacing Nothing cases with assert as this on the hot path.
321  extract (QBE.Base QBE.Single) _ = Nothing
322  extract (QBE.Base QBE.Double) _ = Nothing
323  extract _ (VSingle _) = Nothing
324  extract _ (VDouble _) = Nothing
325  extract extTy v
326    | QBE.extTypeBitSize extTy > bitSize v = Nothing
327    | otherwise =
328        let word = E.toWord64 v
329            mask = (2 `unsafeShiftL` (QBE.extTypeBitSize extTy - 1)) - 1
330         in Just $ E.fromLit extTy (word .&. mask)
331
332  -- This is needed to align the behavior of qute/ and qute-symex/ on
333  -- division-by-zero. QBE does not explicitly mandate a specific behavior
334  -- for this edge case. Therefore, in order to avoid extra branches in the
335  -- symbolic executor, we use the behavior mandated by SMT-LIB here.
336  --
337  -- TODO: Move this into the Expression abstraction (just like overshift handling).
338  div lhs = withZeroDiv (maxValue lhs) (withSDivOverflow (Just lhs) div') lhs
339  udiv lhs = withZeroDiv (maxValue lhs) udiv' lhs
340  urem lhs = withZeroDiv (Just lhs) urem' lhs
341  srem lhs = withZeroDiv (Just lhs) (withSDivOverflow (fromBits (bitSize lhs) 0) srem') lhs
342
343  add = add'
344  sub = sub'
345  mul = mul'
346  or = or'
347  xor = xor'
348  and = and'
349
350  neg = neg'
351
352  sar = shiftInstr shiftSar
353  shr = shiftInstr shiftShr
354  shl = shiftInstr shiftShl
355
356  -- TODO: Provide default implementations
357  eq = eq'
358  ne = ne'
359  sle = sle'
360  slt = slt'
361  sge = sge'
362  sgt = sgt'
363  ule = ule'
364  ult = ult'
365  uge = uge'
366  ugt = ugt'
367
368  ord (VSingle lhs) (VSingle rhs) =
369    Just . fromBool $ not (isNaN lhs || isNaN rhs)
370  ord (VDouble lhs) (VDouble rhs) =
371    Just . fromBool $ not (isNaN lhs || isNaN rhs)
372  ord _ _ = Nothing