diff options
Diffstat (limited to 'backend/Conventions.v')
-rw-r--r-- | backend/Conventions.v | 48 |
1 files changed, 28 insertions, 20 deletions
diff --git a/backend/Conventions.v b/backend/Conventions.v index 69cdd07d..64a83a58 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -22,6 +22,18 @@ Require Export Conventions1. [arch/abi/Conventions1.v]. This file adds various processor-independent definitions and lemmas. *) +Lemma loc_arguments_acceptable_2: + forall s l, + In l (regs_of_rpairs (loc_arguments s)) -> loc_argument_acceptable l. +Proof. + intros until l. generalize (loc_arguments_acceptable s). generalize (loc_arguments s). + induction l0 as [ | p pl]; simpl; intros. +- contradiction. +- rewrite in_app_iff in H0. destruct H0. + exploit H; eauto. destruct p; simpl in *; intuition congruence. + apply IHpl; auto. +Qed. + (** ** Location of function parameters *) (** A function finds the values of its parameter in the same locations @@ -35,22 +47,25 @@ Definition parameter_of_argument (l: loc) : loc := | _ => l end. -Definition loc_parameters (s: signature) := - List.map parameter_of_argument (loc_arguments s). +Definition loc_parameters (s: signature) : list (rpair loc) := + List.map (map_rpair parameter_of_argument) (loc_arguments s). Lemma incoming_slot_in_parameters: forall ofs ty sg, - In (S Incoming ofs ty) (loc_parameters sg) -> - In (S Outgoing ofs ty) (loc_arguments sg). + In (S Incoming ofs ty) (regs_of_rpairs (loc_parameters sg)) -> + In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)). Proof. intros. - unfold loc_parameters in H. + replace (regs_of_rpairs (loc_parameters sg)) with (List.map parameter_of_argument (regs_of_rpairs (loc_arguments sg))) in H. change (S Incoming ofs ty) with (parameter_of_argument (S Outgoing ofs ty)) in H. exploit list_in_map_inv. eexact H. intros [x [A B]]. simpl in A. - exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable; intros. + exploit loc_arguments_acceptable_2; eauto. unfold loc_argument_acceptable; intros. destruct x; simpl in A; try discriminate. destruct sl; try contradiction. inv A. auto. + unfold loc_parameters. generalize (loc_arguments sg). induction l as [ | p l]; simpl; intros. + auto. + rewrite map_app. f_equal; auto. destruct p; auto. Qed. (** * Tail calls *) @@ -62,34 +77,27 @@ Qed. arguments are all passed in registers. *) Definition tailcall_possible (s: signature) : Prop := - forall l, In l (loc_arguments s) -> + forall l, In l (regs_of_rpairs (loc_arguments s)) -> match l with R _ => True | S _ _ _ => False end. (** 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). + List.forallb + (fun l => match l with R _ => true | S _ _ _ => false end) + (regs_of_rpairs (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. + unfold tailcall_is_possible; intros. rewrite forallb_forall in H. + red; intros. apply H in H0. destruct l; [auto|discriminate]. Qed. Lemma zero_size_arguments_tailcall_possible: forall sg, size_arguments sg = 0 -> tailcall_possible sg. Proof. - intros; red; intros. exploit loc_arguments_acceptable; eauto. + intros; red; intros. exploit loc_arguments_acceptable_2; eauto. unfold loc_argument_acceptable. destruct l; intros. auto. destruct sl; try contradiction. destruct H1. generalize (loc_arguments_bounded _ _ _ H0). |