< prev index next >

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

Print this page
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() {


< prev index next >