/*

 * Copyright (c) 2013, Oracle and/or its affiliates. All rights reserved.

 * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.

 *

 * This code is free software; you can redistribute it and/or modify it

 * under the terms of the GNU General Public License version 2 only, as

 * published by the Free Software Foundation.  Oracle designates this

 * particular file as subject to the "Classpath" exception as provided

 * by Oracle in the LICENSE file that accompanied this code.

 *

 * This code is distributed in the hope that it will be useful, but WITHOUT

 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or

 * FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public License

 * version 2 for more details (a copy is included in the LICENSE file that

 * accompanied this code).

 *

 * You should have received a copy of the GNU General Public License version

 * 2 along with this work; if not, write to the Free Software Foundation,

 * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.

 *

 * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA

 * or visit www.oracle.com if you need additional information or have any

 * questions.

 */

package sun.misc;

import java.math.BigInteger;

import java.util.Arrays;

//@ model import org.jmlspecs.models.JMLMath;

/**

 * A simple big integer package specifically for floating point base conversion.

 */

public /*@ spec_bigint_math @*/ class FDBigInteger {

    //

    // This class contains many comments that start with "/*@" mark.

    // They are behavourial specification in

    // the Java Modelling Language (JML):

    // http://www.eecs.ucf.edu/~leavens/JML//index.shtml

    //

    /*@

    @ public pure model static \bigint UNSIGNED(int v) {

    @     return v >= 0 ? v : v + (((\bigint)1) << 32);

    @ }

    @

    @ public pure model static \bigint UNSIGNED(long v) {

    @     return v >= 0 ? v : v + (((\bigint)1) << 64);

    @ }

    @

    @ public pure model static \bigint AP(int[] data, int len) {

    @     return (\sum int i; 0 <= 0 && i < len; UNSIGNED(data[i]) << (i*32));

    @ }

    @

    @ public pure model static \bigint pow52(int p5, int p2) {

    @     ghost \bigint v = 1;

    @     for (int i = 0; i < p5; i++) v *= 5;

    @     return v << p2;

    @ }

    @

    @ public pure model static \bigint pow10(int p10) {

    @     return pow52(p10, p10);

    @ }

    @*/

    static final int[] SMALL_5_POW = {

            1,

            5,

            5 * 5,

            5 * 5 * 5,

            5 * 5 * 5 * 5,

            5 * 5 * 5 * 5 * 5,

            5 * 5 * 5 * 5 * 5 * 5,

            5 * 5 * 5 * 5 * 5 * 5 * 5,

            5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5

    };

    static final long[] LONG_5_POW = {

            1L,

            5L,

            5L * 5,

            5L * 5 * 5,

            5L * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

            5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5,

    };

    // Maximum size of cache of powers of 5 as FDBigIntegers.

    private static final int MAX_FIVE_POW = 340;

    // Cache of big powers of 5 as FDBigIntegers.

    private static final FDBigInteger POW_5_CACHE[];

    // Initialize FDBigInteger cache of powers of 5.

    static {

        POW_5_CACHE = new FDBigInteger[MAX_FIVE_POW];

        int i = 0;

        while (i < SMALL_5_POW.length) {

            FDBigInteger pow5 = new FDBigInteger(new int[]{SMALL_5_POW[i]}, 0);

            pow5.makeImmutable();

            POW_5_CACHE[i] = pow5;

            i++;

        }

        FDBigInteger prev = POW_5_CACHE[i - 1];

        while (i < MAX_FIVE_POW) {

            POW_5_CACHE[i] = prev = prev.mult(5);

            prev.makeImmutable();

            i++;

        }

    }

    // Zero as an FDBigInteger.

    public static final FDBigInteger ZERO = new FDBigInteger(new int[0], 0);

    // Ensure ZERO is immutable.

    static {

        ZERO.makeImmutable();

    }

    // Constant for casting an int to a long via bitwise AND.

    //@ spec_public non_null;

    private int data[];  // value: data[0] is least significant

    //@ spec_public;

    private int offset;  // number of least significant zero padding ints

    //@ spec_public;

    private int nWords;  // data[nWords-1]!=0, all values above are zero

                 // if nWords==0 -> this FDBigInteger is zero

    //@ spec_public;

    private boolean isImmutable = false;

    /*@

     @ public invariant 0 <= nWords && nWords <= data.length && offset >= 0;

     @ public invariant nWords == 0 ==> offset == 0;

     @ public invariant nWords > 0 ==> data[nWords - 1] != 0;

     @ public invariant (\forall int i; nWords <= i && i < data.length; data[i] == 0);

     @ public pure model \bigint value() {

     @     return AP(data, nWords) << (offset*32);

     @ }

     @*/

    /**

     * Constructs an <code>FDBigInteger</code> from data and padding. The

     * <code>data</code> parameter has the least significant <code>int</code> at

     * the zeroth index. The <code>offset</code> parameter gives the number of

     * zero <code>int</code>s to be inferred below the least significant element

     * of <code>data</code>.

     *

     * @param data An array containing all non-zero <code>int</code>s of the value.

     * @param offset An offset indicating the number of zero <code>int</code>s to pad

     * below the least significant element of <code>data</code>.

     */

    /*@

     @ requires data != null && offset >= 0;

     @ ensures this.value() == \old(AP(data, data.length) << (offset*32));

     @ ensures this.data == \old(data);

     @*/

    private FDBigInteger(int[] data, int offset) {

        this.data = data;

        this.offset = offset;

        this.nWords = data.length;

        trimLeadingZeros();

    }

    /**

     * Constructs an <code>FDBigInteger</code> from a starting value and some

     * decimal digits.

     *

     * @param lValue The starting value.

     * @param digits The decimal digits.

     * @param kDigits The initial index into <code>digits</code>.

     * @param nDigits The final index into <code>digits</code>.

     */

    /*@

     @ requires digits != null;

     @ requires 0 <= kDigits && kDigits <= nDigits && nDigits <= digits.length;

     @ requires (\forall int i; 0 <= i && i < nDigits; '0' <= digits[i] && digits[i] <= '9');

     @ ensures this.value() == \old(lValue * pow10(nDigits - kDigits) + (\sum int i; kDigits <= i && i < nDigits; (digits[i] - '0') * pow10(nDigits - i - 1)));

     @*/

    public FDBigInteger(long lValue, char[] digits, int kDigits, int nDigits) {

        int n = Math.max((nDigits + 8) / 9, 2);        // estimate size needed.

        data = new int[n];      // allocate enough space

        data[0] = (int) lValue;    // starting value

        data[1] = (int) (lValue >>> 32);

        offset = 0;

        nWords = 2;

        int i = kDigits;

        int limit = nDigits - 5;       // slurp digits 5 at a time.

        int v;

        while (i < limit) {

            int ilim = i + 5;

            v = (int) digits[i++] - (int) '0';

            while (i < ilim) {

                v = 10 * v + (int) digits[i++] - (int) '0';

            }

            multAddMe(100000, v); // ... where 100000 is 10^5.

        }

        int factor = 1;

        v = 0;

        while (i < nDigits) {

            v = 10 * v + (int) digits[i++] - (int) '0';

            factor *= 10;

        }

        if (factor != 1) {

            multAddMe(factor, v);

        }

        trimLeadingZeros();

    }

    /**

     * Returns an <code>FDBigInteger</code> with the numerical value

     * <code>5<sup>p5</sup> * 2<sup>p2</sup></code>.

     *

     * @param p5 The exponent of the power-of-five factor.

     * @param p2 The exponent of the power-of-two factor.

     * @return <code>5<sup>p5</sup> * 2<sup>p2</sup></code>

     */

    /*@

     @ requires p5 >= 0 && p2 >= 0;

     @ assignable \nothing;

     @ ensures \result.value() == \old(pow52(p5, p2));

     @*/

    public static FDBigInteger valueOfPow52(int p5, int p2) {

        if (p5 != 0) {

            if (p2 == 0) {

                return big5pow(p5);

            } else if (p5 < SMALL_5_POW.length) {

                int pow5 = SMALL_5_POW[p5];

                int wordcount = p2 >> 5;

                int bitcount = p2 & 0x1f;

                if (bitcount == 0) {

                    return new FDBigInteger(new int[]{pow5}, wordcount);

                } else {

                    return new FDBigInteger(new int[]{

                            pow5 << bitcount,

                            pow5 >>> (32 - bitcount)

                    }, wordcount);

                }

            } else {

                return big5pow(p5).leftShift(p2);

            }

        } else {

            return valueOfPow2(p2);

        }

    }

    /**

     * Returns an <code>FDBigInteger</code> with the numerical value

     * <code>value * 5<sup>p5</sup> * 2<sup>p2</sup></code>.

     *

     * @param value The constant factor.

     * @param p5 The exponent of the power-of-five factor.

     * @param p2 The exponent of the power-of-two factor.

     * @return <code>value * 5<sup>p5</sup> * 2<sup>p2</sup></code>

     */

    /*@

     @ requires p5 >= 0 && p2 >= 0;

     @ assignable \nothing;

     @ ensures \result.value() == \old(UNSIGNED(value) * pow52(p5, p2));

     @*/

    public static FDBigInteger valueOfMulPow52(long value, int p5, int p2) {

        assert p5 >= 0 : p5;

        assert p2 >= 0 : p2;

        int v0 = (int) value;

        int v1 = (int) (value >>> 32);

        int wordcount = p2 >> 5;

        int bitcount = p2 & 0x1f;

        if (p5 != 0) {

            if (p5 < SMALL_5_POW.length) {

                long pow5 = SMALL_5_POW[p5] & LONG_MASK;

                long carry = (v0 & LONG_MASK) * pow5;

                v0 = (int) carry;

                carry >>>= 32;

                carry = (v1 & LONG_MASK) * pow5 + carry;

                v1 = (int) carry;

                int v2 = (int) (carry >>> 32);

                if (bitcount == 0) {

                    return new FDBigInteger(new int[]{v0, v1, v2}, wordcount);

                } else {

                    return new FDBigInteger(new int[]{

                            v0 << bitcount,

                            (v1 << bitcount) | (v0 >>> (32 - bitcount)),

                            (v2 << bitcount) | (v1 >>> (32 - bitcount)),

                            v2 >>> (32 - bitcount)

                    }, wordcount);

                }

            } else {

                FDBigInteger pow5 = big5pow(p5);

                int[] r;

                if (v1 == 0) {

                    r = new int[pow5.nWords + 1 + ((p2 != 0) ? 1 : 0)];

                    mult(pow5.data, pow5.nWords, v0, r);

                } else {

                    r = new int[pow5.nWords + 2 + ((p2 != 0) ? 1 : 0)];

                    mult(pow5.data, pow5.nWords, v0, v1, r);

                }

                return (new FDBigInteger(r, pow5.offset)).leftShift(p2);

            }

        } else if (p2 != 0) {

            if (bitcount == 0) {

                return new FDBigInteger(new int[]{v0, v1}, wordcount);

            } else {

                return new FDBigInteger(new int[]{

                         v0 << bitcount,

                        (v1 << bitcount) | (v0 >>> (32 - bitcount)),

                        v1 >>> (32 - bitcount)

                }, wordcount);

            }

        }

        return new FDBigInteger(new int[]{v0, v1}, 0);

    }

    /**

     * Returns an <code>FDBigInteger</code> with the numerical value

     * <code>2<sup>p2</sup></code>.

     *

     * @param p2 The exponent of 2.

     * @return <code>2<sup>p2</sup></code>

     */

    /*@

     @ requires p2 >= 0;

     @ assignable \nothing;

     @ ensures \result.value() == pow52(0, p2);

     @*/

    private static FDBigInteger valueOfPow2(int p2) {

        int wordcount = p2 >> 5;

        int bitcount = p2 & 0x1f;

        return new FDBigInteger(new int[]{1 << bitcount}, wordcount);

    }

    /**

     * Removes all leading zeros from this <code>FDBigInteger</code> adjusting

     * the offset and number of non-zero leading words accordingly.

     */

    /*@

     @ requires data != null;

     @ requires 0 <= nWords && nWords <= data.length && offset >= 0;

     @ requires nWords == 0 ==> offset == 0;

     @ ensures nWords == 0 ==> offset == 0;

     @ ensures nWords > 0 ==> data[nWords - 1] != 0;

     @*/

    private /*@ helper @*/ void trimLeadingZeros() {

        int i = nWords;

        if (i > 0 && (data[--i] == 0)) {

            //for (; i > 0 && data[i - 1] == 0; i--) ;

            while(i > 0 && data[i - 1] == 0) {

                i--;

            }

            this.nWords = i;

            if (i == 0) { // all words are zero

                this.offset = 0;

            }

        }

    }

    /**

     * Retrieves the normalization bias of the <code>FDBigIntger</code>. The

     * normalization bias is a left shift such that after it the highest word

     * of the value will have the 4 highest bits equal to zero:

     * {@code (highestWord & 0xf0000000) == 0}, but the next bit should be 1

     * {@code (highestWord & 0x08000000) != 0}.

     *

     * @return The normalization bias.

     */

    /*@

     @ requires this.value() > 0;

     @*/

    public /*@ pure @*/ int getNormalizationBias() {

        if (nWords == 0) {

            throw new IllegalArgumentException("Zero value cannot be normalized");

        }

        int zeros = Integer.numberOfLeadingZeros(data[nWords - 1]);

        return (zeros < 4) ? 28 + zeros : zeros - 4;

    }

    // TODO: Why is anticount param needed if it is always 32 - bitcount?

    /**

     * Left shifts the contents of one int array into another.

     *

     * @param src The source array.

     * @param idx The initial index of the source array.

     * @param result The destination array.

     * @param bitcount The left shift.

     * @param anticount The left anti-shift, e.g., <code>32-bitcount</code>.

     * @param prev The prior source value.

     */

    /*@

     @ requires 0 < bitcount && bitcount < 32 && anticount == 32 - bitcount;

     @ requires src.length >= idx && result.length > idx;

     @ assignable result[*];

     @ ensures AP(result, \old(idx + 1)) == \old((AP(src, idx) + UNSIGNED(prev) << (idx*32)) << bitcount);

     @*/

    private static void leftShift(int[] src, int idx, int result[], int bitcount, int anticount, int prev){

        for (; idx > 0; idx--) {

            int v = (prev << bitcount);

            prev = src[idx - 1];

            v |= (prev >>> anticount);

            result[idx] = v;

        }

        int v = prev << bitcount;

        result[0] = v;

    }

    /**

     * Shifts this <code>FDBigInteger</code> to the left. The shift is performed

     * in-place unless the <code>FDBigInteger</code> is immutable in which case

     * a new instance of <code>FDBigInteger</code> is returned.

     *

     * @param shift The number of bits to shift left.

     * @return The shifted <code>FDBigInteger</code>.

     */

    /*@

     @ requires this.value() == 0 || shift == 0;

     @ assignable \nothing;

     @ ensures \result == this;

     @

     @  also

     @

     @ requires this.value() > 0 && shift > 0 && this.isImmutable;

     @ assignable \nothing;

     @ ensures \result.value() == \old(this.value() << shift);

     @

     @  also

     @

     @ requires this.value() > 0 && shift > 0 && this.isImmutable;

     @ assignable \nothing;

     @ ensures \result == this;

     @ ensures \result.value() == \old(this.value() << shift);

     @*/

    public FDBigInteger leftShift(int shift) {

        if (shift == 0 || nWords == 0) {

            return this;

        }

        int wordcount = shift >> 5;

        int bitcount = shift & 0x1f;

        if (this.isImmutable) {

            if (bitcount == 0) {

                return new FDBigInteger(Arrays.copyOf(data, nWords), offset + wordcount);

            } else {

                int anticount = 32 - bitcount;

                int idx = nWords - 1;

                int prev = data[idx];

                int hi = prev >>> anticount;

                int[] result;

                if (hi != 0) {

                    result = new int[nWords + 1];

                    result[nWords] = hi;

                } else {

                    result = new int[nWords];

                }

                leftShift(data,idx,result,bitcount,anticount,prev);

                return new FDBigInteger(result, offset + wordcount);

            }

        } else {

            if (bitcount != 0) {

                int anticount = 32 - bitcount;

                if ((data[0] << bitcount) == 0) {

                    int idx = 0;

                    int prev = data[idx];

                    for (; idx < nWords - 1; idx++) {

                        int v = (prev >>> anticount);

                        prev = data[idx + 1];

                        v |= (prev << bitcount);

                        data[idx] = v;

                    }

                    int v = prev >>> anticount;

                    data[idx] = v;

                    if(v==0) {

                        nWords--;

                    }

                    offset++;

                } else {

                    int idx = nWords - 1;

                    int prev = data[idx];

                    int hi = prev >>> anticount;

                    int[] result = data;

                    int[] src = data;

                    if (hi != 0) {

                        if(nWords == data.length) {

                            data = result = new int[nWords + 1];

                        }

                        result[nWords++] = hi;

                    }

                    leftShift(src,idx,result,bitcount,anticount,prev);

                }

            }

            offset += wordcount;

            return this;

        }

    }

    /**

     * Returns the number of <code>int</code>s this <code>FDBigInteger</code> represents.

     *

     * @return Number of <code>int</code>s required to represent this <code>FDBigInteger</code>.

     */

    /*@

     @ requires this.value() == 0;

     @ ensures \result == 0;

     @

     @  also