GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity

FFI: Formatting

Browse Source
This commit is contained in:
Bretton 2022-08-10 15:11:14 -07:00
parent b301d66cbc
commit 8e4f749952
6 changed files with 133 additions and 110 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -118,9 +118,11 @@ unloadForeignLib :: Ptr () -> IO ()
unloadForeignLib = dlclose . DLHandle
withForeignSrc :: ForeignSrc -> (Ptr () -> IO a) -> IO a
withForeignSrc ForeignSrc {..} f = withMVar foreignSrcLoaded \case
True -> withForeignPtr foreignSrcFPtr f
False -> panic "[FFI] withForeignSrc" ["Use of foreign library after unload"]
withForeignSrc ForeignSrc {..} f = withMVar foreignSrcLoaded
\case
True -> withForeignPtr foreignSrcFPtr f
False ->
panic "[FFI] withForeignSrc" ["Use of foreign library after unload"]
-- | An implementation of a foreign function.
data ForeignImpl = ForeignImpl

19
src/Cryptol/Backend/FFI/Error.hs
View File

@ -19,12 +19,13 @@ data FFILoadError
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"
<+> text path <.> colon)
4 (text msg)
CantLoadFFIImpl name msg ->
hang (text "Could not load foreign implementation for binding"
<+> text name <.> colon)
4 (text msg)
ppPrec _ e =
case e of
CantLoadFFISrc path msg ->
hang (text "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"
<+> text name <.> colon)
4 (text msg)

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

@ -238,12 +238,13 @@ getMarshalBasicArg :: FFIBasicType ->
(forall a. FFIArg a => (GenValue Concrete -> Eval a) -> b) -> b
getMarshalBasicArg (FFIWord _ s) f = withWordType s \(_ :: p t) ->
f @t $ fmap (fromInteger . bvVal) . fromVWord Concrete "getMarshalBasicArg"
getMarshalBasicArg (FFIFloat _ _ s) f = case s of
-- LibBF can only convert to 'Double' directly, so we do that first then
-- convert to 'Float', which should not result in any loss of precision if
-- the original data was 32-bit anyways.
FFIFloat32 -> f $ pure . CFloat . double2Float . toDouble
FFIFloat64 -> f $ pure . CDouble . toDouble
getMarshalBasicArg (FFIFloat _ _ s) f =
case s of
-- LibBF can only convert to 'Double' directly, so we do that first then
-- convert to 'Float', which should not result in any loss of precision if
-- the original data was 32-bit anyways.
FFIFloat32 -> f $ pure . CFloat . double2Float . toDouble
FFIFloat64 -> f $ pure . CDouble . toDouble
where toDouble = fst . bfToDouble NearEven . bfValue . fromVFloat
-- | Given a 'FFIBasicType', call the callback with an unmarshalling function
@ -254,9 +255,10 @@ getMarshalBasicRet :: FFIBasicType ->
(forall a. FFIRet a => (a -> Eval (GenValue Concrete)) -> b) -> b
getMarshalBasicRet (FFIWord n s) f = withWordType s \(_ :: p t) ->
f @t $ word Concrete n . toInteger
getMarshalBasicRet (FFIFloat e p s) f = case s of
FFIFloat32 -> f $ toValue . \case CFloat x -> float2Double x
FFIFloat64 -> f $ toValue . \case CDouble x -> x
getMarshalBasicRet (FFIFloat e p s) f =
case s of
FFIFloat32 -> f $ toValue . \case CFloat x -> float2Double x
FFIFloat64 -> f $ toValue . \case CDouble x -> x
where toValue = pure . VFloat . BF e p . bfFromDouble
-- | Call the callback with the Word type corresponding to the given

111
src/Cryptol/TypeCheck/FFI.hs
View File

