mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-23 14:16:39 +03:00
Track file content fingerprints alongside loaded modules
This commit is contained in:
parent
00b58277bb
commit
5786fcf190
@ -47,6 +47,7 @@ library
|
|||||||
bytestring >= 0.10,
|
bytestring >= 0.10,
|
||||||
array >= 0.4,
|
array >= 0.4,
|
||||||
containers >= 0.5,
|
containers >= 0.5,
|
||||||
|
cryptohash-sha1 >= 0.11 && < 0.12,
|
||||||
deepseq >= 1.3,
|
deepseq >= 1.3,
|
||||||
directory >= 1.2.2.0,
|
directory >= 1.2.2.0,
|
||||||
filepath >= 1.3,
|
filepath >= 1.3,
|
||||||
@ -100,6 +101,7 @@ library
|
|||||||
Cryptol.ModuleSystem,
|
Cryptol.ModuleSystem,
|
||||||
Cryptol.ModuleSystem.Base,
|
Cryptol.ModuleSystem.Base,
|
||||||
Cryptol.ModuleSystem.Env,
|
Cryptol.ModuleSystem.Env,
|
||||||
|
Cryptol.ModuleSystem.Fingerprint,
|
||||||
Cryptol.ModuleSystem.Interface,
|
Cryptol.ModuleSystem.Interface,
|
||||||
Cryptol.ModuleSystem.Monad,
|
Cryptol.ModuleSystem.Monad,
|
||||||
Cryptol.ModuleSystem.Name,
|
Cryptol.ModuleSystem.Name,
|
||||||
|
@ -15,6 +15,7 @@
|
|||||||
module Cryptol.ModuleSystem.Base where
|
module Cryptol.ModuleSystem.Base where
|
||||||
|
|
||||||
import Cryptol.ModuleSystem.Env (DynamicEnv(..), deIfaceDecls)
|
import Cryptol.ModuleSystem.Env (DynamicEnv(..), deIfaceDecls)
|
||||||
|
import Cryptol.ModuleSystem.Fingerprint
|
||||||
import Cryptol.ModuleSystem.Interface
|
import Cryptol.ModuleSystem.Interface
|
||||||
import Cryptol.ModuleSystem.Monad
|
import Cryptol.ModuleSystem.Monad
|
||||||
import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap)
|
import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap)
|
||||||
@ -48,13 +49,12 @@ import Cryptol.Prelude (writePreludeContents)
|
|||||||
|
|
||||||
import Cryptol.Transform.MonoValues (rewModule)
|
import Cryptol.Transform.MonoValues (rewModule)
|
||||||
|
|
||||||
import Control.DeepSeq
|
|
||||||
import qualified Control.Exception as X
|
import qualified Control.Exception as X
|
||||||
import Control.Monad (unless,when)
|
import Control.Monad (unless,when)
|
||||||
|
import qualified Data.ByteString as B
|
||||||
import Data.Maybe (fromMaybe)
|
import Data.Maybe (fromMaybe)
|
||||||
import Data.Monoid ((<>))
|
import Data.Monoid ((<>))
|
||||||
import Data.Text(Text)
|
import Data.Text.Encoding (decodeUtf8')
|
||||||
import qualified Data.Text.IO as T
|
|
||||||
import System.Directory (doesFileExist, canonicalizePath)
|
import System.Directory (doesFileExist, canonicalizePath)
|
||||||
import System.FilePath ( addExtension
|
import System.FilePath ( addExtension
|
||||||
, isAbsolute
|
, isAbsolute
|
||||||
@ -105,23 +105,28 @@ noPat a = do
|
|||||||
|
|
||||||
-- Parsing ---------------------------------------------------------------------
|
-- Parsing ---------------------------------------------------------------------
|
||||||
|
|
||||||
parseModule :: FilePath -> ModuleM (P.Module PName)
|
parseModule :: FilePath -> ModuleM (Fingerprint, P.Module PName)
|
||||||
parseModule path = do
|
parseModule path = do
|
||||||
|
|
||||||
e <- io $ X.try $ do
|
bytesRes <- io (X.try (B.readFile path))
|
||||||
bytes <- T.readFile path
|
|
||||||
return $!! bytes
|
bytes <- case bytesRes of
|
||||||
bytes <- case (e :: Either X.IOException Text) of
|
|
||||||
Right bytes -> return bytes
|
Right bytes -> return bytes
|
||||||
Left exn | IOE.isDoesNotExistError exn -> cantFindFile path
|
Left exn | IOE.isDoesNotExistError exn -> cantFindFile path
|
||||||
| otherwise -> otherIOError path exn
|
| otherwise -> otherIOError path exn
|
||||||
|
|
||||||
|
txt <- case decodeUtf8' bytes of
|
||||||
|
Right txt -> return txt
|
||||||
|
Left e -> badUtf8 path e
|
||||||
|
|
||||||
let cfg = P.defaultConfig
|
let cfg = P.defaultConfig
|
||||||
{ P.cfgSource = path
|
{ P.cfgSource = path
|
||||||
, P.cfgPreProc = P.guessPreProc path
|
, P.cfgPreProc = P.guessPreProc path
|
||||||
}
|
}
|
||||||
case P.parseModule cfg bytes of
|
|
||||||
Right pm -> return pm
|
case P.parseModule cfg txt of
|
||||||
|
Right pm -> let fp = fingerprint bytes
|
||||||
|
in fp `seq` return (fp, pm)
|
||||||
Left err -> moduleParseError path err
|
Left err -> moduleParseError path err
|
||||||
|
|
||||||
|
|
||||||
@ -132,7 +137,7 @@ loadModuleByPath :: FilePath -> ModuleM T.Module
|
|||||||
loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do
|
loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do
|
||||||
let fileName = takeFileName path
|
let fileName = takeFileName path
|
||||||
foundPath <- findFile fileName
|
foundPath <- findFile fileName
|
||||||
pm <- parseModule foundPath
|
(fp, pm) <- parseModule foundPath
|
||||||
let n = thing (P.mName pm)
|
let n = thing (P.mName pm)
|
||||||
|
|
||||||
-- Check whether this module name has already been loaded from a different file
|
-- Check whether this module name has already been loaded from a different file
|
||||||
@ -142,7 +147,7 @@ loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do
|
|||||||
path' <- io $ canonicalizePath foundPath
|
path' <- io $ canonicalizePath foundPath
|
||||||
case lookupModule n env of
|
case lookupModule n env of
|
||||||
-- loadModule will calculate the canonical path again
|
-- loadModule will calculate the canonical path again
|
||||||
Nothing -> doLoadModule (FromModule n) foundPath pm
|
Nothing -> doLoadModule (FromModule n) foundPath fp pm
|
||||||
Just lm
|
Just lm
|
||||||
| path' == loaded -> return (lmModule lm)
|
| path' == loaded -> return (lmModule lm)
|
||||||
| otherwise -> duplicateModuleName n path' loaded
|
| otherwise -> duplicateModuleName n path' loaded
|
||||||
@ -159,16 +164,18 @@ loadModuleFrom isrc =
|
|||||||
Nothing ->
|
Nothing ->
|
||||||
do path <- findModule n
|
do path <- findModule n
|
||||||
errorInFile path $
|
errorInFile path $
|
||||||
do pm <- parseModule path
|
do (fp, pm) <- parseModule path
|
||||||
m <- doLoadModule isrc path pm
|
m <- doLoadModule isrc path fp pm
|
||||||
return (path,m)
|
return (path,m)
|
||||||
|
|
||||||
-- | Load dependencies, typecheck, and add to the eval environment.
|
-- | Load dependencies, typecheck, and add to the eval environment.
|
||||||
doLoadModule :: ImportSource ->
|
doLoadModule ::
|
||||||
FilePath ->
|
ImportSource ->
|
||||||
P.Module PName ->
|
FilePath ->
|
||||||
ModuleM T.Module
|
Fingerprint ->
|
||||||
doLoadModule isrc path pm0 =
|
P.Module PName ->
|
||||||
|
ModuleM T.Module
|
||||||
|
doLoadModule isrc path fp pm0 =
|
||||||
loading isrc $
|
loading isrc $
|
||||||
do let pm = addPrelude pm0
|
do let pm = addPrelude pm0
|
||||||
loadDeps pm
|
loadDeps pm
|
||||||
@ -180,7 +187,7 @@ doLoadModule isrc path pm0 =
|
|||||||
-- extend the eval env, unless a functor.
|
-- extend the eval env, unless a functor.
|
||||||
unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv tcm)
|
unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv tcm)
|
||||||
canonicalPath <- io (canonicalizePath path)
|
canonicalPath <- io (canonicalizePath path)
|
||||||
loadedModule path canonicalPath tcm
|
loadedModule path canonicalPath fp tcm
|
||||||
|
|
||||||
return tcm
|
return tcm
|
||||||
where
|
where
|
||||||
|
@ -18,6 +18,7 @@ import Paths_cryptol (getDataDir)
|
|||||||
#endif
|
#endif
|
||||||
|
|
||||||
import Cryptol.Eval (EvalEnv)
|
import Cryptol.Eval (EvalEnv)
|
||||||
|
import Cryptol.ModuleSystem.Fingerprint
|
||||||
import Cryptol.ModuleSystem.Interface
|
import Cryptol.ModuleSystem.Interface
|
||||||
import Cryptol.ModuleSystem.Name (Supply,emptySupply)
|
import Cryptol.ModuleSystem.Name (Supply,emptySupply)
|
||||||
import qualified Cryptol.ModuleSystem.NamingEnv as R
|
import qualified Cryptol.ModuleSystem.NamingEnv as R
|
||||||
@ -248,13 +249,14 @@ instance Monoid LoadedModules where
|
|||||||
mappend l r = l <> r
|
mappend l r = l <> r
|
||||||
|
|
||||||
data LoadedModule = LoadedModule
|
data LoadedModule = LoadedModule
|
||||||
{ lmName :: ModName
|
{ lmName :: ModName
|
||||||
, lmFilePath :: FilePath
|
, lmFilePath :: FilePath
|
||||||
-- ^ The file path used to load this module (may not be canonical)
|
-- ^ The file path used to load this module (may not be canonical)
|
||||||
, lmCanonicalPath :: FilePath
|
, lmCanonicalPath :: FilePath
|
||||||
-- ^ The canonical version of the path of this module
|
-- ^ The canonical version of the path of this module
|
||||||
, lmInterface :: Iface
|
, lmInterface :: Iface
|
||||||
, lmModule :: T.Module
|
, lmModule :: T.Module
|
||||||
|
, lmFingerprint :: Fingerprint
|
||||||
} deriving (Show, Generic, NFData)
|
} deriving (Show, Generic, NFData)
|
||||||
|
|
||||||
-- | Has this module been loaded already.
|
-- | Has this module been loaded already.
|
||||||
@ -275,8 +277,8 @@ lookupModule mn me = search lmLoadedModules `mplus` search lmLoadedParamModules
|
|||||||
-- | Add a freshly loaded module. If it was previously loaded, then
|
-- | Add a freshly loaded module. If it was previously loaded, then
|
||||||
-- the new version is ignored.
|
-- the new version is ignored.
|
||||||
addLoadedModule ::
|
addLoadedModule ::
|
||||||
FilePath -> FilePath -> T.Module -> LoadedModules -> LoadedModules
|
FilePath -> FilePath -> Fingerprint -> T.Module -> LoadedModules -> LoadedModules
|
||||||
addLoadedModule path canonicalPath tm lm
|
addLoadedModule path canonicalPath fp tm lm
|
||||||
| isLoaded (T.mName tm) lm = lm
|
| isLoaded (T.mName tm) lm = lm
|
||||||
| T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded :
|
| T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded :
|
||||||
lmLoadedParamModules lm }
|
lmLoadedParamModules lm }
|
||||||
@ -284,11 +286,12 @@ addLoadedModule path canonicalPath tm lm
|
|||||||
lmLoadedModules lm ++ [loaded] }
|
lmLoadedModules lm ++ [loaded] }
|
||||||
where
|
where
|
||||||
loaded = LoadedModule
|
loaded = LoadedModule
|
||||||
{ lmName = T.mName tm
|
{ lmName = T.mName tm
|
||||||
, lmFilePath = path
|
, lmFilePath = path
|
||||||
, lmCanonicalPath = canonicalPath
|
, lmCanonicalPath = canonicalPath
|
||||||
, lmInterface = genIface tm
|
, lmInterface = genIface tm
|
||||||
, lmModule = tm
|
, lmModule = tm
|
||||||
|
, lmFingerprint = fp
|
||||||
}
|
}
|
||||||
|
|
||||||
-- | Remove a previously loaded module.
|
-- | Remove a previously loaded module.
|
||||||
|
40
src/Cryptol/ModuleSystem/Fingerprint.hs
Normal file
40
src/Cryptol/ModuleSystem/Fingerprint.hs
Normal file
@ -0,0 +1,40 @@
|
|||||||
|
-- |
|
||||||
|
-- Module : Cryptol.ModuleSystem.Fingerprint
|
||||||
|
-- Copyright : (c) 2019 Galois, Inc.
|
||||||
|
-- License : BSD3
|
||||||
|
-- Maintainer : cryptol@galois.com
|
||||||
|
-- Stability : provisional
|
||||||
|
-- Portability : portable
|
||||||
|
|
||||||
|
module Cryptol.ModuleSystem.Fingerprint
|
||||||
|
( Fingerprint
|
||||||
|
, fingerprint
|
||||||
|
, fingerprintFile
|
||||||
|
) where
|
||||||
|
|
||||||
|
import Control.DeepSeq (NFData (rnf))
|
||||||
|
import Crypto.Hash.SHA1 (hash)
|
||||||
|
import Data.ByteString (ByteString)
|
||||||
|
import System.IO.Error (IOError)
|
||||||
|
import Control.Exception (try)
|
||||||
|
import qualified Data.ByteString as B
|
||||||
|
|
||||||
|
newtype Fingerprint = Fingerprint ByteString
|
||||||
|
deriving (Eq, Show)
|
||||||
|
|
||||||
|
instance NFData Fingerprint where
|
||||||
|
rnf (Fingerprint fp) = rnf fp
|
||||||
|
|
||||||
|
-- | Compute a fingerprint for a bytestring.
|
||||||
|
fingerprint :: ByteString -> Fingerprint
|
||||||
|
fingerprint = Fingerprint . hash
|
||||||
|
|
||||||
|
-- | Attempt to compute the fingerprint of the file at the given path.
|
||||||
|
-- Returns 'Nothing' in the case of an error.
|
||||||
|
fingerprintFile :: FilePath -> IO (Maybe Fingerprint)
|
||||||
|
fingerprintFile path =
|
||||||
|
do res <- try (B.readFile path)
|
||||||
|
return $!
|
||||||
|
case res :: Either IOError ByteString of
|
||||||
|
Left{} -> Nothing
|
||||||
|
Right b -> Just $! fingerprint b
|
@ -16,6 +16,7 @@ import Cryptol.Eval (EvalEnv,EvalOpts(..))
|
|||||||
|
|
||||||
import qualified Cryptol.Eval.Monad as E
|
import qualified Cryptol.Eval.Monad as E
|
||||||
import Cryptol.ModuleSystem.Env
|
import Cryptol.ModuleSystem.Env
|
||||||
|
import Cryptol.ModuleSystem.Fingerprint
|
||||||
import Cryptol.ModuleSystem.Interface
|
import Cryptol.ModuleSystem.Interface
|
||||||
import Cryptol.ModuleSystem.Name (FreshM(..),Supply)
|
import Cryptol.ModuleSystem.Name (FreshM(..),Supply)
|
||||||
import Cryptol.ModuleSystem.Renamer
|
import Cryptol.ModuleSystem.Renamer
|
||||||
@ -37,6 +38,7 @@ import Control.Monad.IO.Class
|
|||||||
import Control.Exception (IOException)
|
import Control.Exception (IOException)
|
||||||
import Data.Function (on)
|
import Data.Function (on)
|
||||||
import Data.Maybe (isJust)
|
import Data.Maybe (isJust)
|
||||||
|
import Data.Text.Encoding.Error (UnicodeException)
|
||||||
import MonadLib
|
import MonadLib
|
||||||
|
|
||||||
import GHC.Generics (Generic)
|
import GHC.Generics (Generic)
|
||||||
@ -76,6 +78,8 @@ data ModuleError
|
|||||||
-- ^ Unable to find the module given, tried looking in these paths
|
-- ^ Unable to find the module given, tried looking in these paths
|
||||||
| CantFindFile FilePath
|
| CantFindFile FilePath
|
||||||
-- ^ Unable to open a file
|
-- ^ Unable to open a file
|
||||||
|
| BadUtf8 FilePath UnicodeException
|
||||||
|
-- ^ Bad UTF-8 encoding in while decoding this file
|
||||||
| OtherIOError FilePath IOException
|
| OtherIOError FilePath IOException
|
||||||
-- ^ Some other IO error occurred while reading this file
|
-- ^ Some other IO error occurred while reading this file
|
||||||
| ModuleParseError FilePath Parser.ParseError
|
| ModuleParseError FilePath Parser.ParseError
|
||||||
@ -113,6 +117,7 @@ instance NFData ModuleError where
|
|||||||
rnf e = case e of
|
rnf e = case e of
|
||||||
ModuleNotFound src path -> src `deepseq` path `deepseq` ()
|
ModuleNotFound src path -> src `deepseq` path `deepseq` ()
|
||||||
CantFindFile path -> path `deepseq` ()
|
CantFindFile path -> path `deepseq` ()
|
||||||
|
BadUtf8 path ue -> rnf (path, ue)
|
||||||
OtherIOError path exn -> path `deepseq` exn `seq` ()
|
OtherIOError path exn -> path `deepseq` exn `seq` ()
|
||||||
ModuleParseError source err -> source `deepseq` err `deepseq` ()
|
ModuleParseError source err -> source `deepseq` err `deepseq` ()
|
||||||
RecursiveModules mods -> mods `deepseq` ()
|
RecursiveModules mods -> mods `deepseq` ()
|
||||||
@ -146,6 +151,10 @@ instance PP ModuleError where
|
|||||||
text "[error]" <+>
|
text "[error]" <+>
|
||||||
text "can't find file:" <+> text path
|
text "can't find file:" <+> text path
|
||||||
|
|
||||||
|
BadUtf8 path _ue ->
|
||||||
|
text "[error]" <+>
|
||||||
|
text "bad utf-8 encoding:" <+> text path
|
||||||
|
|
||||||
OtherIOError path exn ->
|
OtherIOError path exn ->
|
||||||
hang (text "[error]" <+>
|
hang (text "[error]" <+>
|
||||||
text "IO error while loading file:" <+> text path <.> colon)
|
text "IO error while loading file:" <+> text path <.> colon)
|
||||||
@ -198,6 +207,9 @@ moduleNotFound name paths = ModuleT (raise (ModuleNotFound name paths))
|
|||||||
cantFindFile :: FilePath -> ModuleM a
|
cantFindFile :: FilePath -> ModuleM a
|
||||||
cantFindFile path = ModuleT (raise (CantFindFile path))
|
cantFindFile path = ModuleT (raise (CantFindFile path))
|
||||||
|
|
||||||
|
badUtf8 :: FilePath -> UnicodeException -> ModuleM a
|
||||||
|
badUtf8 path ue = ModuleT (raise (BadUtf8 path ue))
|
||||||
|
|
||||||
otherIOError :: FilePath -> IOException -> ModuleM a
|
otherIOError :: FilePath -> IOException -> ModuleM a
|
||||||
otherIOError path exn = ModuleT (raise (OtherIOError path exn))
|
otherIOError path exn = ModuleT (raise (OtherIOError path exn))
|
||||||
|
|
||||||
@ -444,10 +456,10 @@ unloadModule rm = ModuleT $ do
|
|||||||
env <- get
|
env <- get
|
||||||
set $! env { meLoadedModules = removeLoadedModule rm (meLoadedModules env) }
|
set $! env { meLoadedModules = removeLoadedModule rm (meLoadedModules env) }
|
||||||
|
|
||||||
loadedModule :: FilePath -> FilePath -> T.Module -> ModuleM ()
|
loadedModule :: FilePath -> FilePath -> Fingerprint -> T.Module -> ModuleM ()
|
||||||
loadedModule path canonicalPath m = ModuleT $ do
|
loadedModule path canonicalPath fp m = ModuleT $ do
|
||||||
env <- get
|
env <- get
|
||||||
set $! env { meLoadedModules = addLoadedModule path canonicalPath m (meLoadedModules env) }
|
set $! env { meLoadedModules = addLoadedModule path canonicalPath fp m (meLoadedModules env) }
|
||||||
|
|
||||||
modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM ()
|
modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM ()
|
||||||
modifyEvalEnv f = ModuleT $ do
|
modifyEvalEnv f = ModuleT $ do
|
||||||
|
Loading…
Reference in New Issue
Block a user