From 2f10fa0ea21f3ae8675247fb28f219bc0bc0e1bb Mon Sep 17 00:00:00 2001 From: Antonin Reitz Date: Sun, 21 Jul 2024 00:37:17 +0200 Subject: [PATCH] refresh dist/ --- dist/Config.c | 2 +- dist/Slabs.c | 192 +++++++++++++++++++++++++++++++++++--- dist/internal/ArrayList.h | 7 ++ src/Config.fst | 2 +- 4 files changed, 188 insertions(+), 15 deletions(-) diff --git a/dist/Config.c b/dist/Config.c index 8689ed77..079708a8 100644 --- 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 index e8880993..2cf1b055 100644 --- 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 index 0cd2e981..b980fe7e 100644 --- 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 index ac3c6617..730b1bf4 100644 --- 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