Merge tag 'v3.4' into mppa_k1c

Conflicts:
	.gitignore

12 files changed, 245 insertions, 90 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 585fb0da..1804f46b 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -1317,15 +1317,6 @@ Proof.
   eauto.
 Qed.
 
-Definition callee_save_loc (l: loc) :=
-  match l with
-  | R r => is_callee_save r = true
-  | S sl ofs ty => sl <> Outgoing
-  end.
-
-Definition agree_callee_save (ls1 ls2: locset) : Prop :=
-  forall l, callee_save_loc l -> ls1 l = ls2 l.
-
 Lemma return_regs_agree_callee_save:
   forall caller callee,
   agree_callee_save caller (return_regs caller callee).
@@ -2476,10 +2467,10 @@ Proof.
   rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss.
   rewrite val_longofwords_eq_1 by auto. auto.
   red; intros. rewrite (AG l H0).
-  symmetry; apply Locmap.gpo.
-  assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)).
-  { intros. destruct l; simpl in *. congruence. auto. }
-  generalize (loc_result_caller_save (ef_sig ef)). destruct (loc_result (ef_sig ef)); simpl; intuition auto.
+  rewrite locmap_get_set_loc_result_callee_save by auto.
+  unfold undef_caller_save_regs. destruct l; simpl in H0.
+  rewrite H0; auto.
+  destruct sl; auto; congruence.
   eapply external_call_well_typed; eauto.
 
 (* return *)
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 62c4a702..0f666a65 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -97,6 +97,16 @@ let translate_annot sp preg_to_dwarf annot =
   | [] -> None
   | a::_ -> aux a)
 
+let builtin_nop =
+  let signature ={sig_args = []; sig_res = None; sig_cc = cc_default} in
+  let name = coqstring_of_camlstring "__builtin_nop" in
+  Pbuiltin(EF_builtin(name,signature),[],BR_none)
+
+let rec lbl_follows = function
+  | Pbuiltin (EF_debug _, _, _):: rest ->
+    lbl_follows rest
+  | Plabel _ :: _ -> true
+  | _ -> false
 
 let expand_debug id sp preg simple l =
   let get_lbl = function
@@ -144,6 +154,11 @@ let expand_debug id sp preg simple l =
           | _ ->
               aux None scopes rest
         end
+    | (Pbuiltin(EF_annot (kind, _, _),_,_) as annot)::rest ->
+      simple annot;
+      if P.to_int kind = 2 && lbl_follows rest then
+        simple builtin_nop;
+      aux None scopes rest
     | (Plabel lbl)::rest -> simple (Plabel lbl); aux (Some lbl) scopes rest
     | i::rest -> simple i; aux None scopes rest in
   (* We need to move all closing debug annotations before the last real statement *)
@@ -157,3 +172,20 @@ let expand_debug id sp preg simple l =
     | b::rest -> List.rev ((List.rev (b::bcc)@List.rev acc)@rest) (* We found the first non debug location *)
     | [] -> List.rev acc (* This actually can never happen *) in
   aux None [] (move_debug [] [] (List.rev l))
+
+let expand_simple simple l =
+  let rec aux = function
+   | (Pbuiltin(EF_annot (kind, _, _),_,_) as annot)::rest ->
+     simple annot;
+     if P.to_int kind = 2 && lbl_follows rest then
+       simple builtin_nop;
+     aux rest
+   | i::rest -> simple i; aux rest
+   | [] -> () in
+  aux l
+
+let expand id sp preg simple l =
+  if !Clflags.option_g then
+    expand_debug id sp preg simple l
+  else
+    expand_simple simple l
diff --git a/backend/Asmexpandaux.mli b/backend/Asmexpandaux.mli
index 797eb10c..d80b4aec 100644
--- a/backend/Asmexpandaux.mli
+++ b/backend/Asmexpandaux.mli
@@ -31,6 +31,6 @@ val set_current_function: coq_function -> unit
   (* Set the current function *)
 val get_current_function: unit -> coq_function
   (* Get the current function *)
