refactor(util/numerics): explicit initialization/finalization

src/init/init.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "util/stackinfo.h"
 #include "util/init_module.h"
+#include "util/numerics/init_module.h"
 #include "util/sexpr/init_module.h"
 #include "kernel/init_module.h"
 #include "kernel/inductive/inductive.h"
@@ -20,6 +21,7 @@ namespace lean {
 void initialize() {
     save_stack_info();
     initialize_util_module();
+    initialize_numerics_module();
     initialize_sexpr_module();
     initialize_kernel_module();
     initialize_inductive_module();
@@ -36,6 +38,7 @@ void finalize() {
     finalize_inductive_module();
     finalize_kernel_module();
     finalize_sexpr_module();
+    finalize_numerics_module();
     finalize_util_module();
 }
 

src/tests/util/numerics/numeric_traits.cpp

@@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/test.h"
+#include "util/init_module.h"
+#include "util/numerics/init_module.h"
 #include "util/numerics/mpq.h"
 #include "util/numerics/mpz.h"
 #include "util/numerics/mpbq.h"
@@ -38,6 +40,10 @@ static void tst1() {
 }
 
 int main() {
+    initialize_util_module();
+    initialize_numerics_module();
     tst1();
+    finalize_numerics_module();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }

src/tests/util/numerics/primes.cpp

@@ -6,7 +6,9 @@ Author: Leonardo de Moura
 */
 #include <iostream>
 #include "util/test.h"
+#include "util/init_module.h"
 #include "util/numerics/primes.h"
+#include "util/numerics/init_module.h"
 using namespace lean;
 
 #define NUM_SMALL_PRIMES 168
@@ -36,8 +38,11 @@ static void tst2() {
 }
 
 int main() {
+    initialize_util_module();
+    initialize_numerics_module();
     tst1();
     tst2();
+    finalize_numerics_module();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }
-

src/util/numerics/CMakeLists.txt

@@ -1,4 +1,4 @@
-add_library(numerics gmp_init.cpp mpz.cpp mpq.cpp mpbq.cpp mpfp.cpp
+add_library(numerics init_module.cpp mpz.cpp mpq.cpp mpbq.cpp mpfp.cpp
 float.cpp double.cpp numeric_traits.cpp primes.cpp zpz.cpp)
 
 target_link_libraries(numerics ${LEAN_LIBS} ${EXTRA_LIBS})

src/util/numerics/gmp_init.cpp

@@ -1,26 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <gmp.h>
-#include "util/memory.h"
-
-extern "C" void * cxx_malloc(size_t size) { return lean::malloc(size); }
-extern "C" void * cxx_realloc(void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); }
-extern "C" void cxx_free(void * p, size_t) { return lean::free(p); }
-
-/**
-   \brief Auxiliary class for initializing the GMP memory allocation
-   functions. We overhide the default ones because we want to sign
-   the C++ exception std::bad_alloc when we run out-of-memory.
-*/
-class gmp_init {
-public:
-    gmp_init() {
-        mp_set_memory_functions(cxx_malloc, cxx_realloc, cxx_free);
-    }
-};
-
-gmp_init g_gmp_init;

src/util/numerics/init_module.cpp

@@ -0,0 +1,39 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <gmp.h>
+#include "util/memory.h"
+#include "util/numerics/mpz.h"
+#include "util/numerics/mpq.h"
+#include "util/numerics/mpbq.h"
+#include "util/numerics/mpfp.h"
+#include "util/numerics/zpz.h"
+#include "util/numerics/primes.h"
+
+namespace lean {
+extern "C" void * cxx_malloc(size_t size) { return lean::malloc(size); }
+extern "C" void * cxx_realloc(void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); }
+extern "C" void cxx_free(void * p, size_t) { return lean::free(p); }
+
+void initialize_numerics_module() {
+    mp_set_memory_functions(cxx_malloc, cxx_realloc, cxx_free);
+    initialize_mpz();
+    initialize_mpq();
+    initialize_mpbq();
+    initialize_mpfp();
+    initialize_zpz();
+    initialize_primes();
+}
+
+void finalize_numerics_module() {
+    finalize_primes();
+    finalize_zpz();
+    finalize_mpfp();
+    finalize_mpbq();
+    finalize_mpq();
+    finalize_mpz();
+}
+}

src/util/numerics/init_module.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+void initialize_numerics_module();
+void finalize_numerics_module();
+}

