[m-rev.] for post-commit review: fix mantis bug #367

[Peter Wang]

On Wed, 03 Dec 2014 18:20:15 +1100 (EST), "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> Fix Mantis bug #367.

Please avoid using only a bug number for commit summary.

> diff --git a/library/array.m b/library/array.m
> index f9cba24..be7fb8b 100644
> --- a/library/array.m
> +++ b/library/array.m
...
> @@ -2135,8 +2153,32 @@ array.binary_search(A, X, I) :-
>      array.binary_search(ordering, A, X, I).
>  
>  array.binary_search(Cmp, A, X, I) :-
> -    array.approx_binary_search(Cmp, A, X, I),
> -    A ^ elem(I) = X.
> +    Lo = 0,
> +    Hi = array.size(A) - 1,
> +    binary_search_loop(Cmp, A, X, Lo, Hi, I).
> +
> +:- pred binary_search_loop(comparison_func(T)::in, array(T)::array_ui,
> +    T::in, int::in, int::in, int::out) is semidet.
> +
> +binary_search_loop(Cmp, A, X, Lo, Hi, I) :-
> +    % loop invariant: if X is anywhere in A[0] .. A[array.size(A)-1],
> +    % then it is in A[Lo] .. A[Hi].
> +    Lo =< Hi,
> +    Mid = (Lo + Hi) / 2,
> +    array.unsafe_lookup(A, Mid, MidX),
> +    O = Cmp(MidX, X),
> +    (
> +        O = (>),
> +        binary_search_loop(Cmp, A, X, Lo, Mid - 1, I)
> +    ;
> +        O = (=),
> +        I = Mid         % XXX repetitions

Did you mean to leave these in?

> -approx_binary_search_2(Cmp, A, X, Lo, Hi, I) :-
> +approx_binary_search_loop(Cmp, A, X, Lo, Hi, I) :-
> +    % loop invariant: if X is anywhere in A[0] .. A[array.size(A)-1],
> +    % then it is in A[Lo] .. A[Hi].
>      Lo =< Hi,
>      Mid = (Lo + Hi) / 2,
> -    O = Cmp(A ^ elem(Mid), X),
> +    array.unsafe_lookup(A, Mid, MidX),
> +    O = Cmp(MidX, X),
>      (
>          O = (>),
> -        approx_binary_search_2(Cmp, A, X, Lo, Mid - 1, I)
> +        approx_binary_search_loop(Cmp, A, X, Lo, Mid - 1, I)
>      ;
>          O = (=),
> -        I = Mid
> +        I = Mid         % XXX repetitions
>      ;
>          O = (<),
> -        ( if ( Mid < Hi, X @< A ^ elem(Mid + 1) ; Mid = Hi ) then
> +        ( if
> +            (
> +                Mid < Hi,
> +                % Mid + 1 cannot exceed Hi, so the array access is safe.
> +                array.unsafe_lookup(A, Mid + 1, MidP1X),
> +                (<) = Cmp(X, MidP1X)
> +            ;
> +                Mid = Hi
> +            )
> +        then
>              I = Mid
> -          else
> -            approx_binary_search_2(Cmp, A, X, Mid + 1, Hi, I)
> +        else
> +            approx_binary_search_loop(Cmp, A, X, Mid + 1, Hi, I)
>          )
>      ).

The unsafe_lookup goals could potentially be ordered before the bounds
checks.  Do you want to want to fix it?

Thanks, Zoltan.

Peter