diff options
| -rw-r--r-- | arm/PrintAsm.ml | 4 | ||||
| -rw-r--r-- | common/Memdata.v | 347 | ||||
| -rw-r--r-- | common/Memdataaux.ml | 51 | ||||
| -rw-r--r-- | extraction/extraction.v | 6 | ||||
| -rw-r--r-- | lib/Camlcoq.ml | 33 | ||||
| -rw-r--r-- | lib/Floataux.ml | 19 | ||||
| -rw-r--r-- | lib/Floats.v | 18 | ||||
| -rw-r--r-- | lib/Integers.v | 14 |
8 files changed, 261 insertions, 231 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index f5907f4..90b082b 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -14,7 +14,6 @@ open Printf open Datatypes -open Integers open Camlcoq open AST open Asm @@ -119,7 +118,8 @@ let label_float f = max_pos_constants := min !max_pos_constants (!currpos + 1024); lbl' -let symbol_labels = (Hashtbl.create 39 : (ident * Int.int, int) Hashtbl.t) +let symbol_labels = + (Hashtbl.create 39 : (ident * Integers.Int.int, int) Hashtbl.t) let label_symbol id ofs = try 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 *) - diff --git a/extraction/extraction.v b/extraction/extraction.v index e8fc572..797204f 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -42,11 +42,13 @@ Extract Constant Floats.Float.mul => "( *. )". Extract Constant Floats.Float.div => "( /. )". Extract Constant Floats.Float.cmp => "Floataux.cmp". Extract Constant Floats.Float.eq_dec => "fun (x: float) (y: float) -> x = y". +Extract Constant Floats.Float.bits_of_double => "Floataux.bits_of_double". +Extract Constant Floats.Float.double_of_bits => "Floataux.double_of_bits". +Extract Constant Floats.Float.bits_of_single => "Floataux.bits_of_single". +Extract Constant Floats.Float.single_of_bits => "Floataux.single_of_bits". (* Memdata *) Extract Constant Memdata.big_endian => "Memdataaux.big_endian". -Extract Constant Memdata.encode_float => "Memdataaux.encode_float". -Extract Constant Memdata.decode_float => "Memdataaux.decode_float". (* Memory - work around an extraction bug. *) Extraction NoInline Memory.Mem.valid_pointer. diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml index 51915fd..34aaa0f 100644 --- a/lib/Camlcoq.ml +++ b/lib/Camlcoq.ml @@ -18,7 +18,6 @@ open Datatypes open BinPos open BinInt -open Integers (* Integers *) @@ -32,7 +31,19 @@ let camlint_of_z = function | Zpos p -> camlint_of_positive p | Zneg p -> Int32.neg (camlint_of_positive p) -let camlint_of_coqint : Int.int -> int32 = camlint_of_z +let camlint_of_coqint : Integers.Int.int -> int32 = camlint_of_z + +let rec camlint64_of_positive = function + | Coq_xI p -> Int64.add (Int64.shift_left (camlint64_of_positive p) 1) 1L + | Coq_xO p -> Int64.shift_left (camlint64_of_positive p) 1 + | Coq_xH -> 1L + +let camlint64_of_z = function + | Z0 -> 0L + | Zpos p -> camlint64_of_positive p + | Zneg p -> Int64.neg (camlint64_of_positive p) + +let camlint64_of_coqint : Integers.Int64.int -> int64 = camlint64_of_z let rec camlint_of_nat = function | O -> 0 @@ -54,10 +65,26 @@ let z_of_camlint n = if n > 0l then Zpos (positive_of_camlint n) else Zneg (positive_of_camlint (Int32.neg n)) -let coqint_of_camlint (n: int32) : Int.int = +let coqint_of_camlint (n: int32) : Integers.Int.int = (* Interpret n as unsigned so that resulting Z is in range *) if n = 0l then Z0 else Zpos (positive_of_camlint n) +let rec positive_of_camlint64 n = + if n = 0L then assert false else + if n = 1L then Coq_xH else + if Int64.logand n 1L = 0L + then Coq_xO (positive_of_camlint64 (Int64.shift_right_logical n 1)) + else Coq_xI (positive_of_camlint64 (Int64.shift_right_logical n 1)) + +let z_of_camlint64 n = + if n = 0L then Z0 else + if n > 0L then Zpos (positive_of_camlint64 n) + else Zneg (positive_of_camlint64 (Int64.neg n)) + +let coqint_of_camlint64 (n: int64) : Integers.Int64.int = + (* Interpret n as unsigned so that resulting Z is in range *) + if n = 0L then Z0 else Zpos (positive_of_camlint64 n) + (* Atoms (positive integers representing strings) *) let atom_of_string = (Hashtbl.create 17 : (string, positive) Hashtbl.t) diff --git a/lib/Floataux.ml b/lib/Floataux.ml index 6b3b825..ebea884 100644 --- a/lib/Floataux.ml +++ b/lib/Floataux.ml @@ -11,7 +11,6 @@ (* *********************************************************************) open Camlcoq -open Integers let singleoffloat f = Int32.float_of_bits (Int32.bits_of_float f) @@ -31,9 +30,15 @@ let floatofintu i = let cmp c (x: float) (y: float) = match c with - | Ceq -> x = y - | Cne -> x <> y - | Clt -> x < y - | Cle -> x <= y - | Cgt -> x > y - | Cge -> x >= y + | Integers.Ceq -> x = y + | Integers.Cne -> x <> y + | Integers.Clt -> x < y + | Integers.Cle -> x <= y + | Integers.Cgt -> x > y + | Integers.Cge -> x >= y + +let bits_of_single f = coqint_of_camlint (Int32.bits_of_float f) +let single_of_bits f = Int32.float_of_bits (camlint_of_coqint f) + +let bits_of_double f = coqint_of_camlint64 (Int64.bits_of_float f) +let double_of_bits f = Int64.float_of_bits (camlint64_of_coqint f) diff --git a/lib/Floats.v b/lib/Floats.v index 2e60d73..50298f7 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -47,6 +47,12 @@ Parameter cmp: comparison -> float -> float -> bool. Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}. +Parameter bits_of_double: float -> int64. +Parameter double_of_bits: int64 -> float. + +Parameter bits_of_single: float -> int. +Parameter single_of_bits: int -> float. + (** Below are the only properties of floating-point arithmetic that we rely on in the compiler proof. *) @@ -67,4 +73,16 @@ Axiom cmp_ge_gt_eq: Axiom eq_zero_true: cmp Ceq zero zero = true. Axiom eq_zero_false: forall f, f <> zero -> cmp Ceq f zero = false. +Axiom bits_of_double_of_bits: + forall n, bits_of_double (double_of_bits n) = n. +Axiom double_of_bits_of_double: + forall f, double_of_bits (bits_of_double f) = f. +Axiom bits_of_single_of_bits: + forall n, bits_of_single (single_of_bits n) = n. +Axiom single_of_bits_of_single: + forall f, single_of_bits (bits_of_single f) = singleoffloat f. + +Axiom bits_of_singleoffloat: + forall f, bits_of_single (singleoffloat f) = bits_of_single f. + End Float. diff --git a/lib/Integers.v b/lib/Integers.v index d047199..f2aca96 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -2770,7 +2770,7 @@ Qed. End Make. -(** * Specialization to 32-bit integers and to bytes. *) +(** * Specialization to integers of size 8, 32, and 64 bits *) Module Wordsize_32. Definition wordsize := 32%nat. @@ -2797,3 +2797,15 @@ End Wordsize_8. Module Byte := Integers.Make(Wordsize_8). Notation byte := Byte.int. + +Module Wordsize_64. + Definition wordsize := 64%nat. + Remark wordsize_not_zero: wordsize <> 0%nat. + Proof. unfold wordsize; congruence. Qed. +End Wordsize_64. + +Module Int64 := Make(Wordsize_64). + +Notation int64 := Int64.int. + + |