1# 2# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3# 4# SPDX-License-Identifier: GPL-2.0-only 5# 6 7cmake_minimum_required(VERSION 3.7.2) 8 9set(configure_string "${config_configure_string}") 10 11config_option( 12 KernelIsMCS KERNEL_MCS "Use the MCS kernel configuration, which is not verified." 13 DEFAULT OFF 14) 15 16# Error for unsupported MCS platforms 17if(KernelIsMCS AND (NOT KernelPlatformSupportsMCS)) 18 message( 19 FATAL_ERROR "KernelIsMCS selected, but platform: ${KernelPlatform} does not support it." 20 ) 21endif() 22 23# Proof based configuration variables 24set(CSPEC_DIR "." CACHE PATH "") 25set(SKIP_MODIFIES ON CACHE BOOL "") 26set(SORRY_BITFIELD_PROOFS OFF CACHE BOOL "") 27find_file(UMM_TYPES umm_types.txt CMAKE_FIND_ROOT_PATH_BOTH) 28set(force FORCE) 29if(KernelVerificationBuild) 30 set(force CLEAR) 31endif() 32mark_as_advanced(${force} CSPEC_DIR SKIP_MODIFIES SORRY_BITFIELD_PROOFS UMM_TYPES) 33# Use a custom target for collecting information during generation that we need during build 34add_custom_target(kernel_config_target) 35# Put our common top level types in 36set_property( 37 TARGET kernel_config_target 38 APPEND 39 PROPERTY 40 TOPLEVELTYPES 41 cte_C 42 tcb_C 43 endpoint_C 44 notification_C 45 asid_pool_C 46 pte_C 47 user_data_C 48 user_data_device_C 49) 50 51# These options are now set in seL4Config.cmake 52if(DEFINED CONFIGURE_MAX_IRQ) 53 # calculate the irq cnode size based on MAX_IRQ 54 if("${KernelArch}" STREQUAL "riscv") 55 set(MAX_IRQ "${CONFIGURE_PLIC_MAX_NUM_INT}") 56 math(EXPR MAX_NUM_IRQ "${MAX_IRQ} + 2") 57 else() 58 if( 59 DEFINED KernelMaxNumNodes 60 AND CONFIGURE_NUM_PPI GREATER "0" 61 AND "${KernelArch}" STREQUAL "arm" 62 ) 63 math( 64 EXPR MAX_NUM_IRQ 65 "(${KernelMaxNumNodes}-1)*${CONFIGURE_NUM_PPI} + ${CONFIGURE_MAX_IRQ}" 66 ) 67 else() 68 set(MAX_NUM_IRQ "${CONFIGURE_MAX_IRQ}") 69 endif() 70 endif() 71 set(BITS "0") 72 while(MAX_NUM_IRQ GREATER "0") 73 math(EXPR BITS "${BITS} + 1") 74 math(EXPR MAX_NUM_IRQ "${MAX_NUM_IRQ} >> 1") 75 endwhile() 76 math(EXPR SLOTS "1 << ${BITS}") 77 if("${SLOTS}" LESS "${MAX_IRQ}") 78 math(EXPR BITS "${BITS} + 1") 79 endif() 80 set(CONFIGURE_IRQ_SLOT_BITS "${BITS}" CACHE INTERNAL "") 81 if(NOT DEFINED ${CONFIGURE_TIMER_PRECISION}) 82 set(CONFIGURE_TIMER_PRECISION "0") 83 endif() 84 configure_file( 85 src/arch/${KernelArch}/platform_gen.h.in 86 ${CMAKE_CURRENT_BINARY_DIR}/gen_headers/plat/platform_gen.h @ONLY 87 ) 88 include_directories(include/plat/default) 89endif() 90 91# Set defaults for common variables 92set(KernelHaveFPU OFF) 93set(KernelSetTLSBaseSelf OFF) 94 95include(src/arch/${KernelArch}/config.cmake) 96include(include/${KernelWordSize}/mode/config.cmake) 97include(src/config.cmake) 98 99if(DEFINED KernelDTSList AND (NOT "${KernelDTSList}" STREQUAL "")) 100 set(KernelDTSIntermediate "${CMAKE_CURRENT_BINARY_DIR}/kernel.dts") 101 set( 102 KernelDTBPath "${CMAKE_CURRENT_BINARY_DIR}/kernel.dtb" 103 CACHE INTERNAL "Location of kernel DTB file" 104 ) 105 set(compatibility_outfile "${CMAKE_CURRENT_BINARY_DIR}/kernel_compat.txt") 106 set(device_dest "${CMAKE_CURRENT_BINARY_DIR}/gen_headers/plat/machine/devices_gen.h") 107 set( 108 platform_yaml "${CMAKE_CURRENT_BINARY_DIR}/gen_headers/plat/machine/platform_gen.yaml" 109 CACHE INTERNAL "Location of platform YAML description" 110 ) 111 set(config_file "${CMAKE_CURRENT_SOURCE_DIR}/tools/hardware.yml") 112 set(config_schema "${CMAKE_CURRENT_SOURCE_DIR}/tools/hardware_schema.yml") 113 114 find_program(DTC_TOOL dtc) 115 if("${DTC_TOOL}" STREQUAL "DTC_TOOL-NOTFOUND") 116 message(FATAL_ERROR "Cannot find 'dtc' program.") 117 endif() 118 find_program(STAT_TOOL stat) 119 if("${STAT_TOOL}" STREQUAL "STAT_TOOL-NOTFOUND") 120 message(FATAL_ERROR "Cannot find 'stat' program.") 121 endif() 122 mark_as_advanced(DTC_TOOL STAT_TOOL) 123 # Generate final DTS based on Linux DTS + seL4 overlay[s] 124 foreach(entry ${KernelDTSList}) 125 get_absolute_source_or_binary(dts_tmp ${entry}) 126 list(APPEND dts_list "${dts_tmp}") 127 endforeach() 128 129 check_outfile_stale(regen ${KernelDTBPath} dts_list ${CMAKE_CURRENT_BINARY_DIR}/dts.cmd) 130 if(regen) 131 file(REMOVE "${KernelDTSIntermediate}") 132 foreach(entry ${dts_list}) 133 file(READ ${entry} CONTENTS) 134 file(APPEND "${KernelDTSIntermediate}" "${CONTENTS}") 135 endforeach() 136 # Compile DTS to DTB 137 execute_process( 138 COMMAND 139 ${DTC_TOOL} -q -I dts -O dtb -o ${KernelDTBPath} ${KernelDTSIntermediate} 140 ) 141 # Track the size of the DTB for downstream tools 142 execute_process( 143 COMMAND 144 ${STAT_TOOL} -c '%s' ${KernelDTBPath} 145 OUTPUT_VARIABLE KernelDTBSize 146 OUTPUT_STRIP_TRAILING_WHITESPACE 147 ) 148 string( 149 REPLACE 150 "\'" 151 "" 152 KernelDTBSize 153 ${KernelDTBSize} 154 ) 155 set(KernelDTBSize "${KernelDTBSize}" CACHE INTERNAL "Size of DTB blob, in bytes") 156 endif() 157 158 set(deps ${KernelDTBPath} ${config_file} ${config_schema} ${HARDWARE_GEN_PATH}) 159 check_outfile_stale(regen ${device_dest} deps ${CMAKE_CURRENT_BINARY_DIR}/gen_header.cmd) 160 if(regen) 161 # Generate devices_gen header based on DTB 162 message(STATUS "${device_dest} is out of date. Regenerating...") 163 file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/gen_headers/plat/machine/") 164 execute_process( 165 COMMAND 166 ${PYTHON3} "${HARDWARE_GEN_PATH}" --dtb "${KernelDTBPath}" --compat-strings 167 --compat-strings-out "${compatibility_outfile}" --c-header --header-out 168 "${device_dest}" --hardware-config "${config_file}" --hardware-schema 169 "${config_schema}" --yaml --yaml-out "${platform_yaml}" --arch "${KernelArch}" 170 --addrspace-max "${KernelPaddrUserTop}" 171 INPUT_FILE /dev/stdin 172 OUTPUT_FILE /dev/stdout 173 ERROR_FILE /dev/stderr 174 RESULT_VARIABLE error 175 ) 176 if(error) 177 message(FATAL_ERROR "Failed to generate: ${device_dest}") 178 endif() 179 endif() 180 file(READ "${compatibility_outfile}" compatibility_strings) 181 182 # Mark all file dependencies as CMake rerun dependencies. 183 set(cmake_deps ${deps} ${KernelDTSIntermediate} ${KernelDTSList} ${compatibility_outfile}) 184 set_property( 185 DIRECTORY "${CMAKE_CURRENT_SOURCE_DIR}" 186 APPEND 187 PROPERTY CMAKE_CONFIGURE_DEPENDS ${cmake_deps} 188 ) 189 190 include(src/drivers/config.cmake) 191endif() 192 193# Enshrine common variables in the config 194config_set(KernelHaveFPU HAVE_FPU "${KernelHaveFPU}") 195config_set(KernelPaddrUserTop PADDR_USER_DEVICE_TOP "${KernelPaddrUserTop}") 196 197# System parameters 198config_string( 199 KernelRootCNodeSizeBits ROOT_CNODE_SIZE_BITS "Root CNode Size (2^n slots) \ 200 The acceptable range is 8-27 and 7-26, for 32-bit and 64-bit respectively. \ 201 The root CNode needs at least enough space to contain up to BI_CAP_DYN_START." 202 DEFAULT 12 203 UNQUOTE 204) 205 206config_string( 207 KernelTimerTickMS TIMER_TICK_MS "Timer tick period in milliseconds" 208 DEFAULT 2 209 UNQUOTE 210 DEPENDS "NOT KernelIsMCS" UNDEF_DISABLED 211) 212config_string( 213 KernelTimeSlice TIME_SLICE "Number of timer ticks until a thread is preempted." 214 DEFAULT 5 215 UNQUOTE 216 DEPENDS "NOT KernelIsMCS" UNDEF_DISABLED 217) 218config_string( 219 KernelBootThreadTimeSlice BOOT_THREAD_TIME_SLICE 220 "Number of milliseconds until the boot thread is preempted." 221 DEFAULT 5 222 UNQUOTE 223 DEPENDS "KernelIsMCS" UNDEF_DISABLED 224) 225config_string( 226 KernelRetypeFanOutLimit RETYPE_FAN_OUT_LIMIT 227 "Maximum number of objects that can be created in a single Retype() invocation." 228 DEFAULT 256 229 UNQUOTE 230) 231config_string( 232 KernelMaxNumWorkUnitsPerPreemption MAX_NUM_WORK_UNITS_PER_PREEMPTION 233 "Maximum number of work units (delete/revoke iterations) until the kernel checks for\ 234 pending interrupts (and preempts the currently running syscall if interrupts are pending)." 235 DEFAULT 100 236 UNQUOTE 237) 238config_string( 239 KernelResetChunkBits RESET_CHUNK_BITS 240 "Maximum size in bits of chunks of memory to zero before checking a preemption point." 241 DEFAULT 8 242 UNQUOTE 243) 244config_string( 245 KernelMaxNumBootinfoUntypedCaps MAX_NUM_BOOTINFO_UNTYPED_CAPS 246 "Max number of bootinfo untyped caps" 247 DEFAULT 230 248 UNQUOTE 249) 250config_option(KernelFastpath FASTPATH "Enable IPC fastpath" DEFAULT ON) 251 252config_string( 253 KernelNumDomains NUM_DOMAINS "The number of scheduler domains in the system" 254 DEFAULT 1 255 UNQUOTE 256) 257 258find_file( 259 KernelDomainSchedule default_domain.c 260 PATHS src/config 261 CMAKE_FIND_ROOT_PATH_BOTH 262 DOC "A C file providing the symbols ksDomSchedule and ksDomeScheudleLength \ 263 to be linked with the kernel as a scheduling configuration." 264) 265if(SEL4_CONFIG_DEFAULT_ADVANCED) 266 mark_as_advanced(KernelDomainSchedule) 267endif() 268 269config_string( 270 KernelNumPriorities NUM_PRIORITIES "The number of priority levels per domain. Valid range 1-256" 271 DEFAULT 256 272 UNQUOTE 273) 274 275config_string( 276 KernelMaxNumNodes MAX_NUM_NODES "Max number of CPU cores to boot" 277 DEFAULT 1 278 DEPENDS "${KernelNumDomains} EQUAL 1" 279 UNQUOTE 280) 281 282config_string( 283 KernelStackBits KERNEL_STACK_BITS 284 "This describes the log2 size of the kernel stack. Great care should be taken as\ 285 there is no guard below the stack so setting this too small will cause random\ 286 memory corruption" 287 DEFAULT 12 288 UNQUOTE 289) 290 291config_string( 292 KernelFPUMaxRestoresSinceSwitch FPU_MAX_RESTORES_SINCE_SWITCH 293 "This option is a heuristic to attempt to detect when the FPU is no longer in use,\ 294 allowing the kernel to save the FPU state out so that the FPU does not have to be\ 295 enabled/disabled every thread swith. Every time we restore a thread and there is\ 296 active FPU state, we increment this setting and if it exceeds this threshold we\ 297 switch to the NULL state." 298 DEFAULT 64 299 DEPENDS "KernelHaveFPU" UNDEF_DISABLED 300 UNQUOTE 301) 302 303config_option( 304 KernelVerificationBuild VERIFICATION_BUILD 305 "When enabled this configuration option prevents the usage of any other options that\ 306 would compromise the verification story of the kernel. Enabling this option does NOT\ 307 imply you are using a verified kernel." 308 DEFAULT ON 309) 310 311config_option( 312 KernelDebugBuild DEBUG_BUILD "Enable debug facilities (symbols and assertions) in the kernel" 313 DEFAULT ON 314 DEPENDS "NOT KernelVerificationBuild" 315 DEFAULT_DISABLED OFF 316) 317 318config_option( 319 HardwareDebugAPI HARDWARE_DEBUG_API 320 "Builds the kernel with support for a userspace debug API, which can \ 321 allows userspace processes to set breakpoints, watchpoints and to \ 322 single-step through thread execution." 323 DEFAULT OFF 324 DEPENDS "NOT KernelVerificationBuild;NOT KernelHardwareDebugAPIUnsupported" 325) 326config_option( 327 KernelPrinting PRINTING 328 "Allow the kernel to print out messages to the serial console during bootup and execution." 329 DEFAULT "${KernelDebugBuild}" 330 DEPENDS "NOT KernelVerificationBuild" 331 DEFAULT_DISABLED OFF 332) 333 334config_option( 335 KernelInvocationReportErrorIPC KERNEL_INVOCATION_REPORT_ERROR_IPC 336 "Allows the kernel to write the userError to the IPC buffer" 337 DEFAULT OFF 338 DEPENDS "KernelPrinting" 339 DEFAULT_DISABLED OFF 340) 341 342config_choice( 343 KernelBenchmarks 344 KERNEL_BENCHMARK 345 "Enable benchamrks including logging and tracing info. \ 346 Setting this value > 1 enables a 1MB log buffer and functions for extracting data from it \ 347 at user level. NOTE this is only tested on the sabre and will not work on platforms with < 512mb memory. \ 348 This is not fully implemented for x86. \ 349 none -> No Benchmarking features enabled. \ 350 generic -> Enable global benchmarks config variable with no specific features. \ 351 track_kernel_entries -> Log kernel entries information including timing, number of invocations and arguments for \ 352 system calls, interrupts, user faults and VM faults. \ 353 tracepoints -> Enable manually inserted tracepoints that the kernel will track time consumed between. \ 354 track_utilisation -> Enable the kernel to track each thread's utilisation time." 355 "none;KernelBenchmarksNone;NO_BENCHMARKS" 356 "generic;KernelBenchmarksGeneric;BENCHMARK_GENERIC;NOT KernelVerificationBuild" 357 "track_kernel_entries;KernelBenchmarksTrackKernelEntries;BENCHMARK_TRACK_KERNEL_ENTRIES;NOT KernelVerificationBuild" 358 "tracepoints;KernelBenchmarksTracepoints;BENCHMARK_TRACEPOINTS;NOT KernelVerificationBuild" 359 "track_utilisation;KernelBenchmarksTrackUtilisation;BENCHMARK_TRACK_UTILISATION;NOT KernelVerificationBuild" 360) 361if(NOT (KernelBenchmarks STREQUAL "none")) 362 config_set(KernelEnableBenchmarks ENABLE_BENCHMARKS ON) 363else() 364 config_set(KernelEnableBenchmarks ENABLE_BENCHMARKS OFF) 365endif() 366config_string( 367 KernelMaxNumTracePoints MAX_NUM_TRACE_POINTS 368 "Use TRACE_POINT_START(k) and TRACE_POINT_STOP(k) macros for recording data, \ 369 where k is an integer between 0 and this value - 1. The maximum number of \ 370 different trace point identifiers which can be used." 371 DEFAULT 1 372 DEPENDS "NOT KernelVerificationBuild;KernelBenchmarksTracepoints" DEFAULT_DISABLED 0 373 UNQUOTE 374) 375 376config_option( 377 KernelIRQReporting IRQ_REPORTING 378 "seL4 does not properly check for and handle spurious interrupts. This can result \ 379 in unnecessary output from the kernel during debug builds. If you are CERTAIN these \ 380 messages are benign then use this config to turn them off." 381 DEFAULT ON 382 DEPENDS "KernelPrinting" 383 DEFAULT_DISABLED OFF 384) 385config_option( 386 KernelColourPrinting COLOUR_PRINTING 387 "In debug mode, seL4 prints diagnostic messages to its serial output describing, \ 388 e.g., the cause of system call errors. This setting determines whether ANSI escape \ 389 codes are applied to colour code these error messages. You may wish to disable this \ 390 setting if your serial output is redirected to a file or pipe." 391 DEFAULT ON 392 DEPENDS "KernelPrinting" 393 DEFAULT_DISABLED OFF 394) 395config_string( 396 KernelUserStackTraceLength USER_STACK_TRACE_LENGTH 397 "On a double fault the kernel can try and print out the users stack to aid \ 398 debugging. This option determines how many words of stack should be printed." 399 DEFAULT 16 400 DEPENDS "KernelPrinting" DEFAULT_DISABLED 0 401 UNQUOTE 402) 403 404config_choice( 405 KernelOptimisation 406 KERNEL_OPT_LEVEL 407 "Select the kernel optimisation level" 408 "-O2;KernelOptimisationO2;KERNEL_OPT_LEVEL_O2" 409 "-Os;KernelOptimisationOS;KERNEL_OPT_LEVEL_OS" 410 "-O0;KernelOptimisationO0;KERNEL_OPT_LEVEL_O0" 411 "-O1;KernelOptimisationO1;KERNEL_OPT_LEVEL_O1" 412 "-O3;KernelOptimisationO3;KERNEL_OPT_LEVEL_O3" 413) 414 415config_option( 416 KernelFWholeProgram KERNEL_FWHOLE_PROGRAM 417 "Enable -fwhole-program when linking kernel. This should work modulo gcc bugs, which \ 418 are not uncommon with -fwhole-program. Consider this feature experimental!" 419 DEFAULT OFF 420) 421 422config_option( 423 KernelDangerousCodeInjection DANGEROUS_CODE_INJECTION 424 "Adds a system call that allows users to specify code to be run in kernel mode. \ 425 Useful for profiling." 426 DEFAULT OFF 427 DEPENDS 428 "NOT KernelARMHypervisorSupport;NOT KernelVerificationBuild;NOT KernelPlatformHikey;NOT KernelSkimWindow" 429) 430 431config_option( 432 KernelDebugDisablePrefetchers DEBUG_DISABLE_PREFETCHERS 433 "On ia32 platforms, this option disables the L2 hardware prefetcher, the L2 adjacent \ 434 cache line prefetcher, the DCU prefetcher and the DCU IP prefetcher. On the cortex \ 435 a53 this disables the L1 Data prefetcher." 436 DEFAULT OFF 437 DEPENDS "KernelArchX86 OR KernelPlatformHikey" 438) 439 440# Builds the kernel with support for an invocation to set the TLS_BASE 441# of the currently running thread without a capability. 442config_set(KernelSetTLSBaseSelf SET_TLS_BASE_SELF ${KernelSetTLSBaseSelf}) 443 444config_string( 445 KernelWcetScale KERNEL_WCET_SCALE 446 "Multiplier to scale kernel WCET estimate by: the kernel WCET estimate \ 447 is used to ensure a thread has enough budget to get in and out of the \ 448 kernel. When running in a simulator the WCET estimate, which is tuned \ 449 for hardware, may not be sufficient. This option provides a hacky knob \ 450 that can be fiddled with when running inside a simulator." 451 DEFAULT 1 452 UNQUOTE 453 DEPENDS "KernelIsMCS" UNDEF_DISABLED 454) 455 456config_string( 457 KernelStaticMaxBudgetUs KERNEL_STATIC_MAX_BUDGET_US 458 "Specifies a static maximum to which scheduling context can have \ 459 either its period or budget configured." 460 DEFAULT 0 461 UNQUOTE 462 DEPENDS "KernelIsMCS" UNDEF_DISABLED 463) 464 465add_config_library(kernel "${configure_string}") 466