mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-22 03:19:57 +03:00
Merge branch 'master' into conditional-constraints
This commit is contained in:
Henry Blanchette
commit
57cb59a845
4
.github/workflows/ci.yml
vendored
4
.github/workflows/ci.yml
vendored
@ -299,7 +299,9 @@ jobs:
|
||||
name: test-lib ${{ matrix.target }}
|
||||
run: |
|
||||
export PATH=$PWD/bin:$PWD/dist/bin:$PATH
|
||||
./bin/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol ./tests/${{ matrix.target }}
|
||||
if ${{ matrix.target != 'ffi' }} || dist/bin/cryptol -v | grep -q 'FFI enabled'; then
|
||||
./bin/test-runner --ext=.icry -F -b --exe=dist/bin/cryptol ./tests/${{ matrix.target }}
|
||||
fi
|
||||
|
||||
- if: matrix.suite == 'rpc'
|
||||
shell: bash
|
||||
|
||||
14
cry
14
cry
@ -79,11 +79,21 @@ case $COMMAND in
|
||||
test)
|
||||
echo Running tests
|
||||
setup_external_tools
|
||||
if [ "$#" == "0" ]; then TESTS=tests; else TESTS=$*; fi
|
||||
if [ "$#" == "0" ]; then
|
||||
if cabal v2-exec cryptol -- -v | grep -q 'FFI enabled'; then
|
||||
TESTS=(tests/*)
|
||||
else
|
||||
GLOBIGNORE="tests/ffi"
|
||||
TESTS=(tests/*)
|
||||
unset GLOBIGNORE
|
||||
fi
|
||||
else
|
||||
TESTS=("$*")
|
||||
fi
|
||||
$BIN/test-runner --ext=.icry \
|
||||
--exe=cabal \
|
||||
-F v2-run -F -v0 -F exe:cryptol -F -- -F -b \
|
||||
$TESTS
|
||||
"${TESTS[@]}"
|
||||
;;
|
||||
|
||||
rpc-test)
|
||||
|
||||
@ -107,6 +107,10 @@ cryptolError modErr warns =
|
||||
NotAParameterizedModule x ->
|
||||
(20650, [ ("module", jsonPretty x)
|
||||
])
|
||||
FFILoadErrors x errs ->
|
||||
(20660, [ ("module", jsonPretty x)
|
||||
, ("errors", jsonList (map jsonPretty errs))
|
||||
])
|
||||
OtherFailure x ->
|
||||
(29999, [ ("error", jsonString x)
|
||||
])
|
||||
|
||||
@ -37,6 +37,10 @@ flag relocatable
|
||||
default: True
|
||||
description: Don't use the Cabal-provided data directory for looking up Cryptol libraries. This is useful when the data directory can't be known ahead of time, like for a relocatable distribution.
|
||||
|
||||
flag ffi
|
||||
default: True
|
||||
description: Enable the foreign function interface
|
||||
|
||||
library
|
||||
Default-language:
|
||||
Haskell2010
|
||||
@ -81,6 +85,11 @@ library
|
||||
else
|
||||
build-depends: integer-gmp >= 1.0 && < 1.1
|
||||
|
||||
if flag(ffi)
|
||||
build-depends: libffi >= 0.2,
|
||||
unix
|
||||
cpp-options: -DFFI_ENABLED
|
||||
|
||||
Build-tool-depends: alex:alex, happy:happy
|
||||
hs-source-dirs: src
|
||||
|
||||
@ -148,6 +157,9 @@ library
|
||||
Cryptol.TypeCheck.TypeMap,
|
||||
Cryptol.TypeCheck.TypeOf,
|
||||
Cryptol.TypeCheck.Sanity,
|
||||
Cryptol.TypeCheck.FFI,
|
||||
Cryptol.TypeCheck.FFI.Error,
|
||||
Cryptol.TypeCheck.FFI.FFIType,
|
||||
|
||||
Cryptol.TypeCheck.Solver.Types,
|
||||
Cryptol.TypeCheck.Solver.SMT,
|
||||
@ -170,6 +182,8 @@ library
|
||||
Cryptol.Backend,
|
||||
Cryptol.Backend.Arch,
|
||||
Cryptol.Backend.Concrete,
|
||||
Cryptol.Backend.FFI,
|
||||
Cryptol.Backend.FFI.Error,
|
||||
Cryptol.Backend.FloatHelpers,
|
||||
Cryptol.Backend.Monad,
|
||||
Cryptol.Backend.SeqMap,
|
||||
@ -180,6 +194,7 @@ library
|
||||
Cryptol.Eval,
|
||||
Cryptol.Eval.Concrete,
|
||||
Cryptol.Eval.Env,
|
||||
Cryptol.Eval.FFI,
|
||||
Cryptol.Eval.Generic,
|
||||
Cryptol.Eval.Prims,
|
||||
Cryptol.Eval.Reference,
|
||||
|
||||
@ -291,7 +291,7 @@ main = do
|
||||
|
||||
if Seq.null (rdReplout rd)
|
||||
then do let cryCmd = (P.shell (exe ++ " --interactive-batch " ++ inFile ++ " -e"))
|
||||
(cryEC, cryOut, _) <- P.readCreateProcessWithExitCode cryCmd ""
|
||||
(cryEC, cryOut, cryErr) <- P.readCreateProcessWithExitCode cryCmd ""
|
||||
|
||||
|
||||
Line lnReplinStart _ Seq.:<| _ <- return $ rdReplin rd
|
||||
@ -301,6 +301,7 @@ main = do
|
||||
putStrLn $ "REPL error (replin lines " ++
|
||||
show lnReplinStart ++ "-" ++ show lnReplinEnd ++ ")."
|
||||
putStr cryOut
|
||||
putStr cryErr
|
||||
exitFailure
|
||||
ExitSuccess -> do
|
||||
-- remove temporary input file
|
||||
|
||||
306
docs/RefMan/FFI.rst
Normal file
306
docs/RefMan/FFI.rst
Normal file
@ -0,0 +1,306 @@
|
||||
Foreign Function Interface
|
||||
==========================
|
||||
|
||||
The foreign function interface (FFI) allows Cryptol to call functions written in
|
||||
C (or other languages that use the C calling convention).
|
||||
|
||||
Platform support
|
||||
----------------
|
||||
|
||||
The FFI is currently **not supported on Windows**, and only works on Unix-like
|
||||
systems (macOS and Linux).
|
||||
|
||||
Basic usage
|
||||
-----------
|
||||
|
||||
Suppose we want to call the following C function:
|
||||
|
||||
.. code-block:: c
|
||||
|
||||
uint32_t add(uint32_t x, uint32_t y) {
|
||||
return x + y;
|
||||
}
|
||||
|
||||
In our Cryptol file, we write a ``foreign`` declaration with no body:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
foreign add : [32] -> [32] -> [32]
|
||||
|
||||
The C code must first be compiled into a dynamically loaded shared library. When
|
||||
Cryptol loads the module containing the ``foreign`` declaration, it will look
|
||||
for a shared library in the same directory as the Cryptol module, with the same
|
||||
name as the Cryptol file but with a different file extension. The exact
|
||||
extension it uses is platform-specific:
|
||||
|
||||
* On Linux, it looks for the extension ``.so``.
|
||||
* On macOS, it looks for the extension ``.dylib``.
|
||||
|
||||
For example, if you are on Linux and your ``foreign`` declaration is in
|
||||
``Foo.cry``, Cryptol will dynamically load ``Foo.so``. Then for each ``foreign``
|
||||
declaration it will look for a symbol with the same name in the shared library.
|
||||
So in this case the function we want to call must be bound to the symbol ``add``
|
||||
in the shared library.
|
||||
|
||||
Once the module is loaded, the foreign ``add`` function can be called like any
|
||||
other Cryptol function. Cryptol automatically converts between Cryptol ``[32]``
|
||||
values and C ``uint32_t`` values.
|
||||
|
||||
The whole process would look something like this:
|
||||
|
||||
.. code-block::
|
||||
|
||||
$ cc -fPIC -shared Example.c -o Example.so
|
||||
$ cryptol
|
||||
Loading module Cryptol
|
||||
Cryptol> :l Example.cry
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
Main> add 1 2
|
||||
0x00000003
|
||||
|
||||
Note: Since Cryptol currently only accesses the compiled binary and not the C
|
||||
source, it has no way of checking that the Cryptol function type you declare in
|
||||
your Cryptol code actually matches the type of the C function. **It is your
|
||||
responsibility to make sure the types match up**. If they do not then there may
|
||||
be undefined behavior.
|
||||
|
||||
Compiling C code
|
||||
----------------
|
||||
|
||||
Cryptol currently does not handle compilation of C code to shared libraries. For
|
||||
simple usages, you can do this manually with the following commands:
|
||||
|
||||
* Linux: ``cc -fPIC -shared Foo.c -o Foo.so``
|
||||
* macOS: ``cc -dynamiclib Foo.c -o Foo.dylib``
|
||||
|
||||
Converting between Cryptol and C types
|
||||
--------------------------------------
|
||||
|
||||
This section describes how a given Cryptol function signature maps to a C
|
||||
function prototype. The FFI only supports a limited set of Cryptol types which
|
||||
have a clear translation into C.
|
||||
|
||||
Overall structure
|
||||
~~~~~~~~~~~~~~~~~
|
||||
|
||||
Cryptol ``foreign`` bindings must be functions. These functions may have
|
||||
multiple (curried) arguments; they may also be polymorphic, with certain
|
||||
limitations. That is, the general structure of a ``foreign`` declaration would
|
||||
look something like this:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
foreign f : {a1, ..., ak} (c1, ..., cn) => T1 -> ... -> Tm -> Tr
|
||||
|
||||
Each type argument to the Cryptol function (``a1, ..., ak`` above) corresponds
|
||||
to a value argument to the C function. These arguments are passed first, in the
|
||||
order of the type variables declared in the Cryptol signature, before any
|
||||
Cryptol value arguments.
|
||||
|
||||
Each value argument to the Cryptol function (``T1, ..., Tm`` above) corresponds
|
||||
to a number of value arguments to the C function. That is, a Cryptol value
|
||||
argument could correspond to zero, one, or many C arguments. The C arguments for
|
||||
each Cryptol value argument are passed in the order of the Cryptol value
|
||||
arguments, after any C arguments corresponding to Cryptol type arguments.
|
||||
|
||||
The return value of the Cryptol function (``Tr`` above) is either obtained by
|
||||
directly returning from the C function or by passing *output arguments* to the C
|
||||
function, depending on the return type. Output arguments are pointers to memory
|
||||
which can be modified by the C function to store its output values. If output
|
||||
arguments are used, they are passed last, after the C arguments corresponding to
|
||||
Cryptol arguments.
|
||||
|
||||
The following tables list the C type(s) that each Cryptol type (or kind)
|
||||
corresponds to.
|
||||
|
||||
Type parameters
|
||||
~~~~~~~~~~~~~~~
|
||||
|
||||
============ ==========
|
||||
Cryptol kind C type
|
||||
============ ==========
|
||||
``#`` ``size_t``
|
||||
============ ==========
|
||||
|
||||
Only numeric type parameters are allowed in polymorphic ``foreign`` functions.
|
||||
Furthermore, each type parameter ``n`` must satisfy ``fin n``. This has to be
|
||||
explicitly declared in the Cryptol signature.
|
||||
|
||||
Note that if a polymorphic foreign function is called with a type argument that
|
||||
does not fit in a ``size_t``, there will be a runtime error. (While we could
|
||||
check this statically by requiring that all type variables in foreign functions
|
||||
satisfy ``< 2^^64`` instead of just ``fin``, in practice this would be too
|
||||
cumbersome.)
|
||||
|
||||
Bit
|
||||
~~~
|
||||
|
||||
============ ===========
|
||||
Cryptol type C type
|
||||
============ ===========
|
||||
``Bit`` ``uint8_t``
|
||||
============ ===========
|
||||
|
||||
When converting to C, ``True`` is converted to ``1`` and ``False`` to ``0``.
|
||||
When converting to Cryptol, any nonzero number is converted to ``True`` and
|
||||
``0`` is converted to ``False``.
|
||||
|
||||
Integral types
|
||||
~~~~~~~~~~~~~~
|
||||
|
||||
Let ``K : #`` be a Cryptol type. Note ``K`` must be an actual fixed numeric type
|
||||
and not a type variable.
|
||||
|
||||
================================== ============
|
||||
Cryptol type C type
|
||||
================================== ============
|
||||
``[K]Bit`` where ``0 <= K <= 8`` ``uint8_t``
|
||||
``[K]Bit`` where ``8 < K <= 16`` ``uint16_t``
|
||||
``[K]Bit`` where ``16 < K <= 32`` ``uint32_t``
|
||||
``[K]Bit`` where ``32 < K <= 64`` ``uint64_t``
|
||||
================================== ============
|
||||
|
||||
If the Cryptol type is smaller than the C type, then when converting to C the
|
||||
value is padded with zero bits, and when converting to Cryptol the extra bits
|
||||
are ignored. For instance, for the Cryptol type ``[4]``, the Cryptol value ``0xf
|
||||
: [4]`` is converted to the C value ``uint8_t`` ``0x0f``, and the C ``uint8_t``
|
||||
``0xaf`` is converted to the Cryptol value ``0xf : [4]``.
|
||||
|
||||
Note that words larger than 64 bits are not supported, since there is no
|
||||
standard C integral type for that. You can split it into a sequence of smaller
|
||||
words first in Cryptol, then use the FFI conversion for sequences of words to
|
||||
handle it in C as an array.
|
||||
|
||||
Floating point types
|
||||
~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
============ ==========
|
||||
Cryptol type C type
|
||||
============ ==========
|
||||
``Float32`` ``float``
|
||||
``Float64`` ``double``
|
||||
============ ==========
|
||||
|
||||
Note: the Cryptol ``Float`` types are defined in the built-in module ``Float``.
|
||||
Other sizes of floating points are not supported.
|
||||
|
||||
Sequences
|
||||
~~~~~~~~~
|
||||
|
||||
Let ``n : #`` be a Cryptol type, possibly containing type variables, that
|
||||
satisfies ``fin n``, and ``T`` be one of the above Cryptol *integral types* or
|
||||
*floating point types*. Let ``U`` be the C type that ``T`` corresponds to.
|
||||
|
||||
============ ===========
|
||||
Cryptol type C type
|
||||
============ ===========
|
||||
``[n]T`` ``U*``
|
||||
============ ===========
|
||||
|
||||
The C pointer points to an array of ``n`` elements of type ``U``. Note that,
|
||||
while the length of the array itself is not explicitly passed along with the
|
||||
pointer, any type arguments contained in the size are passed as C ``size_t``'s
|
||||
earlier, so the C code can always know the length of the array.
|
||||
|
||||
Tuples and records
|
||||
~~~~~~~~~~~~~~~~~~
|
||||
|
||||
Let ``T1, T2, ..., Tn`` be Cryptol types supported by the FFI (which may be any
|
||||
of the types mentioned above, or tuples and records themselves). Let
|
||||
``U1, U2, ..., Un`` be the C types that ``T1, T2, ..., Tn`` respectively
|
||||
correspond to. Let ``f1, f2, ..., fn`` be arbitrary field names.
|
||||
|
||||
================================= ===================
|
||||
Cryptol type C types
|
||||
================================= ===================
|
||||
``(T1, T2, ..., Tn)`` ``U1, U2, ..., Un``
|
||||
``{f1: T1, f2: T2, ..., fn: Tn}`` ``U1, U2, ..., Un``
|
||||
================================= ===================
|
||||
|
||||
In this case, each Cryptol tuple or record is flattened out; passing a tuple as
|
||||
an argument behaves the same as if you passed its components individually. This
|
||||
flattening is applied recursively for nested tuples and records. Note that this
|
||||
means empty tuples don't map to any C values at all.
|
||||
|
||||
Type synonyms
|
||||
~~~~~~~~~~~~~
|
||||
|
||||
All type synonyms are expanded before applying the above rules, so you can use
|
||||
type synonyms in ``foreign`` declarations to improve readability.
|
||||
|
||||
Return values
|
||||
~~~~~~~~~~~~~
|
||||
|
||||
If the Cryptol return type is ``Bit`` or one of the above *integral types* or
|
||||
*floating point types*, the value is returned directly from the C function. In
|
||||
that case, the return type of the C function will be the C type corresponding to
|
||||
the Cryptol type, and no extra arguments are added.
|
||||
|
||||
If the Cryptol return type is a sequence, tuple, or record, then the value is
|
||||
returned using output arguments, and the return type of the C function will be
|
||||
``void``. For tuples and records, each component is recursively returned as
|
||||
output arguments. When treated as an output argument, each C type ``U`` will be
|
||||
a pointer ``U*`` instead, except in the case of sequences, where the output and
|
||||
input versions are the same type, because it is already a pointer.
|
||||
|
||||
Quick reference
|
||||
~~~~~~~~~~~~~~~
|
||||
|
||||
================================== =================== ============= =========================
|
||||
Cryptol type (or kind) C argument type(s) C return type C output argument type(s)
|
||||
================================== =================== ============= =========================
|
||||
``#`` ``size_t`` N/A N/A
|
||||
``Bit`` ``uint8_t`` ``uint8_t`` ``uint8_t*``
|
||||
``[K]Bit`` where ``0 <= K <= 8`` ``uint8_t`` ``uint8_t`` ``uint8_t*``
|
||||
``[K]Bit`` where ``8 < K <= 16`` ``uint16_t`` ``uint16_t`` ``uint16_t*``
|
||||
``[K]Bit`` where ``16 < K <= 32`` ``uint32_t`` ``uint32_t`` ``uint32_t*``
|
||||
``[K]Bit`` where ``32 < K <= 64`` ``uint64_t`` ``uint64_t`` ``uint64_t*``
|
||||
``Float32`` ``float`` ``float`` ``float*``
|
||||
``Float64`` ``double`` ``double`` ``double*``
|
||||
``[n]T`` ``U*`` N/A ``U*``
|
||||
``(T1, T2, ..., Tn)`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn``
|
||||
``{f1: T1, f2: T2, ..., fn: Tn}`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn``
|
||||
================================== =================== ============= =========================
|
||||
|
||||
where ``K`` is a constant number, ``n`` is a variable number, ``Ti`` is a type,
|
||||
``Ui`` is its C argument type, and ``Vi`` is its C output argument type.
|
||||
|
||||
Memory
|
||||
------
|
||||
|
||||
When pointers are involved, namely in the cases of sequences and output
|
||||
arguments, they point to memory. This memory is always allocated and deallocated
|
||||
by Cryptol; the C code does not need to manage this memory.
|
||||
|
||||
In the case of sequences, the pointer will point to an array. In the case of an
|
||||
output argument for a non-sequence type, the pointer will point to a piece of
|
||||
memory large enough to hold the given C type, and you should not try to access
|
||||
any adjacent memory.
|
||||
|
||||
For input sequence arguments, the array will already be set to the values
|
||||
corresponding to the Cryptol values in the sequence. For output arguments, the
|
||||
memory may be uninitialized when passed to C, and the C code should not read
|
||||
from it. It must write to the memory the value it is returning.
|
||||
|
||||
Evaluation
|
||||
----------
|
||||
|
||||
All Cryptol arguments are fully evaluated when a foreign function is called.
|
||||
|
||||
Example
|
||||
-------
|
||||
|
||||
The Cryptol signature
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
foreign f : {n} (fin n) => [n][10] -> {a : Bit, b : [64]}
|
||||
-> (Float64, [n + 1][20])
|
||||
|
||||
corresponds to the C signature
|
||||
|
||||
.. code-block:: c
|
||||
|
||||
void f(size_t n, uint16_t *in0, uint8_t in1, uint64_t in2,
|
||||
double *out0, uint32_t *out1);
|
||||
@ -12,4 +12,5 @@ Cryptol Reference Manual
|
||||
OverloadedOperations
|
||||
TypeDeclarations
|
||||
Modules
|
||||
FFI
|
||||
|
||||
|
||||
Binary file not shown.
Binary file not shown.
Binary file not shown.
BIN
docs/RefMan/_build/doctrees/FFI.doctree
Normal file
BIN
docs/RefMan/_build/doctrees/FFI.doctree
Normal file
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
@ -43,7 +43,6 @@
|
||||
<li class="toctree-l1 current"><a class="current reference internal" href="#">Basic Syntax</a><ul>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#declarations">Declarations</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#type-signatures">Type Signatures</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#numeric-constraint-guards">Numeric Constraint Guards</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#layout">Layout</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#comments">Comments</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#identifiers">Identifiers</a></li>
|
||||
@ -57,6 +56,7 @@
|
||||
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="FFI.html">Foreign Function Interface</a></li>
|
||||
</ul>
|
||||
|
||||
</div>
|
||||
@ -97,40 +97,6 @@
|
||||
</pre></div>
|
||||
</div>
|
||||
</section>
|
||||
<section id="numeric-constraint-guards">
|
||||
<h2>Numeric Constraint Guards<a class="headerlink" href="#numeric-constraint-guards" title="Permalink to this heading"></a></h2>
|
||||
<p>A declaration with a signature can use numeric constraint guards, which are like
|
||||
normal guards (such as in a multi-branch <cite>if`</cite> expression) except that the
|
||||
guarding conditions can be numeric constraints. For example:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">len</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">n</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">fin</span><span class="w"> </span><span class="n">n</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="p">[</span><span class="n">n</span><span class="p">]</span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kt">Integer</span><span class="w"></span>
|
||||
<span class="nf">len</span><span class="w"> </span><span class="n">xs</span><span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="mi">0</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">></span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">len</span><span class="w"> </span><span class="p">(</span><span class="n">drop</span><span class="w"> </span><span class="p">`{</span><span class="mi">1</span><span class="p">}</span><span class="w"> </span><span class="n">xs</span><span class="p">)</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>Note that this is importantly different from</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">len'</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">n</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">fin</span><span class="w"> </span><span class="n">n</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="p">[</span><span class="n">n</span><span class="p">]</span><span class="n">a</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kt">Integer</span><span class="w"></span>
|
||||
<span class="nf">len'</span><span class="w"> </span><span class="n">xs</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="kr">if</span><span class="w"> </span><span class="p">`</span><span class="n">n</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="mi">0</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="p">`</span><span class="n">n</span><span class="w"> </span><span class="o">></span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">len</span><span class="w"> </span><span class="p">(</span><span class="n">drop</span><span class="w"> </span><span class="p">`{</span><span class="mi">1</span><span class="p">}</span><span class="w"> </span><span class="n">xs</span><span class="p">)</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>In <cite>len’</cite>, the type-checker cannot determine that <cite>n >= 1</cite> which is
|
||||
required to use the</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">drop</span><span class="w"> </span><span class="p">`{</span><span class="mi">1</span><span class="p">}</span><span class="w"> </span><span class="n">xs</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>since the <cite>if</cite>’s condition is only on values, not types.</p>
|
||||
<p>However, in <cite>len</cite>, the type-checker locally-assumes the constraint <cite>n > 0</cite> in
|
||||
that constraint-guarded branch and so it can in fact determine that <cite>n >= 1</cite>.</p>
|
||||
<dl class="simple">
|
||||
<dt>Requirements:</dt><dd><ul class="simple">
|
||||
<li><p>Numeric constraint guards only support constraints over numeric literals,
|
||||
such as <cite>fin</cite>, <cite><=</cite>, <cite>==</cite>, etc. Type constraint aliases can also be used as
|
||||
long as they only constraint numeric literals.</p></li>
|
||||
<li><p>The numeric constraint guards of a declaration must be exhaustive.</p></li>
|
||||
</ul>
|
||||
</dd>
|
||||
</dl>
|
||||
</section>
|
||||
<section id="layout">
|
||||
<h2>Layout<a class="headerlink" href="#layout" title="Permalink to this heading"></a></h2>
|
||||
<p>Groups of declarations are organized based on indentation.
|
||||
|
||||
@ -55,6 +55,7 @@
|
||||
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="FFI.html">Foreign Function Interface</a></li>
|
||||
</ul>
|
||||
|
||||
</div>
|
||||
|
||||
@ -57,6 +57,7 @@
|
||||
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="FFI.html">Foreign Function Interface</a></li>
|
||||
</ul>
|
||||
|
||||
</div>
|
||||
|
||||
519
docs/RefMan/_build/html/FFI.html
Normal file
519
docs/RefMan/_build/html/FFI.html
Normal file
@ -0,0 +1,519 @@
|
||||
<!DOCTYPE html>
|
||||
<html class="writer-html5" lang="en" >
|
||||
<head>
|
||||
<meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />
|
||||
|
||||
<meta name="viewport" content="width=device-width, initial-scale=1.0" />
|
||||
<title>Foreign Function Interface — Cryptol 2.11.0 documentation</title>
|
||||
<link rel="stylesheet" href="_static/pygments.css" type="text/css" />
|
||||
<link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
|
||||
<!--[if lt IE 9]>
|
||||
<script src="_static/js/html5shiv.min.js"></script>
|
||||
<![endif]-->
|
||||
|
||||
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
|
||||
<script src="_static/jquery.js"></script>
|
||||
<script src="_static/underscore.js"></script>
|
||||
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
|
||||
<script src="_static/doctools.js"></script>
|
||||
<script src="_static/js/theme.js"></script>
|
||||
<link rel="index" title="Index" href="genindex.html" />
|
||||
<link rel="search" title="Search" href="search.html" />
|
||||
<link rel="prev" title="Modules" href="Modules.html" />
|
||||
</head>
|
||||
|
||||
<body class="wy-body-for-nav">
|
||||
<div class="wy-grid-for-nav">
|
||||
<nav data-toggle="wy-nav-shift" class="wy-nav-side">
|
||||
<div class="wy-side-scroll">
|
||||
<div class="wy-side-nav-search" >
|
||||
<a href="RefMan.html" class="icon icon-home"> Cryptol
|
||||
</a>
|
||||
<div role="search">
|
||||
<form id="rtd-search-form" class="wy-form" action="search.html" method="get">
|
||||
<input type="text" name="q" placeholder="Search docs" />
|
||||
<input type="hidden" name="check_keywords" value="yes" />
|
||||
<input type="hidden" name="area" value="default" />
|
||||
</form>
|
||||
</div>
|
||||
</div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
|
||||
<p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
|
||||
<ul class="current">
|
||||
<li class="toctree-l1"><a class="reference internal" href="BasicSyntax.html">Basic Syntax</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="Expressions.html">Expressions</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="BasicTypes.html">Basic Types</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
|
||||
<li class="toctree-l1 current"><a class="current reference internal" href="#">Foreign Function Interface</a><ul>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#platform-support">Platform support</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#basic-usage">Basic usage</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#compiling-c-code">Compiling C code</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#converting-between-cryptol-and-c-types">Converting between Cryptol and C types</a><ul>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#overall-structure">Overall structure</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#type-parameters">Type parameters</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#bit">Bit</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#integral-types">Integral types</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#floating-point-types">Floating point types</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#sequences">Sequences</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#tuples-and-records">Tuples and records</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#type-synonyms">Type synonyms</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#return-values">Return values</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="#quick-reference">Quick reference</a></li>
|
||||
</ul>
|
||||
</li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#memory">Memory</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#evaluation">Evaluation</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="#example">Example</a></li>
|
||||
</ul>
|
||||
</li>
|
||||
</ul>
|
||||
|
||||
</div>
|
||||
</div>
|
||||
</nav>
|
||||
|
||||
<section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
|
||||
<i data-toggle="wy-nav-top" class="fa fa-bars"></i>
|
||||
<a href="RefMan.html">Cryptol</a>
|
||||
</nav>
|
||||
|
||||
<div class="wy-nav-content">
|
||||
<div class="rst-content">
|
||||
<div role="navigation" aria-label="Page navigation">
|
||||
<ul class="wy-breadcrumbs">
|
||||
<li><a href="RefMan.html" class="icon icon-home"></a> »</li>
|
||||
<li>Foreign Function Interface</li>
|
||||
<li class="wy-breadcrumbs-aside">
|
||||
<a href="_sources/FFI.rst.txt" rel="nofollow"> View page source</a>
|
||||
</li>
|
||||
</ul>
|
||||
<hr/>
|
||||
</div>
|
||||
<div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
|
||||
<div itemprop="articleBody">
|
||||
|
||||
<section id="foreign-function-interface">
|
||||
<h1>Foreign Function Interface<a class="headerlink" href="#foreign-function-interface" title="Permalink to this heading"></a></h1>
|
||||
<p>The foreign function interface (FFI) allows Cryptol to call functions written in
|
||||
C (or other languages that use the C calling convention).</p>
|
||||
<section id="platform-support">
|
||||
<h2>Platform support<a class="headerlink" href="#platform-support" title="Permalink to this heading"></a></h2>
|
||||
<p>The FFI is currently <strong>not supported on Windows</strong>, and only works on Unix-like
|
||||
systems (macOS and Linux).</p>
|
||||
</section>
|
||||
<section id="basic-usage">
|
||||
<h2>Basic usage<a class="headerlink" href="#basic-usage" title="Permalink to this heading"></a></h2>
|
||||
<p>Suppose we want to call the following C function:</p>
|
||||
<div class="highlight-c notranslate"><div class="highlight"><pre><span></span><span class="kt">uint32_t</span><span class="w"> </span><span class="nf">add</span><span class="p">(</span><span class="kt">uint32_t</span><span class="w"> </span><span class="n">x</span><span class="p">,</span><span class="w"> </span><span class="kt">uint32_t</span><span class="w"> </span><span class="n">y</span><span class="p">)</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="k">return</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">y</span><span class="p">;</span><span class="w"></span>
|
||||
<span class="p">}</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>In our Cryptol file, we write a <code class="docutils literal notranslate"><span class="pre">foreign</span></code> declaration with no body:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">foreign</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">[</span><span class="mi">32</span><span class="p">]</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="p">[</span><span class="mi">32</span><span class="p">]</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="p">[</span><span class="mi">32</span><span class="p">]</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>The C code must first be compiled into a dynamically loaded shared library. When
|
||||
Cryptol loads the module containing the <code class="docutils literal notranslate"><span class="pre">foreign</span></code> declaration, it will look
|
||||
for a shared library in the same directory as the Cryptol module, with the same
|
||||
name as the Cryptol file but with a different file extension. The exact
|
||||
extension it uses is platform-specific:</p>
|
||||
<ul class="simple">
|
||||
<li><p>On Linux, it looks for the extension <code class="docutils literal notranslate"><span class="pre">.so</span></code>.</p></li>
|
||||
<li><p>On macOS, it looks for the extension <code class="docutils literal notranslate"><span class="pre">.dylib</span></code>.</p></li>
|
||||
</ul>
|
||||
<p>For example, if you are on Linux and your <code class="docutils literal notranslate"><span class="pre">foreign</span></code> declaration is in
|
||||
<code class="docutils literal notranslate"><span class="pre">Foo.cry</span></code>, Cryptol will dynamically load <code class="docutils literal notranslate"><span class="pre">Foo.so</span></code>. Then for each <code class="docutils literal notranslate"><span class="pre">foreign</span></code>
|
||||
declaration it will look for a symbol with the same name in the shared library.
|
||||
So in this case the function we want to call must be bound to the symbol <code class="docutils literal notranslate"><span class="pre">add</span></code>
|
||||
in the shared library.</p>
|
||||
<p>Once the module is loaded, the foreign <code class="docutils literal notranslate"><span class="pre">add</span></code> function can be called like any
|
||||
other Cryptol function. Cryptol automatically converts between Cryptol <code class="docutils literal notranslate"><span class="pre">[32]</span></code>
|
||||
values and C <code class="docutils literal notranslate"><span class="pre">uint32_t</span></code> values.</p>
|
||||
<p>The whole process would look something like this:</p>
|
||||
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span>$ cc -fPIC -shared Example.c -o Example.so
|
||||
$ cryptol
|
||||
Loading module Cryptol
|
||||
Cryptol> :l Example.cry
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
Main> add 1 2
|
||||
0x00000003
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>Note: Since Cryptol currently only accesses the compiled binary and not the C
|
||||
source, it has no way of checking that the Cryptol function type you declare in
|
||||
your Cryptol code actually matches the type of the C function. <strong>It is your
|
||||
responsibility to make sure the types match up</strong>. If they do not then there may
|
||||
be undefined behavior.</p>
|
||||
</section>
|
||||
<section id="compiling-c-code">
|
||||
<h2>Compiling C code<a class="headerlink" href="#compiling-c-code" title="Permalink to this heading"></a></h2>
|
||||
<p>Cryptol currently does not handle compilation of C code to shared libraries. For
|
||||
simple usages, you can do this manually with the following commands:</p>
|
||||
<ul class="simple">
|
||||
<li><p>Linux: <code class="docutils literal notranslate"><span class="pre">cc</span> <span class="pre">-fPIC</span> <span class="pre">-shared</span> <span class="pre">Foo.c</span> <span class="pre">-o</span> <span class="pre">Foo.so</span></code></p></li>
|
||||
<li><p>macOS: <code class="docutils literal notranslate"><span class="pre">cc</span> <span class="pre">-dynamiclib</span> <span class="pre">Foo.c</span> <span class="pre">-o</span> <span class="pre">Foo.dylib</span></code></p></li>
|
||||
</ul>
|
||||
</section>
|
||||
<section id="converting-between-cryptol-and-c-types">
|
||||
<h2>Converting between Cryptol and C types<a class="headerlink" href="#converting-between-cryptol-and-c-types" title="Permalink to this heading"></a></h2>
|
||||
<p>This section describes how a given Cryptol function signature maps to a C
|
||||
function prototype. The FFI only supports a limited set of Cryptol types which
|
||||
have a clear translation into C.</p>
|
||||
<section id="overall-structure">
|
||||
<h3>Overall structure<a class="headerlink" href="#overall-structure" title="Permalink to this heading"></a></h3>
|
||||
<p>Cryptol <code class="docutils literal notranslate"><span class="pre">foreign</span></code> bindings must be functions. These functions may have
|
||||
multiple (curried) arguments; they may also be polymorphic, with certain
|
||||
limitations. That is, the general structure of a <code class="docutils literal notranslate"><span class="pre">foreign</span></code> declaration would
|
||||
look something like this:</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">foreign</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a1</span><span class="p">,</span><span class="w"> </span><span class="o">...</span><span class="p">,</span><span class="w"> </span><span class="n">ak</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="n">c1</span><span class="p">,</span><span class="w"> </span><span class="o">...</span><span class="p">,</span><span class="w"> </span><span class="n">cn</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="kt">T1</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="o">...</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kt">Tm</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="kt">Tr</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>Each type argument to the Cryptol function (<code class="docutils literal notranslate"><span class="pre">a1,</span> <span class="pre">...,</span> <span class="pre">ak</span></code> above) corresponds
|
||||
to a value argument to the C function. These arguments are passed first, in the
|
||||
order of the type variables declared in the Cryptol signature, before any
|
||||
Cryptol value arguments.</p>
|
||||
<p>Each value argument to the Cryptol function (<code class="docutils literal notranslate"><span class="pre">T1,</span> <span class="pre">...,</span> <span class="pre">Tm</span></code> above) corresponds
|
||||
to a number of value arguments to the C function. That is, a Cryptol value
|
||||
argument could correspond to zero, one, or many C arguments. The C arguments for
|
||||
each Cryptol value argument are passed in the order of the Cryptol value
|
||||
arguments, after any C arguments corresponding to Cryptol type arguments.</p>
|
||||
<p>The return value of the Cryptol function (<code class="docutils literal notranslate"><span class="pre">Tr</span></code> above) is either obtained by
|
||||
directly returning from the C function or by passing <em>output arguments</em> to the C
|
||||
function, depending on the return type. Output arguments are pointers to memory
|
||||
which can be modified by the C function to store its output values. If output
|
||||
arguments are used, they are passed last, after the C arguments corresponding to
|
||||
Cryptol arguments.</p>
|
||||
<p>The following tables list the C type(s) that each Cryptol type (or kind)
|
||||
corresponds to.</p>
|
||||
</section>
|
||||
<section id="type-parameters">
|
||||
<h3>Type parameters<a class="headerlink" href="#type-parameters" title="Permalink to this heading"></a></h3>
|
||||
<table class="docutils align-default">
|
||||
<colgroup>
|
||||
<col style="width: 55%" />
|
||||
<col style="width: 45%" />
|
||||
</colgroup>
|
||||
<thead>
|
||||
<tr class="row-odd"><th class="head"><p>Cryptol kind</p></th>
|
||||
<th class="head"><p>C type</p></th>
|
||||
</tr>
|
||||
</thead>
|
||||
<tbody>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">#</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">size_t</span></code></p></td>
|
||||
</tr>
|
||||
</tbody>
|
||||
</table>
|
||||
<p>Only numeric type parameters are allowed in polymorphic <code class="docutils literal notranslate"><span class="pre">foreign</span></code> functions.
|
||||
Furthermore, each type parameter <code class="docutils literal notranslate"><span class="pre">n</span></code> must satisfy <code class="docutils literal notranslate"><span class="pre">fin</span> <span class="pre">n</span></code>. This has to be
|
||||
explicitly declared in the Cryptol signature.</p>
|
||||
<p>Note that if a polymorphic foreign function is called with a type argument that
|
||||
does not fit in a <code class="docutils literal notranslate"><span class="pre">size_t</span></code>, there will be a runtime error. (While we could
|
||||
check this statically by requiring that all type variables in foreign functions
|
||||
satisfy <code class="docutils literal notranslate"><span class="pre"><</span> <span class="pre">2^^64</span></code> instead of just <code class="docutils literal notranslate"><span class="pre">fin</span></code>, in practice this would be too
|
||||
cumbersome.)</p>
|
||||
</section>
|
||||
<section id="bit">
|
||||
<h3>Bit<a class="headerlink" href="#bit" title="Permalink to this heading"></a></h3>
|
||||
<table class="docutils align-default">
|
||||
<colgroup>
|
||||
<col style="width: 52%" />
|
||||
<col style="width: 48%" />
|
||||
</colgroup>
|
||||
<thead>
|
||||
<tr class="row-odd"><th class="head"><p>Cryptol type</p></th>
|
||||
<th class="head"><p>C type</p></th>
|
||||
</tr>
|
||||
</thead>
|
||||
<tbody>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">Bit</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint8_t</span></code></p></td>
|
||||
</tr>
|
||||
</tbody>
|
||||
</table>
|
||||
<p>When converting to C, <code class="docutils literal notranslate"><span class="pre">True</span></code> is converted to <code class="docutils literal notranslate"><span class="pre">1</span></code> and <code class="docutils literal notranslate"><span class="pre">False</span></code> to <code class="docutils literal notranslate"><span class="pre">0</span></code>.
|
||||
When converting to Cryptol, any nonzero number is converted to <code class="docutils literal notranslate"><span class="pre">True</span></code> and
|
||||
<code class="docutils literal notranslate"><span class="pre">0</span></code> is converted to <code class="docutils literal notranslate"><span class="pre">False</span></code>.</p>
|
||||
</section>
|
||||
<section id="integral-types">
|
||||
<h3>Integral types<a class="headerlink" href="#integral-types" title="Permalink to this heading"></a></h3>
|
||||
<p>Let <code class="docutils literal notranslate"><span class="pre">K</span> <span class="pre">:</span> <span class="pre">#</span></code> be a Cryptol type. Note <code class="docutils literal notranslate"><span class="pre">K</span></code> must be an actual fixed numeric type
|
||||
and not a type variable.</p>
|
||||
<table class="docutils align-default">
|
||||
<colgroup>
|
||||
<col style="width: 74%" />
|
||||
<col style="width: 26%" />
|
||||
</colgroup>
|
||||
<thead>
|
||||
<tr class="row-odd"><th class="head"><p>Cryptol type</p></th>
|
||||
<th class="head"><p>C type</p></th>
|
||||
</tr>
|
||||
</thead>
|
||||
<tbody>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[K]Bit</span></code> where <code class="docutils literal notranslate"><span class="pre">0</span>  <span class="pre"><=</span> <span class="pre">K</span> <span class="pre"><=</span> <span class="pre">8</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint8_t</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">[K]Bit</span></code> where <code class="docutils literal notranslate"><span class="pre">8</span>  <span class="pre"><</span>  <span class="pre">K</span> <span class="pre"><=</span> <span class="pre">16</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint16_t</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[K]Bit</span></code> where <code class="docutils literal notranslate"><span class="pre">16</span> <span class="pre"><</span>  <span class="pre">K</span> <span class="pre"><=</span> <span class="pre">32</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint32_t</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">[K]Bit</span></code> where <code class="docutils literal notranslate"><span class="pre">32</span> <span class="pre"><</span>  <span class="pre">K</span> <span class="pre"><=</span> <span class="pre">64</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint64_t</span></code></p></td>
|
||||
</tr>
|
||||
</tbody>
|
||||
</table>
|
||||
<p>If the Cryptol type is smaller than the C type, then when converting to C the
|
||||
value is padded with zero bits, and when converting to Cryptol the extra bits
|
||||
are ignored. For instance, for the Cryptol type <code class="docutils literal notranslate"><span class="pre">[4]</span></code>, the Cryptol value <code class="docutils literal notranslate"><span class="pre">0xf</span>
|
||||
<span class="pre">:</span> <span class="pre">[4]</span></code> is converted to the C value <code class="docutils literal notranslate"><span class="pre">uint8_t</span></code> <code class="docutils literal notranslate"><span class="pre">0x0f</span></code>, and the C <code class="docutils literal notranslate"><span class="pre">uint8_t</span></code>
|
||||
<code class="docutils literal notranslate"><span class="pre">0xaf</span></code> is converted to the Cryptol value <code class="docutils literal notranslate"><span class="pre">0xf</span> <span class="pre">:</span> <span class="pre">[4]</span></code>.</p>
|
||||
<p>Note that words larger than 64 bits are not supported, since there is no
|
||||
standard C integral type for that. You can split it into a sequence of smaller
|
||||
words first in Cryptol, then use the FFI conversion for sequences of words to
|
||||
handle it in C as an array.</p>
|
||||
</section>
|
||||
<section id="floating-point-types">
|
||||
<h3>Floating point types<a class="headerlink" href="#floating-point-types" title="Permalink to this heading"></a></h3>
|
||||
<table class="docutils align-default">
|
||||
<colgroup>
|
||||
<col style="width: 55%" />
|
||||
<col style="width: 45%" />
|
||||
</colgroup>
|
||||
<thead>
|
||||
<tr class="row-odd"><th class="head"><p>Cryptol type</p></th>
|
||||
<th class="head"><p>C type</p></th>
|
||||
</tr>
|
||||
</thead>
|
||||
<tbody>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">Float32</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">float</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">Float64</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">double</span></code></p></td>
|
||||
</tr>
|
||||
</tbody>
|
||||
</table>
|
||||
<p>Note: the Cryptol <code class="docutils literal notranslate"><span class="pre">Float</span></code> types are defined in the built-in module <code class="docutils literal notranslate"><span class="pre">Float</span></code>.
|
||||
Other sizes of floating points are not supported.</p>
|
||||
</section>
|
||||
<section id="sequences">
|
||||
<h3>Sequences<a class="headerlink" href="#sequences" title="Permalink to this heading"></a></h3>
|
||||
<p>Let <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">:</span> <span class="pre">#</span></code> be a Cryptol type, possibly containing type variables, that
|
||||
satisfies <code class="docutils literal notranslate"><span class="pre">fin</span> <span class="pre">n</span></code>, and <code class="docutils literal notranslate"><span class="pre">T</span></code> be one of the above Cryptol <em>integral types</em> or
|
||||
<em>floating point types</em>. Let <code class="docutils literal notranslate"><span class="pre">U</span></code> be the C type that <code class="docutils literal notranslate"><span class="pre">T</span></code> corresponds to.</p>
|
||||
<table class="docutils align-default">
|
||||
<colgroup>
|
||||
<col style="width: 52%" />
|
||||
<col style="width: 48%" />
|
||||
</colgroup>
|
||||
<thead>
|
||||
<tr class="row-odd"><th class="head"><p>Cryptol type</p></th>
|
||||
<th class="head"><p>C type</p></th>
|
||||
</tr>
|
||||
</thead>
|
||||
<tbody>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[n]T</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">U*</span></code></p></td>
|
||||
</tr>
|
||||
</tbody>
|
||||
</table>
|
||||
<p>The C pointer points to an array of <code class="docutils literal notranslate"><span class="pre">n</span></code> elements of type <code class="docutils literal notranslate"><span class="pre">U</span></code>. Note that,
|
||||
while the length of the array itself is not explicitly passed along with the
|
||||
pointer, any type arguments contained in the size are passed as C <code class="docutils literal notranslate"><span class="pre">size_t</span></code>’s
|
||||
earlier, so the C code can always know the length of the array.</p>
|
||||
</section>
|
||||
<section id="tuples-and-records">
|
||||
<h3>Tuples and records<a class="headerlink" href="#tuples-and-records" title="Permalink to this heading"></a></h3>
|
||||
<p>Let <code class="docutils literal notranslate"><span class="pre">T1,</span> <span class="pre">T2,</span> <span class="pre">...,</span> <span class="pre">Tn</span></code> be Cryptol types supported by the FFI (which may be any
|
||||
of the types mentioned above, or tuples and records themselves). Let
|
||||
<code class="docutils literal notranslate"><span class="pre">U1,</span> <span class="pre">U2,</span> <span class="pre">...,</span> <span class="pre">Un</span></code> be the C types that <code class="docutils literal notranslate"><span class="pre">T1,</span> <span class="pre">T2,</span> <span class="pre">...,</span> <span class="pre">Tn</span></code> respectively
|
||||
correspond to. Let <code class="docutils literal notranslate"><span class="pre">f1,</span> <span class="pre">f2,</span> <span class="pre">...,</span> <span class="pre">fn</span></code> be arbitrary field names.</p>
|
||||
<table class="docutils align-default">
|
||||
<colgroup>
|
||||
<col style="width: 63%" />
|
||||
<col style="width: 37%" />
|
||||
</colgroup>
|
||||
<thead>
|
||||
<tr class="row-odd"><th class="head"><p>Cryptol type</p></th>
|
||||
<th class="head"><p>C types</p></th>
|
||||
</tr>
|
||||
</thead>
|
||||
<tbody>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">(T1,</span> <span class="pre">T2,</span> <span class="pre">...,</span> <span class="pre">Tn)</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">U1,</span> <span class="pre">U2,</span> <span class="pre">...,</span> <span class="pre">Un</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">{f1:</span> <span class="pre">T1,</span> <span class="pre">f2:</span> <span class="pre">T2,</span> <span class="pre">...,</span> <span class="pre">fn:</span> <span class="pre">Tn}</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">U1,</span> <span class="pre">U2,</span> <span class="pre">...,</span> <span class="pre">Un</span></code></p></td>
|
||||
</tr>
|
||||
</tbody>
|
||||
</table>
|
||||
<p>In this case, each Cryptol tuple or record is flattened out; passing a tuple as
|
||||
an argument behaves the same as if you passed its components individually. This
|
||||
flattening is applied recursively for nested tuples and records. Note that this
|
||||
means empty tuples don’t map to any C values at all.</p>
|
||||
</section>
|
||||
<section id="type-synonyms">
|
||||
<h3>Type synonyms<a class="headerlink" href="#type-synonyms" title="Permalink to this heading"></a></h3>
|
||||
<p>All type synonyms are expanded before applying the above rules, so you can use
|
||||
type synonyms in <code class="docutils literal notranslate"><span class="pre">foreign</span></code> declarations to improve readability.</p>
|
||||
</section>
|
||||
<section id="return-values">
|
||||
<h3>Return values<a class="headerlink" href="#return-values" title="Permalink to this heading"></a></h3>
|
||||
<p>If the Cryptol return type is <code class="docutils literal notranslate"><span class="pre">Bit</span></code> or one of the above <em>integral types</em> or
|
||||
<em>floating point types</em>, the value is returned directly from the C function. In
|
||||
that case, the return type of the C function will be the C type corresponding to
|
||||
the Cryptol type, and no extra arguments are added.</p>
|
||||
<p>If the Cryptol return type is a sequence, tuple, or record, then the value is
|
||||
returned using output arguments, and the return type of the C function will be
|
||||
<code class="docutils literal notranslate"><span class="pre">void</span></code>. For tuples and records, each component is recursively returned as
|
||||
output arguments. When treated as an output argument, each C type <code class="docutils literal notranslate"><span class="pre">U</span></code> will be
|
||||
a pointer <code class="docutils literal notranslate"><span class="pre">U*</span></code> instead, except in the case of sequences, where the output and
|
||||
input versions are the same type, because it is already a pointer.</p>
|
||||
</section>
|
||||
<section id="quick-reference">
|
||||
<h3>Quick reference<a class="headerlink" href="#quick-reference" title="Permalink to this heading"></a></h3>
|
||||
<table class="docutils align-default">
|
||||
<colgroup>
|
||||
<col style="width: 37%" />
|
||||
<col style="width: 21%" />
|
||||
<col style="width: 14%" />
|
||||
<col style="width: 27%" />
|
||||
</colgroup>
|
||||
<thead>
|
||||
<tr class="row-odd"><th class="head"><p>Cryptol type (or kind)</p></th>
|
||||
<th class="head"><p>C argument type(s)</p></th>
|
||||
<th class="head"><p>C return type</p></th>
|
||||
<th class="head"><p>C output argument type(s)</p></th>
|
||||
</tr>
|
||||
</thead>
|
||||
<tbody>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">#</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">size_t</span></code></p></td>
|
||||
<td><p>N/A</p></td>
|
||||
<td><p>N/A</p></td>
|
||||
</tr>
|
||||
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">Bit</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint8_t</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint8_t</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint8_t*</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[K]Bit</span></code> where <code class="docutils literal notranslate"><span class="pre">0</span>  <span class="pre"><=</span> <span class="pre">K</span> <span class="pre"><=</span> <span class="pre">8</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint8_t</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint8_t</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint8_t*</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">[K]Bit</span></code> where <code class="docutils literal notranslate"><span class="pre">8</span>  <span class="pre"><</span>  <span class="pre">K</span> <span class="pre"><=</span> <span class="pre">16</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint16_t</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint16_t</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint16_t*</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[K]Bit</span></code> where <code class="docutils literal notranslate"><span class="pre">16</span> <span class="pre"><</span>  <span class="pre">K</span> <span class="pre"><=</span> <span class="pre">32</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint32_t</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint32_t</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint32_t*</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">[K]Bit</span></code> where <code class="docutils literal notranslate"><span class="pre">32</span> <span class="pre"><</span>  <span class="pre">K</span> <span class="pre"><=</span> <span class="pre">64</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint64_t</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint64_t</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">uint64_t*</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">Float32</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">float</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">float</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">float*</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">Float64</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">double</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">double</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">double*</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">[n]T</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">U*</span></code></p></td>
|
||||
<td><p>N/A</p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">U*</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-odd"><td><p><code class="docutils literal notranslate"><span class="pre">(T1,</span> <span class="pre">T2,</span> <span class="pre">...,</span> <span class="pre">Tn)</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">U1,</span> <span class="pre">U2,</span> <span class="pre">...,</span> <span class="pre">Un</span></code></p></td>
|
||||
<td><p>N/A</p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">V1,</span> <span class="pre">V2,</span> <span class="pre">...,</span> <span class="pre">Vn</span></code></p></td>
|
||||
</tr>
|
||||
<tr class="row-even"><td><p><code class="docutils literal notranslate"><span class="pre">{f1:</span> <span class="pre">T1,</span> <span class="pre">f2:</span> <span class="pre">T2,</span> <span class="pre">...,</span> <span class="pre">fn:</span> <span class="pre">Tn}</span></code></p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">U1,</span> <span class="pre">U2,</span> <span class="pre">...,</span> <span class="pre">Un</span></code></p></td>
|
||||
<td><p>N/A</p></td>
|
||||
<td><p><code class="docutils literal notranslate"><span class="pre">V1,</span> <span class="pre">V2,</span> <span class="pre">...,</span> <span class="pre">Vn</span></code></p></td>
|
||||
</tr>
|
||||
</tbody>
|
||||
</table>
|
||||
<p>where <code class="docutils literal notranslate"><span class="pre">K</span></code> is a constant number, <code class="docutils literal notranslate"><span class="pre">n</span></code> is a variable number, <code class="docutils literal notranslate"><span class="pre">Ti</span></code> is a type,
|
||||
<code class="docutils literal notranslate"><span class="pre">Ui</span></code> is its C argument type, and <code class="docutils literal notranslate"><span class="pre">Vi</span></code> is its C output argument type.</p>
|
||||
</section>
|
||||
</section>
|
||||
<section id="memory">
|
||||
<h2>Memory<a class="headerlink" href="#memory" title="Permalink to this heading"></a></h2>
|
||||
<p>When pointers are involved, namely in the cases of sequences and output
|
||||
arguments, they point to memory. This memory is always allocated and deallocated
|
||||
by Cryptol; the C code does not need to manage this memory.</p>
|
||||
<p>In the case of sequences, the pointer will point to an array. In the case of an
|
||||
output argument for a non-sequence type, the pointer will point to a piece of
|
||||
memory large enough to hold the given C type, and you should not try to access
|
||||
any adjacent memory.</p>
|
||||
<p>For input sequence arguments, the array will already be set to the values
|
||||
corresponding to the Cryptol values in the sequence. For output arguments, the
|
||||
memory may be uninitialized when passed to C, and the C code should not read
|
||||
from it. It must write to the memory the value it is returning.</p>
|
||||
</section>
|
||||
<section id="evaluation">
|
||||
<h2>Evaluation<a class="headerlink" href="#evaluation" title="Permalink to this heading"></a></h2>
|
||||
<p>All Cryptol arguments are fully evaluated when a foreign function is called.</p>
|
||||
</section>
|
||||
<section id="example">
|
||||
<h2>Example<a class="headerlink" href="#example" title="Permalink to this heading"></a></h2>
|
||||
<p>The Cryptol signature</p>
|
||||
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">foreign</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">n</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">fin</span><span class="w"> </span><span class="n">n</span><span class="p">)</span><span class="w"> </span><span class="ow">=></span><span class="w"> </span><span class="p">[</span><span class="n">n</span><span class="p">][</span><span class="mi">10</span><span class="p">]</span><span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kr">Bit</span><span class="p">,</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">[</span><span class="mi">64</span><span class="p">]}</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="ow">-></span><span class="w"> </span><span class="p">(</span><span class="kt">Float64</span><span class="p">,</span><span class="w"> </span><span class="p">[</span><span class="n">n</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="mi">1</span><span class="p">][</span><span class="mi">20</span><span class="p">])</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
<p>corresponds to the C signature</p>
|
||||
<div class="highlight-c notranslate"><div class="highlight"><pre><span></span><span class="kt">void</span><span class="w"> </span><span class="nf">f</span><span class="p">(</span><span class="kt">size_t</span><span class="w"> </span><span class="n">n</span><span class="p">,</span><span class="w"> </span><span class="kt">uint16_t</span><span class="w"> </span><span class="o">*</span><span class="n">in0</span><span class="p">,</span><span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="n">in1</span><span class="p">,</span><span class="w"> </span><span class="kt">uint64_t</span><span class="w"> </span><span class="n">in2</span><span class="p">,</span><span class="w"></span>
|
||||
<span class="w"> </span><span class="kt">double</span><span class="w"> </span><span class="o">*</span><span class="n">out0</span><span class="p">,</span><span class="w"> </span><span class="kt">uint32_t</span><span class="w"> </span><span class="o">*</span><span class="n">out1</span><span class="p">);</span><span class="w"></span>
|
||||
</pre></div>
|
||||
</div>
|
||||
</section>
|
||||
</section>
|
||||
|
||||
|
||||
</div>
|
||||
</div>
|
||||
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
|
||||
<a href="Modules.html" class="btn btn-neutral float-left" title="Modules" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
|
||||
</div>
|
||||
|
||||
<hr/>
|
||||
|
||||
<div role="contentinfo">
|
||||
<p>© Copyright 2021, The Cryptol Team.</p>
|
||||
</div>
|
||||
|
||||
Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
|
||||
<a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
|
||||
provided by <a href="https://readthedocs.org">Read the Docs</a>.
|
||||
|
||||
|
||||
</footer>
|
||||
</div>
|
||||
</div>
|
||||
</section>
|
||||
</div>
|
||||
<script>
|
||||
jQuery(function () {
|
||||
SphinxRtdTheme.Navigation.enable(true);
|
||||
});
|
||||
</script>
|
||||
|
||||
</body>
|
||||
</html>
|
||||
@ -19,6 +19,7 @@
|
||||
<script src="_static/js/theme.js"></script>
|
||||
<link rel="index" title="Index" href="genindex.html" />
|
||||
<link rel="search" title="Search" href="search.html" />
|
||||
<link rel="next" title="Foreign Function Interface" href="FFI.html" />
|
||||
<link rel="prev" title="Type Declarations" href="TypeDeclarations.html" />
|
||||
</head>
|
||||
|
||||
@ -71,6 +72,7 @@
|
||||
</li>
|
||||
</ul>
|
||||
</li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="FFI.html">Foreign Function Interface</a></li>
|
||||
</ul>
|
||||
|
||||
</div>
|
||||
@ -766,6 +768,7 @@ in an instantiation. Here is an example:</p>
|
||||
</div>
|
||||
<footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
|
||||
<a href="TypeDeclarations.html" class="btn btn-neutral float-left" title="Type Declarations" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
|
||||
<a href="FFI.html" class="btn btn-neutral float-right" title="Foreign Function Interface" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
|
||||
</div>
|
||||
|
||||
<hr/>
|
||||
|
||||
@ -57,6 +57,7 @@
|
||||
</li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="FFI.html">Foreign Function Interface</a></li>
|
||||
</ul>
|
||||
|
||||
</div>
|
||||
|
||||
@ -45,6 +45,7 @@
|
||||
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="FFI.html">Foreign Function Interface</a></li>
|
||||
</ul>
|
||||
|
||||
</div>
|
||||
@ -154,6 +155,28 @@
|
||||
</li>
|
||||
</ul>
|
||||
</li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="FFI.html">Foreign Function Interface</a><ul>
|
||||
<li class="toctree-l2"><a class="reference internal" href="FFI.html#platform-support">Platform support</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="FFI.html#basic-usage">Basic usage</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="FFI.html#compiling-c-code">Compiling C code</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="FFI.html#converting-between-cryptol-and-c-types">Converting between Cryptol and C types</a><ul>
|
||||
<li class="toctree-l3"><a class="reference internal" href="FFI.html#overall-structure">Overall structure</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="FFI.html#type-parameters">Type parameters</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="FFI.html#bit">Bit</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="FFI.html#integral-types">Integral types</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="FFI.html#floating-point-types">Floating point types</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="FFI.html#sequences">Sequences</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="FFI.html#tuples-and-records">Tuples and records</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="FFI.html#type-synonyms">Type synonyms</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="FFI.html#return-values">Return values</a></li>
|
||||
<li class="toctree-l3"><a class="reference internal" href="FFI.html#quick-reference">Quick reference</a></li>
|
||||
</ul>
|
||||
</li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="FFI.html#memory">Memory</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="FFI.html#evaluation">Evaluation</a></li>
|
||||
<li class="toctree-l2"><a class="reference internal" href="FFI.html#example">Example</a></li>
|
||||
</ul>
|
||||
</li>
|
||||
</ul>
|
||||
</div>
|
||||
</section>
|
||||
|
||||
@ -50,6 +50,7 @@
|
||||
</ul>
|
||||
</li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="FFI.html">Foreign Function Interface</a></li>
|
||||
</ul>
|
||||
|
||||
</div>
|
||||
|
||||
306
docs/RefMan/_build/html/_sources/FFI.rst.txt
Normal file
306
docs/RefMan/_build/html/_sources/FFI.rst.txt
Normal file
@ -0,0 +1,306 @@
|
||||
Foreign Function Interface
|
||||
==========================
|
||||
|
||||
The foreign function interface (FFI) allows Cryptol to call functions written in
|
||||
C (or other languages that use the C calling convention).
|
||||
|
||||
Platform support
|
||||
----------------
|
||||
|
||||
The FFI is currently **not supported on Windows**, and only works on Unix-like
|
||||
systems (macOS and Linux).
|
||||
|
||||
Basic usage
|
||||
-----------
|
||||
|
||||
Suppose we want to call the following C function:
|
||||
|
||||
.. code-block:: c
|
||||
|
||||
uint32_t add(uint32_t x, uint32_t y) {
|
||||
return x + y;
|
||||
}
|
||||
|
||||
In our Cryptol file, we write a ``foreign`` declaration with no body:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
foreign add : [32] -> [32] -> [32]
|
||||
|
||||
The C code must first be compiled into a dynamically loaded shared library. When
|
||||
Cryptol loads the module containing the ``foreign`` declaration, it will look
|
||||
for a shared library in the same directory as the Cryptol module, with the same
|
||||
name as the Cryptol file but with a different file extension. The exact
|
||||
extension it uses is platform-specific:
|
||||
|
||||
* On Linux, it looks for the extension ``.so``.
|
||||
* On macOS, it looks for the extension ``.dylib``.
|
||||
|
||||
For example, if you are on Linux and your ``foreign`` declaration is in
|
||||
``Foo.cry``, Cryptol will dynamically load ``Foo.so``. Then for each ``foreign``
|
||||
declaration it will look for a symbol with the same name in the shared library.
|
||||
So in this case the function we want to call must be bound to the symbol ``add``
|
||||
in the shared library.
|
||||
|
||||
Once the module is loaded, the foreign ``add`` function can be called like any
|
||||
other Cryptol function. Cryptol automatically converts between Cryptol ``[32]``
|
||||
values and C ``uint32_t`` values.
|
||||
|
||||
The whole process would look something like this:
|
||||
|
||||
.. code-block::
|
||||
|
||||
$ cc -fPIC -shared Example.c -o Example.so
|
||||
$ cryptol
|
||||
Loading module Cryptol
|
||||
Cryptol> :l Example.cry
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
Main> add 1 2
|
||||
0x00000003
|
||||
|
||||
Note: Since Cryptol currently only accesses the compiled binary and not the C
|
||||
source, it has no way of checking that the Cryptol function type you declare in
|
||||
your Cryptol code actually matches the type of the C function. **It is your
|
||||
responsibility to make sure the types match up**. If they do not then there may
|
||||
be undefined behavior.
|
||||
|
||||
Compiling C code
|
||||
----------------
|
||||
|
||||
Cryptol currently does not handle compilation of C code to shared libraries. For
|
||||
simple usages, you can do this manually with the following commands:
|
||||
|
||||
* Linux: ``cc -fPIC -shared Foo.c -o Foo.so``
|
||||
* macOS: ``cc -dynamiclib Foo.c -o Foo.dylib``
|
||||
|
||||
Converting between Cryptol and C types
|
||||
--------------------------------------
|
||||
|
||||
This section describes how a given Cryptol function signature maps to a C
|
||||
function prototype. The FFI only supports a limited set of Cryptol types which
|
||||
have a clear translation into C.
|
||||
|
||||
Overall structure
|
||||
~~~~~~~~~~~~~~~~~
|
||||
|
||||
Cryptol ``foreign`` bindings must be functions. These functions may have
|
||||
multiple (curried) arguments; they may also be polymorphic, with certain
|
||||
limitations. That is, the general structure of a ``foreign`` declaration would
|
||||
look something like this:
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
foreign f : {a1, ..., ak} (c1, ..., cn) => T1 -> ... -> Tm -> Tr
|
||||
|
||||
Each type argument to the Cryptol function (``a1, ..., ak`` above) corresponds
|
||||
to a value argument to the C function. These arguments are passed first, in the
|
||||
order of the type variables declared in the Cryptol signature, before any
|
||||
Cryptol value arguments.
|
||||
|
||||
Each value argument to the Cryptol function (``T1, ..., Tm`` above) corresponds
|
||||
to a number of value arguments to the C function. That is, a Cryptol value
|
||||
argument could correspond to zero, one, or many C arguments. The C arguments for
|
||||
each Cryptol value argument are passed in the order of the Cryptol value
|
||||
arguments, after any C arguments corresponding to Cryptol type arguments.
|
||||
|
||||
The return value of the Cryptol function (``Tr`` above) is either obtained by
|
||||
directly returning from the C function or by passing *output arguments* to the C
|
||||
function, depending on the return type. Output arguments are pointers to memory
|
||||
which can be modified by the C function to store its output values. If output
|
||||
arguments are used, they are passed last, after the C arguments corresponding to
|
||||
Cryptol arguments.
|
||||
|
||||
The following tables list the C type(s) that each Cryptol type (or kind)
|
||||
corresponds to.
|
||||
|
||||
Type parameters
|
||||
~~~~~~~~~~~~~~~
|
||||
|
||||
============ ==========
|
||||
Cryptol kind C type
|
||||
============ ==========
|
||||
``#`` ``size_t``
|
||||
============ ==========
|
||||
|
||||
Only numeric type parameters are allowed in polymorphic ``foreign`` functions.
|
||||
Furthermore, each type parameter ``n`` must satisfy ``fin n``. This has to be
|
||||
explicitly declared in the Cryptol signature.
|
||||
|
||||
Note that if a polymorphic foreign function is called with a type argument that
|
||||
does not fit in a ``size_t``, there will be a runtime error. (While we could
|
||||
check this statically by requiring that all type variables in foreign functions
|
||||
satisfy ``< 2^^64`` instead of just ``fin``, in practice this would be too
|
||||
cumbersome.)
|
||||
|
||||
Bit
|
||||
~~~
|
||||
|
||||
============ ===========
|
||||
Cryptol type C type
|
||||
============ ===========
|
||||
``Bit`` ``uint8_t``
|
||||
============ ===========
|
||||
|
||||
When converting to C, ``True`` is converted to ``1`` and ``False`` to ``0``.
|
||||
When converting to Cryptol, any nonzero number is converted to ``True`` and
|
||||
``0`` is converted to ``False``.
|
||||
|
||||
Integral types
|
||||
~~~~~~~~~~~~~~
|
||||
|
||||
Let ``K : #`` be a Cryptol type. Note ``K`` must be an actual fixed numeric type
|
||||
and not a type variable.
|
||||
|
||||
================================== ============
|
||||
Cryptol type C type
|
||||
================================== ============
|
||||
``[K]Bit`` where ``0 <= K <= 8`` ``uint8_t``
|
||||
``[K]Bit`` where ``8 < K <= 16`` ``uint16_t``
|
||||
``[K]Bit`` where ``16 < K <= 32`` ``uint32_t``
|
||||
``[K]Bit`` where ``32 < K <= 64`` ``uint64_t``
|
||||
================================== ============
|
||||
|
||||
If the Cryptol type is smaller than the C type, then when converting to C the
|
||||
value is padded with zero bits, and when converting to Cryptol the extra bits
|
||||
are ignored. For instance, for the Cryptol type ``[4]``, the Cryptol value ``0xf
|
||||
: [4]`` is converted to the C value ``uint8_t`` ``0x0f``, and the C ``uint8_t``
|
||||
``0xaf`` is converted to the Cryptol value ``0xf : [4]``.
|
||||
|
||||
Note that words larger than 64 bits are not supported, since there is no
|
||||
standard C integral type for that. You can split it into a sequence of smaller
|
||||
words first in Cryptol, then use the FFI conversion for sequences of words to
|
||||
handle it in C as an array.
|
||||
|
||||
Floating point types
|
||||
~~~~~~~~~~~~~~~~~~~~
|
||||
|
||||
============ ==========
|
||||
Cryptol type C type
|
||||
============ ==========
|
||||
``Float32`` ``float``
|
||||
``Float64`` ``double``
|
||||
============ ==========
|
||||
|
||||
Note: the Cryptol ``Float`` types are defined in the built-in module ``Float``.
|
||||
Other sizes of floating points are not supported.
|
||||
|
||||
Sequences
|
||||
~~~~~~~~~
|
||||
|
||||
Let ``n : #`` be a Cryptol type, possibly containing type variables, that
|
||||
satisfies ``fin n``, and ``T`` be one of the above Cryptol *integral types* or
|
||||
*floating point types*. Let ``U`` be the C type that ``T`` corresponds to.
|
||||
|
||||
============ ===========
|
||||
Cryptol type C type
|
||||
============ ===========
|
||||
``[n]T`` ``U*``
|
||||
============ ===========
|
||||
|
||||
The C pointer points to an array of ``n`` elements of type ``U``. Note that,
|
||||
while the length of the array itself is not explicitly passed along with the
|
||||
pointer, any type arguments contained in the size are passed as C ``size_t``'s
|
||||
earlier, so the C code can always know the length of the array.
|
||||
|
||||
Tuples and records
|
||||
~~~~~~~~~~~~~~~~~~
|
||||
|
||||
Let ``T1, T2, ..., Tn`` be Cryptol types supported by the FFI (which may be any
|
||||
of the types mentioned above, or tuples and records themselves). Let
|
||||
``U1, U2, ..., Un`` be the C types that ``T1, T2, ..., Tn`` respectively
|
||||
correspond to. Let ``f1, f2, ..., fn`` be arbitrary field names.
|
||||
|
||||
================================= ===================
|
||||
Cryptol type C types
|
||||
================================= ===================
|
||||
``(T1, T2, ..., Tn)`` ``U1, U2, ..., Un``
|
||||
``{f1: T1, f2: T2, ..., fn: Tn}`` ``U1, U2, ..., Un``
|
||||
================================= ===================
|
||||
|
||||
In this case, each Cryptol tuple or record is flattened out; passing a tuple as
|
||||
an argument behaves the same as if you passed its components individually. This
|
||||
flattening is applied recursively for nested tuples and records. Note that this
|
||||
means empty tuples don't map to any C values at all.
|
||||
|
||||
Type synonyms
|
||||
~~~~~~~~~~~~~
|
||||
|
||||
All type synonyms are expanded before applying the above rules, so you can use
|
||||
type synonyms in ``foreign`` declarations to improve readability.
|
||||
|
||||
Return values
|
||||
~~~~~~~~~~~~~
|
||||
|
||||
If the Cryptol return type is ``Bit`` or one of the above *integral types* or
|
||||
*floating point types*, the value is returned directly from the C function. In
|
||||
that case, the return type of the C function will be the C type corresponding to
|
||||
the Cryptol type, and no extra arguments are added.
|
||||
|
||||
If the Cryptol return type is a sequence, tuple, or record, then the value is
|
||||
returned using output arguments, and the return type of the C function will be
|
||||
``void``. For tuples and records, each component is recursively returned as
|
||||
output arguments. When treated as an output argument, each C type ``U`` will be
|
||||
a pointer ``U*`` instead, except in the case of sequences, where the output and
|
||||
input versions are the same type, because it is already a pointer.
|
||||
|
||||
Quick reference
|
||||
~~~~~~~~~~~~~~~
|
||||
|
||||
================================== =================== ============= =========================
|
||||
Cryptol type (or kind) C argument type(s) C return type C output argument type(s)
|
||||
================================== =================== ============= =========================
|
||||
``#`` ``size_t`` N/A N/A
|
||||
``Bit`` ``uint8_t`` ``uint8_t`` ``uint8_t*``
|
||||
``[K]Bit`` where ``0 <= K <= 8`` ``uint8_t`` ``uint8_t`` ``uint8_t*``
|
||||
``[K]Bit`` where ``8 < K <= 16`` ``uint16_t`` ``uint16_t`` ``uint16_t*``
|
||||
``[K]Bit`` where ``16 < K <= 32`` ``uint32_t`` ``uint32_t`` ``uint32_t*``
|
||||
``[K]Bit`` where ``32 < K <= 64`` ``uint64_t`` ``uint64_t`` ``uint64_t*``
|
||||
``Float32`` ``float`` ``float`` ``float*``
|
||||
``Float64`` ``double`` ``double`` ``double*``
|
||||
``[n]T`` ``U*`` N/A ``U*``
|
||||
``(T1, T2, ..., Tn)`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn``
|
||||
``{f1: T1, f2: T2, ..., fn: Tn}`` ``U1, U2, ..., Un`` N/A ``V1, V2, ..., Vn``
|
||||
================================== =================== ============= =========================
|
||||
|
||||
where ``K`` is a constant number, ``n`` is a variable number, ``Ti`` is a type,
|
||||
``Ui`` is its C argument type, and ``Vi`` is its C output argument type.
|
||||
|
||||
Memory
|
||||
------
|
||||
|
||||
When pointers are involved, namely in the cases of sequences and output
|
||||
arguments, they point to memory. This memory is always allocated and deallocated
|
||||
by Cryptol; the C code does not need to manage this memory.
|
||||
|
||||
In the case of sequences, the pointer will point to an array. In the case of an
|
||||
output argument for a non-sequence type, the pointer will point to a piece of
|
||||
memory large enough to hold the given C type, and you should not try to access
|
||||
any adjacent memory.
|
||||
|
||||
For input sequence arguments, the array will already be set to the values
|
||||
corresponding to the Cryptol values in the sequence. For output arguments, the
|
||||
memory may be uninitialized when passed to C, and the C code should not read
|
||||
from it. It must write to the memory the value it is returning.
|
||||
|
||||
Evaluation
|
||||
----------
|
||||
|
||||
All Cryptol arguments are fully evaluated when a foreign function is called.
|
||||
|
||||
Example
|
||||
-------
|
||||
|
||||
The Cryptol signature
|
||||
|
||||
.. code-block:: cryptol
|
||||
|
||||
foreign f : {n} (fin n) => [n][10] -> {a : Bit, b : [64]}
|
||||
-> (Float64, [n + 1][20])
|
||||
|
||||
corresponds to the C signature
|
||||
|
||||
.. code-block:: c
|
||||
|
||||
void f(size_t n, uint16_t *in0, uint8_t in1, uint64_t in2,
|
||||
double *out0, uint32_t *out1);
|
||||
@ -12,4 +12,5 @@ Cryptol Reference Manual
|
||||
OverloadedOperations
|
||||
TypeDeclarations
|
||||
Modules
|
||||
FFI
|
||||
|
||||
|
||||
@ -236,7 +236,6 @@ div.body p, div.body dd, div.body li, div.body blockquote {
|
||||
a.headerlink {
|
||||
visibility: hidden;
|
||||
}
|
||||
|
||||
a.brackets:before,
|
||||
span.brackets > a:before{
|
||||
content: "[";
|
||||
@ -247,6 +246,7 @@ span.brackets > a:after {
|
||||
content: "]";
|
||||
}
|
||||
|
||||
|
||||
h1:hover > a.headerlink,
|
||||
h2:hover > a.headerlink,
|
||||
h3:hover > a.headerlink,
|
||||
@ -334,14 +334,12 @@ aside.sidebar {
|
||||
p.sidebar-title {
|
||||
font-weight: bold;
|
||||
}
|
||||
|
||||
div.admonition, div.topic, aside.topic, blockquote {
|
||||
div.admonition, div.topic, blockquote {
|
||||
clear: left;
|
||||
}
|
||||
|
||||
/* -- topics ---------------------------------------------------------------- */
|
||||
|
||||
div.topic, aside.topic {
|
||||
div.topic {
|
||||
border: 1px solid #ccc;
|
||||
padding: 7px;
|
||||
margin: 10px 0 10px 0;
|
||||
@ -380,7 +378,6 @@ div.body p.centered {
|
||||
div.sidebar > :last-child,
|
||||
aside.sidebar > :last-child,
|
||||
div.topic > :last-child,
|
||||
aside.topic > :last-child,
|
||||
div.admonition > :last-child {
|
||||
margin-bottom: 0;
|
||||
}
|
||||
@ -388,7 +385,6 @@ div.admonition > :last-child {
|
||||
div.sidebar::after,
|
||||
aside.sidebar::after,
|
||||
div.topic::after,
|
||||
aside.topic::after,
|
||||
div.admonition::after,
|
||||
blockquote::after {
|
||||
display: block;
|
||||
@ -612,8 +608,6 @@ ol.simple p,
|
||||
ul.simple p {
|
||||
margin-bottom: 0;
|
||||
}
|
||||
|
||||
/* Docutils 0.17 and older (footnotes & citations) */
|
||||
dl.footnote > dt,
|
||||
dl.citation > dt {
|
||||
float: left;
|
||||
@ -631,33 +625,6 @@ dl.citation > dd:after {
|
||||
clear: both;
|
||||
}
|
||||
|
||||
/* Docutils 0.18+ (footnotes & citations) */
|
||||
aside.footnote > span,
|
||||
div.citation > span {
|
||||
float: left;
|
||||
}
|
||||
aside.footnote > span:last-of-type,
|
||||
div.citation > span:last-of-type {
|
||||
padding-right: 0.5em;
|
||||
}
|
||||
aside.footnote > p {
|
||||
margin-left: 2em;
|
||||
}
|
||||
div.citation > p {
|
||||
margin-left: 4em;
|
||||
}
|
||||
aside.footnote > p:last-of-type,
|
||||
div.citation > p:last-of-type {
|
||||
margin-bottom: 0em;
|
||||
}
|
||||
aside.footnote > p:last-of-type:after,
|
||||
div.citation > p:last-of-type:after {
|
||||
content: "";
|
||||
clear: both;
|
||||
}
|
||||
|
||||
/* Footnotes & citations ends */
|
||||
|
||||
dl.field-list {
|
||||
display: grid;
|
||||
grid-template-columns: fit-content(30%) auto;
|
||||
@ -669,11 +636,11 @@ dl.field-list > dt {
|
||||
padding-left: 0.5em;
|
||||
padding-right: 5px;
|
||||
}
|
||||
|
||||
dl.field-list > dt:after {
|
||||
content: ":";
|
||||
}
|
||||
|
||||
|
||||
dl.field-list > dd {
|
||||
padding-left: 0.5em;
|
||||
margin-top: 0em;
|
||||
|
||||
@ -10,5 +10,5 @@ var DOCUMENTATION_OPTIONS = {
|
||||
SOURCELINK_SUFFIX: '.txt',
|
||||
NAVIGATION_WITH_KEYS: false,
|
||||
SHOW_SEARCH_SUMMARY: true,
|
||||
ENABLE_SEARCH_SHORTCUTS: false,
|
||||
ENABLE_SEARCH_SHORTCUTS: true,
|
||||
};
|
||||
@ -88,7 +88,7 @@ const _displayItem = (item, highlightTerms, searchTerms) => {
|
||||
linkEl.href = linkUrl + "?" + params.toString() + anchor;
|
||||
linkEl.innerHTML = title;
|
||||
if (descr)
|
||||
listItem.appendChild(document.createElement("span")).innerText =
|
||||
listItem.appendChild(document.createElement("span")).innerHTML =
|
||||
" (" + descr + ")";
|
||||
else if (showSearchSummary)
|
||||
fetch(requestUrl)
|
||||
@ -155,10 +155,8 @@ const Search = {
|
||||
_pulse_status: -1,
|
||||
|
||||
htmlToText: (htmlString) => {
|
||||
const htmlElement = document
|
||||
.createRange()
|
||||
.createContextualFragment(htmlString);
|
||||
_removeChildren(htmlElement.querySelectorAll(".headerlink"));
|
||||
const htmlElement = new DOMParser().parseFromString(htmlString, 'text/html');
|
||||
htmlElement.querySelectorAll(".headerlink").forEach((el) => { el.remove() });
|
||||
const docContent = htmlElement.querySelector('[role="main"]');
|
||||
if (docContent !== undefined) return docContent.textContent;
|
||||
console.warn(
|
||||
@ -504,11 +502,12 @@ const Search = {
|
||||
* latter for highlighting it.
|
||||
*/
|
||||
makeSearchSummary: (htmlText, keywords, highlightWords) => {
|
||||
const text = Search.htmlToText(htmlText).toLowerCase();
|
||||
const text = Search.htmlToText(htmlText);
|
||||
if (text === "") return null;
|
||||
|
||||
const textLower = text.toLowerCase();
|
||||
const actualStartPosition = [...keywords]
|
||||
.map((k) => text.indexOf(k.toLowerCase()))
|
||||
.map((k) => textLower.indexOf(k.toLowerCase()))
|
||||
.filter((i) => i > -1)
|
||||
.slice(-1)[0];
|
||||
const startWithContext = Math.max(actualStartPosition - 120, 0);
|
||||
@ -516,9 +515,9 @@ const Search = {
|
||||
const top = startWithContext === 0 ? "" : "...";
|
||||
const tail = startWithContext + 240 < text.length ? "..." : "";
|
||||
|
||||
let summary = document.createElement("div");
|
||||
let summary = document.createElement("p");
|
||||
summary.classList.add("context");
|
||||
summary.innerText = top + text.substr(startWithContext, 240).trim() + tail;
|
||||
summary.textContent = top + text.substr(startWithContext, 240).trim() + tail;
|
||||
|
||||
highlightWords.forEach((highlightWord) =>
|
||||
_highlightText(summary, highlightWord, "highlighted")
|
||||
|
||||
@ -43,6 +43,7 @@
|
||||
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="FFI.html">Foreign Function Interface</a></li>
|
||||
</ul>
|
||||
|
||||
</div>
|
||||
|
||||
Binary file not shown.
@ -46,6 +46,7 @@
|
||||
<li class="toctree-l1"><a class="reference internal" href="OverloadedOperations.html">Overloaded Operations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="TypeDeclarations.html">Type Declarations</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="Modules.html">Modules</a></li>
|
||||
<li class="toctree-l1"><a class="reference internal" href="FFI.html">Foreign Function Interface</a></li>
|
||||
</ul>
|
||||
|
||||
</div>
|
||||
|
||||
File diff suppressed because one or more lines are too long
227
src/Cryptol/Backend/FFI.hs
Normal file
227
src/Cryptol/Backend/FFI.hs
Normal file
@ -0,0 +1,227 @@
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE ExistentialQuantification #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TypeApplications #-}
|
||||
|
||||
-- | The implementation of loading and calling external functions from shared
|
||||
-- libraries. Currently works on Unix only.
|
||||
module Cryptol.Backend.FFI
|
||||
( ForeignSrc
|
||||
, loadForeignSrc
|
||||
, unloadForeignSrc
|
||||
#ifdef FFI_ENABLED
|
||||
, ForeignImpl
|
||||
, loadForeignImpl
|
||||
, FFIArg
|
||||
, FFIRet
|
||||
, SomeFFIArg (..)
|
||||
, callForeignImpl
|
||||
#endif
|
||||
)
|
||||
where
|
||||
|
||||
import Control.DeepSeq
|
||||
|
||||
import Cryptol.Backend.FFI.Error
|
||||
|
||||
#ifdef FFI_ENABLED
|
||||
|
||||
import Control.Concurrent.MVar
|
||||
import Control.Exception
|
||||
import Control.Monad
|
||||
import Data.Bifunctor
|
||||
import Data.Word
|
||||
import Foreign hiding (newForeignPtr)
|
||||
import Foreign.C.Types
|
||||
import Foreign.Concurrent
|
||||
import Foreign.LibFFI
|
||||
import System.FilePath ((-<.>))
|
||||
import System.IO.Error
|
||||
import System.Posix.DynamicLinker
|
||||
|
||||
import Cryptol.Utils.Panic
|
||||
|
||||
#else
|
||||
|
||||
import GHC.Generics
|
||||
|
||||
#endif
|
||||
|
||||
#ifdef FFI_ENABLED
|
||||
|
||||
-- | A source from which we can retrieve implementations of foreign functions.
|
||||
data ForeignSrc = ForeignSrc
|
||||
{ -- | The 'ForeignPtr' wraps the pointer returned by 'dlopen', where the
|
||||
-- finalizer calls 'dlclose' when the library is no longer needed. We keep
|
||||
-- references to the 'ForeignPtr' in each foreign function that is in the
|
||||
-- evaluation environment, so that the shared library will stay open as long
|
||||
-- as there are references to it.
|
||||
foreignSrcFPtr :: ForeignPtr ()
|
||||
-- | We support explicit unloading of the shared library so we keep track of
|
||||
-- if it has already been unloaded, and if so the finalizer does nothing.
|
||||
-- This is updated atomically when the library is unloaded.
|
||||
, foreignSrcLoaded :: MVar Bool }
|
||||
|
||||
instance Show ForeignSrc where
|
||||
show = show . foreignSrcFPtr
|
||||
|
||||
instance NFData ForeignSrc where
|
||||
rnf ForeignSrc {..} = foreignSrcFPtr `seq` foreignSrcLoaded `deepseq` ()
|
||||
|
||||
-- | Load a 'ForeignSrc' for the given __Cryptol__ file path. The file path of
|
||||
-- the shared library that we try to load is the same as the Cryptol file path
|
||||
-- except with a platform specific extension.
|
||||
loadForeignSrc :: FilePath -> IO (Either FFILoadError ForeignSrc)
|
||||
loadForeignSrc = loadForeignLib >=> traverse \ptr -> do
|
||||
foreignSrcLoaded <- newMVar True
|
||||
foreignSrcFPtr <- newForeignPtr ptr (unloadForeignSrc' foreignSrcLoaded ptr)
|
||||
pure ForeignSrc {..}
|
||||
|
||||
loadForeignLib :: FilePath -> IO (Either FFILoadError (Ptr ()))
|
||||
#ifdef darwin_HOST_OS
|
||||
-- On Darwin, try loading .dylib first, and if that fails try .so
|
||||
loadForeignLib path =
|
||||
(Right <$> open "dylib") `catchIOError` \e1 ->
|
||||
(Right <$> open "so") `catchIOError` \e2 ->
|
||||
pure $ Left $ CantLoadFFISrc path $
|
||||
displayException e1 ++ "\n" ++ displayException e2
|
||||
#else
|
||||
-- On other platforms, use .so
|
||||
loadForeignLib path =
|
||||
tryLoad (CantLoadFFISrc path) $ open "so"
|
||||
#endif
|
||||
where -- RTLD_NOW so we can make sure that the symbols actually exist at
|
||||
-- module loading time
|
||||
open ext = undl <$> dlopen (path -<.> ext) [RTLD_NOW]
|
||||
|
||||
-- | Explicitly unload a 'ForeignSrc' immediately instead of waiting for the
|
||||
-- garbage collector to do it. This can be useful if you want to immediately
|
||||
-- load the same library again to pick up new changes.
|
||||
--
|
||||
-- The 'ForeignSrc' __must not__ be used in any way after this is called,
|
||||
-- including calling 'ForeignImpl's loaded from it.
|
||||
unloadForeignSrc :: ForeignSrc -> IO ()
|
||||
unloadForeignSrc ForeignSrc {..} = withForeignPtr foreignSrcFPtr $
|
||||
unloadForeignSrc' foreignSrcLoaded
|
||||
|
||||
unloadForeignSrc' :: MVar Bool -> Ptr () -> IO ()
|
||||
unloadForeignSrc' loaded lib = modifyMVar_ loaded \l -> do
|
||||
when l $ unloadForeignLib lib
|
||||
pure False
|
||||
|
||||
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"]
|
||||
|
||||
-- | An implementation of a foreign function.
|
||||
data ForeignImpl = ForeignImpl
|
||||
{ foreignImplFun :: FunPtr ()
|
||||
-- | We don't need this to call the function but we want to keep the library
|
||||
-- around as long as we still have a function from it so that it isn't
|
||||
-- unloaded too early.
|
||||
, foreignImplSrc :: ForeignSrc
|
||||
}
|
||||
|
||||
-- | Load a 'ForeignImpl' with the given name from the given 'ForeignSrc'.
|
||||
loadForeignImpl :: ForeignSrc -> String -> IO (Either FFILoadError ForeignImpl)
|
||||
loadForeignImpl foreignImplSrc name =
|
||||
withForeignSrc foreignImplSrc \lib ->
|
||||
tryLoad (CantLoadFFIImpl name) do
|
||||
foreignImplFun <- loadForeignFunPtr lib name
|
||||
pure ForeignImpl {..}
|
||||
|
||||
loadForeignFunPtr :: Ptr () -> String -> IO (FunPtr ())
|
||||
loadForeignFunPtr = dlsym . DLHandle
|
||||
|
||||
tryLoad :: (String -> FFILoadError) -> IO a -> IO (Either FFILoadError a)
|
||||
tryLoad err = fmap (first $ err . displayException) . tryIOError
|
||||
|
||||
-- | Types which can be converted into libffi arguments.
|
||||
--
|
||||
-- The Storable constraint is so that we can put them in arrays.
|
||||
class Storable a => FFIArg a where
|
||||
ffiArg :: a -> Arg
|
||||
|
||||
instance FFIArg Word8 where
|
||||
ffiArg = argWord8
|
||||
|
||||
instance FFIArg Word16 where
|
||||
ffiArg = argWord16
|
||||
|
||||
instance FFIArg Word32 where
|
||||
ffiArg = argWord32
|
||||
|
||||
instance FFIArg Word64 where
|
||||
ffiArg = argWord64
|
||||
|
||||
instance FFIArg CFloat where
|
||||
ffiArg = argCFloat
|
||||
|
||||
instance FFIArg CDouble where
|
||||
ffiArg = argCDouble
|
||||
|
||||
instance FFIArg (Ptr a) where
|
||||
ffiArg = argPtr
|
||||
|
||||
instance FFIArg CSize where
|
||||
ffiArg = argCSize
|
||||
|
||||
-- | Types which can be returned from libffi.
|
||||
--
|
||||
-- The Storable constraint is so that we can put them in arrays.
|
||||
class Storable a => FFIRet a where
|
||||
ffiRet :: RetType a
|
||||
|
||||
instance FFIRet Word8 where
|
||||
ffiRet = retWord8
|
||||
|
||||
instance FFIRet Word16 where
|
||||
ffiRet = retWord16
|
||||
|
||||
instance FFIRet Word32 where
|
||||
ffiRet = retWord32
|
||||
|
||||
instance FFIRet Word64 where
|
||||
ffiRet = retWord64
|
||||
|
||||
instance FFIRet CFloat where
|
||||
ffiRet = retCFloat
|
||||
|
||||
instance FFIRet CDouble where
|
||||
ffiRet = retCDouble
|
||||
|
||||
instance FFIRet () where
|
||||
ffiRet = retVoid
|
||||
|
||||
-- | Existential wrapper around a 'FFIArg'.
|
||||
data SomeFFIArg = forall a. FFIArg a => SomeFFIArg a
|
||||
|
||||
-- | Call a 'ForeignImpl' with the given arguments. The type parameter decides
|
||||
-- how the return value should be converted into a Haskell value.
|
||||
callForeignImpl :: forall a. FFIRet a => ForeignImpl -> [SomeFFIArg] -> IO a
|
||||
callForeignImpl ForeignImpl {..} xs = withForeignSrc foreignImplSrc \_ ->
|
||||
callFFI foreignImplFun (ffiRet @a) $ map toArg xs
|
||||
where toArg (SomeFFIArg x) = ffiArg x
|
||||
|
||||
#else
|
||||
|
||||
data ForeignSrc = ForeignSrc deriving (Show, Generic, NFData)
|
||||
|
||||
loadForeignSrc :: FilePath -> IO (Either FFILoadError ForeignSrc)
|
||||
loadForeignSrc _ = pure $ Right ForeignSrc
|
||||
|
||||
unloadForeignSrc :: ForeignSrc -> IO ()
|
||||
unloadForeignSrc _ = pure ()
|
||||
|
||||
#endif
|
||||
31
src/Cryptol/Backend/FFI/Error.hs
Normal file
31
src/Cryptol/Backend/FFI/Error.hs
Normal file
@ -0,0 +1,31 @@
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
|
||||
-- | Errors from dynamic loading of shared libraries for FFI.
|
||||
module Cryptol.Backend.FFI.Error where
|
||||
|
||||
import Control.DeepSeq
|
||||
import GHC.Generics
|
||||
|
||||
import Cryptol.Utils.PP
|
||||
|
||||
data FFILoadError
|
||||
= CantLoadFFISrc
|
||||
FilePath -- ^ Path to cryptol module
|
||||
String -- ^ Error message
|
||||
| CantLoadFFIImpl
|
||||
String -- ^ Function name
|
||||
String -- ^ Error message
|
||||
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)
|
||||
@ -54,7 +54,7 @@ import qualified Control.Exception as X
|
||||
import Cryptol.Parser.Position
|
||||
import Cryptol.Utils.Panic
|
||||
import Cryptol.Utils.PP
|
||||
import Cryptol.TypeCheck.AST(Name)
|
||||
import Cryptol.TypeCheck.AST(Name, TParam)
|
||||
|
||||
-- | A computation that returns an already-evaluated value.
|
||||
ready :: a -> Eval a
|
||||
@ -412,17 +412,20 @@ evalPanic cxt = panic ("[Eval] " ++ cxt)
|
||||
|
||||
-- | Data type describing errors that can occur during evaluation.
|
||||
data EvalError
|
||||
= InvalidIndex (Maybe Integer) -- ^ Out-of-bounds index
|
||||
| DivideByZero -- ^ Division or modulus by 0
|
||||
| NegativeExponent -- ^ Exponentiation by negative integer
|
||||
| LogNegative -- ^ Logarithm of a negative integer
|
||||
| UserError String -- ^ Call to the Cryptol @error@ primitive
|
||||
| LoopError String -- ^ Detectable nontermination
|
||||
| NoPrim Name -- ^ Primitive with no implementation
|
||||
| BadRoundingMode Integer -- ^ Invalid rounding mode
|
||||
| BadValue String -- ^ Value outside the domain of a partial function.
|
||||
= InvalidIndex (Maybe Integer) -- ^ Out-of-bounds index
|
||||
| DivideByZero -- ^ Division or modulus by 0
|
||||
| NegativeExponent -- ^ Exponentiation by negative integer
|
||||
| LogNegative -- ^ Logarithm of a negative integer
|
||||
| UserError String -- ^ Call to the Cryptol @error@ primitive
|
||||
| LoopError String -- ^ Detectable nontermination
|
||||
| NoPrim Name -- ^ Primitive with no implementation
|
||||
| BadRoundingMode Integer -- ^ Invalid rounding mode
|
||||
| BadValue String -- ^ Value outside the domain of a partial function.
|
||||
| NoMatchingPropGuardCase String -- ^ No prop guard holds for the given type variables.
|
||||
deriving Typeable
|
||||
| FFINotSupported Name -- ^ Foreign function cannot be called
|
||||
| FFITypeNumTooBig Name TParam Integer -- ^ Number passed to foreign function
|
||||
-- as a type argument is too large
|
||||
deriving Typeable
|
||||
|
||||
instance PP EvalError where
|
||||
ppPrec _ e = case e of
|
||||
@ -442,6 +445,17 @@ instance PP EvalError where
|
||||
BadValue x -> "invalid input for" <+> backticks (text x)
|
||||
NoPrim x -> text "unimplemented primitive:" <+> pp x
|
||||
NoMatchingPropGuardCase msg -> text $ "No matching prop guard case; " ++ msg
|
||||
FFINotSupported x -> vcat
|
||||
[ text "cannot call foreign function" <+> pp x
|
||||
, text "FFI calls are not supported in this context"
|
||||
, text "If you are trying to evaluate an expression, try rebuilding"
|
||||
, text " Cryptol with FFI support enabled."
|
||||
]
|
||||
FFITypeNumTooBig f p n -> vcat
|
||||
[ text "numeric type argument to foreign function is too large:"
|
||||
<+> integer n
|
||||
, text "in type parameter" <+> pp p <+> "of function" <+> pp f
|
||||
, text "type arguments must fit in a C `size_t`" ]
|
||||
|
||||
instance Show EvalError where
|
||||
show = show . pp
|
||||
|
||||
@ -438,9 +438,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)]
|
||||
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
|
||||
@ -474,6 +476,18 @@ evalDecl sym renv env d = do
|
||||
Just (Left ex) -> bindVar sym (dName d) (evalExpr sym renv ex) env
|
||||
Nothing -> bindVar sym (dName d) (cryNoPrimError sym (dName d)) env
|
||||
|
||||
DForeign _ -> do
|
||||
-- Foreign declarations should have been handled by the previous
|
||||
-- Cryptol.Eval.FFI.evalForeignDecls pass already, so they should already
|
||||
-- be in the environment. If not, then either Cryptol was not compiled
|
||||
-- with FFI support enabled, or we are in a non-Concrete backend. In that
|
||||
-- case, we just bind the name to an error computation which will raise an
|
||||
-- error if we try to evaluate it.
|
||||
case lookupVar (dName d) env of
|
||||
Just _ -> pure env
|
||||
Nothing -> bindVar sym (dName d)
|
||||
(raiseError sym $ FFINotSupported $ dName d) env
|
||||
|
||||
DExpr e -> bindVar sym (dName d) (evalExpr sym renv e) env
|
||||
|
||||
|
||||
@ -747,5 +761,6 @@ evalMatch sym (lsz, lenv) m = seq lsz $ case m of
|
||||
where
|
||||
f env =
|
||||
case dDefinition d of
|
||||
DPrim -> evalPanic "evalMatch" ["Unexpected local primitive"]
|
||||
DExpr e -> evalExpr sym env e
|
||||
DPrim -> evalPanic "evalMatch" ["Unexpected local primitive"]
|
||||
DForeign _ -> evalPanic "evalMatch" ["Unexpected local foreign"]
|
||||
DExpr e -> evalExpr sym env e
|
||||
|
||||
281
src/Cryptol/Eval/FFI.hs
Normal file
281
src/Cryptol/Eval/FFI.hs
Normal file
@ -0,0 +1,281 @@
|
||||
{-# 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
|
||||
( evalForeignDecls
|
||||
) where
|
||||
|
||||
import Cryptol.Backend.FFI
|
||||
import Cryptol.Backend.FFI.Error
|
||||
import Cryptol.Eval
|
||||
import Cryptol.ModuleSystem.Env
|
||||
import Cryptol.TypeCheck.AST
|
||||
|
||||
#ifdef FFI_ENABLED
|
||||
|
||||
import Data.Either
|
||||
import Data.IORef
|
||||
import Data.Maybe
|
||||
import Data.Proxy
|
||||
import Data.Traversable
|
||||
import Data.Word
|
||||
import Foreign
|
||||
import Foreign.C.Types
|
||||
import GHC.Float
|
||||
import LibBF (bfFromDouble, bfToDouble,
|
||||
pattern NearEven)
|
||||
import System.Directory
|
||||
|
||||
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.FFI.FFIType
|
||||
import Cryptol.Utils.Ident
|
||||
import Cryptol.Utils.RecordMap
|
||||
|
||||
-- | Find all the foreign declarations in the module and add them to the
|
||||
-- environment. This is a separate pass from the main evaluation functions in
|
||||
-- "Cryptol.Eval" since it only works for the Concrete backend.
|
||||
--
|
||||
-- Note: 'Right' is only returned if we successfully loaded some foreign
|
||||
-- functions and the environment was modified. If there were no foreign
|
||||
-- declarations at all then @Left []@ is returned, so 'Left' does not
|
||||
-- necessarily indicate an error.
|
||||
evalForeignDecls :: ModulePath -> Module -> EvalEnv ->
|
||||
Eval (Either [FFILoadError] (ForeignSrc, EvalEnv))
|
||||
evalForeignDecls path m env = io
|
||||
case mapMaybe getForeign $ mDecls m of
|
||||
[] -> pure $ Left []
|
||||
foreigns ->
|
||||
case path of
|
||||
InFile p -> canonicalizePath p >>= loadForeignSrc >>=
|
||||
\case
|
||||
Right fsrc -> collect <$> for foreigns \(name, ffiType) ->
|
||||
fmap ((name,) . foreignPrimPoly name ffiType) <$>
|
||||
loadForeignImpl fsrc (unpackIdent $ nameIdent name)
|
||||
where collect (partitionEithers -> (errs, primMap))
|
||||
| null errs = Right
|
||||
(fsrc, foldr (uncurry bindVarDirect) env primMap)
|
||||
| otherwise = Left errs
|
||||
Left err -> pure $ Left [err]
|
||||
-- We don't handle in-memory modules for now
|
||||
InMem _ _ -> evalPanic "evalForeignDecls"
|
||||
["Can't find foreign source of in-memory module"]
|
||||
where getForeign (NonRecursive Decl { dName, dDefinition = DForeign ffiType })
|
||||
= Just (dName, ffiType)
|
||||
getForeign _ = Nothing
|
||||
|
||||
-- | 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 fft impl = buildNumPoly (ffiTParams fft) 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 (tp:tps) tenv = PNumPoly \n ->
|
||||
buildNumPoly tps $ bindTypeVar (TVBound tp) (Left n) tenv
|
||||
buildNumPoly [] tenv = foreignPrim name fft impl 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
|
||||
{ getRetAsValue :: forall a. FFIRet a => IO a
|
||||
, getRetAsOutArgs :: [SomeFFIArg] -> IO () }
|
||||
|
||||
-- | 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 {..} impl tenv = buildFun 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 (argType:argTypes) typesAndVals = PStrict \val ->
|
||||
buildFun argTypes $ typesAndVals ++ [(argType, val)]
|
||||
buildFun [] typesAndVals = PPrim $
|
||||
marshalArgs typesAndVals \inArgs -> do
|
||||
tyArgs <- traverse marshalTyArg ffiTParams
|
||||
let tyInArgs = tyArgs ++ inArgs
|
||||
marshalRet ffiRetType GetRet
|
||||
{ getRetAsValue = callForeignImpl impl tyInArgs
|
||||
, getRetAsOutArgs = callForeignImpl impl . (tyInArgs ++) }
|
||||
|
||||
-- Look up the value of a type parameter in the type environment and marshal
|
||||
-- it.
|
||||
marshalTyArg :: TParam -> Eval SomeFFIArg
|
||||
marshalTyArg tp
|
||||
| n <= toInteger (maxBound :: CSize) =
|
||||
pure $ SomeFFIArg @CSize $ fromInteger n
|
||||
| otherwise = raiseError Concrete $ FFITypeNumTooBig name tp n
|
||||
where n = evalFinType $ TVar $ TVBound 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 FFIBool val f = f [SomeFFIArg @Word8 $ fromBool $ fromVBit val]
|
||||
marshalArg (FFIBasic t) val f = getMarshalBasicArg t \m -> do
|
||||
arg <- m val
|
||||
f [SomeFFIArg arg]
|
||||
marshalArg (FFIArray (evalFinType -> n) t) val f =
|
||||
getMarshalBasicArg t \m -> do
|
||||
args <- traverse (>>= m) $ enumerateSeqMap n $ fromVSeq val
|
||||
-- Since we need to do an Eval action in an IO callback, we need to
|
||||
-- manually unwrap and wrap the Eval datatype
|
||||
Eval \stk ->
|
||||
withArray args \ptr ->
|
||||
runEval stk $ f [SomeFFIArg ptr]
|
||||
marshalArg (FFITuple types) val f = do
|
||||
vals <- sequence $ fromVTuple val
|
||||
marshalArgs (zip types vals) f
|
||||
marshalArg (FFIRecord typeMap) val f = do
|
||||
vals <- traverse (`lookupRecord` val) $ displayOrder typeMap
|
||||
marshalArgs (zip (displayElements typeMap) vals) 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 typesAndVals f = go typesAndVals []
|
||||
where go [] args = f args
|
||||
go ((t, v):tvs) prevArgs = marshalArg t v \currArgs ->
|
||||
go tvs (prevArgs ++ currArgs)
|
||||
|
||||
-- Given a 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 FFIBool gr = VBit . toBool <$> io (getRetAsValue gr @Word8)
|
||||
marshalRet (FFIBasic t) gr = getMarshalBasicRet t (io (getRetAsValue gr) >>=)
|
||||
marshalRet (FFIArray (evalFinType -> n) t) gr = getMarshalBasicRet t \m ->
|
||||
fmap (VSeq n . finiteSeqMap Concrete . map m) $
|
||||
io $ allocaArray (fromInteger n) \ptr -> do
|
||||
getRetAsOutArgs gr [SomeFFIArg ptr]
|
||||
peekArray (fromInteger n) ptr
|
||||
marshalRet (FFITuple types) gr = VTuple <$> marshalMultiRet types gr
|
||||
marshalRet (FFIRecord typeMap) gr =
|
||||
VRecord . recordFromFields . zip (displayOrder typeMap) <$>
|
||||
marshalMultiRet (displayElements typeMap) 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 types gr = Eval \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.
|
||||
vals <- newIORef []
|
||||
let go [] args = getRetAsOutArgs gr args
|
||||
go (t:ts) prevArgs = do
|
||||
val <- runEval stk $ marshalRet t $ getRetFromAsOutArgs \currArgs ->
|
||||
go ts (prevArgs ++ currArgs)
|
||||
modifyIORef' vals (val :)
|
||||
go types []
|
||||
map pure <$> readIORef vals
|
||||
|
||||
-- Evaluate a finite numeric type expression.
|
||||
evalFinType :: Type -> Integer
|
||||
evalFinType = finNat' . evalNumType 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 f = GetRet
|
||||
{ getRetAsValue = alloca \ptr -> do
|
||||
f [SomeFFIArg ptr]
|
||||
peek ptr
|
||||
, getRetAsOutArgs = f }
|
||||
|
||||
-- | Given a 'FFIBasicType', call the callback with a marshalling function that
|
||||
-- marshals values to the 'FFIArg' type corresponding to the 'FFIBasicType'.
|
||||
-- The callback must be able to handle marshalling functions that marshal to any
|
||||
-- 'FFIArg' type.
|
||||
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
|
||||
where toDouble = fst . bfToDouble NearEven . bfValue . fromVFloat
|
||||
|
||||
-- | Given a 'FFIBasicType', call the callback with an unmarshalling function
|
||||
-- from the 'FFIRet' type corresponding to the 'FFIBasicType' to Cryptol values.
|
||||
-- The callback must be able to handle unmarshalling functions from any 'FFIRet'
|
||||
-- type.
|
||||
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
|
||||
where toValue = pure . VFloat . BF e p . 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 FFIWord8 f = f $ Proxy @Word8
|
||||
withWordType FFIWord16 f = f $ Proxy @Word16
|
||||
withWordType FFIWord32 f = f $ Proxy @Word32
|
||||
withWordType FFIWord64 f = f $ Proxy @Word64
|
||||
|
||||
#else
|
||||
|
||||
-- | Dummy implementation for when FFI is disabled. Does not add anything to
|
||||
-- the environment.
|
||||
evalForeignDecls :: ModulePath -> Module -> EvalEnv ->
|
||||
Eval (Either [FFILoadError] (ForeignSrc, EvalEnv))
|
||||
evalForeignDecls _ _ _ = pure $ Left []
|
||||
|
||||
#endif
|
||||
@ -511,8 +511,9 @@ the new bindings.
|
||||
> evalDecl :: Env -> Decl -> (Name, E Value)
|
||||
> evalDecl env d =
|
||||
> case dDefinition d of
|
||||
> DPrim -> (dName d, pure (evalPrim (dName d)))
|
||||
> DExpr e -> (dName d, evalExpr env e)
|
||||
> DPrim -> (dName d, pure (evalPrim (dName d)))
|
||||
> DForeign _ -> (dName d, cryError $ FFINotSupported $ dName d)
|
||||
> DExpr e -> (dName d, evalExpr env e)
|
||||
>
|
||||
|
||||
Newtypes
|
||||
|
||||
@ -93,6 +93,7 @@ instance FreeVars Decl where
|
||||
instance FreeVars DeclDef where
|
||||
freeVars d = case d of
|
||||
DPrim -> mempty
|
||||
DForeign _ -> mempty
|
||||
DExpr e -> freeVars e
|
||||
|
||||
|
||||
|
||||
@ -64,8 +64,9 @@ findModule n env = runModuleM env (Base.findModule n)
|
||||
|
||||
-- | Load the module contained in the given file.
|
||||
loadModuleByPath :: FilePath -> ModuleCmd (ModulePath,T.Module)
|
||||
loadModuleByPath path minp =
|
||||
runModuleM minp{ minpModuleEnv = resetModuleEnv (minpModuleEnv minp) } $ do
|
||||
loadModuleByPath path minp = do
|
||||
moduleEnv' <- resetModuleEnv $ minpModuleEnv minp
|
||||
runModuleM minp{ minpModuleEnv = moduleEnv' } $ do
|
||||
unloadModule ((InFile path ==) . lmFilePath)
|
||||
m <- Base.loadModuleByPath path
|
||||
setFocusedModule (T.mName m)
|
||||
@ -73,8 +74,9 @@ loadModuleByPath path minp =
|
||||
|
||||
-- | Load the given parsed module.
|
||||
loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.Module)
|
||||
loadModuleByName n minp =
|
||||
runModuleM minp{ minpModuleEnv = resetModuleEnv (minpModuleEnv minp) } $ do
|
||||
loadModuleByName n minp = do
|
||||
moduleEnv' <- resetModuleEnv $ minpModuleEnv minp
|
||||
runModuleM minp{ minpModuleEnv = moduleEnv' } $ do
|
||||
unloadModule ((n ==) . lmName)
|
||||
(path,m') <- Base.loadModuleFrom False (FromModule n)
|
||||
setFocusedModule (T.mName m')
|
||||
|
||||
@ -11,6 +11,7 @@
|
||||
|
||||
{-# LANGUAGE FlexibleContexts #-}
|
||||
{-# LANGUAGE ImplicitParams #-}
|
||||
{-# LANGUAGE LambdaCase #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
@ -18,6 +19,7 @@ module Cryptol.ModuleSystem.Base where
|
||||
|
||||
import qualified Control.Exception as X
|
||||
import Control.Monad (unless,when)
|
||||
import Data.Functor.Compose
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Monoid ((<>))
|
||||
import Data.Text.Encoding (decodeUtf8')
|
||||
@ -52,6 +54,7 @@ import Cryptol.ModuleSystem.Env (lookupModule
|
||||
import qualified Cryptol.Eval as E
|
||||
import qualified Cryptol.Eval.Concrete as Concrete
|
||||
import Cryptol.Eval.Concrete (Concrete(..))
|
||||
import Cryptol.Eval.FFI
|
||||
import qualified Cryptol.ModuleSystem.NamingEnv as R
|
||||
import qualified Cryptol.ModuleSystem.Renamer as R
|
||||
import qualified Cryptol.Parser as P
|
||||
@ -248,8 +251,17 @@ doLoadModule quiet isrc path fp pm0 =
|
||||
let ?evalPrim = \i -> Right <$> Map.lookup i tbl
|
||||
callStacks <- getCallStacks
|
||||
let ?callStacks = callStacks
|
||||
unless (T.isParametrizedModule tcm) $ modifyEvalEnv (E.moduleEnv Concrete tcm)
|
||||
loadedModule path fp nameEnv tcm
|
||||
foreignSrc <-
|
||||
if T.isParametrizedModule tcm
|
||||
then pure Nothing
|
||||
else (getCompose
|
||||
<$> modifyEvalEnvM (fmap Compose . evalForeignDecls path tcm)
|
||||
>>= \case
|
||||
Left [] -> pure Nothing
|
||||
Left errs -> ffiLoadErrors (T.mName tcm) errs
|
||||
Right (foreignSrc, ()) -> pure (Just foreignSrc))
|
||||
<* modifyEvalEnv (E.moduleEnv Concrete tcm)
|
||||
loadedModule path fp nameEnv foreignSrc tcm
|
||||
|
||||
return tcm
|
||||
where
|
||||
|
||||
@ -18,6 +18,7 @@ module Cryptol.ModuleSystem.Env where
|
||||
import Paths_cryptol (getDataDir)
|
||||
#endif
|
||||
|
||||
import Cryptol.Backend.FFI (ForeignSrc, unloadForeignSrc)
|
||||
import Cryptol.Eval (EvalEnv)
|
||||
import Cryptol.ModuleSystem.Fingerprint
|
||||
import Cryptol.ModuleSystem.Interface
|
||||
@ -41,6 +42,7 @@ import System.Directory (getAppUserDataDirectory, getCurrentDirectory)
|
||||
import System.Environment(getExecutablePath)
|
||||
import System.FilePath ((</>), normalise, joinPath, splitPath, takeDirectory)
|
||||
import qualified Data.List as List
|
||||
import Data.Foldable
|
||||
|
||||
import GHC.Generics (Generic)
|
||||
import Control.DeepSeq
|
||||
@ -99,14 +101,19 @@ data CoreLint = NoCoreLint -- ^ Don't run core lint
|
||||
| CoreLint -- ^ Run core lint
|
||||
deriving (Generic, NFData)
|
||||
|
||||
resetModuleEnv :: ModuleEnv -> ModuleEnv
|
||||
resetModuleEnv env = env
|
||||
{ meLoadedModules = mempty
|
||||
, meNameSeeds = T.nameSeeds
|
||||
, meEvalEnv = mempty
|
||||
, meFocusedModule = Nothing
|
||||
, meDynEnv = mempty
|
||||
}
|
||||
resetModuleEnv :: ModuleEnv -> IO ModuleEnv
|
||||
resetModuleEnv env = do
|
||||
for_ (getLoadedModules $ meLoadedModules env) $ \lm ->
|
||||
case lmForeignSrc lm of
|
||||
Just fsrc -> unloadForeignSrc fsrc
|
||||
_ -> pure ()
|
||||
pure env
|
||||
{ meLoadedModules = mempty
|
||||
, meNameSeeds = T.nameSeeds
|
||||
, meEvalEnv = mempty
|
||||
, meFocusedModule = Nothing
|
||||
, meDynEnv = mempty
|
||||
}
|
||||
|
||||
initialModuleEnv :: IO ModuleEnv
|
||||
initialModuleEnv = do
|
||||
@ -342,6 +349,9 @@ data LoadedModule = LoadedModule
|
||||
-- ^ The actual type-checked module
|
||||
|
||||
, lmFingerprint :: Fingerprint
|
||||
|
||||
, lmForeignSrc :: Maybe ForeignSrc
|
||||
-- ^ The dynamically loaded source for any foreign functions in the module
|
||||
} deriving (Show, Generic, NFData)
|
||||
|
||||
-- | Has this module been loaded already.
|
||||
@ -362,9 +372,9 @@ lookupModule mn me = search lmLoadedModules `mplus` search lmLoadedParamModules
|
||||
-- | Add a freshly loaded module. If it was previously loaded, then
|
||||
-- the new version is ignored.
|
||||
addLoadedModule ::
|
||||
ModulePath -> String -> Fingerprint -> R.NamingEnv -> T.Module ->
|
||||
LoadedModules -> LoadedModules
|
||||
addLoadedModule path ident fp nameEnv tm lm
|
||||
ModulePath -> String -> Fingerprint -> R.NamingEnv -> Maybe ForeignSrc ->
|
||||
T.Module -> LoadedModules -> LoadedModules
|
||||
addLoadedModule path ident fp nameEnv fsrc tm lm
|
||||
| isLoaded (T.mName tm) lm = lm
|
||||
| T.isParametrizedModule tm = lm { lmLoadedParamModules = loaded :
|
||||
lmLoadedParamModules lm }
|
||||
@ -379,6 +389,7 @@ addLoadedModule path ident fp nameEnv tm lm
|
||||
, lmInterface = T.genIface tm
|
||||
, lmModule = tm
|
||||
, lmFingerprint = fp
|
||||
, lmForeignSrc = fsrc
|
||||
}
|
||||
|
||||
-- | Remove a previously loaded module.
|
||||
|
||||
@ -231,8 +231,9 @@ instance Inst DeclGroup where
|
||||
instance Inst DeclDef where
|
||||
inst env d =
|
||||
case d of
|
||||
DPrim -> DPrim
|
||||
DExpr e -> DExpr (inst env e)
|
||||
DPrim -> DPrim
|
||||
DForeign t -> DForeign t
|
||||
DExpr e -> DExpr (inst env e)
|
||||
|
||||
instance Inst Decl where
|
||||
inst env d = d { dSignature = inst env (dSignature d)
|
||||
|
||||
@ -14,6 +14,8 @@ module Cryptol.ModuleSystem.Monad where
|
||||
|
||||
import Cryptol.Eval (EvalEnv,EvalOpts(..))
|
||||
|
||||
import Cryptol.Backend.FFI (ForeignSrc)
|
||||
import Cryptol.Backend.FFI.Error
|
||||
import qualified Cryptol.Backend.Monad as E
|
||||
|
||||
import Cryptol.ModuleSystem.Env
|
||||
@ -43,9 +45,11 @@ import Control.Monad.IO.Class
|
||||
import Control.Exception (IOException)
|
||||
import Data.ByteString (ByteString)
|
||||
import Data.Function (on)
|
||||
import Data.Functor.Identity
|
||||
import Data.Map (Map)
|
||||
import Data.Maybe (isJust)
|
||||
import Data.Text.Encoding.Error (UnicodeException)
|
||||
import Data.Traversable
|
||||
import MonadLib
|
||||
import System.Directory (canonicalizePath)
|
||||
|
||||
@ -116,6 +120,8 @@ data ModuleError
|
||||
| FailedToParameterizeModDefs P.ModName [T.Name]
|
||||
-- ^ Failed to add the module parameters to all definitions in a module.
|
||||
| NotAParameterizedModule P.ModName
|
||||
| FFILoadErrors P.ModName [FFILoadError]
|
||||
-- ^ Errors loading foreign function implementations
|
||||
|
||||
| ErrorInFile ModulePath ModuleError
|
||||
-- ^ This is just a tag on the error, indicating the file containing it.
|
||||
@ -145,6 +151,7 @@ instance NFData ModuleError where
|
||||
ImportedParamModule x -> x `deepseq` ()
|
||||
FailedToParameterizeModDefs x xs -> x `deepseq` xs `deepseq` ()
|
||||
NotAParameterizedModule x -> x `deepseq` ()
|
||||
FFILoadErrors x errs -> x `deepseq` errs `deepseq` ()
|
||||
ErrorInFile x y -> x `deepseq` y `deepseq` ()
|
||||
|
||||
instance PP ModuleError where
|
||||
@ -213,6 +220,11 @@ instance PP ModuleError where
|
||||
NotAParameterizedModule x ->
|
||||
text "[error] Module" <+> pp x <+> text "does not have parameters."
|
||||
|
||||
FFILoadErrors x errs ->
|
||||
hang (text "[error] Failed to load foreign implementations for module"
|
||||
<+> pp x <.> colon)
|
||||
4 (vcat $ map pp errs)
|
||||
|
||||
ErrorInFile _ x -> ppPrec prec x
|
||||
|
||||
moduleNotFound :: P.ModName -> [FilePath] -> ModuleM a
|
||||
@ -277,6 +289,9 @@ failedToParameterizeModDefs x xs =
|
||||
notAParameterizedModule :: P.ModName -> ModuleM a
|
||||
notAParameterizedModule x = ModuleT (raise (NotAParameterizedModule x))
|
||||
|
||||
ffiLoadErrors :: P.ModName -> [FFILoadError] -> ModuleM a
|
||||
ffiLoadErrors x errs = ModuleT (raise (FFILoadErrors x errs))
|
||||
|
||||
-- | Run the computation, and if it caused and error, tag the error
|
||||
-- with the given file.
|
||||
errorInFile :: ModulePath -> ModuleM a -> ModuleM a
|
||||
@ -522,22 +537,27 @@ unloadModule rm = ModuleT $ do
|
||||
set $! env { meLoadedModules = removeLoadedModule rm (meLoadedModules env) }
|
||||
|
||||
loadedModule ::
|
||||
ModulePath -> Fingerprint -> NamingEnv -> T.Module -> ModuleM ()
|
||||
loadedModule path fp nameEnv m = ModuleT $ do
|
||||
ModulePath -> Fingerprint -> NamingEnv -> Maybe ForeignSrc -> T.Module ->
|
||||
ModuleM ()
|
||||
loadedModule path fp nameEnv fsrc m = ModuleT $ do
|
||||
env <- get
|
||||
ident <- case path of
|
||||
InFile p -> unModuleT $ io (canonicalizePath p)
|
||||
InMem l _ -> pure l
|
||||
|
||||
set $! env { meLoadedModules = addLoadedModule path ident fp nameEnv m
|
||||
set $! env { meLoadedModules = addLoadedModule path ident fp nameEnv fsrc m
|
||||
(meLoadedModules env) }
|
||||
|
||||
modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM ()
|
||||
modifyEvalEnv f = ModuleT $ do
|
||||
modifyEvalEnvM :: Traversable t =>
|
||||
(EvalEnv -> E.Eval (t EvalEnv)) -> ModuleM (t ())
|
||||
modifyEvalEnvM f = ModuleT $ do
|
||||
env <- get
|
||||
let evalEnv = meEvalEnv env
|
||||
evalEnv' <- inBase $ E.runEval mempty (f evalEnv)
|
||||
set $! env { meEvalEnv = evalEnv' }
|
||||
inBase (E.runEval mempty (f evalEnv))
|
||||
>>= traverse (\evalEnv' -> set $! env { meEvalEnv = evalEnv' })
|
||||
|
||||
modifyEvalEnv :: (EvalEnv -> E.Eval EvalEnv) -> ModuleM ()
|
||||
modifyEvalEnv = fmap runIdentity . modifyEvalEnvM . (fmap Identity .)
|
||||
|
||||
getEvalEnv :: ModuleM EvalEnv
|
||||
getEvalEnv = ModuleT (meEvalEnv `fmap` get)
|
||||
|
||||
@ -683,6 +683,7 @@ instance Rename Bind where
|
||||
|
||||
instance Rename BindDef where
|
||||
rename DPrim = return DPrim
|
||||
rename DForeign = return DForeign
|
||||
rename (DExpr e) = DExpr <$> rename e
|
||||
rename (DPropGuards cases) = DPropGuards <$> traverse renameCase cases
|
||||
where
|
||||
|
||||
@ -90,6 +90,7 @@ import Paths_cryptol
|
||||
|
||||
'primitive' { Located $$ (Token (KW KW_primitive) _)}
|
||||
'constraint'{ Located $$ (Token (KW KW_constraint) _)}
|
||||
'foreign' { Located $$ (Token (KW KW_foreign) _)}
|
||||
'Prop' { Located $$ (Token (KW KW_Prop) _)}
|
||||
|
||||
'[' { Located $$ (Token (Sym BracketL) _)}
|
||||
@ -251,6 +252,7 @@ vtop_decl :: { [TopDecl PName] }
|
||||
{ [exportDecl $1 Public (mkProperty $3 [] $5)] }
|
||||
| mbDoc newtype { [exportNewtype Public $1 $2] }
|
||||
| prim_bind { $1 }
|
||||
| foreign_bind { $1 }
|
||||
| private_decls { $1 }
|
||||
| parameter_decls { $1 }
|
||||
| mbDoc 'submodule'
|
||||
@ -273,6 +275,8 @@ prim_bind :: { [TopDecl PName] }
|
||||
| mbDoc 'primitive' '(' op ')' ':' schema { mkPrimDecl $1 $4 $7 }
|
||||
| mbDoc 'primitive' 'type' schema ':' kind {% mkPrimTypeDecl $1 $4 $6 }
|
||||
|
||||
foreign_bind :: { [TopDecl PName] }
|
||||
: mbDoc 'foreign' name ':' schema { mkForeignDecl $1 $3 $5 }
|
||||
|
||||
parameter_decls :: { [TopDecl PName] }
|
||||
: 'parameter' 'v{' par_decls 'v}' { reverse $3 }
|
||||
|
||||
@ -279,6 +279,7 @@ data Bind name = Bind
|
||||
type LBindDef = Located (BindDef PName)
|
||||
|
||||
data BindDef name = DPrim
|
||||
| DForeign
|
||||
| DExpr (Expr name)
|
||||
| DPropGuards [([Prop name], Expr name)]
|
||||
deriving (Eq, Show, Generic, NFData, Functor)
|
||||
@ -727,6 +728,7 @@ instance (Show name, PPName name) => PP (Bind name) where
|
||||
|
||||
instance (Show name, PPName name) => PP (BindDef name) where
|
||||
ppPrec _ DPrim = text "<primitive>"
|
||||
ppPrec _ DForeign = text "<foreign>"
|
||||
ppPrec p (DExpr e) = ppPrec p e
|
||||
ppPrec _p (DPropGuards _guards) = text "propguards"
|
||||
|
||||
|
||||
@ -126,6 +126,7 @@ $white+ { emit $ White Space }
|
||||
"primitive" { emit $ KW KW_primitive }
|
||||
"parameter" { emit $ KW KW_parameter }
|
||||
"constraint" { emit $ KW KW_constraint }
|
||||
"foreign" { emit $ KW KW_foreign }
|
||||
|
||||
"Prop" { emit $ KW KW_Prop }
|
||||
|
||||
|
||||
@ -65,6 +65,7 @@ namesB b =
|
||||
|
||||
namesDef :: Ord name => BindDef name -> Set name
|
||||
namesDef DPrim = Set.empty
|
||||
namesDef DForeign = Set.empty
|
||||
namesDef (DExpr e) = namesE e
|
||||
namesDef (DPropGuards guards) = mconcat . fmap (\(_props, e) -> namesE e) $ guards
|
||||
|
||||
@ -186,6 +187,7 @@ tnamesB b = Set.unions [setS, setP, setE]
|
||||
|
||||
tnamesDef :: Ord name => BindDef name -> Set name
|
||||
tnamesDef DPrim = Set.empty
|
||||
tnamesDef DForeign = Set.empty
|
||||
tnamesDef (DExpr e) = tnamesE e
|
||||
tnamesDef (DPropGuards guards) = mconcat . fmap (\(_props, e) -> tnamesE e) $ guards
|
||||
|
||||
|
||||
@ -219,6 +219,11 @@ noMatchB b =
|
||||
| otherwise -> panic "NoPat" [ "noMatchB: primitive with params"
|
||||
, show b ]
|
||||
|
||||
DForeign
|
||||
| null (bParams b) -> return b
|
||||
| otherwise -> panic "NoPat" [ "noMatchB: foreign with params"
|
||||
, show b ]
|
||||
|
||||
DExpr e ->
|
||||
do e' <- noPatFun (Just (thing (bName b))) 0 (bParams b) e
|
||||
return b { bParams = [], bDef = DExpr e' <$ bDef b }
|
||||
|
||||
@ -645,19 +645,26 @@ mkIf ifThens theElse = foldr addIfThen theElse ifThens
|
||||
where
|
||||
addIfThen (cond, doexpr) elseExpr = EIf cond doexpr elseExpr
|
||||
|
||||
-- | Generate a signature and a primitive binding. The reason for generating
|
||||
-- both instead of just adding the signature at this point is that it means the
|
||||
-- primitive declarations don't need to be treated differently in the noPat
|
||||
mkPrimDecl :: Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName]
|
||||
mkPrimDecl = mkNoImplDecl DPrim
|
||||
|
||||
mkForeignDecl :: Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName]
|
||||
mkForeignDecl = mkNoImplDecl DForeign
|
||||
|
||||
-- | Generate a signature and a binding for value declarations with no
|
||||
-- implementation (i.e. primitive or foreign declarations). The reason for
|
||||
-- generating both instead of just adding the signature at this point is that it
|
||||
-- means the declarations don't need to be treated differently in the noPat
|
||||
-- pass. This is also the reason we add the doc to the TopLevel constructor,
|
||||
-- instead of just place it on the binding directly. A better solution might be
|
||||
-- to just have a different constructor for primitives.
|
||||
mkPrimDecl ::
|
||||
Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName]
|
||||
mkPrimDecl mbDoc ln sig =
|
||||
-- to just have a different constructor for primitives and foreigns.
|
||||
mkNoImplDecl :: BindDef PName
|
||||
-> Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName]
|
||||
mkNoImplDecl def mbDoc ln sig =
|
||||
[ exportDecl mbDoc Public
|
||||
$ DBind Bind { bName = ln
|
||||
, bParams = []
|
||||
, bDef = at sig (Located emptyRange DPrim)
|
||||
, bDef = at sig (Located emptyRange def)
|
||||
, bSignature = Nothing
|
||||
, bPragmas = []
|
||||
, bMono = False
|
||||
|
||||
@ -37,6 +37,11 @@ data Range = Range { from :: !Position
|
||||
, source :: FilePath }
|
||||
deriving (Eq, Ord, Show, Generic, NFData)
|
||||
|
||||
-- | Returns `True` if the first range is contained in the second one.
|
||||
rangeWithin :: Range -> Range -> Bool
|
||||
a `rangeWithin` b =
|
||||
source a == source b && from a >= from b && to a <= to b
|
||||
|
||||
-- | An empty range.
|
||||
--
|
||||
-- Caution: using this on the LHS of a use of rComb will cause the empty source
|
||||
|
||||
@ -51,6 +51,7 @@ data TokenKW = KW_else
|
||||
| KW_primitive
|
||||
| KW_parameter
|
||||
| KW_constraint
|
||||
| KW_foreign
|
||||
| KW_Prop
|
||||
| KW_by
|
||||
| KW_down
|
||||
|
||||
@ -147,11 +147,12 @@ instance AddParams DeclGroup where
|
||||
instance AddParams Decl where
|
||||
addParams ps d =
|
||||
case dDefinition d of
|
||||
DPrim -> 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
|
||||
@ -280,6 +281,7 @@ instance Inst DeclDef where
|
||||
inst ps d =
|
||||
case d of
|
||||
DPrim -> DPrim
|
||||
DForeign t -> DForeign t
|
||||
DExpr e -> DExpr (inst ps e)
|
||||
|
||||
instance Inst Type where
|
||||
|
||||
@ -218,8 +218,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 rews (DExpr e) = DExpr <$> rewE rews e
|
||||
rewDef _ DPrim = return DPrim
|
||||
rewDef _ (DForeign t) = return $ DForeign t
|
||||
|
||||
rewDeclGroup :: RewMap -> DeclGroup -> M DeclGroup
|
||||
rewDeclGroup rews dg =
|
||||
@ -239,11 +240,12 @@ rewDeclGroup rews dg =
|
||||
|
||||
consider d =
|
||||
case dDefinition d of
|
||||
DPrim -> 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) ->
|
||||
|
||||
@ -188,9 +188,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
|
||||
DExpr e -> do e' <- specializeExpr =<< instantiateExpr ts n e
|
||||
return (DExpr e')
|
||||
DPrim -> return DPrim
|
||||
DForeign t -> return $ DForeign t
|
||||
let decl' = decl { dName = qname', dSignature = sig', dDefinition = rhs' }
|
||||
modifySpecCache (Map.adjust (fmap (insertTM ts (qname', Just decl'))) qname)
|
||||
return (EVar qname')
|
||||
|
||||
@ -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.FFIType
|
||||
import Cryptol.TypeCheck.PP
|
||||
import Cryptol.TypeCheck.Type
|
||||
|
||||
@ -180,6 +181,7 @@ data Decl = Decl { dName :: !Name
|
||||
} deriving (Generic, NFData, Show)
|
||||
|
||||
data DeclDef = DPrim
|
||||
| DForeign FFIFunType
|
||||
| DExpr Expr
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
@ -375,8 +377,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 (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
|
||||
|
||||
@ -13,12 +13,13 @@ import Data.List((\\),sortBy,groupBy,partition)
|
||||
import Data.Function(on)
|
||||
|
||||
import qualified Cryptol.Parser.AST as P
|
||||
import Cryptol.Parser.Position(Located(..), Range(..))
|
||||
import Cryptol.Parser.Position(Located(..), Range(..), rangeWithin)
|
||||
import Cryptol.TypeCheck.PP
|
||||
import Cryptol.TypeCheck.Type
|
||||
import Cryptol.TypeCheck.InferTypes
|
||||
import Cryptol.TypeCheck.Subst
|
||||
import Cryptol.TypeCheck.Unify(Path,isRootPath)
|
||||
import Cryptol.TypeCheck.FFI.Error
|
||||
import Cryptol.ModuleSystem.Name(Name)
|
||||
import Cryptol.Utils.Ident(Ident)
|
||||
import Cryptol.Utils.RecordMap
|
||||
@ -56,6 +57,8 @@ cleanupErrors = dropErrorsFromSameLoc
|
||||
-- | Should the first error suppress the next one.
|
||||
subsumes :: (Range,Error) -> (Range,Error) -> Bool
|
||||
subsumes (_,NotForAll _ _ x _) (_,NotForAll _ _ y _) = x == y
|
||||
subsumes (r1,UnexpectedTypeWildCard) (r2,UnsupportedFFIType{}) =
|
||||
r1 `rangeWithin` r2
|
||||
subsumes (r1,KindMismatch {}) (r2,err) =
|
||||
case err of
|
||||
KindMismatch {} -> r1 == r2
|
||||
@ -144,6 +147,11 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind
|
||||
| MissingModTParam (Located Ident)
|
||||
| MissingModVParam (Located Ident)
|
||||
|
||||
| UnsupportedFFIKind TypeSource TParam Kind
|
||||
-- ^ Kind is not supported for FFI
|
||||
| UnsupportedFFIType TypeSource FFITypeError
|
||||
-- ^ Type is not supported for FFI
|
||||
|
||||
| TemporaryError Doc
|
||||
-- ^ This is for errors that don't fit other cateogories.
|
||||
-- We should not use it much, and is generally to be used
|
||||
@ -200,7 +208,9 @@ errorImportance err =
|
||||
|
||||
AmbiguousSize {} -> 2
|
||||
|
||||
|
||||
UnsupportedFFIKind {} -> 10
|
||||
UnsupportedFFIType {} -> 7
|
||||
-- less than UnexpectedTypeWildCard
|
||||
|
||||
|
||||
instance TVars Warning where
|
||||
@ -252,6 +262,9 @@ instance TVars Error where
|
||||
MissingModTParam {} -> err
|
||||
MissingModVParam {} -> err
|
||||
|
||||
UnsupportedFFIKind {} -> err
|
||||
UnsupportedFFIType src e -> UnsupportedFFIType src !$ apSubst su e
|
||||
|
||||
TemporaryError {} -> err
|
||||
|
||||
|
||||
@ -287,6 +300,9 @@ instance FVS Error where
|
||||
MissingModTParam {} -> Set.empty
|
||||
MissingModVParam {} -> Set.empty
|
||||
|
||||
UnsupportedFFIKind {} -> Set.empty
|
||||
UnsupportedFFIType _ t -> fvs t
|
||||
|
||||
TemporaryError {} -> Set.empty
|
||||
|
||||
instance PP Warning where
|
||||
@ -329,7 +345,7 @@ instance PP (WithNames Error) where
|
||||
UnexpectedTypeWildCard ->
|
||||
addTVarsDescsAfter names err $
|
||||
nested "Wild card types are not allowed in this context"
|
||||
"(e.g., they cannot be used in type synonyms)."
|
||||
"(e.g., they cannot be used in type synonyms or FFI declarations)."
|
||||
|
||||
KindMismatch mbsrc k1 k2 ->
|
||||
addTVarsDescsAfter names err $
|
||||
@ -464,6 +480,17 @@ instance PP (WithNames Error) where
|
||||
MissingModVParam x ->
|
||||
"Missing definition for value parameter" <+> quotes (pp (thing x))
|
||||
|
||||
UnsupportedFFIKind src param k ->
|
||||
nested "Kind of type variable unsupported for FFI: " $
|
||||
vcat
|
||||
[ pp param <+> colon <+> pp k
|
||||
, "Only type variables of kind" <+> pp KNum <+> "are supported"
|
||||
, "When checking" <+> pp src ]
|
||||
|
||||
UnsupportedFFIType src t -> vcat
|
||||
[ ppWithNames names t
|
||||
, "When checking" <+> pp src ]
|
||||
|
||||
TemporaryError doc -> doc
|
||||
where
|
||||
bullets xs = vcat [ "•" <+> d | d <- xs ]
|
||||
|
||||
102
src/Cryptol/TypeCheck/FFI.hs
Normal file
102
src/Cryptol/TypeCheck/FFI.hs
Normal file
@ -0,0 +1,102 @@
|
||||
{-# LANGUAGE BlockArguments #-}
|
||||
{-# LANGUAGE RecordWildCards #-}
|
||||
{-# LANGUAGE ViewPatterns #-}
|
||||
|
||||
-- | Checking and conversion of 'Type's to 'FFIType's.
|
||||
module Cryptol.TypeCheck.FFI
|
||||
( toFFIFunType
|
||||
) where
|
||||
|
||||
import Data.Containers.ListUtils
|
||||
import Data.Either
|
||||
|
||||
import Cryptol.TypeCheck.FFI.Error
|
||||
import Cryptol.TypeCheck.FFI.FFIType
|
||||
import Cryptol.TypeCheck.SimpType
|
||||
import Cryptol.TypeCheck.Type
|
||||
import Cryptol.Utils.RecordMap
|
||||
|
||||
-- | Convert a 'Schema' to a 'FFIFunType', along with any 'Prop's that must be
|
||||
-- satisfied for the 'FFIFunType' to be valid.
|
||||
toFFIFunType :: Schema -> Either FFITypeError ([Prop], FFIFunType)
|
||||
toFFIFunType (Forall params _ t) =
|
||||
-- Remove all type synonyms and simplify the type before processing it
|
||||
case go $ tRebuild' False t of
|
||||
Just (Right (props, fft)) -> Right
|
||||
-- Remove duplicate constraints
|
||||
(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']
|
||||
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
|
||||
|
||||
-- | 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
|
||||
|
||||
fin :: Type -> Prop
|
||||
fin t = TCon (PC PFin) [t]
|
||||
81
src/Cryptol/TypeCheck/FFI/Error.hs
Normal file
81
src/Cryptol/TypeCheck/FFI/Error.hs
Normal file
@ -0,0 +1,81 @@
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
{-# LANGUAGE FlexibleInstances #-}
|
||||
{-# LANGUAGE OverloadedStrings #-}
|
||||
|
||||
-- | Errors from typechecking foreign functions.
|
||||
module Cryptol.TypeCheck.FFI.Error where
|
||||
|
||||
import Control.DeepSeq
|
||||
import GHC.Generics
|
||||
|
||||
import Cryptol.TypeCheck.PP
|
||||
import Cryptol.TypeCheck.Subst
|
||||
import Cryptol.TypeCheck.Type
|
||||
|
||||
data FFITypeError = FFITypeError Type FFITypeErrorReason
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
data FFITypeErrorReason
|
||||
= FFIBadWordSize
|
||||
| FFIBadFloatSize
|
||||
| FFIBadArrayType
|
||||
| FFIBadComponentTypes [FFITypeError]
|
||||
| FFIBadType
|
||||
| FFINotFunction
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
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
|
||||
|
||||
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
|
||||
|
||||
instance PP (WithNames FFITypeError) where
|
||||
ppPrec _ (WithNames (FFITypeError t r) names) =
|
||||
nest 2 $ "Type unsupported for FFI:" $$
|
||||
vcat
|
||||
[ ppWithNames names t
|
||||
, "Due to:"
|
||||
, 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"
|
||||
57
src/Cryptol/TypeCheck/FFI/FFIType.hs
Normal file
57
src/Cryptol/TypeCheck/FFI/FFIType.hs
Normal file
@ -0,0 +1,57 @@
|
||||
{-# LANGUAGE DeriveAnyClass #-}
|
||||
{-# LANGUAGE DeriveGeneric #-}
|
||||
|
||||
-- | This module defines a nicer intermediate representation of Cryptol types
|
||||
-- allowed for the FFI, which the typechecker generates then stores in the AST.
|
||||
-- This way the FFI evaluation code does not have to examine the raw type
|
||||
-- signatures again.
|
||||
module Cryptol.TypeCheck.FFI.FFIType where
|
||||
|
||||
import Control.DeepSeq
|
||||
import GHC.Generics
|
||||
|
||||
import Cryptol.TypeCheck.Type
|
||||
import Cryptol.Utils.Ident
|
||||
import Cryptol.Utils.RecordMap
|
||||
|
||||
-- | Type of a foreign function.
|
||||
data FFIFunType = FFIFunType
|
||||
{ -- | Note: any type variables within this function type must be bound here.
|
||||
ffiTParams :: [TParam]
|
||||
, ffiArgTypes :: [FFIType]
|
||||
, ffiRetType :: FFIType }
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
-- | Type of a value that can be passed to or returned from a foreign function.
|
||||
data FFIType
|
||||
= FFIBool
|
||||
| FFIBasic FFIBasicType
|
||||
| FFIArray
|
||||
Type -- ^ Size (should be of kind @\#@)
|
||||
FFIBasicType -- ^ Element type
|
||||
| FFITuple [FFIType]
|
||||
| FFIRecord (RecordMap Ident FFIType)
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
-- | Types which can be elements of FFI sequences.
|
||||
data FFIBasicType
|
||||
= FFIWord
|
||||
Integer -- ^ The size of the Cryptol type
|
||||
FFIWordSize -- ^ The machine word size that it corresponds to
|
||||
| FFIFloat
|
||||
Integer -- ^ Exponent
|
||||
Integer -- ^ Precision
|
||||
FFIFloatSize -- ^ The machine float size that it corresponds to
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
data FFIWordSize
|
||||
= FFIWord8
|
||||
| FFIWord16
|
||||
| FFIWord32
|
||||
| FFIWord64
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
data FFIFloatSize
|
||||
= FFIFloat32
|
||||
| FFIFloat64
|
||||
deriving (Show, Generic, NFData)
|
||||
@ -52,6 +52,8 @@ 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.TypeCheck.FFI.FFIType
|
||||
import Cryptol.Utils.Ident
|
||||
import Cryptol.Utils.Panic(panic)
|
||||
import Cryptol.Utils.RecordMap
|
||||
@ -66,7 +68,8 @@ import Data.Maybe(isJust, fromMaybe, mapMaybe)
|
||||
import Data.Ratio(numerator,denominator)
|
||||
import Data.Traversable(forM)
|
||||
import Data.Function(on)
|
||||
import Control.Monad(zipWithM,unless,foldM,forM_,mplus, join)
|
||||
import Control.Monad(zipWithM, unless, foldM, forM_, mplus, zipWithM,
|
||||
unless, foldM, forM_, mplus, when)
|
||||
import Data.Bifunctor (Bifunctor(second))
|
||||
|
||||
|
||||
@ -839,7 +842,12 @@ guessType exprMap b@(P.Bind { .. }) =
|
||||
case bSignature of
|
||||
|
||||
Just s ->
|
||||
do s1 <- checkSchema AllowWildCards s
|
||||
do let wildOk = case thing bDef of
|
||||
P.DForeign {} -> NoWildCards
|
||||
P.DPrim -> NoWildCards
|
||||
P.DExpr {} -> AllowWildCards
|
||||
P.DPropGuards {} -> NoWildCards
|
||||
s1 <- checkSchema wildOk s
|
||||
return ((name, ExtVar (fst s1)), Left (checkSigB b s1))
|
||||
|
||||
Nothing
|
||||
@ -933,8 +941,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
|
||||
DExpr e -> DExpr (genE e)
|
||||
DPrim -> DPrim
|
||||
DForeign t -> DForeign t
|
||||
, dSignature = Forall asPs qs
|
||||
$ apSubst su $ sType $ dSignature d
|
||||
}
|
||||
@ -956,6 +965,8 @@ checkMonoB b t =
|
||||
|
||||
P.DPrim -> panic "checkMonoB" ["Primitive with no signature?"]
|
||||
|
||||
P.DForeign -> panic "checkMonoB" ["Foreign with no signature?"]
|
||||
|
||||
P.DExpr e ->
|
||||
do let nm = thing (P.bName b)
|
||||
let tGoal = WithSource t (DefinitionOf nm) (getLoc b)
|
||||
@ -993,6 +1004,37 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
|
||||
, dDoc = P.bDoc b
|
||||
}
|
||||
|
||||
P.DForeign -> do
|
||||
let loc = getLoc b
|
||||
name' = thing $ P.bName b
|
||||
src = DefinitionOf name'
|
||||
inRangeMb loc do
|
||||
-- Ensure all type params are of kind #
|
||||
forM_ as \a ->
|
||||
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 <$ do
|
||||
ffiGoals <- traverse (newGoal (CtFFI name')) props
|
||||
proveImplication True (Just name') as asmps0 $
|
||||
validSchema ++ ffiGoals
|
||||
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
|
||||
, dPragmas = P.bPragmas b
|
||||
, dInfix = P.bInfix b
|
||||
, dFixity = P.bFixity b
|
||||
, dDoc = P.bDoc b
|
||||
}
|
||||
|
||||
P.DExpr e0 ->
|
||||
inRangeMb (getLoc b) $
|
||||
withTParams as $ do
|
||||
@ -1013,7 +1055,6 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
|
||||
withTParams as $ do
|
||||
asmps1 <- applySubstPreds asmps0
|
||||
t1 <- applySubst t0
|
||||
|
||||
-- Checking each guarded case is the same as checking a DExpr, except
|
||||
-- that the guarding assumptions are added first.
|
||||
let checkPropGuardCase :: ([P.Prop Name], P.Expr Name) -> InferM ([Prop], Expr)
|
||||
@ -1028,7 +1069,7 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
|
||||
second concat . unzip <$>
|
||||
checkPropGuard mb_rng `traverse` guards0
|
||||
-- try to prove all goals
|
||||
su <- proveImplication (Just name) as (asmps1 <> guards1) goals
|
||||
su <- proveImplication True (Just name) as (asmps1 <> guards1) goals
|
||||
extendSubst su
|
||||
-- Preprends the goals to the constraints, because these must be
|
||||
-- checked first before the rest of the constraints (during
|
||||
@ -1076,21 +1117,21 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
|
||||
panicInvalid = tcPanic "checkSigB"
|
||||
[ "This type shouldn't be a valid type constraint: " ++
|
||||
"`" ++ pretty prop ++ "`"]
|
||||
|
||||
|
||||
negateSimpleNumProps :: [Prop] -> [[Prop]]
|
||||
negateSimpleNumProps props = do
|
||||
prop <- props
|
||||
maybe mempty pure (negateSimpleNumProp prop)
|
||||
|
||||
toGoal :: Prop -> Goal
|
||||
toGoal prop =
|
||||
toGoal :: Prop -> Goal
|
||||
toGoal prop =
|
||||
Goal
|
||||
{ goalSource = CtPropGuardsExhaustive name
|
||||
, goalRange = srcRange $ P.bName b
|
||||
, goal = prop }
|
||||
|
||||
canProve :: [Prop] -> [Goal] -> InferM Bool
|
||||
canProve asmps goals = isRight <$>
|
||||
canProve asmps goals = isRight <$>
|
||||
tryProveImplication (Just name) as asmps goals
|
||||
|
||||
-- Try to prove that the first guard will be satisfied. If cannot,
|
||||
@ -1109,14 +1150,14 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
|
||||
checkExhaustive :: [Prop] -> [[Prop]] -> InferM Bool
|
||||
checkExhaustive _asmps [] = pure False -- empty GuardProps
|
||||
checkExhaustive asmps [guard] = do
|
||||
canProve asmps (toGoal <$> guard)
|
||||
checkExhaustive asmps (guard : guards) =
|
||||
canProve asmps (toGoal <$> guard) >>= \case
|
||||
canProve asmps (toGoal <$> guard)
|
||||
checkExhaustive asmps (guard : guards) =
|
||||
canProve asmps (toGoal <$> guard) >>= \case
|
||||
True -> pure True
|
||||
False -> and <$> mapM
|
||||
(\asmps' -> checkExhaustive (asmps <> asmps') guards)
|
||||
(negateSimpleNumProps guard)
|
||||
|
||||
|
||||
checkExhaustive asmps1 (fst <$> cases1) >>= \case
|
||||
True ->
|
||||
-- proved exhaustive
|
||||
@ -1125,7 +1166,7 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
|
||||
-- didn't prove exhaustive i.e. none of the guarding props
|
||||
-- necessarily hold
|
||||
recordWarning (NonExhaustivePropGuards name)
|
||||
|
||||
|
||||
return Decl
|
||||
{ dName = name
|
||||
, dSignature = Forall as asmps1 t1
|
||||
@ -1178,7 +1219,7 @@ checkSigB b (Forall as asmps0 t0, validSchema) =
|
||||
|
||||
-- includes asmpsSign for the sake of implication, but doesn't actually
|
||||
-- include them in the resulting asmps
|
||||
su <- proveImplication (Just (thing (P.bName b))) as (asmpsSign <> asmps2) stay
|
||||
su <- proveImplication True (Just (thing (P.bName b))) as (asmpsSign <> asmps2) stay
|
||||
extendSubst su
|
||||
|
||||
let asmps = concatMap pSplitAnd (apSubst su asmps2)
|
||||
@ -1274,8 +1315,8 @@ checkDecl isTopLevel d mbDoc =
|
||||
checkParameterFun :: P.ParameterFun Name -> InferM ModVParam
|
||||
checkParameterFun x =
|
||||
do (s,gs) <- checkSchema NoWildCards (P.pfSchema x)
|
||||
su <- proveImplication (Just (thing (P.pfName x)))
|
||||
(sVars s) (sProps s) gs
|
||||
su <- proveImplication False (Just (thing (P.pfName x)))
|
||||
(sVars s) (sProps s) gs
|
||||
unless (isEmptySubst su) $
|
||||
panic "checkParameterFun" ["Subst not empty??"]
|
||||
let n = thing (P.pfName x)
|
||||
|
||||
@ -221,6 +221,8 @@ data ConstraintSource
|
||||
| CtPattern TypeSource -- ^ Constraints arising from type-checking patterns
|
||||
| CtModuleInstance ModName -- ^ Instantiating a parametrized module
|
||||
| CtPropGuardsExhaustive Name -- ^ Checking that a use of prop guards is exhastive
|
||||
| CtFFI Name -- ^ Constraints on a foreign declaration required
|
||||
-- by the FFI (e.g. sequences must be finite)
|
||||
deriving (Show, Generic, NFData)
|
||||
|
||||
selSrc :: Selector -> TypeSource
|
||||
@ -249,6 +251,7 @@ instance TVars ConstraintSource where
|
||||
CtPattern _ -> src
|
||||
CtModuleInstance _ -> src
|
||||
CtPropGuardsExhaustive _ -> src
|
||||
CtFFI _ -> src
|
||||
|
||||
|
||||
instance FVS Goal where
|
||||
@ -356,6 +359,7 @@ instance PP ConstraintSource where
|
||||
CtPattern ad -> "checking a pattern:" <+> pp ad
|
||||
CtModuleInstance n -> "module instantiation" <+> pp n
|
||||
CtPropGuardsExhaustive n -> "exhaustion check for prop guards used in defining" <+> pp n
|
||||
CtFFI f -> "declaration of foreign function" <+> pp f
|
||||
|
||||
ppUse :: Expr -> Doc
|
||||
ppUse expr =
|
||||
|
||||
@ -95,6 +95,7 @@ instance ShowParseable Decl where
|
||||
|
||||
instance ShowParseable DeclDef where
|
||||
showParseable DPrim = text (show DPrim)
|
||||
showParseable (DForeign t) = text (show $ DForeign t)
|
||||
showParseable (DExpr e) = parens (text "DExpr" $$ showParseable e)
|
||||
|
||||
instance ShowParseable DeclGroup where
|
||||
|
||||
@ -404,6 +404,10 @@ checkDecl checkSig d =
|
||||
do when checkSig $ checkSchema $ dSignature d
|
||||
return (dName d, dSignature d)
|
||||
|
||||
DForeign _ ->
|
||||
do when checkSig $ checkSchema $ dSignature d
|
||||
return (dName d, dSignature d)
|
||||
|
||||
DExpr e ->
|
||||
do let s = dSignature d
|
||||
when checkSig $ checkSchema s
|
||||
|
||||
@ -38,6 +38,7 @@ import Cryptol.Utils.Patterns(matchMaybe)
|
||||
|
||||
import Control.Applicative ((<|>))
|
||||
import Control.Monad(mzero)
|
||||
import Data.Containers.ListUtils (nubOrd)
|
||||
import Data.Map (Map)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Set ( Set )
|
||||
@ -266,20 +267,21 @@ proveModuleTopLevel =
|
||||
cs <- getParamConstraints
|
||||
case cs of
|
||||
[] -> addGoals gs1
|
||||
_ -> do su2 <- proveImplication Nothing [] [] gs1
|
||||
_ -> do su2 <- proveImplication False Nothing [] [] gs1
|
||||
extendSubst su2
|
||||
|
||||
-- | Prove an implication, and return any improvements that we computed.
|
||||
-- Records errors, if any of the goals couldn't be solved.
|
||||
proveImplication :: Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Subst
|
||||
proveImplication lnam as ps gs =
|
||||
proveImplication :: Bool -> Maybe Name ->
|
||||
[TParam] -> [Prop] -> [Goal] -> InferM Subst
|
||||
proveImplication dedupErrs lnam as ps gs =
|
||||
do evars <- varsWithAsmps
|
||||
solver <- getSolver
|
||||
|
||||
extraAs <- (map mtpParam . Map.elems) <$> getParamTypes
|
||||
extra <- map thing <$> getParamConstraints
|
||||
|
||||
(mbErr,su) <- io (proveImplicationIO solver lnam evars
|
||||
(mbErr,su) <- io (proveImplicationIO solver dedupErrs lnam evars
|
||||
(extraAs ++ as) (extra ++ ps) gs)
|
||||
case mbErr of
|
||||
Right ws -> mapM_ recordWarning ws
|
||||
@ -301,7 +303,7 @@ tryProveImplication lnam as ps gs =
|
||||
extraAs <- (map mtpParam . Map.elems) <$> getParamTypes
|
||||
extra <- map thing <$> getParamConstraints
|
||||
|
||||
(mbErr,su) <- io (proveImplicationIO solver lnam evars
|
||||
(mbErr,su) <- io (proveImplicationIO solver False lnam evars
|
||||
(extraAs ++ as) (extra ++ ps) gs)
|
||||
case mbErr of
|
||||
Left errs -> pure . Left $ do
|
||||
@ -311,6 +313,7 @@ tryProveImplication lnam as ps gs =
|
||||
return su
|
||||
|
||||
proveImplicationIO :: Solver
|
||||
-> Bool -- ^ Whether to remove duplicate goals in errors
|
||||
-> Maybe Name -- ^ Checking this function
|
||||
-> Set TVar -- ^ These appear in the env., and we should
|
||||
-- not try to default them
|
||||
@ -318,8 +321,8 @@ proveImplicationIO :: Solver
|
||||
-> [Prop] -- ^ Assumed constraint
|
||||
-> [Goal] -- ^ Collected constraints
|
||||
-> IO (Either [Error] [Warning], Subst)
|
||||
proveImplicationIO _ _ _ _ [] [] = return (Right [], emptySubst)
|
||||
proveImplicationIO s f varsInEnv ps asmps0 gs0 =
|
||||
proveImplicationIO _ _ _ _ _ [] [] = return (Right [], emptySubst)
|
||||
proveImplicationIO s dedupErrs f varsInEnv ps asmps0 gs0 =
|
||||
do let ctxt = buildSolverCtxt asmps
|
||||
res <- quickSolverIO ctxt gs
|
||||
case res of
|
||||
@ -339,7 +342,7 @@ proveImplicationIO s f varsInEnv ps asmps0 gs0 =
|
||||
return (Left (err gs3:errs), su) -- XXX: Old?
|
||||
(_,newGs,newSu,ws,errs) ->
|
||||
do let su1 = newSu @@ su
|
||||
(res1,su2) <- proveImplicationIO s f varsInEnv ps
|
||||
(res1,su2) <- proveImplicationIO s dedupErrs f varsInEnv ps
|
||||
(apSubst su1 asmps0) newGs
|
||||
let su3 = su2 @@ su1
|
||||
case res1 of
|
||||
@ -353,7 +356,7 @@ proveImplicationIO s f varsInEnv ps asmps0 gs0 =
|
||||
$ DelayedCt { dctSource = f
|
||||
, dctForall = ps
|
||||
, dctAsmps = asmps0
|
||||
, dctGoals = us
|
||||
, dctGoals = if dedupErrs then nubOrd us else us
|
||||
}
|
||||
|
||||
|
||||
|
||||
@ -408,8 +408,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 su (DExpr e) = DExpr !$ (apSubst su e)
|
||||
apSubst _ DPrim = DPrim
|
||||
apSubst _ (DForeign t) = DForeign t
|
||||
|
||||
instance TVars Module where
|
||||
apSubst su m =
|
||||
|
||||
@ -22,6 +22,7 @@ module Cryptol.Utils.RecordMap
|
||||
, canonicalFields
|
||||
, displayFields
|
||||
, recordElements
|
||||
, displayElements
|
||||
, fieldSet
|
||||
, recordFromFields
|
||||
, recordFromFieldsErr
|
||||
@ -90,6 +91,11 @@ recordElements = map snd . canonicalFields
|
||||
canonicalFields :: RecordMap a b -> [(a,b)]
|
||||
canonicalFields = Map.toList . recordMap
|
||||
|
||||
-- | Retrieve the elements of the record in display order
|
||||
-- of the field names.
|
||||
displayElements :: (Show a, Ord a) => RecordMap a b -> [b]
|
||||
displayElements = map snd . displayFields
|
||||
|
||||
-- | Return a list of field/value pairs in display order.
|
||||
displayFields :: (Show a, Ord a) => RecordMap a b -> [(a,b)]
|
||||
displayFields r = map find (displayOrder r)
|
||||
|
||||
@ -7,6 +7,8 @@
|
||||
-- Portability : portable
|
||||
|
||||
-- {-# LANGUAGE Safe #-}
|
||||
{-# LANGUAGE CPP #-}
|
||||
{-# LANGUAGE Safe #-}
|
||||
|
||||
module Cryptol.Version (
|
||||
commitHash
|
||||
@ -39,6 +41,9 @@ displayVersion putLn = do
|
||||
putLn ("Cryptol " ++ ver)
|
||||
putLn ("Git commit " ++ commitHash)
|
||||
putLn (" branch " ++ commitBranch ++ dirtyLab)
|
||||
#ifdef FFI_ENABLED
|
||||
putLn "FFI enabled"
|
||||
#endif
|
||||
where
|
||||
dirtyLab | commitDirty = " (non-committed files present during build)"
|
||||
| otherwise = ""
|
||||
|
||||
2
tests/.gitignore
vendored
2
tests/.gitignore
vendored
@ -1 +1,3 @@
|
||||
output
|
||||
*.so
|
||||
*.dylib
|
||||
|
||||
28
tests/ffi/Makefile
Normal file
28
tests/ffi/Makefile
Normal file
@ -0,0 +1,28 @@
|
||||
CFLAGS += -Wall -Werror
|
||||
|
||||
# For each C file foo.c, we make a phony target foo, then depending on the OS
|
||||
# map that to either foo.dylib or foo.so.
|
||||
|
||||
CFILES = $(wildcard *.c)
|
||||
TARGETS = $(CFILES:.c=)
|
||||
|
||||
all: $(TARGETS)
|
||||
|
||||
.PHONY: all clean $(TARGETS)
|
||||
|
||||
ifeq ($(shell uname),Darwin)
|
||||
EXT = .dylib
|
||||
else
|
||||
EXT = .so
|
||||
endif
|
||||
|
||||
$(TARGETS): %: %$(EXT)
|
||||
|
||||
%.dylib: %.c
|
||||
$(CC) $(CFLAGS) -dynamiclib $< -o $@
|
||||
|
||||
%.so: %.c
|
||||
$(CC) $(CFLAGS) -fPIC -shared $< -o $@
|
||||
|
||||
clean:
|
||||
rm *$(EXT)
|
||||
1
tests/ffi/ffi-reload.cry
Normal file
1
tests/ffi/ffi-reload.cry
Normal file
@ -0,0 +1 @@
|
||||
foreign test : () -> Bit
|
||||
10
tests/ffi/ffi-reload.icry
Normal file
10
tests/ffi/ffi-reload.icry
Normal file
@ -0,0 +1,10 @@
|
||||
:! echo '#include <stdint.h>\nuint8_t test() { return 0; }' > ffi-reload.c
|
||||
:! make -s ffi-reload
|
||||
:l ffi-reload.cry
|
||||
test ()
|
||||
:! sleep 1
|
||||
:! sed -i.bak 's/return 0/return 1/' ffi-reload.c
|
||||
:! make -s ffi-reload
|
||||
:r
|
||||
test ()
|
||||
:! rm ffi-reload.c ffi-reload.c.bak
|
||||
7
tests/ffi/ffi-reload.icry.stdout
Normal file
7
tests/ffi/ffi-reload.icry.stdout
Normal file
@ -0,0 +1,7 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
False
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
True
|
||||
10
tests/ffi/ffi-runtime-errors.c
Normal file
10
tests/ffi/ffi-runtime-errors.c
Normal file
@ -0,0 +1,10 @@
|
||||
#include <stddef.h>
|
||||
#include <stdint.h>
|
||||
|
||||
uint8_t f(size_t n, uint8_t *p) {
|
||||
return n == 0;
|
||||
}
|
||||
|
||||
uint8_t g(uint8_t x) {
|
||||
return x;
|
||||
}
|
||||
2
tests/ffi/ffi-runtime-errors.cry
Normal file
2
tests/ffi/ffi-runtime-errors.cry
Normal file
@ -0,0 +1,2 @@
|
||||
foreign f : {n} (fin n, n >= 2^^64) => [n - 2^^64][8] -> Bit
|
||||
foreign g : Bit -> Bit
|
||||
9
tests/ffi/ffi-runtime-errors.icry
Normal file
9
tests/ffi/ffi-runtime-errors.icry
Normal file
@ -0,0 +1,9 @@
|
||||
:! make -s ffi-runtime-errors
|
||||
:l ffi-runtime-errors.cry
|
||||
|
||||
f []
|
||||
|
||||
:prove g
|
||||
:sat g
|
||||
:safe g
|
||||
:eval g
|
||||
28
tests/ffi/ffi-runtime-errors.icry.stdout
Normal file
28
tests/ffi/ffi-runtime-errors.icry.stdout
Normal file
@ -0,0 +1,28 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
|
||||
numeric type argument to foreign function is too large: 18446744073709551616
|
||||
in type parameter n`899 of function Main::f
|
||||
type arguments must fit in a C `size_t`
|
||||
-- Backtrace --
|
||||
Main::f called at ffi-runtime-errors.icry:4:1--4:2
|
||||
|
||||
cannot call foreign function Main::g
|
||||
FFI calls are not supported in this context
|
||||
If you are trying to evaluate an expression, try rebuilding
|
||||
Cryptol with FFI support enabled.
|
||||
|
||||
cannot call foreign function Main::g
|
||||
FFI calls are not supported in this context
|
||||
If you are trying to evaluate an expression, try rebuilding
|
||||
Cryptol with FFI support enabled.
|
||||
|
||||
cannot call foreign function Main::g
|
||||
FFI calls are not supported in this context
|
||||
If you are trying to evaluate an expression, try rebuilding
|
||||
Cryptol with FFI support enabled.
|
||||
cannot call foreign function Main::g
|
||||
FFI calls are not supported in this context
|
||||
If you are trying to evaluate an expression, try rebuilding
|
||||
Cryptol with FFI support enabled.
|
||||
11
tests/ffi/ffi-type-errors.cry
Normal file
11
tests/ffi/ffi-type-errors.cry
Normal file
@ -0,0 +1,11 @@
|
||||
import Float
|
||||
|
||||
foreign badWordSizes : [65] -> [128]
|
||||
foreign badFloatSizes : Float16 -> Float128
|
||||
foreign badArrayTypes : {n} (fin n) => [n]Bit -> [n]([16], [16]) -> [n][4][8]
|
||||
foreign badTypes : Integer -> Z 3
|
||||
foreign notFunction : [32]
|
||||
foreign badKind : {t} t -> [32]
|
||||
foreign noFin : {n} [n][32] -> [n * 2][32]
|
||||
foreign infSeq : [inf][32] -> Bit
|
||||
foreign wildcard : { x : [8], y : Float32 } -> _
|
||||
1
tests/ffi/ffi-type-errors.icry
Normal file
1
tests/ffi/ffi-type-errors.icry
Normal file
@ -0,0 +1 @@
|
||||
:l ffi-type-errors.cry
|
||||
102
tests/ffi/ffi-type-errors.icry.stdout
Normal file
102
tests/ffi/ffi-type-errors.icry.stdout
Normal file
@ -0,0 +1,102 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Float
|
||||
Loading module Main
|
||||
|
||||
[error] at ffi-type-errors.cry:3:9--3:37:
|
||||
Type unsupported for FFI:
|
||||
[65] -> [128]
|
||||
Due to:
|
||||
Type unsupported for FFI:
|
||||
[65]
|
||||
Due to:
|
||||
Unsupported word size
|
||||
Only words of up to 64 bits are supported
|
||||
Type unsupported for FFI:
|
||||
[128]
|
||||
Due to:
|
||||
Unsupported word size
|
||||
Only words of up to 64 bits are supported
|
||||
When checking the type of 'Main::badWordSizes'
|
||||
[error] at ffi-type-errors.cry:4:9--4:44:
|
||||
Type unsupported for FFI:
|
||||
Float 5 11 -> Float 15 113
|
||||
Due to:
|
||||
Type unsupported for FFI:
|
||||
Float 5 11
|
||||
Due to:
|
||||
Unsupported Float format
|
||||
Only Float32 and Float64 are supported
|
||||
Type unsupported for FFI:
|
||||
Float 15 113
|
||||
Due to:
|
||||
Unsupported Float format
|
||||
Only Float32 and Float64 are supported
|
||||
When checking the type of 'Main::badFloatSizes'
|
||||
[error] at ffi-type-errors.cry:5:9--5:78:
|
||||
Type unsupported for FFI:
|
||||
[n`969] -> [n`969]([16], [16]) -> [n`969][4][8]
|
||||
Due to:
|
||||
Type unsupported for FFI:
|
||||
[n`969]
|
||||
Due to:
|
||||
Unsupported sequence element type
|
||||
Only words or floats are supported as the element type of sequences
|
||||
Type unsupported for FFI:
|
||||
[n`969]([16], [16])
|
||||
Due to:
|
||||
Unsupported sequence element type
|
||||
Only words or floats are supported as the element type of sequences
|
||||
Type unsupported for FFI:
|
||||
[n`969][4][8]
|
||||
Due to:
|
||||
Unsupported sequence element type
|
||||
Only words or floats are supported as the element type of sequences
|
||||
When checking the type of 'Main::badArrayTypes'
|
||||
[error] at ffi-type-errors.cry:6:9--6:34:
|
||||
Type unsupported for FFI:
|
||||
Integer -> Z 3
|
||||
Due to:
|
||||
Type unsupported for FFI:
|
||||
Integer
|
||||
Due to:
|
||||
Only Bit, words, floats, sequences of words or floats,
|
||||
or structs or tuples of the above are supported as FFI
|
||||
argument or return types
|
||||
Type unsupported for FFI:
|
||||
Z 3
|
||||
Due to:
|
||||
Only Bit, words, floats, sequences of words or floats,
|
||||
or structs or tuples of the above are supported as FFI
|
||||
argument or return types
|
||||
When checking the type of 'Main::badTypes'
|
||||
[error] at ffi-type-errors.cry:7:9--7:27:
|
||||
Type unsupported for FFI:
|
||||
[32]
|
||||
Due to:
|
||||
FFI binding must be a function
|
||||
When checking the type of 'Main::notFunction'
|
||||
[error] at ffi-type-errors.cry:8:9--8:32:
|
||||
Kind of type variable unsupported for FFI:
|
||||
t`970 : *
|
||||
Only type variables of kind # are supported
|
||||
When checking the type of 'Main::badKind'
|
||||
[error] at ffi-type-errors.cry:9:9--9:43:
|
||||
Failed to validate user-specified signature.
|
||||
in the definition of 'Main::noFin', at ffi-type-errors.cry:9:9--9:14,
|
||||
we need to show that
|
||||
for any type n
|
||||
the following constraints hold:
|
||||
• fin n
|
||||
arising from
|
||||
declaration of foreign function Main::noFin
|
||||
at ffi-type-errors.cry:9:9--9:43
|
||||
[error] at ffi-type-errors.cry:10:9--10:34:
|
||||
• Unsolvable constraint:
|
||||
fin inf
|
||||
arising from
|
||||
declaration of foreign function Main::infSeq
|
||||
at ffi-type-errors.cry:10:9--10:34
|
||||
[error] at ffi-type-errors.cry:11:48--11:49:
|
||||
Wild card types are not allowed in this context
|
||||
(e.g., they cannot be used in type synonyms or FFI declarations).
|
||||
118
tests/ffi/test-ffi.c
Normal file
118
tests/ffi/test-ffi.c
Normal file
@ -0,0 +1,118 @@
|
||||
#include <assert.h>
|
||||
#include <math.h>
|
||||
#include <stdint.h>
|
||||
#include <stddef.h>
|
||||
|
||||
uint8_t add8(uint8_t x, uint8_t y) {
|
||||
return x + y;
|
||||
}
|
||||
|
||||
uint16_t sub16(uint16_t x, uint16_t y) {
|
||||
return x - y;
|
||||
}
|
||||
|
||||
uint32_t mul32(uint32_t x, uint32_t y) {
|
||||
return x * y;
|
||||
}
|
||||
|
||||
uint64_t div64(uint64_t x, uint64_t y) {
|
||||
return x / y;
|
||||
}
|
||||
|
||||
uint8_t extendInput(uint8_t x) {
|
||||
return x;
|
||||
}
|
||||
|
||||
uint8_t maskOutput(uint8_t x) {
|
||||
return x;
|
||||
}
|
||||
|
||||
uint8_t noBits(uint8_t zero) {
|
||||
assert(zero == 0);
|
||||
return 1;
|
||||
}
|
||||
|
||||
uint8_t not(uint8_t x) {
|
||||
return !x;
|
||||
}
|
||||
|
||||
float addFloat32(float x, float y) {
|
||||
return x + y;
|
||||
}
|
||||
|
||||
double subFloat64(double x, double y) {
|
||||
return x - y;
|
||||
}
|
||||
|
||||
float specialFloats(uint8_t select) {
|
||||
switch (select) {
|
||||
case 0:
|
||||
return INFINITY;
|
||||
case 1:
|
||||
return -INFINITY;
|
||||
case 2:
|
||||
return NAN;
|
||||
case 3:
|
||||
return -0.0f;
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
uint8_t usesTypeSynonym(uint32_t x, float y) {
|
||||
return x == y;
|
||||
}
|
||||
|
||||
uint32_t sum10(uint32_t *xs) {
|
||||
uint32_t sum = 0;
|
||||
for (unsigned i = 0; i < 10; ++i) {
|
||||
sum += xs[i];
|
||||
}
|
||||
return sum;
|
||||
}
|
||||
|
||||
void reverse5(double *in, double *out) {
|
||||
for (unsigned i = 0; i < 5; ++i) {
|
||||
out[i] = in[4 - i];
|
||||
}
|
||||
}
|
||||
|
||||
void compoundTypes(uint32_t n, uint16_t x, uint32_t *y, uint32_t *z,
|
||||
uint16_t *a_0, uint16_t *a_1, uint32_t *c, uint8_t *d, uint8_t *e) {
|
||||
*a_0 = n >> 16;
|
||||
*a_1 = n;
|
||||
for (unsigned i = 0; i < 3; ++i) {
|
||||
c[i] = y[i];
|
||||
}
|
||||
for (unsigned i = 0; i < 5; ++i) {
|
||||
c[i + 3] = z[i];
|
||||
}
|
||||
*d = x >> 5;
|
||||
*e = x;
|
||||
}
|
||||
|
||||
uint64_t typeToValue(size_t n) {
|
||||
return n;
|
||||
}
|
||||
|
||||
uint32_t sumPoly(size_t n, uint32_t *xs) {
|
||||
uint32_t sum = 0;
|
||||
for (size_t i = 0; i < n; ++i) {
|
||||
sum += xs[i];
|
||||
}
|
||||
return sum;
|
||||
}
|
||||
|
||||
void inits(size_t n, uint8_t *in, uint8_t *out) {
|
||||
for (unsigned i = 1; i <= n; ++i) {
|
||||
for (unsigned j = 0; j < i; ++j) {
|
||||
*out++ = in[j];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void zipMul3(size_t n, size_t m, size_t p, float *xs, float *ys, float *zs,
|
||||
float *out) {
|
||||
for (size_t i = 0; i < n && i < m && i < p; ++i) {
|
||||
out[i] = xs[i] * ys[i] * zs[i];
|
||||
}
|
||||
}
|
||||
40
tests/ffi/test-ffi.cry
Normal file
40
tests/ffi/test-ffi.cry
Normal file
@ -0,0 +1,40 @@
|
||||
import Float
|
||||
|
||||
// Basic integral types
|
||||
foreign add8 : [8] -> [8] -> [8]
|
||||
foreign sub16 : [16] -> [16] -> [16]
|
||||
foreign mul32 : [32] -> [32] -> [32]
|
||||
foreign div64 : [64] -> [64] -> [64]
|
||||
|
||||
// Non-machine integer sizes
|
||||
foreign extendInput : [3] -> [8]
|
||||
foreign maskOutput : [8] -> [3]
|
||||
foreign noBits : [0] -> [0]
|
||||
|
||||
// Bit
|
||||
foreign not : Bit -> Bit
|
||||
|
||||
// Float
|
||||
foreign addFloat32 : Float32 -> Float32 -> Float32
|
||||
foreign subFloat64 : Float64 -> Float64 -> Float64
|
||||
foreign specialFloats : [2] -> Float32
|
||||
|
||||
// Type synonyms
|
||||
type Word32 = [32]
|
||||
type MyFunc = Word32 -> Float32 -> Bit
|
||||
foreign usesTypeSynonym : MyFunc
|
||||
|
||||
// Sequences
|
||||
foreign sum10 : [10]Word32 -> Word32
|
||||
foreign reverse5 : [5]Float64 -> [5]Float64
|
||||
|
||||
// Tuples and records
|
||||
foreign compoundTypes : ([32], { x : [10], y : [3][20] }) -> { z : [5][20] }
|
||||
-> { a : ([16], [16]), b : { c : [8][20], d : [5], e : [5] } }
|
||||
|
||||
// Polymorphic sizes
|
||||
foreign typeToValue : {n} (fin n) => () -> [64]
|
||||
foreign sumPoly : {n} (fin n) => [n]Word32 -> Word32
|
||||
foreign inits : {n} (fin n) => [n][8] -> [n * (n + 1) / 2][8]
|
||||
foreign zipMul3 : {n, m, p} (fin n, fin m, fin p) =>
|
||||
[n]Float32 -> [m]Float32 -> [p]Float32 -> [min n (min m p)]Float32
|
||||
34
tests/ffi/test-ffi.icry
Normal file
34
tests/ffi/test-ffi.icry
Normal file
@ -0,0 +1,34 @@
|
||||
:! make -s test-ffi
|
||||
:l test-ffi.cry
|
||||
|
||||
add8 1 2
|
||||
sub16 12345 6789
|
||||
mul32 123456 7890
|
||||
div64 12345678901234567890 987654321
|
||||
|
||||
extendInput 7
|
||||
maskOutput 255
|
||||
noBits 0
|
||||
|
||||
not True
|
||||
|
||||
addFloat32 12.34 56.78
|
||||
subFloat64 1234.5678 9012.3456
|
||||
specialFloats 0
|
||||
specialFloats 1
|
||||
specialFloats 2
|
||||
specialFloats 3
|
||||
|
||||
usesTypeSynonym 42 42
|
||||
|
||||
sum10 [1..10]
|
||||
reverse5 [0x1.23, -0x3.45, 0x6.78, -0x9.0a, 0xb.cd]
|
||||
|
||||
compoundTypes (0x12345678, {y = [10, 20, 30], x = 300}) {z = [40, 50, 60, 70, 80]}
|
||||
|
||||
typeToValue`{0x12345678deadbeef} ()
|
||||
sumPoly []
|
||||
sumPoly [1..10]
|
||||
sumPoly [1..10000]
|
||||
inits [1..5]
|
||||
zipMul3 [1, 2, 3] [3, 4, 5, 6] [6, 7, 8, 9, 10]
|
||||
33
tests/ffi/test-ffi.icry.stdout
Normal file
33
tests/ffi/test-ffi.icry.stdout
Normal file
@ -0,0 +1,33 @@
|
||||
Loading module Cryptol
|
||||
Loading module Cryptol
|
||||
Loading module Float
|
||||
Loading module Main
|
||||
0x03
|
||||
0x15b4
|
||||
0x3a0f1880
|
||||
0x00000002e90edc8f
|
||||
0x07
|
||||
0x7
|
||||
0x0
|
||||
False
|
||||
0x45.1eb8
|
||||
-0x1e61.c71de69ad5
|
||||
fpPosInf
|
||||
fpNegInf
|
||||
fpNaN
|
||||
-0.0
|
||||
True
|
||||
0x00000037
|
||||
[0xb.cd, -0x9.0a, 0x6.78, -0x3.45, 0x1.23]
|
||||
{a = (0x1234, 0x5678),
|
||||
b = {c = [0x0000a, 0x00014, 0x0001e, 0x00028, 0x00032, 0x0003c,
|
||||
0x00046, 0x00050],
|
||||
d = 0x09,
|
||||
e = 0x0c}}
|
||||
0x12345678deadbeef
|
||||
0x00000000
|
||||
0x00000037
|
||||
0x02fb0408
|
||||
[0x01, 0x01, 0x02, 0x01, 0x02, 0x03, 0x01, 0x02, 0x03, 0x04, 0x01,
|
||||
0x02, 0x03, 0x04, 0x05]
|
||||
[0x12.0, 0x38.0, 0x78.0]
|
||||
@ -77,7 +77,7 @@ Loading module Main
|
||||
|
||||
[error] at tc-errors-4.cry:1:10--1:11:
|
||||
Wild card types are not allowed in this context
|
||||
(e.g., they cannot be used in type synonyms).
|
||||
(e.g., they cannot be used in type synonyms or FFI declarations).
|
||||
Loading module Cryptol
|
||||
Loading module Main
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user