From 7998ccfd709b97f1a2306df4570365d58a5bb4b5 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 12 Jan 2014 10:48:56 +0000 Subject: - Back to origins: suppress Mfloat64al32 chunk and align Mfloat64 to 4. - Revised printing of intermediate RTL code. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2403 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/AST.v | 7 ++----- common/Memdata.v | 23 ++++++++--------------- common/Memory.v | 6 +++++- common/PrintAST.ml | 1 - common/Values.v | 2 +- 5 files changed, 16 insertions(+), 23 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index 5eee291..6f35be0 100644 --- a/common/AST.v +++ b/common/AST.v @@ -133,8 +133,7 @@ Inductive memory_chunk : Type := | Mint32 (**r 32-bit integer, or pointer *) | Mint64 (**r 64-bit integer *) | Mfloat32 (**r 32-bit single-precision float *) - | Mfloat64 (**r 64-bit double-precision float *) - | Mfloat64al32. (**r 64-bit double-precision float, 4-aligned *) + | Mfloat64. (**r 64-bit double-precision float *) Definition chunk_eq: forall (c1 c2: memory_chunk), {c1=c2} + {c1<>c2}. Proof. decide equality. Defined. @@ -152,7 +151,6 @@ Definition type_of_chunk (c: memory_chunk) : typ := | Mint64 => Tlong | Mfloat32 => Tsingle | Mfloat64 => Tfloat - | Mfloat64al32 => Tfloat end. Definition type_of_chunk_use (c: memory_chunk) : typ := @@ -165,7 +163,6 @@ Definition type_of_chunk_use (c: memory_chunk) : typ := | Mint64 => Tlong | Mfloat32 => Tfloat | Mfloat64 => Tfloat - | Mfloat64al32 => Tfloat end. (** The chunk that is appropriate to store and reload a value of @@ -174,7 +171,7 @@ Definition type_of_chunk_use (c: memory_chunk) : typ := Definition chunk_of_type (ty: typ) := match ty with | Tint => Mint32 - | Tfloat => Mfloat64al32 + | Tfloat => Mfloat64 | Tlong => Mint64 | Tsingle => Mfloat32 end. diff --git a/common/Memdata.v b/common/Memdata.v index d8d347e..1b74705 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -39,7 +39,6 @@ Definition size_chunk (chunk: memory_chunk) : Z := | Mint64 => 8 | Mfloat32 => 4 | Mfloat64 => 8 - | Mfloat64al32 => 8 end. Lemma size_chunk_pos: @@ -86,8 +85,7 @@ Definition align_chunk (chunk: memory_chunk) : Z := | Mint32 => 4 | Mint64 => 8 | Mfloat32 => 4 - | Mfloat64 => 8 - | Mfloat64al32 => 4 + | Mfloat64 => 4 end. Lemma align_chunk_pos: @@ -343,7 +341,7 @@ Definition encode_val (chunk: memory_chunk) (v: val) : list memval := | Vptr b ofs, Mint32 => inj_pointer 4%nat b ofs | Vlong n, Mint64 => inj_bytes (encode_int 8%nat (Int64.unsigned n)) | Vfloat n, Mfloat32 => inj_bytes (encode_int 4%nat (Int.unsigned (Float.bits_of_single n))) - | Vfloat n, (Mfloat64 | Mfloat64al32) => inj_bytes (encode_int 8%nat (Int64.unsigned (Float.bits_of_double 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. @@ -358,7 +356,7 @@ Definition decode_val (chunk: memory_chunk) (vl: list memval) : val := | Mint32 => Vint(Int.repr(decode_int bl)) | Mint64 => Vlong(Int64.repr(decode_int bl)) | Mfloat32 => Vfloat(Float.single_of_bits (Int.repr (decode_int bl))) - | Mfloat64 | Mfloat64al32 => Vfloat(Float.double_of_bits (Int64.repr (decode_int bl))) + | Mfloat64 => Vfloat(Float.double_of_bits (Int64.repr (decode_int bl))) end | None => match chunk with @@ -397,19 +395,19 @@ Definition decode_encode_val (v1: val) (chunk1 chunk2: memory_chunk) (v2: val) : | Vint n, Mint16unsigned, Mint16unsigned => v2 = Vint(Int.zero_ext 16 n) | Vint n, Mint32, Mint32 => v2 = Vint n | Vint n, Mint32, Mfloat32 => v2 = Vfloat(Float.single_of_bits n) - | Vint n, (Mint64 | Mfloat32 | Mfloat64 | Mfloat64al32), _ => v2 = Vundef + | Vint n, (Mint64 | Mfloat32 | Mfloat64), _ => v2 = Vundef | Vint n, _, _ => True (**r nothing meaningful to say about v2 *) | Vptr b ofs, Mint32, Mint32 => v2 = Vptr b ofs | Vptr b ofs, _, _ => v2 = Vundef | Vlong n, Mint64, Mint64 => v2 = Vlong n - | Vlong n, Mint64, (Mfloat64 | Mfloat64al32) => v2 = Vfloat(Float.double_of_bits n) - | Vlong n, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mfloat64|Mfloat64al32), _ => v2 = Vundef + | Vlong n, Mint64, Mfloat64 => v2 = Vfloat(Float.double_of_bits n) + | Vlong n, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mfloat32|Mfloat64), _ => v2 = Vundef | Vlong n, _, _ => True (**r nothing meaningful to say about v2 *) | Vfloat f, Mfloat32, Mfloat32 => v2 = Vfloat(Float.singleoffloat f) | Vfloat f, Mfloat32, Mint32 => v2 = Vint(Float.bits_of_single f) - | Vfloat f, (Mfloat64 | Mfloat64al32), (Mfloat64 | Mfloat64al32) => v2 = Vfloat f + | Vfloat f, Mfloat64, Mfloat64 => v2 = Vfloat f | Vfloat f, (Mint8signed|Mint8unsigned|Mint16signed|Mint16unsigned|Mint32|Mint64), _ => v2 = Vundef - | Vfloat f, (Mfloat64 | Mfloat64al32), Mint64 => v2 = Vlong(Float.bits_of_double f) + | Vfloat f, Mfloat64, Mint64 => v2 = Vlong(Float.bits_of_double f) | Vfloat f, _, _ => True (* nothing interesting to say about v2 *) end. @@ -439,15 +437,10 @@ Opaque inj_pointer. rewrite decode_encode_int_4. auto. rewrite decode_encode_int_8. auto. rewrite decode_encode_int_8. auto. - rewrite decode_encode_int_8. 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. auto. rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double. - rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double. - rewrite decode_encode_int_8. auto. - rewrite decode_encode_int_8. decEq. apply Float.double_of_bits_of_double. - 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. diff --git a/common/Memory.v b/common/Memory.v index 0260a89..9afdfd3 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -727,6 +727,7 @@ Proof. rewrite pred_dec_false; auto. Qed. +(* Theorem load_float64al32: forall m b ofs v, load Mfloat64 m b ofs = Some v -> load Mfloat64al32 m b ofs = Some v. @@ -742,6 +743,7 @@ Theorem loadv_float64al32: Proof. unfold loadv; intros. destruct a; auto. apply load_float64al32; auto. Qed. +*) (** ** Properties related to [loadbytes] *) @@ -1411,6 +1413,7 @@ Proof. auto. Qed. +(* Theorem store_float64al32: forall m b ofs v m', store Mfloat64 m b ofs v = Some m' -> store Mfloat64al32 m b ofs v = Some m'. @@ -1428,6 +1431,7 @@ Theorem storev_float64al32: Proof. unfold storev; intros. destruct a; auto. apply store_float64al32; auto. Qed. +*) (** ** Properties related to [storebytes]. *) @@ -3422,7 +3426,7 @@ Proof. destruct H0. subst; exists Mint8unsigned; auto. destruct H0. subst; exists Mint16unsigned; auto. destruct H0. subst; exists Mint32; auto. - subst; exists Mfloat64; auto. + subst; exists Mint64; auto. destruct R as [chunk [A B]]. assert (valid_access m chunk b ofs Nonempty). split. red; intros; apply H3. omega. congruence. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index a3f6bcf..329c0c7 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -31,7 +31,6 @@ let name_of_chunk = function | Mint64 -> "int64" | Mfloat32 -> "float32" | Mfloat64 -> "float64" - | Mfloat64al32 -> "float64al32" let name_of_external = function | EF_external(name, sg) -> sprintf "extern %S" (extern_atom name) diff --git a/common/Values.v b/common/Values.v index 99a994b..5ac9f3e 100644 --- a/common/Values.v +++ b/common/Values.v @@ -682,7 +682,7 @@ Definition load_result (chunk: memory_chunk) (v: val) := | Mint32, Vptr b ofs => Vptr b ofs | Mint64, Vlong n => Vlong n | Mfloat32, Vfloat f => Vfloat(Float.singleoffloat f) - | (Mfloat64 | Mfloat64al32), Vfloat f => Vfloat f + | Mfloat64, Vfloat f => Vfloat f | _, _ => Vundef end. -- cgit v1.2.3