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
 92  fromAddress addr = Concolic (E.fromAddress addr) Nothing
 93  toAddress Concolic {concrete = c} = E.toAddress c
 94  isZero Concolic {concrete = c} = E.isZero c
 95
 96  add = binaryOp E.add E.add
 97  sub = binaryOp E.sub E.sub
 98  mul = binaryOp E.mul E.mul
 99  or = binaryOp E.or E.or
100  xor = binaryOp E.xor E.xor
101  and = binaryOp E.and E.and
102  urem = binaryOp E.urem E.urem
103  srem = binaryOp E.srem E.srem
104  udiv = binaryOp E.udiv E.udiv
105
106  eq = binaryOp E.eq E.eq
107  ne = binaryOp E.ne E.ne
108  sle = binaryOp E.sle E.sle
109  slt = binaryOp E.slt E.slt
110  sge = binaryOp E.sge E.sge
111  sgt = binaryOp E.sgt E.sgt
112  ule = binaryOp E.ule E.ule
113  ult = binaryOp E.ult E.ult
114  uge = binaryOp E.uge E.uge
115  ugt = binaryOp E.ugt E.ugt
116
117  wordToLong ty = unaryOp (E.wordToLong ty) (E.wordToLong ty)
118  subType ty = unaryOp (E.subType ty) (E.subType ty)