diff options
| -rw-r--r-- | arm/Asmexpand.ml | 2 | ||||
| -rw-r--r-- | arm/Constantexpand.ml | 1 | ||||
| -rw-r--r-- | arm/Machregs.v | 1 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 53 | ||||
| -rw-r--r-- | backend/PrintAsmaux.ml | 6 | ||||
| -rw-r--r-- | test/monniaux/minisat/Makefile.profiled | 3 |
6 files changed, 58 insertions, 8 deletions
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; diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index c7161615..cc7b33c3 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -358,11 +358,7 @@ let write_symbol_pointer oc sym = then fprintf oc " .8byte %s\n" sym else fprintf oc " .4byte %s\n" sym;; -let declare_function oc name = - fprintf oc " .type %s, @function\n" name; - fprintf oc " .size %s, . - %s\n" name name;; - -let print_profiling_epilogue finalizer_call_method print_profiling_stub oc = +let print_profiling_epilogue declare_function finalizer_call_method print_profiling_stub oc = let nr_items = !next_profiling_position in if nr_items > 0 then diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled index f411b5e7..fac3e3af 100644 --- a/test/monniaux/minisat/Makefile.profiled +++ b/test/monniaux/minisat/Makefile.profiled @@ -5,7 +5,8 @@ CCOMP=../../../ccomp GCC=aarch64-linux-gnu-gcc #GCC=k1-cos-gcc -EXECUTE=qemu-aarch64 +#EXECUTE=qemu-aarch64 +EXECUTE=qemu-arm #EXECUTE=k1-cluster -- EXECUTE_CYCLES=k1-cluster --cycle-based -- |