< prev index next >

## src/java.base/share/classes/jdk/internal/math/FDBigInteger.java

rev 55787 : 8228507: Archive FDBigInteger
Reviewed-by: TBD
   7 * published by the Free Software Foundation. Oracle designates this 8 * particular file as subject to the "Classpath" exception as provided 9 * by Oracle in the LICENSE file that accompanied this code. 10 * 11 * This code is distributed in the hope that it will be useful, but WITHOUT 12 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 13 * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 14 * version 2 for more details (a copy is included in the LICENSE file that 15 * accompanied this code). 16 * 17 * You should have received a copy of the GNU General Public License version 18 * 2 along with this work; if not, write to the Free Software Foundation, 19 * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA. 20 * 21 * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA 22 * or visit www.oracle.com if you need additional information or have any 23 * questions. 24 */ 25 package jdk.internal.math; 26 27 import java.math.BigInteger; 28 import java.util.Arrays; 29 //@ model import org.jmlspecs.models.JMLMath; 30 31 /** 32 * A simple big integer package specifically for floating point base conversion. 33 */ 34 public /*@ spec_bigint_math @*/ class FDBigInteger { 35 36 // 37 // This class contains many comments that start with "/*@" mark. 38 // They are behavourial specification in 39 // the Java Modelling Language (JML): 40 // http://www.eecs.ucf.edu/~leavens/JML//index.shtml 41 // 42 43 /*@ 44 @ public pure model static \bigint UNSIGNED(int v) { 45 @ return v >= 0 ? v : v + (((\bigint)1) << 32); 46 @ } 47 @ 48 @ public pure model static \bigint UNSIGNED(long v) { 49 @ return v >= 0 ? v : v + (((\bigint)1) << 64); 50 @ } 51 @ 52 @ public pure model static \bigint AP(int[] data, int len) { 53 @ return (\sum int i; 0 <= 0 && i < len; UNSIGNED(data[i]) << (i*32)); 54 @ } 55 @ 56 @ public pure model static \bigint pow52(int p5, int p2) { 57 @ ghost \bigint v = 1; 58 @ for (int i = 0; i < p5; i++) v *= 5; 59 @ return v << p2; 60 @ } 61 @ 62 @ public pure model static \bigint pow10(int p10) { 63 @ return pow52(p10, p10); 64 @ } 65 @*/ 66 67 static final int[] SMALL_5_POW = { 68 1, 69 5, 70 5 * 5, 71 5 * 5 * 5, 72 5 * 5 * 5 * 5, 73 5 * 5 * 5 * 5 * 5, 74 5 * 5 * 5 * 5 * 5 * 5, 75 5 * 5 * 5 * 5 * 5 * 5 * 5, 76 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 77 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 78 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 79 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 80 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 81 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 82 }; 83 84 static final long[] LONG_5_POW = { 85 1L, 86 5L, 87 5L * 5, 88 5L * 5 * 5, 89 5L * 5 * 5 * 5, 90 5L * 5 * 5 * 5 * 5, 91 5L * 5 * 5 * 5 * 5 * 5, 92 5L * 5 * 5 * 5 * 5 * 5 * 5, 93 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5, 94 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 95 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 96 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 97 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 98 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 99 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 100 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 101 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 102 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 103 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 104 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 105 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 106 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 107 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 108 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 109 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 110 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, 111 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, 112 }; 113 114 // Maximum size of cache of powers of 5 as FDBigIntegers. 115 private static final int MAX_FIVE_POW = 340; 116 117 // Cache of big powers of 5 as FDBigIntegers. 118 private static final FDBigInteger POW_5_CACHE[]; 119 120 // Initialize FDBigInteger cache of powers of 5. 121 static { 122 POW_5_CACHE = new FDBigInteger[MAX_FIVE_POW]; 123 int i = 0; 124 while (i < SMALL_5_POW.length) { 125 FDBigInteger pow5 = new FDBigInteger(new int[]{SMALL_5_POW[i]}, 0); 126 pow5.makeImmutable(); 127 POW_5_CACHE[i] = pow5; 128 i++; 129 } 130 FDBigInteger prev = POW_5_CACHE[i - 1]; 131 while (i < MAX_FIVE_POW) { 132 POW_5_CACHE[i] = prev = prev.mult(5); 133 prev.makeImmutable(); 134 i++; 135 } 136 } 137 138 // Zero as an FDBigInteger. 139 public static final FDBigInteger ZERO = new FDBigInteger(new int[0], 0); 140 141 // Ensure ZERO is immutable. 142 static { 143 ZERO.makeImmutable(); 144 } 145 146 // Constant for casting an int to a long via bitwise AND. 147 private static final long LONG_MASK = 0xffffffffL; 148 149 //@ spec_public non_null; 150 private int data[]; // value: data[0] is least significant 151 //@ spec_public; 152 private int offset; // number of least significant zero padding ints 153 //@ spec_public; 154 private int nWords; // data[nWords-1]!=0, all values above are zero 155 // if nWords==0 -> this FDBigInteger is zero 156 //@ spec_public; 157 private boolean isImmutable = false; 158 159 /*@ 160 @ public invariant 0 <= nWords && nWords <= data.length && offset >= 0; 161 @ public invariant nWords == 0 ==> offset == 0; 162 @ public invariant nWords > 0 ==> data[nWords - 1] != 0; 163 @ public invariant (\forall int i; nWords <= i && i < data.length; data[i] == 0); 164 @ public pure model \bigint value() {    7 * published by the Free Software Foundation. Oracle designates this 8 * particular file as subject to the "Classpath" exception as provided 9 * by Oracle in the LICENSE file that accompanied this code. 10 * 11 * This code is distributed in the hope that it will be useful, but WITHOUT 12 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 13 * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 14 * version 2 for more details (a copy is included in the LICENSE file that 15 * accompanied this code). 16 * 17 * You should have received a copy of the GNU General Public License version 18 * 2 along with this work; if not, write to the Free Software Foundation, 19 * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA. 20 * 21 * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA 22 * or visit www.oracle.com if you need additional information or have any 23 * questions. 24 */ 25 package jdk.internal.math; 26 27 import jdk.internal.misc.VM; 28 29 import java.math.BigInteger; 30 import java.util.Arrays; 31 //@ model import org.jmlspecs.models.JMLMath; 32 33 /** 34 * A simple big integer package specifically for floating point base conversion. 35 */ 36 public /*@ spec_bigint_math @*/ class FDBigInteger { 37 38 // 39 // This class contains many comments that start with "/*@" mark. 40 // They are behavourial specification in 41 // the Java Modelling Language (JML): 42 // http://www.eecs.ucf.edu/~leavens/JML//index.shtml 43 // 44 45 /*@ 46 @ public pure model static \bigint UNSIGNED(int v) { 47 @ return v >= 0 ? v : v + (((\bigint)1) << 32); 48 @ } 49 @ 50 @ public pure model static \bigint UNSIGNED(long v) { 51 @ return v >= 0 ? v : v + (((\bigint)1) << 64); 52 @ } 53 @ 54 @ public pure model static \bigint AP(int[] data, int len) { 55 @ return (\sum int i; 0 <= 0 && i < len; UNSIGNED(data[i]) << (i*32)); 56 @ } 57 @ 58 @ public pure model static \bigint pow52(int p5, int p2) { 59 @ ghost \bigint v = 1; 60 @ for (int i = 0; i < p5; i++) v *= 5; 61 @ return v << p2; 62 @ } 63 @ 64 @ public pure model static \bigint pow10(int p10) { 65 @ return pow52(p10, p10); 66 @ } 67 @*/ 68 69 static final int[] SMALL_5_POW; 70 71 static final long[] LONG_5_POW; 72 73 // Maximum size of cache of powers of 5 as FDBigIntegers. 74 private static final int MAX_FIVE_POW = 340; 75 76 // Cache of big powers of 5 as FDBigIntegers. 77 private static final FDBigInteger POW_5_CACHE[]; 78 79 // Archive proxy 80 private static Object[] archivedCaches; 81 82 // Initialize FDBigInteger cache of powers of 5. 83 static { 84 VM.initializeFromArchive(FDBigInteger.class); 85 if (archivedCaches == null) { 86 long[] long5pow = { 87 1L, 88 5L, 89 5L * 5, 90 5L * 5 * 5, 91 5L * 5 * 5 * 5, 92 5L * 5 * 5 * 5 * 5, 93 5L * 5 * 5 * 5 * 5 * 5, 94 5L * 5 * 5 * 5 * 5 * 5 * 5, 95 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5, 96 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 97 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 98 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 99 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 100 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 101 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 102 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 103 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 104 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 105 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 106 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 107 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 108 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 109 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 110 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 111 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 112 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, 113 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, 114 }; 115 int[] small5pow = { 116 1, 117 5, 118 5 * 5, 119 5 * 5 * 5, 120 5 * 5 * 5 * 5, 121 5 * 5 * 5 * 5 * 5, 122 5 * 5 * 5 * 5 * 5 * 5, 123 5 * 5 * 5 * 5 * 5 * 5 * 5, 124 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 125 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 126 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 127 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 128 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 129 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 130 }; 131 FDBigInteger[] pow5cache = new FDBigInteger[MAX_FIVE_POW]; 132 int i = 0; 133 while (i < small5pow.length) { 134 FDBigInteger pow5 = new FDBigInteger(new int[] { small5pow[i] }, 0); 135 pow5.makeImmutable(); 136 pow5cache[i] = pow5; 137 i++; 138 } 139 FDBigInteger prev = pow5cache[i - 1]; 140 while (i < MAX_FIVE_POW) { 141 pow5cache[i] = prev = prev.mult(5); 142 prev.makeImmutable(); 143 i++; 144 } 145 FDBigInteger zero = new FDBigInteger(new int[0], 0); 146 zero.makeImmutable(); 147 archivedCaches = new Object[] {small5pow, long5pow, pow5cache, zero}; 148 } 149 SMALL_5_POW = (int[])archivedCaches[0]; 150 LONG_5_POW = (long[])archivedCaches[1]; 151 POW_5_CACHE = (FDBigInteger[])archivedCaches[2]; 152 ZERO = (FDBigInteger)archivedCaches[3]; 153 } 154 155 // Zero as an FDBigInteger. 156 public static final FDBigInteger ZERO; 157 158 // Constant for casting an int to a long via bitwise AND. 159 private static final long LONG_MASK = 0xffffffffL; 160 161 //@ spec_public non_null; 162 private int data[]; // value: data[0] is least significant 163 //@ spec_public; 164 private int offset; // number of least significant zero padding ints 165 //@ spec_public; 166 private int nWords; // data[nWords-1]!=0, all values above are zero 167 // if nWords==0 -> this FDBigInteger is zero 168 //@ spec_public; 169 private boolean isImmutable = false; 170 171 /*@ 172 @ public invariant 0 <= nWords && nWords <= data.length && offset >= 0; 173 @ public invariant nWords == 0 ==> offset == 0; 174 @ public invariant nWords > 0 ==> data[nWords - 1] != 0; 175 @ public invariant (\forall int i; nWords <= i && i < data.length; data[i] == 0); 176 @ public pure model \bigint value() {