diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-05-08 07:07:25 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-05-08 07:07:25 +0000 |
commit | c45fc2431ea70e0cb5a80e65d0ac99f91e94693e (patch) | |
tree | dfc11f4507c6ddaab96074382d8406dbc4031f60 /backend/CleanupLabelstyping.v | |
parent | 67e74f6f1a24247bfcd3d6c165a2d6cd45c83b06 (diff) | |
download | compcert-c45fc2431ea70e0cb5a80e65d0ac99f91e94693e.tar.gz compcert-c45fc2431ea70e0cb5a80e65d0ac99f91e94693e.zip |
Added pass CleanupLabels to remove unreferenced labels in a proved way.
ia32/PrintAsm.ml: simplified accordingly; other PrintAsm.ml to be fixed.
ia32/Asm.v: Pmov_ri can undef flags (if translated to xor)
cparser/Ceval.ml: treat ~ in constant exprs
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1647 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/CleanupLabelstyping.v')
-rw-r--r-- | backend/CleanupLabelstyping.v | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/backend/CleanupLabelstyping.v b/backend/CleanupLabelstyping.v new file mode 100644 index 00000000..ea9de868 --- /dev/null +++ b/backend/CleanupLabelstyping.v @@ -0,0 +1,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. |