various fixes for aarch64 profiling

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++;
+}