diff options
-rw-r--r-- | scheduling/BTLtoRTLproof.v | 47 |
1 files changed, 31 insertions, 16 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 8f892020..ef640d22 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -106,6 +106,12 @@ Proof. intros. inv H0. inv H. inv STACKS. constructor. Qed. +Definition is_goto (i: final): option exit := + match i with + | Bgoto pc => Some pc + | _ => None + end. + (* suggestion *) Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin): @@ -114,11 +120,14 @@ Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin , match ofin with | None => exists pc1,(opc = Some pc1) /\ plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) - | Some fin => True (* TODO: A CHANGER *) + | Some fin => + (* A CHANGER ? *) + exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin opc + /\ star RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) end. Proof. - induction IBIS; simpl; auto; - intros. + induction IBIS; simpl; intros. + - repeat econstructor; eauto. - inv MIB. exists pc'; split; auto. apply plus_one. apply exec_Inop; trivial. - inv MIB. exists pc'; split; auto. @@ -133,19 +142,25 @@ Proof. apply plus_one. eapply exec_Istore; eauto. erewrite <- eval_addressing_preserved; eauto. intros; rewrite symbols_preserved; trivial. - - - destruct ofin; simpl; auto. - inv MIB. - admit. - (*eexists; split; auto.*) - (*apply IHIBIS2.*) - (*inv MIB. exists pc'; split; auto.*) - (*apply plus_one. eapply exec_Istore; eauto.*) - (*erewrite <- eval_addressing_preserved; eauto.*) - (*intros; rewrite symbols_preserved; trivial.*) - - destruct ofin; simpl; auto. inv MIB. - destruct b. - eapply IHIBIS. + - inv MIB. + exploit IHIBIS; eauto. + intros (isfst' & pc1 & M1 & STAR). + inv M1. + - inv MIB. + exploit IHIBIS1; eauto. + intros (pc1 & EQpc1 & STEP1); inv EQpc1. + exploit IHIBIS2; eauto. + destruct ofin; simpl. + + intros (ifst2 & pc2 & M2 & STEP2). + repeat eexists; eauto. + eapply star_trans; eauto. + eapply plus_star; eauto. + eauto. + + intros (pc2 & EQpc2 & STEP2); inv EQpc2. + eexists; split; auto. + eapply plus_trans; eauto. + - inv MIB. + destruct b; exploit IHIBIS; eauto. Admitted. Inductive iblock_istep_gen sp dupmap stack f pc0 cfg ib: trace -> bool -> option final -> option node -> Prop := |