Nettoyage du traitement des signatures au return dans LTL et LTLin

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

6 files changed, 96 insertions, 107 deletions

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 68d6868c..051be1e6 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -552,12 +552,13 @@ Qed.
   The bottom horizontal bar is the [match_states] relation.
 *)
 
-Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signature -> Prop :=
-  | match_stackframes_nil: forall ty_args,
-      match_stackframes nil nil (mksignature ty_args (Some Tint))
+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,
-      match_stackframes s ts (RTL.fn_sig f) ->
+      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 ->
@@ -569,13 +570,13 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signa
               (Locmap.set (assign res) (ls1 (R (loc_result sig))) ls1)) ->
       match_stackframes
         (RTL.Stackframe res (RTL.fn_code f) sp pc rs :: s)
-        (LTL.Stackframe (assign res) (transf_fun f live assign) sp ls pc :: ts)
-        sig.
+        (LTL.Stackframe sig (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
-      (STACKS: match_stackframes s ts (RTL.fn_sig f))
+      (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)
@@ -585,7 +586,8 @@ Inductive match_states: RTL.state -> LTL.state -> Prop :=
                    (LTL.State ts (transf_fun f live assign) sp pc ls tm)
   | match_states_call:
       forall s f args m ts tf ls tm,
-      match_stackframes s ts (RTL.funsig f) ->
+      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 ->
@@ -593,28 +595,13 @@ Inductive match_states: RTL.state -> LTL.state -> Prop :=
       match_states (RTL.Callstate s f args m)
                    (LTL.Callstate ts tf ls tm)
   | match_states_return:
-      forall s v m ts sig ls tm,
-      match_stackframes s ts sig ->
-      Val.lessdef v (ls (R (loc_result sig))) ->
+      forall s v m ts ls tm,
+      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 sig ls tm).
-
-Remark match_stackframes_change:
-  forall s ts sig,
-  match_stackframes s ts sig ->
-  forall sig',
-  sig_res sig' = sig_res sig ->
-  match_stackframes s ts sig'.
-Proof.
-  induction 1; intros.
-  destruct sig'. simpl in H; inv H. constructor.
-  assert (loc_result sig' = loc_result sig).
-  unfold loc_result. rewrite H4; auto.
-  econstructor; eauto.
-  rewrite H5. auto. 
-Qed.
+                   (LTL.Returnstate ts ls tm).
 
 (** The simulation proof is by case analysis over the RTL transition
   taken in the source program. *)
@@ -808,8 +795,7 @@ Proof.
   rewrite (sig_function_translated _ _ TF). eauto.
   rewrite (sig_function_translated _ _ TF).
   econstructor; eauto.
-  apply match_stackframes_change with (RTL.fn_sig f0); auto.
-  inv WTI. auto.
+  inv WTI. congruence.
   rewrite (sig_function_translated _ _ TF).
   rewrite return_regs_arguments. 
   change Regset.elt with reg in PM1. 
@@ -865,13 +851,16 @@ Proof.
   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.
 
   (* internal function *)
-  generalize H6. simpl.  unfold transf_function.
+  generalize H7. simpl.  unfold transf_function.
   caseEq (type_function f); simpl; try congruence. intros env TYP.
   assert (WTF: wt_function f env). apply type_function_correct; auto.
   caseEq (analyze f); simpl; try congruence. intros live ANL.
@@ -902,13 +891,16 @@ Proof.
   apply list_map_exten. intros. symmetry. eapply call_regs_param_of_arg; eauto.
 
   (* external function *)
-  injection H6; intro EQ; inv EQ.
+  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.
-  intros. rewrite <- H10; auto. apply Locmap.gso.
+  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. 
 
@@ -940,7 +932,7 @@ Proof.
   econstructor; eauto.
   rewrite symbols_preserved. 
   rewrite (transform_partial_program_main _ _ TRANSF).  auto.
-  constructor; auto. rewrite H2; constructor. 
+  constructor; auto. constructor. rewrite H2; auto. 
 Qed.
 
 Lemma transf_final_states:
@@ -948,7 +940,7 @@ Lemma transf_final_states:
   match_states st1 st2 -> RTL.final_state st1 r -> LTL.final_state st2 r.
 Proof.
   intros. inv H0. inv H. inv H3. econstructor.
-  inv H4. auto. 
+  simpl in H4. inv H4. auto. 
 Qed.
 
 Theorem transf_program_correct:
diff --git a/backend/LTL.v b/backend/LTL.v
index e99e016e..a082e122 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -140,7 +140,8 @@ Definition set_result_reg (s: signature) (or: option loc) (ls: locset) :=
 
 Inductive stackframe : Set :=
   | Stackframe:
-      forall (res: loc)         (**r where to store the result *)
+      forall (sig: signature)   (**r signature of call *)
+             (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 *)
@@ -164,7 +165,6 @@ Inductive state : Set :=
       state
   | Returnstate:
       forall (stack: list stackframe) (**r call stack *)
-             (sig: signature)         (**r signature of returning function *)
              (ls: locset)             (**r location state at point of return *)
              (m: mem),                (**r memory state *)
       state.
@@ -172,7 +172,13 @@ Inductive state : Set :=
 Definition parent_locset (stack: list stackframe) : locset :=
   match stack with
   | nil => Locmap.init Vundef
-  | Stackframe res f sp ls pc :: stack' => ls
+  | 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.
@@ -261,7 +267,7 @@ Inductive step: state -> trace -> state -> Prop :=
       funsig f' = sig ->
       let rs1 := parmov args (loc_arguments sig) rs in
       step (State s f sp pc rs m)
-        E0 (Callstate (Stackframe res f sp rs1 pc' :: s) f' rs1 m)
+        E0 (Callstate (Stackframe sig res f sp rs1 pc' :: s) f' rs1 m)
   | exec_Ltailcall:
       forall s f stk pc rs m sig ros args f',
       (fn_code f)!pc = Some(Ltailcall sig ros args) ->
@@ -299,7 +305,7 @@ Inductive step: state -> trace -> state -> Prop :=
       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 f.(fn_sig) rs2 (Mem.free m stk))
+        E0 (Returnstate s rs2 (Mem.free m stk))
   | exec_function_internal:
       forall s f rs m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
@@ -314,12 +320,11 @@ Inductive step: state -> trace -> state -> Prop :=
       let rs1 :=
         Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in
       step (Callstate s (External ef) rs m)
-         t (Returnstate s ef.(ef_sig) rs1 m)
+         t (Returnstate s rs1 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 res f sp rs0 pc :: s) 
-                        sig rs m)
+      step (Returnstate (Stackframe sig res f sp rs0 pc :: s) rs m)
         E0 (State s f sp pc rs1 m).
 
 End RELSEM.
@@ -339,9 +344,9 @@ Inductive initial_state (p: program): state -> Prop :=
       initial_state p (Callstate nil f (Locmap.init Vundef) m0).
 
 Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall sig rs m r,
-      rs (R (loc_result sig)) = Vint r ->
-      final_state (Returnstate nil sig rs m) r.
+  | final_state_intro: forall rs m r,
+      rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r ->
+      final_state (Returnstate nil rs m) r.
 
 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 6cf2eb53..157b6d47 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -112,7 +112,8 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
 
 Inductive stackframe : Set :=
   | Stackframe:
-      forall (res: loc)       (**r where to store the result *)
+      forall (sig: signature) (**r signature of call *)
+             (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 *)
@@ -136,7 +137,6 @@ Inductive state : Set :=
       state
   | Returnstate:
       forall (stack: list stackframe) (**r call stack *)
-             (sig: signature)         (**r signature of returning function *)
              (ls: locset)             (**r location state at point of return *)
              (m: mem),                (**r memory state *)
       state.
@@ -144,7 +144,13 @@ Inductive state : Set :=
 Definition parent_locset (stack: list stackframe) : locset :=
   match stack with
   | nil => Locmap.init Vundef
-  | Stackframe res f sp ls pc :: stack' => ls
+  | 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.
@@ -185,7 +191,7 @@ Inductive step: state -> trace -> state -> Prop :=
       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 res f sp rs1 b :: s) f' rs1 m)
+        E0 (Callstate (Stackframe sig res f sp rs1 b :: s) f' rs1 m)
   | exec_Ltailcall:
       forall s f stk sig ros args b rs m f',
       find_function ros rs = Some f' ->
@@ -228,7 +234,7 @@ Inductive step: state -> trace -> state -> Prop :=
       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 f.(fn_sig) rs2 (Mem.free m stk))
+        E0 (Returnstate s rs2 (Mem.free m stk))
   | exec_function_internal:
       forall s f rs m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
@@ -243,11 +249,11 @@ Inductive step: state -> trace -> state -> Prop :=
       let rs1 :=
         Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in
       step (Callstate s (External ef) rs m)
-         t (Returnstate s ef.(ef_sig) rs1 m)
+         t (Returnstate s rs1 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 res f sp rs0 b :: s) sig rs m)
+      step (Returnstate (Stackframe sig res f sp rs0 b :: s) rs m)
         E0 (State s f sp b rs1 m).
 
 End RELSEM.
