forked from Imagelibrary/seL4
config.cmake: apply cmake-format style changes
Signed-off-by: julia <git.ts@trainwit.ch>
This commit is contained in:
127
config.cmake
127
config.cmake
@@ -7,8 +7,7 @@
|
||||
cmake_minimum_required(VERSION 3.16.0)
|
||||
|
||||
config_option(
|
||||
KernelIsMCS KERNEL_MCS "Use the MCS kernel configuration, which is not verified."
|
||||
DEFAULT OFF
|
||||
KernelIsMCS KERNEL_MCS "Use the MCS kernel configuration, which is not verified." DEFAULT OFF
|
||||
)
|
||||
|
||||
# Error for unsupported MCS platforms
|
||||
@@ -19,9 +18,18 @@ if(KernelIsMCS AND (NOT KernelPlatformSupportsMCS))
|
||||
endif()
|
||||
|
||||
# Proof based configuration variables
|
||||
set(CSPEC_DIR "." CACHE PATH "")
|
||||
set(SKIP_MODIFIES ON CACHE BOOL "")
|
||||
set(SORRY_BITFIELD_PROOFS OFF CACHE BOOL "")
|
||||
set(CSPEC_DIR
|
||||
"."
|
||||
CACHE PATH ""
|
||||
)
|
||||
set(SKIP_MODIFIES
|
||||
ON
|
||||
CACHE BOOL ""
|
||||
)
|
||||
set(SORRY_BITFIELD_PROOFS
|
||||
OFF
|
||||
CACHE BOOL ""
|
||||
)
|
||||
find_file(UMM_TYPES umm_types.txt CMAKE_FIND_ROOT_PATH_BOTH)
|
||||
set(force FORCE)
|
||||
if(KernelVerificationBuild)
|
||||
@@ -34,8 +42,7 @@ add_custom_target(kernel_config_target)
|
||||
set_property(
|
||||
TARGET kernel_config_target
|
||||
APPEND
|
||||
PROPERTY
|
||||
TOPLEVELTYPES
|
||||
PROPERTY TOPLEVELTYPES
|
||||
cte_C
|
||||
tcb_C
|
||||
endpoint_C
|
||||
@@ -52,13 +59,11 @@ if(DEFINED CALLED_declare_default_headers)
|
||||
if("${KernelArch}" STREQUAL "riscv")
|
||||
math(EXPR MAX_NUM_IRQ "${CONFIGURE_MAX_IRQ} + 2")
|
||||
else()
|
||||
if(
|
||||
DEFINED KernelMaxNumNodes
|
||||
if(DEFINED KernelMaxNumNodes
|
||||
AND CONFIGURE_NUM_PPI GREATER "0"
|
||||
AND "${KernelArch}" STREQUAL "arm"
|
||||
)
|
||||
math(
|
||||
EXPR MAX_NUM_IRQ
|
||||
math(EXPR MAX_NUM_IRQ
|
||||
"(${KernelMaxNumNodes}-1)*${CONFIGURE_NUM_PPI} + ${CONFIGURE_MAX_IRQ}"
|
||||
)
|
||||
else()
|
||||
@@ -70,7 +75,10 @@ if(DEFINED CALLED_declare_default_headers)
|
||||
math(EXPR BITS "${BITS} + 1")
|
||||
math(EXPR MAX_NUM_IRQ "${MAX_NUM_IRQ} >> 1")
|
||||
endwhile()
|
||||
set(CONFIGURE_IRQ_SLOT_BITS "${BITS}" CACHE INTERNAL "")
|
||||
set(CONFIGURE_IRQ_SLOT_BITS
|
||||
"${BITS}"
|
||||
CACHE INTERNAL ""
|
||||
)
|
||||
if(NOT DEFINED CONFIGURE_TIMER_PRECISION)
|
||||
set(CONFIGURE_TIMER_PRECISION "0")
|
||||
endif()
|
||||
@@ -92,8 +100,11 @@ include(src/arch/${KernelArch}/config.cmake)
|
||||
include(include/${KernelWordSize}/mode/config.cmake)
|
||||
include(src/config.cmake)
|
||||
|
||||
set(KernelCustomDTS "" CACHE FILEPATH "Provide a device tree file to use instead of the \
|
||||
KernelPlatform's defaults")
|
||||
set(KernelCustomDTS
|
||||
""
|
||||
CACHE FILEPATH "Provide a device tree file to use instead of the \
|
||||
KernelPlatform's defaults"
|
||||
)
|
||||
|
||||
if(NOT "${KernelCustomDTS}" STREQUAL "")
|
||||
if(NOT EXISTS ${KernelCustomDTS})
|
||||
@@ -110,7 +121,9 @@ config_set(KernelPaddrUserTop PADDR_USER_DEVICE_TOP "${KernelPaddrUserTop}")
|
||||
|
||||
# System parameters
|
||||
config_string(
|
||||
KernelRootCNodeSizeBits ROOT_CNODE_SIZE_BITS "Root CNode Size (2^n slots) \
|
||||
KernelRootCNodeSizeBits
|
||||
ROOT_CNODE_SIZE_BITS
|
||||
"Root CNode Size (2^n slots) \
|
||||
The acceptable range is 8-27 and 7-26, for 32-bit and 64-bit respectively. \
|
||||
The root CNode needs at least enough space to contain seL4_NumInitialCaps \
|
||||
plus enough room for all the Untyped Caps."
|
||||
@@ -218,7 +231,8 @@ else()
|
||||
endif()
|
||||
|
||||
config_string(
|
||||
KernelStackBits KERNEL_STACK_BITS
|
||||
KernelStackBits
|
||||
KERNEL_STACK_BITS
|
||||
"This describes the log2 size of the kernel stack. Great care should be taken as\
|
||||
there is no guard below the stack so setting this too small will cause random\
|
||||
memory corruption"
|
||||
@@ -227,7 +241,8 @@ config_string(
|
||||
)
|
||||
|
||||
config_string(
|
||||
KernelFPUMaxRestoresSinceSwitch FPU_MAX_RESTORES_SINCE_SWITCH
|
||||
KernelFPUMaxRestoresSinceSwitch
|
||||
FPU_MAX_RESTORES_SINCE_SWITCH
|
||||
"This option is a heuristic to attempt to detect when the FPU is no longer in use,\
|
||||
allowing the kernel to save the FPU state out so that the FPU does not have to be\
|
||||
enabled/disabled every thread switch. Every time we restore a thread and there is\
|
||||
@@ -239,7 +254,8 @@ config_string(
|
||||
)
|
||||
|
||||
config_option(
|
||||
KernelVerificationBuild VERIFICATION_BUILD
|
||||
KernelVerificationBuild
|
||||
VERIFICATION_BUILD
|
||||
"When enabled this configuration option prevents the usage of any other options that\
|
||||
would compromise the verification story of the kernel. Enabling this option does NOT\
|
||||
imply you are using a verified kernel."
|
||||
@@ -247,7 +263,8 @@ config_option(
|
||||
)
|
||||
|
||||
config_option(
|
||||
KernelBinaryVerificationBuild BINARY_VERIFICATION_BUILD
|
||||
KernelBinaryVerificationBuild
|
||||
BINARY_VERIFICATION_BUILD
|
||||
"When enabled, this configuration option restricts the use of other options that would \
|
||||
interfere with binary verification. For example, it will disable some inter-procedural \
|
||||
optimisations. Enabling this options does NOT imply that you are using a verified kernel."
|
||||
@@ -263,7 +280,8 @@ config_option(
|
||||
)
|
||||
|
||||
config_option(
|
||||
HardwareDebugAPI HARDWARE_DEBUG_API
|
||||
HardwareDebugAPI
|
||||
HARDWARE_DEBUG_API
|
||||
"Builds the kernel with support for a userspace debug API, which can \
|
||||
allows userspace processes to set breakpoints, watchpoints and to \
|
||||
single-step through thread execution."
|
||||
@@ -319,7 +337,8 @@ else()
|
||||
endif()
|
||||
|
||||
config_string(
|
||||
KernelMaxNumTracePoints MAX_NUM_TRACE_POINTS
|
||||
KernelMaxNumTracePoints
|
||||
MAX_NUM_TRACE_POINTS
|
||||
"Use TRACE_POINT_START(k) and TRACE_POINT_STOP(k) macros for recording data, \
|
||||
where k is an integer between 0 and this value - 1. The maximum number of \
|
||||
different trace point identifiers which can be used."
|
||||
@@ -329,7 +348,8 @@ config_string(
|
||||
)
|
||||
|
||||
config_option(
|
||||
KernelIRQReporting IRQ_REPORTING
|
||||
KernelIRQReporting
|
||||
IRQ_REPORTING
|
||||
"seL4 does not properly check for and handle spurious interrupts. This can result \
|
||||
in unnecessary output from the kernel during debug builds. If you are CERTAIN these \
|
||||
messages are benign then use this config to turn them off."
|
||||
@@ -338,7 +358,8 @@ config_option(
|
||||
DEFAULT_DISABLED OFF
|
||||
)
|
||||
config_option(
|
||||
KernelColourPrinting COLOUR_PRINTING
|
||||
KernelColourPrinting
|
||||
COLOUR_PRINTING
|
||||
"In debug mode, seL4 prints diagnostic messages to its serial output describing, \
|
||||
e.g., the cause of system call errors. This setting determines whether ANSI escape \
|
||||
codes are applied to colour code these error messages. You may wish to disable this \
|
||||
@@ -368,7 +389,8 @@ config_choice(
|
||||
)
|
||||
|
||||
config_option(
|
||||
KernelOptimisationCloneFunctions KERNEL_OPTIMISATION_CLONE_FUNCTIONS
|
||||
KernelOptimisationCloneFunctions
|
||||
KERNEL_OPTIMISATION_CLONE_FUNCTIONS
|
||||
"If enabled, allow inter-procedural optimisations that can generate cloned or partial \
|
||||
functions, according to the coarse optimisation setting (KernelOptimisation). \
|
||||
By default, these optimisations are present at -O2 and higher. \
|
||||
@@ -399,7 +421,8 @@ config_option(
|
||||
)
|
||||
|
||||
config_option(
|
||||
KernelDebugDisablePrefetchers DEBUG_DISABLE_PREFETCHERS
|
||||
KernelDebugDisablePrefetchers
|
||||
DEBUG_DISABLE_PREFETCHERS
|
||||
"On ia32 platforms, this option disables the L2 hardware prefetcher, the L2 adjacent \
|
||||
cache line prefetcher, the DCU prefetcher and the DCU IP prefetcher. On the cortex \
|
||||
a53 this disables the L1 Data prefetcher."
|
||||
@@ -412,7 +435,8 @@ config_option(
|
||||
config_set(KernelSetTLSBaseSelf SET_TLS_BASE_SELF ${KernelSetTLSBaseSelf})
|
||||
|
||||
config_string(
|
||||
KernelWcetScale KERNEL_WCET_SCALE
|
||||
KernelWcetScale
|
||||
KERNEL_WCET_SCALE
|
||||
"Multiplier to scale kernel WCET estimate by: the kernel WCET estimate \
|
||||
is used to ensure a thread has enough budget to get in and out of the \
|
||||
kernel. When running in a simulator the WCET estimate, which is tuned \
|
||||
@@ -436,64 +460,57 @@ config_string(
|
||||
|
||||
config_option(
|
||||
KernelClz32 CLZ_32 "Define a __clzsi2 function to count leading zeros for uint32_t arguments. \
|
||||
Only needed on platforms which lack a builtin instruction."
|
||||
DEFAULT OFF
|
||||
Only needed on platforms which lack a builtin instruction." DEFAULT OFF
|
||||
)
|
||||
|
||||
config_option(
|
||||
KernelClz64 CLZ_64 "Define a __clzdi2 function to count leading zeros for uint64_t arguments. \
|
||||
Only needed on platforms which lack a builtin instruction."
|
||||
DEFAULT OFF
|
||||
Only needed on platforms which lack a builtin instruction." DEFAULT OFF
|
||||
)
|
||||
|
||||
config_option(
|
||||
KernelCtz32 CTZ_32 "Define a __ctzsi2 function to count trailing zeros for uint32_t arguments. \
|
||||
Only needed on platforms which lack a builtin instruction."
|
||||
DEFAULT OFF
|
||||
Only needed on platforms which lack a builtin instruction." DEFAULT OFF
|
||||
)
|
||||
|
||||
config_option(
|
||||
KernelCtz64 CTZ_64 "Define a __ctzdi2 function to count trailing zeros for uint64_t arguments. \
|
||||
Only needed on platforms which lack a builtin instruction."
|
||||
DEFAULT OFF
|
||||
Only needed on platforms which lack a builtin instruction." DEFAULT OFF
|
||||
)
|
||||
|
||||
config_option(
|
||||
KernelClzNoBuiltin CLZ_NO_BUILTIN
|
||||
"Expose implementations of clzl and clzll to verification by avoiding the use \
|
||||
of __builtin_clzl and __builtin_clzll."
|
||||
DEFAULT OFF
|
||||
of __builtin_clzl and __builtin_clzll." DEFAULT OFF
|
||||
)
|
||||
|
||||
config_option(
|
||||
KernelCtzNoBuiltin CTZ_NO_BUILTIN
|
||||
"Expose implementations of ctzl and ctzll to verification by avoiding the use \
|
||||
of __builtin_ctzl and __builtin_ctzll."
|
||||
DEFAULT OFF
|
||||
of __builtin_ctzl and __builtin_ctzll." DEFAULT OFF
|
||||
)
|
||||
|
||||
if(DEFINED KernelDTSList AND (NOT "${KernelDTSList}" STREQUAL ""))
|
||||
set(KernelDTSIntermediate "${CMAKE_CURRENT_BINARY_DIR}/kernel.dts")
|
||||
set(
|
||||
KernelDTBPath "${CMAKE_CURRENT_BINARY_DIR}/kernel.dtb"
|
||||
set(KernelDTBPath
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/kernel.dtb"
|
||||
CACHE INTERNAL "Location of kernel DTB file"
|
||||
)
|
||||
set(compatibility_outfile "${CMAKE_CURRENT_BINARY_DIR}/kernel_compat.txt")
|
||||
set(device_dest "${CMAKE_CURRENT_BINARY_DIR}/gen_headers/plat/machine/devices_gen.h")
|
||||
set(
|
||||
platform_yaml "${CMAKE_CURRENT_BINARY_DIR}/gen_headers/plat/machine/platform_gen.yaml"
|
||||
set(platform_yaml
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/gen_headers/plat/machine/platform_gen.yaml"
|
||||
CACHE INTERNAL "Location of platform YAML description"
|
||||
)
|
||||
set(
|
||||
platform_json "${CMAKE_CURRENT_BINARY_DIR}/gen_headers/plat/machine/platform_gen.json"
|
||||
set(platform_json
|
||||
"${CMAKE_CURRENT_BINARY_DIR}/gen_headers/plat/machine/platform_gen.json"
|
||||
CACHE INTERNAL "Location of platform JSON description"
|
||||
)
|
||||
set(config_file "${CMAKE_CURRENT_SOURCE_DIR}/tools/hardware.yml")
|
||||
set(config_schema "${CMAKE_CURRENT_SOURCE_DIR}/tools/hardware_schema.yml")
|
||||
set(
|
||||
KernelCustomDTSOverlay ""
|
||||
CACHE
|
||||
STRING
|
||||
set(KernelCustomDTSOverlay
|
||||
""
|
||||
CACHE STRING
|
||||
"Provide an additional list of overlays to append to the selected KernelPlatform's \
|
||||
device tree during build time"
|
||||
)
|
||||
@@ -531,8 +548,7 @@ if(DEFINED KernelDTSList AND (NOT "${KernelDTSList}" STREQUAL ""))
|
||||
endforeach()
|
||||
# Compile DTS to DTB
|
||||
execute_process(
|
||||
COMMAND
|
||||
${DTC_TOOL} -q -I dts -O dtb -o ${KernelDTBPath} ${KernelDTSIntermediate}
|
||||
COMMAND ${DTC_TOOL} -q -I dts -O dtb -o ${KernelDTBPath} ${KernelDTSIntermediate}
|
||||
RESULT_VARIABLE error
|
||||
)
|
||||
if(error)
|
||||
@@ -556,14 +572,11 @@ if(DEFINED KernelDTSList AND (NOT "${KernelDTSList}" STREQUAL ""))
|
||||
if(error)
|
||||
message(FATAL_ERROR "Failed to determine KernelDTBSize: ${KernelDTBPath}")
|
||||
endif()
|
||||
string(
|
||||
REPLACE
|
||||
"\'"
|
||||
""
|
||||
KernelDTBSize
|
||||
${KernelDTBSize}
|
||||
string(REPLACE "\'" "" KernelDTBSize ${KernelDTBSize})
|
||||
set(KernelDTBSize
|
||||
"${KernelDTBSize}"
|
||||
CACHE INTERNAL "Size of DTB blob, in bytes"
|
||||
)
|
||||
set(KernelDTBSize "${KernelDTBSize}" CACHE INTERNAL "Size of DTB blob, in bytes")
|
||||
endif()
|
||||
|
||||
set(deps ${KernelDTBPath} ${config_file} ${config_schema} ${HARDWARE_GEN_PATH})
|
||||
|
||||
Reference in New Issue
Block a user