aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/TargetPrinter.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@college-de-france.fr>2022-08-22 17:35:49 +0200
committerXavier Leroy <xavier.leroy@college-de-france.fr>2022-08-29 13:55:35 +0200
commit169007c52e27ce1fce6ca5fdd5fc7f43071b8841 (patch)
tree86e52680d32759cf4c78219fb245bd0467c070a1 /aarch64/TargetPrinter.ml
parent50836f2a04575402aa61a256fe7047c16610992f (diff)
downloadcompcert-169007c52e27ce1fce6ca5fdd5fc7f43071b8841.tar.gz
compcert-169007c52e27ce1fce6ca5fdd5fc7f43071b8841.zip
Support mergeable sections for fixed-size literals
On platforms that support them (ELF, macOS), use mergeable sections (like `.rodata.cst8`) for 4-, 8- and 16-byte wide literals. Works only if the LITERAL section is the default one. If the user provided their own LITERAL section, all literals are put in it regardless of their sizes. Support for mergeable string sections is introduced in this commit too but needs further changes in C2C.ml .
Diffstat (limited to 'aarch64/TargetPrinter.ml')
-rw-r--r--aarch64/TargetPrinter.ml57
1 files changed, 25 insertions, 32 deletions
diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
index a9d47bdd..ce6c51fc 100644
--- a/aarch64/TargetPrinter.ml
+++ b/aarch64/TargetPrinter.ml
@@ -165,8 +165,10 @@ module ELF_System : SYSTEM =
variable_section ~sec:".data" ~bss:".bss" i
| Section_const i | Section_small_const i ->
variable_section ~sec:".section .rodata" i
- | Section_string -> ".section .rodata"
- | Section_literal -> ".section .rodata"
+ | Section_string sz ->
+ elf_mergeable_string_section sz ".section .rodata"
+ | Section_literal sz ->
+ elf_mergeable_literal_section sz ".section .rodata"
| Section_jumptable -> ".section .rodata"
| Section_debug_info _ -> ".section .debug_info,\"\",%progbits"
| Section_debug_loc -> ".section .debug_loc,\"\",%progbits"
@@ -227,8 +229,10 @@ module MacOS_System : SYSTEM =
variable_section ~sec:".data" i
| Section_const i | Section_small_const i ->
variable_section ~sec:".const" ~reloc:".const_data" i
- | Section_string -> ".const"
- | Section_literal -> ".const"
+ | Section_string sz ->
+ macos_mergeable_string_section sz
+ | Section_literal sz ->
+ macos_mergeable_literal_section sz
| Section_jumptable -> ".text"
| Section_user(s, wr, ex) ->
sprintf ".section \"%s\", %s, %s"
@@ -273,25 +277,21 @@ module Target(System: SYSTEM): TARGET =
(* Associate labels to floating-point constants and to symbols. *)
let emit_constants oc lit =
- if exists_constants () then begin
- section oc lit;
- if Hashtbl.length literal64_labels > 0 then
- begin
- fprintf oc " .balign 8\n";
- Hashtbl.iter
- (fun bf lbl -> fprintf oc "%a: .quad 0x%Lx\n" label lbl bf)
- literal64_labels
- end;
- if Hashtbl.length literal32_labels > 0 then
- begin
- fprintf oc " .balign 4\n";
- Hashtbl.iter
- (fun bf lbl ->
- fprintf oc "%a: .long 0x%lx\n" label lbl bf)
- literal32_labels
- end;
- reset_literals ()
- end
+ if Hashtbl.length literal64_labels > 0 then begin
+ section oc (Sections.with_size 8 lit);
+ fprintf oc " .balign 8\n";
+ Hashtbl.iter
+ (fun bf lbl -> fprintf oc "%a: .quad 0x%Lx\n" label lbl bf)
+ literal64_labels
+ end;
+ if Hashtbl.length literal32_labels > 0 then begin
+ section oc (Sections.with_size 4 lit);
+ fprintf oc " .balign 4\n";
+ Hashtbl.iter
+ (fun bf lbl -> fprintf oc "%a: .long 0x%lx\n" label lbl bf)
+ literal32_labels
+ end;
+ reset_literals ()
(* Emit .file / .loc debugging directives *)
@@ -644,17 +644,10 @@ module Target(System: SYSTEM): TARGET =
assert false
end
- let get_section_names name =
- let (text, lit) =
- match C2C.atom_sections name with
- | t :: l :: _ -> (t, l)
- | _ -> (Section_text, Section_literal) in
- text,lit,Section_jumptable
-
let print_align oc alignment =
fprintf oc " .balign %d\n" alignment
- let print_jumptable oc jmptbl =
+ let print_jumptable oc _jmptbl =
let print_tbl oc (lbl, tbl) =
fprintf oc "%a:\n" label lbl;
List.iter
@@ -663,7 +656,7 @@ module Target(System: SYSTEM): TARGET =
tbl in
if !jumptables <> [] then
begin
- section oc jmptbl;
+ section oc Section_jumptable;
fprintf oc " .balign 4\n";
List.iter (print_tbl oc) !jumptables;
jumptables := []