src/util/numerics/mpbq.cpp

@@ -350,10 +350,17 @@ void display_decimal(std::ostream & out, mpbq const & a, unsigned prec) {
     }
 }
 
-static mpbq g_zero;
+static mpbq * g_zero = nullptr;
 mpbq const & numeric_traits<mpbq>::zero() {
-    lean_assert(is_zero(g_zero));
-    return g_zero;
+    lean_assert(is_zero(*g_zero));
+    return *g_zero;
+}
+
+void initialize_mpbq() {
+    g_zero = new mpbq();
+}
+void finalize_mpbq() {
+    delete g_zero;
 }
 }
 

src/util/numerics/mpbq.h

@@ -305,5 +305,6 @@ public:
     static void acosh(mpbq & ) { lean_unreachable(); } // LCOV_EXCL_LINE
     static void atanh(mpbq & ) { lean_unreachable(); } // LCOV_EXCL_LINE
 };
-
+void initialize_mpbq();
+void finalize_mpbq();
 }

src/util/numerics/mpfp.cpp

@@ -13,10 +13,6 @@ Author: Soonho Kong
 namespace lean {
 MK_THREAD_LOCAL_GET(mpfr_rnd_t, get_g_mpfp_rnd, MPFR_RNDN);
 
-mpfp numeric_traits<mpfp>::pi_l;
-mpfp numeric_traits<mpfp>::pi_n;
-mpfp numeric_traits<mpfp>::pi_u;
-
 void set_mpfp_rnd(bool plus_inf) {
     get_g_mpfp_rnd() = plus_inf ? MPFR_RNDU : MPFR_RNDD;
 }
@@ -25,16 +21,6 @@ mpfr_rnd_t get_mpfp_rnd() {
     return get_g_mpfp_rnd();
 }
 
-/**
-    \brief Auxiliary class for invoking mpfr_free_cache before
-    exiting and avoiding Valgrind memory leak warnings.
-*/
-class mpfr_finalizer {
-public:
-    ~mpfr_finalizer() { mpfr_free_cache(); }
-};
-static mpfr_finalizer g_mpfr_finalizer;
-
 inline unsigned necessary_digits(mpfr_prec_t p) {
     static constexpr double LOG10_2 = 0.30102999566;
     return std::ceil(p * LOG10_2) + 2;
@@ -51,11 +37,19 @@ std::ostream & operator<<(std::ostream & out, mpfp const & v) {
     return out;
 }
 
-static mpfp g_zero(0.0);
+static mpfp * g_zero = nullptr;
 mpfp const & numeric_traits<mpfp>::zero() {
-    lean_assert(is_zero(g_zero));
-    return g_zero;
-}
+    lean_assert(is_zero(*g_zero));
+    return *g_zero;
 }
 
+void initialize_mpfp() {
+    g_zero = new mpfp(0.0);
+}
+
+void finalize_mpfp() {
+    delete g_zero;
+    mpfr_free_cache();
+}
+}
 void print(lean::mpfp const & v) { std::cout << v << std::endl; }

src/util/numerics/mpfp.h

@@ -513,19 +513,18 @@ public:
     static void ceil(mpfp & v) { v.ceil(); }
     static void floor(mpfp & v) { v.floor(); }
 
-    // constants
-    static mpfp pi_l;
-    static mpfp pi_n;
-    static mpfp pi_u;
     static inline mpfp pi_lower()       {
+        mpfp pi_l;
         mpfr_const_pi(pi_l.m_val, MPFR_RNDD);
         return pi_l;
     }
     static inline mpfp pi()             {
+        mpfp pi_n;
         mpfr_const_pi(pi_n.m_val, MPFR_RNDN);
         return pi_n;
     }
     static inline mpfp pi_upper()       {
+        mpfp pi_u;
         mpfr_const_pi(pi_u.m_val, MPFR_RNDU);
         return pi_u;
     }
