Disallow foreign with the same name and in functors

Fixes #1442

src/Cryptol/Backend/FFI/Error.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE DeriveGeneric  #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE Safe  #-}
 
 -- | Errors from dynamic loading of shared libraries for FFI.
@@ -9,6 +10,7 @@ import           Control.DeepSeq
 import           GHC.Generics
 
 import           Cryptol.Utils.PP
+import           Cryptol.ModuleSystem.Name
 
 data FFILoadError
   = CantLoadFFISrc
@@ -17,16 +19,26 @@ data FFILoadError
   | CantLoadFFIImpl
     String   -- ^ Function name
     String   -- ^ Error message
+  | FFIDuplicates [Name]
+  | FFIInFunctor  Name
   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"
+        hang ("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"
+        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))) <+>
+                 "defined at" <+> align (vcat (map (pp . nameLoc) xs)))
+      FFIInFunctor x ->
+        hang (pp (nameLoc x) <.> ":")
+          4 "Foreign declaration" <+> backticks (pp (nameIdent x)) <+>
+                "may not appear in a parameterized module."

src/Cryptol/Eval/FFI.hs

@@ -17,8 +17,6 @@ module Cryptol.Eval.FFI
   , evalForeignDecls
   ) where
 
-import           Data.Maybe
-
 import           Cryptol.Backend.FFI
 import           Cryptol.Backend.FFI.Error
 import           Cryptol.Eval
@@ -58,15 +56,6 @@ import           Cryptol.Utils.RecordMap
 
 #endif
 
