From 5909a0340ad0fe871dede1eaead855fb4b68fb0e Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 8 Aug 2011 06:31:10 +0000 Subject: 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 --- backend/Mach.v | 24 ++++++++++++++++++++++-- 1 file changed, 22 insertions(+), 2 deletions(-) (limited to 'backend/Mach.v') 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 -- cgit v1.2.3