portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

libsel4: Document errors in IDL

Browse source 
Also, remove any detailed discussion of error codes from method
descriptions.

Fixes #499

Signed-off-by: Jimmy Brush <code@jimmah.com>
This commit is contained in:
Jimmy Brush 2021-08-31 12:27:33 -04:00 committed by Gerwin Klein
parent 02a5f761f7
commit 73180e0e8d
7 changed files with 2478 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

633
libsel4/arch_include/arm/interfaces/sel4arch.xml
View file

@ -16,11 +16,6 @@
Takes a VSpace capability as an argument,
and installs a reference to the invoked
<texttt text='PageTable'/> in the VSpace according to the provided virtual address.
If higher-level paging structures do not exist for the virtual address
this operation will fail, returning a seL4_FailedLookup error. If the page table
is already mapped this operation will fail, returning a seL4_InvalidCapability error. If
another object is already mapped at this level for the virtual address
this operation will fail, returning a seL4_DeleteFirst error.
</description>
<param dir="in" name="vspace" type="seL4_CPtr"
description="Capability to the VSpace which will contain the mapping.
@ -31,6 +26,33 @@
<description>
VM Attributes for the mapping. <docref>Possible values for this type are given in <autoref label="ch:vspace"/> .</docref>
</description>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists for this level in <texttt text="vspace"/> at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
On aarch64, <texttt text="vspace"/> does not have a Page Directory mapped at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="vaddr"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is not assigned to an ASID pool.
Or, <texttt text="_service"/> is already mapped in a VSpace.
</description>
</error>
</param>
</method>
<method id="ARMPageTableUnmap" name="Unmap" manual_label="pagetable_unmap">
@ -41,15 +63,62 @@
Removes the reference to the invoked <texttt text="Page Table"/> from its
containing <texttt text="Page Directory"/>.
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
A copy of the <texttt text="_service"/> capability exists.
</description>
</error>
</method>
</interface>
<interface name="seL4_ARM_IOPageTable" manual_name="I/O Page Table"
cap_description="Capability to the I/O page table being operated on.">
<method id="ARMIOPageTableMap" name="Map" condition="defined(CONFIG_TK1_SMMU)">
<description>
TODO
</description>
<param dir="in" name="iospace" type="seL4_ARM_IOSpace"/>
<param dir="in" name="ioaddr" type="seL4_Word"/>
<error name="seL4_DeleteFirst">
<description>
All required page tables are already mapped in <texttt text="iospace"/> at <texttt text="ioaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="iospace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is already mapped in an IOSpace.
</description>
</error>
</method>
<method id="ARMIOPageTableUnmap" name="Unmap" condition="defined(CONFIG_TK1_SMMU)">
<description>
TODO
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
<interface name="seL4_ARM_Page" manual_name="Page"
@ -59,14 +128,12 @@
Map a page into an address space or update the mapping attributes.
</brief>
<description>
Takes a VSpace capability, as an
argument and installs a reference
Takes a VSpace capability, as an argument and installs a reference
to the given <texttt text="Page"/> in the lowest-level unmapped paging structure
corresponding to the given address, or updates the mapping attributes if the page is
already mapped at this address. If the required paging structures are not present
this operation will fail, returning a seL4_FailedLookup error. The page must not
already be mapped through this capability in a different VSpace or at a different
address; the page may be mapped in multiple VSpaces by copying the capability.
corresponding to the given address, or updates the mapping attributes if the page is
already mapped at this address. The page must not already be mapped through this
capability in a different VSpace or at a different address; the page may be mapped
in multiple VSpaces by copying the capability.
</description>
<param dir="in" name="vspace" type="seL4_CPtr"
description="Capability to the VSpace which will contain the mapping.
@ -83,6 +150,39 @@
VM Attributes for the mapping.<docref>Possible values for this type are given in <autoref label="ch:vspace"/> .</docref>
</description>
</param>
<error name="seL4_AlignmentError">
<description>
The <texttt text="vaddr"/> is not aligned to the page size of <texttt text="_service."/>
</description>
</error>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists in <texttt text="vspace"/> at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="vspace"/> does not have a paging structure at the required level mapped at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="_service"/> is already mapped in <texttt text="vspace"/> at a different virtual address.
Or, <texttt text="vaddr"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is not assigned to an ASID pool.
Or, <texttt text="_service"/> is already mapped in a different VSpace.
</description>
</error>
</method>
<method id="ARMPageUnmap" name="Unmap">
<brief>
@ -91,17 +191,55 @@
<description>
Removes an existing mapping.
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="ARMPageMapIO" name="MapIO" condition="defined(CONFIG_TK1_SMMU)" manual_name="Map I/O">
<brief>
TODO
</brief>
<description>
TODO
</description>
<param dir="in" name="iospace" type="seL4_ARM_IOSpace"/>
<param dir="in" name="rights" type="seL4_CapRights_t"/>
<param dir="in" name="ioaddr" type="seL4_Word"/>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists in <texttt text="iospace"/> at <texttt text="ioaddr."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="iospace"/> does not have a sufficient number of IO Page Tables mapped at <texttt text="ioaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
No rights were specified in <texttt text="rights."/>
Or, the rights in the <texttt text="_service"/> capability do not include <texttt text="rights"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="iospace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is already mapped.
Or, <texttt text="_service"/> is not a page of size 4 KiB.
</description>
</error>
</method>
<method id="ARMPageClean_Data" name="Clean_Data" manual_name="Clean Data">
<brief>
@ -114,6 +252,24 @@
description="The offset, relative to the start of the page inclusive."/>
<param dir="in" name="end_offset" type="seL4_Word"
description="The offset, relative to the start of the page exclusive."/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not mapped in a VSpace.
Or, if hypervisor support is configured, the requested range overlaps the kernel physical address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start_offset"/> is greater than or equal to <texttt text="end_offset"/>.
Or, <texttt text="start_offset"/> or <texttt text="end_offset"/> exceeds the page size of <texttt text="_service"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="ARMPageInvalidate_Data" name="Invalidate_Data" manual_name="Invalidate Data">
<brief>
@ -129,6 +285,24 @@
description="The offset, relative to the start of the page inclusive."/>
<param dir="in" name="end_offset" type="seL4_Word"
description="The offset, relative to the start of the page exclusive."/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not mapped in a VSpace.
Or, if hypervisor support is configured, the requested range overlaps the kernel physical address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start_offset"/> is greater than or equal to <texttt text="end_offset"/>.
Or, <texttt text="start_offset"/> or <texttt text="end_offset"/> exceeds the page size of <texttt text="_service"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="ARMPageCleanInvalidate_Data" name="CleanInvalidate_Data"
manual_name="Clean and Invalidate Data">
@ -143,6 +317,24 @@
description="The offset, relative to the start of the page inclusive."/>
<param dir="in" name="end_offset" type="seL4_Word"
description="The offset, relative to the start of the page exclusive."/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not mapped in a VSpace.
Or, if hypervisor support is configured, the requested range overlaps the kernel physical address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start_offset"/> is greater than or equal to <texttt text="end_offset"/>.
Or, <texttt text="start_offset"/> or <texttt text="end_offset"/> exceeds the page size of <texttt text="_service"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="ARMPageUnify_Instruction" name="Unify_Instruction" manual_name="Unify Instruction">
<brief>
@ -158,6 +350,24 @@
description="The offset, relative to the start of the page inclusive."/>
<param dir="in" name="end_offset" type="seL4_Word"
description="The offset, relative to the start of the page exclusive."/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not mapped in a VSpace.
Or, if hypervisor support is configured, the requested range overlaps the kernel physical address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start_offset"/> is greater than or equal to <texttt text="end_offset"/>.
Or, <texttt text="start_offset"/> or <texttt text="end_offset"/> exceeds the page size of <texttt text="_service"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="ARMPageGetAddress" name="GetAddress" manual_name="Get Address">
<brief>
@ -173,6 +383,16 @@
of the message register and tag contents upon error.</docref>
</return>
<param dir="out" name="paddr" type="seL4_Word"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
<interface name="seL4_ARM_ASIDControl" manual_name="ASID Control"
@ -194,6 +414,41 @@
description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
<param dir="in" name="depth" type="seL4_Uint8"
description="Number of bits of index to resolve to find the destination slot."/>
<error name="seL4_DeleteFirst">
<description>
The destination slot contains a capability.
Or, there are no more ASID pools available.
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="untyped"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="untyped"/> is not the exact size of an ASID pool object.
Or, <texttt text="untyped"/> is a device untyped <docref>(see <autoref label="sec:kernmemalloc"/>).</docref>
</description>
</error>
<error name="seL4_RangeError">
<description>
The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
The <texttt text="untyped"/> has been used to retype an object.
Or, a copy of the <texttt text="untyped"/> capability exists.
</description>
</error>
</method>
</interface>
<interface name="seL4_ARM_ASIDPool" manual_name="ASID Pool"
@ -208,6 +463,22 @@
</description>
<param dir="in" name="vspace" type="seL4_CPtr"
description="The VSpace that is being assigned to an ASID pool. Must not already be assigned to an ASID pool."/>
<error name="seL4_DeleteFirst">
<description>
There are no more ASIDs available in <texttt text="_service."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is already assigned to an ASID pool.
</description>
</error>
</method>
</interface>
<interface name="seL4_ARM_VCPU" manual_name="VCPU"
@ -224,12 +495,25 @@
</description>
<param dir="in" name="tcb" type="seL4_TCB"
description="Capability to TCB to bind to a virtual CPU"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> or <texttt text="tcb"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="ARMVCPUInjectIRQ" name="InjectIRQ" condition="defined(CONFIG_ARM_HYPERVISOR_SUPPORT)"
manual_name="Inject IRQ">
<brief>
Inject an IRQ to a virtual CPU
</brief>
<description>
TODO
</description>
<param dir="in" name="virq" type="seL4_Uint16"
description="Virtual IRQ ID"/>
<param dir="in" name="priority" type="seL4_Uint8"
@ -238,26 +522,82 @@
description="IRQ group"/>
<param dir="in" name="index" type="seL4_Uint8"
description="IRQ index"/>
<error name="seL4_DeleteFirst">
<description>
The <texttt text="index"/> is in use.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RangeError">
<description>
The <texttt text="virq,"/> <texttt text="priority,"/> <texttt text="group,"/> or <texttt text="index"/> is invalid.
</description>
</error>
</method>
<method id="ARMVCPUReadReg" name="ReadRegs" condition="defined(CONFIG_ARM_HYPERVISOR_SUPPORT)"
manual_name="Read Registers">
<brief>
Read a virtual CPU register
</brief>
<description>
TODO
</description>
<param dir="in" name="field" type="seL4_Word"
description="Register to read from a VCPU"/>
<param dir="out" name="value" type="seL4_Word"
description="Returned value of the VCPU register"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="field"/> is invalid.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="ARMVCPUWriteReg" name="WriteRegs" condition="defined(CONFIG_ARM_HYPERVISOR_SUPPORT)"
manual_name="Write Registers">
<brief>
Write a virtual CPU register
</brief>
<description>
TODO
</description>
<param dir="in" name="field" type="seL4_Word"
description="Register ID to write to a VCPU"/>
<param dir="in" name="value" type="seL4_Word"
description="Value to be written to the VCPU register"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="field"/> is invalid.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="ARMVCPUAckVPPI" name="AckVPPI" condition="defined(CONFIG_ARM_HYPERVISOR_SUPPORT)"
manual_name="Acknowledge Virtual PPI IRQ">
@ -270,7 +610,21 @@
</description>
<param dir="in" name="irq" type="seL4_Word"
description="irq to ack."/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="irq"/> is invalid.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
<interface name="seL4_IRQControl" manual_name="IRQ Control" cap_description="An IRQControl capability. This gives you the authority to make this call.">
@ -289,6 +643,39 @@
<param dir="in" name="root" type="seL4_CNode" description="CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize."/>
<param dir="in" name="index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
<param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/>
<error name="seL4_DeleteFirst">
<description>
The destination slot contains a capability.
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, the platform does not support setting the IRQ trigger.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RangeError">
<description>
The <texttt text="irq"/> is invalid.
Or, <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
An IRQ handler capability for <texttt text="irq"/> has already been created.
</description>
</error>
</method>
<method id="ARMIRQIssueIRQHandlerTriggerCore" name="GetTriggerCore" manual_name="GetTriggerCore"
@ -306,6 +693,43 @@
<param dir="in" name="index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
<param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/>
<param dir="in" name="target" type="seL4_Word" description="Indicates the target core ID to which this irq will be sent."/>
<error name="seL4_DeleteFirst">
<description>
The destination slot contains a capability.
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, SMP support is not enabled.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="target"/> is invalid.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RangeError">
<description>
The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
An IRQ handler capability for <texttt text="irq"/> has already been created.
</description>
</error>
</method>
</interface>
<interface name="seL4_ARM_SIDControl" manual_name="SID Control" cap_description="A SIDControl capability. This gives you the authority to make this call.">
@ -321,6 +745,38 @@
<param dir="in" name="root" type="seL4_CNode" description="CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize."/>
<param dir="in" name="index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
<param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/>
<error name="seL4_DeleteFirst">
<description>
The destination slot contains a capability.
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RangeError">
<description>
The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="sid"/> is invalid.
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
An SID capability for <texttt text="sid"/> has already been created.
</description>
</error>
</method>
<method id="ARMSIDGetFault" name="GetFault" manual_name="GetFault"
manual_label="sid_controlgetfault" condition="defined(CONFIG_ARM_SMMU)">
@ -341,6 +797,16 @@
<param dir="out" name="status" type="seL4_Word"/>
<param dir="out" name="syndrome_0" type="seL4_Word"/>
<param dir="out" name="syndrome_1" type="seL4_Word"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="ARMSIDClearFault" name="ClearFault" manual_name="ClearFault"
manual_label="sid_controlclearfault" condition="defined(CONFIG_ARM_SMMU)">
@ -350,6 +816,16 @@
<description>
<docref>See <autoref label="sec:smmuv2-fault-handling"/>.</docref>
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
<interface name="seL4_ARM_SID" manual_name="SID" cap_description="A SID capability. This gives you the authority to make this call.">
@ -363,6 +839,22 @@
</description>
<param dir="in" name="cb" type="seL4_CPtr"
description="The CB that is being binded to a stream ID. Must already has an assigned vspace."/>
<error name="seL4_DeleteFirst">
<description>
The <texttt text="_service"/> is already bound to a context bank.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="cb"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="cb"/> is not assigned to a VSpace.
</description>
</error>
</method>
<method id="ARMSIDUnbindCB" name="UnbindCB" manual_name="UnbindCB"
manual_label="sid_unbindcb" condition="defined(CONFIG_ARM_SMMU)">
@ -372,6 +864,17 @@
<description>
<docref>See <autoref label="sec:smmuv2-configuring-streams-transactions"/>.</docref>
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not bound to a context block.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
<interface name="seL4_ARM_CBControl" manual_name="CB Control" cap_description="A CBControl capability. This gives you the authority to make this call.">
@ -387,6 +890,38 @@
<param dir="in" name="root" type="seL4_CNode" description="CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize."/>
<param dir="in" name="index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
<param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/>
<error name="seL4_DeleteFirst">
<description>
The destination slot contains a capability.
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RangeError">
<description>
The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="cb"/> is invalid.
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
A CB capability for <texttt text="cb"/> has already been created.
</description>
</error>
</method>
<method id="ARMCBTLBInvalidateAll" name="TLBInvalidateAll" manual_name="TLBInvalidateAll"
manual_label="cb_controltlbinvalidate" condition="defined(CONFIG_ARM_SMMU)">
@ -396,6 +931,16 @@
<description>
<docref>See <autoref label="sec:smmuv2-tlb-invalidation"/>.</docref>
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
<interface name="seL4_ARM_CB" manual_name="CB" cap_description="A CB capability. This gives you the authority to make this call.">
@ -409,6 +954,22 @@
</description>
<param dir="in" name="vspace" type="seL4_CPtr"
description="The VSpace that is being assigned to a context bank. Must already has an assigned ASID."/>
<error name="seL4_DeleteFirst">
<description>
The <texttt text="_service"/> is already assigned to a VSpace.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is not assigned to an ASID pool.
</description>
</error>
</method>
<method id="ARMCBUnassignVspace" name="UnassignVspace" manual_name="UnassignVspace"
manual_label="cb_unassignvspace" condition="defined(CONFIG_ARM_SMMU)">
@ -418,6 +979,17 @@
<description>
<docref>See <autoref label="sec:smmuv2-configuring-context-banks"/>.</docref>
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not assigned to a VSpace.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="ARMCBTLBInvalidate" name="TLBInvalidate" manual_name="TLBInvalidate"
manual_label="cb_tlbinvalidate" condition="defined(CONFIG_ARM_SMMU)">
@ -427,6 +999,17 @@
<description>
<docref>See <autoref label="sec:smmuv2-tlb-invalidation"/>.</docref>
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not assigned to a VSpace.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="ARMCBGetFault" name="CBGetFault" manual_name="CBGetFault"
manual_label="cb_getfault" condition="defined(CONFIG_ARM_SMMU)">
@ -445,6 +1028,16 @@
</return>
<param dir="out" name="status" type="seL4_Word"/>
<param dir="out" name="address" type="seL4_Word"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="ARMCBClearFault" name="CBClearFault" manual_name="CBClearFault"
manual_label="cb_clearfault" condition="defined(CONFIG_ARM_SMMU)">
@ -454,6 +1047,16 @@
<description>
<docref>See <autoref label="sec:smmuv2-fault-handling"/>.</docref>
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
</api>

