max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(runtime): C backend

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-21 21:04:42 -07:00
parent cf18cda557
commit dcd15f3424
24 changed files with 1335 additions and 2450 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/CMakeLists.txt
View file

@ -530,8 +530,7 @@ function(add_exec_test name tgt)
endif()
endfunction()
# C++ unit tests are disabled for now since they rely on `format` which relies on `Lean` generated code.
# add_subdirectory(tests/util)
add_subdirectory(tests/util)
# Include style check
if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows") AND PYTHONINTERP_FOUND)

4
src/kernel/local_ctx.cpp
View file

@ -61,7 +61,7 @@ local_decl local_ctx::mk_local_decl(name const & n, name const & un, expr const
object * p = lean_local_ctx_mk_let_decl(raw(), n.to_obj_arg(), un.to_obj_arg(), type.to_obj_arg(), value.to_obj_arg());
local_decl decl(cnstr_get(p, 0));
m_obj = cnstr_get(p, 1);
free_heap_obj(p);
lean_free_heap_obj(p);
return decl;
}
@ -69,7 +69,7 @@ local_decl local_ctx::mk_local_decl(name const & n, name const & un, expr const
object * p = lean_local_ctx_mk_local_decl(raw(), n.to_obj_arg(), un.to_obj_arg(), type.to_obj_arg(), static_cast<uint8>(bi));
local_decl decl(cnstr_get(p, 0));
m_obj = cnstr_get(p, 1);
free_heap_obj(p);
lean_free_heap_obj(p);
return decl;
}

4
src/library/module.cpp
View file

