refresh dist/

Inria-Prosecco · Jul 20, 2024 · 2f10fa0 · 2f10fa0
1 parent 1d6c81f
commit 2f10fa0
Show file tree

Hide file tree

Showing 4 changed files with 188 additions and 15 deletions.
diff --git a/dist/Config.c b/dist/Config.c
@@ -13,7 +13,7 @@ size_t Config_guard_pages_interval = (size_t)2U;
 
 bool Config_enable_quarantine = true;
 
-bool Config_enable_quarantine_slot = true;
+bool Config_enable_quarantine_slot = false;
 
 bool Config_enable_quarantine_trap = true;
 

diff --git a/dist/Slabs.c b/dist/Slabs.c
@@ -6,6 +6,82 @@
 #include "internal/Slots.h"
 #include "internal/ArrayList.h"
 
+typedef struct tuple4_s
+{
+  size_t x;
+  size_t y;
+  size_t z;
+  size_t w;
+}
+tuple4;
+
+static tuple4
+update_quarantine2_aux(
+  ArrayList_cell *md_region,
+  size_t idx1,
+  size_t idx5,
+  size_t idx6,
+  size_t idx7
+)
+{
+  ArrayList_cell cell = md_region[idx6];
+  if (cell.next != (size_t)16777217U)
+  {
+    ArrayList_cell next = md_region[cell.next];
+    ArrayList_cell next1 = { .prev = cell.prev, .next = next.next, .data = next.data };
+    md_region[cell.next] = next1;
+  }
+  size_t tl_ = cell.prev;
+  if (cell.prev != (size_t)16777217U)
+  {
+    ArrayList_cell prev = md_region[cell.prev];
+    ArrayList_cell prev1 = { .prev = prev.prev, .next = cell.next, .data = prev.data };
+    md_region[cell.prev] = prev1;
+  }
+  size_t hd_;
+  if (idx5 == idx6)
+    hd_ = cell.next;
+  else
+    hd_ = idx5;
+  size_t sz_ = idx7 - (size_t)1U;
+  ArrayListGen_tuple3 idxs = { .x = hd_, .y = tl_, .z = sz_ };
+  ArrayList_insert(md_region, idx1, idx6, 0U);
+  return ((tuple4){ .x = idx6, .y = idxs.x, .z = idxs.y, .w = idxs.z });
+}
+
+static tuple4
+update_quarantine2(
+  ArrayList_cell *md_region,
+  size_t idx1,
+  size_t idx5,
+  size_t idx6,
+  size_t idx7
+)
+{
+  if (idx7 < (size_t)1024U)
+    return ((tuple4){ .x = idx1, .y = idx5, .z = idx6, .w = idx7 });
+  else
+  {
+    tuple4 idxs = update_quarantine2_aux(md_region, idx1, idx5, idx6, idx7);
+    return idxs;
+  }
+}
+
+static void update_quarantine3_aux(uint8_t *slab_region, tuple4 idxs)
+{
+  size_t idx = idxs.x;
+  uint8_t *ptr = slab_region;
+  size_t page_size_t = (size_t)4096U;
+  size_t shift_size_t = idx * page_size_t;
+  mmap_untrap(ptr + shift_size_t, (size_t)4096U);
+}
+
+static void update_quarantine3(uint8_t *slab_region, size_t idx7, tuple4 idxs)
+{
+  if (!(idx7 < (size_t)1024U))
+    update_quarantine3_aux(slab_region, idxs);
+}
+
 bool
 SlabsFree_deallocate_slab(
   uint8_t *ptr,
@@ -19,8 +95,13 @@ SlabsFree_deallocate_slab(
   size_t diff_
 )
 {
-  KRML_MAYBE_UNUSED_VAR(r_idxs);
   size_t md_count_v_ = *md_count;
+  size_t idx1_ = r_idxs[0U];
+  size_t idx2_ = r_idxs[1U];
+  size_t idx3_ = r_idxs[2U];
+  size_t idx5_ = r_idxs[4U];
+  size_t idx6_ = r_idxs[5U];
+  size_t idx7_ = r_idxs[6U];
   size_t pos = diff_ / (size_t)4096U;
   size_t pos2 = diff_ % (size_t)4096U;
   if (pos < md_count_v_)
@@ -29,44 +110,129 @@ SlabsFree_deallocate_slab(
     if (status1 == 2U)
     {
       uint8_t *ptr10 = slab_region;
-      size_t page_size_t = (size_t)4096U;
-      size_t shift_size_t0 = pos * page_size_t;
+      size_t page_size_t0 = (size_t)4096U;
+      size_t shift_size_t0 = pos * page_size_t0;
       uint64_t *ptr11 = md_bm_region;
       size_t shift_size_t1 = pos * (size_t)4U;
-      uint64_t *ptr1 = md_bm_region_q;
-      size_t shift_size_t = pos * (size_t)4U;
+      uint64_t *ptr12 = md_bm_region_q;
+      size_t shift_size_t2 = pos * (size_t)4U;
       bool
       b =
         SlotsFree_deallocate_slot(size_class,
           ptr10 + shift_size_t0,
           ptr11 + shift_size_t1,
-          ptr1 + shift_size_t,
+          ptr12 + shift_size_t2,
           ptr,
           pos2);
       if (b)
-        return true;
+      {
+        uint64_t *ptr1 = md_bm_region;
+        size_t shift_size_t = pos * (size_t)4U;
+        bool r1 = Utils2_is_empty_s(size_class, ptr1 + shift_size_t);
+        bool cond = r1;
+        if (cond)
+        {
+          uint8_t *ptr1 = slab_region;
+          size_t page_size_t = (size_t)4096U;
+          size_t shift_size_t = pos * page_size_t;
+          mmap_trap(ptr1 + shift_size_t, (size_t)4096U);
+          tuple4 idxs = update_quarantine2(md_region, idx1_, idx5_, idx6_, idx7_);
+          size_t v = ArrayList_remove(md_region, idx3_, pos);
+          size_t idx3_ = v;
+          ArrayList_cell cell = { .prev = (size_t)16777217U, .next = idxs.y, .data = 4U };
+          md_region[pos] = cell;
+          if (idxs.y != (size_t)16777217U)
+          {
+            ArrayList_cell cell1 = md_region[idxs.y];
+            ArrayList_cell cell2 = { .prev = pos, .next = cell1.next, .data = cell1.data };
+            md_region[idxs.y] = cell2;
+          }
+          size_t tl_;
+          if (idxs.y == (size_t)16777217U)
+            tl_ = pos;
+          else
+            tl_ = idxs.z;
+          size_t sz_ = idxs.w + (size_t)1U;
+          ArrayListGen_tuple2 idxs_ = { .x1 = tl_, .y1 = sz_ };
+          update_quarantine3(slab_region, idx7_, idxs);
+          r_idxs[0U] = idxs.x;
+          r_idxs[2U] = idx3_;
+          r_idxs[4U] = pos;
+          r_idxs[5U] = idxs_.x1;
+          r_idxs[6U] = idxs_.y1;
+          return b;
+        }
+        else
+        {
+          size_t v = ArrayList_remove(md_region, idx3_, pos);
+          size_t idx3_ = v;
+          ArrayList_insert(md_region, idx2_, pos, 1U);
+          r_idxs[2U] = idx3_;
+          r_idxs[1U] = pos;
+          return b;
+        }
+      }
       else
         return b;
     }
     else if (status1 == 1U)
     {
       uint8_t *ptr10 = slab_region;
-      size_t page_size_t = (size_t)4096U;
-      size_t shift_size_t0 = pos * page_size_t;
+      size_t page_size_t0 = (size_t)4096U;
+      size_t shift_size_t0 = pos * page_size_t0;
       uint64_t *ptr11 = md_bm_region;
       size_t shift_size_t1 = pos * (size_t)4U;
-      uint64_t *ptr1 = md_bm_region_q;
-      size_t shift_size_t = pos * (size_t)4U;
+      uint64_t *ptr12 = md_bm_region_q;
+      size_t shift_size_t2 = pos * (size_t)4U;
       bool
       b =
         SlotsFree_deallocate_slot(size_class,
           ptr10 + shift_size_t0,
           ptr11 + shift_size_t1,
-          ptr1 + shift_size_t,
+          ptr12 + shift_size_t2,
           ptr,
           pos2);
       if (b)
-        return true;
+      {
+        uint64_t *ptr1 = md_bm_region;
+        size_t shift_size_t = pos * (size_t)4U;
+        bool r1 = Utils2_is_empty_s(size_class, ptr1 + shift_size_t);
+        bool cond = r1;
+        if (cond)
+        {
+          uint8_t *ptr1 = slab_region;
+          size_t page_size_t = (size_t)4096U;
+          size_t shift_size_t = pos * page_size_t;
+          mmap_trap(ptr1 + shift_size_t, (size_t)4096U);
+          tuple4 idxs = update_quarantine2(md_region, idx1_, idx5_, idx6_, idx7_);
+          size_t v = ArrayList_remove(md_region, idx2_, pos);
+          size_t idx2_ = v;
+          ArrayList_cell cell = { .prev = (size_t)16777217U, .next = idxs.y, .data = 4U };
+          md_region[pos] = cell;
+          if (idxs.y != (size_t)16777217U)
+          {
+            ArrayList_cell cell1 = md_region[idxs.y];
+            ArrayList_cell cell2 = { .prev = pos, .next = cell1.next, .data = cell1.data };
+            md_region[idxs.y] = cell2;
+          }
+          size_t tl_;
+          if (idxs.y == (size_t)16777217U)
+            tl_ = pos;
+          else
+            tl_ = idxs.z;
+          size_t sz_ = idxs.w + (size_t)1U;
+          ArrayListGen_tuple2 idxs_ = { .x1 = tl_, .y1 = sz_ };
+          update_quarantine3(slab_region, idx7_, idxs);
+          r_idxs[0U] = idxs.x;
+          r_idxs[1U] = idx2_;
+          r_idxs[4U] = pos;
+          r_idxs[5U] = idxs_.x1;
+          r_idxs[6U] = idxs_.y1;
+          return b;
+        }
+        else
+          return b;
+      }
       else
         return b;
     }

diff --git a/dist/internal/ArrayList.h b/dist/internal/ArrayList.h
@@ -16,6 +16,13 @@ typedef struct ArrayListGen_tuple3_s
 }
 ArrayListGen_tuple3;
 
+typedef struct ArrayListGen_tuple2_s
+{
+  size_t x1;
+  size_t y1;
+}
+ArrayListGen_tuple2;
+
 uint32_t ArrayList_read_in_place(ArrayList_cell *r, size_t idx);
 
 size_t ArrayList_remove(ArrayList_cell *r, size_t hd1, size_t idx);

diff --git a/src/Config.fst b/src/Config.fst
@@ -150,7 +150,7 @@ let guard_pages_interval = 2sz
 
 // quarantine
 let enable_quarantine = true
-let enable_quarantine_slot = true
+let enable_quarantine_slot = false
 let enable_quarantine_trap = true
 let enable_quarantine_strict_trap = false
 let quarantine_queue_length = 1024sz