From d71a5cfd10378301b71d32659d5936e01d72ae50 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 9 May 2010 08:18:51 +0000 Subject: Revised encoding/decoding of floats git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Memdata.v | 347 +++++++++++++++++++++++++++------------------------ common/Memdataaux.ml | 51 -------- 2 files changed, 182 insertions(+), 216 deletions(-) (limited to 'common') diff --git a/common/Memdata.v b/common/Memdata.v index c5ec9a0..8bbb404 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -137,132 +137,129 @@ Inductive memval: Type := (** We define functions to convert between integers and lists of bytes according to a given memory chunk. *) +Fixpoint bytes_of_int (n: nat) (x: Z) {struct n}: list byte := + match n with + | O => nil + | S m => Byte.repr x :: bytes_of_int m (x / 256) + end. + +Fixpoint int_of_bytes (l: list byte): Z := + match l with + | nil => 0 + | b :: l' => Byte.unsigned b + int_of_bytes l' * 256 + end. + +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 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)). +Proof. + induction n; intros. + simpl. rewrite Zmod_1_r. auto. + 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. + rewrite Zmod_recombine. rewrite IHn. rewrite Zplus_comm. reflexivity. + apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega. +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_le (l: list byte) : list byte := - if big_endian then l else List.rev l. +Definition rev_if_be (l: list byte) : list byte := + if big_endian then List.rev l else l. -Lemma rev_if_le_involutive: - forall l, rev_if_le (rev_if_le l) = l. +Lemma rev_if_be_involutive: + forall l, rev_if_be (rev_if_be l) = l. Proof. - intros; unfold rev_if_le; destruct big_endian. - auto. + intros; unfold rev_if_be; destruct big_endian. apply List.rev_involutive. + auto. Qed. -Lemma rev_if_le_length: - forall l, length (rev_if_le l) = length l. +Lemma rev_if_be_length: + forall l, length (rev_if_be l) = length l. Proof. - intros; unfold rev_if_le; destruct big_endian. - auto. + intros; unfold rev_if_be; destruct big_endian. apply List.rev_length. + auto. Qed. Definition encode_int (c: memory_chunk) (x: int) : list byte := let n := Int.unsigned x in - rev_if_le (match c with - | Mint8signed | Mint8unsigned => - Byte.repr n :: nil - | Mint16signed | Mint16unsigned => - Byte.repr (n/256) :: Byte.repr n :: nil - | Mint32 => - Byte.repr (n/16777216) :: Byte.repr (n/65536) :: Byte.repr (n/256) :: Byte.repr n :: nil - | Mfloat32 => - Byte.zero :: Byte.zero :: Byte.zero :: Byte.zero :: nil - | Mfloat64 => - Byte.zero :: Byte.zero :: Byte.zero :: Byte.zero :: - Byte.zero :: Byte.zero :: Byte.zero :: Byte.zero :: nil + rev_if_be (match c with + | Mint8signed | Mint8unsigned => bytes_of_int 1%nat n + | Mint16signed | Mint16unsigned => bytes_of_int 2%nat n + | Mint32 => bytes_of_int 4%nat n + | Mfloat32 => bytes_of_int 4%nat 0 + | Mfloat64 => bytes_of_int 8%nat 0 end). Definition decode_int (c: memory_chunk) (b: list byte) : int := - match c, rev_if_le b with - | Mint8signed, b1 :: nil => - Int.sign_ext 8 (Int.repr (Byte.unsigned b1)) - | Mint8unsigned, b1 :: nil => - Int.repr (Byte.unsigned b1) - | Mint16signed, b1 :: b2 :: nil => - Int.sign_ext 16 (Int.repr (Byte.unsigned b1 * 256 + Byte.unsigned b2)) - | Mint16unsigned, b1 :: b2 :: nil => - Int.repr (Byte.unsigned b1 * 256 + Byte.unsigned b2) - | Mint32, b1 :: b2 :: b3 :: b4 :: nil => - Int.repr (Byte.unsigned b1 * 16777216 + Byte.unsigned b2 * 65536 - + Byte.unsigned b3 * 256 + Byte.unsigned b4) - | _, _ => Int.zero + let b' := rev_if_be b in + match c with + | Mint8signed => Int.sign_ext 8 (Int.repr (int_of_bytes b')) + | Mint8unsigned => Int.zero_ext 8 (Int.repr (int_of_bytes b')) + | Mint16signed => Int.sign_ext 16 (Int.repr (int_of_bytes b')) + | Mint16unsigned => Int.zero_ext 16 (Int.repr (int_of_bytes b')) + | Mint32 => Int.repr (int_of_bytes b') + | Mfloat32 => Int.zero + | Mfloat64 => Int.zero end. Lemma encode_int_length: forall chunk n, length(encode_int chunk n) = size_chunk_nat chunk. Proof. - intros. unfold encode_int. rewrite rev_if_le_length. - destruct chunk; reflexivity. + intros. unfold encode_int. rewrite rev_if_be_length. + destruct chunk; rewrite length_bytes_of_int; reflexivity. Qed. -Lemma decode_encode_int8unsigned: forall n, - decode_int Mint8unsigned (encode_int Mint8unsigned n) = Int.zero_ext 8 n. -Proof. - intros. unfold decode_int, encode_int. rewrite rev_if_le_involutive. - simpl. auto. -Qed. - -Lemma decode_encode_int8signed: forall n, - decode_int Mint8signed (encode_int Mint8signed n) = Int.sign_ext 8 n. -Proof. - intros. unfold decode_int, encode_int. rewrite rev_if_le_involutive. simpl. - change (Int.repr (Int.unsigned n mod Byte.modulus)) - with (Int.zero_ext 8 n). - apply Int.sign_ext_zero_ext. compute; auto. -Qed. - -Remark recombine_16: - forall x, - (x / 256) mod Byte.modulus * 256 + x mod Byte.modulus = x mod (two_p 16). -Proof. - intros. symmetry. apply (Zmod_recombine x 256 256); omega. -Qed. - -Lemma decode_encode_int16unsigned: forall n, - decode_int Mint16unsigned (encode_int Mint16unsigned n) = Int.zero_ext 16 n. -Proof. - intros. unfold decode_int, encode_int. rewrite rev_if_le_involutive. simpl. - rewrite recombine_16. auto. -Qed. - -Lemma decode_encode_int16signed: forall n, - decode_int Mint16signed (encode_int Mint16signed n) = Int.sign_ext 16 n. +Lemma decode_encode_int: + forall c x, + decode_int c (encode_int c x) = + match c with + | Mint8signed => Int.sign_ext 8 x + | Mint8unsigned => Int.zero_ext 8 x + | Mint16signed => Int.sign_ext 16 x + | Mint16unsigned => Int.zero_ext 16 x + | Mint32 => x + | Mfloat32 => Int.zero + | Mfloat64 => Int.zero + end. Proof. - intros. unfold decode_int, encode_int. rewrite rev_if_le_involutive. simpl. - rewrite recombine_16. - fold (Int.zero_ext 16 n). apply Int.sign_ext_zero_ext. compute; auto. -Qed. - -Remark recombine_32: - forall x, - (x / 16777216) mod Byte.modulus * 16777216 - + (x / 65536) mod Byte.modulus * 65536 - + (x / 256) mod Byte.modulus * 256 - + x mod Byte.modulus = - x mod Int.modulus. -Proof. - intros. change Byte.modulus with 256. - exploit (Zmod_recombine x 65536 65536). omega. omega. intro EQ1. - exploit (Zmod_recombine x 256 256). omega. omega. - change (256 * 256) with 65536. intro EQ2. - exploit (Zmod_recombine (x/65536) 256 256). omega. omega. - rewrite Zdiv_Zdiv. change (65536*256) with 16777216. change (256 * 256) with 65536. - intro EQ3. - change Int.modulus with (65536 * 65536). - rewrite EQ1. rewrite EQ2. rewrite EQ3. omega. - omega. omega. -Qed. - -Lemma decode_encode_int32: forall n, - decode_int Mint32 (encode_int Mint32 n) = n. -Proof. - intros. unfold decode_int, encode_int. rewrite rev_if_le_involutive. simpl. - rewrite recombine_32. - transitivity (Int.repr (Int.unsigned n)). 2: apply Int.repr_unsigned. - apply Int.eqm_samerepr. apply Int.eqm_sym. red. apply Int.eqmod_mod. - apply Int.modulus_pos. + 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. + 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. Qed. Lemma encode_int8_signed_unsigned: forall n, @@ -276,7 +273,7 @@ Remark encode_8_mod: Int.eqmod (two_p 8) (Int.unsigned x) (Int.unsigned y) -> encode_int Mint8unsigned x = encode_int Mint8unsigned y. Proof. - intros. unfold encode_int. decEq. decEq. apply Byte.eqm_samerepr. exact H. + intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto. Qed. Lemma encode_int8_zero_ext: @@ -307,19 +304,7 @@ Remark encode_16_mod: Int.eqmod (two_p 16) (Int.unsigned x) (Int.unsigned y) -> encode_int Mint16unsigned x = encode_int Mint16unsigned y. Proof. - intros. unfold encode_int. decEq. - set (x' := Int.unsigned x) in *. - set (y' := Int.unsigned y) in *. - assert (Int.eqmod (two_p 8) x' y'). - eapply Int.eqmod_divides; eauto. exists (two_p 8); auto. - assert (Int.eqmod (two_p 8) (x' / 256) (y' / 256)). - destruct H as [k EQ]. - exists k. rewrite EQ. - replace (k * two_p 16) with ((k * two_p 8) * two_p 8). - rewrite Zplus_comm. rewrite Z_div_plus. omega. - omega. rewrite <- Zmult_assoc. auto. - decEq. apply Byte.eqm_samerepr. exact H1. - decEq. apply Byte.eqm_samerepr. exact H0. + intros. unfold encode_int. decEq. apply bytes_of_int_mod. auto. Qed. Lemma encode_int16_zero_ext: @@ -343,91 +328,123 @@ Lemma decode_int8_zero_ext: forall l, Int.zero_ext 8 (decode_int Mint8unsigned l) = decode_int Mint8unsigned l. Proof. - intros; simpl. destruct (rev_if_le l); auto. destruct l0; auto. - unfold Int.zero_ext. decEq. - generalize (Byte.unsigned_range i). intro. - rewrite Int.unsigned_repr. apply Zmod_small. assumption. - assert (Byte.modulus < Int.max_unsigned). vm_compute. auto. - omega. + intros; simpl. apply Int.zero_ext_idem. vm_compute; auto. Qed. Lemma decode_int8_sign_ext: forall l, Int.sign_ext 8 (decode_int Mint8signed l) = decode_int Mint8signed l. Proof. - intros; simpl. destruct (rev_if_le l); auto. destruct l0; auto. - rewrite Int.sign_ext_idem. auto. vm_compute; auto. + intros; simpl. apply Int.sign_ext_idem. vm_compute; auto. Qed. Lemma decode_int16_zero_ext: forall l, Int.zero_ext 16 (decode_int Mint16unsigned l) = decode_int Mint16unsigned l. Proof. - intros; simpl. destruct (rev_if_le l); auto. destruct l0; auto. destruct l0; auto. - unfold Int.zero_ext. decEq. - generalize (Byte.unsigned_range i) (Byte.unsigned_range i0). - change Byte.modulus with 256. intros. - assert (0 <= Byte.unsigned i * 256 + Byte.unsigned i0 < 65536). omega. - rewrite Int.unsigned_repr. apply Zmod_small. assumption. - assert (65536 < Int.max_unsigned). vm_compute. auto. - omega. + intros; simpl. apply Int.zero_ext_idem. vm_compute; auto. Qed. Lemma decode_int16_sign_ext: forall l, Int.sign_ext 16 (decode_int Mint16signed l) = decode_int Mint16signed l. Proof. - intros; simpl. destruct (rev_if_le l); auto. destruct l0; auto. destruct l0; auto. - rewrite Int.sign_ext_idem. auto. vm_compute; auto. + intros; simpl. apply Int.sign_ext_idem. vm_compute; auto. Qed. Lemma decode_int8_signed_unsigned: forall l, decode_int Mint8signed l = Int.sign_ext 8 (decode_int Mint8unsigned l). Proof. - unfold decode_int; intros. destruct (rev_if_le l); auto. destruct l0; auto. + intros; simpl. rewrite Int.sign_ext_zero_ext; auto. vm_compute; auto. Qed. Lemma decode_int16_signed_unsigned: forall l, decode_int Mint16signed l = Int.sign_ext 16 (decode_int Mint16unsigned l). Proof. - unfold decode_int; intros. destruct (rev_if_le l); auto. - destruct l0; auto. destruct l0; auto. + intros; simpl. rewrite Int.sign_ext_zero_ext; auto. vm_compute; auto. Qed. (** * Encoding and decoding floats *) -Parameter encode_float: memory_chunk -> float -> list byte. -Parameter decode_float: memory_chunk -> list byte -> float. +Definition encode_float (c: memory_chunk) (f: float) : list byte := + rev_if_be (match c with + | Mint8signed | Mint8unsigned => bytes_of_int 1%nat 0 + | Mint16signed | Mint16unsigned => bytes_of_int 2%nat 0 + | Mint32 => bytes_of_int 4%nat 0 + | Mfloat32 => bytes_of_int 4%nat (Int.unsigned (Float.bits_of_single f)) + | Mfloat64 => bytes_of_int 8%nat (Int64.unsigned (Float.bits_of_double f)) + end). -Axiom encode_float_length: +Definition decode_float (c: memory_chunk) (b: list byte) : float := + let b' := rev_if_be b in + match c with + | Mfloat32 => Float.single_of_bits (Int.repr (int_of_bytes b')) + | Mfloat64 => Float.double_of_bits (Int64.repr (int_of_bytes b')) + | _ => Float.zero + end. + +Lemma encode_float_length: forall chunk n, length(encode_float chunk n) = size_chunk_nat chunk. +Proof. + unfold encode_float; intros. + rewrite rev_if_be_length. + destruct chunk; apply length_bytes_of_int. +Qed. -(* More realistic: - decode_float Mfloat32 (encode_float Mfloat32 (Float.singleoffloat n)) = - Float.singleoffloat n -*) -Axiom decode_encode_float32: forall n, +Lemma decode_encode_float32: forall n, decode_float Mfloat32 (encode_float Mfloat32 n) = Float.singleoffloat n. -Axiom decode_encode_float64: forall n, - decode_float Mfloat64 (encode_float Mfloat64 n) = n. +Proof. + intros; unfold decode_float, encode_float. + 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. -Axiom encode_float32_singleoffloat: forall n, - encode_float Mfloat32 (Float.singleoffloat n) = encode_float Mfloat32 n. +Lemma decode_encode_float64: forall n, + decode_float Mfloat64 (encode_float Mfloat64 n) = n. +Proof. + intros; unfold decode_float, encode_float. + 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. -Axiom encode_float8_signed_unsigned: forall n, +Lemma encode_float8_signed_unsigned: forall n, encode_float Mint8signed n = encode_float Mint8unsigned n. -Axiom encode_float16_signed_unsigned: forall n, +Proof. + intros. reflexivity. +Qed. + +Lemma encode_float16_signed_unsigned: forall n, encode_float Mint16signed n = encode_float Mint16unsigned n. +Proof. + intros. reflexivity. +Qed. -Axiom encode_float32_cast: +Lemma encode_float32_cast: forall f, encode_float Mfloat32 (Float.singleoffloat f) = encode_float Mfloat32 f. +Proof. + intros; unfold encode_float. decEq. decEq. decEq. + apply Float.bits_of_singleoffloat. +Qed. -Axiom decode_float32_cast: +Lemma decode_float32_cast: forall l, Float.singleoffloat (decode_float Mfloat32 l) = decode_float Mfloat32 l. +Proof. + intros; unfold decode_float. rewrite <- Float.single_of_bits_of_single. + rewrite Float.bits_of_single_of_bits. auto. +Qed. (** * Encoding and decoding values *) @@ -573,16 +590,16 @@ Proof. simpl. destruct chunk1; auto; destruct chunk2; auto; unfold decode_val; rewrite proj_inj_bytes. - rewrite decode_encode_int8signed. auto. - rewrite encode_int8_signed_unsigned. rewrite decode_encode_int8unsigned. auto. - rewrite <- encode_int8_signed_unsigned. rewrite decode_encode_int8signed. auto. - rewrite decode_encode_int8unsigned. auto. - rewrite decode_encode_int16signed. auto. - rewrite encode_int16_signed_unsigned. rewrite decode_encode_int16unsigned. auto. - rewrite <- encode_int16_signed_unsigned. rewrite decode_encode_int16signed. auto. - rewrite decode_encode_int16unsigned. auto. - rewrite decode_encode_int32. auto. - auto. + rewrite decode_encode_int. auto. + rewrite encode_int8_signed_unsigned. rewrite decode_encode_int. auto. + rewrite <- encode_int8_signed_unsigned. rewrite decode_encode_int. auto. + rewrite decode_encode_int. auto. + rewrite decode_encode_int. auto. + rewrite encode_int16_signed_unsigned. rewrite decode_encode_int. auto. + rewrite <- encode_int16_signed_unsigned. rewrite decode_encode_int. auto. + rewrite decode_encode_int. auto. + rewrite decode_encode_int. auto. + reflexivity. (* Vfloat *) unfold decode_val, encode_val, decode_encode_val; destruct chunk1; auto; destruct chunk2; auto; unfold decode_val; @@ -636,13 +653,13 @@ Qed. Lemma encode_val_int8_signed_unsigned: forall v, encode_val Mint8signed v = encode_val Mint8unsigned v. Proof. - intros. destruct v; simpl; auto. rewrite encode_float8_signed_unsigned; auto. + intros. destruct v; simpl; auto. Qed. Lemma encode_val_int16_signed_unsigned: forall v, encode_val Mint16signed v = encode_val Mint16unsigned v. Proof. - intros. destruct v; simpl; auto. rewrite encode_float16_signed_unsigned; auto. + intros. destruct v; simpl; auto. Qed. Lemma encode_val_int8_zero_ext: diff --git a/common/Memdataaux.ml b/common/Memdataaux.ml index 3a39428..0ec7523 100644 --- a/common/Memdataaux.ml +++ b/common/Memdataaux.ml @@ -10,59 +10,8 @@ (* *) (* *********************************************************************) -open Camlcoq -open Integers -open AST - let big_endian = match Configuration.arch with | "powerpc" -> true | "arm" -> false | _ -> assert false - -let encode_float chunk f = - match chunk with - | Mint8unsigned | Mint8signed -> - [Byte.zero] - | Mint16unsigned | Mint16signed -> - [Byte.zero; Byte.zero] - | Mint32 -> - [Byte.zero; Byte.zero; Byte.zero; Byte.zero] - | Mfloat32 -> - let bits = Int32.bits_of_float f in - let byte n = - coqint_of_camlint - (Int32.logand (Int32.shift_right_logical bits n) 0xFFl) in - if big_endian then - [byte 24; byte 16; byte 8; byte 0] - else - [byte 0; byte 8; byte 16; byte 24] - | Mfloat64 -> - let bits = Int64.bits_of_float f in - let byte n = - coqint_of_camlint - (Int64.to_int32 - (Int64.logand (Int64.shift_right_logical bits n) 0xFFL)) in - if big_endian then - [byte 56; byte 48; byte 40; byte 32; byte 24; byte 16; byte 8; byte 0] - else - [byte 0; byte 8; byte 16; byte 24; byte 32; byte 40; byte 48; byte 56] - -let decode_float chunk bytes = - match chunk with - | Mfloat32 -> - let combine accu b = - Int32.logor (Int32.shift_left accu 8) (camlint_of_coqint b) in - Int32.float_of_bits - (List.fold_left combine 0l - (if big_endian then bytes else List.rev bytes)) - | Mfloat64 -> - let combine accu b = - Int64.logor (Int64.shift_left accu 8) - (Int64.of_int32 (camlint_of_coqint b)) in - Int64.float_of_bits - (List.fold_left combine 0L - (if big_endian then bytes else List.rev bytes)) - | _ -> - 0.0 (* unspecified *) - -- cgit v1.2.3