uc-crux-llvm: Use HasCallStack for malformedLLVMModule

GaloisInc · Dec 13, 2021 · 8e81d9a · 8e81d9a
1 parent 4e5ff4d
commit 8e81d9a
Show file tree

Hide file tree

Showing 4 changed files with 27 additions and 21 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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,