Skip to content

Commit

Permalink
Merge pull request #1580 from GaloisInc/T1574
Browse files Browse the repository at this point in the history
Always show foreign dependencies in `file-deps`, and whether or not they exist on disk
  • Loading branch information
qsctr authored Oct 10, 2023
2 parents ed40d6f + d41b5f9 commit 8604e21
Show file tree
Hide file tree
Showing 6 changed files with 40 additions and 29 deletions.
3 changes: 2 additions & 1 deletion cryptol-remote-api/src/CryptolServer/FileDeps.hs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ module CryptolServer.FileDeps
) where

import Data.Text (Text)
import qualified Data.Map as Map
import qualified Data.Set as Set

import qualified Data.Aeson as JSON
Expand Down Expand Up @@ -68,7 +69,7 @@ instance ToJSON FileDeps where
, "fingerprint" .= fingerprintHexString (fiFingerprint fi)
, "includes" .= Set.toList (fiIncludeDeps fi)
, "imports" .= map (show . pp) (Set.toList (fiImportDeps fi))
, "foreign" .= Set.toList (fiForeignDeps fi)
, "foreign" .= Map.toList (fiForeignDeps fi)
]
where
fi = fdInfo fd
Expand Down
35 changes: 21 additions & 14 deletions src/Cryptol/Backend/FFI.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}

