hacps stuff. part 1 complete

This commit is contained in:
Dane Sabo 2025-02-12 14:40:53 -05:00
parent 98acab49b5
commit edfdd215b3
2290 changed files with 468150 additions and 0 deletions

Binary file not shown.

View File

@ -0,0 +1,20 @@
<!--
Copyright 2023, seL4 Project a Series of LF Projects, LLC.
SPDX-License-Identifier: CC-BY-SA-4.0
-->
# License
The files in the Microkit project are released under standard open source
licenses, identified by [SPDX license tags][1]. See the individual file headers
for details, or use one of the publicly available SPDX tools to generate a bill
of materials. The directory [`LICENSES`][2] contains the text for all licenses
that are mentioned by files in this project.
Code contributions to this project should be licensed under the [BSD-2-Clause]
license, and documentation under the [CC-BY-SA-4.0] license.
[1]: https://spdx.org
[2]: LICENSES/
[BSD-2-CLAUSE]: LICENSES/BSD-2-Clause.txt
[CC-BY-SA-4.0]: LICENSES/CC-BY-SA-4.0.txt

View File

@ -0,0 +1,9 @@
Copyright (c) <year> <owner>
Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

View File

@ -0,0 +1,170 @@
Creative Commons Attribution-ShareAlike 4.0 International
Creative Commons Corporation (“Creative Commons”) is not a law firm and does not provide legal services or legal advice. Distribution of Creative Commons public licenses does not create a lawyer-client or other relationship. Creative Commons makes its licenses and related information available on an “as-is” basis. Creative Commons gives no warranties regarding its licenses, any material licensed under their terms and conditions, or any related information. Creative Commons disclaims all liability for damages resulting from their use to the fullest extent possible.
Using Creative Commons Public Licenses
Creative Commons public licenses provide a standard set of terms and conditions that creators and other rights holders may use to share original works of authorship and other material subject to copyright and certain other rights specified in the public license below. The following considerations are for informational purposes only, are not exhaustive, and do not form part of our licenses.
Considerations for licensors: Our public licenses are intended for use by those authorized to give the public permission to use material in ways otherwise restricted by copyright and certain other rights. Our licenses are irrevocable. Licensors should read and understand the terms and conditions of the license they choose before applying it. Licensors should also secure all rights necessary before applying our licenses so that the public can reuse the material as expected. Licensors should clearly mark any material not subject to the license. This includes other CC-licensed material, or material used under an exception or limitation to copyright. More considerations for licensors.
Considerations for the public: By using one of our public licenses, a licensor grants the public permission to use the licensed material under specified terms and conditions. If the licensors permission is not necessary for any reasonfor example, because of any applicable exception or limitation to copyrightthen that use is not regulated by the license. Our licenses grant only permissions under copyright and certain other rights that a licensor has authority to grant. Use of the licensed material may still be restricted for other reasons, including because others have copyright or other rights in the material. A licensor may make special requests, such as asking that all changes be marked or described.
Although not required by our licenses, you are encouraged to respect those requests where reasonable. More considerations for the public.
Creative Commons Attribution-ShareAlike 4.0 International Public License
By exercising the Licensed Rights (defined below), You accept and agree to be bound by the terms and conditions of this Creative Commons Attribution-ShareAlike 4.0 International Public License ("Public License"). To the extent this Public License may be interpreted as a contract, You are granted the Licensed Rights in consideration of Your acceptance of these terms and conditions, and the Licensor grants You such rights in consideration of benefits the Licensor receives from making the Licensed Material available under these terms and conditions.
Section 1 Definitions.
a. Adapted Material means material subject to Copyright and Similar Rights that is derived from or based upon the Licensed Material and in which the Licensed Material is translated, altered, arranged, transformed, or otherwise modified in a manner requiring permission under the Copyright and Similar Rights held by the Licensor. For purposes of this Public License, where the Licensed Material is a musical work, performance, or sound recording, Adapted Material is always produced where the Licensed Material is synched in timed relation with a moving image.
b. Adapter's License means the license You apply to Your Copyright and Similar Rights in Your contributions to Adapted Material in accordance with the terms and conditions of this Public License.
c. BY-SA Compatible License means a license listed at creativecommons.org/compatiblelicenses, approved by Creative Commons as essentially the equivalent of this Public License.
d. Copyright and Similar Rights means copyright and/or similar rights closely related to copyright including, without limitation, performance, broadcast, sound recording, and Sui Generis Database Rights, without regard to how the rights are labeled or categorized. For purposes of this Public License, the rights specified in Section 2(b)(1)-(2) are not Copyright and Similar Rights.
e. Effective Technological Measures means those measures that, in the absence of proper authority, may not be circumvented under laws fulfilling obligations under Article 11 of the WIPO Copyright Treaty adopted on December 20, 1996, and/or similar international agreements.
f. Exceptions and Limitations means fair use, fair dealing, and/or any other exception or limitation to Copyright and Similar Rights that applies to Your use of the Licensed Material.
g. License Elements means the license attributes listed in the name of a Creative Commons Public License. The License Elements of this Public License are Attribution and ShareAlike.
h. Licensed Material means the artistic or literary work, database, or other material to which the Licensor applied this Public License.
i. Licensed Rights means the rights granted to You subject to the terms and conditions of this Public License, which are limited to all Copyright and Similar Rights that apply to Your use of the Licensed Material and that the Licensor has authority to license.
j. Licensor means the individual(s) or entity(ies) granting rights under this Public License.
k. Share means to provide material to the public by any means or process that requires permission under the Licensed Rights, such as reproduction, public display, public performance, distribution, dissemination, communication, or importation, and to make material available to the public including in ways that members of the public may access the material from a place and at a time individually chosen by them.
l. Sui Generis Database Rights means rights other than copyright resulting from Directive 96/9/EC of the European Parliament and of the Council of 11 March 1996 on the legal protection of databases, as amended and/or succeeded, as well as other essentially equivalent rights anywhere in the world.
m. You means the individual or entity exercising the Licensed Rights under this Public License. Your has a corresponding meaning.
Section 2 Scope.
a. License grant.
1. Subject to the terms and conditions of this Public License, the Licensor hereby grants You a worldwide, royalty-free, non-sublicensable, non-exclusive, irrevocable license to exercise the Licensed Rights in the Licensed Material to:
A. reproduce and Share the Licensed Material, in whole or in part; and
B. produce, reproduce, and Share Adapted Material.
2. Exceptions and Limitations. For the avoidance of doubt, where Exceptions and Limitations apply to Your use, this Public License does not apply, and You do not need to comply with its terms and conditions.
3. Term. The term of this Public License is specified in Section 6(a).
4. Media and formats; technical modifications allowed. The Licensor authorizes You to exercise the Licensed Rights in all media and formats whether now known or hereafter created, and to make technical modifications necessary to do so. The Licensor waives and/or agrees not to assert any right or authority to forbid You from making technical modifications necessary to exercise the Licensed Rights, including technical modifications necessary to circumvent Effective Technological Measures. For purposes of this Public License, simply making modifications authorized by this Section 2(a)(4) never produces Adapted Material.
5. Downstream recipients.
A. Offer from the Licensor Licensed Material. Every recipient of the Licensed Material automatically receives an offer from the Licensor to exercise the Licensed Rights under the terms and conditions of this Public License.
B. Additional offer from the Licensor Adapted Material. Every recipient of Adapted Material from You automatically receives an offer from the Licensor to exercise the Licensed Rights in the Adapted Material under the conditions of the Adapters License You apply.
C. No downstream restrictions. You may not offer or impose any additional or different terms or conditions on, or apply any Effective Technological Measures to, the Licensed Material if doing so restricts exercise of the Licensed Rights by any recipient of the Licensed Material.
6. No endorsement. Nothing in this Public License constitutes or may be construed as permission to assert or imply that You are, or that Your use of the Licensed Material is, connected with, or sponsored, endorsed, or granted official status by, the Licensor or others designated to receive attribution as provided in Section 3(a)(1)(A)(i).
b. Other rights.
1. Moral rights, such as the right of integrity, are not licensed under this Public License, nor are publicity, privacy, and/or other similar personality rights; however, to the extent possible, the Licensor waives and/or agrees not to assert any such rights held by the Licensor to the limited extent necessary to allow You to exercise the Licensed Rights, but not otherwise.
2. Patent and trademark rights are not licensed under this Public License.
3. To the extent possible, the Licensor waives any right to collect royalties from You for the exercise of the Licensed Rights, whether directly or through a collecting society under any voluntary or waivable statutory or compulsory licensing scheme. In all other cases the Licensor expressly reserves any right to collect such royalties.
Section 3 License Conditions.
Your exercise of the Licensed Rights is expressly made subject to the following conditions.
a. Attribution.
1. If You Share the Licensed Material (including in modified form), You must:
A. retain the following if it is supplied by the Licensor with the Licensed Material:
i. identification of the creator(s) of the Licensed Material and any others designated to receive attribution, in any reasonable manner requested by the Licensor (including by pseudonym if designated);
ii. a copyright notice;
iii. a notice that refers to this Public License;
iv. a notice that refers to the disclaimer of warranties;
v. a URI or hyperlink to the Licensed Material to the extent reasonably practicable;
B. indicate if You modified the Licensed Material and retain an indication of any previous modifications; and
C. indicate the Licensed Material is licensed under this Public License, and include the text of, or the URI or hyperlink to, this Public License.
2. You may satisfy the conditions in Section 3(a)(1) in any reasonable manner based on the medium, means, and context in which You Share the Licensed Material. For example, it may be reasonable to satisfy the conditions by providing a URI or hyperlink to a resource that includes the required information.
3. If requested by the Licensor, You must remove any of the information required by Section 3(a)(1)(A) to the extent reasonably practicable.
b. ShareAlike.In addition to the conditions in Section 3(a), if You Share Adapted Material You produce, the following conditions also apply.
1. The Adapters License You apply must be a Creative Commons license with the same License Elements, this version or later, or a BY-SA Compatible License.
2. You must include the text of, or the URI or hyperlink to, the Adapter's License You apply. You may satisfy this condition in any reasonable manner based on the medium, means, and context in which You Share Adapted Material.
3. You may not offer or impose any additional or different terms or conditions on, or apply any Effective Technological Measures to, Adapted Material that restrict exercise of the rights granted under the Adapter's License You apply.
Section 4 Sui Generis Database Rights.
Where the Licensed Rights include Sui Generis Database Rights that apply to Your use of the Licensed Material:
a. for the avoidance of doubt, Section 2(a)(1) grants You the right to extract, reuse, reproduce, and Share all or a substantial portion of the contents of the database;
b. if You include all or a substantial portion of the database contents in a database in which You have Sui Generis Database Rights, then the database in which You have Sui Generis Database Rights (but not its individual contents) is Adapted Material, including for purposes of Section 3(b); and
c. You must comply with the conditions in Section 3(a) if You Share all or a substantial portion of the contents of the database.
For the avoidance of doubt, this Section 4 supplements and does not replace Your obligations under this Public License where the Licensed Rights include other Copyright and Similar Rights.
Section 5 Disclaimer of Warranties and Limitation of Liability.
a. Unless otherwise separately undertaken by the Licensor, to the extent possible, the Licensor offers the Licensed Material as-is and as-available, and makes no representations or warranties of any kind concerning the Licensed Material, whether express, implied, statutory, or other. This includes, without limitation, warranties of title, merchantability, fitness for a particular purpose, non-infringement, absence of latent or other defects, accuracy, or the presence or absence of errors, whether or not known or discoverable. Where disclaimers of warranties are not allowed in full or in part, this disclaimer may not apply to You.
b. To the extent possible, in no event will the Licensor be liable to You on any legal theory (including, without limitation, negligence) or otherwise for any direct, special, indirect, incidental, consequential, punitive, exemplary, or other losses, costs, expenses, or damages arising out of this Public License or use of the Licensed Material, even if the Licensor has been advised of the possibility of such losses, costs, expenses, or damages. Where a limitation of liability is not allowed in full or in part, this limitation may not apply to You.
c. The disclaimer of warranties and limitation of liability provided above shall be interpreted in a manner that, to the extent possible, most closely approximates an absolute disclaimer and waiver of all liability.
Section 6 Term and Termination.
a. This Public License applies for the term of the Copyright and Similar Rights licensed here. However, if You fail to comply with this Public License, then Your rights under this Public License terminate automatically.
b. Where Your right to use the Licensed Material has terminated under Section 6(a), it reinstates:
1. automatically as of the date the violation is cured, provided it is cured within 30 days of Your discovery of the violation; or
2. upon express reinstatement by the Licensor.
c. For the avoidance of doubt, this Section 6(b) does not affect any right the Licensor may have to seek remedies for Your violations of this Public License.
d. For the avoidance of doubt, the Licensor may also offer the Licensed Material under separate terms or conditions or stop distributing the Licensed Material at any time; however, doing so will not terminate this Public License.
e. Sections 1, 5, 6, 7, and 8 survive termination of this Public License.
Section 7 Other Terms and Conditions.
a. The Licensor shall not be bound by any additional or different terms or conditions communicated by You unless expressly agreed.
b. Any arrangements, understandings, or agreements regarding the Licensed Material not stated herein are separate from and independent of the terms and conditions of this Public License.
Section 8 Interpretation.
a. For the avoidance of doubt, this Public License does not, and shall not be interpreted to, reduce, limit, restrict, or impose conditions on any use of the Licensed Material that could lawfully be made without permission under this Public License.
b. To the extent possible, if any provision of this Public License is deemed unenforceable, it shall be automatically reformed to the minimum extent necessary to make it enforceable. If the provision cannot be reformed, it shall be severed from this Public License without affecting the enforceability of the remaining terms and conditions.
c. No term or condition of this Public License will be waived and no failure to comply consented to unless expressly agreed to by the Licensor.
d. Nothing in this Public License constitutes or may be interpreted as a limitation upon, or waiver of, any privileges and immunities that apply to the Licensor or You, including from the legal processes of any jurisdiction or authority.
Creative Commons is not a party to its public licenses. Notwithstanding, Creative Commons may elect to apply one of its public licenses to material it publishes and in those instances will be considered the “Licensor.” Except for the limited purpose of indicating that material is shared under a Creative Commons public license or as otherwise permitted by the Creative Commons policies published at creativecommons.org/policies, Creative Commons does not authorize the use of the trademark “Creative Commons” or any other trademark or logo of Creative Commons without its prior written consent including, without limitation, in connection with any unauthorized modifications to any of its public licenses or any other arrangements, understandings, or agreements concerning use of licensed material. For the avoidance of doubt, this paragraph does not form part of the public licenses.
Creative Commons may be contacted at creativecommons.org.

View File

@ -0,0 +1,4 @@
For license and usage guidelines on the seL4 trademark and logo, including
the seL4 Foundation logo, see https://sel4.systems/Foundation/Trademark/
No further license is granted from use in this repository.

View File

@ -0,0 +1,106 @@
<?xml version="1.0" ?>
<!--
Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
SPDX-License-Identifier: BSD-2-Clause
-->
<!-- Please see syscalls.xsd to see the format of this file -->
<syscalls>
<!-- official API syscalls -->
<api-master>
<config>
<syscall name="Call" />
<syscall name="ReplyRecv" />
<syscall name="Send" />
<syscall name="NBSend" />
<syscall name="Recv" />
<syscall name="Reply" />
<syscall name="Yield" />
<syscall name="NBRecv" />
</config>
</api-master>
<api-mcs>
<config>
<syscall name="Call" />
<syscall name="ReplyRecv" />
<syscall name="NBSendRecv" />
<syscall name="NBSendWait" />
<syscall name="Send" />
<syscall name="NBSend" />
<syscall name="Recv" />
<syscall name="NBRecv" />
<syscall name="Wait" />
<syscall name="NBWait" />
<syscall name="Yield" />
</config>
</api-mcs>
<!-- Syscalls on the unknown syscall path. These definitions will be wrapped in #if condition -->
<debug>
<config>
<condition><config var="CONFIG_PRINTING"/></condition>
<syscall name="DebugPutChar" />
<syscall name="DebugDumpScheduler" />
</config>
<config>
<condition><config var="CONFIG_DEBUG_BUILD"/></condition>
<syscall name="DebugHalt" />
<syscall name="DebugCapIdentify" />
<syscall name="DebugSnapshot" />
<syscall name="DebugNameThread"/>
</config>
<config>
<condition>
<and>
<config var="CONFIG_DEBUG_BUILD"/>
<config var="CONFIG_ENABLE_SMP_SUPPORT"/>
</and>
</condition>
<syscall name="DebugSendIPI"/>
</config>
<config>
<condition><config var="CONFIG_DANGEROUS_CODE_INJECTION"/></condition>
<syscall name="DebugRun"/>
</config>
<config>
<condition><config var="CONFIG_ENABLE_BENCHMARKS"/></condition>
<syscall name="BenchmarkFlushCaches" />
<syscall name="BenchmarkResetLog" />
<syscall name="BenchmarkFinalizeLog" />
<syscall name="BenchmarkSetLogBuffer" />
<syscall name="BenchmarkNullSyscall" />
</config>
<config>
<condition><config var="CONFIG_BENCHMARK_TRACK_UTILISATION"/></condition>
<syscall name="BenchmarkGetThreadUtilisation" />
<syscall name="BenchmarkResetThreadUtilisation" />
</config>
<config>
<condition>
<and>
<config var="CONFIG_DEBUG_BUILD"/>
<config var="CONFIG_BENCHMARK_TRACK_UTILISATION"/>
</and>
</condition>
<syscall name="BenchmarkDumpAllThreadsUtilisation" />
<syscall name="BenchmarkResetAllThreadsUtilisation" />
</config>
<config>
<condition><config var="CONFIG_KERNEL_X86_DANGEROUS_MSR"/></condition>
<syscall name="X86DangerousWRMSR"/>
<syscall name="X86DangerousRDMSR"/>
</config>
<!-- This is not a debug syscall, but it needs to not appear in the 'API' syscall list
so that the check of 'is this a valid syscall' can remain a simple range check.
Therefore we'll put this here and the arch code will handle it before
passing to handleUnknownSyscall -->
<config>
<condition><config var="CONFIG_VTX"/></condition>
<syscall name="VMEnter"/>
</config>
<config>
<condition><config var="CONFIG_SET_TLS_BASE_SELF"/></condition>
<syscall name="SetTLSBase"/>
</config>
</debug>
</syscalls>

View File

@ -0,0 +1,71 @@
<xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema">
<!--
Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
SPDX-License-Identifier: BSD-2-Clause
-->
<xsd:annotation>
<xsd:documentation xml:lang="en">
Syscall number generator schema.
</xsd:documentation>
</xsd:annotation>
<xsd:element name="syscalls" type="SyscallListType" />
<xsd:complexType name="SyscallListType">
<xsd:sequence>
<xsd:element name="api-master" type="ApiType" />
<xsd:element name="api-mcs" type="ApiType" />
<xsd:element name="debug" type="DebugType" />
</xsd:sequence>
</xsd:complexType>
<xsd:complexType name="ApiType">
<xsd:sequence>
<xsd:element name="config" minOccurs="1" maxOccurs="unbounded" type="ConfigType" />
</xsd:sequence>
</xsd:complexType>
<xsd:complexType name="DebugType">
<xsd:sequence>
<xsd:element name="config" type="ConfigType" maxOccurs="unbounded"/>
</xsd:sequence>
</xsd:complexType>
<xsd:complexType name="ConfigType" >
<xsd:sequence>
<xsd:element name="condition" minOccurs="0" maxOccurs="1" type="Unary"/>
<xsd:element name="syscall" minOccurs="1" maxOccurs="unbounded" type="SyscallType"/>
</xsd:sequence>
</xsd:complexType>
<xsd:group name="ConfigGroup">
<xsd:choice>
<xsd:element name="and" type="N-ary" />
<xsd:element name="or" type="N-ary" />
<xsd:element name="not" type="Unary" />
<xsd:element name="config">
<xsd:complexType>
<xsd:attribute name="var" type="xsd:string" use="required"/>
</xsd:complexType>
</xsd:element>
</xsd:choice>
</xsd:group>
<xsd:complexType name="Unary">
<xsd:group ref="ConfigGroup"/>
</xsd:complexType>
<xsd:complexType name="N-ary">
<xsd:sequence>
<xsd:group ref="ConfigGroup" minOccurs="2" maxOccurs="unbounded"/>
</xsd:sequence>
</xsd:complexType>
<xsd:complexType name="SyscallType">
<xsd:attribute name="name" type="xsd:string" />
</xsd:complexType>
</xsd:schema>

View File

@ -0,0 +1,5 @@
#pragma once
#include <kernel/gen_config.h>
#include <sel4/gen_config.h>

View File

@ -0,0 +1,236 @@
<?xml version="1.0" ?>
<!--
Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
SPDX-License-Identifier: BSD-2-Clause
-->
<api name="ObjectApiAarch64" label_prefix="aarch64_">
<struct name="seL4_UserContext">
<member name="pc"/>
<member name="sp"/>
<member name="spsr"/>
<member name="x0"/>
<member name="x1"/>
<member name="x2"/>
<member name="x3"/>
<member name="x4"/>
<member name="x5"/>
<member name="x6"/>
<member name="x7"/>
<member name="x8"/>
<member name="x16"/>
<member name="x17"/>
<member name="x18"/>
<member name="x29"/>
<member name="x30"/>
<member name="x9"/>
<member name="x10"/>
<member name="x11"/>
<member name="x12"/>
<member name="x13"/>
<member name="x14"/>
<member name="x15"/>
<member name="x19"/>
<member name="x20"/>
<member name="x21"/>
<member name="x22"/>
<member name="x23"/>
<member name="x24"/>
<member name="x25"/>
<member name="x26"/>
<member name="x27"/>
<member name="x28"/>
<member name="tpidr_el0"/>
<member name="tpidrro_el0"/>
</struct>
<struct name="seL4_ARM_SMCContext">
<member name="x0"/>
<member name="x1"/>
<member name="x2"/>
<member name="x3"/>
<member name="x4"/>
<member name="x5"/>
<member name="x6"/>
<member name="x7"/>
</struct>
<interface name="seL4_ARM_VSpace" manual_name="Page Global Directory"
cap_description="Capability to the top level translation table being operated on.">
<method id="ARMVSpaceClean_Data" name="Clean_Data" manual_label="vspace_clean"
manual_name="Clean Data">
<brief>
Clean cached pages within a top level translation table
</brief>
<description>
<docref>See <autoref label="ch:vspace"/>.</docref>
</description>
<param dir="in" name="start" type="seL4_Word"
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_FailedLookup">
<description>
The <texttt text="_service"/> 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.
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">
<brief>
Invalidate cached pages within a top level translation table
</brief>
<description>
<docref>See <autoref label="ch:vspace"/>.</docref>
</description>
<param dir="in" name="start" type="seL4_Word"
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_FailedLookup">
<description>
The <texttt text="_service"/> 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.
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">
<brief>
Clean and invalidate cached pages within a top level translation table
</brief>
<description>
<docref>See <autoref label="ch:vspace"/>.</docref>
</description>
<param dir="in" name="start" type="seL4_Word"
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_FailedLookup">
<description>
The <texttt text="_service"/> 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.
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">
<brief>
Clean and invalidate cached instruction pages to point of unification
</brief>
<description>
<docref>See <autoref label="ch:vspace"/>.</docref>
</description>
<param dir="in" name="start" type="seL4_Word"
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_FailedLookup">
<description>
The <texttt text="_service"/> 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.
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_SMC" manual_name="SMC" cap_description="Capability to allow threads to make Secure Monitor Calls.">
<method id="ARMSMCCall" name="Call" manual_name="SMC Call" manual_label="smc_call">
<brief>
Tell the kernel to make the real SMC call.
</brief>
<description>
Takes x0-x7 as arguments to an SMC call which are defined as a seL4_ARM_SMCContext
struct. The kernel makes the SMC call and then returns the results as a
new seL4_ARM_SMCContext.
</description>
<param dir="in" name="smc_args" type="seL4_ARM_SMCContext"
description="The structure that has the provided arguments."/>
<param dir="out" name="smc_response" type="seL4_ARM_SMCContext"
description="The structure to capture the responses."/>
</method>
</interface>
</api>

View File

