Skip to content

The CertiCoq plugin

Jump to bottom
Matthieu Sozeau edited this page Feb 8, 2024 · 22 revisions

The CertiCoq plugin provides commands to compile Gallina programs to Clight, to register external functions realized in C, and to compile and run the generated C code. It uses the extracted sources of CertiCoq to OCaml.

The CertiCoq plugin can be loaded with:

From CertiCoq.Plugin Require Import CertiCoq.

For usage information type:

CertiCoq -help.

Compiling Gallina to C

CertiCoq Compile <options> <definition>.

This command (recursively) compiles a Gallina definition to a C program. The relevant environment dependencies are compiled as well. The command will generate two files: filename.c and filename.h: The generated C code and the corresponding header file.

By default, the filename will be the fully qualified name of the definition to be compiled.

The command options are:

  • -file "filename": Specifies the filename of the generated C files.

  • -ext "suff": Specifies a suffix to be appended to the filename.

  • -cps: Compiles the program to continuation-passing style. The default is direct-style compilation. Note that CPS is generally less efficient and it will result in around 2x overhead.

  • -time: Prints timing info for each compilation phase.

  • -O N, where N=0 or N=1: N=1 (default) will enable the λΑΝF transformation lambda-lifting that will try to allocate closure environments is registers. N=0 disables lambda lifting.

  • -time_anf: print timing info for each phase of the λANF pipeline.

  • -args N : Maximum number of (user) arguments in the generated C code. The default is N=5. The rest of the arguments are passed using a global array.

Note that compiling code that contains computationally relevant axioms will fail, unless user specifies C functions that realize the axiom. (next section).

Extracting constants to C functions

CertiCoq supports mapping Gallina constants (including axioms) to specific C functions.

CertiCoq Compile <options> <definitions>
  Extract Constants [ constant1 => "c_function1" (with tinfo)?,
                      ... , 
                      constantN => "c_functionN" ]
  Include [ "file1.h", "/foo/bar.h" as absolute, ..., "fileM.h" as library, "file_C.h" "file_coq.h" as library ].

The above command will map and specify which Gallina constants are compiled to which functions and the files that contain the function declarations (that will be included in the generated C code). The optional with tinfo annotation is necessary when the C code needs to use the garbage collector's interface, e.g. when it allocates. By default the includes are used as is when compiling the C code, so they are #included in quotes and should be in the same directory as the generated code. The as absolute qualifier passes the absolute path while the as library qualifier expects the file to be in CertiCoq's runtime directory (usually `coqc -where`/user-contrib/CertiCoq/Plugin/runtime). When both "file_C.h" and "file_coq.h" are given with the as library qualifier, the first is used for all the commands below except for CertiCoq Eval which allows to dynamically link the code to Coq, in which case file_coq.h and file_coq.c can use OCaml's FFI to call back Coq APIs.

An N-ary Gallina function should be implemented with an N-ary C function unless it allocates, in case it gets an additional first argument of type thread_info* (defined in gc_stack.h or gc.h). Note that in Gallina the constant is still a first-class function that can be handled as an ordinary function (e.g., partial application).

A 0-ary Gallina definition should be implemented with a 0-ary C function.

