source: extracted/byteValues.ml @ 2649

Last change on this file since 2649 was 2649, checked in by sacerdot, 7 years ago

...

File size: 31.6 KB
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open ErrorMessages
10
11open PreIdentifiers
12
13open Errors
14
15open Extralib
16
17open Setoids
18
19open Monad
20
21open Option
22
23open Lists
24
25open Identifiers
26
27open Integers
28
29open AST
30
31open Division
32
33open Arithmetic
34
35open Extranat
36
37open Vector
38
39open Div_and_mod
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Util
48
49open FoldStuff
50
51open BitVector
52
53open Types
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Positive
70
71open Z
72
73open BitVectorZ
74
75open Pointers
76
77open Hide
78
79type cpointer = Pointers.pointer Types.sig0
80
81type xpointer = Pointers.pointer Types.sig0
82
83type program_counter = { pc_block : Pointers.block Types.sig0;
84                         pc_offset : Positive.pos }
85
86(** val program_counter_rect_Type4 :
87    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
88    'a1 **)
89let rec program_counter_rect_Type4 h_mk_program_counter x_4510 =
90  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4510 in
91  h_mk_program_counter pc_block0 pc_offset0
92
93(** val program_counter_rect_Type5 :
94    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
95    'a1 **)
96let rec program_counter_rect_Type5 h_mk_program_counter x_4512 =
97  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4512 in
98  h_mk_program_counter pc_block0 pc_offset0
99
100(** val program_counter_rect_Type3 :
101    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
102    'a1 **)
103let rec program_counter_rect_Type3 h_mk_program_counter x_4514 =
104  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4514 in
105  h_mk_program_counter pc_block0 pc_offset0
106
107(** val program_counter_rect_Type2 :
108    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
109    'a1 **)
110let rec program_counter_rect_Type2 h_mk_program_counter x_4516 =
111  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4516 in
112  h_mk_program_counter pc_block0 pc_offset0
113
114(** val program_counter_rect_Type1 :
115    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
116    'a1 **)
117let rec program_counter_rect_Type1 h_mk_program_counter x_4518 =
118  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4518 in
119  h_mk_program_counter pc_block0 pc_offset0
120
121(** val program_counter_rect_Type0 :
122    (Pointers.block Types.sig0 -> Positive.pos -> 'a1) -> program_counter ->
123    'a1 **)
124let rec program_counter_rect_Type0 h_mk_program_counter x_4520 =
125  let { pc_block = pc_block0; pc_offset = pc_offset0 } = x_4520 in
126  h_mk_program_counter pc_block0 pc_offset0
127
128(** val pc_block : program_counter -> Pointers.block Types.sig0 **)
129let rec pc_block xxx =
130  xxx.pc_block
131
132(** val pc_offset : program_counter -> Positive.pos **)
133let rec pc_offset xxx =
134  xxx.pc_offset
135
136(** val program_counter_inv_rect_Type4 :
137    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
138    'a1) -> 'a1 **)
139let program_counter_inv_rect_Type4 hterm h1 =
140  let hcut = program_counter_rect_Type4 h1 hterm in hcut __
141
142(** val program_counter_inv_rect_Type3 :
143    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
144    'a1) -> 'a1 **)
145let program_counter_inv_rect_Type3 hterm h1 =
146  let hcut = program_counter_rect_Type3 h1 hterm in hcut __
147
148(** val program_counter_inv_rect_Type2 :
149    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
150    'a1) -> 'a1 **)
151let program_counter_inv_rect_Type2 hterm h1 =
152  let hcut = program_counter_rect_Type2 h1 hterm in hcut __
153
154(** val program_counter_inv_rect_Type1 :
155    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
156    'a1) -> 'a1 **)
157let program_counter_inv_rect_Type1 hterm h1 =
158  let hcut = program_counter_rect_Type1 h1 hterm in hcut __
159
160(** val program_counter_inv_rect_Type0 :
161    program_counter -> (Pointers.block Types.sig0 -> Positive.pos -> __ ->
162    'a1) -> 'a1 **)
163let program_counter_inv_rect_Type0 hterm h1 =
164  let hcut = program_counter_rect_Type0 h1 hterm in hcut __
165
166(** val program_counter_discr : program_counter -> program_counter -> __ **)
167let program_counter_discr x y =
168  Logic.eq_rect_Type2 x
169    (let { pc_block = a0; pc_offset = a1 } = x in
170    Obj.magic (fun _ dH -> dH __ __)) y
171
172(** val program_counter_jmdiscr :
173    program_counter -> program_counter -> __ **)
174let program_counter_jmdiscr x y =
175  Logic.eq_rect_Type2 x
176    (let { pc_block = a0; pc_offset = a1 } = x in
177    Obj.magic (fun _ dH -> dH __ __)) y
178
179(** val eq_program_counter :
180    program_counter -> program_counter -> Bool.bool **)
181let eq_program_counter pc1 pc2 =
182  Bool.andb
183    (Pointers.eq_block (Types.pi1 pc1.pc_block) (Types.pi1 pc2.pc_block))
184    (Positive.eqb0 pc1.pc_offset pc2.pc_offset)
185
186(** val bitvector_from_pos :
187    Nat.nat -> Positive.pos -> BitVector.bitVector **)
188let bitvector_from_pos n p =
189  BitVectorZ.bitvector_of_Z n (Z.zpred (Z.Pos p))
190
191(** val pos_from_bitvector :
192    Nat.nat -> BitVector.bitVector -> Positive.pos **)
193let pos_from_bitvector n v =
194  (match Z.zsucc (BitVectorZ.z_of_unsigned_bitvector n v) with
195   | Z.OZ -> (fun _ -> assert false (* absurd case *))
196   | Z.Pos x -> (fun _ -> x)
197   | Z.Neg x -> (fun _ -> assert false (* absurd case *))) __
198
199(** val cpointer_of_pc : program_counter -> cpointer Types.option **)
200let cpointer_of_pc pc =
201  let pc_off = pc.pc_offset in
202  (match Positive.leb0 pc_off (Positive.two_power_nat Pointers.offset_size) with
203   | Bool.True ->
204     Obj.magic
205       (Monad.m_return0 (Monad.max_def Option.option0) { Pointers.pblock =
206         (Types.pi1 pc.pc_block); Pointers.poff =
207         (bitvector_from_pos Pointers.offset_size pc_off) })
208   | Bool.False -> Types.None)
209
210type part =
211  Nat.nat
212  (* singleton inductive, whose constructor was mk_part *)
213
214(** val part_rect_Type4 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
215let rec part_rect_Type4 h_mk_part x_4536 =
216  let part_no = x_4536 in h_mk_part part_no __
217
218(** val part_rect_Type5 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
219let rec part_rect_Type5 h_mk_part x_4538 =
220  let part_no = x_4538 in h_mk_part part_no __
221
222(** val part_rect_Type3 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
223let rec part_rect_Type3 h_mk_part x_4540 =
224  let part_no = x_4540 in h_mk_part part_no __
225
226(** val part_rect_Type2 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
227let rec part_rect_Type2 h_mk_part x_4542 =
228  let part_no = x_4542 in h_mk_part part_no __
229
230(** val part_rect_Type1 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
231let rec part_rect_Type1 h_mk_part x_4544 =
232  let part_no = x_4544 in h_mk_part part_no __
233
234(** val part_rect_Type0 : (Nat.nat -> __ -> 'a1) -> part -> 'a1 **)
235let rec part_rect_Type0 h_mk_part x_4546 =
236  let part_no = x_4546 in h_mk_part part_no __
237
238(** val part_no : part -> Nat.nat **)
239let rec part_no xxx =
240  let yyy = xxx in yyy
241
242(** val part_inv_rect_Type4 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
243let part_inv_rect_Type4 hterm h1 =
244  let hcut = part_rect_Type4 h1 hterm in hcut __
245
246(** val part_inv_rect_Type3 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
247let part_inv_rect_Type3 hterm h1 =
248  let hcut = part_rect_Type3 h1 hterm in hcut __
249
250(** val part_inv_rect_Type2 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
251let part_inv_rect_Type2 hterm h1 =
252  let hcut = part_rect_Type2 h1 hterm in hcut __
253
254(** val part_inv_rect_Type1 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
255let part_inv_rect_Type1 hterm h1 =
256  let hcut = part_rect_Type1 h1 hterm in hcut __
257
258(** val part_inv_rect_Type0 : part -> (Nat.nat -> __ -> __ -> 'a1) -> 'a1 **)
259let part_inv_rect_Type0 hterm h1 =
260  let hcut = part_rect_Type0 h1 hterm in hcut __
261
262(** val part_discr : part -> part -> __ **)
263let part_discr x y =
264  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
265
266(** val part_jmdiscr : part -> part -> __ **)
267let part_jmdiscr x y =
268  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __ __)) y
269
270(** val dpi1__o__part_no__o__inject :
271    (part, 'a1) Types.dPair -> Nat.nat Types.sig0 **)
272let dpi1__o__part_no__o__inject x2 =
273  part_no x2.Types.dpi1
274
275(** val dpi1__o__part_no__o__Z_of_nat : (part, 'a1) Types.dPair -> Z.z **)
276let dpi1__o__part_no__o__Z_of_nat x1 =
277  Z.z_of_nat (part_no x1.Types.dpi1)
278
279(** val eject__o__part_no__o__inject :
280    part Types.sig0 -> Nat.nat Types.sig0 **)
281let eject__o__part_no__o__inject x2 =
282  part_no (Types.pi1 x2)
283
284(** val eject__o__part_no__o__Z_of_nat : part Types.sig0 -> Z.z **)
285let eject__o__part_no__o__Z_of_nat x1 =
286  Z.z_of_nat (part_no (Types.pi1 x1))
287
288(** val part_no__o__Z_of_nat : part -> Z.z **)
289let part_no__o__Z_of_nat x0 =
290  Z.z_of_nat (part_no x0)
291
292(** val part_no__o__inject : part -> Nat.nat Types.sig0 **)
293let part_no__o__inject x1 =
294  part_no x1
295
296(** val dpi1__o__part_no : (part, 'a1) Types.dPair -> Nat.nat **)
297let dpi1__o__part_no x1 =
298  part_no x1.Types.dpi1
299
300(** val eject__o__part_no : part Types.sig0 -> Nat.nat **)
301let eject__o__part_no x1 =
302  part_no (Types.pi1 x1)
303
304(** val part_from_sig : Nat.nat Types.sig0 -> part **)
305let part_from_sig n_sig =
306  Types.pi1 n_sig
307
308type beval =
309| BVundef
310| BVnonzero
311| BVXor of Pointers.pointer Types.option * Pointers.pointer Types.option
312   * part
313| BVByte of BitVector.byte
314| BVnull of part
315| BVptr of Pointers.pointer * part
316| BVpc of program_counter * part
317
318(** val beval_rect_Type4 :
319    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
320    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
321    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
322    -> beval -> 'a1 **)
323let rec beval_rect_Type4 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
324| BVundef -> h_BVundef
325| BVnonzero -> h_BVnonzero
326| BVXor (x_4580, x_4579, x_4578) -> h_BVXor x_4580 x_4579 x_4578
327| BVByte x_4581 -> h_BVByte x_4581
328| BVnull x_4582 -> h_BVnull x_4582
329| BVptr (x_4584, x_4583) -> h_BVptr x_4584 x_4583
330| BVpc (x_4586, x_4585) -> h_BVpc x_4586 x_4585
331
332(** val beval_rect_Type5 :
333    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
334    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
335    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
336    -> beval -> 'a1 **)
337let rec beval_rect_Type5 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
338| BVundef -> h_BVundef
339| BVnonzero -> h_BVnonzero
340| BVXor (x_4597, x_4596, x_4595) -> h_BVXor x_4597 x_4596 x_4595
341| BVByte x_4598 -> h_BVByte x_4598
342| BVnull x_4599 -> h_BVnull x_4599
343| BVptr (x_4601, x_4600) -> h_BVptr x_4601 x_4600
344| BVpc (x_4603, x_4602) -> h_BVpc x_4603 x_4602
345
346(** val beval_rect_Type3 :
347    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
348    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
349    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
350    -> beval -> 'a1 **)
351let rec beval_rect_Type3 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
352| BVundef -> h_BVundef
353| BVnonzero -> h_BVnonzero
354| BVXor (x_4614, x_4613, x_4612) -> h_BVXor x_4614 x_4613 x_4612
355| BVByte x_4615 -> h_BVByte x_4615
356| BVnull x_4616 -> h_BVnull x_4616
357| BVptr (x_4618, x_4617) -> h_BVptr x_4618 x_4617
358| BVpc (x_4620, x_4619) -> h_BVpc x_4620 x_4619
359
360(** val beval_rect_Type2 :
361    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
362    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
363    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
364    -> beval -> 'a1 **)
365let rec beval_rect_Type2 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
366| BVundef -> h_BVundef
367| BVnonzero -> h_BVnonzero
368| BVXor (x_4631, x_4630, x_4629) -> h_BVXor x_4631 x_4630 x_4629
369| BVByte x_4632 -> h_BVByte x_4632
370| BVnull x_4633 -> h_BVnull x_4633
371| BVptr (x_4635, x_4634) -> h_BVptr x_4635 x_4634
372| BVpc (x_4637, x_4636) -> h_BVpc x_4637 x_4636
373
374(** val beval_rect_Type1 :
375    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
376    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
377    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
378    -> beval -> 'a1 **)
379let rec beval_rect_Type1 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
380| BVundef -> h_BVundef
381| BVnonzero -> h_BVnonzero
382| BVXor (x_4648, x_4647, x_4646) -> h_BVXor x_4648 x_4647 x_4646
383| BVByte x_4649 -> h_BVByte x_4649
384| BVnull x_4650 -> h_BVnull x_4650
385| BVptr (x_4652, x_4651) -> h_BVptr x_4652 x_4651
386| BVpc (x_4654, x_4653) -> h_BVpc x_4654 x_4653
387
388(** val beval_rect_Type0 :
389    'a1 -> 'a1 -> (Pointers.pointer Types.option -> Pointers.pointer
390    Types.option -> part -> 'a1) -> (BitVector.byte -> 'a1) -> (part -> 'a1)
391    -> (Pointers.pointer -> part -> 'a1) -> (program_counter -> part -> 'a1)
392    -> beval -> 'a1 **)
393let rec beval_rect_Type0 h_BVundef h_BVnonzero h_BVXor h_BVByte h_BVnull h_BVptr h_BVpc = function
394| BVundef -> h_BVundef
395| BVnonzero -> h_BVnonzero
396| BVXor (x_4665, x_4664, x_4663) -> h_BVXor x_4665 x_4664 x_4663
397| BVByte x_4666 -> h_BVByte x_4666
398| BVnull x_4667 -> h_BVnull x_4667
399| BVptr (x_4669, x_4668) -> h_BVptr x_4669 x_4668
400| BVpc (x_4671, x_4670) -> h_BVpc x_4671 x_4670
401
402(** val beval_inv_rect_Type4 :
403    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
404    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
405    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
406    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
407let beval_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 =
408  let hcut = beval_rect_Type4 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
409
410(** val beval_inv_rect_Type3 :
411    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
412    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
413    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
414    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
415let beval_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 =
416  let hcut = beval_rect_Type3 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
417
418(** val beval_inv_rect_Type2 :
419    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
420    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
421    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
422    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
423let beval_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 =
424  let hcut = beval_rect_Type2 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
425
426(** val beval_inv_rect_Type1 :
427    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
428    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
429    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
430    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
431let beval_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 =
432  let hcut = beval_rect_Type1 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
433
434(** val beval_inv_rect_Type0 :
435    beval -> (__ -> 'a1) -> (__ -> 'a1) -> (Pointers.pointer Types.option ->
436    Pointers.pointer Types.option -> part -> __ -> 'a1) -> (BitVector.byte ->
437    __ -> 'a1) -> (part -> __ -> 'a1) -> (Pointers.pointer -> part -> __ ->
438    'a1) -> (program_counter -> part -> __ -> 'a1) -> 'a1 **)
439let beval_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 =
440  let hcut = beval_rect_Type0 h1 h2 h3 h4 h5 h6 h7 hterm in hcut __
441
442(** val beval_discr : beval -> beval -> __ **)
443let beval_discr x y =
444  Logic.eq_rect_Type2 x
445    (match x with
446     | BVundef -> Obj.magic (fun _ dH -> dH)
447     | BVnonzero -> Obj.magic (fun _ dH -> dH)
448     | BVXor (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
449     | BVByte a0 -> Obj.magic (fun _ dH -> dH __)
450     | BVnull a0 -> Obj.magic (fun _ dH -> dH __)
451     | BVptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
452     | BVpc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
453
454(** val beval_jmdiscr : beval -> beval -> __ **)
455let beval_jmdiscr x y =
456  Logic.eq_rect_Type2 x
457    (match x with
458     | BVundef -> Obj.magic (fun _ dH -> dH)
459     | BVnonzero -> Obj.magic (fun _ dH -> dH)
460     | BVXor (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
461     | BVByte a0 -> Obj.magic (fun _ dH -> dH __)
462     | BVnull a0 -> Obj.magic (fun _ dH -> dH __)
463     | BVptr (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
464     | BVpc (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)) y
465
466(** val eq_bv_suffix :
467    Nat.nat -> Nat.nat -> Nat.nat -> BitVector.bitVector ->
468    BitVector.bitVector -> Bool.bool **)
469let eq_bv_suffix n m p v1 v2 =
470  let b1 = (Vector.vsplit n p v1).Types.snd in
471  let b2 = (Vector.vsplit m p v2).Types.snd in BitVector.eq_bv p b1 b2
472
473(** val pointer_of_bevals :
474    beval List.list -> Pointers.pointer Errors.res **)
475let pointer_of_bevals = function
476| List.Nil ->
477  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
478    List.Nil))
479| List.Cons (bv1, tl) ->
480  (match tl with
481   | List.Nil ->
482     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
483       List.Nil))
484   | List.Cons (bv2, tl') ->
485     (match tl' with
486      | List.Nil ->
487        (match bv1 with
488         | BVundef ->
489           Errors.Error (List.Cons ((Errors.MSG
490             ErrorMessages.CorruptedPointer), List.Nil))
491         | BVnonzero ->
492           Errors.Error (List.Cons ((Errors.MSG
493             ErrorMessages.CorruptedPointer), List.Nil))
494         | BVXor (x, x0, x1) ->
495           Errors.Error (List.Cons ((Errors.MSG
496             ErrorMessages.CorruptedPointer), List.Nil))
497         | BVByte x ->
498           Errors.Error (List.Cons ((Errors.MSG
499             ErrorMessages.CorruptedPointer), List.Nil))
500         | BVnull x ->
501           Errors.Error (List.Cons ((Errors.MSG
502             ErrorMessages.CorruptedPointer), List.Nil))
503         | BVptr (ptr1, p3) ->
504           (match bv2 with
505            | BVundef ->
506              Errors.Error (List.Cons ((Errors.MSG
507                ErrorMessages.CorruptedPointer), List.Nil))
508            | BVnonzero ->
509              Errors.Error (List.Cons ((Errors.MSG
510                ErrorMessages.CorruptedPointer), List.Nil))
511            | BVXor (x, x0, x1) ->
512              Errors.Error (List.Cons ((Errors.MSG
513                ErrorMessages.CorruptedPointer), List.Nil))
514            | BVByte x ->
515              Errors.Error (List.Cons ((Errors.MSG
516                ErrorMessages.CorruptedPointer), List.Nil))
517            | BVnull x ->
518              Errors.Error (List.Cons ((Errors.MSG
519                ErrorMessages.CorruptedPointer), List.Nil))
520            | BVptr (ptr2, p4) ->
521              (match Bool.andb
522                       (Bool.andb
523                         (Bool.andb (Nat.eqb (part_no p3) Nat.O)
524                           (Nat.eqb (part_no p4) (Nat.S Nat.O)))
525                         (Pointers.eq_block ptr1.Pointers.pblock
526                           ptr2.Pointers.pblock))
527                       (eq_bv_suffix (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
528                         (Nat.S (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S
529                         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
530                         Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
531                         (Nat.S (Nat.S (Nat.S Nat.O))))))))
532                         (Pointers.offv ptr1.Pointers.poff)
533                         (Pointers.offv ptr2.Pointers.poff)) with
534               | Bool.True ->
535                 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
536               | Bool.False ->
537                 Errors.Error (List.Cons ((Errors.MSG
538                   ErrorMessages.CorruptedPointer), List.Nil)))
539            | BVpc (x, x0) ->
540              Errors.Error (List.Cons ((Errors.MSG
541                ErrorMessages.CorruptedPointer), List.Nil)))
542         | BVpc (x, x0) ->
543           Errors.Error (List.Cons ((Errors.MSG
544             ErrorMessages.CorruptedPointer), List.Nil)))
545      | List.Cons (x, x0) ->
546        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
547          List.Nil))))
548
549(** val pc_of_bevals : beval List.list -> program_counter Errors.res **)
550let pc_of_bevals = function
551| List.Nil ->
552  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
553    List.Nil))
554| List.Cons (bv1, tl) ->
555  (match tl with
556   | List.Nil ->
557     Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
558       List.Nil))
559   | List.Cons (bv2, tl') ->
560     (match tl' with
561      | List.Nil ->
562        (match bv1 with
563         | BVundef ->
564           Errors.Error (List.Cons ((Errors.MSG
565             ErrorMessages.CorruptedPointer), List.Nil))
566         | BVnonzero ->
567           Errors.Error (List.Cons ((Errors.MSG
568             ErrorMessages.CorruptedPointer), List.Nil))
569         | BVXor (x, x0, x1) ->
570           Errors.Error (List.Cons ((Errors.MSG
571             ErrorMessages.CorruptedPointer), List.Nil))
572         | BVByte x ->
573           Errors.Error (List.Cons ((Errors.MSG
574             ErrorMessages.CorruptedPointer), List.Nil))
575         | BVnull x ->
576           Errors.Error (List.Cons ((Errors.MSG
577             ErrorMessages.CorruptedPointer), List.Nil))
578         | BVptr (x, x0) ->
579           Errors.Error (List.Cons ((Errors.MSG
580             ErrorMessages.CorruptedPointer), List.Nil))
581         | BVpc (ptr1, p3) ->
582           (match bv2 with
583            | BVundef ->
584              Errors.Error (List.Cons ((Errors.MSG
585                ErrorMessages.CorruptedPointer), List.Nil))
586            | BVnonzero ->
587              Errors.Error (List.Cons ((Errors.MSG
588                ErrorMessages.CorruptedPointer), List.Nil))
589            | BVXor (x, x0, x1) ->
590              Errors.Error (List.Cons ((Errors.MSG
591                ErrorMessages.CorruptedPointer), List.Nil))
592            | BVByte x ->
593              Errors.Error (List.Cons ((Errors.MSG
594                ErrorMessages.CorruptedPointer), List.Nil))
595            | BVnull x ->
596              Errors.Error (List.Cons ((Errors.MSG
597                ErrorMessages.CorruptedPointer), List.Nil))
598            | BVptr (x, x0) ->
599              Errors.Error (List.Cons ((Errors.MSG
600                ErrorMessages.CorruptedPointer), List.Nil))
601            | BVpc (ptr2, p4) ->
602              (match Bool.andb
603                       (Bool.andb (Nat.eqb (part_no p3) Nat.O)
604                         (Nat.eqb (part_no p4) (Nat.S Nat.O)))
605                       (eq_program_counter ptr1 ptr2) with
606               | Bool.True ->
607                 Obj.magic (Monad.m_return0 (Monad.max_def Errors.res0) ptr2)
608               | Bool.False ->
609                 Errors.Error (List.Cons ((Errors.MSG
610                   ErrorMessages.CorruptedPointer), List.Nil)))))
611      | List.Cons (x, x0) ->
612        Errors.Error (List.Cons ((Errors.MSG ErrorMessages.CorruptedPointer),
613          List.Nil))))
614
615(** val bevals_of_pointer : Pointers.pointer -> beval List.list **)
616let bevals_of_pointer p =
617  List.map (fun n_sig -> BVptr (p, (part_from_sig n_sig)))
618    (Lists.range_strong AST.size_pointer)
619
620(** val bevals_of_pc : program_counter -> beval List.list **)
621let bevals_of_pc p =
622  List.map (fun n_sig -> BVpc (p, (part_from_sig n_sig)))
623    (Lists.range_strong AST.size_pointer)
624
625(** val list_to_pair : 'a1 List.list -> ('a1, 'a1) Types.prod **)
626let list_to_pair l =
627  (match l with
628   | List.Nil ->
629     (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S (Nat.S Nat.O)) __)
630   | List.Cons (a, tl) ->
631     (match tl with
632      | List.Nil ->
633        (fun _ ->
634          Obj.magic Nat.nat_discr (Nat.S Nat.O) (Nat.S (Nat.S Nat.O)) __
635            (fun _ -> Obj.magic Nat.nat_discr Nat.O (Nat.S Nat.O) __))
636      | List.Cons (b, tl') ->
637        (match tl' with
638         | List.Nil -> (fun _ -> { Types.fst = a; Types.snd = b })
639         | List.Cons (c, tl'') ->
640           (fun _ ->
641             Obj.magic Nat.nat_discr (Nat.S (Nat.S (Nat.S
642               (List.length tl'')))) (Nat.S (Nat.S Nat.O)) __ (fun _ ->
643               Obj.magic Nat.nat_discr (Nat.S (Nat.S (List.length tl'')))
644                 (Nat.S Nat.O) __ (fun _ ->
645                 Obj.magic Nat.nat_discr (Nat.S (List.length tl'')) Nat.O __))))))
646    __
647
648(** val beval_pair_of_pointer :
649    Pointers.pointer -> (beval, beval) Types.prod **)
650let beval_pair_of_pointer p =
651  list_to_pair (bevals_of_pointer p)
652
653(** val beval_pair_of_pc : program_counter -> (beval, beval) Types.prod **)
654let beval_pair_of_pc p =
655  list_to_pair (bevals_of_pc p)
656
657(** val bool_of_beval : beval -> Bool.bool Errors.res **)
658let bool_of_beval = function
659| BVundef ->
660  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
661    List.Nil))
662| BVnonzero -> Errors.OK Bool.True
663| BVXor (x, x0, x1) ->
664  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
665    List.Nil))
666| BVByte b ->
667  Errors.OK
668    (BitVector.eq_bv (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
669      Nat.O))))))))
670      (BitVector.zero (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
671        Nat.O))))))))) b)
672| BVnull x -> Errors.OK Bool.False
673| BVptr (x, x0) -> Errors.OK Bool.True
674| BVpc (x, x0) ->
675  Errors.Error (List.Cons ((Errors.MSG ErrorMessages.ValueNotABoolean),
676    List.Nil))
677
678(** val byte_of_val :
679    ErrorMessages.errorMessage -> beval -> BitVector.byte Errors.res **)
680let byte_of_val err = function
681| BVundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
682| BVnonzero -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
683| BVXor (x, x0, x1) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
684| BVByte b0 -> Errors.OK b0
685| BVnull x -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
686| BVptr (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
687| BVpc (x, x0) -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
688
689(** val word_of_list_beval : beval List.list -> Integers.int Errors.res **)
690let word_of_list_beval l =
691  let first_byte = fun l0 ->
692    match l0 with
693    | List.Nil ->
694      Obj.magic (Errors.Error (List.Cons ((Errors.MSG
695        ErrorMessages.NotAnInt32Val), List.Nil)))
696    | List.Cons (hd0, tl) ->
697      Monad.m_bind0 (Monad.max_def Errors.res0)
698        (Obj.magic (byte_of_val ErrorMessages.NotAnInt32Val hd0)) (fun b ->
699        Obj.magic (Errors.OK { Types.fst = b; Types.snd = tl }))
700  in
701  Obj.magic
702    (Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l) (fun b1 l0 ->
703      Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l0) (fun b2 l1 ->
704        Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l1)
705          (fun b3 l2 ->
706          Monad.m_bind2 (Monad.max_def Errors.res0) (first_byte l2)
707            (fun b4 l3 ->
708            match l3 with
709            | List.Nil ->
710              Obj.magic (Errors.OK
711                (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
712                  (Nat.S (Nat.S Nat.O))))))))
713                  (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
714                    (Nat.S Nat.O))))))))
715                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
716                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
717                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) b4
718                  (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
719                    (Nat.S (Nat.S Nat.O))))))))
720                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
721                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
722                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O))))))))) b3
723                    (Vector.append0 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
724                      (Nat.S (Nat.S Nat.O)))))))) (Nat.S (Nat.S (Nat.S (Nat.S
725                      (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))) b2 b1))))
726            | List.Cons (x, x0) ->
727              Obj.magic (Errors.Error (List.Cons ((Errors.MSG
728                ErrorMessages.NotAnInt32Val), List.Nil))))))))
729
730type bebit =
731| BBbit of Bool.bool
732| BBundef
733| BBptrcarry of Bool.bool * Pointers.pointer * part * BitVector.bitVector
734
735(** val bebit_rect_Type4 :
736    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
737    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
738let rec bebit_rect_Type4 h_BBbit h_BBundef h_BBptrcarry = function
739| BBbit x_4790 -> h_BBbit x_4790
740| BBundef -> h_BBundef
741| BBptrcarry (x_4793, x_4792, p, x_4791) ->
742  h_BBptrcarry x_4793 x_4792 p x_4791
743
744(** val bebit_rect_Type5 :
745    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
746    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
747let rec bebit_rect_Type5 h_BBbit h_BBundef h_BBptrcarry = function
748| BBbit x_4798 -> h_BBbit x_4798
749| BBundef -> h_BBundef
750| BBptrcarry (x_4801, x_4800, p, x_4799) ->
751  h_BBptrcarry x_4801 x_4800 p x_4799
752
753(** val bebit_rect_Type3 :
754    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
755    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
756let rec bebit_rect_Type3 h_BBbit h_BBundef h_BBptrcarry = function
757| BBbit x_4806 -> h_BBbit x_4806
758| BBundef -> h_BBundef
759| BBptrcarry (x_4809, x_4808, p, x_4807) ->
760  h_BBptrcarry x_4809 x_4808 p x_4807
761
762(** val bebit_rect_Type2 :
763    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
764    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
765let rec bebit_rect_Type2 h_BBbit h_BBundef h_BBptrcarry = function
766| BBbit x_4814 -> h_BBbit x_4814
767| BBundef -> h_BBundef
768| BBptrcarry (x_4817, x_4816, p, x_4815) ->
769  h_BBptrcarry x_4817 x_4816 p x_4815
770
771(** val bebit_rect_Type1 :
772    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
773    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
774let rec bebit_rect_Type1 h_BBbit h_BBundef h_BBptrcarry = function
775| BBbit x_4822 -> h_BBbit x_4822
776| BBundef -> h_BBundef
777| BBptrcarry (x_4825, x_4824, p, x_4823) ->
778  h_BBptrcarry x_4825 x_4824 p x_4823
779
780(** val bebit_rect_Type0 :
781    (Bool.bool -> 'a1) -> 'a1 -> (Bool.bool -> Pointers.pointer -> part ->
782    BitVector.bitVector -> 'a1) -> bebit -> 'a1 **)
783let rec bebit_rect_Type0 h_BBbit h_BBundef h_BBptrcarry = function
784| BBbit x_4830 -> h_BBbit x_4830
785| BBundef -> h_BBundef
786| BBptrcarry (x_4833, x_4832, p, x_4831) ->
787  h_BBptrcarry x_4833 x_4832 p x_4831
788
789(** val bebit_inv_rect_Type4 :
790    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
791    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
792let bebit_inv_rect_Type4 hterm h1 h2 h3 =
793  let hcut = bebit_rect_Type4 h1 h2 h3 hterm in hcut __
794
795(** val bebit_inv_rect_Type3 :
796    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
797    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
798let bebit_inv_rect_Type3 hterm h1 h2 h3 =
799  let hcut = bebit_rect_Type3 h1 h2 h3 hterm in hcut __
800
801(** val bebit_inv_rect_Type2 :
802    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
803    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
804let bebit_inv_rect_Type2 hterm h1 h2 h3 =
805  let hcut = bebit_rect_Type2 h1 h2 h3 hterm in hcut __
806
807(** val bebit_inv_rect_Type1 :
808    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
809    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
810let bebit_inv_rect_Type1 hterm h1 h2 h3 =
811  let hcut = bebit_rect_Type1 h1 h2 h3 hterm in hcut __
812
813(** val bebit_inv_rect_Type0 :
814    bebit -> (Bool.bool -> __ -> 'a1) -> (__ -> 'a1) -> (Bool.bool ->
815    Pointers.pointer -> part -> BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
816let bebit_inv_rect_Type0 hterm h1 h2 h3 =
817  let hcut = bebit_rect_Type0 h1 h2 h3 hterm in hcut __
818
819(** val bebit_discr : bebit -> bebit -> __ **)
820let bebit_discr x y =
821  Logic.eq_rect_Type2 x
822    (match x with
823     | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
824     | BBundef -> Obj.magic (fun _ dH -> dH)
825     | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
826    y
827
828(** val bebit_jmdiscr : bebit -> bebit -> __ **)
829let bebit_jmdiscr x y =
830  Logic.eq_rect_Type2 x
831    (match x with
832     | BBbit a0 -> Obj.magic (fun _ dH -> dH __)
833     | BBundef -> Obj.magic (fun _ dH -> dH)
834     | BBptrcarry (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __))
835    y
836
837(** val bit_of_val :
838    ErrorMessages.errorMessage -> bebit -> BitVector.bit Errors.res **)
839let bit_of_val err = function
840| BBbit b0 -> Errors.OK b0
841| BBundef -> Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
842| BBptrcarry (x, x0, x1, x2) ->
843  Errors.Error (List.Cons ((Errors.MSG err), List.Nil))
844
Note: See TracBrowser for help on using the repository browser.