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 --- aarch64/TargetPrinter.ml | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) (limited to 'aarch64/TargetPrinter.ml') diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index e54673dd..bd26a45f 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -227,6 +227,28 @@ module Target : TARGET = | EOuxtw n -> fprintf oc ", uxtw #%a" coqint n | EOuxtx n -> fprintf oc ", uxtx #%a" coqint n + let next_profiling_label = + let atomic_incr_counter = ref 0 in + fun () -> + let r = sprintf ".compcert_atomic_incr%d" !atomic_incr_counter in + incr atomic_incr_counter; r;; + + let print_profiling_logger oc id kind = + assert (kind >= 0); + assert (kind <= 1); + fprintf oc "%s begin profiling %a %d: atomic increment\n" comment + Profilingaux.pp_id id kind; + let ofs = profiling_offset id kind and lbl = next_profiling_label () in + fprintf oc " adrp x15, %s+%d\n" profiling_counter_table_name ofs; + fprintf oc " add x15, x15, :lo12:(%s+%d)\n" profiling_counter_table_name ofs; + fprintf oc "%s:\n" lbl; + fprintf oc " ldaxr x17, [x15]\n"; + fprintf oc " add x17, x17, 1\n"; + fprintf oc " stlxr w17, x17, [x15]\n"; + fprintf oc " cbnz w17, %s\n" lbl; + fprintf oc "%s end profiling %a %d\n" comment + Profilingaux.pp_id id kind;; + (* Printing of instructions *) let print_instruction oc = function (* Branches *) @@ -519,6 +541,8 @@ module Target : TARGET = fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment + | EF_profiling (id, coq_kind) -> + print_profiling_logger oc id (Z.to_int coq_kind) | _ -> assert false end @@ -575,7 +599,19 @@ module Target : TARGET = section oc Section_text; end + let aarch64_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name = + fprintf oc " ret\n"; + fprintf oc " adrp x2, %s\n" profiling_counter_table_name; + fprintf oc " adrp x1, %s\n" profiling_id_table_name; + fprintf oc " add x2, x2, :lo12:%s\n" profiling_counter_table_name; + fprintf oc " add x1, x1, :lo12:%s\n" profiling_id_table_name; + fprintf oc " mov w0, %d\n" nr_items; + fprintf oc " b %s\n" profiling_write_table_helper ;; + let print_epilogue oc = + print_profiling fini_section aarch64_profiling_stub oc; if !Clflags.option_g then begin Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); section oc Section_text; -- cgit From 5659daa886559566fdb6306d989578707838a267 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Apr 2020 16:47:51 +0200 Subject: profiling still crashes on Aarch64 --- aarch64/TargetPrinter.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'aarch64/TargetPrinter.ml') diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index bd26a45f..0eaf3923 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -602,7 +602,6 @@ module Target : TARGET = let aarch64_profiling_stub oc nr_items profiling_id_table_name profiling_counter_table_name = - fprintf oc " ret\n"; fprintf oc " adrp x2, %s\n" profiling_counter_table_name; fprintf oc " adrp x1, %s\n" profiling_id_table_name; fprintf oc " add x2, x2, :lo12:%s\n" profiling_counter_table_name; -- cgit From b19b9defebf96ba8599f481d4c617d43c21642ef Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 10 Apr 2020 18:09:34 +0200 Subject: use proper local labels --- aarch64/TargetPrinter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64/TargetPrinter.ml') diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 0eaf3923..9d605336 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -230,7 +230,7 @@ module Target : TARGET = let next_profiling_label = let atomic_incr_counter = ref 0 in fun () -> - let r = sprintf ".compcert_atomic_incr%d" !atomic_incr_counter in + let r = sprintf ".Lcompcert_atomic_incr%d" !atomic_incr_counter in incr atomic_incr_counter; r;; let print_profiling_logger oc id kind = -- 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 --- aarch64/TargetPrinter.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'aarch64/TargetPrinter.ml') diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 9d605336..5f62c936 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -608,9 +608,15 @@ module Target : TARGET = fprintf oc " add x1, x1, :lo12:%s\n" profiling_id_table_name; fprintf oc " mov w0, %d\n" nr_items; fprintf oc " b %s\n" profiling_write_table_helper ;; + + let print_atexit oc to_be_called = + fprintf oc " adrp x0, %s\n" to_be_called; + fprintf oc " add x0, x0, :lo12:%s\n" to_be_called; + fprintf oc " b atexit\n";; + let print_epilogue oc = - print_profiling fini_section aarch64_profiling_stub oc; + print_profiling_epilogue (Init_atexit print_atexit) aarch64_profiling_stub oc; if !Clflags.option_g then begin Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); section oc Section_text; -- 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 --- aarch64/TargetPrinter.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64/TargetPrinter.ml') diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 5f62c936..ef9045ea 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -616,7 +616,7 @@ module Target : TARGET = let print_epilogue oc = - print_profiling_epilogue (Init_atexit print_atexit) aarch64_profiling_stub oc; + print_profiling_epilogue elf_text_print_fun_info (Init_atexit print_atexit) aarch64_profiling_stub oc; if !Clflags.option_g then begin Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f)); section oc Section_text; -- cgit