From 7f8f5ef11d93073ed2aba9bd49f33198d06fad15 Mon Sep 17 00:00:00 2001 From: Rob Dockins Date: Mon, 6 Jun 2022 10:08:23 -0700 Subject: [PATCH] WIP, add a proof script version of `subshell` --- saw/Main.hs | 3 +- saw/SAWScript/REPL/Command.hs | 6 +- saw/SAWScript/REPL/Monad.hs | 52 +++++++++++++++- src/SAWScript/Interpreter.hs | 109 +++++++++++++++++++++++++--------- src/SAWScript/Value.hs | 20 +++++++ 5 files changed, 156 insertions(+), 34 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..f92fd51462 100644 --- a/saw/SAWScript/REPL/Monad.hs +++ b/saw/SAWScript/REPL/Monad.hs @@ -22,7 +22,9 @@ module SAWScript.REPL.Monad ( , catchOther , exceptionProtect , liftTopLevel + , liftProofScript , subshell + , proof_subshell , Refs(..) -- ** Errors @@ -50,6 +52,7 @@ module SAWScript.REPL.Monad ( , getValueEnvironment , getEnvironment, modifyEnvironment, putEnvironment , getEnvironmentRef + , getProofStateRef , getSAWScriptNames ) where @@ -69,7 +72,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 +95,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(..)) 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 +114,7 @@ data Refs = Refs , eIsBatch :: Bool , eTopLevelRO :: TopLevelRO , environment :: IORef TopLevelRW + , proofState :: Maybe (IORef ProofState) } -- | Initial, empty environment. @@ -119,6 +128,7 @@ defaultRefs isBatch opts = , eIsBatch = isBatch , eTopLevelRO = ro , environment = rwRef + , proofState = Nothing } -- | Build up the prompt for the REPL. @@ -154,11 +164,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 +324,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 @@ -420,6 +464,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 +496,3 @@ data EnvVal | EnvNum !Int | EnvBool Bool deriving (Show) - diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 2c17480d78..d14011676f 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))