source: extracted/simplifyCasts.ml @ 2968

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

Everything extracted again.

File size: 28.3 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Lists
22
23open Positive
24
25open Identifiers
26
27open Exp
28
29open Arithmetic
30
31open Vector
32
33open Div_and_mod
34
35open Util
36
37open FoldStuff
38
39open BitVector
40
41open Jmeq
42
43open Russell
44
45open List
46
47open Setoids
48
49open Monad
50
51open Option
52
53open Extranat
54
55open Bool
56
57open Relations
58
59open Nat
60
61open Integers
62
63open Hints_declaration
64
65open Core_notation
66
67open Pts
68
69open Logic
70
71open Types
72
73open AST
74
75open Csyntax
76
77open TypeComparison
78
79open ClassifyOp
80
81open Smallstep
82
83open Extra_bool
84
85open FrontEndVal
86
87open Hide
88
89open ByteValues
90
91open GenMem
92
93open FrontEndMem
94
95open Globalenvs
96
97open Csem
98
99open SmallstepExec
100
101open Division
102
103open Z
104
105open BitVectorZ
106
107open Pointers
108
109open Values
110
111open Events
112
113open IOMonad
114
115open IO
116
117open Cexec
118
119open Casts
120
121open CexecInd
122
123open CexecSound
124
125open Sets
126
127open Listb
128
129open Star
130
131open Frontend_misc
132
133(** val reduce_bits :
134    Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
135    BitVector.bitVector Types.option **)
136let rec reduce_bits n m exp v =
137  (match n with
138   | Nat.O -> (fun v0 -> Types.Some v0)
139   | Nat.S n' ->
140     (fun v0 ->
141       match BitVector.eq_b (Vector.head' (Nat.plus n' (Nat.S m)) v0) exp with
142       | Bool.True ->
143         reduce_bits n' m exp (Vector.tail (Nat.plus n' (Nat.S m)) v0)
144       | Bool.False -> Types.None)) v
145
146(** val pred_bitsize_of_intsize : AST.intsize -> Nat.nat **)
147let pred_bitsize_of_intsize sz =
148  Nat.pred (AST.bitsize_of_intsize sz)
149
150(** val signed : AST.signedness -> Bool.bool **)
151let signed = function
152| AST.Signed -> Bool.True
153| AST.Unsigned -> Bool.False
154
155(** val simplify_int :
156    AST.intsize -> AST.intsize -> AST.signedness -> AST.signedness ->
157    AST.bvint -> AST.bvint Types.option **)
158let rec simplify_int sz sz' sg sg' i =
159  let bit =
160    Bool.andb (signed sg)
161      (Vector.head'
162        (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
163          Nat.O)))))))
164          (Nat.times (AST.pred_size_intsize sz) (Nat.S (Nat.S (Nat.S (Nat.S
165            (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) i)
166  in
167  (match Extranat.nat_compare (pred_bitsize_of_intsize sz)
168           (pred_bitsize_of_intsize sz') with
169   | Extranat.Nat_lt (x, x0) -> (fun i0 -> Types.None)
170   | Extranat.Nat_eq x -> (fun i0 -> Types.Some i0)
171   | Extranat.Nat_gt (x, y) ->
172     (fun i0 ->
173       match reduce_bits (Nat.S x) y bit i0 with
174       | Types.None -> Types.None
175       | Types.Some i' ->
176         (match signed sg' with
177          | Bool.True ->
178            (match BitVector.eq_b bit (Vector.head' y i') with
179             | Bool.True -> Types.Some i'
180             | Bool.False -> Types.None)
181          | Bool.False -> Types.Some i'))) i
182
183(** val size_lt_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum **)
184let size_lt_dec = function
185| AST.I8 ->
186  (fun clearme0 ->
187    match clearme0 with
188    | AST.I8 -> Types.Inr __
189    | AST.I16 -> Types.Inl __
190    | AST.I32 -> Types.Inl __)
191| AST.I16 ->
192  (fun clearme0 ->
193    match clearme0 with
194    | AST.I8 -> Types.Inr __
195    | AST.I16 -> Types.Inr __
196    | AST.I32 -> Types.Inl __)
197| AST.I32 ->
198  (fun clearme0 ->
199    match clearme0 with
200    | AST.I8 -> Types.Inr __
201    | AST.I16 -> Types.Inr __
202    | AST.I32 -> Types.Inr __)
203
204(** val size_not_lt_to_ge :
205    AST.intsize -> AST.intsize -> (__, __) Types.sum **)
206let size_not_lt_to_ge clearme sz2 =
207  (match clearme with
208   | AST.I8 ->
209     (fun clearme0 ->
210       match clearme0 with
211       | AST.I8 -> (fun _ -> Types.Inl __)
212       | AST.I16 -> (fun _ -> Types.Inr __)
213       | AST.I32 -> (fun _ -> Types.Inr __))
214   | AST.I16 ->
215     (fun clearme0 ->
216       match clearme0 with
217       | AST.I8 -> (fun _ -> Types.Inr __)
218       | AST.I16 -> (fun _ -> Types.Inl __)
219       | AST.I32 -> (fun _ -> Types.Inr __))
220   | AST.I32 ->
221     (fun clearme0 ->
222       match clearme0 with
223       | AST.I8 -> (fun _ -> Types.Inr __)
224       | AST.I16 -> (fun _ -> Types.Inr __)
225       | AST.I32 -> (fun _ -> Types.Inl __))) sz2 __
226
227(** val sign_eq_dect :
228    AST.signedness -> AST.signedness -> (__, __) Types.sum **)
229let sign_eq_dect = function
230| AST.Signed ->
231  (fun clearme0 ->
232    match clearme0 with
233    | AST.Signed -> TypeComparison.sg_eq_dec AST.Signed AST.Signed
234    | AST.Unsigned -> TypeComparison.sg_eq_dec AST.Signed AST.Unsigned)
235| AST.Unsigned ->
236  (fun clearme0 ->
237    match clearme0 with
238    | AST.Signed -> TypeComparison.sg_eq_dec AST.Unsigned AST.Signed
239    | AST.Unsigned -> TypeComparison.sg_eq_dec AST.Unsigned AST.Unsigned)
240
241(** val necessary_conditions :
242    AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness ->
243    Bool.bool **)
244let necessary_conditions src_sz src_sg target_sz target_sg =
245  match size_lt_dec target_sz src_sz with
246  | Types.Inl _ -> Bool.True
247  | Types.Inr _ ->
248    (match TypeComparison.sz_eq_dec target_sz src_sz with
249     | Types.Inl _ ->
250       (match sign_eq_dect src_sg target_sg with
251        | Types.Inl _ -> Bool.False
252        | Types.Inr _ -> Bool.True)
253     | Types.Inr _ -> Bool.False)
254
255(** val assert_int_value :
256    Values.val0 Types.option -> AST.intsize -> BitVector.bitVector
257    Types.option **)
258let rec assert_int_value v expected_size =
259  match v with
260  | Types.None -> Types.None
261  | Types.Some v0 ->
262    (match v0 with
263     | Values.Vundef -> Types.None
264     | Values.Vint (sz, i) ->
265       (match TypeComparison.sz_eq_dec sz expected_size with
266        | Types.Inl _ ->
267          Types.Some
268            (Extralib.eq_rect_Type0_r expected_size (fun i0 -> i0) sz i)
269        | Types.Inr _ -> Types.None)
270     | Values.Vnull -> Types.None
271     | Values.Vptr x -> Types.None)
272
273(** val binop_simplifiable : Csyntax.binary_operation -> Bool.bool **)
274let binop_simplifiable = function
275| Csyntax.Oadd -> Bool.True
276| Csyntax.Osub -> Bool.True
277| Csyntax.Omul -> Bool.False
278| Csyntax.Odiv -> Bool.False
279| Csyntax.Omod -> Bool.False
280| Csyntax.Oand -> Bool.False
281| Csyntax.Oor -> Bool.False
282| Csyntax.Oxor -> Bool.False
283| Csyntax.Oshl -> Bool.False
284| Csyntax.Oshr -> Bool.False
285| Csyntax.Oeq -> Bool.False
286| Csyntax.One -> Bool.False
287| Csyntax.Olt -> Bool.False
288| Csyntax.Ogt -> Bool.False
289| Csyntax.Ole -> Bool.False
290| Csyntax.Oge -> Bool.False
291
292(** val simplify_expr :
293    Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool,
294    Csyntax.expr) Types.prod Types.sig0 **)
295let rec simplify_expr e target_sz target_sg =
296  (let Csyntax.Expr (ed, ty) = e in
297  (fun _ ->
298  (match ed with
299   | Csyntax.Econst_int (cst_sz, i) ->
300     (fun _ ->
301       (match ty with
302        | Csyntax.Tvoid ->
303          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
304        | Csyntax.Tint (ty_sz, sg) ->
305          (fun _ ->
306            match TypeComparison.sz_eq_dec cst_sz ty_sz with
307            | Types.Inl _ ->
308              (match TypeComparison.type_eq_dec ty (Csyntax.Tint (target_sz,
309                       target_sg)) with
310               | Types.Inl _ -> { Types.fst = Bool.True; Types.snd = e }
311               | Types.Inr _ ->
312                 (match simplify_int cst_sz target_sz sg target_sg i with
313                  | Types.None ->
314                    (fun _ -> { Types.fst = Bool.False; Types.snd = e })
315                  | Types.Some i' ->
316                    (fun _ -> { Types.fst = Bool.True; Types.snd =
317                      (Csyntax.Expr ((Csyntax.Econst_int (target_sz, i')),
318                      (Csyntax.Tint (target_sz, target_sg)))) })) __)
319            | Types.Inr _ -> { Types.fst = Bool.False; Types.snd = e })
320        | Csyntax.Tpointer x ->
321          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
322        | Csyntax.Tarray (x, x0) ->
323          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
324        | Csyntax.Tfunction (x, x0) ->
325          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
326        | Csyntax.Tstruct (x, x0) ->
327          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
328        | Csyntax.Tunion (x, x0) ->
329          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
330        | Csyntax.Tcomp_ptr x ->
331          (fun _ -> { Types.fst = Bool.False; Types.snd = e })) __)
332   | Csyntax.Evar id ->
333     (fun _ -> { Types.fst =
334       (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg)));
335       Types.snd = (Csyntax.Expr (ed, ty)) })
336   | Csyntax.Ederef e1 ->
337     (fun _ ->
338       (let e2 = simplify_inside e1 in
339         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
340         ((Csyntax.Ederef e2), ty)) })) __)
341   | Csyntax.Eaddrof e1 ->
342     (fun _ ->
343       (let e2 = simplify_inside e1 in
344         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
345         ((Csyntax.Eaddrof e2), ty)) })) __)
346   | Csyntax.Eunop (op, e1) ->
347     (fun _ ->
348       (let e2 = simplify_inside e1 in
349         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
350         ((Csyntax.Eunop (op, e2)), ty)) })) __)
351   | Csyntax.Ebinop (op, lhs, rhs) ->
352     (fun _ ->
353       (match binop_simplifiable op with
354        | Bool.True ->
355          (fun _ ->
356            match TypeComparison.assert_type_eq ty (Csyntax.typeof lhs) with
357            | Errors.OK _ ->
358              (match TypeComparison.assert_type_eq (Csyntax.typeof lhs)
359                       (Csyntax.typeof rhs) with
360               | Errors.OK _ ->
361                 (let eta2089 = simplify_expr lhs target_sz target_sg in
362                   (fun _ ->
363                   (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
364                      eta2089
365                    in
366                   (fun _ ->
367                   (let eta2088 = simplify_expr rhs target_sz target_sg in
368                     (fun _ ->
369                     (let { Types.fst = desired_type_rhs; Types.snd =
370                        rhs1 } = eta2088
371                      in
372                     (fun _ ->
373                     (match Bool.andb desired_type_lhs desired_type_rhs with
374                      | Bool.True ->
375                        (fun _ -> { Types.fst = Bool.True; Types.snd =
376                          (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)),
377                          (Csyntax.Tint (target_sz, target_sg)))) })
378                      | Bool.False ->
379                        (fun _ ->
380                          (let lhs10 = simplify_inside lhs in
381                            (fun _ ->
382                            (let rhs10 = simplify_inside rhs in
383                              (fun _ -> { Types.fst = Bool.False; Types.snd =
384                              (Csyntax.Expr ((Csyntax.Ebinop (op, lhs10,
385                              rhs10)), ty)) })) __)) __)) __)) __)) __)) __))
386                   __
387               | Errors.Error x ->
388                 (let lhs1 = simplify_inside lhs in
389                   (fun _ ->
390                   (let rhs1 = simplify_inside rhs in
391                     (fun _ -> { Types.fst = Bool.False; Types.snd =
392                     (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)),
393                     ty)) })) __)) __)
394            | Errors.Error x ->
395              (let lhs1 = simplify_inside lhs in
396                (fun _ ->
397                (let rhs1 = simplify_inside rhs in
398                  (fun _ -> { Types.fst = Bool.False; Types.snd =
399                  (Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)) }))
400                  __)) __)
401        | Bool.False ->
402          (fun _ ->
403            (let lhs1 = simplify_inside lhs in
404              (fun _ ->
405              (let rhs1 = simplify_inside rhs in
406                (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
407                ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)) })) __)) __)) __)
408   | Csyntax.Ecast (cast_ty, castee) ->
409     (fun _ ->
410       (match cast_ty with
411        | Csyntax.Tvoid ->
412          (fun _ ->
413            (let castee1 = simplify_inside castee in
414              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
415              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
416        | Csyntax.Tint (cast_sz, cast_sg) ->
417          (fun _ ->
418            match TypeComparison.type_eq_dec ty cast_ty with
419            | Types.Inl _ ->
420              (match necessary_conditions cast_sz cast_sg target_sz target_sg with
421               | Bool.True ->
422                 (fun _ ->
423                   (let eta2091 = simplify_expr castee target_sz target_sg in
424                     (fun _ ->
425                     (let { Types.fst = desired_type; Types.snd = castee1 } =
426                        eta2091
427                      in
428                     (fun _ ->
429                     (match desired_type with
430                      | Bool.True ->
431                        (fun _ -> { Types.fst = Bool.True; Types.snd =
432                          castee1 })
433                      | Bool.False ->
434                        (fun _ ->
435                          (let eta2090 = simplify_expr castee cast_sz cast_sg
436                           in
437                            (fun _ ->
438                            (let { Types.fst = desired_type2; Types.snd =
439                               castee2 } = eta2090
440                             in
441                            (fun _ ->
442                            (match desired_type2 with
443                             | Bool.True ->
444                               (fun _ -> { Types.fst = Bool.False;
445                                 Types.snd = castee2 })
446                             | Bool.False ->
447                               (fun _ -> { Types.fst = Bool.False;
448                                 Types.snd = (Csyntax.Expr ((Csyntax.Ecast
449                                 (ty, castee2)), cast_ty)) })) __)) __)) __))
450                       __)) __)) __)
451               | Bool.False ->
452                 (fun _ ->
453                   (let eta2092 = simplify_expr castee cast_sz cast_sg in
454                     (fun _ ->
455                     (let { Types.fst = desired_type2; Types.snd =
456                        castee2 } = eta2092
457                      in
458                     (fun _ ->
459                     (match desired_type2 with
460                      | Bool.True ->
461                        (fun _ -> { Types.fst = Bool.False; Types.snd =
462                          castee2 })
463                      | Bool.False ->
464                        (fun _ -> { Types.fst = Bool.False; Types.snd =
465                          (Csyntax.Expr ((Csyntax.Ecast (ty, castee2)),
466                          cast_ty)) })) __)) __)) __)) __
467            | Types.Inr _ ->
468              (let castee1 = simplify_inside castee in
469                (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
470                ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
471        | Csyntax.Tpointer x ->
472          (fun _ ->
473            (let castee1 = simplify_inside castee in
474              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
475              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
476        | Csyntax.Tarray (x, x0) ->
477          (fun _ ->
478            (let castee1 = simplify_inside castee in
479              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
480              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
481        | Csyntax.Tfunction (x, x0) ->
482          (fun _ ->
483            (let castee1 = simplify_inside castee in
484              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
485              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
486        | Csyntax.Tstruct (x, x0) ->
487          (fun _ ->
488            (let castee1 = simplify_inside castee in
489              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
490              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
491        | Csyntax.Tunion (x, x0) ->
492          (fun _ ->
493            (let castee1 = simplify_inside castee in
494              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
495              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
496        | Csyntax.Tcomp_ptr x ->
497          (fun _ ->
498            (let castee1 = simplify_inside castee in
499              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
500              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)) __)
501   | Csyntax.Econdition (cond, iftrue, iffalse) ->
502     (fun _ ->
503       (let cond1 = simplify_inside cond in
504         (fun _ ->
505         match TypeComparison.assert_type_eq ty (Csyntax.typeof iftrue) with
506         | Errors.OK _ ->
507           (match TypeComparison.assert_type_eq (Csyntax.typeof iftrue)
508                    (Csyntax.typeof iffalse) with
509            | Errors.OK _ ->
510              (let eta2094 = simplify_expr iftrue target_sz target_sg in
511                (fun _ ->
512                (let { Types.fst = desired_true; Types.snd = iftrue1 } =
513                   eta2094
514                 in
515                (fun _ ->
516                (let eta2093 = simplify_expr iffalse target_sz target_sg in
517                  (fun _ ->
518                  (let { Types.fst = desired_false; Types.snd = iffalse1 } =
519                     eta2093
520                   in
521                  (fun _ ->
522                  (match Bool.andb desired_true desired_false with
523                   | Bool.True ->
524                     (fun _ -> { Types.fst = Bool.True; Types.snd =
525                       (Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
526                       iffalse1)), (Csyntax.Tint (target_sz, target_sg)))) })
527                   | Bool.False ->
528                     (fun _ ->
529                       (let iftrue10 = simplify_inside iftrue in
530                         (fun _ ->
531                         (let iffalse10 = simplify_inside iffalse in
532                           (fun _ -> { Types.fst = Bool.False; Types.snd =
533                           (Csyntax.Expr ((Csyntax.Econdition (cond1,
534                           iftrue10, iffalse10)), ty)) })) __)) __)) __)) __))
535                  __)) __)) __
536            | Errors.Error x ->
537              (let iftrue1 = simplify_inside iftrue in
538                (fun _ ->
539                (let iffalse1 = simplify_inside iffalse in
540                  (fun _ -> { Types.fst = Bool.False; Types.snd =
541                  (Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
542                  iffalse1)), ty)) })) __)) __)
543         | Errors.Error x ->
544           (let iftrue1 = simplify_inside iftrue in
545             (fun _ ->
546             (let iffalse1 = simplify_inside iffalse in
547               (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
548               ((Csyntax.Econdition (cond1, iftrue1, iffalse1)), ty)) })) __))
549             __)) __)
550   | Csyntax.Eandbool (lhs, rhs) ->
551     (fun _ ->
552       (let lhs1 = simplify_inside lhs in
553         (fun _ ->
554         (let rhs1 = simplify_inside rhs in
555           (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
556           ((Csyntax.Eandbool (lhs1, rhs1)), ty)) })) __)) __)
557   | Csyntax.Eorbool (lhs, rhs) ->
558     (fun _ ->
559       (let lhs1 = simplify_inside lhs in
560         (fun _ ->
561         (let rhs1 = simplify_inside rhs in
562           (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
563           ((Csyntax.Eorbool (lhs1, rhs1)), ty)) })) __)) __)
564   | Csyntax.Esizeof t ->
565     (fun _ -> { Types.fst =
566       (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg)));
567       Types.snd = (Csyntax.Expr (ed, ty)) })
568   | Csyntax.Efield (rec_expr, f) ->
569     (fun _ ->
570       (let rec_expr1 = simplify_inside rec_expr in
571         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
572         ((Csyntax.Efield (rec_expr1, f)), ty)) })) __)
573   | Csyntax.Ecost (l, e1) ->
574     (fun _ ->
575       match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with
576       | Types.Inl _ ->
577         (let eta2095 = simplify_expr e1 target_sz target_sg in
578           (fun _ ->
579           (let { Types.fst = desired_type; Types.snd = e2 } = eta2095 in
580           (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
581           ((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __
582       | Types.Inr _ ->
583         (let e2 = simplify_inside e1 in
584           (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
585           ((Csyntax.Ecost (l, e2)), ty)) })) __)) __)) __
586(** val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0 **)
587and simplify_inside e =
588  (let Csyntax.Expr (ed, ty) = e in
589  (fun _ ->
590  (match ed with
591   | Csyntax.Econst_int (x, x0) -> (fun _ -> e)
592   | Csyntax.Evar x -> (fun _ -> e)
593   | Csyntax.Ederef e1 ->
594     (fun _ ->
595       (let e2 = simplify_inside e1 in
596         (fun _ -> Csyntax.Expr ((Csyntax.Ederef e2), ty))) __)
597   | Csyntax.Eaddrof e1 ->
598     (fun _ ->
599       (let e2 = simplify_inside e1 in
600         (fun _ -> Csyntax.Expr ((Csyntax.Eaddrof e2), ty))) __)
601   | Csyntax.Eunop (op, e1) ->
602     (fun _ ->
603       (let e2 = simplify_inside e1 in
604         (fun _ -> Csyntax.Expr ((Csyntax.Eunop (op, e2)), ty))) __)
605   | Csyntax.Ebinop (op, lhs, rhs) ->
606     (fun _ ->
607       (let lhs1 = simplify_inside lhs in
608         (fun _ ->
609         (let rhs1 = simplify_inside rhs in
610           (fun _ -> Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)))
611           __)) __)
612   | Csyntax.Ecast (cast_ty, castee) ->
613     (fun _ ->
614       match TypeComparison.type_eq_dec ty cast_ty with
615       | Types.Inl _ ->
616         (match cast_ty with
617          | Csyntax.Tvoid -> (fun _ -> e)
618          | Csyntax.Tint (cast_sz, cast_sg) ->
619            (fun _ ->
620              (let eta2096 = simplify_expr castee cast_sz cast_sg in
621                (fun _ ->
622                (let { Types.fst = success; Types.snd = castee1 } = eta2096
623                 in
624                (fun _ ->
625                (match success with
626                 | Bool.True -> (fun _ -> castee1)
627                 | Bool.False ->
628                   (fun _ -> Csyntax.Expr ((Csyntax.Ecast (cast_ty,
629                     castee1)), ty))) __)) __)) __)
630          | Csyntax.Tpointer x -> (fun _ -> e)
631          | Csyntax.Tarray (x, x0) -> (fun _ -> e)
632          | Csyntax.Tfunction (x, x0) -> (fun _ -> e)
633          | Csyntax.Tstruct (x, x0) -> (fun _ -> e)
634          | Csyntax.Tunion (x, x0) -> (fun _ -> e)
635          | Csyntax.Tcomp_ptr x -> (fun _ -> e)) __
636       | Types.Inr _ -> e)
637   | Csyntax.Econdition (cond, iftrue, iffalse) ->
638     (fun _ ->
639       (let cond1 = simplify_inside cond in
640         (fun _ ->
641         (let iftrue1 = simplify_inside iftrue in
642           (fun _ ->
643           (let iffalse1 = simplify_inside iffalse in
644             (fun _ -> Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
645             iffalse1)), ty))) __)) __)) __)
646   | Csyntax.Eandbool (lhs, rhs) ->
647     (fun _ ->
648       (let lhs1 = simplify_inside lhs in
649         (fun _ ->
650         (let rhs1 = simplify_inside rhs in
651           (fun _ -> Csyntax.Expr ((Csyntax.Eandbool (lhs1, rhs1)), ty))) __))
652         __)
653   | Csyntax.Eorbool (lhs, rhs) ->
654     (fun _ ->
655       (let lhs1 = simplify_inside lhs in
656         (fun _ ->
657         (let rhs1 = simplify_inside rhs in
658           (fun _ -> Csyntax.Expr ((Csyntax.Eorbool (lhs1, rhs1)), ty))) __))
659         __)
660   | Csyntax.Esizeof x -> (fun _ -> e)
661   | Csyntax.Efield (rec_expr, f) ->
662     (fun _ ->
663       (let rec_expr1 = simplify_inside rec_expr in
664         (fun _ -> Csyntax.Expr ((Csyntax.Efield (rec_expr1, f)), ty))) __)
665   | Csyntax.Ecost (l, e1) ->
666     (fun _ ->
667       (let e2 = simplify_inside e1 in
668         (fun _ -> Csyntax.Expr ((Csyntax.Ecost (l, e2)), ty))) __)) __)) __
669
670(** val simplify_e : Csyntax.expr -> Csyntax.expr **)
671let simplify_e e =
672  Types.pi1 (simplify_inside e)
673
674(** val simplify_statement : Csyntax.statement -> Csyntax.statement **)
675let rec simplify_statement = function
676| Csyntax.Sskip -> Csyntax.Sskip
677| Csyntax.Sassign (e1, e2) ->
678  Csyntax.Sassign ((simplify_e e1), (simplify_e e2))
679| Csyntax.Scall (eo, e, es) ->
680  Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e),
681    (List.map simplify_e es))
682| Csyntax.Ssequence (s1, s2) ->
683  Csyntax.Ssequence ((simplify_statement s1), (simplify_statement s2))
684| Csyntax.Sifthenelse (e, s1, s2) ->
685  Csyntax.Sifthenelse ((simplify_e e), (simplify_statement s1),
686    (simplify_statement s2))
687| Csyntax.Swhile (e, s1) ->
688  Csyntax.Swhile ((simplify_e e), (simplify_statement s1))
689| Csyntax.Sdowhile (e, s1) ->
690  Csyntax.Sdowhile ((simplify_e e), (simplify_statement s1))
691| Csyntax.Sfor (s1, e, s2, s3) ->
692  Csyntax.Sfor ((simplify_statement s1), (simplify_e e),
693    (simplify_statement s2), (simplify_statement s3))
694| Csyntax.Sbreak -> Csyntax.Sbreak
695| Csyntax.Scontinue -> Csyntax.Scontinue
696| Csyntax.Sreturn eo -> Csyntax.Sreturn (Types.option_map simplify_e eo)
697| Csyntax.Sswitch (e, ls) ->
698  Csyntax.Sswitch ((simplify_e e), (simplify_ls ls))
699| Csyntax.Slabel (l, s1) -> Csyntax.Slabel (l, (simplify_statement s1))
700| Csyntax.Sgoto l -> Csyntax.Sgoto l
701| Csyntax.Scost (l, s1) -> Csyntax.Scost (l, (simplify_statement s1))
702(** val simplify_ls :
703    Csyntax.labeled_statements -> Csyntax.labeled_statements **)
704and simplify_ls = function
705| Csyntax.LSdefault s -> Csyntax.LSdefault (simplify_statement s)
706| Csyntax.LScase (sz, i, s, ls') ->
707  Csyntax.LScase (sz, i, (simplify_statement s), (simplify_ls ls'))
708
709(** val simplify_function : Csyntax.function0 -> Csyntax.function0 **)
710let simplify_function f =
711  { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
712    f.Csyntax.fn_params; Csyntax.fn_vars = f.Csyntax.fn_vars;
713    Csyntax.fn_body = (simplify_statement f.Csyntax.fn_body) }
714
715(** val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef **)
716let simplify_fundef f = match f with
717| Csyntax.CL_Internal f0 -> Csyntax.CL_Internal (simplify_function f0)
718| Csyntax.CL_External (x, x0, x1) -> f
719
720(** val simplify_program :
721    Csyntax.clight_program -> Csyntax.clight_program **)
722let simplify_program p =
723  AST.transform_program p (fun x -> simplify_fundef)
724
725(** val related_globals_rect_Type4 :
726    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
727    __ -> __ -> 'a2) -> 'a2 **)
728let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
729  h_mk_related_globals __ __ __
730
731(** val related_globals_rect_Type5 :
732    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
733    __ -> __ -> 'a2) -> 'a2 **)
734let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
735  h_mk_related_globals __ __ __
736
737(** val related_globals_rect_Type3 :
738    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
739    __ -> __ -> 'a2) -> 'a2 **)
740let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
741  h_mk_related_globals __ __ __
742
743(** val related_globals_rect_Type2 :
744    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
745    __ -> __ -> 'a2) -> 'a2 **)
746let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
747  h_mk_related_globals __ __ __
748
749(** val related_globals_rect_Type1 :
750    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
751    __ -> __ -> 'a2) -> 'a2 **)
752let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
753  h_mk_related_globals __ __ __
754
755(** val related_globals_rect_Type0 :
756    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
757    __ -> __ -> 'a2) -> 'a2 **)
758let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
759  h_mk_related_globals __ __ __
760
761(** val related_globals_inv_rect_Type4 :
762    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
763    __ -> __ -> __ -> 'a2) -> 'a2 **)
764let related_globals_inv_rect_Type4 x2 x3 x4 h1 =
765  let hcut = related_globals_rect_Type4 x2 x3 x4 h1 in hcut __
766
767(** val related_globals_inv_rect_Type3 :
768    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
769    __ -> __ -> __ -> 'a2) -> 'a2 **)
770let related_globals_inv_rect_Type3 x2 x3 x4 h1 =
771  let hcut = related_globals_rect_Type3 x2 x3 x4 h1 in hcut __
772
773(** val related_globals_inv_rect_Type2 :
774    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
775    __ -> __ -> __ -> 'a2) -> 'a2 **)
776let related_globals_inv_rect_Type2 x2 x3 x4 h1 =
777  let hcut = related_globals_rect_Type2 x2 x3 x4 h1 in hcut __
778
779(** val related_globals_inv_rect_Type1 :
780    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
781    __ -> __ -> __ -> 'a2) -> 'a2 **)
782let related_globals_inv_rect_Type1 x2 x3 x4 h1 =
783  let hcut = related_globals_rect_Type1 x2 x3 x4 h1 in hcut __
784
785(** val related_globals_inv_rect_Type0 :
786    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
787    __ -> __ -> __ -> 'a2) -> 'a2 **)
788let related_globals_inv_rect_Type0 x2 x3 x4 h1 =
789  let hcut = related_globals_rect_Type0 x2 x3 x4 h1 in hcut __
790
791(** val related_globals_discr :
792    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
793let related_globals_discr a2 a3 a4 =
794  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
795
796(** val related_globals_jmdiscr :
797    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
798let related_globals_jmdiscr a2 a3 a4 =
799  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
800
Note: See TracBrowser for help on using the repository browser.