@ -27,65 +27,76 @@ toFFIFunType (Forall params _ t) =
(nubOrd $ map (fin . TVar . TVBound) params ++ props, fft)
Just (Left errs) -> Left $ FFITypeError t $ FFIBadComponentTypes errs
Nothing -> Left $ FFITypeError t FFINotFunction
where go (TCon (TC TCFun) [argType, retType]) = Just case toFFIType argType of
Right (ps, ffiArgType) -> case go retType of
Just (Right (ps', ffiFunType)) -> Right
( ps ++ ps'
, ffiFunType
{ ffiArgTypes = ffiArgType : ffiArgTypes ffiFunType } )
Just (Left errs) -> Left errs
Nothing -> case toFFIType retType of
Right (ps', ffiRetType) -> Right
( ps ++ ps'
, FFIFunType
{ ffiTParams = params, ffiArgTypes = [ffiArgType], .. } )
Left err -> Left [err]
Left err -> Left case go retType of
Just (Right _) -> [err]
Just (Left errs) -> err : errs
Nothing -> case toFFIType retType of
Right _ -> [err]
Left err' -> [err, err']
where go (TCon (TC TCFun) [argType, retType]) = Just
case toFFIType argType of
Right (ps, ffiArgType) ->
case go retType of
Just (Right (ps', ffiFunType)) -> Right
( ps ++ ps'
, ffiFunType
{ ffiArgTypes = ffiArgType : ffiArgTypes ffiFunType } )
Just (Left errs) -> Left errs
Nothing ->
case toFFIType retType of
Right (ps', ffiRetType) -> Right
( ps ++ ps'
, FFIFunType
{ ffiTParams = params
, ffiArgTypes = [ffiArgType], .. } )
Left err -> Left [err]
Left err -> Left
case go retType of
Just (Right _) -> [err]
Just (Left errs) -> err : errs
Nothing ->
case toFFIType retType of
Right _ -> [err]
Left err' -> [err, err']
go _ = Nothing
-- | Convert a 'Type' to a 'FFIType', along with any 'Prop's that must be
-- satisfied for the 'FFIType' to be valid.
toFFIType :: Type -> Either FFITypeError ([Prop], FFIType)
toFFIType t = case t of
TCon (TC TCBit) [] -> Right ([], FFIBool)
(toFFIBasicType -> Just r) -> (\fbt -> ([], FFIBasic fbt)) <$> r
TCon (TC TCSeq) [sz, bt] -> case toFFIBasicType bt of
Just (Right fbt) -> Right ([fin sz], FFIArray sz fbt)
Just (Left err) -> Left $ FFITypeError t $ FFIBadComponentTypes [err]
Nothing -> Left $ FFITypeError t FFIBadArrayType
TCon (TC (TCTuple _)) ts -> case partitionEithers $ map toFFIType ts of
([], unzip -> (pss, fts)) -> Right (concat pss, FFITuple fts)
(errs, _) -> Left $ FFITypeError t $ FFIBadComponentTypes errs
TRec tMap -> case sequence resMap of
Right resMap' -> Right $ FFIRecord <$>
recordMapAccum (\ps (ps', ft) -> (ps' ++ ps, ft)) [] resMap'
Left _ -> Left $ FFITypeError t $
FFIBadComponentTypes $ lefts $ displayElements resMap
where resMap = fmap toFFIType tMap
_ -> Left $ FFITypeError t FFIBadType
toFFIType t =
case t of
TCon (TC TCBit) [] -> Right ([], FFIBool)
(toFFIBasicType -> Just r) -> (\fbt -> ([], FFIBasic fbt)) <$> r
TCon (TC TCSeq) [sz, bt] ->
case toFFIBasicType bt of
Just (Right fbt) -> Right ([fin sz], FFIArray sz fbt)
Just (Left err) -> Left $ FFITypeError t $ FFIBadComponentTypes [err]
Nothing -> Left $ FFITypeError t FFIBadArrayType
TCon (TC (TCTuple _)) ts ->
case partitionEithers $ map toFFIType ts of
([], unzip -> (pss, fts)) -> Right (concat pss, FFITuple fts)
(errs, _) -> Left $ FFITypeError t $ FFIBadComponentTypes errs
TRec tMap ->
case sequence resMap of
Right resMap' -> Right $ FFIRecord <$>
recordMapAccum (\ps (ps', ft) -> (ps' ++ ps, ft)) [] resMap'
Left _ -> Left $ FFITypeError t $
FFIBadComponentTypes $ lefts $ displayElements resMap
where resMap = fmap toFFIType tMap
_ -> Left $ FFITypeError t FFIBadType
-- | Convert a 'Type' to a 'FFIBasicType', returning 'Nothing' if it isn't a
-- basic type and 'Left' if it is but there was some other issue with it.
toFFIBasicType :: Type -> Maybe (Either FFITypeError FFIBasicType)
toFFIBasicType t = case t of
TCon (TC TCSeq) [TCon (TC (TCNum n)) [], TCon (TC TCBit) []]
| n <= 8 -> word FFIWord8
| n <= 16 -> word FFIWord16
| n <= 32 -> word FFIWord32
| n <= 64 -> word FFIWord64
| otherwise -> Just $ Left $ FFITypeError t FFIBadWordSize
where word = Just . Right . FFIWord n
TCon (TC TCFloat) [TCon (TC (TCNum e)) [], TCon (TC (TCNum p)) []]
| e == 8, p == 24 -> float FFIFloat32
| e == 11, p == 53 -> float FFIFloat64
| otherwise -> Just $ Left $ FFITypeError t FFIBadFloatSize
where float = Just . Right . FFIFloat e p
_ -> Nothing
toFFIBasicType t =
case t of
TCon (TC TCSeq) [TCon (TC (TCNum n)) [], TCon (TC TCBit) []]
| n <= 8 -> word FFIWord8
| n <= 16 -> word FFIWord16
| n <= 32 -> word FFIWord32
| n <= 64 -> word FFIWord64
| otherwise -> Just $ Left $ FFITypeError t FFIBadWordSize
where word = Just . Right . FFIWord n
TCon (TC TCFloat) [TCon (TC (TCNum e)) [], TCon (TC (TCNum p)) []]
| e == 8, p == 24 -> float FFIFloat32
| e == 11, p == 53 -> float FFIFloat64
| otherwise -> Just $ Left $ FFITypeError t FFIBadFloatSize
where float = Just . Right . FFIFloat e p
_ -> Nothing
fin :: Type -> Prop
fin t = TCon (PC PFin) [t]

65
src/Cryptol/TypeCheck/FFI/Error.hs
View File

@ -29,25 +29,27 @@ instance TVars FFITypeError where
apSubst su (FFITypeError t r) = FFITypeError !$ apSubst su t !$ apSubst su r
instance TVars FFITypeErrorReason where
apSubst su r = case r of
FFIBadWordSize -> r
FFIBadFloatSize -> r
FFIBadArrayType -> r
FFIBadComponentTypes errs -> FFIBadComponentTypes !$ apSubst su errs
FFIBadType -> r
FFINotFunction -> r
apSubst su r =
case r of
FFIBadWordSize -> r
FFIBadFloatSize -> r
FFIBadArrayType -> r
FFIBadComponentTypes errs -> FFIBadComponentTypes !$ apSubst su errs
FFIBadType -> r
FFINotFunction -> r
instance FVS FFITypeError where
fvs (FFITypeError t r) = fvs (t, r)
instance FVS FFITypeErrorReason where
fvs r = case r of
FFIBadWordSize -> mempty
FFIBadFloatSize -> mempty
FFIBadArrayType -> mempty
FFIBadComponentTypes errs -> fvs errs
FFIBadType -> mempty
FFINotFunction -> mempty
fvs r =
case r of
FFIBadWordSize -> mempty
FFIBadFloatSize -> mempty
FFIBadArrayType -> mempty
FFIBadComponentTypes errs -> fvs errs
FFIBadType -> mempty
FFINotFunction -> mempty
instance PP (WithNames FFITypeError) where
ppPrec _ (WithNames (FFITypeError t r) names) =
@ -58,19 +60,22 @@ instance PP (WithNames FFITypeError) where
, ppWithNames names r ]
instance PP (WithNames FFITypeErrorReason) where
ppPrec _ (WithNames r names) = case r of
FFIBadWordSize -> vcat
[ "Unsupported word size"
, "Only words of up to 64 bits are supported" ]
FFIBadFloatSize -> vcat
[ "Unsupported Float format"
, "Only Float32 and Float64 are supported" ]
FFIBadArrayType -> vcat
[ "Unsupported sequence element type"
, "Only words or floats are supported as the element type of sequences" ]
FFIBadComponentTypes errs -> indent 2 $ vcat $ map (ppWithNames names) errs
FFIBadType -> vcat
[ "Only Bit, words, floats, sequences of words or floats,"
, "or structs or tuples of the above are supported as FFI"
, "argument or return types"]
FFINotFunction -> "FFI binding must be a function"
ppPrec _ (WithNames r names) =
case r of
FFIBadWordSize -> vcat
[ "Unsupported word size"
, "Only words of up to 64 bits are supported" ]
FFIBadFloatSize -> vcat
[ "Unsupported Float format"
, "Only Float32 and Float64 are supported" ]
FFIBadArrayType -> vcat
[ "Unsupported sequence element type"
, "Only words or floats are supported as the element type of sequences"
]
FFIBadComponentTypes errs ->
indent 2 $ vcat $ map (ppWithNames names) errs
FFIBadType -> vcat
[ "Only Bit, words, floats, sequences of words or floats,"
, "or structs or tuples of the above are supported as FFI"
, "argument or return types"]
FFINotFunction -> "FFI binding must be a function"

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

@ -998,15 +998,17 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
when (tpKind a /= KNum) $
recordErrorLoc loc $ UnsupportedFFIKind src a $ tpKind a
withTParams as do
ffiFunType <- case toFFIFunType (Forall as asmps0 t0) of
Right (props, ffiFunType) -> ffiFunType <$
(traverse (newGoal (CtFFI name)) props
>>= proveImplication True (Just name) as asmps0)
Left err -> do
recordErrorLoc loc $ UnsupportedFFIType src err
-- Just a placeholder type
pure FFIFunType
{ ffiTParams = as, ffiArgTypes = [], ffiRetType = FFITuple [] }
ffiFunType <-
case toFFIFunType (Forall as asmps0 t0) of
Right (props, ffiFunType) -> ffiFunType <$
(traverse (newGoal (CtFFI name)) props
>>= proveImplication True (Just name) as asmps0)
Left err -> do
recordErrorLoc loc $ UnsupportedFFIType src err
-- Just a placeholder type
pure FFIFunType
{ ffiTParams = as, ffiArgTypes = []
, ffiRetType = FFITuple [] }
pure Decl { dName = thing (P.bName b)
, dSignature = Forall as asmps0 t0
, dDefinition = DForeign ffiFunType