Merge pull request #12 from Inria-Prosecco/areitz/tweak-dist

WIP: dist/ tweaks
Inria-Prosecco · Jun 24, 2024 · e897e99 · e897e99
2 parents f8024fa + 37db6e8
commit e897e99
Show file tree

Hide file tree

Showing 9 changed files with 22 additions and 42 deletions.
diff --git a/dist/ArrayList.c b/dist/ArrayList.c
@@ -42,37 +42,19 @@ void ArrayList_insert(ArrayList_cell *r, size_t hd, size_t idx, uint32_t v)
   }
 }
 
-static void extend_insert_aux__uint32_t(ArrayList_cell *r, size_t k, size_t i, uint32_t v1)
-{
-  ArrayList_cell cell1 = { .prev = (size_t)16777217U, .next = k + i, .data = v1 };
-  r[k + i + (size_t)1U] = cell1;
-  if (k + i != (size_t)16777217U)
-  {
-    ArrayList_cell cell2 = r[k + i];
-    ArrayList_cell cell3 = { .prev = k + i + (size_t)1U, .next = cell2.next, .data = cell2.data };
-    r[k + i] = cell3;
-  }
-}
-
-static void extend_insert_aux2__uint32_t(ArrayList_cell *r, size_t k, size_t i, uint32_t v1)
-{
-  extend_insert_aux__uint32_t(r, k, i, v1);
-}
-
-static void extend_insert_aux3__uint32_t(ArrayList_cell *r, size_t k, size_t i, uint32_t v1)
-{
-  extend_insert_aux2__uint32_t(r, k, i, v1);
-}
-
-static void extend_insert_aux4__uint32_t(ArrayList_cell *r, size_t k, uint32_t v1, size_t i)
-{
-  extend_insert_aux3__uint32_t(r, k, i, v1);
-}
-
 static void extend_insert__uint32_t(size_t n2, ArrayList_cell *r, size_t k, uint32_t v1)
 {
   for (size_t i = (size_t)0U; i < n2; i++)
-    extend_insert_aux4__uint32_t(r, k, v1, i);
+  {
+    ArrayList_cell cell1 = { .prev = (size_t)16777217U, .next = k + i, .data = v1 };
+    r[k + i + (size_t)1U] = cell1;
+    if (k + i != (size_t)16777217U)
+    {
+      ArrayList_cell cell2 = r[k + i];
+      ArrayList_cell cell3 = { .prev = k + i + (size_t)1U, .next = cell2.next, .data = cell2.data };
+      r[k + i] = cell3;
+    }
+  }
 }
 
 void

diff --git a/dist/Config.h b/dist/Config.h
@@ -8,8 +8,6 @@
 
 #define CONFIG_NB_SIZE_CLASSES ((size_t)27U)
 
-typedef size_t (*Config_sc_selection_f)(uint32_t x0);
-
 extern bool Config_enable_sc_fast_selection;
 
 #define CONFIG_NB_ARENAS ((size_t)4U)

diff --git a/dist/Constants.h b/dist/Constants.h
@@ -8,8 +8,6 @@
 
 extern uint32_t Constants_page_size;
 
-typedef uint32_t Constants_sc;
-
 
 #define __Constants_H_DEFINED
 #endif
diff --git a/dist/Utils2.c b/dist/Utils2.c
@@ -3,8 +3,6 @@
 
 #include "Utils2.h"
 
