------------------------------------------------------------------------
-- |
-- 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 { FunctionName -> Text
getFunctionName :: Text }
  deriving (FunctionName -> FunctionName -> Bool
(FunctionName -> FunctionName -> Bool)
-> (FunctionName -> FunctionName -> Bool) -> Eq FunctionName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FunctionName -> FunctionName -> Bool
== :: FunctionName -> FunctionName -> Bool
$c/= :: FunctionName -> FunctionName -> Bool
/= :: FunctionName -> FunctionName -> Bool
Eq, Semigroup FunctionName
FunctionName
Semigroup FunctionName =>
FunctionName
-> (FunctionName -> FunctionName -> FunctionName)
-> ([FunctionName] -> FunctionName)
-> Monoid FunctionName
[FunctionName] -> FunctionName
FunctionName -> FunctionName -> FunctionName
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: FunctionName
mempty :: FunctionName
$cmappend :: FunctionName -> FunctionName -> FunctionName
mappend :: FunctionName -> FunctionName -> FunctionName
$cmconcat :: [FunctionName] -> FunctionName
mconcat :: [FunctionName] -> FunctionName
Monoid, Eq FunctionName
Eq FunctionName =>
(FunctionName -> FunctionName -> Ordering)
-> (FunctionName -> FunctionName -> Bool)
-> (FunctionName -> FunctionName -> Bool)
-> (FunctionName -> FunctionName -> Bool)
-> (FunctionName -> FunctionName -> Bool)
-> (FunctionName -> FunctionName -> FunctionName)
-> (FunctionName -> FunctionName -> FunctionName)
-> Ord FunctionName
FunctionName -> FunctionName -> Bool
FunctionName -> FunctionName -> Ordering
FunctionName -> FunctionName -> FunctionName
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: FunctionName -> FunctionName -> Ordering
compare :: FunctionName -> FunctionName -> Ordering
$c< :: FunctionName -> FunctionName -> Bool
< :: FunctionName -> FunctionName -> Bool
$c<= :: FunctionName -> FunctionName -> Bool
<= :: FunctionName -> FunctionName -> Bool
$c> :: FunctionName -> FunctionName -> Bool
> :: FunctionName -> FunctionName -> Bool
$c>= :: FunctionName -> FunctionName -> Bool
>= :: FunctionName -> FunctionName -> Bool
$cmax :: FunctionName -> FunctionName -> FunctionName
max :: FunctionName -> FunctionName -> FunctionName
$cmin :: FunctionName -> FunctionName -> FunctionName
min :: FunctionName -> FunctionName -> FunctionName
Ord, NonEmpty FunctionName -> FunctionName
FunctionName -> FunctionName -> FunctionName
(FunctionName -> FunctionName -> FunctionName)
-> (NonEmpty FunctionName -> FunctionName)
-> (forall b. Integral b => b -> FunctionName -> FunctionName)
-> Semigroup FunctionName
forall b. Integral b => b -> FunctionName -> FunctionName
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: FunctionName -> FunctionName -> FunctionName
<> :: FunctionName -> FunctionName -> FunctionName
$csconcat :: NonEmpty FunctionName -> FunctionName
sconcat :: NonEmpty FunctionName -> FunctionName
$cstimes :: forall b. Integral b => b -> FunctionName -> FunctionName
stimes :: forall b. Integral b => b -> FunctionName -> FunctionName
Semigroup)

