From 28e4632d36d175ac9da0befa1a727a58604031e1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 2 Mar 2010 16:18:04 +0000 Subject: 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 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, -- cgit