@@ -262,9 +268,9 @@ Inductive initial_state (p: program): state -> Prop :=
       initial_state p (Callstate nil f (Locmap.init Vundef) m0).
 
 Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall sig rs m r,
-      rs (R (loc_result sig)) = Vint r ->
-      final_state (Returnstate nil sig rs m) r.
+  | final_state_intro: forall rs m r,
+      rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r ->
+      final_state (Returnstate nil rs m) r.
 
 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/Linearizeproof.v b/backend/Linearizeproof.v
index a7b01861..303482e0 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 res f sp pc ls tf c,
+      forall sig 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 res f sp ls pc)
-        (LTLin.Stackframe res tf sp ls (add_branch pc c)).
+        (LTL.Stackframe sig res f sp ls pc)
+        (LTLin.Stackframe sig res tf sp ls (add_branch pc c)).
 
 Inductive match_states: LTL.state -> LTLin.state -> Prop :=
   | match_states_intro:
@@ -496,10 +496,10 @@ Inductive match_states: LTL.state -> LTLin.state -> Prop :=
       match_states (LTL.Callstate s f ls m)
                    (LTLin.Callstate ts tf ls m)
   | match_states_return:
-      forall s sig ls m ts,
+      forall s ls m ts,
       list_forall2 match_stackframes s ts ->
