From dc4bed2cf06f46687225275131f411c86c773598 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 21 Dec 2008 13:32:24 +0000 Subject: Revised back-end so that only 2 integer registers are reserved for reloading. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@925 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Reloadtyping.v | 63 +++++++++++++++++++++++++++++++++----------------- 1 file changed, 42 insertions(+), 21 deletions(-) (limited to 'backend/Reloadtyping.v') diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index 2edb482..e531c54 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -186,37 +186,38 @@ Hint Resolve wt_reg_for: reloadty. Lemma wt_regs_for_rec: forall locs itmps ftmps, - (List.length locs <= List.length itmps)%nat -> - (List.length locs <= List.length ftmps)%nat -> + enough_temporaries_rec locs itmps ftmps = true -> (forall r, In r itmps -> mreg_type r = Tint) -> (forall r, In r ftmps -> mreg_type r = Tfloat) -> List.map mreg_type (regs_for_rec locs itmps ftmps) = List.map Loc.type locs. Proof. induction locs; intros. simpl. auto. - destruct itmps; simpl in H. omegaContradiction. - destruct ftmps; simpl in H0. omegaContradiction. - simpl. apply (f_equal2 (@cons typ)). - destruct a. reflexivity. simpl. case (slot_type s). - apply H1; apply in_eq. apply H2; apply in_eq. - apply IHlocs. omega. omega. - intros; apply H1; apply in_cons; auto. - intros; apply H2; apply in_cons; auto. + simpl in H. simpl. + destruct a. + simpl. decEq. eauto. + caseEq (slot_type s); intro SLOTTYPE; rewrite SLOTTYPE in H. + destruct itmps. discriminate. simpl. decEq. + rewrite SLOTTYPE. auto with coqlib. + apply IHlocs; auto with coqlib. + destruct ftmps. discriminate. simpl. decEq. + rewrite SLOTTYPE. auto with coqlib. + apply IHlocs; auto with coqlib. Qed. Lemma wt_regs_for: forall locs, - (List.length locs <= 3)%nat -> + enough_temporaries locs = true -> List.map mreg_type (regs_for locs) = List.map Loc.type locs. Proof. intros. unfold regs_for. apply wt_regs_for_rec. - simpl. auto. simpl. auto. + auto. simpl; intros; intuition; subst r; reflexivity. simpl; intros; intuition; subst r; reflexivity. Qed. Hint Resolve wt_regs_for: reloadty. -Hint Resolve length_op_args length_addr_args length_cond_args: reloadty. +Hint Resolve enough_temporaries_op_args enough_temporaries_cond enough_temporaries_addr: reloadty. Hint Extern 4 (_ = _) => congruence : reloadty. @@ -240,35 +241,55 @@ Proof. assert (mreg_type (reg_for dst) = Loc.type dst). eauto with reloadty. auto with reloadty. - caseEq (regs_for (src :: args)); intros. - red; simpl; tauto. + caseEq (enough_temporaries (src :: args)); intro ENOUGH. + caseEq (regs_for (src :: args)); intros. auto. assert (map mreg_type (regs_for (src :: args)) = map Loc.type (src :: args)). - apply wt_regs_for. simpl. apply le_n_S. eauto with reloadty. + apply wt_regs_for. auto. rewrite H in H5. injection H5; intros. auto with reloadty. + apply wt_add_reloads; auto with reloadty. + symmetry. apply wt_regs_for. eauto with reloadty. + assert (op_for_binary_addressing addr <> Omove). + unfold op_for_binary_addressing; destruct addr; congruence. + assert (type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint)). + apply type_op_for_binary_addressing. + rewrite <- H1. rewrite list_length_map. + eapply not_enough_temporaries_length; eauto. + apply wt_code_cons. + constructor; auto. rewrite H5. decEq. rewrite <- H1. eauto with reloadty. + apply wt_add_reload; auto with reloadty. + apply wt_code_cons; auto. constructor. reflexivity. + rewrite <- H2. eauto with reloadty. assert (locs_valid (transf_function f) (loc_arguments sig)). red; intros. generalize (loc_arguments_acceptable sig l H). destruct l; simpl; auto. destruct s; simpl; intuition. assert (locs_writable (loc_arguments sig)). - red; intros. generalize (loc_arguments_acceptable sig l H7). + red; intros. generalize (loc_arguments_acceptable sig l H6). destruct l; simpl; auto. destruct s; simpl; intuition. assert (map Loc.type args = map Loc.type (loc_arguments sig)). rewrite loc_arguments_type; auto. assert (Loc.type res = mreg_type (loc_result sig)). - rewrite H3. unfold loc_result. + rewrite H2. unfold loc_result. unfold proj_sig_res. destruct (sig_res sig); auto. destruct t; auto. - destruct ros; auto 10 with reloadty. + destruct ros. + destruct H3 as [A [B C]]. + apply wt_parallel_move; eauto with reloadty. + apply wt_add_reload; eauto with reloadty. + apply wt_code_cons; eauto with reloadty. + constructor. rewrite <- A. auto with reloadty. + auto with reloadty. assert (locs_valid (transf_function f) (loc_arguments sig)). red; intros. generalize (loc_arguments_acceptable sig l H). destruct l; simpl; auto. destruct s; simpl; intuition. assert (locs_writable (loc_arguments sig)). - red; intros. generalize (loc_arguments_acceptable sig l H7). + red; intros. generalize (loc_arguments_acceptable sig l H6). destruct l; simpl; auto. destruct s; simpl; intuition. assert (map Loc.type args = map Loc.type (loc_arguments sig)). rewrite loc_arguments_type; auto. - destruct ros; auto 10 with reloadty. + destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty. + auto 10 with reloadty. assert (map mreg_type (regs_for args) = map Loc.type args). eauto with reloadty. -- cgit v1.2.3