{-# LANGUAGE BangPatterns        #-}
{-# LANGUAGE BlockArguments      #-}
{-# LANGUAGE CPP                 #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE PatternSynonyms     #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE RecordWildCards     #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections       #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE ViewPatterns        #-}

-- | Evaluation of foreign functions.
module Cryptol.Eval.FFI
  ( findForeignDecls
  , evalForeignDecls
  ) where

import           Cryptol.Backend.FFI
import           Cryptol.Backend.FFI.Error
import           Cryptol.Eval
import           Cryptol.TypeCheck.AST
import           Cryptol.TypeCheck.FFI.FFIType

#ifdef FFI_ENABLED

import           Control.Exception(bracket_)
import           Data.Either
import           Data.Foldable
import           Data.IORef
import           Data.Proxy
import           Data.Ratio
import           Data.Traversable
import           Data.Word
import           Foreign
import           Foreign.C.Types
import           GHC.Float
import           LibBF                         (bfFromDouble, bfToDouble,
                                                pattern NearEven)
import           Numeric.GMP.Raw.Unsafe
import           Numeric.GMP.Utils

import           Cryptol.Backend
import           Cryptol.Backend.Concrete
import           Cryptol.Backend.FloatHelpers
import           Cryptol.Backend.Monad
import           Cryptol.Backend.SeqMap
import           Cryptol.Eval.Env
import           Cryptol.Eval.Prims
import           Cryptol.Eval.Type
import           Cryptol.Eval.Value
import           Cryptol.ModuleSystem.Name
import           Cryptol.TypeCheck.Solver.InfNat
import           Cryptol.Utils.Ident
import           Cryptol.Utils.RecordMap

#endif

#ifdef FFI_ENABLED

-- | Add the given foreign declarations to the environment, loading their
-- 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 ([FFILoadError], EvalEnv)
evalForeignDecls :: ForeignSrc
-> [(Name, FFIFunType)]
-> EvalEnv
-> Eval ([FFILoadError], EvalEnv)
evalForeignDecls ForeignSrc
fsrc [(Name, FFIFunType)]
decls EvalEnv
env = IO ([FFILoadError], EvalEnv) -> Eval ([FFILoadError], EvalEnv)
forall a. IO a -> Eval a
io do
  ([FFILoadError]
errs, [(Name, Prim Concrete)]
prims) <- [Either FFILoadError (Name, Prim Concrete)]
-> ([FFILoadError], [(Name, Prim Concrete)])
forall a b. [Either a b] -> ([a], [b])
partitionEithers ([Either FFILoadError (Name, Prim Concrete)]
 -> ([FFILoadError], [(Name, Prim Concrete)]))
-> IO [Either FFILoadError (Name, Prim Concrete)]
-> IO ([FFILoadError], [(Name, Prim Concrete)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Name, FFIFunType)]
-> ((Name, FFIFunType)
    -> IO (Either FFILoadError (Name, Prim Concrete)))
-> IO [Either FFILoadError (Name, Prim Concrete)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [(Name, FFIFunType)]
decls \(Name
name, FFIFunType
ffiFunType) ->
    (ForeignImpl -> (Name, Prim Concrete))
-> Either FFILoadError ForeignImpl
-> Either FFILoadError (Name, Prim Concrete)
forall a b.
(a -> b) -> Either FFILoadError a -> Either FFILoadError b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name
name,) (Prim Concrete -> (Name, Prim Concrete))
-> (ForeignImpl -> Prim Concrete)
-> ForeignImpl
-> (Name, Prim Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> FFIFunType -> ForeignImpl -> Prim Concrete
foreignPrimPoly Name
name FFIFunType
ffiFunType) (Either FFILoadError ForeignImpl
 -> Either FFILoadError (Name, Prim Concrete))
-> IO (Either FFILoadError ForeignImpl)
-> IO (Either FFILoadError (Name, Prim Concrete))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      ForeignSrc -> String -> IO (Either FFILoadError ForeignImpl)
loadForeignImpl ForeignSrc
fsrc (Ident -> String
unpackIdent (Ident -> String) -> Ident -> String
forall a b. (a -> b) -> a -> b
$ Name -> Ident
nameIdent Name
name)
  ([FFILoadError], EvalEnv) -> IO ([FFILoadError], EvalEnv)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([FFILoadError]
errs, ((Name, Prim Concrete) -> EvalEnv -> EvalEnv)
-> EvalEnv -> [(Name, Prim Concrete)] -> EvalEnv
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Name -> Prim Concrete -> EvalEnv -> EvalEnv)
-> (Name, Prim Concrete) -> EvalEnv -> EvalEnv
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Prim Concrete -> EvalEnv -> EvalEnv
forall sym.
Backend sym =>
Name -> Prim sym -> GenEvalEnv sym -> GenEvalEnv sym
bindVarDirect) EvalEnv
env [(Name, Prim Concrete)]
prims)

-- | Generate a 'Prim' value representing the given foreign function, containing
-- all the code necessary to marshal arguments and return values and do the
-- actual FFI call.
foreignPrimPoly :: Name -> FFIFunType -> ForeignImpl -> Prim Concrete
foreignPrimPoly :: Name -> FFIFunType -> ForeignImpl -> Prim Concrete
foreignPrimPoly Name
name FFIFunType
fft ForeignImpl
impl = [TParam] -> TypeEnv -> Prim Concrete
buildNumPoly (FFIFunType -> [TParam]
ffiTParams FFIFunType
fft) TypeEnv
forall a. Monoid a => a
mempty
  where -- Add type lambdas for the type parameters and build a type environment
        -- that we can look up later to compute e.g. array sizes.
        --
        -- Given [p1, p2, ..., pk] {}, returns
        -- PNumPoly \n1 -> PNumPoly \n2 -> ... PNumPoly \nk ->
        --   foreignPrim name fft impl {p1 = n1, p2 = n2, ..., pk = nk}
        buildNumPoly :: [TParam] -> TypeEnv -> Prim Concrete
buildNumPoly (TParam
tp:[TParam]
tps) TypeEnv
tenv = (Nat' -> Prim Concrete) -> Prim Concrete
forall sym. (Nat' -> Prim sym) -> Prim sym
PNumPoly \Nat'
n ->
          [TParam] -> TypeEnv -> Prim Concrete
buildNumPoly [TParam]
tps (TypeEnv -> Prim Concrete) -> TypeEnv -> Prim Concrete
forall a b. (a -> b) -> a -> b
$ TVar -> Either Nat' TValue -> TypeEnv -> TypeEnv
bindTypeVar (TParam -> TVar
TVBound TParam
tp) (Nat' -> Either Nat' TValue
forall a b. a -> Either a b
Left Nat'
n) TypeEnv
tenv
        buildNumPoly [] TypeEnv
tenv = Name -> FFIFunType -> ForeignImpl -> TypeEnv -> Prim Concrete
foreignPrim Name
name FFIFunType
fft ForeignImpl
impl TypeEnv
tenv

-- | Methods for obtaining a return value. The producer of this type must supply
-- both 1) a polymorphic IO object directly containing a return value that the
-- consumer can instantiate at any 'FFIRet' type, and 2) an effectful function
-- that takes some output arguments and modifies what they are pointing at to
-- store a return value. The consumer can choose which one to use.
data GetRet = GetRet
  { GetRet -> forall a. FFIRet a => IO a
getRetAsValue   :: forall a. FFIRet a => IO a
  , GetRet -> [SomeFFIArg] -> IO ()
getRetAsOutArgs :: [SomeFFIArg] -> IO () }

-- | Operations needed for returning a basic reference type.
data BasicRefRet a = BasicRefRet
  { -- | Initialize the object before passing to foreign function.
    forall a. BasicRefRet a -> Ptr a -> IO ()
initBasicRefRet    :: Ptr a -> IO ()
    -- | Free the object after returning from foreign function and obtaining
    -- return value.
  , forall a. BasicRefRet a -> Ptr a -> IO ()
clearBasicRefRet   :: Ptr a -> IO ()
    -- | Convert the object to a Cryptol value.
  , forall a. BasicRefRet a -> a -> Eval (GenValue Concrete)
marshalBasicRefRet :: a -> Eval (GenValue Concrete) }

-- | Generate the monomorphic part of the foreign 'Prim', given a 'TypeEnv'
-- containing all the type arguments we have already received.
foreignPrim :: Name -> FFIFunType -> ForeignImpl -> TypeEnv -> Prim Concrete
foreignPrim :: Name -> FFIFunType -> ForeignImpl -> TypeEnv -> Prim Concrete
foreignPrim Name
name FFIFunType {[TParam]
[FFIType]
FFIType
ffiTParams :: FFIFunType -> [TParam]
ffiTParams :: [TParam]
ffiArgTypes :: [FFIType]
ffiRetType :: FFIType
ffiArgTypes :: FFIFunType -> [FFIType]
ffiRetType :: FFIFunType -> FFIType
..} ForeignImpl
impl TypeEnv
tenv = [FFIType] -> [(FFIType, GenValue Concrete)] -> Prim Concrete
buildFun [FFIType]
ffiArgTypes []
  where

  -- Build up the 'Prim' function for the FFI call.
  --
  -- Given [t1, t2 ... tm] we return
  -- PStrict \v1 -> PStrict \v2 -> ... PStrict \vm -> PPrim $
  --   marshalArg t1 v1 \a1 ->
  --     marshalArg t2 v2 \a2 -> ... marshalArg tm vm \am ->
  --       marshalRet ffiRetType GetRet
  --         { getRetAsValue = callForeignImpl impl [n1, ..., nk, a1, ..., am]
  --         , getRetAsOutArgs = \[o1, ..., ol] ->
  --             callForeignImpl impl [n1, ..., nk, a1, ..., am, o1, ..., ol] }
  buildFun :: [FFIType] -> [(FFIType, GenValue Concrete)] -> Prim Concrete
  buildFun :: [FFIType] -> [(FFIType, GenValue Concrete)] -> Prim Concrete
buildFun (FFIType
argType:[FFIType]
argTypes) [(FFIType, GenValue Concrete)]
typesAndVals = (GenValue Concrete -> Prim Concrete) -> Prim Concrete
forall sym. (GenValue sym -> Prim sym) -> Prim sym
PStrict \GenValue Concrete
val ->
    [FFIType] -> [(FFIType, GenValue Concrete)] -> Prim Concrete
buildFun [FFIType]
argTypes ([(FFIType, GenValue Concrete)] -> Prim Concrete)
-> [(FFIType, GenValue Concrete)] -> Prim Concrete
forall a b. (a -> b) -> a -> b
$ [(FFIType, GenValue Concrete)]
typesAndVals [(FFIType, GenValue Concrete)]
-> [(FFIType, GenValue Concrete)] -> [(FFIType, GenValue Concrete)]
forall a. [a] -> [a] -> [a]
++ [(FFIType
argType, GenValue Concrete
val)]
  buildFun [] [(FFIType, GenValue Concrete)]
typesAndVals = SEval Concrete (GenValue Concrete) -> Prim Concrete
forall sym. SEval sym (GenValue sym) -> Prim sym
PPrim (SEval Concrete (GenValue Concrete) -> Prim Concrete)
-> SEval Concrete (GenValue Concrete) -> Prim Concrete
forall a b. (a -> b) -> a -> b
$
    [(FFIType, GenValue Concrete)]
-> ([SomeFFIArg] -> Eval (GenValue Concrete))
-> Eval (GenValue Concrete)
forall a.
[(FFIType, GenValue Concrete)]
-> ([SomeFFIArg] -> Eval a) -> Eval a
marshalArgs [(FFIType, GenValue Concrete)]
typesAndVals \[SomeFFIArg]
inArgs -> do
      [SomeFFIArg]
tyArgs <- (TParam -> Eval SomeFFIArg) -> [TParam] -> Eval [SomeFFIArg]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse TParam -> Eval SomeFFIArg
marshalTyArg [TParam]
ffiTParams
      let tyInArgs :: [SomeFFIArg]
tyInArgs = [SomeFFIArg]
tyArgs [SomeFFIArg] -> [SomeFFIArg] -> [SomeFFIArg]
forall a. [a] -> [a] -> [a]
++ [SomeFFIArg]
inArgs
      FFIType -> GetRet -> Eval (GenValue Concrete)
marshalRet FFIType
ffiRetType GetRet
        { getRetAsValue :: forall a. FFIRet a => IO a
getRetAsValue = ForeignImpl -> [SomeFFIArg] -> IO a
forall a. FFIRet a => ForeignImpl -> [SomeFFIArg] -> IO a
callForeignImpl ForeignImpl
impl [SomeFFIArg]
tyInArgs
        , getRetAsOutArgs :: [SomeFFIArg] -> IO ()
getRetAsOutArgs = ForeignImpl -> [SomeFFIArg] -> IO ()
forall a. FFIRet a => ForeignImpl -> [SomeFFIArg] -> IO a
callForeignImpl ForeignImpl
impl ([SomeFFIArg] -> IO ())
-> ([SomeFFIArg] -> [SomeFFIArg]) -> [SomeFFIArg] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SomeFFIArg]
tyInArgs [SomeFFIArg] -> [SomeFFIArg] -> [SomeFFIArg]
forall a. [a] -> [a] -> [a]
++) }

  -- Look up the value of a type parameter in the type environment and marshal
  -- it.
  marshalTyArg :: TParam -> Eval SomeFFIArg
  marshalTyArg :: TParam -> Eval SomeFFIArg
