From 40cd35c9152ceba673e255ee1d6108e224a54c3f Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 12 Apr 2020 08:09:23 +0200 Subject: x86-64 profiling --- x86/Asmexpand.ml | 2 +- x86/TargetPrinter.ml | 63 +++++++++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 61 insertions(+), 4 deletions(-) (limited to 'x86') 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 6159437e..3ffad3d0 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -165,7 +165,42 @@ 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" + 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" + 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 @@ -395,8 +430,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: @@ -834,6 +889,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 -- cgit From 8bbb1bbaad236901afea1cbb7033dcc097e7b94e Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 12 Apr 2020 08:30:14 +0200 Subject: fix IA32 profiling bug --- x86/TargetPrinter.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'x86') diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index 3ffad3d0..b690c817 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -176,7 +176,8 @@ module ELF_System : SYSTEM = begin fprintf oc " pushl $%s\n" to_be_called; fprintf oc " call atexit\n"; - fprintf oc " addl $4, %%esp\n" + fprintf oc " addl $4, %%esp\n"; + fprintf oc " ret\n" end let x86_profiling_stub oc nr_items @@ -196,7 +197,8 @@ module ELF_System : SYSTEM = 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 " addl $12, %%esp\n"; + fprintf oc " ret\n" end;; let print_epilogue oc = -- cgit