aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-03-02 15:41:50 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-03-26 08:57:39 +0200
commitb5aed34bb8bbdda27646720db29a8d47c79653b9 (patch)
treeab5ca6003048afc0b8d0c2c4d9bce7e7a079cce2
parente128900aee63c972d7977fd47e3fd21649b63409 (diff)
Moving the VM global data to a ML reference.
-rw-r--r--kernel/byterun/coq_interp.c17
-rw-r--r--kernel/byterun/coq_interp.h8
-rw-r--r--kernel/byterun/coq_memory.c37
-rw-r--r--kernel/byterun/coq_memory.h4
-rw-r--r--kernel/csymtable.ml31
-rw-r--r--kernel/csymtable.mli2
-rw-r--r--kernel/kernel.mllib2
-rw-r--r--kernel/vm.ml7
-rw-r--r--kernel/vmvalues.ml3
-rw-r--r--kernel/vmvalues.mli3
10 files changed, 48 insertions, 66 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index af89712d5..ced2a175d 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -163,8 +163,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_global_data, value coq_env, long coq_extra_args)
{
+ /* coq_accu is not allocated on the OCaml heap */
+ CAMLparam1(coq_global_data);
+
/*Declaration des variables */
#ifdef PC_REG
register code_t pc PC_REG;
@@ -196,7 +199,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;
@@ -1460,7 +1463,7 @@ value coq_interprete
Instruct(STOP){
print_instr("STOP");
coq_sp = sp;
- return accu;
+ CAMLreturn(accu);
}
@@ -1512,12 +1515,12 @@ 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 g, value e, value ea) {
print_instr("coq_interprete");
- return coq_interprete((code_t)tcode, a, e, Long_val(ea));
+ return coq_interprete((code_t)tcode, a, 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_eval_tcode (value tcode, value g, value e) {
+ return coq_interprete_ml(tcode, Val_unit, g, e, 0);
}
diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h
index 60865c32e..189c9a127 100644
--- a/kernel/byterun/coq_interp.h
+++ b/kernel/byterun/coq_interp.h
@@ -17,11 +17,9 @@ 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 g, value e, value ea);
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_global_data, value coq_env, long coq_extra_args);
+value coq_eval_tcode (value tcode, value g, value e);
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 45cfae509..40dbda866 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -25,7 +25,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size;
/* global_data */
-value coq_global_data;
value coq_atom_tbl;
int drawinstr;
@@ -59,7 +58,6 @@ 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++) {
@@ -79,14 +77,6 @@ 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);
@@ -96,7 +86,7 @@ void init_coq_atom_tbl(long requested_size){
void init_coq_interpreter()
{
coq_sp = coq_stack_high;
- coq_interprete(NULL, Val_unit, Val_unit, 0);
+ coq_interprete(NULL, Val_unit, Atom(0), Val_unit, 0);
}
static int coq_vm_initialized = 0;
@@ -112,7 +102,6 @@ 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();
@@ -157,35 +146,11 @@ 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;
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index cec34f566..06711ad70 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,7 +33,6 @@ extern value * coq_stack_threshold;
/* global_data */
-extern value coq_global_data;
extern int coq_all_transp;
extern value coq_atom_tbl;
@@ -53,8 +51,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 */
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 012948954..dfe3d8fb1 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -26,7 +26,9 @@ open Cbytegen
module NamedDecl = Context.Named.Declaration
module RelDecl = Context.Rel.Declaration
-external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
+external eval_tcode : tcode -> vm_global -> values array -> values = "coq_eval_tcode"
+
+type global_data = { mutable glob_len : int; mutable glob_val : values array }
(*******************)
(* Linkage du code *)
@@ -37,21 +39,28 @@ external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
(* [global_data] contient les valeurs des constantes globales
(axiomes,definitions), les annotations des switch et les structured
constant *)
-external global_data : unit -> values array = "get_coq_global_data"
+let global_data = {
+ glob_len = 0;
+ glob_val = Array.make 4096 crazy_val;
+}
-(* [realloc_global_data n] augmente de n la taille de [global_data] *)
-external realloc_global_data : int -> unit = "realloc_coq_global_data"
+let get_global_data () = Vmvalues.vm_global global_data.glob_val
-let check_global_data n =
- if n >= Array.length (global_data()) then realloc_global_data n
+let realloc_global_data n =
+ let n = min (n + 0x100) Sys.max_array_length in
+ let ans = Array.make n crazy_val in
+ let src = global_data.glob_val in
+ let () = Array.blit src 0 ans 0 (Array.length src) in
+ global_data.glob_val <- ans
-let num_global = ref 0
+let check_global_data n =
+ if n >= Array.length global_data.glob_val then realloc_global_data n
let set_global v =
- let n = !num_global in
+ let n = global_data.glob_len in
check_global_data n;
- (global_data()).(n) <- v;
- incr num_global;
+ global_data.glob_val.(n) <- v;
+ global_data.glob_len <- global_data.glob_len + 1;
n
(* table pour les structured_constant et les annotations des switchs *)
@@ -164,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_env
+ eval_tcode tc (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/csymtable.mli b/kernel/csymtable.mli
index 19b2b8b50..d32cfba36 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -18,3 +18,5 @@ val val_of_constr : env -> constr -> Vmvalues.values
val set_opaque_const : Constant.t -> unit
val set_transparent_const : Constant.t -> unit
+
+val get_global_data : unit -> Vmvalues.vm_global
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 370185a72..5d270125a 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -43,6 +43,6 @@ Subtyping
Mod_typing
Nativelibrary
Safe_typing
-Vm
Csymtable
+Vm
Vconv
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 14aeb732f..160575ac7 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -42,9 +42,12 @@ external push_vstack : vstack -> int -> unit = "coq_push_vstack"
(* interpreteur *)
-external interprete : tcode -> values -> vm_env -> int -> values =
+external coq_interprete : tcode -> values -> vm_global -> vm_env -> int -> values =
"coq_interprete_ml"
+let interprete code v env k =
+ coq_interprete code v (Csymtable.get_global_data ()) env k
+
(* Functions over arguments *)
(* Apply a value to arguments contained in [vargs] *)
@@ -184,6 +187,6 @@ let apply_whd k whd =
push_val v;
interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0
| Vatom_stk(a,stk) ->
- apply_stack (val_of_atom a) stk v
+ apply_stack (val_of_atom a) stk v
| Vuniv_level lvl -> assert false
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 0e0cb4e58..6377e947f 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -43,6 +43,7 @@ let fix_val v = (Obj.magic v : values)
let cofix_upd_val v = (Obj.magic v : values)
type vm_env
+type vm_global
let fun_env v = (Obj.magic v : vm_env)
let fix_env v = (Obj.magic v : vm_env)
let cofix_env v = (Obj.magic v : vm_env)
@@ -51,6 +52,8 @@ type vstack = values array
let fun_of_val v = (Obj.magic v : vfun)
+let vm_global (v : values array) = (Obj.magic v : vm_global)
+
(*******************************************)
(* Machine code *** ************************)
(*******************************************)
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index c6e342a96..1fa889288 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -15,6 +15,7 @@ open Cbytecodes
type values
type vm_env
+type vm_global
type vprod
type vfun
type vfix
@@ -33,6 +34,8 @@ val fix_env : vfix -> vm_env
val cofix_env : vcofix -> vm_env
val cofix_upd_env : to_update -> vm_env
+val vm_global : values array -> vm_global
+
(** Cast a value known to be a function, unsafe in general *)
val fun_of_val : values -> vfun