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.DFS
  7  ( PathSel,
  8    newPathSel,
  9    trackTrace,
 10    findUnexplored,
 11  )
 12where
 13
 14import Control.Applicative ((<|>))
 15import Control.Exception (throwIO)
 16import Language.QBE.Backend (SolverError (UnknownResult), prefixLength)
 17import Language.QBE.Backend.ExecTree (BTree (..), ExecTree, addTrace, mkTree)
 18import Language.QBE.Backend.Model qualified as Model
 19import Language.QBE.Backend.Tracer (Branch (..), ExecTrace)
 20import Language.QBE.Simulator.Symbolic.Expression qualified as SE
 21import SimpleSMT qualified as SMT
 22
 23-- The 'PathSel' encapsulates data for the Dynamic Symbolic Execution (DSE)
 24-- algorithm. Specifically for path selection and incremental solving.
 25data PathSel
 26  = PathSel
 27      ExecTree -- The current execution tree for the DSE algorithm
 28      ExecTrace -- The last solved trace, for incremental solving.
 29
 30-- Create a new empty 'PathSel' object without anything traced yet.
 31newPathSel :: PathSel
 32newPathSel = PathSel (mkTree []) []
 33
 34-- Track a new 'ExecTrace' in the 'PathSel'.
 35trackTrace :: PathSel -> ExecTrace -> PathSel
 36trackTrace (PathSel tree t) trace =
 37  PathSel (addTrace tree trace) t
 38
 39-- For a given execution trace, return an assignment (represented
 40-- as a 'Model') which statisfies all symbolic branch conditions.
 41-- If such an assignment does not exist, then 'Nothing' is returned.
 42--
 43-- Throws a 'SolverError' on an unknown solver result (e.g., on timeout).
 44--
 45-- TODO: Remove dependency on 'PathSel' and move this elsewhere.
 46solveTrace :: SMT.Solver -> [SMT.SExpr] -> PathSel -> ExecTrace -> IO (Maybe Model.Model)
 47solveTrace solver inputVars (PathSel _ oldTrace) newTrace = do
 48  -- Determine the common prefix of the current trace and the old trace
 49  -- drop constraints beyond this common prefix from the current solver
 50  -- context. Thereby, keeping the common prefix and making use of
 51  -- incremental solving capabilities.
 52  let prefix = prefixLength newTrace oldTrace
 53  let toDrop = length oldTrace - prefix
 54  -- TODO: Don't pop if toDrop is zero.
 55  SMT.popMany solver $ fromIntegral toDrop
 56
 57  -- Only enforce new constraints, i.e. those beyond the common prefix.
 58  assertTrace (drop prefix newTrace)
 59
 60  isSat <- SMT.check solver
 61  case isSat of
 62    SMT.Sat -> Just <$> Model.getModel solver inputVars
 63    SMT.Unsat -> pure Nothing
 64    SMT.Unknown -> throwIO UnknownResult
 65  where
 66    -- Add all conditions enforced by the given 'ExecTrace' to the solver.
 67    -- Returns a list of all asserted conditions.
 68    assertTrace :: ExecTrace -> IO ()
 69    assertTrace [] = pure ()
 70    assertTrace t = do
 71      -- TODO: use pushMany
 72      let conds = map (\(b, Branch _ c) -> SE.toCond b c) t
 73      mapM_ (\c -> SMT.push solver >> SMT.assert solver c) conds
 74
 75-- Find an assignment that causes exploration of a new execution path through
 76-- the tested software. This function updates the metadata in the execution
 77-- tree and thus returns a new execution tree, even if no satisfiable
 78-- assignment was found.
 79--
 80-- TODO: Can we get by without passing 'inputVars` here again?
 81findUnexplored :: SMT.Solver -> [SMT.SExpr] -> PathSel -> IO (Maybe Model.Model, PathSel)
 82findUnexplored solver inputVars tracer@(PathSel tree _) = do
 83  case negateBranch tree of
 84    Nothing -> pure (Nothing, tracer)
 85    Just nt -> do
 86      let nextTracer = PathSel (addTrace tree nt) nt
 87      res <- solveTrace solver inputVars tracer nt
 88      case res of
 89        Nothing -> findUnexplored solver inputVars nextTracer
 90        Just m -> pure (Just m, nextTracer)
 91  where
 92    -- Negate an unnegated branch in the execution tree and return an
 93    -- 'ExecTrace' which leads to an unexplored execution path. If no
 94    -- such path exists, then 'Nothing' is returned. If such a path
 95    -- exists a concrete variable assignment for it can be calculated
 96    -- using 'solveTrace'.
 97    --
 98    -- The branch node metadata in the resulting 'ExecTree' is updated
 99    -- to reflect that negation of the selected branch node was attempted.
100    -- If further branches are to be negated, the resulting trace should
101    -- be added to the 'ExecTree' using 'addTrace' to update the metadata
102    -- in the tree as well.
103    negateBranch :: ExecTree -> Maybe ExecTrace
104    negateBranch Leaf = Nothing
105    negateBranch (Node (Branch wasNeg ast) Nothing _)
106      | wasNeg = Nothing
107      | otherwise = Just [(True, Branch True ast)]
108    negateBranch (Node (Branch wasNeg ast) _ Nothing)
109      | wasNeg = Nothing
110      | otherwise = Just [(False, Branch True ast)]
111    negateBranch (Node br (Just ifTrue) (Just ifFalse)) =
112      do
113        (++) [(True, br)] <$> negateBranch ifTrue
114        <|> (++) [(False, br)] <$> negateBranch ifFalse