diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-11 16:51:47 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-11 16:51:47 +0200 |
commit | 417b6e77e5a0c4ea3431d5f379ff054a26b1e326 (patch) | |
tree | 9a2da7aedccf9d07aed0aa95e3167819c6047e25 /backend | |
parent | 5361fd9e5bfb9a1c80103cf83a06427b24b57369 (diff) | |
download | compcert-kvx-417b6e77e5a0c4ea3431d5f379ff054a26b1e326.tar.gz compcert-kvx-417b6e77e5a0c4ea3431d5f379ff054a26b1e326.zip |
Fixing Linking problem
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Duplicate.v | 30 | ||||
-rw-r--r-- | backend/Duplicateproof.v | 32 |
2 files changed, 31 insertions, 31 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 5c0b1d58..cb3936bb 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -34,35 +34,35 @@ Definition verify_mapping (xf: xfunction) (tc: code) (tentry: node) : res unit : (** * Entry points *) -Definition transf_function (f: function) : res xfunction := +Definition transf_function_aux (f: function) : res xfunction := let (tcte, mp) := duplicate_aux f in let (tc, te) := tcte in let xf := {| fn_RTL := (mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te); fn_revmap := mp |} in do u <- verify_mapping xf tc te; OK xf. -Theorem transf_function_preserves: +Theorem transf_function_aux_preserves: forall f xf, - transf_function f = OK xf -> + transf_function_aux f = OK xf -> fn_sig f = fn_sig (fn_RTL xf) /\ fn_params f = fn_params (fn_RTL xf) /\ fn_stacksize f = fn_stacksize (fn_RTL xf). Proof. - intros. unfold transf_function in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H. + intros. unfold transf_function_aux in H. destruct (duplicate_aux _) as (tcte & mp). destruct tcte as (tc & te). monadInv H. repeat (split; try reflexivity). Qed. -Remark transf_function_fnsig: forall f xf, transf_function f = OK xf -> fn_sig f = fn_sig (fn_RTL xf). - Proof. apply transf_function_preserves. Qed. -Remark transf_function_fnparams: forall f xf, transf_function f = OK xf -> fn_params f = fn_params (fn_RTL xf). - Proof. apply transf_function_preserves. Qed. -Remark transf_function_fnstacksize: forall f xf, transf_function f = OK xf -> fn_stacksize f = fn_stacksize (fn_RTL xf). - Proof. apply transf_function_preserves. Qed. +Remark transf_function_aux_fnsig: forall f xf, transf_function_aux f = OK xf -> fn_sig f = fn_sig (fn_RTL xf). + Proof. apply transf_function_aux_preserves. Qed. +Remark transf_function_aux_fnparams: forall f xf, transf_function_aux f = OK xf -> fn_params f = fn_params (fn_RTL xf). + Proof. apply transf_function_aux_preserves. Qed. +Remark transf_function_aux_fnstacksize: forall f xf, transf_function_aux f = OK xf -> fn_stacksize f = fn_stacksize (fn_RTL xf). + Proof. apply transf_function_aux_preserves. Qed. -Definition transf_fundef_aux (f: fundef) : res xfundef := - transf_partial_fundef transf_function f. +Definition transf_function (f: function) : res function := + do xf <- transf_function_aux f; + OK (fn_RTL xf). -Definition transf_fundef (f: fundef): res fundef := - do xf <- transf_fundef_aux f; - OK (fundef_RTL xf). +Definition transf_fundef (f: fundef) : res fundef := + transf_partial_fundef transf_function f. Definition transf_program (p: program) : res program := transform_partial_program transf_fundef p.
\ No newline at end of file diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index 1127a505..a368174f 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -3,7 +3,7 @@ Require Import AST Linking Errors Globalenvs Smallstep. Require Import Coqlib Maps Events Values. Require Import Op RTL Duplicate. -Definition match_prog (p: program) (tp: program) := +Definition match_prog (p tp: program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. Lemma transf_program_match: @@ -37,12 +37,12 @@ Inductive match_inst (is_copy: node -> option node): instruction -> instruction | match_inst_return: forall or, match_inst is_copy (Ireturn or) (Ireturn or). Axiom revmap_correct: forall f xf n n', - transf_function f = OK xf -> + transf_function_aux f = OK xf -> (fn_revmap xf)!n' = Some n -> (forall i, (fn_code f)!n = Some i -> exists i', (fn_code (fn_RTL xf))!n' = Some i' /\ match_inst (fun n => (fn_revmap xf)!n) i i'). Axiom revmap_entrypoint: - forall f xf, transf_function f = OK xf -> (fn_revmap xf)!(fn_entrypoint (fn_RTL xf)) = Some (fn_entrypoint f). + forall f xf, transf_function_aux f = OK xf -> (fn_revmap xf)!(fn_entrypoint (fn_RTL xf)) = Some (fn_entrypoint f). Section PRESERVATION. @@ -96,8 +96,8 @@ Lemma function_sig_translated: forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f. Proof. intros. destruct f. - - simpl in H. monadInv H. simpl. symmetry. monadInv EQ. apply transf_function_preserves. assumption. - - simpl in H. monadInv H. monadInv EQ. reflexivity. + - simpl in H. monadInv H. simpl. symmetry. monadInv EQ. apply transf_function_aux_preserves. assumption. + - simpl in H. monadInv H. (* monadInv EQ. *) reflexivity. Qed. Lemma sig_preserved: @@ -106,7 +106,7 @@ Lemma sig_preserved: funsig tf = funsig f. Proof. unfold transf_fundef, transf_partial_fundef; intros. - destruct f. monadInv H. simpl. symmetry. monadInv EQ. apply transf_function_preserves. assumption. + destruct f. monadInv H. simpl. symmetry. monadInv EQ. apply transf_function_aux_preserves. assumption. inv H. reflexivity. Qed. @@ -130,7 +130,7 @@ Qed. Inductive match_stackframes: stackframe -> stackframe -> Prop := | match_stackframe_intro: forall res f sp pc rs xf pc' - (TRANSF: transf_function f = OK xf) + (TRANSF: transf_function_aux f = OK xf) (DUPLIC: (fn_revmap xf)!pc' = Some pc), match_stackframes (Stackframe res f sp pc rs) (Stackframe res (fn_RTL xf) sp pc' rs). @@ -138,7 +138,7 @@ Inductive match_states: state -> state -> Prop := | match_states_intro: forall st f sp pc rs m st' xf pc' (STACKS: list_forall2 match_stackframes st st') - (TRANSF: transf_function f = OK xf) + (TRANSF: transf_function_aux f = OK xf) (DUPLIC: (fn_revmap xf)!pc' = Some pc), match_states (State st f sp pc rs m) (State st' (fn_RTL xf) sp pc' rs m) | match_states_call: @@ -164,8 +164,8 @@ Proof. symmetry. eapply match_program_main. eauto. + exploit function_ptr_translated; eauto. + destruct f. - * monadInv TRANSF. monadInv EQ. rewrite <- H3. symmetry; eapply transf_function_preserves. assumption. - * monadInv TRANSF. monadInv EQ. assumption. + * monadInv TRANSF. monadInv EQ. rewrite <- H3. symmetry; eapply transf_function_aux_preserves. assumption. + * monadInv TRANSF. (* monadInv EQ. *) assumption. - constructor; eauto. constructor. Qed. @@ -239,14 +239,14 @@ Proof. eexists. split. + eapply exec_Itailcall. eassumption. simpl. eassumption. apply function_sig_translated. assumption. - erewrite <- transf_function_fnstacksize; eauto. + erewrite <- transf_function_aux_fnstacksize; eauto. + repeat (constructor; auto). * simpl in H0. destruct (Genv.find_symbol _ _) eqn:GFS; try discriminate. apply function_ptr_translated in H0. destruct H0 as (tf & GFF & TF). eexists. split. + eapply exec_Itailcall. eassumption. simpl. rewrite symbols_preserved. rewrite GFS. eassumption. apply function_sig_translated. assumption. - erewrite <- transf_function_fnstacksize; eauto. + erewrite <- transf_function_aux_fnstacksize; eauto. + repeat (constructor; auto). (* Ibuiltin *) - eapply revmap_correct in DUPLIC; eauto. @@ -276,15 +276,15 @@ Proof. destruct DUPLIC as (i' & H2 & H3). inv H3. pose symbols_preserved as SYMPRES. eexists. split. - + eapply exec_Ireturn; eauto. erewrite <- transf_function_fnstacksize; eauto. + + eapply exec_Ireturn; eauto. erewrite <- transf_function_aux_fnstacksize; eauto. + constructor; auto. (* exec_function_internal *) - monadInv TRANSF. monadInv EQ. eexists. split. - + eapply exec_function_internal. erewrite <- transf_function_fnstacksize; eauto. - + erewrite transf_function_fnparams; eauto. + + eapply exec_function_internal. erewrite <- transf_function_aux_fnstacksize; eauto. + + erewrite transf_function_aux_fnparams; eauto. econstructor; eauto. apply revmap_entrypoint. assumption. (* exec_function_external *) - - monadInv TRANSF. monadInv EQ. eexists. split. + - monadInv TRANSF. (* monadInv EQ. *) eexists. split. + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved. + constructor. assumption. (* exec_return *) |