Simplified the treatment of the PowerPC small data area; now more specific to the Diab toolchain.

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

1 files changed, 72 insertions, 98 deletions

diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 226c175..3baeb79 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -188,30 +188,18 @@ Lemma preg_of_not_GPR1:
 Proof.
   intro. case r; discriminate.
 Qed.
-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.
+Hint Resolve preg_of_not_GPR1: 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 /\
-  rs#GPR13 = small_data_area_base ge /\ 
-  forall r: mreg, ms r = rs#(preg_of r).
+  rs#GPR1 = sp /\ 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. destruct H as [A [B C]]. auto.
+  intros. elim H. auto.
 Qed.
   
 Lemma ireg_val:
@@ -220,8 +208,8 @@ Lemma ireg_val:
   mreg_type r = Tint ->
   ms r = rs#(ireg_of r).
 Proof.
-  intros. rewrite (preg_val ms sp rs); auto. 
-  unfold preg_of. rewrite H0. auto.
+  intros. elim H; intros.
+  generalize (H2 r). unfold preg_of. rewrite H0. auto.
 Qed.
 
 Lemma freg_val:
@@ -230,8 +218,8 @@ Lemma freg_val:
   mreg_type r = Tfloat ->
   ms r = rs#(freg_of r).
 Proof.
-  intros. rewrite (preg_val ms sp rs); auto. 
-  unfold preg_of. rewrite H0. auto.
+  intros. elim H; intros.
+  generalize (H2 r). unfold preg_of. rewrite H0. auto.
 Qed.
 
 Lemma sp_val:
@@ -239,15 +227,7 @@ Lemma sp_val:
   agree ms sp rs ->
   sp = rs#GPR1.
 Proof.
-  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.
+  intros. elim H; auto.
 Qed.
 
 Lemma agree_exten_1:
@@ -256,9 +236,8 @@ Lemma agree_exten_1:
   (forall r, is_data_reg r -> rs'#r = rs#r) ->
   agree ms sp rs'.
 Proof.
-  unfold agree; intros. destruct H as [A [B C]]. 
-  split. rewrite H0. auto. exact I.
-  split. rewrite H0. auto. exact I.
+  unfold agree; intros. elim H; intros.
+  split. rewrite H0. auto. exact I. 
   intros. rewrite H0. auto. apply preg_of_is_data_reg.
 Qed.
 
@@ -284,9 +263,8 @@ Lemma agree_set_mreg:
   agree ms sp rs ->
   agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v).
 Proof.
-  unfold agree; intros. destruct H as [A [B C]]. 
+  unfold agree; intros. elim H; intros; clear H.
   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. 
@@ -339,9 +317,15 @@ 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. 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.
+  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.
 Qed.
 Hint Resolve agree_set_mireg_twice: ppcgen.
 
@@ -351,12 +335,10 @@ Lemma agree_set_twice_mireg:
   mreg_type r = Tint ->
   agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v).
 Proof.
-  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). 
+  intros. elim H; intros.
+  split. rewrite Pregmap.gso. auto. 
+  generalize (ireg_of_not_GPR1 r); congruence.
+  intros. generalize (H2 r0). 
   case (mreg_eq r0 r); intro.
   subst r0. repeat rewrite Regmap.gss. unfold preg_of; rewrite H0.
   rewrite Pregmap.gss. auto.
@@ -484,6 +466,11 @@ 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
@@ -491,8 +478,6 @@ Qed.
   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:
@@ -1422,9 +1407,9 @@ Lemma transl_load_store_correct:
   forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
     addr args k ms sp rs m ms' m',
   (forall cst (r1: ireg) (rs1: regset) k,
-    eval_addressing_total ge sp addr (map ms args) = Val.add rs1#r1 (const_low ge cst) ->
+    eval_addressing_total ge sp addr (map ms args) =
+                Val.add (gpr_or_zero rs1 r1) (const_low ge cst) ->
     agree ms sp rs1 ->
-    r1 <> GPR0 ->
     exists rs',
     exec_straight (mk1 cst r1 :: k) rs1 m k rs' m' /\
     agree ms' sp rs') ->
@@ -1448,14 +1433,13 @@ Proof.
   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#GPR12 (const_low ge (Cint (low_s i)))).
-    simpl. unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss.
+                Val.add (gpr_or_zero rs2 GPR12) (const_low ge (Cint (low_s i)))).
+    simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+    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: GPR12 <> GPR0). discriminate.
-  generalize (H _ _ _ k ADDR AG NOT0).
-  intros [rs' [EX' AG']].
+  destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
   exists rs'. split.
   apply exec_straight_trans with (mk1 (Cint (low_s i)) GPR12 :: k) rs2 m.
   apply exec_straight_two with rs1 m.
@@ -1467,20 +1451,21 @@ Proof.
   (* Aindexed short *)
   case (Int.eq (high_s i) Int.zero).
   assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) =
