diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-02 12:42:19 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-09-02 12:42:19 +0000 |
commit | 265fa07b34a813ba9d8249ddad82d71e6002c10d (patch) | |
tree | 45831b1793c7920b10969fc7cf6316c202d78e91 /backend/Allocproof.v | |
parent | 94470fb6a652cb993982269fcb7a0e8319b54488 (diff) | |
download | compcert-265fa07b34a813ba9d8249ddad82d71e6002c10d.tar.gz compcert-265fa07b34a813ba9d8249ddad82d71e6002c10d.zip |
Merge of the reuse-temps branch:
- Reload temporaries are marked as destroyed (set to Vundef) across
operations in the semantics of LTL, LTLin, Linear and Mach,
allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Allocproof.v')
-rw-r--r-- | backend/Allocproof.v | 32 |
1 files changed, 27 insertions, 5 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index d06c26fa..5a5e4c4d 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -235,6 +235,14 @@ Proof. rewrite H0. apply H. auto. eapply regalloc_not_temporary; eauto. Qed. +Lemma agree_undef_temps: + forall live rs ls, + agree live rs ls -> agree live rs (undef_temps ls). +Proof. + intros. apply agree_exten with ls; auto. + intros. apply Locmap.guo; auto. +Qed. + (** If a register is dead, assigning it an arbitrary value in [rs] and leaving [ls] unchanged preserves agreement. (This corresponds to an operation over a dead register in the original program @@ -603,7 +611,11 @@ Proof. (* sub-case: non-redundant move *) econstructor; split. eapply exec_Lop; eauto. simpl. eauto. MatchStates. - rewrite <- H1. eapply agree_move_live; eauto. + rewrite <- H1. set (ls1 := undef_temps ls). + replace (ls (assign arg)) with (ls1 (assign arg)). + eapply agree_move_live; eauto. + unfold ls1. eapply agree_undef_temps; eauto. + unfold ls1. simpl. apply Locmap.guo. eapply regalloc_not_temporary; eauto. (* Not a move *) intros INMO CORR CODE. assert (eval_operation tge sp op (map ls (map assign args)) = Some v). @@ -612,6 +624,7 @@ Proof. eapply agree_eval_regs; eauto. econstructor; split. eapply exec_Lop; eauto. MatchStates. apply agree_assign_live with f env live; auto. + eapply agree_undef_temps; eauto. eapply agree_reg_list_live; eauto. (* Result is not live, instruction turned into a nop *) intro CODE. econstructor; split. eapply exec_Lnop; eauto. @@ -633,6 +646,7 @@ Proof. unfold correct_alloc_instr. intro CORR. MatchStates. eapply agree_assign_live; eauto. + eapply agree_undef_temps; eauto. eapply agree_reg_list_live; eauto. (* dst is dead *) econstructor; split. @@ -650,7 +664,9 @@ Proof. econstructor; split. eapply exec_Lstore; eauto. TranslInstr. rewrite <- ESRC. eauto. - MatchStates. eapply agree_reg_live. eapply agree_reg_list_live. eauto. + MatchStates. + eapply agree_undef_temps; eauto. + eapply agree_reg_live. eapply agree_reg_list_live. eauto. (* Icall *) exploit transl_find_function; eauto. intros [tf [TFIND TF]]. @@ -695,20 +711,26 @@ Proof. eapply agree_eval_regs; eauto. econstructor; split. eapply exec_Lcond_true; eauto. TranslInstr. - MatchStates. eapply agree_reg_list_live. eauto. + MatchStates. + eapply agree_undef_temps; eauto. + eapply agree_reg_list_live. eauto. (* Icond, false *) assert (COND: eval_condition cond (map ls (map assign args)) = Some false). replace (map ls (map assign args)) with (rs##args). auto. eapply agree_eval_regs; eauto. econstructor; split. eapply exec_Lcond_false; eauto. TranslInstr. - MatchStates. eapply agree_reg_list_live. eauto. + MatchStates. + eapply agree_undef_temps; eauto. + eapply agree_reg_list_live. eauto. (* Ijumptable *) assert (rs#arg = ls (assign arg)). apply AG. apply Regset.add_1. auto. econstructor; split. eapply exec_Ljumptable; eauto. TranslInstr. congruence. - MatchStates. eapply list_nth_z_in; eauto. eapply agree_reg_live; eauto. + MatchStates. eapply list_nth_z_in; eauto. + eapply agree_undef_temps; eauto. + eapply agree_reg_live; eauto. (* Ireturn *) econstructor; split. |