diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-01-23 17:14:10 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-01-23 17:14:10 +0100 |
| commit | 463bcb7f90d7b0d803710b81b5bb47593d0cec65 (patch) | |
| tree | d795469c7bd896960327c6335ca245f0ad9a531a /mppa_k1c/PostpassSchedulingproof.v | |
| parent | afe2e1ebb808fb2e281a09b76f29c64467fbb1e1 (diff) | |
| download | compcert-kvx-463bcb7f90d7b0d803710b81b5bb47593d0cec65.tar.gz compcert-kvx-463bcb7f90d7b0d803710b81b5bb47593d0cec65.zip | |
Proof of builtin case for transf_step_correct in PostpassSchedulingproof
Diffstat (limited to 'mppa_k1c/PostpassSchedulingproof.v')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingproof.v | 26 |
1 files changed, 25 insertions, 1 deletions
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v index 2b09bb01..fbb05ca2 100644 --- a/mppa_k1c/PostpassSchedulingproof.v +++ b/mppa_k1c/PostpassSchedulingproof.v @@ -256,6 +256,14 @@ Lemma concat_all_equiv_cons: Proof.
Admitted.
+Lemma verified_schedule_builtin_idem:
+ forall bi ef args res lbb,
+ exit bi = Some (PExpand (Pbuiltin ef args res)) ->
+ verified_schedule bi = OK lbb ->
+ lbb = bi :: nil.
+Proof.
+Admitted.
+
Lemma transf_step_simu:
forall tf b lbb ofs c tbb rs m rs' m',
Genv.find_funct_ptr tge b = Some (Internal tf) ->
@@ -290,14 +298,30 @@ Proof. 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.
+
erewrite transf_exec_bblock in H2; eauto.
inv BBEQ. rewrite H3 in H2.
exists (State rs' m'). split; try (constructor; auto).
eapply transf_step_simu; eauto.
- - destruct TODO.
+ - 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.
+ eapply plus_one. subst s'.
+ eapply exec_step_builtin.
+ 3: eapply find_bblock_tail. simpl in TAIL. 3: eauto.
+ 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.
+
Theorem transf_program_correct:
forward_simulation (Asmblock.semantics prog) (Asmblock.semantics tprog).
Proof.
|