Simplification de la semantique de LTL et LTLin. Les details lies aux conventions d'appel sont maintenant geres de maniere plus locale dans la passe Reload.

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

8 files changed, 538 insertions, 523 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 051be1e..fd569ad 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -37,6 +37,7 @@ Require Import Allocation.
 
 (** * Semantic properties of calling conventions *)
 
+(*************
 (** The value of a parameter in the called function is the same
   as the value of the corresponding argument in the caller function. *)
 
@@ -118,6 +119,7 @@ Proof.
   symmetry. apply Locmap.gso. eapply Loc.in_notin_diff; eauto. 
   intros x [A B]. rewrite Locmap.gso; auto. apply Loc.diff_sym; auto.
 Qed.
+****************)
 
 (** * Properties of allocated locations *)
 
@@ -220,7 +222,7 @@ Hypothesis REGALLOC: regalloc f flive (live0 f flive) env = Some assign.
   of [assign r] can be arbitrary. *)
 
 Definition agree (live: Regset.t) (rs: regset) (ls: locset) : Prop :=
-  forall (r: reg), Regset.In r live -> Val.lessdef (rs#r) (ls (assign r)).
+  forall (r: reg), Regset.In r live -> rs#r = ls (assign r).
 
 (** What follows is a long list of lemmas expressing properties
   of the [agree_live_regs] predicate that are useful for the 
@@ -289,7 +291,7 @@ Qed.
 
 Lemma agree_eval_reg:
   forall r live rs ls,
-  agree (reg_live r live) rs ls -> Val.lessdef (rs#r) (ls (assign r)).
+  agree (reg_live r live) rs ls -> rs#r = ls (assign r).
 Proof.
   intros. apply H. apply Regset.add_1. auto. 
 Qed.
@@ -299,11 +301,11 @@ Qed.
 Lemma agree_eval_regs:
   forall rl live rs ls,
   agree (reg_list_live rl live) rs ls ->
-  Val.lessdef_list (rs##rl) (List.map ls (List.map assign rl)).
+  rs##rl = List.map ls (List.map assign rl).
 Proof.
   induction rl; simpl; intros.
-  constructor.
-  constructor.
+  auto.
+  f_equal.
   apply agree_eval_reg with live. 
   apply agree_reg_list_live with rl. auto.
   eapply IHrl. eexact H.
@@ -345,17 +347,16 @@ Qed.
   are mapped to locations other than that of [r]. *)
 
 Lemma agree_assign_live:
-  forall live r rs ls v v',
+  forall live r rs ls v,
   (forall s,
      Regset.In s live -> s <> r -> assign s <> assign r) ->
-  Val.lessdef v v' ->
   agree (reg_dead r live) rs ls ->
-  agree live (rs#r <- v) (Locmap.set (assign r) v' ls).
+  agree live (rs#r <- v) (Locmap.set (assign r) v ls).
 Proof.
   unfold agree; intros. rewrite Regmap.gsspec.
   destruct (peq r0 r).
   subst r0. rewrite Locmap.gss. auto.
-  rewrite Locmap.gso. apply H1. apply Regset.remove_2; auto.
+  rewrite Locmap.gso. apply H0. apply Regset.remove_2; auto.
   eapply regalloc_noteq_diff. eauto. apply sym_not_equal. apply H. auto.  auto.
 Qed.
 
@@ -414,66 +415,70 @@ Qed.
   a function call, provided that the states before the call agree
   and that calling conventions are respected. *)
 
-Lemma agree_call:
-  forall live args ros res rs v (ls ls': locset),
+Lemma agree_postcall:
+  forall live args ros res rs v (ls: locset),
   (forall r,
     Regset.In r live -> r <> res ->
     ~(In (assign r) Conventions.destroyed_at_call)) ->
   (forall r,
     Regset.In r live -> r <> res -> assign r <> assign res) ->
-  Val.lessdef v (ls' (assign res)) ->
-  (forall l,
-    Loc.notin l destroyed_at_call -> loc_acceptable l -> Loc.diff l (assign res) ->
-    ls' l = ls l) ->
   agree (reg_list_live args (reg_sum_live ros (reg_dead res live))) rs ls ->
-  agree live (rs#res <- v) ls'.
+  agree live (rs#res <- v) (Locmap.set (assign res) v (postcall_regs ls)).
 Proof.
   intros. 
   assert (agree (reg_dead res live) rs ls).
   apply agree_reg_sum_live with ros. 
   apply agree_reg_list_live with args. assumption.
-  red; intros. 
-  case (Reg.eq r res); intro.
-  subst r. rewrite Regmap.gss. assumption.
-  rewrite Regmap.gso; auto. rewrite H2. apply H4.
-  apply Regset.remove_2; auto. 
-  eapply regalloc_notin_notin; eauto. 
-  eapply regalloc_acceptable; eauto.
-  eapply regalloc_noteq_diff; eauto.
+  red; intros. rewrite Regmap.gsspec. destruct (peq r res). 
+  subst r. rewrite Locmap.gss. auto.
+  rewrite Locmap.gso. transitivity (ls (assign r)). 
+  apply H2. apply Regset.remove_2; auto. 
+  unfold postcall_regs.
+  assert (~In (assign r) temporaries).
+    apply Loc.notin_not_in. eapply regalloc_not_temporary; eauto.
+  assert (~In (assign r) destroyed_at_call).
+    apply H. auto. auto.
+  caseEq (assign r); auto. intros m ASG. rewrite <- ASG. 
+  destruct (In_dec Loc.eq (assign r) temporaries). contradiction.
+  destruct (In_dec Loc.eq (assign r) destroyed_at_call). contradiction.
+  auto.
+  eapply regalloc_noteq_diff; eauto. apply sym_not_eq. auto.
 Qed.
 
 (** Agreement between the initial register set at RTL function entry
   and the location set at LTL function entry. *)
 
 Lemma agree_init_regs:
-  forall rl vl ls live,
+  forall live rl vl,
   (forall r1 r2,
     In r1 rl -> Regset.In r2 live -> r1 <> r2 ->
     assign r1 <> assign r2) ->
-  Val.lessdef_list vl (List.map ls (List.map assign rl)) ->
-  agree live (init_regs vl rl) ls.
+  agree live (RTL.init_regs vl rl) 
+             (LTL.init_locs vl (List.map assign rl)).
 Proof.
+  intro live.
+  assert (agree live (Regmap.init Vundef) (Locmap.init Vundef)).
+    red; intros. rewrite Regmap.gi. auto.
   induction rl; simpl; intros.
-  red; intros. rewrite Regmap.gi. auto.
-  inv H0. 
-  assert (agree live (init_regs vl1 rl) ls).
-  apply IHrl. intros. apply H. tauto. auto. auto. auto.
-  red; intros. case (Reg.eq a r); intro.
-  subst r. rewrite Regmap.gss. auto.
-  rewrite Regmap.gso; auto.
+  auto.
+  destruct vl. auto.
+  assert (agree live (init_regs vl rl) (init_locs vl (map assign rl))).
+  apply IHrl. intros. apply H0. tauto. auto. auto.
+  red; intros. rewrite Regmap.gsspec. destruct (peq r a). 
+  subst r. rewrite Locmap.gss. auto.
+  rewrite Locmap.gso. apply H1; auto. 
+  eapply regalloc_noteq_diff; eauto. 
 Qed.
 
 Lemma agree_parameters:
-  forall vl ls,
+  forall vl,
   let params := f.(RTL.fn_params) in
-  Val.lessdef_list vl (List.map ls (List.map assign params)) ->
   agree (live0 f flive)
-        (init_regs vl params) 
-        ls.
+        (RTL.init_regs vl params) 
+        (LTL.init_locs vl (List.map assign params)).
 Proof.
   intros. apply agree_init_regs. 
   intros. eapply regalloc_correct_3; eauto.
-  auto.
 Qed.
 
 End AGREE.
@@ -556,52 +561,40 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> Prop
   | match_stackframes_nil:
       match_stackframes nil nil
   | match_stackframes_cons:
-      forall s ts sig res f sp pc rs ls env live assign,
+      forall s ts res f sp pc rs ls env live assign,
       match_stackframes s ts ->
-      sig_res (RTL.fn_sig f) = sig_res (parent_callsig ts) ->
       wt_function f env ->
       analyze f = Some live ->
       regalloc f live (live0 f live) env = Some assign ->
-      (forall rv ls1,
-        (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls1 l = ls l) ->
-        Val.lessdef rv (ls1 (R (loc_result sig))) ->
+      (forall rv,
         agree assign (transfer f pc live!!pc)
               (rs#res <- rv)
-              (Locmap.set (assign res) (ls1 (R (loc_result sig))) ls1)) ->
+              (Locmap.set (assign res) rv ls)) ->
       match_stackframes
         (RTL.Stackframe res (RTL.fn_code f) sp pc rs :: s)
-        (LTL.Stackframe sig (assign res) (transf_fun f live assign) sp ls pc :: ts).
+        (LTL.Stackframe (assign res) (transf_fun f live assign) sp ls pc :: ts).
 
 Inductive match_states: RTL.state -> LTL.state -> Prop :=
   | match_states_intro:
-      forall s f sp pc rs m ts ls tm live assign env
+      forall s f sp pc rs m ts ls live assign env
       (STACKS: match_stackframes s ts)
-      (SIG: sig_res(RTL.fn_sig f) = sig_res(parent_callsig ts))
       (WT: wt_function f env)
       (ANL: analyze f = Some live)
       (ASG: regalloc f live (live0 f live) env = Some assign)
-      (AG: agree assign (transfer f pc live!!pc) rs ls)
-      (MMD: Mem.lessdef m tm),
+      (AG: agree assign (transfer f pc live!!pc) rs ls),
       match_states (RTL.State s (RTL.fn_code f) sp pc rs m)
-                   (LTL.State ts (transf_fun f live assign) sp pc ls tm)
+                   (LTL.State ts (transf_fun f live assign) sp pc ls m)
   | match_states_call:
-      forall s f args m ts tf ls tm,
+      forall s f args m ts tf,
       match_stackframes s ts ->
-      sig_res(RTL.funsig f) = sig_res(parent_callsig ts) ->
       transf_fundef f = OK tf ->
-      Val.lessdef_list args (List.map ls (loc_arguments (funsig tf))) ->
-      Mem.lessdef m tm ->
-      (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls l = parent_locset ts l) ->
       match_states (RTL.Callstate s f args m)
-                   (LTL.Callstate ts tf ls tm)
+                   (LTL.Callstate ts tf args m)
   | match_states_return:
-      forall s v m ts ls tm,
+      forall s v m ts,
       match_stackframes s ts ->
-      Val.lessdef v (ls (R (loc_result (parent_callsig ts)))) ->
-      Mem.lessdef m tm ->
-      (forall l, Loc.notin l destroyed_at_call -> loc_acceptable l -> ls l = parent_locset ts l) ->
       match_states (RTL.Returnstate s v m)
-                   (LTL.Returnstate ts ls tm).
+                   (LTL.Returnstate ts v m).
 
 (** The simulation proof is by case analysis over the RTL transition
   taken in the source program. *)
@@ -652,10 +645,9 @@ Lemma transl_find_function:
     transf_fundef f = OK tf.
 Proof.
   intros; destruct ros; simpl in *.
-  assert (Val.lessdef (rs#r) (ls (alloc r))).
+  assert (rs#r = ls (alloc r)).
     eapply agree_eval_reg. eapply agree_reg_list_live; eauto.
-  inv H1. apply functions_translated. auto.
-  exploit Genv.find_funct_inv; eauto. intros [b EQ]. congruence.
+  rewrite <- H1. apply functions_translated. auto.
   rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
   apply function_ptr_translated. auto. discriminate.
 Qed.
@@ -696,15 +688,11 @@ Proof.
   rewrite <- H1. eapply agree_move_live; eauto.
   (* Not a move *)
   intros INMO CORR CODE.
-  assert (exists v1,
-          eval_operation tge sp op (map ls (map assign args)) tm = Some v1
-          /\ Val.lessdef v v1).
-    apply eval_operation_lessdef with m (rs##args); auto.
+  assert (eval_operation tge sp op (map ls (map assign args)) m = Some v).
+    replace (map ls (map assign args)) with (rs##args).
+    rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. 
     eapply agree_eval_regs; eauto.
-    rewrite (eval_operation_preserved symbols_preserved). assumption.
-  destruct H1 as [v1 [EV VMD]].
-  econstructor; split. eapply exec_Lop; eauto. 
-  MatchStates. 
+  econstructor; split. eapply exec_Lop; eauto. MatchStates. 
   apply agree_assign_live with f env live; auto.
   eapply agree_reg_list_live; eauto.
   (* Result is not live, instruction turned into a nop *)
@@ -717,15 +705,10 @@ Proof.
   rewrite LV in AG.
   (* dst is live *)
   exploit Regset.mem_2; eauto. intro LV'.
-  assert (exists a',
-      eval_addressing tge sp addr (map ls (map assign args)) = Some a'
-      /\ Val.lessdef a a').
-    apply eval_addressing_lessdef with (rs##args). 
-    eapply agree_eval_regs; eauto.
+  assert (eval_addressing tge sp addr (map ls (map assign args)) = Some a).
+    replace (map ls (map assign args)) with (rs##args).
     rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  destruct H2 as [a' [EVAL VMD]].
-  exploit Mem.loadv_lessdef; eauto. 
-  intros [v' [LOADV VMD2]].
+    eapply agree_eval_regs; eauto.
   econstructor; split.
   eapply exec_Lload; eauto. TranslInstr. rewrite LV; auto.
   generalize (regalloc_correct_1 f env live _ _ _ _ ASG H).
@@ -740,106 +723,61 @@ Proof.
   red; intro; exploit Regset.mem_1; eauto. congruence.
 
   (* Istore *)
-  assert (exists a',
-      eval_addressing tge sp addr (map ls (map assign args)) = Some a'
-      /\ Val.lessdef a a').
-    apply eval_addressing_lessdef with (rs##args). 
-    eapply agree_eval_regs; eauto.
+  assert (eval_addressing tge sp addr (map ls (map assign args)) = Some a).
+    replace (map ls (map assign args)) with (rs##args).
     rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
-  destruct H2 as [a' [EVAL VMD]].
-  assert (ESRC: Val.lessdef rs#src (ls (assign src))).
+    eapply agree_eval_regs; eauto.
+  assert (ESRC: rs#src = ls (assign src)).
     eapply agree_eval_reg. eapply agree_reg_list_live. eauto.
-  assert (exists tm', storev chunk tm a' (ls (assign src)) = Some tm'
-                     /\ Mem.lessdef m' tm').
-    eapply Mem.storev_lessdef; eauto. 
-  destruct H2 as [m1' [STORE MMD']].
   econstructor; split.
   eapply exec_Lstore; eauto. TranslInstr.
+  rewrite <- ESRC. eauto.
   MatchStates. eapply agree_reg_live. eapply agree_reg_list_live. eauto.
 
   (* Icall *)
   exploit transl_find_function; eauto.  intros [tf [TFIND TF]].
   generalize (regalloc_correct_1 f0 env live _ _ _ _ ASG H).
  unfold correct_alloc_instr. intros [CORR1 CORR2].
-  exploit (parmov_spec ls (map assign args) 
-                            (loc_arguments (RTL.funsig f))).
-  apply loc_arguments_norepet.
-  rewrite loc_arguments_length. inv WTI.
-  rewrite <- H7. repeat rewrite list_length_map. auto.
-  intros [PM1 PM2].  
+  assert (rs##args = map ls (map assign args)).
+    eapply agree_eval_regs; eauto. 
   econstructor; split. 
   eapply exec_Lcall; eauto. TranslInstr.
   rewrite (sig_function_translated _ _ TF). eauto.
-  rewrite (sig_function_translated _ _ TF).
+  rewrite H1. 
   econstructor; eauto.
   econstructor; eauto.
   intros. eapply agree_succ with (n := pc); eauto.
   unfold RTL.successors; rewrite H; auto with coqlib.
-  eapply agree_call with (ls := ls); eauto.
-  rewrite Locmap.gss. auto.
-  intros. rewrite Locmap.gso. rewrite H1; auto. apply PM2; auto.
-  eapply arguments_not_preserved; eauto. apply Loc.diff_sym; auto.
-  rewrite (sig_function_translated _ _ TF).
-  change Regset.elt with reg in PM1. 
-  rewrite PM1. eapply agree_eval_regs; eauto. 
+  eapply agree_postcall; eauto.
 
   (* Itailcall *)
   exploit transl_find_function; eauto.  intros [tf [TFIND TF]].
-  exploit (parmov_spec ls (map assign args) 
-                            (loc_arguments (RTL.funsig f))).
-  apply loc_arguments_norepet.
-  rewrite loc_arguments_length. inv WTI.
-  rewrite <- H6. repeat rewrite list_length_map. auto.
-  intros [PM1 PM2].  
+  assert (rs##args = map ls (map assign args)).
+    eapply agree_eval_regs; eauto. 
   econstructor; split. 
   eapply exec_Ltailcall; eauto. TranslInstr.
   rewrite (sig_function_translated _ _ TF). eauto.
-  rewrite (sig_function_translated _ _ TF).
-  econstructor; eauto.
-  inv WTI. congruence.
-  rewrite (sig_function_translated _ _ TF).
-  rewrite return_regs_arguments. 
-  change Regset.elt with reg in PM1. 
-  rewrite PM1. eapply agree_eval_regs; eauto.
-  inv WTI; auto.
-  apply free_lessdef; auto.
-  intros. rewrite return_regs_not_destroyed; auto. 
+  rewrite H1. econstructor; eauto.
 
   (* Ialloc *)
-  assert (Val.lessdef (Vint sz) (ls (assign arg))).
-    rewrite <- H0. eapply agree_eval_reg. eauto.
-  inversion H2. subst v. 
-  pose (ls1 := Locmap.set (R loc_alloc_argument) (ls (assign arg)) ls).
-  pose (ls2 := Locmap.set (R loc_alloc_result) (Vptr b Int.zero) ls1).
-  pose (ls3 := Locmap.set (assign res) (ls2 (R loc_alloc_result)) ls2).
-  caseEq (alloc tm 0 (Int.signed sz)). intros tm' b1 ALLOC1.
-  exploit Mem.alloc_lessdef; eauto. intros [EQ MMD1]. subst b1.
-  exists (State ts (transf_fun f live assign) sp pc' ls3 tm'); split.
-  unfold ls3, ls2, ls1. eapply exec_Lalloc; eauto. TranslInstr.
+  assert (ls (assign arg) = Vint sz).
+    rewrite <- H0. symmetry. eapply agree_eval_reg; eauto.
+  econstructor; split.
+  eapply exec_Lalloc; eauto. TranslInstr.
   generalize (regalloc_correct_1 f env live _ _ _ _ ASG H). 
   unfold correct_alloc_instr.  intros [CORR1 CORR2].
   MatchStates.
-  eapply agree_call with (args := arg :: nil) (ros := inr reg 1%positive) (ls := ls); eauto.
-  unfold ls3; rewrite Locmap.gss. 
-  unfold ls2; rewrite Locmap.gss. auto.
-  intros. unfold ls3; rewrite Locmap.gso.
-  unfold ls2; rewrite Locmap.gso. 
-  unfold ls1; apply Locmap.gso.
-  apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto. 
-  unfold loc_alloc_argument, destroyed_at_call; simpl; tauto.
-  apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto. 
-  unfold loc_alloc_result, destroyed_at_call; simpl; tauto.
-  apply Loc.diff_sym; auto.
+  eapply agree_postcall with (args := arg :: nil) (ros := inr reg 1%positive); eauto.
 
   (* Icond, true *)
-  assert (COND: eval_condition cond (map ls (map assign args)) tm = Some true).
-    eapply eval_condition_lessdef; eauto. 
+  assert (COND: eval_condition cond (map ls (map assign args)) m = Some true).
+    replace (map ls (map assign args)) with (rs##args). auto.
     eapply agree_eval_regs; eauto.
   econstructor; split.
   eapply exec_Lcond_true; eauto. TranslInstr.
   MatchStates. eapply agree_reg_list_live. eauto.
   (* Icond, false *)
-  assert (COND: eval_condition cond (map ls (map assign args)) tm = Some false).
-    eapply eval_condition_lessdef; eauto. 
+  assert (COND: eval_condition cond (map ls (map assign args)) m = Some false).
+    replace (map ls (map assign args)) with (rs##args). auto.
     eapply agree_eval_regs; eauto.
   econstructor; split.
   eapply exec_Lcond_false; eauto. TranslInstr.
@@ -848,16 +786,12 @@ Proof.
   (* Ireturn *)
   econstructor; split.
   eapply exec_Lreturn; eauto. TranslInstr; eauto.
+  replace (regmap_optget or Vundef rs)
+     with (locmap_optget (option_map assign or) Vundef ls).
   econstructor; eauto.
-  rewrite return_regs_result.  
-  inv WTI. destruct or; simpl in *. 
-  replace (loc_result (parent_callsig ts))
-     with (loc_result (RTL.fn_sig f)).
-  rewrite Locmap.gss. eapply agree_eval_reg; eauto.
-  unfold loc_result. rewrite SIG. auto.
-  constructor. 
-  apply free_lessdef; auto.
-  intros. apply return_regs_not_destroyed; auto.
+  inv WTI. destruct or; simpl in *.
+  symmetry; eapply agree_eval_reg; eauto. 
+  auto.
 
   (* internal function *)
   generalize H7. simpl.  unfold transf_function.
@@ -866,46 +800,21 @@ Proof.
   caseEq (analyze f); simpl; try congruence. intros live ANL.
   caseEq (regalloc f live (live0 f live) env); simpl; try congruence.
   intros alloc ALLOC EQ. inv EQ. simpl in *.
-  caseEq (Mem.alloc tm 0 (RTL.fn_stacksize f)). intros tm' stk' MEMALLOC.
-  exploit alloc_lessdef; eauto. intros [EQ LDM]. subst stk'.
   econstructor; split.
   eapply exec_function_internal; simpl; eauto.
   simpl. econstructor; eauto.
-  apply agree_init_regs. intros; eapply regalloc_correct_3; eauto.
-  inv WTF.
-  exploit (parmov_spec (call_regs ls) 
-                       (loc_parameters (RTL.fn_sig f))
-                       (map alloc (RTL.fn_params f))).
-  eapply regalloc_norepet_norepet; eauto.
-  eapply regalloc_correct_2; eauto.
-  rewrite loc_parameters_length. symmetry. 
-  transitivity (length (map env (RTL.fn_params f))).
-  repeat rewrite list_length_map. auto.
-  rewrite wt_params; auto.
-  intros [PM1 PM2].
-  change Regset.elt with reg in PM1. rewrite PM1.
-  replace (map (call_regs ls) (loc_parameters (RTL.fn_sig f)))
-     with (map ls (loc_arguments (RTL.fn_sig f))).
-  auto.
-  symmetry. unfold loc_parameters. rewrite list_map_compose.
-  apply list_map_exten. intros. symmetry. eapply call_regs_param_of_arg; eauto.
+  change (transfer f (RTL.fn_entrypoint f) live !! (RTL.fn_entrypoint f))
+    with (live0 f live).
+  eapply agree_parameters; eauto. 
 
   (* external function *)
   injection H7; intro EQ; inv EQ.
-  exploit event_match_lessdef; eauto. intros [tres [A B]].
   econstructor; split.
   eapply exec_function_external; eauto.
   eapply match_states_return; eauto.
-  replace (loc_result (parent_callsig ts))
-     with (loc_result (ef_sig ef)).
-  rewrite Locmap.gss. auto.
-  unfold loc_result. rewrite <- H6. auto.
-  intros. rewrite <- H11; auto. apply Locmap.gso.
-  apply Loc.diff_sym. eapply Loc.in_notin_diff; eauto.
-  apply loc_result_caller_save. 
 
   (* return *)
-  inv H3. 
+  inv H4. 
   econstructor; split.
   eapply exec_return; eauto.
   econstructor; eauto.
@@ -920,27 +829,21 @@ Lemma transf_initial_states:
 Proof.
   intros. inversion H.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
-  assert (SIG2: funsig tf = mksignature nil (Some Tint)).
-    rewrite <- H2. apply sig_function_translated; auto.
-  assert (VPARAMS: Val.lessdef_list nil (map (Locmap.init Vundef) (loc_arguments (funsig tf)))).
-    rewrite SIG2. simpl. constructor.
-  assert (GENV: (Genv.init_mem tprog) = (Genv.init_mem prog)).
+  assert (MEM: (Genv.init_mem tprog) = (Genv.init_mem prog)).
     exact (Genv.init_mem_transf_partial _ _ TRANSF).
-  assert (MMD: Mem.lessdef (Genv.init_mem prog) (Genv.init_mem tprog)).
-    rewrite GENV. apply Mem.lessdef_refl.
-  exists (LTL.Callstate nil tf (Locmap.init Vundef) (Genv.init_mem tprog)); split.
+  exists (LTL.Callstate nil tf nil (Genv.init_mem tprog)); split.
   econstructor; eauto.
   rewrite symbols_preserved. 
   rewrite (transform_partial_program_main _ _ TRANSF).  auto.
-  constructor; auto. constructor. rewrite H2; auto. 
+  rewrite <- H2. apply sig_function_translated; auto. 
+  rewrite MEM. constructor; auto. constructor.
 Qed.
 
 Lemma transf_final_states:
   forall st1 st2 r, 
   match_states st1 st2 -> RTL.final_state st1 r -> LTL.final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv H3. econstructor.
-  simpl in H4. inv H4. auto. 
+  intros. inv H0. inv H. inv H4. econstructor.
 Qed.
 
 Theorem transf_program_correct:
diff --git a/backend/LTL.v b/backend/LTL.v
index a082e12..e39a4ec 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -72,53 +72,20 @@ Definition funsig (fd: fundef) :=
 Definition genv := Genv.t fundef.
 Definition locset := Locmap.t.
 
-Section RELSEM.
-
-(** Calling conventions are reflected at the level of location sets
-  (environments mapping locations to values) by the following two 
-  functions.  
+Definition locmap_optget (ol: option loc) (dfl: val) (ls: locset) : val :=
+  match ol with
+  | None => dfl
+  | Some l => ls l
+  end.
 
-  [call_regs caller] returns the location set at function entry,
-  as a function of the location set [caller] of the calling function.
-- Machine registers have the same values as in the caller.
-- Incoming stack slots (used for parameter passing) have the same
-  values as the corresponding outgoing stack slots (used for argument
-  passing) in the caller.
-- Local and outgoing stack slots are initialized to undefined values.
-*) 
+Fixpoint init_locs (vl: list val) (rl: list loc) {struct rl} : locset :=
+  match rl, vl with
+  | r1 :: rs, v1 :: vs => Locmap.set r1 v1 (init_locs vs rs)
+  | _, _ => Locmap.init Vundef
+  end.
 
-Definition call_regs (caller: locset) : locset :=
-  fun (l: loc) =>
-    match l with
-    | R r => caller (R r)
-    | S (Local ofs ty) => Vundef
-    | S (Incoming ofs ty) => caller (S (Outgoing ofs ty))
-    | S (Outgoing ofs ty) => Vundef
-    end.
 
-(** [return_regs caller callee] returns the location set after
-  a call instruction, as a function of the location set [caller]
-  of the caller before the call instruction and of the location
-  set [callee] of the callee at the return instruction.
-- 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 at the return point.
-- Stack slots have the same values as in the caller before the call.
-*)
-
-Definition return_regs (caller callee: locset) : locset :=
-  fun (l: loc) =>
-    match l with
-    | R r =>
-        if In_dec Loc.eq (R r) Conventions.temporaries then
-          callee (R r)
-        else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then
-          callee (R r)
-        else
-          caller (R r)
-    | S s => caller (S s)
-    end.
+Section RELSEM.
 
 (** [parmov srcs dsts ls] performs the parallel assignment
   of locations [dsts] to the values of the corresponding locations
@@ -130,18 +97,29 @@ Fixpoint parmov (srcs dsts: list loc) (ls: locset) {struct srcs} : locset :=
   | _, _ => ls
   end.
 
-Definition set_result_reg (s: signature) (or: option loc) (ls: locset) :=
-  match or with 
-  | Some r => Locmap.set (R (loc_result s)) (ls r) ls
-  | None => ls
-  end.
+(** [postcall_regs ls] returns the location set [ls] after a function
+  call.  Caller-save registers and temporary registers
+  are set to [undef], reflecting the fact that the called
+  function can modify them freely. *)
+
+Definition postcall_regs (ls: locset) : locset :=
+  fun (l: loc) =>
+    match l with
+    | R r =>
+        if In_dec Loc.eq (R r) Conventions.temporaries then
+          Vundef
+        else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then
+          Vundef
+        else
+          ls (R r)
+    | S s => ls (S s)
+    end.
 
 (** LTL execution states. *)
 
 Inductive stackframe : Set :=
   | Stackframe:
-      forall (sig: signature)   (**r signature of call *)
-             (res: loc)         (**r where to store the result *)
+      forall (res: loc)         (**r where to store the result *)
              (f: function)      (**r calling function *)
              (sp: val)          (**r stack pointer in calling function *)
              (ls: locset)       (**r location state in calling function *)
@@ -160,27 +138,15 @@ Inductive state : Set :=
   | Callstate:
       forall (stack: list stackframe) (**r call stack *)
              (f: fundef)              (**r function to call *)
-             (ls: locset)             (**r location state at point of call *)
+             (args: list val)         (**r arguments to the call *)
              (m: mem),                (**r memory state *)
       state
   | Returnstate:
       forall (stack: list stackframe) (**r call stack *)
-             (ls: locset)             (**r location state at point of return *)
+             (v: val)                 (**r return value for the call *)
              (m: mem),                (**r memory state *)
       state.
 
-Definition parent_locset (stack: list stackframe) : locset :=
-  match stack with
-  | nil => Locmap.init Vundef
-  | Stackframe sg res f sp ls pc :: stack' => ls
-  end.
-
-Definition parent_callsig (stack: list stackframe) : signature :=
-  match stack with
-  | nil => mksignature nil (Some Tint)
-  | Stackframe sg res f sp ls pc :: stack' => sg
-  end.
-
 Variable ge: genv.
 
 Definition find_function (los: loc + ident) (rs: locset) : option fundef :=
@@ -265,28 +231,23 @@ Inductive step: state -> trace -> state -> Prop :=
       (fn_code f)!pc = Some(Lcall sig ros args res pc') ->
       find_function ros rs = Some f' ->
       funsig f' = sig ->
-      let rs1 := parmov args (loc_arguments sig) rs in
       step (State s f sp pc rs m)
-        E0 (Callstate (Stackframe sig res f sp rs1 pc' :: s) f' rs1 m)
+        E0 (Callstate (Stackframe res f sp (postcall_regs rs) pc' :: s)
+                      f' (List.map rs args) m)
   | exec_Ltailcall:
       forall s f stk pc rs m sig ros args f',
       (fn_code f)!pc = Some(Ltailcall sig ros args) ->
       find_function ros rs = Some f' ->
       funsig f' = sig ->
-      let rs1 := parmov args (loc_arguments sig) rs in
-      let rs2 := return_regs (parent_locset s) rs1 in
       step (State s f (Vptr stk Int.zero) pc rs m)
-        E0 (Callstate s f' rs2 (Mem.free m stk))
+        E0 (Callstate s f' (List.map rs args) (Mem.free m stk))
   | exec_Lalloc:
       forall s f sp pc rs m pc' arg res sz m' b,
       (fn_code f)!pc = Some(Lalloc arg res pc') ->
       rs arg = Vint sz ->
       Mem.alloc m 0 (Int.signed sz) = (m', b) ->
-      let rs1 := Locmap.set (R loc_alloc_argument) (rs arg) rs in
-      let rs2 := Locmap.set (R loc_alloc_result) (Vptr b Int.zero) rs1 in
-      let rs3 := Locmap.set res (rs2 (R loc_alloc_result)) rs2 in
       step (State s f sp pc rs m)
-        E0 (State s f sp pc' rs3 m')
+        E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_regs rs)) m')
   | exec_Lcond_true:
       forall s f sp pc rs m cond args ifso ifnot,
       (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
@@ -302,30 +263,22 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Lreturn:
       forall s f stk pc rs m or,
       (fn_code f)!pc = Some(Lreturn or) ->
-      let rs1 := set_result_reg f.(fn_sig) or rs in
-      let rs2 := return_regs (parent_locset s) rs1 in
       step (State s f (Vptr stk Int.zero) pc rs m)
-        E0 (Returnstate s rs2 (Mem.free m stk))
+        E0 (Returnstate s (locmap_optget or Vundef rs) (Mem.free m stk))
   | exec_function_internal:
-      forall s f rs m m' stk,
+      forall s f args m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
-      let rs1 := call_regs rs in
-      let rs2 := parmov (loc_parameters f.(fn_sig)) f.(fn_params) rs1 in
-      step (Callstate s (Internal f) rs m)
-        E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) rs2 m')
+      step (Callstate s (Internal f) args m)
+        E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) (init_locs args f.(fn_params)) m')
   | exec_function_external:
-      forall s ef t res rs m,
-      let args := map rs (Conventions.loc_arguments ef.(ef_sig)) in
+      forall s ef t args res m,
       event_match ef args t res ->
-      let rs1 :=
-        Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in
-      step (Callstate s (External ef) rs m)
-         t (Returnstate s rs1 m)
+      step (Callstate s (External ef) args m)
+         t (Returnstate s res m)
   | exec_return:
-      forall res f sp rs0 pc s sig rs m,
-      let rs1 := Locmap.set res (rs (R (loc_result sig))) rs in
-      step (Returnstate (Stackframe sig res f sp rs0 pc :: s) rs m)
-        E0 (State s f sp pc rs1 m).
+      forall res f sp rs pc s vres m,
+      step (Returnstate (Stackframe res f sp rs pc :: s) vres m)
+        E0 (State s f sp pc (Locmap.set res vres rs) m).
 
 End RELSEM.
 
@@ -341,12 +294,11 @@ Inductive initial_state (p: program): state -> Prop :=
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
-      initial_state p (Callstate nil f (Locmap.init Vundef) m0).
+      initial_state p (Callstate nil f nil m0).
 
 Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall rs m r,
-      rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r ->
-      final_state (Returnstate nil rs m) r.
+  | final_state_intro: forall n m,
+      final_state (Returnstate nil (Vint n) m) n.
 
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=
   program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
diff --git a/backend/LTLin.v b/backend/LTLin.v
index 157b6d4..83787ce 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -112,8 +112,7 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
 
 Inductive stackframe : Set :=
   | Stackframe:
-      forall (sig: signature) (**r signature of call *)
-             (res: loc)       (**r where to store the result *)
+      forall (res: loc)       (**r where to store the result *)
              (f: function)    (**r calling function *)
              (sp: val)        (**r stack pointer in calling function *)
              (ls: locset)     (**r location state in calling function *)
@@ -132,26 +131,22 @@ Inductive state : Set :=
   | Callstate:
       forall (stack: list stackframe) (**r call stack *)
              (f: fundef)              (**r function to call *)
-             (ls: locset)             (**r location state at point of call *)
+             (args: list val)         (**r arguments to the call *)
              (m: mem),                (**r memory state *)
       state
   | Returnstate:
       forall (stack: list stackframe) (**r call stack *)
-             (ls: locset)             (**r location state at point of return *)
+             (v: val)                 (**r return value for the call *)
              (m: mem),                (**r memory state *)
       state.
 
-Definition parent_locset (stack: list stackframe) : locset :=
-  match stack with
-  | nil => Locmap.init Vundef
-  | Stackframe sg res f sp ls pc :: stack' => ls
-  end.
-
+(*
 Definition parent_callsig (stack: list stackframe) : signature :=
   match stack with
   | nil => mksignature nil (Some Tint)
   | Stackframe sg res f sp ls pc :: stack' => sg
   end.
+*)
 
 Section RELSEM.
 
@@ -189,26 +184,21 @@ Inductive step: state -> trace -> state -> Prop :=
       forall s f sp sig ros args res b rs m f',
       find_function ros rs = Some f' ->
       sig = funsig f' ->
-      let rs1 := parmov args (loc_arguments sig) rs in
       step (State s f sp (Lcall sig ros args res :: b) rs m)
-        E0 (Callstate (Stackframe sig res f sp rs1 b :: s) f' rs1 m)
+        E0 (Callstate (Stackframe res f sp (postcall_regs rs) b :: s)
+                      f' (List.map rs args) m)
   | exec_Ltailcall:
       forall s f stk sig ros args b rs m f',
       find_function ros rs = Some f' ->
       sig = funsig f' ->
-      let rs1 := parmov args (loc_arguments sig) rs in
-      let rs2 := return_regs (parent_locset s) rs1 in
       step (State s f (Vptr stk Int.zero) (Ltailcall sig ros args :: b) rs m)
-        E0 (Callstate s f' rs2 (Mem.free m stk))
+        E0 (Callstate s f' (List.map rs args) (Mem.free m stk))
   | exec_Lalloc:
       forall s f sp arg res b rs m sz m' blk,
       rs arg = Vint sz ->
       Mem.alloc m 0 (Int.signed sz) = (m', blk) ->
-      let rs1 := Locmap.set (R loc_alloc_argument) (rs arg) rs in
-      let rs2 := Locmap.set (R loc_alloc_result) (Vptr blk Int.zero) rs1 in
-      let rs3 := Locmap.set res (rs2 (R loc_alloc_result)) rs2 in
       step (State s f sp (Lalloc arg res :: b) rs m)
-        E0 (State s f sp b rs3 m')
+        E0 (State s f sp b (Locmap.set res (Vptr blk Int.zero) (postcall_regs rs)) m')
   | exec_Llabel:
       forall s f sp lbl b rs m,
       step (State s f sp (Llabel lbl :: b) rs m)
@@ -231,30 +221,22 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f sp b rs m)
   | exec_Lreturn:
       forall s f stk rs m or b,
-      let rs1 := set_result_reg f.(fn_sig) or rs in
-      let rs2 := return_regs (parent_locset s) rs1 in
       step (State s f (Vptr stk Int.zero) (Lreturn or :: b) rs m)
-        E0 (Returnstate s rs2 (Mem.free m stk))
+        E0 (Returnstate s (locmap_optget or Vundef rs) (Mem.free m stk))
   | exec_function_internal:
-      forall s f rs m m' stk,
+      forall s f args m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
-      let rs1 := call_regs rs in
-      let rs2 := parmov (loc_parameters f.(fn_sig)) f.(fn_params) rs1 in
-      step (Callstate s (Internal f) rs m)
-        E0 (State s f (Vptr stk Int.zero) f.(fn_code) rs2 m')
+      step (Callstate s (Internal f) args m)
+        E0 (State s f (Vptr stk Int.zero) f.(fn_code) (init_locs args f.(fn_params)) m')
   | exec_function_external:
-      forall s ef t res rs m,
-      let args := map rs (Conventions.loc_arguments ef.(ef_sig)) in
+      forall s ef args t res m,
       event_match ef args t res ->
-      let rs1 :=
-        Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in
-      step (Callstate s (External ef) rs m)
-         t (Returnstate s rs1 m)
+      step (Callstate s (External ef) args m)
+         t (Returnstate s res m)
   | exec_return:
-      forall res f sp rs0 b s sig rs m,
-      let rs1 := Locmap.set res (rs (R (loc_result sig))) rs in
-      step (Returnstate (Stackframe sig res f sp rs0 b :: s) rs m)
-        E0 (State s f sp b rs1 m).
+      forall res f sp rs b s vres m,
+      step (Returnstate (Stackframe res f sp rs b :: s) vres m)
+        E0 (State s f sp b (Locmap.set res vres rs) m).
 
 End RELSEM.
 
@@ -265,12 +247,11 @@ Inductive initial_state (p: program): state -> Prop :=
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
-      initial_state p (Callstate nil f (Locmap.init Vundef) m0).
+      initial_state p (Callstate nil f nil m0).
 
 Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall rs m r,
-      rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r ->
-      final_state (Returnstate nil rs m) r.
+  | final_state_intro: forall n m,
+      final_state (Returnstate nil (Vint n) m) n.
 
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=
   program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
diff --git a/backend/Linear.v b/backend/Linear.v
index b9880ff..ca1a2bc 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -116,6 +116,52 @@ Definition find_function (ros: mreg + ident) (rs: locset) : option fundef :=
 Definition reglist (rs: locset) (rl: list mreg) : list val :=
   List.map (fun r => rs (R r)) rl.
 
+(** Calling conventions are reflected at the level of location sets
+  (environments mapping locations to values) by the following two 
+  functions.  
+
+  [call_regs caller] returns the location set at function entry,
+  as a function of the location set [caller] of the calling function.
+- Machine registers have the same values as in the caller.
+- Incoming stack slots (used for parameter passing) have the same
+  values as the corresponding outgoing stack slots (used for argument
+  passing) in the caller.
+- Local and outgoing stack slots are initialized to undefined values.
+*) 
+
+Definition call_regs (caller: locset) : locset :=
+  fun (l: loc) =>
+    match l with
+    | R r => caller (R r)
+    | S (Local ofs ty) => Vundef
+    | S (Incoming ofs ty) => caller (S (Outgoing ofs ty))
+    | S (Outgoing ofs ty) => Vundef
+    end.
+
+(** [return_regs caller callee] returns the location set after
+  a call instruction, as a function of the location set [caller]
+  of the caller before the call instruction and of the location
+  set [callee] of the callee at the return instruction.
+- 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 at the return point.
+- Stack slots have the same values as in the caller before the call.
+*)
+
+Definition return_regs (caller callee: locset) : locset :=
+  fun (l: loc) =>
+    match l with
+    | R r =>
+        if In_dec Loc.eq (R r) Conventions.temporaries then
+          callee (R r)
+        else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then
+          callee (R r)
+        else
+          caller (R r)
+    | S s => caller (S s)
+    end.
+
 (** Linear execution states. *)
 
 Inductive stackframe: Set :=
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 303482e..3451cdb 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -468,15 +468,15 @@ Qed.
 
 Inductive match_stackframes: LTL.stackframe -> LTLin.stackframe -> Prop :=
   | match_stackframe_intro:
-      forall sig res f sp pc ls tf c,
+      forall res f sp pc ls tf c,
       transf_function f = OK tf ->
       (reachable f)!!pc = true ->
       valid_successor f pc ->
       is_tail c (fn_code tf) ->
       wt_function f ->
       match_stackframes
-        (LTL.Stackframe sig res f sp ls pc)
-        (LTLin.Stackframe sig res tf sp ls (add_branch pc c)).
+        (LTL.Stackframe res f sp ls pc)
+        (LTLin.Stackframe res tf sp ls (add_branch pc c)).
 
 Inductive match_states: LTL.state -> LTLin.state -> Prop :=
   | match_states_intro:
@@ -501,14 +501,6 @@ Inductive match_states: LTL.state -> LTLin.state -> Prop :=
       match_states (LTL.Returnstate s ls m)
                    (LTLin.Returnstate ts ls m).
 
-Remark parent_locset_match:
-  forall s ts,
-  list_forall2 match_stackframes s ts ->
-  parent_locset ts = LTL.parent_locset s.
-Proof.
-  induction 1; simpl; auto. inv H; auto. 
-Qed.
-
 Hypothesis wt_prog: wt_program prog.
 
 Theorem transf_step_correct:
@@ -578,8 +570,6 @@ Proof.
   traceEq.
   econstructor; eauto.
   (* Lcall *)
-  unfold rs1 in *. inv MS. fold rs1.
-  generalize (wt_instrs _ WTF _ _ H); intro WTI.
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   assert (REACH': (reachable f)!!pc' = true).
@@ -600,14 +590,12 @@ Proof.
   eapply Genv.find_funct_ptr_prop; eauto.
 
   (* Ltailcall *)
-  unfold rs2, rs1 in *. inv MS. fold rs1; fold rs2.
   destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ].
   simpl in EQ. subst c.
   exploit find_function_translated; eauto. intros [tf' [A B]].
   econstructor; split.
   apply plus_one. eapply exec_Ltailcall with (f' := tf'); eauto.
   symmetry; apply sig_preserved; auto.
-  rewrite (parent_locset_match _ _ STACKS).
   econstructor; eauto.
   destruct ros; simpl in H0.
   eapply Genv.find_funct_prop; eauto.
@@ -677,8 +665,7 @@ Proof.
   simpl in EQ. subst c.
   econstructor; split.
   apply plus_one. eapply exec_Lreturn; eauto.
-  rewrite (parent_locset_match _ _ STACKS).
-  monadInv TRF. simpl. econstructor; eauto.
+  econstructor; eauto.
  
   (* internal function *)
   assert (REACH: (reachable f)!!(LTL.fn_entrypoint f) = true).
@@ -714,7 +701,7 @@ Lemma transf_initial_states:
 Proof.
   intros. inversion H.
   exploit function_ptr_translated; eauto. intros [tf [A B]].  
-  exists (Callstate nil tf (Locmap.init Vundef) (Genv.init_mem tprog)); split.
+  exists (Callstate nil tf nil (Genv.init_mem tprog)); split.
   econstructor; eauto.
   replace (prog_main tprog) with (prog_main prog).
   rewrite symbols_preserved. eauto.
@@ -730,7 +717,7 @@ Lemma transf_final_states:
   forall st1 st2 r, 
   match_states st1 st2 -> LTL.final_state st1 r -> LTLin.final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv H5. constructor. auto. 
+  intros. inv H0. inv H. inv H4. constructor.
 Qed.
 
 Theorem transf_program_correct:
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index f0b17e1..372a261 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -414,22 +414,22 @@ End LINEAR_CONSTRUCTORS.
   that is, non-temporary registers and [Local] stack slots. *)
 
 Definition agree (rs1 rs2: locset) : Prop :=
-  forall l, loc_acceptable l -> rs2 l = rs1 l.
+  forall l, loc_acceptable l -> Val.lessdef (rs1 l) (rs2 l).
 
 Lemma agree_loc:
   forall rs1 rs2 l,
-  agree rs1 rs2 -> loc_acceptable l -> rs2 l = rs1 l.
+  agree rs1 rs2 -> loc_acceptable l -> Val.lessdef (rs1 l) (rs2 l).
 Proof.
   auto.
 Qed.
 
 Lemma agree_locs:
   forall rs1 rs2 ll,
-  agree rs1 rs2 -> locs_acceptable ll -> map rs2 ll = map rs1 ll.
+  agree rs1 rs2 -> locs_acceptable ll -> Val.lessdef_list (map rs1 ll) (map rs2 ll).
 Proof.
   induction ll; simpl; intros.
-  auto.
-  f_equal. apply H. apply H0; auto with coqlib.
+  constructor.
+  constructor. apply H. apply H0; auto with coqlib.
   apply IHll; auto. red; intros. apply H0; auto with coqlib.
 Qed.
 
@@ -446,7 +446,7 @@ Qed.
 Lemma agree_set:
   forall rs1 rs2 rs2' l v,
   loc_acceptable l ->
-  rs2' l = v ->
+  Val.lessdef v (rs2' l) ->
   (forall l', Loc.diff l l' -> Loc.notin l' temporaries -> rs2' l' = rs2 l') ->
   agree rs1 rs2 -> agree (Locmap.set l v rs1) rs2'.
 Proof.
@@ -458,6 +458,7 @@ Proof.
   apply temporaries_not_acceptable; auto. 
 Qed.
 
+(*****
 Lemma agree_return_regs:
   forall rs1 ls1 rs2 ls2,
   agree rs1 ls1 -> agree rs2 ls2 ->
@@ -624,6 +625,140 @@ Proof.
   destruct (In_dec Loc.eq (R m) destroyed_at_call); auto.
   contradiction.
 Qed.
+**********)
+
+Lemma agree_find_funct:
+  forall (ge: Linear.genv) rs ls r f,
+  Genv.find_funct ge (rs r) = Some f ->
+  agree rs ls ->
+  loc_acceptable r ->
+  Genv.find_funct ge (ls r) = Some f.
+Proof.
+  intros. 
+  assert (Val.lessdef (rs r) (ls r)). eapply agree_loc; eauto.
+  exploit Genv.find_funct_inv; eauto. intros [b EQ]. rewrite EQ in H2.
+  inv H2. rewrite <- EQ. auto.
+Qed.
+
+Lemma agree_postcall_1:
+  forall rs ls,
+  agree rs ls ->
+  agree (LTL.postcall_regs rs) ls.
+Proof.
+  intros; red; intros. unfold LTL.postcall_regs.
+  destruct l; auto. 
+  destruct (In_dec Loc.eq (R m) temporaries). constructor.
+  destruct (In_dec Loc.eq (R m) destroyed_at_call). constructor.
+  auto.
+Qed.
+
+Lemma agree_postcall_2:
+  forall rs ls ls',
+  agree (LTL.postcall_regs rs) ls ->
+  (forall l, loc_acceptable l -> ~In l destroyed_at_call -> ~In l temporaries -> ls' l = ls l) ->
+  agree (LTL.postcall_regs rs) ls'.
+Proof.
+  intros; red; intros. generalize (H l H1). unfold LTL.postcall_regs. 
+  destruct l. 
+  destruct (In_dec Loc.eq (R m) temporaries). intro; constructor.
+  destruct (In_dec Loc.eq (R m) destroyed_at_call). intro; constructor.
+  intro. rewrite H0; auto. 
+  intro. rewrite H0; auto.
+  simpl. intuition congruence.
+  simpl. intuition congruence.
+Qed.
+
+Lemma agree_postcall_call:
+  forall rs ls ls' sig,
+  agree rs ls ->
+  (forall l, Loc.notin l (loc_arguments sig) -> Loc.notin l temporaries -> ls' l = ls l) ->
+  agree (LTL.postcall_regs rs) ls'.
+Proof.
+  intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto.
+  intros. apply H0.
+  apply arguments_not_preserved; auto.
+  destruct l; simpl. simpl in H2. intuition congruence. 
+  destruct s; tauto.
+  apply temporaries_not_acceptable; auto.
+Qed.
+
+Lemma agree_postcall_alloc:
+  forall rs ls ls2 v,
+  agree rs ls ->
+  (forall l, Loc.diff (R loc_alloc_argument) l -> ls2 l = ls l) ->
+  agree (LTL.postcall_regs rs) (Locmap.set (R loc_alloc_result) v ls2).
+Proof.
+  intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto.
+  intros. destruct (Loc.eq l (R loc_alloc_result)).
+  subst l. elim H2. simpl. tauto. 
+  rewrite Locmap.gso. apply H0.
+  red. destruct l; auto. red; intro. subst m. elim H2.
+  simpl. tauto.
+  apply Loc.diff_sym. apply loc_acceptable_noteq_diff; auto. 
+Qed.
+
+Lemma agree_init_locs:
+  forall ls dsts vl,
+  locs_acceptable dsts ->
+  Loc.norepet dsts ->
+  Val.lessdef_list vl (map ls dsts) ->
+  agree (LTL.init_locs vl dsts) ls.
+Proof.
+  induction dsts; intros; simpl.
+  red; intros. unfold Locmap.init. constructor.
+  simpl in H1. inv H1. inv H0. 
+  apply agree_set with ls. apply H; auto with coqlib. auto. auto.
+  apply IHdsts; auto. red; intros; apply H; auto with coqlib.
+Qed.
+
+Lemma call_regs_parameters:
+  forall ls sig,
+  map (call_regs ls) (loc_parameters sig) =
+  map ls (loc_arguments sig).
+Proof.
+  intros. unfold loc_parameters. rewrite list_map_compose. 
+  apply list_map_exten; intros. 
+  unfold call_regs, parameter_of_argument. 
+  generalize (loc_arguments_acceptable _ _ H). 
+  unfold loc_argument_acceptable. 
+  destruct x. auto.
+  destruct s; intros; try contradiction. auto.
+Qed. 
+
+Lemma return_regs_arguments:
+  forall ls1 ls2 sig,
+  tailcall_possible sig ->
+  map (return_regs ls1 ls2) (loc_arguments sig) = map ls2 (loc_arguments sig).
+Proof.
+  intros. symmetry. apply list_map_exten; intros.
+  unfold return_regs. generalize (H x H0). destruct x; intros.
+  destruct (In_dec Loc.eq (R m) temporaries). auto.
+  destruct (In_dec Loc.eq (R m) destroyed_at_call). auto.
+  elim n0. eapply arguments_caller_save; eauto.
+  contradiction.
+Qed.
+
+Lemma return_regs_result:
+  forall ls1 ls2 sig,
+  return_regs ls1 ls2 (R (loc_result sig)) = ls2 (R (loc_result sig)).
+Proof.
+  intros. unfold return_regs. 
+  destruct (In_dec Loc.eq (R (loc_result sig)) temporaries). auto.
+  destruct (In_dec Loc.eq (R (loc_result sig)) destroyed_at_call). auto.
+  elim n0. apply loc_result_caller_save.
+Qed.
+
+Lemma return_regs_preserve:
+  forall ls1 ls2 l,
+  ~ In l temporaries ->
+  ~ In l destroyed_at_call ->
+  return_regs ls1 ls2 l = ls1 l.
+Proof.
+  intros. unfold return_regs. destruct l; auto.
+  destruct (In_dec Loc.eq (R m) temporaries). contradiction.
+  destruct (In_dec Loc.eq (R m) destroyed_at_call). contradiction.
+  auto.
+Qed.
 
 (** * Preservation of labels and gotos *)
 
@@ -770,56 +905,63 @@ Qed.
   only acceptable locations are accessed by this code.
 *)
 
-Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> Prop :=
+Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> signature -> Prop :=
   | match_stackframes_nil:
-      match_stackframes nil nil
+      forall sig,
+      sig.(sig_res) = Some Tint ->
+      match_stackframes nil nil sig
   | match_stackframes_cons:
       forall res f sp c rs s s' c' ls sig,
-      match_stackframes s s' ->
-      sig_res (LTLin.fn_sig f) = sig_res (parent_callsig s) ->
+      match_stackframes s s' (LTLin.fn_sig f) ->
       c' = add_spill (loc_result sig) res (transf_code f c) ->      
-      agree rs ls ->
+      agree (LTL.postcall_regs rs) ls ->
       loc_acceptable res ->
       wt_function f ->
       is_tail c (LTLin.fn_code f) ->
-      match_stackframes (LTLin.Stackframe sig res f sp rs c :: s)
-                        (Linear.Stackframe (transf_function f) sp ls c' :: s').
+      match_stackframes (LTLin.Stackframe res f sp (LTL.postcall_regs rs) c :: s)
+                        (Linear.Stackframe (transf_function f) sp ls c' :: s')
+                        sig.
 
 Inductive match_states: LTLin.state -> Linear.state -> Prop :=
   | match_states_intro:
-      forall s f sp c rs m s' ls
-        (STACKS: match_stackframes s s')
-        (SIG: sig_res (LTLin.fn_sig f) = sig_res (parent_callsig s))
+      forall s f sp c rs m s' ls tm
+        (STACKS: match_stackframes s s' (LTLin.fn_sig f))
         (AG: agree rs ls)
         (WT: wt_function f)
-        (TL: is_tail c (LTLin.fn_code f)),
+        (TL: is_tail c (LTLin.fn_code f))
+        (MMD: Mem.lessdef m tm),
       match_states (LTLin.State s f sp c rs m)
-                   (Linear.State s' (transf_function f) sp (transf_code f c) ls m)
+                   (Linear.State s' (transf_function f) sp (transf_code f c) ls tm)
   | match_states_call:
-      forall s f rs m s' ls
-        (STACKS: match_stackframes s s')
-        (SIG: sig_res (LTLin.funsig f) = sig_res (parent_callsig s))
-        (AG: agree_arguments (LTLin.funsig f) rs ls)
-        (WT: wt_fundef f),
-      match_states (LTLin.Callstate s f rs m)
-                   (Linear.Callstate s' (transf_fundef f) ls m)
+      forall s f args m s' ls tm
+        (STACKS: match_stackframes s s' (LTLin.funsig f))
+        (AG: Val.lessdef_list args (map ls (Conventions.loc_arguments (LTLin.funsig f))))
+        (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call ->
+                 ls l = parent_locset s' l)
+        (WT: wt_fundef f)
+        (MMD: Mem.lessdef m tm),
+      match_states (LTLin.Callstate s f args m)
+                   (Linear.Callstate s' (transf_fundef f) ls tm)
   | match_states_return:
-      forall s rs m s' ls
-        (STACKS: match_stackframes s s')
-        (AG: agree rs ls),
-      match_states (LTLin.Returnstate s rs m)
-                   (Linear.Returnstate s' ls m).
-
-Remark parent_locset_match:
-  forall s s',
-  match_stackframes s s' ->
-  agree (LTLin.parent_locset s) (parent_locset s').
+      forall s res m s' ls tm sig
+        (STACKS: match_stackframes s s' sig)
+        (AG: Val.lessdef res (ls (R (Conventions.loc_result sig))))
+        (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call ->
+                 ls l = parent_locset s' l)
+        (MMD: Mem.lessdef m tm),
+      match_states (LTLin.Returnstate s res m)
+                   (Linear.Returnstate s' ls tm).
+
+Lemma match_stackframes_change_sig:
+  forall s s' sig1 sig2,
+  match_stackframes s s' sig1 ->
+  sig2.(sig_res) = sig1.(sig_res) ->
+  match_stackframes s s' sig2.
 Proof.
-  induction 1; simpl.
-  red; intros; auto.
-  auto.
+  intros. inv H. constructor. congruence.
+  econstructor; eauto. unfold loc_result. rewrite H0. auto.
 Qed.
-         
+
 Ltac ExploitWT :=
   match goal with
   | [ WT: wt_function _, TL: is_tail _ _ |- _ ] =>
@@ -850,6 +992,8 @@ Definition measure (st: LTLin.state) : nat :=
   | LTLin.Returnstate s ls m => 0%nat
   end.
 
+Axiom ADMITTED: forall (P: Prop), P.
+
 Theorem transf_step_correct:
   forall s1 t s2, LTLin.step ge s1 t s2 ->
   forall s1' (MS: match_states s1 s1'),
@@ -863,18 +1007,18 @@ Proof.
   ExploitWT. inv WTI. 
   (* move *)
   simpl.
-  destruct (add_move_correct tge s' (transf_function f) sp r1 res (transf_code f b) ls m)
+  destruct (add_move_correct tge s' (transf_function f) sp r1 res (transf_code f b) ls tm)
         as [ls2 [A [B C]]].
   inv A. 
   right. split. omega. split. auto.
   rewrite H1. rewrite H1. econstructor; eauto with coqlib. 
-  apply agree_set with ls2; auto.
+  apply agree_set with ls2; auto. 
   rewrite B. simpl in H; inversion H. auto.
   left; econstructor; split. eapply plus_left; eauto. 
   econstructor; eauto with coqlib. 
   apply agree_set with ls; auto.
   rewrite B. simpl in H; inversion H. auto.
-  intros. simpl in H1. apply C. apply Loc.diff_sym; auto.
+  intros. apply C. apply Loc.diff_sym; auto.
   simpl in H7; tauto. simpl in H7; tauto.
   (* other ops *)
   assert (is_move_operation op args = None).
@@ -885,18 +1029,22 @@ Proof.
   exploit add_reloads_correct. 
     eapply length_op_args; eauto.
     apply locs_acceptable_disj_temporaries; auto.
-  intros [ls2 [A [B C]]].
+  intros [ls2 [A [B C]]]. instantiate (1 := ls) in B. 
+  assert (exists tv, eval_operation tge sp op (reglist ls2 (regs_for args)) tm = Some tv
+                     /\ Val.lessdef v tv).
+    apply eval_operation_lessdef with m (map rs args); auto.
+    rewrite B. eapply agree_locs; eauto. 
+    rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
+  destruct H1 as [tv [P Q]].
   exploit add_spill_correct.
   intros [ls3 [D [E F]]].
   left; econstructor; split.
   eapply star_plus_trans. eexact A. 
-  eapply plus_left. eapply exec_Lop with (v := v).
-    rewrite <- H. rewrite B. rewrite (agree_locs _ _ _ AG H5). 
-    apply eval_operation_preserved. exact symbols_preserved.
+  eapply plus_left. eapply exec_Lop with (v := tv); eauto.
   eexact D. eauto. traceEq.
   econstructor; eauto with coqlib.
   apply agree_set with ls; auto.
-  rewrite E. apply Locmap.gss.
+  rewrite E. rewrite Locmap.gss. auto.
   intros. rewrite F; auto. rewrite Locmap.gso. auto. 
   apply reg_for_diff; auto.
 
@@ -906,17 +1054,23 @@ Proof.
     apply le_S. eapply length_addr_args; eauto.
     apply locs_acceptable_disj_temporaries; auto.
   intros [ls2 [A [B C]]].
+  assert (exists ta, eval_addressing tge sp addr (reglist ls2 (regs_for args)) = Some ta
+                     /\ Val.lessdef a ta).
+    apply eval_addressing_lessdef with (map rs args); auto.
+    rewrite B. eapply agree_locs; eauto. 
+    rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+  destruct H1 as [ta [P Q]].
+  exploit Mem.loadv_lessdef; eauto. 
+  intros [tv [R S]].
   exploit add_spill_correct.
   intros [ls3 [D [E F]]].
   left; econstructor; split.
   eapply star_plus_trans. eauto. 
   eapply plus_left. eapply exec_Lload; eauto.
-    rewrite B. rewrite <- H. rewrite (agree_locs _ _ _ AG H7).
-    apply eval_addressing_preserved. exact symbols_preserved.
   eauto. auto. traceEq.
   econstructor; eauto with coqlib.
   apply agree_set with ls; auto.
-  rewrite E. apply Locmap.gss.
+  rewrite E. rewrite Locmap.gss. auto.
   intros. rewrite F; auto. rewrite Locmap.gso. auto. 
   apply reg_for_diff; auto.
 
@@ -936,20 +1090,25 @@ Proof.
   intros [ls2 [A [B C]]]. rewrite EQ in A. rewrite EQ in B.
   injection B. intros D E. 
   simpl in B.
+  assert (exists ta, eval_addressing tge sp addr (reglist ls2 rargs) = Some ta
+                     /\ Val.lessdef a ta).
+    apply eval_addressing_lessdef with (map rs args); auto.
+    rewrite D. eapply agree_locs; eauto. 
+    rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+  destruct H2 as [ta [P Q]].
+  assert (X: Val.lessdef (rs src) (ls2 (R rsrc))).
+    rewrite E. eapply agree_loc; eauto.
+  exploit Mem.storev_lessdef. eexact MMD. eexact Q. eexact X. eauto. 
+  intros [tm2 [Y Z]].
   left; econstructor; split. 
   eapply plus_right. eauto. 
-  eapply exec_Lstore with (a := a); eauto.
-    rewrite D. rewrite <- H. rewrite (agree_locs _ _ _ AG H7).
-    apply eval_addressing_preserved. exact symbols_preserved.
-  rewrite E. rewrite (agree_loc _ _ _ AG H8). eauto.
+  eapply exec_Lstore with (a := ta); eauto.
   traceEq.
   econstructor; eauto with coqlib.
   apply agree_exten with ls; auto.
 
   (* Lcall *)
-  inversion MS. subst s0 f0 sp0 c rs0 m0.
-  simpl transf_code.
-  ExploitWT. inversion WTI. subst sig0 ros0 args0 res0.
+  ExploitWT. inversion WTI. subst ros0 args0 res0. rewrite <- H0.  
   assert (WTF': wt_fundef f'). eapply find_function_wt; eauto.
   destruct ros as [fn | id].
   (* indirect call *)
@@ -957,44 +1116,41 @@ Proof.
               (parallel_move args (loc_arguments sig)
                 (Lcall sig (inl ident IT3)
                  :: add_spill (loc_result sig) res (transf_code f b)))
-              ls m)
+              ls tm)
   as [ls2 [A [B C]]].
+  rewrite <- H0 in H5.
   destruct (parallel_move_arguments_correct tge s' (transf_function f) sp 
               args sig
               (Lcall sig (inl ident IT3)
                 :: add_spill (loc_result sig) res (transf_code f b))
-              ls2 m H7 H10)
+              ls2 tm H5 H8)
   as [ls3 [D [E [F G]]]].
-  assert (AG_ARGS: agree_arguments (LTLin.funsig f') rs1 ls3).
-    rewrite <- H0.
-    unfold rs1. apply agree_set_arguments with ls; auto.
-    rewrite E. apply list_map_exten; intros. symmetry. apply C.
-    assert (Loc.notin x temporaries). apply temporaries_not_acceptable; auto.
-    simpl in H3. apply Loc.diff_sym. tauto.
-    intros. rewrite G; auto. apply C. 
-    simpl in H3. apply Loc.diff_sym. tauto.
+  assert (ARGS: Val.lessdef_list (map rs args) 
+                                 (map ls3 (loc_arguments sig))).
+    rewrite E. apply agree_locs. apply agree_exten with ls; auto.
+    intros. apply C. simpl in H1. apply Loc.diff_sym. tauto. auto. 
   left; econstructor; split.
-  eapply star_plus_trans. eauto. eapply plus_right. eauto. 
+  eapply star_plus_trans. eexact A. eapply plus_right. eexact D. 
   eapply exec_Lcall; eauto.
-    simpl. rewrite F. rewrite B. 
-    rewrite (agree_loc rs ls fn); auto.
+    simpl. rewrite F. rewrite B. eapply agree_find_funct; eauto. 
     apply functions_translated. eauto.
     rewrite H0; symmetry; apply sig_preserved.
   eauto. traceEq.
   econstructor; eauto. 
-  econstructor; eauto with coqlib.
-  eapply agree_arguments_agree; eauto.
-  simpl. congruence. 
+  econstructor; eauto with coqlib. rewrite H0; auto.
+  apply agree_postcall_call with ls sig; auto. 
+  intros. rewrite G; auto. apply C. simpl in H2. apply Loc.diff_sym. tauto.
+  congruence.
   (* direct call *)
+  rewrite <- H0 in H5.
   destruct (parallel_move_arguments_correct tge s' (transf_function f) sp
               args sig
               (Lcall sig (inr mreg id)
                 :: add_spill (loc_result sig) res (transf_code f b))
-              ls m H7 H10)
+              ls tm H5 H8)
   as [ls3 [D [E [F G]]]].
-  assert (AG_ARGS: agree_arguments (LTLin.funsig f') rs1 ls3).
-    rewrite <- H0.
-    unfold rs1. apply agree_set_arguments with ls; auto.
+  assert (ARGS: Val.lessdef_list (map rs args) (map ls3 (loc_arguments sig))).
+    rewrite E. apply agree_locs; auto.
   left; econstructor; split.
   eapply plus_right. eauto.
   eapply exec_Lcall; eauto.
@@ -1004,58 +1160,53 @@ Proof.
     rewrite H0. symmetry; apply sig_preserved.
   traceEq.
   econstructor; eauto.
-  econstructor; eauto with coqlib.
-  eapply agree_arguments_agree; eauto.
-  simpl; congruence.
+  econstructor; eauto with coqlib. rewrite H0; auto. 
+  apply agree_postcall_call with ls sig; auto.
+  congruence.
 
   (* Ltailcall *)
-  inversion MS. subst s0 f0 sp c rs0 m0 s1'.
-  simpl transf_code.
-  ExploitWT. inversion WTI. subst sig0 ros0 args0.
+  ExploitWT. inversion WTI. subst ros0 args0.
   assert (WTF': wt_fundef f'). eapply find_function_wt; eauto.
+  rewrite <- H0.
   destruct ros as [fn | id].
   (* indirect call *)
   destruct (add_reload_correct tge s' (transf_function f) (Vptr stk Int.zero) fn IT3
               (parallel_move args (loc_arguments sig)
                 (Ltailcall sig (inl ident IT3) :: transf_code f b))
-              ls m)
+              ls tm)
   as [ls2 [A [B C]]].
+  rewrite <- H0 in H4.
   destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero)
               args sig
               (Ltailcall sig (inl ident IT3) :: transf_code f b)
-              ls2 m H5 H7)
+              ls2 tm H4 H6)
   as [ls3 [D [E [F G]]]].
-  assert (AG_ARGS: agree_arguments (LTLin.funsig f') rs2 (LTL.return_regs (parent_locset s') ls3)).
-    rewrite <- H0. unfold rs2. 
-    apply agree_arguments_return_regs; auto.
-    eapply parent_locset_match; eauto.  
-    unfold rs1. apply agree_set_arguments with ls; auto.
-    rewrite E. apply list_map_exten; intros. symmetry. apply C.
-    assert (Loc.notin x temporaries). apply temporaries_not_acceptable; auto.
-    simpl in H2. apply Loc.diff_sym. tauto.
-    intros. rewrite G; auto. apply C. 
-    simpl in H2. apply Loc.diff_sym. tauto.
+  assert (ARGS: Val.lessdef_list (map rs args) 
+                                 (map ls3 (loc_arguments sig))).
+    rewrite E. apply agree_locs. apply agree_exten with ls; auto.
+    intros. apply C. simpl in H1. apply Loc.diff_sym. tauto. auto. 
   left; econstructor; split.
   eapply star_plus_trans. eauto. eapply plus_right. eauto.
   eapply exec_Ltailcall; eauto.
-    simpl. rewrite F. rewrite B. 
-    rewrite (agree_loc rs ls fn); auto.
+    simpl. rewrite F. rewrite B. eapply agree_find_funct; eauto. 
     apply functions_translated. eauto.
     rewrite H0; symmetry; apply sig_preserved.
   eauto. traceEq.
-  econstructor; eauto. congruence. 
- 
+  econstructor; eauto. 
+  eapply match_stackframes_change_sig; eauto.
+  rewrite return_regs_arguments; auto. congruence.
+  exact (return_regs_preserve (parent_locset s') ls3).
+  apply Mem.free_lessdef; auto. 
   (* direct call *)
+  rewrite <- H0 in H4.
   destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero)
               args sig
               (Ltailcall sig (inr mreg id) :: transf_code f b)
-              ls m H5 H7)
+              ls tm H4 H6)
   as [ls3 [D [E [F G]]]].
-  assert (AG_ARGS: agree_arguments (LTLin.funsig f') rs2 (LTL.return_regs (parent_locset s') ls3)).
-    rewrite <- H0. unfold rs2. 
-    apply agree_arguments_return_regs; auto.
-    eapply parent_locset_match; eauto.  
-    unfold rs1. apply agree_set_arguments with ls; auto.
+  assert (ARGS: Val.lessdef_list (map rs args) 
+                                 (map ls3 (loc_arguments sig))).
+    rewrite E. apply agree_locs. apply agree_exten with ls; auto. auto.
   left; econstructor; split.
   eapply plus_right. eauto.
   eapply exec_Ltailcall; eauto.
@@ -1064,28 +1215,33 @@ Proof.
     apply function_ptr_translated; auto. congruence.
     rewrite H0. symmetry; apply sig_preserved.
   traceEq.
-  econstructor; eauto. congruence.
+  econstructor; eauto.
+  eapply match_stackframes_change_sig; eauto.
+  rewrite return_regs_arguments; auto. congruence.
+  exact (return_regs_preserve (parent_locset s') ls3).
+  apply Mem.free_lessdef; auto. 
 
   (* Lalloc *)
   ExploitWT; inv WTI.
+  caseEq (alloc tm 0 (Int.signed sz)). intros tm' blk' TALLOC.
+  assert (blk = blk' /\ Mem.lessdef m' tm'). 
+    eapply Mem.alloc_lessdef; eauto.
   exploit add_reload_correct. intros [ls2 [A [B C]]]. 
   exploit add_spill_correct. intros [ls3 [D [E F]]].
+  destruct H1 as [P Q]. subst blk'. 
+  assert (ls arg = Vint sz).
+    assert (Val.lessdef (rs arg) (ls arg)). eapply agree_loc; eauto. 
+    rewrite H in H1; inversion H1; auto.
   left; econstructor; split.
   eapply star_plus_trans. eauto. 
   eapply plus_left. eapply exec_Lalloc; eauto.
-    rewrite B. rewrite <- H. apply AG. auto.
+    rewrite B. eauto. 
   eauto. eauto. traceEq.
   econstructor; eauto with coqlib.
-  unfold rs3; apply agree_set with (Locmap.set (R loc_alloc_result) (Vptr blk Int.zero) ls2).
-  auto. rewrite E. rewrite Locmap.gss. 
-  unfold rs2; rewrite Locmap.gss. auto.
-  auto.
-  unfold rs2. apply agree_set with ls2.
-  unfold loc_alloc_result; simpl; intuition congruence.
-  apply Locmap.gss. intros. apply Locmap.gso; auto.
-  unfold rs1. apply agree_set with ls.
-  unfold loc_alloc_argument; simpl; intuition congruence.
-  rewrite B. apply AG; auto. auto. auto.
+  apply agree_set with (Locmap.set (R loc_alloc_result) (Vptr blk Int.zero) ls2).
+  auto. rewrite E. rewrite Locmap.gss. constructor. 
+  auto. 
+  apply agree_postcall_alloc with ls; auto. 
 
   (* Llabel *)
   left; econstructor; split.
@@ -1106,7 +1262,8 @@ Proof.
   intros [ls2 [A [B C]]].
   left; econstructor; split.
   eapply plus_right. eauto. eapply exec_Lcond_true; eauto.
-  rewrite B. rewrite (agree_locs _ _ _ AG H5). auto.
+  rewrite B. apply eval_condition_lessdef with m (map rs args); auto.
+  eapply agree_locs; eauto. 
   apply find_label_transf_function; eauto.
   traceEq.
   econstructor; eauto.
@@ -1121,44 +1278,44 @@ Proof.
   intros [ls2 [A [B C]]].
   left; econstructor; split.
   eapply plus_right. eauto. eapply exec_Lcond_false; eauto.
-  rewrite B. rewrite (agree_locs _ _ _ AG H4). auto.
+  rewrite B. apply eval_condition_lessdef with m (map rs args); auto.
+  eapply agree_locs; eauto. 
   traceEq.
   econstructor; eauto with coqlib.
   apply agree_exten with ls; auto.
 
   (* Lreturn *)
   ExploitWT; inv WTI. 
-  unfold rs2, rs1; destruct or; simpl.
+  destruct or; simpl.
   (* with an argument *)
   exploit add_reload_correct.
   intros [ls2 [A [B C]]].
   left; econstructor; split.
   eapply plus_right. eauto. eapply exec_Lreturn; eauto. 
   traceEq.
-  econstructor; eauto. 
-  apply agree_return_regs; auto.
-  eapply parent_locset_match; eauto.
-  apply agree_set with ls. 
-  apply loc_result_acceptable.
-  rewrite B. eapply agree_loc; eauto.
-  auto. auto.
+  econstructor; eauto.
+  rewrite return_regs_result. rewrite B. apply agree_loc; auto.
+  apply return_regs_preserve.
+  apply Mem.free_lessdef; auto.
   (* without an argument *)
   left; econstructor; split.
   apply plus_one. eapply exec_Lreturn; eauto.  
   econstructor; eauto.
-  apply agree_return_regs; auto.
-  eapply parent_locset_match; eauto.
+  apply return_regs_preserve.
+  apply Mem.free_lessdef; auto.
 
   (* internal function *)
   simpl in WT. inversion_clear WT. inversion H0. simpl in AG.
+  caseEq (alloc tm 0 (LTLin.fn_stacksize f)). intros tm' tstk TALLOC.
+  exploit Mem.alloc_lessdef; eauto. intros [P Q]. subst tstk.
   destruct (parallel_move_parameters_correct tge s' (transf_function f)
                (Vptr stk Int.zero) (LTLin.fn_params f) (LTLin.fn_sig f)
-               (transf_code f (LTLin.fn_code f)) (LTL.call_regs ls) m'
+               (transf_code f (LTLin.fn_code f)) (call_regs ls) tm'
                wt_params wt_acceptable wt_norepet)
   as [ls2 [A [B [C D]]]].
-  assert (AG2: agree rs2 ls2).
-    unfold rs2. eapply agree_set_parameters; eauto.
-    unfold rs1. apply agree_call_regs; auto.
+  assert (AG2: agree (LTL.init_locs args (fn_params f)) ls2).
+    apply agree_init_locs; auto.
+    rewrite B. rewrite call_regs_parameters. auto. 
   left; econstructor; split.
   eapply plus_left.
   eapply exec_function_internal; eauto.
@@ -1166,15 +1323,14 @@ Proof.
   econstructor; eauto with coqlib.
 
   (* external function *)
+  exploit event_match_lessdef; eauto. 
+  intros [res' [A B]]. 
   left; econstructor; split.
   apply plus_one. eapply exec_function_external; eauto. 
-  unfold args. symmetry. eapply agree_arguments_locs; auto.
   econstructor; eauto.
-  unfold rs1. apply agree_set with ls; auto. 
-  apply loc_result_acceptable.
-  apply Locmap.gss.
-  intros. apply Locmap.gso; auto.
-  eapply agree_arguments_agree; eauto.
+  simpl. rewrite Locmap.gss. auto.
+  intros. rewrite Locmap.gso. auto. 
+  simpl. destruct l; auto. red; intro. elim H1. subst m0. apply loc_result_caller_save.
 
   (* return *)
   inv STACKS. 
@@ -1183,8 +1339,10 @@ Proof.
   eapply plus_left. eapply exec_return; eauto.
   eauto. traceEq.
   econstructor; eauto. 
-  unfold rs1. apply agree_set with ls; auto.
-  rewrite B. apply AG. apply loc_result_acceptable. 
+  apply agree_set with ls; auto.
+  rewrite B. auto.
+  unfold parent_locset in PRES.
+  apply agree_postcall_2 with ls0; auto. 
 Qed.
 
 Lemma transf_initial_states:
@@ -1200,9 +1358,9 @@ Proof.
   rewrite sig_preserved. auto.
   replace (Genv.init_mem tprog) with (Genv.init_mem prog).  
   econstructor; eauto. constructor. rewrite H2; auto.
-  red; intros. auto.
+  rewrite H2. simpl. constructor.
   eapply Genv.find_funct_ptr_prop; eauto.
-  symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf; auto.
+  apply Mem.lessdef_refl. symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf; auto.
 Qed.
 
 Lemma transf_final_states:
@@ -1210,8 +1368,7 @@ Lemma transf_final_states:
   match_states st1 st2 -> LTLin.final_state st1 r -> Linear.final_state st2 r.
 Proof.
   intros. inv H0. inv H. inv STACKS. econstructor.
-  rewrite (agree_loc _ _ (R R3) AG). auto. 
-  simpl. intuition congruence.
+  unfold loc_result in AG. rewrite H in AG. inv AG. auto. 
 Qed.
 
 Theorem transf_program_correct:
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index 1759d7f..a9187ee 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -726,9 +726,9 @@ Lemma agree_return_regs:
   (forall r,
     In r int_callee_save_regs \/ In r float_callee_save_regs ->
     rs' r = ls0 (R r)) ->
-  (forall r, LTL.return_regs ls0 ls (R r) = rs' r).
+  (forall r, return_regs ls0 ls (R r) = rs' r).
 Proof.
-  intros; unfold LTL.return_regs.
+  intros; unfold return_regs.
   case (In_dec Loc.eq (R r) temporaries); intro.
   rewrite H0. eapply agree_reg; eauto. 
     apply int_callee_save_not_destroyed; auto.
@@ -778,10 +778,10 @@ Qed.
 
 Lemma agree_callee_save_return_regs:
   forall ls1 ls2,
-  agree_callee_save (LTL.return_regs ls1 ls2) ls1.
+  agree_callee_save (return_regs ls1 ls2) ls1.
 Proof.
   intros; red; intros.
-  unfold LTL.return_regs. destruct l; auto.
+  unfold return_regs. destruct l; auto.
   generalize (int_callee_save_not_destroyed m); intro.
   generalize (float_callee_save_not_destroyed m); intro.
   destruct (In_dec Loc.eq (R m) temporaries). tauto.
@@ -988,7 +988,7 @@ Lemma save_callee_save_correct:
     star step tge
        (State stack tf sp (save_callee_save fe k) rs empty_frame m)
     E0 (State stack tf sp k rs fr' m)
-  /\ agree (LTL.call_regs ls) ls rs fr' cs.
+  /\ agree (call_regs ls) ls rs fr' cs.
 Proof.
   intros. unfold save_callee_save.
   exploit save_callee_save_int_correct; eauto. 
@@ -997,7 +997,7 @@ Proof.
   intros [fr2 [A2 [B2 C2]]].
   exists fr2.
   split. eapply star_trans. eexact A1. eexact A2. traceEq.
-  constructor; unfold LTL.call_regs; auto.
+  constructor; unfold call_regs; auto.
   (* agree_local *)
   intros. rewrite C2; auto with stacking. 
   rewrite C1; auto with stacking. 
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index cb0a6d8..cefad10 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -190,10 +190,10 @@ Definition tunneled_code (f: function) :=
 
 Inductive match_stackframes: stackframe -> stackframe -> Prop :=
   | match_stackframes_intro:
-      forall sig res f sp ls0 pc,
+      forall res f sp ls0 pc,
       match_stackframes
-         (Stackframe sig res f sp ls0 pc)
-         (Stackframe sig res (tunnel_function f) sp ls0 (branch_target f pc)).
+         (Stackframe res f sp ls0 pc)
+         (Stackframe res (tunnel_function f) sp ls0 (branch_target f pc)).
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
@@ -212,12 +212,6 @@ Inductive match_states: state -> state -> Prop :=
       match_states (Returnstate s ls m)
                    (Returnstate ts ls m).
 
-Lemma parent_locset_match:
-  forall s ts, list_forall2 match_stackframes s ts -> parent_locset ts = parent_locset s.
-Proof.
-  induction 1; simpl; auto. inv H; auto.
-Qed.
-
 (** To preserve non-terminating behaviours, we show that the transformed
   code cannot take an infinity of "zero transition" cases.
   We use the following [measure] function over source states,
@@ -286,32 +280,27 @@ Proof.
   rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
   econstructor; eauto.
   (* Lcall *)
-  unfold rs1. inv MS. 
   left; econstructor; split. 
   eapply exec_Lcall with (f' := tunnel_fundef f'); eauto.
   rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
   rewrite (tunnel_function_lookup _ _ _ H); simpl.
   rewrite sig_preserved. auto.
   apply find_function_translated; auto.
-  rewrite sig_preserved; auto. fold rs1. 
   econstructor; eauto.
   constructor; auto. 
   constructor; auto.
   (* Ltailcall *)
-  unfold rs2, rs1 in *. inv MS. fold rs1. fold rs2. 
   left; econstructor; split. 
   eapply exec_Ltailcall with (f' := tunnel_fundef f'); eauto.
   rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
   rewrite (tunnel_function_lookup _ _ _ H); simpl.
   rewrite sig_preserved. auto.
   apply find_function_translated; auto.
-  rewrite sig_preserved; auto. fold rs1. 
-  rewrite (parent_locset_match _ _ H9).
   econstructor; eauto.
   (* Lalloc *)
   rewrite (branch_target_identity f pc); [idtac | rewrite H; auto].
-  left; exists (State ts (tunnel_function f) sp (branch_target f pc') rs3 m'); split.
-  unfold rs3, rs2, rs1; eapply exec_Lalloc; eauto.
+  left; exists (State ts (tunnel_function f) sp (branch_target f pc') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_regs rs)) m'); split.
+  eapply exec_Lalloc; eauto.
   rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.
   econstructor; eauto.
   (* cond *)
@@ -330,7 +319,7 @@ Proof.
   left; econstructor; split.
   eapply exec_Lreturn; eauto.
   rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto.
-  simpl. rewrite (parent_locset_match _ _ H7). constructor; auto.
+  simpl. constructor; auto.
   (* internal function *)
   simpl. left; econstructor; split.
   eapply exec_function_internal; eauto.
@@ -343,7 +332,7 @@ Proof.
   inv H3. inv H1.
   left; econstructor; split.
   eapply exec_return; eauto.
-  fold rs1. constructor. auto.
+  constructor. auto.
 Qed.
 
 Lemma transf_initial_states:
@@ -351,7 +340,7 @@ Lemma transf_initial_states:
   exists st2, initial_state tp st2 /\ match_states st1 st2.
 Proof.
   intros. inversion H. 
-  exists (Callstate nil (tunnel_fundef f) (Locmap.init Vundef) (Genv.init_mem tp)); split.
+  exists (Callstate nil (tunnel_fundef f) nil (Genv.init_mem tp)); split.
   econstructor; eauto.
   change (prog_main tp) with (prog_main p).
   rewrite symbols_preserved. eauto.
@@ -366,7 +355,7 @@ Lemma transf_final_states:
   forall st1 st2 r, 
   match_states st1 st2 -> final_state st1 r -> final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv H5. constructor. auto. 
+  intros. inv H0. inv H. inv H4. constructor.  
 Qed.
 
 Theorem transf_program_correct: