diff options
Diffstat (limited to 'backend/Cminorgenproof.v')
| -rw-r--r-- | backend/Cminorgenproof.v | 1209 |
1 files changed, 645 insertions, 564 deletions
diff --git a/backend/Cminorgenproof.v b/backend/Cminorgenproof.v index 7b3bc9bb..7820095a 100644 --- a/backend/Cminorgenproof.v +++ b/backend/Cminorgenproof.v @@ -8,6 +8,7 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import Mem. +Require Import Events. Require Import Globalenvs. Require Import Csharpminor. Require Import Op. @@ -29,38 +30,51 @@ Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. intro. unfold ge, tge. - apply Genv.find_symbol_transf_partial with (transl_function gce). + apply Genv.find_symbol_transf_partial with (transl_fundef gce). exact TRANSL. Qed. Lemma function_ptr_translated: - forall (b: block) (f: Csharpminor.function), + 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_function gce f = Some 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_function gce) TRANSL H). - case (transl_function gce f). + (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.function), + forall (v: val) (f: Csharpminor.fundef), Genv.find_funct ge v = Some f -> exists tf, - Genv.find_funct tge v = Some tf /\ transl_function gce f = Some tf. + Genv.find_funct tge v = Some tf /\ transl_fundef gce f = Some tf. Proof. intros. generalize - (Genv.find_funct_transf_partial (transl_function gce) TRANSL H). - case (transl_function gce f). + (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 @@ -72,9 +86,9 @@ Definition global_compilenv_match (ce: compilenv) (gv: gvarenv) : Prop := Lemma global_compilenv_charact: global_compilenv_match gce (global_var_env prog). Proof. - set (mkgve := fun gv vars => + set (mkgve := fun gv (vars: list (ident * var_kind * list init_data)) => List.fold_left - (fun gv (id_vi: ident * var_kind) => PTree.set (fst id_vi) (snd id_vi) gv) + (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 -> @@ -83,7 +97,7 @@ Proof. induction vars; simpl; intros. auto. apply IHvars. intro id1. unfold assign_global_variable. - destruct a as [id2 lv2]. destruct lv2; simpl; rewrite PMap.gsspec; rewrite PTree.gsspec. + 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. @@ -283,6 +297,7 @@ Qed. 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. @@ -305,34 +320,31 @@ Lemma load_result_normalized: 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 v tv -> - val_normalized chunk tv -> + 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 H3. constructor; auto. + intros. inversion H2. constructor; auto. intros. generalize (me_vars0 id0); intro. - inversion H4; subst. + inversion H3; subst. (* var_local *) case (peq id id0); intro. (* the stored variable *) subst id0. - change Csharpminor.var_kind with var_kind in H5. - rewrite H in H6. injection H6; clear H6; intros; subst b0 chunk0. + 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. - replace tv with (Val.load_result chunk tv). - apply Mem.load_result_inject. constructor; auto. - apply load_result_normalized; auto. + auto. (* a different variable *) econstructor; eauto. - rewrite <- H7. eapply load_store_other; eauto. + rewrite <- H6. eapply load_store_other; eauto. rewrite PTree.gso; auto. (* var_stack_scalar *) econstructor; eauto. @@ -375,16 +387,15 @@ 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 v tv -> - val_normalized chunk tv -> + 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 H3. constructor; auto. + intros. inversion H2. constructor; auto. eapply match_env_store_local; eauto. eapply match_callstack_store_above; eauto. - inversion H17. + inversion H16. generalize (me_bounded0 _ _ _ H). omega. Qed. @@ -409,20 +420,19 @@ 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 v tv -> - val_normalized chunk tv -> + 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 H4. constructor; auto. + 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 H18. + inversion H17. generalize (me_bounded0 _ _ _ H). omega. Qed. @@ -698,6 +708,90 @@ Proof. 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: @@ -757,14 +851,14 @@ Qed. provided arguments match pairwise ([val_list_inject f] hypothesis). *) Lemma make_op_correct: - forall al a op vl m2 v sp le te1 tm1 te2 tm2 tvl f, + 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 te2 tm2 tvl -> + 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 te2 tm2 tv + eval_expr tge (Vptr sp Int.zero) le te1 tm1 a t te2 tm2 tv /\ val_inject f v tv. Proof. intros. @@ -782,23 +876,27 @@ Proof. (* floatconst *) TrivialOp. econstructor. constructor. reflexivity. (* Unary operators *) - inversion H1. subst sp0 le0 e m a0 bl e2 m0 tvl. - inversion H14. subst sp0 le0 e m e1 m1 vl0. - inversion H2. subst vl v' vl'. inversion H8. subst vl0. + 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. subst sp0 le0 e m a0 bl e2 m0 tvl. - inversion H14. subst sp0 le0 e m a0 bl e2 m3 vl0. - inversion H16. subst sp0 le0 e m e0 m0 vl1. - inversion H2. subst vl v' vl'. - inversion H8. subst vl0 v' vl'. - inversion H12. subst vl. + 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 H9; subst v0; subst v1; + inversion H7; inversion H8; subst v0; subst v1; TrivialOp. (* add int ptr *) exists (Vptr b2 (Int.add ofs2 i)); split. @@ -815,7 +913,8 @@ Proof. (* 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 ofs2 ofs3)); split. eauto with evalexpr. + exists (Vint (Int.sub ofs3 ofs2)); split. + eauto with evalexpr. subst ofs2 ofs3. replace x0 with x. rewrite Int.sub_shifted. constructor. congruence. (* divs *) @@ -842,11 +941,11 @@ Proof. (* cmp int ptr *) elim (eval_compare_null_inv _ _ _ H0); intros; subst i1 i. exists v; split. eauto with evalexpr. - elim H18; intros [A B]; subst v; unfold Vtrue, Vfalse; constructor. + 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 H18; intros [A B]; subst v; unfold Vtrue, Vfalse; constructor. + 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. @@ -854,7 +953,7 @@ Proof. assert (b4 = b2); [congruence|subst b4]. assert (x0 = x); [congruence|subst x0]. elim (andb_prop _ _ EQ); intros. - exists (Val.of_bool (Int.cmp c ofs2 ofs3)); split. + 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. @@ -866,55 +965,51 @@ Qed. normalized according to the given memory chunk. *) Lemma make_cast_correct: - forall f sp le te1 tm1 a te2 tm2 v chunk v' tv, - eval_expr tge (Vptr sp Int.zero) le te1 tm1 a te2 tm2 tv -> - cast chunk v = Some v' -> + 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) - te2 tm2 tv' - /\ val_inject f v' tv' - /\ val_normalized chunk tv'. + t te2 tm2 tv' + /\ val_inject f (Val.load_result chunk v) tv'. Proof. - intros. destruct chunk; destruct v; simplify_eq H0; intro; subst v'; simpl; - inversion H1; subst tv. + intros. destruct chunk. - exists (Vint (Int.cast8signed i)). + exists (Val.cast8signed tv). split. apply eval_cast8signed; auto. - split. constructor. exists (Vint i); reflexivity. + inversion H0; simpl; constructor. - exists (Vint (Int.cast8unsigned i)). + exists (Val.cast8unsigned tv). split. apply eval_cast8unsigned; auto. - split. constructor. exists (Vint i); reflexivity. + inversion H0; simpl; constructor. - exists (Vint (Int.cast16signed i)). + exists (Val.cast16signed tv). split. apply eval_cast16signed; auto. - split. constructor. exists (Vint i); reflexivity. + inversion H0; simpl; constructor. - exists (Vint (Int.cast16unsigned i)). + exists (Val.cast16unsigned tv). split. apply eval_cast16unsigned; auto. - split. constructor. exists (Vint i); reflexivity. - - exists (Vint i). - split. auto. split. auto. exists (Vint i); reflexivity. + inversion H0; simpl; constructor. - exists (Vptr b2 ofs2). - split. auto. split. auto. exists (Vptr b2 ofs2); reflexivity. + exists tv. + split. simpl; auto. + inversion H0; simpl; econstructor; eauto. - exists (Vfloat (Float.singleoffloat f0)). + exists (Val.singleoffloat tv). split. apply eval_singleoffloat; auto. - split. constructor. exists (Vfloat f0); reflexivity. + inversion H0; simpl; constructor. - exists (Vfloat f0). - split. auto. split. auto. exists (Vfloat f0); reflexivity. + 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) - te tm (Vptr sp (Int.repr ofs)). + E0 te tm (Vptr sp (Int.repr ofs)). Proof. intros; unfold make_stackaddr. eapply eval_Eop. econstructor. simpl. decEq. decEq. @@ -926,7 +1021,7 @@ Lemma make_globaladdr_correct: Genv.find_symbol tge id = Some b -> eval_expr tge (Vptr sp Int.zero) le te tm (make_globaladdr id) - te tm (Vptr b Int.zero). + E0 te tm (Vptr b Int.zero). Proof. intros; unfold make_globaladdr. eapply eval_Eop. econstructor. simpl. rewrite H. auto. @@ -935,67 +1030,75 @@ Qed. (** Correctness of [make_load] and [make_store]. *) Lemma make_load_correct: - forall sp le te1 tm1 a te2 tm2 va chunk v, - eval_expr tge (Vptr sp Int.zero) le te1 tm1 a te2 tm2 va -> + 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) - te2 tm2 v. + t te2 tm2 v. Proof. intros; unfold make_load. eapply eval_load; eauto. Qed. -Lemma val_content_inject_cast: - forall f chunk v1 v2 tv1, - cast chunk v1 = Some v2 -> - val_inject f v1 tv1 -> - val_content_inject f (mem_chunk chunk) v2 tv1. +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. destruct chunk; destruct v1; simplify_eq H; intro; subst v2; - inversion H0; simpl. - 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. - constructor; constructor. - constructor; econstructor; eauto. - apply val_content_inject_32. apply Float.singleoffloat_idem. - constructor; constructor. + 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 le te1 tm1 addr te2 tm2 tvaddr rhs te3 tm3 tvrhs - chunk vrhs v m3 vaddr m4, - eval_expr tge (Vptr sp Int.zero) le - te1 tm1 addr te2 tm2 tvaddr -> - eval_expr tge (Vptr sp Int.zero) le - te2 tm2 rhs te3 tm3 tvrhs -> - cast chunk vrhs = Some v -> - Mem.storev chunk m3 vaddr v = Some m4 -> + 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, exists tv, - eval_expr tge (Vptr sp Int.zero) le + exists tm4, + exec_stmt tge (Vptr sp Int.zero) te1 tm1 (make_store chunk addr rhs) - te3 tm4 tv + (t1**t2) te3 tm4 Out_normal /\ mem_inject f m4 tm4 - /\ val_inject f v tv /\ nextblock tm4 = nextblock tm3. Proof. intros. unfold make_store. - assert (val_content_inject f (mem_chunk chunk) v tvrhs). - eapply val_content_inject_cast; eauto. - elim (storev_mapped_inject_1 _ _ _ _ _ _ _ _ _ H3 H2 H4 H6). - intros tm4 [STORE MEMINJ]. - generalize (eval_store _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H H0 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. - elim (make_cast_correct _ _ _ _ _ _ _ _ _ _ _ _ EVALSTORE H1 H5). - intros tv [EVALCAST [VALINJ VALNORM]]. - exists tm4; exists tv. intuition. + exists tm4. + split. apply exec_Sexpr with tv. auto. + split. auto. unfold storev in STORE; destruct tvaddr; try discriminate. - generalize (store_inv _ _ _ _ _ _ STORE). simpl. tauto. + exploit store_inv; eauto. simpl. tauto. Qed. (** Correctness of the variable accessors [var_get], [var_set] @@ -1009,7 +1112,7 @@ Lemma var_get_correct: 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 te tm 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. @@ -1025,8 +1128,8 @@ Proof. inversion H2; [subst|congruence]. assert (b0 = b). congruence. subst b0. assert (chunk0 = chunk). congruence. subst chunk0. - assert (loadv chunk m (Vptr b Int.zero) = Some v). assumption. - generalize (loadv_inject _ _ _ _ _ _ _ H1 H9 H7). + 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. @@ -1052,7 +1155,7 @@ Lemma var_addr_correct: 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 te tm 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. @@ -1086,65 +1189,61 @@ Proof. Qed. Lemma var_set_correct: - forall cenv id rhs a f e te2 sp lo hi m2 cs tm2 le te1 tm1 vrhs b chunk v1 v2 m3, + 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) le te1 tm1 rhs te2 tm2 vrhs -> - val_inject f v1 vrhs -> + 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 -> - cast chunk v1 = Some v2 -> - store chunk m2 b 0 v2 = Some m3 -> - exists te3, exists tm3, exists tv, - eval_expr tge (Vptr sp Int.zero) le te1 tm1 a te3 tm3 tv /\ - val_inject f v2 tv /\ + 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). - generalize (store_inv _ _ _ _ _ _ H6). simpl. tauto. + 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 H20; auto. - inversion H7; subst; rewrite <- H8 in H; inversion H; subst; clear H. + 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. - elim (make_cast_correct _ _ _ _ _ _ _ _ _ _ _ _ H1 H5 H2). - intros tv [EVAL [INJ NORM]]. - exists (PTree.set id tv te2); exists tm2; exists tv. - split. eapply eval_Eassign. auto. - split. auto. + 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) v2 = Some m3). assumption. - generalize (make_stackaddr_correct sp le te1 tm1 ofs). intro EVALSTACKADDR. - generalize (make_store_correct _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - EVALSTACKADDR H1 H5 H11 H3 H10 H2). - intros [tm3 [tv [EVAL [MEMINJ [VALINJ TNEXTBLOCK]]]]]. - exists te2; exists tm3; exists tv. - split. auto. split. auto. split. auto. + 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 H10; congruence. + inversion H9; congruence. (* var_global_scalar *) inversion H4; [congruence|subst]. assert (chunk0 = chunk). congruence. subst chunk0. - assert (storev chunk m2 (Vptr b Int.zero) v2 = Some m3). assumption. + assert (storev chunk m2 (Vptr b Int.zero) v = Some m3). assumption. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inversion H14. destruct (mg_symbols0 _ _ H11) as [A B]. - assert (val_inject f (Vptr b Int.zero) (Vptr b Int.zero)). econstructor; eauto. - generalize (make_globaladdr_correct sp le te1 tm1 id b B). intro EVALGLOBALADDR. - generalize (make_store_correct _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - EVALGLOBALADDR H1 H5 H13 H3 H15 H2). - intros [tm3 [tv [EVAL [MEMINJ [VALINJ TNEXTBLOCK]]]]]. - exists te2; exists tm3; exists tv. - split. auto. split. auto. split. auto. + 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. @@ -1228,36 +1327,26 @@ Proof. omega. omega. omega. omega. unfold sizeof; rewrite LV. omega. intros. left. generalize (BOUND _ _ H5). omega. elim H3; intros MINJ1 INCR1; clear H3. - assert (MATCH1: match_callstack f1 - (mkframe cenv1 (PTree.set id (b1, lv) e) te sp lo (nextblock m1) :: cs) - (nextblock m1) (nextblock tm) m1). - unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. - assert (SZ1POS: 0 <= sz1). rewrite <- H1. omega. - assert (BOUND1: forall b delta, f1 b = Some(sp, delta) -> - high_bound m1 b + delta <= sz1). + 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. - generalize (IHalloc_variables _ _ _ ASVS MATCH1 MINJ1 SZ1POS BOUND1 DEFINED1). 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. - generalize (alloc_unmapped_inject _ _ _ _ _ _ _ MINJ H). + exploit alloc_unmapped_inject; eauto. set (f1 := extend_inject b1 None f). intros [MINJ1 INCR1]. - assert (MATCH1: match_callstack f1 - (mkframe cenv1 (PTree.set id (b1, lv) e) te sp lo (nextblock m1) :: cs) - (nextblock m1) (nextblock tm) m1). - unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. - assert (BOUND1: forall b delta, f1 b = Some(sp, delta) -> - high_bound m1 b + delta <= sz). + 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. - generalize (IHalloc_variables _ _ _ ASVS MATCH1 MINJ1 SZPOS BOUND1 DEFINED1). intros [f' [INCR2 [MINJ2 MATCH2]]]. exists f'; intuition. eapply inject_incr_trans; eauto. (* 2. lv = LVarray dim, info = Var_stack_array *) @@ -1273,20 +1362,15 @@ Proof. unfold f1; eapply alloc_mapped_inject; eauto. omega. omega. omega. omega. unfold sizeof; rewrite LV. omega. intros. left. generalize (BOUND _ _ H8). omega. - elim H6; intros MINJ1 INCR1; clear H6. - assert (MATCH1: match_callstack f1 - (mkframe cenv1 (PTree.set id (b1, lv) e) te sp lo (nextblock m1) :: cs) - (nextblock m1) (nextblock tm) m1). + destruct H6 as [MINJ1 INCR1]. + exploit IHalloc_variables; eauto. unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. - assert (SZ1POS: 0 <= sz1). rewrite <- H1. omega. - assert (BOUND1: forall b delta, f1 b = Some(sp, delta) -> - high_bound m1 b + delta <= sz1). - 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. - generalize (IHalloc_variables _ _ _ ASVS MATCH1 MINJ1 SZ1POS BOUND1 DEFINED1). + 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. @@ -1370,15 +1454,15 @@ Proof. (* me_inj *) intros until lv2. unfold Csharpminor.empty_env; rewrite PTree.gempty; congruence. (* me_inv *) - intros. elim (mi_mappedblocks _ _ _ H4 _ _ _ H5); intros. - elim (fresh_block_alloc _ _ _ _ _ H2 H6). + intros. exploit mi_mappedblocks; eauto. intros [A B]. + elim (fresh_block_alloc _ _ _ _ _ H2 A). (* me_incr *) - intros. elim (mi_mappedblocks _ _ _ H4 _ _ _ H5); intros. + intros. exploit mi_mappedblocks; eauto. intros [A B]. rewrite SP; auto. rewrite SP; auto. eapply alloc_right_inject; eauto. omega. - intros. elim (mi_mappedblocks _ _ _ H4 _ _ _ H5); intros. + intros. exploit mi_mappedblocks; eauto. intros [A B]. unfold block in SP; omegaContradiction. (* defined *) intros. unfold te. apply set_locals_params_defined. @@ -1421,7 +1505,7 @@ Proof. unfold block; rewrite H2; omega. elim H4; intro. left; congruence. right; auto. elim H3; intro. subst b b1. - generalize (alloc_variables_nextblock_incr _ _ _ _ _ _ H0). + generalize (alloc_variables_nextblock_incr _ _ _ _ _ _ H0). rewrite H2. omega. generalize (B H4). rewrite H2. omega. Qed. @@ -1465,7 +1549,7 @@ Lemma store_parameters_correct: exists te2, exists tm2, exec_stmt tge (Vptr sp Int.zero) te1 tm1 (store_parameters cenv params) - te2 tm2 Out_normal + 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. @@ -1476,59 +1560,54 @@ Proof. 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 H19. + inversion H18. inversion NOREPET. subst hd tl. assert (NEXT: nextblock m1 = nextblock m). - generalize (store_inv _ _ _ _ _ _ H1). simpl; tauto. - generalize (me_vars0 id). intro. inversion H3; subst. + 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'. - assert (eval_expr tge (Vptr sp Int.zero) nil te1 tm1 (Evar id) te1 tm1 tv). - constructor. auto. - generalize (make_cast_correct _ _ _ _ _ _ _ _ _ _ _ _ - H15 H0 H11). - intros [tv' [EVAL1 [VINJ1 VNORM]]]. + 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 H5. change id with (fst (id, lv)). apply List.in_map; auto. - generalize (store_unmapped_inject _ _ _ _ _ _ _ _ MINJ H1 H9); intro MINJ2. - generalize (match_callstack_store_local _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - H VINJ1 VNORM H1 MATCH); + 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. - destruct (IHbind_parameters _ _ _ _ _ _ _ _ VVM2 H6 MINJ2 MATCH2) - as [te3 [tm3 [EXEC3 [MINJ3 MATCH3]]]]. + exploit IHbind_parameters; eauto. + intros [te3 [tm3 [EXEC3 [MINJ3 MATCH3]]]]. exists te3; exists tm3. (* execution *) - split. apply exec_Sseq_continue with te2 tm1. - econstructor. unfold te2. constructor. assumption. - assumption. + 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. - pose (EVAL1 := make_stackaddr_correct sp nil te1 tm1 ofs). - assert (EVAL2: eval_expr tge (Vptr sp Int.zero) nil te1 tm1 (Evar id) te1 tm1 tv). - constructor. auto. - destruct (make_store_correct _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - (Vptr b Int.zero) _ - EVAL1 EVAL2 H0 H1 MINJ H8 H11) - as [tm2 [tv' [EVAL3 [MINJ2 [VINJ NEXT1]]]]]. - assert (f b <> None). inversion H8. congruence. - generalize (match_callstack_mapped _ _ _ _ _ MATCH _ _ _ _ _ H9 H1). + 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. - destruct (IHbind_parameters _ _ _ _ _ _ _ _ - H12 H6 MINJ2 MATCH2) as [te3 [tm3 [EVAL4 [MINJ3 MATCH3]]]]. + exploit IHbind_parameters; eauto. + intros [te3 [tm3 [EVAL4 [MINJ3 MATCH3]]]]. exists te3; exists tm3. (* execution *) - split. apply exec_Sseq_continue with te1 tm2. - econstructor. eauto. - assumption. + split. apply exec_Sseq_continue with (E0**E0) te1 tm2 E0. + auto. assumption. traceEq. (* meminj & match_callstack *) tauto. @@ -1589,44 +1668,6 @@ Proof. induction 1; simpl; eauto. Qed. -(**** -Lemma build_compilenv_domain: - forall f id chunk, - In (id, chunk) f.(Csharpminor.fn_params) -> - (fst (build_compilenv gce f))!id <> None. -Proof. - assert (forall atk id lv cenv_sz id0, - let cenv_sz' := assign_variable atk (id, lv) cenv_sz in - (fst cenv_sz')!id <> None - /\ ((fst cenv_sz)!id0 <> None -> (fst cenv_sz')!id0 <> None)). - intros. unfold cenv_sz'. destruct cenv_sz as [cenv sz]. - unfold assign_variable. destruct lv. - case (Identset.mem id atk); simpl. split. rewrite PTree.gss. congruence. - rewrite PTree.gsspec. case (peq id0 id); intros. congruence. auto. - split. rewrite PTree.gss. congruence. - rewrite PTree.gsspec. case (peq id0 id); intros. congruence. auto. - simpl. split. rewrite PTree.gss. congruence. - rewrite PTree.gsspec. case (peq id0 id); intros. congruence. auto. - - assert (forall atk id_lv_list cenv_sz id lv, - In (id, lv) id_lv_list \/ (fst cenv_sz)!id <> None -> - (fst (assign_variables atk id_lv_list cenv_sz))!id <> None). - induction id_lv_list; simpl; intros. - tauto. - apply IHid_lv_list with lv. - destruct a as [id0 lv0]. - generalize (H atk id0 lv0 cenv_sz id). - simpl. intro. intuition. injection H0; intros; subst id0 lv0. intuition. - - intros. unfold build_compilenv. apply H0 with (Vscalar chunk). - left. unfold fn_variables. apply List.in_or_app. left. - set (g := fun (id_chunk : ident * memory_chunk) => (fst id_chunk, Vscalar (snd id_chunk))). - change positive with ident. - change (id, Vscalar chunk) with (g (id, chunk)). - apply List.in_map. auto. -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 @@ -1649,7 +1690,7 @@ Lemma function_entry_ok: exists f2, exists te2, exists tm2, exec_stmt tge (Vptr sp Int.zero) te tm1 (store_parameters cenv fn.(Csharpminor.fn_params)) - te2 tm2 Out_normal + E0 te2 tm2 Out_normal /\ mem_inject f2 m2 tm2 /\ inject_incr f f2 /\ match_callstack f2 @@ -1658,24 +1699,21 @@ Lemma function_entry_ok: /\ (forall b, m.(nextblock) <= b < m1.(nextblock) <-> In b lb). Proof. intros. - generalize (bind_parameters_length _ _ _ _ _ H0); intro LEN1. - destruct (match_callstack_alloc_variables _ _ _ _ _ _ _ _ _ _ _ _ tvargs - H2 H3 H H4 H1 H6) - as [f1 [INCR1 [MINJ1 MATCH1]]]. - fold te in MATCH1. - assert (VLI: val_list_inject f1 vargs tvargs). - eapply val_list_inject_incr; eauto. - generalize (vars_vals_match_holds _ _ _ _ LEN1 VLI _ - (list_norepet_append_commut _ _ H7)). - fold te. intro VVM. - assert (NOREPET: list_norepet (List.map (@fst ident memory_chunk) fn.(Csharpminor.fn_params))). - unfold fn_params_names in H7. - eapply list_norepet_append_left; eauto. - destruct (store_parameters_correct _ _ _ _ _ H0 _ _ _ _ _ _ _ _ - VVM NOREPET MINJ1 MATCH1) - as [te2 [tm2 [EXEC [MINJ2 MATCH2]]]]. + 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. + split; auto. split; auto. split; auto. split; auto. intros; eapply alloc_variables_list_block; eauto. Qed. @@ -1745,7 +1783,7 @@ Ltac monadInv H := hypotheses in the proof of simulation. *) Definition eval_expr_prop - (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (a: Csharpminor.expr) (m2: mem) (v: val) : 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) @@ -1754,7 +1792,7 @@ Definition eval_expr_prop (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 te2 tm2 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 @@ -1763,7 +1801,7 @@ Definition eval_expr_prop m2.(nextblock) tm2.(nextblock) m2. Definition eval_exprlist_prop - (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (al: Csharpminor.exprlist) (m2: mem) (vl: list val) : 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) @@ -1772,7 +1810,7 @@ Definition eval_exprlist_prop (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 te2 tm2 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 @@ -1781,14 +1819,14 @@ Definition eval_exprlist_prop m2.(nextblock) tm2.(nextblock) m2. Definition eval_funcall_prop - (m1: mem) (fn: Csharpminor.function) (args: list val) (m2: mem) (res: val) : Prop := + (m1: mem) (fn: Csharpminor.fundef) (args: list val) (t: trace) (m2: mem) (res: val) : Prop := forall tfn f1 tm1 cs targs - (TR: transl_function gce fn = Some tfn) + (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 tm2 tres + eval_funcall tge tm1 tfn targs t tm2 tres /\ val_inject f2 res tres /\ mem_inject f2 m2 tm2 /\ inject_incr f1 f2 @@ -1807,7 +1845,7 @@ Inductive outcome_inject (f: meminj) : Csharpminor.outcome -> outcome -> Prop := outcome_inject f (Csharpminor.Out_return (Some v1)) (Out_return (Some v2)). Definition exec_stmt_prop - (e: Csharpminor.env) (m1: mem) (s: Csharpminor.stmt) (m2: mem) (out: Csharpminor.outcome): 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) @@ -1815,7 +1853,7 @@ Definition exec_stmt_prop (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 te2 tm2 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 @@ -1823,14 +1861,6 @@ Definition exec_stmt_prop (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2. -(* -Check (eval_funcall_ind4 prog - eval_expr_prop - eval_exprlist_prop - eval_funcall_prop - exec_stmt_prop). -*) - (** There are as many cases in the inductive proof as there are evaluation rules in the Csharpminor semantics. We treat each case as a separate lemma. *) @@ -1841,33 +1871,12 @@ Lemma transl_expr_Evar_correct: (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) m v. + eval_expr_prop le e m (Csharpminor.Evar id) E0 m v. Proof. intros; red; intros. unfold transl_expr in TR. - generalize (var_get_correct _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ tle - TR MATCH MINJ H H0). + exploit var_get_correct; eauto. intros [tv [EVAL VINJ]]. - exists f1; exists te1; exists tm1; exists tv; intuition. -Qed. - -Lemma transl_expr_Eassign_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (id : positive) (a : Csharpminor.expr) (m1 : mem) (b : block) - (chunk : memory_chunk) (v1 v2 : val) (m2 : mem), - Csharpminor.eval_expr prog le e m a m1 v1 -> - eval_expr_prop le e m a m1 v1 -> - eval_var_ref prog e id b chunk -> - cast chunk v1 = Some v2 -> - store chunk m1 b 0 v2 = Some m2 -> - eval_expr_prop le e m (Csharpminor.Eassign id a) m2 v2. -Proof. - intros; red; intros. monadInv TR; intro EQ0. - generalize (H0 _ _ _ _ _ _ _ _ _ _ EQ LINJ MINJ MATCH). - intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR12 MATCH1]]]]]]]]. - generalize (var_set_correct _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - EQ0 MATCH1 EVAL1 VINJ1 MINJ1 H1 H2 H3). - intros [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 MATCH2]]]]]]. - exists f2; exists te3; exists tm3; exists tv2. tauto. + exists f1; exists te1; exists tm1; exists tv; intuition eauto. Qed. Lemma transl_expr_Eaddrof_correct: @@ -1875,199 +1884,162 @@ Lemma transl_expr_Eaddrof_correct: (e : Csharpminor.env) (m : mem) (id : positive) (b : block), eval_var_addr prog e id b -> - eval_expr_prop le e m (Eaddrof id) m (Vptr b Int.zero). + eval_expr_prop le e m (Eaddrof id) E0 m (Vptr b Int.zero). Proof. intros; red; intros. simpl in TR. - generalize (var_addr_correct _ _ _ _ _ _ _ _ _ _ _ _ _ tle - MATCH TR H). + exploit var_addr_correct; eauto. intros [tv [EVAL VINJ]]. - exists f1; exists te1; exists tm1; exists tv. intuition. + 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) (m1 : mem) - (vl : list val) (v : val), - Csharpminor.eval_exprlist prog le e m al m1 vl -> - eval_exprlist_prop le e m al m1 vl -> + (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) m1 v. + eval_expr_prop le e m (Csharpminor.Eop op al) t m1 v. Proof. intros; red; intros. monadInv TR; intro EQ0. - generalize (H0 _ _ _ _ _ _ _ _ _ _ EQ LINJ MINJ MATCH). + exploit H0; eauto. intros [f2 [te2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. - generalize (make_op_correct _ _ _ _ _ _ _ _ _ _ _ _ _ _ - EQ0 H1 EVAL1 VINJ1 MINJ1). + 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) (m1 : mem) + (chunk : memory_chunk) (a : Csharpminor.expr) (t: trace) (m1 : mem) (v1 v : val), - Csharpminor.eval_expr prog le e m a m1 v1 -> - eval_expr_prop le e m a m1 v1 -> + 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) m1 v. + eval_expr_prop le e m (Csharpminor.Eload chunk a) t m1 v. Proof. intros; red; intros. monadInv TR. - destruct (H0 _ _ _ _ _ _ _ _ _ _ EQ LINJ MINJ MATCH) - as [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]]. - destruct (loadv_inject _ _ _ _ _ _ _ MINJ2 H1 VINJ1) - as [tv [TLOAD VINJ]]. + 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_Estore_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (chunk : memory_chunk) (a b : Csharpminor.expr) (m1 : mem) - (v1 : val) (m2 : mem) (v2 : val) (m3 : mem) (v3 : val), - Csharpminor.eval_expr prog le e m a m1 v1 -> - eval_expr_prop le e m a m1 v1 -> - Csharpminor.eval_expr prog le e m1 b m2 v2 -> - eval_expr_prop le e m1 b m2 v2 -> - cast chunk v2 = Some v3 -> - storev chunk m2 v1 v3 = Some m3 -> - eval_expr_prop le e m (Csharpminor.Estore chunk a b) m3 v3. -Proof. - intros; red; intros. monadInv TR. - destruct (H0 _ _ _ _ _ _ _ _ _ _ EQ LINJ MINJ MATCH) - as [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - assert (LINJ2: val_list_inject f2 le tle). eapply val_list_inject_incr; eauto. - destruct (H2 _ _ _ _ _ _ _ _ _ _ EQ0 LINJ2 MINJ2 MATCH2) - as [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. - assert (VINJ1': val_inject f3 v1 tv1). eapply val_inject_incr; eauto. - destruct (make_store_correct _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - EVAL1 EVAL2 H3 H4 MINJ3 VINJ1' VINJ2) - as [tm4 [tv [EVAL [MINJ4 [VINJ4 NEXTBLOCK]]]]]. - exists f3; exists te3; exists tm4; exists tv. - rewrite <- H6. intuition. - eapply inject_incr_trans; eauto. - assert (val_inject f3 v1 tv1). eapply val_inject_incr; eauto. - unfold storev in H4; destruct v1; try discriminate. - inversion H5. - rewrite NEXTBLOCK. replace (nextblock m3) with (nextblock m2). - eapply match_callstack_mapped; eauto. congruence. - generalize (store_inv _ _ _ _ _ _ H4). simpl; symmetry; tauto. -Qed. - -Lemma sig_transl_function: - forall f tf, transl_function gce f = Some tf -> tf.(fn_sig) = f.(Csharpminor.fn_sig). -Proof. - intros f tf. unfold transl_function. - destruct (build_compilenv gce f). - case (zle z Int.max_signed); intros. - monadInv H. subst tf; reflexivity. - congruence. -Qed. - Lemma transl_expr_Ecall_correct: forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) (sig : signature) (a : Csharpminor.expr) (bl : Csharpminor.exprlist) - (m1 m2 m3 : mem) (vf : val) (vargs : list val) (vres : val) - (f : Csharpminor.function), - Csharpminor.eval_expr prog le e m a m1 vf -> - eval_expr_prop le e m a m1 vf -> - Csharpminor.eval_exprlist prog le e m1 bl m2 vargs -> - eval_exprlist_prop le e m1 bl m2 vargs -> + (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.fn_sig f = sig -> - Csharpminor.eval_funcall prog m2 f vargs m3 vres -> - eval_funcall_prop m2 f vargs m3 vres -> - eval_expr_prop le e m (Csharpminor.Ecall sig a bl) m3 vres. + 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. - generalize (H0 _ _ _ _ _ _ _ _ _ _ EQ LINJ MINJ MATCH). + exploit H0; eauto. intros [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. - assert (LINJ1: val_list_inject f2 le tle). eapply val_list_inject_incr; eauto. - generalize (H2 _ _ _ _ _ _ _ _ _ _ EQ0 LINJ1 MINJ1 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 _ H8 _ H7). intro. + 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]. - generalize (H6 _ _ _ _ _ TRF MINJ2 MATCH2 VINJ2). + 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_transl_function; auto. + 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) (m1 : mem) (v1 : val) (m2 : mem) - (v2 : val), - Csharpminor.eval_expr prog le e m a m1 v1 -> - eval_expr_prop le e m a m1 v1 -> + (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 m2 v2 -> - eval_expr_prop le e m1 b m2 v2 -> - eval_expr_prop le e m (Csharpminor.Econdition a b c) m2 v2. + 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. - destruct (H0 _ _ _ _ _ _ _ _ _ _ EQ LINJ MINJ MATCH) - as [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. - assert (LINJ1: val_list_inject f2 le tle). eapply val_list_inject_incr; eauto. - destruct (H3 _ _ _ _ _ _ _ _ _ _ EQ0 LINJ1 MINJ1 MATCH1) - as [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]]. + 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 <- H5. eapply eval_conditionalexpr_true; eauto. + 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) (m1 : mem) (v1 : val) (m2 : mem) - (v2 : val), - Csharpminor.eval_expr prog le e m a m1 v1 -> - eval_expr_prop le e m a m1 v1 -> + (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 m2 v2 -> - eval_expr_prop le e m1 c m2 v2 -> - eval_expr_prop le e m (Csharpminor.Econdition a b c) m2 v2. + 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. - destruct (H0 _ _ _ _ _ _ _ _ _ _ EQ LINJ MINJ MATCH) - as [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. - assert (LINJ1: val_list_inject f2 le tle). eapply val_list_inject_incr; eauto. - destruct (H3 _ _ _ _ _ _ _ _ _ _ EQ1 LINJ1 MINJ1 MATCH1) - as [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]]. + 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 <- H5. eapply eval_conditionalexpr_false; eauto. + 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) (m1 : mem) (v1 : val) (m2 : mem) (v2 : val), - Csharpminor.eval_expr prog le e m a m1 v1 -> - eval_expr_prop le e m a m1 v1 -> - Csharpminor.eval_expr prog (v1 :: le) e m1 b m2 v2 -> - eval_expr_prop (v1 :: le) e m1 b m2 v2 -> - eval_expr_prop le e m (Csharpminor.Elet a b) m2 v2. + (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. - destruct (H0 _ _ _ _ _ _ _ _ _ _ EQ LINJ MINJ MATCH) - as [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]]. - assert (LINJ1: val_list_inject f2 (v1 :: le) (tv1 :: tle)). - constructor. auto. eapply val_list_inject_incr; eauto. - destruct (H2 _ _ _ _ _ _ _ _ _ _ EQ0 LINJ1 MINJ1 MATCH1) - as [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]]. + 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. @@ -2089,19 +2061,46 @@ 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) m v. + eval_expr_prop le e m (Csharpminor.Eletvar n) E0 m v. Proof. intros; red; intros. monadInv TR. - destruct (val_list_inject_nth _ _ _ LINJ _ _ H) - as [tv [A B]]. + 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 m nil. + 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). @@ -2110,50 +2109,55 @@ Qed. Lemma transl_exprlist_Econs_correct: forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (a : Csharpminor.expr) (bl : Csharpminor.exprlist) (m1 : mem) - (v : val) (m2 : mem) (vl : list val), - Csharpminor.eval_expr prog le e m a m1 v -> - eval_expr_prop le e m a m1 v -> - Csharpminor.eval_exprlist prog le e m1 bl m2 vl -> - eval_exprlist_prop le e m1 bl m2 vl -> - eval_exprlist_prop le e m (Csharpminor.Econs a bl) m2 (v :: vl). + (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. - destruct (H0 _ _ _ _ _ _ _ _ _ _ EQ LINJ MINJ MATCH) - as [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - assert (LINJ2: val_list_inject f2 le tle). eapply val_list_inject_incr; eauto. - destruct (H2 _ _ _ _ _ _ _ _ _ _ EQ0 LINJ2 MINJ2 MATCH2) - as [f3 [te3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. - assert (VINJ1': val_inject f3 v tv1). eapply val_inject_incr; eauto. + 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_correct: +Lemma transl_funcall_internal_correct: forall (m : mem) (f : Csharpminor.function) (vargs : list val) - (e : Csharpminor.env) (m1 : mem) (lb : list block) (m2 m3 : mem) - (out : Csharpminor.outcome) (vres : 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) m3 out -> - exec_stmt_prop e m2 (Csharpminor.fn_body f) m3 out -> + 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 f vargs (free_list m3 lb) vres. + eval_funcall_prop m (Internal f) vargs t (free_list m3 lb) vres. Proof. intros; red. intros tfn f1 tm; intros. - unfold transl_function in TR. + 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. - destruct (function_entry_ok _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - H0 H1 MATCH CENV z ALLOC ARGSINJ MINJ H) - as [f2 [te2 [tm2 [STOREPARAM [MINJ2 [INCR12 [MATCH2 BLOCKS]]]]]]]. - destruct (H3 _ _ _ _ _ _ _ _ _ EQ MINJ2 MATCH2) - as [f3 [te3 [tm3 [tout [EXECBODY [OUTINJ [MINJ3 [INCR23 MATCH3]]]]]]]]. + 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). @@ -2167,13 +2171,14 @@ Proof. destruct (sig_res (Csharpminor.fn_sig f)); intro. exists v2; split. auto. subst vres; auto. contradiction. - elim H5; clear H5; intros tvres [TOUT VINJRES]. + 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 te2 tm2. + apply exec_Sseq_continue with E0 te2 tm2 t. exact STOREPARAM. eexact EXECBODY. + traceEq. (* val_inject *) split. assumption. (* mem_inject *) @@ -2190,9 +2195,22 @@ Proof. 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 m Csharpminor.Out_normal. + 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. @@ -2201,33 +2219,90 @@ Qed. Lemma transl_stmt_Sexpr_correct: forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (m1 : mem) (v : val), - Csharpminor.eval_expr prog nil e m a m1 v -> - eval_expr_prop nil e m a m1 v -> - exec_stmt_prop e m (Csharpminor.Sexpr a) m1 Csharpminor.Out_normal. + (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. - destruct (H0 _ _ _ _ _ _ _ _ _ _ EQ (val_nil_inject f1) MINJ MATCH) - as [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + 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) - (m1 m2 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m s1 m1 Csharpminor.Out_normal -> - exec_stmt_prop e m s1 m1 Csharpminor.Out_normal -> - Csharpminor.exec_stmt prog e m1 s2 m2 out -> - exec_stmt_prop e m1 s2 m2 out -> - exec_stmt_prop e m (Csharpminor.Sseq s1 s2) m2 out. + (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. - destruct (H0 _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - destruct (H2 _ _ _ _ _ _ _ _ _ EQ0 MINJ2 MATCH2) - as [f3 [te3 [tm3 [tout2 [EXEC2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. + 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. @@ -2236,15 +2311,15 @@ Qed. Lemma transl_stmt_Sseq_stop_correct: forall (e : Csharpminor.env) (m : mem) (s1 s2 : Csharpminor.stmt) - (m1 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m s1 m1 out -> - exec_stmt_prop e m s1 m1 out -> + (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) m1 out. + exec_stmt_prop e m (Csharpminor.Sseq s1 s2) t1 m1 out. Proof. intros; red; intros; monadInv TR. - destruct (H0 _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + 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. @@ -2252,64 +2327,70 @@ Qed. Lemma transl_stmt_Sifthenelse_true_correct: forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (sl1 sl2 : Csharpminor.stmt) (m1 : mem) (v1 : val) (m2 : mem) - (out : Csharpminor.outcome), - Csharpminor.eval_expr prog nil e m a m1 v1 -> - eval_expr_prop nil e m a m1 v1 -> + (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 m2 out -> - exec_stmt_prop e m1 sl1 m2 out -> - exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) m2 out. + 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. - destruct (H0 _ _ _ _ _ _ _ _ _ _ EQ (val_nil_inject f1) MINJ MATCH) - as [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - destruct (H3 _ _ _ _ _ _ _ _ _ EQ0 MINJ2 MATCH2) - as [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]]. + 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. eapply exec_ifthenelse_true; eauto. + 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) (m1 : mem) (v1 : val) (m2 : mem) - (out : Csharpminor.outcome), - Csharpminor.eval_expr prog nil e m a m1 v1 -> - eval_expr_prop nil e m a m1 v1 -> + (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 m2 out -> - exec_stmt_prop e m1 sl2 m2 out -> - exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) m2 out. + 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. - destruct (H0 _ _ _ _ _ _ _ _ _ _ EQ (val_nil_inject f1) MINJ MATCH) - as [f2 [te2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - destruct (H3 _ _ _ _ _ _ _ _ _ EQ1 MINJ2 MATCH2) - as [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]]. + 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. eapply exec_ifthenelse_false; eauto. + 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) - (m1 m2 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m sl m1 Csharpminor.Out_normal -> - exec_stmt_prop e m sl m1 Csharpminor.Out_normal -> - Csharpminor.exec_stmt prog e m1 (Csharpminor.Sloop sl) m2 out -> - exec_stmt_prop e m1 (Csharpminor.Sloop sl) m2 out -> - exec_stmt_prop e m (Csharpminor.Sloop sl) m2 out. + (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. - destruct (H0 _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - destruct (H2 _ _ _ _ _ _ _ _ _ TR MINJ2 MATCH2) - as [f3 [te3 [tm3 [tout2 [EVAL2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. + 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. @@ -2317,18 +2398,17 @@ Proof. eapply inject_incr_trans; eauto. Qed. - Lemma transl_stmt_Sloop_exit_correct: forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) - (m1 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m sl m1 out -> - exec_stmt_prop e m sl m1 out -> + (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) m1 out. + exec_stmt_prop e m (Csharpminor.Sloop sl) t1 m1 out. Proof. intros; red; intros. monadInv TR. - destruct (H0 _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + 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. @@ -2336,15 +2416,15 @@ Qed. Lemma transl_stmt_Sblock_correct: forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) - (m1 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m sl m1 out -> - exec_stmt_prop e m sl m1 out -> - exec_stmt_prop e m (Csharpminor.Sblock sl) m1 + (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. - destruct (H0 _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. + 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. @@ -2356,7 +2436,7 @@ Qed. Lemma transl_stmt_Sexit_correct: forall (e : Csharpminor.env) (m : mem) (n : nat), - exec_stmt_prop e m (Csharpminor.Sexit n) m (Csharpminor.Out_exit n). + 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). @@ -2366,15 +2446,15 @@ Qed. Lemma transl_stmt_Sswitch_correct: forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) (cases : list (int * nat)) (default : nat) - (m1 : mem) (n : int), - Csharpminor.eval_expr prog nil e m a m1 (Vint n) -> - eval_expr_prop nil e m a m1 (Vint n) -> - exec_stmt_prop e m (Csharpminor.Sswitch a cases default) m1 + (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. - destruct (H0 _ _ _ _ _ _ _ _ _ _ EQ (val_nil_inject f1) MINJ MATCH) - as [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]]. + 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. @@ -2383,7 +2463,7 @@ Qed. Lemma transl_stmt_Sreturn_none_correct: forall (e : Csharpminor.env) (m : mem), - exec_stmt_prop e m (Csharpminor.Sreturn None) m + exec_stmt_prop e m (Csharpminor.Sreturn None) E0 m (Csharpminor.Out_return None). Proof. intros; red; intros. monadInv TR. @@ -2393,15 +2473,15 @@ Qed. Lemma transl_stmt_Sreturn_some_correct: forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (m1 : mem) (v : val), - Csharpminor.eval_expr prog nil e m a m1 v -> - eval_expr_prop nil e m a m1 v -> - exec_stmt_prop e m (Csharpminor.Sreturn (Some a)) m1 + (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. - destruct (H0 _ _ _ _ _ _ _ _ _ _ EQ (val_nil_inject f1) MINJ MATCH) - as [f2 [te2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]]. + 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. @@ -2410,9 +2490,9 @@ Qed. evaluation derivation, using the lemmas above for each case. *) Lemma transl_function_correct: - forall m1 f vargs m2 vres, - Csharpminor.eval_funcall prog m1 f vargs m2 vres -> - eval_funcall_prop m1 f vargs m2 vres. + 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 @@ -2421,21 +2501,23 @@ Proof exec_stmt_prop transl_expr_Evar_correct - transl_expr_Eassign_correct transl_expr_Eaddrof_correct transl_expr_Eop_correct transl_expr_Eload_correct - transl_expr_Estore_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_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 @@ -2472,11 +2554,11 @@ Qed. follows. *) Theorem transl_program_correct: - forall n, - Csharpminor.exec_program prog (Vint n) -> - exec_program tprog (Vint n). + forall t n, + Csharpminor.exec_program prog t (Vint n) -> + exec_program tprog t (Vint n). Proof. - intros n [b [fn [m [FINDS [FINDF [SIG EVAL]]]]]]. + 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). @@ -2488,26 +2570,25 @@ Proof. split. auto. constructor. compute. split; congruence. left; auto. intros; omega. - generalize (Genv.initmem_undef (program_of_program prog) b0). fold m0. intros [lo [hi EQ]]. - rewrite EQ. simpl. constructor. + 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. - destruct (transl_function_correct _ _ _ _ _ EVAL - _ _ _ _ _ TR MINJ0 MATCH0 (val_nil_inject f)) - as [f1 [tm1 [tres [TEVAL [VINJ [MINJ1 [INCR MATCH1]]]]]]]. + 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_function gce). assumption. + apply transform_partial_program_main with (transl_fundef gce). assumption. reflexivity. split. assumption. - split. rewrite <- SIG. apply sig_transl_function; auto. - rewrite (Genv.init_mem_transf_partial (transl_function gce) _ TRANSL). + split. rewrite <- SIG. apply sig_preserved; auto. + rewrite (Genv.init_mem_transf_partial (transl_fundef gce) _ TRANSL). inversion VINJ; subst tres. assumption. Qed. |