## Worst sorting algorithm I ever saw: proving it using KLEE

Kernighan/Pike's book "The Practice of Programming" has a nice exercise:

Exercise 2-4. Design and implement an algorithm that will sort an array of n integers
as slowly as possible. You have to play fair: the algorithm must make progress and
eventually terminate, and the implementation must not cheat with tricks like timewasting
loops. What is the complexity of your algorithm as a function of n?


The problem is in fact tricky, but I've seen solution once in a serious and big piece of code I've rewritten to C.

Here it is:

void swap_ints (int *a, int *b)
{
int tmp=*a;
*a=*b;
*b=tmp;
};

void weird_sort(int* array, size_t size)
{
for (int i=0; i<size; i++)
for (int j=0; j<size-1; j++)
if (array[j]>array[j+1])
swap_ints (array+j, array+j+1);
};


This is bubble sort went wrong, there are no has-been-swapped variable, so the author added another loop, just to be sure everything is sorted at the end.

Bubble sort has worst-case performance $O(n^2)$ and best-case $O(n)$, this one always requires $n^2$ steps.

The moral of the story: sometimes it's easier to observe inputs/outputs, then to comprehend the code.

Even worse, when I googled for "bubble sort", just to be sure I'm correct, I've found quite similar implementation, also without has-been-swapped variable:

/* Bubble sort code */

#include

int main()
{
int array[100], n, c, d, swap;

printf("Enter number of elements\n");
scanf("%d", &n);

printf("Enter %d integers\n", n);

for (c = 0; c < n; c++)
scanf("%d", &array[c]);

for (c = 0 ; c < ( n - 1 ); c++)
{
for (d = 0 ; d < n - c - 1; d++)
{
if (array[d] > array[d+1]) /* For decreasing order use < */
{
swap       = array[d];
array[d]   = array[d+1];
array[d+1] = swap;
}
}
}

printf("Sorted list in ascending order:\n");

for ( c = 0 ; c < n ; c++ )
printf("%d\n", array[c]);

return 0;
}


It's somewhat faster ($O(\frac{n^2}{2})$, if I'm correct), but still weird. I've found it on programmingsimplified.com website:

Let's hope this is some kind of prank and they are not serious about it.

### Proving it using KLEE

Despite the fact, it's so bad, it's still correct. Or is it? We can prove it using KLEE:

void swap_unsigned_chars (unsigned char *a, unsigned char *b)
{
unsigned char tmp=*a;
*a=*b;
*b=tmp;
};

void weird_sort(unsigned char* array, size_t size)
{
for (unsigned char i=0; i<size; i++)
for (unsigned char j=0; j<size-1; j++)
if (array[j]>array[j+1])
swap_unsigned_chars (array+j, array+j+1);
};

int main()
{
#define SIZE 6

unsigned char buf[SIZE];
klee_make_symbolic(buf, sizeof buf, "buf");

weird_sort(buf, SIZE);

// check it

for (unsigned char i=0; i<SIZE; i++)
for (unsigned char j=i+1; j<SIZE; j++)
if (buf[i]>buf[j])
klee_assert(0);
};


We're asking KLEE to find such a 6 bytes in buf[], so that the buf[] will not be sorted after weird_sort() call.

It's not possible:

klee@774a0f6e485f:~\$ time klee -libc=uclibc bad_sort.bc
KLEE: NOTE: Using klee-uclibc : /home/klee/klee_build/klee/Release+Debug+Asserts/lib/klee-uclibc.bca
KLEE: output directory is "/home/klee/klee-out-21"
Using STP solver backend
KLEE: WARNING: undefined reference to function: fcntl
KLEE: WARNING: undefined reference to function: fstat
KLEE: WARNING: undefined reference to function: ioctl
KLEE: WARNING: undefined reference to function: klee_assert
KLEE: WARNING: undefined reference to function: open
KLEE: WARNING: undefined reference to function: write
KLEE: WARNING ONCE: calling external: ioctl(0, 21505, 59516896)
KLEE: WARNING ONCE: calling __user_main with extra arguments.

KLEE: done: total instructions = 674686
KLEE: done: completed paths = 720
KLEE: done: generated tests = 720


KLEE can't find counterexample. Otherwise it would report (klee_assert() would be called):

KLEE: ERROR: /home/klee/bad_sort.c:32: failed external call: klee_assert


Unfortunately, I could only check it again 6-element array of bytes. And it took 2-3 minutes on my venerable Intel Xeon E3-1220 3.10GHz. So we can prove it's correct for all arrays of 1..6 elements of bytes.