diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-04 11:49:32 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-04 11:49:32 +0200 |
| commit | 4a5f1db8abe7831649f6f15178958e0c57955a25 (patch) | |
| tree | 9c7c227494b39b5b6d2228983ee228309caba1f2 /backend | |
| parent | f91f8296b6d2f663878223d473cd9e887403f73f (diff) | |
| download | compcert-kvx-4a5f1db8abe7831649f6f15178958e0c57955a25.tar.gz compcert-kvx-4a5f1db8abe7831649f6f15178958e0c57955a25.zip | |
Duplicate: exec_function_internal
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Duplicate.v | 9 | ||||
| -rw-r--r-- | backend/Duplicateproof.v | 36 |
2 files changed, 43 insertions, 2 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index ac67cfe1..8a78ee80 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -33,6 +33,15 @@ Proof. repeat (split; try reflexivity). Qed. +Remark transf_function_fnsig: forall f tf, transf_function f = OK tf -> fn_sig f = fn_sig tf. + Proof. apply transf_function_preserves. Qed. +Remark transf_function_fnparams: forall f tf, transf_function f = OK tf -> fn_params f = fn_params tf. + Proof. apply transf_function_preserves. Qed. +Remark transf_function_fnstacksize: forall f tf, transf_function f = OK tf -> fn_stacksize f = fn_stacksize tf. + Proof. apply transf_function_preserves. Qed. +Remark transf_function_fnentrypoint: forall f tf, transf_function f = OK tf -> fn_entrypoint f = fn_entrypoint tf. + Proof. apply transf_function_preserves. Qed. + Definition transf_fundef (f: fundef) : res fundef := transf_partial_fundef transf_function f. diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index b30c2c14..69fc41ae 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -144,15 +144,47 @@ Theorem transf_final_states: forall s1 s2 r, match_states s1 s2 -> final_state s1 r -> final_state s2 r. Proof. -Admitted. + intros. inv H0. inv H. inv STACKS. constructor. +Qed. Theorem step_simulation: forall s1 t s1', step ge s1 t s1' -> - forall s2, match_states s1 s2 -> + forall s2 (MS: match_states s1 s2), exists s2', step tge s2 t s2' /\ match_states s1' s2'. Proof. + induction 1; intros; inv MS. +(* Inop *) + - admit. +(* Iop *) + - admit. +(* Iload *) + - admit. +(* Istore *) + - admit. +(* Icall *) + - admit. +(* Itailcall *) + - admit. +(* Ibuiltin *) + - admit. +(* Icond *) + - admit. +(* Ijumptable *) + - admit. +(* Ireturn *) + - admit. +(* exec_function_internal *) + - monadInv TRANSF. eexists. split. + + econstructor. erewrite <- transf_function_fnstacksize; eauto. + + erewrite transf_function_fnentrypoint; eauto. + erewrite transf_function_fnparams; eauto. + econstructor; eauto. constructor. +(* exec_function_external *) + - admit. +(* exec_return *) + - admit. Admitted. Theorem transf_program_correct: |