From 258a1feeafb9ebcec4d46601fe7016bed04a8ea7 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 30 Oct 2009 09:15:06 +0000
Subject: [PATCH] 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
---
powerpc/Asm.v | 4 ++--
powerpc/Asmgenproof.v | 4 +++-
powerpc/Asmgenproof1.v | 37 ++++++++++++++++++++++++++-----------
powerpc/PrintAsm.ml | 6 ++++--
4 files changed, 35 insertions(+), 16 deletions(-)
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 9c03558b1..ab70072b9 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 0c1edec2f..b4176f220 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 5eda7adf3..38525c980 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 e86b7dc4b..335a6cf29 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) ->
--
GitLab