178
libsel4/arch_include/riscv/interfaces/sel4arch.xml
View file

@ -62,6 +62,29 @@
in <autoref label="ch:vspace"/>.</docref>
</description>
</param>
<error name="seL4_DeleteFirst">
<description>
A page is mapped in <texttt text="vspace"/> at <texttt text="vaddr."/>
Or, all required page tables are already mapped in <texttt text="vspace"/> at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="vaddr"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is not assigned to an ASID pool.
Or, <texttt text="_service"/> is already mapped in a VSpace.
</description>
</error>
</method>
<method id="RISCVPageTableUnmap" name="Unmap" manual_label="pagetable_unmap">
<brief>
@ -70,6 +93,22 @@
<description>
<docref>See <autoref label="ch:vspace"/></docref>
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
The <texttt text="_service"/> is the root of a VSpace.
Or, a copy of the <texttt text="_service"/> capability exists.
</description>
</error>
</method>
</interface>
<interface name="seL4_RISCV_Page" manual_name="Page" cap_description="Capability to the page to invoke.">
@ -101,6 +140,40 @@
in <autoref label="ch:vspace"/>.</docref>
</description>
</param>
<error name="seL4_AlignmentError">
<description>
The <texttt text="vaddr"/> is not aligned to the page size of <texttt text="_service."/>
</description>
</error>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists in <texttt text="vspace"/> at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="vspace"/> does not have a paging structure at the required level mapped at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="_service"/> is already mapped in <texttt text="vspace"/> at a different virtual address.
Or, <texttt text="vaddr"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is not the root of a VSpace.
Or, <texttt text="vspace"/> is not assigned to an ASID pool.
Or, <texttt text="_service"/> is already mapped in a different VSpace.
</description>
</error>
</method>
<method id="RISCVPageUnmap" name="Unmap">
<brief>
@ -109,6 +182,16 @@
<description>
Removes an existing mapping.
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="RISCVPageGetAddress" name="GetAddress">
<brief>
@ -124,6 +207,16 @@
of the message register and tag contents upon error.</docref>
</return>
<param dir="out" name="paddr" type="seL4_Word"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
<interface name="seL4_RISCV_ASIDControl" manual_name="ASID Control"
@ -145,6 +238,41 @@
description="CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth of 32."/>
<param dir="in" name="depth" type="seL4_Uint8"
description="Number of bits of index to resolve to find the destination slot."/>
<error name="seL4_DeleteFirst">
<description>
The destination slot contains a capability.
Or, there are no more ASID pools available.
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="untyped"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="untyped"/> is not the exact size of an ASID pool object.
Or, <texttt text="untyped"/> is a device untyped <docref>(see <autoref label="sec:kernmemalloc"/>).</docref>
</description>
</error>
<error name="seL4_RangeError">
<description>
The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
The <texttt text="untyped"/> has been used to retype an object.
Or, a copy of the <texttt text="untyped"/> capability exists.
</description>
</error>
</method>
</interface>
<interface name="seL4_RISCV_ASIDPool" manual_name="ASID Pool"
@ -162,6 +290,23 @@
to an ASID pool.
</description>
</param>
<error name="seL4_DeleteFirst">
<description>
There are no more ASIDs available in <texttt text="_service."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is already assigned to an ASID pool.
Or, <texttt text="vspace"/> is mapped in a VSpace.
</description>
</error>
</method>
</interface>
<interface name="seL4_IRQControl" manual_name="IRQ Control" cap_description="An IRQControl capability. This gives you the authority to make this call.">
@ -180,6 +325,39 @@
<param dir="in" name="root" type="seL4_CNode" description="CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize."/>
<param dir="in" name="index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
<param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/>
<error name="seL4_DeleteFirst">
<description>
The destination slot contains a capability.
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, the platform does not support setting the IRQ trigger.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RangeError">
<description>
The <texttt text="irq"/> is invalid.
Or, <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
An IRQ handler capability for <texttt text="irq"/> has already been created.
</description>
</error>
</method>
</interface>

