From e99d18c442c40a14e6eaea722cbc7ef0ca6dd26a Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 21 Aug 2010 10:21:11 +0000 Subject: Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext as bitwise operations rather than arithmetic ones. CastOptimproof: fixed for ARM port. Other files: adapted to changes in Integers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1472 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgenproof.v | 6 ++-- powerpc/Asmgenproof1.v | 54 ++++++++++++--------------------- powerpc/SelectOp.v | 80 +++++++++++++++++++++++++++++++++++++++++++++++-- powerpc/SelectOpproof.v | 6 ++-- 4 files changed, 102 insertions(+), 44 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index ee2867e6..fc14830c 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -1217,10 +1217,10 @@ Proof. rewrite <- Int.shl_rolm. rewrite Int.shl_mul. rewrite Int.mul_signed. apply Int.signed_repr. - split. apply Zle_trans with 0. vm_compute; congruence. omega. + split. apply Zle_trans with 0. compute; congruence. omega. omega. - vm_compute. reflexivity. - vm_compute. apply Int.mkint_eq. auto. + compute. reflexivity. + apply Int.mkint_eq. compute. reflexivity. inv AT. simpl in H7. set (k1 := Pbtbl GPR12 tbl :: transl_code f c). set (rs1 := nextinstr (rs0 # GPR12 <- (Vint (Int.rolm n (Int.repr 2) (Int.repr (-4)))))). diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 5ebde633..0b146daa 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -79,41 +79,25 @@ Proof. unfold high_s. rewrite <- (Int.divu_pow2 (Int.sub n (low_s n)) (Int.repr 65536) (Int.repr 16)). change (two_p (Int.unsigned (Int.repr 16))) with 65536. - - assert (forall x y, y > 0 -> (x - x mod y) mod y = 0). - intros. apply Zmod_unique with (x / y). - generalize (Z_div_mod_eq x y H). intro. rewrite Zmult_comm. omega. - omega. - - assert (Int.modu (Int.sub n (low_s n)) (Int.repr 65536) = Int.zero). - unfold Int.modu, Int.zero. decEq. - change (Int.unsigned (Int.repr 65536)) with 65536. - unfold Int.sub. - assert (forall a b, Int.eqm a b -> b mod 65536 = 0 -> a mod 65536 = 0). - intros a b [k EQ] H1. rewrite EQ. - change Int.modulus with (65536 * 65536). - rewrite Zmult_assoc. rewrite Zplus_comm. rewrite Z_mod_plus. auto. - omega. - eapply H0. apply Int.eqm_sym. apply Int.eqm_unsigned_repr. - unfold low_s. unfold Int.sign_ext. - change (two_p 16) with 65536. change (two_p (16-1)) with 32768. - set (N := Int.unsigned n). - case (zlt (N mod 65536) 32768); intro. - apply H0 with (N - N mod 65536). auto with ints. - apply H. omega. - apply H0 with (N - (N mod 65536 - 65536)). auto with ints. - replace (N - (N mod 65536 - 65536)) - with ((N - N mod 65536) + 1 * 65536). - rewrite Z_mod_plus. apply H. omega. omega. ring. - - assert (Int.repr 65536 <> Int.zero). compute. congruence. - generalize (Int.modu_divu_Euclid (Int.sub n (low_s n)) (Int.repr 65536) H1). - rewrite H0. rewrite Int.add_zero. intro. rewrite <- H2. - rewrite Int.sub_add_opp. rewrite Int.add_assoc. - replace (Int.add (Int.neg (low_s n)) (low_s n)) with Int.zero. - apply Int.add_zero. symmetry. rewrite Int.add_commut. - rewrite <- Int.sub_add_opp. apply Int.sub_idem. - + set (x := Int.sub n (low_s n)). + assert (x = Int.add (Int.mul (Int.divu x (Int.repr 65536)) (Int.repr 65536)) + (Int.modu x (Int.repr 65536))). + apply Int.modu_divu_Euclid. compute; congruence. + assert (Int.modu x (Int.repr 65536) = Int.zero). + unfold Int.modu, Int.zero. decEq. + change 0 with (0 mod 65536). + change (Int.unsigned (Int.repr 65536)) with 65536. + apply Int.eqmod_mod_eq. omega. + unfold x, low_s. eapply Int.eqmod_trans. + eapply Int.eqm_eqmod_two_p with (n := 16). compute; auto. + unfold Int.sub. apply Int.eqm_unsigned_repr_l. apply Int.eqm_refl. + replace 0 with (Int.unsigned n - Int.unsigned n) by omega. + apply Int.eqmod_sub. apply Int.eqmod_refl. apply Int.eqmod_sign_ext'. + compute; auto. + rewrite H0 in H. rewrite Int.add_zero in H. + rewrite <- H. unfold x. rewrite Int.sub_add_opp. rewrite Int.add_assoc. + rewrite (Int.add_commut (Int.neg (low_s n))). rewrite <- Int.sub_add_opp. + rewrite Int.sub_idem. apply Int.add_zero. reflexivity. Qed. diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v index fe30b96a..e6a281b2 100644 --- a/powerpc/SelectOp.v +++ b/powerpc/SelectOp.v @@ -371,6 +371,80 @@ Definition sub (e1: expr) (e2: expr) := (** ** Rotates and immediate shifts *) +(** Recognition of integers that are acceptable as immediate operands + to the [rlwim] PowerPC instruction. These integers are of the form + [000011110000] or [111100001111], that is, a run of one bits + surrounded by zero bits, or conversely. We recognize these integers by + running the following automaton on the bits. The accepting states are + 2, 3, 4, 5, and 6. +<< + 0 1 0 + / \ / \ / \ + \ / \ / \ / + -0--> [1] --1--> [2] --0--> [3] + / + [0] + \ + -1--> [4] --0--> [5] --1--> [6] + / \ / \ / \ + \ / \ / \ / + 1 0 1 +>> +*) + +Inductive rlw_state: Type := + | RLW_S0 : rlw_state + | RLW_S1 : rlw_state + | RLW_S2 : rlw_state + | RLW_S3 : rlw_state + | RLW_S4 : rlw_state + | RLW_S5 : rlw_state + | RLW_S6 : rlw_state + | RLW_Sbad : rlw_state. + +Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state := + match s, b with + | RLW_S0, false => RLW_S1 + | RLW_S0, true => RLW_S4 + | RLW_S1, false => RLW_S1 + | RLW_S1, true => RLW_S2 + | RLW_S2, false => RLW_S3 + | RLW_S2, true => RLW_S2 + | RLW_S3, false => RLW_S3 + | RLW_S3, true => RLW_Sbad + | RLW_S4, false => RLW_S5 + | RLW_S4, true => RLW_S4 + | RLW_S5, false => RLW_S5 + | RLW_S5, true => RLW_S6 + | RLW_S6, false => RLW_Sbad + | RLW_S6, true => RLW_S6 + | RLW_Sbad, _ => RLW_Sbad + end. + +Definition rlw_accepting (s: rlw_state) : bool := + match s with + | RLW_S0 => false + | RLW_S1 => false + | RLW_S2 => true + | RLW_S3 => true + | RLW_S4 => true + | RLW_S5 => true + | RLW_S6 => true + | RLW_Sbad => false + end. + +Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool := + match n with + | O => + rlw_accepting s + | S m => + let (b, y) := Int.Z_bin_decomp x in + is_rlw_mask_rec m (rlw_transition s b) y + end. + +Definition is_rlw_mask (x: int) : bool := + is_rlw_mask_rec Int.wordsize RLW_S0 (Int.unsigned x). + (* Definition rolm (e1: expr) := match e1 with @@ -414,7 +488,7 @@ Definition rolm (e1: expr) (amount2 mask2: int) := | rolm_case2 amount1 mask1 t1 => let amount := Int.modu (Int.add amount1 amount2) Int.iwordsize in let mask := Int.and (Int.rol mask1 amount2) mask2 in - if Int.is_rlw_mask mask + if is_rlw_mask mask then Eop (Orolm amount mask) (t1:::Enil) else Eop (Orolm amount2 mask2) (e1:::Enil) | rolm_default e1 => @@ -548,7 +622,7 @@ Definition mul (e1: expr) (e2: expr) := (** ** Bitwise and, or, xor *) Definition andimm (n1: int) (e2: expr) := - if Int.is_rlw_mask n1 + if is_rlw_mask n1 then rolm e2 Int.zero n1 else Eop (Oandimm n1) (e2:::Enil). @@ -591,7 +665,7 @@ Definition or (e1: expr) (e2: expr) := match or_match e1 e2 with | or_case1 amount1 mask1 t1 amount2 mask2 t2 => if Int.eq amount1 amount2 - && Int.is_rlw_mask (Int.or mask1 mask2) + && is_rlw_mask (Int.or mask1 mask2) && same_expr_pure t1 t2 then Eop (Orolm amount1 (Int.or mask1 mask2)) (t1:::Enil) else Eop Oor (e1:::e2:::Enil) diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 21614e82..2fc13273 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -355,7 +355,7 @@ Lemma eval_rolm: Proof. intros until x. unfold rolm; case (rolm_match a); intros; InvEval. eauto with evalexpr. - case (Int.is_rlw_mask (Int.and (Int.rol mask1 amount) mask)). + case (is_rlw_mask (Int.and (Int.rol mask1 amount) mask)). EvalOp. simpl. subst x. decEq. decEq. symmetry. apply Int.rolm_rolm. apply int_wordsize_divides_modulus. @@ -460,7 +460,7 @@ Theorem eval_andimm: 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). + intros. unfold andimm. case (is_rlw_mask n). rewrite <- Int.rolm_zero. apply eval_rolm; auto. EvalOp. Qed. @@ -500,7 +500,7 @@ Lemma eval_or: 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) + && 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. -- cgit