-- SPDX-FileCopyrightText: 2024 University of Bremen
-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
--
-- SPDX-License-Identifier: MIT AND GPL-3.0-only

module Language.QBE.Backend.ExecTree
  ( BTree (..),
    ExecTree,
    mkTree,
    addTrace,
  )
where

import Language.QBE.Backend.Tracer (Branch, ExecTrace, fromBranch)

-- A binary tree.
data BTree a = Node a (Maybe (BTree a)) (Maybe (BTree a)) | Leaf
  deriving (Int -> BTree a -> ShowS
[BTree a] -> ShowS
BTree a -> String
(Int -> BTree a -> ShowS)
-> (BTree a -> String) -> ([BTree a] -> ShowS) -> Show (BTree a)
forall a. Show a => Int -> BTree a -> ShowS
forall a. Show a => [BTree a] -> ShowS
forall a. Show a => BTree a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> BTree a -> ShowS
showsPrec :: Int -> BTree a -> ShowS
$cshow :: forall a. Show a => BTree a -> String
show :: BTree a -> String
$cshowList :: forall a. Show a => [BTree a] -> ShowS
showList :: [BTree a] -> ShowS
Show, BTree a -> BTree a -> Bool
(BTree a -> BTree a -> Bool)
-> (BTree a -> BTree a -> Bool) -> Eq (BTree a)
forall a. Eq a => BTree a -> BTree a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => BTree a -> BTree a -> Bool
== :: BTree a -> BTree a -> Bool
$c/= :: forall a. Eq a => BTree a -> BTree a -> Bool
/= :: BTree a -> BTree a -> Bool
Eq)

-- Execution tree for the exeucted software, represented as follows:
--
--                                 a
--                          True  / \  False
--                               b   …
--                              / \
--                             N   L
--
-- where the edges indicate what happens if branch a is true/false.
-- The left edge covers the true path while the right edge covers the
-- false path.
--
-- The Nothing (N) value indicates that a path has not been explored.
-- In the example above the path `[(True, a), (True, b)]` has not been
-- explored. A Leaf (L) node is used to indicate that a path has been
-- explored but we haven't discored additional branches yet. In the
-- example above the deepest path is hence `[(True a), (False, b)]`.
type ExecTree = BTree Branch

-- Returns 'True' if we can continue exploring on this branch node.
-- This is the case if the node is either a 'Leaf' or 'Nothing'.
canCont :: Maybe (BTree a) -> Bool
canCont :: forall a. Maybe (BTree a) -> Bool
canCont Maybe (BTree a)
Nothing = Bool
True
canCont (Just BTree a
Leaf) = Bool
True
canCont Maybe (BTree a)
_ = Bool
False

-- Create a new execution tree from a trace.
mkTree :: ExecTrace -> ExecTree
mkTree :: ExecTrace -> ExecTree
mkTree [] = ExecTree
forall a. BTree a
Leaf
mkTree [(Bool
wasTrue, Branch
br)]
  | Bool
wasTrue = Branch -> Maybe ExecTree -> Maybe ExecTree -> ExecTree
forall a. a -> Maybe (BTree a) -> Maybe (BTree a) -> BTree a
Node Branch
br (ExecTree -> Maybe ExecTree
forall a. a -> Maybe a
Just ExecTree
forall a. BTree a
Leaf) Maybe ExecTree
forall a. Maybe a
Nothing
  | Bool
otherwise = Branch -> Maybe ExecTree -> Maybe ExecTree -> ExecTree
forall a. a -> Maybe (BTree a) -> Maybe (BTree a) -> BTree a
Node Branch
br Maybe ExecTree
forall a. Maybe a
Nothing (ExecTree -> Maybe ExecTree
forall a. a -> Maybe a
Just ExecTree
forall a. BTree a
Leaf)
mkTree ((Bool
True, Branch
br) : ExecTrace
xs) = Branch -> Maybe ExecTree -> Maybe ExecTree -> ExecTree
forall a. a -> Maybe (BTree a) -> Maybe (BTree a) -> BTree a
Node Branch
br (ExecTree -> Maybe ExecTree
forall a. a -> Maybe a
Just (ExecTree -> Maybe ExecTree) -> ExecTree -> Maybe ExecTree
forall a b. (a -> b) -> a -> b
$ ExecTrace -> ExecTree
mkTree ExecTrace
xs) Maybe ExecTree
forall a. Maybe a
Nothing
mkTree ((Bool
False, Branch
br) : ExecTrace
xs) = Branch -> Maybe ExecTree -> Maybe ExecTree -> ExecTree
forall a. a -> Maybe (BTree a) -> Maybe (BTree a) -> BTree a
Node Branch
br Maybe ExecTree
forall a. Maybe a
Nothing (ExecTree -> Maybe ExecTree
forall a. a -> Maybe a
Just (ExecTree -> Maybe ExecTree) -> ExecTree -> Maybe ExecTree
forall a b. (a -> b) -> a -> b
$ ExecTrace -> ExecTree
mkTree ExecTrace
xs)

