portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

configs: additional verified platforms

Browse source 
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>
This commit is contained in:
Gerwin Klein 2024-09-28 09:20:54 +02:00
parent 03ad568c89
commit c5b23791ea
27 changed files with 221 additions and 191 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
configs/AARCH64_bcm2711_verified.cmake
View file

@ -1,26 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2022, Proofcraft Pty Ltd
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
cmake_script_build_kernel()
include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
set(KernelPlatform "bcm2711" CACHE STRING "")
set(KernelSel4Arch "aarch64" CACHE STRING "")
set(KernelArmHypervisorSupport ON CACHE BOOL "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
set(KernelArmSMMU OFF CACHE BOOL "")

10
configs/AARCH64_hikey_verified.cmake Executable file
View file

@ -0,0 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
set(KernelPlatform "hikey" CACHE STRING "")

10
configs/AARCH64_odroidc2_verified.cmake Executable file
View file

@ -0,0 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
set(KernelPlatform "odroidc2" CACHE STRING "")

10
configs/AARCH64_odroidc4_verified.cmake Executable file
View file

@ -0,0 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
set(KernelPlatform "odroidc4" CACHE STRING "")

23
configs/AARCH64_verified.cmake
View file

@ -1,29 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2022, Proofcraft Pty Ltd
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
# This is a preliminary configuration to be used for developing functional
# correctness proofs for the AArch64 architecture.
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
cmake_script_build_kernel()
include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
set(KernelPlatform "tx2" CACHE STRING "")
set(KernelSel4Arch "aarch64" CACHE STRING "")
set(KernelArmHypervisorSupport ON CACHE BOOL "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
set(KernelArmSMMU OFF CACHE BOOL "")

20
configs/AARCH64_zynqmp_verified.cmake
View file

@ -1,26 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2022, Proofcraft Pty Ltd
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
cmake_script_build_kernel()
include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
set(KernelPlatform "zynqmp" CACHE STRING "")
set(KernelSel4Arch "aarch64" CACHE STRING "")
set(KernelArmHypervisorSupport ON CACHE BOOL "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
set(KernelArmSMMU OFF CACHE BOOL "")

11
configs/ARM_HYP_exynos5410_verified.cmake Executable file
View file

@ -0,0 +1,11 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_HYP_verified_include.cmake)
set(KernelPlatform "exynos5" CACHE STRING "")
set(KernelARMPlatform "exynos5410" CACHE STRING "")

20
configs/ARM_HYP_exynos5_verified.cmake
View file

@ -1,27 +1,11 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
cmake_script_build_kernel()
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_HYP_verified_include.cmake)
set(KernelPlatform "exynos5" CACHE STRING "")
set(KernelARMPlatform "exynos5422" CACHE STRING "")
set(KernelSel4Arch "arm_hyp" CACHE STRING "")
set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")
set(KernelRootCNodeSizeBits 19 CACHE STRING "")
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")

20
configs/ARM_HYP_verified.cmake
View file

@ -1,26 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
cmake_script_build_kernel()
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_HYP_verified_include.cmake)
set(KernelPlatform "tk1" CACHE STRING "")
set(KernelSel4Arch "arm_hyp" CACHE STRING "")
set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")
set(KernelRootCNodeSizeBits 19 CACHE STRING "")
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")

20
configs/ARM_MCS_verified.cmake
View file

@ -1,28 +1,12 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
cmake_script_build_kernel()
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
set(KernelPlatform "imx6" CACHE STRING "")
set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelBinaryVerificationBuild ON CACHE BOOL "")
set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")
set(KernelMaxNumBootinfoUntypedCaps 230 CACHE STRING "")
set(KernelIsMCS ON CACHE BOOL "")
set(KernelStaticMaxPeriodUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "")

10
configs/ARM_exynos4_verified.cmake Executable file
View file

@ -0,0 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
set(KernelPlatform "exynos4" CACHE STRING "")

11
configs/ARM_exynos5410_verified.cmake Executable file
View file

@ -0,0 +1,11 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
set(KernelPlatform "exynos5" CACHE STRING "")
set(KernelARMPlatform "exynos5410" CACHE STRING "")

11
configs/ARM_exynos5422_verified.cmake Executable file
View file

@ -0,0 +1,11 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
set(KernelPlatform "exynos5" CACHE STRING "")
set(KernelARMPlatform "exynos5422" CACHE STRING "")

10
configs/ARM_hikey_verified.cmake Executable file
View file

@ -0,0 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
set(KernelPlatform "hikey" CACHE STRING "")

21
configs/ARM_imx8mm_verified.cmake
View file

@ -1,26 +1,11 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
cmake_script_build_kernel()
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
set(KernelPlatform "imx8mm-evk" CACHE STRING "")
set(KernelSel4Arch "aarch32" CACHE STRING "")
set(KernelAArch32FPUEnableContextSwitch ON CACHE BOOL "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelBinaryVerificationBuild ON CACHE BOOL "")
set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")
set(KernelAArch32FPUEnableContextSwitch ON CACHE BOOL "" FORCE)

10
configs/ARM_tk1_verified.cmake Executable file
View file

@ -0,0 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
set(KernelPlatform "tk1" CACHE STRING "")

19
configs/ARM_verified.cmake
View file

@ -1,25 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
cmake_script_build_kernel()
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
set(KernelPlatform "imx6" CACHE STRING "")
set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelBinaryVerificationBuild ON CACHE BOOL "")
set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")

10
configs/ARM_zynq7000_verified.cmake Executable file
View file

@ -0,0 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
set(KernelPlatform "zynq7000" CACHE STRING "")

