Branch relaxation

aarch64/Asmexpand.ml

@@ -407,6 +407,70 @@ let expand_builtin_inline name args res =
   | _ ->
      raise (Error ("unrecognized builtin " ^ name))
 
+(* Branch relaxation *)
+
+module BInfo: BRANCH_INFORMATION = struct
+
+  let builtin_size = function
+    | EF_annot _ -> 0
+    | EF_debug _ -> 0
+    | EF_inline_asm _ -> 32  (* hope it's no more than 8 instructions *)
+    | _ -> assert false
+
+  let instr_size = function
+    | Pfmovimmd _ | Pfmovimms _ -> 8
+    | Pbtbl(_, tbl) -> 12 + 4 * List.length tbl
+    | Plabel _ | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
+    | Pbuiltin(ef, _, _) -> builtin_size ef
+    | _ -> 4
+
+  let branch_overflow ~map pc lbl range =
+    let displ = pc + 4 - map lbl in
+    displ < -range || displ >= range
+
+  let need_relaxation ~map pc instr =
+    match instr with
+    | Pbc(_, lbl) | Pcbnz(_, _, lbl) | Pcbz(_, _, lbl) ->
+        (* +/- 1 MB *)
+        branch_overflow ~map pc lbl 0x100_000
+    | Ptbnz(_, _, _, lbl) | Ptbz(_, _, _, lbl) ->
+        (* +/- 32 KB *)
+        branch_overflow ~map pc lbl 0x8_000
+    | _ ->
+        false
+
+  let negate_testcond = function
+    | TCeq -> TCne   | TCne -> TCeq
+    | TChs -> TClo   | TClo -> TChs
+    | TCmi -> TCpl   | TCpl -> TCmi
+    | TChi -> TCls   | TCls -> TChi
+    | TCge -> TClt   | TClt -> TCge
+    | TCgt -> TCle   | TCle -> TCgt
+
+  let relax_instruction instr =
+    match instr with
+    | Pbc(c, lbl) ->
+        let lbl' = new_label() in
+        [Pbc(negate_testcond c, lbl'); Pb lbl; Plabel lbl']
+    | Pcbnz(sz, r, lbl) ->
+        let lbl' = new_label() in
+        [Pcbz(sz, r, lbl'); Pb lbl; Plabel lbl']
+    | Pcbz(sz, r, lbl) ->
+        let lbl' = new_label() in
+        [Pcbnz(sz, r, lbl'); Pb lbl; Plabel lbl']
+    | Ptbnz(sz, r, n, lbl) ->
+        let lbl' = new_label() in
+        [Ptbz(sz, r, n, lbl'); Pb lbl; Plabel lbl']
+    | Ptbz(sz, r, n, lbl) ->
+        let lbl' = new_label() in
+        [Ptbnz(sz, r, n, lbl'); Pb lbl; Plabel lbl']
+    | _ ->
+        assert false
+
+end
+
+module BRelax = Branch_relaxation (BInfo)
+
 (* Expansion of instructions *)
 
 let expand_instruction instr =
@@ -478,7 +542,8 @@ let expand_function id fn =
   try
     set_current_function fn;
     expand id (* sp= *) 31 preg_to_dwarf expand_instruction fn.fn_code;
-    Errors.OK (get_current_function ())
+    let fn' = BRelax.relaxation (get_current_function ()) in
+    Errors.OK fn'
   with Error s ->
     Errors.Error (Errors.msg s)
 

backend/Asmexpandaux.ml

@@ -11,9 +11,10 @@
 (*                                                                     *)
 (* *********************************************************************)
 
-(* Util functions used for the expansion of built-ins and some
+(* Utility functions used for the expansion of built-ins and some
    pseudo-instructions *)
 
+open Maps
 open Asm
 open AST
 open Camlcoq
@@ -186,3 +187,63 @@ let expand id sp preg simple l =
     expand_debug id sp preg simple l
   else
     expand_simple simple l
+
+(* Branch relaxation *)
+
+module type BRANCH_INFORMATION = sig
+  val instr_size: instruction -> int
+  val need_relaxation: map: (label -> int) -> int -> instruction -> bool
+  val relax_instruction: instruction -> instruction list
+end
+
+module Branch_relaxation (B: BRANCH_INFORMATION) = struct
+
+(* Fill the table label -> position in code *)
+
+let rec set_label_positions tbl pc = function
+  | [] ->
+      tbl
+  | Plabel lbl :: code ->
+      set_label_positions (PTree.set lbl pc tbl) pc code
+  | instr :: code ->
+      set_label_positions tbl (pc + B.instr_size instr) code
+
+let get_label_position tbl lbl =
+  match PTree.get lbl tbl with
+  | Some pc -> pc
+  | None -> 
+      invalid_arg
+        (Printf.sprintf "Fatal error: unknown label %d" (P.to_int lbl))
+
+let rec need_relaxation tbl pc = function
+  | [] ->
+      false
+  | instr :: code ->
+      B.need_relaxation ~map:(get_label_position tbl) pc instr
+      || need_relaxation tbl (pc + B.instr_size instr) code
+
+let rec do_relaxation tbl accu pc = function
+  | [] ->
+      List.rev accu
+  | instr :: code ->
+      do_relaxation
+        tbl
+        (if B.need_relaxation ~map:(get_label_position tbl) pc instr
+         then List.rev_append (B.relax_instruction instr) accu
+         else instr :: accu)
+        (pc + B.instr_size instr)
+        code
+
+let relaxation fn =
+  set_current_function fn;
+  let rec relax fn =
+    let tbl = set_label_positions PTree.empty 0 fn.fn_code in
+    if not (need_relaxation tbl 0 fn.fn_code) then fn else begin
+      let code' = do_relaxation tbl [] 0 fn.fn_code in
+      relax {fn with fn_code = code'}
+    end in
+  let res = relax fn in
+  set_current_function dummy_function;
+  res
+
+end

backend/Asmexpandaux.mli

@@ -34,3 +34,26 @@ val get_current_function: unit -> coq_function
 val expand: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit
   (* Expand the instruction sequence of a function. Takes the function id, the register number of the stackpointer, a
      function to get the dwarf mapping of variable names and for the expansion of simple instructions *)
+
+(** Branch relaxation.  Rewrite the Asm code after builtin expansion
+    to avoid overflows in displacements of branching instructions. *)
+
+module type BRANCH_INFORMATION = sig
+  val instr_size: instruction -> int
+      (* The size in bytes of the given instruction.
+         Can over-approximate. *)
+  val need_relaxation: map: (label -> int) -> int -> instruction -> bool
+      (* [need_relaxation ~map pc instr] returns [true] if
+         the given instruction is a branch that can overflow and
+         needs to be rewritten.
+         [pc] is the position of the instruction in the code (in bytes).
+         [map] is a mapping from labels to code positions (also in bytes). *)
+  val relax_instruction: instruction -> instruction list
+      (* [relaxation instr] returns the list of instructions that perform
+         the same branch as [instr] but avoid branch overflow.
+         Can call [Asmexpandaux.new_label] to obtain fresh labels. *)
+end
+
+module Branch_relaxation (_: BRANCH_INFORMATION) : sig
+  val relaxation: coq_function -> coq_function
+end

powerpc/Asmexpand.ml

@@ -827,6 +827,49 @@ let set_cr6 sg =
     else emit (Pcrxor(CRbit_6, CRbit_6, CRbit_6))
   end
 
+(* Branch relaxation *)
+
+module BInfo: BRANCH_INFORMATION = struct
+
+  let builtin_size = function
+    | EF_annot _ -> 0
+    | EF_debug _ -> 0
+    | EF_inline_asm _ -> 32  (* hope it's no more than 8 instructions *)
+    | _ -> assert false
+
+  let instr_size = function
+    | Pbtbl(r, tbl) -> 20
+    | Pldi (r1,c) -> 8
+    | Plfi(r1, c) -> 8
+    | Plfis(r1, c) -> 8
+    | Plabel lbl -> 0
+    | Pbuiltin(ef, _, _) -> builtin_size ef
+    | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
+    | _ -> 4
+
+  let need_relaxation ~map pc instr =
+    match instr with
+    | Pbf(_, lbl) | Pbt(_, lbl) ->
+        let displ = pc + 4 - map lbl in
+        displ < -0x8000 || displ >= 0x8000
+    | _ ->
+        false
+
+  let relax_instruction instr =
+    match instr with
+    | Pbf(bit, lbl) ->
+        let lbl' = new_label() in
+        [Pbt(bit, lbl'); Pb lbl; Plabel lbl']
+    | Pbt(bit, lbl) ->
+        let lbl' = new_label() in
+        [Pbf(bit, lbl'); Pb lbl; Plabel lbl']
+    | _ ->
+        assert false
+
+end
+
+module BRelax = Branch_relaxation (BInfo)
+
 (* Expand instructions *)
 
 let expand_instruction instr =
@@ -973,7 +1016,8 @@ let expand_function id fn =
   try
     set_current_function fn;
     expand id 1 preg_to_dwarf expand_instruction fn.fn_code;
-    Errors.OK (get_current_function ())
+    let fn' = BRelax.relaxation (get_current_function ()) in
+    Errors.OK fn'
   with Error s ->
     Errors.Error (Errors.msg s)
 

powerpc/TargetPrinter.ml

@@ -14,7 +14,6 @@
 
 open Printf
 open Fileinfo
-open Maps
 open Camlcoq
 open Sections
 open AST
@@ -381,17 +380,9 @@ module Target (System : SYSTEM):TARGET =
           assert false
       in leftmost_one 0 0x8000_0000_0000_0000L
 
-    (* 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 print_instruction oc tbl pc fallthrough = function
+    let print_instruction oc fallthrough = function
       | Padd(r1, r2, r3) | Padd64(r1, r2, r3) ->
           fprintf oc "	add	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
       | Paddc(r1, r2, r3) ->
@@ -435,14 +426,7 @@ module Target (System : SYSTEM):TARGET =
       | Pbf(bit, lbl) ->
           if !Clflags.option_faligncondbranchs > 0 then
             fprintf oc "	.balign	%d\n" !Clflags.option_faligncondbranchs;
-          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
+          fprintf oc "	bf	%a, %a\n" crbit bit label (transl_label lbl)
       | Pbl(s, sg) ->
           fprintf oc "	bl	%a\n" symbol s
       | Pbs(s, sg) ->
@@ -452,14 +436,7 @@ module Target (System : SYSTEM):TARGET =
       | Pbt(bit, lbl) ->
           if !Clflags.option_faligncondbranchs > 0 then
             fprintf oc "	.balign	%d\n" !Clflags.option_faligncondbranchs;
-          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
+          fprintf oc "	bt	%a, %a\n" crbit bit label (transl_label lbl)
       | Pbtbl(r, tbl) ->
           let lbl = new_label() in
           fprintf oc "%s begin pseudoinstr btbl(%a)\n" comment ireg r;
@@ -866,39 +843,15 @@ module Target (System : SYSTEM):TARGET =
       | Pblr -> false
       | _ -> true
 
-    (* Estimate the size of an Asm instruction encoding, in number of actual
-       PowerPC instructions.  We can over-approximate. *)
-
-    let instr_size = function
-      | Pbf(bit, lbl) -> 2
-      | Pbt(bit, lbl) -> 2
-      | Pbtbl(r, tbl) -> 5
-      | Pldi (r1,c) -> 2
-      | Plfi(r1, c) -> 2
-      | Plfis(r1, c) -> 2
-      | Plabel lbl -> 0
-      | Pbuiltin((EF_annot _ | EF_debug _), args, res) -> 0
-      | Pbuiltin(ef, args, res) -> 3
-      | Pcfi_adjust _ | Pcfi_rel_offset _ -> 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 print_instructions oc fn =
-      let rec aux  oc tbl pc fallthrough = function
+      let rec aux oc fallthrough = function
       | [] -> ()
       | i :: c ->
-          print_instruction oc tbl pc fallthrough i;
-         aux oc tbl (pc + instr_size i) (instr_fall_through i) c in
-      aux oc (label_positions PTree.empty 0 fn.fn_code) 0 true fn.fn_code
+          print_instruction oc fallthrough i;
+          aux oc (instr_fall_through i) c in
+      aux oc true fn.fn_code
 
     (* Print the code for a function *)