diff options
Diffstat (limited to 'src/mul_1_extracted.c')
-rw-r--r-- | src/mul_1_extracted.c | 314 |
1 files changed, 314 insertions, 0 deletions
diff --git a/src/mul_1_extracted.c b/src/mul_1_extracted.c new file mode 100644 index 000000000..8ac09c09d --- /dev/null +++ b/src/mul_1_extracted.c @@ -0,0 +1,314 @@ +/* mpfr_mul_1 -- internal function to perform a one-limb multiplication + This code was extracted by Kremlin from a formal proof in F* + done by Jianyang Pan in April-August 2018: do not modify it! + +Copyright 2004-2018 Free Software Foundation, Inc. +Contributed by the AriC and Caramba projects, INRIA. + +This file is part of the GNU MPFR Library. + +The GNU MPFR Library is free software; you can redistribute it and/or modify +it under the terms of the GNU Lesser General Public License as published by +the Free Software Foundation; either version 3 of the License, or (at your +option) any later version. + +The GNU MPFR Library is distributed in the hope that it will be useful, but +WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY +or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public +License for more details. + +You should have received a copy of the GNU Lesser General Public License +along with the GNU MPFR Library; see the file COPYING.LESSER. If not, see +http://www.gnu.org/licenses/ or write to the Free Software Foundation, Inc., +51 Franklin St, Fifth Floor, Boston, MA 02110-1301, USA. */ + +#define uint32_t mpfr_prec_t +#define int32_t mpfr_exp_t +#define uint64_t mp_limb_t +#define bool int + +typedef struct K___int32_t_uint64_t_uint64_t_s +{ + int32_t fst; + uint64_t snd; + uint64_t thd; +} +K___int32_t_uint64_t_uint64_t; + +#define MPFR_Lib_mpfr_struct __mpfr_struct +#define MPFR_Lib_mpfr_RET(I) (I) != 0 ? ((__gmpfr_flags |= MPFR_FLAGS_INEXACT), (I)) : 0 +#define MPFR_Exceptions_mpfr_overflow mpfr_overflow +#define MPFR_Exceptions_mpfr_underflow mpfr_underflow +#define mpfr_prec _mpfr_prec +#define mpfr_exp _mpfr_exp +#define mpfr_d _mpfr_d +#define mpfr_sign _mpfr_sign +#define MPFR_Lib_gmp_NUMB_BITS GMP_NUMB_BITS +#define MPFR_Lib_mpfr_EMAX __gmpfr_emax +#define MPFR_Lib_mpfr_EMIN __gmpfr_emin +#define MPFR_RoundingMode_MPFR_RNDZ MPFR_RNDZ + +#define MPFR_RoundingMode_uu___is_MPFR_RNDN(rnd_mode) (rnd_mode == MPFR_RNDN) +#define MPFR_RoundingMode_mpfr_IS_LIKE_RNDZ MPFR_IS_LIKE_RNDZ +#define MPFR_RoundingMode_mpfr_IS_LIKE_RNDA MPFR_IS_LIKE_RNDA + +/* Special code for prec(a) < GMP_NUMB_BITS and + prec(b), prec(c) <= GMP_NUMB_BITS. + Note: this code was copied in sqr.c, function mpfr_sqr_1 (this saves a few cycles + with respect to have this function exported). As a consequence, any change here + should be reported in mpfr_sqr_1. */ +static int +mpfr_mul_1 (mpfr_ptr a, mpfr_srcptr b, mpfr_srcptr c, mpfr_rnd_t rnd_mode, + mpfr_prec_t p) +{ + uint64_t *ap = a->mpfr_d; + uint64_t *bp = b->mpfr_d; + uint64_t *cp = c->mpfr_d; + uint64_t b0 = bp[0U]; + uint64_t c0 = cp[0U]; + uint32_t sh = MPFR_Lib_gmp_NUMB_BITS - p; + uint64_t mask = ((uint64_t)1U << sh) - (uint64_t)1U; + int32_t ax = b->mpfr_exp + c->mpfr_exp; + //K___uint64_t_uint64_t scrut0 = MPFR_Umul_ppmm_umul_ppmm(b0, c0); + //uint64_t a0 = scrut0.fst; + //uint64_t sb = scrut0.snd; + uint64_t a0, sb; + umul_ppmm (a0, sb, b0, c0); + K___int32_t_uint64_t_uint64_t scrut; + if (a0 < (uint64_t)0x8000000000000000U) + scrut = + ( + (K___int32_t_uint64_t_uint64_t){ + .fst = ax - (int32_t)1, + .snd = a0 << (uint32_t)1U | sb >> (MPFR_Lib_gmp_NUMB_BITS - (uint32_t)1U), + .thd = sb << (uint32_t)1U + } + ); + else + scrut = ((K___int32_t_uint64_t_uint64_t){ .fst = ax, .snd = a0, .thd = sb }); + int32_t ax1 = scrut.fst; + uint64_t a01 = scrut.snd; + uint64_t sb1 = scrut.thd; + uint64_t rb = a01 & (uint64_t)1U << (sh - (uint32_t)1U); + uint64_t sb2 = sb1 | ((a01 & mask) ^ rb); + ap[0U] = a01 & ~mask; + MPFR_Lib_mpfr_struct uu___63_2736 = a[0U]; + a[0U] = + ( + (MPFR_Lib_mpfr_struct){ + .mpfr_prec = uu___63_2736.mpfr_prec, + .mpfr_sign = b->mpfr_sign * c->mpfr_sign, + .mpfr_exp = uu___63_2736.mpfr_exp, + .mpfr_d = uu___63_2736.mpfr_d + } + ); + uint64_t *ap1 = a->mpfr_d; + uint64_t a02 = ap1[0U]; + if (ax1 > MPFR_Lib_mpfr_EMAX) + return MPFR_Exceptions_mpfr_overflow(a, rnd_mode, a->mpfr_sign); + else if (ax1 < MPFR_Lib_mpfr_EMIN) + { + bool aneg = a->mpfr_sign < (int32_t)0; + if + ( + ax1 + == MPFR_Lib_mpfr_EMIN - (int32_t)1 + && a02 == ~mask + && + ((MPFR_RoundingMode_uu___is_MPFR_RNDN(rnd_mode) && rb > (uint64_t)0U) + || ((rb | sb2) > (uint64_t)0U && MPFR_RoundingMode_mpfr_IS_LIKE_RNDA(rnd_mode, aneg))) + ) + { + uint64_t *ap2 = a->mpfr_d; + uint64_t a03 = ap2[0U]; + MPFR_Lib_mpfr_struct uu___62_2887 = a[0U]; + a[0U] = + ( + (MPFR_Lib_mpfr_struct){ + .mpfr_prec = uu___62_2887.mpfr_prec, + .mpfr_sign = uu___62_2887.mpfr_sign, + .mpfr_exp = ax1, + .mpfr_d = uu___62_2887.mpfr_d + } + ); + if (rb == (uint64_t)0U && sb2 == (uint64_t)0U) + return MPFR_Lib_mpfr_RET((int32_t)0); + else if (MPFR_RoundingMode_uu___is_MPFR_RNDN(rnd_mode)) + if + (rb == (uint64_t)0U || (sb2 == (uint64_t)0U && (a03 & (uint64_t)1U << sh) == (uint64_t)0U)) + { + int32_t ite; + if (a->mpfr_sign == (int32_t)1) + ite = (int32_t)-1; + else + ite = (int32_t)1; + return MPFR_Lib_mpfr_RET(ite); + } + else + { + uint64_t *ap3 = a->mpfr_d; + ap3[0U] = ap3[0U] + ((uint64_t)1U << sh); + if (ap3[0U] == (uint64_t)0U) + { + ap3[0U] = (uint64_t)0x8000000000000000U; + if (ax1 + (int32_t)1 > MPFR_Lib_mpfr_EMAX) + return MPFR_Exceptions_mpfr_overflow(a, rnd_mode, a->mpfr_sign); + else + { + MPFR_Lib_mpfr_struct uu___62_3027 = a[0U]; + a[0U] = + ( + (MPFR_Lib_mpfr_struct){ + .mpfr_prec = uu___62_3027.mpfr_prec, + .mpfr_sign = uu___62_3027.mpfr_sign, + .mpfr_exp = ax1 + (int32_t)1, + .mpfr_d = uu___62_3027.mpfr_d + } + ); + return MPFR_Lib_mpfr_RET(a->mpfr_sign); + } + } + else + return MPFR_Lib_mpfr_RET(a->mpfr_sign); + } + else if (MPFR_RoundingMode_mpfr_IS_LIKE_RNDZ(rnd_mode, a->mpfr_sign < (int32_t)0)) + { + int32_t ite; + if (a->mpfr_sign == (int32_t)1) + ite = (int32_t)-1; + else + ite = (int32_t)1; + return MPFR_Lib_mpfr_RET(ite); + } + else + { + uint64_t *ap3 = a->mpfr_d; + ap3[0U] = ap3[0U] + ((uint64_t)1U << sh); + if (ap3[0U] == (uint64_t)0U) + { + ap3[0U] = (uint64_t)0x8000000000000000U; + if (ax1 + (int32_t)1 > MPFR_Lib_mpfr_EMAX) + return MPFR_Exceptions_mpfr_overflow(a, rnd_mode, a->mpfr_sign); + else + { + MPFR_Lib_mpfr_struct uu___62_3217 = a[0U]; + a[0U] = + ( + (MPFR_Lib_mpfr_struct){ + .mpfr_prec = uu___62_3217.mpfr_prec, + .mpfr_sign = uu___62_3217.mpfr_sign, + .mpfr_exp = ax1 + (int32_t)1, + .mpfr_d = uu___62_3217.mpfr_d + } + ); + return MPFR_Lib_mpfr_RET(a->mpfr_sign); + } + } + else + return MPFR_Lib_mpfr_RET(a->mpfr_sign); + } + } + else if + ( + MPFR_RoundingMode_uu___is_MPFR_RNDN(rnd_mode) + && + (ax1 + < MPFR_Lib_mpfr_EMIN - (int32_t)1 + || (a02 == (uint64_t)0x8000000000000000U && (rb | sb2) == (uint64_t)0U)) + ) + return MPFR_Exceptions_mpfr_underflow(a, MPFR_RoundingMode_MPFR_RNDZ, a->mpfr_sign); + else + return MPFR_Exceptions_mpfr_underflow(a, rnd_mode, a->mpfr_sign); + } + else + { + uint64_t *ap2 = a->mpfr_d; + uint64_t a03 = ap2[0U]; + MPFR_Lib_mpfr_struct uu___62_3402 = a[0U]; + a[0U] = + ( + (MPFR_Lib_mpfr_struct){ + .mpfr_prec = uu___62_3402.mpfr_prec, + .mpfr_sign = uu___62_3402.mpfr_sign, + .mpfr_exp = ax1, + .mpfr_d = uu___62_3402.mpfr_d + } + ); + if (rb == (uint64_t)0U && sb2 == (uint64_t)0U) + return MPFR_Lib_mpfr_RET((int32_t)0); + else if (MPFR_RoundingMode_uu___is_MPFR_RNDN(rnd_mode)) + if (rb == (uint64_t)0U || (sb2 == (uint64_t)0U && (a03 & (uint64_t)1U << sh) == (uint64_t)0U)) + { + int32_t ite; + if (a->mpfr_sign == (int32_t)1) + ite = (int32_t)-1; + else + ite = (int32_t)1; + return MPFR_Lib_mpfr_RET(ite); + } + else + { + uint64_t *ap3 = a->mpfr_d; + ap3[0U] = ap3[0U] + ((uint64_t)1U << sh); + if (ap3[0U] == (uint64_t)0U) + { + ap3[0U] = (uint64_t)0x8000000000000000U; + if (ax1 + (int32_t)1 > MPFR_Lib_mpfr_EMAX) + return MPFR_Exceptions_mpfr_overflow(a, rnd_mode, a->mpfr_sign); + else + { + MPFR_Lib_mpfr_struct uu___62_3542 = a[0U]; + a[0U] = + ( + (MPFR_Lib_mpfr_struct){ + .mpfr_prec = uu___62_3542.mpfr_prec, + .mpfr_sign = uu___62_3542.mpfr_sign, + .mpfr_exp = ax1 + (int32_t)1, + .mpfr_d = uu___62_3542.mpfr_d + } + ); + return MPFR_Lib_mpfr_RET(a->mpfr_sign); + } + } + else + return MPFR_Lib_mpfr_RET(a->mpfr_sign); + } + else if (MPFR_RoundingMode_mpfr_IS_LIKE_RNDZ(rnd_mode, a->mpfr_sign < (int32_t)0)) + { + int32_t ite; + if (a->mpfr_sign == (int32_t)1) + ite = (int32_t)-1; + else + ite = (int32_t)1; + return MPFR_Lib_mpfr_RET(ite); + } + else + { + uint64_t *ap3 = a->mpfr_d; + ap3[0U] = ap3[0U] + ((uint64_t)1U << sh); + if (ap3[0U] == (uint64_t)0U) + { + ap3[0U] = (uint64_t)0x8000000000000000U; + if (ax1 + (int32_t)1 > MPFR_Lib_mpfr_EMAX) + return MPFR_Exceptions_mpfr_overflow(a, rnd_mode, a->mpfr_sign); + else + { + MPFR_Lib_mpfr_struct uu___62_3732 = a[0U]; + a[0U] = + ( + (MPFR_Lib_mpfr_struct){ + .mpfr_prec = uu___62_3732.mpfr_prec, + .mpfr_sign = uu___62_3732.mpfr_sign, + .mpfr_exp = ax1 + (int32_t)1, + .mpfr_d = uu___62_3732.mpfr_d + } + ); + return MPFR_Lib_mpfr_RET(a->mpfr_sign); + } + } + else + return MPFR_Lib_mpfr_RET(a->mpfr_sign); + } + } +} + |