diff options
| author | Léo Gourdin <leo.gourdin@lilo.org> | 2021-07-27 11:22:33 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@lilo.org> | 2021-07-27 11:22:33 +0200 |
| commit | 70ed73cba9347b398c509488051ae54d193eb875 (patch) | |
| tree | 0dfe7586746d4d8acd76ddf28512abc8d94e4188 /scheduling/BTLmatchRTL.v | |
| parent | 0b076ef6eb5553be43ce81c27e438f632b17cb32 (diff) | |
| parent | b063fb03af84483671833d40491f4fa8d2c8b4c9 (diff) | |
| download | compcert-kvx-70ed73cba9347b398c509488051ae54d193eb875.tar.gz compcert-kvx-70ed73cba9347b398c509488051ae54d193eb875.zip | |
Merge branch 'BTL-SEimpl' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into BTL-SEimpl
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. |