MAJ documentation

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

7 files changed, 111 insertions, 362 deletions

diff --git a/.depend b/.depend
index cf24f7f..bc2750a 100644
--- a/.depend
+++ b/.depend
@@ -20,7 +20,7 @@ backend/Cminor.vo: backend/Cminor.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/
 backend/Op.vo: backend/Op.v lib/Coqlib.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo
 backend/CminorSel.vo: backend/CminorSel.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Events.vo common/Values.vo common/Mem.vo backend/Cminor.vo backend/Op.vo common/Globalenvs.vo common/Switch.vo common/Smallstep.vo
 backend/Selection.vo: backend/Selection.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Globalenvs.vo backend/Cminor.vo backend/Op.vo backend/CminorSel.vo
-backend/Selectionproof.vo: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo backend/Cminor.vo backend/Op.vo backend/CminorSel.vo backend/Selection.vo
+backend/Selectionproof.vo: backend/Selectionproof.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Mem.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Cminor.vo backend/Op.vo backend/CminorSel.vo backend/Selection.vo
 backend/Registers.vo: backend/Registers.v lib/Coqlib.vo common/AST.vo lib/Maps.vo lib/Ordered.vo
 backend/RTL.vo: backend/RTL.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Events.vo common/Mem.vo common/Globalenvs.vo common/Smallstep.vo backend/Op.vo backend/Registers.vo
 backend/RTLgen.vo: backend/RTLgen.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Switch.vo backend/Op.vo backend/Registers.vo backend/CminorSel.vo backend/RTL.vo
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index fd569ad..58ed3b6 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -35,92 +35,6 @@ Require Import Coloring.
 Require Import Coloringproof.
 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. *)
