diff options
-rw-r--r-- | aarch64/Asmexpand.ml | 2 | ||||
-rw-r--r-- | aarch64/Machregs.v | 1 | ||||
-rw-r--r-- | aarch64/TargetPrinter.ml | 36 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 14 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 2 | ||||
-rw-r--r-- | test/monniaux/cycles.h | 14 | ||||
-rw-r--r-- | test/monniaux/minisat/Makefile.profiled | 16 | ||||
-rw-r--r-- | test/monniaux/minisat/solver.h | 5 | ||||
-rw-r--r-- | test/monniaux/profiling/profiling_call.c | 27 |
9 files changed, 105 insertions, 12 deletions
diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index 471ad501..b0787d0a 100644 --- a/aarch64/Asmexpand.ml +++ b/aarch64/Asmexpand.ml @@ -400,7 +400,7 @@ let expand_instruction instr = expand_annot_val kind txt targ args res | EF_memcpy(sz, al) -> expand_builtin_memcpy (Z.to_int sz) (Z.to_int 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/aarch64/Machregs.v b/aarch64/Machregs.v index b2a2308e..3d27f48f 100644 --- a/aarch64/Machregs.v +++ b/aarch64/Machregs.v @@ -158,6 +158,7 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_memcpy sz al => R15 :: R17 :: R29 :: nil | EF_inline_asm txt sg clob => destroyed_by_clobber clob + | EF_profiling _ _ => R15 :: R17 :: nil | _ => nil end. diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index e54673dd..bd26a45f 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -227,6 +227,28 @@ module Target : TARGET = | EOuxtw n -> fprintf oc ", uxtw #%a" coqint n | EOuxtx n -> fprintf oc ", uxtx #%a" coqint n + let next_profiling_label = + let atomic_incr_counter = ref 0 in + fun () -> + let r = sprintf ".compcert_atomic_incr%d" !atomic_incr_counter in + incr atomic_incr_counter; r;; + + let print_profiling_logger oc id kind = + assert (kind >= 0); + assert (kind <= 1); + fprintf oc "%s begin profiling %a %d: atomic increment\n" comment + Profilingaux.pp_id id kind; + let ofs = profiling_offset id kind and lbl = next_profiling_label () in + fprintf oc " adrp x15, %s+%d\n" profiling_counter_table_name ofs; + fprintf oc " add x15, x15, :lo12:(%s+%d)\n" profiling_counter_table_name ofs; + fprintf oc "%s:\n" lbl; + fprintf oc " ldaxr x17, [x15]\n"; + fprintf oc " add x17, x17, 1\n"; + fprintf oc " stlxr w17, x17, [x15]\n"; + fprintf oc " cbnz w17, %s\n" lbl; + fprintf oc "%s end profiling %a %d\n" comment + Profilingaux.pp_id id kind;; + (* Printing of instructions *) let print_instruction oc = function (* Branches *) @@ -519,6 +541,8 @@ module Target : 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 @@ -575,7 +599,19 @@ module Target : TARGET = section oc Section_text; end + let aarch64_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name = + fprintf oc " ret\n"; + fprintf oc " adrp x2, %s\n" profiling_counter_table_name; + fprintf oc " adrp x1, %s\n" profiling_id_table_name; + fprintf oc " add x2, x2, :lo12:%s\n" profiling_counter_table_name; + fprintf oc " add x1, x1, :lo12:%s\n" profiling_id_table_name; + fprintf oc " mov w0, %d\n" nr_items; + fprintf oc " b %s\n" profiling_write_table_helper ;; + let print_epilogue oc = + print_profiling fini_section aarch64_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 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;; diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index eae05c05..71979705 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -351,7 +351,7 @@ module Target (*: TARGET*) = fprintf oc " make $r62 = 1\n"; fprintf oc " ;;\n"; fprintf oc " afaddd %d[$r63] = $r62\n" - (((profiling_position id)*2 + kind)*8); + (profiling_offset id kind); fprintf oc " ;;\n" | _ -> assert false diff --git a/test/monniaux/cycles.h b/test/monniaux/cycles.h index c7dc582b..097d6882 100644 --- a/test/monniaux/cycles.h +++ b/test/monniaux/cycles.h @@ -50,6 +50,11 @@ static inline cycle_t get_cycle(void) { typedef uint32_t cycle_t; #define PRcycle PRId32 +#ifdef ARM_NOPRIVILEGE +static inline cycle_t get_cycle(void) { + return 0; +} +#else /* need this kernel module https://github.com/zertyz/MTL/tree/master/cpp/time/kernel/arm */ static inline cycle_t get_cycle(void) { @@ -57,14 +62,20 @@ static inline cycle_t get_cycle(void) { __asm__ volatile ("mrc p15, 0, %0, c9, c13, 0":"=r" (cycles)); return cycles; } +#endif #else #define PRcycle PRId64 typedef uint64_t cycle_t; + +#ifdef ARM_NOPRIVILEGE +static inline cycle_t get_cycle(void) { + return 0; +} +#else /* need this kernel module: https://github.com/jerinjacobk/armv8_pmu_cycle_counter_el0 on 5+ kernels, remove first argument of access_ok macro */ - static inline cycle_t get_cycle(void) { uint64_t val; @@ -72,6 +83,7 @@ static inline cycle_t get_cycle(void) return val; } #endif +#endif #else #define PRcycle PRId32 diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled index 840261b4..349089b7 100644 --- a/test/monniaux/minisat/Makefile.profiled +++ b/test/monniaux/minisat/Makefile.profiled @@ -1,28 +1,32 @@ +# -*- mode: makefile; -*- + CFILES=main.c solver.c clock.c GCDAFILES=$(CFILES:.c=.gcda) CCOMP=../../../ccomp -GCC=k1-cos-gcc +GCC=aarch64-linux-gnu-gcc # k1-cos-gcc LIBS=-lm PROFILING_DAT=compcert_profiling.dat -EXECUTE=k1-cluster -- +EXECUTE=qemu-aarch64 # k1-cluster -- EXECUTE_CYCLES=k1-cluster --cycle-based -- EXAMPLE=sudoku.sat -CCOMPFLAGS=-finline-auto-threshold 50 +CCOMPFLAGS=-finline-auto-threshold 50 -static -finline-asm +GCCFLAGS=-static ALL=minisat.ccomp.log minisat.ccomp.trace-linearize.log minisat.ccomp.profiled.log minisat.gcc-O3.log minisat.gcc-O3.profiled.log all: $(ALL) +exe: $(ALL:.log=.exe) minisat.ccomp.exe: $(CFILES) $(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@ $(LIBS) minisat.ccomp.profile-arcs.exe: $(CFILES) - $(CCOMP) $(CCOMPFLAGS) -fprofile-arcs $(CFILES) -o $@ $(LIBS) + $(CCOMP) -DAMD_NO_PRIVILEGE $(CCOMPFLAGS) -fprofile-arcs $(CFILES) -o $@ $(LIBS) minisat.gcc-O3.exe: $(CFILES) $(GCC) $(GCCFLAGS) -O3 $(CFILES) -o $@ $(LIBS) minisat.gcc-O3.profile-arcs.exe: $(CFILES) - $(GCC) $(GCCFLAGS) -fprofile-arcs -O3 $(CFILES) -o $@ $(LIBS) + $(GCC) -DAMD_NO_PRIVILEGE $(GCCFLAGS) -fprofile-arcs -O3 $(CFILES) -o $@ $(LIBS) gcda: minisat.gcc-O3.profile-arcs.exe $(EXECUTE) $< $(EXAMPLE) @@ -48,6 +52,6 @@ minisat.ccomp.profiled.exe: $(CFILES) $(PROFILING_DAT) clean: -rm -f *.log *.exe $(PROFILING_DAT) $(GCDAFILES) -.PHONY: clean gcda +.PHONY: clean gcda exe all .SECONDARY: diff --git a/test/monniaux/minisat/solver.h b/test/monniaux/minisat/solver.h index c9ce0219..4b96b017 100644 --- a/test/monniaux/minisat/solver.h +++ b/test/monniaux/minisat/solver.h @@ -19,6 +19,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA **************************************************************************************************/ // Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko +#include <stdint.h> + #ifndef solver_h #define solver_h @@ -39,11 +41,14 @@ static const bool false = 0; typedef int lit; typedef char lbool; +#if 0 #ifdef _WIN32 typedef signed __int64 uint64; // compatible with MS VS 6.0 #else typedef unsigned long long uint64; #endif +#endif +typedef uint64_t uint64; static const int var_Undef = -1; static const lit lit_Undef = -2; diff --git a/test/monniaux/profiling/profiling_call.c b/test/monniaux/profiling/profiling_call.c new file mode 100644 index 00000000..ce20241d --- /dev/null +++ b/test/monniaux/profiling/profiling_call.c @@ -0,0 +1,27 @@ +/* +For knowing how to write assembly profiling stubs. + */ + +#include <stdint.h> +#include <stdio.h> +#include <errno.h> + +typedef uint8_t md5_hash[16]; +typedef uint64_t condition_counters[2]; + +void _compcert_write_profiling_table(unsigned int nr_items, + md5_hash id_table[], + condition_counters counter_table[]); + +static md5_hash id_table[42] = {{1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16}}; +static condition_counters counter_table[42]; + +void write_profile(void) { + _compcert_write_profiling_table(42, id_table, counter_table); +} + +static _Atomic uint64_t counter; + +void incr_counter(void) { + counter++; +} |