Merge of the reuse-temps branch:

- Reload temporaries are marked as destroyed (set to Vundef) across
  operations in the semantics of LTL, LTLin, Linear and Mach, 
  allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.



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

1 files changed, 22 insertions, 8 deletions

diff --git a/backend/Linear.v b/backend/Linear.v
index 0f44206d..40f7e416 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -163,6 +163,20 @@ Definition return_regs (caller callee: locset) : locset :=
     | S s => caller (S s)
     end.
 
+(** Temporaries destroyed across operations *)
+
+Definition undef_op (op: operation) (rs: locset) :=
+  match op with
+  | Omove => rs
+  | _ => undef_temps rs
+  end.
+
+Definition undef_getstack (s: slot) (rs: locset) :=
+  match s with
+  | Incoming _ _ => Locmap.set (R IT1) Vundef rs
+  | _ => rs
+  end.
+
 (** Linear execution states. *)
 
 Inductive stackframe: Type :=
@@ -241,7 +255,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Lgetstack:
       forall s f sp sl r b rs m,
       step (State s f sp (Lgetstack sl r :: b) rs m)
-        E0 (State s f sp b (Locmap.set (R r) (rs (S sl)) rs) m)
+        E0 (State s f sp b (Locmap.set (R r) (rs (S sl)) (undef_getstack sl rs)) m)
   | exec_Lsetstack:
       forall s f sp r sl b rs m,
       step (State s f sp (Lsetstack r sl :: b) rs m)
@@ -250,19 +264,19 @@ Inductive step: state -> trace -> state -> Prop :=
       forall s f sp op args res b rs m v,
       eval_operation ge sp op (reglist rs args) = Some v ->
       step (State s f sp (Lop op args res :: b) rs m)
-        E0 (State s f sp b (Locmap.set (R res) v rs) m)
+        E0 (State s f sp b (Locmap.set (R res) v (undef_op op rs)) m)
   | exec_Lload:
       forall s f sp chunk addr args dst b rs m a v,
       eval_addressing ge sp addr (reglist rs args) = Some a ->
       Mem.loadv chunk m a = Some v ->
       step (State s f sp (Lload chunk addr args dst :: b) rs m)
-        E0 (State s f sp b (Locmap.set (R dst) v rs) m)
+        E0 (State s f sp b (Locmap.set (R dst) v (undef_temps rs)) m)
   | exec_Lstore:
       forall s f sp chunk addr args src b rs m m' a,
       eval_addressing ge sp addr (reglist rs args) = Some a ->
       Mem.storev chunk m a (rs (R src)) = Some m' ->
       step (State s f sp (Lstore chunk addr args src :: b) rs m)
-        E0 (State s f sp b rs m')
+        E0 (State s f sp b (undef_temps rs) m')
   | exec_Lcall:
       forall s f sp sig ros b rs m f',
       find_function ros rs = Some f' ->
@@ -280,7 +294,7 @@ Inductive step: state -> trace -> state -> Prop :=
       forall s f sp rs m ef args res b t v m',
       external_call ef ge (reglist rs args) m t v m' ->
       step (State s f sp (Lbuiltin ef args res :: b) rs m)
-         t (State s f sp b (Locmap.set (R res) v rs) m')
+         t (State s f sp b (Locmap.set (R res) v (undef_temps rs)) m')
   | exec_Llabel:
       forall s f sp lbl b rs m,
       step (State s f sp (Llabel lbl :: b) rs m)
@@ -295,19 +309,19 @@ Inductive step: state -> trace -> state -> Prop :=
       eval_condition cond (reglist rs args) = Some true ->
       find_label lbl f.(fn_code) = Some b' ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
-        E0 (State s f sp b' rs m)
+        E0 (State s f sp b' (undef_temps rs) m)
   | exec_Lcond_false:
       forall s f sp cond args lbl b rs m,
       eval_condition cond (reglist rs args) = Some false ->
       step (State s f sp (Lcond cond args lbl :: b) rs m)
-        E0 (State s f sp b rs m)
+        E0 (State s f sp b (undef_temps rs) m)
   | exec_Ljumptable:
       forall s f sp arg tbl b rs m n lbl b',
       rs (R arg) = Vint n ->
       list_nth_z tbl (Int.signed n) = Some lbl ->
       find_label lbl f.(fn_code) = Some b' ->
       step (State s f sp (Ljumptable arg tbl :: b) rs m)
-        E0 (State s f sp b' rs m)
+        E0 (State s f sp b' (undef_temps rs) m)
   | exec_Lreturn:
       forall s f stk b rs m m',
       Mem.free m stk 0 f.(fn_stacksize) = Some m' ->