diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-24 22:41:35 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-05-24 22:41:35 +0200 |
commit | 51ec982b84851ac3526a0cb3f22e41f974b2d592 (patch) | |
tree | 137124a7cf7e3604e71124aa5957923412c5069d /scheduling/BTL.v | |
parent | 0efe7783c50d72858352fda93d30e0f52792d658 (diff) | |
download | compcert-kvx-51ec982b84851ac3526a0cb3f22e41f974b2d592.tar.gz compcert-kvx-51ec982b84851ac3526a0cb3f22e41f974b2d592.zip |
tiny simplifications in RTLtoBTLproof
Diffstat (limited to 'scheduling/BTL.v')
-rw-r--r-- | scheduling/BTL.v | 92 |
1 files changed, 1 insertions, 91 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 0f9ef44f..97c54021 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -810,94 +810,4 @@ Definition is_goto (ib: iblock): bool := match ib with | BF (Bgoto _) _ => true | _ => false - end. - -Definition is_RTLatom (ib: iblock): bool := - match ib with - | Bseq _ _ | Bcond _ _ _ _ _ | Bnop None => false - | _ => true - end. - -Definition Bnop_dec k: { k=Bnop None} + { k<>(Bnop None) }. -Proof. - destruct k; simpl; try destruct oiinfo; - intuition congruence. -Defined. - -(** Is expand property to only support atomic instructions on the left part of a Bseq: - The tree is right-expanded, and block are normalized to simplify RTL simulation *) -Inductive is_expand: iblock -> Prop := - | exp_Bseq ib1 ib2: - is_RTLatom ib1 = true -> - is_expand ib2 -> - is_expand (Bseq ib1 ib2) - | exp_Bcond cond args ib1 ib2 i: - is_expand ib1 -> - is_expand ib2 -> - is_expand (Bcond cond args ib1 ib2 i) - | exp_others ib: - is_RTLatom ib = true -> - is_expand ib - . -Local Hint Constructors is_expand: core. - -(** The weak version with more specific hypothesis for conditions *) -Inductive is_wexpand: iblock -> Prop := - | wexp_Bseq ib1 ib2: - is_RTLatom ib1 = true -> - is_wexpand ib2 -> - is_wexpand (Bseq ib1 ib2) - | wexp_Bcond cond args ib1 ib2 iinfo: - (ib1 <> Bnop None -> is_wexpand ib1) -> - (ib2 <> Bnop None -> is_wexpand ib2) -> - is_wexpand (Bcond cond args ib1 ib2 iinfo) - | wexp_others ib: - is_RTLatom ib = true -> - is_wexpand ib - . -Local Hint Constructors is_wexpand: core. - -Fixpoint normRTL (ib: iblock) (k: iblock): iblock := - match ib with - | Bseq ib1 ib2 => normRTL ib1 (normRTL ib2 k) - | Bcond cond args ib1 ib2 iinfo => - Bcond cond args (normRTL ib1 k) (normRTL ib2 k) iinfo - | BF fin iinfo => BF fin iinfo - | Bnop None => k - | ib => - if Bnop_dec k then ib else Bseq ib k - end. - -Lemma normRTL_correct ib: forall k, - (k <> (Bnop None) -> is_wexpand k) -> - (normRTL ib k) <> Bnop None -> - is_wexpand (normRTL ib k). -Proof. - induction ib; simpl; intros; try autodestruct; auto. - intros; destruct (Bnop_dec k); auto. -Qed. - -Lemma is_join_opt_None {A} (opc1 opc2: option A): - is_join_opt opc1 opc2 None -> opc1 = None /\ opc2 = None. -Proof. - intros X. inv X; auto. -Qed. - -Lemma match_iblock_None_not_Bnop dupmap cfg isfst pc ib: - match_iblock dupmap cfg isfst pc ib None -> ib <> Bnop None. -Proof. - intros X; inv X; try congruence. -Qed. -Local Hint Resolve match_iblock_None_not_Bnop: core. - -Lemma is_wexpand_expand dupmap cfg ib: - is_wexpand ib -> - forall isfst pc - (MIB: match_iblock dupmap cfg isfst pc ib None), - is_expand ib. -Proof. - induction 1; simpl; intros; auto; try (inv MIB); eauto. - (* Bcond *) - destruct (is_join_opt_None opc1 opc2); subst; eauto. - econstructor; eauto. -Qed. + end.
\ No newline at end of file |