From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: 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 --- backend/Asmgenproof0.v | 134 +++++++++++++++++++++++++++++++------------------ 1 file changed, 86 insertions(+), 48 deletions(-) (limited to 'backend/Asmgenproof0.v') diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 72de80af..f74fba88 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -80,29 +80,6 @@ Qed. Hint Resolve preg_of_not_SP preg_of_not_PC: asmgen. -Lemma nontemp_diff: - forall r r', - nontemp_preg r = true -> nontemp_preg r' = false -> r <> r'. -Proof. - congruence. -Qed. -Hint Resolve nontemp_diff: asmgen. - -Lemma temporaries_temp_preg: - forall r, In r temporary_regs -> nontemp_preg (preg_of r) = false. -Proof. - assert (List.forallb (fun r => negb (nontemp_preg (preg_of r))) temporary_regs = true) by reflexivity. - rewrite List.forallb_forall in H. intros. generalize (H r H0). - destruct (nontemp_preg (preg_of r)); simpl; congruence. -Qed. - -Lemma nontemp_data_preg: - forall r, nontemp_preg r = true -> data_preg r = true. -Proof. - destruct r; try (destruct i); try (destruct f); simpl; congruence. -Qed. -Hint Resolve nontemp_data_preg: asmgen. - Lemma nextinstr_pc: forall rs, (nextinstr rs)#PC = Val.add rs#PC Vone. Proof. @@ -121,12 +98,6 @@ Proof. intros. apply nextinstr_inv. red; intro; subst; discriminate. Qed. -Lemma nextinstr_inv2: - forall r rs, nontemp_preg r = true -> (nextinstr rs)#r = rs#r. -Proof. - intros. apply nextinstr_inv1; auto with asmgen. -Qed. - Lemma nextinstr_set_preg: forall rs m v, (nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone. @@ -135,6 +106,58 @@ Proof. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_PC. Qed. +Lemma undef_regs_other: + forall r rl rs, + (forall r', In r' rl -> r <> r') -> + undef_regs rl rs r = rs r. +Proof. + induction rl; simpl; intros. auto. + rewrite IHrl by auto. rewrite Pregmap.gso; auto. +Qed. + +Fixpoint preg_notin (r: preg) (rl: list mreg) : Prop := + match rl with + | nil => True + | r1 :: nil => r <> preg_of r1 + | r1 :: rl => r <> preg_of r1 /\ preg_notin r rl + end. + +Remark preg_notin_charact: + forall r rl, + preg_notin r rl <-> (forall mr, In mr rl -> r <> preg_of mr). +Proof. + induction rl; simpl; intros. + tauto. + destruct rl. + simpl. split. intros. intuition congruence. auto. + rewrite IHrl. split. + intros [A B]. intros. destruct H. congruence. auto. + auto. +Qed. + +Lemma undef_regs_other_2: + forall r rl rs, + preg_notin r rl -> + undef_regs (map preg_of rl) rs r = rs r. +Proof. + intros. apply undef_regs_other. intros. + exploit list_in_map_inv; eauto. intros [mr [A B]]. subst. + rewrite preg_notin_charact in H. auto. +Qed. + +Lemma set_pregs_other_2: + forall r rl vl rs, + preg_notin r rl -> + set_regs (map preg_of rl) vl rs r = rs r. +Proof. + induction rl; simpl; intros. + auto. + destruct vl; auto. + assert (r <> preg_of a) by (destruct rl; tauto). + assert (preg_notin r rl) by (destruct rl; simpl; tauto). + rewrite IHrl by auto. apply Pregmap.gso; auto. +Qed. + (** * Agreement between Mach registers and processor registers *) Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree { @@ -224,7 +247,21 @@ Proof. intros. unfold nextinstr. apply agree_set_other. auto. auto. Qed. -Lemma agree_undef_regs: +Lemma agree_set_mregs: + forall sp rl vl vl' ms rs, + agree ms sp rs -> + Val.lessdef_list vl vl' -> + agree (Mach.set_regs rl vl ms) sp (set_regs (map preg_of rl) vl' rs). +Proof. + induction rl; simpl; intros. + auto. + inv H0. auto. apply IHrl; auto. + eapply agree_set_mreg. eexact H. + rewrite Pregmap.gss. auto. + intros. apply Pregmap.gso; auto. +Qed. + +Lemma agree_undef_nondata_regs: forall ms sp rl rs, agree ms sp rs -> (forall r, In r rl -> data_preg r = false) -> @@ -237,31 +274,33 @@ Proof. intros. apply H0; auto. Qed. -Lemma agree_exten_temps: - forall ms sp rs rs', +Lemma agree_undef_regs: + forall ms sp rl rs rs', agree ms sp rs -> - (forall r, nontemp_preg r = true -> rs'#r = rs#r) -> - agree (undef_temps ms) sp rs'. + (forall r', data_preg r' = true -> preg_notin r' rl -> rs'#r' = rs#r') -> + agree (Mach.undef_regs rl ms) sp rs'. Proof. intros. destruct H. split; auto. - rewrite H0; auto. auto. - intros. unfold undef_temps. - destruct (In_dec mreg_eq r temporary_regs). - rewrite Mach.undef_regs_same; auto. - rewrite Mach.undef_regs_other; auto. rewrite H0; auto. - simpl in n. destruct r; auto; intuition. + rewrite <- agree_sp0. apply H0; auto. + rewrite preg_notin_charact. intros. apply not_eq_sym. apply preg_of_not_SP. + intros. destruct (In_dec mreg_eq r rl). + rewrite Mach.undef_regs_same; auto. + rewrite Mach.undef_regs_other; auto. rewrite H0; auto. + apply preg_of_data. + rewrite preg_notin_charact. intros; red; intros. elim n. + exploit preg_of_injective; eauto. congruence. Qed. Lemma agree_set_undef_mreg: - forall ms sp rs r v rs', + forall ms sp rs r v rl rs', agree ms sp rs -> Val.lessdef v (rs'#(preg_of r)) -> - (forall r', nontemp_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v (undef_temps ms)) sp rs'. + (forall r', data_preg r' = true -> r' <> preg_of r -> preg_notin r' rl -> rs'#r' = rs#r') -> + agree (Regmap.set r v (Mach.undef_regs rl ms)) sp rs'. Proof. intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto. - eapply agree_exten_temps; eauto. - intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). + apply agree_undef_regs with rs; auto. + intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of r)). congruence. auto. intros. rewrite Pregmap.gso; auto. Qed. @@ -291,9 +330,7 @@ Proof. exploit Mem.loadv_extends; eauto. intros [v' [A B]]. rewrite (sp_val _ _ _ H) in A. exists v'; split; auto. - destruct ty; econstructor. - reflexivity. assumption. - reflexivity. assumption. + econstructor. eauto. assumption. Qed. Lemma extcall_args_match: @@ -667,6 +704,7 @@ Ltac TailNoLabel := match goal with | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [auto; exact I | TailNoLabel] | [ H: Error _ = OK _ |- _ ] => discriminate + | [ H: assertion_failed = OK _ |- _ ] => discriminate | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabel | [ H: bind _ _ = OK _ |- _ ] => monadInv H; TailNoLabel | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabel -- cgit