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 Language.QBE.Simulator.Default.Expression qualified as D
 15import Language.QBE.Simulator.Expression qualified as E
 16import Language.QBE.Simulator.Symbolic.Expression qualified as SE
 17import Language.QBE.Simulator.Symbolic.Tracer (ExecTrace, appendBranch, newBranch)
 18import Language.QBE.Simulator.Tracer (Tracer (..))
 19
 20data Concolic
 21  = Concolic
 22  { concrete :: D.RegVal,
 23    symbolic :: Maybe SE.BitVector
 24  }
 25  deriving (Show)
 26
 27hasSymbolic :: Concolic -> Bool
 28hasSymbolic Concolic {symbolic = Just _} = True
 29hasSymbolic _ = False
 30
 31getSymbolicDef :: Concolic -> SE.BitVector
 32getSymbolicDef Concolic {concrete = c, symbolic = s} =
 33  fromMaybe (SE.fromReg c) s
 34
 35------------------------------------------------------------------------
 36
 37instance E.Storable Concolic where
 38  toBytes Concolic {concrete = c, symbolic = s} =
 39    let cbytes = E.toBytes c
 40        nbytes = length cbytes
 41        sbytes = maybe (replicate nbytes Nothing) (map Just . E.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 <- E.fromBytes ty conBytes
 49
 50      let mkConcolic = Concolic con
 51      if any hasSymbolic bytes
 52        then do
 53          let symBVs = map getSymbolicDef bytes
 54          E.fromBytes ty symBVs <&> mkConcolic . Just
 55        else Just $ mkConcolic Nothing
 56
 57instance Tracer ExecTrace Concolic where
 58  branch t Concolic {symbolic = Just s} condResult =
 59    appendBranch t condResult (newBranch s)
 60  branch t _ _ = t
 61
 62------------------------------------------------------------------------
 63
 64unaryOp ::
 65  (D.RegVal -> Maybe D.RegVal) ->
 66  (SE.BitVector -> Maybe SE.BitVector) ->
 67  Concolic ->
 68  Maybe Concolic
 69unaryOp fnCon fnSym Concolic {concrete = c, symbolic = s} = do
 70  c' <- fnCon c
 71  let con = Concolic c'
 72  case s of
 73    Just s' -> fnSym s' <&> con . Just
 74    Nothing -> pure $ con Nothing
 75
 76binaryOp ::
 77  (D.RegVal -> D.RegVal -> Maybe D.RegVal) ->
 78  (SE.BitVector -> SE.BitVector -> Maybe SE.BitVector) ->
 79  Concolic ->
 80  Concolic ->
 81  Maybe Concolic
 82binaryOp fnCon fnSym lhs rhs =
 83  do
 84    c <- concrete lhs `fnCon` concrete rhs
 85    if hasSymbolic lhs || hasSymbolic rhs
 86      then
 87        let lhsS = getSymbolicDef lhs
 88            rhsS = getSymbolicDef rhs
 89         in (lhsS `fnSym` rhsS) <&> Concolic c . Just
 90      else pure $ Concolic c Nothing
 91
 92instance E.ValueRepr Concolic where
 93  fromLit ty v = Concolic (E.fromLit ty v) Nothing
 94  fromFloat fl = Concolic (E.fromFloat fl) Nothing
 95  fromDouble d = Concolic (E.fromDouble d) Nothing
 96
 97  fromAddress addr = Concolic (E.fromAddress addr) Nothing
 98  toAddress Concolic {concrete = c} = E.toAddress c
 99  isZero Concolic {concrete = c} = E.isZero c
100
101  add = binaryOp E.add E.add
102  sub = binaryOp E.sub E.sub
103
104  extend ty = unaryOp (E.extend ty) (E.extend ty)
105  subType ty = unaryOp (E.subType ty) (E.subType ty)