Merge pull request #1565 from GaloisInc/foreign-cryptol-def

Allow cryptol implementation of foreign functions

CHANGES.md

@@ -1,5 +1,13 @@
 # UNRELEASED
 
+## Language changes
+
+* `foreign` functions can now have an optional Cryptol implementation, which by
+  default is used when the foreign implementation cannot be found, or if the FFI
+  is unavailable. The `:set evalForeign` REPL option controls this behavior.
+
+## Bug fixes
+
 * Fixed #1556, #1237, and #1561.
 * Fixed #1455, making anything in scope of the functor in scope at the REPL as
   well when an instantiation of the functor is loaded and focused,

cryptol-remote-api/src/CryptolServer/Data/Expression.hs

@@ -518,7 +518,7 @@ getCryptolExpr (Let binds body) =
               , CP.bExport = CP.Public
               }) .
       fakeLoc .
-      CP.DExpr <$>
+      CP.exprDef <$>
         getCryptolExpr rhs
 
     fakeLoc = Located emptyRange

docs/RefMan/FFI.rst

@@ -353,6 +353,22 @@ make any guarantees about the order in which side effects will be executed, nor
 does it make any guarantees about preserving any global state between
 invocations of impure FFI functions.
 
+Cryptol implementation of foreign functions
+-------------------------------------------
+
+``foreign`` declarations can have an optional Cryptol implementation, which by
+default will be called when the foreign implementation cannot be found, or when
+the FFI cannot be used, such as during symbolic evaluation, evaluation with the
+reference interpreter, or if Cryptol was built with FFI support disabled.
+
+.. code-block:: cryptol
+
+  foreign add : [32] -> [32] -> [32]
+  add x y = x + y
+
+The ``:set evalForeign`` REPL option controls which implementation is used; see
+``:help :set evalForeign`` for more details.
+
 Example
 -------
 

src/Cryptol/Backend/FFI.hs

@@ -42,10 +42,10 @@ import           Foreign                    hiding (newForeignPtr)
 import           Foreign.C.Types
 import           Foreign.Concurrent
 import           Foreign.LibFFI
+import           System.Directory           (doesFileExist, canonicalizePath)
 import           System.FilePath            ((-<.>))
-import           System.Directory(doesFileExist)
+import           System.Info                (os)
 import           System.IO.Error
-import           System.Info(os)
 
 #if defined(mingw32_HOST_OS)
 import           System.Win32.DLL
@@ -101,23 +101,21 @@ loadForeignSrc = loadForeignLib >=> traverse \(foreignSrcPath, ptr) -> do
 -- | 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 =
+foreignLibPath path = do
+  path' <- canonicalizePath path
+  let 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
   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 path =
   do mb <- foreignLibPath path
@@ -273,4 +271,7 @@ loadForeignSrc _ = pure $ Right ForeignSrc
 unloadForeignSrc :: ForeignSrc -> IO ()
 unloadForeignSrc _ = pure ()
 
+foreignLibPath :: FilePath -> IO (Maybe FilePath)
+foreignLibPath _ = pure Nothing
+
 #endif

src/Cryptol/Backend/FFI/Error.hs

@@ -30,10 +30,12 @@ instance PP FFILoadError where
         hang ("Could not load foreign source for module located at"
               <+> text path <.> colon)
           4 (text msg)
-      CantLoadFFIImpl name msg ->
-        hang ("Could not load foreign implementation for binding"
-              <+> text name <.> colon)
-          4 (text msg)
+      CantLoadFFIImpl name _msg ->
+        "Could not load foreign implementation for binding" <+> text name
+        -- We don't print the OS error message for more consistent test output
+        -- hang ("Could not load foreign implementation for binding"
+        --       <+> text name <.> colon)
+        --   4 (text _msg)
       FFIDuplicates xs ->
         hang "Multiple foreign declarations with the same name:"
            4 (backticks (pp (nameIdent (head xs))) <+>

src/Cryptol/Backend/Monad.hs

@@ -447,9 +447,8 @@ instance PP EvalError where
     NoMatchingPropGuardCase msg -> text $ "No matching constraint guard; " ++ msg
     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."
+      , text "No foreign implementation is loaded,"
+      , text "  or FFI calls are not supported in this context."
       ]
     FFITypeNumTooBig f p n -> vcat
       [ text "numeric type argument to foreign function is too large:"

src/Cryptol/Eval.hs

@@ -432,11 +432,11 @@ declHole ::
   sym -> Decl -> SEval sym (Name, Schema, SEval sym (GenValue sym), SEval sym (GenValue sym) -> SEval sym ())
 declHole sym d =
   case dDefinition d of
-    DPrim      -> evalPanic "Unexpected primitive declaration in recursive group"
+    DPrim        -> evalPanic "Unexpected primitive declaration in recursive group"
                             [show (ppLocName nm)]
-    DForeign _ -> evalPanic "Unexpected foreign declaration in recursive group"
+    DForeign _ _ -> evalPanic "Unexpected foreign declaration in recursive group"
                             [show (ppLocName nm)]
-    DExpr _    -> do
+    DExpr _      -> do
       (hole, fill) <- sDeclareHole sym msg
       return (nm, sch, hole, fill)
   where
@@ -470,17 +470,22 @@ evalDecl sym renv env d = do
         Just (Left ex) -> bindVar sym (dName d) (evalExpr sym renv ex) env
         Nothing        -> bindVar sym (dName d) (cryNoPrimError sym (dName d)) env
 
-    DForeign _ -> 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 just bind the name to an error computation which will raise an
-      -- error if we try to evaluate it.
+      -- 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)
-          (raiseError sym $ FFINotSupported $ dName d) env
+        Nothing -> bindVar sym (dName d) val env
+          where
+          val =
+            case me of
+              Just e -> evalExpr sym renv e
+              Nothing -> raiseError sym $ FFINotSupported $ dName d
 
     DExpr e -> bindVar sym (dName d) (evalExpr sym renv e) env
 
