summaryrefslogtreecommitdiff
path: root/kernel/cemitcodes.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/cemitcodes.ml')
-rw-r--r--kernel/cemitcodes.ml90
1 files changed, 47 insertions, 43 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 3c9692a5..2535a64d 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -10,7 +10,6 @@
machine, Oct 2004 *)
(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
-open Names
open Term
open Cbytecodes
open Copcodes
@@ -24,34 +23,22 @@ type reloc_info =
type patch = reloc_info * int
+let patch_char4 buff pos c1 c2 c3 c4 =
+ String.unsafe_set buff pos c1;
+ String.unsafe_set buff (pos + 1) c2;
+ String.unsafe_set buff (pos + 2) c3;
+ String.unsafe_set buff (pos + 3) c4
+
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))
-
+ patch_char4 buff pos
+ (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8)) (Char.unsafe_chr (n asr 16))
+ (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_word b1 b2 b3 b4 =
let p = !out_position in
if p >= String.length !out_buffer then begin
@@ -67,13 +54,10 @@ let out_word b1 b2 b3 b4 =
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);
+ patch_char4 !out_buffer p (Char.unsafe_chr b1)
+ (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4);
out_position := p + 4
-
let out opcode =
out_word opcode 0 0 0
@@ -102,7 +86,7 @@ let extend_label_table needed =
let backpatch (pos, orig) =
let displ = (!out_position - orig) asr 2 in
- !out_buffer.[pos] <- Char.unsafe_chr displ;
+ !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)
@@ -223,8 +207,12 @@ let emit_instr = function
out_label typlbl; out_label swlbl;
slot_for_annot annot;out_int sz
| Kswitch (tbl_const, tbl_block) ->
+ let lenb = Array.length tbl_block in
+ let lenc = Array.length tbl_const in
+ assert (lenb < 0x100 && lenc < 0x1000000);
out opSWITCH;
- out_int (Array.length tbl_const + (Array.length tbl_block lsl 16));
+ out_word lenc (lenc asr 8) (lenc asr 16) (lenb);
+(* out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); *)
let org = !out_position in
Array.iter (out_label_with_orig org) tbl_const;
Array.iter (out_label_with_orig org) tbl_block
@@ -334,25 +322,41 @@ let subst_patch s (ri,pos) =
let subst_to_patch s (code,pl,fv) =
code,List.rev_map (subst_patch s) pl,fv
+let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
+
type body_code =
| BCdefined of to_patch
| BCallias of pconstant
| BCconstant
-let subst_body_code s = function
- | BCdefined tp -> BCdefined (subst_to_patch s tp)
- | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u)
- | 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 repr_body_code = repr_substituted
+type to_patch_substituted =
+| PBCdefined of to_patch substituted
+| PBCallias of pconstant substituted
+| PBCconstant
+
+let from_val = function
+| BCdefined tp -> PBCdefined (from_val tp)
+| BCallias cu -> PBCallias (from_val cu)
+| BCconstant -> PBCconstant
+
+let force = function
+| PBCdefined tp -> BCdefined (force subst_to_patch tp)
+| PBCallias cu -> BCallias (force subst_pconstant cu)
+| PBCconstant -> BCconstant
+
+let subst_to_patch_subst s = function
+| PBCdefined tp -> PBCdefined (subst_substituted s tp)
+| PBCallias cu -> PBCallias (subst_substituted s cu)
+| PBCconstant -> PBCconstant
+
+let repr_body_code = function
+| PBCdefined tp ->
+ let (s, tp) = repr_substituted tp in
+ (s, BCdefined tp)
+| PBCallias cu ->
+ let (s, cu) = repr_substituted cu in
+ (s, BCallias cu)
+| PBCconstant -> (None, BCconstant)
let to_memory (init_code, fun_code, fv) =
init();