summaryrefslogtreecommitdiff
path: root/Build/source/libs/mpfr/mpfr-src/src/sub1sp1_extracted.c
diff options
context:
space:
mode:
Diffstat (limited to 'Build/source/libs/mpfr/mpfr-src/src/sub1sp1_extracted.c')
-rw-r--r--Build/source/libs/mpfr/mpfr-src/src/sub1sp1_extracted.c530
1 files changed, 530 insertions, 0 deletions
diff --git a/Build/source/libs/mpfr/mpfr-src/src/sub1sp1_extracted.c b/Build/source/libs/mpfr/mpfr-src/src/sub1sp1_extracted.c
new file mode 100644
index 00000000000..8e62b3f4dcf
--- /dev/null
+++ b/Build/source/libs/mpfr/mpfr-src/src/sub1sp1_extracted.c
@@ -0,0 +1,530 @@
+/* mpfr_sub1sp1 -- internal function to perform a "real" subtraction on one limb
+ This code was extracted by Kremlin from a formal proof in F*
+ done by FĂ©lix Breton in June-July 2019: do not modify it!
+
+Source: https://github.com/project-everest/hacl-star/tree/dev_mpfr/code/mpfr
+
+Copyright 2004-2020 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
+https://www.gnu.org/licenses/ or write to the Free Software Foundation, Inc.,
+51 Franklin St, Fifth Floor, Boston, MA 02110-1301, USA. */
+
+#include "stdint.h"
+#include "inttypes.h" /* for __builtin_clzll */
+
+/* beginning of manually added declarations */
+
+#define MPFR_mpfr_sub1sp1 mpfr_sub1sp1
+#define MPFR_RoundingMode_mpfr_rnd_t mpfr_rnd_t
+#define MPFR_Lib_mpfr_struct __mpfr_struct
+#define MPFR_Lib_gmp_NUMB_BITS GMP_NUMB_BITS
+#define __eq__MPFR_RoundingMode_mpfr_rnd_t(x,y) ((x)==(y))
+#define MPFR_RoundingMode_MPFR_RNDD MPFR_RNDD
+#define MPFR_RoundingMode_MPFR_RNDN MPFR_RNDN
+#define MPFR_RoundingMode_MPFR_RNDZ MPFR_RNDZ
+#define MPFR_RoundingMode_MPFR_RNDU MPFR_RNDU
+#define MPFR_Lib_mpfr_SET_EXP MPFR_SET_EXP
+#define MPFR_Lib_mpfr_RET MPFR_RET
+#define MPFR_Lib_mpfr_NEG_SIGN(x) (-(x))
+#define MPFR_Exceptions_mpfr_underflow mpfr_underflow
+#define MPFR_Exceptions_mpfr_overflow mpfr_overflow
+#define true 1
+#define false 0
+
+/* the original code had mpfr_exp instead of _mpfr_exp */
+#define mpfr_exp _mpfr_exp
+/* the original code had mpfr_d instead of _mpfr_d */
+#define mpfr_d _mpfr_d
+/* the original code had mpfr_prec instead of _mpfr_prec */
+#define mpfr_prec _mpfr_prec
+/* the original code had mpfr_sign instead of _mpfr_sign */
+#define mpfr_sign _mpfr_sign
+#define bool int /* to avoid conflict with C++ keyword */
+
+/* end of manually added declarations */
+
+static uint32_t MPFR_Lib_Clz_count_leading_zeros (uint64_t a) {
+ return __builtin_clzll(a);
+}
+
+typedef struct MPFR_Add1sp1_state_s
+{
+ int64_t sh;
+ int64_t bx;
+ uint64_t rb;
+ uint64_t sb;
+}
+MPFR_Add1sp1_state;
+
+typedef struct
+K___MPFR_Lib_mpfr_struct__MPFR_Lib_mpfr_struct__int64_t_int64_t_uint64_t__uint64_t__s
+{
+ const MPFR_Lib_mpfr_struct *fst; /* added const */
+ const MPFR_Lib_mpfr_struct *snd; /* added const */
+ int64_t thd;
+ int64_t f3;
+ uint64_t *f4;
+ uint64_t *f5;
+}
+K___MPFR_Lib_mpfr_struct__MPFR_Lib_mpfr_struct__int64_t_int64_t_uint64_t__uint64_t_;
+
+static MPFR_Add1sp1_state
+MPFR_Add1sp1_mk_state(int64_t sh, int64_t bx, uint64_t rb, uint64_t sb)
+{
+ MPFR_Add1sp1_state lit;
+ lit.sh = sh;
+ lit.bx = bx;
+ lit.rb = rb;
+ lit.sb = sb;
+ return lit;
+}
+
+static MPFR_Add1sp1_state
+MPFR_Sub1sp1_mpfr_sub1sp1_gt_branch_1(
+ MPFR_Lib_mpfr_struct *a,
+ const MPFR_Lib_mpfr_struct *b, /* added const */
+ const MPFR_Lib_mpfr_struct *c, /* added const */
+ uint64_t *ap,
+ uint64_t *bp,
+ uint64_t *cp,
+ int64_t bx,
+ int64_t cx,
+ int64_t p,
+ int64_t sh,
+ uint64_t mask,
+ uint64_t sb_1,
+ uint64_t a0_base
+)
+{
+ uint32_t cnt = MPFR_Lib_Clz_count_leading_zeros(a0_base);
+ uint64_t a0;
+ if (cnt == (uint32_t)0U)
+ {
+ a0 = a0_base;
+ }
+ else
+ {
+ a0 = a0_base << cnt | sb_1 >> ((uint32_t)64U - cnt);
+ }
+ {
+ uint64_t sb_2 = sb_1 << cnt;
+ uint64_t rb = a0 & (uint64_t)1U << (uint32_t)(sh - (int64_t)1);
+ uint64_t sb = sb_2 | ((a0 & mask) ^ rb);
+ ap[0U] = a0 & ~mask;
+ return MPFR_Add1sp1_mk_state(sh, bx - (int64_t)cnt, rb, sb);
+ }
+}
+
+static bool MPFR_RoundingMode_uu___is_MPFR_RNDN(MPFR_RoundingMode_mpfr_rnd_t projectee)
+{
+ switch (projectee)
+ {
+ case MPFR_RoundingMode_MPFR_RNDN:
+ {
+ return true;
+ }
+ default:
+ {
+ return false;
+ }
+ }
+}
+
+static bool MPFR_RoundingMode_uu___is_MPFR_RNDZ(MPFR_RoundingMode_mpfr_rnd_t projectee)
+{
+ switch (projectee)
+ {
+ case MPFR_RoundingMode_MPFR_RNDZ:
+ {
+ return true;
+ }
+ default:
+ {
+ return false;
+ }
+ }
+}
+
+static bool MPFR_RoundingMode_uu___is_MPFR_RNDU(MPFR_RoundingMode_mpfr_rnd_t projectee)
+{
+ switch (projectee)
+ {
+ case MPFR_RoundingMode_MPFR_RNDU:
+ {
+ return true;
+ }
+ default:
+ {
+ return false;
+ }
+ }
+}
+
+static bool MPFR_RoundingMode_uu___is_MPFR_RNDD(MPFR_RoundingMode_mpfr_rnd_t projectee)
+{
+ switch (projectee)
+ {
+ case MPFR_RoundingMode_MPFR_RNDD:
+ {
+ return true;
+ }
+ default:
+ {
+ return false;
+ }
+ }
+}
+
+static int32_t
+MPFR_Sub1sp1_mpfr_sub1sp1(
+ MPFR_Lib_mpfr_struct *a,
+ const MPFR_Lib_mpfr_struct *b, /* added const */
+ const MPFR_Lib_mpfr_struct *c, /* added const */
+ MPFR_RoundingMode_mpfr_rnd_t rnd_mode,
+ int64_t p
+)
+{
+ int64_t bx = b->mpfr_exp;
+ int64_t cx = c->mpfr_exp;
+ uint64_t *ap = a->mpfr_d;
+ uint64_t *bp = b->mpfr_d;
+ uint64_t *cp = c->mpfr_d;
+ int64_t sh = MPFR_Lib_gmp_NUMB_BITS - p;
+ uint64_t bp0ul = bp[0U];
+ uint64_t cp0ul = cp[0U];
+ if (bx == cx && bp0ul == cp0ul)
+ {
+ if (__eq__MPFR_RoundingMode_mpfr_rnd_t(rnd_mode, MPFR_RoundingMode_MPFR_RNDD))
+ {
+ MPFR_Lib_mpfr_struct uu____0 = a[0U];
+ MPFR_Lib_mpfr_struct lit;
+ lit.mpfr_prec = uu____0.mpfr_prec;
+ lit.mpfr_sign = (int32_t)-1;
+ lit.mpfr_exp = uu____0.mpfr_exp;
+ lit.mpfr_d = uu____0.mpfr_d;
+ a[0U] = lit;
+ }
+ else
+ {
+ MPFR_Lib_mpfr_struct uu____1 = a[0U];
+ MPFR_Lib_mpfr_struct lit;
+ lit.mpfr_prec = uu____1.mpfr_prec;
+ lit.mpfr_sign = (int32_t)1;
+ lit.mpfr_exp = uu____1.mpfr_exp;
+ lit.mpfr_d = uu____1.mpfr_d;
+ a[0U] = lit;
+ }
+ MPFR_Lib_mpfr_SET_EXP(a, (int64_t)-0x7fffffffffffffff);
+ /* the following return was commented out from the extracted code */
+ /*return*/ MPFR_Lib_mpfr_RET((int32_t)0);
+ }
+ else
+ {
+ MPFR_Add1sp1_state st;
+ if (bx == cx)
+ {
+ /* Prims_int vb = FStar_UInt64_v(bp[0U]); */ /* unused */
+ /* Prims_int vc = FStar_UInt64_v(cp[0U]); */ /* unused */
+ /* Prims_int vsh = FStar_Int64_v(sh); */ /* unused */
+ if (cp[0U] > bp[0U])
+ {
+ uint64_t a0 = cp[0U] - bp[0U];
+ uint32_t cnt = MPFR_Lib_Clz_count_leading_zeros(a0);
+ int32_t uu____2 = MPFR_Lib_mpfr_NEG_SIGN(b->mpfr_sign);
+ MPFR_Lib_mpfr_struct uu____3 = a[0U];
+ MPFR_Lib_mpfr_struct lit;
+ lit.mpfr_prec = uu____3.mpfr_prec;
+ lit.mpfr_sign = uu____2;
+ lit.mpfr_exp = uu____3.mpfr_exp;
+ lit.mpfr_d = uu____3.mpfr_d;
+ a[0U] = lit;
+ ap[0U] = a0 << cnt;
+ {
+ int64_t bx1 = bx - (int64_t)cnt;
+ st = MPFR_Add1sp1_mk_state(sh, bx1, (uint64_t)0U, (uint64_t)0U);
+ }
+ }
+ else
+ {
+ uint64_t a0 = bp[0U] - cp[0U];
+ uint32_t cnt = MPFR_Lib_Clz_count_leading_zeros(a0);
+ MPFR_Lib_mpfr_struct uu____4 = a[0U];
+ MPFR_Lib_mpfr_struct lit;
+ lit.mpfr_prec = uu____4.mpfr_prec;
+ lit.mpfr_sign = b->mpfr_sign;
+ lit.mpfr_exp = uu____4.mpfr_exp;
+ lit.mpfr_d = uu____4.mpfr_d;
+ a[0U] = lit;
+ ap[0U] = a0 << cnt;
+ {
+ int64_t bx1 = bx - (int64_t)cnt;
+ st = MPFR_Add1sp1_mk_state(sh, bx1, (uint64_t)0U, (uint64_t)0U);
+ }
+ }
+ }
+ else
+ {
+ K___MPFR_Lib_mpfr_struct__MPFR_Lib_mpfr_struct__int64_t_int64_t_uint64_t__uint64_t_ scrut;
+ if (bx >= cx)
+ {
+ MPFR_Lib_mpfr_struct uu____5 = a[0U];
+ MPFR_Lib_mpfr_struct lit;
+ lit.mpfr_prec = uu____5.mpfr_prec;
+ lit.mpfr_sign = b->mpfr_sign;
+ lit.mpfr_exp = uu____5.mpfr_exp;
+ lit.mpfr_d = uu____5.mpfr_d;
+ a[0U] = lit;
+ {
+ K___MPFR_Lib_mpfr_struct__MPFR_Lib_mpfr_struct__int64_t_int64_t_uint64_t__uint64_t_ lit0;
+ lit0.fst = b;
+ lit0.snd = c;
+ lit0.thd = bx;
+ lit0.f3 = cx;
+ lit0.f4 = bp;
+ lit0.f5 = cp;
+ scrut = lit0;
+ }
+ }
+ else
+ {
+ int32_t uu____6 = MPFR_Lib_mpfr_NEG_SIGN(b->mpfr_sign);
+ MPFR_Lib_mpfr_struct uu____7 = a[0U];
+ MPFR_Lib_mpfr_struct lit;
+ lit.mpfr_prec = uu____7.mpfr_prec;
+ lit.mpfr_sign = uu____6;
+ lit.mpfr_exp = uu____7.mpfr_exp;
+ lit.mpfr_d = uu____7.mpfr_d;
+ a[0U] = lit;
+ {
+ K___MPFR_Lib_mpfr_struct__MPFR_Lib_mpfr_struct__int64_t_int64_t_uint64_t__uint64_t_ lit0;
+ lit0.fst = c;
+ lit0.snd = b;
+ lit0.thd = cx;
+ lit0.f3 = bx;
+ lit0.f4 = cp;
+ lit0.f5 = bp;
+ scrut = lit0;
+ }
+ }
+ {
+ const MPFR_Lib_mpfr_struct *b1 = scrut.fst; /* added const */
+ const MPFR_Lib_mpfr_struct *c1 = scrut.snd; /* added const */
+ int64_t bx1 = scrut.thd;
+ int64_t cx1 = scrut.f3;
+ uint64_t *bp1 = scrut.f4;
+ uint64_t *cp1 = scrut.f5;
+ int64_t d = bx1 - cx1;
+ uint64_t bp0ul1 = bp1[0U];
+ uint64_t cp0ul1 = cp1[0U];
+ uint64_t mask = ((uint64_t)1U << (uint32_t)sh) - (uint64_t)1U;
+ if (d < (int64_t)64)
+ {
+ uint64_t sb_1 = ~(cp0ul1 << (uint32_t)(MPFR_Lib_gmp_NUMB_BITS - d)) + (uint64_t)1U;
+ uint64_t ite;
+ if (sb_1 == (uint64_t)0U)
+ {
+ ite = (uint64_t)0U;
+ }
+ else
+ {
+ ite = (uint64_t)1U;
+ }
+ st =
+ MPFR_Sub1sp1_mpfr_sub1sp1_gt_branch_1(a,
+ b1,
+ c1,
+ ap,
+ bp1,
+ cp1,
+ bx1,
+ cx1,
+ p,
+ sh,
+ mask,
+ sb_1,
+ bp0ul1 - ite - (cp0ul1 >> (uint32_t)d));
+ }
+ else if (bp0ul1 > (uint64_t)0x8000000000000000U)
+ {
+ ap[0U] = bp0ul1 - ((uint64_t)1U << (uint32_t)sh);
+ st = MPFR_Add1sp1_mk_state(sh, bx1, (uint64_t)1U, (uint64_t)1U);
+ }
+ else
+ {
+ bool
+ rb =
+ sh
+ > (int64_t)1
+ || d > MPFR_Lib_gmp_NUMB_BITS
+ || cp0ul1 == (uint64_t)0x8000000000000000U;
+ bool
+ sb =
+ sh
+ > (int64_t)1
+ || d > MPFR_Lib_gmp_NUMB_BITS
+ || cp0ul1 != (uint64_t)0x8000000000000000U;
+ ap[0U] = ~mask;
+ {
+ uint64_t ite0;
+ if (rb)
+ {
+ ite0 = (uint64_t)1U;
+ }
+ else
+ {
+ ite0 = (uint64_t)0U;
+ }
+ {
+ uint64_t ite;
+ if (sb)
+ {
+ ite = (uint64_t)1U;
+ }
+ else
+ {
+ ite = (uint64_t)0U;
+ }
+ st = MPFR_Add1sp1_mk_state(sh, bx1 - (int64_t)1, ite0, ite);
+ }
+ }
+ }
+ }
+ }
+ /* the constant (int64_t)-0x000000003fffffff from the original extracted
+ code was manually replaced by __gmpfr_emin */
+ if (st.bx < __gmpfr_emin)
+ {
+ int32_t s = a->mpfr_sign;
+ uint64_t ap0ul = ap[0U];
+ if
+ (
+ __eq__MPFR_RoundingMode_mpfr_rnd_t(rnd_mode,
+ MPFR_RoundingMode_MPFR_RNDN)
+ /* the constant (int64_t)-1073741824 from the original extracted
+ code was manually replaced by __gmpfr_emin-1 */
+ && (st.bx < __gmpfr_emin - 1 || ap0ul == (uint64_t)0x8000000000000000U)
+ )
+ {
+ MPFR_Lib_mpfr_SET_EXP(a, (int64_t)-0x7fffffffffffffff);
+ return MPFR_Lib_mpfr_NEG_SIGN(s);
+ }
+ else
+ {
+ int32_t t = MPFR_Exceptions_mpfr_underflow(a, rnd_mode, s);
+ return t;
+ }
+ }
+ else
+ {
+ uint64_t a0 = ap[0U];
+ MPFR_Lib_mpfr_SET_EXP(a, st.bx);
+ if (st.rb == (uint64_t)0U && st.sb == (uint64_t)0U)
+ {
+ /* the following return was commented out from the extracted code */
+ /*return*/ MPFR_Lib_mpfr_RET((int32_t)0);
+ }
+ else if (MPFR_RoundingMode_uu___is_MPFR_RNDN(rnd_mode))
+ {
+ if
+ (
+ st.rb
+ == (uint64_t)0U
+ || (st.sb == (uint64_t)0U && (a0 & (uint64_t)1U << (uint32_t)st.sh) == (uint64_t)0U)
+ )
+ {
+ /* the following return was commented out from the extracted code */
+ /*return*/ MPFR_Lib_mpfr_RET(MPFR_Lib_mpfr_NEG_SIGN(a->mpfr_sign));
+ }
+ else if (ap[0U] + ((uint64_t)1U << (uint32_t)st.sh) == (uint64_t)0U)
+ {
+ ap[0U] = ap[0U] + ((uint64_t)1U << (uint32_t)st.sh);
+ ap[0U] = (uint64_t)0x8000000000000000U;
+ /* the constant (int64_t)0x000000003fffffff from the original
+ extracted code was replaced by __gmpfr_emax */
+ if (st.bx + (int64_t)1 <= __gmpfr_emax)
+ {
+ MPFR_Lib_mpfr_SET_EXP(a, st.bx + (int64_t)1);
+ /* the following return was commented out from the extracted code */
+ /*return*/ MPFR_Lib_mpfr_RET(a->mpfr_sign);
+ }
+ else
+ {
+ int32_t t = MPFR_Exceptions_mpfr_overflow(a, rnd_mode, a->mpfr_sign);
+ /* the following return was commented out from the extracted code */
+ /*return*/ MPFR_Lib_mpfr_RET(t);
+ }
+ }
+ else
+ {
+ ap[0U] = ap[0U] + ((uint64_t)1U << (uint32_t)st.sh);
+ /* the following return was commented out from the extracted code */
+ /*return*/ MPFR_Lib_mpfr_RET(a->mpfr_sign);
+ }
+ }
+ else
+ {
+ bool uu____8 = a->mpfr_sign < (int32_t)0;
+ if
+ (
+ MPFR_RoundingMode_uu___is_MPFR_RNDZ(rnd_mode)
+ || (MPFR_RoundingMode_uu___is_MPFR_RNDU(rnd_mode) && uu____8)
+ || (MPFR_RoundingMode_uu___is_MPFR_RNDD(rnd_mode) && !uu____8)
+ )
+ {
+ /* the following return was commented out from the extracted code */
+ /*return*/ MPFR_Lib_mpfr_RET(MPFR_Lib_mpfr_NEG_SIGN(a->mpfr_sign));
+ }
+ else if (ap[0U] + ((uint64_t)1U << (uint32_t)st.sh) == (uint64_t)0U)
+ {
+ ap[0U] = ap[0U] + ((uint64_t)1U << (uint32_t)st.sh);
+ ap[0U] = (uint64_t)0x8000000000000000U;
+ /* the constant (int64_t)0x000000003fffffff from the original
+ extracted code was replaced by __gmpfr_emax */
+ if (st.bx + (int64_t)1 <= __gmpfr_emax)
+ {
+ MPFR_Lib_mpfr_SET_EXP(a, st.bx + (int64_t)1);
+ /* the following return was commented out from the extracted code */
+ /*return*/ MPFR_Lib_mpfr_RET(a->mpfr_sign);
+ }
+ else
+ {
+ int32_t t = MPFR_Exceptions_mpfr_overflow(a, rnd_mode, a->mpfr_sign);
+ /* the following return was commented out from the extracted code */
+ /*return*/ MPFR_Lib_mpfr_RET(t);
+ }
+ }
+ else
+ {
+ ap[0U] = ap[0U] + ((uint64_t)1U << (uint32_t)st.sh);
+ /* the following return was commented out from the extracted code */
+ /*return*/ MPFR_Lib_mpfr_RET(a->mpfr_sign);
+ }
+ }
+ }
+ }
+}
+
+int32_t
+(*MPFR_mpfr_sub1sp1)(
+ MPFR_Lib_mpfr_struct *x0,
+ const MPFR_Lib_mpfr_struct *x1, /* added const */
+ const MPFR_Lib_mpfr_struct *x2, /* added const */
+ MPFR_RoundingMode_mpfr_rnd_t x3,
+ int64_t x4
+) = MPFR_Sub1sp1_mpfr_sub1sp1;
+