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/Conventions.v | 208 +++++--------------------------------------------- 1 file changed, 19 insertions(+), 189 deletions(-) (limited to 'backend/Conventions.v') diff --git a/backend/Conventions.v b/backend/Conventions.v index c11bf47c..abfe4eee 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -22,110 +22,6 @@ Require Export Conventions1. [arch/abi/Conventions1.v]. This file adds various processor-independent definitions and lemmas. *) -(** * Acceptable locations for register allocation *) - -(** The following predicate describes the locations that can be assigned - to an RTL pseudo-register during register allocation: a non-temporary - machine register or a [Local] stack slot are acceptable. *) - -Definition loc_acceptable (l: loc) : Prop := - match l with - | R r => ~(In l temporaries) - | S (Local ofs ty) => ofs >= 0 - | S (Incoming _ _) => False - | S (Outgoing _ _) => False - end. - -Definition locs_acceptable (ll: list loc) : Prop := - forall l, In l ll -> loc_acceptable l. - -Lemma temporaries_not_acceptable: - forall l, loc_acceptable l -> Loc.notin l temporaries. -Proof. - unfold loc_acceptable; destruct l. - simpl. intuition congruence. - destruct s; try contradiction. - intro. simpl. tauto. -Qed. -Hint Resolve temporaries_not_acceptable: locs. - -Lemma locs_acceptable_disj_temporaries: - forall ll, locs_acceptable ll -> Loc.disjoint ll temporaries. -Proof. - intros. apply Loc.notin_disjoint. intros. - 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. - -(** * Additional properties of result and argument locations *) - -(** The result location is not a callee-save register. *) - -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_caller_save s). - generalize (int_callee_save_not_destroyed (loc_result s)). - generalize (float_callee_save_not_destroyed (loc_result s)). - tauto. -Qed. - -(** Callee-save registers do not overlap with argument locations. *) - -Lemma arguments_not_preserved: - forall sig l, - Loc.notin l destroyed_at_call -> loc_acceptable l -> - Loc.notin l (loc_arguments sig). -Proof. - intros. destruct l; red in H0. - apply Loc.reg_notin. red; intros. - exploit Loc.notin_not_in; eauto. eapply arguments_caller_save; eauto. - destruct s; try contradiction. - unfold loc_arguments. apply loc_arguments_rec_notin_local. -Qed. - -(** There is no partial overlap between arguments and acceptable locations. *) - -Lemma no_overlap_arguments: - forall args sg, - locs_acceptable args -> - Loc.no_overlap args (loc_arguments sg). -Proof. - unfold Loc.no_overlap; intros. - generalize (H r H0). - generalize (loc_arguments_acceptable _ _ H1). - destruct s; destruct r; simpl. - intros. case (mreg_eq m0 m); intro. left; congruence. tauto. - intros. right; destruct s; auto. - intros. right. auto. - destruct s; try tauto. destruct s0; tauto. -Qed. - (** ** Location of function parameters *) (** A function finds the values of its parameter in the same locations @@ -135,86 +31,39 @@ Qed. Definition parameter_of_argument (l: loc) : loc := match l with - | S (Outgoing n ty) => S (Incoming n ty) + | S Outgoing n ty => S Incoming n ty | _ => l end. Definition loc_parameters (s: signature) := List.map parameter_of_argument (loc_arguments s). -Lemma loc_parameters_type: - forall sig, List.map Loc.type (loc_parameters sig) = sig.(sig_args). -Proof. - intros. unfold loc_parameters. - rewrite list_map_compose. - rewrite <- loc_arguments_type. - apply list_map_exten. - intros. destruct x; simpl. auto. - 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. - intro; red; intros. - unfold loc_parameters in H. - elim (list_in_map_inv _ _ _ H). intros y [EQ IN]. - generalize (loc_arguments_not_temporaries sig y x2 IN H0). - subst x1. destruct x2. - destruct y; simpl. auto. destruct s; auto. - byContradiction. generalize H0. simpl. NotOrEq. -Qed. - -Lemma no_overlap_parameters: - forall params sg, - locs_acceptable params -> - Loc.no_overlap (loc_parameters sg) params. -Proof. - unfold Loc.no_overlap; intros. - unfold loc_parameters in H0. - elim (list_in_map_inv _ _ _ H0). intros t [EQ IN]. - rewrite EQ. - generalize (loc_arguments_acceptable _ _ IN). - generalize (H s H1). - destruct s; destruct t; simpl. - intros. case (mreg_eq m0 m); intro. left; congruence. tauto. - intros. right; destruct s; simpl; auto. - intros; right; auto. - destruct s; try tauto. destruct s0; try tauto. - intros; simpl. tauto. -Qed. - 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) (loc_parameters sg) -> + In (S Outgoing ofs ty) (loc_arguments sg). Proof. intros. unfold loc_parameters in H. - change (S (Incoming ofs ty)) with (parameter_of_argument (S (Outgoing ofs ty))) 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. destruct x; simpl in A; try discriminate. - destruct s; try contradiction. + destruct sl; try contradiction. inv A. auto. Qed. - (** * Tail calls *) +(** A tail-call is possible for a signature if the corresponding + arguments are all passed in registers. *) + (** 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. + match l with R _ => True | S _ _ _ => False end. (** Decide whether a tailcall is possible. *) @@ -223,7 +72,7 @@ Definition tailcall_is_possible (sg: signature) : bool := match l with | nil => true | R _ :: l' => tcisp l' - | S _ :: l' => false + | S _ _ _ :: l' => false end in tcisp (loc_arguments sg). @@ -237,31 +86,12 @@ Proof. destruct H0. subst l0. auto. apply IHl. auto. auto. discriminate. Qed. -(** * Counting temporaries *) - -(** Given a list [tys] of types representing arguments to an operator, - [arity_ok tys] returns [true] if there are enough temporaries to - reload all arguments into temporaries. *) - -Fixpoint arity_ok_rec (tys: list typ) (itmps ftmps: list mreg) - {struct tys} : bool := - match tys with - | nil => true - | Tint :: ts => - match itmps with - | nil => false - | it1 :: its => arity_ok_rec ts its ftmps - end - | Tfloat :: ts => - match ftmps with - | nil => false - | ft1 :: fts => arity_ok_rec ts itmps fts - end - end. - -Definition arity_ok (tys: list typ) := - arity_ok_rec tys int_temporaries float_temporaries. - - - - +Lemma zero_size_arguments_tailcall_possible: + forall sg, size_arguments sg = 0 -> tailcall_possible sg. +Proof. + intros; red; intros. exploit loc_arguments_acceptable; eauto. + unfold loc_argument_acceptable. + destruct l; intros. auto. destruct sl; try contradiction. destruct H1. + generalize (loc_arguments_bounded _ _ _ H0). + generalize (typesize_pos ty). omega. +Qed. -- cgit