Joseph Ferano
e403e74b90
The verdict, as DISCUSS.md item 15. One function goes from Tast to machine
code and answers correctly, so the question is not whether it can be done.
Three findings decide the shape. Layout is already owned -- emit.ml computes
C struct layout for DWARF and is tested against LLVM's own answer -- so the
silent-drift risk item 10 feared most does not arise. The C boundary is the
easy half, because check.ml already rejects aggregates in a declare and the
shim flattens them. And the hard half was not on anyone's list: Flan calling
Flan passes aggregates by value, and LLVM's lowering of a first-class struct
is per-field rather than the C psABI -- { i8, float } comes back in al and
xmm0 where C would pack it into rax, and a %vec return takes a hidden sret
pointer that does not appear in the define line. The internal convention is
an implementation, not a document.
The audit stands on its own: overflow, shifts and evaluation order are
defined; division by zero, INT64_MIN/-1, the float cast, Uninit and
unreachable are not. Uninit is the one that bites, because poison is where
the two backends are supposed to differ.
Unloading: the shadow stack answers the running half and every dev-build
function is on it -- only the slot table is gated, not the frame. It cannot
answer the pointed-into half, which BUILT.md says is the actual reason
nothing is dlclose'd. Escaped function values need a rule the language does
not have.
103 lines
4.2 KiB
C
103 lines
4.2 KiB
C
/* The three things OCaml cannot do for itself: get executable memory, put
|
|
* bytes in it, and jump to them. Everything interesting is in x86.ml; this
|
|
* file is deliberately dumb.
|
|
*
|
|
* Shaped after lib/dynload_stubs.c's rule, which spike/embed took verbatim for
|
|
* the same reason: the boundary passes pointers and scalars, never an OCaml
|
|
* [value] into foreign storage. Nothing here keeps anything.
|
|
*
|
|
* RW then mprotect to R+X, never RWX in one mmap: a hardened kernel may refuse
|
|
* a writable-executable anonymous mapping outright, and a policy denial that
|
|
* comes back as a null pointer reads exactly like an encoding bug. */
|
|
|
|
#include <caml/mlvalues.h>
|
|
#include <caml/memory.h>
|
|
#include <caml/alloc.h>
|
|
#include <caml/fail.h>
|
|
|
|
#include <sys/mman.h>
|
|
#include <string.h>
|
|
#include <stdint.h>
|
|
#include <stdio.h>
|
|
#include <dlfcn.h>
|
|
|
|
value spike_jit_alloc(value vlen) {
|
|
size_t len = (size_t)Long_val(vlen);
|
|
void *p = mmap(NULL, len, PROT_READ | PROT_WRITE,
|
|
MAP_PRIVATE | MAP_ANONYMOUS, -1, 0);
|
|
if (p == MAP_FAILED) caml_failwith("spike_jit_alloc: mmap failed");
|
|
return caml_copy_nativeint((intnat)p);
|
|
}
|
|
|
|
value spike_jit_write(value vp, value vbytes) {
|
|
char *p = (char *)Nativeint_val(vp);
|
|
memcpy(p, String_val(vbytes), caml_string_length(vbytes));
|
|
return Val_unit;
|
|
}
|
|
|
|
value spike_jit_protect(value vp, value vlen) {
|
|
void *p = (void *)Nativeint_val(vp);
|
|
if (mprotect(p, (size_t)Long_val(vlen), PROT_READ | PROT_EXEC) != 0)
|
|
caml_failwith("spike_jit_protect: mprotect failed");
|
|
return Val_unit;
|
|
}
|
|
|
|
/* Every Flan function's emitted signature is its parameters followed by the
|
|
* transfer channel (emit.ml, [signature]), so the trampolines below all pass a
|
|
* trailing pointer. Nothing in the spike transfers, so it is NULL. */
|
|
typedef int64_t (*fn0)(void *);
|
|
typedef int64_t (*fn1)(int64_t, void *);
|
|
typedef int64_t (*fn2)(int64_t, int64_t, void *);
|
|
|
|
value spike_call0(value vp) {
|
|
return caml_copy_int64(((fn0)Nativeint_val(vp))(NULL));
|
|
}
|
|
value spike_call1(value vp, value a) {
|
|
return caml_copy_int64(((fn1)Nativeint_val(vp))(Int64_val(a), NULL));
|
|
}
|
|
value spike_call2(value vp, value a, value b) {
|
|
return caml_copy_int64(((fn2)Nativeint_val(vp))(Int64_val(a), Int64_val(b), NULL));
|
|
}
|
|
|
|
value spike_sym(value vname) {
|
|
void *h = dlsym(RTLD_DEFAULT, String_val(vname));
|
|
if (h == NULL) caml_failwith("spike_sym: not found");
|
|
return caml_copy_nativeint((intnat)h);
|
|
}
|
|
|
|
/* ── The C side of the ABI probes ──────────────────────────────────── */
|
|
|
|
/* Eight integers: six in registers, two on the stack, which is the case a
|
|
* register-only convention silently gets wrong. The answer is positional so a
|
|
* swapped pair cannot pass. */
|
|
int64_t spike_probe8(int64_t a, int64_t b, int64_t c, int64_t d,
|
|
int64_t e, int64_t f, int64_t g, int64_t h) {
|
|
return a * 1 + b * 10 + c * 100 + d * 1000 + e * 10000 + f * 100000
|
|
+ g * 1000000 + h * 10000000;
|
|
}
|
|
|
|
/* The alignment check, and it has to be done with an aligned load rather than
|
|
* by reading rsp, because that is how raylib finds out: the SysV ABI promises
|
|
* rsp % 16 == 0 at the call instruction, so on entry rsp+8 is aligned, and a
|
|
* callee that spills an __m128 to its frame faults when it is not. -O2 is what
|
|
* turns this into an actual movaps; without it the bug hides. */
|
|
__attribute__((noinline))
|
|
int64_t spike_probe_align(int64_t x) {
|
|
volatile double v[2] __attribute__((aligned(16))) = { 1.0, 2.0 };
|
|
/* Reading rsp as well, so a failure says which of the two it was. */
|
|
uintptr_t sp;
|
|
__asm__ volatile ("mov %%rsp, %0" : "=r"(sp));
|
|
if ((sp % 16) != 8) return -1; /* entry rsp is call-site rsp minus 8 */
|
|
return x + (int64_t)(v[0] + v[1]);
|
|
}
|
|
|
|
/* No float probe either, for a plainer reason: this emitter has no SSE, so
|
|
* there is nothing here that could call one. Floats are counted as work in
|
|
* item 15 rather than claimed as done.
|
|
*
|
|
* And no struct-by-value probe, and that is a finding rather than an
|
|
* omission: check.ml rejects an aggregate in a [declare] signature and the
|
|
* generated shim flattens every one, so no Flan-emitted call ever passes a
|
|
* struct to C. The aggregate problem is real but it is on the Flan-to-Flan
|
|
* side, which is measured in DISCUSS.md item 15 and not from here. */
|