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

1 files changed, 99 insertions, 196 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: