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() {
|