From fd5dc5b37e765bdb864e874c451d42d03d737792 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 3 Mar 2018 19:43:02 +0100 Subject: Moving the VM global atom table to a ML reference. --- kernel/byterun/coq_interp.c | 16 ++++++++++------ kernel/byterun/coq_interp.h | 7 ++++--- kernel/byterun/coq_memory.c | 37 +------------------------------------ kernel/byterun/coq_memory.h | 3 --- 4 files changed, 15 insertions(+), 48 deletions(-) (limited to 'kernel/byterun') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index ced2a175d..cfeb0a9ee 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -163,10 +163,10 @@ extern void caml_process_pending_signals(void); /* The interpreter itself */ value coq_interprete -(code_t coq_pc, value coq_accu, value coq_global_data, 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 */ - CAMLparam1(coq_global_data); + CAMLparam2(coq_atom_tbl, coq_global_data); /*Declaration des variables */ #ifdef PC_REG @@ -1515,12 +1515,16 @@ value coq_push_vstack(value stk, value max_stack_size) { return Val_unit; } -value coq_interprete_ml(value tcode, value a, value g, value e, value ea) { +value coq_interprete_ml(value tcode, value a, value t, value g, value e, value ea) { print_instr("coq_interprete"); - return coq_interprete((code_t)tcode, a, g, e, Long_val(ea)); + return coq_interprete((code_t)tcode, a, t, g, e, Long_val(ea)); print_instr("end coq_interprete"); } -value coq_eval_tcode (value tcode, value g, value e) { - return coq_interprete_ml(tcode, Val_unit, g, 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 189c9a127..c04e9e00b 100644 --- a/kernel/byterun/coq_interp.h +++ b/kernel/byterun/coq_interp.h @@ -17,9 +17,10 @@ value coq_push_arguments(value args); value coq_push_vstack(value stk); -value coq_interprete_ml(value tcode, value a, value g, 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_global_data, 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); -value coq_eval_tcode (value tcode, value g, value e); +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 40dbda866..b2917a55e 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -24,9 +24,6 @@ value * coq_stack_threshold; asize_t coq_max_stack_size = Coq_max_stack_size; /* global_data */ - -value coq_atom_tbl; - int drawinstr; /* interp state */ @@ -57,8 +54,6 @@ 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_atom_tbl, &coq_atom_tbl); /* Scan the stack */ for (i = coq_sp; i < coq_stack_high; i++) { (*action) (*i, i); @@ -77,16 +72,10 @@ void init_coq_stack() coq_max_stack_size = Coq_max_stack_size; } -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, Atom(0), Val_unit, 0); + coq_interprete(NULL, Val_unit, Atom(0), Atom(0), Val_unit, 0); } static int coq_vm_initialized = 0; @@ -102,7 +91,6 @@ value init_coq_vm(value unit) /* ML */ #endif /* THREADED_CODE */ /* Allocate the table of global and the stack */ init_coq_stack(); - init_coq_atom_tbl(40); /* Initialing the interpreter */ init_coq_interpreter(); @@ -146,29 +134,6 @@ void realloc_coq_stack(asize_t required_space) #undef shift } -value get_coq_atom_tbl(value unit) /* ML */ -{ - return coq_atom_tbl; -} - -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 06711ad70..9375b15de 100644 --- a/kernel/byterun/coq_memory.h +++ b/kernel/byterun/coq_memory.h @@ -34,7 +34,6 @@ extern value * coq_stack_threshold; /* global_data */ extern int coq_all_transp; -extern value coq_atom_tbl; extern int drawinstr; /* interp state */ @@ -51,8 +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_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_ */ -- cgit v1.2.3