-
Notifications
You must be signed in to change notification settings - Fork 126
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Support calls to foreign functions #1090
Comments
From a language design point of view, I think this will be pretty easy actually. Our internal AST already has places to pipe in "pragmas" that can be attached to bindings. It's then just a matter of deciding what the syntax should be. I suggest something like the following:
Then the interpreter and any code-gen backends just have to know which FFI conventions to pay attention to and how to interpret them. |
A minor point: we'll still need a way of annotating the type for the symbol. I expect this is essentially the same as writing
More importantly, considering the above example, some backends might need/want additional information, so it should be possible to apply multiple annotations. Presumably these don't need too much structure, and the responsibility for interpreting the annotation belongs to the interpreter. Taking hardware as an example, I'd think we might want to tell the translator: (1) what the name of the module is, (2) what the names of the input/output signals are |
I wonder if this just boils down to exposing the ability to annotate declarations? In the case of translator-specific foreign definitions, I'm not sure that the annotations really have no meaning to Cryptol itself, except to say that there may not be an implementation. |
We won't need to annotate the type, the typechecker will figure it out for us. The idea is that |
E.g. you might write
I don't know what we would want to do with polymorphic things, binding those to external stuff seems much harder. |
One thing that may be worth thinking about is how/whether to handle polymorphic primitives. Maybe for some languages it doesn't make sense... but then again maybe there's some suitable representation of cryptol types we could create in that language to supply as a parameter and cause it to make sense. For the "allow users to create high-performance primitives" one in particular, I could easily imagine having Haskell as a choice of implementation language, and it seems completely reasonable to allow such primitives to be polymorphic. |
This would probably be part of the calling convention. For example, I could imagine a calling convention where numeric type parameters are mapped to some kind of number when calling |
One consideration might be whether we want to be able to have one external reference used in multiple ways. Say we have a signature algorithm that builds on SHA3. In the interpreter, we may want to call out to an external implementation in a specific shared library. When compiling to C, we may want to include a call to some existing C source code. And we may want to be able to do both from the same source file. What this suggests to me is that the declaration "this thing is external" and the metadata "here's where to find it" are somewhat separate and it may make sense to put them in different places. The "this is external" aspect maybe belongs in the source code but the "here's where to find it" part may make sense as separate input to the interpreter/compiler/whatever. Another thing that might simplify things: because we're talking about assuming a calling convention that we specify, might it also be sensible to assume that the external function has the same name that it does internally in Cryptol? So |
@atomb Perhaps you could simply allow multiple
or something like that. |
See #1376 for an implementation of this idea. Some interesting challenges have arisen while prototyping this feature regarding how we should link against the
First, let me explain each issue in more detail:
How should we address each of these problems?
|
I came across this issue some time after I had already begun working on the FFI, so the currently implemented syntax is a little different than what is proposed in this issue. But right now in #1376 I have the following implemented: given a file
when the module is loaded, Cryptol will look for a file named Currently the only type that is supported is unsigned long func(unsigned long x) {
return x + 1;
} The tentative plans for support for more types are, after discussions with @yav:
There is also the question of how ownership of memory is handled when using arrays. @yav came up with two choices:
I also think that there could be a third option:
Finally we probably want to also support sequences of non-fixed length. The issue here is that in Cryptol the length is encoded as a type parameter while in C it is usually a value parameter passed with the pointer. So I was thinking that we can just insert the type parameters as value parameters, so something like I created a github "project" at https://github.com/GaloisInc/cryptol/projects/1 where I'm tracking specific things I'm working on at the moment related to the FFI if anyone is curious. |
@qsctr @robdockins I was thinking a bit about what types should be Representtaion
Arguments of tuples/structs types are passed into function as multiple arguments, We have to be careful to pass the fields of a struct in the correct order, Results of tuple/struct types are retruend into multiple output arguments. OwnershipI am still not quite decided on what policy to use for passing arrays. The 2
The choice of ownership policy has an effect on how C functions should return
Examples:
corresponds to a C function of type with ownership schema (1):
corresponds to a C function of type with ownership schema (2):
I am leaning slightly towards ownership schema 2, but could go either way. Thoughts? |
I am leaning towards 2 as well, since it feels simpler overall. The non-uniform behavior for arrays is unfortunate but I guess just a consequence of how C handles passing arrays differently compared to other values. For the representation of |
Another option is to provide an interface that programmers must target. Here's a pretty simple example for bitvector types: https://github.com/weaversa/bitvector (as well as some sequences). The same could be done for languages other than C -- this is how the old cryptol java code generator worked - it provided it's own interface it would compile to, rather than going to native Java types. (for those w/ access, see: https://gitlab-ext.galois.com/cryptol/cryptol-codegen/-/blob/master/java-support/BitVector.java). I can also imagine targeting hacspec for Rust. Yet another alternative is to follow the semantics of SAW. In the Python interface (at least) cryptol in |
The types I listed are the types that map, more or less, 1-1 to C types. There are various ways to support more types, but I think it might be better to handle those by writing a bit of Cryptol code to translate to/from the basic types, as this would make the required representation explicit. For example, if I want to pass in Once we have this working well, it should be relatively easy, I think, to build a library on top of it, or extend it with extra types. Edit: Thinking a bit more about this, |
@weaversa and @eddywestbrook mentioned that once we are done with the FFI it would be nice to reimplement something like the SuiteB AES primitives with FFI to try it out (as a separate module for now which can be a drop-in replacement for SuiteB). This would hopefully result in a speedup in code like this. (FFI is almost done by the way, everything mentioned in @yav's earlier comment is already working except for size-polymorphic sequences) |
Since #1376 has been merged, containing an initial implementation of the FFI, I'm going to close this issue for now. I've moved a few things mentioned in this discussion that weren't included in the initial PR into separate issues with the |
Allowing Cryptol programs to reference external functions, written in other languages, could have several benefits:
It could be possible to do this with very little change to the language. The notion of a
primitive
in Cryptol, as it exists, is close to what we need. Ultimately, this construct currently means that any prover, interpreter, or compiler needs to know how to model, execute, or generate code for that function without (necessarily) having access to Cryptol source code for it.Given that users can already declare primitives within any source file, the missing piece seems to be having a way to map primitives to external references. Some programming languages with foreign function interfaces have very flexible mechanisms allowing users to specify how external code is called, how parameters are passed, and so on. In the name of simplicity, it may be better (at least at first, potentially permanently) to simply state what the calling convention for external code should be.
If we do that, then the only remaining piece is a way for users to specify where an external symbol is located. For the four use cases listed above, here are some possibilities:
One potential issue here would be the accidental use of primitives. Currently, trying to
:prove
a formula that references a user-declared primitive that the symbolic backend doesn't know about yields an "unimplemented primitive" message. It might be less user-friendly to instead get an error back from the solver that it doesn't understand the formula Cryptol has sent it. Perhaps an additional marker, such as anexternal primitive
or even justexternal
could make this more explicit?For case (1), one remaining issue is to tell the interpreter where to find the shared library containing the code to execute. We could follow Cryptol 1 by adding syntax to specify this within a Cryptol source file. Or we could allow the interpreter to read some sort of separate "map" file that tells it where to find primitives it doesn't have built-in support for.
The text was updated successfully, but these errors were encountered: