Rajout d'un return_address_offset. Besoin de changer forward_simu de mach machblock

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.