diff options
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/Cminorgen.v | 77 | ||||
-rw-r--r-- | cfrontend/Cminorgenproof.v | 1293 | ||||
-rw-r--r-- | cfrontend/Csem.v | 477 | ||||
-rw-r--r-- | cfrontend/Csharpminor.v | 415 | ||||
-rw-r--r-- | cfrontend/Cshmgen.v | 89 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof1.v | 63 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof2.v | 182 | ||||
-rw-r--r-- | cfrontend/Cshmgenproof3.v | 1357 | ||||
-rw-r--r-- | cfrontend/Csyntax.v | 9 | ||||
-rw-r--r-- | cfrontend/Ctyping.v | 96 |
10 files changed, 2275 insertions, 1783 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index d021a63c..8596ebfa 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -79,7 +79,7 @@ Definition store_arg (chunk: memory_chunk) (e: expr) : expr := end. Definition make_store (chunk: memory_chunk) (e1 e2: expr): stmt := - Sexpr (Estore chunk e1 (store_arg chunk e2)). + Sstore chunk e1 (store_arg chunk e2). Definition make_stackaddr (ofs: Z): expr := Econst (Oaddrstack (Int.repr ofs)). @@ -160,35 +160,22 @@ Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr) | Csharpminor.Eload chunk e => do te <- transl_expr cenv e; OK (Eload chunk te) - | Csharpminor.Ecall sig e el => - do te <- transl_expr cenv e; - do tel <- transl_exprlist cenv el; - OK (Ecall sig te tel) | Csharpminor.Econdition e1 e2 e3 => do te1 <- transl_expr cenv e1; do te2 <- transl_expr cenv e2; do te3 <- transl_expr cenv e3; OK (Econdition te1 te2 te3) - | Csharpminor.Elet e1 e2 => - do te1 <- transl_expr cenv e1; - do te2 <- transl_expr cenv e2; - OK (Elet te1 te2) - | Csharpminor.Eletvar n => - OK (Eletvar n) - | Csharpminor.Ealloc e => - do te <- transl_expr cenv e; - OK (Ealloc te) - end + end. -with transl_exprlist (cenv: compilenv) (el: Csharpminor.exprlist) - {struct el}: res exprlist := +Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr) + {struct el}: res (list expr) := match el with - | Csharpminor.Enil => - OK Enil - | Csharpminor.Econs e1 e2 => + | nil => + OK nil + | e1 :: e2 => do te1 <- transl_expr cenv e1; do te2 <- transl_exprlist cenv e2; - OK (Econs te1 te2) + OK (te1 :: te2) end. (** Translation of statements. Entirely straightforward. *) @@ -198,14 +185,21 @@ Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt) match s with | Csharpminor.Sskip => OK Sskip - | Csharpminor.Sexpr e => - do te <- transl_expr cenv e; OK(Sexpr te) | Csharpminor.Sassign id e => do te <- transl_expr cenv e; var_set cenv id te | Csharpminor.Sstore chunk e1 e2 => do te1 <- transl_expr cenv e1; do te2 <- transl_expr cenv e2; OK (make_store chunk te1 te2) + | Csharpminor.Scall None sig e el => + do te <- transl_expr cenv e; + do tel <- transl_exprlist cenv el; + OK (Scall None sig te tel) + | Csharpminor.Scall (Some id) sig e el => + do te <- transl_expr cenv e; + do tel <- transl_exprlist cenv el; + do s <- var_set cenv id (Evar id); + OK (Sseq (Scall (Some id) sig te tel) s) | Csharpminor.Sseq s1 s2 => do ts1 <- transl_stmt cenv s1; do ts2 <- transl_stmt cenv s2; @@ -245,31 +239,26 @@ Fixpoint addr_taken_expr (e: Csharpminor.expr): Identset.t := | Csharpminor.Ebinop op e1 e2 => Identset.union (addr_taken_expr e1) (addr_taken_expr e2) | Csharpminor.Eload chunk e => addr_taken_expr e - | Csharpminor.Ecall sig e el => - Identset.union (addr_taken_expr e) (addr_taken_exprlist el) | Csharpminor.Econdition e1 e2 e3 => Identset.union (addr_taken_expr e1) (Identset.union (addr_taken_expr e2) (addr_taken_expr e3)) - | Csharpminor.Elet e1 e2 => - Identset.union (addr_taken_expr e1) (addr_taken_expr e2) - | Csharpminor.Eletvar n => Identset.empty - | Csharpminor.Ealloc e => addr_taken_expr e - end + end. -with addr_taken_exprlist (e: Csharpminor.exprlist): Identset.t := +Fixpoint addr_taken_exprlist (e: list Csharpminor.expr): Identset.t := match e with - | Csharpminor.Enil => Identset.empty - | Csharpminor.Econs e1 e2 => + | nil => Identset.empty + | e1 :: e2 => Identset.union (addr_taken_expr e1) (addr_taken_exprlist e2) end. Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := match s with | Csharpminor.Sskip => Identset.empty - | Csharpminor.Sexpr e => addr_taken_expr e | Csharpminor.Sassign id e => addr_taken_expr e | Csharpminor.Sstore chunk e1 e2 => Identset.union (addr_taken_expr e1) (addr_taken_expr e2) + | Csharpminor.Scall optid sig e el => + Identset.union (addr_taken_expr e) (addr_taken_exprlist el) | Csharpminor.Sseq s1 s2 => Identset.union (addr_taken_stmt s1) (addr_taken_stmt s2) | Csharpminor.Sifthenelse e s1 s2 => @@ -342,20 +331,13 @@ Definition build_global_compilenv (p: Csharpminor.program) : compilenv := Fixpoint store_parameters (cenv: compilenv) (params: list (ident * memory_chunk)) - {struct params} : stmt := + {struct params} : res stmt := match params with - | nil => Sskip + | nil => OK Sskip | (id, chunk) :: rem => - match PMap.get id cenv with - | Var_local chunk => - Sseq (Sassign id (make_cast chunk (Evar id))) - (store_parameters cenv rem) - | Var_stack_scalar chunk ofs => - Sseq (make_store chunk (make_stackaddr ofs) (Evar id)) - (store_parameters cenv rem) - | _ => - Sskip (* should never happen *) - end + do s1 <- var_set cenv id (Evar id); + do s2 <- store_parameters cenv rem; + OK (Sseq s1 s2) end. (** Translation of a Csharpminor function. We must check that the @@ -368,12 +350,13 @@ Definition transl_function let (cenv, stacksize) := build_compilenv gce f in if zle stacksize Int.max_signed then do tbody <- transl_stmt cenv f.(Csharpminor.fn_body); + do sparams <- store_parameters cenv f.(Csharpminor.fn_params); OK (mkfunction (Csharpminor.fn_sig f) (Csharpminor.fn_params_names f) (Csharpminor.fn_vars_names f) stacksize - (Sseq (store_parameters cenv f.(Csharpminor.fn_params)) tbody)) + (Sseq sparams tbody)) else Error(msg "Cminorgen: too many local variables, stack size exceeded"). Definition transl_fundef (gce: compilenv) (f: Csharpminor.fundef): res fundef := diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index 5bcb8801..ff10bb3e 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -12,6 +12,7 @@ Require Import Mem. Require Import Events. Require Import Globalenvs. Require Import Csharpminor. +Require Import Op. Require Import Cminor. Require Import Cminorgen. @@ -279,30 +280,6 @@ 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. - -Lemma load_result_idem: - forall chunk v, - Val.load_result chunk (Val.load_result chunk v) = - Val.load_result chunk v. -Proof. - destruct chunk; destruct v; simpl; auto. - rewrite Int.cast8_signed_idem; auto. - rewrite Int.cast8_unsigned_idem; auto. - rewrite Int.cast16_signed_idem; auto. - rewrite Int.cast16_unsigned_idem; auto. - rewrite Float.singleoffloat_idem; auto. -Qed. - -Lemma load_result_normalized: - forall chunk v, - val_normalized chunk v -> Val.load_result chunk v = v. -Proof. - intros chunk v [v0 EQ]. rewrite EQ. apply load_result_idem. -Qed. -*) Lemma match_env_store_local: forall f cenv e m1 m2 te sp lo hi id b chunk v tv, e!id = Some(b, Vscalar chunk) -> @@ -796,21 +773,12 @@ Qed. (** * Correctness of Cminor construction functions *) -Hint Resolve eval_Econst eval_Eunop eval_Ebinop eval_Eload: evalexpr. - Remark val_inject_val_of_bool: forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). Proof. intros; destruct b; unfold Val.of_bool, Vtrue, Vfalse; constructor. Qed. -Remark val_inject_bool_of_val: - forall f v b tv, - val_inject f v tv -> Val.bool_of_val v b -> Val.bool_of_val tv b. -Proof. - intros. inv H; inv H0; constructor; auto. -Qed. - Remark val_inject_eval_compare_null: forall f c i v, eval_compare_null c i = Some v -> @@ -822,6 +790,8 @@ Proof. discriminate. Qed. +Hint Resolve eval_Econst eval_Eunop eval_Ebinop eval_Eload: evalexpr. + Ltac TrivialOp := match goal with | [ |- exists y, _ /\ val_inject _ (Vint ?x) _ ] => @@ -838,6 +808,17 @@ Ltac TrivialOp := | _ => idtac end. +Remark eval_compare_null_inv: + forall c i v, + eval_compare_null c i = Some v -> + i = Int.zero /\ (c = Ceq /\ v = Vfalse \/ c = Cne /\ v = Vtrue). +Proof. + intros until v. unfold eval_compare_null. + predSpec Int.eq Int.eq_spec i Int.zero. + case c; intro EQ; simplify_eq EQ; intro; subst v; tauto. + congruence. +Qed. + (** Correctness of [transl_constant]. *) Lemma transl_constant_correct: @@ -865,12 +846,12 @@ Proof. inv H; inv H0; simpl; TrivialOp. inv H; inv H0; simpl; TrivialOp. inv H; inv H0; simpl; TrivialOp. - inv H0; inv H. TrivialOp. + inv H0; inv H. TrivialOp. unfold Vfalse; TrivialOp. inv H0; inv H. TrivialOp. unfold Vfalse; TrivialOp. inv H0; inv H; TrivialOp. inv H0; inv H; TrivialOp. inv H0; inv H; TrivialOp. - inv H; inv H0; simpl; TrivialOp. + inv H0; inv H; TrivialOp. inv H0; inv H; TrivialOp. inv H0; inv H; TrivialOp. inv H0; inv H; TrivialOp. @@ -950,12 +931,11 @@ Qed. normalized according to the given memory chunk. *) Lemma make_cast_correct: - forall f sp le te tm1 a t tm2 v chunk tv, - eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 tv -> + forall f sp te tm a v tv chunk, + eval_expr tge sp te tm a tv -> val_inject f v tv -> exists tv', - eval_expr tge (Vptr sp Int.zero) le - te tm1 (make_cast chunk a) t tm2 tv' + eval_expr tge sp te tm (make_cast chunk a) tv' /\ val_inject f (Val.load_result chunk v) tv'. Proof. intros. destruct chunk; simpl make_cast. @@ -983,46 +963,44 @@ Proof. Qed. Lemma make_stackaddr_correct: - forall sp le te tm ofs, - eval_expr tge (Vptr sp Int.zero) le - te tm (make_stackaddr ofs) - E0 tm (Vptr sp (Int.repr ofs)). + forall sp te tm ofs, + eval_expr tge (Vptr sp Int.zero) te tm + (make_stackaddr ofs) (Vptr sp (Int.repr ofs)). Proof. intros; unfold make_stackaddr. - econstructor. simpl. decEq. decEq. + eapply eval_Econst. simpl. decEq. decEq. rewrite Int.add_commut. apply Int.add_zero. Qed. Lemma make_globaladdr_correct: - forall sp le te tm id b, + forall sp te tm id b, Genv.find_symbol tge id = Some b -> - eval_expr tge (Vptr sp Int.zero) le - te tm (make_globaladdr id) - E0 tm (Vptr b Int.zero). + eval_expr tge (Vptr sp Int.zero) te tm + (make_globaladdr id) (Vptr b Int.zero). Proof. intros; unfold make_globaladdr. - econstructor. simpl. rewrite H. auto. + eapply eval_Econst. simpl. rewrite H. auto. Qed. (** Correctness of [make_store]. *) Lemma store_arg_content_inject: - forall f sp le te tm1 a t tm2 v va chunk, - eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 va -> + forall f sp te tm a v va chunk, + eval_expr tge sp te tm a va -> val_inject f v va -> exists vb, - eval_expr tge (Vptr sp Int.zero) le te tm1 (store_arg chunk a) t tm2 vb + eval_expr tge sp te tm (store_arg chunk a) vb /\ val_content_inject f chunk v vb. Proof. intros. assert (exists vb, - eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 vb + eval_expr tge sp te tm a vb /\ val_content_inject f chunk v vb). exists va; split. assumption. constructor. assumption. destruct a; simpl store_arg; trivial; destruct u; trivial; destruct chunk; trivial; - inv H; simpl in H12; inv H12; + inv H; simpl in H6; inv H6; econstructor; (split; [eauto|idtac]); destruct v1; simpl in H0; inv H0; try (constructor; constructor). apply val_content_inject_8. auto. apply Int.cast8_unsigned_idem. @@ -1033,47 +1011,43 @@ Proof. Qed. Lemma make_store_correct: - forall f sp te tm1 addr tm2 tvaddr rhs tm3 tvrhs - chunk vrhs m3 vaddr m4 t1 t2, - eval_expr tge (Vptr sp Int.zero) nil - te tm1 addr t1 tm2 tvaddr -> - eval_expr tge (Vptr sp Int.zero) nil - te tm2 rhs t2 tm3 tvrhs -> - Mem.storev chunk m3 vaddr vrhs = Some m4 -> - mem_inject f m3 tm3 -> + forall f sp te tm addr tvaddr rhs tvrhs chunk m vaddr vrhs m', + eval_expr tge sp te tm addr tvaddr -> + eval_expr tge sp te tm rhs tvrhs -> + Mem.storev chunk m vaddr vrhs = Some m' -> + mem_inject f m tm -> val_inject f vaddr tvaddr -> val_inject f vrhs tvrhs -> - exists tm4, - exec_stmt tge (Vptr sp Int.zero) - te tm1 (make_store chunk addr rhs) - (t1**t2) te tm4 Out_normal - /\ mem_inject f m4 tm4 - /\ nextblock tm4 = nextblock tm3. + exists tm', + exec_stmt tge sp te tm (make_store chunk addr rhs) + E0 te tm' Out_normal + /\ mem_inject f m' tm' + /\ nextblock tm' = nextblock tm. Proof. intros. unfold make_store. exploit store_arg_content_inject. eexact H0. eauto. intros [tv [EVAL VCINJ]]. exploit storev_mapped_inject_1; eauto. - intros [tm4 [STORE MEMINJ]]. - exists tm4. - split. apply exec_Sexpr with tv. eapply eval_Estore; eauto. - split. auto. + intros [tm' [STORE MEMINJ]]. + exists tm'. + split. eapply exec_Sstore; eauto. + split. auto. unfold storev in STORE; destruct tvaddr; try discriminate. eapply nextblock_store; eauto. Qed. -(** Correctness of the variable accessors [var_get], [var_set] - and [var_addr]. *) +(** Correctness of the variable accessors [var_get], [var_addr], + and [var_set]. *) Lemma var_get_correct: - forall cenv id a f e te sp lo hi m cs tm b chunk v le, + forall cenv id a f e te sp lo hi m cs tm b chunk v, var_get cenv id = OK a -> match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> mem_inject f m tm -> eval_var_ref prog e id b chunk -> load chunk m b 0 = Some v -> exists tv, - eval_expr tge (Vptr sp Int.zero) le te tm a E0 tm tv /\ + eval_expr tge (Vptr sp Int.zero) te tm a tv /\ val_inject f v tv. Proof. unfold var_get; intros. @@ -1093,7 +1067,7 @@ Proof. unfold loadv. eexact H3. intros [tv [LOAD INJ]]. exists tv; split. - econstructor; eauto. eapply make_stackaddr_correct; eauto. + eapply eval_Eload; eauto. eapply make_stackaddr_correct; eauto. auto. (* var_global_scalar *) inversion H2; [congruence|subst]. @@ -1106,17 +1080,17 @@ Proof. generalize (loadv_inject _ _ _ _ _ _ _ H1 H12 H13). intros [tv [LOAD INJ]]. exists tv; split. - econstructor; eauto. eapply make_globaladdr_correct; eauto. + eapply eval_Eload; eauto. eapply make_globaladdr_correct; eauto. auto. Qed. Lemma var_addr_correct: - forall cenv id a f e te sp lo hi m cs tm b le, + forall cenv id a f e te sp lo hi m cs tm b, match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> var_addr cenv id = OK a -> eval_var_addr prog e id b -> exists tv, - eval_expr tge (Vptr sp Int.zero) le te tm a E0 tm tv /\ + eval_expr tge (Vptr sp Int.zero) te tm a tv /\ val_inject f (Vptr b Int.zero) tv. Proof. unfold var_addr; intros. @@ -1150,62 +1124,169 @@ Proof. Qed. Lemma var_set_correct: - forall cenv id rhs a f e te sp lo hi m2 cs tm2 tm1 tv b chunk v m3 t, + forall cenv id rhs a f e te sp lo hi m cs tm tv v m', var_set cenv id rhs = OK a -> - match_callstack f (mkframe cenv e te sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2 -> - eval_expr tge (Vptr sp Int.zero) nil te tm1 rhs t tm2 tv -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> + eval_expr tge (Vptr sp Int.zero) te tm rhs tv -> val_inject f v tv -> - mem_inject f m2 tm2 -> - eval_var_ref prog e id b chunk -> - store chunk m2 b 0 v = Some m3 -> - exists te3, exists tm3, - exec_stmt tge (Vptr sp Int.zero) te 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. + mem_inject f m tm -> + exec_assign prog e m id v m' -> + exists te', exists tm', + exec_stmt tge (Vptr sp Int.zero) te tm a E0 te' tm' Out_normal /\ + mem_inject f m' tm' /\ + match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m' /\ + (forall id', id' <> id -> te'!id' = te!id'). Proof. unfold var_set; intros. - assert (NEXTBLOCK: nextblock m3 = nextblock m2). + inv H4. + assert (NEXTBLOCK: nextblock m' = nextblock m). eapply nextblock_store; eauto. - inversion H0. subst. - assert (match_var f id e m2 te sp cenv!!id). inversion H19; auto. - inversion H6; subst; rewrite <- H7 in H; inversion H; subst; clear H. + inversion H0; subst. + assert (match_var f id e m te sp cenv!!id). inversion H19; auto. + inv H4; rewrite <- H7 in H; inv H. (* var_local *) - inversion H4; [subst|congruence]. - assert (b0 = b). congruence. subst b0. - assert (chunk0 = chunk). congruence. subst chunk0. + inversion H5; [subst|congruence]. + assert (b0 = b) by congruence. subst b0. + assert (chunk0 = chunk) by congruence. subst chunk0. exploit make_cast_correct; eauto. intros [tv' [EVAL INJ]]. - exists (PTree.set id tv' te); exists tm2. + exists (PTree.set id tv' te); exists tm. split. eapply exec_Sassign. eauto. split. eapply store_unmapped_inject; eauto. - rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto. + split. rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto. + intros. apply PTree.gso; auto. (* var_stack_scalar *) + inversion H5; [subst|congruence]. + assert (b0 = b) by congruence. subst b0. + assert (chunk0 = chunk) by congruence. subst chunk0. + assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption. + exploit make_store_correct. + eapply make_stackaddr_correct. + eauto. eauto. eauto. eauto. eauto. + intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. + exists te; exists tm'. + split. auto. split. auto. + split. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. + eapply match_callstack_mapped; eauto. + inversion H9; congruence. + auto. + (* var_global_scalar *) + inversion H5; [congruence|subst]. + assert (chunk0 = chunk) by congruence. subst chunk0. + assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption. + assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. + inversion H12. destruct (mg_symbols0 _ _ H4) as [A B]. + exploit make_store_correct. + eapply make_globaladdr_correct; eauto. + eauto. eauto. eauto. eauto. eauto. + intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. + exists te; exists tm'. + split. auto. split. auto. + split. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. + eapply match_callstack_mapped; eauto. congruence. + auto. +Qed. + +Lemma match_env_extensional': + forall f cenv e m te1 sp lo hi, + match_env f cenv e m te1 sp lo hi -> + forall te2, + (forall id, + match cenv!!id with + | Var_local _ => te2!id = te1!id + | _ => True + end) -> + match_env f cenv e m te2 sp lo hi. +Proof. + induction 1; intros; econstructor; eauto. + intros. generalize (me_vars0 id); intro. + inversion H0; econstructor; eauto. + generalize (H id). rewrite <- H1. congruence. +Qed. + + +Lemma match_callstack_extensional: + forall f cenv e te1 te2 sp lo hi cs bound tbound m, + (forall id, + match cenv!!id with + | Var_local _ => te2!id = te1!id + | _ => True + end) -> + match_callstack f (mkframe cenv e te1 sp lo hi :: cs) bound tbound m -> + match_callstack f (mkframe cenv e te2 sp lo hi :: cs) bound tbound m. +Proof. + intros. inv H0. constructor; auto. + apply match_env_extensional' with te1; auto. +Qed. + +Lemma var_set_self_correct: + forall cenv id a f e te sp lo hi m cs tm tv v m', + var_set cenv id (Evar id) = OK a -> + match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> + val_inject f v tv -> + mem_inject f m tm -> + exec_assign prog e m id v m' -> + exists te', exists tm', + exec_stmt tge (Vptr sp Int.zero) (PTree.set id tv te) tm a E0 te' tm' Out_normal /\ + mem_inject f m' tm' /\ + match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m'. +Proof. + unfold var_set; intros. + inv H3. + assert (NEXTBLOCK: nextblock m' = nextblock m). + eapply nextblock_store; eauto. + inversion H0; subst. + assert (EVAR: eval_expr tge (Vptr sp Int.zero) (PTree.set id tv te) tm (Evar id) tv). + constructor. apply PTree.gss. + assert (match_var f id e m te sp cenv!!id). inversion H18; auto. + inv H3; rewrite <- H6 in H; inv H. + (* var_local *) inversion H4; [subst|congruence]. - assert (b0 = b). congruence. subst b0. - assert (chunk0 = chunk). congruence. subst chunk0. - assert (storev chunk m2 (Vptr b Int.zero) v = Some m3). assumption. + assert (b0 = b) by congruence. subst b0. + assert (chunk0 = chunk) by congruence. subst chunk0. + exploit make_cast_correct; eauto. + intros [tv' [EVAL INJ]]. + exists (PTree.set id tv' (PTree.set id tv te)); exists tm. + split. eapply exec_Sassign. eauto. + split. eapply store_unmapped_inject; eauto. + rewrite NEXTBLOCK. + apply match_callstack_extensional with (PTree.set id tv' te). + intros. destruct (cenv!!id0); auto. + repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. + eapply match_callstack_store_local; eauto. + (* var_stack_scalar *) + inversion H4; [subst|congruence]. + assert (b0 = b) by congruence. subst b0. + assert (chunk0 = chunk) by congruence. subst chunk0. + assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption. exploit make_store_correct. eapply make_stackaddr_correct. eauto. eauto. eauto. eauto. eauto. - rewrite E0_left. intros [tm3 [EVAL [MEMINJ TNEXTBLOCK]]]. - exists te; exists tm3. + intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. + exists (PTree.set id tv te); exists tm'. split. auto. split. auto. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. + apply match_callstack_extensional with te. + intros. caseEq (cenv!!id0); intros; auto. + rewrite PTree.gsspec. destruct (peq id0 id). congruence. auto. eapply match_callstack_mapped; eauto. - inversion H9; congruence. + inversion H8; congruence. (* var_global_scalar *) inversion H4; [congruence|subst]. - assert (chunk0 = chunk). congruence. subst chunk0. - assert (storev chunk m2 (Vptr b Int.zero) v = Some m3). assumption. + assert (chunk0 = chunk) by congruence. subst chunk0. + assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inversion H13. destruct (mg_symbols0 _ _ H10) as [A B]. + inversion H11. destruct (mg_symbols0 _ _ H3) 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 te; exists tm3. + intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. + exists (PTree.set id tv te); exists tm'. split. auto. split. auto. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. + apply match_callstack_extensional with te. + intros. caseEq (cenv!!id0); intros; auto. + rewrite PTree.gsspec. destruct (peq id0 id). congruence. auto. eapply match_callstack_mapped; eauto. congruence. Qed. @@ -1501,79 +1582,42 @@ Qed. Lemma store_parameters_correct: forall e m1 params vl m2, bind_parameters e m1 params vl m2 -> - forall f te1 cenv sp lo hi cs tm1, + forall s f te1 cenv sp lo hi cs tm1, vars_vals_match f params vl te1 -> list_norepet (List.map (@fst ident memory_chunk) params) -> mem_inject f m1 tm1 -> match_callstack f (mkframe cenv e te1 sp lo hi :: cs) m1.(nextblock) tm1.(nextblock) m1 -> + store_parameters cenv params = OK s -> exists te2, exists tm2, exec_stmt tge (Vptr sp Int.zero) - te1 tm1 (store_parameters cenv params) + te1 tm1 s E0 te2 tm2 Out_normal /\ mem_inject f m2 tm2 /\ match_callstack f (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2. Proof. induction 1. (* base case *) - intros; simpl. exists te1; exists tm1. split. constructor. tauto. + intros; simpl. monadInv H3. + exists te1; exists tm1. split. constructor. tauto. (* inductive case *) - intros until tm1. intros VVM NOREPET MINJ MATCH. simpl. + intros until tm1. intros VVM NOREPET MINJ MATCH STOREP. + monadInv STOREP. inversion VVM. subst f0 id0 chunk0 vars v vals te. - inversion MATCH. subst f0 cenv0 e0 te sp0 lo0 hi0 cs0 bound tbound m0. - inversion H18. inversion NOREPET. subst hd tl. - assert (NEXT: nextblock m1 = nextblock m). - eapply nextblock_store; eauto. - generalize (me_vars0 id). intro. inversion H2; subst. - (* cenv!!id = Var_local chunk *) - assert (b0 = b). congruence. subst b0. - assert (chunk0 = chunk). congruence. subst chunk0. - assert (v' = tv). congruence. subst v'. - exploit make_cast_correct. - apply eval_Evar with (id := id). eauto. - eexact H10. - intros [tv' [EVAL1 VINJ1]]. - set (te2 := PTree.set id tv' te1). - assert (VVM2: vars_vals_match f params vl te2). + exploit var_set_correct; eauto. + constructor; auto. + econstructor; eauto. + econstructor; eauto. + intros [te2 [tm2 [EXEC1 [MINJ1 [MATCH1 UNCHANGED1]]]]]. + assert (vars_vals_match f params vl te2). apply vars_vals_match_extensional with te1; auto. - intros. unfold te2; apply PTree.gso. red; intro; subst id0. - elim H4. change id with (fst (id, lv)). apply List.in_map; auto. - exploit store_unmapped_inject; eauto. intro MINJ2. - exploit match_callstack_store_local; eauto. - fold te2; rewrite <- NEXT; intro MATCH2. + intros. apply UNCHANGED1. red; intro; subst id0. + elim H4. change id with (fst (id, lv)). apply List.in_map. auto. exploit IHbind_parameters; eauto. - intros [te3 [tm3 [EXEC3 [MINJ3 MATCH3]]]]. - exists te3; exists tm3. - (* execution *) - split. apply exec_Sseq_continue with E0 te2 tm1 E0. - unfold te2. constructor. eassumption. assumption. traceEq. - (* meminj & match_callstack *) - tauto. - - (* cenv!!id = Var_stack_scalar *) - assert (b0 = b). congruence. subst b0. - assert (chunk0 = chunk). congruence. subst chunk0. - exploit make_store_correct. - eapply make_stackaddr_correct. - apply eval_Evar with (id := id). - eauto. 2:eauto. 2:eauto. unfold storev; eexact H0. eauto. - intros [tm2 [EVAL3 [MINJ2 NEXT1]]]. - exploit match_callstack_mapped. - eexact MATCH. 2:eauto. inversion H7. congruence. - rewrite <- NEXT; rewrite <- NEXT1; intro MATCH2. - exploit IHbind_parameters; eauto. - intros [te3 [tm3 [EVAL4 [MINJ3 MATCH3]]]]. + intros [te3 [tm3 [EXEC2 [MINJ2 MATCH2]]]]. exists te3; exists tm3. - (* execution *) - split. apply exec_Sseq_continue with (E0**E0) te1 tm2 E0. - auto. assumption. traceEq. - (* meminj & match_callstack *) - tauto. - - (* Impossible cases on cenv!!id *) - congruence. - congruence. - congruence. + split. econstructor; eauto. + auto. Qed. Lemma vars_vals_match_holds_1: @@ -1634,7 +1678,7 @@ Qed. and initialize the blocks corresponding to function parameters). *) Lemma function_entry_ok: - forall fn m e m1 lb vargs m2 f cs tm cenv sz tm1 sp tvargs, + forall fn m e m1 lb vargs m2 f cs tm cenv sz tm1 sp tvargs s, alloc_variables empty_env m (fn_variables fn) e m1 lb -> bind_parameters e m1 fn.(Csharpminor.fn_params) vargs m2 -> match_callstack f cs m.(nextblock) tm.(nextblock) m -> @@ -1646,9 +1690,10 @@ Lemma function_entry_ok: val_list_inject f vargs tvargs -> mem_inject f m tm -> list_norepet (fn_params_names fn ++ fn_vars_names fn) -> + store_parameters cenv fn.(Csharpminor.fn_params) = OK s -> exists f2, exists te2, exists tm2, exec_stmt tge (Vptr sp Int.zero) - te tm1 (store_parameters cenv fn.(Csharpminor.fn_params)) + te tm1 s E0 te2 tm2 Out_normal /\ mem_inject f2 m2 tm2 /\ inject_incr f f2 @@ -1669,7 +1714,7 @@ Proof. exploit store_parameters_correct. eauto. eauto. unfold fn_params_names in H7. eapply list_norepet_append_left; eauto. - eexact MINJ1. eauto. + eexact MINJ1. eauto. eauto. intros [te2 [tm2 [EXEC [MINJ2 MATCH2]]]]. exists f1; exists te2; exists tm2. split; auto. split; auto. split; auto. split; auto. @@ -1681,64 +1726,101 @@ Qed. (** The proof of semantic preservation uses simulation diagrams of the following form: << - le, e, m1, a --------------- tle, sp, te1, tm1, ta - | | + e, m1, s ----------------- sp, te1, tm1, ts | | + t| |t v v - le, e, m2, v --------------- tle, sp, te2, tm2, tv + e, m2, out --------------- sp, te2, tm2, tout >> - where [ta] is the Cminor expression obtained by translating the - Csharpminor expression [a]. The left vertical arrow is an evaluation - of a Csharpminor expression. The right vertical arrow is an evaluation - of a Cminor expression. The precondition (top vertical bar) + where [ts] is the Cminor statement obtained by translating the + Csharpminor statement [s]. The left vertical arrow is an execution + of a Csharpminor statement. The right vertical arrow is an execution + of a Cminor statement. The precondition (top vertical bar) includes a [mem_inject] relation between the memory states [m1] and [tm1], - a [val_list_inject] relation between the let environments [le] and [tle], and a [match_callstack] relation for any callstack having [e], [te1], [sp] as top frame. The postcondition (bottom vertical bar) is the existence of a memory injection [f2] that extends the injection [f1] we started with, preserves the [match_callstack] relation for the transformed callstack at the final state, and validates a - [val_inject] relation between the result values [v] and [tv]. + [outcome_inject] relation between the outcomes [out] and [tout]. +*) - We capture these diagrams by the following predicates, parameterized - over the Csharpminor executions, which will serve as induction - hypotheses in the proof of simulation. *) +(** ** Semantic preservation for expressions *) -Definition eval_expr_prop - (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (a: Csharpminor.expr) (t: trace) (m2: mem) (v: val) : Prop := - forall cenv ta f1 tle te tm1 sp lo hi cs - (TR: transl_expr cenv a = OK ta) - (LINJ: val_list_inject f1 le tle) - (MINJ: mem_inject f1 m1 tm1) - (MATCH: match_callstack f1 - (mkframe cenv e te sp lo hi :: cs) - m1.(nextblock) tm1.(nextblock) m1), - exists f2, exists tm2, exists tv, - eval_expr tge (Vptr sp Int.zero) tle te tm1 ta t tm2 tv - /\ val_inject f2 v tv - /\ mem_inject f2 m2 tm2 - /\ inject_incr f1 f2 - /\ match_callstack f2 - (mkframe cenv e te sp lo hi :: cs) - m2.(nextblock) tm2.(nextblock) m2. +Remark bool_of_val_inject: + forall f v tv b, + Val.bool_of_val v b -> val_inject f v tv -> Val.bool_of_val tv b. +Proof. + intros. inv H0; inv H; constructor; auto. +Qed. -Definition eval_exprlist_prop - (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (al: Csharpminor.exprlist) (t: trace) (m2: mem) (vl: list val) : Prop := - forall cenv tal f1 tle te tm1 sp lo hi cs - (TR: transl_exprlist cenv al = OK tal) - (LINJ: val_list_inject f1 le tle) - (MINJ: mem_inject f1 m1 tm1) - (MATCH: match_callstack f1 - (mkframe cenv e te sp lo hi :: cs) - m1.(nextblock) tm1.(nextblock) m1), - exists f2, exists tm2, exists tvl, - eval_exprlist tge (Vptr sp Int.zero) tle te tm1 tal t tm2 tvl - /\ val_list_inject f2 vl tvl - /\ mem_inject f2 m2 tm2 - /\ inject_incr f1 f2 - /\ match_callstack f2 - (mkframe cenv e te sp lo hi :: cs) - m2.(nextblock) tm2.(nextblock) m2. +Lemma transl_expr_correct: + forall f m tm cenv e te sp lo hi cs + (MINJ: mem_inject f m tm) + (MATCH: match_callstack f + (mkframe cenv e te sp lo hi :: cs) + m.(nextblock) tm.(nextblock) m), + forall a v, + Csharpminor.eval_expr prog e m a v -> + forall ta + (TR: transl_expr cenv a = OK ta), + exists tv, + eval_expr tge (Vptr sp Int.zero) te tm ta tv + /\ val_inject f v tv. +Proof. + induction 3; intros; simpl in TR; try (monadInv TR). + (* Evar *) + eapply var_get_correct; eauto. + (* Eaddrof *) + eapply var_addr_correct; eauto. + (* Econst *) + exploit transl_constant_correct; eauto. intros [tv [A B]]. + exists tv; split. constructor; eauto. eauto. + (* Eunop *) + exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]]. + exploit eval_unop_compat; eauto. intros [tv [EVAL INJ]]. + exists tv; split. econstructor; eauto. auto. + (* Ebinop *) + exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 INJ1]]. + exploit IHeval_expr2; eauto. intros [tv2 [EVAL2 INJ2]]. + exploit eval_binop_compat; eauto. intros [tv [EVAL INJ]]. + exists tv; split. econstructor; eauto. auto. + (* Eload *) + exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]]. + exploit loadv_inject; eauto. intros [tv [LOAD INJ]]. + exists tv; split. econstructor; eauto. auto. + (* Econdition *) + exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 INJ1]]. + assert (transl_expr cenv (if vb1 then b else c) = + OK (if vb1 then x0 else x1)). + destruct vb1; auto. + exploit IHeval_expr2; eauto. intros [tv2 [EVAL2 INJ2]]. + exists tv2; split. eapply eval_Econdition; eauto. + eapply bool_of_val_inject; eauto. auto. +Qed. + +Lemma transl_exprlist_correct: + forall f m tm cenv e te sp lo hi cs + (MINJ: mem_inject f m tm) + (MATCH: match_callstack f + (mkframe cenv e te sp lo hi :: cs) + m.(nextblock) tm.(nextblock) m), + forall a v, + Csharpminor.eval_exprlist prog e m a v -> + forall ta + (TR: transl_exprlist cenv a = OK ta), + exists tv, + eval_exprlist tge (Vptr sp Int.zero) te tm ta tv + /\ val_list_inject f v tv. +Proof. + induction 3; intros; monadInv TR. + exists (@nil val); split. constructor. constructor. + exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]]. + exploit IHeval_exprlist; eauto. intros [tv2 [EVAL2 VINJ2]]. + exists (tv1 :: tv2); split. constructor; auto. constructor; auto. +Qed. + +(** ** Semantic preservation for statements and functions *) Definition eval_funcall_prop (m1: mem) (fn: Csharpminor.fundef) (args: list val) (t: trace) (m2: mem) (res: val) : Prop := @@ -1783,316 +1865,12 @@ Definition exec_stmt_prop (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2. +(* Check (Csharpminor.eval_funcall_ind2 prog eval_funcall_prop exec_stmt_prop). *) + (** There are as many cases in the inductive proof as there are evaluation rules in the Csharpminor semantics. We treat each case as a separate lemma. *) -Lemma transl_expr_Evar_correct: - forall (le : Csharpminor.letenv) - (e : Csharpminor.env) (m : mem) (id : positive) - (b : block) (chunk : memory_chunk) (v : val), - eval_var_ref prog e id b chunk -> - load chunk m b 0 = Some v -> - eval_expr_prop le e m (Csharpminor.Evar id) E0 m v. -Proof. - intros; red; intros. unfold transl_expr in TR. - exploit var_get_correct; eauto. - intros [tv [EVAL VINJ]]. - exists f1; exists tm1; exists tv; intuition eauto. -Qed. - -Lemma transl_expr_Eaddrof_correct: - forall (le : Csharpminor.letenv) - (e : Csharpminor.env) (m : mem) (id : positive) - (b : block), - eval_var_addr prog e id b -> - eval_expr_prop le e m (Eaddrof id) E0 m (Vptr b Int.zero). -Proof. - intros; red; intros. simpl in TR. - exploit var_addr_correct; eauto. - intros [tv [EVAL VINJ]]. - exists f1; exists tm1; exists tv. intuition eauto. -Qed. - -Lemma transl_expr_Econst_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (cst : Csharpminor.constant) (v : val), - Csharpminor.eval_constant cst = Some v -> - eval_expr_prop le e m (Csharpminor.Econst cst) E0 m v. -Proof. - intros; red; intros; monadInv TR. - exploit transl_constant_correct; eauto. - intros [tv [EVAL VINJ]]. - exists f1; exists tm1; exists tv. intuition eauto. - constructor; eauto. -Qed. - -Lemma transl_expr_Eunop_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (op : unary_operation) (a : Csharpminor.expr) (t : trace) - (m1 : mem) (v1 v : val), - Csharpminor.eval_expr prog le e m a t m1 v1 -> - eval_expr_prop le e m a t m1 v1 -> - Csharpminor.eval_unop op v1 = Some v -> - eval_expr_prop le e m (Csharpminor.Eunop op a) t m1 v. -Proof. - intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]. - exploit eval_unop_compat; eauto. intros [tv [EVAL VINJ]]. - exists f2; exists tm2; exists tv; intuition. - econstructor; eauto. -Qed. - -Lemma transl_expr_Ebinop_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (op : binary_operation) (a1 a2 : Csharpminor.expr) (t1 : trace) - (m1 : mem) (v1 : val) (t2 : trace) (m2 : mem) (v2 : val) - (t : trace) (v : val), - Csharpminor.eval_expr prog le e m a1 t1 m1 v1 -> - eval_expr_prop le e m a1 t1 m1 v1 -> - Csharpminor.eval_expr prog le e m1 a2 t2 m2 v2 -> - eval_expr_prop le e m1 a2 t2 m2 v2 -> - Csharpminor.eval_binop op v1 v2 m2 = Some v -> - t = t1 ** t2 -> - eval_expr_prop le e m (Csharpminor.Ebinop op a1 a2) t m2 v. -Proof. - intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]. - exploit H2. - eauto. eapply val_list_inject_incr; eauto. eauto. eauto. - intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]. - exploit eval_binop_compat. - eauto. eapply val_inject_incr; eauto. eauto. eauto. - intros [tv [EVAL VINJ]]. - exists f3; exists tm3; exists tv; intuition. - econstructor; eauto. - eapply inject_incr_trans; eauto. -Qed. - -Lemma transl_expr_Eload_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (chunk : memory_chunk) (a : Csharpminor.expr) (t: trace) (m1 : mem) - (v1 v : val), - Csharpminor.eval_expr prog le e m a t m1 v1 -> - eval_expr_prop le e m a t m1 v1 -> - loadv chunk m1 v1 = Some v -> - eval_expr_prop le e m (Csharpminor.Eload chunk a) t m1 v. -Proof. - intros; red; intros. - monadInv TR. - exploit H0; eauto. - intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]. - exploit loadv_inject; eauto. - intros [tv [TLOAD VINJ]]. - exists f2; exists tm2; exists tv. - intuition. - econstructor; eauto. -Qed. - -Lemma transl_expr_Ecall_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (sig : signature) (a : Csharpminor.expr) (bl : Csharpminor.exprlist) - (t1: trace) (m1: mem) (t2: trace) (m2: mem) (t3: trace) (m3: mem) - (vf : val) (vargs : list val) (vres : val) - (f : Csharpminor.fundef) (t: trace), - Csharpminor.eval_expr prog le e m a t1 m1 vf -> - eval_expr_prop le e m a t1 m1 vf -> - Csharpminor.eval_exprlist prog le e m1 bl t2 m2 vargs -> - eval_exprlist_prop le e m1 bl t2 m2 vargs -> - Genv.find_funct ge vf = Some f -> - Csharpminor.funsig f = sig -> - Csharpminor.eval_funcall prog m2 f vargs t3 m3 vres -> - eval_funcall_prop m2 f vargs t3 m3 vres -> - t = t1 ** t2 ** t3 -> - eval_expr_prop le e m (Csharpminor.Ecall sig a bl) t m3 vres. -Proof. - intros;red;intros. monadInv TR. - exploit H0; eauto. - intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]. - exploit H2. - eauto. eapply val_list_inject_incr; eauto. eauto. eauto. - intros [f3 [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_negative H3). intro. - assert (match_globalenvs f2). eapply match_callstack_match_globalenvs; eauto. - generalize (mg_functions _ H7 _ H4). intro. - rewrite VF in VINJ1. inversion VINJ1. subst vf. - decEq. congruence. - subst ofs2. replace x1 with 0. reflexivity. congruence. - subst tv1. elim (functions_translated _ _ H3). intros tf [FIND TRF]. - exploit H6; eauto. - intros [f4 [tm4 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]]. - exists f4; exists tm4; exists tres. intuition. - eapply eval_Ecall; eauto. - apply sig_preserved; auto. - apply inject_incr_trans with f2; auto. - apply inject_incr_trans with f3; auto. -Qed. - -Lemma transl_expr_Econdition_true_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (a b c : Csharpminor.expr) (t1: trace) (m1 : mem) (v1 : val) - (t2: trace) (m2 : mem) (v2 : val) (t: trace), - Csharpminor.eval_expr prog le e m a t1 m1 v1 -> - eval_expr_prop le e m a t1 m1 v1 -> - Val.is_true v1 -> - Csharpminor.eval_expr prog le e m1 b t2 m2 v2 -> - eval_expr_prop le e m1 b t2 m2 v2 -> - t = t1 ** t2 -> - eval_expr_prop le e m (Csharpminor.Econdition a b c) t m2 v2. -Proof. - intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]. - exploit H3. - eauto. eapply val_list_inject_incr; eauto. eauto. eauto. - intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]. - exists f3; exists tm3; exists tv2. - intuition. - eapply eval_Econdition with (b1 := true); eauto. - eapply val_inject_bool_of_val; eauto. apply Val.bool_of_true_val; eauto. - eapply inject_incr_trans; eauto. -Qed. - -Lemma transl_expr_Econdition_false_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (a b c : Csharpminor.expr) (t1: trace) (m1 : mem) (v1 : val) - (t2: trace) (m2 : mem) (v2 : val) (t: trace), - Csharpminor.eval_expr prog le e m a t1 m1 v1 -> - eval_expr_prop le e m a t1 m1 v1 -> - Val.is_false v1 -> - Csharpminor.eval_expr prog le e m1 c t2 m2 v2 -> - eval_expr_prop le e m1 c t2 m2 v2 -> - t = t1 ** t2 -> - eval_expr_prop le e m (Csharpminor.Econdition a b c) t m2 v2. -Proof. - intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]. - exploit H3. - eauto. eapply val_list_inject_incr; eauto. eauto. eauto. - intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]. - exists f3; exists tm3; exists tv2. - intuition. - eapply eval_Econdition with (b1 := false); eauto. - eapply val_inject_bool_of_val; eauto. apply Val.bool_of_false_val; eauto. - eapply inject_incr_trans; eauto. -Qed. - -Lemma transl_expr_Elet_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (a b : Csharpminor.expr) (t1: trace) (m1 : mem) (v1 : val) - (t2: trace) (m2 : mem) (v2 : val) (t: trace), - Csharpminor.eval_expr prog le e m a t1 m1 v1 -> - eval_expr_prop le e m a t1 m1 v1 -> - Csharpminor.eval_expr prog (v1 :: le) e m1 b t2 m2 v2 -> - eval_expr_prop (v1 :: le) e m1 b t2 m2 v2 -> - t = t1 ** t2 -> - eval_expr_prop le e m (Csharpminor.Elet a b) t m2 v2. -Proof. - intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]. - exploit H2. - eauto. - constructor. eauto. eapply val_list_inject_incr; eauto. - eauto. eauto. - intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]. - exists f3; exists tm3; exists tv2. - intuition. - eapply eval_Elet; eauto. - eapply inject_incr_trans; eauto. -Qed. - -Remark val_list_inject_nth: - forall f l1 l2, val_list_inject f l1 l2 -> - forall n v1, nth_error l1 n = Some v1 -> - exists v2, nth_error l2 n = Some v2 /\ val_inject f v1 v2. -Proof. - induction 1; destruct n; simpl; intros. - discriminate. discriminate. - injection H1; intros; subst v. exists v'; split; auto. - eauto. -Qed. - -Lemma transl_expr_Eletvar_correct: - forall (le : list val) (e : Csharpminor.env) (m : mem) (n : nat) - (v : val), - nth_error le n = Some v -> - eval_expr_prop le e m (Csharpminor.Eletvar n) E0 m v. -Proof. - intros; red; intros. monadInv TR. - exploit val_list_inject_nth; eauto. intros [tv [A B]]. - exists f1; exists tm1; exists tv. - intuition. - 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 [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 tm3; exists (Vptr tb Int.zero). - split. econstructor; eauto. - split. econstructor. unfold extend_inject, eq_block. rewrite zeq_true. reflexivity. - reflexivity. - split. assumption. - split. eapply inject_incr_trans; eauto. - eapply match_callstack_alloc; eauto. -Qed. - -Lemma transl_exprlist_Enil_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem), - eval_exprlist_prop le e m Csharpminor.Enil E0 m nil. -Proof. - intros; red; intros. monadInv TR. - exists f1; exists tm1; exists (@nil val). - intuition. constructor. -Qed. - -Lemma transl_exprlist_Econs_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (a : Csharpminor.expr) (bl : Csharpminor.exprlist) - (t1: trace) (m1 : mem) (v : val) - (t2: trace) (m2 : mem) (vl : list val) (t: trace), - Csharpminor.eval_expr prog le e m a t1 m1 v -> - eval_expr_prop le e m a t1 m1 v -> - Csharpminor.eval_exprlist prog le e m1 bl t2 m2 vl -> - eval_exprlist_prop le e m1 bl t2 m2 vl -> - t = t1 ** t2 -> - eval_exprlist_prop le e m (Csharpminor.Econs a bl) t m2 (v :: vl). -Proof. - intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]. - exploit H2. - eauto. eapply val_list_inject_incr; eauto. eauto. eauto. - intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]. - exists f3; exists tm3; exists (tv1 :: tv2). - intuition. econstructor; eauto. - constructor. eapply val_inject_incr; eauto. auto. - eapply inject_incr_trans; eauto. -Qed. - Lemma transl_funcall_internal_correct: forall (m : mem) (f : Csharpminor.function) (vargs : list val) (e : Csharpminor.env) (m1 : mem) (lb : list block) (m2: mem) @@ -2176,77 +1954,104 @@ Proof. intuition. constructor. constructor. Qed. -Lemma transl_stmt_Sexpr_correct: - forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (t: trace) (m1 : mem) (v : val), - Csharpminor.eval_expr prog nil e m a t m1 v -> - eval_expr_prop nil e m a t m1 v -> - exec_stmt_prop e m (Csharpminor.Sexpr a) t m1 Csharpminor.Out_normal. -Proof. - intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]. - exists f2; exists te1; exists tm2; exists Out_normal. - intuition. 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. + forall (e : Csharpminor.env) (m : mem) (id : ident) + (a : Csharpminor.expr) (v : val) (m' : mem), + Csharpminor.eval_expr prog e m a v -> + exec_assign prog e m id v m' -> + exec_stmt_prop e m (Csharpminor.Sassign id a) E0 m' Csharpminor.Out_normal. Proof. intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [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. + exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]]. + exploit var_set_correct; eauto. + intros [te2 [tm2 [EVAL2 [MINJ2 MATCH2]]]]. + exists f1; exists te2; exists tm2; exists Out_normal. intuition. constructor. Qed. Lemma transl_stmt_Sstore_correct: - forall (e : Csharpminor.env) (m : mem) - (chunk : memory_chunk) (a b : Csharpminor.expr) (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. + forall (e : Csharpminor.env) (m : mem) (chunk : memory_chunk) + (a b : Csharpminor.expr) (v1 v2 : val) (m' : mem), + Csharpminor.eval_expr prog e m a v1 -> + Csharpminor.eval_expr prog e m b v2 -> + storev chunk m v1 v2 = Some m' -> + exec_stmt_prop e m (Csharpminor.Sstore chunk a b) E0 m' Csharpminor.Out_normal. Proof. intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]. - exploit H2. - eauto. - eapply val_list_inject_incr; eauto. - eauto. eauto. - intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]. + exploit transl_expr_correct. + eauto. eauto. eexact H. eauto. + intros [tv1 [EVAL1 INJ1]]. + exploit transl_expr_correct. + eauto. eauto. eexact H0. eauto. + intros [tv2 [EVAL2 INJ2]]. exploit make_store_correct. - eexact EVAL1. eexact EVAL2. eauto. eauto. - eapply val_inject_incr; eauto. eauto. - intros [tm4 [EVAL [MINJ4 NEXTBLOCK]]]. - exists f3; exists te1; exists tm4; exists Out_normal. + eexact EVAL1. eexact EVAL2. eauto. eauto. eauto. eauto. + intros [tm2 [EXEC [MINJ2 NEXTBLOCK]]]. + exists f1; exists te1; exists tm2; exists Out_normal. 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). + unfold storev in H1; destruct v1; try discriminate. + inv INJ1. + rewrite NEXTBLOCK. replace (nextblock m') with (nextblock m). eapply match_callstack_mapped; eauto. congruence. symmetry. eapply nextblock_store; eauto. Qed. +Lemma transl_stmt_Scall_correct: + forall (e : Csharpminor.env) (m : mem) (optid : option ident) + (sig : signature) (a : Csharpminor.expr) + (bl : list Csharpminor.expr) (vf : val) (vargs : list val) + (f : Csharpminor.fundef) (t : trace) (m1 : mem) (vres : val) + (m2 : mem), + Csharpminor.eval_expr prog e m a vf -> + Csharpminor.eval_exprlist prog e m bl vargs -> + Genv.find_funct (Genv.globalenv prog) vf = Some f -> + Csharpminor.funsig f = sig -> + Csharpminor.eval_funcall prog m f vargs t m1 vres -> + eval_funcall_prop m f vargs t m1 vres -> + exec_opt_assign prog e m1 optid vres m2 -> + exec_stmt_prop e m (Csharpminor.Scall optid sig a bl) t m2 Csharpminor.Out_normal. +Proof. + intros;red;intros. + assert (forall tv, val_inject f1 vf tv -> tv = vf). + intros. + elim (Genv.find_funct_inv H1). intros bf VF. rewrite VF in H1. + rewrite Genv.find_funct_find_funct_ptr in H1. + generalize (Genv.find_funct_ptr_negative H1). intro. + assert (match_globalenvs f1). eapply match_callstack_match_globalenvs; eauto. + generalize (mg_functions _ H8 _ H7). intro. + rewrite VF in H6. inv H6. + decEq. congruence. + replace x with 0. reflexivity. congruence. + inv H5; monadInv TR. + (* optid = None *) + exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]]. + exploit transl_exprlist_correct; eauto. intros [tv2 [EVAL2 VINJ2]]. + rewrite <- (H6 _ VINJ1) in H1. + elim (functions_translated _ _ H1). intros tf [FIND TRF]. + exploit H4; eauto. + intros [f2 [tm2 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]]. + exists f2; exists te1; exists tm2; exists Out_normal. + intuition. eapply exec_Scall; eauto. + apply sig_preserved; auto. + constructor. + (* optid = Some id *) + exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]]. + exploit transl_exprlist_correct; eauto. intros [tv2 [EVAL2 VINJ2]]. + rewrite <- (H6 _ VINJ1) in H1. + elim (functions_translated _ _ H1). intros tf [FIND TRF]. + exploit H4; eauto. + intros [f2 [tm2 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]]. + exploit var_set_self_correct. + eauto. eexact MATCH3. eauto. eauto. eauto. + intros [te3 [tm3 [EVAL4 [MINJ4 MATCH4]]]]. + exists f2; exists te3; exists tm3; exists Out_normal. intuition. + eapply exec_Sseq_continue. eapply exec_Scall; eauto. + apply sig_preserved; auto. + simpl. eexact EVAL4. traceEq. + constructor. +Qed. + Lemma transl_stmt_Sseq_continue_correct: forall (e : Csharpminor.env) (m : mem) (s1 s2 : Csharpminor.stmt) (t1 t2: trace) (m1 m2 : mem) (t: trace) (out : Csharpminor.outcome), @@ -2284,54 +2089,27 @@ Proof. inversion OINJ1; subst out tout1; congruence. Qed. -Lemma transl_stmt_Sifthenelse_true_correct: - forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (sl1 sl2 : Csharpminor.stmt) - (t1: trace) (m1 : mem) (v1 : val) (t2: trace) (m2 : mem) - (out : Csharpminor.outcome) (t: trace), - Csharpminor.eval_expr prog nil e m a t1 m1 v1 -> - eval_expr_prop nil e m a t1 m1 v1 -> - Val.is_true v1 -> - Csharpminor.exec_stmt prog e m1 sl1 t2 m2 out -> - exec_stmt_prop e m1 sl1 t2 m2 out -> - t = t1 ** t2 -> - exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) t m2 out. -Proof. - intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [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. - eapply exec_Sifthenelse with (b1 := true); eauto. - eapply val_inject_bool_of_val; eauto. apply Val.bool_of_true_val; auto. - eapply inject_incr_trans; eauto. -Qed. - -Lemma transl_stmt_Sifthenelse_false_correct: - forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (sl1 sl2 : Csharpminor.stmt) - (t1: trace) (m1 : mem) (v1 : val) (t2: trace) (m2 : mem) - (out : Csharpminor.outcome) (t: trace), - Csharpminor.eval_expr prog nil e m a t1 m1 v1 -> - eval_expr_prop nil e m a t1 m1 v1 -> - Val.is_false v1 -> - Csharpminor.exec_stmt prog e m1 sl2 t2 m2 out -> - exec_stmt_prop e m1 sl2 t2 m2 out -> - t = t1 ** t2 -> - exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) t m2 out. +Lemma transl_stmt_Sifthenelse_correct: + forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) + (sl1 sl2 : Csharpminor.stmt) (v : val) (vb : bool) (t : trace) + (m' : mem) (out : Csharpminor.outcome), + Csharpminor.eval_expr prog e m a v -> + Val.bool_of_val v vb -> + Csharpminor.exec_stmt prog e m (if vb then sl1 else sl2) t m' out -> + exec_stmt_prop e m (if vb then sl1 else sl2) t m' out -> + exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) t m' out. Proof. intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [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. + exploit transl_expr_correct; eauto. + intros [tv1 [EVAL1 VINJ1]]. + assert (transl_stmt cenv (if vb then sl1 else sl2) = + OK (if vb then x0 else x1)). destruct vb; auto. + exploit H2; eauto. + intros [f2 [te2 [tm2 [tout [EVAL2 [OINJ [MINJ2 [INCR2 MATCH2]]]]]]]]. + exists f2; exists te2; exists tm2; exists tout. intuition. - eapply exec_Sifthenelse with (b1 := false); eauto. - eapply val_inject_bool_of_val; eauto. apply Val.bool_of_false_val; auto. - eapply inject_incr_trans; eauto. + eapply exec_Sifthenelse; eauto. + eapply bool_of_val_inject; eauto. Qed. Lemma transl_stmt_Sloop_loop_correct: @@ -2373,6 +2151,18 @@ Proof. inversion OINJ1; subst out tout1; congruence. Qed. +Remark outcome_block_inject: + forall f out tout, + outcome_inject f out tout -> + outcome_inject f (Csharpminor.outcome_block out) (outcome_block tout). +Proof. + induction 1; simpl. + constructor. + destruct n; constructor. + constructor. + constructor; auto. +Qed. + Lemma transl_stmt_Sblock_correct: forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) (t1: trace) (m1 : mem) (out : Csharpminor.outcome), @@ -2386,11 +2176,7 @@ Proof. intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. exists f2; exists te2; exists tm2; exists (outcome_block tout1). intuition. eapply exec_Sblock; eauto. - inversion OINJ1; subst out tout1; simpl. - constructor. - destruct n; constructor. - constructor. - constructor; auto. + apply outcome_block_inject; auto. Qed. Lemma transl_stmt_Sexit_correct: @@ -2403,21 +2189,22 @@ Proof. Qed. Lemma transl_stmt_Sswitch_correct: - forall (e : Csharpminor.env) (m : mem) - (a : Csharpminor.expr) (cases : list (int * nat)) (default : nat) - (t1 : trace) (m1 : mem) (n : int), - Csharpminor.eval_expr prog nil e m a t1 m1 (Vint n) -> - eval_expr_prop nil e m a t1 m1 (Vint n) -> - exec_stmt_prop e m (Csharpminor.Sswitch a cases default) t1 m1 - (Csharpminor.Out_exit (Csharpminor.switch_target n default cases)). + forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) + (cases : list (int * nat)) (default : nat) (n : int), + Csharpminor.eval_expr prog e m a (Vint n) -> + exec_stmt_prop e m (Csharpminor.Sswitch a cases default) E0 m + (Csharpminor.Out_exit (switch_target n default cases)). Proof. intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]. - exists f2; exists te1; exists tm2; - exists (Out_exit (switch_target n default cases)). intuition. - constructor. inversion VINJ1. subst tv1. assumption. - constructor. + exploit transl_expr_correct; eauto. + intros [tv1 [EVAL VINJ1]]. + inv VINJ1. + exists f1; exists te1; exists tm1; exists (Out_exit (switch_target n default cases)). + split. constructor. auto. + split. constructor. + split. auto. + split. apply inject_incr_refl. + auto. Qed. Lemma transl_stmt_Sreturn_none_correct: @@ -2431,17 +2218,16 @@ Proof. Qed. Lemma transl_stmt_Sreturn_some_correct: - forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (t1: trace) (m1 : mem) (v : val), - Csharpminor.eval_expr prog nil e m a t1 m1 v -> - eval_expr_prop nil e m a t1 m1 v -> - exec_stmt_prop e m (Csharpminor.Sreturn (Some a)) t1 m1 - (Csharpminor.Out_return (Some v)). + forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) + (v : val), + Csharpminor.eval_expr prog e m a v -> + exec_stmt_prop e m (Csharpminor.Sreturn (Some a)) E0 m + (Csharpminor.Out_return (Some v)). Proof. intros; red; intros; monadInv TR. - exploit H0; eauto. - intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]. - exists f2; exists te1; exists tm2; exists (Out_return (Some tv1)). + exploit transl_expr_correct; eauto. + intros [tv1 [EVAL VINJ1]]. + exists f1; exists te1; exists tm1; exists (Out_return (Some tv1)). intuition. econstructor; eauto. constructor; auto. Qed. @@ -2453,36 +2239,45 @@ Lemma transl_function_correct: Csharpminor.eval_funcall prog m1 f vargs t m2 vres -> eval_funcall_prop m1 f vargs t m2 vres. Proof - (Csharpminor.eval_funcall_ind4 prog - eval_expr_prop - eval_exprlist_prop + (Csharpminor.eval_funcall_ind2 prog + eval_funcall_prop + exec_stmt_prop + + transl_funcall_internal_correct + transl_funcall_external_correct + transl_stmt_Sskip_correct + transl_stmt_Sassign_correct + transl_stmt_Sstore_correct + transl_stmt_Scall_correct + transl_stmt_Sseq_continue_correct + transl_stmt_Sseq_stop_correct + transl_stmt_Sifthenelse_correct + transl_stmt_Sloop_loop_correct + transl_stmt_Sloop_exit_correct + transl_stmt_Sblock_correct + transl_stmt_Sexit_correct + transl_stmt_Sswitch_correct + transl_stmt_Sreturn_none_correct + transl_stmt_Sreturn_some_correct). + +Lemma transl_stmt_correct: + forall e m1 s t m2 out, + Csharpminor.exec_stmt prog e m1 s t m2 out -> + exec_stmt_prop e m1 s t m2 out. +Proof + (Csharpminor.exec_stmt_ind2 prog eval_funcall_prop exec_stmt_prop - transl_expr_Evar_correct - transl_expr_Eaddrof_correct - transl_expr_Econst_correct - transl_expr_Eunop_correct - transl_expr_Ebinop_correct - transl_expr_Eload_correct - transl_expr_Ecall_correct - transl_expr_Econdition_true_correct - transl_expr_Econdition_false_correct - transl_expr_Elet_correct - transl_expr_Eletvar_correct - transl_expr_Ealloc_correct - transl_exprlist_Enil_correct - transl_exprlist_Econs_correct transl_funcall_internal_correct transl_funcall_external_correct transl_stmt_Sskip_correct - transl_stmt_Sexpr_correct transl_stmt_Sassign_correct transl_stmt_Sstore_correct + transl_stmt_Scall_correct transl_stmt_Sseq_continue_correct transl_stmt_Sseq_stop_correct - transl_stmt_Sifthenelse_true_correct - transl_stmt_Sifthenelse_false_correct + transl_stmt_Sifthenelse_correct transl_stmt_Sloop_loop_correct transl_stmt_Sloop_exit_correct transl_stmt_Sblock_correct @@ -2491,6 +2286,133 @@ Proof transl_stmt_Sreturn_none_correct transl_stmt_Sreturn_some_correct). +(** ** Semantic preservation for divergence *) + +Definition evalinf_funcall_prop + (m1: mem) (fn: Csharpminor.fundef) (args: list val) (t: traceinf) : Prop := + forall tfn f1 tm1 cs targs + (TR: transl_fundef gce fn = OK tfn) + (MINJ: mem_inject f1 m1 tm1) + (MATCH: match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1) + (ARGSINJ: val_list_inject f1 args targs), + evalinf_funcall tge tm1 tfn targs t. + +Definition execinf_stmt_prop + (e: Csharpminor.env) (m1: mem) (s: Csharpminor.stmt) (t: traceinf): Prop := + forall cenv ts f1 te1 tm1 sp lo hi cs + (TR: transl_stmt cenv s = OK ts) + (MINJ: mem_inject f1 m1 tm1) + (MATCH: match_callstack f1 + (mkframe cenv e te1 sp lo hi :: cs) + m1.(nextblock) tm1.(nextblock) m1), + execinf_stmt tge (Vptr sp Int.zero) te1 tm1 ts t. + +Theorem transl_function_divergence_correct: + forall m1 fn args t, + Csharpminor.evalinf_funcall prog m1 fn args t -> + evalinf_funcall_prop m1 fn args t. +Proof. + unfold evalinf_funcall_prop; cofix FUNCALL. + assert (STMT: forall e m1 s t, + Csharpminor.execinf_stmt prog e m1 s t -> + execinf_stmt_prop e m1 s t). + unfold execinf_stmt_prop; cofix STMT. + intros. inv H; simpl in TR; try (monadInv TR). + (* Scall *) + assert (forall tv, val_inject f1 vf tv -> tv = vf). + intros. + elim (Genv.find_funct_inv H2). intros bf VF. rewrite VF in H2. + rewrite Genv.find_funct_find_funct_ptr in H2. + generalize (Genv.find_funct_ptr_negative H2). intro. + assert (match_globalenvs f1). eapply match_callstack_match_globalenvs; eauto. + generalize (mg_functions _ H5 _ H3). intro. + rewrite VF in H. inv H. + decEq. congruence. + replace x with 0. reflexivity. congruence. + destruct optid; monadInv TR. + (* optid = Some i *) + destruct (transl_expr_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H0 _ EQ) + as [tv1 [EVAL1 VINJ1]]. + destruct (transl_exprlist_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H1 _ EQ1) + as [tv2 [EVAL2 VINJ2]]. + rewrite <- (H _ VINJ1) in H2. + elim (functions_translated _ _ H2). intros tf [FIND TRF]. + apply execinf_Sseq_1. eapply execinf_Scall. + eauto. eauto. eauto. apply sig_preserved; auto. + eapply FUNCALL; eauto. + (* optid = None *) + destruct (transl_expr_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H0 _ EQ) + as [tv1 [EVAL1 VINJ1]]. + destruct (transl_exprlist_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H1 _ EQ1) + as [tv2 [EVAL2 VINJ2]]. + rewrite <- (H _ VINJ1) in H2. + elim (functions_translated _ _ H2). intros tf [FIND TRF]. + eapply execinf_Scall. + eauto. eauto. eauto. apply sig_preserved; auto. + eapply FUNCALL; eauto. + (* Sseq, 1 *) + apply execinf_Sseq_1. eapply STMT; eauto. + (* Sseq, 2 *) + destruct (transl_stmt_correct _ _ _ _ _ _ H0 + _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) + as [f2 [te2 [tm2 [tout [EXEC1 [OUT [MINJ2 [INCR12 MATCH2]]]]]]]]. + inv OUT. + eapply execinf_Sseq_2. eexact EXEC1. + eapply STMT; eauto. + auto. + (* Sifthenelse, true *) + destruct (transl_expr_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H0 _ EQ) + as [tv1 [EVAL1 VINJ1]]. + assert (transl_stmt cenv (if vb then sl1 else sl2) = + OK (if vb then x0 else x1)). destruct vb; auto. + eapply execinf_Sifthenelse. eexact EVAL1. + eapply bool_of_val_inject; eauto. + eapply STMT; eauto. + (* Sloop, body *) + eapply execinf_Sloop_body. eapply STMT; eauto. + (* Sloop, loop *) + destruct (transl_stmt_correct _ _ _ _ _ _ H0 + _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) + as [f2 [te2 [tm2 [tout [EXEC1 [OUT [MINJ2 [INCR12 MATCH2]]]]]]]]. + inv OUT. + eapply execinf_Sloop_loop. eexact EXEC1. + eapply STMT; eauto. + simpl. rewrite EQ. auto. auto. + (* Sblock *) + apply execinf_Sblock. eapply STMT; eauto. + (* stutter *) + generalize (execinf_stmt_N_inv _ _ _ _ _ _ H0); intro. + destruct s; try contradiction; monadInv TR. + apply execinf_Sseq_1. eapply STMT; eauto. + apply execinf_Sblock. eapply STMT; eauto. + (* Sloop_block *) + destruct (transl_stmt_correct _ _ _ _ _ _ H0 + _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) + as [f2 [te2 [tm2 [tout [EXEC1 [OUT [MINJ2 [INCR12 MATCH2]]]]]]]]. + inv OUT. + eapply execinf_Sloop_loop. eexact EXEC1. + eapply STMT with (s := Csharpminor.Sloop sl); eauto. + apply execinf_Sblock_inv; eauto. + simpl. rewrite EQ; auto. auto. + (* Function *) + intros. inv H. + monadInv TR. generalize EQ. + unfold transl_function. + caseEq (build_compilenv gce f); intros cenv stacksize CENV. + destruct (zle stacksize Int.max_signed); try congruence. + intro TR. monadInv TR. + caseEq (alloc tm1 0 stacksize). intros tm2 sp ALLOC. + destruct (function_entry_ok _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ + H1 H2 MATCH CENV z ALLOC ARGSINJ MINJ H0 EQ2) + as [f2 [te2 [tm3 [STOREPARAM [MINJ2 [INCR12 [MATCH2 BLOCKS]]]]]]]. + eapply evalinf_funcall_internal; simpl. + eauto. reflexivity. eapply execinf_Sseq_2. eexact STOREPARAM. + unfold execinf_stmt_prop in STMT. eapply STMT; eauto. + traceEq. +Qed. + +(** ** Semantic preservation for whole programs *) + (** The [match_globalenvs] relation holds for the global environments of the source program and the transformed program. *) @@ -2513,12 +2435,11 @@ Qed. follows. *) Theorem transl_program_correct: - forall t n, - Csharpminor.exec_program prog t (Vint n) -> - exec_program tprog t (Vint n). + forall beh, + Csharpminor.exec_program prog beh -> + exec_program tprog beh. Proof. - intros t n [b [fn [m [FINDS [FINDF [SIG EVAL]]]]]]. - elim (function_ptr_translated _ _ FINDF). intros tfn [TFIND TR]. + intros. set (m0 := Genv.init_mem prog) in *. set (f := meminj_init m0). assert (MINJ0: mem_inject f m0 m0). @@ -2526,17 +2447,31 @@ Proof. unfold m0; apply Genv.initmem_inject_neutral. assert (MATCH0: match_callstack f nil m0.(nextblock) m0.(nextblock) m0). constructor. unfold f; apply match_globalenvs_init. - fold ge in EVAL. + inv H. + (* Terminating case *) + subst ge0 m1. + elim (function_ptr_translated _ _ H1). intros tfn [TFIND TR]. + fold ge in H3. exploit transl_function_correct; eauto. intros [f1 [tm1 [tres [TEVAL [VINJ [MINJ1 [INCR MATCH1]]]]]]]. - 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. + econstructor; eauto. + fold tge. rewrite <- H0. fold ge. + replace (prog_main prog) with (AST.prog_main tprog). apply symbols_preserved. apply transform_partial_program2_main with (transl_fundef gce) transl_globvar. assumption. - split. assumption. - split. rewrite <- SIG. apply sig_preserved; auto. + rewrite <- H2. apply sig_preserved; auto. + rewrite (Genv.init_mem_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). + inv VINJ. fold tge; fold m0. eexact TEVAL. + (* Diverging case *) + subst ge0 m1. + elim (function_ptr_translated _ _ H1). intros tfn [TFIND TR]. + econstructor; eauto. + fold tge. rewrite <- H0. fold ge. + replace (prog_main prog) with (AST.prog_main tprog). apply symbols_preserved. + apply transform_partial_program2_main with (transl_fundef gce) transl_globvar. assumption. + rewrite <- H2. apply sig_preserved; auto. rewrite (Genv.init_mem_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). - inversion VINJ; subst tres. assumption. + fold tge; fold m0. + eapply (transl_function_divergence_correct _ _ _ _ H3); eauto. Qed. End TRANSLATION. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 385f7c68..af601aca 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -11,6 +11,7 @@ Require Import Mem. Require Import Events. Require Import Globalenvs. Require Import Csyntax. +Require Import Smallstep. (** * Semantics of type-dependent operations *) @@ -509,129 +510,108 @@ Section RELSEM. Variable ge: genv. -(** [eval_expr ge e m1 a t m2 v] defines the evaluation of expression [a] - in r-value position. [v] is the value of the expression. - [m1] is the initial memory state, [m2] the final memory state. - [t] is the trace of input/output events performed during this - evaluation. *) +Section EXPR. + +Variable e: env. +Variable m: mem. -Inductive eval_expr: env -> mem -> expr -> trace -> mem -> val -> Prop := - | eval_Econst_int: forall e m i ty, - eval_expr e m (Expr (Econst_int i) ty) - E0 m (Vint i) - | eval_Econst_float: forall e m f ty, - eval_expr e m (Expr (Econst_float f) ty) - E0 m (Vfloat f) - | eval_Elvalue: forall e m a ty t m1 loc ofs v, - eval_lvalue e m (Expr a ty) t m1 loc ofs -> - load_value_of_type ty m1 loc ofs = Some v -> - eval_expr e m (Expr a ty) - t m1 v - | eval_Eaddrof: forall e m a t m1 loc ofs ty, - eval_lvalue e m a t m1 loc ofs -> - eval_expr e m (Expr (Eaddrof a) ty) - t m1 (Vptr loc ofs) - | eval_Esizeof: forall e m ty' ty, - eval_expr e m (Expr (Esizeof ty') ty) - E0 m (Vint (Int.repr (sizeof ty'))) - | eval_Eunop: forall e m op a ty t m1 v1 v, - eval_expr e m a t m1 v1 -> +(** [eval_expr ge e m a v] defines the evaluation of expression [a] + in r-value position. [v] is the value of the expression. + [e] is the current environment and [m] is the current memory state. *) + +Inductive eval_expr: expr -> val -> Prop := + | eval_Econst_int: forall i ty, + eval_expr (Expr (Econst_int i) ty) (Vint i) + | eval_Econst_float: forall f ty, + eval_expr (Expr (Econst_float f) ty) (Vfloat f) + | eval_Elvalue: forall a ty loc ofs v, + eval_lvalue (Expr a ty) loc ofs -> + load_value_of_type ty m loc ofs = Some v -> + eval_expr (Expr a ty) v + | eval_Eaddrof: forall a ty loc ofs, + eval_lvalue a loc ofs -> + eval_expr (Expr (Eaddrof a) ty) (Vptr loc ofs) + | eval_Esizeof: forall ty' ty, + eval_expr (Expr (Esizeof ty') ty) (Vint (Int.repr (sizeof ty'))) + | eval_Eunop: forall op a ty v1 v, + eval_expr a v1 -> sem_unary_operation op v1 (typeof a) = Some v -> - eval_expr e m (Expr (Eunop op a) ty) - t m1 v - | eval_Ebinop: forall e m op a1 a2 ty t1 m1 v1 t2 m2 v2 v, - eval_expr e m a1 t1 m1 v1 -> - eval_expr e m1 a2 t2 m2 v2 -> - sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m2 = Some v -> - eval_expr e m (Expr (Ebinop op a1 a2) ty) - (t1 ** t2) m2 v - | eval_Eorbool_1: forall e m a1 a2 t m1 v1 ty, - eval_expr e m a1 t m1 v1 -> + eval_expr (Expr (Eunop op a) ty) v + | eval_Ebinop: forall op a1 a2 ty v1 v2 v, + eval_expr a1 v1 -> + eval_expr a2 v2 -> + sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v -> + eval_expr (Expr (Ebinop op a1 a2) ty) v + | eval_Eorbool_1: forall a1 a2 ty v1, + eval_expr a1 v1 -> is_true v1 (typeof a1) -> - eval_expr e m (Expr (Eorbool a1 a2) ty) - t m1 Vtrue - | eval_Eorbool_2: forall e m a1 a2 ty t1 m1 v1 t2 m2 v2 v, - eval_expr e m a1 t1 m1 v1 -> + eval_expr (Expr (Eorbool a1 a2) ty) Vtrue + | eval_Eorbool_2: forall a1 a2 ty v1 v2 v, + eval_expr a1 v1 -> is_false v1 (typeof a1) -> - eval_expr e m1 a2 t2 m2 v2 -> + eval_expr a2 v2 -> bool_of_val v2 (typeof a2) v -> - eval_expr e m (Expr (Eorbool a1 a2) ty) - (t1 ** t2) m2 v - | eval_Eandbool_1: forall e m a1 a2 t m1 v1 ty, - eval_expr e m a1 t m1 v1 -> + eval_expr (Expr (Eorbool a1 a2) ty) v + | eval_Eandbool_1: forall a1 a2 ty v1, + eval_expr a1 v1 -> is_false v1 (typeof a1) -> - eval_expr e m (Expr (Eandbool a1 a2) ty) - t m1 Vfalse - | eval_Eandbool_2: forall e m a1 a2 ty t1 m1 v1 t2 m2 v2 v, - eval_expr e m a1 t1 m1 v1 -> + eval_expr (Expr (Eandbool a1 a2) ty) Vfalse + | eval_Eandbool_2: forall a1 a2 ty v1 v2 v, + eval_expr a1 v1 -> is_true v1 (typeof a1) -> - eval_expr e m1 a2 t2 m2 v2 -> + eval_expr a2 v2 -> bool_of_val v2 (typeof a2) v -> - eval_expr e m (Expr (Eandbool a1 a2) ty) - (t1 ** t2) m2 v - | eval_Ecast: forall e m a ty t m1 v1 v, - eval_expr e m a t m1 v1 -> + eval_expr (Expr (Eandbool a1 a2) ty) v + | eval_Ecast: forall a ty v1 v, + eval_expr a v1 -> cast v1 (typeof a) ty v -> - eval_expr e m (Expr (Ecast ty a) ty) - t m1 v - | eval_Ecall: forall e m a bl ty m3 vres t1 m1 vf t2 m2 vargs f t3, - eval_expr e m a t1 m1 vf -> - eval_exprlist e m1 bl t2 m2 vargs -> - Genv.find_funct ge vf = Some f -> - type_of_fundef f = typeof a -> - eval_funcall m2 f vargs t3 m3 vres -> - eval_expr e m (Expr (Ecall a bl) ty) - (t1 ** t2 ** t3) m3 vres - -(** [eval_lvalue ge e m1 a t m2 b ofs] defines the evaluation of - expression [a] in r-value position. The result of the evaluation - is the block reference [b] and the byte offset [ofs] of the - memory location where the value of [a] resides. - The other parameters are as in [eval_expr]. *) - -with eval_lvalue: env -> mem -> expr -> trace -> mem -> block -> int -> Prop := - | eval_Evar_local: forall e m id l ty, + eval_expr (Expr (Ecast ty a) ty) v + +(** [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a] + in l-value position. The result is the memory location [b, ofs] + that contains the value of the expression [a]. *) + +with eval_lvalue: expr -> block -> int -> Prop := + | eval_Evar_local: forall id l ty, e!id = Some l -> - eval_lvalue e m (Expr (Evar id) ty) - E0 m l Int.zero - | eval_Evar_global: forall e m id l ty, + eval_lvalue (Expr (Evar id) ty) l Int.zero + | eval_Evar_global: forall id l ty, e!id = None -> Genv.find_symbol ge id = Some l -> - eval_lvalue e m (Expr (Evar id) ty) - E0 m l Int.zero - | eval_Ederef: forall e m m1 a t ofs ty l, - eval_expr e m a t m1 (Vptr l ofs) -> - eval_lvalue e m (Expr (Ederef a) ty) - t m1 l ofs - | eval_Eindex: forall e m a1 t1 m1 v1 a2 t2 m2 v2 l ofs ty, - eval_expr e m a1 t1 m1 v1 -> - eval_expr e m1 a2 t2 m2 v2 -> + eval_lvalue (Expr (Evar id) ty) l Int.zero + | eval_Ederef: forall a ty l ofs, + eval_expr a (Vptr l ofs) -> + eval_lvalue (Expr (Ederef a) ty) l ofs + | eval_Eindex: forall a1 a2 ty v1 v2 l ofs, + eval_expr a1 v1 -> + eval_expr a2 v2 -> sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) -> - eval_lvalue e m (Expr (Eindex a1 a2) ty) - (t1 ** t2) m2 l ofs - | eval_Efield_struct: forall e m a t m1 l ofs id fList i ty delta, - eval_lvalue e m a t m1 l ofs -> + eval_lvalue (Expr (Eindex a1 a2) ty) l ofs + | eval_Efield_struct: forall a i ty l ofs id fList delta, + eval_lvalue a l ofs -> typeof a = Tstruct id fList -> field_offset i fList = OK delta -> - eval_lvalue e m (Expr (Efield a i) ty) - t m1 l (Int.add ofs (Int.repr delta)) - | eval_Efield_union: forall e m a t m1 l ofs id fList i ty, - eval_lvalue e m a t m1 l ofs -> + eval_lvalue (Expr (Efield a i) ty) l (Int.add ofs (Int.repr delta)) + | eval_Efield_union: forall a i ty l ofs id fList, + eval_lvalue a l ofs -> typeof a = Tunion id fList -> - eval_lvalue e m (Expr (Efield a i) ty) - t m1 l ofs + eval_lvalue (Expr (Efield a i) ty) l ofs. + +Scheme eval_expr_ind2 := Minimality for eval_expr Sort Prop + with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop. -(** [eval_exprlist ge e m1 al t m2 vl] evaluates a list of r-value +(** [eval_exprlist ge e m al vl] evaluates a list of r-value expressions [al] to their values [vl]. *) -with eval_exprlist: env -> mem -> exprlist -> trace -> mem -> list val -> Prop := - | eval_Enil: forall e m, - eval_exprlist e m Enil E0 m nil - | eval_Econs: forall e m a bl t1 m1 v t2 m2 vl, - eval_expr e m a t1 m1 v -> - eval_exprlist e m1 bl t2 m2 vl -> - eval_exprlist e m (Econs a bl) - (t1 ** t2) m2 (v :: vl) +Inductive eval_exprlist: list expr -> list val -> Prop := + | eval_Enil: + eval_exprlist nil nil + | eval_Econs: forall a bl v vl, + eval_expr a v -> + eval_exprlist bl vl -> + eval_exprlist (a :: bl) (v :: vl). + +End EXPR. (** [exec_stmt ge e m1 s t m2 out] describes the execution of the statement [s]. [out] is the outcome for this execution. @@ -639,20 +619,34 @@ with eval_exprlist: env -> mem -> exprlist -> trace -> mem -> list val -> Prop : [t] is the trace of input/output events performed during this evaluation. *) -with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := +Inductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := | exec_Sskip: forall e m, exec_stmt e m Sskip E0 m Out_normal - | exec_Sexpr: forall e m a t m1 v, - eval_expr e m a t m1 v -> - exec_stmt e m (Sexpr a) - t m1 Out_normal - | exec_Sassign: forall e m a1 a2 t1 m1 loc ofs t2 m2 v2 m3, - eval_lvalue e m a1 t1 m1 loc ofs -> - eval_expr e m1 a2 t2 m2 v2 -> - store_value_of_type (typeof a1) m2 loc ofs v2 = Some m3 -> + | exec_Sassign: forall e m a1 a2 loc ofs v2 m', + eval_lvalue e m a1 loc ofs -> + eval_expr e m a2 v2 -> + store_value_of_type (typeof a1) m loc ofs v2 = Some m' -> exec_stmt e m (Sassign a1 a2) - (t1 ** t2) m3 Out_normal + E0 m' Out_normal + | exec_Scall_none: forall e m a al vf vargs f t m' vres, + eval_expr e m a vf -> + eval_exprlist e m al vargs -> + Genv.find_funct ge vf = Some f -> + type_of_fundef f = typeof a -> + eval_funcall m f vargs t m' vres -> + exec_stmt e m (Scall None a al) + t m' Out_normal + | exec_Scall_some: forall e m lhs a al loc ofs vf vargs f t m' vres m'', + eval_lvalue e m lhs loc ofs -> + eval_expr e m a vf -> + eval_exprlist e m al vargs -> + Genv.find_funct ge vf = Some f -> + type_of_fundef f = typeof a -> + eval_funcall m f vargs t m' vres -> + store_value_of_type (typeof lhs) m' loc ofs vres = Some m'' -> + exec_stmt e m (Scall (Some lhs) a al) + t m'' Out_normal | exec_Sseq_1: forall e m s1 s2 t1 m1 t2 m2 out, exec_stmt e m s1 t1 m1 Out_normal -> exec_stmt e m1 s2 t2 m2 out -> @@ -663,102 +657,103 @@ with exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop := out <> Out_normal -> exec_stmt e m (Ssequence s1 s2) t1 m1 out - | exec_Sifthenelse_true: forall e m a s1 s2 t1 m1 v1 t2 m2 out, - eval_expr e m a t1 m1 v1 -> + | exec_Sifthenelse_true: forall e m a s1 s2 v1 t m' out, + eval_expr e m a v1 -> is_true v1 (typeof a) -> - exec_stmt e m1 s1 t2 m2 out -> + exec_stmt e m s1 t m' out -> exec_stmt e m (Sifthenelse a s1 s2) - (t1 ** t2) m2 out - | exec_Sifthenelse_false: forall e m a s1 s2 t1 m1 v1 t2 m2 out, - eval_expr e m a t1 m1 v1 -> + t m' out + | exec_Sifthenelse_false: forall e m a s1 s2 v1 t m' out, + eval_expr e m a v1 -> is_false v1 (typeof a) -> - exec_stmt e m1 s2 t2 m2 out -> + exec_stmt e m s2 t m' out -> exec_stmt e m (Sifthenelse a s1 s2) - (t1 ** t2) m2 out + t m' out | exec_Sreturn_none: forall e m, exec_stmt e m (Sreturn None) E0 m (Out_return None) - | exec_Sreturn_some: forall e m a t m1 v, - eval_expr e m a t m1 v -> + | exec_Sreturn_some: forall e m a v, + eval_expr e m a v -> exec_stmt e m (Sreturn (Some a)) - t m1 (Out_return (Some v)) + E0 m (Out_return (Some v)) | exec_Sbreak: forall e m, exec_stmt e m Sbreak E0 m Out_break | exec_Scontinue: forall e m, exec_stmt e m Scontinue E0 m Out_continue - | exec_Swhile_false: forall e m s a t v m1, - eval_expr e m a t m1 v -> + | exec_Swhile_false: forall e m a s v, + eval_expr e m a v -> is_false v (typeof a) -> exec_stmt e m (Swhile a s) - t m1 Out_normal - | exec_Swhile_stop: forall e m a t1 m1 v s m2 t2 out2 out, - eval_expr e m a t1 m1 v -> + E0 m Out_normal + | exec_Swhile_stop: forall e m a v s t m' out' out, + eval_expr e m a v -> is_true v (typeof a) -> - exec_stmt e m1 s t2 m2 out2 -> - out_break_or_return out2 out -> + exec_stmt e m s t m' out' -> + out_break_or_return out' out -> exec_stmt e m (Swhile a s) - (t1 ** t2) m2 out - | exec_Swhile_loop: forall e m a t1 m1 v s out2 out t2 m2 t3 m3, - eval_expr e m a t1 m1 v -> + t m' out + | exec_Swhile_loop: forall e m a s v t1 m1 out1 t2 m2 out, + eval_expr e m a v -> is_true v (typeof a) -> - exec_stmt e m1 s t2 m2 out2 -> - out_normal_or_continue out2 -> - exec_stmt e m2 (Swhile a s) t3 m3 out -> - exec_stmt e m (Swhile a s) - (t1 ** t2 ** t3) m3 out - | exec_Sdowhile_false: forall e m s a t1 m1 out1 v t2 m2, exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> - eval_expr e m1 a t2 m2 v -> + exec_stmt e m1 (Swhile a s) t2 m2 out -> + exec_stmt e m (Swhile a s) + (t1 ** t2) m2 out + | exec_Sdowhile_false: forall e m s a t m1 out1 v, + exec_stmt e m s t m1 out1 -> + out_normal_or_continue out1 -> + eval_expr e m1 a v -> is_false v (typeof a) -> exec_stmt e m (Sdowhile a s) - (t1 ** t2) m2 Out_normal + t m1 Out_normal | exec_Sdowhile_stop: forall e m s a t m1 out1 out, exec_stmt e m s t m1 out1 -> out_break_or_return out1 out -> exec_stmt e m (Sdowhile a s) t m1 out - | exec_Sdowhile_loop: forall e m s a m1 m2 m3 t1 t2 t3 out out1 v, + | exec_Sdowhile_loop: forall e m s a m1 m2 t1 t2 out out1 v, exec_stmt e m s t1 m1 out1 -> out_normal_or_continue out1 -> - eval_expr e m1 a t2 m2 v -> + eval_expr e m1 a v -> is_true v (typeof a) -> - exec_stmt e m2 (Sdowhile a s) t3 m3 out -> + exec_stmt e m1 (Sdowhile a s) t2 m2 out -> exec_stmt e m (Sdowhile a s) - (t1 ** t2 ** t3) m3 out + (t1 ** t2) m2 out | exec_Sfor_start: forall e m s a1 a2 a3 out m1 m2 t1 t2, + a1 <> Sskip -> exec_stmt e m a1 t1 m1 Out_normal -> exec_stmt e m1 (Sfor Sskip a2 a3 s) t2 m2 out -> exec_stmt e m (Sfor a1 a2 a3 s) (t1 ** t2) m2 out - | exec_Sfor_false: forall e m s a2 a3 t v m1, - eval_expr e m a2 t m1 v -> + | exec_Sfor_false: forall e m s a2 a3 v, + eval_expr e m a2 v -> is_false v (typeof a2) -> exec_stmt e m (Sfor Sskip a2 a3 s) - t m1 Out_normal - | exec_Sfor_stop: forall e m s a2 a3 v m1 m2 t1 t2 out2 out, - eval_expr e m a2 t1 m1 v -> + E0 m Out_normal + | exec_Sfor_stop: forall e m s a2 a3 v m1 t out1 out, + eval_expr e m a2 v -> is_true v (typeof a2) -> - exec_stmt e m1 s t2 m2 out2 -> - out_break_or_return out2 out -> + exec_stmt e m s t m1 out1 -> + out_break_or_return out1 out -> exec_stmt e m (Sfor Sskip a2 a3 s) - (t1 ** t2) m2 out - | exec_Sfor_loop: forall e m s a2 a3 v m1 m2 m3 m4 t1 t2 t3 t4 out2 out, - eval_expr e m a2 t1 m1 v -> + t m1 out + | exec_Sfor_loop: forall e m s a2 a3 v m1 m2 m3 t1 t2 t3 out1 out, + eval_expr e m a2 v -> is_true v (typeof a2) -> - exec_stmt e m1 s t2 m2 out2 -> - out_normal_or_continue out2 -> - exec_stmt e m2 a3 t3 m3 Out_normal -> - exec_stmt e m3 (Sfor Sskip a2 a3 s) t4 m4 out -> + exec_stmt e m s t1 m1 out1 -> + out_normal_or_continue out1 -> + exec_stmt e m1 a3 t2 m2 Out_normal -> + exec_stmt e m2 (Sfor Sskip a2 a3 s) t3 m3 out -> exec_stmt e m (Sfor Sskip a2 a3 s) - (t1 ** t2 ** t3 ** t4) m4 out - | exec_Sswitch: forall e m a t1 m1 n sl t2 m2 out, - eval_expr e m a t1 m1 (Vint n) -> - exec_lblstmts e m1 (select_switch n sl) t2 m2 out -> + (t1 ** t2 ** t3) m3 out + | exec_Sswitch: forall e m a t n sl m1 out, + eval_expr e m a (Vint n) -> + exec_lblstmts e m (select_switch n sl) t m1 out -> exec_stmt e m (Sswitch a sl) - (t1 ** t2) m2 (outcome_switch out) + t m1 (outcome_switch out) (** [exec_lblstmts ge e m1 ls t m2 out] is a variant of [exec_stmt] that executes in sequence all statements in the list of labeled @@ -791,25 +786,137 @@ with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := event_match (external_function id targs tres) vargs t vres -> eval_funcall m (External id targs tres) vargs t m vres. -Scheme eval_expr_ind6 := Minimality for eval_expr Sort Prop - with eval_lvalue_ind6 := Minimality for eval_lvalue Sort Prop - with eval_exprlist_ind6 := Minimality for eval_exprlist Sort Prop - with exec_stmt_ind6 := Minimality for exec_stmt Sort Prop - with exec_lblstmts_ind6 := Minimality for exec_lblstmts Sort Prop - with eval_funcall_ind6 := Minimality for eval_funcall Sort Prop. +Scheme exec_stmt_ind3 := Minimality for exec_stmt Sort Prop + with exec_lblstmts_ind3 := Minimality for exec_lblstmts Sort Prop + with eval_funcall_ind3 := Minimality for eval_funcall Sort Prop. + +(** Coinductive semantics for divergence. + [execinf_stmt ge e m s t] holds if the execution of statement [s] + diverges, i.e. loops infinitely. [t] is the possibly infinite + trace of observable events performed during the execution. *) + +CoInductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop := + | execinf_Scall: forall e m lhs a al vf vargs f t, + eval_expr e m a vf -> + eval_exprlist e m al vargs -> + Genv.find_funct ge vf = Some f -> + type_of_fundef f = typeof a -> + evalinf_funcall m f vargs t -> + execinf_stmt e m (Scall lhs a al) t + | execinf_Sseq_1: forall e m s1 s2 t, + execinf_stmt e m s1 t -> + execinf_stmt e m (Ssequence s1 s2) t + | execinf_Sseq_2: forall e m s1 s2 t1 m1 t2, + exec_stmt e m s1 t1 m1 Out_normal -> + execinf_stmt e m1 s2 t2 -> + execinf_stmt e m (Ssequence s1 s2) (t1 *** t2) + | execinf_Sifthenelse_true: forall e m a s1 s2 v1 t, + eval_expr e m a v1 -> + is_true v1 (typeof a) -> + execinf_stmt e m s1 t -> + execinf_stmt e m (Sifthenelse a s1 s2) t + | execinf_Sifthenelse_false: forall e m a s1 s2 v1 t, + eval_expr e m a v1 -> + is_false v1 (typeof a) -> + execinf_stmt e m s2 t -> + execinf_stmt e m (Sifthenelse a s1 s2) t + | execinf_Swhile_body: forall e m a v s t, + eval_expr e m a v -> + is_true v (typeof a) -> + execinf_stmt e m s t -> + execinf_stmt e m (Swhile a s) t + | execinf_Swhile_loop: forall e m a s v t1 m1 out1 t2, + eval_expr e m a v -> + is_true v (typeof a) -> + exec_stmt e m s t1 m1 out1 -> + out_normal_or_continue out1 -> + execinf_stmt e m1 (Swhile a s) t2 -> + execinf_stmt e m (Swhile a s) (t1 *** t2) + | execinf_Sdowhile_body: forall e m s a t, + execinf_stmt e m s t -> + execinf_stmt e m (Sdowhile a s) t + | execinf_Sdowhile_loop: forall e m s a m1 t1 t2 out1 v, + exec_stmt e m s t1 m1 out1 -> + out_normal_or_continue out1 -> + eval_expr e m1 a v -> + is_true v (typeof a) -> + execinf_stmt e m1 (Sdowhile a s) t2 -> + execinf_stmt e m (Sdowhile a s) (t1 *** t2) + | execinf_Sfor_start_1: forall e m s a1 a2 a3 t, + execinf_stmt e m a1 t -> + execinf_stmt e m (Sfor a1 a2 a3 s) t + | execinf_Sfor_start_2: forall e m s a1 a2 a3 m1 t1 t2, + a1 <> Sskip -> + exec_stmt e m a1 t1 m1 Out_normal -> + execinf_stmt e m1 (Sfor Sskip a2 a3 s) t2 -> + execinf_stmt e m (Sfor a1 a2 a3 s) (t1 *** t2) + | execinf_Sfor_body: forall e m s a2 a3 v t, + eval_expr e m a2 v -> + is_true v (typeof a2) -> + execinf_stmt e m s t -> + execinf_stmt e m (Sfor Sskip a2 a3 s) t + | execinf_Sfor_next: forall e m s a2 a3 v m1 t1 t2 out1, + eval_expr e m a2 v -> + is_true v (typeof a2) -> + exec_stmt e m s t1 m1 out1 -> + out_normal_or_continue out1 -> + execinf_stmt e m1 a3 t2 -> + execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2) + | execinf_Sfor_loop: forall e m s a2 a3 v m1 m2 t1 t2 t3 out1, + eval_expr e m a2 v -> + is_true v (typeof a2) -> + exec_stmt e m s t1 m1 out1 -> + out_normal_or_continue out1 -> + exec_stmt e m1 a3 t2 m2 Out_normal -> + execinf_stmt e m2 (Sfor Sskip a2 a3 s) t3 -> + execinf_stmt e m (Sfor Sskip a2 a3 s) (t1 *** t2 *** t3) + | execinf_Sswitch: forall e m a t n sl, + eval_expr e m a (Vint n) -> + execinf_lblstmts e m (select_switch n sl) t -> + execinf_stmt e m (Sswitch a sl) t + +with execinf_lblstmts: env -> mem -> labeled_statements -> traceinf -> Prop := + | execinf_LSdefault: forall e m s t, + execinf_stmt e m s t -> + execinf_lblstmts e m (LSdefault s) t + | execinf_LScase_body: forall e m n s ls t, + execinf_stmt e m s t -> + execinf_lblstmts e m (LScase n s ls) t + | execinf_LScase_fallthrough: forall e m n s ls t1 m1 t2, + exec_stmt e m s t1 m1 Out_normal -> + execinf_lblstmts e m1 ls t2 -> + execinf_lblstmts e m (LScase n s ls) (t1 *** t2) + +(** [evalinf_funcall ge m fd args t] holds if the invocation of function + [fd] on arguments [args] diverges, with observable trace [t]. *) + +with evalinf_funcall: mem -> fundef -> list val -> traceinf -> Prop := + | evalinf_funcall_internal: forall m f vargs t e m1 lb m2, + alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 lb -> + bind_parameters e m1 f.(fn_params) vargs m2 -> + execinf_stmt e m2 f.(fn_body) t -> + evalinf_funcall m (Internal f) vargs t. End RELSEM. -(** Execution of a whole program: [exec_program p t r] - holds if the application of [p]'s main function to no arguments - in the initial memory state for [p] performs the input/output - operations described in the trace [t], and eventually returns value [r]. -*) - -Definition exec_program (p: program) (t: trace) (r: val) : Prop := - let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in - exists b, exists f, exists m1, - Genv.find_symbol ge p.(prog_main) = Some b /\ - Genv.find_funct_ptr ge b = Some f /\ - eval_funcall ge m0 f nil t m1 r. +(** Execution of a whole program. [exec_program p beh] holds + if the application of [p]'s main function to no arguments + in the initial memory state for [p] executes without errors and produces + the observable behaviour [beh]. *) + +Inductive exec_program (p: program): program_behavior -> Prop := + | program_terminates: forall b f m1 t r, + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + eval_funcall ge m0 f nil t m1 (Vint r) -> + exec_program p (Terminates t r) + | program_diverges: forall b f t, + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + evalinf_funcall ge m0 f nil t -> + exec_program p (Diverges t). + diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 7d805c38..7afe27f2 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -10,6 +10,7 @@ Require Import Mem. Require Import Events. Require Import Globalenvs. Require Cminor. +Require Import Smallstep. (** Abstract syntax *) @@ -17,10 +18,7 @@ Require Cminor. statements, functions and programs. Expressions include reading global or local variables, reading store locations, arithmetic operations, function calls, and conditional expressions - (similar to [e1 ? e2 : e3] in C). The [Elet] and [Eletvar] constructs - enable sharing the computations of subexpressions. De Bruijn notation - is used: [Eletvar n] refers to the value bound by then [n+1]-th enclosing - [Elet] construct. + (similar to [e1 ? e2 : e3] in C). Unlike in Cminor (the next intermediate language of the back-end), Csharpminor local variables reside in memory, and their addresses can @@ -41,27 +39,19 @@ Inductive expr : Set := | Eunop : unary_operation -> expr -> expr (**r unary operation *) | Ebinop : binary_operation -> expr -> expr -> expr (**r binary operation *) | Eload : memory_chunk -> expr -> expr (**r memory read *) - | Ecall : signature -> expr -> exprlist -> expr (**r function call *) - | Econdition : expr -> expr -> expr -> expr (**r conditional expression *) - | Elet : expr -> expr -> expr (**r let binding *) - | Eletvar : nat -> expr (**r reference to a let-bound variable *) - | Ealloc : expr -> expr (**r memory allocation *) - -with exprlist : Set := - | Enil: exprlist - | Econs: expr -> exprlist -> exprlist. + | Econdition : expr -> expr -> expr -> expr. (**r conditional expression *) (** Statements include expression evaluation, variable assignment, - memory stores, an if/then/else conditional, + memory stores, function calls, an if/then/else conditional, infinite loops, blocks and early block exits, and early function returns. [Sexit n] terminates prematurely the execution of the [n+1] enclosing [Sblock] statements. *) Inductive stmt : Set := | Sskip: stmt - | Sexpr: expr -> stmt | Sassign : ident -> expr -> stmt | Sstore : memory_chunk -> expr -> expr -> stmt + | Scall : option ident -> signature -> expr -> list expr -> stmt | Sseq: stmt -> stmt -> stmt | Sifthenelse: expr -> stmt -> stmt -> stmt | Sloop: stmt -> stmt @@ -136,19 +126,17 @@ Fixpoint switch_target (n: int) (dfl: nat) (cases: list (int * nat)) | (n1, lbl1) :: rem => if Int.eq n n1 then lbl1 else switch_target n dfl rem end. -(** Four kinds of evaluation environments are involved: +(** Three kinds of evaluation environments are involved: - [genv]: global environments, define symbols and functions; - [gvarenv]: map global variables to variable informations (type [var_kind]); - [env]: local environments, map local variables - to memory blocks and variable informations; -- [lenv]: let environments, map de Bruijn indices to values. + to memory blocks and variable informations. *) Definition genv := Genv.t fundef. Definition gvarenv := PTree.t var_kind. Definition env := PTree.t (block * var_kind). Definition empty_env : env := PTree.empty (block * var_kind). -Definition letenv := list val. Definition sizeof (lv: var_kind) : Z := match lv with @@ -252,111 +240,80 @@ Inductive eval_var_ref: env -> ident -> block -> memory_chunk -> Prop := PTree.get id (global_var_env prg) = Some (Vscalar chunk) -> eval_var_ref e id b chunk. -(** Evaluation of an expression: [eval_expr prg le e m a t m' v] states - that expression [a], in initial memory state [m], evaluates to value - [v]. [m'] is the final memory state, respectively, reflecting - memory stores possibly performed by [a]. [t] is the trace of input/output - events generated during the evaluation. - [e] and [le] are the local environment and let environment respectively. *) - -Inductive eval_expr: - letenv -> env -> - mem -> expr -> trace -> mem -> val -> Prop := - | eval_Evar: - forall le e m id b chunk v, +(** Evaluation of an expression: [eval_expr prg e m a v] states + that expression [a], in initial memory state [m] and local + environment [e], evaluates to value [v]. *) + +Section EVAL_EXPR. + +Variable e: env. +Variable m: mem. + +Inductive eval_expr: expr -> val -> Prop := + | eval_Evar: forall id b chunk v, eval_var_ref e id b chunk -> Mem.load chunk m b 0 = Some v -> - eval_expr le e m (Evar id) E0 m v - | eval_Eaddrof: - forall le e m id b, + eval_expr (Evar id) v + | eval_Eaddrof: forall id b, eval_var_addr e id b -> - eval_expr le e m (Eaddrof id) E0 m (Vptr b Int.zero) - | eval_Econst: - forall le e m cst v, + eval_expr (Eaddrof id) (Vptr b Int.zero) + | eval_Econst: forall cst v, eval_constant cst = Some v -> - eval_expr le e m (Econst cst) E0 m v - | eval_Eunop: - forall le e m op a t m1 v1 v, - eval_expr le e m a t m1 v1 -> + eval_expr (Econst cst) v + | eval_Eunop: forall op a1 v1 v, + eval_expr a1 v1 -> eval_unop op v1 = Some v -> - eval_expr le e m (Eunop op a) t m1 v - | eval_Ebinop: - forall le e m op a1 a2 t1 m1 v1 t2 m2 v2 t v, - eval_expr le e m a1 t1 m1 v1 -> - eval_expr le e m1 a2 t2 m2 v2 -> - eval_binop op v1 v2 m2 = Some v -> - t = t1 ** t2 -> - eval_expr le e m (Ebinop op a1 a2) t m2 v - | eval_Eload: - forall le e m chunk a t m1 v1 v, - eval_expr le e m a t m1 v1 -> - Mem.loadv chunk m1 v1 = Some v -> - eval_expr le e m (Eload chunk a) t m1 v - | eval_Ecall: - forall le e m sig a bl t1 m1 t2 m2 t3 m3 vf vargs vres f t, - eval_expr le e m a t1 m1 vf -> - eval_exprlist le e m1 bl t2 m2 vargs -> - Genv.find_funct ge vf = Some f -> - funsig f = sig -> - eval_funcall m2 f vargs t3 m3 vres -> - t = t1 ** t2 ** t3 -> - eval_expr le e m (Ecall sig a bl) t m3 vres - | eval_Econdition_true: - forall le e m a b c t1 m1 v1 t2 m2 v2 t, - eval_expr le e m a t1 m1 v1 -> - Val.is_true v1 -> - eval_expr le e m1 b t2 m2 v2 -> - t = t1 ** t2 -> - eval_expr le e m (Econdition a b c) t m2 v2 - | eval_Econdition_false: - forall le e m a b c t1 m1 v1 t2 m2 v2 t, - eval_expr le e m a t1 m1 v1 -> - Val.is_false v1 -> - eval_expr le e m1 c t2 m2 v2 -> - t = t1 ** t2 -> - eval_expr le e m (Econdition a b c) t m2 v2 - | eval_Elet: - forall le e m a b t1 m1 v1 t2 m2 v2 t, - eval_expr le e m a t1 m1 v1 -> - eval_expr (v1::le) e m1 b t2 m2 v2 -> - t = t1 ** t2 -> - eval_expr le e m (Elet a b) t m2 v2 - | eval_Eletvar: - forall le e m n v, - nth_error le n = Some v -> - eval_expr le e m (Eletvar n) E0 m v - | eval_Ealloc: - forall le e m a t m1 n m2 b, - eval_expr le e m a t m1 (Vint n) -> - Mem.alloc m1 0 (Int.signed n) = (m2, b) -> - eval_expr le e m (Ealloc a) t m2 (Vptr b Int.zero) + eval_expr (Eunop op a1) v + | eval_Ebinop: forall op a1 a2 v1 v2 v, + eval_expr a1 v1 -> + eval_expr a2 v2 -> + eval_binop op v1 v2 m = Some v -> + eval_expr (Ebinop op a1 a2) v + | eval_Eload: forall chunk a v1 v, + eval_expr a v1 -> + Mem.loadv chunk m v1 = Some v -> + eval_expr (Eload chunk a) v + | eval_Econdition: forall a b c v1 vb1 v2, + eval_expr a v1 -> + Val.bool_of_val v1 vb1 -> + eval_expr (if vb1 then b else c) v2 -> + eval_expr (Econdition a b c) v2. (** Evaluation of a list of expressions: - [eval_exprlist prg le al m a t m' vl] - states that the list [al] of expressions evaluate - to the list [vl] of values. - The other parameters are as in [eval_expr]. -*) + [eval_exprlist prg e m al vl] states that the list [al] of + expressions evaluate to the list [vl] of values. The other + parameters are as in [eval_expr]. *) -with eval_exprlist: - letenv -> env -> - mem -> exprlist -> trace -> - mem -> list val -> Prop := +Inductive eval_exprlist: list expr -> list val -> Prop := | eval_Enil: - forall le e m, - eval_exprlist le e m Enil E0 m nil - | eval_Econs: - forall le e m a bl t1 m1 v t2 m2 vl t, - eval_expr le e m a t1 m1 v -> - eval_exprlist le e m1 bl t2 m2 vl -> - t = t1 ** t2 -> - eval_exprlist le e m (Econs a bl) t m2 (v :: vl) + eval_exprlist nil nil + | eval_Econs: forall a1 al v1 vl, + eval_expr a1 v1 -> eval_exprlist al vl -> + eval_exprlist (a1 :: al) (v1 :: vl). + +End EVAL_EXPR. + +(** Execution of an assignment to a variable. *) + +Inductive exec_assign: env -> mem -> ident -> val -> mem -> Prop := + exec_assign_intro: forall e m id v b chunk m', + eval_var_ref e id b chunk -> + Mem.store chunk m b 0 v = Some m' -> + exec_assign e m id v m'. + +Inductive exec_opt_assign: env -> mem -> option ident -> val -> mem -> Prop := + | exec_assign_none: forall e m v, + exec_opt_assign e m None v m + | exec_assign_some: forall e m id v m', + exec_assign e m id v m' -> + exec_opt_assign e m (Some id) v m'. (** Evaluation of a function invocation: [eval_funcall prg m f args t m' res] means that the function [f], applied to the arguments [args] in memory state [m], returns the value [res] in modified memory state [m']. -*) -with eval_funcall: + [t] is the trace of observable events performed during the call. *) + +Inductive eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := | eval_funcall_internal: @@ -374,6 +331,8 @@ with eval_funcall: (** Execution of a statement: [exec_stmt prg e m s t m' out] means that statement [s] executes with outcome [out]. + [m] is the initial memory state, [m'] the final memory state, + and [t] the trace of events performed. The other parameters are as in [eval_expr]. *) with exec_stmt: @@ -383,23 +342,26 @@ with exec_stmt: | exec_Sskip: forall e m, exec_stmt e m Sskip E0 m Out_normal - | exec_Sexpr: - forall e m a t m1 v, - eval_expr nil e m a t m1 v -> - exec_stmt e m (Sexpr a) t m1 Out_normal - | eval_Sassign: - forall e m id a t m1 b chunk v m2, - eval_expr nil e m a t m1 v -> - eval_var_ref e id b chunk -> - Mem.store chunk m1 b 0 v = Some m2 -> - exec_stmt e m (Sassign id a) t m2 Out_normal - | eval_Sstore: - forall e m chunk a b t1 m1 v1 t2 m2 v2 t3 m3, - eval_expr nil e m a t1 m1 v1 -> - eval_expr nil e m1 b t2 m2 v2 -> - Mem.storev chunk m2 v1 v2 = Some m3 -> - t3 = t1 ** t2 -> - exec_stmt e m (Sstore chunk a b) t3 m3 Out_normal + | exec_Sassign: + forall e m id a v m', + eval_expr e m a v -> + exec_assign e m id v m' -> + exec_stmt e m (Sassign id a) E0 m' Out_normal + | exec_Sstore: + forall e m chunk a b v1 v2 m', + eval_expr e m a v1 -> + eval_expr e m b v2 -> + Mem.storev chunk m v1 v2 = Some m' -> + exec_stmt e m (Sstore chunk a b) E0 m' Out_normal + | exec_Scall: + forall e m optid sig a bl vf vargs f t m1 vres m2, + eval_expr e m a vf -> + eval_exprlist e m bl vargs -> + Genv.find_funct ge vf = Some f -> + funsig f = sig -> + eval_funcall m f vargs t m1 vres -> + exec_opt_assign e m1 optid vres m2 -> + exec_stmt e m (Scall optid sig a bl) t m2 Out_normal | exec_Sseq_continue: forall e m s1 s2 t1 t2 m1 m2 t out, exec_stmt e m s1 t1 m1 Out_normal -> @@ -411,20 +373,12 @@ with exec_stmt: exec_stmt e m s1 t1 m1 out -> out <> Out_normal -> exec_stmt e m (Sseq s1 s2) t1 m1 out - | exec_Sifthenelse_true: - forall e m a sl1 sl2 t1 m1 v1 t2 m2 out t, - eval_expr nil e m a t1 m1 v1 -> - Val.is_true v1 -> - exec_stmt e m1 sl1 t2 m2 out -> - t = t1 ** t2 -> - exec_stmt e m (Sifthenelse a sl1 sl2) t m2 out - | exec_Sifthenelse_false: - forall e m a sl1 sl2 t1 m1 v1 t2 m2 out t, - eval_expr nil e m a t1 m1 v1 -> - Val.is_false v1 -> - exec_stmt e m1 sl2 t2 m2 out -> - t = t1 ** t2 -> - exec_stmt e m (Sifthenelse a sl1 sl2) t m2 out + | exec_Sifthenelse: + forall e m a sl1 sl2 v vb t m' out, + eval_expr e m a v -> + Val.bool_of_val v vb -> + exec_stmt e m (if vb then sl1 else sl2) t m' out -> + exec_stmt e m (Sifthenelse a sl1 sl2) t m' out | exec_Sloop_loop: forall e m sl t1 m1 t2 m2 out t, exec_stmt e m sl t1 m1 Out_normal -> @@ -444,35 +398,166 @@ with exec_stmt: forall e m n, exec_stmt e m (Sexit n) E0 m (Out_exit n) | exec_Sswitch: - forall e m a cases default t1 m1 n, - eval_expr nil e m a t1 m1 (Vint n) -> + forall e m a cases default n, + eval_expr e m a (Vint n) -> exec_stmt e m (Sswitch a cases default) - t1 m1 (Out_exit (switch_target n default cases)) + E0 m (Out_exit (switch_target n default cases)) | exec_Sreturn_none: forall e m, exec_stmt e m (Sreturn None) E0 m (Out_return None) | exec_Sreturn_some: - forall e m a t1 m1 v, - eval_expr nil e m a t1 m1 v -> - exec_stmt e m (Sreturn (Some a)) t1 m1 (Out_return (Some v)). - -Scheme eval_expr_ind4 := Minimality for eval_expr Sort Prop - with eval_exprlist_ind4 := Minimality for eval_exprlist Sort Prop - with eval_funcall_ind4 := Minimality for eval_funcall Sort Prop - with exec_stmt_ind4 := Minimality for exec_stmt Sort Prop. + forall e m a v, + eval_expr e m a v -> + exec_stmt e m (Sreturn (Some a)) E0 m (Out_return (Some v)). + +Scheme eval_funcall_ind2 := Minimality for eval_funcall Sort Prop + with exec_stmt_ind2 := Minimality for exec_stmt Sort Prop. + +(** Coinductive semantics for divergence. *) + +Inductive block_seq_context: (stmt -> stmt) -> Prop := + | block_seq_context_base_1: + block_seq_context (fun x => Sblock x) + | block_seq_context_base_2: forall s, + block_seq_context (fun x => Sseq x s) + | block_seq_context_ctx_1: forall ctx, + block_seq_context ctx -> + block_seq_context (fun x => Sblock (ctx x)) + | block_seq_context_ctx_2: forall s ctx, + block_seq_context ctx -> + block_seq_context (fun x => Sseq (ctx x) s). + +CoInductive evalinf_funcall: + mem -> fundef -> list val -> traceinf -> Prop := + | evalinf_funcall_internal: + forall m f vargs e m1 lb m2 t, + 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 f.(fn_params) vargs m2 -> + execinf_stmt e m2 f.(fn_body) t -> + evalinf_funcall m (Internal f) vargs t + +with execinf_stmt: + env -> mem -> stmt -> traceinf -> Prop := + | execinf_Scall: + forall e m optid sig a bl vf vargs f t, + eval_expr e m a vf -> + eval_exprlist e m bl vargs -> + Genv.find_funct ge vf = Some f -> + funsig f = sig -> + evalinf_funcall m f vargs t -> + execinf_stmt e m (Scall optid sig a bl) t + | execinf_Sseq_1: + forall e m s1 s2 t, + execinf_stmt e m s1 t -> + execinf_stmt e m (Sseq s1 s2) t + | execinf_Sseq_2: + forall e m s1 s2 t1 t2 m1 t, + exec_stmt e m s1 t1 m1 Out_normal -> + execinf_stmt e m1 s2 t2 -> + t = t1 *** t2 -> + execinf_stmt e m (Sseq s1 s2) t + | execinf_Sifthenelse: + forall e m a sl1 sl2 v vb t, + eval_expr e m a v -> + Val.bool_of_val v vb -> + execinf_stmt e m (if vb then sl1 else sl2) t -> + execinf_stmt e m (Sifthenelse a sl1 sl2) t + | execinf_Sloop_body: + forall e m sl t, + execinf_stmt e m sl t -> + execinf_stmt e m (Sloop sl) t + | execinf_Sloop_loop: + forall e m sl t1 m1 t2 t, + exec_stmt e m sl t1 m1 Out_normal -> + execinf_stmt e m1 (Sloop sl) t2 -> + t = t1 *** t2 -> + execinf_stmt e m (Sloop sl) t + | execinf_Sblock: + forall e m sl t, + execinf_stmt e m sl t -> + execinf_stmt e m (Sblock sl) t + | execinf_stutter: + forall n e m s t, + execinf_stmt_N n e m s t -> + execinf_stmt e m s t + | execinf_Sloop_block: + forall e m sl t1 m1 t2 t, + exec_stmt e m sl t1 m1 Out_normal -> + execinf_stmt e m1 (Sblock (Sloop sl)) t2 -> + t = t1 *** t2 -> + execinf_stmt e m (Sloop sl) t + +with execinf_stmt_N: + nat -> env -> mem -> stmt -> traceinf -> Prop := + | execinf_context: forall n e m s t ctx, + execinf_stmt e m s t -> block_seq_context ctx -> + execinf_stmt_N n e m (ctx s) t + | execinf_sleep: forall n e m s t, + execinf_stmt_N n e m s t -> + execinf_stmt_N (S n) e m s t. + +Lemma execinf_stmt_N_inv: + forall n e m s t, + execinf_stmt_N n e m s t -> + match s with + | Sblock s1 => execinf_stmt e m s1 t + | Sseq s1 s2 => execinf_stmt e m s1 t + | _ => False + end. +Proof. + assert (BASECASE: forall e m s t ctx, + execinf_stmt e m s t -> block_seq_context ctx -> + match ctx s with + | Sblock s1 => execinf_stmt e m s1 t + | Sseq s1 s2 => execinf_stmt e m s1 t + | _ => False + end). + intros. inv H0. + auto. + auto. + apply execinf_stutter with O. apply execinf_context; eauto. + apply execinf_stutter with O. apply execinf_context; eauto. + + induction n; intros; inv H. + apply BASECASE; auto. + apply BASECASE; auto. + eapply IHn; eauto. +Qed. + +Lemma execinf_Sblock_inv: + forall e m s t, + execinf_stmt e m (Sblock s) t -> + execinf_stmt e m s t. +Proof. + intros. inv H. + auto. + exact (execinf_stmt_N_inv _ _ _ _ _ H0). +Qed. End RELSEM. -(** Execution of a whole program: [exec_program p t r] +(** Execution of a whole program: [exec_program p beh] holds if the application of [p]'s main function to no arguments - in the initial memory state for [p] performs the events described - in trace [t] and eventually returns value [r]. *) - -Definition exec_program (p: program) (t: trace) (r: val) : Prop := - let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in - exists b, exists f, exists m, - Genv.find_symbol ge p.(prog_main) = Some b /\ - Genv.find_funct_ptr ge b = Some f /\ - funsig f = mksignature nil (Some Tint) /\ - eval_funcall p m0 f nil t m r. + in the initial memory state for [p] has [beh] as observable + behavior. *) + +Inductive exec_program (p: program): program_behavior -> Prop := + | program_terminates: + forall b f t m r, + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + funsig f = mksignature nil (Some Tint) -> + eval_funcall p m0 f nil t m (Vint r) -> + exec_program p (Terminates t r) + | program_diverges: + forall b f t, + let ge := Genv.globalenv p in + let m0 := Genv.init_mem p in + Genv.find_symbol ge p.(prog_main) = Some b -> + Genv.find_funct_ptr ge b = Some f -> + funsig f = mksignature nil (Some Tint) -> + evalinf_funcall p m0 f nil t -> + exec_program p (Diverges t). diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 937ea78a..6ec3757b 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -253,6 +253,14 @@ Definition make_store (addr: expr) (ty: type) (rhs: expr) := (** * Reading and writing variables *) +(** Determine if a C expression is a variable *) + +Definition is_variable (e: Csyntax.expr) : option ident := + match e with + | Expr (Csyntax.Evar id) _ => Some id + | _ => None + end. + (** [var_get id ty] returns Csharpminor code that evaluates to the value of C variable [id] with type [ty]. Note that C variables of array or function type evaluate to the address @@ -277,7 +285,19 @@ Definition var_set (id: ident) (ty: type) (rhs: expr) := | _ => Error (MSG "Cshmgen.var_set " :: CTX id :: nil) end. -(** * Translation of operators *) +(** Auxiliary for translating call statements *) + +Definition transl_lhs_call (opta: option Csyntax.expr) : res (option ident) := + match opta with + | None => OK None + | Some a => + match is_variable a with + | None => Error (msg "LHS of function call is not a variable") + | Some id => OK (Some id) + end + end. + +(** ** Translation of operators *) Definition transl_unop (op: Csyntax.unary_operation) (a: expr) (ta: type) : res expr := match op with @@ -350,15 +370,6 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : res expr := do tc <- transl_expr c; do ts <- make_add tb (typeof b) tc (typeof c); make_load ts ty - | Expr (Csyntax.Ecall b cl) _ => - match (classify_fun (typeof b)) with - | fun_case_f args res => - do tb <- transl_expr b; - do tcl <- transl_exprlist cl; - OK(Ecall (signature_of_type args res) tb tcl) - | _ => - Error(msg "Cshmgen.transl_expr(call)") - end | Expr (Csyntax.Eandbool b c) _ => do tb <- transl_expr b; do tc <- transl_expr c; @@ -413,31 +424,23 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : res expr := end | _ => Error(msg "Cshmgen.transl_lvalue") - end + end. (** [transl_exprlist al] returns a list of Csharpminor expressions that compute the values of the list [al] of Csyntax expressions. Used for function applications. *) -with transl_exprlist (al: Csyntax.exprlist): res exprlist := +Fixpoint transl_exprlist (al: list Csyntax.expr): res (list expr) := match al with - | Csyntax.Enil => OK Enil - | Csyntax.Econs a1 a2 => + | nil => OK nil + | a1 :: a2 => do ta1 <- transl_expr a1; do ta2 <- transl_exprlist a2; - OK (Econs ta1 ta2) + OK (ta1 :: ta2) end. (** * Translation of statements *) -(** Determine if a C expression is a variable *) - -Definition is_variable (e: Csyntax.expr) : option ident := - match e with - | Expr (Csyntax.Evar id) _ => Some id - | _ => None - end. - (** [exit_if_false e] return the statement that tests the boolean value of the Clight expression [e]. If [e] evaluates to false, an [exit 0] is performed. If [e] evaluates to true, the generated @@ -512,15 +515,18 @@ Fixpoint switch_table (sl: labeled_statements) (k: nat) {struct sl} : list (int | LScase ni _ rem => (ni, k) :: switch_table rem (k+1) end. +Definition is_Sskip: + forall (s: Csyntax.statement), {s = Csyntax.Sskip} + {s <> Csyntax.Sskip}. +Proof. + destruct s; ((left; reflexivity) || (right; congruence)). +Qed. + Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : res stmt := match s with | Csyntax.Sskip => OK Sskip - | Csyntax.Sexpr e => - do te <- transl_expr e; - OK (Sexpr te) | Csyntax.Sassign b c => - match (is_variable b) with + match is_variable b with | Some id => do tc <- transl_expr c; var_set id (typeof b) tc @@ -529,6 +535,15 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : r do tc <- transl_expr c; make_store tb (typeof b) tc end + | Csyntax.Scall opta b cl => + match classify_fun (typeof b) with + | fun_case_f args res => + do optid <- transl_lhs_call opta; + do tb <- transl_expr b; + do tcl <- transl_exprlist cl; + OK(Scall optid (signature_of_type args res) tb tcl) + | _ => Error(msg "Cshmgen.transl_stmt(call)") + end | Csyntax.Ssequence s1 s2 => do ts1 <- transl_statement nbrk ncnt s1; do ts2 <- transl_statement nbrk ncnt s2; @@ -547,11 +562,17 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : r do ts1 <- transl_statement 1%nat 0%nat s1; OK (Sblock (Sloop (Sseq (Sblock ts1) te))) | Csyntax.Sfor e1 e2 e3 s1 => - do te1 <- transl_statement nbrk ncnt e1; - do te2 <- exit_if_false e2; - do te3 <- transl_statement nbrk ncnt e3; - do ts1 <- transl_statement 1%nat 0%nat s1; - OK (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))) + if is_Sskip e1 then + (do te2 <- exit_if_false e2; + do te3 <- transl_statement nbrk ncnt e3; + do ts1 <- transl_statement 1%nat 0%nat s1; + OK (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))) + else + (do te1 <- transl_statement nbrk ncnt e1; + do te2 <- exit_if_false e2; + do te3 <- transl_statement nbrk ncnt e3; + do ts1 <- transl_statement 1%nat 0%nat s1; + OK (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3)))))) | Csyntax.Sbreak => OK (Sexit nbrk) | Csyntax.Scontinue => @@ -579,7 +600,7 @@ with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt) transl_lblstmts (pred nbrk) (pred ncnt) rem (Sblock (Sseq body ts)) end. -(** * Translation of functions and programs *) +(*** Translation of functions *) Definition prefix_var_name (id: ident) : errmsg := MSG "In local variable " :: CTX id :: MSG ":\n" :: nil. @@ -603,6 +624,8 @@ Definition transl_fundef (f: Csyntax.fundef) : res fundef := OK(AST.External (external_function id args res)) end. +(** ** Translation of programs *) + Definition transl_globvar (ty: type) := var_kind_of_type ty. Definition transl_program (p: Csyntax.program) : res program := diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v index b86b09bf..9930ef80 100644 --- a/cfrontend/Cshmgenproof1.v +++ b/cfrontend/Cshmgenproof1.v @@ -175,8 +175,8 @@ Proof. Qed. Lemma transl_expr_lvalue: - forall ge e m1 a ty t m2 loc ofs ta, - Csem.eval_lvalue ge e m1 (Expr a ty) t m2 loc ofs -> + forall ge e m a ty loc ofs ta, + Csem.eval_lvalue ge e m (Expr a ty) loc ofs -> transl_expr (Expr a ty) = OK ta -> (exists id, a = Csyntax.Evar id /\ var_get id ty = OK ta) \/ (exists tb, transl_lvalue (Expr a ty) = OK tb /\ @@ -188,28 +188,44 @@ Proof. monadInv H0. right. exists x; split; auto. simpl. monadInv H0. right. exists x1; split; auto. simpl. rewrite EQ; rewrite EQ1. simpl. auto. - rewrite H6 in H0. monadInv H0. right. + rewrite H4 in H0. monadInv H0. right. exists (Ebinop Oadd x (make_intconst (Int.repr x0))). split; auto. - simpl. rewrite H6. rewrite EQ. rewrite EQ1. auto. - rewrite H10 in H0. monadInv H0. right. + simpl. rewrite H4. rewrite EQ. rewrite EQ1. auto. + rewrite H6 in H0. monadInv H0. right. exists x; split; auto. - simpl. rewrite H10. auto. + simpl. rewrite H6. auto. Qed. Lemma transl_stmt_Sfor_start: forall nbrk ncnt s1 e2 s3 s4 ts, transl_statement nbrk ncnt (Sfor s1 e2 s3 s4) = OK ts -> + s1 <> Csyntax.Sskip -> exists ts1, exists ts2, ts = Sseq ts1 ts2 /\ transl_statement nbrk ncnt s1 = OK ts1 - /\ transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 s3 s4) = OK (Sseq Sskip ts2). + /\ transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 s3 s4) = OK ts2. Proof. - intros. monadInv H. econstructor; econstructor. + intros. simpl in H. destruct (is_Sskip s1). contradiction. + monadInv H. econstructor; econstructor. split. reflexivity. split. auto. simpl. + destruct (is_Sskip Csyntax.Sskip). 2: tauto. rewrite EQ1; rewrite EQ0; rewrite EQ2; auto. Qed. -(** Properties related to [switch] constructs. *) +Open Local Scope error_monad_scope. + +Lemma transl_stmt_Sfor_not_start: + forall nbrk ncnt e2 e3 s1, + transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 e3 s1) = + (do te2 <- exit_if_false e2; + do te3 <- transl_statement nbrk ncnt e3; + do ts1 <- transl_statement 1%nat 0%nat s1; + OK (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))). +Proof. + intros. simpl. destruct (is_Sskip Csyntax.Sskip). auto. congruence. +Qed. + +(** Properties related to switch constructs *) Fixpoint lblstmts_length (sl: labeled_statements) : nat := match sl with @@ -233,4 +249,33 @@ Proof. induction sl; intro; simpl. auto. decEq; auto. Qed. +Lemma block_seq_context_compose: + forall ctx2 ctx1, + block_seq_context ctx1 -> + block_seq_context ctx2 -> + block_seq_context (fun x => ctx1 (ctx2 x)). +Proof. + induction 1; intros; constructor; auto. +Qed. + +Lemma transl_lblstmts_context: + forall sl nbrk ncnt body s, + transl_lblstmts nbrk ncnt sl body = OK s -> + exists ctx, block_seq_context ctx /\ s = ctx body. +Proof. + induction sl; simpl; intros. + monadInv H. exists (fun y => Sblock (Sseq y x)); split. + apply block_seq_context_ctx_1. apply block_seq_context_base_2. + auto. + monadInv H. exploit IHsl; eauto. intros [ctx [A B]]. + exists (fun y => ctx (Sblock (Sseq y x))); split. + apply block_seq_context_compose with + (ctx1 := ctx) + (ctx2 := fun y => Sblock (Sseq y x)). + auto. apply block_seq_context_ctx_1. apply block_seq_context_base_2. + auto. +Qed. + + + diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index a75621ca..aa4e391a 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -60,17 +60,17 @@ Qed. (** * Correctness of Csharpminor construction functions *) Lemma make_intconst_correct: - forall n le e m1, - Csharpminor.eval_expr tprog le e m1 (make_intconst n) E0 m1 (Vint n). + forall n e m, + eval_expr tprog e m (make_intconst n) (Vint n). Proof. - intros. unfold make_intconst. econstructor. constructor. + intros. unfold make_intconst. econstructor. reflexivity. Qed. Lemma make_floatconst_correct: - forall n le e m1, - Csharpminor.eval_expr tprog le e m1 (make_floatconst n) E0 m1 (Vfloat n). + forall n e m, + eval_expr tprog e m (make_floatconst n) (Vfloat n). Proof. - intros. unfold make_floatconst. econstructor. constructor. + intros. unfold make_floatconst. econstructor. reflexivity. Qed. Hint Resolve make_intconst_correct make_floatconst_correct @@ -88,18 +88,18 @@ Proof. Qed. Lemma make_boolean_correct_true: - forall le e m1 a t m2 v ty, - Csharpminor.eval_expr tprog le e m1 a t m2 v -> + forall e m a v ty, + eval_expr tprog e m a v -> is_true v ty -> exists vb, - Csharpminor.eval_expr tprog le e m1 (make_boolean a ty) t m2 vb + eval_expr tprog e m (make_boolean a ty) vb /\ Val.is_true vb. Proof. intros until ty; intros EXEC VTRUE. destruct ty; simpl; try (exists v; intuition; inversion VTRUE; simpl; auto; fail). exists Vtrue; split. - econstructor; eauto with cshm. + eapply eval_Ebinop; eauto with cshm. inversion VTRUE; simpl. replace (Float.cmp Cne f0 Float.zero) with (negb (Float.cmp Ceq f0 Float.zero)). rewrite Float.eq_zero_false. reflexivity. auto. @@ -108,18 +108,18 @@ Proof. Qed. Lemma make_boolean_correct_false: - forall le e m1 a t m2 v ty, - Csharpminor.eval_expr tprog le e m1 a t m2 v -> + forall e m a v ty, + eval_expr tprog e m a v -> is_false v ty -> exists vb, - Csharpminor.eval_expr tprog le e m1 (make_boolean a ty) t m2 vb + eval_expr tprog e m (make_boolean a ty) vb /\ Val.is_false vb. Proof. intros until ty; intros EXEC VFALSE. destruct ty; simpl; try (exists v; intuition; inversion VFALSE; simpl; auto; fail). exists Vfalse; split. - econstructor; eauto with cshm. + eapply eval_Ebinop; eauto with cshm. inversion VFALSE; simpl. replace (Float.cmp Cne Float.zero Float.zero) with (negb (Float.cmp Ceq Float.zero Float.zero)). rewrite Float.eq_zero_true. reflexivity. @@ -128,38 +128,38 @@ Proof. Qed. Lemma make_neg_correct: - forall a tya c ta va v le e m1 m2, + forall a tya c va v e m, sem_neg va tya = Some v -> make_neg a tya = OK c -> - eval_expr tprog le e m1 a ta m2 va -> - eval_expr tprog le e m1 c ta m2 v. + eval_expr tprog e m a va -> + eval_expr tprog e m c v. Proof. - intros until m2; intro SEM. unfold make_neg. + intros until m; intro SEM. unfold make_neg. functional inversion SEM; intros. - inversion H4. econstructor; eauto with cshm. + inversion H4. eapply eval_Eunop; eauto with cshm. inversion H4. eauto with cshm. Qed. Lemma make_notbool_correct: - forall a tya c ta va v le e m1 m2, + forall a tya c va v e m, sem_notbool va tya = Some v -> make_notbool a tya = c -> - eval_expr tprog le e m1 a ta m2 va -> - eval_expr tprog le e m1 c ta m2 v. + eval_expr tprog e m a va -> + eval_expr tprog e m c v. Proof. - intros until m2; intro SEM. unfold make_notbool. + intros until m; intro SEM. unfold make_notbool. functional inversion SEM; intros; inversion H4; simpl; eauto with cshm. Qed. Lemma make_notint_correct: - forall a tya c ta va v le e m1 m2, + forall a tya c va v e m, sem_notint va = Some v -> make_notint a tya = c -> - eval_expr tprog le e m1 a ta m2 va -> - eval_expr tprog le e m1 c ta m2 v. + eval_expr tprog e m a va -> + eval_expr tprog e m c v. Proof. - intros until m2; intro SEM. unfold make_notint. + intros until m; intro SEM. unfold make_notint. functional inversion SEM; intros. inversion H2; eauto with cshm. Qed. @@ -167,143 +167,141 @@ Qed. Definition binary_constructor_correct (make: expr -> type -> expr -> type -> res expr) (sem: val -> type -> val -> type -> option val): Prop := - forall a tya b tyb c ta va tb vb v le e m1 m2 m3, + forall a tya b tyb c va vb v e m, sem va tya vb tyb = Some v -> make a tya b tyb = OK c -> - eval_expr tprog le e m1 a ta m2 va -> - eval_expr tprog le e m2 b tb m3 vb -> - eval_expr tprog le e m1 c (ta ** tb) m3 v. + eval_expr tprog e m a va -> + eval_expr tprog e m b vb -> + eval_expr tprog e m c v. Definition binary_constructor_correct' (make: expr -> type -> expr -> type -> res expr) (sem: val -> val -> option val): Prop := - forall a tya b tyb c ta va tb vb v le e m1 m2 m3, + forall a tya b tyb c va vb v e m, sem va vb = Some v -> make a tya b tyb = OK c -> - eval_expr tprog le e m1 a ta m2 va -> - eval_expr tprog le e m2 b tb m3 vb -> - eval_expr tprog le e m1 c (ta ** tb) m3 v. + eval_expr tprog e m a va -> + eval_expr tprog e m b vb -> + eval_expr tprog e m c v. Lemma make_add_correct: binary_constructor_correct make_add sem_add. Proof. - red; intros until m3. intro SEM. unfold make_add. + red; intros until m. intro SEM. unfold make_add. functional inversion SEM; rewrite H0; intros. inversion H7. eauto with cshm. inversion H7. eauto with cshm. inversion H7. - econstructor. eauto. - econstructor. eauto with cshm. eauto. + eapply eval_Ebinop. eauto. + eapply eval_Ebinop. eauto with cshm. eauto. simpl. reflexivity. reflexivity. - simpl. reflexivity. traceEq. Qed. Lemma make_sub_correct: binary_constructor_correct make_sub sem_sub. Proof. - red; intros until m3. intro SEM. unfold make_sub. + red; intros until m. intro SEM. unfold make_sub. functional inversion SEM; rewrite H0; intros; inversion H7; eauto with cshm. - econstructor. eauto. - econstructor. eauto with cshm. eauto. + eapply eval_Ebinop. eauto. + eapply eval_Ebinop. eauto with cshm. eauto. simpl. reflexivity. reflexivity. - simpl. reflexivity. traceEq. - inversion H9. econstructor. - econstructor; eauto. + inversion H9. eapply eval_Ebinop. + eapply eval_Ebinop; eauto. simpl. unfold eq_block; rewrite H3. reflexivity. - eauto with cshm. simpl. rewrite H8. reflexivity. traceEq. + eauto with cshm. simpl. rewrite H8. reflexivity. Qed. Lemma make_mul_correct: binary_constructor_correct make_mul sem_mul. Proof. - red; intros until m3. intro SEM. unfold make_mul. + red; intros until m. intro SEM. unfold make_mul. functional inversion SEM; rewrite H0; intros; inversion H7; eauto with cshm. Qed. Lemma make_div_correct: binary_constructor_correct make_div sem_div. Proof. - red; intros until m3. intro SEM. unfold make_div. + red; intros until m. intro SEM. unfold make_div. functional inversion SEM; rewrite H0; intros. - inversion H8. econstructor; eauto with cshm. + inversion H8. eapply eval_Ebinop; eauto with cshm. simpl. rewrite H7; auto. - inversion H8. econstructor; eauto with cshm. + inversion H8. eapply eval_Ebinop; eauto with cshm. simpl. rewrite H7; auto. inversion H7; eauto with cshm. Qed. Lemma make_mod_correct: binary_constructor_correct make_mod sem_mod. - red; intros until m3. intro SEM. unfold make_mod. + red; intros until m. intro SEM. unfold make_mod. functional inversion SEM; rewrite H0; intros. - inversion H8. econstructor; eauto with cshm. + inversion H8. eapply eval_Ebinop; eauto with cshm. simpl. rewrite H7; auto. - inversion H8. econstructor; eauto with cshm. + inversion H8. eapply eval_Ebinop; eauto with cshm. simpl. rewrite H7; auto. Qed. Lemma make_and_correct: binary_constructor_correct' make_and sem_and. Proof. - red; intros until m3. intro SEM. unfold make_and. + red; intros until m. intro SEM. unfold make_and. functional inversion SEM. intros. inversion H4. eauto with cshm. Qed. Lemma make_or_correct: binary_constructor_correct' make_or sem_or. Proof. - red; intros until m3. intro SEM. unfold make_or. + red; intros until m. intro SEM. unfold make_or. functional inversion SEM. intros. inversion H4. eauto with cshm. Qed. Lemma make_xor_correct: binary_constructor_correct' make_xor sem_xor. Proof. - red; intros until m3. intro SEM. unfold make_xor. + red; intros until m. intro SEM. unfold make_xor. functional inversion SEM. intros. inversion H4. eauto with cshm. Qed. Lemma make_shl_correct: binary_constructor_correct' make_shl sem_shl. Proof. - red; intros until m3. intro SEM. unfold make_shl. + red; intros until m. intro SEM. unfold make_shl. functional inversion SEM. intros. inversion H5. - econstructor; eauto with cshm. + eapply eval_Ebinop; eauto with cshm. simpl. rewrite H4. auto. Qed. Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr. Proof. - red; intros until m3. intro SEM. unfold make_shr. + red; intros until m. intro SEM. unfold make_shr. functional inversion SEM; intros; rewrite H0 in H8; inversion H8. - econstructor; eauto with cshm. + eapply eval_Ebinop; eauto with cshm. simpl; rewrite H7; auto. - econstructor; eauto with cshm. + eapply eval_Ebinop; eauto with cshm. simpl; rewrite H7; auto. Qed. Lemma make_cmp_correct: - forall cmp a tya b tyb c ta va tb vb v le e m1 m2 m3, - sem_cmp cmp va tya vb tyb m3 = Some v -> + forall cmp a tya b tyb c va vb v e m, + sem_cmp cmp va tya vb tyb m = Some v -> make_cmp cmp a tya b tyb = OK c -> - eval_expr tprog le e m1 a ta m2 va -> - eval_expr tprog le e m2 b tb m3 vb -> - eval_expr tprog le e m1 c (ta ** tb) m3 v. + eval_expr tprog e m a va -> + eval_expr tprog e m b vb -> + eval_expr tprog e m c v. Proof. - intros until m3. intro SEM. unfold make_cmp. + intros until m. intro SEM. unfold make_cmp. functional inversion SEM; rewrite H0; intros. inversion H8. eauto with cshm. inversion H8. eauto with cshm. inversion H8. eauto with cshm. - inversion H9. econstructor; eauto with cshm. + inversion H9. eapply eval_Ebinop; eauto with cshm. simpl. functional inversion H; subst; unfold eval_compare_null; rewrite H8; auto. - inversion H10. econstructor; eauto with cshm. + inversion H10. eapply eval_Ebinop; eauto with cshm. simpl. rewrite H3. unfold eq_block; rewrite H9. auto. Qed. Lemma transl_unop_correct: - forall op a tya c ta va v le e m1 m2, + forall op a tya c va v e m, transl_unop op a tya = OK c -> sem_unary_operation op va tya = Some v -> - eval_expr tprog le e m1 a ta m2 va -> - eval_expr tprog le e m1 c ta m2 v. + eval_expr tprog e m a va -> + eval_expr tprog e m c v. Proof. intros. destruct op; simpl in *. eapply make_notbool_correct; eauto. congruence. @@ -312,12 +310,12 @@ Proof. Qed. Lemma transl_binop_correct: -forall op a tya b tyb c ta va tb vb v le e m1 m2 m3, + forall op a tya b tyb c va vb v e m, transl_binop op a tya b tyb = OK c -> - sem_binary_operation op va tya vb tyb m3 = Some v -> - eval_expr tprog le e m1 a ta m2 va -> - eval_expr tprog le e m2 b tb m3 vb -> - eval_expr tprog le e m1 c (ta ** tb) m3 v. + sem_binary_operation op va tya vb tyb m = Some v -> + eval_expr tprog e m a va -> + eval_expr tprog e m b vb -> + eval_expr tprog e m c v. Proof. intros. destruct op; simpl in *. eapply make_add_correct; eauto. @@ -339,10 +337,10 @@ Proof. Qed. Lemma make_cast_correct: - forall le e m1 a t m2 v ty1 ty2 v', - eval_expr tprog le e m1 a t m2 v -> + forall e m a v ty1 ty2 v', + eval_expr tprog e m a v -> cast v ty1 ty2 v' -> - eval_expr tprog le e m1 (make_cast ty1 ty2 a) t m2 v'. + eval_expr tprog e m (make_cast ty1 ty2 a) v'. Proof. unfold make_cast, make_cast1, make_cast2. intros until v'; intros EVAL CAST. @@ -362,14 +360,14 @@ Proof. Qed. Lemma make_load_correct: - forall addr ty code b ofs v le e m1 t m2, + forall addr ty code b ofs v e m, make_load addr ty = OK code -> - eval_expr tprog le e m1 addr t m2 (Vptr b ofs) -> - load_value_of_type ty m2 b ofs = Some v -> - eval_expr tprog le e m1 code t m2 v. + eval_expr tprog e m addr (Vptr b ofs) -> + load_value_of_type ty m b ofs = Some v -> + eval_expr tprog e m code v. Proof. unfold make_load, load_value_of_type. - intros until m2; intros MKLOAD EVEXP LDVAL. + intros until m; intros MKLOAD EVEXP LDVAL. destruct (access_mode ty); inversion MKLOAD. (* access_mode ty = By_value m *) apply eval_Eload with (Vptr b ofs); auto. @@ -378,18 +376,18 @@ Proof. Qed. Lemma make_store_correct: - forall addr ty rhs code e m1 t1 m2 b ofs t2 m3 v m4, + forall addr ty rhs code e m b ofs v m', make_store addr ty rhs = OK code -> - eval_expr tprog nil e m1 addr t1 m2 (Vptr b ofs) -> - eval_expr tprog nil e m2 rhs t2 m3 v -> - store_value_of_type ty m3 b ofs v = Some m4 -> - exec_stmt tprog e m1 code (t1 ** t2) m4 Out_normal. + eval_expr tprog e m addr (Vptr b ofs) -> + eval_expr tprog e m rhs v -> + store_value_of_type ty m b ofs v = Some m' -> + exec_stmt tprog e m code E0 m' Out_normal. Proof. unfold make_store, store_value_of_type. - intros until m4; intros MKSTORE EV1 EV2 STVAL. + intros until m'; intros MKSTORE EV1 EV2 STVAL. destruct (access_mode ty); inversion MKSTORE. (* access_mode ty = By_value m *) - eapply eval_Sstore; eauto. + eapply exec_Sstore; eauto. Qed. End CONSTRUCTORS. diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index 10f48f61..54f9b772 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -10,6 +10,7 @@ Require Import Values. Require Import Events. Require Import Mem. Require Import Globalenvs. +Require Import Smallstep. Require Import Csyntax. Require Import Csem. Require Import Ctyping. @@ -307,13 +308,13 @@ Qed. (** Correctness of the code generated by [var_get]. *) Lemma var_get_correct: - forall e m id ty loc ofs v tyenv code te le, - Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) E0 m loc ofs -> + forall e m id ty loc ofs v tyenv code te, + Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) loc ofs -> load_value_of_type ty m loc ofs = Some v -> wt_expr tyenv (Expr (Csyntax.Evar id) ty) -> var_get id ty = OK code -> match_env tyenv e te -> - eval_expr tprog le te m code E0 m v. + eval_expr tprog te m code v. Proof. intros. inversion H1; subst; clear H1. unfold load_value_of_type in H0. @@ -356,14 +357,14 @@ Qed. (** Correctness of the code generated by [var_set]. *) Lemma var_set_correct: - forall e m id ty m1 loc ofs t1 m2 v t2 m3 tyenv code te rhs, - Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) t1 m1 loc ofs -> - store_value_of_type ty m2 loc ofs v = Some m3 -> + forall e m id ty loc ofs v m' tyenv code te rhs, + 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 nil te m1 rhs t2 m2 v -> - exec_stmt tprog te m code (t1 ** t2) m3 Out_normal. + eval_expr tprog te m rhs v -> + exec_stmt tprog te m code E0 m' Out_normal. Proof. intros. inversion H1; subst; clear H1. unfold store_value_of_type in H0. @@ -372,16 +373,16 @@ Proof. (* access mode By_value *) intros chunk ACC. rewrite ACC in H0. rewrite ACC in H2. inversion H2; clear H2; subst. - inversion H; subst; clear H; rewrite E0_left. + 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 eval_Sassign. eauto. - eapply eval_var_ref_local. eauto. assumption. + eapply exec_Sassign. eauto. + econstructor. eapply eval_var_ref_local. eauto. assumption. (* global variable *) exploit me_global; eauto. intros [A B]. - eapply eval_Sassign. eauto. - eapply eval_var_ref_global. auto. + eapply exec_Sassign. eauto. + econstructor. eapply eval_var_ref_global. auto. fold tge. rewrite symbols_preserved. eauto. eauto. assumption. (* access mode By_reference *) @@ -390,158 +391,145 @@ Proof. intros. rewrite H1 in H0; discriminate. Qed. -(** * Proof of semantic simulation *) +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 -> + 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 *) + 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. +Qed. + +(** * Proof of semantic preservation *) + +(** ** Semantic preservation for expressions *) -(** The proof of semantic preservation for this compiler pass relies - on simulation diagrams of the following form: +(** The proof of semantic preservation for the translation of expressions + relies on simulation diagrams of the following form: << - e, m1, a ------------------- te, m1, ta + e, m, a ------------------- te, m, ta | | t| |t | | v v - e, m2, v ------------------- te, m2, v + e, m, v ------------------- te, m, v >> - Left: evaluation of expression [a] in Clight. + Left: evaluation of r-value expression [a] in Clight. Right: evaluation of its translation [ta] in Csharpminor. Top (precondition): matching between environments [e], [te], plus well-typedness of expression [a]. - Bottom (postcondition): the result values [v] and final memory states [m2] + Bottom (postcondition): the result values [v] are identical in both evaluations. We state these diagrams as the following properties, parameterized by the Clight evaluation. *) -Definition eval_expr_prop - (e: Csem.env) (m1: mem) (a: Csyntax.expr) (t: trace) (m2: mem) (v: val) : Prop := - forall tyenv ta te tle +Section EXPR. + +Variable e: Csem.env. +Variable m: mem. +Variable te: Csharpminor.env. +Variable tyenv: typenv. +Hypothesis MENV: match_env tyenv e te. + +Definition eval_expr_prop (a: Csyntax.expr) (v: val) : Prop := + forall ta (WT: wt_expr tyenv a) - (TR: transl_expr a = OK ta) - (MENV: match_env tyenv e te), - Csharpminor.eval_expr tprog tle te m1 ta t m2 v. + (TR: transl_expr a = OK ta), + Csharpminor.eval_expr tprog te m ta v. -Definition eval_lvalue_prop - (e: Csem.env) (m1: mem) (a: Csyntax.expr) (t: trace) - (m2: mem) (b: block) (ofs: int) : Prop := - forall tyenv ta te tle +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) - (MENV: match_env tyenv e te), - Csharpminor.eval_expr tprog tle te m1 ta t m2 (Vptr b ofs). + (TR: transl_lvalue a = OK ta), + Csharpminor.eval_expr tprog te m ta (Vptr b ofs). -Definition eval_exprlist_prop - (e: Csem.env) (m1: mem) (al: Csyntax.exprlist) (t: trace) - (m2: mem) (vl: list val) : Prop := - forall tyenv tal te tle +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) - (MENV: match_env tyenv e te), - Csharpminor.eval_exprlist tprog tle te m1 tal t m2 vl. - -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. + (TR: transl_exprlist al = OK tal), + Csharpminor.eval_exprlist tprog te m tal vl. -(** The proof of semantic preservation is by induction on the Clight - evaluation derivation. Since this proof is large, we break it - into one lemma for each Clight evaluation rule. *) +(* Check (eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop).*) Lemma transl_Econst_int_correct: - (forall (e : Csem.env) (m : mem) (i : int) (ty : type), - eval_expr_prop e m (Expr (Econst_int i) ty) E0 m (Vint i)). + forall (i : int) (ty : type), + eval_expr_prop (Expr (Econst_int i) ty) (Vint i). Proof. intros; red; intros. monadInv TR. apply make_intconst_correct. Qed. Lemma transl_Econst_float_correct: - (forall (e : Csem.env) (m : mem) (f0 : float) (ty : type), - eval_expr_prop e m (Expr (Econst_float f0) ty) E0 m (Vfloat f0)). + forall (f0 : float) (ty : type), + eval_expr_prop (Expr (Econst_float f0) ty) (Vfloat f0). Proof. intros; red; intros. monadInv TR. apply make_floatconst_correct. Qed. Lemma transl_Elvalue_correct: - (forall (e : Csem.env) (m : mem) (a : expr_descr) (ty : type) - (t : trace) (m1 : mem) (loc : block) (ofs : int) (v : val), - eval_lvalue ge e m (Expr a ty) t m1 loc ofs -> - eval_lvalue_prop e m (Expr a ty) t m1 loc ofs -> - load_value_of_type ty m1 loc ofs = Some v -> - eval_expr_prop e m (Expr a ty) t m1 v). + forall (a : expr_descr) (ty : type) (loc : block) (ofs : int) + (v : val), + eval_lvalue ge e m (Expr a ty) loc ofs -> + eval_lvalue_prop (Expr a ty) loc ofs -> + load_value_of_type ty m loc ofs = Some v -> + eval_expr_prop (Expr a ty) v. Proof. intros; red; intros. exploit transl_expr_lvalue; eauto. intros [[id [EQ VARGET]] | [tb [TRLVAL MKLOAD]]]. (* Case a is a variable *) - subst a. - assert (t = E0 /\ m1 = m). inversion H; auto. - destruct H2; subst t m1. - eapply var_get_correct; eauto. + subst a. eapply var_get_correct; eauto. (* Case a is another lvalue *) eapply make_load_correct; eauto. Qed. Lemma transl_Eaddrof_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace) - (m1 : mem) (loc : block) (ofs : int) (ty : type), - eval_lvalue ge e m a t m1 loc ofs -> - eval_lvalue_prop e m a t m1 loc ofs -> - eval_expr_prop e m (Expr (Csyntax.Eaddrof a) ty) t m1 (Vptr loc ofs)). + forall (a : Csyntax.expr) (ty : type) (loc : block) (ofs : int), + eval_lvalue ge e m a loc ofs -> + eval_lvalue_prop a loc ofs -> + eval_expr_prop (Expr (Csyntax.Eaddrof a) ty) (Vptr loc ofs). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR. eauto. Qed. Lemma transl_Esizeof_correct: - (forall (e : Csem.env) (m : mem) (ty' ty : type), - eval_expr_prop e m (Expr (Esizeof ty') ty) E0 m - (Vint (Int.repr (Csyntax.sizeof ty')))). + forall ty' ty : type, + eval_expr_prop (Expr (Esizeof ty') ty) + (Vint (Int.repr (Csyntax.sizeof ty'))). Proof. intros; red; intros. monadInv TR. apply make_intconst_correct. Qed. Lemma transl_Eunop_correct: - (forall (e : Csem.env) (m : mem) (op : Csyntax.unary_operation) - (a : Csyntax.expr) (ty : type) (t : trace) (m1 : mem) (v1 v : val), - Csem.eval_expr ge e m a t m1 v1 -> - eval_expr_prop e m a t m1 v1 -> - sem_unary_operation op v1 (typeof a) = Some v -> - eval_expr_prop e m (Expr (Csyntax.Eunop op a) ty) t m1 v). + forall (op : Csyntax.unary_operation) (a : Csyntax.expr) (ty : type) + (v1 v : val), + Csem.eval_expr ge e m a v1 -> + eval_expr_prop a v1 -> + sem_unary_operation op v1 (typeof a) = Some v -> + eval_expr_prop (Expr (Csyntax.Eunop op a) ty) v. Proof. intros; red; intros. inversion WT; clear WT; subst. @@ -550,15 +538,14 @@ Proof. Qed. Lemma transl_Ebinop_correct: - (forall (e : Csem.env) (m : mem) (op : Csyntax.binary_operation) - (a1 a2 : Csyntax.expr) (ty : type) (t1 : trace) (m1 : mem) - (v1 : val) (t2 : trace) (m2 : mem) (v2 v : val), - Csem.eval_expr ge e m a1 t1 m1 v1 -> - eval_expr_prop e m a1 t1 m1 v1 -> - Csem.eval_expr ge e m1 a2 t2 m2 v2 -> - eval_expr_prop e m1 a2 t2 m2 v2 -> - sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m2 = Some v -> - eval_expr_prop e m (Expr (Csyntax.Ebinop op a1 a2) ty) (t1 ** t2) m2 v). + forall (op : Csyntax.binary_operation) (a1 a2 : Csyntax.expr) + (ty : type) (v1 v2 v : val), + Csem.eval_expr ge e m a1 v1 -> + eval_expr_prop a1 v1 -> + Csem.eval_expr ge e m a2 v2 -> + eval_expr_prop a2 v2 -> + sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v -> + eval_expr_prop (Expr (Csyntax.Ebinop op a1 a2) ty) v. Proof. intros; red; intros. inversion WT; clear WT; subst. @@ -567,137 +554,93 @@ Proof. Qed. Lemma transl_Eorbool_1_correct: - (forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (t : trace) - (m1 : mem) (v1 : val) (ty : type), - Csem.eval_expr ge e m a1 t m1 v1 -> - eval_expr_prop e m a1 t m1 v1 -> - is_true v1 (typeof a1) -> - eval_expr_prop e m (Expr (Eorbool a1 a2) ty) t m1 Vtrue). + forall (a1 a2 : Csyntax.expr) (ty : type) (v1 : val), + Csem.eval_expr ge e m a1 v1 -> + eval_expr_prop a1 v1 -> + is_true v1 (typeof a1) -> + eval_expr_prop (Expr (Eorbool a1 a2) ty) Vtrue. Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. unfold make_orbool. exploit make_boolean_correct_true; eauto. intros [vb [EVAL ISTRUE]]. - eapply eval_Econdition_true; eauto. - unfold Vtrue; apply make_intconst_correct. traceEq. + eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto. + simpl. unfold Vtrue; apply make_intconst_correct. Qed. Lemma transl_Eorbool_2_correct: - (forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (ty : type) - (t1 : trace) (m1 : mem) (v1 : val) (t2 : trace) (m2 : mem) - (v2 v : val), - Csem.eval_expr ge e m a1 t1 m1 v1 -> - eval_expr_prop e m a1 t1 m1 v1 -> - is_false v1 (typeof a1) -> - Csem.eval_expr ge e m1 a2 t2 m2 v2 -> - eval_expr_prop e m1 a2 t2 m2 v2 -> - bool_of_val v2 (typeof a2) v -> - eval_expr_prop e m (Expr (Eorbool a1 a2) ty) (t1 ** t2) m2 v). + forall (a1 a2 : Csyntax.expr) (ty : type) (v1 v2 v : val), + Csem.eval_expr ge e m a1 v1 -> + eval_expr_prop a1 v1 -> + is_false v1 (typeof a1) -> + Csem.eval_expr ge e m a2 v2 -> + eval_expr_prop a2 v2 -> + bool_of_val v2 (typeof a2) v -> + eval_expr_prop (Expr (Eorbool a1 a2) ty) v. Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. unfold make_orbool. exploit make_boolean_correct_false. eapply H0; eauto. eauto. intros [vb [EVAL ISFALSE]]. - eapply eval_Econdition_false; eauto. - inversion H4; subst. + eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto. + simpl. inversion H4; subst. exploit make_boolean_correct_true. eapply H3; eauto. eauto. intros [vc [EVAL' ISTRUE']]. - eapply eval_Econdition_true; eauto. - unfold Vtrue; apply make_intconst_correct. traceEq. + eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto. + unfold Vtrue; apply make_intconst_correct. exploit make_boolean_correct_false. eapply H3; eauto. eauto. intros [vc [EVAL' ISFALSE']]. - eapply eval_Econdition_false; eauto. - unfold Vfalse; apply make_intconst_correct. traceEq. + eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto. + unfold Vfalse; apply make_intconst_correct. Qed. Lemma transl_Eandbool_1_correct: - (forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (t : trace) - (m1 : mem) (v1 : val) (ty : type), - Csem.eval_expr ge e m a1 t m1 v1 -> - eval_expr_prop e m a1 t m1 v1 -> - is_false v1 (typeof a1) -> - eval_expr_prop e m (Expr (Eandbool a1 a2) ty) t m1 Vfalse). + forall (a1 a2 : Csyntax.expr) (ty : type) (v1 : val), + Csem.eval_expr ge e m a1 v1 -> + eval_expr_prop a1 v1 -> + is_false v1 (typeof a1) -> + eval_expr_prop (Expr (Eandbool a1 a2) ty) Vfalse. Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. unfold make_andbool. exploit make_boolean_correct_false; eauto. intros [vb [EVAL ISFALSE]]. - eapply eval_Econdition_false; eauto. - unfold Vfalse; apply make_intconst_correct. traceEq. + eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto. + unfold Vfalse; apply make_intconst_correct. Qed. Lemma transl_Eandbool_2_correct: - (forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (ty : type) - (t1 : trace) (m1 : mem) (v1 : val) (t2 : trace) (m2 : mem) - (v2 v : val), - Csem.eval_expr ge e m a1 t1 m1 v1 -> - eval_expr_prop e m a1 t1 m1 v1 -> - is_true v1 (typeof a1) -> - Csem.eval_expr ge e m1 a2 t2 m2 v2 -> - eval_expr_prop e m1 a2 t2 m2 v2 -> - bool_of_val v2 (typeof a2) v -> - eval_expr_prop e m (Expr (Eandbool a1 a2) ty) (t1 ** t2) m2 v). + forall (a1 a2 : Csyntax.expr) (ty : type) (v1 v2 v : val), + Csem.eval_expr ge e m a1 v1 -> + eval_expr_prop a1 v1 -> + is_true v1 (typeof a1) -> + Csem.eval_expr ge e m a2 v2 -> + eval_expr_prop a2 v2 -> + bool_of_val v2 (typeof a2) v -> + eval_expr_prop (Expr (Eandbool a1 a2) ty) v. Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. unfold make_andbool. exploit make_boolean_correct_true. eapply H0; eauto. eauto. intros [vb [EVAL ISTRUE]]. - eapply eval_Econdition_true; eauto. - inversion H4; subst. + eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto. + simpl. inversion H4; subst. exploit make_boolean_correct_true. eapply H3; eauto. eauto. intros [vc [EVAL' ISTRUE']]. - eapply eval_Econdition_true; eauto. - unfold Vtrue; apply make_intconst_correct. traceEq. + eapply eval_Econdition; eauto. apply Val.bool_of_true_val; eauto. + unfold Vtrue; apply make_intconst_correct. exploit make_boolean_correct_false. eapply H3; eauto. eauto. intros [vc [EVAL' ISFALSE']]. - eapply eval_Econdition_false; eauto. - unfold Vfalse; apply make_intconst_correct. traceEq. + eapply eval_Econdition; eauto. apply Val.bool_of_false_val; eauto. + unfold Vfalse; apply make_intconst_correct. Qed. Lemma transl_Ecast_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (ty : type) - (t : trace) (m1 : mem) (v1 v : val), - Csem.eval_expr ge e m a t m1 v1 -> - eval_expr_prop e m a t m1 v1 -> - cast v1 (typeof a) ty v -> - eval_expr_prop e m (Expr (Ecast ty a) ty) t m1 v). + forall (a : Csyntax.expr) (ty : type) (v1 v : val), + Csem.eval_expr ge e m a v1 -> + eval_expr_prop a v1 -> + cast v1 (typeof a) ty v -> eval_expr_prop (Expr (Ecast ty a) ty) v. Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. eapply make_cast_correct; eauto. Qed. -Lemma transl_Ecall_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) - (bl : Csyntax.exprlist) (ty : type) (m3 : mem) (vres : val) - (t1 : trace) (m1 : mem) (vf : val) (t2 : trace) (m2 : mem) - (vargs : list val) (f : Csyntax.fundef) (t3 : trace), - Csem.eval_expr ge e m a t1 m1 vf -> - eval_expr_prop e m a t1 m1 vf -> - Csem.eval_exprlist ge e m1 bl t2 m2 vargs -> - eval_exprlist_prop e m1 bl t2 m2 vargs -> - Genv.find_funct ge vf = Some f -> - type_of_fundef f = typeof a -> - Csem.eval_funcall ge m2 f vargs t3 m3 vres -> - eval_funcall_prop m2 f vargs t3 m3 vres -> - eval_expr_prop e m (Expr (Csyntax.Ecall a bl) ty) (t1 ** t2 ** t3) m3 - vres). -Proof. - intros; red; intros. - inversion WT; clear WT; subst. - simpl in TR. - caseEq (classify_fun (typeof a)). - 2: intros; rewrite H7 in TR; discriminate. - intros targs tres EQ. rewrite EQ in TR. - monadInv TR. - rewrite <- H4 in EQ. - exploit functions_translated; eauto. intros [tf [FIND TRL]]. - econstructor. - eapply H0; eauto. - eapply H2; eauto. - eexact FIND. - eapply transl_fundef_sig1; eauto. - eapply H6; eauto. - eapply functions_well_typed; eauto. - auto. -Qed. - Lemma transl_Evar_local_correct: - (forall (e : Csem.env) (m : mem) (id : positive) (l : block) - (ty : type), - e ! id = Some l -> - eval_lvalue_prop e m (Expr (Csyntax.Evar id) ty) E0 m l Int.zero). + forall (id : ident) (l : block) (ty : type), + e ! id = Some l -> + 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]]. @@ -705,11 +648,10 @@ Proof. Qed. Lemma transl_Evar_global_correct: - (forall (e : PTree.t block) (m : mem) (id : positive) (l : block) - (ty : type), - e ! id = None -> - Genv.find_symbol ge id = Some l -> - eval_lvalue_prop e m (Expr (Csyntax.Evar id) ty) E0 m l Int.zero). + forall (id : ident) (l : block) (ty : type), + e ! id = None -> + Genv.find_symbol ge id = Some l -> + eval_lvalue_prop (Expr (Csyntax.Evar id) ty) l Int.zero. Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. exploit (me_global _ _ _ MENV); eauto. intros [A B]. @@ -718,83 +660,183 @@ Proof. Qed. Lemma transl_Ederef_correct: - (forall (e : Csem.env) (m m1 : mem) (a : Csyntax.expr) (t : trace) - (ofs : int) (ty : type) (l : block), - Csem.eval_expr ge e m a t m1 (Vptr l ofs) -> - eval_expr_prop e m a t m1 (Vptr l ofs) -> - eval_lvalue_prop e m (Expr (Ederef a) ty) t m1 l ofs). + forall (a : Csyntax.expr) (ty : type) (l : block) (ofs : int), + Csem.eval_expr ge e m a (Vptr l ofs) -> + eval_expr_prop a (Vptr l ofs) -> + eval_lvalue_prop (Expr (Ederef a) ty) l ofs. Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR. eauto. Qed. Lemma transl_Eindex_correct: - (forall (e : Csem.env) (m : mem) (a1 : Csyntax.expr) (t1 : trace) - (m1 : mem) (v1 : val) (a2 : Csyntax.expr) (t2 : trace) (m2 : mem) - (v2 : val) (l : block) (ofs : int) (ty : type), - Csem.eval_expr ge e m a1 t1 m1 v1 -> - eval_expr_prop e m a1 t1 m1 v1 -> - Csem.eval_expr ge e m1 a2 t2 m2 v2 -> - eval_expr_prop e m1 a2 t2 m2 v2 -> - sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) -> - eval_lvalue_prop e m (Expr (Eindex a1 a2) ty) (t1 ** t2) m2 l ofs). + forall (a1 a2 : Csyntax.expr) (ty : type) (v1 v2 : val) (l : block) + (ofs : int), + Csem.eval_expr ge e m a1 v1 -> + eval_expr_prop a1 v1 -> + Csem.eval_expr ge e m a2 v2 -> + eval_expr_prop a2 v2 -> + sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) -> + eval_lvalue_prop (Expr (Eindex a1 a2) ty) l ofs. Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR. monadInv TR. eapply (make_add_correct tprog); eauto. Qed. Lemma transl_Efield_struct_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace) - (m1 : mem) (l : block) (ofs : int) (id: ident) (fList : fieldlist) (i : ident) - (ty : type) (delta : Z), - eval_lvalue ge e m a t m1 l ofs -> - eval_lvalue_prop e m a t m1 l ofs -> - typeof a = Tstruct id fList -> - field_offset i fList = OK delta -> - eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 l - (Int.add ofs (Int.repr delta))). + forall (a : Csyntax.expr) (i : ident) (ty : type) (l : block) + (ofs : int) (id : ident) (fList : fieldlist) (delta : Z), + eval_lvalue ge e m a l ofs -> + eval_lvalue_prop a l ofs -> + typeof a = Tstruct id fList -> + field_offset i fList = OK delta -> + eval_lvalue_prop (Expr (Efield a i) ty) l (Int.add ofs (Int.repr delta)). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR. rewrite H1 in TR. monadInv TR. - econstructor; eauto. + eapply eval_Ebinop; eauto. apply make_intconst_correct. - simpl. congruence. traceEq. + simpl. congruence. Qed. Lemma transl_Efield_union_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace) - (m1 : mem) (l : block) (ofs : int) (id: ident) (fList : fieldlist) (i : ident) - (ty : type), - eval_lvalue ge e m a t m1 l ofs -> - eval_lvalue_prop e m a t m1 l ofs -> - typeof a = Tunion id fList -> - eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 l ofs). + forall (a : Csyntax.expr) (i : ident) (ty : type) (l : block) + (ofs : int) (id : ident) (fList : fieldlist), + eval_lvalue ge e m a l ofs -> + eval_lvalue_prop a l ofs -> + typeof a = Tunion id fList -> + eval_lvalue_prop (Expr (Efield a i) ty) l ofs. Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR. rewrite H1 in TR. eauto. Qed. -Lemma transl_Enil_correct: - (forall (e : Csem.env) (m : mem), - eval_exprlist_prop e m Csyntax.Enil E0 m nil). -Proof. - intros; red; intros. monadInv TR. constructor. -Qed. +Lemma transl_expr_correct: + forall a v, + Csem.eval_expr ge e m a v -> + eval_expr_prop a v. +Proof + (eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop + transl_Econst_int_correct + transl_Econst_float_correct + transl_Elvalue_correct + transl_Eaddrof_correct + transl_Esizeof_correct + transl_Eunop_correct + transl_Ebinop_correct + transl_Eorbool_1_correct + transl_Eorbool_2_correct + transl_Eandbool_1_correct + transl_Eandbool_2_correct + transl_Ecast_correct + transl_Evar_local_correct + transl_Evar_global_correct + transl_Ederef_correct + transl_Eindex_correct + transl_Efield_struct_correct + transl_Efield_union_correct). -Lemma transl_Econs_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) - (bl : Csyntax.exprlist) (t1 : trace) (m1 : mem) (v : val) - (t2 : trace) (m2 : mem) (vl : list val), - Csem.eval_expr ge e m a t1 m1 v -> - eval_expr_prop e m a t1 m1 v -> - Csem.eval_exprlist ge e m1 bl t2 m2 vl -> - eval_exprlist_prop e m1 bl t2 m2 vl -> - eval_exprlist_prop e m (Csyntax.Econs a bl) (t1 ** t2) m2 (v :: vl)). +Lemma transl_lvalue_correct: + forall a blk ofs, + Csem.eval_lvalue ge e m a blk ofs -> + eval_lvalue_prop a blk ofs. +Proof + (eval_lvalue_ind2 ge e m eval_expr_prop eval_lvalue_prop + transl_Econst_int_correct + transl_Econst_float_correct + transl_Elvalue_correct + transl_Eaddrof_correct + transl_Esizeof_correct + transl_Eunop_correct + transl_Ebinop_correct + transl_Eorbool_1_correct + transl_Eorbool_2_correct + transl_Eandbool_1_correct + transl_Eandbool_2_correct + transl_Ecast_correct + transl_Evar_local_correct + transl_Evar_global_correct + transl_Ederef_correct + transl_Eindex_correct + transl_Efield_struct_correct + transl_Efield_union_correct). + +Lemma transl_exprlist_correct: + forall al vl, + Csem.eval_exprlist ge e m al vl -> + eval_exprlist_prop al vl. Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - econstructor; eauto. + induction 1; red; intros; monadInv TR; inv WT. + constructor. + constructor. eapply (transl_expr_correct _ _ H); eauto. eauto. 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. + +(* +Set 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). @@ -802,28 +844,13 @@ Proof. intros; red; intros. monadInv TR. simpl. constructor. Qed. -Lemma transl_Sexpr_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace) - (m1 : mem) (v : val), - Csem.eval_expr ge e m a t m1 v -> - eval_expr_prop e m a t m1 v -> - exec_stmt_prop e m (Csyntax.Sexpr a) t m1 Csem.Out_normal). -Proof. - intros; red; intros; simpl. inversion WT; clear WT; subst. - monadInv TR. econstructor; eauto. -Qed. - Lemma transl_Sassign_correct: - (forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (t1 : trace) - (m1 : mem) (loc : block) (ofs : int) (t2 : trace) (m2 : mem) - (v2 : val) (m3 : mem), - eval_lvalue ge e m a1 t1 m1 loc ofs -> - eval_lvalue_prop e m a1 t1 m1 loc ofs -> - Csem.eval_expr ge e m1 a2 t2 m2 v2 -> - eval_expr_prop e m1 a2 t2 m2 v2 -> - store_value_of_type (typeof a1) m2 loc ofs v2 = Some m3 -> - exec_stmt_prop e m (Csyntax.Sassign a1 a2) (t1 ** t2) m3 - Csem.Out_normal). + 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. @@ -832,12 +859,70 @@ Proof. (* a = variable id *) intros id ISVAR. rewrite ISVAR in TR. generalize (is_variable_correct _ _ ISVAR). intro EQ. - rewrite EQ in H; rewrite EQ in H0; rewrite EQ in H6. + rewrite EQ in H; rewrite EQ in H4. monadInv TR. - eapply var_set_correct; eauto. + 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: @@ -867,35 +952,39 @@ Proof. Qed. Lemma transl_Sifthenelse_true_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) - (s1 s2 : statement) (t1 : trace) (m1 : mem) (v1 : val) (t2 : trace) - (m2 : mem) (out : Csem.outcome), - Csem.eval_expr ge e m a t1 m1 v1 -> - eval_expr_prop e m a t1 m1 v1 -> + (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 m1 s1 t2 m2 out -> - exec_stmt_prop e m1 s1 t2 m2 out -> - exec_stmt_prop e m (Csyntax.Sifthenelse a s1 s2) (t1 ** t2) m2 out). + 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 H0; eauto. eauto. intros [vb [EVAL ISTRUE]]. - eapply exec_Sifthenelse_true; eauto. + 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) (t1 : trace) (m1 : mem) (v1 : val) (t2 : trace) - (m2 : mem) (out : Csem.outcome), - Csem.eval_expr ge e m a t1 m1 v1 -> - eval_expr_prop e m a t1 m1 v1 -> + (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 m1 s2 t2 m2 out -> - exec_stmt_prop e m1 s2 t2 m2 out -> - exec_stmt_prop e m (Csyntax.Sifthenelse a s1 s2) (t1 ** t2) m2 out). + 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 H0; eauto. eauto. intros [vb [EVAL ISFALSE]]. - eapply exec_Sifthenelse_false; eauto. + 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: @@ -907,15 +996,13 @@ Proof. Qed. Lemma transl_Sreturn_some_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace) - (m1 : mem) (v : val), - Csem.eval_expr ge e m a t m1 v -> - eval_expr_prop e m a t m1 v -> - exec_stmt_prop e m (Csyntax.Sreturn (Some a)) t m1 - (Csem.Out_return (Some v))). + (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. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - simpl. eapply exec_Sreturn_some; eauto. + 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: @@ -935,47 +1022,51 @@ Proof. Qed. Lemma exit_if_false_true: - forall a ts e m1 t m2 v tyenv te, + forall a ts e m v tyenv te, exit_if_false a = OK ts -> - eval_expr_prop e m1 a t m2 v -> + Csem.eval_expr ge e m a v -> + is_true v (typeof a) -> match_env tyenv e te -> wt_expr tyenv a -> - is_true v (typeof a) -> - exec_stmt tprog te m1 ts t m2 Out_normal. + exec_stmt tprog te m ts E0 m Out_normal. Proof. - intros. monadInv H. - exploit make_boolean_correct_true. eapply H0; eauto. eauto. + intros. monadInv H. + exploit make_boolean_correct_true. + eapply (transl_expr_correct _ _ _ _ H2 _ _ H0); eauto. + eauto. intros [vb [EVAL ISTRUE]]. - eapply exec_Sifthenelse_true with (v1 := vb); eauto. - constructor. traceEq. + eapply exec_Sifthenelse with (v := vb); eauto. + apply Val.bool_of_true_val; eauto. + constructor. Qed. Lemma exit_if_false_false: - forall a ts e m1 t m2 v tyenv te, + forall a ts e m v tyenv te, exit_if_false a = OK ts -> - eval_expr_prop e m1 a t m2 v -> + Csem.eval_expr ge e m a v -> + is_false v (typeof a) -> match_env tyenv e te -> wt_expr tyenv a -> - is_false v (typeof a) -> - exec_stmt tprog te m1 ts t m2 (Out_exit 0). + exec_stmt tprog te m ts E0 m (Out_exit 0). Proof. - intros. monadInv H. - exploit make_boolean_correct_false. eapply H0; eauto. eauto. + intros. monadInv H. + exploit make_boolean_correct_false. + eapply (transl_expr_correct _ _ _ _ H2 _ _ H0); eauto. + eauto. intros [vb [EVAL ISFALSE]]. - eapply exec_Sifthenelse_false with (v1 := vb); eauto. - constructor. traceEq. + eapply exec_Sifthenelse with (v := vb); eauto. + apply Val.bool_of_false_val; eauto. + simpl. constructor. Qed. Lemma transl_Swhile_false_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr) - (t : trace) (v : val) (m1 : mem), - Csem.eval_expr ge e m a t m1 v -> - eval_expr_prop e m a t m1 v -> + (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) t m1 Csem.Out_normal). + exec_stmt_prop e m (Swhile a s) E0 m Csem.Out_normal). Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - simpl. + 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. @@ -999,48 +1090,45 @@ Proof. Qed. Lemma transl_Swhile_stop_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t1 : trace) - (m1 : mem) (v : val) (s : statement) (m2 : mem) (t2 : trace) - (out2 out : Csem.outcome), - Csem.eval_expr ge e m a t1 m1 v -> - eval_expr_prop e m a t1 m1 v -> + (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 m1 s t2 m2 out2 -> - exec_stmt_prop e m1 s t2 m2 out2 -> - out_break_or_return out2 out -> - exec_stmt_prop e m (Swhile a s) (t1 ** t2) m2 out). + 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. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - rewrite (transl_out_break_or_return _ _ nbrk ncnt H4). + 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. - auto. inversion H4; simpl; congruence. + apply exec_Sblock. eauto. traceEq. + inversion H3; simpl; congruence. Qed. Lemma transl_Swhile_loop_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t1 : trace) - (m1 : mem) (v : val) (s : statement) (out2 out : Csem.outcome) - (t2 : trace) (m2 : mem) (t3 : trace) (m3 : mem), - Csem.eval_expr ge e m a t1 m1 v -> - eval_expr_prop e m a t1 m1 v -> + (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 m1 s t2 m2 out2 -> - exec_stmt_prop e m1 s t2 m2 out2 -> - out_normal_or_continue out2 -> - Csem.exec_stmt ge e m2 (Swhile a s) t3 m3 out -> - exec_stmt_prop e m2 (Swhile a s) t3 m3 out -> - exec_stmt_prop e m (Swhile a s) (t1 ** t2 ** t3) m3 out). + 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 H6; eauto. intro NEXTITER. - inversion WT; clear WT; subst. simpl in TR; monadInv TR. + 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 _ H4). + rewrite (transl_out_normal_or_continue _ H3). apply exec_Sblock. eauto. reflexivity. eassumption. traceEq. @@ -1048,23 +1136,21 @@ Qed. Lemma transl_Sdowhile_false_correct: (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr) - (t1 : trace) (m1 : mem) (out1 : Csem.outcome) (v : val) - (t2 : trace) (m2 : mem), - Csem.exec_stmt ge e m s t1 m1 out1 -> - exec_stmt_prop e m s t1 m1 out1 -> + (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 t2 m2 v -> - eval_expr_prop e m1 a t2 m2 v -> + Csem.eval_expr ge e m1 a v -> is_false v (typeof a) -> - exec_stmt_prop e m (Sdowhile a s) (t1 ** t2) m2 Csem.Out_normal). + exec_stmt_prop e m (Sdowhile a s) t m1 Csem.Out_normal). Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. + 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. auto. congruence. + eapply exit_if_false_false; eauto. traceEq. congruence. Qed. Lemma transl_Sdowhile_stop_correct: @@ -1075,7 +1161,7 @@ Lemma transl_Sdowhile_stop_correct: out_break_or_return out1 out -> exec_stmt_prop e m (Sdowhile a s) t m1 out). Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. + intros; red; intros. inv WT. monadInv TR. simpl. assert (outcome_block (transl_outcome 1 0 out1) <> Out_normal). inversion H1; simpl; congruence. @@ -1087,22 +1173,19 @@ Qed. Lemma transl_Sdowhile_loop_correct: (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr) - (m1 m2 m3 : mem) (t1 t2 t3 : trace) (out out1 : Csem.outcome) - (v : val), + (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 t2 m2 v -> - eval_expr_prop e m1 a t2 m2 v -> + Csem.eval_expr ge e m1 a v -> is_true v (typeof a) -> - Csem.exec_stmt ge e m2 (Sdowhile a s) t3 m3 out -> - exec_stmt_prop e m2 (Sdowhile a s) t3 m3 out -> - exec_stmt_prop e m (Sdowhile a s) (t1 ** t2 ** t3) m3 out). + 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 H6; eauto. intro NEXTITER. - inversion WT; clear WT; subst. simpl in TR; monadInv TR. - inversion NEXTITER; subst. + 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). @@ -1115,6 +1198,7 @@ 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 -> @@ -1122,101 +1206,88 @@ Lemma transl_Sfor_start_correct: exec_stmt_prop e m (Sfor a1 a2 a3 s) (t1 ** t2) m2 out). Proof. intros; red; intros. - exploit transl_stmt_Sfor_start; eauto. - intros [ts1 [ts2 [A [B C]]]]. - clear TR; subst ts. - inversion WT; subst. + 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 H0; eauto. simpl. intro EXEC1. - exploit H2; eauto. intro EXEC2. - assert (EXEC3: exec_stmt tprog te m1 ts2 t2 m2 (transl_outcome nbrk ncnt out)). - inversion EXEC2; subst. - inversion H5; subst. rewrite E0_left; auto. - inversion H11; subst. congruence. - eapply exec_Sseq_continue; eauto. + exploit H1; eauto. simpl. intro EXEC1. + exploit H3; eauto. intro EXEC2. + eapply exec_Sseq_continue; eauto. Qed. Lemma transl_Sfor_false_correct: (forall (e : Csem.env) (m : mem) (s : statement) (a2 : Csyntax.expr) - (a3 : statement) (t : trace) (v : val) (m1 : mem), - Csem.eval_expr ge e m a2 t m1 v -> - eval_expr_prop e m a2 t m1 v -> + (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) t m1 Csem.Out_normal). + exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) E0 m Csem.Out_normal). Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. + intros; red; intros. inv WT. + rewrite transl_stmt_Sfor_not_start in TR; monadInv TR. simpl. - eapply exec_Sseq_continue. apply exec_Sskip. 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. traceEq. + congruence. congruence. Qed. Lemma transl_Sfor_stop_correct: (forall (e : Csem.env) (m : mem) (s : statement) (a2 : Csyntax.expr) - (a3 : statement) (v : val) (m1 m2 : mem) (t1 t2 : trace) - (out2 out : Csem.outcome), - Csem.eval_expr ge e m a2 t1 m1 v -> - eval_expr_prop e m a2 t1 m1 v -> + (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 m1 s t2 m2 out2 -> - exec_stmt_prop e m1 s t2 m2 out2 -> - out_break_or_return out2 out -> - exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) (t1 ** t2) m2 out). + 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. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - simpl. - assert (outcome_block (transl_outcome 1 0 out2) <> Out_normal). - inversion H4; simpl; congruence. - rewrite (transl_out_break_or_return _ _ nbrk ncnt H4). - eapply exec_Sseq_continue. apply exec_Sskip. + 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. traceEq. + auto. reflexivity. auto. Qed. Lemma transl_Sfor_loop_correct: (forall (e : Csem.env) (m : mem) (s : statement) (a2 : Csyntax.expr) - (a3 : statement) (v : val) (m1 m2 m3 m4 : mem) - (t1 t2 t3 t4 : trace) (out2 out : Csem.outcome), - Csem.eval_expr ge e m a2 t1 m1 v -> - eval_expr_prop e m a2 t1 m1 v -> + (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 m1 s t2 m2 out2 -> - exec_stmt_prop e m1 s t2 m2 out2 -> - out_normal_or_continue out2 -> - Csem.exec_stmt ge e m2 a3 t3 m3 Csem.Out_normal -> - exec_stmt_prop e m2 a3 t3 m3 Csem.Out_normal -> - Csem.exec_stmt ge e m3 (Sfor Csyntax.Sskip a2 a3 s) t4 m4 out -> - exec_stmt_prop e m3 (Sfor Csyntax.Sskip a2 a3 s) t4 m4 out -> - exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) - (t1 ** t2 ** t3 ** t4) m4 out). + 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). Proof. intros; red; intros. - exploit H8; eauto. intro NEXTITER. - inversion WT; clear WT; subst. simpl in TR; monadInv TR. + exploit H7; eauto. intro NEXTITER. + inv WT. + rewrite transl_stmt_Sfor_not_start in TR; monadInv TR. inversion NEXTITER; subst. - inversion H11; subst. - inversion H18; subst. - eapply exec_Sseq_continue. apply exec_Sskip. 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 _ H4). + rewrite (transl_out_normal_or_continue _ H3). apply exec_Sblock. eauto. - red in H6; simpl in H6; eauto. + red in H5; simpl in H5; eauto. reflexivity. reflexivity. eassumption. - reflexivity. traceEq. - inversion H17. congruence. + traceEq. Qed. Lemma transl_lblstmts_switch: - forall e m0 t1 m1 n nbrk ncnt tyenv te t2 m2 out sl body ts, - exec_stmt tprog te m0 body t1 m1 + 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) @@ -1224,8 +1295,8 @@ Lemma transl_lblstmts_switch: sl (Sblock body) = OK ts -> wt_lblstmts tyenv sl -> match_env tyenv e te -> - exec_lblstmts_prop e m1 (select_switch n sl) t2 m2 out -> - Csharpminor.exec_stmt tprog te m0 ts (t1 ** t2) m2 + 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)). Proof. induction sl; intros. @@ -1251,24 +1322,20 @@ Proof. Qed. Lemma transl_Sswitch_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t1 : trace) - (m1 : mem) (n : int) (sl : labeled_statements) (t2 : trace) - (m2 : mem) (out : Csem.outcome), - Csem.eval_expr ge e m a t1 m1 (Vint n) -> - eval_expr_prop e m a t1 m1 (Vint n) -> - exec_lblstmts ge e m1 (select_switch n sl) t2 m2 out -> - exec_lblstmts_prop e m1 (select_switch n sl) t2 m2 out -> - exec_stmt_prop e m (Csyntax.Sswitch a sl) (t1 ** t2) m2 - (outcome_switch out)). + (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. - inversion WT; clear WT; subst. - simpl in TR. monadInv TR. + 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. - eapply transl_lblstmts_switch; eauto. - constructor. eapply H0; eauto. + change t with (E0 ** t). eapply transl_lblstmts_switch; eauto. + constructor. eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto. Qed. Lemma transl_LSdefault_correct: @@ -1278,9 +1345,7 @@ Lemma transl_LSdefault_correct: exec_stmt_prop e m s t m1 out -> exec_lblstmts_prop e m (LSdefault s) t m1 out). Proof. - intros; red; intros. - inversion WT; subst. - simpl in TR. monadInv TR. + 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. @@ -1299,11 +1364,9 @@ Lemma transl_LScase_fallthrough_correct: 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. - inversion WT; subst. - monadInv TR. + intros; red; intros. inv WT. monadInv TR. assert (exec_stmt tprog te m0 (Sblock (Sseq body x)) - (t0 ** t1) m1 Out_normal). + (t0 ** t1) m1 Out_normal). change Out_normal with (outcome_block (transl_outcome (S (lblstmts_length ls)) (S (S (lblstmts_length ls + ncnt))) @@ -1316,7 +1379,7 @@ Proof. Qed. Lemma transl_LScase_stop_correct: - (forall (e : Csem.env) (m : mem) (n : int) (s : statement) + (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 -> @@ -1324,9 +1387,7 @@ Lemma transl_LScase_stop_correct: out <> Csem.Out_normal -> exec_lblstmts_prop e m (LScase n s ls) t m1 out). Proof. - intros; red; intros. - inversion WT; subst. - monadInv TR. + intros; red; intros. inv WT. monadInv TR. exploit H0; eauto. intro EXEC. destruct out; simpl; simpl in EXEC. (* out = Out_break *) @@ -1378,8 +1439,7 @@ Lemma transl_funcall_internal_correct: Proof. intros; red; intros. (* Exploitation of typing hypothesis *) - inversion WT; clear WT; subst. - inversion H6; clear H6; subst. + inv WT. inv H6. (* Exploitation of translation hypothesis *) monadInv TR. monadInv EQ. @@ -1419,38 +1479,55 @@ Theorem transl_funcall_correct: Csem.eval_funcall ge m f l t m0 v -> eval_funcall_prop m f l t m0 v. Proof - (Csem.eval_funcall_ind6 ge - eval_expr_prop - eval_lvalue_prop - eval_exprlist_prop + (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_Econst_int_correct - transl_Econst_float_correct - transl_Elvalue_correct - transl_Eaddrof_correct - transl_Esizeof_correct - transl_Eunop_correct - transl_Ebinop_correct - transl_Eorbool_1_correct - transl_Eorbool_2_correct - transl_Eandbool_1_correct - transl_Eandbool_2_correct - transl_Ecast_correct - transl_Ecall_correct - transl_Evar_local_correct - transl_Evar_global_correct - transl_Ederef_correct - transl_Eindex_correct - transl_Efield_struct_correct - transl_Efield_union_correct - transl_Enil_correct - transl_Econs_correct transl_Sskip_correct - transl_Sexpr_correct transl_Sassign_correct + transl_Scall_None_correct + transl_Scall_Some_correct transl_Ssequence_1_correct transl_Ssequence_2_correct transl_Sifthenelse_true_correct @@ -1476,41 +1553,287 @@ Proof 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. +Proof. + cofix FUNCALL. + assert (STMT: + 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). + cofix STMT. + assert(LBLSTMT: + 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)). + + cofix LBLSTMT; 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 STMT; 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 STMT; 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 LBLSTMT 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 LBLSTMT 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 STMT; eauto. auto. + (* 2.2.2 we diverge later *) + simpl. apply execinf_sleep. + replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3). + eapply LBLSTMT 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 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 FUNCALL; eauto. + eapply functions_well_typed; eauto. + (* Sseq 1 *) + apply execinf_Sseq_1. eapply STMT; 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 STMT; 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 STMT; 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 STMT; eauto. + (* Swhile, body *) + apply execinf_Sblock. apply execinf_Sloop_body. + eapply execinf_Sseq_2. eapply exit_if_false_true; eauto. + apply execinf_Sblock. eapply STMT; 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 STMT 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 STMT; 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 STMT 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 STMT; 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 STMT; 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 STMT; 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 STMT; 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 STMT; 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 LBLSTMT; eauto. + left. split. apply exec_Sblock. constructor. + eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. + auto. + + (* 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 STMT; eauto. +Qed. + End CORRECTNESS. (** Semantic preservation for whole programs. *) Theorem transl_program_correct: - forall prog tprog t r, + forall prog tprog beh, transl_program prog = OK tprog -> Ctyping.wt_program prog -> - Csem.exec_program prog t r -> - Csharpminor.exec_program tprog t r. + Csem.exec_program prog beh -> + Csharpminor.exec_program tprog beh. Proof. - intros until r. intros TRANSL WT [b [f [m1 [FINDS [FINDF EVAL]]]]]. - inversion WT; subst. - + 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 H; clear H; intros targs TYP. + elim H1; clear H1; intros targs TYP. assert (targs = Tnil). - inversion EVAL; subst; simpl in TYP. - inversion H0; subst. injection TYP. rewrite <- H6. simpl; auto. - inversion TYP; subst targs0 tres. inversion H. simpl in H0. - inversion H0. destruct targs; simpl in H8; congruence. + 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]]. - exists b; exists tf; exists m1. - split. - rewrite (symbols_preserved _ _ TRANSL). - rewrite (transform_partial_program2_main transl_fundef transl_globvar prog TRANSL). auto. - split. auto. - split. - generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD TYP). simpl; auto. - rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog TRANSL). - generalize (transl_funcall_correct _ _ WT TRANSL _ _ _ _ _ _ EVAL). - intro. eapply H. + 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. Qed. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index 3866669a..31d1d873 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -136,15 +136,10 @@ with expr_descr : Set := | Ebinop: binary_operation -> expr -> expr -> expr_descr (**r binary operation *) | Ecast: type -> expr -> expr_descr (**r type cast ([(ty) e]) *) | Eindex: expr -> expr -> expr_descr (**r array indexing ([e1[e2]]) *) - | Ecall: expr -> exprlist -> expr_descr (**r function call *) | Eandbool: expr -> expr -> expr_descr (**r sequential and ([&&]) *) | Eorbool: expr -> expr -> expr_descr (**r sequential or ([||]) *) | Esizeof: type -> expr_descr (**r size of a type *) - | Efield: expr -> ident -> expr_descr (**r access to a member of a struct or union *) - -with exprlist : Set := - | Enil: exprlist - | Econs: expr -> exprlist -> exprlist. + | Efield: expr -> ident -> expr_descr. (**r access to a member of a struct or union *) (** Extract the type part of a type-annotated Clight expression. *) @@ -160,8 +155,8 @@ Definition typeof (e: expr) : type := Inductive statement : Set := | Sskip : statement (**r do nothing *) - | Sexpr : expr -> statement (**r evaluate expression for its side-effects *) | Sassign : expr -> expr -> statement (**r assignment [lvalue = rvalue] *) + | Scall: option expr -> expr -> list expr -> statement (**r function call *) | Ssequence : statement -> statement -> statement (**r sequence *) | Sifthenelse : expr -> statement -> statement -> statement (**r conditional *) | Swhile : expr -> statement -> statement (**r [while] loop *) diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index cb572c09..72c4edf2 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -47,10 +47,6 @@ Inductive wt_expr: expr -> Prop := | wt_Eindex: forall e1 e2 ty, wt_expr e1 -> wt_expr e2 -> wt_expr (Expr (Eindex e1 e2) ty) - | wt_Ecall: forall e1 el ty, - wt_expr e1 -> - wt_exprlist el -> - wt_expr (Expr (Ecall e1 el) ty) | wt_Eandbool: forall e1 e2 ty, wt_expr e1 -> wt_expr e2 -> wt_expr (Expr (Eandbool e1 e2) ty) @@ -61,23 +57,32 @@ Inductive wt_expr: expr -> Prop := wt_expr (Expr (Esizeof ty') ty) | wt_Efield: forall e id ty, wt_expr e -> - wt_expr (Expr (Efield e id) ty) + wt_expr (Expr (Efield e id) ty). + +Inductive wt_optexpr: option expr -> Prop := + | wt_Enone: + wt_optexpr None + | wt_Esome: forall e, + wt_expr e -> + wt_optexpr (Some e). -with wt_exprlist: exprlist -> Prop := +Inductive wt_exprlist: list expr -> Prop := | wt_Enil: - wt_exprlist Enil + wt_exprlist nil | wt_Econs: forall e el, - wt_expr e -> wt_exprlist el -> wt_exprlist (Econs e el). + wt_expr e -> wt_exprlist el -> wt_exprlist (e :: el). Inductive wt_stmt: statement -> Prop := | wt_Sskip: wt_stmt Sskip - | wt_Sexpr: forall e, - wt_expr e -> - wt_stmt (Sexpr e) | wt_Sassign: forall e1 e2, wt_expr e1 -> wt_expr e2 -> wt_stmt (Sassign e1 e2) + | wt_Scall: forall lhs e1 el, + wt_optexpr lhs -> + wt_expr e1 -> + wt_exprlist el -> + wt_stmt (Scall lhs e1 el) | wt_Ssequence: forall s1 s2, wt_stmt s1 -> wt_stmt s2 -> wt_stmt (Ssequence s1 s2) @@ -97,11 +102,9 @@ Inductive wt_stmt: statement -> Prop := wt_stmt Sbreak | wt_Scontinue: wt_stmt Scontinue - | wt_Sreturn_some: forall e, - wt_expr e -> - wt_stmt (Sreturn (Some e)) - | wt_Sreturn_none: - wt_stmt (Sreturn None) + | wt_Sreturn: forall opte, + wt_optexpr opte -> + wt_stmt (Sreturn opte) | wt_Sswitch: forall e sl, wt_expr e -> wt_lblstmts sl -> wt_stmt (Sswitch e sl) @@ -282,49 +285,35 @@ with typecheck_exprdescr (a: Csyntax.expr_descr) (ty: type) {struct a} : bool := | Csyntax.Ebinop op b c => typecheck_expr b && typecheck_expr c | Csyntax.Ecast ty b => typecheck_expr b | Csyntax.Eindex b c => typecheck_expr b && typecheck_expr c - | Csyntax.Ecall b cl => typecheck_expr b && typecheck_exprlist cl | Csyntax.Eandbool b c => typecheck_expr b && typecheck_expr c | Csyntax.Eorbool b c => typecheck_expr b && typecheck_expr c | Csyntax.Esizeof ty => true | Csyntax.Efield b i => typecheck_expr b - end + end. -with typecheck_exprlist (al: Csyntax.exprlist): bool := +Fixpoint typecheck_exprlist (al: list Csyntax.expr): bool := match al with - | Csyntax.Enil => true - | Csyntax.Econs a1 a2 => typecheck_expr a1 && typecheck_exprlist a2 + | nil => true + | a1 :: a2 => typecheck_expr a1 && typecheck_exprlist a2 + end. + +Definition typecheck_optexpr (opta: option Csyntax.expr): bool := + match opta with + | None => true + | Some a => typecheck_expr a end. -Scheme expr_ind_3 := Induction for expr Sort Prop - with expr_descr_ind_3 := Induction for expr_descr Sort Prop - with exprlist_ind_3 := Induction for exprlist Sort Prop. +Scheme expr_ind_2 := Induction for expr Sort Prop + with expr_descr_ind_2 := Induction for expr_descr Sort Prop. Lemma typecheck_expr_correct: forall a, typecheck_expr a = true -> wt_expr env a. Proof. - apply (expr_ind_3 (fun a => typecheck_expr a = true -> wt_expr env a) - (fun a => forall ty, typecheck_exprdescr a ty = true -> wt_expr env (Expr a ty)) - (fun a => typecheck_exprlist a = true -> wt_exprlist env a)); - simpl; intros; TrueInv. - auto. - constructor. - constructor. - constructor. destruct (env!i). decEq; symmetry; apply eq_type_correct; auto. + apply (expr_ind_2 (fun a => typecheck_expr a = true -> wt_expr env a) + (fun a => forall ty, typecheck_exprdescr a ty = true -> wt_expr env (Expr a ty))); + simpl; intros; TrueInv; try constructor; auto. + destruct (env!i). decEq; symmetry; apply eq_type_correct; auto. discriminate. - constructor; auto. - constructor; auto. - constructor; auto. - constructor; auto. - constructor; auto. - constructor; auto. - constructor; auto. - constructor; auto. - constructor; auto. - auto. - constructor; auto. - constructor; auto. - constructor. - constructor; auto. Qed. Lemma typecheck_exprlist_correct: @@ -335,11 +324,19 @@ Proof. TrueInv. constructor; auto. apply typecheck_expr_correct; auto. Qed. +Lemma typecheck_optexpr_correct: + forall a, typecheck_optexpr a = true -> wt_optexpr env a. +Proof. + destruct a; simpl; intros. + constructor. apply typecheck_expr_correct; auto. + constructor. +Qed. + Fixpoint typecheck_stmt (s: Csyntax.statement) {struct s} : bool := match s with | Csyntax.Sskip => true - | Csyntax.Sexpr e => typecheck_expr e | Csyntax.Sassign b c => typecheck_expr b && typecheck_expr c + | Csyntax.Scall a b cl => typecheck_optexpr a && typecheck_expr b && typecheck_exprlist cl | Csyntax.Ssequence s1 s2 => typecheck_stmt s1 && typecheck_stmt s2 | Csyntax.Sifthenelse e s1 s2 => typecheck_expr e && typecheck_stmt s1 && typecheck_stmt s2 @@ -368,10 +365,11 @@ Lemma typecheck_stmt_correct: forall s, typecheck_stmt s = true -> wt_stmt env s. Proof. generalize typecheck_expr_correct; intro. + generalize typecheck_exprlist_correct; intro. + generalize typecheck_optexpr_correct; intro. apply (stmt_ind_2 (fun s => typecheck_stmt s = true -> wt_stmt env s) (fun s => typecheck_lblstmts s = true -> wt_lblstmts env s)); - simpl; intros; TrueInv; try constructor; auto. - destruct o; constructor; auto. + simpl; intros; TrueInv; constructor; auto. Qed. End TYPECHECKING. |