aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
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 /riscV
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 'riscV')
-rw-r--r--riscV/TargetPrinter.ml51
1 files changed, 21 insertions, 30 deletions
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 366dc02e..f86664e9 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -111,8 +111,10 @@ module Target : TARGET =
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"
@@ -131,25 +133,21 @@ module Target : 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 " .align 3\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 " .align 2\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 " .align 3\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 " .align 2\n";
+ Hashtbl.iter
+ (fun bf lbl -> fprintf oc "%a: .long 0x%lx\n" label lbl bf)
+ literal32_labels
+ end;
+ reset_literals ()
(* Generate code to load the address of id + ofs in register r *)
@@ -590,17 +588,10 @@ module Target : 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
@@ -609,7 +600,7 @@ module Target : 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 := []