@ -0,0 +1,135 @@
#pragma once
#define CONFIG_ARM_HIKEY_OUTSTANDING_PREFETCHERS 0
#define CONFIG_ARM_HIKEY_PREFETCHER_STRIDE 0
#define CONFIG_ARM_HIKEY_PREFETCHER_NPFSTRM 0
/* disabled: CONFIG_ARM_HIKEY_PREFETCHER_STBPFDIS */
/* disabled: CONFIG_ARM_HIKEY_PREFETCHER_STBPFRS */
/* disabled: CONFIG_PLAT_IMX7 */
/* disabled: CONFIG_ARCH_AARCH32 */
#define CONFIG_ARCH_AARCH64 1
/* disabled: CONFIG_ARCH_ARM_HYP */
/* disabled: CONFIG_ARCH_RISCV32 */
/* disabled: CONFIG_ARCH_RISCV64 */
/* disabled: CONFIG_ARCH_X86_64 */
/* disabled: CONFIG_ARCH_IA32 */
#define CONFIG_SEL4_ARCH aarch64
#define CONFIG_ARCH_ARM 1
#define CONFIG_ARCH arm
#define CONFIG_WORD_SIZE 64
#define CONFIG_ARM_PLAT imx8mm-evk
/* disabled: CONFIG_PLAT_BCM2711 */
/* disabled: CONFIG_PLAT_BCM2837 */
/* disabled: CONFIG_PLAT_FVP */
/* disabled: CONFIG_PLAT_HIKEY */
/* disabled: CONFIG_PLAT_IMX8MQ_EVK */
#define CONFIG_PLAT_IMX8MM_EVK 1
/* disabled: CONFIG_PLAT_IMX8MP_EVK */
/* disabled: CONFIG_PLAT_MAAXBOARD */
/* disabled: CONFIG_PLAT_ODROIDC2 */
/* disabled: CONFIG_PLAT_ODROIDC4 */
/* disabled: CONFIG_PLAT_QEMU_ARM_VIRT */
/* disabled: CONFIG_PLAT_QUARTZ64 */
/* disabled: CONFIG_PLAT_ROCKPRO64 */
/* disabled: CONFIG_PLAT_TQMA8XQP1GB */
/* disabled: CONFIG_PLAT_TX1 */
/* disabled: CONFIG_PLAT_TX2 */
/* disabled: CONFIG_PLAT_ZYNQMP */
#define CONFIG_PLAT imx8mm-evk
/* disabled: CONFIG_ARM_CORTEX_A7 */
/* disabled: CONFIG_ARM_CORTEX_A8 */
/* disabled: CONFIG_ARM_CORTEX_A9 */
/* disabled: CONFIG_ARM_CORTEX_A15 */
/* disabled: CONFIG_ARM_CORTEX_A35 */
#define CONFIG_ARM_CORTEX_A53 1
/* disabled: CONFIG_ARM_CORTEX_A55 */
/* disabled: CONFIG_ARM_CORTEX_A57 */
/* disabled: CONFIG_ARM_CORTEX_A72 */
/* disabled: CONFIG_ARCH_ARM_V7A */
/* disabled: CONFIG_ARCH_ARM_V7VE */
#define CONFIG_ARCH_ARM_V8A 1
/* disabled: CONFIG_AARCH64_SERROR_IGNORE */
#define CONFIG_ARM_MACH imx
#define CONFIG_KERNEL_MCS 1
#define CONFIG_ARM_PA_SIZE_BITS_40 1
/* disabled: CONFIG_ARM_PA_SIZE_BITS_44 */
#define CONFIG_ARM_ICACHE_VIPT 1
/* disabled: CONFIG_DEBUG_DISABLE_L2_CACHE */
/* disabled: CONFIG_DEBUG_DISABLE_L1_ICACHE */
/* disabled: CONFIG_DEBUG_DISABLE_L1_DCACHE */
/* disabled: CONFIG_DEBUG_DISABLE_BRANCH_PREDICTION */
#define CONFIG_ARM_HYPERVISOR_SUPPORT 1
#define CONFIG_ARM_GIC_V3_SUPPORT 1
/* disabled: CONFIG_AARCH64_VSPACE_S2_START_L1 */
/* disabled: CONFIG_ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE */
/* disabled: CONFIG_ARM_ERRATA_430973 */
/* disabled: CONFIG_ARM_ERRATA_773022 */
/* disabled: CONFIG_ARM_SMMU */
/* disabled: CONFIG_TK1_SMMU */
/* disabled: CONFIG_ENABLE_A9_PREFETCHER */
#define CONFIG_EXPORT_PMU_USER 1
/* disabled: CONFIG_DISABLE_WFI_WFE_TRAPS */
/* disabled: CONFIG_SMMU_INTERRUPT_ENABLE */
/* disabled: CONFIG_AARCH32_FPU_ENABLE_CONTEXT_SWITCH */
#define CONFIG_AARCH64_USER_CACHE_ENABLE 1
/* disabled: CONFIG_ALLOW_SMC_CALLS */
#define CONFIG_L1_CACHE_LINE_SIZE_BITS 6
#define CONFIG_EXPORT_PCNT_USER 1
/* disabled: CONFIG_EXPORT_VCNT_USER */
/* disabled: CONFIG_EXPORT_PTMR_USER */
/* disabled: CONFIG_EXPORT_VTMR_USER */
/* disabled: CONFIG_VTIMER_UPDATE_VOFFSET */
#define CONFIG_HAVE_FPU 1
#define CONFIG_PADDR_USER_DEVICE_TOP 1099511627776
#define CONFIG_ROOT_CNODE_SIZE_BITS 12
#define CONFIG_BOOT_THREAD_TIME_SLICE 5
#define CONFIG_RETYPE_FAN_OUT_LIMIT 256
#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100
#define CONFIG_RESET_CHUNK_BITS 8
#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 230
#define CONFIG_FASTPATH 1
/* disabled: CONFIG_EXCEPTION_FASTPATH */
#define CONFIG_NUM_DOMAINS 1
/* disabled: CONFIG_SIGNAL_FASTPATH */
#define CONFIG_NUM_PRIORITIES 256
#define CONFIG_MAX_NUM_NODES 1
/* disabled: CONFIG_ENABLE_SMP_SUPPORT */
#define CONFIG_KERNEL_STACK_BITS 12
#define CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH 64
/* disabled: CONFIG_VERIFICATION_BUILD */
/* disabled: CONFIG_BINARY_VERIFICATION_BUILD */
/* disabled: CONFIG_DEBUG_BUILD */
/* disabled: CONFIG_HARDWARE_DEBUG_API */
/* disabled: CONFIG_PRINTING */
/* disabled: CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC */
/* disabled: CONFIG_NO_BENCHMARKS */
/* disabled: CONFIG_BENCHMARK_GENERIC */
/* disabled: CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES */
/* disabled: CONFIG_BENCHMARK_TRACEPOINTS */
#define CONFIG_BENCHMARK_TRACK_UTILISATION 1
#define CONFIG_KERNEL_BENCHMARK track_utilisation
#define CONFIG_ENABLE_BENCHMARKS 1
/* disabled: CONFIG_KERNEL_LOG_BUFFER */
#define CONFIG_MAX_NUM_TRACE_POINTS 0
/* disabled: CONFIG_IRQ_REPORTING */
/* disabled: CONFIG_COLOUR_PRINTING */
#define CONFIG_USER_STACK_TRACE_LENGTH 0
#define CONFIG_KERNEL_OPT_LEVEL_O2 1
/* disabled: CONFIG_KERNEL_OPT_LEVEL_OS */
/* disabled: CONFIG_KERNEL_OPT_LEVEL_O0 */
/* disabled: CONFIG_KERNEL_OPT_LEVEL_O1 */
/* disabled: CONFIG_KERNEL_OPT_LEVEL_O3 */
#define CONFIG_KERNEL_OPT_LEVEL -O2
#define CONFIG_KERNEL_OPTIMISATION_CLONE_FUNCTIONS 1
/* disabled: CONFIG_KERNEL_FWHOLE_PROGRAM */
/* disabled: CONFIG_DANGEROUS_CODE_INJECTION */
/* disabled: CONFIG_DEBUG_DISABLE_PREFETCHERS */
/* disabled: CONFIG_SET_TLS_BASE_SELF */
#define CONFIG_KERNEL_WCET_SCALE 1
#define CONFIG_KERNEL_STATIC_MAX_PERIOD_US 0
/* disabled: CONFIG_CLZ_32 */
/* disabled: CONFIG_CLZ_64 */
/* disabled: CONFIG_CTZ_32 */
/* disabled: CONFIG_CTZ_64 */
/* disabled: CONFIG_CLZ_NO_BUILTIN */
/* disabled: CONFIG_CTZ_NO_BUILTIN */

View File

@ -0,0 +1,135 @@
{
"ARM_HIKEY_OUTSTANDING_PREFETCHERS": "0",
"ARM_HIKEY_PREFETCHER_STRIDE": "0",
"ARM_HIKEY_PREFETCHER_NPFSTRM": "0",
"ARM_HIKEY_PREFETCHER_STBPFDIS": false,
"ARM_HIKEY_PREFETCHER_STBPFRS": false,
"PLAT_IMX7": false,
"ARCH_AARCH32": false,
"ARCH_AARCH64": true,
"ARCH_ARM_HYP": false,
"ARCH_RISCV32": false,
"ARCH_RISCV64": false,
"ARCH_X86_64": false,
"ARCH_IA32": false,
"SEL4_ARCH": "aarch64",
"ARCH_ARM": true,
"ARCH": "arm",
"WORD_SIZE": "64",
"ARM_PLAT": "imx8mm-evk",
"PLAT_BCM2711": false,
"PLAT_BCM2837": false,
"PLAT_FVP": false,
"PLAT_HIKEY": false,
"PLAT_IMX8MQ_EVK": false,
"PLAT_IMX8MM_EVK": true,
"PLAT_IMX8MP_EVK": false,
"PLAT_MAAXBOARD": false,
"PLAT_ODROIDC2": false,
"PLAT_ODROIDC4": false,
"PLAT_QEMU_ARM_VIRT": false,
"PLAT_QUARTZ64": false,
"PLAT_ROCKPRO64": false,
"PLAT_TQMA8XQP1GB": false,
"PLAT_TX1": false,
"PLAT_TX2": false,
"PLAT_ZYNQMP": false,
"PLAT": "imx8mm-evk",
"ARM_CORTEX_A7": false,
"ARM_CORTEX_A8": false,
"ARM_CORTEX_A9": false,
"ARM_CORTEX_A15": false,
"ARM_CORTEX_A35": false,
"ARM_CORTEX_A53": true,
"ARM_CORTEX_A55": false,
"ARM_CORTEX_A57": false,
"ARM_CORTEX_A72": false,
"ARCH_ARM_V7A": false,
"ARCH_ARM_V7VE": false,
"ARCH_ARM_V8A": true,
"AARCH64_SERROR_IGNORE": false,
"ARM_MACH": "imx",
"KERNEL_MCS": true,
"ARM_PA_SIZE_BITS_40": true,
"ARM_PA_SIZE_BITS_44": false,
"ARM_ICACHE_VIPT": true,
"DEBUG_DISABLE_L2_CACHE": false,
"DEBUG_DISABLE_L1_ICACHE": false,
"DEBUG_DISABLE_L1_DCACHE": false,
"DEBUG_DISABLE_BRANCH_PREDICTION": false,
"ARM_HYPERVISOR_SUPPORT": true,
"ARM_GIC_V3_SUPPORT": true,
"AARCH64_VSPACE_S2_START_L1": false,
"ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE": false,
"ARM_ERRATA_430973": false,
"ARM_ERRATA_773022": false,
"ARM_SMMU": false,
"TK1_SMMU": false,
"ENABLE_A9_PREFETCHER": false,
"EXPORT_PMU_USER": true,
"DISABLE_WFI_WFE_TRAPS": false,
"SMMU_INTERRUPT_ENABLE": false,
"AARCH32_FPU_ENABLE_CONTEXT_SWITCH": false,
"AARCH64_USER_CACHE_ENABLE": true,
"ALLOW_SMC_CALLS": false,
"L1_CACHE_LINE_SIZE_BITS": "6",
"EXPORT_PCNT_USER": true,
"EXPORT_VCNT_USER": false,
"EXPORT_PTMR_USER": false,
"EXPORT_VTMR_USER": false,
"VTIMER_UPDATE_VOFFSET": false,
"HAVE_FPU": true,
"PADDR_USER_DEVICE_TOP": "1099511627776",
"ROOT_CNODE_SIZE_BITS": "12",
"BOOT_THREAD_TIME_SLICE": "5",
"RETYPE_FAN_OUT_LIMIT": "256",
"MAX_NUM_WORK_UNITS_PER_PREEMPTION": "100",
"RESET_CHUNK_BITS": "8",
"MAX_NUM_BOOTINFO_UNTYPED_CAPS": "230",
"FASTPATH": true,
"EXCEPTION_FASTPATH": false,
"NUM_DOMAINS": "1",
"SIGNAL_FASTPATH": false,
"NUM_PRIORITIES": "256",
"MAX_NUM_NODES": "1",
"ENABLE_SMP_SUPPORT": false,
"KERNEL_STACK_BITS": "12",
"FPU_MAX_RESTORES_SINCE_SWITCH": "64",
"VERIFICATION_BUILD": false,
"BINARY_VERIFICATION_BUILD": false,
"DEBUG_BUILD": false,
"HARDWARE_DEBUG_API": false,
"PRINTING": false,
"KERNEL_INVOCATION_REPORT_ERROR_IPC": false,
"NO_BENCHMARKS": false,
"BENCHMARK_GENERIC": false,
"BENCHMARK_TRACK_KERNEL_ENTRIES": false,
"BENCHMARK_TRACEPOINTS": false,
"BENCHMARK_TRACK_UTILISATION": true,
"KERNEL_BENCHMARK": "track_utilisation",
"ENABLE_BENCHMARKS": true,
"KERNEL_LOG_BUFFER": false,
"MAX_NUM_TRACE_POINTS": "0",
"IRQ_REPORTING": false,
"COLOUR_PRINTING": false,
"USER_STACK_TRACE_LENGTH": "0",
"KERNEL_OPT_LEVEL_O2": true,
"KERNEL_OPT_LEVEL_OS": false,
"KERNEL_OPT_LEVEL_O0": false,
"KERNEL_OPT_LEVEL_O1": false,
"KERNEL_OPT_LEVEL_O3": false,
"KERNEL_OPT_LEVEL": "-O2",
"KERNEL_OPTIMISATION_CLONE_FUNCTIONS": true,
"KERNEL_FWHOLE_PROGRAM": false,
"DANGEROUS_CODE_INJECTION": false,
"DEBUG_DISABLE_PREFETCHERS": false,
"SET_TLS_BASE_SELF": false,
"KERNEL_WCET_SCALE": "1",
"KERNEL_STATIC_MAX_PERIOD_US": "0",
"CLZ_32": false,
"CLZ_64": false,
"CTZ_32": false,
"CTZ_64": false,
"CLZ_NO_BUILTIN": false,
"CTZ_NO_BUILTIN": false
}

View File

@ -0,0 +1,221 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
/* Microkit interface */
#pragma once
#define __thread
#include <sel4/sel4.h>
typedef unsigned int microkit_channel;
typedef unsigned int microkit_child;
typedef seL4_MessageInfo_t microkit_msginfo;
#define MONITOR_EP 5
/* Only valid in the 'benchmark' configuration */
#define TCB_CAP 6
#define BASE_OUTPUT_NOTIFICATION_CAP 10
#define BASE_ENDPOINT_CAP 74
#define BASE_IRQ_CAP 138
#define BASE_TCB_CAP 202
#define BASE_VM_TCB_CAP 266
#define BASE_VCPU_CAP 330
#define MICROKIT_MAX_CHANNELS 62
/* User provided functions */
void init(void);
void notified(microkit_channel ch);
microkit_msginfo protected(microkit_channel ch, microkit_msginfo msginfo);
seL4_Bool fault(microkit_child child, microkit_msginfo msginfo, microkit_msginfo *reply_msginfo);
extern char microkit_name[16];
/* These next three variables are so our PDs can combine a signal with the next Recv syscall */
extern seL4_Bool microkit_have_signal;
extern seL4_CPtr microkit_signal_cap;
extern seL4_MessageInfo_t microkit_signal_msg;
/*
* Output a single character on the debug console.
*/
void microkit_dbg_putc(int c);
/*
* Output a NUL terminated string to the debug console.
*/
void microkit_dbg_puts(const char *s);
static inline void microkit_internal_crash(seL4_Error err)
{
/*
* Currently crash be dereferencing NULL page
*
* Actually derference 'err' which means the crash reporting will have
* `err` as the fault address. A bit of a cute hack. Not a good long term
* solution but good for now.
*/
int *x = (int *)(seL4_Word) err;
*x = 0;
}
static inline void microkit_notify(microkit_channel ch)
{
seL4_Signal(BASE_OUTPUT_NOTIFICATION_CAP + ch);
}
static inline void microkit_irq_ack(microkit_channel ch)
{
seL4_IRQHandler_Ack(BASE_IRQ_CAP + ch);
}
static inline void microkit_pd_restart(microkit_child pd, seL4_Word entry_point)
{
seL4_Error err;
seL4_UserContext ctxt = {0};
ctxt.pc = entry_point;
err = seL4_TCB_WriteRegisters(
BASE_TCB_CAP + pd,
seL4_True,
0, /* No flags */
1, /* writing 1 register */
&ctxt
);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_pd_restart: error writing TCB registers\n");
microkit_internal_crash(err);
}
}
static inline void microkit_pd_stop(microkit_child pd)
{
seL4_Error err;
err = seL4_TCB_Suspend(BASE_TCB_CAP + pd);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_pd_stop: error writing TCB registers\n");
microkit_internal_crash(err);
}
}
static inline microkit_msginfo microkit_ppcall(microkit_channel ch, microkit_msginfo msginfo)
{
return seL4_Call(BASE_ENDPOINT_CAP + ch, msginfo);
}
static inline microkit_msginfo microkit_msginfo_new(seL4_Word label, seL4_Uint16 count)
{
return seL4_MessageInfo_new(label, 0, 0, count);
}
static inline seL4_Word microkit_msginfo_get_label(microkit_msginfo msginfo)
{
return seL4_MessageInfo_get_label(msginfo);
}
static inline seL4_Word microkit_msginfo_get_count(microkit_msginfo msginfo)
{
return seL4_MessageInfo_get_length(msginfo);
}
static void microkit_mr_set(seL4_Uint8 mr, seL4_Word value)
{
seL4_SetMR(mr, value);
}
static seL4_Word microkit_mr_get(seL4_Uint8 mr)
{
return seL4_GetMR(mr);
}
/* The following APIs are only available where the kernel is built as a hypervisor. */
#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT)
static inline void microkit_vcpu_restart(microkit_child vcpu, seL4_Word entry_point)
{
seL4_Error err;
seL4_UserContext ctxt = {0};
ctxt.pc = entry_point;
err = seL4_TCB_WriteRegisters(
BASE_VM_TCB_CAP + vcpu,
seL4_True,
0, /* No flags */
1, /* writing 1 register */
&ctxt
);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_vm_restart: error writing registers\n");
microkit_internal_crash(err);
}
}
static inline void microkit_vcpu_stop(microkit_child vcpu)
{
seL4_Error err;
err = seL4_TCB_Suspend(BASE_VM_TCB_CAP + vcpu);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_vm_stop: error suspending TCB\n");
microkit_internal_crash(err);
}
}
static inline void microkit_vcpu_arm_inject_irq(microkit_child vcpu, seL4_Uint16 irq, seL4_Uint8 priority,
seL4_Uint8 group, seL4_Uint8 index)
{
seL4_Error err;
err = seL4_ARM_VCPU_InjectIRQ(BASE_VCPU_CAP + vcpu, irq, priority, group, index);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_arm_vcpu_inject_irq: error injecting IRQ\n");
microkit_internal_crash(err);
}
}
static inline void microkit_vcpu_arm_ack_vppi(microkit_child vcpu, seL4_Word irq)
{
seL4_Error err;
err = seL4_ARM_VCPU_AckVPPI(BASE_VCPU_CAP + vcpu, irq);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_arm_vcpu_ack_vppi: error acking VPPI\n");
microkit_internal_crash(err);
}
}
static inline seL4_Word microkit_vcpu_arm_read_reg(microkit_child vcpu, seL4_Word reg)
{
seL4_ARM_VCPU_ReadRegs_t ret;
ret = seL4_ARM_VCPU_ReadRegs(BASE_VCPU_CAP + vcpu, reg);
if (ret.error != seL4_NoError) {
microkit_dbg_puts("microkit_arm_vcpu_read_reg: error reading vCPU register\n");
microkit_internal_crash(ret.error);
}
return ret.value;
}
static inline void microkit_vcpu_arm_write_reg(microkit_child vcpu, seL4_Word reg, seL4_Word value)
{
seL4_Error err;
err = seL4_ARM_VCPU_WriteRegs(BASE_VCPU_CAP + vcpu, reg, value);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_arm_vcpu_write_reg: error writing vCPU register\n");
microkit_internal_crash(err);
}
}
#endif
static inline void microkit_deferred_notify(microkit_channel ch)
{
microkit_have_signal = seL4_True;
microkit_signal_msg = seL4_MessageInfo_new(0, 0, 0, 0);
microkit_signal_cap = (BASE_OUTPUT_NOTIFICATION_CAP + ch);
}
static inline void microkit_deferred_irq_ack(microkit_channel ch)
{
microkit_have_signal = seL4_True;
microkit_signal_msg = seL4_MessageInfo_new(IRQAckIRQ, 0, 0, 0);
microkit_signal_cap = (BASE_IRQ_CAP + ch);
}

View File

@ -0,0 +1,8 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A15)
#error CONFIG_ARM_CORTEX_A15 is not defined
#endif
/* Cortex-A15 Manual, Section 10.2.2 */
#define seL4_NumHWBreakpoints 10
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A35)
#error CONFIG_ARM_CORTEX_A35 is not defined
#endif
/* Cortex-A35 Manual, Table C7.1 */
#define seL4_NumHWBreakpoints 6
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A53)
#error CONFIG_ARM_CORTEX_A53 is not defined
#endif
/* Cortex-A53 Manual, Section 11.6.1 */
#define seL4_NumHWBreakpoints 10
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A55)
#error CONFIG_ARM_CORTEX_A55 is not defined
#endif
/* Cortex-A55 Manual */
#define seL4_NumHWBreakpoints 10
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A57)
#error CONFIG_ARM_CORTEX_A57 is not defined
#endif
/* Cortex-A57 Manual, Section 10.6.1 */
#define seL4_NumHWBreakpoints 10
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A7)
#error CONFIG_ARM_CORTEX_A7 is not defined
#endif
/* Cortex-A7 Manual, Table 10-2 */
#define seL4_NumHWBreakpoints 10
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A72)
#error CONFIG_ARM_CORTEX_A72 is not defined
#endif
/* Cortex-A72 Manual, Section 10.3 */
#define seL4_NumHWBreakpoints 10
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A8)
#error CONFIG_ARM_CORTEX_A8 is not defined
#endif
/* Cortex-A8 Manual, Table 12-11 */
#define seL4_NumHWBreakpoints 8
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 2
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A9)
#error CONFIG_ARM_CORTEX_A9 is not defined
#endif
/* Cortex-A9 Manual, Section 10.1.2 */
#define seL4_NumHWBreakpoints 10
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,11 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
/* nothing here */

View File

@ -0,0 +1,91 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
** SPDX-License-Identifier: BSD-2-Clause
*/
/* This header was generated by kernel/tools/invocation_header_gen.py.
*
* To add an invocation call number, edit libsel4/include/interfaces/sel4.xml.
*
*/
#pragma once
enum arch_invocation_label {
ARMPageTableMap = nSeL4ArchInvocationLabels,
ARMPageTableUnmap,
#if defined(CONFIG_TK1_SMMU)
ARMIOPageTableMap,
#endif
#if defined(CONFIG_TK1_SMMU)
ARMIOPageTableUnmap,
#endif
ARMPageMap,
ARMPageUnmap,
#if defined(CONFIG_TK1_SMMU)
ARMPageMapIO,
#endif
ARMPageClean_Data,
ARMPageInvalidate_Data,
ARMPageCleanInvalidate_Data,
ARMPageUnify_Instruction,
ARMPageGetAddress,
ARMASIDControlMakePool,
ARMASIDPoolAssign,
#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT)
ARMVCPUSetTCB,
#endif
#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT)
ARMVCPUInjectIRQ,
#endif
#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT)
ARMVCPUReadReg,
#endif
#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT)
ARMVCPUWriteReg,
#endif
#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT)
ARMVCPUAckVPPI,
#endif
ARMIRQIssueIRQHandlerTrigger,
#if defined(CONFIG_ENABLE_SMP_SUPPORT)
ARMIRQIssueIRQHandlerTriggerCore,
#endif
#if defined(CONFIG_ARM_SMMU)
ARMSIDIssueSIDManager,
#endif
#if defined(CONFIG_ARM_SMMU)
ARMSIDGetFault,
#endif
#if defined(CONFIG_ARM_SMMU)
ARMSIDClearFault,
#endif
#if defined(CONFIG_ARM_SMMU)
ARMSIDBindCB,
#endif
#if defined(CONFIG_ARM_SMMU)
ARMSIDUnbindCB,
#endif
#if defined(CONFIG_ARM_SMMU)
ARMCBIssueCBManager,
#endif
#if defined(CONFIG_ARM_SMMU)
ARMCBTLBInvalidateAll,
#endif
#if defined(CONFIG_ARM_SMMU)
ARMCBAssignVspace,
#endif
#if defined(CONFIG_ARM_SMMU)
ARMCBUnassignVspace,
#endif
#if defined(CONFIG_ARM_SMMU)
ARMCBTLBInvalidate,
#endif
#if defined(CONFIG_ARM_SMMU)
ARMCBGetFault,
#endif
#if defined(CONFIG_ARM_SMMU)
ARMCBClearFault,
#endif
nArchInvocationLabels
};

View File

@ -0,0 +1,11 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/sel4_arch/mapping.h>

View File

@ -0,0 +1,36 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
typedef enum _object {
seL4_ARM_SmallPageObject = seL4_ModeObjectTypeCount,
seL4_ARM_LargePageObject,
#ifdef CONFIG_ARCH_AARCH32
seL4_ARM_SectionObject,
seL4_ARM_SuperSectionObject,
#endif
seL4_ARM_PageTableObject,
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
seL4_ARM_VCPUObject,
#endif
#ifdef CONFIG_TK1_SMMU
seL4_ARM_IOPageTableObject,
#endif
seL4_ObjectTypeCount
} seL4_ArchObjectType;
typedef seL4_Word object_t;
#ifndef CONFIG_ARM_HYPERVISOR_SUPPORT
#define seL4_ARM_VCPUObject 0xfffe
#endif
#ifndef CONFIG_TK1_SMMU
#define seL4_ARM_IOPageTableObject 0xffff
#endif

View File

@ -0,0 +1,13 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/sel4_arch/constants.h>
#include <sel4/sel4_arch/objecttype.h>
#include <sel4/arch/objecttype.h>

View File

@ -0,0 +1,9 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/sel4_arch/simple_types.h>

View File

