diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-12 19:23:28 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-12 19:23:28 +0200 |
commit | 9e00dd1645b6adcdb46739562cba0fc314ec3bed (patch) | |
tree | 9519a4d28224197b93d25dc55687322730757487 /aarch64 | |
parent | 47ecb1ec8d00636d6e7bb4cebd21df5d0b9b5ac7 (diff) | |
parent | 9e7f5e5611c5b5281b74b075b4524aef7bc05437 (diff) | |
download | compcert-kvx-9e00dd1645b6adcdb46739562cba0fc314ec3bed.tar.gz compcert-kvx-9e00dd1645b6adcdb46739562cba0fc314ec3bed.zip |
Merge remote-tracking branch 'origin/mppa-profiling' into mppa-features
Diffstat (limited to 'aarch64')
-rw-r--r-- | aarch64/Asmexpand.ml | 2 | ||||
-rw-r--r-- | aarch64/Machregs.v | 1 | ||||
-rw-r--r-- | aarch64/TargetPrinter.ml | 41 |
3 files changed, 43 insertions, 1 deletions
diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index 471ad501..b0787d0a 100644 --- a/aarch64/Asmexpand.ml +++ b/aarch64/Asmexpand.ml @@ -400,7 +400,7 @@ let expand_instruction instr = expand_annot_val kind txt targ args res | EF_memcpy(sz, al) -> expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args - | EF_annot _ | EF_debug _ | EF_inline_asm _ -> + | EF_annot _ | EF_debug _ | EF_inline_asm _ | EF_profiling _ -> emit instr | _ -> assert false diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v index b2a2308e..3d27f48f 100644 --- a/aarch64/Machregs.v +++ b/aarch64/Machregs.v @@ -158,6 +158,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_memcpy sz al => R15 :: R17 :: R29 :: nil | EF_inline_asm txt sg clob => destroyed_by_clobber clob + | EF_profiling _ _ => R15 :: R17 :: nil | _ => nil end. diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index e7edcf0d..8d74daf4 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -229,6 +229,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 ".Lcompcert_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 *) @@ -521,6 +543,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 @@ -577,7 +601,24 @@ 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 " 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_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_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; |