11 files changed, 59 insertions, 92 deletions
diff --git a/test/monniaux/Makefile b/test/monniaux/Makefile
index a6b19891..d7437eea 100644
--- a/test/monniaux/Makefile
+++ b/test/monniaux/Makefile
@@ -20,9 +20,12 @@ oracle_times.txt: PostpassSchedulingOracle.patch
 	bash build_benches.sh $@
 
 measures.csv:
-	(cd ../../ && make -j20 && make install)
-	bash build_benches.sh
-	bash run_benches.sh $@
+	@echo "Building compcert.."
+	@(cd ../../ && make -s -j20 && make -s install)
+	@echo "Building benches..."
+	@bash build_benches.sh
+	@echo "Benches built. Running benches..."
+	@bash run_benches.sh $@
 
 #compile_times.pdf: gencompile.py verifier_times.txt oracle_times.txt
 #	python3.5 $^ $@
@@ -32,4 +35,5 @@ measures.csv:
 
 .PHONY:
 clean:
+	@bash clean_benches.sh
 	rm -f verifier_times.txt oracle_times.txt compile_times.pdf measure_times.k1c.pdf measures.csv
diff --git a/test/monniaux/README.md b/test/monniaux/README.md
index dbb3f337..f2af67fb 100644
--- a/test/monniaux/README.md
+++ b/test/monniaux/README.md
@@ -37,6 +37,7 @@ float_mat c3,  1504675,  751514,  553235, 1929369,  1372441
 - `K1C_CC`: GCC compiler (default k1-cos-gcc)
 - `K1C_CCOMP`: compcert compiler (default ccomp)
 - `EXECUTE_CYCLES`: running command (default `k1-cluster` with some options)
