From d71a5cfd10378301b71d32659d5936e01d72ae50 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 9 May 2010 08:18:51 +0000
Subject: [PATCH] Revised encoding/decoding of floats
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1341 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
arm/PrintAsm.ml | 4 +-
common/Memdata.v | 347 +++++++++++++++++++++-------------------
common/Memdataaux.ml | 51 ------
extraction/extraction.v | 6 +-
lib/Camlcoq.ml | 33 +++-
lib/Floataux.ml | 19 ++-
lib/Floats.v | 18 +++
lib/Integers.v | 14 +-
8 files changed, 261 insertions(+), 231 deletions(-)
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index f5907f407..90b082bea 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 c5ec9a05a..8bbb4043b 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 3a3942846..0ec7523b3 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 e8fc57214..797204fbc 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 51915fd53..34aaa0fde 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 6b3b825f1..ebea88414 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 2e60d73e0..50298f707 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 d047199d6..f2aca962b 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.
+
+
--
GitLab