diff options
Diffstat (limited to 'backend/Alloctyping.v')
| -rw-r--r-- | backend/Alloctyping.v | 516 |
1 files changed, 71 insertions, 445 deletions
diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v index 4c4c4f7..c0abf0d 100644 --- a/backend/Alloctyping.v +++ b/backend/Alloctyping.v @@ -2,6 +2,7 @@ Require Import Coqlib. Require Import Maps. +Require Import Errors. Require Import AST. Require Import Op. Require Import Registers. @@ -15,7 +16,6 @@ Require Import Allocproof. Require Import RTLtyping. Require Import LTLtyping. Require Import Conventions. -Require Import Parallelmove. (** This file proves that register allocation (the translation from RTL to LTL defined in file [Allocation]) preserves typing: @@ -30,9 +30,10 @@ Variable live: PMap.t Regset.t. Variable alloc: reg -> loc. Variable tf: LTL.function. -Hypothesis TYPE_RTL: type_function f = Some env. +Hypothesis TYPE_RTL: type_function f = OK env. +Hypothesis LIVE: analyze f = Some live. Hypothesis ALLOC: regalloc f live (live0 f live) env = Some alloc. -Hypothesis TRANSL: transf_function f = Some tf. +Hypothesis TRANSL: transf_function f = OK tf. Lemma wt_rtl_function: RTLtyping.wt_function f env. Proof. @@ -51,473 +52,90 @@ Proof. intros. symmetry. apply alloc_type. Qed. -(** [loc_read_ok l] states whether location [l] is well-formed in an - argument context (for reading). *) - -Definition loc_read_ok (l: loc) : Prop := - match l with R r => True | S s => slot_bounded tf s end. - -(** [loc_write_ok l] states whether location [l] is well-formed in a - result context (for writing). *) - -Definition loc_write_ok (l: loc) : Prop := - match l with - | R r => True - | S (Incoming _ _) => False - | S s => slot_bounded tf s end. - -Definition locs_read_ok (ll: list loc) : Prop := - forall l, In l ll -> loc_read_ok l. - -Definition locs_write_ok (ll: list loc) : Prop := - forall l, In l ll -> loc_write_ok l. - -Remark loc_write_ok_read_ok: - forall l, loc_write_ok l -> loc_read_ok l. -Proof. - destruct l; simpl. auto. - destruct s; tauto. -Qed. -Hint Resolve loc_write_ok_read_ok: allocty. - -Remark locs_write_ok_read_ok: - forall ll, locs_write_ok ll -> locs_read_ok ll. -Proof. - unfold locs_write_ok, locs_read_ok. auto with allocty. -Qed. -Hint Resolve locs_write_ok_read_ok: allocty. - -Lemma alloc_write_ok: - forall r, loc_write_ok (alloc r). +Lemma alloc_acceptable: + forall r, loc_acceptable (alloc r). Proof. - intros. generalize (regalloc_acceptable _ _ _ _ _ r ALLOC). - destruct (alloc r); simpl. auto. - destruct s; try contradiction. simpl. omega. + intros. eapply regalloc_acceptable; eauto. Qed. -Hint Resolve alloc_write_ok: allocty. -Lemma allocs_write_ok: - forall rl, locs_write_ok (List.map alloc rl). +Lemma allocs_acceptable: + forall rl, locs_acceptable (List.map alloc rl). Proof. - intros; red; intros. - generalize (list_in_map_inv _ _ _ H). intros [r [EQ IN]]. - subst l. auto with allocty. + intros. eapply regsalloc_acceptable; eauto. Qed. -Hint Resolve allocs_write_ok: allocty. - -(** * Typing LTL constructors *) - -(** We show that the LTL constructor functions defined in [Allocation] - generate well-typed LTL basic blocks, given sufficient typing - and well-formedness hypotheses over the locations involved. *) -Lemma wt_add_reload: - forall src dst k, - loc_read_ok src -> - Loc.type src = mreg_type dst -> - wt_block tf k -> - wt_block tf (add_reload src dst k). +Remark transf_unroll: + tf = transf_fun f live alloc. Proof. - intros. unfold add_reload. destruct src. - case (mreg_eq m dst); intro. auto. apply wt_Bopmove. exact H0. auto. - apply wt_Bgetstack. exact H0. exact H. auto. + generalize TRANSL. unfold transf_function. + rewrite TYPE_RTL. rewrite LIVE. rewrite ALLOC. congruence. Qed. -Lemma wt_add_spill: - forall src dst k, - loc_write_ok dst -> - mreg_type src = Loc.type dst -> - wt_block tf k -> - wt_block tf (add_spill src dst k). +Lemma valid_successor_transf: + forall s, + RTLtyping.valid_successor f s -> + LTLtyping.valid_successor tf s. Proof. - intros. unfold add_spill. destruct dst. - case (mreg_eq src m); intro. auto. - apply wt_Bopmove. exact H0. auto. - apply wt_Bsetstack. generalize H. simpl. destruct s; auto. - symmetry. exact H0. generalize H. simpl. destruct s; auto. contradiction. - auto. -Qed. + unfold RTLtyping.valid_successor, LTLtyping.valid_successor. + intros s [i AT]. + rewrite transf_unroll; simpl. rewrite PTree.gmap. + rewrite AT. exists (transf_instr f live alloc s i). auto. +Qed. -Lemma wt_add_reloads: - forall srcs dsts k, - locs_read_ok srcs -> - List.map Loc.type srcs = List.map mreg_type dsts -> - wt_block tf k -> - wt_block tf (add_reloads srcs dsts k). -Proof. - induction srcs; intros. - destruct dsts. simpl; auto. simpl in H0; discriminate. - destruct dsts; simpl in H0. discriminate. simpl. - apply wt_add_reload. apply H; apply in_eq. congruence. - apply IHsrcs. red; intros; apply H; apply in_cons; auto. - congruence. auto. -Qed. - -Lemma wt_reg_for: - forall l, mreg_type (reg_for l) = Loc.type l. -Proof. - intros. destruct l; simpl. auto. - case (slot_type s); reflexivity. -Qed. -Hint Resolve wt_reg_for: allocty. - -Lemma wt_regs_for_rec: - forall locs itmps ftmps, - (List.length locs <= List.length itmps)%nat -> - (List.length locs <= List.length ftmps)%nat -> - (forall r, In r itmps -> mreg_type r = Tint) -> - (forall r, In r ftmps -> mreg_type r = Tfloat) -> - List.map mreg_type (regs_for_rec locs itmps ftmps) = List.map Loc.type locs. -Proof. - induction locs; intros. - simpl. auto. - destruct itmps; simpl in H. omegaContradiction. - destruct ftmps; simpl in H0. omegaContradiction. - simpl. apply (f_equal2 (@cons typ)). - destruct a. reflexivity. simpl. case (slot_type s). - apply H1; apply in_eq. apply H2; apply in_eq. - apply IHlocs. omega. omega. - intros; apply H1; apply in_cons; auto. - intros; apply H2; apply in_cons; auto. -Qed. - -Lemma wt_regs_for: - forall locs, - (List.length locs <= 3)%nat -> - List.map mreg_type (regs_for locs) = List.map Loc.type locs. -Proof. - intros. unfold regs_for. apply wt_regs_for_rec. - simpl. auto. simpl. auto. - simpl; intros; intuition; subst r; reflexivity. - simpl; intros; intuition; subst r; reflexivity. -Qed. -Hint Resolve wt_regs_for: allocty. - -Lemma wt_add_move: - forall src dst b, - loc_read_ok src -> loc_write_ok dst -> - Loc.type src = Loc.type dst -> - wt_block tf b -> - wt_block tf (add_move src dst b). -Proof. - intros. unfold add_move. - case (Loc.eq src dst); intro. - auto. - destruct src. apply wt_add_spill; auto. - destruct dst. apply wt_add_reload; auto. - set (tmp := match slot_type s with Tint => IT1 | Tfloat => FT1 end). - apply wt_add_reload. auto. - simpl. unfold tmp. case (slot_type s); reflexivity. - apply wt_add_spill. auto. - simpl. simpl in H1. rewrite <- H1. unfold tmp. case (slot_type s); reflexivity. - auto. -Qed. - -Lemma wt_add_moves: - forall b moves, - (forall s d, In (s, d) moves -> - loc_read_ok s /\ loc_write_ok d /\ Loc.type s = Loc.type d) -> - wt_block tf b -> - wt_block tf - (List.fold_right (fun p k => add_move (fst p) (snd p) k) b moves). -Proof. - induction moves; simpl; intros. - auto. - destruct a as [s d]. simpl. - elim (H s d). intros A [B C]. apply wt_add_move; auto. auto. -Qed. - -Theorem wt_parallel_move: - forall srcs dsts b, - List.map Loc.type srcs = List.map Loc.type dsts -> - locs_read_ok srcs -> - locs_write_ok dsts -> wt_block tf b -> wt_block tf (parallel_move srcs dsts b). -Proof. - intros. unfold parallel_move. apply wt_add_moves; auto. - intros. - elim (parmove_prop_2 _ _ _ _ H3); intros A B. - split. destruct A as [C|[C|C]]. - apply H0; auto. subst s; exact I. subst s; exact I. - split. destruct B as [C|[C|C]]. - apply H1; auto. subst d; exact I. subst d; exact I. - eapply parmove_prop_3; eauto. -Qed. - -Lemma wt_add_op_move: - forall src res s, - Loc.type src = Loc.type res -> - loc_read_ok src -> loc_write_ok res -> - wt_block tf (add_op Omove (src :: nil) res s). -Proof. - intros. unfold add_op. simpl. - apply wt_add_move. auto. auto. auto. constructor. -Qed. - -Lemma wt_add_op_undef: - forall res s, - loc_write_ok res -> - wt_block tf (add_op Oundef nil res s). -Proof. - intros. unfold add_op. simpl. - apply wt_Bopundef. apply wt_add_spill. auto. auto with allocty. - constructor. -Qed. - -Lemma wt_add_op_others: - forall op args res s, - op <> Omove -> op <> Oundef -> - (List.map Loc.type args, Loc.type res) = type_of_operation op -> - locs_read_ok args -> - loc_write_ok res -> - wt_block tf (add_op op args res s). -Proof. - intros. unfold add_op. - caseEq (is_move_operation op args). intros. - generalize (is_move_operation_correct op args H4). tauto. - intro. assert ((List.length args <= 3)%nat). - replace (length args) with (length (fst (type_of_operation op))). - apply Allocproof.length_type_of_operation. - rewrite <- H1. simpl. apply list_length_map. - generalize (wt_regs_for args H5); intro. - generalize (wt_reg_for res); intro. - apply wt_add_reloads. auto. auto. - apply wt_Bop. auto. auto. congruence. - apply wt_add_spill. auto. auto. constructor. -Qed. - -Lemma wt_add_load: - forall chunk addr args dst s, - List.map Loc.type args = type_of_addressing addr -> - Loc.type dst = type_of_chunk chunk -> - locs_read_ok args -> - loc_write_ok dst -> - wt_block tf (add_load chunk addr args dst s). -Proof. - intros. unfold add_load. - assert ((List.length args <= 2)%nat). - replace (length args) with (length (type_of_addressing addr)). - apply Allocproof.length_type_of_addressing. - rewrite <- H. apply list_length_map. - assert ((List.length args <= 3)%nat). omega. - generalize (wt_regs_for args H4); intro. - generalize (wt_reg_for dst); intro. - apply wt_add_reloads. auto. auto. - apply wt_Bload. congruence. congruence. - apply wt_add_spill. auto. auto. constructor. -Qed. - -Lemma wt_add_store: - forall chunk addr args src s, - List.map Loc.type args = type_of_addressing addr -> - Loc.type src = type_of_chunk chunk -> - locs_read_ok args -> - loc_read_ok src -> - wt_block tf (add_store chunk addr args src s). -Proof. - intros. unfold add_store. - assert ((List.length args <= 2)%nat). - replace (length args) with (length (type_of_addressing addr)). - apply Allocproof.length_type_of_addressing. - rewrite <- H. apply list_length_map. - assert ((List.length (src :: args) <= 3)%nat). simpl. omega. - generalize (wt_regs_for (src :: args) H4); intro. - caseEq (regs_for (src :: args)). - intro. constructor. - intros rsrc rargs EQ. rewrite EQ in H5. simpl in H5. - apply wt_add_reloads. - red; intros. elim H6; intro. subst l; auto. auto. - simpl. congruence. - apply wt_Bstore. congruence. congruence. constructor. -Qed. - -Lemma wt_add_call: - forall sig los args res s, - match los with inl l => Loc.type l = Tint | inr s => True end -> - List.map Loc.type args = sig.(sig_args) -> - Loc.type res = match sig.(sig_res) with None => Tint | Some ty => ty end -> - locs_read_ok args -> - match los with inl l => loc_read_ok l | inr s => True end -> - loc_write_ok res -> - wt_block tf (add_call sig los args res s). -Proof. - intros. - assert (locs_write_ok (loc_arguments sig)). - red; intros. generalize (loc_arguments_acceptable sig l H5). - destruct l; simpl. auto. - destruct s0; try contradiction. simpl. omega. - unfold add_call. destruct los. - apply wt_add_reload. auto. simpl; congruence. - apply wt_parallel_move. rewrite loc_arguments_type. auto. - auto. auto. - apply wt_Bcall. reflexivity. - apply wt_add_spill. auto. - rewrite loc_result_type. auto. constructor. - apply wt_parallel_move. rewrite loc_arguments_type. auto. - auto. auto. - apply wt_Bcall. auto. - apply wt_add_spill. auto. - rewrite loc_result_type. auto. constructor. -Qed. - -Lemma wt_add_alloc: - forall arg res s, - Loc.type arg = Tint -> Loc.type res = Tint -> - loc_read_ok arg -> loc_write_ok res -> - wt_block tf (add_alloc arg res s). -Proof. - intros. - unfold add_alloc. apply wt_add_reload. auto. rewrite H; reflexivity. - apply wt_Balloc. apply wt_add_spill. auto. rewrite H0; reflexivity. - apply wt_Bgoto. -Qed. - -Lemma wt_add_cond: - forall cond args ifso ifnot, - List.map Loc.type args = type_of_condition cond -> - locs_read_ok args -> - wt_block tf (add_cond cond args ifso ifnot). -Proof. - intros. - assert ((List.length args) <= 3)%nat. - replace (length args) with (length (type_of_condition cond)). - apply Allocproof.length_type_of_condition. - rewrite <- H. apply list_length_map. - generalize (wt_regs_for args H1). intro. - unfold add_cond. apply wt_add_reloads. - auto. auto. - apply wt_Bcond. congruence. -Qed. - -Lemma wt_add_return: - forall sig optarg, - option_map Loc.type optarg = sig.(sig_res) -> - match optarg with None => True | Some arg => loc_read_ok arg end -> - wt_block tf (add_return sig optarg). -Proof. - intros. unfold add_return. destruct optarg. - apply wt_add_reload. auto. rewrite loc_result_type. - simpl in H. destruct (sig_res sig). congruence. discriminate. - constructor. - apply wt_Bopundef. constructor. -Qed. - -Lemma wt_add_undefs: - forall ll b, - wt_block tf b -> wt_block tf (add_undefs ll b). -Proof. - induction ll; intros. - simpl. auto. - simpl. destruct a. apply wt_Bopundef. auto. auto. -Qed. - -Lemma wt_add_entry: - forall params undefs s, - List.map Loc.type params = sig_args (RTL.fn_sig f) -> - locs_write_ok params -> - wt_block tf (add_entry (RTL.fn_sig f) params undefs s). -Proof. - set (sig := RTL.fn_sig f). - assert (sig = tf.(fn_sig)). - unfold sig. - assert (transf_fundef (Internal f) = Some (Internal tf)). - unfold transf_fundef, transf_partial_fundef. rewrite TRANSL; auto. - generalize (Allocproof.sig_function_translated _ _ H). simpl; auto. - assert (locs_read_ok (loc_parameters sig)). - red; unfold loc_parameters. intros. - generalize (list_in_map_inv _ _ _ H0). intros [l1 [EQ IN]]. - subst l. generalize (loc_arguments_acceptable _ _ IN). - destruct l1. simpl. auto. - destruct s; try contradiction. - simpl; intros. split. omega. rewrite <- H. - apply loc_arguments_bounded. auto. - intros. unfold add_entry. - apply wt_parallel_move. rewrite loc_parameters_type. auto. - auto. auto. - apply wt_add_undefs. constructor. -Qed. +Hint Resolve alloc_acceptable allocs_acceptable: allocty. +Hint Rewrite alloc_type alloc_types: allocty. +Hint Resolve valid_successor_transf: allocty. (** * Type preservation during translation from RTL to LTL *) +Ltac WT := + constructor; auto with allocty; autorewrite with allocty; auto. + Lemma wt_transf_instr: forall pc instr, - RTLtyping.wt_instr env f.(RTL.fn_sig) instr -> - wt_block tf (transf_instr f live alloc pc instr). + RTLtyping.wt_instr env f instr -> + wt_instr tf (transf_instr f live alloc pc instr). Proof. - intros. inversion H; simpl. + intros. inv H; simpl. (* nop *) - constructor. + WT. (* move *) - case (Regset.mem r live!!pc). - apply wt_add_op_move; auto with allocty. - repeat rewrite alloc_type. auto. constructor. - (* undef *) - case (Regset.mem r live!!pc). - apply wt_add_op_undef; auto with allocty. - constructor. + destruct (Regset.mem r live!!pc). + destruct (is_redundant_move Omove (r1 :: nil) r alloc); WT. + WT. (* other ops *) - case (Regset.mem res live!!pc). - apply wt_add_op_others; auto with allocty. - rewrite alloc_types. rewrite alloc_type. auto. - constructor. + destruct (Regset.mem res live!!pc). + destruct (is_redundant_move op args res alloc); WT. + WT. (* load *) - case (Regset.mem dst live!!pc). - apply wt_add_load; auto with allocty. - rewrite alloc_types. auto. rewrite alloc_type. auto. - constructor. + destruct (Regset.mem dst live!!pc); WT. (* store *) - apply wt_add_store; auto with allocty. - rewrite alloc_types. auto. rewrite alloc_type. auto. + WT. (* call *) - apply wt_add_call. - destruct ros; simpl. rewrite alloc_type; auto. auto. - rewrite alloc_types; auto. - rewrite alloc_type. auto. - auto with allocty. + WT. + destruct ros; simpl. autorewrite with allocty; auto. auto. + destruct ros; simpl; auto with allocty. + (* tailcall *) + WT. + destruct ros; simpl. autorewrite with allocty; auto. auto. destruct ros; simpl; auto with allocty. - auto with allocty. + rewrite transf_unroll; auto. (* alloc *) - apply wt_add_alloc; auto with allocty. - rewrite alloc_type; auto. rewrite alloc_type; auto. + WT. (* cond *) - apply wt_add_cond. rewrite alloc_types; auto. auto with allocty. + WT. (* return *) - apply wt_add_return. - destruct optres; simpl. rewrite alloc_type. exact H0. exact H0. + WT. + rewrite transf_unroll; simpl. + destruct optres; simpl. autorewrite with allocty. auto. auto. destruct optres; simpl; auto with allocty. Qed. -Lemma wt_transf_instrs: - let c := PTree.map (transf_instr f live alloc) (RTL.fn_code f) in - forall pc b, c!pc = Some b -> wt_block tf b. -Proof. - intros until b. - unfold c. rewrite PTree.gmap. caseEq (RTL.fn_code f)!pc. - intros instr EQ. simpl. intros. injection H; intro; subst b. - apply wt_transf_instr. eapply RTLtyping.wt_instrs; eauto. - apply wt_rtl_function. - simpl; intros; discriminate. -Qed. - -Lemma wt_transf_entrypoint: - let c := transf_entrypoint f live alloc - (PTree.map (transf_instr f live alloc) (RTL.fn_code f)) in - (forall pc b, c!pc = Some b -> wt_block tf b). -Proof. - simpl. unfold transf_entrypoint. - intros pc b. rewrite PTree.gsspec. - case (peq pc (fn_nextpc f)); intros. - injection H; intro; subst b. - apply wt_add_entry. - rewrite alloc_types. eapply RTLtyping.wt_params. apply wt_rtl_function. - auto with allocty. - apply wt_transf_instrs with pc; auto. -Qed. - End TYPING_FUNCTION. Lemma wt_transf_function: forall f tf, - transf_function f = Some tf -> wt_function tf. + transf_function f = OK tf -> wt_function tf. Proof. intros. generalize H; unfold transf_function. caseEq (type_function f). intros env TYP. @@ -527,19 +145,27 @@ Proof. with (live0 f live). caseEq (regalloc f live (live0 f live) env). intros alloc ALLOC. - intro EQ; injection EQ; intro; subst tf. - red. simpl. intros. eapply wt_transf_entrypoint; eauto. - intros; discriminate. - intros; discriminate. - intros; discriminate. -Qed. + intro EQ; injection EQ; intro. + assert (RTLtyping.wt_function f env). apply type_function_correct; auto. + inversion H1. + constructor; rewrite <- H0; simpl. + rewrite (alloc_types _ _ _ _ ALLOC). auto. + eapply regsalloc_acceptable; eauto. + eapply regalloc_norepet_norepet; eauto. + eapply regalloc_correct_2; eauto. + intros until instr. rewrite PTree.gmap. + caseEq (RTL.fn_code f)!pc; simpl; intros. + inversion H3. eapply wt_transf_instr; eauto. congruence. discriminate. + eapply valid_successor_transf; eauto. congruence. + congruence. congruence. congruence. +Qed. Lemma wt_transf_fundef: forall f tf, - transf_fundef f = Some tf -> wt_fundef tf. + transf_fundef f = OK tf -> wt_fundef tf. Proof. intros until tf; destruct f; simpl. - caseEq (transf_function f). intros g TF EQ. inversion EQ. + caseEq (transf_function f); simpl. intros g TF EQ. inversion EQ. constructor. eapply wt_transf_function; eauto. congruence. intros. inversion H. constructor. @@ -547,7 +173,7 @@ Qed. Lemma program_typing_preserved: forall (p: RTL.program) (tp: LTL.program), - transf_program p = Some tp -> + transf_program p = OK tp -> LTLtyping.wt_program tp. Proof. intros; red; intros. |