//! A table entry that is empty or holds a value, like `Option`, but whose
//! empty state is guaranteed to be all zero bytes. The kernel's tables are
//! one static; if every empty entry is zero, the whole static starts zero
//! and costs nothing in the kernel image (`.bss`). `Option` makes no such
//! promise (its `None` is whatever the compiler picks).

/// `#[repr(u8)]` fixes the layout: a tag byte, `Empty` being 0, then the
/// value (left uninitialised when empty).
#[cfg(not(kani))]
#[repr(u8)]
#[derive(Debug, Clone, Copy, PartialEq, Eq, Default)]
pub enum Slot<T> {
    #[default]
    Empty = 0,
    Full(T) = 1,
}

/// For the proofs, the same behaviour over `Option`: only the byte layout
/// differs, which no proof depends on, and CBMC is far faster on `Option`
/// than on an enum with an uninitialised payload.
#[cfg(kani)]
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct Slot<T>(Option<T>);

#[cfg(kani)]
impl<T> Default for Slot<T> {
    fn default() -> Self {
        Self(None)
    }
}

#[cfg(kani)]
#[allow(non_upper_case_globals, non_snake_case)]
impl<T> Slot<T> {
    pub const Empty: Self = Self(None);

    pub const fn Full(value: T) -> Self {
        Self(Some(value))
    }

    pub const fn is_full(&self) -> bool {
        self.0.is_some()
    }

    pub const fn as_ref(&self) -> Option<&T> {
        self.0.as_ref()
    }

    pub fn as_mut(&mut self) -> Option<&mut T> {
        self.0.as_mut()
    }

    pub fn take(&mut self) -> Option<T> {
        self.0.take()
    }

    pub fn set(&mut self, value: T) {
        self.0 = Some(value);
    }
}

#[cfg(kani)]
impl<T: Copy> Slot<T> {
    pub const fn get(&self) -> Option<T> {
        self.0
    }
}

#[cfg(kani)]
impl<T> From<Option<T>> for Slot<T> {
    fn from(o: Option<T>) -> Self {
        Self(o)
    }
}

#[cfg(not(kani))]
impl<T> Slot<T> {
    pub const fn is_full(&self) -> bool {
        matches!(self, Slot::Full(_))
    }

    pub const fn as_ref(&self) -> Option<&T> {
        match self {
            Slot::Full(v) => Some(v),
            Slot::Empty => None,
        }
    }

    pub fn as_mut(&mut self) -> Option<&mut T> {
        match self {
            Slot::Full(v) => Some(v),
            Slot::Empty => None,
        }
    }

    /// The value, leaving the slot empty.
    pub fn take(&mut self) -> Option<T> {
        match core::mem::replace(self, Slot::Empty) {
            Slot::Full(v) => Some(v),
            Slot::Empty => None,
        }
    }

    pub fn set(&mut self, value: T) {
        *self = Slot::Full(value);
    }
}

#[cfg(not(kani))]
impl<T: Copy> Slot<T> {
    pub const fn get(&self) -> Option<T> {
        match self {
            Slot::Full(v) => Some(*v),
            Slot::Empty => None,
        }
    }
}

#[cfg(not(kani))]
impl<T> From<Option<T>> for Slot<T> {
    fn from(o: Option<T>) -> Self {
        match o {
            Some(v) => Slot::Full(v),
            None => Slot::Empty,
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn a_slot_behaves_like_an_option() {
        let mut s: Slot<u32> = Slot::Empty;
        assert!(!s.is_full() && s.get().is_none());
        s.set(5);
        *s.as_mut().unwrap() += 1;
        assert_eq!(s.get(), Some(6));
        assert_eq!(s.take(), Some(6));
        assert_eq!(s, Slot::Empty);
        assert_eq!(Slot::from(Some(1)), Slot::Full(1));
    }
}