649
libsel4/arch_include/x86/interfaces/sel4arch.xml
View file

@ -33,6 +33,33 @@
VM attributes for the mapping. <docref>Possible values for this type are given in <autoref label='ch:vspace'/></docref>
</description>
</param>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists for this level in <texttt text="vspace"/> at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="vspace"/> does not have a PDPT mapped at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="vaddr"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is not assigned to an ASID pool.
Or, <texttt text="_service"/> is already mapped in a VSpace.
</description>
</error>
</method>
<method id="X86PageDirectoryUnmap" name="Unmap">
<brief>
@ -41,6 +68,21 @@
<description>
<docref>See <autoref label="ch:vspace"/></docref>
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
A copy of the <texttt text="_service"/> capability exists.
</description>
</error>
</method>
<method id="X86PageDirectoryGetStatusBits" name="GetStatusBits" manual_name="Get Status Bits" condition="defined(CONFIG_ARCH_IA32)">
<brief>
@ -56,6 +98,22 @@
<param dir="in" name="vaddr" type="seL4_Word" description='Virtual address of the page to query'/>
<param dir="out" name="accessed" type="seL4_Word"/>
<param dir="out" name="dirty" type="seL4_Word"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="_service"/> does not have a mapping at <texttt text="vaddr."/>
Or, <texttt text="vaddr"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
@ -79,6 +137,33 @@
VM attributes for the mapping. <docref>Possible values for this type are given in <autoref label='ch:vspace'/></docref>
</description>
</param>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists for this level in <texttt text="vspace"/> at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="vspace"/> does not have a Page Directory mapped at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="vaddr"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is not assigned to an ASID pool.
Or, <texttt text="_service"/> is already mapped in a VSpace.
</description>
</error>
</method>
<method id="X86PageTableUnmap" name="Unmap" manual_label="pagetable_unmap">
<brief>
@ -89,6 +174,21 @@
<texttt text="PageDirectory"/>.
<docref>See <autoref label="ch:vspace"/></docref>
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
A copy of the <texttt text="_service"/> capability exists.
</description>
</error>
</method>
</interface>
@ -105,6 +205,23 @@
description='The IOSpace to map the page table into.'/>
<param dir="in" name="ioaddr" type="seL4_Word"
description='The address to map the page table at.'/>
<error name="seL4_DeleteFirst">
<description>
All required page tables are already mapped in <texttt text="iospace"/> at <texttt text="ioaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="iospace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="iospace"/> is not assigned to a PCI device.
Or, <texttt text="_service"/> is already mapped in an IOSpace.
</description>
</error>
</method>
<method id="X86IOPageTableUnmap" name="Unmap" condition='defined(CONFIG_IOMMU)'>
<brief>
@ -114,6 +231,16 @@
<docref>See <autoref label="sec:iospace"/></docref>
</description>
<cap_param append_description='The page table to unmap.'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
@ -143,6 +270,40 @@
VM attributes for the mapping. <docref>Possible values for this type are given in <autoref label='ch:vspace'/></docref>
</description>
</param>
<error name="seL4_AlignmentError">
<description>
The <texttt text="vaddr"/> is not aligned to the page size of <texttt text="_service."/>
</description>
</error>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists in <texttt text="vspace"/> at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="vspace"/> does not have a paging structure at the required level mapped at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is already mapped in an IOSpace.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="_service"/> is already mapped in <texttt text="vspace"/> at a different virtual address.
Or, <texttt text="vaddr"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is not assigned to an ASID pool.
Or, <texttt text="_service"/> is already mapped in a different VSpace.
</description>
</error>
</method>
<method id="X86PageUnmap" name="Unmap" manual_label='page_unmap'>
<brief>
@ -151,6 +312,16 @@
<description>
Removes an existing mapping.
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="X86PageMapIO" name="MapIO" manual_name="Map I/O" manual_label='page_map_io' condition='defined(CONFIG_IOMMU)'>
<brief>
@ -168,6 +339,35 @@
</param>
<param dir="in" name="ioaddr" type="seL4_Word"
description='The address that the frame is being mapped at.'/>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists in <texttt text="iospace"/> at <texttt text="ioaddr."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="iospace"/> does not have a sufficient number of IO Page Tables mapped at <texttt text="ioaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
No rights were specified in <texttt text="rights."/>
Or, the rights in the <texttt text="_service"/> capability do not include <texttt text="rights"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="iospace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is already mapped.
Or, <texttt text="_service"/> is not a page of size 4 KiB.
Or, <texttt text="iospace"/> is not assigned to a PCI device.
</description>
</error>
</method>
<method id="X86PageGetAddress" name="GetAddress" manual_name="Get Address"
manual_label='page_getaddress'>
@ -184,12 +384,53 @@
of the message register and tag contents upon error.</docref>
</return>
<param dir="out" name="paddr" type="seL4_Word"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="X86PageMapEPT" name="MapEPT" condition="defined(CONFIG_VTX)" manual_name="Map EPT">
<description>
TODO
</description>
<param dir="in" name="vspace" type="seL4_X86_EPTPML4"/>
<param dir="in" name="vaddr" type="seL4_Word"/>
<param dir="in" name="rights" type="seL4_CapRights_t"/>
<param dir="in" name="attr" type="seL4_X86_VMAttributes"/>
<error name="seL4_AlignmentError">
<description>
The <texttt text="vaddr"/> is not aligned to the page size of <texttt text="_service."/>
</description>
</error>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists in <texttt text="vspace"/> at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="vspace"/> does not have a paging structure at the required level mapped at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is not assigned to an ASID pool.
Or, <texttt text="_service"/> is already mapped.
Or, <texttt text="_service"/> has an unsupported page size.
</description>
</error>
</method>
</interface>
@ -213,6 +454,41 @@
description='CPTR to the destination slot. Resolved from the root of the destination CSpace.'/>
<param dir="in" name="depth" type="seL4_Uint8"
description='Number of bits of index to resolve to find the destination slot.'/>
<error name="seL4_DeleteFirst">
<description>
The destination slot contains a capability.
Or, there are no more ASID pools available.
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="untyped"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="untyped"/> is not the exact size of an ASID pool object.
Or, <texttt text="untyped"/> is a device untyped <docref>(see <autoref label="sec:kernmemalloc"/>).</docref>
</description>
</error>
<error name="seL4_RangeError">
<description>
The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
The <texttt text="untyped"/> has been used to retype an object.
Or, a copy of the <texttt text="untyped"/> capability exists.
</description>
</error>
</method>
</interface>
@ -226,6 +502,22 @@
</description>
<cap_param append_description='The ASID pool which is being assigned to. Must not be full. Each ASID pool can contain 1024 entries.'/>
<param dir="in" name="vspace" type="seL4_CPtr" description='The page directory that is being assigned to an ASID pool. Must not already be assigned to an ASID pool.'/>
<error name="seL4_DeleteFirst">
<description>
There are no more ASIDs available in <texttt text="_service."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is already assigned to an ASID pool.
</description>
</error>
</method>
</interface>
@ -242,6 +534,42 @@
<param dir="in" name="root" type="seL4_CNode" description="CPTR to the CNode that forms the root of the destination CSpace."/>
<param dir="in" name="index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
<param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/>
<error name="seL4_DeleteFirst">
<description>
The destination slot contains a capability.
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="last_port"/> is less than <texttt text="first_port."/>
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RangeError">
<description>
The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
One or more ports in the requested range have already been issued.
</description>
</error>
</method>
</interface>
@ -258,6 +586,17 @@
</return>
<param dir="out" name="result" type="seL4_Uint8" />
<param dir="in" name="port" type="seL4_Uint16" description='The port to read from.'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, reading from <texttt text="port"/> is not authorized by the capability.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="X86IOPortIn16" name="In16">
<brief>
@ -271,6 +610,17 @@
</return>
<param dir="out" name="result" type="seL4_Uint16"/>
<param dir="in" name="port" type="seL4_Uint16" description='The port to read from.'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, reading from <texttt text="port"/> and <texttt text="port+1"/> is not authorized by the capability.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="X86IOPortIn32" name="In32">
<brief>
@ -284,6 +634,17 @@
</return>
<param dir="out" name="result" type="seL4_Uint32"/>
<param dir="in" name="port" type="seL4_Uint16" description='The port to read from.'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, reading from ports <texttt text="port"/> through <texttt text="port+3"/> is not authorized by the capability.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="X86IOPortOut8" name="Out8">
<brief>
@ -294,6 +655,17 @@
</description>
<param dir="in" name="port" type="seL4_Word" description='The port to write to.'/>
<param dir="in" name="data" type="seL4_Word" description='Data to write to the IO port.'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, writing to <texttt text="port"/> is not authorized by the capability.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="X86IOPortOut16" name="Out16">
<brief>
@ -304,6 +676,17 @@
</description>
<param dir="in" name="port" type="seL4_Word" description='The port to write to.'/>
<param dir="in" name="data" type="seL4_Word" description='Data to write to the IO port.'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, writing to <texttt text="port"/> and <texttt text="port+1"/> is not authorized by the capability.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="X86IOPortOut32" name="Out32">
<brief>
@ -314,6 +697,17 @@
</description>
<param dir="in" name="port" type="seL4_Word" description='The port to write to.'/>
<param dir="in" name="data" type="seL4_Word" description='Data to write to the IO port.'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, writing to ports <texttt text="port"/> through <texttt text="port+3"/> is not authorized by the capability.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
@ -340,6 +734,40 @@
<param dir="in" name="polarity" type="seL4_Word" description='Indicates whether the IOAPIC should be programmed to treat this interrupt as high or
low triggered'/>
<param dir="in" name="vector" type="seL4_Word" description='CPU vector to deliver the interrupt to.'/>
<error name="seL4_DeleteFirst">
<description>
The destination slot contains a capability.
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, an IOAPIC is not in use.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RangeError">
<description>
The <texttt text="vector,"/> <texttt text="ioapic,"/> or <texttt text="pin"/> is invalid.
Or, <texttt text="level"/> or <texttt text="polarity"/> is not 0 or 1.
Or, <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
An IRQ handler capability for <texttt text="vector"/> has already been created.
</description>
</error>
</method>
<method id="X86IRQIssueIRQHandlerMSI" name="GetMSI" manual_name="Get MSI">
<brief>
@ -359,6 +787,39 @@
<param dir="in" name="pci_func" type="seL4_Word" description='PCI function ID of the device that will generate the interrupt.'/>
<param dir="in" name="handle" type="seL4_Word" description='Value of the handle programmed into the data portion of the MSI.'/>
<param dir="in" name="vector" type="seL4_Word" description='CPU vector to deliver the interrupt to.'/>
<error name="seL4_DeleteFirst">
<description>
The destination slot contains a capability.
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, an IOAPIC is not in use.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RangeError">
<description>
The <texttt text="vector,"/> <texttt text="pic_bus,"/> <texttt text="pci_dev,"/> or <texttt text="pci_func"/> is invalid.
Or, the <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>).</docref>
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
An IRQ handler capability for <texttt text="vector"/> has already been created.
</description>
</error>
</method>
</interface>
<interface name="seL4_TCB" manual_name="TCB">
@ -371,6 +832,17 @@
</description>
<param dir="in" name="eptpml4" type="seL4_X86_EPTPML4"
description='CPTR to an EPT PML4 object to act as the guest mode vspace root'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> or <texttt text="eptpml4"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="eptpml4"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
<interface name="seL4_X86_VCPU" manual_name="VCPU" cap_description='VCPU object to operate on'>
@ -383,6 +855,16 @@
in both. <docref>See <autoref label='sec:virt'/>.</docref>
</description>
<param dir="in" name="tcb" type="seL4_TCB" description='CPTR of the TCB to bind to'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> or <texttt text="tcb"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="X86VCPUReadVMCS" name="ReadVMCS" condition="defined(CONFIG_VTX)" manual_name="Read VMCS" manual_label="vcpu_readvmcs">
<brief>
@ -403,6 +885,17 @@
description='Field to give to `vmread` instruction'/>
<param dir="out" name="value" type="seL4_Word"
description='Value returned by `vmread` instruction'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="field"/> is invalid or unsupported.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="X86VCPUWriteVMCS" name="WriteVMCS" condition="defined(CONFIG_VTX)" manual_name="Write VMCS" manual_label="vcpu_writevmcs">
<brief>
@ -430,6 +923,17 @@
description='Value to write using `vmwrite` instruction'/>
<param dir="out" name="written" type="seL4_Word"
description='Final value written using `vmwrite` after kernel validation'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="field"/> is invalid or unsupported.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="X86VCPUEnableIOPort" name="EnableIOPort" condition="defined(CONFIG_VTX)"
manual_name="Enable IO Port" manual_label="vcpu_enableioport">
@ -450,6 +954,21 @@
description='Start of the I/O port range to enable'/>
<param dir="in" name="high" type="seL4_Word"
description='Last I/O port in the range to enable'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> or <texttt text="ioPort"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="low"/> or <texttt text="high"/> IO port exceeds the range authorized by <texttt text="ioPort."/>
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="X86VCPUDisableIOPort" name="DisableIOPort" condition="defined(CONFIG_VTX)"
manual_name="Disable IO Port">
@ -464,6 +983,16 @@
description='Start of the I/O port range to disable'/>
<param dir="in" name="high" type="seL4_Word"
description='Last I/O port in the range to disable'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
<method id="X86VCPUWriteRegisters" name="WriteRegisters" condition="defined(CONFIG_VTX)"
manual_name="Write Registers">
@ -475,6 +1004,16 @@
</description>
<param dir="in" name="regs" type="seL4_VCPUContext"
description='Data structure containing the new register values.'/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
</method>
</interface>
<interface name="seL4_X86_EPTPDPT" manual_name="Extended Page Table Page Directory Page Table"
@ -495,6 +1034,27 @@
VM attributes for the mapping. <docref>Possible values for this type are given in <autoref label='ch:vspace'/></docref>
</description>
</param>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists for this level in <texttt text="eptpml4"/> at <texttt text="gpa."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="eptpml4"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="eptpml4"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is already mapped in a VSpace.
</description>
</error>
</method>
<method id="X86EPTPDPTUnmap" name="Unmap" condition="defined(CONFIG_VTX)">
<brief>
@ -503,6 +1063,21 @@
<description>
<docref>See <autoref label="ch:vspace"/></docref>
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
A copy of the <texttt text="_service"/> capability exists.
</description>
</error>
</method>
</interface>
<interface name="seL4_X86_EPTPD" manual_name="Extended Page Table Page Directory"
@ -523,6 +1098,28 @@
VM attributes for the mapping. <docref>Possible values for this type are given in <autoref label='ch:vspace'/></docref>
</description>
</param>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists for this level in <texttt text="eptpml4"/> at <texttt text="gpa."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="eptpml4"/> is not assigned to an ASID pool.
Or, <texttt text="eptpml4"/> does not have an EPTPDPT mapped at <texttt text="gpa."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="eptpml4"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is already mapped in a VSpace.
</description>
</error>
</method>
<method id="X86EPTPDUnmap" name="Unmap" condition="defined(CONFIG_VTX)">
<brief>
@ -531,6 +1128,21 @@
<description>
<docref>See <autoref label="ch:vspace"/></docref>
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
A copy of the <texttt text="_service"/> capability exists.
</description>
</error>
</method>
</interface>
<interface name="seL4_X86_EPTPT" manual_name="Extended Page Table Page Table"
@ -551,6 +1163,28 @@
VM attributes for the mapping. <docref>Possible values for this type are given in <autoref label='ch:vspace'/></docref>
</description>
</param>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists for this level in <texttt text="eptpml4"/> at <texttt text="gpa."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="eptpml4"/> is not assigned to an ASID pool.
Or, <texttt text="eptpml4"/> does not have an EPTPD mapped at <texttt text="gpa."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="eptpml4"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is already mapped in a VSpace.
</description>
</error>
</method>
<method id="X86EPTPTUnmap" name="Unmap" condition="defined(CONFIG_VTX)">
<brief>
@ -559,6 +1193,21 @@
<description>
<docref>See <autoref label="ch:vspace"/></docref>
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
A copy of the <texttt text="_service"/> capability exists.
</description>
</error>
</method>
</interface>
</api>