-- | Call stacks (lists of function names), mostly for diagnostics
newtype CallStack =
  CallStack { CallStack -> Seq FunctionName
runCallStack :: Seq FunctionName }
  deriving (CallStack -> CallStack -> Bool
(CallStack -> CallStack -> Bool)
-> (CallStack -> CallStack -> Bool) -> Eq CallStack
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CallStack -> CallStack -> Bool
== :: CallStack -> CallStack -> Bool
$c/= :: CallStack -> CallStack -> Bool
/= :: CallStack -> CallStack -> Bool
Eq, Semigroup CallStack
CallStack
Semigroup CallStack =>
CallStack
-> (CallStack -> CallStack -> CallStack)
-> ([CallStack] -> CallStack)
-> Monoid CallStack
[CallStack] -> CallStack
CallStack -> CallStack -> CallStack
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: CallStack
mempty :: CallStack
$cmappend :: CallStack -> CallStack -> CallStack
mappend :: CallStack -> CallStack -> CallStack
$cmconcat :: [CallStack] -> CallStack
mconcat :: [CallStack] -> CallStack
Monoid, Eq CallStack
Eq CallStack =>
(CallStack -> CallStack -> Ordering)
-> (CallStack -> CallStack -> Bool)
-> (CallStack -> CallStack -> Bool)
-> (CallStack -> CallStack -> Bool)
-> (CallStack -> CallStack -> Bool)
-> (CallStack -> CallStack -> CallStack)
-> (CallStack -> CallStack -> CallStack)
-> Ord CallStack
CallStack -> CallStack -> Bool
CallStack -> CallStack -> Ordering
CallStack -> CallStack -> CallStack
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: CallStack -> CallStack -> Ordering
compare :: CallStack -> CallStack -> Ordering
$c< :: CallStack -> CallStack -> Bool
< :: CallStack -> CallStack -> Bool
$c<= :: CallStack -> CallStack -> Bool
<= :: CallStack -> CallStack -> Bool
$c> :: CallStack -> CallStack -> Bool
> :: CallStack -> CallStack -> Bool
$c>= :: CallStack -> CallStack -> Bool
>= :: CallStack -> CallStack -> Bool
$cmax :: CallStack -> CallStack -> CallStack
max :: CallStack -> CallStack -> CallStack
$cmin :: CallStack -> CallStack -> CallStack
min :: CallStack -> CallStack -> CallStack
Ord, NonEmpty CallStack -> CallStack
CallStack -> CallStack -> CallStack
(CallStack -> CallStack -> CallStack)
-> (NonEmpty CallStack -> CallStack)
-> (forall b. Integral b => b -> CallStack -> CallStack)
-> Semigroup CallStack
forall b. Integral b => b -> CallStack -> CallStack
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: CallStack -> CallStack -> CallStack
<> :: CallStack -> CallStack -> CallStack
$csconcat :: NonEmpty CallStack -> CallStack
sconcat :: NonEmpty CallStack -> CallStack
$cstimes :: forall b. Integral b => b -> CallStack -> CallStack
stimes :: forall b. Integral b => b -> CallStack -> CallStack
Semigroup)

-- | Add a function name to the top of the call stack
cons :: FunctionName -> CallStack -> CallStack
cons :: FunctionName -> CallStack -> CallStack
cons FunctionName
top (CallStack Seq FunctionName
rest) = Seq FunctionName -> CallStack
CallStack (FunctionName
top FunctionName -> Seq FunctionName -> Seq FunctionName
forall a. a -> Seq a -> Seq a
Seq.<| Seq FunctionName
rest)

-- | Is this 'CallStack' empty?
null :: CallStack -> Bool
null :: CallStack -> Bool
null = Seq FunctionName -> Bool
forall a. Seq a -> Bool
Seq.null (Seq FunctionName -> Bool)
-> (CallStack -> Seq FunctionName) -> CallStack -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Seq FunctionName
runCallStack

-- | Summarize the 'StackFrame's of a 'MemState' into a 'CallStack'
getCallStack :: MemState sym -> CallStack
getCallStack :: forall sym. MemState sym -> CallStack
getCallStack =
  \case
    EmptyMem{} -> Seq FunctionName -> CallStack
CallStack Seq FunctionName
forall a. Monoid a => a
mempty
    StackFrame Int
_ Int
_ Text
nm MemChanges sym
_ MemState sym
rest -> FunctionName -> CallStack -> CallStack
cons (Text -> FunctionName
FunctionName Text
nm) (MemState sym -> CallStack
forall sym. MemState sym -> CallStack
getCallStack MemState sym
rest)
    BranchFrame Int
_ Int
_ MemChanges sym
_ MemState sym
rest -> MemState sym -> CallStack
forall sym. MemState sym -> CallStack
getCallStack MemState sym
rest

-- | Pretty-print a call stack (one function per line)
ppCallStack :: CallStack -> PP.Doc ann
ppCallStack :: forall ann. CallStack -> Doc ann
ppCallStack =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vsep ([Doc ann] -> Doc ann)
-> (CallStack -> [Doc ann]) -> CallStack -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq (Doc ann) -> [Doc ann]
forall a. Seq a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList (Seq (Doc ann) -> [Doc ann])
-> (CallStack -> Seq (Doc ann)) -> CallStack -> [Doc ann]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FunctionName -> Doc ann) -> Seq FunctionName -> Seq (Doc ann)
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Doc ann
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (Text -> Doc ann)
-> (FunctionName -> Text) -> FunctionName -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FunctionName -> Text
getFunctionName) (Seq FunctionName -> Seq (Doc ann))
-> (CallStack -> Seq FunctionName) -> CallStack -> Seq (Doc ann)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> Seq FunctionName
runCallStack