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  getType Concolic {concrete = c} = E.getType c
 93
 94  extend ty s = unaryOp (E.extend ty s) (E.extend ty s)
 95  extract ty = unaryOp (E.extract ty) (E.extract ty)
 96
 97  -- TODO: Add constraint which enforces concrete value on
 98  -- symbolic part instead of silently discarding it. See
 99  -- the address concretization implementation for details.
100  floatToInt ty s Concolic {concrete = c} =
101    (`Concolic` Nothing) <$> E.floatToInt ty s c
102  intToFloat ty s Concolic {concrete = c} =
103    (`Concolic` Nothing) <$> E.intToFloat ty s c
104  extendFloat Concolic {concrete = c} =
105    (`Concolic` Nothing) <$> E.extendFloat c
106  truncFloat Concolic {concrete = c} =
107    (`Concolic` Nothing) <$> E.truncFloat c
108
109  add = binaryOp E.add E.add
110  sub = binaryOp E.sub E.sub
111  mul = binaryOp E.mul E.mul
112  div = binaryOp E.div E.div
113  or = binaryOp E.or E.or
114  xor = binaryOp E.xor E.xor
115  and = binaryOp E.and E.and
116  urem = binaryOp E.urem E.urem
117  srem = binaryOp E.srem E.srem
118  udiv = binaryOp E.udiv E.udiv
119
120  neg = unaryOp E.neg E.neg
121
122  sar = binaryOp E.sar E.sar
123  shr = binaryOp E.shr E.shr
124  shl = binaryOp E.shl E.shl
125
126  eq = binaryOp E.eq E.eq
127  ne = binaryOp E.ne E.ne
128  sle = binaryOp E.sle E.sle
129  slt = binaryOp E.slt E.slt
130  sge = binaryOp E.sge E.sge
131  sgt = binaryOp E.sgt E.sgt
132  ule = binaryOp E.ule E.ule
133  ult = binaryOp E.ult E.ult
134  uge = binaryOp E.uge E.uge
135  ugt = binaryOp E.ugt E.ugt
136
137  -- TODO: Add constraint which enforces concrete value on
138  -- symbolic part instead of silently discarding it. See
139  -- the address concretization implementation for details.
140  ord lhs rhs = (`Concolic` Nothing) <$> E.ord (concrete lhs) (concrete rhs)