-val expand_debug: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit
-  (* Expand builtin debug function. Takes the function id, the register number of the stackpointer, a
-     function to get the dwarf mapping of varibale names  and for the expansion of simple instructions *)
+val expand: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit
+  (* Expand the instruction sequence of a function. Takes the function id, the register number of the stackpointer, a
+     function to get the dwarf mapping of varibale names and for the expansion of simple instructions *)
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index 8dfa8828..3e25c79b 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -318,6 +318,23 @@ Proof.
   intros. rewrite Pregmap.gso; auto.
 Qed.
 
+Lemma agree_undef_caller_save_regs:
+  forall ms sp rs,
+  agree ms sp rs ->
+  agree (Mach.undef_caller_save_regs ms) sp (Asm.undef_caller_save_regs rs).
+Proof.
+  intros. destruct H. unfold Mach.undef_caller_save_regs, Asm.undef_caller_save_regs; split.
+- unfold proj_sumbool; rewrite dec_eq_true. auto.
+- auto.
+- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). 
+  destruct (in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl.
++ apply list_in_map_inv in i. destruct i as (mr & A & B). 
+  assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A.
+  apply List.filter_In in B. destruct B as [C D]. rewrite D. auto.
++ destruct (is_callee_save r) eqn:CS; auto.
+  elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. 
+Qed.
+
 Lemma agree_change_sp:
   forall ms sp rs sp',
   agree ms sp rs -> sp' <> Vundef ->
diff --git a/backend/Conventions.v b/backend/Conventions.v
index bdc4c8b6..989bfa05 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -103,3 +103,56 @@ Proof.
   generalize (loc_arguments_bounded _ _ _ H0).
   generalize (typesize_pos ty). omega.
 Qed.
+
+
+(** * Callee-save locations *)
+
+(** We classify locations as either
+- callee-save, i.e. preserved across function calls:
+  callee-save registers, [Local] and [Incoming] stack slots;
+- caller-save, i.e. possibly modified by a function call:
+  non-callee-save registers, [Outgoing] stack slots.
+
+Concerning [Outgoing] stack slots: several ABIs allow a function to modify
+the stack slots used for passing parameters to this function.
+The code currently generated by CompCert never does so, but the code
+generated by other compilers often does so (e.g. GCC for x86-32).
+Hence, CompCert-generated code must not assume that [Outgoing] stack slots
+are preserved across function calls, because they might not be preserved
+if the called function was compiled by another compiler. 
+*)
+
+Definition callee_save_loc (l: loc) :=
+  match l with
+  | R r => is_callee_save r = true
+  | S sl ofs ty => sl <> Outgoing
+  end.
+
+Hint Unfold callee_save_loc.
+
+Definition agree_callee_save (ls1 ls2: Locmap.t) : Prop :=
+  forall l, callee_save_loc l -> ls1 l = ls2 l.
+
+(** * Assigning result locations *)
+
+(** Useful lemmas to reason about the result of an external call. *)
+
+Lemma locmap_get_set_loc_result:
+  forall sg v rs l,
+  match l with R r => is_callee_save r = true | S _ _ _ => True end ->
+  Locmap.setpair (loc_result sg) v rs l = rs l.
+Proof.
+  intros. apply Locmap.gpo. 
+  assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)).
+  { intros. destruct l; simpl. congruence. auto. }
+  generalize (loc_result_caller_save sg). destruct (loc_result sg); simpl; intuition auto.
+Qed.
+
+Lemma locmap_get_set_loc_result_callee_save:
+  forall sg v rs l,
+  callee_save_loc l ->
+  Locmap.setpair (loc_result sg) v rs l = rs l.
+Proof.
+  intros. apply locmap_get_set_loc_result. 
+  red in H; destruct l; auto.
+Qed.
diff --git a/backend/LTL.v b/backend/LTL.v
index 8567a891..5e7eec8c 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -96,16 +96,31 @@ Definition call_regs (caller: locset) : locset :=
 - Callee-save machine registers have the same values as in the caller
   before the call.
 - Caller-save machine registers have the same values as in the callee.
