diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-04-20 07:54:52 +0000 |
commit | 255cee09b71255051c2b40eae0c88bffce1f6f32 (patch) | |
tree | 7951b1b13e8fd5e525b9223e8be0580e83550f55 /backend/CleanupLabelstyping.v | |
parent | 6e5041958df01c56762e90770abd704b95a36e5d (diff) |
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
1- new register allocator (+ live range splitting, spilling&reloading, etc)
based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/CleanupLabelstyping.v')
-rw-r--r-- | backend/CleanupLabelstyping.v | 59 |
1 files changed, 0 insertions, 59 deletions
diff --git a/backend/CleanupLabelstyping.v b/backend/CleanupLabelstyping.v deleted file mode 100644 index 11b516f..0000000 --- a/backend/CleanupLabelstyping.v +++ /dev/null @@ -1,59 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 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. - unfold remove_unused_labels, remove_unused. induction c; simpl. - auto. - rewrite list_fold_right_eq. 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. |