//! Live AArch64 exercise of the bounded EL1 channel model. This probe does
//! not claim a user-mode IPC syscall or blocking scheduler integration.
use super::*;
use turkos_kernel::ipc::{self, ChannelTable};
use turkos_kernel::task::Scheduler;

fn fail(reason: &str) -> ! {
    write_str("TURKOS/IPC-BASIC-ERROR: ");
    write_line(reason);
    park()
}

pub(super) fn smoke_test() -> ! {
    let mut scheduler = Scheduler::new();
    let a = scheduler
        .spawn()
        .unwrap_or_else(|_| fail("producer TaskId"));
    let b = scheduler
        .spawn()
        .unwrap_or_else(|_| fail("consumer TaskId"));
    let foreign = scheduler.spawn().unwrap_or_else(|_| fail("foreign TaskId"));
    let mut table = ChannelTable::new();
    let first = table
        .create(a, b)
        .unwrap_or_else(|_| fail("create channel"));

    if table.send(first, foreign, b"BAD") != Err(ipc::Error::WrongProducer)
        || table.send(first, a, b"ONE") != Ok(())
        || table.send(first, a, b"TWO") != Ok(())
        || table.receive(first, foreign) != Err(ipc::Error::WrongConsumer)
        || table.queued(first) != Ok(2)
    {
        fail("FIFO ownership and enqueue");
    }
    let one = table
        .receive(first, b)
        .unwrap_or_else(|_| fail("first receive"));
    let two = table
        .receive(first, b)
        .unwrap_or_else(|_| fail("second receive"));
    if one.bytes() != b"ONE" || two.bytes() != b"TWO" || table.queued(first) != Ok(0) {
        fail("FIFO message order");
    }
    write_line("TURKOS/IPC-BASIC-FIFO: FIRST=ONE SECOND=TWO FOREIGN=REJECT");

    if table.send(first, a, &[b'X'; ipc::MAX_MESSAGE_BYTES]) != Ok(())
        || table.send(first, a, &[b'Y'; ipc::MAX_MESSAGE_BYTES + 1]) != Err(ipc::Error::TooLarge)
        || table.queued(first) != Ok(1)
        || table
            .receive(first, b)
            .unwrap_or_else(|_| fail("bounded receive"))
            .bytes()
            != &[b'X'; ipc::MAX_MESSAGE_BYTES]
    {
        fail("bounded message is failure atomic");
    }
    write_str("TURKOS/IPC-BASIC-LIMIT: ACCEPTED=0x");
    write_hex(ipc::MAX_MESSAGE_BYTES);
    write_str(" REJECTED=0x");
    write_hex(ipc::MAX_MESSAGE_BYTES + 1);
    write_str(" QUEUE-UNCHANGED=PASS\r\n");

    if table.send(first, a, b"") != Ok(()) || table.queued(first) != Ok(1) {
        fail("zero message enqueue");
    }
    let zero = table
        .receive(first, b)
        .unwrap_or_else(|_| fail("zero message receive"));
    if !zero.is_empty() || zero.len() != 0 || table.queued(first) != Ok(0) {
        fail("zero message lost");
    }
    write_line("TURKOS/IPC-BASIC-ZERO: QUEUED=0x0000000000000001 RECEIVED=0x0000000000000000");

    if table.close_receiver(first, foreign) != Err(ipc::Error::WrongConsumer)
        || table.close_receiver(first, b) != Ok(())
        || table.send(first, a, b"LATE") != Err(ipc::Error::NoReceiver)
        || table.queued(first) != Ok(0)
    {
        fail("missing receiver send");
    }
    write_line("TURKOS/IPC-BASIC-NO-RECEIVER: SEND=REJECT QUEUED=0x0000000000000000");

    if table.destroy(first, foreign) != Err(ipc::Error::WrongProducer)
        || table.destroy(first, a) != Ok(())
    {
        fail("channel owner close");
    }
    let second = table
        .create(a, b)
        .unwrap_or_else(|_| fail("recreate channel"));
    if second <= first
        || table.send(first, a, b"STALE") != Err(ipc::Error::InvalidChannel)
        || table.receive(first, b) != Err(ipc::Error::InvalidChannel)
        || table.queued(second) != Ok(0)
        || table.live_channels() != 1
    {
        fail("stale channel number reused");
    }
    write_str("TURKOS/IPC-BASIC-ID: OLD=0x");
    write_hex(first as usize);
    write_str(" NEW=0x");
    write_hex(second as usize);
    write_str(" STALE=REJECT\r\n");
    write_line("TURKOS/IPC-BASIC: PASS");
    park()
}