Skip to content

Commit c5b2379

Browse files
lsf37lsf37
committed
configs: additional verified platforms
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 <[email protected]>
1 parent 03ad568 commit c5b2379

27 files changed

+221
-191
lines changed

‎configs/AARCH64_bcm2711_verified.cmake‎

Lines changed: 2 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,10 @@
11
#!/usr/bin/env -S cmake -P
22
#
3-
# Copyright 2022, Proofcraft Pty Ltd
4-
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3+
# Copyright 2024, Proofcraft Pty Ltd
54
#
65
# SPDX-License-Identifier: GPL-2.0-only
76
#
87

9-
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
10-
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
11-
cmake_script_build_kernel()
8+
include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
129

1310
set(KernelPlatform "bcm2711" CACHE STRING "")
14-
set(KernelSel4Arch "aarch64" CACHE STRING "")
15-
set(KernelArmHypervisorSupport ON CACHE BOOL "")
16-
set(KernelVerificationBuild ON CACHE BOOL "")
17-
set(KernelMaxNumNodes "1" CACHE STRING "")
18-
set(KernelOptimisation "-O2" CACHE STRING "")
19-
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
20-
set(KernelBenchmarks "none" CACHE STRING "")
21-
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
22-
set(KernelFastpath ON CACHE BOOL "")
23-
set(KernelPrinting OFF CACHE BOOL "")
24-
set(KernelNumDomains 16 CACHE STRING "")
25-
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
26-
set(KernelArmSMMU OFF CACHE BOOL "")

‎configs/AARCH64_hikey_verified.cmake‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#!/usr/bin/env -S cmake -P
2+
#
3+
# Copyright 2024, Proofcraft Pty Ltd
4+
#
5+
# SPDX-License-Identifier: GPL-2.0-only
6+
#
7+
8+
include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
9+
10+
set(KernelPlatform "hikey" CACHE STRING "")

‎configs/AARCH64_odroidc2_verified.cmake‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#!/usr/bin/env -S cmake -P
2+
#
3+
# Copyright 2024, Proofcraft Pty Ltd
4+
#
5+
# SPDX-License-Identifier: GPL-2.0-only
6+
#
7+
8+
include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
9+
10+
set(KernelPlatform "odroidc2" CACHE STRING "")

‎configs/AARCH64_odroidc4_verified.cmake‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
#!/usr/bin/env -S cmake -P
2+
#
3+
# Copyright 2024, Proofcraft Pty Ltd
4+
#
5+
# SPDX-License-Identifier: GPL-2.0-only
6+
#
7+
8+
include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
9+
10+
set(KernelPlatform "odroidc4" CACHE STRING "")

‎configs/AARCH64_verified.cmake‎

Lines changed: 2 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,10 @@
11
#!/usr/bin/env -S cmake -P
22
#
3-
# Copyright 2022, Proofcraft Pty Ltd
4-
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3+
# Copyright 2024, Proofcraft Pty Ltd
54
#
65
# SPDX-License-Identifier: GPL-2.0-only
76
#
87

9-
# This is a preliminary configuration to be used for developing functional
10-
# correctness proofs for the AArch64 architecture.
11-
12-
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
13-
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
14-
cmake_script_build_kernel()
8+
include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
159

1610
set(KernelPlatform "tx2" CACHE STRING "")
17-
set(KernelSel4Arch "aarch64" CACHE STRING "")
18-
set(KernelArmHypervisorSupport ON CACHE BOOL "")
19-
set(KernelVerificationBuild ON CACHE BOOL "")
20-
set(KernelMaxNumNodes "1" CACHE STRING "")
21-
set(KernelOptimisation "-O2" CACHE STRING "")
22-
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
23-
set(KernelBenchmarks "none" CACHE STRING "")
24-
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
25-
set(KernelFastpath ON CACHE BOOL "")
26-
set(KernelPrinting OFF CACHE BOOL "")
27-
set(KernelNumDomains 16 CACHE STRING "")
28-
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
29-
set(KernelArmSMMU OFF CACHE BOOL "")

‎configs/AARCH64_zynqmp_verified.cmake‎

Lines changed: 2 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,10 @@
11
#!/usr/bin/env -S cmake -P
22
#
3-
# Copyright 2022, Proofcraft Pty Ltd
4-
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3+
# Copyright 2024, Proofcraft Pty Ltd
54
#
65
# SPDX-License-Identifier: GPL-2.0-only
76
#
87

9-
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
10-
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
11-
cmake_script_build_kernel()
8+
include(${CMAKE_CURRENT_LIST_DIR}/include/AARCH64_verified_include.cmake)
129

1310
set(KernelPlatform "zynqmp" CACHE STRING "")
14-
set(KernelSel4Arch "aarch64" CACHE STRING "")
15-
set(KernelArmHypervisorSupport ON CACHE BOOL "")
16-
set(KernelVerificationBuild ON CACHE BOOL "")
17-
set(KernelMaxNumNodes "1" CACHE STRING "")
18-
set(KernelOptimisation "-O2" CACHE STRING "")
19-
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
20-
set(KernelBenchmarks "none" CACHE STRING "")
21-
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
22-
set(KernelFastpath ON CACHE BOOL "")
23-
set(KernelPrinting OFF CACHE BOOL "")
24-
set(KernelNumDomains 16 CACHE STRING "")
25-
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")
26-
set(KernelArmSMMU OFF CACHE BOOL "")