marshalTyArg TParam
tp
    | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= CSize -> Integer
forall a. Integral a => a -> Integer
toInteger (CSize
forall a. Bounded a => a
maxBound :: CSize) =
      SomeFFIArg -> Eval SomeFFIArg
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeFFIArg -> Eval SomeFFIArg) -> SomeFFIArg -> Eval SomeFFIArg
forall a b. (a -> b) -> a -> b
$ forall a. FFIArg a => a -> SomeFFIArg
SomeFFIArg @CSize (CSize -> SomeFFIArg) -> CSize -> SomeFFIArg
forall a b. (a -> b) -> a -> b
$ Integer -> CSize
forall a. Num a => Integer -> a
fromInteger Integer
n
    | Bool
otherwise = Concrete -> EvalError -> SEval Concrete SomeFFIArg
forall sym a. Backend sym => sym -> EvalError -> SEval sym a
forall a. Concrete -> EvalError -> SEval Concrete a
raiseError Concrete
Concrete (EvalError -> SEval Concrete SomeFFIArg)
-> EvalError -> SEval Concrete SomeFFIArg
forall a b. (a -> b) -> a -> b
$ Name -> TParam -> Integer -> EvalError
FFITypeNumTooBig Name
name TParam
tp Integer
n
    where n :: Integer
n = Type -> Integer
evalFinType (Type -> Integer) -> Type -> Integer
forall a b. (a -> b) -> a -> b
$ TVar -> Type
TVar (TVar -> Type) -> TVar -> Type
forall a b. (a -> b) -> a -> b
$ TParam -> TVar
TVBound TParam
tp

  -- Marshal the given value as the given FFIType and call the given function
  -- with the results. A single Cryptol argument may correspond to any number of
  -- C arguments, so the callback takes a list.
  --
  -- NOTE: the result must be used only in the callback since it may have a
  -- limited lifetime (e.g. pointer returned by alloca).
  marshalArg ::
    FFIType ->
    GenValue Concrete ->
    ([SomeFFIArg] -> Eval a) ->
    Eval a

  marshalArg :: forall a.
FFIType -> GenValue Concrete -> ([SomeFFIArg] -> Eval a) -> Eval a
marshalArg FFIType
FFIBool GenValue Concrete
val [SomeFFIArg] -> Eval a
f = [SomeFFIArg] -> Eval a
f [forall a. FFIArg a => a -> SomeFFIArg
SomeFFIArg @Word8 (Bool -> Word8
forall a. Num a => Bool -> a
fromBool (GenValue Concrete -> SBit Concrete
forall sym. Backend sym => GenValue sym -> SBit sym
fromVBit GenValue Concrete
val))]

  marshalArg (FFIBasic (FFIBasicVal FFIBasicValType
t)) GenValue Concrete
val [SomeFFIArg] -> Eval a
f =
    FFIBasicValType