-- Stack slots have the same values as in the caller.
+- Local and Incoming stack slots have the same values as in the caller.
+- Outgoing stack slots are set to Vundef to  reflect the fact that they
+  may have been changed by the callee.
 *)
 
 Definition return_regs (caller callee: locset) : locset :=
   fun (l: loc) =>
     match l with
     | R r => if is_callee_save r then caller (R r) else callee (R r)
+    | S Outgoing ofs ty => Vundef
     | S sl ofs ty => caller (S sl ofs ty)
     end.
 
+(** [undef_caller_save_regs ls] models the effect of calling
+    an external function: caller-save registers and outgoing locations
+    can change unpredictably, hence we set them to [Vundef]. *)
+
+Definition undef_caller_save_regs (ls: locset) : locset :=
+  fun (l: loc) =>
+    match l with
+    | R r => if is_callee_save r then ls (R r) else Vundef
+    | S Outgoing ofs ty => Vundef
+    | S sl ofs ty => ls (S sl ofs ty)
+    end.
+
 (** LTL execution states. *)
 
 Inductive stackframe : Type :=
@@ -259,7 +274,7 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_function_external: forall s ef t args res rs m rs' m',
       args = map (fun p => Locmap.getpair p rs) (loc_arguments (ef_sig ef)) ->
       external_call ef ge args m t res m' ->
-      rs' = Locmap.setpair (loc_result (ef_sig ef)) res rs ->
+      rs' = Locmap.setpair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) ->
       step (Callstate s (External ef) rs m)
          t (Returnstate s rs' m')
   | exec_return: forall f sp rs1 bb s rs m,
diff --git a/backend/Linear.v b/backend/Linear.v
index 55f92d16..447c6ba6 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -239,7 +239,7 @@ Inductive step: state -> trace -> state -> Prop :=
       forall s ef args res rs1 rs2 m t m',
       args = map (fun p => Locmap.getpair p rs1) (loc_arguments (ef_sig ef)) ->
       external_call ef ge args m t res m' ->
-      rs2 = Locmap.setpair (loc_result (ef_sig ef)) res rs1 ->
+      rs2 = Locmap.setpair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs1) ->
       step (Callstate s (External ef) rs1 m)
          t (Returnstate s rs2 m')
   | exec_return:
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index d5fadd4c..55d86448 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -146,7 +146,18 @@ Lemma wt_return_regs:
   wt_locset caller -> wt_locset callee -> wt_locset (return_regs caller callee).
 Proof.
   intros; red; intros.
-  unfold return_regs. destruct l; auto. destruct (is_callee_save r); auto.
+  unfold return_regs. destruct l.
+- destruct (is_callee_save r); auto.
+- destruct sl; auto; red; auto.
+Qed.
+
+Lemma wt_undef_caller_save_regs:
+  forall ls, wt_locset ls -> wt_locset (undef_caller_save_regs ls).
+Proof.
+  intros; red; intros. unfold undef_caller_save_regs.
+  destruct l.
+  destruct (is_callee_save r); auto; simpl; auto.
+  destruct sl; auto; red; auto. 
 Qed.
 
 Lemma wt_init:
@@ -197,6 +208,24 @@ Proof.
   auto.
 Qed.
 
+(** In addition to type preservation during evaluation, we also show
+  properties of the environment [ls] at call points and at return points.
+  These properties are used in the proof of the [Stacking] pass.
+  For call points, we have that the current environment [ls] and the
+  one from the top call stack agree on the [Outgoing] locations
+  used for parameter passing. *)
+
+Definition agree_outgoing_arguments (sg: signature) (ls pls: locset) : Prop :=
+  forall ty ofs,
+  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments sg)) ->
+  ls (S Outgoing ofs ty) = pls (S Outgoing ofs ty).
+
+(** For return points, we have that all [Outgoing] stack locations have
+  been set to [Vundef]. *)
+
+Definition outgoing_undef (ls: locset) : Prop :=
+  forall ty ofs, ls (S Outgoing ofs ty) = Vundef.
+
 (** Soundness of the type system *)
 
 Definition wt_fundef (fd: fundef) :=
