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

7 files changed, 272 insertions, 142 deletions

diff --git a/backend/Linear.v b/backend/Linear.v
index 3553ced..b218531 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -169,8 +169,8 @@ Definition return_regs (caller callee: locset) : locset :=
 
 Definition undef_op (op: operation) (rs: locset) :=
   match op with
-  | Omove => rs
-  | _ => undef_temps rs
+  | Omove => Locmap.undef destroyed_at_move rs
+  | _ => Locmap.undef temporaries rs
   end.
 
 Definition undef_getstack (s: slot) (rs: locset) :=
@@ -179,6 +179,9 @@ Definition undef_getstack (s: slot) (rs: locset) :=
   | _ => rs
   end.
 
+Definition undef_setstack (rs: locset) :=
+  Locmap.undef destroyed_at_move rs.
+
 (** Linear execution states. *)
 
 Inductive stackframe: Type :=
@@ -261,7 +264,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Lsetstack:
       forall s f sp r sl b rs m,
       step (State s f sp (Lsetstack r sl :: b) rs m)
-        E0 (State s f sp b (Locmap.set (S sl) (rs (R r)) rs) m)
+        E0 (State s f sp b (Locmap.set (S sl) (rs (R r)) (undef_setstack rs)) m)
   | exec_Lop:
       forall s f sp op args res b rs m v,
       eval_operation ge sp op (reglist rs args) m = Some v ->
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index 390b630..3930da3 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -153,18 +153,23 @@ Proof.
   auto.
 Qed.
 
+Lemma wt_undef_locs:
+  forall locs ls, wt_locset ls -> wt_locset (Locmap.undef locs ls).
+Proof.
+  induction locs; simpl; intros. auto. apply IHlocs. apply wt_setloc; auto. red; auto.
+Qed.
+
 Lemma wt_undef_temps:
   forall ls, wt_locset ls -> wt_locset (undef_temps ls).
 Proof.
-  unfold undef_temps. generalize temporaries. induction l; simpl; intros.
-  auto.
-  apply IHl. apply wt_setloc; auto. red; auto.
+  intros; unfold undef_temps. apply wt_undef_locs; auto.
 Qed.
 
 Lemma wt_undef_op:
   forall op ls, wt_locset ls -> wt_locset (undef_op op ls).
 Proof.
-  intros. generalize (wt_undef_temps ls H); intro. case op; simpl; auto.
+  intros. generalize (wt_undef_temps ls H); intro. 
+  unfold undef_op; destruct op; auto; apply wt_undef_locs; auto.
 Qed.
 
 Lemma wt_undef_getstack:
@@ -173,6 +178,12 @@ Proof.
   intros. unfold undef_getstack. destruct s; auto. apply wt_setloc; auto. red; auto.
 Qed.
 
+Lemma wt_undef_setstack:
+  forall ls, wt_locset ls -> wt_locset (undef_setstack ls).
+Proof.
+  intros. unfold undef_setstack. apply wt_undef_locs; auto.
+Qed.
+
 Lemma wt_call_regs:
   forall ls, wt_locset ls -> wt_locset (call_regs ls).
 Proof.
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
diff --git a/backend/Machsem.v b/backend/Machsem.v
index 853e8a7..a802323 100644
--- a/backend/Machsem.v
+++ b/backend/Machsem.v
@@ -149,7 +149,7 @@ Inductive step: state -> trace -> state -> Prop :=
       forall s f sp src ofs ty c rs m m',
       store_stack m sp ty ofs (rs src) = Some m' ->
       step (State s f sp (Msetstack src ofs ty :: c) rs m)
