From 28e4632d36d175ac9da0befa1a727a58604031e1 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Tue, 2 Mar 2010 16:18:04 +0000
Subject: [PATCH] Wrong rlwinm generated for 'x mod 1'
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1265 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
powerpc/SelectOp.v | 106 ++++++++++++++++++------------------
powerpc/SelectOpproof.v | 115 ++++++++++++++++++++--------------------
2 files changed, 110 insertions(+), 111 deletions(-)
diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v
index 40201e77d..2f4d76e50 100644
--- a/powerpc/SelectOp.v
+++ b/powerpc/SelectOp.v
@@ -529,59 +529,6 @@ Definition mul (e1: expr) (e2: expr) :=
Eop Omul (e1:::e2:::Enil)
end.
-(** ** Integer division and modulus *)
-
-Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
-
-Definition mod_aux (divop: operation) (e1 e2: expr) :=
- Elet e1
- (Elet (lift e2)
- (Eop Osub (Eletvar 1 :::
- Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) :::
- Eletvar 0 :::
- Enil) :::
- Enil))).
-
-Definition mods := mod_aux Odiv.
-
-Inductive divu_cases: forall (e2: expr), Type :=
- | divu_case1:
- forall (n2: int),
- divu_cases (Eop (Ointconst n2) Enil)
- | divu_default:
- forall (e2: expr),
- divu_cases e2.
-
-Definition divu_match (e2: expr) :=
- match e2 as z1 return divu_cases z1 with
- | Eop (Ointconst n2) Enil =>
- divu_case1 n2
- | e2 =>
- divu_default e2
- end.
-
-Definition divu (e1: expr) (e2: expr) :=
- match divu_match e2 with
- | divu_case1 n2 =>
- match Int.is_power2 n2 with
- | Some l2 => shruimm e1 l2
- | None => Eop Odivu (e1:::e2:::Enil)
- end
- | divu_default e2 =>
- Eop Odivu (e1:::e2:::Enil)
- end.
-
-Definition modu (e1: expr) (e2: expr) :=
- match divu_match e2 with
- | divu_case1 n2 =>
- match Int.is_power2 n2 with
- | Some l2 => rolm e1 Int.zero (Int.sub n2 Int.one)
- | None => mod_aux Odivu e1 e2
- end
- | divu_default e2 =>
- mod_aux Odivu e1 e2
- end.
-
(** ** Bitwise and, or, xor *)
Definition andimm (n1: int) (e2: expr) :=
@@ -636,6 +583,59 @@ Definition or (e1: expr) (e2: expr) :=
Eop Oor (e1:::e2:::Enil)
end.
+(** ** Integer division and modulus *)
+
+Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+
+Definition mod_aux (divop: operation) (e1 e2: expr) :=
+ Elet e1
+ (Elet (lift e2)
+ (Eop Osub (Eletvar 1 :::
+ Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) :::
+ Eletvar 0 :::
+ Enil) :::
+ Enil))).
+
+Definition mods := mod_aux Odiv.
+
+Inductive divu_cases: forall (e2: expr), Type :=
+ | divu_case1:
+ forall (n2: int),
+ divu_cases (Eop (Ointconst n2) Enil)
+ | divu_default:
+ forall (e2: expr),
+ divu_cases e2.
+
+Definition divu_match (e2: expr) :=
+ match e2 as z1 return divu_cases z1 with
+ | Eop (Ointconst n2) Enil =>
+ divu_case1 n2
+ | e2 =>
+ divu_default e2
+ end.
+
+Definition divu (e1: expr) (e2: expr) :=
+ match divu_match e2 with
+ | divu_case1 n2 =>
+ match Int.is_power2 n2 with
+ | Some l2 => shruimm e1 l2
+ | None => Eop Odivu (e1:::e2:::Enil)
+ end
+ | divu_default e2 =>
+ Eop Odivu (e1:::e2:::Enil)
+ end.
+
+Definition modu (e1: expr) (e2: expr) :=
+ match divu_match e2 with
+ | divu_case1 n2 =>
+ match Int.is_power2 n2 with
+ | Some l2 => andimm (Int.sub n2 Int.one) e1
+ | None => mod_aux Odivu e1 e2
+ end
+ | divu_default e2 =>
+ mod_aux Odivu e1 e2
+ end.
+
(** ** General shifts *)
Inductive shift_cases: forall (e1: expr), Type :=
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index ae152b388..2736e9e92 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -443,6 +443,62 @@ Proof.
EvalOp.
Qed.
+Theorem eval_andimm:
+ forall le n a x,
+ eval_expr ge sp e m le a (Vint x) ->
+ eval_expr ge sp e m le (andimm n a) (Vint (Int.and x n)).
+Proof.
+ intros. unfold andimm. case (Int.is_rlw_mask n).
+ rewrite <- Int.rolm_zero. apply eval_rolm; auto.
+ EvalOp.
+Qed.
+
+Theorem eval_and:
+ forall le a x b y,
+ eval_expr ge sp e m le a (Vint x) ->
+ eval_expr ge sp e m le b (Vint y) ->
+ eval_expr ge sp e m le (and a b) (Vint (Int.and x y)).
+Proof.
+ intros until y; unfold and; case (mul_match a b); intros; InvEval.
+ rewrite Int.and_commut. apply eval_andimm; auto.
+ apply eval_andimm; auto.
+ EvalOp.
+Qed.
+
+Remark eval_same_expr:
+ forall a1 a2 le v1 v2,
+ same_expr_pure a1 a2 = true ->
+ eval_expr ge sp e m le a1 v1 ->
+ eval_expr ge sp e m le a2 v2 ->
+ a1 = a2 /\ v1 = v2.
+Proof.
+ intros until v2.
+ destruct a1; simpl; try (intros; discriminate).
+ destruct a2; simpl; try (intros; discriminate).
+ case (ident_eq i i0); intros.
+ subst i0. inversion H0. inversion H1. split. auto. congruence.
+ discriminate.
+Qed.
+
+Lemma eval_or:
+ forall le a x b y,
+ eval_expr ge sp e m le a (Vint x) ->
+ eval_expr ge sp e m le b (Vint y) ->
+ eval_expr ge sp e m le (or a b) (Vint (Int.or x y)).
+Proof.
+ intros until y; unfold or; case (or_match a b); intros; InvEval.
+ caseEq (Int.eq amount1 amount2
+ && Int.is_rlw_mask (Int.or mask1 mask2)
+ && same_expr_pure t1 t2); intro.
+ destruct (andb_prop _ _ H1). destruct (andb_prop _ _ H4).
+ generalize (Int.eq_spec amount1 amount2). rewrite H6. intro. subst amount2.
+ exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2.
+ simpl. EvalOp. simpl. rewrite Int.or_rolm. auto.
+ simpl. apply eval_Eop with (Vint x :: Vint y :: nil).
+ econstructor. EvalOp. simpl. congruence.
+ econstructor. EvalOp. simpl. congruence. constructor. auto.
+ EvalOp.
+Qed.
Theorem eval_divs:
forall le a b x y,
eval_expr ge sp e m le a (Vint x) ->
@@ -535,8 +591,7 @@ Theorem eval_modu:
Proof.
intros until y; unfold modu; case (divu_match b); intros; InvEval.
caseEq (Int.is_power2 y).
- intros. rewrite (Int.modu_and x y i H0).
- rewrite <- Int.rolm_zero. apply eval_rolm. auto.
+ intros. rewrite (Int.modu_and x y i H0). apply eval_andimm. auto.
intro. rewrite Int.modu_divu. eapply eval_mod_aux.
intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero.
contradiction. auto.
@@ -546,62 +601,6 @@ Proof.
contradiction. auto. auto. auto. auto. auto.
Qed.
-Theorem eval_andimm:
- forall le n a x,
- eval_expr ge sp e m le a (Vint x) ->
- eval_expr ge sp e m le (andimm n a) (Vint (Int.and x n)).
-Proof.
- intros. unfold andimm. case (Int.is_rlw_mask n).
- rewrite <- Int.rolm_zero. apply eval_rolm; auto.
- EvalOp.
-Qed.
-
-Theorem eval_and:
- forall le a x b y,
- eval_expr ge sp e m le a (Vint x) ->
- eval_expr ge sp e m le b (Vint y) ->
- eval_expr ge sp e m le (and a b) (Vint (Int.and x y)).
-Proof.
- intros until y; unfold and; case (mul_match a b); intros; InvEval.
- rewrite Int.and_commut. apply eval_andimm; auto.
- apply eval_andimm; auto.
- EvalOp.
-Qed.
-
-Remark eval_same_expr:
- forall a1 a2 le v1 v2,
- same_expr_pure a1 a2 = true ->
- eval_expr ge sp e m le a1 v1 ->
- eval_expr ge sp e m le a2 v2 ->
- a1 = a2 /\ v1 = v2.
-Proof.
- intros until v2.
- destruct a1; simpl; try (intros; discriminate).
- destruct a2; simpl; try (intros; discriminate).
- case (ident_eq i i0); intros.
- subst i0. inversion H0. inversion H1. split. auto. congruence.
- discriminate.
-Qed.
-
-Lemma eval_or:
- forall le a x b y,
- eval_expr ge sp e m le a (Vint x) ->
- eval_expr ge sp e m le b (Vint y) ->
- eval_expr ge sp e m le (or a b) (Vint (Int.or x y)).
-Proof.
- intros until y; unfold or; case (or_match a b); intros; InvEval.
- caseEq (Int.eq amount1 amount2
- && Int.is_rlw_mask (Int.or mask1 mask2)
- && same_expr_pure t1 t2); intro.
- destruct (andb_prop _ _ H1). destruct (andb_prop _ _ H4).
- generalize (Int.eq_spec amount1 amount2). rewrite H6. intro. subst amount2.
- exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2.
- simpl. EvalOp. simpl. rewrite Int.or_rolm. auto.
- simpl. apply eval_Eop with (Vint x :: Vint y :: nil).
- econstructor. EvalOp. simpl. congruence.
- econstructor. EvalOp. simpl. congruence. constructor. auto.
- EvalOp.
-Qed.
Theorem eval_shl:
forall le a x b y,
--
GitLab