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    fromReg,
  8    fromSExpr,
  9    toSExpr,
 10    symbolic,
 11    toCond,
 12  )
 13where
 14
 15import Control.Exception (assert)
 16import Language.QBE.Simulator.Default.Expression qualified as D
 17import Language.QBE.Simulator.Expression qualified as E
 18import Language.QBE.Types qualified as QBE
 19import SimpleSMT qualified as SMT
 20
 21data BitVector
 22  = BitVector
 23  { sexpr :: SMT.SExpr,
 24    qtype :: QBE.ExtType
 25  }
 26  deriving (Show, Eq)
 27
 28fromReg :: D.RegVal -> BitVector
 29fromReg (D.VByte v) = BitVector (SMT.bvBin 8 $ fromIntegral v) QBE.Byte
 30fromReg (D.VHalf v) = BitVector (SMT.bvBin 16 $ fromIntegral v) QBE.HalfWord
 31fromReg (D.VWord v) = BitVector (SMT.bvBin 32 $ fromIntegral v) (QBE.Base QBE.Word)
 32fromReg (D.VLong v) = BitVector (SMT.bvBin 64 $ fromIntegral v) (QBE.Base QBE.Long)
 33fromReg (D.VSingle _) = error "symbolic floats not supported"
 34fromReg (D.VDouble _) = error "symbolic doubles not supported"
 35
 36fromSExpr :: QBE.BaseType -> SMT.SExpr -> BitVector
 37fromSExpr ty sexpr = BitVector sexpr (QBE.Base ty)
 38
 39toSExpr :: BitVector -> SMT.SExpr
 40toSExpr = sexpr
 41
 42symbolic :: SMT.Solver -> String -> QBE.BaseType -> IO BitVector
 43symbolic solver name ty = do
 44  let bits = SMT.tBits $ fromIntegral (QBE.baseTypeBitSize ty)
 45  sym <- SMT.declare solver name bits
 46  return $ BitVector sym (QBE.Base ty)
 47
 48-- In the QBE a condition (see `jnz`) is true if the Word value is not zero.
 49toCond :: Bool -> BitVector -> SMT.SExpr
 50toCond isTrue BitVector {sexpr = s, qtype = ty} =
 51  -- Equality is only defined for Words.
 52  assert (ty == QBE.Base QBE.Word) $
 53    let zeroSExpr = sexpr (fromReg $ E.fromLit QBE.Word 0)
 54     in toCond' s zeroSExpr
 55  where
 56    toCond' lhs rhs
 57      | isTrue = SMT.not (SMT.eq lhs rhs) -- /= 0
 58      | otherwise = SMT.eq lhs rhs -- == 0
 59
 60------------------------------------------------------------------------
 61
 62instance E.Storable BitVector where
 63  toBytes BitVector {sexpr = s, qtype = ty} =
 64    assert (size `mod` 8 == 0) $
 65      map (\n -> BitVector (nthByte s n) QBE.Byte) [1 .. size `div` 8]
 66    where
 67      size :: Integer
 68      size = fromIntegral $ QBE.extTypeBitSize ty
 69
 70      nthByte :: SMT.SExpr -> Integer -> SMT.SExpr
 71      nthByte expr n = SMT.extract expr ((n * 8) - 1) ((n - 1) * 8)
 72
 73  fromBytes _ [] = Nothing
 74  fromBytes ty bytes@(BitVector {sexpr = s} : xs) =
 75    if length bytes /= QBE.extTypeByteSize ty
 76      then Nothing
 77      else Just $ BitVector (foldl concatBV s xs) ty
 78    where
 79      concatBV :: SMT.SExpr -> BitVector -> SMT.SExpr
 80      concatBV acc byte =
 81        assert (qtype byte == QBE.Byte) $
 82          SMT.concat (sexpr byte) acc
 83
 84------------------------------------------------------------------------
 85
 86binaryOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector
 87binaryOp op lhs@(BitVector {sexpr = slhs}) rhs@(BitVector {sexpr = srhs})
 88  | qtype lhs == qtype rhs = Just $ lhs {sexpr = slhs `op` srhs}
 89  | otherwise = Nothing
 90
 91-- TODO: If we Change E.ValueRepr to operate in 'Exec' then we can do IO stuff here.
 92instance E.ValueRepr BitVector where
 93  fromLit ty n =
 94    let exty = QBE.Base ty
 95        size = fromIntegral $ QBE.extTypeBitSize exty
 96     in BitVector (SMT.bvBin size $ fromIntegral n) exty
 97
 98  fromFloat = error "symbolic floats currently unsupported"
 99  fromDouble = error "symbolic doubles currently unsupported"
100
101  -- XXX: This only works for constants values, but this is fine since we implement
102  -- concolic execution and can obtain the address from the concrete value part.
103  toAddress addr =
104    case SMT.sexprToVal (sexpr addr) of
105      -- TODO: Don't hardcode address type
106      SMT.Bits 64 n -> Just $ fromIntegral n
107      _ -> Nothing
108  fromAddress addr = fromReg (E.fromLit QBE.Long addr)
109
110  -- TODO: Don't hardcode bitsizes here
111  -- TODO: refactor (just need to select sign/zero extend)
112  extend QBE.SignedByte (BitVector {sexpr = s, qtype = QBE.Byte}) =
113    Just $ BitVector (SMT.signExtend 56 s) (QBE.Base QBE.Long)
114  extend QBE.UnsignedByte (BitVector {sexpr = s, qtype = QBE.Byte}) =
115    Just $ BitVector (SMT.zeroExtend 56 s) (QBE.Base QBE.Long)
116  extend QBE.SignedHalf (BitVector {sexpr = s, qtype = QBE.HalfWord}) =
117    Just $ BitVector (SMT.signExtend 48 s) (QBE.Base QBE.Long)
118  extend QBE.UnsignedHalf (BitVector {sexpr = s, qtype = QBE.HalfWord}) =
119    Just $ BitVector (SMT.zeroExtend 48 s) (QBE.Base QBE.Long)
120  extend _ _ = Nothing
121
122  subType QBE.Word v@(BitVector {qtype = QBE.Base QBE.Word}) = Just v
123  subType QBE.Word (BitVector {qtype = QBE.Base QBE.Long, sexpr = s}) =
124    Just $ BitVector (SMT.extract s 31 0) (QBE.Base QBE.Word)
125  subType QBE.Long v@(BitVector {qtype = QBE.Base QBE.Long}) = Just v
126  subType QBE.Single v@(BitVector {qtype = QBE.Base QBE.Single}) = Just v
127  subType QBE.Double v@(BitVector {qtype = QBE.Base QBE.Double}) = Just v
128  subType _ _ = Nothing
129
130  -- XXX: This only works for constants values, but this is fine (see above).
131  isZero bv =
132    case SMT.sexprToVal (sexpr bv) of
133      SMT.Bits _ v -> v == 0
134      _ -> error "unreachable"
135
136  add = binaryOp SMT.bvAdd
137  sub = binaryOp SMT.bvSub