The arguments and the results of the C functions must fit into machine integers (default 64 bits). Opaque datatypes realized in C must be either pointers outside the CertiCoq heap or have a 64-bit unboxed representation with the least significant bit set to 1 (for compatibility with CertiCoq's garbage collector).

For modular registration of extracted constants, use the CertiCoq Register command:

CertiCoq Register 
  [ constant1 => "c_function1", 
    ... , 
    constantN => "c_functionN" ]
  Include [ "file1.h", ... , "fileM.h" ].

The effects of CertiCoq Register commands can be accumulated to register FFI functions, and are taken into account in subsequent calls to the CertiCoq Compile commands.

If you are writing foreign functions in C, you will want to generate glue code. The command that generates glue code is CertiCoq Generate Glue:

CertiCoq Generate Glue -file "glue" [ bool, nat, option ].

The code generated through this command is described in more detail in a separate page.

Default FFI implementations

When loading CertiCoq.CertiCoq, one gets FFI implementations for primitive integer (CertiCoq.PrimInt63) and floating point (CertiCoq.PrimFloats) operations along with an interface for calling Coq back CertiCoq.CoqMsgFFI. This module provides the following functions that are realized by calling back Coq:

Axiom (coq_msg_info : string -> unit).
Axiom (coq_msg_notice : string -> unit).
Axiom (coq_msg_debug : string -> unit).
Axiom (coq_user_error : string -> unit).

These send message to the various channels available in Coq's IDEs (info, notices, debug) or raise an error.

Compiling the generated C code

Once the C files are generated they can be compiled with an ordinary C compiler (like GCC or Clang) or the CompCert verified compiler. The generated C files must be linked with the garbage collector.

This is currently done manually:

  • The files gc_stack.c (or gc.c if -cps is used), gc.h, values.h must be included (and .o files linked) from the RUNTIME_PATH directory which one can define as:
RUNTIME_PATH=`coqc -where`/user-contrib/CertiCoq/Plugin/runtime/

The recommended compilation command is then:

gcc -o <file> -Wno-everything -O2 -fomit-frame-pointer -I ${RUNTIME_PATH} -L ${RUNTIME_PATH} ${RUNTIME_LIBS} filename.c glue.c <other_files>

where filename.c is the generated C code, glue.c is the generated glue code, and ${RUNTIME_LIBS} is the CertiCoq runtime including the garbage collector implementation and FFI bindings.

There are a few options for ${RUNTIME_LIBS}:

  • It must include gc_stack.o when using the ANF pipeline or gc.o when using the CPS pipeline.
  • If the code is expected to be linked to Coq afterwards, use coq_ffi.o to bind the coq_msg_* functions with Coq's code. Otherwise use coq_c_ffi.o to bind those to functions that print to standard output and standard error, or exit the program after printing a message on coq_user_error.
  • If the code is using primitive integers or floats, it must include prim_int63.o and prim_floats.o respectively.

Hence the standard setting to build a standalone executable is:

RUNTIME_LIBS = gc_stack.o coq_c_ffi.o prim_int63.o prim_floats.o

Compiling and running programs

The CertiCoq Eval command provides an all-in-one command that produces C files, compiles them with gcc (preferably) or clang-11, dynamically loads the code and runs it, finally reifying the result to a Coq term. In this case the libs are:

RUNTIME_LIBS = gc_stack.o coq_ffi.o prim_int63.o prim_floats.o

The certicoq_eval c k tactic compiles and evaluates c and passes the reified result to the ltac continuation function k (usually of the form ltac:(fun c_value => ...). Beware that at Qed time, Coq cannot call back the compiler, any conversion between c and c_value that is necessary for typechecking will be performed by the standard conversion algorithm of Coq.

Compiling and running standalone programs

The CertiCoq Run command provides an all-in-one command that produces C files, compiles them with gcc (preferably) or clang-11, and runs them, redirecting standard output to Coq's info channel and standard error to Coq's warnings channel. The generated program can also be run standalone outside of Coq in this case. The libraries in this case are:

RUNTIME_LIBS = gc_stack.o coq_c_ffi.o prim_int63.o prim_floats.o

Printing λANF

The CertiCoq plugin allows to emit λANF, the core intermediate representation of CertiCoq.

CertiCoq Show IR <options> <definition>.

CertiCoq Show IR <options> <definition> 
  Extract Constants [ constant1 => "c_function1", 
                      ... , 
                      constantN => "c_functionN" ].

Note that the program is printed after compilation through the λANF pipeline, and it is closure-converted and hoisted (i.e., all functions are defined at the top-level, just as a C program).

Clone this wiki locally