From be92a8c71192e014caf292312865dee32ee1b901 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Apr 2020 08:29:28 +0200 Subject: moved to common place --- backend/PrintAsmaux.ml | 56 +++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 55 insertions(+), 1 deletion(-) (limited to 'backend/PrintAsmaux.ml') diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index d82e6f84..27d161ee 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -310,4 +310,58 @@ let common_section ?(sec = ".bss") () = if !Clflags.option_fcommon then "COMM" else - sec + sec;; + +(* Profiling *) +let profiling_table : (Digest.t, int) Hashtbl.t = Hashtbl.create 1000;; +let next_profiling_position = ref 0;; +let profiling_position (x : Digest.t) : int = + match Hashtbl.find_opt profiling_table x with + | None -> let y = !next_profiling_position in + next_profiling_position := succ y; + Hashtbl.replace profiling_table x y; + y + | Some y -> y;; + +let profiling_ids () = + let nr_items = !next_profiling_position in + let ar = Array.make nr_items "" in + Hashtbl.iter + (fun x y -> ar.(y) <- x) + profiling_table; + ar;; + +let print_profiling_id oc id = + assert (String.length id = 16); + output_string oc " .byte"; + for i=0 to 15 do + fprintf oc " 0x%02x" (Char.code (String.get id i)); + if i < 15 then output_char oc ',' + done; + output_char oc '\n';; + +let profiling_counter_table_name = ".compcert_profiling_counters" +and profiling_id_table_name = ".compcert_profiling_ids" +and profiling_write_table = ".compcert_profiling_write_table" +and profiling_write_table_helper = "_compcert_write_profiling_table" +and dtor_section = ".dtors.65435";; + +let print_profiling finalizer_section print_profiling_stub oc = + let nr_items = !next_profiling_position in + if nr_items > 0 + then + begin + fprintf oc " .lcomm %s, %d\n" + profiling_counter_table_name (nr_items * 16); + fprintf oc " .section .rodata\n"; + fprintf oc "%s:\n" profiling_id_table_name; + Array.iter (print_profiling_id oc) (profiling_ids ()); + fprintf oc " .text\n"; + fprintf oc "%s:\n" profiling_write_table; + print_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name; + fprintf oc " .section %s,\"aw\",@progbits\n" finalizer_section; + fprintf oc " .align 8\n"; + fprintf oc " .8byte %s\n" profiling_write_table + end;; -- cgit From 3d0204fddb71ca377fa65952ede872583c8a7242 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Apr 2020 14:06:41 +0200 Subject: various fixes for aarch64 profiling --- backend/PrintAsmaux.ml | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) (limited to 'backend/PrintAsmaux.ml') diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 27d161ee..153b9412 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -344,7 +344,8 @@ let profiling_counter_table_name = ".compcert_profiling_counters" and profiling_id_table_name = ".compcert_profiling_ids" and profiling_write_table = ".compcert_profiling_write_table" and profiling_write_table_helper = "_compcert_write_profiling_table" -and dtor_section = ".dtors.65435";; +and dtor_section = ".dtors.65435,\"aw\",@progbits" +and fini_section = ".fini_array.00100,\"aw\"";; let print_profiling finalizer_section print_profiling_stub oc = let nr_items = !next_profiling_position in @@ -361,7 +362,14 @@ let print_profiling finalizer_section print_profiling_stub oc = print_profiling_stub oc nr_items profiling_id_table_name profiling_counter_table_name; - fprintf oc " .section %s,\"aw\",@progbits\n" finalizer_section; + fprintf oc " .type %s, @function\n" profiling_write_table; + fprintf oc " .size %s, . - %s\n" profiling_write_table profiling_write_table; + fprintf oc " .section %s\n" finalizer_section; fprintf oc " .align 8\n"; - fprintf oc " .8byte %s\n" profiling_write_table + (if Archi.ptr64 + then fprintf oc " .8byte %s\n" profiling_write_table + else fprintf oc " .4byte %s\n" profiling_write_table) end;; + +let profiling_offset id kind = + ((profiling_position id)*2 + kind)*8;; -- cgit From 76f48469c4b4ca49159dc736830cd806f8dbbf07 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Apr 2020 14:57:37 +0200 Subject: fix write table --- backend/PrintAsmaux.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'backend/PrintAsmaux.ml') diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 153b9412..5a074867 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -365,7 +365,6 @@ let print_profiling finalizer_section print_profiling_stub oc = fprintf oc " .type %s, @function\n" profiling_write_table; fprintf oc " .size %s, . - %s\n" profiling_write_table profiling_write_table; fprintf oc " .section %s\n" finalizer_section; - fprintf oc " .align 8\n"; (if Archi.ptr64 then fprintf oc " .8byte %s\n" profiling_write_table else fprintf oc " .4byte %s\n" profiling_write_table) -- cgit From 50d59f7ab7ae06de2ae6439752f0b56695d539df Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Apr 2020 20:55:44 +0200 Subject: fix writing profiling info for Aarch64 --- backend/PrintAsmaux.ml | 39 ++++++++++++++++++++++++++++++--------- 1 file changed, 30 insertions(+), 9 deletions(-) (limited to 'backend/PrintAsmaux.ml') diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 5a074867..c7161615 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -342,12 +342,27 @@ let print_profiling_id oc id = let profiling_counter_table_name = ".compcert_profiling_counters" and profiling_id_table_name = ".compcert_profiling_ids" -and profiling_write_table = ".compcert_profiling_write_table" +and profiling_write_table = ".compcert_profiling_save_for_this_object" +and profiling_init = ".compcert_profiling_init" and profiling_write_table_helper = "_compcert_write_profiling_table" and dtor_section = ".dtors.65435,\"aw\",@progbits" -and fini_section = ".fini_array.00100,\"aw\"";; +(* and fini_section = ".fini_array_00100,\"aw\"" *) +and init_section = ".init_array,\"aw\"";; -let print_profiling finalizer_section print_profiling_stub oc = +type finalizer_call_method = + | Dtors + | Init_atexit of (out_channel -> string -> unit);; + +let write_symbol_pointer oc sym = + if Archi.ptr64 + then fprintf oc " .8byte %s\n" sym + else fprintf oc " .4byte %s\n" sym;; + +let declare_function oc name = + fprintf oc " .type %s, @function\n" name; + fprintf oc " .size %s, . - %s\n" name name;; + +let print_profiling_epilogue finalizer_call_method print_profiling_stub oc = let nr_items = !next_profiling_position in if nr_items > 0 then @@ -362,12 +377,18 @@ let print_profiling finalizer_section print_profiling_stub oc = print_profiling_stub oc nr_items profiling_id_table_name profiling_counter_table_name; - fprintf oc " .type %s, @function\n" profiling_write_table; - fprintf oc " .size %s, . - %s\n" profiling_write_table profiling_write_table; - fprintf oc " .section %s\n" finalizer_section; - (if Archi.ptr64 - then fprintf oc " .8byte %s\n" profiling_write_table - else fprintf oc " .4byte %s\n" profiling_write_table) + declare_function oc profiling_write_table; + match finalizer_call_method with + | Dtors -> + fprintf oc " .section %s\n" dtor_section; + write_symbol_pointer oc profiling_write_table + | Init_atexit(atexit_call) -> + fprintf oc " .section %s\n" init_section; + write_symbol_pointer oc profiling_init; + fprintf oc " .text\n"; + fprintf oc "%s:\n" profiling_init; + atexit_call oc profiling_write_table; + declare_function oc profiling_init end;; let profiling_offset id kind = -- cgit From f50a1c1e1dc194c78b68ecdc7e3f6c0b0448f5f4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 Apr 2020 10:29:45 +0200 Subject: seems like the ARM profiling perhaps works --- backend/PrintAsmaux.ml | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) (limited to 'backend/PrintAsmaux.ml') diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index c7161615..cc7b33c3 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -358,11 +358,7 @@ let write_symbol_pointer oc sym = then fprintf oc " .8byte %s\n" sym else fprintf oc " .4byte %s\n" sym;; -let declare_function oc name = - fprintf oc " .type %s, @function\n" name; - fprintf oc " .size %s, . - %s\n" name name;; - -let print_profiling_epilogue finalizer_call_method print_profiling_stub oc = +let print_profiling_epilogue declare_function finalizer_call_method print_profiling_stub oc = let nr_items = !next_profiling_position in if nr_items > 0 then -- cgit From 5862a7517105b822224191e05ff203924e408ed5 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 Apr 2020 11:24:30 +0200 Subject: fix for aarch64 --- backend/PrintAsmaux.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'backend/PrintAsmaux.ml') diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index cc7b33c3..25792df5 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -111,6 +111,10 @@ let elf_symbol_offset oc (symb, ofs) = if ofs <> 0L then fprintf oc " + %Ld" ofs (* Functions for fun and var info *) +let elf_text_print_fun_info oc name = + fprintf oc " .type %s, @function\n" name; + fprintf oc " .size %s, . - %s\n" name name + let elf_print_fun_info oc name = fprintf oc " .type %a, @function\n" elf_symbol name; fprintf oc " .size %a, . - %a\n" elf_symbol name elf_symbol name -- cgit From 7299996cac6c4747b6611b17f0af15fb08c6ee80 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 Apr 2020 22:02:46 +0200 Subject: fix reverse printing problem for hashes --- backend/PrintAsmaux.ml | 54 ++++++++++++++++++++++++++------------------------ 1 file changed, 28 insertions(+), 26 deletions(-) (limited to 'backend/PrintAsmaux.ml') diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 25792df5..7a281684 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -363,33 +363,35 @@ let write_symbol_pointer oc sym = else fprintf oc " .4byte %s\n" sym;; let print_profiling_epilogue declare_function finalizer_call_method print_profiling_stub oc = - let nr_items = !next_profiling_position in - if nr_items > 0 + if !Clflags.option_profile_arcs then - begin - fprintf oc " .lcomm %s, %d\n" - profiling_counter_table_name (nr_items * 16); - fprintf oc " .section .rodata\n"; - fprintf oc "%s:\n" profiling_id_table_name; - Array.iter (print_profiling_id oc) (profiling_ids ()); - fprintf oc " .text\n"; - fprintf oc "%s:\n" profiling_write_table; - print_profiling_stub oc nr_items - profiling_id_table_name - profiling_counter_table_name; - declare_function oc profiling_write_table; - match finalizer_call_method with - | Dtors -> - fprintf oc " .section %s\n" dtor_section; - write_symbol_pointer oc profiling_write_table - | Init_atexit(atexit_call) -> - fprintf oc " .section %s\n" init_section; - write_symbol_pointer oc profiling_init; - fprintf oc " .text\n"; - fprintf oc "%s:\n" profiling_init; - atexit_call oc profiling_write_table; - declare_function oc profiling_init - end;; + let nr_items = !next_profiling_position in + if nr_items > 0 + then + begin + fprintf oc " .lcomm %s, %d\n" + profiling_counter_table_name (nr_items * 16); + fprintf oc " .section .rodata\n"; + fprintf oc "%s:\n" profiling_id_table_name; + Array.iter (print_profiling_id oc) (profiling_ids ()); + fprintf oc " .text\n"; + fprintf oc "%s:\n" profiling_write_table; + print_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name; + declare_function oc profiling_write_table; + match finalizer_call_method with + | Dtors -> + fprintf oc " .section %s\n" dtor_section; + write_symbol_pointer oc profiling_write_table + | Init_atexit(atexit_call) -> + fprintf oc " .section %s\n" init_section; + write_symbol_pointer oc profiling_init; + fprintf oc " .text\n"; + fprintf oc "%s:\n" profiling_init; + atexit_call oc profiling_write_table; + declare_function oc profiling_init + end;; let profiling_offset id kind = ((profiling_position id)*2 + kind)*8;; -- cgit