diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-04 12:37:54 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-04 12:37:54 +0200 |
| commit | f592b3b46908a97e2181f270cf631e9f8d60d726 (patch) | |
| tree | e005bff3eb641e9e77d3fb7efd14371ecd79897a /scheduling/BTLtoRTLproof.v | |
| parent | 6e7822b5313eaa01478530a5c47cc0d8f3776681 (diff) | |
| download | compcert-kvx-f592b3b46908a97e2181f270cf631e9f8d60d726.tar.gz compcert-kvx-f592b3b46908a97e2181f270cf631e9f8d60d726.zip | |
one example case on main proof
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 38 |
1 files changed, 20 insertions, 18 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index bfc09d65..94ec84bf 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -219,26 +219,28 @@ Lemma iblock_step_simulation sp dupmap stack stack' f f' ib rs0 m0 rs1 m1 pc0 fi :exists s', plus RTL.step tge (RTL.State stack' f' sp pc0 rs0 m0) t s' /\ match_states s s'. Proof. intros; exploit iblock_istep_simulation; eauto. - simpl. intros (isfst' & pc1 & MI & STAR). inv MI. - - (* Final instruction except Bgoto *) - inv FS. - + (* absurd case *) inv H3. - + inv H3. inv STAR. - * - eexists; split. eapply plus_one. - eapply exec_Ireturn; eauto. + simpl. intros (isfst' & pc1 & MI & STAR). + induction FS. + - inv MI. + + inv STAR; inv H3. + + inv STAR; try discriminate. + eexists; split. eauto. + econstructor; eauto. + - inv MI. + inv STAR. + + inv H5. eexists; split. + eapply plus_one. eapply exec_Ireturn; eauto. erewrite <- preserv_fnstacksize; eauto. econstructor; eauto. - * inv H. - admit. - + admit. - + admit. - + admit. - + admit. - - (* Bgoto *) - inv STAR; try discriminate. inv FS. - eexists; split. eauto. - econstructor; eauto. + + inv H5. eexists; split. + eapply plus_trans. eauto. + eapply plus_one. eapply exec_Ireturn; eauto. + erewrite <- preserv_fnstacksize; eauto. eauto. + econstructor; eauto. + - admit. + - admit. + - admit. + - admit. Admitted. (* BROUILLON |