Storing of single floats: must insert frsp instruction before store. (Temporary fix.)

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

4 files changed, 35 insertions, 16 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 9c03558b..ab70072b 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -718,9 +718,9 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
   | Pstfdx rd r1 r2 =>
       store2 Mfloat64 rd r1 r2 rs m
   | Pstfs rd cst r1 =>
-      store1 Mfloat32 rd cst r1 rs m
+      store1 Mfloat32 rd cst r1 (rs#FPR13 <- Vundef) m
   | Pstfsx rd r1 r2 =>
-      store2 Mfloat32 rd r1 r2 rs m
+      store2 Mfloat32 rd r1 r2 (rs#FPR13 <- Vundef) m
   | Psth rd cst r1 =>
       store1 Mint16unsigned rd cst r1 rs m
   | Psthx rd r1 r2 =>
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 0c1edec2..b4176f22 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -842,7 +842,9 @@ Proof.
   try (rewrite storev_8_signed_unsigned in H0);
   try (rewrite storev_16_signed_unsigned in H0);
   simpl; eapply transl_store_correct; eauto;
-  intros; unfold preg_of; rewrite H6; reflexivity.
+  intros; (econstructor; split; [unfold preg_of; rewrite H6; reflexivity | auto]).
+  intros. apply Pregmap.gso; auto. 
+  intros. apply Pregmap.gso; auto.
 Qed.
 
 Lemma exec_Mcall_prop:
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 5eda7adf..38525c98 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1594,11 +1594,15 @@ Lemma transl_store_correct:
   forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
     chunk addr args k ms sp rs m src a m',
   (forall cst (r1: ireg) (rs1: regset),
+    exists rs2,
     exec_instr ge fn (mk1 cst r1) rs1 m =
-    store1 ge chunk (preg_of src) cst r1 rs1 m) ->
+    store1 ge chunk (preg_of src) cst r1 rs2 m
+    /\ (forall (r: preg), r <> FPR13 -> rs2 r = rs1 r)) ->
   (forall (r1 r2: ireg) (rs1: regset),
+    exists rs2,
     exec_instr ge fn (mk2 r1 r2) rs1 m =
-    store2 chunk (preg_of src) r1 r2 rs1 m) ->
+    store2 chunk (preg_of src) r1 r2 rs2 m
+    /\ (forall (r: preg), r <> FPR13 -> rs2 r = rs1 r)) ->
   agree ms sp rs ->
   map mreg_type args = type_of_addressing addr ->
   eval_addressing ge sp addr (map ms args) = Some a ->
@@ -1608,21 +1612,32 @@ Lemma transl_store_correct:
                         k rs' m'
   /\ agree ms sp rs'.
 Proof.
-  intros.   apply transl_load_store_correct with ms.
-  intros. exists (nextinstr rs1). 
-  split. apply exec_straight_one. rewrite H. 
-  unfold store1. rewrite gpr_or_zero_not_zero; auto. 
+  intros. apply transl_load_store_correct with ms.
+  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. 
   rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4.
   rewrite H5 in H4. elim H6; intros. rewrite H9 in H4.
   rewrite H4. auto.
-  auto with ppcgen. auto with ppcgen. 
-  intros. exists (nextinstr rs1).
-  split. apply exec_straight_one. rewrite H0. 
-  unfold store2. 
+  apply preg_of_not. simpl. tauto.
+  discriminate.
+  rewrite <- B. auto. discriminate.
+  apply agree_nextinstr. eapply agree_exten_2; eauto.
+
+  intros. destruct (H0 r1 r2 rs1) as [rs2 [A B]].
+  exists (nextinstr rs2). 
+  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 H4. auto.
-  auto with ppcgen. auto with ppcgen. 
+  apply preg_of_not. simpl. tauto.
+  discriminate. discriminate.
+  rewrite <- B. auto. discriminate.
+  apply agree_nextinstr. eapply agree_exten_2; eauto.
+
   auto. auto.
 Qed.
 
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index e86b7dc4..335a6cf2 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -434,9 +434,11 @@ let print_instruction oc labels = function
   | Pstfdx(r1, r2, r3) ->
       fprintf oc "	stfdx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
   | Pstfs(r1, c, r2) ->
-      fprintf oc "	stfs	%a, %a(%a)\n" freg r1 constant c ireg r2
+      fprintf oc "	frsp	%a, %a\n" freg FPR13 freg r1;
+      fprintf oc "	stfs	%a, %a(%a)\n" freg FPR13 constant c ireg r2
   | Pstfsx(r1, r2, r3) ->
-      fprintf oc "	stfsx	%a, %a, %a\n" freg r1 ireg r2 ireg r3
+      fprintf oc "	frsp	%a, %a\n" freg FPR13 freg r1;
+      fprintf oc "	stfsx	%a, %a, %a\n" freg FPR13 ireg r2 ireg r3
   | Psth(r1, c, r2) ->
       fprintf oc "	sth	%a, %a(%a)\n" ireg r1 constant c ireg r2
   | Psthx(r1, r2, r3) ->