@@ -559,4 +558,6 @@ public:
     static void acosh(mpfp & v) { LEAN_TRANS_MPFP_FUNC(acosh, v, rnd()); }
     static void atanh(mpfp & v) { LEAN_TRANS_MPFP_FUNC(atanh, v, rnd()); }
 };
+void initialize_mpfp();
+void finalize_mpfp();
 }

src/util/numerics/mpq.cpp

@@ -10,10 +10,21 @@ Author: Leonardo de Moura
 #include "util/numerics/mpbq.h"
 
 namespace lean {
+mpq * numeric_traits<mpq>::pi_l = nullptr;
+mpq * numeric_traits<mpq>::pi_n = nullptr;
+mpq * numeric_traits<mpq>::pi_u = nullptr;
 
-const mpq numeric_traits<mpq>::pi_l((3373259426.0 + 273688.0 / (1<<21)) / (1<<30));
-const mpq numeric_traits<mpq>::pi_n((3373259426.0 + 273688.0 / (1<<21)) / (1<<30));
-const mpq numeric_traits<mpq>::pi_u((3373259426.0 + 273688.0 / (1<<21)) / (1<<30));
+void numeric_traits<mpq>::initialize() {
+    pi_l = new mpq((3373259426.0 + 273688.0 / (1<<21)) / (1<<30));
+    pi_n = new mpq((3373259426.0 + 273688.0 / (1<<21)) / (1<<30));
+    pi_u = new mpq((3373259426.0 + 273688.0 / (1<<21)) / (1<<30));
+}
+
+void numeric_traits<mpq>::finalize() {
+    delete pi_l;
+    delete pi_n;
+    delete pi_u;
+}
 
 mpq & mpq::operator=(mpbq const & b) {
     *this = 2;
@@ -119,11 +130,11 @@ void display_decimal(std::ostream & out, mpq const & a, unsigned prec) {
     out << "?";
 }
 
-static mpq g_zero;
+static mpq * g_zero = nullptr;
 
 mpq const & numeric_traits<mpq>::zero() {
-    lean_assert(is_zero(g_zero));
-    return g_zero;
+    lean_assert(is_zero(*g_zero));
+    return *g_zero;
 }
 
 serializer & operator<<(serializer & s, mpq const & n) {
@@ -133,6 +144,16 @@ serializer & operator<<(serializer & s, mpq const & n) {
     return s;
 }
 
+void initialize_mpq() {
+    g_zero = new mpq();
+    numeric_traits<mpq>::initialize();
+}
+
+void finalize_mpq() {
+    numeric_traits<mpq>::finalize();
+    delete g_zero;
+}
+
 mpq read_mpq(deserializer & d) {
     return mpq(d.read_string().c_str());
 }

src/util/numerics/mpq.h

@@ -223,7 +223,13 @@ public:
 
 template<>
 class numeric_traits<mpq> {
+    static mpq * pi_l;
+    static mpq * pi_n;
+    static mpq * pi_u;
 public:
+    static void initialize();
+    static void finalize();
+
     static bool precise() { return true; }
     static bool is_zero(mpq const &  v) { return v.is_zero(); }
     static bool is_pos(mpq const & v) { return v.is_pos(); }
@@ -240,18 +246,15 @@ public:
     static void floor(mpq & v) { v.floor(); }
 
     // constants
-    static const  mpq pi_l;
-    static const  mpq pi_n;
-    static const  mpq pi_u;
-    static inline mpq pi_lower()       { return pi_l;     }
-    static inline mpq pi()             { return pi_n;     }
-    static inline mpq pi_upper()       { return pi_u;     }
-    static inline mpq pi_half_lower()  { return pi_l / 2; }
-    static inline mpq pi_half()        { return pi_n / 2; }
-    static inline mpq pi_half_upper()  { return pi_u / 2; }
-    static inline mpq pi_twice_lower() { return pi_l * 2; }
-    static inline mpq pi_twice()       { return pi_n * 2; }
-    static inline mpq pi_twice_upper() { return pi_u * 2; }
+    static inline mpq pi_lower()       { return *pi_l;     }
+    static inline mpq pi()             { return *pi_n;     }
+    static inline mpq pi_upper()       { return *pi_u;     }
+    static inline mpq pi_half_lower()  { return *pi_l / 2; }
+    static inline mpq pi_half()        { return *pi_n / 2; }
+    static inline mpq pi_half_upper()  { return *pi_u / 2; }
+    static inline mpq pi_twice_lower() { return *pi_l * 2; }
+    static inline mpq pi_twice()       { return *pi_n * 2; }
+    static inline mpq pi_twice_upper() { return *pi_u * 2; }
 
     // Transcendental functions
     static void exp(mpq & )   { lean_unreachable(); } // LCOV_EXCL_LINE
@@ -284,4 +287,7 @@ inline deserializer & operator>>(deserializer & d, mpq & n) { n = read_mpq(d); r
 UDATA_DEFS(mpq)
 mpq to_mpq_ext(lua_State * L, int idx);
 void open_mpq(lua_State * L);
+
+void initialize_mpq();
+void finalize_mpq();
 }

src/util/numerics/mpz.cpp

@@ -77,11 +77,19 @@ std::ostream & operator<<(std::ostream & out, mpz const & v) {
     return out;
 }
 
-static mpz g_zero;
+static mpz * g_zero = nullptr;
 
 mpz const & numeric_traits<mpz>::zero() {
-    lean_assert(is_zero(g_zero));
-    return g_zero;
+    lean_assert(is_zero(*g_zero));
+    return *g_zero;
+}
+
+void initialize_mpz() {
+    g_zero = new mpz();
+}
+
+void finalize_mpz() {
+    delete g_zero;
 }
 
 serializer & operator<<(serializer & s, mpz const & n) {

src/util/numerics/mpz.h

@@ -244,4 +244,7 @@ inline deserializer & operator>>(deserializer & d, mpz & n) { n = read_mpz(d); r
 UDATA_DEFS(mpz)
 mpz to_mpz_ext(lua_State * L, int idx);
 void open_mpz(lua_State * L);
+
+void initialize_mpz();
+void finalize_mpz();
 }

src/util/numerics/primes.cpp

@@ -90,9 +90,18 @@ public:
     }
 };
 
-static prime_generator g_prime_generator;
-static mutex           g_prime_generator_mutex;
+static prime_generator * g_prime_generator = nullptr;
+static mutex           * g_prime_generator_mutex = nullptr;
 
+void initialize_primes() {
+    g_prime_generator = new prime_generator();
+    g_prime_generator_mutex = new mutex();
+}
+
+void finalize_primes() {
+    delete g_prime_generator_mutex;
+    delete g_prime_generator;
+}
 
 prime_iterator::prime_iterator():
     m_idx(0) {
@@ -102,8 +111,8 @@ uint64 prime_iterator::next() {
     unsigned idx = m_idx;
     m_idx++;
     {
-        lock_guard<mutex> guard(g_prime_generator_mutex);
-        return g_prime_generator(idx);
+        lock_guard<mutex> guard(*g_prime_generator_mutex);
+        return (*g_prime_generator)(idx);
     }
 }
 

src/util/numerics/primes.h

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#pragma once
 #include "util/int64.h"
 
 namespace lean {
@@ -17,4 +18,7 @@ public:
 };
 /** \brief Return true iff \c p is a prime number. */
 bool is_prime(uint64 p);
+
+void initialize_primes();
+void finalize_primes();
 }

src/util/numerics/zpz.cpp

@@ -19,8 +19,14 @@ void zpz::inv() {
     m_value = remainder(a, static_cast<int64>(m_p));
 }
 
-static zpz g_zero;
+static zpz * g_zero = nullptr;
 zpz const & numeric_traits<zpz>::zero() {
-    return g_zero;
+    return *g_zero;
+}
+void initialize_zpz() {
+    g_zero = new zpz();
+}
+void finalize_zpz() {
+    delete g_zero;
 }
 }

src/util/numerics/zpz.h

@@ -115,4 +115,7 @@ public:
     static void power(zpz & v, unsigned k) { v = lean::power(v, k); }
     static zpz const & zero();
 };
+
+void initialize_zpz();
+void finalize_zpz();
 }