aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/cbytecodes.ml
blob: 5ed9b6c675b5b1bbc3345638f34d063b53bfd1e3 (plain)
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
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* 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 Constr

type tag = int

let accu_tag = 0

let type_atom_tag = 2
let max_atom_tag = 2
let proj_tag = 3
let fix_app_tag = 4
let switch_tag = 5
let cofix_tag = 6
let cofix_evaluated_tag = 7

(* It would be great if OCaml exported this value,
   So fixme if this happens in a new version of OCaml *)
let last_variant_tag = 245 

type structured_constant =
  | Const_sort of Sorts.t
  | Const_ind of inductive
  | Const_proj of Constant.t
  | Const_b0 of tag
  | Const_bn of tag * structured_constant array
  | Const_univ_level of Univ.Level.t

type reloc_table = (tag * int) array

type annot_switch =
   {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}

let rec eq_structured_constant c1 c2 = match c1, c2 with
| Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2
| Const_sort _, _ -> false
| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
| Const_ind _, _ -> false
| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
| Const_proj _, _ -> false
| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
| Const_b0 _, _ -> false
| Const_bn (t1, a1), Const_bn (t2, a2) ->
  Int.equal t1 t2 && CArray.equal eq_structured_constant a1 a2
| Const_bn _, _ -> false
| Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2
| Const_univ_level _ , _ -> false

let rec hash_structured_constant c =
  let open Hashset.Combine in
  match c with
  | Const_sort s -> combinesmall 1 (Sorts.hash s)
  | Const_ind i -> combinesmall 2 (ind_hash i)
  | Const_proj p -> combinesmall 3 (Constant.hash p)
  | Const_b0 t -> combinesmall 4 (Int.hash t)
  | Const_bn (t, a) ->
    let fold h c = combine h (hash_structured_constant c) in
    let h = Array.fold_left fold 0 a in
    combinesmall 5 (combine (Int.hash t) h)
  | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)

let eq_annot_switch asw1 asw2 =
  let eq_ci ci1 ci2 =
    eq_ind ci1.ci_ind ci2.ci_ind &&
    Int.equal ci1.ci_npar ci2.ci_npar &&
    CArray.equal Int.equal ci1.ci_cstr_ndecls ci2.ci_cstr_ndecls
  in
  let eq_rlc (i1, j1) (i2, j2) = Int.equal i1 i2 && Int.equal j1 j2 in
  eq_ci asw1.ci asw2.ci &&
  CArray.equal eq_rlc asw1.rtbl asw2.rtbl &&
  (asw1.tailcall : bool) == asw2.tailcall

let hash_annot_switch asw =
  let open Hashset.Combine in
  let h1 = Constr.case_info_hash asw.ci in
  let h2 = Array.fold_left (fun h (t, i) -> combine3 h t i) 0 asw.rtbl in
  let h3 = if asw.tailcall then 1 else 0 in
  combine3 h1 h2 h3

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
  | Kappterm of int * int
  | Kreturn of int
  | Kjump
  | Krestart
  | Kgrab of int
  | Kgrabrec of int
  | Kclosure of Label.t * int
  | Kclosurerec of int * int * Label.t array * Label.t array
  | Kclosurecofix of int * int * Label.t array * Label.t array
                   (* nb fv, init, lbl types, lbl bodies *)
  | Kgetglobal of Constant.t
  | Kconst of structured_constant
  | Kmakeblock of int * tag
  | Kmakeprod
  | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
  | Kswitch of Label.t array * Label.t array
  | Kpushfields of int
  | Kfield of int
  | Ksetfield of int
  | Kstop
  | Ksequence of bytecodes * bytecodes
  | Kproj of int * Constant.t  (* index of the projected argument,
                                           name of projection *)
  | Kensurestackcapacity of int
(* 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 *)
  | Klorint31                            (* bitwise operations: or and xor *)
  | Klandint31
  | Klxorint31
(* /spiwack *)

and bytecodes = instruction list

type fv_elem =
  | FVnamed of Id.t
  | FVrel of int
  | FVuniv_var of int
  | FVevar of Evar.t

type fv = fv_elem array

(* spiwack: this exception is expected to be raised by function expecting
            closed terms. *)
exception NotClosed


module Fv_elem =
struct
type t = fv_elem

let compare e1 e2 = match e1, e2 with
| FVnamed id1, FVnamed id2 -> Id.compare id1 id2
| FVnamed _, (FVrel _ | FVuniv_var _ | FVevar _) -> -1
| FVrel _, FVnamed _ -> 1
| FVrel r1, FVrel r2 -> Int.compare r1 r2
| FVrel _, (FVuniv_var _ | FVevar _) -> -1
| FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2
| FVuniv_var i1, (FVnamed _ | FVrel _) -> 1
| FVuniv_var i1, FVevar _ -> -1
| FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1
| FVevar e1, FVevar e2 -> Evar.compare e1 e2

end

module FvMap = Map.Make(Fv_elem)

(*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] *)
    fv_fwd : int FvMap.t;    (* reverse mapping *)
  }


