source: extracted/simplifyCasts.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
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 eta865 = simplify_expr lhs target_sz target_sg in
362                   (fun _ ->
363                   (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
364                      eta865
365                    in
366                   (fun _ ->
367                   (let eta864 = simplify_expr rhs target_sz target_sg in
368                     (fun _ ->
369                     (let { Types.fst = desired_type_rhs; Types.snd =
370                        rhs1 } = eta864
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 eta867 = simplify_expr castee target_sz target_sg in
424                     (fun _ ->
425                     (let { Types.fst = desired_type; Types.snd = castee1 } =
426                        eta867
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 eta866 = simplify_expr castee cast_sz cast_sg
436                           in
437                            (fun _ ->
438                            (let { Types.fst = desired_type2; Types.snd =
439                               castee2 } = eta866
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 eta868 = simplify_expr castee cast_sz cast_sg in
454                     (fun _ ->
455                     (let { Types.fst = desired_type2; Types.snd =
456                        castee2 } = eta868
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 eta870 = simplify_expr iftrue target_sz target_sg in
511                (fun _ ->
512                (let { Types.fst = desired_true; Types.snd = iftrue1 } =
513                   eta870
514                 in
515                (fun _ ->
516                (let eta869 = simplify_expr iffalse target_sz target_sg in
517                  (fun _ ->
518                  (let { Types.fst = desired_false; Types.snd = iffalse1 } =
519                     eta869
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 eta871 = simplify_expr e1 target_sz target_sg in
578           (fun _ ->
579           (let { Types.fst = desired_type; Types.snd = e2 } = eta871 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 eta872 = simplify_expr castee cast_sz cast_sg in
621                (fun _ ->
622                (let { Types.fst = success; Types.snd = castee1 } = eta872 in
623                (fun _ ->
624                (match success with
625                 | Bool.True -> (fun _ -> castee1)
626                 | Bool.False ->
627                   (fun _ -> Csyntax.Expr ((Csyntax.Ecast (cast_ty,
628                     castee1)), ty))) __)) __)) __)
629          | Csyntax.Tpointer x -> (fun _ -> e)
630          | Csyntax.Tarray (x, x0) -> (fun _ -> e)
631          | Csyntax.Tfunction (x, x0) -> (fun _ -> e)
632          | Csyntax.Tstruct (x, x0) -> (fun _ -> e)
633          | Csyntax.Tunion (x, x0) -> (fun _ -> e)
634          | Csyntax.Tcomp_ptr x -> (fun _ -> e)) __
635       | Types.Inr _ -> e)
636   | Csyntax.Econdition (cond, iftrue, iffalse) ->
637     (fun _ ->
638       (let cond1 = simplify_inside cond in
639         (fun _ ->
640         (let iftrue1 = simplify_inside iftrue in
641           (fun _ ->
642           (let iffalse1 = simplify_inside iffalse in
643             (fun _ -> Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
644             iffalse1)), ty))) __)) __)) __)
645   | Csyntax.Eandbool (lhs, rhs) ->
646     (fun _ ->
647       (let lhs1 = simplify_inside lhs in
648         (fun _ ->
649         (let rhs1 = simplify_inside rhs in
650           (fun _ -> Csyntax.Expr ((Csyntax.Eandbool (lhs1, rhs1)), ty))) __))
651         __)
652   | Csyntax.Eorbool (lhs, rhs) ->
653     (fun _ ->
654       (let lhs1 = simplify_inside lhs in
655         (fun _ ->
656         (let rhs1 = simplify_inside rhs in
657           (fun _ -> Csyntax.Expr ((Csyntax.Eorbool (lhs1, rhs1)), ty))) __))
658         __)
659   | Csyntax.Esizeof x -> (fun _ -> e)
660   | Csyntax.Efield (rec_expr, f) ->
661     (fun _ ->
662       (let rec_expr1 = simplify_inside rec_expr in
663         (fun _ -> Csyntax.Expr ((Csyntax.Efield (rec_expr1, f)), ty))) __)
664   | Csyntax.Ecost (l, e1) ->
665     (fun _ ->
666       (let e2 = simplify_inside e1 in
667         (fun _ -> Csyntax.Expr ((Csyntax.Ecost (l, e2)), ty))) __)) __)) __
668
669(** val simplify_e : Csyntax.expr -> Csyntax.expr **)
670let simplify_e e =
671  Types.pi1 (simplify_inside e)
672
673(** val simplify_statement : Csyntax.statement -> Csyntax.statement **)
674let rec simplify_statement = function
675| Csyntax.Sskip -> Csyntax.Sskip
676| Csyntax.Sassign (e1, e2) ->
677  Csyntax.Sassign ((simplify_e e1), (simplify_e e2))
678| Csyntax.Scall (eo, e, es) ->
679  Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e),
680    (List.map simplify_e es))
681| Csyntax.Ssequence (s1, s2) ->
682  Csyntax.Ssequence ((simplify_statement s1), (simplify_statement s2))
683| Csyntax.Sifthenelse (e, s1, s2) ->
684  Csyntax.Sifthenelse ((simplify_e e), (simplify_statement s1),
685    (simplify_statement s2))
686| Csyntax.Swhile (e, s1) ->
687  Csyntax.Swhile ((simplify_e e), (simplify_statement s1))
688| Csyntax.Sdowhile (e, s1) ->
689  Csyntax.Sdowhile ((simplify_e e), (simplify_statement s1))
690| Csyntax.Sfor (s1, e, s2, s3) ->
691  Csyntax.Sfor ((simplify_statement s1), (simplify_e e),
692    (simplify_statement s2), (simplify_statement s3))
693| Csyntax.Sbreak -> Csyntax.Sbreak
694| Csyntax.Scontinue -> Csyntax.Scontinue
695| Csyntax.Sreturn eo -> Csyntax.Sreturn (Types.option_map simplify_e eo)
696| Csyntax.Sswitch (e, ls) ->
697  Csyntax.Sswitch ((simplify_e e), (simplify_ls ls))
698| Csyntax.Slabel (l, s1) -> Csyntax.Slabel (l, (simplify_statement s1))
699| Csyntax.Sgoto l -> Csyntax.Sgoto l
700| Csyntax.Scost (l, s1) -> Csyntax.Scost (l, (simplify_statement s1))
701(** val simplify_ls :
702    Csyntax.labeled_statements -> Csyntax.labeled_statements **)
703and simplify_ls = function
704| Csyntax.LSdefault s -> Csyntax.LSdefault (simplify_statement s)
705| Csyntax.LScase (sz, i, s, ls') ->
706  Csyntax.LScase (sz, i, (simplify_statement s), (simplify_ls ls'))
707
708(** val simplify_function : Csyntax.function0 -> Csyntax.function0 **)
709let simplify_function f =
710  { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
711    f.Csyntax.fn_params; Csyntax.fn_vars = f.Csyntax.fn_vars;
712    Csyntax.fn_body = (simplify_statement f.Csyntax.fn_body) }
713
714(** val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef **)
715let simplify_fundef f = match f with
716| Csyntax.CL_Internal f0 -> Csyntax.CL_Internal (simplify_function f0)
717| Csyntax.CL_External (x, x0, x1) -> f
718
719(** val simplify_program :
720    Csyntax.clight_program -> Csyntax.clight_program **)
721let simplify_program p =
722  AST.transform_program p (fun x -> simplify_fundef)
723
724(** val related_globals_rect_Type4 :
725    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
726    __ -> __ -> 'a2) -> 'a2 **)
727let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
728  h_mk_related_globals __ __ __
729
730(** val related_globals_rect_Type5 :
731    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
732    __ -> __ -> 'a2) -> 'a2 **)
733let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
734  h_mk_related_globals __ __ __
735
736(** val related_globals_rect_Type3 :
737    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
738    __ -> __ -> 'a2) -> 'a2 **)
739let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
740  h_mk_related_globals __ __ __
741
742(** val related_globals_rect_Type2 :
743    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
744    __ -> __ -> 'a2) -> 'a2 **)
745let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
746  h_mk_related_globals __ __ __
747
748(** val related_globals_rect_Type1 :
749    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
750    __ -> __ -> 'a2) -> 'a2 **)
751let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
752  h_mk_related_globals __ __ __
753
754(** val related_globals_rect_Type0 :
755    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
756    __ -> __ -> 'a2) -> 'a2 **)
757let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
758  h_mk_related_globals __ __ __
759
760(** val related_globals_inv_rect_Type4 :
761    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
762    __ -> __ -> __ -> 'a2) -> 'a2 **)
763let related_globals_inv_rect_Type4 x2 x3 x4 h1 =
764  let hcut = related_globals_rect_Type4 x2 x3 x4 h1 in hcut __
765
766(** val related_globals_inv_rect_Type3 :
767    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
768    __ -> __ -> __ -> 'a2) -> 'a2 **)
769let related_globals_inv_rect_Type3 x2 x3 x4 h1 =
770  let hcut = related_globals_rect_Type3 x2 x3 x4 h1 in hcut __
771
772(** val related_globals_inv_rect_Type2 :
773    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
774    __ -> __ -> __ -> 'a2) -> 'a2 **)
775let related_globals_inv_rect_Type2 x2 x3 x4 h1 =
776  let hcut = related_globals_rect_Type2 x2 x3 x4 h1 in hcut __
777
778(** val related_globals_inv_rect_Type1 :
779    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
780    __ -> __ -> __ -> 'a2) -> 'a2 **)
781let related_globals_inv_rect_Type1 x2 x3 x4 h1 =
782  let hcut = related_globals_rect_Type1 x2 x3 x4 h1 in hcut __
783
784(** val related_globals_inv_rect_Type0 :
785    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
786    __ -> __ -> __ -> 'a2) -> 'a2 **)
787let related_globals_inv_rect_Type0 x2 x3 x4 h1 =
788  let hcut = related_globals_rect_Type0 x2 x3 x4 h1 in hcut __
789
790(** val related_globals_discr :
791    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
792let related_globals_discr a2 a3 a4 =
793  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
794
795(** val related_globals_jmdiscr :
796    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
797let related_globals_jmdiscr a2 a3 a4 =
798  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
799
Note: See TracBrowser for help on using the repository browser.