diff options
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 43 |
1 files changed, 27 insertions, 16 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 14e986aa..46f360c5 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -58,11 +58,11 @@ Qed. Lemma transf_function_correct f f': transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. -Proof. +Proof. Admitted. (* unfold transf_function; unfold bind. repeat autodestruct. intros H _ _ X. inversion X; subst; clear X. eexists; eapply verify_function_correct; simpl; eauto. -Qed. + Qed.*) Lemma transf_fundef_correct f f': transf_fundef f = OK f' -> match_fundef f f'. @@ -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,9 +230,9 @@ 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, 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. @@ -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. @@ -255,12 +266,12 @@ 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. + 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 *) @@ -268,25 +279,25 @@ Proof. + (* 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 *) 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 *) - intros (isfst' & pc1 & MI & STAR). + intros (isfst' & pc1 & iinfo' & MI & STAR). repeat eexists; eauto. eapply css_plus_trans; eauto. * (* ofin is None *) 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 @@ -342,7 +353,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. |