Skip to content

Commit

Permalink
Prevent the REPL from grabbing and printing exceptions it should
Browse files Browse the repository at this point in the history
be leaving alone (async and exit exceptions).
  • Loading branch information
robdockins committed Apr 22, 2022
1 parent 999bf5b commit 28cc62f
Show file tree
Hide file tree
Showing 2 changed files with 12 additions and 3 deletions.
4 changes: 3 additions & 1 deletion saw/SAWScript/REPL/Command.hs
Original file line number Diff line number Diff line change
Expand Up @@ -39,7 +39,9 @@ import SAWScript.Position (getPos)
import Cryptol.Parser (ParseError())
import Cryptol.Utils.PP hiding ((</>))

import Control.Exception (displayException)
import Control.Monad (guard)

import Data.Char (isSpace,isPunctuation,isSymbol)
import Data.Function (on)
import Data.List (intercalate)
Expand Down Expand Up @@ -146,7 +148,7 @@ runCommand c = case c of
`SAWScript.REPL.Monad.catchOther` handlerPrint
where
handlerPP re = io (putStrLn "" >> print (pp re))
handlerPrint e = io (putStrLn "" >> print e)
handlerPrint e = io (putStrLn "" >> putStrLn (displayException e))
handlerFail s = io (putStrLn "" >> putStrLn s)

Unknown cmd -> io (putStrLn ("Unknown command: " ++ cmd))
Expand Down
11 changes: 9 additions & 2 deletions saw/SAWScript/REPL/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ Stability : provisional
{-# LANGUAGE CPP #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}

module SAWScript.REPL.Monad (
Expand Down Expand Up @@ -76,6 +77,7 @@ import Data.Typeable (Typeable)
import System.Console.ANSI (setTitle)
import qualified Control.Exception as X
import System.IO.Error (isUserError, ioeGetErrorString)
import System.Exit (ExitCode)

import Verifier.SAW.SharedTerm (Term)
import Verifier.SAW.CryptolEnv
Expand Down Expand Up @@ -238,9 +240,14 @@ catchFail m k = REPL (\ ref -> X.catchJust sel (unREPL m ref) (\s -> unREPL (k s
sel e | isUserError e = Just (ioeGetErrorString e)
| otherwise = Nothing

-- | Handle any other exception
-- | Handle any other exception (except that we ignore async exceptions and exitWith)
catchOther :: REPL a -> (X.SomeException -> REPL a) -> REPL a
catchOther = catchEx
catchOther m k = REPL (\ref -> X.catchJust flt (unREPL m ref) (\s -> unREPL (k s) ref))
where
flt e
| Just (_ :: X.AsyncException) <- X.fromException e = Nothing
| Just (_ :: ExitCode) <- X.fromException e = Nothing
| otherwise = Just e

rethrowEvalError :: IO a -> IO a
rethrowEvalError m = run `X.catch` rethrow
Expand Down

0 comments on commit 28cc62f

Please sign in to comment.