Fix timsort invariant loop re: Envisage article

See http://envisage-project.eu/proving-android-java-and-python-sorting-algorithm-is-broken-and-how-to-fix-it/

We use a "runLen" array of size 128, so it should be nearly impossible
to have our implementation overflow.

But in any case, the fix is relatively simple -- checking two extra
conditions in the invariant calculation.

I also took this opportunity to remove some redundancy in the
left/right merge logic in the invariant loop.

1 files changed, 39 insertions, 35 deletions

diff --git a/timsort.h b/timsort.h
index efa3aab1..795f2721 100644
--- a/timsort.h
+++ b/timsort.h
@@ -392,62 +392,66 @@ static void TIM_SORT_MERGE(SORT_TYPE *dst, const TIM_SORT_RUN_T *stack, const in
 
 static int TIM_SORT_COLLAPSE(SORT_TYPE *dst, TIM_SORT_RUN_T *stack, int stack_curr, TEMP_STORAGE_T *store, const size_t size)
 {
-  while (1)
-  {
-    int64_t A, B, C;
+  while (1) {
+    int64_t A, B, C, D;
+    int ABC, BCD, BD, CD;
+
     /* if the stack only has one thing on it, we are done with the collapse */
-    if (stack_curr <= 1) break;
+    if (stack_curr <= 1) {
+      break;
+    }
+
     /* if this is the last merge, just do it */
-    if ((stack_curr == 2) &&
-        (stack[0].length + stack[1].length == (int64_t) size))
-    {
+    if ((stack_curr == 2) && (stack[0].length + stack[1].length == size)) {
       TIM_SORT_MERGE(dst, stack, stack_curr, store);
       stack[0].length += stack[1].length;
       stack_curr--;
       break;
     }
     /* check if the invariant is off for a stack of 2 elements */
-    else if ((stack_curr == 2) && (stack[0].length <= stack[1].length))
-    {
+    else if ((stack_curr == 2) && (stack[0].length <= stack[1].length)) {
       TIM_SORT_MERGE(dst, stack, stack_curr, store);
       stack[0].length += stack[1].length;
       stack_curr--;
       break;
-    }
-    else if (stack_curr == 2)
+    } else if (stack_curr == 2) {
       break;
+    }
 
-    A = stack[stack_curr - 3].length;
-    B = stack[stack_curr - 2].length;
-    C = stack[stack_curr - 1].length;
+    B = stack[stack_curr - 3].length;
+    C = stack[stack_curr - 2].length;
+    D = stack[stack_curr - 1].length;
 
-    /* check first invariant */
-    if (A <= B + C)
-    {
-      if (A < C)
-      {
-        TIM_SORT_MERGE(dst, stack, stack_curr - 1, store);
-        stack[stack_curr - 3].length += stack[stack_curr - 2].length;
-        stack[stack_curr - 2] = stack[stack_curr - 1];
-        stack_curr--;
-      }
-      else
-      {
-        TIM_SORT_MERGE(dst, stack, stack_curr, store);
-        stack[stack_curr - 2].length += stack[stack_curr - 1].length;
-        stack_curr--;
-      }
+    if (stack_curr >= 4) {
+      A = stack[stack_curr - 4].length;
+      ABC = (A <= B + C);
+    } else {
+      ABC = 0;
     }
-    /* check second invariant */
-    else if (B <= C)
-    {
+
+    BCD = (B <= C + D) || ABC;
+    CD = (C <= D);
+    BD = (B < D);
+
+    /* Both invariants are good */
+    if (!BCD && !CD) {
+      break;
+    }
+
+    /* left merge */
+    if (BCD && !CD) {
+      TIM_SORT_MERGE(dst, stack, stack_curr - 1, store);
+      stack[stack_curr - 3].length += stack[stack_curr - 2].length;
+      stack[stack_curr - 2] = stack[stack_curr - 1];
+      stack_curr--;
+    } else {
+      /* right merge */
       TIM_SORT_MERGE(dst, stack, stack_curr, store);
       stack[stack_curr - 2].length += stack[stack_curr - 1].length;
       stack_curr--;
     }
-    else
-      break;
   }
+
   return stack_curr;
 }