From 581b8d52fe93d666045d4878a1b48dad916451ec Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 23 Feb 2017 04:09:33 +0100 Subject: [safe_string] kernel/cemitcodes The `emitcodes` string type was used in both a functional and an imperative way, so we have to handle it with care in order to preserve the previous optimizations and semantics. --- kernel/cemitcodes.ml | 39 +++++++++++++++++++++++++-------------- 1 file changed, 25 insertions(+), 14 deletions(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index ad7a41a347..a0a13174ff 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -24,33 +24,45 @@ 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 + Bytes.unsafe_set buff pos c1; + Bytes.unsafe_set buff (pos + 1) c2; + Bytes.unsafe_set buff (pos + 2) c3; + Bytes.unsafe_set buff (pos + 3) c4 let patch buff (pos, n) = 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)) +(* val patch_int : emitcodes -> ((\*pos*\)int * int) list -> emitcodes *) let patch_int buff patches = (* copy code *before* patching because of nested evaluations: the code we are patching might be called (and thus "concurrently" patched) and results in wrong results. Side-effects... *) - let buff = String.copy buff in + let buff = Bytes.of_string buff in let () = List.iter (fun p -> patch buff p) patches in - buff + (* Note: we follow the apporach suggested by Gabriel Scherer in + PR#136 here, and use unsafe as we own buff. + + The crux of the question that avoids defining emitcodes just as a + Byte.t is the call to hcons in to_memory below. Even if disabling + this optimization has no visible time impact, test data shows + that the optimization is indeed triggered quite often so we + choose ugliness over altering the semantics. + + Handle with care. + *) + Bytes.unsafe_to_string buff (* Buffering of bytecode *) -let out_buffer = ref(String.create 1024) +let out_buffer = ref(Bytes.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 + if p >= Bytes.length !out_buffer then begin + let len = Bytes.length !out_buffer in let new_len = if len <= Sys.max_string_length / 2 then 2 * len @@ -58,8 +70,8 @@ let out_word b1 b2 b3 b4 = if len = Sys.max_string_length then invalid_arg "String.create" (* Pas la bonne exception .... *) else Sys.max_string_length in - let new_buffer = String.create new_len in - String.blit !out_buffer 0 new_buffer 0 len; + let new_buffer = Bytes.create new_len in + Bytes.blit !out_buffer 0 new_buffer 0 len; out_buffer := new_buffer end; patch_char4 !out_buffer p (Char.unsafe_chr b1) @@ -305,7 +317,7 @@ let init () = label_table := Array.make 16 (Label_undefined []); reloc_info := [] -type emitcodes = string +type emitcodes = String.t let length = String.length @@ -369,9 +381,8 @@ 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; (** Later uses of this string are all purely functional *) + let code = Bytes.sub_string !out_buffer 0 !out_position in let code = CString.hcons code in let reloc = List.rev !reloc_info in Array.iter (fun lbl -> -- cgit v1.2.3 From d25b1431eb73a04bdfc0f1ad2922819b69bba93a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 20 Mar 2017 15:14:01 +0100 Subject: [misc] Remove warnings about String.set The `a.[i] <- x` notation is deprecated and we were getting a couple of warnings. --- kernel/cemitcodes.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index a0a13174ff..f2c3b402b3 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -106,10 +106,10 @@ 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+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) + Bytes.set !out_buffer pos @@ Char.unsafe_chr displ; + Bytes.set !out_buffer (pos+1) @@ Char.unsafe_chr (displ asr 8); + Bytes.set !out_buffer (pos+2) @@ Char.unsafe_chr (displ asr 16); + Bytes.set !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; -- cgit v1.2.3 From 76c263b5eceac313ac2cdd3a3e7e2961876d3e31 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Mon, 20 Mar 2017 12:21:12 -0400 Subject: In the Kami project, that causes a stack overflow in one of the example files (ProcThreeStInl.v, when the final "Defined" runs). I've verified that the change here fixes the stack overflow there with Coq 8.5pl2. In this version, all the recursive calls are in tail position. Instead of taking a single list of instructions, `emit' here takes a curent list and a remaining list of lists of instructions. That means the two calls elsewhere in the file now add an empty list argument. The algorithm works on the current list until it's empty, then works on the remaining lists. The most complex case is for Ksequence, where one of the pieces becomes the new current list, and the other pieces are consed onto the remaining sub-lists. --- kernel/cemitcodes.ml | 31 +++++++++++++++++-------------- 1 file changed, 17 insertions(+), 14 deletions(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index ad7a41a347..f13620e101 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -262,41 +262,44 @@ let emit_instr = function | Kstop -> out opSTOP -(* Emission of a list of instructions. Include some peephole optimization. *) +(* Emission of a current list and remaining lists of instructions. Include some peephole optimization. *) -let rec emit = function - | [] -> () +let rec emit insns remaining = match insns with + | [] -> + (match remaining with + [] -> () + | (first::rest) -> emit first rest) (* Peephole optimizations *) | Kpush :: Kacc n :: c -> if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n); - emit c + emit c remaining | Kpush :: Kenvacc n :: c -> if n >= 1 && n <= 4 then out(opPUSHENVACC1 + n - 1) else (out opPUSHENVACC; out_int n); - emit c + emit c remaining | Kpush :: Koffsetclosure ofs :: c -> if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2 then out(opPUSHOFFSETCLOSURE0 + ofs / 2) else (out opPUSHOFFSETCLOSURE; out_int ofs); - emit c + emit c remaining | Kpush :: Kgetglobal id :: c -> - out opPUSHGETGLOBAL; slot_for_getglobal id; emit c + out opPUSHGETGLOBAL; slot_for_getglobal id; emit c remaining | Kpush :: Kconst (Const_b0 i) :: c -> if i >= 0 && i <= 3 then out (opPUSHCONST0 + i) else (out opPUSHCONSTINT; out_int i); - emit c + emit c remaining | Kpush :: Kconst const :: c -> out opPUSHGETGLOBAL; slot_for_const const; - emit c + emit c remaining | Kpop n :: Kjump :: c -> - out opRETURN; out_int n; emit c + out opRETURN; out_int n; emit c remaining | Ksequence(c1,c2)::c -> - emit c1; emit c2;emit c + emit c1 (c2::c::remaining) (* Default case *) | instr :: c -> - emit_instr instr; emit c + emit_instr instr; emit c remaining (* Initialization *) @@ -367,8 +370,8 @@ let repr_body_code = function let to_memory (init_code, fun_code, fv) = init(); - emit init_code; - emit fun_code; + emit init_code []; + emit fun_code []; let code = String.create !out_position in String.unsafe_blit !out_buffer 0 code 0 !out_position; (** Later uses of this string are all purely functional *) -- cgit v1.2.3