Merge remote-tracking branch 'origin/mppa-profiling' into mppa-features

8 files changed, 142 insertions, 2 deletions

diff --git a/test/monniaux/cycles.h b/test/monniaux/cycles.h
index c7dc582b..5011b18c 100644
--- a/test/monniaux/cycles.h
+++ b/test/monniaux/cycles.h
@@ -45,11 +45,16 @@ static inline cycle_t get_cycle(void) {
   return cycles;
 }
 
-#elif defined (__ARM_ARCH) && (__ARM_ARCH >= 6)
+#elif defined (__ARM_ARCH) // && (__ARM_ARCH >= 6)
 #if (__ARM_ARCH < 8)
 typedef uint32_t cycle_t;
 #define PRcycle PRId32
 
+#ifdef ARM_NO_PRIVILEGE
+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_NO_PRIVILEGE
+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.on_marte b/test/monniaux/minisat/Makefile.on_marte
new file mode 100644
index 00000000..af7b9145
--- /dev/null
+++ b/test/monniaux/minisat/Makefile.on_marte
@@ -0,0 +1,16 @@
+EXE=minisat.ccomp.exe minisat.ccomp.trace-linearize.exe \
+  minisat.gcc-O3.exe \
+  minisat.ccomp.profiled.exe      minisat.gcc-O3.profiled.exe
+
+LOG=$(EXE:.exe=.dat)
+
+all: $(LOG)
+
+%.log : %.exe
+	rm -f $@
+	for i in `seq 1 1000` ; do ./$< sudoku.sat >> $@; done
+
+%.dat : %.log
+	grep 'time cycles: ' $< | sed -e 's/time cycles: //' | awk '{ total += $$1; count++ } END { print total/count }' > $@
+
+.SECONDARY:
diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled
new file mode 100644
index 00000000..77ba8b43
--- /dev/null
+++ b/test/monniaux/minisat/Makefile.profiled
@@ -0,0 +1,64 @@
+# -*- mode: makefile; -*-
+
+CFILES=main.c solver.c clock.c
+CCOMP=../../../ccomp
+
+#GCC=aarch64-linux-gnu-gcc
+GCC=k1-cos-gcc
+#EXECUTE=qemu-aarch64
+#EXECUTE=qemu-arm
+#EXECUTE=k1-cluster --
+#EXECUTE_CYCLES=k1-cluster --cycle-based --
+
+LIBS=-lm
+PROFILING_DAT=compcert_profiling.dat
+EXAMPLE=sudoku.sat
+CCOMPFLAGS=-static -finline-asm -finline-auto-threshold 50 
+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) -DARM_NO_PRIVILEGE $(CCOMPFLAGS) -fprofile-arcs $(CFILES) -o $@ $(LIBS)
+
+minisat.gcc-O3.exe: $(CFILES)
+	$(GCC) $(GCCFLAGS) -O3 $(CFILES) -o $@ $(LIBS)
+
+clock.gcc-O3.noprofile.o : clock.c
+	$(GCC) -DARM_NO_PRIVILEGE $(GCCFLAGS) -O3 -c $< -o @
+
+minisat.gcc-O3.profile-arcs.exe: main.c solver.c clock.gcc-O3.noprofile.o
+	$(GCC) -DARM_NO_PRIVILEGE $(GCCFLAGS) -fprofile-arcs -O3 $+ -o $@ $(LIBS)
+
+gcda: minisat.gcc-O3.profile-arcs.exe
+	$(EXECUTE) ./$< $(EXAMPLE)
+
+main.gcda solver.gcda: gcda
+
+minisat.gcc-O3.profiled.exe: $(CFILES) $(GCDAFILES)
+	$(GCC) $(GCCFLAGS) -O3 -fprofile-use $(CFILES) -o $@ $(LIBS)
+
+minisat.ccomp.trace-linearize.exe: $(CFILES)
+	$(CCOMP) $(CCOMPFLAGS) -fduplicate 0 -ftracelinearize $(CFILES) -o $@ $(LIBS)
+
+$(PROFILING_DAT): minisat.ccomp.profile-arcs.exe
+	-rm -f $(PROFILING_DAT)
+	$(EXECUTE) ./$< $(EXAMPLE)
+
+minisat.ccomp.profiled.exe: $(CFILES) $(PROFILING_DAT)
+	$(CCOMP) $(CCOMPFLAGS) -fprofile-use= $(PROFILING_DAT) -ftracelinearize $(CFILES) -o $@ $(LIBS)
+
+%.log : %.exe
+	$(EXECUTE_CYCLES) $< $(EXAMPLE) 2>&1 | tee $@
+
+clean:
+	-rm -f *.log *.exe $(PROFILING_DAT) $(GCDAFILES)
+
+.PHONY: clean gcda exe all
+
+.SECONDARY:
diff --git a/test/monniaux/minisat/clock.c b/test/monniaux/minisat/clock.c
new file mode 120000
index 00000000..d6bade99
--- /dev/null
+++ b/test/monniaux/minisat/clock.c
@@ -0,0 +1 @@
+../clock.c
\ No newline at end of file
diff --git a/test/monniaux/minisat/cycles.h b/test/monniaux/minisat/cycles.h
new file mode 120000
index 00000000..84e54d21
--- /dev/null
+++ b/test/monniaux/minisat/cycles.h
@@ -0,0 +1 @@
+../cycles.h
\ No newline at end of file
diff --git a/test/monniaux/minisat/k1c.inline_50.log b/test/monniaux/minisat/k1c.inline_50.log
new file mode 100644
index 00000000..438a06b4
--- /dev/null
+++ b/test/monniaux/minisat/k1c.inline_50.log
@@ -0,0 +1,14 @@
+==> minisat.ccomp.log <==
+time cycles: 3252345
+
+==> minisat.ccomp.profiled.log <==
+time cycles: 3150170
+
+==> minisat.ccomp.trace-linearize.log <==
+time cycles: 3192299
+
+==> minisat.gcc-O3.log <==
+time cycles: 2780324
+
+==> minisat.gcc-O3.profiled.log <==
+time cycles: 2487533
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++;
+}