Skip to content

Commit a2f18b4

Browse files
robdockinsrobdockins
committed
WIP, add a proof script version of subshell 
1 parent b58f3f0 commit a2f18b4

File tree

5 files changed

+156
-34
lines changed

5 files changed

+156
-34
lines changed

‎saw/Main.hs

+2-1
Original file line numberDiff line numberDiff line change
@@ -43,12 +43,13 @@ main = do
4343
[] -> checkZ3 opts'' *> REPL.run opts''
4444
_ | runInteractively opts'' -> checkZ3 opts'' *> REPL.run opts''
4545
[file] -> checkZ3 opts'' *>
46-
processFile (AIGProxy AIG.compactProxy) opts'' file subsh `catch`
46+
processFile (AIGProxy AIG.compactProxy) opts'' file subsh proofSubsh`catch`
4747
(\(ErrorCall msg) -> err opts'' msg)
4848
(_:_) -> err opts'' "Multiple files not yet supported."
4949
(_, _, errs) -> do hPutStrLn stderr (concat errs ++ usageInfo header options)
5050
exitProofUnknown
5151
where subsh = Just (REPL.subshell (REPL.replBody Nothing (return ())))
52+
proofSubsh = Just (REPL.proof_subshell (REPL.replBody Nothing (return ())))
5253
header = "Usage: saw [OPTION...] [-I | file]"
5354
checkZ3 opts = do
5455
p <- findExecutable "z3"

‎saw/SAWScript/REPL/Command.hs

+5-1
Original file line numberDiff line numberDiff line change
@@ -221,7 +221,11 @@ sawScriptCmd str = do
221221
let tokens = SAWScript.Lexer.lexSAW replFileName str
222222
case SAWScript.Parser.parseStmtSemi tokens of
223223
Left err -> io $ print err
224-
Right stmt -> void $ liftTopLevel (interpretStmt True stmt)
224+
Right stmt ->
225+
do mr <- getProofStateRef
226+
case mr of
227+
Nothing -> void $ liftTopLevel (interpretStmt True stmt)
228+
Just r -> void $ liftProofScript (interpretStmt True stmt) r
225229

226230
replFileName :: String
227231
replFileName = "<stdin>"

‎saw/SAWScript/REPL/Monad.hs

+49-3
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,9 @@ module SAWScript.REPL.Monad (
2222
, catchOther
2323
, exceptionProtect
2424
, liftTopLevel
25+
, liftProofScript
2526
, subshell
27+
, proof_subshell
2628
, Refs(..)
2729

2830
-- ** Errors
@@ -50,6 +52,7 @@ module SAWScript.REPL.Monad (
5052
, getValueEnvironment
5153
, getEnvironment, modifyEnvironment, putEnvironment
5254
, getEnvironmentRef
55+
, getProofStateRef
5356
, getSAWScriptNames
5457
) where
5558

@@ -69,7 +72,8 @@ import Control.Applicative (Applicative(..), pure, (<*>))
6972
#endif
7073
import Control.Monad (unless, ap, void)
7174
import Control.Monad.Reader (ask)
72-
import Control.Monad.State (put, get)
75+
import Control.Monad.State (put, get, StateT(..))
76+
import Control.Monad.Except (ExceptT(..), runExceptT)
7377
import Control.Monad.IO.Class (liftIO)
7478
import qualified Control.Monad.Fail as Fail
7579
import Data.IORef (IORef, newIORef, readIORef, modifyIORef, writeIORef)
@@ -91,9 +95,13 @@ import qualified Data.AIG.CompactGraph as AIG
9195
import SAWScript.AST (Located(getVal))
9296
import SAWScript.Interpreter (buildTopLevelEnv)
9397
import SAWScript.Options (Options)
98+
import SAWScript.Proof (ProofState, ProofResult(..))
9499
import SAWScript.TopLevel (TopLevelRO(..), TopLevelRW(..), TopLevel(..), runTopLevel,
95100
makeCheckpoint, restoreCheckpoint)
96-
import SAWScript.Value (AIGProxy(..), mergeLocalEnv, IsValue, Value)
101+
import SAWScript.Value
102+
( AIGProxy(..), mergeLocalEnv, IsValue, Value
103+
, ProofScript(..), showsProofResult, toValue
104+
)
97105
import Verifier.SAW (SharedContext)
98106

99107
deriving instance Typeable AIG.Proxy
@@ -106,6 +114,7 @@ data Refs = Refs
106114
, eIsBatch :: Bool
107115
, eTopLevelRO :: TopLevelRO
108116
, environment :: IORef TopLevelRW
117+
, proofState :: Maybe (IORef ProofState)
109118
}
110119

