fix extraction, thus fix CI

Makefile

@@ -65,6 +65,7 @@ extract: $(ALL_KRML_FILES)
 	  -bundle Steel.SpinLock= -bundle 'FStar.\*,Steel.\*' \
 	  -bundle 'StarMalloc=Map.\*,Impl.\*,Spec.\*,Main,Main2,Main.Meta,LargeAlloc'[rename=StarMalloc] \
 	  -bundle 'SlabsCommon,SlabsFree,SlabsAlloc'[rename=Slabs] \
+	  -bundle 'SlabsCommon2,SlabsFree2,SlabsAlloc2'[rename=Slabs2] \
 	  -bundle 'SlotsFree,SlotsAlloc'[rename=Slots] \
 	  -bundle 'ArrayList,ArrayListGen'[rename=ArrayList] \
 	  -no-prefix LargeAlloc \
@@ -86,6 +87,7 @@ FILES = \
   dist/krmlinit.c \
   dist/StarMalloc.c \
   dist/Slabs.c \
+  dist/Slabs2.c \
   dist/Slots.c \
   dist/Bitmap5.c \
   dist/Utils2.c \

c/memory.c

@@ -116,6 +116,11 @@ uint32_t* mmap_sizes_init (size_t len) {
   return (uint32_t*) mmap_init(len * sizeof(uint32_t));
 }
 
+// slabs allocator init
+bool* mmap_bool_init (size_t len) {
+  return (bool*) mmap_init(len * sizeof(bool));
+}
+
 // large allocator init
 Impl_Trees_Types_node** mmap_ptr_metadata() {
   return (Impl_Trees_Types_node**) mmap_init(sizeof(Impl_Trees_Types_node*));

dist/Config.c

@@ -3,6 +3,8 @@
 
 #include "Config.h"
 
+bool Config_enable_extended_size_classes = true;
+
 bool Config_enable_sc_fast_selection = true;
 
 size_t Config_metadata_max = (size_t)16777216U;

dist/Config.h

@@ -6,7 +6,13 @@
 
 #include "krmllib.h"
 
-#define CONFIG_NB_SIZE_CLASSES ((size_t)27U)
+#define CONFIG_NB_SIZE_CLASSES ((size_t)31U)
+
+#define CONFIG_NB_SIZE_CLASSES_SC ((size_t)27U)
+
+#define CONFIG_NB_SIZE_CLASSES_SC_EX ((size_t)4U)
+
+extern bool Config_enable_extended_size_classes;
 
 extern bool Config_enable_sc_fast_selection;
 

dist/Constants.c

@@ -5,3 +5,51 @@
 
 uint32_t Constants_page_size = 4096U;
 
+size_t Constants_max_sc_coef = (size_t)32U;
+
+size_t Constants_sc_ex_slab_size = (size_t)4096U * (size_t)64U;
+
+bool Constants_uu___is_Sc(Constants_sc_union projectee)
+{
+  if (projectee.tag == Constants_Sc)
+    return true;
+  else
+    return false;
+}
+
+bool Constants_uu___is_Sc_ex(Constants_sc_union projectee)
+{
+  if (projectee.tag == Constants_Sc_ex)
+    return true;
+  else
+    return false;
+}
+
+uint32_t Constants_get_sc(Constants_sc_union scu)
+{
+  if (scu.tag == Constants_Sc)
+    return scu.case_Sc;
+  else
+  {
+    KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
+      __FILE__,
+      __LINE__,
+      "unreachable (pattern matches are exhaustive in F*)");
+    KRML_HOST_EXIT(255U);
+  }
+}
+
+uint32_t Constants_get_sc_ex(Constants_sc_union scu)
+{
+  if (scu.tag == Constants_Sc_ex)
+    return scu.case_Sc_ex;
+  else
+  {
+    KRML_HOST_EPRINTF("KaRaMeL abort at %s:%d\n%s\n",
+      __FILE__,
+      __LINE__,
+      "unreachable (pattern matches are exhaustive in F*)");
+    KRML_HOST_EXIT(255U);
+  }
+}
+