-> (forall rep.
    FFIArg rep =>
    (GenValue Concrete -> Eval rep) -> Eval a)
-> Eval a
forall result.
FFIBasicValType
-> (forall rep.
    FFIArg rep =>
    (GenValue Concrete -> Eval rep) -> result)
-> result
getMarshalBasicValArg FFIBasicValType
t \GenValue Concrete -> Eval rep
doExport ->
    do rep
arg <- GenValue Concrete -> Eval rep
doExport GenValue Concrete
val
       [SomeFFIArg] -> Eval a
f [rep -> SomeFFIArg
forall a. FFIArg a => a -> SomeFFIArg
SomeFFIArg rep
arg]

  marshalArg (FFIBasic (FFIBasicRef FFIBasicRefType
t)) GenValue Concrete
val [SomeFFIArg] -> Eval a
f =
    FFIBasicRefType
-> (forall rep.
    Storable rep =>
    (GenValue Concrete -> (rep -> IO a) -> IO a) -> Eval a)
-> Eval a
forall val result.
FFIBasicRefType
-> (forall rep.
    Storable rep =>
    (GenValue Concrete -> (rep -> IO val) -> IO val) -> result)
-> result
getMarshalBasicRefArg FFIBasicRefType
t \GenValue Concrete -> (rep -> IO a) -> IO a
doExport  ->
    -- Since we need to do Eval actions in an IO callback, we need to manually
    -- unwrap and wrap the Eval datatype
    (CallStack -> IO a) -> Eval a
forall a. (CallStack -> IO a) -> Eval a
Eval \CallStack
stk ->
      GenValue Concrete -> (rep -> IO a) -> IO a
doExport GenValue Concrete
val \rep
arg ->
        rep -> (Ptr rep -> IO a) -> IO a
forall a b. Storable a => a -> (Ptr a -> IO b) -> IO b
with rep
arg \Ptr rep
ptr ->
          CallStack -> Eval a -> IO a
forall a. CallStack -> Eval a -> IO a
runEval CallStack
stk ([SomeFFIArg] -> Eval a
f [Ptr rep -> SomeFFIArg
forall a. FFIArg a => a -> SomeFFIArg
SomeFFIArg Ptr rep
ptr])

  marshalArg (FFIArray ((Type -> Integer) -> [Type] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Integer
evalFinType -> [Integer]
sizes) FFIBasicType
bt) GenValue Concrete
val [SomeFFIArg] -> Eval a
f =
    case FFIBasicType
bt of

      FFIBasicVal FFIBasicValType
t ->
        FFIBasicValType
-> (forall rep.
    FFIArg rep =>
    (GenValue Concrete -> Eval rep) -> Eval a)
-> Eval a
forall result.
FFIBasicValType
-> (forall rep.
    FFIArg rep =>
    (GenValue Concrete -> Eval rep) -> result)
-> result
getMarshalBasicValArg FFIBasicValType
t \GenValue Concrete -> Eval rep
doExport  ->
          -- Since we need to do Eval actions in an IO callback,
          -- we need to manually unwrap and wrap the Eval datatype
          (CallStack -> IO a) -> Eval a
forall a. (CallStack -> IO a) -> Eval a
Eval \CallStack
stk ->
            CallStack -> (GenValue Concrete -> (rep -> IO ()) -> IO ()) -> IO a
forall {a}.
Storable a =>
CallStack -> (GenValue Concrete -> (a -> IO ()) -> IO ()) -> IO a
marshalArrayArg CallStack
stk \GenValue Concrete
v rep -> IO ()
k ->
              rep -> IO ()
k (rep -> IO ()) -> IO rep -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< CallStack -> Eval rep -> IO rep
forall a. CallStack -> Eval a -> IO a
runEval CallStack
stk (GenValue Concrete -> Eval rep
doExport GenValue Concrete
v)

      FFIBasicRef FFIBasicRefType
t -> (CallStack -> IO a) -> Eval a
forall a. (CallStack -> IO a) -> Eval a
Eval \CallStack
stk ->
        FFIBasicRefType
-> (forall rep.
    Storable rep =>
    (GenValue Concrete -> (rep -> IO ()) -> IO ()) -> IO a)
-> IO a
forall val result.
FFIBasicRefType
-> (forall rep.
    Storable rep =>
    (GenValue Concrete -> (rep -> IO val) -> IO val) -> result)
-> result
getMarshalBasicRefArg FFIBasicRefType
t \GenValue Concrete -> (rep -> IO ()) -> IO ()
doExport ->
        CallStack -> (GenValue Concrete -> (rep -> IO ()) -> IO ()) -> IO a
forall {a}.
Storable a =>
CallStack -> (GenValue Concrete -> (a -> IO ()) -> IO ()) -> IO a
marshalArrayArg CallStack
stk GenValue Concrete -> (rep -> IO ()) -> IO ()
doExport

    where marshalArrayArg :: CallStack -> (GenValue Concrete -> (a -> IO ()) -> IO ()) -> IO a
marshalArrayArg CallStack
stk GenValue Concrete -> (a -> IO ()) -> IO ()
doExport =
            Int -> (Ptr a -> IO a) -> IO a
forall a b. Storable a => Int -> (Ptr a -> IO b) -> IO b
allocaArray (Integer -> Int
forall a. Num a => Integer -> a
fromInteger ([Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [Integer]
sizes)) \Ptr a
ptr -> do
              -- Traverse the nested sequences and write the elements to the
              -- array in order.
              -- ns is the dimensions of the values we are currently
              -- processing.
              -- vs is the values we are currently processing.
              -- nvss is the stack of previous ns and vs that we keep track of
              -- that we push onto when we start processing a nested sequence
              -- and pop off when we finish processing the current ones.
              -- i is the index into the array.

              let
                  -- write next element of multi-dimensional array
                  write :: [a]
-> [GenValue Concrete]
-> [(a, [GenValue Concrete])]
-> Int
-> IO ()
write (a
n:[a]
ns) (GenValue Concrete
v:[GenValue Concrete]
vs) [(a, [GenValue Concrete])]
nvss !Int
i =
                    do [GenValue Concrete]
vs' <- (Eval (GenValue Concrete) -> IO (GenValue Concrete))
-> [Eval (GenValue Concrete)] -> IO [GenValue Concrete]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (CallStack -> Eval (GenValue Concrete) -> IO (GenValue Concrete)
forall a. CallStack -> Eval a -> IO a
runEval CallStack
stk)
                                       (a
-> SeqMap Concrete (GenValue Concrete)
-> [SEval Concrete (GenValue Concrete)]
forall sym n a.
(Backend sym, Integral n) =>
n -> SeqMap sym a -> [SEval sym a]
enumerateSeqMap a
n (GenValue Concrete -> SeqMap Concrete (GenValue Concrete)
forall sym.
Backend sym =>
GenValue sym -> SeqMap sym (GenValue sym)
fromVSeq GenValue Concrete
v))
                       [a]
-> [GenValue Concrete]
-> [(a, [GenValue Concrete])]
-> Int
-> IO ()
write [a]
ns [GenValue Concrete]
vs' ((a
n, [GenValue Concrete]
vs)(a, [GenValue Concrete])
-> [(a, [GenValue Concrete])] -> [(a, [GenValue Concrete])]
forall a. a -> [a] -> [a]
:[(a, [GenValue Concrete])]
nvss) Int
i

                  -- write next element in flat array
                  write [] (GenValue Concrete
v:[GenValue Concrete]
vs) [(a, [GenValue Concrete])]
nvss !Int
i =
                    GenValue Concrete -> (a -> IO ()) -> IO ()
doExport GenValue Concrete
v \a
rep ->
                      do Ptr a -> Int -> a -> IO ()
forall a. Storable a => Ptr a -> Int -> a -> IO ()
pokeElemOff Ptr a
ptr Int
i a
rep
                         [a]