111120
-- | Initial, empty environment.
@@ -119,6 +128,7 @@ defaultRefs isBatch opts =
119128
, eIsBatch = isBatch
120129
, eTopLevelRO = ro
121130
, environment = rwRef
131+
, proofState = Nothing
122132
}
123133

124134
-- | Build up the prompt for the REPL.
@@ -154,11 +164,33 @@ subshell (REPL m) = TopLevel_ $
154164
, eIsBatch = False
155165
, eTopLevelRO = ro
156166
, environment = rwRef
167+
, proofState = Nothing
157168
}
158169
m refs
159170
readIORef rwRef
160171
put rw'
161172

173+
proof_subshell :: REPL () -> ProofScript ()
174+
proof_subshell (REPL m) =
175+
ProofScript $ ExceptT $ StateT $ \proofSt ->
176+
do ro <- ask
177+
rw <- get
178+
(rw', outProofSt) <- liftIO $
179+
do contRef <- newIORef True
180+
rwRef <- newIORef rw
181+
proofRef <- newIORef proofSt
182+
let refs = Refs
183+
{ eContinue = contRef
184+
, eIsBatch = False
185+
, eTopLevelRO = ro
186+
, environment = rwRef
187+
, proofState = Just proofRef
188+
}
189+
m refs
190+
(,) <$> readIORef rwRef <*> readIORef proofRef
191+
put rw'
192+
return (Right (), outProofSt)
193+
162194
instance Functor REPL where
163195
{-# INLINE fmap #-}
164196
fmap f m = REPL (\ ref -> fmap f (unREPL m ref))
@@ -292,6 +324,18 @@ liftTopLevel m =
292324
writeIORef ref rw'
293325
return v
294326

327+
liftProofScript :: IsValue a => ProofScript a -> IORef ProofState -> REPL Value
328+
liftProofScript m ref =
329+
liftTopLevel $
330+
do st <- liftIO $ readIORef ref
331+
(res, st') <- runStateT (runExceptT (unProofScript m)) st
332+
liftIO $ writeIORef ref st'
333+
case res of
334+
Left (stats, cex) ->
335+
do ppOpts <- rwPPOpts <$> get
336+
fail (showsProofResult ppOpts (InvalidProof stats cex st') "")
337+
Right x -> return (toValue x)
338+
295339
-- Primitives ------------------------------------------------------------------
296340

297341
io :: IO a -> REPL a
@@ -420,6 +464,9 @@ getTopLevelRO = REPL (return . eTopLevelRO)
420464
getEnvironmentRef :: REPL (IORef TopLevelRW)
421465
getEnvironmentRef = environment <$> getRefs
422466

467+
getProofStateRef :: REPL (Maybe (IORef ProofState))
468+
getProofStateRef = proofState <$> getRefs
469+
423470
getEnvironment :: REPL TopLevelRW
424471
getEnvironment = readRef environment
425472

@@ -449,4 +496,3 @@ data EnvVal
449496
| EnvNum !Int
450497
| EnvBool Bool
451498
deriving (Show)
452-

‎src/SAWScript/Interpreter.hs

+80-29
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Stability : provisional
1515
{-# LANGUAGE OverlappingInstances #-}
1616
#endif
1717
{-# LANGUAGE OverloadedStrings #-}
18+
{-# LANGUAGE RankNTypes #-}
1819
{-# LANGUAGE ScopedTypeVariables #-}
1920
{-# LANGUAGE TupleSections #-}
2021
{-# LANGUAGE ViewPatterns #-}
@@ -26,6 +27,7 @@ module SAWScript.Interpreter
2627
, processFile
2728
, buildTopLevelEnv
2829
, primDocEnv
30+
, InteractiveMonad(..)
2931
)
3032
where
3133

@@ -262,34 +264,40 @@ stmtInterpreter :: StmtInterpreter
262264
stmtInterpreter ro rw stmts =
263265
fst <$> runTopLevel (withLocalEnv emptyLocal (interpretStmts stmts)) ro rw
264266

265-
processStmtBind :: Bool -> SS.Pattern -> Maybe SS.Type -> SS.Expr -> TopLevel ()
267+
processStmtBind ::
268+
InteractiveMonad m =>
269+
Bool ->
270+
SS.Pattern ->
271+
Maybe SS.Type ->
272+
SS.Expr ->
273+
m ()
266274
processStmtBind printBinds pat _mc expr = do -- mx mt
267275
let (mx, mt) = case pat of
268276
SS.PWild t -> (Nothing, t)
269277
SS.PVar x t -> (Just x, t)
270278
_ -> (Nothing, Nothing)
271279
let it = SS.Located "it" "it" SS.PosREPL
272280
let lname = maybe it id mx
273-
let ctx = SS.tContext SS.TopLevel
281+
ctx <- SS.tContext <$> getMonadContext
274282
let expr' = case mt of
275283
Nothing -> expr
276284
Just t -> SS.TSig expr (SS.tBlock ctx t)
277285
let decl = SS.Decl (SS.getPos expr) pat Nothing expr'
278-
rw <- getMergedEnv
286+
rw <- liftTopLevel getMergedEnv
279287
let opts = rwPPOpts rw
280288

281-
~(SS.Decl _ _ (Just schema) expr'') <-
289+
~(SS.Decl _ _ (Just schema) expr'') <- liftTopLevel $
282290
either failTypecheck return $ checkDecl (rwTypes rw) (rwTypedef rw) decl
283291

284-
val <- interpret expr''
292+
val <- liftTopLevel $ interpret expr''
285293

286294
-- Run the resulting TopLevel action.
287295
(result, ty) <-
288296
case schema of
289297
SS.Forall [] t ->
290298
case t of
291299
SS.TyCon SS.BlockCon [c, t'] | c == ctx -> do
292-
result <- SAWScript.Value.fromValue val
300+
result <- actionFromValue val
293301
return (result, t')
294302
_ -> return (val, t)
295303
_ -> fail $ "Not a monomorphic type: " ++ SS.pShow schema
@@ -299,39 +307,70 @@ processStmtBind printBinds pat _mc expr = do -- mx mt
299307
-- Print non-unit result if it was not bound to a variable
300308
case pat of
301309
SS.PWild _ | printBinds && not (isVUnit result) ->
302-
printOutLnTop Info (showsPrecValue opts 0 result "")
310+
liftTopLevel $ printOutLnTop Info (showsPrecValue opts 0 result "")
303311
_ -> return ()
304312

305313
-- Print function type if result was a function
306314
case ty of
307-
SS.TyCon SS.FunCon _ -> printOutLnTop Info $ getVal lname ++ " : " ++ SS.pShow ty
315+
SS.TyCon SS.FunCon _ ->
316+
liftTopLevel $ printOutLnTop Info $ getVal lname ++ " : " ++ SS.pShow ty
308317
_ -> return ()
309318

310-
rw' <- getTopLevelRW
311-
putTopLevelRW =<< bindPatternEnv pat (Just (SS.tMono ty)) result rw'
319+
liftTopLevel $
320+
do rw' <- getTopLevelRW
321+
putTopLevelRW =<< bindPatternEnv pat (Just (SS.tMono ty)) result rw'
322+
323+
324+
class (Monad m, MonadFail m) => InteractiveMonad m where
325+
liftTopLevel :: TopLevel a -> m a
326+
withTopLevel :: (forall b. TopLevel b -> TopLevel b) -> m a -> m a
327+
actionFromValue :: FromValue a => Value -> m a
328+
getMonadContext :: m SS.Context
329+
330+
instance InteractiveMonad TopLevel where
331+
liftTopLevel m = m
332+
withTopLevel f m = f m
333+
actionFromValue = fromValue
334+
getMonadContext = return SS.TopLevel
335+
336+
instance InteractiveMonad ProofScript where
337+
liftTopLevel m = scriptTopLevel m
338+
withTopLevel f (ProofScript m) = ProofScript (underExceptT (underStateT f) m)
339+
actionFromValue = fromValue
340+
getMonadContext = return SS.ProofScript
312341

313342
-- | Interpret a block-level statement in the TopLevel monad.
314-
interpretStmt ::
343+
interpretStmt :: InteractiveMonad m =>
315344
Bool {-^ whether to print non-unit result values -} ->
316345
SS.Stmt ->
317-
TopLevel ()
346+
m ()
318347
interpretStmt printBinds stmt =
319348
let ?fileReader = BS.readFile in
320349
case stmt of
321-
SS.StmtBind pos pat mc expr -> withPosition pos (processStmtBind printBinds pat mc expr)
322-
SS.StmtLet _ dg -> do rw <- getTopLevelRW
323-
dg' <- either failTypecheck return $
324-
checkDeclGroup (rwTypes rw) (rwTypedef rw) dg
325-
env <- interpretDeclGroup dg'
326-
withLocalEnv env getMergedEnv >>= putTopLevelRW
327-
SS.StmtCode _ lstr -> do rw <- getTopLevelRW
328-
sc <- getSharedContext
329-
--io $ putStrLn $ "Processing toplevel code: " ++ show lstr
330-
--showCryptolEnv
331-
cenv' <- io $ CEnv.parseDecls sc (rwCryptol rw) $ locToInput lstr
332-
putTopLevelRW $ rw { rwCryptol = cenv' }
333-
--showCryptolEnv
350+
351+
SS.StmtBind pos pat mc expr ->
352+
withTopLevel (withPosition pos) (processStmtBind printBinds pat mc expr)
353+
354+
SS.StmtLet _ dg ->
355+
liftTopLevel $
356+
do rw <- getTopLevelRW
357+
dg' <- either failTypecheck return $
358+
checkDeclGroup (rwTypes rw) (rwTypedef rw) dg
359+
env <- interpretDeclGroup dg'
360+
withLocalEnv env getMergedEnv >>= putTopLevelRW
361+
362+
SS.StmtCode _ lstr ->
363+
liftTopLevel $
364+
do rw <- getTopLevelRW
365+
sc <- getSharedContext
366+
--io $ putStrLn $ "Processing toplevel code: " ++ show lstr
367+
--showCryptolEnv
368+
cenv' <- io $ CEnv.parseDecls sc (rwCryptol rw) $ locToInput lstr
369+
putTopLevelRW $ rw { rwCryptol = cenv' }
370+
--showCryptolEnv
371+
334372
SS.StmtImport _ imp ->
373+
liftTopLevel $
335374
do rw <- getTopLevelRW
336375
sc <- getSharedContext
337376
--showCryptolEnv
@@ -342,8 +381,10 @@ interpretStmt printBinds stmt =
342381
putTopLevelRW $ rw { rwCryptol = cenv' }
343382
--showCryptolEnv
344383

345-
SS.StmtTypedef _ name ty -> do rw <- getTopLevelRW
346-
putTopLevelRW $ addTypedef (getVal name) ty rw
384+
SS.StmtTypedef _ name ty ->
385+
liftTopLevel $
386+
do rw <- getTopLevelRW
387+
putTopLevelRW $ addTypedef (getVal name) ty rw
347388

348389
interpretFile :: FilePath -> Bool {- ^ run main? -} -> TopLevel ()
349390
interpretFile file runMain = do
@@ -414,6 +455,7 @@ buildTopLevelEnv proxy opts =
414455
, roBasicSS = ss
415456
, roStackTrace = []
416457
, roSubshell = fail "Subshells not supported"
458+
, roProofSubshell = fail "Proof subshells not supported"
417459
, roLocalEnv = []
418460
}
419461
let bic = BuiltinContext {
@@ -464,16 +506,20 @@ processFile ::
464506
Options ->
465507
FilePath ->
466508
Maybe (TopLevel ()) ->
509+
Maybe (ProofScript ()) ->
467510
IO ()
468-
processFile proxy opts file mbSubshell = do
511+
processFile proxy opts file mbSubshell mbProofSubshell = do
469512
(_, ro, rw) <- buildTopLevelEnv proxy opts
470513
let ro' = case mbSubshell of
471514
Nothing -> ro
472515
Just m -> ro{ roSubshell = m }
516+
let ro'' = case mbProofSubshell of
517+
Nothing -> ro'
518+
Just m -> ro'{ roProofSubshell = m }
473519
oldpath <- getCurrentDirectory
474520
file' <- canonicalizePath file
475521
setCurrentDirectory (takeDirectory file')
476-
_ <- runTopLevel (interpretFile file' True) ro' rw
522+
_ <- runTopLevel (interpretFile file' True) ro'' rw
477523
`X.catch` (handleException opts)
478524
setCurrentDirectory oldpath
479525
return ()
@@ -817,6 +863,11 @@ primitives = Map.fromList
817863
Experimental
818864
[]
819865

866+
, prim "proof_subshell" "() -> ProofScript ()"
867+
(\ _ _ -> proofScriptSubshell)
868+
Experimental
869+
[]
870+
820871
, prim "define" "String -> Term -> TopLevel Term"
821872
(pureVal definePrim)
822873
Current

0 commit comments

Comments
 (0)