diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-30 16:52:21 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-04-30 16:52:21 +0200 |
| commit | 989e85b700161867c2f80df55c2dfaaaa5fe82b4 (patch) | |
| tree | 0e00fd1577a470cfbb19de49926274f8b70abb64 /scheduling/BTLtoRTLproof.v | |
| parent | af2c82cfd7f2318fcd81da2ea4cf3fd695db3b40 (diff) | |
| download | compcert-kvx-989e85b700161867c2f80df55c2dfaaaa5fe82b4.tar.gz compcert-kvx-989e85b700161867c2f80df55c2dfaaaa5fe82b4.zip | |
BTLtoRTL: proof for internal/external/return states
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 26b5bae6..a3be20b5 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -112,6 +112,31 @@ Theorem plus_simulation s1 t s1': exists s2', plus RTL.step tge s2 t s2' /\ match_states s1' s2'. +Proof. + induction 1; intros; inv MS. + - eapply dupmap_correct in DUPLIC; eauto. + destruct DUPLIC as (ib' & FNC & MIB). + inv H0. destruct H1 as (m' & fin & IBIS & FS). + admit. + (* Définir une relation inductive qui provient du MS, + et qui relie le iblock_istep avec le RTL. Il faut prendre en compte + le "isfst" pour savoir si on doit avoir du "stuttering" côté RTL. *) + (* exec_function_internal *) + - inversion TRANSF as [dupmap f0 f0' MATCHF|]; subst. eexists. split. + + eapply plus_one. apply RTL.exec_function_internal. + erewrite <- preserv_fnstacksize; eauto. + + erewrite <- preserv_fnparams; eauto. + eapply match_states_intro; eauto. + apply dupmap_entrypoint. assumption. + (* exec_function_external *) + - inversion TRANSF as [|]; subst. eexists. split. + + eapply plus_one. econstructor. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. + + constructor. assumption. + (* exec_return *) + - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split. + + eapply plus_one. constructor. + + inv H1. econstructor; eauto. Admitted. (* TODO: première étape *) Theorem transf_program_correct: |