quebex

  1-- SPDX-FileCopyrightText: 2024 University of Bremen
  2-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
  3--
  4-- SPDX-License-Identifier: MIT AND GPL-3.0-only
  5
  6module Language.QBE.Backend.Tracer
  7  ( Branch (Branch),
  8    newBranch,
  9    fromBranch,
 10    ExecTrace,
 11    newExecTrace,
 12    toSExprs,
 13    appendBranch,
 14    appendCons,
 15    solveTrace,
 16  )
 17where
 18
 19import Control.Exception (throwIO)
 20import Control.Monad (when)
 21import Language.QBE.Backend (SolverError (UnknownResult), prefixLength)
 22import Language.QBE.Backend.Model qualified as Model
 23import Language.QBE.Simulator.Symbolic.Expression qualified as SE
 24import SimpleBV qualified as SMT
 25
 26-- Represents a branch condition in the executed code
 27data Branch
 28  = Branch
 29      Bool -- Whether negation of the branch was attempted
 30      SE.BitVector -- The symbolic branch condition
 31  deriving (Show, Eq)
 32
 33-- Create a new branch condition.
 34newBranch :: SE.BitVector -> Branch
 35newBranch = Branch False
 36
 37-- Create a new branch from an existing branch, thereby updating its metadata.
 38-- It is assumed that the condition, encoded in the branches, is equal.
 39fromBranch :: Branch -> Branch -> Branch
 40fromBranch (Branch wasNeg' _) (Branch wasNeg ast) =
 41  Branch (wasNeg || wasNeg') ast
 42
 43------------------------------------------------------------------------
 44
 45-- Represents a single execution through a program, tracking for each
 46-- symbolic branch condition if it was 'True' or 'False'.
 47type ExecTrace = [(Bool, Branch)]
 48
 49-- Create a new empty execution tree.
 50newExecTrace :: ExecTrace
 51newExecTrace = []
 52
 53-- Return all branch conditions of an 'ExecTrace'.
 54toSExprs :: ExecTrace -> [SMT.SExpr]
 55toSExprs = map (\(_, Branch _ bv) -> SE.toSExpr bv)
 56
 57-- Append a branch to the execution trace, denoting via a 'Bool'
 58-- if the branch was taken or if it was not taken.
 59appendBranch :: ExecTrace -> Bool -> Branch -> ExecTrace
 60appendBranch trace wasTrue branch = trace ++ [(wasTrue, branch)]
 61
 62-- Append a constraint to the execution tree. This constraint must
 63-- be true and, contrary to appendBranch, negation will not be
 64-- attempted for it.
 65appendCons :: ExecTrace -> SE.BitVector -> ExecTrace
 66appendCons trace cons = trace ++ [(True, Branch True cons)]
 67
 68-- For a given execution trace, return an assignment (represented
 69-- as a 'Model') which statisfies all symbolic branch conditions.
 70-- If such an assignment does not exist, then 'Nothing' is returned.
 71--
 72-- Throws a 'SolverError' on an unknown solver result (e.g., on timeout).
 73solveTrace :: SMT.Solver -> [SMT.SExpr] -> ExecTrace -> ExecTrace -> IO (Maybe Model.Model)
 74solveTrace solver inputVars oldTrace newTrace = do
 75  -- Determine the common prefix of the current trace and the old trace
 76  -- drop constraints beyond this common prefix from the current solver
 77  -- context. Thereby, keeping the common prefix and making use of
 78  -- incremental solving capabilities.
 79  let prefix = prefixLength newTrace oldTrace
 80  let toDrop = length oldTrace - prefix
 81
 82  -- Micro optimization: When we don't have anything to drop, then
 83  -- don't call .popMany thereby avoiding communication with the solver.
 84  when (toDrop /= 0) $
 85    SMT.popMany solver (fromIntegral toDrop)
 86
 87  -- Only enforce new constraints, i.e. those beyond the common prefix.
 88  assertTrace (drop prefix newTrace)
 89
 90  isSat <- SMT.check solver
 91  case isSat of
 92    SMT.Sat -> Just <$> Model.getModel solver inputVars
 93    SMT.Unsat -> pure Nothing
 94    SMT.Unknown -> throwIO UnknownResult
 95  where
 96    -- Add all conditions enforced by the given 'ExecTrace' to the solver.
 97    -- Returns a list of all asserted conditions.
 98    assertTrace :: ExecTrace -> IO ()
 99    assertTrace [] = pure ()
100    assertTrace t = do
101      let conds = map (\(b, Branch _ c) -> SE.toCond b c) t
102      mapM_ (\c -> SMT.push solver >> SMT.assert solver c) conds