From 8e81d9a040a9510a3e41e5753b19a44d1c73fbc2 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Mon, 13 Dec 2021 16:15:14 -0500
Subject: [PATCH] uc-crux-llvm: Use HasCallStack for malformedLLVMModule

---
 .../src/UCCrux/LLVM/Context/Function.hs       | 16 ++++++++-------
 .../src/UCCrux/LLVM/Context/Module.hs         |  2 ++
 .../UCCrux/LLVM/Errors/MalformedLLVMModule.hs | 10 ++++++----
 .../src/UCCrux/LLVM/FullType/Translation.hs   | 20 +++++++++----------
 4 files changed, 27 insertions(+), 21 deletions(-)

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Context/Function.hs b/uc-crux-llvm/src/UCCrux/LLVM/Context/Function.hs
index c90d5bb69..97a6f1fb4 100644
--- a/uc-crux-llvm/src/UCCrux/LLVM/Context/Function.hs
+++ b/uc-crux-llvm/src/UCCrux/LLVM/Context/Function.hs
@@ -40,6 +40,7 @@ import           Data.Map (Map)
 import           Data.Monoid (getFirst, First(First))
 import           Data.Text (Text)
 import qualified Data.Text as Text
+import           GHC.Stack (HasCallStack)
 
 import qualified Prettyprinter as PP
 
@@ -120,17 +121,17 @@ ppFunctionContextError =
         ]
     BadMemType _ -> "Bad MemType"
 
-throwFunctionContextError :: FunctionContextError -> a
+-- | Callers should also be annotated with 'HasCallStack'
+throwFunctionContextError :: HasCallStack => FunctionContextError -> a
 throwFunctionContextError err =
   case err of
-    BadMemType {} -> isMalformed
-    BadLift {} -> isMalformed
-    BadLiftArgs {} -> doPanic
+    BadMemType {} -> malformedLLVMModule (PP.pretty prettyErr) []
+    BadLift {} -> malformedLLVMModule (PP.pretty prettyErr) []
+    BadLiftArgs {} -> panic nm [Text.unpack prettyErr]
   where
+    prettyErr = ppFunctionContextError err
     nm = "throwFunctionContextError"
-    doPanic = panic nm [Text.unpack (ppFunctionContextError err)]
-    isMalformed =
-      malformedLLVMModule nm (PP.pretty (ppFunctionContextError err)) []
+
 
 withPtrWidthOf ::
   LLVMTrans.ModuleTranslation arch ->
@@ -145,6 +146,7 @@ withPtrWidthOf trans k =
 -- malformed LLVM module, and are thrown as exceptions.
 makeFunctionContext ::
   forall m arch fullTypes.
+  HasCallStack =>
   ArchOk arch =>
   ModuleContext m arch ->
   DefnSymbol m ->
diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Context/Module.hs b/uc-crux-llvm/src/UCCrux/LLVM/Context/Module.hs
index 1822ac247..30e400ca0 100644
--- a/uc-crux-llvm/src/UCCrux/LLVM/Context/Module.hs
+++ b/uc-crux-llvm/src/UCCrux/LLVM/Context/Module.hs
@@ -40,6 +40,7 @@ where
 import           Control.Lens ((^.), Simple, Getter, Lens, lens, to, at)
 import           Data.Proxy (Proxy(Proxy))
 import           Data.Type.Equality ((:~:)(Refl), testEquality)
+import           GHC.Stack (HasCallStack)
 
 import           Text.LLVM.AST (Symbol(Symbol))
 import qualified Text.LLVM.AST as L
@@ -119,6 +120,7 @@ withTypeContext context computation =
 -- | Any errors encountered in this function are bugs in UC-Crux or results of a
 -- malformed LLVM module, and are thrown as exceptions.
 makeModuleContext ::
+  HasCallStack =>
   ArchOk arch =>
   FilePath ->
   L.Module ->
diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Errors/MalformedLLVMModule.hs b/uc-crux-llvm/src/UCCrux/LLVM/Errors/MalformedLLVMModule.hs
index 08522042b..d3294b992 100644
--- a/uc-crux-llvm/src/UCCrux/LLVM/Errors/MalformedLLVMModule.hs
+++ b/uc-crux-llvm/src/UCCrux/LLVM/Errors/MalformedLLVMModule.hs
@@ -14,6 +14,7 @@ where
 
 {- ORMOLU_DISABLE -}
 import           Data.Void (Void)
