GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-11 08:37:35 +03:00
Code Issues Projects Releases Wiki Activity

Add FFI for all integral types

Browse Source
This commit is contained in:
Bretton 2022-07-13 14:40:59 -07:00
parent 3456a7d339
commit b8b53a1bf4
17 changed files with 169 additions and 92 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
cryptol.cabal
View File

@ -156,6 +156,7 @@ library
Cryptol.TypeCheck.TypeMap,
Cryptol.TypeCheck.TypeOf,
Cryptol.TypeCheck.Sanity,
Cryptol.TypeCheck.FFI,
Cryptol.TypeCheck.Solver.Types,
Cryptol.TypeCheck.Solver.SMT,

45
src/Cryptol/Backend/FFI.hs
View File

@ -4,21 +4,27 @@
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeSynonymInstances #-}
-- We need some instances that the unix package doesn't define
{-# OPTIONS_GHC -Wno-orphans #-}
#ifdef FFI_ENABLED
module Cryptol.Backend.FFI
#ifdef FFI_ENABLED
( ForeignSrc
, ForeignImpl
, loadForeignSrc
, loadForeignImpl
, FFIType
, callForeignImpl
) where
)
#endif
where
#ifdef FFI_ENABLED
import Control.DeepSeq
import Control.Exception
@ -51,8 +57,6 @@ type ForeignLib = DL
deriving instance Generic ForeignLib
deriving instance NFData ForeignLib
data ForeignImpl = forall a. ForeignImpl (ForeignPtr a)
loadForeignSrc :: FilePath -> IO (Either FFILoadError ForeignSrc)
loadForeignSrc = loadForeignLib >=> traverse \foreignLib -> do
foreignRefs <- newIORef 0
@ -75,6 +79,8 @@ loadForeignLib path =
unloadForeignLib :: ForeignLib -> IO ()
unloadForeignLib = dlclose
data ForeignImpl = forall a. ForeignImpl (ForeignPtr a)
loadForeignImpl :: ForeignSrc -> String -> IO (Either FFILoadError ForeignImpl)
loadForeignImpl ForeignSrc {..} name = tryLoad (CantLoadFFIImpl name) do
ptr <- castFunPtrToPtr <$> loadForeignFunPtr foreignLib name
@ -89,12 +95,29 @@ loadForeignFunPtr = dlsym
tryLoad :: (String -> FFILoadError) -> IO a -> IO (Either FFILoadError a)
tryLoad err = fmap (first $ err . displayException) . tryIOError
callForeignImpl :: ForeignImpl -> Word64 -> IO Word64
class FFIType a where
ffiArg :: a -> Arg
ffiRet :: RetType a
instance FFIType Word8 where
ffiArg = argWord8
ffiRet = retWord8
instance FFIType Word16 where
ffiArg = argWord16
ffiRet = retWord16
instance FFIType Word32 where
ffiArg = argWord32
ffiRet = retWord32
instance FFIType Word64 where
ffiArg = argWord64
ffiRet = retWord64
callForeignImpl :: forall a b.
(FFIType a, FFIType b) => ForeignImpl -> a -> IO b
callForeignImpl (ForeignImpl fp) x = withForeignPtr fp \p ->
callFFI (castPtrToFunPtr p) retWord64 [argWord64 x]
#else
module Cryptol.Backend.FFI where
callFFI (castPtrToFunPtr p) (ffiRet @b) [ffiArg x]
#endif

18
src/Cryptol/Eval.hs
View File

@ -382,11 +382,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"
[show (ppLocName nm)]
DForeign -> evalPanic "Unexpected foreign declaration in recursive group"
[show (ppLocName nm)]
DExpr _ -> do
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)
where
@ -418,7 +418,7 @@ evalDecl sym renv env d =
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 _ -> do
case lookupVar (dName d) env of
Just _ -> pure env
Nothing -> bindVar sym (dName d)
@ -697,6 +697,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

47
src/Cryptol/Eval/FFI.hs
View File

