Reset directory on failed file interpretation

intTests/test_directory_reset/README.md

@@ -0,0 +1,5 @@
+Test that a failed `include` leaves the current working directory, as printed by
+`:pwd`, unchanged. Do this by `include`ing a bogus file outside the current
+directory, bracketed with calls to `:pwd`, making sure that those calls produce
+identical output, and that that output is the same as the initial working
+directory.

intTests/test_directory_reset/err/err.saw

@@ -0,0 +1 @@
+this file probably won't parse

intTests/test_directory_reset/test.sh

@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+
+set -e
+
+HERE=`pwd`
+RES=`printf '%s\n%s\n%s\n' ':pwd' 'include "err/err.saw"' ':pwd' | \
+    $SAW --interactive --no-color | \
+    sed -r '/^\s*$/d' | \
+    sort | \
+    uniq -d`
+[[ "$RES" =~ .*"$HERE"$.* ]]

src/SAWScript/Interpreter.hs

@@ -390,13 +390,17 @@ interpretStmt printBinds stmt =
          putTopLevelRW $ addTypedef (getVal name) ty rw
 
 interpretFile :: FilePath -> Bool {- ^ run main? -} -> TopLevel ()
-interpretFile file runMain = do
-  opts <- getOptions
-  stmts <- io $ SAWScript.Import.loadFile opts file
-  mapM_ stmtWithPrint stmts
-  when runMain interpretMain
-  writeVerificationSummary
+interpretFile file runMain = 
+  bracketTopLevel (io getCurrentDirectory) (io . setCurrentDirectory) (const interp)
   where
+    interp = 
+      do  opts <- getOptions
+          io $ setCurrentDirectory (takeDirectory file)
+          stmts <- io $ SAWScript.Import.loadFile opts file
+          mapM_ stmtWithPrint stmts
+          when runMain interpretMain
+          writeVerificationSummary
+
     stmtWithPrint s = do let withPos str = unlines $
                                            ("[output] at " ++ show (SS.getPos s) ++ ": ") :
                                              map (\l -> "\t"  ++ l) (lines str)
@@ -520,12 +524,9 @@ processFile proxy opts file mbSubshell mbProofSubshell = do
   let ro'' = case mbProofSubshell of
               Nothing -> ro'
               Just m  -> ro'{ roProofSubshell = m }
-  oldpath <- getCurrentDirectory
   file' <- canonicalizePath file
-  setCurrentDirectory (takeDirectory file')
   _ <- runTopLevel (interpretFile file' True) ro'' rw
             `X.catch` (handleException opts)
-  setCurrentDirectory oldpath
   return ()
 
 -- Primitives ------------------------------------------------------------------
@@ -711,11 +712,8 @@ set_crucible_timeout t = do
 
 include_value :: FilePath -> TopLevel ()
 include_value file = do
-  oldpath <- io $ getCurrentDirectory
   file' <- io $ canonicalizePath file
-  io $ setCurrentDirectory (takeDirectory file')
   interpretFile file' False
-  io $ setCurrentDirectory oldpath
 
 set_ascii :: Bool -> TopLevel ()
 set_ascii b = do

src/SAWScript/Value.hs

@@ -37,7 +37,7 @@ import Control.Applicative (Applicative)
 #endif
 import Control.Lens
 import Control.Monad.Fail (MonadFail(..))
-import Control.Monad.Catch (MonadThrow(..), MonadCatch(..), catches, Handler(..))
+import Control.Monad.Catch (MonadThrow(..), MonadCatch(..), catches, Handler(..), try)
 import Control.Monad.Except (ExceptT(..), runExceptT, MonadError(..))
 import Control.Monad.Reader (MonadReader)
 import qualified Control.Exception as X
@@ -562,6 +562,16 @@ runTopLevel :: IsValue a => TopLevel a -> TopLevelRO -> TopLevelRW -> IO (Value,
 runTopLevel (TopLevel_ m) ro rw =
   runStateContT (runReaderT m ro) (\a s -> return (toValue a,s)) rw
 
+-- | A version of 'Control.Exception.bracket' specialized to 'TopLevel'. We
+-- can't use 'Control.Monad.Catch.bracket' because it requires 'TopLevel' to
+-- implement 'Control.Monad.Catch.MonadMask', which it can't do.
+bracketTopLevel :: TopLevel a -> (a -> TopLevel b) -> (a -> TopLevel c) -> TopLevel c
+bracketTopLevel acquire release action =
+  do  resource <- acquire
+      try (action resource) >>= \case
+        Left (bad :: X.SomeException) -> release resource >> throwM bad
+        Right good -> release resource >> pure good
+
 instance MonadIO TopLevel where
   liftIO = io