source: extracted/csem.ml @ 3001

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

New extraction.

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