diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-30 08:36:16 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-30 08:36:16 +0000 |
commit | 13910458660eeb3cfa88490e1c645f07294252c1 (patch) | |
tree | 6a4a65c70fb573cc43099ff239db26dd3fbce156 /backend/InterfGraph.v | |
parent | ccddcdc4a8aecca88188e3355958f55d44c83400 (diff) | |
download | compcert-13910458660eeb3cfa88490e1c645f07294252c1.tar.gz compcert-13910458660eeb3cfa88490e1c645f07294252c1.zip |
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
Diffstat (limited to 'backend/InterfGraph.v')
-rw-r--r-- | backend/InterfGraph.v | 14 |
1 files 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. |