@ -155,7 +155,7 @@ extern "C" object * lean_serialize_modifications(object * mod_list, object * w)
std::string bytes = out.str();
object * r = alloc_sarray(1, bytes.size(), bytes.size());
memcpy(sarray_cptr<uint8>(r), bytes.data(), bytes.size());
memcpy(sarray_cptr(r), bytes.data(), bytes.size());
return set_io_result(w, r);
} catch (exception & ex) {
@ -165,7 +165,7 @@ extern "C" object * lean_serialize_modifications(object * mod_list, object * w)
extern "C" object * lean_perform_serialized_modifications(object * env0, object * bytes, object * w) {
environment env(env0);
std::string code(sarray_cptr<char>(bytes), sarray_size(bytes));
std::string code((char*)sarray_cptr(bytes), sarray_size(bytes));
dec_ref(bytes);
try {
std::istringstream in(code, std::ios_base::binary);

53
src/runtime/alloc.cpp
View file

@ -7,12 +7,9 @@ Author: Leonardo de Moura
#include <vector>
#include "runtime/thread.h"
#include "runtime/debug.h"
#include "runtime/compiler_hints.h"
#include "runtime/object.h"
#include "runtime/alloc.h"
#include "runtime/lean.h"
#define LEAN_OBJECT_SIZE_DELTA 8
#define LEAN_MAX_SMALL_OBJECT_SIZE 512
#define LEAN_PAGE_SIZE 8192 // 8 Kb
#define LEAN_SEGMENT_SIZE 8*1024*1024 // 8 Mb
#define LEAN_NUM_SLOTS (LEAN_MAX_SMALL_OBJECT_SIZE / LEAN_OBJECT_SIZE_DELTA)
@ -73,12 +70,8 @@ struct page {
void push_free_obj(void * o);
};
inline size_t align(size_t v, size_t a) {
return (v / a)*a + a * (v % a != 0);
}
inline char * align_ptr(char * p, size_t a) {
return reinterpret_cast<char*>(align(reinterpret_cast<size_t>(p), a));
return reinterpret_cast<char*>(lean_align(reinterpret_cast<size_t>(p), a));
}
struct segment {
@ -149,12 +142,6 @@ LEAN_THREAD_GLOBAL_PTR(page *, g_curr_pages);
LEAN_THREAD_PTR(heap, g_heap);
static heap_manager * g_heap_manager = nullptr;
inline unsigned get_slot_idx(unsigned obj_size) {
lean_assert(obj_size > 0);
lean_assert(align(obj_size, LEAN_OBJECT_SIZE_DELTA) == obj_size);
return obj_size / LEAN_OBJECT_SIZE_DELTA - 1;
}
inline void set_next_obj(void * obj, void * next) {
*reinterpret_cast<void**>(obj) = next;
}
@ -300,7 +287,7 @@ void heap::alloc_segment() {
}
static page * alloc_page(heap * h, unsigned obj_size) {
lean_assert(align(obj_size, LEAN_OBJECT_SIZE_DELTA) == obj_size);
lean_assert(lean_align(obj_size, LEAN_OBJECT_SIZE_DELTA) == obj_size);
segment * s = h->m_curr_segment;
LEAN_RUNTIME_STAT_CODE(g_num_pages++);
page * p = new (s->m_next_page_mem) page();
@ -309,7 +296,7 @@ static page * alloc_page(heap * h, unsigned obj_size) {
/* s is full, we need to allocate a new one. */
h->alloc_segment();
}
unsigned slot_idx = get_slot_idx(obj_size);
unsigned slot_idx = lean_get_slot_idx(obj_size);
p->m_header.m_heap = h;
page_list_insert(h->m_curr_page[slot_idx], p);
p->m_header.m_slot_idx = slot_idx;
@ -372,17 +359,7 @@ void init_thread_heap() {
init_heap(false);
}
void * alloc(size_t sz) {
sz = align(sz, LEAN_OBJECT_SIZE_DELTA);
LEAN_RUNTIME_STAT_CODE(g_num_alloc++);
if (LEAN_UNLIKELY(sz > LEAN_MAX_SMALL_OBJECT_SIZE)) {
void * r = malloc(sz);
if (r == nullptr) throw std::bad_alloc();
return r;
}
lean_assert(g_heap);
LEAN_RUNTIME_STAT_CODE(g_num_small_alloc++);
unsigned slot_idx = get_slot_idx(sz);
extern "C" void * lean_alloc_small(unsigned sz, unsigned slot_idx) {
page * p = g_heap->m_curr_page[slot_idx];
void * r = p->m_header.m_free_list;
if (LEAN_UNLIKELY(r == nullptr)) {
@ -402,6 +379,20 @@ void * alloc(size_t sz) {
return r;
}
void * alloc(size_t sz) {
sz = lean_align(sz, LEAN_OBJECT_SIZE_DELTA);
LEAN_RUNTIME_STAT_CODE(g_num_alloc++);
if (LEAN_UNLIKELY(sz > LEAN_MAX_SMALL_OBJECT_SIZE)) {
void * r = malloc(sz);
if (r == nullptr) lean_panic_out_of_memory();
return r;
}
lean_assert(g_heap);
LEAN_RUNTIME_STAT_CODE(g_num_small_alloc++);
unsigned slot_idx = lean_get_slot_idx(sz);
return lean_alloc_small(sz, slot_idx);
}
static inline void dealloc_small_core(void * o) {
LEAN_RUNTIME_STAT_CODE(g_num_small_dealloc++);
if (LEAN_UNLIKELY(g_heap == nullptr)) {
@ -424,18 +415,18 @@ static inline void dealloc_small_core(void * o) {
void dealloc(void * o, size_t sz) {
LEAN_RUNTIME_STAT_CODE(g_num_dealloc++);
sz = align(sz, LEAN_OBJECT_SIZE_DELTA);
sz = lean_align(sz, LEAN_OBJECT_SIZE_DELTA);
if (LEAN_UNLIKELY(sz > LEAN_MAX_SMALL_OBJECT_SIZE)) {
return free(o);
}
dealloc_small_core(o);
}
void dealloc_small(void * o) {
extern "C" void lean_free_small(void * o) {
dealloc_small_core(o);
}
unsigned get_small_object_size(void * o) {
extern "C" unsigned lean_small_mem_size(void * o) {
page * p = get_page_of(o);
return p->m_header.m_obj_size;
}

2
src/runtime/alloc.h
View file

@ -11,8 +11,6 @@ namespace lean {
void init_thread_heap();
void * alloc(size_t sz);
void dealloc(void * o, size_t sz);
void dealloc_small(void * o);
unsigned get_small_object_size(void * o);
void initialize_alloc();
void finalize_alloc();
}

902
src/runtime/apply.cpp
View file

File diff suppressed because it is too large Load diff

119
src/runtime/compact.cpp
View file

@ -12,23 +12,18 @@ Author: Leonardo de Moura
#define LEAN_COMPACTOR_INIT_SZ 1024*1024
namespace lean {
#define TERMINATOR_ID (static_cast<unsigned>(object_kind::External) + 1)
/*
Special object that terminates the data block constructing the object graph rooted in `m_value`.
We use this object to ensure `m_value` is correctly aligned. In the past, we would allocate
a chunk of memory `p` of size `sizeof(object) + sizeof(object*)`, and then write at `p + sizeof(object)`.
This is incorrect because `sizeof(object)` is not a multiple of the word size.
*/
struct terminator_object : public object {
object * m_value;
explicit terminator_object(object * value) : object(object_kind::External, object_memory_kind::Region), m_value(value) {
// not an actual `object_kind`, so write to the field directly
m_kind = TERMINATOR_ID;
}
struct terminator_object {
lean_object m_header;
lean_object * m_value;
};
object_compactor::object_compactor():
m_begin(malloc(LEAN_COMPACTOR_INIT_SZ)),
m_end(m_begin),
@ -75,16 +70,17 @@ object_offset object_compactor::to_offset(object * o) {
}
void object_compactor::insert_terminator(object * o) {
void * mem = alloc(sizeof(terminator_object));
new (mem) terminator_object(to_offset(o));
terminator_object * t = (terminator_object*) alloc(sizeof(terminator_object));
lean_set_other_header((lean_object*)t, LeanReserved, 0);
t->m_value = to_offset(o);
}
object * object_compactor::copy_object(object * o) {
size_t sz = obj_byte_size(o);
size_t sz = lean_object_byte_size(o);
void * mem = alloc(sz);
memcpy(mem, o, sz);
object * r = static_cast<object*>(mem);
r->m_mem_kind = static_cast<unsigned>(object_memory_kind::Region);
lean_set_other_mem_kind(r);
save(o, r);
return r;
}
@ -121,12 +117,15 @@ bool object_compactor::insert_array(object * o) {
}
if (missing_children)
return false;
void * mem = alloc(sizeof(array_object) + sz * sizeof(object *));
object * new_o = new (mem) array_object(sz, sz, object_memory_kind::Region);
lean_array_object * new_o = (lean_array_object*)alloc(sizeof(lean_array_object) + sizeof(void*)*sz);
lean_set_other_header((lean_object*)new_o, LeanArray, 0);
new_o->m_size = sz;
new_o->m_capacity = sz;
for (size_t i = 0; i < sz; i++) {
array_set(new_o, i, offsets[i]);
array_set((lean_object*)new_o, i, offsets[i]);
}
save(o, new_o);
save(o, (lean_object*)new_o);
return true;
}
@ -136,17 +135,17 @@ bool object_compactor::insert_thunk(object * o) {
if (c == g_null_offset)
return false;
object * r = copy_object(o);
to_thunk(r)->m_value = c;
lean_to_thunk(r)->m_value = c;
return true;
}
bool object_compactor::insert_ref(object * o) {
object * v = to_ref(o)->m_value;
object * v = lean_to_ref(o)->m_value;
object_offset c = to_offset(v);
if (c == g_null_offset)
return false;
object * r = copy_object(o);
to_ref(r)->m_value = c;
lean_to_ref(r)->m_value = c;
return true;
}
@ -164,9 +163,11 @@ bool object_compactor::insert_task(object * o) {
To cope with this issue, we always save tasks as thunks,
and rely on the fact that all task API accepts thunks as arguments
even when multi-threading is enabled. */
void * mem = alloc(sizeof(thunk_object));
object * new_o = new (mem) thunk_object(c, true, object_memory_kind::Region);
save(o, new_o);
lean_thunk_object * new_o = (lean_thunk_object*)alloc(sizeof(lean_thunk_object));
lean_set_other_header((lean_object*)new_o, LeanThunk, 0);
new_o->m_value = c;
new_o->m_closure = (lean_object*)0;
save(o, (lean_object*)new_o);
return true;
}
@ -177,8 +178,9 @@ void object_compactor::insert_mpz(object * o) {
into an mpz number. So, we use std::max to make sure we have enough space for both. */
size_t extra_space = std::max(s.size() + 1, sizeof(mpz_object*));
void * mem = alloc(sizeof(mpz_object) + extra_space);
object * new_o = new (mem) object(object_kind::MPZ, object_memory_kind::Region);
save(o, new_o);
mpz_object * new_o = new (mem) mpz_object();
lean_set_other_header((lean_object*)new_o, LeanMPZ, 0);
save(o, (lean_object*)new_o);
void * data = reinterpret_cast<char*>(new_o) + sizeof(mpz_object);
memcpy(data, s.c_str(), s.size() + 1);
}
@ -195,17 +197,18 @@ void object_compactor::operator()(object * o) {
}
lean_assert(!is_scalar(curr));
bool r = true;
switch (get_kind(curr)) {
case object_kind::Constructor: r = insert_constructor(curr); break;
case object_kind::Closure: throw exception("closures cannot be compacted");
case object_kind::Array: r = insert_array(curr); break;
case object_kind::ScalarArray: copy_object(curr); break;
case object_kind::String: copy_object(curr); break;
case object_kind::MPZ: insert_mpz(curr); break;
case object_kind::Thunk: r = insert_thunk(curr); break;
case object_kind::Task: r = insert_task(curr); break;
case object_kind::Ref: r = insert_ref(curr); break;
case object_kind::External: throw exception("external objects cannot be compacted");
switch (lean_ptr_tag(curr)) {
case LeanClosure: throw exception("closures cannot be compacted");
case LeanArray: r = insert_array(curr); break;
case LeanScalarArray: copy_object(curr); break;
case LeanString: copy_object(curr); break;
case LeanMPZ: insert_mpz(curr); break;
case LeanThunk: r = insert_thunk(curr); break;
case LeanTask: r = insert_task(curr); break;
case LeanRef: r = insert_ref(curr); break;
case LeanExternal: throw exception("external objects cannot be compacted");
case LeanReserved: lean_unreachable();
default: r = insert_constructor(curr); break;
}
if (r) m_todo.pop_back();
}
@ -256,7 +259,7 @@ inline void compacted_region::fix_constructor(object * o) {
for (; it != end; it++) {
*it = fix_object_ptr(*it);
}
move(cnstr_byte_size(o));
move(lean_ctor_byte_size(o));
}
inline void compacted_region::fix_array(object * o) {
@ -265,17 +268,17 @@ inline void compacted_region::fix_array(object * o) {
for (; it != end; it++) {
*it = fix_object_ptr(*it);
}
move(array_byte_size(o));
move(lean_array_byte_size(o));
}
inline void compacted_region::fix_thunk(object * o) {
to_thunk(o)->m_value = fix_object_ptr(to_thunk(o)->m_value);
move(sizeof(thunk_object));
lean_to_thunk(o)->m_value = fix_object_ptr(lean_to_thunk(o)->m_value);
move(sizeof(lean_thunk_object));
}
inline void compacted_region::fix_ref(object * o) {
to_ref(o)->m_value = fix_object_ptr(to_ref(o)->m_value);
move(sizeof(ref_object));
lean_to_ref(o)->m_value = fix_object_ptr(lean_to_ref(o)->m_value);
move(sizeof(lean_ref_object));
}
void compacted_region::fix_mpz(object * o) {
@ -290,10 +293,10 @@ void compacted_region::fix_mpz(object * o) {
sz++;
}
/* use string to initialize memory */
new (&(to_mpz(o)->m_value)) mpz(s.c_str());
new (&(((mpz_object*)o)->m_value)) mpz(s.c_str());
/* update m_nested_mpzs list */
*reinterpret_cast<mpz_object**>(m_next) = m_nested_mpzs;
m_nested_mpzs = to_mpz(o);
m_nested_mpzs = (mpz_object*)o;
/* consume region after mpz_object */
sz++; // string delimiter
if (sz < sizeof(mpz_object*))
@ -307,23 +310,23 @@ object * compacted_region::read() {
while (true) {
lean_assert(static_cast<char*>(m_next) + sizeof(object) <= m_end);
object * curr = reinterpret_cast<object*>(m_next);
if (curr->m_kind == TERMINATOR_ID) {
switch (lean_ptr_tag(curr)) {
case LeanClosure: lean_unreachable();
case LeanArray: fix_array(curr); break;
case LeanScalarArray: move(lean_sarray_byte_size(curr)); break;
case LeanString: move(lean_string_byte_size(curr)); break;
case LeanMPZ: fix_mpz(curr); break;
case LeanThunk: fix_thunk(curr); break;
case LeanRef: fix_ref(curr); break;
case LeanTask: lean_unreachable();
case LeanExternal: lean_unreachable();
case LeanReserved: {
object * r = reinterpret_cast<terminator_object*>(m_next)->m_value;
move(sizeof(terminator_object));
return fix_object_ptr(r);
} else {
switch (get_kind(curr)) {
case object_kind::Constructor: fix_constructor(curr); break;
case object_kind::Closure: lean_unreachable();
case object_kind::Array: fix_array(curr); break;
case object_kind::ScalarArray: move(sarray_byte_size(curr)); break;
case object_kind::String: move(string_byte_size(curr)); break;
case object_kind::MPZ: fix_mpz(curr); break;
case object_kind::Thunk: fix_thunk(curr); break;
case object_kind::Ref: fix_ref(curr); break;
case object_kind::Task: lean_unreachable();
case object_kind::External: lean_unreachable();
}
}
default:
fix_constructor(curr); break;
}
}
}

2
src/runtime/compact.h
View file

@ -11,7 +11,7 @@ Author: Leonardo de Moura
#include "runtime/object.h"
namespace lean {
typedef object * object_offset;
typedef lean_object * object_offset;
class object_compactor {
std::unordered_map<object*, object_offset, std::hash<object*>, std::equal_to<object*>> m_obj_table;

1
src/runtime/debug.h
View file

@ -8,7 +8,6 @@ Author: Leonardo de Moura
#include <iostream>
#include <typeinfo>
#include "runtime/exception.h"
#include "runtime/compiler_hints.h"
#ifndef __has_builtin
#define __has_builtin(x) 0

48
src/runtime/io.cpp
View file

@ -14,12 +14,14 @@ Author: Leonardo de Moura
#endif
#include <iostream>
#include <chrono>
#include <sstream>
#include <fstream>
#include <iomanip>
#include <string>
#include <cstdlib>
#include <sys/stat.h>
#include "runtime/object.h"
#include "runtime/thread.h"
#include "runtime/allocprof.h"
#ifdef _MSC_VER
@ -31,7 +33,7 @@ Author: Leonardo de Moura
namespace lean {
static obj_res const REAL_WORLD = box(0);
void io_result_show_error(b_obj_arg r) {
extern "C" void lean_io_result_show_error(b_obj_arg r) {
std::cerr << "uncaught exception: " << string_cstr(io_result_get_error(r)) << std::endl;
}
@ -76,7 +78,7 @@ obj_res set_io_error(obj_arg r, std::string const & msg) {
}
static bool g_initializing = true;
void io_mark_end_initialization() {
extern "C" void lean_io_mark_end_initialization() {
g_initializing = false;
}
@ -254,15 +256,17 @@ extern "C" obj_res lean_io_app_dir(obj_arg r) {
// =======================================
// IO ref primitives
obj_res io_mk_ref(obj_arg a, obj_arg r) {
object * ref = new (alloc_heap_object(sizeof(ref_object))) ref_object(a);
return set_io_result(r, ref);
extern "C" obj_res lean_io_mk_ref(obj_arg a, obj_arg r) {
lean_ref_object * o = (lean_ref_object*)lean_alloc_small_object(sizeof(lean_ref_object));
lean_set_st_header((lean_object*)o, LeanRef, 0);
o->m_value = a;
return set_io_result(r, (lean_object*)o);
}
static object * g_io_error_nullptr_read = nullptr;
static inline atomic<object*> * mt_ref_val_addr(object * o) {
return reinterpret_cast<atomic<object*> *>(&(to_ref(o)->m_value));
return reinterpret_cast<atomic<object*> *>(&(lean_to_ref(o)->m_value));
}
/*
@ -276,13 +280,9 @@ static inline atomic<object*> * mt_ref_val_addr(object * o) {
object as we do for multi-threaded `IO.Ref`s. It makes sense since
the global `IO.Ref` may be used to communicate data between threads.
*/
static inline bool ref_maybe_mt(b_obj_arg ref) {
return
ref->m_mem_kind == static_cast<unsigned>(object_memory_kind::MTHeap) ||
ref->m_mem_kind == static_cast<unsigned>(object_memory_kind::Persistent);
}
static inline bool ref_maybe_mt(b_obj_arg ref) { return lean_is_mt(ref) || lean_is_persistent(ref); }
obj_res io_ref_get(b_obj_arg ref, obj_arg r) {
extern "C" obj_res lean_io_ref_get(b_obj_arg ref, obj_arg r) {
if (ref_maybe_mt(ref)) {
atomic<object *> * val_addr = mt_ref_val_addr(ref);
object * val = val_addr->exchange(nullptr);
@ -296,7 +296,7 @@ obj_res io_ref_get(b_obj_arg ref, obj_arg r) {
}
return set_io_result(r, val);
} else {
object * val = to_ref(ref)->m_value;
object * val = lean_to_ref(ref)->m_value;
if (val == nullptr)
return set_io_error(r, g_io_error_nullptr_read);
inc(val);
@ -306,7 +306,7 @@ obj_res io_ref_get(b_obj_arg ref, obj_arg r) {
static_assert(sizeof(atomic<unsigned short>) == sizeof(unsigned short), "`atomic<unsigned short>` and `unsigned short` must have the same size"); // NOLINT
obj_res io_ref_reset(b_obj_arg ref, obj_arg r) {
extern "C" obj_res lean_io_ref_reset(b_obj_arg ref, obj_arg r) {
if (ref_maybe_mt(ref)) {
atomic<object *> * val_addr = mt_ref_val_addr(ref);
object * old_a = val_addr->exchange(nullptr);
@ -314,14 +314,14 @@ obj_res io_ref_reset(b_obj_arg ref, obj_arg r) {
dec(old_a);
return r;
} else {
if (to_ref(ref)->m_value != nullptr)
dec(to_ref(ref)->m_value);
to_ref(ref)->m_value = nullptr;
if (lean_to_ref(ref)->m_value != nullptr)
dec(lean_to_ref(ref)->m_value);
lean_to_ref(ref)->m_value = nullptr;
return r;
}
}
obj_res io_ref_set(b_obj_arg ref, obj_arg a, obj_arg r) {
extern "C" obj_res lean_io_ref_set(b_obj_arg ref, obj_arg a, obj_arg r) {
if (ref_maybe_mt(ref)) {
/* We must mark `a` as multi-threaded if `ref` is marked as multi-threaded.
Reason: our runtime relies on the fact that a single-threaded object
@ -333,14 +333,14 @@ obj_res io_ref_set(b_obj_arg ref, obj_arg a, obj_arg r) {
dec(old_a);
return r;
} else {
if (to_ref(ref)->m_value != nullptr)
dec(to_ref(ref)->m_value);
to_ref(ref)->m_value = a;
if (lean_to_ref(ref)->m_value != nullptr)
dec(lean_to_ref(ref)->m_value);
lean_to_ref(ref)->m_value = a;
return r;
}
}
obj_res io_ref_swap(b_obj_arg ref, obj_arg a, obj_arg r) {
extern "C" obj_res lean_io_ref_swap(b_obj_arg ref, obj_arg a, obj_arg r) {
if (ref_maybe_mt(ref)) {
/* See io_ref_write */
mark_mt(a);
@ -350,10 +350,10 @@ obj_res io_ref_swap(b_obj_arg ref, obj_arg a, obj_arg r) {
return set_io_error(r, g_io_error_nullptr_read);
return set_io_result(r, old_a);
} else {
object * old_a = to_ref(ref)->m_value;
object * old_a = lean_to_ref(ref)->m_value;
if (old_a == nullptr)
return set_io_error(r, g_io_error_nullptr_read);
to_ref(ref)->m_value = a;
lean_to_ref(ref)->m_value = a;
return set_io_result(r, old_a);
}
}

79
src/runtime/lean.h
View file

@ -15,6 +15,9 @@ Author: Leonardo de Moura
#include <malloc.h>
#endif
#define LEAN_SMALL_ALLOCATOR
#define LEAN_COMPRESSED_OBJECT_HEADER
#ifdef __cplusplus
#include <atomic>
#define _Atomic(t) std::atomic<t>
@ -25,7 +28,9 @@ extern "C" {
#define LEAN_USING_STD
#endif
#define LEAN_CLOSURE_MAX_ARGS 16
#define LEAN_CLOSURE_MAX_ARGS 16
#define LEAN_OBJECT_SIZE_DELTA 8
#define LEAN_MAX_SMALL_OBJECT_SIZE 512
#ifdef _MSC_VER
#define LEAN_ALLOCA(s) _alloca(s)
@ -43,6 +48,12 @@ extern "C" {
#define LEAN_ALWAYS_INLINE
#endif
#ifdef LEAN_RUNTIME_STATS
#define LEAN_RUNTIME_STAT_CODE(c) c
#else
#define LEAN_RUNTIME_STAT_CODE(c)
#endif
#define LEAN_BYTE(Var, Index) *(((uint8_t*)&Var)+Index)
#define LeanMaxCtorTag 244
@ -218,8 +229,52 @@ static inline size_t lean_unbox(lean_object * o) { return (size_t)(o) >> 1; }
void lean_panic_out_of_memory();
void * lean_alloc_heap_object(size_t sz);
void lean_free_heap_obj(lean_object * o);
static inline size_t lean_align(size_t v, size_t a) {
return (v / a)*a + a * (v % a != 0);
}
static inline unsigned lean_get_slot_idx(unsigned sz) {
assert(sz > 0);
assert(lean_align(sz, LEAN_OBJECT_SIZE_DELTA) == sz);
return sz / LEAN_OBJECT_SIZE_DELTA - 1;
}
void * lean_alloc_small(unsigned sz, unsigned slot_idx);
void lean_free_small(void * p);
unsigned lean_small_mem_size(void * p);
static inline lean_object * lean_alloc_small_object(unsigned sz) {
#ifdef LEAN_SMALL_ALLOCATOR
sz = lean_align(sz, LEAN_OBJECT_SIZE_DELTA);
unsigned slot_idx = lean_get_slot_idx(sz);
assert(sz <= LEAN_MAX_SMALL_OBJECT_SIZE);
return (lean_object*)lean_alloc_small(sz, slot_idx);
#else
void * mem = malloc(sizeof(size_t) + sz);
if (mem == 0) lean_panic_out_of_memory();
*(size_t*)mem = sz;
return (lean_object*)((size_t*)mem + 1);
#endif
}
static inline unsigned lean_small_object_size(lean_object * o) {
#ifdef LEAN_SMALL_ALLOCATOR
return lean_small_mem_size(o);
#else
return *((size_t*)o - 1);
#endif
}
static inline void lean_free_small_object(lean_object * o) {
#ifdef LEAN_SMALL_ALLOCATOR
lean_free_small(o);
#else
free((size_t*)o - 1);
#endif
}
lean_object * lean_alloc_object(size_t sz);
void lean_free_object(lean_object * o);
/* The object size may be slightly bigger for constructor objects.
The runtime does not track the size of the scalar size area.
@ -260,7 +315,7 @@ static inline bool lean_is_persistent(lean_object * o) {
#endif
}
static inline bool lean_is_heap_obj(lean_object * o) {
static inline bool lean_is_heap_object(lean_object * o) {
return lean_is_st(o) || lean_is_mt(o);
}
@ -485,7 +540,7 @@ static inline uint8_t * lean_ctor_scalar_cptr(lean_object * o) {
static inline lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, unsigned scalar_sz) {
assert(tag <= LeanMaxCtorTag && num_objs < 256 && scalar_sz < 1024);
lean_object * o = (lean_object*)lean_alloc_heap_object(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz);
lean_object * o = lean_alloc_small_object(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz);
lean_set_st_header(o, tag, num_objs);
return o;
}
@ -575,7 +630,7 @@ static inline lean_object ** lean_closure_arg_cptr(lean_object * o) { return lea
static inline lean_obj_res lean_alloc_closure(void * fun, unsigned arity, unsigned num_fixed) {
assert(arity > 0);
assert(num_fixed < arity);
lean_closure_object * o = (lean_closure_object*)lean_alloc_heap_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
lean_closure_object * o = (lean_closure_object*)lean_alloc_small_object(sizeof(lean_closure_object) + sizeof(void*)*num_fixed);
lean_set_st_header((lean_object*)o, LeanClosure, 0);
o->m_fun = fun;
o->m_arity = arity;
@ -622,7 +677,7 @@ lean_obj_res lean_fixpoint6(lean_obj_arg rec, lean_obj_arg a1, lean_obj_arg a2,
/* Arrays of objects (low level API) */
static inline lean_obj_res lean_alloc_array(size_t size, size_t capacity) {
lean_array_object * o = (lean_array_object*)lean_alloc_heap_object(sizeof(lean_array_object) + sizeof(void*)*capacity);
lean_array_object * o = (lean_array_object*)lean_alloc_object(sizeof(lean_array_object) + sizeof(void*)*capacity);
lean_set_st_header((lean_object*)o, LeanArray, 0);
o->m_size = size;
o->m_capacity = capacity;
@ -771,7 +826,7 @@ lean_object * lean_mk_array(lean_obj_arg n, lean_obj_arg v);
/* Array of scalars */
static inline lean_obj_res lean_alloc_sarray(unsigned elem_size, size_t size, size_t capacity) {
lean_sarray_object * o = (lean_sarray_object*)lean_alloc_heap_object(sizeof(lean_sarray_object) + elem_size*capacity);
lean_sarray_object * o = (lean_sarray_object*)lean_alloc_object(sizeof(lean_sarray_object) + elem_size*capacity);
lean_set_st_header((lean_object*)o, LeanScalarArray, elem_size);
o->m_size = size;
o->m_capacity = capacity;
@ -847,7 +902,7 @@ static inline lean_obj_res lean_byte_array_set(lean_obj_arg a, b_lean_obj_arg i,
/* Strings */
static inline lean_obj_res lean_alloc_string(size_t size, size_t capacity, size_t len) {
lean_string_object * o = (lean_string_object*)lean_alloc_heap_object(sizeof(lean_string_object) + capacity);
lean_string_object * o = (lean_string_object*)lean_alloc_object(sizeof(lean_string_object) + capacity);
lean_set_st_header((lean_object*)o, LeanString, 0);
o->m_size = size;
o->m_capacity = capacity;
@ -892,7 +947,7 @@ size_t lean_string_hash(b_lean_obj_arg);
/* Thunks */
static inline lean_obj_res lean_mk_thunk(lean_obj_arg c) {
lean_thunk_object * o = (lean_thunk_object*)lean_alloc_heap_object(sizeof(lean_thunk_object));
lean_thunk_object * o = (lean_thunk_object*)lean_alloc_small_object(sizeof(lean_thunk_object));
lean_set_st_header((lean_object*)o, LeanThunk, 0);
o->m_value = (lean_object*)0;
o->m_closure = c;
@ -901,7 +956,7 @@ static inline lean_obj_res lean_mk_thunk(lean_obj_arg c) {
/* Thunk.pure : A -> Thunk A */
static inline lean_obj_res lean_thunk_pure(lean_obj_arg v) {
lean_thunk_object * o = (lean_thunk_object*)lean_alloc_heap_object(sizeof(lean_thunk_object));
lean_thunk_object * o = (lean_thunk_object*)lean_alloc_small_object(sizeof(lean_thunk_object));
lean_set_st_header((lean_object*)o, LeanThunk, 0);
o->m_value = v;
o->m_closure = (lean_object*)0;
@ -957,7 +1012,7 @@ b_lean_obj_res lean_io_wait_any_core(b_lean_obj_arg task_list);
/* External objects */
static inline lean_object * lean_alloc_external(lean_external_class * cls, void * data) {
lean_external_object * o = (lean_external_object*)lean_alloc_heap_object(sizeof(lean_external_object));
lean_external_object * o = (lean_external_object*)lean_alloc_small_object(sizeof(lean_external_object));
lean_set_st_header((lean_object*)o, LeanExternal, 0);
o->m_class = cls;
o->m_data = data;

1
src/runtime/mpq.h
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#pragma once
#include "runtime/mpz.h"
#include "runtime/serializer.h"
namespace lean {
/**

8
src/runtime/mpz.h
View file

@ -10,9 +10,12 @@ Author: Leonardo de Moura
#include <string>
#include <iostream>
#include <limits>
#include "runtime/int64.h"
#include "runtime/debug.h"
#include "runtime/serializer.h"
#include "runtime/lean.h"
namespace lean {
class mpq;
/** \brief Wrapper for GMP integers */
class mpz {
@ -275,7 +278,4 @@ public:
struct mpz_cmp_fn {
int operator()(mpz const & v1, mpz const & v2) const { return cmp(v1, v2); }
};
inline serializer & operator<<(serializer & s, mpz const & n) { s.write_mpz(n); return s; }
inline deserializer & operator>>(deserializer & d, mpz & n) { n = d.read_mpz(); return d; }
}

714
src/runtime/object.cpp
View file

@ -4,251 +4,169 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <limits>
#include <iostream>
#include <string>
#include <algorithm>
#include <map>
#include <vector>
#include <utility>
#include <unordered_set>
#include <deque>
#include "runtime/stackinfo.h"
#include "runtime/object.h"
#include "runtime/utf8.h"
#include "runtime/apply.h"
#include "runtime/flet.h"
#include "runtime/interrupt.h"
#include "runtime/hash.h"
#include "runtime/thread.h"
#include "runtime/alloc.h"
#include "runtime/debug.h"
#include "util/buffer.h" // move to runtime
#define LEAN_MAX_PRIO 8
namespace lean {
// =======================================
// External objects
struct external_object_class {
external_object_finalize_proc m_finalize;
external_object_foreach_proc m_foreach;
};
static std::vector<external_object_class*> * g_ext_classes;
static mutex * g_ext_classes_mutex;
external_object_class * register_external_object_class(external_object_finalize_proc p1, external_object_foreach_proc p2) {
unique_lock<mutex> lock(*g_ext_classes_mutex);
external_object_class * cls = new external_object_class{p1, p2};
g_ext_classes->push_back(cls);
return cls;
extern "C" void lean_panic_out_of_memory() {
std::cerr << "out of memory\n";
std::exit(1);
}
// =======================================
// Object
size_t obj_byte_size(object * o) {
switch (get_kind(o)) {
case object_kind::Constructor: return cnstr_byte_size(o);
case object_kind::Closure: return closure_byte_size(o);
case object_kind::Array: return array_byte_size(o);
case object_kind::ScalarArray: return sarray_byte_size(o);
case object_kind::String: return string_byte_size(o);
case object_kind::MPZ: return sizeof(mpz_object);
case object_kind::Thunk: return sizeof(thunk_object);
case object_kind::Task: return sizeof(task_object);
case object_kind::Ref: return sizeof(ref_object);
case object_kind::External: lean_unreachable();
extern "C" size_t lean_object_byte_size(lean_object * o) {
switch (lean_ptr_tag(o)) {
case LeanArray: return lean_array_byte_size(o);
case LeanScalarArray: return lean_sarray_byte_size(o);
case LeanString: return lean_string_byte_size(o);
default: return lean_small_object_size(o);
}
lean_unreachable();
}
size_t obj_header_size(object * o) {
switch (get_kind(o)) {
case object_kind::Constructor: return sizeof(constructor_object);
case object_kind::Closure: return sizeof(closure_object);
case object_kind::Array: return sizeof(array_object);
case object_kind::ScalarArray: return sizeof(sarray_object);
case object_kind::String: return sizeof(string_object);
case object_kind::MPZ: return sizeof(mpz_object);
case object_kind::Thunk: return sizeof(thunk_object);
case object_kind::Task: return sizeof(task_object);
case object_kind::Ref: return sizeof(ref_object);
case object_kind::External: lean_unreachable();
}
lean_unreachable();
static inline lean_object * get_next(lean_object * o) {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
size_t header = o->m_header;
LEAN_BYTE(header, 6) = 0;
LEAN_BYTE(header, 7) = 0;
return (lean_object*)(header);
#else
return (lean_object*)(o->m_rc);
#endif
}
/* We use the RC memory to implement a linked list of lean objects to be deleted.
This hack is safe because rc_type is uintptr_t. */
static inline void set_next(lean_object * o, lean_object * n) {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
size_t new_header = (size_t)n;
LEAN_BYTE(new_header, 6) = LEAN_BYTE(o->m_header, 6);
LEAN_BYTE(new_header, 7) = LEAN_BYTE(o->m_header, 7);
o->m_header = new_header;
#else
*(lean_object*)(o->m_rc) = n;
#endif
}
static_assert(sizeof(atomic<rc_type>) == sizeof(object*), "unexpected atomic<rc_type> size, the object GC assumes these two types have the same size"); // NOLINT
static inline void push_back(lean_object * & todo, lean_object * v) {
set_next(v, todo);
todo = v;
}
static inline lean_object * pop_back(lean_object * & todo) {
lean_object * r = todo;
todo = get_next(todo);
return r;
}
static inline void dec_ref(lean_object * o, lean_object* & todo) {
if (lean_dec_ref_core(o))
push_back(todo, o);
}
static inline void dec(lean_object * o, lean_object* & todo) {
if (!lean_is_scalar(o) && lean_dec_ref_core(o))
push_back(todo, o);
}
#ifdef LEAN_LAZY_RC
LEAN_THREAD_PTR(object, g_to_free);
#endif
inline object * get_next(object * o) {
return *reinterpret_cast<object**>(st_rc_addr(o));
}
inline void set_next(object * o, object * n) {
*reinterpret_cast<object**>(st_rc_addr(o)) = n;
}
inline void push_back(object * & todo, object * v) {
set_next(v, todo);
todo = v;
}
inline object * pop_back(object * & todo) {
object * r = todo;
todo = get_next(todo);
return r;
}
inline void dec_ref(object * o, object* & todo) {
if (dec_ref_core(o))
push_back(todo, o);
}
inline void dec(object * o, object* & todo) {
if (!is_scalar(o) && dec_ref_core(o))
push_back(todo, o);
}
void deactivate_task(task_object * t);
static void lean_del_core(object * o, object * & todo);
extern "C" lean_object * lean_alloc_object(size_t sz) {
#ifdef LEAN_LAZY_RC
if (g_to_free) {
object * o = pop_back(g_to_free);
lean_del_core(o, g_to_free);
}
#endif
#ifdef LEAN_SMALL_ALLOCATOR
static inline void free_heap_obj_core(object * o, size_t sz) {
return (lean_object*)alloc(sz);
#else
static inline void free_heap_obj_core(object * o) {
#endif
#ifdef LEAN_FAKE_FREE
// Set kinds to invalid values, which should trap any further accesses in debug mode.
lean_always_assert(o->m_kind != 42);
o->m_kind = 42;
o->m_mem_kind = 42;
#else
#ifdef LEAN_SMALL_ALLOCATOR
dealloc(reinterpret_cast<char *>(o) - sizeof(rc_type), sz);
#else
free(reinterpret_cast<char *>(o) - sizeof(rc_type));
#endif
void * r = malloc(sz);
if (r == nullptr) lean_panic_out_of_memory();
return (lean_object*)r;
#endif
}
#ifdef LEAN_SMALL_ALLOCATOR
#define FREE_OBJ(o, sz) free_heap_obj_core(o, sz)
static void deactivate_task(lean_task_object * t);
static inline void lean_set_tag(b_lean_obj_arg o, uint8_t new_tag) {
assert(new_tag <= LeanMaxCtorTag);
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
LEAN_BYTE(o->m_header, 7) = new_tag;
#else
#define FREE_OBJ(o, sz) free_heap_obj_core(o)
o->m_tag = new_tag;
#endif
void free_heap_obj(object * o) {
FREE_OBJ(o, obj_byte_size(o) + sizeof(rc_type));
}
static inline void free_cnstr_obj(object * o) {
FREE_OBJ(o, cnstr_byte_size(o) + sizeof(rc_type));
}
static inline void free_closure_obj_core(object * o) {
FREE_OBJ(o, closure_byte_size(o) + sizeof(rc_type));
}
void free_closure_obj(object * o) {
return free_closure_obj_core(o);
}
static inline void free_array_obj(object * o) {
FREE_OBJ(o, array_byte_size(o) + sizeof(rc_type));
}
static inline void free_sarray_obj(object * o) {
FREE_OBJ(o, sarray_byte_size(o) + sizeof(rc_type));
}
static inline void free_string_obj(object * o) {
FREE_OBJ(o, string_byte_size(o) + sizeof(rc_type));
}
inline void free_mpz_obj(object * o) {
FREE_OBJ(o, sizeof(mpz_object) + sizeof(rc_type));
}
static inline void free_thunk_obj(object * o) {
FREE_OBJ(o, sizeof(thunk_object) + sizeof(rc_type));
}
static inline void free_ref_obj(object * o) {
FREE_OBJ(o, sizeof(ref_object) + sizeof(rc_type));
}
static inline void free_task_obj(object * o) {
FREE_OBJ(o, sizeof(task_object) + sizeof(rc_type));
}
static inline void free_external_obj(object * o) {
FREE_OBJ(o, sizeof(external_object) + sizeof(rc_type));
}
static void del_core(object * o, object * & todo) {
lean_assert(is_heap_obj(o));
LEAN_RUNTIME_STAT_CODE(g_num_del++);
switch (get_kind(o)) {
case object_kind::Constructor: {
object ** it = cnstr_obj_cptr(o);
object ** end = it + cnstr_num_objs(o);
static void lean_del_core(object * o, object * & todo) {
lean_assert(lean_is_heap_object(o));
uint8 tag = lean_ptr_tag(o);
if (tag <= LeanMaxCtorTag) {
object ** it = lean_ctor_obj_cptr(o);
object ** end = it + lean_ctor_num_objs(o);
for (; it != end; ++it) dec(*it, todo);
free_cnstr_obj(o);
break;
lean_free_small(o);
return;
}
case object_kind::Closure: {
object ** it = closure_arg_cptr(o);
object ** end = it + closure_num_fixed(o);
switch (tag) {
case LeanClosure: {
object ** it = lean_closure_arg_cptr(o);
object ** end = it + lean_closure_num_fixed(o);
for (; it != end; ++it) dec(*it, todo);
free_closure_obj_core(o);
lean_free_small(o);
break;
}
case object_kind::Array: {
object ** it = array_cptr(o);
object ** end = it + array_size(o);
case LeanArray: {
object ** it = lean_array_cptr(o);
object ** end = it + lean_array_size(o);
for (; it != end; ++it) dec(*it, todo);
free_array_obj(o);
dealloc(o, lean_array_byte_size(o));
break;
}
case object_kind::ScalarArray:
free_sarray_obj(o); break;
case object_kind::String:
free_string_obj(o); break;
case object_kind::MPZ:
dealloc_mpz(o); break;
case object_kind::Thunk:
if (object * c = to_thunk(o)->m_closure) dec(c, todo);
if (object * v = to_thunk(o)->m_value) dec(v, todo);
free_thunk_obj(o);
case LeanScalarArray:
dealloc(o, lean_sarray_byte_size(o));
break;
case object_kind::Ref:
if (object * v = to_ref(o)->m_value) dec(v, todo);
free_ref_obj(o);
case LeanString:
dealloc(o, lean_string_byte_size(o));
break;
case object_kind::Task:
deactivate_task(to_task(o));
case LeanMPZ:
to_mpz(o)->m_value.~mpz();
lean_free_small(o);
break;
case object_kind::External:
to_external(o)->m_class->m_finalize(to_external(o)->m_data);
free_external_obj(o);
case LeanThunk:
if (object * c = lean_to_thunk(o)->m_closure) dec(c, todo);
if (object * v = lean_to_thunk(o)->m_value) dec(v, todo);
lean_free_small(o);
break;
case LeanRef:
if (object * v = lean_to_ref(o)->m_value) dec(v, todo);
lean_free_small(o);
break;
case LeanTask:
deactivate_task(lean_to_task(o));
break;
case LeanExternal:
lean_to_external(o)->m_class->m_finalize(lean_to_external(o)->m_data);
lean_free_small(o);
break;
default:
lean_unreachable();
}
}
void del(object * o) {
extern "C" void lean_del(object * o) {
#ifdef LEAN_LAZY_RC
push_back(g_to_free, o);
#else
object * todo = nullptr;
while (true) {
lean_assert(is_heap_obj(o));
del_core(o, todo);
lean_assert(lean_is_heap_object(o));
lean_del_core(o, todo);
if (todo == nullptr)
return;
o = pop_back(todo);
@ -256,23 +174,6 @@ void del(object * o) {
#endif
}
void * alloc_heap_object(size_t sz) {
#ifdef LEAN_LAZY_RC
if (g_to_free) {
object * o = pop_back(g_to_free);
del_core(o, g_to_free);
}
#endif
#ifdef LEAN_SMALL_ALLOCATOR
void * r = alloc(sizeof(rc_type) + sz);
#else
void * r = malloc(sizeof(rc_type) + sz);
if (r == nullptr) throw std::bad_alloc();
#endif
*static_cast<rc_type *>(r) = 1;
return static_cast<char *>(r) + sizeof(rc_type);
}
// =======================================
// Arrays
static object * g_array_empty = nullptr;
@ -281,6 +182,7 @@ object * array_mk_empty() {
return g_array_empty;
}
// =======================================
// Closures
@ -288,15 +190,15 @@ typedef object * (*lean_cfun2)(object *, object *); // NOLINT
typedef object * (*lean_cfun3)(object *, object *, object *); // NOLINT
static obj_res mk_closure_2_1(lean_cfun2 fn, obj_arg a) {
object * c = alloc_closure(fn, 1);
closure_set(c, 0, a);
object * c = lean_alloc_closure((void*)fn, 2, 1);
lean_closure_set(c, 0, a);
return c;
}
static obj_res mk_closure_3_2(lean_cfun3 fn, obj_arg a1, obj_arg a2) {
object * c = alloc_closure(fn, 2);
closure_set(c, 0, a1);
closure_set(c, 1, a2);
object * c = lean_alloc_closure((void*)fn, 3, 2);
lean_closure_set(c, 0, a1);
lean_closure_set(c, 1, a2);
return c;
}
@ -304,11 +206,11 @@ static obj_res mk_closure_3_2(lean_cfun3 fn, obj_arg a1, obj_arg a2) {
// Thunks
static obj_res mk_thunk_3_2(lean_cfun3 fn, obj_arg a1, obj_arg a2) {
return mk_thunk(mk_closure_3_2(fn, a1, a2));
return lean_mk_thunk(mk_closure_3_2(fn, a1, a2));
}
b_obj_res thunk_get_core(b_obj_arg t) {
object * c = to_thunk(t)->m_closure.exchange(nullptr);
extern "C" b_obj_res lean_thunk_get_core(b_obj_arg t) {
object * c = lean_to_thunk(t)->m_closure.exchange(nullptr);
if (c != nullptr) {
/* Recall that a closure uses the standard calling convention.
`thunk_get` "consumes" the result `r` by storing it at `to_thunk(t)->m_value`.
@ -317,48 +219,225 @@ b_obj_res thunk_get_core(b_obj_arg t) {
to be object stored in the constructor object.
Recall that `apply_1` also consumes `c`'s RC. */
object * r = apply_1(c, box(0));
object * r = lean_apply_1(c, lean_box(0));
lean_assert(r != nullptr); /* Closure must return a valid lean object */
lean_assert(to_thunk(t)->m_value == nullptr);
to_thunk(t)->m_value = r;
lean_assert(lean_to_thunk(t)->m_value == nullptr);
lean_to_thunk(t)->m_value = r;
return r;
} else {
lean_assert(c == nullptr);
/* There is another thread executing the closure. We keep waiting for the m_value to be
set by another thread. */
while (!to_thunk(t)->m_value) {
while (!lean_to_thunk(t)->m_value) {
this_thread::yield();
}
return to_thunk(t)->m_value;
return lean_to_thunk(t)->m_value;
}
}
static obj_res thunk_map_fn_closure(obj_arg f, obj_arg t, obj_arg /* u */) {
b_obj_res v = thunk_get(t);
inc(v);
obj_res r = apply_1(f, v);
dec(v);
b_obj_res v = lean_thunk_get(t);
lean_inc(v);
obj_res r = lean_apply_1(f, v);
lean_dec(v);
return r;
}
obj_res thunk_map(obj_arg f, obj_arg t) {
lean_assert(is_closure(f));
lean_assert(is_thunk(t));
extern "C" obj_res lean_thunk_map(obj_arg f, obj_arg t) {
lean_assert(lean_is_closure(f));
lean_assert(lean_is_thunk(t));
return mk_thunk_3_2(thunk_map_fn_closure, f, t);
}
static obj_res thunk_bind_fn_closure(obj_arg x, obj_arg f, obj_arg /* u */) {
b_obj_res v = thunk_get(x);
inc(v);
obj_res r = apply_1(f, v);
dec(x);
b_obj_res v = lean_thunk_get(x);
lean_inc(v);
obj_res r = lean_apply_1(f, v);
lean_dec(x);
return r;
}
obj_res thunk_bind(obj_arg x, obj_arg f) {
extern "C" obj_res lean_thunk_bind(obj_arg x, obj_arg f) {
return mk_thunk_3_2(thunk_bind_fn_closure, x, f);
}
// =======================================
// Fixpoint
static inline object * ptr_to_weak_ptr(object * p) {
return reinterpret_cast<object*>(reinterpret_cast<uintptr_t>(p) | 1);
}
static inline object * weak_ptr_to_ptr(object * w) {
return reinterpret_cast<object*>((reinterpret_cast<uintptr_t>(w) >> 1) << 1);
}
obj_res fixpoint_aux(obj_arg rec, obj_arg weak_k, obj_arg a) {
object * k = weak_ptr_to_ptr(weak_k);
lean_inc(k);
return lean_apply_2(rec, k, a);
}
extern "C" obj_res lean_fixpoint(obj_arg rec, obj_arg a) {
object * k = lean_alloc_closure((void*)fixpoint_aux, 3, 2);
lean_inc(rec);
lean_closure_set(k, 0, rec);
lean_closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = lean_apply_2(rec, k, a);
return r;
}
obj_res fixpoint_aux2(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2) {
object * k = weak_ptr_to_ptr(weak_k);
lean_inc(k);
return lean_apply_3(rec, k, a1, a2);
}
extern "C" obj_res lean_fixpoint2(obj_arg rec, obj_arg a1, obj_arg a2) {
object * k = lean_alloc_closure((void*)fixpoint_aux2, 4, 2);
lean_inc(rec);
lean_closure_set(k, 0, rec);
lean_closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = lean_apply_3(rec, k, a1, a2);
return r;
}
obj_res fixpoint_aux3(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3) {
object * k = weak_ptr_to_ptr(weak_k);
lean_inc(k);
return lean_apply_4(rec, k, a1, a2, a3);
}
extern "C" obj_res lean_fixpoint3(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3) {
object * k = lean_alloc_closure((void*)fixpoint_aux3, 5, 2);
lean_inc(rec);
lean_closure_set(k, 0, rec);
lean_closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = lean_apply_4(rec, k, a1, a2, a3);
return r;
}
obj_res fixpoint_aux4(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4) {
object * k = weak_ptr_to_ptr(weak_k);
lean_inc(k);
return lean_apply_5(rec, k, a1, a2, a3, a4);
}
extern "C" obj_res lean_fixpoint4(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4) {
object * k = lean_alloc_closure((void*)fixpoint_aux4, 6, 2);
lean_inc(rec);
lean_closure_set(k, 0, rec);
lean_closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = lean_apply_5(rec, k, a1, a2, a3, a4);
return r;
}
obj_res fixpoint_aux5(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5) {
object * k = weak_ptr_to_ptr(weak_k);
lean_inc(k);
return lean_apply_6(rec, k, a1, a2, a3, a4, a5);
}
extern "C" obj_res lean_fixpoint5(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5) {
object * k = lean_alloc_closure((void*)fixpoint_aux5, 7, 2);
lean_inc(rec);
lean_closure_set(k, 0, rec);
lean_closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = lean_apply_6(rec, k, a1, a2, a3, a4, a5);
return r;
}
obj_res fixpoint_aux6(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6) {
object * k = weak_ptr_to_ptr(weak_k);
lean_inc(k);
return lean_apply_7(rec, k, a1, a2, a3, a4, a5, a6);
}
extern "C" obj_res lean_fixpoint6(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6) {
object * k = lean_alloc_closure((void*)fixpoint_aux6, 8, 2);
lean_inc(rec);
lean_closure_set(k, 0, rec);
lean_closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = lean_apply_7(rec, k, a1, a2, a3, a4, a5, a6);
return r;
}
// =======================================
// Mark Persistent
extern "C" void lean_mark_persistent(object * o);
static obj_res mark_persistent_fn(obj_arg o) {
lean_mark_persistent(o);
return box(0);
}
extern "C" void lean_mark_persistent(object * o) {
buffer<object*> todo;
todo.push_back(o);
while (!todo.empty()) {
object * o = todo.back();
todo.pop_back();
if (!lean_is_scalar(o) && lean_is_heap_object(o)) {
#ifdef LEAN_COMPRESSED_OBJECT_HEADER
o->m_header &= ~((1ull << LEAN_ST_BIT) | (1ull << LEAN_MT_BIT));
o->m_header |= (1ull << LEAN_PERSISTENT_BIT);
#else
o->m_mem_kind = LEAN_PERSISTENT_MEM_KIND;
#endif
switch (lean_ptr_tag(o)) {
case LeanScalarArray:
case LeanString:
case LeanMPZ:
break;
case LeanExternal: {
object * fn = lean_alloc_closure(reinterpret_cast<void*>(mark_persistent_fn), 1, 0);
lean_to_external(o)->m_class->m_foreach(lean_to_external(o)->m_data, fn);
lean_dec(fn);
break;
}
case LeanTask:
todo.push_back(lean_task_get(o));
break;
case LeanClosure: {
object ** it = lean_closure_arg_cptr(o);
object ** end = it + lean_closure_num_fixed(o);
for (; it != end; ++it) todo.push_back(*it);
break;
}
case LeanArray: {
object ** it = lean_array_cptr(o);
object ** end = it + lean_array_size(o);
for (; it != end; ++it) todo.push_back(*it);
break;
}
case LeanThunk:
if (object * c = lean_to_thunk(o)->m_closure) todo.push_back(c);
if (object * v = lean_to_thunk(o)->m_value) todo.push_back(v);
break;
case LeanRef:
if (object * v = lean_to_ref(o)->m_value) todo.push_back(v);
break;
case LeanReserved:
lean_unreachable();
break;
default: {
object ** it = lean_ctor_obj_cptr(o);
object ** end = it + lean_ctor_num_objs(o);
for (; it != end; ++it) todo.push_back(*it);
break;
}}
}
}
}
}
#if 0
namespace lean {
// =======================================
// Tasks
@ -841,64 +920,6 @@ b_obj_res io_wait_any_core(b_obj_arg task_list) {
return g_task_manager->wait_any(task_list);
}
void mark_persistent(object * o);
static obj_res mark_persistent_fn(obj_arg o) {
mark_persistent(o);
return box(0);
}
void mark_persistent(object * o) {
buffer<object*> todo;
todo.push_back(o);
while (!todo.empty()) {
object * o = todo.back();
todo.pop_back();
if (!is_scalar(o) && is_heap_obj(o)) {
o->m_mem_kind = static_cast<unsigned>(object_memory_kind::Persistent);
switch (get_kind(o)) {
case object_kind::ScalarArray:
case object_kind::String:
case object_kind::MPZ:
break;
case object_kind::External: {
object * fn = alloc_closure(reinterpret_cast<void*>(mark_persistent_fn), 1, 0);
to_external(o)->m_class->m_foreach(to_external(o)->m_data, fn);
dec(fn);
break;
}
case object_kind::Task:
todo.push_back(task_get(o));
break;
case object_kind::Constructor: {
object ** it = cnstr_obj_cptr(o);
object ** end = it + cnstr_num_objs(o);
for (; it != end; ++it) todo.push_back(*it);
break;
}
case object_kind::Closure: {
object ** it = closure_arg_cptr(o);
object ** end = it + closure_num_fixed(o);
for (; it != end; ++it) todo.push_back(*it);
break;
}
case object_kind::Array: {
object ** it = array_cptr(o);
object ** end = it + array_size(o);
for (; it != end; ++it) todo.push_back(*it);
break;
}
case object_kind::Thunk:
if (object * c = to_thunk(o)->m_closure) todo.push_back(c);
if (object * v = to_thunk(o)->m_value) todo.push_back(v);
break;
case object_kind::Ref:
if (object * v = to_ref(o)->m_value) todo.push_back(v);
break;
}
}
}
}
// =======================================
// Natural numbers
@ -1605,106 +1626,6 @@ object * array_push(obj_arg a, obj_arg v) {
return r;
}
// =======================================
// fixpoint
static inline object * ptr_to_weak_ptr(object * p) {
return reinterpret_cast<object*>(reinterpret_cast<uintptr_t>(p) | 1);
}
static inline object * weak_ptr_to_ptr(object * w) {
return reinterpret_cast<object*>((reinterpret_cast<uintptr_t>(w) >> 1) << 1);
}
obj_res fixpoint_aux(obj_arg rec, obj_arg weak_k, obj_arg a) {
object * k = weak_ptr_to_ptr(weak_k);
inc(k);
return apply_2(rec, k, a);
}
obj_res fixpoint(obj_arg rec, obj_arg a) {
object * k = alloc_closure(fixpoint_aux, 2);
inc(rec);
closure_set(k, 0, rec);
closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = apply_2(rec, k, a);
return r;
}
obj_res fixpoint_aux2(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2) {
object * k = weak_ptr_to_ptr(weak_k);
inc(k);
return apply_3(rec, k, a1, a2);
}
obj_res fixpoint2(obj_arg rec, obj_arg a1, obj_arg a2) {
object * k = alloc_closure(fixpoint_aux2, 2);
inc(rec);
closure_set(k, 0, rec);
closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = apply_3(rec, k, a1, a2);
return r;
}
obj_res fixpoint_aux3(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3) {
object * k = weak_ptr_to_ptr(weak_k);
inc(k);
return apply_4(rec, k, a1, a2, a3);
}
obj_res fixpoint3(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3) {
object * k = alloc_closure(fixpoint_aux3, 2);
inc(rec);
closure_set(k, 0, rec);
closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = apply_4(rec, k, a1, a2, a3);
return r;
}
obj_res fixpoint_aux4(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4) {
object * k = weak_ptr_to_ptr(weak_k);
inc(k);
return apply_5(rec, k, a1, a2, a3, a4);
}
obj_res fixpoint4(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4) {
object * k = alloc_closure(fixpoint_aux4, 2);
inc(rec);
closure_set(k, 0, rec);
closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = apply_5(rec, k, a1, a2, a3, a4);
return r;
}
obj_res fixpoint_aux5(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5) {
object * k = weak_ptr_to_ptr(weak_k);
inc(k);
return apply_6(rec, k, a1, a2, a3, a4, a5);
}
obj_res fixpoint5(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5) {
object * k = alloc_closure(fixpoint_aux5, 2);
inc(rec);
closure_set(k, 0, rec);
closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = apply_6(rec, k, a1, a2, a3, a4, a5);
return r;
}
obj_res fixpoint_aux6(obj_arg rec, obj_arg weak_k, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6) {
object * k = weak_ptr_to_ptr(weak_k);
inc(k);
return apply_7(rec, k, a1, a2, a3, a4, a5, a6);
}
obj_res fixpoint6(obj_arg rec, obj_arg a1, obj_arg a2, obj_arg a3, obj_arg a4, obj_arg a5, obj_arg a6) {
object * k = alloc_closure(fixpoint_aux6, 2);
inc(rec);
closure_set(k, 0, rec);
closure_set(k, 1, ptr_to_weak_ptr(k));
object * r = apply_7(rec, k, a1, a2, a3, a4, a5, a6);
return r;
}
// =======================================
// Runtime info
@ -1812,3 +1733,4 @@ void finalize_object() {
extern "C" void lean_dbg_print_str(lean::object* o) { lean::dbg_print_str(o); }
extern "C" void lean_dbg_print_num(lean::object* o) { lean::dbg_print_num(o); }
#endif

1695
src/runtime/object.h
View file

File diff suppressed because it is too large Load diff

1
src/runtime/optional.h
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "runtime/lean.h"
#include "runtime/debug.h"
namespace lean {

69
src/runtime/serializer.cpp
View file

@ -75,7 +75,10 @@ void serializer::write_blob(std::string const & s) {
void serializer::write_constructor(object * o) {
lean_assert(is_cnstr(o));
unsigned num_objs = cnstr_num_objs(o);
unsigned scalar_sz = cnstr_scalar_size(o);
unsigned obj_size = lean_object_byte_size(o);
unsigned main_size = sizeof(lean_ctor_object) + sizeof(lean_object*)*num_objs;
lean_assert(obj_size >= main_size);
unsigned scalar_sz = obj_size - main_size;
write_unsigned_short(cnstr_tag(o));
write_unsigned_short(num_objs);
write_unsigned_short(scalar_sz);
@ -127,8 +130,8 @@ void serializer::write_scalar_array(object * o) {
write_unsigned(esz);
write_size_t(sz);
size_t num_bytes = sz*esz;
unsigned char const * it = sarray_cptr_core<unsigned char>(o);
unsigned char const * end = it + num_bytes;
uint8 const * it = sarray_cptr(o);
uint8 const * end = it + num_bytes;
for (; it != end; ++it)
m_out.put(*it);
}
@ -167,19 +170,19 @@ void serializer::write_object(object * o) {
m_out.put(1);
write_unsigned(it->second);
} else {
object_kind k = get_kind(o);
uint8 k = lean_ptr_tag(o);
m_out.put(static_cast<unsigned>(k) + 2);
switch (k) {
case object_kind::Constructor: write_constructor(o); break;
case object_kind::Closure: write_closure(o); break;
case object_kind::Task: write_task(o); break;
case object_kind::Thunk: write_thunk(o); break;
case object_kind::Array: write_array(o); break;
case object_kind::ScalarArray: write_scalar_array(o); break;
case object_kind::String: write_string_object(o); break;
case object_kind::MPZ: write_mpz(mpz_value(o)); break;
case object_kind::External: write_external(o); break;
default: lean_unreachable();
case LeanClosure: write_closure(o); break;
case LeanTask: write_task(o); break;
case LeanThunk: write_thunk(o); break;
case LeanArray: write_array(o); break;
case LeanScalarArray: write_scalar_array(o); break;
case LeanString: write_string_object(o); break;
case LeanMPZ: write_mpz(mpz_value(o)); break;
case LeanExternal: write_external(o); break;
case LeanReserved: lean_unreachable(); break;
default: write_constructor(o); break;
}
inc_ref(o);
m_obj_table.insert(std::make_pair(o, m_obj_table.size()));
@ -320,11 +323,11 @@ object * deserializer::read_array() {
}
object * deserializer::read_scalar_array() {
unsigned esz = read_unsigned();
size_t sz = read_size_t();
object * r = alloc_sarray(esz, sz, sz);
unsigned char * it = sarray_cptr_core<unsigned char>(r);
unsigned char * end = it + sz*esz;
unsigned esz = read_unsigned();
size_t sz = read_size_t();
object * r = alloc_sarray(esz, sz, sz);
uint8 * it = sarray_cptr(r);
uint8 * end = it + sz*esz;
for (; it != end; ++it)
*it = m_in.get();
return r;
@ -355,19 +358,23 @@ object * deserializer::read_object() {
throw corrupted_stream_exception();
return m_objs[i];
} else {
object_kind k = static_cast<object_kind>(c - 2);
object * r;
switch (k) {
case object_kind::Constructor: r = read_constructor(); break;
case object_kind::Closure: r = read_closure(); break;
case object_kind::Thunk: r = read_thunk(); break;
case object_kind::Task: r = read_task(); break;
case object_kind::Array: r = read_array(); break;
case object_kind::ScalarArray: r = read_scalar_array(); break;
case object_kind::String: r = read_string_object(); break;
case object_kind::MPZ: r = alloc_mpz(read_mpz()); break;
case object_kind::External: r = read_external(); break;
default: throw corrupted_stream_exception();
switch (c - 2) {
case LeanClosure: r = read_closure(); break;
case LeanThunk: r = read_thunk(); break;
case LeanTask: r = read_task(); break;
case LeanArray: r = read_array(); break;
case LeanScalarArray: r = read_scalar_array(); break;
case LeanString: r = read_string_object(); break;
case LeanMPZ: r = alloc_mpz(read_mpz()); break;
case LeanExternal: r = read_external(); break;
case LeanReserved: throw corrupted_stream_exception();
default:
if (c - 2 < LeanMaxCtorTag)
r = read_constructor();
else
throw corrupted_stream_exception();
break;
}
m_objs.push_back(r);
return r;

7
src/runtime/serializer.h
View file

@ -12,12 +12,10 @@ Author: Leonardo de Moura
#include <functional>
#include <unordered_map>
#include <cstring>
#include "runtime/int64.h"
#include "runtime/object.h"
#include "runtime/optional.h"
namespace lean {
struct object;
class mpz;
class serializer {
std::ostream & m_out;
std::unordered_map<object*, unsigned, std::hash<object*>, std::equal_to<object*>> m_obj_table;
@ -138,4 +136,7 @@ deserializer & operator>>(deserializer & d, optional<T> & a) {
a = read_optional<T>(d);
return d;
}
inline serializer & operator<<(serializer & s, mpz const & n) { s.write_mpz(n); return s; }
inline deserializer & operator>>(deserializer & d, mpz & n) { n = d.read_mpz(); return d; }
}

49
src/tests/util/CMakeLists.txt
View file

@ -4,48 +4,7 @@ add_exec_test(object "object")
add_executable(compact compact.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(compact ${EXTRA_LIBS})
add_exec_test(compact "compact")
add_executable(name name.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(name ${EXTRA_LIBS})
add_exec_test(name "name")
add_executable(nat nat.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(nat ${EXTRA_LIBS})
add_exec_test(nat "nat")
add_executable(buffer buffer.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(buffer ${EXTRA_LIBS})
add_exec_test(buffer "buffer")
add_executable(list list.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(list ${EXTRA_LIBS})
add_exec_test(list "list")
add_executable(rb_tree rb_tree.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(rb_tree ${EXTRA_LIBS})
add_exec_test(rb_tree "rb_tree")
add_executable(rb_map rb_map.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(rb_map ${EXTRA_LIBS})
add_exec_test(rb_map "rb_map")
add_executable(bit_tricks bit_tricks.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(bit_tricks ${EXTRA_LIBS})
add_exec_test(bit_tricks "bit_tricks")
add_executable(hash hash.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(hash ${EXTRA_LIBS})
add_exec_test(hash "hash")
add_executable(set set.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(set ${EXTRA_LIBS})
add_exec_test(set "set")
add_executable(optional optional.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(optional ${EXTRA_LIBS})
add_exec_test(optional "optional")
add_executable(stackinfo stackinfo.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(stackinfo ${EXTRA_LIBS})
add_exec_test(stackinfo "stackinfo")
add_executable(serializer serializer.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(serializer ${EXTRA_LIBS})
add_exec_test(serializer "serializer")
add_executable(trie trie.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(trie ${EXTRA_LIBS})
add_exec_test(trie "trie")
add_executable(thread thread.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(thread ${EXTRA_LIBS})
add_exec_test(thread "thread")
add_executable(bitap_fuzzy_search bitap_fuzzy_search.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
target_link_libraries(bitap_fuzzy_search ${EXTRA_LIBS})
add_exec_test(bitap_fuzzy_search "bitap_fuzzy_search")
add_executable(testruntime runtime.cpp ${LEAN_SOURCE_DIR}/runtime/object.cpp ${LEAN_SOURCE_DIR}/runtime/alloc.cpp ${LEAN_SOURCE_DIR}/runtime/thread.cpp
${LEAN_SOURCE_DIR}/runtime/exception.cpp ${LEAN_SOURCE_DIR}/runtime/interrupt.cpp ${LEAN_SOURCE_DIR}/runtime/stackinfo.cpp ${LEAN_SOURCE_DIR}/runtime/memory.cpp ${LEAN_SOURCE_DIR}/runtime/debug.cpp ${LEAN_SOURCE_DIR}/runtime/apply.cpp)
target_link_libraries(testruntime ${EXTRA_LIBS})
add_exec_test(testruntime "runtime")

7
src/tests/util/object.cpp
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include "util/test.h" // <<< comment this list for performance experiments
#include "util/timeit.h"
#include "runtime/stackinfo.h"
#include "runtime/thread.h"
#include "runtime/serializer.h"
#include "runtime/sstream.h"
#include "util/object_ref.h"
@ -433,7 +434,7 @@ bool contains(object * l, object * v) {
object * h = cnstr_get(l, 0);
object * t = cnstr_get(l, 1);
if (!is_shared(l)) {
free_heap_obj(l);
lean_free_object(l);
} else {
inc(h);
inc(t);
@ -482,7 +483,7 @@ bool contains_hybrid(object * l, object * v) {
if (l_b) {
t = mark_borrowed(t_obj);
} else if (!is_shared(l_obj)) {
free_heap_obj(l_obj);
lean_free_object(l_obj);
t = t_obj;
} else {
inc(h_obj);
@ -511,7 +512,7 @@ bool contains_fast_hybrid(object * l, object * v) {
object * t = cnstr_get(l, 1);
bool shared = is_shared(l);
if (!shared) {
free_heap_obj(l);
lean_free_object(l);
} else {
inc(h);
inc(t);

2
src/util/CMakeLists.txt
View file

@ -1,5 +1,5 @@
add_library(util OBJECT object_ref.cpp name.cpp name_set.cpp fresh_name.cpp
escaped.cpp bit_tricks.cpp ascii.cpp shared_mutex.cpp
escaped.cpp bit_tricks.cpp ascii.cpp
path.cpp lean_path.cpp lbool.cpp bitap_fuzzy_search.cpp
init_module.cpp list_fn.cpp file_lock.cpp timeit.cpp timer.cpp
parser_exception.cpp name_generator.cpp kvmap.cpp map_foreach.cpp

5
src/util/object_ref.h
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include <string>
#include "runtime/object.h"
#include "runtime/optional.h"
#include "runtime/serializer.h"
namespace lean {
/* Smart point for Lean objects. It is useful for writing C++ code that manipulates Lean objects. */
@ -17,7 +18,7 @@ protected:
object * m_obj;
public:
object_ref():m_obj(box(0)) {}
explicit object_ref(obj_arg o):m_obj(o) { lean_assert(is_scalar(o) || !is_heap_obj(o) || get_rc(o) > 0); }
explicit object_ref(obj_arg o):m_obj(o) { lean_assert(is_scalar(o) || !is_heap_obj(o) || lean_nonzero_rc(o)); }
object_ref(b_obj_arg o, bool):m_obj(o) { inc(o); }
object_ref(object_ref const & s):m_obj(s.m_obj) { inc(m_obj); }
object_ref(object_ref && s):m_obj(s.m_obj) { s.m_obj = box(0); }
@ -128,7 +129,7 @@ inline object_ref mk_cnstr(unsigned tag, object_ref const & o1, object_ref const
inline object_ref const & cnstr_get_ref(object * o, unsigned i) {
static_assert(sizeof(object_ref) == sizeof(object *), "unexpected object_ref size"); // NOLINT
lean_assert(is_cnstr(o));
return reinterpret_cast<object_ref const *>(reinterpret_cast<char*>(o) + sizeof(constructor_object))[i];
return reinterpret_cast<object_ref const *>(lean_to_ctor(o)->m_objs)[i];
}
inline object_ref const & cnstr_get_ref(object_ref const & ref, unsigned i) {

9
src/util/option_declarations.cpp
View file

@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/shared_mutex.h"
#include "util/option_declarations.h"
namespace lean {
@ -46,11 +45,11 @@ void option_declaration::display_value(std::ostream & out, options const & o) co
}
static option_declarations * g_option_declarations = nullptr;
static shared_mutex * g_option_declarations_guard = nullptr;
static mutex * g_option_declarations_guard = nullptr;
void initialize_option_declarations() {
g_option_declarations = new option_declarations();
g_option_declarations_guard = new shared_mutex();
g_option_declarations_guard = new mutex();
}
void finalize_option_declarations() {
@ -61,14 +60,14 @@ void finalize_option_declarations() {
option_declarations get_option_declarations() {
option_declarations r;
{
shared_lock lock(*g_option_declarations_guard);
unique_lock<mutex> lock(*g_option_declarations_guard);
r = *g_option_declarations;
}
return r;
}
void register_option(name const & n, data_value_kind k, char const * default_value, char const * description) {
exclusive_lock lock(*g_option_declarations_guard);
unique_lock<mutex> lock(*g_option_declarations_guard);
g_option_declarations->insert(n, option_declaration(n, k, default_value, description));
}
}

1
src/util/pair_ref.h
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "runtime/serializer.h"
#include "util/object_ref.h"
namespace lean {