-
-Lemma call_regs_param_of_arg:
-  forall sig ls l,
-  In l (loc_arguments sig) ->
-  LTL.call_regs ls (parameter_of_argument l) = ls l.
-Proof.
-  intros. 
-  generalize (loc_arguments_acceptable sig l H).
-  unfold LTL.call_regs; unfold parameter_of_argument.
-  unfold loc_argument_acceptable.
-  destruct l. auto. destruct s; tauto.
-Qed.
-
-(** The return value, stored in the conventional return register,
-  is correctly passed from the callee back to the caller. *)
-
-Lemma return_regs_result:
-  forall sig caller callee,
-  LTL.return_regs caller callee (R (loc_result sig)) =
-    callee (R (loc_result sig)).
-Proof.
-  intros. unfold LTL.return_regs.
-  case (In_dec Loc.eq (R (loc_result sig)) temporaries); intro.
-  auto.
-  case (In_dec Loc.eq (R (loc_result sig)) destroyed_at_call); intro.
-  auto.
-  elim n0. apply loc_result_caller_save.
-Qed.
-
-(** Function arguments for a tail call are preserved by a
-    [return_regs] operation. *)
-
-Lemma return_regs_arguments:
-  forall sig caller callee,
-  tailcall_possible sig ->
-  map (LTL.return_regs caller callee) (loc_arguments sig) =
-  map callee (loc_arguments sig).
-Proof.
-  intros. apply list_map_exten; intros.
-  generalize (H x H0). destruct x; intro.
-  unfold LTL.return_regs.
-  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. 
-
-(** Acceptable locations that are not destroyed at call keep
-  their values across a call. *)
-
-Lemma return_regs_not_destroyed:
-  forall caller callee l,
-  Loc.notin l destroyed_at_call -> loc_acceptable l ->
-  LTL.return_regs caller callee l = caller l.
-Proof.
-  unfold loc_acceptable, LTL.return_regs.
-  destruct l; auto.
-  intros. case (In_dec Loc.eq (R m) temporaries); intro.
-  contradiction.
-  case (In_dec Loc.eq (R m) destroyed_at_call); intro.
-  elim (Loc.notin_not_in _ _ H i). 
-  auto.
-Qed.
-
-(** Characterization of parallel assignments. *)
-
-Lemma parmov_spec:
-  forall ls srcs dsts,
-  Loc.norepet dsts -> List.length srcs = List.length dsts ->
-  List.map (LTL.parmov srcs dsts ls) dsts = List.map ls srcs /\
-  (forall l, Loc.notin l dsts -> LTL.parmov srcs dsts ls l = ls l).
-Proof.
-  induction srcs; destruct dsts; simpl; intros; try discriminate.
-  auto.
-  inv H. inv H0. destruct (IHsrcs _ H4 H1). split.
-  f_equal. apply Locmap.gss. rewrite <- H. apply list_map_exten; intros.
-  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 *)
 
 (** We list here various properties of the locations [alloc r],
@@ -256,9 +170,8 @@ Proof.
   red; intros. elim (Regset.empty_1 _ H4).
   unfold RTL.successors in H0; rewrite H2 in H0; elim H0.
 Qed.
-

-(** Some useful special cases of [agree_increasing]. *)
 
+(** Some useful special cases of [agree_increasing]. *)
 
 Lemma agree_reg_live:
   forall r live rs ls,
@@ -423,7 +336,7 @@ Lemma agree_postcall:
   (forall r,
     Regset.In r live -> r <> res -> assign r <> assign res) ->
   agree (reg_list_live args (reg_sum_live ros (reg_dead res live))) rs ls ->
-  agree live (rs#res <- v) (Locmap.set (assign res) v (postcall_regs ls)).
+  agree live (rs#res <- v) (Locmap.set (assign res) v (postcall_locs ls)).
 Proof.
   intros. 
   assert (agree (reg_dead res live) rs ls).
@@ -433,7 +346,7 @@ Proof.
   subst r. rewrite Locmap.gss. auto.
   rewrite Locmap.gso. transitivity (ls (assign r)). 
   apply H2. apply Regset.remove_2; auto. 
-  unfold postcall_regs.
+  unfold postcall_locs.
   assert (~In (assign r) temporaries).
     apply Loc.notin_not_in. eapply regalloc_not_temporary; eauto.
   assert (~In (assign r) destroyed_at_call).
diff --git a/backend/LTL.v b/backend/LTL.v
index e39a4ec..6ee07f7 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -84,25 +84,12 @@ Fixpoint init_locs (vl: list val) (rl: list loc) {struct rl} : locset :=
   | _, _ => Locmap.init Vundef
   end.
 
-
-Section RELSEM.
-
-(** [parmov srcs dsts ls] performs the parallel assignment
-  of locations [dsts] to the values of the corresponding locations
-  [srcs].  *)
-
-Fixpoint parmov (srcs dsts: list loc) (ls: locset) {struct srcs} : locset :=
-  match srcs, dsts with
-  | s1 :: sl, d1 :: dl => Locmap.set d1 (ls s1) (parmov sl dl ls)
-  | _, _ => ls
-  end.
-
-(** [postcall_regs ls] returns the location set [ls] after a function
+(** [postcall_locs 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 :=
+Definition postcall_locs (ls: locset) : locset :=
   fun (l: loc) =>
     match l with
     | R r =>
@@ -147,6 +134,9 @@ Inductive state : Set :=
              (m: mem),                (**r memory state *)
       state.
 
+
+Section RELSEM.
+
 Variable ge: genv.
 
 Definition find_function (los: loc + ident) (rs: locset) : option fundef :=
@@ -159,46 +149,12 @@ Definition find_function (los: loc + ident) (rs: locset) : option fundef :=
       end
   end.
 
-(** The main difference between the LTL transition relation
-  and the RTL transition relation is the handling of function calls.
-  In RTL, arguments and results to calls are transmitted via
-  [vargs] and [vres] components of [Callstate] and [Returnstate],
-  respectively.  The semantics takes care of transferring these values
-  between the pseudo-registers of the caller and of the callee.
-  
-  In lower-level intermediate languages (e.g [Linear], [Mach], [PPC]),
-  arguments and results are transmitted implicitly: the generated
-  code for the caller arranges for arguments to be left in conventional
-  registers and stack locations, as determined by the calling conventions,
-  where the function being called will find them.  Similarly,
-  conventional registers will be used to pass the result value back
-  to the caller.
-
-  In LTL, we take an hybrid view of argument and result passing.
-  The LTL code does not contain (yet) instructions for moving
-  arguments and results to the conventional registers.  However,
-  the dynamic semantics "goes through the motions" of such code:
-- The [exec_Lcall] transition from [State] to [Callstate]
-  leaves the values of arguments in the conventional locations
-  given by [loc_arguments].
-- The [exec_function_internal] transition from [Callstate] to [State]
-  changes the view of stack slots ([Outgoing] slots slide to
-  [Incoming] slots as per [call_regs]), then recovers the
-  values of parameters from the conventional locations given by
-  [loc_parameters].
-- The [exec_Lreturn] transition from [State] to [Returnstate]
-  moves the result value to the conventional location [loc_result],
-  then restores the values of callee-save locations from
-  the location state of the caller, using [return_regs].
-- The [exec_return] transition from [Returnstate] to [State]
-  reads the result value from the conventional location [loc_result],
-  then stores it in the result location for the [Lcall] instruction.
-
-This complicated protocol will make it much easier to prove
-the correctness of the [Stacking] pass later, which inserts actual
-code that performs all the shuffling of arguments and results
-described above.
-*)
+(** The LTL transition relation is very similar to that of RTL,
+  with locations being used in place of pseudo-registers.
+  The main difference is for the [call] instruction: caller-save
+  registers are set to [Vundef] across the call, using the [postcall_locs]
+  function defined above.  This forces the LTL producer to avoid
+  storing values live across the call in a caller-save register. *)
 
 Inductive step: state -> trace -> state -> Prop :=
   | exec_Lnop:
@@ -232,7 +188,7 @@ Inductive step: state -> trace -> state -> Prop :=
       find_function ros rs = Some f' ->
       funsig f' = sig ->
       step (State s f sp pc rs m)
-        E0 (Callstate (Stackframe res f sp (postcall_regs rs) pc' :: s)
+        E0 (Callstate (Stackframe res f sp (postcall_locs rs) pc' :: s)
                       f' (List.map rs args) m)
   | exec_Ltailcall:
       forall s f stk pc rs m sig ros args f',
@@ -247,7 +203,7 @@ Inductive step: state -> trace -> state -> Prop :=
       rs arg = Vint sz ->
       Mem.alloc m 0 (Int.signed sz) = (m', b) ->
       step (State s f sp pc rs m)
-        E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_regs rs)) m')
+        E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_locs 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) ->
diff --git a/backend/LTLin.v b/backend/LTLin.v
index 83787ce..fae6417 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -140,14 +140,6 @@ Inductive state : Set :=
              (m: mem),                (**r memory state *)
       state.
 
-(*
-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.
 
 Variable ge: genv.
@@ -185,7 +177,7 @@ Inductive step: state -> trace -> state -> Prop :=
       find_function ros rs = Some f' ->
       sig = funsig f' ->
       step (State s f sp (Lcall sig ros args res :: b) rs m)
-        E0 (Callstate (Stackframe res f sp (postcall_regs rs) b :: s)
+        E0 (Callstate (Stackframe res f sp (postcall_locs rs) b :: s)
                       f' (List.map rs args) m)
   | exec_Ltailcall:
       forall s f stk sig ros args b rs m f',
@@ -198,7 +190,7 @@ Inductive step: state -> trace -> state -> Prop :=
       rs arg = Vint sz ->
       Mem.alloc m 0 (Int.signed sz) = (m', blk) ->
       step (State s f sp (Lalloc arg res :: b) rs m)
-        E0 (State s f sp b (Locmap.set res (Vptr blk Int.zero) (postcall_regs rs)) m')
+        E0 (State s f sp b (Locmap.set res (Vptr blk Int.zero) (postcall_locs rs)) m')
   | exec_Llabel:
       forall s f sp lbl b rs m,
       step (State s f sp (Llabel lbl :: b) rs m)
diff --git a/backend/Linear.v b/backend/Linear.v
index ca1a2bc..900b6a5 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -202,6 +202,40 @@ Definition parent_locset (stack: list stackframe) : locset :=
   | Stackframe f sp ls c :: stack' => ls
   end.
 
+(** The main difference between the Linear transition relation
+  and the LTL transition relation is the handling of function calls.
+  In LTL, arguments and results to calls are transmitted via
+  [vargs] and [vres] components of [Callstate] and [Returnstate],
+  respectively.  The semantics takes care of transferring these values
+  between the locations of the caller and of the callee.
+  
+  In Linear and lower-level languages (Mach, PPC), arguments and
+  results are transmitted implicitly: the generated code for the
+  caller arranges for arguments to be left in conventional registers
+  and stack locations, as determined by the calling conventions, where
+  the function being called will find them.  Similarly, conventional
+  registers will be used to pass the result value back to the caller.
+  This is reflected in the definition of [Callstate] and [Returnstate] 
+  above, where a whole location state [rs] is passed instead of just
+  the values of arguments or returns as in LTL.
+
+  These location states passed across calls are treated in a way that
+  reflects the callee-save/caller-save convention:
+- The [exec_Lcall] transition from [State] to [Callstate]
+  saves the current location state [ls] in the call stack,
+  and passes it to the callee.
+- The [exec_function_internal] transition from [Callstate] to [State]
+  changes the view of stack slots ([Outgoing] slots slide to
+  [Incoming] slots as per [call_regs]).
+- The [exec_Lreturn] transition from [State] to [Returnstate]
+  restores the values of callee-save locations from
+  the location state of the caller, using [return_regs].
+
+This protocol makes it much easier to later prove the correctness of
+the [Stacking] pass, which inserts actual code that performs the
+saving and restoring of callee-save registers described above.
+*)
+
 Inductive step: state -> trace -> state -> Prop :=
   | exec_Lgetstack:
       forall s f sp sl r b rs m,
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 372a261..3177eaf 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -410,8 +410,19 @@ End LINEAR_CONSTRUCTORS.
 (** * Agreement between values of locations *)
 
 (** The predicate [agree] states that two location maps
-  give the same values to all acceptable locations,
-  that is, non-temporary registers and [Local] stack slots. *)
+  give compatible values to all acceptable locations,
+  that is, non-temporary registers and [Local] stack slots.
+  The notion of compatibility used is the [Val.lessdef] ordering,
+  which enables a [Vundef] value in the original program to be refined
+  into any value in the transformed program.  
+
+  A typical situation where this refinement of values occurs is at
+  function entry point.  In LTLin, all registers except those
+  belonging to the function parameters are set to [Vundef].  In
+  Linear, these registers have whatever value they had in the caller
+  function.  This difference is harmless: if the original LTLin code
+  does not get stuck, we know that it does not use any of these
+  [Vundef] values. *)
 
 Definition agree (rs1 rs2: locset) : Prop :=
   forall l, loc_acceptable l -> Val.lessdef (rs1 l) (rs2 l).
@@ -425,7 +436,8 @@ Qed.
 
 Lemma agree_locs:
   forall rs1 rs2 ll,
-  agree rs1 rs2 -> locs_acceptable ll -> Val.lessdef_list (map rs1 ll) (map rs2 ll).
+  agree rs1 rs2 -> locs_acceptable ll -> 
+  Val.lessdef_list (map rs1 ll) (map rs2 ll).
 Proof.
   induction ll; simpl; intros.
   constructor.
@@ -458,175 +470,6 @@ Proof.
   apply temporaries_not_acceptable; auto. 
 Qed.
 
-(*****
-Lemma agree_return_regs:
-  forall rs1 ls1 rs2 ls2,
-  agree rs1 ls1 -> agree rs2 ls2 ->
-  agree (LTL.return_regs rs1 rs2) (LTL.return_regs ls1 ls2).
-Proof.
-  intros; red; intros. unfold LTL.return_regs.
-  assert (~In l temporaries). 
-  apply Loc.notin_not_in. apply temporaries_not_acceptable; auto.
-  destruct l.
-  destruct (In_dec Loc.eq (R m) temporaries). contradiction.
-  destruct (In_dec Loc.eq (R m) destroyed_at_call); auto.
-  auto.
-Qed.
-
-Lemma agree_set_result:
-  forall rs1 ls1 rs2 ls2 sig res ls3,
-  loc_acceptable res -> agree rs1 ls1 -> agree rs2 ls2 ->
-  ls3 res = LTL.return_regs ls1 ls2 (R (loc_result sig)) ->
-  (forall l : loc, Loc.diff res l -> ls3 l = LTL.return_regs ls1 ls2 l) ->
-  let rs_merge := LTL.return_regs rs1 rs2 in
-  agree (Locmap.set res (rs_merge (R (loc_result sig))) rs_merge) ls3.
-Proof.
-  intros. apply agree_set with (LTL.return_regs ls1 ls2); auto.
-  rewrite H2; unfold rs_merge. 
-  repeat rewrite return_regs_result. apply H1. apply loc_result_acceptable.
-  unfold rs_merge. apply agree_return_regs; auto.
-Qed.
-
-(** [agree_arguments] and [agree_parameters] are two stronger
-  variants of the predicate [agree].  They additionally demand
-  equality of the values of locations that are arguments or parameters
-  (respectively) for a call to a function of signature [sg]. *)
-
-Definition agree_arguments (sg: signature) (rs1 rs2: locset) : Prop :=
-  forall l, loc_acceptable l \/ In l (loc_arguments sg) -> rs2 l = rs1 l.
-
-Definition agree_parameters (sg: signature) (rs1 rs2: locset) : Prop :=
-  forall l, loc_acceptable l \/ In l (loc_parameters sg) -> rs2 l = rs1 l.
-
-Remark parallel_assignment:
-  forall (P: loc -> Prop) (rs1 rs2 ls1 ls2: locset) srcs dsts,
-  map rs2 dsts = map rs1 srcs ->
-  map ls2 dsts = map ls1 srcs ->
-  (forall l, In l srcs -> P l) ->
-  (forall l, P l -> ls1 l = rs1 l) ->
-  (forall l, In l dsts -> ls2 l = rs2 l).
-Proof.
-  induction srcs; destruct dsts; simpl; intros; try congruence.
-  contradiction.
-  inv H; inv H0. elim H3; intro. subst l0.
-  rewrite H5; rewrite H4. auto with coqlib.
-  eapply IHsrcs; eauto. 
-Qed.
-
-Lemma agree_set_arguments:
-  forall rs1 ls1 ls2 args sg,
-  agree rs1 ls1 ->
-  List.map Loc.type args = sg.(sig_args) ->
-  locs_acceptable args ->
-  List.map ls2 (loc_arguments sg) = map ls1 args ->
-  (forall l : loc,
-    Loc.notin l (loc_arguments sg) ->
-    Loc.notin l temporaries -> ls2 l = ls1 l) ->
-  agree_arguments sg (LTL.parmov args (loc_arguments sg) rs1) ls2.
-Proof.
-  intros.  
-  assert (Loc.norepet (loc_arguments sg)).
-    apply loc_arguments_norepet.
-  assert (List.length args = List.length (loc_arguments sg)).
-    rewrite loc_arguments_length. rewrite <- H0.
-    symmetry. apply list_length_map.
-  destruct (parmov_spec rs1 _ _ H4 H5) as [A B].
-  set (rs2 := LTL.parmov args (loc_arguments sg) rs1) in *.
-  assert (forall l, In l (loc_arguments sg) -> ls2 l = rs2 l).
-    intros.
-    eapply parallel_assignment with (P := loc_acceptable); eauto.
-  red; intros. 
-  destruct (In_dec Loc.eq l (loc_arguments sg)).
-  auto.
-  assert (loc_acceptable l) by tauto.
-  assert (Loc.notin l (loc_arguments sg)).
-    eapply loc_acceptable_notin_notin; eauto.
-  rewrite H3; auto. rewrite B; auto. 
-  apply temporaries_not_acceptable; auto.
-Qed.
-
-Lemma agree_arguments_agree:
-  forall sg rs ls, agree_arguments sg rs ls -> agree rs ls.
-Proof.
-  intros; red; intros; auto.
-Qed.
-
-Lemma agree_arguments_locs:
-  forall sg rs1 rs2,
-  agree_arguments sg rs1 rs2 ->
-  map rs2 (loc_arguments sg) = map rs1 (loc_arguments sg).
-Proof.
-  intros.
-  assert (forall ll, incl ll (loc_arguments sg) -> map rs2 ll = map rs1 ll).
-    induction ll; simpl; intros. auto.
-    f_equal. apply H. right. apply H0. auto with coqlib.
-    apply IHll. eapply incl_cons_inv; eauto.
-  apply H0. apply incl_refl.
-Qed.
-
-Lemma agree_set_parameters:
-  forall rs1 ls1 ls2 sg params,
-  agree_parameters sg rs1 ls1 ->
-  List.map Loc.type params = sg.(sig_args) ->
-  locs_acceptable params ->
-  Loc.norepet params ->
-  List.map ls2 params = List.map ls1 (loc_parameters sg) ->
-  (forall l : loc,
-    Loc.notin l params ->
-    Loc.notin l temporaries -> ls2 l = ls1 l) ->
-  agree (LTL.parmov (loc_parameters sg) params rs1) ls2.
-Proof.
-  intros.
-  assert (List.length (loc_parameters sg) = List.length params).
-    unfold loc_parameters. rewrite list_length_map. 
-    rewrite loc_arguments_length. rewrite <- H0.
-    apply list_length_map.
-  destruct (parmov_spec rs1 _ _ H2 H5) as [A B].
-  set (rs2 := LTL.parmov (loc_parameters sg) params rs1) in *.
-  red; intros.
-  assert (forall l, In l params -> ls2 l = rs2 l).
-    intros.
-    eapply parallel_assignment with (P := fun l => In l (loc_parameters sg)); eauto.
-  destruct (In_dec Loc.eq l params).
-  auto.
-  assert (Loc.notin l params).
-    eapply loc_acceptable_notin_notin; eauto.
-  rewrite B; auto. rewrite H4; auto. 
-  apply temporaries_not_acceptable; auto.
-Qed.
-
-Lemma agree_call_regs:
-  forall sg rs ls,
-  agree_arguments sg rs ls ->
-  agree_parameters sg (LTL.call_regs rs) (LTL.call_regs ls).
-Proof.
-  intros; red; intros. elim H0.
-  destruct l; simpl; auto. destruct s; auto.
-  unfold loc_parameters. intro. 
-  destruct (list_in_map_inv _ _ _ H1) as [r [A B]].
-  subst l. generalize (loc_arguments_acceptable _ _ B). 
-  destruct r; simpl; auto. destruct s; simpl; auto.
-Qed.
-
-Lemma agree_arguments_return_regs:
-  forall sg rs1 rs2 ls1 ls2,
-  tailcall_possible sg ->
-  agree rs1 ls1 ->
-  agree_arguments sg rs2 ls2 ->
-  agree_arguments sg (LTL.return_regs rs1 rs2) (LTL.return_regs ls1 ls2).
-Proof.
-  intros; red; intros. generalize (H1 l H2). intro.
-  elim H2; intro. generalize (H0 l H4); intro. 
-  unfold LTL.return_regs. destruct l; auto.
-  destruct (In_dec Loc.eq (R m) temporaries); auto.
-  destruct (In_dec Loc.eq (R m) destroyed_at_call); auto.
-  generalize (H l H4). unfold LTL.return_regs; destruct l; intro.
-  destruct (In_dec Loc.eq (R m) temporaries); auto.
-  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 ->
@@ -643,9 +486,9 @@ Qed.
 Lemma agree_postcall_1:
   forall rs ls,
   agree rs ls ->
-  agree (LTL.postcall_regs rs) ls.
+  agree (LTL.postcall_locs rs) ls.
 Proof.
-  intros; red; intros. unfold LTL.postcall_regs.
+  intros; red; intros. unfold LTL.postcall_locs.
   destruct l; auto. 
   destruct (In_dec Loc.eq (R m) temporaries). constructor.
   destruct (In_dec Loc.eq (R m) destroyed_at_call). constructor.
@@ -654,11 +497,13 @@ 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'.
+  agree (LTL.postcall_locs rs) ls ->
+  (forall l,
+      loc_acceptable l -> ~In l destroyed_at_call -> ~In l temporaries ->
+      ls' l = ls l) ->
+  agree (LTL.postcall_locs rs) ls'.
 Proof.
-  intros; red; intros. generalize (H l H1). unfold LTL.postcall_regs. 
+  intros; red; intros. generalize (H l H1). unfold LTL.postcall_locs. 
   destruct l. 
   destruct (In_dec Loc.eq (R m) temporaries). intro; constructor.
   destruct (In_dec Loc.eq (R m) destroyed_at_call). intro; constructor.
@@ -671,8 +516,10 @@ 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'.
+  (forall l,
+     Loc.notin l (loc_arguments sig) -> Loc.notin l temporaries -> 
+     ls' l = ls l) ->
+  agree (LTL.postcall_locs rs) ls'.
 Proof.
   intros. apply agree_postcall_2 with ls. apply agree_postcall_1; auto.
   intros. apply H0.
@@ -686,7 +533,7 @@ 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).
+  agree (LTL.postcall_locs 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)).
@@ -713,8 +560,7 @@ Qed.
 
 Lemma call_regs_parameters:
   forall ls sig,
-  map (call_regs ls) (loc_parameters sig) =
-  map ls (loc_arguments 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. 
@@ -725,12 +571,24 @@ Proof.
   destruct s; intros; try contradiction. auto.
 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.
+
 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.
+  intros. 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.
@@ -748,18 +606,6 @@ Proof.
   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 *)
 
 Lemma find_label_add_spill:
@@ -899,13 +745,22 @@ Qed.
   it enforces are:
 - Agreement between the values of locations in the two programs,
   according to the [agree] or [agree_arguments] predicates.
+- Agreement between the memory states of the two programs,
+  according to the [Mem.lessdef] predicate.
 - Lists of LTLin instructions appearing in the source state
   are always suffixes of the code for the corresponding functions.
 - Well-typedness of the source code, which ensures that
   only acceptable locations are accessed by this code.
+- Agreement over return types during calls: the return type of a function
+  is always equal to the return type of the signature of the corresponding
+  call.  This invariant is necessary since the conventional location
+  used for passing return values depend on the return type.  This invariant
+  is enforced through the third parameter of the [match_stackframes]
+  predicate, which is the signature of the called function.
 *)
 
-Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> signature -> Prop :=
+Inductive match_stackframes:
+       list LTLin.stackframe -> list Linear.stackframe -> signature -> Prop :=
   | match_stackframes_nil:
       forall sig,
       sig.(sig_res) = Some Tint ->
@@ -914,13 +769,14 @@ Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe ->
       forall res f sp c rs s s' c' ls sig,
       match_stackframes s s' (LTLin.fn_sig f) ->
       c' = add_spill (loc_result sig) res (transf_code f c) ->      
-      agree (LTL.postcall_regs rs) ls ->
+      agree (LTL.postcall_locs rs) ls ->
       loc_acceptable res ->
       wt_function f ->
       is_tail c (LTLin.fn_code f) ->
-      match_stackframes (LTLin.Stackframe res f sp (LTL.postcall_regs rs) c :: s)
-                        (Linear.Stackframe (transf_function f) sp ls c' :: s')
-                        sig.
+      match_stackframes
+         (LTLin.Stackframe res f sp (LTL.postcall_locs rs) c :: s)
+         (Linear.Stackframe (transf_function f) sp ls c' :: s')
+         sig.
 
 Inductive match_states: LTLin.state -> Linear.state -> Prop :=
   | match_states_intro:
@@ -992,8 +848,6 @@ 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'),
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index cefad10..7ad75ba 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -299,7 +299,7 @@ Proof.
   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') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_regs rs)) m'); split.
+  left; exists (State ts (tunnel_function f) sp (branch_target f pc') (Locmap.set res (Vptr b Integers.Int.zero) (postcall_locs rs)) m'); split.
   eapply exec_Lalloc; eauto.
   rewrite (tunnel_function_lookup _ _ _ H); simpl; auto.
   econstructor; eauto.