//! Final ownership and interval checks over published kernel objects.

use kernel::abi;

use kernel::boot;

use kernel::slots;

use kernel::capability;

use kernel::domains;

use kernel::budgets;

use kernel::interrupts;

use kernel::sync;

/// Select authoritative capability storage, including the fixture's boot owner.

/// The bootstrap table and domain memory must outlive the metadata transaction.

unsafe fn table(owner: abi::Ref, bootstrap: &capability::Table) -> *unsafe capability::Table {

    if owner == bootstrap.owner { return bootstrap as *unsafe capability::Table; }

    let domain = try! domains::get(&domains::STORE, owner);

    assert domain.state <> domains::Lifecycle::Dead;

    assert domain.memory.table.owner == owner;

    return &domain.memory.table;

}

/// Check live references, exclusive execution ownership, and disjoint CPU windows.

/// Each budget or IRQ check uses a separate bounded metadata transaction.

export unsafe fn check(bootstrap: &capability::Table) {

    let guard = sync::enter();

    let mut occupied: u32 = 0;

    for i in 0..domains::STORE.contextSlots.len {

        if domains::STORE.contextSlots[i].state <> slots::State::Live { continue; }

        let context = domains::STORE.contexts[i];

        let owner = try! domains::get(&domains::STORE, context.owner);

        assert owner.state <> domains::Lifecycle::Dead;

        if let hart = context.hart {

            assert hart < 8 and (boot::PLATFORM.harts & (1 << hart)) <> 0;

            assert (occupied & (1 << hart)) == 0;

            set occupied |= 1 << hart;

        }

    }

    sync::leave(guard);

    for i in 0..budgets::STORE.slots.len {

        let guard = sync::enter();

        if budgets::STORE.slots[i].state == slots::State::Live {

            let object = abi::Ref { index: i, generation: budgets::STORE.slots[i].generation };

            let window = try! budgets::get(&budgets::STORE, object);

            assert window.start < window.end and window.hart < 8;

            assert (boot::PLATFORM.harts & (1 << window.hart)) <> 0;

            let owner = table(window.owner, bootstrap);

            let entry = try! capability::get(&*owner, window.handle);

            assert entry.kind == abi::Kind::Budget and entry.object == object;

            if let context = window.context {

                let bound = try! domains::context(&domains::STORE, window.owner, context);

                assert bound.owner == window.owner;

            }

            for j in i + 1..budgets::STORE.slots.len {

                if budgets::STORE.slots[j].state <> slots::State::Live { continue; }

                let other = budgets::STORE.windows[j];

                if other.hart == window.hart {

                    assert window.end <= other.start or other.end <= window.start;

                }

            }

        }

        sync::leave(guard);

    }

    for i in 0..interrupts::STORE.count {

        let guard = sync::enter();

        if interrupts::STORE.slots[i].state == slots::State::Live {

            let object = abi::Ref { index: i, generation: interrupts::STORE.slots[i].generation };

            let irq = try! interrupts::get(&interrupts::STORE, object);

            let owner = table(irq.owner, bootstrap);

            let entry = try! capability::get(&*owner, irq.handle);

            assert entry.kind == abi::Kind::Interrupt and entry.object == object;

        }

        sync::leave(guard);

    }

}