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/Asmgenproof1.v | 54 ++++++++++++++++++-------------------------------- 1 file changed, 19 insertions(+), 35 deletions(-) (limited to 'powerpc/Asmgenproof1.v') 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. -- cgit