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

3 files changed, 393 insertions, 9 deletions

diff --git a/test/monniaux/des/des.c b/test/monniaux/des/des.c
index e8fae267..64ccdc5e 100644
--- a/test/monniaux/des/des.c
+++ b/test/monniaux/des/des.c
@@ -1,3 +1,4 @@
+/* From Rosetta Code */
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
diff --git a/test/monniaux/sha-2/sha-256.c b/test/monniaux/sha-2/sha-256.c
index 53d6ff2e..17ba98aa 100644
--- a/test/monniaux/sha-2/sha-256.c
+++ b/test/monniaux/sha-2/sha-256.c
@@ -1,5 +1,10 @@
 #include <stdint.h>
 #include <string.h>
+#if 0 /* __COMPCERT__ */
+#define my_memcpy(dst, src, size) __builtin_memcpy_aligned(dst, src, size, 1)
+#else
+#define my_memcpy(dst, src, size) memcpy(dst, src, size)
+#endif
 
 #include "sha-256.h"
 
@@ -66,7 +71,7 @@ static int calc_chunk(uint8_t chunk[CHUNK_SIZE], struct buffer_state * state)
 	}
 
 	if (state->len >= CHUNK_SIZE) {
-		memcpy(chunk, state->p, CHUNK_SIZE);
+		my_memcpy(chunk, state->p, CHUNK_SIZE);
 		state->p += CHUNK_SIZE;
 		state->len -= CHUNK_SIZE;
 		return 1;
@@ -121,6 +126,7 @@ static int calc_chunk(uint8_t chunk[CHUNK_SIZE], struct buffer_state * state)
  *   for bit string lengths that are not multiples of eight, and it really operates on arrays of bytes.
  *   In particular, the len parameter is a number of bytes.
  */
+#if USE_ORIGINAL
 void calc_sha_256(uint8_t hash[32], const void * input, size_t len)
 {
 	/*
@@ -208,3 +214,337 @@ void calc_sha_256(uint8_t hash[32], const void * input, size_t len)
 		hash[j++] = (uint8_t) h[i];
 	}
 }
+#else
+#if DO_NOT_UNROLL
+/* Modified by D. Monniaux */
+void calc_sha_256(uint8_t hash[32], const void * input, size_t len)
+{
+	/*
+	 * Note 1: All integers (expect indexes) are 32-bit unsigned integers and addition is calculated modulo 2^32.
+	 * Note 2: For each round, there is one round constant k[i] and one entry in the message schedule array w[i], 0 = i = 63
+	 * Note 3: The compression function uses 8 working variables, a through h
+	 * Note 4: Big-endian convention is used when expressing the constants in this pseudocode,
+	 *     and when parsing message block data from bytes to words, for example,
+	 *     the first word of the input message "abc" after padding is 0x61626380
+	 */
+
+	/*
+	 * Initialize hash values:
+	 * (first 32 bits of the fractional parts of the square roots of the first 8 primes 2..19):
+	 */
+	uint32_t h[] = { 0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a, 0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19 };
+	int i, j;
+
+	/* 512-bit chunks is what we will operate on. */
+	uint8_t chunk[64];
+
+	struct buffer_state state;
+
+	init_buf_state(&state, input, len);
+
+	while (calc_chunk(chunk, &state)) {
+	        uint32_t ah0, ah1, ah2, ah3, ah4, ah5, ah6, ah7;
+		
+		/*
+		 * create a 64-entry message schedule array w[0..63] of 32-bit words
+		 * (The initial values in w[0..63] don't matter, so many implementations zero them here)
+		 * copy chunk into first 16 words w[0..15] of the message schedule array
+		 */
+		uint32_t w[64];
+		const uint8_t *p = chunk;
+
+		memset(w, 0x00, sizeof w);
+		for (i = 0; i < 16; i++) {
+			w[i] = (uint32_t) p[0] << 24 | (uint32_t) p[1] << 16 |
+				(uint32_t) p[2] << 8 | (uint32_t) p[3];
+			p += 4;
+		}
+
+		/* Extend the first 16 words into the remaining 48 words w[16..63] of the message schedule array: */
+		for (i = 16; i < 64; i++) {
+			const uint32_t s0 = right_rot(w[i - 15], 7) ^ right_rot(w[i - 15], 18) ^ (w[i - 15] >> 3);
+			const uint32_t s1 = right_rot(w[i - 2], 17) ^ right_rot(w[i - 2], 19) ^ (w[i - 2] >> 10);
+			w[i] = w[i - 16] + s0 + w[i - 7] + s1;
+		}
+		
+		/* Initialize working variables to current hash value: */
+		ah0 = h[0];
+		ah1 = h[1];
+		ah2 = h[2];
+		ah3 = h[3];
+		ah4 = h[4];
+		ah5 = h[5];
+		ah6 = h[6];
+		ah7 = h[7];
+
+		/* Compression function main loop: */
+		for (i = 0; i < 64; i++) {
+			const uint32_t s1 = right_rot(ah4, 6) ^ right_rot(ah4, 11) ^ right_rot(ah4, 25);
+			const uint32_t ch = (ah4 & ah5) ^ (~ah4 & ah6);
+			const uint32_t temp1 = ah7 + s1 + ch + k[i] + w[i];
+			const uint32_t s0 = right_rot(ah0, 2) ^ right_rot(ah0, 13) ^ right_rot(ah0, 22);
+			const uint32_t maj = (ah0 & ah1) ^ (ah0 & ah2) ^ (ah1 & ah2);
+			const uint32_t temp2 = s0 + maj;
+
+			ah7 = ah6;
+			ah6 = ah5;
+			ah5 = ah4;
+			ah4 = ah3 + temp1;
+			ah3 = ah2;
+			ah2 = ah1;
+			ah1 = ah0;
+			ah0 = temp1 + temp2;
+		}
+
+		/* Add the compressed chunk to the current hash value: */
+		h[0] += ah0;
+		h[1] += ah1;
+		h[2] += ah2;
+		h[3] += ah3;
+		h[4] += ah4;
+		h[5] += ah5;
+		h[6] += ah6;
+		h[7] += ah7;
+	}
+
+	/* Produce the final hash value (big-endian): */
+	for (i = 0, j = 0; i < 8; i++)
+	{
+		hash[j++] = (uint8_t) (h[i] >> 24);
+		hash[j++] = (uint8_t) (h[i] >> 16);
+		hash[j++] = (uint8_t) (h[i] >> 8);
+		hash[j++] = (uint8_t) h[i];
+	}
+}
+#else
+/* Modified by D. Monniaux */
+void calc_sha_256(uint8_t hash[32], const void * input, size_t len)
+{
+	/*
+	 * Note 1: All integers (expect indexes) are 32-bit unsigned integers and addition is calculated modulo 2^32.
+	 * Note 2: For each round, there is one round constant k[i] and one entry in the message schedule array w[i], 0 = i = 63
+	 * Note 3: The compression function uses 8 working variables, a through h
+	 * Note 4: Big-endian convention is used when expressing the constants in this pseudocode,
+	 *     and when parsing message block data from bytes to words, for example,
+	 *     the first word of the input message "abc" after padding is 0x61626380
+	 */
+
+	/*
+	 * Initialize hash values:
+	 * (first 32 bits of the fractional parts of the square roots of the first 8 primes 2..19):
+	 */
+	uint32_t h[] = { 0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a, 0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19 };
+	int i, j;
+
+	/* 512-bit chunks is what we will operate on. */
+	uint8_t chunk[64];
+
+	struct buffer_state state;
+
+	init_buf_state(&state, input, len);
+
+	while (calc_chunk(chunk, &state)) {
+	        uint32_t ah0, ah1, ah2, ah3, ah4, ah5, ah6, ah7;
+		
+		/*
+		 * create a 64-entry message schedule array w[0..63] of 32-bit words
+		 * (The initial values in w[0..63] don't matter, so many implementations zero them here)
+		 * copy chunk into first 16 words w[0..15] of the message schedule array
+		 */
+		uint32_t w[64];
+		const uint8_t *p = chunk;
+
+		memset(w, 0x00, sizeof w);
+		for (i = 0; i < 16; i++) {
+			w[i] = (uint32_t) p[0] << 24 | (uint32_t) p[1] << 16 |
+				(uint32_t) p[2] << 8 | (uint32_t) p[3];
+			p += 4;
+		}
+
+		/* Extend the first 16 words into the remaining 48 words w[16..63] of the message schedule array: */
+		for (i = 16; i < 64; i++) {
+			const uint32_t s0 = right_rot(w[i - 15], 7) ^ right_rot(w[i - 15], 18) ^ (w[i - 15] >> 3);
+			const uint32_t s1 = right_rot(w[i - 2], 17) ^ right_rot(w[i - 2], 19) ^ (w[i - 2] >> 10);
+			w[i] = w[i - 16] + s0 + w[i - 7] + s1;
+		}
+		
+		/* Initialize working variables to current hash value: */
+		ah0 = h[0];
+		ah1 = h[1];
+		ah2 = h[2];
+		ah3 = h[3];
+		ah4 = h[4];
+		ah5 = h[5];
+		ah6 = h[6];
+		ah7 = h[7];
+
+		/* Compression function main loop: */
+		for (i = 0; i < 64; ) {
+		  {
+			const uint32_t s1 = right_rot(ah4, 6) ^ right_rot(ah4, 11) ^ right_rot(ah4, 25);
+			const uint32_t ch = (ah4 & ah5) ^ (~ah4 & ah6);
+			const uint32_t temp1 = ah7 + s1 + ch + k[i] + w[i];
+			const uint32_t s0 = right_rot(ah0, 2) ^ right_rot(ah0, 13) ^ right_rot(ah0, 22);
+			const uint32_t maj = (ah0 & ah1) ^ (ah0 & ah2) ^ (ah1 & ah2);
+			const uint32_t temp2 = s0 + maj;
+
+			ah7 = ah6;
+			ah6 = ah5;
+			ah5 = ah4;
+			ah4 = ah3 + temp1;
+			ah3 = ah2;
+			ah2 = ah1;
+			ah1 = ah0;
+			ah0 = temp1 + temp2;
+			i++;
+		  }
+		  {
+			const uint32_t s1 = right_rot(ah4, 6) ^ right_rot(ah4, 11) ^ right_rot(ah4, 25);
+			const uint32_t ch = (ah4 & ah5) ^ (~ah4 & ah6);
+			const uint32_t temp1 = ah7 + s1 + ch + k[i] + w[i];
+			const uint32_t s0 = right_rot(ah0, 2) ^ right_rot(ah0, 13) ^ right_rot(ah0, 22);
+			const uint32_t maj = (ah0 & ah1) ^ (ah0 & ah2) ^ (ah1 & ah2);
+			const uint32_t temp2 = s0 + maj;
+
+			ah7 = ah6;
+			ah6 = ah5;
+			ah5 = ah4;
+			ah4 = ah3 + temp1;
+			ah3 = ah2;
+			ah2 = ah1;
+			ah1 = ah0;
+			ah0 = temp1 + temp2;
+			i++;
+		  }
+		  {
+			const uint32_t s1 = right_rot(ah4, 6) ^ right_rot(ah4, 11) ^ right_rot(ah4, 25);
+			const uint32_t ch = (ah4 & ah5) ^ (~ah4 & ah6);
+			const uint32_t temp1 = ah7 + s1 + ch + k[i] + w[i];
+			const uint32_t s0 = right_rot(ah0, 2) ^ right_rot(ah0, 13) ^ right_rot(ah0, 22);
+			const uint32_t maj = (ah0 & ah1) ^ (ah0 & ah2) ^ (ah1 & ah2);
+			const uint32_t temp2 = s0 + maj;
+
+			ah7 = ah6;
+			ah6 = ah5;
+			ah5 = ah4;
+			ah4 = ah3 + temp1;
+			ah3 = ah2;
+			ah2 = ah1;
+			ah1 = ah0;
+			ah0 = temp1 + temp2;
+			i++;
+		  }
+		  {
+			const uint32_t s1 = right_rot(ah4, 6) ^ right_rot(ah4, 11) ^ right_rot(ah4, 25);
+			const uint32_t ch = (ah4 & ah5) ^ (~ah4 & ah6);
+			const uint32_t temp1 = ah7 + s1 + ch + k[i] + w[i];
+			const uint32_t s0 = right_rot(ah0, 2) ^ right_rot(ah0, 13) ^ right_rot(ah0, 22);
+			const uint32_t maj = (ah0 & ah1) ^ (ah0 & ah2) ^ (ah1 & ah2);
+			const uint32_t temp2 = s0 + maj;
+
+			ah7 = ah6;
+			ah6 = ah5;
+			ah5 = ah4;
+			ah4 = ah3 + temp1;
+			ah3 = ah2;
+			ah2 = ah1;
+			ah1 = ah0;
+			ah0 = temp1 + temp2;
+			i++;
+		  }
+		  {
+			const uint32_t s1 = right_rot(ah4, 6) ^ right_rot(ah4, 11) ^ right_rot(ah4, 25);
+			const uint32_t ch = (ah4 & ah5) ^ (~ah4 & ah6);
+			const uint32_t temp1 = ah7 + s1 + ch + k[i] + w[i];
+			const uint32_t s0 = right_rot(ah0, 2) ^ right_rot(ah0, 13) ^ right_rot(ah0, 22);
+			const uint32_t maj = (ah0 & ah1) ^ (ah0 & ah2) ^ (ah1 & ah2);
+			const uint32_t temp2 = s0 + maj;
+
+			ah7 = ah6;
+			ah6 = ah5;
+			ah5 = ah4;
+			ah4 = ah3 + temp1;
+			ah3 = ah2;
+			ah2 = ah1;
+			ah1 = ah0;
+			ah0 = temp1 + temp2;
+			i++;
+		  }
+		  {
+			const uint32_t s1 = right_rot(ah4, 6) ^ right_rot(ah4, 11) ^ right_rot(ah4, 25);
+			const uint32_t ch = (ah4 & ah5) ^ (~ah4 & ah6);
+			const uint32_t temp1 = ah7 + s1 + ch + k[i] + w[i];
+			const uint32_t s0 = right_rot(ah0, 2) ^ right_rot(ah0, 13) ^ right_rot(ah0, 22);
+			const uint32_t maj = (ah0 & ah1) ^ (ah0 & ah2) ^ (ah1 & ah2);
+			const uint32_t temp2 = s0 + maj;
+
+			ah7 = ah6;
+			ah6 = ah5;
+			ah5 = ah4;
+			ah4 = ah3 + temp1;
+			ah3 = ah2;
+			ah2 = ah1;
+			ah1 = ah0;
+			ah0 = temp1 + temp2;
+			i++;
+		  }
+		  {
+			const uint32_t s1 = right_rot(ah4, 6) ^ right_rot(ah4, 11) ^ right_rot(ah4, 25);
+			const uint32_t ch = (ah4 & ah5) ^ (~ah4 & ah6);
+			const uint32_t temp1 = ah7 + s1 + ch + k[i] + w[i];
+			const uint32_t s0 = right_rot(ah0, 2) ^ right_rot(ah0, 13) ^ right_rot(ah0, 22);
+			const uint32_t maj = (ah0 & ah1) ^ (ah0 & ah2) ^ (ah1 & ah2);
+			const uint32_t temp2 = s0 + maj;
+
+			ah7 = ah6;
+			ah6 = ah5;
+			ah5 = ah4;
+			ah4 = ah3 + temp1;
+			ah3 = ah2;
+			ah2 = ah1;
+			ah1 = ah0;
+			ah0 = temp1 + temp2;
+			i++;
+		  }
+		  {
+			const uint32_t s1 = right_rot(ah4, 6) ^ right_rot(ah4, 11) ^ right_rot(ah4, 25);
+			const uint32_t ch = (ah4 & ah5) ^ (~ah4 & ah6);
+			const uint32_t temp1 = ah7 + s1 + ch + k[i] + w[i];
+			const uint32_t s0 = right_rot(ah0, 2) ^ right_rot(ah0, 13) ^ right_rot(ah0, 22);
+			const uint32_t maj = (ah0 & ah1) ^ (ah0 & ah2) ^ (ah1 & ah2);
+			const uint32_t temp2 = s0 + maj;
+
+			ah7 = ah6;
+			ah6 = ah5;
+			ah5 = ah4;
+			ah4 = ah3 + temp1;
+			ah3 = ah2;
+			ah2 = ah1;
+			ah1 = ah0;
+			ah0 = temp1 + temp2;
+			i++;
+		  }
+		}
+
+		/* Add the compressed chunk to the current hash value: */
+		h[0] += ah0;
+		h[1] += ah1;
+		h[2] += ah2;
+		h[3] += ah3;
+		h[4] += ah4;
+		h[5] += ah5;
+		h[6] += ah6;
+		h[7] += ah7;
+	}
+
+	/* Produce the final hash value (big-endian): */
+	for (i = 0, j = 0; i < 8; i++)
+	{
+		hash[j++] = (uint8_t) (h[i] >> 24);
+		hash[j++] = (uint8_t) (h[i] >> 16);
+		hash[j++] = (uint8_t) (h[i] >> 8);
+		hash[j++] = (uint8_t) h[i];
+	}
+}
+#endif
+#endif
diff --git a/test/monniaux/sha-2/sha-256_run.c b/test/monniaux/sha-2/sha-256_run.c
index 5b5031c3..546b7dbc 100644
--- a/test/monniaux/sha-2/sha-256_run.c
+++ b/test/monniaux/sha-2/sha-256_run.c
@@ -2,7 +2,8 @@
 #include <stdio.h>
 #include <string.h>
 #include <stdlib.h>
-
+#include <inttypes.h>
+#include "../cycles.h"
 #include "sha-256.h"
 
 struct string_vector {
@@ -42,7 +43,8 @@ static const struct string_vector STRING_VECTORS[] = {
 	}
 };
 
-#define LARGE_MESSAGES 1
+#define LARGE_MESSAGES 0
+#define LARGER_MESSAGES 0
 
 static uint8_t data1[] = { 0xbd };
 static uint8_t data2[] = { 0xc9, 0x8c, 0x8e, 0x55 };
@@ -109,14 +111,14 @@ static struct vector vectors[] = {
 		data9,
 		sizeof data9,
 		"f4d62ddec0f3dd90ea1380fa16a5ff8dc4c54b21740650f24afc4120903552b0"
-	}
+	},
 #if LARGE_MESSAGES
-	,
 	{
 		NULL,
 		1000000,
 		"d29751f2649b32ff572b5e0a9f541ea660a50f94ff0beedfb0b692b924cc8025"
 	},
+#if LARGER_MESSAGES
 	{
 		NULL,
 		SIZEOF_DATA11,
@@ -133,21 +135,34 @@ static struct vector vectors[] = {
 		"c23ce8a7895f4b21ec0daf37920ac0a262a220045a03eb2dfed48ef9b05aabea"
 	}
 #endif
+#endif
 };
 
+#if LARGE_MESSAGES
+static void *my_malloc(size_t size) {
+  void *p=malloc(size);
+  if (p==0) {
+    fprintf(stderr, "malloc(%zu) failed\n", size);
+    abort();
+  }
+  return p;
+}
+#endif
+
 static void construct_binary_messages(void)
 {
 	memset(data7, 0x00, sizeof data7);
 	memset(data8, 0x41, sizeof data8);
 	memset(data9, 0x55, sizeof data9);
 #if LARGE_MESSAGES
+#if LARGER_MESSAGES
 	/*
 	 * Heap allocation as a workaround for some linkers not liking
 	 * large BSS segments.
 	 */
-	data11 = malloc(SIZEOF_DATA11);
-	data12 = malloc(SIZEOF_DATA12);
-	data13 = malloc(SIZEOF_DATA13);
+	data11 = my_malloc(SIZEOF_DATA11);
+	data12 = my_malloc(SIZEOF_DATA12);
+	data13 = my_malloc(SIZEOF_DATA13);
 	memset(data11, 0x5a, SIZEOF_DATA11);
 	memset(data12, 0x00, SIZEOF_DATA12);
 	memset(data13, 0x42, SIZEOF_DATA13);
@@ -155,15 +170,23 @@ static void construct_binary_messages(void)
 	vectors[10].input = data11;
 	vectors[11].input = data12;
 	vectors[12].input = data13;
+#else
+	vectors[9].input = data12 = my_malloc(vectors[9].input_len);
+	memset(data12, 0x00, vectors[9].input_len);
+#endif
 #endif
 }
 
 static void destruct_binary_messages(void)
 {
 #if LARGE_MESSAGES
+#if LARGER_MESSAGES
 	free(data11);
 	free(data12);
 	free(data13);
+#else
+	free(data12);
+#endif
 #endif
 }
 
@@ -174,12 +197,26 @@ static void hash_to_string(char string[65], const uint8_t hash[32])
 		string += sprintf(string, "%02x", hash[i]);
 	}
 }	
-	
+
+static cycle_t cycle_total, cycle_start_time;
+
+static void cycle_count_start(void) {
+  cycle_start_time=get_cycle();
+}
+
+static void cycle_count_end(void) {
+  cycle_total += get_cycle()-cycle_start_time;
+}
+
 static int string_test(const char input[], const char output[])
 {
 	uint8_t hash[32];
 	char hash_string[65];
+
+	cycle_count_start();
 	calc_sha_256(hash, input, strlen(input));
+	cycle_count_end();
+	
 	hash_to_string(hash_string, hash);
 	printf("input: %s\n", input);
 	printf("hash : %s\n", hash_string);
@@ -203,7 +240,11 @@ static int test(const uint8_t * input, size_t input_len, const char output[])
 {
 	uint8_t hash[32];
 	char hash_string[65];
+
+	cycle_count_start();
 	calc_sha_256(hash, input, input_len);
+	cycle_count_end();
+
 	hash_to_string(hash_string, hash);
 	printf("input starts with 0x%02x, length %lu\n", *input, (unsigned long) input_len);
 	printf("hash : %s\n", hash_string);
@@ -218,6 +259,7 @@ static int test(const uint8_t * input, size_t input_len, const char output[])
 
 int main(void)
 {
+        cycle_count_config();
 	size_t i;
 	for (i = 0; i < (sizeof STRING_VECTORS / sizeof (struct string_vector)); i++) {
 		const struct string_vector *vector = &STRING_VECTORS[i];
@@ -234,5 +276,6 @@ int main(void)
 		}
 	}
 	destruct_binary_messages();
+	printf("total cycles = %" PRIu64 "\n", cycle_total);
 	return 0;
 }