1-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>2--3-- SPDX-License-Identifier: GPL-3.0-only45module Language.QBE.Simulator.Symbolic.Expression6 ( BitVector,7 fromByte,8 fromReg,9 fromSExpr,10 toSExpr,11 symbolic,12 toCond,13 )14where1516import Control.Exception (assert)17import Data.Word (Word8)18import Language.QBE.Simulator.Default.Expression qualified as D19import Language.QBE.Simulator.Expression qualified as E20import Language.QBE.Simulator.Memory qualified as MEM21import Language.QBE.Types qualified as QBE22import SimpleSMT qualified as SMT2324-- This types supports more than just the 'QBE.BaseType' to ease the25-- implementation of the 'MEM.Storable' type class. Essentially, this26-- data type just provides a generic BitVector abstraction on top of27-- 'SMT.SExpr'.28data BitVector29 = BitVector30 { sexpr :: SMT.SExpr,31 -- TODO: For BitVectors, we can extract the type from the SExpr.32 -- Technically, we don't need the 'ExtType' here and can just33 -- turn this into a newtype.34 qtype :: QBE.ExtType35 }36 deriving (Show, Eq)3738fromByte :: Word8 -> BitVector39fromByte byte = BitVector (SMT.bvBin 8 $ fromIntegral byte) QBE.Byte4041fromReg :: D.RegVal -> BitVector42fromReg (D.VWord v) = BitVector (SMT.bvBin 32 $ fromIntegral v) (QBE.Base QBE.Word)43fromReg (D.VLong v) = BitVector (SMT.bvBin 64 $ fromIntegral v) (QBE.Base QBE.Long)44fromReg (D.VSingle _) = error "symbolic floats not supported"45fromReg (D.VDouble _) = error "symbolic doubles not supported"4647fromSExpr :: QBE.BaseType -> SMT.SExpr -> BitVector48fromSExpr ty sexpr = BitVector sexpr (QBE.Base ty)4950toSExpr :: BitVector -> SMT.SExpr51toSExpr = sexpr5253symbolic :: SMT.Solver -> String -> QBE.BaseType -> IO BitVector54symbolic solver name ty = do55 let bits = SMT.tBits $ fromIntegral (QBE.baseTypeBitSize ty)56 sym <- SMT.declare solver name bits57 return $ BitVector sym (QBE.Base ty)5859-- In the QBE a condition (see `jnz`) is true if the Word value is not zero.60toCond :: Bool -> BitVector -> SMT.SExpr61toCond isTrue BitVector {sexpr = s, qtype = ty} =62 -- Equality is only defined for Words.63 assert (ty == QBE.Base QBE.Word) $64 let zeroSExpr = sexpr (fromReg $ E.fromLit QBE.Word 0)65 in toCond' s zeroSExpr66 where67 toCond' lhs rhs68 | isTrue = SMT.not (SMT.eq lhs rhs) -- /= 069 | otherwise = SMT.eq lhs rhs -- == 07071------------------------------------------------------------------------7273instance MEM.Storable BitVector BitVector where74 toBytes BitVector {sexpr = s, qtype = ty} =75 assert (size `mod` 8 == 0) $76 map (\n -> BitVector (nthByte s n) QBE.Byte) [1 .. size `div` 8]77 where78 size :: Integer79 size = fromIntegral $ QBE.extTypeBitSize ty8081 nthByte :: SMT.SExpr -> Integer -> SMT.SExpr82 nthByte expr n = SMT.extract expr ((n * 8) - 1) ((n - 1) * 8)8384 fromBytes _ [] = Nothing85 fromBytes ty bytes@(BitVector {sexpr = s} : xs) =86 if length bytes /= fromIntegral (QBE.loadByteSize ty)87 then Nothing88 else case (ty, bytes) of89 (QBE.LSubWord QBE.UnsignedByte, [_]) ->90 Just (BitVector (SMT.zeroExtend 24 concated) (QBE.Base QBE.Word))91 (QBE.LSubWord QBE.SignedByte, [_]) ->92 Just (BitVector (SMT.signExtend 24 concated) (QBE.Base QBE.Word))93 (QBE.LSubWord QBE.SignedHalf, [_, _]) ->94 Just (BitVector (SMT.signExtend 16 concated) (QBE.Base QBE.Word))95 (QBE.LSubWord QBE.UnsignedHalf, [_, _]) ->96 Just (BitVector (SMT.zeroExtend 16 concated) (QBE.Base QBE.Word))97 (QBE.LBase QBE.Word, [_, _, _, _]) ->98 Just (BitVector concated (QBE.Base QBE.Word))99 (QBE.LBase QBE.Long, [_, _, _, _, _, _, _, _]) ->100 Just (BitVector concated (QBE.Base QBE.Long))101 (QBE.LBase QBE.Single, [_, _, _, _]) ->102 error "float loading not implemented"103 (QBE.LBase QBE.Double, [_, _, _, _, _, _, _, _]) ->104 error "double loading not implemented"105 _ -> Nothing106 where107 concated :: SMT.SExpr108 concated = foldl concatBV s xs109110 concatBV :: SMT.SExpr -> BitVector -> SMT.SExpr111 concatBV acc byte =112 assert (qtype byte == QBE.Byte) $113 SMT.concat (sexpr byte) acc114115------------------------------------------------------------------------116117binaryOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector118binaryOp op lhs@(BitVector {sexpr = slhs}) rhs@(BitVector {sexpr = srhs})119 | qtype lhs == qtype rhs = Just $ lhs {sexpr = slhs `op` srhs}120 | otherwise = Nothing121122binaryBoolOp :: (SMT.SExpr -> SMT.SExpr -> SMT.SExpr) -> BitVector -> BitVector -> Maybe BitVector123binaryBoolOp op lhs rhs = do124 bv <- binaryOp op lhs rhs125 -- TODO: Can we get rid of the ITE somehow?126 return $ fromSExpr QBE.Long (SMT.ite (toSExpr bv) trueValue falseValue)127 where128 -- TODO: Declare these as constants.129 trueValue :: SMT.SExpr130 trueValue = toSExpr $ E.fromLit QBE.Long 1131132 falseValue :: SMT.SExpr133 falseValue = toSExpr $ E.fromLit QBE.Long 0134135-- TODO: If we Change E.ValueRepr to operate in 'Exec' then we can do IO stuff here.136instance E.ValueRepr BitVector where137 fromLit ty n =138 let exty = QBE.Base ty139 size = fromIntegral $ QBE.extTypeBitSize exty140 in BitVector (SMT.bvBin size $ fromIntegral n) exty141142 fromFloat = error "symbolic floats currently unsupported"143 fromDouble = error "symbolic doubles currently unsupported"144145 -- XXX: This only works for constants values, but this is fine since we implement146 -- concolic execution and can obtain the address from the concrete value part.147 toAddress addr =148 case SMT.sexprToVal (sexpr addr) of149 -- TODO: Don't hardcode address type150 SMT.Bits 64 n -> Just $ fromIntegral n151 _ -> Nothing152 fromAddress addr = fromReg (E.fromLit QBE.Long addr)153154 wordToLong (QBE.SLSubWord QBE.SignedByte) (BitVector {sexpr = s, qtype = QBE.Base QBE.Word}) =155 Just $ BitVector (SMT.signExtend 56 (SMT.extract s 7 0)) (QBE.Base QBE.Long)156 wordToLong (QBE.SLSubWord QBE.UnsignedByte) (BitVector {sexpr = s, qtype = QBE.Base QBE.Word}) =157 Just $ BitVector (SMT.zeroExtend 56 (SMT.extract s 7 0)) (QBE.Base QBE.Long)158 wordToLong (QBE.SLSubWord QBE.SignedHalf) (BitVector {sexpr = s, qtype = QBE.Base QBE.Word}) =159 Just $ BitVector (SMT.signExtend 48 (SMT.extract s 15 0)) (QBE.Base QBE.Long)160 wordToLong (QBE.SLSubWord QBE.UnsignedHalf) (BitVector {sexpr = s, qtype = QBE.Base QBE.Word}) =161 Just $ BitVector (SMT.zeroExtend 48 (SMT.extract s 15 0)) (QBE.Base QBE.Long)162 wordToLong QBE.SLSignedWord (BitVector {sexpr = s, qtype = QBE.Base QBE.Word}) =163 Just $ BitVector (SMT.signExtend 32 s) (QBE.Base QBE.Long)164 wordToLong QBE.SLUnsignedWord (BitVector {sexpr = s, qtype = QBE.Base QBE.Word}) =165 Just $ BitVector (SMT.zeroExtend 32 s) (QBE.Base QBE.Long)166 wordToLong _ _ = Nothing167168 subType QBE.Word v@(BitVector {qtype = QBE.Base QBE.Word}) = Just v169 subType QBE.Word (BitVector {qtype = QBE.Base QBE.Long, sexpr = s}) =170 Just $ BitVector (SMT.extract s 31 0) (QBE.Base QBE.Word)171 subType QBE.Long v@(BitVector {qtype = QBE.Base QBE.Long}) = Just v172 subType QBE.Single v@(BitVector {qtype = QBE.Base QBE.Single}) = Just v173 subType QBE.Double v@(BitVector {qtype = QBE.Base QBE.Double}) = Just v174 subType _ _ = Nothing175176 -- XXX: This only works for constants values, but this is fine (see above).177 isZero bv =178 case SMT.sexprToVal (sexpr bv) of179 SMT.Bits _ v -> v == 0180 _ -> error "unreachable"181182 add = binaryOp SMT.bvAdd183 sub = binaryOp SMT.bvSub184 mul = binaryOp SMT.bvMul185 or = binaryOp SMT.bvOr186 xor = binaryOp SMT.bvXOr187 and = binaryOp SMT.bvAnd188 urem = binaryOp SMT.bvURem189 srem = binaryOp SMT.bvSRem190 udiv = binaryOp SMT.bvUDiv191192 eq = binaryBoolOp SMT.eq193 ne = binaryBoolOp (\lhs rhs -> SMT.not $ SMT.eq lhs rhs)194 sle = binaryBoolOp SMT.bvSLeq195 slt = binaryBoolOp SMT.bvSLt196 sge = binaryBoolOp (\lhs rhs -> SMT.not $ SMT.bvSLt lhs rhs)197 sgt = binaryBoolOp (\lhs rhs -> SMT.not $ SMT.bvSLeq lhs rhs)198 ule = binaryBoolOp SMT.bvULeq199 ult = binaryBoolOp SMT.bvULt200 uge = binaryBoolOp (\lhs rhs -> SMT.not $ SMT.bvULt lhs rhs)201 ugt = binaryBoolOp (\lhs rhs -> SMT.not $ SMT.bvULeq lhs rhs)