Skip to content

Commit 14c0b59

Browse files
xavierleroyxavierleroy
authored
Merge pull request #575 from AbsInt/relaxation
Branch relaxation for AArch64 and PowerPC, prior to asm generation.
2 parents 7b1f02b + 1eb6cc7 commit 14c0b59

6 files changed

Lines changed: 236 additions & 58 deletions

File tree

‎aarch64/Asmexpand.ml‎

Lines changed: 81 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -407,6 +407,85 @@ let expand_builtin_inline name args res =
407407
| _ ->
408408
raise (Error ("unrecognized builtin " ^ name))
409409

410+
(* Number of statements in a piece of inline assembly code.
411+
This gives an upper bound on the number of machine instructions.
412+
(Some statements can be labels or directives.) *)
413+
414+
let re_asm_comment = Str.regexp "\\(//\\|^#\\).*$" (* // or # at BOL *)
415+
let re_blank_line = Str.regexp "^[ \t]*\n"
416+
let re_asm_stmt_separator = Str.regexp "[\n;]" (* newline or ; *)
417+
418+
let num_statements_inline_asm txt =
419+
txt |> Str.global_replace re_asm_comment ""
420+
|> Str.global_replace re_blank_line ""
421+
|> Str.split re_asm_stmt_separator
422+
|> List.length
423+
424+
(* Branch relaxation *)
425+
426+
module BInfo: BRANCH_INFORMATION = struct
427+
428+
let builtin_size = function
429+
| EF_annot _ -> 0
430+
| EF_debug _ -> 0
431+
| EF_inline_asm(txt, _, _) -> 4 * num_statements_inline_asm txt
432+
| _ -> assert false
433+
434+
let instr_size = function
435+
| Pfmovimmd _ | Pfmovimms _ -> 8
436+
| Ploadsymbol _ -> 2
437+
| Pbtbl(_, tbl) -> 12 + 4 * List.length tbl
438+
| Plabel _ | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
439+
| Pbuiltin(ef, _, _) -> builtin_size ef
440+
| _ -> 4
441+
442+
let branch_overflow ~map pc lbl range =
443+
let displ = pc + 4 - map lbl in
444+
displ < -range || displ >= range
445+
446+
let need_relaxation ~map pc instr =
447+
match instr with
448+
| Pbc(_, lbl) | Pcbnz(_, _, lbl) | Pcbz(_, _, lbl) ->
449+
(* +/- 1 MB *)
450+
branch_overflow ~map pc lbl 0x100_000
451+
| Ptbnz(_, _, _, lbl) | Ptbz(_, _, _, lbl) ->
452+
(* +/- 32 KB *)
453+
branch_overflow ~map pc lbl 0x8_000
454+
| _ ->
455+
false
456+
457+
let negate_testcond = function
458+
| TCeq -> TCne | TCne -> TCeq
459+
| TChs -> TClo | TClo -> TChs
460+
| TCmi -> TCpl | TCpl -> TCmi
461+
| TChi -> TCls | TCls -> TChi
462+
| TCge -> TClt | TClt -> TCge
463+
| TCgt -> TCle | TCle -> TCgt
464+
465+
let relax_instruction instr =
466+
match instr with
467+
| Pbc(c, lbl) ->
468+
let lbl' = new_label() in
469+
[Pbc(negate_testcond c, lbl'); Pb lbl; Plabel lbl']
470+
| Pcbnz(sz, r, lbl) ->
471+
let lbl' = new_label() in
472+
[Pcbz(sz, r, lbl'); Pb lbl; Plabel lbl']
473+
| Pcbz(sz, r, lbl) ->
474+
let lbl' = new_label() in
475+
[Pcbnz(sz, r, lbl'); Pb lbl; Plabel lbl']
476+
| Ptbnz(sz, r, n, lbl) ->
477+
let lbl' = new_label() in
478+
[Ptbz(sz, r, n, lbl'); Pb lbl; Plabel lbl']
479+
| Ptbz(sz, r, n, lbl) ->
480+
let lbl' = new_label() in
481+
[Ptbnz(sz, r, n, lbl'); Pb lbl; Plabel lbl']
482+
| _ ->
483+
assert false
484+
485+
end
486+
487+
module BRelax = Branch_relaxation (BInfo)
488+
410489
(* Expansion of instructions *)
411490

412491
let expand_instruction instr =
@@ -478,7 +557,8 @@ let expand_function id fn =
478557
try
479558
set_current_function fn;
480559
expand id (* sp= *) 31 preg_to_dwarf expand_instruction fn.fn_code;
481-
Errors.OK (get_current_function ())
560+
let fn' = BRelax.relaxation (get_current_function ()) in
561+
Errors.OK fn'
482562
with Error s ->
483563
Errors.Error (Errors.msg s)
484564

‎backend/Asmexpandaux.ml‎

Lines changed: 62 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,9 +11,10 @@
1111
(* *)
1212
(* *********************************************************************)
1313

14-
(* Util functions used for the expansion of built-ins and some
14+
(* Utility functions used for the expansion of built-ins and some
1515
pseudo-instructions *)
1616

17+
open Maps
1718
open Asm
1819
open AST
1920
open Camlcoq
@@ -186,3 +187,63 @@ let expand id sp preg simple l =
186187
expand_debug id sp preg simple l
187188
else
188189
expand_simple simple l
190+
191+
(* Branch relaxation *)
192+
193+
module type BRANCH_INFORMATION = sig
194+
val instr_size: instruction -> int
195+
val need_relaxation: map: (label -> int) -> int -> instruction -> bool
196+
val relax_instruction: instruction -> instruction list
197+
end
198+
199+
module Branch_relaxation (B: BRANCH_INFORMATION) = struct
200+
201+
(* Fill the table label -> position in code *)
202+
203+
let rec set_label_positions tbl pc = function
204+
| [] ->
205+
tbl
206+
| Plabel lbl :: code ->
207+
set_label_positions (PTree.set lbl pc tbl) pc code
208+
| instr :: code ->
209+
set_label_positions tbl (pc + B.instr_size instr) code
210+
211+
let get_label_position tbl lbl =
212+
match PTree.get lbl tbl with
213+
| Some pc -> pc
214+
| None ->
215+
invalid_arg
216+
(Printf.sprintf "Fatal error: unknown label %d" (P.to_int lbl))
217+
218+
let rec need_relaxation tbl pc = function
219+
| [] ->
220+
false
221+
| instr :: code ->
222+
B.need_relaxation ~map:(get_label_position tbl) pc instr
223+
|| need_relaxation tbl (pc + B.instr_size instr) code
224+
225+
let rec do_relaxation tbl accu pc = function
226+
| [] ->
227+
List.rev accu
228+
| instr :: code ->
229+
do_relaxation
230+
tbl
231+
(if B.need_relaxation ~map:(get_label_position tbl) pc instr
232+
then List.rev_append (B.relax_instruction instr) accu
233+
else instr :: accu)
234+
(pc + B.instr_size instr)
235+
code
236+
237+
let relaxation fn =
238+
set_current_function fn;
239+
let rec relax fn =
240+
let tbl = set_label_positions PTree.empty 0 fn.fn_code in
241+
if not (need_relaxation tbl 0 fn.fn_code) then fn else begin
242+
let code' = do_relaxation tbl [] 0 fn.fn_code in
243+
relax {fn with fn_code = code'}
244+
end in
245+
let res = relax fn in
246+
set_current_function dummy_function;
247+
res
248+
249+
end

‎backend/Asmexpandaux.mli‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,3 +34,26 @@ val get_current_function: unit -> coq_function
3434
val expand: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit
3535
(* Expand the instruction sequence of a function. Takes the function id, the register number of the stackpointer, a
3636
function to get the dwarf mapping of variable names and for the expansion of simple instructions *)
37+
38+
(** Branch relaxation. Rewrite the Asm code after builtin expansion
39+
to avoid overflows in displacements of branching instructions. *)
40+
41+
module type BRANCH_INFORMATION = sig
42+
val instr_size: instruction -> int
43+
(* The size in bytes of the given instruction.
44+
Can over-approximate. *)
45+
val need_relaxation: map: (label -> int) -> int -> instruction -> bool
46+
(* [need_relaxation ~map pc instr] returns [true] if
47+
the given instruction is a branch that can overflow and
48+
needs to be rewritten.
49+
[pc] is the position of the instruction in the code (in bytes).
50+
[map] is a mapping from labels to code positions (also in bytes). *)
51+
val relax_instruction: instruction -> instruction list
52+
(* [relaxation instr] returns the list of instructions that perform
53+
the same branch as [instr] but avoid branch overflow.
54+
Can call [Asmexpandaux.new_label] to obtain fresh labels. *)
55+
end
56+
57+
module Branch_relaxation (_: BRANCH_INFORMATION) : sig
58+
val relaxation: coq_function -> coq_function
59+
end

‎powerpc/Asmexpand.ml‎

Lines changed: 62 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -827,6 +827,66 @@ let set_cr6 sg =
827827
else emit (Pcrxor(CRbit_6, CRbit_6, CRbit_6))
828828
end
829829

830+
(* Number of statements in a piece of inline assembly code.
831+
This gives an upper bound on the number of machine instructions.
832+
(Some statements can be labels or directives.) *)
833+
834+
let re_asm_comment =
835+
if Configuration.system = "diab"
836+
then Str.regexp "[#;].*$" (* comments start with # or ; *)
837+
else Str.regexp "#.*$" (* comments start with # *)
838+
let re_blank_line = Str.regexp "^[ \t]*\n"
839+
let re_asm_stmt_separator = Str.regexp "[\n;]" (* newline or ; *)
840+
841+
let num_statements_inline_asm txt =
842+
txt |> Str.global_replace re_asm_comment ""
843+
|> Str.global_replace re_blank_line ""
844+
|> Str.split re_asm_stmt_separator
845+
|> List.length
846+
847+
(* Branch relaxation *)
848+
849+
module BInfo: BRANCH_INFORMATION = struct
850+
851+
let builtin_size = function
852+
| EF_annot _ -> 0
853+
| EF_debug _ -> 0
854+
| EF_inline_asm(txt, _, _) -> 4 * num_statements_inline_asm txt
855+
| _ -> assert false
856+
857+
let instr_size = function
858+
| Pbtbl(r, tbl) -> 20
859+
| Pldi (r1,c) -> 8
860+
| Plfi(r1, c) -> 8
861+
| Plfis(r1, c) -> 8
862+
| Plabel lbl -> 0
863+
| Pbuiltin(ef, _, _) -> builtin_size ef
864+
| Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
865+
| _ -> 4
866+
867+
let need_relaxation ~map pc instr =
868+
match instr with
869+
| Pbf(_, lbl) | Pbt(_, lbl) ->
870+
let displ = pc + 4 - map lbl in
871+
displ < -0x8000 || displ >= 0x8000
872+
| _ ->
873+
false
874+
875+
let relax_instruction instr =
876+
match instr with
877+
| Pbf(bit, lbl) ->
878+
let lbl' = new_label() in
879+
[Pbt(bit, lbl'); Pb lbl; Plabel lbl']
880+
| Pbt(bit, lbl) ->
881+
let lbl' = new_label() in
882+
[Pbf(bit, lbl'); Pb lbl; Plabel lbl']
883+
| _ ->
884+
assert false
885+
886+
end
887+
888+
module BRelax = Branch_relaxation (BInfo)
889+
830890
(* Expand instructions *)
831891

832892
let expand_instruction instr =
@@ -973,7 +1033,8 @@ let expand_function id fn =
9731033
try
9741034
set_current_function fn;
9751035
expand id 1 preg_to_dwarf expand_instruction fn.fn_code;
976-
Errors.OK (get_current_function ())
1036+
let fn' = BRelax.relaxation (get_current_function ()) in
1037+
Errors.OK fn'
9771038
with Error s ->
9781039
Errors.Error (Errors.msg s)
9791040

‎powerpc/TargetPrinter.ml‎

Lines changed: 7 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@
1414

1515
open Printf
1616
open Fileinfo
17-
open Maps
1817
open Camlcoq
1918
open Sections
2019
open AST
@@ -381,17 +380,9 @@ module Target (System : SYSTEM):TARGET =
381380
assert false
382381
in leftmost_one 0 0x8000_0000_0000_0000L
383382

384-
(* Determine if the displacement of a conditional branch fits the short form *)
385-
386-
let short_cond_branch tbl pc lbl_dest =
387-
match PTree.get lbl_dest tbl with
388-
| None -> assert false
389-
| Some pc_dest ->
390-
let disp = pc_dest - pc in -0x2000 <= disp && disp < 0x2000
391-
392383
(* Printing of instructions *)
393384

394-
let print_instruction oc tbl pc fallthrough = function
385+
let print_instruction oc fallthrough = function
395386
| Padd(r1, r2, r3) | Padd64(r1, r2, r3) ->
396387
fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3
397388
| Paddc(r1, r2, r3) ->
@@ -435,14 +426,7 @@ module Target (System : SYSTEM):TARGET =
435426
| Pbf(bit, lbl) ->
436427
if !Clflags.option_faligncondbranchs > 0 then
437428
fprintf oc " .balign %d\n" !Clflags.option_faligncondbranchs;
438-
if short_cond_branch tbl pc lbl then
439-
fprintf oc " bf %a, %a\n" crbit bit label (transl_label lbl)
440-
else begin
441-
let next = new_label() in
442-
fprintf oc " bt %a, %a\n" crbit bit label next;
443-
fprintf oc " b %a\n" label (transl_label lbl);
444-
fprintf oc "%a:\n" label next
445-
end
429+
fprintf oc " bf %a, %a\n" crbit bit label (transl_label lbl)
446430
| Pbl(s, sg) ->
447431
fprintf oc " bl %a\n" symbol s
448432
| Pbs(s, sg) ->
@@ -452,14 +436,7 @@ module Target (System : SYSTEM):TARGET =
452436
| Pbt(bit, lbl) ->
453437
if !Clflags.option_faligncondbranchs > 0 then
454438
fprintf oc " .balign %d\n" !Clflags.option_faligncondbranchs;
455-
if short_cond_branch tbl pc lbl then
456-
fprintf oc " bt %a, %a\n" crbit bit label (transl_label lbl)
457-
else begin
458-
let next = new_label() in
459-
fprintf oc " bf %a, %a\n" crbit bit label next;
460-
fprintf oc " b %a\n" label (transl_label lbl);
461-
fprintf oc "%a:\n" label next
462-
end
439+
fprintf oc " bt %a, %a\n" crbit bit label (transl_label lbl)
463440
| Pbtbl(r, tbl) ->
464441
let lbl = new_label() in
465442
fprintf oc "%s begin pseudoinstr btbl(%a)\n" comment ireg r;
@@ -866,39 +843,15 @@ module Target (System : SYSTEM):TARGET =
866843
| Pblr -> false
867844
| _ -> true
868845

869-
(* Estimate the size of an Asm instruction encoding, in number of actual
870-
PowerPC instructions. We can over-approximate. *)
871-
872-
let instr_size = function
873-
| Pbf(bit, lbl) -> 2
874-
| Pbt(bit, lbl) -> 2
875-
| Pbtbl(r, tbl) -> 5
876-
| Pldi (r1,c) -> 2
877-
| Plfi(r1, c) -> 2
878-
| Plfis(r1, c) -> 2
879-
| Plabel lbl -> 0
880-
| Pbuiltin((EF_annot _ | EF_debug _), args, res) -> 0
881-
| Pbuiltin(ef, args, res) -> 3
882-
| Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
883-
| _ -> 1
884-
885-
(* Build a table label -> estimated position in generated code.
886-
Used to predict if relative conditional branches can use the short form. *)
887-
888-
let rec label_positions tbl pc = function
889-
| [] -> tbl
890-
| Plabel lbl :: c -> label_positions (PTree.set lbl pc tbl) pc c
891-
| i :: c -> label_positions tbl (pc + instr_size i) c
892-
893846
(* Emit a sequence of instructions *)
894847

895848
let print_instructions oc fn =
896-
let rec aux oc tbl pc fallthrough = function
849+
let rec aux oc fallthrough = function
897850
| [] -> ()
898851
| i :: c ->
899-
print_instruction oc tbl pc fallthrough i;
900-
aux oc tbl (pc + instr_size i) (instr_fall_through i) c in
901-
aux oc (label_positions PTree.empty 0 fn.fn_code) 0 true fn.fn_code
852+
print_instruction oc fallthrough i;
853+
aux oc (instr_fall_through i) c in
854+
aux oc true fn.fn_code
902855

903856
(* Print the code for a function *)
904857

‎test‎

0 commit comments

Comments
 (0)