From aade9586e0dc476bd20342df9c9e6ee0417a4bbe Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 21 Apr 2022 09:35:41 -0700 Subject: [PATCH 01/14] Reimplement the `TopLevel` monad based on the StateContT transformer, which gives us the ability to capture continuations. This allows us to implement `callcc` as a saw-script command. Additionally, implement a "checkpoint" command that will capture the TopLevel monad state and allow it to be restored later. Also, rework some aspects of error handling. The previous method no longer worked properly with a continuation-based TopLevel monad. --- intTests/test_external_abc/test.saw | 4 +- saw-remote-api/src/SAWServer/TopLevel.hs | 15 +-- saw/SAWScript/REPL/Command.hs | 8 +- src/SAWScript/Builtins.hs | 22 ++-- src/SAWScript/Exceptions.hs | 5 +- src/SAWScript/Interpreter.hs | 38 +++++- src/SAWScript/Prover/Exporter.hs | 9 +- src/SAWScript/Value.hs | 147 +++++++++++++---------- 8 files changed, 156 insertions(+), 92 deletions(-) diff --git a/intTests/test_external_abc/test.saw b/intTests/test_external_abc/test.saw index b735c92df5..51a0ec92c8 100644 --- a/intTests/test_external_abc/test.saw +++ b/intTests/test_external_abc/test.saw @@ -44,8 +44,8 @@ let order_res = {{ ([[0x02,0x03],[0x04,0x05]], 0x81050fff) }}; // Check that Verilog counterexamples are in the right order sr1 <- sat w4_abc_verilog order_term; -caseSatResult sr1 undefined (\t -> prove_print yices {{ t == order_res }}); +caseSatResult sr1 (fail "ABC verilog sat fail") (\t -> prove_print yices {{ t == order_res }}); // Check that AIGER counterexamples are in the right order sr2 <- sat w4_abc_aiger order_term; -caseSatResult sr2 undefined (\t -> prove_print yices {{ t == order_res }}); +caseSatResult sr2 (fail "ABC aiger sat fail") (\t -> prove_print yices {{ t == order_res }}); diff --git a/saw-remote-api/src/SAWServer/TopLevel.hs b/saw-remote-api/src/SAWServer/TopLevel.hs index 780f8ef0ef..5999a1c34c 100644 --- a/saw-remote-api/src/SAWServer/TopLevel.hs +++ b/saw-remote-api/src/SAWServer/TopLevel.hs @@ -5,10 +5,9 @@ module SAWServer.TopLevel (tl) where import Control.Exception ( try, SomeException(..) ) import Control.Lens ( view, set ) import Control.Monad.State ( MonadIO(liftIO) ) -import Data.IORef import Data.Typeable (cast) -import SAWScript.Value ( TopLevel, runTopLevel ) +import SAWScript.Value ( TopLevel, runTopLevel, IsValue(..), FromValue(..) ) import qualified Argo import CryptolServer.Exceptions (cryptolError) @@ -16,20 +15,18 @@ import SAWServer ( SAWState, sawTopLevelRO, sawTopLevelRW ) import SAWServer.CryptolExpression (CryptolModuleException(..)) import SAWServer.Exceptions ( verificationException ) -tl :: TopLevel a -> Argo.Command SAWState a +tl :: (FromValue a, IsValue a) => TopLevel a -> Argo.Command SAWState a tl act = do st <- Argo.getState let ro = view sawTopLevelRO st rw = view sawTopLevelRW st - ref <- liftIO (newIORef rw) - liftIO (try (runTopLevel act ro ref)) >>= + liftIO (try (runTopLevel act ro rw)) >>= \case Left e@(SomeException e') | Just (CryptolModuleException err warnings) <- cast e' -> Argo.raise (cryptolError err warnings) | otherwise -> Argo.raise (verificationException e) - Right res -> - do rw' <- liftIO (readIORef ref) - Argo.modifyState $ set sawTopLevelRW rw' - return res + Right (res, rw') -> + do Argo.modifyState $ set sawTopLevelRW rw' + return (fromValue res) diff --git a/saw/SAWScript/REPL/Command.hs b/saw/SAWScript/REPL/Command.hs index 9b5d2fa6c1..aaedba4f62 100644 --- a/saw/SAWScript/REPL/Command.hs +++ b/saw/SAWScript/REPL/Command.hs @@ -30,6 +30,8 @@ module SAWScript.REPL.Command ( --import Verifier.SAW.SharedTerm (SharedContext) +import Data.IORef + import SAWScript.REPL.Monad import SAWScript.REPL.Trie import SAWScript.Position (getPos) @@ -228,8 +230,10 @@ sawScriptCmd str = do Left err -> io $ print err Right stmt -> do ro <- getTopLevelRO - rwRef <- getEnvironmentRef - io $ runTopLevel (interpretStmt True stmt) ro rwRef + ref <- getEnvironmentRef + rw <- io $ readIORef ref + (_, rw') <- io $ runTopLevel (interpretStmt True stmt) ro rw + io $ writeIORef ref rw' replFileName :: String replFileName = "" diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 9402c1d3f1..bf1b981837 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -208,11 +208,13 @@ readSBV path unintlst = -- support for latches in the 'AIGNetwork' SAWScript type. dsecPrint :: TypedTerm -> TypedTerm -> TopLevel () dsecPrint t1 t2 = do - withSystemTempFile ".aig" $ \path1 _handle1 -> do - withSystemTempFile ".aig" $ \path2 _handle2 -> do - Prover.writeSAIGInferLatches path1 t1 - Prover.writeSAIGInferLatches path2 t2 - io $ callCommand (abcDsec path1 path2) + write_t1 <- Prover.writeSAIGInferLatches t1 + write_t2 <- Prover.writeSAIGInferLatches t2 + io $ withSystemTempFile ".aig" $ \path1 _handle1 -> + withSystemTempFile ".aig" $ \path2 _handle2 -> + do write_t1 path1 + write_t2 path2 + callCommand (abcDsec path1 path2) where -- The '-w' here may be overkill ... abcDsec path1 path2 = printf "abc -c 'read %s; dsec -v -w %s;'" path1 path2 @@ -792,7 +794,9 @@ writeAIGPrim :: FilePath -> Term -> TopLevel () writeAIGPrim = Prover.writeAIG writeSAIGPrim :: FilePath -> TypedTerm -> TopLevel () -writeSAIGPrim = Prover.writeSAIGInferLatches +writeSAIGPrim file tt = + do write_tt <- Prover.writeSAIGInferLatches tt + io $ write_tt file writeSAIGComputedPrim :: FilePath -> Term -> Int -> TopLevel () writeSAIGComputedPrim = Prover.writeSAIG @@ -1375,12 +1379,14 @@ timePrim a = do printOutLnTop Info $ printf "Time: %s\n" (show diff) return r +failPrim :: String -> TopLevel SV.Value +failPrim msg = fail msg + failsPrim :: TopLevel SV.Value -> TopLevel () failsPrim m = do topRO <- getTopLevelRO topRW <- getTopLevelRW - ref <- liftIO $ newIORef topRW - x <- liftIO $ Ex.try (runTopLevel m topRO ref) + x <- liftIO $ Ex.try (runTopLevel m topRO topRW) case x of Left (ex :: Ex.SomeException) -> do liftIO $ putStrLn "== Anticipated failure message ==" diff --git a/src/SAWScript/Exceptions.hs b/src/SAWScript/Exceptions.hs index 0d7481a5e3..f509587d75 100644 --- a/src/SAWScript/Exceptions.hs +++ b/src/SAWScript/Exceptions.hs @@ -64,9 +64,10 @@ topLevelExceptionFromException x = instance Exception TopLevelException -data TraceException = TraceException String +data TraceException = TraceException [String] SomeException instance Show TraceException where - show (TraceException msg) = "Stack trace:\n" ++ msg + show (TraceException msg ex) = + unlines (["Stack trace:"] ++ msg ++ [displayException ex]) instance Exception TraceException diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 671405035a..07d4078602 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -38,7 +38,6 @@ import Control.Monad (unless, (>=>), when) import Control.Monad.IO.Class (liftIO) import qualified Data.ByteString as BS import Data.Foldable (foldrM) -import Data.IORef import qualified Data.Map as Map import Data.Map ( Map ) import qualified Data.Set as Set @@ -283,8 +282,7 @@ interpretStmts env stmts = stmtInterpreter :: StmtInterpreter stmtInterpreter ro rw stmts = - do ref <- newIORef rw - runTopLevel (interpretStmts emptyLocal stmts) ro ref + fst <$> runTopLevel (interpretStmts emptyLocal stmts) ro rw processStmtBind :: Bool -> SS.Pattern -> Maybe SS.Type -> SS.Expr -> TopLevel () processStmtBind printBinds pat _mc expr = do -- mx mt @@ -458,6 +456,7 @@ buildTopLevelEnv proxy opts = , roInitWorkDir = currDir , roBasicSS = ss , roTheoremDB = thmDB + , roStackTrace = [] } let bic = BuiltinContext { biSharedContext = sc @@ -508,8 +507,7 @@ processFile proxy opts file = do oldpath <- getCurrentDirectory file' <- canonicalizePath file setCurrentDirectory (takeDirectory file') - ref <- newIORef rw - _ <- runTopLevel (interpretFile file' True) ro ref + _ <- runTopLevel (interpretFile file' True) ro rw `X.catch` (handleException opts) setCurrentDirectory oldpath return () @@ -823,6 +821,31 @@ primitives = Map.fromList Current [ "Concatenate two strings to yield a third." ] + , prim "callcc" "{a} ((a -> TopLevel ()) -> TopLevel a) -> TopLevel a" + (\_ _ -> toplevelCallCC) + Experimental + [ "Call-with-current-continuation." + , "" + , "This is a highly experimental control operator that can be used" + , "to capure the surrounding top-level computation as a continuation." + , "The consequences of delaying and reentering the current continuation" + , "may be somewhat unpredictable, so use this operator with great caution." + ] + + , prim "checkpoint" "TopLevel (() -> TopLevel ())" + (pureVal checkpoint) + Experimental + [ "Capure the current state of the SAW interpreter, and return" + , "A TopLevel monadic action that, if invoked, will reset the" + , "state of the interpreter back to to what it was at the" + , "moment checkpoint was invoked." + , "" + , "NOTE that this facility is highly experimental and may not" + , "be entirely reliable. It is intended only for proof development" + , "where it can speed up the process of experimenting with" + , "mid-proof changes. Finalized proofs should not use this facility." + ] + , prim "define" "String -> Term -> TopLevel Term" (pureVal definePrim) Current @@ -2320,6 +2343,11 @@ primitives = Map.fromList , "process." ] + , prim "fail" "{a} String -> TopLevel a" + (\_ _ -> toValue failPrim) + Current + [ "Throw an exception in the top level monad." ] + , prim "fails" "{a} TopLevel a -> TopLevel ()" (\_ _ -> toValue failsPrim) Current diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs index 63d66a18bf..ee4cecd7ea 100644 --- a/src/SAWScript/Prover/Exporter.hs +++ b/src/SAWScript/Prover/Exporter.hs @@ -203,13 +203,16 @@ writeSAIG file tt numLatches = do -- | Given a term a type '(i, s) -> (o, s)', call @writeSAIG@ on term -- with latch bits set to '|s|', the width of 's'. -writeSAIGInferLatches :: FilePath -> TypedTerm -> TopLevel () -writeSAIGInferLatches file tt = do +writeSAIGInferLatches :: TypedTerm -> TopLevel (FilePath -> IO ()) +writeSAIGInferLatches tt = do sc <- getSharedContext ty <- io $ scTypeOf sc (ttTerm tt) s <- getStateType sc ty let numLatches = sizeFiniteType s - writeSAIG file (ttTerm tt) numLatches + AIGProxy proxy <- getProxy + return $ \file -> + do aig <- bitblastPrim proxy sc (ttTerm tt) + AIG.writeAigerWithLatches file aig numLatches where die :: String -> TopLevel a die why = throwTopLevel $ diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index eed42f404f..c065723f24 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -37,15 +37,14 @@ import Control.Applicative (Applicative) #endif import Control.Lens import Control.Monad.Fail (MonadFail(..)) -import Control.Monad.Catch (MonadThrow(..), MonadMask(..), - MonadCatch(..), catches, Handler(..)) +import Control.Monad.Catch (MonadThrow(..), MonadCatch(..), catches, Handler(..)) import Control.Monad.Except (ExceptT(..), runExceptT, MonadError(..)) import Control.Monad.Reader (MonadReader) import qualified Control.Exception as X import qualified System.IO.Error as IOError import Control.Monad.IO.Class (MonadIO, liftIO) import Control.Monad.Reader (ReaderT(..), ask, asks, local) -import Control.Monad.State (MonadState(..), StateT(..), get, gets, put) +import Control.Monad.State (StateT(..), gets) import Control.Monad.Trans.Class (MonadTrans(lift)) import Data.IORef import Data.List ( intersperse ) @@ -74,7 +73,7 @@ import qualified Text.LLVM.AST as LLVM (Type) import qualified Text.LLVM.PP as LLVM (ppType) import SAWScript.JavaExpr (JavaType(..)) import SAWScript.JavaPretty (prettyClass) -import SAWScript.Options (Options(printOutFn),printOutLn,Verbosity) +import SAWScript.Options (Options(printOutFn),printOutLn,Verbosity(..)) import SAWScript.Proof import SAWScript.Prover.SolverStats import SAWScript.Prover.MRSolver.Term as MRSolver @@ -108,7 +107,8 @@ import qualified Lang.Crucible.FunctionHandle as Crucible (HandleAllocator) import Lang.Crucible.JVM (JVM) import qualified Lang.Crucible.JVM as CJ -import Lang.Crucible.LLVM.ArraySizeProfile +import Lang.Crucible.Utils.StateContT +import Lang.Crucible.LLVM.ArraySizeProfile import What4.ProgramLoc (ProgramLoc(..)) @@ -381,6 +381,17 @@ evaluateTypedTerm _sc (TypedTerm tp _) = , show (CMS.ppTypedTermType tp) ] +-- NB, the precise locations of VTopLevel constructors in this +-- operator are rather delicate, which is why we write it out +-- here explicitly. +toplevelCallCC :: Value +toplevelCallCC = VLambda body + where + body (VLambda m) = + callCC $ \(k :: Value -> TopLevel Value) -> + m (VLambda (\v -> return (VTopLevel (k ((VTopLevel (return v))))))) + body _ = error "toplevelCallCC : expected lambda" + applyValue :: Value -> Value -> TopLevel Value applyValue (VLambda f) x = f x applyValue _ _ = throwTopLevel "applyValue" @@ -423,6 +434,11 @@ data TopLevelRO = , roInitWorkDir :: FilePath , roBasicSS :: SAWSimpset , roTheoremDB :: TheoremDB + , roStackTrace :: [String] + -- ^ SAWScript-internal backtrace for use + -- when displaying exceptions and such + -- NB, stored with most recent calls on + -- top of the stack. } data TopLevelRW = @@ -467,66 +483,97 @@ data TopLevelRW = } newtype TopLevel a = - TopLevel (ReaderT TopLevelRO (ReaderT (IORef TopLevelRW) IO) a) - deriving (Applicative, Functor, Generic, Generic1, Monad, MonadIO, MonadThrow, MonadCatch, MonadMask) + TopLevel_ (ReaderT TopLevelRO (StateContT TopLevelRW (Value, TopLevelRW) IO) a) + deriving (Applicative, Functor, Generic, Generic1, Monad, MonadThrow, MonadCatch) deriving instance MonadReader TopLevelRO TopLevel - -instance MonadState TopLevelRW TopLevel where - get = TopLevel (lift (ReaderT readIORef)) - put s = TopLevel (lift (ReaderT (flip writeIORef s))) - state f = TopLevel (lift (ReaderT (flip atomicModifyIORef (swap . f)))) - where swap (x, y) = (y, x) - -instance Wrapped (TopLevel a) where +deriving instance MonadState TopLevelRW TopLevel +deriving instance MonadCont TopLevel instance MonadFail TopLevel where fail = throwTopLevel -runTopLevel :: TopLevel a -> TopLevelRO -> IORef TopLevelRW -> IO a -runTopLevel (TopLevel m) ro ref = - runReaderT (runReaderT m ro) ref +runTopLevel :: IsValue a => TopLevel a -> TopLevelRO -> TopLevelRW -> IO (Value, TopLevelRW) +runTopLevel (TopLevel_ m) ro rw = + runStateContT (runReaderT m ro) (\a s -> return (toValue a,s)) rw + +instance MonadIO TopLevel where + liftIO = io io :: IO a -> TopLevel a -io f = liftIO f +io f = (TopLevel_ (liftIO f)) `catches` [ Handler (\(ex :: X86Unsupported) -> handleX86Unsupported ex) , Handler (\(ex :: X86Error) -> handleX86Error ex) + , Handler handleTopLevel + , Handler handleIO ] where + rethrow :: X.Exception ex => ex -> TopLevel a + rethrow ex = + do stk <- getStackTrace + throwM (SS.TraceException stk (X.SomeException ex)) + + handleTopLevel :: SS.TopLevelException -> TopLevel a + handleTopLevel e = rethrow e + + handleIO :: X.IOException -> TopLevel a + handleIO e + | IOError.isUserError e = + do pos <- getPosition + rethrow (SS.TopLevelException pos (init . drop 12 $ show e)) + | otherwise = rethrow e + handleX86Unsupported (X86Unsupported s) = - throwTopLevel $ "Unsupported x86 feature: " ++ s + do pos <- getPosition + rethrow (SS.TopLevelException pos ("Unsupported x86 feature: " ++ s)) + handleX86Error (X86Error s) = - throwTopLevel $ "Error in x86 code: " ++ s + do pos <- getPosition + rethrow (SS.TopLevelException pos ("Error in x86 code: " ++ s)) + +-- | Capture the current state of the TopLevel monad +-- and return an action that, if invoked, resets +-- the state back to that point. +checkpoint :: TopLevel (() -> TopLevel ()) +checkpoint = + do rw <- getTopLevelRW + return $ \_ -> + do printOutLnTop Info "Restoring state from checkpoint" + putTopLevelRW rw throwTopLevel :: String -> TopLevel a throwTopLevel msg = do pos <- getPosition - X.throw $ SS.TopLevelException pos msg + stk <- getStackTrace + throwM (SS.TraceException stk (X.SomeException (SS.TopLevelException pos msg))) withPosition :: SS.Pos -> TopLevel a -> TopLevel a -withPosition pos (TopLevel m) = TopLevel (local (\ro -> ro{ roPosition = pos }) m) +withPosition pos (TopLevel_ m) = TopLevel_ (local (\ro -> ro{ roPosition = pos }) m) getPosition :: TopLevel SS.Pos -getPosition = TopLevel (asks roPosition) +getPosition = TopLevel_ (asks roPosition) + +getStackTrace :: TopLevel [String] +getStackTrace = TopLevel_ (reverse <$> asks roStackTrace) getSharedContext :: TopLevel SharedContext -getSharedContext = TopLevel (asks roSharedContext) +getSharedContext = TopLevel_ (asks roSharedContext) getJavaCodebase :: TopLevel JSS.Codebase -getJavaCodebase = TopLevel (asks roJavaCodebase) +getJavaCodebase = TopLevel_ (asks roJavaCodebase) getOptions :: TopLevel Options -getOptions = TopLevel (asks roOptions) +getOptions = TopLevel_ (asks roOptions) getProxy :: TopLevel AIGProxy -getProxy = TopLevel (asks roProxy) +getProxy = TopLevel_ (asks roProxy) getBasicSS :: TopLevel SAWSimpset -getBasicSS = TopLevel (asks roBasicSS) +getBasicSS = TopLevel_ (asks roBasicSS) localOptions :: (Options -> Options) -> TopLevel a -> TopLevel a -localOptions f (TopLevel m) = TopLevel (local (\x -> x {roOptions = f (roOptions x)}) m) +localOptions f (TopLevel_ m) = TopLevel_ (local (\x -> x {roOptions = f (roOptions x)}) m) printOutLnTop :: Verbosity -> String -> TopLevel () printOutLnTop v s = @@ -539,10 +586,10 @@ printOutTop v s = io $ printOutFn opts v s getHandleAlloc :: TopLevel Crucible.HandleAllocator -getHandleAlloc = TopLevel (asks roHandleAlloc) +getHandleAlloc = TopLevel_ (asks roHandleAlloc) getTopLevelRO :: TopLevel TopLevelRO -getTopLevelRO = TopLevel ask +getTopLevelRO = TopLevel_ ask getTopLevelRW :: TopLevel TopLevelRW getTopLevelRW = get @@ -722,6 +769,10 @@ class FromValue a where instance (FromValue a, IsValue b) => IsValue (a -> b) where toValue f = VLambda (\v -> return (toValue (f (fromValue v)))) +instance (IsValue a, FromValue b) => FromValue (a -> TopLevel b) where + fromValue (VLambda f) = \x -> fromValue <$> f (toValue x) + fromValue _ = error "fromValue (->)" + instance FromValue Value where fromValue x = x @@ -1060,39 +1111,13 @@ addTrace str val = -- TODO? JVM setup blocks too? _ -> val --- | Wrap an action with a handler that catches and rethrows user --- errors with an extended message. -addTraceIO :: forall a. String -> IO a -> IO a -addTraceIO str action = X.catches action - [ X.Handler handleTopLevel - , X.Handler handleTrace - , X.Handler handleIO - ] - where - rethrow msg = X.throwIO . SS.TraceException $ mconcat [str, ":\n", msg] - handleTopLevel :: SS.TopLevelException -> IO a - handleTopLevel e = rethrow $ show e - handleTrace (SS.TraceException msg) = rethrow msg - handleIO :: X.IOException -> IO a - handleIO e - | IOError.isUserError e = rethrow . init . drop 12 $ show e - | otherwise = X.throwIO e - --- | Similar to 'addTraceIO', but for state monads built from 'TopLevel'. -addTraceStateT :: String -> StateT s TopLevel a -> StateT s TopLevel a -addTraceStateT str = underStateT (addTraceTopLevel str) - addTraceProofScript :: String -> ProofScript a -> ProofScript a addTraceProofScript str (ProofScript m) = ProofScript (underExceptT (underStateT (addTraceTopLevel str)) m) --- | Similar to 'addTraceIO', but for reader monads built from 'TopLevel'. -addTraceReaderT :: String -> ReaderT s TopLevel a -> ReaderT s TopLevel a -addTraceReaderT str = underReaderT (addTraceTopLevel str) - --- | Similar to 'addTraceIO', but for the 'TopLevel' monad. addTraceTopLevel :: String -> TopLevel a -> TopLevel a -addTraceTopLevel str action = action & _Wrapped' %~ - underReaderT (underReaderT (liftIO . addTraceIO str)) +addTraceTopLevel str (TopLevel_ action) = + TopLevel_ (local (\ro -> ro{ roStackTrace = str : roStackTrace ro }) action) + data SkeletonState = SkeletonState { _skelArgs :: [(Maybe TypedTerm, Maybe (CMSLLVM.AllLLVM CMS.SetupValue), Maybe Text)] From 8f37eeb204324de1854ff75294465cb3094054c8 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 21 Apr 2022 14:42:14 -0700 Subject: [PATCH 02/14] Implement a "subshell" command. When invoked from a batch file (or from an ongoing REPL session) starts a "subshell" REPL session. The intent here is to allow for exploration and experimentation in the middle of a larger run. For now, subshells are not very useful, as there isn't a good way to expose the local SAW environment to the shell. --- saw-script.cabal | 1 + saw/Main.hs | 8 +++++-- saw/SAWScript/REPL/Haskeline.hs | 23 ++++++++++++++----- saw/SAWScript/REPL/Monad.hs | 40 ++++++++++++++++++++++++--------- src/SAWScript/Interpreter.hs | 22 +++++++++++++----- src/SAWScript/Value.hs | 9 ++++++++ 6 files changed, 80 insertions(+), 23 deletions(-) diff --git a/saw-script.cabal b/saw-script.cabal index 36a3f9bd1b..42e3b42e82 100644 --- a/saw-script.cabal +++ b/saw-script.cabal @@ -213,6 +213,7 @@ executable saw , exceptions , filepath , haskeline + , mtl , QuickCheck , transformers , saw-script diff --git a/saw/Main.hs b/saw/Main.hs index 06d56c09ac..f8a611dc41 100644 --- a/saw/Main.hs +++ b/saw/Main.hs @@ -21,6 +21,8 @@ import SAWScript.Options import SAWScript.Utils import SAWScript.Interpreter (processFile) import qualified SAWScript.REPL as REPL +import qualified SAWScript.REPL.Haskeline as REPL +import qualified SAWScript.REPL.Monad as REPL import SAWScript.Version (shortVersionText) import SAWScript.Value (AIGProxy(..)) import qualified Data.AIG.CompactGraph as AIG @@ -41,12 +43,13 @@ main = do [] -> checkZ3 opts'' *> REPL.run opts'' _ | runInteractively opts'' -> checkZ3 opts'' *> REPL.run opts'' [file] -> checkZ3 opts'' *> - processFile (AIGProxy AIG.compactProxy) opts'' file `catch` + processFile (AIGProxy AIG.compactProxy) opts'' file subsh `catch` (\(ErrorCall msg) -> err opts'' msg) (_:_) -> err opts'' "Multiple files not yet supported." (_, _, errs) -> do hPutStrLn stderr (concat errs ++ usageInfo header options) exitProofUnknown - where header = "Usage: saw [OPTION...] [-I | file]" + where subsh = Just (REPL.subshell (REPL.replBody Nothing (return ()))) + header = "Usage: saw [OPTION...] [-I | file]" checkZ3 opts = do p <- findExecutable "z3" unless (isJust p) @@ -55,3 +58,4 @@ main = do when (verbLevel opts >= Error) (hPutStrLn stderr msg) exitProofUnknown + diff --git a/saw/SAWScript/REPL/Haskeline.hs b/saw/SAWScript/REPL/Haskeline.hs index bcd43e97d7..4c142765bb 100644 --- a/saw/SAWScript/REPL/Haskeline.hs +++ b/saw/SAWScript/REPL/Haskeline.hs @@ -21,6 +21,7 @@ import qualified Control.Monad.Catch as E import Data.Char (isAlphaNum, isSpace) import Data.Function (on) import Data.List (isPrefixOf,sortBy) +import Data.Maybe (isJust) import System.Console.Haskeline import System.Directory(getAppUserDataDirectory,createDirectoryIfMissing) import System.FilePath(()) @@ -29,6 +30,7 @@ import qualified Control.Monad.Trans.Class as MTL import qualified Control.Exception as X import SAWScript.Options (Options) +import SAWScript.TopLevel( TopLevelRO(..) ) -- | Haskeline-specific repl implementation. @@ -38,22 +40,31 @@ import SAWScript.Options (Options) -- handle this. repl :: Maybe FilePath -> Options -> REPL () -> IO () repl mbBatch opts begin = - do settings <- setHistoryFile replSettings - runREPL isBatch opts (runInputTBehavior style settings body) + runREPL (isJust mbBatch) opts (replBody mbBatch begin) + + +replBody :: Maybe FilePath -> REPL () -> REPL () +replBody mbBatch begin = + do settings <- MTL.liftIO (setHistoryFile replSettings) + enableSubshell (runInputTBehavior style settings body) where body = withInterrupt $ do MTL.lift begin loop - (isBatch,style) = case mbBatch of - Nothing -> (False,defaultBehavior) - Just path -> (True,useFile path) + style = case mbBatch of + Nothing -> defaultBehavior + Just path -> useFile path + + enableSubshell m = + REPL $ \refs -> + do let ro' = (eTopLevelRO refs){ roSubshell = subshell (runInputT replSettings (withInterrupt loop)) } + unREPL m refs{ eTopLevelRO = ro' } loop = do prompt <- MTL.lift getPrompt mb <- handleInterrupt (return (Just "")) (getInputLines prompt []) case mb of - Just line | Just cmd <- parseCommand findCommand line -> do continue <- MTL.lift $ do diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs index 3da468e0fe..f9e7df1374 100644 --- a/saw/SAWScript/REPL/Monad.hs +++ b/saw/SAWScript/REPL/Monad.hs @@ -19,6 +19,8 @@ module SAWScript.REPL.Monad ( , catch , catchFail , catchOther + , subshell + , Refs(..) -- ** Errors , REPLException(..) @@ -62,6 +64,9 @@ import Cryptol.Utils.PP import Control.Applicative (Applicative(..), pure, (<*>)) #endif import Control.Monad (unless, ap) +import Control.Monad.Reader (ask) +import Control.Monad.State (put, get) +import Control.Monad.IO.Class (liftIO) import qualified Control.Monad.Fail as Fail import Data.IORef (IORef, newIORef, readIORef, modifyIORef) import Data.Map (Map) @@ -81,7 +86,7 @@ import qualified Data.AIG.CompactGraph as AIG import SAWScript.AST (Located(getVal)) import SAWScript.Interpreter (buildTopLevelEnv) import SAWScript.Options (Options) -import SAWScript.TopLevel (TopLevelRO(..), TopLevelRW(..)) +import SAWScript.TopLevel (TopLevelRO(..), TopLevelRW(..), TopLevel(..)) import SAWScript.Value (AIGProxy(..)) import Verifier.SAW (SharedContext) @@ -92,8 +97,8 @@ deriving instance Typeable AIG.Proxy -- REPL Environment. data Refs = Refs { eContinue :: IORef Bool - , eIsBatch :: IORef Bool - , eTopLevelRO :: IORef TopLevelRO + , eIsBatch :: Bool + , eTopLevelRO :: TopLevelRO , environment :: IORef TopLevelRW } @@ -102,13 +107,11 @@ defaultRefs :: Bool -> Options -> IO Refs defaultRefs isBatch opts = do (_biContext, ro, rw) <- buildTopLevelEnv (AIGProxy AIG.compactProxy) opts contRef <- newIORef True - batchRef <- newIORef isBatch - roRef <- newIORef ro rwRef <- newIORef rw return Refs { eContinue = contRef - , eIsBatch = batchRef - , eTopLevelRO = roRef + , eIsBatch = isBatch + , eTopLevelRO = ro , environment = rwRef } @@ -133,6 +136,23 @@ runREPL isBatch opts m = do refs <- defaultRefs isBatch opts unREPL m refs +subshell :: REPL () -> TopLevel () +subshell (REPL m) = TopLevel_ $ + do ro <- ask + rw <- get + rw' <- liftIO $ + do contRef <- newIORef True + rwRef <- newIORef rw + let refs = Refs + { eContinue = contRef + , eIsBatch = False + , eTopLevelRO = ro + , environment = rwRef + } + m refs + readIORef rwRef + put rw' + instance Functor REPL where {-# INLINE fmap #-} fmap f m = REPL (\ ref -> fmap f (unREPL m ref)) @@ -250,7 +270,7 @@ modifyRef r f = REPL (\refs -> modifyIORef (r refs) f) -- | Construct the prompt for the current environment. getPrompt :: REPL String -getPrompt = mkPrompt <$> readRef eIsBatch +getPrompt = mkPrompt <$> (REPL (return . eIsBatch)) shouldContinue :: REPL Bool shouldContinue = readRef eContinue @@ -260,7 +280,7 @@ stop = modifyRef eContinue (const False) unlessBatch :: REPL () -> REPL () unlessBatch body = - do batch <- readRef eIsBatch + do batch <- REPL (return . eIsBatch) unless batch body setREPLTitle :: REPL () @@ -357,7 +377,7 @@ getSharedContext :: REPL SharedContext getSharedContext = fmap roSharedContext getTopLevelRO getTopLevelRO :: REPL TopLevelRO -getTopLevelRO = readRef eTopLevelRO +getTopLevelRO = REPL (return . eTopLevelRO) getEnvironmentRef :: REPL (IORef TopLevelRW) getEnvironmentRef = environment <$> getRefs diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 07d4078602..d84f362665 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -457,6 +457,7 @@ buildTopLevelEnv proxy opts = , roBasicSS = ss , roTheoremDB = thmDB , roStackTrace = [] + , roSubshell = fail "Subshells not supported" } let bic = BuiltinContext { biSharedContext = sc @@ -499,15 +500,21 @@ buildTopLevelEnv proxy opts = } return (bic, ro0, rw0) -processFile :: AIGProxy - -> Options - -> FilePath -> IO () -processFile proxy opts file = do +processFile :: + AIGProxy -> + Options -> + FilePath -> + Maybe (TopLevel ()) -> + IO () +processFile proxy opts file mbSubshell = do (_, ro, rw) <- buildTopLevelEnv proxy opts + let ro' = case mbSubshell of + Nothing -> ro + Just m -> ro{ roSubshell = m } oldpath <- getCurrentDirectory file' <- canonicalizePath file setCurrentDirectory (takeDirectory file') - _ <- runTopLevel (interpretFile file' True) ro rw + _ <- runTopLevel (interpretFile file' True) ro' rw `X.catch` (handleException opts) setCurrentDirectory oldpath return () @@ -846,6 +853,11 @@ primitives = Map.fromList , "mid-proof changes. Finalized proofs should not use this facility." ] + , prim "subshell" "() -> TopLevel ()" + (\_ _ -> toplevelSubshell) + Experimental + [] + , prim "define" "String -> Term -> TopLevel Term" (pureVal definePrim) Current diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index c065723f24..52643a3ab8 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -392,6 +392,11 @@ toplevelCallCC = VLambda body m (VLambda (\v -> return (VTopLevel (k ((VTopLevel (return v))))))) body _ = error "toplevelCallCC : expected lambda" +toplevelSubshell :: Value +toplevelSubshell = VLambda $ \_ -> + do m <- roSubshell <$> ask + return (VTopLevel (toValue <$> m)) + applyValue :: Value -> Value -> TopLevel Value applyValue (VLambda f) x = f x applyValue _ _ = throwTopLevel "applyValue" @@ -439,6 +444,10 @@ data TopLevelRO = -- when displaying exceptions and such -- NB, stored with most recent calls on -- top of the stack. + , roSubshell :: TopLevel () + -- ^ An action for entering a subshell. This + -- may raise an error if the current execution + -- mode doesn't support subshells (e.g., the remote API) } data TopLevelRW = From 7a305d7e8ea642a62952bb456f6a4ed53bcd93cd Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 21 Apr 2022 17:24:33 -0700 Subject: [PATCH 03/14] Push the SAW script "local environment" into the read-only section of the TopLevel monad. This allows it to interact with primitive operations; in particular, we can start a subshell with local SAW script bindings in scope. --- saw/SAWScript/REPL/Command.hs | 4 +- saw/SAWScript/REPL/Monad.hs | 9 ++- src/SAWScript/Builtins.hs | 3 +- src/SAWScript/Interpreter.hs | 141 +++++++++++++++------------------- src/SAWScript/Value.hs | 40 +++++++++- 5 files changed, 111 insertions(+), 86 deletions(-) diff --git a/saw/SAWScript/REPL/Command.hs b/saw/SAWScript/REPL/Command.hs index aaedba4f62..e390c39881 100644 --- a/saw/SAWScript/REPL/Command.hs +++ b/saw/SAWScript/REPL/Command.hs @@ -163,7 +163,7 @@ typeOfCmd str = Left err -> fail (show err) Right expr -> return expr let decl = SS.Decl (getPos expr) (SS.PWild Nothing) Nothing expr - rw <- getEnvironment + rw <- getValueEnvironment ~(SS.Decl _pos _ (Just schema) _expr') <- either failTypecheck return $ checkDecl (rwTypes rw) (rwTypedef rw) decl io $ putStrLn $ SS.pShow schema @@ -174,7 +174,7 @@ quitCmd = stop envCmd :: REPL () envCmd = do - env <- getEnvironment + env <- getValueEnvironment let showLName = SS.getVal io $ sequence_ [ putStrLn (showLName x ++ " : " ++ SS.pShow v) | (x, v) <- Map.assocs (rwTypes env) ] diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs index f9e7df1374..890b24d94d 100644 --- a/saw/SAWScript/REPL/Monad.hs +++ b/saw/SAWScript/REPL/Monad.hs @@ -44,6 +44,7 @@ module SAWScript.REPL.Monad ( -- ** SAWScript stuff , getSharedContext , getTopLevelRO + , getValueEnvironment , getEnvironment, modifyEnvironment, putEnvironment , getEnvironmentRef , getSAWScriptNames @@ -87,7 +88,7 @@ import SAWScript.AST (Located(getVal)) import SAWScript.Interpreter (buildTopLevelEnv) import SAWScript.Options (Options) import SAWScript.TopLevel (TopLevelRO(..), TopLevelRW(..), TopLevel(..)) -import SAWScript.Value (AIGProxy(..)) +import SAWScript.Value (AIGProxy(..), mergeLocalEnv) import Verifier.SAW (SharedContext) deriving instance Typeable AIG.Proxy @@ -385,6 +386,12 @@ getEnvironmentRef = environment <$> getRefs getEnvironment :: REPL TopLevelRW getEnvironment = readRef environment +getValueEnvironment :: REPL TopLevelRW +getValueEnvironment = + do ro <- getTopLevelRO + rw <- getEnvironment + io (mergeLocalEnv (roSharedContext ro) (roLocalEnv ro) rw) + putEnvironment :: TopLevelRW -> REPL () putEnvironment = modifyEnvironment . const diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index bf1b981837..bfaf3866bb 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -1343,10 +1343,9 @@ caseSatResultPrim sr vUnsat vSat = do tt <- io $ typedTermOfFirstOrderValue sc fov SV.applyValue vSat (SV.toValue tt) - envCmd :: TopLevel () envCmd = do - m <- rwTypes <$> getTopLevelRW + m <- rwTypes <$> SV.getMergedEnv opts <- getOptions let showLName = getVal io $ sequence_ [ printOutLn opts Info (showLName x ++ " : " ++ pShow v) | (x, v) <- Map.assocs m ] diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index d84f362665..bbe62cb05f 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -33,11 +33,11 @@ module SAWScript.Interpreter import Control.Applicative import Data.Traversable hiding ( mapM ) #endif +import Control.Applicative ( (<|>) ) import qualified Control.Exception as X import Control.Monad (unless, (>=>), when) import Control.Monad.IO.Class (liftIO) import qualified Data.ByteString as BS -import Data.Foldable (foldrM) import qualified Data.Map as Map import Data.Map ( Map ) import qualified Data.Set as Set @@ -109,37 +109,11 @@ import SAWScript.VerificationSummary -- Environment ----------------------------------------------------------------- -data LocalBinding - = LocalLet SS.LName (Maybe SS.Schema) (Maybe String) Value - | LocalTypedef SS.Name SS.Type - -type LocalEnv = [LocalBinding] - -emptyLocal :: LocalEnv -emptyLocal = [] - -extendLocal :: SS.LName -> Maybe SS.Schema -> Maybe String -> Value -> LocalEnv -> LocalEnv -extendLocal x mt md v env = LocalLet x mt md v : env - -addTypedef :: SS.Name -> SS.Type -> TopLevelRW -> TopLevelRW -addTypedef name ty rw = rw { rwTypedef = Map.insert name ty (rwTypedef rw) } - -mergeLocalEnv :: SharedContext -> LocalEnv -> TopLevelRW -> IO TopLevelRW -mergeLocalEnv sc env rw = foldrM addBinding rw env - where addBinding (LocalLet x mt md v) = extendEnv sc x mt md v - addBinding (LocalTypedef n ty) = pure . addTypedef n ty - -getMergedEnv :: LocalEnv -> TopLevel TopLevelRW -getMergedEnv env = - do sc <- getSharedContext - rw <- getTopLevelRW - liftIO $ mergeLocalEnv sc env rw - bindPatternLocal :: SS.Pattern -> Maybe SS.Schema -> Value -> LocalEnv -> LocalEnv bindPatternLocal pat ms v env = case pat of SS.PWild _ -> env - SS.PVar x _ -> extendLocal x ms Nothing v env + SS.PVar x mt -> extendLocal x (ms <|> (SS.tMono <$> mt)) Nothing v env SS.PTuple ps -> case v of VTuple vs -> foldr ($) env (zipWith3 bindPatternLocal ps mss vs) @@ -147,17 +121,17 @@ bindPatternLocal pat ms v env = Nothing -> repeat Nothing Just (SS.Forall ks (SS.TyCon (SS.TupleCon _) ts)) -> [ Just (SS.Forall ks t) | t <- ts ] - _ -> error "bindPattern: expected tuple value" - _ -> error "bindPattern: expected tuple value" + Just t -> error ("bindPatternLocal: expected tuple type " ++ show t) + _ -> error "bindPatternLocal: expected tuple value" SS.LPattern _ pat' -> bindPatternLocal pat' ms v env bindPatternEnv :: SS.Pattern -> Maybe SS.Schema -> Value -> TopLevelRW -> TopLevel TopLevelRW bindPatternEnv pat ms v env = case pat of SS.PWild _ -> pure env - SS.PVar x _ -> + SS.PVar x mt -> do sc <- getSharedContext - liftIO $ extendEnv sc x ms Nothing v env + liftIO $ extendEnv sc x (ms <|> (SS.tMono <$> mt)) Nothing v env SS.PTuple ps -> case v of VTuple vs -> foldr (=<<) (pure env) (zipWith3 bindPatternEnv ps mss vs) @@ -165,60 +139,61 @@ bindPatternEnv pat ms v env = Nothing -> repeat Nothing Just (SS.Forall ks (SS.TyCon (SS.TupleCon _) ts)) -> [ Just (SS.Forall ks t) | t <- ts ] - _ -> error "bindPattern: expected tuple value" - _ -> error "bindPattern: expected tuple value" + Just t -> error ("bindPatternEnv: expected tuple type " ++ show t) + _ -> error "bindPatternEnv: expected tuple value" SS.LPattern _ pat' -> bindPatternEnv pat' ms v env -- Interpretation of SAWScript ------------------------------------------------- -interpret :: LocalEnv -> SS.Expr -> TopLevel Value -interpret env expr = +interpret :: SS.Expr -> TopLevel Value +interpret expr = let ?fileReader = BS.readFile in case expr of SS.Bool b -> return $ VBool b SS.String s -> return $ VString (Text.pack s) SS.Int z -> return $ VInteger z SS.Code str -> do sc <- getSharedContext - cenv <- fmap rwCryptol (getMergedEnv env) + cenv <- fmap rwCryptol getMergedEnv --io $ putStrLn $ "Parsing code: " ++ show str --showCryptolEnv' cenv t <- io $ CEnv.parseTypedTerm sc cenv $ locToInput str return (toValue t) - SS.CType str -> do cenv <- fmap rwCryptol (getMergedEnv env) + SS.CType str -> do cenv <- fmap rwCryptol getMergedEnv s <- io $ CEnv.parseSchema cenv $ locToInput str return (toValue s) - SS.Array es -> VArray <$> traverse (interpret env) es - SS.Block stmts -> interpretStmts env stmts - SS.Tuple es -> VTuple <$> traverse (interpret env) es - SS.Record bs -> VRecord <$> traverse (interpret env) bs - SS.Index e1 e2 -> do a <- interpret env e1 - i <- interpret env e2 + SS.Array es -> VArray <$> traverse interpret es + SS.Block stmts -> interpretStmts stmts + SS.Tuple es -> VTuple <$> traverse interpret es + SS.Record bs -> VRecord <$> traverse interpret bs + SS.Index e1 e2 -> do a <- interpret e1 + i <- interpret e2 return (indexValue a i) - SS.Lookup e n -> do a <- interpret env e + SS.Lookup e n -> do a <- interpret e return (lookupValue a n) - SS.TLookup e i -> do a <- interpret env e + SS.TLookup e i -> do a <- interpret e return (tupleLookupValue a i) - SS.Var x -> do rw <- getMergedEnv env + SS.Var x -> do rw <- getMergedEnv case Map.lookup x (rwValues rw) of Nothing -> fail $ "unknown variable: " ++ SS.getVal x Just v -> return (addTrace (show x) v) - SS.Function pat e -> do let f v = interpret (bindPatternLocal pat Nothing v env) e + SS.Function pat e -> do env <- getLocalEnv + let f v = withLocalEnv (bindPatternLocal pat Nothing v env) (interpret e) return $ VLambda f - SS.Application e1 e2 -> do v1 <- interpret env e1 - v2 <- interpret env e2 + SS.Application e1 e2 -> do v1 <- interpret e1 + v2 <- interpret e2 case v1 of VLambda f -> f v2 _ -> fail $ "interpret Application: " ++ show v1 - SS.Let dg e -> do env' <- interpretDeclGroup env dg - interpret env' e - SS.TSig e _ -> interpret env e - SS.IfThenElse e1 e2 e3 -> do v1 <- interpret env e1 + SS.Let dg e -> do env' <- interpretDeclGroup dg + withLocalEnv env' (interpret e) + SS.TSig e _ -> interpret e + SS.IfThenElse e1 e2 e3 -> do v1 <- interpret e1 case v1 of - VBool b -> interpret env (if b then e2 else e3) + VBool b -> interpret (if b then e2 else e3) _ -> fail $ "interpret IfThenElse: " ++ show v1 - SS.LExpr _ e -> interpret env e + SS.LExpr _ e -> interpret e locToInput :: Located String -> CEnv.InputText locToInput l = CEnv.InputText { CEnv.inpText = getVal l @@ -236,53 +211,58 @@ locToInput l = CEnv.InputText { CEnv.inpText = getVal l interpretDecl :: LocalEnv -> SS.Decl -> TopLevel LocalEnv interpretDecl env (SS.Decl _ pat mt expr) = do - v <- interpret env expr + v <- interpret expr return (bindPatternLocal pat mt v env) interpretFunction :: LocalEnv -> SS.Expr -> Value interpretFunction env expr = case expr of SS.Function pat e -> VLambda f - where f v = interpret (bindPatternLocal pat Nothing v env) e + where f v = withLocalEnv (bindPatternLocal pat Nothing v env) (interpret e) SS.TSig e _ -> interpretFunction env e _ -> error "interpretFunction: not a function" -interpretDeclGroup :: LocalEnv -> SS.DeclGroup -> TopLevel LocalEnv -interpretDeclGroup env (SS.NonRecursive d) = interpretDecl env d -interpretDeclGroup env (SS.Recursive ds) = return env' - where - env' = foldr addDecl env ds - addDecl (SS.Decl _ pat mty e) = bindPatternLocal pat mty (interpretFunction env' e) - -interpretStmts :: LocalEnv -> [SS.Stmt] -> TopLevel Value -interpretStmts env stmts = +interpretDeclGroup :: SS.DeclGroup -> TopLevel LocalEnv +interpretDeclGroup (SS.NonRecursive d) = + do env <- getLocalEnv + interpretDecl env d +interpretDeclGroup (SS.Recursive ds) = + do env <- getLocalEnv + let addDecl (SS.Decl _ pat mty e) = bindPatternLocal pat mty (interpretFunction env' e) + env' = foldr addDecl env ds + return env' + +interpretStmts :: [SS.Stmt] -> TopLevel Value +interpretStmts stmts = let ?fileReader = BS.readFile in case stmts of [] -> fail "empty block" - [SS.StmtBind pos (SS.PWild _) _ e] -> withPosition pos (interpret env e) + [SS.StmtBind pos (SS.PWild _) _ e] -> withPosition pos (interpret e) SS.StmtBind pos pat _mcxt e : ss -> - do v1 <- withPosition pos (interpret env e) - let f v = interpretStmts (bindPatternLocal pat Nothing v env) ss + do env <- getLocalEnv + v1 <- withPosition pos (interpret e) + let f v = withLocalEnv (bindPatternLocal pat Nothing v env) (interpretStmts ss) bindValue pos v1 (VLambda f) - SS.StmtLet _ bs : ss -> interpret env (SS.Let bs (SS.Block ss)) + SS.StmtLet _ bs : ss -> interpret (SS.Let bs (SS.Block ss)) SS.StmtCode _ s : ss -> do sc <- getSharedContext - rw <- getMergedEnv env + rw <- getMergedEnv ce' <- io $ CEnv.parseDecls sc (rwCryptol rw) $ locToInput s -- FIXME: Local bindings get saved into the global cryptol environment here. -- We should change parseDecls to return only the new bindings instead. putTopLevelRW $ rw{rwCryptol = ce'} - interpretStmts env ss + interpretStmts ss SS.StmtImport _ _ : _ -> do fail "block import unimplemented" SS.StmtTypedef _ name ty : ss -> - do let env' = LocalTypedef (getVal name) ty : env - interpretStmts env' ss + do env <- getLocalEnv + let env' = LocalTypedef (getVal name) ty : env + withLocalEnv env' (interpretStmts ss) stmtInterpreter :: StmtInterpreter stmtInterpreter ro rw stmts = - fst <$> runTopLevel (interpretStmts emptyLocal stmts) ro rw + fst <$> runTopLevel (withLocalEnv emptyLocal (interpretStmts stmts)) ro rw processStmtBind :: Bool -> SS.Pattern -> Maybe SS.Type -> SS.Expr -> TopLevel () processStmtBind printBinds pat _mc expr = do -- mx mt @@ -297,13 +277,13 @@ processStmtBind printBinds pat _mc expr = do -- mx mt Nothing -> expr Just t -> SS.TSig expr (SS.tBlock ctx t) let decl = SS.Decl (SS.getPos expr) pat Nothing expr' - rw <- getTopLevelRW + rw <- getMergedEnv let opts = rwPPOpts rw ~(SS.Decl _ _ (Just schema) expr'') <- either failTypecheck return $ checkDecl (rwTypes rw) (rwTypedef rw) decl - val <- interpret emptyLocal expr'' + val <- interpret expr'' -- Run the resulting TopLevel action. (result, ty) <- @@ -344,8 +324,8 @@ interpretStmt printBinds stmt = SS.StmtLet _ dg -> do rw <- getTopLevelRW dg' <- either failTypecheck return $ checkDeclGroup (rwTypes rw) (rwTypedef rw) dg - env <- interpretDeclGroup emptyLocal dg' - getMergedEnv env >>= putTopLevelRW + env <- interpretDeclGroup dg' + withLocalEnv env getMergedEnv >>= putTopLevelRW SS.StmtCode _ lstr -> do rw <- getTopLevelRW sc <- getSharedContext --io $ putStrLn $ "Processing toplevel code: " ++ show lstr @@ -458,6 +438,7 @@ buildTopLevelEnv proxy opts = , roTheoremDB = thmDB , roStackTrace = [] , roSubshell = fail "Subshells not supported" + , roLocalEnv = [] } let bic = BuiltinContext { biSharedContext = sc diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 52643a3ab8..9b9b401889 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -47,6 +47,7 @@ import Control.Monad.Reader (ReaderT(..), ask, asks, local) import Control.Monad.State (StateT(..), gets) import Control.Monad.Trans.Class (MonadTrans(lift)) import Data.IORef +import Data.Foldable(foldrM) import Data.List ( intersperse ) import qualified Data.Map as M import Data.Map ( Map ) @@ -395,7 +396,8 @@ toplevelCallCC = VLambda body toplevelSubshell :: Value toplevelSubshell = VLambda $ \_ -> do m <- roSubshell <$> ask - return (VTopLevel (toValue <$> m)) + env <- getLocalEnv + return (VTopLevel (toValue <$> withLocalEnv env m)) applyValue :: Value -> Value -> TopLevel Value applyValue (VLambda f) x = f x @@ -427,6 +429,35 @@ data PrimitiveLifecycle request at the moment. -} deriving (Eq, Ord, Show) +data LocalBinding + = LocalLet SS.LName (Maybe SS.Schema) (Maybe String) Value + | LocalTypedef SS.Name SS.Type + deriving (Show) + +type LocalEnv = [LocalBinding] + +emptyLocal :: LocalEnv +emptyLocal = [] + +extendLocal :: SS.LName -> Maybe SS.Schema -> Maybe String -> Value -> LocalEnv -> LocalEnv +extendLocal x mt md v env = LocalLet x mt md v : env + +addTypedef :: SS.Name -> SS.Type -> TopLevelRW -> TopLevelRW +addTypedef name ty rw = rw { rwTypedef = M.insert name ty (rwTypedef rw) } + +mergeLocalEnv :: SharedContext -> LocalEnv -> TopLevelRW -> IO TopLevelRW +mergeLocalEnv sc env rw = foldrM addBinding rw env + where addBinding (LocalLet x mt md v) = extendEnv sc x mt md v + addBinding (LocalTypedef n ty) = pure . addTypedef n ty + +getMergedEnv :: TopLevel TopLevelRW +getMergedEnv = + do sc <- getSharedContext + env <- getLocalEnv + rw <- getTopLevelRW + liftIO $ mergeLocalEnv sc env rw + + -- | TopLevel Read-Only Environment. data TopLevelRO = TopLevelRO @@ -448,6 +479,7 @@ data TopLevelRO = -- ^ An action for entering a subshell. This -- may raise an error if the current execution -- mode doesn't support subshells (e.g., the remote API) + , roLocalEnv :: LocalEnv } data TopLevelRW = @@ -560,6 +592,12 @@ throwTopLevel msg = do withPosition :: SS.Pos -> TopLevel a -> TopLevel a withPosition pos (TopLevel_ m) = TopLevel_ (local (\ro -> ro{ roPosition = pos }) m) +withLocalEnv :: LocalEnv -> TopLevel a -> TopLevel a +withLocalEnv env (TopLevel_ m) = TopLevel_ (local (\ro -> ro{ roLocalEnv = env }) m) + +getLocalEnv :: TopLevel LocalEnv +getLocalEnv = TopLevel_ (asks roLocalEnv) + getPosition :: TopLevel SS.Pos getPosition = TopLevel_ (asks roPosition) From dbe32ba2281e8aa599c6c93bcd19a3d1b65e936b Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 21 Apr 2022 17:58:07 -0700 Subject: [PATCH 04/14] Prevent the REPL from grabbing and printing exceptions it should be leaving alone (async and exit exceptions). --- saw/SAWScript/REPL/Command.hs | 4 +++- saw/SAWScript/REPL/Monad.hs | 11 +++++++++-- 2 files changed, 12 insertions(+), 3 deletions(-) diff --git a/saw/SAWScript/REPL/Command.hs b/saw/SAWScript/REPL/Command.hs index e390c39881..8602ad8a7d 100644 --- a/saw/SAWScript/REPL/Command.hs +++ b/saw/SAWScript/REPL/Command.hs @@ -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) @@ -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)) diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs index 890b24d94d..d2f7ac4738 100644 --- a/saw/SAWScript/REPL/Monad.hs +++ b/saw/SAWScript/REPL/Monad.hs @@ -8,6 +8,7 @@ Stability : provisional {-# LANGUAGE CPP #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} module SAWScript.REPL.Monad ( @@ -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 @@ -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 From d9f6ba0564f5dee9b39dbd87deb49ac7a0acaac3 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Fri, 22 Apr 2022 10:57:00 -0700 Subject: [PATCH 05/14] Fix the saw-remote-api build --- saw-remote-api/src/SAWServer.hs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index b3abfd01c8..a485bfac55 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -212,6 +212,9 @@ initialState readFileFn = , roInitWorkDir = cwd , roBasicSS = ss , roTheoremDB = db + , roStackTrace = [] + , roSubshell = fail "SAW server does not support subshells." + , roLocalEnv = [] } rw = TopLevelRW { rwValues = mempty From e85d331d18e886ce7c5b8bb9d02d8a13547d70e0 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Wed, 27 Apr 2022 16:35:17 -0700 Subject: [PATCH 06/14] Make `checkpoint` somewhat less broken. This change causes the `NameSeeds` value used internally by Cryptol to be carried forward across checkpoints. This prevents internal nonce values from being reused, which, in turn, avoids errors about registering duplicate names. It is unclear if this is the correct long-term fix, but it allows checkpoint to work more reliably when importing Cryptol modules or using `let {{ ... }}` constructs. --- .../src/Verifier/SAW/CryptolEnv.hs | 10 +++++++ src/SAWScript/Value.hs | 28 +++++++++++++++++-- 2 files changed, 36 insertions(+), 2 deletions(-) diff --git a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs index 4d9444e90e..74892c7895 100644 --- a/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs +++ b/cryptol-saw-core/src/Verifier/SAW/CryptolEnv.hs @@ -16,6 +16,7 @@ module Verifier.SAW.CryptolEnv , loadCryptolModule , bindCryptolModule , lookupCryptolModule + , combineCryptolEnv , importModule , bindTypedTerm , bindType @@ -345,6 +346,15 @@ genTermEnv sc modEnv cryEnv0 = do -------------------------------------------------------------------------------- + +combineCryptolEnv :: CryptolEnv -> CryptolEnv -> IO CryptolEnv +combineCryptolEnv chkEnv newEnv = + do let newMEnv = eModuleEnv newEnv + let chkMEnv = eModuleEnv chkEnv + let menv' = chkMEnv{ ME.meNameSeeds = ME.meNameSeeds newMEnv } + return chkEnv{ eModuleEnv = menv' } + + checkNotParameterized :: T.Module -> IO () checkNotParameterized m = when (T.isParametrizedModule m) $ diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 9b9b401889..971acb838c 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -573,15 +573,39 @@ io f = (TopLevel_ (liftIO f)) do pos <- getPosition rethrow (SS.TopLevelException pos ("Error in x86 code: " ++ s)) + + + +combineRW :: TopLevelCheckpoint -> TopLevelRW -> IO TopLevelRW +combineRW (TopLevelCheckpoint chk) rw = + do cenv' <- CEnv.combineCryptolEnv (rwCryptol chk) (rwCryptol rw) + return chk{ rwCryptol = cenv' } + +-- | Represents the mutable state of the TopLevel monad +-- that can later be restored. +newtype TopLevelCheckpoint = + TopLevelCheckpoint TopLevelRW + +makeCheckpoint :: TopLevel TopLevelCheckpoint +makeCheckpoint = + do rw <- getTopLevelRW + return (TopLevelCheckpoint rw) + +restoreCheckpoint :: TopLevelCheckpoint -> TopLevel () +restoreCheckpoint chk = + do rw <- getTopLevelRW + rw' <- io (combineRW chk rw) + putTopLevelRW rw' + -- | Capture the current state of the TopLevel monad -- and return an action that, if invoked, resets -- the state back to that point. checkpoint :: TopLevel (() -> TopLevel ()) checkpoint = - do rw <- getTopLevelRW + do chk <- makeCheckpoint return $ \_ -> do printOutLnTop Info "Restoring state from checkpoint" - putTopLevelRW rw + restoreCheckpoint chk throwTopLevel :: String -> TopLevel a throwTopLevel msg = do From 8bb8cae34802ab863bd756fc7dee20c38702918b Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 28 Apr 2022 15:06:52 -0700 Subject: [PATCH 07/14] Move the `SharedContext` and `TheoremDB` objects into the mutable state part of the TopLevel monad. This allows them to participate in the checkpoint/restore mechanism. --- saw-remote-api/src/SAWServer.hs | 6 +++--- saw/SAWScript/REPL/Monad.hs | 4 ++-- src/SAWScript/Builtins.hs | 31 ++++++++++++++++++++++++++----- src/SAWScript/Interpreter.hs | 26 +++----------------------- src/SAWScript/Value.hs | 15 ++++++++++----- 5 files changed, 44 insertions(+), 38 deletions(-) diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index a485bfac55..08f3f40246 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -199,8 +199,7 @@ initialState readFileFn = cwd <- getCurrentDirectory db <- newTheoremDB let ro = TopLevelRO - { roSharedContext = sc - , roJavaCodebase = jcb + { roJavaCodebase = jcb , roOptions = opts , roHandleAlloc = halloc , roPosition = PosInternal "SAWServer" @@ -211,7 +210,6 @@ initialState readFileFn = #endif , roInitWorkDir = cwd , roBasicSS = ss - , roTheoremDB = db , roStackTrace = [] , roSubshell = fail "SAW server does not support subshells." , roLocalEnv = [] @@ -225,6 +223,8 @@ initialState readFileFn = , rwMonadify = defaultMonEnv , rwMRSolverEnv = emptyMREnv , rwPPOpts = defaultPPOpts + , rwTheoremDB = db + , rwSharedContext = sc , rwJVMTrans = jvmTrans , rwPrimsAvail = mempty , rwSMTArrayMemoryModel = False diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs index d2f7ac4738..239fed9305 100644 --- a/saw/SAWScript/REPL/Monad.hs +++ b/saw/SAWScript/REPL/Monad.hs @@ -382,7 +382,7 @@ setCryptolEnv :: CryptolEnv -> REPL () setCryptolEnv x = modifyCryptolEnv (const x) getSharedContext :: REPL SharedContext -getSharedContext = fmap roSharedContext getTopLevelRO +getSharedContext = rwSharedContext <$> getEnvironment getTopLevelRO :: REPL TopLevelRO getTopLevelRO = REPL (return . eTopLevelRO) @@ -397,7 +397,7 @@ getValueEnvironment :: REPL TopLevelRW getValueEnvironment = do ro <- getTopLevelRO rw <- getEnvironment - io (mergeLocalEnv (roSharedContext ro) (roLocalEnv ro) rw) + io (mergeLocalEnv (rwSharedContext rw) (roLocalEnv ro) rw) putEnvironment :: TopLevelRW -> REPL () putEnvironment = modifyEnvironment . const diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index bfaf3866bb..cf9e669870 100644 --- a/src/SAWScript/Builtins.hs +++ b/src/SAWScript/Builtins.hs @@ -51,6 +51,7 @@ import qualified System.Environment import qualified System.Exit as Exit import System.IO import System.IO.Temp (withSystemTempFile, emptySystemTempFile) +import System.FilePath (hasDrive, ()) import System.Process (callCommand, readProcessWithExitCode) import Text.Printf (printf) import Text.Read (readMaybe) @@ -1644,7 +1645,7 @@ core_axiom input = pos <- SV.getPosition t <- parseCore input p <- io (termToProp sc t) - db <- roTheoremDB <$> getTopLevelRO + db <- SV.getTheoremDB thm <- io (admitTheorem db "core_axiom" p pos "core_axiom") SV.returnProof thm @@ -1653,14 +1654,14 @@ core_thm input = do t <- parseCore input sc <- getSharedContext pos <- SV.getPosition - db <- roTheoremDB <$> getTopLevelRO + db <- SV.getTheoremDB thm <- io (proofByTerm sc db t pos "core_thm") SV.returnProof thm specialize_theorem :: Theorem -> [TypedTerm] -> TopLevel Theorem specialize_theorem thm ts = do sc <- getSharedContext - db <- roTheoremDB <$> getTopLevelRO + db <- SV.getTheoremDB pos <- SV.getPosition thm' <- io (specializeTheorem sc db pos "specialize_theorem" thm (map ttTerm ts)) SV.returnProof thm' @@ -1995,7 +1996,7 @@ summarize_verification = let jspecs = [ s | SV.VJVMMethodSpec s <- values ] lspecs = [ s | SV.VLLVMCrucibleMethodSpec s <- values ] thms = [ t | SV.VTheorem t <- values ] - db <- roTheoremDB <$> getTopLevelRO + db <- SV.getTheoremDB summary <- io (computeVerificationSummary db jspecs lspecs thms) io $ putStrLn $ prettyVerificationSummary summary @@ -2005,6 +2006,26 @@ summarize_verification_json fpath = let jspecs = [ s | SV.VJVMMethodSpec s <- values ] lspecs = [ s | SV.VLLVMCrucibleMethodSpec s <- values ] thms = [ t | SV.VTheorem t <- values ] - db <- roTheoremDB <$> getTopLevelRO + db <- SV.getTheoremDB summary <- io (computeVerificationSummary db jspecs lspecs thms) io (writeFile fpath (jsonVerificationSummary summary)) + +writeVerificationSummary :: TopLevel () +writeVerificationSummary = do + do + db <- SV.getTheoremDB + values <- rwProofs <$> getTopLevelRW + let jspecs = [ s | SV.VJVMMethodSpec s <- values ] + lspecs = [ s | SV.VLLVMCrucibleMethodSpec s <- values ] + thms = [ t | SV.VTheorem t <- values ] + summary <- io (computeVerificationSummary db jspecs lspecs thms) + opts <- roOptions <$> getTopLevelRO + dir <- roInitWorkDir <$> getTopLevelRO + case summaryFile opts of + Nothing -> return () + Just f -> let + f' = if hasDrive f then f else dir f + formatSummary = case summaryFormat opts of + JSON -> jsonVerificationSummary + Pretty -> prettyVerificationSummary + in io $ writeFile f' $ formatSummary summary diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index bbe62cb05f..9d5abf68f9 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -347,26 +347,6 @@ interpretStmt printBinds stmt = SS.StmtTypedef _ name ty -> do rw <- getTopLevelRW putTopLevelRW $ addTypedef (getVal name) ty rw -writeVerificationSummary :: TopLevel () -writeVerificationSummary = do - do - db <- roTheoremDB <$> getTopLevelRO - values <- rwProofs <$> getTopLevelRW - let jspecs = [ s | VJVMMethodSpec s <- values ] - lspecs = [ s | VLLVMCrucibleMethodSpec s <- values ] - thms = [ t | VTheorem t <- values ] - summary <- io (computeVerificationSummary db jspecs lspecs thms) - opts <- roOptions <$> getTopLevelRO - dir <- roInitWorkDir <$> getTopLevelRO - case summaryFile opts of - Nothing -> return () - Just f -> let - f' = if hasDrive f then f else dir f - formatSummary = case summaryFormat opts of - JSON -> jsonVerificationSummary - Pretty -> prettyVerificationSummary - in io $ writeFile f' $ formatSummary summary - interpretFile :: FilePath -> Bool {- ^ run main? -} -> TopLevel () interpretFile file runMain = do opts <- getOptions @@ -427,15 +407,13 @@ buildTopLevelEnv proxy opts = thmDB <- newTheoremDB Crucible.withHandleAllocator $ \halloc -> do let ro0 = TopLevelRO - { roSharedContext = sc - , roJavaCodebase = jcb + { roJavaCodebase = jcb , roOptions = opts , roHandleAlloc = halloc , roPosition = SS.Unknown , roProxy = proxy , roInitWorkDir = currDir , roBasicSS = ss - , roTheoremDB = thmDB , roStackTrace = [] , roSubshell = fail "Subshells not supported" , roLocalEnv = [] @@ -459,6 +437,8 @@ buildTopLevelEnv proxy opts = , rwMRSolverEnv = emptyMREnv , rwProofs = [] , rwPPOpts = SAWScript.Value.defaultPPOpts + , rwSharedContext = sc + , rwTheoremDB = thmDB , rwJVMTrans = jvmTrans , rwPrimsAvail = primsAvail , rwSMTArrayMemoryModel = False diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index 971acb838c..acaf10e060 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -461,15 +461,13 @@ getMergedEnv = -- | TopLevel Read-Only Environment. data TopLevelRO = TopLevelRO - { roSharedContext :: SharedContext - , roJavaCodebase :: JSS.Codebase + { roJavaCodebase :: JSS.Codebase , roOptions :: Options , roHandleAlloc :: Crucible.HandleAllocator , roPosition :: SS.Pos , roProxy :: AIGProxy , roInitWorkDir :: FilePath , roBasicSS :: SAWSimpset - , roTheoremDB :: TheoremDB , roStackTrace :: [String] -- ^ SAWScript-internal backtrace for use -- when displaying exceptions and such @@ -493,6 +491,9 @@ data TopLevelRW = , rwMRSolverEnv :: MRSolver.MREnv , rwProofs :: [Value] {- ^ Values, generated anywhere, that represent proofs. -} , rwPPOpts :: PPOpts + , rwSharedContext :: SharedContext + , rwTheoremDB :: TheoremDB + -- , rwCrucibleLLVMCtx :: Crucible.LLVMContext , rwJVMTrans :: CJ.JVMContext -- ^ crucible-jvm: Handles and info for classes that have already been translated @@ -597,6 +598,7 @@ restoreCheckpoint chk = rw' <- io (combineRW chk rw) putTopLevelRW rw' + -- | Capture the current state of the TopLevel monad -- and return an action that, if invoked, resets -- the state back to that point. @@ -629,11 +631,14 @@ getStackTrace :: TopLevel [String] getStackTrace = TopLevel_ (reverse <$> asks roStackTrace) getSharedContext :: TopLevel SharedContext -getSharedContext = TopLevel_ (asks roSharedContext) +getSharedContext = TopLevel_ (rwSharedContext <$> get) getJavaCodebase :: TopLevel JSS.Codebase getJavaCodebase = TopLevel_ (asks roJavaCodebase) +getTheoremDB :: TopLevel TheoremDB +getTheoremDB = TopLevel_ (rwTheoremDB <$> get) + getOptions :: TopLevel Options getOptions = TopLevel_ (asks roOptions) @@ -808,7 +813,7 @@ runProofScript (ProofScript m) gl ploc rsn = Left (stats,cex) -> return (SAWScript.Proof.InvalidProof stats cex pstate) Right _ -> do sc <- getSharedContext - db <- roTheoremDB <$> getTopLevelRO + db <- rwTheoremDB <$> getTopLevelRW io (finishProof sc db pstate) scriptTopLevel :: TopLevel a -> ProofScript a From 8780ee2088132b4a9a472e0f3bb755dddaf3b509 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 28 Apr 2022 15:35:05 -0700 Subject: [PATCH 08/14] Add checkpoint capabilities to the SharedContext --- saw-core/src/Verifier/SAW/SharedTerm.hs | 30 ++++++++++++++++++++++++- src/SAWScript/Value.hs | 19 ++++++++++------ 2 files changed, 41 insertions(+), 8 deletions(-) diff --git a/saw-core/src/Verifier/SAW/SharedTerm.hs b/saw-core/src/Verifier/SAW/SharedTerm.hs index d0cfae71e7..da056dc77c 100644 --- a/saw-core/src/Verifier/SAW/SharedTerm.hs +++ b/saw-core/src/Verifier/SAW/SharedTerm.hs @@ -59,6 +59,9 @@ module Verifier.SAW.SharedTerm , SharedContext , mkSharedContext , scGetModuleMap + , SharedContextCheckpoint + , checkpointSharedContext + , restoreSharedContext -- ** Low-level generic term constructors , scTermF , scFlatTermF @@ -282,7 +285,7 @@ import qualified Data.HashMap.Strict as HMap import Data.IntMap (IntMap) import qualified Data.IntMap as IntMap import qualified Data.IntSet as IntSet -import Data.IORef (IORef,newIORef,readIORef,modifyIORef',atomicModifyIORef') +import Data.IORef (IORef,newIORef,readIORef,modifyIORef',atomicModifyIORef',writeIORef) import Data.Map (Map) import qualified Data.Map as Map import Data.Ref ( C ) @@ -360,6 +363,31 @@ data SharedContext = SharedContext , scFreshGlobalVar :: IO VarIndex } +data SharedContextCheckpoint = + SCC + { sccModuleMap :: ModuleMap + , sccNamingEnv :: SAWNamingEnv + , sccGlobalEnv :: HashMap Ident Term + } + +checkpointSharedContext :: SharedContext -> IO SharedContextCheckpoint +checkpointSharedContext sc = + do mmap <- readIORef (scModuleMap sc) + nenv <- readIORef (scNamingEnv sc) + genv <- readIORef (scGlobalEnv sc) + return SCC + { sccModuleMap = mmap + , sccNamingEnv = nenv + , sccGlobalEnv = genv + } + +restoreSharedContext :: SharedContextCheckpoint -> SharedContext -> IO SharedContext +restoreSharedContext scc sc = + do writeIORef (scModuleMap sc) (sccModuleMap scc) + writeIORef (scNamingEnv sc) (sccNamingEnv scc) + writeIORef (scGlobalEnv sc) (sccGlobalEnv scc) + return sc + -- | Create a new term from a lower-level 'FlatTermF' term. scFlatTermF :: SharedContext -> FlatTermF Term -> IO Term scFlatTermF sc ftf = scTermF sc (FTermF ftf) diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index acaf10e060..ba98b105c6 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -576,21 +576,26 @@ io f = (TopLevel_ (liftIO f)) - combineRW :: TopLevelCheckpoint -> TopLevelRW -> IO TopLevelRW -combineRW (TopLevelCheckpoint chk) rw = +combineRW (TopLevelCheckpoint chk scc) rw = do cenv' <- CEnv.combineCryptolEnv (rwCryptol chk) (rwCryptol rw) - return chk{ rwCryptol = cenv' } + sc' <- restoreSharedContext scc (rwSharedContext rw) + return chk{ rwCryptol = cenv' + , rwSharedContext = sc' + } -- | Represents the mutable state of the TopLevel monad -- that can later be restored. -newtype TopLevelCheckpoint = - TopLevelCheckpoint TopLevelRW +data TopLevelCheckpoint = + TopLevelCheckpoint + TopLevelRW + SharedContextCheckpoint makeCheckpoint :: TopLevel TopLevelCheckpoint makeCheckpoint = - do rw <- getTopLevelRW - return (TopLevelCheckpoint rw) + do rw <- getTopLevelRW + scc <- io (checkpointSharedContext (rwSharedContext rw)) + return (TopLevelCheckpoint rw scc) restoreCheckpoint :: TopLevelCheckpoint -> TopLevel () restoreCheckpoint chk = From d94298840812e9459650eed154ee4f42958a9ea1 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 28 Apr 2022 16:43:16 -0700 Subject: [PATCH 09/14] Add checkpoint/resume commands to REPL command invocations. --- saw/SAWScript/REPL/Command.hs | 22 ++++--------------- saw/SAWScript/REPL/Monad.hs | 40 ++++++++++++++++++++++++++++++----- src/SAWScript/Interpreter.hs | 4 +--- src/SAWScript/TopLevel.hs | 2 ++ src/SAWScript/Value.hs | 12 +++++------ 5 files changed, 47 insertions(+), 33 deletions(-) diff --git a/saw/SAWScript/REPL/Command.hs b/saw/SAWScript/REPL/Command.hs index 8602ad8a7d..addf1fd963 100644 --- a/saw/SAWScript/REPL/Command.hs +++ b/saw/SAWScript/REPL/Command.hs @@ -30,17 +30,14 @@ module SAWScript.REPL.Command ( --import Verifier.SAW.SharedTerm (SharedContext) -import Data.IORef import SAWScript.REPL.Monad import SAWScript.REPL.Trie import SAWScript.Position (getPos) import Cryptol.Parser (ParseError()) -import Cryptol.Utils.PP hiding (()) -import Control.Exception (displayException) -import Control.Monad (guard) +import Control.Monad (guard, void) import Data.Char (isSpace,isPunctuation,isSymbol) import Data.Function (on) @@ -60,7 +57,7 @@ import SAWScript.MGU (checkDecl) import SAWScript.Interpreter (interpretStmt) import qualified SAWScript.Lexer (lexSAW) import qualified SAWScript.Parser (parseStmtSemi, parseExpression) -import SAWScript.TopLevel (TopLevelRW(..), runTopLevel) +import SAWScript.TopLevel (TopLevelRW(..)) -- Commands -------------------------------------------------------------------- @@ -143,13 +140,7 @@ genHelp cs = map cmdHelp cs runCommand :: Command -> REPL () runCommand c = case c of - Command cmd -> cmd `SAWScript.REPL.Monad.catch` handlerPP - `SAWScript.REPL.Monad.catchFail` handlerFail - `SAWScript.REPL.Monad.catchOther` handlerPrint - where - handlerPP re = io (putStrLn "" >> print (pp re)) - handlerPrint e = io (putStrLn "" >> putStrLn (displayException e)) - handlerFail s = io (putStrLn "" >> putStrLn s) + Command cmd -> exceptionProtect cmd Unknown cmd -> io (putStrLn ("Unknown command: " ++ cmd)) @@ -230,12 +221,7 @@ sawScriptCmd str = do let tokens = SAWScript.Lexer.lexSAW replFileName str case SAWScript.Parser.parseStmtSemi tokens of Left err -> io $ print err - Right stmt -> - do ro <- getTopLevelRO - ref <- getEnvironmentRef - rw <- io $ readIORef ref - (_, rw') <- io $ runTopLevel (interpretStmt True stmt) ro rw - io $ writeIORef ref rw' + Right stmt -> void $ liftTopLevel (interpretStmt True stmt) replFileName :: String replFileName = "" diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs index 239fed9305..abdd8aa870 100644 --- a/saw/SAWScript/REPL/Monad.hs +++ b/saw/SAWScript/REPL/Monad.hs @@ -20,6 +20,8 @@ module SAWScript.REPL.Monad ( , catch , catchFail , catchOther + , exceptionProtect + , liftTopLevel , subshell , Refs(..) @@ -65,12 +67,12 @@ import Cryptol.Utils.PP #if !MIN_VERSION_base(4,8,0) import Control.Applicative (Applicative(..), pure, (<*>)) #endif -import Control.Monad (unless, ap) +import Control.Monad (unless, ap, void) import Control.Monad.Reader (ask) import Control.Monad.State (put, get) import Control.Monad.IO.Class (liftIO) import qualified Control.Monad.Fail as Fail -import Data.IORef (IORef, newIORef, readIORef, modifyIORef) +import Data.IORef (IORef, newIORef, readIORef, modifyIORef, writeIORef) import Data.Map (Map) import qualified Data.Map as Map import Data.Typeable (Typeable) @@ -89,8 +91,9 @@ import qualified Data.AIG.CompactGraph as AIG import SAWScript.AST (Located(getVal)) import SAWScript.Interpreter (buildTopLevelEnv) import SAWScript.Options (Options) -import SAWScript.TopLevel (TopLevelRO(..), TopLevelRW(..), TopLevel(..)) -import SAWScript.Value (AIGProxy(..), mergeLocalEnv) +import SAWScript.TopLevel (TopLevelRO(..), TopLevelRW(..), TopLevel(..), runTopLevel, + makeCheckpoint, restoreCheckpoint) +import SAWScript.Value (AIGProxy(..), mergeLocalEnv, IsValue, Value) import Verifier.SAW (SharedContext) deriving instance Typeable AIG.Proxy @@ -260,7 +263,34 @@ rethrowEvalError m = run `X.catch` rethrow rethrow (EvalErrorEx _ exn) = X.throwIO (EvalError exn) - +exceptionProtect :: REPL () -> REPL () +exceptionProtect cmd = + do chk <- io . makeCheckpoint =<< getEnvironment + cmd `catch` (handlerPP chk) + `catchFail` (handlerFail chk) + `catchOther` (handlerPrint chk) + + where + handlerPP chk re = + do io (putStrLn "" >> print (pp re)) + void $ liftTopLevel (restoreCheckpoint chk) + return () + handlerPrint chk e = + do io (putStrLn "" >> putStrLn (X.displayException e)) + void $ liftTopLevel (restoreCheckpoint chk) + + handlerFail chk s = + do io (putStrLn "" >> putStrLn s) + void $ liftTopLevel (restoreCheckpoint chk) + +liftTopLevel :: IsValue a => TopLevel a -> REPL Value +liftTopLevel m = + do ro <- getTopLevelRO + ref <- getEnvironmentRef + io $ do rw <- readIORef ref + (v,rw') <- runTopLevel m ro rw + writeIORef ref rw' + return v -- Primitives ------------------------------------------------------------------ diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 9d5abf68f9..4b13b05350 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -44,7 +44,7 @@ import qualified Data.Set as Set import Data.Set ( Set ) import qualified Data.Text as Text import System.Directory (getCurrentDirectory, setCurrentDirectory, canonicalizePath) -import System.FilePath (takeDirectory, hasDrive, ()) +import System.FilePath (takeDirectory) import System.Process (readProcess) import qualified SAWScript.AST as SS @@ -105,8 +105,6 @@ import SAWScript.AutoMatch import qualified Lang.Crucible.FunctionHandle as Crucible -import SAWScript.VerificationSummary - -- Environment ----------------------------------------------------------------- bindPatternLocal :: SS.Pattern -> Maybe SS.Schema -> Value -> LocalEnv -> LocalEnv diff --git a/src/SAWScript/TopLevel.hs b/src/SAWScript/TopLevel.hs index 8db01b48e3..c9599fb477 100644 --- a/src/SAWScript/TopLevel.hs +++ b/src/SAWScript/TopLevel.hs @@ -19,6 +19,8 @@ module SAWScript.TopLevel , getTopLevelRW , localOptions , putTopLevelRW + , makeCheckpoint + , restoreCheckpoint ) where import SAWScript.Value diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index ba98b105c6..fe6d2affd8 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -591,10 +591,9 @@ data TopLevelCheckpoint = TopLevelRW SharedContextCheckpoint -makeCheckpoint :: TopLevel TopLevelCheckpoint -makeCheckpoint = - do rw <- getTopLevelRW - scc <- io (checkpointSharedContext (rwSharedContext rw)) +makeCheckpoint :: TopLevelRW -> IO TopLevelCheckpoint +makeCheckpoint rw = + do scc <- checkpointSharedContext (rwSharedContext rw) return (TopLevelCheckpoint rw scc) restoreCheckpoint :: TopLevelCheckpoint -> TopLevel () @@ -603,13 +602,12 @@ restoreCheckpoint chk = rw' <- io (combineRW chk rw) putTopLevelRW rw' - -- | Capture the current state of the TopLevel monad -- and return an action that, if invoked, resets -- the state back to that point. checkpoint :: TopLevel (() -> TopLevel ()) -checkpoint = - do chk <- makeCheckpoint +checkpoint = TopLevel_ $ + do chk <- liftIO . makeCheckpoint =<< get return $ \_ -> do printOutLnTop Info "Restoring state from checkpoint" restoreCheckpoint chk From bbb8055263e1538b42ba134309762b9150e09387 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 23 Jun 2022 16:21:28 -0700 Subject: [PATCH 10/14] Add a `saw_assert` override function with the following signature: ``` void saw_assert( uint32_t ); ``` This allows the program source to directly assert a proposition inline which is then assumed as part of the path condition. This can sometimes help the path sat checker by stating helpful lemmas whose proof can be deferred to the VC-checking phase. It can also be helpful for program/proof exploration, allowing the user to directly state inline hypotheses about program behavior, and then attempt to prove them. --- src/SAWScript/Crucible/LLVM/Builtins.hs | 36 ++++++++++++++++++++++--- 1 file changed, 32 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index a2042501b3..0b883eaa8f 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -17,9 +17,11 @@ Stability : provisional {-# LANGUAGE ParallelListComp #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE RankNTypes #-} +{-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-orphans #-} @@ -130,6 +132,7 @@ import qualified Control.Monad.Trans.Maybe as MaybeT import Data.Parameterized.Classes import Data.Parameterized.NatRepr import Data.Parameterized.Some +import qualified Data.Parameterized.Context as Ctx -- cryptol import qualified Cryptol.TypeCheck.Type as Cryptol @@ -164,13 +167,13 @@ import qualified Lang.Crucible.LLVM.Bytes as Crucible import qualified Lang.Crucible.LLVM.Intrinsics as Crucible import qualified Lang.Crucible.LLVM.MemModel as Crucible import qualified Lang.Crucible.LLVM.MemType as Crucible +import Lang.Crucible.LLVM.QQ( llvmOvr ) import qualified Lang.Crucible.LLVM.Translation as Crucible import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible -- parameterized-utils import qualified Data.Parameterized.TraversableFC as Ctx -import qualified Data.Parameterized.Context as Ctx -- saw-core import Verifier.SAW.FiniteValue (ppFirstOrderValue) @@ -1782,10 +1785,10 @@ setupLLVMCrucibleContext pathSat lm action = let globals = Crucible.llvmGlobals (Crucible.llvmMemVar ctx) mem let setupMem = - do -- register the callable override functions - Crucible.register_llvm_overrides llvm_mod [] [] ctx - -- register all the functions defined in the LLVM module + do -- register all the functions defined in the LLVM module Crucible.registerLazyModule (handleTranslationWarning opts) mtrans + -- register the callable override functions + Crucible.register_llvm_overrides llvm_mod saw_llvm_overrides saw_llvm_overrides ctx let initExecState = Crucible.InitialState simctx globals Crucible.defaultAbortHandler Crucible.UnitRepr $ @@ -1819,6 +1822,31 @@ handleTranslationWarning opts (Crucible.LLVMTranslationWarning s p msg) = -------------------------------------------------------------------------------- +saw_llvm_overrides :: + ( Crucible.IsSymInterface sym, Crucible.HasLLVMAnn sym, Crucible.HasPtrWidth wptr ) => + [Crucible.OverrideTemplate p sym arch rtp l a] +saw_llvm_overrides = + [ Crucible.basic_llvm_override saw_assert_override + ] + +saw_assert_override :: + ( Crucible.IsSymInterface sym, Crucible.HasLLVMAnn sym, Crucible.HasPtrWidth wptr ) => + Crucible.LLVMOverride p sym + (Crucible.EmptyCtx Crucible.::> Crucible.BVType 32) + Crucible.UnitType +saw_assert_override = + [llvmOvr| void @saw_assert( i32 ) |] + (\_memOps bak (Ctx.Empty Ctx.:> p) -> + do let sym = Crucible.backendGetSym bak + let msg = Crucible.GenericSimError "saw_assert" + liftIO $ + do loc <- W4.getCurrentProgramLoc sym + cond <- W4.bvIsNonzero sym (Crucible.regValue p) + putStrLn $ unlines ["SAW assert!", show loc, show (W4.printSymExpr cond)] + Crucible.addDurableAssertion bak (Crucible.LabeledPred cond (Crucible.SimError loc msg)) + Crucible.addAssumption bak (Crucible.GenericAssumption loc "crucible_assume" cond) + ) + baseCryptolType :: Crucible.BaseTypeRepr tp -> Maybe Cryptol.Type baseCryptolType bt = case bt of From 4101e38ae63bb8ae84c60816f7b8005b9c5a496c Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 6 Jun 2022 10:08:23 -0700 Subject: [PATCH 11/14] Add a proof script version of `subshell` --- saw/Main.hs | 3 +- saw/SAWScript/REPL/Command.hs | 6 +- saw/SAWScript/REPL/Monad.hs | 68 ++++++++++++++++++--- src/SAWScript/Interpreter.hs | 109 +++++++++++++++++++++++++--------- src/SAWScript/Value.hs | 20 +++++++ 5 files changed, 166 insertions(+), 40 deletions(-) diff --git a/saw/Main.hs b/saw/Main.hs index f8a611dc41..d942ed546d 100644 --- a/saw/Main.hs +++ b/saw/Main.hs @@ -43,12 +43,13 @@ main = do [] -> checkZ3 opts'' *> REPL.run opts'' _ | runInteractively opts'' -> checkZ3 opts'' *> REPL.run opts'' [file] -> checkZ3 opts'' *> - processFile (AIGProxy AIG.compactProxy) opts'' file subsh `catch` + processFile (AIGProxy AIG.compactProxy) opts'' file subsh proofSubsh`catch` (\(ErrorCall msg) -> err opts'' msg) (_:_) -> err opts'' "Multiple files not yet supported." (_, _, errs) -> do hPutStrLn stderr (concat errs ++ usageInfo header options) exitProofUnknown where subsh = Just (REPL.subshell (REPL.replBody Nothing (return ()))) + proofSubsh = Just (REPL.proof_subshell (REPL.replBody Nothing (return ()))) header = "Usage: saw [OPTION...] [-I | file]" checkZ3 opts = do p <- findExecutable "z3" diff --git a/saw/SAWScript/REPL/Command.hs b/saw/SAWScript/REPL/Command.hs index addf1fd963..df278eb073 100644 --- a/saw/SAWScript/REPL/Command.hs +++ b/saw/SAWScript/REPL/Command.hs @@ -221,7 +221,11 @@ sawScriptCmd str = do let tokens = SAWScript.Lexer.lexSAW replFileName str case SAWScript.Parser.parseStmtSemi tokens of Left err -> io $ print err - Right stmt -> void $ liftTopLevel (interpretStmt True stmt) + Right stmt -> + do mr <- getProofStateRef + case mr of + Nothing -> void $ liftTopLevel (interpretStmt True stmt) + Just r -> void $ liftProofScript (interpretStmt True stmt) r replFileName :: String replFileName = "" diff --git a/saw/SAWScript/REPL/Monad.hs b/saw/SAWScript/REPL/Monad.hs index abdd8aa870..74e5b03638 100644 --- a/saw/SAWScript/REPL/Monad.hs +++ b/saw/SAWScript/REPL/Monad.hs @@ -6,6 +6,7 @@ Maintainer : huffman Stability : provisional -} {-# LANGUAGE CPP #-} +{-# LANGUAGE LambdaCase #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE ScopedTypeVariables #-} @@ -22,7 +23,9 @@ module SAWScript.REPL.Monad ( , catchOther , exceptionProtect , liftTopLevel + , liftProofScript , subshell + , proof_subshell , Refs(..) -- ** Errors @@ -50,6 +53,7 @@ module SAWScript.REPL.Monad ( , getValueEnvironment , getEnvironment, modifyEnvironment, putEnvironment , getEnvironmentRef + , getProofStateRef , getSAWScriptNames ) where @@ -69,7 +73,8 @@ import Control.Applicative (Applicative(..), pure, (<*>)) #endif import Control.Monad (unless, ap, void) import Control.Monad.Reader (ask) -import Control.Monad.State (put, get) +import Control.Monad.State (put, get, StateT(..)) +import Control.Monad.Except (ExceptT(..), runExceptT) import Control.Monad.IO.Class (liftIO) import qualified Control.Monad.Fail as Fail import Data.IORef (IORef, newIORef, readIORef, modifyIORef, writeIORef) @@ -91,9 +96,13 @@ import qualified Data.AIG.CompactGraph as AIG import SAWScript.AST (Located(getVal)) import SAWScript.Interpreter (buildTopLevelEnv) import SAWScript.Options (Options) +import SAWScript.Proof (ProofState, ProofResult(..), psGoals) import SAWScript.TopLevel (TopLevelRO(..), TopLevelRW(..), TopLevel(..), runTopLevel, makeCheckpoint, restoreCheckpoint) -import SAWScript.Value (AIGProxy(..), mergeLocalEnv, IsValue, Value) +import SAWScript.Value + ( AIGProxy(..), mergeLocalEnv, IsValue, Value + , ProofScript(..), showsProofResult, toValue + ) import Verifier.SAW (SharedContext) deriving instance Typeable AIG.Proxy @@ -106,6 +115,7 @@ data Refs = Refs , eIsBatch :: Bool , eTopLevelRO :: TopLevelRO , environment :: IORef TopLevelRW + , proofState :: Maybe (IORef ProofState) } -- | Initial, empty environment. @@ -119,13 +129,9 @@ defaultRefs isBatch opts = , eIsBatch = isBatch , eTopLevelRO = ro , environment = rwRef + , proofState = Nothing } --- | Build up the prompt for the REPL. -mkPrompt :: Bool {- ^ is batch -} -> String -mkPrompt batch - | batch = "" - | otherwise = "sawscript> " mkTitle :: Refs -> String mkTitle _refs = "sawscript" @@ -154,11 +160,33 @@ subshell (REPL m) = TopLevel_ $ , eIsBatch = False , eTopLevelRO = ro , environment = rwRef + , proofState = Nothing } m refs readIORef rwRef put rw' +proof_subshell :: REPL () -> ProofScript () +proof_subshell (REPL m) = + ProofScript $ ExceptT $ StateT $ \proofSt -> + do ro <- ask + rw <- get + (rw', outProofSt) <- liftIO $ + do contRef <- newIORef True + rwRef <- newIORef rw + proofRef <- newIORef proofSt + let refs = Refs + { eContinue = contRef + , eIsBatch = False + , eTopLevelRO = ro + , environment = rwRef + , proofState = Just proofRef + } + m refs + (,) <$> readIORef rwRef <*> readIORef proofRef + put rw' + return (Right (), outProofSt) + instance Functor REPL where {-# INLINE fmap #-} fmap f m = REPL (\ ref -> fmap f (unREPL m ref)) @@ -292,6 +320,18 @@ liftTopLevel m = writeIORef ref rw' return v +liftProofScript :: IsValue a => ProofScript a -> IORef ProofState -> REPL Value +liftProofScript m ref = + liftTopLevel $ + do st <- liftIO $ readIORef ref + (res, st') <- runStateT (runExceptT (unProofScript m)) st + liftIO $ writeIORef ref st' + case res of + Left (stats, cex) -> + do ppOpts <- rwPPOpts <$> get + fail (showsProofResult ppOpts (InvalidProof stats cex st') "") + Right x -> return (toValue x) + -- Primitives ------------------------------------------------------------------ io :: IO a -> REPL a @@ -308,7 +348,15 @@ modifyRef r f = REPL (\refs -> modifyIORef (r refs) f) -- | Construct the prompt for the current environment. getPrompt :: REPL String -getPrompt = mkPrompt <$> (REPL (return . eIsBatch)) +getPrompt = + do batch <- REPL (return . eIsBatch) + if batch then return "" + else + getProofStateRef >>= \case + Nothing -> return "sawscript> " + Just psr -> + do ps <- io (readIORef psr) + return ("proof ("++show (length (psGoals ps))++")> ") shouldContinue :: REPL Bool shouldContinue = readRef eContinue @@ -420,6 +468,9 @@ getTopLevelRO = REPL (return . eTopLevelRO) getEnvironmentRef :: REPL (IORef TopLevelRW) getEnvironmentRef = environment <$> getRefs +getProofStateRef :: REPL (Maybe (IORef ProofState)) +getProofStateRef = proofState <$> getRefs + getEnvironment :: REPL TopLevelRW getEnvironment = readRef environment @@ -449,4 +500,3 @@ data EnvVal | EnvNum !Int | EnvBool Bool deriving (Show) - diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 4b13b05350..ad2221e693 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -15,6 +15,7 @@ Stability : provisional {-# LANGUAGE OverlappingInstances #-} #endif {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE ViewPatterns #-} @@ -26,6 +27,7 @@ module SAWScript.Interpreter , processFile , buildTopLevelEnv , primDocEnv + , InteractiveMonad(..) ) where @@ -262,7 +264,13 @@ stmtInterpreter :: StmtInterpreter stmtInterpreter ro rw stmts = fst <$> runTopLevel (withLocalEnv emptyLocal (interpretStmts stmts)) ro rw -processStmtBind :: Bool -> SS.Pattern -> Maybe SS.Type -> SS.Expr -> TopLevel () +processStmtBind :: + InteractiveMonad m => + Bool -> + SS.Pattern -> + Maybe SS.Type -> + SS.Expr -> + m () processStmtBind printBinds pat _mc expr = do -- mx mt let (mx, mt) = case pat of SS.PWild t -> (Nothing, t) @@ -270,18 +278,18 @@ processStmtBind printBinds pat _mc expr = do -- mx mt _ -> (Nothing, Nothing) let it = SS.Located "it" "it" SS.PosREPL let lname = maybe it id mx - let ctx = SS.tContext SS.TopLevel + ctx <- SS.tContext <$> getMonadContext let expr' = case mt of Nothing -> expr Just t -> SS.TSig expr (SS.tBlock ctx t) let decl = SS.Decl (SS.getPos expr) pat Nothing expr' - rw <- getMergedEnv + rw <- liftTopLevel getMergedEnv let opts = rwPPOpts rw - ~(SS.Decl _ _ (Just schema) expr'') <- + ~(SS.Decl _ _ (Just schema) expr'') <- liftTopLevel $ either failTypecheck return $ checkDecl (rwTypes rw) (rwTypedef rw) decl - val <- interpret expr'' + val <- liftTopLevel $ interpret expr'' -- Run the resulting TopLevel action. (result, ty) <- @@ -289,7 +297,7 @@ processStmtBind printBinds pat _mc expr = do -- mx mt SS.Forall [] t -> case t of SS.TyCon SS.BlockCon [c, t'] | c == ctx -> do - result <- SAWScript.Value.fromValue val + result <- actionFromValue val return (result, t') _ -> return (val, t) _ -> fail $ "Not a monomorphic type: " ++ SS.pShow schema @@ -299,39 +307,70 @@ processStmtBind printBinds pat _mc expr = do -- mx mt -- Print non-unit result if it was not bound to a variable case pat of SS.PWild _ | printBinds && not (isVUnit result) -> - printOutLnTop Info (showsPrecValue opts 0 result "") + liftTopLevel $ printOutLnTop Info (showsPrecValue opts 0 result "") _ -> return () -- Print function type if result was a function case ty of - SS.TyCon SS.FunCon _ -> printOutLnTop Info $ getVal lname ++ " : " ++ SS.pShow ty + SS.TyCon SS.FunCon _ -> + liftTopLevel $ printOutLnTop Info $ getVal lname ++ " : " ++ SS.pShow ty _ -> return () - rw' <- getTopLevelRW - putTopLevelRW =<< bindPatternEnv pat (Just (SS.tMono ty)) result rw' + liftTopLevel $ + do rw' <- getTopLevelRW + putTopLevelRW =<< bindPatternEnv pat (Just (SS.tMono ty)) result rw' + + +class (Monad m, MonadFail m) => InteractiveMonad m where + liftTopLevel :: TopLevel a -> m a + withTopLevel :: (forall b. TopLevel b -> TopLevel b) -> m a -> m a + actionFromValue :: FromValue a => Value -> m a + getMonadContext :: m SS.Context + +instance InteractiveMonad TopLevel where + liftTopLevel m = m + withTopLevel f m = f m + actionFromValue = fromValue + getMonadContext = return SS.TopLevel + +instance InteractiveMonad ProofScript where + liftTopLevel m = scriptTopLevel m + withTopLevel f (ProofScript m) = ProofScript (underExceptT (underStateT f) m) + actionFromValue = fromValue + getMonadContext = return SS.ProofScript -- | Interpret a block-level statement in the TopLevel monad. -interpretStmt :: +interpretStmt :: InteractiveMonad m => Bool {-^ whether to print non-unit result values -} -> SS.Stmt -> - TopLevel () + m () interpretStmt printBinds stmt = let ?fileReader = BS.readFile in case stmt of - SS.StmtBind pos pat mc expr -> withPosition pos (processStmtBind printBinds pat mc expr) - SS.StmtLet _ dg -> do rw <- getTopLevelRW - dg' <- either failTypecheck return $ - checkDeclGroup (rwTypes rw) (rwTypedef rw) dg - env <- interpretDeclGroup dg' - withLocalEnv env getMergedEnv >>= putTopLevelRW - SS.StmtCode _ lstr -> do rw <- getTopLevelRW - sc <- getSharedContext - --io $ putStrLn $ "Processing toplevel code: " ++ show lstr - --showCryptolEnv - cenv' <- io $ CEnv.parseDecls sc (rwCryptol rw) $ locToInput lstr - putTopLevelRW $ rw { rwCryptol = cenv' } - --showCryptolEnv + + SS.StmtBind pos pat mc expr -> + withTopLevel (withPosition pos) (processStmtBind printBinds pat mc expr) + + SS.StmtLet _ dg -> + liftTopLevel $ + do rw <- getTopLevelRW + dg' <- either failTypecheck return $ + checkDeclGroup (rwTypes rw) (rwTypedef rw) dg + env <- interpretDeclGroup dg' + withLocalEnv env getMergedEnv >>= putTopLevelRW + + SS.StmtCode _ lstr -> + liftTopLevel $ + do rw <- getTopLevelRW + sc <- getSharedContext + --io $ putStrLn $ "Processing toplevel code: " ++ show lstr + --showCryptolEnv + cenv' <- io $ CEnv.parseDecls sc (rwCryptol rw) $ locToInput lstr + putTopLevelRW $ rw { rwCryptol = cenv' } + --showCryptolEnv + SS.StmtImport _ imp -> + liftTopLevel $ do rw <- getTopLevelRW sc <- getSharedContext --showCryptolEnv @@ -342,8 +381,10 @@ interpretStmt printBinds stmt = putTopLevelRW $ rw { rwCryptol = cenv' } --showCryptolEnv - SS.StmtTypedef _ name ty -> do rw <- getTopLevelRW - putTopLevelRW $ addTypedef (getVal name) ty rw + SS.StmtTypedef _ name ty -> + liftTopLevel $ + do rw <- getTopLevelRW + putTopLevelRW $ addTypedef (getVal name) ty rw interpretFile :: FilePath -> Bool {- ^ run main? -} -> TopLevel () interpretFile file runMain = do @@ -414,6 +455,7 @@ buildTopLevelEnv proxy opts = , roBasicSS = ss , roStackTrace = [] , roSubshell = fail "Subshells not supported" + , roProofSubshell = fail "Proof subshells not supported" , roLocalEnv = [] } let bic = BuiltinContext { @@ -464,16 +506,20 @@ processFile :: Options -> FilePath -> Maybe (TopLevel ()) -> + Maybe (ProofScript ()) -> IO () -processFile proxy opts file mbSubshell = do +processFile proxy opts file mbSubshell mbProofSubshell = do (_, ro, rw) <- buildTopLevelEnv proxy opts let ro' = case mbSubshell of Nothing -> ro Just m -> ro{ roSubshell = m } + 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 + _ <- runTopLevel (interpretFile file' True) ro'' rw `X.catch` (handleException opts) setCurrentDirectory oldpath return () @@ -817,6 +863,11 @@ primitives = Map.fromList Experimental [] + , prim "proof_subshell" "() -> ProofScript ()" + (\ _ _ -> proofScriptSubshell) + Experimental + [] + , prim "define" "String -> Term -> TopLevel Term" (pureVal definePrim) Current diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index fe6d2affd8..d041f08770 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -399,6 +399,12 @@ toplevelSubshell = VLambda $ \_ -> env <- getLocalEnv return (VTopLevel (toValue <$> withLocalEnv env m)) +proofScriptSubshell :: Value +proofScriptSubshell = VLambda $ \_ -> + do m <- roProofSubshell <$> ask + env <- getLocalEnv + return (VProofScript (toValue <$> withLocalEnvProof env m)) + applyValue :: Value -> Value -> TopLevel Value applyValue (VLambda f) x = f x applyValue _ _ = throwTopLevel "applyValue" @@ -477,6 +483,12 @@ data TopLevelRO = -- ^ An action for entering a subshell. This -- may raise an error if the current execution -- mode doesn't support subshells (e.g., the remote API) + + , roProofSubshell :: ProofScript () + -- ^ An action for entering a subshell in proof mode. This + -- may raise an error if the current execution + -- mode doesn't support subshells (e.g., the remote API) + , roLocalEnv :: LocalEnv } @@ -624,6 +636,10 @@ withPosition pos (TopLevel_ m) = TopLevel_ (local (\ro -> ro{ roPosition = pos } withLocalEnv :: LocalEnv -> TopLevel a -> TopLevel a withLocalEnv env (TopLevel_ m) = TopLevel_ (local (\ro -> ro{ roLocalEnv = env }) m) +withLocalEnvProof :: LocalEnv -> ProofScript a -> ProofScript a +withLocalEnvProof env (ProofScript m) = + ProofScript (underExceptT (underStateT (withLocalEnv env)) m) + getLocalEnv :: TopLevel LocalEnv getLocalEnv = TopLevel_ (asks roLocalEnv) @@ -915,6 +931,10 @@ instance IsValue a => IsValue (ProofScript a) where instance FromValue a => FromValue (ProofScript a) where fromValue (VProofScript m) = fmap fromValue m + -- Inject top-level computations automatically into proof scripts. + -- This should really only possible in interactive subshell mode; otherwise + -- the type system should keep this from happening. + fromValue (VTopLevel m) = ProofScript (lift (lift (fmap fromValue m))) fromValue (VReturn v) = return (fromValue v) fromValue (VBind pos m1 v2) = ProofScript $ do v1 <- underExceptT (underStateT (withPosition pos)) (unProofScript (fromValue m1)) From eef3bb4858be1bc0aff3cb9af694c314c81e0e77 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Thu, 23 Jun 2022 16:33:08 -0700 Subject: [PATCH 12/14] Update saw-remote-api --- saw-remote-api/src/SAWServer.hs | 1 + saw-remote-api/src/SAWServer/Eval.hs | 3 ++- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs index 08f3f40246..260a338356 100644 --- a/saw-remote-api/src/SAWServer.hs +++ b/saw-remote-api/src/SAWServer.hs @@ -212,6 +212,7 @@ initialState readFileFn = , roBasicSS = ss , roStackTrace = [] , roSubshell = fail "SAW server does not support subshells." + , roProofSubshell = fail "SAW server does not support subshells." , roLocalEnv = [] } rw = TopLevelRW diff --git a/saw-remote-api/src/SAWServer/Eval.hs b/saw-remote-api/src/SAWServer/Eval.hs index 7e783f32f2..de03e61f67 100644 --- a/saw-remote-api/src/SAWServer/Eval.hs +++ b/saw-remote-api/src/SAWServer/Eval.hs @@ -75,7 +75,8 @@ instance Doc.DescribedMethod (EvalParams Bool cryptolExpr) (EvalResult Bool) whe Doc.Paragraph [Doc.Text "The boolean value of the expresssion."]) ] -eval :: (TypedTerm -> SV.TopLevel a) -> EvalParams a Expression -> Argo.Command SAWState (EvalResult a) +eval :: (SV.FromValue a, SV.IsValue a) => + (TypedTerm -> SV.TopLevel a) -> EvalParams a Expression -> Argo.Command SAWState (EvalResult a) eval f params = do state <- Argo.getState fileReader <- Argo.getFileReader From b8d17bc9d61f495d61a5e4f097281c78b446969a Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 25 Jul 2022 10:55:42 -0700 Subject: [PATCH 13/14] Add help strings to the `subshell` and `proof_subshell` commands. --- src/SAWScript/Interpreter.hs | 36 ++++++++++++++++++++++++++++++++---- 1 file changed, 32 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index ad2221e693..7fc5bf2fd8 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -839,7 +839,7 @@ primitives = Map.fromList [ "Call-with-current-continuation." , "" , "This is a highly experimental control operator that can be used" - , "to capure the surrounding top-level computation as a continuation." + , "to capture the surrounding top-level computation as a continuation." , "The consequences of delaying and reentering the current continuation" , "may be somewhat unpredictable, so use this operator with great caution." ] @@ -847,7 +847,7 @@ primitives = Map.fromList , prim "checkpoint" "TopLevel (() -> TopLevel ())" (pureVal checkpoint) Experimental - [ "Capure the current state of the SAW interpreter, and return" + [ "Capture the current state of the SAW interpreter, and return" , "A TopLevel monadic action that, if invoked, will reset the" , "state of the interpreter back to to what it was at the" , "moment checkpoint was invoked." @@ -861,12 +861,40 @@ primitives = Map.fromList , prim "subshell" "() -> TopLevel ()" (\_ _ -> toplevelSubshell) Experimental - [] + [ "Open an interactive subshell instance in the context where" + , "'subshell' was called. This works either from within execution" + , "of a outer shell instance, or from interpreting a file in batch" + , "mode. Enter the end-of-file character in your terminal (Ctrl^D, usually)" + , "to exit the subshell and resume execution." + , "" + , "This command is especially useful in conjunction with the 'checkpoint'" + , "and 'callcc' commands, which allow state reset capabilities and the capturing" + , "of the calling context." + , "" + , "Note that, due to the way the SAW script interpreter works, changes made" + , "to a script file in which the 'subshell' command directly appears will" + , "NOT affect subsequent execution following a 'checkpoint' or 'callcc' use." + , "However, changes made in a file that executed via 'include' WILL affect" + , "restarted executions, as the 'include' command will read and parse the" + , "file from scratch." + ] , prim "proof_subshell" "() -> ProofScript ()" (\ _ _ -> proofScriptSubshell) Experimental - [] + [ "Open an interactive subshell instance in the context of the current proof." + , "This allows the user to interactively execute 'ProofScript' tactic commands" + , "directly on the command line an examine their effects using, e.g., 'print_goal'." + , "In proof mode, the command prompt will change to 'proof (n)', where the 'n'" + , "indicates the number of subgoals remaining to proof for the current overall goal." + , "In this mode, tactic commands applied will only affect the current subgoal." + , "When a particular subgoal is completed, the next subgoal will automatically become" + , "the active subgoal. An overall goal is completed when all subgoals are proved" + , "and the current number of subgoals is 0." + , "" + , "Enter the end-of-file character in your terminal (Ctrl^D, usually) to exit the proof" + , "subshell and resume execution." + ] , prim "define" "String -> Term -> TopLevel Term" (pureVal definePrim) From 6952456e6e7fa9f6613c59b96489e6ecb8f7b751 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 25 Jul 2022 12:44:45 -0700 Subject: [PATCH 14/14] Add a `proof_checkpoint` command that captures and allows the user to restore proof states. --- src/SAWScript/Interpreter.hs | 14 ++++++++++++++ src/SAWScript/Value.hs | 9 +++++++++ 2 files changed, 23 insertions(+) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 7fc5bf2fd8..d10529e645 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -896,6 +896,20 @@ primitives = Map.fromList , "subshell and resume execution." ] + , prim "proof_checkpoint" "ProofScript (() -> ProofScript ())" + (pureVal proof_checkpoint) + Experimental + [ "Capture the current state of the proof and return a" + , "ProofScript monadic action that, if invoked, will reset the" + , "state of the proof back to to what it was at the" + , "moment checkpoint was invoked." + , "" + , "NOTE that this facility is highly experimental and may not" + , "be entirely reliable. It is intended only for proof development" + , "where it can speed up the process of experimenting with" + , "mid-proof changes. Finalized proofs should not use this facility." + ] + , prim "define" "String -> Term -> TopLevel Term" (pureVal definePrim) Current diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs index d041f08770..3ea01878f6 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -624,6 +624,15 @@ checkpoint = TopLevel_ $ do printOutLnTop Info "Restoring state from checkpoint" restoreCheckpoint chk +-- | Capture the current proof state and return an +-- action that, if invoked, resets the state back to that point. +proof_checkpoint :: ProofScript (() -> ProofScript ()) +proof_checkpoint = + do ps <- get + return $ \_ -> + do scriptTopLevel (printOutLnTop Info "Restoring proof state from checkpoint") + put ps + throwTopLevel :: String -> TopLevel a throwTopLevel msg = do pos <- getPosition