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 | |
| parent | af2c82cfd7f2318fcd81da2ea4cf3fd695db3b40 (diff) | |
| download | compcert-kvx-989e85b700161867c2f80df55c2dfaaaa5fe82b4.tar.gz compcert-kvx-989e85b700161867c2f80df55c2dfaaaa5fe82b4.zip | |
BTLtoRTL: proof for internal/external/return states
Diffstat (limited to 'scheduling')
| -rw-r--r-- | scheduling/BTL.v | 4 | ||||
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 25 |
2 files changed, 27 insertions, 2 deletions
diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 8bdafb89..8529010c 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -451,7 +451,7 @@ Inductive match_stackframes: stackframe -> RTL.stackframe -> Prop := | match_stackframe_intro dupmap res f sp pc rs f' pc' (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc' = Some pc) + (DUPLIC: dupmap!pc = Some pc') : match_stackframes (Stackframe res f sp pc rs) (RTL.Stackframe res f' sp pc' rs). Inductive match_states: state -> RTL.state -> Prop := @@ -459,7 +459,7 @@ Inductive match_states: state -> RTL.state -> Prop := dupmap st f sp pc rs m st' f' pc' (STACKS: list_forall2 match_stackframes st st') (TRANSF: match_function dupmap f f') - (DUPLIC: dupmap!pc' = Some pc) + (DUPLIC: dupmap!pc = Some pc') : match_states (State st f sp pc rs m) (RTL.State st' f' sp pc' rs m) | match_states_call st st' f f' args m 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: |