diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-07 10:31:29 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-07 10:31:29 +0200 |
| commit | 65a1029a0e2c1b1678e522f485b1e914b6e6d52a (patch) | |
| tree | 869a1a8f314f626af98785e7a753b15fcf8e6610 /scheduling/RTLtoBTLproof.v | |
| parent | cb683f0bd30799ceb60bd04cb7a6561b8da5cc97 (diff) | |
| download | compcert-kvx-65a1029a0e2c1b1678e522f485b1e914b6e6d52a.tar.gz compcert-kvx-65a1029a0e2c1b1678e522f485b1e914b6e6d52a.zip | |
proof OK for Call and Return states
Diffstat (limited to 'scheduling/RTLtoBTLproof.v')
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 27 |
1 files changed, 21 insertions, 6 deletions
diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index aac7772c..79b7ca1a 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -252,10 +252,11 @@ Proof. inv H. + (* Internal function *) inv TRANSF. - rename H0 into MF. - eapply dupmap_entrypoint in MF as ENTRY. - eapply dupmap_correct in MF as DMC. unfold match_cfg in DMC. - apply DMC in ENTRY as DMC'. destruct DMC' as [ib [CENTRY MI]]. + rename H0 into TRANSF. + eapply dupmap_entrypoint in TRANSF as ENTRY. + eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. + apply DMC in ENTRY as DMC'. + destruct DMC' as [ib [CENTRY MI]]; clear DMC. eexists; left; eexists; split. * eapply exec_function_internal. erewrite preserv_fnstacksize; eauto. @@ -264,8 +265,22 @@ Proof. all: erewrite preserv_fnparams; eauto. constructor. + (* External function *) - admit. - - admit. + inv TRANSF. + eexists; left; eexists; split. + * eapply exec_function_external. + eapply external_call_symbols_preserved. + eapply senv_preserved. eauto. + * econstructor; eauto. + - (* Returnstate *) + inv H. inv STACKS. inv H1. + eapply dupmap_correct in TRANSF as DMC. unfold match_cfg in DMC. + remember DUPLIC as ODUPLIC; clear HeqODUPLIC. + apply DMC in DUPLIC as [ib [FNC MI]]; clear DMC. + eexists; left; eexists; split. + + eapply exec_return. + + econstructor; eauto. + eapply code_right_assoc; eauto. + constructor. Admitted. Local Hint Resolve plus_one star_refl: core. |