From b5aed34bb8bbdda27646720db29a8d47c79653b9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 2 Mar 2018 15:41:50 +0100 Subject: Moving the VM global data to a ML reference. --- kernel/csymtable.ml | 31 ++++++++++++++++++++----------- 1 file changed, 20 insertions(+), 11 deletions(-) (limited to 'kernel/csymtable.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 -- cgit v1.2.3