Merge remote-tracking branch 'origin/main' into areitz/extended-size-…

…classes
Inria-Prosecco · Jul 11, 2024 · b7163f4 · b7163f4
2 parents 5e4001f + c5b206b
commit b7163f4
Show file tree

Hide file tree

Showing 23 changed files with 636 additions and 4,621 deletions.
diff --git a/Makefile b/Makefile
@@ -65,13 +65,14 @@ extract: $(ALL_KRML_FILES)
 	  -header spdx-header.txt \
 	  -library Steel.ArrayArith -static-header Steel.ArrayArith -no-prefix Steel.ArrayArith \
 	  -bundle Steel.SpinLock= -bundle 'FStar.\*,Steel.\*' \
-	  -bundle 'StarMalloc=Map.\*,Impl.\*,Spec.\*,Main,Main2,Main.Meta,LargeAlloc'[rename=StarMalloc] \
+	  -bundle 'StarMalloc=Mman2,FatalError,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 \
 	  -no-prefix Mman \
+	  -no-prefix Mman2 \
 	  -no-prefix MemoryTrap \
 	  -no-prefix ExternUtils \
 	  -warn-error +9 \

diff --git a/c/memory.c b/c/memory.c
@@ -6,6 +6,8 @@
 #include "internal/StarMalloc.h"
 #include "fatal_error.h"
 