-> [GenValue Concrete]
-> [(a, [GenValue Concrete])]
-> Int
-> IO ()
write [] [GenValue Concrete]
vs [(a, [GenValue Concrete])]
nvss (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

                  -- finished with flat array, do next element of multi-d array
                  write [a]
ns [] ((a
n, [GenValue Concrete]
vs):[(a, [GenValue Concrete])]
nvss) !Int
i = [a]
-> [GenValue Concrete]
-> [(a, [GenValue Concrete])]
-> Int
-> IO ()
write (a
na -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
ns) [GenValue Concrete]
vs [(a, [GenValue Concrete])]
nvss Int
i

                  -- done
                  write [a]
_ [GenValue Concrete]
_ [] Int
_ = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()


              [Integer]
-> [GenValue Concrete]
-> [(Integer, [GenValue Concrete])]
-> Int
-> IO ()
forall {a}.
Integral a =>
[a]
-> [GenValue Concrete]
-> [(a, [GenValue Concrete])]
-> Int
-> IO ()
write [Integer]
sizes [GenValue Concrete
val] [] Int
0
              CallStack -> Eval a -> IO a
forall a. CallStack -> Eval a -> IO a
runEval CallStack
stk (Eval a -> IO a) -> Eval a -> IO a
forall a b. (a -> b) -> a -> b
$ [SomeFFIArg] -> Eval a
f [Ptr a -> SomeFFIArg
forall a. FFIArg a => a -> SomeFFIArg
SomeFFIArg Ptr a
ptr]

  marshalArg (FFITuple [FFIType]
types) GenValue Concrete
val [SomeFFIArg] -> Eval a
f =
    do [GenValue Concrete]
vals <- [Eval (GenValue Concrete)] -> Eval [GenValue Concrete]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence (GenValue Concrete -> [SEval Concrete (GenValue Concrete)]
forall sym.
Backend sym =>
GenValue sym -> [SEval sym (GenValue sym)]
fromVTuple GenValue Concrete
val)
       [(FFIType, GenValue Concrete)]
-> ([SomeFFIArg] -> Eval a) -> Eval a
forall a.
[(FFIType, GenValue Concrete)]
-> ([SomeFFIArg] -> Eval a) -> Eval a
marshalArgs ([FFIType]
types [FFIType] -> [GenValue Concrete] -> [(FFIType, GenValue Concrete)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [GenValue Concrete]
vals) [SomeFFIArg] -> Eval a
f

  marshalArg (FFIRecord RecordMap Ident FFIType
typeMap) GenValue Concrete
val [SomeFFIArg] -> Eval a
f =
    do [GenValue Concrete]
vals <- (Ident -> Eval (GenValue Concrete))
-> [Ident] -> Eval [GenValue Concrete]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (Ident -> GenValue Concrete -> SEval Concrete (GenValue Concrete)
forall sym.
Backend sym =>
Ident -> GenValue sym -> SEval sym (GenValue sym)
`lookupRecord` GenValue Concrete
val) (RecordMap Ident FFIType -> [Ident]
forall a b. RecordMap a b -> [a]
displayOrder RecordMap Ident FFIType
typeMap)
       [(FFIType, GenValue Concrete)]
-> ([SomeFFIArg] -> Eval a) -> Eval a
forall a.
[(FFIType, GenValue Concrete)]
-> ([SomeFFIArg] -> Eval a) -> Eval a
marshalArgs (RecordMap Ident FFIType -> [FFIType]
forall a b. (Show a, Ord a) => RecordMap a b -> [b]
displayElements RecordMap Ident FFIType
typeMap [FFIType] -> [GenValue Concrete] -> [(FFIType, GenValue Concrete)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [GenValue Concrete]
vals) [SomeFFIArg] -> Eval a
f

  -- Call marshalArg on a bunch of arguments and collect the results together
  -- (in the order of the arguments).
  marshalArgs ::
    [(FFIType, GenValue Concrete)] ->
    ([SomeFFIArg] -> Eval a) ->
    Eval a
  marshalArgs :: forall a.
[(FFIType, GenValue Concrete)]
-> ([SomeFFIArg] -> Eval a) -> Eval a
marshalArgs [(FFIType, GenValue Concrete)]
typesAndVals [SomeFFIArg] -> Eval a
f = [(FFIType, GenValue Concrete)] -> [[SomeFFIArg]] -> Eval a
go [(FFIType, GenValue Concrete)]
typesAndVals []
    where
    go :: [(FFIType, GenValue Concrete)] -> [[SomeFFIArg]] -> Eval a
go [] [[SomeFFIArg]]
args = [SomeFFIArg] -> Eval a
f ([[SomeFFIArg]] -> [SomeFFIArg]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[SomeFFIArg]] -> [[SomeFFIArg]]
forall a. [a] -> [a]
reverse [[SomeFFIArg]]
args))
    go ((FFIType
t, GenValue Concrete
v):[(FFIType, GenValue Concrete)]
tvs) [[SomeFFIArg]]
prevArgs =
      FFIType -> GenValue Concrete -> ([SomeFFIArg] -> Eval a) -> Eval a
forall a.
FFIType -> GenValue Concrete -> ([SomeFFIArg] -> Eval a) -> Eval a
marshalArg FFIType
t GenValue Concrete
v \[SomeFFIArg]
currArgs ->
      [(FFIType, GenValue Concrete)] -> [[SomeFFIArg]] -> Eval a
go [(FFIType, GenValue Concrete)]
tvs ([SomeFFIArg]
currArgs [SomeFFIArg] -> [[SomeFFIArg]] -> [[SomeFFIArg]]
forall a. a -> [a] -> [a]
: [[SomeFFIArg]]
prevArgs)

  -- Given an FFIType and a GetRet, obtain a return value and convert it to a
  -- Cryptol value. The return value is obtained differently depending on the
  -- FFIType.
  marshalRet :: FFIType -> GetRet -> Eval (GenValue Concrete)
  marshalRet :: FFIType -> GetRet -> Eval (GenValue Concrete)
marshalRet FFIType
FFIBool GetRet
gr =
    do Word8
rep <- IO Word8 -> Eval Word8
forall a. IO a -> Eval a
io (GetRet -> forall a. FFIRet a => IO a
getRetAsValue GetRet
gr @Word8)
       GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SBit Concrete -> GenValue Concrete
forall sym. SBit sym -> GenValue sym
VBit (Word8 -> Bool
forall a. (Eq a, Num a) => a -> Bool
toBool Word8
rep))

  marshalRet (FFIBasic (FFIBasicVal FFIBasicValType
t)) GetRet
gr =
    FFIBasicValType
-> (forall a.
    FFIRet a =>
    (a -> Eval (GenValue Concrete)) -> Eval (GenValue Concrete))
-> Eval (GenValue Concrete)
forall b.
FFIBasicValType
-> (forall a. FFIRet a => (a -> Eval (GenValue Concrete)) -> b)
-> b
getMarshalBasicValRet FFIBasicValType
t \a -> Eval (GenValue Concrete)
doImport ->
      do a
rep <- IO a -> Eval a
forall a. IO a -> Eval a
io (GetRet -> forall a. FFIRet a => IO a
getRetAsValue GetRet
gr)
         a -> Eval (GenValue Concrete)
doImport a
rep

  marshalRet (FFIBasic (FFIBasicRef FFIBasicRefType
t)) GetRet
gr =
    FFIBasicRefType
-> (forall a.
    Storable a =>
    BasicRefRet a -> Eval (GenValue Concrete))
-> Eval (GenValue Concrete)
forall b.
FFIBasicRefType
-> (forall a. Storable a => BasicRefRet a -> b) -> b
getBasicRefRet FFIBasicRefType
t \BasicRefRet a
how ->
    (CallStack -> IO (GenValue Concrete)) -> Eval (GenValue Concrete)
forall a. (CallStack -> IO a) -> Eval a
Eval             \CallStack
stk ->
    (Ptr a -> IO (GenValue Concrete)) -> IO (GenValue Concrete)
forall a b. Storable a => (Ptr a -> IO b) -> IO b
alloca           \Ptr a
ptr ->
    IO () -> IO () -> IO (GenValue Concrete) -> IO (GenValue Concrete)
