From 74f6c8c40942d57ea66d9f28bd15309ce59438b6 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 22 Mar 2018 17:49:13 +0100 Subject: Wrap VM bytecode used on the OCaml side in an OCaml block. This prevents the existence of a few naked pointers to C heap from the OCaml heap. VM bytecode is represented as any block of size at least 1 whose first field points to a C-allocated string. This representation is compatible with the Coq VM representation of (potentially recursive) closures, which are already specifically tailored in the OCaml GC to be able to contain out-of-heap data. --- kernel/byterun/coq_memory.c | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'kernel/byterun/coq_memory.c') diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index b2917a55ee..9102af702e 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -10,6 +10,7 @@ #include #include +#include #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -46,7 +47,11 @@ value coq_static_alloc(value size) /* ML */ value accumulate_code(value unit) /* ML */ { - return (value) accumulate; + CAMLparam1(unit); + CAMLlocal1(res); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = accumulate; + CAMLreturn(res); } static void (*coq_prev_scan_roots_hook) (scanning_action); -- cgit v1.2.3 From 415c1dae83891f217952941b6bae3e0c7b027c76 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 26 Mar 2018 09:51:48 +0200 Subject: Make the VM accumulator look like an OCaml block. We allocate an additional header so that the accumulator is not a naked pointer. Indeed, it is contained in accumulator blocks which are scanned by the GC as their tags is 0. --- kernel/byterun/coq_memory.c | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'kernel/byterun/coq_memory.c') diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 9102af702e..3cf5fc092e 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -99,8 +99,12 @@ value init_coq_vm(value unit) /* ML */ /* Initialing the interpreter */ init_coq_interpreter(); - /* Some predefined pointer code */ - accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t)); + /* Some predefined pointer code. + * It is typically contained in accumlator blocks whose tag is 0 and thus + * scanned by the GC, so make it look like an OCaml block. */ + value accu_block = (value) coq_stat_alloc(2 * sizeof(value)); + Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \ + accumulate = (code_t) Val_hp(accu_block); *accumulate = VALINSTR(ACCUMULATE); /* Initialize GC */ -- cgit v1.2.3 From 5c0b2171844cee7a5344c535c2793e362d925e0c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 26 Mar 2018 10:02:54 +0200 Subject: Adapt the VM GC hook to handle the no-naked-pointers option flag. The Coq VM stack is scanned by the OCaml GC, but it can contain raw pointers to C-allocated strings standing for VM bytecode. If the the no-naked-pointers option is set, we perform the check that a stack value lives on the OCaml heap ourselves. --- kernel/byterun/coq_memory.c | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'kernel/byterun/coq_memory.c') diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 3cf5fc092e..542a05fd25 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -11,6 +11,7 @@ #include #include #include +#include #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -61,6 +62,10 @@ static void coq_scan_roots(scanning_action action) register value * i; /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { +#ifdef NO_NAKED_POINTERS + /* The VM stack may contain C-allocated bytecode */ + if (Is_block(*i) && !Is_in_heap_or_young(*i)) continue; +#endif (*action) (*i, i); }; /* Hook */ -- cgit v1.2.3