Interacting with CakeML via C function call

[tanyongkiam]

This issue is about setting up an alternative pathway to call into CakeML-generated code from C/C++.

Right now, the default exporter only allows running CakeML code as the "main" function.

One might like to instead call CakeML code as follows (instead of argc/argv, one could also imagine calling it with some other arguments):

//setup/other stuff
...  
int ret = cml_main(argc,argv);  
//do more stuff with ret  
...

The implementation could e.g., add a flag to the compiler to tell it the name to use for the exposed function.

[tanyongkiam]

I've tried this on x64:

    .globl  cdecl(cml_main)
    .globl  cdecl(argc)
    .globl  cdecl(argv)
cdecl(cml_main):
    movabs  $cdecl(argc), %rdx
    movabs  $cdecl(argv), %rcx
    movq    %rdi, 0(%rdx)  # %rdi stores argc
    movq    %rsi, 0(%rcx)  # %rsi stores argv
    pushq   %rbp
    movq    %rsp, %rbp  # move stack pointer
    pushq   %rbx        # save registers that CakeML could clobber
    pushq   %r12
    pushq   %r13
    pushq   %r14
    pushq   %r15
    movabs  $cake_main, %rdi        # arg1: entry address
    movabs  $cake_heap, %rsi        # arg2: first address of heap
    movabs  $cake_bitmaps, %rdx
    movq    %rdx, 0(%rsi)           # store bitmap pointer
    movabs  $cake_stack, %rdx       # arg3: first address of stack
    movabs  $cake_end, %rcx         # arg4: first address past the stack
    jmp     cake_main

/* CakeML FFI interface (each block is 16 bytes long) */

    .p2align 4

cake_clear:
    movq    %rdi, %rax
    jmp     ret_exit
    .p2align 4

cake_exit:
    movq    %rdi, %rax
    jmp     ret_exit
    .p2align 4

... CakeML bytes here ...

ret_exit:
    movq    -40(%rbp), %r15 # restore clobbered registers
    movq    -32(%rbp), %r14
    movq    -24(%rbp), %r13
    movq    -16(%rbp), %r12
    movq     -8(%rbp), %rbx
    movq    %rbp, %rsp  # restore stack pointer
    popq    %rbp        # pop base pointer
    ret

[sorear]

I think this is done? The exporter already generates a function named cml_main, and you can return control to C code with a FFI that calls longjmp (a better FFI would support just returning, but longjmp is standard C so I think this is good enough for now).

[tanyongkiam]

I think this was intended more for cml_main itself to be a callable C function rather than requiring a set_jmp long_jmp loop around it. i.e., so that e.g. int foo = cml_main(...) puts the return value from the CakeML call into foo and returns control to the caller.