This is useful for all x86 IOMMU work, which otherwise has
to duplicate the definitions of VTD_PT_INDEX_BITS in userspace
code. Follow the same pattern as many other existing code in
the libsel4 headers where the kernel depends on it.
Note we can't define seL4_IOPageTableBits in terms of Index + Entry
because the capDL tool does the c-preprocessor to make a YAML file
containing the constant, and it won't do evaluation.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
This value was inconsistent across platforms, and one
should use seL4_UserVSpaceTop instead.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
This is a consistent, inclusive-top value that is conveying
similar information to that of seL4_UserTop. We are adding
this so as to not break existing userspace, but it will make
it easier for userspace to deal with other platforms.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
Currently causes compile errors. It should match seL4_DebugCapIdentify,
except return affinity instead of cap type.
Signed-off-by: Indan Zupancic <indan@nul.nu>
This is useful for sel4test et al for testing that a certain
PD has been succesfully migrated between cores, or that it
is running on a particular core.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
The IPC queue changes for MCS in commit 771c9e43ce has decreased the
TCB size slightly, which brings TCB_SIZE_BITS down for config
combinations that have MCS + SMP + HYP + benchmarking enabled.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
In the definition of tcb_t, there's extra fields if there's
SMP or BENCHMARK_TRACK_UTILISATION or ARM_HYPERIVSOR_SUPPORT.
It looks like the combination of all three (which Microkit uses)
is not enough for 11 bits.
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
This was missed in cb8ee83f0cd2268b1d6b1cd5ca30b031db5896c4; their
use was removed from syscall_stub_gen but their typedefs remained.
Signed-off-by: julia <git.ts@trainwit.ch>
Save and restore the CNTKCTL register alongside other virtual timer
registers when switching VCPUs.
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
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>
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>
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>
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>
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>
Currently, building `libsel4` as a static library with `KernelIsMCS`
enabled fails with the following error:
```
static declaration of 'seL4_NBWait' follows non-static declaration
```
This [was mentioned][1] in the original PR that modified exported
functions to use `LIBSEL4_INLINE_FUNC`.
[1]: https://github.com/seL4/seL4/pull/101#issuecomment-442010551
Signed-off-by: Klim Tsoutsman <klim@tsoutsman.com>
Add a comment that they are empty on purpose. They are not removed to
keep the infrastructure in case there will be deprecated items in the
future.
Signed-off-by: Axel Heider <axelheider@gmx.de>
The MCS-related macros were causing the build to fail when configured to
use the sysenter instruction. Additionally, some message registers
weren't explicitly being passed to the assembly block for
seL4_NBSendRecv in this configuration.
Signed-off-by: Jimmy Brush <code@jimmah.com>
Now that there is no need to reserve page table entries in each VSpace
object, the full architecture specified address space range is usable.
Signed-off-by: Kent McLeod <kent@kry10.com>
Commit 8035f1a7c4 removed "-fno-integrated-as" for llvm, which on more
recent versions (clang-11) means that we now need `#` instead of `$`
for immediate values.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- KernelGlobalsFrame caused the definition of seL4_GlobalsFrame which
was a reservation at the top of the user address space on ARMv6
platforms.
- KernelDangerousCodeInjectionOnUndefInstr was used to implement calling
user code in kernel mode won ARMv6.
Signed-off-by: Kent McLeod <kent@kry10.com>
