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.DeepSeq (NFData, NFData1)
 12import Control.Exception (assert)
 13import Data.Functor ((<&>))
 14import Data.Maybe (fromMaybe)
 15import Data.Word (Word8)
 16import GHC.Generics (Generic, Generic1)
 17import Language.QBE.Simulator.Default.Expression qualified as D
 18import Language.QBE.Simulator.Expression qualified as E
 19import Language.QBE.Simulator.Memory qualified as MEM
 20import Language.QBE.Simulator.Symbolic.Expression qualified as SE
 21
 22data Concolic v
 23  = Concolic
 24  { concrete :: v,
 25    symbolic :: Maybe SE.BitVector
 26  }
 27  deriving (Show, Generic, Generic1)
 28
 29instance (NFData a) => NFData (Concolic a)
 30
 31instance NFData1 Concolic
 32
 33hasSymbolic :: Concolic v -> Bool
 34hasSymbolic Concolic {symbolic = Just _} = True
 35hasSymbolic _ = False
 36
 37getSymbolicDef :: (v -> SE.BitVector) -> Concolic v -> SE.BitVector
 38getSymbolicDef conc Concolic {concrete = c, symbolic = s} =
 39  fromMaybe (conc c) s
 40
 41------------------------------------------------------------------------
 42
 43instance MEM.Storable (Concolic D.RegVal) (Concolic Word8) where
 44  toBytes Concolic {concrete = c, symbolic = s} =
 45    let cbytes = MEM.toBytes c
 46        nbytes = length cbytes
 47        sbytes = maybe (replicate nbytes Nothing) (map Just . MEM.toBytes) s
 48     in assert (nbytes == length sbytes) $
 49          zipWith Concolic cbytes sbytes
 50
 51  fromBytes ty bytes =
 52    do
 53      let conBytes = map concrete bytes
 54      con <- MEM.fromBytes ty conBytes
 55
 56      let mkConcolic = Concolic con
 57      if any hasSymbolic bytes
 58        then do
 59          let symBVs = map (getSymbolicDef SE.fromByte) bytes
 60          MEM.fromBytes ty symBVs <&> mkConcolic . Just
 61        else Just $ mkConcolic Nothing
 62
 63------------------------------------------------------------------------
 64
 65unaryOp ::
 66  (D.RegVal -> Maybe D.RegVal) ->
 67  (SE.BitVector -> Maybe SE.BitVector) ->
 68  Concolic D.RegVal ->
 69  Maybe (Concolic D.RegVal)
 70unaryOp fnCon fnSym Concolic {concrete = c, symbolic = s} = do
 71  c' <- fnCon c
 72  let con = Concolic c'
 73  case s of
 74    Just s' -> fnSym s' <&> con . Just
 75    Nothing -> pure $ con Nothing
 76
 77binaryOp ::
 78  (D.RegVal -> D.RegVal -> Maybe D.RegVal) ->
 79  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->
 80  Concolic D.RegVal ->
 81  Concolic D.RegVal ->
 82  Maybe (Concolic D.RegVal)
 83binaryOp fnCon fnSym lhs rhs =
 84  do
 85    c <- concrete lhs `fnCon` concrete rhs
 86    if hasSymbolic lhs || hasSymbolic rhs
 87      then
 88        let lhsS = getSymbolicDef SE.fromReg lhs
 89            rhsS = getSymbolicDef SE.fromReg rhs
 90         in (lhsS `fnSym` rhsS) <&> Concolic c . Just
 91      else pure $ Concolic c Nothing
 92
 93instance E.ValueRepr (Concolic D.RegVal) where
 94  fromLit ty v = Concolic (E.fromLit ty v) Nothing
 95  fromFloat fl = Concolic (E.fromFloat fl) Nothing
 96  fromDouble d = Concolic (E.fromDouble d) Nothing
 97  toWord64 Concolic {concrete = c} = E.toWord64 c
 98  getType Concolic {concrete = c} = E.getType c
 99
100  extend ty s = unaryOp (E.extend ty s) (E.extend ty s)
101  extract ty = unaryOp (E.extract ty) (E.extract ty)
102
103  -- TODO: Add constraint which enforces concrete value on
104  -- symbolic part instead of silently discarding it. See
105  -- the address concretization implementation for details.
106  floatToInt ty s Concolic {concrete = c} =
107    (`Concolic` Nothing) <$> E.floatToInt ty s c
108  intToFloat ty s Concolic {concrete = c} =
109    (`Concolic` Nothing) <$> E.intToFloat ty s c
110  extendFloat Concolic {concrete = c} =
111    (`Concolic` Nothing) <$> E.extendFloat c
112  truncFloat Concolic {concrete = c} =
113    (`Concolic` Nothing) <$> E.truncFloat c
114
115  add = binaryOp E.add E.add
116  sub = binaryOp E.sub E.sub
117  mul = binaryOp E.mul E.mul
118  div = binaryOp E.div E.div
119  or = binaryOp E.or E.or
120  xor = binaryOp E.xor E.xor
121  and = binaryOp E.and E.and
122  urem = binaryOp E.urem E.urem
123  srem = binaryOp E.srem E.srem
124  udiv = binaryOp E.udiv E.udiv
125
126  neg = unaryOp E.neg E.neg
127
128  sar = binaryOp E.sar E.sar
129  shr = binaryOp E.shr E.shr
130  shl = binaryOp E.shl E.shl
131
132  eq = binaryOp E.eq E.eq
133  ne = binaryOp E.ne E.ne
134  sle = binaryOp E.sle E.sle
135  slt = binaryOp E.slt E.slt
136  sge = binaryOp E.sge E.sge
137  sgt = binaryOp E.sgt E.sgt
138  ule = binaryOp E.ule E.ule
139  ult = binaryOp E.ult E.ult
140  uge = binaryOp E.uge E.uge
141  ugt = binaryOp E.ugt E.ugt
142
143  -- TODO: Add constraint which enforces concrete value on
144  -- symbolic part instead of silently discarding it. See
145  -- the address concretization implementation for details.
146  ord lhs rhs = (`Concolic` Nothing) <$> E.ord (concrete lhs) (concrete rhs)