Wrong rlwinm generated for 'x mod 1'

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

2 files changed, 110 insertions, 111 deletions

diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v
index 40201e77..2f4d76e5 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 ae152b38..2736e9e9 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,