Revert commits r2435 and r2436 (coarser RTLtyping / finer Lineartyping):

the new Lineartyping can't keep track of single floats that were spilled.


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

1 files changed, 19 insertions, 5 deletions

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