From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Sep 2010 12:42:19 +0000 Subject: 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 --- backend/Allocproof.v | 32 +++++++++++++++++++++++++++----- 1 file changed, 27 insertions(+), 5 deletions(-) (limited to 'backend/Allocproof.v') diff --git a/backend/Allocproof.v b/backend/Allocproof.v index d06c26f..5a5e4c4 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. -- cgit v1.2.3