forall a b c. IO a -> IO b -> IO c -> IO c
bracket_ (BasicRefRet a -> Ptr a -> IO ()
forall a. BasicRefRet a -> Ptr a -> IO ()
initBasicRefRet BasicRefRet a
how Ptr a
ptr) (BasicRefRet a -> Ptr a -> IO ()
forall a. BasicRefRet a -> Ptr a -> IO ()
clearBasicRefRet BasicRefRet a
how Ptr a
ptr)
      do GetRet -> [SomeFFIArg] -> IO ()
getRetAsOutArgs GetRet
gr [Ptr a -> SomeFFIArg
forall a. FFIArg a => a -> SomeFFIArg
SomeFFIArg Ptr a
ptr]
         a
rep <- Ptr a -> IO a
forall a. Storable a => Ptr a -> IO a
peek Ptr a
ptr
         CallStack -> Eval (GenValue Concrete) -> IO (GenValue Concrete)
forall a. CallStack -> Eval a -> IO a
runEval CallStack
stk (BasicRefRet a -> a -> Eval (GenValue Concrete)
forall a. BasicRefRet a -> a -> Eval (GenValue Concrete)
marshalBasicRefRet BasicRefRet a
how a
rep)

  marshalRet (FFIArray ((Type -> Integer) -> [Type] -> [Integer]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Integer
evalFinType -> [Integer]
sizes) FFIBasicType
bt) GetRet
gr =
    (CallStack -> IO (GenValue Concrete)) -> Eval (GenValue Concrete)
forall a. (CallStack -> IO a) -> Eval a
Eval \CallStack
stk -> do
    let totalSize :: Int
totalSize = Integer -> Int
forall a. Num a => Integer -> a
fromInteger ([Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product [Integer]
sizes)
        getResult :: (t -> Eval (GenValue Concrete)) -> Ptr t -> IO (GenValue Concrete)
getResult t -> Eval (GenValue Concrete)
marshal Ptr t
ptr = do
          GetRet -> [SomeFFIArg] -> IO ()
getRetAsOutArgs GetRet
gr [Ptr t -> SomeFFIArg
forall a. FFIArg a => a -> SomeFFIArg
SomeFFIArg Ptr t
ptr]
          let tyv :: TValue
tyv = case FFIBasicType
bt of
                FFIBasicVal FFIBasicValType
bv -> case FFIBasicValType
bv of
                  FFIWord Integer
len FFIWordSize
_ -> Integer -> TValue -> TValue
TVSeq Integer
len TValue
TVBit
                  FFIFloat Integer
e Integer
p FFIFloatSize
_ -> Integer -> Integer -> TValue
TVFloat Integer
e Integer
p
                FFIBasicRef FFIBasicRefType
br -> case FFIBasicRefType
br of
                  FFIInteger Maybe Type
Nothing -> TValue
TVInteger
                  FFIInteger (Just Type
z) -> Integer -> TValue
TVIntMod (Integer -> TValue) -> Integer -> TValue
forall a b. (a -> b) -> a -> b
$ Type -> Integer
evalFinType Type
z
                  FFIBasicRefType
FFIRational -> TValue
TVRational

          let build :: [Integer] -> Int -> IO (GenValue Concrete)
build (Integer
n:[Integer]
ns) !Int
i = do
                -- We need to be careful to actually run this here and not just
                -- stick the IO action into the sequence with io, or else we
                -- will read from the array after it is deallocated.
                [GenValue Concrete]
vs <- [Int] -> (Int -> IO (GenValue Concrete)) -> IO [GenValue Concrete]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
t a -> (a -> f b) -> f (t b)
for [Int
0 .. Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] \Int
j ->
                  [Integer] -> Int -> IO (GenValue Concrete)
build [Integer]
ns (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
* Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
j)
                CallStack -> Eval (GenValue Concrete) -> IO (GenValue Concrete)
forall a. CallStack -> Eval a -> IO a
runEval CallStack
stk (Eval (GenValue Concrete) -> IO (GenValue Concrete))
-> Eval (GenValue Concrete) -> IO (GenValue Concrete)
forall a b. (a -> b) -> a -> b
$ 
                  Concrete
-> Nat'
-> TValue
-> SeqMap Concrete (GenValue Concrete)
-> SEval Concrete (GenValue Concrete)
forall sym.
Backend sym =>
sym
-> Nat'
-> TValue
-> SeqMap sym (GenValue sym)
-> SEval sym (GenValue sym)
mkSeq Concrete
Concrete (Integer -> Nat'
Nat Integer
n) TValue
tyv (Concrete
-> [SEval Concrete (GenValue Concrete)]
-> SeqMap Concrete (GenValue Concrete)
forall sym a. Backend sym => sym -> [SEval sym a] -> SeqMap sym a
finiteSeqMap Concrete
Concrete ((GenValue Concrete -> Eval (GenValue Concrete))
-> [GenValue Concrete] -> [Eval (GenValue Concrete)]
forall a b. (a -> b) -> [a] -> [b]
map GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [GenValue Concrete]
vs))
              build [] !Int
i = do
                t
e <- Ptr t -> Int -> IO t
forall a. Storable a => Ptr a -> Int -> IO a
peekElemOff Ptr t
ptr Int
i
                CallStack -> Eval (GenValue Concrete) -> IO (GenValue Concrete)
forall a. CallStack -> Eval a -> IO a
runEval CallStack
stk (t -> Eval (GenValue Concrete)
marshal t
e)

          [Integer] -> Int -> IO (GenValue Concrete)
build [Integer]
sizes Int
0

    case FFIBasicType
bt of

      FFIBasicVal FFIBasicValType
t ->
        FFIBasicValType
-> (forall a.
    FFIRet a =>
    (a -> Eval (GenValue Concrete)) -> IO (GenValue Concrete))
-> IO (GenValue Concrete)
forall b.
FFIBasicValType
-> (forall a. FFIRet a => (a -> Eval (GenValue Concrete)) -> b)
-> b
getMarshalBasicValRet FFIBasicValType
t \a -> Eval (GenValue Concrete)
doImport ->
        Int -> (Ptr a -> IO (GenValue Concrete)) -> IO (GenValue Concrete)
forall a b. Storable a => Int -> (Ptr a -> IO b) -> IO b
allocaArray Int
totalSize ((a -> Eval (GenValue Concrete)) -> Ptr a -> IO (GenValue Concrete)
forall {t}.
Storable t =>
(t -> Eval (GenValue Concrete)) -> Ptr t -> IO (GenValue Concrete)
getResult a -> Eval (GenValue Concrete)
doImport)

      FFIBasicRef FFIBasicRefType
t ->
        FFIBasicRefType
-> (forall a.
    Storable a =>
    BasicRefRet a -> IO (GenValue Concrete))
-> IO (GenValue Concrete)
forall b.
FFIBasicRefType
-> (forall a. Storable a => BasicRefRet a -> b) -> b
getBasicRefRet FFIBasicRefType
t      \BasicRefRet a
how ->
        Int -> (Ptr a -> IO (GenValue Concrete)) -> IO (GenValue Concrete)
forall a b. Storable a => Int -> (Ptr a -> IO b) -> IO b
allocaArray Int
totalSize \Ptr a
ptr ->
          do let forEach :: (Ptr a -> f b) -> f ()
forEach Ptr a -> f b
f = [Int] -> (Int -> f b) -> f ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Int
0 .. Int
totalSize Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1] (Ptr a -> f b
f (Ptr a -> f b) -> (Int -> Ptr a) -> Int -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ptr a -> Int -> Ptr a
forall a. Storable a => Ptr a -> Int -> Ptr a
advancePtr Ptr a
ptr)
             IO () -> IO () -> IO (GenValue Concrete) -> IO (GenValue Concrete)
