Merge pull request #939 from langston-barrett/lb/malformed-llvm-module

uc-crux-llvm: Improve error handling in cases of a malformed LLVM module

uc-crux-llvm/src/UCCrux/LLVM/Context/Function.hs

@@ -17,9 +17,11 @@ Stability    : provisional
 
 module UCCrux.LLVM.Context.Function
   ( FunctionContext (..),
-    FunctionContextError (..),
+    FunctionContextError,
     ppFunctionContextError,
+    throwFunctionContextError,
     makeFunctionContext,
+    tryMakeFunctionContext,
     functionName,
     argumentNames,
     argumentCrucibleTypes,
@@ -38,6 +40,9 @@ 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
 
 import qualified Text.LLVM.AST as L
 
@@ -53,6 +58,8 @@ import qualified Lang.Crucible.LLVM.Translation as LLVMTrans
 import           Crux.LLVM.Overrides (ArchOk)
 
 import           UCCrux.LLVM.Context.Module (ModuleContext, withTypeContext, llvmModule, moduleTranslation)
+import           UCCrux.LLVM.Errors.MalformedLLVMModule (malformedLLVMModule)
+import           UCCrux.LLVM.Errors.Panic (panic)
 import           UCCrux.LLVM.Errors.Unimplemented (unimplemented, Unimplemented(VarArgsFunction))
 import           UCCrux.LLVM.FullType.Type (FullType, FullTypeRepr, MapToCrucibleType)
 import           UCCrux.LLVM.Module (DefnSymbol, defnSymbol, getDefnSymbol, moduleDefnMap, getModule)
@@ -88,9 +95,7 @@ argumentStorageTypes :: Simple Lens (FunctionContext m arch argTypes) (Ctx.Assig
 argumentStorageTypes = lens _argumentStorageTypes (\s v -> s {_argumentStorageTypes = v})
 
 data FunctionContextError
-  = -- | Couldn't find 'L.Define' of entrypoint
-    MissingEntrypoint Text
-  | -- | Couldn't lift types in declaration to 'MemType'
+  = -- | Couldn't lift types in declaration to 'MemType'
     BadLift Text
   | -- | Wrong number of arguments after lifting declaration
     BadLiftArgs !Int !Int !Int
@@ -100,7 +105,6 @@ data FunctionContextError
 ppFunctionContextError :: FunctionContextError -> Text
 ppFunctionContextError =
   \case
-    MissingEntrypoint name -> "Couldn't find definition of function " <> name
     BadLift name -> "Couldn't lift argument/return types to MemTypes for " <> name
     BadLiftArgs decl tys idx ->
       Text.unwords
@@ -117,24 +121,52 @@ ppFunctionContextError =
         ]
     BadMemType _ -> "Bad MemType"
 
+-- | Callers should also be annotated with 'HasCallStack'
+throwFunctionContextError :: HasCallStack => FunctionContextError -> a
+throwFunctionContextError err =
+  case err of
+    BadMemType {} -> malformedLLVMModule (PP.pretty prettyErr) []
+    BadLift {} -> malformedLLVMModule (PP.pretty prettyErr) []
+    BadLiftArgs {} -> panic nm [Text.unpack prettyErr]
+  where
+    prettyErr = ppFunctionContextError err
+    nm = "throwFunctionContextError"
+
+
 withPtrWidthOf ::
   LLVMTrans.ModuleTranslation arch ->
   (ArchOk arch => b) ->
   b
 withPtrWidthOf trans k =
   LLVMTrans.llvmPtrWidth (trans ^. LLVMTrans.transContext) (\ptrW -> withPtrWidth ptrW k)
 
--- | This function does some precomputation of ubiquitously used values, and
--- some handling of what should generally be very rare errors.
+-- | This function does some precomputation of ubiquitously used values.
+--
+-- Any errors encountered in this process are bugs in UC-Crux or results of a
+-- malformed LLVM module, and are thrown as exceptions.
 makeFunctionContext ::
   forall m arch fullTypes.
+  HasCallStack =>
   ArchOk arch =>
   ModuleContext m arch ->
   DefnSymbol m ->
   Ctx.Assignment (FullTypeRepr m) fullTypes ->
   Ctx.Assignment CrucibleTypes.TypeRepr (MapToCrucibleType arch fullTypes) ->
-  Either FunctionContextError (FunctionContext m arch fullTypes)
+  FunctionContext m arch fullTypes
 makeFunctionContext modCtx defnSymb argFullTypes argTypes =
+  case tryMakeFunctionContext modCtx defnSymb argFullTypes argTypes of
+    Left err -> throwFunctionContextError err
+    Right funCtx -> funCtx
+
+tryMakeFunctionContext ::
+  forall m arch fullTypes.
+  ArchOk arch =>
+  ModuleContext m arch ->
+  DefnSymbol m ->
+  Ctx.Assignment (FullTypeRepr m) fullTypes ->
+  Ctx.Assignment CrucibleTypes.TypeRepr (MapToCrucibleType arch fullTypes) ->
+  Either FunctionContextError (FunctionContext m arch fullTypes)
+tryMakeFunctionContext modCtx defnSymb argFullTypes argTypes =
   do
     let llvmMod = modCtx ^. llvmModule
     let L.Symbol strName = getDefnSymbol defnSymb

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
@@ -63,7 +64,7 @@ import           UCCrux.LLVM.Errors.Panic (panic)
 import           UCCrux.LLVM.Errors.Unimplemented (unimplemented)
 import qualified UCCrux.LLVM.Errors.Unimplemented as Unimplemented
 import           UCCrux.LLVM.FullType.CrucibleType (testCompatibility)
-import           UCCrux.LLVM.FullType.Translation (TranslatedTypes(..), TypeTranslationError, FunctionTypes(..), MatchingAssign(..), translateModuleDefines)
+import           UCCrux.LLVM.FullType.Translation (TranslatedTypes(..), TypeTranslationError, FunctionTypes(..), MatchingAssign(..), translateModuleDefines, throwTypeTranslationError)
 import           UCCrux.LLVM.FullType.Type (FullTypeRepr, ModuleTypes, MapToCrucibleType)
 import           UCCrux.LLVM.FullType.ReturnType (ReturnType(..), ReturnTypeToCrucibleType)
 import           UCCrux.LLVM.FullType.VarArgs (VarArgsRepr, varArgsReprToBool)
@@ -116,13 +117,27 @@ withTypeContext context computation =
   let ?lc = context ^. moduleTranslation . LLVMTrans.transContext . LLVMTrans.llvmTypeCtx
    in 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 ->
   ModuleTranslation arch ->
-  Either TypeTranslationError (SomeModuleContext arch)
+  SomeModuleContext arch
 makeModuleContext path llvmMod trans =
+  case tryMakeModuleContext path llvmMod trans of
+    Left err -> throwTypeTranslationError err
+    Right modCtx -> modCtx
+
+tryMakeModuleContext ::
+  ArchOk arch =>
+  FilePath ->
+  L.Module ->
+  ModuleTranslation arch ->
+  Either TypeTranslationError (SomeModuleContext arch)
+tryMakeModuleContext path llvmMod trans =
   let ?lc = trans ^. LLVMTrans.transContext . LLVMTrans.llvmTypeCtx
    in case translateModuleDefines llvmMod trans of
         Left err -> Left err

uc-crux-llvm/src/UCCrux/LLVM/Errors/MalformedLLVMModule.hs

@@ -0,0 +1,48 @@
+{-
+Module       : UCCrux.LLVM.Errors.MalformedLLVMModule
+Description  : Problems with the (our assumptions about) the input program(s)
+Copyright    : (c) Galois, Inc 2021
+License      : BSD3
+Maintainer   : Langston Barrett <[email protected]>
+Stability    : provisional
+-}
+
+module UCCrux.LLVM.Errors.MalformedLLVMModule
+  ( malformedLLVMModule,
+  )
+where
+
+{- ORMOLU_DISABLE -}
+import           Data.Void (Void)
+import           GHC.Stack (HasCallStack, prettyCallStack, callStack)
+
+import           Prettyprinter (Doc, pretty)
+
+import qualified Lang.Crucible.LLVM.MalformedLLVMModule as M
+{- ORMOLU_ENABLE -}
+
+-- | Throw a 'Lang.Crucible.LLVM.MalformedLLVMModule.MalformedLLVMModule'
+-- exception.
+malformedLLVMModule ::
+  HasCallStack =>
+  -- | Short explanation
+  Doc Void ->
+  -- | Details
+  [Doc Void] ->
+  a
+malformedLLVMModule short details =
+  M.malformedLLVMModule short $
+    concat
+      [ [ pretty "Call stack:"
+        , pretty (prettyCallStack callStack)
+        ]
+      , details
+      , map
+          pretty
+          [ "This is either a bug in the compiler that produced the LLVM module",
+            "or in UC-Crux's assumptions about the form of valid LLVM modules.",
+            "Try running `opt -disable-output -verify < your-module.bc`.",
+            "If opt reports no problems, please report this error here:",
+            "https://github.com/GaloisInc/crucible/issues"
+          ]
+      ]

uc-crux-llvm/src/UCCrux/LLVM/FullType/Translation.hs

@@ -24,9 +24,10 @@ module UCCrux.LLVM.FullType.Translation
   ( FunctionTypes (..),
     MatchingAssign (..),
     TranslatedTypes (..),
-    TypeTranslationError (..),
+    TypeTranslationError,
     translateModuleDefines,
     ppTypeTranslationError,
+    throwTypeTranslationError,
   )
 where
 
@@ -39,6 +40,10 @@ 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
 
 import qualified Text.LLVM.AST as L
 
@@ -55,6 +60,7 @@ import qualified Lang.Crucible.LLVM.Translation as LLVMTrans
 import           Lang.Crucible.LLVM.TypeContext (TypeContext)
 
 import           Crux.LLVM.Overrides (ArchOk)
+import           UCCrux.LLVM.Errors.MalformedLLVMModule (malformedLLVMModule)
 import           UCCrux.LLVM.Errors.Panic (panic)
 import           UCCrux.LLVM.FullType.CrucibleType (SomeAssign'(..), testCompatibilityAssign, assignmentToCrucibleType)
 import           UCCrux.LLVM.FullType.Type
@@ -102,15 +108,29 @@ data TypeTranslationError
     BadLiftArgs !L.Symbol
   | FullTypeTranslation L.Ident
 
-ppTypeTranslationError :: TypeTranslationError -> String
+ppTypeTranslationError :: TypeTranslationError -> Doc ann
 ppTypeTranslationError =
-  \case
-    NoCFG (L.Symbol name) -> "Couldn't find definition of function " <> name
-    BadLift name -> "Couldn't lift argument/return types to MemTypes for " <> name
-    BadLiftArgs (L.Symbol name) ->
-      "Wrong number of arguments after lifting declaration of " <> name
-    FullTypeTranslation (L.Ident ident) ->
-      "Couldn't find or couldn't translate type: " <> ident
+  PP.pretty .
+    \case
+      NoCFG (L.Symbol name) -> "Couldn't find definition of function " <> name
+      BadLift name -> "Couldn't lift argument/return types to MemTypes for " <> name
+      BadLiftArgs (L.Symbol name) ->
+        "Wrong number of arguments after lifting declaration of " <> name
+      FullTypeTranslation (L.Ident ident) ->
+        "Couldn't find or couldn't translate type: " <> ident
+
+-- | Callers should also be annotated with 'HasCallStack'
+throwTypeTranslationError :: HasCallStack => TypeTranslationError -> a
+throwTypeTranslationError err =
+  case err of
+    NoCFG {} -> panic nm [show prettyErr]
+    BadLift {} -> malformedLLVMModule prettyErr []
+    BadLiftArgs {} -> panic nm [show prettyErr]
+    FullTypeTranslation {} -> panic nm [show prettyErr]
+  where
+    prettyErr = ppTypeTranslationError err
+    nm = "throwTypeTranslationError"
+
 
 -- | Precondition: The 'TypeContext' must correspond to the 'L.Module'.
 translateModuleDefines ::

uc-crux-llvm/src/UCCrux/LLVM/Main.hs

@@ -85,8 +85,6 @@ import           UCCrux.LLVM.Context.App (AppContext)
 import           UCCrux.LLVM.Context.Module (ModuleContext, SomeModuleContext(..), makeModuleContext, defnTypes, withModulePtrWidth)
 import           UCCrux.LLVM.Equivalence (checkEquiv)
 import qualified UCCrux.LLVM.Equivalence.Config as EqConfig
-import           UCCrux.LLVM.Errors.Panic (panic)
-import           UCCrux.LLVM.FullType.Translation (ppTypeTranslationError)
 import qualified UCCrux.LLVM.Logging as Log
 import qualified UCCrux.LLVM.Main.Config.FromEnv as Config.FromEnv
 import           UCCrux.LLVM.Main.Config.Type (TopLevelConfig)
@@ -237,14 +235,7 @@ translateLLVMModule llOpts halloc memVar moduleFilePath llvmMod =
           withPtrWidth
             ptrW
             ( case makeModuleContext moduleFilePath llvmMod trans of
-                Left err ->
-                  panic
-                    "translateLLVMModule"
-                    [ "Type translation failed",
-                      ppTypeTranslationError err
-                    ]
-                Right (SomeModuleContext modCtx) ->
-                  pure (SomeModuleContext' modCtx)
+                SomeModuleContext modCtx -> pure (SomeModuleContext' modCtx)
             )
       )
 

uc-crux-llvm/src/UCCrux/LLVM/Run/Check.hs

@@ -35,7 +35,6 @@ import qualified Data.IORef as IORef
 import           Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import           Data.Maybe (catMaybes)
-import qualified Data.Text as Text
 import           Data.Traversable (for)
 import           Data.Type.Equality ((:~:)(Refl), testEquality)
 
@@ -73,7 +72,7 @@ import           UCCrux.LLVM.Constraints (Constraints, emptyConstraints, ppConst
 import           UCCrux.LLVM.Cursor (ppSelector)
 import           UCCrux.LLVM.Context.App (AppContext)
 import           UCCrux.LLVM.Context.Module (ModuleContext, CFGWithTypes(..), findFun)
-import           UCCrux.LLVM.Context.Function (FunctionContext, makeFunctionContext, ppFunctionContextError, argumentFullTypes)
+import           UCCrux.LLVM.Context.Function (FunctionContext, makeFunctionContext, argumentFullTypes)
 import           UCCrux.LLVM.Errors.Panic (panic)
 import           UCCrux.LLVM.FullType (FullType, FullTypeRepr, MapToCrucibleType)
 import qualified UCCrux.LLVM.FullType.CrucibleType as FT
@@ -201,15 +200,7 @@ checkInferredContracts appCtx modCtx funCtx halloc cruxOpts llOpts constraints c
            do CFGWithTypes ovCfg argFTys _retTy _varArgs <-
                 pure (findFun modCtx (FuncDefnSymbol func))
               let argCTys = Crucible.cfgArgTypes ovCfg
-              ovFunCtx <-
-                case makeFunctionContext modCtx func argFTys argCTys of
-                  Left err ->
-                    panic
-                      "checkInferredContracts"
-                      [ "Function: " ++ defnSymbolToString func
-                      , Text.unpack (ppFunctionContextError err)
-                      ]
-                  Right funCtx' -> return funCtx'
+              let ovFunCtx = makeFunctionContext modCtx func argFTys argCTys
               let ?memOpts = CruxLLVM.memOpts llOpts
               case testEquality argFTys types of
                 Nothing ->
@@ -261,13 +252,8 @@ checkInferredContractsFromEntryPoints appCtx modCtx halloc cruxOpts llOpts entri
         do CFGWithTypes cfg argFTys _retTy _varArgs <-
              pure (findFun modCtx (FuncDefnSymbol entry))
 
-           funCtx <-
-             case makeFunctionContext modCtx entry argFTys (Crucible.cfgArgTypes cfg) of
-               Left err ->
-                 panic
-                   "checkInferredContracts"
-                   [Text.unpack (ppFunctionContextError err)]
-               Right funCtxF -> return funCtxF
+           let funCtx =
+                 makeFunctionContext modCtx entry argFTys (Crucible.cfgArgTypes cfg)
            result <-
             checkInferredContracts
               appCtx

uc-crux-llvm/src/UCCrux/LLVM/Run/Loop.hs

@@ -65,7 +65,7 @@ import           UCCrux.LLVM.Classify.Types (Located(locatedValue), Explanation,
 import           UCCrux.LLVM.Constraints (Constraints, NewConstraint, ppConstraints, emptyConstraints, addConstraint, ppExpansionError)
 import           UCCrux.LLVM.Newtypes.FunctionName (FunctionName, functionNameToString, functionNameFromString)
 import           UCCrux.LLVM.Context.App (AppContext, log)
-import           UCCrux.LLVM.Context.Function (FunctionContext, argumentFullTypes, makeFunctionContext, functionName, ppFunctionContextError)
+import           UCCrux.LLVM.Context.Function (FunctionContext, argumentFullTypes, makeFunctionContext, functionName)
 import           UCCrux.LLVM.Context.Module (ModuleContext, moduleTranslation, CFGWithTypes(..), findFun, llvmModule, defnTypes)
 import           UCCrux.LLVM.Errors.Panic (panic)
 import           UCCrux.LLVM.Errors.Unimplemented (Unimplemented, catchUnimplemented)
@@ -237,20 +237,18 @@ loopOnFunction appCtx modCtx halloc cruxOpts llOpts fn =
             ( do
                 CFGWithTypes cfg argFTys _retTy _varArgs <-
                   pure (findFun modCtx (FuncDefnSymbol fn))
-                case makeFunctionContext modCtx fn argFTys (Crucible.cfgArgTypes cfg) of
-                  Left err -> panic "loopOnFunction" [Text.unpack (ppFunctionContextError err)]
-                  Right funCtx ->
-                    do
-                      (appCtx ^. log) Hi $ "Checking function " <> (funCtx ^. functionName)
-                      uncurry (SomeBugfindingResult argFTys)
-                        <$> bugfindingLoop
-                          appCtx
-                          modCtx
-                          funCtx
-                          cfg
-                          cruxOpts
-                          llOpts
-                          halloc
+                let funCtx =
+                      makeFunctionContext modCtx fn argFTys (Crucible.cfgArgTypes cfg)
+                (appCtx ^. log) Hi $ "Checking function " <> (funCtx ^. functionName)
+                uncurry (SomeBugfindingResult argFTys)
+                  <$> bugfindingLoop
+                    appCtx
+                    modCtx
+                    funCtx
+                    cfg
+                    cruxOpts
+                    llOpts
+                    halloc
             )
       )