diff options
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 32 |
1 files changed, 31 insertions, 1 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 31652697..8df8ef1e 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -179,7 +179,37 @@ Proof. eapply plus_trans; eauto. - inv MIB. destruct b; exploit IHIBIS; eauto. -Admitted. + + (* taking ifso *) + destruct ofin; simpl. + * (* ofin is Some final *) + intros (isfst' & pc1 & MI & STAR). + repeat eexists; eauto. + eapply css_plus_trans. + eapply plus_one. eapply exec_Icond; eauto. + eauto. + * (* ofin is None *) + intros (pc1 & OPC & PLUS). inv OPC. + inv H10; eexists; split; eauto. + all: + eapply plus_trans; + [ eapply plus_one; eapply exec_Icond; eauto + | eauto | eauto ]. + + (* taking ifnot *) + destruct ofin; simpl. + * (* ofin is Some final *) + intros (isfst' & pc1 & MI & STAR). + repeat eexists; eauto. + eapply css_plus_trans. + eapply plus_one. eapply exec_Icond; eauto. + eauto. + * (* ofin is None *) + intros (pc1 & OPC & PLUS). inv OPC. + inv H10; eexists; split; eauto. + all: + eapply plus_trans; + [ eapply plus_one; eapply exec_Icond; eauto + | eauto | eauto ]. +Qed. Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fin t s (STACKS: list_forall2 match_stackframes stack stack') |