-typedef uint64_t *slab_metadata;
-
 uint32_t Utils2_nb_slots(uint32_t size_class)
 {
   return 4096U / size_class;

diff --git a/dist/Utils2.h b/dist/Utils2.h
@@ -6,14 +6,10 @@
 
 #include "krmllib.h"
 
-typedef void *Utils2_same_base_array;
-
 uint32_t Utils2_nb_slots(uint32_t size_class);
 
 size_t Utils2_rounding(uint32_t size_class);
 
-typedef void *Utils2_zf_b;
-
 uint64_t Utils2_full_n_aux(uint32_t bound);
 
 uint64_t Utils2_full_n(uint32_t bound);
@@ -26,10 +22,6 @@ bool Utils2_is_partial_s(uint32_t size_class, uint64_t *md);
 
 bool Utils2_is_full_s(uint32_t size_class, uint64_t *md);
 
-typedef void *Utils2_zf_u64;
-
-typedef void *Utils2_zf_u8;
-
 
 #define __Utils2_H_DEFINED
 #endif
diff --git a/lib_list/ArrayListGen.fst b/lib_list/ArrayListGen.fst
@@ -2304,6 +2304,7 @@ open Config
 #restart-solver
 
 #push-options "--compat_pre_typed_indexed_effects --query_stats --z3rlimit 50"
+inline_for_extraction noextract
 let extend_insert_aux (#a: Type)
   (#pred1 #pred2 #pred3 #pred4 #pred5: a -> prop)
   (r: A.array (cell a))
@@ -2498,6 +2499,7 @@ let lemma_upd_is_append (#a: Type0)
   Seq.lemma_split (Seq.slice s2 0 (k+i+2)) (k+1);
   ()
 
+inline_for_extraction noextract
 let extend_insert_aux2 (#a: Type0)
   (#pred1 #pred2 #pred3 #pred4 #pred5: a -> prop)
   (r: A.array (cell a){A.length r <= US.v metadata_max})
@@ -2595,6 +2597,7 @@ let extend_insert_aux2 (#a: Type0)
     v1;
   ()
 
+inline_for_extraction noextract
 let extend_insert_aux3 (#a: Type0)
   (#pred1 #pred2 #pred3 #pred4 #pred5: a -> prop)
   (r: A.array (cell a){A.length r <= US.v metadata_max})
@@ -2913,6 +2916,7 @@ let selpred_equiv_selpred2
 
 #restart-solver
 
+inline_for_extraction noextract
 let extend_insert_aux4_aux (#a: Type) (#opened: _)
   (#pred1 #pred2 #pred3 #pred4 #pred5: a -> prop)
   (r: A.array (cell a){A.length r <= US.v metadata_max})
@@ -2958,6 +2962,7 @@ let extend_insert_aux4_aux (#a: Type) (#opened: _)
 
 #restart-solver
 
+inline_for_extraction noextract
 val extend_insert_aux4 (#a: Type)
   (#pred1 #pred2 #pred3 #pred4 #pred5: a -> prop)
   (r: A.array (cell a){A.length r <= US.v metadata_max})

diff --git a/src/Config.fsti b/src/Config.fsti
@@ -20,6 +20,7 @@ inline_for_extraction
 [@ CMacro ]
 val nb_size_classes: v:US.t{US.v v > 0 /\ US.v v == L.length sc_list}
 
+noextract
 unfold type sc_selection_f = (x:U32.t) -> Pure US.t
   (requires
     U32.v x <= max_sc)

diff --git a/src/Constants.fst b/src/Constants.fst
@@ -22,6 +22,7 @@ let max_sc = U32.v page_size
 // this allows to only have a particular mechanism
 // for the first u64 of the bitmap
 // note: this mechanism does not rely on any loop!
+inline_for_extraction noextract
 let sc = x:U32.t{
   (
     U32.eq x 16ul \/

diff --git a/src/Utils2.fsti b/src/Utils2.fsti
@@ -18,10 +18,12 @@ open Constants
 let array = Steel.ST.Array.array
 let ptr = Steel.ST.Array.ptr
 
+noextract
 unfold let same_base_array (#a: Type) (arr1 arr2: array a)
   =
   A.base (A.ptr_of arr1) == A.base (A.ptr_of arr2)
 
+noextract
 unfold let slab_metadata = r:array U64.t{A.length r = 4}
 
 // abstract property that the underlying pointer v-bytes aligned
@@ -86,6 +88,7 @@ let nb_slots_correct
   assert (U32.v (U32.mul (nb_slots size_class) size_class) <= U32.v page_size)
 #pop-options
 
+noextract
 let zf_b
   (arr: Seq.seq bool)
   : prop
@@ -505,6 +508,7 @@ let zeroes_impl_empty
   (ensures is_empty size_class s)
   = ()
 
+noextract
 let zf_u64
   (arr: Seq.seq U64.t)
   : prop
@@ -532,6 +536,7 @@ let zf_u64_split
   zf_u64_slice arr 0 i;
   zf_u64_slice arr i (Seq.length arr)
 
+noextract
 let zf_u8
   (arr: Seq.seq U8.t)
   : prop