diff options
Diffstat (limited to 'test/monniaux')
-rw-r--r-- | test/monniaux/picosat-965/onefile/picosat.c | 25 | ||||
-rwxr-xr-x | test/monniaux/picosat-965/onefile/testcmp.sh | 146 | ||||
-rw-r--r-- | test/monniaux/picosat-965/small.dat | 2 | ||||
-rw-r--r-- | test/monniaux/picosat-965/tiny.dat | 2 | ||||
-rw-r--r-- | test/monniaux/reduced_picosat/reduced_picosat.c | 23 | ||||
-rw-r--r-- | test/monniaux/reduced_picosat/test_a.s | 10 | ||||
-rw-r--r-- | test/monniaux/reduced_picosat/test_b.c | 9 | ||||
-rwxr-xr-x | test/monniaux/reduced_picosat/testcmp.sh | 146 | ||||
-rw-r--r-- | test/monniaux/rules.mk | 24 |
9 files changed, 375 insertions, 12 deletions
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..7d9457fd 100644 --- a/test/monniaux/rules.mk +++ b/test/monniaux/rules.mk @@ -21,10 +21,10 @@ 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 @@ -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 -ftracelinearize -fduplicate 0 +CCOMP2FLAGS?=$(ALL_CCOMPFLAGS) -O2 -ftracelinearize -fduplicate 1 -fprepass -fprepass= list +CCOMP3FLAGS?=$(ALL_CCOMPFLAGS) -O2 -ftracelinearize -fduplicate 2 -fprepass -fprepass= list +CCOMP4FLAGS?=$(ALL_CCOMPFLAGS) -O2 -ftracelinearize -fduplicate 0 -fprepass -fprepass= list # 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.linearize +CCOMP2PREFIX?=.ccomp.prepass1 +CCOMP3PREFIX?=.ccomp.prepass2 +CCOMP4PREFIX?=.ccomp.prepass0 # List of outfiles, updated by gen_rules OUTFILES:= |