diff options
Diffstat (limited to 'cfrontend/Cshmgenproof3.v')
| -rw-r--r-- | cfrontend/Cshmgenproof3.v | 1921 |
1 files changed, 869 insertions, 1052 deletions
diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index af6dc90a..92a09562 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -41,6 +41,8 @@ Hypothesis TRANSL: transl_program prog = OK tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. +Let tgvare : gvarenv := global_var_env tprog. +Let tgve := (tge, tgvare). Lemma symbols_preserved: forall s, Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -80,6 +82,17 @@ Proof. assumption. Qed. +Lemma sig_translated: + forall fd tfd targs tres, + classify_fun (type_of_fundef fd) = fun_case_f targs tres -> + transl_fundef fd = OK tfd -> + funsig tfd = signature_of_type targs tres. +Proof. + intros. destruct fd; monadInv H0; inv H. + monadInv EQ. simpl. auto. + simpl. auto. +Qed. + (** * Matching between environments *) (** In this section, we define a matching relation between @@ -95,9 +108,15 @@ Definition match_var_kind (ty: type) (vk: var_kind) : Prop := Record match_env (tyenv: typenv) (e: Csem.env) (te: Csharpminor.env) : Prop := mk_match_env { me_local: - forall id b ty, - e!id = Some b -> tyenv!id = Some ty -> - exists vk, match_var_kind ty vk /\ te!id = Some (b, vk); + forall id b, + e!id = Some b -> + exists vk, exists ty, + tyenv!id = Some ty + /\ match_var_kind ty vk + /\ te!id = Some (b, vk); + me_local_inv: + forall id b vk, + te!id = Some (b, vk) -> e!id = Some b; me_global: forall id ty, e!id = None -> tyenv!id = Some ty -> @@ -105,6 +124,66 @@ Record match_env (tyenv: typenv) (e: Csem.env) (te: Csharpminor.env) : Prop := (forall chunk, access_mode ty = By_value chunk -> (global_var_env tprog)!id = Some (Vscalar chunk)) }. + +Lemma match_env_same_blocks: + forall tyenv e te, + match_env tyenv e te -> + forall b, In b (Csem.blocks_of_env e) <-> In b (blocks_of_env te). +Proof. + intros. inv H. + unfold Csem.blocks_of_env, blocks_of_env. + set (f := (fun id_b_lv : positive * (block * var_kind) => + let (_, y) := id_b_lv in let (b0, _) := y in b0)). + split; intros. + exploit list_in_map_inv; eauto. intros [[id b'] [A B]]. + simpl in A; subst b'. + exploit (me_local0 id b). apply PTree.elements_complete; auto. + intros [vk [ty [C [D E]]]]. + change b with (f (id, (b, vk))). + apply List.in_map. apply PTree.elements_correct. auto. + exploit list_in_map_inv; eauto. intros [[id [b' vk]] [A B]]. + simpl in A; subst b'. + exploit (me_local_inv0 id b vk). apply PTree.elements_complete; auto. + intro. + change b with (snd (id, b)). + apply List.in_map. apply PTree.elements_correct. auto. +Qed. + +Remark free_list_charact: + forall l m, + free_list m l = + mkmem (fun b => if In_dec eq_block b l then empty_block 0 0 else m.(blocks) b) + m.(nextblock) + m.(nextblock_pos). +Proof. + induction l; intros; simpl. + destruct m; simpl. decEq. apply extensionality. auto. + rewrite IHl. unfold free; simpl. decEq. apply extensionality; intro b. + unfold update. destruct (eq_block a b). + subst b. apply zeq_true. + rewrite zeq_false; auto. + destruct (In_dec eq_block b l); auto. +Qed. + +Lemma mem_free_list_same: + forall m l1 l2, + (forall b, In b l1 <-> In b l2) -> + free_list m l1 = free_list m l2. +Proof. + intros. repeat rewrite free_list_charact. decEq. apply extensionality; intro b. + destruct (In_dec eq_block b l1); destruct (In_dec eq_block b l2); auto. + rewrite H in i. contradiction. + rewrite <- H in i. contradiction. +Qed. + +Lemma match_env_free_blocks: + forall tyenv e te m, + match_env tyenv e te -> + Mem.free_list m (Csem.blocks_of_env e) = Mem.free_list m (blocks_of_env te). +Proof. + intros. apply mem_free_list_same. intros; eapply match_env_same_blocks; eauto. +Qed. + Definition match_globalenv (tyenv: typenv) (gv: gvarenv): Prop := forall id ty chunk, tyenv!id = Some ty -> access_mode ty = By_value chunk -> @@ -117,7 +196,8 @@ Lemma match_globalenv_match_env_empty: Proof. intros. unfold Csem.empty_env, Csharpminor.empty_env. constructor. - intros until ty. repeat rewrite PTree.gempty. congruence. + intros until b. repeat rewrite PTree.gempty. congruence. + intros until vk. rewrite PTree.gempty. congruence. intros. split. apply PTree.gempty. intros. red in H. eauto. @@ -136,13 +216,13 @@ Qed. local variables and initialization of the parameters. *) Lemma match_env_alloc_variables: - forall e1 m1 vars e2 m2 lb, - Csem.alloc_variables e1 m1 vars e2 m2 lb -> + forall e1 m1 vars e2 m2, + Csem.alloc_variables e1 m1 vars e2 m2 -> forall tyenv te1 tvars, match_env tyenv e1 te1 -> transl_vars vars = OK tvars -> exists te2, - Csharpminor.alloc_variables te1 m1 tvars te2 m2 lb + Csharpminor.alloc_variables te1 m1 tvars te2 m2 /\ match_env (Ctyping.add_vars tyenv vars) e2 te2. Proof. induction 1; intros. @@ -156,10 +236,14 @@ Proof. assert (match_env (add_var tyenv (id, ty)) (PTree.set id b1 e) te2). inversion H1. unfold te2, add_var. constructor. (* me_local *) - intros until ty0. repeat rewrite PTree.gsspec. simpl. destruct (peq id0 id); intros. - subst id0. exists vk; split. - apply match_var_kind_of_type. congruence. congruence. + intros until b. simpl. repeat rewrite PTree.gsspec. + destruct (peq id0 id); intros. + inv H3. exists vk; exists ty; intuition. + apply match_var_kind_of_type. congruence. auto. + (* me_local_inv *) + intros until vk0. repeat rewrite PTree.gsspec. + destruct (peq id0 id); intros. congruence. eauto. (* me_global *) intros until ty0. repeat rewrite PTree.gsspec. simpl. destruct (peq id0 id); intros. discriminate. @@ -167,7 +251,7 @@ Proof. destruct (IHalloc_variables _ _ _ H3 TVARS) as [te3 [ALLOC MENV]]. exists te3; split. econstructor; eauto. - rewrite (sizeof_var_kind_of_type _ _ VK). auto. + rewrite (sizeof_var_kind_of_type _ _ VK). eauto. auto. Qed. @@ -192,8 +276,9 @@ Proof. unfold store_value_of_type in H0. rewrite H4 in H0. apply bind_parameters_cons with b m1. assert (tyenv!id = Some ty). apply H2. apply in_eq. - destruct (me_local _ _ _ H3 _ _ _ H H5) as [vk [A B]]. - red in A; rewrite H4 in A. congruence. + destruct (me_local _ _ _ H3 _ _ H) as [vk [ty' [A [B C]]]]. + assert (ty' = ty) by congruence. subst ty'. + red in B; rewrite H4 in B. congruence. assumption. apply IHbind_parameters with tyenv; auto. intros. apply H2. apply in_cons; auto. @@ -326,7 +411,7 @@ Lemma var_get_correct: wt_expr tyenv (Expr (Csyntax.Evar id) ty) -> var_get id ty = OK code -> match_env tyenv e te -> - eval_expr tprog te m code v. + eval_expr tgve te m code v. Proof. intros. inversion H1; subst; clear H1. unfold load_value_of_type in H0. @@ -337,8 +422,9 @@ Proof. inversion H2; clear H2; subst. inversion H; subst; clear H. (* local variable *) - exploit me_local; eauto. intros [vk [A B]]. - red in A; rewrite ACC in A. + exploit me_local; eauto. intros [vk [ty' [A [B C]]]]. + assert (ty' = ty) by congruence. subst ty'. + red in B; rewrite ACC in B. subst vk. eapply eval_Evar. eapply eval_var_ref_local. eauto. assumption. @@ -354,7 +440,7 @@ Proof. inversion H2; clear H2; subst. inversion H; subst; clear H. (* local variable *) - exploit me_local; eauto. intros [vk [A B]]. + exploit me_local; eauto. intros [vk [ty' [A [B C]]]]. eapply eval_Eaddrof. eapply eval_var_addr_local. eauto. (* global variable *) @@ -369,14 +455,14 @@ Qed. (** Correctness of the code generated by [var_set]. *) Lemma var_set_correct: - forall e m id ty loc ofs v m' tyenv code te rhs, + forall e m id ty loc ofs v m' tyenv code te rhs f k, Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) loc ofs -> store_value_of_type ty m loc ofs v = Some m' -> wt_expr tyenv (Expr (Csyntax.Evar id) ty) -> var_set id ty rhs = OK code -> match_env tyenv e te -> - eval_expr tprog te m rhs v -> - exec_stmt tprog te m code E0 m' Out_normal. + eval_expr tgve te m rhs v -> + step tgve (State f code k te m) E0 (State f Sskip k te m'). Proof. intros. inversion H1; subst; clear H1. unfold store_value_of_type in H0. @@ -387,15 +473,16 @@ Proof. inversion H2; clear H2; subst. inversion H; subst; clear H. (* local variable *) - exploit me_local; eauto. intros [vk [A B]]. - red in A; rewrite ACC in A; subst vk. - eapply exec_Sassign. eauto. + exploit me_local; eauto. intros [vk [ty' [A [B C]]]]. + assert (ty' = ty) by congruence. subst ty'. + red in B; rewrite ACC in B; subst vk. + eapply step_assign. eauto. econstructor. eapply eval_var_ref_local. eauto. assumption. (* global variable *) exploit me_global; eauto. intros [A B]. - eapply exec_Sassign. eauto. - econstructor. eapply eval_var_ref_global. auto. - fold tge. rewrite symbols_preserved. eauto. + eapply step_assign. eauto. + econstructor. eapply eval_var_ref_global. auto. + change (fst tgve) with tge. rewrite symbols_preserved. eauto. eauto. assumption. (* access mode By_reference *) intros ACC. rewrite ACC in H0. discriminate. @@ -403,35 +490,59 @@ Proof. intros. rewrite H1 in H0; discriminate. Qed. -Lemma call_dest_set_correct: - forall e m0 lhs loc ofs m1 v m2 tyenv optid te, - Csem.eval_lvalue ge e m0 lhs loc ofs -> - store_value_of_type (typeof lhs) m1 loc ofs v = Some m2 -> +Lemma call_dest_correct: + forall e m lhs loc ofs tyenv optid te, + Csem.eval_lvalue ge e m lhs loc ofs -> wt_expr tyenv lhs -> transl_lhs_call (Some lhs) = OK optid -> match_env tyenv e te -> - exec_opt_assign tprog te m1 optid v m2. -Proof. - intros. generalize H2. simpl. caseEq (is_variable lhs). 2: congruence. - intros. inv H5. - exploit is_variable_correct; eauto. intro. - rewrite H5 in H. rewrite H5 in H1. inversion H1. subst i ty. - constructor. - generalize H0. unfold store_value_of_type. - caseEq (access_mode (typeof lhs)); intros; try discriminate. - (* access mode By_value *) - inversion H. - (* local variable *) + exists id, + optid = Some id + /\ tyenv!id = Some (typeof lhs) + /\ ofs = Int.zero + /\ match access_mode (typeof lhs) with + | By_value chunk => eval_var_ref tgve te id loc chunk + | _ => True + end. +Proof. + intros. generalize H1. simpl. caseEq (is_variable lhs); try congruence. + intros id ISV EQ. inv EQ. + exploit is_variable_correct; eauto. intro EQ. + rewrite EQ in H0. inversion H0. subst id0 ty. + exists id. split; auto. split. rewrite EQ in H0. inversion H0. auto. + rewrite EQ in H. inversion H. +(* local variable *) + split. auto. subst id0 ty l ofs. exploit me_local; eauto. - intros [vk [A B]]. red in A. rewrite H6 in A. subst vk. - econstructor. eapply eval_var_ref_local; eauto. assumption. - (* global variable *) - subst id0 ty l ofs. exploit me_global; eauto. - intros [A B]. - econstructor. eapply eval_var_ref_global; eauto. - rewrite symbols_preserved. eauto. assumption. + intros [vk [ty [A [B C]]]]. + assert (ty = typeof lhs) by congruence. rewrite <- H3. + generalize B; unfold match_var_kind. destruct (access_mode ty); auto. + intros. subst vk. apply eval_var_ref_local; auto. +(* global variable *) + split. auto. + subst id0 ty l ofs. exploit me_global; eauto. intros [A B]. + case_eq (access_mode (typeof lhs)); intros; auto. + apply eval_var_ref_global; auto. + simpl. rewrite <- H9. apply symbols_preserved. +Qed. + +Lemma set_call_dest_correct: + forall ty m loc v m' tyenv e te id, + store_value_of_type ty m loc Int.zero v = Some m' -> + match access_mode ty with + | By_value chunk => eval_var_ref tgve te id loc chunk + | _ => True + end -> + match_env tyenv e te -> + tyenv!id = Some ty -> + exec_opt_assign tgve te m (Some id) v m'. +Proof. + intros. generalize H. unfold store_value_of_type. case_eq (access_mode ty); intros; try congruence. + rewrite H3 in H0. + constructor. econstructor. eauto. auto. Qed. + (** * Proof of semantic preservation *) (** ** Semantic preservation for expressions *) @@ -441,7 +552,7 @@ Qed. << e, m, a ------------------- te, m, ta | | - t| |t + | | | | v v e, m, v ------------------- te, m, v @@ -468,19 +579,19 @@ Definition eval_expr_prop (a: Csyntax.expr) (v: val) : Prop := forall ta (WT: wt_expr tyenv a) (TR: transl_expr a = OK ta), - Csharpminor.eval_expr tprog te m ta v. + Csharpminor.eval_expr tgve te m ta v. Definition eval_lvalue_prop (a: Csyntax.expr) (b: block) (ofs: int) : Prop := forall ta (WT: wt_expr tyenv a) (TR: transl_lvalue a = OK ta), - Csharpminor.eval_expr tprog te m ta (Vptr b ofs). + Csharpminor.eval_expr tgve te m ta (Vptr b ofs). Definition eval_exprlist_prop (al: list Csyntax.expr) (vl: list val) : Prop := forall tal (WT: wt_exprlist tyenv al) (TR: transl_exprlist al = OK tal), - Csharpminor.eval_exprlist tprog te m tal vl. + Csharpminor.eval_exprlist tgve te m tal vl. (* Check (eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop). *) @@ -687,7 +798,8 @@ Lemma transl_Evar_local_correct: eval_lvalue_prop (Expr (Csyntax.Evar id) ty) l Int.zero. Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. - exploit (me_local _ _ _ MENV); eauto. intros [vk [A B]]. + exploit (me_local _ _ _ MENV); eauto. + intros [vk [ty' [A [B C]]]]. econstructor. eapply eval_var_addr_local. eauto. Qed. @@ -805,1068 +917,773 @@ Qed. End EXPR. -(** ** Semantic preservation for statements *) - -(** The simulation diagrams for terminating statements and function - calls are of the following form: - relies on simulation diagrams of the following form: -<< - e, m1, s ------------------- te, m1, ts - | | - t| |t - | | - v v - e, m2, out ----------------- te, m2, tout ->> - Left: execution of statement [s] in Clight. - Right: execution of its translation [ts] in Csharpminor. - Top (precondition): matching between environments [e], [te], - plus well-typedness of statement [s]. - Bottom (postcondition): the outcomes [out] and [tout] are - related per the following function [transl_outcome]. -*) - -Definition transl_outcome (nbrk ncnt: nat) (out: Csem.outcome): Csharpminor.outcome := - match out with - | Csem.Out_normal => Csharpminor.Out_normal - | Csem.Out_break => Csharpminor.Out_exit nbrk - | Csem.Out_continue => Csharpminor.Out_exit ncnt - | Csem.Out_return vopt => Csharpminor.Out_return vopt - end. - -Definition exec_stmt_prop - (e: Csem.env) (m1: mem) (s: Csyntax.statement) (t: trace) - (m2: mem) (out: Csem.outcome) : Prop := - forall tyenv nbrk ncnt ts te - (WT: wt_stmt tyenv s) - (TR: transl_statement nbrk ncnt s = OK ts) - (MENV: match_env tyenv e te), - Csharpminor.exec_stmt tprog te m1 ts t m2 (transl_outcome nbrk ncnt out). - -Definition exec_lblstmts_prop - (e: Csem.env) (m1: mem) (s: Csyntax.labeled_statements) - (t: trace) (m2: mem) (out: Csem.outcome) : Prop := - forall tyenv nbrk ncnt body ts te m0 t0 - (WT: wt_lblstmts tyenv s) - (TR: transl_lblstmts (lblstmts_length s) - (1 + lblstmts_length s + ncnt) - s body = OK ts) - (MENV: match_env tyenv e te) - (BODY: Csharpminor.exec_stmt tprog te m0 body t0 m1 Out_normal), - Csharpminor.exec_stmt tprog te m0 ts (t0 ** t) m2 - (transl_outcome nbrk ncnt (outcome_switch out)). - -Definition eval_funcall_prop - (m1: mem) (f: Csyntax.fundef) (params: list val) - (t: trace) (m2: mem) (res: val) : Prop := - forall tf - (WT: wt_fundef (global_typenv prog) f) - (TR: transl_fundef f = OK tf), - Csharpminor.eval_funcall tprog m1 tf params t m2 res. - -(* -Type Printing Depth 100. -Check (Csem.eval_funcall_ind3 ge exec_stmt_prop exec_lblstmts_prop eval_funcall_prop). -*) - -Lemma transl_Sskip_correct: - (forall (e : Csem.env) (m : mem), - exec_stmt_prop e m Csyntax.Sskip E0 m Csem.Out_normal). -Proof. - intros; red; intros. monadInv TR. simpl. constructor. -Qed. - -Lemma transl_Sassign_correct: - forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (loc : block) - (ofs : int) (v2 : val) (m' : mem), - eval_lvalue ge e m a1 loc ofs -> - Csem.eval_expr ge e m a2 v2 -> - store_value_of_type (typeof a1) m loc ofs v2 = Some m' -> - exec_stmt_prop e m (Csyntax.Sassign a1 a2) E0 m' Csem.Out_normal. -Proof. - intros; red; intros. - inversion WT; subst; clear WT. - simpl in TR. - caseEq (is_variable a1). - (* a = variable id *) - intros id ISVAR. rewrite ISVAR in TR. - generalize (is_variable_correct _ _ ISVAR). intro EQ. - rewrite EQ in H; rewrite EQ in H4. - monadInv TR. - eapply var_set_correct; eauto. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. - (* a is not a variable *) - intro ISVAR; rewrite ISVAR in TR. monadInv TR. - eapply make_store_correct; eauto. - eapply (transl_lvalue_correct _ _ _ _ MENV _ _ _ H); eauto. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. -Qed. - -Lemma transl_Scall_None_correct: - forall (e : Csem.env) (m : mem) (a : Csyntax.expr) - (al : list Csyntax.expr) (vf : val) (vargs : list val) - (f : Csyntax.fundef) (t : trace) (m' : mem) (vres : val), - Csem.eval_expr ge e m a vf -> - Csem.eval_exprlist ge e m al vargs -> - Genv.find_funct ge vf = Some f -> - type_of_fundef f = typeof a -> - Csem.eval_funcall ge m f vargs t m' vres -> - eval_funcall_prop m f vargs t m' vres -> - exec_stmt_prop e m (Csyntax.Scall None a al) t m' Csem.Out_normal. -Proof. - intros; red; intros; simpl. - inv WT. simpl in TR. - caseEq (classify_fun (typeof a)); intros; rewrite H5 in TR; monadInv TR. - exploit functions_translated; eauto. intros [tf [TFIND TFD]]. - econstructor. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto. - eapply (transl_exprlist_correct _ _ _ _ MENV _ _ H0); eauto. - eauto. - eapply transl_fundef_sig1; eauto. rewrite H2; auto. - eapply H4; eauto. - eapply functions_well_typed; eauto. - constructor. -Qed. - -Lemma transl_Scall_Some_correct: - forall (e : Csem.env) (m : mem) (lhs a : Csyntax.expr) - (al : list Csyntax.expr) (loc : block) (ofs : int) (vf : val) - (vargs : list val) (f : Csyntax.fundef) (t : trace) (m' : mem) - (vres : val) (m'' : mem), - eval_lvalue ge e m lhs loc ofs -> - Csem.eval_expr ge e m a vf -> - Csem.eval_exprlist ge e m al vargs -> - Genv.find_funct ge vf = Some f -> - type_of_fundef f = typeof a -> - Csem.eval_funcall ge m f vargs t m' vres -> - eval_funcall_prop m f vargs t m' vres -> - store_value_of_type (typeof lhs) m' loc ofs vres = Some m'' -> - exec_stmt_prop e m (Csyntax.Scall (Some lhs) a al) t m'' Csem.Out_normal. -Proof. - intros; red; intros; simpl. - inv WT. inv H10. unfold transl_statement in TR. - caseEq (classify_fun (typeof a)); intros; rewrite H7 in TR; monadInv TR. - exploit functions_translated; eauto. intros [tf [TFIND TFD]]. - econstructor. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. - eapply (transl_exprlist_correct _ _ _ _ MENV _ _ H1); eauto. - eauto. - eapply transl_fundef_sig1; eauto. rewrite H3; auto. - eapply H5; eauto. - eapply functions_well_typed; eauto. - eapply call_dest_set_correct; eauto. -Qed. - -Lemma transl_Ssequence_1_correct: - (forall (e : Csem.env) (m : mem) (s1 s2 : statement) (t1 : trace) - (m1 : mem) (t2 : trace) (m2 : mem) (out : Csem.outcome), - Csem.exec_stmt ge e m s1 t1 m1 Csem.Out_normal -> - exec_stmt_prop e m s1 t1 m1 Csem.Out_normal -> - Csem.exec_stmt ge e m1 s2 t2 m2 out -> - exec_stmt_prop e m1 s2 t2 m2 out -> - exec_stmt_prop e m (Ssequence s1 s2) (t1 ** t2) m2 out). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - red in H0; simpl in H0. eapply exec_Sseq_continue; eauto. -Qed. - -Lemma transl_Ssequence_2_correct: - (forall (e : Csem.env) (m : mem) (s1 s2 : statement) (t1 : trace) - (m1 : mem) (out : Csem.outcome), - Csem.exec_stmt ge e m s1 t1 m1 out -> - exec_stmt_prop e m s1 t1 m1 out -> - out <> Csem.Out_normal -> - exec_stmt_prop e m (Ssequence s1 s2) t1 m1 out). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - eapply exec_Sseq_stop; eauto. - destruct out; simpl; congruence. -Qed. - -Lemma transl_Sifthenelse_true_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) - (s1 s2 : statement) (v1 : val) (t : trace) (m' : mem) - (out : Csem.outcome), - Csem.eval_expr ge e m a v1 -> - is_true v1 (typeof a) -> - Csem.exec_stmt ge e m s1 t m' out -> - exec_stmt_prop e m s1 t m' out -> - exec_stmt_prop e m (Csyntax.Sifthenelse a s1 s2) t m' out). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - exploit make_boolean_correct_true. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto. - eauto. - intros [vb [EVAL ISTRUE]]. - eapply exec_Sifthenelse; eauto. apply Val.bool_of_true_val; eauto. simpl; eauto. -Qed. - -Lemma transl_Sifthenelse_false_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) - (s1 s2 : statement) (v1 : val) (t : trace) (m' : mem) - (out : Csem.outcome), - Csem.eval_expr ge e m a v1 -> - is_false v1 (typeof a) -> - Csem.exec_stmt ge e m s2 t m' out -> - exec_stmt_prop e m s2 t m' out -> - exec_stmt_prop e m (Csyntax.Sifthenelse a s1 s2) t m' out). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - exploit make_boolean_correct_false. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto. - eauto. - intros [vb [EVAL ISFALSE]]. - eapply exec_Sifthenelse; eauto. apply Val.bool_of_false_val; eauto. simpl; eauto. -Qed. - -Lemma transl_Sreturn_none_correct: - (forall (e : Csem.env) (m : mem), - exec_stmt_prop e m (Csyntax.Sreturn None) E0 m (Csem.Out_return None)). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - simpl. apply exec_Sreturn_none. -Qed. - -Lemma transl_Sreturn_some_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (v : val), - Csem.eval_expr ge e m a v -> - exec_stmt_prop e m (Csyntax.Sreturn (Some a)) E0 m (Csem.Out_return (Some v))). -Proof. - intros; red; intros. inv WT. inv H1. monadInv TR. - simpl. eapply exec_Sreturn_some; eauto. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto. -Qed. - -Lemma transl_Sbreak_correct: - (forall (e : Csem.env) (m : mem), - exec_stmt_prop e m Sbreak E0 m Out_break). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - simpl. apply exec_Sexit. -Qed. - -Lemma transl_Scontinue_correct: - (forall (e : Csem.env) (m : mem), - exec_stmt_prop e m Scontinue E0 m Out_continue). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - simpl. apply exec_Sexit. -Qed. - Lemma exit_if_false_true: - forall a ts e m v tyenv te, + forall a ts e m v tyenv te f tk, exit_if_false a = OK ts -> Csem.eval_expr ge e m a v -> is_true v (typeof a) -> match_env tyenv e te -> wt_expr tyenv a -> - exec_stmt tprog te m ts E0 m Out_normal. + step tgve (State f ts tk te m) E0 (State f Sskip tk te m). Proof. intros. monadInv H. exploit make_boolean_correct_true. eapply (transl_expr_correct _ _ _ _ H2 _ _ H0); eauto. eauto. intros [vb [EVAL ISTRUE]]. - eapply exec_Sifthenelse with (v := vb); eauto. + change Sskip with (if true then Sskip else Sexit 0). + eapply step_ifthenelse; eauto. apply Val.bool_of_true_val; eauto. - constructor. Qed. Lemma exit_if_false_false: - forall a ts e m v tyenv te, + forall a ts e m v tyenv te f tk, exit_if_false a = OK ts -> Csem.eval_expr ge e m a v -> is_false v (typeof a) -> match_env tyenv e te -> wt_expr tyenv a -> - exec_stmt tprog te m ts E0 m (Out_exit 0). + step tgve (State f ts tk te m) E0 (State f (Sexit 0) tk te m). Proof. intros. monadInv H. exploit make_boolean_correct_false. eapply (transl_expr_correct _ _ _ _ H2 _ _ H0); eauto. eauto. intros [vb [EVAL ISFALSE]]. - eapply exec_Sifthenelse with (v := vb); eauto. + change (Sexit 0) with (if false then Sskip else Sexit 0). + eapply step_ifthenelse; eauto. apply Val.bool_of_false_val; eauto. - simpl. constructor. Qed. -Lemma transl_Swhile_false_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (s : statement) - (v : val), - Csem.eval_expr ge e m a v -> - is_false v (typeof a) -> - exec_stmt_prop e m (Swhile a s) E0 m Csem.Out_normal). -Proof. - intros; red; intros; simpl. inv WT. monadInv TR. - change Out_normal with (outcome_block (Out_exit 0)). - apply exec_Sblock. apply exec_Sloop_stop. apply exec_Sseq_stop. - eapply exit_if_false_false; eauto. congruence. congruence. -Qed. +(** ** Semantic preservation for statements *) -Lemma transl_out_break_or_return: - forall out1 out2 nbrk ncnt, - out_break_or_return out1 out2 -> - transl_outcome nbrk ncnt out2 = - outcome_block (outcome_block (transl_outcome 1 0 out1)). -Proof. - intros. inversion H; subst; reflexivity. -Qed. +(** The simulation diagram for the translation of statements and functions + is a "plus" diagram of the form +<< + I + S1 ------- R1 + | | + t | + | t + v v + S2 ------- R2 + I I +>> -Lemma transl_out_normal_or_continue: - forall out, - out_normal_or_continue out -> - Out_normal = outcome_block (transl_outcome 1 0 out). -Proof. - intros; inversion H; reflexivity. -Qed. +The invariant [I] is the [match_states] predicate that we now define. +*) -Lemma transl_Swhile_stop_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (v : val) - (s : statement) (t : trace) (m' : mem) (out' out : Csem.outcome), - Csem.eval_expr ge e m a v -> - is_true v (typeof a) -> - Csem.exec_stmt ge e m s t m' out' -> - exec_stmt_prop e m s t m' out' -> - out_break_or_return out' out -> - exec_stmt_prop e m (Swhile a s) t m' out). -Proof. - intros; red; intros. inv WT. monadInv TR. - rewrite (transl_out_break_or_return _ _ nbrk ncnt H3). - apply exec_Sblock. apply exec_Sloop_stop. - eapply exec_Sseq_continue. - eapply exit_if_false_true; eauto. - apply exec_Sblock. eauto. traceEq. - inversion H3; simpl; congruence. -Qed. +Definition typenv_fun (f: Csyntax.function) := + add_vars (global_typenv prog) (f.(Csyntax.fn_params) ++ f.(Csyntax.fn_vars)). -Lemma transl_Swhile_loop_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (s : statement) - (v : val) (t1 : trace) (m1 : mem) (out1 : Csem.outcome) - (t2 : trace) (m2 : mem) (out : Csem.outcome), - Csem.eval_expr ge e m a v -> - is_true v (typeof a) -> - Csem.exec_stmt ge e m s t1 m1 out1 -> - exec_stmt_prop e m s t1 m1 out1 -> - out_normal_or_continue out1 -> - Csem.exec_stmt ge e m1 (Swhile a s) t2 m2 out -> - exec_stmt_prop e m1 (Swhile a s) t2 m2 out -> - exec_stmt_prop e m (Swhile a s) (t1 ** t2) m2 out). -Proof. - intros; red; intros. - exploit H5; eauto. intro NEXTITER. - inv WT. monadInv TR. - inversion NEXTITER; subst. - apply exec_Sblock. - eapply exec_Sloop_loop. eapply exec_Sseq_continue. - eapply exit_if_false_true; eauto. - rewrite (transl_out_normal_or_continue _ H3). - apply exec_Sblock. eauto. - reflexivity. eassumption. - traceEq. -Qed. +Inductive match_transl: stmt -> cont -> stmt -> cont -> Prop := + | match_transl_0: forall ts tk, + match_transl ts tk ts tk + | match_transl_1: forall ts tk, + match_transl (Sblock ts) tk ts (Kblock tk). -Lemma transl_Sdowhile_false_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr) - (t : trace) (m1 : mem) (out1 : Csem.outcome) (v : val), - Csem.exec_stmt ge e m s t m1 out1 -> - exec_stmt_prop e m s t m1 out1 -> - out_normal_or_continue out1 -> - Csem.eval_expr ge e m1 a v -> - is_false v (typeof a) -> - exec_stmt_prop e m (Sdowhile a s) t m1 Csem.Out_normal). +Lemma match_transl_step: + forall ts tk ts' tk' f te m, + match_transl (Sblock ts) tk ts' tk' -> + star step tgve (State f ts' tk' te m) E0 (State f ts (Kblock tk) te m). Proof. - intros; red; intros. inv WT. monadInv TR. - simpl. - change Out_normal with (outcome_block (Out_exit 0)). - apply exec_Sblock. apply exec_Sloop_stop. eapply exec_Sseq_continue. - rewrite (transl_out_normal_or_continue out1 H1). - apply exec_Sblock. eauto. - eapply exit_if_false_false; eauto. traceEq. congruence. -Qed. + intros. inv H. + apply star_one. constructor. + apply star_refl. +Qed. + +Inductive match_cont: typenv -> nat -> nat -> Csem.cont -> Csharpminor.cont -> Prop := + | match_Kstop: forall tyenv nbrk ncnt, + match_cont tyenv nbrk ncnt Csem.Kstop Kstop + | match_Kseq: forall tyenv nbrk ncnt s k ts tk, + transl_statement nbrk ncnt s = OK ts -> + wt_stmt tyenv s -> + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv nbrk ncnt + (Csem.Kseq s k) + (Kseq ts tk) + | match_Kwhile: forall tyenv nbrk ncnt a s k ta ts tk, + exit_if_false a = OK ta -> + transl_statement 1%nat 0%nat s = OK ts -> + wt_expr tyenv a -> + wt_stmt tyenv s -> + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv 1%nat 0%nat + (Csem.Kwhile a s k) + (Kblock (Kseq (Sloop (Sseq ta (Sblock ts))) (Kblock tk))) + | match_Kdowhile: forall tyenv nbrk ncnt a s k ta ts tk, + exit_if_false a = OK ta -> + transl_statement 1%nat 0%nat s = OK ts -> + wt_expr tyenv a -> + wt_stmt tyenv s -> + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv 1%nat 0%nat + (Csem.Kdowhile a s k) + (Kblock (Kseq ta (Kseq (Sloop (Sseq (Sblock ts) ta)) (Kblock tk)))) + | match_Kfor2: forall tyenv nbrk ncnt a2 a3 s k ta2 ta3 ts tk, + exit_if_false a2 = OK ta2 -> + transl_statement nbrk ncnt a3 = OK ta3 -> + transl_statement 1%nat 0%nat s = OK ts -> + wt_expr tyenv a2 -> wt_stmt tyenv a3 -> wt_stmt tyenv s -> + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv 1%nat 0%nat + (Csem.Kfor2 a2 a3 s k) + (Kblock (Kseq ta3 (Kseq (Sloop (Sseq ta2 (Sseq (Sblock ts) ta3))) (Kblock tk)))) + | match_Kfor3: forall tyenv nbrk ncnt a2 a3 s k ta2 ta3 ts tk, + exit_if_false a2 = OK ta2 -> + transl_statement nbrk ncnt a3 = OK ta3 -> + transl_statement 1%nat 0%nat s = OK ts -> + wt_expr tyenv a2 -> wt_stmt tyenv a3 -> wt_stmt tyenv s -> + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv nbrk ncnt + (Csem.Kfor3 a2 a3 s k) + (Kseq (Sloop (Sseq ta2 (Sseq (Sblock ts) ta3))) (Kblock tk)) + | match_Kswitch: forall tyenv nbrk ncnt k tk, + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv 0%nat (S ncnt) + (Csem.Kswitch k) + (Kblock tk) + | match_Kcall_none: forall tyenv nbrk ncnt nbrk' ncnt' f e k tf te tk, + transl_function f = OK tf -> + wt_stmt (typenv_fun f) f.(Csyntax.fn_body) -> + match_env (typenv_fun f) e te -> + match_cont (typenv_fun f) nbrk' ncnt' k tk -> + match_cont tyenv nbrk ncnt + (Csem.Kcall None f e k) + (Kcall None tf te tk) + | match_Kcall_some: forall tyenv nbrk ncnt nbrk' ncnt' loc ofs ty f e k id tf te tk, + transl_function f = OK tf -> + wt_stmt (typenv_fun f) f.(Csyntax.fn_body) -> + match_env (typenv_fun f) e te -> + ofs = Int.zero -> + (typenv_fun f)!id = Some ty -> + match access_mode ty with + | By_value chunk => eval_var_ref tgve te id loc chunk + | _ => True + end -> + match_cont (typenv_fun f) nbrk' ncnt' k tk -> + match_cont tyenv nbrk ncnt + (Csem.Kcall (Some(loc, ofs, ty)) f e k) + (Kcall (Some id) tf te tk). + +Inductive match_states: Csem.state -> Csharpminor.state -> Prop := + | match_state: + forall f nbrk ncnt s k e m tf ts tk te ts' tk' + (TRF: transl_function f = OK tf) + (TR: transl_statement nbrk ncnt s = OK ts) + (MTR: match_transl ts tk ts' tk') + (WTF: wt_stmt (typenv_fun f) f.(Csyntax.fn_body)) + (WT: wt_stmt (typenv_fun f) s) + (MENV: match_env (typenv_fun f) e te) + (MK: match_cont (typenv_fun f) nbrk ncnt k tk), + match_states (Csem.State f s k e m) + (State tf ts' tk' te m) + | match_callstate: + forall fd args k m tfd tk + (TR: transl_fundef fd = OK tfd) + (WT: wt_fundef (global_typenv prog) fd) + (MK: match_cont (global_typenv prog) 0%nat 0%nat k tk) + (ISCC: Csem.is_call_cont k), + match_states (Csem.Callstate fd args k m) + (Callstate tfd args tk m) + | match_returnstate: + forall res k m tk + (MK: match_cont (global_typenv prog) 0%nat 0%nat k tk), + match_states (Csem.Returnstate res k m) + (Returnstate res tk m). + +Remark match_states_skip: + forall f e te nbrk ncnt k tf tk m, + transl_function f = OK tf -> + wt_stmt (typenv_fun f) f.(Csyntax.fn_body) -> + match_env (typenv_fun f) e te -> + match_cont (typenv_fun f) nbrk ncnt k tk -> + match_states (Csem.State f Csyntax.Sskip k e m) (State tf Sskip tk te m). +Proof. + intros. econstructor; eauto. simpl; reflexivity. constructor. constructor. +Qed. + +(** Commutation between label resolution and compilation *) + +Section FIND_LABEL. +Variable lbl: label. +Variable tyenv: typenv. -Lemma transl_Sdowhile_stop_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr) - (t : trace) (m1 : mem) (out1 out : Csem.outcome), - Csem.exec_stmt ge e m s t m1 out1 -> - exec_stmt_prop e m s t m1 out1 -> - out_break_or_return out1 out -> - exec_stmt_prop e m (Sdowhile a s) t m1 out). -Proof. - intros; red; intros. inv WT. monadInv TR. - simpl. - assert (outcome_block (transl_outcome 1 0 out1) <> Out_normal). - inversion H1; simpl; congruence. - rewrite (transl_out_break_or_return _ _ nbrk ncnt H1). - apply exec_Sblock. apply exec_Sloop_stop. - apply exec_Sseq_stop. apply exec_Sblock. eauto. - auto. auto. -Qed. +Remark exit_if_false_no_label: + forall a s, exit_if_false a = OK s -> forall k, find_label lbl s k = None. +Proof. + intros. unfold exit_if_false in H. monadInv H. simpl. auto. +Qed. + +Lemma transl_find_label: + forall s nbrk ncnt k ts tk + (WT: wt_stmt tyenv s) + (TR: transl_statement nbrk ncnt s = OK ts) + (MC: match_cont tyenv nbrk ncnt k tk), + match Csem.find_label lbl s k with + | None => find_label lbl ts tk = None + | Some (s', k') => + exists ts', exists tk', exists nbrk', exists ncnt', + find_label lbl ts tk = Some (ts', tk') + /\ transl_statement nbrk' ncnt' s' = OK ts' + /\ match_cont tyenv nbrk' ncnt' k' tk' + /\ wt_stmt tyenv s' + end + +with transl_find_label_ls: + forall ls nbrk ncnt k tls tk + (WT: wt_lblstmts tyenv ls) + (TR: transl_lbl_stmt nbrk ncnt ls = OK tls) + (MC: match_cont tyenv nbrk ncnt k tk), + match Csem.find_label_ls lbl ls k with + | None => find_label_ls lbl tls tk = None + | Some (s', k') => + exists ts', exists tk', exists nbrk', exists ncnt', + find_label_ls lbl tls tk = Some (ts', tk') + /\ transl_statement nbrk' ncnt' s' = OK ts' + /\ match_cont tyenv nbrk' ncnt' k' tk' + /\ wt_stmt tyenv s' + end. -Lemma transl_Sdowhile_loop_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr) - (m1 m2 : mem) (t1 t2 : trace) (out out1 : Csem.outcome) (v : val), - Csem.exec_stmt ge e m s t1 m1 out1 -> - exec_stmt_prop e m s t1 m1 out1 -> - out_normal_or_continue out1 -> - Csem.eval_expr ge e m1 a v -> - is_true v (typeof a) -> - Csem.exec_stmt ge e m1 (Sdowhile a s) t2 m2 out -> - exec_stmt_prop e m1 (Sdowhile a s) t2 m2 out -> - exec_stmt_prop e m (Sdowhile a s) (t1 ** t2) m2 out). Proof. - intros; red; intros. - exploit H5; eauto. intro NEXTITER. - inv WT. monadInv TR. inversion NEXTITER; subst. - apply exec_Sblock. - eapply exec_Sloop_loop. eapply exec_Sseq_continue. - rewrite (transl_out_normal_or_continue _ H1). - apply exec_Sblock. eauto. - eapply exit_if_false_true; eauto. - reflexivity. eassumption. traceEq. -Qed. + intro s; case s; intros; inv WT; try (monadInv TR); simpl. +(* skip *) + auto. +(* assign *) + simpl in TR. destruct (is_variable e); monadInv TR. + unfold var_set in EQ0. destruct (access_mode (typeof e)); inv EQ0. auto. + unfold make_store in EQ2. destruct (access_mode (typeof e)); inv EQ2. auto. +(* call *) + simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto. +(* seq *) + exploit (transl_find_label s0 nbrk ncnt (Csem.Kseq s1 k)); eauto. constructor; eauto. + destruct (Csem.find_label lbl s0 (Csem.Kseq s1 k)) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H. eapply transl_find_label; eauto. +(* ifthenelse *) + exploit (transl_find_label s0); eauto. + destruct (Csem.find_label lbl s0 k) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H. eapply transl_find_label; eauto. +(* while *) + rewrite (exit_if_false_no_label _ _ EQ). + eapply transl_find_label; eauto. econstructor; eauto. +(* dowhile *) + exploit (transl_find_label s0 1%nat 0%nat (Csem.Kdowhile e s0 k)); eauto. econstructor; eauto. + destruct (Csem.find_label lbl s0 (Kdowhile e s0 k)) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H. eapply exit_if_false_no_label; eauto. +(* for *) + simpl in TR. destruct (is_Sskip s0); monadInv TR. + simpl. rewrite (exit_if_false_no_label _ _ EQ). + exploit (transl_find_label s2 1%nat 0%nat (Kfor2 e s1 s2 k)); eauto. econstructor; eauto. + destruct (Csem.find_label lbl s2 (Kfor2 e s1 s2 k)) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H. + eapply transl_find_label; eauto. econstructor; eauto. + exploit (transl_find_label s0 nbrk ncnt (Csem.Kseq (Sfor Csyntax.Sskip e s1 s2) k)); eauto. + econstructor; eauto. simpl. rewrite is_Sskip_true. rewrite EQ1; simpl. rewrite EQ0; simpl. rewrite EQ2; simpl. reflexivity. + constructor; auto. constructor. + simpl. rewrite (exit_if_false_no_label _ _ EQ1). + destruct (Csem.find_label lbl s0 (Csem.Kseq (Sfor Csyntax.Sskip e s1 s2) k)) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H. + exploit (transl_find_label s2 1%nat 0%nat (Kfor2 e s1 s2 k)); eauto. econstructor; eauto. + destruct (Csem.find_label lbl s2 (Kfor2 e s1 s2 k)) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H0. + eapply transl_find_label; eauto. econstructor; eauto. +(* break *) + auto. +(* continue *) + auto. +(* return *) + simpl in TR. destruct o; monadInv TR. auto. auto. +(* switch *) + eapply transl_find_label_ls with (k := Csem.Kswitch k); eauto. econstructor; eauto. +(* label *) + destruct (ident_eq lbl l). + exists x; exists tk; exists nbrk; exists ncnt; auto. + eapply transl_find_label; eauto. +(* goto *) + auto. -Lemma transl_Sfor_start_correct: - (forall (e : Csem.env) (m : mem) (s a1 : statement) - (a2 : Csyntax.expr) (a3 : statement) (out : Csem.outcome) - (m1 m2 : mem) (t1 t2 : trace), - a1 <> Csyntax.Sskip -> - Csem.exec_stmt ge e m a1 t1 m1 Csem.Out_normal -> - exec_stmt_prop e m a1 t1 m1 Csem.Out_normal -> - Csem.exec_stmt ge e m1 (Sfor Csyntax.Sskip a2 a3 s) t2 m2 out -> - exec_stmt_prop e m1 (Sfor Csyntax.Sskip a2 a3 s) t2 m2 out -> - exec_stmt_prop e m (Sfor a1 a2 a3 s) (t1 ** t2) m2 out). -Proof. - intros; red; intros. - destruct (transl_stmt_Sfor_start _ _ _ _ _ _ _ TR H) as [ts1 [ts2 [EQ [TR1 TR2]]]]. - subst ts. - inv WT. - assert (WT': wt_stmt tyenv (Sfor Csyntax.Sskip a2 a3 s)). - constructor; auto. constructor. - exploit H1; eauto. simpl. intro EXEC1. - exploit H3; eauto. intro EXEC2. - eapply exec_Sseq_continue; eauto. + intro ls; case ls; intros; inv WT; monadInv TR; simpl. +(* default *) + eapply transl_find_label; eauto. +(* case *) + exploit (transl_find_label s nbrk ncnt (Csem.Kseq (seq_of_labeled_statement l) k)); eauto. + econstructor; eauto. apply transl_lbl_stmt_2; eauto. + apply wt_seq_of_labeled_statement; auto. + destruct (Csem.find_label lbl s (Csem.Kseq (seq_of_labeled_statement l) k)) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H. + eapply transl_find_label_ls; eauto. Qed. -Lemma transl_Sfor_false_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a2 : Csyntax.expr) - (a3 : statement) (v : val), - Csem.eval_expr ge e m a2 v -> - is_false v (typeof a2) -> - exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) E0 m Csem.Out_normal). -Proof. - intros; red; intros. inv WT. - rewrite transl_stmt_Sfor_not_start in TR; monadInv TR. - simpl. - change Out_normal with (outcome_block (Out_exit 0)). - apply exec_Sblock. apply exec_Sloop_stop. - apply exec_Sseq_stop. eapply exit_if_false_false; eauto. - congruence. congruence. -Qed. +End FIND_LABEL. -Lemma transl_Sfor_stop_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a2 : Csyntax.expr) - (a3 : statement) (v : val) (m1 : mem) (t : trace) - (out1 out : Csem.outcome), - Csem.eval_expr ge e m a2 v -> - is_true v (typeof a2) -> - Csem.exec_stmt ge e m s t m1 out1 -> - exec_stmt_prop e m s t m1 out1 -> - out_break_or_return out1 out -> - exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) t m1 out). -Proof. - intros; red; intros. inv WT. - rewrite transl_stmt_Sfor_not_start in TR; monadInv TR. - assert (outcome_block (transl_outcome 1 0 out1) <> Out_normal). - inversion H3; simpl; congruence. - rewrite (transl_out_break_or_return _ _ nbrk ncnt H3). - apply exec_Sblock. apply exec_Sloop_stop. - eapply exec_Sseq_continue. eapply exit_if_false_true; eauto. - apply exec_Sseq_stop. apply exec_Sblock. eauto. - auto. reflexivity. auto. -Qed. +(** Properties of call continuations *) -Lemma transl_Sfor_loop_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a2 : Csyntax.expr) - (a3 : statement) (v : val) (m1 m2 m3 : mem) (t1 t2 t3 : trace) - (out1 out : Csem.outcome), - Csem.eval_expr ge e m a2 v -> - is_true v (typeof a2) -> - Csem.exec_stmt ge e m s t1 m1 out1 -> - exec_stmt_prop e m s t1 m1 out1 -> - out_normal_or_continue out1 -> - Csem.exec_stmt ge e m1 a3 t2 m2 Csem.Out_normal -> - exec_stmt_prop e m1 a3 t2 m2 Csem.Out_normal -> - Csem.exec_stmt ge e m2 (Sfor Csyntax.Sskip a2 a3 s) t3 m3 out -> - exec_stmt_prop e m2 (Sfor Csyntax.Sskip a2 a3 s) t3 m3 out -> - exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) (t1 ** t2 ** t3) m3 out). +Lemma match_cont_call_cont: + forall nbrk' ncnt' tyenv' tyenv nbrk ncnt k tk, + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv' nbrk' ncnt' (Csem.call_cont k) (call_cont tk). Proof. - intros; red; intros. - exploit H7; eauto. intro NEXTITER. - inv WT. - rewrite transl_stmt_Sfor_not_start in TR; monadInv TR. - inversion NEXTITER; subst. - apply exec_Sblock. - eapply exec_Sloop_loop. eapply exec_Sseq_continue. - eapply exit_if_false_true; eauto. - eapply exec_Sseq_continue. - rewrite (transl_out_normal_or_continue _ H3). - apply exec_Sblock. eauto. - red in H5; simpl in H5; eauto. - reflexivity. reflexivity. eassumption. - traceEq. + induction 1; simpl; auto. + constructor. + econstructor; eauto. + econstructor; eauto. Qed. -Lemma transl_lblstmts_switch: - forall e m0 m1 n nbrk ncnt tyenv te t0 t m2 out sl body ts, - exec_stmt tprog te m0 body t0 m1 - (Out_exit (switch_target n (lblstmts_length sl) (switch_table sl 0))) -> - transl_lblstmts - (lblstmts_length sl) - (S (lblstmts_length sl + ncnt)) - sl (Sblock body) = OK ts -> - wt_lblstmts tyenv sl -> - match_env tyenv e te -> - exec_lblstmts_prop e m1 (select_switch n sl) t m2 out -> - Csharpminor.exec_stmt tprog te m0 ts (t0 ** t) m2 - (transl_outcome nbrk ncnt (outcome_switch out)). +Lemma match_cont_is_call_cont: + forall typenv nbrk ncnt k tk typenv' nbrk' ncnt', + match_cont typenv nbrk ncnt k tk -> + Csem.is_call_cont k -> + match_cont typenv' nbrk' ncnt' k tk /\ is_call_cont tk. Proof. - induction sl; intros. - simpl in H. simpl in H3. - eapply H3; eauto. - change Out_normal with (outcome_block (Out_exit 0)). - apply exec_Sblock. auto. - (* Inductive case *) - simpl in H. simpl in H3. rewrite Int.eq_sym in H3. destruct (Int.eq n i). - (* first case selected *) - eapply H3; eauto. - change Out_normal with (outcome_block (Out_exit 0)). - apply exec_Sblock. auto. - (* next case selected *) - inversion H1; clear H1; subst. - simpl in H0; monadInv H0. - eapply IHsl with (body := Sseq (Sblock body) x); eauto. - apply exec_Sseq_stop. - change (Out_exit (switch_target n (lblstmts_length sl) (switch_table sl 0))) - with (outcome_block (Out_exit (S (switch_target n (lblstmts_length sl) (switch_table sl 0))))). - apply exec_Sblock. - rewrite switch_target_table_shift in H. auto. congruence. + intros. inv H; simpl in H0; try contradiction; simpl; intuition. + constructor. + econstructor; eauto. + econstructor; eauto. Qed. -Lemma transl_Sswitch_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace) - (n : int) (sl : labeled_statements) (m1 : mem) (out : Csem.outcome), - Csem.eval_expr ge e m a (Vint n) -> - exec_lblstmts ge e m (select_switch n sl) t m1 out -> - exec_lblstmts_prop e m (select_switch n sl) t m1 out -> - exec_stmt_prop e m (Csyntax.Sswitch a sl) t m1 (outcome_switch out)). -Proof. - intros; red; intros. - inv WT. monadInv TR. - rewrite length_switch_table in EQ0. - replace (ncnt + lblstmts_length sl + 1)%nat - with (S (lblstmts_length sl + ncnt))%nat in EQ0 by omega. - change t with (E0 ** t). eapply transl_lblstmts_switch; eauto. - constructor. eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto. -Qed. +(** The simulation proof *) + +Lemma transl_step: + forall S1 t S2, Csem.step ge S1 t S2 -> + forall T1, match_states S1 T1 -> + exists T2, plus step tgve T1 t T2 /\ match_states S2 T2. +Proof. + induction 1; intros T1 MST; inv MST. + +(* assign *) + simpl in TR. inv WT. + case_eq (is_variable a1); intros. + rewrite H2 in TR. monadInv TR. + exploit is_variable_correct; eauto. intro EQ1. rewrite EQ1 in H. + assert (ts' = ts /\ tk' = tk). + inversion MTR. auto. + subst ts. unfold var_set in EQ0. destruct (access_mode (typeof a1)); congruence. + destruct H3; subst ts' tk'. + econstructor; split. + apply plus_one. eapply var_set_correct; eauto. congruence. + exploit transl_expr_correct; eauto. + eapply match_states_skip; eauto. + + rewrite H2 in TR. monadInv TR. + assert (ts' = ts /\ tk' = tk). + inversion MTR. auto. + subst ts. unfold make_store in EQ2. destruct (access_mode (typeof a1)); congruence. + destruct H3; subst ts' tk'. + econstructor; split. + apply plus_one. eapply make_store_correct; eauto. + exploit transl_lvalue_correct; eauto. + exploit transl_expr_correct; eauto. + eapply match_states_skip; eauto. + +(* call none *) + generalize TR. simpl. case_eq (classify_fun (typeof a)); try congruence. + intros targs tres CF TR'. monadInv TR'. inv MTR. inv WT. + exploit functions_translated; eauto. intros [tfd [FIND TFD]]. + econstructor; split. + apply plus_one. econstructor; eauto. + exploit transl_expr_correct; eauto. + exploit transl_exprlist_correct; eauto. + eapply sig_translated; eauto. congruence. + econstructor; eauto. eapply functions_well_typed; eauto. + econstructor; eauto. simpl. auto. + +(* call some *) + generalize TR. simpl. case_eq (classify_fun (typeof a)); try congruence. + intros targs tres CF TR'. monadInv TR'. inv MTR. inv WT. + exploit functions_translated; eauto. intros [tfd [FIND TFD]]. + inv H7. exploit call_dest_correct; eauto. + intros [id [A [B [C D]]]]. subst x ofs. + econstructor; split. + apply plus_one. econstructor; eauto. + exploit transl_expr_correct; eauto. + exploit transl_exprlist_correct; eauto. + eapply sig_translated; eauto. congruence. + econstructor; eauto. eapply functions_well_typed; eauto. + econstructor; eauto. simpl; auto. + +(* seq *) + monadInv TR. inv WT. inv MTR. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. constructor. + econstructor; eauto. -Lemma transl_LSdefault_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (t : trace) - (m1 : mem) (out : Csem.outcome), - Csem.exec_stmt ge e m s t m1 out -> - exec_stmt_prop e m s t m1 out -> - exec_lblstmts_prop e m (LSdefault s) t m1 out). -Proof. - intros; red; intros. inv WT. monadInv TR. - replace (transl_outcome nbrk ncnt (outcome_switch out)) - with (outcome_block (transl_outcome 0 (S ncnt) out)). - constructor. - eapply exec_Sseq_continue. eauto. - eapply H0; eauto. traceEq. - destruct out; simpl; auto. -Qed. +(* skip seq *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. apply step_skip_seq. + econstructor; eauto. constructor. + +(* continue seq *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl. reflexivity. constructor. + +(* break seq *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl. reflexivity. constructor. + +(* ifthenelse true *) + monadInv TR. inv MTR. inv WT. + exploit make_boolean_correct_true; eauto. + exploit transl_expr_correct; eauto. + intros [v [A B]]. + econstructor; split. + apply plus_one. apply step_ifthenelse with (v := v) (b := true). + auto. apply Val.bool_of_true_val. auto. + econstructor; eauto. constructor. + +(* ifthenelse false *) + monadInv TR. inv MTR. inv WT. + exploit make_boolean_correct_false; eauto. + exploit transl_expr_correct; eauto. + intros [v [A B]]. + econstructor; split. + apply plus_one. apply step_ifthenelse with (v := v) (b := false). + auto. apply Val.bool_of_false_val. auto. + econstructor; eauto. constructor. + +(* while false *) + monadInv TR. inv WT. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_false; eauto. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* while true *) + monadInv TR. inv WT. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_true; eauto. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. reflexivity. traceEq. + econstructor; eauto. constructor. + econstructor; eauto. -Lemma transl_LScase_fallthrough_correct: - (forall (e : Csem.env) (m : mem) (n : int) (s : statement) - (ls : labeled_statements) (t1 : trace) (m1 : mem) (t2 : trace) - (m2 : mem) (out : Csem.outcome), - Csem.exec_stmt ge e m s t1 m1 Csem.Out_normal -> - exec_stmt_prop e m s t1 m1 Csem.Out_normal -> - exec_lblstmts ge e m1 ls t2 m2 out -> - exec_lblstmts_prop e m1 ls t2 m2 out -> - exec_lblstmts_prop e m (LScase n s ls) (t1 ** t2) m2 out). -Proof. - intros; red; intros. inv WT. monadInv TR. - assert (exec_stmt tprog te m0 (Sblock (Sseq body x)) - (t0 ** t1) m1 Out_normal). - change Out_normal with - (outcome_block (transl_outcome (S (lblstmts_length ls)) - (S (S (lblstmts_length ls + ncnt))) - Csem.Out_normal)). - apply exec_Sblock. eapply exec_Sseq_continue. eexact BODY. - eapply H0; eauto. - auto. - exploit H2. eauto. simpl; eauto. eauto. eauto. simpl. - rewrite Eapp_assoc. eauto. -Qed. +(* skip or continue while *) + assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H0. inv MK. + econstructor; split. + eapply plus_left. + destruct H0; subst ts'; constructor. + apply star_one. constructor. traceEq. + econstructor; eauto. + simpl. rewrite H5; simpl. rewrite H6; simpl. reflexivity. + constructor. constructor; auto. + +(* break while *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + eapply plus_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* dowhile *) + monadInv TR. inv WT. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. traceEq. + econstructor; eauto. constructor. + econstructor; eauto. -Lemma transl_LScase_stop_correct: - (forall (e : Csem.env) (m : mem) (n : int) (s : statement) - (ls : labeled_statements) (t : trace) (m1 : mem) - (out : Csem.outcome), - Csem.exec_stmt ge e m s t m1 out -> - exec_stmt_prop e m s t m1 out -> - out <> Csem.Out_normal -> - exec_lblstmts_prop e m (LScase n s ls) t m1 out). -Proof. - intros; red; intros. inv WT. monadInv TR. - exploit H0; eauto. intro EXEC. - destruct out; simpl; simpl in EXEC. - (* out = Out_break *) - change Out_normal with (outcome_block (Out_exit 0)). - eapply transl_lblstmts_exit with (body := Sblock (Sseq body x)); eauto. - rewrite plus_0_r. - change (Out_exit (lblstmts_length ls)) - with (outcome_block (Out_exit (S (lblstmts_length ls)))). - constructor. eapply exec_Sseq_continue; eauto. - (* out = Out_continue *) - change (Out_exit ncnt) with (outcome_block (Out_exit (S ncnt))). - eapply transl_lblstmts_exit with (body := Sblock (Sseq body x)); eauto. - replace (Out_exit (lblstmts_length ls + S ncnt)) - with (outcome_block (Out_exit (S (S (lblstmts_length ls + ncnt))))). - constructor. eapply exec_Sseq_continue; eauto. - simpl. decEq. omega. - (* out = Out_normal *) - congruence. - (* out = Out_return *) - eapply transl_lblstmts_return with (body := Sblock (Sseq body x)); eauto. - change (Out_return o) - with (outcome_block (Out_return o)). - constructor. eapply exec_Sseq_continue; eauto. -Qed. +(* skip or continue dowhile false *) + assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H2. inv MK. + econstructor; split. + eapply plus_left. destruct H2; subst ts'; constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_false; eauto. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* skip or continue dowhile true *) + assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H2. inv MK. + econstructor; split. + eapply plus_left. destruct H2; subst ts'; constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_true; eauto. + apply star_one. constructor. + reflexivity. reflexivity. traceEq. + econstructor; eauto. + simpl. rewrite H7; simpl. rewrite H8; simpl. reflexivity. constructor. + constructor; auto. -Remark outcome_result_value_match: - forall out ty v nbrk ncnt, - Csem.outcome_result_value out ty v -> - Csharpminor.outcome_result_value (transl_outcome nbrk ncnt out) (opttyp_of_type ty) v. -Proof. - intros until ncnt. - destruct out; simpl; try contradiction. - destruct ty; simpl; auto. - destruct o. intros [A B]. destruct ty; simpl; congruence. - destruct ty; simpl; auto. -Qed. +(* break dowhile *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* for start *) + simpl in TR. rewrite is_Sskip_false in TR; auto. monadInv TR. inv MTR. inv WT. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. constructor. + constructor; auto. simpl. rewrite is_Sskip_true. rewrite EQ1; simpl. rewrite EQ0; simpl. rewrite EQ2; auto. + constructor; auto. constructor. + +(* for false *) + simpl in TR. rewrite is_Sskip_true in TR. monadInv TR. inv WT. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_false; eauto. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. + eapply match_states_skip; eauto. + +(* for true *) + simpl in TR. rewrite is_Sskip_true in TR. monadInv TR. inv WT. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_true; eauto. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. + econstructor; eauto. constructor. + econstructor; eauto. + +(* skip or continue for2 *) + assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H0. inv MK. + econstructor; split. + eapply plus_left. destruct H0; subst ts'; constructor. + apply star_one. constructor. reflexivity. + econstructor; eauto. constructor. + constructor; auto. + +(* break for2 *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* skip for3 *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + simpl. rewrite is_Sskip_true. rewrite H3; simpl. rewrite H4; simpl. rewrite H5; simpl. reflexivity. + constructor. constructor; auto. + +(* return none *) + monadInv TR. inv MTR. + econstructor; split. + apply plus_one. constructor. monadInv TRF. simpl. rewrite H. auto. + rewrite (match_env_free_blocks _ _ _ m MENV). econstructor; eauto. + eapply match_cont_call_cont. eauto. + +(* return some *) + monadInv TR. inv MTR. inv WT. inv H2. + econstructor; split. + apply plus_one. constructor. monadInv TRF. simpl. + unfold opttyp_of_type. destruct (fn_return f); congruence. + exploit transl_expr_correct; eauto. + rewrite (match_env_free_blocks _ _ _ m MENV). econstructor; eauto. + eapply match_cont_call_cont. eauto. + +(* skip call *) + monadInv TR. inv MTR. + exploit match_cont_is_call_cont; eauto. intros [A B]. + econstructor; split. + apply plus_one. apply step_skip_call. auto. + monadInv TRF. simpl. rewrite H0. auto. + rewrite (match_env_free_blocks _ _ _ m MENV). constructor. eauto. + +(* switch *) + monadInv TR. inv WT. + exploit transl_expr_correct; eauto. intro EV. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + apply plus_one. econstructor. eauto. traceEq. + econstructor; eauto. + apply transl_lbl_stmt_2. apply transl_lbl_stmt_1. eauto. + constructor. + apply wt_seq_of_labeled_statement. apply wt_select_switch. auto. + econstructor. eauto. + +(* skip or break switch *) + assert ((ts' = Sskip \/ ts' = Sexit nbrk) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H0. inv MK. + econstructor; split. + apply plus_one. destruct H0; subst ts'; constructor. + eapply match_states_skip; eauto. + + +(* continue switch *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl. reflexivity. constructor. + +(* label *) + monadInv TR. inv WT. inv MTR. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. constructor. + +(* goto *) + monadInv TR. inv MTR. + generalize TRF. unfold transl_function. intro TRF'. monadInv TRF'. + exploit (transl_find_label lbl). eexact WTF. eexact EQ0. eapply match_cont_call_cont. eauto. + rewrite H. + intros [ts' [tk'' [nbrk' [ncnt' [A [B [C D]]]]]]]. + econstructor; split. + apply plus_one. constructor. simpl. eexact A. + econstructor; eauto. constructor. + +(* internal function *) + monadInv TR. inv WT. inv H3. monadInv EQ. + exploit match_cont_is_call_cont; eauto. intros [A B]. + exploit match_env_alloc_variables; eauto. + apply match_globalenv_match_env_empty. apply match_global_typenv. + apply transl_fn_variables. eauto. eauto. + intros [te1 [C D]]. + econstructor; split. + apply plus_one. econstructor. + eapply transl_names_norepet; eauto. + eexact C. eapply bind_parameters_match; eauto. + econstructor; eauto. + unfold transl_function. rewrite EQ0; simpl. rewrite EQ; simpl. rewrite EQ1; auto. + constructor. -Lemma transl_funcall_internal_correct: - (forall (m : mem) (f : Csyntax.function) (vargs : list val) - (t : trace) (e : Csem.env) (m1 : mem) (lb : list block) - (m2 m3 : mem) (out : Csem.outcome) (vres : val), - Csem.alloc_variables Csem.empty_env m - (Csyntax.fn_params f ++ Csyntax.fn_vars f) e m1 lb -> - Csem.bind_parameters e m1 (Csyntax.fn_params f) vargs m2 -> - Csem.exec_stmt ge e m2 (Csyntax.fn_body f) t m3 out -> - exec_stmt_prop e m2 (Csyntax.fn_body f) t m3 out -> - Csem.outcome_result_value out (fn_return f) vres -> - eval_funcall_prop m (Internal f) vargs t (free_list m3 lb) vres). -Proof. - intros; red; intros. - (* Exploitation of typing hypothesis *) - inv WT. inv H6. - (* Exploitation of translation hypothesis *) +(* external function *) monadInv TR. - monadInv EQ. - (* Allocation of variables *) - exploit match_env_alloc_variables; eauto. - apply match_globalenv_match_env_empty. - apply match_global_typenv. - eexact (transl_fn_variables _ _ (signature_of_function f) _ _ x2 EQ0 EQ). - intros [te [ALLOCVARS MATCHENV]]. - (* Execution *) - econstructor; simpl. - (* Norepet *) - eapply transl_names_norepet; eauto. - (* Alloc *) - eexact ALLOCVARS. - (* Bind *) - eapply bind_parameters_match; eauto. - (* Execution of body *) - eapply H2; eauto. - (* Outcome_result_value *) - apply outcome_result_value_match; auto. -Qed. + exploit match_cont_is_call_cont; eauto. intros [A B]. + econstructor; split. + apply plus_one. constructor. eauto. + econstructor; eauto. -Lemma transl_funcall_external_correct: - (forall (m : mem) (id : ident) (targs : typelist) (tres : type) - (vargs : list val) (t : trace) (vres : val), - event_match (external_function id targs tres) vargs t vres -> - eval_funcall_prop m (External id targs tres) vargs t m vres). -Proof. - intros; red; intros. - monadInv TR. constructor. auto. +(* returnstate 0 *) + inv MK. + econstructor; split. + apply plus_one. constructor. constructor. + econstructor; eauto. simpl; reflexivity. constructor. constructor. + +(* returnstate 1 *) + inv MK. + econstructor; split. + apply plus_one. constructor. eapply set_call_dest_correct; eauto. + econstructor; eauto. simpl; reflexivity. constructor. constructor. +Qed. + +Lemma transl_initial_states: + forall S t S', Csem.initial_state prog S -> Csem.step ge S t S' -> + exists R, initial_state tprog R /\ match_states S R. +Proof. + intros. inv H. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + assert (C: Genv.find_symbol tge (prog_main tprog) = Some b). + rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog). + exact H1. symmetry. unfold transl_program in TRANSL. + eapply transform_partial_program2_main; eauto. + exploit function_ptr_well_typed. eauto. intro WTF. + assert (exists targs, type_of_fundef f = Tfunction targs (Tint I32 Signed)). + eapply wt_program_main. eauto. + eapply Genv.find_funct_ptr_symbol_inversion; eauto. + destruct H as [targs D]. + assert (targs = Tnil). + inv H0. inv H9. simpl in D. unfold type_of_function in D. rewrite <- H4 in D. + simpl in D. congruence. + simpl in D. inv D. inv H8. inv H. + destruct targs; simpl in H5; congruence. + subst targs. + assert (funsig tf = signature_of_type Tnil (Tint I32 Signed)). + eapply sig_translated; eauto. rewrite D; auto. + econstructor; split. + econstructor; eauto. + rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog TRANSL). + constructor; auto. constructor. exact I. Qed. -Theorem transl_funcall_correct: - forall (m : mem) (f : Csyntax.fundef) (l : list val) (t : trace) - (m0 : mem) (v : val), - Csem.eval_funcall ge m f l t m0 v -> - eval_funcall_prop m f l t m0 v. -Proof - (Csem.eval_funcall_ind3 ge - exec_stmt_prop - exec_lblstmts_prop - eval_funcall_prop - - transl_Sskip_correct - transl_Sassign_correct - transl_Scall_None_correct - transl_Scall_Some_correct - transl_Ssequence_1_correct - transl_Ssequence_2_correct - transl_Sifthenelse_true_correct - transl_Sifthenelse_false_correct - transl_Sreturn_none_correct - transl_Sreturn_some_correct - transl_Sbreak_correct - transl_Scontinue_correct - transl_Swhile_false_correct - transl_Swhile_stop_correct - transl_Swhile_loop_correct - transl_Sdowhile_false_correct - transl_Sdowhile_stop_correct - transl_Sdowhile_loop_correct - transl_Sfor_start_correct - transl_Sfor_false_correct - transl_Sfor_stop_correct - transl_Sfor_loop_correct - transl_Sswitch_correct - transl_LSdefault_correct - transl_LScase_fallthrough_correct - transl_LScase_stop_correct - transl_funcall_internal_correct - transl_funcall_external_correct). - -Theorem transl_stmt_correct: - forall (e: Csem.env) (m1: mem) (s: Csyntax.statement) (t: trace) - (m2: mem) (out: Csem.outcome), - Csem.exec_stmt ge e m1 s t m2 out -> - exec_stmt_prop e m1 s t m2 out. -Proof - (Csem.exec_stmt_ind3 ge - exec_stmt_prop - exec_lblstmts_prop - eval_funcall_prop - - transl_Sskip_correct - transl_Sassign_correct - transl_Scall_None_correct - transl_Scall_Some_correct - transl_Ssequence_1_correct - transl_Ssequence_2_correct - transl_Sifthenelse_true_correct - transl_Sifthenelse_false_correct - transl_Sreturn_none_correct - transl_Sreturn_some_correct - transl_Sbreak_correct - transl_Scontinue_correct - transl_Swhile_false_correct - transl_Swhile_stop_correct - transl_Swhile_loop_correct - transl_Sdowhile_false_correct - transl_Sdowhile_stop_correct - transl_Sdowhile_loop_correct - transl_Sfor_start_correct - transl_Sfor_false_correct - transl_Sfor_stop_correct - transl_Sfor_loop_correct - transl_Sswitch_correct - transl_LSdefault_correct - transl_LScase_fallthrough_correct - transl_LScase_stop_correct - transl_funcall_internal_correct - transl_funcall_external_correct). - -(** ** Semantic preservation for divergence *) - -Lemma transl_funcall_divergence_correct: - forall m1 f params t tf, - Csem.evalinf_funcall ge m1 f params t -> - wt_fundef (global_typenv prog) f -> - transl_fundef f = OK tf -> - Csharpminor.evalinf_funcall tprog m1 tf params t - -with transl_stmt_divergence_correct: - forall e m1 s t, - Csem.execinf_stmt ge e m1 s t -> - forall tyenv nbrk ncnt ts te - (WT: wt_stmt tyenv s) - (TR: transl_statement nbrk ncnt s = OK ts) - (MENV: match_env tyenv e te), - Csharpminor.execinf_stmt tprog te m1 ts t - -with transl_lblstmt_divergence_correct: - forall s ncnt body ts tyenv e te m0 t0 m1 t1 n, - transl_lblstmts (lblstmts_length s) - (S (lblstmts_length s + ncnt)) - s body = OK ts -> - wt_lblstmts tyenv s -> - match_env tyenv e te -> - (exec_stmt tprog te m0 body t0 m1 - (outcome_block (Out_exit - (switch_target n (lblstmts_length s) (switch_table s 0)))) - /\ execinf_lblstmts ge e m1 (select_switch n s) t1) - \/ (exec_stmt tprog te m0 body t0 m1 Out_normal - /\ execinf_lblstmts ge e m1 s t1) -> - execinf_stmt_N tprog (lblstmts_length s) te m0 ts (t0 *** t1). - +Lemma transl_final_states: + forall S R r, + match_states S R -> Csem.final_state S r -> final_state R r. Proof. - (* Functions *) - intros. inv H. - (* Exploitation of typing hypothesis *) - inv H0. inv H6. - (* Exploitation of translation hypothesis *) - monadInv H1. monadInv EQ. - (* Allocation of variables *) - assert (match_env (global_typenv prog) Csem.empty_env Csharpminor.empty_env). - apply match_globalenv_match_env_empty. apply match_global_typenv. - generalize (transl_fn_variables _ _ (signature_of_function f0) _ _ x2 EQ0 EQ). - intro. - destruct (match_env_alloc_variables _ _ _ _ _ _ H2 _ _ _ H1 H5) - as [te [ALLOCVARS MATCHENV]]. - (* Execution *) - econstructor; simpl. - eapply transl_names_norepet; eauto. - eexact ALLOCVARS. - eapply bind_parameters_match; eauto. - eapply transl_stmt_divergence_correct; eauto. - -(* Statements *) - - intros. inv H; inv WT; try (generalize TR; intro TR'; monadInv TR'). - (* Scall *) - simpl in TR. - caseEq (classify_fun (typeof a)); intros; rewrite H in TR; monadInv TR. - destruct (functions_translated _ _ H2) as [tf [TFIND TFD]]. - eapply execinf_Scall. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. - eapply (transl_exprlist_correct _ _ _ _ MENV _ _ H1); eauto. - eauto. - eapply transl_fundef_sig1; eauto. rewrite H3; auto. - eapply transl_funcall_divergence_correct; eauto. - eapply functions_well_typed; eauto. - (* Sseq 1 *) - apply execinf_Sseq_1. eapply transl_stmt_divergence_correct; eauto. - (* Sseq 2 *) - eapply execinf_Sseq_2. - change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal). - eapply (transl_stmt_correct _ _ _ _ _ _ H0); eauto. - eapply transl_stmt_divergence_correct; eauto. auto. - (* Sifthenelse, true *) - assert (eval_expr tprog te m1 x v1). - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. - destruct (make_boolean_correct_true _ _ _ _ _ _ H H1) as [vb [A B]]. - eapply execinf_Sifthenelse. eauto. apply Val.bool_of_true_val; eauto. - auto. eapply transl_stmt_divergence_correct; eauto. - (* Sifthenelse, false *) - assert (eval_expr tprog te m1 x v1). - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. - destruct (make_boolean_correct_false _ _ _ _ _ _ H H1) as [vb [A B]]. - eapply execinf_Sifthenelse. eauto. apply Val.bool_of_false_val; eauto. - auto. eapply transl_stmt_divergence_correct; eauto. - (* Swhile, body *) - apply execinf_Sblock. apply execinf_Sloop_body. - eapply execinf_Sseq_2. eapply exit_if_false_true; eauto. - apply execinf_Sblock. eapply transl_stmt_divergence_correct; eauto. traceEq. - (* Swhile, loop *) - apply execinf_Sblock. eapply execinf_Sloop_block. - eapply exec_Sseq_continue. eapply exit_if_false_true; eauto. - rewrite (transl_out_normal_or_continue out1 H3). - apply exec_Sblock. - eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto. reflexivity. - eapply transl_stmt_divergence_correct with (nbrk := 1%nat) (ncnt := 0%nat); eauto. - constructor; eauto. - traceEq. - (* Sdowhile, body *) - apply execinf_Sblock. apply execinf_Sloop_body. - apply execinf_Sseq_1. apply execinf_Sblock. - eapply transl_stmt_divergence_correct; eauto. - (* Sdowhile, loop *) - apply execinf_Sblock. eapply execinf_Sloop_block. - eapply exec_Sseq_continue. - rewrite (transl_out_normal_or_continue out1 H1). - apply exec_Sblock. - eapply (transl_stmt_correct _ _ _ _ _ _ H0); eauto. - eapply exit_if_false_true; eauto. reflexivity. - eapply transl_stmt_divergence_correct with (nbrk := 1%nat) (ncnt := 0%nat); eauto. - constructor; auto. - traceEq. - (* Sfor start 1 *) - simpl in TR. destruct (is_Sskip a1). - subst a1. inv H0. - monadInv TR. - apply execinf_Sseq_1. eapply transl_stmt_divergence_correct; eauto. - (* Sfor start 2 *) - destruct (transl_stmt_Sfor_start _ _ _ _ _ _ _ TR H0) as [ts1 [ts2 [EQ [TR1 TR2]]]]. - subst ts. - eapply execinf_Sseq_2. - change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal). - eapply (transl_stmt_correct _ _ _ _ _ _ H1); eauto. - eapply transl_stmt_divergence_correct; eauto. - constructor; auto. constructor. - auto. - (* Sfor_body *) - rewrite transl_stmt_Sfor_not_start in TR; monadInv TR. - apply execinf_Sblock. apply execinf_Sloop_body. - eapply execinf_Sseq_2. - eapply exit_if_false_true; eauto. - apply execinf_Sseq_1. apply execinf_Sblock. - eapply transl_stmt_divergence_correct; eauto. - traceEq. - (* Sfor next *) - rewrite transl_stmt_Sfor_not_start in TR; monadInv TR. - apply execinf_Sblock. apply execinf_Sloop_body. - eapply execinf_Sseq_2. - eapply exit_if_false_true; eauto. - eapply execinf_Sseq_2. - rewrite (transl_out_normal_or_continue out1 H3). - apply exec_Sblock. - eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto. - eapply transl_stmt_divergence_correct; eauto. - reflexivity. traceEq. - (* Sfor loop *) - generalize TR. rewrite transl_stmt_Sfor_not_start; intro TR'; monadInv TR'. - apply execinf_Sblock. eapply execinf_Sloop_block. - eapply exec_Sseq_continue. - eapply exit_if_false_true; eauto. - eapply exec_Sseq_continue. - rewrite (transl_out_normal_or_continue out1 H3). - apply exec_Sblock. - eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto. - change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal). - eapply (transl_stmt_correct _ _ _ _ _ _ H4); eauto. - reflexivity. reflexivity. - eapply transl_stmt_divergence_correct; eauto. - constructor; auto. - traceEq. - (* Sswitch *) - apply execinf_stutter with (lblstmts_length sl). - rewrite length_switch_table in EQ0. - replace (ncnt + lblstmts_length sl + 1)%nat - with (S (lblstmts_length sl + ncnt))%nat in EQ0 by omega. - change t with (E0 *** t). - eapply transl_lblstmt_divergence_correct; eauto. - left. split. apply exec_Sblock. constructor. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. - auto. - -(* Labeled statements *) - intros. destruct s; simpl in *; monadInv H; inv H0. - (* 1. LSdefault *) - assert (exec_stmt tprog te m0 body t0 m1 Out_normal) by tauto. - assert (execinf_lblstmts ge e m1 (LSdefault s) t1) by tauto. - clear H2. inv H0. - change (Sblock (Sseq body x)) - with ((fun z => Sblock z) (Sseq body x)). - apply execinf_context. - eapply execinf_Sseq_2. eauto. eapply transl_stmt_divergence_correct; eauto. auto. - constructor. - (* 2. LScase *) - elim H2; clear H2. - (* 2.1 searching for the case *) - rewrite (Int.eq_sym i n). - destruct (Int.eq n i). - (* 2.1.1 found it! *) - intros [A B]. inv B. - (* 2.1.1.1 we diverge because of this case *) - destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]]. - rewrite EQ1. apply execinf_context; auto. - apply execinf_Sblock. eapply execinf_Sseq_2. eauto. - eapply transl_stmt_divergence_correct; eauto. auto. - (* 2.1.1.2 we diverge later, after falling through *) - simpl. apply execinf_sleep. - replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3). - eapply transl_lblstmt_divergence_correct with (n := n); eauto. right. split. - change Out_normal with (outcome_block Out_normal). - apply exec_Sblock. - eapply exec_Sseq_continue. eauto. - change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal). - eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto. - auto. auto. traceEq. - (* 2.1.2 still searching *) - rewrite switch_target_table_shift. intros [A B]. - apply execinf_sleep. - eapply transl_lblstmt_divergence_correct with (n := n); eauto. left. split. - fold (outcome_block (Out_exit (switch_target n (lblstmts_length s0) (switch_table s0 0)))). - apply exec_Sblock. apply exec_Sseq_stop. eauto. congruence. - auto. - (* 2.2 found the case already, falling through next cases *) - intros [A B]. inv B. - (* 2.2.1 we diverge because of this case *) - destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]]. - rewrite EQ1. apply execinf_context; auto. - apply execinf_Sblock. eapply execinf_Sseq_2. eauto. - eapply transl_stmt_divergence_correct; eauto. auto. - (* 2.2.2 we diverge later *) - simpl. apply execinf_sleep. - replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3). - eapply transl_lblstmt_divergence_correct with (n := n); eauto. right. split. - change Out_normal with (outcome_block Out_normal). - apply exec_Sblock. - eapply exec_Sseq_continue. eauto. - change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal). - eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto. - auto. auto. traceEq. + intros. inv H0. inv H. inv MK. constructor. Qed. -End CORRECTNESS. - -(** Semantic preservation for whole programs. *) - Theorem transl_program_correct: - forall prog tprog beh, - transl_program prog = OK tprog -> - Ctyping.wt_program prog -> + forall (beh: program_behavior), Csem.exec_program prog beh -> Csharpminor.exec_program tprog beh. Proof. - intros. inversion H0; subst. inv H1. - (* Termination *) - assert (exists targs, type_of_fundef f = Tfunction targs (Tint I32 Signed)). - apply wt_program_main. - eapply Genv.find_funct_ptr_symbol_inversion; eauto. - elim H1; clear H1; intros targs TYP. - assert (targs = Tnil). - inv H4; simpl in TYP. - inv H5. injection TYP. rewrite <- H10. simpl. auto. - inv TYP. inv H1. - destruct targs; simpl in H4. auto. inv H4. - subst targs. - exploit function_ptr_translated; eauto. intros [tf [TFINDF TRANSLFD]]. - apply program_terminates with b tf m1. - rewrite (symbols_preserved _ _ H). - rewrite (transform_partial_program2_main transl_fundef transl_globvar prog H). auto. - auto. - generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD TYP). simpl; auto. - rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog H). - generalize (transl_funcall_correct _ _ H0 H _ _ _ _ _ _ H4). - intro. eapply H1. - eapply function_ptr_well_typed; eauto. - auto. - (* Divergence *) - assert (exists targs, type_of_fundef f = Tfunction targs (Tint I32 Signed)). - apply wt_program_main. - eapply Genv.find_funct_ptr_symbol_inversion; eauto. - elim H1; clear H1; intros targs TYP. - assert (targs = Tnil). - inv H4; simpl in TYP. - inv H5. injection TYP. rewrite <- H9. simpl. auto. - subst targs. - exploit function_ptr_translated; eauto. intros [tf [TFINDF TRANSLFD]]. - apply program_diverges with b tf. - rewrite (symbols_preserved _ _ H). - rewrite (transform_partial_program2_main transl_fundef transl_globvar prog H). auto. - auto. - generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD TYP). simpl; auto. - rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog H). - eapply transl_funcall_divergence_correct; eauto. - eapply function_ptr_well_typed; eauto. + set (order := fun (S1 S2: Csem.state) => False). + assert (transl_step': + forall S1 t S2, Csem.step ge S1 t S2 -> + forall T1, match_states S1 T1 -> + exists T2, + (plus step tgve T1 t T2 \/ star step tgve T1 t T2 /\ order S2 S1) + /\ match_states S2 T2). + intros. exploit transl_step; eauto. intros [T2 [A B]]. + exists T2; split. auto. auto. + intros. inv H. + assert (exists t1, exists s1, Csem.step (Genv.globalenv prog) s t1 s1). + inv H1. inv H0; inv H2. exists t1; exists s2; auto. + destruct H as [t1 [s1 ST]]. + exploit transl_initial_states; eauto. intros [R [A B]]. + exploit simulation_star_star; eauto. intros [R' [C D]]. + econstructor; eauto. eapply transl_final_states; eauto. + assert (exists t1, exists s1, Csem.step (Genv.globalenv prog) s t1 s1). + inv H1. exists t; exists s2; auto. + destruct H as [t1 [s1 ST]]. + exploit transl_initial_states; eauto. intros [R [A B]]. + exploit simulation_star_forever; eauto. + unfold order; red. intros. constructor; intros. contradiction. + intro C. + econstructor; eauto. Qed. + +End CORRECTNESS. |