From 9d286aa671a9c320114337a821fab8677e03558e Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 3 Apr 2019 19:12:21 +0200 Subject: bien meilleure façon de s'inspirer de l'ancienne traduction MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/Machblockgenproof.v | 130 ++++++++++++++++++++----------------------- 1 file changed, 59 insertions(+), 71 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index 07718ede..0ca23a36 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -195,7 +195,7 @@ Qed. Definition concat (h: list label) (c: code): code := match c with - | nil => empty_bblock::nil + | nil => {| header := h; body := nil; exit := None |}::nil | b::c' => {| header := h ++ (header b); body := body b; exit := exit b |}::c' end. @@ -325,6 +325,7 @@ Proof. subst_is_trans_code H. omega. Admitted. (* A FINIR *) +Local Hint Resolve dist_end_block_code_simu_mid_block. Lemma size_nonzero c b bl: @@ -333,9 +334,41 @@ Proof. intros H; inversion H; subst. Admitted. (* A FINIR *) -Axiom TODO: False. (* a éliminer *) +(* TODO: définir les predicats inductifs suivants de façon à prouver le lemme [is_trans_code_decompose] ci-dessous *) -Local Hint Resolve dist_end_block_code_simu_mid_block. +Inductive is_header: list label -> Mach.code -> Mach.code -> Prop := + . (* A FAIRE *) + +Inductive is_body: list basic_inst -> Mach.code -> Mach.code -> Prop := + . (* A FAIRE *) + +Inductive is_exit: option control_flow_inst -> Mach.code -> Mach.code -> Prop := + . (* A FAIRE *) + +Lemma trans_code_decompose c bc: + is_trans_code c bc -> forall b blc, bc=(b::blc) -> + exists c0 c1 c2, is_header (header b) c c0 /\ is_body (body b) c0 c1 /\ is_exit (exit b) c1 c2 /\ is_trans_code c2 blc. +Proof. + induction 1; intros b blc X; inversion X; subst; clear X. +Admitted. + +Lemma step_simu_header st f sp rs m s c h c' t: + is_header h c c' -> + starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length h) (Mach.State st f sp c rs m) t s -> + s = Mach.State st f sp c' rs m /\ t = E0. +Proof. + induction 1. (* A FINIR *) +Admitted. +(* VIELLE PREUVE -- UTILE POUR S'INSPIRER ??? + induction c as [ | i c]; simpl; intros h c' t H. + - inversion_clear H. simpl; intros H; inversion H; auto. + - destruct i; try (injection H; clear H; intros H H2; subst; simpl; intros H; inversion H; subst; auto). + remember (to_bblock_header c) as bhc. destruct bhc as [h0 c0]. + injection H; clear H; intros H H2; subst; simpl; intros H; inversion H; subst. + inversion H1; clear H1; subst; auto. autorewrite with trace_rewrite. + exploit IHc; eauto. +Qed. +*) Lemma step_simu_basic_step (i: Mach.instruction) (bi: basic_inst) (c: Mach.code) s f sp rs m (t:trace) (s':Mach.state): trans_inst i = MB_basic bi -> @@ -356,19 +389,12 @@ Proof. unfold Genv.symbol_address; rewrite symbols_preserved; auto. Qed. -Inductive is_first_bblock b c blc: Prop := - | Tr_dummy_nil: b = empty_bblock -> c=nil -> blc = nil -> is_first_bblock b c blc - | Tr_trans_code: is_trans_code c (b::blc) -> is_first_bblock b c blc - . - -Lemma star_step_simu_body_step s f sp c bl: - is_trans_code c bl -> forall b blc rs m t s', - bl=b::blc -> - (header b)=nil -> - starN (Mach.step (inv_trans_rao rao)) ge (length (body b)) (Mach.State s f sp c rs m) t s' -> - exists c' rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp (body b) rs m rs' m' /\ is_first_bblock {| header := nil; body:=nil; exit := exit b |} c' blc. +Lemma star_step_simu_body_step s f sp c bdy c': + is_body bdy c c' -> forall rs m t s', + starN (Mach.step (inv_trans_rao rao)) ge (length bdy) (Mach.State s f sp c rs m) t s' -> + exists rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp bdy rs m rs' m'. Proof. - induction 1; intros b blc rs m t s' X; inversion X; subst; clear X. + induction 1. Admitted. (* A FINIR *) (* VIELLE PREUVE -- UTILE POUR S'INSPIRER ??? @@ -397,6 +423,8 @@ Qed. Local Hint Resolve exec_MBcall exec_MBtailcall exec_MBbuiltin exec_MBgoto exec_MBcond_true exec_MBcond_false exec_MBjumptable exec_MBreturn exec_Some_exit exec_None_exit. Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same. + +Axiom TODO: False. (* a éliminer *) Lemma match_states_concat_trans_code st f sp c rs m h: match_states (Mach.State st f sp c rs m) (State (trans_stack st) f sp (concat h (trans_code c)) rs m). Proof. @@ -464,14 +492,12 @@ Proof. Qed. *) -Lemma step_simu_exit_step c stk f sp rs m t s1 b blc b': - is_trans_code c (b::blc) -> - (header b)=nil -> - (body b)=nil -> - starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length_opt (exit b)) (Mach.State stk f sp c rs m) t s1 -> - exists c' s2, exit_step rao tge (exit b) (State (trans_stack stk) f sp (b'::blc) rs m) t s2 /\ match_states s1 s2 /\ is_trans_code c' blc. +Lemma step_simu_exit_step stk f sp rs m t s1 e c c' b blc: + is_exit e c c' -> is_trans_code c' blc -> + starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length_opt e) (Mach.State stk f sp c rs m) t s1 -> + exists s2, exit_step rao tge e (State (trans_stack stk) f sp (b::blc) rs m) t s2 /\ match_states s1 s2. Proof. - inversion_clear 1. (* A FINIR *) + destruct 1. (* A FINIR *) Admitted. (* VIELLE PREUVE -- UTILE POUR S'INSPIRER ??? Proof. @@ -488,25 +514,6 @@ Proof. Qed. *) -Lemma step_simu_header st f sp rs m s c bl: - is_trans_code c bl -> forall b blc t, bl=b::blc -> - starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length (header b)) (Mach.State st f sp c rs m) t s -> - exists c', s = Mach.State st f sp c' rs m /\ t = E0 /\ is_first_bblock {| header := nil; body:=body b; exit := exit b |} c' blc. -Proof. - induction 1; intros b blc t X; inversion X; subst; clear X. -Admitted. - -(* VIELLE PREUVE -- UTILE POUR S'INSPIRER ??? - induction c as [ | i c]; simpl; intros h c' t H. - - inversion_clear H. simpl; intros H; inversion H; auto. - - destruct i; try (injection H; clear H; intros H H2; subst; simpl; intros H; inversion H; subst; auto). - remember (to_bblock_header c) as bhc. destruct bhc as [h0 c0]. - injection H; clear H; intros H H2; subst; simpl; intros H; inversion H; subst. - inversion H1; clear H1; subst; auto. autorewrite with trace_rewrite. - exploit IHc; eauto. -Qed. -*) - Lemma simu_end_block: forall s1 t s1', starN (Mach.step (inv_trans_rao rao)) ge (Datatypes.S (dist_end_block s1)) s1 t s1' -> @@ -532,44 +539,25 @@ Proof. omega. } rewrite X in H; unfold size in H. - destruct b as [bh bb be]; simpl in * |- *. (* decomposition of starN in 3 parts: header + body + exit *) - destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H _ _ refl_equal) as [t3 [t4 [s1' [H0 [H3 H4]]]]]. + destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H _ _ refl_equal) as (t3&t4&s1'&H0&H3&H4). subst t; clear X H. - destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H0 _ _ refl_equal) as [t1 [t2 [s1'' [H [H1 H2]]]]]. + destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H0 _ _ refl_equal) as (t1&t2&s1''&H&H1&H2). subst t3; clear H0. + exploit trans_code_decompose; eauto. clear Heqtc. + intros (c0&c1&c2&Hc0&Hc1&Hc2&Heqtc). (* header steps *) exploit step_simu_header; eauto. - clear c Heqtc H; simpl; intros (c & X1 & X2 & X3); subst. - destruct X3 as [H|Heqtc]. - { subst. inversion H. subst. simpl in * |-. - inversion H1. subst. - inversion H3. subst. - autorewrite with trace_rewrite. - eapply ex_intro; intuition eauto. - eapply exec_bblock; simpl; eauto. - } - autorewrite with trace_rewrite. - (* body steps *) - exploit (star_step_simu_body_step); eauto. - clear H1; simpl; intros (rs' & m' & X1 & X2 & X3 & X4 & X5); subst. - elim TODO. (* A FAIRE *) - (* VIELLE PREUVE -- UTILE POUR S'INSPIRER !!! - - (* header steps *) - exploit step_simu_header; eauto. - intros [X1 X2]; subst s0 t1. + clear H; intros [X1 X2]; subst. (* body steps *) exploit (star_step_simu_body_step); eauto. - clear H1; intros [rs' [m' [H0 [H1 H2]]]]. - subst s1 t2. autorewrite with trace_rewrite. + clear H1; intros (rs'&m'&H0&H1&H2). subst. + autorewrite with trace_rewrite. (* exit step *) - subst tc0. - exploit step_simu_exit_step; eauto. clear H3. - intros (s2' & H3 & H4). + exploit step_simu_exit_step; eauto. + clear H3; intros (s2' & H3 & H4). eapply ex_intro; intuition eauto. - eapply exec_bblock; eauto. -*) + (* VIELLE PREUVE: eapply exec_bblock; eauto. *) + (* Callstate *) intros t s1' H; inversion_clear H. eapply ex_intro; constructor 1; eauto. @@ -591,7 +579,7 @@ Proof. inversion H1; subst; clear H1. inversion_clear H0; simpl. eapply exec_return. -Qed. +Admitted. (* A FIXER *) Theorem transf_program_correct: forward_simulation (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog). -- cgit