dist/Constants.h

@@ -8,6 +8,36 @@
 
 extern uint32_t Constants_page_size;
 
+extern size_t Constants_max_sc_coef;
+
+extern size_t Constants_sc_ex_slab_size;
+
+typedef uint32_t Constants_sc_ex;
+
+#define Constants_Sc 0
+#define Constants_Sc_ex 1
+
+typedef uint8_t Constants_sc_union_tags;
+
+typedef struct Constants_sc_union_s
+{
+  Constants_sc_union_tags tag;
+  union {
+    uint32_t case_Sc;
+    uint32_t case_Sc_ex;
+  }
+  ;
+}
+Constants_sc_union;
+
+bool Constants_uu___is_Sc(Constants_sc_union projectee);
+
+bool Constants_uu___is_Sc_ex(Constants_sc_union projectee);
+
+uint32_t Constants_get_sc(Constants_sc_union scu);
+
+uint32_t Constants_get_sc_ex(Constants_sc_union scu);
+
 
 #define __Constants_H_DEFINED
 #endif

dist/Makefile.include

@@ -1,5 +1,5 @@
 USER_TARGET=
 USER_CFLAGS=
 USER_C_FILES=
-ALL_C_FILES=ArrayList.c Bitmap5.c Config.c Constants.c SizeClass.c SizeClassSelection.c Slabs.c Slots.c StarMalloc.c Utils2.c krmlinit.c
-ALL_H_FILES=ArrayList.h Bitmap5.h Config.h Constants.h ExternUtils.h MemoryTrap.h Mman.h SizeClass.h SizeClassSelection.h StarMalloc.h Steel_SpinLock.h Utils2.h internal/ArrayList.h internal/Slabs.h internal/Slots.h internal/StarMalloc.h krmlinit.h
+ALL_C_FILES=ArrayList.c Bitmap5.c Config.c Constants.c SizeClass.c SizeClassSelection.c Slabs.c Slabs2.c Slots.c StarMalloc.c Utils2.c krmlinit.c
+ALL_H_FILES=ArrayList.h Bitmap5.h Config.h Constants.h ExternUtils.h MemoryTrap.h Mman.h SizeClass.h SizeClassSelection.h StarMalloc.h Steel_SpinLock.h Utils2.h internal/ArrayList.h internal/Slabs.h internal/Slabs2.h internal/Slots.h internal/StarMalloc.h krmlinit.h

dist/Mman.h

@@ -15,6 +15,8 @@ extern uint64_t *mmap_u64_init(size_t len);
 
 extern ArrayList_cell *mmap_cell_status_init(size_t len);
 
+extern bool *mmap_bool_init(size_t len);
+
 extern size_t *mmap_ptr_us_init(void);
 
 extern size_t *mmap_array_us_init(size_t len);

dist/SizeClass.c

@@ -3,13 +3,19 @@
 
 #include "SizeClass.h"
 
+#include "internal/Slabs2.h"
 #include "internal/Slabs.h"
 
