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.ExecTree
 7  ( BTree (..),
 8    ExecTree,
 9    mkTree,
10    addTrace,
11  )
12where
13
14import Language.QBE.Simulator.Symbolic.Tracer (Branch, ExecTrace, fromBranch)
15
16-- A binary tree.
17data BTree a = Node a (Maybe (BTree a)) (Maybe (BTree a)) | Leaf
18  deriving (Show, Eq)
19
20-- Execution tree for the exeucted software, represented as follows:
21--
22--                                 a
23--                          True  / \  False
24--                               b   …
25--                              / \
26--                             N   L
27--
28-- where the edges indicate what happens if branch a is true/false.
29-- The left edge covers the true path while the right edge covers the
30-- false path.
31--
32-- The Nothing (N) value indicates that a path has not been explored.
33-- In the example above the path `[(True, a), (True, b)]` has not been
34-- explored. A Leaf (L) node is used to indicate that a path has been
35-- explored but we haven't discored additional branches yet. In the
36-- example above the deepest path is hence `[(True a), (False, b)]`.
37type ExecTree = BTree Branch
38
39-- Returns 'True' if we can continue exploring on this branch node.
40-- This is the case if the node is either a 'Leaf' or 'Nothing'.
41canCont :: Maybe (BTree a) -> Bool
42canCont Nothing = True
43canCont (Just Leaf) = True
44canCont _ = False
45
46-- Create a new execution tree from a trace.
47mkTree :: ExecTrace -> ExecTree
48mkTree [] = Leaf
49mkTree [(wasTrue, br)]
50  | wasTrue = Node br (Just Leaf) Nothing
51  | otherwise = Node br Nothing (Just Leaf)
52mkTree ((True, br) : xs) = Node br (Just $ mkTree xs) Nothing
53mkTree ((False, br) : xs) = Node br Nothing (Just $ mkTree xs)
54
55-- Add a trace to an existing execution tree. The control flow
56-- in the trace must match the existing tree. If it diverges,
57-- an error is raised.
58--
59-- This function prefers the branch nodes from the trace in the
60-- resulting 'ExecTree', thus allowing updating their metadata via
61-- this function.
62--
63-- Assertion: The branch encode in the Node and the branch encoded in
64-- the trace should also be equal, regarding the encoded condition.
65addTrace :: ExecTree -> ExecTrace -> ExecTree
66addTrace tree [] = tree
67-- The trace takes the True branch and we have taken that previously.
68--  ↳ Recursively decent on that branch and look at remaining trace.
69addTrace (Node br' (Just tb) fb) ((True, br) : xs) =
70  Node (fromBranch br' br) (Just $ addTrace tb xs) fb
71-- The trace takes the False branch and we have taken that previously.
72--  ↳ Recursively decent on that branch and look at remaining trace.
73addTrace (Node br' tb (Just fb)) ((False, br) : xs) =
74  Node (fromBranch br' br) tb (Just $ addTrace fb xs)
75-- If the trace takes the True/False branch and we have not taken that
76-- yet (i.e. canCont is True) we insert the trace at that position.
77addTrace (Node br' tb fb) ((wasTrue, br) : xs)
78  | canCont tb && wasTrue = Node (fromBranch br' br) (Just $ mkTree xs) fb
79  | canCont fb && not wasTrue = Node (fromBranch br' br) tb (Just $ mkTree xs)
80  | otherwise = error "unreachable"
81-- If we encounter a leaf, this part hasn't been explored yet.
82-- That is, we can just insert the trace "as is" at this point.
83addTrace Leaf trace = mkTree trace