-- Add a trace to an existing execution tree. The control flow
-- in the trace must match the existing tree. If it diverges,
-- an error is raised.
--
-- This function prefers the branch nodes from the trace in the
-- resulting 'ExecTree', thus allowing updating their metadata via
-- this function.
--
-- Assertion: The branch encode in the Node and the branch encoded in
-- the trace should also be equal, regarding the encoded condition.
addTrace :: ExecTree -> ExecTrace -> ExecTree
addTrace :: ExecTree -> ExecTrace -> ExecTree
addTrace ExecTree
tree [] = ExecTree
tree
-- The trace takes the True branch and we have taken that previously.
--  ↳ Recursively decent on that branch and look at remaining trace.
addTrace (Node Branch
br' (Just ExecTree
tb) Maybe ExecTree
fb) ((Bool
True, Branch
br) : ExecTrace
xs) =
  Branch -> Maybe ExecTree -> Maybe ExecTree -> ExecTree
forall a. a -> Maybe (BTree a) -> Maybe (BTree a) -> BTree a
Node (Branch -> Branch -> Branch
fromBranch Branch
br' Branch
br) (ExecTree -> Maybe ExecTree
forall a. a -> Maybe a
Just (ExecTree -> Maybe ExecTree) -> ExecTree -> Maybe ExecTree
forall a b. (a -> b) -> a -> b
$ ExecTree -> ExecTrace -> ExecTree
addTrace ExecTree
tb ExecTrace
xs) Maybe ExecTree
fb
-- The trace takes the False branch and we have taken that previously.
--  ↳ Recursively decent on that branch and look at remaining trace.
addTrace (Node Branch
br' Maybe ExecTree
tb (Just ExecTree
fb)) ((Bool
False, Branch
br) : ExecTrace
xs) =
  Branch -> Maybe ExecTree -> Maybe ExecTree -> ExecTree
forall a. a -> Maybe (BTree a) -> Maybe (BTree a) -> BTree a
Node (Branch -> Branch -> Branch
fromBranch Branch
br' Branch
br) Maybe ExecTree
tb (ExecTree -> Maybe ExecTree
forall a. a -> Maybe a
Just (ExecTree -> Maybe ExecTree) -> ExecTree -> Maybe ExecTree
forall a b. (a -> b) -> a -> b
$ ExecTree -> ExecTrace -> ExecTree
addTrace ExecTree
fb ExecTrace
xs)
-- If the trace takes the True/False branch and we have not taken that
-- yet (i.e. canCont is True) we insert the trace at that position.
addTrace (Node Branch
br' Maybe ExecTree
tb Maybe ExecTree
fb) ((Bool
wasTrue, Branch
br) : ExecTrace
xs)
  | Maybe ExecTree -> Bool
forall a. Maybe (BTree a) -> Bool
canCont Maybe ExecTree
tb Bool -> Bool -> Bool
&& Bool
wasTrue = Branch -> Maybe ExecTree -> Maybe ExecTree -> ExecTree
forall a. a -> Maybe (BTree a) -> Maybe (BTree a) -> BTree a
Node (Branch -> Branch -> Branch
fromBranch Branch
br' Branch
br) (ExecTree -> Maybe ExecTree
forall a. a -> Maybe a
Just (ExecTree -> Maybe ExecTree) -> ExecTree -> Maybe ExecTree
forall a b. (a -> b) -> a -> b
$ ExecTrace -> ExecTree
mkTree ExecTrace
xs) Maybe ExecTree
fb
  | Maybe ExecTree -> Bool
forall a. Maybe (BTree a) -> Bool
canCont Maybe ExecTree
fb Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
wasTrue = Branch -> Maybe ExecTree -> Maybe ExecTree -> ExecTree
forall a. a -> Maybe (BTree a) -> Maybe (BTree a) -> BTree a
Node (Branch -> Branch -> Branch
fromBranch Branch
br' Branch
br) Maybe ExecTree
tb (ExecTree -> Maybe ExecTree
forall a. a -> Maybe a
Just (ExecTree -> Maybe ExecTree) -> ExecTree -> Maybe ExecTree
forall a b. (a -> b) -> a -> b
$ ExecTrace -> ExecTree
mkTree ExecTrace
xs)
  | Bool
otherwise = String -> ExecTree
forall a. HasCallStack => String -> a
error String
"unreachable"
-- If we encounter a leaf, this part hasn't been explored yet.
-- That is, we can just insert the trace "as is" at this point.
addTrace ExecTree
Leaf ExecTrace
trace = ExecTrace -> ExecTree
mkTree ExecTrace
trace