-uint8_t *SizeClass_allocate_size_class(SizeClass_size_class_struct_ scs)
+uint8_t *SizeClass_allocate_size_class_sc(SizeClass_size_class_struct_ scs)
 {
+  uint32_t ite;
+  if (scs.size.tag == Constants_Sc)
+    ite = scs.size.case_Sc;
+  else
+    ite = KRML_EABORT(uint32_t, "unreachable (pattern matches are exhaustive in F*)");
   uint8_t
   *result =
-    SlabsAlloc_allocate_slab(scs.size,
+    SlabsAlloc_allocate_slab(ite,
       scs.slab_region,
       scs.md_bm_region,
       scs.md_region,
@@ -19,12 +25,17 @@ uint8_t *SizeClass_allocate_size_class(SizeClass_size_class_struct_ scs)
 }
 
 bool
-SizeClass_deallocate_size_class(SizeClass_size_class_struct_ scs, uint8_t *ptr, size_t diff)
+SizeClass_deallocate_size_class_sc(SizeClass_size_class_struct_ scs, uint8_t *ptr, size_t diff)
 {
+  uint32_t ite;
+  if (scs.size.tag == Constants_Sc)
+    ite = scs.size.case_Sc;
+  else
+    ite = KRML_EABORT(uint32_t, "unreachable (pattern matches are exhaustive in F*)");
   bool
   b =
     SlabsFree_deallocate_slab(ptr,
-      scs.size,
+      ite,
       scs.slab_region,
       scs.md_bm_region,
       scs.md_region,
@@ -34,3 +45,71 @@ SizeClass_deallocate_size_class(SizeClass_size_class_struct_ scs, uint8_t *ptr,
   return b;
 }
 
+static uint8_t *allocate_size_class_sc_ex(SizeClass_size_class_struct_ scs)
+{
+  uint32_t ite;
+  if (scs.size.tag == Constants_Sc_ex)
+    ite = scs.size.case_Sc_ex;
+  else
+    ite = KRML_EABORT(uint32_t, "unreachable (pattern matches are exhaustive in F*)");
+  uint8_t
+  *result =
+    SlabsAlloc2_allocate_slab(ite,
+      scs.slab_region,
+      scs.md_bm_region_b,
+      scs.md_region,
+      scs.md_count,
+      scs.slabs_idxs);
+  return result;
+}
+
+static bool
+deallocate_size_class_sc_ex(SizeClass_size_class_struct_ scs, uint8_t *ptr, size_t diff)
+{
+  uint32_t ite;
+  if (scs.size.tag == Constants_Sc_ex)
+    ite = scs.size.case_Sc_ex;
+  else
+    ite = KRML_EABORT(uint32_t, "unreachable (pattern matches are exhaustive in F*)");
+  bool
+  b =
+    SlabsFree2_deallocate_slab(ptr,
+      ite,
+      scs.slab_region,
+      scs.md_bm_region_b,
+      scs.md_region,
+      scs.md_count,
+      scs.slabs_idxs,
+      diff);
+  return b;
+}
+
+uint8_t *SizeClass_allocate_size_class(SizeClass_size_class_struct_ scs)
+{
+  if (scs.is_extended)
+  {
+    uint8_t *r = allocate_size_class_sc_ex(scs);
+    return r;
+  }
+  else
+  {
+    uint8_t *r = SizeClass_allocate_size_class_sc(scs);
+    return r;
+  }
+}
+
+bool
+SizeClass_deallocate_size_class(SizeClass_size_class_struct_ scs, uint8_t *ptr, size_t diff)
+{
+  if (scs.is_extended)
+  {
+    bool r = deallocate_size_class_sc_ex(scs, ptr, diff);
+    return r;
+  }
+  else
+  {
+    bool r = SizeClass_deallocate_size_class_sc(scs, ptr, diff);
+    return r;
+  }
+}
+

dist/SizeClass.h

@@ -6,21 +6,33 @@
 
 #include "krmllib.h"
 
+#include "Constants.h"
 #include "ArrayList.h"
 
 typedef struct SizeClass_size_class_struct__s
 {
-  uint32_t size;
+  Constants_sc_union size;
+  bool is_extended;
   size_t *slabs_idxs;
   size_t *md_count;
   uint8_t *slab_region;
   uint64_t *md_bm_region;
+  bool *md_bm_region_b;
   ArrayList_cell *md_region;
 }
 SizeClass_size_class_struct_;
 
 typedef SizeClass_size_class_struct_ SizeClass_size_class_struct;
 
+typedef SizeClass_size_class_struct_ SizeClass_size_class_struct_sc;
+
+typedef SizeClass_size_class_struct_ SizeClass_size_class_struct_sc_ex;
+
+uint8_t *SizeClass_allocate_size_class_sc(SizeClass_size_class_struct_ scs);
+
+bool
+SizeClass_deallocate_size_class_sc(SizeClass_size_class_struct_ scs, uint8_t *ptr, size_t diff);
+
 uint8_t *SizeClass_allocate_size_class(SizeClass_size_class_struct_ scs);
 
 bool