forall a b c. IO a -> IO b -> IO c -> IO c
bracket_ ((Ptr a -> IO ()) -> IO ()
forall {f :: * -> *} {b}. Applicative f => (Ptr a -> f b) -> f ()
forEach (BasicRefRet a -> Ptr a -> IO ()
forall a. BasicRefRet a -> Ptr a -> IO ()
initBasicRefRet BasicRefRet a
how))
                      ((Ptr a -> IO ()) -> IO ()
forall {f :: * -> *} {b}. Applicative f => (Ptr a -> f b) -> f ()
forEach (BasicRefRet a -> Ptr a -> IO ()
forall a. BasicRefRet a -> Ptr a -> IO ()
clearBasicRefRet BasicRefRet a
how))
                      ((a -> Eval (GenValue Concrete)) -> Ptr a -> IO (GenValue Concrete)
forall {t}.
Storable t =>
(t -> Eval (GenValue Concrete)) -> Ptr t -> IO (GenValue Concrete)
getResult (BasicRefRet a -> a -> Eval (GenValue Concrete)
forall a. BasicRefRet a -> a -> Eval (GenValue Concrete)
marshalBasicRefRet BasicRefRet a
how) Ptr a
ptr)

  marshalRet (FFITuple [FFIType]
types) GetRet
gr = [Eval (GenValue Concrete)] -> GenValue Concrete
[SEval Concrete (GenValue Concrete)] -> GenValue Concrete
forall sym. [SEval sym (GenValue sym)] -> GenValue sym
VTuple ([Eval (GenValue Concrete)] -> GenValue Concrete)
-> Eval [Eval (GenValue Concrete)] -> Eval (GenValue Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FFIType] -> GetRet -> Eval [Eval (GenValue Concrete)]
marshalMultiRet [FFIType]
types GetRet
gr

  marshalRet (FFIRecord RecordMap Ident FFIType
typeMap) GetRet
gr =
    RecordMap Ident (Eval (GenValue Concrete)) -> GenValue Concrete
RecordMap Ident (SEval Concrete (GenValue Concrete))
-> GenValue Concrete
forall sym.
RecordMap Ident (SEval sym (GenValue sym)) -> GenValue sym
VRecord (RecordMap Ident (Eval (GenValue Concrete)) -> GenValue Concrete)
-> ([Eval (GenValue Concrete)]
    -> RecordMap Ident (Eval (GenValue Concrete)))
-> [Eval (GenValue Concrete)]
-> GenValue Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Ident, Eval (GenValue Concrete))]
-> RecordMap Ident (Eval (GenValue Concrete))
forall a b. (Show a, Ord a) => [(a, b)] -> RecordMap a b
recordFromFields ([(Ident, Eval (GenValue Concrete))]
 -> RecordMap Ident (Eval (GenValue Concrete)))
-> ([Eval (GenValue Concrete)]
    -> [(Ident, Eval (GenValue Concrete))])
