source: extracted/simplifyCasts.ml @ 2717

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

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.
File size: 28.4 KB
Line 
1open Preamble
2
3open BitVectorTrie
4
5open CostLabel
6
7open Coqlib
8
9open Proper
10
11open PositiveMap
12
13open Deqsets
14
15open ErrorMessages
16
17open PreIdentifiers
18
19open Errors
20
21open Extralib
22
23open Setoids
24
25open Monad
26
27open Option
28
29open Lists
30
31open Positive
32
33open Identifiers
34
35open Exp
36
37open Arithmetic
38
39open Vector
40
41open Div_and_mod
42
43open Jmeq
44
45open Russell
46
47open List
48
49open Util
50
51open FoldStuff
52
53open BitVector
54
55open Extranat
56
57open Bool
58
59open Relations
60
61open Nat
62
63open Integers
64
65open Hints_declaration
66
67open Core_notation
68
69open Pts
70
71open Logic
72
73open Types
74
75open AST
76
77open Csyntax
78
79open TypeComparison
80
81open ClassifyOp
82
83open Smallstep
84
85open Extra_bool
86
87open FrontEndVal
88
89open Hide
90
91open ByteValues
92
93open GenMem
94
95open FrontEndMem
96
97open Globalenvs
98
99open Csem
100
101open SmallstepExec
102
103open Division
104
105open Z
106
107open BitVectorZ
108
109open Pointers
110
111open Values
112
113open Events
114
115open IOMonad
116
117open IO
118
119open Cexec
120
121open Casts
122
123open CexecInd
124
125open CexecSound
126
127open Sets
128
129open Listb
130
131open Star
132
133open Frontend_misc
134
135(** val reduce_bits :
136    Nat.nat -> Nat.nat -> Bool.bool -> BitVector.bitVector ->
137    BitVector.bitVector Types.option **)
138let rec reduce_bits n m exp0 v =
139  (match n with
140   | Nat.O -> (fun v0 -> Types.Some v0)
141   | Nat.S n' ->
142     (fun v0 ->
143       match BitVector.eq_b (Vector.head' (Nat.plus n' (Nat.S m)) v0) exp0 with
144       | Bool.True ->
145         reduce_bits n' m exp0 (Vector.tail0 (Nat.plus n' (Nat.S m)) v0)
146       | Bool.False -> Types.None)) v
147
148(** val pred_bitsize_of_intsize : AST.intsize -> Nat.nat **)
149let pred_bitsize_of_intsize sz =
150  Nat.pred (AST.bitsize_of_intsize sz)
151
152(** val signed : AST.signedness -> Bool.bool **)
153let signed = function
154| AST.Signed -> Bool.True
155| AST.Unsigned -> Bool.False
156
157(** val simplify_int :
158    AST.intsize -> AST.intsize -> AST.signedness -> AST.signedness ->
159    AST.bvint -> AST.bvint Types.option **)
160let rec simplify_int sz sz' sg sg' i =
161  let bit0 =
162    Bool.andb (signed sg)
163      (Vector.head'
164        (Nat.plus (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
165          Nat.O)))))))
166          (Nat.times (AST.pred_size_intsize sz) (Nat.S (Nat.S (Nat.S (Nat.S
167            (Nat.S (Nat.S (Nat.S (Nat.S Nat.O)))))))))) i)
168  in
169  (match Extranat.nat_compare (pred_bitsize_of_intsize sz)
170           (pred_bitsize_of_intsize sz') with
171   | Extranat.Nat_lt (x, x0) -> (fun i0 -> Types.None)
172   | Extranat.Nat_eq x -> (fun i0 -> Types.Some i0)
173   | Extranat.Nat_gt (x, y) ->
174     (fun i0 ->
175       match reduce_bits (Nat.S x) y bit0 i0 with
176       | Types.None -> Types.None
177       | Types.Some i' ->
178         (match signed sg' with
179          | Bool.True ->
180            (match BitVector.eq_b bit0 (Vector.head' y i') with
181             | Bool.True -> Types.Some i'
182             | Bool.False -> Types.None)
183          | Bool.False -> Types.Some i'))) i
184
185(** val size_lt_dec : AST.intsize -> AST.intsize -> (__, __) Types.sum **)
186let size_lt_dec = function
187| AST.I8 ->
188  (fun clearme0 ->
189    match clearme0 with
190    | AST.I8 -> Types.Inr __
191    | AST.I16 -> Types.Inl __
192    | AST.I32 -> Types.Inl __)
193| AST.I16 ->
194  (fun clearme0 ->
195    match clearme0 with
196    | AST.I8 -> Types.Inr __
197    | AST.I16 -> Types.Inr __
198    | AST.I32 -> Types.Inl __)
199| AST.I32 ->
200  (fun clearme0 ->
201    match clearme0 with
202    | AST.I8 -> Types.Inr __
203    | AST.I16 -> Types.Inr __
204    | AST.I32 -> Types.Inr __)
205
206(** val size_not_lt_to_ge :
207    AST.intsize -> AST.intsize -> (__, __) Types.sum **)
208let size_not_lt_to_ge clearme sz2 =
209  (match clearme with
210   | AST.I8 ->
211     (fun clearme0 ->
212       match clearme0 with
213       | AST.I8 -> (fun _ -> Types.Inl __)
214       | AST.I16 -> (fun _ -> Types.Inr __)
215       | AST.I32 -> (fun _ -> Types.Inr __))
216   | AST.I16 ->
217     (fun clearme0 ->
218       match clearme0 with
219       | AST.I8 -> (fun _ -> Types.Inr __)
220       | AST.I16 -> (fun _ -> Types.Inl __)
221       | AST.I32 -> (fun _ -> Types.Inr __))
222   | AST.I32 ->
223     (fun clearme0 ->
224       match clearme0 with
225       | AST.I8 -> (fun _ -> Types.Inr __)
226       | AST.I16 -> (fun _ -> Types.Inr __)
227       | AST.I32 -> (fun _ -> Types.Inl __))) sz2 __
228
229(** val sign_eq_dect :
230    AST.signedness -> AST.signedness -> (__, __) Types.sum **)
231let sign_eq_dect = function
232| AST.Signed ->
233  (fun clearme0 ->
234    match clearme0 with
235    | AST.Signed -> TypeComparison.sg_eq_dec AST.Signed AST.Signed
236    | AST.Unsigned -> TypeComparison.sg_eq_dec AST.Signed AST.Unsigned)
237| AST.Unsigned ->
238  (fun clearme0 ->
239    match clearme0 with
240    | AST.Signed -> TypeComparison.sg_eq_dec AST.Unsigned AST.Signed
241    | AST.Unsigned -> TypeComparison.sg_eq_dec AST.Unsigned AST.Unsigned)
242
243(** val necessary_conditions :
244    AST.intsize -> AST.signedness -> AST.intsize -> AST.signedness ->
245    Bool.bool **)
246let necessary_conditions src_sz src_sg target_sz target_sg =
247  match size_lt_dec target_sz src_sz with
248  | Types.Inl _ -> Bool.True
249  | Types.Inr _ ->
250    (match TypeComparison.sz_eq_dec target_sz src_sz with
251     | Types.Inl _ ->
252       (match sign_eq_dect src_sg target_sg with
253        | Types.Inl _ -> Bool.False
254        | Types.Inr _ -> Bool.True)
255     | Types.Inr _ -> Bool.False)
256
257(** val assert_int_value :
258    Values.val0 Types.option -> AST.intsize -> BitVector.bitVector
259    Types.option **)
260let rec assert_int_value v expected_size =
261  match v with
262  | Types.None -> Types.None
263  | Types.Some v0 ->
264    (match v0 with
265     | Values.Vundef -> Types.None
266     | Values.Vint (sz, i) ->
267       (match TypeComparison.sz_eq_dec sz expected_size with
268        | Types.Inl _ ->
269          Types.Some
270            (Extralib.eq_rect_Type0_r1 expected_size (fun i0 -> i0) sz i)
271        | Types.Inr _ -> Types.None)
272     | Values.Vnull -> Types.None
273     | Values.Vptr x -> Types.None)
274
275(** val binop_simplifiable : Csyntax.binary_operation -> Bool.bool **)
276let binop_simplifiable = function
277| Csyntax.Oadd -> Bool.True
278| Csyntax.Osub -> Bool.True
279| Csyntax.Omul -> Bool.False
280| Csyntax.Odiv -> Bool.False
281| Csyntax.Omod -> Bool.False
282| Csyntax.Oand -> Bool.False
283| Csyntax.Oor -> Bool.False
284| Csyntax.Oxor -> Bool.False
285| Csyntax.Oshl -> Bool.False
286| Csyntax.Oshr -> Bool.False
287| Csyntax.Oeq -> Bool.False
288| Csyntax.One0 -> Bool.False
289| Csyntax.Olt -> Bool.False
290| Csyntax.Ogt -> Bool.False
291| Csyntax.Ole -> Bool.False
292| Csyntax.Oge -> Bool.False
293
294(** val simplify_expr :
295    Csyntax.expr -> AST.intsize -> AST.signedness -> (Bool.bool,
296    Csyntax.expr) Types.prod Types.sig0 **)
297let rec simplify_expr e1 target_sz target_sg =
298  (let Csyntax.Expr (ed, ty) = e1 in
299  (fun _ ->
300  (match ed with
301   | Csyntax.Econst_int (cst_sz, i) ->
302     (fun _ ->
303       (match ty with
304        | Csyntax.Tvoid ->
305          (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
306        | Csyntax.Tint (ty_sz, sg) ->
307          (fun _ ->
308            match TypeComparison.sz_eq_dec cst_sz ty_sz with
309            | Types.Inl _ ->
310              (match TypeComparison.type_eq_dec ty (Csyntax.Tint (target_sz,
311                       target_sg)) with
312               | Types.Inl _ -> { Types.fst = Bool.True; Types.snd = e1 }
313               | Types.Inr _ ->
314                 (match simplify_int cst_sz target_sz sg target_sg i with
315                  | Types.None ->
316                    (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
317                  | Types.Some i' ->
318                    (fun _ -> { Types.fst = Bool.True; Types.snd =
319                      (Csyntax.Expr ((Csyntax.Econst_int (target_sz, i')),
320                      (Csyntax.Tint (target_sz, target_sg)))) })) __)
321            | Types.Inr _ -> { Types.fst = Bool.False; Types.snd = e1 })
322        | Csyntax.Tpointer x ->
323          (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
324        | Csyntax.Tarray (x, x0) ->
325          (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
326        | Csyntax.Tfunction (x, x0) ->
327          (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
328        | Csyntax.Tstruct (x, x0) ->
329          (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
330        | Csyntax.Tunion (x, x0) ->
331          (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })
332        | Csyntax.Tcomp_ptr x ->
333          (fun _ -> { Types.fst = Bool.False; Types.snd = e1 })) __)
334   | Csyntax.Evar id ->
335     (fun _ -> { Types.fst =
336       (TypeComparison.type_eq ty (Csyntax.Tint (target_sz, target_sg)));
337       Types.snd = (Csyntax.Expr (ed, ty)) })
338   | Csyntax.Ederef e2 ->
339     (fun _ ->
340       (let e3 = simplify_inside e2 in
341         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
342         ((Csyntax.Ederef e3), ty)) })) __)
343   | Csyntax.Eaddrof e2 ->
344     (fun _ ->
345       (let e3 = simplify_inside e2 in
346         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
347         ((Csyntax.Eaddrof e3), ty)) })) __)
348   | Csyntax.Eunop (op0, e2) ->
349     (fun _ ->
350       (let e3 = simplify_inside e2 in
351         (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
352         ((Csyntax.Eunop (op0, e3)), ty)) })) __)
353   | Csyntax.Ebinop (op0, lhs, rhs) ->
354     (fun _ ->
355       (match binop_simplifiable op0 with
356        | Bool.True ->
357          (fun _ ->
358            match TypeComparison.assert_type_eq ty (Csyntax.typeof lhs) with
359            | Errors.OK _ ->
360              (match TypeComparison.assert_type_eq (Csyntax.typeof lhs)
361                       (Csyntax.typeof rhs) with
362               | Errors.OK _ ->
363                 (let eta2519 = simplify_expr lhs target_sz target_sg in
364                   (fun _ ->
365                   (let { Types.fst = desired_type_lhs; Types.snd = lhs1 } =
366                      eta2519
367                    in
368                   (fun _ ->
369                   (let eta2518 = simplify_expr rhs target_sz target_sg in
370                     (fun _ ->
371                     (let { Types.fst = desired_type_rhs; Types.snd =
372                        rhs1 } = eta2518
373                      in
374                     (fun _ ->
375                     (match Bool.andb desired_type_lhs desired_type_rhs with
376                      | Bool.True ->
377                        (fun _ -> { Types.fst = Bool.True; Types.snd =
378                          (Csyntax.Expr ((Csyntax.Ebinop (op0, lhs1, rhs1)),
379                          (Csyntax.Tint (target_sz, target_sg)))) })
380                      | Bool.False ->
381                        (fun _ ->
382                          (let lhs10 = simplify_inside lhs in
383                            (fun _ ->
384                            (let rhs10 = simplify_inside rhs in
385                              (fun _ -> { Types.fst = Bool.False; Types.snd =
386                              (Csyntax.Expr ((Csyntax.Ebinop (op0, lhs10,
387                              rhs10)), ty)) })) __)) __)) __)) __)) __)) __))
388                   __
389               | Errors.Error x ->
390                 (let lhs1 = simplify_inside lhs in
391                   (fun _ ->
392                   (let rhs1 = simplify_inside rhs in
393                     (fun _ -> { Types.fst = Bool.False; Types.snd =
394                     (Csyntax.Expr ((Csyntax.Ebinop (op0, lhs1, rhs1)),
395                     ty)) })) __)) __)
396            | Errors.Error x ->
397              (let lhs1 = simplify_inside lhs in
398                (fun _ ->
399                (let rhs1 = simplify_inside rhs in
400                  (fun _ -> { Types.fst = Bool.False; Types.snd =
401                  (Csyntax.Expr ((Csyntax.Ebinop (op0, lhs1, rhs1)), ty)) }))
402                  __)) __)
403        | Bool.False ->
404          (fun _ ->
405            (let lhs1 = simplify_inside lhs in
406              (fun _ ->
407              (let rhs1 = simplify_inside rhs in
408                (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
409                ((Csyntax.Ebinop (op0, lhs1, rhs1)), ty)) })) __)) __)) __)
410   | Csyntax.Ecast (cast_ty, castee) ->
411     (fun _ ->
412       (match cast_ty with
413        | Csyntax.Tvoid ->
414          (fun _ ->
415            (let castee1 = simplify_inside castee in
416              (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
417              ((Csyntax.Ecast (cast_ty, castee1)), ty)) })) __)
418        | Csyntax.Tint (cast_sz, cast_sg) ->
419          (fun _ ->
420            match TypeComparison.type_eq_dec ty cast_ty with
421            | Types.Inl _ ->
422              (match necessary_conditions cast_sz cast_sg target_sz target_sg with
423               | Bool.True ->
424                 (fun _ ->
425                   (let eta2521 = simplify_expr castee target_sz target_sg in
426                     (fun _ ->
427                     (let { Types.fst = desired_type; Types.snd = castee1 } =
428                        eta2521
429                      in
430                     (fun _ ->
431                     (match desired_type with
432                      | Bool.True ->
433                        (fun _ -> { Types.fst = Bool.True; Types.snd =
434                          castee1 })
435                      | Bool.False ->
436                        (fun _ ->
437                          (let eta2520 = simplify_expr castee cast_sz cast_sg
438                           in
439                            (fun _ ->
440                            (let { Types.fst = desired_type2; Types.snd =
441                               castee2 } = eta2520
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 eta2522 = simplify_expr castee cast_sz cast_sg in
456                     (fun _ ->
457                     (let { Types.fst = desired_type2; Types.snd =
458                        castee2 } = eta2522
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 eta2524 = simplify_expr iftrue target_sz target_sg in
513                (fun _ ->
514                (let { Types.fst = desired_true; Types.snd = iftrue1 } =
515                   eta2524
516                 in
517                (fun _ ->
518                (let eta2523 = simplify_expr iffalse target_sz target_sg in
519                  (fun _ ->
520                  (let { Types.fst = desired_false; Types.snd = iffalse1 } =
521                     eta2523
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, e2) ->
576     (fun _ ->
577       match TypeComparison.type_eq_dec ty (Csyntax.typeof e2) with
578       | Types.Inl _ ->
579         (let eta2525 = simplify_expr e2 target_sz target_sg in
580           (fun _ ->
581           (let { Types.fst = desired_type; Types.snd = e3 } = eta2525 in
582           (fun _ -> { Types.fst = desired_type; Types.snd = (Csyntax.Expr
583           ((Csyntax.Ecost (l, e3)), (Csyntax.typeof e3))) })) __)) __
584       | Types.Inr _ ->
585         (let e3 = simplify_inside e2 in
586           (fun _ -> { Types.fst = Bool.False; Types.snd = (Csyntax.Expr
587           ((Csyntax.Ecost (l, e3)), ty)) })) __)) __)) __
588(** val simplify_inside : Csyntax.expr -> Csyntax.expr Types.sig0 **)
589and simplify_inside e1 =
590  (let Csyntax.Expr (ed, ty) = e1 in
591  (fun _ ->
592  (match ed with
593   | Csyntax.Econst_int (x, x0) -> (fun _ -> e1)
594   | Csyntax.Evar x -> (fun _ -> e1)
595   | Csyntax.Ederef e2 ->
596     (fun _ ->
597       (let e3 = simplify_inside e2 in
598         (fun _ -> Csyntax.Expr ((Csyntax.Ederef e3), ty))) __)
599   | Csyntax.Eaddrof e2 ->
600     (fun _ ->
601       (let e3 = simplify_inside e2 in
602         (fun _ -> Csyntax.Expr ((Csyntax.Eaddrof e3), ty))) __)
603   | Csyntax.Eunop (op0, e2) ->
604     (fun _ ->
605       (let e3 = simplify_inside e2 in
606         (fun _ -> Csyntax.Expr ((Csyntax.Eunop (op0, e3)), ty))) __)
607   | Csyntax.Ebinop (op0, 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 (op0, 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 _ -> e1)
620          | Csyntax.Tint (cast_sz, cast_sg) ->
621            (fun _ ->
622              (let eta2526 = simplify_expr castee cast_sz cast_sg in
623                (fun _ ->
624                (let { Types.fst = success; Types.snd = castee1 } = eta2526
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 _ -> e1)
633          | Csyntax.Tarray (x, x0) -> (fun _ -> e1)
634          | Csyntax.Tfunction (x, x0) -> (fun _ -> e1)
635          | Csyntax.Tstruct (x, x0) -> (fun _ -> e1)
636          | Csyntax.Tunion (x, x0) -> (fun _ -> e1)
637          | Csyntax.Tcomp_ptr x -> (fun _ -> e1)) __
638       | Types.Inr _ -> e1)
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 _ -> e1)
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, e2) ->
668     (fun _ ->
669       (let e3 = simplify_inside e2 in
670         (fun _ -> Csyntax.Expr ((Csyntax.Ecost (l, e3)), ty))) __)) __)) __
671
672(** val simplify_e : Csyntax.expr -> Csyntax.expr **)
673let simplify_e e1 =
674  Types.pi1 (simplify_inside e1)
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, e1, es) ->
682  Csyntax.Scall ((Types.option_map simplify_e eo), (simplify_e e1),
683    (List.map simplify_e es))
684| Csyntax.Ssequence (s1, s2) ->
685  Csyntax.Ssequence ((simplify_statement s1), (simplify_statement s2))
686| Csyntax.Sifthenelse (e1, s1, s2) ->
687  Csyntax.Sifthenelse ((simplify_e e1), (simplify_statement s1),
688    (simplify_statement s2))
689| Csyntax.Swhile (e1, s1) ->
690  Csyntax.Swhile ((simplify_e e1), (simplify_statement s1))
691| Csyntax.Sdowhile (e1, s1) ->
692  Csyntax.Sdowhile ((simplify_e e1), (simplify_statement s1))
693| Csyntax.Sfor (s1, e1, s2, s3) ->
694  Csyntax.Sfor ((simplify_statement s1), (simplify_e e1),
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 (e1, ls) ->
700  Csyntax.Sswitch ((simplify_e e1), (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_Type6 :
728    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
729    __ -> __ -> 'a2) -> 'a2 **)
730let rec related_globals_rect_Type6 t ge0 ge' h_mk_related_globals =
731  h_mk_related_globals __ __ __
732
733(** val related_globals_rect_Type7 :
734    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
735    __ -> __ -> 'a2) -> 'a2 **)
736let rec related_globals_rect_Type7 t ge0 ge' h_mk_related_globals =
737  h_mk_related_globals __ __ __
738
739(** val related_globals_rect_Type8 :
740    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
741    __ -> __ -> 'a2) -> 'a2 **)
742let rec related_globals_rect_Type8 t ge0 ge' h_mk_related_globals =
743  h_mk_related_globals __ __ __
744
745(** val related_globals_rect_Type9 :
746    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
747    __ -> __ -> 'a2) -> 'a2 **)
748let rec related_globals_rect_Type9 t ge0 ge' h_mk_related_globals =
749  h_mk_related_globals __ __ __
750
751(** val related_globals_rect_Type10 :
752    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
753    __ -> __ -> 'a2) -> 'a2 **)
754let rec related_globals_rect_Type10 t ge0 ge' h_mk_related_globals =
755  h_mk_related_globals __ __ __
756
757(** val related_globals_rect_Type11 :
758    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
759    __ -> __ -> 'a2) -> 'a2 **)
760let rec related_globals_rect_Type11 t ge0 ge' h_mk_related_globals =
761  h_mk_related_globals __ __ __
762
763(** val related_globals_inv_rect_Type5 :
764    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
765    __ -> __ -> __ -> 'a2) -> 'a2 **)
766let related_globals_inv_rect_Type5 x2 x3 x4 h1 =
767  let hcut = related_globals_rect_Type6 x2 x3 x4 h1 in hcut __
768
769(** val related_globals_inv_rect_Type6 :
770    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
771    __ -> __ -> __ -> 'a2) -> 'a2 **)
772let related_globals_inv_rect_Type6 x2 x3 x4 h1 =
773  let hcut = related_globals_rect_Type8 x2 x3 x4 h1 in hcut __
774
775(** val related_globals_inv_rect_Type7 :
776    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
777    __ -> __ -> __ -> 'a2) -> 'a2 **)
778let related_globals_inv_rect_Type7 x2 x3 x4 h1 =
779  let hcut = related_globals_rect_Type9 x2 x3 x4 h1 in hcut __
780
781(** val related_globals_inv_rect_Type8 :
782    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
783    __ -> __ -> __ -> 'a2) -> 'a2 **)
784let related_globals_inv_rect_Type8 x2 x3 x4 h1 =
785  let hcut = related_globals_rect_Type10 x2 x3 x4 h1 in hcut __
786
787(** val related_globals_inv_rect_Type9 :
788    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> (__ ->
789    __ -> __ -> __ -> 'a2) -> 'a2 **)
790let related_globals_inv_rect_Type9 x2 x3 x4 h1 =
791  let hcut = related_globals_rect_Type11 x2 x3 x4 h1 in hcut __
792
793(** val related_globals_discr0 :
794    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
795let related_globals_discr0 a2 a3 a4 =
796  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
797
798(** val related_globals_jmdiscr0 :
799    ('a1 -> 'a1) -> 'a1 Globalenvs.genv_t -> 'a1 Globalenvs.genv_t -> __ **)
800let related_globals_jmdiscr0 a2 a3 a4 =
801  Logic.eq_rect_Type2 __ (Obj.magic (fun _ dH -> dH __ __ __)) __
802
Note: See TracBrowser for help on using the repository browser.