Added builtins for call frame and return address.

This builtins can be used to get the call frame address and the return
address. To correctly compute the load address of the return address
the allocframe is extended to contain the offset of the return address.

6 files changed, 29 insertions, 9 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 2ad99304..796bad3d 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -142,7 +142,7 @@ Inductive instruction : Type :=
   | Paddic: ireg -> ireg -> constant -> instruction           (**r add immediate and set carry *)
   | Paddis: ireg -> ireg -> constant -> instruction           (**r add immediate high *)
   | Paddze: ireg -> ireg -> instruction                       (**r add carry *)
-  | Pallocframe: Z -> int -> instruction                      (**r allocate new stack frame (pseudo) *)
+  | Pallocframe: Z -> int -> int -> instruction               (**r allocate new stack frame (pseudo) *)
   | Pand_: ireg -> ireg -> ireg -> instruction                (**r bitwise and *)
   | Pandc: ireg -> ireg -> ireg -> instruction                (**r bitwise and-complement *)
   | Pandi_: ireg -> ireg -> constant -> instruction           (**r and immediate and set conditions *)
@@ -324,7 +324,7 @@ lbl:    .double floatcst
         lfd     rdst, 0(r1)
         addi    r1, r1, 8
 >>
-- [Pallocframe sz ofs]: in the formal semantics, this pseudo-instruction
+- [Pallocframe sz ofs retofs]: in the formal semantics, this pseudo-instruction
   allocates a memory block with bounds [0] and [sz], stores the value
   of register [r1] (the stack pointer, by convention) at offset [ofs]
   in this block, and sets [r1] to a pointer to the bottom of this
@@ -623,7 +623,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Paddze rd r1 =>
       Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY)
                        #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m
-  | Pallocframe sz ofs =>
+  | Pallocframe sz ofs _ =>
       let (m1, stk) := Mem.alloc m 0 sz in
       let sp := Vptr stk Int.zero in
       match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 0ace4eaa..8f2b4dc2 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -152,7 +152,7 @@ let p_instruction oc ic =
   | Paddic  (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddic\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
   | Paddis  (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Paddis\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
   | Paddze (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Paddze\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
-  | Pallocframe (c,i) -> assert false(* Should not occur *)
+  | Pallocframe (c,i,r) -> assert false(* Should not occur *)
   | Pand_ (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pand_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pandc (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pandc\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pandi_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandi_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index b3d357ef..929e6325 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -276,6 +276,9 @@ let expand_builtin_vstore chunk args =
       assert false
 
 (* Handling of varargs *)
+let linkregister_offset = ref  Int.zero
+
+let retaddr_offset = ref Int.zero
 
 let current_function_stacksize = ref 0l
 
@@ -470,6 +473,16 @@ let expand_builtin_inline name args res =
       emit (Pmtspr(n, a1))
   | "__builtin_set_spr", _, _ ->
       raise (Error "the first argument of __builtin_set_spr must be a constant")
+  (* Frame and return address *)
+  | "__builtin_call_frame", _,BR (IR res) ->
+      let sz = !current_function_stacksize 
+      and ofs = !linkregister_offset in
+      if sz < 0x8000l then
+        emit (Paddi(res, GPR1, Cint(coqint_of_camlint sz)))
+      else
+        emit (Plwz(res, Cint ofs, GPR1))
+  | "__builtin_return_address",_,BR (IR res) ->
+      emit (Plwz (res, Cint! retaddr_offset,GPR1))
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
@@ -497,7 +510,7 @@ let num_crbit = function
 
 let expand_instruction instr =
   match instr with
-  | Pallocframe(sz, ofs) ->
+  | Pallocframe(sz, ofs,retofs) ->
       let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in
       let sz = camlint_of_coqint sz in
       assert (ofs = Int.zero);
@@ -516,7 +529,9 @@ let expand_instruction instr =
                   {sig_args = []; sig_res = None; sig_cc = cc_default}));
         emit (Pmtlr GPR0)
       end;
-      current_function_stacksize := sz
+      current_function_stacksize := sz;
+      linkregister_offset := ofs;
+      retaddr_offset := retofs
   | Pbctr sg | Pbctrl sg | Pbl(_, sg) | Pbs(_, sg) ->
       set_cr6 sg;
       emit instr
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 541fe7c6..db3b7028 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -711,7 +711,7 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo
 Definition transl_function (f: Mach.function) :=
   do c <- transl_code' f f.(Mach.fn_code) false;
   OK (mkfunction f.(Mach.fn_sig)
-       (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
+       (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) f.(fn_retaddr_ofs) ::
         Pmflr GPR0 ::
         Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
         Pcfi_rel_offset f.(fn_retaddr_ofs) :: c)).
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 2e014b4c..6d7b2aff 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -110,7 +110,12 @@ let builtins = {
     "__builtin_get_spr",
       (TInt(IUInt, []), [TInt(IInt, [])], false);
     "__builtin_set_spr",
-      (TVoid [], [TInt(IInt, []); TInt(IUInt, [])], false)
+      (TVoid [], [TInt(IInt, []); TInt(IUInt, [])], false);
+    (* Frame and return address *)
+    "__builtin_call_frame",
+      (TPtr (TVoid [],[]),[],false);
+    "__builtin_return_address",
+      (TPtr (TVoid [],[]),[],false)
   ]
 }
 
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index df78f801..cdb7aa97 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -383,7 +383,7 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	addis	%a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c
       | Paddze(r1, r2) ->
           fprintf oc "	addze	%a, %a\n" ireg r1 ireg r2
-      | Pallocframe(sz, ofs) ->
+      | Pallocframe(sz, ofs, _) ->
           assert false
       | Pand_(r1, r2, r3) ->
           fprintf oc "	and.	%a, %a, %a\n" ireg r1 ireg r2 ireg r3