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 /x86 | |
| 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 'x86')
| -rw-r--r-- | x86/Asmexpand.ml | 2 | ||||
| -rw-r--r-- | x86/TargetPrinter.ml | 65 |
2 files changed, 63 insertions, 4 deletions
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index b8353046..ad667e3d 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -552,7 +552,7 @@ let expand_instruction instr = expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args | EF_annot_val(kind,txt, targ) -> expand_annot_val kind txt targ args res - | EF_annot _ | EF_debug _ | EF_inline_asm _ -> + | EF_annot _ | EF_debug _ | EF_inline_asm _ | EF_profiling _ -> emit instr | _ -> assert false diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index e371380c..38eff731 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -167,7 +167,44 @@ module ELF_System : SYSTEM = let print_var_info = elf_print_var_info - let print_epilogue _ = () + let print_atexit oc to_be_called = + if Archi.ptr64 + then + begin + fprintf oc " leaq %s(%%rip), %%rdi\n" to_be_called; + fprintf oc " jmp atexit\n" + end + else + begin + fprintf oc " pushl $%s\n" to_be_called; + fprintf oc " call atexit\n"; + fprintf oc " addl $4, %%esp\n"; + fprintf oc " ret\n" + end + + let x86_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name = + if Archi.ptr64 + then + begin + fprintf oc " leaq %s(%%rip), %%rdx\n" profiling_counter_table_name; + fprintf oc " leaq %s(%%rip), %%rsi\n" profiling_id_table_name; + fprintf oc " movl $%d, %%edi\n" nr_items; + fprintf oc " jmp %s\n" profiling_write_table_helper + end + else + begin + fprintf oc " pushl $%s\n" profiling_counter_table_name; + fprintf oc " pushl $%s\n" profiling_id_table_name; + fprintf oc " pushl $%d\n" nr_items; + fprintf oc " call %s\n" profiling_write_table_helper ; + fprintf oc " addl $12, %%esp\n"; + fprintf oc " ret\n" + end;; + + let print_epilogue oc = + print_profiling_epilogue elf_text_print_fun_info (Init_atexit print_atexit) x86_profiling_stub oc;; let print_comm_decl oc name sz al = fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al @@ -401,8 +438,28 @@ module Target(System: SYSTEM):TARGET = fprintf oc "%a(%%rip)" label lbl end - - + let print_profiling_logger oc id kind = + assert (kind >= 0); + assert (kind <= 1); + let ofs = profiling_offset id kind in + if Archi.ptr64 + then + begin + fprintf oc "%s profiling %a %d: atomic increment\n" comment + Profilingaux.pp_id id kind; + fprintf oc " lock addq $1, %s+%d(%%rip)\n" + profiling_counter_table_name ofs + end + else + begin + fprintf oc "%s begin profiling %a %d: increment\n" comment + Profilingaux.pp_id id kind; + fprintf oc " addl $1, %s+%d\n" profiling_counter_table_name ofs; + fprintf oc " adcl $1, %s+%d\n" profiling_counter_table_name (ofs+4); + fprintf oc "%s end profiling %a %d: increment\n" comment + Profilingaux.pp_id id kind; + end + (* Printing of instructions *) (* Reminder on X86 assembly syntaxes: @@ -840,6 +897,8 @@ module Target(System: SYSTEM):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 |