At the moment, the seL4 microkit does not setup TLS variable
support. The workaround has been to `#define __thread` (blank)
before including `<sel4/sel4.h>` in `<microkit.h>`, which causes
issues if `<microkit.h>` is included *after* `<sel4/sel4.h>`,
often with obscure linker errors to `__emutls_**` symbols.
Instead we add a libsel4 config option that allows us to build
it with __thread copied out. We introduce an LIBSEL4_THREAD_LOCAL
macro in a similar way to the existing LIBSEL4_INLINE macro.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
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>
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>
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>
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>
These files should have been released under BSD-2-Clause in the first
place (as per parent LICENSE.md file).
Closes#245
Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
Introduced a new config flag to enable
userError format strings to be written to the IPC buffer.
Another config bool has been introduced to toggle
printing the error out and this can also be set at runtime.
Signed-off-by: Saer Debel <saer.debel@data61.csiro.au>
This commit also converts our own copyright headers to directly use
SPDX, but leaves all other copyright header intact, only adding the
SPDX ident. As far as possible this commit also merges multiple
Data61 copyright statements/headers into one for consistency.
Update all scripts and build system to call python3, given python2's
upcoming doom. Use sys.maxsize instead of sys.maxint in one script
(maxint does not exist in python3).
Our upcoming cmake styling tool requires any custom functions you want
styled nicely to be lower case. We only need to style these two nicely,
as they have kwargs we would like aligned.
Now these bitfield definitions are generated from the same source file
in the kernel and libsel4, and also result in the same include path: <sel4/shared_types_gen.h>
add_config_library for sel4 adds sel4_Gen custom target. Having two targets with
names that only differ in case results in strange build problems on systems with
case insensitive file systems (I've seen it only on OS X but I assume Win is
affected too).
CPPFile is a much more robust version of GenCPP command. We drop the `extra_cflags`
as the CPPFile command uses regular cmake compilation and will use the include
directories added by `include_directories`, which includes all the directories from
`extra_cflags`
include_directories makes these directories directly available to all compilation that
happens, without needing to provide additional target link directories. This is the
first step to removing the `extra_cflags` variable
Placing lists directly in the generater expression means that this string, despite having
semicolons in it, is not actually a list, as it has an expression (the generator expression)
spanning multiple lists. This leads to confusion during argument processing and expansion
The definitions of guard and badge sizes is going to be changed for 64-bit platforms,
this change provides an easy way of providing different definitions
Using the bitfield generator to treat guards and badges as a union type can be convenient,
but it requires reserving a bit in the data for the bitfield run time type information.
This type information is not needed by the kernel as it knows implicitly whether the passed
data is a badge or a guard based on the kind of cap being operated on. However, with the
type information present we cannot pass a word sized piece of data to the kernel.
The solution here is to go back to using a plain seL4_Word as the type for invocations
that want a capdata and let the user either construct a badge as a plain word, or use
the seL4_CNode_CapData bitfield for constructing a guard, although they have to manually extract
the word representation out of it.
