diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-21 21:18:59 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-21 21:18:59 +0200 |
| commit | 3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a (patch) | |
| tree | abbb54fca752a15a190e66dcb902a42b0be97cd9 /scheduling/BTLtoRTLproof.v | |
| parent | 65247b67cbd469b9cd3bea22410bd11af450696c (diff) | |
| download | compcert-kvx-3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a.tar.gz compcert-kvx-3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a.zip | |
Now supporting Bnop insertion in conditions
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 29 |
1 files changed, 20 insertions, 9 deletions
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 |