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

7 files changed, 1109 insertions, 0 deletions

diff --git a/test/monniaux/heapsort/Makefile b/test/monniaux/heapsort/Makefile
new file mode 100644
index 00000000..69f0c3ca
--- /dev/null
+++ b/test/monniaux/heapsort/Makefile
@@ -0,0 +1,3 @@
+TARGET=heapsort
+
+include ../rules.mk
diff --git a/test/monniaux/heapsort/heapsort.c b/test/monniaux/heapsort/heapsort.c
new file mode 100644
index 00000000..550eff4d
--- /dev/null
+++ b/test/monniaux/heapsort/heapsort.c
@@ -0,0 +1,58 @@
+#include "heapsort.h"
+
+/* Rosetta Code */
+static inline int max (data *a, int n, int i, int j, int k) {
+    int m = i;
+    if (j < n && a[j] > a[m]) {
+        m = j;
+    }
+    if (k < n && a[k] > a[m]) {
+        m = k;
+    }
+    return m;
+}
+ 
+static void downheap (data *a, int n, int i) {
+    while (1) {
+        int j = max(a, n, i, 2 * i + 1, 2 * i + 2);
+        if (j == i) {
+            break;
+        }
+        data t = a[i];
+        a[i] = a[j];
+        a[j] = t;
+        i = j;
+    }
+}
+ 
+void heapsort (data *a, int n) {
+    int i;
+    for (i = (n - 2) / 2; i >= 0; i--) {
+        downheap(a, n, i);
+    }
+    for (i = 0; i < n; i++) {
+        data t = a[n - i - 1];
+        a[n - i - 1] = a[0];
+        a[0] = t;
+        downheap(a, n - i - 1, 0);
+    }
+}
+
+data data_random(void) {
+  static uint64_t next = 1325997111;
+  next = next * 1103515249 + 12345;
+  return next;
+}
+
+void data_vec_random(data *a, unsigned len) {
+  for(unsigned i=0; i<len; i++) {
+    a[i] = data_random();
+  }
+}
+
+bool data_vec_is_sorted(const data *a, unsigned len) {
+  for(unsigned i=0; i<len-1; i++) {
+    if (a[i] > a[i+1]) return false;
+  }
+  return true;
+}
diff --git a/test/monniaux/heapsort/heapsort.ccomp.k1c.s.modified5 b/test/monniaux/heapsort/heapsort.ccomp.k1c.s.modified5
new file mode 100644
index 00000000..9263169b
--- /dev/null
+++ b/test/monniaux/heapsort/heapsort.ccomp.k1c.s.modified5
@@ -0,0 +1,333 @@
+# File generated by CompCert 3.4
+# Command line: -Wall -O3 -S heapsort.c -o heapsort.ccomp.k1c.s
+	.text
+	.balign 2
+downheap:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -16
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+.L100:
+	sllw	$r3 = $r2, 1
+	addd	$r4 = $r2, 0
+;;
+	addw	$r5 = $r3, 1
+	addw	$r3 = $r3, 2
+;;
+	compw.ge	$r32 = $r5, $r1
+;;
+	cb.wnez	$r32?.L101
+;;
+	sxwd	$r11 = $r5
+	sxwd	$r43 = $r4
+;;
+	ld.xs	$r7 = $r11[$r0]
+;;
+	ld.xs	$r35 = $r43[$r0]
+;;
+	compd.leu	$r32 = $r7, $r35
+;;
+	cmoved.weqz $r32? $r4 = $r5
+.L101:
+	compw.ge	$r32 = $r3, $r1
+;;
+	cb.wnez	$r32?.L102
+;;
+	sxwd	$r10 = $r3
+	sxwd	$r34 = $r4
+;;
+	ld.xs	$r45 = $r10[$r0]
+;;
+	ld.xs	$r44 = $r34[$r0]
+;;
+	compd.leu	$r32 = $r45, $r44
+;;
+	cb.wnez	$r32?.L102
+;;
+	addd	$r4 = $r3, 0
+;;
+.L102:
+	compw.eq	$r32 = $r4, $r2
+;;
+	cb.wnez	$r32?.L103
+;;
+	sxwd	$r46 = $r2
+	sxwd	$r6 = $r4
+	addd	$r2 = $r4, 0
+;;
+	ld.xs	$r33 = $r6[$r0]
+;;
+	ld.xs	$r42 = $r46[$r0]
+;;
+	sd.xs	$r46[$r0] = $r33
+;;
+	sd.xs	$r6[$r0] = $r42
+	goto	.L100
+;;
+.L103:
+;;
+	ld	$r16 = 8[$r12]
+;;
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 16
+;;
+	ret	
+;;
+	.type	downheap, @function
+	.size	downheap, . - downheap
+	.text
+	.balign 2
+	.globl heapsort
+heapsort:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -48
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+	sd	16[$r12] = $r18
+;;
+	sd	24[$r12] = $r19
+	addd	$r19 = $r1, 0
+;;
+	addw	$r6 = $r19, 4294967294
+;;
+	sraw	$r32 = $r6, 31
+;;
+	sd	32[$r12] = $r20
+	addd	$r20 = $r0, 0
+	srlw	$r32 = $r32, 31
+;;
+	addw	$r32 = $r6, $r32
+;;
+	sraw	$r18 = $r32, 1
+;;
+.L104:
+	cb.wltz	$r18?.L105
+;;
+	addd	$r2 = $r18, 0
+	addd	$r1 = $r19, 0
+	addd	$r0 = $r20, 0
+	call	downheap
+;;
+	addw	$r18 = $r18, 4294967295
+	goto	.L104
+;;
+.L105:
+	make	$r18, 0
+;;
+.L106:
+	compw.ge	$r32 = $r18, $r19
+;;
+	cb.wnez	$r32?.L107
+;;
+	sbfw	$r3 = $r18, $r19
+	ld	$r4 = 0[$r20]
+;;
+	addw	$r1 = $r3, 4294967295
+;;
+	sxwd	$r7 = $r1
+;;
+	make	$r2, 0
+	ld.xs	$r9 = $r7[$r20]
+;;
+	sd	0[$r0] = $r4
+	addd	$r0 = $r20, 0
+;;
+	sd	0[$r20] = $r9
+	call	downheap
+;;
+	addw	$r18 = $r18, 1
+	goto	.L106
+;;
+.L107:
+	ld	$r16 = 8[$r12]
+;;
+	ld	$r18 = 16[$r12]
+;;
+	ld	$r19 = 24[$r12]
+;;
+	ld	$r20 = 32[$r12]
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 48
+;;
+	ret	
+;;
+	.type	heapsort, @function
+	.size	heapsort, . - heapsort
+	.data
+	.balign 8
+next:
+	.long	0x4f091c37, 0x0
+	.type	next, @object
+	.size	next, . - next
+	.text
+	.balign 2
+	.globl data_random
+data_random:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -16
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+	make	$r32 = next
+	make	$r0, 1103515249
+;;
+	ld	$r1 = 0[$r32]
+	make	$r32 = next
+;;
+	muld	$r63 = $r1, $r0
+;;
+	addd	$r0 = $r63, 12345
+;;
+	sd	0[$r32] = $r0
+;;
+	ld	$r16 = 8[$r12]
+;;
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 16
+;;
+	ret	
+;;
+	.type	data_random, @function
+	.size	data_random, . - data_random
+	.text
+	.balign 2
+	.globl data_vec_random
+data_vec_random:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -48
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+	sd	16[$r12] = $r18
+	addd	$r18 = $r1, 0
+;;
+	sd	24[$r12] = $r19
+	addd	$r19 = $r0, 0
+;;
+	sd	32[$r12] = $r20
+	make	$r20, 0
+;;
+.L108:
+	compw.geu	$r32 = $r20, $r18
+;;
+	cb.wnez	$r32?.L109
+;;
+	call	data_random
+;;
+	addd	$r1 = $r20, 0
+	addw	$r20 = $r20, 1
+;;
+	zxwd	$r1 = $r1
+;;
+	slld	$r2 = $r1, 3
+;;
+	addd	$r3 = $r19, $r2
+;;
+	sd	0[$r3] = $r0
+	goto	.L108
+;;
+.L109:
+	ld	$r16 = 8[$r12]
+;;
+	ld	$r18 = 16[$r12]
+;;
+	ld	$r19 = 24[$r12]
+;;
+	ld	$r20 = 32[$r12]
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 48
+;;
+	ret	
+;;
+	.type	data_vec_random, @function
+	.size	data_vec_random, . - data_vec_random
+	.text
+	.balign 2
+	.globl data_vec_is_sorted
+data_vec_is_sorted:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -16
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+	make	$r2, 0
+;;
+.L110:
+	addw	$r6 = $r1, 4294967295
+;;
+	compw.geu	$r32 = $r2, $r6
+;;
+	cb.wnez	$r32?.L111
+;;
+	addd	$r3 = $r2, 0
+	addw	$r2 = $r2, 1
+;;
+	zxwd	$r3 = $r3
+;;
+	slld	$r5 = $r3, 3
+	addd	$r3 = $r2, 0
+;;
+	addd	$r10 = $r0, $r5
+	zxwd	$r3 = $r3
+;;
+	slld	$r8 = $r3, 3
+;;
+	addd	$r3 = $r0, $r8
+;;
+	ld	$r4 = 0[$r10]
+;;
+	ld	$r9 = 0[$r3]
+;;
+	compd.leu	$r32 = $r4, $r9
+;;
+	cb.wnez	$r32?.L110
+;;
+	make	$r0, 0
+	goto	.L112
+;;
+.L111:
+	make	$r0, 1
+;;
+.L112:
+;;
+	ld	$r16 = 8[$r12]
+;;
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 16
+;;
+	ret	
+;;
+	.type	data_vec_is_sorted, @function
+	.size	data_vec_is_sorted, . - data_vec_is_sorted
diff --git a/test/monniaux/heapsort/heapsort.ccomp.k1c.s.modified7 b/test/monniaux/heapsort/heapsort.ccomp.k1c.s.modified7
new file mode 100644
index 00000000..4d6a12de
--- /dev/null
+++ b/test/monniaux/heapsort/heapsort.ccomp.k1c.s.modified7
@@ -0,0 +1,328 @@
+# File generated by CompCert 3.4
+# Command line: -Wall -O3 -S heapsort.c -o heapsort.ccomp.k1c.s
+	.text
+	.balign 2
+downheap:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -16
+;;
+	sd	0[$r12] = $r14
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+.L100:
+	sllw	$r3 = $r2, 1
+	addd	$r4 = $r2, 0
+;;
+	addw	$r5 = $r3, 1
+	addw	$r3 = $r3, 2
+;;
+	compw.ge	$r32 = $r5, $r1
+;;
+	cb.wnez	$r32?.L101
+;;
+	sxwd	$r11 = $r5
+	sxwd	$r43 = $r4
+;;
+	ld.xs	$r7 = $r11[$r0]
+;;
+	ld.xs	$r35 = $r43[$r0]
+;;
+	compd.leu	$r32 = $r7, $r35
+;;
+	cmoved.weqz $r32? $r4 = $r5
+;;
+.L101:
+	compw.ge	$r32 = $r3, $r1
+;;
+	cb.wnez	$r32?.L102
+;;
+	sxwd	$r10 = $r3
+	sxwd	$r34 = $r4
+;;
+	ld.xs	$r45 = $r10[$r0]
+;;
+	ld.xs	$r44 = $r34[$r0]
+;;
+	compd.leu	$r32 = $r45, $r44
+;;
+	cmoved.weqz	$r32? $r4=$r3
+;; 
+.L102:
+	compw.eq	$r32 = $r4, $r2
+;;
+	cb.wnez	$r32?.L103
+;;
+	sxwd	$r46 = $r2
+	sxwd	$r6 = $r4
+	addd	$r2 = $r4, 0
+;;
+	ld.xs	$r33 = $r6[$r0]
+;;
+	ld.xs	$r42 = $r46[$r0]
+;;
+	sd.xs	$r46[$r0] = $r33
+;;
+	sd.xs	$r6[$r0] = $r42
+	goto	.L100
+;;
+.L103:
+;;
+	ld	$r16 = 8[$r12]
+;;
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 16
+;;
+	ret	
+;;
+	.type	downheap, @function
+	.size	downheap, . - downheap
+	.text
+	.balign 2
+	.globl heapsort
+heapsort:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -48
+;;
+	sd	0[$r12] = $r14
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+	sd	16[$r12] = $r18
+;;
+	sd	24[$r12] = $r19
+	addd	$r19 = $r1, 0
+;;
+	addw	$r6 = $r19, 4294967294
+;;
+	sraw	$r32 = $r6, 31
+;;
+	sd	32[$r12] = $r20
+	addd	$r20 = $r0, 0
+	srlw	$r32 = $r32, 31
+;;
+	addw	$r32 = $r6, $r32
+;;
+	sraw	$r18 = $r32, 1
+;;
+.L104:
+	cb.wltz	$r18?.L105
+;;
+	addd	$r2 = $r18, 0
+	addd	$r1 = $r19, 0
+	addd	$r0 = $r20, 0
+	call	downheap
+;;
+	addw	$r18 = $r18, 4294967295
+	goto	.L104
+;;
+.L105:
+	make	$r18, 0
+;;
+.L106:
+	compw.ge	$r32 = $r18, $r19
+;;
+	cb.wnez	$r32?.L107
+;;
+	sbfw	$r3 = $r18, $r19
+	ld	$r4 = 0[$r20]
+;;
+	addw	$r1 = $r3, 4294967295
+;;
+	sxwd	$r7 = $r1
+;;
+	make	$r2, 0
+	ld.xs	$r9 = $r7[$r20]
+;;
+	sd	0[$r0] = $r4
+	addd	$r0 = $r20, 0
+;;
+	sd	0[$r20] = $r9
+	call	downheap
+;;
+	addw	$r18 = $r18, 1
+	goto	.L106
+;;
+.L107:
+	ld	$r16 = 8[$r12]
+;;
+	ld	$r18 = 16[$r12]
+;;
+	ld	$r19 = 24[$r12]
+;;
+	ld	$r20 = 32[$r12]
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 48
+;;
+	ret	
+;;
+	.type	heapsort, @function
+	.size	heapsort, . - heapsort
+	.data
+	.balign 8
+next:
+	.long	0x4f091c37, 0x0
+	.type	next, @object
+	.size	next, . - next
+	.text
+	.balign 2
+	.globl data_random
+data_random:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -16
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+	make	$r32 = next
+	make	$r0, 1103515249
+;;
+	ld	$r1 = 0[$r32]
+	make	$r32 = next
+;;
+	muld	$r63 = $r1, $r0
+;;
+	addd	$r0 = $r63, 12345
+;;
+	sd	0[$r32] = $r0
+;;
+	ld	$r16 = 8[$r12]
+;;
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 16
+;;
+	ret	
+;;
+	.type	data_random, @function
+	.size	data_random, . - data_random
+	.text
+	.balign 2
+	.globl data_vec_random
+data_vec_random:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -48
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+	sd	16[$r12] = $r18
+	addd	$r18 = $r1, 0
+;;
+	sd	24[$r12] = $r19
+	addd	$r19 = $r0, 0
+;;
+	sd	32[$r12] = $r20
+	make	$r20, 0
+;;
+.L108:
+	compw.geu	$r32 = $r20, $r18
+;;
+	cb.wnez	$r32?.L109
+;;
+	call	data_random
+;;
+	addd	$r1 = $r20, 0
+	addw	$r20 = $r20, 1
+;;
+	zxwd	$r1 = $r1
+;;
+	slld	$r2 = $r1, 3
+;;
+	addd	$r3 = $r19, $r2
+;;
+	sd	0[$r3] = $r0
+	goto	.L108
+;;
+.L109:
+	ld	$r16 = 8[$r12]
+;;
+	ld	$r18 = 16[$r12]
+;;
+	ld	$r19 = 24[$r12]
+;;
+	ld	$r20 = 32[$r12]
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 48
+;;
+	ret	
+;;
+	.type	data_vec_random, @function
+	.size	data_vec_random, . - data_vec_random
+	.text
+	.balign 2
+	.globl data_vec_is_sorted
+data_vec_is_sorted:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -16
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+	make	$r2, 0
+;;
+.L110:
+	addw	$r6 = $r1, 4294967295
+;;
+	compw.geu	$r32 = $r2, $r6
+;;
+	cb.wnez	$r32?.L111
+;;
+	addd	$r3 = $r2, 0
+	addw	$r2 = $r2, 1
+;;
+	zxwd	$r3 = $r3
+;;
+	slld	$r5 = $r3, 3
+	addd	$r3 = $r2, 0
+;;
+	addd	$r10 = $r0, $r5
+	zxwd	$r3 = $r3
+;;
+	slld	$r8 = $r3, 3
+;;
+	addd	$r3 = $r0, $r8
+;;
+	ld	$r4 = 0[$r10]
+;;
+	ld	$r9 = 0[$r3]
+;;
+	compd.leu	$r32 = $r4, $r9
+;;
+	cb.wnez	$r32?.L110
+;;
+	make	$r0, 0
+	goto	.L112
+;;
+.L111:
+	make	$r0, 1
+;;
+.L112:
+;;
+	ld	$r16 = 8[$r12]
+;;
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 16
+;;
+	ret	
+;;
+	.type	data_vec_is_sorted, @function
+	.size	data_vec_is_sorted, . - data_vec_is_sorted
diff --git a/test/monniaux/heapsort/heapsort.ccomp.k1c.s.orig b/test/monniaux/heapsort/heapsort.ccomp.k1c.s.orig
new file mode 100644
index 00000000..3dc370b8
--- /dev/null
+++ b/test/monniaux/heapsort/heapsort.ccomp.k1c.s.orig
@@ -0,0 +1,358 @@
+# File generated by CompCert 3.4
+# Command line: -Wall -O3 -S heapsort.c -o heapsort.ccomp.k1c.s
+	.text
+	.balign 2
+downheap:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -16
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+.L100:
+	sllw	$r3 = $r2, 1
+	addd	$r4 = $r2, 0
+;;
+	addw	$r5 = $r3, 1
+	addw	$r3 = $r3, 2
+;;
+	compw.ge	$r32 = $r5, $r1
+;;
+	cb.wnez	$r32?.L101
+;;
+	sxwd	$r11 = $r5
+	sxwd	$r43 = $r4
+;;
+	slld	$r38 = $r11, 3
+	slld	$r37 = $r43, 3
+;;
+	addd	$r8 = $r0, $r38
+	addd	$r40 = $r0, $r37
+;;
+	ld	$r7 = 0[$r8]
+;;
+	ld	$r35 = 0[$r40]
+;;
+	compd.leu	$r32 = $r7, $r35
+;;
+	cb.wnez	$r32?.L101
+;;
+	addd	$r4 = $r5, 0
+;;
+.L101:
+	compw.ge	$r32 = $r3, $r1
+;;
+	cb.wnez	$r32?.L102
+;;
+	sxwd	$r10 = $r3
+	sxwd	$r34 = $r4
+;;
+	slld	$r17 = $r10, 3
+	slld	$r9 = $r34, 3
+;;
+	addd	$r36 = $r0, $r17
+	addd	$r47 = $r0, $r9
+;;
+	ld	$r45 = 0[$r36]
+;;
+	ld	$r44 = 0[$r47]
+;;
+	compd.leu	$r32 = $r45, $r44
+;;
+	cb.wnez	$r32?.L102
+;;
+	addd	$r4 = $r3, 0
+;;
+.L102:
+	compw.eq	$r32 = $r4, $r2
+;;
+	cb.wnez	$r32?.L103
+;;
+	sxwd	$r46 = $r2
+	sxwd	$r6 = $r4
+	addd	$r2 = $r4, 0
+;;
+	slld	$r41 = $r46, 3
+	slld	$r39 = $r6, 3
+;;
+	addd	$r5 = $r0, $r41
+	addd	$r3 = $r0, $r39
+;;
+	ld	$r33 = 0[$r3]
+;;
+	ld	$r42 = 0[$r5]
+;;
+	sd	0[$r5] = $r33
+;;
+	sd	0[$r3] = $r42
+	goto	.L100
+;;
+.L103:
+;;
+	ld	$r16 = 8[$r12]
+;;
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 16
+;;
+	ret	
+;;
+	.type	downheap, @function
+	.size	downheap, . - downheap
+	.text
+	.balign 2
+	.globl heapsort
+heapsort:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -48
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+	sd	16[$r12] = $r18
+;;
+	sd	24[$r12] = $r19
+	addd	$r19 = $r1, 0
+;;
+	addw	$r6 = $r19, 4294967294
+;;
+	sraw	$r32 = $r6, 31
+;;
+	sd	32[$r12] = $r20
+	addd	$r20 = $r0, 0
+	srlw	$r32 = $r32, 31
+;;
+	addw	$r32 = $r6, $r32
+;;
+	sraw	$r18 = $r32, 1
+;;
+.L104:
+	cb.wltz	$r18?.L105
+;;
+	addd	$r2 = $r18, 0
+	addd	$r1 = $r19, 0
+	addd	$r0 = $r20, 0
+	call	downheap
+;;
+	addw	$r18 = $r18, 4294967295
+	goto	.L104
+;;
+.L105:
+	make	$r18, 0
+;;
+.L106:
+	compw.ge	$r32 = $r18, $r19
+;;
+	cb.wnez	$r32?.L107
+;;
+	sbfw	$r3 = $r18, $r19
+	ld	$r4 = 0[$r20]
+;;
+	addw	$r1 = $r3, 4294967295
+;;
+	sxwd	$r7 = $r1
+;;
+	slld	$r2 = $r7, 3
+;;
+	addd	$r0 = $r20, $r2
+	make	$r2, 0
+;;
+	ld	$r9 = 0[$r0]
+;;
+	sd	0[$r0] = $r4
+	addd	$r0 = $r20, 0
+;;
+	sd	0[$r20] = $r9
+	call	downheap
+;;
+	addw	$r18 = $r18, 1
+	goto	.L106
+;;
+.L107:
+	ld	$r16 = 8[$r12]
+;;
+	ld	$r18 = 16[$r12]
+;;
+	ld	$r19 = 24[$r12]
+;;
+	ld	$r20 = 32[$r12]
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 48
+;;
+	ret	
+;;
+	.type	heapsort, @function
+	.size	heapsort, . - heapsort
+	.data
+	.balign 8
+next:
+	.long	0x4f091c37, 0x0
+	.type	next, @object
+	.size	next, . - next
+	.text
+	.balign 2
+	.globl data_random
+data_random:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -16
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+	make	$r32 = next
+	make	$r0, 1103515249
+;;
+	ld	$r1 = 0[$r32]
+	make	$r32 = next
+;;
+	muld	$r63 = $r1, $r0
+;;
+	addd	$r0 = $r63, 12345
+;;
+	sd	0[$r32] = $r0
+;;
+	ld	$r16 = 8[$r12]
+;;
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 16
+;;
+	ret	
+;;
+	.type	data_random, @function
+	.size	data_random, . - data_random
+	.text
+	.balign 2
+	.globl data_vec_random
+data_vec_random:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -48
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+	sd	16[$r12] = $r18
+	addd	$r18 = $r1, 0
+;;
+	sd	24[$r12] = $r19
+	addd	$r19 = $r0, 0
+;;
+	sd	32[$r12] = $r20
+	make	$r20, 0
+;;
+.L108:
+	compw.geu	$r32 = $r20, $r18
+;;
+	cb.wnez	$r32?.L109
+;;
+	call	data_random
+;;
+	addd	$r1 = $r20, 0
+	addw	$r20 = $r20, 1
+;;
+	zxwd	$r1 = $r1
+;;
+	slld	$r2 = $r1, 3
+;;
+	addd	$r3 = $r19, $r2
+;;
+	sd	0[$r3] = $r0
+	goto	.L108
+;;
+.L109:
+	ld	$r16 = 8[$r12]
+;;
+	ld	$r18 = 16[$r12]
+;;
+	ld	$r19 = 24[$r12]
+;;
+	ld	$r20 = 32[$r12]
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 48
+;;
+	ret	
+;;
+	.type	data_vec_random, @function
+	.size	data_vec_random, . - data_vec_random
+	.text
+	.balign 2
+	.globl data_vec_is_sorted
+data_vec_is_sorted:
+	addd	$r14 = $r12, 0
+	addd	$r12 = $r12, -16
+;;
+	sd	0[$r12] = $r14
+;;
+;;
+	get	$r16 = $ra
+;;
+	sd	8[$r12] = $r16
+;;
+	make	$r2, 0
+;;
+.L110:
+	addw	$r6 = $r1, 4294967295
+;;
+	compw.geu	$r32 = $r2, $r6
+;;
+	cb.wnez	$r32?.L111
+;;
+	addd	$r3 = $r2, 0
+	addw	$r2 = $r2, 1
+;;
+	zxwd	$r3 = $r3
+;;
+	slld	$r5 = $r3, 3
+	addd	$r3 = $r2, 0
+;;
+	addd	$r10 = $r0, $r5
+	zxwd	$r3 = $r3
+;;
+	slld	$r8 = $r3, 3
+;;
+	addd	$r3 = $r0, $r8
+;;
+	ld	$r4 = 0[$r10]
+;;
+	ld	$r9 = 0[$r3]
+;;
+	compd.leu	$r32 = $r4, $r9
+;;
+	cb.wnez	$r32?.L110
+;;
+	make	$r0, 0
+	goto	.L112
+;;
+.L111:
+	make	$r0, 1
+;;
+.L112:
+;;
+	ld	$r16 = 8[$r12]
+;;
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 16
+;;
+	ret	
+;;
+	.type	data_vec_is_sorted, @function
+	.size	data_vec_is_sorted, . - data_vec_is_sorted
diff --git a/test/monniaux/heapsort/heapsort.h b/test/monniaux/heapsort/heapsort.h
new file mode 100644
index 00000000..247d6773
--- /dev/null
+++ b/test/monniaux/heapsort/heapsort.h
@@ -0,0 +1,7 @@
+#include <stdint.h>
+#include <stdbool.h>
+
+typedef uint64_t data;
+void heapsort(data *A, int len);
+void data_vec_random(data *a, unsigned len);
+bool data_vec_is_sorted(const data *a, unsigned len);
diff --git a/test/monniaux/heapsort/heapsort_run.c b/test/monniaux/heapsort/heapsort_run.c
new file mode 100644
index 00000000..8f2d3fe0
--- /dev/null
+++ b/test/monniaux/heapsort/heapsort_run.c
@@ -0,0 +1,22 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <inttypes.h>
+#include "heapsort.h"
+#include "../cycles.h"
+
+int main (void) {
+  cycle_count_config();
+  unsigned len=30000;
+  data *vec = malloc(sizeof(data) * len);
+  data_vec_random(vec, len);
+  cycle_t heapsort_time = get_cycle();
+  heapsort(vec, len);
+  heapsort_time = get_cycle() - heapsort_time;
+  printf("sorted=%s\n"
+	 "time cycles:%" PRIu64 "\n",
+	 data_vec_is_sorted(vec, len)?"true":"false",
+	 heapsort_time);
+  free(vec);
+  return 0;
+}
+