diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-27 23:47:55 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-07-27 23:47:55 +0200 |
commit | 8cee2111e40fdd0c12afab1718e732f1bad71d5c (patch) | |
tree | 21f61d5ef916e003be23e1d1f1bc410001d4bb00 /test | |
parent | ea70d7a4ef0e4fbf7b19378c4bfdf6a451ddf025 (diff) | |
parent | d2a72d9218f633e99028d6ac59d19ec1bec81493 (diff) | |
download | compcert-kvx-8cee2111e40fdd0c12afab1718e732f1bad71d5c.tar.gz compcert-kvx-8cee2111e40fdd0c12afab1718e732f1bad71d5c.zip |
Merge branch 'mppa-RTLpathSE-verif-hash-junk' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-RTLpathSE-verif-hash-junk
Diffstat (limited to 'test')
-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 |
4 files changed, 188 insertions, 0 deletions
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 |