Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Foreign Function Interface #1376

Merged
merged 65 commits into from
Aug 12, 2022
Merged
Show file tree
Hide file tree
Changes from 50 commits
Commits
Show all changes
65 commits
Select commit Hold shift + click to select a range
9bccc79
Add frontend for FFI
qsctr Jun 25, 2022
1e18568
Add basic FFI for concrete backend (unix only)
qsctr Jun 28, 2022
7fcfeeb
Refactor FFI code out of Backend class
qsctr Jun 29, 2022
9a4de13
Clean up FFI code
qsctr Jun 29, 2022
b5ab79a
Handle dlopen/dlsym errors
qsctr Jul 1, 2022
6a07099
Handle FFI loading errors in remote API
qsctr Jul 1, 2022
c5ebac4
Call dlclose in ForeignImpl finalizer
qsctr Jul 6, 2022
20403c2
Panic on recursive foreign decl group
qsctr Jul 6, 2022
56af466
Revert "Panic on recursive foreign decl group"
qsctr Jul 6, 2022
7bac9db
Add cabal flag for FFI
qsctr Jul 6, 2022
9551a15
Debug check-exercises failure
qsctr Jul 6, 2022
7f43cf0
Load .dylib for FFI on macOS
qsctr Jul 6, 2022
e4a7a0f
Bump CI CACHE_VERSION
qsctr Jul 6, 2022
3456a7d
Debugging libffi on ubuntu 18.04 CI
qsctr Jul 7, 2022
b8b53a1
Add FFI for all integral types
qsctr Jul 13, 2022
0cf81a3
Refactor FFI marshalling code
qsctr Jul 13, 2022
543862d
Revert "Debugging libffi on ubuntu 18.04 CI"
qsctr Jul 13, 2022
9d7bb04
Improve FFI marshalling of Bits
qsctr Jul 13, 2022
ecace94
Fix type errors in ghc 9.0+
qsctr Jul 13, 2022
cc3366a
FFI: Support multi argument functions
qsctr Jul 14, 2022
d161e95
FFI: Refactor loading/unloading shared libraries
qsctr Jul 15, 2022
fb5122d
FFI: Fix argument passing order
qsctr Jul 16, 2022
21cf642
FFI: Add support for floats
qsctr Jul 18, 2022
f8221c2
FFI: Support type synonyms
qsctr Jul 18, 2022
47f6370
FFI: Support passing and returning arrays
qsctr Jul 21, 2022
2fc195f
FFI: Rename FFIRep to FFIType
qsctr Jul 21, 2022
e1ede19
FFI: Support passing and returning tuples
qsctr Jul 24, 2022
c2ac894
FFI: Support passing and returning records
qsctr Jul 25, 2022
3534826
FFI: Simplify placeholder type in Infer
qsctr Jul 26, 2022
45dfcaa
FFI: Add size polymorphism and improve type errors
qsctr Jul 29, 2022
5d41a82
FFI: Remove duplicate type constraint errors
qsctr Jul 29, 2022
e4880c9
FFI: Refactor eval code and add comments
qsctr Aug 1, 2022
7294acc
FFI: Set up tests
qsctr Aug 3, 2022
8d28f59
FFI: Try linking against ghc's libffi at runtime
qsctr Aug 3, 2022
1b36a13
FFI: Fix linker flags
qsctr Aug 3, 2022
7f904e0
FFI: copy libffi to dist/lib/ and cryptol/../lib
qsctr Aug 3, 2022
3fb609d
FFI: add ghc libffi for other cryptol executables
qsctr Aug 4, 2022
6366447
FFI: Add ffi flag for cryptol-remote-api
qsctr Aug 4, 2022
ae843a0
FFI: Add integral and float tests
qsctr Aug 4, 2022
65cb428
FFI: Copy libffi to bin
qsctr Aug 4, 2022
9efd822
FFI: Canonicalize module path for finding dylib
qsctr Aug 5, 2022
59f0b30
FFI: Print whether FFI is enabled in -v/:v command
qsctr Aug 5, 2022
6b1210d
FFI: Revert dynamic linking hacks for linux
qsctr Aug 5, 2022
d7a9cfe
FFI: Revert changes to cryptol-remote-api.cabal
qsctr Aug 5, 2022
fb7c989
FFI: Add libffi package fork as submodule
qsctr Aug 5, 2022
5c2a409
Merge branch 'master' into ffi
qsctr Aug 5, 2022
8827a5b
FFI: Move CI ffi test check to test job
qsctr Aug 5, 2022
70fc5e2
FFI: Add more tests
qsctr Aug 5, 2022
d529c16
Don't allow wild cards in FFI declarations.
yav Aug 8, 2022
3509438
Fix test
yav Aug 8, 2022
6cc5cec
FFI: Add explicit reloading and refactor eval code
qsctr Aug 10, 2022
33fd5c2
FFI: Define ForeignSrc when FFI disabled
qsctr Aug 10, 2022
7ae7489
FFI: Add test for reloading with new changes
qsctr Aug 10, 2022
c6162c6
FFI: Use evalFinType in marshalTyArg
qsctr Aug 10, 2022
b301d66
FFI: Revert CI CACHE_VERSION bump
qsctr Aug 10, 2022
8e4f749
FFI: Formatting
qsctr Aug 10, 2022
0bc3bb7
FFI: Add docs
qsctr Aug 11, 2022
36fcdb3
FFI: Use upstream libffi
qsctr Aug 11, 2022
60a342a
FFI: Improve docs
qsctr Aug 11, 2022
46cb2f9
Fix rangeWithin comparison
qsctr Aug 11, 2022
65ba788
FFI: Add test for type errors
qsctr Aug 11, 2022
9652cf4
FFI: Call proveImplication on validSchema in Infer
qsctr Aug 12, 2022
8a274d0
FFI: Don't panic in reference evaluator
qsctr Aug 12, 2022
4fd7e17
FFI: Add test for runtime errors
qsctr Aug 12, 2022
d933fa6
FFI: Improve docs
qsctr Aug 12, 2022
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ env:
# older .so files are cached, which can have various effects
# (e.g. cabal complains it can't find a valid version of the "happy"
# tool).
CACHE_VERSION: 1
CACHE_VERSION: 2

