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    fromSExpr,
 10    toSExpr,
 11    symbolic,
 12    toCond,
 13  )
 14where
 15
 16import Control.Exception (assert)
 17import Data.Word (Word64, Word8)
 18import Language.QBE.Simulator.Default.Expression qualified as D
 19import Language.QBE.Simulator.Expression qualified as E
 20import Language.QBE.Simulator.Memory qualified as MEM
 21import Language.QBE.Simulator.Symbolic.Folding qualified as F
 22import Language.QBE.Types qualified as QBE
 23import SimpleSMT qualified as SMT
 24
 25-- This types supports more than just the 'QBE.BaseType' to ease the
 26-- implementation of the 'MEM.Storable' type class. Essentially, this
 27-- data type just provides a generic BitVector abstraction on top of
 28-- 'SMT.SExpr'.
 29data BitVector
 30  = BitVector
 31  { sexpr :: SMT.SExpr,
 32    -- TODO: For BitVectors, we can extract the type from the SExpr.
 33    -- Technically, we don't need the 'ExtType' here and can just
 34    -- turn this into a newtype.
 35    qtype :: QBE.ExtType
 36  }
 37  deriving (Show, Eq)
 38
 39fromByte :: Word8 -> BitVector
 40fromByte byte = BitVector (SMT.bvBin 8 $ fromIntegral byte) QBE.Byte
 41
 42fromReg :: D.RegVal -> BitVector
 43fromReg (D.VWord v) = BitVector (SMT.bvBin 32 $ fromIntegral v) (QBE.Base QBE.Word)
 44fromReg (D.VLong v) = BitVector (SMT.bvBin 64 $ fromIntegral v) (QBE.Base QBE.Long)
 45fromReg (D.VSingle _) = error "symbolic floats not supported"
 46fromReg (D.VDouble _) = error "symbolic doubles not supported"
 47
 48fromSExpr :: QBE.BaseType -> SMT.SExpr -> BitVector
 49fromSExpr ty sexpr = BitVector sexpr (QBE.Base ty)
 50
 51toSExpr :: BitVector -> SMT.SExpr
 52toSExpr = sexpr
 53
 54symbolic :: SMT.Solver -> String -> QBE.BaseType -> IO BitVector
 55symbolic solver name ty = do
 56  let bits = SMT.tBits $ fromIntegral (QBE.baseTypeBitSize ty)
 57  sym <- SMT.declare solver name bits
 58  return $ BitVector sym (QBE.Base ty)
 59
 60-- In the QBE a condition (see `jnz`) is true if the Word value is not zero.
 61toCond :: Bool -> BitVector -> SMT.SExpr
 62toCond isTrue BitVector {sexpr = s, qtype = ty} =
 63  -- Equality is only defined for Words.
 64  assert (ty == QBE.Base QBE.Word) $
 65    let zeroSExpr = sexpr (fromReg $ E.fromLit QBE.Word 0)
 66     in toCond' s zeroSExpr
 67  where
 68    toCond' lhs rhs
 69      | isTrue = F.notExpr (F.eqExpr lhs rhs) -- /= 0
 70      | otherwise = F.eqExpr lhs rhs -- == 0
 71
 72------------------------------------------------------------------------
 73
 74instance MEM.Storable BitVector BitVector where
 75  toBytes BitVector {sexpr = s, qtype = ty} =
 76    assert (size `mod` 8 == 0) $
 77      map (\n -> BitVector (nthByte s n) QBE.Byte) [1 .. fromIntegral size `div` 8]
 78    where
 79      size :: Integer
 80      size = fromIntegral $ QBE.extTypeBitSize ty
 81
 82      nthByte :: SMT.SExpr -> Int -> SMT.SExpr
 83      nthByte expr n = F.extractExpr expr ((n - 1) * 8) 8
 84
 85  fromBytes _ [] = Nothing
 86  fromBytes ty bytes@(BitVector {sexpr = s} : xs) =
 87    if length bytes /= fromIntegral (QBE.loadByteSize ty)
 88      then Nothing
 89      else case (ty, bytes) of
 90        (QBE.LSubWord QBE.UnsignedByte, [_]) ->
 91          Just (BitVector (SMT.zeroExtend 24 concated) (QBE.Base QBE.Word))
 92        (QBE.LSubWord QBE.SignedByte, [_]) ->
 93          Just (BitVector (SMT.signExtend 24 concated) (QBE.Base QBE.Word))
 94        (QBE.LSubWord QBE.SignedHalf, [_, _]) ->
 95          Just (BitVector (SMT.signExtend 16 concated) (QBE.Base QBE.Word))
 96        (QBE.LSubWord QBE.UnsignedHalf, [_, _]) ->
 97          Just (BitVector (SMT.zeroExtend 16 concated) (QBE.Base QBE.Word))
 98        (QBE.LBase QBE.Word, [_, _, _, _]) ->
 99          Just (BitVector concated (QBE.Base QBE.Word))
