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

9 files changed, 122 insertions, 10 deletions

diff --git a/test/gourdinl/builtin_memcpy.c b/test/gourdinl/builtin_memcpy.c
new file mode 100644
index 00000000..421f543c
--- /dev/null
+++ b/test/gourdinl/builtin_memcpy.c
@@ -0,0 +1,9 @@
+struct a b;
+struct a {
+  short;
+  int;
+  short;
+} c() {
+  struct a d[2][16];
+  b = d[1][7];
+}
diff --git a/test/monniaux/codegen/comp0.c b/test/monniaux/codegen/comp0.c
new file mode 100644
index 00000000..60f8ba77
--- /dev/null
+++ b/test/monniaux/codegen/comp0.c
@@ -0,0 +1,3 @@
+int toto(unsigned x) {
+  return (x < 0) ? 1 : 2;
+}
diff --git a/test/monniaux/csmith/Makefile b/test/monniaux/csmith/Makefile
index aa4eccab..1412921d 100644
--- a/test/monniaux/csmith/Makefile
+++ b/test/monniaux/csmith/Makefile
@@ -1,9 +1,16 @@
+all:
+
+.SECONDARY:
+
 INCLUDES=-I csmith/include/csmith-2.3.0/
 TARGET_CCOMP=../../../ccomp
+
+ifndef TARGET_CC
 TARGET_CC=gcc
+endif
 
 ifndef EXECUTE
-EXECUTE=timeout 2s
+EXECUTE=timeout 10s 
 endif
 
 CFLAGS += -Wno-incompatible-pointer-types
@@ -11,12 +18,13 @@ CFLAGS += -Wno-incompatible-pointer-types
 ifndef CSMITH
 CSMITH=csmith/bin/csmith
 endif
+CSMITHOPT=--max-funcs 10 --no-packed-struct
 
-MAX=300
+MAX=500
 PREFIX=ran%06.f
 
-CCOMPOTS=-static
-CCOMPFLAGS+= -fstruct-passing -fbitfields -fno-cse2 -stdlib ../../../runtime
+# CCOMPOPTS=-Wl,--defsym=USER_STACK_SIZE=0x80000
+CCOMPFLAGS+= -fstruct-passing -fbitfields -fno-cse2 -fno-cse -fno-cse3 -stdlib ../../../runtime
 
 TESTS_C=$(shell seq --format $(PREFIX)/source.c 1 $(MAX))
 
@@ -69,12 +77,13 @@ ran%/example.gcc.host: ran%/source.gcc.host.o
 
 ran%/source.c:
 	mkdir -p ran$*
-	$(CSMITH) --seed $* --output ran$*/source.c
+	$(CSMITH) $(CSMITHOPT) --seed $* --output ran$*/source.c
 
-ran%/example.target.cmp : ran%/example.gcc.target.out ran%/example.ccomp.target.out
+ran%/example.target.cmp : ran%/example.ccomp.target.out ran%/example.gcc.target.out
 	cmp $+ > $@
+	cat $<
 
-ran%/example.host_target.cmp : ran%/example.gcc.host.out ran%/example.ccomp.target.out
+ran%/example.host_target.cmp : ran%/example.ccomp.target.out ran%/example.gcc.host.out
 	cmp $+ > $@
 
 .PHONY: all clean tests_c tests_c
@@ -82,7 +91,9 @@ ran%/example.host_target.cmp : ran%/example.gcc.host.out ran%/example.ccomp.targ
 clean:
 	-rm -rf ran*
 
-csmith/bin/csmith:
-	curl -L -o csmith-2.3.0.tar.gz https://embed.cs.utah.edu/csmith/csmith-2.3.0.tar.gz
+csmith-2.3.0.tar.gz:
+	curl -L -o $@  https://embed.cs.utah.edu/csmith/csmith-2.3.0.tar.gz
+
+csmith/bin/csmith: csmith-2.3.0.tar.gz
 	tar xfz csmith-2.3.0.tar.gz
 	WD=`pwd` && cd csmith-2.3.0 && ./configure --prefix=$$WD/csmith && make install
