1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Author: Benjamin Grégoire as part of the bytecode-based virtual reduction
machine, Oct 2004 *)
(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
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 Names.constant
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 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))
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 () = List.iter (fun p -> patch buff p) patches in
buff
(* 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_len =
if len <= Sys.max_string_length / 2
then 2 * len
else
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;
out_buffer := new_buffer
end;
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
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.make !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 ->
(* spiwack: patchlist is supposed to be non-empty all the time
thus I commented that out. If there is no problem I suggest
removing it for next release (cur: 8.1) *)
(*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
let slot_for_annot a =
enter (Reloc_annot a);
out_int 0
let slot_for_getglobal p =
enter (Reloc_getglobal p);
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 Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal 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
| 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
| Kclosurecofix(nfv,init,lbl_types,lbl_bodies) ->
out opCLOSURECOFIX;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 Int.equal n 0 then invalid_arg "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
| 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_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
| Kpushfields n ->
out opPUSHFIELDS;out_int n
| Kfield n ->
if n <= 1 then out (opGETFIELD0+n)
else (out opGETFIELD;out_int n)
| Ksetfield n ->
if n <= 1 then out (opSETFIELD0+n)
else (out opSETFIELD;out_int n)
| Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
| Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p)
| Kensurestackcapacity size -> out opENSURESTACKCAPACITY; out_int size
(* spiwack *)
| Kbranch lbl -> out opBRANCH; out_label lbl
| Kaddint31 -> out opADDINT31
| Kaddcint31 -> out opADDCINT31
| Kaddcarrycint31 -> out opADDCARRYCINT31
| Ksubint31 -> out opSUBINT31
| Ksubcint31 -> out opSUBCINT31
| Ksubcarrycint31 -> out opSUBCARRYCINT31
| Kmulint31 -> out opMULINT31
| Kmulcint31 -> out opMULCINT31
| Kdiv21int31 -> out opDIV21INT31
| Kdivint31 -> out opDIVINT31
| Kaddmuldivint31 -> out opADDMULDIVINT31
| Kcompareint31 -> out opCOMPAREINT31
| Khead0int31 -> out opHEAD0INT31
| Ktail0int31 -> out opTAIL0INT31
| Kisconst lbl -> out opISCONST; out_label lbl
| Kareconst(n,lbl) -> out opARECONST; out_int n; out_label lbl
| Kcompint31 -> out opCOMPINT31
| Kdecompint31 -> out opDECOMPINT31
| Klorint31 -> out opORINT31
| Klandint31 -> out opANDINT31
| Klxorint31 -> out opXORINT31
(*/spiwack *)
| Kstop ->
out opSTOP
(* 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 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
| 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.make 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 _ | Const_univ_level _ | Const_type _ -> sc
| Const_proj p -> Const_proj (subst_constant s p)
| Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
| Const_ind ind -> let kn,i = ind in Const_ind (subst_mind 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_mind 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 (subst_constant 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 to_patch
| BCalias of Names.constant
| BCconstant
type to_patch_substituted =
| PBCdefined of to_patch substituted
| PBCalias of Names.constant substituted
| PBCconstant
let from_val = function
| BCdefined tp -> PBCdefined (from_val tp)
| BCalias cu -> PBCalias (from_val cu)
| BCconstant -> PBCconstant
let force = function
| PBCdefined tp -> BCdefined (force subst_to_patch tp)
| PBCalias cu -> BCalias (force subst_constant cu)
| PBCconstant -> BCconstant
let subst_to_patch_subst s = function
| PBCdefined tp -> PBCdefined (subst_substituted s tp)
| PBCalias cu -> PBCalias (subst_substituted s cu)
| PBCconstant -> PBCconstant
let repr_body_code = function
| PBCdefined tp ->
let (s, tp) = repr_substituted tp in
(s, BCdefined tp)
| PBCalias cu ->
let (s, cu) = repr_substituted cu in
(s, BCalias cu)
| PBCconstant -> (None, BCconstant)
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 = CString.hcons code in
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)
|