@ -0,0 +1,805 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <sel4/functions.h>
#include <sel4/sel4_arch/syscalls.h>
#include <sel4/types.h>
#ifdef CONFIG_KERNEL_MCS
#define LIBSEL4_MCS_REPLY reply
#else
#define LIBSEL4_MCS_REPLY 0
#endif
LIBSEL4_INLINE_FUNC void seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
arm_sys_send(seL4_SysSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
}
LIBSEL4_INLINE_FUNC void seL4_SendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
arm_sys_send(seL4_SysSend, dest, msgInfo.words[0],
mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
);
}
LIBSEL4_INLINE_FUNC void seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
arm_sys_send(seL4_SysNBSend, dest, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
}
LIBSEL4_INLINE_FUNC void seL4_NBSendWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
arm_sys_send(seL4_SysNBSend, dest, msgInfo.words[0],
mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
);
}
#ifndef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC void seL4_Reply(seL4_MessageInfo_t msgInfo)
{
arm_sys_reply(seL4_SysReply, msgInfo.words[0], seL4_GetMR(0), seL4_GetMR(1), seL4_GetMR(2), seL4_GetMR(3));
}
LIBSEL4_INLINE_FUNC void seL4_ReplyWithMRs(seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
arm_sys_reply(seL4_SysReply, msgInfo.words[0],
mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr0 : 0,
mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr1 : 0,
mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr2 : 0,
mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0 ? *mr3 : 0
);
}
#endif
LIBSEL4_INLINE_FUNC void seL4_Signal(seL4_CPtr dest)
{
arm_sys_send_null(seL4_SysSend, dest, seL4_MessageInfo_new(0, 0, 0, 0).words[0]);
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Recv(seL4_CPtr src, seL4_Word *sender)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0;
seL4_Word msg1;
seL4_Word msg2;
seL4_Word msg3;
arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
seL4_SetMR(2, msg2);
seL4_SetMR(3, msg3);
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_RecvWithMRs(seL4_CPtr src, seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
seL4_Word msg2 = 0;
seL4_Word msg3 = 0;
arm_sys_recv(seL4_SysRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
/* Write the message back out to memory. */
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (mr2 != seL4_Null) {
*mr2 = msg2;
}
if (mr3 != seL4_Null) {
*mr3 = msg3;
}
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBRecv(seL4_CPtr src, seL4_Word *sender)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0;
seL4_Word msg1;
seL4_Word msg2;
seL4_Word msg3;
arm_sys_recv(seL4_SysNBRecv, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, LIBSEL4_MCS_REPLY);
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
seL4_SetMR(2, msg2);
seL4_SetMR(3, msg3);
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo)
{
seL4_MessageInfo_t info;
seL4_Word msg0 = seL4_GetMR(0);
seL4_Word msg1 = seL4_GetMR(1);
seL4_Word msg2 = seL4_GetMR(2);
seL4_Word msg3 = seL4_GetMR(3);
arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
/* Write out the data back to memory. */
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
seL4_SetMR(2, msg2);
seL4_SetMR(3, msg3);
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_CallWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
seL4_MessageInfo_t info;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
seL4_Word msg2 = 0;
seL4_Word msg3 = 0;
/* Load beginning of the message into registers. */
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
msg2 = *mr2;
}
if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
msg3 = *mr3;
}
arm_sys_send_recv(seL4_SysCall, dest, &dest, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
/* Write out the data back to memory. */
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (mr2 != seL4_Null) {
*mr2 = msg2;
}
if (mr3 != seL4_Null) {
*mr3 = msg3;
}
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender,
seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0;
seL4_Word msg1;
seL4_Word msg2;
seL4_Word msg3;
/* Load beginning of the message into registers. */
msg0 = seL4_GetMR(0);
msg1 = seL4_GetMR(1);
msg2 = seL4_GetMR(2);
msg3 = seL4_GetMR(3);
arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
LIBSEL4_MCS_REPLY);
/* Write the message back out to memory. */
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
seL4_SetMR(2, msg2);
seL4_SetMR(3, msg3);
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply)
#else
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_ReplyRecvWithMRs(seL4_CPtr src, seL4_MessageInfo_t msgInfo,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
#endif
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
seL4_Word msg2 = 0;
seL4_Word msg3 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
msg2 = *mr2;
}
if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
msg3 = *mr3;
}
arm_sys_send_recv(seL4_SysReplyRecv, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
LIBSEL4_MCS_REPLY);
/* Write out the data back to memory. */
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (mr2 != seL4_Null) {
*mr2 = msg2;
}
if (mr3 != seL4_Null) {
*mr3 = msg3;
}
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
seL4_Word *sender, seL4_CPtr reply)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0;
seL4_Word msg1;
seL4_Word msg2;
seL4_Word msg3;
/* Load beginning of the message into registers. */
msg0 = seL4_GetMR(0);
msg1 = seL4_GetMR(1);
msg2 = seL4_GetMR(2);
msg3 = seL4_GetMR(3);
arm_sys_nbsend_recv(seL4_SysNBSendRecv, dest, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
reply);
/* Write the message back out to memory. */
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
seL4_SetMR(2, msg2);
seL4_SetMR(3, msg3);
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendRecvWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3, seL4_CPtr reply)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
seL4_Word msg2 = 0;
seL4_Word msg3 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
msg2 = *mr2;
}
if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
msg3 = *mr3;
}
arm_sys_nbsend_recv(seL4_SysNBSendRecv, dest, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
reply);
/* Write out the data back to memory. */
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (mr2 != seL4_Null) {
*mr2 = msg2;
}
if (mr3 != seL4_Null) {
*mr3 = msg3;
}
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0;
seL4_Word msg1;
seL4_Word msg2;
seL4_Word msg3;
/* Load beginning of the message into registers. */
msg0 = seL4_GetMR(0);
msg1 = seL4_GetMR(1);
msg2 = seL4_GetMR(2);
msg3 = seL4_GetMR(3);
arm_sys_nbsend_recv(seL4_SysNBSendWait, 0, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
dest);
/* Write the message back out to memory. */
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
seL4_SetMR(2, msg2);
seL4_SetMR(3, msg3);
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBSendWaitWithMRs(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src,
seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
seL4_Word msg2 = 0;
seL4_Word msg3 = 0;
if (mr0 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 0) {
msg0 = *mr0;
}
if (mr1 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 1) {
msg1 = *mr1;
}
if (mr2 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 2) {
msg2 = *mr2;
}
if (mr3 != seL4_Null && seL4_MessageInfo_get_length(msgInfo) > 3) {
msg3 = *mr3;
}
arm_sys_nbsend_recv(seL4_SysNBSendRecv, 0, src, &badge, msgInfo.words[0], &info.words[0], &msg0, &msg1, &msg2, &msg3,
dest);
/* Write out the data back to memory. */
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (mr2 != seL4_Null) {
*mr2 = msg2;
}
if (mr3 != seL4_Null) {
*mr3 = msg3;
}
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
#endif
LIBSEL4_INLINE_FUNC void seL4_Yield(void)
{
arm_sys_null(seL4_SysYield);
asm volatile("" ::: "memory");
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Wait(seL4_CPtr src, seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0;
seL4_Word msg1;
seL4_Word msg2;
seL4_Word msg3;
arm_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
seL4_SetMR(2, msg2);
seL4_SetMR(3, msg3);
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_WaitWithMRs(seL4_CPtr src, seL4_Word *sender,
seL4_Word *mr0, seL4_Word *mr1, seL4_Word *mr2, seL4_Word *mr3)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0 = 0;
seL4_Word msg1 = 0;
seL4_Word msg2 = 0;
seL4_Word msg3 = 0;
arm_sys_recv(seL4_SysWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
/* Write the message back out to memory. */
if (mr0 != seL4_Null) {
*mr0 = msg0;
}
if (mr1 != seL4_Null) {
*mr1 = msg1;
}
if (mr2 != seL4_Null) {
*mr2 = msg2;
}
if (mr3 != seL4_Null) {
*mr3 = msg3;
}
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_NBWait(seL4_CPtr src, seL4_Word *sender)
{
seL4_MessageInfo_t info;
seL4_Word badge;
seL4_Word msg0;
seL4_Word msg1;
seL4_Word msg2;
seL4_Word msg3;
arm_sys_recv(seL4_SysNBWait, src, &badge, &info.words[0], &msg0, &msg1, &msg2, &msg3, 0);
seL4_SetMR(0, msg0);
seL4_SetMR(1, msg1);
seL4_SetMR(2, msg2);
seL4_SetMR(3, msg3);
/* Return back sender and message information. */
if (sender) {
*sender = badge;
}
return info;
}
#endif
#ifdef CONFIG_PRINTING
LIBSEL4_INLINE_FUNC void seL4_DebugPutChar(char c)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
arm_sys_send_recv(seL4_SysDebugPutChar, c, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
}
LIBSEL4_INLINE_FUNC void seL4_DebugPutString(char *str)
{
for (char *s = str; *s; s++) {
seL4_DebugPutChar(*s);
}
return;
}
LIBSEL4_INLINE_FUNC void seL4_DebugDumpScheduler(void)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
arm_sys_send_recv(seL4_SysDebugDumpScheduler, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
}
#endif
#if CONFIG_DEBUG_BUILD
LIBSEL4_INLINE_FUNC void seL4_DebugHalt(void)
{
arm_sys_null(seL4_SysDebugHalt);
}
LIBSEL4_INLINE_FUNC void seL4_DebugSnapshot(void)
{
arm_sys_null(seL4_SysDebugSnapshot);
asm volatile("" ::: "memory");
}
LIBSEL4_INLINE_FUNC seL4_Uint32 seL4_DebugCapIdentify(seL4_CPtr cap)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
arm_sys_send_recv(seL4_SysDebugCapIdentify, cap, &cap, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
return (seL4_Uint32)cap;
}
char *strcpy(char *, const char *);
LIBSEL4_INLINE_FUNC void seL4_DebugNameThread(seL4_CPtr tcb, const char *name)
{
strcpy((char *)seL4_GetIPCBuffer()->msg, name);
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
arm_sys_send_recv(seL4_SysDebugNameThread, tcb, &unused0, 0, &unused1, &unused2, &unused3, &unused4, &unused5, 0);
}
#if CONFIG_ENABLE_SMP_SUPPORT
LIBSEL4_INLINE_FUNC void seL4_DebugSendIPI(seL4_Uint8 target, unsigned irq)
{
arm_sys_send(seL4_SysDebugSendIPI, target, irq, 0, 0, 0, 0);
}
#endif /* CONFIG_ENABLE_SMP_SUPPORT */
#endif
#ifdef CONFIG_DANGEROUS_CODE_INJECTION
LIBSEL4_INLINE_FUNC void seL4_DebugRun(void (* userfn)(void *), void *userarg)
{
arm_sys_send_null(seL4_SysDebugRun, (seL4_Word)userfn, (seL4_Word)userarg);
asm volatile("" ::: "memory");
}
#endif
#ifdef CONFIG_ENABLE_BENCHMARKS
/* set the log index back to 0 */
LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkResetLog(void)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
seL4_Word ret;
arm_sys_send_recv(seL4_SysBenchmarkResetLog, 0, &ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
return (seL4_Error) ret;
}
LIBSEL4_INLINE_FUNC seL4_Word seL4_BenchmarkFinalizeLog(void)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
seL4_Word index_ret;
arm_sys_send_recv(seL4_SysBenchmarkFinalizeLog, 0, &index_ret, 0, &unused0, &unused1, &unused2, &unused3, &unused4, 0);
return (seL4_Word) index_ret;
}
LIBSEL4_INLINE_FUNC seL4_Error seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
arm_sys_send_recv(seL4_SysBenchmarkSetLogBuffer, frame_cptr, &frame_cptr, 0, &unused0, &unused1, &unused2, &unused3,
&unused4, 0);
return (seL4_Error) frame_cptr;
}
LIBSEL4_INLINE_FUNC void seL4_BenchmarkNullSyscall(void)
{
arm_sys_null(seL4_SysBenchmarkNullSyscall);
asm volatile("" ::: "memory");
}
LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushCaches(void)
{
arm_sys_send_null(seL4_SysBenchmarkFlushCaches, 0, 0);
asm volatile("" ::: "memory");
}
LIBSEL4_INLINE_FUNC void seL4_BenchmarkFlushL1Caches(seL4_Word cache_type)
{
arm_sys_send_null(seL4_SysBenchmarkFlushCaches, 1, cache_type);
asm volatile("" ::: "memory");
}
#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
LIBSEL4_INLINE_FUNC void seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
arm_sys_send_recv(seL4_SysBenchmarkGetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3, &unused4,
&unused5, 0);
}
LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
arm_sys_send_recv(seL4_SysBenchmarkResetThreadUtilisation, tcb_cptr, &unused0, 0, &unused1, &unused2, &unused3,
&unused4, &unused5, 0);
}
#ifdef CONFIG_DEBUG_BUILD
LIBSEL4_INLINE_FUNC void seL4_BenchmarkDumpAllThreadsUtilisation(void)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
arm_sys_send_recv(seL4_SysBenchmarkDumpAllThreadsUtilisation, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4,
&unused5, 0);
}
LIBSEL4_INLINE_FUNC void seL4_BenchmarkResetAllThreadsUtilisation(void)
{
seL4_Word unused0 = 0;
seL4_Word unused1 = 0;
seL4_Word unused2 = 0;
seL4_Word unused3 = 0;
seL4_Word unused4 = 0;
seL4_Word unused5 = 0;
arm_sys_send_recv(seL4_SysBenchmarkResetAllThreadsUtilisation, 0, &unused0, 0, &unused1, &unused2, &unused3, &unused4,
&unused5, 0);
}
#endif
#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */
#endif /* CONFIG_ENABLE_BENCHMARKS */
#ifdef CONFIG_SET_TLS_BASE_SELF
LIBSEL4_INLINE_FUNC void seL4_SetTLSBase(seL4_Word tls_base)
{
arm_sys_send_null(seL4_SysSetTLSBase, tls_base, 0);
asm volatile("" ::: "memory");
}
#endif /* CONFIG_SET_TLS_BASE_SELF */
#ifndef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC void seL4_Wait(seL4_CPtr src, seL4_Word *sender)
{
seL4_Recv(src, sender);
}
#endif
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Poll(seL4_CPtr src, seL4_Word *sender)
{
#ifdef CONFIG_KERNEL_MCS
return seL4_NBWait(src, sender);
#else
return seL4_NBRecv(src, sender);
#endif
}

View File

@ -0,0 +1,42 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/macros.h>
#include <sel4/simple_types.h>
#include <sel4/sel4_arch/types.h>
typedef seL4_CPtr seL4_ARM_Page;
typedef seL4_CPtr seL4_ARM_PageTable;
typedef seL4_CPtr seL4_ARM_PageDirectory;
typedef seL4_CPtr seL4_ARM_ASIDControl;
typedef seL4_CPtr seL4_ARM_ASIDPool;
typedef seL4_CPtr seL4_ARM_VCPU;
typedef seL4_CPtr seL4_ARM_IOSpace;
typedef seL4_CPtr seL4_ARM_IOPageTable;
typedef seL4_CPtr seL4_ARM_SIDControl;
typedef seL4_CPtr seL4_ARM_SID;
typedef seL4_CPtr seL4_ARM_CBControl;
typedef seL4_CPtr seL4_ARM_CB;
typedef seL4_CPtr seL4_ARM_SMC;
typedef enum {
seL4_ARM_PageCacheable = 0x01,
seL4_ARM_ParityEnabled = 0x02,
seL4_ARM_Default_VMAttributes = 0x03,
seL4_ARM_ExecuteNever = 0x04,
/* seL4_ARM_PageCacheable | seL4_ARM_ParityEnabled */
SEL4_FORCE_LONG_ENUM(seL4_ARM_VMAttributes),
} seL4_ARM_VMAttributes;
typedef enum {
seL4_ARM_CacheI = 1,
seL4_ARM_CacheD = 2,
seL4_ARM_CacheID = 3,
SEL4_FORCE_LONG_ENUM(seL4_ARM_CacheType),
} seL4_ARM_CacheType;

View File

