diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-07 15:52:58 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-07 15:52:58 +0000 |
commit | a74f6b45d72834b5b8417297017bd81424123d98 (patch) | |
tree | d291cf3f05397658f0fe9d8ecce9b8785a50d270 /backend/RTLgenproof.v | |
parent | 54cba6d4cae1538887f296a62be1c99378fe0916 (diff) | |
download | compcert-a74f6b45d72834b5b8417297017bd81424123d98.tar.gz compcert-a74f6b45d72834b5b8417297017bd81424123d98.zip |
Merge of the newmem and newextcalls branches:
- Revised memory model with concrete representation of ints & floats,
and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/RTLgenproof.v')
-rw-r--r-- | backend/RTLgenproof.v | 132 |
1 files changed, 72 insertions, 60 deletions
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index d07bd081..f4d1342a 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -17,7 +17,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Smallstep. Require Import Globalenvs. @@ -337,7 +337,7 @@ Lemma function_ptr_translated: exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. Proof - (Genv.find_funct_ptr_transf_partial transl_fundef TRANSL). + (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL). Lemma functions_translated: forall (v: val) (f: CminorSel.fundef), @@ -345,7 +345,7 @@ Lemma functions_translated: exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf. Proof - (Genv.find_funct_transf_partial transl_fundef TRANSL). + (Genv.find_funct_transf_partial transl_fundef _ TRANSL). Lemma sig_transl_function: forall (f: CminorSel.fundef) (tf: RTL.fundef), @@ -365,10 +365,10 @@ Qed. (** Correctness of the code generated by [add_move]. *) Lemma tr_move_correct: - forall r1 ns r2 nd cs code sp rs m, - tr_move code ns r1 nd r2 -> + forall r1 ns r2 nd cs f sp rs m, + tr_move f.(fn_code) ns r1 nd r2 -> exists rs', - star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) /\ + star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\ rs'#r2 = rs#r1 /\ (forall r, r <> r2 -> rs'#r = rs#r). Proof. @@ -382,13 +382,13 @@ Qed. (** Correctness of the code generated by [store_var] and [store_optvar]. *) Lemma tr_store_var_correct: - forall rs cs code map r id ns nd e sp m, - tr_store_var code map r id ns nd -> + forall rs cs f map r id ns nd e sp m, + tr_store_var f.(fn_code) map r id ns nd -> map_wf map -> match_env map e nil rs -> exists rs', - star step tge (State cs code sp ns rs m) - E0 (State cs code sp nd rs' m) + star step tge (State cs f sp ns rs m) + E0 (State cs f sp nd rs' m) /\ match_env map (PTree.set id rs#r e) nil rs'. Proof. intros. destruct H as [rv [A B]]. @@ -402,13 +402,13 @@ Proof. Qed. Lemma tr_store_optvar_correct: - forall rs cs code map r optid ns nd e sp m, - tr_store_optvar code map r optid ns nd -> + forall rs cs f map r optid ns nd e sp m, + tr_store_optvar f.(fn_code) map r optid ns nd -> map_wf map -> match_env map e nil rs -> exists rs', - star step tge (State cs code sp ns rs m) - E0 (State cs code sp nd rs' m) + star step tge (State cs f sp ns rs m) + E0 (State cs f sp nd rs' m) /\ match_env map (set_optvar optid rs#r e) nil rs'. Proof. intros. destruct optid; simpl in *. @@ -419,15 +419,15 @@ Qed. (** Correctness of the translation of [switch] statements *) Lemma transl_switch_correct: - forall cs sp e m code map r nexits t ns, - tr_switch code map r nexits t ns -> + forall cs sp e m f map r nexits t ns, + tr_switch f.(fn_code) map r nexits t ns -> forall rs i act, rs#r = Vint i -> map_wf map -> match_env map e nil rs -> comptree_match i t = Some act -> exists nd, exists rs', - star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) /\ + star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\ nth_error nexits act = Some nd /\ match_env map e nil rs'. Proof. @@ -458,7 +458,7 @@ Proof. set (rs1 := rs#rt <- (Vint(Int.sub i ofs))). assert (ME1: match_env map e nil rs1). unfold rs1. eauto with rtlg. - assert (EX1: step tge (State cs code sp n rs m) E0 (State cs code sp n1 rs1 m)). + assert (EX1: step tge (State cs f sp n rs m) E0 (State cs f sp n1 rs1 m)). eapply exec_Iop; eauto. predSpec Int.eq Int.eq_spec ofs Int.zero; simpl. rewrite H10. rewrite Int.sub_zero_l. congruence. @@ -521,12 +521,12 @@ Variable m: mem. Definition transl_expr_prop (le: letenv) (a: expr) (v: val) : Prop := - forall cs code map pr ns nd rd rs + forall cs f map pr ns nd rd rs (MWF: map_wf map) - (TE: tr_expr code map pr a ns nd rd) + (TE: tr_expr f.(fn_code) map pr a ns nd rd) (ME: match_env map e le rs), exists rs', - star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) + star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\ match_env map e le rs' /\ rs'#rd = v /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). @@ -536,25 +536,25 @@ Definition transl_expr_prop Definition transl_exprlist_prop (le: letenv) (al: exprlist) (vl: list val) : Prop := - forall cs code map pr ns nd rl rs + forall cs f map pr ns nd rl rs (MWF: map_wf map) - (TE: tr_exprlist code map pr al ns nd rl) + (TE: tr_exprlist f.(fn_code) map pr al ns nd rl) (ME: match_env map e le rs), exists rs', - star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) + star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\ match_env map e le rs' /\ rs'##rl = vl /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). Definition transl_condition_prop (le: letenv) (a: condexpr) (vb: bool) : Prop := - forall cs code map pr ns ntrue nfalse rs + forall cs f map pr ns ntrue nfalse rs (MWF: map_wf map) - (TE: tr_condition code map pr a ns ntrue nfalse) + (TE: tr_condition f.(fn_code) map pr a ns ntrue nfalse) (ME: match_env map e le rs), exists rs', - star step tge (State cs code sp ns rs m) E0 - (State cs code sp (if vb then ntrue else nfalse) rs' m) + star step tge (State cs f sp ns rs m) E0 + (State cs f sp (if vb then ntrue else nfalse) rs' m) /\ match_env map e le rs' /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). @@ -604,7 +604,7 @@ Proof. split. eapply star_right. eexact EX1. eapply exec_Iop; eauto. subst vargs. - rewrite (@eval_operation_preserved CminorSel.fundef RTL.fundef ge tge). + rewrite (@eval_operation_preserved CminorSel.fundef _ _ _ ge tge). auto. exact symbols_preserved. traceEq. (* Match-env *) @@ -621,7 +621,7 @@ Lemma transl_expr_Eload_correct: eval_exprlist ge sp e m le args vargs -> transl_exprlist_prop le args vargs -> Op.eval_addressing ge sp addr vargs = Some vaddr -> - loadv chunk m vaddr = Some v -> + Mem.loadv chunk m vaddr = Some v -> transl_expr_prop le (Eload chunk addr args) v. Proof. intros; red; intros. inv TE. @@ -629,7 +629,7 @@ Proof. exists (rs1#rd <- v). (* Exec *) split. eapply star_right. eexact EX1. eapply exec_Iload; eauto. - rewrite RES1. rewrite (@eval_addressing_preserved _ _ ge tge). + rewrite RES1. rewrite (@eval_addressing_preserved _ _ _ _ ge tge). exact H1. exact symbols_preserved. traceEq. (* Match-env *) split. eauto with rtlg. @@ -650,7 +650,7 @@ Lemma transl_expr_Econdition_correct: Proof. intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]]. - assert (tr_expr code map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd). + assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd). destruct vcond; auto. exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2. @@ -767,7 +767,7 @@ Lemma transl_condition_CEcondition_correct: Proof. intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]]. - assert (tr_condition code map pr (if vcond then ifso else ifnot) + assert (tr_condition f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue' else nfalse') ntrue nfalse). destruct vcond; auto. exploit H2; eauto. intros [rs2 [EX2 [ME2 OTHER2]]]. @@ -977,12 +977,13 @@ Qed. *) -Inductive tr_funbody (c: code) (map: mapping) (f: CminorSel.function) +Inductive tr_fun (tf: function) (map: mapping) (f: CminorSel.function) (ngoto: labelmap) (nret: node) (rret: option reg) : Prop := - | tr_funbody_intro: forall nentry r, + | tr_fun_intro: forall nentry r, rret = ret_reg f.(CminorSel.fn_sig) r -> - tr_stmt c map f.(fn_body) nentry nret nil ngoto nret rret -> - tr_funbody c map f ngoto nret rret. + tr_stmt tf.(fn_code) map f.(fn_body) nentry nret nil ngoto nret rret -> + tf.(fn_stacksize) = f.(fn_stackspace) -> + tr_fun tf map f ngoto nret rret. Inductive tr_cont: RTL.code -> mapping -> CminorSel.cont -> node -> list node -> labelmap -> node -> option reg -> @@ -1006,25 +1007,25 @@ Inductive tr_cont: RTL.code -> mapping -> with match_stacks: CminorSel.cont -> list RTL.stackframe -> Prop := | match_stacks_stop: match_stacks Kstop nil - | match_stacks_call: forall optid f sp e k r c n rs cs map nexits ngoto nret rret n', + | match_stacks_call: forall optid f sp e k r tf n rs cs map nexits ngoto nret rret n', map_wf map -> - tr_funbody c map f ngoto nret rret -> + tr_fun tf map f ngoto nret rret -> match_env map e nil rs -> - tr_store_optvar c map r optid n n' -> + tr_store_optvar tf.(fn_code) map r optid n n' -> ~reg_in_map map r -> - tr_cont c map k n' nexits ngoto nret rret cs -> - match_stacks (Kcall optid f sp e k) (Stackframe r c sp n rs :: cs). + tr_cont tf.(fn_code) map k n' nexits ngoto nret rret cs -> + match_stacks (Kcall optid f sp e k) (Stackframe r tf sp n rs :: cs). Inductive match_states: CminorSel.state -> RTL.state -> Prop := | match_state: - forall f s k sp e m cs c ns rs map ncont nexits ngoto nret rret + forall f s k sp e m cs tf ns rs map ncont nexits ngoto nret rret (MWF: map_wf map) - (TS: tr_stmt c map s ns ncont nexits ngoto nret rret) - (TF: tr_funbody c map f ngoto nret rret) - (TK: tr_cont c map k ncont nexits ngoto nret rret cs) + (TS: tr_stmt tf.(fn_code) map s ns ncont nexits ngoto nret rret) + (TF: tr_fun tf map f ngoto nret rret) + (TK: tr_cont tf.(fn_code) map k ncont nexits ngoto nret rret cs) (ME: match_env map e nil rs), match_states (CminorSel.State f s k sp e m) - (RTL.State cs c sp ns rs m) + (RTL.State cs tf sp ns rs m) | match_callstate: forall f args k m cs tf (TF: transl_fundef f = OK tf) @@ -1109,15 +1110,19 @@ Proof. (* skip return *) inv TS. - assert (c!ncont = Some(Ireturn rret) /\ match_stacks k cs). - inv TK; simpl in H; try contradiction; auto. - destruct H1. + assert ((fn_code tf)!ncont = Some(Ireturn rret) + /\ match_stacks k cs). + inv TK; simpl in H; try contradiction; auto. + destruct H2. assert (rret = None). inv TF. unfold ret_reg. rewrite H0. auto. + assert (fn_stacksize tf = fn_stackspace f). + inv TF. auto. subst rret. econstructor; split. left; apply plus_one. eapply exec_Ireturn. eauto. - simpl. constructor; auto. + rewrite H5. eauto. + constructor; auto. (* assign *) inv TS. @@ -1152,7 +1157,7 @@ Proof. intros [rs' [A [B [C D]]]]. exploit transl_exprlist_correct; eauto. intros [rs'' [E [F [G J]]]]. - exploit functions_translated; eauto. intros [tf [P Q]]. + exploit functions_translated; eauto. intros [tf' [P Q]]. econstructor; split. left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. eapply exec_Icall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto. @@ -1166,12 +1171,14 @@ Proof. intros [rs' [A [B [C D]]]]. exploit transl_exprlist_correct; eauto. intros [rs'' [E [F [G J]]]]. - exploit functions_translated; eauto. intros [tf [P Q]]. + exploit functions_translated; eauto. intros [tf' [P Q]]. exploit match_stacks_call_cont; eauto. intros [U V]. + assert (fn_stacksize tf = fn_stackspace f). inv TF; auto. econstructor; split. left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. eapply exec_Itailcall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto. apply sig_transl_function; auto. + rewrite H2; eauto. traceEq. rewrite G. constructor; auto. (* seq *) @@ -1234,17 +1241,21 @@ Proof. (* return none *) inv TS. exploit match_stacks_call_cont; eauto. intros [U V]. + inversion TF. econstructor; split. left; apply plus_one. eapply exec_Ireturn; eauto. - simpl. constructor; auto. + rewrite H2; eauto. + constructor; auto. (* return some *) inv TS. exploit transl_expr_correct; eauto. intros [rs' [A [B [C D]]]]. - exploit match_stacks_call_cont; eauto. intros [U V]. + exploit match_stacks_call_cont; eauto. intros [U V]. + inversion TF. econstructor; split. - left; eapply plus_right. eexact A. eapply exec_Ireturn; eauto. traceEq. + left; eapply plus_right. eexact A. eapply exec_Ireturn; eauto. + rewrite H4; eauto. traceEq. simpl. rewrite C. constructor; auto. (* label *) @@ -1301,11 +1312,12 @@ Proof. induction 1. exploit function_ptr_translated; eauto. intros [tf [A B]]. econstructor; split. - econstructor. rewrite (transform_partial_program_main _ _ TRANSL). fold tge. - rewrite symbols_preserved. eexact H. + econstructor. apply (Genv.init_mem_transf_partial _ _ TRANSL); eauto. + rewrite (transform_partial_program_main _ _ TRANSL). fold tge. + rewrite symbols_preserved. eauto. eexact A. - rewrite <- H1. apply sig_transl_function; auto. - rewrite (Genv.init_mem_transf_partial _ _ TRANSL). constructor. auto. constructor. + rewrite <- H2. apply sig_transl_function; auto. + constructor. auto. constructor. Qed. Lemma transl_final_states: |