736
libsel4/include/interfaces/sel4.xml
View file

File diff suppressed because it is too large Load diff

88
libsel4/sel4_arch_include/aarch32/interfaces/sel4arch.xml
View file

@ -40,6 +40,28 @@
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="start"/> or <texttt text="end"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start"/> is greater than or equal to <texttt text="end"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_RangeError">
<description>
The specified range crosses a page boundary.
</description>
</error>
</method>
<method id="ARMPDInvalidate_Data" name="Invalidate_Data" manual_name="Invalidate Data" manual_label="pd_invalidate">
<brief>
@ -52,6 +74,28 @@
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="start"/> or <texttt text="end"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start"/> is greater than or equal to <texttt text="end"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_RangeError">
<description>
The specified range crosses a page boundary.
</description>
</error>
</method>
<method id="ARMPDCleanInvalidate_Data" name="CleanInvalidate_Data"
manual_name="Clean and Invalidate Data" manual_label="pd_clean_invalidate">
@ -65,6 +109,28 @@
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="start"/> or <texttt text="end"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start"/> is greater than or equal to <texttt text="end"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_RangeError">
<description>
The specified range crosses a page boundary.
</description>
</error>
</method>
<method id="ARMPDUnify_Instruction" name="Unify_Instruction" manual_name="Unify Instruction" manual_label="pd_unify_instruction">
<brief>
@ -77,6 +143,28 @@
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="start"/> or <texttt text="end"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start"/> is greater than or equal to <texttt text="end"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_RangeError">
<description>
The specified range crosses a page boundary.
</description>
</error>
</method>
</interface>
</api>

