Only call the command on CMake files that may be the first file
evaluated from the project. Remove from all other files.
Signed-off-by: Kent McLeod <kent@kry10.com>
The AArch64 kernel now has verification support for SMC caps. Remove
dependency of KernelAllowSMCCalls on "NOT KernelVerificationBuild" and
set KernelAllowSMCCalls to ON by default for AArch64 verification
builds.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Previously, this would error with a (confusing) warning since #546 about
Variable 'KernelArch' is not set
sel4test/settings.cmake had some code which complained about an invalid
platform, but it only ran if the kernel was found correctly:
set(valid_platforms ${KernelPlatform_all_strings})
set_property(CACHE PLATFORM PROPERTY STRINGS ${valid_platforms})
if(NOT "${PLATFORM}" IN_LIST valid_platforms)
message(FATAL_ERROR "Invalid PLATFORM selected: \"${PLATFORM}\"
Valid platforms are: \"${valid_platforms}\"")
endif()
Because of the CMake cache, if a correct platform was set, *then* an
incorrect platform, you could see this error, as the KernelArch would be
retained between builds in the cache. (Note: because of the cache, the
error message within the kernel is not triggered if we go from a valid
to an invalid platform. However the sel4test/settings.cmake one is).
Previously:
- If no platform is specified:
sel4test/build$ ../init-build.sh
loading initial cache file sel4test/projects/sel4test/settings.cmake
-- Set platform details from PLATFORM=
-- KernelPlatform:
-- Found seL4: sel4test/kernel
CMake Error at sel4test/kernel/configs/seL4Config.cmake:185
Variable 'KernelArch' is not set.
Call Stack (most recent call first):
sel4test/kernel/FindseL4.cmake:21 (include)
settings.cmake:32 (sel4_configure_platform_settings)
- If an invalid platform is specified:
sel4test/build$ ../init-build.sh -DPLATFORM=Cheshire
loading initial cache file sel4test/projects/sel4test/settings.cmake
-- Set platform details from PLATFORM=Cheshire
-- KernelPlatform: Cheshire
-- Found seL4: sel4test/kernel
CMake Error at sel4test/kernel/configs/seL4Config.cmake:185
Variable 'KernelArch' is not set.
Call Stack (most recent call first):
sel4test/kernel/FindseL4.cmake:21 (include)
settings.cmake:32 (sel4_configure_platform_settings)
Now, it looks like:
- If no platform is specified:
sel4test/build$ ../init-build.sh
loading initial cache file sel4test/projects/sel4test/settings.cmake
-- Set platform details from PLATFORM=
-- KernelPlatform:
-- Found seL4: sel4test/kernel
CMake Error at sel4test/kernel/configs/seL4Config.cmake:180
Variable 'KernelPlatform' is not set - is PLATFORM '' correct? Valid
platforms are
'allwinnerA20;am335x;apq8064;ariane;bcm2711;bcm2837;cheshire;...'
Call Stack (most recent call first):
sel4test/kernel/FindseL4.cmake:21 (include)
settings.cmake:32 (sel4_configure_platform_settings)
- If an invalid platform is specified:
sel4test/build$ ../init-build.sh -DPLATFORM=Cheshire
loading initial cache file sel4test/projects/sel4test/settings.cmake
-- Set platform details from PLATFORM=Cheshire
-- KernelPlatform: Cheshire
-- Found seL4: sel4test/kernel
CMake Error at sel4test/kernel/configs/seL4Config.cmake:180
Variable 'KernelPlatform' is not set - is PLATFORM 'Cheshire'
correct? Valid platforms are 'allwinnerA20;am335x;apq8064;...'
Call Stack (most recent call first):
sel4test/kernel/FindseL4.cmake:21 (include)
settings.cmake:32 (sel4_configure_platform_settings)
- If a valid platform is specified:
sel4test/build$ ./init-build.sh -DPLATFORM=cheshire
loading initial cache file sel4test/projects/sel4test/settings.cmake
-- Set platform details from PLATFORM=cheshire
-- KernelPlatform: cheshire
-- Found seL4: sel4test/kernel
-- platform cheshire supports multiple architectures, none was given
-- defaulting to: riscv64
-- Found GCC with prefix riscv64-none-elf-
Signed-off-by: julia <git.ts@trainwit.ch>
This changes the default configuration values of the build options:
KernelRiscvExtF and KernelRiscvExtD from OFF to ON.
The options control whether the kernel will support user applications
that use either of the floating point extensions. When these options are
off, FPU instructions will cause an exception.
Arm and x86 default FPU architecture support to ON and so this change is
making the default option consistent across architectures.
Signed-off-by: Kent McLeod <kent@kry10.com>
With recent proof improvements the proofs now apply to further platforms
in the ARM and AARCH64 configurations.
Refactor the verified configs to build on one include file per major
architecture which is then used for each platform with potentially
modified settings. Add path argument to `cmake_script_build_kernel`
macro to accommodate inclusion from different locations in the file
system.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Use `ARM_HYP_verified.cmake` from branch exynos5-ver as
`ARM_HYP_exynos5_verified.cmake` on master, so both can be used by
verification CI without switching branches.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Use `ARM_verified.cmake` from branch imx8-fpu-ver as
`ARM_imx8mm_verified.cmake` on master, so both can be used by
verification CI without switching branches.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Turn FPU off by default for the verification builds we have so far.
Only the imx8mm branch currently supports FPU for AArch32.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
The verified configs have a typo in the name of the
KernelMaxNumBootinfoUntypedCaps setting, which is then ignored by the
build system and the default is used if not otherwise set.
Remove the instances that have been ignored so far and replace with
the default value if they are not otherwise set. This means there is
no actual config change.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
For verified configurations on which we perform binary verification,
ensure that we disable certain whole-program optimisations that are
incompatible with binary verification.
Signed-off-by: Matthew Brecknell <matt@kry10.com>
The TX2 is currently the only platform that supports CONFIG_ARM_SMMU and
wants it on by default, however the CMake scripts wouldn't allow it to
be disabled. Now it should work normally:
- When TX2 is set the config is enabled unless it's preconfigured to
OFF.
- When the platform is changed to not TX2, the SMMU option is turned
off.
Signed-off-by: Kent McLeod <kent@kry10.com>
For ARM currently TIMER_PRECISION exists, but that is in microseconds
and not fine-grained enough.
This is needed to make periodic tasks synchronous with the system clock.
If this value is zero every period will be extended with the overhead of
taking an interrupt and reading the system clock. To avoid this drift,
the configured value should be set to at least the average overhead.
See also issue #844.
Signed-off-by: Indan Zupancic <Indan.Zupancic@mep-info.com>
For ongoing verification of seL4 on AArch64. This config has SMMU and
hypervisor support enabled. AArch64 also implies FPU support is on.
The target board for now is the TX2, which has an SMMU.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Remove all support for ARMv6 architectures now that all platforms and
CPUs that use this architecture have been removed.
Signed-off-by: Kent McLeod <kent@kry10.com>
Verify that KernelArch and KernelWordSize have been correctly
set after including the platform cmake files.
Signed-off-by: Ben Leslie <benno@brkawy.com>
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>
This adds basic support for the ARM Cortex A55 cpu core as is used in
the Amlogic S905x3 that is found in the ODroid C4.
Signed-off-by: Curtis Millar <curtis@curtism.me>
KernelAArch64SErrorIgnore needs to be saved into the cache in
seL4Config.cmake if it is set by any platform's config.cmake.
Signed-off-by: Kent McLeod <kent@kry10.com>
Don't create CONFIG_ARCH_AARCH32 on every platform and architecture.
Remove KernelSel4ArmHypAarch32.
Signed-off-by: Axel Heider <axel.heider@hensoldt-cyber.de>
As this variable bounds both the period and the budget and the period
itself bounds the budget, the name for this variable would be more
appropriately named 'MAX_PERIOD'
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
the function is not always passed the TIMER_PRECISION argument. If it is
not, we should not set the global varaible.
Signed-off-by: Curtis Millar <curtis.millar@data61.csiro.au>
For RISC-V platforms that do not provide machine instructions to count
leading and trailing zeros, this commit includes more efficient library
functions. For verification, we expose the bodies of the functions to
the proofs.
Kernel config options `CLZ_BUILTIN` and `CTZ_BUILTIN` allow selection of
whether compiler builtin functions should be used. These are only
supported on platforms where the builtin compiles to inline assembly. By
default, the options are on for all platforms except RISC-V.
Signed-off-by: Matthew Brecknell <Matthew.Brecknell@data61.csiro.au>
The A35 core is available on some recent ARMv8 SOCs (such as the
NXP i.MX8X family).
This change enables building for the A35, however no platforms
currently target the A35. It is an enabler for future platform
support additions.
Signed-off-by: Ben Leslie <benno@brkawy.com>
Remove unused cases and add break in switch statements.
Add conditions to sel4arch.xml.
Change guard in capdl printing to correct TK1_SMMU.
Set KernelArmSMMU default to off.
Add types to aarch32 syscall_stub_gen.py.
Signed-off-by: Oliver Scott <Oliver.Scott@data61.csiro.au>
