Glue Code and FFI

Generated glue code

When the CertiRocq Generate Glue vernacular command is run, as described in the plugin page, CertiRocq creates a glue code file. This file does not contain the compiled program; these are functions in C that the programmer can use when writing foreign functions. Here is a list of what is are generated:

1. C functions to construct Rocq values. For each of the Rocq types specified in the CertiRocq Generate Glue command, you will have separate functions. For instance, for the list type, you would have:

value make_Corelib_Init_Datatypes_list_nil(void)
{
  return 1;
}

value make_Corelib_Init_Datatypes_list_cons(value arg0, value arg1, value *argv)
{
  // elided
}

value alloc_make_Corelib_Init_Datatypes_list_cons(struct thread_info *tinfo, value arg0, value arg1)
{
  // elided
}

The nil constructor takes no arguments, so it is represented as an integer in runtime.

The cons constructor is represented as a pointer to a part of memory that holds the arguments. When creating new Rocq values in C, the programmer can decide whether to put this information in the memory controlled by the CertiRocq garbage collector. We call this area the CertiRocq heap. Or the programmer can decide to manually allocate some memory for the arguments of the constructor. We will call this the C heap.

• The make_Corelib_Init_Datatypes_list_cons function is for creating Rocq values on the C heap. The last argument argv needs to have available memory for this function to write on, one word for each constructor. It also need a word right before where the pointer points to, to store header information. For mutable structures, we recommend allocating on the C heap, but the programmer is responsible for freeing this memory later or keeping track of what can be freed when. The CertiRocq garbage collector will not touch this piece of memory.
• The alloc_make_Corelib_Init_Datatypes_list_cons function is for creating Rocq values on the CertiRocq heap. It takes a tinfo argument, which contains information about the CertiRocq runtime. At the call site, the programmer must have this runtime argument to be able to allocate on the CertiRocq heap. We recommend this function for Rocq values that will be treated purely.

2. A function to get which constructor a Rocq value representation belongs to. (the tag of the constructor) For each of the Rocq types specified in the CertiRocq Generate Glue command, you will have a separate function. For instance, for the list type, this would be:

unsigned int get_Corelib_Init_Datatypes_list_tag(value v)
{
  // elided
}

A tag is an index (starting from 0) denoting the order of the constructor that was used to create the value at hand. When the C representation of a Rocq value is passed into this function, it returns 0 for nil and 1 for cons. For further ease of use the programmer can define typedef enum { NIL, CONS } rocq_list; and treat the result of this function to be of type rocq_list, but CertiRocq does not generate this yet.

For a type Inductive T := A | B | C | D., A would have the tag 0, B would have 1, C would have 2, and D would have 3, regardless of what arguments the constructors of T take. There is also a concept of constructor ordinals in the compiler, which is counting boxed and unboxed constructor separately, starting from 0, but that should not be confused with tags. We advise FFI users not to use ordinals.

3. A function to extract arguments from a Rocq value representation. This is generalized for any type or any constructor.

value *get_args(value v) {
  return (value *) v;
}

4. C functions to print Rocq value representations as S-expressions. For each of the Rocq types specified in the CertiRocq Generate Glue command, you will have a separate function. For instance, for the list type, this would be:

void print_Corelib_Init_Datatypes_list(value v, void print_param_A(value))
{
  unsigned int tag;
  void *args;
  tag = get_Corelib_Init_Datatypes_list_tag(v);
  switch (tag) {
    case 0:
      printf(*(names_of_Corelib_Init_Datatypes_list + tag));
      break;
    case 1:
      args = (get_Corelib_Init_Datatypes_cons_args)(v);
      printf(lparen_lit);
      printf(*(names_of_Corelib_Init_Datatypes_list + tag));
      printf(space_lit);
      print_param_A(*((value *) args + 0));
      printf(space_lit);
      print_Corelib_Init_Datatypes_list(*((value *) args + 1), print_param_A);
      printf(rparen_lit);
      break;
    
  }
}

Notice how since list is a parameterized type, the printing functions take a function pointer to deal with values of the parameter type.

5. A way to call Rocq closures inside C.

value call(struct thread_info *tinfo, value clo, value arg)

If the programmer compiles a function definition with CertiRocq, they can use call with the compiled expression to call the compiled function with a certain Rocq value representation in C, which they can also create with the glue functions here.

---

The glue code generator also includes certain string literals and helper functions used in the glue code generation.

Examples

...