180
libsel4/sel4_arch_include/aarch64/interfaces/sel4arch.xml
View file

@ -58,6 +58,28 @@
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="end"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start"/> is greater than or equal to <texttt text="end"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_RangeError">
<description>
The specified range crosses a page boundary.
</description>
</error>
</method>
<method id="ARMVSpaceInvalidate_Data" name="Invalidate_Data"
manual_name="Invalidate Data" manual_label="vspace_invalidate">
@ -71,6 +93,28 @@
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="end"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start"/> is greater than or equal to <texttt text="end"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_RangeError">
<description>
The specified range crosses a page boundary.
</description>
</error>
</method>
<method id="ARMVSpaceCleanInvalidate_Data" name="CleanInvalidate_Data"
manual_name="Clean and Invalidate Data" manual_label="vspace_clean_invalidate">
@ -84,6 +128,28 @@
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="end"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start"/> is greater than or equal to <texttt text="end"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_RangeError">
<description>
The specified range crosses a page boundary.
</description>
</error>
</method>
<method id="ARMVSpaceUnify_Instruction" name="Unify_Instruction"
manual_name="Unify Instruction" manual_label="vspace_unify_instruction">
@ -97,6 +163,28 @@
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="end"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="start"/> is greater than or equal to <texttt text="end"/>.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="_service"/> is not assigned to an ASID pool.
</description>
</error>
<error name="seL4_RangeError">
<description>
The specified range crosses a page boundary.
</description>
</error>
</method>
</interface>
<interface name="seL4_ARM_PageUpperDirectory" manual_name="Page Upper Directory"
@ -107,10 +195,6 @@
</brief>
<description>
Map an upper page directory (level 1) to a top level translation table (level 0).
If the upper page directory is already mapped this operation will fail,
returning a seL4_InvalidCapability error. If another object is already mapped at this
level for the virtual address this operation will fail,
returning a seL4_DeleteFirst error.
</description>
<param dir="in" name="vspace" type="seL4_CPtr"
description="Top level translation table. Must be assigned to an ASID pool."/>
@ -121,9 +205,49 @@
VM Attributes for the mapping.<docref>Possible values for this type are given in <autoref label="ch:vspace"/> .</docref>
</description>
</param>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists for this level in <texttt text="vspace"/> at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="vaddr"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is not assigned to an ASID pool.
Or, <texttt text="_service"/> is already mapped in a VSpace.
</description>
</error>
</method>
<method id="ARMPageUpperDirectoryUnmap" name="Unmap"
condition="!(defined CONFIG_ARM_HYPERVISOR_SUPPORT &amp;&amp; defined CONFIG_ARM_PA_SIZE_BITS_40)">
<description>
TODO
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
A copy of the <texttt text="_service"/> capability exists.
</description>
</error>
</method>
</interface>
<interface name="seL4_ARM_PageDirectory" manual_name="Page Directory"
@ -134,12 +258,6 @@
</brief>
<description>
Map a page directory (level 2) to an upper page directory (level 1).
If an upper page directory does not exist for the virtual address this
operation will fail, returning a seL4_FailedLookup error. If the page
directory is already mapped this operation will fail,
returning a seL4_InvalidCapability error. If another object is already mapped
at this level for the virtual address this operation will
fail, returning a seL4_DeleteFirst error.
</description>
<param dir="in" name="vspace" type="seL4_CPtr"
description="Top level translation table. Must be assigned to an ASID pool."/>
@ -150,6 +268,33 @@
VM Attributes for the mapping.<docref>Possible values for this type are given in <autoref label="ch:vspace"/> .</docref>
</description>
</param>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists for this level in <texttt text="vspace"/> at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_FailedLookup">
<description>
The <texttt text="vspace"/> does not have a Page Upper Directory mapped at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="vaddr"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="vspace"/> is not assigned to an ASID pool.
Or, <texttt text="_service"/> is already mapped in a VSpace.
</description>
</error>
</method>
<method id="ARMPageDirectoryUnmap" name="Unmap">
<brief>
@ -158,6 +303,21 @@
<description>
Unmap a page directory (level 2) from an upper page directory (level 1)
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
A copy of the <texttt text="_service"/> capability exists.
</description>
</error>
</method>
</interface>
</api>

43
libsel4/sel4_arch_include/x86_64/interfaces/sel4arch.xml
View file

@ -31,11 +31,54 @@
<interface name="seL4_X86_PDPT" manual_name="PDPT">
<method id="X86PDPTMap" name="Map">
<description>
TODO
</description>
<param dir="in" name="pml4" type="seL4_X64_PML4"/>
<param dir="in" name="vaddr" type="seL4_Word"/>
<param dir="in" name="attr" type="seL4_X86_VMAttributes"/>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists for this level in <texttt text="vspace"/> at <texttt text="vaddr."/>
</description>
</error>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidArgument">
<description>
The <texttt text="vaddr"/> is in the kernel virtual address range.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> or <texttt text="pml4"/> is a CPtr to a capability of the wrong type.
Or, <texttt text="pml4"/> is not assigned to an ASID pool.
Or, <texttt text="_service"/> is already mapped in a VSpace.
</description>
</error>
</method>
<method id="X86PDPTUnmap" name="Unmap">
<description>
TODO
</description>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_InvalidCapability">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
</description>
</error>
<error name="seL4_RevokeFirst">
<description>
A copy of the <texttt text="_service"/> capability exists.
</description>
</error>
</method>
</interface>
</api>