Correct exported functions that were still defined as 'static inline' to
use LIBSEL4_INLINE_FUNC so that they can be controlled by
LibSel4FunctionAttributes.
This is important to other languages that want to bind to the libsel4
static library instead of using the inline C functions.
- renamed an architecture label so that it begins with ARM.
- changed setIRQTrigger so that it takes a boolean value instead of an int.
- Arch_decodeIRQControlInvocation converts the second argument (trigger)
to a boolean immediately.
Add a new invocation which allows an irq handler capability to be
obtained with a specific trigger method (edge or level). Obtaining
this capability modifies the GIC state.
This change updates the vspace chapter to separate the high-level concept of a VSpace from the
architectually defined objects. It also updates the various names for the vspace parameter to all be
vspace.
- increases the maintainability of the docs
- move descriptions of methods to the API reference
- remove hardcoded invocations in manual
This commit removes the content completely from vspace.tex, as it is out of date and needs
restructuring. The next commit does the restructuring.
Introduced a new Doxygen XML tag '<docref>'. The intention of
this tag is to indicate a section of text in the Doxygen XML that
will contain a reference to another section in the Manual e.g.
"See \autoref<sec:x>". As other generation formats aren't aware of
other chapters/sections in the manual, the <docref> encapsulation
allows it to omit the text from the output. The Latex generator
has been modified to continue parsing the 'docref' contents.
Changes the way IO ports work such that instead of 'minting' IO port caps down into new
IO port caps with smaller ranges new IO port ranges must be allocated centrally from
an IO port control cap. This mechanism acts in a very similar fashion as IRQ handler/control
capabilities and ensures that allocated IO ports do not overlap. Disallowing overlapping
IO ports is necessary to ensure the CDT remains valid as capabilities are deleted.
The GetStatusBits invocation is only implemented on ia32. Adding the condition to the
XML list prevents the invocation from being in the list of invocations on x86_64, when
it has no implementation.
Using the bitfield generator to treat guards and badges as a union type can be convenient,
but it requires reserving a bit in the data for the bitfield run time type information.
This type information is not needed by the kernel as it knows implicitly whether the passed
data is a badge or a guard based on the kind of cap being operated on. However, with the
type information present we cannot pass a word sized piece of data to the kernel.
The solution here is to go back to using a plain seL4_Word as the type for invocations
that want a capdata and let the user either construct a badge as a plain word, or use
the seL4_CNode_CapData bitfield for constructing a guard, although they have to manually extract
the word representation out of it.
This provides documentation for kernel design of the x86 virtualisation, the additional
syscall and object invocations. The ARM design is not fully expanded.
Fixes an inconsistency between manual_label for the x86 AsidPool_Assign invocation
and its reference in the manual. This makes the x86 align with the ARM name.
Nested structs with attributes are not understandable by the C parser. This change simply
moves the nested definitions into the global namespace (with suitable names).
The IOMMU implementation is not going to be verified at the moment, and so the code for
it needs to be hidden from verification, which we do by #ifdef'ing it out if the IOMMU
is not enabled. As a result the IOMMU configuration depends on a non verification target
- when CONFIG_DEBUG is enabled, track all threads
- when CONFIG_PRINTING is enabled, provide seL4_DebugDumpScheduler which
allows the user to dump the state of the kernel scheduler.
There is no way to know how many entries the syscall log contains
otherwise. One option was iterating through until finding a 0
terminator, however this requires the log to be zeroed before each
trial. This changes the FinalizeLog syscall to return the number of
entries.
Previously the #ifdefs for some debug syscalls relied on definitions
from Makefile.flags in sel4_tools. This changes them to use configs
defined in autoconf.h which makes them easier to import when building
projects that don't use sel4_tools.
CONFIG_LIB_SEL4_PUBLIC_SYMBOLS=y will disable inlining for external
interfaces (except deprecated functions), thereby providing public
symbols for easy linkage with other languages.
This also moves the description of TCBSetEPTRoot from the general object
invocation xml file to the x86-specific one to prevent the need for
documentation-generating scripts to distinguish between VTX (ie. x86)
invocations, and truly architecture independent invocations.
JIRA: SELFOUR-606
This change
* changes seL4_CapRights from the kernel to be seL4_CapRights_t in
libsel4
* deprecates the duplicated seL4_CapRights in libsel4, which is
now the bitfield generated type seL4_CapRights_t.
* fixes all usages in kernel and libsel4
Impact: for verification, this will require the type to change name
from cap_rights to seL4_CapRights_t.
This is a breaking libsel4 API change, although most code uses
seL4_AllRights or similar constants, which will not break
at a source level as these constants have been updated.
This is a *breaking API change*
This commit:
* makes seL4_Fault_tag_t common between the kernel and libsel4
* deprecates the existing functions from sel4/messages.h includes
* introduces a new fault API in sel4/faults.h and
* sel4/sel4_arch/faults.h
* deprecates seL4_GetTag(), as the function did not work without
the user calling seL4_SetTag() first (seL4_MessageInfo is passed
in registers and not set in the IPC buffer)
* removes previously deprecated functions (deprecated prior to 3.0.0)
* updates the seL4 manual to reflect the changes
Prior to this commit faults were separate
per architecture. This commit extracts the common
fault types and introduces arch specific faults,
reducing code duplication across architectures.
This commit adds support for using the ThreadID registers of the ARM MPCore
platforms for storing the address of the IPC buffer instead of the globals
frame. The choice of using the user readable/writeable ThreadID register
is chosen, even though it means the user cannot use it for its own
purposes, as it leaves room in the future for doing TLS support in the
user read only register, where compilers expect it.
This commit implements the body of SELFOUR-499. The API exposes the x86 DR0-7
and ARM coprocessor 14 features to userspace by virtualizing them as context-
switched registers in the TCB. Implemented as TCB invocations. This feature is
only built when CONFIG_HARDWARE_DEBUG_API is selected.
* Add low-level support routines for setting, unsetting, getting, enabling
and disabling breakpoints.
* Add support for single-stepping as well.
^ Single-stepping is not supported on ARMv6 since the hardware
doesn't have support.
^ ARM implements single-stepping as instruction breakpoints
configured to fault on every instruction -- this is achieved through
the "mismatch" mode, which is only supported from ARMv7 onwards.
* Also support explicit software break requests, a la "BKPT" and "INT $3".
* New invocations:
* seL4_TCB_SetBreakpoint().
* seL4_TCB_GetBreakpoint().
* seL4_TCB_UnsetBreakpoint().
* seL4_TCB_ConfigureSingleStepping().
* New constants:
^ Event types:
^ seL4_InstructionBreakpoint.
^ seL4_DataBreakpoint.
^ seL4_SoftwareBreakRequest.
^ Access types:
^ seL4_BreakOnRead.
^ seL4_BreakOnWrite.
^ seL4_BreakOnReadWrite.
^ Exports:
^ seL4_NumHWBreakpoints.
^ seL4_NumExclusiveBreakpoints.
^ seL4_NumExclusiveWatchpoints.
^ seL4_NumDualFunctionMonitors.
^ seL4_FirstBreakpoint.
^ seL4_FirstWatchpoint.
^ seL4_FirstDualFunctionMonitor.
See documentation in the seL4 API manual.
Rename all functions, constants and types in libsel4 that are in the
general x86 architecture to have an X86 name instead of an IA32 name.
As libsel4 and the kernel share names this requires changing those
in the kernel as well.
All the original IA32 names can still be used for the moment, but are
marked as deprecated.
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
Moving the section and super section objects to the aarch32 mode headers caused the
object orders to be reordered, which breaks verification. This commit undoes this
until it can either be verified or refactored a different way.
* commit '1a1110a0949c76a2d372e2bba6b2526898c51a68':
Modify Kconfig and Makefile for aach32 as sel4_arch libsel4: updates to include aarch32 as sel4_arch
Guarding code with #ifdef's makes even cursor testing of 'does this code compile'
difficult due to code being hidden by the pre-processor. Using config_set in
regular C if statements is performant as the compiler can trivially detect
dead code at compile time, and at -O1 and above will not even link in symbols
referenced by dead code in these blocks, so this will not bloat image size
