From 1b35564dcf300e1a007d14529996286b538b5f81 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 11 Jul 2006 11:56:28 +0000 Subject: Revu sémantique de Eaddrof en Csharpminor: on peut prendre l'adresse de globaux qui ne sont pas déclarés dans les variables du programme, notamment les fonctions. Adaptation de Cminorgen et de sa preuve en conséquence. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@47 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Cminorgen.v | 47 +++++----- backend/Cminorgenproof.v | 223 ++++++++++++++++++++--------------------------- backend/Csharpminor.v | 44 +++++++--- 3 files changed, 149 insertions(+), 165 deletions(-) (limited to 'backend') diff --git a/backend/Cminorgen.v b/backend/Cminorgen.v index e4c9a424..cb889928 100644 --- a/backend/Cminorgen.v +++ b/backend/Cminorgen.v @@ -139,42 +139,41 @@ Inductive var_info: Set := | Var_global_scalar: memory_chunk -> var_info | Var_global_array: var_info. -Definition compilenv := PTree.t var_info. +Definition compilenv := PMap.t var_info. (** Generation of Cminor code corresponding to accesses to Csharpminor local variables: reads, assignments, and taking the address of. *) Definition var_get (cenv: compilenv) (id: ident): option expr := - match PTree.get id cenv with - | Some(Var_local chunk) => + match PMap.get id cenv with + | Var_local chunk => Some(Evar id) - | Some(Var_stack_scalar chunk ofs) => + | Var_stack_scalar chunk ofs => Some(make_load chunk (make_stackaddr ofs)) - | Some(Var_global_scalar chunk) => + | Var_global_scalar chunk => Some(make_load chunk (make_globaladdr id)) | _ => None end. Definition var_set (cenv: compilenv) (id: ident) (rhs: expr): option expr := - match PTree.get id cenv with - | Some(Var_local chunk) => + match PMap.get id cenv with + | Var_local chunk => Some(Eassign id (make_cast chunk rhs)) - | Some(Var_stack_scalar chunk ofs) => + | Var_stack_scalar chunk ofs => Some(make_store chunk (make_stackaddr ofs) rhs) - | Some(Var_global_scalar chunk) => + | Var_global_scalar chunk => Some(make_store chunk (make_globaladdr id) rhs) | _ => None end. Definition var_addr (cenv: compilenv) (id: ident): option expr := - match PTree.get id cenv with - | Some(Var_stack_scalar chunk ofs) => Some (make_stackaddr ofs) - | Some(Var_stack_array ofs) => Some (make_stackaddr ofs) - | Some(Var_global_scalar chunk) => Some (make_globaladdr id) - | Some(Var_global_array) => Some (make_globaladdr id) - | _ => None + match PMap.get id cenv with + | Var_local chunk => None + | Var_stack_scalar chunk ofs => Some (make_stackaddr ofs) + | Var_stack_array ofs => Some (make_stackaddr ofs) + | _ => Some (make_globaladdr id) end. (** The translation from Csharpminor to Cminor can fail, which we @@ -334,14 +333,14 @@ Definition assign_variable match id_lv with | (id, Varray sz) => let ofs := align stacksize 8 in - (PTree.set id (Var_stack_array ofs) cenv, ofs + Zmax 0 sz) + (PMap.set id (Var_stack_array ofs) cenv, ofs + Zmax 0 sz) | (id, Vscalar chunk) => if Identset.mem id atk then let sz := Mem.size_chunk chunk in let ofs := align stacksize sz in - (PTree.set id (Var_stack_scalar chunk ofs) cenv, ofs + sz) + (PMap.set id (Var_stack_scalar chunk ofs) cenv, ofs + sz) else - (PTree.set id (Var_local chunk) cenv, stacksize) + (PMap.set id (Var_local chunk) cenv, stacksize) end. Fixpoint assign_variables @@ -365,13 +364,13 @@ Definition build_compilenv Definition assign_global_variable (ce: compilenv) (id_vi: ident * var_kind) : compilenv := match id_vi with - | (id, Vscalar chunk) => PTree.set id (Var_global_scalar chunk) ce - | (id, Varray sz) => PTree.set id Var_global_array ce + | (id, Vscalar chunk) => PMap.set id (Var_global_scalar chunk) ce + | (id, Varray sz) => PMap.set id Var_global_array ce end. Definition build_global_compilenv (p: Csharpminor.program) : compilenv := List.fold_left assign_global_variable - p.(prog_vars) (PTree.empty var_info). + p.(prog_vars) (PMap.init Var_global_array). (** Function parameters whose address is taken must be stored in their stack slots at function entry. (Cminor passes these parameters in @@ -383,11 +382,11 @@ Fixpoint store_parameters match params with | nil => Sskip | (id, chunk) :: rem => - match PTree.get id cenv with - | Some(Var_local chunk) => + match PMap.get id cenv with + | Var_local chunk => Sseq (Sexpr (Eassign id (make_cast chunk (Evar id)))) (store_parameters cenv rem) - | Some(Var_stack_scalar chunk ofs) => + | Var_stack_scalar chunk ofs => Sseq (Sexpr (make_store chunk (make_stackaddr ofs) (Evar id))) (store_parameters cenv rem) | _ => diff --git a/backend/Cminorgenproof.v b/backend/Cminorgenproof.v index e6218a84..7b3bc9bb 100644 --- a/backend/Cminorgenproof.v +++ b/backend/Cminorgenproof.v @@ -61,43 +61,35 @@ Proof. intros [A B]. elim B. reflexivity. Qed. -Definition var_info_global (id: ident) (vi: var_info) (lv: var_kind) := - match vi with - | Var_global_scalar chunk => lv = Vscalar chunk - | Var_global_array => exists sz, lv = Varray sz +Definition global_compilenv_match (ce: compilenv) (gv: gvarenv) : Prop := + forall id, + match ce!!id with + | Var_global_scalar chunk => gv!id = Some (Vscalar chunk) + | Var_global_array => True | _ => False end. Lemma global_compilenv_charact: - forall id vi, gce!id = Some vi -> - exists lv, (global_var_env prog)!id = Some lv /\ var_info_global id vi lv. + global_compilenv_match gce (global_var_env prog). Proof. set (mkgve := fun gv vars => List.fold_left (fun gv (id_vi: ident * var_kind) => PTree.set (fst id_vi) (snd id_vi) gv) vars gv). assert (forall vars gv ce, - (forall id vi, ce!id = Some vi -> - exists lv, gv!id = Some lv /\ var_info_global id vi lv) -> - (forall id vi, - (List.fold_left assign_global_variable vars ce)!id = Some vi -> - exists lv, (mkgve gv vars)!id = Some lv /\ var_info_global id vi lv)). + global_compilenv_match ce gv -> + global_compilenv_match (List.fold_left assign_global_variable vars ce) + (mkgve gv vars)). induction vars; simpl; intros. - eauto. - apply IHvars with (assign_global_variable ce a); auto. - intros until vi0. unfold assign_global_variable. destruct a as [id1 vi1]. - simpl. destruct vi1. - repeat rewrite PTree.gsspec. case (peq id0 id1); intros. - inversion H1. exists (Vscalar m). split. auto. red; auto. - eauto. - repeat rewrite PTree.gsspec. case (peq id0 id1); intros. - inversion H1. exists (Varray z). split. auto. red. exists z; auto. - eauto. + auto. + apply IHvars. intro id1. unfold assign_global_variable. + destruct a as [id2 lv2]. destruct lv2; simpl; rewrite PMap.gsspec; rewrite PTree.gsspec. + case (peq id1 id2); intro. auto. apply H. + case (peq id1 id2); intro. auto. apply H. - intros. change (global_var_env prog) with (mkgve (PTree.empty var_kind) prog.(Csharpminor.prog_vars)). - apply H with (PTree.empty var_info). - intros until vi0. rewrite PTree.gempty. congruence. - exact H0. + change (global_var_env prog) with (mkgve (PTree.empty var_kind) prog.(Csharpminor.prog_vars)). + unfold gce, build_global_compilenv. apply H. + intro. rewrite PMap.gi. auto. Qed. (** * Correspondence between Csharpminor's and Cminor's environments and memory states *) @@ -158,9 +150,7 @@ Inductive match_var (f: meminj) (id: ident) PTree.get id (global_var_env prog) = Some (Vscalar chunk) -> match_var f id e m te sp (Var_global_scalar chunk) | match_var_global_array: - forall sz, PTree.get id e = None -> - PTree.get id (global_var_env prog) = Some (Varray sz) -> match_var f id e m te sp (Var_global_array). (** Matching between a Csharpminor environment [e] and a Cminor @@ -175,7 +165,7 @@ Record match_env (f: meminj) (cenv: compilenv) (** Each variable mentioned in the compilation environment must match as defined above. *) me_vars: - forall id vi, PTree.get id cenv = Some vi -> match_var f id e m te sp vi; + forall id, match_var f id e m te sp (PMap.get id cenv); (** The range [lo, hi] must not be empty. *) me_low_high: @@ -270,8 +260,8 @@ Lemma match_env_store_mapped: Proof. intros. inversion H1. constructor; auto. (* vars *) - intros. generalize (me_vars0 _ _ H2); intro. - inversion H3; econstructor; eauto. + intros. generalize (me_vars0 id); intro. + inversion H2; econstructor; eauto. rewrite <- H5. eapply load_store_other; eauto. left. congruence. Qed. @@ -326,13 +316,13 @@ Lemma match_env_store_local: match_env f cenv e m2 (PTree.set id tv te) sp lo hi. Proof. intros. inversion H3. constructor; auto. - intros. generalize (me_vars0 _ _ H4); intro. - inversion H5; subst. + intros. generalize (me_vars0 id0); intro. + inversion H4; subst. (* var_local *) case (peq id id0); intro. (* the stored variable *) subst id0. - change Csharpminor.var_kind with var_kind in H6. + change Csharpminor.var_kind with var_kind in H5. rewrite H in H6. injection H6; clear H6; intros; subst b0 chunk0. econstructor. eauto. eapply load_store_same; eauto. auto. @@ -362,8 +352,8 @@ Lemma match_env_store_above: match_env f cenv e m2 te sp lo hi. Proof. intros. inversion H1; constructor; auto. - intros. generalize (me_vars0 _ _ H2); intro. - inversion H3; econstructor; eauto. + intros. generalize (me_vars0 id); intro. + inversion H2; econstructor; eauto. rewrite <- H5. eapply load_store_other; eauto. left. generalize (me_bounded0 _ _ _ H4). unfold block in *. omega. Qed. @@ -411,8 +401,8 @@ Lemma match_env_extensional: match_env f cenv e m te2 sp lo hi. Proof. induction 1; intros; econstructor; eauto. - intros. generalize (me_vars0 _ _ H0); intro. - inversion H1; econstructor; eauto. + intros. generalize (me_vars0 id); intro. + inversion H0; econstructor; eauto. rewrite H. auto. Qed. @@ -468,10 +458,10 @@ Lemma match_env_freelist: match_env f cenv e (free_list m fbl) te sp lo hi. Proof. intros. inversion H. econstructor; eauto. - intros. generalize (me_vars0 _ _ H1); intro. - inversion H2; econstructor; eauto. + intros. generalize (me_vars0 id); intro. + inversion H1; econstructor; eauto. rewrite <- H4. apply load_freelist. - intros. generalize (H0 _ H9); intro. + intros. generalize (H0 _ H8); intro. generalize (me_bounded0 _ _ _ H3). unfold block; omega. Qed. @@ -534,7 +524,7 @@ Lemma match_env_alloc_same: match_env f1 cenv1 e1 m1 te sp lo m1.(nextblock) -> te!id = Some tv -> let f2 := extend_inject b data f1 in - let cenv2 := PTree.set id info cenv1 in + let cenv2 := PMap.set id info cenv1 in let e2 := PTree.set id (b, lv) e1 in inject_incr f1 f2 -> match_env f2 cenv2 e2 m2 te sp lo m2.(nextblock). @@ -546,9 +536,9 @@ Proof. injection H; intros. rewrite <- H6; reflexivity. inversion H1. constructor. (* me_vars *) - intros id0 vi. unfold cenv2. rewrite PTree.gsspec. case (peq id0 id); intros. + intros id0. unfold cenv2. rewrite PMap.gsspec. case (peq id0 id); intros. (* same var *) - subst id0. injection H6; clear H6; intro; subst vi. destruct info. + subst id0. destruct info. (* info = Var_local chunk *) elim H0; intros. apply match_var_local with b Vundef tv. @@ -576,8 +566,8 @@ Proof. contradiction. contradiction. (* other vars *) - generalize (me_vars0 _ _ H6); intros. - inversion H7; econstructor; eauto. + generalize (me_vars0 id0); intros. + inversion H6; econstructor; eauto. unfold e2; rewrite PTree.gso; auto. unfold f2, extend_inject, eq_block; rewrite zeq_false; auto. generalize (me_bounded0 _ _ _ H8). unfold block in *; omega. @@ -628,8 +618,8 @@ Proof. rewrite <- H4 in H1. inversion H2. constructor; auto. (* me_vars *) - intros. generalize (me_vars0 _ _ H5); intro. - inversion H6; econstructor; eauto. + intros. generalize (me_vars0 id); intro. + inversion H5; econstructor; eauto. unfold f2, extend_inject, eq_block. rewrite zeq_false. auto. generalize (me_bounded0 _ _ _ H7). unfold block in *; omega. (* me_bounded *) @@ -681,7 +671,7 @@ Lemma match_callstack_alloc_left: match_callstack f1 (mkframe cenv1 e1 te sp lo m1.(nextblock) :: cs) m1.(nextblock) tbound m1 -> te!id = Some tv -> let f2 := extend_inject b data f1 in - let cenv2 := PTree.set id info cenv1 in + let cenv2 := PMap.set id info cenv1 in let e2 := PTree.set id (b, lv) e1 in inject_incr f1 f2 -> match_callstack f2 (mkframe cenv2 e2 te sp lo m2.(nextblock) :: cs) m2.(nextblock) tbound m2. @@ -1016,43 +1006,40 @@ Lemma var_get_correct: var_get cenv id = Some a -> match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> mem_inject f m tm -> - eval_var prog e id b (Vscalar chunk) -> + eval_var_ref prog e id b chunk -> load chunk m b 0 = Some v -> exists tv, eval_expr tge (Vptr sp Int.zero) le te tm a te tm tv /\ val_inject f v tv. Proof. unfold var_get; intros. - caseEq (cenv!id); [intros vi EQ | intros EQ]; rewrite EQ in H; try discriminate. - assert (match_var f id e m te sp vi). + assert (match_var f id e m te sp cenv!!id). inversion H0. inversion H17. auto. - caseEq vi; intros; rewrite H5 in H; simplify_eq H; clear H; intros; subst a vi. + inversion H4; subst; rewrite <- H5 in H; inversion H; subst. (* var_local *) - inversion H4. subst m0. inversion H2. subst. + inversion H2; [subst|congruence]. exists v'; split. apply eval_Evar. auto. replace v with v0. auto. congruence. - congruence. (* var_stack_scalar *) - inversion H4. subst m0 z. inversion H2; [subst|congruence]. - inversion H7. subst. + inversion H2; [subst|congruence]. assert (b0 = b). congruence. subst b0. assert (chunk0 = chunk). congruence. subst chunk0. assert (loadv chunk m (Vptr b Int.zero) = Some v). assumption. - generalize (loadv_inject _ _ _ _ _ _ _ H1 H5 H7). + generalize (loadv_inject _ _ _ _ _ _ _ H1 H9 H7). intros [tv [LOAD INJ]]. exists tv; split. eapply make_load_correct; eauto. eapply make_stackaddr_correct; eauto. auto. (* var_global_scalar *) - inversion H4. subst m0. inversion H2; [congruence|subst]. + inversion H2; [congruence|subst]. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inversion H9. destruct (mg_symbols0 _ _ H7) as [A B]. + inversion H11. destruct (mg_symbols0 _ _ H9) as [A B]. assert (chunk0 = chunk). congruence. subst chunk0. assert (loadv chunk m (Vptr b Int.zero) = Some v). assumption. assert (val_inject f (Vptr b Int.zero) (Vptr b Int.zero)). econstructor; eauto. - generalize (loadv_inject _ _ _ _ _ _ _ H1 H10 H11). + generalize (loadv_inject _ _ _ _ _ _ _ H1 H12 H13). intros [tv [LOAD INJ]]. exists tv; split. eapply make_load_correct; eauto. eapply make_globaladdr_correct; eauto. @@ -1060,42 +1047,39 @@ Proof. Qed. Lemma var_addr_correct: - forall cenv id a f e te sp lo hi m cs tm b lv le, - var_addr cenv id = Some a -> + forall cenv id a f e te sp lo hi m cs tm b le, match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> - eval_var prog e id b lv -> + var_addr cenv id = Some a -> + eval_var_addr prog e id b -> exists tv, eval_expr tge (Vptr sp Int.zero) le te tm a te tm tv /\ val_inject f (Vptr b Int.zero) tv. Proof. - intros until le. unfold var_addr. - caseEq (cenv!id). 2: intros; discriminate. - intros vi EQ. intros. - assert (match_var f id e m te sp vi). - inversion H0. inversion H15. auto. - caseEq vi; intros; rewrite H3 in H; simplify_eq H; clear H; intros; subst a; - rewrite H3 in H2; inversion H2. + unfold var_addr; intros. + assert (match_var f id e m te sp cenv!!id). + inversion H. inversion H15. auto. + inversion H2; subst; rewrite <- H3 in H0; inversion H0; subst; clear H0. (* var_stack_scalar *) - subst m0 z. inversion H1; [subst|congruence]. + inversion H1; [subst|congruence]. exists (Vptr sp (Int.repr ofs)); split. eapply make_stackaddr_correct. replace b with b0. auto. congruence. (* var_stack_array *) - subst z. inversion H1; [subst|congruence]. + inversion H1; [subst|congruence]. exists (Vptr sp (Int.repr ofs)); split. eapply make_stackaddr_correct. replace b with b0. auto. congruence. (* var_global_scalar *) - subst m0. inversion H1; [congruence|subst]. + inversion H1; [congruence|subst]. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inversion H3. destruct (mg_symbols0 _ _ H6) as [A B]. + inversion H7. destruct (mg_symbols0 _ _ H6) as [A B]. exists (Vptr b Int.zero); split. eapply make_globaladdr_correct. eauto. econstructor; eauto. (* var_global_array *) inversion H1; [congruence|subst]. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inversion H3. destruct (mg_symbols0 _ _ H6) as [A B]. + inversion H6. destruct (mg_symbols0 _ _ H5) as [A B]. exists (Vptr b Int.zero); split. eapply make_globaladdr_correct. eauto. econstructor; eauto. @@ -1108,7 +1092,7 @@ Lemma var_set_correct: eval_expr tge (Vptr sp Int.zero) le te1 tm1 rhs te2 tm2 vrhs -> val_inject f v1 vrhs -> mem_inject f m2 tm2 -> - eval_var prog e id b (Vscalar chunk) -> + eval_var_ref prog e id b chunk -> cast chunk v1 = Some v2 -> store chunk m2 b 0 v2 = Some m3 -> exists te3, exists tm3, exists tv, @@ -1117,18 +1101,16 @@ Lemma var_set_correct: mem_inject f m3 tm3 /\ match_callstack f (mkframe cenv e te3 sp lo hi :: cs) m3.(nextblock) tm3.(nextblock) m3. Proof. - intros until m3. unfold var_set. - caseEq (cenv!id). 2:intros;congruence. intros vi EQ; intros. + unfold var_set; intros. assert (NEXTBLOCK: nextblock m3 = nextblock m2). generalize (store_inv _ _ _ _ _ _ H6). simpl. tauto. inversion H0. subst f0 cenv0 e0 te sp0 lo0 hi0 cs0 bound tbound m. - inversion H20. - caseEq vi; intros; subst vi; simplify_eq H; clear H; intros; subst a. + assert (match_var f id e m2 te2 sp cenv!!id). inversion H20; auto. + inversion H7; subst; rewrite <- H8 in H; inversion H; subst; clear H. (* var_local *) - generalize (me_vars0 _ _ EQ); intro. inversion H. subst chunk0. inversion H4; [subst|congruence]. assert (b0 = b). congruence. subst b0. - assert (m = chunk). congruence. subst m. + assert (chunk0 = chunk). congruence. subst chunk0. elim (make_cast_correct _ _ _ _ _ _ _ _ _ _ _ _ H1 H5 H2). intros tv [EVAL [INJ NORM]]. exists (PTree.set id tv te2); exists tm2; exists tv. @@ -1137,15 +1119,13 @@ Proof. split. eapply store_unmapped_inject; eauto. rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto. (* var_stack_scalar *) - generalize (me_vars0 _ _ EQ); intro. inversion H. - subst chunk0 z. inversion H4; [subst|congruence]. assert (b0 = b). congruence. subst b0. - assert (m = chunk). congruence. subst m. + assert (chunk0 = chunk). congruence. subst chunk0. assert (storev chunk m2 (Vptr b Int.zero) v2 = Some m3). assumption. generalize (make_stackaddr_correct sp le te1 tm1 ofs). intro EVALSTACKADDR. generalize (make_store_correct _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - EVALSTACKADDR H1 H5 H8 H3 H10 H2). + EVALSTACKADDR H1 H5 H11 H3 H10 H2). intros [tm3 [tv [EVAL [MEMINJ [VALINJ TNEXTBLOCK]]]]]. exists te2; exists tm3; exists tv. split. auto. split. auto. split. auto. @@ -1153,23 +1133,20 @@ Proof. eapply match_callstack_mapped; eauto. inversion H10; congruence. (* var_global_scalar *) - generalize (me_vars0 _ _ EQ); intro. inversion H. - subst chunk0. inversion H4; [congruence|subst]. - assert (m = chunk). congruence. subst m. + assert (chunk0 = chunk). congruence. subst chunk0. assert (storev chunk m2 (Vptr b Int.zero) v2 = Some m3). assumption. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inversion H13. destruct (mg_symbols0 _ _ H10) as [A B]. + inversion H14. destruct (mg_symbols0 _ _ H11) as [A B]. assert (val_inject f (Vptr b Int.zero) (Vptr b Int.zero)). econstructor; eauto. generalize (make_globaladdr_correct sp le te1 tm1 id b B). intro EVALGLOBALADDR. generalize (make_store_correct _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ - EVALGLOBALADDR H1 H5 H12 H3 H14 H2). + EVALGLOBALADDR H1 H5 H13 H3 H15 H2). intros [tm3 [tv [EVAL [MEMINJ [VALINJ TNEXTBLOCK]]]]]. exists te2; exists tm3; exists tv. split. auto. split. auto. split. auto. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. - eapply match_callstack_mapped; eauto. - inversion H11; congruence. + eapply match_callstack_mapped; eauto. congruence. Qed. (** * Correctness of stack allocation of local variables *) @@ -1380,16 +1357,12 @@ Proof. constructor. omega. change (valid_block tm' sp). eapply valid_new_block; eauto. constructor. (* me_vars *) - intros. generalize (global_compilenv_charact _ _ H5). - intros [lv [A B]]. - destruct vi; simpl in B; try contradiction. + intros. generalize (global_compilenv_charact id). + destruct (gce!!id); intro; try contradiction. + constructor. + unfold Csharpminor.empty_env. apply PTree.gempty. auto. constructor. unfold Csharpminor.empty_env. apply PTree.gempty. - congruence. - destruct B as [sz1 C]. - apply match_var_global_array with sz1. - unfold Csharpminor.empty_env. apply PTree.gempty. - congruence. (* me_low_high *) omega. (* me_bounded *) @@ -1489,7 +1462,6 @@ Lemma store_parameters_correct: 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 -> - (forall id chunk, In (id, chunk) params -> cenv!id <> None) -> exists te2, exists tm2, exec_stmt tge (Vptr sp Int.zero) te1 tm1 (store_parameters cenv params) @@ -1508,28 +1480,26 @@ Proof. inversion NOREPET. subst hd tl. assert (NEXT: nextblock m1 = nextblock m). generalize (store_inv _ _ _ _ _ _ H1). simpl; tauto. - caseEq (cenv!id); intros. - destruct v; generalize (me_vars0 _ _ H3); intro MV; inversion MV; subst. - (* cenv!id = Some(Var_local chunk) *) + generalize (me_vars0 id). intro. inversion H3; subst. + (* cenv!!id = Var_local chunk *) assert (b0 = b). congruence. subst b0. - assert (m0 = chunk). congruence. subst m0. + assert (chunk0 = chunk). congruence. subst chunk0. assert (v' = tv). congruence. subst v'. assert (eval_expr tge (Vptr sp Int.zero) nil te1 tm1 (Evar id) te1 tm1 tv). constructor. auto. generalize (make_cast_correct _ _ _ _ _ _ _ _ _ _ _ _ - H7 H0 H11). + H15 H0 H11). intros [tv' [EVAL1 [VINJ1 VNORM]]]. set (te2 := PTree.set id tv' te1). assert (VVM2: vars_vals_match f params vl te2). apply vars_vals_match_extensional with te1; auto. intros. unfold te2; apply PTree.gso. red; intro; subst id0. elim H5. change id with (fst (id, lv)). apply List.in_map; auto. - generalize (store_unmapped_inject _ _ _ _ _ _ _ _ MINJ H1 H13); intro MINJ2. + generalize (store_unmapped_inject _ _ _ _ _ _ _ _ MINJ H1 H9); intro MINJ2. generalize (match_callstack_store_local _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ H VINJ1 VNORM H1 MATCH); fold te2; rewrite <- NEXT; intro MATCH2. - assert (forall id chunk, In (id, chunk) params -> cenv!id <> None). intros; eauto. - destruct (IHbind_parameters _ _ _ _ _ _ _ _ VVM2 H6 MINJ2 MATCH2 H16) + destruct (IHbind_parameters _ _ _ _ _ _ _ _ VVM2 H6 MINJ2 MATCH2) as [te3 [tm3 [EXEC3 [MINJ3 MATCH3]]]]. exists te3; exists tm3. (* execution *) @@ -1539,22 +1509,21 @@ Proof. (* meminj & match_callstack *) tauto. - (* cenv!!id = Some(Var_stack_scalar) *) + (* cenv!!id = Var_stack_scalar *) assert (b0 = b). congruence. subst b0. - assert (m0 = chunk). congruence. subst m0. - pose (EVAL1 := make_stackaddr_correct sp nil te1 tm1 z). + assert (chunk0 = chunk). congruence. subst chunk0. + pose (EVAL1 := make_stackaddr_correct sp nil te1 tm1 ofs). assert (EVAL2: eval_expr tge (Vptr sp Int.zero) nil te1 tm1 (Evar id) te1 tm1 tv). constructor. auto. destruct (make_store_correct _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ (Vptr b Int.zero) _ - EVAL1 EVAL2 H0 H1 MINJ H13 H11) + EVAL1 EVAL2 H0 H1 MINJ H8 H11) as [tm2 [tv' [EVAL3 [MINJ2 [VINJ NEXT1]]]]]. - assert (f b <> None). inversion H13. congruence. - generalize (match_callstack_mapped _ _ _ _ _ MATCH _ _ _ _ _ H7 H1). + assert (f b <> None). inversion H8. congruence. + generalize (match_callstack_mapped _ _ _ _ _ MATCH _ _ _ _ _ H9 H1). rewrite <- NEXT; rewrite <- NEXT1; intro MATCH2. - assert (forall id chunk, In (id, chunk) params -> cenv!id <> None). intros; eauto. destruct (IHbind_parameters _ _ _ _ _ _ _ _ - H12 H6 MINJ2 MATCH2 H8) as [te3 [tm3 [EVAL4 [MINJ3 MATCH3]]]]. + H12 H6 MINJ2 MATCH2) as [te3 [tm3 [EVAL4 [MINJ3 MATCH3]]]]. exists te3; exists tm3. (* execution *) split. apply exec_Sseq_continue with te1 tm2. @@ -1567,7 +1536,6 @@ Proof. congruence. congruence. congruence. - elim (H4 id chunk); auto. Qed. Lemma vars_vals_match_holds_1: @@ -1621,6 +1589,7 @@ Proof. induction 1; simpl; eauto. Qed. +(**** Lemma build_compilenv_domain: forall f id chunk, In (id, chunk) f.(Csharpminor.fn_params) -> @@ -1656,6 +1625,7 @@ Proof. change (id, Vscalar chunk) with (g (id, chunk)). apply List.in_map. auto. Qed. +****) (** The final result in this section: the behaviour of function entry in the generated Cminor code (allocate stack data block and store @@ -1701,9 +1671,8 @@ Proof. assert (NOREPET: list_norepet (List.map (@fst ident memory_chunk) fn.(Csharpminor.fn_params))). unfold fn_params_names in H7. eapply list_norepet_append_left; eauto. - generalize (build_compilenv_domain fn). rewrite H2. intro. destruct (store_parameters_correct _ _ _ _ _ H0 _ _ _ _ _ _ _ _ - VVM NOREPET MINJ1 MATCH1 H8) + VVM NOREPET MINJ1 MATCH1) as [te2 [tm2 [EXEC [MINJ2 MATCH2]]]]. exists f1; exists te2; exists tm2. split. auto. split. auto. split. auto. split. auto. @@ -1870,7 +1839,7 @@ Lemma transl_expr_Evar_correct: forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) (id : positive) (b : block) (chunk : memory_chunk) (v : val), - eval_var prog e id b (Vscalar chunk) -> + eval_var_ref prog e id b chunk -> load chunk m b 0 = Some v -> eval_expr_prop le e m (Csharpminor.Evar id) m v. Proof. @@ -1887,7 +1856,7 @@ Lemma transl_expr_Eassign_correct: (chunk : memory_chunk) (v1 v2 : val) (m2 : mem), Csharpminor.eval_expr prog le e m a m1 v1 -> eval_expr_prop le e m a m1 v1 -> - eval_var prog e id b (Vscalar chunk) -> + eval_var_ref prog e id b chunk -> cast chunk v1 = Some v2 -> store chunk m1 b 0 v2 = Some m2 -> eval_expr_prop le e m (Csharpminor.Eassign id a) m2 v2. @@ -1904,13 +1873,13 @@ Qed. Lemma transl_expr_Eaddrof_correct: forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) (id : positive) - (b : block) (lv : var_kind), - eval_var prog e id b lv -> + (b : block), + eval_var_addr prog e id b -> eval_expr_prop le e m (Eaddrof id) m (Vptr b Int.zero). Proof. intros; red; intros. simpl in TR. - generalize (var_addr_correct _ _ _ _ _ _ _ _ _ _ _ _ _ _ tle - TR MATCH H). + generalize (var_addr_correct _ _ _ _ _ _ _ _ _ _ _ _ _ tle + MATCH TR H). intros [tv [EVAL VINJ]]. exists f1; exists te1; exists tm1; exists tv. intuition. Qed. diff --git a/backend/Csharpminor.v b/backend/Csharpminor.v index c0d4cae4..49fd3df3 100644 --- a/backend/Csharpminor.v +++ b/backend/Csharpminor.v @@ -324,21 +324,37 @@ Section RELSEM. Variable prg: program. Let ge := Genv.globalenv (program_of_program prg). -(* Evaluation of a variable reference: [eval_var prg ge e id b vi] states - that variable [id] in environment [e] evaluates to block [b] - and is associated with the variable info [vi]. *) +(* Evaluation of the address of a variable: + [eval_var_addr prg ge e id b] states that variable [id] + in environment [e] evaluates to block [b]. *) -Inductive eval_var: env -> ident -> block -> var_kind -> Prop := - | eval_var_local: +Inductive eval_var_addr: env -> ident -> block -> Prop := + | eval_var_addr_local: forall e id b vi, PTree.get id e = Some (b, vi) -> - eval_var e id b vi - | eval_var_global: - forall e id b vi, + eval_var_addr e id b + | eval_var_addr_global: + forall e id b, + PTree.get id e = None -> + Genv.find_symbol ge id = Some b -> + eval_var_addr e id b. + +(* Evaluation of a reference to a scalar variable: + [eval_var_ref prg ge e id b chunk] states + that variable [id] in environment [e] evaluates to block [b] + and is associated with the memory chunk [chunk]. *) + +Inductive eval_var_ref: env -> ident -> block -> memory_chunk -> Prop := + | eval_var_ref_local: + forall e id b chunk, + PTree.get id e = Some (b, Vscalar chunk) -> + eval_var_ref e id b chunk + | eval_var_ref_global: + 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 vi -> - eval_var e id b vi. + PTree.get id (global_var_env prg) = Some (Vscalar chunk) -> + eval_var_ref e id b chunk. (** Evaluation of an expression: [eval_expr prg le e m a m' v] states that expression [a], in initial memory state [m], evaluates to value @@ -351,19 +367,19 @@ Inductive eval_expr: mem -> expr -> mem -> val -> Prop := | eval_Evar: forall le e m id b chunk v, - eval_var e id b (Vscalar chunk) -> + eval_var_ref e id b chunk -> Mem.load chunk m b 0 = Some v -> eval_expr le e m (Evar id) m v | eval_Eassign: forall le e m id a m1 b chunk v1 v2 m2, eval_expr le e m a m1 v1 -> - eval_var e id b (Vscalar chunk) -> + eval_var_ref e id b chunk -> cast chunk v1 = Some v2 -> Mem.store chunk m1 b 0 v2 = Some m2 -> eval_expr le e m (Eassign id a) m2 v2 | eval_Eaddrof: - forall le e m id b lv, - eval_var e id b lv -> + forall le e m id b, + eval_var_addr e id b -> eval_expr le e m (Eaddrof id) m (Vptr b Int.zero) | eval_Eop: forall le e m op al m1 vl v, -- cgit