This introduces two new constants to the vcpu reg enum, with the goal of
unifying reg range saves/restores and making explicit which registers
are affected.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
seL4_VCPUReg_CPACR was sometimes saved to an inactive current VCPU,
overwriting the previous value and erroneously enabling FPU access.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Compatibility with versions <3.10 is going away.
As it happens, we're not using any CMake features that have changed
between 3.7 and 3.16, so bump the lowest version to 3.16.
Also remove the minimum version statement from the platform config
files --- they're all very simple files that are version independent;
and the version is checked elsewhere anyway.
Also, Fix style issue
A commit to fix style to make the PR go through.
Signed-off-by: Peter Chubb <Peter.Chubb@unsw.edu.au>
Nowhere else in the documentation uses the phrase
"Must be a depth of 32"
which seems incorrect for 64-bit riscv.
Also, the index parameter had the same description as root, which
is incorrect.
Signed-off-by: julia <git.ts@trainwit.ch>
This configuration is not in CI (hence why it lead to
a build error in the first place) so I just tested
it locally via sel4test with:
```
../init-build.sh -DPLATFORM=qemu-riscv-virt \
-DMCS=1 -DKernelRiscvExtD=1 \
-DKernelRiscvExtF=1 -DRISCV32=1
```
and it passed.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
This commit's parent renames the interface XML files.
The symlinks added in this commit serve to ease the transition to the
new names for downstream projects.
These links are added:
- include/interfaces/{sel4.xml -> object-api.xml}
- arch_include/*/interfaces/{sel4arch.xml -> object-api-arch.xml}
- sel4_arch_include/*/interfaces/{
sel4arch.xml -> object-api-sel4-arch.xml
}
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Before, some object API XML files conflicted when the include,
arch_include, and sel4_arch_include directories were combined:
- include/interfaces/sel4.xml
- arch_include/*/interfaces/sel4arch.xml
- sel4_arch_include/*/interfaces/sel4arch.xml
This commit renames them to:
- include/interfaces/object-api.xml
- arch_include/*/interfaces/object-api-arch.xml
- sel4_arch_include/*/interfaces/object-api-sel4-arch.xml
Now, when the include, arch_include, and sel4_arch_include directories
are combined, we are left with:
- interfaces/object-api.xml
- interfaces/object-api-arch.xml
- interfaces/object-api-sel4-arch.xml
Signed-off-by: Nick Spinale <nick@nickspinale.com>
This new platform is NXP Semiconductor's Evaluation Kit for the i.MX 8M
Plus Applications Processor. It's from the i.MX 8M family of processors
and is largely similar to the existing i.MX 8M Quad and i.MX 8M Mini
platforms.
Signed-off-by: Damon Lee <damon@kry10.com>
Check for CONFIG_ENABLE_SMP_SUPPORT instead of checking for the
number in CONFIG_MAX_NUM_NODES. This allows enabling SMP support
with just one node also.
Signed-off-by: Axel Heider <axel.heider@codasip.com>
- fix: brackets in check
- fix: use CONFIG_ENABLE_SMP_SUPPORT
- conditions for CONFIG_MAX_NUM_NODES have been removed
Signed-off-by: Axel Heider <axel.heider@codasip.com>
Add a glossary with seL4-specific terms and their
definitions.
Remove chapter number from bibliography
Tweak Makefile for glossary
Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
This way common error codes can be in their own file.
To use, add the xmlns:xi="http://www.w3.org/2001/XInclude
attribute to the top level node and use:
<xi:include href="file-to-include.xml"/>
The content of the file will be included verbatim.
Include files must be complete XML documents, but without
<?xml version="1.0" ?> at the top. Practically this means
all nodes within the file need to be contained in one root
element.
Caveat: There is no proper dependency for Xincludes files in
the Makefile, so you need to do make clean after changing an
included XML file!
Signed-off-by: Indan Zupancic <indan@nul.nu>
Currently the seL4_VCPUReg enum only defines the seL4_VCPUReg_VMPIDR_EL2
register when the kernel is configured for SMP. This register should be
available for unicore systems too as otherwise a user level VMM is not
able to control the value of MPIDR_EL1 that the guest VM reads.
Signed-off-by: Kent McLeod <kent@kry10.com>
Disambiguate (for the reader) between normal and mcs versions of
SetSpace in the manual. This does not yet solve doxygen confusion.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Provide seL4_BootInfoFrameSize (and seL4_BootInfoFrameBits) for
userland, to there is no longer a need to hard-code the 4 KiByte
assumption.
Signed-off-by: Axel Heider <axelheider@gmx.de>
Additional header files may now be included in non-C contexts and so we
need to guard some C definitions with the __ASSEMBLER__ guards
convention.
Signed-off-by: Kent McLeod <kent@kry10.com>
Some slot positions in the rootnode would depend on configuration.
However that makes it difficult to add new root caps, especially if
multiple caps only exist based on configuration. Make all caps always
there, but null if not configured.
Signed-off-by: Robbie VanVossen <robert.vanvossen@dornerworks.com>
Now the vspace_cap is used for all vspace roots and all other page
tables are referred to by page table caps.
Signed-off-by: Kent McLeod <kent@kry10.com>
Guard the new implementation of 64-bit x86 guests behind a config
option. This is done so that existing projects that use x86_64 hosts
with ia32-bit guests can continue to be supported until either the old
feature is preferred to be deprecated, or support can be added to
support both simmultaneously.
Signed-off-by: Kent McLeod <kent@kry10.com>
This commit combines a number of smaller commits which do the following:
* Enter IA-32e mode when running a 64-bit host
* Handle additional general purpose registers in 64-bit mode
* Handle 64-bit specific MSR events
* Properly save and restore FS, GS, and Shadow GS registers
CCDC-GVSC DISTRIBUTION A. Approved for public release; distribution
unlimited. OPSEC#4481.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
__builtin_offsetof is not part of the verification C subset -- avoid
accidental use by not declaring a macro for it and filter out the
single use by explicitly marking it as invisible to verification.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add a `--form_file <file>` option to the bitfield generator for
printing a `/* generated from <file> */` message in a comment.
Use this option in cmake to provide the original source .bf file before
preprocessing so it's easier to find out where the corresponding
definitions are.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This header file is shared by kernel and userland. We can control the
kernel compiler setting, but userland might use an arbitrary setup.
Put a safeguard in place that things works as expected.
Signed-off-by: Axel Heider <axelheider@gmx.de>
The "excluding extra refills" was confusing. seL4_CoreSchedContextBytes
is the size of sched_context_t + minimum refills, excluding any extra
refills.
We'd write it that way, but sched_context_t is not in scope in this
file.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
