From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:08:29 +0000 Subject: 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 --- backend/RTLgenproof.v | 503 +++++++++++++++++++++++++++++--------------------- 1 file changed, 289 insertions(+), 214 deletions(-) (limited to 'backend/RTLgenproof.v') diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index d34bae96..24cc41b4 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. -- cgit