From 213bf38509f4f92545d4c5749c25a55b9a9dda36 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 3 Aug 2009 15:32:27 +0000 Subject: Transition semantics for Clight and Csharpminor git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgenproof.v | 1525 +++++++++++++++++++++++--------------------- 1 file changed, 799 insertions(+), 726 deletions(-) (limited to 'cfrontend/Cminorgenproof.v') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index f256bb2..1a68c10 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -23,6 +23,7 @@ Require Import Values. Require Import Mem. Require Import Events. Require Import Globalenvs. +Require Import Smallstep. Require Import Csharpminor. Require Import Op. Require Import Cminor. @@ -36,8 +37,10 @@ Variable prog: Csharpminor.program. Variable tprog: program. Hypothesis TRANSL: transl_program prog = OK tprog. Let ge : Csharpminor.genv := Genv.globalenv prog. -Let tge: genv := Genv.globalenv tprog. +Let gvare : gvarenv := global_var_env prog. +Let gve := (ge, gvare). Let gce : compilenv := build_global_compilenv prog. +Let tge: genv := Genv.globalenv tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -58,6 +61,14 @@ Lemma functions_translated: Genv.find_funct tge v = Some tf /\ transl_fundef gce f = OK tf. Proof (Genv.find_funct_transf_partial2 (transl_fundef gce) transl_globvar TRANSL). +Lemma sig_preserved_body: + forall f tf cenv size, + transl_funbody cenv size f = OK tf -> + tf.(fn_sig) = f.(Csharpminor.fn_sig). +Proof. + intros. monadInv H. reflexivity. +Qed. + Lemma sig_preserved: forall f tf, transl_fundef gce f = OK tf -> @@ -65,8 +76,8 @@ Lemma sig_preserved: Proof. intros until tf; destruct f; simpl. unfold transl_function. destruct (build_compilenv gce f). - case (zle z Int.max_signed); simpl; try congruence. - intros. monadInv H. monadInv EQ. reflexivity. + case (zle z Int.max_signed); simpl bind; try congruence. + intros. monadInv H. simpl. eapply sig_preserved_body; eauto. intro. inv H. reflexivity. Qed. @@ -79,7 +90,7 @@ Definition global_compilenv_match (ce: compilenv) (gv: gvarenv) : Prop := end. Lemma global_compilenv_charact: - global_compilenv_match gce (global_var_env prog). + global_compilenv_match gce gvare. Proof. set (mkgve := fun gv (vars: list (ident * list init_data * var_kind)) => List.fold_left @@ -96,7 +107,7 @@ Proof. case (peq id1 id2); intro. auto. apply H. case (peq id1 id2); intro. auto. apply H. - change (global_var_env prog) with (mkgve (PTree.empty var_kind) prog.(prog_vars)). + change gvare with (mkgve (PTree.empty var_kind) prog.(prog_vars)). unfold gce, build_global_compilenv. apply H. intro. rewrite PMap.gi. auto. Qed. @@ -156,7 +167,7 @@ Inductive match_var (f: meminj) (id: ident) | match_var_global_scalar: forall chunk, PTree.get id e = None -> - PTree.get id (global_var_env prog) = Some (Vscalar chunk) -> + PTree.get id gvare = Some (Vscalar chunk) -> match_var f id e m te sp (Var_global_scalar chunk) | match_var_global_array: PTree.get id e = None -> @@ -192,11 +203,12 @@ Record match_env (f: meminj) (cenv: compilenv) PTree.get id2 e = Some(b2, lv2) -> id1 <> id2 -> b1 <> b2; -(** All blocks mapped to sub-blocks of the Cminor stack data must be in - the range [lo, hi]. *) +(** All blocks mapped to sub-blocks of the Cminor stack data must be + images of variables from the Csharpminor environment [e] *) me_inv: forall b delta, - f b = Some(sp, delta) -> lo <= b < hi; + f b = Some(sp, delta) -> + exists id, exists lv, PTree.get id e = Some(b, lv); (** All Csharpminor blocks below [lo] (i.e. allocated before the blocks referenced from [e]) must map to blocks that are below [sp] @@ -460,17 +472,37 @@ Proof. generalize (H3 _ H4). inversion H1. omega. Qed. +Lemma blocks_of_env_charact: + forall b e, + In b (blocks_of_env e) <-> + exists id, exists lv, e!id = Some(b, lv). +Proof. + unfold blocks_of_env. + set (f := fun id_b_lv : positive * (block * var_kind) => + let (_, y) := id_b_lv in let (b0, _) := y in b0). + intros; split; intros. + exploit list_in_map_inv; eauto. intros [[id [b' lv]] [A B]]. + simpl in A. subst b'. exists id; exists lv. apply PTree.elements_complete. auto. + destruct H as [id [lv EQ]]. + change b with (f (id, (b, lv))). apply List.in_map. + apply PTree.elements_correct. auto. +Qed. + Lemma match_callstack_freelist: - forall f cenv e te sp lo hi cs bound tbound m fbl, - (forall b, In b fbl -> lo <= b) -> + forall f cenv e te sp lo hi cs bound tbound m tm, + mem_inject f m tm -> match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m -> - match_callstack f cs bound tbound (free_list m fbl). + match_callstack f cs bound tbound (free_list m (blocks_of_env e)) + /\ mem_inject f (free_list m (blocks_of_env e)) (free tm sp). Proof. - intros. inversion H0. inversion H14. + intros. inv H0. inv H14. split. apply match_callstack_incr_bound with lo sp. - apply match_callstack_freelist_rec. auto. - assumption. + apply match_callstack_freelist_rec. auto. + intros. rewrite blocks_of_env_charact in H0. + destruct H0 as [id [lv EQ]]. exploit me_bounded0; eauto. omega. omega. omega. + apply Mem.free_inject; auto. + intros. rewrite blocks_of_env_charact. eauto. Qed. (** Preservation of [match_callstack] when allocating a block for @@ -501,6 +533,7 @@ Lemma match_env_alloc_same: end -> match_env f1 cenv1 e1 m1 te sp lo m1.(nextblock) -> te!id = Some tv -> + e1!id = None -> let f2 := extend_inject b data f1 in let cenv2 := PMap.set id info cenv1 in let e2 := PTree.set id (b, lv) e1 in @@ -511,7 +544,7 @@ Proof. assert (b = m1.(nextblock)). injection H; intros. auto. assert (m2.(nextblock) = Zsucc m1.(nextblock)). - injection H; intros. rewrite <- H6; reflexivity. + injection H; intros. rewrite <- H7; reflexivity. inversion H1. constructor. (* me_vars *) intros id0. unfold cenv2. rewrite PMap.gsspec. case (peq id0 id); intros. @@ -522,7 +555,7 @@ Proof. apply match_var_local with b Vundef tv. unfold e2; rewrite PTree.gss. congruence. eapply load_from_alloc_is_undef; eauto. - rewrite H7 in H. unfold sizeof in H. eauto. + rewrite H8 in H. unfold sizeof in H. eauto. unfold f2, extend_inject, eq_block. rewrite zeq_true. auto. auto. constructor. @@ -545,12 +578,12 @@ Proof. contradiction. (* other vars *) generalize (me_vars0 id0); intros. - inversion H6. + inversion H7. eapply match_var_local with (v := v); eauto. unfold e2; rewrite PTree.gso; eauto. eapply load_alloc_other; eauto. unfold f2, extend_inject, eq_block; rewrite zeq_false; auto. - generalize (me_bounded0 _ _ _ H8). unfold block in *; omega. + generalize (me_bounded0 _ _ _ H9). unfold block in *; omega. econstructor; eauto. unfold e2; rewrite PTree.gso; eauto. econstructor; eauto. @@ -564,22 +597,24 @@ Proof. (* me_bounded *) intros until lv0. unfold e2; rewrite PTree.gsspec. case (peq id0 id); intros. - subst id0. inversion H6. subst b0. unfold block in *; omega. - generalize (me_bounded0 _ _ _ H6). rewrite H5. omega. + subst id0. inversion H7. subst b0. unfold block in *; omega. + generalize (me_bounded0 _ _ _ H7). rewrite H6. omega. (* me_inj *) intros until lv2. unfold e2; repeat rewrite PTree.gsspec. case (peq id1 id); case (peq id2 id); intros. congruence. - inversion H6. subst b1. rewrite H4. + inversion H7. subst b1. rewrite H5. + generalize (me_bounded0 _ _ _ H8). unfold block; omega. + inversion H8. subst b2. rewrite H5. generalize (me_bounded0 _ _ _ H7). unfold block; omega. - inversion H7. subst b2. rewrite H4. - generalize (me_bounded0 _ _ _ H6). unfold block; omega. eauto. (* me_inv *) intros until delta. unfold f2, extend_inject, eq_block. case (zeq b0 b); intros. - subst b0. rewrite H4; rewrite H5. omega. - generalize (me_inv0 _ _ H6). rewrite H5. omega. + subst b0. exists id; exists lv. unfold e2. apply PTree.gss. + exploit me_inv0; eauto. intros [id' [lv' EQ]]. + exists id'; exists lv'. unfold e2. rewrite PTree.gso; auto. + congruence. (* me_incr *) intros until delta. unfold f2, extend_inject, eq_block. case (zeq b0 b); intros. @@ -660,6 +695,7 @@ Lemma match_callstack_alloc_left: end -> match_callstack f1 (mkframe cenv1 e1 te sp lo m1.(nextblock) :: cs) m1.(nextblock) tbound m1 -> te!id = Some tv -> + e1!id = None -> let f2 := extend_inject b data f1 in let cenv2 := PMap.set id info cenv1 in let e2 := PTree.set id (b, lv) e1 in @@ -670,12 +706,12 @@ Proof. unfold f2, cenv2, e2. eapply match_env_alloc_same; eauto. unfold f2; eapply match_callstack_alloc_other; eauto. destruct info. - elim H0; intros. rewrite H19. auto. - elim H0; intros. rewrite H19. omega. - elim H0; intros. rewrite H19. omega. + elim H0; intros. rewrite H20. auto. + elim H0; intros. rewrite H20. omega. + elim H0; intros. rewrite H20. omega. contradiction. contradiction. - inversion H17; omega. + inversion H18; omega. Qed. Lemma match_callstack_alloc_right: @@ -1029,7 +1065,7 @@ Proof. Qed. Lemma make_store_correct: - forall f sp te tm addr tvaddr rhs tvrhs chunk m vaddr vrhs m', + forall f sp te tm addr tvaddr rhs tvrhs chunk m vaddr vrhs m' fn k, eval_expr tge sp te tm addr tvaddr -> eval_expr tge sp te tm rhs tvrhs -> Mem.storev chunk m vaddr vrhs = Some m' -> @@ -1037,8 +1073,8 @@ Lemma make_store_correct: val_inject f vaddr tvaddr -> val_inject f vrhs tvrhs -> exists tm', - exec_stmt tge sp te tm (make_store chunk addr rhs) - E0 te tm' Out_normal + step tge (State fn (make_store chunk addr rhs) k sp te tm) + E0 (State fn Sskip k sp te tm') /\ mem_inject f m' tm' /\ nextblock tm' = nextblock tm. Proof. @@ -1048,7 +1084,7 @@ Proof. exploit storev_mapped_inject_1; eauto. intros [tm' [STORE MEMINJ]]. exists tm'. - split. eapply exec_Sstore; eauto. + split. eapply step_store; eauto. split. auto. unfold storev in STORE; destruct tvaddr; try discriminate. eapply nextblock_store; eauto. @@ -1062,7 +1098,7 @@ Lemma var_get_correct: var_get cenv id = OK a -> match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> mem_inject f m tm -> - eval_var_ref prog e id b chunk -> + eval_var_ref gve e id b chunk -> load chunk m b 0 = Some v -> exists tv, eval_expr tge (Vptr sp Int.zero) te tm a tv /\ @@ -1088,7 +1124,7 @@ Proof. eapply eval_Eload; eauto. eapply make_stackaddr_correct; eauto. auto. (* var_global_scalar *) - inversion H2; [congruence|subst]. + inversion H2; [congruence|subst]. simpl in H9; simpl in H10. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. inversion H11. destruct (mg_symbols0 _ _ H9) as [A B]. assert (chunk0 = chunk). congruence. subst chunk0. @@ -1106,7 +1142,7 @@ Lemma var_addr_correct: forall cenv id a f e te sp lo hi m cs tm b, match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> var_addr cenv id = OK a -> - eval_var_addr prog e id b -> + eval_var_addr gve e id b -> exists tv, eval_expr tge (Vptr sp Int.zero) te tm a tv /\ val_inject f (Vptr b Int.zero) tv. @@ -1142,15 +1178,16 @@ Proof. Qed. Lemma var_set_correct: - forall cenv id rhs a f e te sp lo hi m cs tm tv v m', + forall cenv id rhs a f e te sp lo hi m cs tm tv v m' fn k, var_set cenv id rhs = OK a -> match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> eval_expr tge (Vptr sp Int.zero) te tm rhs tv -> val_inject f v tv -> mem_inject f m tm -> - exec_assign prog e m id v m' -> + exec_assign gve e m id v m' -> exists te', exists tm', - exec_stmt tge (Vptr sp Int.zero) te tm a E0 te' tm' Out_normal /\ + step tge (State fn a k (Vptr sp Int.zero) te tm) + E0 (State fn Sskip k (Vptr sp Int.zero) te' tm') /\ mem_inject f m' tm' /\ match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m' /\ (forall id', id' <> id -> te'!id' = te!id'). @@ -1169,7 +1206,7 @@ Proof. exploit make_cast_correct; eauto. intros [tv' [EVAL INJ]]. exists (PTree.set id tv' te); exists tm. - split. eapply exec_Sassign. eauto. + split. eapply step_assign. eauto. split. eapply store_unmapped_inject; eauto. split. rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto. intros. apply PTree.gso; auto. @@ -1183,13 +1220,13 @@ Proof. eauto. eauto. eauto. eauto. eauto. intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. exists te; exists tm'. - split. auto. split. auto. + split. eauto. split. auto. split. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. eapply match_callstack_mapped; eauto. inversion H9; congruence. auto. (* var_global_scalar *) - inversion H5; [congruence|subst]. + inversion H5; [congruence|subst]. simpl in H4; simpl in H10. assert (chunk0 = chunk) by congruence. subst chunk0. assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. @@ -1199,7 +1236,7 @@ Proof. eauto. eauto. eauto. eauto. eauto. intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. exists te; exists tm'. - split. auto. split. auto. + split. eauto. split. auto. split. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. eapply match_callstack_mapped; eauto. congruence. auto. @@ -1238,14 +1275,15 @@ Proof. Qed. Lemma var_set_self_correct: - forall cenv id a f e te sp lo hi m cs tm tv v m', + forall cenv id a f e te sp lo hi m cs tm tv v m' fn k, var_set cenv id (Evar id) = OK a -> match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> val_inject f v tv -> mem_inject f m tm -> - exec_assign prog e m id v m' -> + exec_assign gve e m id v m' -> exists te', exists tm', - exec_stmt tge (Vptr sp Int.zero) (PTree.set id tv te) tm a E0 te' tm' Out_normal /\ + step tge (State fn a k (Vptr sp Int.zero) (PTree.set id tv te) tm) + E0 (State fn Sskip k (Vptr sp Int.zero) te' tm') /\ mem_inject f m' tm' /\ match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m'. Proof. @@ -1265,7 +1303,7 @@ Proof. exploit make_cast_correct; eauto. intros [tv' [EVAL INJ]]. exists (PTree.set id tv' (PTree.set id tv te)); exists tm. - split. eapply exec_Sassign. eauto. + split. eapply step_assign. eauto. split. eapply store_unmapped_inject; eauto. rewrite NEXTBLOCK. apply match_callstack_extensional with (PTree.set id tv' te). @@ -1282,7 +1320,7 @@ Proof. eauto. eauto. eauto. eauto. eauto. intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. exists (PTree.set id tv te); exists tm'. - split. auto. split. auto. + split. eauto. split. auto. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. apply match_callstack_extensional with te. intros. caseEq (cenv!!id0); intros; auto. @@ -1290,7 +1328,7 @@ Proof. eapply match_callstack_mapped; eauto. inversion H8; congruence. (* var_global_scalar *) - inversion H4; [congruence|subst]. + inversion H4; [congruence|subst]. simpl in H3; simpl in H9. assert (chunk0 = chunk) by congruence. subst chunk0. assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. @@ -1300,7 +1338,7 @@ Proof. eauto. eauto. eauto. eauto. eauto. intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. exists (PTree.set id tv te); exists tm'. - split. auto. split. auto. + split. eauto. split. auto. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. apply match_callstack_extensional with te. intros. caseEq (cenv!!id0); intros; auto. @@ -1390,8 +1428,8 @@ Lemma match_callstack_alloc_variables_rec: low_bound tm sp = 0 -> high_bound tm sp = sz' -> sz' <= Int.max_signed -> - forall e m vars e' m' lb, - alloc_variables e m vars e' m' lb -> + forall e m vars e' m', + alloc_variables e m vars e' m' -> forall f cenv sz, assign_variables atk vars (cenv, sz) = (cenv', sz') -> match_callstack f (mkframe cenv e te sp lo m.(nextblock) :: cs) @@ -1400,6 +1438,8 @@ Lemma match_callstack_alloc_variables_rec: 0 <= sz -> (forall b delta, f b = Some(sp, delta) -> high_bound m b + delta <= sz) -> (forall id lv, In (id, lv) vars -> te!id <> None) -> + list_norepet (List.map (@fst ident var_kind) vars) -> + (forall id lv, In (id, lv) vars -> e!id = None) -> exists f', inject_incr f f' /\ mem_inject f' m' tm @@ -1416,13 +1456,21 @@ Proof. change (assign_variables atk ((id, lv) :: vars) (cenv, sz)) with (assign_variables atk vars (assign_variable atk (id, lv) (cenv, sz))). caseEq (assign_variable atk (id, lv) (cenv, sz)). - intros cenv1 sz1 ASV1 ASVS MATCH MINJ SZPOS BOUND DEFINED. + intros cenv1 sz1 ASV1 ASVS MATCH MINJ SZPOS BOUND DEFINED NOREPET UNDEFINED. assert (DEFINED1: forall id0 lv0, In (id0, lv0) vars -> te!id0 <> None). intros. eapply DEFINED. simpl. right. eauto. assert (exists tv, te!id = Some tv). assert (te!id <> None). eapply DEFINED. simpl; left; auto. destruct (te!id). exists v; auto. congruence. elim H1; intros tv TEID; clear H1. + assert (UNDEFINED1: forall (id0 : ident) (lv0 : var_kind), + In (id0, lv0) vars -> + (PTree.set id (b1, lv) e)!id0 = None). + intros. rewrite PTree.gso. eapply UNDEFINED; eauto with coqlib. + simpl in NOREPET. inversion NOREPET. red; intro; subst id0. + elim H4. change id with (fst (id, lv0)). apply List.in_map. auto. + assert (NOREPET1: list_norepet (map (fst (A:=ident) (B:=var_kind)) vars)). + inv NOREPET; auto. generalize ASV1. unfold assign_variable. caseEq lv. (* 1. lv = LVscalar chunk *) @@ -1443,13 +1491,13 @@ Proof. intros. left. generalize (BOUND _ _ H5). omega. elim H3; intros MINJ1 INCR1; clear H3. exploit IHalloc_variables; eauto. - unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. + unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto with coqlib. rewrite <- H1. omega. intros until delta; unfold f1, extend_inject, eq_block. rewrite (high_bound_alloc _ _ _ _ _ H b). case (zeq b b1); intros. inversion H3. unfold sizeof; rewrite LV. omega. - generalize (BOUND _ _ H3). omega. + generalize (BOUND _ _ H3). omega. intros [f' [INCR2 [MINJ2 MATCH2]]]. exists f'; intuition. eapply inject_incr_trans; eauto. (* 1.2 info = Var_local chunk *) @@ -1457,7 +1505,7 @@ Proof. exploit alloc_unmapped_inject; eauto. set (f1 := extend_inject b1 None f). intros [MINJ1 INCR1]. exploit IHalloc_variables; eauto. - unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. + unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto with coqlib. intros until delta; unfold f1, extend_inject, eq_block. rewrite (high_bound_alloc _ _ _ _ _ H b). case (zeq b b1); intros. discriminate. @@ -1480,7 +1528,7 @@ Proof. intros. left. generalize (BOUND _ _ H7). omega. destruct H5 as [MINJ1 INCR1]. exploit IHalloc_variables; eauto. - unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. + unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto with coqlib. rewrite <- H1. omega. intros until delta; unfold f1, extend_inject, eq_block. rewrite (high_bound_alloc _ _ _ _ _ H b). @@ -1530,10 +1578,11 @@ Qed. of Csharpminor local variables and of the Cminor stack data block. *) Lemma match_callstack_alloc_variables: - forall fn cenv sz m e m' lb tm tm' sp f cs targs, + forall fn cenv sz m e m' tm tm' sp f cs targs, build_compilenv gce fn = (cenv, sz) -> sz <= Int.max_signed -> - alloc_variables Csharpminor.empty_env m (fn_variables fn) e m' lb -> + list_norepet (fn_params_names fn ++ fn_vars_names fn) -> + alloc_variables Csharpminor.empty_env m (fn_variables fn) e m' -> Mem.alloc tm 0 sz = (tm', sp) -> match_callstack f cs m.(nextblock) tm.(nextblock) m -> mem_inject f m tm -> @@ -1547,7 +1596,7 @@ Lemma match_callstack_alloc_variables: m'.(nextblock) tm'.(nextblock) m'. Proof. intros. - assert (SP: sp = nextblock tm). injection H2; auto. + assert (SP: sp = nextblock tm). injection H3; auto. unfold build_compilenv in H. eapply match_callstack_alloc_variables_rec with (sz' := sz); eauto with mem. eapply low_bound_alloc_same; eauto. @@ -1570,7 +1619,7 @@ Proof. intros until lv2. unfold Csharpminor.empty_env; rewrite PTree.gempty; congruence. (* me_inv *) intros. exploit mi_mappedblocks; eauto. intro A. - elim (fresh_block_alloc _ _ _ _ _ H2 A). + elim (fresh_block_alloc _ _ _ _ _ H3 A). (* me_incr *) intros. exploit mi_mappedblocks; eauto. intro A. rewrite SP; auto. @@ -1584,45 +1633,17 @@ Proof. unfold tparams, tvars. unfold fn_variables in H5. change Csharpminor.fn_params with Csharpminor.fn_params in H5. change Csharpminor.fn_vars with Csharpminor.fn_vars in H5. - elim (in_app_or _ _ _ H5); intros. - elim (list_in_map_inv _ _ _ H6). intros x [A B]. + elim (in_app_or _ _ _ H6); intros. + elim (list_in_map_inv _ _ _ H7). intros x [A B]. apply in_or_app; left. inversion A. apply List.in_map. auto. apply in_or_app; right. change id with (fst (id, lv)). apply List.in_map; auto. -Qed. - -(** Characterization of the range of addresses for the blocks allocated - to hold Csharpminor local variables. *) - -Lemma alloc_variables_nextblock_incr: - forall e1 m1 vars e2 m2 lb, - alloc_variables e1 m1 vars e2 m2 lb -> - nextblock m1 <= nextblock m2. -Proof. - induction 1; intros. - omega. - inversion H; subst m1; simpl in IHalloc_variables. omega. -Qed. - -Lemma alloc_variables_list_block: - forall e1 m1 vars e2 m2 lb, - alloc_variables e1 m1 vars e2 m2 lb -> - forall b, m1.(nextblock) <= b < m2.(nextblock) <-> In b lb. -Proof. - induction 1; intros. - simpl; split; intro. omega. contradiction. - elim (IHalloc_variables b); intros A B. - assert (nextblock m = b1). injection H; intros. auto. - assert (nextblock m1 = Zsucc (nextblock m)). - injection H; intros; subst m1; reflexivity. - simpl; split; intro. - assert (nextblock m = b \/ nextblock m1 <= b < nextblock m2). - unfold block; rewrite H2; omega. - elim H4; intro. left; congruence. right; auto. - elim H3; intro. subst b b1. - generalize (alloc_variables_nextblock_incr _ _ _ _ _ _ H0). - rewrite H2. omega. - generalize (B H4). rewrite H2. omega. + (* norepet *) + unfold fn_variables. + rewrite List.map_app. rewrite list_map_compose. simpl. + assumption. + (* undef *) + intros. unfold empty_env. apply PTree.gempty. Qed. (** Correctness of the code generated by [store_parameters] @@ -1656,16 +1677,15 @@ Qed. Lemma store_parameters_correct: forall e m1 params vl m2, bind_parameters e m1 params vl m2 -> - forall s f te1 cenv sp lo hi cs tm1, + forall s f te1 cenv sp lo hi cs tm1 fn k, vars_vals_match f params vl te1 -> list_norepet (List.map (@fst ident memory_chunk) params) -> mem_inject f m1 tm1 -> match_callstack f (mkframe cenv e te1 sp lo hi :: cs) m1.(nextblock) tm1.(nextblock) m1 -> store_parameters cenv params = OK s -> exists te2, exists tm2, - exec_stmt tge (Vptr sp Int.zero) - te1 tm1 s - E0 te2 tm2 Out_normal + star step tge (State fn s k (Vptr sp Int.zero) te1 tm1) + E0 (State fn Sskip k (Vptr sp Int.zero) te2 tm2) /\ mem_inject f m2 tm2 /\ match_callstack f (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2. Proof. @@ -1674,7 +1694,7 @@ Proof. intros; simpl. monadInv H3. exists te1; exists tm1. split. constructor. tauto. (* inductive case *) - intros until tm1. intros VVM NOREPET MINJ MATCH STOREP. + intros until k. intros VVM NOREPET MINJ MATCH STOREP. monadInv STOREP. inversion VVM. subst f0 id0 chunk0 vars v vals te. inversion NOREPET. subst hd tl. @@ -1690,7 +1710,10 @@ Proof. exploit IHbind_parameters; eauto. intros [te3 [tm3 [EXEC2 [MINJ2 MATCH2]]]]. exists te3; exists tm3. - split. econstructor; eauto. + split. eapply star_left. constructor. + eapply star_left. eexact EXEC1. + eapply star_left. constructor. eexact EXEC2. + reflexivity. reflexivity. reflexivity. auto. Qed. @@ -1752,8 +1775,8 @@ Qed. and initialize the blocks corresponding to function parameters). *) Lemma function_entry_ok: - forall fn m e m1 lb vargs m2 f cs tm cenv sz tm1 sp tvargs s, - alloc_variables empty_env m (fn_variables fn) e m1 lb -> + forall fn m e m1 vargs m2 f cs tm cenv sz tm1 sp tvargs s fn' k, + alloc_variables empty_env m (fn_variables fn) e m1 -> bind_parameters e m1 fn.(Csharpminor.fn_params) vargs m2 -> match_callstack f cs m.(nextblock) tm.(nextblock) m -> build_compilenv gce fn = (cenv, sz) -> @@ -1766,15 +1789,13 @@ Lemma function_entry_ok: list_norepet (fn_params_names fn ++ fn_vars_names fn) -> store_parameters cenv fn.(Csharpminor.fn_params) = OK s -> exists f2, exists te2, exists tm2, - exec_stmt tge (Vptr sp Int.zero) - te tm1 s - E0 te2 tm2 Out_normal + star step tge (State fn' s k (Vptr sp Int.zero) te tm1) + E0 (State fn' Sskip k (Vptr sp Int.zero) te2 tm2) /\ mem_inject f2 m2 tm2 /\ inject_incr f f2 /\ match_callstack f2 (mkframe cenv e te2 sp m.(nextblock) m1.(nextblock) :: cs) - m2.(nextblock) tm2.(nextblock) m2 - /\ (forall b, m.(nextblock) <= b < m1.(nextblock) <-> In b lb). + m2.(nextblock) tm2.(nextblock) m2. Proof. intros. exploit bind_parameters_length; eauto. intro LEN1. @@ -1791,8 +1812,7 @@ Proof. eexact MINJ1. eauto. eauto. intros [te2 [tm2 [EXEC [MINJ2 MATCH2]]]]. exists f1; exists te2; exists tm2. - split; auto. split; auto. split; auto. split; auto. - intros; eapply alloc_variables_list_block; eauto. + split. eauto. auto. Qed. (** * Semantic preservation for the translation *) @@ -1835,7 +1855,7 @@ Lemma transl_expr_correct: (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m), forall a v, - Csharpminor.eval_expr prog e m a v -> + Csharpminor.eval_expr gve e m a v -> forall ta (TR: transl_expr cenv a = OK ta), exists tv, @@ -1880,7 +1900,7 @@ Lemma transl_exprlist_correct: (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m), forall a v, - Csharpminor.eval_exprlist prog e m a v -> + Csharpminor.eval_exprlist gve e m a v -> forall ta (TR: transl_exprlist cenv a = OK ta), exists tv, @@ -1896,656 +1916,709 @@ Qed. (** ** Semantic preservation for statements and functions *) -Definition eval_funcall_prop - (m1: mem) (fn: Csharpminor.fundef) (args: list val) (t: trace) (m2: mem) (res: val) : Prop := - forall tfn f1 tm1 cs targs - (TR: transl_fundef gce fn = OK tfn) - (MINJ: mem_inject f1 m1 tm1) - (MATCH: match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1) - (ARGSINJ: val_list_inject f1 args targs), - exists f2, exists tm2, exists tres, - eval_funcall tge tm1 tfn targs t tm2 tres - /\ val_inject f2 res tres - /\ mem_inject f2 m2 tm2 - /\ inject_incr f1 f2 - /\ match_callstack f2 cs m2.(nextblock) tm2.(nextblock) m2. - -Inductive outcome_inject (f: meminj) : Csharpminor.outcome -> outcome -> Prop := - | outcome_inject_normal: - outcome_inject f Csharpminor.Out_normal Out_normal - | outcome_inject_exit: - forall n, outcome_inject f (Csharpminor.Out_exit n) (Out_exit n) - | outcome_inject_return_none: - outcome_inject f (Csharpminor.Out_return None) (Out_return None) - | outcome_inject_return_some: - forall v1 v2, - val_inject f v1 v2 -> - outcome_inject f (Csharpminor.Out_return (Some v1)) (Out_return (Some v2)). - -Definition exec_stmt_prop - (e: Csharpminor.env) (m1: mem) (s: Csharpminor.stmt) (t: trace) (m2: mem) (out: Csharpminor.outcome): Prop := - forall cenv ts f1 te1 tm1 sp lo hi cs - (TR: transl_stmt cenv s = OK ts) - (MINJ: mem_inject f1 m1 tm1) - (MATCH: match_callstack f1 - (mkframe cenv e te1 sp lo hi :: cs) - m1.(nextblock) tm1.(nextblock) m1), - exists f2, exists te2, exists tm2, exists tout, - exec_stmt tge (Vptr sp Int.zero) te1 tm1 ts t te2 tm2 tout - /\ outcome_inject f2 out tout - /\ mem_inject f2 m2 tm2 - /\ inject_incr f1 f2 - /\ match_callstack f2 - (mkframe cenv e te2 sp lo hi :: cs) - m2.(nextblock) tm2.(nextblock) m2. - -(* Check (Csharpminor.eval_funcall_ind2 prog eval_funcall_prop exec_stmt_prop). *) - -(** There are as many cases in the inductive proof as there are evaluation - rules in the Csharpminor semantics. We treat each case as a separate - lemma. *) - -Lemma transl_funcall_internal_correct: - forall (m : mem) (f : Csharpminor.function) (vargs : list val) - (e : Csharpminor.env) (m1 : mem) (lb : list block) (m2: mem) - (t: trace) (m3 : mem) (out : Csharpminor.outcome) (vres : val), - list_norepet (fn_params_names f ++ fn_vars_names f) -> - alloc_variables empty_env m (fn_variables f) e m1 lb -> - bind_parameters e m1 (Csharpminor.fn_params f) vargs m2 -> - Csharpminor.exec_stmt prog e m2 (Csharpminor.fn_body f) t m3 out -> - exec_stmt_prop e m2 (Csharpminor.fn_body f) t m3 out -> - Csharpminor.outcome_result_value out (sig_res (Csharpminor.fn_sig f)) vres -> - eval_funcall_prop m (Internal f) vargs t (free_list m3 lb) vres. -Proof. - intros; red. intros tfn f1 tm; intros. - monadInv TR. generalize EQ. - unfold transl_function. - caseEq (build_compilenv gce f); intros cenv stacksize CENV. - destruct (zle stacksize Int.max_signed); try congruence. - intro TR. monadInv TR. - caseEq (alloc tm 0 stacksize). intros tm1 sp ALLOC. - exploit function_entry_ok; eauto. - intros [f2 [te2 [tm2 [STOREPARAM [MINJ2 [INCR12 [MATCH2 BLOCKS]]]]]]]. - red in H3; exploit H3; eauto. - intros [f3 [te3 [tm3 [tout [EXECBODY [OUTINJ [MINJ3 [INCR23 MATCH3]]]]]]]]. - assert (exists tvres, - outcome_result_value tout f.(Csharpminor.fn_sig).(sig_res) tvres /\ - val_inject f3 vres tvres). - generalize H4. unfold Csharpminor.outcome_result_value, outcome_result_value. - inversion OUTINJ. - destruct (sig_res (Csharpminor.fn_sig f)); intro. contradiction. - exists Vundef; split. auto. subst vres; constructor. - tauto. - destruct (sig_res (Csharpminor.fn_sig f)); intro. contradiction. - exists Vundef; split. auto. subst vres; constructor. - destruct (sig_res (Csharpminor.fn_sig f)); intro. - exists v2; split. auto. subst vres; auto. - contradiction. - destruct H5 as [tvres [TOUT VINJRES]]. - assert (outcome_free_mem tout tm3 sp = Mem.free tm3 sp). - inversion OUTINJ; auto. - exists f3; exists (Mem.free tm3 sp); exists tvres. - (* execution *) - split. rewrite <- H5. econstructor; simpl; eauto. - apply exec_Sseq_continue with E0 te2 tm2 t. - exact STOREPARAM. - eexact EXECBODY. - traceEq. - (* val_inject *) - split. assumption. - (* mem_inject *) - split. apply free_inject; auto. - intros. elim (BLOCKS b1); intros B1 B2. apply B1. inversion MATCH3. inversion H20. - eapply me_inv0. eauto. - (* inject_incr *) - split. eapply inject_incr_trans; eauto. - (* match_callstack *) - assert (forall bl mm, nextblock (free_list mm bl) = nextblock mm). - induction bl; intros. reflexivity. simpl. auto. - unfold free; simpl nextblock. rewrite H6. - eapply match_callstack_freelist; eauto. - intros. elim (BLOCKS b); intros B1 B2. generalize (B2 H7). omega. -Qed. - -Lemma transl_funcall_external_correct: - forall (m : mem) (ef : external_function) (vargs : list val) - (t : trace) (vres : val), - event_match ef vargs t vres -> - eval_funcall_prop m (External ef) vargs t m vres. +Inductive match_cont: Csharpminor.cont -> Cminor.cont -> compilenv -> exit_env -> callstack -> Prop := + | match_Kstop: forall cenv xenv, + match_cont Csharpminor.Kstop Kstop cenv xenv nil + | match_Kseq: forall s k ts tk cenv xenv cs, + transl_stmt cenv xenv s = OK ts -> + match_cont k tk cenv xenv cs -> + match_cont (Csharpminor.Kseq s k) (Kseq ts tk) cenv xenv cs + | match_Kseq2: forall s1 s2 k ts1 tk cenv xenv cs, + transl_stmt cenv xenv s1 = OK ts1 -> + match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs -> + match_cont (Csharpminor.Kseq (Csharpminor.Sseq s1 s2) k) + (Kseq ts1 tk) cenv xenv cs + | match_Kblock: forall k tk cenv xenv cs, + match_cont k tk cenv xenv cs -> + match_cont (Csharpminor.Kblock k) (Kblock tk) cenv (true :: xenv) cs + | match_Kblock2: forall k tk cenv xenv cs, + match_cont k tk cenv xenv cs -> + match_cont k (Kblock tk) cenv (false :: xenv) cs + | match_Kcall_none: forall fn e k tfn sp te tk cenv xenv lo hi cs sz cenv', + transl_funbody cenv sz fn = OK tfn -> + match_cont k tk cenv xenv cs -> + match_cont (Csharpminor.Kcall None fn e k) + (Kcall None tfn (Vptr sp Int.zero) te tk) + cenv' nil + (mkframe cenv e te sp lo hi :: cs) + | match_Kcall_some: forall id fn e k tfn s sp te tk cenv xenv lo hi cs sz cenv', + transl_funbody cenv sz fn = OK tfn -> + var_set cenv id (Evar id) = OK s -> + match_cont k tk cenv xenv cs -> + match_cont (Csharpminor.Kcall (Some id) fn e k) + (Kcall (Some id) tfn (Vptr sp Int.zero) te (Kseq s tk)) + cenv' nil + (mkframe cenv e te sp lo hi :: cs). + +Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := + | match_state: + forall fn s k e m tfn ts tk sp te tm cenv xenv f lo hi cs sz + (TRF: transl_funbody cenv sz fn = OK tfn) + (TR: transl_stmt cenv xenv s = OK ts) + (MINJ: mem_inject f m tm) + (MCS: match_callstack f + (mkframe cenv e te sp lo hi :: cs) + m.(nextblock) tm.(nextblock) m) + (MK: match_cont k tk cenv xenv cs), + match_states (Csharpminor.State fn s k e m) + (State tfn ts tk (Vptr sp Int.zero) te tm) + | match_state_seq: + forall fn s1 s2 k e m tfn ts1 tk sp te tm cenv xenv f lo hi cs sz + (TRF: transl_funbody cenv sz fn = OK tfn) + (TR: transl_stmt cenv xenv s1 = OK ts1) + (MINJ: mem_inject f m tm) + (MCS: match_callstack f + (mkframe cenv e te sp lo hi :: cs) + m.(nextblock) tm.(nextblock) m) + (MK: match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs), + match_states (Csharpminor.State fn (Csharpminor.Sseq s1 s2) k e m) + (State tfn ts1 tk (Vptr sp Int.zero) te tm) + | match_callstate: + forall fd args k m tfd targs tk tm f cs cenv + (TR: transl_fundef gce fd = OK tfd) + (MINJ: mem_inject f m tm) + (MCS: match_callstack f cs m.(nextblock) tm.(nextblock) m) + (MK: match_cont k tk cenv nil cs) + (ISCC: Csharpminor.is_call_cont k) + (ARGSINJ: val_list_inject f args targs), + match_states (Csharpminor.Callstate fd args k m) + (Callstate tfd targs tk tm) + | match_returnstate: + forall v k m tv tk tm f cs cenv + (MINJ: mem_inject f m tm) + (MCS: match_callstack f cs m.(nextblock) tm.(nextblock) m) + (MK: match_cont k tk cenv nil cs) + (RESINJ: val_inject f v tv), + match_states (Csharpminor.Returnstate v k m) + (Returnstate tv tk tm). + +Remark nextblock_freelist: + forall lb m, nextblock (free_list m lb) = nextblock m. +Proof. induction lb; intros; simpl; auto. Qed. + +Remark val_inject_function_pointer: + forall v fd f tv, + Genv.find_funct tge v = Some fd -> + match_globalenvs f -> + val_inject f v tv -> + tv = v. Proof. - intros; red; intros. monadInv TR. - exploit event_match_inject; eauto. intros [A B]. - exists f1; exists tm1; exists vres; intuition. - constructor; auto. + intros. exploit Genv.find_funct_inv; eauto. intros [b EQ]. subst v. + rewrite Genv.find_funct_find_funct_ptr in H. + assert (b < 0). unfold tge in H. eapply Genv.find_funct_ptr_negative; eauto. + assert (f b = Some(b, 0)). eapply mg_functions; eauto. + inv H1. rewrite H3 in H6; inv H6. reflexivity. Qed. -Lemma transl_stmt_Sskip_correct: - forall (e : Csharpminor.env) (m : mem), - exec_stmt_prop e m Csharpminor.Sskip E0 m Csharpminor.Out_normal. +Lemma match_call_cont: + forall k tk cenv xenv cs, + match_cont k tk cenv xenv cs -> + match_cont (Csharpminor.call_cont k) (call_cont tk) cenv nil cs. Proof. - intros; red; intros. monadInv TR. - exists f1; exists te1; exists tm1; exists Out_normal. - intuition. constructor. constructor. + induction 1; simpl; auto; econstructor; eauto. Qed. -Lemma transl_stmt_Sassign_correct: - forall (e : Csharpminor.env) (m : mem) (id : ident) - (a : Csharpminor.expr) (v : val) (m' : mem), - Csharpminor.eval_expr prog e m a v -> - exec_assign prog e m id v m' -> - exec_stmt_prop e m (Csharpminor.Sassign id a) E0 m' Csharpminor.Out_normal. +Lemma match_is_call_cont: + forall tfn te sp tm k tk cenv xenv cs, + match_cont k tk cenv xenv cs -> + Csharpminor.is_call_cont k -> + exists tk', + star step tge (State tfn Sskip tk sp te tm) + E0 (State tfn Sskip tk' sp te tm) + /\ is_call_cont tk' + /\ match_cont k tk' cenv nil cs. Proof. - intros; red; intros. monadInv TR. - exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]]. - exploit var_set_correct; eauto. - intros [te2 [tm2 [EVAL2 [MINJ2 MATCH2]]]]. - exists f1; exists te2; exists tm2; exists Out_normal. - intuition. constructor. -Qed. - -Lemma transl_stmt_Sstore_correct: - forall (e : Csharpminor.env) (m : mem) (chunk : memory_chunk) - (a b : Csharpminor.expr) (v1 v2 : val) (m' : mem), - Csharpminor.eval_expr prog e m a v1 -> - Csharpminor.eval_expr prog e m b v2 -> - storev chunk m v1 v2 = Some m' -> - exec_stmt_prop e m (Csharpminor.Sstore chunk a b) E0 m' Csharpminor.Out_normal. -Proof. - intros; red; intros. monadInv TR. - exploit transl_expr_correct. - eauto. eauto. eexact H. eauto. - intros [tv1 [EVAL1 INJ1]]. - exploit transl_expr_correct. - eauto. eauto. eexact H0. eauto. - intros [tv2 [EVAL2 INJ2]]. - exploit make_store_correct. - eexact EVAL1. eexact EVAL2. eauto. eauto. eauto. eauto. - intros [tm2 [EXEC [MINJ2 NEXTBLOCK]]]. - exists f1; exists te1; exists tm2; exists Out_normal. - intuition. - constructor. - unfold storev in H1; destruct v1; try discriminate. - inv INJ1. - rewrite NEXTBLOCK. replace (nextblock m') with (nextblock m). - eapply match_callstack_mapped; eauto. congruence. - symmetry. eapply nextblock_store; eauto. -Qed. - -Lemma transl_stmt_Scall_correct: - forall (e : Csharpminor.env) (m : mem) (optid : option ident) - (sig : signature) (a : Csharpminor.expr) - (bl : list Csharpminor.expr) (vf : val) (vargs : list val) - (f : Csharpminor.fundef) (t : trace) (m1 : mem) (vres : val) - (m2 : mem), - Csharpminor.eval_expr prog e m a vf -> - Csharpminor.eval_exprlist prog e m bl vargs -> - Genv.find_funct (Genv.globalenv prog) vf = Some f -> - Csharpminor.funsig f = sig -> - Csharpminor.eval_funcall prog m f vargs t m1 vres -> - eval_funcall_prop m f vargs t m1 vres -> - exec_opt_assign prog e m1 optid vres m2 -> - exec_stmt_prop e m (Csharpminor.Scall optid sig a bl) t m2 Csharpminor.Out_normal. -Proof. - intros;red;intros. - assert (forall tv, val_inject f1 vf tv -> tv = vf). - intros. - elim (Genv.find_funct_inv H1). intros bf VF. rewrite VF in H1. - rewrite Genv.find_funct_find_funct_ptr in H1. - generalize (Genv.find_funct_ptr_negative H1). intro. - assert (match_globalenvs f1). eapply match_callstack_match_globalenvs; eauto. - generalize (mg_functions _ H8 _ H7). intro. - rewrite VF in H6. inv H6. - decEq. congruence. - replace x with 0. reflexivity. congruence. - inv H5; monadInv TR. - (* optid = None *) - exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]]. - exploit transl_exprlist_correct; eauto. intros [tv2 [EVAL2 VINJ2]]. - rewrite <- (H6 _ VINJ1) in H1. - elim (functions_translated _ _ H1). intros tf [FIND TRF]. - exploit H4; eauto. - intros [f2 [tm2 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]]. - exists f2; exists te1; exists tm2; exists Out_normal. - intuition. eapply exec_Scall; eauto. - apply sig_preserved; auto. - constructor. - (* optid = Some id *) - exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]]. - exploit transl_exprlist_correct; eauto. intros [tv2 [EVAL2 VINJ2]]. - rewrite <- (H6 _ VINJ1) in H1. - elim (functions_translated _ _ H1). intros tf [FIND TRF]. - exploit H4; eauto. - intros [f2 [tm2 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]]. - exploit var_set_self_correct. - eauto. eexact MATCH3. eauto. eauto. eauto. - intros [te3 [tm3 [EVAL4 [MINJ4 MATCH4]]]]. - exists f2; exists te3; exists tm3; exists Out_normal. intuition. - eapply exec_Sseq_continue. eapply exec_Scall; eauto. - apply sig_preserved; auto. - simpl. eexact EVAL4. traceEq. - constructor. + induction 1; simpl; intros; try contradiction. + econstructor; split. apply star_refl. split. exact I. econstructor; eauto. + exploit IHmatch_cont; eauto. + intros [tk' [A B]]. exists tk'; split. + eapply star_left; eauto. constructor. traceEq. auto. + econstructor; split. apply star_refl. split. exact I. econstructor; eauto. + econstructor; split. apply star_refl. split. exact I. econstructor; eauto. Qed. -Lemma transl_stmt_Sseq_continue_correct: - forall (e : Csharpminor.env) (m : mem) (s1 s2 : Csharpminor.stmt) - (t1 t2: trace) (m1 m2 : mem) (t: trace) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m s1 t1 m1 Csharpminor.Out_normal -> - exec_stmt_prop e m s1 t1 m1 Csharpminor.Out_normal -> - Csharpminor.exec_stmt prog e m1 s2 t2 m2 out -> - exec_stmt_prop e m1 s2 t2 m2 out -> - t = t1 ** t2 -> - exec_stmt_prop e m (Csharpminor.Sseq s1 s2) t m2 out. -Proof. - intros; red; intros; monadInv TR. - exploit H0; eauto. - intros [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - exploit H2; eauto. - intros [f3 [te3 [tm3 [tout2 [EXEC2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. - exists f3; exists te3; exists tm3; exists tout2. - intuition. eapply exec_Sseq_continue; eauto. - inversion OINJ1. subst tout1. auto. - eapply inject_incr_trans; eauto. -Qed. - -Lemma transl_stmt_Sseq_stop_correct: - forall (e : Csharpminor.env) (m : mem) (s1 s2 : Csharpminor.stmt) - (t1: trace) (m1 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m s1 t1 m1 out -> - exec_stmt_prop e m s1 t1 m1 out -> - out <> Csharpminor.Out_normal -> - exec_stmt_prop e m (Csharpminor.Sseq s1 s2) t1 m1 out. -Proof. - intros; red; intros; monadInv TR. - exploit H0; eauto. - intros [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - exists f2; exists te2; exists tm2; exists tout1. - intuition. eapply exec_Sseq_stop; eauto. - inversion OINJ1; subst out tout1; congruence. -Qed. - -Lemma transl_stmt_Sifthenelse_correct: - forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (sl1 sl2 : Csharpminor.stmt) (v : val) (vb : bool) (t : trace) - (m' : mem) (out : Csharpminor.outcome), - Csharpminor.eval_expr prog e m a v -> - Val.bool_of_val v vb -> - Csharpminor.exec_stmt prog e m (if vb then sl1 else sl2) t m' out -> - exec_stmt_prop e m (if vb then sl1 else sl2) t m' out -> - exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) t m' out. -Proof. - intros; red; intros. monadInv TR. - exploit transl_expr_correct; eauto. - intros [tv1 [EVAL1 VINJ1]]. - assert (transl_stmt cenv (if vb then sl1 else sl2) = - OK (if vb then x0 else x1)). destruct vb; auto. - exploit H2; eauto. - intros [f2 [te2 [tm2 [tout [EVAL2 [OINJ [MINJ2 [INCR2 MATCH2]]]]]]]]. - exists f2; exists te2; exists tm2; exists tout. - intuition. - eapply exec_Sifthenelse; eauto. - eapply bool_of_val_inject; eauto. -Qed. - -Lemma transl_stmt_Sloop_loop_correct: - forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) - (t1: trace) (m1: mem) (t2: trace) (m2 : mem) - (out : Csharpminor.outcome) (t: trace), - Csharpminor.exec_stmt prog e m sl t1 m1 Csharpminor.Out_normal -> - exec_stmt_prop e m sl t1 m1 Csharpminor.Out_normal -> - Csharpminor.exec_stmt prog e m1 (Csharpminor.Sloop sl) t2 m2 out -> - exec_stmt_prop e m1 (Csharpminor.Sloop sl) t2 m2 out -> - t = t1 ** t2 -> - exec_stmt_prop e m (Csharpminor.Sloop sl) t m2 out. -Proof. - intros; red; intros. generalize TR; intro TR'; monadInv TR'. - exploit H0; eauto. - intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - exploit H2; eauto. - intros [f3 [te3 [tm3 [tout2 [EVAL2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. - exists f3; exists te3; exists tm3; exists tout2. - intuition. - eapply exec_Sloop_loop; eauto. - inversion OINJ1; subst tout1; eauto. - eapply inject_incr_trans; eauto. -Qed. - -Lemma transl_stmt_Sloop_exit_correct: - forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) - (t1: trace) (m1 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m sl t1 m1 out -> - exec_stmt_prop e m sl t1 m1 out -> - out <> Csharpminor.Out_normal -> - exec_stmt_prop e m (Csharpminor.Sloop sl) t1 m1 out. -Proof. - intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - exists f2; exists te2; exists tm2; exists tout1. - intuition. eapply exec_Sloop_stop; eauto. - inversion OINJ1; subst out tout1; congruence. -Qed. - -Remark outcome_block_inject: - forall f out tout, - outcome_inject f out tout -> - outcome_inject f (Csharpminor.outcome_block out) (outcome_block tout). -Proof. - induction 1; simpl. - constructor. - destruct n; constructor. - constructor. - constructor; auto. -Qed. +(** Properties of [switch] compilation *) + +Require Import Switch. -Lemma transl_stmt_Sblock_correct: - forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) - (t1: trace) (m1 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m sl t1 m1 out -> - exec_stmt_prop e m sl t1 m1 out -> - exec_stmt_prop e m (Csharpminor.Sblock sl) t1 m1 - (Csharpminor.outcome_block out). +Remark switch_table_shift: + forall n sl base dfl, + switch_target n (S dfl) (switch_table sl (S base)) = + S (switch_target n dfl (switch_table sl base)). Proof. - intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - exists f2; exists te2; exists tm2; exists (outcome_block tout1). - intuition. eapply exec_Sblock; eauto. - apply outcome_block_inject; auto. + induction sl; intros; simpl. auto. destruct (Int.eq n i); auto. Qed. -Lemma transl_stmt_Sexit_correct: - forall (e : Csharpminor.env) (m : mem) (n : nat), - exec_stmt_prop e m (Csharpminor.Sexit n) E0 m (Csharpminor.Out_exit n). +Remark length_switch_table: + forall sl base1 base2, + length (switch_table sl base1) = length (switch_table sl base2). Proof. - intros; red; intros. monadInv TR. - exists f1; exists te1; exists tm1; exists (Out_exit n). - intuition. constructor. constructor. + induction sl; intros; simpl. auto. decEq; auto. Qed. -Lemma transl_stmt_Sswitch_correct: - forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (cases : list (int * nat)) (default : nat) (n : int), - Csharpminor.eval_expr prog e m a (Vint n) -> - exec_stmt_prop e m (Csharpminor.Sswitch a cases default) E0 m - (Csharpminor.Out_exit (switch_target n default cases)). +Inductive transl_lblstmt_cont (cenv: compilenv) (xenv: exit_env): lbl_stmt -> cont -> cont -> Prop := + | tlsc_default: forall s k ts, + transl_stmt cenv (switch_env (LSdefault s) xenv) s = OK ts -> + transl_lblstmt_cont cenv xenv (LSdefault s) k (Kblock (Kseq ts k)) + | tlsc_case: forall i s ls k ts k', + transl_stmt cenv (switch_env (LScase i s ls) xenv) s = OK ts -> + transl_lblstmt_cont cenv xenv ls k k' -> + transl_lblstmt_cont cenv xenv (LScase i s ls) k (Kblock (Kseq ts k')). + +Lemma switch_descent: + forall cenv xenv k ls body s, + transl_lblstmt cenv (switch_env ls xenv) ls body = OK s -> + exists k', + transl_lblstmt_cont cenv xenv ls k k' + /\ (forall f sp e m, + plus step tge (State f s k sp e m) E0 (State f body k' sp e m)). Proof. - intros; red; intros. monadInv TR. - exploit transl_expr_correct; eauto. - intros [tv1 [EVAL VINJ1]]. - inv VINJ1. - exists f1; exists te1; exists tm1; exists (Out_exit (switch_target n default cases)). - split. constructor. auto. - split. constructor. - split. auto. - split. apply inject_incr_refl. - auto. + induction ls; intros. + monadInv H. econstructor; split. + econstructor; eauto. + intros. eapply plus_left. constructor. apply star_one. constructor. traceEq. + monadInv H. exploit IHls; eauto. intros [k' [A B]]. + econstructor; split. + econstructor; eauto. + intros. eapply plus_star_trans. eauto. + eapply star_left. constructor. apply star_one. constructor. + reflexivity. traceEq. +Qed. + +Lemma switch_ascent: + forall f n sp e m cenv xenv k ls k1, + let tbl := switch_table ls O in + let ls' := select_switch n ls in + transl_lblstmt_cont cenv xenv ls k k1 -> + exists k2, + star step tge (State f (Sexit (switch_target n (length tbl) tbl)) k1 sp e m) + E0 (State f (Sexit O) k2 sp e m) + /\ transl_lblstmt_cont cenv xenv ls' k k2. +Proof. + induction ls; intros; unfold tbl, ls'; simpl. + inv H. econstructor; split. apply star_refl. econstructor; eauto. + simpl in H. inv H. + rewrite Int.eq_sym. destruct (Int.eq i n). + econstructor; split. apply star_refl. econstructor; eauto. + exploit IHls; eauto. intros [k2 [A B]]. + rewrite (length_switch_table ls 1%nat 0%nat). + rewrite switch_table_shift. + econstructor; split. + eapply star_left. constructor. eapply star_left. constructor. eexact A. + reflexivity. traceEq. + exact B. +Qed. + +Lemma switch_match_cont: + forall cenv xenv k cs tk ls tk', + match_cont k tk cenv xenv cs -> + transl_lblstmt_cont cenv xenv ls tk tk' -> + match_cont (Csharpminor.Kseq (seq_of_lbl_stmt ls) k) tk' cenv (false :: switch_env ls xenv) cs. +Proof. + induction ls; intros; simpl. + inv H0. apply match_Kblock2. econstructor; eauto. + inv H0. apply match_Kblock2. eapply match_Kseq2. auto. eauto. +Qed. + +Lemma transl_lblstmt_suffix: + forall n cenv xenv ls body ts, + transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts -> + let ls' := select_switch n ls in + exists body', exists ts', + transl_lblstmt cenv (switch_env ls' xenv) ls' body' = OK ts'. +Proof. + induction ls; simpl; intros. + monadInv H. + exists body; econstructor. rewrite EQ; eauto. simpl. reflexivity. + monadInv H. + destruct (Int.eq i n). + exists body; econstructor. simpl. rewrite EQ; simpl. rewrite EQ0; simpl. reflexivity. + eauto. Qed. -Lemma transl_stmt_Sreturn_none_correct: - forall (e : Csharpminor.env) (m : mem), - exec_stmt_prop e m (Csharpminor.Sreturn None) E0 m - (Csharpminor.Out_return None). +Lemma switch_match_states: + forall fn k e m tfn ts tk sp te tm cenv xenv f lo hi cs sz ls body tk' + (TRF: transl_funbody cenv sz fn = OK tfn) + (TR: transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts) + (MINJ: mem_inject f m tm) + (MCS: match_callstack f + (mkframe cenv e te sp lo hi :: cs) + m.(nextblock) tm.(nextblock) m) + (MK: match_cont k tk cenv xenv cs) + (TK: transl_lblstmt_cont cenv xenv ls tk tk'), + exists S, + plus step tge (State tfn (Sexit O) tk' (Vptr sp Int.zero) te tm) E0 S + /\ match_states (Csharpminor.State fn (seq_of_lbl_stmt ls) k e m) S. +Proof. + intros. destruct ls; simpl. + inv TK. econstructor; split. + eapply plus_left. constructor. apply star_one. constructor. traceEq. + eapply match_state; eauto. + inv TK. econstructor; split. + eapply plus_left. constructor. apply star_one. constructor. traceEq. + eapply match_state_seq; eauto. + simpl. eapply switch_match_cont; eauto. +Qed. + +(** Commutation between [find_label] and compilation *) + +Section FIND_LABEL. + +Variable lbl: label. +Variable cenv: compilenv. +Variable cs: callstack. + +Remark find_label_var_set: + forall id e s k, + var_set cenv id e = OK s -> + find_label lbl s k = None. +Proof. + intros. unfold var_set in H. + destruct (cenv!!id); monadInv H; reflexivity. +Qed. + +Lemma transl_lblstmt_find_label_context: + forall cenv xenv ls body ts tk1 tk2 ts' tk', + transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts -> + transl_lblstmt_cont cenv xenv ls tk1 tk2 -> + find_label lbl body tk2 = Some (ts', tk') -> + find_label lbl ts tk1 = Some (ts', tk'). +Proof. + induction ls; intros. + monadInv H. inv H0. simpl. simpl in H2. replace x with ts by congruence. rewrite H1. auto. + monadInv H. inv H0. + eapply IHls. eauto. eauto. simpl in H6. replace x with ts0 by congruence. simpl. + rewrite H1. auto. +Qed. + +Lemma transl_find_label: + forall s k xenv ts tk, + transl_stmt cenv xenv s = OK ts -> + match_cont k tk cenv xenv cs -> + match Csharpminor.find_label lbl s k with + | None => find_label lbl ts tk = None + | Some(s', k') => + exists ts', exists tk', exists xenv', + find_label lbl ts tk = Some(ts', tk') + /\ transl_stmt cenv xenv' s' = OK ts' + /\ match_cont k' tk' cenv xenv' cs + end + +with transl_lblstmt_find_label: + forall ls xenv body k ts tk tk1, + transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts -> + match_cont k tk cenv xenv cs -> + transl_lblstmt_cont cenv xenv ls tk tk1 -> + find_label lbl body tk1 = None -> + match Csharpminor.find_label_ls lbl ls k with + | None => find_label lbl ts tk = None + | Some(s', k') => + exists ts', exists tk', exists xenv', + find_label lbl ts tk = Some(ts', tk') + /\ transl_stmt cenv xenv' s' = OK ts' + /\ match_cont k' tk' cenv xenv' cs + end. Proof. - intros; red; intros. monadInv TR. - exists f1; exists te1; exists tm1; exists (Out_return None). - intuition. constructor. constructor. -Qed. + intros. destruct s; try (monadInv H); simpl; auto. + (* assign *) + eapply find_label_var_set; eauto. + (* call *) + destruct o; monadInv H; simpl; auto. + eapply find_label_var_set; eauto. + (* seq *) + exploit (transl_find_label s1). eauto. eapply match_Kseq. eexact EQ1. eauto. + destruct (Csharpminor.find_label lbl s1 (Csharpminor.Kseq s2 k)) as [[s' k'] | ]. + intros [ts' [tk' [xenv' [A [B C]]]]]. + exists ts'; exists tk'; exists xenv'. intuition. rewrite A; auto. + intro. rewrite H. apply transl_find_label with xenv; auto. + (* ifthenelse *) + exploit (transl_find_label s1). eauto. eauto. + destruct (Csharpminor.find_label lbl s1 k) as [[s' k'] | ]. + intros [ts' [tk' [xenv' [A [B C]]]]]. + exists ts'; exists tk'; exists xenv'. intuition. rewrite A; auto. + intro. rewrite H. apply transl_find_label with xenv; auto. + (* loop *) + apply transl_find_label with xenv. auto. econstructor; eauto. simpl. rewrite EQ; auto. + (* block *) + apply transl_find_label with (true :: xenv). auto. constructor; auto. + (* switch *) + exploit switch_descent; eauto. intros [k' [A B]]. + eapply transl_lblstmt_find_label. eauto. eauto. eauto. reflexivity. + (* return *) + destruct o; monadInv H; auto. + (* label *) + destruct (ident_eq lbl l). + exists x; exists tk; exists xenv; auto. + apply transl_find_label with xenv; auto. + + intros. destruct ls; monadInv H; simpl. + (* default *) + inv H1. simpl in H3. replace x with ts by congruence. rewrite H2. + eapply transl_find_label; eauto. + (* case *) + inv H1. simpl in H7. + exploit (transl_find_label s). eauto. eapply switch_match_cont; eauto. + destruct (Csharpminor.find_label lbl s (Csharpminor.Kseq (seq_of_lbl_stmt ls) k)) as [[s' k''] | ]. + intros [ts' [tk' [xenv' [A [B C]]]]]. + exists ts'; exists tk'; exists xenv'; intuition. + eapply transl_lblstmt_find_label_context; eauto. + simpl. replace x with ts0 by congruence. rewrite H2. auto. + intro. + eapply transl_lblstmt_find_label. eauto. auto. eauto. + simpl. replace x with ts0 by congruence. rewrite H2. auto. +Qed. + +Remark find_label_store_parameters: + forall vars s k, + store_parameters cenv vars = OK s -> find_label lbl s k = None. +Proof. + induction vars; intros. + monadInv H. auto. + simpl in H. destruct a as [id lv]. monadInv H. + simpl. rewrite (find_label_var_set id (Evar id)); auto. +Qed. + +End FIND_LABEL. + +Lemma transl_find_label_body: + forall cenv xenv size f tf k tk cs lbl s' k', + transl_funbody cenv size f = OK tf -> + match_cont k tk cenv xenv cs -> + Csharpminor.find_label lbl f.(Csharpminor.fn_body) (Csharpminor.call_cont k) = Some (s', k') -> + exists ts', exists tk', exists xenv', + find_label lbl tf.(fn_body) (call_cont tk) = Some(ts', tk') + /\ transl_stmt cenv xenv' s' = OK ts' + /\ match_cont k' tk' cenv xenv' cs. +Proof. + intros. monadInv H. simpl. + rewrite (find_label_store_parameters lbl cenv (Csharpminor.fn_params f)); auto. + exploit transl_find_label. eexact EQ. eapply match_call_cont. eexact H0. + instantiate (1 := lbl). rewrite H1. auto. +Qed. + + +Require Import Coq.Program.Equality. + +Fixpoint seq_left_depth (s: Csharpminor.stmt) : nat := + match s with + | Csharpminor.Sseq s1 s2 => S (seq_left_depth s1) + | _ => O + end. + +Definition measure (S: Csharpminor.state) : nat := + match S with + | Csharpminor.State fn s k e m => seq_left_depth s + | _ => O + end. -Lemma transl_stmt_Sreturn_some_correct: - forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (v : val), - Csharpminor.eval_expr prog e m a v -> - exec_stmt_prop e m (Csharpminor.Sreturn (Some a)) E0 m - (Csharpminor.Out_return (Some v)). +Lemma transl_step_correct: + forall S1 t S2, Csharpminor.step gve S1 t S2 -> + forall T1, match_states S1 T1 -> + (exists T2, plus step tge T1 t T2 /\ match_states S2 T2) + \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat. Proof. - intros; red; intros; monadInv TR. - exploit transl_expr_correct; eauto. - intros [tv1 [EVAL VINJ1]]. - exists f1; exists te1; exists tm1; exists (Out_return (Some tv1)). - intuition. econstructor; eauto. constructor; auto. -Qed. - -(** We conclude by an induction over the structure of the Csharpminor - evaluation derivation, using the lemmas above for each case. *) - -Lemma transl_function_correct: - forall m1 f vargs t m2 vres, - Csharpminor.eval_funcall prog m1 f vargs t m2 vres -> - eval_funcall_prop m1 f vargs t m2 vres. -Proof - (Csharpminor.eval_funcall_ind2 prog - eval_funcall_prop - exec_stmt_prop - - transl_funcall_internal_correct - transl_funcall_external_correct - transl_stmt_Sskip_correct - transl_stmt_Sassign_correct - transl_stmt_Sstore_correct - transl_stmt_Scall_correct - transl_stmt_Sseq_continue_correct - transl_stmt_Sseq_stop_correct - transl_stmt_Sifthenelse_correct - transl_stmt_Sloop_loop_correct - transl_stmt_Sloop_exit_correct - transl_stmt_Sblock_correct - transl_stmt_Sexit_correct - transl_stmt_Sswitch_correct - transl_stmt_Sreturn_none_correct - transl_stmt_Sreturn_some_correct). - -Lemma transl_stmt_correct: - forall e m1 s t m2 out, - Csharpminor.exec_stmt prog e m1 s t m2 out -> - exec_stmt_prop e m1 s t m2 out. -Proof - (Csharpminor.exec_stmt_ind2 prog - eval_funcall_prop - exec_stmt_prop - - transl_funcall_internal_correct - transl_funcall_external_correct - transl_stmt_Sskip_correct - transl_stmt_Sassign_correct - transl_stmt_Sstore_correct - transl_stmt_Scall_correct - transl_stmt_Sseq_continue_correct - transl_stmt_Sseq_stop_correct - transl_stmt_Sifthenelse_correct - transl_stmt_Sloop_loop_correct - transl_stmt_Sloop_exit_correct - transl_stmt_Sblock_correct - transl_stmt_Sexit_correct - transl_stmt_Sswitch_correct - transl_stmt_Sreturn_none_correct - transl_stmt_Sreturn_some_correct). - -(** ** Semantic preservation for divergence *) - -Definition evalinf_funcall_prop - (m1: mem) (fn: Csharpminor.fundef) (args: list val) (t: traceinf) : Prop := - forall tfn f1 tm1 cs targs - (TR: transl_fundef gce fn = OK tfn) - (MINJ: mem_inject f1 m1 tm1) - (MATCH: match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1) - (ARGSINJ: val_list_inject f1 args targs), - evalinf_funcall tge tm1 tfn targs t. - -Definition execinf_stmt_prop - (e: Csharpminor.env) (m1: mem) (s: Csharpminor.stmt) (t: traceinf): Prop := - forall cenv ts f1 te1 tm1 sp lo hi cs - (TR: transl_stmt cenv s = OK ts) - (MINJ: mem_inject f1 m1 tm1) - (MATCH: match_callstack f1 - (mkframe cenv e te1 sp lo hi :: cs) - m1.(nextblock) tm1.(nextblock) m1), - execinf_stmt tge (Vptr sp Int.zero) te1 tm1 ts t. - -Theorem transl_function_divergence_correct: - forall m1 fn args t, - Csharpminor.evalinf_funcall prog m1 fn args t -> - evalinf_funcall_prop m1 fn args t. -Proof. - unfold evalinf_funcall_prop; cofix FUNCALL. - assert (STMT: forall e m1 s t, - Csharpminor.execinf_stmt prog e m1 s t -> - execinf_stmt_prop e m1 s t). - unfold execinf_stmt_prop; cofix STMT. - intros. inv H; simpl in TR; try (monadInv TR). - (* Scall *) - assert (forall tv, val_inject f1 vf tv -> tv = vf). - intros. - elim (Genv.find_funct_inv H2). intros bf VF. rewrite VF in H2. - rewrite Genv.find_funct_find_funct_ptr in H2. - generalize (Genv.find_funct_ptr_negative H2). intro. - assert (match_globalenvs f1). eapply match_callstack_match_globalenvs; eauto. - generalize (mg_functions _ H5 _ H3). intro. - rewrite VF in H. inv H. - decEq. congruence. - replace x with 0. reflexivity. congruence. - destruct optid; monadInv TR. - (* optid = Some i *) - destruct (transl_expr_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H0 _ EQ) - as [tv1 [EVAL1 VINJ1]]. - destruct (transl_exprlist_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H1 _ EQ1) - as [tv2 [EVAL2 VINJ2]]. - rewrite <- (H _ VINJ1) in H2. - elim (functions_translated _ _ H2). intros tf [FIND TRF]. - apply execinf_Sseq_1. eapply execinf_Scall. - eauto. eauto. eauto. apply sig_preserved; auto. - eapply FUNCALL; eauto. - (* optid = None *) - destruct (transl_expr_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H0 _ EQ) - as [tv1 [EVAL1 VINJ1]]. - destruct (transl_exprlist_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H1 _ EQ1) - as [tv2 [EVAL2 VINJ2]]. - rewrite <- (H _ VINJ1) in H2. - elim (functions_translated _ _ H2). intros tf [FIND TRF]. - eapply execinf_Scall. - eauto. eauto. eauto. apply sig_preserved; auto. - eapply FUNCALL; eauto. - (* Sseq, 1 *) - apply execinf_Sseq_1. eapply STMT; eauto. - (* Sseq, 2 *) - destruct (transl_stmt_correct _ _ _ _ _ _ H0 - _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout [EXEC1 [OUT [MINJ2 [INCR12 MATCH2]]]]]]]]. - inv OUT. - eapply execinf_Sseq_2. eexact EXEC1. - eapply STMT; eauto. + induction 1; intros T1 MSTATE; inv MSTATE. + +(* skip seq *) + monadInv TR. left. + dependent induction MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + econstructor; split. + apply plus_one. constructor. + eapply match_state_seq; eauto. + exploit IHMK; eauto. intros [T2 [A B]]. + exists T2; split. eapply plus_left. constructor. apply plus_star; eauto. traceEq. auto. - (* Sifthenelse, true *) - destruct (transl_expr_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H0 _ EQ) - as [tv1 [EVAL1 VINJ1]]. - assert (transl_stmt cenv (if vb then sl1 else sl2) = - OK (if vb then x0 else x1)). destruct vb; auto. - eapply execinf_Sifthenelse. eexact EVAL1. - eapply bool_of_val_inject; eauto. - eapply STMT; eauto. - (* Sloop, body *) - eapply execinf_Sloop_body. eapply STMT; eauto. - (* Sloop, loop *) - destruct (transl_stmt_correct _ _ _ _ _ _ H0 - _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout [EXEC1 [OUT [MINJ2 [INCR12 MATCH2]]]]]]]]. - inv OUT. - eapply execinf_Sloop_loop. eexact EXEC1. - eapply STMT; eauto. - simpl. rewrite EQ. auto. auto. - (* Sblock *) - apply execinf_Sblock. eapply STMT; eauto. - (* stutter *) - generalize (execinf_stmt_N_inv _ _ _ _ _ _ H0); intro. - destruct s; try contradiction; monadInv TR. - apply execinf_Sseq_1. eapply STMT; eauto. - apply execinf_Sblock. eapply STMT; eauto. - (* Sloop_block *) - destruct (transl_stmt_correct _ _ _ _ _ _ H0 - _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout [EXEC1 [OUT [MINJ2 [INCR12 MATCH2]]]]]]]]. - inv OUT. - eapply execinf_Sloop_loop. eexact EXEC1. - eapply STMT with (s := Csharpminor.Sloop sl); eauto. - apply execinf_Sblock_inv; eauto. - simpl. rewrite EQ; auto. auto. - (* Function *) - intros. inv H. - monadInv TR. generalize EQ. - unfold transl_function. - caseEq (build_compilenv gce f); intros cenv stacksize CENV. - destruct (zle stacksize Int.max_signed); try congruence. - intro TR. monadInv TR. - caseEq (alloc tm1 0 stacksize). intros tm2 sp ALLOC. - destruct (function_entry_ok _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - H1 H2 MATCH CENV z ALLOC ARGSINJ MINJ H0 EQ2) - as [f2 [te2 [tm3 [STOREPARAM [MINJ2 [INCR12 [MATCH2 BLOCKS]]]]]]]. - eapply evalinf_funcall_internal; simpl. - eauto. reflexivity. eapply execinf_Sseq_2. eexact STOREPARAM. - unfold execinf_stmt_prop in STMT. eapply STMT; eauto. +(* skip block *) + monadInv TR. left. + dependent induction MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + exploit IHMK; eauto. intros [T2 [A B]]. + exists T2; split. eapply plus_left. constructor. apply plus_star; eauto. traceEq. + auto. +(* skip call *) + monadInv TR. left. + exploit match_is_call_cont; eauto. intros [tk' [A [B C]]]. + exploit match_callstack_freelist; eauto. intros [P Q]. + econstructor; split. + eapply plus_right. eexact A. apply step_skip_call. auto. + rewrite (sig_preserved_body _ _ _ _ TRF). auto. traceEq. + econstructor; eauto. rewrite nextblock_freelist. simpl. eauto. + +(* assign *) + monadInv TR. + exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. + exploit var_set_correct; eauto. intros [te' [tm' [EXEC [MINJ' [MCS' OTHER]]]]]. + left; econstructor; split. + apply plus_one. eexact EXEC. + econstructor; eauto. + +(* store *) + monadInv TR. + exploit transl_expr_correct. eauto. eauto. eexact H. eauto. + intros [tv1 [EVAL1 VINJ1]]. + exploit transl_expr_correct. eauto. eauto. eexact H0. eauto. + intros [tv2 [EVAL2 VINJ2]]. + exploit make_store_correct. eexact EVAL1. eexact EVAL2. eauto. eauto. auto. auto. + intros [tm' [EXEC [MINJ' NEXTBLOCK]]]. + left; econstructor; split. + apply plus_one. eexact EXEC. + unfold storev in H1; destruct vaddr; try discriminate. + econstructor; eauto. + replace (nextblock m') with (nextblock m). rewrite NEXTBLOCK. eauto. + eapply match_callstack_mapped; eauto. inv VINJ1. congruence. + symmetry. eapply nextblock_store; eauto. + +(* call *) + simpl in H1. exploit functions_translated; eauto. intros [tfd [FIND TRANS]]. + simpl in TR. destruct optid; monadInv TR. +(* with return value *) + exploit transl_expr_correct; eauto. + intros [tvf [EVAL1 VINJ1]]. + assert (tvf = vf). + eapply val_inject_function_pointer; eauto. + eapply match_callstack_match_globalenvs; eauto. + subst tvf. + exploit transl_exprlist_correct; eauto. + intros [tvargs [EVAL2 VINJ2]]. + left; econstructor; split. + eapply plus_left. constructor. apply star_one. + eapply step_call; eauto. + apply sig_preserved; eauto. traceEq. -Qed. + econstructor; eauto. + eapply match_Kcall_some with (cenv' := cenv); eauto. + red; auto. +(* without return value *) + exploit transl_expr_correct; eauto. + intros [tvf [EVAL1 VINJ1]]. + assert (tvf = vf). + eapply val_inject_function_pointer; eauto. + eapply match_callstack_match_globalenvs; eauto. + subst tvf. + exploit transl_exprlist_correct; eauto. + intros [tvargs [EVAL2 VINJ2]]. + left; econstructor; split. + apply plus_one. + eapply step_call; eauto. + apply sig_preserved; eauto. + econstructor; eauto. + eapply match_Kcall_none with (cenv' := cenv); eauto. + red; auto. -(** ** Semantic preservation for whole programs *) +(* seq *) + monadInv TR. + left; econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + econstructor; eauto. +(* seq 2 *) + right. split. auto. split. auto. econstructor; eauto. + +(* ifthenelse *) + monadInv TR. + exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. + left; exists (State tfn (if b then x0 else x1) tk (Vptr sp Int.zero) te tm); split. + apply plus_one. eapply step_ifthenelse; eauto. eapply bool_of_val_inject; eauto. + econstructor; eauto. destruct b; auto. + +(* loop *) + monadInv TR. + left; econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + econstructor; eauto. simpl. rewrite EQ; auto. -(** The [match_globalenvs] relation holds for the global environments - of the source program and the transformed program. *) +(* block *) + monadInv TR. + left; econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + econstructor; eauto. + +(* exit seq *) + monadInv TR. left. + dependent induction MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl. auto. + exploit IHMK; eauto. intros [T2 [A B]]. + exists T2; split; auto. eapply plus_left. constructor. apply plus_star; eauto. traceEq. + exploit IHMK; eauto. intros [T2 [A B]]. + exists T2; split; auto. eapply plus_left. + simpl. constructor. apply plus_star; eauto. traceEq. + +(* exit block 0 *) + monadInv TR. left. + dependent induction MK. + econstructor; split. + simpl. apply plus_one. constructor. + econstructor; eauto. + exploit IHMK; eauto. intros [T2 [A B]]. + exists T2; split; auto. simpl. + eapply plus_left. constructor. apply plus_star; eauto. traceEq. + +(* exit block n+1 *) + monadInv TR. left. + dependent induction MK. + econstructor; split. + simpl. apply plus_one. constructor. + econstructor; eauto. auto. + exploit IHMK; eauto. intros [T2 [A B]]. + exists T2; split; auto. simpl. + eapply plus_left. constructor. apply plus_star; eauto. traceEq. + +(* switch *) + monadInv TR. left. + exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. + inv VINJ. + exploit switch_descent; eauto. intros [k1 [A B]]. + exploit switch_ascent; eauto. intros [k2 [C D]]. + exploit transl_lblstmt_suffix; eauto. simpl. intros [body' [ts' E]]. + exploit switch_match_states; eauto. intros [T2 [F G]]. + exists T2; split. + eapply plus_star_trans. eapply B. + eapply star_left. econstructor; eauto. + eapply star_trans. eexact C. + apply plus_star. eexact F. + reflexivity. reflexivity. traceEq. + auto. + +(* return none *) + monadInv TR. left. + exploit match_callstack_freelist; eauto. intros [A B]. + econstructor; split. + apply plus_one. apply step_return_0. +(* + rewrite (sig_preserved_body _ _ _ _ TRF). auto. +*) + econstructor; eauto. rewrite nextblock_freelist. simpl. eauto. + eapply match_call_cont; eauto. + +(* return some *) + monadInv TR. left. + exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. + exploit match_callstack_freelist; eauto. intros [A B]. + econstructor; split. + apply plus_one. apply step_return_1. eauto. + econstructor; eauto. rewrite nextblock_freelist. simpl. eauto. + eapply match_call_cont; eauto. + +(* label *) + monadInv TR. + left; econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + +(* goto *) + monadInv TR. + exploit transl_find_label_body; eauto. + intros [ts' [tk' [xenv' [A [B C]]]]]. + left; econstructor; split. + apply plus_one. apply step_goto. eexact A. + econstructor; eauto. + +(* internal call *) + monadInv TR. generalize EQ; clear EQ; unfold transl_function. + caseEq (build_compilenv gce f). intros ce sz BC. + destruct (zle sz Int.max_signed); try congruence. + intro TRBODY. + generalize TRBODY; intro TMP. monadInv TMP. + caseEq (alloc tm 0 sz). intros tm' sp ALLOC'. + exploit function_entry_ok; eauto. + intros [f2 [te2 [tm2 [EXEC [MINJ2 [IINCR MCS2]]]]]]. + left; econstructor; split. + eapply plus_left. constructor; simpl; eauto. + simpl. eapply star_left. constructor. + eapply star_right. eexact EXEC. constructor. + reflexivity. reflexivity. traceEq. + econstructor. eexact TRBODY. eauto. eexact MINJ2. + eexact MCS2. + inv MK; simpl in ISCC; contradiction || econstructor; eauto. + +(* external call *) + monadInv TR. + exploit event_match_inject; eauto. intros [A B]. + left; econstructor; split. + apply plus_one. econstructor; eauto. + econstructor; eauto. + +(* return *) + inv MK; inv H. + (* no argument *) + left; econstructor; split. + apply plus_one. econstructor; eauto. + simpl. econstructor; eauto. + (* one argument *) + exploit var_set_self_correct; eauto. + intros [te' [tm' [A [B C]]]]. + left; econstructor; split. + eapply plus_left. econstructor. simpl. eapply star_left. econstructor. + eapply star_one. eexact A. + reflexivity. traceEq. + econstructor; eauto. +Qed. Lemma match_globalenvs_init: let m := Genv.init_mem prog in - let tm := Genv.init_mem tprog in - let f := fun b => if zlt b m.(nextblock) then Some(b, 0) else None in - match_globalenvs f. + match_globalenvs (meminj_init m). Proof. intros. constructor. intros. split. - unfold f. rewrite zlt_true. auto. unfold m. - eapply Genv.find_symbol_not_fresh; eauto. + unfold meminj_init. rewrite zlt_true. auto. + unfold m; eapply Genv.find_symbol_not_fresh; eauto. rewrite <- H. apply symbols_preserved. - intros. unfold f. rewrite zlt_true. auto. + intros. unfold meminj_init. rewrite zlt_true. auto. generalize (nextblock_pos m). omega. Qed. -(** The correctness of the translation of a whole Csharpminor program - follows. *) +Lemma transl_initial_states: + forall S, Csharpminor.initial_state prog S -> + exists R, Cminor.initial_state tprog R /\ match_states S R. +Proof. + induction 1. + exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. + econstructor; split. + econstructor. + simpl. fold tge. rewrite symbols_preserved. + replace (prog_main tprog) with (prog_main prog). eexact H. + symmetry. unfold transl_program in TRANSL. + eapply transform_partial_program2_main; eauto. + eexact FIND. + rewrite <- H1. apply sig_preserved; auto. + rewrite (Genv.init_mem_transf_partial2 _ _ _ TRANSL). + fold m0. + eapply match_callstate with (f := meminj_init m0) (cs := @nil frame). + auto. + apply init_inject. unfold m0. apply Genv.initmem_inject_neutral. + constructor. apply match_globalenvs_init. + instantiate (1 := gce). constructor. + red; auto. + constructor. +Qed. + +Lemma transl_final_states: + forall S R r, + match_states S R -> Csharpminor.final_state S r -> Cminor.final_state R r. +Proof. + intros. inv H0. inv H. inv MK. inv RESINJ. constructor. +Qed. Theorem transl_program_correct: - forall beh, + forall (beh: program_behavior), Csharpminor.exec_program prog beh -> - exec_program tprog beh. -Proof. - intros. apply exec_program_bigstep_transition. - set (m0 := Genv.init_mem prog) in *. - set (f := meminj_init m0). - assert (MINJ0: mem_inject f m0 m0). - unfold f; apply init_inject. - unfold m0; apply Genv.initmem_inject_neutral. - assert (MATCH0: match_callstack f nil m0.(nextblock) m0.(nextblock) m0). - constructor. unfold f; apply match_globalenvs_init. - inv H. - (* Terminating case *) - subst ge0 m1. - elim (function_ptr_translated _ _ H1). intros tfn [TFIND TR]. - fold ge in H3. - exploit transl_function_correct; eauto. - intros [f1 [tm1 [tres [TEVAL [VINJ [MINJ1 [INCR MATCH1]]]]]]]. - econstructor; eauto. - fold tge. rewrite <- H0. fold ge. - replace (prog_main prog) with (AST.prog_main tprog). apply symbols_preserved. - apply transform_partial_program2_main with (transl_fundef gce) transl_globvar. assumption. - rewrite <- H2. apply sig_preserved; auto. - rewrite (Genv.init_mem_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). - inv VINJ. fold tge; fold m0. eexact TEVAL. - (* Diverging case *) - subst ge0 m1. - elim (function_ptr_translated _ _ H1). intros tfn [TFIND TR]. - econstructor; eauto. - fold tge. rewrite <- H0. fold ge. - replace (prog_main prog) with (AST.prog_main tprog). apply symbols_preserved. - apply transform_partial_program2_main with (transl_fundef gce) transl_globvar. assumption. - rewrite <- H2. apply sig_preserved; auto. - rewrite (Genv.init_mem_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). - fold tge; fold m0. - eapply (transl_function_divergence_correct _ _ _ _ H3); eauto. + Cminor.exec_program tprog beh. +Proof. + unfold Csharpminor.exec_program, Cminor.exec_program; intros. + eapply simulation_star_preservation; eauto. + eexact transl_initial_states. + eexact transl_final_states. + eexact transl_step_correct. Qed. End TRANSLATION. + -- cgit v1.2.3