-> [Eval (GenValue Concrete)]
-> RecordMap Ident (Eval (GenValue Concrete))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Ident]
-> [Eval (GenValue Concrete)]
-> [(Ident, Eval (GenValue Concrete))]
forall a b. [a] -> [b] -> [(a, b)]
zip (RecordMap Ident FFIType -> [Ident]
forall a b. RecordMap a b -> [a]
displayOrder RecordMap Ident FFIType
typeMap) ([Eval (GenValue Concrete)] -> GenValue Concrete)
-> Eval [Eval (GenValue Concrete)] -> Eval (GenValue Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      [FFIType] -> GetRet -> Eval [Eval (GenValue Concrete)]
marshalMultiRet (RecordMap Ident FFIType -> [FFIType]
forall a b. (Show a, Ord a) => RecordMap a b -> [b]
displayElements RecordMap Ident FFIType
typeMap) GetRet
gr

  -- Obtain multiple return values as output arguments for a composite return
  -- type. Each return value is fully evaluated but put back in an Eval since
  -- VTuple and VRecord expect it.
  marshalMultiRet :: [FFIType] -> GetRet -> Eval [Eval (GenValue Concrete)]
  -- Since IO callbacks are involved we just do the whole thing in IO and wrap
  -- it in an Eval at the end. This should be fine since we are not changing
  -- the (Cryptol) call stack.
  marshalMultiRet :: [FFIType] -> GetRet -> Eval [Eval (GenValue Concrete)]
marshalMultiRet [FFIType]
types GetRet
gr = (CallStack -> IO [Eval (GenValue Concrete)])
-> Eval [Eval (GenValue Concrete)]
forall a. (CallStack -> IO a) -> Eval a
Eval \CallStack
stk -> do
    -- We use this IORef hack here since we are calling marshalRet recursively
    -- but marshalRet doesn't let us return any extra information from the
    -- callback through to the result of the function. So we remember the result
    -- as a side effect.
    IORef [GenValue Concrete]
vals <- [GenValue Concrete] -> IO (IORef [GenValue Concrete])
forall a. a -> IO (IORef a)
newIORef []
    let go :: [FFIType] -> [SomeFFIArg] -> IO ()
go [] [SomeFFIArg]
args = GetRet -> [SomeFFIArg] -> IO ()
getRetAsOutArgs GetRet
gr [SomeFFIArg]
args
        go (FFIType
t:[FFIType]
ts) [SomeFFIArg]
prevArgs = do
          GenValue Concrete
val <- CallStack -> Eval (GenValue Concrete) -> IO (GenValue Concrete)
forall a. CallStack -> Eval a -> IO a
runEval CallStack
stk (Eval (GenValue Concrete) -> IO (GenValue Concrete))
-> Eval (GenValue Concrete) -> IO (GenValue Concrete)
forall a b. (a -> b) -> a -> b
$ FFIType -> GetRet -> Eval (GenValue Concrete)
marshalRet FFIType
t (GetRet -> Eval (GenValue Concrete))
-> GetRet -> Eval (GenValue Concrete)
forall a b. (a -> b) -> a -> b
$ ([SomeFFIArg] -> IO ()) -> GetRet
getRetFromAsOutArgs \[SomeFFIArg]
currArgs ->
            [FFIType] -> [SomeFFIArg] -> IO ()
go [FFIType]
ts ([SomeFFIArg]
prevArgs [SomeFFIArg] -> [SomeFFIArg] -> [SomeFFIArg]
forall a. [a] -> [a] -> [a]
++ [SomeFFIArg]
currArgs)
          IORef [GenValue Concrete]
-> ([GenValue Concrete] -> [GenValue Concrete]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef [GenValue Concrete]
vals (GenValue Concrete
val GenValue Concrete -> [GenValue Concrete] -> [GenValue Concrete]
forall a. a -> [a] -> [a]
:)
    [FFIType] -> [SomeFFIArg] -> IO ()
go [FFIType]
types []
    (GenValue Concrete -> Eval (GenValue Concrete))
-> [GenValue Concrete] -> [Eval (GenValue Concrete)]
forall a b. (a -> b) -> [a] -> [b]
map GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([GenValue Concrete] -> [Eval (GenValue Concrete)])
-> IO [GenValue Concrete] -> IO [Eval (GenValue Concrete)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [GenValue Concrete] -> IO [GenValue Concrete]
forall a. IORef a -> IO a
readIORef IORef [GenValue Concrete]
vals

  -- | Call the callback with a 'BasicRefRet' for the given type.
  getBasicRefRet :: FFIBasicRefType ->
    (forall a. Storable a => BasicRefRet a -> b) -> b
  getBasicRefRet :: forall b.
FFIBasicRefType
-> (forall a. Storable a => BasicRefRet a -> b) -> b
getBasicRefRet (FFIInteger Maybe Type
mbMod) forall a. Storable a => BasicRefRet a -> b
f = BasicRefRet MPZ -> b
forall a. Storable a => BasicRefRet a -> b
f BasicRefRet
    { initBasicRefRet :: Ptr MPZ -> IO ()
initBasicRefRet = Ptr MPZ -> IO ()
mpz_init
    , clearBasicRefRet :: Ptr MPZ -> IO ()
clearBasicRefRet = Ptr MPZ -> IO ()
mpz_clear
    , marshalBasicRefRet :: MPZ -> Eval (GenValue Concrete)
marshalBasicRefRet = \MPZ
mpz -> do
        Integer
n <- IO Integer -> Eval Integer
forall a. IO a -> Eval a
io (IO Integer -> Eval Integer) -> IO Integer -> Eval Integer
forall a b. (a -> b) -> a -> b
$ MPZ -> IO Integer
peekInteger' MPZ
mpz
        Integer -> GenValue Concrete
SInteger Concrete -> GenValue Concrete
forall sym. SInteger sym -> GenValue sym
VInteger (Integer -> GenValue Concrete)
-> Eval Integer -> Eval (GenValue Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
          case Maybe Type
mbMod of
            Maybe Type
Nothing -> Integer -> Eval Integer
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
n
            Just Type
m  -> Concrete
-> Integer
-> SInteger Concrete
-> SEval Concrete (SInteger Concrete)
forall sym.
Backend sym =>
sym -> Integer -> SInteger sym -> SEval sym (SInteger sym)
intToZn Concrete
Concrete (Type -> Integer
evalFinType Type
m) Integer
SInteger Concrete
n }
  getBasicRefRet FFIBasicRefType
FFIRational forall a. Storable a => BasicRefRet a -> b
f = BasicRefRet MPQ -> b
forall a. Storable a => BasicRefRet a -> b
f BasicRefRet
    { initBasicRefRet :: Ptr MPQ -> IO ()
initBasicRefRet = Ptr MPQ -> IO ()
mpq_init
    , clearBasicRefRet :: Ptr MPQ -> IO ()
clearBasicRefRet = Ptr MPQ -> IO ()
mpq_clear
    , marshalBasicRefRet :: MPQ -> Eval (GenValue Concrete)
marshalBasicRefRet = \MPQ
mpq -> do
        Rational
r <- IO Rational -> Eval Rational
forall a. IO a -> Eval a
io (IO Rational -> Eval Rational) -> IO Rational -> Eval Rational
forall a b. (a -> b) -> a -> b
$ MPQ -> IO Rational
peekRational' MPQ
mpq
        GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue Concrete -> Eval (GenValue Concrete))
-> GenValue Concrete -> Eval (GenValue Concrete)
forall a b. (a -> b) -> a -> b
$ SRational Concrete -> GenValue Concrete
forall sym. SRational sym -> GenValue sym
VRational (SRational Concrete -> GenValue Concrete)
-> SRational Concrete -> GenValue Concrete
forall a b. (a -> b) -> a -> b
$ SInteger Concrete -> SInteger Concrete -> SRational Concrete
forall sym. SInteger sym -> SInteger sym -> SRational sym
SRational (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
r) (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
r) }

  -- Evaluate a finite numeric type expression.
  evalFinType :: Type -> Integer
  evalFinType :: Type -> Integer
evalFinType = Nat' -> Integer
finNat' (Nat' -> Integer) -> (Type -> Nat') -> Type -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeEnv -> Type -> Nat'
evalNumType TypeEnv
tenv

-- | Given a way to 'getRetAsOutArgs', create a 'GetRet', where the
-- 'getRetAsValue' simply allocates a temporary space to call 'getRetAsOutArgs'
-- on. This is useful for return types that we know how to obtain directly as a
-- value but need to obtain as an output argument when multiple return values
-- are involved.
getRetFromAsOutArgs :: ([SomeFFIArg] -> IO ()) -> GetRet
getRetFromAsOutArgs :: ([SomeFFIArg] -> IO ()) -> GetRet
getRetFromAsOutArgs [SomeFFIArg] -> IO ()
f = GetRet
  { getRetAsValue :: forall a. FFIRet a => IO a
getRetAsValue = (Ptr a -> IO a) -> IO a
forall a b. Storable a => (Ptr a -> IO b) -> IO b
alloca \Ptr a
ptr -> do
      [SomeFFIArg] -> IO ()
f [Ptr a -> SomeFFIArg
forall a. FFIArg a => a -> SomeFFIArg
SomeFFIArg Ptr a
ptr]
      Ptr a -> IO a
forall a. Storable a => Ptr a -> IO a
peek Ptr a
ptr
  , getRetAsOutArgs :: [SomeFFIArg] -> IO ()
getRetAsOutArgs = [SomeFFIArg] -> IO ()
f }

-- | Given a 'FFIBasicValType', call the callback with a marshalling function
-- that marshals values to the 'FFIArg' type corresponding to the
-- 'FFIBasicValType'. The callback must be able to handle marshalling functions
-- that marshal to any 'FFIArg' type.
getMarshalBasicValArg ::
  FFIBasicValType ->
  (forall rep.
      FFIArg rep =>
      (GenValue Concrete -> Eval rep) ->
      result) ->
  result

getMarshalBasicValArg :: forall result.
FFIBasicValType
-> (forall rep.
    FFIArg rep =>
    (GenValue Concrete -> Eval rep) -> result)
-> result
getMarshalBasicValArg (FFIWord Integer
_ FFIWordSize
s) forall rep. FFIArg rep => (GenValue Concrete -> Eval rep) -> result
f = FFIWordSize
-> (forall a.
    (FFIArg a, FFIRet a, Integral a) =>
    Proxy a -> result)
-> result
forall b.
FFIWordSize
-> (forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b)
-> b
withWordType FFIWordSize
s \(Proxy a
_ :: p t) ->
  forall rep. FFIArg rep => (GenValue Concrete -> Eval rep) -> result
f @t ((GenValue Concrete -> Eval a) -> result)
-> (GenValue Concrete -> Eval a) -> result
forall a b. (a -> b) -> a -> b
$ (BV -> a) -> Eval BV -> Eval a
forall a b. (a -> b) -> Eval a -> Eval b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Integer -> a
forall a. Num a => Integer -> a
fromInteger (Integer -> a) -> (BV -> Integer) -> BV -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BV -> Integer
bvVal) (Eval BV -> Eval a)
-> (GenValue Concrete -> Eval BV) -> GenValue Concrete -> Eval a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Concrete
-> String -> GenValue Concrete -> SEval Concrete (SWord Concrete)
forall sym.
Backend sym =>
sym -> String -> GenValue sym -> SEval sym (SWord sym)
fromVWord Concrete
Concrete String
"getMarshalBasicValArg"

getMarshalBasicValArg (FFIFloat Integer
_ Integer
_ FFIFloatSize
s) forall rep. FFIArg rep => (GenValue Concrete -> Eval rep) -> result
f =
  case FFIFloatSize
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.
    FFIFloatSize
FFIFloat32 -> (GenValue Concrete -> Eval CFloat) -> result
forall rep. FFIArg rep => (GenValue Concrete -> Eval rep) -> result
f ((GenValue Concrete -> Eval CFloat) -> result)
-> (GenValue Concrete -> Eval CFloat) -> result
forall a b. (a -> b) -> a -> b
$ CFloat -> Eval CFloat
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CFloat -> Eval CFloat)
-> (GenValue Concrete -> CFloat)
-> GenValue Concrete
-> Eval CFloat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Float -> CFloat
CFloat (Float -> CFloat)
-> (GenValue Concrete -> Float) -> GenValue Concrete -> CFloat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> Float
double2Float (Double -> Float)
-> (GenValue Concrete -> Double) -> GenValue Concrete -> Float
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenValue Concrete -> Double
toDouble
    FFIFloatSize
FFIFloat64 -> (GenValue Concrete -> Eval CDouble) -> result
forall rep. FFIArg rep => (GenValue Concrete -> Eval rep) -> result
f ((GenValue Concrete -> Eval CDouble) -> result)
-> (GenValue Concrete -> Eval CDouble) -> result
forall a b. (a -> b) -> a -> b
$ CDouble -> Eval CDouble
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CDouble -> Eval CDouble)
-> (GenValue Concrete -> CDouble)
-> GenValue Concrete
-> Eval CDouble
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> CDouble
CDouble (Double -> CDouble)
-> (GenValue Concrete -> Double) -> GenValue Concrete -> CDouble
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenValue Concrete -> Double
toDouble
  where
  toDouble :: GenValue Concrete -> Double
