From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: Fusion des modifications faites sur les branches "tailcalls" et "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Conventions.v | 281 +++++++++++++++++++++++++++++++++++--------------- 1 file changed, 196 insertions(+), 85 deletions(-) (limited to 'backend/Conventions.v') diff --git a/backend/Conventions.v b/backend/Conventions.v index d621e7c0..9d005b34 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -247,6 +247,31 @@ Proof. apply temporaries_not_acceptable. auto. Qed. +Lemma loc_acceptable_noteq_diff: + forall l1 l2, + loc_acceptable l1 -> l1 <> l2 -> Loc.diff l1 l2. +Proof. + unfold loc_acceptable, Loc.diff; destruct l1; destruct l2; + try (destruct s); try (destruct s0); intros; auto; try congruence. + case (zeq z z0); intro. + compare t t0; intro. + subst z0; subst t0; tauto. + tauto. tauto. + contradiction. contradiction. +Qed. + +Lemma loc_acceptable_notin_notin: + forall r ll, + loc_acceptable r -> + ~(In r ll) -> Loc.notin r ll. +Proof. + induction ll; simpl; intros. + auto. + split. apply loc_acceptable_noteq_diff. assumption. + apply sym_not_equal. tauto. + apply IHll. assumption. tauto. +Qed. + (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -292,9 +317,20 @@ Proof. reflexivity. Qed. -(** The result location is a caller-save register. *) +(** The result location is acceptable. *) Lemma loc_result_acceptable: + forall sig, loc_acceptable (R (loc_result sig)). +Proof. + intros. unfold loc_acceptable. red. + unfold loc_result. destruct (sig_res sig). + destruct t; simpl; NotOrEq. + simpl; NotOrEq. +Qed. + +(** The result location is a caller-save register. *) + +Lemma loc_result_caller_save: forall (s: signature), In (R (loc_result s)) destroyed_at_call. Proof. intros; unfold loc_result. @@ -309,7 +345,7 @@ Lemma loc_result_not_callee_save: forall (s: signature), ~(In (loc_result s) int_callee_save_regs \/ In (loc_result s) float_callee_save_regs). Proof. - intros. generalize (loc_result_acceptable s). + intros. generalize (loc_result_caller_save s). generalize (int_callee_save_not_destroyed (loc_result s)). generalize (float_callee_save_not_destroyed (loc_result s)). tauto. @@ -340,16 +376,18 @@ Fixpoint loc_arguments_rec | nil => nil | Tint :: tys => match iregl with - | nil => S (Outgoing ofs Tint) - | ireg :: _ => R ireg - end :: - loc_arguments_rec tys (list_drop1 iregl) fregl (ofs + 1) + | nil => + S (Outgoing ofs Tint) :: loc_arguments_rec tys nil fregl (ofs + 1) + | ireg :: iregs => + R ireg :: loc_arguments_rec tys iregs fregl ofs + end | Tfloat :: tys => match fregl with - | nil => S (Outgoing ofs Tfloat) - | freg :: _ => R freg - end :: - loc_arguments_rec tys (list_drop2 iregl) (list_drop1 fregl) (ofs + 2) + | nil => + S (Outgoing ofs Tfloat) :: loc_arguments_rec tys iregl nil (ofs + 2) + | freg :: fregs => + R freg :: loc_arguments_rec tys (list_drop2 iregl) fregs ofs + end end. Definition int_param_regs := @@ -361,28 +399,45 @@ Definition float_param_regs := when calling a function with signature [s]. *) Definition loc_arguments (s: signature) : list loc := - loc_arguments_rec s.(sig_args) int_param_regs float_param_regs 6. + loc_arguments_rec s.(sig_args) int_param_regs float_param_regs 14. (** [size_arguments s] returns the number of [Outgoing] slots used to call a function with signature [s]. *) -Fixpoint size_arguments_rec (tyl: list typ) : Z := +Fixpoint size_arguments_rec + (tyl: list typ) (iregl: list mreg) (fregl: list mreg) + (ofs: Z) {struct tyl} : Z := match tyl with - | nil => 6 - | Tint :: tys => 1 + size_arguments_rec tys - | Tfloat :: tys => 2 + size_arguments_rec tys + | nil => ofs + | Tint :: tys => + match iregl with + | nil => size_arguments_rec tys nil fregl (ofs + 1) + | ireg :: iregs => size_arguments_rec tys iregs fregl ofs + end + | Tfloat :: tys => + match fregl with + | nil => size_arguments_rec tys iregl nil (ofs + 2) + | freg :: fregs => size_arguments_rec tys (list_drop2 iregl) fregs ofs + end end. Definition size_arguments (s: signature) : Z := - size_arguments_rec s.(sig_args). + size_arguments_rec s.(sig_args) int_param_regs float_param_regs 14. + +(** A tail-call is possible for a signature if the corresponding + arguments are all passed in registers. *) + +Definition tailcall_possible (s: signature) : Prop := + forall l, In l (loc_arguments s) -> + match l with R _ => True | S _ => False end. (** Argument locations are either non-temporary registers or [Outgoing] - stack slots at offset 6 or more. *) + stack slots at offset 14 or more. *) Definition loc_argument_acceptable (l: loc) : Prop := match l with | R r => ~(In l temporaries) - | S (Outgoing ofs ty) => ofs >= 6 + | S (Outgoing ofs ty) => ofs >= 14 | _ => False end. @@ -397,16 +452,18 @@ Remark loc_arguments_rec_charact: Proof. induction tyl; simpl loc_arguments_rec; intros. elim H. - destruct a; elim H; intros. - destruct iregl; subst l. omega. left; auto with coqlib. - generalize (IHtyl _ _ _ _ H0). - destruct l. intros [A|B]. left; apply list_drop1_incl; auto. tauto. - destruct s; try contradiction. omega. - destruct fregl; subst l. omega. right; auto with coqlib. - generalize (IHtyl _ _ _ _ H0). - destruct l. intros [A|B]. left; apply list_drop2_incl; auto. - right; apply list_drop1_incl; auto. - destruct s; try contradiction. omega. + destruct a. + destruct iregl; elim H; intro. + subst l. omega. + generalize (IHtyl _ _ _ _ H0). destruct l; auto. destruct s; auto. omega. + subst l. auto with coqlib. + generalize (IHtyl _ _ _ _ H0). destruct l; auto. simpl; intuition. + destruct fregl; elim H; intro. + subst l. omega. + generalize (IHtyl _ _ _ _ H0). destruct l; auto. destruct s; auto. omega. + subst l. auto with coqlib. + generalize (IHtyl _ _ _ _ H0). destruct l; auto. + intros [A|B]. left; apply list_drop2_incl; auto. right; auto with coqlib. Qed. Lemma loc_arguments_acceptable: @@ -432,12 +489,15 @@ Remark loc_arguments_rec_notin_reg: Proof. induction tyl; simpl; intros. auto. - destruct a; simpl; split. - destruct iregl. auto. red; intro; subst m. apply H. auto with coqlib. - apply IHtyl. red; intro. apply H. apply list_drop1_incl; auto. auto. - destruct fregl. auto. red; intro; subst m. apply H0. auto with coqlib. - apply IHtyl. red; intro. apply H. apply list_drop2_incl; auto. - red; intro. apply H0. apply list_drop1_incl; auto. + destruct a. + destruct iregl; simpl. auto. + simpl in H. split. apply sym_not_equal. tauto. + apply IHtyl. tauto. tauto. + destruct fregl; simpl. auto. + simpl in H0. split. apply sym_not_equal. tauto. + apply IHtyl. + red; intro. apply H. apply list_drop2_incl. auto. + tauto. Qed. Remark loc_arguments_rec_notin_local: @@ -446,11 +506,9 @@ Remark loc_arguments_rec_notin_local: Proof. induction tyl; simpl; intros. auto. - destruct a; simpl; split. - destruct iregl. auto. auto. - apply IHtyl. - destruct fregl. auto. auto. - apply IHtyl. + destruct a. + destruct iregl; simpl; auto. + destruct fregl; simpl; auto. Qed. Remark loc_arguments_rec_notin_outgoing: @@ -460,11 +518,13 @@ Remark loc_arguments_rec_notin_outgoing: Proof. induction tyl; simpl; intros. auto. - destruct a; simpl; split. - destruct iregl. omega. auto. - apply IHtyl. omega. - destruct fregl. omega. auto. - apply IHtyl. omega. + destruct a. + destruct iregl; simpl. + split. omega. eapply IHtyl. omega. + auto. + destruct fregl; simpl. + split. omega. eapply IHtyl. omega. + auto. Qed. Lemma loc_arguments_norepet: @@ -477,21 +537,21 @@ Proof. Loc.norepet (loc_arguments_rec tyl iregl fregl ofs)). induction tyl; simpl; intros. constructor. - destruct a; constructor. - destruct iregl. - apply loc_arguments_rec_notin_outgoing. simpl; omega. - apply loc_arguments_rec_notin_reg. simpl. inversion H. auto. + destruct a. + destruct iregl; constructor. + apply loc_arguments_rec_notin_outgoing. simpl; omega. auto. + apply loc_arguments_rec_notin_reg. inversion H. auto. apply list_disjoint_notin with (m :: iregl); auto with coqlib. - apply IHtyl. apply list_drop1_norepet; auto. auto. - red; intros. apply H1. apply list_drop1_incl; auto. auto. - destruct fregl. - apply loc_arguments_rec_notin_outgoing. simpl; omega. - apply loc_arguments_rec_notin_reg. simpl. + apply IHtyl. inv H; auto. auto. + eapply list_disjoint_cons_left; eauto. + destruct fregl; constructor. + apply loc_arguments_rec_notin_outgoing. simpl; omega. auto. + apply loc_arguments_rec_notin_reg. red; intro. apply (H1 m m). apply list_drop2_incl; auto. - auto with coqlib. auto. - simpl. inversion H0. auto. - apply IHtyl. apply list_drop2_norepet; auto. apply list_drop1_norepet; auto. - red; intros. apply H1. apply list_drop2_incl; auto. apply list_drop1_incl; auto. + auto with coqlib. auto. inv H0; auto. + apply IHtyl. apply list_drop2_norepet; auto. + inv H0; auto. + red; intros. apply H1. apply list_drop2_incl; auto. auto with coqlib. intro. unfold loc_arguments. apply H. unfold int_param_regs. NoRepet. @@ -501,32 +561,42 @@ Qed. (** The offsets of [Outgoing] arguments are below [size_arguments s]. *) +Remark size_arguments_rec_above: + forall tyl iregl fregl ofs0, + ofs0 <= size_arguments_rec tyl iregl fregl ofs0. +Proof. + induction tyl; simpl; intros. + omega. + destruct a. + destruct iregl. apply Zle_trans with (ofs0 + 1); auto; omega. auto. + destruct fregl. apply Zle_trans with (ofs0 + 2); auto; omega. auto. +Qed. + +Lemma size_arguments_above: + forall s, size_arguments s >= 14. +Proof. + intros; unfold size_arguments. apply Zle_ge. + apply size_arguments_rec_above. +Qed. + Lemma loc_arguments_bounded: forall (s: signature) (ofs: Z) (ty: typ), In (S (Outgoing ofs ty)) (loc_arguments s) -> ofs + typesize ty <= size_arguments s. Proof. intros. - assert (forall tyl, size_arguments_rec tyl >= 6). - induction tyl; unfold size_arguments_rec; fold size_arguments_rec; intros. - omega. - destruct a; omega. assert (forall tyl iregl fregl ofs0, In (S (Outgoing ofs ty)) (loc_arguments_rec tyl iregl fregl ofs0) -> - ofs + typesize ty <= size_arguments_rec tyl + ofs0 - 6). - induction tyl; simpl loc_arguments_rec; intros. - elim H1. - unfold size_arguments_rec; fold size_arguments_rec. - destruct a. - elim H1; intro. destruct iregl; simplify_eq H2; intros. - subst ty; subst ofs. generalize (H0 tyl). simpl typesize. omega. - generalize (IHtyl _ _ _ H2). omega. - elim H1; intro. destruct fregl; simplify_eq H2; intros. - subst ty; subst ofs. generalize (H0 tyl). simpl typesize. omega. - generalize (IHtyl _ _ _ H2). omega. - replace (size_arguments s) with (size_arguments s + 6 - 6). - unfold size_arguments. eapply H1. unfold loc_arguments in H. eauto. - omega. + ofs + typesize ty <= size_arguments_rec tyl iregl fregl ofs0). + induction tyl; simpl; intros. + elim H0. + destruct a. destruct iregl; elim H0; intro. + inv H1. simpl. apply size_arguments_rec_above. auto. + discriminate. auto. + destruct fregl; elim H0; intro. + inv H1. simpl. apply size_arguments_rec_above. auto. + discriminate. auto. + unfold size_arguments. eapply H0. unfold loc_arguments in H. eauto. Qed. (** Temporary registers do not overlap with argument locations. *) @@ -543,6 +613,18 @@ Proof. Qed. Hint Resolve loc_arguments_not_temporaries: locs. +(** Argument registers are caller-save. *) + +Lemma arguments_caller_save: + forall sig r, + In (R r) (loc_arguments sig) -> In (R r) destroyed_at_call. +Proof. + unfold loc_arguments; intros. + elim (loc_arguments_rec_charact _ _ _ _ _ H); simpl. + ElimOrEq; intuition. + ElimOrEq; intuition. +Qed. + (** Callee-save registers do not overlap with argument locations. *) Lemma arguments_not_preserved: @@ -571,7 +653,9 @@ Proof. List.length (loc_arguments_rec tyl iregl fregl ofs) = List.length tyl). induction tyl; simpl; intros. auto. - destruct a; simpl; decEq; auto. + destruct a. + destruct iregl; simpl; decEq; auto. + destruct fregl; simpl; decEq; auto. intros. unfold loc_arguments. auto. Qed. @@ -586,14 +670,10 @@ Proof. List.map Loc.type (loc_arguments_rec tyl iregl fregl ofs) = tyl). induction tyl; simpl; intros. auto. - destruct a; simpl; apply (f_equal2 (@cons typ)). - destruct iregl. reflexivity. simpl. apply H. auto with coqlib. - apply IHtyl. - intros. apply H. apply list_drop1_incl. auto. auto. - destruct fregl. reflexivity. simpl. apply H0. auto with coqlib. - apply IHtyl. - intros. apply H. apply list_drop2_incl. auto. - intros. apply H0. apply list_drop1_incl. auto. + destruct a; [destruct iregl|destruct fregl]; simpl; + f_equal; eauto with coqlib. + apply IHtyl. intros. apply H. apply list_drop2_incl; auto. + eauto with coqlib. intros. unfold loc_arguments. apply H. intro; simpl. ElimOrEq; reflexivity. @@ -618,6 +698,30 @@ Proof. destruct s; try tauto. destruct s0; tauto. Qed. +(** A tailcall is possible if and only if the size of arguments is 14. *) + +Lemma tailcall_possible_size: + forall s, tailcall_possible s <-> size_arguments s = 14. +Proof. + intro; split; intro. + assert (forall tyl iregl fregl ofs, + (forall l, In l (loc_arguments_rec tyl iregl fregl ofs) -> + match l with R _ => True | S _ => False end) -> + size_arguments_rec tyl iregl fregl ofs = ofs). + induction tyl; simpl; intros. + auto. + destruct a. destruct iregl. elim (H0 _ (in_eq _ _)). + apply IHtyl; intros. apply H0. auto with coqlib. + destruct fregl. elim (H0 _ (in_eq _ _)). + apply IHtyl; intros. apply H0. auto with coqlib. + unfold size_arguments. apply H0. assumption. + red; intros. + generalize (loc_arguments_acceptable s l H0). + destruct l; simpl. auto. destruct s0; intro; auto. + generalize (loc_arguments_bounded _ _ _ H0). + generalize (typesize_pos t). omega. +Qed. + (** ** Location of function parameters *) (** A function finds the values of its parameter in the same locations @@ -645,6 +749,13 @@ Proof. destruct s; reflexivity. Qed. +Lemma loc_parameters_length: + forall sg, List.length (loc_parameters sg) = List.length sg.(sig_args). +Proof. + intros. unfold loc_parameters. rewrite list_length_map. + apply loc_arguments_length. +Qed. + Lemma loc_parameters_not_temporaries: forall sig, Loc.disjoint (loc_parameters sig) temporaries. Proof. @@ -676,7 +787,7 @@ Proof. intros; simpl. tauto. Qed. -(** ** Location of argument and result of dynamic allocation *) +(** ** Location of argument and result for dynamic memory allocation *) Definition loc_alloc_argument := R3. Definition loc_alloc_result := R3. -- cgit