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, 16 insertions, 0 deletions

diff --git a/backend/Mach.v b/backend/Mach.v
index 2ec312e4..c6a692a1 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -27,6 +27,7 @@ Require Import Events.
 Require Import Globalenvs.
 Require Import Op.
 Require Import Locations.
+Require Import Conventions.
 
 (** * Abstract syntax *)
 
@@ -101,6 +102,21 @@ Definition regset := Regmap.t val.
 Notation "a ## b" := (List.map a b) (at level 1).
 Notation "a # b <- c" := (Regmap.set b c a) (at level 1, b at next level).
 
+Fixpoint undef_regs (rl: list mreg) (rs: regset) {struct rl} : regset :=
+  match rl with
+  | nil => rs
+  | r1 :: rl' => undef_regs rl' (Regmap.set r1 Vundef rs)
+  end.
+
+Definition undef_temps (rs: regset) := 
+  undef_regs (int_temporaries ++ float_temporaries) rs.
+
+Definition undef_op (op: operation) (rs: regset) :=
+  match op with
+  | Omove => rs
+  | _ => undef_temps rs
+  end.
+
 Definition is_label (lbl: label) (instr: instruction) : bool :=
   match instr with
   | Mlabel lbl' => if peq lbl lbl' then true else false