1694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak/* 2694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Copyright (c) 2013, Oracle and/or its affiliates. All rights reserved. 3694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER. 4694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 5694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * This code is free software; you can redistribute it and/or modify it 6694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * under the terms of the GNU General Public License version 2 only, as 7694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * published by the Free Software Foundation. Oracle designates this 8694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * particular file as subject to the "Classpath" exception as provided 9694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * by Oracle in the LICENSE file that accompanied this code. 10694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 11694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * This code is distributed in the hope that it will be useful, but WITHOUT 12694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 13694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License 14694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * version 2 for more details (a copy is included in the LICENSE file that 15694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * accompanied this code). 16694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 17694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * You should have received a copy of the GNU General Public License version 18694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 2 along with this work; if not, write to the Free Software Foundation, 19694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA. 20694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 21694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA 22694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * or visit www.oracle.com if you need additional information or have any 23694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * questions. 24694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 25694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniakpackage sun.misc; 26694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 27694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniakimport java.math.BigInteger; 28694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniakimport java.util.Arrays; 29694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak//@ model import org.jmlspecs.models.JMLMath; 30694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 31694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak/** 32694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * A simple big integer package specifically for floating point base conversion. 33694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 34694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniakpublic /*@ spec_bigint_math @*/ class FDBigInteger { 35694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 36694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // 37694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // This class contains many comments that start with "/*@" mark. 38694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // They are behavourial specification in 39694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // the Java Modelling Language (JML): 40694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // http://www.eecs.ucf.edu/~leavens/JML//index.shtml 41694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // 42694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 43694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 44694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ public pure model static \bigint UNSIGNED(int v) { 45694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ return v >= 0 ? v : v + (((\bigint)1) << 32); 46694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ } 47694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 48694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ public pure model static \bigint UNSIGNED(long v) { 49694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ return v >= 0 ? v : v + (((\bigint)1) << 64); 50694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ } 51694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 52694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ public pure model static \bigint AP(int[] data, int len) { 53694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ return (\sum int i; 0 <= 0 && i < len; UNSIGNED(data[i]) << (i*32)); 54694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ } 55694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 56694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ public pure model static \bigint pow52(int p5, int p2) { 57694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ghost \bigint v = 1; 58694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ for (int i = 0; i < p5; i++) v *= 5; 59694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ return v << p2; 60694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ } 61694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 62694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ public pure model static \bigint pow10(int p10) { 63694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ return pow52(p10, p10); 64694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ } 65694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 66694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 67694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak static final int[] SMALL_5_POW = { 68694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1, 69694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5, 70694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5 * 5, 71694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5 * 5 * 5, 72694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5 * 5 * 5 * 5, 73694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5 * 5 * 5 * 5 * 5, 74694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5 * 5 * 5 * 5 * 5 * 5, 75694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5 * 5 * 5 * 5 * 5 * 5 * 5, 76694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 77694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 78694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 79694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 80694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 81694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 82694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak }; 83694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 84694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak static final long[] LONG_5_POW = { 85694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1L, 86694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L, 87694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5, 88694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5, 89694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5, 90694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5, 91694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5, 92694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5, 93694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5, 94694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 95694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 96694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 97694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 98694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 99694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 100694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 101694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 102694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 103694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 104694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 105694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 106694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 107694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 108694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 109694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 5L * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5 * 5, 110694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 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, 111694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 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, 112694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak }; 113694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 114694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // Maximum size of cache of powers of 5 as FDBigIntegers. 115694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private static final int MAX_FIVE_POW = 340; 116694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 117694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // Cache of big powers of 5 as FDBigIntegers. 118694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private static final FDBigInteger POW_5_CACHE[]; 119694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 120694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // Initialize FDBigInteger cache of powers of 5. 121694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak static { 122694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak POW_5_CACHE = new FDBigInteger[MAX_FIVE_POW]; 123694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int i = 0; 124694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak while (i < SMALL_5_POW.length) { 125694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak FDBigInteger pow5 = new FDBigInteger(new int[]{SMALL_5_POW[i]}, 0); 126694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak pow5.makeImmutable(); 127694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak POW_5_CACHE[i] = pow5; 128694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak i++; 129694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 130694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak FDBigInteger prev = POW_5_CACHE[i - 1]; 131694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak while (i < MAX_FIVE_POW) { 132694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak POW_5_CACHE[i] = prev = prev.mult(5); 133694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak prev.makeImmutable(); 134694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak i++; 135694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 136694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 137694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 138694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // Zero as an FDBigInteger. 139694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public static final FDBigInteger ZERO = new FDBigInteger(new int[0], 0); 140694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 141694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // Ensure ZERO is immutable. 142694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak static { 143694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak ZERO.makeImmutable(); 144694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 145694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 146694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // Constant for casting an int to a long via bitwise AND. 147694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private final static long LONG_MASK = 0xffffffffL; 148694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 149694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ spec_public non_null; 150694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private int data[]; // value: data[0] is least significant 151694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ spec_public; 152694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private int offset; // number of least significant zero padding ints 153694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ spec_public; 154694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private int nWords; // data[nWords-1]!=0, all values above are zero 155694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // if nWords==0 -> this FDBigInteger is zero 156694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ spec_public; 157694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private boolean isImmutable = false; 158694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 159694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 160694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ public invariant 0 <= nWords && nWords <= data.length && offset >= 0; 161694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ public invariant nWords == 0 ==> offset == 0; 162694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ public invariant nWords > 0 ==> data[nWords - 1] != 0; 163694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ public invariant (\forall int i; nWords <= i && i < data.length; data[i] == 0); 164694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ public pure model \bigint value() { 165694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ return AP(data, nWords) << (offset*32); 166694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ } 167694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 168694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 169694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 170694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Constructs an <code>FDBigInteger</code> from data and padding. The 171694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code>data</code> parameter has the least significant <code>int</code> at 172694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * the zeroth index. The <code>offset</code> parameter gives the number of 173694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * zero <code>int</code>s to be inferred below the least significant element 174694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * of <code>data</code>. 175694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 176694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param data An array containing all non-zero <code>int</code>s of the value. 177694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param offset An offset indicating the number of zero <code>int</code>s to pad 178694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * below the least significant element of <code>data</code>. 179694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 180694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 181694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires data != null && offset >= 0; 182694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures this.value() == \old(AP(data, data.length) << (offset*32)); 183694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures this.data == \old(data); 184694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 185694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private FDBigInteger(int[] data, int offset) { 186694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak this.data = data; 187694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak this.offset = offset; 188694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak this.nWords = data.length; 189694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak trimLeadingZeros(); 190694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 191694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 192694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 193694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Constructs an <code>FDBigInteger</code> from a starting value and some 194694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * decimal digits. 195694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 196694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param lValue The starting value. 197694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param digits The decimal digits. 198694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param kDigits The initial index into <code>digits</code>. 199694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param nDigits The final index into <code>digits</code>. 200694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 201694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 202694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires digits != null; 203694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires 0 <= kDigits && kDigits <= nDigits && nDigits <= digits.length; 204694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires (\forall int i; 0 <= i && i < nDigits; '0' <= digits[i] && digits[i] <= '9'); 205694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures this.value() == \old(lValue * pow10(nDigits - kDigits) + (\sum int i; kDigits <= i && i < nDigits; (digits[i] - '0') * pow10(nDigits - i - 1))); 206694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 207694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public FDBigInteger(long lValue, char[] digits, int kDigits, int nDigits) { 208694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int n = Math.max((nDigits + 8) / 9, 2); // estimate size needed. 209694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak data = new int[n]; // allocate enough space 210694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak data[0] = (int) lValue; // starting value 211694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak data[1] = (int) (lValue >>> 32); 212694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak offset = 0; 213694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak nWords = 2; 214694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int i = kDigits; 215694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int limit = nDigits - 5; // slurp digits 5 at a time. 216694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int v; 217694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak while (i < limit) { 218694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int ilim = i + 5; 219694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v = (int) digits[i++] - (int) '0'; 220694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak while (i < ilim) { 221694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v = 10 * v + (int) digits[i++] - (int) '0'; 222694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 223694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak multAddMe(100000, v); // ... where 100000 is 10^5. 224694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 225694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int factor = 1; 226694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v = 0; 227694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak while (i < nDigits) { 228694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v = 10 * v + (int) digits[i++] - (int) '0'; 229694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak factor *= 10; 230694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 231694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (factor != 1) { 232694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak multAddMe(factor, v); 233694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 234694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak trimLeadingZeros(); 235694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 236694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 237694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 238694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Returns an <code>FDBigInteger</code> with the numerical value 239694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code>5<sup>p5</sup> * 2<sup>p2</sup></code>. 240694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 241694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param p5 The exponent of the power-of-five factor. 242694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param p2 The exponent of the power-of-two factor. 243694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return <code>5<sup>p5</sup> * 2<sup>p2</sup></code> 244694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 245694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 246694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires p5 >= 0 && p2 >= 0; 247694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 248694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(pow52(p5, p2)); 249694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 250694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public static FDBigInteger valueOfPow52(int p5, int p2) { 251694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (p5 != 0) { 252694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (p2 == 0) { 253694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return big5pow(p5); 254694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else if (p5 < SMALL_5_POW.length) { 255694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int pow5 = SMALL_5_POW[p5]; 256694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int wordcount = p2 >> 5; 257694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int bitcount = p2 & 0x1f; 258694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (bitcount == 0) { 259694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(new int[]{pow5}, wordcount); 260694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 261694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(new int[]{ 262694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak pow5 << bitcount, 263694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak pow5 >>> (32 - bitcount) 264694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak }, wordcount); 265694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 266694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 267694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return big5pow(p5).leftShift(p2); 268694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 269694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 270694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return valueOfPow2(p2); 271694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 272694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 273694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 274694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 275694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Returns an <code>FDBigInteger</code> with the numerical value 276694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code>value * 5<sup>p5</sup> * 2<sup>p2</sup></code>. 277694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 278694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param value The constant factor. 279694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param p5 The exponent of the power-of-five factor. 280694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param p2 The exponent of the power-of-two factor. 281694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return <code>value * 5<sup>p5</sup> * 2<sup>p2</sup></code> 282694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 283694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 284694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires p5 >= 0 && p2 >= 0; 285694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 286694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(UNSIGNED(value) * pow52(p5, p2)); 287694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 288694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public static FDBigInteger valueOfMulPow52(long value, int p5, int p2) { 289694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak assert p5 >= 0 : p5; 290694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak assert p2 >= 0 : p2; 291694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int v0 = (int) value; 292694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int v1 = (int) (value >>> 32); 293694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int wordcount = p2 >> 5; 294694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int bitcount = p2 & 0x1f; 295694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (p5 != 0) { 296694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (p5 < SMALL_5_POW.length) { 297694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long pow5 = SMALL_5_POW[p5] & LONG_MASK; 298694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long carry = (v0 & LONG_MASK) * pow5; 299694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v0 = (int) carry; 300694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak carry >>>= 32; 301694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak carry = (v1 & LONG_MASK) * pow5 + carry; 302694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v1 = (int) carry; 303694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int v2 = (int) (carry >>> 32); 304694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (bitcount == 0) { 305694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(new int[]{v0, v1, v2}, wordcount); 306694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 307694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(new int[]{ 308694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v0 << bitcount, 309694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak (v1 << bitcount) | (v0 >>> (32 - bitcount)), 310694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak (v2 << bitcount) | (v1 >>> (32 - bitcount)), 311694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v2 >>> (32 - bitcount) 312694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak }, wordcount); 313694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 314694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 315694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak FDBigInteger pow5 = big5pow(p5); 316694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] r; 317694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (v1 == 0) { 318694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak r = new int[pow5.nWords + 1 + ((p2 != 0) ? 1 : 0)]; 319694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak mult(pow5.data, pow5.nWords, v0, r); 320694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 321694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak r = new int[pow5.nWords + 2 + ((p2 != 0) ? 1 : 0)]; 322694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak mult(pow5.data, pow5.nWords, v0, v1, r); 323694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 324694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return (new FDBigInteger(r, pow5.offset)).leftShift(p2); 325694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 326694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else if (p2 != 0) { 327694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (bitcount == 0) { 328694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(new int[]{v0, v1}, wordcount); 329694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 330694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(new int[]{ 331694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v0 << bitcount, 332694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak (v1 << bitcount) | (v0 >>> (32 - bitcount)), 333694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v1 >>> (32 - bitcount) 334694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak }, wordcount); 335694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 336694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 337694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(new int[]{v0, v1}, 0); 338694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 339694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 340694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 341694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Returns an <code>FDBigInteger</code> with the numerical value 342694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code>2<sup>p2</sup></code>. 343694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 344694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param p2 The exponent of 2. 345694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return <code>2<sup>p2</sup></code> 346694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 347694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 348694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires p2 >= 0; 349694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 350694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == pow52(0, p2); 351694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 352694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private static FDBigInteger valueOfPow2(int p2) { 353694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int wordcount = p2 >> 5; 354694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int bitcount = p2 & 0x1f; 355694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(new int[]{1 << bitcount}, wordcount); 356694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 357694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 358694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 359694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Removes all leading zeros from this <code>FDBigInteger</code> adjusting 360694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * the offset and number of non-zero leading words accordingly. 361694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 362694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 363694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires data != null; 364694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires 0 <= nWords && nWords <= data.length && offset >= 0; 365694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires nWords == 0 ==> offset == 0; 366694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures nWords == 0 ==> offset == 0; 367694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures nWords > 0 ==> data[nWords - 1] != 0; 368694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 369694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private /*@ helper @*/ void trimLeadingZeros() { 370694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int i = nWords; 371694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (i > 0 && (data[--i] == 0)) { 372694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //for (; i > 0 && data[i - 1] == 0; i--) ; 373694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak while(i > 0 && data[i - 1] == 0) { 374694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak i--; 375694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 376694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak this.nWords = i; 377694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (i == 0) { // all words are zero 378694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak this.offset = 0; 379694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 380694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 381694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 382694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 383694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 384694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Retrieves the normalization bias of the <code>FDBigIntger</code>. The 385694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * normalization bias is a left shift such that after it the highest word 386694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * of the value will have the 4 highest bits equal to zero: 387694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code>(highestWord & 0xf0000000) == 0</code>, but the next bit should be 1 388694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code>(highestWord & 0x08000000) != 0</code>. 389694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 390694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return The normalization bias. 391694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 392694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 393694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() > 0; 394694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 395694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public /*@ pure @*/ int getNormalizationBias() { 396694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (nWords == 0) { 397694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak throw new IllegalArgumentException("Zero value cannot be normalized"); 398694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 399694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int zeros = Integer.numberOfLeadingZeros(data[nWords - 1]); 400694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return (zeros < 4) ? 28 + zeros : zeros - 4; 401694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 402694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 403694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // TODO: Why is anticount param needed if it is always 32 - bitcount? 404694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 405694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Left shifts the contents of one int array into another. 406694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 407694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param src The source array. 408694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param idx The initial index of the source array. 409694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param result The destination array. 410694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param bitcount The left shift. 411694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param anticount The left anti-shift, e.g., <code>32-bitcount</code>. 412694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param prev The prior source value. 413694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 414694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 415694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires 0 < bitcount && bitcount < 32 && anticount == 32 - bitcount; 416694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires src.length >= idx && result.length > idx; 417694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable result[*]; 418694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures AP(result, \old(idx + 1)) == \old((AP(src, idx) + UNSIGNED(prev) << (idx*32)) << bitcount); 419694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 420694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private static void leftShift(int[] src, int idx, int result[], int bitcount, int anticount, int prev){ 421694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (; idx > 0; idx--) { 422694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int v = (prev << bitcount); 423694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak prev = src[idx - 1]; 424694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v |= (prev >>> anticount); 425694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak result[idx] = v; 426694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 427694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int v = prev << bitcount; 428694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak result[0] = v; 429694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 430694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 431694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 432694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Shifts this <code>FDBigInteger</code> to the left. The shift is performed 433694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * in-place unless the <code>FDBigInteger</code> is immutable in which case 434694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * a new instance of <code>FDBigInteger</code> is returned. 435694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 436694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param shift The number of bits to shift left. 437694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return The shifted <code>FDBigInteger</code>. 438694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 439694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 440694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() == 0 || shift == 0; 441694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 442694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == this; 443694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 444694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 445694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 446694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() > 0 && shift > 0 && this.isImmutable; 447694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 448694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() << shift); 449694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 450694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 451694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 452694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() > 0 && shift > 0 && this.isImmutable; 453694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 454694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == this; 455694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() << shift); 456694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 457694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public FDBigInteger leftShift(int shift) { 458694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (shift == 0 || nWords == 0) { 459694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return this; 460694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 461694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int wordcount = shift >> 5; 462694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int bitcount = shift & 0x1f; 463694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (this.isImmutable) { 464694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (bitcount == 0) { 465694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(Arrays.copyOf(data, nWords), offset + wordcount); 466694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 467694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int anticount = 32 - bitcount; 468694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int idx = nWords - 1; 469694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int prev = data[idx]; 470694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int hi = prev >>> anticount; 471694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] result; 472694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (hi != 0) { 473694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak result = new int[nWords + 1]; 474694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak result[nWords] = hi; 475694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 476694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak result = new int[nWords]; 477694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 478694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak leftShift(data,idx,result,bitcount,anticount,prev); 479694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(result, offset + wordcount); 480694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 481694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 482694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (bitcount != 0) { 483694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int anticount = 32 - bitcount; 484694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if ((data[0] << bitcount) == 0) { 485694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int idx = 0; 486694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int prev = data[idx]; 487694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (; idx < nWords - 1; idx++) { 488694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int v = (prev >>> anticount); 489694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak prev = data[idx + 1]; 490694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v |= (prev << bitcount); 491694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak data[idx] = v; 492694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 493694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int v = prev >>> anticount; 494694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak data[idx] = v; 495694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if(v==0) { 496694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak nWords--; 497694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 498694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak offset++; 499694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 500694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int idx = nWords - 1; 501694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int prev = data[idx]; 502694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int hi = prev >>> anticount; 503694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] result = data; 504694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] src = data; 505694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (hi != 0) { 506694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if(nWords == data.length) { 507694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak data = result = new int[nWords + 1]; 508694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 509694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak result[nWords++] = hi; 510694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 511694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak leftShift(src,idx,result,bitcount,anticount,prev); 512694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 513694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 514694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak offset += wordcount; 515694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return this; 516694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 517694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 518694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 519694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 520694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Returns the number of <code>int</code>s this <code>FDBigInteger</code> represents. 521694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 522694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return Number of <code>int</code>s required to represent this <code>FDBigInteger</code>. 523694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 524694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 525694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() == 0; 526694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == 0; 527694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 528694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 529694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 530694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() > 0; 531694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures ((\bigint)1) << (\result - 1) <= this.value() && this.value() <= ((\bigint)1) << \result; 532694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 533694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private /*@ pure @*/ int size() { 534694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return nWords + offset; 535694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 536694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 537694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 538694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 539694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Computes 540694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <pre> 541694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * q = (int)( this / S ) 542694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * this = 10 * ( this mod S ) 543694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Return q. 544694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * </pre> 545694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * This is the iteration step of digit development for output. 546694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * We assume that S has been normalized, as above, and that 547694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * "this" has been left-shifted accordingly. 548694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Also assumed, of course, is that the result, q, can be expressed 549694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * as an integer, 0 <= q < 10. 550694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 551694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param The divisor of this <code>FDBigInteger</code>. 552694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return <code>q = (int)(this / S)</code>. 553694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 554694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 555694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires !this.isImmutable; 556694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.size() <= S.size(); 557694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.data.length + this.offset >= S.size(); 558694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires S.value() >= ((\bigint)1) << (S.size()*32 - 4); 559694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable this.nWords, this.offset, this.data, this.data[*]; 560694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == \old(this.value() / S.value()); 561694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures this.value() == \old(10 * (this.value() % S.value())); 562694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 563694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public int quoRemIteration(FDBigInteger S) throws IllegalArgumentException { 564694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak assert !this.isImmutable : "cannot modify immutable value"; 565694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // ensure that this and S have the same number of 566694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // digits. If S is properly normalized and q < 10 then 567694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // this must be so. 568694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int thSize = this.size(); 569694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int sSize = S.size(); 570694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (thSize < sSize) { 571694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // this value is significantly less than S, result of division is zero. 572694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // just mult this by 10. 573694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int p = multAndCarryBy10(this.data, this.nWords, this.data); 574694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if(p!=0) { 575694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak this.data[nWords++] = p; 576694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 577694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak trimLeadingZeros(); 578694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 579694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return 0; 580694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else if (thSize > sSize) { 581694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak throw new IllegalArgumentException("disparate values"); 582694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 583694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // estimate q the obvious way. We will usually be 584694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // right. If not, then we're only off by a little and 585694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // will re-add. 586694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long q = (this.data[this.nWords - 1] & LONG_MASK) / (S.data[S.nWords - 1] & LONG_MASK); 587694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long diff = multDiffMe(q, S); 588694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (diff != 0L) { 589694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert q != 0; 590694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert this.offset == \old(Math.min(this.offset, S.offset)); 591694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert this.offset <= S.offset; 592694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 593694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // q is too big. 594694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // add S back in until this turns +. This should 595694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // not be very many times! 596694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long sum = 0L; 597694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int tStart = S.offset - this.offset; 598694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert tStart >= 0; 599694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] sd = S.data; 600694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] td = this.data; 601694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak while (sum == 0L) { 602694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (int sIndex = 0, tIndex = tStart; tIndex < this.nWords; sIndex++, tIndex++) { 603694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak sum += (td[tIndex] & LONG_MASK) + (sd[sIndex] & LONG_MASK); 604694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak td[tIndex] = (int) sum; 605694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak sum >>>= 32; // Signed or unsigned, answer is 0 or 1 606694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 607694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // 608694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // Originally the following line read 609694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // "if ( sum !=0 && sum != -1 )" 610694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // but that would be wrong, because of the 611694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // treatment of the two values as entirely unsigned, 612694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // it would be impossible for a carry-out to be interpreted 613694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // as -1 -- it would have to be a single-bit carry-out, or +1. 614694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // 615694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak assert sum == 0 || sum == 1 : sum; // carry out of division correction 616694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak q -= 1; 617694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 618694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 619694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // finally, we can multiply this by 10. 620694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // it cannot overflow, right, as the high-order word has 621694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // at least 4 high-order zeros! 622694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int p = multAndCarryBy10(this.data, this.nWords, this.data); 623694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak assert p == 0 : p; // Carry out of *10 624694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak trimLeadingZeros(); 625694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return (int) q; 626694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 627694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 628694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 629694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Multiplies this <code>FDBigInteger</code> by 10. The operation will be 630694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * performed in place unless the <code>FDBigInteger</code> is immutable in 631694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * which case a new <code>FDBigInteger</code> will be returned. 632694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 633694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return The <code>FDBigInteger</code> multiplied by 10. 634694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 635694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 636694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() == 0; 637694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 638694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == this; 639694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 640694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 641694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 642694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() > 0 && this.isImmutable; 643694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 644694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() * 10); 645694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 646694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 647694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 648694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() > 0 && !this.isImmutable; 649694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable this.nWords, this.data, this.data[*]; 650694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == this; 651694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() * 10); 652694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 653694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public FDBigInteger multBy10() { 654694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (nWords == 0) { 655694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return this; 656694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 657694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (isImmutable) { 658694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] res = new int[nWords + 1]; 659694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak res[nWords] = multAndCarryBy10(data, nWords, res); 660694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(res, offset); 661694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 662694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int p = multAndCarryBy10(this.data, this.nWords, this.data); 663694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (p != 0) { 664694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (nWords == data.length) { 665694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (data[0] == 0) { 666694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak System.arraycopy(data, 1, data, 0, --nWords); 667694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak offset++; 668694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 669694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak data = Arrays.copyOf(data, data.length + 1); 670694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 671694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 672694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak data[nWords++] = p; 673694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 674694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak trimLeadingZeros(); 675694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 676694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return this; 677694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 678694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 679694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 680694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 681694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Multiplies this <code>FDBigInteger</code> by 682694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code>5<sup>p5</sup> * 2<sup>p2</sup></code>. The operation will be 683694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * performed in place if possible, otherwise a new <code>FDBigInteger</code> 684694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * will be returned. 685694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 686694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param p5 The exponent of the power-of-five factor. 687694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param p2 The exponent of the power-of-two factor. 688694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return 689694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 690694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 691694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() == 0 || p5 == 0 && p2 == 0; 692694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 693694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == this; 694694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 695694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 696694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 697694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() > 0 && (p5 > 0 && p2 >= 0 || p5 == 0 && p2 > 0 && this.isImmutable); 698694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 699694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() * pow52(p5, p2)); 700694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 701694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 702694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 703694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() > 0 && p5 == 0 && p2 > 0 && !this.isImmutable; 704694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable this.nWords, this.data, this.data[*]; 705694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == this; 706694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() * pow52(p5, p2)); 707694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 708694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public FDBigInteger multByPow52(int p5, int p2) { 709694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (this.nWords == 0) { 710694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return this; 711694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 712694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak FDBigInteger res = this; 713694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (p5 != 0) { 714694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] r; 715694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int extraSize = (p2 != 0) ? 1 : 0; 716694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (p5 < SMALL_5_POW.length) { 717694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak r = new int[this.nWords + 1 + extraSize]; 718694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak mult(this.data, this.nWords, SMALL_5_POW[p5], r); 719694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak res = new FDBigInteger(r, this.offset); 720694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 721694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak FDBigInteger pow5 = big5pow(p5); 722694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak r = new int[this.nWords + pow5.size() + extraSize]; 723694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak mult(this.data, this.nWords, pow5.data, pow5.nWords, r); 724694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak res = new FDBigInteger(r, this.offset + pow5.offset); 725694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 726694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 727694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return res.leftShift(p2); 728694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 729694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 730694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 731694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Multiplies two big integers represented as int arrays. 732694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 733694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param s1 The first array factor. 734694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param s1Len The number of elements of <code>s1</code> to use. 735694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param s2 The second array factor. 736694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param s2Len The number of elements of <code>s2</code> to use. 737694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param dst The product array. 738694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 739694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 740694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires s1 != dst && s2 != dst; 741694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires s1.length >= s1Len && s2.length >= s2Len && dst.length >= s1Len + s2Len; 742694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable dst[0 .. s1Len + s2Len - 1]; 743694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures AP(dst, s1Len + s2Len) == \old(AP(s1, s1Len) * AP(s2, s2Len)); 744694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 745694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private static void mult(int[] s1, int s1Len, int[] s2, int s2Len, int[] dst) { 746694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (int i = 0; i < s1Len; i++) { 747694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long v = s1[i] & LONG_MASK; 748694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long p = 0L; 749694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (int j = 0; j < s2Len; j++) { 750694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak p += (dst[i + j] & LONG_MASK) + v * (s2[j] & LONG_MASK); 751694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak dst[i + j] = (int) p; 752694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak p >>>= 32; 753694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 754694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak dst[i + s2Len] = (int) p; 755694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 756694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 757694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 758694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 759694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Subtracts the supplied <code>FDBigInteger</code> subtrahend from this 760694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code>FDBigInteger</code>. Assert that the result is positive. 761694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * If the subtrahend is immutable, store the result in this(minuend). 762694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * If this(minuend) is immutable a new <code>FDBigInteger</code> is created. 763694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 764694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param subtrahend The <code>FDBigInteger</code> to be subtracted. 765694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return This <code>FDBigInteger</code> less the subtrahend. 766694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 767694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 768694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.isImmutable; 769694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() >= subtrahend.value(); 770694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 771694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() - subtrahend.value()); 772694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 773694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 774694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 775694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires !subtrahend.isImmutable; 776694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() >= subtrahend.value(); 777694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable this.nWords, this.offset, this.data, this.data[*]; 778694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == this; 779694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() - subtrahend.value()); 780694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 781694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public FDBigInteger leftInplaceSub(FDBigInteger subtrahend) { 782694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak assert this.size() >= subtrahend.size() : "result should be positive"; 783694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak FDBigInteger minuend; 784694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (this.isImmutable) { 785694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak minuend = new FDBigInteger(this.data.clone(), this.offset); 786694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 787694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak minuend = this; 788694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 789694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int offsetDiff = subtrahend.offset - minuend.offset; 790694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] sData = subtrahend.data; 791694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] mData = minuend.data; 792694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int subLen = subtrahend.nWords; 793694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int minLen = minuend.nWords; 794694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (offsetDiff < 0) { 795694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // need to expand minuend 796694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int rLen = minLen - offsetDiff; 797694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (rLen < mData.length) { 798694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak System.arraycopy(mData, 0, mData, -offsetDiff, minLen); 799694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak Arrays.fill(mData, 0, -offsetDiff, 0); 800694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 801694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] r = new int[rLen]; 802694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak System.arraycopy(mData, 0, r, -offsetDiff, minLen); 803694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak minuend.data = mData = r; 804694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 805694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak minuend.offset = subtrahend.offset; 806694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak minuend.nWords = minLen = rLen; 807694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak offsetDiff = 0; 808694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 809694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long borrow = 0L; 810694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int mIndex = offsetDiff; 811694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (int sIndex = 0; sIndex < subLen && mIndex < minLen; sIndex++, mIndex++) { 812694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long diff = (mData[mIndex] & LONG_MASK) - (sData[sIndex] & LONG_MASK) + borrow; 813694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak mData[mIndex] = (int) diff; 814694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak borrow = diff >> 32; // signed shift 815694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 816694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (; borrow != 0 && mIndex < minLen; mIndex++) { 817694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long diff = (mData[mIndex] & LONG_MASK) + borrow; 818694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak mData[mIndex] = (int) diff; 819694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak borrow = diff >> 32; // signed shift 820694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 821694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak assert borrow == 0L : borrow; // borrow out of subtract, 822694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // result should be positive 823694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak minuend.trimLeadingZeros(); 824694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return minuend; 825694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 826694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 827694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 828694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Subtracts the supplied <code>FDBigInteger</code> subtrahend from this 829694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code>FDBigInteger</code>. Assert that the result is positive. 830694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * If the this(minuend) is immutable, store the result in subtrahend. 831694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * If subtrahend is immutable a new <code>FDBigInteger</code> is created. 832694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 833694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param subtrahend The <code>FDBigInteger</code> to be subtracted. 834694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return This <code>FDBigInteger</code> less the subtrahend. 835694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 836694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 837694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires subtrahend.isImmutable; 838694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() >= subtrahend.value(); 839694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 840694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() - subtrahend.value()); 841694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 842694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 843694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 844694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires !subtrahend.isImmutable; 845694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() >= subtrahend.value(); 846694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable subtrahend.nWords, subtrahend.offset, subtrahend.data, subtrahend.data[*]; 847694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == subtrahend; 848694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() - subtrahend.value()); 849694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 850694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public FDBigInteger rightInplaceSub(FDBigInteger subtrahend) { 851694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak assert this.size() >= subtrahend.size() : "result should be positive"; 852694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak FDBigInteger minuend = this; 853694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (subtrahend.isImmutable) { 854694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak subtrahend = new FDBigInteger(subtrahend.data.clone(), subtrahend.offset); 855694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 856694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int offsetDiff = minuend.offset - subtrahend.offset; 857694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] sData = subtrahend.data; 858694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] mData = minuend.data; 859694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int subLen = subtrahend.nWords; 860694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int minLen = minuend.nWords; 861694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (offsetDiff < 0) { 862694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int rLen = minLen; 863694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (rLen < sData.length) { 864694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak System.arraycopy(sData, 0, sData, -offsetDiff, subLen); 865694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak Arrays.fill(sData, 0, -offsetDiff, 0); 866694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 867694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] r = new int[rLen]; 868694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak System.arraycopy(sData, 0, r, -offsetDiff, subLen); 869694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak subtrahend.data = sData = r; 870694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 871694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak subtrahend.offset = minuend.offset; 872694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak subLen -= offsetDiff; 873694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak offsetDiff = 0; 874694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 875694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int rLen = minLen + offsetDiff; 876694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (rLen >= sData.length) { 877694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak subtrahend.data = sData = Arrays.copyOf(sData, rLen); 878694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 879694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 880694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert minuend == this && minuend.value() == \old(this.value()); 881694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert mData == minuend.data && minLen == minuend.nWords; 882694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert subtrahend.offset + subtrahend.data.length >= minuend.size(); 883694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert sData == subtrahend.data; 884694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert AP(subtrahend.data, subtrahend.data.length) << subtrahend.offset == \old(subtrahend.value()); 885694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert subtrahend.offset == Math.min(\old(this.offset), minuend.offset); 886694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert offsetDiff == minuend.offset - subtrahend.offset; 887694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert 0 <= offsetDiff && offsetDiff + minLen <= sData.length; 888694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int sIndex = 0; 889694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long borrow = 0L; 890694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (; sIndex < offsetDiff; sIndex++) { 891694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long diff = 0L - (sData[sIndex] & LONG_MASK) + borrow; 892694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak sData[sIndex] = (int) diff; 893694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak borrow = diff >> 32; // signed shift 894694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 895694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert sIndex == offsetDiff; 896694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (int mIndex = 0; mIndex < minLen; sIndex++, mIndex++) { 897694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak //@ assert sIndex == offsetDiff + mIndex; 898694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long diff = (mData[mIndex] & LONG_MASK) - (sData[sIndex] & LONG_MASK) + borrow; 899694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak sData[sIndex] = (int) diff; 900694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak borrow = diff >> 32; // signed shift 901694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 902694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak assert borrow == 0L : borrow; // borrow out of subtract, 903694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // result should be positive 904694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak subtrahend.nWords = sIndex; 905694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak subtrahend.trimLeadingZeros(); 906694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return subtrahend; 907694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 908694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 909694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 910694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 911694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Determines whether all elements of an array are zero for all indices less 912694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * than a given index. 913694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 914694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param a The array to be examined. 915694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param from The index strictly below which elements are to be examined. 916694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return Zero if all elements in range are zero, 1 otherwise. 917694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 918694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 919694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires 0 <= from && from <= a.length; 920694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == (AP(a, from) == 0 ? 0 : 1); 921694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 922694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private /*@ pure @*/ static int checkZeroTail(int[] a, int from) { 923694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak while (from > 0) { 924694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (a[--from] != 0) { 925694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return 1; 926694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 927694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 928694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return 0; 929694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 930694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 931694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 932694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Compares the parameter with this <code>FDBigInteger</code>. Returns an 933694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * integer accordingly as: 934694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <pre> 935694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * >0: this > other 936694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 0: this == other 937694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <0: this < other 938694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * </pre> 939694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 940694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param other The <code>FDBigInteger</code> to compare. 941694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return A negative value, zero, or a positive value according to the 942694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * result of the comparison. 943694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 944694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 945694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == (this.value() < other.value() ? -1 : this.value() > other.value() ? +1 : 0); 946694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 947694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public /*@ pure @*/ int cmp(FDBigInteger other) { 948694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int aSize = nWords + offset; 949694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int bSize = other.nWords + other.offset; 950694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (aSize > bSize) { 951694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return 1; 952694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else if (aSize < bSize) { 953694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return -1; 954694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 955694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int aLen = nWords; 956694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int bLen = other.nWords; 957694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak while (aLen > 0 && bLen > 0) { 958694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int a = data[--aLen]; 959694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int b = other.data[--bLen]; 960694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (a != b) { 961694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return ((a & LONG_MASK) < (b & LONG_MASK)) ? -1 : 1; 962694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 963694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 964694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (aLen > 0) { 965694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return checkZeroTail(data, aLen); 966694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 967694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (bLen > 0) { 968694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return -checkZeroTail(other.data, bLen); 969694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 970694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return 0; 971694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 972694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 973694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 974694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Compares this <code>FDBigInteger</code> with 975694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code>5<sup>p5</sup> * 2<sup>p2</sup></code>. 976694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Returns an integer accordingly as: 977694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <pre> 978694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * >0: this > other 979694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 0: this == other 980694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <0: this < other 981694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * </pre> 982694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param p5 The exponent of the power-of-five factor. 983694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param p2 The exponent of the power-of-two factor. 984694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return A negative value, zero, or a positive value according to the 985694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * result of the comparison. 986694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 987694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 988694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires p5 >= 0 && p2 >= 0; 989694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == (this.value() < pow52(p5, p2) ? -1 : this.value() > pow52(p5, p2) ? +1 : 0); 990694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 991694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public /*@ pure @*/ int cmpPow52(int p5, int p2) { 992694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (p5 == 0) { 993694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int wordcount = p2 >> 5; 994694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int bitcount = p2 & 0x1f; 995694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int size = this.nWords + this.offset; 996694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (size > wordcount + 1) { 997694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return 1; 998694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else if (size < wordcount + 1) { 999694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return -1; 1000694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1001694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int a = this.data[this.nWords -1]; 1002694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int b = 1 << bitcount; 1003694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (a != b) { 1004694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return ( (a & LONG_MASK) < (b & LONG_MASK)) ? -1 : 1; 1005694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1006694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return checkZeroTail(this.data, this.nWords - 1); 1007694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1008694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return this.cmp(big5pow(p5).leftShift(p2)); 1009694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1010694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1011694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1012694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Compares this <code>FDBigInteger</code> with <code>x + y</code>. Returns a 1013694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * value according to the comparison as: 1014694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <pre> 1015694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * -1: this < x + y 1016694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 0: this == x + y 1017694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1: this > x + y 1018694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * </pre> 1019694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param x The first addend of the sum to compare. 1020694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param y The second addend of the sum to compare. 1021694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return -1, 0, or 1 according to the result of the comparison. 1022694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1023694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 1024694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == (this.value() < x.value() + y.value() ? -1 : this.value() > x.value() + y.value() ? +1 : 0); 1025694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 1026694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public /*@ pure @*/ int addAndCmp(FDBigInteger x, FDBigInteger y) { 1027694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak FDBigInteger big; 1028694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak FDBigInteger small; 1029694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int xSize = x.size(); 1030694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int ySize = y.size(); 1031694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int bSize; 1032694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int sSize; 1033694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (xSize >= ySize) { 1034694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak big = x; 1035694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak small = y; 1036694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak bSize = xSize; 1037694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak sSize = ySize; 1038694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 1039694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak big = y; 1040694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak small = x; 1041694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak bSize = ySize; 1042694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak sSize = xSize; 1043694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1044694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int thSize = this.size(); 1045694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (bSize == 0) { 1046694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return thSize == 0 ? 0 : 1; 1047694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1048694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (sSize == 0) { 1049694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return this.cmp(big); 1050694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1051694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (bSize > thSize) { 1052694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return -1; 1053694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1054694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (bSize + 1 < thSize) { 1055694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return 1; 1056694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1057694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long top = (big.data[big.nWords - 1] & LONG_MASK); 1058694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (sSize == bSize) { 1059694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak top += (small.data[small.nWords - 1] & LONG_MASK); 1060694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1061694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if ((top >>> 32) == 0) { 1062694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (((top + 1) >>> 32) == 0) { 1063694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // good case - no carry extension 1064694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (bSize < thSize) { 1065694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return 1; 1066694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1067694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // here sum.nWords == this.nWords 1068694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long v = (this.data[this.nWords - 1] & LONG_MASK); 1069694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (v < top) { 1070694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return -1; 1071694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1072694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (v > top + 1) { 1073694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return 1; 1074694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1075694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1076694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { // (top>>>32)!=0 guaranteed carry extension 1077694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (bSize + 1 > thSize) { 1078694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return -1; 1079694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1080694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // here sum.nWords == this.nWords 1081694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak top >>>= 32; 1082694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long v = (this.data[this.nWords - 1] & LONG_MASK); 1083694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (v < top) { 1084694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return -1; 1085694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1086694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (v > top + 1) { 1087694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return 1; 1088694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1089694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1090694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return this.cmp(big.add(small)); 1091694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1092694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1093694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1094694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Makes this <code>FDBigInteger</code> immutable. 1095694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1096694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 1097694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable this.isImmutable; 1098694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures this.isImmutable; 1099694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 1100694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public void makeImmutable() { 1101694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak this.isImmutable = true; 1102694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1103694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1104694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1105694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Multiplies this <code>FDBigInteger</code> by an integer. 1106694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1107694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param i The factor by which to multiply this <code>FDBigInteger</code>. 1108694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return This <code>FDBigInteger</code> multiplied by an integer. 1109694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1110694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 1111694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() == 0; 1112694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 1113694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == this; 1114694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 1115694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 1116694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 1117694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() != 0; 1118694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 1119694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() * UNSIGNED(i)); 1120694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 1121694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private FDBigInteger mult(int i) { 1122694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (this.nWords == 0) { 1123694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return this; 1124694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1125694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] r = new int[nWords + 1]; 1126694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak mult(data, nWords, i, r); 1127694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(r, offset); 1128694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1129694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1130694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1131694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Multiplies this <code>FDBigInteger</code> by another <code>FDBigInteger</code>. 1132694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1133694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param other The <code>FDBigInteger</code> factor by which to multiply. 1134694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return The product of this and the parameter <code>FDBigInteger</code>s. 1135694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1136694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 1137694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() == 0; 1138694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 1139694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == this; 1140694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 1141694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 1142694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 1143694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() != 0 && other.value() == 0; 1144694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 1145694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == other; 1146694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 1147694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 1148694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 1149694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value() != 0 && other.value() != 0; 1150694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 1151694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() * other.value()); 1152694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 1153694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private FDBigInteger mult(FDBigInteger other) { 1154694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (this.nWords == 0) { 1155694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return this; 1156694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1157694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (this.size() == 1) { 1158694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return other.mult(data[0]); 1159694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1160694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (other.nWords == 0) { 1161694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return other; 1162694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1163694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (other.size() == 1) { 1164694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return this.mult(other.data[0]); 1165694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1166694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] r = new int[nWords + other.nWords]; 1167694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak mult(this.data, this.nWords, other.data, other.nWords, r); 1168694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(r, this.offset + other.offset); 1169694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1170694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1171694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1172694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Adds another <code>FDBigInteger</code> to this <code>FDBigInteger</code>. 1173694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1174694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param other The <code>FDBigInteger</code> to add. 1175694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return The sum of the <code>FDBigInteger</code>s. 1176694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1177694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 1178694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 1179694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result.value() == \old(this.value() + other.value()); 1180694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 1181694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private FDBigInteger add(FDBigInteger other) { 1182694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak FDBigInteger big, small; 1183694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int bigLen, smallLen; 1184694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int tSize = this.size(); 1185694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int oSize = other.size(); 1186694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (tSize >= oSize) { 1187694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak big = this; 1188694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak bigLen = tSize; 1189694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak small = other; 1190694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak smallLen = oSize; 1191694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 1192694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak big = other; 1193694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak bigLen = oSize; 1194694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak small = this; 1195694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak smallLen = tSize; 1196694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1197694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] r = new int[bigLen + 1]; 1198694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int i = 0; 1199694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long carry = 0L; 1200694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (; i < smallLen; i++) { 1201694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak carry += (i < big.offset ? 0L : (big.data[i - big.offset] & LONG_MASK) ) 1202694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak + ((i < small.offset ? 0L : (small.data[i - small.offset] & LONG_MASK))); 1203694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak r[i] = (int) carry; 1204694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak carry >>= 32; // signed shift. 1205694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1206694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (; i < bigLen; i++) { 1207694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak carry += (i < big.offset ? 0L : (big.data[i - big.offset] & LONG_MASK) ); 1208694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak r[i] = (int) carry; 1209694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak carry >>= 32; // signed shift. 1210694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1211694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak r[bigLen] = (int) carry; 1212694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new FDBigInteger(r, 0); 1213694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1214694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1215694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1216694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1217694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Multiplies a <code>FDBigInteger</code> by an int and adds another int. The 1218694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * result is computed in place. This method is intended only to be invoked 1219694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * from 1220694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code> 1221694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * FDBigInteger(long lValue, char[] digits, int kDigits, int nDigits) 1222694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * </code>. 1223694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1224694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param iv The factor by which to multiply this <code>FDBigInteger</code>. 1225694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param addend The value to add to the product of this 1226694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code>FDBigInteger</code> and <code>iv</code>. 1227694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1228694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 1229694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.value()*UNSIGNED(iv) + UNSIGNED(addend) < ((\bigint)1) << ((this.data.length + this.offset)*32); 1230694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable this.data[*]; 1231694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures this.value() == \old(this.value()*UNSIGNED(iv) + UNSIGNED(addend)); 1232694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 1233694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private /*@ helper @*/ void multAddMe(int iv, int addend) { 1234694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long v = iv & LONG_MASK; 1235694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // unroll 0th iteration, doing addition. 1236694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long p = v * (data[0] & LONG_MASK) + (addend & LONG_MASK); 1237694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak data[0] = (int) p; 1238694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak p >>>= 32; 1239694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (int i = 1; i < nWords; i++) { 1240694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak p += v * (data[i] & LONG_MASK); 1241694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak data[i] = (int) p; 1242694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak p >>>= 32; 1243694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1244694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (p != 0L) { 1245694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak data[nWords++] = (int) p; // will fail noisily if illegal! 1246694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1247694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1248694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1249694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // 1250694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // original doc: 1251694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // 1252694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // do this -=q*S 1253694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // returns borrow 1254694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // 1255694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1256694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Multiplies the parameters and subtracts them from this 1257694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * <code>FDBigInteger</code>. 1258694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1259694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param q The integer parameter. 1260694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param S The <code>FDBigInteger</code> parameter. 1261694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return <code>this - q*S</code>. 1262694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1263694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 1264694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures nWords == 0 ==> offset == 0; 1265694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures nWords > 0 ==> data[nWords - 1] != 0; 1266694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 1267694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 1268694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires 0 < q && q <= (1L << 31); 1269694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires data != null; 1270694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires 0 <= nWords && nWords <= data.length && offset >= 0; 1271694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires !this.isImmutable; 1272694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this.size() == S.size(); 1273694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires this != S; 1274694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable this.nWords, this.offset, this.data, this.data[*]; 1275694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures -q <= \result && \result <= 0; 1276694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures this.size() == \old(this.size()); 1277694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures this.value() + (\result << (this.size()*32)) == \old(this.value() - q*S.value()); 1278694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures this.offset == \old(Math.min(this.offset, S.offset)); 1279694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \old(this.offset <= S.offset) ==> this.nWords == \old(this.nWords); 1280694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \old(this.offset <= S.offset) ==> this.offset == \old(this.offset); 1281694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \old(this.offset <= S.offset) ==> this.data == \old(this.data); 1282694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 1283694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ also 1284694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ 1285694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires q == 0; 1286694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable \nothing; 1287694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures \result == 0; 1288694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 1289694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private /*@ helper @*/ long multDiffMe(long q, FDBigInteger S) { 1290694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long diff = 0L; 1291694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (q != 0) { 1292694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int deltaSize = S.offset - this.offset; 1293694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (deltaSize >= 0) { 1294694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] sd = S.data; 1295694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] td = this.data; 1296694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (int sIndex = 0, tIndex = deltaSize; sIndex < S.nWords; sIndex++, tIndex++) { 1297694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak diff += (td[tIndex] & LONG_MASK) - q * (sd[sIndex] & LONG_MASK); 1298694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak td[tIndex] = (int) diff; 1299694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak diff >>= 32; // N.B. SIGNED shift. 1300694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1301694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 1302694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak deltaSize = -deltaSize; 1303694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] rd = new int[nWords + deltaSize]; 1304694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int sIndex = 0; 1305694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int rIndex = 0; 1306694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] sd = S.data; 1307694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (; rIndex < deltaSize && sIndex < S.nWords; sIndex++, rIndex++) { 1308694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak diff -= q * (sd[sIndex] & LONG_MASK); 1309694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak rd[rIndex] = (int) diff; 1310694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak diff >>= 32; // N.B. SIGNED shift. 1311694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1312694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int tIndex = 0; 1313694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int[] td = this.data; 1314694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (; sIndex < S.nWords; sIndex++, tIndex++, rIndex++) { 1315694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak diff += (td[tIndex] & LONG_MASK) - q * (sd[sIndex] & LONG_MASK); 1316694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak rd[rIndex] = (int) diff; 1317694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak diff >>= 32; // N.B. SIGNED shift. 1318694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1319694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak this.nWords += deltaSize; 1320694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak this.offset -= deltaSize; 1321694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak this.data = rd; 1322694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1323694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1324694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return diff; 1325694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1326694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1327694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1328694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1329694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Multiplies by 10 a big integer represented as an array. The final carry 1330694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * is returned. 1331694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1332694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param src The array representation of the big integer. 1333694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param srcLen The number of elements of <code>src</code> to use. 1334694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param dst The product array. 1335694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return The final carry of the multiplication. 1336694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1337694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 1338694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires src.length >= srcLen && dst.length >= srcLen; 1339694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable dst[0 .. srcLen - 1]; 1340694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures 0 <= \result && \result < 10; 1341694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures AP(dst, srcLen) + (\result << (srcLen*32)) == \old(AP(src, srcLen) * 10); 1342694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 1343694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private static int multAndCarryBy10(int[] src, int srcLen, int[] dst) { 1344694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long carry = 0; 1345694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (int i = 0; i < srcLen; i++) { 1346694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long product = (src[i] & LONG_MASK) * 10L + carry; 1347694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak dst[i] = (int) product; 1348694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak carry = product >>> 32; 1349694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1350694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return (int) carry; 1351694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1352694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1353694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1354694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Multiplies by a constant value a big integer represented as an array. 1355694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * The constant factor is an <code>int</code>. 1356694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1357694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param src The array representation of the big integer. 1358694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param srcLen The number of elements of <code>src</code> to use. 1359694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param value The constant factor by which to multiply. 1360694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param dst The product array. 1361694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1362694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 1363694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires src.length >= srcLen && dst.length >= srcLen + 1; 1364694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable dst[0 .. srcLen]; 1365694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures AP(dst, srcLen + 1) == \old(AP(src, srcLen) * UNSIGNED(value)); 1366694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 1367694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private static void mult(int[] src, int srcLen, int value, int[] dst) { 1368694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long val = value & LONG_MASK; 1369694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long carry = 0; 1370694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (int i = 0; i < srcLen; i++) { 1371694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long product = (src[i] & LONG_MASK) * val + carry; 1372694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak dst[i] = (int) product; 1373694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak carry = product >>> 32; 1374694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1375694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak dst[srcLen] = (int) carry; 1376694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1377694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1378694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1379694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Multiplies by a constant value a big integer represented as an array. 1380694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * The constant factor is a long represent as two <code>int</code>s. 1381694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1382694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param src The array representation of the big integer. 1383694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param srcLen The number of elements of <code>src</code> to use. 1384694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param v0 The lower 32 bits of the long factor. 1385694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param v1 The upper 32 bits of the long factor. 1386694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param dst The product array. 1387694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1388694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /*@ 1389694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires src != dst; 1390694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ requires src.length >= srcLen && dst.length >= srcLen + 2; 1391694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ assignable dst[0 .. srcLen + 1]; 1392694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @ ensures AP(dst, srcLen + 2) == \old(AP(src, srcLen) * (UNSIGNED(v0) + (UNSIGNED(v1) << 32))); 1393694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @*/ 1394694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private static void mult(int[] src, int srcLen, int v0, int v1, int[] dst) { 1395694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long v = v0 & LONG_MASK; 1396694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long carry = 0; 1397694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (int j = 0; j < srcLen; j++) { 1398694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long product = v * (src[j] & LONG_MASK) + carry; 1399694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak dst[j] = (int) product; 1400694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak carry = product >>> 32; 1401694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1402694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak dst[srcLen] = (int) carry; 1403694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak v = v1 & LONG_MASK; 1404694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak carry = 0; 1405694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (int j = 0; j < srcLen; j++) { 1406694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak long product = (dst[j + 1] & LONG_MASK) + v * (src[j] & LONG_MASK) + carry; 1407694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak dst[j + 1] = (int) product; 1408694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak carry = product >>> 32; 1409694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1410694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak dst[srcLen + 1] = (int) carry; 1411694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1412694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1413694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // Fails assertion for negative exponent. 1414694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1415694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Computes <code>5</code> raised to a given power. 1416694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1417694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param p The exponent of 5. 1418694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return <code>5<sup>p</sup></code>. 1419694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1420694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private static FDBigInteger big5pow(int p) { 1421694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak assert p >= 0 : p; // negative power of 5 1422694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (p < MAX_FIVE_POW) { 1423694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return POW_5_CACHE[p]; 1424694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1425694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return big5powRec(p); 1426694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1427694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1428694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // slow path 1429694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1430694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Computes <code>5</code> raised to a given power. 1431694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1432694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @param p The exponent of 5. 1433694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return <code>5<sup>p</sup></code>. 1434694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1435694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak private static FDBigInteger big5powRec(int p) { 1436694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (p < MAX_FIVE_POW) { 1437694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return POW_5_CACHE[p]; 1438694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1439694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // construct the value. 1440694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // recursively. 1441694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int q, r; 1442694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // in order to compute 5^p, 1443694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // compute its square root, 5^(p/2) and square. 1444694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // or, let q = p / 2, r = p -q, then 1445694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // 5^p = 5^(q+r) = 5^q * 5^r 1446694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak q = p >> 1; 1447694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak r = p - q; 1448694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak FDBigInteger bigq = big5powRec(q); 1449694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if (r < SMALL_5_POW.length) { 1450694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return bigq.mult(SMALL_5_POW[r]); 1451694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } else { 1452694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return bigq.mult(big5powRec(r)); 1453694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1454694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1455694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1456694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // for debugging ... 1457694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1458694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Converts this <code>FDBigInteger</code> to a hexadecimal string. 1459694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1460694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return The hexadecimal string representation. 1461694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1462694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public String toHexString(){ 1463694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak if(nWords ==0) { 1464694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return "0"; 1465694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1466694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak StringBuilder sb = new StringBuilder((nWords +offset)*8); 1467694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for(int i= nWords -1; i>=0; i--) { 1468694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak String subStr = Integer.toHexString(data[i]); 1469694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for(int j = subStr.length(); j<8; j++) { 1470694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak sb.append('0'); 1471694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1472694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak sb.append(subStr); 1473694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1474694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for(int i=offset; i>0; i--) { 1475694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak sb.append("00000000"); 1476694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1477694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return sb.toString(); 1478694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1479694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1480694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // for debugging ... 1481694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1482694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Converts this <code>FDBigInteger</code> to a <code>BigInteger</code>. 1483694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1484694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return The <code>BigInteger</code> representation. 1485694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1486694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public BigInteger toBigInteger() { 1487694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak byte[] magnitude = new byte[nWords * 4 + 1]; 1488694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak for (int i = 0; i < nWords; i++) { 1489694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak int w = data[i]; 1490694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak magnitude[magnitude.length - 4 * i - 1] = (byte) w; 1491694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak magnitude[magnitude.length - 4 * i - 2] = (byte) (w >> 8); 1492694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak magnitude[magnitude.length - 4 * i - 3] = (byte) (w >> 16); 1493694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak magnitude[magnitude.length - 4 * i - 4] = (byte) (w >> 24); 1494694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1495694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return new BigInteger(magnitude).shiftLeft(offset * 32); 1496694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1497694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak 1498694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak // for debugging ... 1499694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak /** 1500694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * Converts this <code>FDBigInteger</code> to a string. 1501694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * 1502694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak * @return The string representation. 1503694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak */ 1504694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak @Override 1505694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak public String toString(){ 1506694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak return toBigInteger().toString(); 1507694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak } 1508694e617f54a7bfbdad24913ce96f5d56f1a1960aPrzemyslaw Szczepaniak} 1509