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

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.