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/Linearizetyping.v | |
parent | 6e5041958df01c56762e90770abd704b95a36e5d (diff) | |
download | compcert-255cee09b71255051c2b40eae0c88bffce1f6f32.tar.gz compcert-255cee09b71255051c2b40eae0c88bffce1f6f32.zip |
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/Linearizetyping.v')
-rw-r--r-- | backend/Linearizetyping.v | 112 |
1 files changed, 0 insertions, 112 deletions
diff --git a/backend/Linearizetyping.v b/backend/Linearizetyping.v deleted file mode 100644 index b4e25de7..00000000 --- a/backend/Linearizetyping.v +++ /dev/null @@ -1,112 +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 Linearize pass *) - -Require Import Coqlib. -Require Import Maps. -Require Import Errors. -Require Import AST. -Require Import Op. -Require Import Locations. -Require Import LTL. -Require Import LTLtyping. -Require Import LTLin. -Require Import Linearize. -Require Import LTLintyping. -Require Import Conventions. - -(** * Type preservation for the linearization pass *) - -Lemma wt_add_instr: - forall f i k, wt_instr f i -> wt_code f k -> wt_code f (i :: k). -Proof. - intros; red; intros. elim H1; intro. subst i0; auto. auto. -Qed. - -Lemma wt_add_branch: - forall f s k, wt_code f k -> wt_code f (add_branch s k). -Proof. - intros; unfold add_branch. destruct (starts_with s k). - auto. apply wt_add_instr; auto. constructor. -Qed. - -Lemma wt_linearize_instr: - forall f instr, - LTLtyping.wt_instr f instr -> - forall k, - wt_code f.(LTL.fn_sig) k -> - wt_code f.(LTL.fn_sig) (linearize_instr instr k). -Proof. - induction 1; simpl; intros. - apply wt_add_branch; auto. - apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. - apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. - apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. - apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. - apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. - apply wt_add_instr. constructor; auto. auto. - apply wt_add_instr. constructor; auto. apply wt_add_branch; auto. - destruct (starts_with s1 k); apply wt_add_instr. - constructor; auto. rewrite H. destruct cond; auto. - apply wt_add_branch; auto. - constructor; auto. apply wt_add_branch; auto. - apply wt_add_instr. constructor; auto. auto. - apply wt_add_instr. constructor; auto. auto. -Qed. - -Lemma wt_linearize_body: - forall f, - (forall pc instr, - f.(LTL.fn_code)!pc = Some instr -> LTLtyping.wt_instr f instr) -> - forall enum, - wt_code f.(LTL.fn_sig) (linearize_body f enum). -Proof. - unfold linearize_body; induction enum; rewrite list_fold_right_eq. - red; simpl; intros; contradiction. - unfold linearize_node. caseEq ((LTL.fn_code f)!a); intros. - apply wt_add_instr. constructor. apply wt_linearize_instr; eauto with coqlib. - auto. -Qed. - -Lemma wt_transf_function: - forall f tf, - LTLtyping.wt_function f -> - transf_function f = OK tf -> - wt_function tf. -Proof. - intros. inv H. monadInv H0. constructor; auto. - simpl. apply wt_add_branch. - apply wt_linearize_body. auto. -Qed. - -Lemma wt_transf_fundef: - forall f tf, - LTLtyping.wt_fundef f -> - transf_fundef f = OK tf -> - wt_fundef tf. -Proof. - induction 1; intros. monadInv H. constructor. - monadInv H0. constructor; eapply wt_transf_function; eauto. -Qed. - -Lemma program_typing_preserved: - forall (p: LTL.program) (tp: LTLin.program), - LTLtyping.wt_program p -> - transf_program p = OK tp -> - LTLintyping.wt_program tp. -Proof. - intros; red; intros. - generalize (transform_partial_program_function transf_fundef _ _ _ H0 H1). - intros [f0 [IN TR]]. - eapply wt_transf_fundef; eauto. -Qed. |