diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-04 11:55:23 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-04 11:55:23 +0200 |
| commit | 6e7822b5313eaa01478530a5c47cc0d8f3776681 (patch) | |
| tree | 402ad7334ef431bb88b51615d0a2f205f52cf27e /scheduling/BTLtoRTLproof.v | |
| parent | d44d44c8fffbd85d501e30b7dfdf93683ed9bb4d (diff) | |
| download | compcert-kvx-6e7822b5313eaa01478530a5c47cc0d8f3776681.tar.gz compcert-kvx-6e7822b5313eaa01478530a5c47cc0d8f3776681.zip | |
Some try in step_simulation
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 23 |
1 files changed, 20 insertions, 3 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 8df8ef1e..bfc09d65 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -131,7 +131,6 @@ Proof. eapply plus_trans; eauto. Qed. -(* suggestion *) Lemma iblock_istep_simulation sp dupmap stack' f' rs0 m0 ib rs1 m1 ofin (IBIS: iblock_istep ge sp rs0 m0 ib rs1 m1 ofin): forall pc0 opc isfst @@ -220,7 +219,26 @@ 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. + 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. + 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. Admitted. (* BROUILLON @@ -328,7 +346,6 @@ Proof. + eapply plus_one. constructor. + inv H1. econstructor; eauto. Qed. -(* Admitted. *) Theorem transf_program_correct: forward_simulation (semantics prog) (RTL.semantics tprog). |