aboutsummaryrefslogtreecommitdiffstats
path: root/backend
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 /backend
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 'backend')
-rw-r--r--backend/JsonAST.ml9
-rw-r--r--backend/PrintAsm.ml7
-rw-r--r--backend/PrintAsmaux.ml27
3 files changed, 39 insertions, 4 deletions
diff --git a/backend/JsonAST.ml b/backend/JsonAST.ml
index 8ab874b1..c79fbde8 100644
--- a/backend/JsonAST.ml
+++ b/backend/JsonAST.ml
@@ -35,6 +35,11 @@ let pp_section pp sec =
pp_jobject_start pp;
pp_jmember ~first:true pp "Section Name" pp_jstring name;
pp_jmember pp "Init" pp_init init;
+ pp_jobject_end pp
+ and pp_complex_int name sz =
+ pp_jobject_start pp;
+ pp_jmember ~first:true pp "Section Name" pp_jstring name;
+ pp_jmember pp "Size" pp_jint sz;
pp_jobject_end pp in
match sec with
@@ -43,8 +48,8 @@ let pp_section pp sec =
| Section_small_data init -> pp_complex "Small Data" init
| Section_const init -> pp_complex "Const" init
| Section_small_const init -> pp_complex "Small Const" init
- | Section_string -> pp_simple "String"
- | Section_literal -> pp_simple "Literal"
+ | Section_string sz -> pp_complex_int "String" sz
+ | Section_literal sz -> pp_complex_int "Literal" sz
| Section_jumptable -> pp_simple "Jumptable"
| Section_user (s,w,e) ->
pp_jobject_start pp;
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index 22df68ae..6d1fafd6 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -37,10 +37,15 @@ module Printer(Target:TARGET) =
let print_location oc loc =
if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc)
+ let get_section_names name =
+ match C2C.atom_sections name with
+ | [t;l;j] -> (t, l, j)
+ | _ -> (Section_text, Section_literal 0, Section_jumptable)
+
let print_function oc name fn =
Hashtbl.clear current_function_labels;
Debug.symbol_printed (extern_atom name);
- let (text, lit, jmptbl) = Target.get_section_names name in
+ let (text, lit, jmptbl) = get_section_names name in
Target.section oc text;
let alignment =
match !Clflags.option_falignfunctions with Some n -> n | None -> Target.default_falignment in
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index e39ba8aa..841f4579 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -28,7 +28,6 @@ module type TARGET =
val print_comm_symb: out_channel -> Z.t -> P.t -> int -> unit
val print_var_info: out_channel -> P.t -> unit
val print_fun_info: out_channel -> P.t -> unit
- val get_section_names: P.t -> section_name * section_name * section_name
val print_file_line: out_channel -> string -> int -> unit
val print_optional_fun_info: out_channel -> unit
val cfi_startproc: out_channel -> unit
@@ -328,3 +327,29 @@ let variable_section ~sec ?bss ?reloc ?(common = !Clflags.option_fcommon) i =
| Init -> sec
| Init_reloc ->
begin match reloc with Some s -> s | None -> sec end
+
+(** ELF and macOS mergeable section names for literals and strings. *)
+
+let elf_mergeable_literal_section sz sec =
+ match sz with
+ | 0 -> sec
+ | 4 | 8 | 16 -> sprintf "%s.cst%d,\"aM\",@progbits,%d" sec sz sz
+ | _ -> assert false
+
+let elf_mergeable_string_section sz sec =
+ match sz with
+ | 0 -> sec
+ | 1 | 2 | 4 -> sprintf "%s.str%d.%d,\"aMS\",@progbits,%d" sec sz sz sz
+ | _ -> assert false
+
+let macos_mergeable_literal_section sz =
+ match sz with
+ | 0 -> ".const"
+ | 4 | 8 | 16 -> sprintf ".literal%d" sz
+ | _ -> assert false
+
+let macos_mergeable_string_section sz =
+ match sz with
+ | 0 | 2 | 4 -> ".const"
+ | 1 -> ".cstring"
+ | _ -> assert false