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.Symbolic.Expression
  6  ( BitVector,
  7    fromByte,
  8    fromReg,
  9    toSExpr,
 10    symbolic,
 11    bitSize,
 12    toCond,
 13  )
 14where
 15
 16import Control.DeepSeq (NFData)
 17import Control.Exception (assert)
 18import Data.Bits (shiftL, (.&.))
 19import Data.Word (Word64, Word8)
 20import GHC.Generics (Generic)
 21import Language.QBE.Simulator.Default.Expression qualified as D
 22import Language.QBE.Simulator.Expression qualified as E
 23import Language.QBE.Simulator.Memory qualified as MEM
 24import Language.QBE.Types qualified as QBE
 25import SimpleBV qualified as SMT
 26
 27-- TODO: Floating point support.
 28newtype BitVector = BitVector SMT.SExpr
 29  deriving (Show, Eq, Generic)
 30
 31instance NFData BitVector
 32
 33fromByte :: Word8 -> BitVector
 34fromByte byte = BitVector (SMT.bvLit 8 $ fromIntegral byte)
 35
 36fromReg :: D.RegVal -> BitVector
 37fromReg (D.VByte v) = BitVector (SMT.bvLit 8 $ fromIntegral v)
 38fromReg (D.VHalf v) = BitVector (SMT.bvLit 16 $ fromIntegral v)
 39fromReg (D.VWord v) = BitVector (SMT.bvLit 32 $ fromIntegral v)
 40fromReg (D.VLong v) = BitVector (SMT.bvLit 64 $ fromIntegral v)
 41fromReg (D.VSingle _) = error "symbolic floats not supported"
 42fromReg (D.VDouble _) = error "symbolic doubles not supported"
 43
 44toSExpr :: BitVector -> SMT.SExpr
 45toSExpr (BitVector s) = s
 46
 47symbolic :: String -> QBE.ExtType -> BitVector
 48symbolic name ty = BitVector (SMT.const name $ QBE.extTypeBitSize ty)
 49
 50bitSize :: BitVector -> Int
 51bitSize = SMT.width . toSExpr
 52
 53-- In the QBE a condition (see `jnz`) is true if the Word value is not zero.
 54toCond :: Bool -> BitVector -> SMT.SExpr
 55toCond isTrue bv =
 56  -- Equality is only defined for Words.
 57  assert (bitSize bv == QBE.baseTypeBitSize QBE.Word) $
 58    let zeroSExpr = toSExpr (fromReg $ E.fromLit (QBE.Base QBE.Word) 0)
 59     in toCond' (toSExpr bv) zeroSExpr
 60  where
 61    toCond' lhs rhs
 62      | isTrue = SMT.not (SMT.eq lhs rhs) -- /= 0
 63      | otherwise = SMT.eq lhs rhs -- == 0
 64
 65------------------------------------------------------------------------
 66
 67instance MEM.Storable BitVector BitVector where
 68  toBytes (BitVector s) =
 69    assert (size `mod` 8 == 0) $
 70      map (BitVector . nthByte s) [1 .. fromIntegral size `div` 8]
 71    where
 72      size :: Integer
 73      size = fromIntegral $ SMT.width s
 74
 75      nthByte :: SMT.SExpr -> Int -> SMT.SExpr
 76      nthByte expr n = SMT.extract expr ((n - 1) * 8) 8
 77
 78  fromBytes _ [] = Nothing
 79  fromBytes ty bytes@(BitVector s : xs) =
 80    if length bytes /= fromIntegral (QBE.loadByteSize ty)
 81      then Nothing
 82      else case (ty, bytes) of
 83        (QBE.LSubWord QBE.UnsignedByte, [_]) ->
 84          Just (BitVector (SMT.zeroExtend 24 concated))
 85        (QBE.LSubWord QBE.SignedByte, [_]) ->
 86          Just (BitVector (SMT.signExtend 24 concated))
 87        (QBE.LSubWord QBE.SignedHalf, [_, _]) ->
 88          Just (BitVector (SMT.signExtend 16 concated))
 89        (QBE.LSubWord QBE.UnsignedHalf, [_, _]) ->
 90          Just (BitVector (SMT.zeroExtend 16 concated))
 91        (QBE.LBase QBE.Word, [_, _, _, _]) ->
 92          Just (BitVector concated)
 93        (QBE.LBase QBE.Long, [_, _, _, _, _, _, _, _]) ->
 94          Just (BitVector concated)
 95        (QBE.LBase QBE.Single, [_, _, _, _]) ->
 96          error "float loading not implemented"
 97        (QBE.LBase QBE.Double, [_, _, _, _, _, _, _, _]) ->
 98          error "double loading not implemented"
 99        _ -> Nothing