10
configs/ARM_zynqmp_verified.cmake Executable file
View file

@ -0,0 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
set(KernelPlatform "zynqmp" CACHE STRING "")

21
configs/RISCV64_MCS_verified.cmake
View file

@ -5,27 +5,8 @@
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
cmake_script_build_kernel()
include(${CMAKE_CURRENT_LIST_DIR}/include/RISCV64_verified_include.cmake)
set(KernelSel4Arch "riscv64" CACHE STRING "")
set(KernelPlatform "hifive" CACHE STRING "")
set(KernelPTLevels "3" CACHE STRING "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelBinaryVerificationBuild ON CACHE BOOL "")
set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")
set(KernelRootCNodeSizeBits 19 CACHE STRING "")
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
set(KernelIsMCS ON CACHE BOOL "")
set(KernelStaticMaxPeriodUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "")
set(KernelClzNoBuiltin ON CACHE BOOL "")
set(KernelCtzNoBuiltin ON CACHE BOOL "")

23
configs/RISCV64_verified.cmake
View file

@ -1,29 +1,10 @@
#!/usr/bin/env -S cmake -P
#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
cmake_script_build_kernel()
include(${CMAKE_CURRENT_LIST_DIR}/include/RISCV64_verified_include.cmake)
set(KernelSel4Arch "riscv64" CACHE STRING "")
set(KernelPlatform "hifive" CACHE STRING "")
set(KernelPTLevels "3" CACHE STRING "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelBinaryVerificationBuild ON CACHE BOOL "")
set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")
set(KernelRootCNodeSizeBits 19 CACHE STRING "")
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
set(KernelClzNoBuiltin ON CACHE BOOL "")
set(KernelCtzNoBuiltin ON CACHE BOOL "")

4
configs/X64_verified.cmake
View file

@ -5,9 +5,9 @@
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
# If this file is executed it will build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
cmake_script_build_kernel()
cmake_script_build_kernel(..)
set(KernelPlatform "pc99" CACHE STRING "")
set(KernelSel4Arch "x86_64" CACHE STRING "")

24
configs/include/AARCH64_verified_include.cmake Normal file
View file

@ -0,0 +1,24 @@
#
# Copyright 2022, Proofcraft Pty Ltd
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed it will build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../../tools/helpers.cmake)
cmake_script_build_kernel(../..)
set(KernelSel4Arch "aarch64" CACHE STRING "")
set(KernelArmHypervisorSupport ON CACHE BOOL "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
set(KernelArmSMMU OFF CACHE BOOL "")

9
configs/include/ARM_HYP_verified_include.cmake Normal file
View file

@ -0,0 +1,9 @@
#
# Copyright 2024, Proofcraft Pty Ltd
#
# SPDX-License-Identifier: GPL-2.0-only
#
include(${CMAKE_CURRENT_LIST_DIR}/ARM_verified_include.cmake)
set(KernelSel4Arch "arm_hyp" CACHE STRING "" FORCE)

24
configs/include/ARM_verified_include.cmake Normal file
View file

@ -0,0 +1,24 @@
#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed it will build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../../tools/helpers.cmake)
cmake_script_build_kernel(../..)
set(KernelSel4Arch "aarch32" CACHE STRING "")
set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelBinaryVerificationBuild ON CACHE BOOL "")
set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")

27
configs/include/RISCV64_verified_include.cmake Normal file
View file

@ -0,0 +1,27 @@
#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: GPL-2.0-only
#
# If this file is executed it will build the kernel.elf and kernel_all_pp.c file
include(${CMAKE_CURRENT_LIST_DIR}/../../tools/helpers.cmake)
cmake_script_build_kernel(../..)
set(KernelSel4Arch "riscv64" CACHE STRING "")
set(KernelPTLevels "3" CACHE STRING "")
set(KernelVerificationBuild ON CACHE BOOL "")
set(KernelBinaryVerificationBuild ON CACHE BOOL "")
set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
set(KernelMaxNumNodes "1" CACHE STRING "")
set(KernelOptimisation "-O2" CACHE STRING "")
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
set(KernelBenchmarks "none" CACHE STRING "")
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
set(KernelFastpath ON CACHE BOOL "")
set(KernelPrinting OFF CACHE BOOL "")
set(KernelNumDomains 16 CACHE STRING "")
set(KernelRootCNodeSizeBits 19 CACHE STRING "")
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
set(KernelClzNoBuiltin ON CACHE BOOL "")
set(KernelCtzNoBuiltin ON CACHE BOOL "")

4
tools/helpers.cmake
View file

@ -688,7 +688,7 @@ endmacro()
# cmake -G Ninja ${args} -C ${CMAKE_ARGV2} ${CMAKE_CURRENT_LIST_DIR}/..
# ninja kernel.elf
# ninja kernel_all_pp_wrapper
macro(cmake_script_build_kernel)
macro(cmake_script_build_kernel RELPATH)
if(NOT "${CMAKE_ARGC}" STREQUAL "")
set(args "")
foreach(i RANGE 3 ${CMAKE_ARGC})
@ -702,7 +702,7 @@ macro(cmake_script_build_kernel)
endforeach()
execute_process(
COMMAND
cmake -G Ninja ${args} -C ${CMAKE_ARGV2} ${CMAKE_CURRENT_LIST_DIR}/..
cmake -G Ninja ${args} -C ${CMAKE_ARGV2} ${CMAKE_CURRENT_LIST_DIR}/${RELPATH}
INPUT_FILE /dev/stdin
OUTPUT_FILE /dev/stdout
ERROR_FILE /dev/stderr