diff --git a/stage0/src/library/compiler/llnf.cpp b/stage0/src/library/compiler/llnf.cpp index d88f956791..7cec77a69e 100644 --- a/stage0/src/library/compiler/llnf.cpp +++ b/stage0/src/library/compiler/llnf.cpp @@ -270,41 +270,6 @@ static void get_cnstr_info_core(type_checker::state & st, name const & n, buffer } } - /* - Add "filler" fields to make sure constructor objects are aligned. - - Recall that in our runtime `lean_object_byte_size` is always - a multiple of the machine word size for constructors. - - The fillers guarantee that the memory allocated for a - constructor is fully initialized. This is important for the sharing - maximizer procedures at `maxsharing.cpp` and `compact.cpp`. - If we didn't have the fillers, then the memory would not be fully - initialized, and we may mistakenly assume to structurally equal - objects are not identical because of uninitialized memory. - */ - unsigned scalar_sz = 0; - for (field_info & info : result) { - if (info.m_kind == field_info::Scalar) - scalar_sz += info.m_size; - } - if (scalar_sz % sizeof(void*) != 0) { - unsigned to_fill_sz = sizeof(void*) - (scalar_sz % sizeof(void*)); - if (to_fill_sz >= 4) { - result.push_back(field_info::mk_scalar_filler(4, *to_uint_type(4))); - max_scalar_size = std::max(max_scalar_size, 4u); - to_fill_sz -= 4; - } - if (to_fill_sz >= 2) { - result.push_back(field_info::mk_scalar_filler(2, *to_uint_type(2))); - max_scalar_size = std::max(max_scalar_size, 2u); - to_fill_sz -= 2; - } - for (unsigned i = 0; i < to_fill_sz; i++) { - result.push_back(field_info::mk_scalar_filler(1, *to_uint_type(1))); - } - } - unsigned next_idx = next_object; /* Remark: - usize fields are stored after object fields. @@ -574,8 +539,6 @@ class to_lambda_pure_fn { cnstr_info cinfo = get_cnstr_info(cnames[i]); buffer fields; for (field_info const & info : cinfo.m_field_info) { - if (info.m_filler) - break; lean_assert(is_lambda(minor)); switch (info.m_kind) { case field_info::Irrelevant: @@ -664,17 +627,11 @@ class to_lambda_pure_fn { buffer obj_args; unsigned j = nparams; for (field_info const & info : k_info.m_field_info) { - // We need the following test because we have "filler" fields - if (j < args.size()) { - if (info.m_kind != field_info::Irrelevant) - args[j] = visit(args[j]); + if (info.m_kind != field_info::Irrelevant) + args[j] = visit(args[j]); - if (info.m_kind == field_info::Object) { - obj_args.push_back(args[j]); - } - } else { - // Create variable for initializing "filler" fields. - args.push_back(mk_let_decl(info.m_type, mk_lit(literal(mpz(0))))); + if (info.m_kind == field_info::Object) { + obj_args.push_back(args[j]); } j++; } diff --git a/stage0/src/library/compiler/llnf.h b/stage0/src/library/compiler/llnf.h index 04e65045a7..0638eeb56b 100644 --- a/stage0/src/library/compiler/llnf.h +++ b/stage0/src/library/compiler/llnf.h @@ -55,18 +55,16 @@ struct field_info { unsigned m_idx; unsigned m_offset; // it is used only if `m_kind == Scalar` expr m_type; - bool m_filler{false}; // true if it is a "filler" field used to align constructor objects field_info():m_kind(Irrelevant), m_idx(0), m_type(mk_enf_neutral()) {} field_info(unsigned idx):m_kind(Object), m_idx(idx), m_type(mk_enf_object_type()) {} field_info(unsigned num, bool):m_kind(USize), m_idx(num), m_type(mk_constant(get_usize_name())) {} - field_info(unsigned sz, unsigned num, unsigned offset, expr const & type, bool filler): - m_kind(Scalar), m_size(sz), m_idx(num), m_offset(offset), m_type(type), m_filler(filler) {} + field_info(unsigned sz, unsigned num, unsigned offset, expr const & type): + m_kind(Scalar), m_size(sz), m_idx(num), m_offset(offset), m_type(type) {} expr get_type() const { return m_type; } static field_info mk_irrelevant() { return field_info(); } static field_info mk_object(unsigned idx) { return field_info(idx); } static field_info mk_usize() { return field_info(0, true); } - static field_info mk_scalar(unsigned sz, expr const & type) { return field_info(sz, 0, 0, type, false); } - static field_info mk_scalar_filler(unsigned sz, expr const & type) { return field_info(sz, 0, 0, type, true); } + static field_info mk_scalar(unsigned sz, expr const & type) { return field_info(sz, 0, 0, type); } }; struct cnstr_info { diff --git a/stage0/src/runtime/lean.h b/stage0/src/runtime/lean.h index 1ffa018bea..8583217d6e 100644 --- a/stage0/src/runtime/lean.h +++ b/stage0/src/runtime/lean.h @@ -278,6 +278,31 @@ static inline lean_object * lean_alloc_small_object(unsigned sz) { #endif } +static inline lean_object * lean_alloc_ctor_memory(unsigned sz) { +#ifdef LEAN_SMALL_ALLOCATOR + unsigned sz1 = lean_align(sz, LEAN_OBJECT_SIZE_DELTA); + unsigned slot_idx = lean_get_slot_idx(sz1); + assert(sz1 <= LEAN_MAX_SMALL_OBJECT_SIZE); + lean_object* r = (lean_object*)lean_alloc_small(sz1, slot_idx); + if (sz1 > sz) { + /* Initialize last word. + In our runtime `lean_object_byte_size` is always + a multiple of the machine word size for constructors. + + By setting the last word to 0, we make sure the sharing + maximizer procedures at `maxsharing.cpp` and `compact.cpp` are + not affected by uninitialized data at the (sz1 - sz) last bytes. + Otherwise, we may mistakenly assume to structurally equal + objects are not identical because of this uninitialized memory. */ + size_t * end = (size_t*)(((char*)r) + sz1); + end[-1] = 0; + } + return r; +#else + return lean_alloc_small_object(sz); +#endif +} + static inline unsigned lean_small_object_size(lean_object * o) { #ifdef LEAN_SMALL_ALLOCATOR return lean_small_mem_size(o); @@ -622,7 +647,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_alloc_small_object(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz); + lean_object * o = lean_alloc_ctor_memory(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz); lean_set_st_header(o, tag, num_objs); return o; } diff --git a/stage0/src/runtime/maxsharing.cpp b/stage0/src/runtime/maxsharing.cpp index 810709c7b1..d104c9db2e 100644 --- a/stage0/src/runtime/maxsharing.cpp +++ b/stage0/src/runtime/maxsharing.cpp @@ -268,17 +268,16 @@ class max_sharing_fn { } if (missing_child) return; - unsigned tag = lean_ptr_tag(a); - unsigned sz = lean_object_byte_size(a); - lean_object * new_a = lean_alloc_small_object(sz); - lean_set_st_header(new_a, tag, num_objs); + unsigned tag = lean_ptr_tag(a); + unsigned sz = lean_object_byte_size(a); + unsigned scalar_offset = sizeof(lean_object) + num_objs*sizeof(void*); + unsigned scalar_sz = sz - scalar_offset; + lean_object * new_a = lean_alloc_ctor(tag, num_objs, scalar_sz); for (unsigned i = 0; i < num_objs; i++) { lean_inc(m_children[i]); lean_ctor_set(new_a, i, m_children[i]); } - unsigned scalar_offset = sizeof(lean_object) + num_objs*sizeof(void*); - if (scalar_offset < sz) { - unsigned scalar_sz = sz - scalar_offset; + if (scalar_sz > 0) { memcpy(reinterpret_cast(new_a) + scalar_offset, reinterpret_cast(a) + scalar_offset, scalar_sz); } save(a, new_a);