Viewing file:  sub1sp1_extracted.c (15.4 KB) -rw-r--r--
Select action/file-type:
 (+) |  (+) |  (+) | Code (+) | Session (+) |  (+) | SDB (+) |  (+) |  (+) |  (+) |  (+) |  (+) |
/* 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;
|
