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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Created by Bruno Barras for Benjamin Grégoire as part of the
bytecode-based reduction machine, Oct 2004 *)
(* Support for native arithmetics by Arnaud Spiwack, May 2007 *)
(* This file defines the type of bytecode instructions *)
open Names
open Term
type tag = int
let id_tag = 0
let iddef_tag = 1
let ind_tag = 2
let fix_tag = 3
let switch_tag = 4
let cofix_tag = 5
let cofix_evaluated_tag = 6
type structured_constant =
| Const_sorts of sorts
| Const_ind of inductive
| Const_b0 of tag
| Const_bn of tag * structured_constant array
type reloc_table = (tag * int) array
type annot_switch =
{ci : case_info; rtbl : reloc_table; tailcall : bool}
module Label =
struct
type t = int
let no = -1
let counter = ref no
let create () = incr counter; !counter
let reset_label_counter () = counter := no
end
type instruction =
| Klabel of Label.t
| Kacc of int
| Kenvacc of int
| Koffsetclosure of int
| Kpush
| Kpop of int
| Kpush_retaddr of Label.t
| Kapply of int (* number of arguments *)
| Kappterm of int * int (* number of arguments, slot size *)
| Kreturn of int (* slot size *)
| Kjump
| Krestart
| Kgrab of int (* number of arguments *)
| Kgrabrec of int (* rec arg *)
| Kclosure of Label.t * int (* label, number of free variables *)
| Kclosurerec of int * int * Label.t array * Label.t array
(* nb fv, init, lbl types, lbl bodies *)
| Kclosurecofix of int * int * Label.t array * Label.t array
(* nb fv, init, lbl types, lbl bodies *)
| Kgetglobal of constant
| Kconst of structured_constant
| Kmakeblock of int * tag (* size, tag *)
| Kmakeprod
| Kmakeswitchblock of Label.t * Label.t * annot_switch * int
| Kswitch of Label.t array * Label.t array (* consts,blocks *)
| Kpushfields of int
| Kfield of int
| Ksetfield of int
| Kstop
| Ksequence of bytecodes * bytecodes
(* spiwack: instructions concerning integers *)
| Kbranch of Label.t (* jump to label *)
| Kaddint31 (* adds the int31 in the accu
and the one ontop of the stack *)
| Kaddcint31 (* makes the sum and keeps the carry *)
| Kaddcarrycint31 (* sum +1, keeps the carry *)
| Ksubint31 (* subtraction modulo *)
| Ksubcint31 (* subtraction, keeps the carry *)
| Ksubcarrycint31 (* subtraction -1, keeps the carry *)
| Kmulint31 (* multiplication modulo *)
| Kmulcint31 (* multiplication, result in two
int31, for exact computation *)
| Kdiv21int31 (* divides a double size integer
(represented by an int31 in the
accumulator and one on the top of
the stack) by an int31. The result
is a pair of the quotient and the
rest.
If the divisor is 0, it returns
0. *)
| Kdivint31 (* euclidian division (returns a pair
quotient,rest) *)
| Kaddmuldivint31 (* generic operation for shifting and
cycling. Takes 3 int31 i j and s,
and returns x*2^s+y/(2^(31-s) *)
| Kcompareint31 (* unsigned comparison of int31
cf COMPAREINT31 in
kernel/byterun/coq_interp.c
for more info *)
| Khead0int31 (* Give the numbers of 0 in head of a in31*)
| Ktail0int31 (* Give the numbers of 0 in tail of a in31
ie low bits *)
| Kisconst of Label.t (* conditional jump *)
| Kareconst of int*Label.t (* conditional jump *)
| Kcompint31 (* dynamic compilation of int31 *)
| Kdecompint31 (* dynamic decompilation of int31 *)
(* /spiwack *)
and bytecodes = instruction list
type fv_elem = FVnamed of identifier | FVrel of int
type fv = fv_elem array
(* spiwack: this exception is expected to be raised by function expecting
closed terms. *)
exception NotClosed
(*spiwack: both type have been moved from Cbytegen because I needed then
for the retroknowledge *)
type vm_env = {
size : int; (* longueur de la liste [n] *)
fv_rev : fv_elem list (* [fvn; ... ;fv1] *)
}
type comp_env = {
nb_stack : int; (* nbre de variables sur la pile *)
in_stack : int list; (* position dans la pile *)
nb_rec : int; (* nbre de fonctions mutuellement *)
(* recursives = nbr *)
pos_rec : instruction list; (* instruction d'acces pour les variables *)
(* de point fix ou de cofix *)
offset : int;
in_env : vm_env ref
}
(* --- Pretty print *)
open Format
let rec instruction ppf = function
| Klabel lbl -> fprintf ppf "L%i:" lbl
| Kacc n -> fprintf ppf "\tacc %i" n
| Kenvacc n -> fprintf ppf "\tenvacc %i" n
| Koffsetclosure n -> fprintf ppf "\toffsetclosure %i" n
| Kpush -> fprintf ppf "\tpush"
| Kpop n -> fprintf ppf "\tpop %i" n
| Kpush_retaddr lbl -> fprintf ppf "\tpush_retaddr L%i" lbl
| Kapply n -> fprintf ppf "\tapply %i" n
| Kappterm(n, m) ->
fprintf ppf "\tappterm %i, %i" n m
| Kreturn n -> fprintf ppf "\treturn %i" n
| Kjump -> fprintf ppf "\tjump"
| Krestart -> fprintf ppf "\trestart"
| Kgrab n -> fprintf ppf "\tgrab %i" n
| Kgrabrec n -> fprintf ppf "\tgrabrec %i" n
| Kclosure(lbl, n) ->
fprintf ppf "\tclosure L%i, %i" lbl n
| Kclosurerec(fv,init,lblt,lblb) ->
fprintf ppf "\tclosurerec";
fprintf ppf "%i , %i, " fv init;
print_string "types = ";
Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
print_string " bodies = ";
Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
| Kclosurecofix (fv,init,lblt,lblb) ->
fprintf ppf "\tclosurecofix";
fprintf ppf " %i , %i, " fv init;
print_string "types = ";
Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
print_string " bodies = ";
Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
| Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
| Kconst cst ->
fprintf ppf "\tconst"
| Kmakeblock(n, m) ->
fprintf ppf "\tmakeblock %i, %i" n m
| Kmakeprod -> fprintf ppf "\tmakeprod"
| Kmakeswitchblock(lblt,lbls,_,sz) ->
fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz
| Kswitch(lblc,lblb) ->
fprintf ppf "\tswitch";
Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc;
Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
| Kpushfields n -> fprintf ppf "\tpushfields %i" n
| Ksetfield n -> fprintf ppf "\tsetfield %i" n
| Kfield n -> fprintf ppf "\tgetfield %i" n
| Kstop -> fprintf ppf "\tstop"
| Ksequence (c1,c2) ->
fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2
(* spiwack *)
| Kbranch lbl -> fprintf ppf "\tbranch %i" lbl
| Kaddint31 -> fprintf ppf "\taddint31"
| Kaddcint31 -> fprintf ppf "\taddcint31"
| Kaddcarrycint31 -> fprintf ppf "\taddcarrycint31"
| Ksubint31 -> fprintf ppf "\tsubint31"
| Ksubcint31 -> fprintf ppf "\tsubcint31"
| Ksubcarrycint31 -> fprintf ppf "\tsubcarrycint31"
| Kmulint31 -> fprintf ppf "\tmulint31"
| Kmulcint31 -> fprintf ppf "\tmulcint31"
| Kdiv21int31 -> fprintf ppf "\tdiv21int31"
| Kdivint31 -> fprintf ppf "\tdivint31"
| Kcompareint31 -> fprintf ppf "\tcompareint31"
| Khead0int31 -> fprintf ppf "\thead0int31"
| Ktail0int31 -> fprintf ppf "\ttail0int31"
| Kaddmuldivint31 -> fprintf ppf "\taddmuldivint31"
| Kisconst lbl -> fprintf ppf "\tisconst %i" lbl
| Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
| Kcompint31 -> fprintf ppf "\tcompint31"
| Kdecompint31 -> fprintf ppf "\tdecompint"
(* /spiwack *)
and instruction_list ppf = function
[] -> ()
| Klabel lbl :: il ->
fprintf ppf "L%i:%a" lbl instruction_list il
| instr :: il ->
fprintf ppf "%a@ %a" instruction instr instruction_list il
(*spiwack: moved this type in this file because I needed it for
retroknowledge which can't depend from cbytegen *)
type block =
| Bconstr of constr
| Bstrconst of structured_constant
| Bmakeblock of int * block array
| Bconstruct_app of int * int * int * block array
(* tag , nparams, arity *)
| Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
(* spiwack: compilation given by a function *)
(* compilation function (see get_vm_constant_dynamic_info in
retroknowledge.mli for more info) , argument array *)
let draw_instr c =
fprintf std_formatter "@[<v 0>%a@]" instruction_list c
|
