From 440a0bf9ab0cae2372e339cca081b01e5551e332 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 26 May 2012 08:13:20 +0000 Subject: Memdata: cleanup continued Maps: add filter1 operation (could be useful some day) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1903 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Memdata.v | 283 +++++++++++++++++++++---------------------------------- 1 file changed, 105 insertions(+), 178 deletions(-) (limited to 'common') diff --git a/common/Memdata.v b/common/Memdata.v index fd77638..6f1ad67 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -136,12 +136,41 @@ Fixpoint int_of_bytes (l: list byte): Z := | b :: l' => Byte.unsigned b + int_of_bytes l' * 256 end. +Parameter big_endian: bool. + +Definition rev_if_be (l: list byte) : list byte := + if big_endian then List.rev l else l. + +Definition encode_int (sz: nat) (x: Z) : list byte := + rev_if_be (bytes_of_int sz x). + +Definition decode_int (b: list byte) : Z := + int_of_bytes (rev_if_be b). + +(** Length properties *) + Lemma length_bytes_of_int: forall n x, length (bytes_of_int n x) = n. Proof. induction n; simpl; intros. auto. decEq. auto. Qed. +Lemma rev_if_be_length: + forall l, length (rev_if_be l) = length l. +Proof. + intros; unfold rev_if_be; destruct big_endian. + apply List.rev_length. + auto. +Qed. + +Lemma encode_int_length: + forall sz x, length(encode_int sz x) = sz. +Proof. + intros. unfold encode_int. rewrite rev_if_be_length. apply length_bytes_of_int. +Qed. + +(** Decoding after encoding *) + Lemma int_of_bytes_of_int: forall n x, int_of_bytes (bytes_of_int n x) = x mod (two_p (Z_of_nat n * 8)). @@ -156,42 +185,6 @@ Opaque Byte.wordsize. 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 -> - bytes_of_int n x = bytes_of_int n y. -Proof. - induction n. - intros; simpl; auto. - intros until y. - rewrite inj_S. - replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega. - rewrite two_p_is_exp; try omega. - intro EQM. - simpl; decEq. - apply Byte.eqm_samerepr. red. - eapply Int.eqmod_divides; eauto. apply Zdivide_factor_l. - apply IHn. - destruct EQM as [k EQ]. exists k. rewrite EQ. - rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega. -Qed. - -Parameter big_endian: bool. - -Definition rev_if_be (l: list byte) : list byte := - if big_endian then List.rev l else l. - Lemma rev_if_be_involutive: forall l, rev_if_be (rev_if_be l) = l. Proof. @@ -200,146 +193,81 @@ Proof. auto. Qed. -Lemma rev_if_be_length: - forall l, length (rev_if_be l) = length l. +Lemma decode_encode_int: + forall n x, decode_int (encode_int n x) = x mod (two_p (Z_of_nat n * 8)). Proof. - intros; unfold rev_if_be; destruct big_endian. - apply List.rev_length. - auto. + unfold decode_int, encode_int; intros. rewrite rev_if_be_involutive. + apply int_of_bytes_of_int. Qed. -Definition encode_int (sz: nat) (x: int) : list byte := - rev_if_be (bytes_of_int sz (Int.unsigned x)). - -Definition decode_int (b: list byte) : int := - Int.repr (int_of_bytes (rev_if_be b)). +Lemma decode_encode_int_1: + forall x, Int.repr (decode_int (encode_int 1 (Int.unsigned x))) = Int.zero_ext 8 x. +Proof. + intros. rewrite decode_encode_int. + rewrite <- (Int.repr_unsigned (Int.zero_ext 8 x)). + decEq. symmetry. apply Int.zero_ext_mod. compute; auto. +Qed. -Lemma encode_int_length: - forall sz x, length(encode_int sz x) = sz. +Lemma decode_encode_int_2: + forall x, Int.repr (decode_int (encode_int 2 (Int.unsigned x))) = Int.zero_ext 16 x. Proof. - intros. unfold encode_int. rewrite rev_if_be_length. apply length_bytes_of_int. + intros. rewrite decode_encode_int. + rewrite <- (Int.repr_unsigned (Int.zero_ext 16 x)). + decEq. symmetry. apply Int.zero_ext_mod. compute; auto. Qed. -Lemma decode_encode_int_1: - forall x, decode_int (encode_int 1%nat x) = Int.zero_ext 8 x. +Lemma decode_encode_int_4: + forall x, Int.repr (decode_int (encode_int 4 (Int.unsigned x))) = x. Proof. - intros; unfold decode_int, encode_int. rewrite rev_if_be_involutive. - rewrite int_of_bytes_of_int_2. reflexivity. auto. + intros. rewrite decode_encode_int. transitivity (Int.repr (Int.unsigned x)). + decEq. apply Zmod_small. apply Int.unsigned_range. apply Int.repr_unsigned. Qed. -Lemma decode_encode_int_2: - forall x, decode_int (encode_int 2%nat x) = Int.zero_ext 16 x. +Lemma decode_encode_int_8: + forall x, Int64.repr (decode_int (encode_int 8 (Int64.unsigned x))) = x. Proof. - intros; unfold decode_int, encode_int. rewrite rev_if_be_involutive. - rewrite int_of_bytes_of_int_2. reflexivity. auto. + intros. rewrite decode_encode_int. transitivity (Int64.repr (Int64.unsigned x)). + decEq. apply Zmod_small. apply Int64.unsigned_range. apply Int64.repr_unsigned. Qed. -Lemma decode_encode_int_4: - forall x, decode_int (encode_int 4%nat x) = x. +(** A length-[n] encoding depends only on the low [8*n] bits of the integer. *) + +Lemma bytes_of_int_mod: + forall n x y, + Int.eqmod (two_p (Z_of_nat n * 8)) x y -> + bytes_of_int n x = bytes_of_int n y. Proof. - intros; unfold decode_int, encode_int. rewrite rev_if_be_involutive. - 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. + induction n. + intros; simpl; auto. + intros until y. + rewrite inj_S. + replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega. + rewrite two_p_is_exp; try omega. + intro EQM. + simpl; decEq. + apply Byte.eqm_samerepr. red. + eapply Int.eqmod_divides; eauto. apply Zdivide_factor_l. + apply IHn. + destruct EQM as [k EQ]. exists k. rewrite EQ. + rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega. Qed. Lemma encode_int_8_mod: forall x y, - Int.eqmod (two_p 8) (Int.unsigned x) (Int.unsigned y) -> + Int.eqmod (two_p 8) x y -> encode_int 1%nat x = encode_int 1%nat y. Proof. intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto. Qed. -Lemma encode_16_mod: +Lemma encode_int_16_mod: forall x y, - Int.eqmod (two_p 16) (Int.unsigned x) (Int.unsigned y) -> + Int.eqmod (two_p 16) x y -> encode_int 2%nat x = encode_int 2%nat y. Proof. intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto. Qed. -(** * Encoding and decoding floats *) - -Definition encode_float_32 (f: float) : list byte := - rev_if_be (bytes_of_int 4%nat (Int.unsigned (Float.bits_of_single f))). - -Definition encode_float_64 (f: float) : list byte := - rev_if_be (bytes_of_int 8%nat (Int64.unsigned (Float.bits_of_double f))). - -Definition decode_float_32 (b: list byte) : float := - Float.single_of_bits (Int.repr (int_of_bytes (rev_if_be b))). - -Definition decode_float_64 (b: list byte) : float := - Float.double_of_bits (Int64.repr (int_of_bytes (rev_if_be b))). - -Lemma encode_float_32_length: - forall n, length(encode_float_32 n) = 4%nat. -Proof. - unfold encode_float_32; intros. rewrite rev_if_be_length. apply length_bytes_of_int. -Qed. - -Lemma encode_float_64_length: - forall n, length(encode_float_64 n) = 8%nat. -Proof. - unfold encode_float_64; intros. rewrite rev_if_be_length. apply length_bytes_of_int. -Qed. - -Lemma decode_encode_float32: forall n, - decode_float_32 (encode_float_32 n) = Float.singleoffloat n. -Proof. - intros; unfold decode_float_32, encode_float_32. - rewrite rev_if_be_involutive. - rewrite int_of_bytes_of_int. rewrite <- Float.single_of_bits_of_single. - decEq. - transitivity (Int.repr (Int.unsigned (Float.bits_of_single n))). - apply Int.eqm_samerepr. apply Int.eqm_sym. apply Int.eqmod_mod. apply two_p_gt_ZERO. omega. - apply Int.repr_unsigned. -Qed. - -Lemma decode_encode_float64: forall n, - decode_float_64 (encode_float_64 n) = n. -Proof. - intros; unfold decode_float_64, encode_float_64. - rewrite rev_if_be_involutive. - rewrite int_of_bytes_of_int. - set (x := Float.bits_of_double n). - transitivity (Float.double_of_bits(Int64.repr (Int64.unsigned x))). - decEq. - apply Int64.eqm_samerepr. apply Int64.eqm_sym. apply Int64.eqmod_mod. apply two_p_gt_ZERO. omega. - rewrite Int64.repr_unsigned. apply Float.double_of_bits_of_double. -Qed. - -Lemma encode_float32_eq: - forall f, encode_float_32 f = encode_int 4%nat (Float.bits_of_single f). -Proof. - auto. -Qed. - -Lemma decode_float32_eq: - forall bl, decode_float_32 bl = Float.single_of_bits (decode_int bl). -Proof. - auto. -Qed. - -(* -Lemma encode_float32_cast: - forall f, - encode_float_32 (Float.singleoffloat f) = encode_float_32 f. -Proof. - intros; unfold encode_float_32. decEq. decEq. decEq. - apply Float.bits_of_singleoffloat. -Qed. - -Lemma decode_float32_cast: - forall l, - Float.singleoffloat (decode_float_32 l) = decode_float_32 l. -Proof. - intros; unfold decode_float_32. rewrite Float.singleoffloat_of_bits. auto. -Qed. -*) - (** * Encoding and decoding values *) Definition inj_bytes (bl: list byte) : list memval := @@ -398,12 +326,12 @@ Definition proj_pointer (vl: list memval) : val := Definition encode_val (chunk: memory_chunk) (v: val) : list memval := match v, chunk with - | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat n) - | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat n) - | Vint n, Mint32 => inj_bytes (encode_int 4%nat n) + | Vint n, (Mint8signed | Mint8unsigned) => inj_bytes (encode_int 1%nat (Int.unsigned n)) + | Vint n, (Mint16signed | Mint16unsigned) => inj_bytes (encode_int 2%nat (Int.unsigned n)) + | Vint n, Mint32 => inj_bytes (encode_int 4%nat (Int.unsigned n)) | Vptr b ofs, Mint32 => inj_pointer 4%nat b ofs - | Vfloat n, Mfloat32 => inj_bytes (encode_float_32 n) - | Vfloat n, Mfloat64 => inj_bytes (encode_float_64 n) + | Vfloat n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float.bits_of_single n))) + | Vfloat n, Mfloat64 => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.bits_of_double n))) | _, _ => list_repeat (size_chunk_nat chunk) Undef end. @@ -411,13 +339,13 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val := match proj_bytes vl with | Some bl => match chunk with - | Mint8signed => Vint(Int.sign_ext 8 (decode_int bl)) - | Mint8unsigned => Vint(Int.zero_ext 8 (decode_int bl)) - | Mint16signed => Vint(Int.sign_ext 16 (decode_int bl)) - | Mint16unsigned => Vint(Int.zero_ext 16 (decode_int bl)) - | Mint32 => Vint(decode_int bl) - | Mfloat32 => Vfloat(decode_float_32 bl) - | Mfloat64 => Vfloat(decode_float_64 bl) + | Mint8signed => Vint(Int.sign_ext 8 (Int.repr (decode_int bl))) + | Mint8unsigned => Vint(Int.zero_ext 8 (Int.repr (decode_int bl))) + | Mint16signed => Vint(Int.sign_ext 16 (Int.repr (decode_int bl))) + | Mint16unsigned => Vint(Int.zero_ext 16 (Int.repr (decode_int bl))) + | Mint32 => Vint(Int.repr(decode_int bl)) + | Mfloat32 => Vfloat(Float.single_of_bits (Int.repr (decode_int bl))) + | Mfloat64 => Vfloat(Float.double_of_bits (Int64.repr (decode_int bl))) end | None => match chunk with @@ -429,8 +357,10 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val := Lemma encode_val_length: forall chunk v, length(encode_val chunk v) = size_chunk_nat chunk. Proof. - intros. destruct v; simpl; destruct chunk; try (apply length_list_repeat); auto; - rewrite length_inj_bytes; try (apply encode_int_length). apply encode_float_64_length. + intros. destruct v; simpl; destruct chunk; + solve [ reflexivity + | apply length_list_repeat + | rewrite length_inj_bytes; apply encode_int_length ]. Qed. Lemma check_inj_pointer: @@ -489,13 +419,13 @@ Opaque inj_pointer. rewrite decode_encode_int_2. decEq. apply Int.sign_ext_zero_ext. compute; auto. rewrite decode_encode_int_2. decEq. apply Int.zero_ext_idem. compute; auto. rewrite decode_encode_int_4. auto. - rewrite decode_float32_eq. rewrite decode_encode_int_4. auto. - rewrite encode_float32_eq. rewrite decode_encode_int_4. auto. - rewrite decode_encode_float32. auto. - rewrite decode_encode_float64. auto. + rewrite decode_encode_int_4. auto. + rewrite decode_encode_int_4. auto. + rewrite decode_encode_int_4. decEq. apply Float.single_of_bits_of_single. + rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double. change (proj_bytes (inj_pointer 4 b i)) with (@None (list byte)). simpl. - unfold proj_pointer. generalize (check_inj_pointer b i 4%nat). -Transparent inj_pointer. + unfold proj_pointer. generalize (check_inj_pointer b i 4%nat). +Transparent inj_pointer. simpl. intros EQ; rewrite EQ; auto. Qed. @@ -552,13 +482,13 @@ Qed. Lemma encode_val_int16_zero_ext: forall n, encode_val Mint16unsigned (Vint (Int.zero_ext 16 n)) = encode_val Mint16unsigned (Vint n). Proof. - intros; unfold encode_val. decEq. apply encode_16_mod. apply Int.eqmod_zero_ext. compute; auto. + intros; unfold encode_val. decEq. apply encode_int_16_mod. apply Int.eqmod_zero_ext. compute; auto. Qed. Lemma encode_val_int16_sign_ext: forall n, encode_val Mint16signed (Vint (Int.sign_ext 16 n)) = encode_val Mint16signed (Vint n). Proof. - intros; unfold encode_val. decEq. apply encode_16_mod. apply Int.eqmod_sign_ext'. compute; auto. + intros; unfold encode_val. decEq. apply encode_int_16_mod. apply Int.eqmod_sign_ext'. compute; auto. Qed. Lemma decode_val_cast: @@ -578,7 +508,7 @@ Proof. unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. compute; auto. unfold Val.sign_ext. rewrite Int.sign_ext_idem; auto. compute; auto. unfold Val.zero_ext. rewrite Int.zero_ext_idem; auto. compute; auto. - simpl. rewrite decode_float32_eq. rewrite Float.singleoffloat_of_bits. auto. + simpl. rewrite Float.singleoffloat_of_bits. auto. Qed. (** Pointers cannot be forged. *) @@ -606,16 +536,15 @@ Lemma encode_val_shape: Proof. intros. destruct (size_chunk_nat_pos chunk) as [sz1 EQ]. - assert (encoding_shape (list_repeat (size_chunk_nat chunk) Undef)). + assert (A: encoding_shape (list_repeat (size_chunk_nat chunk) Undef)). rewrite EQ; simpl; constructor. exact I. intros. replace mv with Undef. exact I. symmetry; eapply in_list_repeat; eauto. - assert (forall bl, length bl = size_chunk_nat chunk -> + assert (B: forall bl, length bl = size_chunk_nat chunk -> encoding_shape (inj_bytes bl)). intros. destruct bl; simpl in *. congruence. constructor. exact I. unfold inj_bytes. intros. - exploit list_in_map_inv; eauto. intros [x [A B]]. subst mv. exact I. - destruct v; auto; destruct chunk; simpl; auto; try (apply H0); try (apply encode_int_length). - apply encode_float_64_length. + exploit list_in_map_inv; eauto. intros [x [C D]]. subst mv. exact I. + destruct v; auto; destruct chunk; simpl; auto; try (apply B; apply encode_int_length). constructor. red. auto. simpl; intros. intuition; subst mv; red; simpl; congruence. Qed. @@ -678,9 +607,7 @@ Proof. intros. destruct bl; simpl in *; congruence. unfold encode_val; destruct v; destruct chunk; (apply A; assumption) || - (apply B; try (rewrite encode_int_length; congruence)) || idtac. - rewrite encode_float_32_length; congruence. - rewrite encode_float_64_length; congruence. + (apply B; rewrite encode_int_length; congruence) || idtac. simpl. intros EQ; inv EQ; auto. Qed. -- cgit v1.2.3