-- | The implementation of loading and calling external functions from shared
Expand Down Expand Up @@ -37,12 +38,13 @@ import Control.Concurrent.MVar
import Control.Exception
import Control.Monad
import Data.Bifunctor
import Data.Maybe
import Data.Word
import Foreign hiding (newForeignPtr)
import Foreign.C.Types
import Foreign.Concurrent
import Foreign.LibFFI
import System.Directory (doesFileExist, canonicalizePath)
import System.Directory (canonicalizePath, doesFileExist)
import System.FilePath ((-<.>))
import System.Info (os)
import System.IO.Error
Expand Down Expand Up @@ -98,19 +100,22 @@ loadForeignSrc = loadForeignLib >=> traverse \(foreignSrcPath, ptr) -> do
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)
-- | Given the path to a Cryptol module, compute the location of the shared
-- library we'd like to load. If FFI is supported, returns the location and
-- whether or not it actually exists on disk. Otherwise, returns Nothing.
foreignLibPath :: FilePath -> IO (Maybe (FilePath, Bool))
foreignLibPath path = do
path' <- canonicalizePath path
let search es =
case es of
[] -> pure Nothing
e : more -> do
let p = path' -<.> e
let libPaths = map (path' -<.>) exts
search ps =
case ps of
[] -> pure ((, False) <$> listToMaybe libPaths)
p : more -> do
yes <- doesFileExist p
if yes then pure (Just p) else search more
search
if yes then pure (Just (p, True)) else search more
search libPaths
where
exts =
case os of
"mingw32" -> ["dll"]
"darwin" -> ["dylib","so"]
Expand All @@ -120,8 +125,10 @@ loadForeignLib :: FilePath -> IO (Either FFILoadError (FilePath, Ptr ()))
loadForeignLib path =
do mb <- foreignLibPath path
case mb of
Nothing -> pure (Left (CantLoadFFISrc path "File not found"))
Just libPath -> tryLoad (CantLoadFFISrc path) (open libPath)
Just (libPath, True) ->
tryLoad (CantLoadFFISrc path) (open libPath)
_ ->
pure (Left (CantLoadFFISrc path "File not found"))

where open libPath = do
#if defined(mingw32_HOST_OS)
Expand Down Expand Up @@ -271,7 +278,7 @@ loadForeignSrc _ = pure $ Right ForeignSrc
unloadForeignSrc :: ForeignSrc -> IO ()
unloadForeignSrc _ = pure ()

foreignLibPath :: FilePath -> IO (Maybe FilePath)
foreignLibPath :: FilePath -> IO (Maybe (FilePath, Bool))
foreignLibPath _ = pure Nothing

#endif
10 changes: 5 additions & 5 deletions src/Cryptol/Eval.hs
Original file line number Diff line number Diff line change
Expand Up @@ -487,11 +487,11 @@ evalDecl sym renv env d = do
DForeign _ me -> do
-- Foreign declarations should have been handled by the previous
-- Cryptol.Eval.FFI.evalForeignDecls pass already, so they should already
-- be in the environment. If not, then either Cryptol was not compiled
-- with FFI support enabled, or we are in a non-Concrete backend. In that
-- case, we bind the name to the fallback cryptol implementation if
-- present, or otherwise to an error computation which will raise an error
-- if we try to evaluate it.
-- be in the environment. If not, then either the foreign source was
-- missing, Cryptol was not compiled with FFI support enabled, or we are
-- in a non-Concrete backend. In that case, we bind the name to the
-- fallback cryptol implementation if present, or otherwise to an error
-- computation which will raise an error if we try to evaluate it.
case lookupVar (dName d) env of
Just _ -> pure env
Nothing -> bindVar sym (dName d) val env
Expand Down
11 changes: 6 additions & 5 deletions src/Cryptol/ModuleSystem/Base.hs
Original file line number Diff line number Diff line change
Expand Up @@ -451,21 +451,22 @@ findDepsOf :: ModulePath -> ModuleM (ModulePath, FileInfo)
findDepsOf mpath =
do (fp, incs, ms) <- parseModule mpath
let (anyF,imps) = mconcat (map (findDeps' . addPrelude) ms)
fpath <- if getAny anyF
fdeps <- if getAny anyF
then do mb <- io case mpath of
InFile path -> foreignLibPath path
InMem {} -> pure Nothing
pure case mb of
Nothing -> Set.empty
Just f -> Set.singleton f
else pure Set.empty
Nothing -> Map.empty
Just (fpath, exists) ->
Map.singleton fpath exists
else pure Map.empty
pure
( mpath
, FileInfo
{ fiFingerprint = fp
, fiIncludeDeps = incs
, fiImportDeps = Set.fromList (map importedModule (appEndo imps []))
, fiForeignDeps = fpath
, fiForeignDeps = fdeps
}
)

Expand Down
7 changes: 4 additions & 3 deletions src/Cryptol/ModuleSystem/Env.hs
Original file line number Diff line number Diff line change
Expand Up @@ -564,7 +564,7 @@ data FileInfo = FileInfo
{ fiFingerprint :: Fingerprint
, fiIncludeDeps :: Set FilePath
, fiImportDeps :: Set ModName
, fiForeignDeps :: Set FilePath
, fiForeignDeps :: Map FilePath Bool
} deriving (Show,Generic,NFData)


Expand All @@ -579,9 +579,10 @@ fileInfo fp incDeps impDeps fsrc =
{ fiFingerprint = fp
, fiIncludeDeps = incDeps
, fiImportDeps = impDeps
, fiForeignDeps = fromMaybe Set.empty
, fiForeignDeps = fromMaybe Map.empty
do src <- fsrc
Set.singleton <$> getForeignSrcPath src
fpath <- getForeignSrcPath src
pure $ Map.singleton fpath True
}


Expand Down
3 changes: 2 additions & 1 deletion src/Cryptol/REPL/Command.hs
Original file line number Diff line number Diff line change
Expand Up @@ -121,6 +121,7 @@ import Data.Bits (shiftL, (.&.), (.|.))
import Data.Char (isSpace,isPunctuation,isSymbol,isAlphaNum,isAscii)
import Data.Function (on)
import Data.List (intercalate, nub, isPrefixOf)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe,mapMaybe,isNothing)
import System.Environment (lookupEnv)
import System.Exit (ExitCode(ExitSuccess))
Expand Down Expand Up @@ -1823,7 +1824,7 @@ moduleInfoCmd isFile name

depList show "includes" (Set.toList (M.fiIncludeDeps fi))
depList (show . show . pp) "imports" (Set.toList (M.fiImportDeps fi))
depList show "foreign" (Set.toList (M.fiForeignDeps fi))
depList show "foreign" (Map.toList (M.fiForeignDeps fi))

rPutStrLn "}"

Expand Down

0 comments on commit 8604e21

Please sign in to comment.