jobs:
config:
Expand Down Expand Up @@ -299,7 +299,9 @@ jobs:
name: test-lib ${{ matrix.target }}
run: |
export PATH=$PWD/bin:$PWD/dist/bin:$PATH
./bin/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol ./tests/${{ matrix.target }}
if ${{ matrix.target != 'ffi' }} || dist/bin/cryptol -v | grep -q 'FFI enabled'; then
./bin/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol ./tests/${{ matrix.target }}
fi

- if: matrix.suite == 'rpc'
shell: bash
Expand Down
4 changes: 4 additions & 0 deletions .gitmodules
Original file line number Diff line number Diff line change
Expand Up @@ -4,3 +4,7 @@
[submodule "deps/argo"]
path = deps/argo
url = https://github.com/galoisinc/argo
[submodule "deps/libffi"]
path = deps/libffi
url = https://github.com/RyanGlScott/libffi
branch = static-linking-alt
1 change: 1 addition & 0 deletions cabal.project
Original file line number Diff line number Diff line change
Expand Up @@ -3,3 +3,4 @@ packages:
cryptol-remote-api
tests
deps/argo/argo
deps/libffi
14 changes: 12 additions & 2 deletions cry
Original file line number Diff line number Diff line change
Expand Up @@ -79,11 +79,21 @@ case $COMMAND in
test)
echo Running tests
setup_external_tools
if [ "$#" == "0" ]; then TESTS=tests; else TESTS=$*; fi
if [ "$#" == "0" ]; then
if cabal v2-exec cryptol -- -v | grep -q 'FFI enabled'; then
TESTS=(tests/*)
else
GLOBIGNORE="tests/ffi"
TESTS=(tests/*)
unset GLOBIGNORE
fi
else
TESTS=("$*")
fi
$BIN/test-runner --ext=.icry \
--exe=cabal \
-F v2-run -F -v0 -F exe:cryptol -F -- -F -b \
$TESTS
"${TESTS[@]}"
;;

rpc-test)
Expand Down
4 changes: 4 additions & 0 deletions cryptol-remote-api/src/CryptolServer/Exceptions.hs
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,10 @@ cryptolError modErr warns =
NotAParameterizedModule x ->
(20650, [ ("module", jsonPretty x)
])
FFILoadErrors x errs ->
(20660, [ ("module", jsonPretty x)
, ("errors", jsonList (map jsonPretty errs))
])
OtherFailure x ->
(29999, [ ("error", jsonString x)
])
Expand Down
15 changes: 15 additions & 0 deletions cryptol.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,10 @@ flag relocatable
default: True
description: Don't use the Cabal-provided data directory for looking up Cryptol libraries. This is useful when the data directory can't be known ahead of time, like for a relocatable distribution.

flag ffi
default: True
description: Enable the foreign function interface

library
Default-language:
Haskell2010
Expand Down Expand Up @@ -81,6 +85,11 @@ library
else
build-depends: integer-gmp >= 1.0 && < 1.1

if flag(ffi)
build-depends: libffi,
unix
cpp-options: -DFFI_ENABLED

Build-tool-depends: alex:alex, happy:happy
hs-source-dirs: src

Expand Down Expand Up @@ -147,6 +156,9 @@ library
Cryptol.TypeCheck.TypeMap,
Cryptol.TypeCheck.TypeOf,
Cryptol.TypeCheck.Sanity,
Cryptol.TypeCheck.FFI,
Cryptol.TypeCheck.FFI.Error,
Cryptol.TypeCheck.FFI.FFIType,

Cryptol.TypeCheck.Solver.Types,
Cryptol.TypeCheck.Solver.SMT,
Expand All @@ -169,6 +181,8 @@ library
Cryptol.Backend,
Cryptol.Backend.Arch,
Cryptol.Backend.Concrete,
Cryptol.Backend.FFI,
Cryptol.Backend.FFI.Error,
Cryptol.Backend.FloatHelpers,
Cryptol.Backend.Monad,
Cryptol.Backend.SeqMap,
Expand All @@ -179,6 +193,7 @@ library
Cryptol.Eval,
Cryptol.Eval.Concrete,
Cryptol.Eval.Env,
Cryptol.Eval.FFI,
Cryptol.Eval.Generic,
Cryptol.Eval.Prims,
Cryptol.Eval.Reference,
Expand Down
3 changes: 2 additions & 1 deletion cryptol/CheckExercises.hs
Original file line number Diff line number Diff line change
Expand Up @@ -291,7 +291,7 @@ main = do

if Seq.null (rdReplout rd)
then do let cryCmd = (P.shell (exe ++ " --interactive-batch " ++ inFile ++ " -e"))
(cryEC, cryOut, _) <- P.readCreateProcessWithExitCode cryCmd ""
(cryEC, cryOut, cryErr) <- P.readCreateProcessWithExitCode cryCmd ""


Line lnReplinStart _ Seq.:<| _ <- return $ rdReplin rd
Expand All @@ -301,6 +301,7 @@ main = do
putStrLn $ "REPL error (replin lines " ++
show lnReplinStart ++ "-" ++ show lnReplinEnd ++ ")."
putStr cryOut
putStr cryErr
exitFailure
ExitSuccess -> do
-- remove temporary input file
Expand Down
1 change: 1 addition & 0 deletions deps/libffi
Submodule libffi added at 3969b8
166 changes: 166 additions & 0 deletions src/Cryptol/Backend/FFI.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,166 @@
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- | The implementation of loading and calling external functions from shared
-- libraries. Currently works on Unix only.
module Cryptol.Backend.FFI
#ifdef FFI_ENABLED
( ForeignSrc
, loadForeignSrc
, ForeignImpl
, loadForeignImpl
, FFIArg
, FFIRet
, SomeFFIArg (..)
, callForeignImpl
)
#endif
where

#ifdef FFI_ENABLED

import Control.Exception
import Control.Monad
import Data.Bifunctor
import Data.Word
import Foreign hiding (newForeignPtr)
import Foreign.C.Types
import Foreign.Concurrent
import Foreign.LibFFI
import System.FilePath ((-<.>))
import System.IO.Error
import System.Posix.DynamicLinker

import Cryptol.Backend.FFI.Error

-- | A source from which we can retrieve implementations of foreign functions.
--
-- This is implemented as a 'ForeignPtr' wrapper around the pointer returned by
-- 'dlopen', where the destructor calls 'dlclose' when the library is no longer
-- needed. We keep references to the 'ForeignPtr' in each foreign function that
-- is in the evaluation environment, so when the Cryptol module is unloaded, the
-- shared library will be closed too.
newtype ForeignSrc = ForeignSrc (ForeignPtr ())

-- | Load a 'ForeignSrc' for the given __Cryptol__ file path. The file path of
-- the shared library that we try to load is the same as the Cryptol file path
-- except with a platform specific extension.
loadForeignSrc :: FilePath -> IO (Either FFILoadError ForeignSrc)
loadForeignSrc = loadForeignLib >=> traverse \ptr ->
ForeignSrc <$> newForeignPtr ptr (unloadForeignLib ptr)

loadForeignLib :: FilePath -> IO (Either FFILoadError (Ptr ()))
#ifdef darwin_HOST_OS
-- On Darwin, try loading .dylib first, and if that fails try .so
loadForeignLib path =
(Right <$> open "dylib") `catchIOError` \e1 ->
(Right <$> open "so") `catchIOError` \e2 ->
pure $ Left $ CantLoadFFISrc path $
displayException e1 ++ "\n" ++ displayException e2
#else
-- On other platforms, use .so
loadForeignLib path =
tryLoad (CantLoadFFISrc path) $ open "so"
#endif
where -- RTLD_NOW so we can make sure that the symbols actually exist at
-- module loading time
open ext = undl <$> dlopen (path -<.> ext) [RTLD_NOW]

unloadForeignLib :: Ptr () -> IO ()
unloadForeignLib = dlclose . DLHandle

-- | An implementation of a foreign function.
data ForeignImpl = ForeignImpl
{ foreignImplFun :: FunPtr ()
-- | We don't need this to call the function but we want to keep the library
-- around as long as we still have a function from it so that the destructor
-- isn't called too early.
, foreignImplLib :: ForeignPtr ()
}

-- | Load a 'ForeignImpl' with the given name from the given 'ForeignSrc'.
loadForeignImpl :: ForeignSrc -> String -> IO (Either FFILoadError ForeignImpl)
loadForeignImpl (ForeignSrc foreignImplLib) name =
withForeignPtr foreignImplLib \lib ->
tryLoad (CantLoadFFIImpl name) do
foreignImplFun <- loadForeignFunPtr lib name
pure ForeignImpl {..}

loadForeignFunPtr :: Ptr () -> String -> IO (FunPtr ())
loadForeignFunPtr = dlsym . DLHandle

tryLoad :: (String -> FFILoadError) -> IO a -> IO (Either FFILoadError a)
tryLoad err = fmap (first $ err . displayException) . tryIOError

-- | Types which can be converted into libffi arguments.
--
-- The Storable constraint is so that we can put them in arrays.
class Storable a => FFIArg a where
ffiArg :: a -> Arg

instance FFIArg Word8 where
ffiArg = argWord8

instance FFIArg Word16 where
ffiArg = argWord16

instance FFIArg Word32 where
ffiArg = argWord32

instance FFIArg Word64 where
ffiArg = argWord64

instance FFIArg CFloat where
ffiArg = argCFloat

instance FFIArg CDouble where
ffiArg = argCDouble

instance FFIArg (Ptr a) where
ffiArg = argPtr

instance FFIArg CSize where
ffiArg = argCSize

-- | Types which can be returned from libffi.
--
-- The Storable constraint is so that we can put them in arrays.
class Storable a => FFIRet a where
ffiRet :: RetType a

instance FFIRet Word8 where
ffiRet = retWord8

instance FFIRet Word16 where
ffiRet = retWord16

instance FFIRet Word32 where
ffiRet = retWord32

instance FFIRet Word64 where
ffiRet = retWord64

instance FFIRet CFloat where
ffiRet = retCFloat

instance FFIRet CDouble where
ffiRet = retCDouble

instance FFIRet () where
ffiRet = retVoid

-- | Existential wrapper around a 'FFIArg'.
data SomeFFIArg = forall a. FFIArg a => SomeFFIArg a

-- | Call a 'ForeignImpl' with the given arguments. The type parameter decides
-- how the return value should be converted into a Haskell value.
callForeignImpl :: forall a. FFIRet a => ForeignImpl -> [SomeFFIArg] -> IO a
callForeignImpl ForeignImpl {..} xs = withForeignPtr foreignImplLib \_ ->
callFFI foreignImplFun (ffiRet @a) $ map toArg xs
where toArg (SomeFFIArg x) = ffiArg x

#endif
30 changes: 30 additions & 0 deletions src/Cryptol/Backend/FFI/Error.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}

-- | Errors from dynamic loading of shared libraries for FFI.
module Cryptol.Backend.FFI.Error where

import Control.DeepSeq
import GHC.Generics

import Cryptol.Utils.PP

data FFILoadError
= CantLoadFFISrc
FilePath -- ^ Path to cryptol module
String -- ^ Error message
| CantLoadFFIImpl
String -- ^ Function name
String -- ^ Error message
deriving (Show, Generic, NFData)

instance PP FFILoadError where
ppPrec _ e = case e of
CantLoadFFISrc path msg ->
hang (text "Could not load foreign source for module located at"
<+> text path <.> colon)
4 (text msg)
CantLoadFFIImpl name msg ->
hang (text "Could not load foreign implementation for binding"
<+> text name <.> colon)
4 (text msg)
34 changes: 24 additions & 10 deletions src/Cryptol/Backend/Monad.hs
Original file line number Diff line number Diff line change
Expand Up @@ -54,7 +54,7 @@ import qualified Control.Exception as X
import Cryptol.Parser.Position
import Cryptol.Utils.Panic
import Cryptol.Utils.PP
import Cryptol.TypeCheck.AST(Name)
import Cryptol.TypeCheck.AST(Name, TParam)

-- | A computation that returns an already-evaluated value.
ready :: a -> Eval a
Expand Down Expand Up @@ -412,15 +412,18 @@ evalPanic cxt = panic ("[Eval] " ++ cxt)

-- | Data type describing errors that can occur during evaluation.
data EvalError
= InvalidIndex (Maybe Integer) -- ^ Out-of-bounds index
| DivideByZero -- ^ Division or modulus by 0
| NegativeExponent -- ^ Exponentiation by negative integer
| LogNegative -- ^ Logarithm of a negative integer
| UserError String -- ^ Call to the Cryptol @error@ primitive
| LoopError String -- ^ Detectable nontermination
| NoPrim Name -- ^ Primitive with no implementation
| BadRoundingMode Integer -- ^ Invalid rounding mode
| BadValue String -- ^ Value outside the domain of a partial function.
= InvalidIndex (Maybe Integer) -- ^ Out-of-bounds index
| DivideByZero -- ^ Division or modulus by 0
| NegativeExponent -- ^ Exponentiation by negative integer
| LogNegative -- ^ Logarithm of a negative integer
| UserError String -- ^ Call to the Cryptol @error@ primitive
| LoopError String -- ^ Detectable nontermination
| NoPrim Name -- ^ Primitive with no implementation
| BadRoundingMode Integer -- ^ Invalid rounding mode
| BadValue String -- ^ Value outside the domain of a partial function.
| FFINotSupported Name -- ^ Foreign function cannot be called
| FFITypeNumTooBig Name TParam Integer -- ^ Number passed to foreign function
-- as a type argument is too large
deriving Typeable

instance PP EvalError where
Expand All @@ -440,6 +443,17 @@ instance PP EvalError where
BadRoundingMode r -> "invalid rounding mode" <+> integer r
BadValue x -> "invalid input for" <+> backticks (text x)
NoPrim x -> text "unimplemented primitive:" <+> pp x
FFINotSupported x -> vcat
[ text "cannot call foreign function" <+> pp x
, text "FFI calls are not supported in this context"
, text "If you are trying to evaluate an expression, try rebuilding"
, text " Cryptol with FFI support enabled."
]
FFITypeNumTooBig f p n -> vcat
[ text "numeric type argument to foreign function is too large:"
<+> integer n
, text "in type parameter" <+> pp p <+> "of function" <+> pp f
, text "type arguments must fit in a C `size_t`" ]

instance Show EvalError where
show = show . pp
Expand Down
Loading