toDouble = (Double, Status) -> Double
forall a b. (a, b) -> a
fst ((Double, Status) -> Double)
-> (GenValue Concrete -> (Double, Status))
-> GenValue Concrete
-> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RoundMode -> BigFloat -> (Double, Status)
bfToDouble RoundMode
NearEven (BigFloat -> (Double, Status))
-> (GenValue Concrete -> BigFloat)
-> GenValue Concrete
-> (Double, Status)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BF -> BigFloat
bfValue (BF -> BigFloat)
-> (GenValue Concrete -> BF) -> GenValue Concrete -> BigFloat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenValue Concrete -> BF
GenValue Concrete -> SFloat Concrete
forall sym. Backend sym => GenValue sym -> SFloat sym
fromVFloat

-- | Given a 'FFIBasicValType', call the callback with an unmarshalling function
-- from the 'FFIRet' type corresponding to the 'FFIBasicValType' to Cryptol
-- values. The callback must be able to handle unmarshalling functions from any
-- 'FFIRet' type.
getMarshalBasicValRet :: FFIBasicValType ->
  (forall a. FFIRet a => (a -> Eval (GenValue Concrete)) -> b) -> b
getMarshalBasicValRet :: forall b.
FFIBasicValType
-> (forall a. FFIRet a => (a -> Eval (GenValue Concrete)) -> b)
-> b
getMarshalBasicValRet (FFIWord Integer
n FFIWordSize
s) forall a. FFIRet a => (a -> Eval (GenValue Concrete)) -> b
f = FFIWordSize
-> (forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b)
-> b
forall b.
FFIWordSize
-> (forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b)
-> b
withWordType FFIWordSize
s \(Proxy a
_ :: p t) ->
  forall a. FFIRet a => (a -> Eval (GenValue Concrete)) -> b
f @t ((a -> Eval (GenValue Concrete)) -> b)
-> (a -> Eval (GenValue Concrete)) -> b
forall a b. (a -> b) -> a -> b
$ Concrete
-> Integer -> Integer -> SEval Concrete (GenValue Concrete)
forall sym.
Backend sym =>
sym -> Integer -> Integer -> SEval sym (GenValue sym)
word Concrete
Concrete Integer
n (Integer -> Eval (GenValue Concrete))
-> (a -> Integer) -> a -> Eval (GenValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Integer
forall a. Integral a => a -> Integer
toInteger
getMarshalBasicValRet (FFIFloat Integer
e Integer
p FFIFloatSize
s) forall a. FFIRet a => (a -> Eval (GenValue Concrete)) -> b
f =
  case FFIFloatSize
s of
    FFIFloatSize
FFIFloat32 -> (CFloat -> Eval (GenValue Concrete)) -> b
forall a. FFIRet a => (a -> Eval (GenValue Concrete)) -> b
f ((CFloat -> Eval (GenValue Concrete)) -> b)
-> (CFloat -> Eval (GenValue Concrete)) -> b
forall a b. (a -> b) -> a -> b
$ Double -> Eval (GenValue Concrete)
toValue (Double -> Eval (GenValue Concrete))
-> (CFloat -> Double) -> CFloat -> Eval (GenValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case CFloat Float
x -> Float -> Double
float2Double Float
x
    FFIFloatSize
FFIFloat64 -> (CDouble -> Eval (GenValue Concrete)) -> b
forall a. FFIRet a => (a -> Eval (GenValue Concrete)) -> b
f ((CDouble -> Eval (GenValue Concrete)) -> b)
-> (CDouble -> Eval (GenValue Concrete)) -> b
forall a b. (a -> b) -> a -> b
$ Double -> Eval (GenValue Concrete)
toValue (Double -> Eval (GenValue Concrete))
-> (CDouble -> Double) -> CDouble -> Eval (GenValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case CDouble Double
x -> Double
x
  where toValue :: Double -> Eval (GenValue Concrete)
toValue = GenValue Concrete -> Eval (GenValue Concrete)
forall a. a -> Eval a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (GenValue Concrete -> Eval (GenValue Concrete))
-> (Double -> GenValue Concrete)
-> Double
-> Eval (GenValue Concrete)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BF -> GenValue Concrete
SFloat Concrete -> GenValue Concrete
forall sym. SFloat sym -> GenValue sym
VFloat (BF -> GenValue Concrete)
-> (Double -> BF) -> Double -> GenValue Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer -> BigFloat -> BF
BF Integer
e Integer
p (BigFloat -> BF) -> (Double -> BigFloat) -> Double -> BF
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> BigFloat
bfFromDouble

-- | Call the callback with the Word type corresponding to the given
-- 'FFIWordSize'.
withWordType :: FFIWordSize ->
  (forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b) -> b
withWordType :: forall b.
FFIWordSize
-> (forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b)
-> b
withWordType FFIWordSize
FFIWord8  forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b
f = Proxy Word8 -> b
forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b
f (Proxy Word8 -> b) -> Proxy Word8 -> b
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Word8
withWordType FFIWordSize
FFIWord16 forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b
f = Proxy Word16 -> b
forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b
f (Proxy Word16 -> b) -> Proxy Word16 -> b
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Word16
withWordType FFIWordSize
FFIWord32 forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b
f = Proxy Word32 -> b
forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b
f (Proxy Word32 -> b) -> Proxy Word32 -> b
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Word32
withWordType FFIWordSize
FFIWord64 forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b
f = Proxy Word64 -> b
forall a. (FFIArg a, FFIRet a, Integral a) => Proxy a -> b
f (Proxy Word64 -> b) -> Proxy Word64 -> b
forall a b. (a -> b) -> a -> b
$ forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Word64

-- | Given a 'FFIBasicRefType', call the callback with a marshalling function
-- that takes a Cryptol value and calls its callback with the 'Storable' type
-- corresponding to the 'FFIBasicRefType'.
getMarshalBasicRefArg :: FFIBasicRefType ->
  (forall rep.
      Storable rep =>
      (GenValue Concrete -> (rep -> IO val) -> IO val) ->
      result) ->
  result
getMarshalBasicRefArg :: forall val result.
FFIBasicRefType
-> (forall rep.
    Storable rep =>
    (GenValue Concrete -> (rep -> IO val) -> IO val) -> result)
-> result
getMarshalBasicRefArg (FFIInteger Maybe Type
_) forall rep.
Storable rep =>
(GenValue Concrete -> (rep -> IO val) -> IO val) -> result
f = (GenValue Concrete -> (MPZ -> IO val) -> IO val) -> result
forall rep.
Storable rep =>
(GenValue Concrete -> (rep -> IO val) -> IO val) -> result
f \GenValue Concrete
val MPZ -> IO val
g ->
  Integer -> (MPZ -> IO val) -> IO val
forall r. Integer -> (MPZ -> IO r) -> IO r
withInInteger' (GenValue Concrete -> SInteger Concrete
forall sym. Backend sym => GenValue sym -> SInteger sym
fromVInteger GenValue Concrete
val) MPZ -> IO val
g
getMarshalBasicRefArg FFIBasicRefType
FFIRational forall rep.
Storable rep =>
(GenValue Concrete -> (rep -> IO val) -> IO val) -> result
f = (GenValue Concrete -> (MPQ -> IO val) -> IO val) -> result
forall rep.
Storable rep =>
(GenValue Concrete -> (rep -> IO val) -> IO val) -> result
f \GenValue Concrete
val MPQ -> IO val
g -> do
  let SRational {SInteger Concrete
sNum :: SInteger Concrete
sDenom :: SInteger Concrete
sNum :: forall sym. SRational sym -> SInteger sym
sDenom :: forall sym. SRational sym -> SInteger sym
..} = GenValue Concrete -> SRational Concrete
forall sym. Backend sym => GenValue sym -> SRational sym
fromVRational GenValue Concrete
val
  Rational -> (MPQ -> IO val) -> IO val
forall r. Rational -> (MPQ -> IO r) -> IO r
withInRational' (Integer
sNum Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
sDenom) MPQ -> IO val
g

#else

-- | Dummy implementation for when FFI is disabled. Does not add anything to
-- the environment or report any errors.
evalForeignDecls :: ForeignSrc -> [(Name, FFIFunType)] -> EvalEnv ->
  Eval ([FFILoadError], EvalEnv)
evalForeignDecls _ _ env = pure ([], env)

#endif