@@ -233,11 +262,15 @@ Inductive wt_state: state -> Prop :=
   | wt_call_state: forall s fd rs m
         (WTSTK: wt_callstack s)
         (WTFD: wt_fundef fd)
-        (WTRS: wt_locset rs),
+        (WTRS: wt_locset rs)
+        (AGCS: agree_callee_save rs (parent_locset s))
+        (AGARGS: agree_outgoing_arguments (funsig fd) rs (parent_locset s)),
       wt_state (Callstate s fd rs m)
   | wt_return_state: forall s rs m
         (WTSTK: wt_callstack s)
-        (WTRS: wt_locset rs),
+        (WTRS: wt_locset rs)
+        (AGCS: agree_callee_save rs (parent_locset s))
+        (UOUT: outgoing_undef rs),
       wt_state (Returnstate s rs m).
 
 (** Preservation of state typing by transitions *)
@@ -307,11 +340,15 @@ Local Opaque mreg_type.
   simpl in *; InvBooleans.
   econstructor; eauto. econstructor; eauto.
   eapply wt_find_function; eauto.
+  red; simpl; auto.
+  red; simpl; auto.
 - (* tailcall *)
   simpl in *; InvBooleans.
   econstructor; eauto.
   eapply wt_find_function; eauto.
   apply wt_return_regs; auto. apply wt_parent_locset; auto.
+  red; simpl; intros. destruct l; simpl in *. rewrite H3; auto. destruct sl; auto; congruence.
+  red; simpl; intros. apply zero_size_arguments_tailcall_possible in H. apply H in H3. contradiction.
 - (* builtin *)
   simpl in *; InvBooleans.
   econstructor; eauto.
@@ -334,13 +371,20 @@ Local Opaque mreg_type.
   simpl in *. InvBooleans.
   econstructor; eauto.
   apply wt_return_regs; auto. apply wt_parent_locset; auto.
+  red; simpl; intros. destruct l; simpl in *. rewrite H0; auto. destruct sl; auto; congruence.
+  red; simpl; intros. auto.
 - (* internal function *)
   simpl in WTFD.
   econstructor. eauto. eauto. eauto.
   apply wt_undef_regs. apply wt_call_regs. auto.
 - (* external function *)
-  econstructor. auto. apply wt_setpair; auto.
+  econstructor. auto. apply wt_setpair. 
   eapply external_call_well_typed; eauto.
+  apply wt_undef_caller_save_regs; auto.
+  red; simpl; intros. destruct l; simpl in *.
+  rewrite locmap_get_set_loc_result by auto. simpl. rewrite H; auto. 
+  rewrite locmap_get_set_loc_result by auto. simpl. destruct sl; auto; congruence.
+  red; simpl; intros. rewrite locmap_get_set_loc_result by auto. auto.
 - (* return *)
   inv WTSTK. econstructor; eauto.
 Qed.
@@ -352,6 +396,8 @@ Proof.
   unfold ge0 in H1. exploit Genv.find_funct_ptr_inversion; eauto.
   intros [id IN]. eapply wt_prog; eauto.
   apply wt_init.
+  red; auto.
+  red; auto.
 Qed.
 
 End SOUNDNESS.
@@ -397,3 +443,19 @@ Lemma wt_callstate_wt_regs:
 Proof.
   intros. inv H. apply WTRS.
 Qed.
