`CertiCoq FFI` produces bad C code

[kuruczgy]

Environment

certicoq commit a426ffe04b38e8f3d23bde5be4fc6a315fa8485c Alpine linux 3.16.2

Steps to reproduce

(This actual test input is not relevant, CertiCoq FFI generates incorrect output on any type class I tried.)

(* Test.v *)
Class Test : Type := { test : unit -> unit }.

From CertiCoq.Plugin Require Import CertiCoq.
CertiCoq FFI Test.

coqc Test.v

gcc -w -c ffi.Test.Test.c

Expected behavior

The generated C file compiles without errors.

Actual behavior

ffi.Test.Test.c:15:3: error: '$result' undeclared (first use in this function); did you mean 'result'?
   15 |   $result = test(tinfo, $arg);
      |   ^~~~~~~
      |   result
ffi.Test.Test.c:15:3: note: each undeclared identifier is reported only once for each function it appears in
ffi.Test.Test.c:15:18: error: 'tinfo' undeclared (first use in this function); did you mean '$tinfo'?
   15 |   $result = test(tinfo, $arg);
      |                  ^~~~~
      |                  $tinfo

Some variable definitions are wrong. An excerpt from ffi.Test.Test.c:

void test_1(struct thread_info *$tinfo, unsigned long long $env, unsigned long long $arg)
{
  unsigned long long result;
  $result = test(tinfo, $arg);
  *((unsigned long long *) (*$tinfo).args + 1LLU) = $result;
  return;
}

The variable should be declared as $result instead of result. tinfo is also wrong, but the other way around.

Workaround

This is what I came up with for now, seems to be working so far: sed -i 's/\$\(result\|arg[0-9]\?\|pair\|new_env\|new_clo\|tinfo\|env\)/\1/g' ffi.*.c

[kuruczgy]

Hm also it seems that the generated code lacks any checks before doing allocations, possibly leading to tinfo->alloc exceeding tinfo->limit.

Also given the fact that the CertiCoq FFI command is not documented on the wiki, my impression is that this feature is not really ready for use.

If anyone from the maintainers is reading this, what's the intended status of this feature? Is it still work in progress, or is it some legacy that's no longer maintained?

[intoverflow]

Thank you for reaching out @kuruczgy! You happened to catch us while most folks are either on vacation or preparing for the next term at university. We are tracking and will update this thread

[kuruczgy]

Thank you for your response :)

Of course, I don't have any expectations on when this will get looked at, given that this is an open source project. Just wanted to leave it here for future reference, in case it's useful to someone.

[joom]

If anyone from the maintainers is reading this, what's the intended status of this feature? Is it still work in progress, or is it some legacy that's no longer maintained?

Hi, I added the CertiCoq FFI command around early 2020. At the time, we were planning to do FFI by passing a collection of closures in C to the Coq function. Later that year we found that this is not as efficient as we want, so we haven't kept it up to date. We do not recommend doing FFI that way and this command will/should be deleted.

[kuruczgy]

I see, thanks. I guess my main question has been answered then.

I am not sure what your policy is with the GitHub issues, do as you wish with this one. You can either close it now since the main question has been answered, or keep it around until CertiCoq FFI has been removed and/or replaced with a better FFI solution.