source: extracted/csem.ml @ 2649

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

...

File size: 50.2 KB
Line 
1open Preamble
2
3open Extra_bool
4
5open Coqlib
6
7open Values
8
9open FrontEndVal
10
11open Hide
12
13open ByteValues
14
15open Division
16
17open Z
18
19open BitVectorZ
20
21open Pointers
22
23open GenMem
24
25open FrontEndMem
26
27open Proper
28
29open PositiveMap
30
31open Deqsets
32
33open Extralib
34
35open Lists
36
37open Identifiers
38
39open Arithmetic
40
41open Vector
42
43open Div_and_mod
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Integers
54
55open AST
56
57open ErrorMessages
58
59open Option
60
61open Setoids
62
63open Monad
64
65open Jmeq
66
67open Russell
68
69open Positive
70
71open PreIdentifiers
72
73open Bool
74
75open Relations
76
77open Nat
78
79open List
80
81open Hints_declaration
82
83open Core_notation
84
85open Pts
86
87open Logic
88
89open Types
90
91open Errors
92
93open Globalenvs
94
95open CostLabel
96
97open Csyntax
98
99open Events
100
101open Smallstep
102
103open TypeComparison
104
105open ClassifyOp
106
107(** val sem_neg :
108    Values.val0 -> Csyntax.type0 -> Values.val0 Types.option **)
109let rec sem_neg v = function
110| Csyntax.Tvoid -> Types.None
111| Csyntax.Tint (sz, x) ->
112  (match v with
113   | Values.Vundef -> Types.None
114   | Values.Vint (sz', n) ->
115     (match AST.eq_intsize sz sz' with
116      | Bool.True ->
117        Types.Some (Values.Vint (sz',
118          (Arithmetic.two_complement_negation (AST.bitsize_of_intsize sz') n)))
119      | Bool.False -> Types.None)
120   | Values.Vnull -> Types.None
121   | Values.Vptr x0 -> Types.None)
122| Csyntax.Tpointer x -> Types.None
123| Csyntax.Tarray (x, x0) -> Types.None
124| Csyntax.Tfunction (x, x0) -> Types.None
125| Csyntax.Tstruct (x, x0) -> Types.None
126| Csyntax.Tunion (x, x0) -> Types.None
127| Csyntax.Tcomp_ptr x -> Types.None
128
129(** val sem_notint : Values.val0 -> Values.val0 Types.option **)
130let rec sem_notint = function
131| Values.Vundef -> Types.None
132| Values.Vint (sz, n) ->
133  Types.Some (Values.Vint (sz,
134    (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz) n
135      (Values.mone0 sz))))
136| Values.Vnull -> Types.None
137| Values.Vptr x -> Types.None
138
139(** val sem_notbool :
140    Values.val0 -> Csyntax.type0 -> Values.val0 Types.option **)
141let rec sem_notbool v = function
142| Csyntax.Tvoid -> Types.None
143| Csyntax.Tint (sz, x) ->
144  (match v with
145   | Values.Vundef -> Types.None
146   | Values.Vint (sz', n) ->
147     (match AST.eq_intsize sz sz' with
148      | Bool.True ->
149        Types.Some
150          (Values.of_bool
151            (BitVector.eq_bv (AST.bitsize_of_intsize sz') n
152              (BitVector.zero (AST.bitsize_of_intsize sz'))))
153      | Bool.False -> Types.None)
154   | Values.Vnull -> Types.None
155   | Values.Vptr x0 -> Types.None)
156| Csyntax.Tpointer x ->
157  (match v with
158   | Values.Vundef -> Types.None
159   | Values.Vint (x0, x1) -> Types.None
160   | Values.Vnull -> Types.Some Values.vtrue
161   | Values.Vptr x0 -> Types.Some Values.vfalse)
162| Csyntax.Tarray (x, x0) -> Types.None
163| Csyntax.Tfunction (x, x0) -> Types.None
164| Csyntax.Tstruct (x, x0) -> Types.None
165| Csyntax.Tunion (x, x0) -> Types.None
166| Csyntax.Tcomp_ptr x -> Types.None
167
168(** val sem_add :
169    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
170    Values.val0 Types.option **)
171let rec sem_add v1 t1 v2 t2 =
172  match ClassifyOp.classify_add t1 t2 with
173  | ClassifyOp.Add_case_ii (x, x0) ->
174    (match v1 with
175     | Values.Vundef -> Types.None
176     | Values.Vint (sz1, n1) ->
177       (match v2 with
178        | Values.Vundef -> Types.None
179        | Values.Vint (sz2, n2) ->
180          AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
181            (sz2,
182            (Arithmetic.addition_n (AST.bitsize_of_intsize sz2) n10 n2))))
183            Types.None
184        | Values.Vnull -> Types.None
185        | Values.Vptr x1 -> Types.None)
186     | Values.Vnull -> Types.None
187     | Values.Vptr x1 -> Types.None)
188  | ClassifyOp.Add_case_pi (x, ty, x0, sg) ->
189    (match v1 with
190     | Values.Vundef -> Types.None
191     | Values.Vint (x1, x2) -> Types.None
192     | Values.Vnull ->
193       (match v2 with
194        | Values.Vundef -> Types.None
195        | Values.Vint (sz2, n2) ->
196          (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
197                   (BitVector.zero (AST.bitsize_of_intsize sz2)) with
198           | Bool.True -> Types.Some Values.Vnull
199           | Bool.False -> Types.None)
200        | Values.Vnull -> Types.None
201        | Values.Vptr x1 -> Types.None)
202     | Values.Vptr ptr1 ->
203       (match v2 with
204        | Values.Vundef -> Types.None
205        | Values.Vint (sz2, n2) ->
206          Types.Some (Values.Vptr
207            (Pointers.shift_pointer_n (AST.bitsize_of_intsize sz2) ptr1
208              (Csyntax.sizeof ty) sg n2))
209        | Values.Vnull -> Types.None
210        | Values.Vptr x1 -> Types.None))
211  | ClassifyOp.Add_case_ip (x, x0, sg, ty) ->
212    (match v1 with
213     | Values.Vundef -> Types.None
214     | Values.Vint (sz1, n1) ->
215       (match v2 with
216        | Values.Vundef -> Types.None
217        | Values.Vint (x1, x2) -> Types.None
218        | Values.Vnull ->
219          (match BitVector.eq_bv (AST.bitsize_of_intsize sz1) n1
220                   (BitVector.zero (AST.bitsize_of_intsize sz1)) with
221           | Bool.True -> Types.Some Values.Vnull
222           | Bool.False -> Types.None)
223        | Values.Vptr ptr2 ->
224          Types.Some (Values.Vptr
225            (Pointers.shift_pointer_n (AST.bitsize_of_intsize sz1) ptr2
226              (Csyntax.sizeof ty) sg n1)))
227     | Values.Vnull -> Types.None
228     | Values.Vptr x1 -> Types.None)
229  | ClassifyOp.Add_default (x, x0) -> Types.None
230
231(** val sem_sub :
232    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
233    Csyntax.type0 -> Values.val0 Types.option **)
234let rec sem_sub v1 t1 v2 t2 target =
235  match ClassifyOp.classify_sub t1 t2 with
236  | ClassifyOp.Sub_case_ii (x, x0) ->
237    (match v1 with
238     | Values.Vundef -> Types.None
239     | Values.Vint (sz1, n1) ->
240       (match v2 with
241        | Values.Vundef -> Types.None
242        | Values.Vint (sz2, n2) ->
243          AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
244            (sz2,
245            (Arithmetic.subtraction (AST.bitsize_of_intsize sz2) n10 n2))))
246            Types.None
247        | Values.Vnull -> Types.None
248        | Values.Vptr x1 -> Types.None)
249     | Values.Vnull -> Types.None
250     | Values.Vptr x1 -> Types.None)
251  | ClassifyOp.Sub_case_pi (x, ty, x0, sg) ->
252    (match v1 with
253     | Values.Vundef -> Types.None
254     | Values.Vint (x1, x2) -> Types.None
255     | Values.Vnull ->
256       (match v2 with
257        | Values.Vundef -> Types.None
258        | Values.Vint (sz2, n2) ->
259          (match BitVector.eq_bv (AST.bitsize_of_intsize sz2) n2
260                   (BitVector.zero (AST.bitsize_of_intsize sz2)) with
261           | Bool.True -> Types.Some Values.Vnull
262           | Bool.False -> Types.None)
263        | Values.Vnull -> Types.None
264        | Values.Vptr x1 -> Types.None)
265     | Values.Vptr ptr1 ->
266       (match v2 with
267        | Values.Vundef -> Types.None
268        | Values.Vint (sz2, n2) ->
269          Types.Some (Values.Vptr
270            (Pointers.neg_shift_pointer_n (AST.bitsize_of_intsize sz2) ptr1
271              (Csyntax.sizeof ty) sg n2))
272        | Values.Vnull -> Types.None
273        | Values.Vptr x1 -> Types.None))
274  | ClassifyOp.Sub_case_pp (x, x0, ty, x1) ->
275    (match v1 with
276     | Values.Vundef -> Types.None
277     | Values.Vint (x2, x3) -> Types.None
278     | Values.Vnull ->
279       (match v2 with
280        | Values.Vundef -> Types.None
281        | Values.Vint (x2, x3) -> Types.None
282        | Values.Vnull ->
283          (match target with
284           | Csyntax.Tvoid -> Types.None
285           | Csyntax.Tint (tsz, tsg) ->
286             Types.Some (Values.Vint (tsz,
287               (BitVector.zero (AST.bitsize_of_intsize tsz))))
288           | Csyntax.Tpointer x2 -> Types.None
289           | Csyntax.Tarray (x2, x3) -> Types.None
290           | Csyntax.Tfunction (x2, x3) -> Types.None
291           | Csyntax.Tstruct (x2, x3) -> Types.None
292           | Csyntax.Tunion (x2, x3) -> Types.None
293           | Csyntax.Tcomp_ptr x2 -> Types.None)
294        | Values.Vptr x2 -> Types.None)
295     | Values.Vptr ptr1 ->
296       (match v2 with
297        | Values.Vundef -> Types.None
298        | Values.Vint (x2, x3) -> Types.None
299        | Values.Vnull -> Types.None
300        | Values.Vptr ptr2 ->
301          (match Pointers.eq_block ptr1.Pointers.pblock ptr2.Pointers.pblock with
302           | Bool.True ->
303             (match Nat.eqb (Csyntax.sizeof ty) Nat.O with
304              | Bool.True -> Types.None
305              | Bool.False ->
306                (match target with
307                 | Csyntax.Tvoid -> Types.None
308                 | Csyntax.Tint (tsz, tsg) ->
309                   (match Arithmetic.division_u (Nat.S (Nat.S (Nat.S (Nat.S
310                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
311                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
312                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
313                            (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
314                            Nat.O)))))))))))))))))))))))))))))))
315                            (Pointers.sub_offset (Nat.S (Nat.S (Nat.S (Nat.S
316                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
317                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
318                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
319                              (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
320                              (Nat.S (Nat.S (Nat.S (Nat.S
321                              Nat.O))))))))))))))))))))))))))))))))
322                              ptr1.Pointers.poff ptr2.Pointers.poff)
323                            (Integers.repr (Csyntax.sizeof ty)) with
324                    | Types.None -> Types.None
325                    | Types.Some v ->
326                      Types.Some (Values.Vint (tsz,
327                        (Arithmetic.zero_ext (Nat.S (Nat.S (Nat.S (Nat.S
328                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
329                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
330                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
331                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
332                          Nat.O))))))))))))))))))))))))))))))))
333                          (AST.bitsize_of_intsize tsz) v))))
334                 | Csyntax.Tpointer x2 -> Types.None
335                 | Csyntax.Tarray (x2, x3) -> Types.None
336                 | Csyntax.Tfunction (x2, x3) -> Types.None
337                 | Csyntax.Tstruct (x2, x3) -> Types.None
338                 | Csyntax.Tunion (x2, x3) -> Types.None
339                 | Csyntax.Tcomp_ptr x2 -> Types.None))
340           | Bool.False -> Types.None)))
341  | ClassifyOp.Sub_default (x, x0) -> Types.None
342
343(** val sem_mul :
344    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
345    Values.val0 Types.option **)
346let rec sem_mul v1 t1 v2 t2 =
347  match ClassifyOp.classify_aop t1 t2 with
348  | ClassifyOp.Aop_case_ii (x, x0) ->
349    (match v1 with
350     | Values.Vundef -> Types.None
351     | Values.Vint (sz1, n1) ->
352       (match v2 with
353        | Values.Vundef -> Types.None
354        | Values.Vint (sz2, n2) ->
355          AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
356            (sz2,
357            (Arithmetic.short_multiplication (AST.bitsize_of_intsize sz2) n10
358              n2)))) Types.None
359        | Values.Vnull -> Types.None
360        | Values.Vptr x1 -> Types.None)
361     | Values.Vnull -> Types.None
362     | Values.Vptr x1 -> Types.None)
363  | ClassifyOp.Aop_default (x, x0) -> Types.None
364
365(** val sem_div :
366    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
367    Values.val0 Types.option **)
368let rec sem_div v1 t1 v2 t2 =
369  match ClassifyOp.classify_aop t1 t2 with
370  | ClassifyOp.Aop_case_ii (x, sg) ->
371    (match v1 with
372     | Values.Vundef -> Types.None
373     | Values.Vint (sz1, n1) ->
374       (match v2 with
375        | Values.Vundef -> Types.None
376        | Values.Vint (sz2, n2) ->
377          (match sg with
378           | AST.Signed ->
379             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
380               Types.option_map (fun x0 -> Values.Vint (sz2, x0))
381                 (Arithmetic.division_s (AST.bitsize_of_intsize sz2) n10 n2))
382               Types.None
383           | AST.Unsigned ->
384             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
385               Types.option_map (fun x0 -> Values.Vint (sz2, x0))
386                 (Arithmetic.division_u
387                   (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
388                     Nat.O)))))))
389                     (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S
390                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
391                       Nat.O)))))))))) n10 n2)) Types.None)
392        | Values.Vnull -> Types.None
393        | Values.Vptr x0 -> Types.None)
394     | Values.Vnull -> Types.None
395     | Values.Vptr x0 -> Types.None)
396  | ClassifyOp.Aop_default (x, x0) -> Types.None
397
398(** val sem_mod :
399    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
400    Values.val0 Types.option **)
401let rec sem_mod v1 t1 v2 t2 =
402  match ClassifyOp.classify_aop t1 t2 with
403  | ClassifyOp.Aop_case_ii (sz, sg) ->
404    (match v1 with
405     | Values.Vundef -> Types.None
406     | Values.Vint (sz1, n1) ->
407       (match v2 with
408        | Values.Vundef -> Types.None
409        | Values.Vint (sz2, n2) ->
410          (match sg with
411           | AST.Signed ->
412             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
413               Types.option_map (fun x -> Values.Vint (sz2, x))
414                 (Arithmetic.modulus_s (AST.bitsize_of_intsize sz2) n10 n2))
415               Types.None
416           | AST.Unsigned ->
417             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
418               Types.option_map (fun x -> Values.Vint (sz2, x))
419                 (Arithmetic.modulus_u
420                   (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
421                     Nat.O)))))))
422                     (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S
423                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
424                       Nat.O)))))))))) n10 n2)) Types.None)
425        | Values.Vnull -> Types.None
426        | Values.Vptr x -> Types.None)
427     | Values.Vnull -> Types.None
428     | Values.Vptr x -> Types.None)
429  | ClassifyOp.Aop_default (x, x0) -> Types.None
430
431(** val sem_and : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
432let rec sem_and v1 v2 =
433  match v1 with
434  | Values.Vundef -> Types.None
435  | Values.Vint (sz1, n1) ->
436    (match v2 with
437     | Values.Vundef -> Types.None
438     | Values.Vint (sz2, n2) ->
439       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
440         (sz2,
441         (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2))))
442         Types.None
443     | Values.Vnull -> Types.None
444     | Values.Vptr x -> Types.None)
445  | Values.Vnull -> Types.None
446  | Values.Vptr x -> Types.None
447
448(** val sem_or : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
449let rec sem_or v1 v2 =
450  match v1 with
451  | Values.Vundef -> Types.None
452  | Values.Vint (sz1, n1) ->
453    (match v2 with
454     | Values.Vundef -> Types.None
455     | Values.Vint (sz2, n2) ->
456       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
457         (sz2,
458         (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
459           n2)))) Types.None
460     | Values.Vnull -> Types.None
461     | Values.Vptr x -> Types.None)
462  | Values.Vnull -> Types.None
463  | Values.Vptr x -> Types.None
464
465(** val sem_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
466let rec sem_xor v1 v2 =
467  match v1 with
468  | Values.Vundef -> Types.None
469  | Values.Vint (sz1, n1) ->
470    (match v2 with
471     | Values.Vundef -> Types.None
472     | Values.Vint (sz2, n2) ->
473       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
474         (sz2,
475         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
476           n2)))) Types.None
477     | Values.Vnull -> Types.None
478     | Values.Vptr x -> Types.None)
479  | Values.Vnull -> Types.None
480  | Values.Vptr x -> Types.None
481
482(** val sem_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
483let rec sem_shl v1 v2 =
484  match v1 with
485  | Values.Vundef -> Types.None
486  | Values.Vint (sz1, n1) ->
487    (match v2 with
488     | Values.Vundef -> Types.None
489     | Values.Vint (sz2, n2) ->
490       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
491                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
492                  (AST.bitsize_of_intsize sz1)) with
493        | Bool.True ->
494          Types.Some (Values.Vint (sz1,
495            (Vector.shift_left (AST.bitsize_of_intsize sz1)
496              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
497              n1 Bool.False)))
498        | Bool.False -> Types.None)
499     | Values.Vnull -> Types.None
500     | Values.Vptr x -> Types.None)
501  | Values.Vnull -> Types.None
502  | Values.Vptr x -> Types.None
503
504(** val sem_shr :
505    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
506    Values.val0 Types.option **)
507let rec sem_shr v1 t1 v2 t2 =
508  match ClassifyOp.classify_aop t1 t2 with
509  | ClassifyOp.Aop_case_ii (x, sg) ->
510    (match v1 with
511     | Values.Vundef -> Types.None
512     | Values.Vint (sz1, n1) ->
513       (match v2 with
514        | Values.Vundef -> Types.None
515        | Values.Vint (sz2, n2) ->
516          (match sg with
517           | AST.Signed ->
518             (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
519                      (Arithmetic.bitvector_of_nat
520                        (AST.bitsize_of_intsize sz2)
521                        (AST.bitsize_of_intsize sz1)) with
522              | Bool.True ->
523                Types.Some (Values.Vint (sz1,
524                  (Vector.shift_right
525                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
526                      (Nat.S Nat.O)))))))
527                      (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
528                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
529                        Nat.O))))))))))
530                    (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2)
531                      n2) n1
532                    (Vector.head'
533                      (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
534                        (Nat.S Nat.O)))))))
535                        (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
536                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
537                          Nat.O)))))))))) n1))))
538              | Bool.False -> Types.None)
539           | AST.Unsigned ->
540             (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
541                      (Arithmetic.bitvector_of_nat
542                        (AST.bitsize_of_intsize sz2)
543                        (AST.bitsize_of_intsize sz1)) with
544              | Bool.True ->
545                Types.Some (Values.Vint (sz1,
546                  (Vector.shift_right
547                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
548                      (Nat.S Nat.O)))))))
549                      (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
550                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
551                        Nat.O))))))))))
552                    (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2)
553                      n2) n1 Bool.False)))
554              | Bool.False -> Types.None))
555        | Values.Vnull -> Types.None
556        | Values.Vptr x0 -> Types.None)
557     | Values.Vnull -> Types.None
558     | Values.Vptr x0 -> Types.None)
559  | ClassifyOp.Aop_default (x, x0) -> Types.None
560
561(** val sem_cmp_mismatch :
562    Integers.comparison -> Values.val0 Types.option **)
563let rec sem_cmp_mismatch = function
564| Integers.Ceq -> Types.Some Values.vfalse
565| Integers.Cne -> Types.Some Values.vtrue
566| Integers.Clt -> Types.None
567| Integers.Cle -> Types.None
568| Integers.Cgt -> Types.None
569| Integers.Cge -> Types.None
570
571(** val sem_cmp_match : Integers.comparison -> Values.val0 Types.option **)
572let rec sem_cmp_match = function
573| Integers.Ceq -> Types.Some Values.vtrue
574| Integers.Cne -> Types.Some Values.vfalse
575| Integers.Clt -> Types.None
576| Integers.Cle -> Types.None
577| Integers.Cgt -> Types.None
578| Integers.Cge -> Types.None
579
580(** val sem_cmp :
581    Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
582    Csyntax.type0 -> GenMem.mem1 -> Values.val0 Types.option **)
583let rec sem_cmp c v1 t1 v2 t2 m =
584  match ClassifyOp.classify_cmp t1 t2 with
585  | ClassifyOp.Cmp_case_ii (x, sg) ->
586    (match v1 with
587     | Values.Vundef -> Types.None
588     | Values.Vint (sz1, n1) ->
589       (match v2 with
590        | Values.Vundef -> Types.None
591        | Values.Vint (sz2, n2) ->
592          (match sg with
593           | AST.Signed ->
594             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
595               (Values.of_bool
596                 (Values.cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)))
597               Types.None
598           | AST.Unsigned ->
599             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
600               (Values.of_bool
601                 (Values.cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)))
602               Types.None)
603        | Values.Vnull -> Types.None
604        | Values.Vptr x0 -> Types.None)
605     | Values.Vnull -> Types.None
606     | Values.Vptr x0 -> Types.None)
607  | ClassifyOp.Cmp_case_pp (x, x0) ->
608    (match v1 with
609     | Values.Vundef -> Types.None
610     | Values.Vint (x1, x2) -> Types.None
611     | Values.Vnull ->
612       (match v2 with
613        | Values.Vundef -> Types.None
614        | Values.Vint (x1, x2) -> Types.None
615        | Values.Vnull -> sem_cmp_match c
616        | Values.Vptr ptr2 -> sem_cmp_mismatch c)
617     | Values.Vptr ptr1 ->
618       (match v2 with
619        | Values.Vundef -> Types.None
620        | Values.Vint (x1, x2) -> Types.None
621        | Values.Vnull -> sem_cmp_mismatch c
622        | Values.Vptr ptr2 ->
623          (match Bool.andb (FrontEndMem.valid_pointer m ptr1)
624                   (FrontEndMem.valid_pointer m ptr2) with
625           | Bool.True ->
626             (match Pointers.eq_block ptr1.Pointers.pblock
627                      ptr2.Pointers.pblock with
628              | Bool.True ->
629                Types.Some
630                  (Values.of_bool
631                    (Values.cmp_offset c ptr1.Pointers.poff
632                      ptr2.Pointers.poff))
633              | Bool.False -> sem_cmp_mismatch c)
634           | Bool.False -> Types.None)))
635  | ClassifyOp.Cmp_default (x, x0) -> Types.None
636
637(** val cast_bool_to_target :
638    Csyntax.type0 -> Values.val0 Types.option -> Values.val0 Types.option **)
639let cast_bool_to_target ty = function
640| Types.None -> Types.None
641| Types.Some v ->
642  (match ty with
643   | Csyntax.Tvoid -> Types.None
644   | Csyntax.Tint (sz, sg) -> Types.Some (Values.zero_ext1 sz v)
645   | Csyntax.Tpointer x -> Types.None
646   | Csyntax.Tarray (x, x0) -> Types.None
647   | Csyntax.Tfunction (x, x0) -> Types.None
648   | Csyntax.Tstruct (x, x0) -> Types.None
649   | Csyntax.Tunion (x, x0) -> Types.None
650   | Csyntax.Tcomp_ptr x -> Types.None)
651
652(** val sem_unary_operation :
653    Csyntax.unary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
654    Types.option **)
655let sem_unary_operation op0 v ty =
656  match op0 with
657  | Csyntax.Onotbool -> sem_notbool v ty
658  | Csyntax.Onotint -> sem_notint v
659  | Csyntax.Oneg -> sem_neg v ty
660
661(** val sem_binary_operation :
662    Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
663    -> Csyntax.type0 -> GenMem.mem1 -> Csyntax.type0 -> Values.val0
664    Types.option **)
665let rec sem_binary_operation op0 v1 t1 v2 t2 m ty =
666  match op0 with
667  | Csyntax.Oadd -> sem_add v1 t1 v2 t2
668  | Csyntax.Osub -> sem_sub v1 t1 v2 t2 ty
669  | Csyntax.Omul -> sem_mul v1 t1 v2 t2
670  | Csyntax.Odiv -> sem_div v1 t1 v2 t2
671  | Csyntax.Omod -> sem_mod v1 t1 v2 t2
672  | Csyntax.Oand -> sem_and v1 v2
673  | Csyntax.Oor -> sem_or v1 v2
674  | Csyntax.Oxor -> sem_xor v1 v2
675  | Csyntax.Oshl -> sem_shl v1 v2
676  | Csyntax.Oshr -> sem_shr v1 t1 v2 t2
677  | Csyntax.Oeq ->
678    cast_bool_to_target ty (sem_cmp Integers.Ceq v1 t1 v2 t2 m)
679  | Csyntax.One0 ->
680    cast_bool_to_target ty (sem_cmp Integers.Cne v1 t1 v2 t2 m)
681  | Csyntax.Olt ->
682    cast_bool_to_target ty (sem_cmp Integers.Clt v1 t1 v2 t2 m)
683  | Csyntax.Ogt ->
684    cast_bool_to_target ty (sem_cmp Integers.Cgt v1 t1 v2 t2 m)
685  | Csyntax.Ole ->
686    cast_bool_to_target ty (sem_cmp Integers.Cle v1 t1 v2 t2 m)
687  | Csyntax.Oge ->
688    cast_bool_to_target ty (sem_cmp Integers.Cge v1 t1 v2 t2 m)
689
690(** val cast_int_int :
691    AST.intsize -> AST.signedness -> AST.intsize -> BitVector.bitVector ->
692    BitVector.bitVector **)
693let rec cast_int_int sz sg dstsz i =
694  match sg with
695  | AST.Signed ->
696    Arithmetic.sign_ext (AST.bitsize_of_intsize sz)
697      (AST.bitsize_of_intsize dstsz) i
698  | AST.Unsigned ->
699    Arithmetic.zero_ext (AST.bitsize_of_intsize sz)
700      (AST.bitsize_of_intsize dstsz) i
701
702type genv0 = Csyntax.clight_fundef Globalenvs.genv_t
703
704type env = Pointers.block Identifiers.identifier_map
705
706(** val empty_env : env **)
707let empty_env =
708  Identifiers.empty_map PreIdentifiers.SymbolTag
709
710(** val load_value_of_type :
711    Csyntax.type0 -> GenMem.mem1 -> Pointers.block -> Pointers.offset ->
712    Values.val0 Types.option **)
713let rec load_value_of_type ty m b ofs =
714  match Csyntax.access_mode ty with
715  | Csyntax.By_value chunk ->
716    FrontEndMem.loadv chunk m (Values.Vptr { Pointers.pblock = b;
717      Pointers.poff = ofs })
718  | Csyntax.By_reference ->
719    Types.Some (Values.Vptr { Pointers.pblock = b; Pointers.poff = ofs })
720  | Csyntax.By_nothing x -> Types.None
721
722(** val store_value_of_type :
723    Csyntax.type0 -> GenMem.mem1 -> Pointers.block -> Pointers.offset ->
724    Values.val0 -> GenMem.mem1 Types.option **)
725let rec store_value_of_type ty_dest m loc ofs v =
726  match Csyntax.access_mode ty_dest with
727  | Csyntax.By_value chunk ->
728    FrontEndMem.storev chunk m (Values.Vptr { Pointers.pblock = loc;
729      Pointers.poff = ofs }) v
730  | Csyntax.By_reference -> Types.None
731  | Csyntax.By_nothing x -> Types.None
732
733(** val blocks_of_env : env -> Pointers.block List.list **)
734let blocks_of_env e1 =
735  List.map (fun x -> x.Types.snd)
736    (Identifiers.elements PreIdentifiers.SymbolTag e1)
737
738(** val select_switch :
739    AST.intsize -> BitVector.bitVector -> Csyntax.labeled_statements ->
740    Csyntax.labeled_statements Types.option **)
741let rec select_switch sz n sl = match sl with
742| Csyntax.LSdefault x -> Types.Some sl
743| Csyntax.LScase (sz', c, s, sl') ->
744  AST.intsize_eq_elim sz sz' n (fun n0 ->
745    match BitVector.eq_bv (AST.bitsize_of_intsize sz') c n0 with
746    | Bool.True -> Types.Some sl
747    | Bool.False -> select_switch sz' n0 sl') Types.None
748
749(** val seq_of_labeled_statement :
750    Csyntax.labeled_statements -> Csyntax.statement **)
751let rec seq_of_labeled_statement = function
752| Csyntax.LSdefault s -> s
753| Csyntax.LScase (x, c, s, sl') ->
754  Csyntax.Ssequence (s, (seq_of_labeled_statement sl'))
755
756type cont =
757| Kstop
758| Kseq of Csyntax.statement * cont
759| Kwhile of Csyntax.expr * Csyntax.statement * cont
760| Kdowhile of Csyntax.expr * Csyntax.statement * cont
761| Kfor2 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
762| Kfor3 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
763| Kswitch of cont
764| Kcall of ((Pointers.block, Pointers.offset) Types.prod, Csyntax.type0)
765           Types.prod Types.option * Csyntax.function0 * env * cont
766
767(** val cont_rect_Type4 :
768    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
769    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
770    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
771    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
772    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
773    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
774    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
775    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
776let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
777| Kstop -> h_Kstop
778| Kseq (x_5937, x_5936) ->
779  h_Kseq x_5937 x_5936
780    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
781      h_Kswitch h_Kcall x_5936)
782| Kwhile (x_5940, x_5939, x_5938) ->
783  h_Kwhile x_5940 x_5939 x_5938
784    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
785      h_Kswitch h_Kcall x_5938)
786| Kdowhile (x_5943, x_5942, x_5941) ->
787  h_Kdowhile x_5943 x_5942 x_5941
788    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
789      h_Kswitch h_Kcall x_5941)
790| Kfor2 (x_5947, x_5946, x_5945, x_5944) ->
791  h_Kfor2 x_5947 x_5946 x_5945 x_5944
792    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
793      h_Kswitch h_Kcall x_5944)
794| Kfor3 (x_5951, x_5950, x_5949, x_5948) ->
795  h_Kfor3 x_5951 x_5950 x_5949 x_5948
796    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
797      h_Kswitch h_Kcall x_5948)
798| Kswitch x_5952 ->
799  h_Kswitch x_5952
800    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
801      h_Kswitch h_Kcall x_5952)
802| Kcall (x_5956, x_5955, x_5954, x_5953) ->
803  h_Kcall x_5956 x_5955 x_5954 x_5953
804    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
805      h_Kswitch h_Kcall x_5953)
806
807(** val cont_rect_Type3 :
808    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
809    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
810    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
811    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
812    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
813    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
814    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
815    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
816let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
817| Kstop -> h_Kstop
818| Kseq (x_5997, x_5996) ->
819  h_Kseq x_5997 x_5996
820    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
821      h_Kswitch h_Kcall x_5996)
822| Kwhile (x_6000, x_5999, x_5998) ->
823  h_Kwhile x_6000 x_5999 x_5998
824    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
825      h_Kswitch h_Kcall x_5998)
826| Kdowhile (x_6003, x_6002, x_6001) ->
827  h_Kdowhile x_6003 x_6002 x_6001
828    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
829      h_Kswitch h_Kcall x_6001)
830| Kfor2 (x_6007, x_6006, x_6005, x_6004) ->
831  h_Kfor2 x_6007 x_6006 x_6005 x_6004
832    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
833      h_Kswitch h_Kcall x_6004)
834| Kfor3 (x_6011, x_6010, x_6009, x_6008) ->
835  h_Kfor3 x_6011 x_6010 x_6009 x_6008
836    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
837      h_Kswitch h_Kcall x_6008)
838| Kswitch x_6012 ->
839  h_Kswitch x_6012
840    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
841      h_Kswitch h_Kcall x_6012)
842| Kcall (x_6016, x_6015, x_6014, x_6013) ->
843  h_Kcall x_6016 x_6015 x_6014 x_6013
844    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
845      h_Kswitch h_Kcall x_6013)
846
847(** val cont_rect_Type2 :
848    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
849    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
850    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
851    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
852    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
853    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
854    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
855    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
856let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
857| Kstop -> h_Kstop
858| Kseq (x_6027, x_6026) ->
859  h_Kseq x_6027 x_6026
860    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
861      h_Kswitch h_Kcall x_6026)
862| Kwhile (x_6030, x_6029, x_6028) ->
863  h_Kwhile x_6030 x_6029 x_6028
864    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
865      h_Kswitch h_Kcall x_6028)
866| Kdowhile (x_6033, x_6032, x_6031) ->
867  h_Kdowhile x_6033 x_6032 x_6031
868    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
869      h_Kswitch h_Kcall x_6031)
870| Kfor2 (x_6037, x_6036, x_6035, x_6034) ->
871  h_Kfor2 x_6037 x_6036 x_6035 x_6034
872    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
873      h_Kswitch h_Kcall x_6034)
874| Kfor3 (x_6041, x_6040, x_6039, x_6038) ->
875  h_Kfor3 x_6041 x_6040 x_6039 x_6038
876    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
877      h_Kswitch h_Kcall x_6038)
878| Kswitch x_6042 ->
879  h_Kswitch x_6042
880    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
881      h_Kswitch h_Kcall x_6042)
882| Kcall (x_6046, x_6045, x_6044, x_6043) ->
883  h_Kcall x_6046 x_6045 x_6044 x_6043
884    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
885      h_Kswitch h_Kcall x_6043)
886
887(** val cont_rect_Type1 :
888    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
889    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
890    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
891    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
892    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
893    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
894    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
895    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
896let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
897| Kstop -> h_Kstop
898| Kseq (x_6057, x_6056) ->
899  h_Kseq x_6057 x_6056
900    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
901      h_Kswitch h_Kcall x_6056)
902| Kwhile (x_6060, x_6059, x_6058) ->
903  h_Kwhile x_6060 x_6059 x_6058
904    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
905      h_Kswitch h_Kcall x_6058)
906| Kdowhile (x_6063, x_6062, x_6061) ->
907  h_Kdowhile x_6063 x_6062 x_6061
908    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
909      h_Kswitch h_Kcall x_6061)
910| Kfor2 (x_6067, x_6066, x_6065, x_6064) ->
911  h_Kfor2 x_6067 x_6066 x_6065 x_6064
912    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
913      h_Kswitch h_Kcall x_6064)
914| Kfor3 (x_6071, x_6070, x_6069, x_6068) ->
915  h_Kfor3 x_6071 x_6070 x_6069 x_6068
916    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
917      h_Kswitch h_Kcall x_6068)
918| Kswitch x_6072 ->
919  h_Kswitch x_6072
920    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
921      h_Kswitch h_Kcall x_6072)
922| Kcall (x_6076, x_6075, x_6074, x_6073) ->
923  h_Kcall x_6076 x_6075 x_6074 x_6073
924    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
925      h_Kswitch h_Kcall x_6073)
926
927(** val cont_rect_Type0 :
928    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
929    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
930    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
931    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
932    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
933    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
934    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
935    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
936let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
937| Kstop -> h_Kstop
938| Kseq (x_6087, x_6086) ->
939  h_Kseq x_6087 x_6086
940    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
941      h_Kswitch h_Kcall x_6086)
942| Kwhile (x_6090, x_6089, x_6088) ->
943  h_Kwhile x_6090 x_6089 x_6088
944    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
945      h_Kswitch h_Kcall x_6088)
946| Kdowhile (x_6093, x_6092, x_6091) ->
947  h_Kdowhile x_6093 x_6092 x_6091
948    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
949      h_Kswitch h_Kcall x_6091)
950| Kfor2 (x_6097, x_6096, x_6095, x_6094) ->
951  h_Kfor2 x_6097 x_6096 x_6095 x_6094
952    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
953      h_Kswitch h_Kcall x_6094)
954| Kfor3 (x_6101, x_6100, x_6099, x_6098) ->
955  h_Kfor3 x_6101 x_6100 x_6099 x_6098
956    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
957      h_Kswitch h_Kcall x_6098)
958| Kswitch x_6102 ->
959  h_Kswitch x_6102
960    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
961      h_Kswitch h_Kcall x_6102)
962| Kcall (x_6106, x_6105, x_6104, x_6103) ->
963  h_Kcall x_6106 x_6105 x_6104 x_6103
964    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
965      h_Kswitch h_Kcall x_6103)
966
967(** val cont_inv_rect_Type4 :
968    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
969    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
970    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
971    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
972    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
973    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
974    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
975    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
976    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
977let cont_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
978  let hcut = cont_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
979
980(** val cont_inv_rect_Type3 :
981    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
982    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
983    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
984    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
985    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
986    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
987    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
988    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
989    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
990let cont_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
991  let hcut = cont_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
992
993(** val cont_inv_rect_Type2 :
994    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
995    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
996    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
997    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
998    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
999    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1000    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1001    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1002    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1003let cont_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1004  let hcut = cont_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1005
1006(** val cont_inv_rect_Type1 :
1007    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
1008    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1009    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1010    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1011    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1012    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1013    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1014    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1015    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1016let cont_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1017  let hcut = cont_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1018
1019(** val cont_inv_rect_Type0 :
1020    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
1021    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1022    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1023    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1024    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1025    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1026    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1027    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1028    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1029let cont_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1030  let hcut = cont_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1031
1032(** val cont_discr : cont -> cont -> __ **)
1033let cont_discr x y =
1034  Logic.eq_rect_Type2 x
1035    (match x with
1036     | Kstop -> Obj.magic (fun _ dH -> dH)
1037     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1038     | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1039     | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1040     | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1041     | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1042     | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
1043     | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1044
1045(** val cont_jmdiscr : cont -> cont -> __ **)
1046let cont_jmdiscr x y =
1047  Logic.eq_rect_Type2 x
1048    (match x with
1049     | Kstop -> Obj.magic (fun _ dH -> dH)
1050     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1051     | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1052     | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1053     | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1054     | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1055     | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
1056     | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1057
1058(** val call_cont : cont -> cont **)
1059let rec call_cont k = match k with
1060| Kstop -> k
1061| Kseq (s, k0) -> call_cont k0
1062| Kwhile (e1, s, k0) -> call_cont k0
1063| Kdowhile (e1, s, k0) -> call_cont k0
1064| Kfor2 (e2, e3, s, k0) -> call_cont k0
1065| Kfor3 (e2, e3, s, k0) -> call_cont k0
1066| Kswitch k0 -> call_cont k0
1067| Kcall (x, x0, x1, x2) -> k
1068
1069type state0 =
1070| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem1
1071| Callstate of Csyntax.clight_fundef * Values.val0 List.list * cont
1072   * GenMem.mem1
1073| Returnstate of Values.val0 * cont * GenMem.mem1
1074| Finalstate of Integers.int
1075
1076(** val state_rect_Type4 :
1077    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1078    'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
1079    GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
1080    (Integers.int -> 'a1) -> state0 -> 'a1 **)
1081let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
1082| State (f, s, k, e1, m) -> h_State f s k e1 m
1083| Callstate (fd, args, k, m) -> h_Callstate fd args k m
1084| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1085| Finalstate r -> h_Finalstate r
1086
1087(** val state_rect_Type5 :
1088    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1089    'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
1090    GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
1091    (Integers.int -> 'a1) -> state0 -> 'a1 **)
1092let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
1093| State (f, s, k, e1, m) -> h_State f s k e1 m
1094| Callstate (fd, args, k, m) -> h_Callstate fd args k m
1095| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1096| Finalstate r -> h_Finalstate r
1097
1098(** val state_rect_Type3 :
1099    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1100    'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
1101    GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
1102    (Integers.int -> 'a1) -> state0 -> 'a1 **)
1103let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
1104| State (f, s, k, e1, m) -> h_State f s k e1 m
1105| Callstate (fd, args, k, m) -> h_Callstate fd args k m
1106| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1107| Finalstate r -> h_Finalstate r
1108
1109(** val state_rect_Type2 :
1110    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1111    'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
1112    GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
1113    (Integers.int -> 'a1) -> state0 -> 'a1 **)
1114let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
1115| State (f, s, k, e1, m) -> h_State f s k e1 m
1116| Callstate (fd, args, k, m) -> h_Callstate fd args k m
1117| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1118| Finalstate r -> h_Finalstate r
1119
1120(** val state_rect_Type1 :
1121    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1122    'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
1123    GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
1124    (Integers.int -> 'a1) -> state0 -> 'a1 **)
1125let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
1126| State (f, s, k, e1, m) -> h_State f s k e1 m
1127| Callstate (fd, args, k, m) -> h_Callstate fd args k m
1128| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1129| Finalstate r -> h_Finalstate r
1130
1131(** val state_rect_Type0 :
1132    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem1 ->
1133    'a1) -> (Csyntax.clight_fundef -> Values.val0 List.list -> cont ->
1134    GenMem.mem1 -> 'a1) -> (Values.val0 -> cont -> GenMem.mem1 -> 'a1) ->
1135    (Integers.int -> 'a1) -> state0 -> 'a1 **)
1136let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
1137| State (f, s, k, e1, m) -> h_State f s k e1 m
1138| Callstate (fd, args, k, m) -> h_Callstate fd args k m
1139| Returnstate (res1, k, m) -> h_Returnstate res1 k m
1140| Finalstate r -> h_Finalstate r
1141
1142(** val state_inv_rect_Type4 :
1143    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1144    GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
1145    List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
1146    GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1147let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
1148  let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
1149
1150(** val state_inv_rect_Type3 :
1151    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1152    GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
1153    List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
1154    GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1155let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
1156  let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
1157
1158(** val state_inv_rect_Type2 :
1159    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1160    GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
1161    List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
1162    GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1163let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
1164  let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
1165
1166(** val state_inv_rect_Type1 :
1167    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1168    GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
1169    List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
1170    GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1171let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
1172  let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
1173
1174(** val state_inv_rect_Type0 :
1175    state0 -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1176    GenMem.mem1 -> __ -> 'a1) -> (Csyntax.clight_fundef -> Values.val0
1177    List.list -> cont -> GenMem.mem1 -> __ -> 'a1) -> (Values.val0 -> cont ->
1178    GenMem.mem1 -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1179let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
1180  let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
1181
1182(** val state_discr : state0 -> state0 -> __ **)
1183let state_discr x y =
1184  Logic.eq_rect_Type2 x
1185    (match x with
1186     | State (a0, a1, a2, a3, a4) ->
1187       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1188     | Callstate (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1189     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1190     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
1191
1192(** val state_jmdiscr : state0 -> state0 -> __ **)
1193let state_jmdiscr x y =
1194  Logic.eq_rect_Type2 x
1195    (match x with
1196     | State (a0, a1, a2, a3, a4) ->
1197       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1198     | Callstate (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1199     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1200     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
1201
1202(** val find_label :
1203    Csyntax.label -> Csyntax.statement -> cont -> (Csyntax.statement, cont)
1204    Types.prod Types.option **)
1205let rec find_label lbl s k =
1206  match s with
1207  | Csyntax.Sskip -> Types.None
1208  | Csyntax.Sassign (x, x0) -> Types.None
1209  | Csyntax.Scall (x, x0, x1) -> Types.None
1210  | Csyntax.Ssequence (s1, s2) ->
1211    (match find_label lbl s1 (Kseq (s2, k)) with
1212     | Types.None -> find_label lbl s2 k
1213     | Types.Some sk -> Types.Some sk)
1214  | Csyntax.Sifthenelse (a, s1, s2) ->
1215    (match find_label lbl s1 k with
1216     | Types.None -> find_label lbl s2 k
1217     | Types.Some sk -> Types.Some sk)
1218  | Csyntax.Swhile (a, s1) -> find_label lbl s1 (Kwhile (a, s1, k))
1219  | Csyntax.Sdowhile (a, s1) -> find_label lbl s1 (Kdowhile (a, s1, k))
1220  | Csyntax.Sfor (a1, a2, a3, s1) ->
1221    (match find_label lbl a1 (Kseq ((Csyntax.Sfor (Csyntax.Sskip, a2, a3,
1222             s1)), k)) with
1223     | Types.None ->
1224       (match find_label lbl s1 (Kfor2 (a2, a3, s1, k)) with
1225        | Types.None -> find_label lbl a3 (Kfor3 (a2, a3, s1, k))
1226        | Types.Some sk -> Types.Some sk)
1227     | Types.Some sk -> Types.Some sk)
1228  | Csyntax.Sbreak -> Types.None
1229  | Csyntax.Scontinue -> Types.None
1230  | Csyntax.Sreturn x -> Types.None
1231  | Csyntax.Sswitch (e1, sl) -> find_label_ls lbl sl (Kswitch k)
1232  | Csyntax.Slabel (lbl', s') ->
1233    (match AST.ident_eq lbl lbl' with
1234     | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
1235     | Types.Inr _ -> find_label lbl s' k)
1236  | Csyntax.Sgoto x -> Types.None
1237  | Csyntax.Scost (c, s') -> find_label lbl s' k
1238(** val find_label_ls :
1239    Csyntax.label -> Csyntax.labeled_statements -> cont ->
1240    (Csyntax.statement, cont) Types.prod Types.option **)
1241and find_label_ls lbl sl k =
1242  match sl with
1243  | Csyntax.LSdefault s -> find_label lbl s k
1244  | Csyntax.LScase (x, x0, s, sl') ->
1245    (match find_label lbl s (Kseq ((seq_of_labeled_statement sl'), k)) with
1246     | Types.None -> find_label_ls lbl sl' k
1247     | Types.Some sk -> Types.Some sk)
1248
1249(** val fun_typeof : Csyntax.expr -> Csyntax.type0 **)
1250let fun_typeof e1 =
1251  match Csyntax.typeof e1 with
1252  | Csyntax.Tvoid -> Csyntax.Tvoid
1253  | Csyntax.Tint (a, b) -> Csyntax.Tint (a, b)
1254  | Csyntax.Tpointer ty -> ty
1255  | Csyntax.Tarray (a, b) -> Csyntax.Tarray (a, b)
1256  | Csyntax.Tfunction (a, b) -> Csyntax.Tfunction (a, b)
1257  | Csyntax.Tstruct (a, b) -> Csyntax.Tstruct (a, b)
1258  | Csyntax.Tunion (a, b) -> Csyntax.Tunion (a, b)
1259  | Csyntax.Tcomp_ptr a -> Csyntax.Tcomp_ptr a
1260
Note: See TracBrowser for help on using the repository browser.