Restructure the x86 interrupt handling to allow for a more flexible
method of using IOAPIC and MSI interrupts. The essence of this change
is to allow for the user to pick, for both IOAPIC and MSIs, which
CPU vector to use. Additionally there is future support, in the API,
for seL4 to eventually protect MSI interrupts with the vt-d interrupt
routing tables.
API behaviour for legacy systems using the PIC is preserved
Part of SELFOUR-281
The fastpath variant of the resolveAddressBits loop does things out
of order, so we need to do the locateSlotCap early in order to make
sure that the assertion in it is available unconditionally.
Splits the locateSlot operation into locateSlotCNode (checks that
there is indeed a CNode present) and locateSlotTCB (does not). Also
add an alias for use where the CNode pointer is immediately grabbed
from a CNode cap.
The IRQ node is treated specially in the proofs at every level, so
another variant avoids any checking.
A new assertion at retype time is to ensure that retyping either
removes CNode arrays or preserves them, but doesn't cut into them.
This is done with an assertion because it's trivial to prove in the
abstract spec (where CNode arrays are single objects) and painful
elsewhere.
This commit deprecates seL4_ReplyWait, removes seL4_NBwait completely,
and changes the return type of seL4_Wait to void (seL4_Wait should be
used for notification objects, and seL4_Recv should be used where
seL4_Wait was used previously for endpoints).
Once again, we know in the abstract invariants that these must be
async endpoint caps or null caps, but this is only knowable in
haskell by asserting it.
We can't prove that the caller cap must be a reply cap or that
the frames mapped in an arbitrary address space are backed by caps
without appealing to the abstract invariants, which means yet more
assertions in haskell and work in the abstract/haskell refinement.
Consolidating to one simulator to get simulator builds running again. The
source setup is still for multiple potential targets so it remains reasonably
easy to add different architectures like x86 to the Haskell model if needed.
HaskellCPU and Alpha implementations have fallen far behind the current
kernel structure, haven't been used for years, and are not included in
the build.
Removing them to avoid confusion.