diff --git a/test/monniaux/csmith/reduce/reduce.sh b/test/monniaux/csmith/reduce/reduce.sh
new file mode 100755
index 00000000..d8df11a5
--- /dev/null
+++ b/test/monniaux/csmith/reduce/reduce.sh
@@ -0,0 +1,15 @@
+#!/bin/bash
+INCLUDE=-I$COMPCERT/test/monniaux/csmith/csmith/include/csmith-2.3.0
+if kvx-cos-gcc $INCLUDE -Werror=uninitialized -Werror=implicit source.c -o source.gcc.target && kvx-cluster -- source.gcc.target >& source.gcc.log
+then
+    if $COMPCERT/ccomp $INCLUDE -fall -fno-cse -fno-cse2 -fno-cse3 source.c -o source.ccomp.target
+    then
+	kvx-cluster -- source.ccomp.target >& source.ccomp.log
+	grep OPCODE source.ccomp.log
+    else
+	exit 2
+    fi
+else
+    exit 1
+fi
+    
diff --git a/test/monniaux/csmith/reduce/reduce_wrt_host.sh b/test/monniaux/csmith/reduce/reduce_wrt_host.sh
new file mode 100755
index 00000000..7a11596f
--- /dev/null
+++ b/test/monniaux/csmith/reduce/reduce_wrt_host.sh
@@ -0,0 +1,37 @@
+#!/bin/bash
+INCLUDE=-I$COMPCERT/test/monniaux/csmith/csmith/include/csmith-2.3.0
+if /usr/bin/clang $INCLUDE -O -Werror=int-conversion -Werror=format -Werror=strict-prototypes -Werror=uninitialized -Werror=implicit -Werror=return-type source.c -o source.clang.host && valgrind --exit-on-first-error=yes --error-exitcode=120 --log-file=valgrind.out ./source.clang.host > source.clang.host.out ;
+then
+    if gcc $INCLUDE -Werror=int-conversion -Werror=format -Werror=strict-prototypes -Werror=uninitialized -Werror=implicit -Werror=return-type -fsanitize=undefined -fsanitize=address source.c -o source.gcc+san.host && ./source.gcc+san.host > source.gcc+san.host.out ;
+    then
+	if grep "runtime error" source.gcc+san.host.out
+	then
+	    exit 66
+	fi
+	if cmp source.clang.host.out source.gcc+san.host.out && riscv64-linux-gnu-gcc $INCLUDE -Werror=format -Werror=uninitialized -Werror=implicit source.c -Werror=return-type -o source.gcc.target && qemu-riscv64 -L /usr/riscv64-linux-gnu source.gcc.target >& source.gcc.target.out && grep checksum source.gcc.target.out > source.gcc.target.check && diff source.clang.host.out source.gcc.target.out
+	then
+	    if $COMPCERT/ccomp $INCLUDE -Werror=missing-declarations -fall -fno-cse -fno-cse2 -fno-cse3 source.c -o source.ccomp.target
+	    then
+		qemu-riscv64 -L /usr/riscv64-linux-gnu source.ccomp.target >& source.ccomp.target.out
+		if grep checksum source.ccomp.target.out > source.ccomp.target.check
+		then
+		    if diff	source.ccomp.target.check source.gcc.target.check
+		    then exit 40
+		    else exit 0
+		    fi
+		else
+	            exit 50
+		fi
+	    else
+		exit 2
+	    fi
+	else
+	    exit 1
+	fi
+    else
+	exit 4
+    fi
+else
+    exit 5
+fi
+    
diff --git a/test/regression/Makefile b/test/regression/Makefile
index c56532ff..69d25980 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -18,7 +18,7 @@ TESTS?=int32 int64 floats floats-basics floats-lit \
   funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \
   sizeof1 sizeof2 binops bool for1 for2 switch switch2 compound \
   decl1 bitfields9 ptrs3 \
-  parsing krfun ifconv union_passing
+  parsing krfun ifconv many_parameters union_passing
 
 # Can run, but only in compiled mode, and have reference output in Results
 
diff --git a/test/regression/Results/many_parameters b/test/regression/Results/many_parameters
new file mode 100644
index 00000000..838cfd7e
--- /dev/null
+++ b/test/regression/Results/many_parameters
@@ -0,0 +1 @@
+1780
diff --git a/test/monniaux/params/call_many.c b/test/regression/many_parameters.c
index 4d2529c0..4d2529c0 100644
--- a/test/monniaux/params/call_many.c
+++ b/test/regression/many_parameters.c
diff --git a/test/regression/ran000373_reduced.c b/test/regression/ran000373_reduced.c
new file mode 100644
index 00000000..3f26e88a
--- /dev/null
+++ b/test/regression/ran000373_reduced.c
@@ -0,0 +1,36 @@
+#include <stdint.h>
+#include <stdio.h>
+uint32_t au, cc, bk;
+union ba {
+  int64_t bb;
+};
+int32_t *ck;
+int32_t **cr = &ck;
+void a(uint32_t c, int d) { printf("checksum = %X\n", c); }
+void av(uint8_t b) { au = b; }
+void aw(uint64_t ax) { av(ax); }
+void ay(uint64_t ax, char *az, int d) { aw(ax); }
+static const int32_t df(int64_t, union ba, uint16_t, uint8_t);
+const int32_t dh(int32_t, int32_t, uint32_t);
+int16_t e(void) {
+  union ba f = {5};
+  int32_t g = 5;
+  int32_t i[90269];
+  uint32_t s = df(dh(0, 0, cc), f, g, 7);
+  return s;
+}
+const int32_t df(int64_t j, union ba k, uint16_t l, uint8_t m) {
+  *ck = k.bb;
+  return l;
+}
+const int32_t dh(int32_t n, int32_t o, uint32_t p) {
+  int32_t *t = &bk;
+  uint64_t q = 3;
+  *cr = t;
+  return q;
+}
+int main(void) {
+  int r = e();
+  ay(bk, "", r);
+  a(au, r);
+}