File: analyze.ml

package info (click to toggle)
coq 8.9.0-1
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, buster, sid
  • size: 30,604 kB
  • sloc: ml: 192,230; sh: 2,585; python: 2,206; ansic: 1,878; makefile: 818; lisp: 202; xml: 24; sed: 2
file content (423 lines) | stat: -rw-r--r-- 10,673 bytes parent folder | download
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
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
(** Headers *)

let prefix_small_block =         0x80
let prefix_small_int =           0x40
let prefix_small_string =        0x20

[@@@ocaml.warning "-32"]
let code_int8 =                  0x00
let code_int16 =                 0x01
let code_int32 =                 0x02
let code_int64 =                 0x03
let code_shared8 =               0x04
let code_shared16 =              0x05
let code_shared32 =              0x06
let code_double_array32_little = 0x07
let code_block32 =               0x08
let code_string8 =               0x09
let code_string32 =              0x0A
let code_double_big =            0x0B
let code_double_little =         0x0C
let code_double_array8_big =     0x0D
let code_double_array8_little =  0x0E
let code_double_array32_big =    0x0F
let code_codepointer =           0x10
let code_infixpointer =          0x11
let code_custom =                0x12
let code_block64 =               0x13

[@@@ocaml.warning "-37"]
type code_descr =
| CODE_INT8
| CODE_INT16
| CODE_INT32
| CODE_INT64
| CODE_SHARED8
| CODE_SHARED16
| CODE_SHARED32
| CODE_DOUBLE_ARRAY32_LITTLE
| CODE_BLOCK32
| CODE_STRING8
| CODE_STRING32
| CODE_DOUBLE_BIG
| CODE_DOUBLE_LITTLE
| CODE_DOUBLE_ARRAY8_BIG
| CODE_DOUBLE_ARRAY8_LITTLE
| CODE_DOUBLE_ARRAY32_BIG
| CODE_CODEPOINTER
| CODE_INFIXPOINTER
| CODE_CUSTOM
| CODE_BLOCK64

let code_max = 0x13

let magic_number = "\132\149\166\190"

(** Memory reification *)

module LargeArray :
sig
  type 'a t
  val empty : 'a t
  val length : 'a t -> int
  val make : int -> 'a -> 'a t
  val get : 'a t -> int -> 'a
  val set : 'a t -> int -> 'a -> unit
end =
struct

  let max_length = Sys.max_array_length

  type 'a t = 'a array array * 'a array
  (** Invariants:
      - All subarrays of the left array have length [max_length].
      - The right array has length < [max_length].
  *)

  let empty = [||], [||]

  let length (vl, vr) =
    (max_length * Array.length vl) + Array.length vr

  let make n x =
    let k = n / max_length in
    let r = n mod max_length in
    let vl = Array.init k (fun _ -> Array.make max_length x) in
    let vr = Array.make r x in
    (vl, vr)

  let get (vl, vr) n =
    let k = n / max_length in
    let r = n mod max_length in
    let len = Array.length vl in
    if k < len then vl.(k).(r)
    else if k == len then vr.(r)
    else invalid_arg "index out of bounds"

  let set (vl, vr) n x =
    let k = n / max_length in
    let r = n mod max_length in
    let len = Array.length vl in
    if k < len then vl.(k).(r) <- x
    else if k == len then vr.(r) <- x
    else invalid_arg "index out of bounds"

end

type repr =
| RInt of int
| RBlock of (int * int) (* tag × len *)
| RString of string
| RPointer of int
| RCode of int

type data =
| Int of int (* value *)
| Ptr of int (* pointer *)
| Atm of int (* tag *)
| Fun of int (* address *)

type obj =
| Struct of int * data array (* tag × data *)
| String of string

module type Input =
sig
  type t
  val input_byte : t -> int
  val input_binary_int : t -> int
end

module type S =
sig
  type input
  val parse : input -> (data * obj LargeArray.t)
end

module Make(M : Input) =
struct

open M

type input = M.t

let current_offset = ref 0

let input_byte chan =
  let () = incr current_offset in
  input_byte chan

let input_binary_int chan =
  let () = current_offset := !current_offset + 4 in
  input_binary_int chan

