basis_ffi.c

Initially, I was confused by the basis_ffi.c file which you link against both the cake compiler, and compiled cakeml code. First off, in the example provided with the cakeml download, it has you link the same basis_ffi.c against the precompiled cake.S, as well as your result.S which you compiled with the cake executable. However, you don't actually have to use the same basis_ffi.c for both of these cases. This become especially clear when you attempt to use cake as a cross compiler. To do this, you will need to compile basis_ffi.c in your native language to link against cake.S, and then again in your target language to link against result.S. Furthermore, what if your target OS is different than the machine you are compiling with? This is the case when we build cakeML applications for sel4. In this case, we will use the default basis_ffi.c with cake.S to get our compiler executable, and a totally different basis_ffi.c source file for our sel4 cakeML application (the default basis_ffi.c makes use of linux system calls which do not exist on sel4).

Does this all seem weird to you? It did to me. I couldn't figure out why we needed basis_ffi.c for both the compiler and compiled cake code. The key to understanding is realizing that our cake.S is compiled cake code. Like many other compilers, it is bootstrapped, ie written in the same language it compiles and compiled by a previous version of itself (obviously the first version would have had to be compiled with something else though). It needs a basis_ffi.c file for the same reason any other piece of compiled cake code does. Compiled cakeml code is largely OS agnostic, and it makes references to ffi functions in basis_ffi.c to do things like IO, which is incredibly platform specific. So, the precompiled cake.S needs basis_ffi.c to do things like print to the console with errors.

Finally, "basis_ffi.c" is simply the name the cakeML people use, but there is nothing special about it. As we can see in the camkes implementation, you can name it whatever you like, and even separate the contents into multiple files. At the end of the day, cakeml code is simply compiled with reference to external symbols for its FFI functions. You need to define them somewhere, and link them together to resolve those external symbols.