From f50a1c1e1dc194c78b68ecdc7e3f6c0b0448f5f4 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 11 Apr 2020 10:29:45 +0200 Subject: seems like the ARM profiling perhaps works --- arm/Asmexpand.ml | 2 +- arm/Constantexpand.ml | 1 + arm/Machregs.v | 1 + arm/TargetPrinter.ml | 53 ++++++++++++++++++++++++++++++++++++++++++++++++++- 4 files changed, 55 insertions(+), 2 deletions(-) (limited to 'arm') diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 89aab5c7..6996c9bb 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -619,7 +619,7 @@ let expand_instruction instr = | EF_memcpy(sz, al) -> expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz)) (Int32.to_int (camlint_of_coqint 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/arm/Constantexpand.ml b/arm/Constantexpand.ml index 408b291e..8cc32c1f 100644 --- a/arm/Constantexpand.ml +++ b/arm/Constantexpand.ml @@ -106,6 +106,7 @@ let estimate_size = function | Pbuiltin (ef,_,_) -> begin match ef with | EF_inline_asm _ -> 256 + | EF_profiling _ -> 40 | _ -> 0 end | Pcfi_adjust _ | Pcfi_rel_offset _ diff --git a/arm/Machregs.v b/arm/Machregs.v index ae0ff6bf..1ec8f0a1 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -153,6 +153,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_memcpy sz al => R2 :: R3 :: R12 :: F7 :: nil | EF_inline_asm txt sg clob => destroyed_by_clobber clob + | EF_profiling _ _ => R2 :: R3 :: R12 :: nil | _ => nil end. diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 03e06a65..2499dd31 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -202,6 +202,38 @@ struct | SOasr(r, n) -> fprintf oc "%a, asr #%a" ireg r coqint n | SOror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n + + let next_profiling_label = + let profiling_label_counter = ref 0 in + fun () -> + let r = sprintf ".Lprofiling_label%d" !profiling_label_counter in + incr profiling_label_counter; r;; + + let print_profiling_logger oc id kind = + assert (kind >= 0); + assert (kind <= 1); + let ofs = profiling_offset id kind and olbl = next_profiling_label () in + fprintf oc "%s begin profiling %a %d: non-atomic increment\n" comment + Profilingaux.pp_id id kind; + fprintf oc " ldr r2, %s\n" olbl; + fprintf oc " ldr r3, [r2, #%d]\n" + (if Configuration.is_big_endian then 8 else 0); + fprintf oc " ldr r12, [r2, #%d]\n" + (if Configuration.is_big_endian then 0 else 8); + fprintf oc " adds r3, r3, #1\n"; + fprintf oc " adc r12, r12, #0\n"; + fprintf oc " str r3, [r2, #%d]\n" + (if Configuration.is_big_endian then 8 else 0); + fprintf oc " str r12, [r2, #%d]\n" + (if Configuration.is_big_endian then 0 else 8); + let jlbl = next_profiling_label () in + fprintf oc " b %s\n" jlbl; + fprintf oc "%s:\n" olbl; + fprintf oc " .word %s + %d\n" profiling_counter_table_name ofs; + fprintf oc "%s:\n" jlbl; + fprintf oc "%s end profiling %a %d\n" comment + Profilingaux.pp_id id kind;; + let print_instruction oc = function (* Core instructions *) | Padc (r1,r2,so) -> @@ -482,6 +514,7 @@ struct 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 @@ -549,6 +582,11 @@ struct if !Clflags.option_mthumb then fprintf oc " .thumb_func\n" + + let text_print_fun_info oc name = + fprintf oc " .type %s, %%function\n" name; + fprintf oc " .size %s, . - %s\n" name name + let print_fun_info oc name = fprintf oc " .type %a, %%function\n" symbol name; fprintf oc " .size %a, . - %a\n" symbol name symbol name @@ -596,9 +634,22 @@ struct if !Clflags.option_g then begin section oc Section_text; cfi_section oc - end + end + + let arm_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name = + fprintf oc " ldr r2, = %s\n" profiling_counter_table_name; + fprintf oc " ldr r1, = %s\n" profiling_id_table_name; + fprintf oc " mov r0, #%d\n" nr_items; + fprintf oc " b %s\n" profiling_write_table_helper;; + + let print_atexit oc to_be_called = + fprintf oc " ldr r0, = %s\n" to_be_called; + fprintf oc " b atexit\n";; let print_epilogue oc = + print_profiling_epilogue text_print_fun_info (Init_atexit print_atexit) arm_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