diff options
Diffstat (limited to 'powerpc/Asmgenproof1.v')
-rw-r--r-- | powerpc/Asmgenproof1.v | 98 |
1 files changed, 65 insertions, 33 deletions
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 38525c98..226c175f 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -188,18 +188,30 @@ Lemma preg_of_not_GPR1: Proof. intro. case r; discriminate. Qed. -Hint Resolve preg_of_not_GPR1: ppcgen. +Lemma preg_of_not_GPR13: + forall r, preg_of r <> GPR13. +Proof. + intro. case r; discriminate. +Qed. + +Hint Resolve preg_of_not_GPR1 preg_of_not_GPR13: ppcgen. (** Agreement between Mach register sets and PPC register sets. *) +Section AGREEMENT. + +Variable ge: genv. + Definition agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) := - rs#GPR1 = sp /\ forall r: mreg, ms r = rs#(preg_of r). + rs#GPR1 = sp /\ + rs#GPR13 = small_data_area_base ge /\ + forall r: mreg, ms r = rs#(preg_of r). Lemma preg_val: forall ms sp rs r, agree ms sp rs -> ms r = rs#(preg_of r). Proof. - intros. elim H. auto. + intros. destruct H as [A [B C]]. auto. Qed. Lemma ireg_val: @@ -208,8 +220,8 @@ Lemma ireg_val: mreg_type r = Tint -> ms r = rs#(ireg_of r). Proof. - intros. elim H; intros. - generalize (H2 r). unfold preg_of. rewrite H0. auto. + intros. rewrite (preg_val ms sp rs); auto. + unfold preg_of. rewrite H0. auto. Qed. Lemma freg_val: @@ -218,8 +230,8 @@ Lemma freg_val: mreg_type r = Tfloat -> ms r = rs#(freg_of r). Proof. - intros. elim H; intros. - generalize (H2 r). unfold preg_of. rewrite H0. auto. + intros. rewrite (preg_val ms sp rs); auto. + unfold preg_of. rewrite H0. auto. Qed. Lemma sp_val: @@ -227,7 +239,15 @@ Lemma sp_val: agree ms sp rs -> sp = rs#GPR1. Proof. - intros. elim H; auto. + intros. destruct H as [A [B C]]. auto. +Qed. + +Lemma gpr13_val: + forall ms sp rs, + agree ms sp rs -> + small_data_area_base ge = rs#GPR13. +Proof. + intros. destruct H as [A [B C]]. auto. Qed. Lemma agree_exten_1: @@ -236,8 +256,9 @@ Lemma agree_exten_1: (forall r, is_data_reg r -> rs'#r = rs#r) -> agree ms sp rs'. Proof. - unfold agree; intros. elim H; intros. - split. rewrite H0. auto. exact I. + unfold agree; intros. destruct H as [A [B C]]. + split. rewrite H0. auto. exact I. + split. rewrite H0. auto. exact I. intros. rewrite H0. auto. apply preg_of_is_data_reg. Qed. @@ -263,8 +284,9 @@ Lemma agree_set_mreg: agree ms sp rs -> agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v). Proof. - unfold agree; intros. elim H; intros; clear H. + unfold agree; intros. destruct H as [A [B C]]. split. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_GPR1. + split. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_GPR13. intros. unfold Regmap.set. case (RegEq.eq r0 r); intro. subst r0. rewrite Pregmap.gss. auto. rewrite Pregmap.gso. auto. red; intro. @@ -317,15 +339,9 @@ Lemma agree_set_mireg_twice: mreg_type r = Tint -> agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v' #(ireg_of r) <- v). Proof. - intros. replace (IR (ireg_of r)) with (preg_of r). elim H; intros. - split. repeat (rewrite Pregmap.gso; auto with ppcgen). - intros. case (mreg_eq r r0); intro. - subst r0. rewrite Regmap.gss. rewrite Pregmap.gss. auto. - assert (preg_of r <> preg_of r0). - red; intro. elim n. apply preg_of_injective. auto. - rewrite Regmap.gso; auto. - repeat (rewrite Pregmap.gso; auto). - unfold preg_of. rewrite H0. auto. + intros. apply agree_exten_1 with (rs#(ireg_of r) <- v). + apply agree_set_mireg. apply agree_set_mreg. auto. auto. + intros. unfold Pregmap.set. destruct (PregEq.eq r0 (ireg_of r)); auto. Qed. Hint Resolve agree_set_mireg_twice: ppcgen. @@ -335,10 +351,12 @@ Lemma agree_set_twice_mireg: mreg_type r = Tint -> agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v). Proof. - intros. elim H; intros. - split. rewrite Pregmap.gso. auto. - generalize (ireg_of_not_GPR1 r); congruence. - intros. generalize (H2 r0). + intros. destruct H as [A [B C]]. + split. rewrite Pregmap.gso; auto. + generalize (preg_of_not_GPR1 r). unfold preg_of. rewrite H0. congruence. + split. rewrite Pregmap.gso; auto. + generalize (preg_of_not_GPR13 r). unfold preg_of. rewrite H0. congruence. + intros. generalize (C r0). case (mreg_eq r0 r); intro. subst r0. repeat rewrite Regmap.gss. unfold preg_of; rewrite H0. rewrite Pregmap.gss. auto. @@ -466,11 +484,6 @@ Qed. (** * Execution of straight-line code *) -Section STRAIGHTLINE. - -Variable ge: genv. -Variable fn: code. - (** Straight-line code is composed of PPC instructions that execute in sequence (no branches, no function calls and returns). The following inductive predicate relates the machine states @@ -478,6 +491,8 @@ Variable fn: code. Instructions are taken from the first list instead of being fetched from memory. *) +Variable fn: code. + Inductive exec_straight: code -> regset -> mem -> code -> regset -> mem -> Prop := | exec_straight_one: @@ -1474,6 +1489,11 @@ Proof. apply H0. simpl. repeat (rewrite (ireg_val ms sp rs); auto). auto. (* Aglobal *) + case_eq (symbol_is_small_data i i0); intro SISD. + eapply H; eauto. + simpl. rewrite <- (gpr13_val _ _ _ H1). + rewrite small_data_area_addressing; auto. + discriminate. 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#GPR12 (const_low ge (Csymbol_low i i0))). @@ -1619,7 +1639,7 @@ Proof. unfold store1. rewrite gpr_or_zero_not_zero; auto. repeat rewrite B. rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4. - rewrite H5 in H4. elim H6; intros. rewrite H9 in H4. + rewrite H5 in H4. rewrite (preg_val _ _ _ src H6) in H4. rewrite H4. auto. apply preg_of_not. simpl. tauto. discriminate. @@ -1631,7 +1651,7 @@ Proof. split. apply exec_straight_one. rewrite A. unfold store2. repeat rewrite B. rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4. - rewrite H5 in H4. elim H6; intros. rewrite H8 in H4. + rewrite H5 in H4. rewrite (preg_val _ _ _ src H6) in H4. rewrite H4. auto. apply preg_of_not. simpl. tauto. discriminate. discriminate. @@ -1641,6 +1661,18 @@ Proof. auto. auto. Qed. +End AGREEMENT. -End STRAIGHTLINE. - +(* Re-export hints. *) +Hint Resolve agree_set_mreg: ppcgen. +Hint Resolve agree_set_mireg: ppcgen. +Hint Resolve agree_set_mfreg: ppcgen. +Hint Resolve agree_set_other: ppcgen. +Hint Resolve agree_nextinstr: ppcgen. +Hint Resolve agree_set_mireg_twice: ppcgen. +Hint Resolve agree_set_twice_mireg: ppcgen. +Hint Resolve agree_set_commut: ppcgen. +Hint Resolve agree_nextinstr_commut: ppcgen. +Hint Resolve nextinstr_inv: ppcgen. +Hint Resolve nextinstr_set_preg: ppcgen. +Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: ppcgen. |