quicksort experiments

3 files changed, 587 insertions, 1 deletions

diff --git a/test/monniaux/quicksort/Makefile b/test/monniaux/quicksort/Makefile
index cb9c4761..e6e83210 100644
--- a/test/monniaux/quicksort/Makefile
+++ b/test/monniaux/quicksort/Makefile
@@ -1,6 +1,6 @@
 CFLAGS=-Wall -O3
 K1C_CC=k1-mbr-gcc
-K1C_CFLAGS=-Wall -O3 -std=c99
+K1C_CFLAGS=-Wall -std=c99 -O2
 K1C_CCOMP=../../../ccomp
 K1C_CCOMPFLAGS=-Wall -O3
 
diff --git a/test/monniaux/quicksort/quicksort.ccomp.k1c.s_modified5 b/test/monniaux/quicksort/quicksort.ccomp.k1c.s_modified5
new file mode 100644
index 00000000..8a9a75bb
--- /dev/null
+++ b/test/monniaux/quicksort/quicksort.ccomp.k1c.s_modified5
@@ -0,0 +1,285 @@
+# File generated by CompCert 3.4
+# Command line: -Wall -O3 -S quicksort.c -o quicksort.ccomp.k1c.s
+	.text
+	.balign 2
+	.globl quicksort
+quicksort:
+	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
+	make	$r32, 2
+;;
+	compw.lt	$r32 = $r18, $r32
+;;
+	sd	24[$r12] = $r19
+	addd	$r19 = $r0, 0
+;;
+	sd	32[$r12] = $r20
+;;
+	cb.wnez	$r32?.L100
+;;
+	sraw	$r32 = $r18, 31
+	make	$r20, 0
+	addw	$r38 = $r18, 4294967295
+;;
+	srlw	$r32 = $r32, 31
+;;
+	addw	$r32 = $r18, $r32
+;;
+	sraw	$r41 = $r32, 1
+;;
+	sxwd	$r5 = $r41
+;;
+	ld.xs	$r15 = $r5[$r19]
+;;
+.L101:
+	sxwd	$r6 = $r20
+;;
+	ld.xs	$r34 = $r6[$r19]
+;;
+	compd.geu	$r32 = $r34, $r15
+;;
+	cb.wnez	$r32?.L102
+;;
+	addw	$r20 = $r20, 1
+	goto	.L101
+;;
+.L102:
+	sxwd	$r17 = $r38
+;;
+	ld.xs	$r2 = $r17[$r19]
+;;
+	compd.leu	$r32 = $r2, $r15
+;;
+	cb.wnez	$r32?.L103
+;;
+	addw	$r38 = $r38, 4294967295
+	goto	.L102
+;;
+.L103:
+	compw.ge	$r32 = $r20, $r38
+;;
+	cb.wnez	$r32?.L104
+;;
+	sxwd	$r35 = $r20
+	addw	$r20 = $r20, 1
+	addw	$r38 = $r38, 4294967295
+;;
+	ld.xs	$r9 = $r35[$r19]
+;;
+	sd.xs	$r35[$r19] = $r2
+;;
+	sd.xs	$r17[$r19] = $r9
+	goto	.L101
+;;
+.L104:
+	addd	$r1 = $r20, 0
+	addd	$r0 = $r19, 0
+	call	quicksort
+;;
+	sxwd	$r11 = $r20
+	sbfw	$r1 = $r20, $r18
+	ld	$r16 = 8[$r12]
+;;
+	slld	$r33 = $r11, 3
+	ld	$r18 = 16[$r12]
+;;
+	addd	$r0 = $r19, $r33
+	ld	$r19 = 24[$r12]
+;;
+	ld	$r20 = 32[$r12]
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 48
+;;
+	goto	quicksort
+;;
+.L100:
+	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	quicksort, @function
+	.size	quicksort, . - quicksort
+	.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
+;;
+.L105:
+	compw.geu	$r32 = $r20, $r18
+;;
+	cb.wnez	$r32?.L106
+;;
+	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	.L105
+;;
+.L106:
+	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
+;;
+.L107:
+	addw	$r6 = $r1, 4294967295
+;;
+	compw.geu	$r32 = $r2, $r6
+;;
+	cb.wnez	$r32?.L108
+;;
+	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?.L107
+;;
+	make	$r0, 0
+	goto	.L109
+;;
+.L108:
+	make	$r0, 1
+;;
+.L109:
+;;
+	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/quicksort/quicksort.ccomp.k1c.s_orig b/test/monniaux/quicksort/quicksort.ccomp.k1c.s_orig
new file mode 100644
index 00000000..64c1e2bf
--- /dev/null
+++ b/test/monniaux/quicksort/quicksort.ccomp.k1c.s_orig
@@ -0,0 +1,301 @@
+# File generated by CompCert 3.4
+# Command line: -Wall -O3 -S quicksort.c -o quicksort.ccomp.k1c.s
+	.text
+	.balign 2
+	.globl quicksort
+quicksort:
+	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
+	make	$r32, 2
+;;
+	compw.lt	$r32 = $r18, $r32
+;;
+	sd	24[$r12] = $r19
+	addd	$r19 = $r0, 0
+;;
+	sd	32[$r12] = $r20
+;;
+	cb.wnez	$r32?.L100
+;;
+	sraw	$r32 = $r18, 31
+	make	$r20, 0
+	addw	$r38 = $r18, 4294967295
+;;
+	srlw	$r32 = $r32, 31
+;;
+	addw	$r32 = $r18, $r32
+;;
+	sraw	$r41 = $r32, 1
+;;
+	sxwd	$r5 = $r41
+;;
+	slld	$r7 = $r5, 3
+;;
+	addd	$r37 = $r19, $r7
+;;
+	ld	$r15 = 0[$r37]
+;;
+.L101:
+	sxwd	$r6 = $r20
+;;
+	slld	$r40 = $r6, 3
+;;
+	addd	$r4 = $r19, $r40
+;;
+	ld	$r34 = 0[$r4]
+;;
+	compd.geu	$r32 = $r34, $r15
+;;
+	cb.wnez	$r32?.L102
+;;
+	addw	$r20 = $r20, 1
+	goto	.L101
+;;
+.L102:
+	sxwd	$r17 = $r38
+;;
+	slld	$r39 = $r17, 3
+;;
+	addd	$r0 = $r19, $r39
+;;
+	ld	$r2 = 0[$r0]
+;;
+	compd.leu	$r32 = $r2, $r15
+;;
+	cb.wnez	$r32?.L103
+;;
+	addw	$r38 = $r38, 4294967295
+	goto	.L102
+;;
+.L103:
+	compw.ge	$r32 = $r20, $r38
+;;
+	cb.wnez	$r32?.L104
+;;
+	sxwd	$r35 = $r20
+	addw	$r20 = $r20, 1
+	addw	$r38 = $r38, 4294967295
+;;
+	slld	$r10 = $r35, 3
+;;
+	addd	$r1 = $r19, $r10
+;;
+	ld	$r9 = 0[$r1]
+;;
+	sd	0[$r1] = $r2
+;;
+	sd	0[$r0] = $r9
+	goto	.L101
+;;
+.L104:
+	addd	$r1 = $r20, 0
+	addd	$r0 = $r19, 0
+	call	quicksort
+;;
+	sxwd	$r11 = $r20
+	sbfw	$r1 = $r20, $r18
+	ld	$r16 = 8[$r12]
+;;
+	slld	$r33 = $r11, 3
+	ld	$r18 = 16[$r12]
+;;
+	addd	$r0 = $r19, $r33
+	ld	$r19 = 24[$r12]
+;;
+	ld	$r20 = 32[$r12]
+	set	$ra = $r16
+;;
+	addd	$r12 = $r12, 48
+;;
+	goto	quicksort
+;;
+.L100:
+	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	quicksort, @function
+	.size	quicksort, . - quicksort
+	.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
+;;
+.L105:
+	compw.geu	$r32 = $r20, $r18
+;;
+	cb.wnez	$r32?.L106
+;;
+	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	.L105
+;;
+.L106:
+	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
+;;
+.L107:
+	addw	$r6 = $r1, 4294967295
+;;
+	compw.geu	$r32 = $r2, $r6
+;;
+	cb.wnez	$r32?.L108
+;;
+	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?.L107
+;;
+	make	$r0, 0
+	goto	.L109
+;;
+.L108:
+	make	$r0, 1
+;;
+.L109:
+;;
+	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