summaryrefslogtreecommitdiff
path: root/powerpc
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-13 13:10:42 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2012-02-13 13:10:42 +0000
commit14b44ae202de640f2a7a6e973e5fb912b736c002 (patch)
tree92b8bab46a967647c5c646c91907811c25f0ef43 /powerpc
parent7cde5744d5fa12c76f46bcd180ecfe0b4d00afb8 (diff)
Work around limited excursion of conditional branches
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1817 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc')
-rw-r--r--powerpc/PrintAsm.ml90
1 files changed, 86 insertions, 4 deletions
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index f6c1c49..ff7957d 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -14,6 +14,7 @@
open Printf
open Datatypes
+open Maps
open Camlcoq
open Sections
open AST
@@ -509,12 +510,20 @@ let print_builtin_inline oc name args res =
end;
fprintf oc "%s end builtin %s\n" comment name
+(* Determine if the displacement of a conditional branch fits the short form *)
+
+let short_cond_branch tbl pc lbl_dest =
+ match PTree.get lbl_dest tbl with
+ | None -> assert false
+ | Some pc_dest ->
+ let disp = pc_dest - pc in -0x2000 <= disp && disp < 0x2000
+
(* Printing of instructions *)
let float_literals : (int * int64) list ref = ref []
let jumptables : (int * label list) list ref = ref []
-let print_instruction oc = function
+let print_instruction oc tbl pc = function
| Padd(r1, r2, r3) ->
fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3
| Padde(r1, r2, r3) ->
@@ -554,7 +563,14 @@ let print_instruction oc = function
| Pbctrl ->
fprintf oc " bctrl\n"
| Pbf(bit, lbl) ->
- fprintf oc " bf %a, %a\n" crbit bit label (transl_label lbl)
+ if short_cond_branch tbl pc lbl then
+ fprintf oc " bf %a, %a\n" crbit bit label (transl_label lbl)
+ else begin
+ let next = new_label() in
+ fprintf oc " bt %a, %a\n" crbit bit label next;
+ fprintf oc " b %a\n" label (transl_label lbl);
+ fprintf oc "%a:\n" label next
+ end
| Pbl s ->
fprintf oc " bl %a\n" symbol s
| Pbs s ->
@@ -562,7 +578,14 @@ let print_instruction oc = function
| Pblr ->
fprintf oc " blr\n"
| Pbt(bit, lbl) ->
- fprintf oc " bt %a, %a\n" crbit bit label (transl_label lbl)
+ if short_cond_branch tbl pc lbl then
+ fprintf oc " bt %a, %a\n" crbit bit label (transl_label lbl)
+ else begin
+ let next = new_label() in
+ fprintf oc " bf %a, %a\n" crbit bit label next;
+ fprintf oc " b %a\n" label (transl_label lbl);
+ fprintf oc "%a:\n" label next
+ end
| Pbtbl(r, tbl) ->
let lbl = new_label() in
fprintf oc "%s begin pseudoinstr btbl(%a)\n" comment ireg r;
@@ -773,6 +796,65 @@ let print_instruction oc = function
assert false
end
+(* Estimate the size of an Asm instruction encoding, in number of actual
+ PowerPC instructions. We can over-approximate. *)
+
+let instr_size = function
+ | Pallocframe(sz, ofs) -> 3
+ | Pbf(bit, lbl) -> 2
+ | Pbt(bit, lbl) -> 2
+ | Pbtbl(r, tbl) -> 4
+ | Pfcti(r1, r2) -> 4
+ | Pfmake(rd, r1, r2) -> 4
+ | Plfi(r1, c) -> 2
+ | Pmfcrbit(r1, bit) -> 2
+ | Pstfs(r1, c, r2) -> 2
+ | Pstfsx(r1, r2, r3) -> 2
+ | Plabel lbl -> 0
+ | Pbuiltin(ef, args, res) ->
+ begin match ef with
+ | EF_builtin(name, sg) ->
+ begin match extern_atom name with
+ | "__builtin_bswap" -> 3
+ | _ -> 1
+ end
+ | EF_vload chunk ->
+ if chunk = Mint8signed then 2 else 1
+ | EF_vstore chunk ->
+ if chunk = Mfloat32 then 2 else 1
+ | EF_vload_global(chunk, id, ofs) ->
+ if chunk = Mint8signed then 3 else 2
+ | EF_vstore_global(chunk, id, ofs) ->
+ if chunk = Mfloat32 then 3 else 2
+ | EF_memcpy(sz, al) ->
+ let sz = Int32.to_int (camlint_of_coqint sz) in
+ if sz <= 64 then (sz / 4) * 2 + 6 else 11
+ | EF_annot_val(txt, targ) ->
+ 0
+ | _ ->
+ assert false
+ end
+ | Pannot(ef, args) -> 0
+ | _ -> 1
+
+(* Build a table label -> estimated position in generated code.
+ Used to predict if relative conditional branches can use the short form. *)
+
+let rec label_positions tbl pc = function
+ | [] -> tbl
+ | Plabel lbl :: c -> label_positions (PTree.set lbl pc tbl) pc c
+ | i :: c -> label_positions tbl (pc + instr_size i) c
+
+(* Emit a sequence of instructions *)
+
+let rec print_instructions oc tbl pc = function
+ | [] -> ()
+ | i :: c ->
+ print_instruction oc tbl pc i;
+ print_instructions oc tbl (pc + instr_size i) c
+
+(* Print the code for a function *)
+
let print_literal oc (lbl, n) =
let nlo = Int64.to_int32 n
and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in
@@ -794,7 +876,7 @@ let print_function oc name code =
if not (C2C.atom_is_static name) then
fprintf oc " .globl %a\n" symbol name;
fprintf oc "%a:\n" symbol name;
- List.iter (print_instruction oc) code;
+ print_instructions oc (label_positions PTree.empty 0 code) 0 code;
if target <> MacOS then begin
fprintf oc " .type %a, @function\n" symbol name;
fprintf oc " .size %a, . - %a\n" symbol name symbol name