Skip to content

perf: avoid copying mpz wrappers #14978

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
TwoFX wants to merge 1 commit into from
Closed

perf: avoid copying mpz wrappers #14978

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
69 changes: 48 additions & 21 deletions src/runtime/object.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include <atomic>
#include <string>
#include <utility>
#include <algorithm>
#include <vector>
#include <deque>
Expand Down Expand Up @@ -1359,20 +1360,24 @@ void deactivate_promise(lean_promise_object * promise) {
// =======================================
// Natural numbers

object * alloc_mpz(mpz const & m) {
object * alloc_mpz(mpz && m) {
void * mem = lean_alloc_small_object(sizeof(mpz_object));
#ifdef LEAN_MIMALLOC
// placement new is not guaranteed to preserve this field so store and restore it
unsigned sz = ((lean_object *)mem)->m_cs_sz;
#endif
mpz_object * o = new (mem) mpz_object(m);
mpz_object * o = new (mem) mpz_object(std::move(m));
#ifdef LEAN_MIMALLOC
o->m_header.m_cs_sz = sz;
#endif
lean_set_st_header((lean_object*)o, LeanMPZ, 0);
return (lean_object*)o;
}

object * alloc_mpz(mpz const & m) {
return alloc_mpz(mpz(m));
}

#ifdef LEAN_USE_GMP
extern "C" LEAN_EXPORT lean_object * lean_alloc_mpz(mpz_t v) {
return alloc_mpz(mpz(v));
Expand All @@ -1388,11 +1393,16 @@ object * mpz_to_nat_core(mpz const & m) {
return alloc_mpz(m);
}

static inline obj_res mpz_to_nat(mpz const & m) {
object * mpz_to_nat_core(mpz && m) {
lean_assert(!m.is_size_t() || m.get_size_t() > LEAN_MAX_SMALL_NAT);
return alloc_mpz(std::move(m));
}

static inline obj_res mpz_to_nat(mpz && m) {
if (m.is_size_t() && m.get_size_t() <= LEAN_MAX_SMALL_NAT)
return lean_box(m.get_size_t());
else
return mpz_to_nat_core(m);
return mpz_to_nat_core(std::move(m));
}

extern "C" LEAN_EXPORT object * lean_cstr_to_nat(char const * n) {
Expand Down Expand Up @@ -1580,37 +1590,38 @@ extern "C" LEAN_EXPORT lean_obj_res lean_nat_shiftl(b_lean_obj_arg a1, b_lean_ob
if (lean_is_scalar(a1) && lean_unbox(a1) == 0) {
return lean_box(0);
}
auto a = lean_is_scalar(a1)
? mpz::of_size_t(lean_unbox(a1))
: mpz_value(a1);
if (!lean_is_scalar(a2) || lean_unbox(a2) > UINT_MAX) {
lean_internal_panic("Nat.shiftl exponent is too big");
}
mpz r;
mul2k(r, a, lean_unbox(a2));
return mpz_to_nat(r);
if (lean_is_scalar(a1))
mul2k(r, mpz::of_size_t(lean_unbox(a1)), lean_unbox(a2));
else
mul2k(r, mpz_value(a1), lean_unbox(a2));
return mpz_to_nat(std::move(r));
}

extern "C" LEAN_EXPORT lean_obj_res lean_nat_big_shiftr(b_lean_obj_arg a1, b_lean_obj_arg a2) {
if (!lean_is_scalar(a2)) {
return lean_box(0); // This large of an exponent must be 0.
}
auto a = lean_is_scalar(a1)
? mpz::of_size_t(lean_unbox(a1))
: mpz_value(a1);
size_t s = lean_unbox(a2);
// If the shift amount is large, then we fail if it is not large
// enough to zero out all the bits.
if (s > UINT_MAX) {
if (a.log2() >= s) {
// A scalar has fewer than `UINT_MAX` bits, so all of them are shifted out.
if (!lean_is_scalar(a1) && mpz_value(a1).log2() >= s) {
lean_internal_panic("Nat.shiftr exponent is too big");
} else {
return lean_box(0);
}
}
mpz r;
div2k(r, a, s);
return mpz_to_nat(r);
if (lean_is_scalar(a1))
div2k(r, mpz::of_size_t(lean_unbox(a1)), s);
else
div2k(r, mpz_value(a1), s);
return mpz_to_nat(std::move(r));
}

extern "C" LEAN_EXPORT lean_obj_res lean_nat_pow(b_lean_obj_arg a1, b_lean_obj_arg a2) {
Expand Down Expand Up @@ -1660,23 +1671,39 @@ extern "C" LEAN_EXPORT size_t lean_nat_size_in_bytes(b_lean_obj_arg a) {
// =======================================
// Integers

inline object * mpz_to_int_core(mpz const & m) {
object * mk_int_obj_core(mpz const & m) {
lean_assert(m < LEAN_MIN_SMALL_INT || m > LEAN_MAX_SMALL_INT);
return alloc_mpz(m);
}

static object * mpz_to_int(mpz const & m) {
object * mk_int_obj_core(mpz && m) {
lean_assert(m < LEAN_MIN_SMALL_INT || m > LEAN_MAX_SMALL_INT);
return alloc_mpz(std::move(m));
}

inline object * mpz_to_int_core(mpz && m) {
return mk_int_obj_core(std::move(m));
}

static object * mpz_to_int(mpz && m) {
if (m < LEAN_MIN_SMALL_INT || m > LEAN_MAX_SMALL_INT)
return mpz_to_int_core(m);
return mpz_to_int_core(std::move(m));
else
return lean_box(static_cast<unsigned>(m.get_int()));
}

extern "C" LEAN_EXPORT lean_obj_res lean_big_int_to_nat(lean_obj_arg a) {
lean_assert(!lean_is_scalar(a));
mpz m = mpz_value(a);
lean_dec(a);
return mpz_to_nat(m);
lean_assert(mpz_value(a) >= 0);
mpz const & m = mpz_value(a);
if (m.is_size_t() && m.get_size_t() <= LEAN_MAX_SMALL_NAT) {
obj_res r = lean_box(m.get_size_t());
lean_dec(a);
return r;
} else {
// big `Int` and big `Nat` objects have the same representation
return a;
}
}

extern "C" LEAN_EXPORT object * lean_cstr_to_int(char const * n) {
Expand Down
19 changes: 19 additions & 0 deletions src/runtime/object.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#pragma once
#include <string>
#include <utility>
#include <lean/lean.h>
#include "runtime/mpz.h"

Expand All @@ -23,6 +24,7 @@ struct mpz_object {
mpz m_value;
mpz_object() {}
explicit mpz_object(mpz const & m):m_value(m) {}
explicit mpz_object(mpz && m):m_value(std::move(m)) {}
};

typedef lean_external_class external_object_class;
Expand Down Expand Up @@ -175,6 +177,8 @@ inline object* apply_m(object* f, unsigned n, object** args) { return lean_apply
// MPZ

LEAN_EXPORT object * alloc_mpz(mpz const &);
/* Steals the limbs of `m` instead of copying them into the new object. */
LEAN_EXPORT object * alloc_mpz(mpz &&);
inline mpz_object * to_mpz(object * o) { lean_assert(is_mpz(o)); return (mpz_object*)o; }

// =======================================
Expand Down Expand Up @@ -318,13 +322,21 @@ inline obj_res mk_except_err(obj_arg v) { obj_res r = alloc_cnstr(0, 1, 0); cnst

inline mpz const & mpz_value(b_obj_arg o) { return to_mpz(o)->m_value; }
LEAN_EXPORT object * mpz_to_nat_core(mpz const & m);
LEAN_EXPORT object * mpz_to_nat_core(mpz && m);
inline object * mk_nat_obj_core(mpz const & m) { return mpz_to_nat_core(m); }
inline object * mk_nat_obj_core(mpz && m) { return mpz_to_nat_core(std::move(m)); }
inline obj_res mk_nat_obj(mpz const & m) {
if (m.is_size_t() && m.get_size_t() <= LEAN_MAX_SMALL_NAT)
return box(m.get_size_t());
else
return mk_nat_obj_core(m);
}
inline obj_res mk_nat_obj(mpz && m) {
if (m.is_size_t() && m.get_size_t() <= LEAN_MAX_SMALL_NAT)
return box(m.get_size_t());
else
return mk_nat_obj_core(std::move(m));
}
inline obj_res usize_to_nat(usize n) { return lean_usize_to_nat(n); }
inline obj_res mk_nat_obj(unsigned n) { return lean_unsigned_to_nat(n); }
inline obj_res uint64_to_nat(uint64 n) { return lean_uint64_to_nat(n); }
Expand All @@ -350,12 +362,19 @@ inline obj_res nat_lxor(b_obj_arg a1, b_obj_arg a2) { return lean_nat_lxor(a1, a
// =======================================
// Integers
LEAN_EXPORT object * mk_int_obj_core(mpz const & m);
LEAN_EXPORT object * mk_int_obj_core(mpz && m);
inline obj_res mk_int_obj(mpz const & m) {
if (m < LEAN_MIN_SMALL_INT || m > LEAN_MAX_SMALL_INT)
return mk_int_obj_core(m);
else
return box(static_cast<unsigned>(m.get_int()));
}
inline obj_res mk_int_obj(mpz && m) {
if (m < LEAN_MIN_SMALL_INT || m > LEAN_MAX_SMALL_INT)
return mk_int_obj_core(std::move(m));
else
return box(static_cast<unsigned>(m.get_int()));
}
inline obj_res mk_int_obj(int n) { return lean_int_to_int(n); }
inline obj_res mk_int_obj(int64 n) { return lean_int64_to_int(n); }
inline obj_res nat2int(obj_arg a) { return lean_nat_to_int(a); }
Expand Down
3 changes: 2 additions & 1 deletion src/util/nat.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,10 +19,11 @@ class nat : public object_ref {
explicit nat(unsigned v):object_ref(mk_nat_obj(v)) {}
explicit nat(unsigned long v):object_ref(usize_to_nat(v)) {}
explicit nat(mpz const & v):object_ref(mk_nat_obj(v)) {}
explicit nat(mpz && v):object_ref(mk_nat_obj(std::move(v))) {}
explicit nat(char const * v):object_ref(box(0)) {
mpz m(v);
if (m > 0)
*this = nat(mk_nat_obj(m));
*this = nat(mk_nat_obj(std::move(m)));
}
static nat of_size_t(size_t v) { return nat(lean_usize_to_nat(v)); }

Expand Down
Loading