diff options
-rw-r--r-- | backend/Duplicate.v | 23 | ||||
-rw-r--r-- | backend/Duplicateaux.ml | 3 | ||||
-rw-r--r-- | backend/Duplicateproof.v | 70 |
3 files changed, 84 insertions, 12 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index cb52ec04..ac67cfe1 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -6,23 +6,32 @@ Require Import Coqlib Errors. Local Open Scope error_monad_scope. -(** External oracle returning the new RTL function, along with a mapping - of new nodes to old nodes *) -Axiom duplicate_aux: RTL.function -> RTL.function * (PTree.t nat). +(** External oracle returning the new RTL code (entry point unchanged), + along with a mapping of new nodes to old nodes *) +Axiom duplicate_aux: RTL.function -> RTL.code * (PTree.t nat). Extract Constant duplicate_aux => "Duplicateaux.duplicate_aux". (** * Verification of node duplications *) (** Verifies that the mapping [mp] is giving correct information *) -Definition verify_mapping (f tf: function) (mp: PTree.t nat) : res unit := OK tt. (* TODO *) +Definition verify_mapping (f: function) (tc: code) (mp: PTree.t nat) : res unit := OK tt. (* TODO *) (** * Entry points *) Definition transf_function (f: function) : res function := - let (tf, mp) := duplicate_aux f in - do u <- verify_mapping f tf mp; - OK tf. + let (tc, mp) := duplicate_aux f in + do u <- verify_mapping f tc mp; + OK (mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc (fn_entrypoint f)). + +Theorem transf_function_preserves: + forall f tf, + transf_function f = OK tf -> + fn_sig f = fn_sig tf /\ fn_params f = fn_params tf /\ fn_stacksize f = fn_stacksize tf /\ fn_entrypoint f = fn_entrypoint tf. +Proof. + intros. unfold transf_function in H. destruct (duplicate_aux _) as (tc & mp). monadInv H. + repeat (split; try reflexivity). +Qed. Definition transf_fundef (f: fundef) : res fundef := transf_partial_fundef transf_function f. diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml index 8a57f364..621a2dbe 100644 --- a/backend/Duplicateaux.ml +++ b/backend/Duplicateaux.ml @@ -1,3 +1,4 @@ +open RTL open Maps -let duplicate_aux f = (f, PTree.empty) +let duplicate_aux f = ((fn_code f), PTree.empty) diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 264b7dff..b30c2c14 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -20,6 +20,31 @@ Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof (Genv.find_symbol_match TRANSL). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSL). + +Lemma function_ptr_translated: + forall v f, + Genv.find_funct_ptr ge v = Some f -> + exists tf, + Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. +Proof (Genv.find_funct_ptr_transf_partial TRANSL). + +Lemma sig_preserved: + forall f tf, + transf_fundef f = OK tf -> + funsig tf = funsig f. +Proof. + unfold transf_fundef, transf_partial_fundef; intros. + destruct f. monadInv H. simpl. symmetry; apply transf_function_preserves. assumption. + inv H. reflexivity. +Qed. + Inductive match_nodes (f: function): node -> node -> Prop := | match_node_intro: forall n, match_nodes f n n | match_node_nop: forall n n' n1 n1', @@ -84,7 +109,7 @@ Inductive match_states: state -> state -> Prop := | match_states_intro: forall st f sp pc rs m st' f' pc' (STACKS: list_forall2 match_stackframes st st') - (TRANSL: transf_function f = OK f') + (TRANSF: transf_function f = OK f') (DUPLIC: match_nodes f pc pc'), match_states (State st f sp pc rs m) (State st' f' sp pc' rs m) | match_states_call: @@ -97,10 +122,47 @@ Inductive match_states: state -> state -> Prop := (STACKS: list_forall2 match_stackframes st st'), match_states (Returnstate st v m) (Returnstate st' v m). -Theorem transf_program_correct: - forward_simulation (RTL.semantics prog) (RTL.semantics tprog). +Theorem transf_initial_states: + forall s1, initial_state prog s1 -> + exists s2, initial_state tprog s2 /\ match_states s1 s2. +Proof. + intros. inv H. + exploit function_ptr_translated; eauto. intros (tf & FIND & TRANSF). + eexists. split. + - econstructor. + + eapply (Genv.init_mem_transf_partial TRANSL); eauto. + + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. + symmetry. eapply match_program_main. eauto. + + exploit function_ptr_translated; eauto. + + destruct f. + * monadInv TRANSF. rewrite <- H3. symmetry; eapply transf_function_preserves. assumption. + * monadInv TRANSF. assumption. + - constructor; eauto. constructor. +Qed. + +Theorem transf_final_states: + forall s1 s2 r, + match_states s1 s2 -> final_state s1 r -> final_state s2 r. +Proof. +Admitted. + +Theorem step_simulation: + forall s1 t s1', step ge s1 t s1' -> + forall s2, match_states s1 s2 -> + exists s2', + step tge s2 t s2' + /\ match_states s1' s2'. Proof. - (* TODO *) Admitted. +Theorem transf_program_correct: + forward_simulation (semantics prog) (semantics tprog). +Proof. + eapply forward_simulation_step with match_states. + - eapply senv_preserved. + - eapply transf_initial_states. + - eapply transf_final_states. + - eapply step_simulation. +Qed. + End PRESERVATION. |