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.8.2) 8include(CheckCCompilerFlag) 9project(seL4 C ASM) 10 11# First find our helpers 12find_file(KERNEL_HELPERS_PATH helpers.cmake PATHS tools CMAKE_FIND_ROOT_PATH_BOTH) 13mark_as_advanced(FORCE KERNEL_HELPERS_PATH) 14include(${KERNEL_HELPERS_PATH}) 15 16function(RequireTool config file) 17 RequireFile("${config}" "${file}" PATHS tools) 18endfunction(RequireTool) 19 20RequireTool(KERNEL_FLAGS_PATH flags.cmake) 21 22if(CCACHEFOUND) 23 set(ccache "ccache") 24endif() 25 26include(tools/internal.cmake) 27 28# Define tools used by the kernel 29set(PYTHON "python2" CACHE INTERNAL "") 30set(PYTHON3 "python3" CACHE INTERNAL "") 31RequireTool(CPP_GEN_PATH cpp_gen.sh) 32RequireTool(CIRCULAR_INCLUDES circular_includes.py) 33RequireTool(BF_GEN_PATH bitfield_gen.py) 34RequireTool(HARDWARE_GEN_PATH hardware_gen.py) 35RequireTool(INVOCATION_ID_GEN_PATH invocation_header_gen.py) 36RequireTool(SYSCALL_ID_GEN_PATH syscall_header_gen.py) 37RequireTool(XMLLINT_PATH xmllint.sh) 38 39set(c_sources "") 40set(asm_sources "") 41set(bf_declarations "") 42foreach(file IN LISTS config_c_sources) 43 list(APPEND c_sources "${CMAKE_CURRENT_SOURCE_DIR}/${file}") 44endforeach() 45foreach(file IN LISTS config_asm_sources) 46 list(APPEND asm_sources "${CMAKE_CURRENT_SOURCE_DIR}/${file}") 47endforeach() 48foreach(file IN LISTS config_bf_declarations) 49 list(APPEND bf_declarations "${CMAKE_CURRENT_SOURCE_DIR}/${file}") 50endforeach() 51set(KernelDTSList "${config_KernelDTSList}") 52 53# Process the configuration scripts 54include(config.cmake) 55 56# Define default global flag information so that users can compile with the same basic architecture 57# flags as the kernel 58if(KernelArchX86) 59 if(${KernelX86MicroArch} STREQUAL generic) 60 set(build_arch "-mtune=generic") 61 else() 62 set(build_arch "-march=${KernelX86MicroArch}") 63 endif() 64 if(Kernel64) 65 if(NOT LLVM_TOOLCHAIN) 66 string(APPEND asm_common_flags " -Wa,--64") 67 endif() 68 string(APPEND c_common_flags " -m64") 69 else() 70 if(NOT LLVM_TOOLCHAIN) 71 string(APPEND asm_common_flags " -Wa,--32") 72 else() 73 string(APPEND asm_common_flags " -m32") 74 endif() 75 string(APPEND c_common_flags " -m32") 76 endif() 77endif() 78if(KernelArchARM) 79 set(arm_march "${KernelArmArmV}${KernelArmMachFeatureModifiers}") 80 string(APPEND c_common_flags " -march=${arm_march}") 81 string(APPEND asm_common_flags " -march=${arm_march}") 82 # Explicitly request ARM instead of THUMB for compilation. This option is not 83 # relevant on aarch64 84 if(NOT KernelSel4ArchAarch64) 85 string(APPEND c_common_flags " -marm") 86 endif() 87endif() 88if(KernelArchRiscV) 89 if(Kernel64) 90 if(KernelHaveFPU) 91 string(APPEND common_flags " -march=rv64imafdc") 92 string(APPEND common_flags " -mabi=lp64d") 93 else() 94 string(APPEND common_flags " -march=rv64imac") 95 string(APPEND common_flags " -mabi=lp64") 96 endif() 97 else() 98 string(APPEND common_flags " -march=rv32imac") 99 string(APPEND common_flags " -mabi=ilp32") 100 endif() 101endif() 102string(APPEND common_flags " ${build_arch}") 103if(Kernel64) 104 string(APPEND common_flags " -D__KERNEL_64__") 105else() 106 string(APPEND common_flags " -D__KERNEL_32__") 107endif() 108 109set( 110 BASE_ASM_FLAGS "${asm_common_flags} ${common_flags}" 111 CACHE INTERNAL "Default ASM flags for compilation \ 112 (subset of flags used by the kernel build)" 113) 114set( 115 BASE_C_FLAGS "${c_common_flags} ${common_flags}" 116 CACHE INTERNAL "Default C flags for compilation \ 117 (subset of flags used by the kernel)" 118) 119set( 120 BASE_CXX_FLAGS "${cxx_common_flags} ${c_common_flags} ${common_flags}" 121 CACHE INTERNAL "Default CXX flags for compilation" 122) 123if(KernelArchX86) 124 if(Kernel64) 125 string(APPEND common_exe_flags " -Wl,-m -Wl,elf_x86_64") 126 else() 127 string(APPEND common_exe_flags " -Wl,-m -Wl,elf_i386") 128 endif() 129endif() 130set( 131 BASE_EXE_LINKER_FLAGS "${common_flags} ${common_exe_flags} " 132 CACHE INTERNAL "Default flags for linker an elf binary application" 133) 134# Initializing the kernel build flags starting from the same base flags that the users will use 135include(${KERNEL_FLAGS_PATH}) 136 137# Setup kernel specific flags 138macro(KernelCommonFlags) 139 foreach(common_flag IN ITEMS ${ARGV}) 140 add_compile_options(${common_flag}) 141 string(APPEND CMAKE_EXE_LINKER_FLAGS " ${common_flag} ") 142 endforeach() 143endmacro(KernelCommonFlags) 144KernelCommonFlags(-nostdinc -nostdlib ${KernelOptimisation} -DHAVE_AUTOCONF) 145if(KernelFWholeProgram) 146 KernelCommonFlags(-fwhole-program) 147endif() 148if(KernelDebugBuild) 149 KernelCommonFlags(-DDEBUG -g -ggdb) 150 # Pretend to CMake that we're a release build with debug info. This is because 151 # we do actually allow CMake to do the final link step, so we'd like it not to 152 # strip our binary 153 set(CMAKE_BUILD_TYPE "RelWithDebInfo") 154else() 155 set(CMAKE_BUILD_TYPE "Release") 156endif() 157if(KernelArchX86 AND Kernel64) 158 KernelCommonFlags(-mcmodel=kernel) 159endif() 160if(KernelArchARM) 161 if(KernelSel4ArchAarch64) 162 KernelCommonFlags(-mgeneral-regs-only) 163 else() 164 KernelCommonFlags(-mfloat-abi=soft) 165 endif() 166endif() 167if(KernelArchRiscV) 168 KernelCommonFlags(-mcmodel=medany) 169endif() 170KernelCommonFlags(-fno-pic -fno-pie) 171add_compile_options( 172 -fno-stack-protector 173 -fno-asynchronous-unwind-tables 174 -std=c99 175 -Wall 176 -Werror 177 -Wstrict-prototypes 178 -Wmissing-prototypes 179 -Wnested-externs 180 -Wmissing-declarations 181 -Wundef 182 -Wpointer-arith 183 -Wno-nonnull 184 -ffreestanding 185) 186 187# Add all the common flags to the linker args 188string(APPEND CMAKE_EXE_LINKER_FLAGS " -ffreestanding -Wl,--build-id=none -static -Wl,-n ") 189 190if(KernelArchX86) 191 add_compile_options(-mno-mmx -mno-sse -mno-sse2 -mno-3dnow) 192endif() 193 194# Sort the C sources to ensure a stable layout of the final C file 195list(SORT c_sources) 196# Add the domain schedule now that its sorted 197list(APPEND c_sources "${KernelDomainSchedule}") 198 199# Add static header includes 200include_directories("include") 201include_directories("include/${KernelWordSize}") 202include_directories("include/arch/${KernelArch}") 203include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}/") 204include_directories("include/plat/${KernelPlatform}/") 205include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}/") 206if(KernelArchARM) 207 include_directories("include/arch/arm/armv/${KernelArmArmV}/") 208 include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") 209endif() 210if(KernelArmMach STREQUAL "exynos") 211 include_directories("include/plat/exynos_common/") 212endif() 213if(KernelArchRiscV) 214 include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") 215 include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") 216endif() 217 218# Add libsel4 include directories. 219# These are explicitly added instead of calling target_link_libraries(${target} sel4) 220# because we don't want to inherit any other build options from libsel4. 221include_directories( 222 "libsel4/include" 223 "libsel4/arch_include/${KernelArch}" 224 "libsel4/sel4_arch_include/${KernelSel4Arch}" 225 "libsel4/sel4_plat_include/${KernelPlatform}" 226 "libsel4/mode_include/${KernelWordSize}" 227) 228 229# 230# Config generation 231# 232 233include_directories($<TARGET_PROPERTY:kernel_Config,INTERFACE_INCLUDE_DIRECTORIES>) 234# The kernel expects to be able to include an 'autoconf.h' file at the moment. So lets 235# generate one for it to use 236# TODO: use the kernel_Config directly 237generate_autoconf(kernel_autoconf "kernel") 238include_directories($<TARGET_PROPERTY:kernel_autoconf,INTERFACE_INCLUDE_DIRECTORIES>) 239 240# Target for the config / autoconf headers. This is what all the other generated headers 241# can depend upon 242add_custom_target( 243 kernel_config_headers 244 DEPENDS 245 kernel_autoconf_Gen 246 kernel_autoconf 247 kernel_Config 248 kernel_Gen 249) 250 251# Target for all generated headers. We start with just all the config / autoconf headers 252add_custom_target(kernel_headers DEPENDS kernel_config_headers) 253 254# Build up a list of generated files. needed for dependencies in custom commands 255get_generated_files(gen_files_list kernel_autoconf_Gen) 256get_generated_files(gen_files2 kernel_Gen) 257list(APPEND gen_files_list "${gen_files2}") 258 259# 260# C source generation 261# 262 263# Kernel compiles all C sources as a single C file, this provides 264# rules for doing the concatenation 265 266add_custom_command( 267 OUTPUT kernel_all.c 268 COMMAND 269 "${CPP_GEN_PATH}" ${c_sources} > kernel_all.c 270 DEPENDS "${CPP_GEN_PATH}" ${c_sources} 271 COMMENT "Concatenating C files" 272 VERBATIM 273) 274 275add_custom_target(kernel_all_c_wrapper DEPENDS kernel_all.c) 276 277# 278# Header Generation 279# 280 281# Rules for generating invocation and syscall headers 282# Aside from generating file rules for dependencies this section will also produce a target 283# that can be depended upon (along with the desired files themselves) to control parallelism 284 285set(xml_headers "") 286set(header_dest "gen_headers/arch/api/invocation.h") 287gen_invocation_header( 288 OUTPUT ${header_dest} 289 XML ${CMAKE_CURRENT_SOURCE_DIR}/libsel4/arch_include/${KernelArch}/interfaces/sel4arch.xml 290 ARCH 291) 292list(APPEND xml_headers "${header_dest}") 293list(APPEND gen_files_list "${header_dest}") 294 295set(header_dest "gen_headers/arch/api/sel4_invocation.h") 296gen_invocation_header( 297 OUTPUT "${header_dest}" 298 XML 299 "${CMAKE_CURRENT_SOURCE_DIR}/libsel4/sel4_arch_include/${KernelSel4Arch}/interfaces/sel4arch.xml" 300 SEL4ARCH 301) 302list(APPEND xml_headers "${header_dest}") 303list(APPEND gen_files_list "${header_dest}") 304 305set(header_dest "gen_headers/api/invocation.h") 306gen_invocation_header( 307 OUTPUT "${header_dest}" 308 XML "${CMAKE_CURRENT_SOURCE_DIR}/libsel4/include/interfaces/sel4.xml" 309) 310list(APPEND xml_headers "${header_dest}") 311list(APPEND gen_files_list "${header_dest}") 312 313set(syscall_xml_base "${CMAKE_CURRENT_SOURCE_DIR}/libsel4/include/api") 314set(syscall_dest "gen_headers/arch/api/syscall.h") 315if(KernelIsMCS) 316 set(mcs --mcs) 317endif() 318add_custom_command( 319 OUTPUT ${syscall_dest} 320 COMMAND 321 "${XMLLINT_PATH}" 322 --noout 323 --schema "${syscall_xml_base}/syscall.xsd" "${syscall_xml_base}/syscall.xml" 324 COMMAND 325 ${CMAKE_COMMAND} -E remove -f "${syscall_dest}" 326 COMMAND 327 ${PYTHON3} "${SYSCALL_ID_GEN_PATH}" 328 --xml "${syscall_xml_base}/syscall.xml" 329 --kernel_header "${syscall_dest}" ${mcs} 330 DEPENDS 331 "${XMLLINT_PATH}" 332 "${SYSCALL_ID_GEN_PATH}" 333 "${syscall_xml_base}/syscall.xsd" 334 "${syscall_xml_base}/syscall.xml" 335 COMMENT "Generate syscall invocations" 336 VERBATIM 337) 338list(APPEND xml_headers "${syscall_dest}") 339list(APPEND gen_files_list "${syscall_dest}") 340# Construct target for just the xml headers 341add_custom_target(xml_headers_target DEPENDS ${xml_headers}) 342# Add the xml headers to all the kernel headers 343add_dependencies(kernel_headers xml_headers_target) 344include_directories("${CMAKE_CURRENT_BINARY_DIR}/gen_headers") 345 346# 347# Prune list generation 348# 349 350# When generating bitfield files we can pass multiple '--prune' parameters that are source 351# files that get searched for determing which bitfield functions are used. This allows the 352# bitfield generator to only generate functions that are used. Whilst irrelevant for 353# normal compilation, not generating unused functions has significant time savings for the 354# automated verification tools 355 356# To generate a prune file we 'build' the kernel (similar to the kernel_all_pp.c rule 357# below) but strictly WITHOUT the generated header directory where the bitfield generated 358# headers are. This means our preprocessed file will contain all the code used by the 359# normal compilation, just without the bitfield headers (which we generate dummy versions of). 360# If we allowed the bitfield headers to be included then we would have a circular 361# dependency. As a result this rule comes *before* the Bitfield header generation section 362 363set(dummy_headers "") 364foreach(bf_dec ${bf_declarations}) 365 string( 366 REPLACE 367 ":" 368 ";" 369 bf_dec 370 ${bf_dec} 371 ) 372 list(GET bf_dec 0 bf_file) 373 list(GET bf_dec 1 bf_gen_dir) 374 get_filename_component(bf_name "${bf_file}" NAME) 375 string( 376 REPLACE 377 ".bf" 378 "_gen.h" 379 bf_target 380 "${bf_name}" 381 ) 382 list( 383 APPEND 384 dummy_headers "${CMAKE_CURRENT_BINARY_DIR}/generated_prune/${bf_gen_dir}/${bf_target}" 385 ) 386endforeach() 387 388add_custom_command( 389 OUTPUT ${dummy_headers} 390 COMMAND 391 ${CMAKE_COMMAND} -E touch ${dummy_headers} 392 COMMENT "Generate dummy headers for prune compilation" 393) 394 395add_custom_target(dummy_header_wrapper DEPENDS ${dummy_headers}) 396 397cppfile( 398 kernel_all_pp_prune.c 399 kernel_all_pp_prune_wrapper 400 kernel_all.c 401 EXTRA_FLAGS 402 -CC 403 "-I${CMAKE_CURRENT_BINARY_DIR}/generated_prune" 404 EXTRA_DEPS 405 kernel_all_c_wrapper 406 dummy_header_wrapper 407 xml_headers_target 408 kernel_config_headers 409 ${gen_files_list} 410) 411 412# 413# Bitfield header generation 414# 415 416# Need to generate a bunch of unique targets, we'll do this with piano numbers 417set(bf_gen_target "kernel_bf_gen_target_1") 418 419foreach(bf_dec ${bf_declarations}) 420 string( 421 REPLACE 422 ":" 423 ";" 424 bf_dec 425 ${bf_dec} 426 ) 427 list(GET bf_dec 0 bf_file) 428 list(GET bf_dec 1 bf_gen_dir) 429 get_filename_component(bf_name "${bf_file}" NAME) 430 string( 431 REPLACE 432 ".bf" 433 "_gen.h" 434 bf_target 435 "${bf_name}" 436 ) 437 string( 438 REPLACE 439 ".bf" 440 "_defs.thy" 441 defs_target 442 "${bf_name}" 443 ) 444 string( 445 REPLACE 446 ".bf" 447 "_proofs.thy" 448 proofs_target 449 "${bf_name}" 450 ) 451 set(pbf_name "generated/${bf_gen_dir}/${bf_name}.pbf") 452 set(pbf_target "${bf_gen_target}_pbf") 453 cppfile( 454 "${pbf_name}" 455 "${pbf_target}" 456 "${bf_file}" 457 EXTRA_FLAGS 458 -P 459 EXTRA_DEPS 460 kernel_config_headers 461 ${gen_files_list} 462 ) 463 GenHBFTarget( 464 "" 465 ${bf_gen_target} 466 "generated/${bf_gen_dir}/${bf_target}" 467 "${pbf_name}" 468 "${pbf_target}" 469 "kernel_all_pp_prune.c" 470 "kernel_all_pp_prune_wrapper" 471 ) 472 GenDefsBFTarget( 473 "${bf_gen_target}_def" 474 "generated/${bf_gen_dir}/${defs_target}" 475 "${pbf_name}" 476 "${pbf_target}" 477 "kernel_all_pp_prune.c" 478 "kernel_all_pp_prune_wrapper" 479 ) 480 GenProofsBFTarget( 481 "${bf_gen_target}_proof" 482 "generated/${bf_gen_dir}/${proofs_target}" 483 "${pbf_name}" 484 "${pbf_target}" 485 "kernel_all_pp_prune.c" 486 "kernel_all_pp_prune_wrapper" 487 ) 488 list( 489 APPEND 490 theories_deps 491 "${bf_gen_target}_def" 492 "${CMAKE_CURRENT_BINARY_DIR}/generated/${bf_gen_dir}/${defs_target}" 493 "${bf_gen_target}_proof" 494 "${CMAKE_CURRENT_BINARY_DIR}/generated/${bf_gen_dir}/${proofs_target}" 495 ) 496 add_dependencies(kernel_headers "${bf_gen_target}") 497 list(APPEND gen_files_list "${CMAKE_CURRENT_BINARY_DIR}/generated/${bf_gen_dir}/${bf_target}") 498 set(bf_gen_target "${bf_gen_target}1") 499endforeach() 500# At this point we have generated a bunch of headers into ${CMAKE_CURRENT_BINARY_DIR}/generated 501# but we do not pass this to include_directories, as that will cause it to be an include directory 502# for *all* targets in this file (including ones we defined earlier) and the prune generation 503# *must not* see this files and generate dependencies on them as this will result in nonsense. 504# As such we must manually add this as an include directory to future targets 505set(CPPExtraFlags "-I${CMAKE_CURRENT_BINARY_DIR}/generated") 506 507# 508# Kernel compilation 509# 510 511cppfile( 512 kernel_all.i 513 kernel_i_wrapper 514 kernel_all.c 515 EXTRA_DEPS 516 kernel_all_c_wrapper 517 kernel_headers 518 ${gen_files_list} 519 EXTRA_FLAGS 520 -CC 521 "${CPPExtraFlags}" 522 # The circular_includes script relies upon parsing out exactly 'kernel_all_copy.c' as 523 # a special case so we must ask cppfile to use this input name 524 EXACT_NAME kernel_all_copy.c 525) 526 527# Explain to cmake that our object file is actually a C input file 528set_property(SOURCE kernel_all.i PROPERTY LANGUAGE C) 529 530if(KernelArchARM) 531 set(linker_source "src/arch/arm/common_arm.lds") 532elseif(KernelArchRiscV) 533 set(linker_source "src/arch/riscv/common_riscv.lds") 534else() 535 set(linker_source "src/plat/${KernelPlatform}/linker.lds") 536endif() 537set(linker_lds_path "${CMAKE_CURRENT_BINARY_DIR}/linker.lds_pp") 538 539# Preprocess the linker script 540cppfile( 541 "${linker_lds_path}" 542 linker_ld_wrapper 543 "${linker_source}" 544 EXTRA_DEPS 545 kernel_headers 546 ${gen_files_list} 547 EXTRA_FLAGS 548 -CC 549 -P 550 "${CPPExtraFlags}" 551) 552 553add_custom_command( 554 OUTPUT circular_includes_valid 555 COMMAND ${CIRCULAR_INCLUDES} --ignore kernel_all_copy.c < kernel_all.i 556 COMMAND touch circular_includes_valid 557 DEPENDS kernel_i_wrapper kernel_all.i 558) 559 560add_custom_target(circular_includes DEPENDS circular_includes_valid) 561 562add_custom_command( 563 OUTPUT kernel_all_pp.c 564 COMMAND 565 ${CMAKE_COMMAND} -E copy kernel_all.i kernel_all_pp.c 566 DEPENDS kernel_i_wrapper kernel_all.i 567) 568add_custom_target(kernel_all_pp_wrapper DEPENDS kernel_all_pp.c) 569 570add_custom_target(kernel_theories DEPENDS ${theories_deps}) 571 572# Declare final kernel output 573add_executable(kernel.elf EXCLUDE_FROM_ALL ${asm_sources} kernel_all.c) 574target_include_directories(kernel.elf PRIVATE ${config_dir}) 575target_include_directories(kernel.elf PRIVATE include) 576target_include_directories(kernel.elf PRIVATE "${CMAKE_CURRENT_BINARY_DIR}/generated") 577target_link_libraries(kernel.elf PRIVATE kernel_Config kernel_autoconf) 578set_property(TARGET kernel.elf APPEND_STRING PROPERTY LINK_FLAGS " -Wl,-T ${linker_lds_path} ") 579set_target_properties(kernel.elf PROPERTIES LINK_DEPENDS "${linker_lds_path}") 580add_dependencies(kernel.elf circular_includes) 581