From cf5adbd4feb67d249ba1aba6d8331a7ec96e6d96 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 30 Jan 2021 09:58:04 -0800
Subject: [PATCH] chore: increase `LEAN_MAX_SMALL_OBJECT_SIZE` and simplify
 code

---
 src/Lean/Compiler/IR/EmitC.lean         | 19 +------------------
 src/include/lean/lean.h                 |  9 +++------
 src/library/compiler/ir_interpreter.cpp |  3 +--
 src/runtime/alloc.cpp                   |  2 +-
 4 files changed, 6 insertions(+), 27 deletions(-)

diff --git a/src/Lean/Compiler/IR/EmitC.lean b/src/Lean/Compiler/IR/EmitC.lean
index 97571fb925..de8e70d5dd 100644
--- a/src/Lean/Compiler/IR/EmitC.lean
+++ b/src/Lean/Compiler/IR/EmitC.lean
@@ -16,18 +16,6 @@ import Lean.Compiler.IR.Boxing
 namespace Lean.IR.EmitC
 open ExplicitBoxing (requiresBoxedVersion mkBoxedName isBoxedName)
 
-@[extern c inline "lean_box(LEAN_MAX_SMALL_OBJECT_SIZE)"]
-constant getMaxSmallObjectSize : Unit → Nat
-def maxSmallObjectSize := getMaxSmallObjectSize ()
-
-@[extern c inline "lean_box(sizeof(lean_ctor_object))"]
-constant getCtorHeaderSize : Unit → Nat
-def ctorHeaderSize := getCtorHeaderSize ()
-
-@[extern c inline "lean_box(sizeof(size_t))"]
-constant getUSizeSize : Unit → Nat
-def usizeSize := getUSizeSize ()
-
 def leanMainFn := "_lean_main"
 
 structure Context where
@@ -333,18 +321,13 @@ def emitArgs (ys : Array Arg) : M Unit :=
     if i > 0 then emit ", "
     emitArg ys[i]
 
-private def isSmallCtor (c : CtorInfo) : Bool :=
-  let total := ctorHeaderSize + c.size * usizeSize + c.usize * usizeSize + c.ssize
-  total <= maxSmallObjectSize
-
 def emitCtorScalarSize (usize : Nat) (ssize : Nat) : M Unit := do
   if usize == 0 then emit ssize
   else if ssize == 0 then emit "sizeof(size_t)*"; emit usize
   else emit "sizeof(size_t)*"; emit usize; emit " + "; emit ssize
 
 def emitAllocCtor (c : CtorInfo) : M Unit := do
-  emit <| if isSmallCtor c then "lean_alloc_ctor" else "lean_alloc_ctor_big"
-  emit "("; emit c.cidx; emit ", "; emit c.size; emit ", "
+  emit "lean_alloc_ctor("; emit c.cidx; emit ", "; emit c.size; emit ", "
   emitCtorScalarSize c.usize c.ssize; emitLn ");"
 
 def emitCtorSetArgs (z : VarId) (ys : Array Arg) : M Unit :=
diff --git a/src/include/lean/lean.h b/src/include/lean/lean.h
index 9bf5013c32..60a7b43c9c 100644
--- a/src/include/lean/lean.h
+++ b/src/include/lean/lean.h
@@ -28,7 +28,7 @@ extern "C" {
 
 #define LEAN_CLOSURE_MAX_ARGS      16
 #define LEAN_OBJECT_SIZE_DELTA     8
-#define LEAN_MAX_SMALL_OBJECT_SIZE 512
+#define LEAN_MAX_SMALL_OBJECT_SIZE 4096
 
 #ifdef _MSC_VER
 #define LEAN_ALLOCA(s) _alloca(s)
@@ -698,12 +698,9 @@ static inline lean_object * lean_alloc_ctor(unsigned tag, unsigned num_objs, uns
     return o;
 }
 
-/* Similar to lean_alloc_ctor_big, but does not assume ctor is a small object */
+// TODO: delete
 static inline lean_object * lean_alloc_ctor_big(unsigned tag, unsigned num_objs, unsigned scalar_sz) {
-    assert(tag <= LeanMaxCtorTag && num_objs < LEAN_MAX_CTOR_FIELDS && scalar_sz < LEAN_MAX_CTOR_SCALARS_SIZE);
-    lean_object * o = lean_alloc_object(sizeof(lean_ctor_object) + sizeof(void*)*num_objs + scalar_sz);
-    lean_set_st_header(o, tag, num_objs);
-    return o;
+    return lean_alloc_ctor(tag, num_objs, scalar_sz);
 }
 
 static inline b_lean_obj_res lean_ctor_get(b_lean_obj_arg o, unsigned i) {
diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp
index 8068771aae..a6e907aba1 100644
--- a/src/library/compiler/ir_interpreter.cpp
+++ b/src/library/compiler/ir_interpreter.cpp
@@ -385,8 +385,7 @@ private:
             // a constructor without data is optimized to a tagged pointer
             return box(tag);
         } else {
-            // alloc_cnstr_big does not assume the constructors fits in a small object
-            object *o = alloc_cnstr_big(tag, size, usize * sizeof(void *) + ssize);
+            object *o = alloc_cnstr(tag, size, usize * sizeof(void *) + ssize);
             for (size_t i = 0; i < args.size(); i++) {
                 cnstr_set(o, i, eval_arg(args[i]).m_obj);
             }
diff --git a/src/runtime/alloc.cpp b/src/runtime/alloc.cpp
index b53cc94f93..b2071382f5 100644
--- a/src/runtime/alloc.cpp
+++ b/src/runtime/alloc.cpp
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include <lean/alloc.h>
 #include <lean/lean.h>
 
-#define LEAN_PAGE_SIZE             8192        // 8 Kb
+#define LEAN_PAGE_SIZE             65536       // 64 Kb
 #define LEAN_SEGMENT_SIZE          8*1024*1024 // 8 Mb
 #define LEAN_NUM_SLOTS             (LEAN_MAX_SMALL_OBJECT_SIZE / LEAN_OBJECT_SIZE_DELTA)
 #define LEAN_MAX_TO_EXPORT_OBJS    1024