type comp_env = {
    nb_uni_stack : int ;         (* number of universes on the stack,      *)
                                 (* universes are always at the bottom.    *)
    nb_stack : int;              (* number of variables on the stack       *)
    in_stack : int list;         (* position in the stack                  *)
    nb_rec : int;                (* number of mutually recursive functions *)
    pos_rec  : instruction list; (* instruction d'acces pour les variables *)
                                 (*  de point fix ou de cofix              *)
    offset : int;
    in_env : vm_env ref          (* The free variables of the expression   *)
  }

(* --- Pretty print *)
open Pp
open Util

let pp_sort s =
  let open Sorts in
  match s with
  | Prop Null -> str "Prop"
  | Prop Pos -> str "Set"
  | Type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}"

let rec pp_struct_const = function
  | Const_sort s -> pp_sort s
  | Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i
  | Const_proj p -> Constant.print p
  | Const_b0 i -> int i
  | Const_bn (i,t) ->
     int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
  | Const_univ_level l -> Univ.Level.pr l

let pp_lbl lbl = str "L" ++ int lbl

let pp_fv_elem = function
  | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")"
  | FVrel i -> str "Rel(" ++ int i ++ str ")"
  | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")"
  | FVevar e -> str "FVevar(" ++ int (Evar.repr e) ++ str ")"

let rec pp_instr i =
  match i with
  | Klabel _   | Ksequence _ -> assert false
  | Kacc n -> str "acc " ++ int n
  | Kenvacc n -> str "envacc " ++ int n
  | Koffsetclosure n -> str "offsetclosure " ++ int n
  | Kpush -> str "push"
  | Kpop n -> str "pop " ++ int n
  | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl
  | Kapply n -> str "apply " ++ int n
  | Kappterm(n, m) ->
      str "appterm " ++ int n ++ str ", " ++ int m
  | Kreturn n -> str "return " ++ int n
  | Kjump -> str "jump"
  | Krestart -> str "restart"
  | Kgrab n -> str "grab " ++ int n
  | Kgrabrec n -> str "grabrec " ++ int n
  | Kclosure(lbl, n) ->
      str "closure " ++ pp_lbl lbl ++ str ", " ++ int n
  | Kclosurerec(fv,init,lblt,lblb) ->
      h 1 (str "closurerec " ++
	     int fv ++ str ", " ++ int init ++
	     str " types = " ++
	     prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
	     str " bodies = " ++
	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
  | Kclosurecofix (fv,init,lblt,lblb) ->
      h 1 (str "closurecofix " ++
	     int fv ++ str ", " ++ int init ++
	     str " types = " ++
	     prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
	     str " bodies = " ++
	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
  | Kgetglobal idu -> str "getglobal " ++ Constant.print idu
  | Kconst sc ->
      str "const " ++ pp_struct_const sc
  | Kmakeblock(n, m) ->
      str "makeblock " ++ int n ++ str ", " ++ int m
  | Kmakeprod -> str "makeprod"
  | Kmakeswitchblock(lblt,lbls,_,sz) ->
      str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++
	pp_lbl lbls ++ str ", " ++ int sz
  | Kswitch(lblc,lblb) ->
      h 1 (str "switch " ++
	     prlist_with_sep spc pp_lbl (Array.to_list lblc) ++
	     str " | " ++
	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
  | Kpushfields n -> str "pushfields " ++ int n
  | Kfield n -> str "field " ++ int n
  | Ksetfield n -> str "set field" ++ int n

  | Kstop -> str "stop"

  | Kbranch lbl -> str "branch " ++ pp_lbl lbl

  | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p

  | Kensurestackcapacity size -> str "growstack " ++ int size

  | Kaddint31 -> str "addint31"
  | Kaddcint31 -> str "addcint31"
  | Kaddcarrycint31 -> str "addcarrycint31"
  | Ksubint31 -> str "subint31"
  | Ksubcint31 -> str "subcint31"
  | Ksubcarrycint31 -> str "subcarrycint31"
  | Kmulint31 -> str "mulint31"
  | Kmulcint31 -> str "mulcint31"
  | Kdiv21int31 -> str "div21int31"
  | Kdivint31 -> str "divint31"
  | Kcompareint31 -> str "compareint31"
  | Khead0int31 -> str "head0int31"
  | Ktail0int31 -> str "tail0int31"
  | Kaddmuldivint31 -> str "addmuldivint31"
  | Kisconst lbl -> str "isconst " ++ int lbl
  | Kareconst(n,lbl) -> str "areconst " ++ int n ++ spc () ++ int lbl
  | Kcompint31 -> str "compint31"
  | Kdecompint31 -> str "decompint"
  | Klorint31 -> str "lorint31"
  | Klandint31 -> str "landint31"
  | Klxorint31 -> str "lxorint31"


and pp_bytecodes c =
  match c with
  | [] -> str ""
  | Klabel lbl :: c ->
	str "L" ++ int lbl ++ str ":" ++ fnl () ++
	pp_bytecodes c
  | Ksequence (l1, l2) :: c ->
      pp_bytecodes l1 ++ pp_bytecodes l2 ++  pp_bytecodes c
  | i :: c ->
      pp_instr i ++ fnl () ++ pp_bytecodes c