//! A circular doubly-linked list of power-of-two-sized subregions.

use contracts::{ensures, requires};
use core::{fmt, ptr::NonNull};

/// The magic number a non-sentinel node should have.
const FREE_NODE_MAGIC: u64 = u64::from_ne_bytes(*b"FREENODE");

/// The magic number set into the spot for a node's magic number when it is initialized, but not
/// linked into a list.
const INITED_NODE_MAGIC: u64 = u64::from_ne_bytes(*b"NODEINIT");

/// The magic number a sentinel node should have.
const SENTINEL_MAGIC: u64 = u64::from_ne_bytes(*b"SENTINEL");

/// The magic number set into the spot for a node's magic number when it gets unlinked.
const USED_NODE_MAGIC: u64 = u64::from_ne_bytes(*b"ALLOC'ED");

/// A pointer to the sentinel node of a circular doubly-linked list of power-of-two-sized subregions.
pub struct FreeList(NonNull<FreeListNode>);

impl FreeList {
    /// Creates a free-list wrapper for a sentinel node's pointer.
    ///
    /// # Safety
    ///
    /// - `sentinel` must be a pointer to the sentinel of a valid circular doubly-linked list.
    #[requires(unsafe { (*sentinel.as_ptr()).next }.is_some())]
    #[requires(unsafe { (*sentinel.as_ptr()).prev }.is_some())]
    #[requires(unsafe { (*sentinel.as_ptr()).magic } == SENTINEL_MAGIC)]
    #[requires(unsafe { (*sentinel.as_ptr()).self_addr } == sentinel.as_ptr() as usize)]
    pub unsafe fn from_sentinel(sentinel: NonNull<FreeListNode>) -> FreeList {
        FreeList(sentinel)
    }

    /// Returns whether the free-list is empty.
    pub fn is_empty(&self) -> bool {
        let sentinel = self.0.as_ptr();
        // SAFETY: This is sound as long as the sentinel was valid, which is a precondition of
        // `FreeList::from_sentinel()`.
        unsafe {
            // UNWRAP: This is a precondition of the method.
            let next = (*sentinel).next.unwrap();
            (*sentinel).self_addr == next.as_ptr() as usize
        }
    }

    /// Pops a subregion from the free-list, returning ownership to the caller.
    pub fn pop(&mut self) -> Option<NonNull<u8>> {
        if self.is_empty() {
            // If the list is empty, return `None`.
            None
        } else {
            // SAFETY: This is sound as long as the sentinel was valid, which is a precondition of
            // `FreeList::from_sentinel()`.
            unsafe {
                // UNWRAP: In a valid circular doubly-linked list, the pointers are all non-null.
                let node = (*self.0.as_ptr()).next.unwrap();
                Some(FreeListNode::unlink(node))
            }
        }
    }

    /// Pushes a subregion into the free-list.
    ///
    /// # Safety
    ///
    /// - `subregion_ptr` must convey ownership over untyped memory of the correct size.
    pub unsafe fn push(&mut self, subregion_ptr: NonNull<u8>) {
        let node = FreeListNode::init(subregion_ptr);

        let prev = self.0;
        // UNWRAP: In a valid circular doubly-linked list, the pointers are all non-null.
        let next = (*self.0.as_ptr()).next.unwrap();

        (*node.as_ptr()).prev = Some(prev);
        (*node.as_ptr()).next = Some(next);
        (*node.as_ptr()).magic = FREE_NODE_MAGIC;

        (*prev.as_ptr()).next = Some(node);
        (*next.as_ptr()).prev = Some(node);
    }
}

impl fmt::Debug for FreeList {
    fn fmt(&self, fmt: &mut fmt::Formatter) -> fmt::Result {
        // SAFETY: This is sound as long as the sentinel was valid, which is a precondition of
        // `FreeList::from_sentinel()`.
        let sentinel_addr = unsafe { (*self.0.as_ptr()).self_addr };

        let mut fmt = fmt.debug_list();
        let mut ptr = self.0;
        loop {
            // SAFETY: The invariants of FreeList guarantee that the list is valid. In a valid
            // list, the next pointer is always valid and non-null.
            ptr = unsafe { (*ptr.as_ptr()).next.unwrap() };
            if unsafe { (*ptr.as_ptr()).self_addr } == sentinel_addr {
                break fmt.finish();
            }
            fmt.entry(&ptr);
        }
    }
}

/// A node in a free list. This should not be moved without careful thought.
///
/// This type is valid when zero-initialized.
///
/// # Safety
///
/// - This type is valid only if it is zero-initialized or if it contains a valid circular
///   doubly-linked list of subregions of the correct size, which it owns.
#[derive(Debug)]
pub struct FreeListNode {
    next: Option<NonNull<FreeListNode>>,
    prev: Option<NonNull<FreeListNode>>,
    magic: u64,
    self_addr: usize,
}

impl FreeListNode {
    /// Initializes a sentinel node.
    ///
    /// # Safety
    ///
    /// The pointer must convey exclusive access and point to a large-enough allocation.
    #[ensures(unsafe { (*ptr.as_ptr()).magic } == SENTINEL_MAGIC)]
    #[ensures(unsafe { (*ptr.as_ptr()).self_addr } == ptr.as_ptr() as usize)]
    pub unsafe fn init_sentinel(ptr: NonNull<FreeListNode>) {
        (*ptr.as_ptr()).next = Some(ptr);
        (*ptr.as_ptr()).prev = Some(ptr);
        (*ptr.as_ptr()).magic = SENTINEL_MAGIC;
        (*ptr.as_ptr()).self_addr = ptr.as_ptr() as usize;
    }

    /// Initializes a non-sentinel node.
    ///
    /// # Safety
    ///
    /// The pointer must convey ownership and point to a large-enough allocation.
    #[ensures(ptr.as_ptr() as usize == ret.as_ptr() as usize)]
    #[ensures(unsafe { (*ret.as_ptr()).magic } == INITED_NODE_MAGIC)]
    #[ensures(unsafe { (*ret.as_ptr()).self_addr } == ptr.as_ptr() as usize)]
    unsafe fn init(ptr: NonNull<u8>) -> NonNull<FreeListNode> {
        let ptr = ptr.cast();
        ptr.write(FreeListNode {
            next: None,
            prev: None,
            magic: INITED_NODE_MAGIC,
            self_addr: ptr.as_ptr() as usize,
        });
        ptr
    }

    /// Unlinks the node from the circular doubly-linked list.
    ///
    /// # Safety
    ///
    /// The pointer must be a non-sentinel node inside a valid free list.
    #[requires(unsafe { (*node.as_ptr()).magic } == FREE_NODE_MAGIC)]
    #[requires(unsafe { (*node.as_ptr()).self_addr } == node.as_ptr() as usize)]
    pub unsafe fn unlink(node: NonNull<FreeListNode>) -> NonNull<u8> {
        // UNWRAP: In a valid circular doubly-linked list, the pointers are all non-null.
        let prev = (*node.as_ptr()).prev.unwrap();
        let next = (*node.as_ptr()).next.unwrap();

        (*prev.as_ptr()).next = Some(next);
        (*next.as_ptr()).prev = Some(prev);

        (*node.as_ptr()).next = None;
        (*node.as_ptr()).prev = None;
        (*node.as_ptr()).magic = USED_NODE_MAGIC;
        node.cast()
    }
}