From 213bf38509f4f92545d4c5749c25a55b9a9dda36 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 3 Aug 2009 15:32:27 +0000 Subject: Transition semantics for Clight and Csharpminor git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1119 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenproof.v | 40 +- cfrontend/Cminorgen.v | 115 ++- cfrontend/Cminorgenproof.v | 1525 ++++++++++++++++++----------------- cfrontend/Csem.v | 975 +++++++++++++++++++--- cfrontend/Csharpminor.v | 529 ++++++------ cfrontend/Cshmgen.v | 45 +- cfrontend/Cshmgenproof1.v | 102 +-- cfrontend/Cshmgenproof2.v | 110 +-- cfrontend/Cshmgenproof3.v | 1921 ++++++++++++++++++++------------------------ cfrontend/Csyntax.v | 9 +- cfrontend/Ctyping.v | 7 + 11 files changed, 3013 insertions(+), 2365 deletions(-) diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 6d5cd8e..1dd2294 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -930,32 +930,26 @@ Qed. (** ** Semantic preservation for the translation of statements *) (** The simulation diagram for the translation of statements - is of the following form: + and functions is a "star" diagram of the form: << - I /\ P - e, m, a ---------------- State cs code sp ns rs m - || | - t|| t|* - || | - \/ v - e', m', out ------------------ st' - I /\ Q + I I + S1 ------- R1 S1 ------- R1 + | | | | + t | + | t or t | * | t and |S2| < |S1| + v v v | + S2 ------- R2 S2 ------- R2 + I I >> - where [tr_stmt code map a ns ncont nexits nret rret] holds. - The left vertical arrow represents an execution of the statement [a]. - The right vertical arrow represents the execution of - zero, one or several instructions in the generated RTL flow graph [code]. - - The invariant [I] is the agreement between Cminor environments and - RTL register environment, as captured by [match_envs]. - - The precondition [P] is the well-formedness of the compilation - environment [mut]. + where [I] is the [match_states] predicate defined below. It includes: +- Agreement between the Cminor statement under consideration and + the current program point in the RTL control-flow graph, + as captured by the [tr_stmt] predicate. +- Agreement between the Cminor continuation and the RTL control-flow + graph and call stack, as captured by the [tr_cont] predicate below. +- Agreement between Cminor environments and RTL register environments, + as captured by [match_envs]. - The postcondition [Q] characterizes the final RTL state [st']. - It must have memory state [m'] and register state [rs'] that matches - [e']. Moreover, the program point reached must correspond to the outcome - [out]. This is captured by the following [state_for_outcome] predicate. *) +*) Inductive tr_funbody (c: code) (map: mapping) (f: CminorSel.function) (ngoto: labelmap) (nret: node) (rret: option reg) : Prop := diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index 1045d1a..5977ded 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -38,11 +38,15 @@ Open Local Scope error_monad_scope. taken in the Csharpminor code can be mapped to Cminor local variable, since the latter do not reside in memory. - The other task performed during the translation to Cminor is the + Another task performed during the translation to Cminor is the insertion of truncation, zero- and sign-extension operations when assigning to a Csharpminor local variable of ``small'' type (e.g. [Mfloat32] or [Mint8signed]). This is necessary to preserve the ``normalize at assignment-time'' semantics of Clight and Csharpminor. + + Finally, the Clight-like [switch] construct of Csharpminor + is transformed into the simpler, lower-level [switch] construct + of Cminor. *) (** Translation of constants. *) @@ -190,9 +194,50 @@ Fixpoint transl_exprlist (cenv: compilenv) (el: list Csharpminor.expr) OK (te1 :: te2) end. -(** Translation of statements. Entirely straightforward. *) +(** To translate [switch] statements, we wrap the statements associated with + the various cases in a cascade of nested Cminor blocks. + The multi-way branch is performed by a Cminor [switch] + statement that exits to the appropriate case. For instance: +<< +switch (e) { ---> block { block { block { + case N1: s1; switch (e) { N1: exit 0; N2: exit 1; default: exit 2; } + case N2: s2; } ; s1 // with exits shifted by 2 + default: s; } ; s2 // with exits shifted by 1 +} } ; s // with exits unchanged +>> + To shift [exit] statements appropriately, we use a second + compile-time environment, of type [exit_env], which + records the blocks inserted during the translation. + A [true] element means the block was present in the original code; + a [false] element, that it was inserted during translation. +*) + +Definition exit_env := list bool. + +Fixpoint shift_exit (e: exit_env) (n: nat) {struct e} : nat := + match e, n with + | nil, _ => n + | false :: e', _ => S (shift_exit e' n) + | true :: e', O => O + | true :: e', S m => S (shift_exit e' m) + end. + +Fixpoint switch_table (ls: lbl_stmt) (k: nat) {struct ls} : list (int * nat) := + match ls with + | LSdefault _ => nil + | LScase ni _ rem => (ni, k) :: switch_table rem (S k) + end. + +Fixpoint switch_env (ls: lbl_stmt) (e: exit_env) {struct ls}: exit_env := + match ls with + | LSdefault _ => e + | LScase _ _ ls' => false :: switch_env ls' e + end. + +(** Translation of statements. The only nonobvious part is + the translation of [switch] statements, outlined above. *) -Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt) +Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt) {struct s}: res stmt := match s with | Csharpminor.Sskip => @@ -213,28 +258,47 @@ Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt) 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; + do ts1 <- transl_stmt cenv xenv s1; + do ts2 <- transl_stmt cenv xenv s2; OK (Sseq ts1 ts2) | Csharpminor.Sifthenelse e s1 s2 => do te <- transl_expr cenv e; - do ts1 <- transl_stmt cenv s1; - do ts2 <- transl_stmt cenv s2; + do ts1 <- transl_stmt cenv xenv s1; + do ts2 <- transl_stmt cenv xenv s2; OK (Sifthenelse te ts1 ts2) | Csharpminor.Sloop s => - do ts <- transl_stmt cenv s; + do ts <- transl_stmt cenv xenv s; OK (Sloop ts) | Csharpminor.Sblock s => - do ts <- transl_stmt cenv s; + do ts <- transl_stmt cenv (true :: xenv) s; OK (Sblock ts) | Csharpminor.Sexit n => - OK (Sexit n) - | Csharpminor.Sswitch e cases default => - do te <- transl_expr cenv e; OK(Sswitch te cases default) + OK (Sexit (shift_exit xenv n)) + | Csharpminor.Sswitch e ls => + let cases := switch_table ls O in + let default := length cases in + do te <- transl_expr cenv e; + transl_lblstmt cenv (switch_env ls xenv) ls (Sswitch te cases default) | Csharpminor.Sreturn None => OK (Sreturn None) | Csharpminor.Sreturn (Some e) => do te <- transl_expr cenv e; OK (Sreturn (Some te)) + | Csharpminor.Slabel lbl s => + do ts <- transl_stmt cenv xenv s; OK (Slabel lbl ts) + | Csharpminor.Sgoto lbl => + OK (Sgoto lbl) + end + +with transl_lblstmt (cenv: compilenv) (xenv: exit_env) + (ls: Csharpminor.lbl_stmt) (body: stmt) + {struct ls}: res stmt := + match ls with + | Csharpminor.LSdefault s => + do ts <- transl_stmt cenv xenv s; + OK (Sseq (Sblock body) ts) + | Csharpminor.LScase _ s ls' => + do ts <- transl_stmt cenv xenv s; + transl_lblstmt cenv (List.tail xenv) ls' (Sseq (Sblock body) ts) end. (** Computation of the set of variables whose address is taken in @@ -279,9 +343,18 @@ Fixpoint addr_taken_stmt (s: Csharpminor.stmt): Identset.t := | Csharpminor.Sloop s => addr_taken_stmt s | Csharpminor.Sblock s => addr_taken_stmt s | Csharpminor.Sexit n => Identset.empty - | Csharpminor.Sswitch e cases default => addr_taken_expr e + | Csharpminor.Sswitch e ls => + Identset.union (addr_taken_expr e) (addr_taken_lblstmt ls) | Csharpminor.Sreturn None => Identset.empty | Csharpminor.Sreturn (Some e) => addr_taken_expr e + | Csharpminor.Slabel lbl s => addr_taken_stmt s + | Csharpminor.Sgoto lbl => Identset.empty + end + +with addr_taken_lblstmt (ls: Csharpminor.lbl_stmt): Identset.t := + match ls with + | Csharpminor.LSdefault s => addr_taken_stmt s + | Csharpminor.LScase _ s ls' => Identset.union (addr_taken_stmt s) (addr_taken_lblstmt ls') end. (** Layout of the Cminor stack data block and construction of the @@ -362,18 +435,22 @@ Fixpoint store_parameters otherwise address computations within the stack block could overflow machine arithmetic and lead to incorrect code. *) -Definition transl_function - (gce: compilenv) (f: Csharpminor.function): res 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); +Definition transl_funbody + (cenv: compilenv) (stacksize: Z) (f: Csharpminor.function): res function := + do tbody <- transl_stmt cenv nil 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 sparams tbody)) + (Sseq sparams tbody)). + +Definition transl_function + (gce: compilenv) (f: Csharpminor.function): res function := + let (cenv, stacksize) := build_compilenv gce f in + if zle stacksize Int.max_signed + then transl_funbody cenv stacksize f 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 f256bb2..1a68c10 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -23,6 +23,7 @@ Require Import Values. Require Import Mem. Require Import Events. Require Import Globalenvs. +Require Import Smallstep. Require Import Csharpminor. Require Import Op. Require Import Cminor. @@ -36,8 +37,10 @@ Variable prog: Csharpminor.program. Variable tprog: program. Hypothesis TRANSL: transl_program prog = OK tprog. Let ge : Csharpminor.genv := Genv.globalenv prog. -Let tge: genv := Genv.globalenv tprog. +Let gvare : gvarenv := global_var_env prog. +Let gve := (ge, gvare). Let gce : compilenv := build_global_compilenv prog. +Let tge: genv := Genv.globalenv tprog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -58,6 +61,14 @@ Lemma functions_translated: Genv.find_funct tge v = Some tf /\ transl_fundef gce f = OK tf. Proof (Genv.find_funct_transf_partial2 (transl_fundef gce) transl_globvar TRANSL). +Lemma sig_preserved_body: + forall f tf cenv size, + transl_funbody cenv size f = OK tf -> + tf.(fn_sig) = f.(Csharpminor.fn_sig). +Proof. + intros. monadInv H. reflexivity. +Qed. + Lemma sig_preserved: forall f tf, transl_fundef gce f = OK tf -> @@ -65,8 +76,8 @@ Lemma sig_preserved: Proof. intros until tf; destruct f; simpl. unfold transl_function. destruct (build_compilenv gce f). - case (zle z Int.max_signed); simpl; try congruence. - intros. monadInv H. monadInv EQ. reflexivity. + case (zle z Int.max_signed); simpl bind; try congruence. + intros. monadInv H. simpl. eapply sig_preserved_body; eauto. intro. inv H. reflexivity. Qed. @@ -79,7 +90,7 @@ Definition global_compilenv_match (ce: compilenv) (gv: gvarenv) : Prop := end. Lemma global_compilenv_charact: - global_compilenv_match gce (global_var_env prog). + global_compilenv_match gce gvare. Proof. set (mkgve := fun gv (vars: list (ident * list init_data * var_kind)) => List.fold_left @@ -96,7 +107,7 @@ Proof. case (peq id1 id2); intro. auto. apply H. case (peq id1 id2); intro. auto. apply H. - change (global_var_env prog) with (mkgve (PTree.empty var_kind) prog.(prog_vars)). + change gvare with (mkgve (PTree.empty var_kind) prog.(prog_vars)). unfold gce, build_global_compilenv. apply H. intro. rewrite PMap.gi. auto. Qed. @@ -156,7 +167,7 @@ Inductive match_var (f: meminj) (id: ident) | match_var_global_scalar: forall chunk, PTree.get id e = None -> - PTree.get id (global_var_env prog) = Some (Vscalar chunk) -> + PTree.get id gvare = Some (Vscalar chunk) -> match_var f id e m te sp (Var_global_scalar chunk) | match_var_global_array: PTree.get id e = None -> @@ -192,11 +203,12 @@ Record match_env (f: meminj) (cenv: compilenv) PTree.get id2 e = Some(b2, lv2) -> id1 <> id2 -> b1 <> b2; -(** All blocks mapped to sub-blocks of the Cminor stack data must be in - the range [lo, hi]. *) +(** All blocks mapped to sub-blocks of the Cminor stack data must be + images of variables from the Csharpminor environment [e] *) me_inv: forall b delta, - f b = Some(sp, delta) -> lo <= b < hi; + f b = Some(sp, delta) -> + exists id, exists lv, PTree.get id e = Some(b, lv); (** All Csharpminor blocks below [lo] (i.e. allocated before the blocks referenced from [e]) must map to blocks that are below [sp] @@ -460,17 +472,37 @@ Proof. generalize (H3 _ H4). inversion H1. omega. Qed. +Lemma blocks_of_env_charact: + forall b e, + In b (blocks_of_env e) <-> + exists id, exists lv, e!id = Some(b, lv). +Proof. + unfold blocks_of_env. + set (f := fun id_b_lv : positive * (block * var_kind) => + let (_, y) := id_b_lv in let (b0, _) := y in b0). + intros; split; intros. + exploit list_in_map_inv; eauto. intros [[id [b' lv]] [A B]]. + simpl in A. subst b'. exists id; exists lv. apply PTree.elements_complete. auto. + destruct H as [id [lv EQ]]. + change b with (f (id, (b, lv))). apply List.in_map. + apply PTree.elements_correct. auto. +Qed. + Lemma match_callstack_freelist: - forall f cenv e te sp lo hi cs bound tbound m fbl, - (forall b, In b fbl -> lo <= b) -> + forall f cenv e te sp lo hi cs bound tbound m tm, + mem_inject f m tm -> match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m -> - match_callstack f cs bound tbound (free_list m fbl). + match_callstack f cs bound tbound (free_list m (blocks_of_env e)) + /\ mem_inject f (free_list m (blocks_of_env e)) (free tm sp). Proof. - intros. inversion H0. inversion H14. + intros. inv H0. inv H14. split. apply match_callstack_incr_bound with lo sp. - apply match_callstack_freelist_rec. auto. - assumption. + apply match_callstack_freelist_rec. auto. + intros. rewrite blocks_of_env_charact in H0. + destruct H0 as [id [lv EQ]]. exploit me_bounded0; eauto. omega. omega. omega. + apply Mem.free_inject; auto. + intros. rewrite blocks_of_env_charact. eauto. Qed. (** Preservation of [match_callstack] when allocating a block for @@ -501,6 +533,7 @@ Lemma match_env_alloc_same: end -> match_env f1 cenv1 e1 m1 te sp lo m1.(nextblock) -> te!id = Some tv -> + e1!id = None -> let f2 := extend_inject b data f1 in let cenv2 := PMap.set id info cenv1 in let e2 := PTree.set id (b, lv) e1 in @@ -511,7 +544,7 @@ Proof. assert (b = m1.(nextblock)). injection H; intros. auto. assert (m2.(nextblock) = Zsucc m1.(nextblock)). - injection H; intros. rewrite <- H6; reflexivity. + injection H; intros. rewrite <- H7; reflexivity. inversion H1. constructor. (* me_vars *) intros id0. unfold cenv2. rewrite PMap.gsspec. case (peq id0 id); intros. @@ -522,7 +555,7 @@ Proof. apply match_var_local with b Vundef tv. unfold e2; rewrite PTree.gss. congruence. eapply load_from_alloc_is_undef; eauto. - rewrite H7 in H. unfold sizeof in H. eauto. + rewrite H8 in H. unfold sizeof in H. eauto. unfold f2, extend_inject, eq_block. rewrite zeq_true. auto. auto. constructor. @@ -545,12 +578,12 @@ Proof. contradiction. (* other vars *) generalize (me_vars0 id0); intros. - inversion H6. + inversion H7. eapply match_var_local with (v := v); eauto. unfold e2; rewrite PTree.gso; eauto. eapply load_alloc_other; eauto. unfold f2, extend_inject, eq_block; rewrite zeq_false; auto. - generalize (me_bounded0 _ _ _ H8). unfold block in *; omega. + generalize (me_bounded0 _ _ _ H9). unfold block in *; omega. econstructor; eauto. unfold e2; rewrite PTree.gso; eauto. econstructor; eauto. @@ -564,22 +597,24 @@ Proof. (* me_bounded *) intros until lv0. unfold e2; rewrite PTree.gsspec. case (peq id0 id); intros. - subst id0. inversion H6. subst b0. unfold block in *; omega. - generalize (me_bounded0 _ _ _ H6). rewrite H5. omega. + subst id0. inversion H7. subst b0. unfold block in *; omega. + generalize (me_bounded0 _ _ _ H7). rewrite H6. omega. (* me_inj *) intros until lv2. unfold e2; repeat rewrite PTree.gsspec. case (peq id1 id); case (peq id2 id); intros. congruence. - inversion H6. subst b1. rewrite H4. + inversion H7. subst b1. rewrite H5. + generalize (me_bounded0 _ _ _ H8). unfold block; omega. + inversion H8. subst b2. rewrite H5. generalize (me_bounded0 _ _ _ H7). unfold block; omega. - inversion H7. subst b2. rewrite H4. - generalize (me_bounded0 _ _ _ H6). unfold block; omega. eauto. (* me_inv *) intros until delta. unfold f2, extend_inject, eq_block. case (zeq b0 b); intros. - subst b0. rewrite H4; rewrite H5. omega. - generalize (me_inv0 _ _ H6). rewrite H5. omega. + subst b0. exists id; exists lv. unfold e2. apply PTree.gss. + exploit me_inv0; eauto. intros [id' [lv' EQ]]. + exists id'; exists lv'. unfold e2. rewrite PTree.gso; auto. + congruence. (* me_incr *) intros until delta. unfold f2, extend_inject, eq_block. case (zeq b0 b); intros. @@ -660,6 +695,7 @@ Lemma match_callstack_alloc_left: end -> match_callstack f1 (mkframe cenv1 e1 te sp lo m1.(nextblock) :: cs) m1.(nextblock) tbound m1 -> te!id = Some tv -> + e1!id = None -> let f2 := extend_inject b data f1 in let cenv2 := PMap.set id info cenv1 in let e2 := PTree.set id (b, lv) e1 in @@ -670,12 +706,12 @@ Proof. unfold f2, cenv2, e2. eapply match_env_alloc_same; eauto. unfold f2; eapply match_callstack_alloc_other; eauto. destruct info. - elim H0; intros. rewrite H19. auto. - elim H0; intros. rewrite H19. omega. - elim H0; intros. rewrite H19. omega. + elim H0; intros. rewrite H20. auto. + elim H0; intros. rewrite H20. omega. + elim H0; intros. rewrite H20. omega. contradiction. contradiction. - inversion H17; omega. + inversion H18; omega. Qed. Lemma match_callstack_alloc_right: @@ -1029,7 +1065,7 @@ Proof. Qed. Lemma make_store_correct: - forall f sp te tm addr tvaddr rhs tvrhs chunk m vaddr vrhs m', + forall f sp te tm addr tvaddr rhs tvrhs chunk m vaddr vrhs m' fn k, eval_expr tge sp te tm addr tvaddr -> eval_expr tge sp te tm rhs tvrhs -> Mem.storev chunk m vaddr vrhs = Some m' -> @@ -1037,8 +1073,8 @@ Lemma make_store_correct: val_inject f vaddr tvaddr -> val_inject f vrhs tvrhs -> exists tm', - exec_stmt tge sp te tm (make_store chunk addr rhs) - E0 te tm' Out_normal + step tge (State fn (make_store chunk addr rhs) k sp te tm) + E0 (State fn Sskip k sp te tm') /\ mem_inject f m' tm' /\ nextblock tm' = nextblock tm. Proof. @@ -1048,7 +1084,7 @@ Proof. exploit storev_mapped_inject_1; eauto. intros [tm' [STORE MEMINJ]]. exists tm'. - split. eapply exec_Sstore; eauto. + split. eapply step_store; eauto. split. auto. unfold storev in STORE; destruct tvaddr; try discriminate. eapply nextblock_store; eauto. @@ -1062,7 +1098,7 @@ Lemma var_get_correct: var_get cenv id = OK a -> match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> mem_inject f m tm -> - eval_var_ref prog e id b chunk -> + eval_var_ref gve e id b chunk -> load chunk m b 0 = Some v -> exists tv, eval_expr tge (Vptr sp Int.zero) te tm a tv /\ @@ -1088,7 +1124,7 @@ Proof. eapply eval_Eload; eauto. eapply make_stackaddr_correct; eauto. auto. (* var_global_scalar *) - inversion H2; [congruence|subst]. + inversion H2; [congruence|subst]. simpl in H9; simpl in H10. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. inversion H11. destruct (mg_symbols0 _ _ H9) as [A B]. assert (chunk0 = chunk). congruence. subst chunk0. @@ -1106,7 +1142,7 @@ Lemma var_addr_correct: forall cenv id a f e te sp lo hi m cs tm b, match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> var_addr cenv id = OK a -> - eval_var_addr prog e id b -> + eval_var_addr gve e id b -> exists tv, eval_expr tge (Vptr sp Int.zero) te tm a tv /\ val_inject f (Vptr b Int.zero) tv. @@ -1142,15 +1178,16 @@ Proof. Qed. Lemma var_set_correct: - forall cenv id rhs a f e te sp lo hi m cs tm tv v m', + forall cenv id rhs a f e te sp lo hi m cs tm tv v m' fn k, var_set cenv id rhs = OK a -> match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> eval_expr tge (Vptr sp Int.zero) te tm rhs tv -> val_inject f v tv -> mem_inject f m tm -> - exec_assign prog e m id v m' -> + exec_assign gve e m id v m' -> exists te', exists tm', - exec_stmt tge (Vptr sp Int.zero) te tm a E0 te' tm' Out_normal /\ + step tge (State fn a k (Vptr sp Int.zero) te tm) + E0 (State fn Sskip k (Vptr sp Int.zero) te' tm') /\ mem_inject f m' tm' /\ match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m' /\ (forall id', id' <> id -> te'!id' = te!id'). @@ -1169,7 +1206,7 @@ Proof. exploit make_cast_correct; eauto. intros [tv' [EVAL INJ]]. exists (PTree.set id tv' te); exists tm. - split. eapply exec_Sassign. eauto. + split. eapply step_assign. eauto. split. eapply store_unmapped_inject; eauto. split. rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto. intros. apply PTree.gso; auto. @@ -1183,13 +1220,13 @@ Proof. eauto. eauto. eauto. eauto. eauto. intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. exists te; exists tm'. - split. auto. split. auto. + split. eauto. split. auto. split. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. eapply match_callstack_mapped; eauto. inversion H9; congruence. auto. (* var_global_scalar *) - inversion H5; [congruence|subst]. + inversion H5; [congruence|subst]. simpl in H4; simpl in H10. assert (chunk0 = chunk) by congruence. subst chunk0. assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. @@ -1199,7 +1236,7 @@ Proof. eauto. eauto. eauto. eauto. eauto. intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. exists te; exists tm'. - split. auto. split. auto. + split. eauto. split. auto. split. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. eapply match_callstack_mapped; eauto. congruence. auto. @@ -1238,14 +1275,15 @@ Proof. Qed. Lemma var_set_self_correct: - forall cenv id a f e te sp lo hi m cs tm tv v m', + forall cenv id a f e te sp lo hi m cs tm tv v m' fn k, var_set cenv id (Evar id) = OK a -> match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> val_inject f v tv -> mem_inject f m tm -> - exec_assign prog e m id v m' -> + exec_assign gve e m id v m' -> exists te', exists tm', - exec_stmt tge (Vptr sp Int.zero) (PTree.set id tv te) tm a E0 te' tm' Out_normal /\ + step tge (State fn a k (Vptr sp Int.zero) (PTree.set id tv te) tm) + E0 (State fn Sskip k (Vptr sp Int.zero) te' tm') /\ mem_inject f m' tm' /\ match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m'. Proof. @@ -1265,7 +1303,7 @@ Proof. exploit make_cast_correct; eauto. intros [tv' [EVAL INJ]]. exists (PTree.set id tv' (PTree.set id tv te)); exists tm. - split. eapply exec_Sassign. eauto. + split. eapply step_assign. eauto. split. eapply store_unmapped_inject; eauto. rewrite NEXTBLOCK. apply match_callstack_extensional with (PTree.set id tv' te). @@ -1282,7 +1320,7 @@ Proof. eauto. eauto. eauto. eauto. eauto. intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. exists (PTree.set id tv te); exists tm'. - split. auto. split. auto. + split. eauto. split. auto. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. apply match_callstack_extensional with te. intros. caseEq (cenv!!id0); intros; auto. @@ -1290,7 +1328,7 @@ Proof. eapply match_callstack_mapped; eauto. inversion H8; congruence. (* var_global_scalar *) - inversion H4; [congruence|subst]. + inversion H4; [congruence|subst]. simpl in H3; simpl in H9. assert (chunk0 = chunk) by congruence. subst chunk0. assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. @@ -1300,7 +1338,7 @@ Proof. eauto. eauto. eauto. eauto. eauto. intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. exists (PTree.set id tv te); exists tm'. - split. auto. split. auto. + split. eauto. split. auto. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. apply match_callstack_extensional with te. intros. caseEq (cenv!!id0); intros; auto. @@ -1390,8 +1428,8 @@ Lemma match_callstack_alloc_variables_rec: low_bound tm sp = 0 -> high_bound tm sp = sz' -> sz' <= Int.max_signed -> - forall e m vars e' m' lb, - alloc_variables e m vars e' m' lb -> + forall e m vars e' m', + alloc_variables e m vars e' m' -> forall f cenv sz, assign_variables atk vars (cenv, sz) = (cenv', sz') -> match_callstack f (mkframe cenv e te sp lo m.(nextblock) :: cs) @@ -1400,6 +1438,8 @@ Lemma match_callstack_alloc_variables_rec: 0 <= sz -> (forall b delta, f b = Some(sp, delta) -> high_bound m b + delta <= sz) -> (forall id lv, In (id, lv) vars -> te!id <> None) -> + list_norepet (List.map (@fst ident var_kind) vars) -> + (forall id lv, In (id, lv) vars -> e!id = None) -> exists f', inject_incr f f' /\ mem_inject f' m' tm @@ -1416,13 +1456,21 @@ Proof. change (assign_variables atk ((id, lv) :: vars) (cenv, sz)) with (assign_variables atk vars (assign_variable atk (id, lv) (cenv, sz))). caseEq (assign_variable atk (id, lv) (cenv, sz)). - intros cenv1 sz1 ASV1 ASVS MATCH MINJ SZPOS BOUND DEFINED. + intros cenv1 sz1 ASV1 ASVS MATCH MINJ SZPOS BOUND DEFINED NOREPET UNDEFINED. assert (DEFINED1: forall id0 lv0, In (id0, lv0) vars -> te!id0 <> None). intros. eapply DEFINED. simpl. right. eauto. assert (exists tv, te!id = Some tv). assert (te!id <> None). eapply DEFINED. simpl; left; auto. destruct (te!id). exists v; auto. congruence. elim H1; intros tv TEID; clear H1. + assert (UNDEFINED1: forall (id0 : ident) (lv0 : var_kind), + In (id0, lv0) vars -> + (PTree.set id (b1, lv) e)!id0 = None). + intros. rewrite PTree.gso. eapply UNDEFINED; eauto with coqlib. + simpl in NOREPET. inversion NOREPET. red; intro; subst id0. + elim H4. change id with (fst (id, lv0)). apply List.in_map. auto. + assert (NOREPET1: list_norepet (map (fst (A:=ident) (B:=var_kind)) vars)). + inv NOREPET; auto. generalize ASV1. unfold assign_variable. caseEq lv. (* 1. lv = LVscalar chunk *) @@ -1443,13 +1491,13 @@ Proof. intros. left. generalize (BOUND _ _ H5). omega. elim H3; intros MINJ1 INCR1; clear H3. exploit IHalloc_variables; eauto. - unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. + unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto with coqlib. rewrite <- H1. omega. intros until delta; unfold f1, extend_inject, eq_block. rewrite (high_bound_alloc _ _ _ _ _ H b). case (zeq b b1); intros. inversion H3. unfold sizeof; rewrite LV. omega. - generalize (BOUND _ _ H3). omega. + generalize (BOUND _ _ H3). omega. intros [f' [INCR2 [MINJ2 MATCH2]]]. exists f'; intuition. eapply inject_incr_trans; eauto. (* 1.2 info = Var_local chunk *) @@ -1457,7 +1505,7 @@ Proof. exploit alloc_unmapped_inject; eauto. set (f1 := extend_inject b1 None f). intros [MINJ1 INCR1]. exploit IHalloc_variables; eauto. - unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. + unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto with coqlib. intros until delta; unfold f1, extend_inject, eq_block. rewrite (high_bound_alloc _ _ _ _ _ H b). case (zeq b b1); intros. discriminate. @@ -1480,7 +1528,7 @@ Proof. intros. left. generalize (BOUND _ _ H7). omega. destruct H5 as [MINJ1 INCR1]. exploit IHalloc_variables; eauto. - unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. + unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto with coqlib. rewrite <- H1. omega. intros until delta; unfold f1, extend_inject, eq_block. rewrite (high_bound_alloc _ _ _ _ _ H b). @@ -1530,10 +1578,11 @@ Qed. of Csharpminor local variables and of the Cminor stack data block. *) Lemma match_callstack_alloc_variables: - forall fn cenv sz m e m' lb tm tm' sp f cs targs, + forall fn cenv sz m e m' tm tm' sp f cs targs, build_compilenv gce fn = (cenv, sz) -> sz <= Int.max_signed -> - alloc_variables Csharpminor.empty_env m (fn_variables fn) e m' lb -> + list_norepet (fn_params_names fn ++ fn_vars_names fn) -> + alloc_variables Csharpminor.empty_env m (fn_variables fn) e m' -> Mem.alloc tm 0 sz = (tm', sp) -> match_callstack f cs m.(nextblock) tm.(nextblock) m -> mem_inject f m tm -> @@ -1547,7 +1596,7 @@ Lemma match_callstack_alloc_variables: m'.(nextblock) tm'.(nextblock) m'. Proof. intros. - assert (SP: sp = nextblock tm). injection H2; auto. + assert (SP: sp = nextblock tm). injection H3; auto. unfold build_compilenv in H. eapply match_callstack_alloc_variables_rec with (sz' := sz); eauto with mem. eapply low_bound_alloc_same; eauto. @@ -1570,7 +1619,7 @@ Proof. intros until lv2. unfold Csharpminor.empty_env; rewrite PTree.gempty; congruence. (* me_inv *) intros. exploit mi_mappedblocks; eauto. intro A. - elim (fresh_block_alloc _ _ _ _ _ H2 A). + elim (fresh_block_alloc _ _ _ _ _ H3 A). (* me_incr *) intros. exploit mi_mappedblocks; eauto. intro A. rewrite SP; auto. @@ -1584,45 +1633,17 @@ Proof. unfold tparams, tvars. unfold fn_variables in H5. change Csharpminor.fn_params with Csharpminor.fn_params in H5. change Csharpminor.fn_vars with Csharpminor.fn_vars in H5. - elim (in_app_or _ _ _ H5); intros. - elim (list_in_map_inv _ _ _ H6). intros x [A B]. + elim (in_app_or _ _ _ H6); intros. + elim (list_in_map_inv _ _ _ H7). intros x [A B]. apply in_or_app; left. inversion A. apply List.in_map. auto. apply in_or_app; right. change id with (fst (id, lv)). apply List.in_map; auto. -Qed. - -(** Characterization of the range of addresses for the blocks allocated - to hold Csharpminor local variables. *) - -Lemma alloc_variables_nextblock_incr: - forall e1 m1 vars e2 m2 lb, - alloc_variables e1 m1 vars e2 m2 lb -> - nextblock m1 <= nextblock m2. -Proof. - induction 1; intros. - omega. - inversion H; subst m1; simpl in IHalloc_variables. omega. -Qed. - -Lemma alloc_variables_list_block: - forall e1 m1 vars e2 m2 lb, - alloc_variables e1 m1 vars e2 m2 lb -> - forall b, m1.(nextblock) <= b < m2.(nextblock) <-> In b lb. -Proof. - induction 1; intros. - simpl; split; intro. omega. contradiction. - elim (IHalloc_variables b); intros A B. - assert (nextblock m = b1). injection H; intros. auto. - assert (nextblock m1 = Zsucc (nextblock m)). - injection H; intros; subst m1; reflexivity. - simpl; split; intro. - assert (nextblock m = b \/ nextblock m1 <= b < nextblock m2). - unfold block; rewrite H2; omega. - elim H4; intro. left; congruence. right; auto. - elim H3; intro. subst b b1. - generalize (alloc_variables_nextblock_incr _ _ _ _ _ _ H0). - rewrite H2. omega. - generalize (B H4). rewrite H2. omega. + (* norepet *) + unfold fn_variables. + rewrite List.map_app. rewrite list_map_compose. simpl. + assumption. + (* undef *) + intros. unfold empty_env. apply PTree.gempty. Qed. (** Correctness of the code generated by [store_parameters] @@ -1656,16 +1677,15 @@ Qed. Lemma store_parameters_correct: forall e m1 params vl m2, bind_parameters e m1 params vl m2 -> - forall s f te1 cenv sp lo hi cs tm1, + forall s f te1 cenv sp lo hi cs tm1 fn k, vars_vals_match f params vl te1 -> list_norepet (List.map (@fst ident memory_chunk) params) -> mem_inject f m1 tm1 -> match_callstack f (mkframe cenv e te1 sp lo hi :: cs) m1.(nextblock) tm1.(nextblock) m1 -> store_parameters cenv params = OK s -> exists te2, exists tm2, - exec_stmt tge (Vptr sp Int.zero) - te1 tm1 s - E0 te2 tm2 Out_normal + star step tge (State fn s k (Vptr sp Int.zero) te1 tm1) + E0 (State fn Sskip k (Vptr sp Int.zero) te2 tm2) /\ mem_inject f m2 tm2 /\ match_callstack f (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2. Proof. @@ -1674,7 +1694,7 @@ Proof. intros; simpl. monadInv H3. exists te1; exists tm1. split. constructor. tauto. (* inductive case *) - intros until tm1. intros VVM NOREPET MINJ MATCH STOREP. + intros until k. intros VVM NOREPET MINJ MATCH STOREP. monadInv STOREP. inversion VVM. subst f0 id0 chunk0 vars v vals te. inversion NOREPET. subst hd tl. @@ -1690,7 +1710,10 @@ Proof. exploit IHbind_parameters; eauto. intros [te3 [tm3 [EXEC2 [MINJ2 MATCH2]]]]. exists te3; exists tm3. - split. econstructor; eauto. + split. eapply star_left. constructor. + eapply star_left. eexact EXEC1. + eapply star_left. constructor. eexact EXEC2. + reflexivity. reflexivity. reflexivity. auto. Qed. @@ -1752,8 +1775,8 @@ Qed. and initialize the blocks corresponding to function parameters). *) Lemma function_entry_ok: - forall fn m e m1 lb vargs m2 f cs tm cenv sz tm1 sp tvargs s, - alloc_variables empty_env m (fn_variables fn) e m1 lb -> + forall fn m e m1 vargs m2 f cs tm cenv sz tm1 sp tvargs s fn' k, + alloc_variables empty_env m (fn_variables fn) e m1 -> bind_parameters e m1 fn.(Csharpminor.fn_params) vargs m2 -> match_callstack f cs m.(nextblock) tm.(nextblock) m -> build_compilenv gce fn = (cenv, sz) -> @@ -1766,15 +1789,13 @@ Lemma function_entry_ok: list_norepet (fn_params_names fn ++ fn_vars_names fn) -> store_parameters cenv fn.(Csharpminor.fn_params) = OK s -> exists f2, exists te2, exists tm2, - exec_stmt tge (Vptr sp Int.zero) - te tm1 s - E0 te2 tm2 Out_normal + star step tge (State fn' s k (Vptr sp Int.zero) te tm1) + E0 (State fn' Sskip k (Vptr sp Int.zero) te2 tm2) /\ mem_inject f2 m2 tm2 /\ inject_incr f f2 /\ match_callstack f2 (mkframe cenv e te2 sp m.(nextblock) m1.(nextblock) :: cs) - m2.(nextblock) tm2.(nextblock) m2 - /\ (forall b, m.(nextblock) <= b < m1.(nextblock) <-> In b lb). + m2.(nextblock) tm2.(nextblock) m2. Proof. intros. exploit bind_parameters_length; eauto. intro LEN1. @@ -1791,8 +1812,7 @@ Proof. eexact MINJ1. eauto. eauto. intros [te2 [tm2 [EXEC [MINJ2 MATCH2]]]]. exists f1; exists te2; exists tm2. - split; auto. split; auto. split; auto. split; auto. - intros; eapply alloc_variables_list_block; eauto. + split. eauto. auto. Qed. (** * Semantic preservation for the translation *) @@ -1835,7 +1855,7 @@ Lemma transl_expr_correct: (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m), forall a v, - Csharpminor.eval_expr prog e m a v -> + Csharpminor.eval_expr gve e m a v -> forall ta (TR: transl_expr cenv a = OK ta), exists tv, @@ -1880,7 +1900,7 @@ Lemma transl_exprlist_correct: (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m), forall a v, - Csharpminor.eval_exprlist prog e m a v -> + Csharpminor.eval_exprlist gve e m a v -> forall ta (TR: transl_exprlist cenv a = OK ta), exists tv, @@ -1896,656 +1916,709 @@ Qed. (** ** Semantic preservation for statements and functions *) -Definition eval_funcall_prop - (m1: mem) (fn: Csharpminor.fundef) (args: list val) (t: trace) (m2: mem) (res: val) : Prop := - forall tfn f1 tm1 cs targs - (TR: transl_fundef gce fn = OK tfn) - (MINJ: mem_inject f1 m1 tm1) - (MATCH: match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1) - (ARGSINJ: val_list_inject f1 args targs), - exists f2, exists tm2, exists tres, - eval_funcall tge tm1 tfn targs t tm2 tres - /\ val_inject f2 res tres - /\ mem_inject f2 m2 tm2 - /\ inject_incr f1 f2 - /\ match_callstack f2 cs m2.(nextblock) tm2.(nextblock) m2. - -Inductive outcome_inject (f: meminj) : Csharpminor.outcome -> outcome -> Prop := - | outcome_inject_normal: - outcome_inject f Csharpminor.Out_normal Out_normal - | outcome_inject_exit: - forall n, outcome_inject f (Csharpminor.Out_exit n) (Out_exit n) - | outcome_inject_return_none: - outcome_inject f (Csharpminor.Out_return None) (Out_return None) - | outcome_inject_return_some: - forall v1 v2, - val_inject f v1 v2 -> - outcome_inject f (Csharpminor.Out_return (Some v1)) (Out_return (Some v2)). - -Definition exec_stmt_prop - (e: Csharpminor.env) (m1: mem) (s: Csharpminor.stmt) (t: trace) (m2: mem) (out: Csharpminor.outcome): Prop := - forall cenv ts f1 te1 tm1 sp lo hi cs - (TR: transl_stmt cenv s = OK ts) - (MINJ: mem_inject f1 m1 tm1) - (MATCH: match_callstack f1 - (mkframe cenv e te1 sp lo hi :: cs) - m1.(nextblock) tm1.(nextblock) m1), - exists f2, exists te2, exists tm2, exists tout, - exec_stmt tge (Vptr sp Int.zero) te1 tm1 ts t te2 tm2 tout - /\ outcome_inject f2 out tout - /\ mem_inject f2 m2 tm2 - /\ inject_incr f1 f2 - /\ match_callstack f2 - (mkframe cenv e te2 sp lo hi :: cs) - m2.(nextblock) tm2.(nextblock) m2. - -(* Check (Csharpminor.eval_funcall_ind2 prog eval_funcall_prop exec_stmt_prop). *) - -(** There are as many cases in the inductive proof as there are evaluation - rules in the Csharpminor semantics. We treat each case as a separate - lemma. *) - -Lemma transl_funcall_internal_correct: - forall (m : mem) (f : Csharpminor.function) (vargs : list val) - (e : Csharpminor.env) (m1 : mem) (lb : list block) (m2: mem) - (t: trace) (m3 : mem) (out : Csharpminor.outcome) (vres : val), - list_norepet (fn_params_names f ++ fn_vars_names f) -> - alloc_variables empty_env m (fn_variables f) e m1 lb -> - bind_parameters e m1 (Csharpminor.fn_params f) vargs m2 -> - Csharpminor.exec_stmt prog e m2 (Csharpminor.fn_body f) t m3 out -> - exec_stmt_prop e m2 (Csharpminor.fn_body f) t m3 out -> - Csharpminor.outcome_result_value out (sig_res (Csharpminor.fn_sig f)) vres -> - eval_funcall_prop m (Internal f) vargs t (free_list m3 lb) vres. -Proof. - intros; red. intros tfn f1 tm; intros. - monadInv TR. generalize EQ. - unfold transl_function. - caseEq (build_compilenv gce f); intros cenv stacksize CENV. - destruct (zle stacksize Int.max_signed); try congruence. - intro TR. monadInv TR. - caseEq (alloc tm 0 stacksize). intros tm1 sp ALLOC. - exploit function_entry_ok; eauto. - intros [f2 [te2 [tm2 [STOREPARAM [MINJ2 [INCR12 [MATCH2 BLOCKS]]]]]]]. - red in H3; exploit H3; eauto. - intros [f3 [te3 [tm3 [tout [EXECBODY [OUTINJ [MINJ3 [INCR23 MATCH3]]]]]]]]. - assert (exists tvres, - outcome_result_value tout f.(Csharpminor.fn_sig).(sig_res) tvres /\ - val_inject f3 vres tvres). - generalize H4. unfold Csharpminor.outcome_result_value, outcome_result_value. - inversion OUTINJ. - destruct (sig_res (Csharpminor.fn_sig f)); intro. contradiction. - exists Vundef; split. auto. subst vres; constructor. - tauto. - destruct (sig_res (Csharpminor.fn_sig f)); intro. contradiction. - exists Vundef; split. auto. subst vres; constructor. - destruct (sig_res (Csharpminor.fn_sig f)); intro. - exists v2; split. auto. subst vres; auto. - contradiction. - destruct H5 as [tvres [TOUT VINJRES]]. - assert (outcome_free_mem tout tm3 sp = Mem.free tm3 sp). - inversion OUTINJ; auto. - exists f3; exists (Mem.free tm3 sp); exists tvres. - (* execution *) - split. rewrite <- H5. econstructor; simpl; eauto. - apply exec_Sseq_continue with E0 te2 tm2 t. - exact STOREPARAM. - eexact EXECBODY. - traceEq. - (* val_inject *) - split. assumption. - (* mem_inject *) - split. apply free_inject; auto. - intros. elim (BLOCKS b1); intros B1 B2. apply B1. inversion MATCH3. inversion H20. - eapply me_inv0. eauto. - (* inject_incr *) - split. eapply inject_incr_trans; eauto. - (* match_callstack *) - assert (forall bl mm, nextblock (free_list mm bl) = nextblock mm). - induction bl; intros. reflexivity. simpl. auto. - unfold free; simpl nextblock. rewrite H6. - eapply match_callstack_freelist; eauto. - intros. elim (BLOCKS b); intros B1 B2. generalize (B2 H7). omega. -Qed. - -Lemma transl_funcall_external_correct: - forall (m : mem) (ef : external_function) (vargs : list val) - (t : trace) (vres : val), - event_match ef vargs t vres -> - eval_funcall_prop m (External ef) vargs t m vres. +Inductive match_cont: Csharpminor.cont -> Cminor.cont -> compilenv -> exit_env -> callstack -> Prop := + | match_Kstop: forall cenv xenv, + match_cont Csharpminor.Kstop Kstop cenv xenv nil + | match_Kseq: forall s k ts tk cenv xenv cs, + transl_stmt cenv xenv s = OK ts -> + match_cont k tk cenv xenv cs -> + match_cont (Csharpminor.Kseq s k) (Kseq ts tk) cenv xenv cs + | match_Kseq2: forall s1 s2 k ts1 tk cenv xenv cs, + transl_stmt cenv xenv s1 = OK ts1 -> + match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs -> + match_cont (Csharpminor.Kseq (Csharpminor.Sseq s1 s2) k) + (Kseq ts1 tk) cenv xenv cs + | match_Kblock: forall k tk cenv xenv cs, + match_cont k tk cenv xenv cs -> + match_cont (Csharpminor.Kblock k) (Kblock tk) cenv (true :: xenv) cs + | match_Kblock2: forall k tk cenv xenv cs, + match_cont k tk cenv xenv cs -> + match_cont k (Kblock tk) cenv (false :: xenv) cs + | match_Kcall_none: forall fn e k tfn sp te tk cenv xenv lo hi cs sz cenv', + transl_funbody cenv sz fn = OK tfn -> + match_cont k tk cenv xenv cs -> + match_cont (Csharpminor.Kcall None fn e k) + (Kcall None tfn (Vptr sp Int.zero) te tk) + cenv' nil + (mkframe cenv e te sp lo hi :: cs) + | match_Kcall_some: forall id fn e k tfn s sp te tk cenv xenv lo hi cs sz cenv', + transl_funbody cenv sz fn = OK tfn -> + var_set cenv id (Evar id) = OK s -> + match_cont k tk cenv xenv cs -> + match_cont (Csharpminor.Kcall (Some id) fn e k) + (Kcall (Some id) tfn (Vptr sp Int.zero) te (Kseq s tk)) + cenv' nil + (mkframe cenv e te sp lo hi :: cs). + +Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := + | match_state: + forall fn s k e m tfn ts tk sp te tm cenv xenv f lo hi cs sz + (TRF: transl_funbody cenv sz fn = OK tfn) + (TR: transl_stmt cenv xenv s = OK ts) + (MINJ: mem_inject f m tm) + (MCS: match_callstack f + (mkframe cenv e te sp lo hi :: cs) + m.(nextblock) tm.(nextblock) m) + (MK: match_cont k tk cenv xenv cs), + match_states (Csharpminor.State fn s k e m) + (State tfn ts tk (Vptr sp Int.zero) te tm) + | match_state_seq: + forall fn s1 s2 k e m tfn ts1 tk sp te tm cenv xenv f lo hi cs sz + (TRF: transl_funbody cenv sz fn = OK tfn) + (TR: transl_stmt cenv xenv s1 = OK ts1) + (MINJ: mem_inject f m tm) + (MCS: match_callstack f + (mkframe cenv e te sp lo hi :: cs) + m.(nextblock) tm.(nextblock) m) + (MK: match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs), + match_states (Csharpminor.State fn (Csharpminor.Sseq s1 s2) k e m) + (State tfn ts1 tk (Vptr sp Int.zero) te tm) + | match_callstate: + forall fd args k m tfd targs tk tm f cs cenv + (TR: transl_fundef gce fd = OK tfd) + (MINJ: mem_inject f m tm) + (MCS: match_callstack f cs m.(nextblock) tm.(nextblock) m) + (MK: match_cont k tk cenv nil cs) + (ISCC: Csharpminor.is_call_cont k) + (ARGSINJ: val_list_inject f args targs), + match_states (Csharpminor.Callstate fd args k m) + (Callstate tfd targs tk tm) + | match_returnstate: + forall v k m tv tk tm f cs cenv + (MINJ: mem_inject f m tm) + (MCS: match_callstack f cs m.(nextblock) tm.(nextblock) m) + (MK: match_cont k tk cenv nil cs) + (RESINJ: val_inject f v tv), + match_states (Csharpminor.Returnstate v k m) + (Returnstate tv tk tm). + +Remark nextblock_freelist: + forall lb m, nextblock (free_list m lb) = nextblock m. +Proof. induction lb; intros; simpl; auto. Qed. + +Remark val_inject_function_pointer: + forall v fd f tv, + Genv.find_funct tge v = Some fd -> + match_globalenvs f -> + val_inject f v tv -> + tv = v. Proof. - intros; red; intros. monadInv TR. - exploit event_match_inject; eauto. intros [A B]. - exists f1; exists tm1; exists vres; intuition. - constructor; auto. + intros. exploit Genv.find_funct_inv; eauto. intros [b EQ]. subst v. + rewrite Genv.find_funct_find_funct_ptr in H. + assert (b < 0). unfold tge in H. eapply Genv.find_funct_ptr_negative; eauto. + assert (f b = Some(b, 0)). eapply mg_functions; eauto. + inv H1. rewrite H3 in H6; inv H6. reflexivity. Qed. -Lemma transl_stmt_Sskip_correct: - forall (e : Csharpminor.env) (m : mem), - exec_stmt_prop e m Csharpminor.Sskip E0 m Csharpminor.Out_normal. +Lemma match_call_cont: + forall k tk cenv xenv cs, + match_cont k tk cenv xenv cs -> + match_cont (Csharpminor.call_cont k) (call_cont tk) cenv nil cs. Proof. - intros; red; intros. monadInv TR. - exists f1; exists te1; exists tm1; exists Out_normal. - intuition. constructor. constructor. + induction 1; simpl; auto; econstructor; eauto. Qed. -Lemma transl_stmt_Sassign_correct: - forall (e : Csharpminor.env) (m : mem) (id : ident) - (a : Csharpminor.expr) (v : val) (m' : mem), - Csharpminor.eval_expr prog e m a v -> - exec_assign prog e m id v m' -> - exec_stmt_prop e m (Csharpminor.Sassign id a) E0 m' Csharpminor.Out_normal. +Lemma match_is_call_cont: + forall tfn te sp tm k tk cenv xenv cs, + match_cont k tk cenv xenv cs -> + Csharpminor.is_call_cont k -> + exists tk', + star step tge (State tfn Sskip tk sp te tm) + E0 (State tfn Sskip tk' sp te tm) + /\ is_call_cont tk' + /\ match_cont k tk' cenv nil cs. Proof. - intros; red; intros. monadInv TR. - exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]]. - exploit var_set_correct; eauto. - intros [te2 [tm2 [EVAL2 [MINJ2 MATCH2]]]]. - exists f1; exists te2; exists tm2; exists Out_normal. - intuition. constructor. -Qed. - -Lemma transl_stmt_Sstore_correct: - forall (e : Csharpminor.env) (m : mem) (chunk : memory_chunk) - (a b : Csharpminor.expr) (v1 v2 : val) (m' : mem), - Csharpminor.eval_expr prog e m a v1 -> - Csharpminor.eval_expr prog e m b v2 -> - storev chunk m v1 v2 = Some m' -> - exec_stmt_prop e m (Csharpminor.Sstore chunk a b) E0 m' Csharpminor.Out_normal. -Proof. - intros; red; intros. monadInv TR. - exploit transl_expr_correct. - eauto. eauto. eexact H. eauto. - intros [tv1 [EVAL1 INJ1]]. - exploit transl_expr_correct. - eauto. eauto. eexact H0. eauto. - intros [tv2 [EVAL2 INJ2]]. - exploit make_store_correct. - eexact EVAL1. eexact EVAL2. eauto. eauto. eauto. eauto. - intros [tm2 [EXEC [MINJ2 NEXTBLOCK]]]. - exists f1; exists te1; exists tm2; exists Out_normal. - intuition. - constructor. - unfold storev in H1; destruct v1; try discriminate. - inv INJ1. - rewrite NEXTBLOCK. replace (nextblock m') with (nextblock m). - eapply match_callstack_mapped; eauto. congruence. - symmetry. eapply nextblock_store; eauto. -Qed. - -Lemma transl_stmt_Scall_correct: - forall (e : Csharpminor.env) (m : mem) (optid : option ident) - (sig : signature) (a : Csharpminor.expr) - (bl : list Csharpminor.expr) (vf : val) (vargs : list val) - (f : Csharpminor.fundef) (t : trace) (m1 : mem) (vres : val) - (m2 : mem), - Csharpminor.eval_expr prog e m a vf -> - Csharpminor.eval_exprlist prog e m bl vargs -> - Genv.find_funct (Genv.globalenv prog) vf = Some f -> - Csharpminor.funsig f = sig -> - Csharpminor.eval_funcall prog m f vargs t m1 vres -> - eval_funcall_prop m f vargs t m1 vres -> - exec_opt_assign prog e m1 optid vres m2 -> - exec_stmt_prop e m (Csharpminor.Scall optid sig a bl) t m2 Csharpminor.Out_normal. -Proof. - intros;red;intros. - assert (forall tv, val_inject f1 vf tv -> tv = vf). - intros. - elim (Genv.find_funct_inv H1). intros bf VF. rewrite VF in H1. - rewrite Genv.find_funct_find_funct_ptr in H1. - generalize (Genv.find_funct_ptr_negative H1). intro. - assert (match_globalenvs f1). eapply match_callstack_match_globalenvs; eauto. - generalize (mg_functions _ H8 _ H7). intro. - rewrite VF in H6. inv H6. - decEq. congruence. - replace x with 0. reflexivity. congruence. - inv H5; monadInv TR. - (* optid = None *) - exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]]. - exploit transl_exprlist_correct; eauto. intros [tv2 [EVAL2 VINJ2]]. - rewrite <- (H6 _ VINJ1) in H1. - elim (functions_translated _ _ H1). intros tf [FIND TRF]. - exploit H4; eauto. - intros [f2 [tm2 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]]. - exists f2; exists te1; exists tm2; exists Out_normal. - intuition. eapply exec_Scall; eauto. - apply sig_preserved; auto. - constructor. - (* optid = Some id *) - exploit transl_expr_correct; eauto. intros [tv1 [EVAL1 VINJ1]]. - exploit transl_exprlist_correct; eauto. intros [tv2 [EVAL2 VINJ2]]. - rewrite <- (H6 _ VINJ1) in H1. - elim (functions_translated _ _ H1). intros tf [FIND TRF]. - exploit H4; eauto. - intros [f2 [tm2 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]]. - exploit var_set_self_correct. - eauto. eexact MATCH3. eauto. eauto. eauto. - intros [te3 [tm3 [EVAL4 [MINJ4 MATCH4]]]]. - exists f2; exists te3; exists tm3; exists Out_normal. intuition. - eapply exec_Sseq_continue. eapply exec_Scall; eauto. - apply sig_preserved; auto. - simpl. eexact EVAL4. traceEq. - constructor. + induction 1; simpl; intros; try contradiction. + econstructor; split. apply star_refl. split. exact I. econstructor; eauto. + exploit IHmatch_cont; eauto. + intros [tk' [A B]]. exists tk'; split. + eapply star_left; eauto. constructor. traceEq. auto. + econstructor; split. apply star_refl. split. exact I. econstructor; eauto. + econstructor; split. apply star_refl. split. exact I. econstructor; eauto. Qed. -Lemma transl_stmt_Sseq_continue_correct: - forall (e : Csharpminor.env) (m : mem) (s1 s2 : Csharpminor.stmt) - (t1 t2: trace) (m1 m2 : mem) (t: trace) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m s1 t1 m1 Csharpminor.Out_normal -> - exec_stmt_prop e m s1 t1 m1 Csharpminor.Out_normal -> - Csharpminor.exec_stmt prog e m1 s2 t2 m2 out -> - exec_stmt_prop e m1 s2 t2 m2 out -> - t = t1 ** t2 -> - exec_stmt_prop e m (Csharpminor.Sseq s1 s2) t m2 out. -Proof. - intros; red; intros; monadInv TR. - exploit H0; eauto. - intros [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - exploit H2; eauto. - intros [f3 [te3 [tm3 [tout2 [EXEC2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. - exists f3; exists te3; exists tm3; exists tout2. - intuition. eapply exec_Sseq_continue; eauto. - inversion OINJ1. subst tout1. auto. - eapply inject_incr_trans; eauto. -Qed. - -Lemma transl_stmt_Sseq_stop_correct: - forall (e : Csharpminor.env) (m : mem) (s1 s2 : Csharpminor.stmt) - (t1: trace) (m1 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m s1 t1 m1 out -> - exec_stmt_prop e m s1 t1 m1 out -> - out <> Csharpminor.Out_normal -> - exec_stmt_prop e m (Csharpminor.Sseq s1 s2) t1 m1 out. -Proof. - intros; red; intros; monadInv TR. - exploit H0; eauto. - intros [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - exists f2; exists te2; exists tm2; exists tout1. - intuition. eapply exec_Sseq_stop; eauto. - inversion OINJ1; subst out tout1; congruence. -Qed. - -Lemma transl_stmt_Sifthenelse_correct: - forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (sl1 sl2 : Csharpminor.stmt) (v : val) (vb : bool) (t : trace) - (m' : mem) (out : Csharpminor.outcome), - Csharpminor.eval_expr prog e m a v -> - Val.bool_of_val v vb -> - Csharpminor.exec_stmt prog e m (if vb then sl1 else sl2) t m' out -> - exec_stmt_prop e m (if vb then sl1 else sl2) t m' out -> - exec_stmt_prop e m (Csharpminor.Sifthenelse a sl1 sl2) t m' out. -Proof. - intros; red; intros. monadInv TR. - exploit transl_expr_correct; eauto. - intros [tv1 [EVAL1 VINJ1]]. - assert (transl_stmt cenv (if vb then sl1 else sl2) = - OK (if vb then x0 else x1)). destruct vb; auto. - exploit H2; eauto. - intros [f2 [te2 [tm2 [tout [EVAL2 [OINJ [MINJ2 [INCR2 MATCH2]]]]]]]]. - exists f2; exists te2; exists tm2; exists tout. - intuition. - eapply exec_Sifthenelse; eauto. - eapply bool_of_val_inject; eauto. -Qed. - -Lemma transl_stmt_Sloop_loop_correct: - forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) - (t1: trace) (m1: mem) (t2: trace) (m2 : mem) - (out : Csharpminor.outcome) (t: trace), - Csharpminor.exec_stmt prog e m sl t1 m1 Csharpminor.Out_normal -> - exec_stmt_prop e m sl t1 m1 Csharpminor.Out_normal -> - Csharpminor.exec_stmt prog e m1 (Csharpminor.Sloop sl) t2 m2 out -> - exec_stmt_prop e m1 (Csharpminor.Sloop sl) t2 m2 out -> - t = t1 ** t2 -> - exec_stmt_prop e m (Csharpminor.Sloop sl) t m2 out. -Proof. - intros; red; intros. generalize TR; intro TR'; monadInv TR'. - exploit H0; eauto. - intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - exploit H2; eauto. - intros [f3 [te3 [tm3 [tout2 [EVAL2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. - exists f3; exists te3; exists tm3; exists tout2. - intuition. - eapply exec_Sloop_loop; eauto. - inversion OINJ1; subst tout1; eauto. - eapply inject_incr_trans; eauto. -Qed. - -Lemma transl_stmt_Sloop_exit_correct: - forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) - (t1: trace) (m1 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m sl t1 m1 out -> - exec_stmt_prop e m sl t1 m1 out -> - out <> Csharpminor.Out_normal -> - exec_stmt_prop e m (Csharpminor.Sloop sl) t1 m1 out. -Proof. - intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - exists f2; exists te2; exists tm2; exists tout1. - intuition. eapply exec_Sloop_stop; eauto. - inversion OINJ1; subst out tout1; congruence. -Qed. - -Remark outcome_block_inject: - forall f out tout, - outcome_inject f out tout -> - outcome_inject f (Csharpminor.outcome_block out) (outcome_block tout). -Proof. - induction 1; simpl. - constructor. - destruct n; constructor. - constructor. - constructor; auto. -Qed. +(** Properties of [switch] compilation *) + +Require Import Switch. -Lemma transl_stmt_Sblock_correct: - forall (e : Csharpminor.env) (m : mem) (sl : Csharpminor.stmt) - (t1: trace) (m1 : mem) (out : Csharpminor.outcome), - Csharpminor.exec_stmt prog e m sl t1 m1 out -> - exec_stmt_prop e m sl t1 m1 out -> - exec_stmt_prop e m (Csharpminor.Sblock sl) t1 m1 - (Csharpminor.outcome_block out). +Remark switch_table_shift: + forall n sl base dfl, + switch_target n (S dfl) (switch_table sl (S base)) = + S (switch_target n dfl (switch_table sl base)). Proof. - intros; red; intros. monadInv TR. - exploit H0; eauto. - intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. - exists f2; exists te2; exists tm2; exists (outcome_block tout1). - intuition. eapply exec_Sblock; eauto. - apply outcome_block_inject; auto. + induction sl; intros; simpl. auto. destruct (Int.eq n i); auto. Qed. -Lemma transl_stmt_Sexit_correct: - forall (e : Csharpminor.env) (m : mem) (n : nat), - exec_stmt_prop e m (Csharpminor.Sexit n) E0 m (Csharpminor.Out_exit n). +Remark length_switch_table: + forall sl base1 base2, + length (switch_table sl base1) = length (switch_table sl base2). Proof. - intros; red; intros. monadInv TR. - exists f1; exists te1; exists tm1; exists (Out_exit n). - intuition. constructor. constructor. + induction sl; intros; simpl. auto. decEq; auto. Qed. -Lemma transl_stmt_Sswitch_correct: - forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (cases : list (int * nat)) (default : nat) (n : int), - Csharpminor.eval_expr prog e m a (Vint n) -> - exec_stmt_prop e m (Csharpminor.Sswitch a cases default) E0 m - (Csharpminor.Out_exit (switch_target n default cases)). +Inductive transl_lblstmt_cont (cenv: compilenv) (xenv: exit_env): lbl_stmt -> cont -> cont -> Prop := + | tlsc_default: forall s k ts, + transl_stmt cenv (switch_env (LSdefault s) xenv) s = OK ts -> + transl_lblstmt_cont cenv xenv (LSdefault s) k (Kblock (Kseq ts k)) + | tlsc_case: forall i s ls k ts k', + transl_stmt cenv (switch_env (LScase i s ls) xenv) s = OK ts -> + transl_lblstmt_cont cenv xenv ls k k' -> + transl_lblstmt_cont cenv xenv (LScase i s ls) k (Kblock (Kseq ts k')). + +Lemma switch_descent: + forall cenv xenv k ls body s, + transl_lblstmt cenv (switch_env ls xenv) ls body = OK s -> + exists k', + transl_lblstmt_cont cenv xenv ls k k' + /\ (forall f sp e m, + plus step tge (State f s k sp e m) E0 (State f body k' sp e m)). Proof. - intros; red; intros. monadInv TR. - exploit transl_expr_correct; eauto. - intros [tv1 [EVAL VINJ1]]. - inv VINJ1. - exists f1; exists te1; exists tm1; exists (Out_exit (switch_target n default cases)). - split. constructor. auto. - split. constructor. - split. auto. - split. apply inject_incr_refl. - auto. + induction ls; intros. + monadInv H. econstructor; split. + econstructor; eauto. + intros. eapply plus_left. constructor. apply star_one. constructor. traceEq. + monadInv H. exploit IHls; eauto. intros [k' [A B]]. + econstructor; split. + econstructor; eauto. + intros. eapply plus_star_trans. eauto. + eapply star_left. constructor. apply star_one. constructor. + reflexivity. traceEq. +Qed. + +Lemma switch_ascent: + forall f n sp e m cenv xenv k ls k1, + let tbl := switch_table ls O in + let ls' := select_switch n ls in + transl_lblstmt_cont cenv xenv ls k k1 -> + exists k2, + star step tge (State f (Sexit (switch_target n (length tbl) tbl)) k1 sp e m) + E0 (State f (Sexit O) k2 sp e m) + /\ transl_lblstmt_cont cenv xenv ls' k k2. +Proof. + induction ls; intros; unfold tbl, ls'; simpl. + inv H. econstructor; split. apply star_refl. econstructor; eauto. + simpl in H. inv H. + rewrite Int.eq_sym. destruct (Int.eq i n). + econstructor; split. apply star_refl. econstructor; eauto. + exploit IHls; eauto. intros [k2 [A B]]. + rewrite (length_switch_table ls 1%nat 0%nat). + rewrite switch_table_shift. + econstructor; split. + eapply star_left. constructor. eapply star_left. constructor. eexact A. + reflexivity. traceEq. + exact B. +Qed. + +Lemma switch_match_cont: + forall cenv xenv k cs tk ls tk', + match_cont k tk cenv xenv cs -> + transl_lblstmt_cont cenv xenv ls tk tk' -> + match_cont (Csharpminor.Kseq (seq_of_lbl_stmt ls) k) tk' cenv (false :: switch_env ls xenv) cs. +Proof. + induction ls; intros; simpl. + inv H0. apply match_Kblock2. econstructor; eauto. + inv H0. apply match_Kblock2. eapply match_Kseq2. auto. eauto. +Qed. + +Lemma transl_lblstmt_suffix: + forall n cenv xenv ls body ts, + transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts -> + let ls' := select_switch n ls in + exists body', exists ts', + transl_lblstmt cenv (switch_env ls' xenv) ls' body' = OK ts'. +Proof. + induction ls; simpl; intros. + monadInv H. + exists body; econstructor. rewrite EQ; eauto. simpl. reflexivity. + monadInv H. + destruct (Int.eq i n). + exists body; econstructor. simpl. rewrite EQ; simpl. rewrite EQ0; simpl. reflexivity. + eauto. Qed. -Lemma transl_stmt_Sreturn_none_correct: - forall (e : Csharpminor.env) (m : mem), - exec_stmt_prop e m (Csharpminor.Sreturn None) E0 m - (Csharpminor.Out_return None). +Lemma switch_match_states: + forall fn k e m tfn ts tk sp te tm cenv xenv f lo hi cs sz ls body tk' + (TRF: transl_funbody cenv sz fn = OK tfn) + (TR: transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts) + (MINJ: mem_inject f m tm) + (MCS: match_callstack f + (mkframe cenv e te sp lo hi :: cs) + m.(nextblock) tm.(nextblock) m) + (MK: match_cont k tk cenv xenv cs) + (TK: transl_lblstmt_cont cenv xenv ls tk tk'), + exists S, + plus step tge (State tfn (Sexit O) tk' (Vptr sp Int.zero) te tm) E0 S + /\ match_states (Csharpminor.State fn (seq_of_lbl_stmt ls) k e m) S. +Proof. + intros. destruct ls; simpl. + inv TK. econstructor; split. + eapply plus_left. constructor. apply star_one. constructor. traceEq. + eapply match_state; eauto. + inv TK. econstructor; split. + eapply plus_left. constructor. apply star_one. constructor. traceEq. + eapply match_state_seq; eauto. + simpl. eapply switch_match_cont; eauto. +Qed. + +(** Commutation between [find_label] and compilation *) + +Section FIND_LABEL. + +Variable lbl: label. +Variable cenv: compilenv. +Variable cs: callstack. + +Remark find_label_var_set: + forall id e s k, + var_set cenv id e = OK s -> + find_label lbl s k = None. +Proof. + intros. unfold var_set in H. + destruct (cenv!!id); monadInv H; reflexivity. +Qed. + +Lemma transl_lblstmt_find_label_context: + forall cenv xenv ls body ts tk1 tk2 ts' tk', + transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts -> + transl_lblstmt_cont cenv xenv ls tk1 tk2 -> + find_label lbl body tk2 = Some (ts', tk') -> + find_label lbl ts tk1 = Some (ts', tk'). +Proof. + induction ls; intros. + monadInv H. inv H0. simpl. simpl in H2. replace x with ts by congruence. rewrite H1. auto. + monadInv H. inv H0. + eapply IHls. eauto. eauto. simpl in H6. replace x with ts0 by congruence. simpl. + rewrite H1. auto. +Qed. + +Lemma transl_find_label: + forall s k xenv ts tk, + transl_stmt cenv xenv s = OK ts -> + match_cont k tk cenv xenv cs -> + match Csharpminor.find_label lbl s k with + | None => find_label lbl ts tk = None + | Some(s', k') => + exists ts', exists tk', exists xenv', + find_label lbl ts tk = Some(ts', tk') + /\ transl_stmt cenv xenv' s' = OK ts' + /\ match_cont k' tk' cenv xenv' cs + end + +with transl_lblstmt_find_label: + forall ls xenv body k ts tk tk1, + transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts -> + match_cont k tk cenv xenv cs -> + transl_lblstmt_cont cenv xenv ls tk tk1 -> + find_label lbl body tk1 = None -> + match Csharpminor.find_label_ls lbl ls k with + | None => find_label lbl ts tk = None + | Some(s', k') => + exists ts', exists tk', exists xenv', + find_label lbl ts tk = Some(ts', tk') + /\ transl_stmt cenv xenv' s' = OK ts' + /\ match_cont k' tk' cenv xenv' cs + end. Proof. - intros; red; intros. monadInv TR. - exists f1; exists te1; exists tm1; exists (Out_return None). - intuition. constructor. constructor. -Qed. + intros. destruct s; try (monadInv H); simpl; auto. + (* assign *) + eapply find_label_var_set; eauto. + (* call *) + destruct o; monadInv H; simpl; auto. + eapply find_label_var_set; eauto. + (* seq *) + exploit (transl_find_label s1). eauto. eapply match_Kseq. eexact EQ1. eauto. + destruct (Csharpminor.find_label lbl s1 (Csharpminor.Kseq s2 k)) as [[s' k'] | ]. + intros [ts' [tk' [xenv' [A [B C]]]]]. + exists ts'; exists tk'; exists xenv'. intuition. rewrite A; auto. + intro. rewrite H. apply transl_find_label with xenv; auto. + (* ifthenelse *) + exploit (transl_find_label s1). eauto. eauto. + destruct (Csharpminor.find_label lbl s1 k) as [[s' k'] | ]. + intros [ts' [tk' [xenv' [A [B C]]]]]. + exists ts'; exists tk'; exists xenv'. intuition. rewrite A; auto. + intro. rewrite H. apply transl_find_label with xenv; auto. + (* loop *) + apply transl_find_label with xenv. auto. econstructor; eauto. simpl. rewrite EQ; auto. + (* block *) + apply transl_find_label with (true :: xenv). auto. constructor; auto. + (* switch *) + exploit switch_descent; eauto. intros [k' [A B]]. + eapply transl_lblstmt_find_label. eauto. eauto. eauto. reflexivity. + (* return *) + destruct o; monadInv H; auto. + (* label *) + destruct (ident_eq lbl l). + exists x; exists tk; exists xenv; auto. + apply transl_find_label with xenv; auto. + + intros. destruct ls; monadInv H; simpl. + (* default *) + inv H1. simpl in H3. replace x with ts by congruence. rewrite H2. + eapply transl_find_label; eauto. + (* case *) + inv H1. simpl in H7. + exploit (transl_find_label s). eauto. eapply switch_match_cont; eauto. + destruct (Csharpminor.find_label lbl s (Csharpminor.Kseq (seq_of_lbl_stmt ls) k)) as [[s' k''] | ]. + intros [ts' [tk' [xenv' [A [B C]]]]]. + exists ts'; exists tk'; exists xenv'; intuition. + eapply transl_lblstmt_find_label_context; eauto. + simpl. replace x with ts0 by congruence. rewrite H2. auto. + intro. + eapply transl_lblstmt_find_label. eauto. auto. eauto. + simpl. replace x with ts0 by congruence. rewrite H2. auto. +Qed. + +Remark find_label_store_parameters: + forall vars s k, + store_parameters cenv vars = OK s -> find_label lbl s k = None. +Proof. + induction vars; intros. + monadInv H. auto. + simpl in H. destruct a as [id lv]. monadInv H. + simpl. rewrite (find_label_var_set id (Evar id)); auto. +Qed. + +End FIND_LABEL. + +Lemma transl_find_label_body: + forall cenv xenv size f tf k tk cs lbl s' k', + transl_funbody cenv size f = OK tf -> + match_cont k tk cenv xenv cs -> + Csharpminor.find_label lbl f.(Csharpminor.fn_body) (Csharpminor.call_cont k) = Some (s', k') -> + exists ts', exists tk', exists xenv', + find_label lbl tf.(fn_body) (call_cont tk) = Some(ts', tk') + /\ transl_stmt cenv xenv' s' = OK ts' + /\ match_cont k' tk' cenv xenv' cs. +Proof. + intros. monadInv H. simpl. + rewrite (find_label_store_parameters lbl cenv (Csharpminor.fn_params f)); auto. + exploit transl_find_label. eexact EQ. eapply match_call_cont. eexact H0. + instantiate (1 := lbl). rewrite H1. auto. +Qed. + + +Require Import Coq.Program.Equality. + +Fixpoint seq_left_depth (s: Csharpminor.stmt) : nat := + match s with + | Csharpminor.Sseq s1 s2 => S (seq_left_depth s1) + | _ => O + end. + +Definition measure (S: Csharpminor.state) : nat := + match S with + | Csharpminor.State fn s k e m => seq_left_depth s + | _ => O + end. -Lemma transl_stmt_Sreturn_some_correct: - forall (e : Csharpminor.env) (m : mem) (a : Csharpminor.expr) - (v : val), - Csharpminor.eval_expr prog e m a v -> - exec_stmt_prop e m (Csharpminor.Sreturn (Some a)) E0 m - (Csharpminor.Out_return (Some v)). +Lemma transl_step_correct: + forall S1 t S2, Csharpminor.step gve S1 t S2 -> + forall T1, match_states S1 T1 -> + (exists T2, plus step tge T1 t T2 /\ match_states S2 T2) + \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat. Proof. - intros; red; intros; monadInv TR. - exploit transl_expr_correct; eauto. - intros [tv1 [EVAL VINJ1]]. - exists f1; exists te1; exists tm1; exists (Out_return (Some tv1)). - intuition. econstructor; eauto. constructor; auto. -Qed. - -(** We conclude by an induction over the structure of the Csharpminor - evaluation derivation, using the lemmas above for each case. *) - -Lemma transl_function_correct: - forall m1 f vargs t m2 vres, - Csharpminor.eval_funcall prog m1 f vargs t m2 vres -> - eval_funcall_prop m1 f vargs t m2 vres. -Proof - (Csharpminor.eval_funcall_ind2 prog - eval_funcall_prop - exec_stmt_prop - - transl_funcall_internal_correct - transl_funcall_external_correct - transl_stmt_Sskip_correct - transl_stmt_Sassign_correct - transl_stmt_Sstore_correct - transl_stmt_Scall_correct - transl_stmt_Sseq_continue_correct - transl_stmt_Sseq_stop_correct - transl_stmt_Sifthenelse_correct - transl_stmt_Sloop_loop_correct - transl_stmt_Sloop_exit_correct - transl_stmt_Sblock_correct - transl_stmt_Sexit_correct - transl_stmt_Sswitch_correct - transl_stmt_Sreturn_none_correct - transl_stmt_Sreturn_some_correct). - -Lemma transl_stmt_correct: - forall e m1 s t m2 out, - Csharpminor.exec_stmt prog e m1 s t m2 out -> - exec_stmt_prop e m1 s t m2 out. -Proof - (Csharpminor.exec_stmt_ind2 prog - eval_funcall_prop - exec_stmt_prop - - transl_funcall_internal_correct - transl_funcall_external_correct - transl_stmt_Sskip_correct - transl_stmt_Sassign_correct - transl_stmt_Sstore_correct - transl_stmt_Scall_correct - transl_stmt_Sseq_continue_correct - transl_stmt_Sseq_stop_correct - transl_stmt_Sifthenelse_correct - transl_stmt_Sloop_loop_correct - transl_stmt_Sloop_exit_correct - transl_stmt_Sblock_correct - transl_stmt_Sexit_correct - transl_stmt_Sswitch_correct - transl_stmt_Sreturn_none_correct - transl_stmt_Sreturn_some_correct). - -(** ** Semantic preservation for divergence *) - -Definition evalinf_funcall_prop - (m1: mem) (fn: Csharpminor.fundef) (args: list val) (t: traceinf) : Prop := - forall tfn f1 tm1 cs targs - (TR: transl_fundef gce fn = OK tfn) - (MINJ: mem_inject f1 m1 tm1) - (MATCH: match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1) - (ARGSINJ: val_list_inject f1 args targs), - evalinf_funcall tge tm1 tfn targs t. - -Definition execinf_stmt_prop - (e: Csharpminor.env) (m1: mem) (s: Csharpminor.stmt) (t: traceinf): Prop := - forall cenv ts f1 te1 tm1 sp lo hi cs - (TR: transl_stmt cenv s = OK ts) - (MINJ: mem_inject f1 m1 tm1) - (MATCH: match_callstack f1 - (mkframe cenv e te1 sp lo hi :: cs) - m1.(nextblock) tm1.(nextblock) m1), - execinf_stmt tge (Vptr sp Int.zero) te1 tm1 ts t. - -Theorem transl_function_divergence_correct: - forall m1 fn args t, - Csharpminor.evalinf_funcall prog m1 fn args t -> - evalinf_funcall_prop m1 fn args t. -Proof. - unfold evalinf_funcall_prop; cofix FUNCALL. - assert (STMT: forall e m1 s t, - Csharpminor.execinf_stmt prog e m1 s t -> - execinf_stmt_prop e m1 s t). - unfold execinf_stmt_prop; cofix STMT. - intros. inv H; simpl in TR; try (monadInv TR). - (* Scall *) - assert (forall tv, val_inject f1 vf tv -> tv = vf). - intros. - elim (Genv.find_funct_inv H2). intros bf VF. rewrite VF in H2. - rewrite Genv.find_funct_find_funct_ptr in H2. - generalize (Genv.find_funct_ptr_negative H2). intro. - assert (match_globalenvs f1). eapply match_callstack_match_globalenvs; eauto. - generalize (mg_functions _ H5 _ H3). intro. - rewrite VF in H. inv H. - decEq. congruence. - replace x with 0. reflexivity. congruence. - destruct optid; monadInv TR. - (* optid = Some i *) - destruct (transl_expr_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H0 _ EQ) - as [tv1 [EVAL1 VINJ1]]. - destruct (transl_exprlist_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H1 _ EQ1) - as [tv2 [EVAL2 VINJ2]]. - rewrite <- (H _ VINJ1) in H2. - elim (functions_translated _ _ H2). intros tf [FIND TRF]. - apply execinf_Sseq_1. eapply execinf_Scall. - eauto. eauto. eauto. apply sig_preserved; auto. - eapply FUNCALL; eauto. - (* optid = None *) - destruct (transl_expr_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H0 _ EQ) - as [tv1 [EVAL1 VINJ1]]. - destruct (transl_exprlist_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H1 _ EQ1) - as [tv2 [EVAL2 VINJ2]]. - rewrite <- (H _ VINJ1) in H2. - elim (functions_translated _ _ H2). intros tf [FIND TRF]. - eapply execinf_Scall. - eauto. eauto. eauto. apply sig_preserved; auto. - eapply FUNCALL; eauto. - (* Sseq, 1 *) - apply execinf_Sseq_1. eapply STMT; eauto. - (* Sseq, 2 *) - destruct (transl_stmt_correct _ _ _ _ _ _ H0 - _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout [EXEC1 [OUT [MINJ2 [INCR12 MATCH2]]]]]]]]. - inv OUT. - eapply execinf_Sseq_2. eexact EXEC1. - eapply STMT; eauto. + induction 1; intros T1 MSTATE; inv MSTATE. + +(* skip seq *) + monadInv TR. left. + dependent induction MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + econstructor; split. + apply plus_one. constructor. + eapply match_state_seq; eauto. + exploit IHMK; eauto. intros [T2 [A B]]. + exists T2; split. eapply plus_left. constructor. apply plus_star; eauto. traceEq. auto. - (* Sifthenelse, true *) - destruct (transl_expr_correct _ _ _ _ _ _ _ _ _ _ MINJ MATCH _ _ H0 _ EQ) - as [tv1 [EVAL1 VINJ1]]. - assert (transl_stmt cenv (if vb then sl1 else sl2) = - OK (if vb then x0 else x1)). destruct vb; auto. - eapply execinf_Sifthenelse. eexact EVAL1. - eapply bool_of_val_inject; eauto. - eapply STMT; eauto. - (* Sloop, body *) - eapply execinf_Sloop_body. eapply STMT; eauto. - (* Sloop, loop *) - destruct (transl_stmt_correct _ _ _ _ _ _ H0 - _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout [EXEC1 [OUT [MINJ2 [INCR12 MATCH2]]]]]]]]. - inv OUT. - eapply execinf_Sloop_loop. eexact EXEC1. - eapply STMT; eauto. - simpl. rewrite EQ. auto. auto. - (* Sblock *) - apply execinf_Sblock. eapply STMT; eauto. - (* stutter *) - generalize (execinf_stmt_N_inv _ _ _ _ _ _ H0); intro. - destruct s; try contradiction; monadInv TR. - apply execinf_Sseq_1. eapply STMT; eauto. - apply execinf_Sblock. eapply STMT; eauto. - (* Sloop_block *) - destruct (transl_stmt_correct _ _ _ _ _ _ H0 - _ _ _ _ _ _ _ _ _ EQ MINJ MATCH) - as [f2 [te2 [tm2 [tout [EXEC1 [OUT [MINJ2 [INCR12 MATCH2]]]]]]]]. - inv OUT. - eapply execinf_Sloop_loop. eexact EXEC1. - eapply STMT with (s := Csharpminor.Sloop sl); eauto. - apply execinf_Sblock_inv; eauto. - simpl. rewrite EQ; auto. auto. - (* Function *) - intros. inv H. - monadInv TR. generalize EQ. - unfold transl_function. - caseEq (build_compilenv gce f); intros cenv stacksize CENV. - destruct (zle stacksize Int.max_signed); try congruence. - intro TR. monadInv TR. - caseEq (alloc tm1 0 stacksize). intros tm2 sp ALLOC. - destruct (function_entry_ok _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - H1 H2 MATCH CENV z ALLOC ARGSINJ MINJ H0 EQ2) - as [f2 [te2 [tm3 [STOREPARAM [MINJ2 [INCR12 [MATCH2 BLOCKS]]]]]]]. - eapply evalinf_funcall_internal; simpl. - eauto. reflexivity. eapply execinf_Sseq_2. eexact STOREPARAM. - unfold execinf_stmt_prop in STMT. eapply STMT; eauto. +(* skip block *) + monadInv TR. left. + dependent induction MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + exploit IHMK; eauto. intros [T2 [A B]]. + exists T2; split. eapply plus_left. constructor. apply plus_star; eauto. traceEq. + auto. +(* skip call *) + monadInv TR. left. + exploit match_is_call_cont; eauto. intros [tk' [A [B C]]]. + exploit match_callstack_freelist; eauto. intros [P Q]. + econstructor; split. + eapply plus_right. eexact A. apply step_skip_call. auto. + rewrite (sig_preserved_body _ _ _ _ TRF). auto. traceEq. + econstructor; eauto. rewrite nextblock_freelist. simpl. eauto. + +(* assign *) + monadInv TR. + exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. + exploit var_set_correct; eauto. intros [te' [tm' [EXEC [MINJ' [MCS' OTHER]]]]]. + left; econstructor; split. + apply plus_one. eexact EXEC. + econstructor; eauto. + +(* store *) + monadInv TR. + exploit transl_expr_correct. eauto. eauto. eexact H. eauto. + intros [tv1 [EVAL1 VINJ1]]. + exploit transl_expr_correct. eauto. eauto. eexact H0. eauto. + intros [tv2 [EVAL2 VINJ2]]. + exploit make_store_correct. eexact EVAL1. eexact EVAL2. eauto. eauto. auto. auto. + intros [tm' [EXEC [MINJ' NEXTBLOCK]]]. + left; econstructor; split. + apply plus_one. eexact EXEC. + unfold storev in H1; destruct vaddr; try discriminate. + econstructor; eauto. + replace (nextblock m') with (nextblock m). rewrite NEXTBLOCK. eauto. + eapply match_callstack_mapped; eauto. inv VINJ1. congruence. + symmetry. eapply nextblock_store; eauto. + +(* call *) + simpl in H1. exploit functions_translated; eauto. intros [tfd [FIND TRANS]]. + simpl in TR. destruct optid; monadInv TR. +(* with return value *) + exploit transl_expr_correct; eauto. + intros [tvf [EVAL1 VINJ1]]. + assert (tvf = vf). + eapply val_inject_function_pointer; eauto. + eapply match_callstack_match_globalenvs; eauto. + subst tvf. + exploit transl_exprlist_correct; eauto. + intros [tvargs [EVAL2 VINJ2]]. + left; econstructor; split. + eapply plus_left. constructor. apply star_one. + eapply step_call; eauto. + apply sig_preserved; eauto. traceEq. -Qed. + econstructor; eauto. + eapply match_Kcall_some with (cenv' := cenv); eauto. + red; auto. +(* without return value *) + exploit transl_expr_correct; eauto. + intros [tvf [EVAL1 VINJ1]]. + assert (tvf = vf). + eapply val_inject_function_pointer; eauto. + eapply match_callstack_match_globalenvs; eauto. + subst tvf. + exploit transl_exprlist_correct; eauto. + intros [tvargs [EVAL2 VINJ2]]. + left; econstructor; split. + apply plus_one. + eapply step_call; eauto. + apply sig_preserved; eauto. + econstructor; eauto. + eapply match_Kcall_none with (cenv' := cenv); eauto. + red; auto. -(** ** Semantic preservation for whole programs *) +(* seq *) + monadInv TR. + left; econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + econstructor; eauto. +(* seq 2 *) + right. split. auto. split. auto. econstructor; eauto. + +(* ifthenelse *) + monadInv TR. + exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. + left; exists (State tfn (if b then x0 else x1) tk (Vptr sp Int.zero) te tm); split. + apply plus_one. eapply step_ifthenelse; eauto. eapply bool_of_val_inject; eauto. + econstructor; eauto. destruct b; auto. + +(* loop *) + monadInv TR. + left; econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + econstructor; eauto. simpl. rewrite EQ; auto. -(** The [match_globalenvs] relation holds for the global environments - of the source program and the transformed program. *) +(* block *) + monadInv TR. + left; econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + econstructor; eauto. + +(* exit seq *) + monadInv TR. left. + dependent induction MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl. auto. + exploit IHMK; eauto. intros [T2 [A B]]. + exists T2; split; auto. eapply plus_left. constructor. apply plus_star; eauto. traceEq. + exploit IHMK; eauto. intros [T2 [A B]]. + exists T2; split; auto. eapply plus_left. + simpl. constructor. apply plus_star; eauto. traceEq. + +(* exit block 0 *) + monadInv TR. left. + dependent induction MK. + econstructor; split. + simpl. apply plus_one. constructor. + econstructor; eauto. + exploit IHMK; eauto. intros [T2 [A B]]. + exists T2; split; auto. simpl. + eapply plus_left. constructor. apply plus_star; eauto. traceEq. + +(* exit block n+1 *) + monadInv TR. left. + dependent induction MK. + econstructor; split. + simpl. apply plus_one. constructor. + econstructor; eauto. auto. + exploit IHMK; eauto. intros [T2 [A B]]. + exists T2; split; auto. simpl. + eapply plus_left. constructor. apply plus_star; eauto. traceEq. + +(* switch *) + monadInv TR. left. + exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. + inv VINJ. + exploit switch_descent; eauto. intros [k1 [A B]]. + exploit switch_ascent; eauto. intros [k2 [C D]]. + exploit transl_lblstmt_suffix; eauto. simpl. intros [body' [ts' E]]. + exploit switch_match_states; eauto. intros [T2 [F G]]. + exists T2; split. + eapply plus_star_trans. eapply B. + eapply star_left. econstructor; eauto. + eapply star_trans. eexact C. + apply plus_star. eexact F. + reflexivity. reflexivity. traceEq. + auto. + +(* return none *) + monadInv TR. left. + exploit match_callstack_freelist; eauto. intros [A B]. + econstructor; split. + apply plus_one. apply step_return_0. +(* + rewrite (sig_preserved_body _ _ _ _ TRF). auto. +*) + econstructor; eauto. rewrite nextblock_freelist. simpl. eauto. + eapply match_call_cont; eauto. + +(* return some *) + monadInv TR. left. + exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. + exploit match_callstack_freelist; eauto. intros [A B]. + econstructor; split. + apply plus_one. apply step_return_1. eauto. + econstructor; eauto. rewrite nextblock_freelist. simpl. eauto. + eapply match_call_cont; eauto. + +(* label *) + monadInv TR. + left; econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + +(* goto *) + monadInv TR. + exploit transl_find_label_body; eauto. + intros [ts' [tk' [xenv' [A [B C]]]]]. + left; econstructor; split. + apply plus_one. apply step_goto. eexact A. + econstructor; eauto. + +(* internal call *) + monadInv TR. generalize EQ; clear EQ; unfold transl_function. + caseEq (build_compilenv gce f). intros ce sz BC. + destruct (zle sz Int.max_signed); try congruence. + intro TRBODY. + generalize TRBODY; intro TMP. monadInv TMP. + caseEq (alloc tm 0 sz). intros tm' sp ALLOC'. + exploit function_entry_ok; eauto. + intros [f2 [te2 [tm2 [EXEC [MINJ2 [IINCR MCS2]]]]]]. + left; econstructor; split. + eapply plus_left. constructor; simpl; eauto. + simpl. eapply star_left. constructor. + eapply star_right. eexact EXEC. constructor. + reflexivity. reflexivity. traceEq. + econstructor. eexact TRBODY. eauto. eexact MINJ2. + eexact MCS2. + inv MK; simpl in ISCC; contradiction || econstructor; eauto. + +(* external call *) + monadInv TR. + exploit event_match_inject; eauto. intros [A B]. + left; econstructor; split. + apply plus_one. econstructor; eauto. + econstructor; eauto. + +(* return *) + inv MK; inv H. + (* no argument *) + left; econstructor; split. + apply plus_one. econstructor; eauto. + simpl. econstructor; eauto. + (* one argument *) + exploit var_set_self_correct; eauto. + intros [te' [tm' [A [B C]]]]. + left; econstructor; split. + eapply plus_left. econstructor. simpl. eapply star_left. econstructor. + eapply star_one. eexact A. + reflexivity. traceEq. + econstructor; eauto. +Qed. Lemma match_globalenvs_init: let m := Genv.init_mem prog in - let tm := Genv.init_mem tprog in - let f := fun b => if zlt b m.(nextblock) then Some(b, 0) else None in - match_globalenvs f. + match_globalenvs (meminj_init m). Proof. intros. constructor. intros. split. - unfold f. rewrite zlt_true. auto. unfold m. - eapply Genv.find_symbol_not_fresh; eauto. + unfold meminj_init. rewrite zlt_true. auto. + unfold m; eapply Genv.find_symbol_not_fresh; eauto. rewrite <- H. apply symbols_preserved. - intros. unfold f. rewrite zlt_true. auto. + intros. unfold meminj_init. rewrite zlt_true. auto. generalize (nextblock_pos m). omega. Qed. -(** The correctness of the translation of a whole Csharpminor program - follows. *) +Lemma transl_initial_states: + forall S, Csharpminor.initial_state prog S -> + exists R, Cminor.initial_state tprog R /\ match_states S R. +Proof. + induction 1. + exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. + econstructor; split. + econstructor. + simpl. fold tge. rewrite symbols_preserved. + replace (prog_main tprog) with (prog_main prog). eexact H. + symmetry. unfold transl_program in TRANSL. + eapply transform_partial_program2_main; eauto. + eexact FIND. + rewrite <- H1. apply sig_preserved; auto. + rewrite (Genv.init_mem_transf_partial2 _ _ _ TRANSL). + fold m0. + eapply match_callstate with (f := meminj_init m0) (cs := @nil frame). + auto. + apply init_inject. unfold m0. apply Genv.initmem_inject_neutral. + constructor. apply match_globalenvs_init. + instantiate (1 := gce). constructor. + red; auto. + constructor. +Qed. + +Lemma transl_final_states: + forall S R r, + match_states S R -> Csharpminor.final_state S r -> Cminor.final_state R r. +Proof. + intros. inv H0. inv H. inv MK. inv RESINJ. constructor. +Qed. Theorem transl_program_correct: - forall beh, + forall (beh: program_behavior), Csharpminor.exec_program prog beh -> - exec_program tprog beh. -Proof. - intros. apply exec_program_bigstep_transition. - set (m0 := Genv.init_mem prog) in *. - set (f := meminj_init m0). - assert (MINJ0: mem_inject f m0 m0). - unfold f; apply init_inject. - unfold m0; apply Genv.initmem_inject_neutral. - assert (MATCH0: match_callstack f nil m0.(nextblock) m0.(nextblock) m0). - constructor. unfold f; apply match_globalenvs_init. - inv H. - (* Terminating case *) - subst ge0 m1. - elim (function_ptr_translated _ _ H1). intros tfn [TFIND TR]. - fold ge in H3. - exploit transl_function_correct; eauto. - intros [f1 [tm1 [tres [TEVAL [VINJ [MINJ1 [INCR MATCH1]]]]]]]. - econstructor; eauto. - fold tge. rewrite <- H0. fold ge. - replace (prog_main prog) with (AST.prog_main tprog). apply symbols_preserved. - apply transform_partial_program2_main with (transl_fundef gce) transl_globvar. assumption. - rewrite <- H2. apply sig_preserved; auto. - rewrite (Genv.init_mem_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). - inv VINJ. fold tge; fold m0. eexact TEVAL. - (* Diverging case *) - subst ge0 m1. - elim (function_ptr_translated _ _ H1). intros tfn [TFIND TR]. - econstructor; eauto. - fold tge. rewrite <- H0. fold ge. - replace (prog_main prog) with (AST.prog_main tprog). apply symbols_preserved. - apply transform_partial_program2_main with (transl_fundef gce) transl_globvar. assumption. - rewrite <- H2. apply sig_preserved; auto. - rewrite (Genv.init_mem_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). - fold tge; fold m0. - eapply (transl_function_divergence_correct _ _ _ _ H3); eauto. + Cminor.exec_program tprog beh. +Proof. + unfold Csharpminor.exec_program, Cminor.exec_program; intros. + eapply simulation_star_preservation; eauto. + eexact transl_initial_states. + eexact transl_final_states. + eexact transl_step_correct. Qed. End TRANSLATION. + diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 248192c..fb8b8e1 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -355,7 +355,7 @@ Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int := | I8, Unsigned => Int.zero_ext 8 i | I16, Signed => Int.sign_ext 16 i | I16, Unsigned => Int.zero_ext 16 i - | I32 , _ => i + | I32, _ => i end. Definition cast_int_float (si : signedness) (i: int) : float := @@ -422,49 +422,6 @@ Definition env := PTree.t block. (* map variable -> location *) Definition empty_env: env := (PTree.empty block). -(** The execution of a statement produces an ``outcome'', indicating - how the execution terminated: either normally or prematurely - through the execution of a [break], [continue] or [return] statement. *) - -Inductive outcome: Type := - | Out_break: outcome (**r terminated by [break] *) - | Out_continue: outcome (**r terminated by [continue] *) - | Out_normal: outcome (**r terminated normally *) - | Out_return: option val -> outcome. (**r terminated by [return] *) - -Inductive out_normal_or_continue : outcome -> Prop := - | Out_normal_or_continue_N: out_normal_or_continue Out_normal - | Out_normal_or_continue_C: out_normal_or_continue Out_continue. - -Inductive out_break_or_return : outcome -> outcome -> Prop := - | Out_break_or_return_B: out_break_or_return Out_break Out_normal - | Out_break_or_return_R: forall ov, - out_break_or_return (Out_return ov) (Out_return ov). - -Definition outcome_switch (out: outcome) : outcome := - match out with - | Out_break => Out_normal - | o => o - end. - -Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := - match out, t with - | Out_normal, Tvoid => v = Vundef - | Out_return None, Tvoid => v = Vundef - | Out_return (Some v'), ty => ty <> Tvoid /\ v'=v - | _, _ => False - end. - -(** Selection of the appropriate case of a [switch], given the value [n] - of the selector expression. *) - -Fixpoint select_switch (n: int) (sl: labeled_statements) - {struct sl}: labeled_statements := - match sl with - | LSdefault _ => sl - | LScase c s sl' => if Int.eq c n then sl else select_switch n sl' - end. - (** [load_value_of_type ty m b ofs] computes the value of a datum of type [ty] residing in memory [m] at block [b], offset [ofs]. If the type [ty] indicates an access by value, the corresponding @@ -491,24 +448,23 @@ Definition store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) end. (** Allocation of function-local variables. - [alloc_variables e1 m1 vars e2 m2 bl] allocates one memory block + [alloc_variables e1 m1 vars e2 m2] allocates one memory block for each variable declared in [vars], and associates the variable name with this block. [e1] and [m1] are the initial local environment and memory state. [e2] and [m2] are the final local environment - and memory state. The list [bl] collects the references to all - the blocks that were allocated. *) + and memory state. *) Inductive alloc_variables: env -> mem -> list (ident * type) -> - env -> mem -> list block -> Prop := + env -> mem -> Prop := | alloc_variables_nil: forall e m, - alloc_variables e m nil e m nil + alloc_variables e m nil e m | alloc_variables_cons: - forall e m id ty vars m1 b1 m2 e2 lb, + forall e m id ty vars m1 b1 m2 e2, Mem.alloc m 0 (sizeof ty) = (m1, b1) -> - alloc_variables (PTree.set id b1 e) m1 vars e2 m2 lb -> - alloc_variables e m ((id, ty) :: vars) e2 m2 (b1 :: lb). + alloc_variables (PTree.set id b1 e) m1 vars e2 m2 -> + alloc_variables e m ((id, ty) :: vars) e2 m2. (** Initialization of local variables that are parameters to a function. [bind_parameters e m1 params args m2] stores the values [args] @@ -528,10 +484,35 @@ Inductive bind_parameters: env -> bind_parameters e m1 params vl m2 -> bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2. -Section RELSEM. +(** Return the list of blocks in the codomain of [e]. *) + +Definition blocks_of_env (e: env) : list block := + List.map (@snd ident block) (PTree.elements e). + +(** Selection of the appropriate case of a [switch], given the value [n] + of the selector expression. *) + +Fixpoint select_switch (n: int) (sl: labeled_statements) + {struct sl}: labeled_statements := + match sl with + | LSdefault _ => sl + | LScase c s sl' => if Int.eq c n then sl else select_switch n sl' + end. + +(** Turn a labeled statement into a sequence *) + +Fixpoint seq_of_labeled_statement (sl: labeled_statements) : statement := + match sl with + | LSdefault s => s + | LScase c s sl' => Ssequence s (seq_of_labeled_statement sl') + end. + +Section SEMANTICS. Variable ge: genv. +(** ** Evaluation of expressions *) + Section EXPR. Variable e: env. @@ -640,6 +621,322 @@ Inductive eval_exprlist: list expr -> list val -> Prop := End EXPR. +(** ** Transition semantics for statements and functions *) + +(** Continuations *) + +Inductive cont: Type := + | Kstop: cont + | Kseq: statement -> cont -> cont + (* [Kseq s2 k] = after [s1] in [s1;s2] *) + | Kwhile: expr -> statement -> cont -> cont + (* [Kwhile e s k] = after [s] in [while (e) s] *) + | Kdowhile: expr -> statement -> cont -> cont + (* [Kdowhile e s k] = after [s] in [do s while (e)] *) + | Kfor2: expr -> statement -> statement -> cont -> cont + (* [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *) + | Kfor3: expr -> statement -> statement -> cont -> cont + (* [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *) + | Kswitch: cont -> cont + (* catches [break] statements arising out of [switch] *) + | Kcall: option (block * int * type) -> (* where to store result *) + function -> (* calling function *) + env -> (* local env of calling function *) + cont -> cont. + +(** Pop continuation until a call or stop *) + +Fixpoint call_cont (k: cont) : cont := + match k with + | Kseq s k => call_cont k + | Kwhile e s k => call_cont k + | Kdowhile e s k => call_cont k + | Kfor2 e2 e3 s k => call_cont k + | Kfor3 e2 e3 s k => call_cont k + | Kswitch k => call_cont k + | _ => k + end. + +Definition is_call_cont (k: cont) : Prop := + match k with + | Kstop => True + | Kcall _ _ _ _ => True + | _ => False + end. + +(** States *) + +Inductive state: Type := + | State + (f: function) + (s: statement) + (k: cont) + (e: env) + (m: mem) : state + | Callstate + (fd: fundef) + (args: list val) + (k: cont) + (m: mem) : state + | Returnstate + (res: val) + (k: cont) + (m: mem) : state. + +(** Find the statement and manufacture the continuation + corresponding to a label *) + +Fixpoint find_label (lbl: label) (s: statement) (k: cont) + {struct s}: option (statement * cont) := + match s with + | Ssequence s1 s2 => + match find_label lbl s1 (Kseq s2 k) with + | Some sk => Some sk + | None => find_label lbl s2 k + end + | Sifthenelse a s1 s2 => + match find_label lbl s1 k with + | Some sk => Some sk + | None => find_label lbl s2 k + end + | Swhile a s1 => + find_label lbl s1 (Kwhile a s1 k) + | Sdowhile a s1 => + find_label lbl s1 (Kdowhile a s1 k) + | Sfor a1 a2 a3 s1 => + match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 s1) k) with + | Some sk => Some sk + | None => + match find_label lbl s1 (Kfor2 a2 a3 s1 k) with + | Some sk => Some sk + | None => find_label lbl a3 (Kfor3 a2 a3 s1 k) + end + end + | Sswitch e sl => + find_label_ls lbl sl (Kswitch k) + | Slabel lbl' s' => + if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k + | _ => None + end + +with find_label_ls (lbl: label) (sl: labeled_statements) (k: cont) + {struct sl}: option (statement * cont) := + match sl with + | LSdefault s => find_label lbl s k + | LScase _ s sl' => + match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with + | Some sk => Some sk + | None => find_label_ls lbl sl' k + end + end. + +(** Transition relation *) + +Inductive step: state -> trace -> state -> Prop := + + | step_assign: forall f a1 a2 k e m 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' -> + step (State f (Sassign a1 a2) k e m) + E0 (State f Sskip k e m') + + | step_call_none: forall f a al k e m vf vargs fd, + eval_expr e m a vf -> + eval_exprlist e m al vargs -> + Genv.find_funct ge vf = Some fd -> + type_of_fundef fd = typeof a -> + step (State f (Scall None a al) k e m) + E0 (Callstate fd vargs (Kcall None f e k) m) + + | step_call_some: forall f lhs a al k e m loc ofs vf vargs fd, + 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 fd -> + type_of_fundef fd = typeof a -> + step (State f (Scall (Some lhs) a al) k e m) + E0 (Callstate fd vargs (Kcall (Some(loc, ofs, typeof lhs)) f e k) m) + + | step_seq: forall f s1 s2 k e m, + step (State f (Ssequence s1 s2) k e m) + E0 (State f s1 (Kseq s2 k) e m) + | step_skip_seq: forall f s k e m, + step (State f Sskip (Kseq s k) e m) + E0 (State f s k e m) + | step_continue_seq: forall f s k e m, + step (State f Scontinue (Kseq s k) e m) + E0 (State f Scontinue k e m) + | step_break_seq: forall f s k e m, + step (State f Sbreak (Kseq s k) e m) + E0 (State f Sbreak k e m) + + | step_ifthenelse_true: forall f a s1 s2 k e m v1, + eval_expr e m a v1 -> + is_true v1 (typeof a) -> + step (State f (Sifthenelse a s1 s2) k e m) + E0 (State f s1 k e m) + | step_ifthenelse_false: forall f a s1 s2 k e m v1, + eval_expr e m a v1 -> + is_false v1 (typeof a) -> + step (State f (Sifthenelse a s1 s2) k e m) + E0 (State f s2 k e m) + + | step_while_false: forall f a s k e m v, + eval_expr e m a v -> + is_false v (typeof a) -> + step (State f (Swhile a s) k e m) + E0 (State f Sskip k e m) + | step_while_true: forall f a s k e m v, + eval_expr e m a v -> + is_true v (typeof a) -> + step (State f (Swhile a s) k e m) + E0 (State f s (Kwhile a s k) e m) + | step_skip_or_continue_while: forall f x a s k e m, + x = Sskip \/ x = Scontinue -> + step (State f x (Kwhile a s k) e m) + E0 (State f (Swhile a s) k e m) + | step_break_while: forall f a s k e m, + step (State f Sbreak (Kwhile a s k) e m) + E0 (State f Sskip k e m) + + | step_dowhile: forall f a s k e m, + step (State f (Sdowhile a s) k e m) + E0 (State f s (Kdowhile a s k) e m) + | step_skip_or_continue_dowhile_false: forall f x a s k e m v, + x = Sskip \/ x = Scontinue -> + eval_expr e m a v -> + is_false v (typeof a) -> + step (State f x (Kdowhile a s k) e m) + E0 (State f Sskip k e m) + | step_skip_or_continue_dowhile_true: forall f x a s k e m v, + x = Sskip \/ x = Scontinue -> + eval_expr e m a v -> + is_true v (typeof a) -> + step (State f x (Kdowhile a s k) e m) + E0 (State f (Sdowhile a s) k e m) + | step_break_dowhile: forall f a s k e m, + step (State f Sbreak (Kdowhile a s k) e m) + E0 (State f Sskip k e m) + + | step_for_start: forall f a1 a2 a3 s k e m, + a1 <> Sskip -> + step (State f (Sfor a1 a2 a3 s) k e m) + E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m) + | step_for_false: forall f a2 a3 s k e m v, + eval_expr e m a2 v -> + is_false v (typeof a2) -> + step (State f (Sfor Sskip a2 a3 s) k e m) + E0 (State f Sskip k e m) + | step_for_true: forall f a2 a3 s k e m v, + eval_expr e m a2 v -> + is_true v (typeof a2) -> + step (State f (Sfor Sskip a2 a3 s) k e m) + E0 (State f s (Kfor2 a2 a3 s k) e m) + | step_skip_or_continue_for2: forall f x a2 a3 s k e m, + x = Sskip \/ x = Scontinue -> + step (State f x (Kfor2 a2 a3 s k) e m) + E0 (State f a3 (Kfor3 a2 a3 s k) e m) + | step_break_for2: forall f a2 a3 s k e m, + step (State f Sbreak (Kfor2 a2 a3 s k) e m) + E0 (State f Sskip k e m) + | step_skip_for3: forall f a2 a3 s k e m, + step (State f Sskip (Kfor3 a2 a3 s k) e m) + E0 (State f (Sfor Sskip a2 a3 s) k e m) + + | step_return_0: forall f k e m, + f.(fn_return) = Tvoid -> + step (State f (Sreturn None) k e m) + E0 (Returnstate Vundef (call_cont k) (Mem.free_list m (blocks_of_env e))) + | step_return_1: forall f a k e m v, + f.(fn_return) <> Tvoid -> + eval_expr e m a v -> + step (State f (Sreturn (Some a)) k e m) + E0 (Returnstate v (call_cont k) (Mem.free_list m (blocks_of_env e))) + | step_skip_call: forall f k e m, + is_call_cont k -> + f.(fn_return) = Tvoid -> + step (State f Sskip k e m) + E0 (Returnstate Vundef k (Mem.free_list m (blocks_of_env e))) + + | step_switch: forall f a sl k e m n, + eval_expr e m a (Vint n) -> + step (State f (Sswitch a sl) k e m) + E0 (State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m) + | step_skip_break_switch: forall f x k e m, + x = Sskip \/ x = Sbreak -> + step (State f x (Kswitch k) e m) + E0 (State f Sskip k e m) + | step_continue_switch: forall f k e m, + step (State f Scontinue (Kswitch k) e m) + E0 (State f Scontinue k e m) + + | step_label: forall f lbl s k e m, + step (State f (Slabel lbl s) k e m) + E0 (State f s k e m) + + | step_goto: forall f lbl k e m s' k', + find_label lbl f.(fn_body) (call_cont k) = Some (s', k') -> + step (State f (Sgoto lbl) k e m) + E0 (State f s' k' e m) + + | step_internal_function: forall f vargs k m e m1 m2, + alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> + bind_parameters e m1 f.(fn_params) vargs m2 -> + step (Callstate (Internal f) vargs k m) + E0 (State f f.(fn_body) k e m2) + + | step_external_function: forall id targs tres vargs k m vres t, + event_match (external_function id targs tres) vargs t vres -> + step (Callstate (External id targs tres) vargs k m) + t (Returnstate vres k m) + + | step_returnstate_0: forall v f e k m, + step (Returnstate v (Kcall None f e k) m) + E0 (State f Sskip k e m) + + | step_returnstate_1: forall v f e k m m' loc ofs ty, + store_value_of_type ty m loc ofs v = Some m' -> + step (Returnstate v (Kcall (Some(loc, ofs, ty)) f e k) m) + E0 (State f Sskip k e m'). + +(** * Alternate big-step semantics *) + +(** ** Big-step semantics for terminating statements and functions *) + +(** The execution of a statement produces an ``outcome'', indicating + how the execution terminated: either normally or prematurely + through the execution of a [break], [continue] or [return] statement. *) + +Inductive outcome: Type := + | Out_break: outcome (**r terminated by [break] *) + | Out_continue: outcome (**r terminated by [continue] *) + | Out_normal: outcome (**r terminated normally *) + | Out_return: option val -> outcome. (**r terminated by [return] *) + +Inductive out_normal_or_continue : outcome -> Prop := + | Out_normal_or_continue_N: out_normal_or_continue Out_normal + | Out_normal_or_continue_C: out_normal_or_continue Out_continue. + +Inductive out_break_or_return : outcome -> outcome -> Prop := + | Out_break_or_return_B: out_break_or_return Out_break Out_normal + | Out_break_or_return_R: forall ov, + out_break_or_return (Out_return ov) (Out_return ov). + +Definition outcome_switch (out: outcome) : outcome := + match out with + | Out_break => Out_normal + | o => o + end. + +Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := + match out, t with + | Out_normal, Tvoid => v = Vundef + | Out_return None, Tvoid => v = Vundef + | Out_return (Some v'), ty => ty <> Tvoid /\ v'=v + | _, _ => False + end. + (** [exec_stmt ge e m1 s t m2 out] describes the execution of the statement [s]. [out] is the outcome for this execution. [m1] is the initial memory state, [m2] the final memory state. @@ -778,44 +1075,29 @@ Inductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop (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 (seq_of_labeled_statement (select_switch n sl)) t m1 out -> exec_stmt e m (Sswitch a sl) 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 - statements [ls]. *) - -with exec_lblstmts: env -> mem -> labeled_statements -> trace -> mem -> outcome -> Prop := - | exec_LSdefault: forall e m s t m1 out, - exec_stmt e m s t m1 out -> - exec_lblstmts e m (LSdefault s) t m1 out - | exec_LScase_fallthrough: forall e m n s ls t1 m1 t2 m2 out, - exec_stmt e m s t1 m1 Out_normal -> - exec_lblstmts e m1 ls t2 m2 out -> - exec_lblstmts e m (LScase n s ls) (t1 ** t2) m2 out - | exec_LScase_stop: forall e m n s ls t m1 out, - exec_stmt e m s t m1 out -> out <> Out_normal -> - exec_lblstmts e m (LScase n s ls) t m1 out - (** [eval_funcall m1 fd args t m2 res] describes the invocation of function [fd] with arguments [args]. [res] is the value returned by the call. *) with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := - | eval_funcall_internal: forall m f vargs t e m1 lb m2 m3 out vres, - alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 lb -> + | eval_funcall_internal: forall m f vargs t e m1 m2 m3 out vres, + alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> bind_parameters e m1 f.(fn_params) vargs m2 -> exec_stmt e m2 f.(fn_body) t m3 out -> outcome_result_value out f.(fn_return) vres -> - eval_funcall m (Internal f) vargs t (Mem.free_list m3 lb) vres + eval_funcall m (Internal f) vargs t (Mem.free_list m3 (blocks_of_env e)) vres | eval_funcall_external: forall m id targs tres vargs t vres, event_match (external_function id targs tres) vargs t vres -> eval_funcall m (External id targs tres) vargs t m vres. -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. +Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop + with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop. + +(** ** Big-step semantics for diverging statements and functions *) (** Coinductive semantics for divergence. [execinf_stmt ge e m s t] holds if the execution of statement [s] @@ -823,13 +1105,21 @@ Scheme exec_stmt_ind3 := Minimality for exec_stmt Sort Prop 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, + | execinf_Scall_none: forall e m 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 None a al) t + | execinf_Scall_some: forall e m lhs a al loc ofs vf vargs f t, + 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 -> evalinf_funcall m f vargs t -> - execinf_stmt e m (Scall lhs a al) t + execinf_stmt e m (Scall (Some 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 @@ -899,51 +1189,538 @@ CoInductive execinf_stmt: env -> mem -> statement -> traceinf -> Prop := 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 (seq_of_labeled_statement (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 -> + | evalinf_funcall_internal: forall m f vargs t e m1 m2, + alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> 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. +End SEMANTICS. + +(** * Whole-program semantics *) -(** Execution of a whole program. [exec_program p beh] holds +(** Execution of whole programs are described as sequences of transitions + from an initial state to a final state. An initial state is a [Callstate] + corresponding to the invocation of the ``main'' function of the program + without arguments and with an empty continuation. *) + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b f, + 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 -> + initial_state p (Callstate f nil Kstop m0). + +(** A final state is a [Returnstate] with an empty continuation. *) + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall r m, + final_state (Returnstate (Vint r) Kstop m) 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] has [beh] as observable + behavior. *) + +Definition exec_program (p: program) (beh: program_behavior) : Prop := + program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. + +(** Big-step execution of a whole program. + [exec_program_bigstep 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 := +Inductive exec_program_bigstep (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) + exec_program_bigstep 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). - + exec_program_bigstep p (Diverges t). + +(** * Implication from big-step semantics to transition semantics *) + +Section BIGSTEP_TO_TRANSITIONS. + +Variable prog: program. +Let ge : genv := Genv.globalenv prog. + +Definition exec_stmt_eval_funcall_ind + (PS: env -> mem -> statement -> trace -> mem -> outcome -> Prop) + (PF: mem -> fundef -> list val -> trace -> mem -> val -> Prop) := + fun a b c d e f g h i j k l m n o p q r s t u v w x y => + conj (exec_stmt_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y) + (eval_funcall_ind2 ge PS PF a b c d e f g h i j k l m n o p q r s t u v w x y). + +Inductive outcome_state_match + (e: env) (m: mem) (f: function) (k: cont): outcome -> state -> Prop := + | osm_normal: + outcome_state_match e m f k Out_normal (State f Sskip k e m) + | osm_break: + outcome_state_match e m f k Out_break (State f Sbreak k e m) + | osm_continue: + outcome_state_match e m f k Out_continue (State f Scontinue k e m) + | osm_return_none: forall k', + call_cont k' = call_cont k -> + outcome_state_match e m f k + (Out_return None) (State f (Sreturn None) k' e m) + | osm_return_some: forall a v k', + call_cont k' = call_cont k -> + eval_expr ge e m a v -> + outcome_state_match e m f k + (Out_return (Some v)) (State f (Sreturn (Some a)) k' e m). + +Lemma is_call_cont_call_cont: + forall k, is_call_cont k -> call_cont k = k. +Proof. + destruct k; simpl; intros; contradiction || auto. +Qed. + +Lemma exec_stmt_eval_funcall_steps: + (forall e m s t m' out, + exec_stmt ge e m s t m' out -> + forall f k, exists S, + star step ge (State f s k e m) t S + /\ outcome_state_match e m' f k out S) +/\ + (forall m fd args t m' res, + eval_funcall ge m fd args t m' res -> + forall k, + is_call_cont k -> + star step ge (Callstate fd args k m) t (Returnstate res k m')). +Proof. + apply exec_stmt_eval_funcall_ind; intros. + +(* skip *) + econstructor; split. apply star_refl. constructor. + +(* assign *) + econstructor; split. apply star_one. econstructor; eauto. constructor. + +(* call none *) + econstructor; split. + eapply star_left. econstructor; eauto. + eapply star_right. apply H4. simpl; auto. econstructor. reflexivity. traceEq. + constructor. + +(* call some *) + econstructor; split. + eapply star_left. econstructor; eauto. + eapply star_right. apply H5. simpl; auto. econstructor; eauto. reflexivity. traceEq. + constructor. + +(* sequence 2 *) + destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. inv B1. + destruct (H2 f k) as [S2 [A2 B2]]. + econstructor; split. + eapply star_left. econstructor. + eapply star_trans. eexact A1. + eapply star_left. constructor. eexact A2. + reflexivity. reflexivity. traceEq. + auto. + +(* sequence 1 *) + destruct (H0 f (Kseq s2 k)) as [S1 [A1 B1]]. + set (S2 := + match out with + | Out_break => State f Sbreak k e m1 + | Out_continue => State f Scontinue k e m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. econstructor. + eapply star_trans. eexact A1. + unfold S2; inv B1. + congruence. + apply star_one. apply step_break_seq. + apply star_one. apply step_continue_seq. + apply star_refl. + apply star_refl. + reflexivity. traceEq. + unfold S2; inv B1; congruence || econstructor; eauto. + +(* ifthenelse true *) + destruct (H2 f k) as [S1 [A1 B1]]. + exists S1; split. + eapply star_left. eapply step_ifthenelse_true; eauto. eexact A1. traceEq. + auto. + +(* ifthenelse false *) + destruct (H2 f k) as [S1 [A1 B1]]. + exists S1; split. + eapply star_left. eapply step_ifthenelse_false; eauto. eexact A1. traceEq. + auto. + +(* return none *) + econstructor; split. apply star_refl. constructor. auto. + +(* return some *) + econstructor; split. apply star_refl. econstructor; eauto. + +(* break *) + econstructor; split. apply star_refl. constructor. + +(* continue *) + econstructor; split. apply star_refl. constructor. + +(* while false *) + econstructor; split. + apply star_one. eapply step_while_false; eauto. + constructor. + +(* while stop *) + destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]]. + set (S2 := + match out' with + | Out_break => State f Sskip k e m' + | _ => S1 + end). + exists S2; split. + eapply star_left. eapply step_while_true; eauto. + eapply star_trans. eexact A1. + unfold S2. inversion H3; subst. + inv B1. apply star_one. constructor. + apply star_refl. + reflexivity. traceEq. + unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto. + +(* while loop *) + destruct (H2 f (Kwhile a s k)) as [S1 [A1 B1]]. + destruct (H5 f k) as [S2 [A2 B2]]. + exists S2; split. + eapply star_left. eapply step_while_true; eauto. + eapply star_trans. eexact A1. + eapply star_left. + inv H3; inv B1; apply step_skip_or_continue_while; auto. + eexact A2. + reflexivity. reflexivity. traceEq. + auto. + +(* dowhile false *) + destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. + exists (State f Sskip k e m1); split. + eapply star_left. constructor. + eapply star_right. eexact A1. + inv H1; inv B1; eapply step_skip_or_continue_dowhile_false; eauto. + reflexivity. traceEq. + constructor. + +(* dowhile stop *) + destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. + set (S2 := + match out1 with + | Out_break => State f Sskip k e m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. apply step_dowhile. + eapply star_trans. eexact A1. + unfold S2. inversion H1; subst. + inv B1. apply star_one. constructor. + apply star_refl. + reflexivity. traceEq. + unfold S2. inversion H1; subst. constructor. inv B1; econstructor; eauto. + +(* dowhile loop *) + destruct (H0 f (Kdowhile a s k)) as [S1 [A1 B1]]. + destruct (H5 f k) as [S2 [A2 B2]]. + exists S2; split. + eapply star_left. apply step_dowhile. + eapply star_trans. eexact A1. + eapply star_left. + inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto. + eexact A2. + reflexivity. reflexivity. traceEq. + auto. + +(* for start *) + destruct (H1 f (Kseq (Sfor Sskip a2 a3 s) k)) as [S1 [A1 B1]]. inv B1. + destruct (H3 f k) as [S2 [A2 B2]]. + exists S2; split. + eapply star_left. apply step_for_start; auto. + eapply star_trans. eexact A1. + eapply star_left. constructor. eexact A2. + reflexivity. reflexivity. traceEq. + auto. + +(* for false *) + econstructor; split. + eapply star_one. eapply step_for_false; eauto. + constructor. + +(* for stop *) + destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]]. + set (S2 := + match out1 with + | Out_break => State f Sskip k e m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. eapply step_for_true; eauto. + eapply star_trans. eexact A1. + unfold S2. inversion H3; subst. + inv B1. apply star_one. constructor. + apply star_refl. + reflexivity. traceEq. + unfold S2. inversion H3; subst. constructor. inv B1; econstructor; eauto. + +(* for loop *) + destruct (H2 f (Kfor2 a2 a3 s k)) as [S1 [A1 B1]]. + destruct (H5 f (Kfor3 a2 a3 s k)) as [S2 [A2 B2]]. inv B2. + destruct (H7 f k) as [S3 [A3 B3]]. + exists S3; split. + eapply star_left. eapply step_for_true; eauto. + eapply star_trans. eexact A1. + eapply star_trans with (s2 := State f a3 (Kfor3 a2 a3 s k) e m1). + inv H3; inv B1. + apply star_one. constructor. auto. + apply star_one. constructor. auto. + eapply star_trans. eexact A2. + eapply star_left. constructor. + eexact A3. + reflexivity. reflexivity. reflexivity. reflexivity. traceEq. + auto. + +(* switch *) + destruct (H1 f (Kswitch k)) as [S1 [A1 B1]]. + set (S2 := + match out with + | Out_normal => State f Sskip k e m1 + | Out_break => State f Sskip k e m1 + | Out_continue => State f Scontinue k e m1 + | _ => S1 + end). + exists S2; split. + eapply star_left. eapply step_switch; eauto. + eapply star_trans. eexact A1. + unfold S2; inv B1. + apply star_one. constructor. auto. + apply star_one. constructor. auto. + apply star_one. constructor. + apply star_refl. + apply star_refl. + reflexivity. traceEq. + unfold S2. inv B1; simpl; econstructor; eauto. + +(* call internal *) + destruct (H2 f k) as [S1 [A1 B1]]. + eapply star_left. eapply step_internal_function; eauto. + eapply star_right. eexact A1. + inv B1; simpl in H3; try contradiction. + (* Out_normal *) + assert (fn_return f = Tvoid /\ vres = Vundef). + destruct (fn_return f); auto || contradiction. + destruct H5. subst vres. apply step_skip_call; auto. + (* Out_return None *) + assert (fn_return f = Tvoid /\ vres = Vundef). + destruct (fn_return f); auto || contradiction. + destruct H6. subst vres. + rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. + apply step_return_0; auto. + (* Out_return Some *) + destruct H3. subst vres. + rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. + eapply step_return_1; eauto. + reflexivity. traceEq. + +(* call external *) + apply star_one. apply step_external_function; auto. +Qed. + +Lemma exec_stmt_steps: + forall e m s t m' out, + exec_stmt ge e m s t m' out -> + forall f k, exists S, + star step ge (State f s k e m) t S + /\ outcome_state_match e m' f k out S. +Proof (proj1 exec_stmt_eval_funcall_steps). + +Lemma eval_funcall_steps: + forall m fd args t m' res, + eval_funcall ge m fd args t m' res -> + forall k, + is_call_cont k -> + star step ge (Callstate fd args k m) t (Returnstate res k m'). +Proof (proj2 exec_stmt_eval_funcall_steps). + +Definition order (x y: unit) := False. + +Lemma evalinf_funcall_forever: + forall m fd args T k, + evalinf_funcall ge m fd args T -> + forever_N step order ge tt (Callstate fd args k m) T. +Proof. + cofix CIH_FUN. + assert (forall e m s T f k, + execinf_stmt ge e m s T -> + forever_N step order ge tt (State f s k e m) T). + cofix CIH_STMT. + intros. inv H. + +(* call none *) + eapply forever_N_plus. + apply plus_one. eapply step_call_none; eauto. + apply CIH_FUN. eauto. traceEq. +(* call some *) + eapply forever_N_plus. + apply plus_one. eapply step_call_some; eauto. + apply CIH_FUN. eauto. traceEq. + +(* seq 1 *) + eapply forever_N_plus. + apply plus_one. econstructor. + apply CIH_STMT; eauto. traceEq. +(* seq 2 *) + destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kseq s2 k)) as [S1 [A1 B1]]. + inv B1. + eapply forever_N_plus. + eapply plus_left. constructor. eapply star_trans. eexact A1. + apply star_one. constructor. reflexivity. reflexivity. + apply CIH_STMT; eauto. traceEq. + +(* ifthenelse true *) + eapply forever_N_plus. + apply plus_one. eapply step_ifthenelse_true; eauto. + apply CIH_STMT; eauto. traceEq. +(* ifthenelse false *) + eapply forever_N_plus. + apply plus_one. eapply step_ifthenelse_false; eauto. + apply CIH_STMT; eauto. traceEq. + +(* while body *) + eapply forever_N_plus. + eapply plus_one. eapply step_while_true; eauto. + apply CIH_STMT; eauto. traceEq. +(* while loop *) + destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kwhile a s0 k)) as [S1 [A1 B1]]. + eapply forever_N_plus with (s2 := State f (Swhile a s0) k e m1). + eapply plus_left. eapply step_while_true; eauto. + eapply star_right. eexact A1. + inv H3; inv B1; apply step_skip_or_continue_while; auto. + reflexivity. reflexivity. + apply CIH_STMT; eauto. traceEq. + +(* dowhile body *) + eapply forever_N_plus. + eapply plus_one. eapply step_dowhile. + apply CIH_STMT; eauto. + traceEq. + +(* dowhile loop *) + destruct (exec_stmt_steps _ _ _ _ _ _ H0 f (Kdowhile a s0 k)) as [S1 [A1 B1]]. + eapply forever_N_plus with (s2 := State f (Sdowhile a s0) k e m1). + eapply plus_left. eapply step_dowhile. + eapply star_right. eexact A1. + inv H1; inv B1; eapply step_skip_or_continue_dowhile_true; eauto. + reflexivity. reflexivity. + apply CIH_STMT. eauto. + traceEq. + +(* for start 1 *) + assert (a1 <> Sskip). red; intros; subst. inv H0. + eapply forever_N_plus. + eapply plus_one. apply step_for_start; auto. + apply CIH_STMT; eauto. + traceEq. + +(* for start 2 *) + destruct (exec_stmt_steps _ _ _ _ _ _ H1 f (Kseq (Sfor Sskip a2 a3 s0) k)) as [S1 [A1 B1]]. + inv B1. + eapply forever_N_plus. + eapply plus_left. eapply step_for_start; eauto. + eapply star_right. eexact A1. + apply step_skip_seq. + reflexivity. reflexivity. + apply CIH_STMT; eauto. + traceEq. + +(* for body *) + eapply forever_N_plus. + apply plus_one. eapply step_for_true; eauto. + apply CIH_STMT; eauto. + traceEq. + +(* for next *) + destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]]. + eapply forever_N_plus. + eapply plus_left. eapply step_for_true; eauto. + eapply star_trans. eexact A1. + apply star_one. + inv H3; inv B1; apply step_skip_or_continue_for2; auto. + reflexivity. reflexivity. + apply CIH_STMT; eauto. + traceEq. + +(* for body *) + destruct (exec_stmt_steps _ _ _ _ _ _ H2 f (Kfor2 a2 a3 s0 k)) as [S1 [A1 B1]]. + destruct (exec_stmt_steps _ _ _ _ _ _ H4 f (Kfor3 a2 a3 s0 k)) as [S2 [A2 B2]]. + inv B2. + eapply forever_N_plus. + eapply plus_left. eapply step_for_true; eauto. + eapply star_trans. eexact A1. + eapply star_left. inv H3; inv B1; apply step_skip_or_continue_for2; auto. + eapply star_right. eexact A2. + constructor. + reflexivity. reflexivity. reflexivity. reflexivity. + apply CIH_STMT; eauto. + traceEq. + +(* switch *) + eapply forever_N_plus. + eapply plus_one. eapply step_switch; eauto. + apply CIH_STMT; eauto. + traceEq. + +(* call internal *) + intros. inv H0. + eapply forever_N_plus. + eapply plus_one. econstructor; eauto. + apply H; eauto. + traceEq. +Qed. + +(* +Theorem exec_program_bigstep_transition: + forall beh, + exec_program_bigstep prog beh -> + exec_program prog beh. +Proof. + intros. inv H. + (* termination *) + econstructor. + econstructor. eauto. eauto. + apply eval_funcall_steps. eauto. red; auto. + econstructor. + (* divergence *) + econstructor. + econstructor. eauto. eauto. + eapply forever_N_forever with (order := order). + red; intros. constructor; intros. red in H. elim H. + apply evalinf_funcall_forever. auto. +Qed. +*) + +End BIGSTEP_TO_TRANSITIONS. + + + + + + diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 942cfd7..5cdbd84 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -59,6 +59,8 @@ Inductive expr : Type := [Sexit n] terminates prematurely the execution of the [n+1] enclosing [Sblock] statements. *) +Definition label := ident. + Inductive stmt : Type := | Sskip: stmt | Sassign : ident -> expr -> stmt @@ -69,8 +71,14 @@ Inductive stmt : Type := | Sloop: stmt -> stmt | Sblock: stmt -> stmt | Sexit: nat -> stmt - | Sswitch: expr -> list (int * nat) -> nat -> stmt - | Sreturn: option expr -> stmt. + | Sswitch: expr -> lbl_stmt -> stmt + | Sreturn: option expr -> stmt + | Slabel: label -> stmt -> stmt + | Sgoto: label -> stmt + +with lbl_stmt : Type := + | LSdefault: stmt -> lbl_stmt + | LScase: int -> stmt -> lbl_stmt -> lbl_stmt. (** The variables can be either scalar variables (whose type, size and signedness are given by a [memory_chunk] @@ -105,39 +113,6 @@ Definition funsig (fd: fundef) := (** * Operational semantics *) -(** The operational semantics for Csharpminor is given in big-step operational - style. Expressions evaluate to values, and statements evaluate to - ``outcomes'' indicating how execution should proceed afterwards. *) - -Inductive outcome: Type := - | Out_normal: outcome (**r continue in sequence *) - | Out_exit: nat -> outcome (**r terminate [n+1] enclosing blocks *) - | Out_return: option val -> outcome. (**r return immediately to caller *) - -Definition outcome_result_value - (out: outcome) (ot: option typ) (v: val) : Prop := - match out, ot with - | Out_normal, None => v = Vundef - | Out_return None, None => v = Vundef - | Out_return (Some v'), Some ty => v = v' - | _, _ => False - end. - -Definition outcome_block (out: outcome) : outcome := - match out with - | Out_normal => Out_normal - | Out_exit O => Out_normal - | Out_exit (S n) => Out_exit n - | Out_return optv => Out_return optv - end. - -Fixpoint switch_target (n: int) (dfl: nat) (cases: list (int * nat)) - {struct cases} : nat := - match cases with - | nil => dfl - | (n1, lbl1) :: rem => if Int.eq n n1 then lbl1 else switch_target n dfl rem - end. - (** Three kinds of evaluation environments are involved: - [genv]: global environments, define symbols and functions; - [gvarenv]: map global variables to variable informations (type [var_kind]); @@ -167,10 +142,105 @@ Definition fn_params_names (f: function) := Definition fn_vars_names (f: function) := List.map (@fst ident var_kind) f.(fn_vars). -Definition global_var_env (p: program): gvarenv := - List.fold_left - (fun gve x => match x with (id, init, k) => PTree.set id k gve end) - p.(prog_vars) (PTree.empty var_kind). +(** Continuations *) + +Inductive cont: Type := + | Kstop: cont (**r stop program execution *) + | Kseq: stmt -> cont -> cont (**r execute stmt, then cont *) + | Kblock: cont -> cont (**r exit a block, then do cont *) + | Kcall: option ident -> function -> env -> cont -> cont. + (**r return to caller *) + +(** States *) + +Inductive state: Type := + | State: (**r Execution within a function *) + forall (f: function) (**r currently executing function *) + (s: stmt) (**r statement under consideration *) + (k: cont) (**r its continuation -- what to do next *) + (e: env) (**r current local environment *) + (m: mem), (**r current memory state *) + state + | Callstate: (**r Invocation of a function *) + forall (f: fundef) (**r function to invoke *) + (args: list val) (**r arguments provided by caller *) + (k: cont) (**r what to do next *) + (m: mem), (**r memory state *) + state + | Returnstate: (**r Return from a function *) + forall (v: val) (**r Return value *) + (k: cont) (**r what to do next *) + (m: mem), (**r memory state *) + state. + +(** Pop continuation until a call or stop *) + +Fixpoint call_cont (k: cont) : cont := + match k with + | Kseq s k => call_cont k + | Kblock k => call_cont k + | _ => k + end. + +Definition is_call_cont (k: cont) : Prop := + match k with + | Kstop => True + | Kcall _ _ _ _ => True + | _ => False + end. + +(** Resolve [switch] statements. *) + +Fixpoint select_switch (n: int) (sl: lbl_stmt) {struct sl} : lbl_stmt := + match sl with + | LSdefault _ => sl + | LScase c s sl' => if Int.eq c n then sl else select_switch n sl' + end. + +Fixpoint seq_of_lbl_stmt (sl: lbl_stmt) : stmt := + match sl with + | LSdefault s => s + | LScase c s sl' => Sseq s (seq_of_lbl_stmt sl') + end. + +(** Find the statement and manufacture the continuation + corresponding to a label *) + +Fixpoint find_label (lbl: label) (s: stmt) (k: cont) + {struct s}: option (stmt * cont) := + match s with + | Sseq s1 s2 => + match find_label lbl s1 (Kseq s2 k) with + | Some sk => Some sk + | None => find_label lbl s2 k + end + | Sifthenelse a s1 s2 => + match find_label lbl s1 k with + | Some sk => Some sk + | None => find_label lbl s2 k + end + | Sloop s1 => + find_label lbl s1 (Kseq (Sloop s1) k) + | Sblock s1 => + find_label lbl s1 (Kblock k) + | Sswitch a sl => + find_label_ls lbl sl k + | Slabel lbl' s' => + if ident_eq lbl lbl' then Some(s', k) else find_label lbl s' k + | _ => None + end + +with find_label_ls (lbl: label) (sl: lbl_stmt) (k: cont) + {struct sl}: option (stmt * cont) := + match sl with + | LSdefault s => find_label lbl s k + | LScase _ s sl' => + match find_label lbl s (Kseq (seq_of_lbl_stmt sl') k) with + | Some sk => Some sk + | None => find_label_ls lbl sl' k + end + end. + (** Evaluation of operator applications. *) @@ -199,15 +269,21 @@ Definition eval_binop (op: binary_operation) Inductive alloc_variables: env -> mem -> list (ident * var_kind) -> - env -> mem -> list block -> Prop := + env -> mem -> Prop := | alloc_variables_nil: forall e m, - alloc_variables e m nil e m nil + alloc_variables e m nil e m | alloc_variables_cons: - forall e m id lv vars m1 b1 m2 e2 lb, + forall e m id lv vars m1 b1 m2 e2, Mem.alloc m 0 (sizeof lv) = (m1, b1) -> - alloc_variables (PTree.set id (b1, lv) e) m1 vars e2 m2 lb -> - alloc_variables e m ((id, lv) :: vars) e2 m2 (b1 :: lb). + alloc_variables (PTree.set id (b1, lv) e) m1 vars e2 m2 -> + alloc_variables e m ((id, lv) :: vars) e2 m2. + +(** List of blocks mentioned in an environment *) + +Definition blocks_of_env (e: env) : list block := + List.map (fun id_b_lv => match id_b_lv with (id, (b, lv)) => b end) + (PTree.elements e). (** Initialization of local variables that are parameters. The value of the corresponding argument is stored into the memory block @@ -228,8 +304,9 @@ Inductive bind_parameters: env -> Section RELSEM. -Variable prg: program. -Let ge := Genv.globalenv prg. +Variable globenv : genv * gvarenv. +Let ge := fst globenv. +Let gvare := snd globenv. (* Evaluation of the address of a variable: [eval_var_addr prg ge e id b] states that variable [id] @@ -260,7 +337,7 @@ Inductive eval_var_ref: env -> ident -> block -> memory_chunk -> Prop := forall e id b chunk, PTree.get id e = None -> Genv.find_symbol ge id = Some b -> - PTree.get id (global_var_env prg) = Some (Vscalar chunk) -> + PTree.get id gvare = Some (Vscalar chunk) -> eval_var_ref e id b chunk. (** Evaluation of an expression: [eval_expr prg e m a v] states @@ -331,256 +408,148 @@ Inductive exec_opt_assign: env -> mem -> option ident -> val -> mem -> Prop := 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']. - [t] is the trace of observable events performed during the call. *) +(** One step of execution *) -Inductive eval_funcall: - mem -> fundef -> list val -> trace -> - mem -> val -> Prop := - | eval_funcall_internal: - forall m f vargs e m1 lb m2 t m3 out vres, - 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 -> - exec_stmt e m2 f.(fn_body) t m3 out -> - outcome_result_value out f.(fn_sig).(sig_res) vres -> - eval_funcall m (Internal f) vargs t (Mem.free_list m3 lb) vres - | eval_funcall_external: - forall m ef vargs t vres, - event_match ef vargs t vres -> - eval_funcall m (External ef) vargs t m vres - -(** 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: - env -> - mem -> stmt -> trace -> - mem -> outcome -> Prop := - | exec_Sskip: - forall e m, - exec_stmt e m Sskip E0 m Out_normal - | exec_Sassign: - forall e m id a v m', +Inductive step: state -> trace -> state -> Prop := + + | step_skip_seq: forall f s k e m, + step (State f Sskip (Kseq s k) e m) + E0 (State f s k e m) + | step_skip_block: forall f k e m, + step (State f Sskip (Kblock k) e m) + E0 (State f Sskip k e m) + | step_skip_call: forall f k e m, + is_call_cont k -> + f.(fn_sig).(sig_res) = None -> + step (State f Sskip k e m) + E0 (Returnstate Vundef k (Mem.free_list m (blocks_of_env e))) + + | step_assign: forall f id a k e m m' v, 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, + step (State f (Sassign id a) k e m) + E0 (State f Sskip k e m') + + | step_store: forall f chunk addr a k e m vaddr v m', + eval_expr e m addr vaddr -> + eval_expr e m a v -> + Mem.storev chunk m vaddr v = Some m' -> + step (State f (Sstore chunk addr a) k e m) + E0 (State f Sskip k e m') + + | step_call: forall f optid sig a bl k e m vf vargs fd, 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 -> - exec_stmt e m1 s2 t2 m2 out -> - t = t1 ** t2 -> - exec_stmt e m (Sseq s1 s2) t m2 out - | exec_Sseq_stop: - forall e m s1 s2 t1 m1 out, - exec_stmt e m s1 t1 m1 out -> - out <> Out_normal -> - exec_stmt e m (Sseq s1 s2) t1 m1 out - | exec_Sifthenelse: - forall e m a sl1 sl2 v vb t m' out, + Genv.find_funct ge vf = Some fd -> + funsig fd = sig -> + step (State f (Scall optid sig a bl) k e m) + E0 (Callstate fd vargs (Kcall optid f e k) m) + + | step_seq: forall f s1 s2 k e m, + step (State f (Sseq s1 s2) k e m) + E0 (State f s1 (Kseq s2 k) e m) + + | step_ifthenelse: forall f a s1 s2 k e m v b, 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 -> - exec_stmt e m1 (Sloop sl) t2 m2 out -> - t = t1 ** t2 -> - exec_stmt e m (Sloop sl) t m2 out - | exec_Sloop_stop: - forall e m sl t1 m1 out, - exec_stmt e m sl t1 m1 out -> - out <> Out_normal -> - exec_stmt e m (Sloop sl) t1 m1 out - | exec_Sblock: - forall e m sl t1 m1 out, - exec_stmt e m sl t1 m1 out -> - exec_stmt e m (Sblock sl) t1 m1 (outcome_block out) - | exec_Sexit: - forall e m n, - exec_stmt e m (Sexit n) E0 m (Out_exit n) - | exec_Sswitch: - forall e m a cases default n, + Val.bool_of_val v b -> + step (State f (Sifthenelse a s1 s2) k e m) + E0 (State f (if b then s1 else s2) k e m) + + | step_loop: forall f s k e m, + step (State f (Sloop s) k e m) + E0 (State f s (Kseq (Sloop s) k) e m) + + | step_block: forall f s k e m, + step (State f (Sblock s) k e m) + E0 (State f s (Kblock k) e m) + + | step_exit_seq: forall f n s k e m, + step (State f (Sexit n) (Kseq s k) e m) + E0 (State f (Sexit n) k e m) + | step_exit_block_0: forall f k e m, + step (State f (Sexit O) (Kblock k) e m) + E0 (State f Sskip k e m) + | step_exit_block_S: forall f n k e m, + step (State f (Sexit (S n)) (Kblock k) e m) + E0 (State f (Sexit n) k e m) + + | step_switch: forall f a cases k e m n, eval_expr e m a (Vint n) -> - exec_stmt e m (Sswitch a cases default) - 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 v, + step (State f (Sswitch a cases) k e m) + E0 (State f (seq_of_lbl_stmt (select_switch n cases)) k e m) + + | step_return_0: forall f k e m, + f.(fn_sig).(sig_res) = None -> + step (State f (Sreturn None) k e m) + E0 (Returnstate Vundef (call_cont k) + (Mem.free_list m (blocks_of_env e))) + | step_return_1: forall f a k e m v, + f.(fn_sig).(sig_res) <> None -> 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, + step (State f (Sreturn (Some a)) k e m) + E0 (Returnstate v (call_cont k) + (Mem.free_list m (blocks_of_env e))) + + | step_label: forall f lbl s k e m, + step (State f (Slabel lbl s) k e m) + E0 (State f s k e m) + + | step_goto: forall f lbl k e m s' k', + find_label lbl f.(fn_body) (call_cont k) = Some(s', k') -> + step (State f (Sgoto lbl) k e m) + E0 (State f s' k' e m) + + | step_internal_function: forall f vargs k m m1 m2 e, list_norepet (fn_params_names f ++ fn_vars_names f) -> - alloc_variables empty_env m (fn_variables f) e m1 lb -> + alloc_variables empty_env m (fn_variables f) e m1 -> bind_parameters e m1 f.(fn_params) vargs m2 -> - execinf_stmt e m2 f.(fn_body) t -> - evalinf_funcall m (Internal f) vargs t + step (Callstate (Internal f) vargs k m) + E0 (State f f.(fn_body) k e m2) -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. + | step_external_function: forall ef vargs k m t vres, + event_match ef vargs t vres -> + step (Callstate (External ef) vargs k m) + t (Returnstate vres k m) + + | step_return: forall v optid f e k m m', + exec_opt_assign e m optid v m' -> + step (Returnstate v (Kcall optid f e k) m) + E0 (State f Sskip k e m'). End RELSEM. -(** 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] has [beh] as observable - behavior. *) +(** Execution of whole programs are described as sequences of transitions + from an initial state to a final state. An initial state is a [Callstate] + corresponding to the invocation of the ``main'' function of the program + without arguments and with an empty continuation. *) -Inductive exec_program (p: program): program_behavior -> Prop := - | program_terminates: - forall b f t m r, +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall b f, 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). + initial_state p (Callstate f nil Kstop m0). + +(** A final state is a [Returnstate] with an empty continuation. *) + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall r m, + final_state (Returnstate (Vint r) Kstop m) 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] has [beh] as observable + behavior. *) + +Definition global_var_env (p: program): gvarenv := + List.fold_left + (fun gve x => match x with (id, init, k) => PTree.set id k gve end) + p.(prog_vars) (PTree.empty var_kind). + +Definition exec_program (p: program) (beh: program_behavior) : Prop := + program_behaves step (initial_state p) final_state + (Genv.globalenv p, global_var_env p) beh. + + diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 64a58ad..55860ef 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -508,27 +508,9 @@ for (e1;e2;e3) s; ---> e1; } } // break in s branches here ->> - For [switch] statements, we wrap the statements associated with - the various cases in a cascade of nested Csharpminor blocks. - The multi-way branch is performed by a Csharpminor [switch] - statement that exits to the appropriate case. For instance: -<< -switch (e) { ---> block { block { block { block { - case N1: s1; switch (e) { N1: exit 0; N2: exit 1; default: exit 2; } - case N2: s2; } ; s1 // with break -> exit 2 and continue -> exit 3 - default: s; } ; s2 // with break -> exit 1 and continue -> exit 2 -} } ; s // with break -> exit 0 and continue -> exit 1 - } >> *) -Fixpoint switch_table (sl: labeled_statements) (k: nat) {struct sl} : list (int * nat) := - match sl with - | LSdefault _ => nil - | 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. @@ -596,22 +578,27 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : r OK (Sreturn (Some te)) | Csyntax.Sreturn None => OK (Sreturn None) - | Csyntax.Sswitch e sl => - let cases := switch_table sl 0 in - let ncases := List.length cases in - do te <- transl_expr e; - transl_lblstmts ncases (ncnt + ncases + 1)%nat sl (Sblock (Sswitch te cases ncases)) + | Csyntax.Sswitch a sl => + do ta <- transl_expr a; + do tsl <- transl_lbl_stmt 0%nat (S ncnt) sl; + OK (Sblock (Sswitch ta tsl)) + | Csyntax.Slabel lbl s => + do ts <- transl_statement nbrk ncnt s; + OK (Slabel lbl ts) + | Csyntax.Sgoto lbl => + OK (Sgoto lbl) end -with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt) - {struct sl}: res stmt := +with transl_lbl_stmt (nbrk ncnt: nat) (sl: Csyntax.labeled_statements) + {struct sl}: res lbl_stmt := match sl with - | LSdefault s => + | Csyntax.LSdefault s => do ts <- transl_statement nbrk ncnt s; - OK (Sblock (Sseq body ts)) - | LScase _ s rem => + OK (LSdefault ts) + | Csyntax.LScase n s sl' => do ts <- transl_statement nbrk ncnt s; - transl_lblstmts (pred nbrk) (pred ncnt) rem (Sblock (Sseq body ts)) + do tsl' <- transl_lbl_stmt nbrk ncnt sl'; + OK (LScase n ts tsl') end. (*** Translation of functions *) diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v index bd9cf22..86ecd2a 100644 --- a/cfrontend/Cshmgenproof1.v +++ b/cfrontend/Cshmgenproof1.v @@ -206,86 +206,60 @@ Proof. 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 ts2. +Lemma is_Sskip_true: + forall (A: Type) (a b: A), + (if is_Sskip Csyntax.Sskip then a else b) = a. Proof. - 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. + intros. destruct (is_Sskip Csyntax.Sskip); congruence. Qed. -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))))). +Lemma is_Sskip_false: + forall (A: Type) (a b: A) s, + s <> Csyntax.Sskip -> + (if is_Sskip s then a else b) = b. Proof. - intros. simpl. destruct (is_Sskip Csyntax.Sskip). auto. congruence. + intros. destruct (is_Sskip s); congruence. Qed. -(** Properties related to switch constructs *) - -Fixpoint lblstmts_length (sl: labeled_statements) : nat := - match sl with - | LSdefault _ => 0%nat - | LScase _ _ sl' => S (lblstmts_length sl') - end. +(** Properties of labeled statements *) -Lemma switch_target_table_shift: - forall n sl base dfl, - switch_target n (S dfl) (switch_table sl (S base)) = - S(switch_target n dfl (switch_table sl base)). +Lemma transl_lbl_stmt_1: + forall nbrk ncnt n sl tsl, + transl_lbl_stmt nbrk ncnt sl = OK tsl -> + transl_lbl_stmt nbrk ncnt (Csem.select_switch n sl) = OK (select_switch n tsl). Proof. - induction sl; intros; simpl. - auto. - case (Int.eq n i). auto. auto. + induction sl; intros. + monadInv H. simpl. rewrite EQ. auto. + generalize H; intro TR. monadInv TR. simpl. + destruct (Int.eq i n). auto. auto. Qed. -Lemma length_switch_table: - forall sl base, List.length (switch_table sl base) = lblstmts_length sl. +Lemma transl_lbl_stmt_2: + forall nbrk ncnt sl tsl, + transl_lbl_stmt nbrk ncnt sl = OK tsl -> + transl_statement nbrk ncnt (seq_of_labeled_statement sl) = OK (seq_of_lbl_stmt tsl). Proof. - induction sl; intro; simpl. auto. decEq; auto. + induction sl; intros. + monadInv H. simpl. auto. + monadInv H. simpl. rewrite EQ; simpl. rewrite (IHsl _ EQ1). simpl. 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)). +Lemma wt_select_switch: + forall n tyenv sl, + wt_lblstmts tyenv sl -> + wt_lblstmts tyenv (Csem.select_switch n sl). Proof. - induction 1; intros; constructor; auto. + induction 1; simpl. + constructor; auto. + destruct (Int.eq n0 n). constructor; auto. 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. +Lemma wt_seq_of_labeled_statement: + forall tyenv sl, + wt_lblstmts tyenv sl -> + wt_stmt tyenv (seq_of_labeled_statement sl). 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. + induction 1; simpl. auto. + constructor; auto. Qed. - - - - diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index e51533c..4314678 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -32,55 +32,21 @@ Require Import Cshmgenproof1. Section CONSTRUCTORS. -Variable tprog: Csharpminor.program. - -(** * Properties of the translation of [switch] constructs. *) - -Lemma transl_lblstmts_exit: - forall e m1 t m2 sl body n tsl nbrk ncnt, - exec_stmt tprog e m1 body t m2 (Out_exit (lblstmts_length sl + n)) -> - transl_lblstmts nbrk ncnt sl body = OK tsl -> - exec_stmt tprog e m1 tsl t m2 (outcome_block (Out_exit n)). -Proof. - induction sl; intros. - simpl in H; simpl in H0; monadInv H0. - constructor. apply exec_Sseq_stop. auto. congruence. - simpl in H; simpl in H0; monadInv H0. - eapply IHsl with (body := Sblock (Sseq body x)); eauto. - change (Out_exit (lblstmts_length sl + n)) - with (outcome_block (Out_exit (S (lblstmts_length sl + n)))). - constructor. apply exec_Sseq_stop. auto. congruence. -Qed. - -Lemma transl_lblstmts_return: - forall e m1 t m2 sl body optv tsl nbrk ncnt, - exec_stmt tprog e m1 body t m2 (Out_return optv) -> - transl_lblstmts nbrk ncnt sl body = OK tsl -> - exec_stmt tprog e m1 tsl t m2 (Out_return optv). -Proof. - induction sl; intros. - simpl in H; simpl in H0; monadInv H0. - change (Out_return optv) with (outcome_block (Out_return optv)). - constructor. apply exec_Sseq_stop. auto. congruence. - simpl in H; simpl in H0; monadInv H0. - eapply IHsl with (body := Sblock (Sseq body x)); eauto. - change (Out_return optv) with (outcome_block (Out_return optv)). - constructor. apply exec_Sseq_stop. auto. congruence. -Qed. - +Variable globenv : genv * gvarenv. +Let ge := fst globenv. (** * Correctness of Csharpminor construction functions *) Lemma make_intconst_correct: forall n e m, - eval_expr tprog e m (make_intconst n) (Vint n). + eval_expr globenv e m (make_intconst n) (Vint n). Proof. intros. unfold make_intconst. econstructor. reflexivity. Qed. Lemma make_floatconst_correct: forall n e m, - eval_expr tprog e m (make_floatconst n) (Vfloat n). + eval_expr globenv e m (make_floatconst n) (Vfloat n). Proof. intros. unfold make_floatconst. econstructor. reflexivity. Qed. @@ -101,10 +67,10 @@ Qed. Lemma make_boolean_correct_true: forall e m a v ty, - eval_expr tprog e m a v -> + eval_expr globenv e m a v -> is_true v ty -> exists vb, - eval_expr tprog e m (make_boolean a ty) vb + eval_expr globenv e m (make_boolean a ty) vb /\ Val.is_true vb. Proof. intros until ty; intros EXEC VTRUE. @@ -121,10 +87,10 @@ Qed. Lemma make_boolean_correct_false: forall e m a v ty, - eval_expr tprog e m a v -> + eval_expr globenv e m a v -> is_false v ty -> exists vb, - eval_expr tprog e m (make_boolean a ty) vb + eval_expr globenv e m (make_boolean a ty) vb /\ Val.is_false vb. Proof. intros until ty; intros EXEC VFALSE. @@ -143,8 +109,8 @@ Lemma make_neg_correct: forall a tya c va v e m, sem_neg va tya = Some v -> make_neg a tya = OK c -> - eval_expr tprog e m a va -> - eval_expr tprog e m c v. + eval_expr globenv e m a va -> + eval_expr globenv e m c v. Proof. intros until m; intro SEM. unfold make_neg. functional inversion SEM; intros. @@ -156,8 +122,8 @@ Lemma make_notbool_correct: forall a tya c va v e m, sem_notbool va tya = Some v -> make_notbool a tya = c -> - eval_expr tprog e m a va -> - eval_expr tprog e m c v. + eval_expr globenv e m a va -> + eval_expr globenv e m c v. Proof. intros until m; intro SEM. unfold make_notbool. functional inversion SEM; intros; inversion H4; simpl; @@ -168,8 +134,8 @@ Lemma make_notint_correct: forall a tya c va v e m, sem_notint va = Some v -> make_notint a tya = c -> - eval_expr tprog e m a va -> - eval_expr tprog e m c v. + eval_expr globenv e m a va -> + eval_expr globenv e m c v. Proof. intros until m; intro SEM. unfold make_notint. functional inversion SEM; intros. @@ -182,9 +148,9 @@ Definition binary_constructor_correct 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 e m a va -> - eval_expr tprog e m b vb -> - eval_expr tprog e m c v. + eval_expr globenv e m a va -> + eval_expr globenv e m b vb -> + eval_expr globenv e m c v. Definition binary_constructor_correct' (make: expr -> type -> expr -> type -> res expr) @@ -192,9 +158,9 @@ Definition binary_constructor_correct' 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 e m a va -> - eval_expr tprog e m b vb -> - eval_expr tprog e m c v. + eval_expr globenv e m a va -> + eval_expr globenv e m b vb -> + eval_expr globenv e m c v. Lemma make_add_correct: binary_constructor_correct make_add sem_add. Proof. @@ -296,9 +262,9 @@ Lemma make_cmp_correct: 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 e m a va -> - eval_expr tprog e m b vb -> - eval_expr tprog e m c v. + eval_expr globenv e m a va -> + eval_expr globenv e m b vb -> + eval_expr globenv e m c v. Proof. intros until m. intro SEM. unfold make_cmp. functional inversion SEM; rewrite H0; intros. @@ -325,8 +291,8 @@ Lemma transl_unop_correct: 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 e m a va -> - eval_expr tprog e m c v. + eval_expr globenv e m a va -> + eval_expr globenv e m c v. Proof. intros. destruct op; simpl in *. eapply make_notbool_correct; eauto. congruence. @@ -338,9 +304,9 @@ Lemma transl_binop_correct: 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 m = Some v -> - eval_expr tprog e m a va -> - eval_expr tprog e m b vb -> - eval_expr tprog e m c v. + eval_expr globenv e m a va -> + eval_expr globenv e m b vb -> + eval_expr globenv e m c v. Proof. intros. destruct op; simpl in *. eapply make_add_correct; eauto. @@ -363,9 +329,9 @@ Qed. Lemma make_cast_correct: forall e m a v ty1 ty2 v', - eval_expr tprog e m a v -> + eval_expr globenv e m a v -> cast v ty1 ty2 v' -> - eval_expr tprog e m (make_cast ty1 ty2 a) v'. + eval_expr globenv e m (make_cast ty1 ty2 a) v'. Proof. unfold make_cast, make_cast1, make_cast2. intros until v'; intros EVAL CAST. @@ -387,9 +353,9 @@ Qed. Lemma make_load_correct: forall addr ty code b ofs v e m, make_load addr ty = OK code -> - eval_expr tprog e m addr (Vptr b ofs) -> + eval_expr globenv e m addr (Vptr b ofs) -> load_value_of_type ty m b ofs = Some v -> - eval_expr tprog e m code v. + eval_expr globenv e m code v. Proof. unfold make_load, load_value_of_type. intros until m; intros MKLOAD EVEXP LDVAL. @@ -401,18 +367,18 @@ Proof. Qed. Lemma make_store_correct: - forall addr ty rhs code e m b ofs v m', + forall addr ty rhs code e m b ofs v m' f k, make_store addr ty rhs = OK code -> - eval_expr tprog e m addr (Vptr b ofs) -> - eval_expr tprog e m rhs v -> + eval_expr globenv e m addr (Vptr b ofs) -> + eval_expr globenv 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. + step globenv (State f code k e m) E0 (State f Sskip k e m'). Proof. unfold make_store, store_value_of_type. - intros until m'; intros MKSTORE EV1 EV2 STVAL. + intros until k; intros MKSTORE EV1 EV2 STVAL. destruct (access_mode ty); inversion MKSTORE. (* access_mode ty = By_value m *) - eapply exec_Sstore; eauto. + eapply step_store; eauto. Qed. End CONSTRUCTORS. diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index af6dc90..92a0956 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -41,6 +41,8 @@ Hypothesis TRANSL: transl_program prog = OK tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. +Let tgvare : gvarenv := global_var_env tprog. +Let tgve := (tge, tgvare). Lemma symbols_preserved: forall s, Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -80,6 +82,17 @@ Proof. assumption. Qed. +Lemma sig_translated: + forall fd tfd targs tres, + classify_fun (type_of_fundef fd) = fun_case_f targs tres -> + transl_fundef fd = OK tfd -> + funsig tfd = signature_of_type targs tres. +Proof. + intros. destruct fd; monadInv H0; inv H. + monadInv EQ. simpl. auto. + simpl. auto. +Qed. + (** * Matching between environments *) (** In this section, we define a matching relation between @@ -95,9 +108,15 @@ Definition match_var_kind (ty: type) (vk: var_kind) : Prop := Record match_env (tyenv: typenv) (e: Csem.env) (te: Csharpminor.env) : Prop := mk_match_env { me_local: - forall id b ty, - e!id = Some b -> tyenv!id = Some ty -> - exists vk, match_var_kind ty vk /\ te!id = Some (b, vk); + forall id b, + e!id = Some b -> + exists vk, exists ty, + tyenv!id = Some ty + /\ match_var_kind ty vk + /\ te!id = Some (b, vk); + me_local_inv: + forall id b vk, + te!id = Some (b, vk) -> e!id = Some b; me_global: forall id ty, e!id = None -> tyenv!id = Some ty -> @@ -105,6 +124,66 @@ Record match_env (tyenv: typenv) (e: Csem.env) (te: Csharpminor.env) : Prop := (forall chunk, access_mode ty = By_value chunk -> (global_var_env tprog)!id = Some (Vscalar chunk)) }. + +Lemma match_env_same_blocks: + forall tyenv e te, + match_env tyenv e te -> + forall b, In b (Csem.blocks_of_env e) <-> In b (blocks_of_env te). +Proof. + intros. inv H. + unfold Csem.blocks_of_env, blocks_of_env. + set (f := (fun id_b_lv : positive * (block * var_kind) => + let (_, y) := id_b_lv in let (b0, _) := y in b0)). + split; intros. + exploit list_in_map_inv; eauto. intros [[id b'] [A B]]. + simpl in A; subst b'. + exploit (me_local0 id b). apply PTree.elements_complete; auto. + intros [vk [ty [C [D E]]]]. + change b with (f (id, (b, vk))). + apply List.in_map. apply PTree.elements_correct. auto. + exploit list_in_map_inv; eauto. intros [[id [b' vk]] [A B]]. + simpl in A; subst b'. + exploit (me_local_inv0 id b vk). apply PTree.elements_complete; auto. + intro. + change b with (snd (id, b)). + apply List.in_map. apply PTree.elements_correct. auto. +Qed. + +Remark free_list_charact: + forall l m, + free_list m l = + mkmem (fun b => if In_dec eq_block b l then empty_block 0 0 else m.(blocks) b) + m.(nextblock) + m.(nextblock_pos). +Proof. + induction l; intros; simpl. + destruct m; simpl. decEq. apply extensionality. auto. + rewrite IHl. unfold free; simpl. decEq. apply extensionality; intro b. + unfold update. destruct (eq_block a b). + subst b. apply zeq_true. + rewrite zeq_false; auto. + destruct (In_dec eq_block b l); auto. +Qed. + +Lemma mem_free_list_same: + forall m l1 l2, + (forall b, In b l1 <-> In b l2) -> + free_list m l1 = free_list m l2. +Proof. + intros. repeat rewrite free_list_charact. decEq. apply extensionality; intro b. + destruct (In_dec eq_block b l1); destruct (In_dec eq_block b l2); auto. + rewrite H in i. contradiction. + rewrite <- H in i. contradiction. +Qed. + +Lemma match_env_free_blocks: + forall tyenv e te m, + match_env tyenv e te -> + Mem.free_list m (Csem.blocks_of_env e) = Mem.free_list m (blocks_of_env te). +Proof. + intros. apply mem_free_list_same. intros; eapply match_env_same_blocks; eauto. +Qed. + Definition match_globalenv (tyenv: typenv) (gv: gvarenv): Prop := forall id ty chunk, tyenv!id = Some ty -> access_mode ty = By_value chunk -> @@ -117,7 +196,8 @@ Lemma match_globalenv_match_env_empty: Proof. intros. unfold Csem.empty_env, Csharpminor.empty_env. constructor. - intros until ty. repeat rewrite PTree.gempty. congruence. + intros until b. repeat rewrite PTree.gempty. congruence. + intros until vk. rewrite PTree.gempty. congruence. intros. split. apply PTree.gempty. intros. red in H. eauto. @@ -136,13 +216,13 @@ Qed. local variables and initialization of the parameters. *) Lemma match_env_alloc_variables: - forall e1 m1 vars e2 m2 lb, - Csem.alloc_variables e1 m1 vars e2 m2 lb -> + forall e1 m1 vars e2 m2, + Csem.alloc_variables e1 m1 vars e2 m2 -> forall tyenv te1 tvars, match_env tyenv e1 te1 -> transl_vars vars = OK tvars -> exists te2, - Csharpminor.alloc_variables te1 m1 tvars te2 m2 lb + Csharpminor.alloc_variables te1 m1 tvars te2 m2 /\ match_env (Ctyping.add_vars tyenv vars) e2 te2. Proof. induction 1; intros. @@ -156,10 +236,14 @@ Proof. assert (match_env (add_var tyenv (id, ty)) (PTree.set id b1 e) te2). inversion H1. unfold te2, add_var. constructor. (* me_local *) - intros until ty0. repeat rewrite PTree.gsspec. simpl. destruct (peq id0 id); intros. - subst id0. exists vk; split. - apply match_var_kind_of_type. congruence. congruence. + intros until b. simpl. repeat rewrite PTree.gsspec. + destruct (peq id0 id); intros. + inv H3. exists vk; exists ty; intuition. + apply match_var_kind_of_type. congruence. auto. + (* me_local_inv *) + intros until vk0. repeat rewrite PTree.gsspec. + destruct (peq id0 id); intros. congruence. eauto. (* me_global *) intros until ty0. repeat rewrite PTree.gsspec. simpl. destruct (peq id0 id); intros. discriminate. @@ -167,7 +251,7 @@ Proof. destruct (IHalloc_variables _ _ _ H3 TVARS) as [te3 [ALLOC MENV]]. exists te3; split. econstructor; eauto. - rewrite (sizeof_var_kind_of_type _ _ VK). auto. + rewrite (sizeof_var_kind_of_type _ _ VK). eauto. auto. Qed. @@ -192,8 +276,9 @@ Proof. unfold store_value_of_type in H0. rewrite H4 in H0. apply bind_parameters_cons with b m1. assert (tyenv!id = Some ty). apply H2. apply in_eq. - destruct (me_local _ _ _ H3 _ _ _ H H5) as [vk [A B]]. - red in A; rewrite H4 in A. congruence. + destruct (me_local _ _ _ H3 _ _ H) as [vk [ty' [A [B C]]]]. + assert (ty' = ty) by congruence. subst ty'. + red in B; rewrite H4 in B. congruence. assumption. apply IHbind_parameters with tyenv; auto. intros. apply H2. apply in_cons; auto. @@ -326,7 +411,7 @@ Lemma var_get_correct: wt_expr tyenv (Expr (Csyntax.Evar id) ty) -> var_get id ty = OK code -> match_env tyenv e te -> - eval_expr tprog te m code v. + eval_expr tgve te m code v. Proof. intros. inversion H1; subst; clear H1. unfold load_value_of_type in H0. @@ -337,8 +422,9 @@ Proof. inversion H2; clear H2; subst. inversion H; subst; clear H. (* local variable *) - exploit me_local; eauto. intros [vk [A B]]. - red in A; rewrite ACC in A. + exploit me_local; eauto. intros [vk [ty' [A [B C]]]]. + assert (ty' = ty) by congruence. subst ty'. + red in B; rewrite ACC in B. subst vk. eapply eval_Evar. eapply eval_var_ref_local. eauto. assumption. @@ -354,7 +440,7 @@ Proof. inversion H2; clear H2; subst. inversion H; subst; clear H. (* local variable *) - exploit me_local; eauto. intros [vk [A B]]. + exploit me_local; eauto. intros [vk [ty' [A [B C]]]]. eapply eval_Eaddrof. eapply eval_var_addr_local. eauto. (* global variable *) @@ -369,14 +455,14 @@ Qed. (** Correctness of the code generated by [var_set]. *) Lemma var_set_correct: - forall e m id ty loc ofs v m' tyenv code te rhs, + forall e m id ty loc ofs v m' tyenv code te rhs f k, Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) loc ofs -> store_value_of_type ty m loc ofs v = Some m' -> wt_expr tyenv (Expr (Csyntax.Evar id) ty) -> var_set id ty rhs = OK code -> match_env tyenv e te -> - eval_expr tprog te m rhs v -> - exec_stmt tprog te m code E0 m' Out_normal. + eval_expr tgve te m rhs v -> + step tgve (State f code k te m) E0 (State f Sskip k te m'). Proof. intros. inversion H1; subst; clear H1. unfold store_value_of_type in H0. @@ -387,15 +473,16 @@ Proof. inversion H2; clear H2; subst. inversion H; subst; clear H. (* local variable *) - exploit me_local; eauto. intros [vk [A B]]. - red in A; rewrite ACC in A; subst vk. - eapply exec_Sassign. eauto. + exploit me_local; eauto. intros [vk [ty' [A [B C]]]]. + assert (ty' = ty) by congruence. subst ty'. + red in B; rewrite ACC in B; subst vk. + eapply step_assign. eauto. econstructor. eapply eval_var_ref_local. eauto. assumption. (* global variable *) exploit me_global; eauto. intros [A B]. - eapply exec_Sassign. eauto. - econstructor. eapply eval_var_ref_global. auto. - fold tge. rewrite symbols_preserved. eauto. + eapply step_assign. eauto. + econstructor. eapply eval_var_ref_global. auto. + change (fst tgve) with tge. rewrite symbols_preserved. eauto. eauto. assumption. (* access mode By_reference *) intros ACC. rewrite ACC in H0. discriminate. @@ -403,35 +490,59 @@ Proof. intros. rewrite H1 in H0; discriminate. Qed. -Lemma call_dest_set_correct: - forall e m0 lhs loc ofs m1 v m2 tyenv optid te, - Csem.eval_lvalue ge e m0 lhs loc ofs -> - store_value_of_type (typeof lhs) m1 loc ofs v = Some m2 -> +Lemma call_dest_correct: + forall e m lhs loc ofs tyenv optid te, + Csem.eval_lvalue ge e m lhs loc ofs -> wt_expr tyenv lhs -> transl_lhs_call (Some lhs) = OK optid -> match_env tyenv e te -> - exec_opt_assign tprog te m1 optid v m2. -Proof. - intros. generalize H2. simpl. caseEq (is_variable lhs). 2: congruence. - intros. inv H5. - exploit is_variable_correct; eauto. intro. - rewrite H5 in H. rewrite H5 in H1. inversion H1. subst i ty. - constructor. - generalize H0. unfold store_value_of_type. - caseEq (access_mode (typeof lhs)); intros; try discriminate. - (* access mode By_value *) - inversion H. - (* local variable *) + exists id, + optid = Some id + /\ tyenv!id = Some (typeof lhs) + /\ ofs = Int.zero + /\ match access_mode (typeof lhs) with + | By_value chunk => eval_var_ref tgve te id loc chunk + | _ => True + end. +Proof. + intros. generalize H1. simpl. caseEq (is_variable lhs); try congruence. + intros id ISV EQ. inv EQ. + exploit is_variable_correct; eauto. intro EQ. + rewrite EQ in H0. inversion H0. subst id0 ty. + exists id. split; auto. split. rewrite EQ in H0. inversion H0. auto. + rewrite EQ in H. inversion H. +(* local variable *) + split. auto. subst id0 ty l ofs. exploit me_local; eauto. - intros [vk [A B]]. red in A. rewrite H6 in A. subst vk. - econstructor. eapply eval_var_ref_local; eauto. assumption. - (* global variable *) - subst id0 ty l ofs. exploit me_global; eauto. - intros [A B]. - econstructor. eapply eval_var_ref_global; eauto. - rewrite symbols_preserved. eauto. assumption. + intros [vk [ty [A [B C]]]]. + assert (ty = typeof lhs) by congruence. rewrite <- H3. + generalize B; unfold match_var_kind. destruct (access_mode ty); auto. + intros. subst vk. apply eval_var_ref_local; auto. +(* global variable *) + split. auto. + subst id0 ty l ofs. exploit me_global; eauto. intros [A B]. + case_eq (access_mode (typeof lhs)); intros; auto. + apply eval_var_ref_global; auto. + simpl. rewrite <- H9. apply symbols_preserved. +Qed. + +Lemma set_call_dest_correct: + forall ty m loc v m' tyenv e te id, + store_value_of_type ty m loc Int.zero v = Some m' -> + match access_mode ty with + | By_value chunk => eval_var_ref tgve te id loc chunk + | _ => True + end -> + match_env tyenv e te -> + tyenv!id = Some ty -> + exec_opt_assign tgve te m (Some id) v m'. +Proof. + intros. generalize H. unfold store_value_of_type. case_eq (access_mode ty); intros; try congruence. + rewrite H3 in H0. + constructor. econstructor. eauto. auto. Qed. + (** * Proof of semantic preservation *) (** ** Semantic preservation for expressions *) @@ -441,7 +552,7 @@ Qed. << e, m, a ------------------- te, m, ta | | - t| |t + | | | | v v e, m, v ------------------- te, m, v @@ -468,19 +579,19 @@ Definition eval_expr_prop (a: Csyntax.expr) (v: val) : Prop := forall ta (WT: wt_expr tyenv a) (TR: transl_expr a = OK ta), - Csharpminor.eval_expr tprog te m ta v. + Csharpminor.eval_expr tgve te m ta v. Definition eval_lvalue_prop (a: Csyntax.expr) (b: block) (ofs: int) : Prop := forall ta (WT: wt_expr tyenv a) (TR: transl_lvalue a = OK ta), - Csharpminor.eval_expr tprog te m ta (Vptr b ofs). + Csharpminor.eval_expr tgve te m ta (Vptr b ofs). Definition eval_exprlist_prop (al: list Csyntax.expr) (vl: list val) : Prop := forall tal (WT: wt_exprlist tyenv al) (TR: transl_exprlist al = OK tal), - Csharpminor.eval_exprlist tprog te m tal vl. + Csharpminor.eval_exprlist tgve te m tal vl. (* Check (eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop). *) @@ -687,7 +798,8 @@ Lemma transl_Evar_local_correct: eval_lvalue_prop (Expr (Csyntax.Evar id) ty) l Int.zero. Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. - exploit (me_local _ _ _ MENV); eauto. intros [vk [A B]]. + exploit (me_local _ _ _ MENV); eauto. + intros [vk [ty' [A [B C]]]]. econstructor. eapply eval_var_addr_local. eauto. Qed. @@ -805,1068 +917,773 @@ Qed. End EXPR. -(** ** Semantic preservation for statements *) - -(** The simulation diagrams for terminating statements and function - calls are of the following form: - relies on simulation diagrams of the following form: -<< - e, m1, s ------------------- te, m1, ts - | | - t| |t - | | - v v - e, m2, out ----------------- te, m2, tout ->> - Left: execution of statement [s] in Clight. - Right: execution of its translation [ts] in Csharpminor. - Top (precondition): matching between environments [e], [te], - plus well-typedness of statement [s]. - Bottom (postcondition): the outcomes [out] and [tout] are - related per the following function [transl_outcome]. -*) - -Definition transl_outcome (nbrk ncnt: nat) (out: Csem.outcome): Csharpminor.outcome := - match out with - | Csem.Out_normal => Csharpminor.Out_normal - | Csem.Out_break => Csharpminor.Out_exit nbrk - | Csem.Out_continue => Csharpminor.Out_exit ncnt - | Csem.Out_return vopt => Csharpminor.Out_return vopt - end. - -Definition exec_stmt_prop - (e: Csem.env) (m1: mem) (s: Csyntax.statement) (t: trace) - (m2: mem) (out: Csem.outcome) : Prop := - forall tyenv nbrk ncnt ts te - (WT: wt_stmt tyenv s) - (TR: transl_statement nbrk ncnt s = OK ts) - (MENV: match_env tyenv e te), - Csharpminor.exec_stmt tprog te m1 ts t m2 (transl_outcome nbrk ncnt out). - -Definition exec_lblstmts_prop - (e: Csem.env) (m1: mem) (s: Csyntax.labeled_statements) - (t: trace) (m2: mem) (out: Csem.outcome) : Prop := - forall tyenv nbrk ncnt body ts te m0 t0 - (WT: wt_lblstmts tyenv s) - (TR: transl_lblstmts (lblstmts_length s) - (1 + lblstmts_length s + ncnt) - s body = OK ts) - (MENV: match_env tyenv e te) - (BODY: Csharpminor.exec_stmt tprog te m0 body t0 m1 Out_normal), - Csharpminor.exec_stmt tprog te m0 ts (t0 ** t) m2 - (transl_outcome nbrk ncnt (outcome_switch out)). - -Definition eval_funcall_prop - (m1: mem) (f: Csyntax.fundef) (params: list val) - (t: trace) (m2: mem) (res: val) : Prop := - forall tf - (WT: wt_fundef (global_typenv prog) f) - (TR: transl_fundef f = OK tf), - Csharpminor.eval_funcall tprog m1 tf params t m2 res. - -(* -Type Printing Depth 100. -Check (Csem.eval_funcall_ind3 ge exec_stmt_prop exec_lblstmts_prop eval_funcall_prop). -*) - -Lemma transl_Sskip_correct: - (forall (e : Csem.env) (m : mem), - exec_stmt_prop e m Csyntax.Sskip E0 m Csem.Out_normal). -Proof. - intros; red; intros. monadInv TR. simpl. constructor. -Qed. - -Lemma transl_Sassign_correct: - forall (e : Csem.env) (m : mem) (a1 a2 : Csyntax.expr) (loc : block) - (ofs : int) (v2 : val) (m' : mem), - eval_lvalue ge e m a1 loc ofs -> - Csem.eval_expr ge e m a2 v2 -> - store_value_of_type (typeof a1) m loc ofs v2 = Some m' -> - exec_stmt_prop e m (Csyntax.Sassign a1 a2) E0 m' Csem.Out_normal. -Proof. - intros; red; intros. - inversion WT; subst; clear WT. - simpl in TR. - caseEq (is_variable a1). - (* a = variable id *) - intros id ISVAR. rewrite ISVAR in TR. - generalize (is_variable_correct _ _ ISVAR). intro EQ. - rewrite EQ in H; rewrite EQ in H4. - monadInv TR. - eapply var_set_correct; eauto. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. - (* a is not a variable *) - intro ISVAR; rewrite ISVAR in TR. monadInv TR. - eapply make_store_correct; eauto. - eapply (transl_lvalue_correct _ _ _ _ MENV _ _ _ H); eauto. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. -Qed. - -Lemma transl_Scall_None_correct: - forall (e : Csem.env) (m : mem) (a : Csyntax.expr) - (al : list Csyntax.expr) (vf : val) (vargs : list val) - (f : Csyntax.fundef) (t : trace) (m' : mem) (vres : val), - Csem.eval_expr ge e m a vf -> - Csem.eval_exprlist ge e m al vargs -> - Genv.find_funct ge vf = Some f -> - type_of_fundef f = typeof a -> - Csem.eval_funcall ge m f vargs t m' vres -> - eval_funcall_prop m f vargs t m' vres -> - exec_stmt_prop e m (Csyntax.Scall None a al) t m' Csem.Out_normal. -Proof. - intros; red; intros; simpl. - inv WT. simpl in TR. - caseEq (classify_fun (typeof a)); intros; rewrite H5 in TR; monadInv TR. - exploit functions_translated; eauto. intros [tf [TFIND TFD]]. - econstructor. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto. - eapply (transl_exprlist_correct _ _ _ _ MENV _ _ H0); eauto. - eauto. - eapply transl_fundef_sig1; eauto. rewrite H2; auto. - eapply H4; eauto. - eapply functions_well_typed; eauto. - constructor. -Qed. - -Lemma transl_Scall_Some_correct: - forall (e : Csem.env) (m : mem) (lhs a : Csyntax.expr) - (al : list Csyntax.expr) (loc : block) (ofs : int) (vf : val) - (vargs : list val) (f : Csyntax.fundef) (t : trace) (m' : mem) - (vres : val) (m'' : mem), - eval_lvalue ge e m lhs loc ofs -> - Csem.eval_expr ge e m a vf -> - Csem.eval_exprlist ge e m al vargs -> - Genv.find_funct ge vf = Some f -> - type_of_fundef f = typeof a -> - Csem.eval_funcall ge m f vargs t m' vres -> - eval_funcall_prop m f vargs t m' vres -> - store_value_of_type (typeof lhs) m' loc ofs vres = Some m'' -> - exec_stmt_prop e m (Csyntax.Scall (Some lhs) a al) t m'' Csem.Out_normal. -Proof. - intros; red; intros; simpl. - inv WT. inv H10. unfold transl_statement in TR. - caseEq (classify_fun (typeof a)); intros; rewrite H7 in TR; monadInv TR. - exploit functions_translated; eauto. intros [tf [TFIND TFD]]. - econstructor. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. - eapply (transl_exprlist_correct _ _ _ _ MENV _ _ H1); eauto. - eauto. - eapply transl_fundef_sig1; eauto. rewrite H3; auto. - eapply H5; eauto. - eapply functions_well_typed; eauto. - eapply call_dest_set_correct; eauto. -Qed. - -Lemma transl_Ssequence_1_correct: - (forall (e : Csem.env) (m : mem) (s1 s2 : statement) (t1 : trace) - (m1 : mem) (t2 : trace) (m2 : mem) (out : Csem.outcome), - Csem.exec_stmt ge e m s1 t1 m1 Csem.Out_normal -> - exec_stmt_prop e m s1 t1 m1 Csem.Out_normal -> - Csem.exec_stmt ge e m1 s2 t2 m2 out -> - exec_stmt_prop e m1 s2 t2 m2 out -> - exec_stmt_prop e m (Ssequence s1 s2) (t1 ** t2) m2 out). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - red in H0; simpl in H0. eapply exec_Sseq_continue; eauto. -Qed. - -Lemma transl_Ssequence_2_correct: - (forall (e : Csem.env) (m : mem) (s1 s2 : statement) (t1 : trace) - (m1 : mem) (out : Csem.outcome), - Csem.exec_stmt ge e m s1 t1 m1 out -> - exec_stmt_prop e m s1 t1 m1 out -> - out <> Csem.Out_normal -> - exec_stmt_prop e m (Ssequence s1 s2) t1 m1 out). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - eapply exec_Sseq_stop; eauto. - destruct out; simpl; congruence. -Qed. - -Lemma transl_Sifthenelse_true_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) - (s1 s2 : statement) (v1 : val) (t : trace) (m' : mem) - (out : Csem.outcome), - Csem.eval_expr ge e m a v1 -> - is_true v1 (typeof a) -> - Csem.exec_stmt ge e m s1 t m' out -> - exec_stmt_prop e m s1 t m' out -> - exec_stmt_prop e m (Csyntax.Sifthenelse a s1 s2) t m' out). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - exploit make_boolean_correct_true. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto. - eauto. - intros [vb [EVAL ISTRUE]]. - eapply exec_Sifthenelse; eauto. apply Val.bool_of_true_val; eauto. simpl; eauto. -Qed. - -Lemma transl_Sifthenelse_false_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) - (s1 s2 : statement) (v1 : val) (t : trace) (m' : mem) - (out : Csem.outcome), - Csem.eval_expr ge e m a v1 -> - is_false v1 (typeof a) -> - Csem.exec_stmt ge e m s2 t m' out -> - exec_stmt_prop e m s2 t m' out -> - exec_stmt_prop e m (Csyntax.Sifthenelse a s1 s2) t m' out). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - exploit make_boolean_correct_false. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto. - eauto. - intros [vb [EVAL ISFALSE]]. - eapply exec_Sifthenelse; eauto. apply Val.bool_of_false_val; eauto. simpl; eauto. -Qed. - -Lemma transl_Sreturn_none_correct: - (forall (e : Csem.env) (m : mem), - exec_stmt_prop e m (Csyntax.Sreturn None) E0 m (Csem.Out_return None)). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - simpl. apply exec_Sreturn_none. -Qed. - -Lemma transl_Sreturn_some_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (v : val), - Csem.eval_expr ge e m a v -> - exec_stmt_prop e m (Csyntax.Sreturn (Some a)) E0 m (Csem.Out_return (Some v))). -Proof. - intros; red; intros. inv WT. inv H1. monadInv TR. - simpl. eapply exec_Sreturn_some; eauto. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto. -Qed. - -Lemma transl_Sbreak_correct: - (forall (e : Csem.env) (m : mem), - exec_stmt_prop e m Sbreak E0 m Out_break). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - simpl. apply exec_Sexit. -Qed. - -Lemma transl_Scontinue_correct: - (forall (e : Csem.env) (m : mem), - exec_stmt_prop e m Scontinue E0 m Out_continue). -Proof. - intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - simpl. apply exec_Sexit. -Qed. - Lemma exit_if_false_true: - forall a ts e m v tyenv te, + forall a ts e m v tyenv te f tk, exit_if_false a = OK ts -> Csem.eval_expr ge e m a v -> is_true v (typeof a) -> match_env tyenv e te -> wt_expr tyenv a -> - exec_stmt tprog te m ts E0 m Out_normal. + step tgve (State f ts tk te m) E0 (State f Sskip tk te m). Proof. intros. monadInv H. exploit make_boolean_correct_true. eapply (transl_expr_correct _ _ _ _ H2 _ _ H0); eauto. eauto. intros [vb [EVAL ISTRUE]]. - eapply exec_Sifthenelse with (v := vb); eauto. + change Sskip with (if true then Sskip else Sexit 0). + eapply step_ifthenelse; eauto. apply Val.bool_of_true_val; eauto. - constructor. Qed. Lemma exit_if_false_false: - forall a ts e m v tyenv te, + forall a ts e m v tyenv te f tk, exit_if_false a = OK ts -> Csem.eval_expr ge e m a v -> is_false v (typeof a) -> match_env tyenv e te -> wt_expr tyenv a -> - exec_stmt tprog te m ts E0 m (Out_exit 0). + step tgve (State f ts tk te m) E0 (State f (Sexit 0) tk te m). Proof. intros. monadInv H. exploit make_boolean_correct_false. eapply (transl_expr_correct _ _ _ _ H2 _ _ H0); eauto. eauto. intros [vb [EVAL ISFALSE]]. - eapply exec_Sifthenelse with (v := vb); eauto. + change (Sexit 0) with (if false then Sskip else Sexit 0). + eapply step_ifthenelse; eauto. apply Val.bool_of_false_val; eauto. - simpl. constructor. Qed. -Lemma transl_Swhile_false_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (s : statement) - (v : val), - Csem.eval_expr ge e m a v -> - is_false v (typeof a) -> - exec_stmt_prop e m (Swhile a s) E0 m Csem.Out_normal). -Proof. - intros; red; intros; simpl. inv WT. monadInv TR. - change Out_normal with (outcome_block (Out_exit 0)). - apply exec_Sblock. apply exec_Sloop_stop. apply exec_Sseq_stop. - eapply exit_if_false_false; eauto. congruence. congruence. -Qed. +(** ** Semantic preservation for statements *) -Lemma transl_out_break_or_return: - forall out1 out2 nbrk ncnt, - out_break_or_return out1 out2 -> - transl_outcome nbrk ncnt out2 = - outcome_block (outcome_block (transl_outcome 1 0 out1)). -Proof. - intros. inversion H; subst; reflexivity. -Qed. +(** The simulation diagram for the translation of statements and functions + is a "plus" diagram of the form +<< + I + S1 ------- R1 + | | + t | + | t + v v + S2 ------- R2 + I I +>> -Lemma transl_out_normal_or_continue: - forall out, - out_normal_or_continue out -> - Out_normal = outcome_block (transl_outcome 1 0 out). -Proof. - intros; inversion H; reflexivity. -Qed. +The invariant [I] is the [match_states] predicate that we now define. +*) -Lemma transl_Swhile_stop_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (v : val) - (s : statement) (t : trace) (m' : mem) (out' out : Csem.outcome), - Csem.eval_expr ge e m a v -> - is_true v (typeof a) -> - Csem.exec_stmt ge e m s t m' out' -> - exec_stmt_prop e m s t m' out' -> - out_break_or_return out' out -> - exec_stmt_prop e m (Swhile a s) t m' out). -Proof. - intros; red; intros. inv WT. monadInv TR. - rewrite (transl_out_break_or_return _ _ nbrk ncnt H3). - apply exec_Sblock. apply exec_Sloop_stop. - eapply exec_Sseq_continue. - eapply exit_if_false_true; eauto. - apply exec_Sblock. eauto. traceEq. - inversion H3; simpl; congruence. -Qed. +Definition typenv_fun (f: Csyntax.function) := + add_vars (global_typenv prog) (f.(Csyntax.fn_params) ++ f.(Csyntax.fn_vars)). -Lemma transl_Swhile_loop_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (s : statement) - (v : val) (t1 : trace) (m1 : mem) (out1 : Csem.outcome) - (t2 : trace) (m2 : mem) (out : Csem.outcome), - Csem.eval_expr ge e m a v -> - is_true v (typeof a) -> - Csem.exec_stmt ge e m s t1 m1 out1 -> - exec_stmt_prop e m s t1 m1 out1 -> - out_normal_or_continue out1 -> - Csem.exec_stmt ge e m1 (Swhile a s) t2 m2 out -> - exec_stmt_prop e m1 (Swhile a s) t2 m2 out -> - exec_stmt_prop e m (Swhile a s) (t1 ** t2) m2 out). -Proof. - intros; red; intros. - exploit H5; eauto. intro NEXTITER. - inv WT. monadInv TR. - inversion NEXTITER; subst. - apply exec_Sblock. - eapply exec_Sloop_loop. eapply exec_Sseq_continue. - eapply exit_if_false_true; eauto. - rewrite (transl_out_normal_or_continue _ H3). - apply exec_Sblock. eauto. - reflexivity. eassumption. - traceEq. -Qed. +Inductive match_transl: stmt -> cont -> stmt -> cont -> Prop := + | match_transl_0: forall ts tk, + match_transl ts tk ts tk + | match_transl_1: forall ts tk, + match_transl (Sblock ts) tk ts (Kblock tk). -Lemma transl_Sdowhile_false_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr) - (t : trace) (m1 : mem) (out1 : Csem.outcome) (v : val), - Csem.exec_stmt ge e m s t m1 out1 -> - exec_stmt_prop e m s t m1 out1 -> - out_normal_or_continue out1 -> - Csem.eval_expr ge e m1 a v -> - is_false v (typeof a) -> - exec_stmt_prop e m (Sdowhile a s) t m1 Csem.Out_normal). +Lemma match_transl_step: + forall ts tk ts' tk' f te m, + match_transl (Sblock ts) tk ts' tk' -> + star step tgve (State f ts' tk' te m) E0 (State f ts (Kblock tk) te m). Proof. - intros; red; intros. inv WT. monadInv TR. - simpl. - change Out_normal with (outcome_block (Out_exit 0)). - apply exec_Sblock. apply exec_Sloop_stop. eapply exec_Sseq_continue. - rewrite (transl_out_normal_or_continue out1 H1). - apply exec_Sblock. eauto. - eapply exit_if_false_false; eauto. traceEq. congruence. -Qed. + intros. inv H. + apply star_one. constructor. + apply star_refl. +Qed. + +Inductive match_cont: typenv -> nat -> nat -> Csem.cont -> Csharpminor.cont -> Prop := + | match_Kstop: forall tyenv nbrk ncnt, + match_cont tyenv nbrk ncnt Csem.Kstop Kstop + | match_Kseq: forall tyenv nbrk ncnt s k ts tk, + transl_statement nbrk ncnt s = OK ts -> + wt_stmt tyenv s -> + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv nbrk ncnt + (Csem.Kseq s k) + (Kseq ts tk) + | match_Kwhile: forall tyenv nbrk ncnt a s k ta ts tk, + exit_if_false a = OK ta -> + transl_statement 1%nat 0%nat s = OK ts -> + wt_expr tyenv a -> + wt_stmt tyenv s -> + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv 1%nat 0%nat + (Csem.Kwhile a s k) + (Kblock (Kseq (Sloop (Sseq ta (Sblock ts))) (Kblock tk))) + | match_Kdowhile: forall tyenv nbrk ncnt a s k ta ts tk, + exit_if_false a = OK ta -> + transl_statement 1%nat 0%nat s = OK ts -> + wt_expr tyenv a -> + wt_stmt tyenv s -> + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv 1%nat 0%nat + (Csem.Kdowhile a s k) + (Kblock (Kseq ta (Kseq (Sloop (Sseq (Sblock ts) ta)) (Kblock tk)))) + | match_Kfor2: forall tyenv nbrk ncnt a2 a3 s k ta2 ta3 ts tk, + exit_if_false a2 = OK ta2 -> + transl_statement nbrk ncnt a3 = OK ta3 -> + transl_statement 1%nat 0%nat s = OK ts -> + wt_expr tyenv a2 -> wt_stmt tyenv a3 -> wt_stmt tyenv s -> + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv 1%nat 0%nat + (Csem.Kfor2 a2 a3 s k) + (Kblock (Kseq ta3 (Kseq (Sloop (Sseq ta2 (Sseq (Sblock ts) ta3))) (Kblock tk)))) + | match_Kfor3: forall tyenv nbrk ncnt a2 a3 s k ta2 ta3 ts tk, + exit_if_false a2 = OK ta2 -> + transl_statement nbrk ncnt a3 = OK ta3 -> + transl_statement 1%nat 0%nat s = OK ts -> + wt_expr tyenv a2 -> wt_stmt tyenv a3 -> wt_stmt tyenv s -> + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv nbrk ncnt + (Csem.Kfor3 a2 a3 s k) + (Kseq (Sloop (Sseq ta2 (Sseq (Sblock ts) ta3))) (Kblock tk)) + | match_Kswitch: forall tyenv nbrk ncnt k tk, + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv 0%nat (S ncnt) + (Csem.Kswitch k) + (Kblock tk) + | match_Kcall_none: forall tyenv nbrk ncnt nbrk' ncnt' f e k tf te tk, + transl_function f = OK tf -> + wt_stmt (typenv_fun f) f.(Csyntax.fn_body) -> + match_env (typenv_fun f) e te -> + match_cont (typenv_fun f) nbrk' ncnt' k tk -> + match_cont tyenv nbrk ncnt + (Csem.Kcall None f e k) + (Kcall None tf te tk) + | match_Kcall_some: forall tyenv nbrk ncnt nbrk' ncnt' loc ofs ty f e k id tf te tk, + transl_function f = OK tf -> + wt_stmt (typenv_fun f) f.(Csyntax.fn_body) -> + match_env (typenv_fun f) e te -> + ofs = Int.zero -> + (typenv_fun f)!id = Some ty -> + match access_mode ty with + | By_value chunk => eval_var_ref tgve te id loc chunk + | _ => True + end -> + match_cont (typenv_fun f) nbrk' ncnt' k tk -> + match_cont tyenv nbrk ncnt + (Csem.Kcall (Some(loc, ofs, ty)) f e k) + (Kcall (Some id) tf te tk). + +Inductive match_states: Csem.state -> Csharpminor.state -> Prop := + | match_state: + forall f nbrk ncnt s k e m tf ts tk te ts' tk' + (TRF: transl_function f = OK tf) + (TR: transl_statement nbrk ncnt s = OK ts) + (MTR: match_transl ts tk ts' tk') + (WTF: wt_stmt (typenv_fun f) f.(Csyntax.fn_body)) + (WT: wt_stmt (typenv_fun f) s) + (MENV: match_env (typenv_fun f) e te) + (MK: match_cont (typenv_fun f) nbrk ncnt k tk), + match_states (Csem.State f s k e m) + (State tf ts' tk' te m) + | match_callstate: + forall fd args k m tfd tk + (TR: transl_fundef fd = OK tfd) + (WT: wt_fundef (global_typenv prog) fd) + (MK: match_cont (global_typenv prog) 0%nat 0%nat k tk) + (ISCC: Csem.is_call_cont k), + match_states (Csem.Callstate fd args k m) + (Callstate tfd args tk m) + | match_returnstate: + forall res k m tk + (MK: match_cont (global_typenv prog) 0%nat 0%nat k tk), + match_states (Csem.Returnstate res k m) + (Returnstate res tk m). + +Remark match_states_skip: + forall f e te nbrk ncnt k tf tk m, + transl_function f = OK tf -> + wt_stmt (typenv_fun f) f.(Csyntax.fn_body) -> + match_env (typenv_fun f) e te -> + match_cont (typenv_fun f) nbrk ncnt k tk -> + match_states (Csem.State f Csyntax.Sskip k e m) (State tf Sskip tk te m). +Proof. + intros. econstructor; eauto. simpl; reflexivity. constructor. constructor. +Qed. + +(** Commutation between label resolution and compilation *) + +Section FIND_LABEL. +Variable lbl: label. +Variable tyenv: typenv. -Lemma transl_Sdowhile_stop_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr) - (t : trace) (m1 : mem) (out1 out : Csem.outcome), - Csem.exec_stmt ge e m s t m1 out1 -> - exec_stmt_prop e m s t m1 out1 -> - out_break_or_return out1 out -> - exec_stmt_prop e m (Sdowhile a s) t m1 out). -Proof. - intros; red; intros. inv WT. monadInv TR. - simpl. - assert (outcome_block (transl_outcome 1 0 out1) <> Out_normal). - inversion H1; simpl; congruence. - rewrite (transl_out_break_or_return _ _ nbrk ncnt H1). - apply exec_Sblock. apply exec_Sloop_stop. - apply exec_Sseq_stop. apply exec_Sblock. eauto. - auto. auto. -Qed. +Remark exit_if_false_no_label: + forall a s, exit_if_false a = OK s -> forall k, find_label lbl s k = None. +Proof. + intros. unfold exit_if_false in H. monadInv H. simpl. auto. +Qed. + +Lemma transl_find_label: + forall s nbrk ncnt k ts tk + (WT: wt_stmt tyenv s) + (TR: transl_statement nbrk ncnt s = OK ts) + (MC: match_cont tyenv nbrk ncnt k tk), + match Csem.find_label lbl s k with + | None => find_label lbl ts tk = None + | Some (s', k') => + exists ts', exists tk', exists nbrk', exists ncnt', + find_label lbl ts tk = Some (ts', tk') + /\ transl_statement nbrk' ncnt' s' = OK ts' + /\ match_cont tyenv nbrk' ncnt' k' tk' + /\ wt_stmt tyenv s' + end + +with transl_find_label_ls: + forall ls nbrk ncnt k tls tk + (WT: wt_lblstmts tyenv ls) + (TR: transl_lbl_stmt nbrk ncnt ls = OK tls) + (MC: match_cont tyenv nbrk ncnt k tk), + match Csem.find_label_ls lbl ls k with + | None => find_label_ls lbl tls tk = None + | Some (s', k') => + exists ts', exists tk', exists nbrk', exists ncnt', + find_label_ls lbl tls tk = Some (ts', tk') + /\ transl_statement nbrk' ncnt' s' = OK ts' + /\ match_cont tyenv nbrk' ncnt' k' tk' + /\ wt_stmt tyenv s' + end. -Lemma transl_Sdowhile_loop_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a : Csyntax.expr) - (m1 m2 : mem) (t1 t2 : trace) (out out1 : Csem.outcome) (v : val), - Csem.exec_stmt ge e m s t1 m1 out1 -> - exec_stmt_prop e m s t1 m1 out1 -> - out_normal_or_continue out1 -> - Csem.eval_expr ge e m1 a v -> - is_true v (typeof a) -> - Csem.exec_stmt ge e m1 (Sdowhile a s) t2 m2 out -> - exec_stmt_prop e m1 (Sdowhile a s) t2 m2 out -> - exec_stmt_prop e m (Sdowhile a s) (t1 ** t2) m2 out). Proof. - intros; red; intros. - exploit H5; eauto. intro NEXTITER. - inv WT. monadInv TR. inversion NEXTITER; subst. - apply exec_Sblock. - eapply exec_Sloop_loop. eapply exec_Sseq_continue. - rewrite (transl_out_normal_or_continue _ H1). - apply exec_Sblock. eauto. - eapply exit_if_false_true; eauto. - reflexivity. eassumption. traceEq. -Qed. + intro s; case s; intros; inv WT; try (monadInv TR); simpl. +(* skip *) + auto. +(* assign *) + simpl in TR. destruct (is_variable e); monadInv TR. + unfold var_set in EQ0. destruct (access_mode (typeof e)); inv EQ0. auto. + unfold make_store in EQ2. destruct (access_mode (typeof e)); inv EQ2. auto. +(* call *) + simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto. +(* seq *) + exploit (transl_find_label s0 nbrk ncnt (Csem.Kseq s1 k)); eauto. constructor; eauto. + destruct (Csem.find_label lbl s0 (Csem.Kseq s1 k)) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H. eapply transl_find_label; eauto. +(* ifthenelse *) + exploit (transl_find_label s0); eauto. + destruct (Csem.find_label lbl s0 k) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H. eapply transl_find_label; eauto. +(* while *) + rewrite (exit_if_false_no_label _ _ EQ). + eapply transl_find_label; eauto. econstructor; eauto. +(* dowhile *) + exploit (transl_find_label s0 1%nat 0%nat (Csem.Kdowhile e s0 k)); eauto. econstructor; eauto. + destruct (Csem.find_label lbl s0 (Kdowhile e s0 k)) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H. eapply exit_if_false_no_label; eauto. +(* for *) + simpl in TR. destruct (is_Sskip s0); monadInv TR. + simpl. rewrite (exit_if_false_no_label _ _ EQ). + exploit (transl_find_label s2 1%nat 0%nat (Kfor2 e s1 s2 k)); eauto. econstructor; eauto. + destruct (Csem.find_label lbl s2 (Kfor2 e s1 s2 k)) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H. + eapply transl_find_label; eauto. econstructor; eauto. + exploit (transl_find_label s0 nbrk ncnt (Csem.Kseq (Sfor Csyntax.Sskip e s1 s2) k)); eauto. + econstructor; eauto. simpl. rewrite is_Sskip_true. rewrite EQ1; simpl. rewrite EQ0; simpl. rewrite EQ2; simpl. reflexivity. + constructor; auto. constructor. + simpl. rewrite (exit_if_false_no_label _ _ EQ1). + destruct (Csem.find_label lbl s0 (Csem.Kseq (Sfor Csyntax.Sskip e s1 s2) k)) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H. + exploit (transl_find_label s2 1%nat 0%nat (Kfor2 e s1 s2 k)); eauto. econstructor; eauto. + destruct (Csem.find_label lbl s2 (Kfor2 e s1 s2 k)) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H0. + eapply transl_find_label; eauto. econstructor; eauto. +(* break *) + auto. +(* continue *) + auto. +(* return *) + simpl in TR. destruct o; monadInv TR. auto. auto. +(* switch *) + eapply transl_find_label_ls with (k := Csem.Kswitch k); eauto. econstructor; eauto. +(* label *) + destruct (ident_eq lbl l). + exists x; exists tk; exists nbrk; exists ncnt; auto. + eapply transl_find_label; eauto. +(* goto *) + auto. -Lemma transl_Sfor_start_correct: - (forall (e : Csem.env) (m : mem) (s a1 : statement) - (a2 : Csyntax.expr) (a3 : statement) (out : Csem.outcome) - (m1 m2 : mem) (t1 t2 : trace), - a1 <> Csyntax.Sskip -> - Csem.exec_stmt ge e m a1 t1 m1 Csem.Out_normal -> - exec_stmt_prop e m a1 t1 m1 Csem.Out_normal -> - Csem.exec_stmt ge e m1 (Sfor Csyntax.Sskip a2 a3 s) t2 m2 out -> - exec_stmt_prop e m1 (Sfor Csyntax.Sskip a2 a3 s) t2 m2 out -> - exec_stmt_prop e m (Sfor a1 a2 a3 s) (t1 ** t2) m2 out). -Proof. - intros; red; intros. - destruct (transl_stmt_Sfor_start _ _ _ _ _ _ _ TR H) as [ts1 [ts2 [EQ [TR1 TR2]]]]. - subst ts. - inv WT. - assert (WT': wt_stmt tyenv (Sfor Csyntax.Sskip a2 a3 s)). - constructor; auto. constructor. - exploit H1; eauto. simpl. intro EXEC1. - exploit H3; eauto. intro EXEC2. - eapply exec_Sseq_continue; eauto. + intro ls; case ls; intros; inv WT; monadInv TR; simpl. +(* default *) + eapply transl_find_label; eauto. +(* case *) + exploit (transl_find_label s nbrk ncnt (Csem.Kseq (seq_of_labeled_statement l) k)); eauto. + econstructor; eauto. apply transl_lbl_stmt_2; eauto. + apply wt_seq_of_labeled_statement; auto. + destruct (Csem.find_label lbl s (Csem.Kseq (seq_of_labeled_statement l) k)) as [[s' k'] | ]. + intros [ts' [tk' [nbrk' [ncnt' [A [B [C D]]]]]]]. + rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto. + intro. rewrite H. + eapply transl_find_label_ls; eauto. Qed. -Lemma transl_Sfor_false_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a2 : Csyntax.expr) - (a3 : statement) (v : val), - Csem.eval_expr ge e m a2 v -> - is_false v (typeof a2) -> - exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) E0 m Csem.Out_normal). -Proof. - intros; red; intros. inv WT. - rewrite transl_stmt_Sfor_not_start in TR; monadInv TR. - simpl. - change Out_normal with (outcome_block (Out_exit 0)). - apply exec_Sblock. apply exec_Sloop_stop. - apply exec_Sseq_stop. eapply exit_if_false_false; eauto. - congruence. congruence. -Qed. +End FIND_LABEL. -Lemma transl_Sfor_stop_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a2 : Csyntax.expr) - (a3 : statement) (v : val) (m1 : mem) (t : trace) - (out1 out : Csem.outcome), - Csem.eval_expr ge e m a2 v -> - is_true v (typeof a2) -> - Csem.exec_stmt ge e m s t m1 out1 -> - exec_stmt_prop e m s t m1 out1 -> - out_break_or_return out1 out -> - exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) t m1 out). -Proof. - intros; red; intros. inv WT. - rewrite transl_stmt_Sfor_not_start in TR; monadInv TR. - assert (outcome_block (transl_outcome 1 0 out1) <> Out_normal). - inversion H3; simpl; congruence. - rewrite (transl_out_break_or_return _ _ nbrk ncnt H3). - apply exec_Sblock. apply exec_Sloop_stop. - eapply exec_Sseq_continue. eapply exit_if_false_true; eauto. - apply exec_Sseq_stop. apply exec_Sblock. eauto. - auto. reflexivity. auto. -Qed. +(** Properties of call continuations *) -Lemma transl_Sfor_loop_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (a2 : Csyntax.expr) - (a3 : statement) (v : val) (m1 m2 m3 : mem) (t1 t2 t3 : trace) - (out1 out : Csem.outcome), - Csem.eval_expr ge e m a2 v -> - is_true v (typeof a2) -> - Csem.exec_stmt ge e m s t1 m1 out1 -> - exec_stmt_prop e m s t1 m1 out1 -> - out_normal_or_continue out1 -> - Csem.exec_stmt ge e m1 a3 t2 m2 Csem.Out_normal -> - exec_stmt_prop e m1 a3 t2 m2 Csem.Out_normal -> - Csem.exec_stmt ge e m2 (Sfor Csyntax.Sskip a2 a3 s) t3 m3 out -> - exec_stmt_prop e m2 (Sfor Csyntax.Sskip a2 a3 s) t3 m3 out -> - exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) (t1 ** t2 ** t3) m3 out). +Lemma match_cont_call_cont: + forall nbrk' ncnt' tyenv' tyenv nbrk ncnt k tk, + match_cont tyenv nbrk ncnt k tk -> + match_cont tyenv' nbrk' ncnt' (Csem.call_cont k) (call_cont tk). Proof. - intros; red; intros. - exploit H7; eauto. intro NEXTITER. - inv WT. - rewrite transl_stmt_Sfor_not_start in TR; monadInv TR. - inversion NEXTITER; subst. - apply exec_Sblock. - eapply exec_Sloop_loop. eapply exec_Sseq_continue. - eapply exit_if_false_true; eauto. - eapply exec_Sseq_continue. - rewrite (transl_out_normal_or_continue _ H3). - apply exec_Sblock. eauto. - red in H5; simpl in H5; eauto. - reflexivity. reflexivity. eassumption. - traceEq. + induction 1; simpl; auto. + constructor. + econstructor; eauto. + econstructor; eauto. Qed. -Lemma transl_lblstmts_switch: - forall e m0 m1 n nbrk ncnt tyenv te t0 t m2 out sl body ts, - exec_stmt tprog te m0 body t0 m1 - (Out_exit (switch_target n (lblstmts_length sl) (switch_table sl 0))) -> - transl_lblstmts - (lblstmts_length sl) - (S (lblstmts_length sl + ncnt)) - sl (Sblock body) = OK ts -> - wt_lblstmts tyenv sl -> - match_env tyenv e te -> - exec_lblstmts_prop e m1 (select_switch n sl) t m2 out -> - Csharpminor.exec_stmt tprog te m0 ts (t0 ** t) m2 - (transl_outcome nbrk ncnt (outcome_switch out)). +Lemma match_cont_is_call_cont: + forall typenv nbrk ncnt k tk typenv' nbrk' ncnt', + match_cont typenv nbrk ncnt k tk -> + Csem.is_call_cont k -> + match_cont typenv' nbrk' ncnt' k tk /\ is_call_cont tk. Proof. - induction sl; intros. - simpl in H. simpl in H3. - eapply H3; eauto. - change Out_normal with (outcome_block (Out_exit 0)). - apply exec_Sblock. auto. - (* Inductive case *) - simpl in H. simpl in H3. rewrite Int.eq_sym in H3. destruct (Int.eq n i). - (* first case selected *) - eapply H3; eauto. - change Out_normal with (outcome_block (Out_exit 0)). - apply exec_Sblock. auto. - (* next case selected *) - inversion H1; clear H1; subst. - simpl in H0; monadInv H0. - eapply IHsl with (body := Sseq (Sblock body) x); eauto. - apply exec_Sseq_stop. - change (Out_exit (switch_target n (lblstmts_length sl) (switch_table sl 0))) - with (outcome_block (Out_exit (S (switch_target n (lblstmts_length sl) (switch_table sl 0))))). - apply exec_Sblock. - rewrite switch_target_table_shift in H. auto. congruence. + intros. inv H; simpl in H0; try contradiction; simpl; intuition. + constructor. + econstructor; eauto. + econstructor; eauto. Qed. -Lemma transl_Sswitch_correct: - (forall (e : Csem.env) (m : mem) (a : Csyntax.expr) (t : trace) - (n : int) (sl : labeled_statements) (m1 : mem) (out : Csem.outcome), - Csem.eval_expr ge e m a (Vint n) -> - exec_lblstmts ge e m (select_switch n sl) t m1 out -> - exec_lblstmts_prop e m (select_switch n sl) t m1 out -> - exec_stmt_prop e m (Csyntax.Sswitch a sl) t m1 (outcome_switch out)). -Proof. - intros; red; intros. - inv WT. monadInv TR. - rewrite length_switch_table in EQ0. - replace (ncnt + lblstmts_length sl + 1)%nat - with (S (lblstmts_length sl + ncnt))%nat in EQ0 by omega. - change t with (E0 ** t). eapply transl_lblstmts_switch; eauto. - constructor. eapply (transl_expr_correct _ _ _ _ MENV _ _ H); eauto. -Qed. +(** The simulation proof *) + +Lemma transl_step: + forall S1 t S2, Csem.step ge S1 t S2 -> + forall T1, match_states S1 T1 -> + exists T2, plus step tgve T1 t T2 /\ match_states S2 T2. +Proof. + induction 1; intros T1 MST; inv MST. + +(* assign *) + simpl in TR. inv WT. + case_eq (is_variable a1); intros. + rewrite H2 in TR. monadInv TR. + exploit is_variable_correct; eauto. intro EQ1. rewrite EQ1 in H. + assert (ts' = ts /\ tk' = tk). + inversion MTR. auto. + subst ts. unfold var_set in EQ0. destruct (access_mode (typeof a1)); congruence. + destruct H3; subst ts' tk'. + econstructor; split. + apply plus_one. eapply var_set_correct; eauto. congruence. + exploit transl_expr_correct; eauto. + eapply match_states_skip; eauto. + + rewrite H2 in TR. monadInv TR. + assert (ts' = ts /\ tk' = tk). + inversion MTR. auto. + subst ts. unfold make_store in EQ2. destruct (access_mode (typeof a1)); congruence. + destruct H3; subst ts' tk'. + econstructor; split. + apply plus_one. eapply make_store_correct; eauto. + exploit transl_lvalue_correct; eauto. + exploit transl_expr_correct; eauto. + eapply match_states_skip; eauto. + +(* call none *) + generalize TR. simpl. case_eq (classify_fun (typeof a)); try congruence. + intros targs tres CF TR'. monadInv TR'. inv MTR. inv WT. + exploit functions_translated; eauto. intros [tfd [FIND TFD]]. + econstructor; split. + apply plus_one. econstructor; eauto. + exploit transl_expr_correct; eauto. + exploit transl_exprlist_correct; eauto. + eapply sig_translated; eauto. congruence. + econstructor; eauto. eapply functions_well_typed; eauto. + econstructor; eauto. simpl. auto. + +(* call some *) + generalize TR. simpl. case_eq (classify_fun (typeof a)); try congruence. + intros targs tres CF TR'. monadInv TR'. inv MTR. inv WT. + exploit functions_translated; eauto. intros [tfd [FIND TFD]]. + inv H7. exploit call_dest_correct; eauto. + intros [id [A [B [C D]]]]. subst x ofs. + econstructor; split. + apply plus_one. econstructor; eauto. + exploit transl_expr_correct; eauto. + exploit transl_exprlist_correct; eauto. + eapply sig_translated; eauto. congruence. + econstructor; eauto. eapply functions_well_typed; eauto. + econstructor; eauto. simpl; auto. + +(* seq *) + monadInv TR. inv WT. inv MTR. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. constructor. + econstructor; eauto. -Lemma transl_LSdefault_correct: - (forall (e : Csem.env) (m : mem) (s : statement) (t : trace) - (m1 : mem) (out : Csem.outcome), - Csem.exec_stmt ge e m s t m1 out -> - exec_stmt_prop e m s t m1 out -> - exec_lblstmts_prop e m (LSdefault s) t m1 out). -Proof. - intros; red; intros. inv WT. monadInv TR. - replace (transl_outcome nbrk ncnt (outcome_switch out)) - with (outcome_block (transl_outcome 0 (S ncnt) out)). - constructor. - eapply exec_Sseq_continue. eauto. - eapply H0; eauto. traceEq. - destruct out; simpl; auto. -Qed. +(* skip seq *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. apply step_skip_seq. + econstructor; eauto. constructor. + +(* continue seq *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl. reflexivity. constructor. + +(* break seq *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl. reflexivity. constructor. + +(* ifthenelse true *) + monadInv TR. inv MTR. inv WT. + exploit make_boolean_correct_true; eauto. + exploit transl_expr_correct; eauto. + intros [v [A B]]. + econstructor; split. + apply plus_one. apply step_ifthenelse with (v := v) (b := true). + auto. apply Val.bool_of_true_val. auto. + econstructor; eauto. constructor. + +(* ifthenelse false *) + monadInv TR. inv MTR. inv WT. + exploit make_boolean_correct_false; eauto. + exploit transl_expr_correct; eauto. + intros [v [A B]]. + econstructor; split. + apply plus_one. apply step_ifthenelse with (v := v) (b := false). + auto. apply Val.bool_of_false_val. auto. + econstructor; eauto. constructor. + +(* while false *) + monadInv TR. inv WT. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_false; eauto. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* while true *) + monadInv TR. inv WT. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_true; eauto. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. reflexivity. traceEq. + econstructor; eauto. constructor. + econstructor; eauto. -Lemma transl_LScase_fallthrough_correct: - (forall (e : Csem.env) (m : mem) (n : int) (s : statement) - (ls : labeled_statements) (t1 : trace) (m1 : mem) (t2 : trace) - (m2 : mem) (out : Csem.outcome), - Csem.exec_stmt ge e m s t1 m1 Csem.Out_normal -> - exec_stmt_prop e m s t1 m1 Csem.Out_normal -> - exec_lblstmts ge e m1 ls t2 m2 out -> - exec_lblstmts_prop e m1 ls t2 m2 out -> - exec_lblstmts_prop e m (LScase n s ls) (t1 ** t2) m2 out). -Proof. - intros; red; intros. inv WT. monadInv TR. - assert (exec_stmt tprog te m0 (Sblock (Sseq body x)) - (t0 ** t1) m1 Out_normal). - change Out_normal with - (outcome_block (transl_outcome (S (lblstmts_length ls)) - (S (S (lblstmts_length ls + ncnt))) - Csem.Out_normal)). - apply exec_Sblock. eapply exec_Sseq_continue. eexact BODY. - eapply H0; eauto. - auto. - exploit H2. eauto. simpl; eauto. eauto. eauto. simpl. - rewrite Eapp_assoc. eauto. -Qed. +(* skip or continue while *) + assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H0. inv MK. + econstructor; split. + eapply plus_left. + destruct H0; subst ts'; constructor. + apply star_one. constructor. traceEq. + econstructor; eauto. + simpl. rewrite H5; simpl. rewrite H6; simpl. reflexivity. + constructor. constructor; auto. + +(* break while *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + eapply plus_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* dowhile *) + monadInv TR. inv WT. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. traceEq. + econstructor; eauto. constructor. + econstructor; eauto. -Lemma transl_LScase_stop_correct: - (forall (e : Csem.env) (m : mem) (n : int) (s : statement) - (ls : labeled_statements) (t : trace) (m1 : mem) - (out : Csem.outcome), - Csem.exec_stmt ge e m s t m1 out -> - exec_stmt_prop e m s t m1 out -> - out <> Csem.Out_normal -> - exec_lblstmts_prop e m (LScase n s ls) t m1 out). -Proof. - intros; red; intros. inv WT. monadInv TR. - exploit H0; eauto. intro EXEC. - destruct out; simpl; simpl in EXEC. - (* out = Out_break *) - change Out_normal with (outcome_block (Out_exit 0)). - eapply transl_lblstmts_exit with (body := Sblock (Sseq body x)); eauto. - rewrite plus_0_r. - change (Out_exit (lblstmts_length ls)) - with (outcome_block (Out_exit (S (lblstmts_length ls)))). - constructor. eapply exec_Sseq_continue; eauto. - (* out = Out_continue *) - change (Out_exit ncnt) with (outcome_block (Out_exit (S ncnt))). - eapply transl_lblstmts_exit with (body := Sblock (Sseq body x)); eauto. - replace (Out_exit (lblstmts_length ls + S ncnt)) - with (outcome_block (Out_exit (S (S (lblstmts_length ls + ncnt))))). - constructor. eapply exec_Sseq_continue; eauto. - simpl. decEq. omega. - (* out = Out_normal *) - congruence. - (* out = Out_return *) - eapply transl_lblstmts_return with (body := Sblock (Sseq body x)); eauto. - change (Out_return o) - with (outcome_block (Out_return o)). - constructor. eapply exec_Sseq_continue; eauto. -Qed. +(* skip or continue dowhile false *) + assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H2. inv MK. + econstructor; split. + eapply plus_left. destruct H2; subst ts'; constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_false; eauto. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* skip or continue dowhile true *) + assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H2. inv MK. + econstructor; split. + eapply plus_left. destruct H2; subst ts'; constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_true; eauto. + apply star_one. constructor. + reflexivity. reflexivity. traceEq. + econstructor; eauto. + simpl. rewrite H7; simpl. rewrite H8; simpl. reflexivity. constructor. + constructor; auto. -Remark outcome_result_value_match: - forall out ty v nbrk ncnt, - Csem.outcome_result_value out ty v -> - Csharpminor.outcome_result_value (transl_outcome nbrk ncnt out) (opttyp_of_type ty) v. -Proof. - intros until ncnt. - destruct out; simpl; try contradiction. - destruct ty; simpl; auto. - destruct o. intros [A B]. destruct ty; simpl; congruence. - destruct ty; simpl; auto. -Qed. +(* break dowhile *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* for start *) + simpl in TR. rewrite is_Sskip_false in TR; auto. monadInv TR. inv MTR. inv WT. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. constructor. + constructor; auto. simpl. rewrite is_Sskip_true. rewrite EQ1; simpl. rewrite EQ0; simpl. rewrite EQ2; auto. + constructor; auto. constructor. + +(* for false *) + simpl in TR. rewrite is_Sskip_true in TR. monadInv TR. inv WT. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_false; eauto. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. + eapply match_states_skip; eauto. + +(* for true *) + simpl in TR. rewrite is_Sskip_true in TR. monadInv TR. inv WT. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. eapply exit_if_false_true; eauto. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. + econstructor; eauto. constructor. + econstructor; eauto. + +(* skip or continue for2 *) + assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H0. inv MK. + econstructor; split. + eapply plus_left. destruct H0; subst ts'; constructor. + apply star_one. constructor. reflexivity. + econstructor; eauto. constructor. + constructor; auto. + +(* break for2 *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + eapply plus_left. constructor. + eapply star_left. constructor. + eapply star_left. constructor. + apply star_one. constructor. + reflexivity. reflexivity. traceEq. + eapply match_states_skip; eauto. + +(* skip for3 *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. + simpl. rewrite is_Sskip_true. rewrite H3; simpl. rewrite H4; simpl. rewrite H5; simpl. reflexivity. + constructor. constructor; auto. + +(* return none *) + monadInv TR. inv MTR. + econstructor; split. + apply plus_one. constructor. monadInv TRF. simpl. rewrite H. auto. + rewrite (match_env_free_blocks _ _ _ m MENV). econstructor; eauto. + eapply match_cont_call_cont. eauto. + +(* return some *) + monadInv TR. inv MTR. inv WT. inv H2. + econstructor; split. + apply plus_one. constructor. monadInv TRF. simpl. + unfold opttyp_of_type. destruct (fn_return f); congruence. + exploit transl_expr_correct; eauto. + rewrite (match_env_free_blocks _ _ _ m MENV). econstructor; eauto. + eapply match_cont_call_cont. eauto. + +(* skip call *) + monadInv TR. inv MTR. + exploit match_cont_is_call_cont; eauto. intros [A B]. + econstructor; split. + apply plus_one. apply step_skip_call. auto. + monadInv TRF. simpl. rewrite H0. auto. + rewrite (match_env_free_blocks _ _ _ m MENV). constructor. eauto. + +(* switch *) + monadInv TR. inv WT. + exploit transl_expr_correct; eauto. intro EV. + econstructor; split. + eapply star_plus_trans. eapply match_transl_step; eauto. + apply plus_one. econstructor. eauto. traceEq. + econstructor; eauto. + apply transl_lbl_stmt_2. apply transl_lbl_stmt_1. eauto. + constructor. + apply wt_seq_of_labeled_statement. apply wt_select_switch. auto. + econstructor. eauto. + +(* skip or break switch *) + assert ((ts' = Sskip \/ ts' = Sexit nbrk) /\ tk' = tk). + destruct H; subst x; monadInv TR; inv MTR; auto. + destruct H0. inv MK. + econstructor; split. + apply plus_one. destruct H0; subst ts'; constructor. + eapply match_states_skip; eauto. + + +(* continue switch *) + monadInv TR. inv MTR. inv MK. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. simpl. reflexivity. constructor. + +(* label *) + monadInv TR. inv WT. inv MTR. + econstructor; split. + apply plus_one. constructor. + econstructor; eauto. constructor. + +(* goto *) + monadInv TR. inv MTR. + generalize TRF. unfold transl_function. intro TRF'. monadInv TRF'. + exploit (transl_find_label lbl). eexact WTF. eexact EQ0. eapply match_cont_call_cont. eauto. + rewrite H. + intros [ts' [tk'' [nbrk' [ncnt' [A [B [C D]]]]]]]. + econstructor; split. + apply plus_one. constructor. simpl. eexact A. + econstructor; eauto. constructor. + +(* internal function *) + monadInv TR. inv WT. inv H3. monadInv EQ. + exploit match_cont_is_call_cont; eauto. intros [A B]. + exploit match_env_alloc_variables; eauto. + apply match_globalenv_match_env_empty. apply match_global_typenv. + apply transl_fn_variables. eauto. eauto. + intros [te1 [C D]]. + econstructor; split. + apply plus_one. econstructor. + eapply transl_names_norepet; eauto. + eexact C. eapply bind_parameters_match; eauto. + econstructor; eauto. + unfold transl_function. rewrite EQ0; simpl. rewrite EQ; simpl. rewrite EQ1; auto. + constructor. -Lemma transl_funcall_internal_correct: - (forall (m : mem) (f : Csyntax.function) (vargs : list val) - (t : trace) (e : Csem.env) (m1 : mem) (lb : list block) - (m2 m3 : mem) (out : Csem.outcome) (vres : val), - Csem.alloc_variables Csem.empty_env m - (Csyntax.fn_params f ++ Csyntax.fn_vars f) e m1 lb -> - Csem.bind_parameters e m1 (Csyntax.fn_params f) vargs m2 -> - Csem.exec_stmt ge e m2 (Csyntax.fn_body f) t m3 out -> - exec_stmt_prop e m2 (Csyntax.fn_body f) t m3 out -> - Csem.outcome_result_value out (fn_return f) vres -> - eval_funcall_prop m (Internal f) vargs t (free_list m3 lb) vres). -Proof. - intros; red; intros. - (* Exploitation of typing hypothesis *) - inv WT. inv H6. - (* Exploitation of translation hypothesis *) +(* external function *) monadInv TR. - monadInv EQ. - (* Allocation of variables *) - exploit match_env_alloc_variables; eauto. - apply match_globalenv_match_env_empty. - apply match_global_typenv. - eexact (transl_fn_variables _ _ (signature_of_function f) _ _ x2 EQ0 EQ). - intros [te [ALLOCVARS MATCHENV]]. - (* Execution *) - econstructor; simpl. - (* Norepet *) - eapply transl_names_norepet; eauto. - (* Alloc *) - eexact ALLOCVARS. - (* Bind *) - eapply bind_parameters_match; eauto. - (* Execution of body *) - eapply H2; eauto. - (* Outcome_result_value *) - apply outcome_result_value_match; auto. -Qed. + exploit match_cont_is_call_cont; eauto. intros [A B]. + econstructor; split. + apply plus_one. constructor. eauto. + econstructor; eauto. -Lemma transl_funcall_external_correct: - (forall (m : mem) (id : ident) (targs : typelist) (tres : type) - (vargs : list val) (t : trace) (vres : val), - event_match (external_function id targs tres) vargs t vres -> - eval_funcall_prop m (External id targs tres) vargs t m vres). -Proof. - intros; red; intros. - monadInv TR. constructor. auto. +(* returnstate 0 *) + inv MK. + econstructor; split. + apply plus_one. constructor. constructor. + econstructor; eauto. simpl; reflexivity. constructor. constructor. + +(* returnstate 1 *) + inv MK. + econstructor; split. + apply plus_one. constructor. eapply set_call_dest_correct; eauto. + econstructor; eauto. simpl; reflexivity. constructor. constructor. +Qed. + +Lemma transl_initial_states: + forall S t S', Csem.initial_state prog S -> Csem.step ge S t S' -> + exists R, initial_state tprog R /\ match_states S R. +Proof. + intros. inv H. + exploit function_ptr_translated; eauto. intros [tf [A B]]. + assert (C: Genv.find_symbol tge (prog_main tprog) = Some b). + rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog). + exact H1. symmetry. unfold transl_program in TRANSL. + eapply transform_partial_program2_main; eauto. + exploit function_ptr_well_typed. eauto. intro WTF. + assert (exists targs, type_of_fundef f = Tfunction targs (Tint I32 Signed)). + eapply wt_program_main. eauto. + eapply Genv.find_funct_ptr_symbol_inversion; eauto. + destruct H as [targs D]. + assert (targs = Tnil). + inv H0. inv H9. simpl in D. unfold type_of_function in D. rewrite <- H4 in D. + simpl in D. congruence. + simpl in D. inv D. inv H8. inv H. + destruct targs; simpl in H5; congruence. + subst targs. + assert (funsig tf = signature_of_type Tnil (Tint I32 Signed)). + eapply sig_translated; eauto. rewrite D; auto. + econstructor; split. + econstructor; eauto. + rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog TRANSL). + constructor; auto. constructor. exact I. Qed. -Theorem transl_funcall_correct: - forall (m : mem) (f : Csyntax.fundef) (l : list val) (t : trace) - (m0 : mem) (v : val), - Csem.eval_funcall ge m f l t m0 v -> - eval_funcall_prop m f l t m0 v. -Proof - (Csem.eval_funcall_ind3 ge - exec_stmt_prop - exec_lblstmts_prop - eval_funcall_prop - - transl_Sskip_correct - transl_Sassign_correct - transl_Scall_None_correct - transl_Scall_Some_correct - transl_Ssequence_1_correct - transl_Ssequence_2_correct - transl_Sifthenelse_true_correct - transl_Sifthenelse_false_correct - transl_Sreturn_none_correct - transl_Sreturn_some_correct - transl_Sbreak_correct - transl_Scontinue_correct - transl_Swhile_false_correct - transl_Swhile_stop_correct - transl_Swhile_loop_correct - transl_Sdowhile_false_correct - transl_Sdowhile_stop_correct - transl_Sdowhile_loop_correct - transl_Sfor_start_correct - transl_Sfor_false_correct - transl_Sfor_stop_correct - transl_Sfor_loop_correct - transl_Sswitch_correct - transl_LSdefault_correct - transl_LScase_fallthrough_correct - transl_LScase_stop_correct - transl_funcall_internal_correct - transl_funcall_external_correct). - -Theorem transl_stmt_correct: - forall (e: Csem.env) (m1: mem) (s: Csyntax.statement) (t: trace) - (m2: mem) (out: Csem.outcome), - Csem.exec_stmt ge e m1 s t m2 out -> - exec_stmt_prop e m1 s t m2 out. -Proof - (Csem.exec_stmt_ind3 ge - exec_stmt_prop - exec_lblstmts_prop - eval_funcall_prop - - transl_Sskip_correct - transl_Sassign_correct - transl_Scall_None_correct - transl_Scall_Some_correct - transl_Ssequence_1_correct - transl_Ssequence_2_correct - transl_Sifthenelse_true_correct - transl_Sifthenelse_false_correct - transl_Sreturn_none_correct - transl_Sreturn_some_correct - transl_Sbreak_correct - transl_Scontinue_correct - transl_Swhile_false_correct - transl_Swhile_stop_correct - transl_Swhile_loop_correct - transl_Sdowhile_false_correct - transl_Sdowhile_stop_correct - transl_Sdowhile_loop_correct - transl_Sfor_start_correct - transl_Sfor_false_correct - transl_Sfor_stop_correct - transl_Sfor_loop_correct - transl_Sswitch_correct - transl_LSdefault_correct - transl_LScase_fallthrough_correct - transl_LScase_stop_correct - transl_funcall_internal_correct - transl_funcall_external_correct). - -(** ** Semantic preservation for divergence *) - -Lemma transl_funcall_divergence_correct: - forall m1 f params t tf, - Csem.evalinf_funcall ge m1 f params t -> - wt_fundef (global_typenv prog) f -> - transl_fundef f = OK tf -> - Csharpminor.evalinf_funcall tprog m1 tf params t - -with transl_stmt_divergence_correct: - forall e m1 s t, - Csem.execinf_stmt ge e m1 s t -> - forall tyenv nbrk ncnt ts te - (WT: wt_stmt tyenv s) - (TR: transl_statement nbrk ncnt s = OK ts) - (MENV: match_env tyenv e te), - Csharpminor.execinf_stmt tprog te m1 ts t - -with transl_lblstmt_divergence_correct: - forall s ncnt body ts tyenv e te m0 t0 m1 t1 n, - transl_lblstmts (lblstmts_length s) - (S (lblstmts_length s + ncnt)) - s body = OK ts -> - wt_lblstmts tyenv s -> - match_env tyenv e te -> - (exec_stmt tprog te m0 body t0 m1 - (outcome_block (Out_exit - (switch_target n (lblstmts_length s) (switch_table s 0)))) - /\ execinf_lblstmts ge e m1 (select_switch n s) t1) - \/ (exec_stmt tprog te m0 body t0 m1 Out_normal - /\ execinf_lblstmts ge e m1 s t1) -> - execinf_stmt_N tprog (lblstmts_length s) te m0 ts (t0 *** t1). - +Lemma transl_final_states: + forall S R r, + match_states S R -> Csem.final_state S r -> final_state R r. Proof. - (* Functions *) - intros. inv H. - (* Exploitation of typing hypothesis *) - inv H0. inv H6. - (* Exploitation of translation hypothesis *) - monadInv H1. monadInv EQ. - (* Allocation of variables *) - assert (match_env (global_typenv prog) Csem.empty_env Csharpminor.empty_env). - apply match_globalenv_match_env_empty. apply match_global_typenv. - generalize (transl_fn_variables _ _ (signature_of_function f0) _ _ x2 EQ0 EQ). - intro. - destruct (match_env_alloc_variables _ _ _ _ _ _ H2 _ _ _ H1 H5) - as [te [ALLOCVARS MATCHENV]]. - (* Execution *) - econstructor; simpl. - eapply transl_names_norepet; eauto. - eexact ALLOCVARS. - eapply bind_parameters_match; eauto. - eapply transl_stmt_divergence_correct; eauto. - -(* Statements *) - - intros. inv H; inv WT; try (generalize TR; intro TR'; monadInv TR'). - (* Scall *) - simpl in TR. - caseEq (classify_fun (typeof a)); intros; rewrite H in TR; monadInv TR. - destruct (functions_translated _ _ H2) as [tf [TFIND TFD]]. - eapply execinf_Scall. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. - eapply (transl_exprlist_correct _ _ _ _ MENV _ _ H1); eauto. - eauto. - eapply transl_fundef_sig1; eauto. rewrite H3; auto. - eapply transl_funcall_divergence_correct; eauto. - eapply functions_well_typed; eauto. - (* Sseq 1 *) - apply execinf_Sseq_1. eapply transl_stmt_divergence_correct; eauto. - (* Sseq 2 *) - eapply execinf_Sseq_2. - change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal). - eapply (transl_stmt_correct _ _ _ _ _ _ H0); eauto. - eapply transl_stmt_divergence_correct; eauto. auto. - (* Sifthenelse, true *) - assert (eval_expr tprog te m1 x v1). - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. - destruct (make_boolean_correct_true _ _ _ _ _ _ H H1) as [vb [A B]]. - eapply execinf_Sifthenelse. eauto. apply Val.bool_of_true_val; eauto. - auto. eapply transl_stmt_divergence_correct; eauto. - (* Sifthenelse, false *) - assert (eval_expr tprog te m1 x v1). - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. - destruct (make_boolean_correct_false _ _ _ _ _ _ H H1) as [vb [A B]]. - eapply execinf_Sifthenelse. eauto. apply Val.bool_of_false_val; eauto. - auto. eapply transl_stmt_divergence_correct; eauto. - (* Swhile, body *) - apply execinf_Sblock. apply execinf_Sloop_body. - eapply execinf_Sseq_2. eapply exit_if_false_true; eauto. - apply execinf_Sblock. eapply transl_stmt_divergence_correct; eauto. traceEq. - (* Swhile, loop *) - apply execinf_Sblock. eapply execinf_Sloop_block. - eapply exec_Sseq_continue. eapply exit_if_false_true; eauto. - rewrite (transl_out_normal_or_continue out1 H3). - apply exec_Sblock. - eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto. reflexivity. - eapply transl_stmt_divergence_correct with (nbrk := 1%nat) (ncnt := 0%nat); eauto. - constructor; eauto. - traceEq. - (* Sdowhile, body *) - apply execinf_Sblock. apply execinf_Sloop_body. - apply execinf_Sseq_1. apply execinf_Sblock. - eapply transl_stmt_divergence_correct; eauto. - (* Sdowhile, loop *) - apply execinf_Sblock. eapply execinf_Sloop_block. - eapply exec_Sseq_continue. - rewrite (transl_out_normal_or_continue out1 H1). - apply exec_Sblock. - eapply (transl_stmt_correct _ _ _ _ _ _ H0); eauto. - eapply exit_if_false_true; eauto. reflexivity. - eapply transl_stmt_divergence_correct with (nbrk := 1%nat) (ncnt := 0%nat); eauto. - constructor; auto. - traceEq. - (* Sfor start 1 *) - simpl in TR. destruct (is_Sskip a1). - subst a1. inv H0. - monadInv TR. - apply execinf_Sseq_1. eapply transl_stmt_divergence_correct; eauto. - (* Sfor start 2 *) - destruct (transl_stmt_Sfor_start _ _ _ _ _ _ _ TR H0) as [ts1 [ts2 [EQ [TR1 TR2]]]]. - subst ts. - eapply execinf_Sseq_2. - change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal). - eapply (transl_stmt_correct _ _ _ _ _ _ H1); eauto. - eapply transl_stmt_divergence_correct; eauto. - constructor; auto. constructor. - auto. - (* Sfor_body *) - rewrite transl_stmt_Sfor_not_start in TR; monadInv TR. - apply execinf_Sblock. apply execinf_Sloop_body. - eapply execinf_Sseq_2. - eapply exit_if_false_true; eauto. - apply execinf_Sseq_1. apply execinf_Sblock. - eapply transl_stmt_divergence_correct; eauto. - traceEq. - (* Sfor next *) - rewrite transl_stmt_Sfor_not_start in TR; monadInv TR. - apply execinf_Sblock. apply execinf_Sloop_body. - eapply execinf_Sseq_2. - eapply exit_if_false_true; eauto. - eapply execinf_Sseq_2. - rewrite (transl_out_normal_or_continue out1 H3). - apply exec_Sblock. - eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto. - eapply transl_stmt_divergence_correct; eauto. - reflexivity. traceEq. - (* Sfor loop *) - generalize TR. rewrite transl_stmt_Sfor_not_start; intro TR'; monadInv TR'. - apply execinf_Sblock. eapply execinf_Sloop_block. - eapply exec_Sseq_continue. - eapply exit_if_false_true; eauto. - eapply exec_Sseq_continue. - rewrite (transl_out_normal_or_continue out1 H3). - apply exec_Sblock. - eapply (transl_stmt_correct _ _ _ _ _ _ H2); eauto. - change Out_normal with (transl_outcome nbrk ncnt Csem.Out_normal). - eapply (transl_stmt_correct _ _ _ _ _ _ H4); eauto. - reflexivity. reflexivity. - eapply transl_stmt_divergence_correct; eauto. - constructor; auto. - traceEq. - (* Sswitch *) - apply execinf_stutter with (lblstmts_length sl). - rewrite length_switch_table in EQ0. - replace (ncnt + lblstmts_length sl + 1)%nat - with (S (lblstmts_length sl + ncnt))%nat in EQ0 by omega. - change t with (E0 *** t). - eapply transl_lblstmt_divergence_correct; eauto. - left. split. apply exec_Sblock. constructor. - eapply (transl_expr_correct _ _ _ _ MENV _ _ H0); eauto. - auto. - -(* Labeled statements *) - intros. destruct s; simpl in *; monadInv H; inv H0. - (* 1. LSdefault *) - assert (exec_stmt tprog te m0 body t0 m1 Out_normal) by tauto. - assert (execinf_lblstmts ge e m1 (LSdefault s) t1) by tauto. - clear H2. inv H0. - change (Sblock (Sseq body x)) - with ((fun z => Sblock z) (Sseq body x)). - apply execinf_context. - eapply execinf_Sseq_2. eauto. eapply transl_stmt_divergence_correct; eauto. auto. - constructor. - (* 2. LScase *) - elim H2; clear H2. - (* 2.1 searching for the case *) - rewrite (Int.eq_sym i n). - destruct (Int.eq n i). - (* 2.1.1 found it! *) - intros [A B]. inv B. - (* 2.1.1.1 we diverge because of this case *) - destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]]. - rewrite EQ1. apply execinf_context; auto. - apply execinf_Sblock. eapply execinf_Sseq_2. eauto. - eapply transl_stmt_divergence_correct; eauto. auto. - (* 2.1.1.2 we diverge later, after falling through *) - simpl. apply execinf_sleep. - replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3). - eapply transl_lblstmt_divergence_correct with (n := n); eauto. right. split. - change Out_normal with (outcome_block Out_normal). - apply exec_Sblock. - eapply exec_Sseq_continue. eauto. - change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal). - eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto. - auto. auto. traceEq. - (* 2.1.2 still searching *) - rewrite switch_target_table_shift. intros [A B]. - apply execinf_sleep. - eapply transl_lblstmt_divergence_correct with (n := n); eauto. left. split. - fold (outcome_block (Out_exit (switch_target n (lblstmts_length s0) (switch_table s0 0)))). - apply exec_Sblock. apply exec_Sseq_stop. eauto. congruence. - auto. - (* 2.2 found the case already, falling through next cases *) - intros [A B]. inv B. - (* 2.2.1 we diverge because of this case *) - destruct (transl_lblstmts_context _ _ _ _ _ EQ0) as [ctx [CTX EQ1]]. - rewrite EQ1. apply execinf_context; auto. - apply execinf_Sblock. eapply execinf_Sseq_2. eauto. - eapply transl_stmt_divergence_correct; eauto. auto. - (* 2.2.2 we diverge later *) - simpl. apply execinf_sleep. - replace (t0 *** t2 *** t3) with ((t0 ** t2) *** t3). - eapply transl_lblstmt_divergence_correct with (n := n); eauto. right. split. - change Out_normal with (outcome_block Out_normal). - apply exec_Sblock. - eapply exec_Sseq_continue. eauto. - change Out_normal with (transl_outcome (S (lblstmts_length s0)) (S (S (lblstmts_length s0 + ncnt))) Csem.Out_normal). - eapply (transl_stmt_correct _ _ _ _ _ _ H8); eauto. - auto. auto. traceEq. + intros. inv H0. inv H. inv MK. constructor. Qed. -End CORRECTNESS. - -(** Semantic preservation for whole programs. *) - Theorem transl_program_correct: - forall prog tprog beh, - transl_program prog = OK tprog -> - Ctyping.wt_program prog -> + forall (beh: program_behavior), Csem.exec_program prog beh -> Csharpminor.exec_program tprog beh. Proof. - intros. inversion H0; subst. inv H1. - (* Termination *) - assert (exists targs, type_of_fundef f = Tfunction targs (Tint I32 Signed)). - apply wt_program_main. - eapply Genv.find_funct_ptr_symbol_inversion; eauto. - elim H1; clear H1; intros targs TYP. - assert (targs = Tnil). - inv H4; simpl in TYP. - inv H5. injection TYP. rewrite <- H10. simpl. auto. - inv TYP. inv H1. - destruct targs; simpl in H4. auto. inv H4. - subst targs. - exploit function_ptr_translated; eauto. intros [tf [TFINDF TRANSLFD]]. - apply program_terminates with b tf m1. - rewrite (symbols_preserved _ _ H). - rewrite (transform_partial_program2_main transl_fundef transl_globvar prog H). auto. - auto. - generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD TYP). simpl; auto. - rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog H). - generalize (transl_funcall_correct _ _ H0 H _ _ _ _ _ _ H4). - intro. eapply H1. - eapply function_ptr_well_typed; eauto. - auto. - (* Divergence *) - assert (exists targs, type_of_fundef f = Tfunction targs (Tint I32 Signed)). - apply wt_program_main. - eapply Genv.find_funct_ptr_symbol_inversion; eauto. - elim H1; clear H1; intros targs TYP. - assert (targs = Tnil). - inv H4; simpl in TYP. - inv H5. injection TYP. rewrite <- H9. simpl. auto. - subst targs. - exploit function_ptr_translated; eauto. intros [tf [TFINDF TRANSLFD]]. - apply program_diverges with b tf. - rewrite (symbols_preserved _ _ H). - rewrite (transform_partial_program2_main transl_fundef transl_globvar prog H). auto. - auto. - generalize (transl_fundef_sig2 _ _ _ _ TRANSLFD TYP). simpl; auto. - rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog H). - eapply transl_funcall_divergence_correct; eauto. - eapply function_ptr_well_typed; eauto. + set (order := fun (S1 S2: Csem.state) => False). + assert (transl_step': + forall S1 t S2, Csem.step ge S1 t S2 -> + forall T1, match_states S1 T1 -> + exists T2, + (plus step tgve T1 t T2 \/ star step tgve T1 t T2 /\ order S2 S1) + /\ match_states S2 T2). + intros. exploit transl_step; eauto. intros [T2 [A B]]. + exists T2; split. auto. auto. + intros. inv H. + assert (exists t1, exists s1, Csem.step (Genv.globalenv prog) s t1 s1). + inv H1. inv H0; inv H2. exists t1; exists s2; auto. + destruct H as [t1 [s1 ST]]. + exploit transl_initial_states; eauto. intros [R [A B]]. + exploit simulation_star_star; eauto. intros [R' [C D]]. + econstructor; eauto. eapply transl_final_states; eauto. + assert (exists t1, exists s1, Csem.step (Genv.globalenv prog) s t1 s1). + inv H1. exists t; exists s2; auto. + destruct H as [t1 [s1 ST]]. + exploit transl_initial_states; eauto. intros [R [A B]]. + exploit simulation_star_forever; eauto. + unfold order; red. intros. constructor; intros. contradiction. + intro C. + econstructor; eauto. Qed. + +End CORRECTNESS. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index b332e21..f66b5be 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -163,11 +163,13 @@ Definition typeof (e: expr) : type := (** ** Statements *) -(** Clight statements include all C statements except [goto] and labels. +(** Clight statements include all C statements. Only structured forms of [switch] are supported; moreover, the [default] case must occur last. Blocks and block-scoped declarations are not supported. *) +Definition label := ident. + Inductive statement : Type := | Sskip : statement (**r do nothing *) | Sassign : expr -> expr -> statement (**r assignment [lvalue = rvalue] *) @@ -181,6 +183,8 @@ Inductive statement : Type := | Scontinue : statement (**r [continue] statement *) | Sreturn : option expr -> statement (**r [return] statement *) | Sswitch : expr -> labeled_statements -> statement (**r [switch] statement *) + | Slabel : label -> statement -> statement + | Sgoto : label -> statement with labeled_statements : Type := (**r cases of a [switch] *) | LSdefault: statement -> labeled_statements @@ -447,6 +451,9 @@ type must be accessed: - [By_reference]: access by reference, i.e. by just returning the address of the variable; - [By_nothing]: no access is possible, e.g. for the [void] type. + +We currently do not support 64-bit integers and 128-bit floats, so these +have an access mode of [By_nothing]. *) Inductive mode: Type := diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v index c03552c..2bb9a9d 100644 --- a/cfrontend/Ctyping.v +++ b/cfrontend/Ctyping.v @@ -120,6 +120,11 @@ Inductive wt_stmt: statement -> Prop := | wt_Sswitch: forall e sl, wt_expr e -> wt_lblstmts sl -> wt_stmt (Sswitch e sl) + | wt_Slabel: forall lbl s, + wt_stmt s -> + wt_stmt (Slabel lbl s) + | wt_Sgoto: forall lbl, + wt_stmt (Sgoto lbl) with wt_lblstmts: labeled_statements -> Prop := | wt_LSdefault: forall s, @@ -362,6 +367,8 @@ Fixpoint typecheck_stmt (s: Csyntax.statement) {struct s} : bool := | Csyntax.Sreturn (Some e) => typecheck_expr e | Csyntax.Sreturn None => true | Csyntax.Sswitch e sl => typecheck_expr e && typecheck_lblstmts sl + | Csyntax.Slabel lbl s => typecheck_stmt s + | Csyntax.Sgoto lbl => true end with typecheck_lblstmts (sl: labeled_statements) {struct sl}: bool := -- cgit v1.2.3