source: extracted/simplifyCasts.ml @ 2716

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

...

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