‎configs/ARM_HYP_exynos5410_verified.cmake‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#!/usr/bin/env -S cmake -P
2+
#
3+
# Copyright 2024, Proofcraft Pty Ltd
4+
#
5+
# SPDX-License-Identifier: GPL-2.0-only
6+
#
7+
8+
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_HYP_verified_include.cmake)
9+
10+
set(KernelPlatform "exynos5" CACHE STRING "")
11+
set(KernelARMPlatform "exynos5410" CACHE STRING "")

‎configs/ARM_HYP_exynos5_verified.cmake‎

Lines changed: 2 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,27 +1,11 @@
11
#!/usr/bin/env -S cmake -P
22
#
3-
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3+
# Copyright 2024, Proofcraft Pty Ltd
44
#
55
# SPDX-License-Identifier: GPL-2.0-only
66
#
77

8-
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
9-
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
10-
cmake_script_build_kernel()
8+
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_HYP_verified_include.cmake)
119

1210
set(KernelPlatform "exynos5" CACHE STRING "")
1311
set(KernelARMPlatform "exynos5422" CACHE STRING "")
14-
set(KernelSel4Arch "arm_hyp" CACHE STRING "")
15-
set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
16-
set(KernelVerificationBuild ON CACHE BOOL "")
17-
set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
18-
set(KernelMaxNumNodes "1" CACHE STRING "")
19-
set(KernelOptimisation "-O2" CACHE STRING "")
20-
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
21-
set(KernelBenchmarks "none" CACHE STRING "")
22-
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
23-
set(KernelFastpath ON CACHE BOOL "")
24-
set(KernelPrinting OFF CACHE BOOL "")
25-
set(KernelNumDomains 16 CACHE STRING "")
26-
set(KernelRootCNodeSizeBits 19 CACHE STRING "")
27-
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")

‎configs/ARM_HYP_verified.cmake‎

Lines changed: 2 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,10 @@
11
#!/usr/bin/env -S cmake -P
22
#
3-
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3+
# Copyright 2024, Proofcraft Pty Ltd
44
#
55
# SPDX-License-Identifier: GPL-2.0-only
66
#
77

8-
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
9-
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
10-
cmake_script_build_kernel()
8+
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_HYP_verified_include.cmake)
119

1210
set(KernelPlatform "tk1" CACHE STRING "")
13-
set(KernelSel4Arch "arm_hyp" CACHE STRING "")
14-
set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
15-
set(KernelVerificationBuild ON CACHE BOOL "")
16-
set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
17-
set(KernelMaxNumNodes "1" CACHE STRING "")
18-
set(KernelOptimisation "-O2" CACHE STRING "")
19-
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
20-
set(KernelBenchmarks "none" CACHE STRING "")
21-
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
22-
set(KernelFastpath ON CACHE BOOL "")
23-
set(KernelPrinting OFF CACHE BOOL "")
24-
set(KernelNumDomains 16 CACHE STRING "")
25-
set(KernelRootCNodeSizeBits 19 CACHE STRING "")
26-
set(KernelMaxNumBootinfoUntypedCaps 50 CACHE STRING "")

‎configs/ARM_MCS_verified.cmake‎

Lines changed: 2 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -1,28 +1,12 @@
11
#!/usr/bin/env -S cmake -P
22
#
3-
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3+
# Copyright 2024, Proofcraft Pty Ltd
44
#
55
# SPDX-License-Identifier: GPL-2.0-only
66
#
77

8-
# If this file is executed then build the kernel.elf and kernel_all_pp.c file
9-
include(${CMAKE_CURRENT_LIST_DIR}/../tools/helpers.cmake)
10-
cmake_script_build_kernel()
8+
include(${CMAKE_CURRENT_LIST_DIR}/include/ARM_verified_include.cmake)
119

1210
set(KernelPlatform "imx6" CACHE STRING "")
13-
set(KernelAArch32FPUEnableContextSwitch OFF CACHE BOOL "")
14-
set(KernelVerificationBuild ON CACHE BOOL "")
15-
set(KernelBinaryVerificationBuild ON CACHE BOOL "")
16-
set(KernelOptimisationCloneFunctions OFF CACHE BOOL "")
17-
set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
18-
set(KernelMaxNumNodes "1" CACHE STRING "")
19-
set(KernelOptimisation "-O2" CACHE STRING "")
20-
set(KernelRetypeFanOutLimit "256" CACHE STRING "")
21-
set(KernelBenchmarks "none" CACHE STRING "")
22-
set(KernelDangerousCodeInjection OFF CACHE BOOL "")
23-
set(KernelFastpath ON CACHE BOOL "")
24-
set(KernelPrinting OFF CACHE BOOL "")
25-
set(KernelNumDomains 16 CACHE STRING "")
26-
set(KernelMaxNumBootinfoUntypedCaps 230 CACHE STRING "")
2711
set(KernelIsMCS ON CACHE BOOL "")
2812
set(KernelStaticMaxPeriodUs "(60 * 60 * MS_IN_S * US_IN_MS)" CACHE STRING "")

0 commit comments

Comments
 (0)