Merge pull request #1163 from langston-barrett/lb/llvm-callstack

llvm: Export `CallStack` internals from an internal module
GaloisInc · Jan 10, 2024 · 0e097d5 · 0e097d5
2 parents dba7b1b + 50e83e9
commit 0e097d5
Show file tree

Hide file tree

Showing 3 changed files with 59 additions and 35 deletions.
diff --git a/crucible-llvm/crucible-llvm.cabal b/crucible-llvm/crucible-llvm.cabal
@@ -72,6 +72,7 @@ library
     Lang.Crucible.LLVM.MalformedLLVMModule
     Lang.Crucible.LLVM.MemModel
     Lang.Crucible.LLVM.MemModel.CallStack
+    Lang.Crucible.LLVM.MemModel.CallStack.Internal
     Lang.Crucible.LLVM.MemModel.Generic
     Lang.Crucible.LLVM.MemModel.MemLog
     Lang.Crucible.LLVM.MemModel.Partial

diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/CallStack.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/CallStack.hs
@@ -2,48 +2,18 @@
 -- |
 -- Module           : Lang.Crucible.LLVM.MemModel.CallStack
 -- Description      : Call stacks from the LLVM memory model
--- Copyright        : (c) Galois, Inc 2021
+-- Copyright        : (c) Galois, Inc 2024
 -- License          : BSD3
--- Maintainer       : Rob Dockins <rdockins@galois.com>
+-- Maintainer       : Langston Barrett <langston@galois.com>
 -- Stability        : provisional
 ------------------------------------------------------------------------
 
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE LambdaCase #-}
-{-# LANGUAGE OverloadedStrings #-}
-
 module Lang.Crucible.LLVM.MemModel.CallStack
   ( CallStack
+  , null
   , getCallStack
   , ppCallStack
   ) 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)
-
-newtype CallStack =
-  CallStack { runCallStack :: Seq FunctionName }
-  deriving (Eq, Monoid, Ord, Semigroup)
-
-cons :: FunctionName -> CallStack -> CallStack
-cons top (CallStack rest) = CallStack (top Seq.<| rest)
-
-getCallStack :: MemState sym -> CallStack
-getCallStack =
-  \case
-    EmptyMem{} -> CallStack mempty
-    StackFrame _ _ nm _ rest -> cons (FunctionName nm) (getCallStack rest)
-    BranchFrame _ _ _ rest -> getCallStack rest
-
-ppCallStack :: CallStack -> PP.Doc ann
-ppCallStack =
-  PP.vsep . toList . fmap (PP.pretty . getFunctionName) . runCallStack
+import Prelude hiding (null)
+import Lang.Crucible.LLVM.MemModel.CallStack.Internal
diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/CallStack/Internal.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/CallStack/Internal.hs
@@ -0,0 +1,53 @@
+------------------------------------------------------------------------
+-- |
+-- 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 <[email protected]>
+-- 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