From 13910458660eeb3cfa88490e1c645f07294252c1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Mar 2010 08:36:16 +0000 Subject: Include targets of preference edges in all_interf_regs. Not needed for correctness, but this way temporaries that have preferences but no interferences do not fall in the default case of Coloring.alloc_of_coloring. This used to create uncoalesced moves esp. on Arm. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1299 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/InterfGraph.v | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/backend/InterfGraph.v b/backend/InterfGraph.v index 8a9dda67..a73e7d71 100644 --- a/backend/InterfGraph.v +++ b/backend/InterfGraph.v @@ -214,11 +214,10 @@ Definition add_intf1 (r1m2: reg * mreg) (u: Regset.t) : Regset.t := Regset.add (fst r1m2) u. Definition all_interf_regs (g: graph) : Regset.t := - SetRegReg.fold add_intf2 - g.(interf_reg_reg) - (SetRegMreg.fold add_intf1 - g.(interf_reg_mreg) - Regset.empty). + let s1 := SetRegMreg.fold add_intf1 g.(interf_reg_mreg) Regset.empty in + let s2 := SetRegMreg.fold add_intf1 g.(pref_reg_mreg) s1 in + let s3 := SetRegReg.fold add_intf2 g.(interf_reg_reg) s2 in + SetRegReg.fold add_intf2 g.(pref_reg_reg) s3. Lemma in_setregreg_fold: forall g r1 r2 u, @@ -287,6 +286,7 @@ Lemma all_interf_regs_correct_1: Regset.In r2 (all_interf_regs g). Proof. intros. unfold all_interf_regs. + apply in_setregreg_fold. right. apply in_setregreg_fold. tauto. Qed. @@ -296,6 +296,8 @@ Lemma all_interf_regs_correct_2: Regset.In r1 (all_interf_regs g). Proof. intros. unfold all_interf_regs. - apply in_setregreg_fold'. eapply in_setregmreg_fold. eauto. + apply in_setregreg_fold'. apply in_setregreg_fold'. + apply in_setregmreg_fold with mr2. right. + apply in_setregmreg_fold with mr2. eauto. Qed. -- cgit