Proof development primitives

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) $

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 }});

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)

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,10 @@ initialState readFileFn =
 #endif
                 , roInitWorkDir = cwd
                 , roBasicSS = ss
-                , roTheoremDB = db
+                , roStackTrace = []
+                , roSubshell = fail "SAW server does not support subshells."
+                , roProofSubshell = fail "SAW server does not support subshells."
+                , roLocalEnv = []
                 }
          rw = TopLevelRW
                 { rwValues = mempty
@@ -222,6 +224,8 @@ initialState readFileFn =
                 , rwMonadify = defaultMonEnv
                 , rwMRSolverEnv = emptyMREnv
                 , rwPPOpts = defaultPPOpts
+                , rwTheoremDB = db
+                , rwSharedContext = sc
                 , rwJVMTrans = jvmTrans
                 , rwPrimsAvail = mempty
                 , rwSMTArrayMemoryModel = False

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

saw-remote-api/src/SAWServer/TopLevel.hs

@@ -5,31 +5,28 @@ 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)
 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)

saw-script.cabal

@@ -213,6 +213,7 @@ executable saw
     , exceptions
     , filepath
     , haskeline
+    , mtl
     , QuickCheck
     , transformers
     , saw-script

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,14 @@ 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 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 header = "Usage: saw [OPTION...] [-I | file]"
+  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"
           unless (isJust p)
@@ -55,3 +59,4 @@ main = do
           when (verbLevel opts >= Error)
             (hPutStrLn stderr msg)
           exitProofUnknown
+

saw/SAWScript/REPL/Command.hs

@@ -30,14 +30,15 @@ module SAWScript.REPL.Command (
 
 --import Verifier.SAW.SharedTerm (SharedContext)
 
+
 import SAWScript.REPL.Monad
 import SAWScript.REPL.Trie
 import SAWScript.Position (getPos)
 
 import Cryptol.Parser (ParseError())
-import Cryptol.Utils.PP hiding ((</>))
 
-import Control.Monad (guard)
+import Control.Monad (guard, void)
+
 import Data.Char (isSpace,isPunctuation,isSymbol)
 import Data.Function (on)
 import Data.List (intercalate)
@@ -56,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 --------------------------------------------------------------------
@@ -139,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 "" >> print e)
-    handlerFail s = io (putStrLn "" >> putStrLn s)
+  Command cmd -> exceptionProtect cmd
 
   Unknown cmd -> io (putStrLn ("Unknown command: " ++ cmd))
 
@@ -161,7 +156,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
@@ -172,7 +167,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) ]
 
@@ -227,9 +222,10 @@ sawScriptCmd str = do
   case SAWScript.Parser.parseStmtSemi tokens of
     Left err -> io $ print err
     Right stmt ->
-      do ro <- getTopLevelRO
-         rwRef <- getEnvironmentRef
-         io $ runTopLevel (interpretStmt True stmt) ro rwRef
+      do mr <- getProofStateRef
+         case mr of
+           Nothing -> void $ liftTopLevel (interpretStmt True stmt)
+           Just r  -> void $ liftProofScript (interpretStmt True stmt) r
 
 replFileName :: String
 replFileName = "<stdin>"

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