From 85dc46da493448a1d207ed5003ea476cd397b0d9 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 4 May 2021 22:24:33 +0200 Subject: finishing proofs and cleanup --- scheduling/BTLtoRTLproof.v | 182 ++++++++++++--------------------------------- 1 file changed, 48 insertions(+), 134 deletions(-) (limited to 'scheduling/BTLtoRTLproof.v') diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index f23bfcf8..da65d6ac 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -5,8 +5,8 @@ Require Import RTL Op Registers OptionMonad BTL. Require Import Errors Linking BTLtoRTL. -(*****************************) -(* Put this in an other file *) +(**********************************) +(* TODO Put this in an other file *) Require Import Linking. @@ -106,32 +106,22 @@ Proof. intros. inv H0. inv H. inv STACKS. constructor. Qed. -(* TODO copied from Duplicateproof.v *) -(*Lemma list_nth_z_dupmap: +(* Inspired from Duplicateproof.v *) +Lemma list_nth_z_dupmap: forall dupmap ln ln' (pc pc': node) val, - list_nth_z ln val = Some pc' -> - list_forall2 (fun n n' => dupmap!n' = Some n) ln ln' -> - exists pc', + list_nth_z ln val = Some pc -> + list_forall2 (fun n n' => dupmap!n = Some n') ln ln' -> + exists (pc': node), list_nth_z ln' val = Some pc' - /\ dupmap!pc' = Some pc. + /\ dupmap!pc = Some pc'. Proof. -Admitted. induction ln; intros until val; intros LNZ LFA. - inv LNZ. - inv LNZ. destruct (zeq val 0) eqn:ZEQ. + inv H0. destruct ln'; inv LFA. - simpl. exists p. split; auto. + simpl. exists n. split; auto. + inv LFA. simpl. rewrite ZEQ. exploit IHln. 2: eapply H0. all: eauto. - intros (pc'1 & LNZ & REV). exists pc'1. split; auto. congruence. - Qed.*) - -(* FIXME: unused ? -Definition is_goto (i: final): option exit := - match i with - | Bgoto pc => Some pc - | _ => None - end. -*) +Qed. (* variant of [star RTL.step] but requiring proposition [P] on the [refl] (stutttering) case. *) Inductive cond_star_step (P: Prop): RTL.state -> trace -> RTL.state -> Prop := @@ -150,6 +140,15 @@ Proof. eapply plus_trans; eauto. Qed. +Lemma css_star P s0 s1 t: + cond_star_step P s0 t s1 -> + star RTL.step tge s0 t s1. +Proof. + destruct 1. + - eapply star_refl; eauto. + - eapply plus_star; eauto. +Qed. + Local Hint Constructors RTL.step match_states: core. Local Hint Resolve css_refl plus_one transf_fundef_correct: core. @@ -230,16 +229,6 @@ Proof. eapply plus_trans; eauto. Qed. -(* TODO move above *) -Lemma css_star P s0 s1 t: - cond_star_step P s0 t s1 -> - star RTL.step tge s0 t s1. -Proof. - destruct 1. - - eapply star_refl; eauto. - - eapply plus_star; eauto. -Qed. - Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s (STACKS : list_forall2 match_stackframes stack stack') (TRANSF : match_function dupmap f f') @@ -269,7 +258,35 @@ Proof. eexists; split. eapply exec_Icall; eauto. simpl. rewrite symbols_preserved. rewrite GFS. eassumption. apply function_sig_translated. assumption. repeat (econstructor; eauto). -Admitted. + - (* tailcall *) + pose symbols_preserved as SYMPRES. + rename H2 into FIND. + destruct ri. + + simpl in FIND; apply functions_translated in FIND. + destruct FIND as (tf & cunit & TFUN & GFIND & LO). + eexists; split. eapply exec_Itailcall; eauto. + apply function_sig_translated. assumption. + erewrite <- preserv_fnstacksize; eauto. + repeat (econstructor; eauto). + + simpl in FIND. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate. + apply function_ptr_translated in FIND. destruct FIND as (tf & GFF & TF). + eexists; split. eapply exec_Itailcall; eauto. simpl. rewrite symbols_preserved. + rewrite GFS. eassumption. apply function_sig_translated. assumption. + erewrite <- preserv_fnstacksize; eauto. + repeat (econstructor; eauto). + - (* builtin *) + pose symbols_preserved as SYMPRES. + eexists. split. + eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_preserved; eauto. + eapply external_call_symbols_preserved; eauto. eapply senv_preserved. + econstructor; eauto. + - (* jumptable *) + pose symbols_preserved as SYMPRES. + exploit list_nth_z_dupmap; eauto. intros (pc'1 & LNZ & REVM). + eexists. split. + eapply exec_Ijumptable; eauto. + econstructor; eauto. +Qed. Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s (STACKS: list_forall2 match_stackframes stack stack') @@ -296,109 +313,6 @@ Proof. econstructor; eauto. Qed. -(* BROUILLON - -Lemma iblock_step_simulation_draft sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s - (STACKS: list_forall2 match_stackframes stack stack') - (TRANSF: match_function dupmap f f') - (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin)) - (MIB : match_iblock dupmap (RTL.fn_code f') true pc0 ib None) - (FS : final_step ge stack f sp rs1 m1 fin t s) - :exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'. -Proof. - intros; exploit iblock_istep_simulation; eauto. - simpl. intros (isfst' & pc1 & MI & STAR). - induction FS. - - inv MI. - + inv STAR; inv H3. - + inv STAR; try discriminate. - eexists; split. eauto. - econstructor; eauto. - - - inv MI. pose symbols_preserved as SYMPRES. - inv STAR. - + inv H5. eexists; split. - eapply plus_one. eapply exec_Ijumptable; eauto. - exploit list_nth_z_dupmap; eauto. intros (pc'1 & LNZ & REVM). - eexists. split. - + eapply exec_Ijumptable; eauto. - + econstructor; eauto. - - admit. -Admitted. - - -Inductive iblock_istep_gen sp dupmap stack f pc0 cfg ib: trace -> bool -> option final -> option node -> Prop := - | ibis_synced opc pc1 - (HOPC: opc = Some pc1) - (MIB : match_iblock dupmap cfg true pc0 ib opc) - : iblock_istep_gen sp dupmap stack f pc0 cfg ib E0 true None opc - | ibis_stutter rs1 m1 fin ofin s t - (HFIN: ofin = Some fin) - (MIB : match_iblock dupmap cfg false pc0 ib None) - (FS : final_step ge stack f sp rs1 m1 fin t s) - : iblock_istep_gen sp dupmap stack f pc0 cfg ib t false ofin None. - -Lemma iblock_step_simulation - sp dupmap stack stack' f f' rs0 m0 rs1 m1 ib ofin pc0 opc t s isfst - (STACKS: list_forall2 match_stackframes stack stack') - (TRANSF: match_function dupmap f f') - (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin) - (*(MIB : match_iblock dupmap cfg' isfst pc0 ib opc)*) - (*(FS : final_step ge stack f sp rs1 m1 fin t s)*) -(*FNC : (fn_code f) ! pc = Some ib*) - (IBGEN: iblock_istep_gen sp dupmap stack f pc0 (RTL.fn_code f') ib t isfst ofin opc) - :exists s', (if isfst then plus RTL.step else star RTL.step) tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'. -Proof. - (* TODO: généraliser ce lemme pour pouvoir le prouver par induction sur IBIS: - => il faut en particulier généraliser l'hypothèse MIB qui relie le iblock_istep ib en cours d'exécution. - avec le code RTL à partir de pc0. - => ici, le "isfst" a déjà été généralisé: quand il vaut "false", ça veut dire qu'on a le droit de faire du "stuttering" côté RTL. - => il reste à comprendre comment généraliser le "None" en "opc" - ainsi que l'hypothese OFIN pour autoriser le cas "ofin=None" (nécessaire pour l'induction). - Idée: si "ofin = None" alors il y a un pc1 tq "opc = Some pc1" qui permet d'exécuter la suite du bloc... - - Au final, il faut sans doute introduire un "Inductive" pour capturer ces idées dans un prédicat "lisible"/"manipulable"... - *) - (* XXX keep IBIS, MIB, and FS ? *) - induction IBIS. - - admit. - - inv IBGEN; try_simplify_someHyps. - inv MIB. eexists; split. - apply plus_one. econstructor; eauto. - (* - - inversion IBGEN; subst; try_simplify_someHyps. - exploit iblock_istep_simulation; eauto. - inv MIB. - eexists. split. apply plus_one. - eapply exec_Inop; eauto. - try_simplify_someHyps. - admit. - - (* exec_op *) - admit. (* cas absurde car hypothese OFIN trop restrictive *) - - (* exec_load_TRAP *) - admit. (* cas absurde car hypothese OFIN trop restrictive *) - - (* exec_load_store *) - admit. (* cas absurde car hypothese OFIN trop restrictive *) - - (* exec_seq_stop *) - (*inv MIB.*) - eapply IHIBIS; eauto. - (* TODO: c'est ici qu'on voit que l'hypothèse MIB est trop restrictive actuellement - normalement, l'hypothèse d'induction IHIBIS devrait permettre de conclure quasi-directement ici. - *) - admit. - - (* exec_seq_continue *) - (* TODO: ici l'hypothèse d'induction IHIBIS1 n'est pas utilisable à cause de OFIN trop restrictive *) - try_simplify_someHyps. - (*inv MIB.*) - admit. - - (* exec_cond *) - try_simplify_someHyps. - (*inv MIB.*) - admit.*) -Admitted. - -*) - Theorem plus_simulation s1 t s1': step ge s1 t s1' -> forall s2 (MS: match_states s1 s2), -- cgit