From 3d0204fddb71ca377fa65952ede872583c8a7242 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 10 Apr 2020 14:06:41 +0200
Subject: various fixes for aarch64 profiling

---
 test/monniaux/cycles.h                   | 14 +++++++++++++-
 test/monniaux/minisat/Makefile.profiled  | 16 ++++++++++------
 test/monniaux/minisat/solver.h           |  5 +++++
 test/monniaux/profiling/profiling_call.c | 27 +++++++++++++++++++++++++++
 4 files changed, 55 insertions(+), 7 deletions(-)
 create mode 100644 test/monniaux/profiling/profiling_call.c

(limited to 'test')

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