Revised division of labor between RTLtyping and Lineartyping:

- RTLtyping no longer keeps track of single-precision floats,
  switches from subtype-based inference to unification-based inference.
- Unityping: new library for unification-based inference.
- Locations: don't normalize at assignment in a stack slot
- Allocation, Allocproof: simplify accordingly.
- Lineartyping: add inference of machine registers that contain
  a single-precision float.
- Stackingproof: adapted accordingly.

This addresses a defect report by D. Dickman whereas RTLtyping was rejecting code that used a RTL pseudoreg to hold both double- and single-precision floats.



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

1 files changed, 5 insertions, 19 deletions

diff --git a/backend/Locations.v b/backend/Locations.v
index 43ce210..96f1eba 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -301,29 +301,16 @@ Module Locmap.
 
   Definition set (l: loc) (v: val) (m: t) : t :=
     fun (p: loc) =>
-      if Loc.eq l p then
-        match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end
-      else if Loc.diff_dec l p then
-        m p
+      if Loc.eq l p then v
+      else if Loc.diff_dec l p then m p
       else Vundef.
 
   Lemma gss: forall l v m,
-    (set l v m) l = 
-    match l with R r => v | S sl ofs ty => Val.load_result (chunk_of_type ty) v end.
+    (set l v m) l = v.
   Proof.
     intros. unfold set. apply dec_eq_true.
   Qed.
 
-  Lemma gss_reg: forall r v m, (set (R r) v m) (R r) = v.
-  Proof.
-    intros. unfold set. rewrite dec_eq_true. auto.
-  Qed.
-
-  Lemma gss_typed: forall l v m, Val.has_type v (Loc.type l) -> (set l v m) l = v.
-  Proof.
-    intros. rewrite gss. destruct l. auto. apply Val.load_result_same; auto. 
-  Qed.
-
   Lemma gso: forall l v m p, Loc.diff l p -> (set l v m) p = m p.
   Proof.
     intros. unfold set. destruct (Loc.eq l p).
@@ -349,11 +336,10 @@ Module Locmap.
   Proof.
     assert (P: forall ll l m, m l = Vundef -> (undef ll m) l = Vundef).
       induction ll; simpl; intros. auto. apply IHll. 
-      unfold set. destruct (Loc.eq a l).
-      destruct a. auto. destruct ty; reflexivity. 
+      unfold set. destruct (Loc.eq a l). auto.
       destruct (Loc.diff_dec a l); auto.
     induction ll; simpl; intros. contradiction. 
-    destruct H. apply P. subst a. apply gss_typed. exact I. 
+    destruct H. apply P. subst a. apply gss.  
     auto.
   Qed.