From 141f9959c11b1a215689e67a42dd8d86ba9931a2 Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Fri, 18 Nov 2022 11:21:21 -0800 Subject: [PATCH 1/5] Reset directory on failed file interpretation --- src/SAWScript/Interpreter.hs | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 7046982d4d..6ef8918ad4 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -38,6 +38,7 @@ import Data.Traversable hiding ( mapM ) import Control.Applicative ( (<|>) ) import qualified Control.Exception as X import Control.Monad (unless, (>=>), when) +import Control.Monad.Catch (catch, throwM) import Control.Monad.IO.Class (liftIO) import qualified Data.ByteString as BS import qualified Data.Map as Map @@ -392,9 +393,14 @@ interpretStmt printBinds stmt = 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 + oldPath <- io getCurrentDirectory + backtrack oldPath $ + do { io $ setCurrentDirectory (takeDirectory file) + ; stmts <- io $ SAWScript.Import.loadFile opts file + ; mapM_ stmtWithPrint stmts + ; when runMain interpretMain + ; io $ setCurrentDirectory oldPath + } writeVerificationSummary where stmtWithPrint s = do let withPos str = unlines $ @@ -407,6 +413,12 @@ interpretFile file runMain = do (interpretStmt False s) else interpretStmt False s + backtrack :: FilePath -> TopLevel a -> TopLevel a + backtrack oldPath action = + action + `catch` + (\(e :: X.SomeException) -> io (setCurrentDirectory oldPath) >> throwM e) + -- | Evaluate the value called 'main' from the current environment. interpretMain :: TopLevel () interpretMain = do @@ -520,12 +532,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 +720,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 From 2dedbd701156968bdd1e37c4f7e2e7247476ef35 Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Fri, 2 Dec 2022 15:39:47 -0800 Subject: [PATCH 2/5] Implement `bracketTopLevel` and use it for directory backtracking --- src/SAWScript/Interpreter.hs | 29 +++++++++++------------------ src/SAWScript/Value.hs | 12 +++++++++++- 2 files changed, 22 insertions(+), 19 deletions(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 6ef8918ad4..dc1157dab5 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -38,7 +38,7 @@ import Data.Traversable hiding ( mapM ) import Control.Applicative ( (<|>) ) import qualified Control.Exception as X import Control.Monad (unless, (>=>), when) -import Control.Monad.Catch (catch, throwM) +-- import Control.Monad.Catch (bracket, catch, throwM) import Control.Monad.IO.Class (liftIO) import qualified Data.ByteString as BS import qualified Data.Map as Map @@ -391,18 +391,17 @@ interpretStmt printBinds stmt = putTopLevelRW $ addTypedef (getVal name) ty rw interpretFile :: FilePath -> Bool {- ^ run main? -} -> TopLevel () -interpretFile file runMain = do - opts <- getOptions - oldPath <- io getCurrentDirectory - backtrack oldPath $ - do { io $ setCurrentDirectory (takeDirectory file) - ; stmts <- io $ SAWScript.Import.loadFile opts file - ; mapM_ stmtWithPrint stmts - ; when runMain interpretMain - ; io $ setCurrentDirectory oldPath - } - 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) @@ -413,12 +412,6 @@ interpretFile file runMain = do (interpretStmt False s) else interpretStmt False s - backtrack :: FilePath -> TopLevel a -> TopLevel a - backtrack oldPath action = - action - `catch` - (\(e :: X.SomeException) -> io (setCurrentDirectory oldPath) >> throwM e) - -- | Evaluate the value called 'main' from the current environment. interpretMain :: TopLevel () interpretMain = do diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 70a176c0b6..cab2a33e9a 100644 --- a/src/SAWScript/Value.hs +++ b/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.Monad.Catch.bracket` specialized to `TopLevel`. We +-- can't use the former because it requires `TopLevel` to implement +-- `Control.Monad.Catch.MonadMask`, which it can't do. +bracketTopLevel :: TopLevel a -> (a -> TopLevel c) -> (a -> TopLevel b) -> TopLevel b +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 From f25b8f8ca0c7999df705e0be2e55505075e5d2ab Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Mon, 5 Dec 2022 08:10:06 -0800 Subject: [PATCH 3/5] Apply suggestions from code review Co-authored-by: Ryan Scott --- src/SAWScript/Interpreter.hs | 1 - src/SAWScript/Value.hs | 6 +++--- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index dc1157dab5..ed143ce1ac 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -38,7 +38,6 @@ import Data.Traversable hiding ( mapM ) import Control.Applicative ( (<|>) ) import qualified Control.Exception as X import Control.Monad (unless, (>=>), when) --- import Control.Monad.Catch (bracket, catch, throwM) import Control.Monad.IO.Class (liftIO) import qualified Data.ByteString as BS import qualified Data.Map as Map diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index cab2a33e9a..a70928d243 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -562,9 +562,9 @@ 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.Monad.Catch.bracket` specialized to `TopLevel`. We --- can't use the former because it requires `TopLevel` to implement --- `Control.Monad.Catch.MonadMask`, which it can't do. +-- | A version of 'Control.Monad.Catch.bracket' specialized to 'TopLevel'. We +-- can't use the former because it requires 'TopLevel' to implement +-- 'Control.Monad.Catch.MonadMask', which it can't do. bracketTopLevel :: TopLevel a -> (a -> TopLevel c) -> (a -> TopLevel b) -> TopLevel b bracketTopLevel acquire release action = do resource <- acquire From 59d941be79745afa737f27e19ab174d2a6b1f51f Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Mon, 5 Dec 2022 08:17:14 -0800 Subject: [PATCH 4/5] Refer to first-party `bracket` and mimic its type signature --- src/SAWScript/Value.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index a70928d243..5da9c83644 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -562,10 +562,10 @@ 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.Monad.Catch.bracket' specialized to 'TopLevel'. We --- can't use the former because it requires 'TopLevel' to implement --- 'Control.Monad.Catch.MonadMask', which it can't do. -bracketTopLevel :: TopLevel a -> (a -> TopLevel c) -> (a -> TopLevel b) -> TopLevel b +-- | 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 From 9bdaa23b192d34c1c7a8026a9ed53d55968c0f70 Mon Sep 17 00:00:00 2001 From: Sam Cowger Date: Wed, 21 Dec 2022 15:13:12 -0600 Subject: [PATCH 5/5] Add test --- intTests/test_directory_reset/README.md | 5 +++++ intTests/test_directory_reset/err/err.saw | 1 + intTests/test_directory_reset/test.sh | 11 +++++++++++ 3 files changed, 17 insertions(+) create mode 100644 intTests/test_directory_reset/README.md create mode 100644 intTests/test_directory_reset/err/err.saw create mode 100755 intTests/test_directory_reset/test.sh diff --git a/intTests/test_directory_reset/README.md b/intTests/test_directory_reset/README.md new file mode 100644 index 0000000000..0d512e24c7 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/intTests/test_directory_reset/err/err.saw b/intTests/test_directory_reset/err/err.saw new file mode 100644 index 0000000000..c9c1ddc01d --- /dev/null +++ b/intTests/test_directory_reset/err/err.saw @@ -0,0 +1 @@ +this file probably won't parse diff --git a/intTests/test_directory_reset/test.sh b/intTests/test_directory_reset/test.sh new file mode 100755 index 0000000000..dfed005edf --- /dev/null +++ b/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"$.* ]]