From a7c6cf8d4d59e29ed73f9eb8bfc015b0384672a1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:33:05 +0000 Subject: Revu la repartition des sources Coq en sous-repertoires git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@73 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgenproof.v | 2595 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 2595 insertions(+) create mode 100644 cfrontend/Cminorgenproof.v (limited to 'cfrontend/Cminorgenproof.v') diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v new file mode 100644 index 0000000..7820095 --- /dev/null +++ b/cfrontend/Cminorgenproof.v @@ -0,0 +1,2595 @@ +(** Correctness proof for Cminor generation. *) + +Require Import Coqlib. +Require Import Maps. +Require Import Sets. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Events. +Require Import Globalenvs. +Require Import Csharpminor. +Require Import Op. +Require Import Cminor. +Require Cmconstr. +Require Import Cminorgen. +Require Import Cmconstrproof. + +Section TRANSLATION. + +Variable prog: Csharpminor.program. +Variable tprog: program. +Hypothesis TRANSL: transl_program prog = Some tprog. +Let ge : Csharpminor.genv := Genv.globalenv (program_of_program prog). +Let tge: genv := Genv.globalenv tprog. +Let gce : compilenv := build_global_compilenv prog. + +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_fundef gce). + exact TRANSL. +Qed. + +Lemma function_ptr_translated: + forall (b: block) (f: Csharpminor.fundef), + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transl_fundef gce f = Some tf. +Proof. + intros. + generalize + (Genv.find_funct_ptr_transf_partial (transl_fundef gce) TRANSL H). + case (transl_fundef gce f). + intros tf [A B]. exists tf. tauto. + intros [A B]. elim B. reflexivity. +Qed. + +Lemma functions_translated: + forall (v: val) (f: Csharpminor.fundef), + Genv.find_funct ge v = Some f -> + exists tf, + Genv.find_funct tge v = Some tf /\ transl_fundef gce f = Some tf. +Proof. + intros. + generalize + (Genv.find_funct_transf_partial (transl_fundef gce) TRANSL H). + case (transl_fundef gce f). + intros tf [A B]. exists tf. tauto. + intros [A B]. elim B. reflexivity. +Qed. + +Lemma sig_preserved: + forall f tf, + transl_fundef gce f = Some tf -> + Cminor.funsig tf = Csharpminor.funsig f. +Proof. + intros until tf; destruct f; simpl. + unfold transl_function. destruct (build_compilenv gce f). + case (zle z Int.max_signed); try congruence. + intro. case (transl_stmt c (Csharpminor.fn_body f)); simpl; try congruence. + intros. inversion H. reflexivity. + intro. inversion H; reflexivity. +Qed. + +Definition global_compilenv_match (ce: compilenv) (gv: gvarenv) : Prop := + forall id, + match ce!!id with + | Var_global_scalar chunk => gv!id = Some (Vscalar chunk) + | Var_global_array => True + | _ => False + end. + +Lemma global_compilenv_charact: + global_compilenv_match gce (global_var_env prog). +Proof. + set (mkgve := fun gv (vars: list (ident * var_kind * list init_data)) => + List.fold_left + (fun gve x => match x with (id, k, init) => PTree.set id k gve end) + vars gv). + assert (forall vars gv ce, + global_compilenv_match ce gv -> + global_compilenv_match (List.fold_left assign_global_variable vars ce) + (mkgve gv vars)). + induction vars; simpl; intros. + auto. + apply IHvars. intro id1. unfold assign_global_variable. + destruct a as [[id2 lv2] init2]. destruct lv2; simpl; rewrite PMap.gsspec; rewrite PTree.gsspec. + 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.(Csharpminor.prog_vars)). + unfold gce, build_global_compilenv. apply H. + intro. rewrite PMap.gi. auto. +Qed. + +(** * Correspondence between Csharpminor's and Cminor's environments and memory states *) + +(** In Csharpminor, every variable is stored in a separate memory block. + In the corresponding Cminor code, some of these variables reside in + the local variable environment; others are sub-blocks of the stack data + block. We capture these changes in memory via a memory injection [f]: +- [f b = None] means that the Csharpminor block [b] no longer exist + in the execution of the generated Cminor code. This corresponds to + a Csharpminor local variable translated to a Cminor local variable. +- [f b = Some(b', ofs)] means that Csharpminor block [b] corresponds + to a sub-block of Cminor block [b] at offset [ofs]. + + A memory injection [f] defines a relation [val_inject f] between + values and a relation [mem_inject f] between memory states. + These relations, defined in file [Memory], will be used intensively + in our proof of simulation between Csharpminor and Cminor executions. + + In the remainder of this section, we define relations between + Csharpminor and Cminor environments and call stacks. *) + +(** Matching for a Csharpminor variable [id]. +- If this variable is mapped to a Cminor local variable, the + corresponding Csharpminor memory block [b] must no longer exist in + Cminor ([f b = None]). Moreover, the content of block [b] must + match the value of [id] found in the Cminor local environment [te]. +- If this variable is mapped to a sub-block of the Cminor stack data + at offset [ofs], the address of this variable in Csharpminor [Vptr b + Int.zero] must match the address of the sub-block [Vptr sp (Int.repr + ofs)]. +*) + +Inductive match_var (f: meminj) (id: ident) + (e: Csharpminor.env) (m: mem) (te: env) (sp: block) : + var_info -> Prop := + | match_var_local: + forall chunk b v v', + PTree.get id e = Some (b, Vscalar chunk) -> + Mem.load chunk m b 0 = Some v -> + f b = None -> + PTree.get id te = Some v' -> + val_inject f v v' -> + match_var f id e m te sp (Var_local chunk) + | match_var_stack_scalar: + forall chunk ofs b, + PTree.get id e = Some (b, Vscalar chunk) -> + val_inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) -> + match_var f id e m te sp (Var_stack_scalar chunk ofs) + | match_var_stack_array: + forall ofs sz b, + PTree.get id e = Some (b, Varray sz) -> + val_inject f (Vptr b Int.zero) (Vptr sp (Int.repr ofs)) -> + match_var f id e m te sp (Var_stack_array ofs) + | match_var_global_scalar: + forall chunk, + PTree.get id e = None -> + PTree.get id (global_var_env prog) = Some (Vscalar chunk) -> + match_var f id e m te sp (Var_global_scalar chunk) + | match_var_global_array: + PTree.get id e = None -> + match_var f id e m te sp (Var_global_array). + +(** Matching between a Csharpminor environment [e] and a Cminor + environment [te]. The [lo] and [hi] parameters delimit the range + of addresses for the blocks referenced from [te]. *) + +Record match_env (f: meminj) (cenv: compilenv) + (e: Csharpminor.env) (m: mem) (te: env) (sp: block) + (lo hi: Z) : Prop := + mk_match_env { + +(** Each variable mentioned in the compilation environment must match + as defined above. *) + me_vars: + forall id, match_var f id e m te sp (PMap.get id cenv); + +(** The range [lo, hi] must not be empty. *) + me_low_high: + lo <= hi; + +(** Every block appearing in the Csharpminor environment [e] must be + in the range [lo, hi]. *) + me_bounded: + forall id b lv, PTree.get id e = Some(b, lv) -> lo <= b < hi; + +(** Distinct Csharpminor local variables must be mapped to distinct blocks. *) + me_inj: + forall id1 b1 lv1 id2 b2 lv2, + PTree.get id1 e = Some(b1, lv1) -> + 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]. *) + me_inv: + forall b delta, + f b = Some(sp, delta) -> lo <= b < hi; + +(** All Csharpminor blocks below [lo] (i.e. allocated before the blocks + referenced from [e]) must map to blocks that are below [sp] + (i.e. allocated before the stack data for the current Cminor function). *) + me_incr: + forall b tb delta, + f b = Some(tb, delta) -> b < lo -> tb < sp + }. + +(** Global environments match if the memory injection [f] leaves unchanged + the references to global symbols and functions. *) + +Record match_globalenvs (f: meminj) : Prop := + mk_match_globalenvs { + mg_symbols: + forall id b, + Genv.find_symbol ge id = Some b -> + f b = Some (b, 0) /\ Genv.find_symbol tge id = Some b; + mg_functions: + forall b, b < 0 -> f b = Some(b, 0) + }. + +(** Call stacks represent abstractly the execution state of the current + Csharpminor and Cminor functions, as well as the states of the + calling functions. A call stack is a list of frames, each frame + collecting information on the current execution state of a Csharpminor + function and its Cminor translation. *) + +Record frame : Set := + mkframe { + fr_cenv: compilenv; + fr_e: Csharpminor.env; + fr_te: env; + fr_sp: block; + fr_low: Z; + fr_high: Z + }. + +Definition callstack : Set := list frame. + +(** Matching of call stacks imply matching of environments for each of + the frames, plus matching of the global environments, plus disjointness + conditions over the memory blocks allocated for local variables + and Cminor stack data. *) + +Inductive match_callstack: meminj -> callstack -> Z -> Z -> mem -> Prop := + | mcs_nil: + forall f bound tbound m, + match_globalenvs f -> + match_callstack f nil bound tbound m + | mcs_cons: + forall f cenv e te sp lo hi cs bound tbound m, + hi <= bound -> + sp < tbound -> + match_env f cenv e m te sp lo hi -> + match_callstack f cs lo sp m -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m. + +(** The remainder of this section is devoted to showing preservation + of the [match_callstack] invariant under various assignments and memory + stores. First: preservation by memory stores to ``mapped'' blocks + (block that have a counterpart in the Cminor execution). *) + +Lemma match_env_store_mapped: + forall f cenv e m1 m2 te sp lo hi chunk b ofs v, + f b <> None -> + store chunk m1 b ofs v = Some m2 -> + match_env f cenv e m1 te sp lo hi -> + match_env f cenv e m2 te sp lo hi. +Proof. + intros. inversion H1. constructor; auto. + (* vars *) + intros. generalize (me_vars0 id); intro. + inversion H2; econstructor; eauto. + rewrite <- H5. eapply load_store_other; eauto. + left. congruence. +Qed. + +Lemma match_callstack_mapped: + forall f cs bound tbound m1, + match_callstack f cs bound tbound m1 -> + forall chunk b ofs v m2, + f b <> None -> + store chunk m1 b ofs v = Some m2 -> + match_callstack f cs bound tbound m2. +Proof. + induction 1; intros; econstructor; eauto. + eapply match_env_store_mapped; eauto. +Qed. + +(** Preservation by assignment to a Csharpminor variable that is + translated to a Cminor local variable. The value being assigned + must be normalized with respect to the memory chunk of the variable, + in the following sense. *) + +(* +Definition val_normalized (chunk: memory_chunk) (v: val) : Prop := + exists v0, v = Val.load_result chunk v0. + +Lemma load_result_idem: + forall chunk v, + Val.load_result chunk (Val.load_result chunk v) = + Val.load_result chunk v. +Proof. + destruct chunk; destruct v; simpl; auto. + rewrite Int.cast8_signed_idem; auto. + rewrite Int.cast8_unsigned_idem; auto. + rewrite Int.cast16_signed_idem; auto. + rewrite Int.cast16_unsigned_idem; auto. + rewrite Float.singleoffloat_idem; auto. +Qed. + +Lemma load_result_normalized: + forall chunk v, + val_normalized chunk v -> Val.load_result chunk v = v. +Proof. + intros chunk v [v0 EQ]. rewrite EQ. apply load_result_idem. +Qed. +*) +Lemma match_env_store_local: + forall f cenv e m1 m2 te sp lo hi id b chunk v tv, + e!id = Some(b, Vscalar chunk) -> + val_inject f (Val.load_result chunk v) tv -> + store chunk m1 b 0 v = Some m2 -> + match_env f cenv e m1 te sp lo hi -> + match_env f cenv e m2 (PTree.set id tv te) sp lo hi. +Proof. + intros. inversion H2. constructor; auto. + intros. generalize (me_vars0 id0); intro. + inversion H3; subst. + (* var_local *) + case (peq id id0); intro. + (* the stored variable *) + subst id0. + change Csharpminor.var_kind with var_kind in H4. + rewrite H in H5. injection H5; clear H5; intros; subst b0 chunk0. + econstructor. eauto. + eapply load_store_same; eauto. auto. + rewrite PTree.gss. reflexivity. + auto. + (* a different variable *) + econstructor; eauto. + rewrite <- H6. eapply load_store_other; eauto. + rewrite PTree.gso; auto. + (* var_stack_scalar *) + econstructor; eauto. + (* var_stack_array *) + econstructor; eauto. + (* var_global_scalar *) + econstructor; eauto. + (* var_global_array *) + econstructor; eauto. +Qed. + +Lemma match_env_store_above: + forall f cenv e m1 m2 te sp lo hi chunk b v, + store chunk m1 b 0 v = Some m2 -> + hi <= b -> + match_env f cenv e m1 te sp lo hi -> + match_env f cenv e m2 te sp lo hi. +Proof. + intros. inversion H1; constructor; auto. + intros. generalize (me_vars0 id); intro. + inversion H2; econstructor; eauto. + rewrite <- H5. eapply load_store_other; eauto. + left. generalize (me_bounded0 _ _ _ H4). unfold block in *. omega. +Qed. + +Lemma match_callstack_store_above: + forall f cs bound tbound m1, + match_callstack f cs bound tbound m1 -> + forall chunk b v m2, + store chunk m1 b 0 v = Some m2 -> + bound <= b -> + match_callstack f cs bound tbound m2. +Proof. + induction 1; intros; econstructor; eauto. + eapply match_env_store_above with (b := b); eauto. omega. + eapply IHmatch_callstack; eauto. + inversion H1. omega. +Qed. + +Lemma match_callstack_store_local: + forall f cenv e te sp lo hi cs bound tbound m1 m2 id b chunk v tv, + e!id = Some(b, Vscalar chunk) -> + val_inject f (Val.load_result chunk v) tv -> + store chunk m1 b 0 v = Some m2 -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m1 -> + match_callstack f (mkframe cenv e (PTree.set id tv te) sp lo hi :: cs) bound tbound m2. +Proof. + intros. inversion H2. constructor; auto. + eapply match_env_store_local; eauto. + eapply match_callstack_store_above; eauto. + inversion H16. + generalize (me_bounded0 _ _ _ H). omega. +Qed. + +(** A variant of [match_callstack_store_local] where the Cminor environment + [te] already associates to [id] a value that matches the assigned value. + In this case, [match_callstack] is preserved even if no assignment + takes place on the Cminor side. *) + +Lemma match_env_extensional: + forall f cenv e m te1 sp lo hi, + match_env f cenv e m te1 sp lo hi -> + forall te2, + (forall id, te2!id = te1!id) -> + match_env f cenv e m te2 sp lo hi. +Proof. + induction 1; intros; econstructor; eauto. + intros. generalize (me_vars0 id); intro. + inversion H0; econstructor; eauto. + rewrite H. auto. +Qed. + +Lemma match_callstack_store_local_unchanged: + forall f cenv e te sp lo hi cs bound tbound m1 m2 id b chunk v tv, + e!id = Some(b, Vscalar chunk) -> + val_inject f (Val.load_result chunk v) tv -> + store chunk m1 b 0 v = Some m2 -> + te!id = Some tv -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m1 -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m2. +Proof. + intros. inversion H3. constructor; auto. + apply match_env_extensional with (PTree.set id tv te). + eapply match_env_store_local; eauto. + intros. rewrite PTree.gsspec. + case (peq id0 id); intros. congruence. auto. + eapply match_callstack_store_above; eauto. + inversion H17. + generalize (me_bounded0 _ _ _ H). omega. +Qed. + +(** Preservation of [match_callstack] by freeing all blocks allocated + for local variables at function entry (on the Csharpminor side). *) + +Lemma match_callstack_incr_bound: + forall f cs bound tbound m, + match_callstack f cs bound tbound m -> + forall bound' tbound', + bound <= bound' -> tbound <= tbound' -> + match_callstack f cs bound' tbound' m. +Proof. + intros. inversion H; constructor; auto. omega. omega. +Qed. + +Lemma load_freelist: + forall fbl chunk m b ofs, + (forall b', In b' fbl -> b' <> b) -> + load chunk (free_list m fbl) b ofs = load chunk m b ofs. +Proof. + induction fbl; simpl; intros. + auto. + rewrite load_free. apply IHfbl. + intros. apply H. tauto. + apply sym_not_equal. apply H. tauto. +Qed. + +Lemma match_env_freelist: + forall f cenv e m te sp lo hi fbl, + match_env f cenv e m te sp lo hi -> + (forall b, In b fbl -> hi <= b) -> + match_env f cenv e (free_list m fbl) te sp lo hi. +Proof. + intros. inversion H. econstructor; eauto. + intros. generalize (me_vars0 id); intro. + inversion H1; econstructor; eauto. + rewrite <- H4. apply load_freelist. + intros. generalize (H0 _ H8); intro. + generalize (me_bounded0 _ _ _ H3). unfold block; omega. +Qed. + +Lemma match_callstack_freelist_rec: + forall f cs bound tbound m, + match_callstack f cs bound tbound m -> + forall fbl, + (forall b, In b fbl -> bound <= b) -> + match_callstack f cs bound tbound (free_list m fbl). +Proof. + induction 1; intros; constructor; auto. + eapply match_env_freelist; eauto. + intros. generalize (H3 _ H4). omega. + apply IHmatch_callstack. intros. + generalize (H3 _ H4). inversion H1. omega. +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) -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m -> + match_callstack f cs bound tbound (free_list m fbl). +Proof. + intros. inversion H0. inversion H14. + apply match_callstack_incr_bound with lo sp. + apply match_callstack_freelist_rec. auto. + assumption. + omega. omega. +Qed. + +(** Preservation of [match_callstack] when allocating a block for + a local variable on the Csharpminor side. *) + +Lemma load_from_alloc_is_undef: + forall m1 chunk m2 b, + alloc m1 0 (size_chunk chunk) = (m2, b) -> + load chunk m2 b 0 = Some Vundef. +Proof. + intros. + assert (valid_block m2 b). eapply valid_new_block; eauto. + assert (low_bound m2 b <= 0). + generalize (low_bound_alloc _ _ b _ _ _ H). rewrite zeq_true. omega. + assert (0 + size_chunk chunk <= high_bound m2 b). + generalize (high_bound_alloc _ _ b _ _ _ H). rewrite zeq_true. omega. + elim (load_in_bounds _ _ _ _ H0 H1 H2). intros v LOAD. + assert (v = Vundef). eapply load_alloc_same; eauto. + congruence. +Qed. + +Lemma match_env_alloc_same: + forall m1 lv m2 b info f1 cenv1 e1 te sp lo id data tv, + alloc m1 0 (sizeof lv) = (m2, b) -> + match info with + | Var_local chunk => data = None /\ lv = Vscalar chunk + | Var_stack_scalar chunk pos => data = Some(sp, pos) /\ lv = Vscalar chunk + | Var_stack_array pos => data = Some(sp, pos) /\ exists sz, lv = Varray sz + | Var_global_scalar chunk => False + | Var_global_array => False + end -> + match_env f1 cenv1 e1 m1 te sp lo m1.(nextblock) -> + te!id = Some tv -> + 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 + inject_incr f1 f2 -> + match_env f2 cenv2 e2 m2 te sp lo m2.(nextblock). +Proof. + intros. + assert (b = m1.(nextblock)). + injection H; intros. auto. + assert (m2.(nextblock) = Zsucc m1.(nextblock)). + injection H; intros. rewrite <- H6; reflexivity. + inversion H1. constructor. + (* me_vars *) + intros id0. unfold cenv2. rewrite PMap.gsspec. case (peq id0 id); intros. + (* same var *) + subst id0. destruct info. + (* info = Var_local chunk *) + elim H0; intros. + 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. + unfold f2, extend_inject, eq_block. rewrite zeq_true. auto. + auto. + constructor. + (* info = Var_stack_scalar chunk ofs *) + elim H0; intros. + apply match_var_stack_scalar with b. + unfold e2; rewrite PTree.gss. congruence. + eapply val_inject_ptr. + unfold f2, extend_inject, eq_block. rewrite zeq_true. eauto. + rewrite Int.add_commut. rewrite Int.add_zero. auto. + (* info = Var_stack_array z *) + elim H0; intros A [sz B]. + apply match_var_stack_array with sz b. + unfold e2; rewrite PTree.gss. congruence. + eapply val_inject_ptr. + unfold f2, extend_inject, eq_block. rewrite zeq_true. eauto. + rewrite Int.add_commut. rewrite Int.add_zero. auto. + (* info = Var_global *) + contradiction. + contradiction. + (* other vars *) + generalize (me_vars0 id0); intros. + inversion H6; econstructor; eauto. + unfold e2; rewrite PTree.gso; auto. + unfold f2, extend_inject, eq_block; rewrite zeq_false; auto. + generalize (me_bounded0 _ _ _ H8). unfold block in *; omega. + unfold e2; rewrite PTree.gso; eauto. + unfold e2; rewrite PTree.gso; eauto. + unfold e2; rewrite PTree.gso; eauto. + unfold e2; rewrite PTree.gso; eauto. + (* lo <= hi *) + unfold block in *; omega. + (* 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. + (* 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. + 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. + (* me_incr *) + intros until delta. unfold f2, extend_inject, eq_block. + case (zeq b0 b); intros. + subst b0. unfold block in *; omegaContradiction. + eauto. +Qed. + +Lemma match_env_alloc_other: + forall f1 cenv e m1 m2 te sp lo hi chunk b data, + alloc m1 0 (sizeof chunk) = (m2, b) -> + match data with None => True | Some (b', delta') => sp < b' end -> + hi <= m1.(nextblock) -> + match_env f1 cenv e m1 te sp lo hi -> + let f2 := extend_inject b data f1 in + inject_incr f1 f2 -> + match_env f2 cenv e m2 te sp lo hi. +Proof. + intros. + assert (b = m1.(nextblock)). injection H; auto. + rewrite <- H4 in H1. + inversion H2. constructor; auto. + (* me_vars *) + intros. generalize (me_vars0 id); intro. + inversion H5; econstructor; eauto. + unfold f2, extend_inject, eq_block. rewrite zeq_false. auto. + generalize (me_bounded0 _ _ _ H7). unfold block in *; omega. + (* me_bounded *) + intros until delta. unfold f2, extend_inject, eq_block. + case (zeq b0 b); intros. rewrite H5 in H0. omegaContradiction. + eauto. + (* me_incr *) + intros until delta. unfold f2, extend_inject, eq_block. + case (zeq b0 b); intros. subst b0. omegaContradiction. + eauto. +Qed. + +Lemma match_callstack_alloc_other: + forall f1 cs bound tbound m1, + match_callstack f1 cs bound tbound m1 -> + forall lv m2 b data, + alloc m1 0 (sizeof lv) = (m2, b) -> + match data with None => True | Some (b', delta') => tbound <= b' end -> + bound <= m1.(nextblock) -> + let f2 := extend_inject b data f1 in + inject_incr f1 f2 -> + match_callstack f2 cs bound tbound m2. +Proof. + induction 1; intros. + constructor. + inversion H. constructor. + intros. auto. + intros. elim (mg_symbols0 _ _ H4); intros. + split; auto. elim (H3 b0); intros; congruence. + intros. generalize (mg_functions0 _ H4). elim (H3 b0); congruence. + constructor. auto. auto. + unfold f2; eapply match_env_alloc_other; eauto. + destruct data; auto. destruct p. omega. omega. + unfold f2; eapply IHmatch_callstack; eauto. + destruct data; auto. destruct p. omega. + inversion H1; omega. +Qed. + +Lemma match_callstack_alloc_left: + forall m1 lv m2 b info f1 cenv1 e1 te sp lo id data cs tv tbound, + alloc m1 0 (sizeof lv) = (m2, b) -> + match info with + | Var_local chunk => data = None /\ lv = Vscalar chunk + | Var_stack_scalar chunk pos => data = Some(sp, pos) /\ lv = Vscalar chunk + | Var_stack_array pos => data = Some(sp, pos) /\ exists sz, lv = Varray sz + | Var_global_scalar chunk => False + | Var_global_array => False + end -> + match_callstack f1 (mkframe cenv1 e1 te sp lo m1.(nextblock) :: cs) m1.(nextblock) tbound m1 -> + te!id = Some tv -> + 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 + inject_incr f1 f2 -> + match_callstack f2 (mkframe cenv2 e2 te sp lo m2.(nextblock) :: cs) m2.(nextblock) tbound m2. +Proof. + intros. inversion H1. constructor. omega. auto. + 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. + contradiction. + contradiction. + inversion H17; omega. +Qed. + +Lemma match_callstack_alloc_right: + forall f cs bound tm1 m tm2 lo hi b, + alloc tm1 lo hi = (tm2, b) -> + match_callstack f cs bound tm1.(nextblock) m -> + match_callstack f cs bound tm2.(nextblock) m. +Proof. + intros. eapply match_callstack_incr_bound; eauto. omega. + injection H; intros. rewrite <- H2; simpl. omega. +Qed. + +Lemma match_env_alloc: + forall m1 l h m2 b tm1 tm2 tb f1 ce e te sp lo hi, + alloc m1 l h = (m2, b) -> + alloc tm1 l h = (tm2, tb) -> + match_env f1 ce e m1 te sp lo hi -> + hi <= m1.(nextblock) -> + sp < tm1.(nextblock) -> + let f2 := extend_inject b (Some(tb, 0)) f1 in + inject_incr f1 f2 -> + match_env f2 ce e m2 te sp lo hi. +Proof. + intros. + assert (BEQ: b = m1.(nextblock)). injection H; auto. + assert (TBEQ: tb = tm1.(nextblock)). injection H0; auto. + inversion H1. constructor; auto. + (* me_vars *) + intros. generalize (me_vars0 id); intro. inversion H5. + (* var_local *) + econstructor; eauto. + generalize (me_bounded0 _ _ _ H7). intro. + unfold f2, extend_inject. case (eq_block b0 b); intro. + subst b0. rewrite BEQ in H12. omegaContradiction. + auto. + (* var_stack_scalar *) + econstructor; eauto. + (* var_stack_array *) + econstructor; eauto. + (* var_global_scalar *) + econstructor; eauto. + (* var_global_array *) + econstructor; eauto. + (* me_bounded *) + intros until delta. unfold f2, extend_inject. case (eq_block b0 b); intro. + intro. injection H5; clear H5; intros. + rewrite H6 in TBEQ. rewrite TBEQ in H3. omegaContradiction. + eauto. + (* me_inj *) + intros until delta. unfold f2, extend_inject. case (eq_block b0 b); intros. + injection H5; clear H5; intros; subst b0 tb0 delta. + rewrite BEQ in H6. omegaContradiction. + eauto. +Qed. + +Lemma match_callstack_alloc_rec: + forall f1 cs bound tbound m1, + match_callstack f1 cs bound tbound m1 -> + forall l h m2 b tm1 tm2 tb, + alloc m1 l h = (m2, b) -> + alloc tm1 l h = (tm2, tb) -> + bound <= m1.(nextblock) -> + tbound <= tm1.(nextblock) -> + let f2 := extend_inject b (Some(tb, 0)) f1 in + inject_incr f1 f2 -> + match_callstack f2 cs bound tbound m2. +Proof. + induction 1; intros. + constructor. + inversion H. constructor. + intros. elim (mg_symbols0 _ _ H5); intros. + split; auto. elim (H4 b0); intros; congruence. + intros. generalize (mg_functions0 _ H5). elim (H4 b0); congruence. + constructor. auto. auto. + unfold f2. eapply match_env_alloc; eauto. omega. omega. + unfold f2; eapply IHmatch_callstack; eauto. + inversion H1; omega. + omega. +Qed. + +Lemma match_callstack_alloc: + forall f1 cs m1 tm1 l h m2 b tm2 tb, + match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1 -> + alloc m1 l h = (m2, b) -> + alloc tm1 l h = (tm2, tb) -> + let f2 := extend_inject b (Some(tb, 0)) f1 in + inject_incr f1 f2 -> + match_callstack f2 cs m2.(nextblock) tm2.(nextblock) m2. +Proof. + intros. unfold f2 in *. + apply match_callstack_incr_bound with m1.(nextblock) tm1.(nextblock). + eapply match_callstack_alloc_rec; eauto. omega. omega. + injection H0; intros; subst m2; simpl; omega. + injection H1; intros; subst tm2; simpl; omega. +Qed. + +(** [match_callstack] implies [match_globalenvs]. *) + +Lemma match_callstack_match_globalenvs: + forall f cs bound tbound m, + match_callstack f cs bound tbound m -> + match_globalenvs f. +Proof. + induction 1; eauto. +Qed. + +(** * Correctness of Cminor construction functions *) + +Hint Resolve eval_negint eval_negfloat eval_absfloat eval_intoffloat + eval_floatofint eval_floatofintu eval_notint eval_notbool + eval_cast8signed eval_cast8unsigned eval_cast16signed + eval_cast16unsigned eval_singleoffloat eval_add eval_add_ptr + eval_add_ptr_2 eval_sub eval_sub_ptr_int eval_sub_ptr_ptr + eval_mul eval_divs eval_mods eval_divu eval_modu + eval_and eval_or eval_xor eval_shl eval_shr eval_shru + eval_addf eval_subf eval_mulf eval_divf + eval_cmp eval_cmp_null_r eval_cmp_null_l eval_cmp_ptr + eval_cmpu eval_cmpf: evalexpr. + +Remark val_inject_val_of_bool: + forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). +Proof. + intros; destruct b; unfold Val.of_bool, Vtrue, Vfalse; constructor. +Qed. + +Ltac TrivialOp := + match goal with + | [ |- exists x, _ /\ val_inject _ (Vint ?x) _ ] => + exists (Vint x); split; + [eauto with evalexpr | constructor] + | [ |- exists x, _ /\ val_inject _ (Vfloat ?x) _ ] => + exists (Vfloat x); split; + [eauto with evalexpr | constructor] + | [ |- exists x, _ /\ val_inject _ (Val.of_bool ?x) _ ] => + exists (Val.of_bool x); split; + [eauto with evalexpr | apply val_inject_val_of_bool] + | _ => idtac + end. + +Remark eval_compare_null_inv: + forall c i v, + Csharpminor.eval_compare_null c i = Some v -> + i = Int.zero /\ (c = Ceq /\ v = Vfalse \/ c = Cne /\ v = Vtrue). +Proof. + intros until v. unfold Csharpminor.eval_compare_null. + predSpec Int.eq Int.eq_spec i Int.zero. + case c; intro EQ; simplify_eq EQ; intro; subst v; tauto. + congruence. +Qed. + +(** Correctness of [make_op]. The generated Cminor code evaluates + to a value that matches the result value of the Csharpminor operation, + provided arguments match pairwise ([val_list_inject f] hypothesis). *) + +Lemma make_op_correct: + forall al a op vl m2 v sp le te1 tm1 t te2 tm2 tvl f, + make_op op al = Some a -> + Csharpminor.eval_operation op vl m2 = Some v -> + eval_exprlist tge (Vptr sp Int.zero) le te1 tm1 al t te2 tm2 tvl -> + val_list_inject f vl tvl -> + mem_inject f m2 tm2 -> + exists tv, + eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 tv + /\ val_inject f v tv. +Proof. + intros. + destruct al as [ | a1 al]; + [idtac | destruct al as [ | a2 al]; + [idtac | destruct al as [ | a3 al]]]; + simpl in H; try discriminate. + (* Constant operators *) + inversion H1. subst sp0 le0 e m te2 tm1 tvl. + inversion H2. subst vl. + destruct op; simplify_eq H; intro; subst a; + simpl in H0; injection H0; intro; subst v. + (* intconst *) + TrivialOp. econstructor. constructor. reflexivity. + (* floatconst *) + TrivialOp. econstructor. constructor. reflexivity. + (* Unary operators *) + inversion H1; clear H1; subst. + inversion H11; clear H11; subst. + rewrite E0_right. + inversion H2; clear H2; subst. inversion H8; clear H8; subst. + destruct op; simplify_eq H; intro; subst a; + simpl in H0; destruct v1; simplify_eq H0; intro; subst v; + inversion H7; subst v0; + TrivialOp. + change (Vint (Int.cast8unsigned i)) with (Val.cast8unsigned (Vint i)). eauto with evalexpr. + change (Vint (Int.cast8signed i)) with (Val.cast8signed (Vint i)). eauto with evalexpr. + change (Vint (Int.cast16unsigned i)) with (Val.cast16unsigned (Vint i)). eauto with evalexpr. + change (Vint (Int.cast16signed i)) with (Val.cast16signed (Vint i)). eauto with evalexpr. + change (Vfloat (Float.singleoffloat f0)) with (Val.singleoffloat (Vfloat f0)). eauto with evalexpr. + (* Binary operations *) + inversion H1; clear H1; subst. inversion H11; clear H11; subst. + inversion H12; clear H12; subst. rewrite E0_right. + inversion H2; clear H2; subst. inversion H9; clear H9; subst. + inversion H10; clear H10; subst. + destruct op; simplify_eq H; intro; subst a; + simpl in H0; destruct v2; destruct v3; simplify_eq H0; intro; try subst v; + inversion H7; inversion H8; subst v0; subst v1; + TrivialOp. + (* add int ptr *) + exists (Vptr b2 (Int.add ofs2 i)); split. + eauto with evalexpr. apply val_inject_ptr with x. auto. + subst ofs2. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + (* add ptr int *) + exists (Vptr b2 (Int.add ofs2 i0)); split. + eauto with evalexpr. apply val_inject_ptr with x. auto. + subst ofs2. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + (* sub ptr int *) + exists (Vptr b2 (Int.sub ofs2 i0)); split. + eauto with evalexpr. apply val_inject_ptr with x. auto. + subst ofs2. apply Int.sub_add_l. + (* sub ptr ptr *) + destruct (eq_block b b0); simplify_eq H0; intro; subst v; subst b0. + assert (b4 = b2). congruence. subst b4. + exists (Vint (Int.sub ofs3 ofs2)); split. + eauto with evalexpr. + subst ofs2 ofs3. replace x0 with x. rewrite Int.sub_shifted. constructor. + congruence. + (* divs *) + generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro; + simplify_eq H0; intro; subst v. TrivialOp. + (* divu *) + generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro; + simplify_eq H0; intro; subst v. TrivialOp. + (* mods *) + generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro; + simplify_eq H0; intro; subst v. TrivialOp. + (* modu *) + generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro; + simplify_eq H0; intro; subst v. TrivialOp. + (* shl *) + caseEq (Int.ltu i0 (Int.repr 32)); intro EQ; rewrite EQ in H0; + simplify_eq H0; intro; subst v. TrivialOp. + (* shr *) + caseEq (Int.ltu i0 (Int.repr 32)); intro EQ; rewrite EQ in H0; + simplify_eq H0; intro; subst v. TrivialOp. + (* shru *) + caseEq (Int.ltu i0 (Int.repr 32)); intro EQ; rewrite EQ in H0; + simplify_eq H0; intro; subst v. TrivialOp. + (* cmp int ptr *) + elim (eval_compare_null_inv _ _ _ H0); intros; subst i1 i. + exists v; split. eauto with evalexpr. + elim H12; intros [A B]; subst v; unfold Vtrue, Vfalse; constructor. + (* cmp ptr int *) + elim (eval_compare_null_inv _ _ _ H0); intros; subst i1 i0. + exists v; split. eauto with evalexpr. + elim H12; intros [A B]; subst v; unfold Vtrue, Vfalse; constructor. + (* cmp ptr ptr *) + caseEq (valid_pointer m2 b (Int.signed i) && valid_pointer m2 b0 (Int.signed i0)); + intro EQ; rewrite EQ in H0; try discriminate. + destruct (eq_block b b0); simplify_eq H0; intro; subst v b0. + assert (b4 = b2); [congruence|subst b4]. + assert (x0 = x); [congruence|subst x0]. + elim (andb_prop _ _ EQ); intros. + exists (Val.of_bool (Int.cmp c ofs3 ofs2)); split. + eauto with evalexpr. + subst ofs2 ofs3. rewrite Int.translate_cmp. + apply val_inject_val_of_bool. + eapply valid_pointer_inject_no_overflow; eauto. + eapply valid_pointer_inject_no_overflow; eauto. +Qed. + +(** Correctness of [make_cast]. Note that the resulting Cminor value is + normalized according to the given memory chunk. *) + +Lemma make_cast_correct: + forall f sp le te1 tm1 a t te2 tm2 v chunk tv, + eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 tv -> + val_inject f v tv -> + exists tv', + eval_expr tge (Vptr sp Int.zero) le + te1 tm1 (make_cast chunk a) + t te2 tm2 tv' + /\ val_inject f (Val.load_result chunk v) tv'. +Proof. + intros. destruct chunk. + + exists (Val.cast8signed tv). + split. apply eval_cast8signed; auto. + inversion H0; simpl; constructor. + + exists (Val.cast8unsigned tv). + split. apply eval_cast8unsigned; auto. + inversion H0; simpl; constructor. + + exists (Val.cast16signed tv). + split. apply eval_cast16signed; auto. + inversion H0; simpl; constructor. + + exists (Val.cast16unsigned tv). + split. apply eval_cast16unsigned; auto. + inversion H0; simpl; constructor. + + exists tv. + split. simpl; auto. + inversion H0; simpl; econstructor; eauto. + + exists (Val.singleoffloat tv). + split. apply eval_singleoffloat; auto. + inversion H0; simpl; constructor. + + exists tv. + split. simpl; auto. + inversion H0; simpl; constructor. +Qed. + +Lemma make_stackaddr_correct: + forall sp le te tm ofs, + eval_expr tge (Vptr sp Int.zero) le + te tm (make_stackaddr ofs) + E0 te tm (Vptr sp (Int.repr ofs)). +Proof. + intros; unfold make_stackaddr. + eapply eval_Eop. econstructor. simpl. decEq. decEq. + rewrite Int.add_commut. apply Int.add_zero. +Qed. + +Lemma make_globaladdr_correct: + forall sp le te tm id b, + Genv.find_symbol tge id = Some b -> + eval_expr tge (Vptr sp Int.zero) le + te tm (make_globaladdr id) + E0 te tm (Vptr b Int.zero). +Proof. + intros; unfold make_globaladdr. + eapply eval_Eop. econstructor. simpl. rewrite H. auto. +Qed. + +(** Correctness of [make_load] and [make_store]. *) + +Lemma make_load_correct: + forall sp le te1 tm1 a t te2 tm2 va chunk v, + eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 va -> + Mem.loadv chunk tm2 va = Some v -> + eval_expr tge (Vptr sp Int.zero) le + te1 tm1 (make_load chunk a) + t te2 tm2 v. +Proof. + intros; unfold make_load. + eapply eval_load; eauto. +Qed. + +Lemma store_arg_content_inject: + forall f sp le te1 tm1 a t te2 tm2 v va chunk, + eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 va -> + val_inject f v va -> + exists vb, + eval_expr tge (Vptr sp Int.zero) le te1 tm1 (store_arg chunk a) t te2 tm2 vb + /\ val_content_inject f (mem_chunk chunk) v vb. +Proof. + intros. + assert (exists vb, + eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 vb + /\ val_content_inject f (mem_chunk chunk) v vb). + exists va; split. assumption. constructor. assumption. + inversion H; clear H; subst; simpl; trivial. + inversion H2; clear H2; subst; trivial. + inversion H4; clear H4; subst; trivial. + rewrite E0_right. rewrite E0_right in H1. + destruct op; trivial; destruct chunk; trivial; + exists v0; (split; [auto| + simpl in H3; inversion H3; clear H3; subst va; + destruct v0; simpl in H0; inversion H0; subst; try (constructor; constructor)]). + apply val_content_inject_8. apply Int.cast8_unsigned_signed. + apply val_content_inject_8. apply Int.cast8_unsigned_idem. + apply val_content_inject_16. apply Int.cast16_unsigned_signed. + apply val_content_inject_16. apply Int.cast16_unsigned_idem. + apply val_content_inject_32. apply Float.singleoffloat_idem. +Qed. + +Lemma make_store_correct: + forall f sp te1 tm1 addr te2 tm2 tvaddr rhs te3 tm3 tvrhs + chunk vrhs m3 vaddr m4 t1 t2, + eval_expr tge (Vptr sp Int.zero) nil + te1 tm1 addr t1 te2 tm2 tvaddr -> + eval_expr tge (Vptr sp Int.zero) nil + te2 tm2 rhs t2 te3 tm3 tvrhs -> + Mem.storev chunk m3 vaddr vrhs = Some m4 -> + mem_inject f m3 tm3 -> + val_inject f vaddr tvaddr -> + val_inject f vrhs tvrhs -> + exists tm4, + exec_stmt tge (Vptr sp Int.zero) + te1 tm1 (make_store chunk addr rhs) + (t1**t2) te3 tm4 Out_normal + /\ mem_inject f m4 tm4 + /\ nextblock tm4 = nextblock tm3. +Proof. + intros. unfold make_store. + exploit store_arg_content_inject. eexact H0. eauto. + intros [tv [EVAL VCINJ]]. + exploit storev_mapped_inject_1; eauto. + intros [tm4 [STORE MEMINJ]]. + exploit eval_store. eexact H. eexact EVAL. eauto. + intro EVALSTORE. + exists tm4. + split. apply exec_Sexpr with tv. auto. + split. auto. + unfold storev in STORE; destruct tvaddr; try discriminate. + exploit store_inv; eauto. simpl. tauto. +Qed. + +(** Correctness of the variable accessors [var_get], [var_set] + and [var_addr]. *) + +Lemma var_get_correct: + forall cenv id a f e te sp lo hi m cs tm b chunk v le, + var_get cenv id = Some 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 -> + load chunk m b 0 = Some v -> + exists tv, + eval_expr tge (Vptr sp Int.zero) le te tm a E0 te tm tv /\ + val_inject f v tv. +Proof. + unfold var_get; intros. + assert (match_var f id e m te sp cenv!!id). + inversion H0. inversion H17. auto. + inversion H4; subst; rewrite <- H5 in H; inversion H; subst. + (* var_local *) + inversion H2; [subst|congruence]. + exists v'; split. + apply eval_Evar. auto. + replace v with v0. auto. congruence. + (* var_stack_scalar *) + inversion H2; [subst|congruence]. + assert (b0 = b). congruence. subst b0. + assert (chunk0 = chunk). congruence. subst chunk0. + exploit loadv_inject; eauto. + unfold loadv. eexact H3. + intros [tv [LOAD INJ]]. + exists tv; split. + eapply make_load_correct; eauto. eapply make_stackaddr_correct; eauto. + auto. + (* var_global_scalar *) + inversion H2; [congruence|subst]. + 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. + assert (loadv chunk m (Vptr b Int.zero) = Some v). assumption. + assert (val_inject f (Vptr b Int.zero) (Vptr b Int.zero)). + econstructor; eauto. + generalize (loadv_inject _ _ _ _ _ _ _ H1 H12 H13). + intros [tv [LOAD INJ]]. + exists tv; split. + eapply make_load_correct; eauto. eapply make_globaladdr_correct; eauto. + auto. +Qed. + +Lemma var_addr_correct: + forall cenv id a f e te sp lo hi m cs tm b le, + match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> + var_addr cenv id = Some a -> + eval_var_addr prog e id b -> + exists tv, + eval_expr tge (Vptr sp Int.zero) le te tm a E0 te tm tv /\ + val_inject f (Vptr b Int.zero) tv. +Proof. + unfold var_addr; intros. + assert (match_var f id e m te sp cenv!!id). + inversion H. inversion H15. auto. + inversion H2; subst; rewrite <- H3 in H0; inversion H0; subst; clear H0. + (* var_stack_scalar *) + inversion H1; [subst|congruence]. + exists (Vptr sp (Int.repr ofs)); split. + eapply make_stackaddr_correct. + replace b with b0. auto. congruence. + (* var_stack_array *) + inversion H1; [subst|congruence]. + exists (Vptr sp (Int.repr ofs)); split. + eapply make_stackaddr_correct. + replace b with b0. auto. congruence. + (* var_global_scalar *) + inversion H1; [congruence|subst]. + assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. + inversion H7. destruct (mg_symbols0 _ _ H6) as [A B]. + exists (Vptr b Int.zero); split. + eapply make_globaladdr_correct. eauto. + econstructor; eauto. + (* var_global_array *) + inversion H1; [congruence|subst]. + assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. + inversion H6. destruct (mg_symbols0 _ _ H5) as [A B]. + exists (Vptr b Int.zero); split. + eapply make_globaladdr_correct. eauto. + econstructor; eauto. +Qed. + +Lemma var_set_correct: + forall cenv id rhs a f e te2 sp lo hi m2 cs tm2 te1 tm1 tv b chunk v m3 t, + var_set cenv id rhs = Some a -> + match_callstack f (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2 -> + eval_expr tge (Vptr sp Int.zero) nil te1 tm1 rhs t te2 tm2 tv -> + val_inject f v tv -> + mem_inject f m2 tm2 -> + eval_var_ref prog e id b chunk -> + store chunk m2 b 0 v = Some m3 -> + exists te3, exists tm3, + exec_stmt tge (Vptr sp Int.zero) te1 tm1 a t te3 tm3 Out_normal /\ + mem_inject f m3 tm3 /\ + match_callstack f (mkframe cenv e te3 sp lo hi :: cs) m3.(nextblock) tm3.(nextblock) m3. +Proof. + unfold var_set; intros. + assert (NEXTBLOCK: nextblock m3 = nextblock m2). + exploit store_inv; eauto. simpl; tauto. + inversion H0. subst f0 cenv0 e0 te sp0 lo0 hi0 cs0 bound tbound m. + assert (match_var f id e m2 te2 sp cenv!!id). inversion H19; auto. + inversion H6; subst; rewrite <- H7 in H; inversion H; subst; clear H. + (* var_local *) + inversion H4; [subst|congruence]. + assert (b0 = b). congruence. subst b0. + assert (chunk0 = chunk). congruence. subst chunk0. + exploit make_cast_correct; eauto. + intros [tv' [EVAL INJ]]. + exists (PTree.set id tv' te2); exists tm2. + split. eapply exec_Sexpr. eapply eval_Eassign. eauto. + split. eapply store_unmapped_inject; eauto. + rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto. + (* var_stack_scalar *) + inversion H4; [subst|congruence]. + assert (b0 = b). congruence. subst b0. + assert (chunk0 = chunk). congruence. subst chunk0. + assert (storev chunk m2 (Vptr b Int.zero) v = Some m3). assumption. + exploit make_store_correct. + eapply make_stackaddr_correct. + eauto. eauto. eauto. eauto. eauto. + rewrite E0_left. intros [tm3 [EVAL [MEMINJ TNEXTBLOCK]]]. + exists te2; exists tm3. + split. auto. split. auto. + rewrite NEXTBLOCK; rewrite TNEXTBLOCK. + eapply match_callstack_mapped; eauto. + inversion H9; congruence. + (* var_global_scalar *) + inversion H4; [congruence|subst]. + assert (chunk0 = chunk). congruence. subst chunk0. + assert (storev chunk m2 (Vptr b Int.zero) v = Some m3). assumption. + assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. + inversion H13. destruct (mg_symbols0 _ _ H10) as [A B]. + exploit make_store_correct. + eapply make_globaladdr_correct; eauto. + eauto. eauto. eauto. eauto. eauto. + rewrite E0_left. intros [tm3 [EVAL [MEMINJ TNEXTBLOCK]]]. + exists te2; exists tm3. + split. auto. split. auto. + rewrite NEXTBLOCK; rewrite TNEXTBLOCK. + eapply match_callstack_mapped; eauto. congruence. +Qed. + +(** * Correctness of stack allocation of local variables *) + +(** This section shows the correctness of the translation of Csharpminor + local variables, either as Cminor local variables or as sub-blocks + of the Cminor stack data. This is the most difficult part of the proof. *) + +Remark assign_variables_incr: + forall atk vars cenv sz cenv' sz', + assign_variables atk vars (cenv, sz) = (cenv', sz') -> sz <= sz'. +Proof. + induction vars; intros until sz'; simpl. + intro. replace sz' with sz. omega. congruence. + destruct a. destruct v. case (Identset.mem i atk); intros. + generalize (IHvars _ _ _ _ H). + generalize (size_chunk_pos m). intro. + generalize (align_le sz (size_chunk m) H0). omega. + eauto. + intro. generalize (IHvars _ _ _ _ H). + assert (8 > 0). omega. generalize (align_le sz 8 H0). + assert (0 <= Zmax 0 z). apply Zmax_bound_l. omega. + omega. +Qed. + +Lemma match_callstack_alloc_variables_rec: + forall tm sp cenv' sz' te lo cs atk, + valid_block tm sp -> + 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 f cenv sz, + assign_variables atk vars (cenv, sz) = (cenv', sz') -> + match_callstack f (mkframe cenv e te sp lo m.(nextblock) :: cs) + m.(nextblock) tm.(nextblock) m -> + mem_inject f m tm -> + 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) -> + exists f', + inject_incr f f' + /\ mem_inject f' m' tm + /\ match_callstack f' (mkframe cenv' e' te sp lo m'.(nextblock) :: cs) + m'.(nextblock) tm.(nextblock) m'. +Proof. + intros until atk. intros VB LB HB NOOV. + induction 1. + (* base case *) + intros. simpl in H. inversion H; subst cenv sz. + exists f. split. apply inject_incr_refl. split. auto. auto. + (* inductive case *) + intros until sz. + 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. + 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. + generalize ASV1. unfold assign_variable. + caseEq lv. + (* 1. lv = LVscalar chunk *) + intros chunk LV. case (Identset.mem id atk). + (* 1.1 info = Var_stack_scalar chunk ... *) + set (ofs := align sz (size_chunk chunk)). + intro EQ; injection EQ; intros; clear EQ. + set (f1 := extend_inject b1 (Some (sp, ofs)) f). + generalize (size_chunk_pos chunk); intro SIZEPOS. + generalize (align_le sz (size_chunk chunk) SIZEPOS). fold ofs. intro SZOFS. + assert (mem_inject f1 m1 tm /\ inject_incr f f1). + assert (Int.min_signed < 0). compute; auto. + generalize (assign_variables_incr _ _ _ _ _ _ ASVS). intro. + unfold f1; eapply alloc_mapped_inject; eauto. + omega. omega. omega. omega. unfold sizeof; rewrite LV. omega. + 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. + rewrite <- H1. omega. + intros until delta; unfold f1, extend_inject, eq_block. + rewrite (high_bound_alloc _ _ b _ _ _ H). + case (zeq b b1); intros. + inversion H3. unfold sizeof; rewrite LV. omega. + generalize (BOUND _ _ H3). omega. + intros [f' [INCR2 [MINJ2 MATCH2]]]. + exists f'; intuition. eapply inject_incr_trans; eauto. + (* 1.2 info = Var_local chunk *) + intro EQ; injection EQ; intros; clear EQ. subst sz1. + 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. + intros until delta; unfold f1, extend_inject, eq_block. + rewrite (high_bound_alloc _ _ b _ _ _ H). + case (zeq b b1); intros. discriminate. + eapply BOUND; eauto. + intros [f' [INCR2 [MINJ2 MATCH2]]]. + exists f'; intuition. eapply inject_incr_trans; eauto. + (* 2. lv = LVarray dim, info = Var_stack_array *) + intros dim LV EQ. injection EQ; clear EQ; intros. + assert (0 <= Zmax 0 dim). apply Zmax1. + assert (8 > 0). omega. + generalize (align_le sz 8 H4). intro. + set (ofs := align sz 8) in *. + set (f1 := extend_inject b1 (Some (sp, ofs)) f). + assert (mem_inject f1 m1 tm /\ inject_incr f f1). + assert (Int.min_signed < 0). compute; auto. + generalize (assign_variables_incr _ _ _ _ _ _ ASVS). intro. + unfold f1; eapply alloc_mapped_inject; eauto. + omega. omega. omega. omega. unfold sizeof; rewrite LV. omega. + intros. left. generalize (BOUND _ _ H8). omega. + destruct H6 as [MINJ1 INCR1]. + exploit IHalloc_variables; eauto. + unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. + rewrite <- H1. omega. + intros until delta; unfold f1, extend_inject, eq_block. + rewrite (high_bound_alloc _ _ b _ _ _ H). + case (zeq b b1); intros. + inversion H6. unfold sizeof; rewrite LV. omega. + generalize (BOUND _ _ H6). omega. + intros [f' [INCR2 [MINJ2 MATCH2]]]. + exists f'; intuition. eapply inject_incr_trans; eauto. +Qed. + +Lemma set_params_defined: + forall params args id, + In id params -> (set_params args params)!id <> None. +Proof. + induction params; simpl; intros. + elim H. + destruct args. + rewrite PTree.gsspec. case (peq id a); intro. + congruence. eapply IHparams. elim H; intro. congruence. auto. + rewrite PTree.gsspec. case (peq id a); intro. + congruence. eapply IHparams. elim H; intro. congruence. auto. +Qed. + +Lemma set_locals_defined: + forall e vars id, + In id vars \/ e!id <> None -> (set_locals vars e)!id <> None. +Proof. + induction vars; simpl; intros. + tauto. + rewrite PTree.gsspec. case (peq id a); intro. + congruence. + apply IHvars. assert (a <> id). congruence. tauto. +Qed. + +Lemma set_locals_params_defined: + forall args params vars id, + In id (params ++ vars) -> + (set_locals vars (set_params args params))!id <> None. +Proof. + intros. apply set_locals_defined. + elim (in_app_or _ _ _ H); intro. + right. apply set_params_defined; auto. + left; auto. +Qed. + +(** Preservation of [match_callstack] by simultaneous allocation + 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, + build_compilenv gce fn = (cenv, sz) -> + sz <= Int.max_signed -> + alloc_variables Csharpminor.empty_env m (fn_variables fn) e m' lb -> + Mem.alloc tm 0 sz = (tm', sp) -> + match_callstack f cs m.(nextblock) tm.(nextblock) m -> + mem_inject f m tm -> + let tparams := List.map (@fst ident memory_chunk) fn.(Csharpminor.fn_params) in + let tvars := List.map (@fst ident var_kind) fn.(Csharpminor.fn_vars) in + let te := set_locals tvars (set_params targs tparams) in + exists f', + inject_incr f f' + /\ mem_inject f' m' tm' + /\ match_callstack f' (mkframe cenv e te sp m.(nextblock) m'.(nextblock) :: cs) + m'.(nextblock) tm'.(nextblock) m'. +Proof. + intros. + assert (SP: sp = nextblock tm). injection H2; auto. + unfold build_compilenv in H. + eapply match_callstack_alloc_variables_rec with (sz' := sz); eauto. + eapply valid_new_block; eauto. + rewrite (low_bound_alloc _ _ sp _ _ _ H2). apply zeq_true. + rewrite (high_bound_alloc _ _ sp _ _ _ H2). apply zeq_true. + (* match_callstack *) + constructor. omega. change (valid_block tm' sp). eapply valid_new_block; eauto. + constructor. + (* me_vars *) + intros. generalize (global_compilenv_charact id). + destruct (gce!!id); intro; try contradiction. + constructor. + unfold Csharpminor.empty_env. apply PTree.gempty. auto. + constructor. + unfold Csharpminor.empty_env. apply PTree.gempty. + (* me_low_high *) + omega. + (* me_bounded *) + intros until lv. unfold Csharpminor.empty_env. rewrite PTree.gempty. congruence. + (* me_inj *) + intros until lv2. unfold Csharpminor.empty_env; rewrite PTree.gempty; congruence. + (* me_inv *) + intros. exploit mi_mappedblocks; eauto. intros [A B]. + elim (fresh_block_alloc _ _ _ _ _ H2 A). + (* me_incr *) + intros. exploit mi_mappedblocks; eauto. intros [A B]. + rewrite SP; auto. + rewrite SP; auto. + eapply alloc_right_inject; eauto. + omega. + intros. exploit mi_mappedblocks; eauto. intros [A B]. + unfold block in SP; omegaContradiction. + (* defined *) + intros. unfold te. apply set_locals_params_defined. + 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]. + 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. +Qed. + +(** Correctness of the code generated by [store_parameters] + to store in memory the values of parameters that are stack-allocated. *) + +Inductive vars_vals_match: + meminj -> list (ident * memory_chunk) -> list val -> env -> Prop := + | vars_vals_nil: + forall f te, + vars_vals_match f nil nil te + | vars_vals_cons: + forall f te id chunk vars v vals tv, + te!id = Some tv -> + val_inject f v tv -> + vars_vals_match f vars vals te -> + vars_vals_match f ((id, chunk) :: vars) (v :: vals) te. + +Lemma vars_vals_match_extensional: + forall f vars vals te, + vars_vals_match f vars vals te -> + forall te', + (forall id lv, In (id, lv) vars -> te'!id = te!id) -> + vars_vals_match f vars vals te'. +Proof. + induction 1; intros. + constructor. + econstructor; eauto. rewrite <- H. eapply H2. left. reflexivity. + apply IHvars_vals_match. intros. eapply H2; eauto. right. eauto. +Qed. + +Lemma store_parameters_correct: + forall e m1 params vl m2, + bind_parameters e m1 params vl m2 -> + forall f te1 cenv sp lo hi cs tm1, + 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 -> + exists te2, exists tm2, + exec_stmt tge (Vptr sp Int.zero) + te1 tm1 (store_parameters cenv params) + E0 te2 tm2 Out_normal + /\ mem_inject f m2 tm2 + /\ match_callstack f (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2. +Proof. + induction 1. + (* base case *) + intros; simpl. exists te1; exists tm1. split. constructor. tauto. + (* inductive case *) + intros until tm1. intros VVM NOREPET MINJ MATCH. simpl. + inversion VVM. subst f0 id0 chunk0 vars v vals te. + inversion MATCH. subst f0 cenv0 e0 te sp0 lo0 hi0 cs0 bound tbound m0. + inversion H18. + inversion NOREPET. subst hd tl. + assert (NEXT: nextblock m1 = nextblock m). + exploit store_inv; eauto. simpl; tauto. + generalize (me_vars0 id). intro. inversion H2; subst. + (* cenv!!id = Var_local chunk *) + assert (b0 = b). congruence. subst b0. + assert (chunk0 = chunk). congruence. subst chunk0. + assert (v' = tv). congruence. subst v'. + exploit make_cast_correct. + apply eval_Evar with (id := id). eauto. + eexact H10. + intros [tv' [EVAL1 VINJ1]]. + set (te2 := PTree.set id tv' te1). + assert (VVM2: vars_vals_match f params vl te2). + apply vars_vals_match_extensional with te1; auto. + intros. unfold te2; apply PTree.gso. red; intro; subst id0. + elim H4. change id with (fst (id, lv)). apply List.in_map; auto. + exploit store_unmapped_inject; eauto. intro MINJ2. + exploit match_callstack_store_local; eauto. + fold te2; rewrite <- NEXT; intro MATCH2. + exploit IHbind_parameters; eauto. + intros [te3 [tm3 [EXEC3 [MINJ3 MATCH3]]]]. + exists te3; exists tm3. + (* execution *) + split. apply exec_Sseq_continue with E0 te2 tm1 E0. + econstructor. unfold te2. constructor. eassumption. + assumption. traceEq. + (* meminj & match_callstack *) + tauto. + + (* cenv!!id = Var_stack_scalar *) + assert (b0 = b). congruence. subst b0. + assert (chunk0 = chunk). congruence. subst chunk0. + exploit make_store_correct. + eapply make_stackaddr_correct. + apply eval_Evar with (id := id). + eauto. 2:eauto. 2:eauto. unfold storev; eexact H0. eauto. + intros [tm2 [EVAL3 [MINJ2 NEXT1]]]. + exploit match_callstack_mapped. + eexact MATCH. 2:eauto. inversion H7. congruence. + rewrite <- NEXT; rewrite <- NEXT1; intro MATCH2. + exploit IHbind_parameters; eauto. + intros [te3 [tm3 [EVAL4 [MINJ3 MATCH3]]]]. + exists te3; exists tm3. + (* execution *) + split. apply exec_Sseq_continue with (E0**E0) te1 tm2 E0. + auto. assumption. traceEq. + (* meminj & match_callstack *) + tauto. + + (* Impossible cases on cenv!!id *) + congruence. + congruence. + congruence. +Qed. + +Lemma vars_vals_match_holds_1: + forall f params args targs, + list_norepet (List.map (@fst ident memory_chunk) params) -> + List.length params = List.length args -> + val_list_inject f args targs -> + vars_vals_match f params args + (set_params targs (List.map (@fst ident memory_chunk) params)). +Proof. + induction params; destruct args; simpl; intros; try discriminate. + constructor. + inversion H1. subst v0 vl targs. + inversion H. subst hd tl. + destruct a as [id chunk]. econstructor. + simpl. rewrite PTree.gss. reflexivity. + auto. + apply vars_vals_match_extensional + with (set_params vl' (map (@fst ident memory_chunk) params)). + eapply IHparams; eauto. + intros. simpl. apply PTree.gso. red; intro; subst id0. + elim H5. change (fst (id, chunk)) with (fst (id, lv)). + apply List.in_map; auto. +Qed. + +Lemma vars_vals_match_holds: + forall f params args targs, + List.length params = List.length args -> + val_list_inject f args targs -> + forall vars, + list_norepet (List.map (@fst ident var_kind) vars + ++ List.map (@fst ident memory_chunk) params) -> + vars_vals_match f params args + (set_locals (List.map (@fst ident var_kind) vars) + (set_params targs (List.map (@fst ident memory_chunk) params))). +Proof. + induction vars; simpl; intros. + eapply vars_vals_match_holds_1; eauto. + inversion H1. subst hd tl. + eapply vars_vals_match_extensional; eauto. + intros. apply PTree.gso. red; intro; subst id; elim H4. + apply in_or_app. right. change (fst a) with (fst (fst a, lv)). + apply List.in_map; auto. +Qed. + +Lemma bind_parameters_length: + forall e m1 params args m2, + bind_parameters e m1 params args m2 -> + List.length params = List.length args. +Proof. + induction 1; simpl; eauto. +Qed. + +(** The final result in this section: the behaviour of function entry + in the generated Cminor code (allocate stack data block and store + parameters whose address is taken) simulates what happens at function + entry in the original Csharpminor (allocate one block per local variable + 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, + alloc_variables empty_env m (fn_variables fn) e m1 lb -> + 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) -> + sz <= Int.max_signed -> + Mem.alloc tm 0 sz = (tm1, sp) -> + let te := + set_locals (fn_vars_names fn) (set_params tvargs (fn_params_names fn)) in + val_list_inject f vargs tvargs -> + mem_inject f m tm -> + list_norepet (fn_params_names fn ++ fn_vars_names fn) -> + exists f2, exists te2, exists tm2, + exec_stmt tge (Vptr sp Int.zero) + te tm1 (store_parameters cenv fn.(Csharpminor.fn_params)) + E0 te2 tm2 Out_normal + /\ 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). +Proof. + intros. + exploit bind_parameters_length; eauto. intro LEN1. + exploit match_callstack_alloc_variables; eauto. + intros [f1 [INCR1 [MINJ1 MATCH1]]]. + exploit vars_vals_match_holds. + eauto. apply val_list_inject_incr with f. eauto. eauto. + apply list_norepet_append_commut. + unfold fn_vars_names in H7. eexact H7. + intro VVM. + exploit store_parameters_correct. + eauto. eauto. + unfold fn_params_names in H7. eapply list_norepet_append_left; eauto. + eexact MINJ1. 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. +Qed. + +(** * Semantic preservation for the translation *) + +(** These tactics simplify hypotheses of the form [f ... = Some x]. *) + +Ltac monadSimpl1 := + match goal with + | [ |- (bind _ _ ?F ?G = Some ?X) -> _ ] => + unfold bind at 1; + generalize (refl_equal F); + pattern F at -1 in |- *; + case F; + [ (let EQ := fresh "EQ" in + (intro; intro EQ; + try monadSimpl1)) + | intros; discriminate ] + | [ |- (None = Some _) -> _ ] => + intro; discriminate + | [ |- (Some _ = Some _) -> _ ] => + let h := fresh "H" in + (intro h; injection h; intro; clear h) + end. + +Ltac monadSimpl := + match goal with + | [ |- (bind _ _ ?F ?G = Some ?X) -> _ ] => monadSimpl1 + | [ |- (None = Some _) -> _ ] => monadSimpl1 + | [ |- (Some _ = Some _) -> _ ] => monadSimpl1 + | [ |- (?F _ _ _ _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 + | [ |- (?F _ _ _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 + | [ |- (?F _ _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 + | [ |- (?F _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 + | [ |- (?F _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 + | [ |- (?F _ _ = Some _) -> _ ] => simpl F; monadSimpl1 + | [ |- (?F _ = Some _) -> _ ] => simpl F; monadSimpl1 + end. + +Ltac monadInv H := + generalize H; monadSimpl. + +(** The proof of semantic preservation uses simulation diagrams of the + following form: +<< + le, e, m1, a --------------- tle, sp, te1, tm1, ta + | | + | | + v v + le, e, m2, v --------------- tle, sp, te2, tm2, tv +>> + where [ta] is the Cminor expression obtained by translating the + Csharpminor expression [a]. The left vertical arrow is an evaluation + of a Csharpminor expression. The right vertical arrow is an evaluation + of a Cminor expression. The precondition (top vertical bar) + includes a [mem_inject] relation between the memory states [m1] and [tm1], + a [val_list_inject] relation between the let environments [le] and [tle], + and a [match_callstack] relation for any callstack having + [e], [te1], [sp] as top frame. The postcondition (bottom vertical bar) + is the existence of a memory injection [f2] that extends the injection + [f1] we started with, preserves the [match_callstack] relation for + the transformed callstack at the final state, and validates a + [val_inject] relation between the result values [v] and [tv]. + + We capture these diagrams by the following predicates, parameterized + over the Csharpminor executions, which will serve as induction + hypotheses in the proof of simulation. *) + +Definition eval_expr_prop + (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (a: Csharpminor.expr) (t: trace) (m2: mem) (v: val) : Prop := + forall cenv ta f1 tle te1 tm1 sp lo hi cs + (TR: transl_expr cenv a = Some ta) + (LINJ: val_list_inject f1 le tle) + (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 tv, + eval_expr tge (Vptr sp Int.zero) tle te1 tm1 ta t te2 tm2 tv + /\ val_inject f2 v tv + /\ 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. + +Definition eval_exprlist_prop + (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (al: Csharpminor.exprlist) (t: trace) (m2: mem) (vl: list val) : Prop := + forall cenv tal f1 tle te1 tm1 sp lo hi cs + (TR: transl_exprlist cenv al = Some tal) + (LINJ: val_list_inject f1 le tle) + (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 tvl, + eval_exprlist tge (Vptr sp Int.zero) tle te1 tm1 tal t te2 tm2 tvl + /\ val_list_inject f2 vl tvl + /\ 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. + +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 = Some 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 = Some 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. + +(** 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_expr_Evar_correct: + forall (le : Csharpminor.letenv) + (e : Csharpminor.env) (m : mem) (id : positive) + (b : block) (chunk : memory_chunk) (v : val), + eval_var_ref prog e id b chunk -> + load chunk m b 0 = Some v -> + eval_expr_prop le e m (Csharpminor.Evar id) E0 m v. +Proof. + intros; red; intros. unfold transl_expr in TR. + exploit var_get_correct; eauto. + intros [tv [EVAL VINJ]]. + exists f1; exists te1; exists tm1; exists tv; intuition eauto. +Qed. + +Lemma transl_expr_Eaddrof_correct: + forall (le : Csharpminor.letenv) + (e : Csharpminor.env) (m : mem) (id : positive) + (b : block), + eval_var_addr prog e id b -> + eval_expr_prop le e m (Eaddrof id) E0 m (Vptr b Int.zero). +Proof. + intros; red; intros. simpl in TR. + exploit var_addr_correct; eauto. + intros [tv [EVAL VINJ]]. + exists f1; exists te1; exists tm1; exists tv. intuition eauto. +Qed. + +Lemma transl_expr_Eop_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (op : Csharpminor.operation) (al : Csharpminor.exprlist) + (t: trace) (m1 : mem) (vl : list val) (v : val), + Csharpminor.eval_exprlist prog le e m al t m1 vl -> + eval_exprlist_prop le e m al t m1 vl -> + Csharpminor.eval_operation op vl m1 = Some v -> + eval_expr_prop le e m (Csharpminor.Eop op al) t m1 v. +Proof. + intros; red; intros. monadInv TR; intro EQ0. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. + exploit make_op_correct; eauto. + intros [tv [EVAL2 VINJ2]]. + exists f2; exists te2; exists tm2; exists tv. intuition. +Qed. + +Lemma transl_expr_Eload_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (chunk : memory_chunk) (a : Csharpminor.expr) (t: trace) (m1 : mem) + (v1 v : val), + Csharpminor.eval_expr prog le e m a t m1 v1 -> + eval_expr_prop le e m a t m1 v1 -> + loadv chunk m1 v1 = Some v -> + eval_expr_prop le e m (Csharpminor.Eload chunk a) t m1 v. +Proof. + intros; red; intros. + monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]]. + exploit loadv_inject; eauto. + intros [tv [TLOAD VINJ]]. + exists f2; exists te2; exists tm2; exists tv. + intuition. + subst ta. eapply make_load_correct; eauto. +Qed. + +Lemma transl_expr_Ecall_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (sig : signature) (a : Csharpminor.expr) (bl : Csharpminor.exprlist) + (t1: trace) (m1: mem) (t2: trace) (m2: mem) (t3: trace) (m3: mem) + (vf : val) (vargs : list val) (vres : val) + (f : Csharpminor.fundef) (t: trace), + Csharpminor.eval_expr prog le e m a t1 m1 vf -> + eval_expr_prop le e m a t1 m1 vf -> + Csharpminor.eval_exprlist prog le e m1 bl t2 m2 vargs -> + eval_exprlist_prop le e m1 bl t2 m2 vargs -> + Genv.find_funct ge vf = Some f -> + Csharpminor.funsig f = sig -> + Csharpminor.eval_funcall prog m2 f vargs t3 m3 vres -> + eval_funcall_prop m2 f vargs t3 m3 vres -> + t = t1 ** t2 ** t3 -> + eval_expr_prop le e m (Csharpminor.Ecall sig a bl) t m3 vres. +Proof. + intros;red;intros. monadInv TR. subst ta. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. + exploit H2. + eauto. eapply val_list_inject_incr; eauto. eauto. eauto. + intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]]. + assert (tv1 = vf). + elim (Genv.find_funct_inv H3). intros bf VF. rewrite VF in H3. + rewrite Genv.find_funct_find_funct_ptr in H3. + generalize (Genv.find_funct_ptr_inv H3). intro. + assert (match_globalenvs f2). eapply match_callstack_match_globalenvs; eauto. + generalize (mg_functions _ H9 _ H8). intro. + rewrite VF in VINJ1. inversion VINJ1. subst vf. + decEq. congruence. + subst ofs2. replace x with 0. reflexivity. congruence. + subst tv1. elim (functions_translated _ _ H3). intros tf [FIND TRF]. + exploit H6; eauto. + intros [f4 [tm4 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]]. + exists f4; exists te3; exists tm4; exists tres. intuition. + eapply eval_Ecall; eauto. + rewrite <- H4. apply sig_preserved; auto. + apply inject_incr_trans with f2; auto. + apply inject_incr_trans with f3; auto. +Qed. + +Lemma transl_expr_Econdition_true_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (a b c : Csharpminor.expr) (t1: trace) (m1 : mem) (v1 : val) + (t2: trace) (m2 : mem) (v2 : val) (t: trace), + Csharpminor.eval_expr prog le e m a t1 m1 v1 -> + eval_expr_prop le e m a t1 m1 v1 -> + Val.is_true v1 -> + Csharpminor.eval_expr prog le e m1 b t2 m2 v2 -> + eval_expr_prop le e m1 b t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr_prop le e m (Csharpminor.Econdition a b c) t m2 v2. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. + exploit H3. + eauto. eapply val_list_inject_incr; eauto. eauto. eauto. + intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f3; exists te3; exists tm3; exists tv2. + intuition. + rewrite <- H6. subst t; eapply eval_conditionalexpr_true; eauto. + inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto. + eapply inject_incr_trans; eauto. +Qed. + +Lemma transl_expr_Econdition_false_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (a b c : Csharpminor.expr) (t1: trace) (m1 : mem) (v1 : val) + (t2: trace) (m2 : mem) (v2 : val) (t: trace), + Csharpminor.eval_expr prog le e m a t1 m1 v1 -> + eval_expr_prop le e m a t1 m1 v1 -> + Val.is_false v1 -> + Csharpminor.eval_expr prog le e m1 c t2 m2 v2 -> + eval_expr_prop le e m1 c t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr_prop le e m (Csharpminor.Econdition a b c) t m2 v2. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. + exploit H3. + eauto. eapply val_list_inject_incr; eauto. eauto. eauto. + intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f3; exists te3; exists tm3; exists tv2. + intuition. + rewrite <- H6. subst t; eapply eval_conditionalexpr_false; eauto. + inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto. + eapply inject_incr_trans; eauto. +Qed. + +Lemma transl_expr_Elet_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (a b : Csharpminor.expr) (t1: trace) (m1 : mem) (v1 : val) + (t2: trace) (m2 : mem) (v2 : val) (t: trace), + Csharpminor.eval_expr prog le e m a t1 m1 v1 -> + eval_expr_prop le e m a t1 m1 v1 -> + Csharpminor.eval_expr prog (v1 :: le) e m1 b t2 m2 v2 -> + eval_expr_prop (v1 :: le) e m1 b t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr_prop le e m (Csharpminor.Elet a b) t m2 v2. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. + exploit H2. + eauto. + constructor. eauto. eapply val_list_inject_incr; eauto. + eauto. eauto. + intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f3; exists te3; exists tm3; exists tv2. + intuition. + subst ta; eapply eval_Elet; eauto. + eapply inject_incr_trans; eauto. +Qed. + +Remark val_list_inject_nth: + forall f l1 l2, val_list_inject f l1 l2 -> + forall n v1, nth_error l1 n = Some v1 -> + exists v2, nth_error l2 n = Some v2 /\ val_inject f v1 v2. +Proof. + induction 1; destruct n; simpl; intros. + discriminate. discriminate. + injection H1; intros; subst v. exists v'; split; auto. + eauto. +Qed. + +Lemma transl_expr_Eletvar_correct: + forall (le : list val) (e : Csharpminor.env) (m : mem) (n : nat) + (v : val), + nth_error le n = Some v -> + eval_expr_prop le e m (Csharpminor.Eletvar n) E0 m v. +Proof. + intros; red; intros. monadInv TR. + exploit val_list_inject_nth; eauto. intros [tv [A B]]. + exists f1; exists te1; exists tm1; exists tv. + intuition. + subst ta. eapply eval_Eletvar; auto. +Qed. + +Lemma transl_expr_Ealloc_correct: + forall (le: list val) (e: Csharpminor.env) (m1: mem) (a: Csharpminor.expr) + (t: trace) (m2: mem) (n: int) (m3: mem) (b: block), + Csharpminor.eval_expr prog le e m1 a t m2 (Vint n) -> + eval_expr_prop le e m1 a t m2 (Vint n) -> + Mem.alloc m2 0 (Int.signed n) = (m3, b) -> + eval_expr_prop le e m1 (Csharpminor.Ealloc a) t m3 (Vptr b Int.zero). +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + inversion VINJ1. subst tv1 i. + caseEq (alloc tm2 0 (Int.signed n)). intros tm3 tb TALLOC. + assert (LB: Int.min_signed <= 0). compute. congruence. + assert (HB: Int.signed n <= Int.max_signed). + generalize (Int.signed_range n); omega. + exploit alloc_parallel_inject; eauto. + intros [MINJ3 INCR3]. + exists (extend_inject b (Some (tb, 0)) f2); + exists te2; exists tm3; exists (Vptr tb Int.zero). + split. subst ta; econstructor; eauto. + split. econstructor. unfold extend_inject, eq_block. rewrite zeq_true. reflexivity. + reflexivity. + split. assumption. + split. eapply inject_incr_trans; eauto. + eapply match_callstack_alloc; eauto. +Qed. + +Lemma transl_exprlist_Enil_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem), + eval_exprlist_prop le e m Csharpminor.Enil E0 m nil. +Proof. + intros; red; intros. monadInv TR. + exists f1; exists te1; exists tm1; exists (@nil val). + intuition. subst tal; constructor. +Qed. + +Lemma transl_exprlist_Econs_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (a : Csharpminor.expr) (bl : Csharpminor.exprlist) + (t1: trace) (m1 : mem) (v : val) + (t2: trace) (m2 : mem) (vl : list val) (t: trace), + Csharpminor.eval_expr prog le e m a t1 m1 v -> + eval_expr_prop le e m a t1 m1 v -> + Csharpminor.eval_exprlist prog le e m1 bl t2 m2 vl -> + eval_exprlist_prop le e m1 bl t2 m2 vl -> + t = t1 ** t2 -> + eval_exprlist_prop le e m (Csharpminor.Econs a bl) t m2 (v :: vl). +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exploit H2. + eauto. eapply val_list_inject_incr; eauto. eauto. eauto. + intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. + exists f3; exists te3; exists tm3; exists (tv1 :: tv2). + intuition. subst tal; econstructor; eauto. + constructor. eapply val_inject_incr; eauto. auto. + eapply inject_incr_trans; eauto. +Qed. + +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. + generalize TR; clear TR. + unfold transl_fundef, transf_partial_fundef. + caseEq (transl_function gce f); try congruence. + intros tf TR EQ. inversion EQ; clear EQ; subst tfn. + unfold transl_function in TR. + caseEq (build_compilenv gce f); intros cenv stacksize CENV. + rewrite CENV in TR. + destruct (zle stacksize Int.max_signed); try discriminate. + monadInv TR. clear 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]]. + exists f3; exists (Mem.free tm3 sp); exists tvres. + (* execution *) + split. rewrite <- H6; 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 H5. + 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. +Proof. + intros; red; intros. + simpl in TR. inversion TR; clear TR; subst tfn. + exploit event_match_inject; eauto. intros [A B]. + exists f1; exists tm1; exists vres; intuition. + constructor; auto. +Qed. + +Lemma transl_stmt_Sskip_correct: + forall (e : Csharpminor.env) (m : mem), + exec_stmt_prop e m Csharpminor.Sskip E0 m Csharpminor.Out_normal. +Proof. + intros; red; intros. monadInv TR. + exists f1; exists te1; exists tm1; exists Out_normal. + intuition. subst ts; constructor. constructor. +Qed. + +Lemma transl_stmt_Sexpr_correct: + forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) + (t: trace) (m1 : mem) (v : val), + Csharpminor.eval_expr prog nil e m a t m1 v -> + eval_expr_prop nil e m a t m1 v -> + exec_stmt_prop e m (Csharpminor.Sexpr a) t m1 Csharpminor.Out_normal. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f2; exists te2; exists tm2; exists Out_normal. + intuition. subst ts. econstructor; eauto. + constructor. +Qed. + +Lemma transl_stmt_Sassign_correct: + forall (e : Csharpminor.env) (m : mem) + (id : ident) (a : Csharpminor.expr) (t: trace) (m1 : mem) (b : block) + (chunk : memory_chunk) (v : val) (m2 : mem), + Csharpminor.eval_expr prog nil e m a t m1 v -> + eval_expr_prop nil e m a t m1 v -> + eval_var_ref prog e id b chunk -> + store chunk m1 b 0 v = Some m2 -> + exec_stmt_prop e m (Csharpminor.Sassign id a) t m2 Csharpminor.Out_normal. +Proof. + intros; red; intros. monadInv TR; intro EQ0. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR12 MATCH1]]]]]]]]. + exploit var_set_correct; eauto. + intros [te3 [tm3 [EVAL2 [MINJ2 MATCH2]]]]. + exists f2; exists te3; exists tm3; exists Out_normal. + intuition. constructor. +Qed. + +Lemma transl_stmt_Sstore_correct: + forall (e : Csharpminor.env) (m : mem) + (chunk : memory_chunk) (a b : Csharpminor.expr) (t1: trace) (m1 : mem) + (v1 : val) (t2: trace) (m2 : mem) (v2 : val) + (t3: trace) (m3 : mem), + Csharpminor.eval_expr prog nil e m a t1 m1 v1 -> + eval_expr_prop nil e m a t1 m1 v1 -> + Csharpminor.eval_expr prog nil e m1 b t2 m2 v2 -> + eval_expr_prop nil e m1 b t2 m2 v2 -> + storev chunk m2 v1 v2 = Some m3 -> + t3 = t1 ** t2 -> + exec_stmt_prop e m (Csharpminor.Sstore chunk a b) t3 m3 Csharpminor.Out_normal. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exploit H2. + eauto. + eapply val_list_inject_incr; eauto. + eauto. eauto. + intros [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. + exploit make_store_correct. + eexact EVAL1. eexact EVAL2. eauto. eauto. + eapply val_inject_incr; eauto. eauto. + intros [tm4 [EVAL [MINJ4 NEXTBLOCK]]]. + exists f3; exists te3; exists tm4; exists Out_normal. + rewrite <- H6. subst t3. intuition. + constructor. + eapply inject_incr_trans; eauto. + assert (val_inject f3 v1 tv1). eapply val_inject_incr; eauto. + unfold storev in H3; destruct v1; try discriminate. + inversion H4. + rewrite NEXTBLOCK. replace (nextblock m3) with (nextblock m2). + eapply match_callstack_mapped; eauto. congruence. + exploit store_inv; eauto. simpl; symmetry; tauto. +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. subst ts; 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. subst ts; eapply exec_Sseq_stop; eauto. + inversion OINJ1; subst out tout1; congruence. +Qed. + +Lemma transl_stmt_Sifthenelse_true_correct: + forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) + (sl1 sl2 : Csharpminor.stmt) + (t1: trace) (m1 : mem) (v1 : val) (t2: trace) (m2 : mem) + (out : Csharpminor.outcome) (t: trace), + Csharpminor.eval_expr prog nil e m a t1 m1 v1 -> + eval_expr_prop nil e m a t1 m1 v1 -> + Val.is_true v1 -> + Csharpminor.exec_stmt prog e m1 sl1 t2 m2 out -> + exec_stmt_prop e m1 sl1 t2 m2 out -> + t = t1 ** t2 -> + exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) t m2 out. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exploit H3; eauto. + intros [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]]. + exists f3; exists te3; exists tm3; exists tout. + intuition. + subst ts t. eapply exec_ifthenelse_true; eauto. + inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto. + eapply inject_incr_trans; eauto. +Qed. + +Lemma transl_stmt_Sifthenelse_false_correct: + forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) + (sl1 sl2 : Csharpminor.stmt) + (t1: trace) (m1 : mem) (v1 : val) (t2: trace) (m2 : mem) + (out : Csharpminor.outcome) (t: trace), + Csharpminor.eval_expr prog nil e m a t1 m1 v1 -> + eval_expr_prop nil e m a t1 m1 v1 -> + Val.is_false v1 -> + Csharpminor.exec_stmt prog e m1 sl2 t2 m2 out -> + exec_stmt_prop e m1 sl2 t2 m2 out -> + t = t1 ** t2 -> + exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) t m2 out. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + exploit H3; eauto. + intros [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]]. + exists f3; exists te3; exists tm3; exists tout. + intuition. + subst ts t. eapply exec_ifthenelse_false; eauto. + inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto. + eapply inject_incr_trans; 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. 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. + subst ts. 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. subst ts; eapply exec_Sloop_stop; eauto. + inversion OINJ1; subst out tout1; congruence. +Qed. + +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). +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. subst ts; eapply exec_Sblock; eauto. + inversion OINJ1; subst out tout1; simpl. + constructor. + destruct n; constructor. + constructor. + constructor; 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). +Proof. + intros; red; intros. monadInv TR. + exists f1; exists te1; exists tm1; exists (Out_exit n). + intuition. subst ts; constructor. constructor. +Qed. + +Lemma transl_stmt_Sswitch_correct: + forall (e : Csharpminor.env) (m : mem) + (a : Csharpminor.expr) (cases : list (int * nat)) (default : nat) + (t1 : trace) (m1 : mem) (n : int), + Csharpminor.eval_expr prog nil e m a t1 m1 (Vint n) -> + eval_expr_prop nil e m a t1 m1 (Vint n) -> + exec_stmt_prop e m (Csharpminor.Sswitch a cases default) t1 m1 + (Csharpminor.Out_exit (Csharpminor.switch_target n default cases)). +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]]. + exists f2; exists te2; exists tm2; + exists (Out_exit (switch_target n default cases)). intuition. + subst ts. constructor. inversion VINJ1. subst tv1. assumption. + constructor. +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). +Proof. + intros; red; intros. monadInv TR. + exists f1; exists te1; exists tm1; exists (Out_return None). + intuition. subst ts; constructor. constructor. +Qed. + +Lemma transl_stmt_Sreturn_some_correct: + forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) + (t1: trace) (m1 : mem) (v : val), + Csharpminor.eval_expr prog nil e m a t1 m1 v -> + eval_expr_prop nil e m a t1 m1 v -> + exec_stmt_prop e m (Csharpminor.Sreturn (Some a)) t1 m1 + (Csharpminor.Out_return (Some v)). +Proof. + intros; red; intros; monadInv TR. + exploit H0; eauto. + intros [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]]. + exists f2; exists te2; exists tm2; exists (Out_return (Some tv1)). + intuition. subst ts; 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 + (eval_funcall_ind4 prog + eval_expr_prop + eval_exprlist_prop + eval_funcall_prop + exec_stmt_prop + + transl_expr_Evar_correct + transl_expr_Eaddrof_correct + transl_expr_Eop_correct + transl_expr_Eload_correct + transl_expr_Ecall_correct + transl_expr_Econdition_true_correct + transl_expr_Econdition_false_correct + transl_expr_Elet_correct + transl_expr_Eletvar_correct + transl_expr_Ealloc_correct + transl_exprlist_Enil_correct + transl_exprlist_Econs_correct + transl_funcall_internal_correct + transl_funcall_external_correct + transl_stmt_Sskip_correct + transl_stmt_Sexpr_correct + transl_stmt_Sassign_correct + transl_stmt_Sstore_correct + transl_stmt_Sseq_continue_correct + transl_stmt_Sseq_stop_correct + transl_stmt_Sifthenelse_true_correct + transl_stmt_Sifthenelse_false_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). + +(** The [match_globalenvs] relation holds for the global environments + of the source program and the transformed program. *) + +Lemma match_globalenvs_init: + let m := Genv.init_mem (program_of_program 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. +Proof. + intros. constructor. + (* globalvars *) + (* symbols *) + intros. split. + unfold f. rewrite zlt_true. auto. unfold m. + eapply Genv.find_symbol_inv; eauto. + rewrite <- H. apply symbols_preserved. + intros. unfold f. rewrite zlt_true. auto. + generalize (nextblock_pos m). omega. +Qed. + +(** The correctness of the translation of a whole Csharpminor program + follows. *) + +Theorem transl_program_correct: + forall t n, + Csharpminor.exec_program prog t (Vint n) -> + exec_program tprog t (Vint n). +Proof. + intros t n [b [fn [m [FINDS [FINDF [SIG EVAL]]]]]]. + elim (function_ptr_translated _ _ FINDF). intros tfn [TFIND TR]. + set (m0 := Genv.init_mem (program_of_program prog)) in *. + set (f := fun b => if zlt b m0.(nextblock) then Some(b, 0) else None). + assert (MINJ0: mem_inject f m0 m0). + unfold f; constructor; intros. + apply zlt_false; auto. + destruct (zlt b0 (nextblock m0)); try discriminate. + inversion H; subst b' delta. + split. auto. + constructor. compute. split; congruence. left; auto. + intros; omega. + generalize (Genv.initmem_block_init (program_of_program prog) b0). fold m0. intros [idata EQ]. + rewrite EQ. simpl. apply Mem.contents_init_data_inject. + destruct (zlt b1 (nextblock m0)); try discriminate. + destruct (zlt b2 (nextblock m0)); try discriminate. + left; congruence. + assert (MATCH0: match_callstack f nil m0.(nextblock) m0.(nextblock) m0). + constructor. unfold f; apply match_globalenvs_init. + fold ge in EVAL. + exploit transl_function_correct; eauto. + intros [f1 [tm1 [tres [TEVAL [VINJ [MINJ1 [INCR MATCH1]]]]]]]. + exists b; exists tfn; exists tm1. + split. fold tge. rewrite <- FINDS. + replace (prog_main prog) with (AST.prog_main tprog). fold ge. apply symbols_preserved. + transitivity (AST.prog_main (program_of_program prog)). + apply transform_partial_program_main with (transl_fundef gce). assumption. + reflexivity. + split. assumption. + split. rewrite <- SIG. apply sig_preserved; auto. + rewrite (Genv.init_mem_transf_partial (transl_fundef gce) _ TRANSL). + inversion VINJ; subst tres. assumption. +Qed. + +End TRANSLATION. -- cgit v1.2.3