diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-23 18:25:00 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-23 18:25:00 +0200 |
| commit | b063fb03af84483671833d40491f4fa8d2c8b4c9 (patch) | |
| tree | 89033ebd4ec906091d31457b0b7f3c8539e11dc1 /scheduling/BTLmatchRTL.v | |
| parent | 8de8dc6616c49018c6151887f76ea08c8f1ff04e (diff) | |
| download | compcert-kvx-b063fb03af84483671833d40491f4fa8d2c8b4c9.tar.gz compcert-kvx-b063fb03af84483671833d40491f4fa8d2c8b4c9.zip | |
non trapping loads
Diffstat (limited to 'scheduling/BTLmatchRTL.v')
| -rw-r--r-- | scheduling/BTLmatchRTL.v | 14 |
1 files changed, 9 insertions, 5 deletions
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. |