@ -0,0 +1,43 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
/**
* Declares macros and methods for sel4 specific assert and fail.
*
* These are unconditional, there are conditional versions of
* these in debug_assert.h and are name seL4_DebugAssert and
* sl4_DebugCompileTimeAsssert.
*/
#pragma once
#include <sel4/macros.h>
/**
* Hidden function, use the macros seL4_Fail or seL4_Assert.
*/
void __assert_fail(const char *str, const char *file, int line, const char *function);
/**
* If expr evaluates to false _seL4_Fail is called with the
* expr as a string plus the file, line and function.
*/
#define seL4_Fail(s) __assert_fail(s, __FILE__, __LINE__, __func__)
/**
* If expr evaluates to false _seL4_AssertFail is called with the
* expr as a string plus the file, line and function.
*/
#define seL4_Assert(expr) \
do { if (!(expr)) { __assert_fail(#expr, __FILE__, __LINE__, __func__); } } while(0)
/**
* An assert that tests that the expr is a compile time constant and
* evaluates to true.
*/
#define seL4_CompileTimeAssert(expr) \
SEL4_COMPILE_ASSERT(seL4_CompileTimeAssert, expr)

View File

@ -0,0 +1,16 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#ifdef CONFIG_BENCHMARK_TRACEPOINTS
typedef struct benchmark_tracepoint_log_entry {
seL4_Word id;
seL4_Word duration;
} benchmark_tracepoint_log_entry_t;
#endif /* CONFIG_BENCHMARK_TRACEPOINTS */

View File

@ -0,0 +1,64 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <stdint.h>
#if (defined CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES || defined CONFIG_DEBUG_BUILD)
/* the following code can be used at any point in the kernel
* to determine detail about the kernel entry point */
typedef enum {
Entry_Interrupt,
Entry_UnknownSyscall,
Entry_UserLevelFault,
Entry_DebugFault,
Entry_VMFault,
Entry_Syscall,
Entry_UnimplementedDevice,
#ifdef CONFIG_ARCH_ARM
Entry_VCPUFault,
#endif
#ifdef CONFIG_ARCH_X86
Entry_VMExit,
#endif
} entry_type_t;
/**
* @brief Kernel entry logging
*
* Encapsulates useful info about the cause of the kernel entry
*/
typedef struct SEL4_PACKED kernel_entry {
seL4_Word path: 3;
union {
struct {
seL4_Word core: 3;
seL4_Word word: 26;
};
/* Tracked kernel entry info filled from outside this file */
struct {
seL4_Word syscall_no: 4;
seL4_Word cap_type: 5;
seL4_Word is_fastpath: 1;
seL4_Word invocation_tag: 19;
};
};
} kernel_entry_t;
#endif /* CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES || DEBUG */
#ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES
typedef struct benchmark_syscall_log_entry {
uint64_t start_time;
uint32_t duration;
kernel_entry_t entry;
} benchmark_track_kernel_entry_t;
#endif /* CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES || CONFIG_DEBUG_BUILD */

View File

@ -0,0 +1,45 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
enum benchmark_track_util_ipc_index {
/* TCB cap passed in the syscall */
/* Number of cycles thread spends scheduled */
BENCHMARK_TCB_UTILISATION,
/* Number of times thread is scheduled */
BENCHMARK_TCB_NUMBER_SCHEDULES,
/* Number of cycles thread spends in kernel */
BENCHMARK_TCB_KERNEL_UTILISATION,
/* Number of times thread enters kernel */
BENCHMARK_TCB_NUMBER_KERNEL_ENTRIES,
/* Idle thread */
/* Number of cycles idle thread spends scheduled */
BENCHMARK_IDLE_LOCALCPU_UTILISATION,
BENCHMARK_IDLE_TCBCPU_UTILISATION,
/* Number of times idle thread is scheduled */
BENCHMARK_IDLE_NUMBER_SCHEDULES,
/* Number of cycles idle thread spends in kernel */
BENCHMARK_IDLE_KERNEL_UTILISATION,
/* Number of times idle thread enters kernel */
BENCHMARK_IDLE_NUMBER_KERNEL_ENTRIES,
/* Totals for the current core */
/* Total cycles used by the core for the period */
BENCHMARK_TOTAL_UTILISATION,
/* Total number of times the core schedules a different thread */
BENCHMARK_TOTAL_NUMBER_SCHEDULES,
/* Total cycles spent inside the kernel by the core for the period */
BENCHMARK_TOTAL_KERNEL_UTILISATION,
/* Total number of times the kernel is entered on the current core */
BENCHMARK_TOTAL_NUMBER_KERNEL_ENTRIES,
};
#endif /* CONFIG_BENCHMARK_TRACK_UTILISATION */

View File

@ -0,0 +1,17 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/types.h>
#include <sel4/bootinfo_types.h>
#include <sel4/macros.h>
void seL4_InitBootInfo(seL4_BootInfo *bi)
SEL4_DEPRECATED("libsel4 management of bootinfo is deprecated, see the BootInfo Frame section of the manual");
seL4_BootInfo *seL4_GetBootInfo(void)
SEL4_DEPRECATED("libsel4 management of bootinfo is deprecated, see the BootInfo Frame section of the manual");

View File

@ -0,0 +1,122 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <sel4/macros.h>
#include <sel4/sel4_arch/constants.h>
/* caps with fixed slot positions in the root CNode */
enum seL4_RootCNodeCapSlots {
seL4_CapNull = 0, /* null cap */
seL4_CapInitThreadTCB = 1, /* initial thread's TCB cap */
seL4_CapInitThreadCNode = 2, /* initial thread's root CNode cap */
seL4_CapInitThreadVSpace = 3, /* initial thread's VSpace cap */
seL4_CapIRQControl = 4, /* global IRQ controller cap */
seL4_CapASIDControl = 5, /* global ASID controller cap */
seL4_CapInitThreadASIDPool = 6, /* initial thread's ASID pool cap */
seL4_CapIOPortControl = 7, /* global IO port control cap (null cap if not supported) */
seL4_CapIOSpace = 8, /* global IO space cap (null cap if no IOMMU support) */
seL4_CapBootInfoFrame = 9, /* bootinfo frame cap */
seL4_CapInitThreadIPCBuffer = 10, /* initial thread's IPC buffer frame cap */
seL4_CapDomain = 11, /* global domain controller cap */
seL4_CapSMMUSIDControl = 12, /* global SMMU SID controller cap, null cap if not supported */
seL4_CapSMMUCBControl = 13, /* global SMMU CB controller cap, null cap if not supported */
seL4_CapInitThreadSC = 14, /* initial thread's scheduling context cap, null cap if not supported */
seL4_CapSMC = 15, /* global SMC cap, null cap if not supported */
seL4_NumInitialCaps = 16
};
/* Legacy code will have assumptions on the vspace root being a Page Directory
* type, so for now we define one to the other */
#define seL4_CapInitThreadPD seL4_CapInitThreadVSpace
/* types */
typedef seL4_Word seL4_SlotPos;
typedef struct seL4_SlotRegion {
seL4_SlotPos start; /* first CNode slot position OF region */
seL4_SlotPos end; /* first CNode slot position AFTER region */
} seL4_SlotRegion;
typedef struct seL4_UntypedDesc {
seL4_Word paddr; /* physical address of untyped cap */
seL4_Uint8 sizeBits;/* size (2^n) bytes of each untyped */
seL4_Uint8 isDevice;/* whether the untyped is a device */
seL4_Uint8 padding[sizeof(seL4_Word) - 2 * sizeof(seL4_Uint8)];
} seL4_UntypedDesc;
SEL4_COMPILE_ASSERT(
invalid_seL4_UntypedDesc,
sizeof(seL4_UntypedDesc) == 2 * sizeof(seL4_Word));
typedef struct seL4_BootInfo {
seL4_Word extraLen; /* length of any additional bootinfo information */
seL4_NodeId nodeID; /* ID [0..numNodes-1] of the seL4 node (0 if uniprocessor) */
seL4_Word numNodes; /* number of seL4 nodes (1 if uniprocessor) */
seL4_Word numIOPTLevels; /* number of IOMMU PT levels (0 if no IOMMU support) */
seL4_IPCBuffer *ipcBuffer; /* pointer to initial thread's IPC buffer */
seL4_SlotRegion empty; /* empty slots (null caps) */
seL4_SlotRegion sharedFrames; /* shared-frame caps (shared between seL4 nodes) */
seL4_SlotRegion userImageFrames; /* userland-image frame caps */
seL4_SlotRegion userImagePaging; /* userland-image paging structure caps */
seL4_SlotRegion ioSpaceCaps; /* IOSpace caps for ARM SMMU */
seL4_SlotRegion extraBIPages; /* caps for any pages used to back the additional bootinfo information */
seL4_Word initThreadCNodeSizeBits; /* initial thread's root CNode size (2^n slots) */
seL4_Domain initThreadDomain; /* Initial thread's domain ID */
#ifdef CONFIG_KERNEL_MCS
seL4_SlotRegion schedcontrol; /* Caps to sched_control for each node */
#endif
seL4_SlotRegion untyped; /* untyped-object caps (untyped caps) */
seL4_UntypedDesc untypedList[CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS]; /* information about each untyped */
/* the untypedList should be the last entry in this struct, in order
* to make this struct easier to represent in other languages */
} seL4_BootInfo;
/* The boot info frame must be large enough to hold the seL4_BootInfo data
* structure. Due to internal restrictions, the size must be of the form 2^n and
* the minimum is one page.
*/
#define seL4_BootInfoFrameBits seL4_PageBits
#define seL4_BootInfoFrameSize LIBSEL4_BIT(seL4_BootInfoFrameBits)
SEL4_COMPILE_ASSERT(
invalid_seL4_BootInfoFrameSize,
sizeof(seL4_BootInfo) <= seL4_BootInfoFrameSize)
/* If seL4_BootInfo.extraLen > 0, this indicate the presence of additional boot
* information chunks starting at the offset seL4_BootInfoFrameSize. Userland
* code often contains the hard-coded assumption that the offset is 4 KiByte,
* because the boot info frame usually is one page, which is 4 KiByte on x86,
* Arm and RISC-V.
* The additional boot info chunks are arch/platform specific, they may or may
* not exist in any given execution. Each chunk has a header that contains an ID
* to describe the chunk. All IDs share a global namespace to ensure uniqueness.
*/
typedef enum {
SEL4_BOOTINFO_HEADER_PADDING = 0,
SEL4_BOOTINFO_HEADER_X86_VBE = 1,
SEL4_BOOTINFO_HEADER_X86_MBMMAP = 2,
SEL4_BOOTINFO_HEADER_X86_ACPI_RSDP = 3,
SEL4_BOOTINFO_HEADER_X86_FRAMEBUFFER = 4,
SEL4_BOOTINFO_HEADER_X86_TSC_FREQ = 5, /* frequency is in MHz */
SEL4_BOOTINFO_HEADER_FDT = 6, /* device tree */
/* Add more IDs here, the two elements below must always be at the end. */
SEL4_BOOTINFO_HEADER_NUM,
SEL4_FORCE_LONG_ENUM(seL4_BootInfoID)
} seL4_BootInfoID;
/* Common header for all additional bootinfo chunks to describe the chunk. */
typedef struct seL4_BootInfoHeader {
seL4_Word id; /* identifier of the following blob */
seL4_Word len; /* length of the chunk, including this header */
} seL4_BootInfoHeader;
SEL4_COMPILE_ASSERT(
invalid_seL4_BootInfoHeader,
sizeof(seL4_BootInfoHeader) == 2 * sizeof(seL4_Word));

View File

@ -0,0 +1,11 @@
/*
* Copyright 2014, General Dynamics C4 Systems
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
/* Compile-time configuration parameters. Might be set by the build system. */
#include <autoconf.h>

View File

@ -0,0 +1,113 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <sel4/macros.h>
#ifndef __ASSEMBLER__
#ifdef CONFIG_HARDWARE_DEBUG_API
/* API arg values for breakpoint API, "type" arguments. */
typedef enum {
seL4_DataBreakpoint = 0,
seL4_InstructionBreakpoint,
seL4_SingleStep,
seL4_SoftwareBreakRequest,
SEL4_FORCE_LONG_ENUM(seL4_BreakpointType)
} seL4_BreakpointType;
/* API arg values for breakpoint API, "access" arguments. */
typedef enum {
seL4_BreakOnRead = 0,
seL4_BreakOnWrite,
seL4_BreakOnReadWrite,
seL4_MaxBreakpointAccess,
SEL4_FORCE_LONG_ENUM(seL4_BreakpointAccess)
} seL4_BreakpointAccess;
/* Format of a debug-exception message. */
typedef enum {
seL4_DebugException_FaultIP,
seL4_DebugException_ExceptionReason,
seL4_DebugException_TriggerAddress,
seL4_DebugException_BreakpointNumber,
seL4_DebugException_Length,
SEL4_FORCE_LONG_ENUM(seL4_DebugException_Msg)
} seL4_DebugException_Msg;
#endif
enum priorityConstants {
seL4_InvalidPrio = -1,
seL4_MinPrio = 0,
seL4_MaxPrio = CONFIG_NUM_PRIORITIES - 1
};
/* seL4_MessageInfo_t defined in api/shared_types.bf */
enum seL4_MsgLimits {
seL4_MsgLengthBits = 7,
seL4_MsgExtraCapBits = 2,
seL4_MsgMaxLength = 120
};
#define seL4_MsgMaxExtraCaps (LIBSEL4_BIT(seL4_MsgExtraCapBits)-1)
/* seL4_CapRights_t defined in shared_types_*.bf */
#define seL4_CapRightsBits 4
typedef enum {
seL4_NoFailure = 0,
seL4_InvalidRoot,
seL4_MissingCapability,
seL4_DepthMismatch,
seL4_GuardMismatch,
SEL4_FORCE_LONG_ENUM(seL4_LookupFailureType),
} seL4_LookupFailureType;
#endif /* !__ASSEMBLER__ */
#ifdef CONFIG_KERNEL_MCS
/* Minimum size of a scheduling context (2^{n} bytes) */
#define seL4_MinSchedContextBits 7
#ifndef __ASSEMBLER__
/* The size of a scheduling context, including the minimum 2 refills, excluding
any extra refills (= 10 words, 2 tick_t, 2 refills (= 2 tick_t each)) */
#define seL4_CoreSchedContextBytes (10 * sizeof(seL4_Word) + (6 * 8))
/* the size of a single extra refill */
#define seL4_RefillSizeBytes (2 * 8)
SEL4_COMPILE_ASSERT(MinSchedContextBits_min_1, seL4_MinSchedContextBits > 1)
SEL4_COMPILE_ASSERT(MinSchedContextBits_sufficient,
seL4_CoreSchedContextBytes <= LIBSEL4_BIT(seL4_MinSchedContextBits))
SEL4_COMPILE_ASSERT(MinSchedContextBits_necessary,
seL4_CoreSchedContextBytes > LIBSEL4_BIT(seL4_MinSchedContextBits - 1))
/*
* @brief Calculate the max extra refills a scheduling context can contain for a specific size.
*
* @param size of the schedulding context. Must be >= seL4_MinSchedContextBits
* @return the max number of extra refills that can be passed to seL4_SchedControl_Configure for
* this scheduling context
*/
static inline seL4_Word seL4_MaxExtraRefills(seL4_Word size)
{
return (LIBSEL4_BIT(size) - seL4_CoreSchedContextBytes) / seL4_RefillSizeBytes;
}
/* Flags to be used with seL4_SchedControl_ConfigureFlags */
typedef enum {
seL4_SchedContext_NoFlag = 0x0,
seL4_SchedContext_Sporadic = 0x1,
SEL4_FORCE_LONG_ENUM(seL4_SchedContextFlag),
} seL4_SchedContextFlag;
#endif /* !__ASSEMBLER__ */
#endif /* CONFIG_KERNEL_MCS */
#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC
#define DEBUG_MESSAGE_START 6
#define DEBUG_MESSAGE_MAXLEN 50
#endif

View File

@ -0,0 +1,30 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
/**
* Declares macros and methods which are conditional based
* on NDEBUG. If NDEBUG is defined then seL4_DebugAssert
* is a NOP, otherwise it invokes the unconditional version
* in sel4/assert.h.
*/
#pragma once
#ifdef NDEBUG
/** NDEBUG is defined do nothing */
#define seL4_DebugAssert(expr) ((void)(0))
#else // NDEBUG is not defined
#include <sel4/assert.h>
/**
* NDEBUG is not defined invoke seL4_Assert(expr).
*/
#define seL4_DebugAssert(expr) seL4_Assert(expr)
#endif // NDEBUG

View File

@ -0,0 +1,130 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
/* This header collects deprecated items that are no longer part of sel4.h. */
#include <sel4/sel4.h>
#include <sel4/arch/deprecated.h>
#include <sel4/sel4_arch/deprecated.h>
#define SEL4_PFIPC_LABEL SEL4_DEPRECATE_MACRO(seL4_Fault_VMFault)
#define SEL4_PFIPC_LENGTH SEL4_DEPRECATE_MACRO(seL4_VMFault_Length)
#define SEL4_PFIPC_FAULT_IP SEL4_DEPRECATE_MACRO(seL4_VMFault_IP)
#define SEL4_PFIPC_FAULT_ADDR SEL4_DEPRECATE_MACRO(seL4_VMFault_Addr)
#define SEL4_PFIPC_PREFETCH_FAULT SEL4_DEPRECATE_MACRO(seL4_VMFault_PrefetchFault)
#define SEL4_PFIPC_FSR SEL4_DEPRECATE_MACRO(seL4_VMFault_FSR)
#define SEL4_EXCEPT_IPC_LABEL SEL4_DEPRECATE_MACRO(seL4_Fault_UnknownSyscall)
#define SEL4_USER_EXCEPTION_LABEL SEL4_DEPRECATE_MACRO(seL4_Fault_UserException)
#define SEL4_USER_EXCEPTION_LENGTH SEL4_DEPRECATE_MACRO(seL4_UserException_Length)
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
#define SEL4_VGIC_MAINTENANCE_LENGTH SEL4_DEPRECATE_MACRO(seL4_VGICMaintenance_Length)
#define SEL4_VGIC_MAINTENANCE_LABEL SEL4_DEPRECATE_MACRO(seL4_Fault_VGICMaintenance)
#define SEL4_VCPU_FAULT_LENGTH SEL4_DEPRECATE_MACRO(seL4_VCPUFault_Length)
#define SEL4_VCPU_FAULT_LABEL SEL4_DEPRECATE_MACRO(seL4_Fault_VCPUFault)
#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
typedef seL4_CapRights_t seL4_CapRights SEL4_DEPRECATED("use seL4_CapRights_t");
typedef union {
struct {
seL4_Word fault_ip;
seL4_Word fault_addr;
seL4_Word prefetch_fault;
seL4_Word fsr;
} regs;
seL4_Word raw[4];
} seL4_PageFaultIpcRegisters SEL4_DEPRECATED("use seL4_Fault_VMFault_new()");
typedef seL4_Fault_tag_t seL4_FaultType SEL4_DEPRECATED("use seL4_Fault_tag_t");
#define seL4_NoFault SEL4_DEPRECATE_MACRO(seL4_Fault_NullFault)
#define seL4_CapFault SEL4_DEPRECATE_MACRO(seL4_Fault_CapFault)
#define seL4_UnknownSyscall SEL4_DEPRECATE_MACRO(seL4_Fault_UnknownSyscall)
#define seL4_UserException SEL4_DEPRECATE_MACRO(seL4_Fault_UserException)
#define seL4_VMFault SEL4_DEPRECATE_MACRO(seL4_Fault_VMFault)
static inline SEL4_DEPRECATED("removed") seL4_MessageInfo_t
seL4_GetTag(void)
{
return seL4_GetIPCBuffer()->tag;
}
static inline SEL4_DEPRECATED("removed") void
seL4_SetTag(seL4_MessageInfo_t tag)
{
seL4_GetIPCBuffer()->tag = tag;
}
static inline SEL4_DEPRECATED("use seL4_GetMR(seL4_VMFault_IP)") seL4_Word
seL4_PF_FIP(void)
{
return seL4_GetMR(seL4_VMFault_IP);
}
static inline SEL4_DEPRECATED("use seL4_GetMR(seL4_VMFault_Addr)") seL4_Word
seL4_PF_Addr(void)
{
return seL4_GetMR(seL4_VMFault_Addr);
}
static inline SEL4_DEPRECATED("use seL4_isVMFault_tag") seL4_Word
seL4_isPageFault_MSG(void)
{
return seL4_isVMFault_tag(seL4_GetIPCBuffer()->tag);
}
static inline SEL4_DEPRECATED("use seL4_isVMFault_tag") seL4_Word
seL4_isPageFault_Tag(seL4_MessageInfo_t tag)
{
return seL4_isVMFault_tag(tag);
}
static inline SEL4_DEPRECATED("use seL4_isUnknownSyscall_tag") seL4_Word
seL4_isExceptIPC_Tag(seL4_MessageInfo_t tag)
{
return seL4_isUnknownSyscall_tag(tag);
}
static inline SEL4_DEPRECATED("use seL4_GetMR") seL4_Word
seL4_ExceptIPC_Get(seL4_Word mr)
{
return seL4_GetMR(mr);
}
static inline SEL4_DEPRECATED("use seL4_SetMR") void
seL4_ExceptIPC_Set(seL4_Word index, seL4_Word val)
{
seL4_SetMR(index, val);
}
static inline SEL4_DEPRECATED("") seL4_Word
seL4_IsArchSyscallFrom(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_length(tag) == seL4_UnknownSyscall_Length;
}
static inline SEL4_DEPRECATED("") seL4_Word
seL4_IsArchExceptionFrom(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_length(tag) == seL4_UnknownSyscall_Length;
}
typedef seL4_Word seL4_CapData_t SEL4_DEPRECATED("Badge and guard data are just seL4_Word type");
static inline SEL4_DEPRECATED("Badges do not need to be constructed") seL4_Word seL4_CapData_Badge_new(seL4_Word badge)
{
return badge;
}
static inline SEL4_DEPRECATED("Use seL4_CNode_CapData_new().words[0]") seL4_Word seL4_CapData_Guard_new(seL4_Word guard,
seL4_Word bits)
{
return seL4_CNode_CapData_new(guard, bits).words[0];
}

View File

@ -0,0 +1,27 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
typedef enum {
seL4_NoError = 0,
seL4_InvalidArgument,
seL4_InvalidCapability,
seL4_IllegalOperation,
seL4_RangeError,
seL4_AlignmentError,
seL4_FailedLookup,
seL4_TruncatedMessage,
seL4_DeleteFirst,
seL4_RevokeFirst,
seL4_NotEnoughMemory,
/* This should always be the last item in the list
* so it gives a count of the number of errors in the
* enum.
*/
seL4_NumErrors
} seL4_Error;

View File

@ -0,0 +1,84 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <sel4/types.h>
#include <sel4/sel4_arch/faults.h>
LIBSEL4_INLINE_FUNC seL4_Fault_t seL4_getFault(seL4_MessageInfo_t tag)
{
switch (seL4_MessageInfo_get_label(tag)) {
case seL4_Fault_CapFault:
return seL4_Fault_CapFault_new(seL4_GetMR(seL4_CapFault_IP),
seL4_GetMR(seL4_CapFault_Addr),
seL4_GetMR(seL4_CapFault_InRecvPhase),
seL4_GetMR(seL4_CapFault_LookupFailureType),
seL4_GetMR(seL4_CapFault_BitsLeft),
seL4_GetMR(seL4_CapFault_GuardMismatch_GuardFound),
seL4_GetMR(seL4_CapFault_GuardMismatch_BitsFound));
#ifdef CONFIG_HARDWARE_DEBUG_API
case seL4_Fault_DebugException:
return seL4_Fault_DebugException_new(seL4_GetMR(seL4_DebugException_FaultIP),
seL4_GetMR(seL4_DebugException_ExceptionReason),
seL4_GetMR(seL4_DebugException_TriggerAddress),
seL4_GetMR(seL4_DebugException_BreakpointNumber));
#endif
default:
return seL4_getArchFault(tag);
}
}
#ifdef CONFIG_HARDWARE_DEBUG_API
LIBSEL4_INLINE_FUNC seL4_Bool seL4_isDebugException_tag(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_label(tag) == seL4_Fault_DebugException;
}
#endif
LIBSEL4_INLINE_FUNC seL4_Bool seL4_isVMFault_tag(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_label(tag) == seL4_Fault_VMFault;
}
LIBSEL4_INLINE_FUNC seL4_Bool seL4_isUnknownSyscall_tag(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_label(tag) == seL4_Fault_UnknownSyscall;
}
LIBSEL4_INLINE_FUNC seL4_Bool seL4_isUserException_tag(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_label(tag) == seL4_Fault_UserException;
}
LIBSEL4_INLINE_FUNC seL4_Bool seL4_isNullFault_tag(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_label(tag) == seL4_Fault_NullFault;
}
LIBSEL4_INLINE_FUNC seL4_Bool seL4_isCapFault_tag(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_label(tag) == seL4_Fault_CapFault;
}
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE_FUNC seL4_Bool seL4_isTimeoutFault_tag(seL4_MessageInfo_t tag)
{
return seL4_MessageInfo_get_label(tag) == seL4_Fault_Timeout;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_TimeoutReply_new(seL4_Bool resume, seL4_UserContext regs, seL4_Word length)
{
seL4_MessageInfo_t info = seL4_MessageInfo_new(!resume, 0, 0, length);
for (seL4_Word i = 0; i < length; i++) {
seL4_SetMR(i, ((seL4_Word *) &regs)[i]);
}
return info;
}
#endif /* CONFIG_KERNEL_MCS */

View File

@ -0,0 +1,105 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
* Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/types.h>
#include <sel4/syscalls.h>
extern __thread seL4_IPCBuffer *__sel4_ipc_buffer;
#ifdef CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC
extern __thread char __sel4_print_error;
LIBSEL4_INLINE_FUNC char *seL4_GetDebugError(void)
{
return (char *)(__sel4_ipc_buffer->msg + DEBUG_MESSAGE_START);
}
LIBSEL4_INLINE_FUNC void seL4_SetPrintError(char print_error)
{
__sel4_print_error = print_error;
return;
}
LIBSEL4_INLINE_FUNC char seL4_CanPrintError(void)
{
return __sel4_print_error;
}
#endif
LIBSEL4_INLINE_FUNC void seL4_SetIPCBuffer(seL4_IPCBuffer *ipc_buffer)
{
__sel4_ipc_buffer = ipc_buffer;
return;
}
LIBSEL4_INLINE_FUNC seL4_IPCBuffer *seL4_GetIPCBuffer(void)
{
return __sel4_ipc_buffer;
}
LIBSEL4_INLINE_FUNC seL4_Word seL4_GetMR(int i)
{
return seL4_GetIPCBuffer()->msg[i];
}
LIBSEL4_INLINE_FUNC void seL4_SetMR(int i, seL4_Word mr)
{
seL4_GetIPCBuffer()->msg[i] = mr;
}
LIBSEL4_INLINE_FUNC seL4_Word seL4_GetUserData(void)
{
return seL4_GetIPCBuffer()->userData;
}
LIBSEL4_INLINE_FUNC void seL4_SetUserData(seL4_Word data)
{
seL4_GetIPCBuffer()->userData = data;
}
LIBSEL4_INLINE_FUNC seL4_Word seL4_GetBadge(int i)
{
return seL4_GetIPCBuffer()->caps_or_badges[i];
}
LIBSEL4_INLINE_FUNC seL4_CPtr seL4_GetCap(int i)
{
return (seL4_CPtr)seL4_GetIPCBuffer()->caps_or_badges[i];
}
LIBSEL4_INLINE_FUNC void seL4_SetCap(int i, seL4_CPtr cptr)
{
seL4_GetIPCBuffer()->caps_or_badges[i] = (seL4_Word)cptr;
}
LIBSEL4_INLINE_FUNC void seL4_GetCapReceivePath(seL4_CPtr *receiveCNode, seL4_CPtr *receiveIndex,
seL4_Word *receiveDepth)
{
seL4_IPCBuffer *ipcbuffer = seL4_GetIPCBuffer();
if (receiveCNode != (void *)0) {
*receiveCNode = ipcbuffer->receiveCNode;
}
if (receiveIndex != (void *)0) {
*receiveIndex = ipcbuffer->receiveIndex;
}
if (receiveDepth != (void *)0) {
*receiveDepth = ipcbuffer->receiveDepth;
}
}
LIBSEL4_INLINE_FUNC void seL4_SetCapReceivePath(seL4_CPtr receiveCNode, seL4_CPtr receiveIndex, seL4_Word receiveDepth)
{
seL4_IPCBuffer *ipcbuffer = seL4_GetIPCBuffer();
ipcbuffer->receiveCNode = receiveCNode;
ipcbuffer->receiveIndex = receiveIndex;
ipcbuffer->receiveDepth = receiveDepth;
}

View File

@ -0,0 +1,8 @@
#pragma once
#define CONFIG_LIB_SEL4_INLINE_INVOCATIONS 1
/* disabled: CONFIG_LIB_SEL4_DEFAULT_FUNCTION_ATTRIBUTES */
/* disabled: CONFIG_LIB_SEL4_PUBLIC_SYMBOLS */
#define CONFIG_LIB_SEL4_FUNCTION_ATTRIBUTE inline
/* disabled: CONFIG_LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY */
#define CONFIG_LIB_SEL4_PRINT_INVOCATION_ERRORS 0

View File

@ -0,0 +1,8 @@
{
"LIB_SEL4_INLINE_INVOCATIONS": true,
"LIB_SEL4_DEFAULT_FUNCTION_ATTRIBUTES": false,
"LIB_SEL4_PUBLIC_SYMBOLS": false,
"LIB_SEL4_FUNCTION_ATTRIBUTE": "inline",
"LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY": false,
"LIB_SEL4_PRINT_INVOCATION_ERRORS": "0"
}

View File

@ -0,0 +1,101 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
** SPDX-License-Identifier: BSD-2-Clause
*/
/* This header was generated by kernel/tools/invocation_header_gen.py.
*
* To add an invocation call number, edit libsel4/include/interfaces/sel4.xml.
*
*/
#pragma once
enum invocation_label {
InvalidInvocation,
UntypedRetype,
TCBReadRegisters,
TCBWriteRegisters,
TCBCopyRegisters,
#if !defined(CONFIG_KERNEL_MCS)
TCBConfigure,
#endif
#if defined(CONFIG_KERNEL_MCS)
TCBConfigure,
#endif
TCBSetPriority,
TCBSetMCPriority,
#if !defined(CONFIG_KERNEL_MCS)
TCBSetSchedParams,
#endif
#if defined(CONFIG_KERNEL_MCS)
TCBSetSchedParams,
#endif
#if defined(CONFIG_KERNEL_MCS)
TCBSetTimeoutEndpoint,
#endif
TCBSetIPCBuffer,
#if !defined(CONFIG_KERNEL_MCS)
TCBSetSpace,
#endif
#if defined(CONFIG_KERNEL_MCS)
TCBSetSpace,
#endif
TCBSuspend,
TCBResume,
TCBBindNotification,
TCBUnbindNotification,
#if (!defined(CONFIG_KERNEL_MCS) && defined(CONFIG_ENABLE_SMP_SUPPORT))
TCBSetAffinity,
#endif
#if defined(CONFIG_HARDWARE_DEBUG_API)
TCBSetBreakpoint,
#endif
#if defined(CONFIG_HARDWARE_DEBUG_API)
TCBGetBreakpoint,
#endif
#if defined(CONFIG_HARDWARE_DEBUG_API)
TCBUnsetBreakpoint,
#endif
#if defined(CONFIG_HARDWARE_DEBUG_API)
TCBConfigureSingleStepping,
#endif
TCBSetTLSBase,
CNodeRevoke,
CNodeDelete,
CNodeCancelBadgedSends,
CNodeCopy,
CNodeMint,
CNodeMove,
CNodeMutate,
CNodeRotate,
#if !defined(CONFIG_KERNEL_MCS)
CNodeSaveCaller,
#endif
IRQIssueIRQHandler,
IRQAckIRQ,
IRQSetIRQHandler,
IRQClearIRQHandler,
DomainSetSet,
#if defined(CONFIG_KERNEL_MCS)
SchedControlConfigureFlags,
#endif
#if defined(CONFIG_KERNEL_MCS)
SchedContextBind,
#endif
#if defined(CONFIG_KERNEL_MCS)
SchedContextUnbind,
#endif
#if defined(CONFIG_KERNEL_MCS)
SchedContextUnbindObject,
#endif
#if defined(CONFIG_KERNEL_MCS)
SchedContextConsumed,
#endif
#if defined(CONFIG_KERNEL_MCS)
SchedContextYieldTo,
#endif
nInvocationLabels
};
#include <sel4/sel4_arch/invocation.h>
#include <sel4/arch/invocation.h>

View File

@ -0,0 +1,67 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#ifndef CONST
#define CONST __attribute__((__const__))
#endif
#ifndef PURE
#define PURE __attribute__((__pure__))
#endif
#define SEL4_PACKED __attribute__((packed))
#define SEL4_DEPRECATED(x) __attribute__((deprecated(x)))
#define SEL4_DEPRECATE_MACRO(x) _Pragma("deprecated") x
#define LIBSEL4_UNUSED __attribute__((unused))
#define LIBSEL4_WEAK __attribute__((weak))
#define LIBSEL4_NOINLINE __attribute__((noinline))
#ifdef CONFIG_LIB_SEL4_INLINE_INVOCATIONS
#define LIBSEL4_INLINE static inline
#define LIBSEL4_INLINE_FUNC static inline
#elif defined(CONFIG_LIB_SEL4_PUBLIC_SYMBOLS)
#define LIBSEL4_INLINE LIBSEL4_UNUSED LIBSEL4_WEAK
#define LIBSEL4_INLINE_FUNC LIBSEL4_UNUSED LIBSEL4_WEAK
#else
#define LIBSEL4_INLINE LIBSEL4_NOINLINE LIBSEL4_UNUSED LIBSEL4_WEAK
#define LIBSEL4_INLINE_FUNC static inline
#endif
/* _Static_assert() is a c11 feature. Since the kernel is currently compiled
* with c99, we have to emulate it. */
#if defined(__STDC_VERSION__) && (__STDC_VERSION__ >= 201112L)
#define SEL4_COMPILE_ASSERT(name, expr) _Static_assert(expr, #name);
#else
#define SEL4_COMPILE_ASSERT(name, expr) \
typedef int __assert_failed_##name[(expr) ? 1 : -1] LIBSEL4_UNUSED;
#endif
#define SEL4_SIZE_SANITY(index, entry, size) \
SEL4_COMPILE_ASSERT(index##_##entry##_##size, (index) + (entry) == size)
/*
* Some compilers attempt to pack enums into the smallest possible type.
* For ABI compatibility with the kernel, we need to ensure they remain
* the same size as a 'long'.
*/
#define SEL4_FORCE_LONG_ENUM(type) \
_enum_pad_ ## type = ((1ULL << ((sizeof(long)*8) - 1)) - 1)
#define LIBSEL4_BIT(n) (1ul<<(n))

View File

@ -0,0 +1,11 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#define seL4_GuardSizeBits 6
#define seL4_GuardBits 58
#define seL4_BadgeBits 64

View File

@ -0,0 +1,25 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
typedef enum api_object {
seL4_UntypedObject,
seL4_TCBObject,
seL4_EndpointObject,
seL4_NotificationObject,
seL4_CapTableObject,
#ifdef CONFIG_KERNEL_MCS
seL4_SchedContextObject,
seL4_ReplyObject,
#endif
seL4_NonArchObjectTypeCount,
} seL4_ObjectType;
__attribute__((deprecated("use seL4_NotificationObject"))) static const seL4_ObjectType seL4_AsyncEndpointObject =
seL4_NotificationObject;
typedef seL4_Word api_object_t;

View File

@ -0,0 +1,17 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <sel4/arch/constants_cortex_a53.h>
#if CONFIG_WORD_SIZE == 32
/* First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0xe0000000
#else
/* otherwise this is defined at the arch level */
#endif

View File

@ -0,0 +1,30 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <sel4/types.h>
#include <sel4/macros.h>
#include <sel4/syscalls.h>
#include <sel4/arch/syscalls.h>
#include <sel4/sel4_arch/syscalls.h>
#include <sel4/invocation.h>
#include <interfaces/sel4_client.h>
#include <sel4/virtual_client.h>
#include <sel4/bootinfo.h>
#include <sel4/faults.h>
#include <sel4/deprecated.h>
#include <sel4/constants.h>
#include <sel4/sel4_arch/constants.h>
#include <sel4/arch/constants.h>
#include <sel4/plat/api/constants.h>

View File

@ -0,0 +1,253 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <sel4/macros.h>
#ifndef __ASSEMBLER__
/* format of an unknown syscall message */
typedef enum {
seL4_UnknownSyscall_X0,
seL4_UnknownSyscall_X1,
seL4_UnknownSyscall_X2,
seL4_UnknownSyscall_X3,
seL4_UnknownSyscall_X4,
seL4_UnknownSyscall_X5,
seL4_UnknownSyscall_X6,
seL4_UnknownSyscall_X7,
seL4_UnknownSyscall_FaultIP,
seL4_UnknownSyscall_SP,
seL4_UnknownSyscall_LR,
seL4_UnknownSyscall_SPSR,
seL4_UnknownSyscall_Syscall,
/* length of an unknown syscall message */
seL4_UnknownSyscall_Length,
SEL4_FORCE_LONG_ENUM(seL4_UnknownSyscall_Msg),
} seL4_UnknownSyscall_Msg;
/* format of a user exception message */
typedef enum {
seL4_UserException_FaultIP,
seL4_UserException_SP,
seL4_UserException_SPSR,
seL4_UserException_Number,
seL4_UserException_Code,
/* length of a user exception */
seL4_UserException_Length,
SEL4_FORCE_LONG_ENUM(seL4_UserException_Msg),
} seL4_UserException_Msg;
/* format of a vm fault message */
typedef enum {
seL4_VMFault_IP,
seL4_VMFault_Addr,
seL4_VMFault_PrefetchFault,
seL4_VMFault_FSR,
seL4_VMFault_Length,
SEL4_FORCE_LONG_ENUM(seL4_VMFault_Msg),
} seL4_VMFault_Msg;
typedef enum {
seL4_VGICMaintenance_IDX,
seL4_VGICMaintenance_Length,
SEL4_FORCE_LONG_ENUM(seL4_VGICMaintenance_Msg),
} seL4_VGICMaintenance_Msg;
typedef enum {
seL4_VPPIEvent_IRQ,
seL4_VPPIEvent_Length,
SEL4_FORCE_LONG_ENUM(seL4_VPPIEvent_Msg),
} seL4_VPPIEvent_Msg;
typedef enum {
seL4_VCPUFault_HSR,
seL4_VCPUFault_Length,
SEL4_FORCE_LONG_ENUM(seL4_VCPUFault_Msg),
} seL4_VCPUFault_Msg;
typedef enum {
/* VM control registers EL1 */
seL4_VCPUReg_SCTLR = 0,
seL4_VCPUReg_TTBR0,
seL4_VCPUReg_TTBR1,
seL4_VCPUReg_TCR,
seL4_VCPUReg_MAIR,
seL4_VCPUReg_AMAIR,
seL4_VCPUReg_CIDR,
/* other system registers EL1 */
seL4_VCPUReg_ACTLR,
seL4_VCPUReg_CPACR,
/* exception handling registers EL1 */
seL4_VCPUReg_AFSR0,
seL4_VCPUReg_AFSR1,
seL4_VCPUReg_ESR,
seL4_VCPUReg_FAR,
seL4_VCPUReg_ISR,
seL4_VCPUReg_VBAR,
/* thread pointer/ID registers EL0/EL1 */
seL4_VCPUReg_TPIDR_EL1,
/* Virtualisation Multiprocessor ID Register */
seL4_VCPUReg_VMPIDR_EL2,
/* general registers x0 to x30 have been saved by traps.S */
seL4_VCPUReg_SP_EL1,
seL4_VCPUReg_ELR_EL1,
seL4_VCPUReg_SPSR_EL1, // 32-bit
/* generic timer registers, to be completed */
seL4_VCPUReg_CNTV_CTL,
seL4_VCPUReg_CNTV_CVAL,
seL4_VCPUReg_CNTVOFF,
seL4_VCPUReg_CNTKCTL_EL1,
seL4_VCPUReg_Num,
SEL4_FORCE_LONG_ENUM(seL4_VCPUReg),
} seL4_VCPUReg;
#ifdef CONFIG_KERNEL_MCS
typedef enum {
seL4_TimeoutReply_FaultIP,
seL4_TimeoutReply_SP,
seL4_TimeoutReply_SPSR_EL1,
seL4_TimeoutReply_X0,
seL4_TimeoutReply_X1,
seL4_TimeoutReply_X2,
seL4_TimeoutReply_X3,
seL4_TimeoutReply_X4,
seL4_TimeoutReply_X5,
seL4_TimeoutReply_X6,
seL4_TimeoutReply_X7,
seL4_TimeoutReply_X8,
seL4_TimeoutReply_X16,
seL4_TimeoutReply_X17,
seL4_TimeoutReply_X18,
seL4_TimeoutReply_X29,
seL4_TimeoutReply_X30,
seL4_TimeoutReply_X9,
seL4_TimeoutReply_X10,
seL4_TimeoutReply_X11,
seL4_TimeoutReply_X12,
seL4_TimeoutReply_X13,
seL4_TimeoutReply_X14,
seL4_TimeoutReply_X15,
seL4_TimeoutReply_X19,
seL4_TimeoutReply_X20,
seL4_TimeoutReply_X21,
seL4_TimeoutReply_X22,
seL4_TimeoutReply_X23,
seL4_TimeoutReply_X24,
seL4_TimeoutReply_X25,
seL4_TimeoutReply_X26,
seL4_TimeoutReply_X27,
seL4_TimeoutReply_X28,
seL4_TimeoutReply_Length,
SEL4_FORCE_LONG_ENUM(seL4_TimeoutReply_Msg)
} seL4_TimeoutReply_Msg;
typedef enum {
seL4_Timeout_Data,
seL4_Timeout_Consumed,
seL4_Timeout_Length,
SEL4_FORCE_LONG_ENUM(seL4_Timeout_Msg)
} seL4_Timeout_Msg;
#endif
#endif /* !__ASSEMBLER__ */
#define seL4_DataFault 0
#define seL4_InstructionFault 1
/* object sizes - 2^n */
#define seL4_PageBits 12
#define seL4_LargePageBits 21
#define seL4_HugePageBits 30
#define seL4_SlotBits 5
#define seL4_TCBBits 11
#define seL4_EndpointBits 4
#ifdef CONFIG_KERNEL_MCS
#define seL4_NotificationBits 6
#define seL4_ReplyBits 5
#else
#define seL4_NotificationBits 5
#endif
#define seL4_PageTableBits 12
#define seL4_PageTableEntryBits 3
#define seL4_PageTableIndexBits 9
#define seL4_NumASIDPoolsBits 7
#define seL4_ASIDPoolBits 12
#define seL4_ASIDPoolIndexBits 9
#define seL4_IOPageTableBits 12
#define seL4_WordSizeBits 3
#define seL4_VSpaceEntryBits 3
#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined (CONFIG_ARM_PA_SIZE_BITS_40)
/* for a 3 level translation, we skip the PGD */
#define seL4_VSpaceBits 13
#define seL4_VSpaceIndexBits 10
#else
#define seL4_VSpaceBits 12
#define seL4_VSpaceIndexBits 9
#endif
#define seL4_ARM_VCPUBits 12
#define seL4_VCPUBits 12
/* word size */
#define seL4_WordBits (sizeof(seL4_Word) * 8)
/* Untyped size limits */
#define seL4_MinUntypedBits 4
#define seL4_MaxUntypedBits 47
#ifndef __ASSEMBLER__
SEL4_SIZE_SANITY(seL4_PageTableEntryBits, seL4_PageTableIndexBits, seL4_PageTableBits);
SEL4_SIZE_SANITY(seL4_WordSizeBits, seL4_ASIDPoolIndexBits, seL4_ASIDPoolBits);
SEL4_SIZE_SANITY(seL4_VSpaceEntryBits, seL4_VSpaceIndexBits, seL4_VSpaceBits);
#endif
#ifdef CONFIG_ENABLE_BENCHMARKS
/* size of kernel log buffer in bytes */
#define seL4_LogBufferSize (LIBSEL4_BIT(20))
#endif /* CONFIG_ENABLE_BENCHMARKS */
#define seL4_FastMessageRegisters 4
/* IPC buffer is 1024 bytes, giving size bits of 10 */
#define seL4_IPCBufferSizeBits 10
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
/* The userspace occupies the range 0x0 to 0xfffffffffff.
* The stage-1 translation is disabled, and the stage-2
* translation input addree size is constrained by the
* ID_AA64MMFR0_EL1.PARange which is 44 bits on TX1.
* Anything address above the range above triggers an
* address size fault.
*/
/* First address in the virtual address space that is not accessible to user level */
#if defined(CONFIG_ARM_PA_SIZE_BITS_44)
#define seL4_UserTop 0x00000fffffffffff
#elif defined(CONFIG_ARM_PA_SIZE_BITS_40)
#define seL4_UserTop 0x000000ffffffffff
#else
#error "Unknown physical address width"
#endif
#else
/* First address in the virtual address space that is not accessible to user level */
#define seL4_UserTop 0x00007fffffffffff
#endif

View File

@ -0,0 +1,45 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#define seL4_ARM_PageDirectory seL4_ARM_PageTable;
#define seL4_ARM_PageDirectory_Map seL4_ARM_PageTable_Map
#define seL4_ARM_PageDirectory_Unmap seL4_ARM_PageTable_Unmap
#define ARMPageDirectoryMap ARMPageTableMap
#define ARMPageDirectoryUnmap ARMPageTableUnmap
#define seL4_PageDirBits seL4_PageTableBits
#define seL4_PageDirEntryBits seL4_PageTableEntryBits
#define seL4_PageDirIndexBits seL4_PageTableIndexBits
#define seL4_ARM_PageDirectoryObject seL4_ARM_PageTableObject
#define seL4_PUDEntryBits 3
#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT) && defined (CONFIG_ARM_PA_SIZE_BITS_40)
#define seL4_PGDBits 0
#define seL4_PGDEntryBits 0
#define seL4_PGDIndexBits 0
#define seL4_PUDBits 13
#define seL4_PUDIndexBits 10
#define seL4_ARM_PageUpperDirectoryObject seL4_ARM_VSpaceObject
#else
#define seL4_PGDBits 12
#define seL4_PGDEntryBits 3
#define seL4_PGDIndexBits 9
#define seL4_PUDBits 12
#define seL4_PUDIndexBits 9
#define seL4_ARM_PageGlobalDirectoryObject seL4_ARM_VSpaceObject
#define seL4_ARM_PageUpperDirectoryObject seL4_ARM_PageTableObject
#define seL4_ARM_PageUpperDirectory seL4_ARM_PageTable;
#define seL4_ARM_PageUpperDirectory_Map seL4_ARM_PageTable_Map
#define seL4_ARM_PageUpperDirectory_Unmap seL4_ARM_PageTable_Unmap
#endif

View File

@ -0,0 +1,58 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <sel4/faults.h>
#include <sel4/sel4_arch/constants.h>
LIBSEL4_INLINE_FUNC seL4_Fault_t seL4_getArchFault(seL4_MessageInfo_t tag)
{
switch (seL4_MessageInfo_get_label(tag)) {
case seL4_Fault_UnknownSyscall:
return seL4_Fault_UnknownSyscall_new(seL4_GetMR(seL4_UnknownSyscall_X0),
seL4_GetMR(seL4_UnknownSyscall_X1),
seL4_GetMR(seL4_UnknownSyscall_X2),
seL4_GetMR(seL4_UnknownSyscall_X3),
seL4_GetMR(seL4_UnknownSyscall_X4),
seL4_GetMR(seL4_UnknownSyscall_X5),
seL4_GetMR(seL4_UnknownSyscall_X6),
seL4_GetMR(seL4_UnknownSyscall_X7),
seL4_GetMR(seL4_UnknownSyscall_FaultIP),
seL4_GetMR(seL4_UnknownSyscall_SP),
seL4_GetMR(seL4_UnknownSyscall_LR),
seL4_GetMR(seL4_UnknownSyscall_SPSR),
seL4_GetMR(seL4_UnknownSyscall_Syscall));
case seL4_Fault_UserException:
return seL4_Fault_UserException_new(seL4_GetMR(seL4_UserException_FaultIP),
seL4_GetMR(seL4_UserException_SP),
seL4_GetMR(seL4_UserException_SPSR),
seL4_GetMR(seL4_UserException_Number),
seL4_GetMR(seL4_UserException_Code));
case seL4_Fault_VMFault:
return seL4_Fault_VMFault_new(seL4_GetMR(seL4_VMFault_IP),
seL4_GetMR(seL4_VMFault_Addr),
seL4_GetMR(seL4_VMFault_PrefetchFault),
seL4_GetMR(seL4_VMFault_FSR));
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
case seL4_Fault_VGICMaintenance:
return seL4_Fault_VGICMaintenance_new(seL4_GetMR(seL4_VGICMaintenance_IDX));
case seL4_Fault_VCPUFault:
return seL4_Fault_VCPUFault_new(seL4_GetMR(seL4_VCPUFault_HSR));
case seL4_Fault_VPPIEvent:
return seL4_Fault_VPPIEvent_new(seL4_GetMR(seL4_VPPIEvent_IRQ));
#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
#ifdef CONFIG_KERNEL_MCS
case seL4_Fault_Timeout:
return seL4_Fault_Timeout_new(seL4_GetMR(seL4_Timeout_Data),
seL4_GetMR(seL4_Timeout_Consumed));
#endif /* CONFIG_KERNEL_MCS */
default:
return seL4_Fault_NullFault_new();
}
}

View File

@ -0,0 +1,21 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
** SPDX-License-Identifier: BSD-2-Clause
*/
/* This header was generated by kernel/tools/invocation_header_gen.py.
*
* To add an invocation call number, edit libsel4/include/interfaces/sel4.xml.
*
*/
#pragma once
enum sel4_arch_invocation_label {
ARMVSpaceClean_Data = nInvocationLabels,
ARMVSpaceInvalidate_Data,
ARMVSpaceCleanInvalidate_Data,
ARMVSpaceUnify_Instruction,
ARMSMCCall,
nSeL4ArchInvocationLabels
};

View File

@ -0,0 +1,17 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#define SEL4_MAPPING_LOOKUP_LEVEL 2
#define SEL4_MAPPING_LOOKUP_NO_PT 21
#define SEL4_MAPPING_LOOKUP_NO_PD 30
#define SEL4_MAPPING_LOOKUP_NO_PUD 39
LIBSEL4_INLINE_FUNC seL4_Word seL4_MappingFailedLookupLevel(void)
{
return seL4_GetMR(SEL4_MAPPING_LOOKUP_LEVEL);
}

View File

@ -0,0 +1,13 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
typedef enum _mode_object {
seL4_ARM_HugePageObject = seL4_NonArchObjectTypeCount,
seL4_ARM_VSpaceObject,
seL4_ModeObjectTypeCount
} seL4_ModeObjectType;

View File

@ -0,0 +1,10 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#define SEL4_WORD_IS_UINT64
#define SEL4_INT64_IS_LONG

View File

@ -0,0 +1,222 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <sel4/functions.h>
#include <sel4/types.h>
#ifdef CONFIG_KERNEL_MCS
#define MCS_PARAM_DECL(r) register seL4_Word reply_reg asm(r) = reply
#define MCS_PARAM , "r"(reply_reg)
#else
#define MCS_PARAM_DECL(r)
#define MCS_PARAM
#endif
/*
* To simplify the definition of the various seL4 syscalls/syscall-wrappers we define
* some helper assembly functions. These functions are designed to cover the different
* cases of sending/receiving data in registers to/from the kernel. The most 'complex'
* version is arm_sys_send_recv, and all other functions are limited versions that allow
* for registers to not be unnecessarily clobbered
*
* arm_sys_send: Fills all registers into the kernel, expects nothing to be sent back
* by the kernel. Used for direction one way sends that contain data (e.g. seL4_Send,
* seL4_NBSend)
*
* arm_sys_send_null: Only fills metadata registers into the kernel (skips message
* registers). Expects nothing to be sent back by the kernel. Used by directional
* one way sends that do not contain data (e.g. seL4_Notify)
*
* arm_sys_reply: Similar to arm_sys_send except it does not take a word for the
* destination register. Used for undirected one way sends that contain data
* (e.g. seL4_Reply)
*
* arm_sys_recv: Sends one register (destination) to the kernel and expects all
* registers to be returned by the kernel. Used for directed receives that return
* data (e.g. seL4_Recv)
*
* arm_sys_send_recv: Fills all registers into the kernel and expects all of them
* to be filled on return by the kernel. Used for directed send+receives
* where data flows both directions (e.g. seL4_Call, seL4_ReplyWait)
*
* arm_sys_nbsend_recv: Fills all registers into the kernel and expects all of them
* to be filled on return by the kernel. Used for directed send+receives
* where data flows both directions on separate caps (e.g. seL4_NBSendRecv)
*
* arm_sys_null: Does not send any registers to the kernel or expect anything to
* be returned from the kernel. Used to trigger implicit kernel actions without
* any data (e.g. seL4_Yield)
*/
static inline void arm_sys_send(seL4_Word sys, seL4_Word dest, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1,
seL4_Word mr2, seL4_Word mr3)
{
register seL4_Word destptr asm("x0") = dest;
register seL4_Word info asm("x1") = info_arg;
/* Load beginning of the message into registers. */
register seL4_Word msg0 asm("x2") = mr0;
register seL4_Word msg1 asm("x3") = mr1;
register seL4_Word msg2 asm("x4") = mr2;
register seL4_Word msg3 asm("x5") = mr3;
/* Perform the system call. */
register seL4_Word scno asm("x7") = sys;
asm volatile(
"svc #0"
: "+r"(destptr), "+r"(msg0), "+r"(msg1), "+r"(msg2),
"+r"(msg3), "+r"(info)
: "r"(scno)
);
}
#ifndef CONFIG_KERNEL_MCS
static inline void arm_sys_reply(seL4_Word sys, seL4_Word info_arg, seL4_Word mr0, seL4_Word mr1, seL4_Word mr2,
seL4_Word mr3)
{
register seL4_Word info asm("x1") = info_arg;
/* Load beginning of the message into registers. */
register seL4_Word msg0 asm("x2") = mr0;
register seL4_Word msg1 asm("x3") = mr1;
register seL4_Word msg2 asm("x4") = mr2;
register seL4_Word msg3 asm("x5") = mr3;
/* Perform the system call. */
register seL4_Word scno asm("x7") = sys;
asm volatile(
"svc #0"
: "+r"(msg0), "+r"(msg1), "+r"(msg2), "+r"(msg3),
"+r"(info)
: "r"(scno)
);
}
#endif
static inline void arm_sys_send_null(seL4_Word sys, seL4_Word src, seL4_Word info_arg)
{
register seL4_Word destptr asm("x0") = src;
register seL4_Word info asm("x1") = info_arg;
/* Perform the system call. */
register seL4_Word scno asm("x7") = sys;
asm volatile(
"svc #0"
: "+r"(destptr), "+r"(info)
: "r"(scno)
);
}
static inline void arm_sys_recv(seL4_Word sys, seL4_Word src, seL4_Word *out_badge, seL4_Word *out_info,
seL4_Word *out_mr0, seL4_Word *out_mr1, seL4_Word *out_mr2, seL4_Word *out_mr3, LIBSEL4_UNUSED seL4_Word reply)
{
register seL4_Word src_and_badge asm("x0") = src;
register seL4_Word info asm("x1");
/* Incoming message registers. */
register seL4_Word msg0 asm("x2");
register seL4_Word msg1 asm("x3");
register seL4_Word msg2 asm("x4");
register seL4_Word msg3 asm("x5");
MCS_PARAM_DECL("x6");
/* Perform the system call. */
register seL4_Word scno asm("x7") = sys;
asm volatile(
"svc #0"
: "=r"(msg0), "=r"(msg1), "=r"(msg2), "=r"(msg3),
"=r"(info), "+r"(src_and_badge)
: "r"(scno) MCS_PARAM
: "memory"
);
*out_badge = src_and_badge;
*out_info = info;
*out_mr0 = msg0;
*out_mr1 = msg1;
*out_mr2 = msg2;
*out_mr3 = msg3;
}
static inline void arm_sys_send_recv(seL4_Word sys, seL4_Word dest, seL4_Word *out_badge, seL4_Word info_arg,
seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2, seL4_Word *in_out_mr3,
LIBSEL4_UNUSED seL4_Word reply)
{
register seL4_Word destptr asm("x0") = dest;
register seL4_Word info asm("x1") = info_arg;
/* Load beginning of the message into registers. */
register seL4_Word msg0 asm("x2") = *in_out_mr0;
register seL4_Word msg1 asm("x3") = *in_out_mr1;
register seL4_Word msg2 asm("x4") = *in_out_mr2;
register seL4_Word msg3 asm("x5") = *in_out_mr3;
MCS_PARAM_DECL("x6");
/* Perform the system call. */
register seL4_Word scno asm("x7") = sys;
asm volatile(
"svc #0"
: "+r"(msg0), "+r"(msg1), "+r"(msg2), "+r"(msg3),
"+r"(info), "+r"(destptr)
: "r"(scno) MCS_PARAM
: "memory"
);
*out_info = info;
*out_badge = destptr;
*in_out_mr0 = msg0;
*in_out_mr1 = msg1;
*in_out_mr2 = msg2;
*in_out_mr3 = msg3;
}
#ifdef CONFIG_KERNEL_MCS
static inline void arm_sys_nbsend_recv(seL4_Word sys, seL4_Word dest, seL4_Word src, seL4_Word *out_badge,
seL4_Word info_arg,
seL4_Word *out_info, seL4_Word *in_out_mr0, seL4_Word *in_out_mr1, seL4_Word *in_out_mr2,
seL4_Word *in_out_mr3, seL4_Word reply)
{
register seL4_Word src_and_badge asm("x0") = src;
register seL4_Word info asm("x1") = info_arg;
/* Load the beginning of the message info registers */
register seL4_Word msg0 asm("x2") = *in_out_mr0;
register seL4_Word msg1 asm("x3") = *in_out_mr1;
register seL4_Word msg2 asm("x4") = *in_out_mr2;
register seL4_Word msg3 asm("x5") = *in_out_mr3;
register seL4_Word reply_reg asm("x6") = reply;
register seL4_Word dest_reg asm("x8") = dest;
/* Perform the system call. */
register seL4_Word scno asm("x7") = sys;
asm volatile(
"svc #0"
: "+r"(msg0), "+r"(msg1), "+r"(msg2), "+r"(msg3),
"+r"(src_and_badge), "+r"(info)
: "r"(scno), "r"(reply_reg), "r"(dest_reg)
: "memory"
);
*out_badge = src_and_badge;
*out_info = info;
*in_out_mr0 = msg0;
*in_out_mr1 = msg1;
*in_out_mr2 = msg2;
*in_out_mr3 = msg3;
}
#endif
static inline void arm_sys_null(seL4_Word sys)
{
register seL4_Word scno asm("x7") = sys;
asm volatile(
"svc #0"
: /* no outputs */
: "r"(scno)
);
}

View File

@ -0,0 +1,29 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/simple_types.h>
typedef seL4_CPtr seL4_ARM_PageUpperDirectory;
typedef seL4_CPtr seL4_ARM_PageGlobalDirectory;
/* whether the VSpace refers to a PageUpperDirectory or PageGlobalDirectory directly
* depends on the physical address size */
typedef seL4_CPtr seL4_ARM_VSpace;
typedef struct seL4_UserContext_ {
/* frame registers */
seL4_Word pc, sp, spsr, x0, x1, x2, x3, x4, x5, x6, x7, x8, x16, x17, x18, x29, x30;
/* other integer registers */
seL4_Word x9, x10, x11, x12, x13, x14, x15, x19, x20, x21, x22, x23, x24, x25, x26, x27, x28;
/* Thread ID registers */
seL4_Word tpidr_el0, tpidrro_el0;
} seL4_UserContext;
typedef struct seL4_ARM_SMCContext_ {
/* register arguments */
seL4_Word x0, x1, x2, x3, x4, x5, x6, x7;
} seL4_ARM_SMCContext;

View File

@ -0,0 +1,108 @@
--
-- Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
--
-- SPDX-License-Identifier: BSD-2-Clause
--
base 64
block VMFault {
padding 576
field IP 64
field Addr 64
field PrefetchFault 64
field FSR 64
padding 60
field seL4_FaultType 4
}
block NullFault {
padding 832
padding 60
field seL4_FaultType 4
}
block CapFault {
padding 384
field IP 64
field Addr 64
field InRecvPhase 64
field LookupFailureType 64
-- these vary according to LookupFailureType
field MR4 64
field MR5 64
field MR6 64
padding 60
field seL4_FaultType 4
}
block UnknownSyscall {
field X0 64
field X1 64
field X2 64
field X3 64
field X4 64
field X5 64
field X6 64
field X7 64
field FaultIP 64
field SP 64
field LR 64
field SPSR 64
field Syscall 64
padding 60
field seL4_FaultType 4
}
block UserException {
padding 512
field FaultIP 64
field Stack 64
field SPSR 64
field Number 64
field Code 64
padding 60
field seL4_FaultType 4
}
block VGICMaintenance {
padding 768
field IDX 64
padding 60
field seL4_FaultType 4
}
block VCPUFault {
padding 768
padding 32
field HSR 32
padding 60
field seL4_FaultType 4
}
block VPPIEvent {
padding 768
field irq 64
padding 60
field seL4_FaultType 4
}
block Timeout {
padding 704
field data 64
field consumed 64
padding 60
field seL4_FaultType 4
}
--
-- Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
--
-- SPDX-License-Identifier: BSD-2-Clause
--
-- this file contains types shared between libsel4 and the kernel
tagged_union seL4_Fault seL4_FaultType {
-- generic faults
tag NullFault 0
tag CapFault 1
tag UnknownSyscall 2
tag UserException 3
tag Timeout 5
-- arch specific faults
tag VMFault 6
tag VGICMaintenance 7
tag VCPUFault 8
tag VPPIEvent 9
}

View File

@ -0,0 +1,42 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
/* this file is shared between the kernel and libsel4 */
typedef struct seL4_IPCBuffer_ {
seL4_MessageInfo_t tag;
seL4_Word msg[seL4_MsgMaxLength];
seL4_Word userData;
seL4_Word caps_or_badges[seL4_MsgMaxExtraCaps];
seL4_CPtr receiveCNode;
seL4_CPtr receiveIndex;
seL4_Word receiveDepth;
} seL4_IPCBuffer __attribute__((__aligned__(sizeof(struct seL4_IPCBuffer_))));
typedef enum {
seL4_CapFault_IP,
seL4_CapFault_Addr,
seL4_CapFault_InRecvPhase,
seL4_CapFault_LookupFailureType,
seL4_CapFault_BitsLeft,
seL4_CapFault_DepthMismatch_BitsFound,
seL4_CapFault_GuardMismatch_GuardFound = seL4_CapFault_DepthMismatch_BitsFound,
seL4_CapFault_GuardMismatch_BitsFound,
SEL4_FORCE_LONG_ENUM(seL4_CapFault_Msg),
} seL4_CapFault_Msg;
#define seL4_ReadWrite seL4_CapRights_new(0, 0, 1, 1)
#define seL4_AllRights seL4_CapRights_new(1, 1, 1, 1)
#define seL4_CanRead seL4_CapRights_new(0, 0, 1, 0)
#define seL4_CanWrite seL4_CapRights_new(0, 0, 0, 1)
#define seL4_CanGrant seL4_CapRights_new(0, 1, 0, 0)
#define seL4_CanGrantReply seL4_CapRights_new(1, 0, 0, 0)
#define seL4_NoWrite seL4_CapRights_new(1, 1, 1, 0)
#define seL4_NoRead seL4_CapRights_new(1, 1, 0, 1)
#define seL4_NoRights seL4_CapRights_new(0, 0, 0, 0)

View File

@ -0,0 +1,26 @@
--
-- Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
--
-- SPDX-License-Identifier: BSD-2-Clause
--
-- this file contains types shared between libsel4 and the kernel
base 64
block seL4_MessageInfo {
field label 52
field capsUnwrapped 3
field extraCaps 2
field length 7
}
block seL4_CapRights {
padding 32
padding 28
field capAllowGrantReply 1
field capAllowGrant 1
field capAllowRead 1
field capAllowWrite 1
}
-- CNode cap data
block seL4_CNode_CapData {
field guard 58
field guardSize 6
}

View File

@ -0,0 +1,506 @@
/* generated from /Users/ertos/ts/microkit_1.4.1_release/microkit/seL4/libsel4/mode_include/64/sel4/shared_types.bf */
#pragma once
#include <sel4/config.h>
#include <sel4/simple_types.h>
#include <sel4/debug_assert.h>
struct seL4_CNode_CapData {
seL4_Uint64 words[1];
};
typedef struct seL4_CNode_CapData seL4_CNode_CapData_t;
LIBSEL4_INLINE_FUNC seL4_CNode_CapData_t CONST
seL4_CNode_CapData_new(seL4_Uint64 guard, seL4_Uint64 guardSize) {
seL4_CNode_CapData_t seL4_CNode_CapData;
/* fail if user has passed bits that we will override */
seL4_DebugAssert((guard & ~0x3ffffffffffffffull) == ((0 && (guard & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((guardSize & ~0x3full) == ((0 && (guardSize & (1ull << 63))) ? 0x0 : 0));
seL4_CNode_CapData.words[0] = 0
| (guard & 0x3ffffffffffffffull) << 6
| (guardSize & 0x3full) << 0;
return seL4_CNode_CapData;
}
LIBSEL4_INLINE_FUNC void
seL4_CNode_CapData_ptr_new(seL4_CNode_CapData_t *seL4_CNode_CapData_ptr, seL4_Uint64 guard, seL4_Uint64 guardSize) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((guard & ~0x3ffffffffffffffull) == ((0 && (guard & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((guardSize & ~0x3full) == ((0 && (guardSize & (1ull << 63))) ? 0x0 : 0));
seL4_CNode_CapData_ptr->words[0] = 0
| (guard & 0x3ffffffffffffffull) << 6
| (guardSize & 0x3full) << 0;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 CONST
seL4_CNode_CapData_get_guard(seL4_CNode_CapData_t seL4_CNode_CapData) {
seL4_Uint64 ret;
ret = (seL4_CNode_CapData.words[0] & 0xffffffffffffffc0ull) >> 6;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC seL4_CNode_CapData_t CONST
seL4_CNode_CapData_set_guard(seL4_CNode_CapData_t seL4_CNode_CapData, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0xffffffffffffffc0ull >> 6 ) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_CNode_CapData.words[0] &= ~0xffffffffffffffc0ull;
seL4_CNode_CapData.words[0] |= (v64 << 6) & 0xffffffffffffffc0ull;
return seL4_CNode_CapData;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 PURE
seL4_CNode_CapData_ptr_get_guard(seL4_CNode_CapData_t *seL4_CNode_CapData_ptr) {
seL4_Uint64 ret;
ret = (seL4_CNode_CapData_ptr->words[0] & 0xffffffffffffffc0ull) >> 6;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC void
seL4_CNode_CapData_ptr_set_guard(seL4_CNode_CapData_t *seL4_CNode_CapData_ptr, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0xffffffffffffffc0ull >> 6) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_CNode_CapData_ptr->words[0] &= ~0xffffffffffffffc0ull;
seL4_CNode_CapData_ptr->words[0] |= (v64 << 6) & 0xffffffffffffffc0;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 CONST
seL4_CNode_CapData_get_guardSize(seL4_CNode_CapData_t seL4_CNode_CapData) {
seL4_Uint64 ret;
ret = (seL4_CNode_CapData.words[0] & 0x3full) >> 0;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC seL4_CNode_CapData_t CONST
seL4_CNode_CapData_set_guardSize(seL4_CNode_CapData_t seL4_CNode_CapData, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x3full >> 0 ) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_CNode_CapData.words[0] &= ~0x3full;
seL4_CNode_CapData.words[0] |= (v64 << 0) & 0x3full;
return seL4_CNode_CapData;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 PURE
seL4_CNode_CapData_ptr_get_guardSize(seL4_CNode_CapData_t *seL4_CNode_CapData_ptr) {
seL4_Uint64 ret;
ret = (seL4_CNode_CapData_ptr->words[0] & 0x3full) >> 0;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC void
seL4_CNode_CapData_ptr_set_guardSize(seL4_CNode_CapData_t *seL4_CNode_CapData_ptr, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x3full >> 0) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_CNode_CapData_ptr->words[0] &= ~0x3full;
seL4_CNode_CapData_ptr->words[0] |= (v64 << 0) & 0x3f;
}
struct seL4_CapRights {
seL4_Uint64 words[1];
};
typedef struct seL4_CapRights seL4_CapRights_t;
LIBSEL4_INLINE_FUNC seL4_CapRights_t CONST
seL4_CapRights_new(seL4_Uint64 capAllowGrantReply, seL4_Uint64 capAllowGrant, seL4_Uint64 capAllowRead, seL4_Uint64 capAllowWrite) {
seL4_CapRights_t seL4_CapRights;
/* fail if user has passed bits that we will override */
seL4_DebugAssert((capAllowGrantReply & ~0x1ull) == ((0 && (capAllowGrantReply & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((capAllowGrant & ~0x1ull) == ((0 && (capAllowGrant & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((capAllowRead & ~0x1ull) == ((0 && (capAllowRead & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((capAllowWrite & ~0x1ull) == ((0 && (capAllowWrite & (1ull << 63))) ? 0x0 : 0));
seL4_CapRights.words[0] = 0
| (capAllowGrantReply & 0x1ull) << 3
| (capAllowGrant & 0x1ull) << 2
| (capAllowRead & 0x1ull) << 1
| (capAllowWrite & 0x1ull) << 0;
return seL4_CapRights;
}
LIBSEL4_INLINE_FUNC void
seL4_CapRights_ptr_new(seL4_CapRights_t *seL4_CapRights_ptr, seL4_Uint64 capAllowGrantReply, seL4_Uint64 capAllowGrant, seL4_Uint64 capAllowRead, seL4_Uint64 capAllowWrite) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((capAllowGrantReply & ~0x1ull) == ((0 && (capAllowGrantReply & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((capAllowGrant & ~0x1ull) == ((0 && (capAllowGrant & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((capAllowRead & ~0x1ull) == ((0 && (capAllowRead & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((capAllowWrite & ~0x1ull) == ((0 && (capAllowWrite & (1ull << 63))) ? 0x0 : 0));
seL4_CapRights_ptr->words[0] = 0
| (capAllowGrantReply & 0x1ull) << 3
| (capAllowGrant & 0x1ull) << 2
| (capAllowRead & 0x1ull) << 1
| (capAllowWrite & 0x1ull) << 0;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 CONST
seL4_CapRights_get_capAllowGrantReply(seL4_CapRights_t seL4_CapRights) {
seL4_Uint64 ret;
ret = (seL4_CapRights.words[0] & 0x8ull) >> 3;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC seL4_CapRights_t CONST
seL4_CapRights_set_capAllowGrantReply(seL4_CapRights_t seL4_CapRights, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x8ull >> 3 ) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_CapRights.words[0] &= ~0x8ull;
seL4_CapRights.words[0] |= (v64 << 3) & 0x8ull;
return seL4_CapRights;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 PURE
seL4_CapRights_ptr_get_capAllowGrantReply(seL4_CapRights_t *seL4_CapRights_ptr) {
seL4_Uint64 ret;
ret = (seL4_CapRights_ptr->words[0] & 0x8ull) >> 3;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC void
seL4_CapRights_ptr_set_capAllowGrantReply(seL4_CapRights_t *seL4_CapRights_ptr, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x8ull >> 3) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_CapRights_ptr->words[0] &= ~0x8ull;
seL4_CapRights_ptr->words[0] |= (v64 << 3) & 0x8;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 CONST
seL4_CapRights_get_capAllowGrant(seL4_CapRights_t seL4_CapRights) {
seL4_Uint64 ret;
ret = (seL4_CapRights.words[0] & 0x4ull) >> 2;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC seL4_CapRights_t CONST
seL4_CapRights_set_capAllowGrant(seL4_CapRights_t seL4_CapRights, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x4ull >> 2 ) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_CapRights.words[0] &= ~0x4ull;
seL4_CapRights.words[0] |= (v64 << 2) & 0x4ull;
return seL4_CapRights;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 PURE
seL4_CapRights_ptr_get_capAllowGrant(seL4_CapRights_t *seL4_CapRights_ptr) {
seL4_Uint64 ret;
ret = (seL4_CapRights_ptr->words[0] & 0x4ull) >> 2;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC void
seL4_CapRights_ptr_set_capAllowGrant(seL4_CapRights_t *seL4_CapRights_ptr, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x4ull >> 2) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_CapRights_ptr->words[0] &= ~0x4ull;
seL4_CapRights_ptr->words[0] |= (v64 << 2) & 0x4;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 CONST
seL4_CapRights_get_capAllowRead(seL4_CapRights_t seL4_CapRights) {
seL4_Uint64 ret;
ret = (seL4_CapRights.words[0] & 0x2ull) >> 1;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC seL4_CapRights_t CONST
seL4_CapRights_set_capAllowRead(seL4_CapRights_t seL4_CapRights, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x2ull >> 1 ) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_CapRights.words[0] &= ~0x2ull;
seL4_CapRights.words[0] |= (v64 << 1) & 0x2ull;
return seL4_CapRights;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 PURE
seL4_CapRights_ptr_get_capAllowRead(seL4_CapRights_t *seL4_CapRights_ptr) {
seL4_Uint64 ret;
ret = (seL4_CapRights_ptr->words[0] & 0x2ull) >> 1;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC void
seL4_CapRights_ptr_set_capAllowRead(seL4_CapRights_t *seL4_CapRights_ptr, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x2ull >> 1) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_CapRights_ptr->words[0] &= ~0x2ull;
seL4_CapRights_ptr->words[0] |= (v64 << 1) & 0x2;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 CONST
seL4_CapRights_get_capAllowWrite(seL4_CapRights_t seL4_CapRights) {
seL4_Uint64 ret;
ret = (seL4_CapRights.words[0] & 0x1ull) >> 0;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC seL4_CapRights_t CONST
seL4_CapRights_set_capAllowWrite(seL4_CapRights_t seL4_CapRights, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x1ull >> 0 ) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_CapRights.words[0] &= ~0x1ull;
seL4_CapRights.words[0] |= (v64 << 0) & 0x1ull;
return seL4_CapRights;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 PURE
seL4_CapRights_ptr_get_capAllowWrite(seL4_CapRights_t *seL4_CapRights_ptr) {
seL4_Uint64 ret;
ret = (seL4_CapRights_ptr->words[0] & 0x1ull) >> 0;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC void
seL4_CapRights_ptr_set_capAllowWrite(seL4_CapRights_t *seL4_CapRights_ptr, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x1ull >> 0) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_CapRights_ptr->words[0] &= ~0x1ull;
seL4_CapRights_ptr->words[0] |= (v64 << 0) & 0x1;
}
struct seL4_MessageInfo {
seL4_Uint64 words[1];
};
typedef struct seL4_MessageInfo seL4_MessageInfo_t;
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t CONST
seL4_MessageInfo_new(seL4_Uint64 label, seL4_Uint64 capsUnwrapped, seL4_Uint64 extraCaps, seL4_Uint64 length) {
seL4_MessageInfo_t seL4_MessageInfo;
/* fail if user has passed bits that we will override */
seL4_DebugAssert((label & ~0xfffffffffffffull) == ((0 && (label & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((capsUnwrapped & ~0x7ull) == ((0 && (capsUnwrapped & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((extraCaps & ~0x3ull) == ((0 && (extraCaps & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((length & ~0x7full) == ((0 && (length & (1ull << 63))) ? 0x0 : 0));
seL4_MessageInfo.words[0] = 0
| (label & 0xfffffffffffffull) << 12
| (capsUnwrapped & 0x7ull) << 9
| (extraCaps & 0x3ull) << 7
| (length & 0x7full) << 0;
return seL4_MessageInfo;
}
LIBSEL4_INLINE_FUNC void
seL4_MessageInfo_ptr_new(seL4_MessageInfo_t *seL4_MessageInfo_ptr, seL4_Uint64 label, seL4_Uint64 capsUnwrapped, seL4_Uint64 extraCaps, seL4_Uint64 length) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((label & ~0xfffffffffffffull) == ((0 && (label & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((capsUnwrapped & ~0x7ull) == ((0 && (capsUnwrapped & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((extraCaps & ~0x3ull) == ((0 && (extraCaps & (1ull << 63))) ? 0x0 : 0));
seL4_DebugAssert((length & ~0x7full) == ((0 && (length & (1ull << 63))) ? 0x0 : 0));
seL4_MessageInfo_ptr->words[0] = 0
| (label & 0xfffffffffffffull) << 12
| (capsUnwrapped & 0x7ull) << 9
| (extraCaps & 0x3ull) << 7
| (length & 0x7full) << 0;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 CONST
seL4_MessageInfo_get_label(seL4_MessageInfo_t seL4_MessageInfo) {
seL4_Uint64 ret;
ret = (seL4_MessageInfo.words[0] & 0xfffffffffffff000ull) >> 12;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t CONST
seL4_MessageInfo_set_label(seL4_MessageInfo_t seL4_MessageInfo, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0xfffffffffffff000ull >> 12 ) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_MessageInfo.words[0] &= ~0xfffffffffffff000ull;
seL4_MessageInfo.words[0] |= (v64 << 12) & 0xfffffffffffff000ull;
return seL4_MessageInfo;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 PURE
seL4_MessageInfo_ptr_get_label(seL4_MessageInfo_t *seL4_MessageInfo_ptr) {
seL4_Uint64 ret;
ret = (seL4_MessageInfo_ptr->words[0] & 0xfffffffffffff000ull) >> 12;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC void
seL4_MessageInfo_ptr_set_label(seL4_MessageInfo_t *seL4_MessageInfo_ptr, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0xfffffffffffff000ull >> 12) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_MessageInfo_ptr->words[0] &= ~0xfffffffffffff000ull;
seL4_MessageInfo_ptr->words[0] |= (v64 << 12) & 0xfffffffffffff000;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 CONST
seL4_MessageInfo_get_capsUnwrapped(seL4_MessageInfo_t seL4_MessageInfo) {
seL4_Uint64 ret;
ret = (seL4_MessageInfo.words[0] & 0xe00ull) >> 9;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t CONST
seL4_MessageInfo_set_capsUnwrapped(seL4_MessageInfo_t seL4_MessageInfo, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0xe00ull >> 9 ) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_MessageInfo.words[0] &= ~0xe00ull;
seL4_MessageInfo.words[0] |= (v64 << 9) & 0xe00ull;
return seL4_MessageInfo;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 PURE
seL4_MessageInfo_ptr_get_capsUnwrapped(seL4_MessageInfo_t *seL4_MessageInfo_ptr) {
seL4_Uint64 ret;
ret = (seL4_MessageInfo_ptr->words[0] & 0xe00ull) >> 9;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC void
seL4_MessageInfo_ptr_set_capsUnwrapped(seL4_MessageInfo_t *seL4_MessageInfo_ptr, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0xe00ull >> 9) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_MessageInfo_ptr->words[0] &= ~0xe00ull;
seL4_MessageInfo_ptr->words[0] |= (v64 << 9) & 0xe00;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 CONST
seL4_MessageInfo_get_extraCaps(seL4_MessageInfo_t seL4_MessageInfo) {
seL4_Uint64 ret;
ret = (seL4_MessageInfo.words[0] & 0x180ull) >> 7;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t CONST
seL4_MessageInfo_set_extraCaps(seL4_MessageInfo_t seL4_MessageInfo, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x180ull >> 7 ) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_MessageInfo.words[0] &= ~0x180ull;
seL4_MessageInfo.words[0] |= (v64 << 7) & 0x180ull;
return seL4_MessageInfo;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 PURE
seL4_MessageInfo_ptr_get_extraCaps(seL4_MessageInfo_t *seL4_MessageInfo_ptr) {
seL4_Uint64 ret;
ret = (seL4_MessageInfo_ptr->words[0] & 0x180ull) >> 7;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC void
seL4_MessageInfo_ptr_set_extraCaps(seL4_MessageInfo_t *seL4_MessageInfo_ptr, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x180ull >> 7) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_MessageInfo_ptr->words[0] &= ~0x180ull;
seL4_MessageInfo_ptr->words[0] |= (v64 << 7) & 0x180;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 CONST
seL4_MessageInfo_get_length(seL4_MessageInfo_t seL4_MessageInfo) {
seL4_Uint64 ret;
ret = (seL4_MessageInfo.words[0] & 0x7full) >> 0;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t CONST
seL4_MessageInfo_set_length(seL4_MessageInfo_t seL4_MessageInfo, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x7full >> 0 ) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_MessageInfo.words[0] &= ~0x7full;
seL4_MessageInfo.words[0] |= (v64 << 0) & 0x7full;
return seL4_MessageInfo;
}
LIBSEL4_INLINE_FUNC seL4_Uint64 PURE
seL4_MessageInfo_ptr_get_length(seL4_MessageInfo_t *seL4_MessageInfo_ptr) {
seL4_Uint64 ret;
ret = (seL4_MessageInfo_ptr->words[0] & 0x7full) >> 0;
/* Possibly sign extend */
if (__builtin_expect(!!(0 && (ret & (1ull << (63)))), 0)) {
ret |= 0x0;
}
return ret;
}
LIBSEL4_INLINE_FUNC void
seL4_MessageInfo_ptr_set_length(seL4_MessageInfo_t *seL4_MessageInfo_ptr, seL4_Uint64 v64) {
/* fail if user has passed bits that we will override */
seL4_DebugAssert((((~0x7full >> 0) | 0x0) & v64) == ((0 && (v64 & (1ull << (63)))) ? 0x0 : 0));
seL4_MessageInfo_ptr->words[0] &= ~0x7full;
seL4_MessageInfo_ptr->words[0] |= (v64 << 0) & 0x7f;
}

View File

@ -0,0 +1,139 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/macros.h>
/*
* Data | short | int | long | long | void* | notes
* model | | | | long | size_t |
* -------+-------+-----+------+------+--------+----------------
* IP16 | 16 | 16 | 32 | 64 | 16 | MS-DOS SMALL memory model
* LP32 | 16 | 16 | 32 | 64 | 32 | MS-DOS LARGE memory model
* ILP32 | 16 | 32 | 32 | 64 | 32 | common for a 32-bit OS
* LLP64 | 16 | 32 | 32 | 64 | 64 | 64-bit Windows, VC++, MinGW
* LP64 | 16 | 32 | 64 | 64 | 64 | most 64-bit Unix systems
* ILP64 | 16 | 64 | 64 | 64 | 64 | SPARC64, Solaris
* SILP64 | 64 | 64 | 64 | 64 | 64 | UNICOS
*
* libsel4 requires ILP32 on 32-bit systems and and LP64 on 64-bit systems
*/
/* Get the architectural definitions and types */
#include <sel4/arch/simple_types.h>
#define seL4_integer_size_assert(_type_, _size_) \
SEL4_COMPILE_ASSERT( \
sizeof_##_type_##_is_##_size_##_byte, \
sizeof(_type_) == _size_ )
/* C99 defines that this is at least 8-bit */
#define _seL4_int8_type char
typedef signed _seL4_int8_type seL4_Int8;
typedef unsigned _seL4_int8_type seL4_Uint8;
seL4_integer_size_assert(seL4_Int8, 1)
seL4_integer_size_assert(seL4_Uint8, 1)
/* C99 defines that a 'short int' is at least 16 bits. Note that 'short' is
* no basic C type, but only a type modifier. If nothing else is given, the
* default type is 'int' and thus it is often omitted.
*/
#define _seL4_int16_type short int
typedef signed _seL4_int16_type seL4_Int16;
typedef unsigned _seL4_int16_type seL4_Uint16;
seL4_integer_size_assert(seL4_Int16, 2)
seL4_integer_size_assert(seL4_Uint16, 2)
/* C99 does not define that an 'int' is 32-bit, it just has to be no smaller
* than a 'short int'. We require ILP32 on 32-bit systems and and LP64 on 64-bit
* systems, so 'int' is 32-bits. */
#define _seL4_int32_type int
typedef signed _seL4_int32_type seL4_Int32;
typedef unsigned _seL4_int32_type seL4_Uint32;
seL4_integer_size_assert(seL4_Int32, 4)
seL4_integer_size_assert(seL4_Uint32, 4)
/* There is no standard 64-bit type in C, so the architecture specific headers
* must define what to use. C99 just defines that 'long' is at least 32 bits and
* 'long long' at least 64-bit. Note that neither 'long' nor 'long long' are
* basic C types, they are only type modifiers. If nothing else is given, the
* default base type is 'int' and thus it is often omitted.
*/
#if defined(SEL4_INT64_IS_LONG)
#define _seL4_int64_type long int
#define _seL4_int64_fmt l // printf() formatting, integer suffix
#elif defined(SEL4_INT64_IS_LONG_LONG)
#define _seL4_int64_type long long int
#define _seL4_int64_fmt ll // printf() formatting, integer suffix
#else
#error missing definition for 64-bit types
#endif
typedef signed _seL4_int64_type seL4_Int64;
typedef unsigned _seL4_int64_type seL4_Uint64;
/* Define printf() format specifiers for seL4_Int64 and seL4_Uint64. The helper
* macros ensure these format strings are atoms. The macros passed are evaluated
* before the concatenation and stringizing happens.
*/
#define _macro_str_concat_helper2(x) #x
#define _macro_str_concat_helper1(x,y) _macro_str_concat_helper2(x ## y)
#define _macro_str_concat(x,y) _macro_str_concat_helper1(x,y)
#define SEL4_PRId64 _macro_str_concat(_seL4_int64_fmt, d)
#define SEL4_PRIi64 _macro_str_concat(_seL4_int64_fmt, i)
#define SEL4_PRIu64 _macro_str_concat(_seL4_int64_fmt, u)
#define SEL4_PRIx64 _macro_str_concat(_seL4_int64_fmt, x)
/* Define boolean type and true/false */
#define seL4_True 1
#define seL4_False 0
typedef seL4_Int8 seL4_Bool;
/* Define seL4_Null */
#ifdef __cplusplus
#define seL4_Null 0L
#else
#define seL4_Null ((void*)0)
#endif // __cplusplus
/* Define seL4_Word */
#if defined(SEL4_WORD_IS_UINT32)
typedef seL4_Uint32 seL4_Word;
#define _seL4_word_fmt /* empty */
#elif defined(SEL4_WORD_IS_UINT64)
typedef seL4_Uint64 seL4_Word;
#define _seL4_word_fmt _seL4_int64_fmt
#else
#error missing definition for SEL4_WORD type
#endif
/* printf() format specifiers for seL4_Word */
#define SEL4_PRId_word _macro_str_concat(_seL4_word_fmt, d)
#define SEL4_PRIi_word _macro_str_concat(_seL4_word_fmt, i)
#define SEL4_PRIu_word _macro_str_concat(_seL4_word_fmt, u)
#define SEL4_PRIx_word _macro_str_concat(_seL4_word_fmt, x)
#define SEL4_PRI_word SEL4_PRIu_word
typedef seL4_Word seL4_CPtr;
/* sanity check that the seL4_Word matches the definitions of the constants */
#include <sel4/sel4_arch/constants.h>
SEL4_COMPILE_ASSERT(
seL4_WordSizeBits_matches,
sizeof(seL4_Word) == (1u << seL4_WordSizeBits))
SEL4_COMPILE_ASSERT(
seL4_WordBits_matches,
8 * sizeof(seL4_Word) == seL4_WordBits)

View File

@ -0,0 +1,71 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
/* This header was generated by kernel/tools/syscall_header_gen.py.
*
* To add a system call number, edit kernel/libsel4/include/api/syscall.xml
*
*/
#pragma once
#include <sel4/config.h>
typedef enum {
seL4_SysCall = -1,
seL4_SysReplyRecv = -2,
seL4_SysNBSendRecv = -3,
seL4_SysNBSendWait = -4,
seL4_SysSend = -5,
seL4_SysNBSend = -6,
seL4_SysRecv = -7,
seL4_SysNBRecv = -8,
seL4_SysWait = -9,
seL4_SysNBWait = -10,
seL4_SysYield = -11,
#if defined(CONFIG_PRINTING)
seL4_SysDebugPutChar = -12,
seL4_SysDebugDumpScheduler = -13,
#endif /* defined(CONFIG_PRINTING) */
#if defined(CONFIG_DEBUG_BUILD)
seL4_SysDebugHalt = -14,
seL4_SysDebugCapIdentify = -15,
seL4_SysDebugSnapshot = -16,
seL4_SysDebugNameThread = -17,
#endif /* defined(CONFIG_DEBUG_BUILD) */
#if (defined(CONFIG_DEBUG_BUILD) && defined(CONFIG_ENABLE_SMP_SUPPORT))
seL4_SysDebugSendIPI = -18,
#endif /* (defined(CONFIG_DEBUG_BUILD) && defined(CONFIG_ENABLE_SMP_SUPPORT)) */
#if defined(CONFIG_DANGEROUS_CODE_INJECTION)
seL4_SysDebugRun = -19,
#endif /* defined(CONFIG_DANGEROUS_CODE_INJECTION) */
#if defined(CONFIG_ENABLE_BENCHMARKS)
seL4_SysBenchmarkFlushCaches = -20,
seL4_SysBenchmarkResetLog = -21,
seL4_SysBenchmarkFinalizeLog = -22,
seL4_SysBenchmarkSetLogBuffer = -23,
seL4_SysBenchmarkNullSyscall = -24,
#endif /* defined(CONFIG_ENABLE_BENCHMARKS) */
#if defined(CONFIG_BENCHMARK_TRACK_UTILISATION)
seL4_SysBenchmarkGetThreadUtilisation = -25,
seL4_SysBenchmarkResetThreadUtilisation = -26,
#endif /* defined(CONFIG_BENCHMARK_TRACK_UTILISATION) */
#if (defined(CONFIG_DEBUG_BUILD) && defined(CONFIG_BENCHMARK_TRACK_UTILISATION))
seL4_SysBenchmarkDumpAllThreadsUtilisation = -27,
seL4_SysBenchmarkResetAllThreadsUtilisation = -28,
#endif /* (defined(CONFIG_DEBUG_BUILD) && defined(CONFIG_BENCHMARK_TRACK_UTILISATION)) */
#if defined(CONFIG_KERNEL_X86_DANGEROUS_MSR)
seL4_SysX86DangerousWRMSR = -29,
seL4_SysX86DangerousRDMSR = -30,
#endif /* defined(CONFIG_KERNEL_X86_DANGEROUS_MSR) */
#if defined(CONFIG_VTX)
seL4_SysVMEnter = -31,
#endif /* defined(CONFIG_VTX) */
#if defined(CONFIG_SET_TLS_BASE_SELF)
seL4_SysSetTLSBase = -32,
#endif /* defined(CONFIG_SET_TLS_BASE_SELF) */
SEL4_FORCE_LONG_ENUM(seL4_Syscall_ID)
} seL4_Syscall_ID;

View File

@ -0,0 +1,392 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <sel4/functions.h>
/**
* @defgroup SystemCalls System Calls
* @{
*
*/
#ifdef CONFIG_KERNEL_MCS
#include "syscalls_mcs.h"
#else
#include "syscalls_master.h"
#endif
/**
* @defgroup DebuggingSystemCalls
* This section documents debugging system calls available when the kernel is
* build with the `DEBUG_BUILD` configuration. For any system calls that rely
* on a kernel serial driver, `PRINTING` must also be enabled.
*
* @{
*/
#ifdef CONFIG_PRINTING
/**
* @xmlonly <manual name="Put Char" label="sel4_debugputchar"/> @endxmlonly
* @brief Output a single char through the kernel.
*
* Use the kernel serial driver to output a single character. This is useful for
* debugging when a user level serial driver is not available.
*
* @param c The character to output.
*
*/
LIBSEL4_INLINE_FUNC void
seL4_DebugPutChar(char c);
/**
* @xmlonly <manual name="Dump Scheduler" label="sel4_dumpscheduler"/> @endxmlonly
* @brief Output the contents of the kernel scheduler.
*
* Dump the state of the all TCB objects to kernel serial output. This system call
* will output a table containing:
* - Address: the address of the TCB object for that thread,
* - Name: the name of the thread (if set),
* - IP: the contents of the instruction pointer the thread is at,
* - Priority: the priority of that thread,
* - State : the state of the thread.
*/
LIBSEL4_INLINE_FUNC void
seL4_DebugDumpScheduler(void);
#endif
#if CONFIG_DEBUG_BUILD
/**
* @xmlonly <manual name="Halt" label="sel4_debughalt"/> @endxmlonly
* @brief Halt the system.
*
* This debugging system call will cause the kernel immediately cease responding to
* system calls. The kernel will switch permanently to the idle thread with
* interrupts disabled. Depending on the platform, the kernel may switch
* the hardware into a low-power state.
*
*/
LIBSEL4_INLINE_FUNC void
seL4_DebugHalt(void);
/**
* @xmlonly <manual name="Snapshot" label="sel4_debugsnapshot"/> @endxmlonly
* @brief Output a capDL dump of the current kernel state.
*
* This debugging system call will output all of the capabilities in the current
* kernel using capDL.
*
*/
LIBSEL4_INLINE_FUNC void
seL4_DebugSnapshot(void);
/**
* @xmlonly <manual name="Cap Identify" label="sel4_debugcapidentify"/> @endxmlonly
* @brief Identify the type of a capability in the current CSpace.
*
* This debugging system call returns the type of capability in a capability
* slot in the current CSpace. The type returned is not a libsel4 type, but
* refers to an internal seL4 type. This can be looked up in a built kernel by
* looking for the (generated) `enum cap_tag`, type `cap_tag_t`.
*
* @param cap A capability slot in the current CSpace.
* @return The type of capability passed in.
*
*/
LIBSEL4_INLINE_FUNC seL4_Uint32
seL4_DebugCapIdentify(seL4_CPtr cap);
/**
* @xmlonly <manual name="Name Thread" label="sel4_debugnamethread"/> @endxmlonly
* @brief Name a thread.
*
* Name a thread. This name will then be output by the kernel in all debugging output.
* Note that the max name length that can be passed to this function is limited by the
* number of chars that will fit in an IPC message (`seL4_MsgMaxLength` multiplied by the
* amount of chars that fit in a word). However the name is also truncated in order to fit into a TCB object.
* For some platforms you may need to increase `seL4_TCBBits` by 1 in a debug build in order to
* fit a long enough name.
*
* @param tcb A capability to the tcb object for the thread to name.
* @param name The name for the thread.
*
*/
LIBSEL4_INLINE_FUNC void
seL4_DebugNameThread(seL4_CPtr tcb, const char *name);
#if defined(CONFIG_ENABLE_SMP_SUPPORT) && defined(CONFIG_ARCH_ARM)
/**
* @xmlonly <manual name="Send SGI 0-15" label="sel4_debugsendipi"/> @endxmlonly
* @brief Sends arbitrary SGI.
*
* Send an arbitrary SGI (core-specific interrupt 0-15) to the specified target core.
*
* @param target The target core ID.
* @param irq The SGI number (0-15).
*
*/
LIBSEL4_INLINE_FUNC void
seL4_DebugSendIPI(seL4_Uint8 target, unsigned irq);
#endif
#endif
#ifdef CONFIG_DANGEROUS_CODE_INJECTION
/**
* @xmlonly <manual name="Run" label="sel4_debugrun"/> @endxmlonly
* @brief Run a user level function in kernel mode.
*
* This extremely dangerous function is for running benchmarking and debugging code that
* needs to be executed in kernel mode from userlevel. It should never be used in a release kernel.
* This works because the kernel can access all user mappings of device memory, and does not switch page directories
* on kernel entry.
*
* Unlike the other system calls in this section, `seL4_DebugRun` does not
* depend on the `DEBUG_BUILD` configuration option, but its own config
* variable `DANGEROUS_CODE_INJECTION`.
*
* @param userfn The address in userspace of the function to run.
* @param userarg A single argument to pass to the function.
*
*/
LIBSEL4_INLINE_FUNC void
seL4_DebugRun(void (* userfn)(void *), void *userarg);
#endif
/** @} */
/**
* @defgroup BenchmarkingSystemCalls
* This section documents system calls available when the kernel is
* configured with benchmarking enabled.
* There are several different benchmarking modes which can be configured
* when building the kernel:
* 1. `BENCHMARK_TRACEPOINTS`: Enable using tracepoints in the kernel and timing code.
* 2. `BENCHMARK_TRACK_KERNEL_ENTRIES`: Keep track of information on kernel entries.
* 3. `BENCHMARK_TRACK_UTILISATION`: Allow users to get CPU timing info for the system, threads and/or idle thread.
*
* `BENCHMARK_TRACEPOINTS` and `BENCHMARK_TRACK_KERNEL_ENTRIES` use a log buffer that has to be allocated by the user and mapped
* to a fixed location in the kernel window.
* All of timing information is output in cycles.
*
* @{
*/
#ifdef CONFIG_ENABLE_BENCHMARKS
/*
*/
/**
* @xmlonly <manual name="Reset Log" label="sel4_benchmarkresetlog"/> @endxmlonly
* @brief Reset benchmark logging.
*
* The behaviour of this system call depends on benchmarking mode in action while invoking
* this system call:
* 1. `BENCHMARK_TRACEPOINTS`: resets the log index to 0,
* 2. `BENCHMARK_TRACK_KERNEL_ENTRIES`: as above,
* 3. `BENCHMARK_TRACK_UTILISATION`: resets benchmark and current thread
* start time (to the time of invoking this syscall), resets idle
* thread utilisation to 0, and starts tracking utilisation.
*
* @return A `seL4_Error` error if the user-level log buffer has not been set by the user
* (`BENCHMARK_TRACEPOINTS`/`BENCHMARK_TRACK_KERNEL_ENTRIES`).
*/
LIBSEL4_INLINE_FUNC seL4_Error
seL4_BenchmarkResetLog(void);
/**
* @xmlonly <manual name="Finalize Log" label="sel4_benchmarkfinalizelog"/> @endxmlonly
* @brief Stop benchmark logging.
*
* The behaviour of this system call depends on benchmarking mode in action while invoking this system call:
* 1. `BENCHMARK_TRACEPOINTS`: Sets the final log buffer index to the current index,
* 2. `BENCHMARK_TRACK_KERNEL_ENTRIES`: as above,
* 3. `BENCHMARK_TRACK_UTILISATION`: sets benchmark end time to current time, stops tracking utilisation.
*
* @return The index of the final entry in the log buffer (if `BENCHMARK_TRACEPOINTS`/`BENCHMARK_TRACK_KERNEL_ENTRIES` are enabled).
*
*/
LIBSEL4_INLINE_FUNC seL4_Word
seL4_BenchmarkFinalizeLog(void);
/**
* @xmlonly <manual name="Set Log Buffer" label="sel4_benchmarksetlogbuffer"/> @endxmlonly
* @brief Set log buffer.
*
* Provide a large frame object for the kernel to use as a log-buffer.
* The object must not be device memory, and must be `seL4_LargePageBits` in size.
*
* @param[in] frame_cptr A capability pointer to a user allocated frame of seL4_LargePage size.
* @return A `seL4_IllegalOperation` error if `frame_cptr` is not valid and couldn't set the buffer.
*
*/
LIBSEL4_INLINE_FUNC seL4_Error
seL4_BenchmarkSetLogBuffer(seL4_Word frame_cptr);
/**
* @xmlonly <manual name="Null Syscall" label="sel4_benchmarknullsyscall"/> @endxmlonly
* @brief Null system call that enters and exits the kernel immediately, for timing kernel traps in microbenchmarks.
*
* Used to time kernel traps (in and out).
*
*/
LIBSEL4_INLINE_FUNC void
seL4_BenchmarkNullSyscall(void);
/**
* @xmlonly <manual name="Flush Caches" label="sel4_benchmarkflushcaches"/> @endxmlonly
* @brief Flush hardware caches.
*
* Flush all possible hardware caches for this platform.
*/
LIBSEL4_INLINE_FUNC void
seL4_BenchmarkFlushCaches(void);
#ifdef CONFIG_ARCH_ARM
/**
* @xmlonly <manual name="Flush L1 Caches" label="sel4_benchmarkflushl1caches"/> @endxmlonly
* @brief Flush L1 caches.
*
* Flush L1 caches for this platform (currently only support for ARM). Allow to specify the cache type
* to be flushed (i.e. instruction cache only, data cache only and both instruction cache and data cache).
*
* @param[in] cache_type L1 Cache Type to be flushed
*/
LIBSEL4_INLINE_FUNC void
seL4_BenchmarkFlushL1Caches(seL4_Word cache_type);
#endif
#ifdef CONFIG_BENCHMARK_TRACK_UTILISATION
/**
* @xmlonly <manual name="Get Thread Utilisation" label="sel4_benchmarkgetthreadutilisation"/> @endxmlonly
* @brief Get utilisation timing information.
*
* Get timing information for the system, requested thread and idle thread. Such information is written
* into the caller's IPC buffer; see the definition of `benchmark_track_util_ipc_index` enum for more
* details on the data/format returned on the IPC buffer.
*
* @param[in] tcb_cptr TCB cap pointer to a thread to get CPU utilisation for.
*/
LIBSEL4_INLINE_FUNC void
seL4_BenchmarkGetThreadUtilisation(seL4_Word tcb_cptr);
/**
* @xmlonly <manual name="Reset Thread Utilisation" label="sel4_benchmarkresetthreadutilisation"/> @endxmlonly
* @brief Reset utilisation timing for a specific thread.
*
* Reset the kernel's timing information data (start time and utilisation) for a specific thread.
*
* @param[in] tcb_cptr TCB cap pointer to a thread to get CPU utilisation for.
*
*/
LIBSEL4_INLINE_FUNC void
seL4_BenchmarkResetThreadUtilisation(seL4_Word tcb_cptr);
#ifdef CONFIG_DEBUG_BUILD
/**
* @xmlonly <manual name="Dump All Threads Utilisation" label="sel4_benchmarkdumpallthreadsutilisation"/> @endxmlonly
* @brief Print the current accumulated cycle count for every thread on the current node.
*
* Uses kernel's printf to print number of cycles on each line in the following format: thread_name,thread_cycles
*
*/
LIBSEL4_INLINE_FUNC void
seL4_BenchmarkDumpAllThreadsUtilisation(void);
/**
* @xmlonly <manual name="Reset All Threads Utilisation" label="sel4_benchmarkresetallthreadsutilisation"/> @endxmlonly
* @brief Reset the accumulated cycle count for every thread on the current node.
*
* Reset the cycle count for each thread to 0.
*
*/
LIBSEL4_INLINE_FUNC void
seL4_BenchmarkResetAllThreadsUtilisation(void);
#endif
#endif
#endif
/** @} */
#ifdef CONFIG_ARCH_X86
/**
* @defgroup X86SystemCalls X86 System Calls
* @{
*/
#ifdef CONFIG_VTX
/**
* @xmlonly <manual name="VM Enter" label="sel4_vmenter"/> @endxmlonly
* @brief Change current thread to execute from its bound VCPU
*
* Changes the execution mode of the current thread from normal TCB execution, to
* guest execution using its bound VCPU.
* @xmlonly
* <docref>For details on VCPUs and execution modes see <autoref label="sec:virt"/>.</docref>
* @endxmlonly
*
* Invoking `seL4_VMEnter` is similar to replying to a fault in that updates to the registers
* can be given in the message, but unlike a fault no message info
* @xmlonly
* <docref>(see <autoref label="sec:messageinfo"/>)</docref>
* @endxmlonly
* is sent as the registers are not optional and the number that must be sent is fixed.
* The mapping of hardware register to message register is
* - `SEL4_VMENTER_CALL_EIP_MR` Address to start executing instructions at in the guest mode
* - `SEL4_VMENTER_CALL_CONTROL_PPC_MR` New value for the Primary Processor Based VM Execution Controls
* - `SEL4_VMENTER_CALL_CONTROL_ENTRY_MR` New value for the VM Entry Controls
*
* On return these same three message registers will be filled with the values at the point
* that the privileged mode ceased executing. If this function returns with `SEL4_VMENTER_RESULT_FAULT`
* then the following additional message registers will be filled out
* - `SEL4_VMENTER_FAULT_REASON_MR`
* - `SEL4_VMENTER_FAULT_QUALIFICATION_MR`
* - `SEL4_VMENTER_FAULT_INSTRUCTION_LEN_MR`
* - `SEL4_VMENTER_FAULT_GUEST_PHYSICAL_MR`
* - `SEL4_VMENTER_FAULT_RFLAGS_MR`
* - `SEL4_VMENTER_FAULT_GUEST_INT_MR`
* - `SEL4_VMENTER_FAULT_CR3_MR`
* - `SEL4_VMENTER_FAULT_EAX`
* - `SEL4_VMENTER_FAULT_EBX`
* - `SEL4_VMENTER_FAULT_ECX`
* - `SEL4_VMENTER_FAULT_EDX`
* - `SEL4_VMENTER_FAULT_ESI`
* - `SEL4_VMENTER_FAULT_EDI`
* - `SEL4_VMENTER_FAULT_EBP`
*
* @param[out] sender The address to write sender information to.
* If the syscall returns due to receiving a notification
* on the bound notification then the sender information
* is the badge of the notification capability that was invoked.
* This parameter is ignored if `NULL`.
* @return `SEL4_VMENTER_RESULT_NOTIF` if a notification was received or `SEL4_VMENTER_RESULT_FAULT`
* if the guest mode execution faulted for any reason
*/
LIBSEL4_INLINE_FUNC seL4_Word
seL4_VMEnter(seL4_Word *sender);
#endif
/** @} */
#endif
/** @} */
#ifdef CONFIG_SET_TLS_BASE_SELF
/**
* @xmlonly <manual name="Set TLS Base" label="sel4_settlsbase"/> @endxmlonly
* @brief Set the TLS base address and register of the currently executing thread.
*
* This stores the base address of the TLS region in the register
* reserved for that purpose on the given platform.
*
* Each platform has a specific register reserved for tracking the
* base address of the TLS region (as sepcified in the ELF standard) in
* a manner compatible with the TLS method used with that architecture.
*
* @param tls_base The new base address to store in the register.
*/
LIBSEL4_INLINE_FUNC void
seL4_SetTLSBase(seL4_Word tls_base);
#endif

View File

@ -0,0 +1,231 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
/**
* @defgroup GeneralSystemCalls System Calls (non-MCS)
* @{
*/
/**
* @xmlonly <manual name="Send" label="sel4_send"/> @endxmlonly
* @brief Send to a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_send"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Recv" label="sel4_recv"/> @endxmlonly
* @brief Block until a message is received on an endpoint
*
* @xmlonly
* <docref>See <autoref label="sec:sys_recv"/></docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Recv(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Call" label="sel4_call"/> @endxmlonly
* @brief Call a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_call"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Reply" label="sel4_reply"/> @endxmlonly
* @brief Perform a send to a one-off reply capability stored when
* the thread was last called. Does nothing if there is no
* reply capability which can happen if the blocked thread
* was unblocked via an operation such as destroying it.
*
* @xmlonly
* <docref>See <autoref label="sec:sys_reply"/></docref>
* @endxmlonly
*
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_Reply(seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Non-Blocking Send" label="sel4_nbsend"/> @endxmlonly
* @brief Perform a non-blocking send to a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbsend"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Reply Recv" label="sel4_replyrecv"/> @endxmlonly
* @brief Perform a reply followed by a receive in one system call
*
* @xmlonly
* <docref>See <autoref label="sec:sys_replyrecv"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_ReplyRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_Word *sender);
/**
* @xmlonly <manual name="Non-Blocking Recv" label="sel4_nbrecv"/> @endxmlonly
* @brief Receive a message from an endpoint but do not block
* in the case that no messages are pending
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbrecv"/></docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_NBRecv(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Yield" label="sel4_yield"/> @endxmlonly
* @brief Donate the remaining timeslice to a thread of the same priority
*
* @xmlonly
* <docref>See <autoref label="sec:sys_yield"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC void
seL4_Yield(void);
/**
* @xmlonly <manual name="Signal" label="sel4_signal"/> @endxmlonly
* @brief Signal a notification
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_Send().
* It is useful for signalling a notification.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_Send"/> in <autoref label="sec:sys_send"/>.</docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
*/
LIBSEL4_INLINE_FUNC void
seL4_Signal(seL4_CPtr dest);
/**
* @xmlonly <manual name="Wait" label="sel4_wait"/> @endxmlonly
* @brief Perform a receive on a notification object
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_Recv().
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_Recv"/> in <autoref label="sec:sys_recv"/>.</docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*/
LIBSEL4_INLINE_FUNC void
seL4_Wait(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Poll" label="sel4_poll"/> @endxmlonly
* @brief Perform a non-blocking receive on a notification object
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_NBRecv().
* It is useful for doing a non-blocking wait on a notification.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_NBRecv"/> in <autoref label="sec:sys_nbrecv"/>.</docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Poll(seL4_CPtr src, seL4_Word *sender);
/** @} */

View File

@ -0,0 +1,306 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
/**
* @defgroup MCSSystemCalls MCS System Calls
* @{
*/
/**
* @xmlonly <manual name="Send" label="sel4_mcs_send"/> @endxmlonly
* @brief Send to a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_send"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_Send(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Recv" label="sel4_mcs_recv"/> @endxmlonly
* @brief Block until a message is received on an endpoint
*
* @xmlonly
* <docref>See <autoref label="sec:sys_recv"/></docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @param[in] reply The capability to the reply object to use on a call (only used on MCS).
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Recv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply);
/**
* @xmlonly <manual name="Call" label="sel4_mcs_call"/> @endxmlonly
* @brief Call a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_call"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Call(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Non-Blocking Send" label="sel4_mcs_nbsend"/> @endxmlonly
* @brief Perform a non-blocking send to a capability
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbsend"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
*/
LIBSEL4_INLINE_FUNC void
seL4_NBSend(seL4_CPtr dest, seL4_MessageInfo_t msgInfo);
/**
* @xmlonly <manual name="Reply Recv" label="sel4_mcs_replyrecv"/> @endxmlonly
* @brief Perform a reply followed by a receive in one system call
*
* @xmlonly
* <docref>See <autoref label="sec:sys_replyrecv"/></docref>
* @endxmlonly
*
* @param[in] src The capability to perform the receive on.
* @param[in] msgInfo The messageinfo structure for the IPC.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @param[in] reply The capability to the reply object, which is first invoked and then used
* for the receive phase to store a new reply capability.
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_ReplyRecv(seL4_CPtr src, seL4_MessageInfo_t msgInfo, seL4_Word *sender, seL4_CPtr reply);
/**
* @xmlonly <manual name="Non-Blocking Recv" label="sel4_mcs_nbrecv"/> @endxmlonly
* @brief Receive a message from an endpoint but do not block
* in the case that no messages are pending
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbrecv"/></docref>
* @endxmlonly
*
* @param[in] src The capability to receive on.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @param[in] reply The capability to the reply object to use on a call.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_NBRecv(seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply);
/**
* @xmlonly <manual name="Non-Blocking Send Recv" label="sel4_nbsendrecv"/> @endxmlonly
* @brief Non-blocking send on one capability, and a blocking receive on another in a single
* system call.
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbsendrecv"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @param[in] src The capability to receive on.
* @param[in] reply The capability to the reply object, which is first invoked and then used
* for the receive phase to store a new reply capability.
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* as described in <autoref label="sec:messageinfo"/>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_NBSendRecv(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender, seL4_CPtr reply);
/**
* @xmlonly <manual name="Non-Blocking Send Wait" label="sel4_nbsendwait"/> @endxmlonly
* @brief Non-blocking invoke of a capability and wait on another in one system call
*
* @xmlonly
* <docref>See <autoref label="sec:sys_nbsendwait"/></docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
* @param[in] msgInfo The messageinfo structure for the IPC.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @param[in] src The capability to receive on.
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* as described in <autoref label="sec:messageinfo"/>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_NBSendWait(seL4_CPtr dest, seL4_MessageInfo_t msgInfo, seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Yield" label="sel4_mcs_yield"/> @endxmlonly
* @brief Yield the remaining timeslice. Periodic threads will not be scheduled again until their
* next sporadic replenishment.
*
* @xmlonly
* <docref>See <autoref label="sec:sys_yield"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC void
seL4_Yield(void);
/**
* @xmlonly <manual name="Wait" label="sel4_mcs_wait"/> @endxmlonly
* @brief Perform a wait on an endpoint or notification object
*
* Block on a notification or endpoint waiting for a message. No reply object is
* required for a Wait. Wait should not be paired with Call, as it does not provide
* a reply object. If Wait is paired with a Call the waiter will block after receiving
* the message.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_Wait"/> in <autoref label="sec:sys_wait"/>.</docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Wait(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Non-Blocking Wait" label="sel4_nbwait"/> @endxmlonly
* @brief Perform a polling wait on an endpoint or notification object
*
* Poll a notification or endpoint waiting for a message. No reply object is
* required for a Wait. Wait should not be paired with Call.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_NBWait"/> in <autoref label="sec:sys_nbwait"/>.</docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_NBWait(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Poll" label="sel4_mcs_poll"/> @endxmlonly
* @brief Perform a non-blocking receive on a notification object
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_NBWait().
* It is useful for doing a non-blocking wait on a notification.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_NBWait"/> in <autoref label="sec:sys_nbwait"/>.</docref>
* @endxmlonly
*
* @param[in] src The capability to be invoked.
* @param[out] sender The address to write sender information to.
* The sender information is the badge of the
* endpoint capability that was invoked by the
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Poll(seL4_CPtr src, seL4_Word *sender);
/**
* @xmlonly <manual name="Signal" label="sel4_mcs_signal"/> @endxmlonly
* @brief Signal a notification
*
* This is not a proper system call known by the kernel. Rather, it is a
* convenience wrapper which calls seL4_Send().
* It is useful for signalling a notification.
*
* @xmlonly
* <docref>See the description of <nameref name="seL4_Send"/> in <autoref label="sec:sys_send"/>.</docref>
* @endxmlonly
*
* @param[in] dest The capability to be invoked.
*/
LIBSEL4_INLINE_FUNC void
seL4_Signal(seL4_CPtr dest);
/** @} */

View File

@ -0,0 +1,48 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <sel4/simple_types.h>
#include <sel4/macros.h>
#include <sel4/arch/types.h>
#include <sel4/sel4_arch/types.h>
#include <sel4/sel4_arch/types_gen.h>
#include <sel4/syscall.h>
#include <sel4/objecttype.h>
#include <sel4/sel4_arch/objecttype.h>
#include <sel4/arch/objecttype.h>
#include <sel4/errors.h>
#include <sel4/constants.h>
#include <sel4/shared_types_gen.h>
#include <sel4/shared_types.h>
#include <sel4/mode/types.h>
#ifdef CONFIG_RETYPE_FAN_OUT_LIMIT
# define seL4_UntypedRetypeMaxObjects CONFIG_RETYPE_FAN_OUT_LIMIT
#else
# define seL4_UntypedRetypeMaxObjects 256
#endif
typedef seL4_Word seL4_NodeId;
typedef seL4_Word seL4_PAddr;
typedef seL4_Word seL4_Domain;
typedef seL4_CPtr seL4_CNode;
typedef seL4_CPtr seL4_IRQHandler;
typedef seL4_CPtr seL4_IRQControl;
typedef seL4_CPtr seL4_TCB;
typedef seL4_CPtr seL4_Untyped;
typedef seL4_CPtr seL4_DomainSet;
typedef seL4_CPtr seL4_SchedContext;
typedef seL4_CPtr seL4_SchedControl;
typedef seL4_Uint64 seL4_Time;
#define seL4_NilData 0
#include <sel4/arch/constants.h>

View File

@ -0,0 +1,27 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#include <sel4/types.h>
#include <sel4/macros.h>
#include <sel4/invocation.h>
#include <sel4/constants.h>
#include <interfaces/sel4_client.h>
/*
* This file specifies virtual implementations of older invocations
* that can be aliased directly to new invocations.
*/
#ifdef CONFIG_KERNEL_MCS
LIBSEL4_INLINE seL4_Error seL4_SchedControl_Configure(seL4_SchedControl _service, seL4_SchedContext schedcontext,
seL4_Time budget, seL4_Time period, seL4_Word extra_refills, seL4_Word badge)
{
return seL4_SchedControl_ConfigureFlags(_service, schedcontext, budget, period, extra_refills, badge,
seL4_SchedContext_NoFlag);
}
#endif

View File

@ -0,0 +1,65 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
PHDRS
{
text PT_LOAD;
data PT_LOAD;
}
ENTRY(_start);
SECTIONS
{
. = 0x200000;
.text :
{
_text = .;
*(.text.start)
*(.text*)
*(.rodata)
_text_end = .;
} :text
. = ALIGN(0x1000);
/* For some reason the ABI puts init array
* into writable memory, so we have to follow suit */
.init_array :
{
PROVIDE(__init_array_start = .);
KEEP (*(SORT(.init_array.*)))
KEEP (*(.init_array*))
PROVIDE(__init_array_end = .);
} :data
.data :
{
_data = .;
*(.data)
. = ALIGN(8);
__global_pointer$ = . + 0x800;
*(.srodata)
*(.sdata)
_data_end = .;
} :data
.bss :
{
_bss = .;
*(.sbss)
*(.bss)
*(.bss*)
*(COMMON)
. = ALIGN(4);
_bss_end = .;
} :data
. = ALIGN(0x1000);
.ipc_buffer (NOLOAD): {
__sel4_ipc_buffer_obj = .;
}
}

View File

@ -0,0 +1,106 @@
<?xml version="1.0" ?>
<!--
Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
SPDX-License-Identifier: BSD-2-Clause
-->
<!-- Please see syscalls.xsd to see the format of this file -->
<syscalls>
<!-- official API syscalls -->
<api-master>
<config>
<syscall name="Call" />
<syscall name="ReplyRecv" />
<syscall name="Send" />
<syscall name="NBSend" />
<syscall name="Recv" />
<syscall name="Reply" />
<syscall name="Yield" />
<syscall name="NBRecv" />
</config>
</api-master>
<api-mcs>
<config>
<syscall name="Call" />
<syscall name="ReplyRecv" />
<syscall name="NBSendRecv" />
<syscall name="NBSendWait" />
<syscall name="Send" />
<syscall name="NBSend" />
<syscall name="Recv" />
<syscall name="NBRecv" />
<syscall name="Wait" />
<syscall name="NBWait" />
<syscall name="Yield" />
</config>
</api-mcs>
<!-- Syscalls on the unknown syscall path. These definitions will be wrapped in #if condition -->
<debug>
<config>
<condition><config var="CONFIG_PRINTING"/></condition>
<syscall name="DebugPutChar" />
<syscall name="DebugDumpScheduler" />
</config>
<config>
<condition><config var="CONFIG_DEBUG_BUILD"/></condition>
<syscall name="DebugHalt" />
<syscall name="DebugCapIdentify" />
<syscall name="DebugSnapshot" />
<syscall name="DebugNameThread"/>
</config>
<config>
<condition>
<and>
<config var="CONFIG_DEBUG_BUILD"/>
<config var="CONFIG_ENABLE_SMP_SUPPORT"/>
</and>
</condition>
<syscall name="DebugSendIPI"/>
</config>
<config>
<condition><config var="CONFIG_DANGEROUS_CODE_INJECTION"/></condition>
<syscall name="DebugRun"/>
</config>
<config>
<condition><config var="CONFIG_ENABLE_BENCHMARKS"/></condition>
<syscall name="BenchmarkFlushCaches" />
<syscall name="BenchmarkResetLog" />
<syscall name="BenchmarkFinalizeLog" />
<syscall name="BenchmarkSetLogBuffer" />
<syscall name="BenchmarkNullSyscall" />
</config>
<config>
<condition><config var="CONFIG_BENCHMARK_TRACK_UTILISATION"/></condition>
<syscall name="BenchmarkGetThreadUtilisation" />
<syscall name="BenchmarkResetThreadUtilisation" />
</config>
<config>
<condition>
<and>
<config var="CONFIG_DEBUG_BUILD"/>
<config var="CONFIG_BENCHMARK_TRACK_UTILISATION"/>
</and>
</condition>
<syscall name="BenchmarkDumpAllThreadsUtilisation" />
<syscall name="BenchmarkResetAllThreadsUtilisation" />
</config>
<config>
<condition><config var="CONFIG_KERNEL_X86_DANGEROUS_MSR"/></condition>
<syscall name="X86DangerousWRMSR"/>
<syscall name="X86DangerousRDMSR"/>
</config>
<!-- This is not a debug syscall, but it needs to not appear in the 'API' syscall list
so that the check of 'is this a valid syscall' can remain a simple range check.
Therefore we'll put this here and the arch code will handle it before
passing to handleUnknownSyscall -->
<config>
<condition><config var="CONFIG_VTX"/></condition>
<syscall name="VMEnter"/>
</config>
<config>
<condition><config var="CONFIG_SET_TLS_BASE_SELF"/></condition>
<syscall name="SetTLSBase"/>
</config>
</debug>
</syscalls>

View File

@ -0,0 +1,71 @@
<xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema">
<!--
Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
SPDX-License-Identifier: BSD-2-Clause
-->
<xsd:annotation>
<xsd:documentation xml:lang="en">
Syscall number generator schema.
</xsd:documentation>
</xsd:annotation>
<xsd:element name="syscalls" type="SyscallListType" />
<xsd:complexType name="SyscallListType">
<xsd:sequence>
<xsd:element name="api-master" type="ApiType" />
<xsd:element name="api-mcs" type="ApiType" />
<xsd:element name="debug" type="DebugType" />
</xsd:sequence>
</xsd:complexType>
<xsd:complexType name="ApiType">
<xsd:sequence>
<xsd:element name="config" minOccurs="1" maxOccurs="unbounded" type="ConfigType" />
</xsd:sequence>
</xsd:complexType>
<xsd:complexType name="DebugType">
<xsd:sequence>
<xsd:element name="config" type="ConfigType" maxOccurs="unbounded"/>
</xsd:sequence>
</xsd:complexType>
<xsd:complexType name="ConfigType" >
<xsd:sequence>
<xsd:element name="condition" minOccurs="0" maxOccurs="1" type="Unary"/>
<xsd:element name="syscall" minOccurs="1" maxOccurs="unbounded" type="SyscallType"/>
</xsd:sequence>
</xsd:complexType>
<xsd:group name="ConfigGroup">
<xsd:choice>
<xsd:element name="and" type="N-ary" />
<xsd:element name="or" type="N-ary" />
<xsd:element name="not" type="Unary" />
<xsd:element name="config">
<xsd:complexType>
<xsd:attribute name="var" type="xsd:string" use="required"/>
</xsd:complexType>
</xsd:element>
</xsd:choice>
</xsd:group>
<xsd:complexType name="Unary">
<xsd:group ref="ConfigGroup"/>
</xsd:complexType>
<xsd:complexType name="N-ary">
<xsd:sequence>
<xsd:group ref="ConfigGroup" minOccurs="2" maxOccurs="unbounded"/>
</xsd:sequence>
</xsd:complexType>
<xsd:complexType name="SyscallType">
<xsd:attribute name="name" type="xsd:string" />
</xsd:complexType>
</xsd:schema>

View File

@ -0,0 +1,5 @@
#pragma once
#include <kernel/gen_config.h>
#include <sel4/gen_config.h>

View File

@ -0,0 +1,236 @@
<?xml version="1.0" ?>
<!--
Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
SPDX-License-Identifier: BSD-2-Clause
-->
<api name="ObjectApiAarch64" label_prefix="aarch64_">
<struct name="seL4_UserContext">
<member name="pc"/>
<member name="sp"/>
<member name="spsr"/>
<member name="x0"/>
<member name="x1"/>
<member name="x2"/>
<member name="x3"/>
<member name="x4"/>
<member name="x5"/>
<member name="x6"/>
<member name="x7"/>
<member name="x8"/>
<member name="x16"/>
<member name="x17"/>
<member name="x18"/>
<member name="x29"/>
<member name="x30"/>
<member name="x9"/>
<member name="x10"/>
<member name="x11"/>
<member name="x12"/>
<member name="x13"/>
<member name="x14"/>
<member name="x15"/>
<member name="x19"/>
<member name="x20"/>
<member name="x21"/>
<member name="x22"/>
<member name="x23"/>
<member name="x24"/>
<member name="x25"/>
<member name="x26"/>
<member name="x27"/>
<member name="x28"/>
<member name="tpidr_el0"/>
<member name="tpidrro_el0"/>
</struct>
<struct name="seL4_ARM_SMCContext">
<member name="x0"/>
<member name="x1"/>
<member name="x2"/>
<member name="x3"/>
<member name="x4"/>
<member name="x5"/>
<member name="x6"/>
<member name="x7"/>
</struct>
<interface name="seL4_ARM_VSpace" manual_name="Page Global Directory"
cap_description="Capability to the top level translation table being operated on.">
<method id="ARMVSpaceClean_Data" name="Clean_Data" manual_label="vspace_clean"
manual_name="Clean Data">
<brief>
Clean cached pages within a top level translation table
</brief>
<description>
<docref>See <autoref label="ch:vspace"/>.</docref>
</description>
<param dir="in" name="start" type="seL4_Word"
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_FailedLookup">
<description>
The <texttt text="_service"/> 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.
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">
<brief>
Invalidate cached pages within a top level translation table
</brief>
<description>
<docref>See <autoref label="ch:vspace"/>.</docref>
</description>
<param dir="in" name="start" type="seL4_Word"
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_FailedLookup">
<description>
The <texttt text="_service"/> 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.
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">
<brief>
Clean and invalidate cached pages within a top level translation table
</brief>
<description>
<docref>See <autoref label="ch:vspace"/>.</docref>
</description>
<param dir="in" name="start" type="seL4_Word"
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_FailedLookup">
<description>
The <texttt text="_service"/> 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.
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">
<brief>
Clean and invalidate cached instruction pages to point of unification
</brief>
<description>
<docref>See <autoref label="ch:vspace"/>.</docref>
</description>
<param dir="in" name="start" type="seL4_Word"
description="Start address"/>
<param dir="in" name="end" type="seL4_Word"
description="End address"/>
<error name="seL4_FailedLookup">
<description>
The <texttt text="_service"/> 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.
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_SMC" manual_name="SMC" cap_description="Capability to allow threads to make Secure Monitor Calls.">
<method id="ARMSMCCall" name="Call" manual_name="SMC Call" manual_label="smc_call">
<brief>
Tell the kernel to make the real SMC call.
</brief>
<description>
Takes x0-x7 as arguments to an SMC call which are defined as a seL4_ARM_SMCContext
struct. The kernel makes the SMC call and then returns the results as a
new seL4_ARM_SMCContext.
</description>
<param dir="in" name="smc_args" type="seL4_ARM_SMCContext"
description="The structure that has the provided arguments."/>
<param dir="out" name="smc_response" type="seL4_ARM_SMCContext"
description="The structure to capture the responses."/>
</method>
</interface>
</api>

View File

@ -0,0 +1,135 @@
#pragma once
#define CONFIG_ARM_HIKEY_OUTSTANDING_PREFETCHERS 0
#define CONFIG_ARM_HIKEY_PREFETCHER_STRIDE 0
#define CONFIG_ARM_HIKEY_PREFETCHER_NPFSTRM 0
/* disabled: CONFIG_ARM_HIKEY_PREFETCHER_STBPFDIS */
/* disabled: CONFIG_ARM_HIKEY_PREFETCHER_STBPFRS */
/* disabled: CONFIG_PLAT_IMX7 */
/* disabled: CONFIG_ARCH_AARCH32 */
#define CONFIG_ARCH_AARCH64 1
/* disabled: CONFIG_ARCH_ARM_HYP */
/* disabled: CONFIG_ARCH_RISCV32 */
/* disabled: CONFIG_ARCH_RISCV64 */
/* disabled: CONFIG_ARCH_X86_64 */
/* disabled: CONFIG_ARCH_IA32 */
#define CONFIG_SEL4_ARCH aarch64
#define CONFIG_ARCH_ARM 1
#define CONFIG_ARCH arm
#define CONFIG_WORD_SIZE 64
#define CONFIG_ARM_PLAT imx8mm-evk
/* disabled: CONFIG_PLAT_BCM2711 */
/* disabled: CONFIG_PLAT_BCM2837 */
/* disabled: CONFIG_PLAT_FVP */
/* disabled: CONFIG_PLAT_HIKEY */
/* disabled: CONFIG_PLAT_IMX8MQ_EVK */
#define CONFIG_PLAT_IMX8MM_EVK 1
/* disabled: CONFIG_PLAT_IMX8MP_EVK */
/* disabled: CONFIG_PLAT_MAAXBOARD */
/* disabled: CONFIG_PLAT_ODROIDC2 */
/* disabled: CONFIG_PLAT_ODROIDC4 */
/* disabled: CONFIG_PLAT_QEMU_ARM_VIRT */
/* disabled: CONFIG_PLAT_QUARTZ64 */
/* disabled: CONFIG_PLAT_ROCKPRO64 */
/* disabled: CONFIG_PLAT_TQMA8XQP1GB */
/* disabled: CONFIG_PLAT_TX1 */
/* disabled: CONFIG_PLAT_TX2 */
/* disabled: CONFIG_PLAT_ZYNQMP */
#define CONFIG_PLAT imx8mm-evk
/* disabled: CONFIG_ARM_CORTEX_A7 */
/* disabled: CONFIG_ARM_CORTEX_A8 */
/* disabled: CONFIG_ARM_CORTEX_A9 */
/* disabled: CONFIG_ARM_CORTEX_A15 */
/* disabled: CONFIG_ARM_CORTEX_A35 */
#define CONFIG_ARM_CORTEX_A53 1
/* disabled: CONFIG_ARM_CORTEX_A55 */
/* disabled: CONFIG_ARM_CORTEX_A57 */
/* disabled: CONFIG_ARM_CORTEX_A72 */
/* disabled: CONFIG_ARCH_ARM_V7A */
/* disabled: CONFIG_ARCH_ARM_V7VE */
#define CONFIG_ARCH_ARM_V8A 1
/* disabled: CONFIG_AARCH64_SERROR_IGNORE */
#define CONFIG_ARM_MACH imx
#define CONFIG_KERNEL_MCS 1
#define CONFIG_ARM_PA_SIZE_BITS_40 1
/* disabled: CONFIG_ARM_PA_SIZE_BITS_44 */
#define CONFIG_ARM_ICACHE_VIPT 1
/* disabled: CONFIG_DEBUG_DISABLE_L2_CACHE */
/* disabled: CONFIG_DEBUG_DISABLE_L1_ICACHE */
/* disabled: CONFIG_DEBUG_DISABLE_L1_DCACHE */
/* disabled: CONFIG_DEBUG_DISABLE_BRANCH_PREDICTION */
#define CONFIG_ARM_HYPERVISOR_SUPPORT 1
#define CONFIG_ARM_GIC_V3_SUPPORT 1
/* disabled: CONFIG_AARCH64_VSPACE_S2_START_L1 */
/* disabled: CONFIG_ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE */
/* disabled: CONFIG_ARM_ERRATA_430973 */
/* disabled: CONFIG_ARM_ERRATA_773022 */
/* disabled: CONFIG_ARM_SMMU */
/* disabled: CONFIG_TK1_SMMU */
/* disabled: CONFIG_ENABLE_A9_PREFETCHER */
/* disabled: CONFIG_EXPORT_PMU_USER */
/* disabled: CONFIG_DISABLE_WFI_WFE_TRAPS */
/* disabled: CONFIG_SMMU_INTERRUPT_ENABLE */
/* disabled: CONFIG_AARCH32_FPU_ENABLE_CONTEXT_SWITCH */
#define CONFIG_AARCH64_USER_CACHE_ENABLE 1
/* disabled: CONFIG_ALLOW_SMC_CALLS */
#define CONFIG_L1_CACHE_LINE_SIZE_BITS 6
#define CONFIG_EXPORT_PCNT_USER 1
/* disabled: CONFIG_EXPORT_VCNT_USER */
/* disabled: CONFIG_EXPORT_PTMR_USER */
/* disabled: CONFIG_EXPORT_VTMR_USER */
/* disabled: CONFIG_VTIMER_UPDATE_VOFFSET */
#define CONFIG_HAVE_FPU 1
#define CONFIG_PADDR_USER_DEVICE_TOP 1099511627776
#define CONFIG_ROOT_CNODE_SIZE_BITS 12
#define CONFIG_BOOT_THREAD_TIME_SLICE 5
#define CONFIG_RETYPE_FAN_OUT_LIMIT 256
#define CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION 100
#define CONFIG_RESET_CHUNK_BITS 8
#define CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS 230
#define CONFIG_FASTPATH 1
/* disabled: CONFIG_EXCEPTION_FASTPATH */
#define CONFIG_NUM_DOMAINS 1
/* disabled: CONFIG_SIGNAL_FASTPATH */
#define CONFIG_NUM_PRIORITIES 256
#define CONFIG_MAX_NUM_NODES 1
/* disabled: CONFIG_ENABLE_SMP_SUPPORT */
#define CONFIG_KERNEL_STACK_BITS 12
#define CONFIG_FPU_MAX_RESTORES_SINCE_SWITCH 64
/* disabled: CONFIG_VERIFICATION_BUILD */
/* disabled: CONFIG_BINARY_VERIFICATION_BUILD */
#define CONFIG_DEBUG_BUILD 1
/* disabled: CONFIG_HARDWARE_DEBUG_API */
#define CONFIG_PRINTING 1
/* disabled: CONFIG_KERNEL_INVOCATION_REPORT_ERROR_IPC */
#define CONFIG_NO_BENCHMARKS 1
/* disabled: CONFIG_BENCHMARK_GENERIC */
/* disabled: CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES */
/* disabled: CONFIG_BENCHMARK_TRACEPOINTS */
/* disabled: CONFIG_BENCHMARK_TRACK_UTILISATION */
#define CONFIG_KERNEL_BENCHMARK none
/* disabled: CONFIG_ENABLE_BENCHMARKS */
/* disabled: CONFIG_KERNEL_LOG_BUFFER */
#define CONFIG_MAX_NUM_TRACE_POINTS 0
#define CONFIG_IRQ_REPORTING 1
#define CONFIG_COLOUR_PRINTING 1
#define CONFIG_USER_STACK_TRACE_LENGTH 16
#define CONFIG_KERNEL_OPT_LEVEL_O2 1
/* disabled: CONFIG_KERNEL_OPT_LEVEL_OS */
/* disabled: CONFIG_KERNEL_OPT_LEVEL_O0 */
/* disabled: CONFIG_KERNEL_OPT_LEVEL_O1 */
/* disabled: CONFIG_KERNEL_OPT_LEVEL_O3 */
#define CONFIG_KERNEL_OPT_LEVEL -O2
#define CONFIG_KERNEL_OPTIMISATION_CLONE_FUNCTIONS 1
/* disabled: CONFIG_KERNEL_FWHOLE_PROGRAM */
/* disabled: CONFIG_DANGEROUS_CODE_INJECTION */
/* disabled: CONFIG_DEBUG_DISABLE_PREFETCHERS */
/* disabled: CONFIG_SET_TLS_BASE_SELF */
#define CONFIG_KERNEL_WCET_SCALE 1
#define CONFIG_KERNEL_STATIC_MAX_PERIOD_US 0
/* disabled: CONFIG_CLZ_32 */
/* disabled: CONFIG_CLZ_64 */
/* disabled: CONFIG_CTZ_32 */
/* disabled: CONFIG_CTZ_64 */
/* disabled: CONFIG_CLZ_NO_BUILTIN */
/* disabled: CONFIG_CTZ_NO_BUILTIN */

View File

@ -0,0 +1,135 @@
{
"ARM_HIKEY_OUTSTANDING_PREFETCHERS": "0",
"ARM_HIKEY_PREFETCHER_STRIDE": "0",
"ARM_HIKEY_PREFETCHER_NPFSTRM": "0",
"ARM_HIKEY_PREFETCHER_STBPFDIS": false,
"ARM_HIKEY_PREFETCHER_STBPFRS": false,
"PLAT_IMX7": false,
"ARCH_AARCH32": false,
"ARCH_AARCH64": true,
"ARCH_ARM_HYP": false,
"ARCH_RISCV32": false,
"ARCH_RISCV64": false,
"ARCH_X86_64": false,
"ARCH_IA32": false,
"SEL4_ARCH": "aarch64",
"ARCH_ARM": true,
"ARCH": "arm",
"WORD_SIZE": "64",
"ARM_PLAT": "imx8mm-evk",
"PLAT_BCM2711": false,
"PLAT_BCM2837": false,
"PLAT_FVP": false,
"PLAT_HIKEY": false,
"PLAT_IMX8MQ_EVK": false,
"PLAT_IMX8MM_EVK": true,
"PLAT_IMX8MP_EVK": false,
"PLAT_MAAXBOARD": false,
"PLAT_ODROIDC2": false,
"PLAT_ODROIDC4": false,
"PLAT_QEMU_ARM_VIRT": false,
"PLAT_QUARTZ64": false,
"PLAT_ROCKPRO64": false,
"PLAT_TQMA8XQP1GB": false,
"PLAT_TX1": false,
"PLAT_TX2": false,
"PLAT_ZYNQMP": false,
"PLAT": "imx8mm-evk",
"ARM_CORTEX_A7": false,
"ARM_CORTEX_A8": false,
"ARM_CORTEX_A9": false,
"ARM_CORTEX_A15": false,
"ARM_CORTEX_A35": false,
"ARM_CORTEX_A53": true,
"ARM_CORTEX_A55": false,
"ARM_CORTEX_A57": false,
"ARM_CORTEX_A72": false,
"ARCH_ARM_V7A": false,
"ARCH_ARM_V7VE": false,
"ARCH_ARM_V8A": true,
"AARCH64_SERROR_IGNORE": false,
"ARM_MACH": "imx",
"KERNEL_MCS": true,
"ARM_PA_SIZE_BITS_40": true,
"ARM_PA_SIZE_BITS_44": false,
"ARM_ICACHE_VIPT": true,
"DEBUG_DISABLE_L2_CACHE": false,
"DEBUG_DISABLE_L1_ICACHE": false,
"DEBUG_DISABLE_L1_DCACHE": false,
"DEBUG_DISABLE_BRANCH_PREDICTION": false,
"ARM_HYPERVISOR_SUPPORT": true,
"ARM_GIC_V3_SUPPORT": true,
"AARCH64_VSPACE_S2_START_L1": false,
"ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE": false,
"ARM_ERRATA_430973": false,
"ARM_ERRATA_773022": false,
"ARM_SMMU": false,
"TK1_SMMU": false,
"ENABLE_A9_PREFETCHER": false,
"EXPORT_PMU_USER": false,
"DISABLE_WFI_WFE_TRAPS": false,
"SMMU_INTERRUPT_ENABLE": false,
"AARCH32_FPU_ENABLE_CONTEXT_SWITCH": false,
"AARCH64_USER_CACHE_ENABLE": true,
"ALLOW_SMC_CALLS": false,
"L1_CACHE_LINE_SIZE_BITS": "6",
"EXPORT_PCNT_USER": true,
"EXPORT_VCNT_USER": false,
"EXPORT_PTMR_USER": false,
"EXPORT_VTMR_USER": false,
"VTIMER_UPDATE_VOFFSET": false,
"HAVE_FPU": true,
"PADDR_USER_DEVICE_TOP": "1099511627776",
"ROOT_CNODE_SIZE_BITS": "12",
"BOOT_THREAD_TIME_SLICE": "5",
"RETYPE_FAN_OUT_LIMIT": "256",
"MAX_NUM_WORK_UNITS_PER_PREEMPTION": "100",
"RESET_CHUNK_BITS": "8",
"MAX_NUM_BOOTINFO_UNTYPED_CAPS": "230",
"FASTPATH": true,
"EXCEPTION_FASTPATH": false,
"NUM_DOMAINS": "1",
"SIGNAL_FASTPATH": false,
"NUM_PRIORITIES": "256",
"MAX_NUM_NODES": "1",
"ENABLE_SMP_SUPPORT": false,
"KERNEL_STACK_BITS": "12",
"FPU_MAX_RESTORES_SINCE_SWITCH": "64",
"VERIFICATION_BUILD": false,
"BINARY_VERIFICATION_BUILD": false,
"DEBUG_BUILD": true,
"HARDWARE_DEBUG_API": false,
"PRINTING": true,
"KERNEL_INVOCATION_REPORT_ERROR_IPC": false,
"NO_BENCHMARKS": true,
"BENCHMARK_GENERIC": false,
"BENCHMARK_TRACK_KERNEL_ENTRIES": false,
"BENCHMARK_TRACEPOINTS": false,
"BENCHMARK_TRACK_UTILISATION": false,
"KERNEL_BENCHMARK": "none",
"ENABLE_BENCHMARKS": false,
"KERNEL_LOG_BUFFER": false,
"MAX_NUM_TRACE_POINTS": "0",
"IRQ_REPORTING": true,
"COLOUR_PRINTING": true,
"USER_STACK_TRACE_LENGTH": "16",
"KERNEL_OPT_LEVEL_O2": true,
"KERNEL_OPT_LEVEL_OS": false,
"KERNEL_OPT_LEVEL_O0": false,
"KERNEL_OPT_LEVEL_O1": false,
"KERNEL_OPT_LEVEL_O3": false,
"KERNEL_OPT_LEVEL": "-O2",
"KERNEL_OPTIMISATION_CLONE_FUNCTIONS": true,
"KERNEL_FWHOLE_PROGRAM": false,
"DANGEROUS_CODE_INJECTION": false,
"DEBUG_DISABLE_PREFETCHERS": false,
"SET_TLS_BASE_SELF": false,
"KERNEL_WCET_SCALE": "1",
"KERNEL_STATIC_MAX_PERIOD_US": "0",
"CLZ_32": false,
"CLZ_64": false,
"CTZ_32": false,
"CTZ_64": false,
"CLZ_NO_BUILTIN": false,
"CTZ_NO_BUILTIN": false
}

View File

@ -0,0 +1,221 @@
/*
* Copyright 2021, Breakaway Consulting Pty. Ltd.
*
* SPDX-License-Identifier: BSD-2-Clause
*/
/* Microkit interface */
#pragma once
#define __thread
#include <sel4/sel4.h>
typedef unsigned int microkit_channel;
typedef unsigned int microkit_child;
typedef seL4_MessageInfo_t microkit_msginfo;
#define MONITOR_EP 5
/* Only valid in the 'benchmark' configuration */
#define TCB_CAP 6
#define BASE_OUTPUT_NOTIFICATION_CAP 10
#define BASE_ENDPOINT_CAP 74
#define BASE_IRQ_CAP 138
#define BASE_TCB_CAP 202
#define BASE_VM_TCB_CAP 266
#define BASE_VCPU_CAP 330
#define MICROKIT_MAX_CHANNELS 62
/* User provided functions */
void init(void);
void notified(microkit_channel ch);
microkit_msginfo protected(microkit_channel ch, microkit_msginfo msginfo);
seL4_Bool fault(microkit_child child, microkit_msginfo msginfo, microkit_msginfo *reply_msginfo);
extern char microkit_name[16];
/* These next three variables are so our PDs can combine a signal with the next Recv syscall */
extern seL4_Bool microkit_have_signal;
extern seL4_CPtr microkit_signal_cap;
extern seL4_MessageInfo_t microkit_signal_msg;
/*
* Output a single character on the debug console.
*/
void microkit_dbg_putc(int c);
/*
* Output a NUL terminated string to the debug console.
*/
void microkit_dbg_puts(const char *s);
static inline void microkit_internal_crash(seL4_Error err)
{
/*
* Currently crash be dereferencing NULL page
*
* Actually derference 'err' which means the crash reporting will have
* `err` as the fault address. A bit of a cute hack. Not a good long term
* solution but good for now.
*/
int *x = (int *)(seL4_Word) err;
*x = 0;
}
static inline void microkit_notify(microkit_channel ch)
{
seL4_Signal(BASE_OUTPUT_NOTIFICATION_CAP + ch);
}
static inline void microkit_irq_ack(microkit_channel ch)
{
seL4_IRQHandler_Ack(BASE_IRQ_CAP + ch);
}
static inline void microkit_pd_restart(microkit_child pd, seL4_Word entry_point)
{
seL4_Error err;
seL4_UserContext ctxt = {0};
ctxt.pc = entry_point;
err = seL4_TCB_WriteRegisters(
BASE_TCB_CAP + pd,
seL4_True,
0, /* No flags */
1, /* writing 1 register */
&ctxt
);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_pd_restart: error writing TCB registers\n");
microkit_internal_crash(err);
}
}
static inline void microkit_pd_stop(microkit_child pd)
{
seL4_Error err;
err = seL4_TCB_Suspend(BASE_TCB_CAP + pd);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_pd_stop: error writing TCB registers\n");
microkit_internal_crash(err);
}
}
static inline microkit_msginfo microkit_ppcall(microkit_channel ch, microkit_msginfo msginfo)
{
return seL4_Call(BASE_ENDPOINT_CAP + ch, msginfo);
}
static inline microkit_msginfo microkit_msginfo_new(seL4_Word label, seL4_Uint16 count)
{
return seL4_MessageInfo_new(label, 0, 0, count);
}
static inline seL4_Word microkit_msginfo_get_label(microkit_msginfo msginfo)
{
return seL4_MessageInfo_get_label(msginfo);
}
static inline seL4_Word microkit_msginfo_get_count(microkit_msginfo msginfo)
{
return seL4_MessageInfo_get_length(msginfo);
}
static void microkit_mr_set(seL4_Uint8 mr, seL4_Word value)
{
seL4_SetMR(mr, value);
}
static seL4_Word microkit_mr_get(seL4_Uint8 mr)
{
return seL4_GetMR(mr);
}
/* The following APIs are only available where the kernel is built as a hypervisor. */
#if defined(CONFIG_ARM_HYPERVISOR_SUPPORT)
static inline void microkit_vcpu_restart(microkit_child vcpu, seL4_Word entry_point)
{
seL4_Error err;
seL4_UserContext ctxt = {0};
ctxt.pc = entry_point;
err = seL4_TCB_WriteRegisters(
BASE_VM_TCB_CAP + vcpu,
seL4_True,
0, /* No flags */
1, /* writing 1 register */
&ctxt
);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_vm_restart: error writing registers\n");
microkit_internal_crash(err);
}
}
static inline void microkit_vcpu_stop(microkit_child vcpu)
{
seL4_Error err;
err = seL4_TCB_Suspend(BASE_VM_TCB_CAP + vcpu);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_vm_stop: error suspending TCB\n");
microkit_internal_crash(err);
}
}
static inline void microkit_vcpu_arm_inject_irq(microkit_child vcpu, seL4_Uint16 irq, seL4_Uint8 priority,
seL4_Uint8 group, seL4_Uint8 index)
{
seL4_Error err;
err = seL4_ARM_VCPU_InjectIRQ(BASE_VCPU_CAP + vcpu, irq, priority, group, index);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_arm_vcpu_inject_irq: error injecting IRQ\n");
microkit_internal_crash(err);
}
}
static inline void microkit_vcpu_arm_ack_vppi(microkit_child vcpu, seL4_Word irq)
{
seL4_Error err;
err = seL4_ARM_VCPU_AckVPPI(BASE_VCPU_CAP + vcpu, irq);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_arm_vcpu_ack_vppi: error acking VPPI\n");
microkit_internal_crash(err);
}
}
static inline seL4_Word microkit_vcpu_arm_read_reg(microkit_child vcpu, seL4_Word reg)
{
seL4_ARM_VCPU_ReadRegs_t ret;
ret = seL4_ARM_VCPU_ReadRegs(BASE_VCPU_CAP + vcpu, reg);
if (ret.error != seL4_NoError) {
microkit_dbg_puts("microkit_arm_vcpu_read_reg: error reading vCPU register\n");
microkit_internal_crash(ret.error);
}
return ret.value;
}
static inline void microkit_vcpu_arm_write_reg(microkit_child vcpu, seL4_Word reg, seL4_Word value)
{
seL4_Error err;
err = seL4_ARM_VCPU_WriteRegs(BASE_VCPU_CAP + vcpu, reg, value);
if (err != seL4_NoError) {
microkit_dbg_puts("microkit_arm_vcpu_write_reg: error writing vCPU register\n");
microkit_internal_crash(err);
}
}
#endif
static inline void microkit_deferred_notify(microkit_channel ch)
{
microkit_have_signal = seL4_True;
microkit_signal_msg = seL4_MessageInfo_new(0, 0, 0, 0);
microkit_signal_cap = (BASE_OUTPUT_NOTIFICATION_CAP + ch);
}
static inline void microkit_deferred_irq_ack(microkit_channel ch)
{
microkit_have_signal = seL4_True;
microkit_signal_msg = seL4_MessageInfo_new(IRQAckIRQ, 0, 0, 0);
microkit_signal_cap = (BASE_IRQ_CAP + ch);
}

View File

@ -0,0 +1,8 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A15)
#error CONFIG_ARM_CORTEX_A15 is not defined
#endif
/* Cortex-A15 Manual, Section 10.2.2 */
#define seL4_NumHWBreakpoints 10
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A35)
#error CONFIG_ARM_CORTEX_A35 is not defined
#endif
/* Cortex-A35 Manual, Table C7.1 */
#define seL4_NumHWBreakpoints 6
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A53)
#error CONFIG_ARM_CORTEX_A53 is not defined
#endif
/* Cortex-A53 Manual, Section 11.6.1 */
#define seL4_NumHWBreakpoints 10
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A55)
#error CONFIG_ARM_CORTEX_A55 is not defined
#endif
/* Cortex-A55 Manual */
#define seL4_NumHWBreakpoints 10
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

View File

@ -0,0 +1,28 @@
/*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: BSD-2-Clause
*/
#pragma once
#include <sel4/config.h>
#if !defined(CONFIG_ARM_CORTEX_A57)
#error CONFIG_ARM_CORTEX_A57 is not defined
#endif
/* Cortex-A57 Manual, Section 10.6.1 */
#define seL4_NumHWBreakpoints 10
#define seL4_NumExclusiveBreakpoints 6
#define seL4_NumExclusiveWatchpoints 4
#ifdef CONFIG_HARDWARE_DEBUG_API
#define seL4_FirstBreakpoint 0
#define seL4_FirstWatchpoint 6
#define seL4_NumDualFunctionMonitors 0
#define seL4_FirstDualFunctionMonitor (-1)
#endif /* CONFIG_HARDWARE_DEBUG_API */

Some files were not shown because too many files have changed in this diff Show More