From b063fb03af84483671833d40491f4fa8d2c8b4c9 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 23 Jul 2021 18:25:00 +0200 Subject: non trapping loads --- scheduling/RTLtoBTLproof.v | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'scheduling/RTLtoBTLproof.v') diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 8a352434..13ba5a29 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -123,12 +123,15 @@ Lemma normRTLrec_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin1: iblock_istep tge sp rs0 m0 (normRTLrec ib k) rs2 m2 ofin2. Proof. induction 1; simpl; intuition subst; eauto. - { (* Bnop *) autodestruct; eauto. } - 1-3: (* Bop, Bload, Bstore *) - intros; repeat econstructor; eauto. - (* Bcond *) - destruct ofin; intuition subst; - destruct b; eapply IHISTEP; eauto. + - (* Bnop *) autodestruct; eauto. + - (* Bop *) repeat econstructor; eauto. + - (* Bload *) inv LOAD. + + repeat econstructor; eauto. + + do 2 (econstructor; eauto). + eapply has_loaded_default; eauto. + - (* Bcond *) repeat econstructor; eauto. + destruct ofin; intuition subst; + destruct b; eapply IHISTEP; eauto. Qed. Lemma normRTL_iblock_istep_correct tge sp ib rs0 m0 rs1 m1 ofin: -- cgit