Skip to content
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

Foreign Function Interface #1376

Merged
merged 65 commits into from
Aug 12, 2022
Merged

Foreign Function Interface #1376

merged 65 commits into from
Aug 12, 2022

Conversation

qsctr
Copy link
Contributor

@qsctr qsctr commented Jun 25, 2022

This PR adds a foreign function interface (FFI) to Cryptol. This allows Cryptol to call functions written in C.

For instance, we can declare this foreign function in Cryptol

foreign add : [32] -> [32] -> [32]

and implement it in C

uint32_t add(uint32_t x, uint32_t y) {
  return x + y;
}

and then call it like any other Cryptol function.

Main> add 1 2
0x00000003

See the FFI docs for more information.

@qsctr qsctr marked this pull request as ready for review June 28, 2022 23:39
cryptol.cabal Outdated Show resolved Hide resolved
src/Cryptol/Eval/FFI.hs Outdated Show resolved Hide resolved
src/Cryptol/Eval/FFI.hs Outdated Show resolved Hide resolved
Copy link
Member

@yav yav left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good to me. I made a few suggestion for stylistic improvements. On the topic of style, I really prefer the case expressions that do not use inverted indentation because it is quite a bit easier to see what is being matched where. For example like this:

I like:

function = some long prefix thing
   case expr of
       A -> thing1
       B -> thing2

rather than:

function = some long prefix thing case expr of
  A -> thing1
  B -> thing2

src/Cryptol/Eval/FFI.hs Show resolved Hide resolved
src/Cryptol/TypeCheck/Solve.hs Show resolved Hide resolved
src/Cryptol/Eval/FFI.hs Show resolved Hide resolved
@qsctr qsctr changed the title Basic FFI Implementation Foreign Function Interface Aug 11, 2022
docs/RefMan/FFI.rst Outdated Show resolved Hide resolved
docs/RefMan/FFI.rst Show resolved Hide resolved
docs/RefMan/FFI.rst Show resolved Hide resolved
@yav yav merged commit 8298ca3 into master Aug 12, 2022
@qsctr qsctr mentioned this pull request Aug 12, 2022
@qsctr qsctr deleted the ffi branch August 12, 2022 21:04
@RyanGlScott RyanGlScott added the FFI Foreign function interface label Sep 19, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
FFI Foreign function interface
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants