6 files changed, 147 insertions, 0 deletions
diff --git a/test/mppa/prng/.gitignore b/test/mppa/prng/.gitignore
new file mode 100644
index 00000000..0792a78b
--- /dev/null
+++ b/test/mppa/prng/.gitignore
@@ -0,0 +1,3 @@
+prng-test-ccomp-k1c
+prng-test-gcc-x86
+prng-test-gcc-k1c
diff --git a/test/mppa/prng/Makefile b/test/mppa/prng/Makefile
new file mode 100644
index 00000000..9cbb3872
--- /dev/null
+++ b/test/mppa/prng/Makefile
@@ -0,0 +1,69 @@
+K1CC ?= k1-cos-gcc
+CC ?= gcc
+CCOMP ?= ccomp
+CFLAGS ?= -O2
+SIMU ?= k1-mppa
+TIMEOUT ?= 10s
+
+K1CCPATH=$(shell which $(K1CC))
+CCPATH=$(shell which $(CC))
+CCOMPPATH=$(shell which $(CCOMP))
+SIMUPATH=$(shell which $(SIMU))
+
+ALL= prng-test-gcc-x86 prng-test-gcc-k1c prng-test-ccomp-k1c
+CCOMP_OUT= prng-test-ccomp-k1c.out
+GCC_OUT= prng-test-gcc-k1c.out
+X86_GCC_OUT= prng-test-gcc-x86.out
+STUB_OUT=.zero
+
+all: $(ALL)
+
+prng-test-gcc-x86: prng.c $(CCPATH)
+	$(CC) -D__UNIT_TEST_PRNG__ $(CFLAGS) $< -o $@
+
+prng-test-gcc-k1c: prng.c $(K1CCPATH)
+	$(K1CC) -D__UNIT_TEST_PRNG__ $(CFLAGS) $< -o $@
+
+prng-test-ccomp-k1c: prng.c $(CCOMPPATH)
+	$(CCOMP) -D__UNIT_TEST_PRNG__ $(CFLAGS) $< -o $@
+
+.SECONDARY:
+%k1c.out: %k1c $(SIMUPATH)
+	ret=0; timeout $(TIMEOUT) $(SIMU) -- $<  > $@ || { ret=$$?; }; echo $$ret >> $@
+
+%x86.out: %x86
+	ret=0; timeout $(TIMEOUT) ./$< > $@ || { ret=$$?; }; echo $$ret >> $@
+
+.zero:
+	@echo "0" > $@
+
+.PHONY:
+test: test-x86 test-k1c
+
+.PHONY:
+test-x86: $(X86_GCC_OUT) $(STUB_OUT)
+	@if ! diff $< $(STUB_OUT); then\
+		>&2 echo "ERROR x86: $< failed";\
+	else\
+		echo "GOOD x86: $< succeeded";\
+	fi
+
+.PHONY:
+test-k1c: $(GCC_OUT) $(STUB_OUT)
+	@if ! diff $< $(STUB_OUT); then\
+		>&2 echo "ERROR k1c: $< failed";\
+	else\
+		echo "GOOD k1c: $< succeeded";\
+	fi
+
+.PHONY:
+check: $(CCOMP_OUT) $(STUB_OUT)
+	@if ! diff $< $(STUB_OUT); then\
+		>&2 echo "ERROR k1c: $< failed";\
+	else\
+		echo "GOOD k1c: $< succeeded";\
+	fi
+
+.PHONY:
+clean:
+	rm -f prng-test-gcc-x86 prng-test-gcc-k1c prng-test-ccomp-k1c
diff --git a/test/mppa/prng/README.md b/test/mppa/prng/README.md
new file mode 100644
index 00000000..b4c2279b
--- /dev/null
+++ b/test/mppa/prng/README.md
@@ -0,0 +1,17 @@
+PRNG
+====
+
+This is a simple Pseudo Random Number Generator.
+
+`prng.c` contains a simple unitary test that compares the sum of the "bytewise sum"
+of 1000 generated numbers to a hardcoded result, that is the one obtained with
+`gcc -O2` on a x86 processor, and returns 0 if the result is correct.
+
+The following commands can be run inside that folder:
+
+- `make`: produces the unitary test binaries
+  - `prng-test-gcc-x86` : binary from gcc on x86
+  - `prng-test-k1c-x86` : binary from gcc on k1c
+  - `prng-test-ccomp-x86` : binary from ccomp on k1c
+- `make test`: tests the return value of the binaries produced by gcc.
+- `make check`: tests the return value of the binary produced by CompCert.
diff --git a/test/mppa/prng/prng.c b/test/mppa/prng/prng.c
new file mode 100644
index 00000000..71de1dc3
--- /dev/null
+++ b/test/mppa/prng/prng.c
@@ -0,0 +1,41 @@
+// https://en.wikipedia.org/wiki/Linear_congruential_generator -> MMIX Donald Knuth
+// modulo 2^64 = no need to do it explicitly
+
+#include "types.h"
+
+#define MULTIPLIER 6364136223846793005LL
+#define INCREMENT 1442695040888963407LL
+
+static uint64_t current;
+
+void srand(uint64_t seed){
+    current = seed;
+}
+
+uint64_t randlong(void){
+    return (current = MULTIPLIER * current + INCREMENT);
+}
+
+#ifdef __UNIT_TEST_PRNG__
+char bytewise_sum(uint64_t to_check){
+    char sum = 0;
+    int i;
+
+    for (i = 0 ; i < 8 ; i++)
+        sum += (to_check & (uint64_t)(0xFFULL << i*8)) >> i*8;
+
+    return sum;
+}
+
+int main(void){
+    srand(42);
+    int i;
+
+    for (i = 0 ; i < 1000 ; i++)
+        randlong();
+
+    uint64_t last = randlong();
+
+    return !((unsigned char)bytewise_sum(last) == 155);
+}
+#endif // __UNIT_TEST_PRNG__
diff --git a/test/mppa/prng/prng.h b/test/mppa/prng/prng.h
new file mode 100644
index 00000000..6abdb45a
--- /dev/null
+++ b/test/mppa/prng/prng.h
@@ -0,0 +1,10 @@
+#ifndef __PRNG_H__
+#define __PRNG_H__
+
+#include "types.h"
+
+void srand(uint64_t seed);
+
+uint64_t randlong(void);
+
+#endif // __PRNG_H__
diff --git a/test/mppa/prng/types.h b/test/mppa/prng/types.h
new file mode 100644
index 00000000..584023e3
--- /dev/null
+++ b/test/mppa/prng/types.h
@@ -0,0 +1,7 @@
+#ifndef __TYPES_H__
+#define __TYPES_H__
+
+#define uint64_t    unsigned long long
+#define int64_t     signed long long
+
+#endif // __TYPES_H__