From 2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 20 May 2021 11:58:40 +0200 Subject: Changing to an opaq record in BTL info, this is a broken commit --- scheduling/BTLtoRTLproof.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'scheduling/BTLtoRTLproof.v') diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 6c894b78..9b37d8fa 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -221,7 +221,7 @@ 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 => - exists isfst' pc1, match_iblock dupmap (RTL.fn_code f') isfst' pc1 fin None + exists isfst' pc1 iinfo, match_iblock dupmap (RTL.fn_code f') isfst' pc1 (BF fin iinfo) None /\ cond_star_step (isfst = isfst') (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) end. Proof. @@ -255,7 +255,7 @@ Proof. intros (pc1 & EQpc1 & STEP1); inv EQpc1. exploit IHIBIS2; eauto. destruct ofin; simpl. - + intros (ifst2 & pc2 & M2 & STEP2). + + intros (ifst2 & pc2 & iinfo & M2 & STEP2). repeat eexists; eauto. eapply css_plus_trans; eauto. + intros (pc2 & EQpc2 & STEP2); inv EQpc2. @@ -263,12 +263,12 @@ Proof. eapply plus_trans; eauto. - (* exec_cond *) inv MIB. - rename H11 into JOIN. (* is_join_opt opc1 opc2 opc *) + rename H10 into JOIN. (* is_join_opt opc1 opc2 opc *) destruct b; exploit IHIBIS; eauto. + (* taking ifso *) destruct ofin; simpl. * (* ofin is Some final *) - intros (isfst' & pc1 & MI & STAR). + intros (isfst' & pc1 & iinfo' & MI & STAR). repeat eexists; eauto. eapply css_plus_trans; eauto. * (* ofin is None *) @@ -279,7 +279,7 @@ Proof. + (* taking ifnot *) destruct ofin; simpl. * (* ofin is Some final *) - intros (isfst' & pc1 & MI & STAR). + intros (isfst' & pc1 & iinfo' & MI & STAR). repeat eexists; eauto. eapply css_plus_trans; eauto. * (* ofin is None *) @@ -305,14 +305,14 @@ Proof. erewrite <- preserv_fnstacksize; eauto. econstructor; eauto. - (* call *) - rename H8 into FIND. + rename H7 into FIND. exploit find_function_preserved; eauto. intros (fd' & FIND' & TRANSFU). eexists; split. eapply exec_Icall; eauto. apply function_sig_translated. assumption. repeat (econstructor; eauto). - (* tailcall *) - rename H3 into FIND. + rename H2 into FIND. exploit find_function_preserved; eauto. intros (fd' & FIND' & TRANSFU). eexists; split. eapply exec_Itailcall; eauto. @@ -342,7 +342,7 @@ Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fi : 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). clear IBIS MIB. + simpl. intros (isfst' & pc1 & iinfo & MI & STAR). clear IBIS MIB. inv MI. - (* final inst except goto *) exploit final_simu_except_goto; eauto. -- cgit