diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-10 14:06:41 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-10 14:06:41 +0200 |
| commit | 3d0204fddb71ca377fa65952ede872583c8a7242 (patch) | |
| tree | 4563132cbe6e9d103ea6e2178f7b9ecaae4c0246 /backend/PrintAsmaux.ml | |
| parent | be92a8c71192e014caf292312865dee32ee1b901 (diff) | |
| download | compcert-kvx-3d0204fddb71ca377fa65952ede872583c8a7242.tar.gz compcert-kvx-3d0204fddb71ca377fa65952ede872583c8a7242.zip | |
various fixes for aarch64 profiling
Diffstat (limited to 'backend/PrintAsmaux.ml')
| -rw-r--r-- | backend/PrintAsmaux.ml | 14 |
1 files changed, 11 insertions, 3 deletions
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;; |