uc-crux-llvm: Improve handling of TypeTranslationError

Clarify when it's a UC-Crux bug vs. LLVM bug.
GaloisInc · Dec 13, 2021 · 4e5ff4d · 4e5ff4d
1 parent f9e382c
commit 4e5ff4d
Show file tree

Hide file tree

Showing 4 changed files with 54 additions and 35 deletions.
diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Context/Function.hs b/uc-crux-llvm/src/UCCrux/LLVM/Context/Function.hs
@@ -121,20 +121,16 @@ ppFunctionContextError =
     BadMemType _ -> "Bad MemType"
 
 throwFunctionContextError :: FunctionContextError -> a
-throwFunctionContextError =
-  \case
-    err@(BadMemType {}) ->
-      malformedLLVMModule
-        "loopOnFunction"
-        (PP.pretty (ppFunctionContextError err))
-        []
-    err@(BadLift {}) ->
-      malformedLLVMModule
-        "loopOnFunction"
-        (PP.pretty (ppFunctionContextError err))
-        []
-    err@(BadLiftArgs {}) ->
-      panic "loopOnFunction" [Text.unpack (ppFunctionContextError err)]
+throwFunctionContextError err =
+  case err of
+    BadMemType {} -> isMalformed
+    BadLift {} -> isMalformed
+    BadLiftArgs {} -> doPanic
+  where
+    nm = "throwFunctionContextError"
+    doPanic = panic nm [Text.unpack (ppFunctionContextError err)]
+    isMalformed =
+      malformedLLVMModule nm (PP.pretty (ppFunctionContextError err)) []
 
 withPtrWidthOf ::
   LLVMTrans.ModuleTranslation arch ->

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Context/Module.hs b/uc-crux-llvm/src/UCCrux/LLVM/Context/Module.hs
@@ -63,7 +63,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 +116,26 @@ 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 ::
   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

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/FullType/Translation.hs b/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
 
@@ -40,6 +41,9 @@ import           Data.Functor ((<&>))
 import           Data.Proxy (Proxy(Proxy))
 import qualified Data.Map as Map
 
+import           Prettyprinter (Doc)
+import qualified Prettyprinter as PP
+
 import qualified Text.LLVM.AST as L
 
 import qualified Data.Parameterized.Context as Ctx
@@ -55,6 +59,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 +107,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
+
+throwTypeTranslationError :: TypeTranslationError -> a
+throwTypeTranslationError err =
+  case err of
+    NoCFG {} -> doPanic
+    BadLift {} -> isMalformed
+    BadLiftArgs {} -> doPanic
+    FullTypeTranslation {} -> doPanic
+  where
+    nm = "throwTypeTranslationError"
+    doPanic = panic nm [show (ppTypeTranslationError err)]
+    isMalformed = malformedLLVMModule nm (ppTypeTranslationError err) []
+
 
 -- | Precondition: The 'TypeContext' must correspond to the 'L.Module'.
 translateModuleDefines ::

diff --git a/uc-crux-llvm/src/UCCrux/LLVM/Main.hs b/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)
             )
       )