source: extracted/simplifyCasts.ml @ 3009

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

New extraction.

File size: 28.4 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 eta29441 = simplify_expr lhs target_sz target_sg in
362                   (fun _ ->
363                   (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
364                      eta29441
365                    in
366                   (fun _ ->
367                   (let eta29440 = simplify_expr rhs target_sz target_sg in
368                     (fun _ ->
369                     (let { Types.fst = desired_type_rhs; Types.snd =
370                        rhs1 } = eta29440
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 eta29443 = simplify_expr castee target_sz target_sg
424                    in
425                     (fun _ ->
426                     (let { Types.fst = desired_type; Types.snd = castee1 } =
427                        eta29443
428                      in
429                     (fun _ ->
430                     (match desired_type with
431                      | Bool.True ->
432                        (fun _ -> { Types.fst = Bool.True; Types.snd =
433                          castee1 })
434                      | Bool.False ->
435                        (fun _ ->
436                          (let eta29442 =
437                             simplify_expr castee cast_sz cast_sg
438                           in
439                            (fun _ ->
440                            (let { Types.fst = desired_type2; Types.snd =
441                               castee2 } = eta29442
442                             in
443                            (fun _ ->
444                            (match desired_type2 with
445                             | Bool.True ->
446                               (fun _ -> { Types.fst = Bool.False;
447                                 Types.snd = castee2 })
448                             | Bool.False ->
449                               (fun _ -> { Types.fst = Bool.False;
450                                 Types.snd = (Csyntax.Expr ((Csyntax.Ecast
451                                 (ty, castee2)), cast_ty)) })) __)) __)) __))
452                       __)) __)) __)
453               | Bool.False ->
454                 (fun _ ->
455                   (let eta29444 = simplify_expr castee cast_sz cast_sg in
456                     (fun _ ->
457                     (let { Types.fst = desired_type2; Types.snd =
458                        castee2 } = eta29444
459                      in
460                     (fun _ ->
461                     (match desired_type2 with
462                      | Bool.True ->
463                        (fun _ -> { Types.fst = Bool.False; Types.snd =
464                          castee2 })
465                      | Bool.False ->
466                        (fun _ -> { Types.fst = Bool.False; Types.snd =
467                          (Csyntax.Expr ((Csyntax.Ecast (ty, castee2)),
468                          cast_ty)) })) __)) __)) __)) __
469            | Types.Inr _ ->
470              (let castee1 = simplify_inside castee in
471                (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
472                ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
473        | Csyntax.Tpointer x ->
474          (fun _ ->
475            (let castee1 = simplify_inside castee in
476              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
477              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
478        | Csyntax.Tarray (x, x0) ->
479          (fun _ ->
480            (let castee1 = simplify_inside castee in
481              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
482              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
483        | Csyntax.Tfunction (x, x0) ->
484          (fun _ ->
485            (let castee1 = simplify_inside castee in
486              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
487              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
488        | Csyntax.Tstruct (x, x0) ->
489          (fun _ ->
490            (let castee1 = simplify_inside castee in
491              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
492              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
493        | Csyntax.Tunion (x, x0) ->
494          (fun _ ->
495            (let castee1 = simplify_inside castee in
496              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
497              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
498        | Csyntax.Tcomp_ptr x ->
499          (fun _ ->
500            (let castee1 = simplify_inside castee in
501              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
502              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)) __)
503   | Csyntax.Econdition (cond, iftrue, iffalse) ->
504     (fun _ ->
505       (let cond1 = simplify_inside cond in
506         (fun _ ->
507         match TypeComparison.assert_type_eq ty (Csyntax.typeof iftrue) with
508         | Errors.OK _ ->
509           (match TypeComparison.assert_type_eq (Csyntax.typeof iftrue)
510                    (Csyntax.typeof iffalse) with
511            | Errors.OK _ ->
512              (let eta29446 = simplify_expr iftrue target_sz target_sg in
513                (fun _ ->
514                (let { Types.fst = desired_true; Types.snd = iftrue1 } =
515                   eta29446
516                 in
517                (fun _ ->
518                (let eta29445 = simplify_expr iffalse target_sz target_sg in
519                  (fun _ ->
520                  (let { Types.fst = desired_false; Types.snd = iffalse1 } =
521                     eta29445
522                   in
523                  (fun _ ->
524                  (match Bool.andb desired_true desired_false with
525                   | Bool.True ->
526                     (fun _ -> { Types.fst = Bool.True; Types.snd =
527                       (Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
528                       iffalse1)), (Csyntax.Tint (target_sz, target_sg)))) })
529                   | Bool.False ->
530                     (fun _ ->
531                       (let iftrue10 = simplify_inside iftrue in
532                         (fun _ ->
533                         (let iffalse10 = simplify_inside iffalse in
534                           (fun _ -> { Types.fst = Bool.False; Types.snd =
535                           (Csyntax.Expr ((Csyntax.Econdition (cond1,
536                           iftrue10, iffalse10)), ty)) })) __)) __)) __)) __))
537                  __)) __)) __
538            | Errors.Error x ->
539              (let iftrue1 = simplify_inside iftrue in
540                (fun _ ->
541                (let iffalse1 = simplify_inside iffalse in
542                  (fun _ -> { Types.fst = Bool.False; Types.snd =
543                  (Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
544                  iffalse1)), ty)) })) __)) __)
545         | Errors.Error x ->
546           (let iftrue1 = simplify_inside iftrue in
547             (fun _ ->
548             (let iffalse1 = simplify_inside iffalse in
549               (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
550               ((Csyntax.Econdition (cond1, iftrue1, iffalse1)), ty)) })) __))
551             __)) __)
552   | Csyntax.Eandbool (lhs, rhs) ->
553     (fun _ ->
554       (let lhs1 = simplify_inside lhs in
555         (fun _ ->
556         (let rhs1 = simplify_inside rhs in
557           (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
558           ((Csyntax.Eandbool (lhs1, rhs1)), ty)) })) __)) __)
559   | Csyntax.Eorbool (lhs, rhs) ->
560     (fun _ ->
561       (let lhs1 = simplify_inside lhs in
562         (fun _ ->
563         (let rhs1 = simplify_inside rhs in
564           (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
565           ((Csyntax.Eorbool (lhs1, rhs1)), ty)) })) __)) __)
566   | Csyntax.Esizeof t ->
567     (fun _ -> { Types.fst =
568       (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg)));
569       Types.snd = (Csyntax.Expr (ed, ty)) })
570   | Csyntax.Efield (rec_expr, f) ->
571     (fun _ ->
572       (let rec_expr1 = simplify_inside rec_expr in
573         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
574         ((Csyntax.Efield (rec_expr1, f)), ty)) })) __)
575   | Csyntax.Ecost (l, e1) ->
576     (fun _ ->
577       match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with
578       | Types.Inl _ ->
579         (let eta29447 = simplify_expr e1 target_sz target_sg in
580           (fun _ ->
581           (let { Types.fst = desired_type; Types.snd = e2 } = eta29447 in
582           (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
583           ((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __
584       | Types.Inr _ ->
585         (let e2 = simplify_inside e1 in
586           (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
587           ((Csyntax.Ecost (l, e2)), ty)) })) __)) __)) __
588(** val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0 **)
589and simplify_inside e =
590  (let Csyntax.Expr (ed, ty) = e in
591  (fun _ ->
592  (match ed with
593   | Csyntax.Econst_int (x, x0) -> (fun _ -> e)
594   | Csyntax.Evar x -> (fun _ -> e)
595   | Csyntax.Ederef e1 ->
596     (fun _ ->
597       (let e2 = simplify_inside e1 in
598         (fun _ -> Csyntax.Expr ((Csyntax.Ederef e2), ty))) __)
599   | Csyntax.Eaddrof e1 ->
600     (fun _ ->
601       (let e2 = simplify_inside e1 in
602         (fun _ -> Csyntax.Expr ((Csyntax.Eaddrof e2), ty))) __)
603   | Csyntax.Eunop (op, e1) ->
604     (fun _ ->
605       (let e2 = simplify_inside e1 in
606         (fun _ -> Csyntax.Expr ((Csyntax.Eunop (op, e2)), ty))) __)
607   | Csyntax.Ebinop (op, lhs, rhs) ->
608     (fun _ ->
609       (let lhs1 = simplify_inside lhs in
610         (fun _ ->
611         (let rhs1 = simplify_inside rhs in
612           (fun _ -> Csyntax.Expr ((Csyntax.Ebinop (op, lhs1, rhs1)), ty)))
613           __)) __)
614   | Csyntax.Ecast (cast_ty, castee) ->
615     (fun _ ->
616       match TypeComparison.type_eq_dec ty cast_ty with
617       | Types.Inl _ ->
618         (match cast_ty with
619          | Csyntax.Tvoid -> (fun _ -> e)
620          | Csyntax.Tint (cast_sz, cast_sg) ->
621            (fun _ ->
622              (let eta29448 = simplify_expr castee cast_sz cast_sg in
623                (fun _ ->
624                (let { Types.fst = success; Types.snd = castee1 } = eta29448
625                 in
626                (fun _ ->
627                (match success with
628                 | Bool.True -> (fun _ -> castee1)
629                 | Bool.False ->
630                   (fun _ -> Csyntax.Expr ((Csyntax.Ecast (cast_ty,
631                     castee1)), ty))) __)) __)) __)
632          | Csyntax.Tpointer x -> (fun _ -> e)
633          | Csyntax.Tarray (x, x0) -> (fun _ -> e)
634          | Csyntax.Tfunction (x, x0) -> (fun _ -> e)
635          | Csyntax.Tstruct (x, x0) -> (fun _ -> e)
636          | Csyntax.Tunion (x, x0) -> (fun _ -> e)
637          | Csyntax.Tcomp_ptr x -> (fun _ -> e)) __
638       | Types.Inr _ -> e)
639   | Csyntax.Econdition (cond, iftrue, iffalse) ->
640     (fun _ ->
641       (let cond1 = simplify_inside cond in
642         (fun _ ->
643         (let iftrue1 = simplify_inside iftrue in
644           (fun _ ->
645           (let iffalse1 = simplify_inside iffalse in
646             (fun _ -> Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
647             iffalse1)), ty))) __)) __)) __)
648   | Csyntax.Eandbool (lhs, rhs) ->
649     (fun _ ->
650       (let lhs1 = simplify_inside lhs in
651         (fun _ ->
652         (let rhs1 = simplify_inside rhs in
653           (fun _ -> Csyntax.Expr ((Csyntax.Eandbool (lhs1, rhs1)), ty))) __))
654         __)
655   | Csyntax.Eorbool (lhs, rhs) ->
656     (fun _ ->
657       (let lhs1 = simplify_inside lhs in
658         (fun _ ->
659         (let rhs1 = simplify_inside rhs in
660           (fun _ -> Csyntax.Expr ((Csyntax.Eorbool (lhs1, rhs1)), ty))) __))
661         __)
662   | Csyntax.Esizeof x -> (fun _ -> e)
663   | Csyntax.Efield (rec_expr, f) ->
664     (fun _ ->
665       (let rec_expr1 = simplify_inside rec_expr in
666         (fun _ -> Csyntax.Expr ((Csyntax.Efield (rec_expr1, f)), ty))) __)
667   | Csyntax.Ecost (l, e1) ->
668     (fun _ ->
669       (let e2 = simplify_inside e1 in
670         (fun _ -> Csyntax.Expr ((Csyntax.Ecost (l, e2)), ty))) __)) __)) __
671
672(** val simplify_e : Csyntax.expr -> Csyntax.expr **)
673let simplify_e e =
674  Types.pi1 (simplify_inside e)
675
676(** val simplify_statement : Csyntax.statement -> Csyntax.statement **)
677let rec simplify_statement = function
678| Csyntax.Sskip -> Csyntax.Sskip
679| Csyntax.Sassign (e1, e2) ->
680  Csyntax.Sassign ((simplify_e e1), (simplify_e e2))
681| Csyntax.Scall (eo, e, es) ->
682  Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e),
683    (List.map simplify_e es))
684| Csyntax.Ssequence (s1, s2) ->
685  Csyntax.Ssequence ((simplify_statement s1), (simplify_statement s2))
686| Csyntax.Sifthenelse (e, s1, s2) ->
687  Csyntax.Sifthenelse ((simplify_e e), (simplify_statement s1),
688    (simplify_statement s2))
689| Csyntax.Swhile (e, s1) ->
690  Csyntax.Swhile ((simplify_e e), (simplify_statement s1))
691| Csyntax.Sdowhile (e, s1) ->
692  Csyntax.Sdowhile ((simplify_e e), (simplify_statement s1))
693| Csyntax.Sfor (s1, e, s2, s3) ->
694  Csyntax.Sfor ((simplify_statement s1), (simplify_e e),
695    (simplify_statement s2), (simplify_statement s3))
696| Csyntax.Sbreak -> Csyntax.Sbreak
697| Csyntax.Scontinue -> Csyntax.Scontinue
698| Csyntax.Sreturn eo -> Csyntax.Sreturn (Types.option_map simplify_e eo)
699| Csyntax.Sswitch (e, ls) ->
700  Csyntax.Sswitch ((simplify_e e), (simplify_ls ls))
701| Csyntax.Slabel (l, s1) -> Csyntax.Slabel (l, (simplify_statement s1))
702| Csyntax.Sgoto l -> Csyntax.Sgoto l
703| Csyntax.Scost (l, s1) -> Csyntax.Scost (l, (simplify_statement s1))
704(** val simplify_ls :
705    Csyntax.labeled_statements -> Csyntax.labeled_statements **)
706and simplify_ls = function
707| Csyntax.LSdefault s -> Csyntax.LSdefault (simplify_statement s)
708| Csyntax.LScase (sz, i, s, ls') ->
709  Csyntax.LScase (sz, i, (simplify_statement s), (simplify_ls ls'))
710
711(** val simplify_function : Csyntax.function0 -> Csyntax.function0 **)
712let simplify_function f =
713  { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
714    f.Csyntax.fn_params; Csyntax.fn_vars = f.Csyntax.fn_vars;
715    Csyntax.fn_body = (simplify_statement f.Csyntax.fn_body) }
716
717(** val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef **)
718let simplify_fundef f = match f with
719| Csyntax.CL_Internal f0 -> Csyntax.CL_Internal (simplify_function f0)
720| Csyntax.CL_External (x, x0, x1) -> f
721
722(** val simplify_program :
723    Csyntax.clight_program -> Csyntax.clight_program **)
724let simplify_program p =
725  AST.transform_program p (fun x -> simplify_fundef)
726
727(** val related_globals_rect_Type4 :
728    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
729    __ -> __ -> 'a2) -> 'a2 **)
730let rec related_globals_rect_Type4 t ge ge' h_mk_related_globals =
731  h_mk_related_globals __ __ __
732
733(** val related_globals_rect_Type5 :
734    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
735    __ -> __ -> 'a2) -> 'a2 **)
736let rec related_globals_rect_Type5 t ge ge' h_mk_related_globals =
737  h_mk_related_globals __ __ __
738
739(** val related_globals_rect_Type3 :
740    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
741    __ -> __ -> 'a2) -> 'a2 **)
742let rec related_globals_rect_Type3 t ge ge' h_mk_related_globals =
743  h_mk_related_globals __ __ __
744
745(** val related_globals_rect_Type2 :
746    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
747    __ -> __ -> 'a2) -> 'a2 **)
748let rec related_globals_rect_Type2 t ge ge' h_mk_related_globals =
749  h_mk_related_globals __ __ __
750
751(** val related_globals_rect_Type1 :
752    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
753    __ -> __ -> 'a2) -> 'a2 **)
754let rec related_globals_rect_Type1 t ge ge' h_mk_related_globals =
755  h_mk_related_globals __ __ __
756
757(** val related_globals_rect_Type0 :
758    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
759    __ -> __ -> 'a2) -> 'a2 **)
760let rec related_globals_rect_Type0 t ge ge' h_mk_related_globals =
761  h_mk_related_globals __ __ __
762
763(** val related_globals_inv_rect_Type4 :
764    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
765    __ -> __ -> __ -> 'a2) -> 'a2 **)
766let related_globals_inv_rect_Type4 x2 x3 x4 h1 =
767  let hcut = related_globals_rect_Type4 x2 x3 x4 h1 in hcut __
768
769(** val related_globals_inv_rect_Type3 :
770    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
771    __ -> __ -> __ -> 'a2) -> 'a2 **)
772let related_globals_inv_rect_Type3 x2 x3 x4 h1 =
773  let hcut = related_globals_rect_Type3 x2 x3 x4 h1 in hcut __
774
775(** val related_globals_inv_rect_Type2 :
776    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
777    __ -> __ -> __ -> 'a2) -> 'a2 **)
778let related_globals_inv_rect_Type2 x2 x3 x4 h1 =
779  let hcut = related_globals_rect_Type2 x2 x3 x4 h1 in hcut __
780
781(** val related_globals_inv_rect_Type1 :
782    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
783    __ -> __ -> __ -> 'a2) -> 'a2 **)
784let related_globals_inv_rect_Type1 x2 x3 x4 h1 =
785  let hcut = related_globals_rect_Type1 x2 x3 x4 h1 in hcut __
786
787(** val related_globals_inv_rect_Type0 :
788    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
789    __ -> __ -> __ -> 'a2) -> 'a2 **)
790let related_globals_inv_rect_Type0 x2 x3 x4 h1 =
791  let hcut = related_globals_rect_Type0 x2 x3 x4 h1 in hcut __
792
793(** val related_globals_discr :
794    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
795let related_globals_discr a2 a3 a4 =
796  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
797
798(** val related_globals_jmdiscr :
799    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
800let related_globals_jmdiscr a2 a3 a4 =
801  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
802
Note: See TracBrowser for help on using the repository browser.