source: driver/extracted/csem.ml @ 3106

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

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

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

File size: 50.3 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 ptr1.Pointers.pblock ptr2.Pointers.pblock with
304           | Bool.True ->
305             (match Nat.eqb (Csyntax.sizeof ty) Nat.O with
306              | Bool.True -> Types.None
307              | Bool.False ->
308                (match target with
309                 | Csyntax.Tvoid -> Types.None
310                 | Csyntax.Tint (tsz, tsg) ->
311                   (match Arithmetic.division_u (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 (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
316                            Nat.O)))))))))))))))))))))))))))))))
317                            (Pointers.sub_offset (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 (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
323                              Nat.O))))))))))))))))))))))))))))))))
324                              ptr1.Pointers.poff ptr2.Pointers.poff)
325                            (Integers.repr (Csyntax.sizeof ty)) with
326                    | Types.None -> Types.None
327                    | Types.Some v ->
328                      Types.Some (Values.Vint (tsz,
329                        (Arithmetic.zero_ext (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.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.O))))))))))))))))))))))))))))))))
335                          (AST.bitsize_of_intsize tsz) v))))
336                 | Csyntax.Tpointer x2 -> Types.None
337                 | Csyntax.Tarray (x2, x3) -> Types.None
338                 | Csyntax.Tfunction (x2, x3) -> Types.None
339                 | Csyntax.Tstruct (x2, x3) -> Types.None
340                 | Csyntax.Tunion (x2, x3) -> Types.None
341                 | Csyntax.Tcomp_ptr x2 -> Types.None))
342           | Bool.False -> Types.None)))
343  | ClassifyOp.Sub_default (x, x0) -> Types.None
344
345(** val sem_mul :
346    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
347    Values.val0 Types.option **)
348let rec sem_mul v1 t1 v2 t2 =
349  match ClassifyOp.classify_aop t1 t2 with
350  | ClassifyOp.Aop_case_ii (x, x0) ->
351    (match v1 with
352     | Values.Vundef -> Types.None
353     | Values.Vint (sz1, n1) ->
354       (match v2 with
355        | Values.Vundef -> Types.None
356        | Values.Vint (sz2, n2) ->
357          AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
358            (sz2,
359            (Arithmetic.short_multiplication (AST.bitsize_of_intsize sz2) n10
360              n2)))) Types.None
361        | Values.Vnull -> Types.None
362        | Values.Vptr x1 -> Types.None)
363     | Values.Vnull -> Types.None
364     | Values.Vptr x1 -> Types.None)
365  | ClassifyOp.Aop_default (x, x0) -> Types.None
366
367(** val sem_div :
368    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
369    Values.val0 Types.option **)
370let rec sem_div v1 t1 v2 t2 =
371  match ClassifyOp.classify_aop t1 t2 with
372  | ClassifyOp.Aop_case_ii (x, sg) ->
373    (match v1 with
374     | Values.Vundef -> Types.None
375     | Values.Vint (sz1, n1) ->
376       (match v2 with
377        | Values.Vundef -> Types.None
378        | Values.Vint (sz2, n2) ->
379          (match sg with
380           | AST.Signed ->
381             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
382               Types.option_map (fun x0 -> Values.Vint (sz2, x0))
383                 (Arithmetic.division_s (AST.bitsize_of_intsize sz2) n10 n2))
384               Types.None
385           | AST.Unsigned ->
386             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
387               Types.option_map (fun x0 -> Values.Vint (sz2, x0))
388                 (Arithmetic.division_u
389                   (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
390                     Nat.O)))))))
391                     (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S
392                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
393                       Nat.O)))))))))) n10 n2)) Types.None)
394        | Values.Vnull -> Types.None
395        | Values.Vptr x0 -> Types.None)
396     | Values.Vnull -> Types.None
397     | Values.Vptr x0 -> Types.None)
398  | ClassifyOp.Aop_default (x, x0) -> Types.None
399
400(** val sem_mod :
401    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
402    Values.val0 Types.option **)
403let rec sem_mod v1 t1 v2 t2 =
404  match ClassifyOp.classify_aop t1 t2 with
405  | ClassifyOp.Aop_case_ii (sz, sg) ->
406    (match v1 with
407     | Values.Vundef -> Types.None
408     | Values.Vint (sz1, n1) ->
409       (match v2 with
410        | Values.Vundef -> Types.None
411        | Values.Vint (sz2, n2) ->
412          (match sg with
413           | AST.Signed ->
414             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
415               Types.option_map (fun x -> Values.Vint (sz2, x))
416                 (Arithmetic.modulus_s (AST.bitsize_of_intsize sz2) n10 n2))
417               Types.None
418           | AST.Unsigned ->
419             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 ->
420               Types.option_map (fun x -> Values.Vint (sz2, x))
421                 (Arithmetic.modulus_u
422                   (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
423                     Nat.O)))))))
424                     (Nat.times (AST.pred_size_intsize sz2) (Nat.S (Nat.S
425                       (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
426                       Nat.O)))))))))) n10 n2)) Types.None)
427        | Values.Vnull -> Types.None
428        | Values.Vptr x -> Types.None)
429     | Values.Vnull -> Types.None
430     | Values.Vptr x -> Types.None)
431  | ClassifyOp.Aop_default (x, x0) -> Types.None
432
433(** val sem_and : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
434let rec sem_and v1 v2 =
435  match v1 with
436  | Values.Vundef -> Types.None
437  | Values.Vint (sz1, n1) ->
438    (match v2 with
439     | Values.Vundef -> Types.None
440     | Values.Vint (sz2, n2) ->
441       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
442         (sz2,
443         (BitVector.conjunction_bv (AST.bitsize_of_intsize sz2) n10 n2))))
444         Types.None
445     | Values.Vnull -> Types.None
446     | Values.Vptr x -> Types.None)
447  | Values.Vnull -> Types.None
448  | Values.Vptr x -> Types.None
449
450(** val sem_or : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
451let rec sem_or v1 v2 =
452  match v1 with
453  | Values.Vundef -> Types.None
454  | Values.Vint (sz1, n1) ->
455    (match v2 with
456     | Values.Vundef -> Types.None
457     | Values.Vint (sz2, n2) ->
458       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
459         (sz2,
460         (BitVector.inclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
461           n2)))) Types.None
462     | Values.Vnull -> Types.None
463     | Values.Vptr x -> Types.None)
464  | Values.Vnull -> Types.None
465  | Values.Vptr x -> Types.None
466
467(** val sem_xor : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
468let rec sem_xor v1 v2 =
469  match v1 with
470  | Values.Vundef -> Types.None
471  | Values.Vint (sz1, n1) ->
472    (match v2 with
473     | Values.Vundef -> Types.None
474     | Values.Vint (sz2, n2) ->
475       AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some (Values.Vint
476         (sz2,
477         (BitVector.exclusive_disjunction_bv (AST.bitsize_of_intsize sz2) n10
478           n2)))) Types.None
479     | Values.Vnull -> Types.None
480     | Values.Vptr x -> Types.None)
481  | Values.Vnull -> Types.None
482  | Values.Vptr x -> Types.None
483
484(** val sem_shl : Values.val0 -> Values.val0 -> Values.val0 Types.option **)
485let rec sem_shl v1 v2 =
486  match v1 with
487  | Values.Vundef -> Types.None
488  | Values.Vint (sz1, n1) ->
489    (match v2 with
490     | Values.Vundef -> Types.None
491     | Values.Vint (sz2, n2) ->
492       (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
493                (Arithmetic.bitvector_of_nat (AST.bitsize_of_intsize sz2)
494                  (AST.bitsize_of_intsize sz1)) with
495        | Bool.True ->
496          Types.Some (Values.Vint (sz1,
497            (Vector.shift_left (AST.bitsize_of_intsize sz1)
498              (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2) n2)
499              n1 Bool.False)))
500        | Bool.False -> Types.None)
501     | Values.Vnull -> Types.None
502     | Values.Vptr x -> Types.None)
503  | Values.Vnull -> Types.None
504  | Values.Vptr x -> Types.None
505
506(** val sem_shr :
507    Values.val0 -> Csyntax.type0 -> Values.val0 -> Csyntax.type0 ->
508    Values.val0 Types.option **)
509let rec sem_shr v1 t1 v2 t2 =
510  match ClassifyOp.classify_aop t1 t2 with
511  | ClassifyOp.Aop_case_ii (x, sg) ->
512    (match v1 with
513     | Values.Vundef -> Types.None
514     | Values.Vint (sz1, n1) ->
515       (match v2 with
516        | Values.Vundef -> Types.None
517        | Values.Vint (sz2, n2) ->
518          (match sg with
519           | AST.Signed ->
520             (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
521                      (Arithmetic.bitvector_of_nat
522                        (AST.bitsize_of_intsize sz2)
523                        (AST.bitsize_of_intsize sz1)) with
524              | Bool.True ->
525                Types.Some (Values.Vint (sz1,
526                  (Vector.shift_right
527                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
528                      (Nat.S Nat.O)))))))
529                      (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
530                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
531                        Nat.O))))))))))
532                    (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2)
533                      n2) n1
534                    (Vector.head'
535                      (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
536                        (Nat.S Nat.O)))))))
537                        (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
538                          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
539                          Nat.O)))))))))) n1))))
540              | Bool.False -> Types.None)
541           | AST.Unsigned ->
542             (match Arithmetic.lt_u (AST.bitsize_of_intsize sz2) n2
543                      (Arithmetic.bitvector_of_nat
544                        (AST.bitsize_of_intsize sz2)
545                        (AST.bitsize_of_intsize sz1)) with
546              | Bool.True ->
547                Types.Some (Values.Vint (sz1,
548                  (Vector.shift_right
549                    (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
550                      (Nat.S Nat.O)))))))
551                      (Nat.times (AST.pred_size_intsize sz1) (Nat.S (Nat.S
552                        (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
553                        Nat.O))))))))))
554                    (Arithmetic.nat_of_bitvector (AST.bitsize_of_intsize sz2)
555                      n2) n1 Bool.False)))
556              | Bool.False -> Types.None))
557        | Values.Vnull -> Types.None
558        | Values.Vptr x0 -> Types.None)
559     | Values.Vnull -> Types.None
560     | Values.Vptr x0 -> Types.None)
561  | ClassifyOp.Aop_default (x, x0) -> Types.None
562
563(** val sem_cmp_mismatch :
564    Integers.comparison -> Values.val0 Types.option **)
565let rec sem_cmp_mismatch = function
566| Integers.Ceq -> Types.Some Values.vfalse
567| Integers.Cne -> Types.Some Values.vtrue
568| Integers.Clt -> Types.None
569| Integers.Cle -> Types.None
570| Integers.Cgt -> Types.None
571| Integers.Cge -> Types.None
572
573(** val sem_cmp_match : Integers.comparison -> Values.val0 Types.option **)
574let rec sem_cmp_match = function
575| Integers.Ceq -> Types.Some Values.vtrue
576| Integers.Cne -> Types.Some Values.vfalse
577| Integers.Clt -> Types.None
578| Integers.Cle -> Types.None
579| Integers.Cgt -> Types.None
580| Integers.Cge -> Types.None
581
582(** val sem_cmp :
583    Integers.comparison -> Values.val0 -> Csyntax.type0 -> Values.val0 ->
584    Csyntax.type0 -> GenMem.mem -> Values.val0 Types.option **)
585let rec sem_cmp c v1 t1 v2 t2 m =
586  match ClassifyOp.classify_cmp t1 t2 with
587  | ClassifyOp.Cmp_case_ii (x, sg) ->
588    (match v1 with
589     | Values.Vundef -> Types.None
590     | Values.Vint (sz1, n1) ->
591       (match v2 with
592        | Values.Vundef -> Types.None
593        | Values.Vint (sz2, n2) ->
594          (match sg with
595           | AST.Signed ->
596             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
597               (Values.of_bool
598                 (Values.cmp_int (AST.bitsize_of_intsize sz2) c n10 n2)))
599               Types.None
600           | AST.Unsigned ->
601             AST.intsize_eq_elim sz1 sz2 n1 (fun n10 -> Types.Some
602               (Values.of_bool
603                 (Values.cmpu_int (AST.bitsize_of_intsize sz2) c n10 n2)))
604               Types.None)
605        | Values.Vnull -> Types.None
606        | Values.Vptr x0 -> Types.None)
607     | Values.Vnull -> Types.None
608     | Values.Vptr x0 -> Types.None)
609  | ClassifyOp.Cmp_case_pp (x, x0) ->
610    (match v1 with
611     | Values.Vundef -> Types.None
612     | Values.Vint (x1, x2) -> Types.None
613     | Values.Vnull ->
614       (match v2 with
615        | Values.Vundef -> Types.None
616        | Values.Vint (x1, x2) -> Types.None
617        | Values.Vnull -> sem_cmp_match c
618        | Values.Vptr ptr2 -> sem_cmp_mismatch c)
619     | Values.Vptr ptr1 ->
620       (match v2 with
621        | Values.Vundef -> Types.None
622        | Values.Vint (x1, x2) -> Types.None
623        | Values.Vnull -> sem_cmp_mismatch c
624        | Values.Vptr ptr2 ->
625          (match Bool.andb (FrontEndMem.valid_pointer m ptr1)
626                   (FrontEndMem.valid_pointer m ptr2) with
627           | Bool.True ->
628             (match Pointers.eq_block ptr1.Pointers.pblock
629                      ptr2.Pointers.pblock with
630              | Bool.True ->
631                Types.Some
632                  (Values.of_bool
633                    (Values.cmp_offset c ptr1.Pointers.poff
634                      ptr2.Pointers.poff))
635              | Bool.False -> sem_cmp_mismatch c)
636           | Bool.False -> Types.None)))
637  | ClassifyOp.Cmp_default (x, x0) -> Types.None
638
639(** val cast_bool_to_target :
640    Csyntax.type0 -> Values.val0 Types.option -> Values.val0 Types.option **)
641let cast_bool_to_target ty = function
642| Types.None -> Types.None
643| Types.Some v ->
644  (match ty with
645   | Csyntax.Tvoid -> Types.None
646   | Csyntax.Tint (sz, sg) -> Types.Some (Values.zero_ext sz v)
647   | Csyntax.Tpointer x -> Types.None
648   | Csyntax.Tarray (x, x0) -> Types.None
649   | Csyntax.Tfunction (x, x0) -> Types.None
650   | Csyntax.Tstruct (x, x0) -> Types.None
651   | Csyntax.Tunion (x, x0) -> Types.None
652   | Csyntax.Tcomp_ptr x -> Types.None)
653
654(** val sem_unary_operation :
655    Csyntax.unary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
656    Types.option **)
657let sem_unary_operation op v ty =
658  match op with
659  | Csyntax.Onotbool -> sem_notbool v ty
660  | Csyntax.Onotint -> sem_notint v
661  | Csyntax.Oneg -> sem_neg v ty
662
663(** val sem_binary_operation :
664    Csyntax.binary_operation -> Values.val0 -> Csyntax.type0 -> Values.val0
665    -> Csyntax.type0 -> GenMem.mem -> Csyntax.type0 -> Values.val0
666    Types.option **)
667let rec sem_binary_operation op v1 t1 v2 t2 m ty =
668  match op with
669  | Csyntax.Oadd -> sem_add v1 t1 v2 t2
670  | Csyntax.Osub -> sem_sub v1 t1 v2 t2 ty
671  | Csyntax.Omul -> sem_mul v1 t1 v2 t2
672  | Csyntax.Odiv -> sem_div v1 t1 v2 t2
673  | Csyntax.Omod -> sem_mod v1 t1 v2 t2
674  | Csyntax.Oand -> sem_and v1 v2
675  | Csyntax.Oor -> sem_or v1 v2
676  | Csyntax.Oxor -> sem_xor v1 v2
677  | Csyntax.Oshl -> sem_shl v1 v2
678  | Csyntax.Oshr -> sem_shr v1 t1 v2 t2
679  | Csyntax.Oeq ->
680    cast_bool_to_target ty (sem_cmp Integers.Ceq v1 t1 v2 t2 m)
681  | Csyntax.One ->
682    cast_bool_to_target ty (sem_cmp Integers.Cne v1 t1 v2 t2 m)
683  | Csyntax.Olt ->
684    cast_bool_to_target ty (sem_cmp Integers.Clt v1 t1 v2 t2 m)
685  | Csyntax.Ogt ->
686    cast_bool_to_target ty (sem_cmp Integers.Cgt v1 t1 v2 t2 m)
687  | Csyntax.Ole ->
688    cast_bool_to_target ty (sem_cmp Integers.Cle v1 t1 v2 t2 m)
689  | Csyntax.Oge ->
690    cast_bool_to_target ty (sem_cmp Integers.Cge v1 t1 v2 t2 m)
691
692(** val cast_int_int :
693    AST.intsize -> AST.signedness -> AST.intsize -> BitVector.bitVector ->
694    BitVector.bitVector **)
695let rec cast_int_int sz sg dstsz i =
696  match sg with
697  | AST.Signed ->
698    Arithmetic.sign_ext (AST.bitsize_of_intsize sz)
699      (AST.bitsize_of_intsize dstsz) i
700  | AST.Unsigned ->
701    Arithmetic.zero_ext (AST.bitsize_of_intsize sz)
702      (AST.bitsize_of_intsize dstsz) i
703
704type genv = Csyntax.clight_fundef Globalenvs.genv_t
705
706type env = Pointers.block Identifiers.identifier_map
707
708(** val empty_env : env **)
709let empty_env =
710  Identifiers.empty_map PreIdentifiers.SymbolTag
711
712(** val load_value_of_type :
713    Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
714    Values.val0 Types.option **)
715let rec load_value_of_type ty m b ofs =
716  match Csyntax.access_mode ty with
717  | Csyntax.By_value chunk ->
718    FrontEndMem.loadv chunk m (Values.Vptr { Pointers.pblock = b;
719      Pointers.poff = ofs })
720  | Csyntax.By_reference ->
721    Types.Some (Values.Vptr { Pointers.pblock = b; Pointers.poff = ofs })
722  | Csyntax.By_nothing x -> Types.None
723
724(** val store_value_of_type :
725    Csyntax.type0 -> GenMem.mem -> Pointers.block -> Pointers.offset ->
726    Values.val0 -> GenMem.mem Types.option **)
727let rec store_value_of_type ty_dest m loc ofs v =
728  match Csyntax.access_mode ty_dest with
729  | Csyntax.By_value chunk ->
730    FrontEndMem.storev chunk m (Values.Vptr { Pointers.pblock = loc;
731      Pointers.poff = ofs }) v
732  | Csyntax.By_reference -> Types.None
733  | Csyntax.By_nothing x -> Types.None
734
735(** val blocks_of_env : env -> Pointers.block List.list **)
736let blocks_of_env e =
737  List.map (fun x -> x.Types.snd)
738    (Identifiers.elements PreIdentifiers.SymbolTag e)
739
740(** val select_switch :
741    AST.intsize -> BitVector.bitVector -> Csyntax.labeled_statements ->
742    Csyntax.labeled_statements Types.option **)
743let rec select_switch sz n sl = match sl with
744| Csyntax.LSdefault x -> Types.Some sl
745| Csyntax.LScase (sz', c, s, sl') ->
746  AST.intsize_eq_elim sz sz' n (fun n0 ->
747    match BitVector.eq_bv (AST.bitsize_of_intsize sz') c n0 with
748    | Bool.True -> Types.Some sl
749    | Bool.False -> select_switch sz' n0 sl') Types.None
750
751(** val seq_of_labeled_statement :
752    Csyntax.labeled_statements -> Csyntax.statement **)
753let rec seq_of_labeled_statement = function
754| Csyntax.LSdefault s -> s
755| Csyntax.LScase (x, c, s, sl') ->
756  Csyntax.Ssequence (s, (seq_of_labeled_statement sl'))
757
758type cont =
759| Kstop
760| Kseq of Csyntax.statement * cont
761| Kwhile of Csyntax.expr * Csyntax.statement * cont
762| Kdowhile of Csyntax.expr * Csyntax.statement * cont
763| Kfor2 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
764| Kfor3 of Csyntax.expr * Csyntax.statement * Csyntax.statement * cont
765| Kswitch of cont
766| Kcall of ((Pointers.block, Pointers.offset) Types.prod, Csyntax.type0)
767           Types.prod Types.option * Csyntax.function0 * env * cont
768
769(** val cont_rect_Type4 :
770    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
771    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
772    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
773    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
774    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
775    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
776    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
777    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
778let rec cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
779| Kstop -> h_Kstop
780| Kseq (x_8739, x_8738) ->
781  h_Kseq x_8739 x_8738
782    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
783      h_Kswitch h_Kcall x_8738)
784| Kwhile (x_8742, x_8741, x_8740) ->
785  h_Kwhile x_8742 x_8741 x_8740
786    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
787      h_Kswitch h_Kcall x_8740)
788| Kdowhile (x_8745, x_8744, x_8743) ->
789  h_Kdowhile x_8745 x_8744 x_8743
790    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
791      h_Kswitch h_Kcall x_8743)
792| Kfor2 (x_8749, x_8748, x_8747, x_8746) ->
793  h_Kfor2 x_8749 x_8748 x_8747 x_8746
794    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
795      h_Kswitch h_Kcall x_8746)
796| Kfor3 (x_8753, x_8752, x_8751, x_8750) ->
797  h_Kfor3 x_8753 x_8752 x_8751 x_8750
798    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
799      h_Kswitch h_Kcall x_8750)
800| Kswitch x_8754 ->
801  h_Kswitch x_8754
802    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
803      h_Kswitch h_Kcall x_8754)
804| Kcall (x_8758, x_8757, x_8756, x_8755) ->
805  h_Kcall x_8758 x_8757 x_8756 x_8755
806    (cont_rect_Type4 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
807      h_Kswitch h_Kcall x_8755)
808
809(** val cont_rect_Type3 :
810    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
811    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
812    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
813    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
814    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
815    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
816    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
817    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
818let rec cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
819| Kstop -> h_Kstop
820| Kseq (x_8799, x_8798) ->
821  h_Kseq x_8799 x_8798
822    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
823      h_Kswitch h_Kcall x_8798)
824| Kwhile (x_8802, x_8801, x_8800) ->
825  h_Kwhile x_8802 x_8801 x_8800
826    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
827      h_Kswitch h_Kcall x_8800)
828| Kdowhile (x_8805, x_8804, x_8803) ->
829  h_Kdowhile x_8805 x_8804 x_8803
830    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
831      h_Kswitch h_Kcall x_8803)
832| Kfor2 (x_8809, x_8808, x_8807, x_8806) ->
833  h_Kfor2 x_8809 x_8808 x_8807 x_8806
834    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
835      h_Kswitch h_Kcall x_8806)
836| Kfor3 (x_8813, x_8812, x_8811, x_8810) ->
837  h_Kfor3 x_8813 x_8812 x_8811 x_8810
838    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
839      h_Kswitch h_Kcall x_8810)
840| Kswitch x_8814 ->
841  h_Kswitch x_8814
842    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
843      h_Kswitch h_Kcall x_8814)
844| Kcall (x_8818, x_8817, x_8816, x_8815) ->
845  h_Kcall x_8818 x_8817 x_8816 x_8815
846    (cont_rect_Type3 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
847      h_Kswitch h_Kcall x_8815)
848
849(** val cont_rect_Type2 :
850    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
851    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
852    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
853    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
854    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
855    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
856    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
857    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
858let rec cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
859| Kstop -> h_Kstop
860| Kseq (x_8829, x_8828) ->
861  h_Kseq x_8829 x_8828
862    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
863      h_Kswitch h_Kcall x_8828)
864| Kwhile (x_8832, x_8831, x_8830) ->
865  h_Kwhile x_8832 x_8831 x_8830
866    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
867      h_Kswitch h_Kcall x_8830)
868| Kdowhile (x_8835, x_8834, x_8833) ->
869  h_Kdowhile x_8835 x_8834 x_8833
870    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
871      h_Kswitch h_Kcall x_8833)
872| Kfor2 (x_8839, x_8838, x_8837, x_8836) ->
873  h_Kfor2 x_8839 x_8838 x_8837 x_8836
874    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
875      h_Kswitch h_Kcall x_8836)
876| Kfor3 (x_8843, x_8842, x_8841, x_8840) ->
877  h_Kfor3 x_8843 x_8842 x_8841 x_8840
878    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
879      h_Kswitch h_Kcall x_8840)
880| Kswitch x_8844 ->
881  h_Kswitch x_8844
882    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
883      h_Kswitch h_Kcall x_8844)
884| Kcall (x_8848, x_8847, x_8846, x_8845) ->
885  h_Kcall x_8848 x_8847 x_8846 x_8845
886    (cont_rect_Type2 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
887      h_Kswitch h_Kcall x_8845)
888
889(** val cont_rect_Type1 :
890    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
891    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
892    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
893    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
894    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
895    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
896    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
897    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
898let rec cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
899| Kstop -> h_Kstop
900| Kseq (x_8859, x_8858) ->
901  h_Kseq x_8859 x_8858
902    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
903      h_Kswitch h_Kcall x_8858)
904| Kwhile (x_8862, x_8861, x_8860) ->
905  h_Kwhile x_8862 x_8861 x_8860
906    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
907      h_Kswitch h_Kcall x_8860)
908| Kdowhile (x_8865, x_8864, x_8863) ->
909  h_Kdowhile x_8865 x_8864 x_8863
910    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
911      h_Kswitch h_Kcall x_8863)
912| Kfor2 (x_8869, x_8868, x_8867, x_8866) ->
913  h_Kfor2 x_8869 x_8868 x_8867 x_8866
914    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
915      h_Kswitch h_Kcall x_8866)
916| Kfor3 (x_8873, x_8872, x_8871, x_8870) ->
917  h_Kfor3 x_8873 x_8872 x_8871 x_8870
918    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
919      h_Kswitch h_Kcall x_8870)
920| Kswitch x_8874 ->
921  h_Kswitch x_8874
922    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
923      h_Kswitch h_Kcall x_8874)
924| Kcall (x_8878, x_8877, x_8876, x_8875) ->
925  h_Kcall x_8878 x_8877 x_8876 x_8875
926    (cont_rect_Type1 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
927      h_Kswitch h_Kcall x_8875)
928
929(** val cont_rect_Type0 :
930    'a1 -> (Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
931    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
932    Csyntax.statement -> cont -> 'a1 -> 'a1) -> (Csyntax.expr ->
933    Csyntax.statement -> Csyntax.statement -> cont -> 'a1 -> 'a1) ->
934    (Csyntax.expr -> Csyntax.statement -> Csyntax.statement -> cont -> 'a1 ->
935    'a1) -> (cont -> 'a1 -> 'a1) -> (((Pointers.block, Pointers.offset)
936    Types.prod, Csyntax.type0) Types.prod Types.option -> Csyntax.function0
937    -> env -> cont -> 'a1 -> 'a1) -> cont -> 'a1 **)
938let rec cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3 h_Kswitch h_Kcall = function
939| Kstop -> h_Kstop
940| Kseq (x_8889, x_8888) ->
941  h_Kseq x_8889 x_8888
942    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
943      h_Kswitch h_Kcall x_8888)
944| Kwhile (x_8892, x_8891, x_8890) ->
945  h_Kwhile x_8892 x_8891 x_8890
946    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
947      h_Kswitch h_Kcall x_8890)
948| Kdowhile (x_8895, x_8894, x_8893) ->
949  h_Kdowhile x_8895 x_8894 x_8893
950    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
951      h_Kswitch h_Kcall x_8893)
952| Kfor2 (x_8899, x_8898, x_8897, x_8896) ->
953  h_Kfor2 x_8899 x_8898 x_8897 x_8896
954    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
955      h_Kswitch h_Kcall x_8896)
956| Kfor3 (x_8903, x_8902, x_8901, x_8900) ->
957  h_Kfor3 x_8903 x_8902 x_8901 x_8900
958    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
959      h_Kswitch h_Kcall x_8900)
960| Kswitch x_8904 ->
961  h_Kswitch x_8904
962    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
963      h_Kswitch h_Kcall x_8904)
964| Kcall (x_8908, x_8907, x_8906, x_8905) ->
965  h_Kcall x_8908 x_8907 x_8906 x_8905
966    (cont_rect_Type0 h_Kstop h_Kseq h_Kwhile h_Kdowhile h_Kfor2 h_Kfor3
967      h_Kswitch h_Kcall x_8905)
968
969(** val cont_inv_rect_Type4 :
970    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
971    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
972    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
973    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
974    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
975    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
976    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
977    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
978    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
979let cont_inv_rect_Type4 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
980  let hcut = cont_rect_Type4 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
981
982(** val cont_inv_rect_Type3 :
983    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
984    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
985    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
986    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
987    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
988    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
989    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
990    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
991    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
992let cont_inv_rect_Type3 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
993  let hcut = cont_rect_Type3 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
994
995(** val cont_inv_rect_Type2 :
996    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
997    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
998    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
999    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1000    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1001    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1002    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1003    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1004    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1005let cont_inv_rect_Type2 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1006  let hcut = cont_rect_Type2 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1007
1008(** val cont_inv_rect_Type1 :
1009    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
1010    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1011    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1012    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1013    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1014    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1015    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1016    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1017    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1018let cont_inv_rect_Type1 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1019  let hcut = cont_rect_Type1 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1020
1021(** val cont_inv_rect_Type0 :
1022    cont -> (__ -> 'a1) -> (Csyntax.statement -> cont -> (__ -> 'a1) -> __ ->
1023    'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) -> __
1024    -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> cont -> (__ -> 'a1) ->
1025    __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement -> Csyntax.statement ->
1026    cont -> (__ -> 'a1) -> __ -> 'a1) -> (Csyntax.expr -> Csyntax.statement
1027    -> Csyntax.statement -> cont -> (__ -> 'a1) -> __ -> 'a1) -> (cont -> (__
1028    -> 'a1) -> __ -> 'a1) -> (((Pointers.block, Pointers.offset) Types.prod,
1029    Csyntax.type0) Types.prod Types.option -> Csyntax.function0 -> env ->
1030    cont -> (__ -> 'a1) -> __ -> 'a1) -> 'a1 **)
1031let cont_inv_rect_Type0 hterm h1 h2 h3 h4 h5 h6 h7 h8 =
1032  let hcut = cont_rect_Type0 h1 h2 h3 h4 h5 h6 h7 h8 hterm in hcut __
1033
1034(** val cont_discr : cont -> cont -> __ **)
1035let cont_discr x y =
1036  Logic.eq_rect_Type2 x
1037    (match x with
1038     | Kstop -> Obj.magic (fun _ dH -> dH)
1039     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1040     | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1041     | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1042     | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1043     | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1044     | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
1045     | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1046
1047(** val cont_jmdiscr : cont -> cont -> __ **)
1048let cont_jmdiscr x y =
1049  Logic.eq_rect_Type2 x
1050    (match x with
1051     | Kstop -> Obj.magic (fun _ dH -> dH)
1052     | Kseq (a0, a1) -> Obj.magic (fun _ dH -> dH __ __)
1053     | Kwhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1054     | Kdowhile (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1055     | Kfor2 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1056     | Kfor3 (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)
1057     | Kswitch a0 -> Obj.magic (fun _ dH -> dH __)
1058     | Kcall (a0, a1, a2, a3) -> Obj.magic (fun _ dH -> dH __ __ __ __)) y
1059
1060(** val call_cont : cont -> cont **)
1061let rec call_cont k = match k with
1062| Kstop -> k
1063| Kseq (s, k0) -> call_cont k0
1064| Kwhile (e, s, k0) -> call_cont k0
1065| Kdowhile (e, s, k0) -> call_cont k0
1066| Kfor2 (e2, e3, s, k0) -> call_cont k0
1067| Kfor3 (e2, e3, s, k0) -> call_cont k0
1068| Kswitch k0 -> call_cont k0
1069| Kcall (x, x0, x1, x2) -> k
1070
1071type state =
1072| State of Csyntax.function0 * Csyntax.statement * cont * env * GenMem.mem
1073| Callstate of AST.ident * Csyntax.clight_fundef * Values.val0 List.list
1074   * cont * GenMem.mem
1075| Returnstate of Values.val0 * cont * GenMem.mem
1076| Finalstate of Integers.int
1077
1078(** val state_rect_Type4 :
1079    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1080    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1081    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1082    -> (Integers.int -> 'a1) -> state -> 'a1 **)
1083let rec state_rect_Type4 h_State h_Callstate h_Returnstate h_Finalstate = function
1084| State (f, s, k, e, m) -> h_State f s k e m
1085| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1086| Returnstate (res, k, m) -> h_Returnstate res k m
1087| Finalstate r -> h_Finalstate r
1088
1089(** val state_rect_Type5 :
1090    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1091    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1092    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1093    -> (Integers.int -> 'a1) -> state -> 'a1 **)
1094let rec state_rect_Type5 h_State h_Callstate h_Returnstate h_Finalstate = function
1095| State (f, s, k, e, m) -> h_State f s k e m
1096| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1097| Returnstate (res, k, m) -> h_Returnstate res k m
1098| Finalstate r -> h_Finalstate r
1099
1100(** val state_rect_Type3 :
1101    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1102    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1103    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1104    -> (Integers.int -> 'a1) -> state -> 'a1 **)
1105let rec state_rect_Type3 h_State h_Callstate h_Returnstate h_Finalstate = function
1106| State (f, s, k, e, m) -> h_State f s k e m
1107| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1108| Returnstate (res, k, m) -> h_Returnstate res k m
1109| Finalstate r -> h_Finalstate r
1110
1111(** val state_rect_Type2 :
1112    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1113    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1114    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1115    -> (Integers.int -> 'a1) -> state -> 'a1 **)
1116let rec state_rect_Type2 h_State h_Callstate h_Returnstate h_Finalstate = function
1117| State (f, s, k, e, m) -> h_State f s k e m
1118| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1119| Returnstate (res, k, m) -> h_Returnstate res k m
1120| Finalstate r -> h_Finalstate r
1121
1122(** val state_rect_Type1 :
1123    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1124    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1125    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1126    -> (Integers.int -> 'a1) -> state -> 'a1 **)
1127let rec state_rect_Type1 h_State h_Callstate h_Returnstate h_Finalstate = function
1128| State (f, s, k, e, m) -> h_State f s k e m
1129| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1130| Returnstate (res, k, m) -> h_Returnstate res k m
1131| Finalstate r -> h_Finalstate r
1132
1133(** val state_rect_Type0 :
1134    (Csyntax.function0 -> Csyntax.statement -> cont -> env -> GenMem.mem ->
1135    'a1) -> (AST.ident -> Csyntax.clight_fundef -> Values.val0 List.list ->
1136    cont -> GenMem.mem -> 'a1) -> (Values.val0 -> cont -> GenMem.mem -> 'a1)
1137    -> (Integers.int -> 'a1) -> state -> 'a1 **)
1138let rec state_rect_Type0 h_State h_Callstate h_Returnstate h_Finalstate = function
1139| State (f, s, k, e, m) -> h_State f s k e m
1140| Callstate (id, fd, args, k, m) -> h_Callstate id fd args k m
1141| Returnstate (res, k, m) -> h_Returnstate res k m
1142| Finalstate r -> h_Finalstate r
1143
1144(** val state_inv_rect_Type4 :
1145    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1146    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1147    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1148    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1149let state_inv_rect_Type4 hterm h1 h2 h3 h4 =
1150  let hcut = state_rect_Type4 h1 h2 h3 h4 hterm in hcut __
1151
1152(** val state_inv_rect_Type3 :
1153    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1154    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1155    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1156    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1157let state_inv_rect_Type3 hterm h1 h2 h3 h4 =
1158  let hcut = state_rect_Type3 h1 h2 h3 h4 hterm in hcut __
1159
1160(** val state_inv_rect_Type2 :
1161    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1162    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1163    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1164    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1165let state_inv_rect_Type2 hterm h1 h2 h3 h4 =
1166  let hcut = state_rect_Type2 h1 h2 h3 h4 hterm in hcut __
1167
1168(** val state_inv_rect_Type1 :
1169    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1170    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1171    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1172    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1173let state_inv_rect_Type1 hterm h1 h2 h3 h4 =
1174  let hcut = state_rect_Type1 h1 h2 h3 h4 hterm in hcut __
1175
1176(** val state_inv_rect_Type0 :
1177    state -> (Csyntax.function0 -> Csyntax.statement -> cont -> env ->
1178    GenMem.mem -> __ -> 'a1) -> (AST.ident -> Csyntax.clight_fundef ->
1179    Values.val0 List.list -> cont -> GenMem.mem -> __ -> 'a1) -> (Values.val0
1180    -> cont -> GenMem.mem -> __ -> 'a1) -> (Integers.int -> __ -> 'a1) -> 'a1 **)
1181let state_inv_rect_Type0 hterm h1 h2 h3 h4 =
1182  let hcut = state_rect_Type0 h1 h2 h3 h4 hterm in hcut __
1183
1184(** val state_discr : state -> state -> __ **)
1185let state_discr x y =
1186  Logic.eq_rect_Type2 x
1187    (match x with
1188     | State (a0, a1, a2, a3, a4) ->
1189       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1190     | Callstate (a0, a1, a2, a3, a4) ->
1191       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1192     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1193     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
1194
1195(** val state_jmdiscr : state -> state -> __ **)
1196let state_jmdiscr x y =
1197  Logic.eq_rect_Type2 x
1198    (match x with
1199     | State (a0, a1, a2, a3, a4) ->
1200       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1201     | Callstate (a0, a1, a2, a3, a4) ->
1202       Obj.magic (fun _ dH -> dH __ __ __ __ __)
1203     | Returnstate (a0, a1, a2) -> Obj.magic (fun _ dH -> dH __ __ __)
1204     | Finalstate a0 -> Obj.magic (fun _ dH -> dH __)) y
1205
1206(** val find_label :
1207    Csyntax.label -> Csyntax.statement -> cont -> (Csyntax.statement, cont)
1208    Types.prod Types.option **)
1209let rec find_label lbl s k =
1210  match s with
1211  | Csyntax.Sskip -> Types.None
1212  | Csyntax.Sassign (x, x0) -> Types.None
1213  | Csyntax.Scall (x, x0, x1) -> Types.None
1214  | Csyntax.Ssequence (s1, s2) ->
1215    (match find_label lbl s1 (Kseq (s2, k)) with
1216     | Types.None -> find_label lbl s2 k
1217     | Types.Some sk -> Types.Some sk)
1218  | Csyntax.Sifthenelse (a, s1, s2) ->
1219    (match find_label lbl s1 k with
1220     | Types.None -> find_label lbl s2 k
1221     | Types.Some sk -> Types.Some sk)
1222  | Csyntax.Swhile (a, s1) -> find_label lbl s1 (Kwhile (a, s1, k))
1223  | Csyntax.Sdowhile (a, s1) -> find_label lbl s1 (Kdowhile (a, s1, k))
1224  | Csyntax.Sfor (a1, a2, a3, s1) ->
1225    (match find_label lbl a1 (Kseq ((Csyntax.Sfor (Csyntax.Sskip, a2, a3,
1226             s1)), k)) with
1227     | Types.None ->
1228       (match find_label lbl s1 (Kfor2 (a2, a3, s1, k)) with
1229        | Types.None -> find_label lbl a3 (Kfor3 (a2, a3, s1, k))
1230        | Types.Some sk -> Types.Some sk)
1231     | Types.Some sk -> Types.Some sk)
1232  | Csyntax.Sbreak -> Types.None
1233  | Csyntax.Scontinue -> Types.None
1234  | Csyntax.Sreturn x -> Types.None
1235  | Csyntax.Sswitch (e, sl) -> find_label_ls lbl sl (Kswitch k)
1236  | Csyntax.Slabel (lbl', s') ->
1237    (match AST.ident_eq lbl lbl' with
1238     | Types.Inl _ -> Types.Some { Types.fst = s'; Types.snd = k }
1239     | Types.Inr _ -> find_label lbl s' k)
1240  | Csyntax.Sgoto x -> Types.None
1241  | Csyntax.Scost (c, s') -> find_label lbl s' k
1242(** val find_label_ls :
1243    Csyntax.label -> Csyntax.labeled_statements -> cont ->
1244    (Csyntax.statement, cont) Types.prod Types.option **)
1245and find_label_ls lbl sl k =
1246  match sl with
1247  | Csyntax.LSdefault s -> find_label lbl s k
1248  | Csyntax.LScase (x, x0, s, sl') ->
1249    (match find_label lbl s (Kseq ((seq_of_labeled_statement sl'), k)) with
1250     | Types.None -> find_label_ls lbl sl' k
1251     | Types.Some sk -> Types.Some sk)
1252
1253(** val fun_typeof : Csyntax.expr -> Csyntax.type0 **)
1254let fun_typeof e =
1255  match Csyntax.typeof e with
1256  | Csyntax.Tvoid -> Csyntax.Tvoid
1257  | Csyntax.Tint (a, b) -> Csyntax.Tint (a, b)
1258  | Csyntax.Tpointer ty -> ty
1259  | Csyntax.Tarray (a, b) -> Csyntax.Tarray (a, b)
1260  | Csyntax.Tfunction (a, b) -> Csyntax.Tfunction (a, b)
1261  | Csyntax.Tstruct (a, b) -> Csyntax.Tstruct (a, b)
1262  | Csyntax.Tunion (a, b) -> Csyntax.Tunion (a, b)
1263  | Csyntax.Tcomp_ptr a -> Csyntax.Tcomp_ptr a
1264
Note: See TracBrowser for help on using the repository browser.