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 --- common/Memdata.v | 82 ++++++++++++++++++++++---------------------------------- 1 file changed, 32 insertions(+), 50 deletions(-) (limited to 'common') diff --git a/common/Memdata.v b/common/Memdata.v index 20c0b10..c0e1f50 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -148,6 +148,7 @@ Lemma int_of_bytes_of_int: Proof. induction n; intros. simpl. rewrite Zmod_1_r. auto. +Opaque Byte.wordsize. rewrite inj_S. simpl. replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega. rewrite two_p_is_exp; try omega. @@ -155,6 +156,17 @@ Proof. apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega. Qed. +Lemma int_of_bytes_of_int_2: + forall n x, + (n = 1 \/ n = 2)%nat -> + Int.repr (int_of_bytes (bytes_of_int n (Int.unsigned x))) = Int.zero_ext (Z_of_nat n * 8) x. +Proof. + intros. rewrite int_of_bytes_of_int. + rewrite <- (Int.repr_unsigned (Int.zero_ext (Z_of_nat n * 8) x)). + decEq. symmetry. apply Int.zero_ext_mod. + destruct H; subst n; compute; auto. +Qed. + Lemma bytes_of_int_mod: forall n x y, Int.eqmod (two_p (Z_of_nat n * 8)) x y -> @@ -239,11 +251,16 @@ Lemma decode_encode_int: end. Proof. intros. unfold decode_int, encode_int; destruct c; auto; - rewrite rev_if_be_involutive; rewrite int_of_bytes_of_int. - apply Int.sign_ext_zero_ext; vm_compute; auto. - apply Int.zero_ext_idem; vm_compute; auto. - apply Int.sign_ext_zero_ext; vm_compute; auto. - apply Int.zero_ext_idem; vm_compute; auto. + rewrite rev_if_be_involutive. + rewrite int_of_bytes_of_int_2; auto. + apply Int.sign_ext_zero_ext. compute; auto. + rewrite int_of_bytes_of_int_2; auto. + apply Int.zero_ext_idem. compute; auto. + rewrite int_of_bytes_of_int_2; auto. + apply Int.sign_ext_zero_ext. compute; auto. + rewrite int_of_bytes_of_int_2; auto. + apply Int.zero_ext_idem. compute; auto. + rewrite int_of_bytes_of_int. transitivity (Int.repr (Int.unsigned x)). apply Int.eqm_samerepr. apply Int.eqm_sym. apply Int.eqmod_mod. apply two_p_gt_ZERO. omega. apply Int.repr_unsigned. @@ -267,8 +284,7 @@ Lemma encode_int8_zero_ext: forall x, encode_int Mint8unsigned (Int.zero_ext 8 x) = encode_int Mint8unsigned x. Proof. - intros. apply encode_8_mod. apply Int.eqmod_sym. - apply Int.eqmod_two_p_zero_ext. compute; auto. + intros. apply encode_8_mod. apply Int.eqmod_zero_ext. compute; auto. Qed. Lemma encode_int8_sign_ext: @@ -276,8 +292,10 @@ Lemma encode_int8_sign_ext: encode_int Mint8signed (Int.sign_ext 8 x) = encode_int Mint8signed x. Proof. intros. repeat rewrite encode_int8_signed_unsigned. - apply encode_8_mod. apply Int.eqmod_sym. - apply Int.eqmod_two_p_sign_ext. compute; auto. + apply encode_8_mod. eapply Int.eqmod_trans. + apply Int.eqm_eqmod_two_p. compute; auto. + apply Int.eqm_sym. apply Int.eqm_signed_unsigned. + apply Int.eqmod_sign_ext. compute; auto. Qed. Lemma encode_int16_signed_unsigned: forall n, @@ -298,8 +316,7 @@ Lemma encode_int16_zero_ext: forall x, encode_int Mint16unsigned (Int.zero_ext 16 x) = encode_int Mint16unsigned x. Proof. - intros. apply encode_16_mod. apply Int.eqmod_sym. - apply (Int.eqmod_two_p_zero_ext 16). compute; auto. + intros. apply encode_16_mod. apply Int.eqmod_zero_ext. compute; auto. Qed. Lemma encode_int16_sign_ext: @@ -307,8 +324,10 @@ Lemma encode_int16_sign_ext: encode_int Mint16signed (Int.sign_ext 16 x) = encode_int Mint16signed x. Proof. intros. repeat rewrite encode_int16_signed_unsigned. - apply encode_16_mod. apply Int.eqmod_sym. - apply Int.eqmod_two_p_sign_ext. compute; auto. + apply encode_16_mod. eapply Int.eqmod_trans. + apply Int.eqm_eqmod_two_p. compute; auto. + apply Int.eqm_sym. apply Int.eqm_signed_unsigned. + apply Int.eqmod_sign_ext. compute; auto. Qed. Lemma decode_int8_zero_ext: @@ -860,43 +879,6 @@ Proof. split; auto. subst mvl. apply encode_pointer_shape. Qed. -(* -Lemma proj_bytes_none: - forall mv, - match mv with Byte _ => False | _ => True end -> - forall mvl, - In mv mvl -> - proj_bytes mvl = None. -Proof. - induction mvl; simpl; intros. - elim H0. - destruct a; auto. destruct H0. subst mv. contradiction. - rewrite (IHmvl H0); auto. -Qed. - -Lemma decode_val_undef: - forall chunk mv mv1 mvl, - match mv with - | Pointer b ofs n => n = pred (size_chunk_nat Mint32) - | Undef => True - | _ => False - end -> - In mv mvl -> - decode_val chunk (mv1 :: mvl) = Vundef. -Proof. - intros. unfold decode_val. - replace (proj_bytes (mv1 :: mvl)) with (@None (list byte)). - destruct chunk; auto. unfold proj_pointer. destruct mv1; auto. - case_eq (check_pointer (size_chunk_nat Mint32) b i (Pointer b i n :: mvl)); intros. - exploit check_pointer_inv; eauto. simpl. intros. inv H2. - simpl in H0. intuition; subst mv; simpl in H; congruence. - auto. - symmetry. apply proj_bytes_none with mv. - destruct mv; tauto. auto with coqlib. -Qed. - -*) - (** * Compatibility with memory injections *) (** Relating two memory values according to a memory injection. *) -- cgit v1.2.3