Glue Code and FFI

Generated glue code

When the CertiCoq Generate Glue vernacular command is run, as described in the plugin page, CertiCoq 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 Coq values. For each of the Coq types specified in the CertiCoq Generate Glue command, you will have separate functions. For instance, for the list type, you would have:

value make_Coq_Init_Datatypes_list_nil(void)
{
  return 1;
}

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

value alloc_make_Coq_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 Coq values in C, the programmer can decide whether to put this information in the memory controlled by the CertiCoq garbage collector. We call this area the CertiCoq 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_Coq_Init_Datatypes_list_cons function is for creating Coq 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 CertiCoq garbage collector will not touch this piece of memory.
• The alloc_make_Coq_Init_Datatypes_list_cons function is for creating Coq values on the CertiCoq heap. It takes a tinfo argument, which contains information about the CertiCoq runtime. At the call site, the programmer must have this runtime argument to be able to allocate on the CertiCoq heap. We recommend this function for Coq values that will be treated purely.

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

unsigned int get_Coq_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 Coq 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 } coq_list; and treat the result of this function to be of type coq_list, but CertiCoq 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 Coq value representation. This is generalized for any type or any constructor.

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

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

void print_Coq_Init_Datatypes_list(value v, void print_param_A(value))
{
  unsigned int tag;
  void *args;
  tag = get_Coq_Init_Datatypes_list_tag(v);
  switch (tag) {
    case 0:
      printf(*(names_of_Coq_Init_Datatypes_list + tag));
      break;
    case 1:
      args = (get_Coq_Init_Datatypes_cons_args)(v);
      printf(lparen_lit);
      printf(*(names_of_Coq_Init_Datatypes_list + tag));
      printf(space_lit);
      print_param_A(*((value *) args + 0));
      printf(space_lit);
      print_Coq_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 Coq closures inside C.

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

If the programmer compiles a function definition with CertiCoq, they can use call with the compiled expression to call the compiled function with a certain Coq 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

...