--- | Find all the foreign declarations in the module and return their names and
--- FFIFunTypes.
-findForeignDecls :: Module -> [(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
-
 #ifdef FFI_ENABLED
 
 -- | Add the given foreign declarations to the environment, loading their

src/Cryptol/ModuleSystem/Base.hs

@@ -21,6 +21,8 @@ module Cryptol.ModuleSystem.Base where
 import qualified Control.Exception as X
 import Control.Monad (unless,forM)
 import Data.Maybe (fromMaybe)
+import Data.List(sortBy,groupBy)
+import Data.Function(on)
 import Data.Monoid ((<>))
 import Data.Text.Encoding (decodeUtf8')
 import System.Directory (doesFileExist, canonicalizePath)
@@ -44,7 +46,7 @@ import Cryptol.ModuleSystem.Env (DynamicEnv(..))
 import Cryptol.ModuleSystem.Fingerprint
 import Cryptol.ModuleSystem.Interface
 import Cryptol.ModuleSystem.Monad
-import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap,ModPath(..))
+import Cryptol.ModuleSystem.Name (Name,liftSupply,PrimMap,ModPath(..),nameIdent)
 import Cryptol.ModuleSystem.Env ( lookupModule
                                 , lookupTCEntity
                                 , LoadedModuleG(..), lmInterface
@@ -70,6 +72,7 @@ import qualified Cryptol.TypeCheck     as T
 import qualified Cryptol.TypeCheck.AST as T
 import qualified Cryptol.TypeCheck.PP as T
 import qualified Cryptol.TypeCheck.Sanity as TcSanity
+import qualified Cryptol.Backend.FFI.Error as FFI
 
 import Cryptol.Utils.Ident ( preludeName, floatName, arrayName, suiteBName, primeECName
                            , preludeReferenceName, interactiveName, modNameChunks
@@ -281,6 +284,8 @@ doLoadModule eval quiet isrc path fp pm0 =
 
   where
   evalForeign tcm
+    | not (null foreignFs) = ffiLoadErrors (T.mName tcm) (map FFI.FFIInFunctor foreignFs)
+    | not (null dups)      = ffiLoadErrors (T.mName tcm) (map FFI.FFIDuplicates dups)
     | null foreigns = pure Nothing
     | otherwise = case path of
       InFile p -> io (canonicalizePath p >>= loadForeignSrc) >>=
@@ -298,8 +303,11 @@ doLoadModule eval quiet isrc path fp pm0 =
           Left err -> ffiLoadErrors (T.mName tcm) [err]
       InMem m _ -> panic "doLoadModule"
         ["Can't find foreign source of in-memory module", m]
-    where foreigns = findForeignDecls tcm
-
+    where foreigns  = findForeignDecls tcm
+          foreignFs = T.findForeignDeclsInFunctors tcm
+          dups      = [ d | d@(_ : _ : _) <- groupBy ((==) `on` nameIdent)
+                                           $ sortBy (compare `on` nameIdent)
+                                           $ map fst foreigns ]
 
 
 -- | Rewrite an import declaration to be of the form:

src/Cryptol/TypeCheck/AST.hs

@@ -13,6 +13,7 @@
 {-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
 {-# LANGUAGE DeriveAnyClass, DeriveGeneric       #-}
 {-# LANGUAGE OverloadedStrings                   #-}
+{-# LANGUAGE NamedFieldPuns                      #-}
 module Cryptol.TypeCheck.AST
   ( module Cryptol.TypeCheck.AST
   , Name()
@@ -28,6 +29,8 @@ module Cryptol.TypeCheck.AST
   , module Cryptol.TypeCheck.Type
   ) where
 
+import Data.Maybe(mapMaybe)
+
 import Cryptol.Utils.Panic(panic)
 import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim)
 import Cryptol.Parser.Position(Located,Range,HasLoc(..))
@@ -132,6 +135,24 @@ emptyModule nm =
     , mSignatures       = mempty
     }
 
+-- | 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.
+-- This is used to report an error
+findForeignDeclsInFunctors :: ModuleG mname -> [Name]
+findForeignDeclsInFunctors = concatMap fromM . Map.elems . mFunctors
+  where
+  fromM m = map fst (findForeignDecls m) ++ findForeignDeclsInFunctors m
+
+
+
+
 type Module = ModuleG ModName
 
 -- | Is this a parameterized module?

tests/ffi/ffi-no-dup.cry

@@ -0,0 +1,7 @@
+
+
+foreign f : () -> [8]
+
+submodule A where
+  foreign f : () -> [16]
+

tests/ffi/ffi-no-dup.icry

@@ -0,0 +1 @@
+:load ffi-no-dup.cry

tests/ffi/ffi-no-dup.icry.stdout

@@ -0,0 +1,8 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+
+[error] Failed to load foreign implementations for module Main:
+    Multiple foreign declarations with the same name:
+        `f` defined at ffi-no-dup.cry:6:11--6:12
+                       ffi-no-dup.cry:3:9--3:10

tests/ffi/ffi-no-functor.cry

@@ -0,0 +1,7 @@
+
+submodule A where
+  parameter
+    type n : #
+
+  foreign f : (fin n) => [n][8] -> [8]
+

tests/ffi/ffi-no-functor.icry

@@ -0,0 +1 @@
+:load ffi-no-functor.cry

tests/ffi/ffi-no-functor.icry.stdout

@@ -0,0 +1,7 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+
+[error] Failed to load foreign implementations for module Main:
+    ffi-no-functor.cry:6:11--6:12:
+        Foreign declaration `f` may not appear in a parameterized module.

tests/ffi/test-ffi.c

@@ -147,3 +147,4 @@ void iQ2Qi(mpz_t in_0, mpq_t in_1, mpq_t out_0, mpz_t out_1) {
   mpq_set(out_0, in_1);
 }
 
+uint8_t nested() { return 72; }

tests/ffi/test-ffi.cry

@@ -50,4 +50,9 @@ foreign iQ2Qi : (Integer,Rational) -> (Rational,Integer)
 foreign i2Z5  : Integer -> Z 5
 foreign i2Z   : {n} (fin n, n >= 1) => Integer -> Z n
 
+// In a nested module
+submodule A where
+  foreign nested : () -> [8]
+
+
 

tests/ffi/test-ffi.h

@@ -1,6 +1,7 @@
 #include <gmp.h>
 #include <stddef.h>
 #include <stdint.h>
+uint8_t nested(void);
 uint8_t add8(uint8_t in0, uint8_t in1);
 uint16_t sub16(uint16_t in0, uint16_t in1);
 uint32_t mul32(uint32_t in0, uint32_t in1);

tests/ffi/test-ffi.icry

@@ -41,3 +41,5 @@ iQ2Qi (72,37)
 i2Z5 2
 i2Z5 10
 i2Z 123 : Z 10
+
+A::nested ()

tests/ffi/test-ffi.icry.stdout

@@ -42,3 +42,4 @@ True
 2
 0
 1
+0x48