From c45fc2431ea70e0cb5a80e65d0ac99f91e94693e Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 8 May 2011 07:07:25 +0000 Subject: 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 --- backend/CleanupLabelstyping.v | 60 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) create mode 100644 backend/CleanupLabelstyping.v (limited to 'backend/CleanupLabelstyping.v') 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. -- cgit