source: driver/extracted/pointers.ml @ 3085

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

New major extraction that should have solved all remaining issues.
As tests/PROBLEMI shows, we still have some bugs with:

a) initialization of global data (regression)
b) function pointers call

File size: 11.0 KB
Line 
1open Preamble
2
3open Division
4
5open Exp
6
7open Arithmetic
8
9open Setoids
10
11open Monad
12
13open Option
14
15open Extranat
16
17open Vector
18
19open Div_and_mod
20
21open Jmeq
22
23open Russell
24
25open List
26
27open Util
28
29open FoldStuff
30
31open BitVector
32
33open Types
34
35open Bool
36
37open Relations
38
39open Nat
40
41open Hints_declaration
42
43open Core_notation
44
45open Pts
46
47open Logic
48
49open Positive
50
51open Z
52
53open BitVectorZ
54
55open Proper
56
57open PositiveMap
58
59open Deqsets
60
61open ErrorMessages
62
63open PreIdentifiers
64
65open Errors
66
67open Extralib
68
69open Lists
70
71open Identifiers
72
73open Integers
74
75open AST
76
77type block =
78  Z.z
79  (* singleton inductive, whose constructor was mk_block *)
80
81(** val block_rect_Type4 : (Z.z -> 'a1) -> block -> 'a1 **)
82let rec block_rect_Type4 h_mk_block x_5028 =
83  let block_id = x_5028 in h_mk_block block_id
84
85(** val block_rect_Type5 : (Z.z -> 'a1) -> block -> 'a1 **)
86let rec block_rect_Type5 h_mk_block x_5030 =
87  let block_id = x_5030 in h_mk_block block_id
88
89(** val block_rect_Type3 : (Z.z -> 'a1) -> block -> 'a1 **)
90let rec block_rect_Type3 h_mk_block x_5032 =
91  let block_id = x_5032 in h_mk_block block_id
92
93(** val block_rect_Type2 : (Z.z -> 'a1) -> block -> 'a1 **)
94let rec block_rect_Type2 h_mk_block x_5034 =
95  let block_id = x_5034 in h_mk_block block_id
96
97(** val block_rect_Type1 : (Z.z -> 'a1) -> block -> 'a1 **)
98let rec block_rect_Type1 h_mk_block x_5036 =
99  let block_id = x_5036 in h_mk_block block_id
100
101(** val block_rect_Type0 : (Z.z -> 'a1) -> block -> 'a1 **)
102let rec block_rect_Type0 h_mk_block x_5038 =
103  let block_id = x_5038 in h_mk_block block_id
104
105(** val block_id : block -> Z.z **)
106let rec block_id xxx =
107  let yyy = xxx in yyy
108
109(** val block_inv_rect_Type4 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
110let block_inv_rect_Type4 hterm h1 =
111  let hcut = block_rect_Type4 h1 hterm in hcut __
112
113(** val block_inv_rect_Type3 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
114let block_inv_rect_Type3 hterm h1 =
115  let hcut = block_rect_Type3 h1 hterm in hcut __
116
117(** val block_inv_rect_Type2 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
118let block_inv_rect_Type2 hterm h1 =
119  let hcut = block_rect_Type2 h1 hterm in hcut __
120
121(** val block_inv_rect_Type1 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
122let block_inv_rect_Type1 hterm h1 =
123  let hcut = block_rect_Type1 h1 hterm in hcut __
124
125(** val block_inv_rect_Type0 : block -> (Z.z -> __ -> 'a1) -> 'a1 **)
126let block_inv_rect_Type0 hterm h1 =
127  let hcut = block_rect_Type0 h1 hterm in hcut __
128
129(** val block_discr : block -> block -> __ **)
130let block_discr x y =
131  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
132
133(** val block_jmdiscr : block -> block -> __ **)
134let block_jmdiscr x y =
135  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
136
137(** val block_region : block -> AST.region **)
138let block_region b =
139  match Z.zleb (block_id b) Z.OZ with
140  | Bool.True -> AST.Code
141  | Bool.False -> AST.XData
142
143(** val dummy_block_code : block **)
144let dummy_block_code =
145  Z.OZ
146
147(** val eq_block : block -> block -> Bool.bool **)
148let eq_block b1 b2 =
149  Z.eqZb (block_id b1) (block_id b2)
150
151(** val block_eq : Deqsets.deqSet **)
152let block_eq =
153  Obj.magic eq_block
154
155(** val offset_size : Nat.nat **)
156let offset_size =
157  Nat.times (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
158    Nat.O)))))))) AST.size_pointer
159
160type offset =
161  BitVector.bitVector
162  (* singleton inductive, whose constructor was mk_offset *)
163
164(** val offset_rect_Type4 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
165let rec offset_rect_Type4 h_mk_offset x_5054 =
166  let offv = x_5054 in h_mk_offset offv
167
168(** val offset_rect_Type5 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
169let rec offset_rect_Type5 h_mk_offset x_5056 =
170  let offv = x_5056 in h_mk_offset offv
171
172(** val offset_rect_Type3 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
173let rec offset_rect_Type3 h_mk_offset x_5058 =
174  let offv = x_5058 in h_mk_offset offv
175
176(** val offset_rect_Type2 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
177let rec offset_rect_Type2 h_mk_offset x_5060 =
178  let offv = x_5060 in h_mk_offset offv
179
180(** val offset_rect_Type1 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
181let rec offset_rect_Type1 h_mk_offset x_5062 =
182  let offv = x_5062 in h_mk_offset offv
183
184(** val offset_rect_Type0 : (BitVector.bitVector -> 'a1) -> offset -> 'a1 **)
185let rec offset_rect_Type0 h_mk_offset x_5064 =
186  let offv = x_5064 in h_mk_offset offv
187
188(** val offv : offset -> BitVector.bitVector **)
189let rec offv xxx =
190  let yyy = xxx in yyy
191
192(** val offset_inv_rect_Type4 :
193    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
194let offset_inv_rect_Type4 hterm h1 =
195  let hcut = offset_rect_Type4 h1 hterm in hcut __
196
197(** val offset_inv_rect_Type3 :
198    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
199let offset_inv_rect_Type3 hterm h1 =
200  let hcut = offset_rect_Type3 h1 hterm in hcut __
201
202(** val offset_inv_rect_Type2 :
203    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
204let offset_inv_rect_Type2 hterm h1 =
205  let hcut = offset_rect_Type2 h1 hterm in hcut __
206
207(** val offset_inv_rect_Type1 :
208    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
209let offset_inv_rect_Type1 hterm h1 =
210  let hcut = offset_rect_Type1 h1 hterm in hcut __
211
212(** val offset_inv_rect_Type0 :
213    offset -> (BitVector.bitVector -> __ -> 'a1) -> 'a1 **)
214let offset_inv_rect_Type0 hterm h1 =
215  let hcut = offset_rect_Type0 h1 hterm in hcut __
216
217(** val offset_discr : offset -> offset -> __ **)
218let offset_discr x y =
219  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
220
221(** val offset_jmdiscr : offset -> offset -> __ **)
222let offset_jmdiscr x y =
223  Logic.eq_rect_Type2 x (let a0 = x in Obj.magic (fun _ dH -> dH __)) y
224
225(** val eq_offset : offset -> offset -> Bool.bool **)
226let eq_offset x y =
227  BitVector.eq_bv offset_size (offv x) (offv y)
228
229(** val offset_of_Z : Z.z -> offset **)
230let offset_of_Z z =
231  BitVectorZ.bitvector_of_Z offset_size z
232
233(** val shift_offset : Nat.nat -> offset -> BitVector.bitVector -> offset **)
234let shift_offset n o i =
235  Arithmetic.addition_n offset_size (offv o)
236    (Arithmetic.sign_ext n offset_size i)
237
238(** val shift_offset_n :
239    Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
240    offset **)
241let shift_offset_n n o i sg j =
242  Arithmetic.addition_n offset_size (offv o)
243    (Arithmetic.short_multiplication offset_size
244      (Arithmetic.bitvector_of_nat offset_size i)
245      (match sg with
246       | AST.Signed -> Arithmetic.sign_ext n offset_size j
247       | AST.Unsigned -> Arithmetic.zero_ext n offset_size j))
248
249(** val neg_shift_offset :
250    Nat.nat -> offset -> BitVector.bitVector -> offset **)
251let neg_shift_offset n o i =
252  Arithmetic.subtraction offset_size (offv o)
253    (Arithmetic.sign_ext n offset_size i)
254
255(** val neg_shift_offset_n :
256    Nat.nat -> offset -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
257    offset **)
258let neg_shift_offset_n n o i sg j =
259  Arithmetic.subtraction offset_size (offv o)
260    (Arithmetic.short_multiplication offset_size
261      (Arithmetic.bitvector_of_nat offset_size i)
262      (match sg with
263       | AST.Signed -> Arithmetic.sign_ext n offset_size j
264       | AST.Unsigned -> Arithmetic.zero_ext n offset_size j))
265
266(** val sub_offset : Nat.nat -> offset -> offset -> BitVector.bitVector **)
267let sub_offset n x y =
268  Arithmetic.sign_ext offset_size n
269    (Arithmetic.subtraction offset_size (offv x) (offv y))
270
271(** val zero_offset : offset **)
272let zero_offset =
273  BitVector.zero offset_size
274
275(** val lt_offset : offset -> offset -> Bool.bool **)
276let lt_offset x y =
277  Arithmetic.lt_u offset_size (offv x) (offv y)
278
279type pointer = { pblock : block; poff : offset }
280
281(** val pointer_rect_Type4 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
282let rec pointer_rect_Type4 h_mk_pointer x_5080 =
283  let { pblock = pblock0; poff = poff0 } = x_5080 in
284  h_mk_pointer pblock0 poff0
285
286(** val pointer_rect_Type5 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
287let rec pointer_rect_Type5 h_mk_pointer x_5082 =
288  let { pblock = pblock0; poff = poff0 } = x_5082 in
289  h_mk_pointer pblock0 poff0
290
291(** val pointer_rect_Type3 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
292let rec pointer_rect_Type3 h_mk_pointer x_5084 =
293  let { pblock = pblock0; poff = poff0 } = x_5084 in
294  h_mk_pointer pblock0 poff0
295
296(** val pointer_rect_Type2 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
297let rec pointer_rect_Type2 h_mk_pointer x_5086 =
298  let { pblock = pblock0; poff = poff0 } = x_5086 in
299  h_mk_pointer pblock0 poff0
300
301(** val pointer_rect_Type1 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
302let rec pointer_rect_Type1 h_mk_pointer x_5088 =
303  let { pblock = pblock0; poff = poff0 } = x_5088 in
304  h_mk_pointer pblock0 poff0
305
306(** val pointer_rect_Type0 : (block -> offset -> 'a1) -> pointer -> 'a1 **)
307let rec pointer_rect_Type0 h_mk_pointer x_5090 =
308  let { pblock = pblock0; poff = poff0 } = x_5090 in
309  h_mk_pointer pblock0 poff0
310
311(** val pblock : pointer -> block **)
312let rec pblock xxx =
313  xxx.pblock
314
315(** val poff : pointer -> offset **)
316let rec poff xxx =
317  xxx.poff
318
319(** val pointer_inv_rect_Type4 :
320    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
321let pointer_inv_rect_Type4 hterm h1 =
322  let hcut = pointer_rect_Type4 h1 hterm in hcut __
323
324(** val pointer_inv_rect_Type3 :
325    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
326let pointer_inv_rect_Type3 hterm h1 =
327  let hcut = pointer_rect_Type3 h1 hterm in hcut __
328
329(** val pointer_inv_rect_Type2 :
330    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
331let pointer_inv_rect_Type2 hterm h1 =
332  let hcut = pointer_rect_Type2 h1 hterm in hcut __
333
334(** val pointer_inv_rect_Type1 :
335    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
336let pointer_inv_rect_Type1 hterm h1 =
337  let hcut = pointer_rect_Type1 h1 hterm in hcut __
338
339(** val pointer_inv_rect_Type0 :
340    pointer -> (block -> offset -> __ -> 'a1) -> 'a1 **)
341let pointer_inv_rect_Type0 hterm h1 =
342  let hcut = pointer_rect_Type0 h1 hterm in hcut __
343
344(** val pointer_discr : pointer -> pointer -> __ **)
345let pointer_discr x y =
346  Logic.eq_rect_Type2 x
347    (let { pblock = a0; poff = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
348    y
349
350(** val pointer_jmdiscr : pointer -> pointer -> __ **)
351let pointer_jmdiscr x y =
352  Logic.eq_rect_Type2 x
353    (let { pblock = a0; poff = a1 } = x in Obj.magic (fun _ dH -> dH __ __))
354    y
355
356(** val ptype : pointer -> AST.region **)
357let ptype p =
358  block_region p.pblock
359
360(** val shift_pointer :
361    Nat.nat -> pointer -> BitVector.bitVector -> pointer **)
362let shift_pointer n p i =
363  { pblock = p.pblock; poff = (shift_offset n p.poff i) }
364
365(** val shift_pointer_n :
366    Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
367    pointer **)
368let shift_pointer_n n p i sg j =
369  { pblock = p.pblock; poff = (shift_offset_n n p.poff i sg j) }
370
371(** val neg_shift_pointer :
372    Nat.nat -> pointer -> BitVector.bitVector -> pointer **)
373let neg_shift_pointer n p i =
374  { pblock = p.pblock; poff = (neg_shift_offset n p.poff i) }
375
376(** val neg_shift_pointer_n :
377    Nat.nat -> pointer -> Nat.nat -> AST.signedness -> BitVector.bitVector ->
378    pointer **)
379let neg_shift_pointer_n n p i sg j =
380  { pblock = p.pblock; poff = (neg_shift_offset_n n p.poff i sg j) }
381
382(** val eq_pointer : pointer -> pointer -> Bool.bool **)
383let eq_pointer p1 p2 =
384  Bool.andb (eq_block p1.pblock p2.pblock) (eq_offset p1.poff p2.poff)
385
Note: See TracBrowser for help on using the repository browser.