add SpecBot invariant checks

Author: daanx

src/page-queue.c

@@ -246,6 +246,10 @@ static void mi_page_queue_remove(mi_page_queue_t* queue, mi_page_t* page) {
 }
 
 
+#if MI_DEBUG >= 3
+static bool mi_page_queue_is_consistent(const mi_page_queue_t* queue);
+#endif
+
 static void mi_page_queue_push(mi_heap_t* heap, mi_page_queue_t* queue, mi_page_t* page) {
   mi_assert_internal(mi_page_heap(page) == heap);
   mi_assert_internal(!mi_page_queue_contains(queue, page));
@@ -272,8 +276,35 @@ static void mi_page_queue_push(mi_heap_t* heap, mi_page_queue_t* queue, mi_page_
   // update direct
   mi_heap_queue_first_update(heap, queue);
   heap->page_count++;
+
+  // [specbot Q-NEW-1] first/last must be both null or both non-null (L1, O(1))
+  mi_assert_internal((queue->first == NULL) == (queue->last == NULL));
+  // [specbot Q-NEW-2] last element must have no next (L1, O(1))
+  mi_assert_internal(queue->last == NULL || queue->last->next == NULL);
+  mi_assert_expensive(mi_page_queue_is_consistent(queue));
 }
 
+#if MI_DEBUG >= 3
+// [specbot Q-NEW-3] Verify doubly-linked list forward/backward consistency (L2, O(n))
+static bool mi_page_queue_is_consistent(const mi_page_queue_t* queue) {
+  if (queue->first == NULL) return (queue->last == NULL);
+  if (queue->last == NULL) return false;
+  // forward: first -> ... -> last
+  const mi_page_t* p = queue->first;
+  const mi_page_t* prev = NULL;
+  size_t count = 0;
+  while (p != NULL) {
+    mi_assert_internal(p->prev == prev);
+    prev = p;
+    p = p->next;
+    count++;
+    if (count > 100000) return false; // cycle guard
+  }
+  mi_assert_internal(prev == queue->last);
+  return true;
+}
+#endif
+
 static void mi_page_queue_move_to_front(mi_heap_t* heap, mi_page_queue_t* queue, mi_page_t* page) {
   mi_assert_internal(mi_page_heap(page) == heap);
   mi_assert_internal(mi_page_queue_contains(queue, page));

src/page.c

@@ -79,9 +79,17 @@ static bool mi_page_list_is_valid(mi_page_t* page, mi_block_t* p) {
 
 static bool mi_page_is_valid_init(mi_page_t* page) {
   mi_assert_internal(mi_page_block_size(page) > 0);
+  
   mi_assert_internal(page->used <= page->capacity);
   mi_assert_internal(page->capacity <= page->reserved);
 
+  // [specbot P-NEW-1] block_size_shift must be consistent with block_size (L1, O(1))
+  mi_assert_internal(page->block_size_shift == 0 || (mi_page_block_size(page) == ((size_t)1 << page->block_size_shift)));
+  // [specbot P-NEW-2] capacity must be nonzero when blocks are in use (L1, O(1))
+  mi_assert_internal(page->used == 0 || page->capacity > 0);
+  // [specbot P-NEW-4] page_start must be non-null when capacity > 0 (L1, O(1))
+  mi_assert_internal(page->capacity == 0 || mi_page_start(page) != NULL);
+
   uint8_t* start = mi_page_start(page);
   mi_assert_internal(start == _mi_segment_page_start(_mi_page_segment(page), page, NULL));
   mi_assert_internal(page->is_huge == (_mi_page_segment(page)->kind == MI_SEGMENT_HUGE));
@@ -90,6 +98,18 @@ static bool mi_page_is_valid_init(mi_page_t* page) {
   mi_assert_internal(mi_page_list_is_valid(page,page->free));
   mi_assert_internal(mi_page_list_is_valid(page,page->local_free));
 
+  // [specbot P-NEW-7] All free list blocks are aligned to block_size (L2, O(n))
+  {
+    size_t bsize = mi_page_block_size(page);
+    uint8_t* pstart = mi_page_start(page);
+    for (mi_block_t* b = page->free; b != NULL; b = mi_block_next(page, b)) {
+      mi_assert_internal(((uint8_t*)b - pstart) % bsize == 0);
+    }
+    for (mi_block_t* b = page->local_free; b != NULL; b = mi_block_next(page, b)) {
+      mi_assert_internal(((uint8_t*)b - pstart) % bsize == 0);
+    }
+  }
+
   #if MI_DEBUG>3 // generally too expensive to check this
   if (page->free_is_zero) {
     const size_t ubsize = mi_page_usable_block_size(page);
@@ -122,6 +142,9 @@ bool _mi_page_is_valid(mi_page_t* page) {
   if (mi_page_heap(page)!=NULL) {
     mi_segment_t* segment = _mi_page_segment(page);
 
+    // [specbot P-NEW-6] heap_tag must match owning heap's tag (L1, O(1))
+    mi_assert_internal(page->heap_tag == mi_page_heap(page)->tag);
+
     mi_assert_internal(!_mi_process_is_initialized || segment->thread_id==0 || segment->thread_id == mi_page_heap(page)->thread_id);
     #if MI_HUGE_PAGE_ABANDON
     if (segment->kind != MI_SEGMENT_HUGE)

src/segment.c

@@ -275,13 +275,23 @@ static bool mi_segment_is_valid(mi_segment_t* segment, mi_segments_tld_t* tld) {
   mi_assert_internal(segment->abandoned <= segment->used);
   mi_assert_internal(segment->thread_id == 0 || segment->thread_id == _mi_thread_id());
   mi_assert_internal(mi_commit_mask_all_set(&segment->commit_mask, &segment->purge_mask)); // can only decommit committed blocks
+
+  // [specbot S-NEW-1] segment must have at least one slice (L1, O(1))
+  mi_assert_internal(segment->segment_slices > 0);
+  // [specbot S-NEW-2] info slices must leave room for at least one data slice (L1, O(1))
+  mi_assert_internal(segment->segment_info_slices < segment->segment_slices);
+  // [specbot S-NEW-3] slice_entries must not exceed array bounds (L1, O(1))
+  mi_assert_internal(segment->slice_entries <= MI_SLICES_PER_SEGMENT);
+
   //mi_assert_internal(segment->segment_info_size % MI_SEGMENT_SLICE_SIZE == 0);
   mi_slice_t* slice = &segment->slices[0];
   const mi_slice_t* end = mi_segment_slices_end(segment);
   size_t used_count = 0;
+  size_t total_slice_count = 0;
   mi_span_queue_t* sq;
   while(slice < end) {
     mi_assert_internal(slice->slice_count > 0);
+    total_slice_count += slice->slice_count;
     mi_assert_internal(slice->slice_offset == 0);
     size_t index = mi_slice_index(slice);
     size_t maxindex = (index + slice->slice_count >= segment->slice_entries ? segment->slice_entries : index + slice->slice_count) - 1;
@@ -316,6 +326,8 @@ static bool mi_segment_is_valid(mi_segment_t* segment, mi_segments_tld_t* tld) {
     slice = &segment->slices[maxindex+1];
   }
   mi_assert_internal(slice == end);
+  // [specbot S-NEW-5] Total slice counts must sum to segment_slices (L2, O(n))
+  mi_assert_internal(total_slice_count == segment->segment_slices);
   mi_assert_internal(used_count == segment->used + 1);
   return true;
 }