1 /*
2 * Copyright 2018-2020 Raffaello Giulietti
3 *
4 * Permission is hereby granted, free of charge, to any person obtaining a copy
5 * of this software and associated documentation files (the "Software"), to deal
6 * in the Software without restriction, including without limitation the rights
7 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
8 * copies of the Software, and to permit persons to whom the Software is
9 * furnished to do so, subject to the following conditions:
10 *
11 * The above copyright notice and this permission notice shall be included in
12 * all copies or substantial portions of the Software.
13 *
14 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
15 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
16 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
17 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
18 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
19 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
20 * THE SOFTWARE.
21 */
22
23 package jdk.internal.math;
24
25 import java.math.BigInteger;
26
27 import static java.lang.Double.*;
28 import static java.lang.Long.numberOfTrailingZeros;
29 import static java.lang.StrictMath.scalb;
30 import static java.math.BigInteger.*;
31 import static jdk.internal.math.MathUtils.*;
32
33 public class MathUtilsChecker extends BasicChecker {
34
35 private static final BigInteger THREE = valueOf(3);
36
37 // binary constants
38 private static final int P =
39 numberOfTrailingZeros(doubleToRawLongBits(3)) + 2;
40 private static final int W = (SIZE - 1) - (P - 1);
41 private static final int Q_MIN = (-1 << W - 1) - P + 3;
42 private static final int Q_MAX = (1 << W - 1) - P;
43 private static final long C_MIN = 1L << P - 1;
44 private static final long C_MAX = (1L << P) - 1;
45
46 // decimal constants
47 private static final int K_MIN = flog10pow2(Q_MIN);
48 private static final int K_MAX = flog10pow2(Q_MAX);
49 private static final int H = flog10pow2(P) + 2;
50
51 /*
52 Let
53 10^(-k) = beta 2^r
54 for the unique integer r and real beta meeting
55 2^125 <= beta < 2^126
56 Further, let g = g1 2^63 + g0.
57 Checks that:
58 2^62 <= g1 < 2^63,
59 0 <= g0 < 2^63,
60 g - 1 <= beta < g, (that is, g = floor(beta) + 1)
61 The last predicate, after multiplying by 2^r, is equivalent to
62 (g - 1) 2^r <= 10^(-k) < g 2^r
63 This is the predicate that will be checked in various forms.
64 */
65 private static void testG(int k, long g1, long g0) {
66 // 2^62 <= g1 < 2^63, 0 <= g0 < 2^63
67 assertTrue(g1 << 1 < 0 && g1 >= 0 && g0 >= 0, "g");
68
69 BigInteger g = valueOf(g1).shiftLeft(63).or(valueOf(g0));
70 // double check that 2^125 <= g < 2^126
71 assertTrue(g.signum() > 0 && g.bitLength() == 126, "g");
72
73 // see javadoc of MathUtils.g1(int)
74 int r = flog2pow10(-k) - 125;
75
76 /*
77 The predicate
78 (g - 1) 2^r <= 10^(-k) < g 2^r
79 is equivalent to
80 g - 1 <= 10^(-k) 2^(-r) < g
81 When
82 k <= 0 & r < 0
83 all numerical subexpressions are integer-valued. This is the same as
84 g - 1 = 10^(-k) 2^(-r)
85 */
86 if (k <= 0 && r < 0) {
87 assertTrue(
88 g.subtract(ONE).compareTo(TEN.pow(-k).shiftLeft(-r)) == 0,
89 "g");
90 return;
91 }
92
93 /*
94 The predicate
95 (g - 1) 2^r <= 10^(-k) < g 2^r
96 is equivalent to
97 g 10^k - 10^k <= 2^(-r) < g 10^k
98 When
99 k > 0 & r < 0
100 all numerical subexpressions are integer-valued.
101 */
102 if (k > 0 && r < 0) {
103 BigInteger pow5 = TEN.pow(k);
104 BigInteger mhs = ONE.shiftLeft(-r);
105 BigInteger rhs = g.multiply(pow5);
106 assertTrue(rhs.subtract(pow5).compareTo(mhs) <= 0
107 && mhs.compareTo(rhs) < 0,
108 "g");
109 return;
110 }
111
112 /*
113 Finally, when
114 k <= 0 & r >= 0
115 the predicate
116 (g - 1) 2^r <= 10^(-k) < g 2^r
117 can be used straightforwardly as all numerical subexpressions are
118 already integer-valued.
119 */
120 if (k <= 0) {
121 BigInteger mhs = TEN.pow(-k);
122 assertTrue(g.subtract(ONE).shiftLeft(r).compareTo(mhs) <= 0 &&
123 mhs.compareTo(g.shiftLeft(r)) < 0,
124 "g");
125 return;
126 }
127
128 /*
129 For combinatorial reasons, the only remaining case is
130 k > 0 & r >= 0
131 which, however, cannot arise. Indeed, the predicate
132 (g - 1) 2^r <= 10^(-k) < g 2^r
133 has a positive integer left-hand side and a middle side < 1,
134 which cannot hold.
135 */
136 assertTrue(false, "g");
137 }
138
139 /*
140 Verifies the soundness of the values returned by g1() and g0().
141 */
142 private static void testG() {
143 for (int k = MathUtils.K_MIN; k <= MathUtils.K_MAX; ++k) {
144 testG(k, g1(k), g0(k));
145 }
146 }
147
148 /*
149 Let
150 k = floor(log10(3/4 2^e))
151 The method verifies that
152 k = flog10threeQuartersPow2(e), Q_MIN <= e <= Q_MAX
153 This range covers all binary exponents of doubles and floats.
154
155 The first equation above is equivalent to
156 10^k <= 3 2^(e-2) < 10^(k+1)
157 Equality never holds. Henceforth, the predicate to check is
158 10^k < 3 2^(e-2) < 10^(k+1)
159 This will be transformed in various ways for checking purposes.
160
161 For integer n > 0, let further
162 b = len2(n)
163 denote its length in bits. This means exactly the same as
164 2^(b-1) <= n < 2^b
165 */
166 private static void testFlog10threeQuartersPow2() {
167 // First check the case e = 1
168 assertTrue(flog10threeQuartersPow2(1) == 0,
169 "flog10threeQuartersPow2");
170
171 /*
172 Now check the range Q_MIN <= e <= 0.
173 By rewriting, the predicate to check is equivalent to
174 3 10^(-k-1) < 2^(2-e) < 3 10^(-k)
175 As e <= 0, it follows that 2^(2-e) >= 4 and the right inequality
176 implies k < 0, so the powers of 10 are integers.
177
178 The left inequality is equivalent to
179 len2(3 10^(-k-1)) <= 2 - e
180 and the right inequality to
181 2 - e < len2(3 10^(-k))
182 The original predicate is therefore equivalent to
183 len2(3 10^(-k-1)) <= 2 - e < len2(3 10^(-k))
184
185 Starting with e = 0 and decrementing until the lower bound, the code
186 keeps track of the two powers of 10 to avoid recomputing them.
187 This is easy because at each iteration k changes at most by 1. A simple
188 multiplication by 10 computes the next power of 10 when needed.
189 */
190 int e = 0;
191 int k0 = flog10threeQuartersPow2(e);
192 assertTrue(k0 < 0, "flog10threeQuartersPow2");
193 BigInteger l = THREE.multiply(TEN.pow(-k0 - 1));
194 BigInteger u = l.multiply(TEN);
195 for (;;) {
196 assertTrue(l.bitLength() <= 2 - e & 2 - e < u.bitLength(),
197 "flog10threeQuartersPow2");
198 --e;
199 if (e < Q_MIN) {
200 break;
201 }
202 int kp = flog10threeQuartersPow2(e);
203 assertTrue(kp <= k0, "flog10threeQuartersPow2");
204 if (kp < k0) {
205 // k changes at most by 1 at each iteration, hence:
206 assertTrue(k0 - kp == 1, "flog10threeQuartersPow2");
207 k0 = kp;
208 l = u;
209 u = u.multiply(TEN);
210 }
211 }
212
213 /*
214 Finally, check the range 2 <= e <= Q_MAX.
215 In predicate
216 10^k < 3 2^(e-2) < 10^(k+1)
217 the right inequality shows that k >= 0 as soon as e >= 2.
218 It is equivalent to
219 10^k / 3 < 2^(e-2) < 10^(k+1) / 3
220 Both the powers of 10 and the powers of 2 are integers.
221 The left inequality is therefore equivalent to
222 floor(10^k / 3) < 2^(e-2)
223 and thus to
224 len2(floor(10^k / 3)) <= e - 2
225 while the right inequality is equivalent to
226 2^(e-2) <= floor(10^(k+1) / 3)
227 and hence to
228 e - 2 < len2(floor(10^(k+1) / 3))
229 These are summarized as
230 len2(floor(10^k / 3)) <= e - 2 < len2(floor(10^(k+1) / 3))
231 */
232 e = 2;
233 k0 = flog10threeQuartersPow2(e);
234 assertTrue(k0 >= 0, "flog10threeQuartersPow2");
235 BigInteger l10 = TEN.pow(k0);
236 BigInteger u10 = l10.multiply(TEN);
237 l = l10.divide(THREE);
238 u = u10.divide(THREE);
239 for (;;) {
240 assertTrue(l.bitLength() <= e - 2 & e - 2 < u.bitLength(),
241 "flog10threeQuartersPow2");
242 ++e;
243 if (e > Q_MAX) {
244 break;
245 }
246 int kp = flog10threeQuartersPow2(e);
247 assertTrue(kp >= k0, "flog10threeQuartersPow2");
248 if (kp > k0) {
249 // k changes at most by 1 at each iteration, hence:
250 assertTrue(kp - k0 == 1, "flog10threeQuartersPow2");
251 k0 = kp;
252 u10 = u10.multiply(TEN);
253 l = u;
254 u = u10.divide(THREE);
255 }
256 }
257 }
258
259 /*
260 Let
261 k = floor(log10(2^e))
262 The method verifies that
263 k = flog10pow2(e), Q_MIN <= e <= Q_MAX
264 This range covers all binary exponents of doubles and floats.
265
266 The first equation above is equivalent to
267 10^k <= 2^e < 10^(k+1)
268 Equality holds iff e = k = 0.
269 Henceforth, the predicates to check are equivalent to
270 k = 0, if e = 0
271 10^k < 2^e < 10^(k+1), otherwise
272 The latter will be transformed in various ways for checking purposes.
273
274 For integer n > 0, let further
275 b = len2(n)
276 denote its length in bits. This means exactly the same as
277 2^(b-1) <= n < 2^b
278 */
279 private static void testFlog10pow2() {
280 // First check the case e = 0
281 assertTrue(flog10pow2(0) == 0, "flog10pow2");
282
283 /*
284 Now check the range F * Q_MIN <= e < 0.
285 By inverting all quantities, the predicate to check is equivalent to
286 10^(-k-1) < 2^(-e) < 10^(-k)
287 As e < 0, it follows that 2^(-e) >= 2 and the right inequality
288 implies k < 0.
289 The left inequality means exactly the same as
290 len2(10^(-k-1)) <= -e
291 Similarly, the right inequality is equivalent to
292 -e < len2(10^(-k))
293 The original predicate is therefore equivalent to
294 len2(10^(-k-1)) <= -e < len2(10^(-k))
295 The powers of 10 are integers because k < 0.
296
297 Starting with e = -1 and decrementing towards the lower bound, the code
298 keeps track of the two powers of 10 so as to avoid recomputing them.
299 This is easy because at each iteration k changes at most by 1. A simple
300 multiplication by 10 computes the next power of 10 when needed.
301 */
302 int e = -1;
303 int k = flog10pow2(e);
304 assertTrue(k < 0, "flog10pow2");
305 BigInteger l = TEN.pow(-k - 1);
306 BigInteger u = l.multiply(TEN);
307 for (;;) {
308 assertTrue(l.bitLength() <= -e & -e < u.bitLength(),
309 "flog10pow2");
310 --e;
311 if (e < Q_MIN) {
312 break;
313 }
314 int kp = flog10pow2(e);
315 assertTrue(kp <= k, "flog10pow2");
316 if (kp < k) {
317 // k changes at most by 1 at each iteration, hence:
318 assertTrue(k - kp == 1, "flog10pow2");
319 k = kp;
320 l = u;
321 u = u.multiply(TEN);
322 }
323 }
324
325 /*
326 Finally, in a similar vein, check the range 0 <= e <= Q_MAX.
327 In predicate
328 10^k < 2^e < 10^(k+1)
329 the right inequality shows that k >= 0.
330 The left inequality means the same as
331 len2(10^k) <= e
332 and the right inequality holds iff
333 e < len2(10^(k+1))
334 The original predicate is thus equivalent to
335 len2(10^k) <= e < len2(10^(k+1))
336 As k >= 0, the powers of 10 are integers.
337 */
338 e = 1;
339 k = flog10pow2(e);
340 assertTrue(k >= 0, "flog10pow2");
341 l = TEN.pow(k);
342 u = l.multiply(TEN);
343 for (;;) {
344 assertTrue(l.bitLength() <= e & e < u.bitLength(),
345 "flog10pow2");
346 ++e;
347 if (e > Q_MAX) {
348 break;
349 }
350 int kp = flog10pow2(e);
351 assertTrue(kp >= k, "flog10pow2");
352 if (kp > k) {
353 // k changes at most by 1 at each iteration, hence:
354 assertTrue(kp - k == 1, "flog10pow2");
355 k = kp;
356 l = u;
357 u = u.multiply(TEN);
358 }
359 }
360 }
361
362 /*
363 Let
364 k = floor(log2(10^e))
365 The method verifies that
366 k = flog2pow10(e), -K_MAX <= e <= -K_MIN
367 This range covers all decimal exponents of doubles and floats.
368
369 The first equation above is equivalent to
370 2^k <= 10^e < 2^(k+1)
371 Equality holds iff e = 0, implying k = 0.
372 Henceforth, the equivalent predicates to check are
373 k = 0, if e = 0
374 2^k < 10^e < 2^(k+1), otherwise
375 The latter will be transformed in various ways for checking purposes.
376
377 For integer n > 0, let further
378 b = len2(n)
379 denote its length in bits. This means exactly the same as
380 2^(b-1) <= n < 2^b
381 */
382 private static void testFlog2pow10() {
383 // First check the case e = 0
384 assertTrue(flog2pow10(0) == 0, "flog2pow10");
385
386 /*
387 Now check the range K_MIN <= e < 0.
388 By inverting all quantities, the predicate to check is equivalent to
389 2^(-k-1) < 10^(-e) < 2^(-k)
390 As e < 0, this leads to 10^(-e) >= 10 and the right inequality implies
391 k <= -4.
392 The above means the same as
393 len2(10^(-e)) = -k
394 The powers of 10 are integer values since e < 0.
395 */
396 int e = -1;
397 int k0 = flog2pow10(e);
398 assertTrue(k0 <= -4, "flog2pow10");
399 BigInteger l = TEN;
400 for (;;) {
401 assertTrue(l.bitLength() == -k0, "flog2pow10");
402 --e;
403 if (e < -K_MAX) {
404 break;
405 }
406 k0 = flog2pow10(e);
407 l = l.multiply(TEN);
408 }
409
410 /*
411 Finally check the range 0 < e <= K_MAX.
412 From the predicate
413 2^k < 10^e < 2^(k+1)
414 as e > 0, it follows that 10^e >= 10 and the right inequality implies
415 k >= 3.
416 The above means the same as
417 len2(10^e) = k + 1
418 The powers of 10 are all integer valued, as e > 0.
419 */
420 e = 1;
421 k0 = flog2pow10(e);
422 assertTrue(k0 >= 3, "flog2pow10");
423 l = TEN;
424 for (;;) {
425 assertTrue(l.bitLength() == k0 + 1, "flog2pow10");
426 ++e;
427 if (e > -K_MIN) {
428 break;
429 }
430 k0 = flog2pow10(e);
431 l = l.multiply(TEN);
432 }
433 }
434
435 private static void testBinaryConstants() {
436 assertTrue((long) (double) C_MIN == C_MIN, "C_MIN");
437 assertTrue((long) (double) C_MAX == C_MAX, "C_MAX");
438 assertTrue(scalb(1.0, Q_MIN) == MIN_VALUE, "MIN_VALUE");
439 assertTrue(scalb((double) C_MIN, Q_MIN) == MIN_NORMAL, "MIN_NORMAL");
440 assertTrue(scalb((double) C_MAX, Q_MAX) == MAX_VALUE, "MAX_VALUE");
441 }
442
443 private static void testDecimalConstants() {
444 assertTrue(K_MIN == MathUtils.K_MIN, "K_MIN");
445 assertTrue(K_MAX == MathUtils.K_MAX, "K_MAX");
446 assertTrue(H == MathUtils.H, "H");
447 }
448
449 private static void testPow10() {
450 int e = 0;
451 long pow = 1;
452 for (; e <= H; e += 1, pow *= 10) {
453 assertTrue(pow == pow10(e), "pow10");
454 }
455 }
456
457 public static void test() {
458 testBinaryConstants();
459 testFlog10pow2();
460 testFlog10threeQuartersPow2();
461 testDecimalConstants();
462 testFlog2pow10();
463 testPow10();
464 testG();
465 }
466
467 public static void main(String[] args) {
468 test();
469 }
470
471 }