Preliminary support for small data area in PowerPC port.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1163 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

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.