mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
Parameterize module system over filesystem access
Adds the ability for clients of Cryptol-the-library to provide their own means of accessing disk, as a sort of lightweight VFS. This will be used for caching multiple concurrent states in SAW.
This commit is contained in:
parent
e2cf7d95ad
commit
d952f168e6
@ -1645,7 +1645,7 @@ This module implements the core functionality of the `:eval
|
||||
running the reference evaluator on an expression.
|
||||
|
||||
> evaluate :: Expr -> M.ModuleCmd Value
|
||||
> evaluate expr (_,modEnv) = return (Right (evalExpr env expr, modEnv), [])
|
||||
> evaluate expr (_, _, modEnv) = return (Right (evalExpr env expr, modEnv), [])
|
||||
> where
|
||||
> extDgs = concatMap mDecls (M.loadedModules modEnv)
|
||||
> env = foldl evalDeclGroup mempty extDgs
|
||||
|
@ -46,10 +46,11 @@ import Cryptol.Parser.NoPat (RemovePatterns)
|
||||
import qualified Cryptol.TypeCheck.AST as T
|
||||
import qualified Cryptol.Utils.Ident as M
|
||||
|
||||
import Data.ByteString (ByteString)
|
||||
|
||||
-- Public Interface ------------------------------------------------------------
|
||||
|
||||
type ModuleCmd a = (E.EvalOpts,ModuleEnv) -> IO (ModuleRes a)
|
||||
type ModuleCmd a = (E.EvalOpts, FilePath -> IO ByteString, ModuleEnv) -> IO (ModuleRes a)
|
||||
|
||||
type ModuleRes a = (Either ModuleError (a,ModuleEnv), [ModuleWarning])
|
||||
|
||||
@ -62,19 +63,21 @@ findModule n env = runModuleM env (Base.findModule n)
|
||||
|
||||
-- | Load the module contained in the given file.
|
||||
loadModuleByPath :: FilePath -> ModuleCmd (ModulePath,T.Module)
|
||||
loadModuleByPath path (evo,env) = runModuleM (evo,resetModuleEnv env) $ do
|
||||
unloadModule ((InFile path ==) . lmFilePath)
|
||||
m <- Base.loadModuleByPath path
|
||||
setFocusedModule (T.mName m)
|
||||
return (InFile path,m)
|
||||
loadModuleByPath path (evo, byteReader, env) =
|
||||
runModuleM (evo, byteReader, resetModuleEnv env) $ do
|
||||
unloadModule ((InFile path ==) . lmFilePath)
|
||||
m <- Base.loadModuleByPath path
|
||||
setFocusedModule (T.mName m)
|
||||
return (InFile path,m)
|
||||
|
||||
-- | Load the given parsed module.
|
||||
loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.Module)
|
||||
loadModuleByName n (evo,env) = runModuleM (evo,resetModuleEnv env) $ do
|
||||
unloadModule ((n ==) . lmName)
|
||||
(path,m') <- Base.loadModuleFrom (FromModule n)
|
||||
setFocusedModule (T.mName m')
|
||||
return (path,m')
|
||||
loadModuleByName n (evo, byteReader, env) =
|
||||
runModuleM (evo, byteReader, resetModuleEnv env) $ do
|
||||
unloadModule ((n ==) . lmName)
|
||||
(path,m') <- Base.loadModuleFrom (FromModule n)
|
||||
setFocusedModule (T.mName m')
|
||||
return (path,m')
|
||||
|
||||
-- Extended Environments -------------------------------------------------------
|
||||
|
||||
|
@ -55,7 +55,6 @@ import Cryptol.Transform.MonoValues (rewModule)
|
||||
|
||||
import qualified Control.Exception as X
|
||||
import Control.Monad (unless,when)
|
||||
import qualified Data.ByteString as B
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Monoid ((<>))
|
||||
import Data.Text.Encoding (decodeUtf8')
|
||||
@ -112,9 +111,10 @@ noPat a = do
|
||||
|
||||
parseModule :: ModulePath -> ModuleM (Fingerprint, P.Module PName)
|
||||
parseModule path = do
|
||||
getBytes <- getByteReader
|
||||
|
||||
bytesRes <- case path of
|
||||
InFile p -> io (X.try (B.readFile p))
|
||||
InFile p -> io (X.try (getBytes p))
|
||||
InMem _ bs -> pure (Right bs)
|
||||
|
||||
bytes <- case bytesRes of
|
||||
@ -412,7 +412,9 @@ checkSingleModule how isrc path m = do
|
||||
-- this is a more-or-less obsolete feature, we are just not doing
|
||||
-- ot for now.
|
||||
e <- case path of
|
||||
InFile p -> io (removeIncludesModule p m)
|
||||
InFile p -> do
|
||||
r <- getByteReader
|
||||
io (removeIncludesModule r p m)
|
||||
InMem {} -> pure (Right m)
|
||||
|
||||
nim <- case e of
|
||||
|
@ -36,6 +36,7 @@ import Cryptol.Utils.Logger(Logger)
|
||||
import qualified Control.Monad.Fail as Fail
|
||||
import Control.Monad.IO.Class
|
||||
import Control.Exception (IOException)
|
||||
import Data.ByteString (ByteString)
|
||||
import Data.Function (on)
|
||||
import Data.Maybe (isJust)
|
||||
import Data.Text.Encoding.Error (UnicodeException)
|
||||
@ -296,16 +297,21 @@ renamerWarnings ws
|
||||
|
||||
-- Module System Monad ---------------------------------------------------------
|
||||
|
||||
data RO = RO { roLoading :: [ImportSource]
|
||||
, roEvalOpts :: EvalOpts
|
||||
}
|
||||
data RO m =
|
||||
RO { roLoading :: [ImportSource]
|
||||
, roEvalOpts :: EvalOpts
|
||||
, roFileReader :: FilePath -> m ByteString
|
||||
}
|
||||
|
||||
emptyRO :: EvalOpts -> RO
|
||||
emptyRO ev = RO { roLoading = [], roEvalOpts = ev }
|
||||
emptyRO :: EvalOpts -> (FilePath -> m ByteString) -> RO m
|
||||
emptyRO ev fileReader =
|
||||
RO { roLoading = [], roEvalOpts = ev, roFileReader = fileReader }
|
||||
|
||||
newtype ModuleT m a = ModuleT
|
||||
{ unModuleT :: ReaderT RO (StateT ModuleEnv
|
||||
(ExceptionT ModuleError (WriterT [ModuleWarning] m))) a
|
||||
{ unModuleT :: ReaderT (RO m)
|
||||
(StateT ModuleEnv
|
||||
(ExceptionT ModuleError
|
||||
(WriterT [ModuleWarning] m))) a
|
||||
}
|
||||
|
||||
instance Monad m => Functor (ModuleT m) where
|
||||
@ -345,27 +351,36 @@ instance MonadIO m => MonadIO (ModuleT m) where
|
||||
liftIO m = lift $ liftIO m
|
||||
|
||||
runModuleT :: Monad m
|
||||
=> (EvalOpts,ModuleEnv)
|
||||
=> (EvalOpts, FilePath -> m ByteString, ModuleEnv)
|
||||
-> ModuleT m a
|
||||
-> m (Either ModuleError (a, ModuleEnv), [ModuleWarning])
|
||||
runModuleT (ev,env) m =
|
||||
runModuleT (ev, byteReader, env) m =
|
||||
runWriterT
|
||||
$ runExceptionT
|
||||
$ runStateT env
|
||||
$ runReaderT (emptyRO ev)
|
||||
$ runReaderT (emptyRO ev byteReader)
|
||||
$ unModuleT m
|
||||
|
||||
type ModuleM = ModuleT IO
|
||||
|
||||
runModuleM :: (EvalOpts, ModuleEnv) -> ModuleM a
|
||||
runModuleM :: (EvalOpts, FilePath -> IO ByteString, ModuleEnv) -> ModuleM a
|
||||
-> IO (Either ModuleError (a,ModuleEnv),[ModuleWarning])
|
||||
runModuleM = runModuleT
|
||||
|
||||
|
||||
|
||||
io :: BaseM m IO => IO a -> ModuleT m a
|
||||
io m = ModuleT (inBase m)
|
||||
|
||||
getByteReader :: Monad m => ModuleT m (FilePath -> m ByteString)
|
||||
getByteReader = ModuleT $ do
|
||||
RO { roFileReader = readFileBytes } <- ask
|
||||
return readFileBytes
|
||||
|
||||
readBytes :: Monad m => FilePath -> ModuleT m ByteString
|
||||
readBytes fn = do
|
||||
fileReader <- getByteReader
|
||||
ModuleT $ lift $ lift $ lift $ lift $ fileReader fn
|
||||
|
||||
getModuleEnv :: Monad m => ModuleT m ModuleEnv
|
||||
getModuleEnv = ModuleT get
|
||||
|
||||
|
@ -19,7 +19,7 @@ import Control.DeepSeq
|
||||
import qualified Control.Exception as X
|
||||
import qualified Control.Monad.Fail as Fail
|
||||
|
||||
import qualified Data.ByteString as B
|
||||
import Data.ByteString (ByteString)
|
||||
import Data.Either (partitionEithers)
|
||||
import Data.Text(Text)
|
||||
import qualified Data.Text.Encoding as T (decodeUtf8')
|
||||
@ -36,8 +36,12 @@ import Cryptol.Parser.ParserUtils
|
||||
import Cryptol.Parser.Unlit (guessPreProc)
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
removeIncludesModule :: FilePath -> Module PName -> IO (Either [IncludeError] (Module PName))
|
||||
removeIncludesModule modPath m = runNoIncM modPath (noIncludeModule m)
|
||||
removeIncludesModule ::
|
||||
(FilePath -> IO ByteString) ->
|
||||
FilePath ->
|
||||
Module PName ->
|
||||
IO (Either [IncludeError] (Module PName))
|
||||
removeIncludesModule reader modPath m = runNoIncM reader modPath (noIncludeModule m)
|
||||
|
||||
data IncludeError
|
||||
= IncludeFailed (Located FilePath)
|
||||
@ -70,16 +74,18 @@ ppIncludeError ie = case ie of
|
||||
newtype NoIncM a = M
|
||||
{ unM :: ReaderT Env (ExceptionT [IncludeError] IO) a }
|
||||
|
||||
data Env = Env { envSeen :: [Located FilePath]
|
||||
data Env = Env { envSeen :: [Located FilePath]
|
||||
-- ^ Files that have been loaded
|
||||
, envIncPath :: FilePath
|
||||
, envIncPath :: FilePath
|
||||
-- ^ The path that includes are relative to
|
||||
, envFileReader :: FilePath -> IO ByteString
|
||||
-- ^ How to load files
|
||||
}
|
||||
|
||||
runNoIncM :: FilePath -> NoIncM a -> IO (Either [IncludeError] a)
|
||||
runNoIncM sourcePath m =
|
||||
runNoIncM :: (FilePath -> IO ByteString) -> FilePath -> NoIncM a -> IO (Either [IncludeError] a)
|
||||
runNoIncM reader sourcePath m =
|
||||
do incPath <- getIncPath sourcePath
|
||||
runM (unM m) Env { envSeen = [], envIncPath = incPath }
|
||||
runM (unM m) Env { envSeen = [], envIncPath = incPath, envFileReader = reader }
|
||||
|
||||
tryNoIncM :: NoIncM a -> NoIncM (Either [IncludeError] a)
|
||||
tryNoIncM m = M (try (unM m))
|
||||
@ -192,8 +198,9 @@ resolveInclude lf = pushPath lf $ do
|
||||
-- | Read a file referenced by an include.
|
||||
readInclude :: Located FilePath -> NoIncM Text
|
||||
readInclude path = do
|
||||
readBytes <- envFileReader <$> M ask
|
||||
file <- fromIncPath (thing path)
|
||||
sourceBytes <- B.readFile file `failsWith` handler
|
||||
sourceBytes <- readBytes file `failsWith` handler
|
||||
sourceText <- X.evaluate (T.decodeUtf8' sourceBytes) `failsWith` handler
|
||||
case sourceText of
|
||||
Left encodingErr -> M (raise [IncludeDecodeFailed path encodingErr])
|
||||
|
@ -1548,7 +1548,7 @@ liftModuleCmd :: M.ModuleCmd a -> REPL a
|
||||
liftModuleCmd cmd =
|
||||
do evo <- getEvalOpts
|
||||
env <- getModuleEnv
|
||||
moduleCmdResult =<< io (cmd (evo,env))
|
||||
moduleCmdResult =<< io (cmd (evo, BS.readFile, env))
|
||||
|
||||
moduleCmdResult :: M.ModuleRes a -> REPL a
|
||||
moduleCmdResult (res,ws0) = do
|
||||
|
@ -160,7 +160,7 @@ thmSMTResults :: SBV.ThmResult -> [SBV.SMTResult]
|
||||
thmSMTResults (SBV.ThmResult r) = [r]
|
||||
|
||||
proverError :: String -> M.ModuleCmd (Maybe String, ProverResult)
|
||||
proverError msg (_,modEnv) =
|
||||
proverError msg (_, _, modEnv) =
|
||||
return (Right ((Nothing, ProverError msg), modEnv), [])
|
||||
|
||||
|
||||
@ -403,9 +403,9 @@ processResults evo ProverCommand{..} ts results =
|
||||
-- of executing the query.
|
||||
satProve :: SBVProverConfig -> ProverCommand -> M.ModuleCmd (Maybe String, ProverResult)
|
||||
satProve proverCfg pc@ProverCommand {..} =
|
||||
protectStack proverError $ \(evo,modEnv) ->
|
||||
protectStack proverError $ \(evo, byteReader, modEnv) ->
|
||||
|
||||
M.runModuleM (evo,modEnv) $ do
|
||||
M.runModuleM (evo, byteReader, modEnv) $ do
|
||||
|
||||
let lPutStrLn = logPutStrLn (Eval.evalLogger evo)
|
||||
|
||||
@ -424,8 +424,8 @@ satProve proverCfg pc@ProverCommand {..} =
|
||||
-- the SMT input file corresponding to the given prover command.
|
||||
satProveOffline :: SBVProverConfig -> ProverCommand -> M.ModuleCmd (Either String String)
|
||||
satProveOffline _proverCfg pc@ProverCommand {..} =
|
||||
protectStack (\msg (_,modEnv) -> return (Right (Left msg, modEnv), [])) $
|
||||
\(evOpts,modEnv) -> do
|
||||
protectStack (\msg (_,_,modEnv) -> return (Right (Left msg, modEnv), [])) $
|
||||
\(evOpts, _, modEnv) -> do
|
||||
let isSat = case pcQueryType of
|
||||
ProveQuery -> False
|
||||
SafetyQuery -> False
|
||||
|
@ -194,7 +194,7 @@ setupProver nm =
|
||||
|
||||
|
||||
proverError :: String -> M.ModuleCmd (Maybe String, ProverResult)
|
||||
proverError msg (_,modEnv) =
|
||||
proverError msg (_, _, modEnv) =
|
||||
return (Right ((Nothing, ProverError msg), modEnv), [])
|
||||
|
||||
|
||||
@ -285,8 +285,8 @@ satProve ::
|
||||
M.ModuleCmd (Maybe String, ProverResult)
|
||||
|
||||
satProve solverCfg hashConsing ProverCommand {..} =
|
||||
protectStack proverError \(evo, modEnv) ->
|
||||
M.runModuleM (evo,modEnv)
|
||||
protectStack proverError \(evo, byteReader, modEnv) ->
|
||||
M.runModuleM (evo, byteReader, modEnv)
|
||||
do sym <- liftIO makeSym
|
||||
logData <- M.withLogger doLog ()
|
||||
start <- liftIO getCurrentTime
|
||||
@ -343,8 +343,8 @@ satProveOffline (W4Portfolio (p:|_)) hashConsing cmd outputContinuation =
|
||||
satProveOffline (W4ProverConfig p) hashConsing cmd outputContinuation
|
||||
|
||||
satProveOffline (W4ProverConfig (AnAdapter adpt)) hashConsing ProverCommand {..} outputContinuation =
|
||||
protectStack onError \(evo,modEnv) ->
|
||||
M.runModuleM (evo,modEnv)
|
||||
protectStack onError \(evo,byteReader,modEnv) ->
|
||||
M.runModuleM (evo,byteReader,modEnv)
|
||||
do sym <- liftIO makeSym
|
||||
ok <- prepareQuery sym ProverCommand { .. }
|
||||
liftIO
|
||||
@ -363,7 +363,7 @@ satProveOffline (W4ProverConfig (AnAdapter adpt)) hashConsing ProverCommand {..}
|
||||
when hashConsing (W4.startCaching sym)
|
||||
pure sym
|
||||
|
||||
onError msg (_,modEnv) = pure (Right (Just msg, modEnv), [])
|
||||
onError msg (_,_,modEnv) = pure (Right (Just msg, modEnv), [])
|
||||
|
||||
|
||||
decSatNum :: SatNum -> SatNum
|
||||
|
@ -59,13 +59,13 @@ modify f = get >>= (set . f)
|
||||
-- type-specialized versions of all functions called (transitively) by
|
||||
-- the body of the expression.
|
||||
specialize :: Expr -> M.ModuleCmd Expr
|
||||
specialize expr (ev,modEnv) = run $ do
|
||||
specialize expr (ev, byteReader, modEnv) = run $ do
|
||||
let extDgs = allDeclGroups modEnv
|
||||
let (tparams, expr') = destETAbs expr
|
||||
spec' <- specializeEWhere expr' extDgs
|
||||
return (foldr ETAbs spec' tparams)
|
||||
where
|
||||
run = M.runModuleT (ev,modEnv) . fmap fst . runSpecT Map.empty
|
||||
run = M.runModuleT (ev, byteReader, modEnv) . fmap fst . runSpecT Map.empty
|
||||
|
||||
specializeExpr :: Expr -> SpecM Expr
|
||||
specializeExpr expr =
|
||||
|
Loading…
Reference in New Issue
Block a user