diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-03 13:57:37 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-03 13:57:37 +0200 |
commit | c04a5f66c87f3b4483790ae41901f01386d0ce70 (patch) | |
tree | ec4e3c7f55129d298da3e5422a16296a9d88e5a6 /scheduling/BTLtoRTLproof.v | |
parent | cc5f8c4e4d71d824a4d1818745d6bf1015b98f98 (diff) | |
parent | c8b2438685f1a6c4a98cf58727d32a9e474c4f34 (diff) | |
download | compcert-kvx-c04a5f66c87f3b4483790ae41901f01386d0ce70.tar.gz compcert-kvx-c04a5f66c87f3b4483790ae41901f01386d0ce70.zip |
Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
-rw-r--r-- | scheduling/BTLtoRTLproof.v | 57 |
1 files changed, 22 insertions, 35 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index ab3cab69..97ac75fb 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -120,28 +120,26 @@ Proof. induction IBIS; simpl; auto. Admitted. -Inductive iblock_istep_gen sp dupmap stack f rs0 m0 pc0 cfg: state -> trace -> bool -> option final -> option node -> Prop := - | ibis_synced ib rs1 m1 opc pc1 - (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 None) +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 rs0 m0 pc0 cfg (State stack f sp pc0 rs0 m0) E0 true None opc - | ibis_stutter ib rs1 m1 fin ofin s t - (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 (Some fin)) + : 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 rs0 m0 pc0 cfg s t false ofin None. + : 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 ofin pc0 opc t s isfst + 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)*) + (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 rs0 m0 pc0 (RTL.fn_code f') s t isfst ofin opc) + (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: @@ -155,35 +153,24 @@ Proof. 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 IBGEN. - - inv IBIS. - + inv MIB. - eexists. split. apply plus_one. - eapply exec_Inop; eauto. - econstructor; eauto. - try_simplify_someHyps. - admit. - + admit. - + admit. - + admit. - + admit. - + admit. - - admit. - (* induction IBIS. + induction IBIS. - (* exec_final *) try_simplify_someHyps. (* TODO: introduire un lemme pour ce cas specifique ? *) admit. - - (* exec_nop *) - try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *) + - inversion IBGEN; subst; try_simplify_someHyps. + inv MIB. + eexists. split. apply plus_one. + eapply exec_Inop; eauto. + try_simplify_someHyps. + admit. - (* exec_op *) - try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *) + admit. (* cas absurde car hypothese OFIN trop restrictive *) - (* exec_load_TRAP *) - try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *) + admit. (* cas absurde car hypothese OFIN trop restrictive *) - (* exec_load_store *) - try_simplify_someHyps. (* cas absurde car hypothese OFIN trop restrictive *) + admit. (* cas absurde car hypothese OFIN trop restrictive *) - (* exec_seq_stop *) - try_simplify_someHyps. - inv MIB. + (*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. @@ -192,12 +179,12 @@ Proof. - (* 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. + (*inv MIB.*) admit. - (* exec_cond *) try_simplify_someHyps. - inv MIB. - admit.*) + (*inv MIB.*) + admit. Admitted. Theorem plus_simulation s1 t s1': |