mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-12-29 10:53:31 +03:00
Add support for getting the dependencies of a module without loading it.
Hopefully this should be faster as we just parse the module and expand the includes. We do not rename, typecheck, or evaluate anything.
This commit is contained in:
parent
3a66cea2c7
commit
e54971e708
@ -15,6 +15,7 @@ module Cryptol.Backend.FFI
|
|||||||
, getForeignSrcPath
|
, getForeignSrcPath
|
||||||
, loadForeignSrc
|
, loadForeignSrc
|
||||||
, unloadForeignSrc
|
, unloadForeignSrc
|
||||||
|
, foreignLibPath
|
||||||
#ifdef FFI_ENABLED
|
#ifdef FFI_ENABLED
|
||||||
, ForeignImpl
|
, ForeignImpl
|
||||||
, loadForeignImpl
|
, loadForeignImpl
|
||||||
@ -42,7 +43,9 @@ import Foreign.C.Types
|
|||||||
import Foreign.Concurrent
|
import Foreign.Concurrent
|
||||||
import Foreign.LibFFI
|
import Foreign.LibFFI
|
||||||
import System.FilePath ((-<.>))
|
import System.FilePath ((-<.>))
|
||||||
|
import System.Directory(doesFileExist)
|
||||||
import System.IO.Error
|
import System.IO.Error
|
||||||
|
import System.Info(os)
|
||||||
|
|
||||||
#if defined(mingw32_HOST_OS)
|
#if defined(mingw32_HOST_OS)
|
||||||
import System.Win32.DLL
|
import System.Win32.DLL
|
||||||
@ -94,24 +97,35 @@ loadForeignSrc = loadForeignLib >=> traverse \(foreignSrcPath, ptr) -> do
|
|||||||
foreignSrcFPtr <- newForeignPtr ptr (unloadForeignSrc' foreignSrcLoaded ptr)
|
foreignSrcFPtr <- newForeignPtr ptr (unloadForeignSrc' foreignSrcLoaded ptr)
|
||||||
pure ForeignSrc {..}
|
pure ForeignSrc {..}
|
||||||
|
|
||||||
|
|
||||||
|
-- | Given the path to a Cryptol module, compute the location of
|
||||||
|
-- the shared library we'd like to load.
|
||||||
|
foreignLibPath :: FilePath -> IO (Maybe FilePath)
|
||||||
|
foreignLibPath path =
|
||||||
|
search
|
||||||
|
case os of
|
||||||
|
"mingw32" -> ["dll"]
|
||||||
|
"darwin" -> ["dylib","so"]
|
||||||
|
_ -> ["so"]
|
||||||
|
|
||||||
|
where
|
||||||
|
search es =
|
||||||
|
case es of
|
||||||
|
[] -> pure Nothing
|
||||||
|
e : more ->
|
||||||
|
do let p = path -<.> e
|
||||||
|
yes <- doesFileExist p
|
||||||
|
if yes then pure (Just p) else search more
|
||||||
|
|
||||||
|
|
||||||
loadForeignLib :: FilePath -> IO (Either FFILoadError (FilePath, Ptr ()))
|
loadForeignLib :: FilePath -> IO (Either FFILoadError (FilePath, Ptr ()))
|
||||||
#if defined(mingw32_HOST_OS)
|
|
||||||
loadForeignLib path =
|
loadForeignLib path =
|
||||||
tryLoad (CantLoadFFISrc path) $ open "dll"
|
do mb <- foreignLibPath path
|
||||||
#elif defined(darwin_HOST_OS)
|
case mb of
|
||||||
-- On Darwin, try loading .dylib first, and if that fails try .so
|
Nothing -> pure (Left (CantLoadFFISrc path "File not found"))
|
||||||
loadForeignLib path =
|
Just libPath -> tryLoad (CantLoadFFISrc path) (open libPath)
|
||||||
(Right <$> open "dylib") `catchIOError` \e1 ->
|
|
||||||
(Right <$> open "so") `catchIOError` \e2 ->
|
where open libPath = do
|
||||||
pure $ Left $ CantLoadFFISrc path $
|
|
||||||
displayException e1 ++ "\n" ++ displayException e2
|
|
||||||
#else
|
|
||||||
-- On other platforms, use .so
|
|
||||||
loadForeignLib path =
|
|
||||||
tryLoad (CantLoadFFISrc path) $ open "so"
|
|
||||||
#endif
|
|
||||||
where open ext = do
|
|
||||||
let libPath = path -<.> ext
|
|
||||||
#if defined(mingw32_HOST_OS)
|
#if defined(mingw32_HOST_OS)
|
||||||
ptr <- loadLibrary libPath
|
ptr <- loadLibrary libPath
|
||||||
#else
|
#else
|
||||||
|
@ -7,6 +7,7 @@
|
|||||||
-- Portability : portable
|
-- Portability : portable
|
||||||
|
|
||||||
{-# LANGUAGE FlexibleContexts #-}
|
{-# LANGUAGE FlexibleContexts #-}
|
||||||
|
{-# LANGUAGE BlockArguments #-}
|
||||||
|
|
||||||
module Cryptol.ModuleSystem (
|
module Cryptol.ModuleSystem (
|
||||||
-- * Module System
|
-- * Module System
|
||||||
@ -32,6 +33,11 @@ module Cryptol.ModuleSystem (
|
|||||||
|
|
||||||
-- * Interfaces
|
-- * Interfaces
|
||||||
, Iface, IfaceG(..), IfaceDecls(..), T.genIface, IfaceDecl(..)
|
, Iface, IfaceG(..), IfaceDecls(..), T.genIface, IfaceDecl(..)
|
||||||
|
|
||||||
|
-- * Dependencies
|
||||||
|
, M.ModName
|
||||||
|
, getFileDependencies
|
||||||
|
, getModuleDependencies
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import Data.Map (Map)
|
import Data.Map (Map)
|
||||||
@ -137,3 +143,18 @@ renameVar names n env = runModuleM env $ interactive $
|
|||||||
renameType :: R.NamingEnv -> PName -> ModuleCmd Name
|
renameType :: R.NamingEnv -> PName -> ModuleCmd Name
|
||||||
renameType names n env = runModuleM env $ interactive $
|
renameType names n env = runModuleM env $ interactive $
|
||||||
Base.rename M.interactiveName names (R.renameType R.NameUse n)
|
Base.rename M.interactiveName names (R.renameType R.NameUse n)
|
||||||
|
|
||||||
|
--------------------------------------------------------------------------------
|
||||||
|
-- Dependencies
|
||||||
|
|
||||||
|
|
||||||
|
-- | Get information about the dependencies of a module.
|
||||||
|
getFileDependencies :: FilePath -> ModuleCmd (FilePath, FileInfo)
|
||||||
|
getFileDependencies path env = runModuleM env (Base.findDepsOfFile path)
|
||||||
|
|
||||||
|
-- | Get information about the dependencies of a module.
|
||||||
|
-- May return 'Nothing' if this is an `InMem` module
|
||||||
|
getModuleDependencies :: M.ModName -> ModuleCmd (Maybe (FilePath, FileInfo))
|
||||||
|
getModuleDependencies m env = runModuleM env (Base.findDepsOfModule m)
|
||||||
|
|
||||||
|
|
||||||
|
@ -25,7 +25,7 @@ import qualified Data.Set as Set
|
|||||||
import Data.Maybe (fromMaybe)
|
import Data.Maybe (fromMaybe)
|
||||||
import Data.List(sortBy,groupBy)
|
import Data.List(sortBy,groupBy)
|
||||||
import Data.Function(on)
|
import Data.Function(on)
|
||||||
import Data.Monoid ((<>))
|
import Data.Monoid ((<>),Endo(..), Any(..))
|
||||||
import Data.Text.Encoding (decodeUtf8')
|
import Data.Text.Encoding (decodeUtf8')
|
||||||
import System.Directory (doesFileExist, canonicalizePath)
|
import System.Directory (doesFileExist, canonicalizePath)
|
||||||
import System.FilePath ( addExtension
|
import System.FilePath ( addExtension
|
||||||
@ -44,7 +44,7 @@ import Prelude.Compat hiding ( (<>) )
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
import Cryptol.ModuleSystem.Env (DynamicEnv(..),fileInfo)
|
import Cryptol.ModuleSystem.Env (DynamicEnv(..),FileInfo(..),fileInfo)
|
||||||
import Cryptol.ModuleSystem.Fingerprint
|
import Cryptol.ModuleSystem.Fingerprint
|
||||||
import Cryptol.ModuleSystem.Interface
|
import Cryptol.ModuleSystem.Interface
|
||||||
import Cryptol.ModuleSystem.Monad
|
import Cryptol.ModuleSystem.Monad
|
||||||
@ -199,7 +199,8 @@ parseModule path = do
|
|||||||
Left err -> moduleParseError path err
|
Left err -> moduleParseError path err
|
||||||
|
|
||||||
|
|
||||||
-- Top Level Modules and Signatures ----------------------------------------------
|
-- Top Level Modules and Signatures --------------------------------------------
|
||||||
|
|
||||||
|
|
||||||
-- | Load a module by its path.
|
-- | Load a module by its path.
|
||||||
loadModuleByPath ::
|
loadModuleByPath ::
|
||||||
@ -414,25 +415,68 @@ addPrelude m
|
|||||||
-- | Load the dependencies of a module into the environment.
|
-- | Load the dependencies of a module into the environment.
|
||||||
loadDeps :: P.ModuleG mname name -> ModuleM (Set ModName)
|
loadDeps :: P.ModuleG mname name -> ModuleM (Set ModName)
|
||||||
loadDeps m =
|
loadDeps m =
|
||||||
|
do let ds = findDeps m
|
||||||
|
mapM_ (loadModuleFrom False) ds
|
||||||
|
pure (Set.fromList (map importedModule ds))
|
||||||
|
|
||||||
|
-- | Find all imports in a module.
|
||||||
|
findDeps :: P.ModuleG mname name -> [ImportSource]
|
||||||
|
findDeps m = appEndo (snd (findDeps' m)) []
|
||||||
|
|
||||||
|
findDepsOfFile :: FilePath -> ModuleM (FilePath, FileInfo)
|
||||||
|
findDepsOfFile file =
|
||||||
|
do can <- io (canonicalizePath file)
|
||||||
|
(fp, incs, ms) <- parseModule (InFile can)
|
||||||
|
let (anyF,imps) = mconcat (map findDeps' ms)
|
||||||
|
fpath <- if getAny anyF
|
||||||
|
then do mb <- io (foreignLibPath can)
|
||||||
|
pure case mb of
|
||||||
|
Nothing -> Set.empty
|
||||||
|
Just f -> Set.singleton f
|
||||||
|
else pure Set.empty
|
||||||
|
pure
|
||||||
|
( can
|
||||||
|
, FileInfo
|
||||||
|
{ fiFingerprint = fp
|
||||||
|
, fiIncludeDeps = incs
|
||||||
|
, fiImportDeps = Set.fromList (map importedModule (appEndo imps []))
|
||||||
|
, fiForeignDeps = fpath
|
||||||
|
}
|
||||||
|
)
|
||||||
|
|
||||||
|
findDepsOfModule :: ModName -> ModuleM (Maybe (FilePath,FileInfo))
|
||||||
|
findDepsOfModule mo = findDepsOfModPath =<< findModule mo
|
||||||
|
|
||||||
|
findDepsOfModPath :: ModulePath -> ModuleM (Maybe (FilePath,FileInfo))
|
||||||
|
findDepsOfModPath mo =
|
||||||
|
case mo of
|
||||||
|
InFile f -> Just <$> findDepsOfFile f
|
||||||
|
InMem {} -> pure Nothing
|
||||||
|
|
||||||
|
-- | Find the set of top-level modules imported by a module.
|
||||||
|
findModuleDeps :: P.ModuleG mname name -> Set P.ModName
|
||||||
|
findModuleDeps = Set.fromList . map importedModule . findDeps
|
||||||
|
|
||||||
|
-- | A helper `findDeps` and `findModuleDeps` that actually does the searching.
|
||||||
|
findDeps' :: P.ModuleG mname name -> (Any, Endo [ImportSource])
|
||||||
|
findDeps' m =
|
||||||
case mDef m of
|
case mDef m of
|
||||||
NormalModule ds -> Set.unions <$> mapM depsOfDecl ds
|
NormalModule ds -> mconcat (map depsOfDecl ds)
|
||||||
FunctorInstance f as _ ->
|
FunctorInstance f as _ ->
|
||||||
do fds <- loadImpName FromModuleInstance f
|
let fds = loadImpName FromModuleInstance f
|
||||||
ads <- case as of
|
ads = case as of
|
||||||
DefaultInstArg a -> loadInstArg a
|
DefaultInstArg a -> loadInstArg a
|
||||||
DefaultInstAnonArg ds -> Set.unions <$> mapM depsOfDecl ds
|
DefaultInstAnonArg ds -> mconcat (map depsOfDecl ds)
|
||||||
NamedInstArgs args ->
|
NamedInstArgs args -> mconcat (map loadNamedInstArg args)
|
||||||
Set.unions <$> mapM loadNamedInstArg args
|
in fds <> ads
|
||||||
pure (Set.union fds ads)
|
InterfaceModule s -> mconcat (map loadImpD (sigImports s))
|
||||||
InterfaceModule s -> Set.unions <$> mapM loadImpD (sigImports s)
|
|
||||||
where
|
where
|
||||||
loadI i = do _ <- loadModuleFrom False i
|
loadI i = (mempty, Endo (i:))
|
||||||
pure (Set.singleton (importedModule i))
|
|
||||||
|
|
||||||
loadImpName src l =
|
loadImpName src l =
|
||||||
case thing l of
|
case thing l of
|
||||||
ImpTop f -> loadI (src l { thing = f })
|
ImpTop f -> loadI (src l { thing = f })
|
||||||
_ -> pure Set.empty
|
_ -> mempty
|
||||||
|
|
||||||
loadImpD li = loadImpName (FromImport . new) (iModule <$> li)
|
loadImpD li = loadImpName (FromImport . new) (iModule <$> li)
|
||||||
where new i = i { thing = (thing li) { iModule = thing i } }
|
where new i = i { thing = (thing li) { iModule = thing i } }
|
||||||
@ -441,18 +485,30 @@ loadDeps m =
|
|||||||
loadInstArg f =
|
loadInstArg f =
|
||||||
case thing f of
|
case thing f of
|
||||||
ModuleArg mo -> loadImpName FromModuleInstance f { thing = mo }
|
ModuleArg mo -> loadImpName FromModuleInstance f { thing = mo }
|
||||||
_ -> pure Set.empty
|
_ -> mempty
|
||||||
|
|
||||||
depsOfDecl d =
|
depsOfDecl d =
|
||||||
case d of
|
case d of
|
||||||
DImport li -> loadImpD li
|
DImport li -> loadImpD li
|
||||||
|
|
||||||
DModule TopLevel { tlValue = NestedModule nm } -> loadDeps nm
|
DModule TopLevel { tlValue = NestedModule nm } -> findDeps' nm
|
||||||
|
|
||||||
DModParam mo -> loadImpName FromSigImport s
|
DModParam mo -> loadImpName FromSigImport s
|
||||||
where s = mpSignature mo
|
where s = mpSignature mo
|
||||||
|
|
||||||
_ -> pure Set.empty
|
Decl dd -> depsOfDecl' (tlValue dd)
|
||||||
|
|
||||||
|
_ -> mempty
|
||||||
|
|
||||||
|
depsOfDecl' d =
|
||||||
|
case d of
|
||||||
|
DLocated d' _ -> depsOfDecl' d'
|
||||||
|
DBind b ->
|
||||||
|
case thing (bDef b) of
|
||||||
|
DForeign {} -> (Any True, mempty)
|
||||||
|
_ -> mempty
|
||||||
|
_ -> mempty
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user