diff options
| -rw-r--r-- | .depend | 2 | ||||
| -rw-r--r-- | backend/Allocproof.v | 2 | ||||
| -rw-r--r-- | backend/Alloctyping.v | 15 | ||||
| -rw-r--r-- | backend/Coloring.v | 33 | ||||
| -rw-r--r-- | backend/Coloringproof.v | 168 | ||||
| -rw-r--r-- | backend/Conventions.v | 6 | ||||
| -rw-r--r-- | backend/LTLintyping.v | 9 | ||||
| -rw-r--r-- | backend/LTLtyping.v | 12 | ||||
| -rw-r--r-- | backend/Lineartyping.v | 2 | ||||
| -rw-r--r-- | backend/Locations.v | 16 | ||||
| -rw-r--r-- | backend/Op.v | 32 | ||||
| -rw-r--r-- | backend/PPC.v | 8 | ||||
| -rw-r--r-- | backend/PPCgen.v | 78 | ||||
| -rw-r--r-- | backend/PPCgenproof.v | 28 | ||||
| -rw-r--r-- | backend/PPCgenproof1.v | 114 | ||||
| -rw-r--r-- | backend/Parallelmove.v | 10 | ||||
| -rw-r--r-- | backend/Reload.v | 92 | ||||
| -rw-r--r-- | backend/Reloadproof.v | 492 | ||||
| -rw-r--r-- | backend/Reloadtyping.v | 63 | ||||
| -rw-r--r-- | backend/Selectionproof.v | 2 | ||||
| -rw-r--r-- | caml/PrintPPC.ml | 28 | ||||
| -rw-r--r-- | extraction/.depend | 4 |
22 files changed, 795 insertions, 421 deletions
@@ -46,7 +46,7 @@ backend/Tunneling.vo: backend/Tunneling.v lib/Coqlib.vo lib/Maps.vo common/AST.v backend/Tunnelingproof.vo: backend/Tunnelingproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Tunneling.vo backend/Tunnelingtyping.vo: backend/Tunnelingtyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Values.vo common/Mem.vo common/Globalenvs.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/Tunneling.vo backend/Tunnelingproof.vo backend/LTLin.vo: backend/LTLin.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/Conventions.vo -backend/LTLintyping.vo: backend/LTLintyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/LTLin.vo backend/Conventions.vo +backend/LTLintyping.vo: backend/LTLintyping.v lib/Coqlib.vo lib/Maps.vo common/AST.vo backend/Op.vo backend/RTL.vo backend/Locations.vo backend/LTLin.vo backend/LTLtyping.vo backend/Conventions.vo backend/Linearize.vo: backend/Linearize.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo common/Values.vo common/Globalenvs.vo common/Errors.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLin.vo backend/Kildall.vo lib/Lattice.vo backend/Linearizeproof.vo: backend/Linearizeproof.v lib/Coqlib.vo lib/Maps.vo lib/Ordered.vo common/AST.vo lib/Integers.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Errors.vo common/Smallstep.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo lib/Lattice.vo backend/Linearizetyping.vo: backend/Linearizetyping.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo backend/Op.vo backend/Locations.vo backend/LTL.vo backend/LTLtyping.vo backend/LTLin.vo backend/Linearize.vo backend/LTLintyping.vo backend/Conventions.vo diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 58ed3b6..5e38934 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -649,7 +649,7 @@ Proof. (* Icall *) exploit transl_find_function; eauto. intros [tf [TFIND TF]]. - generalize (regalloc_correct_1 f0 env live _ _ _ _ ASG H).
unfold correct_alloc_instr. intros [CORR1 CORR2]. + generalize (regalloc_correct_1 f0 env live _ _ _ _ ASG H).
unfold correct_alloc_instr. intros [CORR1 [CORR2 CORR3]]. assert (rs##args = map ls (map assign args)). eapply agree_eval_regs; eauto. econstructor; split. diff --git a/backend/Alloctyping.v b/backend/Alloctyping.v index 469fd3c..d9ab17b 100644 --- a/backend/Alloctyping.v +++ b/backend/Alloctyping.v @@ -106,6 +106,7 @@ Ltac WT := Lemma wt_transf_instr: forall pc instr, RTLtyping.wt_instr env f instr -> + f.(RTL.fn_code)!pc = Some instr -> wt_instr tf (transf_instr f live alloc pc instr). Proof. intros. inv H; simpl. @@ -124,13 +125,19 @@ Proof. (* store *) WT. (* call *) + exploit regalloc_correct_1; eauto. unfold correct_alloc_instr. + intros [A1 [A2 A3]]. WT. - destruct ros; simpl. autorewrite with allocty; auto. auto. - destruct ros; simpl; auto with allocty. + destruct ros; simpl; auto. + split. autorewrite with allocty; auto. + split. auto with allocty. auto. (* tailcall *) + exploit regalloc_correct_1; eauto. unfold correct_alloc_instr. + intro A1. WT. - destruct ros; simpl. autorewrite with allocty; auto. auto. - destruct ros; simpl; auto with allocty. + destruct ros; simpl; auto. + split. autorewrite with allocty; auto. + split. auto with allocty. auto. rewrite transf_unroll; auto. (* alloc *) WT. diff --git a/backend/Coloring.v b/backend/Coloring.v index 5e91b03..056aaa5 100644 --- a/backend/Coloring.v +++ b/backend/Coloring.v @@ -110,12 +110,26 @@ Definition add_interf_move if Reg.eq r arg then false else true) res live g. -Definition add_interf_call +Definition add_interf_destroyed (live: Regset.t) (destroyed: list mreg) (g: graph): graph := List.fold_left (fun g mr => Regset.fold graph (fun r g => add_interf_mreg r mr g) live g) destroyed g. +Definition add_interfs_indirect_call + (rfun: reg) (locs: list loc) (g: graph): graph := + List.fold_left + (fun g loc => + match loc with R mr => add_interf_mreg rfun mr g | _ => g end) + locs g. + +Definition add_interf_call + (ros: reg + ident) (locs: list loc) (g: graph): graph := + match ros with + | inl rfun => add_interfs_indirect_call rfun locs g + | inr idfun => g + end. + Fixpoint add_prefs_call (args: list reg) (locs: list loc) (g: graph) {struct args} : graph := match args, locs with @@ -157,18 +171,23 @@ Definition add_edges_instr then add_interf_op dst live g else g | Icall sig ros args res s => - add_prefs_call args (loc_arguments sig) - (add_pref_mreg res (loc_result sig) + let largs := loc_arguments sig in + let lres := loc_result sig in + add_prefs_call args largs + (add_pref_mreg res lres (add_interf_op res live - (add_interf_call - (Regset.remove res live) destroyed_at_call_regs g))) + (add_interf_call ros largs + (add_interf_destroyed + (Regset.remove res live) destroyed_at_call_regs g)))) | Itailcall sig ros args => - add_prefs_call args (loc_arguments sig) g + let largs := loc_arguments sig in + add_prefs_call args largs + (add_interf_call ros largs g) | Ialloc arg res s => add_pref_mreg arg loc_alloc_argument (add_pref_mreg res loc_alloc_result (add_interf_op res live - (add_interf_call + (add_interf_destroyed (Regset.remove res live) destroyed_at_call_regs g))) | Ireturn (Some r) => add_pref_mreg r (loc_result sig) g diff --git a/backend/Coloringproof.v b/backend/Coloringproof.v index cea4ce5..ea31a29 100644 --- a/backend/Coloringproof.v +++ b/backend/Coloringproof.v @@ -133,7 +133,7 @@ Proof. rewrite dec_eq_false; auto. rewrite dec_eq_false; auto. Qed. -Lemma add_interf_call_incl_aux_1: +Lemma add_interf_destroyed_incl_aux_1: forall mr live g, graph_incl g (List.fold_left (fun g r => add_interf_mreg r mr g) live g). @@ -145,22 +145,42 @@ Proof. auto. Qed. -Lemma add_interf_call_incl_aux_2: +Lemma add_interf_destroyed_incl_aux_2: forall mr live g, graph_incl g (Regset.fold graph (fun r g => add_interf_mreg r mr g) live g). Proof. - intros. rewrite Regset.fold_1. apply add_interf_call_incl_aux_1. + intros. rewrite Regset.fold_1. apply add_interf_destroyed_incl_aux_1. Qed. -Lemma add_interf_call_incl: +Lemma add_interf_destroyed_incl: forall live destroyed g, - graph_incl g (add_interf_call live destroyed g). + graph_incl g (add_interf_destroyed live destroyed g). Proof. induction destroyed; simpl; intros. apply graph_incl_refl. eapply graph_incl_trans; [idtac|apply IHdestroyed]. - apply add_interf_call_incl_aux_2. + apply add_interf_destroyed_incl_aux_2. +Qed. + +Lemma add_interfs_indirect_call_incl: + forall rfun locs g, + graph_incl g (add_interfs_indirect_call rfun locs g). +Proof. + unfold add_interfs_indirect_call. induction locs; simpl; intros. + apply graph_incl_refl. + destruct a. eapply graph_incl_trans; [idtac|eauto]. + apply add_interf_mreg_incl. + auto. +Qed. + +Lemma add_interfs_call_incl: + forall ros locs g, + graph_incl g (add_interf_call ros locs g). +Proof. + intros. unfold add_interf_call. destruct ros. + apply add_interfs_indirect_call_incl. + apply graph_incl_refl. Qed. Lemma interfere_incl: @@ -181,7 +201,7 @@ Proof. unfold graph_incl; intros. elim H; auto. Qed. -Lemma add_interf_call_correct_aux_1: +Lemma add_interf_destroyed_correct_aux_1: forall mr r live, InA Regset.E.eq r live -> forall g, @@ -190,36 +210,60 @@ Lemma add_interf_call_correct_aux_1: Proof. induction 1; simpl; intros. hnf in H; subst y. eapply interfere_mreg_incl. - apply add_interf_call_incl_aux_1. + apply add_interf_destroyed_incl_aux_1. apply add_interf_mreg_correct. auto. Qed. -Lemma add_interf_call_correct_aux_2: +Lemma add_interf_destroyed_correct_aux_2: forall mr live g r, Regset.In r live -> interfere_mreg r mr (Regset.fold graph (fun r g => add_interf_mreg r mr g) live g). Proof. - intros. rewrite Regset.fold_1. apply add_interf_call_correct_aux_1. + intros. rewrite Regset.fold_1. apply add_interf_destroyed_correct_aux_1. apply Regset.elements_1. auto. Qed. -Lemma add_interf_call_correct: +Lemma add_interf_destroyed_correct: forall live destroyed g r mr, Regset.In r live -> In mr destroyed -> - interfere_mreg r mr (add_interf_call live destroyed g). + interfere_mreg r mr (add_interf_destroyed live destroyed g). Proof. induction destroyed; simpl; intros. elim H0. elim H0; intros. subst a. eapply interfere_mreg_incl. - apply add_interf_call_incl. - apply add_interf_call_correct_aux_2; auto. + apply add_interf_destroyed_incl. + apply add_interf_destroyed_correct_aux_2; auto. apply IHdestroyed; auto. Qed. +Lemma add_interfs_indirect_call_correct: + forall rfun mr locs g, + In (R mr) locs -> + interfere_mreg rfun mr (add_interfs_indirect_call rfun locs g). +Proof. + unfold add_interfs_indirect_call. induction locs; simpl; intros. + elim H. + destruct H. subst a. + eapply interfere_mreg_incl. + apply (add_interfs_indirect_call_incl rfun locs (add_interf_mreg rfun mr g)). + apply add_interf_mreg_correct. + auto. +Qed. + +Lemma add_interfs_call_correct: + forall rfun locs g mr, + In (R mr) locs -> + interfere_mreg rfun mr (add_interf_call (inl _ rfun) locs g). +Proof. + intros. unfold add_interf_call. + apply add_interfs_indirect_call_correct. auto. +Qed. + + Lemma add_prefs_call_incl: forall args locs g, graph_incl g (add_prefs_call args locs g). @@ -336,12 +380,14 @@ Proof. eapply graph_incl_trans; [idtac|apply add_prefs_call_incl]. eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. eapply graph_incl_trans; [idtac|apply add_interf_op_incl]. - apply add_interf_call_incl. - apply add_prefs_call_incl. + eapply graph_incl_trans; [idtac|apply add_interfs_call_incl]. + apply add_interf_destroyed_incl. + eapply graph_incl_trans; [idtac|apply add_prefs_call_incl]. + apply add_interfs_call_incl. eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. eapply graph_incl_trans; [idtac|apply add_interf_op_incl]. - apply add_interf_call_incl. + apply add_interf_destroyed_incl. destruct o. apply add_pref_mreg_incl. apply graph_incl_refl. @@ -379,7 +425,18 @@ Definition correct_interf_instr interfere_mreg r mr g) /\ (forall r, Regset.In r live -> - r <> res -> interfere r res g) + r <> res -> interfere r res g) + /\ (match ros with + | inl rfun => forall mr, In (R mr) (loc_arguments sig) -> + interfere_mreg rfun mr g + | inr idfun => True + end) + | Itailcall sig ros args => + match ros with + | inl rfun => forall mr, In (R mr) (loc_arguments sig) -> + interfere_mreg rfun mr g + | inr idfun => True + end | Ialloc arg res s => (forall r mr, Regset.In r live -> @@ -405,9 +462,11 @@ Proof. intros. eapply interfere_incl; eauto. intros. eapply interfere_incl; eauto. intros. eapply interfere_incl; eauto. - intros [A B]. split. - intros. eapply interfere_mreg_incl; eauto. - intros. eapply interfere_incl; eauto. + intros [A [B C]]. + split. intros. eapply interfere_mreg_incl; eauto. + split. intros. eapply interfere_incl; eauto. + destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. + destruct s0; auto. intros. eapply interfere_mreg_incl; eauto. intros [A B]. split. intros. eapply interfere_mreg_incl; eauto. intros. eapply interfere_incl; eauto. @@ -426,27 +485,46 @@ Proof. intros. rewrite Regset.mem_1; auto. apply add_interf_op_correct; auto. - split; intros. + (* Icall *) + set (largs := loc_arguments s). + set (lres := loc_result s). + split. intros. apply interfere_mreg_incl with - (add_interf_call (Regset.remove r live) destroyed_at_call_regs g). + (add_interf_destroyed (Regset.remove r live) destroyed_at_call_regs g). eapply graph_incl_trans; [idtac|apply add_prefs_call_incl]. eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. - apply add_interf_op_incl. - apply add_interf_call_correct; auto. - apply Regset.remove_2; auto. + eapply graph_incl_trans; [idtac|apply add_interf_op_incl]. + apply add_interfs_call_incl. + apply add_interf_destroyed_correct; auto. + apply Regset.remove_2; auto. + split. intros. eapply interfere_incl. eapply graph_incl_trans; [idtac|apply add_prefs_call_incl]. apply add_pref_mreg_incl. apply add_interf_op_correct; auto. + destruct s0; auto; intros. + eapply interfere_mreg_incl. + eapply graph_incl_trans; [idtac|apply add_prefs_call_incl]. + eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. + apply add_interf_op_incl. + apply add_interfs_call_correct. auto. + + (* Itailcall *) + destruct s0; auto; intros. + eapply interfere_mreg_incl. + apply add_prefs_call_incl. + apply add_interfs_call_correct. auto. + + (* Ialloc *) split; intros. apply interfere_mreg_incl with - (add_interf_call (Regset.remove r0 live) destroyed_at_call_regs g). + (add_interf_destroyed (Regset.remove r0 live) destroyed_at_call_regs g). eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. eapply graph_incl_trans; [idtac|apply add_pref_mreg_incl]. apply add_interf_op_incl. - apply add_interf_call_correct; auto. + apply add_interf_destroyed_correct; auto. apply Regset.remove_2; auto. eapply interfere_incl. @@ -739,6 +817,15 @@ Definition correct_alloc_instr /\ (forall r, Regset.In r live!!pc -> r <> res -> alloc r <> alloc res) + /\ (match ros with + | inl rfun => ~(In (alloc rfun) (loc_arguments sig)) + | inr idfun => True + end) + | Itailcall sig ros args => + (match ros with + | inl rfun => ~(In (alloc rfun) (loc_arguments sig)) + | inr idfun => True + end) | Ialloc arg res s => (forall r, Regset.In r live!!pc -> @@ -810,21 +897,37 @@ Lemma correct_interf_alloc_instr: forall pc instr, (forall r1 r2, interfere r1 r2 g -> alloc r1 <> alloc r2) -> (forall r1 mr2, interfere_mreg r1 mr2 g -> alloc r1 <> R mr2) -> + (forall r, loc_acceptable (alloc r)) -> correct_interf_instr live!!pc instr g -> correct_alloc_instr live alloc pc instr. Proof. - intros pc instr ALL1 ALL2. + intros pc instr ALL1 ALL2 ALL3. unfold correct_interf_instr, correct_alloc_instr; destruct instr; auto. destruct (is_move_operation o l); auto. - intros [A B]. split. - intros; red; intros. + (* Icall *) + intros [A [B C]]. + split. intros; red; intros. unfold destroyed_at_call in H1. generalize (list_in_map_inv R _ _ H1). intros [mr [EQ IN]]. generalize (A r0 mr H IN H0). intro. generalize (ALL2 _ _ H2). contradiction. - auto. + split. auto. + destruct s0; auto. red; intros. + generalize (ALL3 r0). generalize (Conventions.loc_arguments_acceptable _ _ H). + unfold loc_argument_acceptable, loc_acceptable. + caseEq (alloc r0). intros. + elim (ALL2 r0 m). apply C; auto. congruence. auto. + destruct s0; auto. + (* Itailcall *) + destruct s0; auto. red; intros. + generalize (ALL3 r). generalize (Conventions.loc_arguments_acceptable _ _ H0). + unfold loc_argument_acceptable, loc_acceptable. + caseEq (alloc r). intros. + elim (ALL2 r m). apply H; auto. congruence. auto. + destruct s0; auto. + (* Ialloc *) intros [A B]. split. intros; red; intros. unfold destroyed_at_call in H1. @@ -850,6 +953,7 @@ Proof. apply alloc_of_coloring_correct_1. auto. rewrite H4 in H3; auto. intros. rewrite H2. unfold allregs. apply alloc_of_coloring_correct_2. auto. exact H3. + intros. eapply regalloc_acceptable; eauto. unfold g. apply interf_graph_correct_1. auto. Qed. diff --git a/backend/Conventions.v b/backend/Conventions.v index a861eb8..b7d931f 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -51,8 +51,12 @@ Definition destroyed_at_call_regs := Definition destroyed_at_call := List.map R destroyed_at_call_regs. +Definition int_temporaries := IT1 :: IT2 :: nil. + +Definition float_temporaries := FT1 :: FT2 :: FT3 :: nil. + Definition temporaries := - R IT1 :: R IT2 :: R IT3 :: R FT1 :: R FT2 :: R FT3 :: nil. + R IT1 :: R IT2 :: R FT1 :: R FT2 :: R FT3 :: nil. (** The [index_int_callee_save] and [index_float_callee_save] associate a unique positive integer to callee-save registers. This integer is diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index 1c0c3f3..26ec066 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -19,6 +19,7 @@ Require Import Op. Require Import RTL. Require Import Locations. Require Import LTLin. +Require LTLtyping. Require Import Conventions. (** The following predicates define a type system for LTLin similar to that @@ -53,17 +54,15 @@ Inductive wt_instr : instruction -> Prop := wt_instr (Lstore chunk addr args src) | wt_Lcall: forall sig ros args res, - match ros with inl r => Loc.type r = 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 -> - match ros with inl r => loc_acceptable r | inr s => True end -> + Loc.type res = proj_sig_res sig -> + LTLtyping.call_loc_acceptable sig ros -> locs_acceptable args -> loc_acceptable res -> wt_instr (Lcall sig ros args res) | wt_Ltailcall: forall sig ros args, - match ros with inl r => Loc.type r = Tint | inr s => True end -> List.map Loc.type args = sig.(sig_args) -> - match ros with inl r => loc_acceptable r | inr s => True end -> + LTLtyping.call_loc_acceptable sig ros -> locs_acceptable args -> sig.(sig_res) = funsig.(sig_res) -> Conventions.tailcall_possible sig -> diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index 18308b8..950154a 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -35,6 +35,12 @@ Variable funct: function. Definition valid_successor (s: node) : Prop := exists i, funct.(fn_code)!s = Some i. +Definition call_loc_acceptable (sig: signature) (los: loc + ident) : Prop := + match los with + | inl l => Loc.type l = Tint /\ loc_acceptable l /\ ~In l (loc_arguments sig) + | inr s => True + end. + Inductive wt_instr : instruction -> Prop := | wt_Lnop: forall s, @@ -68,18 +74,16 @@ Inductive wt_instr : instruction -> Prop := wt_instr (Lstore chunk addr args src s) | wt_Lcall: forall sig ros args res s, - match ros with inl r => Loc.type r = Tint | inr s => True end -> List.map Loc.type args = sig.(sig_args) -> Loc.type res = proj_sig_res sig -> - match ros with inl r => loc_acceptable r | inr s => True end -> + call_loc_acceptable sig ros -> locs_acceptable args -> loc_acceptable res -> valid_successor s -> wt_instr (Lcall sig ros args res s) | wt_Ltailcall: forall sig ros args, - match ros with inl r => Loc.type r = Tint | inr s => True end -> List.map Loc.type args = sig.(sig_args) -> - match ros with inl r => loc_acceptable r | inr s => True end -> + call_loc_acceptable sig ros -> locs_acceptable args -> sig.(sig_res) = funct.(fn_sig).(sig_res) -> Conventions.tailcall_possible sig -> diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 7dc601f..9ef6e31 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -83,7 +83,7 @@ Inductive wt_instr : instruction -> Prop := | wt_Ltailcall: forall sig ros, tailcall_possible sig -> - match ros with inl r => r = IT3 | _ => True end -> + match ros with inl r => r = IT1 | _ => True end -> wt_instr (Ltailcall sig ros) | wt_Lalloc: wt_instr Lalloc diff --git a/backend/Locations.v b/backend/Locations.v index 1373887..b03657c 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -30,10 +30,10 @@ Require Import Values. - Integer registers that can be allocated to RTL pseudo-registers ([Rxx]). - Floating-point registers that can be allocated to RTL pseudo-registers ([Fxx]). -- Three integer registers, not allocatable, reserved as temporaries for - spilling and reloading ([ITx]). -- Three float registers, not allocatable, reserved as temporaries for - spilling and reloading ([FTx]). +- Two integer registers, not allocatable, reserved as temporaries for + spilling and reloading ([IT1, IT2]). +- Two float registers, not allocatable, reserved as temporaries for + spilling and reloading ([FT1, FT2]). The type [mreg] does not include special-purpose machine registers such as the stack pointer and the condition codes. *) @@ -56,7 +56,7 @@ Inductive mreg: Set := | F24: mreg | F25: mreg | F26: mreg | F27: mreg | F28: mreg | F29: mreg | F30: mreg | F31: mreg (** Integer temporaries *) - | IT1: mreg (* R11 *) | IT2: mreg (* R12 *) | IT3: mreg (* R0 *) + | IT1: mreg (* R11 *) | IT2: mreg (* R0 *) (** Float temporaries *) | FT1: mreg (* F11 *) | FT2: mreg (* F12 *) | FT3: mreg (* F0 *). @@ -79,7 +79,7 @@ Definition mreg_type (r: mreg): typ := | F20 => Tfloat | F21 => Tfloat | F22 => Tfloat | F23 => Tfloat | F24 => Tfloat | F25 => Tfloat | F26 => Tfloat | F27 => Tfloat | F28 => Tfloat | F29 => Tfloat | F30 => Tfloat | F31 => Tfloat - | IT1 => Tint | IT2 => Tint | IT3 => Tint + | IT1 => Tint | IT2 => Tint | FT1 => Tfloat | FT2 => Tfloat | FT3 => Tfloat end. @@ -104,8 +104,8 @@ Module IndexedMreg <: INDEXED_TYPE. | F20 => 44 | F21 => 45 | F22 => 46 | F23 => 47 | F24 => 48 | F25 => 49 | F26 => 50 | F27 => 51 | F28 => 52 | F29 => 53 | F30 => 54 | F31 => 55 - | IT1 => 56 | IT2 => 57 | IT3 => 58 - | FT1 => 59 | FT2 => 60 | FT3 => 61 + | IT1 => 56 | IT2 => 57 + | FT1 => 58 | FT2 => 59 | FT3 => 60 end. Lemma index_inj: forall r1 r2, index r1 = index r2 -> r1 = r2. diff --git a/backend/Op.v b/backend/Op.v index b1136f9..707bcb0 100644 --- a/backend/Op.v +++ b/backend/Op.v @@ -254,7 +254,7 @@ Definition eval_addressing | Aindexed2, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2)) | Aindexed2, Vint n1 :: Vptr b2 n2 :: nil => - Some (Vptr b2 (Int.add n1 n2)) + Some (Vptr b2 (Int.add n2 n1)) | Aglobal s ofs, nil => match Genv.find_symbol genv s with | None => None @@ -759,7 +759,6 @@ Proof. intros. unfold eval_addressing in H; destruct addr; FuncInv; try subst v; simpl; try reflexivity. - decEq. apply Int.add_commut. unfold find_symbol_offset. destruct (Genv.find_symbol genv i); congruence. unfold find_symbol_offset. @@ -876,3 +875,32 @@ Proof. Qed. End EVAL_LESSDEF. + +(** Transformation of addressing modes with two operands or more + into an equivalent arithmetic operation. This is used in the [Reload] + pass when a store instruction cannot be reloaded directly because + it runs out of temporary registers. *) + +(** For the PowerPC, there is only one binary addressing mode: [Aindexed2]. + The corresponding operation is [Oadd]. *) + +Definition op_for_binary_addressing (addr: addressing) : operation := Oadd. + +Lemma eval_op_for_binary_addressing: + forall (F: Set) (ge: Genv.t F) sp addr args m v, + (length args >= 2)%nat -> + eval_addressing ge sp addr args = Some v -> + eval_operation ge sp (op_for_binary_addressing addr) args m = Some v. +Proof. + intros. + unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; + simpl; congruence. +Qed. + +Lemma type_op_for_binary_addressing: + forall addr, + (length (type_of_addressing addr) >= 2)%nat -> + type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint). +Proof. + intros. destruct addr; simpl in H; reflexivity || omegaContradiction. +Qed. diff --git a/backend/PPC.v b/backend/PPC.v index cfd0740..13c7a87 100644 --- a/backend/PPC.v +++ b/backend/PPC.v @@ -564,7 +564,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome let sp := Vptr stk (Int.repr lo) in match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with | None => Error - | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR2 <- Vundef)) m2 + | Some m2 => OK (nextinstr (rs#GPR1 <- sp #GPR12 <- Vundef)) m2 end | Pand_ rd r1 r2 => let v := Val.and rs#r1 rs#r2 in @@ -655,9 +655,9 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pfsub rd r1 r2 => OK (nextinstr (rs#rd <- (Val.subf rs#r1 rs#r2))) m | Pictf rd r1 => - OK (nextinstr (rs#rd <- (Val.floatofint rs#r1) #GPR2 <- Vundef #FPR13 <- Vundef)) m + OK (nextinstr (rs#rd <- (Val.floatofint rs#r1) #GPR12 <- Vundef #FPR13 <- Vundef)) m | Piuctf rd r1 => - OK (nextinstr (rs#rd <- (Val.floatofintu rs#r1) #GPR2 <- Vundef #FPR13 <- Vundef)) m + OK (nextinstr (rs#rd <- (Val.floatofintu rs#r1) #GPR12 <- Vundef #FPR13 <- Vundef)) m | Plbz rd cst r1 => load1 Mint8unsigned rd cst r1 rs m | Plbzx rd r1 r2 => @@ -679,7 +679,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Plhzx rd r1 r2 => load2 Mint16unsigned rd r1 r2 rs m | Plfi rd f => - OK (nextinstr (rs#rd <- (Vfloat f) #GPR2 <- Vundef)) m + OK (nextinstr (rs#rd <- (Vfloat f) #GPR12 <- Vundef)) m | Plwz rd cst r1 => load1 Mint32 rd cst r1 rs m | Plwzx rd r1 r2 => diff --git a/backend/PPCgen.v b/backend/PPCgen.v index f6d1fec..1484a1e 100644 --- a/backend/PPCgen.v +++ b/backend/PPCgen.v @@ -34,7 +34,7 @@ Require Import PPC. results when applied to a LTL register of the wrong type. The proof in [PPCgenproof] will show that this never happens. - Note that no LTL register maps to [GPR2] nor [FPR13]. + Note that no LTL register maps to [GPR12] nor [FPR13]. These two registers are reserved as temporaries, to be used by the generated PPC code. *) @@ -47,7 +47,7 @@ Definition ireg_of (r: mreg) : ireg := | R21 => GPR21 | R22 => GPR22 | R23 => GPR23 | R24 => GPR24 | R25 => GPR25 | R26 => GPR26 | R27 => GPR27 | R28 => GPR28 | R29 => GPR29 | R30 => GPR30 | R31 => GPR31 - | IT1 => GPR11 | IT2 => GPR12 | IT3 => GPR0 + | IT1 => GPR11 | IT2 => GPR0 | _ => GPR0 (* should not happen *) end. @@ -108,7 +108,7 @@ Definition addimm_1 (r1 r2: ireg) (n: int) (k: code) := Paddi r1 r1 (Cint (low_s n)) :: k. Definition addimm_2 (r1 r2: ireg) (n: int) (k: code) := - loadimm GPR2 n (Padd r1 r2 GPR2 :: k). + loadimm GPR12 n (Padd r1 r2 GPR12 :: k). Definition addimm (r1 r2: ireg) (n: int) (k: code) := if ireg_eq r1 GPR0 then @@ -124,7 +124,7 @@ Definition andimm (r1 r2: ireg) (n: int) (k: code) := else if Int.eq (low_u n) Int.zero then Pandis_ r1 r2 (Cint (high_u n)) :: k else - loadimm GPR2 n (Pand_ r1 r2 GPR2 :: k). + loadimm GPR12 n (Pand_ r1 r2 GPR12 :: k). Definition orimm (r1 r2: ireg) (n: int) (k: code) := if Int.eq (high_u n) Int.zero then @@ -158,8 +158,8 @@ Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := if Int.eq (high_s ofs) Int.zero then loadind_aux base ofs ty dst :: k else - Paddis GPR2 base (Cint (high_s ofs)) :: - loadind_aux GPR2 (low_s ofs) ty dst :: k. + Paddis GPR12 base (Cint (high_s ofs)) :: + loadind_aux GPR12 (low_s ofs) ty dst :: k. Definition storeind_aux (src: mreg) (base: ireg) (ofs: int) (ty: typ) := match ty with @@ -171,8 +171,8 @@ Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := if Int.eq (high_s ofs) Int.zero then storeind_aux src base ofs ty :: k else - Paddis GPR2 base (Cint (high_s ofs)) :: - storeind_aux src GPR2 (low_s ofs) ty :: k. + Paddis GPR12 base (Cint (high_s ofs)) :: + storeind_aux src GPR12 (low_s ofs) ty :: k. (** Constructor for a floating-point comparison. The PowerPC has a single [fcmpu] instruction to compare floats, which sets @@ -206,20 +206,20 @@ Definition transl_cond if Int.eq (high_s n) Int.zero then Pcmpwi (ireg_of a1) (Cint n) :: k else - loadimm GPR2 n (Pcmpw (ireg_of a1) GPR2 :: k) + loadimm GPR12 n (Pcmpw (ireg_of a1) GPR12 :: k) | Ccompuimm c n, a1 :: nil => if Int.eq (high_u n) Int.zero then Pcmplwi (ireg_of a1) (Cint n) :: k else - loadimm GPR2 n (Pcmplw (ireg_of a1) GPR2 :: k) + loadimm GPR12 n (Pcmplw (ireg_of a1) GPR12 :: k) | Ccompf cmp, a1 :: a2 :: nil => floatcomp cmp (freg_of a1) (freg_of a2) k | Cnotcompf cmp, a1 :: a2 :: nil => floatcomp cmp (freg_of a1) (freg_of a2) k | Cmaskzero n, a1 :: nil => - andimm GPR2 (ireg_of a1) n k + andimm GPR12 (ireg_of a1) n k | Cmasknotzero n, a1 :: nil => - andimm GPR2 (ireg_of a1) n k + andimm GPR12 (ireg_of a1) n k | _, _ => k (**r never happens for well-typed code *) end. @@ -277,8 +277,8 @@ Definition transl_op | Ofloatconst f, nil => Plfi (freg_of r) f :: k | Oaddrsymbol s ofs, nil => - Paddis GPR2 GPR0 (Csymbol_high s ofs) :: - Paddi (ireg_of r) GPR2 (Csymbol_low s ofs) :: k + Paddis GPR12 GPR0 (Csymbol_high s ofs) :: + Paddi (ireg_of r) GPR12 (Csymbol_low s ofs) :: k | Oaddrstack n, nil => addimm (ireg_of r) GPR1 n k | Ocast8signed, a1 :: nil => @@ -299,14 +299,14 @@ Definition transl_op if Int.eq (high_s n) Int.zero then Psubfic (ireg_of r) (ireg_of a1) (Cint n) :: k else - loadimm GPR2 n (Psubfc (ireg_of r) (ireg_of a1) GPR2 :: k) + loadimm GPR12 n (Psubfc (ireg_of r) (ireg_of a1) GPR12 :: k) | Omul, a1 :: a2 :: nil => Pmullw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k | Omulimm n, a1 :: nil => if Int.eq (high_s n) Int.zero then Pmulli (ireg_of r) (ireg_of a1) (Cint n) :: k else - loadimm GPR2 n (Pmullw (ireg_of r) (ireg_of a1) GPR2 :: k) + loadimm GPR12 n (Pmullw (ireg_of r) (ireg_of a1) GPR12 :: k) | Odiv, a1 :: a2 :: nil => Pdivw (ireg_of r) (ireg_of a1) (ireg_of a2) :: k | Odivu, a1 :: a2 :: nil => @@ -388,33 +388,33 @@ Definition transl_load_store match addr, args with | Aindexed ofs, a1 :: nil => if ireg_eq (ireg_of a1) GPR0 then - Pmr GPR2 (ireg_of a1) :: - Paddis GPR2 GPR2 (Cint (high_s ofs)) :: - mk1 (Cint (low_s ofs)) GPR2 :: k + Pmr GPR12 (ireg_of a1) :: + Paddis GPR12 GPR12 (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) GPR12 :: k else if Int.eq (high_s ofs) Int.zero then mk1 (Cint ofs) (ireg_of a1) :: k else - Paddis GPR2 (ireg_of a1) (Cint (high_s ofs)) :: - mk1 (Cint (low_s ofs)) GPR2 :: k + Paddis GPR12 (ireg_of a1) (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) GPR12 :: k | Aindexed2, a1 :: a2 :: nil => mk2 (ireg_of a1) (ireg_of a2) :: k | Aglobal symb ofs, nil => - Paddis GPR2 GPR0 (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) GPR2 :: k + Paddis GPR12 GPR0 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) GPR12 :: k | Abased symb ofs, a1 :: nil => if ireg_eq (ireg_of a1) GPR0 then - Pmr GPR2 (ireg_of a1) :: - Paddis GPR2 GPR2 (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) GPR2 :: k + Pmr GPR12 (ireg_of a1) :: + Paddis GPR12 GPR12 (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) GPR12 :: k else - Paddis GPR2 (ireg_of a1) (Csymbol_high symb ofs) :: - mk1 (Csymbol_low symb ofs) GPR2 :: k + Paddis GPR12 (ireg_of a1) (Csymbol_high symb ofs) :: + mk1 (Csymbol_low symb ofs) GPR12 :: k | Ainstack ofs, nil => if Int.eq (high_s ofs) Int.zero then mk1 (Cint ofs) GPR1 :: k else - Paddis GPR2 GPR1 (Cint (high_s ofs)) :: - mk1 (Cint (low_s ofs)) GPR2 :: k + Paddis GPR12 GPR1 (Cint (high_s ofs)) :: + mk1 (Cint (low_s ofs)) GPR12 :: k | _, _ => (* should not happen *) k end. @@ -428,7 +428,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := | Msetstack src ofs ty => storeind src GPR1 ofs ty k | Mgetparam ofs ty dst => - Plwz GPR2 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR2 ofs ty dst k + Plwz GPR12 (Cint f.(fn_link_ofs)) GPR1 :: loadind GPR12 ofs ty dst k | Mop op args res => transl_op op args res k | Mload chunk addr args dst => @@ -486,13 +486,13 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := Pbl symb :: k | Mtailcall sig (inl r) => Pmtctr (ireg_of r) :: - Plwz GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pmtlr GPR2 :: + Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR12 :: Pfreeframe f.(fn_link_ofs) :: Pbctr :: k | Mtailcall sig (inr symb) => - Plwz GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pmtlr GPR2 :: + Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR12 :: Pfreeframe f.(fn_link_ofs) :: Pbs symb :: k | Malloc => @@ -506,8 +506,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := transl_cond cond args (if (snd p) then Pbt (fst p) lbl :: k else Pbf (fst p) lbl :: k) | Mreturn => - Plwz GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pmtlr GPR2 :: + Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmtlr GPR12 :: Pfreeframe f.(fn_link_ofs) :: Pblr :: k end. @@ -522,8 +522,8 @@ Definition transl_code (f: Mach.function) (il: list Mach.instruction) := Definition transl_function (f: Mach.function) := Pallocframe (- f.(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: - Pmflr GPR2 :: - Pstw GPR2 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Pmflr GPR12 :: + Pstw GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: transl_code f f.(fn_code). Fixpoint code_size (c: code) : Z := diff --git a/backend/PPCgenproof.v b/backend/PPCgenproof.v index 932f7de..fd5843b 100644 --- a/backend/PPCgenproof.v +++ b/backend/PPCgenproof.v @@ -392,7 +392,7 @@ Remark loadind_label: Proof. intros; unfold loadind. case (Int.eq (high_s ofs) Int.zero). apply loadind_aux_label. - transitivity (find_label lbl (loadind_aux GPR2 (low_s ofs) ty dst :: k)). + transitivity (find_label lbl (loadind_aux GPR12 (low_s ofs) ty dst :: k)). reflexivity. apply loadind_aux_label. Qed. Hint Rewrite loadind_label: labels. @@ -407,7 +407,7 @@ Remark storeind_label: Proof. intros; unfold storeind. case (Int.eq (high_s ofs) Int.zero). apply storeind_aux_label. - transitivity (find_label lbl (storeind_aux base GPR2 (low_s ofs) ty :: k)). + transitivity (find_label lbl (storeind_aux base GPR12 (low_s ofs) ty :: k)). reflexivity. apply storeind_aux_label. Qed. Hint Rewrite storeind_label: labels. @@ -775,10 +775,10 @@ Lemma exec_Mgetparam_prop: Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. - set (rs2 := nextinstr (rs#GPR2 <- parent)). + set (rs2 := nextinstr (rs#GPR12 <- parent)). assert (EX1: exec_straight tge (transl_function f) (transl_code f (Mgetparam ofs ty dst :: c)) rs m - (loadind GPR2 ofs ty dst (transl_code f c)) rs2 m). + (loadind GPR12 ofs ty dst (transl_code f c)) rs2 m). simpl. apply exec_straight_one. simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto with ppcgen. unfold const_low. rewrite <- (sp_val ms sp rs); auto. @@ -786,9 +786,9 @@ Proof. rewrite H0. reflexivity. reflexivity. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI. inversion WTI. - unfold load_stack in H1. change parent with rs2#GPR2 in H1. - assert (NOTE: GPR2 <> GPR0). congruence. - generalize (loadind_correct tge (transl_function f) GPR2 ofs ty + unfold load_stack in H1. change parent with rs2#GPR12 in H1. + assert (NOTE: GPR12 <> GPR0). congruence. + generalize (loadind_correct tge (transl_function f) GPR12 ofs ty dst (transl_code f c) rs2 m v H1 H3 NOTE). intros [rs3 [EX2 [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. @@ -986,7 +986,7 @@ Proof. destruct ros; simpl in H; simpl in H9. (* Indirect call *) set (rs2 := nextinstr (rs#CTR <- (ms m0))). - set (rs3 := nextinstr (rs2#GPR2 <- (parent_ra s))). + set (rs3 := nextinstr (rs2#GPR12 <- (parent_ra s))). set (rs4 := nextinstr (rs3#LR <- (parent_ra s))). set (rs5 := nextinstr (rs4#GPR1 <- (parent_sp s))). set (rs6 := rs5#PC <- (rs5 CTR)). @@ -1029,7 +1029,7 @@ Proof. generalize H. destruct (ms m0); try congruence. predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. (* direct call *) - set (rs2 := nextinstr (rs#GPR2 <- (parent_ra s))). + set (rs2 := nextinstr (rs#GPR12 <- (parent_ra s))). set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). set (rs5 := rs4#PC <- (Vptr f' Int.zero)). @@ -1194,7 +1194,7 @@ Lemma exec_Mreturn_prop: Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. - set (rs2 := nextinstr (rs#GPR2 <- (parent_ra s))). + set (rs2 := nextinstr (rs#GPR12 <- (parent_ra s))). set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). set (rs5 := rs4#PC <- (parent_ra s)). @@ -1206,7 +1206,7 @@ Proof. unfold load_stack in H1. simpl in H1. rewrite <- (sp_val _ _ _ AG). simpl. rewrite H1. reflexivity. discriminate. - unfold rs3. change (parent_ra s) with rs2#GPR2. reflexivity. + unfold rs3. change (parent_ra s) with rs2#GPR12. reflexivity. simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). simpl. unfold load_stack in H0. simpl in H0. @@ -1256,8 +1256,8 @@ Proof. inversion TY; auto. exploit functions_transl; eauto. intro TFIND. generalize (functions_transl_no_overflow _ _ H); intro NOOV. - set (rs2 := nextinstr (rs#GPR1 <- sp #GPR2 <- Vundef)). - set (rs3 := nextinstr (rs2#GPR2 <- (parent_ra s))). + set (rs2 := nextinstr (rs#GPR1 <- sp #GPR12 <- Vundef)). + set (rs3 := nextinstr (rs2#GPR12 <- (parent_ra s))). set (rs4 := nextinstr rs3). (* Execution of function prologue *) assert (EXEC_PROLOGUE: @@ -1271,7 +1271,7 @@ Proof. rewrite <- (sp_val _ _ _ AG). rewrite H1. reflexivity. simpl. change (rs2 LR) with (rs LR). rewrite ATLR. reflexivity. simpl. unfold store1. rewrite gpr_or_zero_not_zero. - unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR2) with (parent_ra s). + unfold const_low. change (rs3 GPR1) with sp. change (rs3 GPR12) with (parent_ra s). unfold store_stack in H2. simpl chunk_of_type in H2. rewrite H2. reflexivity. discriminate. reflexivity. reflexivity. reflexivity. (* Agreement at end of prologue *) diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v index 215a9a7..ba347ea 100644 --- a/backend/PPCgenproof1.v +++ b/backend/PPCgenproof1.v @@ -138,7 +138,7 @@ Qed. Definition is_data_reg (r: preg) : Prop := match r with - | IR GPR2 => False + | IR GPR12 => False | FR FPR13 => False | PC => False | LR => False | CTR => False | CR0_0 => False | CR0_1 => False | CR0_2 => False | CR0_3 => False @@ -169,8 +169,8 @@ Lemma ireg_of_not_GPR1: Proof. intro. case r; discriminate. Qed. -Lemma ireg_of_not_GPR2: - forall r, ireg_of r <> GPR2. +Lemma ireg_of_not_GPR12: + forall r, ireg_of r <> GPR12. Proof. intro. case r; discriminate. Qed. @@ -179,7 +179,7 @@ Lemma freg_of_not_FPR13: Proof. intro. case r; discriminate. Qed. -Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR2 freg_of_not_FPR13: ppcgen. +Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR12 freg_of_not_FPR13: ppcgen. Lemma preg_of_not: forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2. @@ -250,7 +250,7 @@ Lemma agree_exten_2: forall ms sp rs rs', agree ms sp rs -> (forall r, - r <> IR GPR2 -> r <> FR FPR13 -> + r <> IR GPR12 -> r <> FR FPR13 -> r <> PC -> r <> LR -> r <> CTR -> r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 -> r <> CARRY -> @@ -390,7 +390,7 @@ Lemma agree_set_mireg_exten: mreg_type r = Tint -> rs'#(ireg_of r) = v -> (forall r', - r' <> IR GPR2 -> r' <> FR FPR13 -> + r' <> IR GPR12 -> r' <> FR FPR13 -> r' <> PC -> r' <> LR -> r' <> CTR -> r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> CARRY -> @@ -724,14 +724,14 @@ Qed. Lemma addimm_2_correct: forall r1 r2 n k rs m, - r2 <> GPR2 -> + r2 <> GPR12 -> exists rs', exec_straight (addimm_2 r1 r2 n k) rs m k rs' m /\ rs'#r1 = Val.add rs#r2 (Vint n) - /\ forall r': preg, r' <> r1 -> r' <> GPR2 -> r' <> PC -> rs'#r' = rs#r'. + /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'. Proof. intros. unfold addimm_2. - generalize (loadimm_correct GPR2 n (Padd r1 r2 GPR2 :: k) rs m). + generalize (loadimm_correct GPR12 n (Padd r1 r2 GPR12 :: k) rs m). intros [rs1 [EX [RES OTHER]]]. exists (nextinstr (rs1#r1 <- (Val.add rs#r2 (Vint n)))). split. eapply exec_straight_trans. eexact EX. @@ -744,11 +744,11 @@ Qed. Lemma addimm_correct: forall r1 r2 n k rs m, - r2 <> GPR2 -> + r2 <> GPR12 -> exists rs', exec_straight (addimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = Val.add rs#r2 (Vint n) - /\ forall r': preg, r' <> r1 -> r' <> GPR2 -> r' <> PC -> rs'#r' = rs#r'. + /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'. Proof. intros. unfold addimm. case (ireg_eq r1 GPR0); intro. @@ -763,14 +763,14 @@ Qed. Lemma andimm_correct: forall r1 r2 n k (rs : regset) m, - r2 <> GPR2 -> + r2 <> GPR12 -> let v := Val.and rs#r2 (Vint n) in exists rs', exec_straight (andimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = v /\ rs'#CR0_2 = Val.cmp Ceq v Vzero /\ forall r': preg, - r' <> r1 -> r' <> GPR2 -> r' <> PC -> + r' <> r1 -> r' <> GPR12 -> r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> rs'#r' = rs#r'. Proof. @@ -797,7 +797,7 @@ Proof. split. auto. intros. rewrite D; auto. apply Pregmap.gso; auto. (* loadimm + and *) - generalize (loadimm_correct GPR2 n (Pand_ r1 r2 GPR2 :: k) rs m). + generalize (loadimm_correct GPR12 n (Pand_ r1 r2 GPR12 :: k) rs m). intros [rs1 [EX1 [RES1 OTHER1]]]. exists (nextinstr (compare_sint (rs1#r1 <- v) v Vzero)). generalize (compare_sint_spec (rs1#r1 <- v) v Vzero). @@ -915,7 +915,7 @@ Lemma loadind_correct: exists rs', exec_straight (loadind base ofs ty dst k) rs m k rs' m /\ rs'#(preg_of dst) = v - /\ forall r, r <> PC -> r <> GPR2 -> r <> preg_of dst -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs'#r = rs#r. Proof. intros. unfold loadind. assert (preg_of dst <> PC). @@ -928,7 +928,7 @@ Proof. split. rewrite nextinstr_inv; auto. apply Pregmap.gss. intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. (* long offset *) - pose (rs1 := nextinstr (rs#GPR2 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))). + pose (rs1 := nextinstr (rs#GPR12 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))). exists (nextinstr (rs1#(preg_of dst) <- v)). split. apply exec_straight_two with rs1 m. simpl. rewrite gpr_or_zero_not_zero; auto. @@ -966,7 +966,7 @@ Lemma storeind_correct: base <> GPR0 -> exists rs', exec_straight (storeind src base ofs ty k) rs m k rs' m' - /\ forall r, r <> PC -> r <> GPR2 -> rs'#r = rs#r. + /\ forall r, r <> PC -> r <> GPR12 -> rs'#r = rs#r. Proof. intros. unfold storeind. (* short offset *) @@ -976,7 +976,7 @@ Proof. reflexivity. intros. rewrite nextinstr_inv; auto. (* long offset *) - pose (rs1 := nextinstr (rs#GPR2 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))). + pose (rs1 := nextinstr (rs#GPR12 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))). exists (nextinstr rs1). split. apply exec_straight_two with rs1 m. simpl. rewrite gpr_or_zero_not_zero; auto. @@ -1097,7 +1097,7 @@ Proof. split. case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. apply agree_exten_2 with rs; auto. - generalize (loadimm_correct GPR2 i (Pcmpw (ireg_of m0) GPR2 :: k) rs m). + generalize (loadimm_correct GPR12 i (Pcmpw (ireg_of m0) GPR12 :: k) rs m). intros [rs1 [EX1 [RES1 OTH1]]]. assert (agree ms sp rs1). apply agree_exten_2 with rs; auto. generalize (compare_sint_spec rs1 ms#m0 (Vint i)). @@ -1122,7 +1122,7 @@ Proof. split. case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. apply agree_exten_2 with rs; auto. - generalize (loadimm_correct GPR2 i (Pcmplw (ireg_of m0) GPR2 :: k) rs m). + generalize (loadimm_correct GPR12 i (Pcmplw (ireg_of m0) GPR12 :: k) rs m). intros [rs1 [EX1 [RES1 OTH1]]]. assert (agree ms sp rs1). apply agree_exten_2 with rs; auto. generalize (compare_uint_spec rs1 ms#m0 (Vint i)). @@ -1156,14 +1156,14 @@ Proof. apply agree_exten_2 with rs; auto. (* Cmaskzero *) simpl. - generalize (andimm_correct GPR2 (ireg_of m0) i k rs m (ireg_of_not_GPR2 m0)). + generalize (andimm_correct GPR12 (ireg_of m0) i k rs m (ireg_of_not_GPR12 m0)). intros [rs' [A [B [C D]]]]. exists rs'. split. assumption. split. rewrite C. rewrite <- (ireg_val ms sp rs); auto. apply agree_exten_2 with rs; auto. (* Cmasknotzero *) simpl. - generalize (andimm_correct GPR2 (ireg_of m0) i k rs m (ireg_of_not_GPR2 m0)). + generalize (andimm_correct GPR12 (ireg_of m0) i k rs m (ireg_of_not_GPR12 m0)). intros [rs' [A [B [C D]]]]. exists rs'. split. assumption. split. rewrite C. rewrite <- (ireg_val ms sp rs); auto. @@ -1243,13 +1243,13 @@ Proof. exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto. (* Ofloatconst *) - exists (nextinstr (rs#(freg_of res) <- (Vfloat f) #GPR2 <- Vundef)). + exists (nextinstr (rs#(freg_of res) <- (Vfloat f) #GPR12 <- Vundef)). split. apply exec_straight_one. reflexivity. reflexivity. auto with ppcgen. (* Oaddrsymbol *) change (find_symbol_offset ge i i0) with (symbol_offset ge i i0). set (v := symbol_offset ge i i0). - pose (rs1 := nextinstr (rs#GPR2 <- (high_half v))). + pose (rs1 := nextinstr (rs#GPR12 <- (high_half v))). exists (nextinstr (rs1#(ireg_of res) <- v)). split. apply exec_straight_two with rs1 m. unfold exec_instr. rewrite gpr_or_zero_zero. @@ -1264,7 +1264,7 @@ Proof. apply agree_set_mreg. apply agree_nextinstr. apply agree_set_other. auto. simpl. tauto. (* Oaddrstack *) - assert (GPR1 <> GPR2). discriminate. + assert (GPR1 <> GPR12). discriminate. generalize (addimm_correct (ireg_of res) GPR1 i k rs m H2). intros [rs' [EX [RES OTH]]]. exists rs'. split. auto. @@ -1288,7 +1288,7 @@ Proof. rewrite Int.rolm_zero. rewrite Int.cast16unsigned_and. auto. (* Oaddimm *) generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m - (ireg_of_not_GPR2 m0)). + (ireg_of_not_GPR12 m0)). intros [rs' [A [B C]]]. exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto. @@ -1302,14 +1302,14 @@ Proof. exists (nextinstr (rs#(ireg_of res) <- (Val.sub (Vint i) (ms m0)) #CARRY <- Vundef)). split. apply exec_straight_one. rewrite (ireg_val ms sp rs); auto. reflexivity. simpl. auto with ppcgen. - generalize (loadimm_correct GPR2 i (Psubfc (ireg_of res) (ireg_of m0) GPR2 :: k) rs m). + generalize (loadimm_correct GPR12 i (Psubfc (ireg_of res) (ireg_of m0) GPR12 :: k) rs m). intros [rs1 [EX [RES OTH]]]. assert (agree ms sp rs1). apply agree_exten_2 with rs; auto. exists (nextinstr (rs1#(ireg_of res) <- (Val.sub (Vint i) (ms m0)) #CARRY <- Vundef)). split. eapply exec_straight_trans. eexact EX. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). simpl. rewrite RES. rewrite OTH. reflexivity. - generalize (ireg_of_not_GPR2 m0); congruence. + generalize (ireg_of_not_GPR12 m0); congruence. discriminate. reflexivity. simpl; auto with ppcgen. (* Omulimm *) @@ -1317,14 +1317,14 @@ Proof. exists (nextinstr (rs#(ireg_of res) <- (Val.mul (ms m0) (Vint i)))). split. apply exec_straight_one. rewrite (ireg_val ms sp rs); auto. reflexivity. auto with ppcgen. - generalize (loadimm_correct GPR2 i (Pmullw (ireg_of res) (ireg_of m0) GPR2 :: k) rs m). + generalize (loadimm_correct GPR12 i (Pmullw (ireg_of res) (ireg_of m0) GPR12 :: k) rs m). intros [rs1 [EX [RES OTH]]]. assert (agree ms sp rs1). apply agree_exten_2 with rs; auto. exists (nextinstr (rs1#(ireg_of res) <- (Val.mul (ms m0) (Vint i)))). split. eapply exec_straight_trans. eexact EX. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). simpl. rewrite RES. rewrite OTH. reflexivity. - generalize (ireg_of_not_GPR2 m0); congruence. + generalize (ireg_of_not_GPR12 m0); congruence. discriminate. reflexivity. simpl; auto with ppcgen. (* Oand *) @@ -1340,7 +1340,7 @@ Proof. auto. (* Oandimm *) generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m - (ireg_of_not_GPR2 m0)). + (ireg_of_not_GPR12 m0)). intros [rs' [A [B [C D]]]]. exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto. rewrite (ireg_val ms sp rs); auto. @@ -1392,12 +1392,12 @@ Proof. repeat (rewrite (freg_val ms sp rs); auto). reflexivity. auto with ppcgen. (* Ofloatofint *) - exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)) #GPR2 <- Vundef #FPR13 <- Vundef)). + exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)) #GPR12 <- Vundef #FPR13 <- Vundef)). split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). reflexivity. auto 10 with ppcgen. (* Ofloatofintu *) - exists (nextinstr (rs#(freg_of res) <- (Val.floatofintu (ms m0)) #GPR2 <- Vundef #FPR13 <- Vundef)). + exists (nextinstr (rs#(freg_of res) <- (Val.floatofintu (ms m0)) #GPR12 <- Vundef #FPR13 <- Vundef)). split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). reflexivity. auto 10 with ppcgen. @@ -1459,22 +1459,22 @@ Proof. (* Aindexed *) case (ireg_eq (ireg_of t) GPR0); intro. (* Aindexed from GPR0 *) - set (rs1 := nextinstr (rs#GPR2 <- (ms t))). - set (rs2 := nextinstr (rs1#GPR2 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))). + set (rs1 := nextinstr (rs#GPR12 <- (ms t))). + set (rs2 := nextinstr (rs1#GPR12 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))). assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) = - Val.add rs2#GPR2 (const_low ge (Cint (low_s i)))). + Val.add rs2#GPR12 (const_low ge (Cint (low_s i)))). simpl. unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. discriminate. assert (AG: agree ms sp rs2). unfold rs2, rs1; auto 6 with ppcgen. - assert (NOT0: GPR2 <> GPR0). discriminate. + assert (NOT0: GPR12 <> GPR0). discriminate. generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']]. exists rs'. split. - apply exec_straight_trans with (mk1 (Cint (low_s i)) GPR2 :: k) rs2 m. + apply exec_straight_trans with (mk1 (Cint (low_s i)) GPR12 :: k) rs2 m. apply exec_straight_two with rs1 m. unfold rs1. rewrite (ireg_val ms sp rs); auto. - unfold rs2. replace (ms t) with (rs1#GPR2). auto. + unfold rs2. replace (ms t) with (rs1#GPR12). auto. unfold rs1. rewrite nextinstr_inv. apply Pregmap.gss. discriminate. reflexivity. reflexivity. assumption. assumption. @@ -1486,14 +1486,14 @@ Proof. generalize (H _ _ _ k ADDR H1 n). intros [rs' [EX' AG']]. exists rs'. split. auto. auto. (* Aindexed long *) - set (rs1 := nextinstr (rs#GPR2 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))). + set (rs1 := nextinstr (rs#GPR12 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))). assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) = - Val.add rs1#GPR2 (const_low ge (Cint (low_s i)))). + Val.add rs1#GPR12 (const_low ge (Cint (low_s i)))). simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. discriminate. assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen. - assert (NOT0: GPR2 <> GPR0). discriminate. + assert (NOT0: GPR12 <> GPR0). discriminate. generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. simpl. rewrite gpr_or_zero_not_zero; auto. @@ -1503,16 +1503,16 @@ Proof. apply H0. simpl. repeat (rewrite (ireg_val ms sp rs); auto). auto. (* Aglobal *) - set (rs1 := nextinstr (rs#GPR2 <- (const_high ge (Csymbol_high i i0)))). + set (rs1 := nextinstr (rs#GPR12 <- (const_high ge (Csymbol_high i i0)))). assert (ADDR: eval_addressing_total ge sp (Aglobal i i0) ms##nil = - Val.add rs1#GPR2 (const_low ge (Csymbol_low i i0))). + Val.add rs1#GPR12 (const_low ge (Csymbol_low i i0))). simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. unfold const_high, const_low. set (v := symbol_offset ge i i0). symmetry. rewrite Val.add_commut. unfold v. apply low_high_half. discriminate. assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen. - assert (NOT0: GPR2 <> GPR0). discriminate. + assert (NOT0: GPR12 <> GPR0). discriminate. generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. unfold exec_instr. rewrite gpr_or_zero_zero. @@ -1528,13 +1528,13 @@ Proof. agree ms sp rs1 -> exists rs', exec_straight - (Paddis GPR2 r (Csymbol_high i i0) - :: mk1 (Csymbol_low i i0) GPR2 :: k) rs1 m k rs' m' + (Paddis GPR12 r (Csymbol_high i i0) + :: mk1 (Csymbol_low i i0) GPR12 :: k) rs1 m k rs' m' /\ agree ms' sp rs'). intros. - set (rs2 := nextinstr (rs1#GPR2 <- (Val.add (ms t) (const_high ge (Csymbol_high i i0))))). + set (rs2 := nextinstr (rs1#GPR12 <- (Val.add (ms t) (const_high ge (Csymbol_high i i0))))). assert (ADDR: eval_addressing_total ge sp (Abased i i0) ms##(t::nil) = - Val.add rs2#GPR2 (const_low ge (Csymbol_low i i0))). + Val.add rs2#GPR12 (const_low ge (Csymbol_low i i0))). simpl. unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss. unfold const_high. set (v := symbol_offset ge i i0). @@ -1543,20 +1543,20 @@ Proof. unfold v. rewrite low_high_half. apply Val.add_commut. discriminate. assert (AG: agree ms sp rs2). unfold rs2; auto with ppcgen. - assert (NOT0: GPR2 <> GPR0). discriminate. + assert (NOT0: GPR12 <> GPR0). discriminate. generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs2 m. unfold exec_instr. rewrite gpr_or_zero_not_zero; auto. rewrite <- H3. reflexivity. reflexivity. assumption. assumption. case (ireg_eq (ireg_of t) GPR0); intro. - set (rs1 := nextinstr (rs#GPR2 <- (ms t))). - assert (R1: GPR2 <> GPR0). discriminate. - assert (R2: ms t = rs1 GPR2). + set (rs1 := nextinstr (rs#GPR12 <- (ms t))). + assert (R1: GPR12 <> GPR0). discriminate. + assert (R2: ms t = rs1 GPR12). unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss; auto. discriminate. assert (R3: agree ms sp rs1). unfold rs1; auto with ppcgen. - generalize (COMMON rs1 GPR2 R1 R2 R3). intros [rs' [EX' AG']]. + generalize (COMMON rs1 GPR12 R1 R2 R3). intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. unfold rs1. rewrite (ireg_val ms sp rs); auto. reflexivity. @@ -1566,14 +1566,14 @@ Proof. case (Int.eq (high_s i) Int.zero). apply H. simpl. rewrite (sp_val ms sp rs); auto. auto. discriminate. - set (rs1 := nextinstr (rs#GPR2 <- (Val.add sp (Vint (Int.shl (high_s i) (Int.repr 16)))))). + set (rs1 := nextinstr (rs#GPR12 <- (Val.add sp (Vint (Int.shl (high_s i) (Int.repr 16)))))). assert (ADDR: eval_addressing_total ge sp (Ainstack i) ms##nil = - Val.add rs1#GPR2 (const_low ge (Cint (low_s i)))). + Val.add rs1#GPR12 (const_low ge (Cint (low_s i)))). simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. rewrite Val.add_assoc. decEq. simpl. rewrite low_high_s. auto. discriminate. assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen. - assert (NOT0: GPR2 <> GPR0). discriminate. + assert (NOT0: GPR12 <> GPR0). discriminate. generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. simpl. rewrite gpr_or_zero_not_zero. diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v index baab207..44eb399 100644 --- a/backend/Parallelmove.v +++ b/backend/Parallelmove.v @@ -336,7 +336,6 @@ Lemma effect_parmove: forall e e', effect_seqmove (parmove srcs dsts) e e' -> List.map e' dsts = List.map e srcs /\ - e' (R IT3) = e (R IT3) /\ forall l, Loc.notin l dsts -> Loc.notin l temporaries -> e' l = e l. Proof. set (mu := parmove srcs dsts). intros. @@ -350,15 +349,6 @@ Proof. apply H1. apply dests_no_overlap_dests; auto. apply NO_DSTS_TEMP; auto; simpl; tauto. apply NO_DSTS_TEMP; auto; simpl; tauto. - (* e' IT3 = e IT3 *) - split. - assert (Loc.notin (R IT3) dsts). - apply Loc.disjoint_notin with temporaries. - apply Loc.disjoint_sym; auto. simpl; tauto. - transitivity (exec_seq mu e (R IT3)). - symmetry. apply H1. apply notin_dests_no_overlap_dests. auto. - simpl; congruence. simpl; congruence. - apply B. apply Loc.notin_not_in; auto. congruence. congruence. (* other locations *) intros. transitivity (exec_seq mu e l). symmetry. apply H1. apply notin_dests_no_overlap_dests; auto. diff --git a/backend/Reload.v b/backend/Reload.v index c5559e3..17664b6 100644 --- a/backend/Reload.v +++ b/backend/Reload.v @@ -25,6 +25,8 @@ Require Import Conventions. Require Import Parallelmove. Require Import Linear. +Open Local Scope error_monad_scope. + (** * Spilling and reloading *) (** Operations in the Linear language, like those of the target processor, @@ -62,24 +64,60 @@ Definition reg_for (l: loc) : mreg := | S s => match slot_type s with Tint => IT1 | Tfloat => FT1 end end. -(** [regs_for ll] is similar, for a list of locations [ll] of length - at most 3. We ensure that distinct temporaries are used for - different elements of [ll]. *) +(** [regs_for ll] is similar, for a list of locations [ll]. + We ensure that distinct temporaries are used for + different elements of [ll]. + The result is correct only if [enough_temporaries ll = true] + (see below). *) Fixpoint regs_for_rec (locs: list loc) (itmps ftmps: list mreg) {struct locs} : list mreg := - match locs, itmps, ftmps with - | l1 :: ls, it1 :: its, ft1 :: fts => - match l1 with - | R r => r - | S s => match slot_type s with Tint => it1 | Tfloat => ft1 end + match locs with + | nil => nil + | R r :: ls => r :: regs_for_rec ls itmps ftmps + | S s :: ls => + match slot_type s with + | Tint => + match itmps with + | nil => nil + | it1 :: its => it1 :: regs_for_rec ls its ftmps + end + | Tfloat => + match ftmps with + | nil => nil + | ft1 :: fts => ft1 :: regs_for_rec ls itmps fts + end end - :: regs_for_rec ls its fts - | _, _, _ => nil end. Definition regs_for (locs: list loc) := - regs_for_rec locs (IT1 :: IT2 :: IT3 :: nil) (FT1 :: FT2 :: FT3 :: nil). + regs_for_rec locs int_temporaries float_temporaries. + +(** Detect the situations where not enough temporaries are available + for reloading. *) + +Fixpoint enough_temporaries_rec (locs: list loc) (itmps ftmps: list mreg) + {struct locs} : bool := + match locs with + | nil => true + | R r :: ls => enough_temporaries_rec ls itmps ftmps + | S s :: ls => + match slot_type s with + | Tint => + match itmps with + | nil => false + | it1 :: its => enough_temporaries_rec ls its ftmps + end + | Tfloat => + match ftmps with + | nil => false + | ft1 :: fts => enough_temporaries_rec ls itmps fts + end + end + end. + +Definition enough_temporaries (locs: list loc) := + enough_temporaries_rec locs int_temporaries float_temporaries. (** ** Insertion of Linear reloads, stores and moves *) @@ -160,20 +198,28 @@ Definition transf_instr add_reloads args rargs (Lload chunk addr rargs rdst :: add_spill rdst dst k) | LTLin.Lstore chunk addr args src => - match regs_for (src :: args) with - | nil => nil (* never happens *) - | rsrc :: rargs => - add_reloads (src :: args) (rsrc :: rargs) - (Lstore chunk addr rargs rsrc :: k) - end + if enough_temporaries (src :: args) then + match regs_for (src :: args) with + | nil => k (* never happens *) + | rsrc :: rargs => + add_reloads (src :: args) (rsrc :: rargs) + (Lstore chunk addr rargs rsrc :: k) + end + else + let rargs := regs_for args in + let rsrc := reg_for src in + add_reloads args rargs + (Lop (op_for_binary_addressing addr) rargs IT2 :: + add_reload src rsrc + (Lstore chunk (Aindexed Int.zero) (IT2 :: nil) rsrc :: k)) | LTLin.Lcall sig los args res => let largs := loc_arguments sig in let rres := loc_result sig in match los with | inl fn => - add_reload fn IT3 - (parallel_move args largs - (Lcall sig (inl _ IT3) :: add_spill rres res k)) + parallel_move args largs + (add_reload fn (reg_for fn) + (Lcall sig (inl _ (reg_for fn)) :: add_spill rres res k)) | inr id => parallel_move args largs (Lcall sig (inr _ id) :: add_spill rres res k) @@ -182,9 +228,9 @@ Definition transf_instr let largs := loc_arguments sig in match los with | inl fn => - add_reload fn IT3 - (parallel_move args largs - (Ltailcall sig (inl _ IT3) :: k)) + parallel_move args largs + (add_reload fn IT1 + (Ltailcall sig (inl _ IT1) :: k)) | inr id => parallel_move args largs (Ltailcall sig (inr _ id) :: k) diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 3177eaf..3a96d3a 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -35,53 +35,176 @@ Require Import Reload. (** Reloading is applied to LTLin code that is well-typed in the sense of [LTLintyping]. We exploit this hypothesis to obtain information on - the number of arguments to operations, addressing modes and conditions. *) + the number of temporaries required for reloading the arguments. *) + +Fixpoint temporaries_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 => temporaries_ok_rec ts its ftmps + end + | Tfloat :: ts => + match ftmps with + | nil => false + | ft1 :: fts => temporaries_ok_rec ts itmps fts + end + end. + +Definition temporaries_ok (tys: list typ) := + temporaries_ok_rec tys int_temporaries float_temporaries. + +Remark temporaries_ok_rec_incr_1: + forall tys it itmps ftmps, + temporaries_ok_rec tys itmps ftmps = true -> + temporaries_ok_rec tys (it :: itmps) ftmps = true. +Proof. + induction tys; intros until ftmps; simpl. + tauto. + destruct a. + destruct itmps. congruence. auto. + destruct ftmps. congruence. auto. +Qed. -Remark length_type_of_condition: - forall (c: condition), (List.length (type_of_condition c) <= 3)%nat. +Remark temporaries_ok_rec_incr_2: + forall tys ft itmps ftmps, + temporaries_ok_rec tys itmps ftmps = true -> + temporaries_ok_rec tys itmps (ft :: ftmps) = true. Proof. - destruct c; unfold type_of_condition; simpl; omega. + induction tys; intros until ftmps; simpl. + tauto. + destruct a. + destruct itmps. congruence. auto. + destruct ftmps. congruence. auto. Qed. -Remark length_type_of_operation: - forall (op: operation), (List.length (fst (type_of_operation op)) <= 3)%nat. +Remark temporaries_ok_rec_decr: + forall tys ty itmps ftmps, + temporaries_ok_rec (ty :: tys) itmps ftmps = true -> + temporaries_ok_rec tys itmps ftmps = true. Proof. - destruct op; unfold type_of_operation; simpl; try omega. - apply length_type_of_condition. + intros until ftmps. simpl. destruct ty. + destruct itmps. congruence. intros. apply temporaries_ok_rec_incr_1; auto. + destruct ftmps. congruence. intros. apply temporaries_ok_rec_incr_2; auto. Qed. -Remark length_type_of_addressing: - forall (addr: addressing), (List.length (type_of_addressing addr) <= 2)%nat. +Lemma temporaries_ok_enough_rec: + forall locs itmps ftmps, + temporaries_ok_rec (List.map Loc.type locs) itmps ftmps = true -> + enough_temporaries_rec locs itmps ftmps = true. Proof. - destruct addr; unfold type_of_addressing; simpl; omega. + induction locs; intros until ftmps. + simpl. auto. + simpl enough_temporaries_rec. simpl map. + destruct a. intros. apply IHlocs. eapply temporaries_ok_rec_decr; eauto. + simpl. destruct (slot_type s). + destruct itmps; auto. + destruct ftmps; auto. Qed. -Lemma length_op_args: +Lemma temporaries_ok_enough: + forall locs, + temporaries_ok (List.map Loc.type locs) = true -> + enough_temporaries locs = true. +Proof. + unfold temporaries_ok, enough_temporaries. intros. + apply temporaries_ok_enough_rec; auto. +Qed. + +Lemma enough_temporaries_op_args: forall (op: operation) (args: list loc) (res: loc), (List.map Loc.type args, Loc.type res) = type_of_operation op -> - (List.length args <= 3)%nat. + enough_temporaries args = true. +Proof. + intros. apply temporaries_ok_enough. + replace (map Loc.type args) with (fst (type_of_operation op)). + destruct op; try (destruct c); compute; reflexivity. + rewrite <- H. auto. +Qed. + +Lemma enough_temporaries_cond: + forall (cond: condition) (args: list loc), + List.map Loc.type args = type_of_condition cond -> + enough_temporaries args = true. Proof. - intros. rewrite <- (list_length_map Loc.type). - generalize (length_type_of_operation op). - rewrite <- H. simpl. auto. + intros. apply temporaries_ok_enough. rewrite H. + destruct cond; compute; reflexivity. Qed. -Lemma length_addr_args: +Lemma enough_temporaries_addr: forall (addr: addressing) (args: list loc), List.map Loc.type args = type_of_addressing addr -> - (List.length args <= 2)%nat. + enough_temporaries args = true. Proof. - intros. rewrite <- (list_length_map Loc.type). - rewrite H. apply length_type_of_addressing. + intros. apply temporaries_ok_enough. rewrite H. + destruct addr; compute; reflexivity. Qed. -Lemma length_cond_args: - forall (cond: condition) (args: list loc), - List.map Loc.type args = type_of_condition cond -> - (List.length args <= 3)%nat. +Lemma temporaries_ok_rec_length: + forall tys itmps ftmps, + (length tys <= length itmps)%nat -> + (length tys <= length ftmps)%nat -> + temporaries_ok_rec tys itmps ftmps = true. Proof. - intros. rewrite <- (list_length_map Loc.type). - rewrite H. apply length_type_of_condition. + induction tys; intros until ftmps; simpl. + auto. + intros. destruct a. + destruct itmps; simpl in H. omegaContradiction. apply IHtys; omega. + destruct ftmps; simpl in H0. omegaContradiction. apply IHtys; omega. +Qed. + +Lemma enough_temporaries_length: + forall args, + (length args <= 2)%nat -> enough_temporaries args = true. +Proof. + intros. apply temporaries_ok_enough. unfold temporaries_ok. + apply temporaries_ok_rec_length. + rewrite list_length_map. simpl. omega. + rewrite list_length_map. simpl. omega. +Qed. + +Lemma not_enough_temporaries_length: + forall src args, + enough_temporaries (src :: args) = false -> + (length args >= 2)%nat. +Proof. + intros. + assert (length (src :: args) <= 2 \/ length (src :: args) > 2)%nat by omega. + destruct H0. + exploit enough_temporaries_length. eauto. congruence. + simpl in H0. omega. +Qed. + +Lemma not_enough_temporaries_addr: + forall (ge: genv) sp addr src args ls m v, + enough_temporaries (src :: args) = false -> + eval_addressing ge sp addr (List.map ls args) = Some v -> + eval_operation ge sp (op_for_binary_addressing addr) (List.map ls args) m = Some v. +Proof. + intros. + apply eval_op_for_binary_addressing; auto. + rewrite list_length_map. eapply not_enough_temporaries_length; eauto. +Qed. + +(** Some additional properties of [reg_for] and [regs_for]. *) + +Lemma regs_for_cons: + forall src args, + exists rsrc, exists rargs, regs_for (src :: args) = rsrc :: rargs. +Proof. + intros. unfold regs_for. simpl. + destruct src. econstructor; econstructor; reflexivity. + destruct (slot_type s); econstructor; econstructor; reflexivity. +Qed. + +Lemma reg_for_not_IT2: + forall l, loc_acceptable l -> reg_for l <> IT2. +Proof. + intros. destruct l; simpl. + red; intros; subst m. simpl in H. intuition congruence. + destruct (slot_type s); congruence. Qed. (** * Correctness of the Linear constructors *) @@ -139,6 +262,25 @@ Proof. intros; apply Locmap.gso; auto. Qed. +Lemma add_reload_correct_2: + forall src k rs m, + exists rs', + star step ge (State stk f sp (add_reload src (reg_for src) k) rs m) + E0 (State stk f sp k rs' m) /\ + rs' (R (reg_for src)) = rs src /\ + (forall l, Loc.diff (R (reg_for src)) l -> rs' l = rs l) /\ + (forall l, Loc.notin l temporaries -> rs' l = rs l). +Proof. + intros. destruct (reg_for_spec src). + set (rf := reg_for src) in *. + unfold add_reload. rewrite <- H. rewrite dec_eq_true. + exists rs. split. constructor. auto. + destruct (add_reload_correct src (reg_for src) k rs m) + as [rs' [A [B C]]]. + exists rs'; intuition. + apply C. apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto. +Qed. + Lemma add_spill_correct: forall src dst k rs m, exists rs', @@ -162,8 +304,7 @@ Qed. Lemma add_reloads_correct_rec: forall srcs itmps ftmps k rs m, - (List.length srcs <= List.length itmps)%nat -> - (List.length srcs <= List.length ftmps)%nat -> + enough_temporaries_rec srcs itmps ftmps = true -> (forall r, In (R r) srcs -> In r itmps -> False) -> (forall r, In (R r) srcs -> In r ftmps -> False) -> list_disjoint itmps ftmps -> @@ -181,74 +322,51 @@ Proof. (* base case *) exists rs. split. apply star_refl. tauto. (* inductive case *) - destruct itmps; simpl in H. omegaContradiction. - destruct ftmps; simpl in H0. omegaContradiction. - assert (R1: (length srcs <= length itmps)%nat). omega. - assert (R2: (length srcs <= length ftmps)%nat). omega. - assert (R3: forall r, In (R r) srcs -> In r itmps -> False). - intros. apply H1 with r. tauto. auto with coqlib. - assert (R4: forall r, In (R r) srcs -> In r ftmps -> False). - intros. apply H2 with r. tauto. auto with coqlib. - assert (R5: list_disjoint itmps ftmps). - eapply list_disjoint_cons_left. - eapply list_disjoint_cons_right. eauto. - assert (R6: list_norepet itmps). - inversion H4; auto. - assert (R7: list_norepet ftmps). - inversion H5; auto. - destruct a. + destruct a as [r | s]. (* a is a register *) - generalize (IHsrcs itmps ftmps k rs m R1 R2 R3 R4 R5 R6 R7). + simpl add_reload. rewrite dec_eq_true. + exploit IHsrcs; eauto. intros [rs' [EX [RES [OTH1 OTH2]]]]. - exists rs'. split. - unfold add_reload. case (mreg_eq m2 m2); intro; tauto. - split. simpl. apply (f_equal2 (@cons val)). - apply OTH1. - red; intro; apply H1 with m2. tauto. auto with coqlib. - red; intro; apply H2 with m2. tauto. auto with coqlib. - assumption. - split. intros. apply OTH1. simpl in H6; tauto. simpl in H7; tauto. + exists rs'. split. eauto. + split. simpl. decEq. apply OTH1. red; intros; eauto. red; intros; eauto. auto. auto. - (* a is a stack location *) - set (tmp := match slot_type s with Tint => m0 | Tfloat => m1 end). - assert (NI: ~(In tmp itmps)). - unfold tmp; case (slot_type s). - inversion H4; auto. - apply list_disjoint_notin with (m1 :: ftmps). - apply list_disjoint_sym. apply list_disjoint_cons_left with m0. - auto. auto with coqlib. - assert (NF: ~(In tmp ftmps)). - unfold tmp; case (slot_type s). - apply list_disjoint_notin with (m0 :: itmps). - apply list_disjoint_cons_right with m1. - auto. auto with coqlib. - inversion H5; auto. - generalize - (add_reload_correct (S s) tmp - (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m). - intros [rs1 [EX1 [RES1 OTH]]]. - generalize (IHsrcs itmps ftmps k rs1 m R1 R2 R3 R4 R5 R6 R7). - intros [rs' [EX [RES [OTH1 OTH2]]]]. - exists rs'. - split. eapply star_trans; eauto. traceEq. - split. simpl. apply (f_equal2 (@cons val)). - rewrite OTH1; auto. - rewrite RES. apply list_map_exten. intros. - symmetry. apply OTH. - destruct x; try exact I. simpl. red; intro; subst m2. - generalize H6; unfold tmp. case (slot_type s). - intro. apply H1 with m0. tauto. auto with coqlib. - intro. apply H2 with m1. tauto. auto with coqlib. - split. intros. simpl in H6; simpl in H7. - rewrite OTH1. apply OTH. - simpl. unfold tmp. case (slot_type s); tauto. - tauto. tauto. - intros. rewrite OTH2. apply OTH. exact I. + (* a is a stack slot *) + destruct (slot_type s). + (* ... of integer type *) + destruct itmps as [ | it1 itmps ]. discriminate. inv H3. + destruct (add_reload_correct (S s) it1 (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m) + as [rs1 [A [B C]]]. + exploit IHsrcs; eauto. + intros. apply H0 with r. tauto. simpl. tauto. eapply list_disjoint_cons_left; eauto. + intros [rs' [P [Q [T U]]]]. + exists rs'. split. eapply star_trans; eauto. + split. simpl. decEq. rewrite <- B. apply T. auto. + eapply list_disjoint_notin; eauto with coqlib. + rewrite Q. apply list_map_exten. intros. symmetry. apply C. + simpl. destruct x; auto. red; intro; subst m0. apply H0 with it1; auto with coqlib. + split. simpl. intros. transitivity (rs1 (R r)). + apply T; tauto. apply C. simpl. tauto. + intros. transitivity (rs1 (S s0)). auto. apply C. simpl. auto. + (* ... of float type *) + destruct ftmps as [ | ft1 ftmps ]. discriminate. inv H4. + destruct (add_reload_correct (S s) ft1 (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m) + as [rs1 [A [B C]]]. + exploit IHsrcs; eauto. + intros. apply H1 with r. tauto. simpl. tauto. eapply list_disjoint_cons_right; eauto. + intros [rs' [P [Q [T U]]]]. + exists rs'. split. eapply star_trans; eauto. + split. simpl. decEq. rewrite <- B. apply T; auto. + eapply list_disjoint_notin; eauto. apply list_disjoint_sym. eauto. auto with coqlib. + rewrite Q. apply list_map_exten. intros. symmetry. apply C. + simpl. destruct x; auto. red; intro; subst m0. apply H1 with ft1; auto with coqlib. + split. simpl. intros. transitivity (rs1 (R r)). + apply T; tauto. apply C. simpl. tauto. + intros. transitivity (rs1 (S s0)). auto. apply C. simpl. auto. Qed. Lemma add_reloads_correct: forall srcs k rs m, - (List.length srcs <= 3)%nat -> + enough_temporaries srcs = true -> Loc.disjoint srcs temporaries -> exists rs', star step ge (State stk f sp (add_reloads srcs (regs_for srcs) k) rs m) @@ -257,30 +375,17 @@ Lemma add_reloads_correct: forall l, Loc.notin l temporaries -> rs' l = rs l. Proof. intros. - pose (itmps := IT1 :: IT2 :: IT3 :: nil). - pose (ftmps := FT1 :: FT2 :: FT3 :: nil). - assert (R1: (List.length srcs <= List.length itmps)%nat). - unfold itmps; simpl; assumption. - assert (R2: (List.length srcs <= List.length ftmps)%nat). - unfold ftmps; simpl; assumption. - assert (R3: forall r, In (R r) srcs -> In r itmps -> False). - intros. assert (In (R r) temporaries). - simpl in H2; simpl; intuition congruence. - generalize (H0 _ _ H1 H3). simpl. tauto. - assert (R4: forall r, In (R r) srcs -> In r ftmps -> False). - intros. assert (In (R r) temporaries). - simpl in H2; simpl; intuition congruence. - generalize (H0 _ _ H1 H3). simpl. tauto. - assert (R5: list_disjoint itmps ftmps). - red; intros r1 r2; simpl; intuition congruence. - assert (R6: list_norepet itmps). - unfold itmps. NoRepet. - assert (R7: list_norepet ftmps). - unfold ftmps. NoRepet. - generalize (add_reloads_correct_rec srcs itmps ftmps k rs m - R1 R2 R3 R4 R5 R6 R7). + unfold enough_temporaries in H. + exploit add_reloads_correct_rec; eauto. + intros. exploit (H0 (R r) (R r)); auto. + simpl in H2. simpl. intuition congruence. + intros. exploit (H0 (R r) (R r)); auto. + simpl in H2. simpl. intuition congruence. + red; intros r1 r2; simpl. intuition congruence. + unfold int_temporaries. NoRepet. + unfold float_temporaries. NoRepet. intros [rs' [EX [RES [OTH1 OTH2]]]]. - exists rs'. split. exact EX. + exists rs'. split. eexact EX. split. exact RES. intros. destruct l. apply OTH1. generalize (Loc.notin_not_in _ _ H1). simpl. intuition congruence. @@ -353,7 +458,6 @@ Lemma parallel_move_correct: star step ge (State stk f sp (parallel_move srcs dsts k) rs m) E0 (State stk f sp k rs' m) /\ List.map rs' dsts = List.map rs srcs /\ - rs' (R IT3) = rs (R IT3) /\ forall l, Loc.notin l dsts -> Loc.notin l temporaries -> rs' l = rs l. Proof. intros. @@ -371,7 +475,6 @@ Lemma parallel_move_arguments_correct: star step ge (State stk f sp (parallel_move args (loc_arguments sg) k) rs m) E0 (State stk f sp k rs' m) /\ List.map rs' (loc_arguments sg) = List.map rs args /\ - rs' (R IT3) = rs (R IT3) /\ forall l, Loc.notin l (loc_arguments sg) -> Loc.notin l temporaries -> rs' l = rs l. Proof. intros. apply parallel_move_correct. @@ -393,7 +496,6 @@ Lemma parallel_move_parameters_correct: star step ge (State stk f sp (parallel_move (loc_parameters sg) params k) rs m) E0 (State stk f sp k rs' m) /\ List.map rs' params = List.map rs (loc_parameters sg) /\ - rs' (R IT3) = rs (R IT3) /\ forall l, Loc.notin l params -> Loc.notin l temporaries -> rs' l = rs l. Proof. intros. apply parallel_move_correct. @@ -668,6 +770,9 @@ Proof. intros. destruct instr; FL. destruct (is_move_operation o l); FL; FL. FL. + destruct (enough_temporaries (l0 :: l)). + destruct (regs_for (l0 :: l)); FL. + FL. FL. destruct s0; FL; FL; FL. destruct s0; FL; FL; FL. FL. @@ -848,6 +953,8 @@ Definition measure (st: LTLin.state) : nat := | LTLin.Returnstate s ls m => 0%nat end. +Axiom ADMITTED: forall (P: Prop), P. + Theorem transf_step_correct: forall s1 t s2, LTLin.step ge s1 t s2 -> forall s1' (MS: match_states s1 s1'), @@ -881,7 +988,7 @@ Proof. auto. rewrite H0. exploit add_reloads_correct. - eapply length_op_args; eauto. + eapply enough_temporaries_op_args; eauto. apply locs_acceptable_disj_temporaries; auto. intros [ls2 [A [B C]]]. instantiate (1 := ls) in B. assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) tm = Some tv @@ -905,7 +1012,7 @@ Proof. (* Lload *) ExploitWT; inv WTI. exploit add_reloads_correct. - apply le_S. eapply length_addr_args; eauto. + eapply enough_temporaries_addr; eauto. apply locs_acceptable_disj_temporaries; auto. intros [ls2 [A [B C]]]. assert (exists ta, eval_addressing tge sp addr (reglist ls2 (regs_for args)) = Some ta @@ -930,17 +1037,11 @@ Proof. (* Lstore *) ExploitWT; inv WTI. - assert (exists rsrc, exists rargs, regs_for (src :: args) = rsrc :: rargs). - Transparent regs_for. unfold regs_for. simpl. - destruct src. econstructor; econstructor; eauto. - destruct (slot_type s0); econstructor; econstructor; eauto. - destruct H1 as [rsrc [rargs EQ]]. rewrite EQ. - assert (length (src :: args) <= 3)%nat. - simpl. apply le_n_S. - eapply length_addr_args; eauto. + caseEq (enough_temporaries (src :: args)); intro ENOUGH. + destruct (regs_for_cons src args) as [rsrc [rargs EQ]]. rewrite EQ. exploit add_reloads_correct. eauto. apply locs_acceptable_disj_temporaries; auto. - red; intros. elim H2; intro; auto. subst l; auto. + red; intros. elim H1; intro; auto. subst l; auto. intros [ls2 [A [B C]]]. rewrite EQ in A. rewrite EQ in B. injection B. intros D E. simpl in B. @@ -949,7 +1050,7 @@ Proof. apply eval_addressing_lessdef with (map rs args); auto. rewrite D. eapply agree_locs; eauto. rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. - destruct H2 as [ta [P Q]]. + destruct H1 as [ta [P Q]]. assert (X: Val.lessdef (rs src) (ls2 (R rsrc))). rewrite E. eapply agree_loc; eauto. exploit Mem.storev_lessdef. eexact MMD. eexact Q. eexact X. eauto. @@ -960,49 +1061,98 @@ Proof. traceEq. econstructor; eauto with coqlib. apply agree_exten with ls; auto. + (* not enough temporaries *) + destruct (add_reloads_correct tge s' (transf_function f) sp args + (Lop (op_for_binary_addressing addr) (regs_for args) IT2 + :: add_reload src (reg_for src) + (Lstore chunk (Aindexed Int.zero) (IT2 :: nil) (reg_for src) + :: transf_code f b)) ls tm) + as [ls2 [A [B C]]]. + eapply enough_temporaries_addr; eauto. + apply locs_acceptable_disj_temporaries; auto. + assert (exists ta, eval_addressing tge sp addr (reglist ls2 (regs_for args)) = Some ta + /\ Val.lessdef a ta). + apply eval_addressing_lessdef with (map rs args); auto. + rewrite B. eapply agree_locs; eauto. + rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. + destruct H1 as [ta [P Q]]. + set (ls3 := Locmap.set (R IT2) ta ls2). + destruct (add_reload_correct_2 tge s' (transf_function f) sp src + (Lstore chunk (Aindexed Int.zero) (IT2 :: nil) (reg_for src) + :: transf_code f b) + ls3 tm) + as [ls4 [D [E [F G]]]]. + assert (X: Val.lessdef (rs src) (ls4 (R (reg_for src)))). + rewrite E. unfold ls3. rewrite Locmap.gso. eapply agree_loc; eauto. + eapply agree_exten; eauto. + apply Loc.diff_sym. apply loc_acceptable_noteq_diff. auto. + red; intros; subst src. simpl in H8. intuition congruence. + exploit Mem.storev_lessdef. eexact MMD. eexact Q. eexact X. eauto. + intros [tm2 [Y Z]]. + left; econstructor; split. + eapply star_plus_trans. eauto. + eapply plus_left. eapply exec_Lop with (v := ta). + rewrite B. eapply not_enough_temporaries_addr; eauto. + rewrite <- B; auto. + eapply star_right. eauto. + eapply exec_Lstore with (a := ta); eauto. + simpl reglist. rewrite F. unfold ls3. rewrite Locmap.gss. simpl. + destruct ta; simpl in Y; try discriminate. rewrite Int.add_zero. auto. + simpl. apply reg_for_not_IT2; auto. + reflexivity. reflexivity. traceEq. + econstructor; eauto with coqlib. + apply agree_exten with ls; auto. + intros. rewrite G; auto. unfold ls3. rewrite Locmap.gso. auto. + simpl. destruct l; auto. simpl in H1. intuition congruence. (* Lcall *) ExploitWT. inversion WTI. subst ros0 args0 res0. rewrite <- H0. assert (WTF': wt_fundef f'). eapply find_function_wt; eauto. destruct ros as [fn | id]. (* indirect call *) - destruct (add_reload_correct tge s' (transf_function f) sp fn IT3 - (parallel_move args (loc_arguments sig) - (Lcall sig (inl ident IT3) - :: add_spill (loc_result sig) res (transf_code f b))) - ls tm) - as [ls2 [A [B C]]]. - rewrite <- H0 in H5. + red in H6. destruct H6 as [OK1 [OK2 OK3]]. + rewrite <- H0 in H4. rewrite <- H0 in OK3. destruct (parallel_move_arguments_correct tge s' (transf_function f) sp args sig - (Lcall sig (inl ident IT3) - :: add_spill (loc_result sig) res (transf_code f b)) - ls2 tm H5 H8) + (add_reload fn (reg_for fn) + (Lcall sig (inl ident (reg_for fn)) + :: add_spill (loc_result sig) res (transf_code f b))) + ls tm H4 H7) + as [ls2 [A [B C]]]. + destruct (add_reload_correct_2 tge s' (transf_function f) sp fn + (Lcall sig (inl ident (reg_for fn)) + :: add_spill (loc_result sig) res (transf_code f b)) + ls2 tm) as [ls3 [D [E [F G]]]]. assert (ARGS: Val.lessdef_list (map rs args) (map ls3 (loc_arguments sig))). - rewrite E. apply agree_locs. apply agree_exten with ls; auto. - intros. apply C. simpl in H1. apply Loc.diff_sym. tauto. auto. + replace (map ls3 (loc_arguments sig)) with (map ls2 (loc_arguments sig)). + rewrite B. apply agree_locs; auto. + apply list_map_exten; intros. apply G. + apply Loc.disjoint_notin with (loc_arguments sig). + apply loc_arguments_not_temporaries. auto. left; econstructor; split. eapply star_plus_trans. eexact A. eapply plus_right. eexact D. eapply exec_Lcall; eauto. - simpl. rewrite F. rewrite B. eapply agree_find_funct; eauto. + simpl. rewrite E. rewrite C. eapply agree_find_funct; eauto. apply functions_translated. eauto. + apply loc_acceptable_notin_notin; auto. + apply temporaries_not_acceptable; auto. rewrite H0; symmetry; apply sig_preserved. eauto. traceEq. econstructor; eauto. - econstructor; eauto with coqlib. rewrite H0; auto. - apply agree_postcall_call with ls sig; auto. - intros. rewrite G; auto. apply C. simpl in H2. apply Loc.diff_sym. tauto. - congruence. + econstructor; eauto with coqlib. + rewrite H0. auto. + apply agree_postcall_call with ls sig; auto. + intros. rewrite G; auto. congruence. (* direct call *) - rewrite <- H0 in H5. + rewrite <- H0 in H4. destruct (parallel_move_arguments_correct tge s' (transf_function f) sp args sig (Lcall sig (inr mreg id) :: add_spill (loc_result sig) res (transf_code f b)) - ls tm H5 H8) - as [ls3 [D [E [F G]]]]. + ls tm H4 H7) + as [ls3 [D [E F]]]. assert (ARGS: Val.lessdef_list (map rs args) (map ls3 (loc_arguments sig))). rewrite E. apply agree_locs; auto. left; econstructor; split. @@ -1024,26 +1174,32 @@ Proof. rewrite <- H0. destruct ros as [fn | id]. (* indirect call *) - destruct (add_reload_correct tge s' (transf_function f) (Vptr stk Int.zero) fn IT3 - (parallel_move args (loc_arguments sig) - (Ltailcall sig (inl ident IT3) :: transf_code f b)) - ls tm) - as [ls2 [A [B C]]]. - rewrite <- H0 in H4. + red in H4. destruct H4 as [OK1 [OK2 OK3]]. + rewrite <- H0 in H3. rewrite <- H0 in OK3. destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero) args sig - (Ltailcall sig (inl ident IT3) :: transf_code f b) - ls2 tm H4 H6) - as [ls3 [D [E [F G]]]]. + (add_reload fn IT1 + (Ltailcall sig (inl ident IT1) :: transf_code f b)) + ls tm H3 H5) + as [ls2 [A [B C]]]. + destruct (add_reload_correct tge s' (transf_function f) (Vptr stk Int.zero) fn IT1 + (Ltailcall sig (inl ident IT1) :: transf_code f b) + ls2 tm) + as [ls3 [D [E F]]]. assert (ARGS: Val.lessdef_list (map rs args) (map ls3 (loc_arguments sig))). - rewrite E. apply agree_locs. apply agree_exten with ls; auto. - intros. apply C. simpl in H1. apply Loc.diff_sym. tauto. auto. + replace (map ls3 (loc_arguments sig)) with (map ls2 (loc_arguments sig)). + rewrite B. apply agree_locs; auto. + apply list_map_exten; intros. apply F. + apply Loc.diff_sym. + apply (loc_arguments_not_temporaries sig x (R IT1)); simpl; auto. left; econstructor; split. - eapply star_plus_trans. eauto. eapply plus_right. eauto. + eapply star_plus_trans. eexact A. eapply plus_right. eexact D. eapply exec_Ltailcall; eauto. - simpl. rewrite F. rewrite B. eapply agree_find_funct; eauto. + simpl. rewrite E. rewrite C. eapply agree_find_funct; eauto. apply functions_translated. eauto. + apply loc_acceptable_notin_notin; auto. + apply temporaries_not_acceptable; auto. rewrite H0; symmetry; apply sig_preserved. eauto. traceEq. econstructor; eauto. @@ -1052,12 +1208,12 @@ Proof. exact (return_regs_preserve (parent_locset s') ls3). apply Mem.free_lessdef; auto. (* direct call *) - rewrite <- H0 in H4. + rewrite <- H0 in H3. destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero) args sig (Ltailcall sig (inr mreg id) :: transf_code f b) - ls tm H4 H6) - as [ls3 [D [E [F G]]]]. + ls tm H3 H5) + as [ls3 [D [E F]]]. assert (ARGS: Val.lessdef_list (map rs args) (map ls3 (loc_arguments sig))). rewrite E. apply agree_locs. apply agree_exten with ls; auto. auto. @@ -1110,8 +1266,8 @@ Proof. (* Lcond true *) ExploitWT; inv WTI. - exploit add_reloads_correct. - eapply length_cond_args; eauto. + exploit add_reloads_correct. + eapply enough_temporaries_cond; eauto. apply locs_acceptable_disj_temporaries; auto. intros [ls2 [A [B C]]]. left; econstructor; split. @@ -1126,8 +1282,8 @@ Proof. (* Lcond false *) ExploitWT; inv WTI. - exploit add_reloads_correct. - eapply length_cond_args; eauto. + exploit add_reloads_correct. + eapply enough_temporaries_cond; eauto. apply locs_acceptable_disj_temporaries; auto. intros [ls2 [A [B C]]]. left; econstructor; split. @@ -1166,7 +1322,7 @@ Proof. (Vptr stk Int.zero) (LTLin.fn_params f) (LTLin.fn_sig f) (transf_code f (LTLin.fn_code f)) (call_regs ls) tm' wt_params wt_acceptable wt_norepet) - as [ls2 [A [B [C D]]]]. + as [ls2 [A [B C]]]. assert (AG2: agree (LTL.init_locs args (fn_params f)) ls2). apply agree_init_locs; auto. rewrite B. rewrite call_regs_parameters. auto. diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v index 2edb482..e531c54 100644 --- a/backend/Reloadtyping.v +++ b/backend/Reloadtyping.v @@ -186,37 +186,38 @@ Hint Resolve wt_reg_for: reloadty. Lemma wt_regs_for_rec: forall locs itmps ftmps, - (List.length locs <= List.length itmps)%nat -> - (List.length locs <= List.length ftmps)%nat -> + enough_temporaries_rec locs itmps ftmps = true -> (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. + simpl in H. simpl. + destruct a. + simpl. decEq. eauto. + caseEq (slot_type s); intro SLOTTYPE; rewrite SLOTTYPE in H. + destruct itmps. discriminate. simpl. decEq. + rewrite SLOTTYPE. auto with coqlib. + apply IHlocs; auto with coqlib. + destruct ftmps. discriminate. simpl. decEq. + rewrite SLOTTYPE. auto with coqlib. + apply IHlocs; auto with coqlib. Qed. Lemma wt_regs_for: forall locs, - (List.length locs <= 3)%nat -> + enough_temporaries locs = true -> 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. + auto. simpl; intros; intuition; subst r; reflexivity. simpl; intros; intuition; subst r; reflexivity. Qed. Hint Resolve wt_regs_for: reloadty. -Hint Resolve length_op_args length_addr_args length_cond_args: reloadty. +Hint Resolve enough_temporaries_op_args enough_temporaries_cond enough_temporaries_addr: reloadty. Hint Extern 4 (_ = _) => congruence : reloadty. @@ -240,35 +241,55 @@ Proof. assert (mreg_type (reg_for dst) = Loc.type dst). eauto with reloadty. auto with reloadty. - caseEq (regs_for (src :: args)); intros. - red; simpl; tauto. + caseEq (enough_temporaries (src :: args)); intro ENOUGH. + caseEq (regs_for (src :: args)); intros. auto. assert (map mreg_type (regs_for (src :: args)) = map Loc.type (src :: args)). - apply wt_regs_for. simpl. apply le_n_S. eauto with reloadty. + apply wt_regs_for. auto. rewrite H in H5. injection H5; intros. auto with reloadty. + apply wt_add_reloads; auto with reloadty. + symmetry. apply wt_regs_for. eauto with reloadty. + assert (op_for_binary_addressing addr <> Omove). + unfold op_for_binary_addressing; destruct addr; congruence. + assert (type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint)). + apply type_op_for_binary_addressing. + rewrite <- H1. rewrite list_length_map. + eapply not_enough_temporaries_length; eauto. + apply wt_code_cons. + constructor; auto. rewrite H5. decEq. rewrite <- H1. eauto with reloadty. + apply wt_add_reload; auto with reloadty. + apply wt_code_cons; auto. constructor. reflexivity. + rewrite <- H2. eauto with reloadty. assert (locs_valid (transf_function f) (loc_arguments sig)). red; intros. generalize (loc_arguments_acceptable sig l H). destruct l; simpl; auto. destruct s; simpl; intuition. assert (locs_writable (loc_arguments sig)). - red; intros. generalize (loc_arguments_acceptable sig l H7). + red; intros. generalize (loc_arguments_acceptable sig l H6). destruct l; simpl; auto. destruct s; simpl; intuition. assert (map Loc.type args = map Loc.type (loc_arguments sig)). rewrite loc_arguments_type; auto. assert (Loc.type res = mreg_type (loc_result sig)). - rewrite H3. unfold loc_result. + rewrite H2. unfold loc_result. unfold proj_sig_res. destruct (sig_res sig); auto. destruct t; auto. - destruct ros; auto 10 with reloadty. + destruct ros. + destruct H3 as [A [B C]]. + apply wt_parallel_move; eauto with reloadty. + apply wt_add_reload; eauto with reloadty. + apply wt_code_cons; eauto with reloadty. + constructor. rewrite <- A. auto with reloadty. + auto with reloadty. assert (locs_valid (transf_function f) (loc_arguments sig)). red; intros. generalize (loc_arguments_acceptable sig l H). destruct l; simpl; auto. destruct s; simpl; intuition. assert (locs_writable (loc_arguments sig)). - red; intros. generalize (loc_arguments_acceptable sig l H7). + red; intros. generalize (loc_arguments_acceptable sig l H6). destruct l; simpl; auto. destruct s; simpl; intuition. assert (map Loc.type args = map Loc.type (loc_arguments sig)). rewrite loc_arguments_type; auto. - destruct ros; auto 10 with reloadty. + destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty. + auto 10 with reloadty. assert (map mreg_type (regs_for args) = map Loc.type args). eauto with reloadty. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 784823b..b779488 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -1043,7 +1043,7 @@ Proof. simpl. congruence. exists (Vint i :: Vptr b0 i0 :: nil). split. eauto with evalexpr. simpl. - rewrite Int.add_commut. congruence. + congruence. exists (Vptr b0 i :: Vint i0 :: nil). split. eauto with evalexpr. simpl. congruence. exists (v :: nil). split. eauto with evalexpr. diff --git a/caml/PrintPPC.ml b/caml/PrintPPC.ml index 030dcc6..f4f2940 100644 --- a/caml/PrintPPC.ml +++ b/caml/PrintPPC.ml @@ -189,8 +189,8 @@ let print_instruction oc labels = function let lbl1 = new_label() in let lbl2 = new_label() in let lbl3 = new_label() in - fprintf oc " addis r2, 0, ha16(L%d)\n" lbl1; - fprintf oc " lfd f13, lo16(L%d)(r2)\n" lbl1; + fprintf oc " addis r12, 0, ha16(L%d)\n" lbl1; + fprintf oc " lfd f13, lo16(L%d)(r12)\n" lbl1; fprintf oc " fcmpu cr7, %a, f13\n" freg r2; fprintf oc " cror 30, 29, 30\n"; fprintf oc " beq cr7, L%d\n" lbl2; @@ -225,12 +225,12 @@ let print_instruction oc labels = function fprintf oc " fsub %a, %a, %a\n" freg r1 freg r2 freg r3 | Pictf(r1, r2) -> let lbl = new_label() in - fprintf oc " addis r2, 0, 0x4330\n"; - fprintf oc " stw r2, -8(r1)\n"; - fprintf oc " addis r2, %a, 0x8000\n" ireg r2; - fprintf oc " stw r2, -4(r1)\n"; - fprintf oc " addis r2, 0, ha16(L%d)\n" lbl; - fprintf oc " lfd f13, lo16(L%d)(r2)\n" lbl; + fprintf oc " addis r12, 0, 0x4330\n"; + fprintf oc " stw r12, -8(r1)\n"; + fprintf oc " addis r12, %a, 0x8000\n" ireg r2; + fprintf oc " stw r12, -4(r1)\n"; + fprintf oc " addis r12, 0, ha16(L%d)\n" lbl; + fprintf oc " lfd f13, lo16(L%d)(r12)\n" lbl; fprintf oc " lfd %a, -8(r1)\n" freg r1; fprintf oc " fsub %a, %a, f13\n" freg r1 freg r1; fprintf oc " .const_data\n"; @@ -238,11 +238,11 @@ let print_instruction oc labels = function fprintf oc " .text\n" | Piuctf(r1, r2) -> let lbl = new_label() in - fprintf oc " addis r2, 0, 0x4330\n"; - fprintf oc " stw r2, -8(r1)\n"; + fprintf oc " addis r12, 0, 0x4330\n"; + fprintf oc " stw r12, -8(r1)\n"; fprintf oc " stw %a, -4(r1)\n" ireg r2; - fprintf oc " addis r2, 0, ha16(L%d)\n" lbl; - fprintf oc " lfd f13, lo16(L%d)(r2)\n" lbl; + fprintf oc " addis r12, 0, ha16(L%d)\n" lbl; + fprintf oc " lfd f13, lo16(L%d)(r12)\n" lbl; fprintf oc " lfd %a, -8(r1)\n" freg r1; fprintf oc " fsub %a, %a, f13\n" freg r1 freg r1; fprintf oc " .const_data\n"; @@ -258,8 +258,8 @@ let print_instruction oc labels = function fprintf oc " lfdx %a, %a, %a\n" freg r1 ireg r2 ireg r3 | Plfi(r1, c) -> let lbl = new_label() in - fprintf oc " addis r2, 0, ha16(L%d)\n" lbl; - fprintf oc " lfd %a, lo16(L%d)(r2)\n" freg r1 lbl; + fprintf oc " addis r12, 0, ha16(L%d)\n" lbl; + fprintf oc " lfd %a, lo16(L%d)(r12)\n" freg r1 lbl; fprintf oc " .const_data\n"; let n = Int64.bits_of_float c in let nlo = Int64.to_int32 n diff --git a/extraction/.depend b/extraction/.depend index ac888a5..4730714 100644 --- a/extraction/.depend +++ b/extraction/.depend @@ -46,10 +46,6 @@ Coqlib.cmi ../caml/Camlcoq.cmo CList.cmi BinPos.cmi ../caml/Linearizeaux.cmx: Maps.cmx Lattice.cmx LTL.cmx Datatypes.cmx \ Coqlib.cmx ../caml/Camlcoq.cmx CList.cmx BinPos.cmx -../caml/PrintCshm.cmo: Integers.cmi Datatypes.cmi Csharpminor.cmi \ - ../caml/Camlcoq.cmo CList.cmi AST.cmi -../caml/PrintCshm.cmx: Integers.cmx Datatypes.cmx Csharpminor.cmx \ - ../caml/Camlcoq.cmx CList.cmx AST.cmx ../caml/PrintCsyntax.cmo: Datatypes.cmi Csyntax.cmi ../caml/Camlcoq.cmo \ CList.cmi AST.cmi ../caml/PrintCsyntax.cmx: Datatypes.cmx Csyntax.cmx ../caml/Camlcoq.cmx \ |