diff options
author | Christopher Swenson <chris@caswenson.com> | 2015-02-27 14:55:49 +0800 |
---|---|---|
committer | Daniel Veillard <veillard@redhat.com> | 2015-02-27 14:55:49 +0800 |
commit | 9b987f8c98763ee569bde90b5268b43474ca106c (patch) | |
tree | b36ed38b87a33b0749f0b5d48cc5c29a9a81a670 | |
parent | 9b8512337d14c8ddf662fcb98b0135f225a1c489 (diff) | |
download | android_external_libxml2-9b987f8c98763ee569bde90b5268b43474ca106c.tar.gz android_external_libxml2-9b987f8c98763ee569bde90b5268b43474ca106c.tar.bz2 android_external_libxml2-9b987f8c98763ee569bde90b5268b43474ca106c.zip |
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.
-rw-r--r-- | timsort.h | 74 |
1 files changed, 39 insertions, 35 deletions
@@ -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; } |