From 92cca153569e44cd11ba3d1b68c2708c0cc46899 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 28 Jul 2021 17:00:02 +0200 Subject: ci fix? --- scheduling/BTLmatchRTL.v | 13 ++++++------- scheduling/BTLtoRTLproof.v | 2 ++ scheduling/RTLtoBTLproof.v | 27 +++++++++------------------ 3 files changed, 17 insertions(+), 25 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v index c271ae02..07131893 100644 --- a/scheduling/BTLmatchRTL.v +++ b/scheduling/BTLmatchRTL.v @@ -214,9 +214,9 @@ Inductive match_iblock (dupmap: PTree.t node) (cfg: RTL.code): bool -> node -> i | mib_op isfst pc pc' op lr r iinfo: cfg!pc = Some (Iop op lr r pc') -> match_iblock dupmap cfg isfst pc (Bop op lr r iinfo) (Some pc') - | mib_load isfst pc pc' m a lr r iinfo: - cfg!pc = Some (Iload TRAP m a lr r pc') -> - match_iblock dupmap cfg isfst pc (Bload TRAP m a lr r iinfo) (Some pc') + | mib_load isfst pc pc' trap m a lr r iinfo: + cfg!pc = Some (Iload trap m a lr r pc') -> + match_iblock dupmap cfg isfst pc (Bload trap m a lr r iinfo) (Some pc') | mib_store isfst pc pc' m a lr r iinfo: cfg!pc = Some (Istore m a lr r pc') -> match_iblock dupmap cfg isfst pc (Bstore m a lr r iinfo) (Some pc') @@ -407,7 +407,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) | Bload tm m a lr r _ => match cfg!pc with | Some (Iload tm' m' a' lr' r' pc') => - if (trapping_mode_eq tm TRAP && trapping_mode_eq tm' TRAP) then + if (trapping_mode_eq tm tm') then if (chunk_eq m m') then if (eq_addressing a a') then if (list_eq_dec Pos.eq_dec lr lr') then @@ -417,7 +417,7 @@ Fixpoint verify_block (dupmap: PTree.t node) cfg isfst pc ib : res (option node) else Error (msg "BTL.verify_block: different lr in Bload") else Error (msg "BTL.verify_block: different addressing in Bload") else Error (msg "BTL.verify_block: different chunk in Bload") - else Error (msg "BTL.verify_block: NOTRAP trapping_mode unsupported in Bload") + else Error (msg "BTL.verify_block: different trapping_mode in Bload") | _ => Error (msg "BTL.verify_block: incorrect cfg Bload") end | Bstore m a lr r _ => @@ -520,8 +520,7 @@ Proof. constructor; assumption. - (* Bload *) destruct i; try discriminate. - do 2 (destruct (trapping_mode_eq _ _); try discriminate). - simpl in H. + destruct (trapping_mode_eq _ _); try discriminate. destruct (chunk_eq _ _); try discriminate. destruct (eq_addressing _ _); try discriminate. destruct (list_eq_dec _ _ _); try discriminate. diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 324f1d14..4ef55928 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -232,6 +232,8 @@ Proof. inv MIB. exists pc'; split; auto; constructor. apply plus_one. inv LOAD. eapply exec_Iload; eauto. + 2: destruct (eval_addressing _ _ _ _) eqn:EVAL; + [ eapply exec_Iload_notrap2 | eapply exec_Iload_notrap1]; eauto. all: erewrite <- eval_addressing_preserved; eauto; intros; rewrite symbols_preserved; trivial. - (* exec_store *) 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. -- cgit