source: extracted/byteValues.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

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