Previously, CMake defaults to adding various flags to the compile
options, such as `-O3`, `-DNDEBUG`, and `-g`. Here is an excerpt from
CMakeCache.txt:
//Flags used by the C compiler during RELEASE builds.
CMAKE_C_FLAGS_RELEASE:STRING=-O3 -DNDEBUG
//Flags used by the C compiler during RELWITHDEBINFO builds.
CMAKE_C_FLAGS_RELWITHDEBINFO:STRING=-O2 -g -DNDEBUG
We instead change the CMAKE_BUILD_TYPE to 'None' so that CMake
doesn't try to be clever and append extra compile flags. Anything
that depends on seL4 will be unaffected as CMake variables are scoped.
This should have no meaningful change to the kernel's generated code,
as the compile flags were being overridden anyway.
Relevant parts of the build.ninja file for comparison:
- Now, `-DRELEASE=ON`:
FLAGS = -march=armv8-a -D__KERNEL_64__ -std=c99 -Wall -Werror
-Wstrict-prototypes -Wmissing-prototypes -Wnested-externs
-Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull
-nostdinc -ffreestanding -fno-stack-protector
-fno-asynchronous-unwind-tables -fno-common -O2 -nostdlib
-fno-pic -fno-pie -mgeneral-regs-only -mno-outline-atomics
-E -CC -I/sel4test-manifest/build/kernel/generated_prune
- Before, `-DRELEASE=ON`:
FLAGS = -march=armv8-a -D__KERNEL_64__ -O3 -DNDEBUG -std=c99 -Wall
-Werror -Wstrict-prototypes -Wmissing-prototypes
-Wnested-externs -Wmissing-declarations -Wundef
-Wpointer-arith -Wno-nonnull -nostdinc -ffreestanding
-fno-stack-protector -fno-asynchronous-unwind-tables
-fno-common -O2 -nostdlib -fno-pic -fno-pie
-mgeneral-regs-only -mno-outline-atomics -E -CC
-I/sel4test-manifest/build/kernel/generated_prune
Note the lack of -O3 -DNDEBUG options.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
This was done way back in 2017: 0abc72027, but somehow
was missed from CMakeLists.txt and hyp_traps.S files.
Signed-off-by: Julia Vassiliki <julia.vassiliki@unsw.edu.au>
The source layout for arm_hyp configurations uses a symlink to redirect
sel4_arch include paths back to aarch32 when KernelSel4Arch is set to
arm_hyp. This case wasn't being handled by the CMake install target for
installing libsel4 and kernel.elf when the project is used in a
standalone context. The consequence is that the ARM_HYP verified
configurations would fail to install even though they would build
correctly.
We directly address this issue by accounting for the arm_hyp special
case in the installation command where we manually resolve the symlink.
If new arm_hyp symlinks are added in the future, this fix should still
apply providing that the update to the CMake install target uses the
same resolved sel4arch path variable introduced by this change.
There is a longer-term plan to remove the arm_hyp KernelSel4Arch config
value which is expected to remove these sorts of issues.
Signed-off-by: Kent McLeod <kent@kry10.com>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Note for LLVM 20 a new compile error appears:
clang: error: argument unused during compilation: '-c'
[-Werror,-Wunused-command-line-argument]. You'd need
to add -Wno-unused-command-line-argument to the kernel
compile options to build successfully.
Thanks to Chang Liu for mentioning the fix.
Signed-off-by: Indan Zupancic <indan@nul.nu>
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>
These files cannot be installed under the same names as those in the
source tree because the two named sel4arch.xml conflict. These cannot be
renamed in the source tree because of other projects which expect them
under their current names.
Commit cf80db7ef0 enabled them to be installed them under
non-conflicting names, but those names (sel4.xml, sel4-arch.xml,
sel4-sel4arch.xml) are confusing and too close to the original names.
This commit changes the names they are installed under to be more clear
and descriptive (object-api.xml, object-api-arch.xml,
object-api-sel4-arch.xml).
Signed-off-by: Nick Spinale <nick@nickspinale.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>
gen_config.json provides a language-independent means of accessing the
kernel configuration. Before, gen_config.h was generated directly in
CMake. Now, gen_config.yaml is generated directly in CMake, and
gen_config.h and gen_config.json are derived from gen_config.yaml.
Signed-off-by: Nick Spinale <nick@nickspinale.com>
Some inter-procedural optimisations can produce cloned or partial
functions in the binary. Since binary verification is incompatible with
cloned and partial functions, we add a config option to disable these
optimisations.
This does not change any defaults, so to avoid cloned and partial
functions for a binary verification build, it is necessary to explicitly
configure this, e.g. using `-DKernelBinaryVerificationBuild=ON`.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
Changes compiler options and the linker script to group most small data
objects together in a new .small section, and point __global_pointer$ at
.small so that nearly all objects can be referenced via gp.
Signed-off-by: Stefan O'Rear <sorear@fastmail.com>
GNU binutils require specifying the Zicsr and Zifencei extensions
explicitly from version 2.38 onwards. Since both are needed for
building the kernel, we need to add a check for that.
We only check for the GCC version being >= 11.3, since that is the
first GCC version that ships with binutils 2.38 by default.
Check PR #776 for more information.
Signed-off-by: Florian Hofhammer <florian.hofhammer@fhofhammer.de>
When running a python script from CMake, explicitly invoke Python via
the `PYTHON3` variable defined in the seL4 CMake config, rather than
relying on the script to specify its interpreter with `#!`.
This makes it easier to override the Python interpreter used for all
Python scripts called from CMake builds.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
python2 is not used in the kernel build anymore so the tool
definition is unnecessary.
python2 is also end-of-line so there is no reason to think
we would ever depend on it again.
Signed-off-by: Ben Leslie <benno@brkawy.com>
When using CMake to only build the kernel, an install target is now
provided to copy important outputs into an installation directory.
Currently only the following files are installed:
- ./bin/kernel.elf: Location of kernel.elf binary
- ./libsel4/include: The include root for libsel4
- ./libsel4/src: The c source files for the libsel4 library
To build and install this project to an installation directory should
now only require the following from a clean build directory:
```
export CMAKE_GENERATOR=Ninja
cmake -DCMAKE_INSTALL_PREFIX=<path-to-install> -DOption=Val <src-dir>;
cmake --build .;
cmake --install .;
```
Signed-off-by: Kent McLeod <kent@kry10.com>
The option -mno-outline-atomics used to be default before gcc-10 and
now needs to be provided explicitly. Without it gcc will produce
references to `__aarch64_ldadd8_acq_rel` which it expects to exist
in libgcc which we are not linking against.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
seL4Config.cmake is responsible for generating a valid
CMAKE_TOOLCHAIN_FILE and setting up platform config options at the start
of the build. The CMAKE_TOOLCHAIN_FILE variable has to be set before the
first cmake `project()` function is processed to take effect.
Previously this file was required to be imported in a CMake script
before the kernel's CMakeLists.txt could be processed. This prevented
the main CMakeLists.txt file from being used without an additional
configuration file:
cmake -G Ninja -C ../configs/ARM_verified.cmake ../
Now it is possible to do:
cmake -G Ninja -DKernelPlatform=imx6 -DKernelARMPlatform=sabre ../
This should make it easier to invoke CMake for building kernel
configurations from other build environments.
Because this file is now imported in the Kernel's CMakeLists.txt
context, there is no longer a requirement to save all the intermediate
settings into the cache and then read them out again.
Signed-off-by: Kent McLeod <kent@kry10.com>
GCC < 10 and clang < 11 put uninitialized global variables into a
'COMMON' section unless '-fno-common' is specified. The linker will put
anything from 'COMMON' as the end of the '.bss' it nothing else is
specified in the linker script. Besides making the variable placement
look odd, this also tends to waste a page because we puts large aligned
block at the end. Eventually, GCC 10 and clang 11 made '-fno-common'
the default, see
- https://gcc.gnu.org/gcc-10/changes.html
- https://releases.llvm.org/11.0.0/tools/clang/docs/ReleaseNotes.html
Signed-off-by: Axel Heider <axelheider@gmx.de>
This causes the kernel to be relinked and downstream build steps run
when the linker script is modified. Roughly copied from the dependency
handling used by the elfloader's build system.
Signed-off-by: Stefan O'Rear <sorear@fastmail.com>
The F and D extensions are enabled for RV64 when KernelHaveFPU
is enabled. Note that we still use the lp64 abi: no floating-point
arguments will be passed in registers
Signed-off-by: Yanyan Shen <yanyan.shen@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).
Allow projects that use the kernel as a subproject to configure the
kernel in -C scripts.
CMake supports providing a script via -C upon first initialisation of a
build directory. This script is expected to populate the configuration
cache for the rest of the build to depend on. This is how standalone
kernel builds are currently configured. However in buildsystems that add
the kernel as a subproject, it was up to the application to modify
configuration properties before or after the kernel was imported. This
lead to circular dependencies where properties were changed by a module
later in the build, but this then invalidated properties that were set
based on the first property's original value. This lead to running CMake
multiple times in order for settings to reach a stable state.
We now assume that most shared system configuration occurs in initial -C
settings evaluation. seL4Config.cmake is a configuration module that the
kernel exports that allows a configuration script to set kernel platform
and architecture settings in a way that doesn't introduce circular
dependencies.
seL4Config can be imported into other configuration files. This should
make it easier for a full system configuration script to query and
configure kernel configuration values without introducing circular
dependencies on configuration properties.
The DTS compilation was arm platforms only. Moving it to the top level
config file, making it available to RISCV platforms. The generated files
are almost identical with minor differences. A new argument(--arch) is
added to the hardware_gen.py for the differences.
When kernel_all.i was being used as an input for kernel.elf, CMake would
add gcc -MD flags for generating an output dependency file. However GCC
doesn't run the preprocessor on .i files which have already been
preprocessed. This would lead to the expected dependency file not being
created. Ninja would cope by ignoring the missing file and printing an
error with debug flags. However, ccache was parsing the -MD flags and
the missing dependency file caused cache lookup failures resulting in
persistent cache misses on every compilation rerun.
Using kernel_all.c as the input, can mean that we preprocess the file
twice, however for regular builds we don't need to create a
kernel_all_pp.c, and when creating a kernel_all_pp.c for verification we
don't care about speed as much and so can run the preprocessor twice.
