Merge branch 'mppa-work' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work

17 files changed, 199 insertions, 22 deletions

diff --git a/test/monniaux/cse2/noloopinvariant.c b/test/monniaux/cse2/noloopinvariant.c
new file mode 100644
index 00000000..5c7789bf
--- /dev/null
+++ b/test/monniaux/cse2/noloopinvariant.c
@@ -0,0 +1,6 @@
+int toto(int *t, int n) {
+  for(int i=1; i<n; i++) {
+    if (t[i] > t[0]) return i;
+  }
+  return 0;
+}
diff --git a/test/monniaux/cse2/storeload.c b/test/monniaux/cse2/storeload.c
new file mode 100644
index 00000000..028fb835
--- /dev/null
+++ b/test/monniaux/cse2/storeload.c
@@ -0,0 +1,5 @@
+int toto(int *p, int x) {
+  p[0] = x;
+  p[1] = 3;
+  return *p;
+}
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/division/sum_div.c b/test/monniaux/division/sum_div.c
deleted file mode 100644
index 87256922..00000000
--- a/test/monniaux/division/sum_div.c
+++ /dev/null
@@ -1,18 +0,0 @@
-#include <stdio.h>
-#include <stdlib.h>
-#include "../clock.h"
- 
-int main(int argc, char **argv) {
-  unsigned modulus = argc < 2 ? 3371 : atoi(argv[1]);
-  clock_prepare();
-  clock_start();
-  unsigned total=0, total_mod=0;
-  for(int i=0; i<1000; i++) {
-    total += i;
-    total_mod = (total_mod + i)%modulus;
-  }
-  clock_stop();
-  print_total_clock();
-  printf("%u %u %d\n", total, total_mod, total%modulus == total_mod);
-  return 0;
-}
diff --git a/test/monniaux/expect/expect.c b/test/monniaux/expect/expect.c
new file mode 100644
index 00000000..30e0742a
--- /dev/null
+++ b/test/monniaux/expect/expect.c
@@ -0,0 +1,7 @@
+#ifndef PREDICTED
+#define PREDICTED 0
+#endif
+
+int expect(int x, int *y, int *z) {
+  return __builtin_expect(x, PREDICTED) ? *y : *z;
+}
diff --git a/test/monniaux/licm/addv.c b/test/monniaux/licm/addv.c
new file mode 100644
index 00000000..bb0098d0
--- /dev/null
+++ b/test/monniaux/licm/addv.c
@@ -0,0 +1,6 @@
+void addv(double x, double y, int n, int *z)
+{
+  for(int i=0; i<n; i++) {
+    z[i] += (int) (x*y);
+  }
+}
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++;
+}
diff --git a/test/monniaux/thread_local/thread_local.c b/test/monniaux/thread_local/thread_local.c
new file mode 100644
index 00000000..7a50db0a
--- /dev/null
+++ b/test/monniaux/thread_local/thread_local.c
@@ -0,0 +1,13 @@
+#include <stdio.h>
+
+_Thread_local int toto;
+_Thread_local int toto2 = 45;
+
+int foobar(void) {
+  return toto;
+}
+
+int main() {
+  printf("%d %d\n", toto, toto2);
+  return 0;
+}
diff --git a/test/monniaux/thread_local/thread_local2.c b/test/monniaux/thread_local/thread_local2.c
new file mode 100644
index 00000000..ba244ac6
--- /dev/null
+++ b/test/monniaux/thread_local/thread_local2.c
@@ -0,0 +1,18 @@
+#include <stdio.h>
+#include <pthread.h>
+
+_Thread_local int toto;
+_Thread_local int toto2 = 45;
+
+void* poulet(void * dummy) {
+  printf("%p %p\n", &toto, &toto2);
+  return NULL;
+}
+
+int main() {
+  pthread_t thr;
+  poulet(NULL);
+  pthread_create(&thr, NULL, poulet, NULL);
+  pthread_join(thr, NULL);
+  return 0;
+}
diff --git a/test/mppa/hardcheck.sh b/test/mppa/hardcheck.sh
index 82b63182..b6538f0e 100755
--- a/test/mppa/hardcheck.sh
+++ b/test/mppa/hardcheck.sh
@@ -3,4 +3,4 @@
 
 source do_test.sh
 
-do_test hardcheck
+do_test hardcheck 1
diff --git a/test/mppa/hardtest.sh b/test/mppa/hardtest.sh
index 09511da6..6321bc7d 100755
--- a/test/mppa/hardtest.sh
+++ b/test/mppa/hardtest.sh
@@ -3,4 +3,4 @@
 
 source do_test.sh
 
-do_test hardtest
+do_test hardtest 1