-                Val.add rs#(ireg_of t) (const_low ge (Cint i))).
-    simpl. rewrite (ireg_val ms sp rs); auto.
-  generalize (H _ _ _ k ADDR H1 n). intros [rs' [EX' AG']].
+                Val.add (gpr_or_zero rs (ireg_of t)) (const_low ge (Cint i))).
+    simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+    rewrite (ireg_val ms sp rs); auto.
+  destruct (H _ _ _ k ADDR H1) as [rs' [EX' AG']].
   exists rs'. split. auto. auto.
   (* Aindexed long *)
   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#GPR12 (const_low ge (Cint (low_s i)))).
-    simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
+                Val.add (gpr_or_zero rs1 GPR12) (const_low ge (Cint (low_s i)))).
+    simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+    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: GPR12 <> GPR0). discriminate.
-  generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']].
+  destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
   simpl. rewrite gpr_or_zero_not_zero; auto. 
   rewrite <- (ireg_val ms sp rs); auto. reflexivity.
@@ -1490,21 +1475,24 @@ Proof.
   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.
+  (* Aglobal from small data *)
+  apply H. rewrite gpr_or_zero_zero. simpl const_low. 
+  rewrite small_data_area_addressing; auto. simpl. 
+  unfold find_symbol_offset, symbol_offset. 
+  destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero. auto.
+  auto.
+  (* Aglobal general case *)
   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))).
-    simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
+                Val.add (gpr_or_zero rs1 GPR12) (const_low ge (Csymbol_low i i0))).
+    simpl. rewrite gpr_or_zero_not_zero; auto. 
+    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.
+    discriminate. discriminate.
   assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen.
-  assert (NOT0: GPR12 <> GPR0). discriminate.
-  generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']].
+  destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
   unfold exec_instr. rewrite gpr_or_zero_zero. 
   rewrite Val.add_commut. unfold const_high. 
@@ -1525,8 +1513,9 @@ Proof.
   intros. 
   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#GPR12 (const_low ge (Csymbol_low i i0))).
-    simpl. unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss.
+                Val.add (gpr_or_zero rs2 GPR12) (const_low ge (Csymbol_low i i0))).
+    simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+    unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss.
     unfold const_high. 
     set (v := symbol_offset ge i i0).
     rewrite Val.add_assoc. 
@@ -1534,8 +1523,7 @@ 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: GPR12 <> GPR0). discriminate.
-  generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']].
+  destruct (H _ _ _ k ADDR AG) as [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. 
@@ -1555,17 +1543,17 @@ Proof.
   apply COMMON; auto. eapply ireg_val; eauto.
   (* Ainstack *)
   case (Int.eq (high_s i) Int.zero).
-  apply H. simpl. rewrite (sp_val ms sp rs); auto. auto.
-  discriminate.
+  apply H. simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. 
+  rewrite (sp_val ms sp rs); auto. auto.
   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#GPR12 (const_low ge (Cint (low_s i)))).
-    simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss.
+                Val.add (gpr_or_zero rs1 GPR12) (const_low ge (Cint (low_s i)))).
+    simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen.
+    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: GPR12 <> GPR0). discriminate.
-  generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']].
+  destruct (H _ _ _ k ADDR AG) as [rs' [EX' AG']].
   exists rs'. split. apply exec_straight_step with rs1 m.
   simpl. rewrite gpr_or_zero_not_zero. 
   unfold rs1. rewrite (sp_val ms sp rs). reflexivity.
@@ -1595,8 +1583,7 @@ Proof.
   intros. apply transl_load_store_correct with ms.
   intros. exists (nextinstr (rs1#(preg_of dst) <- v)). 
   split. apply exec_straight_one. rewrite H. 
-  unfold load1. rewrite gpr_or_zero_not_zero; auto. 
-  rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
+  unfold load1. rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
   rewrite H5 in H4. rewrite H4. auto.
   auto with ppcgen. auto with ppcgen. 
   intros. exists (nextinstr (rs1#(preg_of dst) <- v)). 
@@ -1636,13 +1623,12 @@ Proof.
   intros. destruct (H cst r1 rs1) as [rs2 [A B]].
   exists (nextinstr rs2). 
   split. apply exec_straight_one. rewrite A. 
-  unfold store1. rewrite gpr_or_zero_not_zero; auto.
-  repeat rewrite B. 
+  unfold store1. rewrite B. replace (gpr_or_zero rs2 r1) with (gpr_or_zero rs1 r1).
   rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
-  rewrite H5 in H4. rewrite (preg_val _ _ _ src H6) in H4. 
+  rewrite H5 in H4. elim H6; intros. rewrite H8 in H4.
   rewrite H4. auto.
+  unfold gpr_or_zero. destruct (ireg_eq r1 GPR0); auto. symmetry. apply B. discriminate.
   apply preg_of_not. simpl. tauto.
-  discriminate.
   rewrite <- B. auto. discriminate.
   apply agree_nextinstr. eapply agree_exten_2; eauto.
 
@@ -1651,7 +1637,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. rewrite (preg_val _ _ _ src H6) in H4. 
+  rewrite H5 in H4. elim H6; intros. rewrite H8 in H4.
   rewrite H4. auto.
   apply preg_of_not. simpl. tauto.
   discriminate. discriminate.
@@ -1661,18 +1647,6 @@ Proof.
   auto. auto.
 Qed.
 
-End AGREEMENT.
 
-(* 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.
+End STRAIGHTLINE.
+