From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- kernel/byterun/coq_fix_code.c | 51 +++++++++++++----------- kernel/byterun/coq_fix_code.h | 2 +- kernel/byterun/coq_interp.c | 55 ++++++++++++++++++-------- kernel/byterun/coq_interp.h | 9 ++--- kernel/byterun/coq_memory.c | 92 +++++++++---------------------------------- kernel/byterun/coq_memory.h | 7 ---- kernel/byterun/coq_values.c | 31 ++++++++++++++- 7 files changed, 119 insertions(+), 128 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index d5feafbf..be2b05da 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -18,6 +18,7 @@ #include #include #include +#include #include #include "coq_instruct.h" #include "coq_fix_code.h" @@ -78,38 +79,41 @@ void * coq_stat_alloc (asize_t sz) } value coq_makeaccu (value i) { - code_t q; - code_t res = coq_stat_alloc(2 * sizeof(opcode_t)); - q = res; + CAMLparam1(i); + CAMLlocal1(res); + code_t q = coq_stat_alloc(2 * sizeof(opcode_t)); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = q; *q++ = VALINSTR(MAKEACCU); *q = (opcode_t)Int_val(i); - return (value)res; + CAMLreturn(res); } value coq_pushpop (value i) { - code_t res; - int n; - n = Int_val(i); + CAMLparam1(i); + CAMLlocal1(res); + code_t q; + res = caml_alloc_small(1, Abstract_tag); + int n = Int_val(i); if (n == 0) { - res = coq_stat_alloc(sizeof(opcode_t)); - *res = VALINSTR(STOP); - return (value)res; + q = coq_stat_alloc(sizeof(opcode_t)); + Code_val(res) = q; + *q = VALINSTR(STOP); + CAMLreturn(res); } else { - code_t q; - res = coq_stat_alloc(3 * sizeof(opcode_t)); - q = res; + q = coq_stat_alloc(3 * sizeof(opcode_t)); + Code_val(res) = q; *q++ = VALINSTR(POP); *q++ = (opcode_t)n; *q = VALINSTR(STOP); - return (value)res; + CAMLreturn(res); } } value coq_is_accumulate_code(value code){ - code_t q; + code_t q = Code_val(code); int res; - q = (code_t)code; res = Is_instruction(q,ACCUMULATE); return Val_bool(res); } @@ -132,11 +136,14 @@ value coq_is_accumulate_code(value code){ #define COPY32(dst,src) (*dst=*src) #endif /* ARCH_BIG_ENDIAN */ -value coq_tcode_of_code (value code, value size) { - code_t p, q, res; - asize_t len = (asize_t) Long_val(size); - res = coq_stat_alloc(len); - q = res; +value coq_tcode_of_code (value code) { + CAMLparam1 (code); + CAMLlocal1 (res); + code_t p, q; + asize_t len = (asize_t) caml_string_length(code); + res = caml_alloc_small(1, Abstract_tag); + q = coq_stat_alloc(len); + Code_val(res) = q; len /= sizeof(opcode_t); for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) { opcode_t instr; @@ -166,5 +173,5 @@ value coq_tcode_of_code (value code, value size) { for(i=0; i #include #include +#include #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -163,8 +164,11 @@ extern void caml_process_pending_signals(void); /* The interpreter itself */ value coq_interprete -(code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args) +(code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args) { + /* coq_accu is not allocated on the OCaml heap */ + CAMLparam2(coq_atom_tbl, coq_global_data); + /*Declaration des variables */ #ifdef PC_REG register code_t pc PC_REG; @@ -196,7 +200,7 @@ value coq_interprete coq_instr_table = (char **) coq_jumptable; coq_instr_base = coq_Jumptbl_base; #endif - return Val_unit; + CAMLreturn(Val_unit); } #if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32) coq_jumptbl_base = coq_Jumptbl_base; @@ -626,7 +630,7 @@ value coq_interprete print_instr("CLOSUREREC"); if (nvars > 0) *--sp = accu; /* construction du vecteur de type */ - Alloc_small(accu, nfuncs, 0); + Alloc_small(accu, nfuncs, Abstract_tag); for(i = 0; i < nfuncs; i++) { Field(accu,i) = (value)(pc+pc[i]); } @@ -662,7 +666,7 @@ value coq_interprete print_instr("CLOSURECOFIX"); if (nvars > 0) *--sp = accu; /* construction du vecteur de type */ - Alloc_small(accu, nfunc, 0); + Alloc_small(accu, nfunc, Abstract_tag); for(i = 0; i < nfunc; i++) { Field(accu,i) = (value)(pc+pc[i]); } @@ -1028,7 +1032,7 @@ value coq_interprete CHECK_STACK(nargs+1); sp -= nargs; for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); - *--sp = accu; // Last argument is the pointer to the suspension + *--sp = accu; // Leftmost argument is the pointer to the suspension print_lint(nargs); coq_extra_args = nargs; pc = Code_val(coq_env); // Trigger evaluation @@ -1068,12 +1072,22 @@ value coq_interprete } } *--sp = accu; - /* We create the switch zipper */ - Alloc_small(accu, 5, Default_tag); - Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; - Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; - Field(accu, 4) = coq_env; - sp++;sp[0] = accu; + /* Create bytecode wrappers */ + Alloc_small(accu, 1, Abstract_tag); + Code_val(accu) = typlbl; + *--sp = accu; + Alloc_small(accu, 1, Abstract_tag); + Code_val(accu) = swlbl; + *--sp = accu; + /* We create the switch zipper */ + Alloc_small(accu, 5, Default_tag); + Field(accu, 0) = sp[1]; + Field(accu, 1) = sp[0]; + Field(accu, 2) = sp[3]; + Field(accu, 3) = sp[2]; + Field(accu, 4) = coq_env; + sp += 3; + sp[0] = accu; /* We create the atom */ Alloc_small(accu, 2, ATOM_SWITCH_TAG); Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; @@ -1460,7 +1474,7 @@ value coq_interprete Instruct(STOP){ print_instr("STOP"); coq_sp = sp; - return accu; + CAMLreturn(accu); } @@ -1473,7 +1487,8 @@ value coq_interprete #endif } -value coq_push_ra(value tcode) { +value coq_push_ra(value code) { + code_t tcode = Code_val(code); print_instr("push_ra"); coq_sp -= 3; coq_sp[0] = (value) tcode; @@ -1512,12 +1527,18 @@ value coq_push_vstack(value stk, value max_stack_size) { return Val_unit; } -value coq_interprete_ml(value tcode, value a, value e, value ea) { +value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) { + // Registering the other arguments w.r.t. the OCaml GC is done by coq_interprete + CAMLparam1(tcode); print_instr("coq_interprete"); - return coq_interprete((code_t)tcode, a, e, Long_val(ea)); + CAMLreturn (coq_interprete(Code_val(tcode), a, t, g, e, Long_val(ea))); print_instr("end coq_interprete"); } -value coq_eval_tcode (value tcode, value e) { - return coq_interprete_ml(tcode, Val_unit, e, 0); +value coq_interprete_byte(value* argv, int argn){ + return coq_interprete_ml(argv[0], argv[1], argv[2], argv[3], argv[4], argv[5]); +} + +value coq_eval_tcode (value tcode, value t, value g, value e) { + return coq_interprete_ml(tcode, Val_unit, t, g, e, 0); } diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h index 60865c32..c04e9e00 100644 --- a/kernel/byterun/coq_interp.h +++ b/kernel/byterun/coq_interp.h @@ -17,11 +17,10 @@ value coq_push_arguments(value args); value coq_push_vstack(value stk); -value coq_interprete_ml(value tcode, value a, value e, value ea); +value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea); +value coq_interprete_byte(value* argv, int argn); value coq_interprete - (code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args); - -value coq_eval_tcode (value tcode, value e); - + (code_t coq_pc, value coq_accu, value coq_atom_tbl, value coq_global_data, value coq_env, long coq_extra_args); +value coq_eval_tcode (value tcode, value t, value g, value e); diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 45cfae50..542a05fd 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -10,6 +10,8 @@ #include #include +#include +#include #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -24,10 +26,6 @@ value * coq_stack_threshold; asize_t coq_max_stack_size = Coq_max_stack_size; /* global_data */ - -value coq_global_data; -value coq_atom_tbl; - int drawinstr; /* interp state */ @@ -50,7 +48,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); @@ -58,11 +60,12 @@ static void (*coq_prev_scan_roots_hook) (scanning_action); static void coq_scan_roots(scanning_action action) { register value * i; - /* Scan the global variables */ - (*action)(coq_global_data, &coq_global_data); - (*action)(coq_atom_tbl, &coq_atom_tbl); /* 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 */ @@ -79,24 +82,10 @@ void init_coq_stack() coq_max_stack_size = Coq_max_stack_size; } -void init_coq_global_data(long requested_size) -{ - int i; - coq_global_data = alloc_shr(requested_size, 0); - for (i = 0; i < requested_size; i++) - Field (coq_global_data, i) = Val_unit; -} - -void init_coq_atom_tbl(long requested_size){ - int i; - coq_atom_tbl = alloc_shr(requested_size, 0); - for (i = 0; i < requested_size; i++) Field (coq_atom_tbl, i) = Val_unit; -} - void init_coq_interpreter() { coq_sp = coq_stack_high; - coq_interprete(NULL, Val_unit, Val_unit, 0); + coq_interprete(NULL, Val_unit, Atom(0), Atom(0), Val_unit, 0); } static int coq_vm_initialized = 0; @@ -112,13 +101,15 @@ value init_coq_vm(value unit) /* ML */ #endif /* THREADED_CODE */ /* Allocate the table of global and the stack */ init_coq_stack(); - init_coq_global_data(Coq_global_data_Size); - init_coq_atom_tbl(40); /* 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 */ @@ -157,53 +148,6 @@ void realloc_coq_stack(asize_t required_space) #undef shift } -value get_coq_global_data(value unit) /* ML */ -{ - return coq_global_data; -} - -value get_coq_atom_tbl(value unit) /* ML */ -{ - return coq_atom_tbl; -} - -value realloc_coq_global_data(value size) /* ML */ -{ - mlsize_t requested_size, actual_size, i; - value new_global_data; - requested_size = Long_val(size); - actual_size = Wosize_val(coq_global_data); - if (requested_size >= actual_size) { - requested_size = (requested_size + 0x100) & 0xFFFFFF00; - new_global_data = alloc_shr(requested_size, 0); - for (i = 0; i < actual_size; i++) - initialize(&Field(new_global_data, i), Field(coq_global_data, i)); - for (i = actual_size; i < requested_size; i++){ - Field (new_global_data, i) = Val_long (0); - } - coq_global_data = new_global_data; - } - return Val_unit; -} - -value realloc_coq_atom_tbl(value size) /* ML */ -{ - mlsize_t requested_size, actual_size, i; - value new_atom_tbl; - requested_size = Long_val(size); - actual_size = Wosize_val(coq_atom_tbl); - if (requested_size >= actual_size) { - requested_size = (requested_size + 0x100) & 0xFFFFFF00; - new_atom_tbl = alloc_shr(requested_size, 0); - for (i = 0; i < actual_size; i++) - initialize(&Field(new_atom_tbl, i), Field(coq_atom_tbl, i)); - for (i = actual_size; i < requested_size; i++) - Field (new_atom_tbl, i) = Val_long (0); - coq_atom_tbl = new_atom_tbl; - } - return Val_unit; -} - value coq_set_drawinstr(value unit) { drawinstr = 1; diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h index cec34f56..9375b15d 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -20,7 +20,6 @@ #define Coq_stack_size (4096 * sizeof(value)) #define Coq_stack_threshold (256 * sizeof(value)) -#define Coq_global_data_Size (4096 * sizeof(value)) #define Coq_max_stack_size (256 * 1024) #define TRANSP 0 @@ -34,9 +33,7 @@ extern value * coq_stack_threshold; /* global_data */ -extern value coq_global_data; extern int coq_all_transp; -extern value coq_atom_tbl; extern int drawinstr; /* interp state */ @@ -53,10 +50,6 @@ value init_coq_vm(value unit); /* ML */ value re_init_coq_vm(value unit); /* ML */ void realloc_coq_stack(asize_t required_space); -value get_coq_global_data(value unit); /* ML */ -value realloc_coq_global_data(value size); /* ML */ -value get_coq_atom_tbl(value unit); /* ML */ -value realloc_coq_atom_tbl(value size); /* ML */ value coq_set_transp_value(value transp); /* ML */ value get_coq_transp_value(value unit); /* ML */ #endif /* _COQ_MEMORY_ */ diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c index 528babeb..e05f3fb8 100644 --- a/kernel/byterun/coq_values.c +++ b/kernel/byterun/coq_values.c @@ -9,6 +9,7 @@ /***********************************************************************/ #include +#include #include "coq_fix_code.h" #include "coq_instruct.h" #include "coq_memory.h" @@ -58,10 +59,36 @@ value coq_offset_closure(value v, value offset){ return (value)&Field(v, Int_val(offset)); } +value coq_set_bytecode_field(value v, value i, value code) { + // No write barrier because the bytecode does not live on the OCaml heap + Field(v, Long_val(i)) = (value) Code_val(code); + return Val_unit; +} + value coq_offset_tcode(value code,value offset){ - return((value)((code_t)code + Int_val(offset))); + CAMLparam1(code); + CAMLlocal1(res); + res = caml_alloc_small(1, Abstract_tag); + Code_val(res) = Code_val(code) + Int_val(offset); + CAMLreturn(res); } -value coq_int_tcode(value code, value offset) { +value coq_int_tcode(value pc, value offset) { + code_t code = Code_val(pc); return Val_int(*((code_t) code + Int_val(offset))); } + +value coq_tcode_array(value tcodes) { + CAMLparam1(tcodes); + CAMLlocal2(res, tmp); + int i; + /* Assumes that the vector of types is small. This was implicit in the + previous code which was building the type array using Alloc_small. */ + res = caml_alloc_small(Wosize_val(tcodes), Default_tag); + for (i = 0; i < Wosize_val(tcodes); i++) { + tmp = caml_alloc_small(1, Abstract_tag); + Code_val(tmp) = (code_t) Field(tcodes, i); + Store_field(res, i, tmp); + } + CAMLreturn(res); +} -- cgit v1.2.3