chore: update stage0

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<expr> 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<expr> 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++;
         }

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 {

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;
 }

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<char*>(new_a) + scalar_offset, reinterpret_cast<char*>(a) + scalar_offset, scalar_sz);
         }
         save(a, new_a);