diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-20 11:58:40 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-20 11:58:40 +0200 |
| commit | 2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10 (patch) | |
| tree | b997c709ea92723f55b23b9b2eb23235b6e70dd6 /scheduling/BTLtoRTLproof.v | |
| parent | f37547880890ec7ff2acfba89848944d492ce9ad (diff) | |
| download | compcert-kvx-2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10.tar.gz compcert-kvx-2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10.zip | |
Changing to an opaq record in BTL info, this is a broken commit
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 16 |
1 files changed, 8 insertions, 8 deletions
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. |