100    where
101      concated :: SMT.SExpr
102      concated = foldl concatBV s xs
103
104      concatBV :: SMT.SExpr -> BitVector -> SMT.SExpr
105      concatBV acc (BitVector byte) =
106        assert (SMT.width byte == 8) $
107          SMT.concat byte acc
108
109------------------------------------------------------------------------
110
111binaryOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector
112binaryOp op (BitVector lhs) (BitVector rhs)
113  | SMT.width lhs == SMT.width rhs = Just $ BitVector (lhs `op` rhs)
114  | otherwise = Nothing
115
116-- TODO: Move this into the expression abstraction.
117toShiftAmount :: Word64 -> BitVector -> Maybe BitVector
118toShiftAmount size amount = amount `E.urem` E.fromLit (QBE.Base QBE.Word) size
119
120shiftOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector
121shiftOp op value amount@(BitVector SMT.Word) =
122  case bitSize value of
123    32 -> toShiftAmount 32 amount >>= binaryOp op value
124    64 -> do
125      shiftAmount <- toShiftAmount 64 amount
126      E.extend (QBE.Base QBE.Long) False shiftAmount >>= binaryOp op value
127    _ -> Nothing
128shiftOp _ _ _ = Nothing -- Shift amount must always be a Word.
129
130binaryBoolOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector
131binaryBoolOp op lhs rhs = do
132  bv <- binaryOp op lhs rhs
133  return $ BitVector (SMT.ite (toSExpr bv) trueValue falseValue)
134  where
135    -- TODO: Declare these as constants.
136    trueValue :: SMT.SExpr
137    trueValue = toSExpr $ E.fromLit (QBE.Base QBE.Long) 1
138
139    falseValue :: SMT.SExpr
140    falseValue = toSExpr $ E.fromLit (QBE.Base QBE.Long) 0
141
142instance E.ValueRepr BitVector where
143  fromLit ty n =
144    let size = QBE.extTypeBitSize ty
145        mask = (1 `shiftL` size) - 1
146     in BitVector $ SMT.bvLit (fromIntegral size) $ fromIntegral (n .&. mask)
147
148  fromFloat = error "symbolic floats currently unsupported"
149  fromDouble = error "symbolic doubles currently unsupported"
150
151  -- XXX: This only works for constants values, but this is fine since we implement
152  -- concolic execution and can obtain the address from the concrete value part.
153  toWord64 (BitVector value) =
154    case SMT.sexprToVal value of
155      SMT.Bits _ n -> fromIntegral n
156      _ -> error "unrechable"
157
158  getType v = case bitSize v of
159    08 -> QBE.Byte
160    16 -> QBE.HalfWord
161    32 -> QBE.Base QBE.Word
162    64 -> QBE.Base QBE.Long
163    _ -> error "unreachable"
164
165  floatToInt = error "symbolic float conversion not supported"
166  intToFloat = error "symbolic float conversion not supported"
167  extendFloat = error "symbolic float extension not supported"
168  truncFloat = error "symbolic float trunction not supported"
169
170  extend extTy isSigned val@(BitVector s)
171    | QBE.extTypeBitSize extTy <= bitSize val = Nothing
172    | otherwise = Just $ BitVector (extFunc targetSize s)
173    where
174      targetSize :: Integer
175      targetSize = fromIntegral $ QBE.extTypeBitSize extTy - bitSize val
176
177      extFunc :: Integer -> SMT.SExpr -> SMT.SExpr
178      extFunc = if isSigned then SMT.signExtend else SMT.zeroExtend
179
180  extract extTy val@(BitVector s)
181    | QBE.extTypeBitSize extTy > bitSize val = Nothing
182    | otherwise = Just $ BitVector (SMT.extract s 0 $ QBE.extTypeBitSize extTy)
183
184  add = binaryOp SMT.bvAdd
185  sub = binaryOp SMT.bvSub
186  mul = binaryOp SMT.bvMul
187  div = binaryOp SMT.bvSDiv
188  or = binaryOp SMT.bvOr
189  xor = binaryOp SMT.bvXOr
190  and = binaryOp SMT.bvAnd
191  urem = binaryOp SMT.bvURem
192  srem = binaryOp SMT.bvSRem
193  udiv = binaryOp SMT.bvUDiv
194
195  neg (BitVector v) = Just $ BitVector (SMT.bvNeg v)
196
197  sar = shiftOp SMT.bvAShr
198  shr = shiftOp SMT.bvLShr
199  shl = shiftOp SMT.bvShl
200
201  eq = binaryBoolOp SMT.eq
202  ne = binaryBoolOp (\lhs rhs -> SMT.not $ SMT.eq lhs rhs)
203  sle = binaryBoolOp SMT.bvSLeq
204  slt = binaryBoolOp SMT.bvSLt
205  sge = binaryBoolOp SMT.bvSGeq
206  sgt = binaryBoolOp SMT.bvSGt
207  ule = binaryBoolOp SMT.bvULeq
208  ult = binaryBoolOp SMT.bvULt
209  uge = binaryBoolOp SMT.bvUGeq
210  ugt = binaryBoolOp SMT.bvUGt
211
212  ord = error "symbolic ordered comparison not supported"
213  unord = error "symbolic unordered comparison not supported"