From 52f3afbfa049c0ced79fa73d3bb98b5462714f45 Mon Sep 17 00:00:00 2001
From: Aaron Tomb <atomb@galois.com>
Date: Mon, 19 Apr 2021 09:18:57 -0700
Subject: [PATCH] Handle x86 errors more gracefully

And provide a template for catching other varieties of exception more
consistently.
---
 src/SAWScript/Crucible/LLVM/X86.hs |  6 +++---
 src/SAWScript/Value.hs             | 15 +++++++++++++--
 src/SAWScript/X86.hs               |  7 +++++--
 3 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
index e9aee747c7..6d1eafd3af 100644
--- a/src/SAWScript/Crucible/LLVM/X86.hs
+++ b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -321,7 +321,7 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se
       liftIO $ sawRegisterSymFunInterp sawst (Macaw.fnShaMaj sfs) $ cryptolUninterpreted cenv "Maj"
 
       let preserved = Set.fromList . catMaybes $ stringToReg . Text.toLower . Text.pack <$> rwPreservedRegs rw
-      (C.SomeCFG cfg, elf, relf, addr, cfgs) <- liftIO $ buildCFG opts halloc preserved path nm
+      (C.SomeCFG cfg, elf, relf, addr, cfgs) <- io $ buildCFG opts halloc preserved path nm
       addrInt <- if Macaw.segmentBase (Macaw.segoffSegment addr) == 0
         then pure . toInteger $ Macaw.segmentOffset (Macaw.segoffSegment addr) + Macaw.segoffOffset addr
         else fail $ mconcat ["Address of \"", nm, "\" is not an absolute address"]
@@ -352,9 +352,9 @@ llvm_verify_x86 (Some (llvmModule :: LLVMModule x)) path nm globsyms checkSat se
 
       let ?lc = modTrans llvmModule ^. C.LLVM.transContext . C.LLVM.llvmTypeCtx
 
-      emptyState <- liftIO $ initialState sym opts sc cc elf relf methodSpec globsyms maxAddr
+      emptyState <- io $ initialState sym opts sc cc elf relf methodSpec globsyms maxAddr
       balign <- integerToAlignment $ rwStackBaseAlign rw
-      (env, preState) <- liftIO . runX86Sim emptyState $ setupMemory globsyms balign
+      (env, preState) <- io . runX86Sim emptyState $ setupMemory globsyms balign
 
       let
         funcLookup = Macaw.LookupFunctionHandle $ \st _mem regs -> do
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index 78db76a374..a237221cbe 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -37,7 +37,8 @@ import Control.Applicative (Applicative)
 #endif
 import Control.Lens
 import Control.Monad.Fail (MonadFail(..))
-import Control.Monad.Catch (MonadThrow(..), MonadMask(..), MonadCatch(..))
+import Control.Monad.Catch (MonadThrow(..), MonadMask(..),
+                            MonadCatch(..), catches, Handler(..))
 import Control.Monad.Except (ExceptT(..), runExceptT, MonadError(..))
 import Control.Monad.Reader (MonadReader)
 import qualified Control.Exception as X
@@ -75,6 +76,7 @@ import SAWScript.Options (Options(printOutFn),printOutLn,Verbosity)
 import SAWScript.Proof
 import SAWScript.Prover.SolverStats
 import SAWScript.Crucible.LLVM.Skeleton
+import SAWScript.X86 (X86Unsupported(..), X86Error(..))
 
 import Verifier.SAW.Name (toShortName)
 import Verifier.SAW.CryptolEnv as CEnv
@@ -423,7 +425,16 @@ runTopLevel :: TopLevel a -> TopLevelRO -> TopLevelRW -> IO (a, TopLevelRW)
 runTopLevel (TopLevel m) ro rw = runStateT (runReaderT m ro) rw
 
 io :: IO a -> TopLevel a
-io = liftIO
+io f = liftIO f
+       `catches`
+       [ Handler (\(ex :: X86Unsupported) -> handleX86Unsupported ex)
+       , Handler (\(ex :: X86Error) -> handleX86Error ex)
+       ]
+  where
+    handleX86Unsupported (X86Unsupported s) =
+      throwTopLevel $ "Unsupported x86 feature: " ++ s
+    handleX86Error (X86Error s) =
+      throwTopLevel $ "Error in x86 code: " ++ s
 
 throwTopLevel :: String -> TopLevel a
 throwTopLevel msg = do
diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs
index f2a970d502..940ff8fbb0 100644
--- a/src/SAWScript/X86.hs
+++ b/src/SAWScript/X86.hs
@@ -264,8 +264,11 @@ getElf path =
        Right (Elf.SomeElf hdr)
          | Elf.ELFCLASS64 <- Elf.headerClass (Elf.header hdr) -> pure hdr
          | otherwise -> unsupported "32-bit ELF format"
-       Left _ -> malformed "Invalid ELF header"
-
+       Left (off, msg) -> malformed $ mconcat [ "Invalid ELF header at offset "
+                                              , show off
+                                              , ": "
+                                              , msg
+                                              ]
 
 
 -- | Extract a Macaw "memory" from an ELF file and resolve symbols.