Merge branch 'kvx-work' into kvx-work-merge3.8

Conflicts:
	Makefile
	configure

11 files changed, 380 insertions, 13 deletions

diff --git a/test/c/Makefile b/test/c/Makefile
index 726631d2..a728d182 100644
--- a/test/c/Makefile
+++ b/test/c/Makefile
@@ -1,6 +1,8 @@
 include ../../Makefile.config
 
 CCOMP=../../ccomp
+# TODO - temporary
+# CCOMPOPTS:=$(CCOMPOPTS) -fall-loads-nontrap -fduplicate 2 -fprepass
 CCOMPFLAGS=$(CCOMPOPTS) -stdlib ../../runtime -dc -dclight -dasm
 
 CFLAGS+=-O2 -Wall
diff --git a/test/monniaux/picosat-965/onefile/picosat.c b/test/monniaux/picosat-965/onefile/picosat.c
new file mode 100644
index 00000000..e1c18438
--- /dev/null
+++ b/test/monniaux/picosat-965/onefile/picosat.c
@@ -0,0 +1,25 @@
+typedef struct b b;
+b *a;
+struct b {
+  int c;
+  int d, **clshead;
+  int **ahead;
+  unsigned h;
+} i;
+b *j();
+int k();
+int main() {
+  a = j();
+  k(a);
+}
+#define e(f) f - g->c
+static void m(b *g, int *l) {
+  if (g)
+    *g->ahead = l;
+}
+b *j() { return &i; }
+int k(b *g) {
+  if (g->d)
+    m(g, e(g->clshead[-1]));
+  return g->h;
+}
diff --git a/test/monniaux/picosat-965/onefile/testcmp.sh b/test/monniaux/picosat-965/onefile/testcmp.sh
new file mode 100755
index 00000000..2228c675
--- /dev/null
+++ b/test/monniaux/picosat-965/onefile/testcmp.sh
@@ -0,0 +1,146 @@
+DEFINES="-DNALARM -DNZIP -DNGETRUSAGE -DNDEBUG"
+COMPCERT=/local/monniaux/Kalray/mppa-RTLpathSE-verif-hash-junk
+DATA=$COMPCERT/test/monniaux/picosat-965/tiny.dat
+CCOMP="$COMPCERT/ccomp -fbitfields -fduplicate 2 -fall-loads-nontrap $DEFINES"
+GCC="kvx-cos-gcc -O -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES"
+HOSTCC0="gcc -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES"
+HOSTCC1="gcc -O -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES"
+HOSTCC2="gcc -O -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror -fsanitize=undefined -fsanitize=address $DEFINES"
+HOSTCC3="gcc -O3 -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES"
+HOSTCC4="clang -Wimplicit -Wuninitialized -Werror $DEFINES"
+HOSTCC5="clang -Wimplicit -Wuninitialized -Werror -fsanitize=undefined -fsanitize=address $DEFINES"
+CFILES="picosat.c"
+SIMU="kvx-cluster --timeout=100000 -- "
+
+if ! $HOSTCC0 $CFILES -o picosat.cc0.host ;
+then exit 30 ;
+fi
+
+if ! $HOSTCC1 $CFILES -o picosat.cc1.host ;
+then exit 31 ;
+fi
+
+if ! $HOSTCC2 $CFILES -o picosat.cc2.host ;
+then exit 32 ;
+fi
+
+if ! $HOSTCC3 $CFILES -o picosat.cc3.host ;
+then exit 33 ;
+fi
+
+if ! $HOSTCC4 $CFILES -o picosat.cc4.host ;
+then exit 34 ;
+fi
+
+if ! $HOSTCC5 $CFILES -o picosat.cc5.host ;
+then exit 35 ;
+fi
+
+timeout 1 ./picosat.cc0.host $DATA 2>&1 > picosat.cc0.out
+if [ $? -ge 100 ];
+then exit 40 ;
+fi
+
+timeout 1 ./picosat.cc1.host $DATA 2>&1 > picosat.cc1.out
+if [ $? -ge 100 ];
+then exit 41 ;
+fi
+
+timeout 1 valgrind --log-file=picosat.cc0.valgrind.log ./picosat.cc0.host $DATA 2>&1 > picosat.cc0.valgrind.out
+if [ $? -ge 100 ];
+then exit 50 ;
+fi
+
+timeout 1 valgrind --log-file=picosat.cc1.valgrind.log ./picosat.cc1.host $DATA 2>&1 > picosat.cc1.valgrind.out
+if [ $? -ge 100 ];
+then exit 51 ;
+fi
+
+timeout 1 ./picosat.cc2.host $DATA 2>&1 > picosat.cc2.out
+if [ $? -ge 100 ];
+then exit 42 ;
+fi
+
+timeout 1 ./picosat.cc3.host $DATA 2>&1 > picosat.cc3.out
+if [ $? -ge 100 ];
+then exit 43 ;
+fi
+
+timeout 1 ./picosat.cc4.host $DATA 2>&1 > picosat.cc4.out
+if [ $? -ge 100 ];
+then exit 44 ;
+fi
+
+timeout 1 ./picosat.cc5.host $DATA 2>&1 > picosat.cc5.out
+if [ $? -ge 100 ];
+then exit 45 ;
+fi
+
+if ! cmp picosat.cc0.out picosat.cc1.out ;
+then exit 60 ;
+fi
+
+if ! cmp picosat.cc0.out picosat.cc0.valgrind.out ;
+then exit 70 ;
+fi
+
+if ! cmp picosat.cc1.out picosat.cc1.valgrind.out ;
+then exit 61 ;
+fi
+
+if ! cmp picosat.cc1.out picosat.cc2.out ;
+then exit 62 ;
+fi
+
+if ! cmp picosat.cc1.out picosat.cc3.out ;
+then exit 63 ;
+fi
+
+if ! $GCC $CFILES -o picosat.gcc.target ;
+then exit 1 ;
+fi
+
+if ! $CCOMP $CFILES -o picosat.ccomp.target ;
+then exit 2 ;
+fi
+
+if ! $CCOMP -fprepass -fprepass= list $CFILES -o picosat.prepass.target ;
+then exit 3 ;
+fi
+
+$SIMU ./picosat.gcc.target $DATA 2>&1 > picosat.gcc.out
+if [ $? -ge 100 ];
+then exit 4 ;
+fi
+
+if ! cmp picosat.gcc.out picosat.cc1.out ;
+then exit 13 ;
+fi
+
+if grep timeout picosat.gcc.out ;
+then exit 8 ;
+fi
+
+$SIMU ./picosat.ccomp.target $DATA 2>&1 > picosat.ccomp.out
+if [ $? -ge 100 ];
+then exit 5 ;
+fi
+
+if grep timeout picosat.ccomp.out ;
+then exit 9 ;
+fi
+
+if ! cmp picosat.gcc.out picosat.ccomp.out ;
+then exit 6 ;
+fi
+
+$SIMU ./picosat.prepass.target $DATA 2>&1 > picosat.prepass.out
+if [ $? -ge 100 ];
+then exit 0 ;
+fi
+
+if cmp picosat.gcc.out picosat.prepass.out ;
+then exit 7 ;
+fi
+
+exit 0
diff --git a/test/monniaux/picosat-965/small.dat b/test/monniaux/picosat-965/small.dat
new file mode 100644
index 00000000..accb9054
--- /dev/null
+++ b/test/monniaux/picosat-965/small.dat
@@ -0,0 +1,2 @@
+p cnf 1 1
+1 0
diff --git a/test/monniaux/picosat-965/tiny.dat b/test/monniaux/picosat-965/tiny.dat
new file mode 100644
index 00000000..1d89b303
--- /dev/null
+++ b/test/monniaux/picosat-965/tiny.dat
@@ -0,0 +1,2 @@
+p cnf 0 1
+0
diff --git a/test/monniaux/reduced_picosat/reduced_picosat.c b/test/monniaux/reduced_picosat/reduced_picosat.c
new file mode 100644
index 00000000..eb9fdaf8
--- /dev/null
+++ b/test/monniaux/reduced_picosat/reduced_picosat.c
@@ -0,0 +1,23 @@
+typedef struct b b;
+b *a;
+struct b {
+  int c;
+  int d, **clshead;
+  int **ahead;
+  unsigned h;
+} glob;
+int k();
+int main() {
+  a = &glob;
+  k(a);
+}
+#define e(f) f - g->c
+static void m(b *g, int *l) {
+  if (g)
+    *g->ahead = l;
+}
+int k(b *g) {
+  if (g->d)
+    m(g, e(g->clshead[-1]));
+  return g->h;
+}
diff --git a/test/monniaux/reduced_picosat/test_a.s b/test/monniaux/reduced_picosat/test_a.s
new file mode 100644
index 00000000..c14cc8f9
--- /dev/null
+++ b/test/monniaux/reduced_picosat/test_a.s
@@ -0,0 +1,10 @@
+	.text
+	.global	dummyload
+	.type	dummyload, @function
+dummyload:
+	make	$r0 = 0
+	;;
+	ld.s	$r0 = -8[$r0]
+	ret
+	;;
+	.size	dummyload, .-dummyload
diff --git a/test/monniaux/reduced_picosat/test_b.c b/test/monniaux/reduced_picosat/test_b.c
new file mode 100644
index 00000000..a0fe625b
--- /dev/null
+++ b/test/monniaux/reduced_picosat/test_b.c
@@ -0,0 +1,9 @@
+#include <stdio.h>
+#include <stdint.h>
+#include <inttypes.h>
+
+extern uint64_t dummyload(void);
+
+int main() {
+  printf("%" PRIu64 "\n", dummyload());
+}
diff --git a/test/monniaux/reduced_picosat/testcmp.sh b/test/monniaux/reduced_picosat/testcmp.sh
new file mode 100755
index 00000000..8dc93de9
--- /dev/null
+++ b/test/monniaux/reduced_picosat/testcmp.sh
@@ -0,0 +1,146 @@
+DEFINES="-DNALARM -DNZIP -DNGETRUSAGE -DNDEBUG"
+COMPCERT=/home/monniaux/work/Kalray/mppa-RTLpathSE-verif-hash-junk
+DATA=$COMPCERT/test/monniaux/picosat-965/tiny.dat
+CCOMP="$COMPCERT/ccomp -fbitfields -fduplicate 2 -fall-loads-nontrap $DEFINES"
+GCC="kvx-cos-gcc -O -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES"
+HOSTCC0="gcc -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES"
+HOSTCC1="gcc -O -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES"
+HOSTCC2="gcc -O -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror -fsanitize=undefined -fsanitize=address $DEFINES"
+HOSTCC3="gcc -O3 -Wimplicit -Wuninitialized -Wmaybe-uninitialized -Werror $DEFINES"
+HOSTCC4="/usr/bin/clang -Wimplicit -Wuninitialized -Werror $DEFINES"
+HOSTCC5="/usr/bin/clang -Wimplicit -Wuninitialized -Werror -fsanitize=undefined -fsanitize=address $DEFINES"
+CFILES="reduced_picosat.c"
+SIMU="kvx-cluster --timeout=10000000 -- "
+
+if ! $HOSTCC0 $CFILES -o picosat.cc0.host ;
+then exit 30 ;
+fi
+
+if ! $HOSTCC1 $CFILES -o picosat.cc1.host ;
+then exit 31 ;
+fi
+
+if ! $HOSTCC2 $CFILES -o picosat.cc2.host ;
+then exit 32 ;
+fi
+
+if ! $HOSTCC3 $CFILES -o picosat.cc3.host ;
+then exit 33 ;
+fi
+
+if ! $HOSTCC4 $CFILES -o picosat.cc4.host ;
+then exit 34 ;
+fi
+
+if ! $HOSTCC5 $CFILES -o picosat.cc5.host ;
+then exit 35 ;
+fi
+
+timeout 1 ./picosat.cc0.host $DATA 2>&1 > picosat.cc0.out
+if [ $? -ge 100 ];
+then exit 40 ;
+fi
+
+timeout 1 ./picosat.cc1.host $DATA 2>&1 > picosat.cc1.out
+if [ $? -ge 100 ];
+then exit 41 ;
+fi
+
+timeout 1 valgrind --log-file=picosat.cc0.valgrind.log ./picosat.cc0.host $DATA 2>&1 > picosat.cc0.valgrind.out
+if [ $? -ge 100 ];
+then exit 50 ;
+fi
+
+timeout 1 valgrind --log-file=picosat.cc1.valgrind.log ./picosat.cc1.host $DATA 2>&1 > picosat.cc1.valgrind.out
+if [ $? -ge 100 ];
+then exit 51 ;
+fi
+
+timeout 1 ./picosat.cc2.host $DATA 2>&1 > picosat.cc2.out
+if [ $? -ge 100 ];
+then exit 42 ;
+fi
+
+timeout 1 ./picosat.cc3.host $DATA 2>&1 > picosat.cc3.out
+if [ $? -ge 100 ];
+then exit 43 ;
+fi
+
+timeout 1 ./picosat.cc4.host $DATA 2>&1 > picosat.cc4.out
+if [ $? -ge 100 ];
+then exit 44 ;
+fi
+
+timeout 1 ./picosat.cc5.host $DATA 2>&1 > picosat.cc5.out
+if [ $? -ge 100 ];
+then exit 45 ;
+fi
+
+if ! cmp picosat.cc0.out picosat.cc1.out ;
+then exit 60 ;
+fi
+
+if ! cmp picosat.cc0.out picosat.cc0.valgrind.out ;
+then exit 70 ;
+fi
+
+if ! cmp picosat.cc1.out picosat.cc1.valgrind.out ;
+then exit 61 ;
+fi
+
+if ! cmp picosat.cc1.out picosat.cc2.out ;
+then exit 62 ;
+fi
+
+if ! cmp picosat.cc1.out picosat.cc3.out ;
+then exit 63 ;
+fi
+
+if ! $GCC $CFILES -o picosat.gcc.target ;
+then exit 1 ;
+fi
+
+if ! $CCOMP $CFILES -o picosat.ccomp.target ;
+then exit 2 ;
+fi
+
+if ! $CCOMP -fprepass -fprepass= list $CFILES -o picosat.prepass.target ;
+then exit 3 ;
+fi
+
+$SIMU ./picosat.gcc.target $DATA 2>&1 > picosat.gcc.out
+if [ $? -ge 100 ];
+then exit 4 ;
+fi
+
+if ! cmp picosat.gcc.out picosat.cc1.out ;
+then exit 13 ;
+fi
+
+if grep timeout picosat.gcc.out ;
+then exit 8 ;
+fi
+
+$SIMU ./picosat.ccomp.target $DATA 2>&1 > picosat.ccomp.out
+if [ $? -ge 100 ];
+then exit 5 ;
+fi
+
+if grep timeout picosat.ccomp.out ;
+then exit 9 ;
+fi
+
+if ! cmp picosat.gcc.out picosat.ccomp.out ;
+then exit 6 ;
+fi
+
+$SIMU ./picosat.prepass.target $DATA 2>&1 > picosat.prepass.out
+if [ $? -ge 100 ];
+then exit 0 ;
+fi
+
+if cmp picosat.gcc.out picosat.prepass.out ;
+then exit 7 ;
+fi
+
+exit 0
diff --git a/test/monniaux/rules.mk b/test/monniaux/rules.mk
index c0594ef9..cab957c0 100644
--- a/test/monniaux/rules.mk
+++ b/test/monniaux/rules.mk
@@ -21,15 +21,15 @@ MEASURES?=time
 ALL_CFLAGS+=-Wall -D__KVX_COS__ -DMAX_MEASURES=$(MAX_MEASURES)
 #ALL_CFLAGS+=-g
 ALL_GCCFLAGS+=$(ALL_CFLAGS) -std=c99 -Wextra -Werror=implicit
-ALL_CCOMPFLAGS+=$(ALL_CFLAGS)
+ALL_CCOMPFLAGS+=$(ALL_CFLAGS) # -fprofile-use= ../compcert_profiling.dat
 
 # The compilers
-KVX_CC?=kvx-cos-gcc
+KVX_CC?=kvx-elf-gcc
 KVX_CCOMP?=ccomp
 
 # Command to execute
 #EXECUTE_CYCLES?=timeout --signal=SIGTERM 3m kvx-cluster --syscall=libstd_scalls.so --cycle-based --
-EXECUTE_CYCLES?=kvx-cluster --syscall=libstd_scalls.so --cycle-based --
+EXECUTE_CYCLES?=kvx-cluster --enable-cache --syscall=libstd_scalls.so --cycle-based --
 
 # You can define up to GCC4FLAGS and CCOMP4FLAGS
 GCC0FLAGS?=$(ALL_GCCFLAGS) -O0
@@ -37,11 +37,11 @@ GCC1FLAGS?=$(ALL_GCCFLAGS) -O1
 GCC2FLAGS?=$(ALL_GCCFLAGS) -O2
 GCC3FLAGS?=$(ALL_GCCFLAGS) -O3
 GCC4FLAGS?=
-CCOMP0FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fno-postpass
-CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fpostpass= greedy
-CCOMP2FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fno-if-conversion
-CCOMP3FLAGS?=$(ALL_CCOMPFLAGS) -O2
-CCOMP4FLAGS?=
+CCOMP0FLAGS?=$(ALL_CCOMPFLAGS) -O2 
+CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fprepass= list
+CCOMP2FLAGS?=$(ALL_CCOMPFLAGS) -O2 -funrollsingle 30
+CCOMP3FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fprepass= list -funrollsingle 30
+CCOMP4FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fprepass= zigzag
 
 # Prefix names
 GCC0PREFIX?=.gcc.o0