-      match_states (LTL.Returnstate s sig ls m)
-                   (LTLin.Returnstate ts sig ls m).
+      match_states (LTL.Returnstate s ls m)
+                   (LTLin.Returnstate ts ls m).
 
 Remark parent_locset_match:
   forall s ts,
@@ -699,7 +699,7 @@ Proof.
   econstructor; eauto.
 
   (* return *)
-  inv H4. inv H1.
+  inv H3. inv H1.
   exploit find_label_lin_succ; eauto. intros [c' AT].
   econstructor; split.
   eapply plus_left'.
@@ -730,7 +730,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 H6. constructor. auto. 
+  intros. inv H0. inv H. inv H5. constructor. auto. 
 Qed.
 
 Theorem transf_program_correct:
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 401ae466..f0b17e1b 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -770,26 +770,26 @@ Qed.
   only acceptable locations are accessed by this code.
 *)
 
-Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> signature -> Prop :=
+Inductive match_stackframes: list LTLin.stackframe -> list Linear.stackframe -> Prop :=
   | match_stackframes_nil:
-      forall tyargs,
-      match_stackframes nil nil (mksignature tyargs (Some Tint))
+      match_stackframes nil nil
   | match_stackframes_cons:
       forall res f sp c rs s s' c' ls sig,
-      match_stackframes s s' (LTLin.fn_sig f) ->
+      match_stackframes s s' ->
+      sig_res (LTLin.fn_sig f) = sig_res (parent_callsig s) ->
       c' = add_spill (loc_result sig) res (transf_code f c) ->      
       agree rs ls ->
       loc_acceptable res ->
       wt_function f ->
       is_tail c (LTLin.fn_code f) ->
-      match_stackframes (LTLin.Stackframe res f sp rs c :: s)
-                        (Linear.Stackframe (transf_function f) sp ls c' :: s')
-                        sig.
+      match_stackframes (LTLin.Stackframe sig res f sp rs c :: s)
+                        (Linear.Stackframe (transf_function f) sp ls c' :: s').
 
 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' (LTLin.fn_sig f))