+import           GHC.Stack (HasCallStack, prettyCallStack, callStack)
 
 import           Prettyprinter (Doc, pretty)
 
@@ -23,17 +24,18 @@ import qualified Lang.Crucible.LLVM.MalformedLLVMModule as M
 -- | Throw a 'Lang.Crucible.LLVM.MalformedLLVMModule.MalformedLLVMModule'
 -- exception.
 malformedLLVMModule ::
-  -- | Function name
-  String ->
+  HasCallStack =>
   -- | Short explanation
   Doc Void ->
   -- | Details
   [Doc Void] ->
   a
-malformedLLVMModule nm short details =
+malformedLLVMModule short details =
   M.malformedLLVMModule short $
     concat
-      [ [ pretty ("In function: " ++ nm) ]
+      [ [ pretty "Call stack:"
+        , pretty (prettyCallStack callStack)
+        ]
       , details
       , map
           pretty
diff --git a/uc-crux-llvm/src/UCCrux/LLVM/FullType/Translation.hs b/uc-crux-llvm/src/UCCrux/LLVM/FullType/Translation.hs
index e8bb98744..3c9ba81b6 100644
--- a/uc-crux-llvm/src/UCCrux/LLVM/FullType/Translation.hs
+++ b/uc-crux-llvm/src/UCCrux/LLVM/FullType/Translation.hs
@@ -16,7 +16,6 @@ Stability        : provisional
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 
@@ -40,6 +39,7 @@ import           Control.Monad.State (State, runState)
 import           Data.Functor ((<&>))
 import           Data.Proxy (Proxy(Proxy))
 import qualified Data.Map as Map
+import           GHC.Stack (HasCallStack)
 
 import           Prettyprinter (Doc)
 import qualified Prettyprinter as PP
@@ -118,17 +118,17 @@ ppTypeTranslationError =
       FullTypeTranslation (L.Ident ident) ->
         "Couldn't find or couldn't translate type: " <> ident
 
-throwTypeTranslationError :: TypeTranslationError -> a
+-- | Callers should also be annotated with 'HasCallStack'
+throwTypeTranslationError :: HasCallStack => TypeTranslationError -> a
 throwTypeTranslationError err =
   case err of
-    NoCFG {} -> doPanic
-    BadLift {} -> isMalformed
-    BadLiftArgs {} -> doPanic
-    FullTypeTranslation {} -> doPanic
+    NoCFG {} -> panic nm [show prettyErr]
+    BadLift {} -> malformedLLVMModule prettyErr []
+    BadLiftArgs {} -> panic nm [show prettyErr]
+    FullTypeTranslation {} -> panic nm [show prettyErr]
   where
+    prettyErr = (ppTypeTranslationError err)
     nm = "throwTypeTranslationError"
-    doPanic = panic nm [show (ppTypeTranslationError err)]
-    isMalformed = malformedLLVMModule nm (ppTypeTranslationError err) []
 
 
 -- | Precondition: The 'TypeContext' must correspond to the 'L.Module'.
@@ -228,7 +228,7 @@ translateModuleDefines llvmModule trans =
             if isVarArgs
               then removeVarArgsRepr crucibleTypes
               else Some crucibleTypes
-        case testCompatibilityAssign (Proxy @arch) fullTypes crucibleTypes' of
+        case testCompatibilityAssign (Proxy :: Proxy arch) fullTypes crucibleTypes' of
           Just Refl ->
             pure $
               FunctionTypes
@@ -272,7 +272,7 @@ translateModuleDefines llvmModule trans =
             (withExceptT FullTypeTranslation . toFullTypeM)
             (fdRetType liftedDecl)
         SomeAssign' crucibleTypes Refl _ <-
-          pure $ assignmentToCrucibleType (Proxy @arch) fullTypes
+          pure $ assignmentToCrucibleType (Proxy :: Proxy arch) fullTypes
         pure $
           FunctionTypes
             { ftArgTypes = MatchingAssign fullTypes crucibleTypes,