diff options
Diffstat (limited to 'arm/Conventions1.v')
| -rw-r--r-- | arm/Conventions1.v | 235 |
1 files changed, 44 insertions, 191 deletions
diff --git a/arm/Conventions1.v b/arm/Conventions1.v index e27a9293..abd28b18 100644 --- a/arm/Conventions1.v +++ b/arm/Conventions1.v @@ -14,6 +14,7 @@ machine registers and stack slots. *) Require Import Coqlib. +Require Import Decidableplus. Require Import AST. Require Import Events. Require Import Locations. @@ -33,6 +34,14 @@ Require Archi. of callee- and caller-save registers. *) +Definition is_callee_save (r: mreg): bool := + match r with + | R0 | R1 | R2 | R3 | R12 => false + | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 => true + | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 => false + | F8 | F9 | F10 | F11 | F12 | F13 | F14 | F15 => true + end. + Definition int_caller_save_regs := R0 :: R1 :: R2 :: R3 :: R12 :: nil. @@ -46,171 +55,11 @@ Definition float_callee_save_regs := F8 :: F9 :: F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: nil. Definition destroyed_at_call := - int_caller_save_regs ++ float_caller_save_regs. + List.filter (fun r => negb (is_callee_save r)) all_mregs. Definition dummy_int_reg := R0. (**r Used in [Coloring]. *) Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) -(** The [index_int_callee_save] and [index_float_callee_save] associate - a unique positive integer to callee-save registers. This integer is - used in [Stacking] to determine where to save these registers in - the activation record if they are used by the current function. *) - -Definition index_int_callee_save (r: mreg) := - match r with - | R4 => 0 | R5 => 1 | R6 => 2 | R7 => 3 - | R8 => 4 | R9 => 5 | R10 => 6 | R11 => 7 - | _ => -1 - end. - -Definition index_float_callee_save (r: mreg) := - match r with - | F8 => 0 | F9 => 1 | F10 => 2 | F11 => 3 - | F12 => 4 | F13 => 5 | F14 => 6 | F15 => 7 - | _ => -1 - end. - -Ltac ElimOrEq := - match goal with - | |- (?x = ?y) \/ _ -> _ => - let H := fresh in - (intro H; elim H; clear H; - [intro H; rewrite <- H; clear H | ElimOrEq]) - | |- False -> _ => - let H := fresh in (intro H; contradiction) - end. - -Ltac OrEq := - match goal with - | |- (?x = ?x) \/ _ => left; reflexivity - | |- (?x = ?y) \/ _ => right; OrEq - | |- False => fail - end. - -Ltac NotOrEq := - match goal with - | |- (?x = ?y) \/ _ -> False => - let H := fresh in ( - intro H; elim H; clear H; [intro; discriminate | NotOrEq]) - | |- False -> False => - contradiction - end. - -Lemma index_int_callee_save_pos: - forall r, In r int_callee_save_regs -> index_int_callee_save r >= 0. -Proof. - intro r. simpl; ElimOrEq; unfold index_int_callee_save; omega. -Qed. - -Lemma index_float_callee_save_pos: - forall r, In r float_callee_save_regs -> index_float_callee_save r >= 0. -Proof. - intro r. simpl; ElimOrEq; unfold index_float_callee_save; omega. -Qed. - -Lemma index_int_callee_save_pos2: - forall r, index_int_callee_save r >= 0 -> In r int_callee_save_regs. -Proof. - destruct r; simpl; intro; omegaContradiction || OrEq. -Qed. - -Lemma index_float_callee_save_pos2: - forall r, index_float_callee_save r >= 0 -> In r float_callee_save_regs. -Proof. - destruct r; simpl; intro; omegaContradiction || OrEq. -Qed. - -Lemma index_int_callee_save_inj: - forall r1 r2, - In r1 int_callee_save_regs -> - In r2 int_callee_save_regs -> - r1 <> r2 -> - index_int_callee_save r1 <> index_int_callee_save r2. -Proof. - intros r1 r2. - simpl; ElimOrEq; ElimOrEq; unfold index_int_callee_save; - intros; congruence. -Qed. - -Lemma index_float_callee_save_inj: - forall r1 r2, - In r1 float_callee_save_regs -> - In r2 float_callee_save_regs -> - r1 <> r2 -> - index_float_callee_save r1 <> index_float_callee_save r2. -Proof. - intros r1 r2. - simpl; ElimOrEq; ElimOrEq; unfold index_float_callee_save; - intros; congruence. -Qed. - -(** The following lemmas show that - (temporaries, destroyed at call, integer callee-save, float callee-save) - is a partition of the set of machine registers. *) - -Lemma int_float_callee_save_disjoint: - list_disjoint int_callee_save_regs float_callee_save_regs. -Proof. - red; intros r1 r2. simpl; ElimOrEq; ElimOrEq; discriminate. -Qed. - -Lemma register_classification: - forall r, - In r destroyed_at_call \/ In r int_callee_save_regs \/ In r float_callee_save_regs. -Proof. - destruct r; - try (left; simpl; OrEq); - try (right; left; simpl; OrEq); - try (right; right; simpl; OrEq). -Qed. - - -Lemma int_callee_save_not_destroyed: - forall r, - In r destroyed_at_call -> In r int_callee_save_regs -> False. -Proof. - intros. revert H0 H. simpl. ElimOrEq; NotOrEq. -Qed. - -Lemma float_callee_save_not_destroyed: - forall r, - In r destroyed_at_call -> In r float_callee_save_regs -> False. -Proof. - intros. revert H0 H. simpl. ElimOrEq; NotOrEq. -Qed. - -Lemma int_callee_save_type: - forall r, In r int_callee_save_regs -> mreg_type r = Tany32. -Proof. - intro. simpl; ElimOrEq; reflexivity. -Qed. - -Lemma float_callee_save_type: - forall r, In r float_callee_save_regs -> mreg_type r = Tany64. -Proof. - intro. simpl; ElimOrEq; reflexivity. -Qed. - -Ltac NoRepet := - match goal with - | |- list_norepet nil => - apply list_norepet_nil - | |- list_norepet (?a :: ?b) => - apply list_norepet_cons; [simpl; intuition discriminate | NoRepet] - end. - -Lemma int_callee_save_norepet: - list_norepet int_callee_save_regs. -Proof. - unfold int_callee_save_regs; NoRepet. -Qed. - -Lemma float_callee_save_norepet: - list_norepet float_callee_save_regs. -Proof. - unfold float_callee_save_regs; NoRepet. -Qed. - (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -260,12 +109,12 @@ Qed. Lemma loc_result_caller_save: forall (s: signature) (r: mreg), - In r (loc_result s) -> In r destroyed_at_call. + In r (loc_result s) -> is_callee_save r = false. Proof. intros. assert (r = R0 \/ r = R1 \/ r = F0). unfold loc_result in H. destruct (sig_res s); [destruct t|idtac]; simpl in H; intuition. - destruct H0 as [A | [A | A]]; subst r; simpl; OrEq. + destruct H0 as [A | [A | A]]; subst r; auto. Qed. (** ** Location of function arguments *) @@ -425,8 +274,8 @@ Definition size_arguments (s: signature) : Z := Definition loc_argument_acceptable (l: loc) : Prop := match l with - | R r => In r destroyed_at_call - | S Outgoing ofs ty => ofs >= 0 /\ ty <> Tlong + | R r => is_callee_save r = false + | S Outgoing ofs ty => ofs >= 0 /\ (typealign ty | ofs) | _ => False end. @@ -451,20 +300,20 @@ Remark loc_arguments_hf_charact: In l (loc_arguments_hf tyl ir fr ofs) -> match l with | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= ofs /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1 | S _ _ _ => False end. Proof. assert (INCR: forall l ofs1 ofs2, match l with | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= ofs2 /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= ofs2 /\ typealign ty = 1 | S _ _ _ => False end -> ofs1 <= ofs2 -> match l with | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= ofs1 /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= ofs1 /\ typealign ty = 1 | S _ _ _ => False end). { @@ -477,13 +326,13 @@ Proof. destruct (zlt ir 4); destruct H. subst. left; apply ireg_param_in_params. eapply IHtyl; eauto. - subst. split; [omega | congruence]. + subst. split; [omega | auto]. eapply INCR. eapply IHtyl; eauto. omega. - (* float *) destruct (zlt fr 8); destruct H. subst. right; apply freg_param_in_params. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. congruence. + subst. split. apply Zle_ge. apply align_le. omega. auto. eapply INCR. eapply IHtyl; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega. - (* long *) @@ -493,26 +342,26 @@ Proof. destruct H. subst l; left; apply ireg_param_in_params. destruct H. subst l; left; apply ireg_param_in_params. eapply IHtyl; eauto. - destruct H. subst l; split; [ omega | congruence ]. - destruct H. subst l; split; [ omega | congruence ]. + destruct H. subst l; split; [ omega | auto ]. + destruct H. subst l; split; [ omega | auto ]. eapply INCR. eapply IHtyl; eauto. omega. - (* single *) destruct (zlt fr 8); destruct H. subst. right; apply freg_param_in_params. eapply IHtyl; eauto. - subst. split; [omega | congruence]. + subst. split; [omega | auto]. eapply INCR. eapply IHtyl; eauto. omega. - (* any32 *) destruct (zlt ir 4); destruct H. subst. left; apply ireg_param_in_params. eapply IHtyl; eauto. - subst. split; [omega | congruence]. + subst. split; [omega | auto]. eapply INCR. eapply IHtyl; eauto. omega. - (* any64 *) destruct (zlt fr 8); destruct H. subst. right; apply freg_param_in_params. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. congruence. + subst. split. apply Zle_ge. apply align_le. omega. auto. eapply INCR. eapply IHtyl; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega. Qed. @@ -522,20 +371,20 @@ Remark loc_arguments_sf_charact: In l (loc_arguments_sf tyl ofs) -> match l with | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs /\ typealign ty = 1 | S _ _ _ => False end. Proof. assert (INCR: forall l ofs1 ofs2, match l with | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs2 /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs2 /\ typealign ty = 1 | S _ _ _ => False end -> ofs1 <= ofs2 -> match l with | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs1 /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs1 /\ typealign ty = 1 | S _ _ _ => False end). { @@ -548,7 +397,7 @@ Proof. destruct H. destruct (zlt ofs 0); subst l. left; apply ireg_param_in_params. - split. xomega. congruence. + split. xomega. auto. eapply INCR. eapply IHtyl; eauto. omega. - (* float *) set (ofs' := align ofs 2) in *. @@ -556,7 +405,7 @@ Proof. destruct H. destruct (zlt ofs' 0); subst l. right; apply freg_param_in_params. - split. xomega. congruence. + split. xomega. auto. eapply INCR. eapply IHtyl; eauto. omega. - (* long *) set (ofs' := align ofs 2) in *. @@ -564,23 +413,23 @@ Proof. destruct H. destruct (zlt ofs' 0); subst l. left; apply ireg_param_in_params. - split. xomega. congruence. + split. xomega. auto. destruct H. destruct (zlt ofs' 0); subst l. left; apply ireg_param_in_params. - split. xomega. congruence. + split. xomega. auto. eapply INCR. eapply IHtyl; eauto. omega. - (* single *) destruct H. destruct (zlt ofs 0); subst l. right; apply freg_param_in_params. - split. xomega. congruence. + split. xomega. auto. eapply INCR. eapply IHtyl; eauto. omega. - (* any32 *) destruct H. destruct (zlt ofs 0); subst l. left; apply ireg_param_in_params. - split. xomega. congruence. + split. xomega. auto. eapply INCR. eapply IHtyl; eauto. omega. - (* any64 *) set (ofs' := align ofs 2) in *. @@ -588,7 +437,7 @@ Proof. destruct H. destruct (zlt ofs' 0); subst l. right; apply freg_param_in_params. - split. xomega. congruence. + split. xomega. auto. eapply INCR. eapply IHtyl; eauto. omega. Qed. @@ -597,14 +446,18 @@ Lemma loc_arguments_acceptable: In l (loc_arguments s) -> loc_argument_acceptable l. Proof. unfold loc_arguments; intros. - assert (forall r, In r int_param_regs \/ In r float_param_regs -> In r destroyed_at_call). - { - intros. elim H0; simpl; ElimOrEq; OrEq. - } + assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by decide_goal. + assert (B: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal. + assert (C: forall r, In r int_param_regs \/ In r float_param_regs -> is_callee_save r = false). + { intros. destruct H0; auto. } assert (In l (loc_arguments_sf (sig_args s) (-4)) -> loc_argument_acceptable l). - { intros. red. exploit loc_arguments_sf_charact; eauto. destruct l; auto. } + { intros. red. exploit loc_arguments_sf_charact; eauto. + destruct l as [r | [] ofs ty]; auto. + intros [P Q]. rewrite Q; split. auto. apply Z.divide_1_l. } assert (In l (loc_arguments_hf (sig_args s) 0 0 0) -> loc_argument_acceptable l). - { intros. red. exploit loc_arguments_hf_charact; eauto. destruct l; auto. } + { intros. red. exploit loc_arguments_hf_charact; eauto. + destruct l as [r | [] ofs ty]; auto. + intros [P Q]. rewrite Q; split. auto. apply Z.divide_1_l. } destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto. Qed. |