Merge pull request #1568 from GaloisInc/foreign-cryptol-def-fixes

Fixes for handling `foreign` functions

src/Cryptol/Eval.hs

@@ -368,7 +368,16 @@ evalDeclGroup ::
   SEval sym (GenEvalEnv sym)
 evalDeclGroup sym env dg = do
   case dg of
-    Recursive ds -> do
+    Recursive ds0 -> do
+      let ds = filter shouldEval ds0
+          -- If there are foreign declarations, we should only evaluate them if
+          -- they are not already bound in the environment by the previous
+          -- Cryptol.Eval.FFI.evalForeignDecls pass.
+          shouldEval d =
+            case (dDefinition d, lookupVar (dName d) env) of
+              (DForeign _ _, Just _) -> False
+              _                      -> True
+
       -- declare a "hole" for each declaration
       -- and extend the evaluation environment
       holes <- mapM (declHole sym) ds
@@ -432,14 +441,19 @@ 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"
-                            [show (ppLocName nm)]
-    DForeign _ _ -> evalPanic "Unexpected foreign declaration in recursive group"
-                            [show (ppLocName nm)]
-    DExpr _      -> do
-      (hole, fill) <- sDeclareHole sym msg
-      return (nm, sch, hole, fill)
+    DPrim -> evalPanic "Unexpected primitive declaration in recursive group"
+                       [show (ppLocName nm)]
+    DForeign _ me ->
+      case me of
+        Nothing -> evalPanic
+          "Unexpected foreign declaration with no cryptol implementation in recursive group"
+          [show (ppLocName nm)]
+        Just _ -> doHole
+    DExpr _ -> doHole
   where
+  doHole = do
+    (hole, fill) <- sDeclareHole sym msg
+    return (nm, sch, hole, fill)
   nm = dName d
   sch = dSignature d
   msg = unwords ["while evaluating", show (pp nm)]

src/Cryptol/TypeCheck/AST.hs

@@ -145,18 +145,23 @@ emptyModule nm =
 
 -- | Find all the foreign declarations in the module and return their names and FFIFunTypes.
 findForeignDecls :: ModuleG mname -> [(Name, FFIFunType)]
-findForeignDecls = mapMaybe getForeign . mDecls
-  where getForeign (NonRecursive Decl { dName, dDefinition = DForeign ffiType _ })
-          = Just (dName, ffiType)
-        -- Recursive DeclGroups can't have foreign decls
-        getForeign _ = Nothing
-
--- | Find all the foreign declarations that are in functors.
+findForeignDecls = mapMaybe getForeign . concatMap groupDecls . mDecls
+  where getForeign d =
+          case dDefinition d of
+            DForeign ffiType _ -> Just (dName d, ffiType)
+            _                  -> Nothing
+
+-- | Find all the foreign declarations that are in functors, including in the
+-- top-level module itself if it is a functor.
 -- This is used to report an error
 findForeignDeclsInFunctors :: ModuleG mname -> [Name]
-findForeignDeclsInFunctors = concatMap fromM . Map.elems . mFunctors
+findForeignDeclsInFunctors mo
+  | isParametrizedModule mo = fromM mo
+  | otherwise               = findInSubs mo
   where
-  fromM m = map fst (findForeignDecls m) ++ findForeignDeclsInFunctors m
+  findInSubs :: ModuleG mname -> [Name]
+  findInSubs = concatMap fromM . Map.elems . mFunctors
+  fromM m = map fst (findForeignDecls m) ++ findInSubs m
 
 
 

tests/ffi/ffi-fallback-rec.c

@@ -0,0 +1,5 @@
+#include <stdint.h>
+
+uint8_t f(uint8_t x) {
+    return x;
+}

tests/ffi/ffi-fallback-rec.cry

@@ -0,0 +1,5 @@
+foreign f : Bit -> Bit
+f x = ~ g x
+
+foreign g : Bit -> Bit
+g x = ~ f x

tests/ffi/ffi-fallback-rec.icry

@@ -0,0 +1,3 @@
+:! make -s ffi-fallback-rec
+:l ffi-fallback-rec.cry
+g True

tests/ffi/ffi-fallback-rec.icry.stdout

@@ -0,0 +1,8 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Loading dynamic library ffi-fallback-rec.so
+[warning] Could not load all foreign implementations for module Main:
+    Could not load foreign implementation for binding g
+    Fallback cryptol implementations will be used if available
+False

tests/ffi/ffi-fallback-rec.icry.stdout.darwin

@@ -0,0 +1,8 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Loading dynamic library ffi-fallback-rec.dylib
+[warning] Could not load all foreign implementations for module Main:
+    Could not load foreign implementation for binding g
+    Fallback cryptol implementations will be used if available
+False

tests/ffi/ffi-fallback-rec.icry.stdout.mingw32

@@ -0,0 +1,8 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+Loading dynamic library ffi-fallback-rec.dll
+[warning] Could not load all foreign implementations for module Main:
+    Could not load foreign implementation for binding g
+    Fallback cryptol implementations will be used if available
+False