+        (STACKS: match_stackframes s s')
+        (SIG: sig_res (LTLin.fn_sig f) = sig_res (parent_callsig s))
         (AG: agree rs ls)
         (WT: wt_function f)
         (TL: is_tail c (LTLin.fn_code f)),
@@ -797,40 +797,28 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop :=
                    (Linear.State s' (transf_function f) sp (transf_code f c) ls m)
   | match_states_call:
       forall s f rs m s' ls
-        (STACKS: match_stackframes s s' (LTLin.funsig f))
+        (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)
   | match_states_return:
-      forall s sig rs m s' ls
-        (STACKS: match_stackframes s s' sig)
+      forall s rs m s' ls
+        (STACKS: match_stackframes s s')
         (AG: agree rs ls),
-      match_states (LTLin.Returnstate s sig rs m)
+      match_states (LTLin.Returnstate s rs m)
                    (Linear.Returnstate s' ls m).
 
 Remark parent_locset_match:
-  forall s s' sig,
-  match_stackframes s s' sig ->
+  forall s s',
+  match_stackframes s s' ->
   agree (LTLin.parent_locset s) (parent_locset s').
 Proof.
   induction 1; simpl.
   red; intros; auto.
   auto.
 Qed.
-
-Remark match_stackframes_inv:
-  forall s ts sig,
-  match_stackframes s ts sig ->
-  forall sig', sig_res sig' = sig_res sig ->
-  match_stackframes s ts sig'.
-Proof.
-  induction 1; intros.
-  destruct sig'. simpl in H; inv H. constructor.
-  assert (loc_result sig' = loc_result sig).
-  unfold loc_result. rewrite H5; auto.
-  econstructor; eauto. rewrite H6; auto.
-Qed. 
          
 Ltac ExploitWT :=
   match goal with
@@ -859,7 +847,7 @@ Definition measure (st: LTLin.state) : nat :=
   match st with
   | LTLin.State s f sp c ls m => List.length c
   | LTLin.Callstate s f ls m => 0%nat
-  | LTLin.Returnstate s sig ls m => 0%nat
+  | LTLin.Returnstate s ls m => 0%nat
   end.
 
 Theorem transf_step_correct:
@@ -995,8 +983,8 @@ Proof.
   eauto. traceEq.
   econstructor; eauto. 
   econstructor; eauto with coqlib.
-  rewrite H0. auto.
   eapply agree_arguments_agree; eauto.
+  simpl. congruence. 
   (* direct call *)
   destruct (parallel_move_arguments_correct tge s' (transf_function f) sp
               args sig
@@ -1017,8 +1005,8 @@ Proof.
   traceEq.
   econstructor; eauto.
   econstructor; eauto with coqlib.
-  rewrite H0; auto.
   eapply agree_arguments_agree; eauto.
+  simpl; congruence.
 
   (* Ltailcall *)
   inversion MS. subst s0 f0 sp c rs0 m0 s1'.
@@ -1055,8 +1043,7 @@ Proof.
     apply functions_translated. eauto.
     rewrite H0; symmetry; apply sig_preserved.
   eauto. traceEq.
-  econstructor; eauto.
-  eapply match_stackframes_inv; eauto. congruence.
+  econstructor; eauto. congruence. 
  
   (* direct call *)
   destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero)
@@ -1077,8 +1064,7 @@ Proof.
     apply function_ptr_translated; auto. congruence.
     rewrite H0. symmetry; apply sig_preserved.
   traceEq.
-  econstructor; eauto.
-  eapply match_stackframes_inv; eauto. congruence.
+  econstructor; eauto. congruence.
 
   (* Lalloc *)
   ExploitWT; inv WTI.
@@ -1213,7 +1199,7 @@ Proof.
   apply function_ptr_translated; eauto. 
   rewrite sig_preserved. auto.
   replace (Genv.init_mem tprog) with (Genv.init_mem prog).  
-  econstructor; eauto. rewrite H2. constructor.
+  econstructor; eauto. constructor. rewrite H2; auto.
   red; intros. auto.
   eapply Genv.find_funct_ptr_prop; eauto.
   symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf; auto.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index d0c95462..cb0a6d83 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 res f sp ls0 pc,
+      forall sig res f sp ls0 pc,
       match_stackframes
-         (Stackframe res f sp ls0 pc)
-         (Stackframe res (tunnel_function f) sp ls0 (branch_target f pc)).
+         (Stackframe sig res f sp ls0 pc)
+         (Stackframe sig res (tunnel_function f) sp ls0 (branch_target f pc)).
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
@@ -207,10 +207,10 @@ Inductive match_states: state -> state -> Prop :=
       match_states (Callstate s f ls m)
                    (Callstate ts (tunnel_fundef f) ls m)
   | match_states_return:
-      forall s sig ls m ts,
+      forall s ls m ts,
       list_forall2 match_stackframes s ts ->
-      match_states (Returnstate s sig ls m)
-                   (Returnstate ts sig ls m).
+      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.
@@ -227,7 +227,7 @@ Definition measure (st: state) : nat :=
   match st with
   | State s f sp pc ls m => count_goto f pc
   | Callstate s f ls m => 0%nat
-  | Returnstate s sig ls m => 0%nat
+  | Returnstate s ls m => 0%nat
   end.
 
 Lemma branch_target_identity:
@@ -340,7 +340,7 @@ Proof.
   eapply exec_function_external; eauto.
   simpl. econstructor; eauto. 
   (* return *)
-  inv H4. inv H1.
+  inv H3. inv H1.
   left; econstructor; split.
   eapply exec_return; eauto.
   fold rs1. constructor. auto.
@@ -366,7 +366,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 H6. constructor. auto. 
+  intros. inv H0. inv H. inv H5. constructor. auto. 
 Qed.
 
 Theorem transf_program_correct: