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 Language.QBE.Backend.ExecTree (BTree (..), ExecTree, addTrace, mkTree)
16import Language.QBE.Backend.Model qualified as Model
17import Language.QBE.Backend.Tracer (Branch (..), ExecTrace, solveTrace)
18import SimpleBV qualified as SMT
19
20-- The 'PathSel' encapsulates data for the Dynamic Symbolic Execution (DSE)
21-- algorithm. Specifically for path selection and incremental solving.
22data PathSel
23  = PathSel
24      ExecTree -- The current execution tree for the DSE algorithm
25      ExecTrace -- The last solved trace, for incremental solving.
26
27-- Create a new empty 'PathSel' object without anything traced yet.
28newPathSel :: PathSel
29newPathSel = PathSel (mkTree []) []
30
31-- Track a new 'ExecTrace' in the 'PathSel'.
32trackTrace :: PathSel -> ExecTrace -> PathSel
33trackTrace (PathSel tree t) trace =
34  PathSel (addTrace tree trace) t
35
36-- Find an assignment that causes exploration of a new execution path through
37-- the tested software. This function updates the metadata in the execution
38-- tree and thus returns a new execution tree, even if no satisfiable
39-- assignment was found.
40findUnexplored :: SMT.Solver -> [SMT.SExpr] -> PathSel -> IO (Maybe Model.Model, PathSel)
41findUnexplored solver inputVars tracer@(PathSel tree oldTrace) = do
42  case negateBranch tree of
43    Nothing -> pure (Nothing, tracer)
44    Just nt -> do
45      let nextTracer = PathSel (addTrace tree nt) nt
46      res <- solveTrace solver inputVars oldTrace nt
47      case res of
48        Nothing -> findUnexplored solver inputVars nextTracer
49        Just m -> pure (Just m, nextTracer)
50  where
51    -- Negate an unnegated branch in the execution tree and return an
52    -- 'ExecTrace' which leads to an unexplored execution path. If no
53    -- such path exists, then 'Nothing' is returned. If such a path
54    -- exists a concrete variable assignment for it can be calculated
55    -- using 'solveTrace'.
56    --
57    -- The branch node metadata in the resulting 'ExecTree' is updated
58    -- to reflect that negation of the selected branch node was attempted.
59    -- If further branches are to be negated, the resulting trace should
60    -- be added to the 'ExecTree' using 'addTrace' to update the metadata
61    -- in the tree as well.
62    negateBranch :: ExecTree -> Maybe ExecTrace
63    negateBranch Leaf = Nothing
64    negateBranch (Node (Branch wasNeg ast) Nothing _)
65      | wasNeg = Nothing
66      | otherwise = Just [(True, Branch True ast)]
67    negateBranch (Node (Branch wasNeg ast) _ Nothing)
68      | wasNeg = Nothing
69      | otherwise = Just [(False, Branch True ast)]
70    negateBranch (Node br (Just ifTrue) (Just ifFalse)) =
71      do
72        (++) [(True, br)] <$> negateBranch ifTrue
73        <|> (++) [(False, br)] <$> negateBranch ifFalse