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 Language.QBE.Backend (SolverError (UnknownResult), prefixLength)
21import Language.QBE.Backend.Model qualified as Model
22import Language.QBE.Simulator.Symbolic.Expression qualified as SE
23import SimpleSMT qualified as SMT
24
25-- Represents a branch condition in the executed code
26data Branch
27  = Branch
28      Bool -- Whether negation of the branch was attempted
29      SE.BitVector -- The symbolic branch condition
30  deriving (Show, Eq)
31
32-- Create a new branch condition.
33newBranch :: SE.BitVector -> Branch
34newBranch = Branch False
35
36-- Create a new branch from an existing branch, thereby updating its metadata.
37-- It is assumed that the condition, encoded in the branches, is equal.
38fromBranch :: Branch -> Branch -> Branch
39fromBranch (Branch wasNeg' _) (Branch wasNeg ast) =
40  Branch (wasNeg || wasNeg') ast
41
42------------------------------------------------------------------------
43
44-- Represents a single execution through a program, tracking for each
45-- symbolic branch condition if it was 'True' or 'False'.
46type ExecTrace = [(Bool, Branch)]
47
48-- Create a new empty execution tree.
49newExecTrace :: ExecTrace
50newExecTrace = []
51
52-- Return all branch conditions of an 'ExecTrace'.
53toSExprs :: ExecTrace -> [SMT.SExpr]
54toSExprs = map (\(_, Branch _ bv) -> SE.toSExpr bv)
55
56-- Append a branch to the execution trace, denoting via a 'Bool'
57-- if the branch was taken or if it was not taken.
58appendBranch :: ExecTrace -> Bool -> Branch -> ExecTrace
59appendBranch trace wasTrue branch = trace ++ [(wasTrue, branch)]
60
61-- Append a constraint to the execution tree. This constraint must
62-- be true and, contrary to appendBranch, negation will not be
63-- attempted for it.
64appendCons :: ExecTrace -> SE.BitVector -> ExecTrace
65appendCons trace cons = trace ++ [(True, Branch True cons)]
66
67-- For a given execution trace, return an assignment (represented
68-- as a 'Model') which statisfies all symbolic branch conditions.
69-- If such an assignment does not exist, then 'Nothing' is returned.
70--
71-- Throws a 'SolverError' on an unknown solver result (e.g., on timeout).
72solveTrace :: SMT.Solver -> [SMT.SExpr] -> ExecTrace -> ExecTrace -> IO (Maybe Model.Model)
73solveTrace solver inputVars oldTrace newTrace = do
74  -- Determine the common prefix of the current trace and the old trace
75  -- drop constraints beyond this common prefix from the current solver
76  -- context. Thereby, keeping the common prefix and making use of
77  -- incremental solving capabilities.
78  let prefix = prefixLength newTrace oldTrace
79  let toDrop = length oldTrace - prefix
80  -- TODO: Don't pop if toDrop is zero.
81  SMT.popMany solver $ fromIntegral toDrop
82
83  -- Only enforce new constraints, i.e. those beyond the common prefix.
84  assertTrace (drop prefix newTrace)
85
86  isSat <- SMT.check solver
87  case isSat of
88    SMT.Sat -> Just <$> Model.getModel solver inputVars
89    SMT.Unsat -> pure Nothing
90    SMT.Unknown -> throwIO UnknownResult
91  where
92    -- Add all conditions enforced by the given 'ExecTrace' to the solver.
93    -- Returns a list of all asserted conditions.
94    assertTrace :: ExecTrace -> IO ()
95    assertTrace [] = pure ()
96    assertTrace t = do
97      let conds = map (\(b, Branch _ c) -> SE.toCond b c) t
98      mapM_ (\c -> SMT.push solver >> SMT.assert solver c) conds