aboutsummaryrefslogtreecommitdiffstats
path: root/backend/JsonAST.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 /backend/JsonAST.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 'backend/JsonAST.ml')
-rw-r--r--backend/JsonAST.ml9
1 files changed, 7 insertions, 2 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;