From fdcbf3fe9e406be24945e6532c9c95cbbc507096 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Aug 2018 12:47:19 -0700 Subject: [PATCH] chore(runtime/object): "section comments" --- src/runtime/object.cpp | 25 +++++++++----- src/runtime/object.h | 76 ++++++++++++++++++++++++++++++------------ 2 files changed, 71 insertions(+), 30 deletions(-) diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp index 473bcf1b38..1c47349932 100644 --- a/src/runtime/object.cpp +++ b/src/runtime/object.cpp @@ -135,7 +135,8 @@ void del(object * o) { } } -/* Scalar arrays */ +// ======================================= +// Scalar arrays #if 0 static object * sarray_ensure_capacity(object * o, size_t extra) { @@ -155,7 +156,9 @@ static object * sarray_ensure_capacity(object * o, size_t extra) { } #endif -/* Strings */ +// ======================================= +// Strings + static inline char * w_string_data(object * o) { lean_assert(is_string(o)); return reinterpret_cast(o) + sizeof(string_object); } static object * string_ensure_capacity(object * o, size_t extra) { @@ -238,7 +241,8 @@ bool string_lt(object * s1, object * s2) { return r < 0 || (r == 0 && sz1 < sz2); } -/* Closures */ +// ======================================= +// Closures typedef object * (*lean_cfun2)(object *, object *); // NOLINT typedef object * (*lean_cfun3)(object *, object *, object *); // NOLINT @@ -256,7 +260,8 @@ static obj_res mk_closure_3_2(lean_cfun3 fn, obj_arg a1, obj_arg a2) { return c; } -/* Thunks */ +// ======================================= +// 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)); @@ -314,7 +319,8 @@ obj_res thunk_bind(obj_arg x, obj_arg f) { return mk_thunk_3_2(thunk_bind_fn_closure, x, f); } -/* Tasks */ +// ======================================= +// Tasks LEAN_THREAD_PTR(task_object, g_current_task_object); @@ -714,7 +720,8 @@ b_obj_res io_wait_any_core(b_obj_arg task_list) { return g_task_manager->wait_any(task_list); } -/* Natural numbers */ +// ======================================= +// Natural numbers object * nat_big_add(object * a1, object * a2) { lean_assert(!is_scalar(a1) || !is_scalar(a2)); @@ -847,7 +854,8 @@ object * nat_big_lxor(object * a1, object * a2) { return mk_nat_obj(mpz_value(a1) ^ mpz_value(a2)); } -/* Integers */ +// ======================================= +// Integers object * int_big_add(object * a1, object * a2) { if (is_scalar(a1)) @@ -926,7 +934,8 @@ bool int_big_lt(object * a1, object * a2) { } } -/* Debugging helper functions */ +// ======================================= +// Debugging helper functions void dbg_print_str(object * o) { lean_assert(is_string(o)); diff --git a/src/runtime/object.h b/src/runtime/object.h index d07b0385de..5926499a5c 100644 --- a/src/runtime/object.h +++ b/src/runtime/object.h @@ -176,7 +176,9 @@ inline void dec_ref(object * o) { if (dec_ref_core(o)) del(o); } inline void inc(object * o) { if (!is_scalar(o)) inc_ref(o); } inline void dec(object * o) { if (!is_scalar(o)) dec_ref(o); } -/* Testers */ +// ======================================= +// Testers + inline object_kind get_kind(object * o) { return static_cast(o->m_kind); } inline bool is_cnstr(object * o) { return get_kind(o) == object_kind::Constructor; } inline bool is_closure(object * o) { return get_kind(o) == object_kind::Closure; } @@ -188,7 +190,9 @@ inline bool is_thunk(object * o) { return get_kind(o) == object_kind::Thunk; } inline bool is_task(object * o) { return get_kind(o) == object_kind::Task; } inline bool is_external(object * o) { return get_kind(o) == object_kind::External; } -/* Casting */ +// ======================================= +// Casting + inline constructor_object * to_cnstr(object * o) { lean_assert(is_cnstr(o)); return static_cast(o); } inline closure_object * to_closure(object * o) { lean_assert(is_closure(o)); return static_cast(o); } inline array_object * to_array(object * o) { lean_assert(is_array(o)); return static_cast(o); } @@ -217,7 +221,8 @@ inline void dealloc(object * o) { } } -/* Object auxiliary functions */ +// ======================================= +// Object auxiliary functions /* Size of the object in bytes. This function is used for debugging purposes. \pre !is_scalar(o) && !is_external(o) */ @@ -244,7 +249,9 @@ inline void obj_set_data(object * o, size_t offset, T v) { *(reinterpret_cast(reinterpret_cast(o) + offset)) = v; } -/* Constructor auxiliary functions */ +// ======================================= +// Constructor auxiliary functions + inline unsigned cnstr_num_objs(object * o) { return to_cnstr(o)->m_num_objs; } inline unsigned cnstr_scalar_size(object * o) { return to_cnstr(o)->m_scalar_size; } inline size_t cnstr_byte_size(object * o) { return sizeof(constructor_object) + cnstr_num_objs(o)*sizeof(object*) + cnstr_scalar_size(o); } // NOLINT @@ -257,7 +264,8 @@ inline unsigned char * cnstr_scalar_cptr(object * o) { return reinterpret_cast(reinterpret_cast(o) + sizeof(constructor_object) + cnstr_num_objs(o)*sizeof(object*)); // NOLINT } -/* Closure auxiliary functions */ +// ======================================= +// Closure auxiliary functions inline lean_cfun closure_fun(object * o) { return to_closure(o)->m_fun; } inline unsigned closure_arity(object * o) { return to_closure(o)->m_arity; } @@ -268,7 +276,8 @@ inline object ** closure_arg_cptr(object * o) { return reinterpret_cast(reinterpret_cast(o) + sizeof(closure_object)); } -/* Thunk auxiliary functions */ +// ======================================= +// Thunk auxiliary functions inline thunk_object::thunk_object(object * c, bool is_value): object(object_kind::Thunk) { @@ -285,7 +294,8 @@ object * apply_1(object * f, object * a1); /* Expensive version of thunk_get which tries to execute the nested closure */ object * thunk_get_core(object * t); -/* Array auxiliary functions */ +// ======================================= +// Array auxiliary functions inline size_t array_capacity(object * o) { return to_array(o)->m_capacity; } inline size_t array_byte_size(object * o) { return sizeof(array_object) + array_capacity(o)*sizeof(object*); } // NOLINT @@ -294,7 +304,8 @@ inline object ** array_cptr(object * o) { return reinterpret_cast(reinterpret_cast(o) + sizeof(array_object)); } -/* Array of scalars auxiliary functions */ +// ======================================= +// Array of scalars auxiliary functions inline unsigned sarray_elem_size(object * o) { return to_sarray(o)->m_elem_size; } inline size_t sarray_capacity(object * o) { return to_sarray(o)->m_capacity; } @@ -304,15 +315,19 @@ T * sarray_cptr_core(object * o) { lean_assert(is_sarray(o)); return reinterpret template T * sarray_cptr(object * o) { lean_assert(sarray_elem_size(o) == sizeof(T)); return sarray_cptr_core(o); } -/* String auxiliary functions */ +// ======================================= +// String auxiliary functions inline size_t string_capacity(object * o) { return to_string(o)->m_capacity; } inline size_t string_byte_size(object * o) { return sizeof(string_object) + string_capacity(o); } // NOLINT -/* MPZ auxiliary function */ +// ======================================= +// MPZ auxiliary function + inline object * alloc_mpz(mpz const & m) { return new mpz_object(m); } -/* Natural numbers auxiliary functions */ +// ======================================= +// Natural numbers auxiliary functions #define LEAN_MAX_SMALL_NAT (sizeof(void*) == 8 ? std::numeric_limits::max() : (std::numeric_limits::max() >> 1)) // NOLINT inline object * mk_nat_obj_core(mpz const & m) { @@ -331,7 +346,8 @@ object * nat_big_land(object * a1, object * a2); object * nat_big_lor(object * a1, object * a2); object * nat_big_xor(object * a1, object * a2); -/* Integers auxiliary functions */ +// ======================================= +// Integers auxiliary functions #define LEAN_MAX_SMALL_INT (sizeof(void*) == 8 ? std::numeric_limits::max() : (1 << 30)) // NOLINT #define LEAN_MIN_SMALL_INT (sizeof(void*) == 8 ? std::numeric_limits::min() : -(1 << 30)) // NOLINT @@ -380,7 +396,9 @@ typedef object * u_obj_arg; /* Unique (aka non shared) object argument. */ typedef object * obj_res; /* Standard object result. */ typedef object * b_obj_res; /* Borrowed object result. */ -/* Constructor objects */ +// ======================================= +// Constructor objects + inline obj_res alloc_cnstr(unsigned tag, unsigned num_objs, unsigned scalar_sz) { lean_assert(tag < 65536 && num_objs < 65536 && scalar_sz < 65536); return new (malloc(sizeof(constructor_object) + num_objs * sizeof(object *) + scalar_sz)) constructor_object(tag, num_objs, scalar_sz); // NOLINT @@ -407,7 +425,9 @@ template inline void cnstr_set_scalar(b_obj_arg o, unsigned i, T v) inline unsigned obj_tag(b_obj_arg o) { if (is_scalar(o)) return unbox(o); else return cnstr_tag(o); } -/* Closures */ +// ======================================= +// Closures + inline obj_res alloc_closure(lean_cfun fun, unsigned arity, unsigned num_fixed) { lean_assert(arity > 0); lean_assert(num_fixed < arity); @@ -422,7 +442,9 @@ inline void closure_set_arg(u_obj_arg o, unsigned i, obj_arg a) { obj_set_data(o, sizeof(closure_object) + sizeof(object*)*i, a); // NOLINT } -/* Array of objects */ +// ======================================= +// Array of objects + inline obj_res alloc_array(size_t size, size_t capacity) { return new (malloc(sizeof(array_object) + capacity * sizeof(object *))) array_object(size, capacity); // NOLINT } @@ -443,7 +465,9 @@ inline void array_set_obj(u_obj_arg o, size_t i, obj_arg v) { obj_set_data(o, sizeof(array_object) + sizeof(object*)*i, v); // NOLINT } -/* Array of scalars */ +// ======================================= +// Array of scalars + inline obj_res alloc_sarray(unsigned elem_size, size_t size, size_t capacity) { return new (malloc(sizeof(sarray_object) + capacity * elem_size)) sarray_object(elem_size, size, capacity); // NOLINT } @@ -459,10 +483,13 @@ inline void sarray_set_size(u_obj_arg o, size_t sz) { to_sarray(o)->m_size = sz; } -/* MPZ */ +// ======================================= +// MPZ + inline mpz const & mpz_value(b_obj_arg o) { return to_mpz(o)->m_value; } -/* Thunks */ +// ======================================= +// Thunks inline obj_res mk_thunk(obj_arg c) { return new (malloc(sizeof(thunk_object))) thunk_object(c, false); // NOLINT @@ -480,7 +507,8 @@ inline b_obj_res thunk_get(b_obj_arg t) { return thunk_get_core(t); } -/* Tasks */ +// ======================================= +// Tasks /* If num_workers == 0, then tasks primitives will just create thunks. It must not be used if task objects have already been created. */ @@ -510,7 +538,9 @@ bool io_has_finished_core(b_obj_arg t); /* primitive for implementing `io.wait_any : list (task A) -> io (task A) */ b_obj_res io_wait_any_core(b_obj_arg task_list); -/* String */ +// ======================================= +// String + inline obj_res alloc_string(size_t size, size_t capacity, size_t len) { return new (malloc(sizeof(string_object) + capacity)) string_object(size, capacity, len); // NOLINT } @@ -527,7 +557,8 @@ inline bool string_ne(b_obj_arg s1, b_obj_arg s2) { return !string_eq(s1, s2); } bool string_eq(b_obj_arg s1, char const * s2); bool string_lt(b_obj_arg s1, b_obj_arg s2); -/* Natural numbers */ +// ======================================= +// Natural numbers inline obj_res mk_nat_obj(mpz const & m) { if (m > LEAN_MAX_SMALL_NAT) @@ -674,7 +705,8 @@ inline obj_res nat_lxor(b_obj_arg a1, b_obj_arg a2) { } } -/* Integers */ +// ======================================= +// Integers inline obj_res mk_int_obj(mpz const & m) { if (m < LEAN_MIN_SMALL_INT || m > LEAN_MAX_SMALL_INT)