added configure option --enable-formally-proven-code and corresponding code

git-svn-id: svn://scm.gforge.inria.fr/svn/mpfr/trunk@13011 280ebfd0-de03-0410-8827-d642c229c3f4

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);
+    }
+  }
+}
+