source: driver/extracted/simplifyCasts.ml @ 3106

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

New extraction.

File size: 25.2 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 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.tail (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 bit =
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 bit i0 with
172       | Types.None -> Types.None
173       | Types.Some i' ->
174         (match signed sg' with
175          | Bool.True ->
176            (match BitVector.eq_b bit (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_r 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.One -> 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 e target_sz target_sg =
294  (let Csyntax.Expr (ed, ty) = e 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 = e })
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 = e }
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 = e })
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 = e })
318        | Csyntax.Tpointer x ->
319          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
320        | Csyntax.Tarray (x, x0) ->
321          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
322        | Csyntax.Tfunction (x, x0) ->
323          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
324        | Csyntax.Tstruct (x, x0) ->
325          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
326        | Csyntax.Tunion (x, x0) ->
327          (fun _ -> { Types.fst = Bool.False; Types.snd = e })
328        | Csyntax.Tcomp_ptr x ->
329          (fun _ -> { Types.fst = Bool.False; Types.snd = e })) __)
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 e1 ->
335     (fun _ ->
336       (let e2 = simplify_inside e1 in
337         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
338         ((Csyntax.Ederef e2), ty)) })) __)
339   | Csyntax.Eaddrof e1 ->
340     (fun _ ->
341       (let e2 = simplify_inside e1 in
342         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
343         ((Csyntax.Eaddrof e2), ty)) })) __)
344   | Csyntax.Eunop (op, e1) ->
345     (fun _ ->
346       (let e2 = simplify_inside e1 in
347         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
348         ((Csyntax.Eunop (op, e2)), ty)) })) __)
349   | Csyntax.Ebinop (op, lhs, rhs) ->
350     (fun _ ->
351       (match binop_simplifiable op 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 eta2033 = simplify_expr lhs target_sz target_sg in
360                   (fun _ ->
361                   (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
362                      eta2033
363                    in
364                   (fun _ ->
365                   (let eta2032 = simplify_expr rhs target_sz target_sg in
366                     (fun _ ->
367                     (let { Types.fst = desired_type_rhs; Types.snd =
368                        rhs1 } = eta2032
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 (op, 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 (op, 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 (op, 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 (op, 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 (op, 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 eta2035 = simplify_expr castee target_sz target_sg in
422                     (fun _ ->
423                     (let { Types.fst = desired_type; Types.snd = castee1 } =
424                        eta2035
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 eta2034 = simplify_expr castee cast_sz cast_sg
434                           in
435                            (fun _ ->
436                            (let { Types.fst = desired_type2; Types.snd =
437                               castee2 } = eta2034
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 eta2036 = simplify_expr castee cast_sz cast_sg in
452                     (fun _ ->
453                     (let { Types.fst = desired_type2; Types.snd =
454                        castee2 } = eta2036
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 eta2038 = simplify_expr iftrue target_sz target_sg in
509                (fun _ ->
510                (let { Types.fst = desired_true; Types.snd = iftrue1 } =
511                   eta2038
512                 in
513                (fun _ ->
514                (let eta2037 = simplify_expr iffalse target_sz target_sg in
515                  (fun _ ->
516                  (let { Types.fst = desired_false; Types.snd = iffalse1 } =
517                     eta2037
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, e1) ->
572     (fun _ ->
573       match TypeComparison.type_eq_dec ty (Csyntax.typeof e1) with
574       | Types.Inl _ ->
575         (let eta2039 = simplify_expr e1 target_sz target_sg in
576           (fun _ ->
577           (let { Types.fst = desired_type; Types.snd = e2 } = eta2039 in
578           (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
579           ((Csyntax.Ecost (l, e2)), (Csyntax.typeof e2))) })) __)) __
580       | Types.Inr _ ->
581         (let e2 = simplify_inside e1 in
582           (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
583           ((Csyntax.Ecost (l, e2)), ty)) })) __)) __)) __
584(** val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0 **)
585and simplify_inside e =
586  (let Csyntax.Expr (ed, ty) = e in
587  (fun _ ->
588  (match ed with
589   | Csyntax.Econst_int (x, x0) -> (fun _ -> e)
590   | Csyntax.Evar x -> (fun _ -> e)
591   | Csyntax.Ederef e1 ->
592     (fun _ ->
593       (let e2 = simplify_inside e1 in
594         (fun _ -> Csyntax.Expr ((Csyntax.Ederef e2), ty))) __)
595   | Csyntax.Eaddrof e1 ->
596     (fun _ ->
597       (let e2 = simplify_inside e1 in
598         (fun _ -> Csyntax.Expr ((Csyntax.Eaddrof e2), ty))) __)
599   | Csyntax.Eunop (op, e1) ->
600     (fun _ ->
601       (let e2 = simplify_inside e1 in
602         (fun _ -> Csyntax.Expr ((Csyntax.Eunop (op, e2)), ty))) __)
603   | Csyntax.Ebinop (op, 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 (op, 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 _ -> e)
616          | Csyntax.Tint (cast_sz, cast_sg) ->
617            (fun _ ->
618              (let eta2040 = simplify_expr castee cast_sz cast_sg in
619                (fun _ ->
620                (let { Types.fst = success; Types.snd = castee1 } = eta2040
621                 in
622                (fun _ ->
623                (match success with
624                 | Bool.True -> (fun _ -> castee1)
625                 | Bool.False ->
626                   (fun _ -> Csyntax.Expr ((Csyntax.Ecast (cast_ty,
627                     castee1)), ty))) __)) __)) __)
628          | Csyntax.Tpointer x -> (fun _ -> e)
629          | Csyntax.Tarray (x, x0) -> (fun _ -> e)
630          | Csyntax.Tfunction (x, x0) -> (fun _ -> e)
631          | Csyntax.Tstruct (x, x0) -> (fun _ -> e)
632          | Csyntax.Tunion (x, x0) -> (fun _ -> e)
633          | Csyntax.Tcomp_ptr x -> (fun _ -> e)) __
634       | Types.Inr _ -> e)
635   | Csyntax.Econdition (cond, iftrue, iffalse) ->
636     (fun _ ->
637       (let cond1 = simplify_inside cond in
638         (fun _ ->
639         (let iftrue1 = simplify_inside iftrue in
640           (fun _ ->
641           (let iffalse1 = simplify_inside iffalse in
642             (fun _ -> Csyntax.Expr ((Csyntax.Econdition (cond1, iftrue1,
643             iffalse1)), ty))) __)) __)) __)
644   | Csyntax.Eandbool (lhs, rhs) ->
645     (fun _ ->
646       (let lhs1 = simplify_inside lhs in
647         (fun _ ->
648         (let rhs1 = simplify_inside rhs in
649           (fun _ -> Csyntax.Expr ((Csyntax.Eandbool (lhs1, rhs1)), ty))) __))
650         __)
651   | Csyntax.Eorbool (lhs, rhs) ->
652     (fun _ ->
653       (let lhs1 = simplify_inside lhs in
654         (fun _ ->
655         (let rhs1 = simplify_inside rhs in
656           (fun _ -> Csyntax.Expr ((Csyntax.Eorbool (lhs1, rhs1)), ty))) __))
657         __)
658   | Csyntax.Esizeof x -> (fun _ -> e)
659   | Csyntax.Efield (rec_expr, f) ->
660     (fun _ ->
661       (let rec_expr1 = simplify_inside rec_expr in
662         (fun _ -> Csyntax.Expr ((Csyntax.Efield (rec_expr1, f)), ty))) __)
663   | Csyntax.Ecost (l, e1) ->
664     (fun _ ->
665       (let e2 = simplify_inside e1 in
666         (fun _ -> Csyntax.Expr ((Csyntax.Ecost (l, e2)), ty))) __)) __)) __
667
668(** val simplify_e : Csyntax.expr -> Csyntax.expr **)
669let simplify_e e =
670  Types.pi1 (simplify_inside e)
671
672(** val simplify_statement : Csyntax.statement -> Csyntax.statement **)
673let rec simplify_statement = function
674| Csyntax.Sskip -> Csyntax.Sskip
675| Csyntax.Sassign (e1, e2) ->
676  Csyntax.Sassign ((simplify_e e1), (simplify_e e2))
677| Csyntax.Scall (eo, e, es) ->
678  Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e),
679    (List.map simplify_e es))
680| Csyntax.Ssequence (s1, s2) ->
681  Csyntax.Ssequence ((simplify_statement s1), (simplify_statement s2))
682| Csyntax.Sifthenelse (e, s1, s2) ->
683  Csyntax.Sifthenelse ((simplify_e e), (simplify_statement s1),
684    (simplify_statement s2))
685| Csyntax.Swhile (e, s1) ->
686  Csyntax.Swhile ((simplify_e e), (simplify_statement s1))
687| Csyntax.Sdowhile (e, s1) ->
688  Csyntax.Sdowhile ((simplify_e e), (simplify_statement s1))
689| Csyntax.Sfor (s1, e, s2, s3) ->
690  Csyntax.Sfor ((simplify_statement s1), (simplify_e e),
691    (simplify_statement s2), (simplify_statement s3))
692| Csyntax.Sbreak -> Csyntax.Sbreak
693| Csyntax.Scontinue -> Csyntax.Scontinue
694| Csyntax.Sreturn eo -> Csyntax.Sreturn (Types.option_map simplify_e eo)
695| Csyntax.Sswitch (e, ls) ->
696  Csyntax.Sswitch ((simplify_e e), (simplify_ls ls))
697| Csyntax.Slabel (l, s1) -> Csyntax.Slabel (l, (simplify_statement s1))
698| Csyntax.Sgoto l -> Csyntax.Sgoto l
699| Csyntax.Scost (l, s1) -> Csyntax.Scost (l, (simplify_statement s1))
700(** val simplify_ls :
701    Csyntax.labeled_statements -> Csyntax.labeled_statements **)
702and simplify_ls = function
703| Csyntax.LSdefault s -> Csyntax.LSdefault (simplify_statement s)
704| Csyntax.LScase (sz, i, s, ls') ->
705  Csyntax.LScase (sz, i, (simplify_statement s), (simplify_ls ls'))
706
707(** val simplify_function : Csyntax.function0 -> Csyntax.function0 **)
708let simplify_function f =
709  { Csyntax.fn_return = f.Csyntax.fn_return; Csyntax.fn_params =
710    f.Csyntax.fn_params; Csyntax.fn_vars = f.Csyntax.fn_vars;
711    Csyntax.fn_body = (simplify_statement f.Csyntax.fn_body) }
712
713(** val simplify_fundef : Csyntax.clight_fundef -> Csyntax.clight_fundef **)
714let simplify_fundef f = match f with
715| Csyntax.CL_Internal f0 -> Csyntax.CL_Internal (simplify_function f0)
716| Csyntax.CL_External (x, x0, x1) -> f
717
718(** val simplify_program :
719    Csyntax.clight_program -> Csyntax.clight_program **)
720let simplify_program p =
721  AST.transform_program p (fun x -> simplify_fundef)
722
Note: See TracBrowser for help on using the repository browser.