From be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 19 May 2013 09:54:40 +0000
Subject: Merge of the float32 branch: - added RTL type "Tsingle" -
 ABI-compatible passing of single-precision floats on ARM and x86

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 common/Values.v | 45 ++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 38 insertions(+), 7 deletions(-)

(limited to 'common/Values.v')

diff --git a/common/Values.v b/common/Values.v
index 76fb2302..bb97cdc5 100644
--- a/common/Values.v
+++ b/common/Values.v
@@ -61,6 +61,7 @@ Definition has_type (v: val) (t: typ) : Prop :=
   | Vint _, Tint => True
   | Vlong _, Tlong => True
   | Vfloat _, Tfloat => True
+  | Vfloat f, Tsingle => Float.is_single f
   | Vptr _ _, Tint => True
   | _, _ => False
   end.
@@ -78,6 +79,23 @@ Definition has_opttype (v: val) (ot: option typ) : Prop :=
   | Some t => has_type v t
   end.
 
+Lemma has_subtype:
+  forall ty1 ty2 v,
+  subtype ty1 ty2 = true -> has_type v ty1 -> has_type v ty2.
+Proof.
+  intros. destruct ty1; destruct ty2; simpl in H; discriminate || assumption || idtac.
+  unfold has_type in *. destruct v; auto. 
+Qed.
+
+Lemma has_subtype_list:
+  forall tyl1 tyl2 vl,
+  subtype_list tyl1 tyl2 = true -> has_type_list vl tyl1 -> has_type_list vl tyl2.
+Proof.
+  induction tyl1; intros; destruct tyl2; try discriminate; destruct vl; try contradiction.
+  red; auto.
+  simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto.
+Qed.
+
 (** Truth values.  Pointers and non-zero integers are treated as [True].
   The integer 0 (also used to represent the null pointer) is [False].
   [Vundef] and floats are neither true nor false. *)
@@ -603,14 +621,14 @@ Definition cmplu (c: comparison) (v1 v2: val): option val :=
 
 End COMPARISONS.
 
-(** [load_result] is used in the memory model (library [Mem])
-  to post-process the results of a memory read.  For instance,
-  consider storing the integer value [0xFFF] on 1 byte at a
-  given address, and reading it back.  If it is read back with
+(** [load_result] reflects the effect of storing a value with a given
+  memory chunk, then reading it back with the same chunk.  Depending
+  on the chunk and the type of the value, some normalization occurs.
+  For instance, consider storing the integer value [0xFFF] on 1 byte
+  at a given address, and reading it back.  If it is read back with
   chunk [Mint8unsigned], zero-extension must be performed, resulting
-  in [0xFF].  If it is read back as a [Mint8signed], sign-extension
-  is performed and [0xFFFFFFFF] is returned.   Type mismatches
-  (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *)
+  in [0xFF].  If it is read back as a [Mint8signed], sign-extension is
+  performed and [0xFFFFFFFF] is returned. *)
 
 Definition load_result (chunk: memory_chunk) (v: val) :=
   match chunk, v with
@@ -626,6 +644,19 @@ Definition load_result (chunk: memory_chunk) (v: val) :=
   | _, _ => Vundef
   end.
 
+Lemma load_result_type:
+  forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk).
+Proof.
+  intros. destruct chunk; destruct v; simpl; auto. apply Float.singleoffloat_is_single.
+Qed.
+
+Lemma load_result_same:
+  forall v ty, has_type v ty -> load_result (chunk_of_type ty) v = v.
+Proof.
+  unfold has_type; intros. destruct v; destruct ty; try contradiction; auto.
+  simpl. rewrite Float.singleoffloat_of_single; auto. 
+Qed.
+
 (** Theorems on arithmetic operations. *)
 
 Theorem cast8unsigned_and:
-- 
cgit