1<?xml version="1.0" ?>
2<!--
3     Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
4
5     SPDX-License-Identifier: BSD-2-Clause
6-->
7
8<api name="ObjectApiX86" label_prefix="x86_">
9    <struct name="seL4_VCPUContext">
10        <member name="eax"/>
11        <member name="ebx"/>
12        <member name="ecx"/>
13        <member name="edx"/>
14        <member name="esi"/>
15        <member name="edi"/>
16        <member name="ebp"/>
17    </struct>
18    <interface name="seL4_X86_PageDirectory" manual_name="Page Directory"
19        cap_description="Capability to the page directory being operated on.">
20        <method id="X86PageDirectoryMap" name="Map">
21            <brief>
22                Map a page directory.
23            </brief>
24            <description>
25                <docref>See <autoref label="ch:vspace"/></docref>
26            </description>
27            <param dir="in" name="vspace" type="seL4_CPtr"
28             description='Capability to the VSpace which will contain the mapping'/>
29            <param dir="in" name="vaddr" type="seL4_Word"
30                description='Virtual address to map the page into.'/>
31            <param dir="in" name="attr" type="seL4_X86_VMAttributes">
32                <description>
33                    VM attributes for the mapping. <docref>Possible values for this type are given in <autoref label='ch:vspace'/></docref>
34                </description>
35            </param>
36            <error name="seL4_DeleteFirst">
37                <description>
38                    A mapping already exists for this level in <texttt text="vspace"/> at <texttt text="vaddr"/>.
39                </description>
40            </error>
41            <error name="seL4_FailedLookup">
42                <description>
43                    The <texttt text="vspace"/> does not have a PDPT mapped at <texttt text="vaddr"/>.
44                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
45                </description>
46            </error>
47            <error name="seL4_IllegalOperation">
48                <description>
49                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
50                </description>
51            </error>
52            <error name="seL4_InvalidArgument">
53                <description>
54                    The <texttt text="vaddr"/> is in the kernel virtual address range.
55                </description>
56            </error>
57            <error name="seL4_InvalidCapability">
58                <description>
59                    The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
60                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
61                    Or, <texttt text="_service"/> is already mapped in a VSpace.
62                </description>
63            </error>
64        </method>
65        <method id="X86PageDirectoryUnmap" name="Unmap">
66            <brief>
67                Unmap a page directory.
68            </brief>
69            <description>
70                <docref>See <autoref label="ch:vspace"/></docref>
71            </description>
72            <error name="seL4_IllegalOperation">
73                <description>
74                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
75                </description>
76            </error>
77            <error name="seL4_InvalidCapability">
78                <description>
79                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
80                </description>
81            </error>
82            <error name="seL4_RevokeFirst">
83                <description>
84                    A copy of the <texttt text="_service"/> capability exists.
85                </description>
86            </error>
87        </method>
88        <method id="X86PageDirectoryGetStatusBits" name="GetStatusBits" manual_name="Get Status Bits" condition="defined(CONFIG_ARCH_IA32)">
89            <brief>
90                Retrieve the accessed and dirty bits of a page mapped into an address space.
91            </brief>
92            <description>
93                <docref>See <autoref label="ch:vspace"/></docref>
94            </description>
95            <return>
96                A <texttt text='seL4_X86_PageDirectory_GetStatusBits_t'/> structure.
97            </return>
98            <cap_param append_description='Capability to the address space to query.'/>
99            <param dir="in" name="vaddr" type="seL4_Word" description='Virtual address of the page to query'/>
100            <param dir="out" name="accessed" type="seL4_Word"/>
101            <param dir="out" name="dirty" type="seL4_Word"/>
102            <error name="seL4_IllegalOperation">
103                <description>
104                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
105                </description>
106            </error>
107            <error name="seL4_InvalidArgument">
108                <description>
109                    The <texttt text="_service"/> does not have a mapping at <texttt text="vaddr"/>.
110                    Or, <texttt text="vaddr"/> is in the kernel virtual address range.
111                </description>
112            </error>
113            <error name="seL4_InvalidCapability">
114                <description>
115                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
116                </description>
117            </error>
118        </method>
119    </interface>
120
121    <interface name="seL4_X86_PageTable" manual_name="Page Table"
122        cap_description="Capability to the page table being operated on.">
123        <method id="X86PageTableMap" name="Map" manual_label="pagetable_map">
124            <brief>
125                Map a page table into an address space.
126            </brief>
127            <description>
128                Takes a <texttt text='PageDirectory'/> capability as an argument,
129                and installs a reference to the invoked
130                <texttt text='PageTable'/> in a specified slot in the <texttt text="PageDirectory"/>.
131            </description>
132            <param dir="in" name="vspace" type="seL4_CPtr"
133             description='Capability to the VSpace which will contain the mapping'/>
134            <param dir="in" name="vaddr" type="seL4_Word"
135                description='Virtual address to map the page into.'/>
136            <param dir="in" name="attr" type="seL4_X86_VMAttributes">
137                <description>
138                    VM attributes for the mapping. <docref>Possible values for this type are given in <autoref label='ch:vspace'/></docref>
139                </description>
140            </param>
141            <error name="seL4_DeleteFirst">
142                <description>
143                    A mapping already exists for this level in <texttt text="vspace"/> at <texttt text="vaddr"/>.
144                </description>
145            </error>
146            <error name="seL4_FailedLookup">
147                <description>
148                    The <texttt text="vspace"/> does not have a Page Directory mapped at <texttt text="vaddr"/>.
149                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
150                </description>
151            </error>
152            <error name="seL4_IllegalOperation">
153                <description>
154                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
155                </description>
156            </error>
157            <error name="seL4_InvalidArgument">
158                <description>
159                    The <texttt text="vaddr"/> is in the kernel virtual address range.
160                </description>
161            </error>
162            <error name="seL4_InvalidCapability">
163                <description>
164                    The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
165                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
166                    Or, <texttt text="_service"/> is already mapped in a VSpace.
167                </description>
168            </error>
169        </method>
170        <method id="X86PageTableUnmap" name="Unmap" manual_label="pagetable_unmap">
171            <brief>
172                Unmap a page table from its address space and zero it out.
173            </brief>
174            <description>
175                Removes the reference to the invoked <texttt text="PageTable"/> from its containing
176                  <texttt text="PageDirectory"/>.
177                <docref>See <autoref label="ch:vspace"/></docref>
178            </description>
179            <error name="seL4_IllegalOperation">
180                <description>
181                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
182                </description>
183            </error>
184            <error name="seL4_InvalidCapability">
185                <description>
186                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
187                </description>
188            </error>
189            <error name="seL4_RevokeFirst">
190                <description>
191                    A copy of the <texttt text="_service"/> capability exists.
192                </description>
193            </error>
194        </method>
195    </interface>
196
197    <interface name="seL4_X86_IOPageTable" manual_name="I/O Page Table"
198        cap_description="Capability to the I/O page table being operated on.">
199        <method id="X86IOPageTableMap" name="Map" condition='defined(CONFIG_IOMMU)'>
200            <brief>
201                Map an IO page table into an IOSpace.
202            </brief>
203            <description>
204                <docref>See <autoref label="sec:iospace"/></docref>
205            </description>
206            <param dir="in" name="iospace" type="seL4_X86_IOSpace"
207                description='The IOSpace to map the page table into.'/>
208            <param dir="in" name="ioaddr" type="seL4_Word"
209                description='The address to map the page table at.'/>
210            <error name="seL4_DeleteFirst">
211                <description>
212                    All required page tables are already mapped in <texttt text="iospace"/> at <texttt text="ioaddr"/>.
213                </description>
214            </error>
215            <error name="seL4_FailedLookup">
216                <description>
217                    The <texttt text="iospace"/> does not have a paging structure at the required level mapped at <texttt text="ioaddr"/>.
218                </description>
219            </error>
220            <error name="seL4_IllegalOperation">
221                <description>
222                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
223                </description>
224            </error>
225            <error name="seL4_InvalidCapability">
226                <description>
227                    The <texttt text="_service"/> or <texttt text="iospace"/> is a CPtr to a capability of the wrong type.
228                    Or, <texttt text="iospace"/> is not assigned to a PCI device.
229                    Or, <texttt text="_service"/> is already mapped in an IOSpace.
230                </description>
231            </error>
232        </method>
233        <method id="X86IOPageTableUnmap" name="Unmap" condition='defined(CONFIG_IOMMU)'>
234            <brief>
235                Unmap an IO page table from an IOSpace.
236            </brief>
237            <description>
238                <docref>See <autoref label="sec:iospace"/></docref>
239            </description>
240            <cap_param append_description='The page table to unmap.'/>
241            <error name="seL4_IllegalOperation">
242                <description>
243                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
244                </description>
245            </error>
246            <error name="seL4_InvalidCapability">
247                <description>
248                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
249                </description>
250            </error>
251        </method>
252    </interface>
253
254    <interface name="seL4_X86_Page" manual_name="Page" cap_description="Capability to the page being operated on.">
255        <method id="X86PageMap" name="Map" manual_label='page_map'>
256            <brief>
257                Map a page into an address space or update the mapping attributes.
258            </brief>
259            <description>
260                Takes a VSpace capability, as an
261                argument and installs a reference
262                to the given <texttt text="Page"/> in the lowest-level unmapped paging structure
263                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
264                this operation will fail, returning a seL4_FailedLookup error.
265            </description>
266            <param dir="in" name="vspace" type="seL4_CPtr"
267                description='Capability to the VSpace which will contain the mapping'/>
268            <param dir="in" name="vaddr" type="seL4_Word"
269                description='Virtual address to map the page into.'/>
270            <param dir="in" name="rights" type="seL4_CapRights_t">
271                <description>
272                    Rights for the mapping. <docref>Possible values for this type are given in <autoref label='sec:cap_rights'/></docref>
273                </description>
274            </param>
275            <param dir="in" name="attr" type="seL4_X86_VMAttributes">
276                <description>
277                    VM attributes for the mapping. <docref>Possible values for this type are given in <autoref label='ch:vspace'/></docref>
278                </description>
279            </param>
280            <error name="seL4_AlignmentError">
281                <description>
282                    The <texttt text="vaddr"/> is not aligned to the page size of <texttt text="_service"/>.
283                </description>
284            </error>
285            <error name="seL4_DeleteFirst">
286                <description>
287                    A mapping already exists in <texttt text="vspace"/> at <texttt text="vaddr"/>.
288                </description>
289            </error>
290            <error name="seL4_FailedLookup">
291                <description>
292                    The <texttt text="vspace"/> does not have a paging structure at the required level mapped at <texttt text="vaddr"/>.
293                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
294                </description>
295            </error>
296            <error name="seL4_IllegalOperation">
297                <description>
298                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
299                    Or, <texttt text="_service"/> is already mapped in an IOSpace.
300                </description>
301            </error>
302            <error name="seL4_InvalidArgument">
303                <description>
304                    The <texttt text="_service"/> is already mapped in <texttt text="vspace"/> at a different virtual address.
305                    Or, <texttt text="vaddr"/> is in the kernel virtual address range.
306                </description>
307            </error>
308            <error name="seL4_InvalidCapability">
309                <description>
310                    The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
311                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
312                    Or, <texttt text="_service"/> is already mapped in a different VSpace.
313                </description>
314            </error>
315        </method>
316        <method id="X86PageUnmap" name="Unmap" manual_label='page_unmap'>
317            <brief>
318                Unmap a page.
319            </brief>
320            <description>
321                Removes an existing mapping.
322            </description>
323            <error name="seL4_IllegalOperation">
324                <description>
325                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
326                </description>
327            </error>
328            <error name="seL4_InvalidCapability">
329                <description>
330                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
331                </description>
332            </error>
333        </method>
334        <method id="X86PageMapIO" name="MapIO" manual_name="Map I/O" manual_label='page_map_io' condition='defined(CONFIG_IOMMU)'>
335            <brief>
336                Map a page into an IOSpace.
337            </brief>
338            <description>
339                <docref>See <autoref label="ch:vspace"/></docref>
340            </description>
341            <param dir="in" name="iospace" type="seL4_X86_IOSpace"
342                description='The IOSpace that the frame is being mapped into'/>
343            <param dir="in" name="rights" type="seL4_CapRights_t">
344                <description>
345                    Rights for the mapping. <docref>Possible values for this type are given in <autoref label='sec:cap_rights'/></docref>
346                </description>
347            </param>
348            <param dir="in" name="ioaddr" type="seL4_Word"
349                description='The address that the frame is being mapped at.'/>
350            <error name="seL4_DeleteFirst">
351                <description>
352                    A mapping already exists in <texttt text="iospace"/> at <texttt text="ioaddr"/>.
353                </description>
354            </error>
355            <error name="seL4_FailedLookup">
356                <description>
357                    The <texttt text="iospace"/> does not have a sufficient number of IO Page Tables mapped at <texttt text="ioaddr"/>.
358                </description>
359            </error>
360            <error name="seL4_IllegalOperation">
361                <description>
362                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
363                </description>
364            </error>
365            <error name="seL4_InvalidArgument">
366                <description>
367                    No rights were specified in <texttt text="rights"/>.
368                    Or, the rights in the <texttt text="_service"/> capability do not include <texttt text="rights"/>.
369                </description>
370            </error>
371            <error name="seL4_InvalidCapability">
372                <description>
373                    The <texttt text="_service"/> or <texttt text="iospace"/> is a CPtr to a capability of the wrong type.
374                    Or, <texttt text="_service"/> is already mapped.
375                    Or, <texttt text="_service"/> is not a page of size 4 KiB.
376                    Or, <texttt text="iospace"/> is not assigned to a PCI device.
377                </description>
378            </error>
379        </method>
380        <method id="X86PageGetAddress" name="GetAddress" manual_name="Get Address"
381            manual_label='page_getaddress'>
382            <brief>
383                Get the physical address of the underlying frame.
384            </brief>
385            <description>
386                <docref>See <autoref label="ch:vspace"/></docref>
387            </description>
388            <return>
389                A <texttt text='seL4_IA32_Page_GetAddress_t'/> struct that contains a
390                <texttt text='seL4_Word paddr'/>, which holds the physical address of the page,
391                and <texttt text='int error'/>. <docref>See <autoref label='sec:errors'/> for a description
392                of the message register and tag contents upon error.</docref>
393            </return>
394            <param dir="out" name="paddr" type="seL4_Word"/>
395            <error name="seL4_IllegalOperation">
396                <description>
397                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
398                </description>
399            </error>
400            <error name="seL4_InvalidCapability">
401                <description>
402                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
403                </description>
404            </error>
405        </method>
406        <method id="X86PageMapEPT" name="MapEPT" condition="defined(CONFIG_VTX)" manual_name="Map EPT">
407            <description>
408                TODO
409            </description>
410            <param dir="in" name="vspace" type="seL4_X86_EPTPML4"/>
411            <param dir="in" name="vaddr" type="seL4_Word"/>
412            <param dir="in" name="rights" type="seL4_CapRights_t"/>
413            <param dir="in" name="attr" type="seL4_X86_VMAttributes"/>
414            <error name="seL4_AlignmentError">
415                <description>
416                    The <texttt text="vaddr"/> is not aligned to the page size of <texttt text="_service"/>.
417                </description>
418            </error>
419            <error name="seL4_DeleteFirst">
420                <description>
421                    A mapping already exists in <texttt text="vspace"/> at <texttt text="vaddr"/>.
422                </description>
423            </error>
424            <error name="seL4_FailedLookup">
425                <description>
426                    The <texttt text="vspace"/> does not have a paging structure at the required level mapped at <texttt text="vaddr"/>.
427                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
428                </description>
429            </error>
430            <error name="seL4_IllegalOperation">
431                <description>
432                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
433                </description>
434            </error>
435            <error name="seL4_InvalidCapability">
436                <description>
437                    The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
438                    Or, <texttt text="vspace"/> is not assigned to an ASID pool.
439                    Or, <texttt text="_service"/> is already mapped.
440                    Or, <texttt text="_service"/> has an unsupported page size.
441                </description>
442            </error>
443        </method>
444    </interface>
445
446    <interface name="seL4_X86_ASIDControl" manual_name="ASID Control">
447        <method id="X86ASIDControlMakePool" name="MakePool" manual_name="Make Pool"
448            manual_label='ASID_controlmakepool'>
449            <brief>
450                Create an X86 ASID pool.
451            </brief>
452            <description>
453                Together with a capability to <texttt text="Untyped Memory"/>, which is passed as an argument,
454                create an <texttt text="ASID Pool"/>. The untyped capability must represent a
455                4K memory object. This will create an ASID pool with enough space for 1024 VSpaces.
456            </description>
457            <cap_param append_description='The master ASIDControl capability.'/>
458            <param dir="in" name="untyped" type="seL4_Untyped"
459                description='Capability to an untyped memory object that will become the pool. Must be 4K bytes.'/>
460            <param dir="in" name="root" type="seL4_CNode"
461                description='CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize.'/>
462            <param dir="in" name="index" type="seL4_Word"
463                description='CPTR to the destination slot. Resolved from the root of the destination CSpace.'/>
464            <param dir="in" name="depth" type="seL4_Uint8"
465                description='Number of bits of index to resolve to find the destination slot.'/>
466            <error name="seL4_DeleteFirst">
467                <description>
468                    The destination slot contains a capability.
469                    Or, there are no more ASID pools available.
470                </description>
471            </error>
472            <error name="seL4_FailedLookup">
473                <description>
474                    The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
475                    Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
476                </description>
477            </error>
478            <error name="seL4_IllegalOperation">
479                <description>
480                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
481                </description>
482            </error>
483            <error name="seL4_InvalidCapability">
484                <description>
485                    The <texttt text="_service"/> or <texttt text="untyped"/> is a CPtr to a capability of the wrong type.
486                    Or, <texttt text="untyped"/> is not the exact size of an ASID pool object.
487                    Or, <texttt text="untyped"/> is a device untyped <docref>(see <autoref label="sec:kernmemalloc"/>)</docref>.
488                </description>
489            </error>
490            <error name="seL4_RangeError">
491                <description>
492                    The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
493                </description>
494            </error>
495            <error name="seL4_RevokeFirst">
496                <description>
497                    The <texttt text="untyped"/> has been used to retype an object.
498                    Or, a copy of the <texttt text="untyped"/> capability exists.
499                </description>
500            </error>
501        </method>
502    </interface>
503
504    <interface name="seL4_X86_ASIDPool" manual_name="ASID Pool">
505        <method id="X86ASIDPoolAssign" name="Assign" manual_label='asidpool_assign'>
506            <brief>
507                Assign an ASID pool.
508            </brief>
509            <description>
510                Assigns an ASID to the VSpace associated with the <texttt text="Page Directory"/> passed in as an argument.
511            </description>
512            <cap_param append_description='The ASID pool which is being assigned to. Must not be full. Each ASID pool can contain 1024 entries.'/>
513            <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.'/>
514            <error name="seL4_DeleteFirst">
515                <description>
516                    There are no more ASIDs available in <texttt text="_service"/>.
517                </description>
518            </error>
519            <error name="seL4_IllegalOperation">
520                <description>
521                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
522                </description>
523            </error>
524            <error name="seL4_InvalidCapability">
525                <description>
526                    The <texttt text="_service"/> or <texttt text="vspace"/> is a CPtr to a capability of the wrong type.
527                    Or, <texttt text="vspace"/> is already assigned to an ASID pool.
528                </description>
529            </error>
530        </method>
531    </interface>
532
533    <interface name="seL4_X86_IOPortControl" manual_name="I/O Port Control" cap_description='Control capability for I/O ports.'>
534        <method id="X86IOPortControlIssue" name="Issue" manual_label="ioport_issue">
535            <brief>
536                Issue an IO port sub range.
537            </brief>
538            <description>
539                <docref>See <autoref label='sec:ioports'/></docref>
540                </description>
541            <param dir="in" name="first_port" type="seL4_Word" description="First port of the range of the issued capability."/>
542            <param dir="in" name="last_port" type="seL4_Word" description="Last port of the range of the issued capability."/>
543            <param dir="in" name="root" type="seL4_CNode" description="CPTR to the CNode that forms the root of the destination CSpace."/>
544            <param dir="in" name="index" type="seL4_Word" description="CPTR to the destination slot. Resolved from the root of the destination CSpace."/>
545            <param dir="in" name="depth" type="seL4_Uint8" description="Number of bits of dest_index to resolve to find the destination slot."/>
546            <error name="seL4_DeleteFirst">
547                <description>
548                    The destination slot contains a capability.
549                </description>
550            </error>
551            <error name="seL4_FailedLookup">
552                <description>
553                    The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
554                    Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
555                </description>
556            </error>
557            <error name="seL4_IllegalOperation">
558                <description>
559                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
560                </description>
561            </error>
562            <error name="seL4_InvalidArgument">
563                <description>
564                    The <texttt text="last_port"/> is less than <texttt text="first_port"/>.
565                </description>
566            </error>
567            <error name="seL4_InvalidCapability">
568                <description>
569                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
570                </description>
571            </error>
572            <error name="seL4_RangeError">
573                <description>
574                    The <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
575                </description>
576            </error>
577            <error name="seL4_RevokeFirst">
578                <description>
579                    One or more ports in the requested range have already been issued.
580                </description>
581            </error>
582        </method>
583    </interface>
584
585    <interface name="seL4_X86_IOPort" manual_name="I/O Port" cap_description='An I/O Port capability.'>
586        <method id="X86IOPortIn8" name="In8">
587            <brief>
588                Read 8 bits from an IO port.
589            </brief>
590            <description>
591                <docref>See <autoref label='sec:ioports'/></docref>
592            </description>
593            <return>
594                A <texttt text='seL4_X86_IOPort_In8_t'/> structure <docref>as described in <autoref label='sec:ioports'/>.</docref>
595            </return>
596            <param dir="out" name="result" type="seL4_Uint8" />
597            <param dir="in" name="port" type="seL4_Uint16" description='The port to read from.'/>
598            <error name="seL4_IllegalOperation">
599                <description>
600                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
601                    Or, reading from <texttt text="port"/> is not authorized by the capability.
602                </description>
603            </error>
604            <error name="seL4_InvalidCapability">
605                <description>
606                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
607                </description>
608            </error>
609        </method>
610        <method id="X86IOPortIn16" name="In16">
611            <brief>
612                Read 16 bits from an IO port.
613            </brief>
614            <description>
615                <docref>See <autoref label='sec:ioports'/></docref>
616            </description>
617            <return>
618                A <texttt text='seL4_X86_IOPort_In16_t'/> structure <docref>as described in <autoref label='sec:ioports'/>.</docref>
619            </return>
620            <param dir="out" name="result" type="seL4_Uint16"/>
621            <param dir="in" name="port" type="seL4_Uint16" description='The port to read from.'/>
622            <error name="seL4_IllegalOperation">
623                <description>
624                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
625                    Or, reading from <texttt text="port"/> and <texttt text="port+1"/> is not authorized by the capability.
626                </description>
627            </error>
628            <error name="seL4_InvalidCapability">
629                <description>
630                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
631                </description>
632            </error>
633        </method>
634        <method id="X86IOPortIn32" name="In32">
635            <brief>
636                Read 32 bits from an IO port.
637            </brief>
638            <description>
639                <docref>See <autoref label='sec:ioports'/></docref>
640            </description>
641            <return>
642                A <texttt text='seL4_X86_IOPort_In32_t'/> structure <docref>as described in <autoref label='sec:ioports'/>.</docref>
643            </return>
644            <param dir="out" name="result" type="seL4_Uint32"/>
645            <param dir="in" name="port" type="seL4_Uint16" description='The port to read from.'/>
646            <error name="seL4_IllegalOperation">
647                <description>
648                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
649                    Or, reading from ports <texttt text="port"/> through <texttt text="port+3"/> is not authorized by the capability.
650                </description>
651            </error>
652            <error name="seL4_InvalidCapability">
653                <description>
654                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
655                </description>
656            </error>
657        </method>
658        <method id="X86IOPortOut8" name="Out8">
659            <brief>
660                Write 8 bits to an IO port.
661            </brief>
662            <description>
663                <docref>See <autoref label='sec:ioports'/></docref>
664            </description>
665            <param dir="in" name="port" type="seL4_Word" description='The port to write to.'/>
666            <param dir="in" name="data" type="seL4_Word" description='Data to write to the IO port.'/>
667            <error name="seL4_IllegalOperation">
668                <description>
669                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
670                    Or, writing to <texttt text="port"/> is not authorized by the capability.
671                </description>
672            </error>
673            <error name="seL4_InvalidCapability">
674                <description>
675                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
676                </description>
677            </error>
678        </method>
679        <method id="X86IOPortOut16" name="Out16">
680            <brief>
681                Write 16 bits to an IO port.
682            </brief>
683            <description>
684                <docref>See <autoref label='sec:ioports'/></docref>
685            </description>
686            <param dir="in" name="port" type="seL4_Word" description='The port to write to.'/>
687            <param dir="in" name="data" type="seL4_Word" description='Data to write to the IO port.'/>
688            <error name="seL4_IllegalOperation">
689                <description>
690                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
691                    Or, writing to <texttt text="port"/> and <texttt text="port+1"/> is not authorized by the capability.
692                </description>
693            </error>
694            <error name="seL4_InvalidCapability">
695                <description>
696                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
697                </description>
698            </error>
699        </method>
700        <method id="X86IOPortOut32" name="Out32">
701            <brief>
702                Write 32 bits to an IO port.
703            </brief>
704            <description>
705                <docref>See <autoref label='sec:ioports'/></docref>
706            </description>
707            <param dir="in" name="port" type="seL4_Word" description='The port to write to.'/>
708            <param dir="in" name="data" type="seL4_Word" description='Data to write to the IO port.'/>
709            <error name="seL4_IllegalOperation">
710                <description>
711                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
712                    Or, writing to ports <texttt text="port"/> through <texttt text="port+3"/> is not authorized by the capability.
713                </description>
714            </error>
715            <error name="seL4_InvalidCapability">
716                <description>
717                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
718                </description>
719            </error>
720        </method>
721    </interface>
722
723    <interface name="seL4_IRQControl" manual_name="IRQ Control" cap_description='An IRQControl capability. This gives you the authority to make this call.'>
724        <method id="X86IRQIssueIRQHandlerIOAPIC" name="GetIOAPIC" manual_name="Get I/O APIC">
725            <brief>
726                Create an IRQ handler capability for an interrupt from an IOAPIC.
727            </brief>
728            <description>
729                <docref>See <autoref label='sec:interrupts'/> and <autoref label='sec:x86_interrupts'/>.</docref>
730            </description>
731            <param dir="in" name="root" type="seL4_CNode"
732                description='CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize.'/>
733            <param dir="in" name="index" type="seL4_Word"
734                description='CPTR to the destination slot. Resolved from the root of the destination CSpace.'/>
735            <param dir="in" name="depth" type="seL4_Uint8"
736                description='Number of bits of index to resolve to find the destination slot.'/>
737
738            <param dir="in" name="ioapic" type="seL4_Word"
739                description='Zero based index of IOAPIC to get interrupt from,
740                             ordered the same as in ACPI tables'/>
741            <param dir="in" name="pin" type="seL4_Word" description='IOAPIC pin that generates the interrupt.'/>
742            <param dir="in" name="level" type="seL4_Word" description='Indicates whether the IOAPIC should be programmed to treat this interrupt as level triggered.'/>
743            <param dir="in" name="polarity" type="seL4_Word" description='Indicates whether the IOAPIC should be programmed to treat this interrupt as high or
744                     low triggered'/>
745            <param dir="in" name="vector" type="seL4_Word" description='CPU vector to deliver the interrupt to.'/>
746            <error name="seL4_DeleteFirst">
747                <description>
748                    The destination slot contains a capability.
749                </description>
750            </error>
751            <error name="seL4_FailedLookup">
752                <description>
753                    The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
754                    Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
755                </description>
756            </error>
757            <error name="seL4_IllegalOperation">
758                <description>
759                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
760                    Or, an IOAPIC is not in use.
761                </description>
762            </error>
763            <error name="seL4_InvalidCapability">
764                <description>
765                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
766                </description>
767            </error>
768            <error name="seL4_RangeError">
769                <description>
770                    The <texttt text="vector"/>, <texttt text="ioapic"/>, or <texttt text="pin"/> is invalid.
771                    Or, <texttt text="level"/> or <texttt text="polarity"/> is not 0 or 1.
772                    Or, <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
773                </description>
774            </error>
775            <error name="seL4_RevokeFirst">
776                <description>
777                    An IRQ handler capability for <texttt text="vector"/> has already been created.
778                </description>
779            </error>
780        </method>
781        <method id="X86IRQIssueIRQHandlerMSI" name="GetMSI" manual_name="Get MSI">
782            <brief>
783                Create an IRQ handler capability for an interrupt from an MSI.
784            </brief>
785            <description>
786                <docref>See <autoref label='sec:interrupts'/> and <autoref label='sec:x86_interrupts'/>.</docref>
787            </description>
788            <param dir="in" name="root" type="seL4_CNode"
789                description='CPTR to the CNode that forms the root of the destination CSpace. Must be at a depth equivalent to the wordsize.'/>
790            <param dir="in" name="index" type="seL4_Word"
791                description='CPTR to the destination slot. Resolved from the root of the destination CSpace.'/>
792            <param dir="in" name="depth" type="seL4_Uint8"
793                description='Number of bits of index to resolve to find the destination slot.'/>
794            <param dir="in" name="pci_bus" type="seL4_Word" description='PCI bus ID of the device that will generate the interrupt.'/>
795            <param dir="in" name="pci_dev" type="seL4_Word" description='PCI device ID of the device that will generate the interrupt.'/>
796            <param dir="in" name="pci_func" type="seL4_Word" description='PCI function ID of the device that will generate the interrupt.'/>
797            <param dir="in" name="handle" type="seL4_Word" description='Value of the handle programmed into the data portion of the MSI.'/>
798            <param dir="in" name="vector" type="seL4_Word" description='CPU vector to deliver the interrupt to.'/>
799            <error name="seL4_DeleteFirst">
800                <description>
801                    The destination slot contains a capability.
802                </description>
803            </error>
804            <error name="seL4_FailedLookup">
805                <description>
806                    The <texttt text="index"/> or <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
807                    Or, <texttt text="root"/> is a CPtr to a capability of the wrong type.
808                </description>
809            </error>
810            <error name="seL4_IllegalOperation">
811                <description>
812                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
813                    Or, an IOAPIC is not in use.
814                </description>
815            </error>
816            <error name="seL4_InvalidCapability">
817                <description>
818                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
819                </description>
820            </error>
821            <error name="seL4_RangeError">
822                <description>
823                    The <texttt text="vector"/>, <texttt text="pic_bus"/>, <texttt text="pci_dev"/>, or <texttt text="pci_func"/> is invalid.
824                    Or, the <texttt text="depth"/> is invalid <docref>(see <autoref label="s:cspace-addressing"/>)</docref>.
825                </description>
826            </error>
827            <error name="seL4_RevokeFirst">
828                <description>
829                    An IRQ handler capability for <texttt text="vector"/> has already been created.
830                </description>
831            </error>
832        </method>
833    </interface>
834    <interface name="seL4_TCB" manual_name="TCB">
835        <method id="TCBSetEPTRoot" name="SetEPTRoot" condition="defined(CONFIG_VTX)" manual_name="Set EPT Root" manual_label="set_eptroot">
836            <brief>
837                Set the EPT root of a thread
838            </brief>
839            <description>
840                <docref>See <autoref label='sec:virt'/>.</docref>
841            </description>
842            <param dir="in" name="eptpml4" type="seL4_X86_EPTPML4"
843                description='CPTR to an EPT PML4 object to act as the guest mode vspace root'/>
844            <error name="seL4_IllegalOperation">
845                <description>
846                    The <texttt text="_service"/> or <texttt text="eptpml4"/> is a CPtr to a capability of the wrong type.
847                    Or, <texttt text="eptpml4"/> is not assigned to an ASID pool.
848                </description>
849            </error>
850            <error name="seL4_InvalidCapability">
851                <description>
852                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
853                </description>
854            </error>
855        </method>
856    </interface>
857    <interface name="seL4_X86_VCPU" manual_name="VCPU" cap_description='VCPU object to operate on'>
858        <method id="X86VCPUSetTCB" name="SetTCB" condition="defined(CONFIG_VTX)" manual_name="Set TCB">
859            <brief>
860                Bind TCB to VCPU
861            </brief>
862            <description>
863                Configures the one-to-one binding of a VCPU and TCB, overwriting any previous binding
864                in both. <docref>See <autoref label='sec:virt'/>.</docref>
865            </description>
866            <param dir="in" name="tcb" type="seL4_TCB" description='CPTR of the TCB to bind to'/>
867            <error name="seL4_IllegalOperation">
868                <description>
869                    The <texttt text="_service"/> or <texttt text="tcb"/> is a CPtr to a capability of the wrong type.
870                </description>
871            </error>
872            <error name="seL4_InvalidCapability">
873                <description>
874                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
875                </description>
876            </error>
877        </method>
878        <method id="X86VCPUReadVMCS" name="ReadVMCS" condition="defined(CONFIG_VTX)" manual_name="Read VMCS" manual_label="vcpu_readvmcs">
879            <brief>
880                Read VMCS field from the hardware
881            </brief>
882            <description>
883                Thin wrapper around the <texttt text='vmread'/> instruction that is performed on the
884                VMCS region that is part of the VCPU object. After validating that a legal
885                field is requested the value of `vmread` is returned directly in the result.
886            </description>
887            <return>
888                A <texttt text='seL4_X86_VCPU_ReadVMCS_t'/> struct that contains a
889                <texttt text='seL4_Word value'/>, which holds the return result of the <texttt text='vmread'/> instruction,
890                and <texttt text='int error'/>. <docref>See <autoref label='sec:errors'/> for a description
891                of the message register and tag contents upon error.</docref>
892            </return>
893            <param dir="in" name="field" type="seL4_Word"
894                description='Field to give to `vmread` instruction'/>
895            <param dir="out" name="value" type="seL4_Word"
896                description='Value returned by `vmread` instruction'/>
897            <error name="seL4_IllegalOperation">
898                <description>
899                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
900                    Or, <texttt text="field"/> is invalid or unsupported.
901                </description>
902            </error>
903            <error name="seL4_InvalidCapability">
904                <description>
905                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
906                </description>
907            </error>
908        </method>
909        <method id="X86VCPUWriteVMCS" name="WriteVMCS" condition="defined(CONFIG_VTX)" manual_name="Write VMCS" manual_label="vcpu_writevmcs">
910            <brief>
911                Write VMCS field to the hardware
912            </brief>
913            <description>
914                Thin wrapper around the `vmwrite` instruction that is performed on the
915                VMCS region that is part of the VCPU object. As well as validating that
916                a legal field is requested, the value may be modified to ensure any
917                bits that are fixed in the hardware are correct, and that any features
918                required for kernel correctness are not disabled <docref>(see <autoref label='sec:virt'/>)</docref>.
919
920                The final value written to the hardware is returned and can be compared
921                to the input parameter to determine what bits the kernel changed.
922            </description>
923            <return>
924                A <texttt text='seL4_X86_VCPU_WriteVMCS_t'/> struct that contains a
925                <texttt text='seL4_Word writen'/>, which holds the final value written with the <texttt text='vmwrite'/> instruction,
926                and <texttt text='int error'/>. <docref>See <autoref label='sec:errors'/> for a description
927                of the message register and tag contents upon error.</docref>
928            </return>
929            <param dir="in" name="field" type="seL4_Word"
930                description='Field to give to `vmwrite` instruction'/>
931            <param dir="in" name="value" type="seL4_Word"
932                description='Value to write using `vmwrite` instruction'/>
933            <param dir="out" name="written" type="seL4_Word"
934                description='Final value written using `vmwrite` after kernel validation'/>
935            <error name="seL4_IllegalOperation">
936                <description>
937                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
938                    Or, <texttt text="field"/> is invalid or unsupported.
939                </description>
940            </error>
941            <error name="seL4_InvalidCapability">
942                <description>
943                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
944                </description>
945            </error>
946        </method>
947        <method id="X86VCPUEnableIOPort" name="EnableIOPort" condition="defined(CONFIG_VTX)"
948            manual_name="Enable IO Port" manual_label="vcpu_enableioport">
949            <brief>
950                Enable I/O port range in guest execution
951            </brief>
952            <description>
953                Enables a range of I/O ports for direct access by the execution mode in
954                the <texttt text='VCPU'/>. The requested port range must be a sub range
955                of the provided I/O port capability.
956
957                This also establishes a link between the provided I/O port capability and
958                the <texttt text='VCPU'/><docref>, see <autoref label='sec:virt'/> for details.</docref>
959            </description>
960            <param dir="in" name="ioPort" type="seL4_X86_IOPort"
961                description='I/O port capability whose authority is being delegating'/>
962            <param dir="in" name="low" type="seL4_Word"
963                description='Start of the I/O port range to enable'/>
964            <param dir="in" name="high" type="seL4_Word"
965                description='Last I/O port in the range to enable'/>
966            <error name="seL4_IllegalOperation">
967                <description>
968                    The <texttt text="_service"/> or <texttt text="ioPort"/> is a CPtr to a capability of the wrong type.
969                </description>
970            </error>
971            <error name="seL4_InvalidArgument">
972                <description>
973                    The <texttt text="low"/> or <texttt text="high"/> IO port exceeds the range authorized by <texttt text="ioPort"/>.
974                </description>
975            </error>
976            <error name="seL4_InvalidCapability">
977                <description>
978                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
979                </description>
980            </error>
981        </method>
982        <method id="X86VCPUDisableIOPort" name="DisableIOPort" condition="defined(CONFIG_VTX)"
983            manual_name="Disable IO Port">
984            <brief>
985                Disable I/O port range in privileged execution
986            </brief>
987            <description>
988                Disable a range of I/O ports for direct access by the execution mode in
989                the <texttt text='VCPU'/>.
990            </description>
991            <param dir="in" name="low" type="seL4_Word"
992                description='Start of the I/O port range to disable'/>
993            <param dir="in" name="high" type="seL4_Word"
994                description='Last I/O port in the range to disable'/>
995            <error name="seL4_IllegalOperation">
996                <description>
997                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
998                </description>
999            </error>
1000            <error name="seL4_InvalidCapability">
1001                <description>
1002                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1003                </description>
1004            </error>
1005        </method>
1006        <method id="X86VCPUWriteRegisters" name="WriteRegisters" condition="defined(CONFIG_VTX)"
1007            manual_name="Write Registers">
1008            <brief>
1009                Set guest mode registers to the fields of a given <texttt text="seL4_VCPUContext"/>
1010            </brief>
1011            <description>
1012                Sets the guest mode registers, which is any registers not already part of the VMCS.
1013            </description>
1014            <param dir="in" name="regs" type="seL4_VCPUContext"
1015                description='Data structure containing the new register values.'/>
1016            <error name="seL4_IllegalOperation">
1017                <description>
1018                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1019                </description>
1020            </error>
1021            <error name="seL4_InvalidCapability">
1022                <description>
1023                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1024                </description>
1025            </error>
1026        </method>
1027    </interface>
1028    <interface name="seL4_X86_EPTPDPT" manual_name="Extended Page Table Page Directory Page Table"
1029        cap_description="Capability to the EPT PDPT being operated on.">
1030        <method id="X86EPTPDPTMap" name="Map" condition="defined(CONFIG_VTX)">
1031            <brief>
1032                Map an EPT page directory page table.
1033            </brief>
1034            <description>
1035                <docref>See <autoref label="ch:vspace"/></docref>
1036            </description>
1037            <param dir="in" name="eptpml4" type="seL4_X86_EPTPML4"
1038                description='Capability to the EPT root which will contain the mapping'/>
1039            <param dir="in" name="gpa" type="seL4_Word"
1040                description='Guest physical address to map the page into.'/>
1041            <param dir="in" name="attr" type="seL4_X86_VMAttributes">
1042                <description>
1043                    VM attributes for the mapping. <docref>Possible values for this type are given in <autoref label='ch:vspace'/></docref>
1044                </description>
1045            </param>
1046            <error name="seL4_DeleteFirst">
1047                <description>
1048                    A mapping already exists for this level in <texttt text="eptpml4"/> at <texttt text="gpa"/>.
1049                </description>
1050            </error>
1051            <error name="seL4_FailedLookup">
1052                <description>
1053                    The <texttt text="eptpml4"/> is not assigned to an ASID pool.
1054                </description>
1055            </error>
1056            <error name="seL4_IllegalOperation">
1057                <description>
1058                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1059                </description>
1060            </error>
1061            <error name="seL4_InvalidCapability">
1062                <description>
1063                    The <texttt text="_service"/> or <texttt text="eptpml4"/> is a CPtr to a capability of the wrong type.
1064                    Or, <texttt text="_service"/> is already mapped in a VSpace.
1065                    Or, <texttt text="eptpml4"/> is not assigned to an ASID pool.
1066                </description>
1067            </error>
1068        </method>
1069        <method id="X86EPTPDPTUnmap" name="Unmap" condition="defined(CONFIG_VTX)">
1070            <brief>
1071                Unmap an EPT page directory page table.
1072            </brief>
1073            <description>
1074                <docref>See <autoref label="ch:vspace"/></docref>
1075            </description>
1076            <error name="seL4_IllegalOperation">
1077                <description>
1078                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1079                </description>
1080            </error>
1081            <error name="seL4_InvalidCapability">
1082                <description>
1083                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1084                </description>
1085            </error>
1086            <error name="seL4_RevokeFirst">
1087                <description>
1088                    A copy of the <texttt text="_service"/> capability exists.
1089                </description>
1090            </error>
1091        </method>
1092    </interface>
1093    <interface name="seL4_X86_EPTPD" manual_name="Extended Page Table Page Directory"
1094        cap_description="Capability to the EPT PD being operated on.">
1095        <method id="X86EPTPDMap" name="Map" condition="defined(CONFIG_VTX)">
1096            <brief>
1097                Map an EPT page directory.
1098            </brief>
1099            <description>
1100                <docref>See <autoref label="ch:vspace"/></docref>
1101            </description>
1102            <param dir="in" name="eptpml4" type="seL4_X86_EPTPML4"
1103                description='Capability to the EPT root which will contain the mapping'/>
1104            <param dir="in" name="gpa" type="seL4_Word"
1105                description='Guest physical address to map the page into.'/>
1106            <param dir="in" name="attr" type="seL4_X86_VMAttributes">
1107                <description>
1108                    VM attributes for the mapping. <docref>Possible values for this type are given in <autoref label='ch:vspace'/></docref>
1109                </description>
1110            </param>
1111            <error name="seL4_DeleteFirst">
1112                <description>
1113                    A mapping already exists for this level in <texttt text="eptpml4"/> at <texttt text="gpa"/>.
1114                </description>
1115            </error>
1116            <error name="seL4_FailedLookup">
1117                <description>
1118                    The <texttt text="eptpml4"/> is not assigned to an ASID pool.
1119                    Or, <texttt text="eptpml4"/> does not have an EPTPDPT mapped at <texttt text="gpa"/>.
1120                </description>
1121            </error>
1122            <error name="seL4_IllegalOperation">
1123                <description>
1124                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1125                </description>
1126            </error>
1127            <error name="seL4_InvalidCapability">
1128                <description>
1129                    The <texttt text="_service"/> or <texttt text="eptpml4"/> is a CPtr to a capability of the wrong type.
1130                    Or, <texttt text="_service"/> is already mapped in a VSpace.
1131                    Or, <texttt text="eptpml4"/> is not assigned to an ASID pool.
1132                </description>
1133            </error>
1134        </method>
1135        <method id="X86EPTPDUnmap" name="Unmap" condition="defined(CONFIG_VTX)">
1136            <brief>
1137                Unmap an EPT page directory.
1138            </brief>
1139            <description>
1140                <docref>See <autoref label="ch:vspace"/></docref>
1141            </description>
1142            <error name="seL4_IllegalOperation">
1143                <description>
1144                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1145                </description>
1146            </error>
1147            <error name="seL4_InvalidCapability">
1148                <description>
1149                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1150                </description>
1151            </error>
1152            <error name="seL4_RevokeFirst">
1153                <description>
1154                    A copy of the <texttt text="_service"/> capability exists.
1155                </description>
1156            </error>
1157        </method>
1158    </interface>
1159    <interface name="seL4_X86_EPTPT" manual_name="Extended Page Table Page Table"
1160            cap_description="Capability to the EPT PT being operated on.">
1161        <method id="X86EPTPTMap" name="Map" condition="defined(CONFIG_VTX)">
1162            <brief>
1163                Map an EPT page table.
1164            </brief>
1165            <description>
1166                <docref>See <autoref label="ch:vspace"/></docref>
1167            </description>
1168            <param dir="in" name="eptpml4" type="seL4_X86_EPTPML4"
1169                description='Capability to the EPT root which will contain the mapping'/>
1170            <param dir="in" name="gpa" type="seL4_Word"
1171                description='Guest physical address to map the page into.'/>
1172            <param dir="in" name="attr" type="seL4_X86_VMAttributes">
1173                <description>
1174                    VM attributes for the mapping. <docref>Possible values for this type are given in <autoref label='ch:vspace'/></docref>
1175                </description>
1176            </param>
1177            <error name="seL4_DeleteFirst">
1178                <description>
1179                    A mapping already exists for this level in <texttt text="eptpml4"/> at <texttt text="gpa"/>.
1180                </description>
1181            </error>
1182            <error name="seL4_FailedLookup">
1183                <description>
1184                    The <texttt text="eptpml4"/> is not assigned to an ASID pool.
1185                    Or, <texttt text="eptpml4"/> does not have an EPTPD mapped at <texttt text="gpa"/>.
1186                </description>
1187            </error>
1188            <error name="seL4_IllegalOperation">
1189                <description>
1190                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1191                </description>
1192            </error>
1193            <error name="seL4_InvalidCapability">
1194                <description>
1195                    The <texttt text="_service"/> or <texttt text="eptpml4"/> is a CPtr to a capability of the wrong type.
1196                    Or, <texttt text="_service"/> is already mapped in a VSpace.
1197                    Or, <texttt text="eptpml4"/> is not assigned to an ASID pool.
1198                </description>
1199            </error>
1200        </method>
1201        <method id="X86EPTPTUnmap" name="Unmap" condition="defined(CONFIG_VTX)">
1202            <brief>
1203                Unmap an EPT page table.
1204            </brief>
1205            <description>
1206                <docref>See <autoref label="ch:vspace"/></docref>
1207            </description>
1208            <error name="seL4_IllegalOperation">
1209                <description>
1210                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1211                </description>
1212            </error>
1213            <error name="seL4_InvalidCapability">
1214                <description>
1215                    The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
1216                </description>
1217            </error>
1218            <error name="seL4_RevokeFirst">
1219                <description>
1220                    A copy of the <texttt text="_service"/> capability exists.
1221                </description>
1222            </error>
1223        </method>
1224    </interface>
1225</api>
1226