JDK8/Java8源码在线阅读
/*
* 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.
private final static long LONG_MASK = 0xffffffffL;
//@ 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</code>, but the next bit should be 1
* <code>(highestWord & 0x08000000) != 0</code>.
*
* @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
@
@ requires this.value() > 0;
@ ensures ((\bigint)1) << (\result - 1) <= this.value() && this.value() <= ((\bigint)1) << \result;
@*/
private /*@ pure @*/ int size() {
return nWords + offset;
}
/**
* Computes
* <pre>
* q = (int)( this / S )
* this = 10 * ( this mod S )
* Return q.
* </pre>
* This is the iteration step of digit development for output.
* We assume that S has been normalized, as above, and that
* "this" has been left-shifted accordingly.
* Also assumed, of course, is that the result, q, can be expressed
* as an integer, 0 <= q < 10.
*
* @param The divisor of this <code>FDBigInteger</code>.
* @return <code>q = (int)(this / S)</code>.
*/
/*@
@ requires !this.isImmutable;
@ requires this.size() <= S.size();
@ requires this.data.length + this.offset >= S.size();
@ requires S.value() >= ((\bigint)1) << (S.size()*32 - 4);
@ assignable this.nWords, this.offset, this.data, this.data[*];
@ ensures \result == \old(this.value() / S.value());
@ ensures this.value() == \old(10 * (this.value() % S.value()));
@*/
public int quoRemIteration(FDBigInteger S) throws IllegalArgumentException {
assert !this.isImmutable : "cannot modify immutable value";
// ensure that this and S have the same number of
// digits. If S is properly normalized and q < 10 then
// this must be so.
int thSize = this.size();
int sSize = S.size();
if (thSize < sSize) {
// this value is significantly less than S, result of division is zero.
// just mult this by 10.
int p = multAndCarryBy10(this.data, this.nWords, this.data);
if(p!=0) {
this.data[nWords++] = p;
} else {
trimLeadingZeros();
}
return 0;
} else if (thSize > sSize) {
throw new IllegalArgumentException("disparate values");
}
// estimate q the obvious way. We will usually be
// right. If not, then we're only off by a little and
// will re-add.
long q = (this.data[this.nWords - 1] & LONG_MASK) / (S.data[S.nWords - 1] & LONG_MASK);
long diff = multDiffMe(q, S);
if (diff != 0L) {
//@ assert q != 0;
//@ assert this.offset == \old(Math.min(this.offset, S.offset));
//@ assert this.offset <= S.offset;
// q is too big.
// add S back in until this turns +. This should
// not be very many times!
long sum = 0L;
int tStart = S.offset - this.offset;
//@ assert tStart >= 0;
int[] sd = S.data;
int[] td = this.data;
while (sum == 0L) {
for (int sIndex = 0, tIndex = tStart; tIndex < this.nWords; sIndex++, tIndex++) {
sum += (td[tIndex] & LONG_MASK) + (sd[sIndex] & LONG_MASK);
td[tIndex] = (int) sum;
sum >>>= 32; // Signed or unsigned, answer is 0 or 1
}
//
// Originally the following line read
// "if ( sum !=0 && sum != -1 )"
// but that would be wrong, because of the
// treatment of the two values as entirely unsigned,
// it would be impossible for a carry-out to be interpreted
// as -1 -- it would have to be a single-bit carry-out, or +1.
//
assert sum == 0 || sum == 1 : sum; // carry out of division correction
q -= 1;
}
}
// finally, we can multiply this by 10.
// it cannot overflow, right, as the high-order word has
// at least 4 high-order zeros!
int p = multAndCarryBy10(this.data, this.nWords, this.data);
assert p == 0 : p; // Carry out of *10
trimLeadingZeros();
return (int) q;
}
/**
* Multiplies this <code>FDBigInteger</code> by 10. The operation will be
* performed in place unless the <code>FDBigInteger</code> is immutable in
* which case a new <code>FDBigInteger</code> will be returned.
*
* @return The <code>FDBigInteger</code> multiplied by 10.
*/
/*@
@ requires this.value() == 0;
@ assignable \nothing;
@ ensures \result == this;
@
@ also
@
@ requires this.value() > 0 && this.isImmutable;
@ assignable \nothing;
@ ensures \result.value() == \old(this.value() * 10);
@
@ also
@
@ requires this.value() > 0 && !this.isImmutable;
@ assignable this.nWords, this.data, this.data[*];
@ ensures \result == this;
@ ensures \result.value() == \old(this.value() * 10);
@*/
public FDBigInteger multBy10() {
if (nWords == 0) {
return this;
}
if (isImmutable) {
int[] res = new int[nWords + 1];
res[nWords] = multAndCarryBy10(data, nWords, res);
return new FDBigInteger(res, offset);
} else {
int p = multAndCarryBy10(this.data, this.nWords, this.data);
if (p != 0) {
if (nWords == data.length) {
if (data[0] == 0) {
System.arraycopy(data, 1, data, 0, --nWords);
offset++;
} else {
data = Arrays.copyOf(data, data.length + 1);
}
}
data[nWords++] = p;
} else {
trimLeadingZeros();
}
return this;
}
}
/**
* Multiplies this <code>FDBigInteger</code> by
* <code>5<sup>p5</sup> * 2<sup>p2</sup></code>. The operation will be
* performed in place if possible, otherwise a new <code>FDBigInteger</code>
* will be returned.
*
* @param p5 The exponent of the power-of-five factor.
* @param p2 The exponent of the power-of-two factor.
* @return
*/
/*@
@ requires this.value() == 0 || p5 == 0 && p2 == 0;
@ assignable \nothing;
@ ensures \result == this;
@
@ also
@
@ requires this.value() > 0 && (p5 > 0 && p2 >= 0 || p5 == 0 && p2 > 0 && this.isImmutable);
@ assignable \nothing;
@ ensures \result.value() == \old(this.value() * pow52(p5, p2));
@
@ also
@
@ requires this.value() > 0 && p5 == 0 && p2 > 0 && !this.isImmutable;
@ assignable this.nWords, this.data, this.data[*];
@ ensures \result == this;
@ ensures \result.value() == \old(this.value() * pow52(p5, p2));
@*/
public FDBigInteger multByPow52(int p5, int p2) {
if (this.nWords == 0) {
return this;
}
FDBigInteger res = this;
if (p5 != 0) {
int[] r;
int extraSize = (p2 != 0) ? 1 : 0;
if (p5 < SMALL_5_POW.length) {
r = new int[this.nWords + 1 + extraSize];
mult(this.data, this.nWords, SMALL_5_POW[p5], r);
res = new FDBigInteger(r, this.offset);
} else {
FDBigInteger pow5 = big5pow(p5);
r = new int[this.nWords + pow5.size() + extraSize];
mult(this.data, this.nWords, pow5.data, pow5.nWords, r);
res = new FDBigInteger(r, this.offset + pow5.offset);
}
}
return res.leftShift(p2);
}
/**
* Multiplies two big integers represented as int arrays.
*
* @param s1 The first array factor.
* @param s1Len The number of elements of <code>s1</code> to use.
* @param s2 The second array factor.
* @param s2Len The number of elements of <code>s2</code> to use.
* @param dst The product array.
*/
/*@
@ requires s1 != dst && s2 != dst;
@ requires s1.length >= s1Len && s2.length >= s2Len && dst.length >= s1Len + s2Len;
@ assignable dst[0 .. s1Len + s2Len - 1];
@ ensures AP(dst, s1Len + s2Len) == \old(AP(s1, s1Len) * AP(s2, s2Len));
@*/
private static void mult(int[] s1, int s1Len, int[] s2, int s2Len, int[] dst) {
for (int i = 0; i < s1Len; i++) {
long v = s1[i] & LONG_MASK;
long p = 0L;
for (int j = 0; j < s2Len; j++) {
p += (dst[i + j] & LONG_MASK) + v * (s2[j] & LONG_MASK);
dst[i + j] = (int) p;
p >>>= 32;
}
dst[i + s2Len] = (int) p;
}
}
/**
* Subtracts the supplied <code>FDBigInteger</code> subtrahend from this
* <code>FDBigInteger</code>. Assert that the result is positive.
* If the subtrahend is immutable, store the result in this(minuend).
* If this(minuend) is immutable a new <code>FDBigInteger</code> is created.
*
* @param subtrahend The <code>FDBigInteger</code> to be subtracted.
* @return This <code>FDBigInteger</code> less the subtrahend.
*/
/*@
@ requires this.isImmutable;
@ requires this.value() >= subtrahend.value();
@ assignable \nothing;
@ ensures \result.value() == \old(this.value() - subtrahend.value());
@
@ also
@
@ requires !subtrahend.isImmutable;
@ requires this.value() >= subtrahend.value();
@ assignable this.nWords, this.offset, this.data, this.data[*];
@ ensures \result == this;
@ ensures \result.value() == \old(this.value() - subtrahend.value());
@*/
public FDBigInteger leftInplaceSub(FDBigInteger subtrahend) {
assert this.size() >= subtrahend.size() : "result should be positive";
FDBigInteger minuend;
if (this.isImmutable) {
minuend = new FDBigInteger(this.data.clone(), this.offset);
} else {
minuend = this;
}
int offsetDiff = subtrahend.offset - minuend.offset;
int[] sData = subtrahend.data;
int[] mData = minuend.data;
int subLen = subtrahend.nWords;
int minLen = minuend.nWords;
if (offsetDiff < 0) {
// need to expand minuend
int rLen = minLen - offsetDiff;
if (rLen < mData.length) {
System.arraycopy(mData, 0, mData, -offsetDiff, minLen);
Arrays.fill(mData, 0, -offsetDiff, 0);
} else {
int[] r = new int[rLen];
System.arraycopy(mData, 0, r, -offsetDiff, minLen);
minuend.data = mData = r;
}
minuend.offset = subtrahend.offset;
minuend.nWords = minLen = rLen;
offsetDiff = 0;
}
long borrow = 0L;
int mIndex = offsetDiff;
for (int sIndex = 0; sIndex < subLen && mIndex < minLen; sIndex++, mIndex++) {
long diff = (mData[mIndex] & LONG_MASK) - (sData[sIndex] & LONG_MASK) + borrow;
mData[mIndex] = (int) diff;
borrow = diff >> 32; // signed shift
}
for (; borrow != 0 && mIndex < minLen; mIndex++) {
long diff = (mData[mIndex] & LONG_MASK) + borrow;
mData[mIndex] = (int) diff;
borrow = diff >> 32; // signed shift
}
assert borrow == 0L : borrow; // borrow out of subtract,
// result should be positive
minuend.trimLeadingZeros();
return minuend;
}
/**
* Subtracts the supplied <code>FDBigInteger</code> subtrahend from this
* <code>FDBigInteger</code>. Assert that the result is positive.
* If the this(minuend) is immutable, store the result in subtrahend.
* If subtrahend is immutable a new <code>FDBigInteger</code> is created.
*
* @param subtrahend The <code>FDBigInteger</code> to be subtracted.
* @return This <code>FDBigInteger</code> less the subtrahend.
*/
/*@
@ requires subtrahend.isImmutable;
@ requires this.value() >= subtrahend.value();
@ assignable \nothing;
@ ensures \result.value() == \old(this.value() - subtrahend.value());
@
@ also
@
@ requires !subtrahend.isImmutable;
@ requires this.value() >= subtrahend.value();
@ assignable subtrahend.nWords, subtrahend.offset, subtrahend.data, subtrahend.data[*];
@ ensures \result == subtrahend;
@ ensures \result.value() == \old(this.value() - subtrahend.value());
@*/
public FDBigInteger rightInplaceSub(FDBigInteger subtrahend) {
assert this.size() >= subtrahend.size() : "result should be positive";
FDBigInteger minuend = this;
if (subtrahend.isImmutable) {
subtrahend = new FDBigInteger(subtrahend.data.clone(), subtrahend.offset);
}
int offsetDiff = minuend.offset - subtrahend.offset;
int[] sData = subtrahend.data;
int[] mData = minuend.data;
int subLen = subtrahend.nWords;
int minLen = minuend.nWords;
if (offsetDiff < 0) {
int rLen = minLen;
if (rLen < sData.length) {
System.arraycopy(sData, 0, sData, -offsetDiff, subLen);
Arrays.fill(sData, 0, -offsetDiff, 0);
} else {
int[] r = new int[rLen];
System.arraycopy(sData, 0, r, -offsetDiff, subLen);
subtrahend.data = sData = r;
}
subtrahend.offset = minuend.offset;
subLen -= offsetDiff;
offsetDiff = 0;
} else {
int rLen = minLen + offsetDiff;
if (rLen >= sData.length) {
subtrahend.data = sData = Arrays.copyOf(sData, rLen);
}
}
//@ assert minuend == this && minuend.value() == \old(this.value());
//@ assert mData == minuend.data && minLen == minuend.nWords;
//@ assert subtrahend.offset + subtrahend.data.length >= minuend.size();
//@ assert sData == subtrahend.data;
//@ assert AP(subtrahend.data, subtrahend.data.length) << subtrahend.offset == \old(subtrahend.value());
//@ assert subtrahend.offset == Math.min(\old(this.offset), minuend.offset);
//@ assert offsetDiff == minuend.offset - subtrahend.offset;
//@ assert 0 <= offsetDiff && offsetDiff + minLen <= sData.length;
int sIndex = 0;
long borrow = 0L;
for (; sIndex < offsetDiff; sIndex++) {
long diff = 0L - (sData[sIndex] & LONG_MASK) + borrow;
sData[sIndex] = (int) diff;
borrow = diff >> 32; // signed shift
}
//@ assert sIndex == offsetDiff;
for (int mIndex = 0; mIndex < minLen; sIndex++, mIndex++) {
//@ assert sIndex == offsetDiff + mIndex;
long diff = (mData[mIndex] & LONG_MASK) - (sData[sIndex] & LONG_MASK) + borrow;
sData[sIndex] = (int) diff;
borrow = diff >> 32; // signed shift
}
assert borrow == 0L : borrow; // borrow out of subtract,
// result should be positive
subtrahend.nWords = sIndex;
subtrahend.trimLeadingZeros();
return subtrahend;
}
/**
* Determines whether all elements of an array are zero for all indices less
* than a given index.
*
* @param a The array to be examined.
* @param from The index strictly below which elements are to be examined.
* @return Zero if all elements in range are zero, 1 otherwise.
*/
/*@
@ requires 0 <= from && from <= a.length;
@ ensures \result == (AP(a, from) == 0 ? 0 : 1);
@*/
private /*@ pure @*/ static int checkZeroTail(int[] a, int from) {
while (from > 0) {
if (a[--from] != 0) {
return 1;
}
}
return 0;
}
/**
* Compares the parameter with this <code>FDBigInteger</code>. Returns an
* integer accordingly as:
* <pre>
* >0: this > other
* 0: this == other
* <0: this < other
* </pre>
*
* @param other The <code>FDBigInteger</code> to compare.
* @return A negative value, zero, or a positive value according to the
* result of the comparison.
*/
/*@
@ ensures \result == (this.value() < other.value() ? -1 : this.value() > other.value() ? +1 : 0);
@*/
public /*@ pure @*/ int cmp(FDBigInteger other) {
int aSize = nWords + offset;
int bSize = other.nWords + other.offset;
if (aSize > bSize) {
return 1;
} else if (aSize < bSize) {
return -1;
}
int aLen = nWords;
int bLen = other.nWords;
while (aLen > 0 && bLen > 0) {
int a = data[--aLen];
int b = other.data[--bLen];
if (a != b) {
return ((a & LONG_MASK) < (b & LONG_MASK)) ? -1 : 1;
}
}
if (aLen > 0) {
return checkZeroTail(data, aLen);
}
if (bLen > 0) {
return -checkZeroTail(other.data, bLen);
}
return 0;
}
/**
* Compares this <code>FDBigInteger</code> with
* <code>5<sup>p5</sup> * 2<sup>p2</sup></code>.
* Returns an integer accordingly as:
* <pre>
* >0: this > other
* 0: this == other
* <0: this < other
* </pre>
* @param p5 The exponent of the power-of-five factor.
* @param p2 The exponent of the power-of-two factor.
* @return A negative value, zero, or a positive value according to the
* result of the comparison.
*/
/*@
@ requires p5 >= 0 && p2 >= 0;
@ ensures \result == (this.value() < pow52(p5, p2) ? -1 : this.value() > pow52(p5, p2) ? +1 : 0);
@*/
public /*@ pure @*/ int cmpPow52(int p5, int p2) {
if (p5 == 0) {
int wordcount = p2 >> 5;
int bitcount = p2 & 0x1f;
int size = this.nWords + this.offset;
if (size > wordcount + 1) {
return 1;
} else if (size < wordcount + 1) {
return -1;
}
int a = this.data[this.nWords -1];
int b = 1 << bitcount;
if (a != b) {
return ( (a & LONG_MASK) < (b & LONG_MASK)) ? -1 : 1;
}
return checkZeroTail(this.data, this.nWords - 1);
}
return this.cmp(big5pow(p5).leftShift(p2));
}
/**
* Compares this <code>FDBigInteger</code> with <code>x + y</code>. Returns a
* value according to the comparison as:
* <pre>
* -1: this < x + y
* 0: this == x + y
* 1: this > x + y
* </pre>
* @param x The first addend of the sum to compare.
* @param y The second addend of the sum to compare.
* @return -1, 0, or 1 according to the result of the comparison.
*/
/*@
@ ensures \result == (this.value() < x.value() + y.value() ? -1 : this.value() > x.value() + y.value() ? +1 : 0);
@*/
public /*@ pure @*/ int addAndCmp(FDBigInteger x, FDBigInteger y) {
FDBigInteger big;
FDBigInteger small;
int xSize = x.size();
int ySize = y.size();
int bSize;
int sSize;
if (xSize >= ySize) {
big = x;
small = y;
bSize = xSize;
sSize = ySize;
} else {
big = y;
small = x;
bSize = ySize;
sSize = xSize;
}
int thSize = this.size();
if (bSize == 0) {
return thSize == 0 ? 0 : 1;
}
if (sSize == 0) {
return this.cmp(big);
}
if (bSize > thSize) {
return -1;
}
if (bSize + 1 < thSize) {
return 1;
}
long top = (big.data[big.nWords - 1] & LONG_MASK);
if (sSize == bSize) {
top += (small.data[small.nWords - 1] & LONG_MASK);
}
if ((top >>> 32) == 0) {
if (((top + 1) >>> 32) == 0) {
// good case - no carry extension
if (bSize < thSize) {
return 1;
}
// here sum.nWords == this.nWords
long v = (this.data[this.nWords - 1] & LONG_MASK);
if (v < top) {
return -1;
}
if (v > top + 1) {
return 1;
}
}
} else { // (top>>>32)!=0 guaranteed carry extension
if (bSize + 1 > thSize) {
return -1;
}
// here sum.nWords == this.nWords
top >>>= 32;
long v = (this.data[this.nWords - 1] & LONG_MASK);
if (v < top) {
return -1;
}
if (v > top + 1) {
return 1;
}
}
return this.cmp(big.add(small));
}
/**
* Makes this <code>FDBigInteger</code> immutable.
*/
/*@
@ assignable this.isImmutable;
@ ensures this.isImmutable;
@*/
public void makeImmutable() {
this.isImmutable = true;
}
/**
* Multiplies this <code>FDBigInteger</code> by an integer.
*
* @param i The factor by which to multiply this <code>FDBigInteger</code>.
* @return This <code>FDBigInteger</code> multiplied by an integer.
*/
/*@
@ requires this.value() == 0;
@ assignable \nothing;
@ ensures \result == this;
@
@ also
@
@ requires this.value() != 0;
@ assignable \nothing;
@ ensures \result.value() == \old(this.value() * UNSIGNED(i));
@*/
private FDBigInteger mult(int i) {
if (this.nWords == 0) {
return this;
}
int[] r = new int[nWords + 1];
mult(data, nWords, i, r);
return new FDBigInteger(r, offset);
}
/**
* Multiplies this <code>FDBigInteger</code> by another <code>FDBigInteger</code>.
*
* @param other The <code>FDBigInteger</code> factor by which to multiply.
* @return The product of this and the parameter <code>FDBigInteger</code>s.
*/
/*@
@ requires this.value() == 0;
@ assignable \nothing;
@ ensures \result == this;
@
@ also
@
@ requires this.value() != 0 && other.value() == 0;
@ assignable \nothing;
@ ensures \result == other;
@
@ also
@
@ requires this.value() != 0 && other.value() != 0;
@ assignable \nothing;
@ ensures \result.value() == \old(this.value() * other.value());
@*/
private FDBigInteger mult(FDBigInteger other) {
if (this.nWords == 0) {
return this;
}
if (this.size() == 1) {
return other.mult(data[0]);
}
if (other.nWords == 0) {
return other;
}
if (other.size() == 1) {
return this.mult(other.data[0]);
}
int[] r = new int[nWords + other.nWords];
mult(this.data, this.nWords, other.data, other.nWords, r);
return new FDBigInteger(r, this.offset + other.offset);
}
/**
* Adds another <code>FDBigInteger</code> to this <code>FDBigInteger</code>.
*
* @param other The <code>FDBigInteger</code> to add.
* @return The sum of the <code>FDBigInteger</code>s.
*/
/*@
@ assignable \nothing;
@ ensures \result.value() == \old(this.value() + other.value());
@*/
private FDBigInteger add(FDBigInteger other) {
FDBigInteger big, small;
int bigLen, smallLen;
int tSize = this.size();
int oSize = other.size();
if (tSize >= oSize) {
big = this;
bigLen = tSize;
small = other;
smallLen = oSize;
} else {
big = other;
bigLen = oSize;
small = this;
smallLen = tSize;
}
int[] r = new int[bigLen + 1];
int i = 0;
long carry = 0L;
for (; i < smallLen; i++) {
carry += (i < big.offset ? 0L : (big.data[i - big.offset] & LONG_MASK) )
+ ((i < small.offset ? 0L : (small.data[i - small.offset] & LONG_MASK)));
r[i] = (int) carry;
carry >>= 32; // signed shift.
}
for (; i < bigLen; i++) {
carry += (i < big.offset ? 0L : (big.data[i - big.offset] & LONG_MASK) );
r[i] = (int) carry;
carry >>= 32; // signed shift.
}
r[bigLen] = (int) carry;
return new FDBigInteger(r, 0);
}
/**
* Multiplies a <code>FDBigInteger</code> by an int and adds another int. The
* result is computed in place. This method is intended only to be invoked
* from
* <code>
* FDBigInteger(long lValue, char[] digits, int kDigits, int nDigits)
* </code>.
*
* @param iv The factor by which to multiply this <code>FDBigInteger</code>.
* @param addend The value to add to the product of this
* <code>FDBigInteger</code> and <code>iv</code>.
*/
/*@
@ requires this.value()*UNSIGNED(iv) + UNSIGNED(addend) < ((\bigint)1) << ((this.data.length + this.offset)*32);
@ assignable this.data[*];
@ ensures this.value() == \old(this.value()*UNSIGNED(iv) + UNSIGNED(addend));
@*/
private /*@ helper @*/ void multAddMe(int iv, int addend) {
long v = iv & LONG_MASK;
// unroll 0th iteration, doing addition.
long p = v * (data[0] & LONG_MASK) + (addend & LONG_MASK);
data[0] = (int) p;
p >>>= 32;
for (int i = 1; i < nWords; i++) {
p += v * (data[i] & LONG_MASK);
data[i] = (int) p;
p >>>= 32;
}
if (p != 0L) {
data[nWords++] = (int) p; // will fail noisily if illegal!
}
}
//
// original doc:
//
// do this -=q*S
// returns borrow
//
/**
* Multiplies the parameters and subtracts them from this
* <code>FDBigInteger</code>.
*
* @param q The integer parameter.
* @param S The <code>FDBigInteger</code> parameter.
* @return <code>this - q*S</code>.
*/
/*@
@ ensures nWords == 0 ==> offset == 0;
@ ensures nWords > 0 ==> data[nWords - 1] != 0;
@*/
/*@
@ requires 0 < q && q <= (1L << 31);
@ requires data != null;
@ requires 0 <= nWords && nWords <= data.length && offset >= 0;
@ requires !this.isImmutable;
@ requires this.size() == S.size();
@ requires this != S;
@ assignable this.nWords, this.offset, this.data, this.data[*];
@ ensures -q <= \result && \result <= 0;
@ ensures this.size() == \old(this.size());
@ ensures this.value() + (\result << (this.size()*32)) == \old(this.value() - q*S.value());
@ ensures this.offset == \old(Math.min(this.offset, S.offset));
@ ensures \old(this.offset <= S.offset) ==> this.nWords == \old(this.nWords);
@ ensures \old(this.offset <= S.offset) ==> this.offset == \old(this.offset);
@ ensures \old(this.offset <= S.offset) ==> this.data == \old(this.data);
@
@ also
@
@ requires q == 0;
@ assignable \nothing;
@ ensures \result == 0;
@*/
private /*@ helper @*/ long multDiffMe(long q, FDBigInteger S) {
long diff = 0L;
if (q != 0) {
int deltaSize = S.offset - this.offset;
if (deltaSize >= 0) {
int[] sd = S.data;
int[] td = this.data;
for (int sIndex = 0, tIndex = deltaSize; sIndex < S.nWords; sIndex++, tIndex++) {
diff += (td[tIndex] & LONG_MASK) - q * (sd[sIndex] & LONG_MASK);
td[tIndex] = (int) diff;
diff >>= 32; // N.B. SIGNED shift.
}
} else {
deltaSize = -deltaSize;
int[] rd = new int[nWords + deltaSize];
int sIndex = 0;
int rIndex = 0;
int[] sd = S.data;
for (; rIndex < deltaSize && sIndex < S.nWords; sIndex++, rIndex++) {
diff -= q * (sd[sIndex] & LONG_MASK);
rd[rIndex] = (int) diff;
diff >>= 32; // N.B. SIGNED shift.
}
int tIndex = 0;
int[] td = this.data;
for (; sIndex < S.nWords; sIndex++, tIndex++, rIndex++) {
diff += (td[tIndex] & LONG_MASK) - q * (sd[sIndex] & LONG_MASK);
rd[rIndex] = (int) diff;
diff >>= 32; // N.B. SIGNED shift.
}
this.nWords += deltaSize;
this.offset -= deltaSize;
this.data = rd;
}
}
return diff;
}
/**
* Multiplies by 10 a big integer represented as an array. The final carry
* is returned.
*
* @param src The array representation of the big integer.
* @param srcLen The number of elements of <code>src</code> to use.
* @param dst The product array.
* @return The final carry of the multiplication.
*/
/*@
@ requires src.length >= srcLen && dst.length >= srcLen;
@ assignable dst[0 .. srcLen - 1];
@ ensures 0 <= \result && \result < 10;
@ ensures AP(dst, srcLen) + (\result << (srcLen*32)) == \old(AP(src, srcLen) * 10);
@*/
/**代码未完, 请加载全部代码(NowJava.com).**/
关注时代Java
关注时代Java