+/// Mman.fst
+
 // syscall wrapper: initialization (fatal error on failure)
 uint8_t *mmap_init(size_t size) {
   void* ptr = mmap(NULL, size, PROT_READ|PROT_WRITE, MAP_ANONYMOUS|MAP_PRIVATE|MAP_NORESERVE, -1, 0);
@@ -42,38 +44,6 @@ void munmap_u8(uint8_t* ptr, size_t len) {
   return;
 }
 
-// syscall wrapper
-void mmap_strict_trap (uint8_t* ptr, size_t len) {
-  void* p = mmap((void*) ptr, len, PROT_NONE, MAP_ANONYMOUS|MAP_PRIVATE|MAP_FIXED, -1, 0);
-  if (p == MAP_FAILED && errno != ENOMEM) {
-    fatal_error("non-ENOMEM mmap failure");
-  }
-  return;
-}
-
-// syscall wrapper
-void mmap_strict_untrap (uint8_t* ptr, size_t len) {
-  void* p = mmap((void*) ptr, len, PROT_READ|PROT_WRITE, MAP_ANONYMOUS|MAP_PRIVATE|MAP_FIXED, -1, 0);
-  if (p == MAP_FAILED && errno != ENOMEM) {
-    fatal_error("non-ENOMEM mmap failure");
-  }
-  return;
-}
-
-// syscall wrapper
-void mmap_trap (uint8_t* ptr, size_t len) {
-  int r = madvise((void*) ptr, len, MADV_DONTNEED);
-  if (r && errno != ENOMEM) {
-    fatal_error("non-ENOMEM MADV_DONTNEED madvise failure");
-  }
-  return;
-}
-
-// wrapper
-void mmap_untrap (uint8_t* ptr, size_t len) {
-  return;
-}
-
 // monomorphised functions
 
 // large allocator allocation wrapper
@@ -121,7 +91,43 @@ bool* mmap_bool_init (size_t len) {
   return (bool*) mmap_init(len * sizeof(bool));
 }
 
+/// Mman2
+
 // large allocator init
-Impl_Trees_Types_node** mmap_ptr_metadata() {
-  return (Impl_Trees_Types_node**) mmap_init(sizeof(Impl_Trees_Types_node*));
+Impl_Trees_Cast_M_node** mmap_ptr_metadata_init() {
+  return (Impl_Trees_Cast_M_node**) mmap_init(sizeof(Impl_Trees_Cast_M_node*));
+}
+
+/// MemoryTrap.fst
+
+// syscall wrapper
+void mmap_strict_trap (uint8_t* ptr, size_t len) {
+  void* p = mmap((void*) ptr, len, PROT_NONE, MAP_ANONYMOUS|MAP_PRIVATE|MAP_FIXED, -1, 0);
+  if (p == MAP_FAILED && errno != ENOMEM) {
+    fatal_error("non-ENOMEM mmap failure");
+  }
+  return;
+}
+
+// syscall wrapper
+void mmap_strict_untrap (uint8_t* ptr, size_t len) {
+  void* p = mmap((void*) ptr, len, PROT_READ|PROT_WRITE, MAP_ANONYMOUS|MAP_PRIVATE|MAP_FIXED, -1, 0);
+  if (p == MAP_FAILED && errno != ENOMEM) {
+    fatal_error("non-ENOMEM mmap failure");
+  }
+  return;
+}
+
+// syscall wrapper
+void mmap_trap (uint8_t* ptr, size_t len) {
+  int r = madvise((void*) ptr, len, MADV_DONTNEED);
+  if (r && errno != ENOMEM) {
+    fatal_error("non-ENOMEM MADV_DONTNEED madvise failure");
+  }
+  return;
+}
+
+// wrapper
+void mmap_untrap (uint8_t* ptr, size_t len) {
+  return;
 }
diff --git a/c/utils.c b/c/utils.c
@@ -23,9 +23,9 @@ size_t builtin_mul_overflow(size_t x, size_t y) {
 }
 
 // required comparison using uintptr_t
-uint64_t Impl_Trees_Types_cmp(
-  Impl_Trees_Types_data x,
-  Impl_Trees_Types_data y) {
+uint64_t Impl_Trees_Cast_M_cmp(
+  Impl_Trees_Cast_M_data x,
+  Impl_Trees_Cast_M_data y) {
   uintptr_t x_cast = (uintptr_t) x.fst;
   uintptr_t y_cast = (uintptr_t) y.fst;
   if (x_cast == y_cast) {
@@ -43,27 +43,12 @@ uint8_t* memcpy_u8(uint8_t* dest, uint8_t* src, size_t n) {
 }
 
 // monomorphized (from void* to uint8_t*) glue
-// TODO: memset can be optimized, use hacl-star libmemzero
+// TODO: compat, use hacl-star libmemzero
 void apply_zeroing_u8(uint8_t* dest, size_t n) {
-  memset((void*) dest, 0, n);
+  explicit_bzero(dest, n);
   return;
 }
 
-// required casts
-Impl_Trees_Types_node* Impl_Trees_Types_array_u8__to__ref_node(uint8_t* arr) {
-  // see lib_avl_mono/Impl.Trees.Types.fst
-  static_assert(sizeof(Impl_Trees_Types_node) <= 64);
-  return (Impl_Trees_Types_node*) arr;
-}
-uint8_t* Impl_Trees_Types_ref_node__to__array_u8(Impl_Trees_Types_node* r) {
-  return (uint8_t*) r;
-}
-
-// TODO: comment
-void StarMalloc_malloc_zeroing_die(uint8_t* ptr) {
-  fatal_error("malloc_zeroing_die");
-}
-
 bool check_zeroing_u8(uint8_t* ptr, size_t len) {
   for (size_t i = 0; i < len; i++) {
     if (ptr[i] != 0) {
@@ -73,7 +58,28 @@ bool check_zeroing_u8(uint8_t* ptr, size_t len) {
   return true;
 }
 
-void SlotsFree_deallocate_zeroing(uint32_t sc, uint8_t* ptr) {
-  size_t len = (size_t) sc;
-  memset(ptr, 0, len);
+// required casts
+Impl_Trees_Cast_M_node* Impl_Trees_Cast_M_array_u8__to__ref_node(uint8_t* arr) {
+  // see lib_avl_mono/Impl.Trees.Types.fst
+  static_assert(sizeof(Impl_Trees_Cast_M_node) <= 64);
+  return (Impl_Trees_Cast_M_node*) arr;
+}
+uint8_t* Impl_Trees_Cast_M_ref_node__to__array_u8(Impl_Trees_Cast_M_node* r) {
+  return (uint8_t*) r;
+}
+
+void FatalError_die_from_avl_node_malloc_failure (Impl_Trees_Cast_M_node x, uint8_t* ptr) {
+  fatal_error("large allocator: AVL node allocation failed");
+}
+void FatalError_die_from_avl_node_free_failure (uint8_t* ptr) {
+  fatal_error("large allocator: AVL node deallocation failed");
+}
+void FatalError_die_from_malloc_zeroing_check_failure (uint8_t* ptr) {
+  fatal_error("small allocator: malloc zeroing check failed");
+}
+void FatalError_die_from_realloc_invalid_previous_alloc (uint8_t* ptr) {
+  fatal_error("realloc: invalid realloc");
+}
+void FatalError_die_from_realloc_free_failure (uint8_t* ptr) {
+  fatal_error("realloc: invalid internal free");
 }
diff --git a/dist/ExternUtils.h b/dist/ExternUtils.h
@@ -10,14 +10,14 @@ extern uint32_t ffs64(uint64_t x);
 
 extern uint32_t clz(uint64_t x);
 
+extern size_t builtin_mul_overflow(size_t x, size_t y);
+
 extern void apply_zeroing_u8(uint8_t *ptr, size_t n);
 
 extern bool check_zeroing_u8(uint8_t *ptr, size_t n);
 
 extern uint8_t *memcpy_u8(uint8_t *dest, uint8_t *src, size_t n);
 
-extern size_t builtin_mul_overflow(size_t x, size_t y);
-
 
 #define __ExternUtils_H_DEFINED
 #endif
diff --git a/dist/Slots.c b/dist/Slots.c
@@ -89,7 +89,10 @@ static uint32_t deallocate_slot_aux1(uint32_t size_class, uint32_t diff)
   return diff / size_class;
 }
 
-extern void SlotsFree_deallocate_zeroing(uint32_t size_class, uint8_t *ptr);
+static void deallocate_zeroing(uint32_t size_class, uint8_t *ptr)
+{
+  apply_zeroing_u8(ptr, (size_t)size_class);
+}
 
 static bool deallocate_slot_(uint32_t size_class, uint64_t *md, uint8_t *ptr, size_t diff_)
 {
@@ -102,7 +105,7 @@ static bool deallocate_slot_(uint32_t size_class, uint64_t *md, uint8_t *ptr, si
     if (b1)
     {
       Bitmap5_bm_unset(md, pos);
-      SlotsFree_deallocate_zeroing(size_class, ptr);
+      deallocate_zeroing(size_class, ptr);
       return true;
     }
     else