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.Concolic.Expression
  6  ( Concolic (..),
  7    hasSymbolic,
  8  )
  9where
 10
 11import Control.Exception (assert)
 12import Data.Functor ((<&>))
 13import Data.Maybe (fromMaybe)
 14import Data.Word (Word8)
 15import Language.QBE.Simulator.Default.Expression qualified as D
 16import Language.QBE.Simulator.Expression qualified as E
 17import Language.QBE.Simulator.Memory qualified as MEM
 18import Language.QBE.Simulator.Symbolic.Expression qualified as SE
 19
 20data Concolic v
 21  = Concolic
 22  { concrete :: v,
 23    symbolic :: Maybe SE.BitVector
 24  }
 25  deriving (Show)
 26
 27hasSymbolic :: Concolic v -> Bool
 28hasSymbolic Concolic {symbolic = Just _} = True
 29hasSymbolic _ = False
 30
 31getSymbolicDef :: (v -> SE.BitVector) -> Concolic v -> SE.BitVector
 32getSymbolicDef conc Concolic {concrete = c, symbolic = s} =
 33  fromMaybe (conc c) s
 34
 35------------------------------------------------------------------------
 36
 37instance MEM.Storable (Concolic D.RegVal) (Concolic Word8) where
 38  toBytes Concolic {concrete = c, symbolic = s} =
 39    let cbytes = MEM.toBytes c
 40        nbytes = length cbytes
 41        sbytes = maybe (replicate nbytes Nothing) (map Just . MEM.toBytes) s
 42     in assert (nbytes == length sbytes) $
 43          zipWith Concolic cbytes sbytes
 44
 45  fromBytes ty bytes =
 46    do
 47      let conBytes = map concrete bytes
 48      con <- MEM.fromBytes ty conBytes
 49
 50      let mkConcolic = Concolic con
 51      if any hasSymbolic bytes
 52        then do
 53          let symBVs = map (getSymbolicDef SE.fromByte) bytes
 54          MEM.fromBytes ty symBVs <&> mkConcolic . Just
 55        else Just $ mkConcolic Nothing
 56
 57------------------------------------------------------------------------
 58
 59unaryOp ::
 60  (D.RegVal -> Maybe D.RegVal) ->
 61  (SE.BitVector -> Maybe SE.BitVector) ->
 62  Concolic D.RegVal ->
 63  Maybe (Concolic D.RegVal)
 64unaryOp fnCon fnSym Concolic {concrete = c, symbolic = s} = do
 65  c' <- fnCon c
 66  let con = Concolic c'
 67  case s of
 68    Just s' -> fnSym s' <&> con . Just
 69    Nothing -> pure $ con Nothing
 70
 71binaryOp ::
 72  (D.RegVal -> D.RegVal -> Maybe D.RegVal) ->
 73  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->
 74  Concolic D.RegVal ->
 75  Concolic D.RegVal ->
 76  Maybe (Concolic D.RegVal)
 77binaryOp fnCon fnSym lhs rhs =
 78  do
 79    c <- concrete lhs `fnCon` concrete rhs
 80    if hasSymbolic lhs || hasSymbolic rhs
 81      then
 82        let lhsS = getSymbolicDef SE.fromReg lhs
 83            rhsS = getSymbolicDef SE.fromReg rhs
 84         in (lhsS `fnSym` rhsS) <&> Concolic c . Just
 85      else pure $ Concolic c Nothing
 86
 87instance E.ValueRepr (Concolic D.RegVal) where
 88  fromLit ty v = Concolic (E.fromLit ty v) Nothing
 89  fromFloat fl = Concolic (E.fromFloat fl) Nothing
 90  fromDouble d = Concolic (E.fromDouble d) Nothing
 91  toWord64 Concolic {concrete = c} = E.toWord64 c
 92
 93  add = binaryOp E.add E.add
 94  sub = binaryOp E.sub E.sub
 95  mul = binaryOp E.mul E.mul
 96  div = binaryOp E.div E.div
 97  or = binaryOp E.or E.or
 98  xor = binaryOp E.xor E.xor
 99  and = binaryOp E.and E.and
100  urem = binaryOp E.urem E.urem
101  srem = binaryOp E.srem E.srem
102  udiv = binaryOp E.udiv E.udiv
103
104  neg = unaryOp E.neg E.neg
105
106  sar = binaryOp E.sar E.sar
107  shr = binaryOp E.shr E.shr
108  shl = binaryOp E.shl E.shl
109
110  eq = binaryOp E.eq E.eq
111  ne = binaryOp E.ne E.ne
112  sle = binaryOp E.sle E.sle
113  slt = binaryOp E.slt E.slt
114  sge = binaryOp E.sge E.sge
115  sgt = binaryOp E.sgt E.sgt
116  ule = binaryOp E.ule E.ule
117  ult = binaryOp E.ult E.ult
118  uge = binaryOp E.uge E.uge
119  ugt = binaryOp E.ugt E.ugt
120
121  wordToLong ty = unaryOp (E.wordToLong ty) (E.wordToLong ty)
122  subType ty = unaryOp (E.subType ty) (E.subType ty)