diff options
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 27 |
1 files changed, 9 insertions, 18 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 13ba5a29..0ca93bce 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -624,26 +624,17 @@ Proof. - (* mib_seq *) inv IS_EXPD; try discriminate. inv H; simpl in *; try congruence; - inv STEP; try_simplify_someHyps; eauto. - + (* Bnop is_rtl *) - intros; eapply match_strong_state_simu; eauto. - + (* Bop *) - intros; eapply match_strong_state_simu; eauto. - econstructor; eauto. + inv STEP; try_simplify_someHyps; + intros; eapply match_strong_state_simu; eauto; + econstructor; eauto. + { (* Bop *) erewrite eval_operation_preserved in H12. erewrite H12 in BTL_RUN; simpl in BTL_RUN; auto. - intros; rewrite <- symbols_preserved; trivial. - + (* Bload *) - intros; eapply match_strong_state_simu; eauto. - econstructor; eauto. - erewrite eval_addressing_preserved in H12. - erewrite H12, H13 in BTL_RUN; simpl in BTL_RUN; auto. - intros; rewrite <- symbols_preserved; trivial. - + (* Bstore *) - intros; eapply match_strong_state_simu; eauto. - econstructor; eauto. - erewrite eval_addressing_preserved in H12. - erewrite H12, H13 in BTL_RUN; simpl in BTL_RUN; auto. + intros; rewrite <- symbols_preserved; trivial. } + all: (* Bload / Bstore *) + erewrite eval_addressing_preserved in H12; + try erewrite H12 in BTL_RUN; try erewrite H13 in BTL_RUN; + simpl in BTL_RUN; try destruct trap; auto; intros; rewrite <- symbols_preserved; trivial. - (* mib_cond *) inv IS_EXPD; try discriminate. |