@@ -49,11 +49,11 @@ GCC1PREFIX?=.gcc.o1
 GCC2PREFIX?=.gcc.o2
 GCC3PREFIX?=.gcc.o3
 GCC4PREFIX?=
-CCOMP0PREFIX?=.ccomp.nobundle
-CCOMP1PREFIX?=.ccomp.greedy
-CCOMP2PREFIX?=.ccomp.noif
-CCOMP3PREFIX?=.ccomp
-CCOMP4PREFIX?=
+CCOMP0PREFIX?=.ccomp
+CCOMP1PREFIX?=.ccomp.prepass_list
+CCOMP2PREFIX?=.ccomp.unrollsingle_30
+CCOMP3PREFIX?=.ccomp.prepass_list-unrollsingle_30
+CCOMP4PREFIX?=.ccomp.prepass_zigzag
 
 # List of outfiles, updated by gen_rules
 OUTFILES:=
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 4dfbe565..56d90469 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -1,6 +1,8 @@
 include ../../Makefile.config
 
 CCOMP=../../ccomp
+# TODO - temporary
+# CCOMPOPTS:=$(CCOMPOPTS) -fall-loads-nontrap -fduplicate 2 -fprepass
 CCOMPFLAGS=$(CCOMPOPTS) -stdlib ../../runtime \
  -dparse -dc -dclight -dasm -fall \
  -DARCH_$(ARCH) -DMODEL_$(MODEL)