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 --- kernel/csymtable.ml | 4 ++-- kernel/vm.ml | 6 +++--- kernel/vmvalues.ml | 21 +++++++++++++-------- kernel/vmvalues.mli | 3 +++ 8 files changed, 36 insertions(+), 61 deletions(-) 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_ */ diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index dfe3d8fb1..23b419473 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -26,7 +26,7 @@ open Cbytegen module NamedDecl = Context.Named.Declaration module RelDecl = Context.Rel.Declaration -external eval_tcode : tcode -> vm_global -> values array -> values = "coq_eval_tcode" +external eval_tcode : tcode -> atom array -> vm_global -> values array -> values = "coq_eval_tcode" type global_data = { mutable glob_len : int; mutable glob_val : values array } @@ -173,7 +173,7 @@ and eval_to_patch env (buff,pl,fv) = in let tc = patch buff pl slots in let vm_env = Array.map (slot_for_fv env) fv in - eval_tcode tc (vm_global global_data.glob_val) vm_env + eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env and val_of_constr env c = match compile ~fail_on_error:true env c with diff --git a/kernel/vm.ml b/kernel/vm.ml index 160575ac7..d7eedc226 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -42,11 +42,11 @@ external push_vstack : vstack -> int -> unit = "coq_push_vstack" (* interpreteur *) -external coq_interprete : tcode -> values -> vm_global -> vm_env -> int -> values = - "coq_interprete_ml" +external coq_interprete : tcode -> values -> atom array -> vm_global -> vm_env -> int -> values = + "coq_interprete_byte" "coq_interprete_ml" let interprete code v env k = - coq_interprete code v (Csymtable.get_global_data ()) env k + coq_interprete code v (get_atom_rel ()) (Csymtable.get_global_data ()) env k (* Functions over arguments *) diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 6377e947f..cbe8c9187 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -410,13 +410,20 @@ let check_fix f1 f2 = else false else false -external atom_rel : unit -> atom array = "get_coq_atom_tbl" -external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl" +let atom_rel : atom array ref = + let init i = Aid (RelKey i) in + ref (Array.init 40 init) + +let get_atom_rel () = !atom_rel + +let realloc_atom_rel n = + let n = min (n + 0x100) Sys.max_array_length in + let init i = Aid (RelKey i) in + let ans = Array.init n init in + atom_rel := ans let relaccu_tbl = - let atom_rel = atom_rel() in - let len = Array.length atom_rel in - for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done; + let len = Array.length !atom_rel in ref (Array.init len mkAccuCode) let relaccu_code i = @@ -425,9 +432,7 @@ let relaccu_code i = else begin realloc_atom_rel i; - let atom_rel = atom_rel () in - let nl = Array.length atom_rel in - for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done; + let nl = Array.length !atom_rel in relaccu_tbl := Array.init nl (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j); diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 1fa889288..550791b2c 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -72,6 +72,9 @@ type atom = | Aind of inductive | Asort of Sorts.t +val get_atom_rel : unit -> atom array +(** Global table of rels *) + (** Zippers *) type zipper = -- cgit v1.2.3