Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 303 insertions, 0 deletions

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
new file mode 100644
index 00000000..cccb1844
--- /dev/null
+++ b/kernel/cemitcodes.ml
@@ -0,0 +1,303 @@
+open Names
+open Term
+open Cbytecodes
+open Copcodes
+open Mod_subst
+
+(* Relocation information *)
+type reloc_info =
+  | Reloc_annot of annot_switch 
+  | Reloc_const of structured_constant
+  | Reloc_getglobal of constant
+
+type patch = reloc_info * int 
+
+let patch_int buff pos n =
+  String.unsafe_set buff pos (Char.unsafe_chr n);
+  String.unsafe_set buff (pos + 1) (Char.unsafe_chr (n asr 8));
+  String.unsafe_set buff (pos + 2) (Char.unsafe_chr (n asr 16));
+  String.unsafe_set buff (pos + 3) (Char.unsafe_chr (n asr 24))
+
+
+(* Buffering of bytecode *)
+
+let out_buffer = ref(String.create 1024)
+and out_position = ref 0
+
+let out_word b1 b2 b3 b4 =
+  let p = !out_position in
+  if p >= String.length !out_buffer then begin
+    let len = String.length !out_buffer in
+    let new_buffer = String.create (2 * len) in
+    String.blit !out_buffer 0 new_buffer 0 len;
+    out_buffer := new_buffer
+  end;
+  String.unsafe_set !out_buffer p (Char.unsafe_chr b1);
+  String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2);
+  String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3);
+  String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4);
+  out_position := p + 4
+
+let out opcode =
+  out_word opcode 0 0 0
+
+let out_int n =
+  out_word n (n asr 8) (n asr 16) (n asr 24)
+
+(* Handling of local labels and backpatching *)
+
+type label_definition =
+    Label_defined of int
+  | Label_undefined of (int * int) list
+
+let label_table  = ref ([| |] : label_definition array)
+(* le ieme element de la table = Label_defined n signifie que l'on a 
+   deja rencontrer le label i et qu'il est a l'offset n.
+                               = Label_undefined l signifie que l'on a 
+   pas encore rencontrer ce label, le premier entier indique ou est l'entier 
+   a patcher dans la string, le deuxieme son origine  *)
+
+let extend_label_table needed =
+  let new_size = ref(Array.length !label_table) in
+  while needed >= !new_size do new_size := 2 * !new_size done;
+  let new_table = Array.create !new_size (Label_undefined []) in
+  Array.blit !label_table 0 new_table 0 (Array.length !label_table);
+  label_table := new_table
+
+let backpatch (pos, orig) =
+  let displ = (!out_position - orig) asr 2 in
+  !out_buffer.[pos] <- Char.unsafe_chr displ;
+  !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8);
+  !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16);
+  !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24)
+
+let define_label lbl =
+  if lbl >= Array.length !label_table then extend_label_table lbl;
+  match (!label_table).(lbl) with
+    Label_defined _ ->
+      raise(Failure "CEmitcode.define_label")
+  | Label_undefined patchlist ->
+      List.iter backpatch patchlist;
+      (!label_table).(lbl) <- Label_defined !out_position
+
+let out_label_with_orig orig lbl =
+  if lbl >= Array.length !label_table then extend_label_table lbl;
+  match (!label_table).(lbl) with
+    Label_defined def ->
+      out_int((def - orig) asr 2)
+  | Label_undefined patchlist ->
+      if patchlist = [] then
+	(!label_table).(lbl) <-
+          Label_undefined((!out_position, orig) :: patchlist);
+      out_int 0
+
+let out_label l = out_label_with_orig !out_position l
+
+(* Relocation information *)
+
+let reloc_info = ref ([] : (reloc_info * int) list)
+
+let enter info =
+  reloc_info := (info, !out_position) :: !reloc_info
+
+let slot_for_const c =
+  enter (Reloc_const c);
+  out_int 0
+
+and slot_for_annot a =
+  enter (Reloc_annot a);
+  out_int 0
+
+and slot_for_getglobal id =
+  enter (Reloc_getglobal id);
+  out_int 0
+
+
+(* Emission of one instruction *)
+
+
+let emit_instr = function
+  | Klabel lbl -> define_label lbl
+  | Kacc n ->
+      if n < 8 then out(opACC0 + n) else (out opACC; out_int n)
+  | Kenvacc n ->
+      if n >= 1 && n <= 4
+      then out(opENVACC1 + n - 1)
+      else (out opENVACC; out_int n)
+  | Koffsetclosure ofs ->
+      if ofs = -2 || ofs = 0 || ofs = 2
+      then out (opOFFSETCLOSURE0 + ofs / 2)
+      else (out opOFFSETCLOSURE; out_int ofs)
+  | Kpush ->      
+      out opPUSH
+  | Kpop n ->      
+      out opPOP; out_int n
+  | Kpush_retaddr lbl -> 
+      out opPUSH_RETADDR; out_label lbl
+  | Kapply n ->
+      if n < 4 then out(opAPPLY1 + n - 1) else (out opAPPLY; out_int n)
+  | Kappterm(n, sz) ->
+      if n < 4 then (out(opAPPTERM1 + n - 1); out_int sz)
+               else (out opAPPTERM; out_int n; out_int sz)
+  | Kreturn n ->
+      out opRETURN; out_int n
+  | Kjump ->
+      out opRETURN; out_int 0
+  | Krestart ->
+      out opRESTART
+  | Kgrab n -> 
+      out opGRAB; out_int n
+  | Kgrabrec(rec_arg) -> 
+      out opGRABREC; out_int rec_arg
+  | Kcograb n -> 
+      out opCOGRAB; out_int n
+  | Kclosure(lbl, n) -> 
+      out opCLOSURE; out_int n; out_label lbl
+  | Kclosurerec(nfv,init,lbl_types,lbl_bodies) ->
+      out opCLOSUREREC;out_int (Array.length lbl_bodies);
+      out_int nfv; out_int init;
+      let org = !out_position in
+      Array.iter (out_label_with_orig org) lbl_types;
+      let org = !out_position in
+      Array.iter (out_label_with_orig org) lbl_bodies
+  | Kgetglobal q -> 
+      out opGETGLOBAL; slot_for_getglobal q
+  | Kconst((Const_b0 i)) -> 
+      if i >= 0 && i <= 3
+          then out (opCONST0 + i)
+          else (out opCONSTINT; out_int i) 
+  | Kconst c ->
+      out opGETGLOBAL; slot_for_const c
+  | Kmakeblock(n, t) ->
+      if n = 0 then raise (Invalid_argument "emit_instr : block size = 0")
+      else if n < 4 then (out(opMAKEBLOCK1 + n - 1); out_int t)
+      else (out opMAKEBLOCK; out_int n; out_int t)
+  | Kmakeprod ->
+      out opMAKEPROD
+  | Kmakeswitchblock(typlbl,swlbl,annot,sz) ->
+      out opMAKESWITCHBLOCK;
+      out_label typlbl; out_label swlbl;
+      slot_for_annot annot;out_int sz
+  | Kforce -> 
+      out opFORCE
+  | Kswitch (tbl_const, tbl_block) ->
+      out opSWITCH;
+      out_int (Array.length tbl_const + (Array.length tbl_block lsl 16));
+      let org = !out_position in
+      Array.iter (out_label_with_orig org) tbl_const;
+      Array.iter (out_label_with_orig org) tbl_block
+  | Kpushfield n ->
+      out opPUSHFIELD;out_int n
+  | Kstop -> 
+      out opSTOP
+  | Ksequence _ -> raise (Invalid_argument "Cemitcodes.emit_instr")
+
+(* Emission of a list of instructions. Include some peephole optimization. *)
+
+let rec emit = function
+  | [] -> ()
+  (* Peephole optimizations *)
+  | Kpush :: Kacc n :: c ->
+      if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n);
+      emit c
+  | Kpush :: Kenvacc n :: c -> 
+      if n >= 1 && n <= 4
+      then out(opPUSHENVACC1 + n - 1)
+      else (out opPUSHENVACC; out_int n);
+      emit c
+  | Kpush :: Koffsetclosure ofs :: c -> 
+      if ofs = -2 || ofs = 0 || ofs = 2
+      then out(opPUSHOFFSETCLOSURE0 + ofs / 2)
+      else (out opPUSHOFFSETCLOSURE; out_int ofs);
+      emit c
+  | Kpush :: Kgetglobal id :: c ->
+      out opPUSHGETGLOBAL; slot_for_getglobal id; emit c 
+  | Kpush :: Kconst (Const_b0 i) :: c -> 
+      if i >= 0 && i <= 3
+      then out (opPUSHCONST0 + i)
+      else (out opPUSHCONSTINT; out_int i);
+      emit c
+  | Kpush :: Kconst const :: c ->
+      out opPUSHGETGLOBAL; slot_for_const const;
+      emit c 
+  | Kpop n :: Kjump :: c ->
+      out opRETURN; out_int n; emit c
+  | Ksequence(c1,c2)::c ->
+      emit c1; emit c2;emit c
+  (* Default case *)
+  | instr :: c ->
+      emit_instr instr; emit c
+
+(* Initialization *)
+
+let init () =
+  out_position := 0;
+  label_table := Array.create 16 (Label_undefined []);
+  reloc_info := []
+
+type emitcodes = string
+
+let length = String.length
+
+type to_patch = emitcodes * (patch list) * fv
+
+(* Substitution *)
+let rec subst_strcst s sc =
+  match sc with
+  | Const_sorts _ | Const_b0 _ -> sc
+  | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
+  | Const_ind(ind) -> let kn,i = ind in Const_ind((subst_kn s kn, i))
+
+let subst_patch s (ri,pos) = 
+  match ri with
+  | Reloc_annot a ->
+      let (kn,i) = a.ci.ci_ind in
+      let ci = {a.ci with ci_ind = (subst_kn s kn,i)} in
+      (Reloc_annot {a with ci = ci},pos)
+  | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
+  | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con s kn)), pos)
+
+let subst_to_patch s (code,pl,fv) = 
+  code,List.rev_map (subst_patch s) pl,fv
+
+type body_code =
+  | BCdefined of bool * to_patch
+  | BCallias of constant
+  | BCconstant
+
+let subst_body_code s = function
+  | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp)
+  | BCallias kn -> BCallias (fst (subst_con s kn))
+  | BCconstant -> BCconstant
+
+type to_patch_substituted = body_code substituted
+
+let from_val = from_val
+
+let force = force subst_body_code
+
+let subst_to_patch_subst = subst_substituted 
+
+let is_boxed tps =
+  match force tps with
+  | BCdefined(b,_) -> b
+  | _ -> false
+
+let to_memory (init_code, fun_code, fv) =
+  init();
+  emit init_code;
+  emit fun_code;
+  let code = String.create !out_position in
+  String.unsafe_blit !out_buffer 0 code 0 !out_position;
+  let reloc = List.rev !reloc_info in
+  Array.iter (fun lbl -> 
+    (match lbl with
+      Label_defined _ -> assert true
+    | Label_undefined patchlist -> 
+	assert (patchlist = []))) !label_table;
+  (code, reloc, fv)
+
+
+
+
+