content: ------------------------------------------------------------------------
  -- |
  -- Module           : Lang.Crucible.LLVM.MemModel.CallStack.Internal
  -- Description      : Call stacks from the LLVM memory model (implementation details)
  -- Copyright        : (c) Galois, Inc 2024
  -- License          : BSD3
  -- Maintainer       : Langston Barrett <langston@galois.com>
  -- Stability        : provisional
  ------------------------------------------------------------------------
  
  {-# LANGUAGE GeneralizedNewtypeDeriving #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE OverloadedStrings #-}
  
  module Lang.Crucible.LLVM.MemModel.CallStack.Internal where
  
  import           Data.Foldable (toList)
  import           Data.Sequence (Seq)
  import qualified Data.Sequence as Seq
  import           Data.Text (Text)
  import qualified Prettyprinter as PP
  
  import           Lang.Crucible.LLVM.MemModel.MemLog (MemState(..))
  
  newtype FunctionName =
    FunctionName { getFunctionName :: Text }
    deriving (Eq, Monoid, Ord, Semigroup)
  
  -- | Call stacks (lists of function names), mostly for diagnostics
  newtype CallStack =
    CallStack { runCallStack :: Seq FunctionName }
    deriving (Eq, Monoid, Ord, Semigroup)
  
  -- | Add a function name to the top of the call stack
  cons :: FunctionName -> CallStack -> CallStack
  cons top (CallStack rest) = CallStack (top Seq.<| rest)
  
  -- | Is this 'CallStack' empty?
  null :: CallStack -> Bool
  null = Seq.null . runCallStack
  
  -- | Summarize the 'StackFrame's of a 'MemState' into a 'CallStack'
  getCallStack :: MemState sym -> CallStack
  getCallStack =
    \case
      EmptyMem{} -> CallStack mempty
      StackFrame _ _ nm _ rest -> cons (FunctionName nm) (getCallStack rest)
      BranchFrame _ _ _ rest -> getCallStack rest
  
  -- | Pretty-print a call stack (one function per line)
  ppCallStack :: CallStack -> PP.Doc ann
  ppCallStack =
    PP.vsep . toList . fmap (PP.pretty . getFunctionName) . runCallStack
  