MPPA - Activated Mtailcall + Pcall

4 files changed, 24 insertions, 8 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 42b5f85f..59b1a139 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -140,7 +140,7 @@ Inductive instruction : Type :=
   | Pget    (rd: ireg) (rs: preg)                    (**r get system register *)
   | Pset    (rd: preg) (rs: ireg)                    (**r set system register *)
   | Pret                                             (**r return *)
-
+  | Pcall   (l: label)                               (**r function call *)
   | Pmv     (rd: ireg) (rs: ireg)                    (**r integer move *)
 
 (** 32-bit integer register-immediate instructions *)
@@ -567,7 +567,17 @@ Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) :=
       | _          => Stuck
       end
   end.
-
+(*
+Definition do_call (f: function) (lbl: label) (rs: regset) (m: mem) :=
+  match label_pos lbl 0 (fn_code f) with
+  | None => Stuck
+  | Some pos =>
+      match rs#PC with
+      | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))#RA <- (rs#PC)) m
+      | _          => Stuck
+      end
+  end.
+*)
 (** Auxiliaries for memory accesses *)
 
 Definition eval_offset (ofs: offset) : ptrofs :=
@@ -625,6 +635,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
     end
   | Pret =>
       Next (rs#PC <- (rs#RA)) m
+  | Pcall s =>
+      Next (rs#PC <- (Genv.symbol_address ge s Ptrofs.zero)) m
   | Pmv d s =>
       Next (nextinstr (rs#d <- (rs#s))) m
 
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 96246bc2..300f21a2 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -831,10 +831,10 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
       OK (Pjal_s symb sig :: k)
   | Mtailcall sig (inl r) =>
       do r1 <- ireg_of r;
-      OK (make_epilogue f (Pj_r r1 sig :: k))
-  | Mtailcall sig (inr symb) =>
-      OK (make_epilogue f (Pj_s symb sig :: k))
-*)| Mbuiltin ef args res =>
+      OK (make_epilogue f (Pcall :: k))
+*)| Mtailcall sig (inr symb) =>
+      OK (make_epilogue f ((Pcall symb) :: k))
+  | Mbuiltin ef args res =>
       OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k)
   | Mlabel lbl =>
       OK (Plabel lbl :: k)
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 414527ad..213cb5d6 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -362,6 +362,8 @@ Lemma transl_instr_label:
 Proof.
   unfold transl_instr; intros; destruct i; TailNoLabel.
 - eapply transl_op_label; eauto.
+- destruct s0; monadInv H; eapply tail_nolabel_trans
+  ; [eapply make_epilogue_label|TailNoLabel]. 
 - eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
 Qed.
 (*
@@ -372,7 +374,6 @@ Qed.
 - eapply transl_op_label; eauto.
 - destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
 - destruct m; monadInv H; eapply transl_memory_access_label; eauto; intros; exact I.
-- destruct s0; monadInv H; TailNoLabel.
 - destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]).
 - eapply transl_cbranch_label; eauto.
 - eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel].
@@ -829,6 +830,7 @@ Local Transparent destroyed_by_op.
   econstructor; eauto.
   apply agree_set_other; auto with asmgen.
   Simpl. rewrite Z by (rewrite <- (ireg_of_eq _ _ EQ1); eauto with asmgen). assumption. 
+*)
 + (* Direct call *)
   exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). 
   exploit exec_straight_steps_2; eauto using functions_transl.                      
@@ -843,7 +845,7 @@ Local Transparent destroyed_by_op.
   econstructor; eauto.
   apply agree_set_other; auto with asmgen.
   Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto.
-*)
+
 - (* Mbuiltin *)
   inv AT. monadInv H4.
   exploit functions_transl; eauto. intro FN.
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 71d2f22d..b25804d2 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -158,6 +158,8 @@ module Target : TARGET =
 
 (* Printing of instructions *)
     let print_instruction oc = function
+      | Pcall(s) ->
+         fprintf oc "	j	%a\n" symbol s
       | Pret ->
          fprintf oc "	ret\n;;\n"
       | Pget (rd, rs) ->