diff options
-rw-r--r-- | driver/Compiler.v | 2 | ||||
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmgen.v | 13 | ||||
-rw-r--r-- | mppa_k1c/Asmgenproof.v | 24 | ||||
-rw-r--r-- | mppa_k1c/Machblockgen.v | 8 | ||||
-rw-r--r-- | mppa_k1c/Machblockgenproof.v | 20 |
6 files changed, 51 insertions, 20 deletions
diff --git a/driver/Compiler.v b/driver/Compiler.v index 75247f71..1cb5bd36 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -404,7 +404,7 @@ Ltac DestructM := eapply compose_forward_simulations. eapply match_if_simulation. eassumption. exact Debugvarproof.transf_program_correct. eapply compose_forward_simulations. - eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof0.return_address_offset). + eapply Stackingproof.transf_program_correct with (return_address_offset := Asmgenproof.return_address_offset). exact Asmgenproof.return_address_exists. eassumption. eapply Asmgenproof.transf_program_correct; eassumption. diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 4bb23e8e..79c28fe9 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -872,7 +872,7 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) := end . -Definition transl_function (f: Machblock.function) := +Definition transf_function (f: Machblock.function) := do lb <- transl_blocks f f.(Machblock.fn_code); OK (mkfunction f.(Machblock.fn_sig) (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b @@ -889,7 +889,7 @@ Definition transl_function (f: Machblock.function) := Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef := - transf_partial_fundef transl_function f. + transf_partial_fundef transf_function f. Definition transf_program (p: Machblock.program) : res Asmblock.program := transform_partial_program transf_fundef p. diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 7b753506..15892818 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -23,4 +23,15 @@ Local Open Scope error_monad_scope. Definition transf_program (p: Mach.program) : res Asm.program := let mbp := Machblockgen.transf_program p in do abp <- Asmblockgen.transf_program mbp; - OK (Asm.transf_program abp).
\ No newline at end of file + OK (Asm.transf_program abp). + +Definition transf_function (f: Mach.function) : res function := + let mbf := Machblockgen.transf_function f in + do abf <- Asmblockgen.transf_function mbf; + OK (Asm.transf_function abf). + +Definition transl_code (f: Mach.function) (l: Mach.code) : res (list instruction) := + let mbf := Machblockgen.transf_function f in + let mbc := Machblockgen.trans_code l in + do abc <- transl_blocks mbf mbc; + OK (unfold abc).
\ No newline at end of file diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 09564718..5660f718 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -40,6 +40,25 @@ Proof. exists tp; split. apply Asm.transf_program_match; auto. auto. Qed. +(** Return Address Offset *) + +Inductive code_tail: Z -> code -> code -> Prop := + | code_tail_0: forall c, + code_tail 0 c c + | code_tail_S: forall pos i c1 c2, + code_tail pos c1 c2 -> + code_tail (pos + 1) (i :: c1) c2. + +Definition return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop := + forall tf tc, + Asmgen.transf_function f = OK tf -> + Asmgen.transl_code f c = OK tc -> + code_tail (Ptrofs.unsigned ofs) (fn_code tf) tc. + +Axiom return_address_exists: + forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> + exists ra, return_address_offset f c ra. + Section PRESERVATION. Variable prog: Mach.program. @@ -49,7 +68,7 @@ Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. Theorem transf_program_correct: - forward_simulation (Mach.semantics (inv_trans_rao return_address_offset) prog) (Asm.semantics tprog). + forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. unfold match_prog in TRANSF. simpl in TRANSF. inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. @@ -60,4 +79,5 @@ Qed. End PRESERVATION. -Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes).
\ No newline at end of file +Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes). + diff --git a/mppa_k1c/Machblockgen.v b/mppa_k1c/Machblockgen.v index c20889b7..1d5555df 100644 --- a/mppa_k1c/Machblockgen.v +++ b/mppa_k1c/Machblockgen.v @@ -563,7 +563,7 @@ Proof. Qed. (* à finir pour passer des Mach.function au function, etc. *) -Definition trans_function (f: Mach.function) : function := +Definition transf_function (f: Mach.function) : function := {| fn_sig:=Mach.fn_sig f; fn_code:=trans_code (Mach.fn_code f); fn_stacksize := Mach.fn_stacksize f; @@ -571,8 +571,8 @@ Definition trans_function (f: Mach.function) : function := fn_retaddr_ofs := Mach.fn_retaddr_ofs f |}. -Definition trans_fundef (f: Mach.fundef) : fundef := - transf_fundef trans_function f. +Definition transf_fundef (f: Mach.fundef) : fundef := + transf_fundef transf_function f. Definition transf_program (src: Mach.program) : program := - transform_program trans_fundef src. + transform_program transf_fundef src. diff --git a/mppa_k1c/Machblockgenproof.v b/mppa_k1c/Machblockgenproof.v index 45ea53cc..62c1e0ed 100644 --- a/mppa_k1c/Machblockgenproof.v +++ b/mppa_k1c/Machblockgenproof.v @@ -18,10 +18,10 @@ Require Import Machblockgen. Require Import ForwardSimulationBlock. Definition inv_trans_rao (rao: function -> code -> ptrofs -> Prop) (f: Mach.function) (c: Mach.code) := - rao (trans_function f) (trans_code c). + rao (transf_function f) (trans_code c). Definition match_prog (p: Mach.program) (tp: Machblock.program) := - match_program (fun _ f tf => tf = trans_fundef f) eq p tp. + match_program (fun _ f tf => tf = transf_fundef f) eq p tp. Lemma transf_program_match: forall p tp, transf_program p = tp -> match_prog p tp. Proof. @@ -90,7 +90,7 @@ Proof (match_program_main TRANSF). Lemma functions_translated: forall b f, Genv.find_funct_ptr ge b = Some f -> - exists tf, Genv.find_funct_ptr tge b = Some tf /\ trans_fundef f = tf. + exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = tf. Proof. intros. exploit (Genv.find_funct_ptr_match TRANSF); eauto. intro. @@ -110,7 +110,7 @@ Qed. Lemma find_funct_ptr_same: forall f f0, Genv.find_funct_ptr ge f = Some (Internal f0) -> - Genv.find_funct_ptr tge f = Some (Internal (trans_function f0)). + Genv.find_funct_ptr tge f = Some (Internal (transf_function f0)). Proof. intros. exploit (Genv.find_funct_ptr_transf TRANSF); eauto. Qed. @@ -295,15 +295,15 @@ Qed. Lemma find_label_preserved: forall l f c, Mach.find_label l (Mach.fn_code f) = Some c -> - exists h, In l h /\ find_label l (fn_code (trans_function f)) = Some (concat h (trans_code c)). + exists h, In l h /\ find_label l (fn_code (transf_function f)) = Some (concat h (trans_code c)). Proof. - intros. cutrewrite ((fn_code (trans_function f)) = trans_code (Mach.fn_code f)); eauto. + intros. cutrewrite ((fn_code (transf_function f)) = trans_code (Mach.fn_code f)); eauto. apply find_label_transcode_preserved; auto. Qed. Lemma mem_free_preserved: forall m stk f, - Mem.free m stk 0 (Mach.fn_stacksize f) = Mem.free m stk 0 (fn_stacksize (trans_function f)). + Mem.free m stk 0 (Mach.fn_stacksize f) = Mem.free m stk 0 (fn_stacksize (transf_function f)). Proof. intros. auto. Qed. @@ -462,10 +462,10 @@ Proof. inversion Hexit; subst; inversion Hstep; subst; simpl ). * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto. - apply exec_MBcall with (f := (trans_function f0)); auto. + apply exec_MBcall with (f := (transf_function f0)); auto. rewrite find_function_ptr_same in H9; auto. * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto. - apply exec_MBtailcall with (f := (trans_function f0)); auto. + apply exec_MBtailcall with (f := (transf_function f0)); auto. rewrite find_function_ptr_same in H9; auto. rewrite parent_sp_preserved in H11; subst; auto. rewrite parent_ra_preserved in H12; subst; auto. @@ -582,7 +582,7 @@ Proof. inversion H1; subst; clear H1. inversion_clear H0; simpl. - (* function_internal*) - cutrewrite (trans_code (Mach.fn_code f0) = fn_code (trans_function f0)); eauto. + cutrewrite (trans_code (Mach.fn_code f0) = fn_code (transf_function f0)); eauto. eapply exec_function_internal; eauto. rewrite <- parent_sp_preserved; eauto. rewrite <- parent_ra_preserved; eauto. |