Merge of "newspilling" branch:

- Support single-precision floats as first-class values
- Introduce chunks Many32, Many64 and types Tany32, Tany64 to
  support saving and restoring registers without knowing
  the exact types (int/single/float) of their contents, just
  their sizes.
- Memory model: generalize the opaque encoding of pointers to
  apply to any value, not just pointers, if chunks Many32/Many64
  are selected.
- More properties of FP arithmetic proved.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 28 insertions, 0 deletions

diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v
index ec0dd2c..c7c7ab2 100644
--- a/backend/SelectLongproof.v
+++ b/backend/SelectLongproof.v
@@ -435,6 +435,34 @@ Proof.
   auto.
 Qed.
 
+Theorem eval_longofsingle:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.longofsingle x = Some y ->
+  exists v, eval_expr ge sp e m le (longofsingle hf a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold longofsingle.
+  destruct x; simpl in H0; inv H0. destruct (Float32.to_long f) as [n|] eqn:EQ; simpl in H2; inv H2.
+  exploit eval_floatofsingle; eauto. intros (v & A & B). simpl in B. inv B.
+  apply Float32.to_long_double in EQ. 
+  eapply eval_longoffloat; eauto. simpl.
+  change (Float.of_single f) with (Float32.to_double f); rewrite EQ; auto.
+Qed.
+
+Theorem eval_longuofsingle:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.longuofsingle x = Some y ->
+  exists v, eval_expr ge sp e m le (longuofsingle hf a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold longuofsingle.
+  destruct x; simpl in H0; inv H0. destruct (Float32.to_longu f) as [n|] eqn:EQ; simpl in H2; inv H2.
+  exploit eval_floatofsingle; eauto. intros (v & A & B). simpl in B. inv B.
+  apply Float32.to_longu_double in EQ. 
+  eapply eval_longuoffloat; eauto. simpl.
+  change (Float.of_single f) with (Float32.to_double f); rewrite EQ; auto.
+Qed.
+
 Theorem eval_singleoflong:
   forall le a x y,
   eval_expr ge sp e m le a x ->