+
+Lemma wt_callstate_agree:
+  forall s f rs m,
+  wt_state (Callstate s f rs m) ->
+  agree_callee_save rs (parent_locset s) /\ agree_outgoing_arguments (funsig f) rs (parent_locset s).
+Proof.
+  intros. inv H; auto.
+Qed.
+
+Lemma wt_returnstate_agree:
+  forall s rs m,
+  wt_state (Returnstate s rs m) ->
+  agree_callee_save rs (parent_locset s) /\ outgoing_undef rs.
+Proof.
+  intros. inv H; auto.
+Qed.
diff --git a/backend/Mach.v b/backend/Mach.v
index 839a25bd..9fdee9eb 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -156,6 +156,9 @@ Proof.
   unfold Regmap.set. destruct (RegEq.eq r a); auto.
 Qed.
 
+Definition undef_caller_save_regs (rs: regset) : regset :=
+  fun r => if is_callee_save r then rs r else Vundef.
+
 Definition set_pair (p: rpair mreg) (v: val) (rs: regset) : regset :=
   match p with
   | One r => rs#r <- v
@@ -407,7 +410,7 @@ Inductive step: state -> trace -> state -> Prop :=
       Genv.find_funct_ptr ge fb = Some (External ef) ->
       extcall_arguments rs m (parent_sp s) (ef_sig ef) args ->
       external_call ef ge args m t res m' ->
-      rs' = set_pair (loc_result (ef_sig ef)) res rs ->
+      rs' = set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) ->
       step (Callstate s fb rs m)
          t (Returnstate s rs' m')
   | exec_return:
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index d4d7362d..19aba4f6 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -644,7 +644,7 @@ let add_interfs_instr g instr live =
       (* Reloads from incoming slots can occur when some 64-bit
          parameters are split and passed as two 32-bit stack locations. *)
       begin match src with
-      | L(Locations.S(Incoming, _, _)) -> 
+      | L(Locations.S(Incoming, _, _)) ->
           add_interfs_def g (vmreg temp_for_parent_frame) live
       | _ -> ()
       end
@@ -1210,9 +1210,9 @@ let regalloc f =
         Errors.OK(first_round f3 liveness)
       with
       | Timeout ->
-          Errors.Error(Errors.msg (coqstring_of_camlstring "Spilling fails to converge"))
+          Errors.Error(Errors.msg (coqstring_of_camlstring "spilling fails to converge"))
       | Type_error_at pc ->
