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/BTLmatchRTL.v | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) (limited to 'scheduling/BTLmatchRTL.v') diff --git a/scheduling/BTLmatchRTL.v b/scheduling/BTLmatchRTL.v index a59c847e..c271ae02 100644 --- a/scheduling/BTLmatchRTL.v +++ b/scheduling/BTLmatchRTL.v @@ -48,11 +48,15 @@ Proof. do 2 eexists; rewrite EVAL'. repeat (split; eauto). eapply set_reg_lessdef; eauto. - (* Bload *) - exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto. - intros (v2 & EVAL' & LESSDEF). exploit Mem.loadv_extends; eauto. - intros (v3 & LOAD' & LESSDEF'). - do 2 eexists; rewrite EVAL', LOAD'. repeat (split; eauto). - eapply set_reg_lessdef; eauto. + inv LOAD. + + exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto. + intros (v2 & EVAL' & LESSDEF). exploit Mem.loadv_extends; eauto. + intros (v3 & LOAD' & LESSDEF'); autodestruct; + do 2 eexists; rewrite EVAL', LOAD'; + repeat (split; eauto); eapply set_reg_lessdef; eauto. + + destruct (eval_addressing ge sp addr rs ## args) eqn:EQA; + repeat autodestruct; do 2 eexists; + repeat (split; eauto); eapply set_reg_lessdef; eauto. - (* Bstore *) exploit (@eval_addressing_lessdef _ _ ge sp addr (rs ## args)); eauto. intros (v2 & EVAL' & LESSDEF). exploit Mem.storev_extends; eauto. -- cgit