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