blob: ea9de8684a1482ce4c5ff061a2ffae11b776888c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Type preservation for the CleanupLabels pass *)
Require Import Coqlib.
Require Import Maps.
Require Import Errors.
Require Import AST.
Require Import Op.
Require Import Locations.
Require Import LTLin.
Require Import CleanupLabels.
Require Import LTLintyping.
Lemma in_remove_unused_labels:
forall bto i c, In i (remove_unused_labels bto c) -> In i c.
Proof.
induction c; simpl.
auto.
destruct a; simpl; intuition.
destruct (Labelset.mem l bto); simpl in H; intuition.
Qed.
Lemma wt_transf_function:
forall f,
wt_function f ->
wt_function (transf_function f).
Proof.
intros. inv H. constructor; simpl; auto.
unfold cleanup_labels; red; intros.
apply wt_instrs. eapply in_remove_unused_labels; eauto.
Qed.
Lemma wt_transf_fundef:
forall f,
wt_fundef f ->
wt_fundef (transf_fundef f).
Proof.
induction 1. constructor. constructor. apply wt_transf_function; auto.
Qed.
Lemma program_typing_preserved:
forall p,
wt_program p ->
wt_program (transf_program p).
Proof.
intros; red; intros.
exploit transform_program_function; eauto. intros [f1 [A B]]. subst f.
apply wt_transf_fundef. eapply H; eauto.
Qed.
|
