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.Simulator.Symbolic.Expression qualified as SE
 20import Language.QBE.Simulator.Symbolic.Tracer (Branch (..), ExecTrace)
 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).
 44solveTrace :: SMT.Solver -> [SMT.SExpr] -> PathSel -> ExecTrace -> IO (Maybe Model.Model)
 45solveTrace solver inputVars (PathSel _ oldTrace) newTrace = do
 46  -- Determine the common prefix of the current trace and the old trace
 47  -- drop constraints beyond this common prefix from the current solver
 48  -- context. Thereby, keeping the common prefix and making use of
 49  -- incremental solving capabilities.
 50  let prefix = prefixLength newTrace oldTrace
 51  let toDrop = length oldTrace - prefix
 52  SMT.popMany solver $ fromIntegral toDrop
 53
 54  -- Only enforce new constraints, i.e. those beyond the common prefix.
 55  assertTrace (drop prefix newTrace)
 56
 57  isSat <- SMT.check solver
 58  case isSat of
 59    SMT.Sat -> Just <$> Model.getModel solver inputVars
 60    SMT.Unsat -> pure Nothing
 61    SMT.Unknown -> throwIO UnknownResult
 62  where
 63    -- Add all conditions enforced by the given 'ExecTrace' to the solver.
 64    -- Returns a list of all asserted conditions.
 65    assertTrace :: ExecTrace -> IO ()
 66    assertTrace [] = pure ()
 67    assertTrace t = do
 68      let conds = map (\(b, Branch _ c) -> SE.toCond b c) t
 69      mapM_ (\c -> SMT.push solver >> SMT.assert solver c) conds
 70
 71-- Find an assignment that causes exploration of a new execution path through
 72-- the tested software. This function updates the metadata in the execution
 73-- tree and thus returns a new execution tree, even if no satisfiable
 74-- assignment was found.
 75--
 76-- TODO: Can we get by without passing 'inputVars` here again?
 77findUnexplored :: SMT.Solver -> [SMT.SExpr] -> PathSel -> IO (Maybe Model.Model, PathSel)
 78findUnexplored solver inputVars tracer@(PathSel tree _) = do
 79  case negateBranch tree of
 80    Nothing -> pure (Nothing, tracer)
 81    Just nt -> do
 82      let nextTracer = PathSel (addTrace tree nt) nt
 83      res <- solveTrace solver inputVars tracer nt
 84      case res of
 85        Nothing -> findUnexplored solver inputVars nextTracer
 86        Just m -> pure (Just m, nextTracer)
 87  where
 88    -- Negate an unnegated branch in the execution tree and return an
 89    -- 'ExecTrace' which leads to an unexplored execution path. If no
 90    -- such path exists, then 'Nothing' is returned. If such a path
 91    -- exists a concrete variable assignment for it can be calculated
 92    -- using 'solveTrace'.
 93    --
 94    -- The branch node metadata in the resulting 'ExecTree' is updated
 95    -- to reflect that negation of the selected branch node was attempted.
 96    -- If further branches are to be negated, the resulting trace should
 97    -- be added to the 'ExecTree' using 'addTrace' to update the metadata
 98    -- in the tree as well.
 99    negateBranch :: ExecTree -> Maybe ExecTrace
100    negateBranch Leaf = Nothing
101    negateBranch (Node (Branch wasNeg ast) Nothing _)
102      | wasNeg = Nothing
103      | otherwise = Just [(True, Branch True ast)]
104    negateBranch (Node (Branch wasNeg ast) _ Nothing)
105      | wasNeg = Nothing
106      | otherwise = Just [(False, Branch True ast)]
107    negateBranch (Node br (Just ifTrue) (Just ifFalse)) =
108      do
109        (++) [(True, br)] <$> negateBranch ifTrue
110        <|> (++) [(False, br)] <$> negateBranch ifFalse