Integration With C - ku-sldg/stairCASE GitHub Wiki

Entry

CakeML is always compiled with a single entry point named "main". This is a problem when integrating cakeML into c, where a main function likely already exists. The current solution is to take the assembly and replace all instances of "cdecl(main)" with "cdecl(cml_entry)", thereby renaming the entry point to "cml_entry" (Here, "c_decl(...)" is a macro that helps with portability when defining a symbol with the naming conventions of a c function. ). Of course we could use any other name, and we may wish to do so if we have multiple cakeML programs which require separate entries.

This find/replace procedure is risky, as we make the assumption that the string "cdecl(main)" only appears in the assembly with reference to the main function. If "cdecl(main)" were to be in a string literal, it too would be replaced (we should be thankful for the cdecl macro here, as "main" is a common word that might appear elsewhere in our code, "cdecl(main)" is not).

To call the cakeML code from c, you then simply declare cml_entry without giving it a definition like so: void cml_entry(void);. Then calling cml_entry() will invoke the cakeML code, assuming the c code is linked with the cakeML.

Exit

After calling cml_entry(), you cannot expect it to ever return like a normal function call. Instead, it will look for void cml_exit(int arg), typically defined in basis_ffi.c. You can regain control there.

FFI

You can define custom FFI functions for cakeML without any HOL tinkering. The c function must look something like the following: void ffifoo(unsigned char *c, long clen, unsigned char *a, long alen) {...}. Note, the name must begin with "ffi". From CakeML, you would then call the function like so: #(foo) strArg w8aArg where strArg is of type string, and w8aArg is of type word8Array (I am unsure why they are different types from CakeML, when they are both byte arrays in c).

To return a value from your ffi function, it seems the convention is to put that value in the second byte array.