+- `EXECUTE_ARGS`: execution arguments
 - `GCCiFLAGS` with i from 0 to 4: the wanted optimizations. If one of these flags is empty, nothing is done. Same for `CCOMPiFLAGS`. For now, the default values:
 ```
 # You can define up to GCC4FLAGS and CCOMP4FLAGS
@@ -68,4 +69,10 @@ The `PREFIX` are the prefixes to add to the .s, .o, etc.. You should be careful
 
 Assembly files will be generated in `asm/`, objects in `obj/`, binaries in `bin/` and outputs in `out/`.
 
-To compile and execute all the benches : `make`
+To compile and execute all the benches : `make` while in the `monniaux` directory (without any `-j` flag).
+
+To compile and/or execute a single bench, `cd` to the bench directory, then:
+- `make` for compiling the bench
+- `make run` for running it
+
+You can use `-j` flag when in a single bench directory
diff --git a/test/monniaux/benches.sh b/test/monniaux/benches.sh
index 2365063a..6014f628 100644
--- a/test/monniaux/benches.sh
+++ b/test/monniaux/benches.sh
@@ -1,3 +1,3 @@
-benches="binary_search bitsliced-aes bitsliced-tea complex float_mat glibc_qsort heapsort idea number_theoretic_transform quicksort sha-2 tacle-bench-lift tacle-bench-powerwindow too_slow heptagon_radio_transmitter lustrev4_lustrec_heater_control lustrev4_lv4_heater_control lustrev4_lv6-en-2cgc_heater_control lustrev6-convertible-en-2cgc xor_and_mat"
+benches="binary_search bitsliced-aes bitsliced-tea complex float_mat glibc_qsort heapsort idea number_theoretic_transform quicksort sha-2 tacle-bench-lift tacle-bench-powerwindow too_slow heptagon_radio_transmitter lustrev4_lustrec_heater_control lustrev4_lv4_heater_control lustrev4_lv6-en-2cgc_heater_control lustrev6-convertible-en-2cgc xor_and_mat glpk-4.65 picosat-965 genann"
 
 # Removed for now : ternary
diff --git a/test/monniaux/build_benches.sh b/test/monniaux/build_benches.sh
index 931cebac..a749779d 100755
--- a/test/monniaux/build_benches.sh
+++ b/test/monniaux/build_benches.sh
@@ -4,11 +4,16 @@ TMPFILE=/tmp/1513times.txt
 
 source benches.sh
 
+default="\e[39m"
+magenta="\e[35m"
+red="\e[31m"
+
 rm -f commands.txt
 rm -f $TMPFILE
 for bench in $benches; do
+  echo -e "${magenta}Building $bench..${default}"
   if [ "$1" == "" ]; then 
-    (cd $bench && make -j20)
+    (cd $bench && make -s -j20 > /dev/null &> /dev/null) || { echo -e "${red}Build failed" && break; }
   else
     (cd $bench && make -j20) | grep -P "\d+: \d+\.\d+" >> $TMPFILE
   fi
diff --git a/test/monniaux/clean_benches.sh b/test/monniaux/clean_benches.sh
index c0a87ff9..dff15fd4 100755
--- a/test/monniaux/clean_benches.sh
+++ b/test/monniaux/clean_benches.sh
@@ -1,8 +1,12 @@
 
 source benches.sh
 
+blue="\e[34m"
+default="\e[39m"
+
 rm -f commands.txt
 for bench in $benches; do
-  (cd $bench && make clean)
+  echo -e "${blue}Cleaning $bench..${default}"
+  (cd $bench && make -s clean)
 done
 rm -f *.o
diff --git a/test/monniaux/genann/Makefile b/test/monniaux/genann/Makefile
new file mode 100644
index 00000000..2e76ec63
--- /dev/null
+++ b/test/monniaux/genann/Makefile
@@ -0,0 +1,4 @@
+ALL_CFILES= example4shorter.c genann.c
+TARGET=genann4
+
+include ../rules.mk
diff --git a/test/monniaux/genann/make.proto b/test/monniaux/genann/make.proto
deleted file mode 100644
index 7c4248bf..00000000
--- a/test/monniaux/genann/make.proto
+++ /dev/null
@@ -1,2 +0,0 @@
-sources: example4shorter.c genann.c
-target: genann4
-\ No newline at end of file
diff --git a/test/monniaux/glpk-4.65/Makefile b/test/monniaux/glpk-4.65/Makefile
index a0ab40dc..eaa3f4b0 100644
--- a/test/monniaux/glpk-4.65/Makefile
+++ b/test/monniaux/glpk-4.65/Makefile
@@ -1,39 +1,6 @@
 ALL_CFLAGS += -I src/amd -I src/colamd -I src/mpl -I src/simplex -I src/api -I src/intopt -I src/minisat -I src/npp -I src/zlib -I src/bflib -I src/env -I src/misc -I src/draft -I src
-
-include ../rules.mk
-
-LIBS = -lm
-
-src=examples/glpsol.c $(wildcard src/*/*.c)
-
-PRODUCTS?=glpsol.gcc.host glpsol.ccomp.host glpsol.gcc.k1c glpsol.gcc.o1.k1c glpsol.ccomp.k1c
-PRODUCTS_OUT=$(addsuffix .out,$(PRODUCTS))
-
-all: $(PRODUCTS)
-
-.PHONY:
-run: measures.csv
-
-
-glpsol.gcc.host: $(src:.c=.gcc.host.o) ../clock.gcc.host.o 
-	$(CC) $(CFLAGS) $+ $(LIBS) -o $@
-glpsol.ccomp.host: $(src:.c=.ccomp.host.o) ../clock.gcc.host.o 
-	$(CCOMP) $(CCOMPFLAGS) $+ $(LIBS) -o $@
-glpsol.gcc.k1c: $(src:.c=.gcc.k1c.o) ../clock.gcc.k1c.o 
-	$(K1C_CC) $(K1C_CFLAGS) $+  $(LIBS) -o $@
-glpsol.gcc.o1.k1c: $(src:.c=.gcc.o1.k1c.o) ../clock.gcc.k1c.o 
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+  $(LIBS) -o $@
-glpsol.ccomp.k1c: $(src:.c=.ccomp.k1c.o) ../clock.gcc.k1c.o 
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+  $(LIBS) -o $@
-
+ALL_CFILES=examples/glpsol.c $(wildcard src/*/*.c)
+TARGET=glpk
 EXECUTE_ARGS=--math examples/prod.mod
 
-measures.csv: $(PRODUCTS_OUT)
-	echo "benches, gcc host,ccomp host,gcc k1c,gcc o1 k1c,ccomp k1c" > $@
-
-.SECONDARY:
-
-.PHONY:
-clean:
-	rm -f *.o *.s *.k1c *.csv
-
+include ../rules.mk
diff --git a/test/monniaux/picosat-965/Makefile b/test/monniaux/picosat-965/Makefile
index 991278ff..a887c0de 100644
--- a/test/monniaux/picosat-965/Makefile
+++ b/test/monniaux/picosat-965/Makefile
@@ -1,37 +1,11 @@
 EXECUTE_ARGS=sudoku.sat
-
-include ../rules.mk
-
-#ALL_CFLAGS = -DNDEBUG
 ALL_CFLAGS = -DNALARM -DNZIP -DNGETRUSAGE -DNDEBUG
-K1C_CFLAGS += $(EMBEDDED_CFLAGS)
-K1C_CCOMPFLAGS += $(EMBEDDED_CFLAGS)
-CCOMPFLAGS += -fbitfields
-K1C_CCOMPFLAGS += -fbitfields # -fno-if-conversion
-
-K1C_CFLAGS += $(ALL_CFLAGS)
-K1C_CCOMPFLAGS += $(ALL_CFLAGS)
-CCOMPFLAGS += $(ALL_CFLAGS)
-CFLAGS += $(ALL_CFLAGS)
-
-all: picosat.ccomp.k1c.s version.ccomp.k1c.s app.ccomp.k1c.s main.ccomp.k1c.s picosat.gcc.k1c.s version.gcc.k1c.s app.gcc.k1c.s main.gcc.k1c.s picosat.ccomp.k1c.out picosat.gcc.o1.k1c.out picosat.gcc.k1c.out picosat picosat.ccomp.host.out picosat.gcc.host.out
-
-picosat.ccomp.k1c : picosat.ccomp.k1c.s version.ccomp.k1c.s app.ccomp.k1c.s main.ccomp.k1c.s ../clock.gcc.k1c.o
-	$(K1C_CCOMP) $(K1C_CCOMPFLAGS) $+ -o $@
+ALL_CCOMPFLAGS += -fbitfields # -fno-if-conversion
+TARGET=picosat
+ALL_CFILES=picosat.c version.c app.c main.c
 
-picosat.gcc.k1c : picosat.gcc.k1c.s version.gcc.k1c.s app.gcc.k1c.s main.gcc.k1c.s ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS) $+ -o $@
-
-picosat.gcc.o1.k1c : picosat.gcc.o1.k1c.s version.gcc.o1.k1c.s app.gcc.o1.k1c.s main.gcc.o1.k1c.s ../clock.gcc.k1c.o
-	$(K1C_CC) $(K1C_CFLAGS_O1) $+ -o $@
-
-picosat.ccomp.host : picosat.ccomp.host.s version.ccomp.host.s app.ccomp.host.s main.ccomp.host.s ../clock.gcc.host.o
-	$(CCOMP) $(CCOMPFLAGS) $+ -o $@
-
-picosat.gcc.host : picosat.gcc.host.s version.gcc.host.s app.gcc.host.s main.gcc.host.s ../clock.gcc.host.o
-	$(CC) $(FLAGS) $+ -o $@
-
-clean:
-	-rm -f *.s *.k1c *.out
+include ../rules.mk
 
-.PHONY: clean
+# FIXME - what were these for?
+#K1C_CFLAGS += $(EMBEDDED_CFLAGS)
+#K1C_CCOMPFLAGS += $(EMBEDDED_CFLAGS)
diff --git a/test/monniaux/rules.mk b/test/monniaux/rules.mk
index 9d05b4d6..9d4f5278 100644
--- a/test/monniaux/rules.mk
+++ b/test/monniaux/rules.mk
@@ -7,6 +7,9 @@ ALL_CFILES?=$(wildcard *.c)
 # Name of the target
 TARGET?=toto
 
+# Arguments of execution
+EXECUTE_ARGS?=
+
 # Name of the clock object
 CLOCK=../clock
 
@@ -28,27 +31,27 @@ K1C_CCOMP?=ccomp
 EXECUTE_CYCLES?=k1-cluster --syscall=libstd_scalls.so --cycle-based --
 
 # You can define up to GCC4FLAGS and CCOMP4FLAGS
-GCC0FLAGS?=
-GCC1FLAGS?=$(ALL_GCCFLAGS) -O1 -g
+GCC0FLAGS?=$(ALL_GCCFLAGS) -O0
+GCC1FLAGS?=$(ALL_GCCFLAGS) -O1
 GCC2FLAGS?=$(ALL_GCCFLAGS) -O2
 GCC3FLAGS?=$(ALL_GCCFLAGS) -O3
 GCC4FLAGS?=
-CCOMP0FLAGS?=
-CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -O1 -g
-CCOMP2FLAGS?=$(ALL_CCOMPFLAGS)
-CCOMP3FLAGS?=
+CCOMP0FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fno-postpass
+CCOMP1FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fpostpass= greedy
+CCOMP2FLAGS?=$(ALL_CCOMPFLAGS) -O2 -fno-if-conversion
+CCOMP3FLAGS?=$(ALL_CCOMPFLAGS) -O2
 CCOMP4FLAGS?=
 
 # Prefix names
-GCC0PREFIX?=
+GCC0PREFIX?=.gcc.o0
 GCC1PREFIX?=.gcc.o1
 GCC2PREFIX?=.gcc.o2
 GCC3PREFIX?=.gcc.o3
 GCC4PREFIX?=
-CCOMP0PREFIX?=
-CCOMP1PREFIX?=.ccomp.o1
-CCOMP2PREFIX?=.ccomp.o2
-CCOMP3PREFIX?=
+CCOMP0PREFIX?=.ccomp.nobundle
+CCOMP1PREFIX?=.ccomp.greedy
+CCOMP2PREFIX?=.ccomp.noif
+CCOMP3PREFIX?=.ccomp
 CCOMP4PREFIX?=
 
 # List of outfiles, updated by gen_rules
@@ -92,7 +95,7 @@ obj/%.o: asm/%.s
 
 out/%.out: bin/%.bin
 	@mkdir -p $(@D)
-	$(EXECUTE_CYCLES) $< | tee $@
+	$(EXECUTE_CYCLES) $< $(EXECUTE_ARGS) | tee $@
 
 ##
 # Generating the rules for all the compiler/flags..
diff --git a/test/monniaux/run_benches.sh b/test/monniaux/run_benches.sh
index 5f9f22cb..60eec865 100755
--- a/test/monniaux/run_benches.sh
+++ b/test/monniaux/run_benches.sh
@@ -3,10 +3,11 @@ source benches.sh
 
 rm -f commands.txt
 for bench in $benches; do
-  echo "(cd $bench && make -j5 run)" >> commands.txt
+  echo "(cd $bench && echo \"Running $bench..\" &&\
+    make -j4 run > /dev/null && echo \"$bench DONE\")" >> commands.txt
 done
 
-cat commands.txt | xargs -n1 -I{} -P4 bash -c '{}'
+cat commands.txt | xargs -n1 -I{} -P6 bash -c '{}'
 
 ##
 # Gather all the CSV files