@@ -755,6 +760,6 @@ evalMatch sym (lsz, lenv) m = seq lsz $ case m of
     where
       f env =
           case dDefinition d of
-            DPrim      -> evalPanic "evalMatch" ["Unexpected local primitive"]
-            DForeign _ -> evalPanic "evalMatch" ["Unexpected local foreign"]
-            DExpr e    -> evalExpr sym env e
+            DPrim        -> evalPanic "evalMatch" ["Unexpected local primitive"]
+            DForeign _ _ -> evalPanic "evalMatch" ["Unexpected local foreign"]
+            DExpr e      -> evalExpr sym env e

src/Cryptol/Eval/FFI.hs

@@ -59,18 +59,19 @@ import           Cryptol.Utils.RecordMap
 #ifdef FFI_ENABLED
 
 -- | Add the given foreign declarations to the environment, loading their
--- implementations from the given 'ForeignSrc'. This is a separate pass from the
--- main evaluation functions in "Cryptol.Eval" since it only works for the
--- Concrete backend.
+-- implementations from the given 'ForeignSrc'. If some implementations fail to
+-- load then errors are reported for them but any successfully loaded
+-- implementations are still added to the environment.
+--
+-- This is a separate pass from the main evaluation functions in "Cryptol.Eval"
+-- since it only works for the Concrete backend.
 evalForeignDecls :: ForeignSrc -> [(Name, FFIFunType)] -> EvalEnv ->
-  Eval (Either [FFILoadError] EvalEnv)
+  Eval ([FFILoadError], EvalEnv)
 evalForeignDecls fsrc decls env = io do
-  ePrims <- for decls \(name, ffiFunType) ->
+  (errs, prims) <- partitionEithers <$> for decls \(name, ffiFunType) ->
     fmap ((name,) . foreignPrimPoly name ffiFunType) <$>
       loadForeignImpl fsrc (unpackIdent $ nameIdent name)
-  pure case partitionEithers ePrims of
-    ([], prims) -> Right $ foldr (uncurry bindVarDirect) env prims
-    (errs, _)   -> Left errs
+  pure (errs, foldr (uncurry bindVarDirect) env prims)
 
 -- | Generate a 'Prim' value representing the given foreign function, containing
 -- all the code necessary to marshal arguments and return values and do the
@@ -422,9 +423,9 @@ getMarshalBasicRefArg FFIRational f = f \val g -> do
 #else
 
 -- | Dummy implementation for when FFI is disabled. Does not add anything to
--- the environment.
+-- the environment or report any errors.
 evalForeignDecls :: ForeignSrc -> [(Name, FFIFunType)] -> EvalEnv ->
-  Eval (Either [FFILoadError] EvalEnv)
-evalForeignDecls _ _ env = pure $ Right env
+  Eval ([FFILoadError], EvalEnv)
+evalForeignDecls _ _ env = pure ([], env)
 
 #endif

src/Cryptol/Eval/Reference.lhs

@@ -531,9 +531,14 @@ the new bindings.
 > evalDecl :: Env -> Decl -> (Name, E Value)
 > evalDecl env d =
 >   case dDefinition d of
->     DPrim      -> (dName d, pure (evalPrim (dName d)))
->     DForeign _ -> (dName d, cryError $ FFINotSupported $ dName d)
->     DExpr e    -> (dName d, evalExpr env e)
+>     DPrim         -> (dName d, pure (evalPrim (dName d)))
+>     DForeign _ me -> (dName d, val)
+>       where
+>         val =
+>           case me of
+>             Just e  -> evalExpr env e
+>             Nothing -> cryError $ FFINotSupported $ dName d
+>     DExpr e       -> (dName d, evalExpr env e)
 >
 
 Newtypes

src/Cryptol/IR/FreeVars.hs

@@ -93,7 +93,7 @@ instance FreeVars Decl where
 instance FreeVars DeclDef where
   freeVars d = case d of
                  DPrim -> mempty
-                 DForeign _ -> mempty
+                 DForeign _ me -> foldMap freeVars me
                  DExpr e -> freeVars e
 
 

src/Cryptol/IR/TraverseNames.hs

@@ -110,7 +110,7 @@ instance TraverseNames DeclDef where
   traverseNamesIP d =
     case d of
       DPrim   -> pure d
