IA32 port: more faithful treatment of pseudoregister ST0.

Related general change: support for destroyed_at_moves.


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

1 files changed, 22 insertions, 2 deletions

diff --git a/backend/Mach.v b/backend/Mach.v
index 3210a9e..5c9cff5 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -117,15 +117,35 @@ Fixpoint undef_regs (rl: list mreg) (rs: regset) {struct rl} : regset :=
   | r1 :: rl' => undef_regs rl' (Regmap.set r1 Vundef rs)
   end.
 
+Lemma undef_regs_other:
+  forall r rl rs, ~In r rl -> undef_regs rl rs r = rs r.
+Proof.
+  induction rl; simpl; intros. auto. rewrite IHrl. apply Regmap.gso. intuition. intuition.
+Qed.
+
+Lemma undef_regs_same:
+  forall r rl rs, In r rl \/ rs r = Vundef -> undef_regs rl rs r = Vundef.
+Proof.
+  induction rl; simpl; intros. tauto.
+  destruct H. destruct H. apply IHrl. right. subst; apply Regmap.gss.
+  auto.
+  apply IHrl. right. unfold Regmap.set. destruct (RegEq.eq r a); auto. 
+Qed.
+
 Definition undef_temps (rs: regset) := 
-  undef_regs (int_temporaries ++ float_temporaries) rs.
+  undef_regs temporary_regs rs.
+
+Definition undef_move (rs: regset) := 
+  undef_regs destroyed_at_move_regs rs.
 
 Definition undef_op (op: operation) (rs: regset) :=
   match op with
-  | Omove => rs
+  | Omove => undef_move rs
   | _ => undef_temps rs
   end.
 
+Definition undef_setstack (rs: regset) := undef_move rs.
+
 Definition is_label (lbl: label) (instr: instruction) : bool :=
   match instr with
   | Mlabel lbl' => if peq lbl lbl' then true else false