diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-23 17:22:53 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-23 17:22:53 +0100 |
| commit | 644aaedd3a62e9dcbfb6d0159564904b2be53285 (patch) | |
| tree | dfc2b4f7b970dff55003a0cb63b23a479356371f | |
| parent | 463bcb7f90d7b0d803710b81b5bb47593d0cec65 (diff) | |
| download | compcert-kvx-644aaedd3a62e9dcbfb6d0159564904b2be53285.tar.gz compcert-kvx-644aaedd3a62e9dcbfb6d0159564904b2be53285.zip | |
3ème cas de transf_step_correct de PostpassSchedulingproof fini
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index fbb05ca2..92f5ebd4 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -303,12 +303,10 @@ Proof. inv BBEQ. rewrite H3 in H2.
exists (State rs' m'). split; try (constructor; auto).
eapply transf_step_simu; eauto.
+
- exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
exploit transf_find_bblock; eauto. intros (lbb & VES & c & TAIL).
exploit verified_schedule_builtin_idem; eauto. intros. subst lbb.
- exploit verified_schedule_correct; eauto. intros (tbb & CONC & BBEQ).
- assert (NOOV: size_blocks x.(fn_blocks) <= Ptrofs.max_unsigned).
- eapply transf_function_no_overflow; eauto.
remember (State (nextblock _ _) _) as s'. exists s'.
split; try constructor; auto.
@@ -318,9 +316,12 @@ Proof. all: eauto.
eapply eval_builtin_args_preserved with (ge1 := ge). exact symbols_preserved. eauto.
eapply external_call_symbols_preserved; eauto. apply senv_preserved.
- - destruct TODO.
-Admitted.
+ - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
+ remember (State _ m') as s'. exists s'. split; try constructor; auto.
+ subst s'. eapply plus_one. eapply exec_step_external; eauto.
+ eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+Qed.
Theorem transf_program_correct:
forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog).
|