-      DForeign t -> DForeign <$> traverseNamesIP t
+      DForeign t me -> DForeign <$> traverseNamesIP t <*> traverseNamesIP me
       DExpr e -> DExpr <$> traverseNamesIP e
 
 instance TraverseNames Schema where

src/Cryptol/ModuleSystem/Base.hs

@@ -54,7 +54,8 @@ import Cryptol.ModuleSystem.Env ( DynamicEnv(..),FileInfo(..),fileInfo
                                 , LoadedModuleG(..), lmInterface
                                 , meCoreLint, CoreLint(..)
                                 , ModContext(..), ModContextParams(..)
-                                , ModulePath(..), modulePathLabel)
+                                , ModulePath(..), modulePathLabel
+                                , EvalForeignPolicy (..))
 import           Cryptol.Backend.FFI
 import qualified Cryptol.Eval                 as E
 import qualified Cryptol.Eval.Concrete as Concrete
@@ -79,7 +80,7 @@ import qualified Cryptol.Backend.FFI.Error as FFI
 import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName
                            , preludeReferenceName, interactiveName, modNameChunks
                            , modNameToNormalModName )
-import Cryptol.Utils.PP (pretty)
+import Cryptol.Utils.PP (pretty, pp, hang, vcat, ($$), (<+>), (<.>), colon)
 import Cryptol.Utils.Panic (panic)
 import Cryptol.Utils.Logger(logPutStrLn, logPrint)
 import Cryptol.Utils.Benchmark
@@ -306,32 +307,45 @@ doLoadModule eval quiet isrc path fp incDeps pm0 =
       ffiLoadErrors (T.mName tcm) (map FFI.FFIDuplicates dups)
     | null foreigns = pure Nothing
     | otherwise =
-      case path of
-        InFile p -> io (canonicalizePath p >>= loadForeignSrc) >>=
-          \case
-
-            Right fsrc -> do
-              unless quiet $
-                case getForeignSrcPath fsrc of
-                  Just fpath -> withLogger logPutStrLn $
-                    "Loading dynamic library " ++ takeFileName fpath
-                  Nothing -> pure ()
-              modifyEvalEnvM (evalForeignDecls fsrc foreigns) >>=
-                \case
-                  Right () -> pure $ Just fsrc
-                  Left errs -> ffiLoadErrors (T.mName tcm) errs
-
-            Left err -> ffiLoadErrors (T.mName tcm) [err]
-
-        InMem m _ -> panic "doLoadModule"
-          ["Can't find foreign source of in-memory module", m]
+      getEvalForeignPolicy >>= \case
+        AlwaysEvalForeign -> doEvalForeign (ffiLoadErrors (T.mName tcm))
+        PreferEvalForeign -> doEvalForeign \errs ->
+          withLogger logPrint $
+            hang
+              ("[warning] Could not load all foreign implementations for module"
+                <+> pp (T.mName tcm) <.> colon) 4 $
+              vcat (map pp errs)
+              $$ "Fallback cryptol implementations will be used if available"
+        NeverEvalForeign -> pure Nothing
 
     where foreigns  = findForeignDecls tcm
           foreignFs = T.findForeignDeclsInFunctors tcm
           dups      = [ d | d@(_ : _ : _) <- groupBy ((==) `on` nameIdent)
                                            $ sortBy (compare `on` nameIdent)
                                            $ map fst foreigns ]
+          doEvalForeign handleErrs =
+            case path of
+              InFile p -> io (loadForeignSrc p) >>=
+                \case
 
+                  Right fsrc -> do
+                    unless quiet $
+                      case getForeignSrcPath fsrc of
+                        Just fpath -> withLogger logPutStrLn $
+                          "Loading dynamic library " ++ takeFileName fpath
+                        Nothing -> pure ()
+                    (errs, ()) <-
+                      modifyEvalEnvM (evalForeignDecls fsrc foreigns)
+                    unless (null errs) $
+                      handleErrs errs
+                    pure $ Just fsrc
+
+                  Left err -> do
+                    handleErrs [err]
+                    pure Nothing
+
+              InMem m _ -> panic "doLoadModule"
+                ["Can't find foreign source of in-memory module", m]
 
 -- | Rewrite an import declaration to be of the form:
 --
@@ -434,16 +448,13 @@ findDepsOfModule m =
      findDepsOf mpath
 
 findDepsOf :: ModulePath -> ModuleM (ModulePath, FileInfo)
-findDepsOf mpath' =
-  do mpath <- case mpath' of
-                InFile file -> InFile <$> io (canonicalizePath file)
-                InMem {}    -> pure mpath'
-     (fp, incs, ms) <- parseModule mpath
+findDepsOf mpath =
+  do (fp, incs, ms) <- parseModule mpath
      let (anyF,imps) = mconcat (map (findDeps' . addPrelude) ms)
      fpath <- if getAny anyF
                 then do mb <- io case mpath of
-                                   InFile can -> foreignLibPath can
-                                   InMem {}   -> pure Nothing
+                                   InFile path -> foreignLibPath path
+                                   InMem {}    -> pure Nothing
                         pure case mb of
                                Nothing -> Set.empty
                                Just f  -> Set.singleton f