-- 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.DFS
  ( PathSel,
    newPathSel,
    trackTrace,
    findUnexplored,
  )
where

import Control.Applicative ((<|>))
import Language.QBE.Backend.ExecTree (BTree (..), ExecTree, addTrace, mkTree)
import Language.QBE.Backend.Model qualified as Model
import Language.QBE.Backend.Tracer (Branch (..), ExecTrace, solveTrace)
import SimpleBV qualified as SMT

-- The 'PathSel' encapsulates data for the Dynamic Symbolic Execution (DSE)
-- algorithm. Specifically for path selection and incremental solving.
data PathSel
  = PathSel
      ExecTree -- The current execution tree for the DSE algorithm
      ExecTrace -- The last solved trace, for incremental solving.

-- Create a new empty 'PathSel' object without anything traced yet.
newPathSel :: PathSel
newPathSel :: PathSel
newPathSel = ExecTree -> ExecTrace -> PathSel
PathSel (ExecTrace -> ExecTree
mkTree []) []

-- Track a new 'ExecTrace' in the 'PathSel'.
trackTrace :: PathSel -> ExecTrace -> PathSel
trackTrace :: PathSel -> ExecTrace -> PathSel
trackTrace (PathSel ExecTree
tree ExecTrace
t) ExecTrace
trace =
  ExecTree -> ExecTrace -> PathSel
PathSel (ExecTree -> ExecTrace -> ExecTree
addTrace ExecTree
tree ExecTrace
trace) ExecTrace
t

-- Find an assignment that causes exploration of a new execution path through
-- the tested software. This function updates the metadata in the execution
-- tree and thus returns a new execution tree, even if no satisfiable
-- assignment was found.
findUnexplored :: SMT.Solver -> [SMT.SExpr] -> PathSel -> IO (Maybe Model.Model, PathSel)
findUnexplored :: Solver -> [SExpr] -> PathSel -> IO (Maybe Model, PathSel)
findUnexplored Solver
solver [SExpr]
inputVars tracer :: PathSel
tracer@(PathSel ExecTree
tree ExecTrace
oldTrace) = do
  case ExecTree -> Maybe ExecTrace
negateBranch ExecTree
tree of
    Maybe ExecTrace
Nothing -> (Maybe Model, PathSel) -> IO (Maybe Model, PathSel)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Model
forall a. Maybe a
Nothing, PathSel
tracer)
    Just ExecTrace
nt -> do
      let nextTracer :: PathSel
nextTracer = ExecTree -> ExecTrace -> PathSel
PathSel (ExecTree -> ExecTrace -> ExecTree
addTrace ExecTree
tree ExecTrace
nt) ExecTrace
nt
      Maybe Model
res <- Solver -> [SExpr] -> ExecTrace -> ExecTrace -> IO (Maybe Model)
solveTrace Solver
solver [SExpr]
inputVars ExecTrace
oldTrace ExecTrace
nt
      case Maybe Model
res of
        Maybe Model
Nothing -> Solver -> [SExpr] -> PathSel -> IO (Maybe Model, PathSel)
findUnexplored Solver
solver [SExpr]
inputVars PathSel
nextTracer
        Just Model
m -> (Maybe Model, PathSel) -> IO (Maybe Model, PathSel)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Model -> Maybe Model
forall a. a -> Maybe a
Just Model
m, PathSel
nextTracer)
  where
    -- Negate an unnegated branch in the execution tree and return an
    -- 'ExecTrace' which leads to an unexplored execution path. If no
    -- such path exists, then 'Nothing' is returned. If such a path
    -- exists a concrete variable assignment for it can be calculated
    -- using 'solveTrace'.
    --
    -- The branch node metadata in the resulting 'ExecTree' is updated
    -- to reflect that negation of the selected branch node was attempted.
    -- If further branches are to be negated, the resulting trace should
    -- be added to the 'ExecTree' using 'addTrace' to update the metadata
    -- in the tree as well.
    negateBranch :: ExecTree -> Maybe ExecTrace
    negateBranch :: ExecTree -> Maybe ExecTrace
negateBranch ExecTree
Leaf = Maybe ExecTrace
forall a. Maybe a
Nothing
    negateBranch (Node (Branch Bool
wasNeg BitVector
ast) Maybe ExecTree
Nothing Maybe ExecTree
_)
      | Bool
wasNeg = Maybe ExecTrace
forall a. Maybe a
Nothing
      | Bool
otherwise = ExecTrace -> Maybe ExecTrace
forall a. a -> Maybe a
Just [(Bool
True, Bool -> BitVector -> Branch
Branch Bool
True BitVector
ast)]
    negateBranch (Node (Branch Bool
wasNeg BitVector
ast) Maybe ExecTree
_ Maybe ExecTree
Nothing)
      | Bool
wasNeg = Maybe ExecTrace
forall a. Maybe a
Nothing
      | Bool
otherwise = ExecTrace -> Maybe ExecTrace
forall a. a -> Maybe a
Just [(Bool
False, Bool -> BitVector -> Branch
Branch Bool
True BitVector
ast)]
    negateBranch (Node Branch
br (Just ExecTree
ifTrue) (Just ExecTree
ifFalse)) =
      do
        ExecTrace -> ExecTrace -> ExecTrace
forall a. [a] -> [a] -> [a]
(++) [(Bool
True, Branch
br)] (ExecTrace -> ExecTrace) -> Maybe ExecTrace -> Maybe ExecTrace
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecTree -> Maybe ExecTrace
negateBranch ExecTree
ifTrue
        Maybe ExecTrace -> Maybe ExecTrace -> Maybe ExecTrace
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ExecTrace -> ExecTrace -> ExecTrace
forall a. [a] -> [a] -> [a]
(++) [(Bool
False, Branch
br)] (ExecTrace -> ExecTrace) -> Maybe ExecTrace -> Maybe ExecTrace
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ExecTree -> Maybe ExecTrace
negateBranch ExecTree
ifFalse