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

Incorrect length for FFI sequence return value #1539

Open
qsctr opened this issue Jun 30, 2023 · 0 comments
Open

Incorrect length for FFI sequence return value #1539

qsctr opened this issue Jun 30, 2023 · 0 comments
Labels
bug Something not working correctly FFI Foreign function interface

Comments

@qsctr
Copy link
Contributor

qsctr commented Jun 30, 2023

As a follow-up to the question in #1538, the user reports:

Output parameters seem to have the same issue. For example, if you have this function:

foreign myfunc :
  {n} (fin n)
  => [n][32] -> [n + 1][32]

Cryptol will only take the first n elements of the output from the FFI function.

I am unable to reproduce this. The corresponding C function should have the signature

void myfunc(size_t n, uint32_t * in, uint32_t * out);

as generated by the :generate-foreign-header Cryptol REPL command. With the following C implementation,

void myfunc(size_t n, uint32_t * in, uint32_t * out) {
    for (size_t i = 0; i < n; ++i) {
        out[i] = in[i];
    }
    out[n] = 42;
}

it seems to return the correct result:

Cryptol> :l test.cry
Loading module Cryptol
Loading module Main
Loading dynamic library test.so
Main> :t myfunc
myfunc : {n} (fin n) => [n][32] -> [1 + n][32]
Main> myfunc [1, 2, 3, 4, 5]
[0x00000001, 0x00000002, 0x00000003, 0x00000004, 0x00000005,
 0x0000002a]

If there are more details regarding the situation in which this bug happens, that would be appreciated!

cc @eddywestbrook @weaversa

@qsctr qsctr added bug Something not working correctly FFI Foreign function interface labels Jun 30, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something not working correctly FFI Foreign function interface
Projects
None yet
Development

No branches or pull requests

1 participant