From 24ff7f7e368df849f2c4d386e2c964968567d253 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 24 Feb 2026 13:48:10 +0100 Subject: [PATCH 1/3] Branch relaxation, target-independent part --- backend/Asmexpandaux.ml | 63 +++++++++++++++++++++++++++++++++++++++- backend/Asmexpandaux.mli | 23 +++++++++++++++ 2 files changed, 85 insertions(+), 1 deletion(-) diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml index 519481a659..455240ef0a 100644 --- a/backend/Asmexpandaux.ml +++ b/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 diff --git a/backend/Asmexpandaux.mli b/backend/Asmexpandaux.mli index e2320418d0..13ce61983c 100644 --- a/backend/Asmexpandaux.mli +++ b/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 From 31209d63a3c8feb77c512a76885cfab5c2bca828 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 24 Feb 2026 13:56:56 +0100 Subject: [PATCH 2/3] Branch relaxation for AArch64 Fixes: #564 --- aarch64/Asmexpand.ml | 67 +++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 66 insertions(+), 1 deletion(-) diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index 98107a85d5..8aee91b783 100644 --- a/aarch64/Asmexpand.ml +++ b/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) From 26b592ffb4344ce70fc99ea8bce6cb2e41ed6b67 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 24 Feb 2026 14:24:55 +0100 Subject: [PATCH 3/3] Branch relaxation for PowerPC Replaces the previous, less precise implementation of branch relaxation. --- powerpc/Asmexpand.ml | 46 +++++++++++++++++++++++++++++- powerpc/TargetPrinter.ml | 61 +++++----------------------------------- 2 files changed, 52 insertions(+), 55 deletions(-) diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 5ff32f25b4..8a5aad9c10 100644 --- a/powerpc/Asmexpand.ml +++ b/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) diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 5274a47c55..47c767f108 100644 --- a/powerpc/TargetPrinter.ml +++ b/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 *)