From 3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 21 May 2021 21:18:59 +0200 Subject: Now supporting Bnop insertion in conditions --- scheduling/BTLtoRTLproof.v | 29 ++++++++++++++++++++--------- 1 file changed, 20 insertions(+), 9 deletions(-) (limited to 'scheduling/BTLtoRTLproof.v') diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 9b37d8fa..2e8d960c 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -202,6 +202,17 @@ Proof. eapply plus_trans; eauto. Qed. +Lemma css_E0_trans isfst isfst' s0 s1 s2: + cond_star_step (isfst=false) s0 E0 s1 -> + cond_star_step (false=isfst') s1 E0 s2 -> + cond_star_step (isfst=isfst') s0 E0 s2. +Proof. + intros S1 S2. + inversion S1; subst; eauto. + inversion S2; subst; eauto. + eapply css_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. @@ -219,7 +230,7 @@ Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin forall pc0 opc isfst (MIB: match_iblock dupmap (RTL.fn_code f') isfst pc0 ib opc), 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) + | None => exists pc1,(opc = Some pc1) /\ cond_star_step (isfst = false) (RTL.State stack' f' sp pc0 rs0 m0) E0 (RTL.State stack' f' sp pc1 rs1 m1) | Some fin => 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) @@ -231,19 +242,19 @@ Proof. subst. repeat eexists; eauto. - (* exec_nop *) - inv MIB. exists pc'; split; eauto. + inv MIB; eexists; split; econstructor; eauto. - (* exec_op *) - inv MIB. exists pc'; split; auto. + inv MIB. exists pc'; split; auto; constructor. apply plus_one. eapply exec_Iop; eauto. erewrite <- eval_operation_preserved; eauto. intros; rewrite symbols_preserved; trivial. - (* exec_load *) - inv MIB. exists pc'; split; auto. + inv MIB. exists pc'; split; auto; constructor. apply plus_one. eapply exec_Iload; eauto. erewrite <- eval_addressing_preserved; eauto. intros; rewrite symbols_preserved; trivial. - (* exec_store *) - inv MIB. exists pc'; split; auto. + inv MIB. exists pc'; split; auto; constructor. apply plus_one. eapply exec_Istore; eauto. erewrite <- eval_addressing_preserved; eauto. intros; rewrite symbols_preserved; trivial. @@ -257,10 +268,10 @@ Proof. destruct ofin; simpl. + intros (ifst2 & pc2 & iinfo & M2 & STEP2). repeat eexists; eauto. - eapply css_plus_trans; eauto. + eapply css_E0_trans; eauto. + intros (pc2 & EQpc2 & STEP2); inv EQpc2. eexists; split; auto. - eapply plus_trans; eauto. + eapply css_E0_trans; eauto. - (* exec_cond *) inv MIB. rename H10 into JOIN. (* is_join_opt opc1 opc2 opc *) @@ -275,7 +286,7 @@ Proof. intros (pc1 & OPC & PLUS). inv OPC. inv JOIN; eexists; split; eauto. all: - eapply plus_trans; eauto. + eapply css_plus_trans; eauto. + (* taking ifnot *) destruct ofin; simpl. * (* ofin is Some final *) @@ -286,7 +297,7 @@ Proof. intros (pc1 & OPC & PLUS). subst. inv JOIN; eexists; split; eauto. all: - eapply plus_trans; eauto. + eapply css_plus_trans; eauto. Qed. Lemma final_simu_except_goto sp dupmap stack stack' f f' rs1 m1 pc1 fin t s -- cgit