let input_char chan = Char.chr (input_byte chan)
let input_string len chan = String.init len (fun _ -> input_char chan)

let parse_header chan =
  let () = current_offset := 0 in
  let magic = input_string 4 chan in
  let length = input_binary_int chan in
  let objects = input_binary_int chan in
  let size32 = input_binary_int chan in
  let size64 = input_binary_int chan in
  (magic, length, size32, size64, objects)

let input_int8s chan =
  let i = input_byte chan in
  if i land 0x80 = 0
    then i
    else i lor ((-1) lsl 8)

let input_int8u = input_byte

let input_int16s chan =
  let i = input_byte chan in
  let j = input_byte chan in
  let ans = (i lsl 8) lor j in
  if i land 0x80 = 0
    then ans
    else ans lor ((-1) lsl 16)

let input_int16u chan =
  let i = input_byte chan in
  let j = input_byte chan in
  (i lsl 8) lor j

let input_int32s chan =
  let i = input_byte chan in
  let j = input_byte chan in
  let k = input_byte chan in
  let l = input_byte chan in
  let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in
  if i land 0x80 = 0
    then ans
    else ans lor ((-1) lsl 31)

let input_int32u chan =
  let i = input_byte chan in
  let j = input_byte chan in
  let k = input_byte chan in
  let l = input_byte chan in
  (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l

let input_int64s chan =
  let i = input_byte chan in
  let j = input_byte chan in
  let k = input_byte chan in
  let l = input_byte chan in
  let m = input_byte chan in
  let n = input_byte chan in
  let o = input_byte chan in
  let p = input_byte chan in
  let ans =
    (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor
    (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p
  in
  if i land 0x80 = 0
    then ans
    else ans lor ((-1) lsl 63)

let input_int64u chan =
  let i = input_byte chan in
  let j = input_byte chan in
  let k = input_byte chan in
  let l = input_byte chan in
  let m = input_byte chan in
  let n = input_byte chan in
  let o = input_byte chan in
  let p = input_byte chan in
  (i lsl 56) lor (j lsl 48) lor (k lsl 40) lor (l lsl 32) lor
  (m lsl 24) lor (n lsl 16) lor (o lsl 8) lor p

let input_header32 chan =
  let i = input_byte chan in
  let j = input_byte chan in
  let k = input_byte chan in
  let l = input_byte chan in
  let tag = l in
  let len = (i lsl 14) lor (j lsl 6) lor (k lsr 2) in
  (tag, len)

let input_header64 chan =
  let i = input_byte chan in
  let j = input_byte chan in
  let k = input_byte chan in
  let l = input_byte chan in
  let m = input_byte chan in
  let n = input_byte chan in
  let o = input_byte chan in
  let p = input_byte chan in
  let tag = p in
  let len =
    (i lsl 46) lor (j lsl 38) lor (k lsl 30) lor (l lsl 22) lor
    (m lsl 14) lor (n lsl 6) lor (o lsr 2)
  in
  (tag, len)

let parse_object chan =
  let data = input_byte chan in
  if prefix_small_block <= data then
    let tag = data land 0x0F in
    let len = (data lsr 4) land 0x07 in
    RBlock (tag, len)
  else if prefix_small_int <= data then
    RInt (data land 0x3F)
  else if prefix_small_string <= data then
    let len = data land 0x1F in
    RString (input_string len chan)
  else if data > code_max then
    assert false
  else match (Obj.magic data) with
  | CODE_INT8 ->
    RInt (input_int8s chan)
  | CODE_INT16 ->
    RInt (input_int16s chan)
  | CODE_INT32 ->
    RInt (input_int32s chan)
  | CODE_INT64 ->
    RInt (input_int64s chan)
  | CODE_SHARED8 ->
    RPointer (input_int8u chan)
  | CODE_SHARED16 ->
    RPointer (input_int16u chan)
  | CODE_SHARED32 ->
    RPointer (input_int32u chan)
  | CODE_BLOCK32 ->
    RBlock (input_header32 chan)
  | CODE_BLOCK64 ->
    RBlock (input_header64 chan)
  | CODE_STRING8 ->
    let len = input_int8u chan in
    RString (input_string len chan)
  | CODE_STRING32 ->
    let len = input_int32u chan in
    RString (input_string len chan)
  | CODE_CODEPOINTER ->
    let addr = input_int32u chan in
    for _i = 0 to 15 do ignore (input_byte chan); done;
    RCode addr
  | CODE_DOUBLE_ARRAY32_LITTLE
  | CODE_DOUBLE_BIG
  | CODE_DOUBLE_LITTLE
  | CODE_DOUBLE_ARRAY8_BIG
  | CODE_DOUBLE_ARRAY8_LITTLE
  | CODE_DOUBLE_ARRAY32_BIG
  | CODE_INFIXPOINTER
  | CODE_CUSTOM ->
    Printf.eprintf "Unhandled code %04x\n%!" data; assert false

let parse chan =
  let (magic, len, _, _, size) = parse_header chan in
  let () = assert (magic = magic_number) in
  let memory = LargeArray.make size (Struct ((-1), [||])) in
  let current_object = ref 0 in
  let fill_obj = function
  | RPointer n ->
    let data = Ptr (!current_object - n) in
    data, None
  | RInt n ->
    let data = Int n in
    data, None
  | RString s ->
    let data = Ptr !current_object in
    let () = LargeArray.set memory !current_object (String s) in
    let () = incr current_object in
    data, None
  | RBlock (tag, 0) ->
    (* Atoms are never shared *)
    let data = Atm tag in
    data, None
  | RBlock (tag, len) ->
    let data = Ptr !current_object in
    let nblock = Array.make len (Atm (-1)) in
    let () = LargeArray.set memory !current_object (Struct (tag, nblock)) in
    let () = incr current_object in
    data, Some nblock
  | RCode addr ->
    let data = Fun addr in
    data, None
  in

  let rec fill block off accu =
    if Array.length block = off then
      match accu with
      | [] -> ()
      | (block, off) :: accu -> fill block off accu
    else
      let data, nobj = fill_obj (parse_object chan) in
      let () = block.(off) <- data in
      let block, off, accu = match nobj with
      | None -> block, succ off, accu
      | Some nblock -> nblock, 0, ((block, succ off) :: accu)
      in
      fill block off accu
  in
  let ans = [|Atm (-1)|] in
  let () = fill ans 0 [] in
  (ans.(0), memory)

end

module IChannel =
struct
  type t = in_channel
  let input_byte = Pervasives.input_byte
  let input_binary_int = Pervasives.input_binary_int
end

module IString =
struct
  type t = (string * int ref)

  let input_byte (s, off) =
    let ans = Char.code (s.[!off]) in
    let () = incr off in
    ans

  let input_binary_int chan =
    let i = input_byte chan in
    let j = input_byte chan in
    let k = input_byte chan in
    let l = input_byte chan in
    let ans = (i lsl 24) lor (j lsl 16) lor (k lsl 8) lor l in
    if i land 0x80 = 0
      then ans
      else ans lor ((-1) lsl 31)

end

module PChannel = Make(IChannel)
module PString = Make(IString)

let parse_channel = PChannel.parse
let parse_string s = PString.parse (s, ref 0)

let instantiate (p, mem) =
  let len = LargeArray.length mem in
  let ans = LargeArray.make len (Obj.repr 0) in
  (** First pass: initialize the subobjects *)
  for i = 0 to len - 1 do
    let obj = match LargeArray.get mem i with
    | Struct (tag, blk) -> Obj.new_block tag (Array.length blk)
    | String str -> Obj.repr str
    in
    LargeArray.set ans i obj
  done;
  let get_data = function
  | Int n -> Obj.repr n
  | Ptr p -> LargeArray.get ans p
  | Atm tag -> Obj.new_block tag 0
  | Fun _ -> assert false (** We shouldn't serialize closures *)
  in
  (** Second pass: set the pointers *)
  for i = 0 to len - 1 do
    match LargeArray.get mem i with
    | Struct (_, blk) ->
      let obj = LargeArray.get ans i in
      for k = 0 to Array.length blk - 1 do
        Obj.set_field obj k (get_data blk.(k))
      done
    | String _ -> ()
  done;
  get_data p