-        E0 (State s f sp c rs m')
+        E0 (State s f sp c (undef_setstack rs) m')
   | exec_Mgetparam:
       forall s fb f sp ofs ty dst c rs m v,
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
diff --git a/backend/Parallelmove.v b/backend/Parallelmove.v
index 44eb399..d7a4217 100644
--- a/backend/Parallelmove.v
+++ b/backend/Parallelmove.v
@@ -238,11 +238,13 @@ Proof.
 Qed.
 
 Lemma source_not_temp1:
-  forall s, In s srcs \/ s = R IT2 \/ s = R FT2 -> Loc.diff s (R IT1) /\ Loc.diff s (R FT1).
+  forall s, In s srcs \/ s = R IT2 \/ s = R FT2 -> 
+  Loc.diff s (R IT1) /\ Loc.diff s (R FT1) /\ Loc.notin s destroyed_at_move.
 Proof.
-  intros. elim H; intro. 
-  split; apply NO_SRCS_TEMP; auto; simpl; tauto.
-  elim H0; intro; subst s; simpl; split; congruence.
+  intros. destruct H.
+  exploit Loc.disjoint_notin. eexact NO_SRCS_TEMP. eauto. 
+  simpl; tauto.
+  destruct H; subst s; simpl; intuition congruence.
 Qed.
 
 Lemma dest_noteq_diff:
@@ -265,16 +267,16 @@ Qed.
 
 Definition locmap_equiv (e1 e2: Locmap.t): Prop :=
   forall l,
-  no_overlap_dests l -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> e2 l = e1 l.
+  no_overlap_dests l -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> Loc.notin l destroyed_at_move -> e2 l = e1 l.
 
 (** The following predicates characterize the effect of one move
   move ([effect_move]) and of a sequence of elementary moves
   ([effect_seqmove]).  We allow the code generated for one move
-  to use the temporaries [IT1] and [FT1] in any way it needs. *)
+  to use the temporaries [IT1] and [FT1] and [destroyed_at_move] in any way it needs. *)
 
 Definition effect_move (src dst: loc) (e e': Locmap.t): Prop :=
   e' dst = e src /\
-  forall l, Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> e' l = e l.
+  forall l, Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> Loc.notin l destroyed_at_move -> e' l = e l.
 
 Inductive effect_seqmove: list (loc * loc) -> Locmap.t -> Locmap.t -> Prop :=
   | effect_seqmove_nil: forall e,
@@ -299,7 +301,7 @@ Lemma effect_move_equiv:
 Proof.
   intros. destruct H2. red; intros. 
   unfold Parmov.update. destruct (Loc.eq l d). 
-  subst l. elim (source_not_temp1 _ H); intros.
+  subst l. destruct (source_not_temp1 _ H) as [A [B C]]. 
   rewrite H2. apply H1; auto. apply source_no_overlap_dests; auto.
   rewrite H3; auto. apply dest_noteq_diff; auto. 
 Qed.
@@ -345,15 +347,16 @@ Proof.
   generalize (parmove_prop_1 srcs dsts LENGTH NOREPET NO_SRCS_TEMP NO_DSTS_TEMP e).
   fold mu. intros [A B]. 
   (* e' dsts = e srcs *)
-  split. rewrite <- A. apply list_map_exten; intros. 
+  split. rewrite <- A. apply list_map_exten; intros.
+  exploit Loc.disjoint_notin. eexact NO_DSTS_TEMP. eauto. simpl; intros.
   apply H1. apply dests_no_overlap_dests; auto.
-  apply NO_DSTS_TEMP; auto; simpl; tauto.
-  apply NO_DSTS_TEMP; auto; simpl; tauto.
+  tauto. tauto. simpl; tauto. 
   (* other locations *)
   intros. transitivity (exec_seq mu e l). 
   symmetry. apply H1. apply notin_dests_no_overlap_dests; auto.
   eapply Loc.in_notin_diff; eauto. simpl; tauto.
   eapply Loc.in_notin_diff; eauto. simpl; tauto.
+  simpl in H3; simpl; tauto.
   apply B. apply Loc.notin_not_in; auto.
   apply Loc.diff_not_eq. eapply Loc.in_notin_diff; eauto. simpl; tauto.
   apply Loc.diff_not_eq. eapply Loc.in_notin_diff; eauto. simpl; tauto.
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index f0a0b97..6ee9263 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -228,16 +228,17 @@ Lemma add_reload_correct:
   forall l, 
     Loc.diff (R dst) l -> 
     loc_acceptable src \/ Loc.diff (R IT1) l ->
+    Loc.notin l destroyed_at_move ->
     rs' l = rs l.
 Proof.
   intros. unfold add_reload. destruct src.
-  case (mreg_eq m0 dst); intro.
+  destruct (mreg_eq m0 dst).
   subst dst. exists rs. split. apply star_refl. tauto.
-  exists (Locmap.set (R dst) (rs (R m0)) rs).
-  split. apply star_one; apply exec_Lop. reflexivity. 
-  split. apply Locmap.gss. 
-  intros; apply Locmap.gso; auto.
-  exists (Locmap.set (R dst) (rs (S s)) (undef_getstack s rs)).
+  econstructor.
+  split. apply star_one; apply exec_Lop. simpl; reflexivity.
+  unfold undef_op. split. apply Locmap.gss. 
+  intros. rewrite Locmap.gso; auto; apply Locmap.guo; auto.
+  econstructor.
   split. apply star_one; apply exec_Lgetstack. 
   split. apply Locmap.gss.
   intros. rewrite Locmap.gso; auto. 
@@ -279,19 +280,31 @@ Lemma add_spill_correct:
   star step ge (State stk f sp (add_spill src dst k) rs m)
             E0 (State stk f sp k rs' m) /\
   rs' dst = rs (R src) /\
-  forall l, Loc.diff dst l -> rs' l = rs l.
+  forall l, Loc.diff dst l -> Loc.notin l destroyed_at_move -> rs' l = rs l.
 Proof.
   intros. unfold add_spill. destruct dst.
-  case (mreg_eq src m0); intro.
+  destruct (mreg_eq src m0).
   subst src. exists rs. split. apply star_refl. tauto.
-  exists (Locmap.set (R m0) (rs (R src)) rs).
-  split. apply star_one. apply exec_Lop. reflexivity.
+  econstructor.
+  split. apply star_one. apply exec_Lop. simpl; reflexivity.
   split. apply Locmap.gss.
-  intros; apply Locmap.gso; auto.
-  exists (Locmap.set (S s) (rs (R src)) rs).
+  intros. rewrite Locmap.gso; auto; unfold undef_op; apply Locmap.guo; auto. 
+  econstructor.
   split. apply star_one. apply exec_Lsetstack. 
   split. apply Locmap.gss.
-  intros; apply Locmap.gso; auto.
+  intros. rewrite Locmap.gso; auto; unfold undef_setstack; apply Locmap.guo; auto.
+Qed.
+
+Remark notin_destroyed_move_1:
+  forall r, ~In r destroyed_at_move_regs -> Loc.notin (R r) destroyed_at_move.
+Proof.
+  intros. simpl in *. intuition congruence.
+Qed.
+
+Remark notin_destroyed_move_2:
+  forall s, Loc.notin (S s) destroyed_at_move.
+Proof.
+  intros. simpl in *. destruct s; auto.
 Qed.
 
 Lemma add_reloads_correct_rec:
@@ -300,21 +313,26 @@ Lemma add_reloads_correct_rec:
   enough_temporaries_rec srcs itmps ftmps = true ->
   (forall r, In (R r) srcs -> In r itmps -> False) ->
   (forall r, In (R r) srcs -> In r ftmps -> False) ->
+  (forall r, In (R r) srcs -> ~In r destroyed_at_move_regs) ->
   list_disjoint itmps ftmps ->
   list_norepet itmps ->
   list_norepet ftmps ->
+  list_disjoint itmps destroyed_at_move_regs ->
+  list_disjoint ftmps destroyed_at_move_regs ->
   exists rs',
   star step ge 
       (State stk f sp (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m)
    E0 (State stk f sp k rs' m) /\
   reglist rs' (regs_for_rec srcs itmps ftmps) = map rs srcs /\
-  (forall r, ~(In r itmps) -> ~(In r ftmps) -> rs' (R r) = rs (R r)) /\
+  (forall r, ~(In r itmps) -> ~(In r ftmps) -> ~(In r destroyed_at_move_regs) -> rs' (R r) = rs (R r)) /\
   (forall s, rs' (S s) = rs (S s)).
 Proof.
+Opaque destroyed_at_move_regs.
   induction srcs; simpl; intros.
   (* base case *)
   exists rs. split. apply star_refl. tauto.
   (* inductive case *)
+  simpl in H0. 
   assert (ACC1: loc_acceptable a) by (auto with coqlib).
   assert (ACC2: locs_acceptable srcs) by (red; auto with coqlib).
   destruct a as [r | s].
@@ -323,41 +341,53 @@ Proof.
   exploit IHsrcs; eauto.
   intros [rs' [EX [RES [OTH1 OTH2]]]].
   exists rs'. split. eauto.
-  split. simpl. decEq. apply OTH1. red; intros; eauto. red; intros; eauto. auto.
+  split. simpl. decEq.
+    apply OTH1. red; intros; eauto. red; intros; eauto. auto.
+    auto.
   auto.
   (* a is a stack slot *)
   destruct (slot_type s).
   (* ... of integer type *)
-  destruct itmps as [ | it1 itmps ]. discriminate. inv H4.
+  destruct itmps as [ | it1 itmps ]. discriminate. inv H5.
   destruct (add_reload_correct (S s) it1 (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m)
   as [rs1 [A [B C]]].
-  exploit IHsrcs; eauto. 
-  intros. apply H1 with r. tauto. simpl. tauto. eapply list_disjoint_cons_left; eauto. 
+  exploit IHsrcs; eauto with coqlib.
+  eapply list_disjoint_cons_left; eauto.
+  eapply list_disjoint_cons_left; eauto. 
   intros [rs' [P [Q [T U]]]]. 
   exists rs'. split. eapply star_trans; eauto. 
-  split. simpl. decEq. rewrite <- B. apply T. auto.
-    eapply list_disjoint_notin; eauto with coqlib.
+  split. simpl. decEq. rewrite <- B. apply T.
+    auto.
+    eapply list_disjoint_notin. eexact H4. eauto with coqlib.
+    eapply list_disjoint_notin. eapply H7. auto with coqlib.
     rewrite Q. apply list_map_exten. intros. symmetry. apply C. 
     simpl. destruct x; auto. red; intro; subst m0. apply H1 with it1; auto with coqlib.
     auto.
+    destruct x. apply notin_destroyed_move_1. auto. apply notin_destroyed_move_2.
   split. simpl. intros. transitivity (rs1 (R r)).
-    apply T; tauto. apply C. simpl. tauto. auto. 
-  intros. transitivity (rs1 (S s0)). auto. apply C. simpl. auto. auto.
+    apply T; tauto. apply C. simpl. tauto. auto.
+    apply notin_destroyed_move_1; auto.
+  intros. transitivity (rs1 (S s0)). auto. apply C. simpl. auto. auto. apply notin_destroyed_move_2.
   (* ... of float type *)
-  destruct ftmps as [ | ft1 ftmps ]. discriminate. inv H5.
+  destruct ftmps as [ | ft1 ftmps ]. discriminate. inv H6.
   destruct (add_reload_correct (S s) ft1 (add_reloads srcs (regs_for_rec srcs itmps ftmps) k) rs m)
   as [rs1 [A [B C]]].
-  exploit IHsrcs; eauto. 
-  intros. apply H2 with r. tauto. simpl. tauto. eapply list_disjoint_cons_right; eauto. 
+  exploit IHsrcs; eauto with coqlib.
+  eapply list_disjoint_cons_right; eauto.
+  eapply list_disjoint_cons_left; eauto.
   intros [rs' [P [Q [T U]]]]. 
-  exists rs'. split. eapply star_trans; eauto. 
-  split. simpl. decEq. rewrite <- B. apply T; auto.
-    eapply list_disjoint_notin; eauto. apply list_disjoint_sym. eauto. auto with coqlib.
+  exists rs'. split. eapply star_trans; eauto.
+  split. simpl. decEq. rewrite <- B. apply T. 
+    eapply list_disjoint_notin; eauto. apply list_disjoint_sym. apply H4. auto with coqlib.
+    auto.
+    eapply list_disjoint_notin. eexact H8. auto with coqlib.
     rewrite Q. apply list_map_exten. intros. symmetry. apply C. 
     simpl. destruct x; auto. red; intro; subst m0. apply H2 with ft1; auto with coqlib. auto.
+    destruct x. apply notin_destroyed_move_1. auto. apply notin_destroyed_move_2.
   split. simpl. intros. transitivity (rs1 (R r)).
-    apply T; tauto. apply C. simpl. tauto. auto. 
-  intros. transitivity (rs1 (S s0)). auto. apply C. simpl. auto. auto.
+    apply T; tauto. apply C. simpl. tauto. auto.  
+    apply notin_destroyed_move_1; auto.
+  intros. transitivity (rs1 (S s0)). auto. apply C. simpl. auto. auto. apply notin_destroyed_move_2; auto.
 Qed.
 
 Lemma add_reloads_correct:
@@ -370,22 +400,26 @@ Lemma add_reloads_correct:
   reglist rs' (regs_for srcs) = List.map rs srcs /\
   forall l, Loc.notin l temporaries -> rs' l = rs l.
 Proof.
+Transparent destroyed_at_move_regs.
   intros.
   unfold enough_temporaries in H.
-  exploit add_reloads_correct_rec; eauto. 
-    intros. generalize (H0 _ H1). unfold loc_acceptable. generalize H2. 
+  exploit add_reloads_correct_rec. eauto. eauto. 
+    intros. generalize (H0 _ H1). unfold loc_acceptable. generalize H2.  
     simpl. intuition congruence. 
     intros. generalize (H0 _ H1). unfold loc_acceptable. generalize H2. 
     simpl. intuition congruence. 
-    red; intros r1 r2; simpl. intuition congruence.
+    intros. generalize (H0 _ H1). unfold loc_acceptable.
+    simpl. intuition congruence. 
+    red; simpl; intros. intuition congruence.
     unfold int_temporaries. NoRepet.
     unfold float_temporaries. NoRepet.
+    red; simpl; intros. intuition congruence.
+    red; simpl; intros. intuition congruence.
   intros [rs' [EX [RES [OTH1 OTH2]]]].
   exists rs'. split. eexact EX. 
   split. exact RES.
-  intros. destruct l. apply OTH1.
-  generalize (Loc.notin_not_in _ _ H1). simpl. intuition congruence.
-  generalize (Loc.notin_not_in _ _ H1). simpl. intuition congruence.
+  intros. destruct l. generalize (Loc.notin_not_in _ _ H1); simpl; intro.
+  apply OTH1; simpl; intuition congruence.
   apply OTH2.
 Qed.
 
@@ -395,19 +429,21 @@ Lemma add_move_correct:
   star step ge (State stk f sp (add_move src dst k) rs m)
             E0 (State stk f sp k rs' m) /\
   rs' dst = rs src /\
-  forall l, Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> rs' l = rs l.
+  forall l, 
+    Loc.diff l dst -> Loc.diff l (R IT1) -> Loc.diff l (R FT1) -> Loc.notin l destroyed_at_move ->
+    rs' l = rs l.
 Proof.
   intros; unfold add_move.
-  case (Loc.eq src dst); intro.
+  destruct (Loc.eq src dst).
   subst dst. exists rs. split. apply star_refl. tauto.
   destruct src.
   (* src is a register *)
   generalize (add_spill_correct m0 dst k rs m); intros [rs' [EX [RES OTH]]].
-  exists rs'; intuition. apply OTH; apply Loc.diff_sym; auto.
+  exists rs'; intuition. apply OTH. apply Loc.diff_sym; auto. auto.
   destruct dst.
   (* src is a stack slot, dst a register *)
   generalize (add_reload_correct (S s) m0 k rs m); intros [rs' [EX [RES OTH]]].
-  exists rs'; intuition. apply OTH. apply Loc.diff_sym; auto. right; apply Loc.diff_sym; auto.
+  exists rs'; intuition. apply OTH. apply Loc.diff_sym; auto. right; apply Loc.diff_sym; auto. auto.
   (* src and dst are stack slots *)
   set (tmp := match slot_type s with Tint => IT1 | Tfloat => FT1 end).
   generalize (add_reload_correct (S s) tmp (add_spill tmp (S s0) k) rs m);
@@ -419,8 +455,8 @@ Proof.
   split. congruence.
   intros. rewrite OTH2. apply OTH1. 
   apply Loc.diff_sym. unfold tmp; case (slot_type s); auto.
-  right. apply Loc.diff_sym; auto. 
-  apply Loc.diff_sym; auto.
+  right. apply Loc.diff_sym; auto. auto. 
+  apply Loc.diff_sym; auto. auto.
 Qed.
 
 Lemma effect_move_sequence:
@@ -440,7 +476,7 @@ Proof.
   destruct (add_move_correct src dst k1 rs m) as [rs1 [A [B C]]].
   destruct (IHmoves rs1 m) as [rs' [D E]].
   exists rs'; split. 
-  eapply star_trans; eauto. traceEq.
+  eapply star_trans; eauto.
   econstructor; eauto. red. tauto. 
 Qed.
 
@@ -566,7 +602,7 @@ Remark undef_op_others:
   Loc.notin l temporaries -> undef_op op rs l = rs l.
 Proof.
   intros. generalize (undef_temps_others rs l H); intro. 
-  destruct op; simpl; auto.
+  unfold undef_op; destruct op; auto; apply Locmap.guo; simpl in *; tauto.
 Qed.
 
 Lemma agree_undef_temps:
@@ -1006,7 +1042,7 @@ Proof.
   apply agree_set2 with ls; auto.
   rewrite B. simpl in H; inversion H. auto.
   intros. apply C. apply Loc.diff_sym; auto.
-  simpl in H7; tauto. simpl in H7; tauto.
+  simpl in H7; tauto. simpl in H7; tauto. simpl in *; tauto.
   (* other ops *)
   assert (is_move_operation op args = None).
     caseEq (is_move_operation op args); intros.
@@ -1032,7 +1068,7 @@ Proof.
   apply agree_set2 with ls; auto.
   rewrite E. rewrite Locmap.gss. auto.
   intros. rewrite F; auto. rewrite Locmap.gso. rewrite undef_op_others; auto. 
-  apply reg_for_diff; auto.
+  apply reg_for_diff; auto. simpl in *; tauto.
 
   (* Lload *)
   ExploitWT; inv WTI.
@@ -1056,7 +1092,7 @@ Proof.
   apply agree_set2 with ls; auto.
   rewrite E. rewrite Locmap.gss. auto.
   intros. rewrite F; auto. rewrite Locmap.gso. rewrite undef_temps_others; auto. 
-  apply reg_for_diff; auto.
+  apply reg_for_diff; auto. simpl in *; tauto.
 
   (* Lstore *)
   ExploitWT; inv WTI.
@@ -1212,10 +1248,12 @@ Proof.
                                  (map ls3 (loc_arguments sig))).
     replace (map ls3 (loc_arguments sig)) with (map ls2 (loc_arguments sig)).
     rewrite B. apply agree_locs; auto. 
-    apply list_map_exten; intros. apply F.
-    apply Loc.diff_sym.
-    apply (loc_arguments_not_temporaries sig x (R IT1)); simpl; auto.
+    apply list_map_exten; intros.
+    exploit Loc.disjoint_notin. apply loc_arguments_not_temporaries. eauto. simpl; intros.
+    apply F.
+    apply Loc.diff_sym; tauto.
     auto.
+    simpl; tauto.
   left; econstructor; split.
   eapply star_plus_trans. eexact A. eapply plus_right. eexact D. 
   eapply exec_Ltailcall; eauto.
@@ -1273,7 +1311,7 @@ Proof.
   apply agree_set with ls; auto.
   rewrite E. rewrite Locmap.gss. auto.
   intros. rewrite F; auto. rewrite Locmap.gso. rewrite undef_temps_others; auto. 
-  apply reg_for_diff; auto.
+  apply reg_for_diff; auto. simpl in *; tauto.
   (* no reload *)
   exploit external_call_mem_extends; eauto. 
   apply agree_locs; eauto. 
@@ -1401,6 +1439,7 @@ Proof.
   econstructor; eauto. 
   apply agree_set with ls; auto.
   rewrite B. auto.
+  intros. apply C; auto. simpl in *; tauto.
   unfold parent_locset in PRES.
   apply agree_postcall_2 with ls0; auto. 
 Qed.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index a2c8ecd..2ec14aa 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -673,17 +673,44 @@ Proof.
   rewrite Locmap.gso; auto. red. auto.
 Qed.
 
+Lemma agree_regs_exten:
+  forall j ls rs ls' rs',
+  agree_regs j ls rs ->
+  (forall r, ls' (R r) = Vundef \/ ls' (R r) = ls (R r) /\ rs' r = rs r) ->
+  agree_regs j ls' rs'.
+Proof.
+  intros; red; intros.
+  destruct (H0 r) as [A | [A B]]. 
+  rewrite A. constructor. 
+  rewrite A; rewrite B; auto.
+Qed.
+
+Lemma agree_regs_undef_list:
+  forall j rl ls rs,
+  agree_regs j ls rs ->
+  agree_regs j (Locmap.undef (List.map R rl) ls) (undef_regs rl rs).
+Proof.
+  induction rl; simpl; intros.
+  auto. 
+  apply IHrl. apply agree_regs_set_reg; auto. 
+Qed.
+
 Lemma agree_regs_undef_temps:
   forall j ls rs,
   agree_regs j ls rs ->
   agree_regs j (LTL.undef_temps ls) (undef_temps rs).
 Proof.
-  unfold LTL.undef_temps, undef_temps.
-  change temporaries with (List.map R (int_temporaries ++ float_temporaries)).
-  generalize (int_temporaries ++ float_temporaries).
-  induction l; simpl; intros.
-  auto. 
-  apply IHl. apply agree_regs_set_reg; auto. 
+  unfold LTL.undef_temps, undef_temps, temporaries.
+  intros; apply agree_regs_undef_list; auto.
+Qed.
+
+Lemma agree_regs_undef_setstack:
+  forall j ls rs,
+  agree_regs j ls rs ->
+  agree_regs j (Linear.undef_setstack ls) (undef_setstack rs).
+Proof.
+  intros. unfold Linear.undef_setstack, undef_setstack, destroyed_at_move.
+  apply agree_regs_undef_list; auto.
 Qed.
 
 Lemma agree_regs_undef_op:
@@ -691,9 +718,9 @@ Lemma agree_regs_undef_op:
   agree_regs j ls rs ->
   agree_regs j (Linear.undef_op op ls) (undef_op (transl_op fe op) rs).
 Proof.
-  intros.
-  generalize (agree_regs_undef_temps _ _ _ H). 
-  destruct op; simpl; auto.
+  intros. generalize (agree_regs_undef_temps _ _ _ H); intro A.
+Opaque destroyed_at_move_regs.
+  destruct op; auto; simpl; apply agree_regs_undef_setstack; auto.
 Qed.
 
 (** Preservation under assignment of stack slot *)
@@ -740,7 +767,7 @@ Lemma agree_frame_set_reg:
   forall j ls ls0 m sp m' sp' parent ra r v,
   agree_frame j ls ls0 m sp m' sp' parent ra ->
   mreg_within_bounds b r ->
-  Val.has_type v (Loc.type (R r)) ->
+   Val.has_type v (Loc.type (R r)) ->
   agree_frame j (Locmap.set (R r) v ls) ls0 m sp m' sp' parent ra.
 Proof.
   intros. inv H; constructor; auto; intros.
@@ -767,25 +794,36 @@ Proof.
   contradiction.
 Qed.
 
-Lemma agree_frame_undef_temps:
-  forall j ls ls0 m sp m' sp' parent ra,
+Lemma agree_frame_undef_locs:
+  forall j ls0 m sp m' sp' parent ra regs ls,
   agree_frame j ls ls0 m sp m' sp' parent ra ->
-  agree_frame j (LTL.undef_temps ls) ls0 m sp m' sp' parent ra.
+  incl (List.map R regs) temporaries ->
+  agree_frame j (Locmap.undef (List.map R regs) ls) ls0 m sp m' sp' parent ra.
 Proof.
-  intros until ra.
-  assert (forall regs ls,
-         incl (List.map R regs) temporaries ->
-         agree_frame j ls ls0 m sp m' sp' parent ra ->
-         agree_frame j (Locmap.undef (List.map R regs) ls) ls0 m sp m' sp' parent ra).
   induction regs; simpl; intros.
   auto.
   apply IHregs; eauto with coqlib.
   apply agree_frame_set_reg; auto. 
   apply temporary_within_bounds; eauto with coqlib.
   red; auto.
-  intros. unfold LTL.undef_temps.
-  change temporaries with (List.map R (int_temporaries ++ float_temporaries)).
-  apply H; auto. apply incl_refl. 
+Qed.
+
+Lemma agree_frame_undef_temps:
+  forall j ls ls0 m sp m' sp' parent ra,
+  agree_frame j ls ls0 m sp m' sp' parent ra ->
+  agree_frame j (LTL.undef_temps ls) ls0 m sp m' sp' parent ra.
+Proof.
+  intros. unfold temporaries. apply agree_frame_undef_locs; auto. apply incl_refl. 
+Qed.
+
+Lemma agree_frame_undef_setstack:
+  forall j ls ls0 m sp m' sp' parent ra,
+  agree_frame j ls ls0 m sp m' sp' parent ra ->
+  agree_frame j (Linear.undef_setstack ls) ls0 m sp m' sp' parent ra.
+Proof.
+  intros. unfold Linear.undef_setstack, destroyed_at_move. 
+  apply agree_frame_undef_locs; auto.
+  red; simpl; tauto.
 Qed.
 
 Lemma agree_frame_undef_op:
@@ -794,7 +832,8 @@ Lemma agree_frame_undef_op:
   agree_frame j (Linear.undef_op op ls) ls0 m sp m' sp' parent ra.
 Proof.
   intros. 
-  exploit agree_frame_undef_temps; eauto. destruct op; simpl; auto.
+  exploit agree_frame_undef_temps; eauto.
+  destruct op; simpl; auto; intros; apply agree_frame_undef_setstack; auto. 
 Qed.
 
 (** Preservation by assignment to local slot *)
@@ -1083,7 +1122,6 @@ Variable fb: block.
 Variable sp: block.
 Variable csregs: list mreg.
 Variable ls: locset.
-Variable rs: regset.
 
 Inductive stores_in_frame: mem -> mem -> Prop :=
   | stores_in_frame_refl: forall m,
@@ -1116,19 +1154,22 @@ Hypothesis mkindex_diff:
 Hypothesis csregs_typ:
   forall r, In r csregs -> mreg_type r = ty.
 
-Hypothesis agree: agree_regs j ls rs.
+Hypothesis ls_temp_undef:
+  forall r, In r destroyed_at_move_regs -> ls (R r) = Vundef.
+
 Hypothesis wt_ls: wt_locset ls.
 
 Lemma save_callee_save_regs_correct:
-  forall l k m,
+  forall l k rs m,
   incl l csregs ->
   list_norepet l ->
   frame_perm_freeable m sp ->
-  exists m',
+  agree_regs j ls rs ->
+  exists rs', exists m',
     star step tge 
        (State cs fb (Vptr sp Int.zero)
          (save_callee_save_regs bound number mkindex ty fe l k) rs m)
-    E0 (State cs fb (Vptr sp Int.zero) k rs m')
+    E0 (State cs fb (Vptr sp Int.zero) k rs' m')
   /\ (forall r,
        In r l -> number r < bound fe ->
        index_contains_inj j m' sp (mkindex (number r)) (ls (R r)))
@@ -1139,12 +1180,13 @@ Lemma save_callee_save_regs_correct:
        index_contains m sp idx v ->
        index_contains m' sp idx v)
   /\ stores_in_frame m m'
-  /\ frame_perm_freeable m' sp.
+  /\ frame_perm_freeable m' sp
+  /\ agree_regs j ls rs'.
 Proof.
   induction l; intros; simpl save_callee_save_regs.
   (* base case *)
-  exists m. split. apply star_refl. 
-  split. intros. elim H2.
+  exists rs; exists m. split. apply star_refl. 
+  split. intros. elim H3.
   split. auto.
   split. constructor.
   auto.
@@ -1156,20 +1198,24 @@ Proof.
   (* a store takes place *)
   exploit store_index_succeeds. apply (mkindex_valid a); auto with coqlib. 
   eauto. instantiate (1 := rs a). intros [m1 ST].
-  exploit (IHl k m1).  auto with coqlib. auto. 
+  exploit (IHl k (undef_setstack rs) m1).  auto with coqlib. auto. 
   red; eauto with mem.
-  intros [m' [A [B [C [D E]]]]].
-  exists m'. 
-  split. eapply star_left; eauto. constructor. 
+  apply agree_regs_exten with ls rs. auto.
+  intros. destruct (In_dec mreg_eq r destroyed_at_move_regs). 
+  left. apply ls_temp_undef; auto. 
+  right; split. auto. unfold undef_setstack, undef_move. apply undef_regs_other; auto.
+  intros [rs' [m' [A [B [C [D [E F]]]]]]].
+  exists rs'; exists m'. 
+  split. eapply star_left; eauto. econstructor. 
   rewrite <- (mkindex_typ (number a)). 
   apply store_stack_succeeds; auto with coqlib.
   traceEq.
   split; intros.
-  simpl in H2. destruct (mreg_eq a r). subst r.
+  simpl in H3. destruct (mreg_eq a r). subst r.
   assert (index_contains_inj j m1 sp (mkindex (number a)) (ls (R a))).
     eapply gss_index_contains_inj; eauto.
     rewrite mkindex_typ. rewrite <- (csregs_typ a). apply wt_ls. auto with coqlib.
-  destruct H4 as [v' [P Q]].
+  destruct H5 as [v' [P Q]].
   exists v'; split; auto. apply C; auto. 
   intros. apply mkindex_inj. apply number_inj; auto with coqlib. 
   inv H0. intuition congruence.
@@ -1182,44 +1228,49 @@ Proof.
   rewrite size_type_chunk. apply offset_of_index_disj_stack_data_2; eauto with coqlib.
   auto.
   (* no store takes place *)
-  exploit (IHl k m); auto with coqlib. 
-  intros [m' [A [B [C [D E]]]]].
-  exists m'; intuition. 
-  simpl in H2. destruct H2. subst r. omegaContradiction. apply B; auto.
+  exploit (IHl k rs m); auto with coqlib. 
+  intros [rs' [m' [A [B [C [D [E F]]]]]]].
+  exists rs'; exists m'; intuition. 
+  simpl in H3. destruct H3. subst r. omegaContradiction. apply B; auto.
   apply C; auto with coqlib.
-  intros. eapply H3; eauto. auto with coqlib.
+  intros. eapply H4; eauto. auto with coqlib.
 Qed.
 
 End SAVE_CALLEE_SAVE.
 
 Lemma save_callee_save_correct:
   forall j ls rs sp cs fb k m,
-  agree_regs j ls rs -> wt_locset ls ->
+  agree_regs j (call_regs ls) rs -> wt_locset (call_regs ls) ->
   frame_perm_freeable m sp ->
-  exists m',
+  exists rs', exists m',
     star step tge 
        (State cs fb (Vptr sp Int.zero) (save_callee_save fe k) rs m)
-    E0 (State cs fb (Vptr sp Int.zero) k rs m')
+    E0 (State cs fb (Vptr sp Int.zero) k rs' m')
   /\ (forall r,
        In r int_callee_save_regs -> index_int_callee_save r < b.(bound_int_callee_save) ->
-       index_contains_inj j m' sp (FI_saved_int (index_int_callee_save r)) (ls (R r)))
+       index_contains_inj j m' sp (FI_saved_int (index_int_callee_save r)) (call_regs ls (R r)))
   /\ (forall r,
        In r float_callee_save_regs -> index_float_callee_save r < b.(bound_float_callee_save) ->
-       index_contains_inj j m' sp (FI_saved_float (index_float_callee_save r)) (ls (R r)))
+       index_contains_inj j m' sp (FI_saved_float (index_float_callee_save r)) (call_regs ls (R r)))
   /\ (forall idx v,
        index_valid idx ->
        match idx with FI_saved_int _ => False | FI_saved_float _ => False | _ => True end ->
        index_contains m sp idx v ->
        index_contains m' sp idx v)
   /\ stores_in_frame sp m m'
-  /\ frame_perm_freeable m' sp.
+  /\ frame_perm_freeable m' sp
+  /\ agree_regs j (call_regs ls) rs'.
 Proof.
   intros.
+  assert (ls_temp_undef: forall r, In r destroyed_at_move_regs -> call_regs ls (R r) = Vundef).
+    intros; unfold call_regs. apply pred_dec_true.
+Transparent destroyed_at_move_regs.
+    simpl in *; intuition congruence.
   exploit (save_callee_save_regs_correct 
              fe_num_int_callee_save
              index_int_callee_save
              FI_saved_int Tint
-             j cs fb sp int_callee_save_regs ls rs).
+             j cs fb sp int_callee_save_regs (call_regs ls)).
   intros. apply index_int_callee_save_inj; auto. 
   intros. simpl. split. apply Zge_le. apply index_int_callee_save_pos; auto. assumption.
   auto.
@@ -1231,12 +1282,13 @@ Proof.
   apply incl_refl. 
   apply int_callee_save_norepet.
   eauto.
-  intros [m1 [A [B [C [D E]]]]].
+  eauto.
+  intros [rs1 [m1 [A [B [C [D [E F]]]]]]].
   exploit (save_callee_save_regs_correct 
              fe_num_float_callee_save
              index_float_callee_save
              FI_saved_float Tfloat
-             j cs fb sp float_callee_save_regs ls rs).
+             j cs fb sp float_callee_save_regs (call_regs ls)).
   intros. apply index_float_callee_save_inj; auto. 
   intros. simpl. split. apply Zge_le. apply index_float_callee_save_pos; auto. assumption.
   simpl; auto.
@@ -1248,8 +1300,9 @@ Proof.
   apply incl_refl. 
   apply float_callee_save_norepet.
   eexact E.
-  intros [m2 [P [Q [R [S T]]]]].
-  exists m2.
+  eexact F.
+  intros [rs2 [m2 [P [Q [R [S [T U]]]]]]].
+  exists rs2; exists m2.
   split. unfold save_callee_save, save_callee_save_int, save_callee_save_float.
   eapply star_trans; eauto. 
   split; intros.
@@ -1318,14 +1371,14 @@ Lemma function_prologue_correct:
   Mem.inject j m1 m1' ->
   Mem.alloc m1 0 f.(Linear.fn_stacksize) = (m2, sp) ->
   Val.has_type parent Tint -> Val.has_type ra Tint ->
-  exists j', exists m2', exists sp', exists m3', exists m4', exists m5',
+  exists j', exists rs', exists m2', exists sp', exists m3', exists m4', exists m5',
      Mem.alloc m1' 0 tf.(fn_stacksize) = (m2', sp')
   /\ store_stack m2' (Vptr sp' Int.zero) Tint tf.(fn_link_ofs) parent = Some m3'
   /\ store_stack m3' (Vptr sp' Int.zero) Tint tf.(fn_retaddr_ofs) ra = Some m4'
   /\ star step tge 
          (State cs fb (Vptr sp' Int.zero) (save_callee_save fe k) (undef_temps rs) m4')
-      E0 (State cs fb (Vptr sp' Int.zero) k (undef_temps rs) m5')
-  /\ agree_regs j' (call_regs ls) (undef_temps rs)
+      E0 (State cs fb (Vptr sp' Int.zero) k rs' m5')
+  /\ agree_regs j' (call_regs ls) rs'
   /\ agree_frame j' (call_regs ls) ls0 m2 sp m5' sp' parent ra
   /\ inject_incr j j'
   /\ inject_separated j j' m1 m1'
@@ -1368,11 +1421,10 @@ Proof.
   assert (PERM4: frame_perm_freeable m4' sp').
     red; intros. eauto with mem. 
   exploit save_callee_save_correct. 
-    apply agree_regs_undef_temps.
-    eapply agree_regs_inject_incr; eauto.
-    apply wt_undef_temps. auto.
+    apply agree_regs_call_regs. eapply agree_regs_inject_incr; eauto.
+    apply wt_call_regs. auto.
     eexact PERM4.
-  intros [m5' [STEPS [ICS [FCS [OTHERS [STORES PERM5]]]]]].
+  intros [rs' [m5' [STEPS [ICS [FCS [OTHERS [STORES [PERM5 AGREGS']]]]]]]].
   (* stores in frames *)
   assert (SIF: stores_in_frame sp' m2' m5').
     econstructor; eauto. 
@@ -1388,7 +1440,7 @@ Proof.
     assert (~Mem.valid_block m1' sp') by eauto with mem.
     contradiction.
   (* Conclusions *)
-  exists j'; exists m2'; exists sp'; exists m3'; exists m4'; exists m5'.
+  exists j'; exists rs'; exists m2'; exists sp'; exists m3'; exists m4'; exists m5'.
   split. auto.
   (* store parent *)
   split. change Tint with (type_of_index FI_link). 
@@ -1401,7 +1453,7 @@ Proof.
   (* saving of registers *)
   split. eexact STEPS.
   (* agree_regs *)
-  split. apply agree_regs_call_regs. apply agree_regs_inject_incr with j; auto.
+  split. auto.
   (* agree frame *)
   split. constructor; intros.
     (* unused regs *)
@@ -1423,15 +1475,15 @@ Proof.
     apply OTHERS; auto. red; auto.
     eapply gss_index_contains; eauto. red; auto.
     (* int callee save *)
-    rewrite <- AGCS. replace (ls (R r)) with (LTL.undef_temps ls (R r)).
+    rewrite <- AGCS. replace (ls (R r)) with (call_regs ls (R r)).
     apply ICS; auto.
-    unfold LTL.undef_temps. apply Locmap.guo. apply Loc.reg_notin. 
+    unfold call_regs. apply pred_dec_false.
     red; intros; exploit int_callee_save_not_destroyed; eauto. 
     auto.
     (* float callee save *)
-    rewrite <- AGCS. replace (ls (R r)) with (LTL.undef_temps ls (R r)).
+    rewrite <- AGCS. replace (ls (R r)) with (call_regs ls (R r)).
     apply FCS; auto.
-    unfold LTL.undef_temps. apply Locmap.guo. apply Loc.reg_notin. 
+    unfold call_regs. apply pred_dec_false.
     red; intros; exploit float_callee_save_not_destroyed; eauto. 
     auto.
     (* inj *)
@@ -2350,7 +2402,7 @@ Proof.
   econstructor; eauto with coqlib. econstructor; eauto.
   apply agree_regs_set_reg. apply agree_regs_set_reg. auto. auto. congruence. 
   eapply agree_frame_set_reg; eauto. eapply agree_frame_set_reg; eauto. 
-  apply temporary_within_bounds. unfold temporaries; auto with coqlib.
+  apply temporary_within_bounds. simpl; auto. 
   simpl; auto. simpl; rewrite <- H1. eapply agree_wt_ls; eauto.
   (* Lgetstack, outgoing *)
   exploit agree_outgoing; eauto. intros [v [A B]].
@@ -2389,11 +2441,13 @@ Proof.
     omega.
   apply match_stacks_change_mach_mem with m'; auto.
   eauto with mem. eauto with mem. intros. rewrite <- H4; eapply Mem.load_store_other; eauto. left; unfold block; omega.
-  apply agree_regs_set_slot; auto.
+  apply agree_regs_set_slot. apply agree_regs_undef_setstack; auto. 
   destruct sl.
-    eapply agree_frame_set_local; eauto. simpl in H1; rewrite H1; eapply agree_wt_ls; eauto.
+    eapply agree_frame_set_local. eapply agree_frame_undef_setstack; eauto. auto. auto.
+    simpl in H1; rewrite H1; eapply agree_wt_ls; eauto. auto.
     simpl in H3; contradiction.
-    eapply agree_frame_set_outgoing; eauto. simpl in H1; rewrite H1; eapply agree_wt_ls; eauto.
+    eapply agree_frame_set_outgoing. apply agree_frame_undef_setstack; eauto. auto. auto.
+    simpl in H1; rewrite H1; eapply agree_wt_ls; eauto. auto.
 
   (* Lop *)
   assert (Val.has_type v (mreg_type res)).
@@ -2611,7 +2665,7 @@ Proof.
   exploit function_prologue_correct; eauto.
   eapply match_stacks_type_sp; eauto. 
   eapply match_stacks_type_retaddr; eauto.
-  intros [j' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]].
+  intros [j' [rs' [m2' [sp' [m3' [m4' [m5' [A [B [C [D [E [F [G [J [K L]]]]]]]]]]]]]]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
   rewrite (unfold_transf_function _ _ TRANSL). unfold fn_code. unfold transl_body.