Fusion de la branche "traces":

- Ajout de traces d'evenements d'E/S dans les semantiques
- Ajout constructions switch et allocation dynamique
- Initialisation des variables globales
- Portage Coq 8.1 beta
Debut d'integration du front-end C:
- Traduction Clight -> Csharpminor dans cfrontend/
- Modifications de Csharpminor et Globalenvs en consequence.


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

1 files changed, 289 insertions, 214 deletions

diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index d34bae9..24cc41b 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -6,6 +6,7 @@ Require Import AST.
 Require Import Integers.
 Require Import Values.
 Require Import Mem.
+Require Import Events.
 Require Import Globalenvs.
 Require Import Op.
 Require Import Registers.
@@ -30,45 +31,59 @@ Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
 Proof.
   intro. unfold ge, tge. 
-  apply Genv.find_symbol_transf_partial with transl_function.
+  apply Genv.find_symbol_transf_partial with transl_fundef.
   exact TRANSL.
 Qed.
 
 Lemma function_ptr_translated:
-  forall (b: block) (f: Cminor.function),
+  forall (b: block) (f: Cminor.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
-  Genv.find_funct_ptr tge b = Some tf /\ transl_function f = Some tf.
+  Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = Some tf.
 Proof.
   intros. 
   generalize 
-   (Genv.find_funct_ptr_transf_partial transl_function TRANSL H).
-  case (transl_function f).
+   (Genv.find_funct_ptr_transf_partial transl_fundef TRANSL H).
+  case (transl_fundef f).
   intros tf [A B]. exists tf. tauto.
   intros [A B]. elim B. reflexivity.
 Qed.
 
 Lemma functions_translated:
-  forall (v: val) (f: Cminor.function),
+  forall (v: val) (f: Cminor.fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
-  Genv.find_funct tge v = Some tf /\ transl_function f = Some tf.
+  Genv.find_funct tge v = Some tf /\ transl_fundef f = Some tf.
 Proof.
   intros. 
   generalize 
-   (Genv.find_funct_transf_partial transl_function TRANSL H).
-  case (transl_function f).
+   (Genv.find_funct_transf_partial transl_fundef TRANSL H).
+  case (transl_fundef f).
   intros tf [A B]. exists tf. tauto.
   intros [A B]. elim B. reflexivity.
 Qed.
 
+Lemma sig_transl_function:
+  forall (f: Cminor.fundef) (tf: RTL.fundef),
+  transl_fundef f = Some tf ->
+  RTL.funsig tf = Cminor.funsig f.
+Proof.
+  intros until tf. unfold transl_fundef, transf_partial_fundef.
+  case f; intro.
+  unfold transl_function. 
+  case (transl_fun f0 init_state); intros.
+  discriminate.
+  destruct p. inversion H. reflexivity.
+  intro. inversion H. reflexivity.
+Qed.
+
 (** Correctness of the code generated by [add_move]. *)
 
 Lemma add_move_correct:
   forall r1 r2 sp nd s ns s' rs m,
   add_move r1 r2 nd s = OK ns s' ->
   exists rs',
-  exec_instrs tge s'.(st_code) sp ns rs m  nd rs' m /\
+  exec_instrs tge s'.(st_code) sp ns rs m E0 nd rs' m /\
   rs'#r2 = rs#r1 /\
   (forall r, r <> r2 -> rs'#r = rs#r).
 Proof.
@@ -118,7 +133,7 @@ Qed.
 
 Definition transl_expr_correct 
   (sp: val) (le: letenv) (e: env) (m: mem) (a: expr)
-                         (e': env) (m': mem) (v: val) : Prop :=
+              (t: trace) (e': env) (m': mem) (v: val) : Prop :=
   forall map mut rd nd s ns s' rs
     (MWF: map_wf map s)
     (TE: transl_expr map mut a rd nd s = OK ns s')
@@ -126,7 +141,7 @@ Definition transl_expr_correct
     (MUT: incl (mutated_expr a) mut)
     (TRG: target_reg_ok s map mut a rd),
   exists rs',
-     exec_instrs tge s'.(st_code) sp ns rs m nd rs' m'
+     exec_instrs tge s'.(st_code) sp ns rs m t nd rs' m'
   /\ match_env map e' le rs'
   /\ rs'#rd = v
   /\ (forall r,
@@ -139,7 +154,7 @@ Definition transl_expr_correct
 
 Definition transl_exprlist_correct 
   (sp: val) (le: letenv) (e: env) (m: mem) (al: exprlist)
-                         (e': env) (m': mem) (vl: list val) : Prop :=
+              (t: trace) (e': env) (m': mem) (vl: list val) : Prop :=
   forall map mut rl nd s ns s' rs
     (MWF: map_wf map s)
     (TE: transl_exprlist map mut al rl nd s = OK ns s')
@@ -147,7 +162,7 @@ Definition transl_exprlist_correct
     (MUT: incl (mutated_exprlist al) mut)
     (TRG: target_regs_ok s map mut al rl),
   exists rs',
-     exec_instrs tge s'.(st_code) sp ns rs m nd rs' m'
+     exec_instrs tge s'.(st_code) sp ns rs m t nd rs' m'
   /\ match_env map e' le rs'
   /\ rs'##rl = vl
   /\ (forall r,
@@ -157,14 +172,14 @@ Definition transl_exprlist_correct
 
 Definition transl_condition_correct 
   (sp: val) (le: letenv) (e: env) (m: mem) (a: condexpr)
-                         (e': env) (m': mem) (vb: bool) : Prop :=
+              (t: trace) (e': env) (m': mem) (vb: bool) : Prop :=
   forall map mut ntrue nfalse s ns s' rs
     (MWF: map_wf map s)
     (TE: transl_condition map mut a ntrue nfalse s = OK ns s')
     (ME: match_env map e le rs)
     (MUT: incl (mutated_condexpr a) mut),
   exists rs',
-     exec_instrs tge s'.(st_code) sp ns rs m (if vb then ntrue else nfalse) rs' m'
+     exec_instrs tge s'.(st_code) sp ns rs m t (if vb then ntrue else nfalse) rs' m'
   /\ match_env map e' le rs'
   /\ (forall r,
         reg_valid r s -> ~(mutated_reg map mut r) ->
@@ -233,7 +248,7 @@ Definition match_return_outcome
 
 Definition transl_stmt_correct 
   (sp: val) (e: env) (m: mem) (a: stmt)
-            (e': env) (m': mem) (out: outcome) : Prop :=
+  (t: trace) (e': env) (m': mem) (out: outcome) : Prop :=
   forall map ncont nexits nret rret s ns s' nd rs
     (MWF: map_wf map s)
     (TE: transl_stmt map a ncont nexits nret rret s = OK ns s')
@@ -241,7 +256,7 @@ Definition transl_stmt_correct
     (OUT: outcome_node out ncont nexits nret nd)
     (RRG: return_reg_ok s map rret),
   exists rs',
-     exec_instrs tge s'.(st_code) sp ns rs m nd rs' m'
+     exec_instrs tge s'.(st_code) sp ns rs m t nd rs' m'
   /\ match_env map e' nil rs'
   /\ match_return_outcome out rret rs'.
 
@@ -251,11 +266,11 @@ Definition transl_stmt_correct
   the same modifications on the memory state. *)
 
 Definition transl_function_correct
-    (m: mem) (f: Cminor.function) (vargs: list val)
-    (m':mem) (vres: val) : Prop :=
+    (m: mem) (f: Cminor.fundef) (vargs: list val)
+    (t: trace) (m':mem) (vres: val) : Prop :=
   forall tf
-    (TE: transl_function f = Some tf),
-  exec_function tge tf vargs m vres m'.
+    (TE: transl_fundef f = Some tf),
+  exec_function tge tf vargs m t vres m'.
 
 (** The correctness of the translation is a huge induction over
   the Cminor evaluation derivation for the source program.  To keep
@@ -268,7 +283,7 @@ Definition transl_function_correct
 Lemma transl_expr_Evar_correct:
   forall (sp: val) (le: letenv) (e: env) (m: mem) (id: ident) (v: val),
   e!id = Some v ->
-  transl_expr_correct sp le e m (Evar id) e m v.
+  transl_expr_correct sp le e m (Evar id) E0 e m v.
 Proof.
   intros; red; intros. monadInv TE. intro. 
   generalize EQ; unfold find_var. caseEq (map_vars map)!id.
@@ -303,12 +318,12 @@ Qed.
 
 Lemma transl_expr_Eop_correct:
   forall (sp: val) (le : letenv) (e : env) (m : mem) (op : operation)
-         (al : exprlist) (e1 : env) (m1 : mem) (vl : list val)
+         (al : exprlist) (t: trace) (e1 : env) (m1 : mem) (vl : list val)
          (v: val),
-  eval_exprlist ge sp le e m al e1 m1 vl ->
-  transl_exprlist_correct sp le e m al e1 m1 vl ->
+  eval_exprlist ge sp le e m al t e1 m1 vl ->
+  transl_exprlist_correct sp le e m al t e1 m1 vl ->
   eval_operation ge sp op vl = Some v ->
-  transl_expr_correct sp le e m (Eop op al) e1 m1 v.
+  transl_expr_correct sp le e m (Eop op al) t e1 m1 v.
 Proof.
   intros until v. intros EEL TEL EOP. red; intros.
   simpl in TE. monadInv TE. intro EQ1. 
@@ -323,9 +338,9 @@ Proof.
   apply exec_instrs_incr with s1. eauto with rtlg.
   apply exec_one; eapply exec_Iop. eauto with rtlg.
   subst vl. 
-  rewrite (@eval_operation_preserved Cminor.function RTL.function ge tge). 
+  rewrite (@eval_operation_preserved Cminor.fundef RTL.fundef ge tge). 
   eexact EOP.
-  exact symbols_preserved.
+  exact symbols_preserved. traceEq.
 (* Match-env *)
   split. inversion TRG. eauto with rtlg.
 (* Result reg *)
@@ -344,11 +359,11 @@ Qed.
 
 Lemma transl_expr_Eassign_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem) 
-    (id : ident) (a : expr) (e1 : env) (m1 : mem) 
+    (id : ident) (a : expr) (t: trace) (e1 : env) (m1 : mem) 
     (v : val),
-  eval_expr ge sp le e m a e1 m1 v ->
-  transl_expr_correct sp le e m a e1 m1 v ->
-  transl_expr_correct sp le e m (Eassign id a) (PTree.set id v e1) m1 v.
+  eval_expr ge sp le e m a t e1 m1 v ->
+  transl_expr_correct sp le e m a t e1 m1 v ->
+  transl_expr_correct sp le e m (Eassign id a) t (PTree.set id v e1) m1 v.
 Proof.
   intros; red; intros.
   simpl in TE. monadInv TE. intro EQ1. 
@@ -366,7 +381,7 @@ Proof.
 (* Exec *)
   split. eapply exec_trans. eexact EX1.
   apply exec_instrs_incr with s1. eauto with rtlg.
-  exact EX2. 
+  eexact EX2. traceEq.
 (* Match-env *)
   split. 
   apply match_env_update_var with rs1 r s s0; auto.
@@ -387,13 +402,13 @@ Qed.
 Lemma transl_expr_Eload_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem)
     (chunk : memory_chunk) (addr : addressing) 
-    (al : exprlist) (e1 : env) (m1 : mem) (v : val) 
+    (al : exprlist) (t: trace) (e1 : env) (m1 : mem) (v : val) 
     (vl : list val) (a: val),
-  eval_exprlist ge sp le e m al e1 m1 vl ->
-  transl_exprlist_correct sp le e m al e1 m1 vl ->
+  eval_exprlist ge sp le e m al t e1 m1 vl ->
+  transl_exprlist_correct sp le e m al t e1 m1 vl ->
   eval_addressing ge sp addr vl = Some a ->
   Mem.loadv chunk m1 a = Some v ->
-  transl_expr_correct sp le e m (Eload chunk addr al) e1 m1 v.
+  transl_expr_correct sp le e m (Eload chunk addr al) t e1 m1 v.
 Proof.
   intros; red; intros. simpl in TE. monadInv TE. intro EQ1. clear TE.
   simpl in MUT.
@@ -407,7 +422,7 @@ Proof.
   apply exec_instrs_incr with s1. eauto with rtlg.
   apply exec_one. eapply exec_Iload. eauto with rtlg.
   rewrite RES1. rewrite (@eval_addressing_preserved _ _ ge tge).
-  eexact H1. exact symbols_preserved. assumption.
+  eexact H1. exact symbols_preserved. assumption. traceEq.
 (* Match-env *)
   split. eapply match_env_update_temp. assumption. inversion TRG. assumption.
 (* Result *)
@@ -425,16 +440,17 @@ Qed.
 Lemma transl_expr_Estore_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem)
     (chunk : memory_chunk) (addr : addressing) 
-    (al : exprlist) (b : expr) (e1 : env) (m1 : mem) 
-    (vl : list val) (e2 : env) (m2 m3 : mem) 
+    (al : exprlist) (b : expr) (t t1: trace) (e1 : env) (m1 : mem) 
+    (vl : list val) (t2: trace) (e2 : env) (m2 m3 : mem) 
     (v : val) (a: val),
-  eval_exprlist ge sp le e m al e1 m1 vl ->
-  transl_exprlist_correct sp le e m al e1 m1 vl ->
-  eval_expr ge sp le e1 m1 b e2 m2 v ->
-  transl_expr_correct sp le e1 m1 b e2 m2 v ->
+  eval_exprlist ge sp le e m al t1 e1 m1 vl ->
+  transl_exprlist_correct sp le e m al t1 e1 m1 vl ->
+  eval_expr ge sp le e1 m1 b t2 e2 m2 v ->
+  transl_expr_correct sp le e1 m1 b t2 e2 m2 v ->
   eval_addressing ge sp addr vl = Some a -> 
   Mem.storev chunk m2 a v = Some m3 ->
-  transl_expr_correct sp le e m (Estore chunk addr al b) e2 m3 v.
+  t = t1 ** t2 ->
+  transl_expr_correct sp le e m (Estore chunk addr al b) t e2 m3 v.
 Proof.
   intros; red; intros. simpl in TE; monadInv TE. intro EQ2; clear TE.
   simpl in MUT. 
@@ -467,10 +483,11 @@ Proof.
     tauto. right. apply sym_not_equal. 
     apply valid_fresh_different with s. inversion TRG; assumption.
     assumption.
-  rewrite H5; rewrite RES1. 
+  rewrite H6; rewrite RES1. 
   rewrite (@eval_addressing_preserved _ _ ge tge).
   eexact H3. exact symbols_preserved. 
   rewrite RES2. assumption.
+  reflexivity. traceEq. 
 (* Match-env *)
   split. assumption.
 (* Result *)
@@ -488,18 +505,20 @@ Qed.
 
 Lemma transl_expr_Ecall_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem) 
-    (sig : signature) (a : expr) (bl : exprlist) 
-    (e1 e2 : env) (m1 m2 m3 : mem) (vf : val) 
-    (vargs : list val) (vres : val) (f : Cminor.function),
-  eval_expr ge sp le e m a e1 m1 vf ->
-  transl_expr_correct sp le e m a e1 m1 vf ->
-  eval_exprlist ge sp le e1 m1 bl e2 m2 vargs ->
-  transl_exprlist_correct sp le e1 m1 bl e2 m2 vargs ->
+    (sig : signature) (a : expr) (bl : exprlist) (t t1: trace)
+    (e1: env) (m1: mem) (t2: trace) (e2 : env) (m2 : mem) 
+    (t3: trace) (m3: mem) (vf : val) 
+    (vargs : list val) (vres : val) (f : Cminor.fundef),
+  eval_expr ge sp le e m a t1 e1 m1 vf ->
+  transl_expr_correct sp le e m a t1 e1 m1 vf ->
+  eval_exprlist ge sp le e1 m1 bl t2 e2 m2 vargs ->
+  transl_exprlist_correct sp le e1 m1 bl t2 e2 m2 vargs ->
   Genv.find_funct ge vf = Some f ->
-  Cminor.fn_sig f = sig ->
-  eval_funcall ge m2 f vargs m3 vres ->
-  transl_function_correct m2 f vargs m3 vres ->
-  transl_expr_correct sp le e m (Ecall sig a bl) e2 m3 vres.
+  Cminor.funsig f = sig ->
+  eval_funcall ge m2 f vargs t3 m3 vres ->
+  transl_function_correct m2 f vargs t3 m3 vres ->
+  t = t1 ** t2 ** t3 ->
+  transl_expr_correct sp le e m (Ecall sig a bl) t e2 m3 vres.
 Proof.
   intros. red; simpl; intros.
   monadInv TE. intro EQ3. clear TE.
@@ -530,7 +549,7 @@ Proof.
   generalize (H6 tf TF). intro EXF.
 
   assert (EX3: exec_instrs tge (st_code s2) sp n rs2 m2
-                     nd (rs2#rd <- vres) m3).
+                     t3 nd (rs2#rd <- vres) m3).
   apply exec_one. eapply exec_Icall.
   eauto with rtlg. simpl. replace (rs2#r) with vf. eexact TFIND.
   rewrite <- RES1. symmetry. apply OTHER2.
@@ -543,10 +562,7 @@ Proof.
   tauto. byContradiction. apply valid_fresh_absurd with r s0.
   eauto with rtlg. assumption.
   tauto.
-  generalize TF. unfold transl_function.
-  destruct (transl_fun f init_state).
-  intro; discriminate. destruct p. intros. injection TF0. intro.
-  rewrite <- H7; simpl. auto.
+  generalize (sig_transl_function _ _ TF). congruence.
   rewrite RES2. assumption.
 
   exists (rs2#rd <- vres).
@@ -555,7 +571,7 @@ Proof.
   apply exec_instrs_incr with s3. eauto with rtlg.
   eapply exec_trans. eexact EX2. 
   apply exec_instrs_incr with s2. eauto with rtlg.
-  exact EX3.
+  eexact EX3. reflexivity. traceEq. 
 (* Match env *)
   split. apply match_env_update_temp. assumption.
   inversion TRG. assumption.
@@ -591,13 +607,14 @@ Qed.
 
 Lemma transl_expr_Econdition_correct:
  forall (sp: val) (le : letenv) (e : env) (m : mem) 
-    (a : condexpr) (b c : expr) (e1 : env) (m1 : mem) 
-    (v1 : bool) (e2 : env) (m2 : mem) (v2 : val),
-  eval_condexpr ge sp le e m a e1 m1 v1 ->
-  transl_condition_correct sp le e m a e1 m1 v1 ->
-  eval_expr ge sp le e1 m1 (if v1 then b else c) e2 m2 v2 ->
-  transl_expr_correct sp le e1 m1 (if v1 then b else c) e2 m2 v2 ->
-  transl_expr_correct sp le e m (Econdition a b c) e2 m2 v2.
+    (a : condexpr) (b c : expr) (t t1: trace) (e1 : env) (m1 : mem) 
+    (v1 : bool) (t2: trace) (e2 : env) (m2 : mem) (v2 : val),
+  eval_condexpr ge sp le e m a t1 e1 m1 v1 ->
+  transl_condition_correct sp le e m a t1 e1 m1 v1 ->
+  eval_expr ge sp le e1 m1 (if v1 then b else c) t2 e2 m2 v2 ->
+  transl_expr_correct sp le e1 m1 (if v1 then b else c) t2 e2 m2 v2 ->
+  t = t1 ** t2 ->
+  transl_expr_correct sp le e m (Econdition a b c) t e2 m2 v2.
 Proof.
   intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE.
   simpl in MUT. 
@@ -619,7 +636,7 @@ Proof.
 (* Exec *)
   split. eapply exec_trans. eexact EX1. 
   apply exec_instrs_incr with s1. eauto with rtlg.
-  exact EX2.
+  eexact EX2. auto.
 (* Match-env *)
   split. assumption.
 (* Result value *)
@@ -639,7 +656,7 @@ Proof.
 (* Exec *)
   split. eapply exec_trans. eexact EX1. 
   apply exec_instrs_incr with s0. eauto with rtlg.
-  exact EX2.
+  eexact EX2. auto.
 (* Match-env *)
   split. assumption.
 (* Result value *)
@@ -653,13 +670,14 @@ Qed.
 
 Lemma transl_expr_Elet_correct:
   forall (sp: val) (le : letenv) (e : env) (m : mem) 
-    (a b : expr) (e1 : env) (m1 : mem) (v1 : val) 
-    (e2 : env) (m2 : mem) (v2 : val),
-  eval_expr ge sp le e m a e1 m1 v1 ->
-  transl_expr_correct sp le e m a e1 m1 v1 ->
-  eval_expr ge sp (v1 :: le) e1 m1 b e2 m2 v2 ->
-  transl_expr_correct sp (v1 :: le) e1 m1 b e2 m2 v2 ->
-  transl_expr_correct sp le e m (Elet a b) e2 m2 v2.
+    (a b : expr) (t t1: trace) (e1 : env) (m1 : mem) (v1 : val) 
+    (t2: trace) (e2 : env) (m2 : mem) (v2 : val),
+  eval_expr ge sp le e m a t1 e1 m1 v1 ->
+  transl_expr_correct sp le e m a t1 e1 m1 v1 ->
+  eval_expr ge sp (v1 :: le) e1 m1 b t2 e2 m2 v2 ->
+  transl_expr_correct sp (v1 :: le) e1 m1 b t2 e2 m2 v2 ->
+  t = t1 ** t2 ->
+  transl_expr_correct sp le e m (Elet a b) t e2 m2 v2.
 Proof.
   intros; red; intros.
   simpl in TE; monadInv TE. intro EQ1.
@@ -678,17 +696,17 @@ Proof.
   assert (TRG2: target_reg_ok s0 (add_letvar map r) mut b rd).
   inversion TRG. apply target_reg_other. 
   unfold reg_in_map, add_letvar; simpl. red; intro.
-  elim H10; intro. apply H3. left. assumption.
-  elim H11; intro. apply valid_fresh_absurd with rd s.
-  assumption. rewrite <- H12. eauto with rtlg.
-  apply H3. right. assumption.
+  elim H11; intro. apply H4. left. assumption.
+  elim H12; intro. apply valid_fresh_absurd with rd s.
+  assumption. rewrite <- H13. eauto with rtlg.
+  apply H4. right. assumption.
   eauto with rtlg.
   generalize (H2 _ _ _ _ _ _ _ _ MWF2 EQ0 ME2 MUT2 TRG2).
   intros [rs2 [EX2 [ME3 [RES2 OTHER2]]]].
   exists rs2.
 (* Exec *)
   split. eapply exec_trans. eexact EX1. 
-  apply exec_instrs_incr with s1. eauto with rtlg. exact EX2.
+  apply exec_instrs_incr with s1. eauto with rtlg. eexact EX2. auto.
 (* Match-env *)
   split. apply mk_match_env. exact (me_vars _ _ _ _ ME3). 
   generalize (me_letvars _ _ _ _ ME3). 
@@ -699,21 +717,21 @@ Proof.
   intros. transitivity (rs1#r0). 
   apply OTHER2. eauto with rtlg. 
   unfold mutated_reg. unfold add_letvar; simpl. assumption.
-  elim H5; intro. left. 
+  elim H6; intro. left. 
   unfold reg_in_map, add_letvar; simpl.
-  unfold reg_in_map in H6; tauto.
+  unfold reg_in_map in H7; tauto.
   tauto.
   apply OTHER1. eauto with rtlg.
   assumption. 
   right. red; intro. apply valid_fresh_absurd with r0 s.
-  assumption. rewrite H6. eauto with rtlg.
+  assumption. rewrite H7. eauto with rtlg.
 Qed.
 
 Lemma transl_expr_Eletvar_correct:
   forall (sp: val) (le : list val) (e : env) 
     (m : mem) (n : nat) (v : val),
   nth_error le n = Some v ->
-  transl_expr_correct sp le e m (Eletvar n) e m v.
+  transl_expr_correct sp le e m (Eletvar n) E0 e m v.
 Proof.
   intros; red; intros. 
   simpl in TE; monadInv TE. intro EQ1.
@@ -746,9 +764,46 @@ Proof.
   intro; monadSimpl.
 Qed.
 
+Lemma transl_expr_Ealloc_correct:
+  forall (sp: val) (le : letenv) (e : env) (m : mem) 
+    (a : expr) (t: trace) (e1 : env) (m1 : mem) (n: int)
+    (m2: mem) (b: block),
+  eval_expr ge sp le e m a t e1 m1 (Vint n) ->
+  transl_expr_correct sp le e m a t e1 m1 (Vint n) ->
+  Mem.alloc m1 0 (Int.signed n) = (m2, b) ->
+  transl_expr_correct sp le e m (Ealloc a) t e1 m2 (Vptr b Int.zero).
+Proof.
+  intros until b; intros EE TEC ALLOC; red; intros.
+  simpl in TE. monadInv TE. intro EQ1.
+  simpl in MUT.
+  assert (TRG': target_reg_ok s1 map mut a r); eauto with rtlg.
+  assert (MWF': map_wf map s1). eauto with rtlg.
+  generalize (TEC _ _ _ _ _ _ _ _ MWF' EQ1 ME MUT TRG').
+  intros [rs1 [EX1 [ME1 [RR1 RO1]]]].
+  exists (rs1#rd <- (Vptr b Int.zero)).
+(* Exec *)
+  split. eapply exec_trans. eexact EX1. 
+  apply exec_instrs_incr with s1. eauto with rtlg.
+  apply exec_one; eapply exec_Ialloc. eauto with rtlg.
+  eexact RR1. assumption. traceEq. 
+(* Match-env *)
+  split. inversion TRG. eauto with rtlg.
+(* Result *)
+  split. apply Regmap.gss.
+(* Other regs *)
+  intros. rewrite Regmap.gso.
+  apply RO1. eauto with rtlg. assumption.
+  case (Reg.eq r0 r); intro.
+  subst r0. left. elim (alloc_reg_fresh_or_in_map _ _ _ _ _ _ MWF EQ); intro. 
+  auto. byContradiction; eauto with rtlg.
+  right; assumption.
+  elim H1; intro. red; intro. subst r0. inversion TRG. contradiction. 
+  auto.
+Qed.
+
 Lemma transl_condition_CEtrue_correct:
   forall (sp: val) (le : letenv) (e : env) (m : mem),
-  transl_condition_correct sp le e m CEtrue e m true.
+  transl_condition_correct sp le e m CEtrue E0 e m true.
 Proof.
   intros; red; intros. simpl in TE; monadInv TE. subst ns.
   exists rs. split. apply exec_refl. split. auto. auto.
@@ -756,7 +811,7 @@ Qed.
 
 Lemma transl_condition_CEfalse_correct:
   forall (sp: val) (le : letenv) (e : env) (m : mem),
-  transl_condition_correct sp le e m CEfalse e m false.
+  transl_condition_correct sp le e m CEfalse E0 e m false.
 Proof.
   intros; red; intros. simpl in TE; monadInv TE. subst ns.
   exists rs. split. apply exec_refl. split. auto. auto.
@@ -764,12 +819,12 @@ Qed.
 
 Lemma transl_condition_CEcond_correct:
   forall (sp: val) (le : letenv) (e : env) (m : mem)
-    (cond : condition) (al : exprlist) (e1 : env) 
+    (cond : condition) (al : exprlist) (t1: trace) (e1 : env) 
     (m1 : mem) (vl : list val) (b : bool),
-  eval_exprlist ge sp le e m al e1 m1 vl ->
-  transl_exprlist_correct sp le e m al e1 m1 vl ->
+  eval_exprlist ge sp le e m al t1 e1 m1 vl ->
+  transl_exprlist_correct sp le e m al t1 e1 m1 vl ->
   eval_condition cond vl =  Some b ->
-  transl_condition_correct sp le e m (CEcond cond al) e1 m1 b.
+  transl_condition_correct sp le e m (CEcond cond al) t1 e1 m1 b.
 Proof.
   intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE.
   assert (MWF1: map_wf map s1). eauto with rtlg.
@@ -788,6 +843,7 @@ Proof.
   rewrite RES1. assumption.
   eapply exec_Icond_false. eauto with rtlg. 
   rewrite RES1. assumption.
+  traceEq.
 (* Match-env *)
   split. assumption.
 (* Regs *)
@@ -800,13 +856,14 @@ Qed.
 
 Lemma transl_condition_CEcondition_correct:
   forall (sp: val) (le : letenv) (e : env) (m : mem)
-    (a b c : condexpr) (e1 : env) (m1 : mem) 
-    (vb1 : bool) (e2 : env) (m2 : mem) (vb2 : bool),
-  eval_condexpr ge sp le e m a e1 m1 vb1 ->
-  transl_condition_correct sp le e m a e1 m1 vb1 ->
-  eval_condexpr ge sp le e1 m1 (if vb1 then b else c) e2 m2 vb2 ->
-  transl_condition_correct sp le e1 m1 (if vb1 then b else c) e2 m2 vb2 ->
-  transl_condition_correct sp le e m (CEcondition a b c) e2 m2 vb2.
+    (a b c : condexpr) (t t1: trace) (e1 : env) (m1 : mem) 
+    (vb1 : bool) (t2: trace) (e2 : env) (m2 : mem) (vb2 : bool),
+  eval_condexpr ge sp le e m a t1 e1 m1 vb1 ->
+  transl_condition_correct sp le e m a t1 e1 m1 vb1 ->
+  eval_condexpr ge sp le e1 m1 (if vb1 then b else c) t2 e2 m2 vb2 ->
+  transl_condition_correct sp le e1 m1 (if vb1 then b else c) t2 e2 m2 vb2 ->
+  t = t1 ** t2 ->
+  transl_condition_correct sp le e m (CEcondition a b c) t e2 m2 vb2.
 Proof.
   intros; red; intros. simpl in TE; monadInv TE. intro EQ1; clear TE.
   simpl in MUT.
@@ -823,7 +880,7 @@ Proof.
   exists rs2.
   split. eapply exec_trans. eexact EX1. 
   apply exec_instrs_incr with s1. eauto with rtlg.
-  exact EX2.
+  eexact EX2. auto.
   split. assumption. 
   intros. transitivity (rs1#r). 
   apply OTHER2; eauto with rtlg.
@@ -835,7 +892,7 @@ Proof.
   exists rs2.
   split. eapply exec_trans. eexact EX1. 
   apply exec_instrs_incr with s0. eauto with rtlg.
-  exact EX2.
+  eexact EX2. auto.
   split. assumption. 
   intros. transitivity (rs1#r). 
   apply OTHER2; eauto with rtlg.
@@ -844,7 +901,7 @@ Qed.
  
 Lemma transl_exprlist_Enil_correct:
   forall (sp: val) (le : letenv) (e : env) (m : mem),
-  transl_exprlist_correct sp le e m Enil e m nil.
+  transl_exprlist_correct sp le e m Enil E0 e m nil.
 Proof.
   intros; red; intros. 
   generalize TE. simpl. destruct rl; monadSimpl. 
@@ -857,17 +914,18 @@ Qed.
 
 Lemma transl_exprlist_Econs_correct:
   forall (sp: val) (le : letenv) (e : env) (m : mem) 
-    (a : expr) (bl : exprlist) (e1 : env) (m1 : mem) 
-    (v : val) (e2 : env) (m2 : mem) (vl : list val),
-  eval_expr ge sp le e m a e1 m1 v ->
-  transl_expr_correct sp le e m a e1 m1 v ->
-  eval_exprlist ge sp le e1 m1 bl e2 m2 vl ->
-  transl_exprlist_correct sp le e1 m1 bl e2 m2 vl ->
-  transl_exprlist_correct sp le e m (Econs a bl) e2 m2 (v :: vl).
+    (a : expr) (bl : exprlist) (t t1: trace) (e1 : env) (m1 : mem) 
+    (v : val) (t2: trace) (e2 : env) (m2 : mem) (vl : list val),
+  eval_expr ge sp le e m a t1 e1 m1 v ->
+  transl_expr_correct sp le e m a t1 e1 m1 v ->
+  eval_exprlist ge sp le e1 m1 bl t2 e2 m2 vl ->
+  transl_exprlist_correct sp le e1 m1 bl t2 e2 m2 vl ->
+  t = t1 ** t2 ->
+  transl_exprlist_correct sp le e m (Econs a bl) t e2 m2 (v :: vl).
 Proof.
   intros. red. intros. 
   inversion TRG.
-  rewrite <- H10 in TE. simpl in TE. monadInv TE. intro EQ1.
+  rewrite <- H11 in TE. simpl in TE. monadInv TE. intro EQ1.
   simpl in MUT.
   assert (MUT1: incl (mutated_expr a) mut); eauto with coqlib.
   assert (MUT2: incl (mutated_exprlist bl) mut); eauto with coqlib.
@@ -875,12 +933,13 @@ Proof.
   assert (TRG1: target_reg_ok s1 map mut a r); eauto with rtlg.
   generalize (H0 _ _ _ _ _ _ _ _ MWF1 EQ1 ME MUT1 TRG1).
   intros [rs1 [EX1 [ME1 [RES1 OTHER1]]]].
-  generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUT2 H11).
+  generalize (H2 _ _ _ _ _ _ _ _ MWF EQ ME1 MUT2 H12).
   intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]].
   exists rs2.
 (* Exec *)
   split. eapply exec_trans. eexact EX1. 
-  apply exec_instrs_incr with s1. eauto with rtlg. assumption.
+  apply exec_instrs_incr with s1. eauto with rtlg. 
+  eexact EX2. auto. 
 (* Match-env *)
   split. assumption.
 (* Results *)
@@ -894,22 +953,23 @@ Proof.
   transitivity (rs1#r0).
   apply OTHER2; auto. tauto. 
   apply OTHER1; auto. eauto with rtlg. 
-  elim H14; intro. left; assumption. right; apply sym_not_equal; tauto.
+  elim H15; intro. left; assumption. right; apply sym_not_equal; tauto.
 Qed.
 
-Lemma transl_funcall_correct:
-  forall (m : mem) (f : Cminor.function) (vargs : list val) 
-    (m1 : mem) (sp : block) (e e2 : env) (m2 : mem) 
-    (out : outcome) (vres : val),
+Lemma transl_funcall_internal_correct:
+  forall (m : mem) (f : Cminor.function)
+         (vargs : list val) (m1 : mem) (sp : block) (e : env) (t : trace)
+         (e2 : env) (m2 : mem) (out : outcome) (vres : val),
   Mem.alloc m 0 (fn_stackspace f) = (m1, sp) ->
-  set_locals (Cminor.fn_vars f) (set_params vargs (Cminor.fn_params f)) = e ->
-  exec_stmt ge (Vptr sp Int.zero) e m1 (fn_body f) e2 m2 out ->
-  transl_stmt_correct (Vptr sp Int.zero) e m1 (fn_body f) e2 m2 out ->
+  set_locals (fn_vars f) (set_params vargs (Cminor.fn_params f)) = e ->
+  exec_stmt ge (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out ->
+  transl_stmt_correct (Vptr sp Int.zero) e m1 (fn_body f) t e2 m2 out ->
   outcome_result_value out f.(Cminor.fn_sig).(sig_res) vres ->
-  transl_function_correct m f vargs (Mem.free m2 sp) vres.
+  transl_function_correct m (Internal f)
+            vargs t (Mem.free m2 sp) vres.
 Proof.
   intros; red; intros.
-  generalize TE. unfold transl_function.
+  generalize TE. unfold transl_fundef, transl_function; simpl.
   caseEq (transl_fun f init_state).
   intros; discriminate.
   intros ns s. unfold transl_fun. monadSimpl. 
@@ -934,30 +994,41 @@ Proof.
   apply map_wf_incr with s1. apply state_incr_trans with s2; eauto with rtlg.
   assumption.
 
-  assert (RRG: return_reg_ok s3 y0 (ret_reg (Cminor.fn_sig f) r)).
+  set (rr := ret_reg (Cminor.fn_sig f) r) in *.
+  assert (RRG: return_reg_ok s3 y0 rr).
   apply return_reg_ok_incr with s2. eauto with rtlg. 
-  apply new_reg_return_ok with s1; assumption.
+  unfold rr; apply new_reg_return_ok with s1; assumption.
 
   generalize (H2 _ _ _ _ _ _ _ _ _ rs MWF EQ3 ME OUT RRG).
   intros [rs1 [EX1 [ME1 MR1]]].
 
-  apply exec_funct with m1 n rs1 (ret_reg (Cminor.fn_sig f) r).
-  rewrite <- TF; simpl; assumption.
-  rewrite <- TF; simpl. exact EX1.
-  rewrite <- TF; simpl. apply instr_at_incr with s3.
+  rewrite <- TF. apply exec_funct_internal with m1 n rs1 rr; simpl.
+  assumption.
+  exact EX1.
+  apply instr_at_incr with s3.
   eauto with rtlg. discriminate. eauto with rtlg.
   generalize MR1. unfold match_return_outcome.
   generalize H3. unfold outcome_result_value.
-  unfold ret_reg; destruct (sig_res (Cminor.fn_sig f)).
+  unfold rr, ret_reg; destruct (sig_res (Cminor.fn_sig f)).
   unfold regmap_optget. destruct out; try contradiction.
   destruct o; try contradiction. intros; congruence.
   unfold regmap_optget. destruct out; contradiction||auto.
   destruct o; contradiction||auto.
 Qed.
 
+Lemma transl_funcall_external_correct:
+  forall (ef : external_function) (m : mem) (args : list val) (t: trace) (res : val),
+  event_match ef args t res ->
+  transl_function_correct m (External ef) args t m res.
+Proof.
+  intros; red; intros. unfold transl_function in TE; simpl in TE.
+  inversion TE; subst tf. 
+  apply exec_funct_external. auto.
+Qed.
+
 Lemma transl_stmt_Sskip_correct:
   forall (sp: val) (e : env) (m : mem),
-  transl_stmt_correct sp e m Sskip e m Out_normal.
+  transl_stmt_correct sp e m Sskip E0 e m Out_normal.
 Proof.
   intros; red; intros. simpl in TE. monadInv TE.
   subst s'; subst ns.
@@ -966,13 +1037,15 @@ Proof.
 Qed.
 
 Lemma transl_stmt_Sseq_continue_correct:
-  forall (sp : val) (e : env) (m : mem) (s1 : stmt) (e1 : env)
-         (m1 : mem) (s2 : stmt) (e2 : env) (m2 : mem) (out : outcome),
-  exec_stmt ge sp e m s1 e1 m1 Out_normal ->
-  transl_stmt_correct sp e m s1 e1 m1 Out_normal ->
-  exec_stmt ge sp e1 m1 s2 e2 m2 out ->
-  transl_stmt_correct sp e1 m1 s2 e2 m2 out ->
-  transl_stmt_correct sp e m (Sseq s1 s2) e2 m2 out.
+  forall (sp : val) (e : env) (m : mem) (t: trace) (s1 : stmt)
+         (t1: trace) (e1 : env) (m1 : mem) (s2 : stmt) (t2: trace)
+         (e2 : env) (m2 : mem) (out : outcome),
+  exec_stmt ge sp e m s1 t1 e1 m1 Out_normal ->
+  transl_stmt_correct sp e m s1 t1 e1 m1 Out_normal ->
+  exec_stmt ge sp e1 m1 s2 t2 e2 m2 out ->
+  transl_stmt_correct sp e1 m1 s2 t2 e2 m2 out ->
+  t = t1 ** t2 ->
+  transl_stmt_correct sp e m (Sseq s1 s2) t e2 m2 out.
 Proof.
   intros; red; intros. simpl in TE; monadInv TE. intro EQ0.
   assert (MWF1: map_wf map s0). eauto with rtlg.
@@ -987,18 +1060,18 @@ Proof.
 (* Exec *)
   split. eapply exec_trans. eexact EX1. 
   apply exec_instrs_incr with s0. eauto with rtlg.
-  exact EX2.
+  eexact EX2. auto.
 (* Match-env + return *)
   tauto.
 Qed.
 
 Lemma transl_stmt_Sseq_stop_correct:
-  forall (sp : val) (e : env) (m : mem) (s1 s2 : stmt) (e1 : env)
+  forall (sp : val) (e : env) (m : mem) (t: trace) (s1 s2 : stmt) (e1 : env)
          (m1 : mem) (out : outcome),
-  exec_stmt ge sp e m s1 e1 m1 out ->
-  transl_stmt_correct sp e m s1 e1 m1 out ->
+  exec_stmt ge sp e m s1 t e1 m1 out ->
+  transl_stmt_correct sp e m s1 t e1 m1 out ->
   out <> Out_normal ->
-  transl_stmt_correct sp e m (Sseq s1 s2) e1 m1 out.
+  transl_stmt_correct sp e m (Sseq s1 s2) t e1 m1 out.
 Proof.
   intros; red; intros. 
   simpl in TE; monadInv TE. intro EQ0; clear TE.
@@ -1010,11 +1083,11 @@ Proof.
 Qed.
 
 Lemma transl_stmt_Sexpr_correct:
-  forall (sp: val) (e : env) (m : mem) (a : expr) 
+  forall (sp: val) (e : env) (m : mem) (a : expr) (t: trace)
     (e1 : env) (m1 : mem) (v : val),
-  eval_expr ge sp nil e m a e1 m1 v ->
-  transl_expr_correct sp nil e m a e1 m1 v ->
-  transl_stmt_correct sp e m (Sexpr a) e1 m1 Out_normal.
+  eval_expr ge sp nil e m a t e1 m1 v ->
+  transl_expr_correct sp nil e m a t e1 m1 v ->
+  transl_stmt_correct sp e m (Sexpr a) t e1 m1 Out_normal.
 Proof.
   intros; red; intros.
   simpl in OUT. subst nd.
@@ -1028,17 +1101,18 @@ Qed.
 
 Lemma transl_stmt_Sifthenelse_correct:
   forall (sp: val) (e : env) (m : mem) (a : condexpr)
-    (sl1 sl2 : stmt) (e1 : env) (m1 : mem) 
-    (v1 : bool) (e2 : env) (m2 : mem) (out : outcome),
-  eval_condexpr ge sp nil e m a e1 m1 v1 ->
-  transl_condition_correct sp nil e m a e1 m1 v1 ->
-  exec_stmt ge sp e1 m1 (if v1 then sl1 else sl2) e2 m2 out ->
-  transl_stmt_correct sp e1 m1 (if v1 then sl1 else sl2) e2 m2 out ->
-  transl_stmt_correct sp e m (Sifthenelse a sl1 sl2) e2 m2 out.
+    (s1 s2 : stmt) (t t1: trace) (e1 : env) (m1 : mem) 
+    (v1 : bool) (t2: trace) (e2 : env) (m2 : mem) (out : outcome),
+  eval_condexpr ge sp nil e m a t1 e1 m1 v1 ->
+  transl_condition_correct sp nil e m a t1 e1 m1 v1 ->
+  exec_stmt ge sp e1 m1 (if v1 then s1 else s2) t2 e2 m2 out ->
+  transl_stmt_correct sp e1 m1 (if v1 then s1 else s2) t2 e2 m2 out ->
+  t = t1 ** t2 ->
+  transl_stmt_correct sp e m (Sifthenelse a s1 s2) t e2 m2 out.
 Proof.
   intros; red; intros until rs; intro MWF.
-  simpl. case (more_likely a sl1 sl2); monadSimpl; intro EQ2; intros.
-  assert (MWF1: map_wf map s1). eauto with rtlg.
+  simpl. case (more_likely a s1 s2); monadSimpl; intro EQ2; intros.
+  assert (MWF1: map_wf map s3). eauto with rtlg.
   generalize (H0 _ _ _ _ _ _ _ rs MWF1 EQ2 ME (incl_refl _)).
   intros [rs1 [EX1 [ME1 OTHER1]]].
   destruct v1.
@@ -1047,17 +1121,17 @@ Proof.
   generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 OUT RRG0).
   intros [rs2 [EX2 [ME2 MRE2]]].
   exists rs2. split.
-  eapply exec_trans. eexact EX1. apply exec_instrs_incr with s1.
-  eauto with rtlg. exact EX2.
+  eapply exec_trans. eexact EX1. apply exec_instrs_incr with s3.
+  eauto with rtlg. eexact EX2. auto.
   tauto.
   generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF EQ ME1 OUT RRG).
   intros [rs2 [EX2 [ME2 MRE2]]].
   exists rs2. split.
   eapply exec_trans. eexact EX1. apply exec_instrs_incr with s0.
-  eauto with rtlg. exact EX2.
+  eauto with rtlg. eexact EX2. auto.
   tauto.
 
-  assert (MWF1: map_wf map s1). eauto with rtlg.
+  assert (MWF1: map_wf map s3). eauto with rtlg.
   generalize (H0 _ _ _ _ _ _ _ rs MWF1 EQ2 ME (incl_refl _)).
   intros [rs1 [EX1 [ME1 OTHER1]]].
   destruct v1.
@@ -1065,27 +1139,28 @@ Proof.
   intros [rs2 [EX2 [ME2 MRE2]]].
   exists rs2. split.
   eapply exec_trans. eexact EX1. apply exec_instrs_incr with s0.
-  eauto with rtlg. exact EX2.
+  eauto with rtlg. eexact EX2. auto.
   tauto.
   assert (MWF0: map_wf map s0). eauto with rtlg.
   assert (RRG0: return_reg_ok s0 map rret). eauto with rtlg.
   generalize (H2 _ _ _ _ _ _ _ _ _ _ MWF0 EQ0 ME1 OUT RRG0).
   intros [rs2 [EX2 [ME2 MRE2]]].
   exists rs2. split.
-  eapply exec_trans. eexact EX1. apply exec_instrs_incr with s1.
-  eauto with rtlg. exact EX2.
+  eapply exec_trans. eexact EX1. apply exec_instrs_incr with s3.
+  eauto with rtlg. eexact EX2. auto.
   tauto.
 Qed.
 
 Lemma transl_stmt_Sloop_loop_correct:
-  forall (sp: val) (e : env) (m : mem) (sl : stmt) 
-    (e1 : env) (m1 : mem) (e2 : env) (m2 : mem) 
+  forall (sp: val) (e : env) (m : mem) (sl : stmt) (t t1: trace)
+    (e1 : env) (m1 : mem) (t2: trace) (e2 : env) (m2 : mem) 
     (out : outcome),
-  exec_stmt ge sp e m sl e1 m1 Out_normal ->
-  transl_stmt_correct sp e m sl e1 m1 Out_normal ->
-  exec_stmt ge sp e1 m1 (Sloop sl) e2 m2 out ->
-  transl_stmt_correct sp e1 m1 (Sloop sl) e2 m2 out ->
-  transl_stmt_correct sp e m (Sloop sl) e2 m2 out.
+  exec_stmt ge sp e m sl t1 e1 m1 Out_normal ->
+  transl_stmt_correct sp e m sl t1 e1 m1 Out_normal ->
+  exec_stmt ge sp e1 m1 (Sloop sl) t2 e2 m2 out ->
+  transl_stmt_correct sp e1 m1 (Sloop sl) t2 e2 m2 out ->
+  t = t1 ** t2 ->
+  transl_stmt_correct sp e m (Sloop sl) t e2 m2 out.
 Proof.
   intros; red; intros.
   generalize TE. simpl. monadSimpl. subst s2; subst n0. intros.
@@ -1107,22 +1182,23 @@ Proof.
   apply exec_instrs_extends with s1. 
   eapply update_instr_extends.
   eexact EQ. eauto with rtlg. eexact EQ1. eexact EX1.
-  apply exec_trans with ns rs1 m1.
+  apply exec_trans with E0 ns rs1 m1 t2.
   apply exec_one. apply exec_Inop. 
   generalize EQ1. unfold update_instr. 
   case (plt n (st_nextnode s1)); intro; monadSimpl.
-  rewrite <- H4. simpl. apply PTree.gss.
+  rewrite <- H5. simpl. apply PTree.gss.
   exact EX2.
+  reflexivity. traceEq. 
   tauto.
 Qed.
 
 Lemma transl_stmt_Sloop_stop_correct:
-  forall (sp: val) (e : env) (m : mem) (sl : stmt) 
+  forall (sp: val) (e : env) (m : mem) (t: trace) (sl : stmt) 
     (e1 : env) (m1 : mem) (out : outcome),
-  exec_stmt ge sp e m sl e1 m1 out ->
-  transl_stmt_correct sp e m sl e1 m1 out ->
+  exec_stmt ge sp e m sl t e1 m1 out ->
+  transl_stmt_correct sp e m sl t e1 m1 out ->
   out <> Out_normal ->
-  transl_stmt_correct sp e m (Sloop sl) e1 m1 out.
+  transl_stmt_correct sp e m (Sloop sl) t e1 m1 out.
 Proof.
   intros; red; intros.
   simpl in TE. monadInv TE. subst s2; subst n0.
@@ -1145,11 +1221,11 @@ Proof.
 Qed.  
 
 Lemma transl_stmt_Sblock_correct:
-  forall (sp: val) (e : env) (m : mem) (sl : stmt) 
+  forall (sp: val) (e : env) (m : mem) (sl : stmt) (t: trace)
     (e1 : env) (m1 : mem) (out : outcome),
-  exec_stmt ge sp e m sl e1 m1 out ->
-  transl_stmt_correct sp e m sl e1 m1 out ->
-  transl_stmt_correct sp e m (Sblock sl) e1 m1 (outcome_block out).
+  exec_stmt ge sp e m sl t e1 m1 out ->
+  transl_stmt_correct sp e m sl t e1 m1 out ->
+  transl_stmt_correct sp e m (Sblock sl) t e1 m1 (outcome_block out).
 Proof.
   intros; red; intros. simpl in TE. 
   assert (OUT': outcome_node out ncont (ncont :: nexits) nret nd).
@@ -1180,7 +1256,7 @@ Qed.
 
 Lemma transl_stmt_Sexit_correct:
   forall (sp: val) (e : env) (m : mem) (n : nat),
-  transl_stmt_correct sp e m (Sexit n) e m (Out_exit n).
+  transl_stmt_correct sp e m (Sexit n) E0 e m (Out_exit n).
 Proof.
   intros; red; intros. 
   simpl in TE. simpl in OUT. 
@@ -1194,7 +1270,7 @@ Lemma transl_switch_correct:
   transl_switch r nexits cases default s = OK ns s' ->
   nth_error nexits (switch_target i default cases) = Some nd ->
   rs#r = Vint i ->
-  exec_instrs tge s'.(st_code) sp ns rs m nd rs m.
+  exec_instrs tge s'.(st_code) sp ns rs m E0 nd rs m.
 Proof.
   induction cases; simpl; intros.
   generalize (transl_exit_correct _ _ _ _ _ H). intros.
@@ -1202,23 +1278,23 @@ Proof.
   destruct a as [key1 exit1]. monadInv H. clear H. intro EQ1.
   caseEq (Int.eq i key1); intro IEQ; rewrite IEQ in H0.
   (* i = key1 *)
-  apply exec_trans with n0 rs m. apply exec_one. 
+  apply exec_trans with E0 n0 rs m E0. apply exec_one. 
   eapply exec_Icond_true. eauto with rtlg. simpl. rewrite H1. congruence.
   generalize (transl_exit_correct _ _ _ _ _ EQ0); intro.
-  assert (n0 = nd). congruence. subst n0. apply exec_refl.
+  assert (n0 = nd). congruence. subst n0. apply exec_refl. traceEq.
   (* i <> key1 *)
-  apply exec_trans with n rs m. apply exec_one.
+  apply exec_trans with E0 n rs m E0. apply exec_one.
   eapply exec_Icond_false. eauto with rtlg. simpl. rewrite H1. congruence.
-  apply exec_instrs_incr with s0; eauto with rtlg. 
+  apply exec_instrs_incr with s0; eauto with rtlg. traceEq.
 Qed.
 
 Lemma transl_stmt_Sswitch_correct:
   forall (sp : val) (e : env) (m : mem) (a : expr)
-         (cases : list (int * nat)) (default : nat) (e1 : env) (m1 : mem)
-         (n : int),
-  eval_expr ge sp nil e m a e1 m1 (Vint n) ->
-  transl_expr_correct sp nil e m a e1 m1 (Vint n) ->
-  transl_stmt_correct sp e m (Sswitch a cases default) e1 m1
+         (cases : list (int * nat)) (default : nat) 
+         (t1 : trace) (e1 : env) (m1 : mem) (n : int),
+  eval_expr ge sp nil e m a t1 e1 m1 (Vint n) ->
+  transl_expr_correct sp nil e m a t1 e1 m1 (Vint n) ->
+  transl_stmt_correct sp e m (Sswitch a cases default) t1 e1 m1
          (Out_exit (switch_target n default cases)).
 Proof.
   intros; red; intros. monadInv TE. clear TE; intros EQ1.
@@ -1234,14 +1310,14 @@ Proof.
   (* execution *)
   split. eapply exec_trans. eexact EXEC1. 
   apply exec_instrs_incr with s1. eauto with rtlg.
-  eapply transl_switch_correct; eauto. 
+  eapply transl_switch_correct; eauto. traceEq. 
   (* match_env & match_reg *)
   tauto.
 Qed.
 
 Lemma transl_stmt_Sreturn_none_correct:
   forall (sp: val) (e : env) (m : mem),
-  transl_stmt_correct sp e m (Sreturn None) e m (Out_return None).
+  transl_stmt_correct sp e m (Sreturn None) E0 e m (Out_return None).
 Proof.
   intros; red; intros. generalize TE. simpl.
   destruct rret; monadSimpl. 
@@ -1250,11 +1326,11 @@ Proof.
 Qed.
 
 Lemma transl_stmt_Sreturn_some_correct:
-  forall (sp: val) (e : env) (m : mem) (a : expr) 
+  forall (sp: val) (e : env) (m : mem) (a : expr) (t: trace)
     (e1 : env) (m1 : mem) (v : val),
-  eval_expr ge sp nil e m a e1 m1 v ->
-  transl_expr_correct sp nil e m a e1 m1 v ->
-  transl_stmt_correct sp e m (Sreturn (Some a)) e1 m1 (Out_return (Some v)).
+  eval_expr ge sp nil e m a t e1 m1 v ->
+  transl_expr_correct sp nil e m a t e1 m1 v ->
+  transl_stmt_correct sp e m (Sreturn (Some a)) t e1 m1 (Out_return (Some v)).
 Proof.
   intros; red; intros. generalize TE; simpl.
   destruct rret. intro EQ.
@@ -1278,9 +1354,9 @@ Scheme eval_expr_ind_5 := Minimality for eval_expr Sort Prop
   with exec_stmt_ind_5 := Minimality for exec_stmt Sort Prop.
 
 Theorem transl_function_correctness:
-  forall m f vargs m' vres,
-  eval_funcall ge m f vargs m' vres ->
-  transl_function_correct m f vargs m' vres.
+  forall m f vargs t m' vres,
+  eval_funcall ge m f vargs t m' vres ->
+  transl_function_correct m f vargs t m' vres.
 Proof
   (eval_funcall_ind_5 ge
     transl_expr_correct
@@ -1298,13 +1374,15 @@ Proof
     transl_expr_Econdition_correct
     transl_expr_Elet_correct
     transl_expr_Eletvar_correct
+    transl_expr_Ealloc_correct
     transl_condition_CEtrue_correct
     transl_condition_CEfalse_correct
     transl_condition_CEcond_correct
     transl_condition_CEcondition_correct
     transl_exprlist_Enil_correct
     transl_exprlist_Econs_correct
-    transl_funcall_correct
+    transl_funcall_internal_correct
+    transl_funcall_external_correct
     transl_stmt_Sskip_correct
     transl_stmt_Sexpr_correct
     transl_stmt_Sifthenelse_correct
@@ -1319,26 +1397,23 @@ Proof
     transl_stmt_Sreturn_some_correct).
 
 Theorem transl_program_correct:
-  forall (r: val),
-  Cminor.exec_program prog r ->
-  RTL.exec_program tprog r.
+  forall (t: trace) (r: val),
+  Cminor.exec_program prog t r ->
+  RTL.exec_program tprog t r.
 Proof.
-  intros r [b [f [m [SYMB [FUNC [SIG EVAL]]]]]].
+  intros t r [b [f [m [SYMB [FUNC [SIG EVAL]]]]]].
   generalize (function_ptr_translated _ _ FUNC).
   intros [tf [TFIND TRANSLF]].
   red; exists b; exists tf; exists m.
   split. rewrite symbols_preserved. 
   replace (prog_main tprog) with (prog_main prog).
   assumption. 
-  symmetry; apply transform_partial_program_main with transl_function.
+  symmetry; apply transform_partial_program_main with transl_fundef.
   exact TRANSL.
   split. exact TFIND.
-  split. generalize TRANSLF. unfold transl_function.
-  destruct (transl_fun f init_state).
-  intro; discriminate. destruct p; intro EQ; injection EQ; intro EQ1.
-  rewrite <- EQ1. simpl. congruence. 
-  rewrite (Genv.init_mem_transf_partial transl_function prog TRANSL).
-  exact (transl_function_correctness _ _ _ _ _ EVAL _ TRANSLF).
+  split. generalize (sig_transl_function _ _ TRANSLF). congruence.
+  unfold fundef; rewrite (Genv.init_mem_transf_partial transl_fundef prog TRANSL).
+  exact (transl_function_correctness _ _ _ _ _ _ EVAL _ TRANSLF).
 Qed.
 
 End CORRECTNESS.