Foreign Function Interface

.github/workflows/ci.yml

@@ -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

cry

@@ -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)

cryptol-remote-api/src/CryptolServer/Exceptions.hs

@@ -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)
                 ])

cryptol.cabal

@@ -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
@@ -81,6 +85,11 @@ library
   else
     build-depends:     integer-gmp       >= 1.0 && < 1.1
 
+  if flag(ffi)
+    build-depends:     libffi            >= 0.2,
+                       unix
+    cpp-options:       -DFFI_ENABLED
+
   Build-tool-depends:  alex:alex, happy:happy
   hs-source-dirs:      src
 
@@ -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,
@@ -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,
@@ -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,

cryptol/CheckExercises.hs

@@ -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
@@ -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