1/* mpfr_sub1sp1 -- internal function to perform a "real" subtraction on one limb 2 This code was extracted by Kremlin from a formal proof in F* 3 done by F��lix Breton in June-July 2019: do not modify it! 4 5Source: https://github.com/project-everest/hacl-star/tree/dev_mpfr/code/mpfr 6 7Copyright 2004-2023 Free Software Foundation, Inc. 8Contributed by the AriC and Caramba projects, INRIA. 9 10This file is part of the GNU MPFR Library. 11 12The GNU MPFR Library is free software; you can redistribute it and/or modify 13it under the terms of the GNU Lesser General Public License as published by 14the Free Software Foundation; either version 3 of the License, or (at your 15option) any later version. 16 17The GNU MPFR Library is distributed in the hope that it will be useful, but 18WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY 19or FITNESS FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public 20License for more details. 21 22You should have received a copy of the GNU Lesser General Public License 23along with the GNU MPFR Library; see the file COPYING.LESSER. If not, see 24https://www.gnu.org/licenses/ or write to the Free Software Foundation, Inc., 2551 Franklin St, Fifth Floor, Boston, MA 02110-1301, USA. */ 26 27#include "stdint.h" 28#include "inttypes.h" /* for __builtin_clzll */ 29 30/* beginning of manually added declarations */ 31 32#define MPFR_mpfr_sub1sp1 mpfr_sub1sp1 33#define MPFR_RoundingMode_mpfr_rnd_t mpfr_rnd_t 34#define MPFR_Lib_mpfr_struct __mpfr_struct 35#define MPFR_Lib_gmp_NUMB_BITS GMP_NUMB_BITS 36#define __eq__MPFR_RoundingMode_mpfr_rnd_t(x,y) ((x)==(y)) 37#define MPFR_RoundingMode_MPFR_RNDD MPFR_RNDD 38#define MPFR_RoundingMode_MPFR_RNDN MPFR_RNDN 39#define MPFR_RoundingMode_MPFR_RNDZ MPFR_RNDZ 40#define MPFR_RoundingMode_MPFR_RNDU MPFR_RNDU 41#define MPFR_Lib_mpfr_SET_EXP MPFR_SET_EXP 42#define MPFR_Lib_mpfr_RET MPFR_RET 43#define MPFR_Lib_mpfr_NEG_SIGN(x) (-(x)) 44#define MPFR_Exceptions_mpfr_underflow mpfr_underflow 45#define MPFR_Exceptions_mpfr_overflow mpfr_overflow 46#define true 1 47#define false 0 48 49/* the original code had mpfr_exp instead of _mpfr_exp */ 50#define mpfr_exp _mpfr_exp 51/* the original code had mpfr_d instead of _mpfr_d */ 52#define mpfr_d _mpfr_d 53/* the original code had mpfr_prec instead of _mpfr_prec */ 54#define mpfr_prec _mpfr_prec 55/* the original code had mpfr_sign instead of _mpfr_sign */ 56#define mpfr_sign _mpfr_sign 57#define bool int /* to avoid conflict with C++ keyword */ 58 59/* end of manually added declarations */ 60 61static uint32_t MPFR_Lib_Clz_count_leading_zeros (uint64_t a) { 62 return __builtin_clzll(a); 63} 64 65typedef struct MPFR_Add1sp1_state_s 66{ 67 int64_t sh; 68 int64_t bx; 69 uint64_t rb; 70 uint64_t sb; 71} 72MPFR_Add1sp1_state; 73 74typedef struct 75K___MPFR_Lib_mpfr_struct__MPFR_Lib_mpfr_struct__int64_t_int64_t_uint64_t__uint64_t__s 76{ 77 const MPFR_Lib_mpfr_struct *fst; /* added const */ 78 const MPFR_Lib_mpfr_struct *snd; /* added const */ 79 int64_t thd; 80 int64_t f3; 81 uint64_t *f4; 82 uint64_t *f5; 83} 84K___MPFR_Lib_mpfr_struct__MPFR_Lib_mpfr_struct__int64_t_int64_t_uint64_t__uint64_t_; 85 86static MPFR_Add1sp1_state 87MPFR_Add1sp1_mk_state(int64_t sh, int64_t bx, uint64_t rb, uint64_t sb) 88{ 89 MPFR_Add1sp1_state lit; 90 lit.sh = sh; 91 lit.bx = bx; 92 lit.rb = rb; 93 lit.sb = sb; 94 return lit; 95} 96 97static MPFR_Add1sp1_state 98MPFR_Sub1sp1_mpfr_sub1sp1_gt_branch_1( 99 MPFR_Lib_mpfr_struct *a, 100 const MPFR_Lib_mpfr_struct *b, /* added const */ 101 const MPFR_Lib_mpfr_struct *c, /* added const */ 102 uint64_t *ap, 103 uint64_t *bp, 104 uint64_t *cp, 105 int64_t bx, 106 int64_t cx, 107 int64_t p, 108 int64_t sh, 109 uint64_t mask, 110 uint64_t sb_1, 111 uint64_t a0_base 112) 113{ 114 uint32_t cnt = MPFR_Lib_Clz_count_leading_zeros(a0_base); 115 uint64_t a0; 116 if (cnt == (uint32_t)0U) 117 { 118 a0 = a0_base; 119 } 120 else 121 { 122 a0 = a0_base << cnt | sb_1 >> ((uint32_t)64U - cnt); 123 } 124 { 125 uint64_t sb_2 = sb_1 << cnt; 126 uint64_t rb = a0 & (uint64_t)1U << (uint32_t)(sh - (int64_t)1); 127 uint64_t sb = sb_2 | ((a0 & mask) ^ rb); 128 ap[0U] = a0 & ~mask; 129 return MPFR_Add1sp1_mk_state(sh, bx - (int64_t)cnt, rb, sb); 130 } 131} 132 133static bool MPFR_RoundingMode_uu___is_MPFR_RNDN(MPFR_RoundingMode_mpfr_rnd_t projectee) 134{ 135 switch (projectee) 136 { 137 case MPFR_RoundingMode_MPFR_RNDN: 138 { 139 return true; 140 } 141 default: 142 { 143 return false; 144 } 145 } 146} 147 148static bool MPFR_RoundingMode_uu___is_MPFR_RNDZ(MPFR_RoundingMode_mpfr_rnd_t projectee) 149{ 150 switch (projectee) 151 { 152 case MPFR_RoundingMode_MPFR_RNDZ: 153 { 154 return true; 155 } 156 default: 157 { 158 return false; 159 } 160 } 161} 162 163static bool MPFR_RoundingMode_uu___is_MPFR_RNDU(MPFR_RoundingMode_mpfr_rnd_t projectee) 164{ 165 switch (projectee) 166 { 167 case MPFR_RoundingMode_MPFR_RNDU: 168 { 169 return true; 170 } 171 default: 172 { 173 return false; 174 } 175 } 176} 177 178static bool MPFR_RoundingMode_uu___is_MPFR_RNDD(MPFR_RoundingMode_mpfr_rnd_t projectee) 179{ 180 switch (projectee) 181 { 182 case MPFR_RoundingMode_MPFR_RNDD: 183 { 184 return true; 185 } 186 default: 187 { 188 return false; 189 } 190 } 191} 192 193static int32_t 194MPFR_Sub1sp1_mpfr_sub1sp1( 195 MPFR_Lib_mpfr_struct *a, 196 const MPFR_Lib_mpfr_struct *b, /* added const */ 197 const MPFR_Lib_mpfr_struct *c, /* added const */ 198 MPFR_RoundingMode_mpfr_rnd_t rnd_mode, 199 int64_t p 200) 201{ 202 int64_t bx = b->mpfr_exp; 203 int64_t cx = c->mpfr_exp; 204 uint64_t *ap = a->mpfr_d; 205 uint64_t *bp = b->mpfr_d; 206 uint64_t *cp = c->mpfr_d; 207 int64_t sh = MPFR_Lib_gmp_NUMB_BITS - p; 208 uint64_t bp0ul = bp[0U]; 209 uint64_t cp0ul = cp[0U]; 210 if (bx == cx && bp0ul == cp0ul) 211 { 212 if (__eq__MPFR_RoundingMode_mpfr_rnd_t(rnd_mode, MPFR_RoundingMode_MPFR_RNDD)) 213 { 214 MPFR_Lib_mpfr_struct uu____0 = a[0U]; 215 MPFR_Lib_mpfr_struct lit; 216 lit.mpfr_prec = uu____0.mpfr_prec; 217 lit.mpfr_sign = (int32_t)-1; 218 lit.mpfr_exp = uu____0.mpfr_exp; 219 lit.mpfr_d = uu____0.mpfr_d; 220 a[0U] = lit; 221 } 222 else 223 { 224 MPFR_Lib_mpfr_struct uu____1 = a[0U]; 225 MPFR_Lib_mpfr_struct lit; 226 lit.mpfr_prec = uu____1.mpfr_prec; 227 lit.mpfr_sign = (int32_t)1; 228 lit.mpfr_exp = uu____1.mpfr_exp; 229 lit.mpfr_d = uu____1.mpfr_d; 230 a[0U] = lit; 231 } 232 MPFR_Lib_mpfr_SET_EXP(a, (int64_t)-0x7fffffffffffffff); 233 /* the following return was commented out from the extracted code */ 234 /*return*/ MPFR_Lib_mpfr_RET((int32_t)0); 235 } 236 else 237 { 238 MPFR_Add1sp1_state st; 239 if (bx == cx) 240 { 241 /* Prims_int vb = FStar_UInt64_v(bp[0U]); */ /* unused */ 242 /* Prims_int vc = FStar_UInt64_v(cp[0U]); */ /* unused */ 243 /* Prims_int vsh = FStar_Int64_v(sh); */ /* unused */ 244 if (cp[0U] > bp[0U]) 245 { 246 uint64_t a0 = cp[0U] - bp[0U]; 247 uint32_t cnt = MPFR_Lib_Clz_count_leading_zeros(a0); 248 int32_t uu____2 = MPFR_Lib_mpfr_NEG_SIGN(b->mpfr_sign); 249 MPFR_Lib_mpfr_struct uu____3 = a[0U]; 250 MPFR_Lib_mpfr_struct lit; 251 lit.mpfr_prec = uu____3.mpfr_prec; 252 lit.mpfr_sign = uu____2; 253 lit.mpfr_exp = uu____3.mpfr_exp; 254 lit.mpfr_d = uu____3.mpfr_d; 255 a[0U] = lit; 256 ap[0U] = a0 << cnt; 257 { 258 int64_t bx1 = bx - (int64_t)cnt; 259 st = MPFR_Add1sp1_mk_state(sh, bx1, (uint64_t)0U, (uint64_t)0U); 260 } 261 } 262 else 263 { 264 uint64_t a0 = bp[0U] - cp[0U]; 265 uint32_t cnt = MPFR_Lib_Clz_count_leading_zeros(a0); 266 MPFR_Lib_mpfr_struct uu____4 = a[0U]; 267 MPFR_Lib_mpfr_struct lit; 268 lit.mpfr_prec = uu____4.mpfr_prec; 269 lit.mpfr_sign = b->mpfr_sign; 270 lit.mpfr_exp = uu____4.mpfr_exp; 271 lit.mpfr_d = uu____4.mpfr_d; 272 a[0U] = lit; 273 ap[0U] = a0 << cnt; 274 { 275 int64_t bx1 = bx - (int64_t)cnt; 276 st = MPFR_Add1sp1_mk_state(sh, bx1, (uint64_t)0U, (uint64_t)0U); 277 } 278 } 279 } 280 else 281 { 282 K___MPFR_Lib_mpfr_struct__MPFR_Lib_mpfr_struct__int64_t_int64_t_uint64_t__uint64_t_ scrut; 283 if (bx >= cx) 284 { 285 MPFR_Lib_mpfr_struct uu____5 = a[0U]; 286 MPFR_Lib_mpfr_struct lit; 287 lit.mpfr_prec = uu____5.mpfr_prec; 288 lit.mpfr_sign = b->mpfr_sign; 289 lit.mpfr_exp = uu____5.mpfr_exp; 290 lit.mpfr_d = uu____5.mpfr_d; 291 a[0U] = lit; 292 { 293 K___MPFR_Lib_mpfr_struct__MPFR_Lib_mpfr_struct__int64_t_int64_t_uint64_t__uint64_t_ lit0; 294 lit0.fst = b; 295 lit0.snd = c; 296 lit0.thd = bx; 297 lit0.f3 = cx; 298 lit0.f4 = bp; 299 lit0.f5 = cp; 300 scrut = lit0; 301 } 302 } 303 else 304 { 305 int32_t uu____6 = MPFR_Lib_mpfr_NEG_SIGN(b->mpfr_sign); 306 MPFR_Lib_mpfr_struct uu____7 = a[0U]; 307 MPFR_Lib_mpfr_struct lit; 308 lit.mpfr_prec = uu____7.mpfr_prec; 309 lit.mpfr_sign = uu____6; 310 lit.mpfr_exp = uu____7.mpfr_exp; 311 lit.mpfr_d = uu____7.mpfr_d; 312 a[0U] = lit; 313 { 314 K___MPFR_Lib_mpfr_struct__MPFR_Lib_mpfr_struct__int64_t_int64_t_uint64_t__uint64_t_ lit0; 315 lit0.fst = c; 316 lit0.snd = b; 317 lit0.thd = cx; 318 lit0.f3 = bx; 319 lit0.f4 = cp; 320 lit0.f5 = bp; 321 scrut = lit0; 322 } 323 } 324 { 325 const MPFR_Lib_mpfr_struct *b1 = scrut.fst; /* added const */ 326 const MPFR_Lib_mpfr_struct *c1 = scrut.snd; /* added const */ 327 int64_t bx1 = scrut.thd; 328 int64_t cx1 = scrut.f3; 329 uint64_t *bp1 = scrut.f4; 330 uint64_t *cp1 = scrut.f5; 331 int64_t d = bx1 - cx1; 332 uint64_t bp0ul1 = bp1[0U]; 333 uint64_t cp0ul1 = cp1[0U]; 334 uint64_t mask = ((uint64_t)1U << (uint32_t)sh) - (uint64_t)1U; 335 if (d < (int64_t)64) 336 { 337 uint64_t sb_1 = ~(cp0ul1 << (uint32_t)(MPFR_Lib_gmp_NUMB_BITS - d)) + (uint64_t)1U; 338 uint64_t ite; 339 if (sb_1 == (uint64_t)0U) 340 { 341 ite = (uint64_t)0U; 342 } 343 else 344 { 345 ite = (uint64_t)1U; 346 } 347 st = 348 MPFR_Sub1sp1_mpfr_sub1sp1_gt_branch_1(a, 349 b1, 350 c1, 351 ap, 352 bp1, 353 cp1, 354 bx1, 355 cx1, 356 p, 357 sh, 358 mask, 359 sb_1, 360 bp0ul1 - ite - (cp0ul1 >> (uint32_t)d)); 361 } 362 else if (bp0ul1 > (uint64_t)0x8000000000000000U) 363 { 364 ap[0U] = bp0ul1 - ((uint64_t)1U << (uint32_t)sh); 365 st = MPFR_Add1sp1_mk_state(sh, bx1, (uint64_t)1U, (uint64_t)1U); 366 } 367 else 368 { 369 bool 370 rb = 371 sh 372 > (int64_t)1 373 || d > MPFR_Lib_gmp_NUMB_BITS 374 || cp0ul1 == (uint64_t)0x8000000000000000U; 375 bool 376 sb = 377 sh 378 > (int64_t)1 379 || d > MPFR_Lib_gmp_NUMB_BITS 380 || cp0ul1 != (uint64_t)0x8000000000000000U; 381 ap[0U] = ~mask; 382 { 383 uint64_t ite0; 384 if (rb) 385 { 386 ite0 = (uint64_t)1U; 387 } 388 else 389 { 390 ite0 = (uint64_t)0U; 391 } 392 { 393 uint64_t ite; 394 if (sb) 395 { 396 ite = (uint64_t)1U; 397 } 398 else 399 { 400 ite = (uint64_t)0U; 401 } 402 st = MPFR_Add1sp1_mk_state(sh, bx1 - (int64_t)1, ite0, ite); 403 } 404 } 405 } 406 } 407 } 408 /* the constant (int64_t)-0x000000003fffffff from the original extracted 409 code was manually replaced by __gmpfr_emin */ 410 if (st.bx < __gmpfr_emin) 411 { 412 int32_t s = a->mpfr_sign; 413 uint64_t ap0ul = ap[0U]; 414 if 415 ( 416 __eq__MPFR_RoundingMode_mpfr_rnd_t(rnd_mode, 417 MPFR_RoundingMode_MPFR_RNDN) 418 /* the constant (int64_t)-1073741824 from the original extracted 419 code was manually replaced by __gmpfr_emin-1 */ 420 && (st.bx < __gmpfr_emin - 1 || ap0ul == (uint64_t)0x8000000000000000U) 421 ) 422 { 423 MPFR_Lib_mpfr_SET_EXP(a, (int64_t)-0x7fffffffffffffff); 424 return MPFR_Lib_mpfr_NEG_SIGN(s); 425 } 426 else 427 { 428 int32_t t = MPFR_Exceptions_mpfr_underflow(a, rnd_mode, s); 429 return t; 430 } 431 } 432 else 433 { 434 uint64_t a0 = ap[0U]; 435 MPFR_Lib_mpfr_SET_EXP(a, st.bx); 436 if (st.rb == (uint64_t)0U && st.sb == (uint64_t)0U) 437 { 438 /* the following return was commented out from the extracted code */ 439 /*return*/ MPFR_Lib_mpfr_RET((int32_t)0); 440 } 441 else if (MPFR_RoundingMode_uu___is_MPFR_RNDN(rnd_mode)) 442 { 443 if 444 ( 445 st.rb 446 == (uint64_t)0U 447 || (st.sb == (uint64_t)0U && (a0 & (uint64_t)1U << (uint32_t)st.sh) == (uint64_t)0U) 448 ) 449 { 450 /* the following return was commented out from the extracted code */ 451 /*return*/ MPFR_Lib_mpfr_RET(MPFR_Lib_mpfr_NEG_SIGN(a->mpfr_sign)); 452 } 453 else if (ap[0U] + ((uint64_t)1U << (uint32_t)st.sh) == (uint64_t)0U) 454 { 455 ap[0U] = ap[0U] + ((uint64_t)1U << (uint32_t)st.sh); 456 ap[0U] = (uint64_t)0x8000000000000000U; 457 /* the constant (int64_t)0x000000003fffffff from the original 458 extracted code was replaced by __gmpfr_emax */ 459 if (st.bx + (int64_t)1 <= __gmpfr_emax) 460 { 461 MPFR_Lib_mpfr_SET_EXP(a, st.bx + (int64_t)1); 462 /* the following return was commented out from the extracted code */ 463 /*return*/ MPFR_Lib_mpfr_RET(a->mpfr_sign); 464 } 465 else 466 { 467 int32_t t = MPFR_Exceptions_mpfr_overflow(a, rnd_mode, a->mpfr_sign); 468 /* the following return was commented out from the extracted code */ 469 /*return*/ MPFR_Lib_mpfr_RET(t); 470 } 471 } 472 else 473 { 474 ap[0U] = ap[0U] + ((uint64_t)1U << (uint32_t)st.sh); 475 /* the following return was commented out from the extracted code */ 476 /*return*/ MPFR_Lib_mpfr_RET(a->mpfr_sign); 477 } 478 } 479 else 480 { 481 bool uu____8 = a->mpfr_sign < (int32_t)0; 482 if 483 ( 484 MPFR_RoundingMode_uu___is_MPFR_RNDZ(rnd_mode) 485 || (MPFR_RoundingMode_uu___is_MPFR_RNDU(rnd_mode) && uu____8) 486 || (MPFR_RoundingMode_uu___is_MPFR_RNDD(rnd_mode) && !uu____8) 487 ) 488 { 489 /* the following return was commented out from the extracted code */ 490 /*return*/ MPFR_Lib_mpfr_RET(MPFR_Lib_mpfr_NEG_SIGN(a->mpfr_sign)); 491 } 492 else if (ap[0U] + ((uint64_t)1U << (uint32_t)st.sh) == (uint64_t)0U) 493 { 494 ap[0U] = ap[0U] + ((uint64_t)1U << (uint32_t)st.sh); 495 ap[0U] = (uint64_t)0x8000000000000000U; 496 /* the constant (int64_t)0x000000003fffffff from the original 497 extracted code was replaced by __gmpfr_emax */ 498 if (st.bx + (int64_t)1 <= __gmpfr_emax) 499 { 500 MPFR_Lib_mpfr_SET_EXP(a, st.bx + (int64_t)1); 501 /* the following return was commented out from the extracted code */ 502 /*return*/ MPFR_Lib_mpfr_RET(a->mpfr_sign); 503 } 504 else 505 { 506 int32_t t = MPFR_Exceptions_mpfr_overflow(a, rnd_mode, a->mpfr_sign); 507 /* the following return was commented out from the extracted code */ 508 /*return*/ MPFR_Lib_mpfr_RET(t); 509 } 510 } 511 else 512 { 513 ap[0U] = ap[0U] + ((uint64_t)1U << (uint32_t)st.sh); 514 /* the following return was commented out from the extracted code */ 515 /*return*/ MPFR_Lib_mpfr_RET(a->mpfr_sign); 516 } 517 } 518 } 519 } 520} 521 522int32_t 523(*MPFR_mpfr_sub1sp1)( 524 MPFR_Lib_mpfr_struct *x0, 525 const MPFR_Lib_mpfr_struct *x1, /* added const */ 526 const MPFR_Lib_mpfr_struct *x2, /* added const */ 527 MPFR_RoundingMode_mpfr_rnd_t x3, 528 int64_t x4 529) = MPFR_Sub1sp1_mpfr_sub1sp1; 530 531