From aaa49526068f528f2233de0dace43549432fba52 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 12 Apr 2008 12:55:21 +0000 Subject: Revu gestion retaddr et link dans Stacking git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@604 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Conventions.v | 41 +++++++++++++++++++---------------------- 1 file changed, 19 insertions(+), 22 deletions(-) (limited to 'backend/Conventions.v') diff --git a/backend/Conventions.v b/backend/Conventions.v index ea7d448e..2ab2ca91 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -710,28 +710,25 @@ 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. +(** Decide whether a tailcall is possible. *) + +Definition tailcall_is_possible (sg: signature) : bool := + let fix tcisp (l: list loc) := + match l with + | nil => true + | R _ :: l' => tcisp l' + | S _ :: l' => false + end + in tcisp (loc_arguments sg). + +Lemma tailcall_is_possible_correct: + forall s, tailcall_is_possible s = true -> tailcall_possible s. +Proof. + intro s. unfold tailcall_is_possible, tailcall_possible. + generalize (loc_arguments s). induction l; simpl; intros. + elim H0. + destruct a. + destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate. Qed. (** ** Location of function parameters *) -- cgit