100        (QBE.LBase QBE.Long, [_, _, _, _, _, _, _, _]) ->
101          Just (BitVector concated (QBE.Base QBE.Long))
102        (QBE.LBase QBE.Single, [_, _, _, _]) ->
103          error "float loading not implemented"
104        (QBE.LBase QBE.Double, [_, _, _, _, _, _, _, _]) ->
105          error "double loading not implemented"
106        _ -> Nothing
107    where
108      concated :: SMT.SExpr
109      concated = foldl concatBV s xs
110
111      concatBV :: SMT.SExpr -> BitVector -> SMT.SExpr
112      concatBV acc byte =
113        assert (qtype byte == QBE.Byte) $
114          F.concatExpr (sexpr byte) acc
115
116------------------------------------------------------------------------
117
118binaryOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector
119binaryOp op lhs@(BitVector {sexpr = slhs}) rhs@(BitVector {sexpr = srhs})
120  | qtype lhs == qtype rhs = Just $ lhs {sexpr = slhs `op` srhs}
121  | otherwise = Nothing
122
123-- TODO: Move this into the expression abstraction.
124toShiftAmount :: Word64 -> BitVector -> Maybe BitVector
125toShiftAmount bitSize amount = amount `E.urem` E.fromLit QBE.Word bitSize
126
127shiftOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector
128shiftOp op value amount@BitVector {qtype = QBE.Base QBE.Word} =
129  case qtype value of
130    QBE.Base QBE.Word -> toShiftAmount 32 amount >>= binaryOp op value
131    QBE.Base QBE.Long -> do
132      shiftAmount <- toShiftAmount 64 amount
133      E.wordToLong QBE.SLUnsignedWord shiftAmount >>= binaryOp op value
134    _ -> Nothing
135shiftOp _ _ _ = Nothing -- Shift amount must always be a Word.
136
137binaryBoolOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector
138binaryBoolOp op lhs rhs = do
139  bv <- binaryOp op lhs rhs
140  -- TODO: Can we get rid of the ITE somehow?
141  return $ fromSExpr QBE.Long (SMT.ite (toSExpr bv) trueValue falseValue)
142  where
143    -- TODO: Declare these as constants.
144    trueValue :: SMT.SExpr
145    trueValue = toSExpr $ E.fromLit QBE.Long 1
146
147    falseValue :: SMT.SExpr
148    falseValue = toSExpr $ E.fromLit QBE.Long 0
149
150-- TODO: If we Change E.ValueRepr to operate in 'Exec' then we can do IO stuff here.
151instance E.ValueRepr BitVector where
152  fromLit ty n =
153    let exty = QBE.Base ty
154        size = fromIntegral $ QBE.extTypeBitSize exty
155     in BitVector (SMT.bvBin size $ fromIntegral n) exty
156
157  fromFloat = error "symbolic floats currently unsupported"
158  fromDouble = error "symbolic doubles currently unsupported"
159
160  -- XXX: This only works for constants values, but this is fine since we implement
161  -- concolic execution and can obtain the address from the concrete value part.
162  toWord64 value =
163    case SMT.sexprToVal (sexpr value) of
164      SMT.Bits _ n -> fromIntegral n
165      _ -> error "unrechable"
166
167  wordToLong (QBE.SLSubWord QBE.SignedByte) (BitVector {sexpr = s, qtype = QBE.Base QBE.Word}) =
168    Just $ BitVector (SMT.signExtend 56 (F.extractExpr s 0 8)) (QBE.Base QBE.Long)
169  wordToLong (QBE.SLSubWord QBE.UnsignedByte) (BitVector {sexpr = s, qtype = QBE.Base QBE.Word}) =
170    Just $ BitVector (SMT.zeroExtend 56 (F.extractExpr s 0 8)) (QBE.Base QBE.Long)
171  wordToLong (QBE.SLSubWord QBE.SignedHalf) (BitVector {sexpr = s, qtype = QBE.Base QBE.Word}) =
172    Just $ BitVector (SMT.signExtend 48 (F.extractExpr s 0 16)) (QBE.Base QBE.Long)
173  wordToLong (QBE.SLSubWord QBE.UnsignedHalf) (BitVector {sexpr = s, qtype = QBE.Base QBE.Word}) =
174    Just $ BitVector (SMT.zeroExtend 48 (F.extractExpr s 0 16)) (QBE.Base QBE.Long)
175  wordToLong QBE.SLSignedWord (BitVector {sexpr = s, qtype = QBE.Base QBE.Word}) =
176    Just $ BitVector (SMT.signExtend 32 s) (QBE.Base QBE.Long)
177  wordToLong QBE.SLUnsignedWord (BitVector {sexpr = s, qtype = QBE.Base QBE.Word}) =
178    Just $ BitVector (SMT.zeroExtend 32 s) (QBE.Base QBE.Long)
179  wordToLong _ _ = Nothing
180
181  subType QBE.Word v@(BitVector {qtype = QBE.Base QBE.Word}) = Just v
182  subType QBE.Word (BitVector {qtype = QBE.Base QBE.Long, sexpr = s}) =
183    Just $ BitVector (F.extractExpr s 0 32) (QBE.Base QBE.Word)
184  subType QBE.Long v@(BitVector {qtype = QBE.Base QBE.Long}) = Just v
185  subType QBE.Single v@(BitVector {qtype = QBE.Base QBE.Single}) = Just v
186  subType QBE.Double v@(BitVector {qtype = QBE.Base QBE.Double}) = Just v
187  subType _ _ = Nothing
188
189  add = binaryOp SMT.bvAdd
190  sub = binaryOp SMT.bvSub
191  mul = binaryOp SMT.bvMul
192  div = binaryOp SMT.bvSDiv
193  or = binaryOp SMT.bvOr
194  xor = binaryOp SMT.bvXOr
195  and = binaryOp SMT.bvAnd
196  urem = binaryOp SMT.bvURem
197  srem = binaryOp SMT.bvSRem
198  udiv = binaryOp SMT.bvUDiv
199
200  neg value = value {sexpr = SMT.bvNeg $ sexpr value}
201
202  sar = shiftOp SMT.bvAShr
203  shr = shiftOp SMT.bvLShr
204  shl = shiftOp SMT.bvShl
205
206  eq = binaryBoolOp F.eqExpr
207  ne = binaryBoolOp (\lhs rhs -> F.notExpr $ F.eqExpr lhs rhs)
208  sle = binaryBoolOp SMT.bvSLeq
209  slt = binaryBoolOp SMT.bvSLt
210  sge = binaryBoolOp (flip SMT.bvSLeq)
211  sgt = binaryBoolOp (flip SMT.bvSLt)
212  ule = binaryBoolOp SMT.bvULeq
213  ult = binaryBoolOp SMT.bvULt
214  uge = binaryBoolOp (\lhs rhs -> SMT.or (SMT.bvULt rhs lhs) (F.eqExpr lhs rhs))
215  ugt = binaryBoolOp (flip SMT.bvULt)