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 SimpleSMT 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.
40--
41-- TODO: Can we get by without passing 'inputVars` here again?
42findUnexplored :: SMT.Solver -> [SMT.SExpr] -> PathSel -> IO (Maybe Model.Model, PathSel)
43findUnexplored solver inputVars tracer@(PathSel tree oldTrace) = do
44  case negateBranch tree of
45    Nothing -> pure (Nothing, tracer)
46    Just nt -> do
47      let nextTracer = PathSel (addTrace tree nt) nt
48      res <- solveTrace solver inputVars oldTrace nt
49      case res of
50        Nothing -> findUnexplored solver inputVars nextTracer
51        Just m -> pure (Just m, nextTracer)
52  where
53    -- Negate an unnegated branch in the execution tree and return an
54    -- 'ExecTrace' which leads to an unexplored execution path. If no
55    -- such path exists, then 'Nothing' is returned. If such a path
56    -- exists a concrete variable assignment for it can be calculated
57    -- using 'solveTrace'.
58    --
59    -- The branch node metadata in the resulting 'ExecTree' is updated
60    -- to reflect that negation of the selected branch node was attempted.
61    -- If further branches are to be negated, the resulting trace should
62    -- be added to the 'ExecTree' using 'addTrace' to update the metadata
63    -- in the tree as well.
64    negateBranch :: ExecTree -> Maybe ExecTrace
65    negateBranch Leaf = Nothing
66    negateBranch (Node (Branch wasNeg ast) Nothing _)
67      | wasNeg = Nothing
68      | otherwise = Just [(True, Branch True ast)]
69    negateBranch (Node (Branch wasNeg ast) _ Nothing)
70      | wasNeg = Nothing
71      | otherwise = Just [(False, Branch True ast)]
72    negateBranch (Node br (Just ifTrue) (Just ifFalse)) =
73      do
74        (++) [(True, br)] <$> negateBranch ifTrue
75        <|> (++) [(False, br)] <$> negateBranch ifFalse