From c90abe06d110eb9c39b941792d896c741dc851dd Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 27 Feb 2009 15:13:38 +0000
Subject: [PATCH] Optimize redundant casts after memory loads
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1002 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
powerpc/Selection.v | 30 ++++++++++++++++++++++++++++++
powerpc/Selectionproof.v | 28 ++++++++++++++++++++++++++++
2 files changed, 58 insertions(+)
diff --git a/powerpc/Selection.v b/powerpc/Selection.v
index f1c5a73b1..46d803907 100644
--- a/powerpc/Selection.v
+++ b/powerpc/Selection.v
@@ -802,6 +802,9 @@ Inductive cast8signed_cases: forall (e1: expr), Set :=
| cast8signed_case1:
forall (e2: expr),
cast8signed_cases (Eop Ocast8signed (e2 ::: Enil))
+ | cast8signed_case2:
+ forall mode args,
+ cast8signed_cases (Eload Mint8signed mode args)
| cast8signed_default:
forall (e1: expr),
cast8signed_cases e1.
@@ -810,6 +813,8 @@ Definition cast8signed_match (e1: expr) :=
match e1 as z1 return cast8signed_cases z1 with
| Eop Ocast8signed (e2 ::: Enil) =>
cast8signed_case1 e2
+ | Eload Mint8signed mode args =>
+ cast8signed_case2 mode args
| e1 =>
cast8signed_default e1
end.
@@ -817,6 +822,7 @@ Definition cast8signed_match (e1: expr) :=
Definition cast8signed (e: expr) :=
match cast8signed_match e with
| cast8signed_case1 e1 => e
+ | cast8signed_case2 mode args => e
| cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil)
end.
@@ -824,6 +830,9 @@ Inductive cast8unsigned_cases: forall (e1: expr), Set :=
| cast8unsigned_case1:
forall (e2: expr),
cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil))
+ | cast8unsigned_case2:
+ forall mode args,
+ cast8unsigned_cases (Eload Mint8unsigned mode args)
| cast8unsigned_default:
forall (e1: expr),
cast8unsigned_cases e1.
@@ -832,6 +841,8 @@ Definition cast8unsigned_match (e1: expr) :=
match e1 as z1 return cast8unsigned_cases z1 with
| Eop Ocast8unsigned (e2 ::: Enil) =>
cast8unsigned_case1 e2
+ | Eload Mint8unsigned mode args =>
+ cast8unsigned_case2 mode args
| e1 =>
cast8unsigned_default e1
end.
@@ -839,6 +850,7 @@ Definition cast8unsigned_match (e1: expr) :=
Definition cast8unsigned (e: expr) :=
match cast8unsigned_match e with
| cast8unsigned_case1 e1 => e
+ | cast8unsigned_case2 mode args => e
| cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil)
end.
@@ -846,6 +858,9 @@ Inductive cast16signed_cases: forall (e1: expr), Set :=
| cast16signed_case1:
forall (e2: expr),
cast16signed_cases (Eop Ocast16signed (e2 ::: Enil))
+ | cast16signed_case2:
+ forall mode args,
+ cast16signed_cases (Eload Mint16signed mode args)
| cast16signed_default:
forall (e1: expr),
cast16signed_cases e1.
@@ -854,6 +869,8 @@ Definition cast16signed_match (e1: expr) :=
match e1 as z1 return cast16signed_cases z1 with
| Eop Ocast16signed (e2 ::: Enil) =>
cast16signed_case1 e2
+ | Eload Mint16signed mode args =>
+ cast16signed_case2 mode args
| e1 =>
cast16signed_default e1
end.
@@ -861,6 +878,7 @@ Definition cast16signed_match (e1: expr) :=
Definition cast16signed (e: expr) :=
match cast16signed_match e with
| cast16signed_case1 e1 => e
+ | cast16signed_case2 mode args => e
| cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil)
end.
@@ -868,6 +886,9 @@ Inductive cast16unsigned_cases: forall (e1: expr), Set :=
| cast16unsigned_case1:
forall (e2: expr),
cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil))
+ | cast16unsigned_case2:
+ forall mode args,
+ cast16unsigned_cases (Eload Mint16unsigned mode args)
| cast16unsigned_default:
forall (e1: expr),
cast16unsigned_cases e1.
@@ -876,6 +897,8 @@ Definition cast16unsigned_match (e1: expr) :=
match e1 as z1 return cast16unsigned_cases z1 with
| Eop Ocast16unsigned (e2 ::: Enil) =>
cast16unsigned_case1 e2
+ | Eload Mint16unsigned mode args =>
+ cast16unsigned_case2 mode args
| e1 =>
cast16unsigned_default e1
end.
@@ -883,6 +906,7 @@ Definition cast16unsigned_match (e1: expr) :=
Definition cast16unsigned (e: expr) :=
match cast16unsigned_match e with
| cast16unsigned_case1 e1 => e
+ | cast16unsigned_case2 mode args => e
| cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil)
end.
@@ -890,6 +914,9 @@ Inductive singleoffloat_cases: forall (e1: expr), Set :=
| singleoffloat_case1:
forall (e2: expr),
singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil))
+ | singleoffloat_case2:
+ forall mode args,
+ singleoffloat_cases (Eload Mfloat32 mode args)
| singleoffloat_default:
forall (e1: expr),
singleoffloat_cases e1.
@@ -898,6 +925,8 @@ Definition singleoffloat_match (e1: expr) :=
match e1 as z1 return singleoffloat_cases z1 with
| Eop Osingleoffloat (e2 ::: Enil) =>
singleoffloat_case1 e2
+ | Eload Mfloat32 mode args =>
+ singleoffloat_case2 mode args
| e1 =>
singleoffloat_default e1
end.
@@ -905,6 +934,7 @@ Definition singleoffloat_match (e1: expr) :=
Definition singleoffloat (e: expr) :=
match singleoffloat_match e with
| singleoffloat_case1 e1 => e
+ | singleoffloat_case2 mode args => e
| singleoffloat_default e1 => Eop Osingleoffloat (e1 ::: Enil)
end.
diff --git a/powerpc/Selectionproof.v b/powerpc/Selectionproof.v
index b6e838cdc..6ffffc18a 100644
--- a/powerpc/Selectionproof.v
+++ b/powerpc/Selectionproof.v
@@ -745,6 +745,29 @@ Proof.
intros. EvalOp.
Qed.
+Lemma loadv_cast:
+ forall chunk addr v,
+ loadv chunk m addr = Some v ->
+ match chunk with
+ | Mint8signed => loadv chunk m addr = Some(Val.sign_ext 8 v)
+ | Mint8unsigned => loadv chunk m addr = Some(Val.zero_ext 8 v)
+ | Mint16signed => loadv chunk m addr = Some(Val.sign_ext 16 v)
+ | Mint16unsigned => loadv chunk m addr = Some(Val.zero_ext 16 v)
+ | Mfloat32 => loadv chunk m addr = Some(Val.singleoffloat v)
+ | _ => True
+ end.
+Proof.
+ intros. rewrite H. destruct addr; simpl in H; try discriminate.
+ exploit Mem.load_inv; eauto.
+ set (v' := (getN (pred_size_chunk chunk) (Int.signed i) (contents (blocks m b)))).
+ intros [A B]. subst v. destruct chunk; auto; destruct v'; simpl; auto.
+ rewrite Int.sign_ext_idem; auto. compute; auto.
+ rewrite Int.zero_ext_idem; auto. compute; auto.
+ rewrite Int.sign_ext_idem; auto. compute; auto.
+ rewrite Int.zero_ext_idem; auto. compute; auto.
+ rewrite Float.singleoffloat_idem; auto.
+Qed.
+
Theorem eval_cast8signed:
forall le a v,
eval_expr ge sp e m le a v ->
@@ -753,6 +776,7 @@ Proof.
intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval.
EvalOp. simpl. subst v. destruct v1; simpl; auto.
rewrite Int.sign_ext_idem. reflexivity. compute; auto.
+ inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7).
EvalOp.
Qed.
@@ -764,6 +788,7 @@ Proof.
intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval.
EvalOp. simpl. subst v. destruct v1; simpl; auto.
rewrite Int.zero_ext_idem. reflexivity. compute; auto.
+ inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7).
EvalOp.
Qed.
@@ -775,6 +800,7 @@ Proof.
intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval.
EvalOp. simpl. subst v. destruct v1; simpl; auto.
rewrite Int.sign_ext_idem. reflexivity. compute; auto.
+ inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7).
EvalOp.
Qed.
@@ -786,6 +812,7 @@ Proof.
intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval.
EvalOp. simpl. subst v. destruct v1; simpl; auto.
rewrite Int.zero_ext_idem. reflexivity. compute; auto.
+ inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7).
EvalOp.
Qed.
@@ -796,6 +823,7 @@ Theorem eval_singleoffloat:
Proof.
intros until v; unfold singleoffloat; case (singleoffloat_match a); intros; InvEval.
EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity.
+ inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7).
EvalOp.
Qed.
--
GitLab