@ -2,6 +2,9 @@
{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE RecordWildCards #-}
module Cryptol.Eval.FFI
( evalForeignDecls
@ -18,15 +21,16 @@ import Control.Monad.Except
import Control.Monad.Writer.Strict
import Data.Foldable
import Data.IORef
import Data.Word
import Cryptol.Backend.Concrete
import Cryptol.Backend.FFI
import Cryptol.Backend.Monad
import Cryptol.Backend.WordValue
import Cryptol.Eval.Env
import Cryptol.Eval.Prims
import Cryptol.Eval.Value
import Cryptol.ModuleSystem.Name
import Cryptol.TypeCheck.FFI
import Cryptol.Utils.Ident
import Cryptol.Utils.Panic
@ -37,7 +41,7 @@ evalForeignDecls path m env = do
let evalForeignDeclGroup e (Recursive ds) = foldlM evalForeignDecl e ds
evalForeignDeclGroup e (NonRecursive d) = evalForeignDecl e d
evalForeignDecl e d = case dDefinition d of
DForeign -> do
DForeign rep -> do
fsrc <- liftIO (readIORef foreignSrc) >>= \case
Nothing -> case path of
InFile p -> do
@ -49,8 +53,9 @@ evalForeignDecls path m env = do
Just fsrc -> pure fsrc
liftIO (loadForeignImpl fsrc $ unpackIdent $ nameIdent $ dName d)
>>= \case
Left err -> tell [err] >> pure e
Right impl -> pure $ bindVarDirect (dName d) (foreignPrim impl) e
Left err -> tell [err] >> pure e
Right impl -> pure $
bindVarDirect (dName d) (foreignPrim rep impl) e
_ -> pure e
report (Left err) = Left [err]
report (Right (env', [])) = Right env'
@ -58,13 +63,33 @@ evalForeignDecls path m env = do
fmap report $ runExceptT $ runWriterT $
foldlM evalForeignDeclGroup env $ mDecls m
foreignPrim :: ForeignImpl -> Prim Concrete
foreignPrim impl = PStrict \case
VWord 64 wv -> PPrim $ fmap (VWord 64 . wordVal) $
asWordVal Concrete wv >>=
io . fmap (mkBv 64 . toInteger) .
callForeignImpl impl . fromInteger . bvVal
_ -> evalPanic "foreignPrim" ["Argument is not a 64-bit word"]
{- HLINT ignore foreignPrim "Avoid lambda" -}
foreignPrim :: FFIFunRep -> ForeignImpl -> Prim Concrete
foreignPrim FFIFunRep {..} impl = PStrict \val ->
PPrim $ withArg ffiArgRep val \arg ->
withRet ffiRetRep $ io $ callForeignImpl impl arg
withArg :: FFIRep -> GenValue Concrete ->
(forall a. FFIType a => a -> Eval b) -> Eval b
withArg FFIBool x f = f @Word8 $ fromIntegral $ fromEnum $ fromVBit x
withArg (FFIWord8 _) x f = withWordArg @Word8 x f
withArg (FFIWord16 _) x f = withWordArg @Word16 x f
withArg (FFIWord32 _) x f = withWordArg @Word32 x f
withArg (FFIWord64 _) x f = withWordArg @Word64 x f
withWordArg :: Integral a => GenValue Concrete -> (a -> Eval b) -> Eval b
withWordArg x f =
fromVWord Concrete "withWordArg" x >>= f . fromInteger . bvVal
withRet :: FFIRep -> (forall a. FFIType a => Eval a) -> Eval (GenValue Concrete)
withRet FFIBool x = VBit . toEnum . fromIntegral <$> x @Word8
withRet (FFIWord8 n) x = wordToValue @Word8 n x
withRet (FFIWord16 n) x = wordToValue @Word16 n x
withRet (FFIWord32 n) x = wordToValue @Word32 n x
withRet (FFIWord64 n) x = wordToValue @Word64 n x
wordToValue :: Integral a => Integer -> Eval a -> Eval (GenValue Concrete)
wordToValue n = (>>= word Concrete n . toInteger)
#else

6
src/Cryptol/Eval/Reference.lhs
View File

@ -510,9 +510,9 @@ the new bindings.
> evalDecl :: Env -> Decl -> (Name, E Value)
> evalDecl env d =
> case dDefinition d of
> DPrim -> (dName d, pure (evalPrim (dName d)))
> DForeign -> evalPanic "FFI unimplemented" []
> DExpr e -> (dName d, evalExpr env e)
> DPrim -> (dName d, pure (evalPrim (dName d)))
> DForeign _ -> evalPanic "FFI unsupported in reference interpreter" []
> DExpr e -> (dName d, evalExpr env e)
>
Newtypes

2
src/Cryptol/IR/FreeVars.hs
View File

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

6
src/Cryptol/ModuleSystem/InstantiateModule.hs
View File

@ -227,9 +227,9 @@ instance Inst DeclGroup where
instance Inst DeclDef where
inst env d =
case d of
DPrim -> DPrim
DForeign -> DForeign
DExpr e -> DExpr (inst env e)
DPrim -> DPrim
DForeign r -> DForeign r
DExpr e -> DExpr (inst env e)
instance Inst Decl where
inst env d = d { dSignature = inst env (dSignature d)

14
src/Cryptol/Transform/AddModParams.hs
View File

@ -146,12 +146,12 @@ instance AddParams DeclGroup where
instance AddParams Decl where
addParams ps d =
case dDefinition d of
DPrim -> d
DForeign -> d
DExpr e -> d { dSignature = addParams ps (dSignature d)
, dDefinition = DExpr (addParams ps e)
, dName = toParamInstName (dName d)
}
DPrim -> d
DForeign _ -> d
DExpr e -> d { dSignature = addParams ps (dSignature d)
, dDefinition = DExpr (addParams ps e)
, dName = toParamInstName (dName d)
}
instance AddParams TySyn where
addParams ps ts = ts { tsParams = pTypes ps ++ tsParams ts
@ -279,7 +279,7 @@ instance Inst DeclDef where
inst ps d =
case d of
DPrim -> DPrim
DForeign -> DForeign
DForeign r -> DForeign r
DExpr e -> DExpr (inst ps e)
instance Inst Type where

18
src/Cryptol/Transform/MonoValues.hs
View File

@ -216,9 +216,9 @@ rewD rews d = do e <- rewDef rews (dDefinition d)
return d { dDefinition = e }
rewDef :: RewMap -> DeclDef -> M DeclDef
rewDef rews (DExpr e) = DExpr <$> rewE rews e
rewDef _ DPrim = return DPrim
rewDef _ DForeign = return DForeign
rewDef rews (DExpr e) = DExpr <$> rewE rews e
rewDef _ DPrim = return DPrim
rewDef _ (DForeign r) = return $ DForeign r
rewDeclGroup :: RewMap -> DeclGroup -> M DeclGroup
rewDeclGroup rews dg =
@ -238,12 +238,12 @@ rewDeclGroup rews dg =
consider d =
case dDefinition d of
DPrim -> Left d
DForeign -> Left d
DExpr e -> let (tps,props,e') = splitTParams e
in if not (null tps) && notFun e'
then Right (d, tps, props, e')
else Left d
DPrim -> Left d
DForeign _ -> Left d
DExpr e -> let (tps,props,e') = splitTParams e
in if not (null tps) && notFun e'
then Right (d, tps, props, e')
else Left d
rewSame ds =
do new <- forM (NE.toList ds) $ \(d,_,_,e) ->

8
src/Cryptol/Transform/Specialize.hs
View File

@ -187,10 +187,10 @@ specializeConst e0 = do
sig' <- instantiateSchema ts n (dSignature decl)
modifySpecCache (Map.adjust (fmap (insertTM ts (qname', Nothing))) qname)
rhs' <- case dDefinition decl of
DExpr e -> do e' <- specializeExpr =<< instantiateExpr ts n e
return (DExpr e')
DPrim -> return DPrim
DForeign -> return DForeign
DExpr e -> do e' <- specializeExpr =<< instantiateExpr ts n e
return (DExpr e')
DPrim -> return DPrim
DForeign r -> return $ DForeign r
let decl' = decl { dName = qname', dSignature = sig', dDefinition = rhs' }
modifySpecCache (Map.adjust (fmap (insertTM ts (qname', Just decl'))) qname)
return (EVar qname')

9
src/Cryptol/TypeCheck/AST.hs
View File

@ -39,6 +39,7 @@ import Cryptol.Parser.AST ( Selector(..),Pragma(..)
, Fixity(..))
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim)
import Cryptol.Utils.RecordMap
import Cryptol.TypeCheck.FFI
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Type
@ -178,7 +179,7 @@ data Decl = Decl { dName :: !Name
} deriving (Generic, NFData, Show)
data DeclDef = DPrim
| DForeign
| DForeign FFIFunRep
| DExpr Expr
deriving (Show, Generic, NFData)
@ -369,9 +370,9 @@ instance PP (WithNames Decl) where
++ [ nest 2 (sep [pp dName <+> text "=", ppWithNames nm dDefinition]) ]
instance PP (WithNames DeclDef) where
ppPrec _ (WithNames DPrim _) = text "<primitive>"
ppPrec _ (WithNames DForeign _) = text "<foreign>"
ppPrec _ (WithNames (DExpr e) nm) = ppWithNames nm e
ppPrec _ (WithNames DPrim _) = text "<primitive>"
ppPrec _ (WithNames (DForeign _) _) = text "<foreign>"
ppPrec _ (WithNames (DExpr e) nm) = ppWithNames nm e
instance PP Decl where
ppPrec = ppWithNamesPrec IntMap.empty

14
src/Cryptol/TypeCheck/Error.hs
View File

@ -144,11 +144,7 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind
| MissingModVParam (Located Ident)
| UnsupportedFFIType TypeSource Type
-- ^ Type is not supported for passing to/returning from a
-- foreign function
| UnsupportedFFIPoly TypeSource
-- ^ Foreign functions cannot be polymorphic
-- ^ Type is not supported for FFI
| TemporaryError Doc
-- ^ This is for errors that don't fit other cateogories.
@ -206,8 +202,7 @@ errorImportance err =
AmbiguousSize {} -> 2
UnsupportedFFIPoly {} -> 10
UnsupportedFFIType {} -> 9
UnsupportedFFIType {} -> 10
instance TVars Warning where
@ -258,7 +253,6 @@ instance TVars Error where
MissingModVParam {} -> err
UnsupportedFFIType src t -> UnsupportedFFIType src !$ apSubst su t
UnsupportedFFIPoly {} -> err
TemporaryError {} -> err
@ -296,7 +290,6 @@ instance FVS Error where
MissingModVParam {} -> Set.empty
UnsupportedFFIType _ t -> fvs t
UnsupportedFFIPoly {} -> Set.empty
TemporaryError {} -> Set.empty
@ -476,9 +469,6 @@ instance PP (WithNames Error) where
vcat
[ ppWithNames names t
, "When checking" <+> pp src]
UnsupportedFFIPoly src ->
nested "Polymorphism is not supported for FFI" $
"When checking" <+> pp src
TemporaryError doc -> doc
where

39
src/Cryptol/TypeCheck/FFI.hs Normal file
View File

@ -0,0 +1,39 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE RecordWildCards #-}
module Cryptol.TypeCheck.FFI where
import Control.DeepSeq
import GHC.Generics
import Cryptol.TypeCheck.Type
data FFIRep
= FFIBool
| FFIWord8 Integer
| FFIWord16 Integer
| FFIWord32 Integer
| FFIWord64 Integer
deriving (Show, Generic, NFData)
data FFIFunRep = FFIFunRep
{ ffiArgRep :: FFIRep
, ffiRetRep :: FFIRep
} deriving (Show, Generic, NFData)
toFFIFunRep :: Schema -> Maybe FFIFunRep
toFFIFunRep (Forall [] [] (TCon (TC TCFun) [argType, retType])) = do
ffiArgRep <- toFFIRep argType
ffiRetRep <- toFFIRep retType
pure FFIFunRep {..}
toFFIFunRep _ = Nothing
toFFIRep :: Type -> Maybe FFIRep
toFFIRep (TCon (TC TCBit) []) = Just FFIBool
toFFIRep (TCon (TC TCSeq) [TCon (TC (TCNum n)) [], TCon (TC TCBit) []])
| n <= 8 = Just $ FFIWord8 n
| n <= 16 = Just $ FFIWord16 n
| n <= 32 = Just $ FFIWord32 n
| n <= 64 = Just $ FFIWord64 n
toFFIRep _ = Nothing

24
src/Cryptol/TypeCheck/Infer.hs
View File

@ -47,6 +47,7 @@ import Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
import Cryptol.TypeCheck.Instantiate
import Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)
import Cryptol.TypeCheck.Unify(rootPath)
import Cryptol.TypeCheck.FFI
import Cryptol.Utils.Ident
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.RecordMap
@ -927,9 +928,9 @@ generalize bs0 gs0 =
genE e = foldr ETAbs (foldr EProofAbs (apSubst su e) qs) asPs
genB d = d { dDefinition = case dDefinition d of
DExpr e -> DExpr (genE e)
DPrim -> DPrim
DForeign -> DForeign
DExpr e -> DExpr (genE e)
DPrim -> DPrim
DForeign r -> DForeign r
, dSignature = Forall asPs qs
$ apSubst su $ sType $ dSignature d
}
@ -982,22 +983,19 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
, dDoc = P.bDoc b
}
-- We only support very specific types for FFI for now
P.DForeign ->
let loc = getLoc b
src = DefinitionOf $ thing $ P.bName b
in inRangeMb loc do
unless (null as && null asmps0) $
recordErrorLoc loc $ UnsupportedFFIPoly src
case t0 of
TCon (TC TCFun)
[ TCon (TC TCSeq) [TCon (TC (TCNum 64)) [], TCon (TC TCBit) []]
, TCon (TC TCSeq) [TCon (TC (TCNum 64)) [], TCon (TC TCBit) []]
] -> pure ()
_ -> recordErrorLoc loc $ UnsupportedFFIType src t0
ffiFunRep <- case toFFIFunRep (Forall as asmps0 t0) of
Just ffiFunRep -> pure ffiFunRep
Nothing -> do
recordErrorLoc loc $ UnsupportedFFIType src t0
-- Just a placeholder
pure FFIFunRep { ffiArgRep = FFIBool, ffiRetRep = FFIBool }
return Decl { dName = thing (P.bName b)
, dSignature = Forall as asmps0 t0
, dDefinition = DForeign
, dDefinition = DForeign ffiFunRep
, dPragmas = P.bPragmas b
, dInfix = P.bInfix b
, dFixity = P.bFixity b

2
src/Cryptol/TypeCheck/Parseable.hs
View File

@ -93,7 +93,7 @@ instance ShowParseable Decl where
instance ShowParseable DeclDef where
showParseable DPrim = text (show DPrim)
showParseable DForeign = text (show DForeign)
showParseable (DForeign r) = text (show $ DForeign r)
showParseable (DExpr e) = parens (text "DExpr" $$ showParseable e)
instance ShowParseable DeclGroup where

2
src/Cryptol/TypeCheck/Sanity.hs
View File

@ -398,7 +398,7 @@ checkDecl checkSig d =
do when checkSig $ checkSchema $ dSignature d
return (dName d, dSignature d)
DForeign ->
DForeign _ ->
do when checkSig $ checkSchema $ dSignature d
return (dName d, dSignature d)

6
src/Cryptol/TypeCheck/Subst.hs
View File

@ -406,9 +406,9 @@ instance TVars Decl where
in d { dSignature = sig', dDefinition = def' }
instance TVars DeclDef where
apSubst su (DExpr e) = DExpr !$ (apSubst su e)
apSubst _ DPrim = DPrim
apSubst _ DForeign = DForeign
apSubst su (DExpr e) = DExpr !$ (apSubst su e)
apSubst _ DPrim = DPrim
apSubst _ (DForeign r) = DForeign r
instance TVars Module where
apSubst su m =