-          Errors.Error [Errors.MSG(coqstring_of_camlstring "Ill-typed XTL code at PC ");
+          Errors.Error [Errors.MSG(coqstring_of_camlstring "ill-typed XTL code at PC ");
                  Errors.POS pc]
       | Bad_LTL ->
-          Errors.Error(Errors.msg (coqstring_of_camlstring "Bad LTL after spilling"))
+          Errors.Error(Errors.msg (coqstring_of_camlstring "bad LTL after spilling"))
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 6d46d04d..c9b07427 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -294,12 +294,13 @@ Qed.
 
 Lemma contains_locations_exten:
   forall ls ls' j sp pos bound sl,
-  (forall ofs ty, ls' (S sl ofs ty) = ls (S sl ofs ty)) ->
+  (forall ofs ty, Val.lessdef (ls' (S sl ofs ty)) (ls (S sl ofs ty))) ->
   massert_imp (contains_locations j sp pos bound sl ls)
               (contains_locations j sp pos bound sl ls').
 Proof.
   intros; split; simpl; intros; auto.
-  intuition auto. rewrite H. eauto.
+  intuition auto. exploit H5; eauto. intros (v & A & B). exists v; split; auto. 
+  specialize (H ofs ty). inv H. congruence. auto. 
 Qed.
 
 Lemma contains_locations_incr:
@@ -481,7 +482,8 @@ Qed.
 
 Lemma frame_contents_exten:
   forall ls ls0 ls' ls0' j sp parent retaddr P m,
-  (forall sl ofs ty, ls' (S sl ofs ty) = ls (S sl ofs ty)) ->
+  (forall ofs ty, Val.lessdef (ls' (S Local ofs ty)) (ls (S Local ofs ty))) ->
+  (forall ofs ty, Val.lessdef (ls' (S Outgoing ofs ty)) (ls (S Outgoing ofs ty))) ->
   (forall r, In r b.(used_callee_save) -> ls0' (R r) = ls0 (R r)) ->
   m |= frame_contents j sp ls ls0 parent retaddr ** P ->
   m |= frame_contents j sp ls' ls0' parent retaddr ** P.
@@ -573,16 +575,6 @@ Record agree_locs (ls ls0: locset) : Prop :=
        ls (S Incoming ofs ty) = ls0 (S Outgoing ofs ty)
 }.
 
-(** Auxiliary predicate used at call points *)
-
-Definition agree_callee_save (ls ls0: locset) : Prop :=
-  forall l,
-  match l with
-  | R r => is_callee_save r = true
-  | S _ _ _ => True
-  end ->
-  ls l = ls0 l.
-
 (** ** Properties of [agree_regs]. *)
 
 (** Values of registers *)
@@ -666,6 +658,16 @@ Proof.
   apply agree_regs_set_reg; auto.
 Qed.
 
+Lemma agree_regs_undef_caller_save_regs:
+  forall j ls rs,
+  agree_regs j ls rs ->
+  agree_regs j (LTL.undef_caller_save_regs ls) (Mach.undef_caller_save_regs rs).
+Proof.
+  intros; red; intros. 
+  unfold LTL.undef_caller_save_regs, Mach.undef_caller_save_regs. 
+  destruct (is_callee_save r); auto. 
+Qed.
+
 (** Preservation under assignment of stack slot *)
 
 Lemma agree_regs_set_slot:
@@ -800,41 +802,7 @@ Lemma agree_locs_return:
 Proof.
   intros. red in H0. inv H; constructor; auto; intros.
 - rewrite H0; auto. unfold mreg_within_bounds in H. tauto.
-- rewrite H0; auto.
-Qed.
-
-(** Preservation at tailcalls (when [ls0] is changed but not [ls]). *)
-
-Lemma agree_locs_tailcall:
-  forall ls ls0 ls0',
-  agree_locs ls ls0 ->
-  agree_callee_save ls0 ls0' ->
-  agree_locs ls ls0'.
-Proof.
-  intros. red in H0. inv H; constructor; auto; intros.
-- rewrite <- H0; auto. unfold mreg_within_bounds in H. tauto.
-- rewrite <- H0; auto.
-Qed.
-
-(** ** Properties of [agree_callee_save]. *)
-
-Lemma agree_callee_save_return_regs:
-  forall ls1 ls2,
-  agree_callee_save (return_regs ls1 ls2) ls1.
-Proof.
-  intros; red; intros.
-  unfold return_regs. destruct l; auto. rewrite H; auto.
-Qed.
-
-Lemma agree_callee_save_set_result:
-  forall sg v ls1 ls2,
-  agree_callee_save ls1 ls2 ->
-  agree_callee_save (Locmap.setpair (loc_result sg) v ls1) ls2.
-Proof.
-  intros; red; intros. rewrite Locmap.gpo. apply H; auto.
-  assert (X: forall r, is_callee_save r = false -> Loc.diff l (R r)).
-  { intros. destruct l; auto. simpl; congruence. }
-  generalize (loc_result_caller_save sg). destruct (loc_result sg); simpl; intuition auto.
+- rewrite <- agree_incoming0 by auto. apply H0. congruence.
 Qed.
 
 (** ** Properties of destroyed registers. *)
@@ -1071,6 +1039,7 @@ Lemma function_prologue_correct:
   forall j ls ls0 ls1 rs rs1 m1 m1' m2 sp parent ra cs fb k P,
   agree_regs j ls rs ->
   agree_callee_save ls ls0 ->
+  agree_outgoing_arguments (Linear.fn_sig f) ls ls0 ->
   (forall r, Val.has_type (ls (R r)) (mreg_type r)) ->
   ls1 = LTL.undef_regs destroyed_at_function_entry (LTL.call_regs ls) ->
   rs1 = undef_regs destroyed_at_function_entry rs ->
@@ -1090,7 +1059,7 @@ Lemma function_prologue_correct:
   /\ j' sp = Some(sp', fe.(fe_stack_data))
   /\ inject_incr j j'.
 Proof.
-  intros until P; intros AGREGS AGCS WTREGS LS1 RS1 ALLOC TYPAR TYRA SEP.
+  intros until P; intros AGREGS AGCS AGARGS WTREGS LS1 RS1 ALLOC TYPAR TYRA SEP.
   rewrite unfold_transf_function.
   unfold fn_stacksize, fn_link_ofs, fn_retaddr_ofs.
   (* Stack layout info *)
@@ -1174,7 +1143,7 @@ Local Opaque b fe.
   split. rewrite LS1. apply agree_locs_undef_locs; [|reflexivity].
     constructor; intros. unfold call_regs. apply AGCS.
     unfold mreg_within_bounds in H; tauto.
-    unfold call_regs. apply AGCS. auto.
+    unfold call_regs. apply AGARGS. apply incoming_slot_in_parameters; auto.
   split. exact SEPFINAL.
   split. exact SAME. exact INCR.
 Qed.
@@ -1325,7 +1294,7 @@ Proof.
     apply CS; auto.
     rewrite NCS by auto. apply AGR.
   split. red; unfold return_regs; intros.
-    destruct l; auto. rewrite H; auto.
+    destruct l. rewrite H; auto. destruct sl; auto; contradiction. 
   assumption.
 Qed.
 
@@ -1619,6 +1588,7 @@ Variable ls: locset.
 Variable rs: regset.
 Hypothesis AGR: agree_regs j ls rs.
 Hypothesis AGCS: agree_callee_save ls (parent_locset cs).
+Hypothesis AGARGS: agree_outgoing_arguments sg ls (parent_locset cs).
 Variable m': mem.
 Hypothesis SEP: m' |= stack_contents j cs cs'.
 
@@ -1641,7 +1611,7 @@ Proof.
   assert (slot_within_bounds (function_bounds f) Outgoing pos ty) by eauto.
   exploit frame_get_outgoing; eauto. intros (v & A & B).
   exists v; split.
-  constructor. exact A. red in AGCS. rewrite AGCS; auto.
+  constructor. exact A. rewrite AGARGS by auto. exact B. 
 Qed.
 
 Lemma transl_external_argument_2:
@@ -1816,7 +1786,6 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
         (TRANSL: transf_fundef f = OK tf)
         (FIND: Genv.find_funct_ptr tge fb = Some tf)
         (AGREGS: agree_regs j ls rs)
-        (AGLOCS: agree_callee_save ls (parent_locset cs))
         (SEP: m' |= stack_contents j cs cs'
                  ** minjection j m
                  ** globalenv_inject ge j),
@@ -1826,7 +1795,6 @@ Inductive match_states: Linear.state -> Mach.state -> Prop :=
       forall cs ls m cs' rs m' j sg
         (STACKS: match_stacks j cs cs' sg)
         (AGREGS: agree_regs j ls rs)
-        (AGLOCS: agree_callee_save ls (parent_locset cs))
         (SEP: m' |= stack_contents j cs cs'
                  ** minjection j m
                  ** globalenv_inject ge j),
@@ -1989,9 +1957,8 @@ Proof.
   econstructor; eauto with coqlib.
   apply Val.Vptr_has_type.
   intros; red.
-    apply Z.le_trans with (size_arguments (Linear.funsig f')); auto.
+    apply Z.le_trans with (size_arguments (Linear.funsig f')); auto. 
     apply loc_arguments_bounded; auto.
-  simpl; red; auto.
   simpl. rewrite sep_assoc. exact SEP.
 
 - (* Ltailcall *)
@@ -2091,6 +2058,7 @@ Proof.
   destruct (transf_function f) as [tfn|] eqn:TRANSL; simpl; try congruence.
   intros EQ; inversion EQ; clear EQ; subst tf.
   rewrite sep_comm, sep_assoc in SEP.
+  exploit wt_callstate_agree; eauto. intros [AGCS AGARGS].
   exploit function_prologue_correct; eauto.
   red; intros; eapply wt_callstate_wt_regs; eauto.
   eapply match_stacks_type_sp; eauto.
@@ -2109,6 +2077,7 @@ Proof.
 
 - (* external function *)
   simpl in TRANSL. inversion TRANSL; subst tf.
+  exploit wt_callstate_agree; eauto. intros [AGCS AGARGS].
   exploit transl_external_arguments; eauto. apply sep_proj1 in SEP; eauto. intros [vl [ARGS VINJ]].
   rewrite sep_comm, sep_assoc in SEP.
   exploit external_call_parallel_rule; eauto.
@@ -2118,18 +2087,22 @@ Proof.
   eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   eapply match_states_return with (j := j').
   eapply match_stacks_change_meminj; eauto.
-  apply agree_regs_set_pair. apply agree_regs_inject_incr with j; auto. auto.
-  apply agree_callee_save_set_result; auto.
+  apply agree_regs_set_pair. apply agree_regs_undef_caller_save_regs. 
+  apply agree_regs_inject_incr with j; auto.
+  auto.
   apply stack_contents_change_meminj with j; auto.
   rewrite sep_comm, sep_assoc; auto.
 
 - (* return *)
-  inv STACKS. simpl in AGLOCS. simpl in SEP. rewrite sep_assoc in SEP.
+  inv STACKS. exploit wt_returnstate_agree; eauto. intros [AGCS OUTU].
+  simpl in AGCS. simpl in SEP. rewrite sep_assoc in SEP.
   econstructor; split.
   apply plus_one. apply exec_return.
   econstructor; eauto.
   apply agree_locs_return with rs0; auto.
   apply frame_contents_exten with rs0 (parent_locset s); auto.
+  intros; apply Val.lessdef_same; apply AGCS; red; congruence.
+  intros; rewrite (OUTU ty ofs); auto. 
 Qed.
 
 Lemma transf_initial_states:
@@ -2147,7 +2120,6 @@ Proof.
   eapply match_states_call with (j := j); eauto.
   constructor. red; intros. rewrite H3, loc_arguments_main in H. contradiction.
   red; simpl; auto.
-  red; simpl; auto.
   simpl. rewrite sep_pure. split; auto. split;[|split].
   eapply Genv.initmem_inject; eauto.
   simpl. exists (Mem.nextblock m0); split. apply Ple_refl.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index c6644ceb..4f95ac9b 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -334,6 +334,16 @@ Proof.
   induction res; intros; simpl; auto using locmap_set_lessdef, Val.loword_lessdef, Val.hiword_lessdef.
 Qed.
 
+Lemma locmap_undef_caller_save_regs_lessdef:
+  forall ls1 ls2,
+  locmap_lessdef ls1 ls2 -> locmap_lessdef (undef_caller_save_regs ls1) (undef_caller_save_regs ls2).
+Proof.
+  intros; red; intros. unfold undef_caller_save_regs. 
+  destruct l.
+- destruct (Conventions1.is_callee_save r); auto.
+- destruct sl; auto.
+Qed.
+
 Lemma find_function_translated:
   forall ros ls tls fd,
   locmap_lessdef ls tls ->
@@ -363,7 +373,7 @@ Lemma return_regs_lessdef:
 Proof.
   intros; red; intros. destruct l; simpl.
 - destruct (Conventions1.is_callee_save r); auto.
-- auto.
+- destruct sl; auto.
 Qed. 
 
 (** To preserve non-terminating behaviours, we show that the transformed
@@ -516,7 +526,7 @@ Proof.
   left; simpl; econstructor; split.
   eapply exec_function_external; eauto.
   eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  simpl. econstructor; eauto using locmap_setpair_lessdef.
+  simpl. econstructor; eauto using locmap_setpair_lessdef, locmap_undef_caller_save_regs_lessdef.
 - (* return *)
   inv STK. inv H1.
   left; econstructor; split.