1# 2# Copyright 2017, Data61 3# Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4# ABN 41 687 119 230. 5# 6# This software may be distributed and modified according to the terms of 7# the GNU General Public License version 2. Note that NO WARRANTY is provided. 8# See "LICENSE_GPLv2.txt" for details. 9# 10# @TAG(DATA61_GPL) 11# 12 13cmake_minimum_required(VERSION 3.8.2) 14include(CheckCCompilerFlag) 15project(seL4 C ASM) 16 17# First find our helpers 18find_file(KERNEL_HELPERS_PATH helpers.cmake PATHS tools CMAKE_FIND_ROOT_PATH_BOTH) 19mark_as_advanced(FORCE KERNEL_HELPERS_PATH) 20include(${KERNEL_HELPERS_PATH}) 21 22function(RequireTool config file) 23 RequireFile("${config}" "${file}" PATHS tools) 24endfunction(RequireTool) 25 26RequireTool(KERNEL_FLAGS_PATH flags.cmake) 27 28if(CCACHEFOUND) 29 set(ccache "ccache") 30endif() 31 32include(tools/internal.cmake) 33 34# Process the configuration scripts 35include(config.cmake) 36 37# Define tools used by the kernel 38set(PYTHON "python" CACHE INTERNAL "") 39RequireTool(CPP_GEN_PATH cpp_gen.sh) 40RequireTool(CIRCULAR_INCLUDES circular_includes.py) 41RequireTool(BF_GEN_PATH bitfield_gen.py) 42RequireTool(INVOCATION_ID_GEN_PATH invocation_header_gen.py) 43RequireTool(SYSCALL_ID_GEN_PATH syscall_header_gen.py) 44RequireTool(XMLLINT_PATH xmllint.sh) 45 46# Define default global flag information so that users can compile with the same basic architecture 47# flags as the kernel 48if(KernelArchX86) 49 if(${KernelX86MicroArch} STREQUAL generic) 50 set(build_arch "-mtune=generic") 51 else() 52 set(build_arch "-march=${KernelX86MicroArch}") 53 endif() 54 if(Kernel64) 55 string(APPEND asm_common_flags " -Wa,--64") 56 string(APPEND c_common_flags " -m64") 57 else() 58 string(APPEND asm_common_flags " -Wa,--32") 59 string(APPEND c_common_flags " -m32") 60 endif() 61endif() 62if(KernelArchARM) 63 set(arm_march "${KernelArmArmV}${KernelArmMachFeatureModifiers}") 64 string(APPEND c_common_flags " -march=${arm_march}") 65 string(APPEND asm_common_flags " -Wa,-march=${arm_march}") 66 # Explicitly request ARM instead of THUMB for compilation. This option is not 67 # relevant on aarch64 68 if(NOT KernelSel4ArchAarch64) 69 string(APPEND c_common_flags " -marm") 70 endif() 71endif() 72if(KernelArchRiscV) 73 if(Kernel64) 74 string(APPEND c_common_flags " -march=rv64imac") 75 string(APPEND c_common_flags " -mabi=lp64") 76 else() 77 string(APPEND c_common_flags " -march=rv32ima") 78 string(APPEND c_common_flags " -mabi=ilp32") 79 endif() 80endif() 81string(APPEND common_flags " ${build_arch}") 82if(Kernel64) 83 string(APPEND common_flags " -D__KERNEL_64__") 84else() 85 string(APPEND common_flags " -D__KERNEL_32__") 86endif() 87 88set(BASE_ASM_FLAGS "${asm_common_flags} ${common_flags}" CACHE INTERNAL "Default ASM flags for compilation \ 89 (subset of flags used by the kernel build)" 90) 91set(BASE_C_FLAGS "${c_common_flags} ${common_flags}" CACHE INTERNAL "Default C flags for compilation \ 92 (subset of flags used by the kernel)" 93) 94set(BASE_CXX_FLAGS "${cxx_common_flags} ${c_common_flags} ${common_flags}" CACHE INTERNAL 95 "Default CXX flags for compilation" 96) 97if(KernelArchX86) 98 if(Kernel64) 99 string(APPEND common_exe_flags " -Wl,-m -Wl,elf_x86_64") 100 else() 101 string(APPEND common_exe_flags " -Wl,-m -Wl,elf_i386") 102 endif() 103endif() 104set(BASE_EXE_LINKER_FLAGS "${common_flags} ${common_exe_flags} " CACHE INTERNAL 105 "Default flags for linker an elf binary application" 106) 107# Initializing the kernel build flags starting from the same base flags that the users will use 108include(${KERNEL_FLAGS_PATH}) 109 110# Setup kernel specific flags 111macro(KernelCommonFlags) 112 foreach(common_flag IN ITEMS ${ARGV}) 113 add_compile_options(${common_flag}) 114 string(APPEND CMAKE_EXE_LINKER_FLAGS " ${common_flag} ") 115 endforeach() 116endmacro(KernelCommonFlags) 117KernelCommonFlags(-nostdinc -nostdlib ${KernelOptimisation} -DHAVE_AUTOCONF) 118if(KernelFWholeProgram) 119 KernelCommonFlags(-fwhole-program) 120endif() 121if(KernelDebugBuild) 122 KernelCommonFlags(-DDEBUG -g -ggdb) 123 # Pretend to CMake that we're a release build with debug info. This is because 124 # we do actually allow CMake to do the final link step, so we'd like it not to 125 # strip our binary 126 set(CMAKE_BUILD_TYPE "RelWithDebInfo") 127else() 128 set(CMAKE_BUILD_TYPE "Release") 129endif() 130if(KernelArchX86 AND Kernel64) 131 KernelCommonFlags(-mcmodel=kernel) 132endif() 133if(KernelArchARM) 134 if(KernelSel4ArchAarch64) 135 KernelCommonFlags(-mgeneral-regs-only) 136 else() 137 KernelCommonFlags(-mfloat-abi=soft) 138 endif() 139endif() 140if(KernelArchRiscV) 141 KernelCommonFlags(-mcmodel=medany) 142endif() 143KernelCommonFlags(-fno-pic -fno-pie) 144add_compile_options( 145 -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 146 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations 147 -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding 148) 149 150# Add all the common flags to the linker args 151string(APPEND CMAKE_EXE_LINKER_FLAGS " -ffreestanding -Wl,--build-id=none -static -Wl,-n ") 152 153if(KernelArchX86) 154 add_compile_options(-mno-mmx -mno-sse -mno-sse2 -mno-3dnow) 155endif() 156 157# Sort the C sources to ensure a stable layout of the final C file 158list(SORT c_sources) 159# Add the domain schedule now that its sorted 160list(APPEND c_sources "${KernelDomainSchedule}") 161 162# Add static header includes 163include_directories("include") 164include_directories("include/${KernelWordSize}") 165include_directories("include/arch/${KernelArch}") 166include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}/") 167include_directories("include/plat/${KernelPlatform}/") 168include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}/") 169include_directories("include/${KernelWordSize}/") 170 171if(KernelArchARM) 172 include_directories("include/arch/arm/armv/${KernelArmArmV}/") 173 include_directories("include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}") 174endif() 175if(KernelArmMach STREQUAL "exynos") 176 include_directories("include/plat/exynos_common/") 177endif() 178if(KernelArchRiscV) 179 include_directories("include/arch/${KernelArch}/arch/${KernelWordSize}") 180 include_directories("include/plat/${KernelPlatform}/plat/${KernelWordSize}") 181endif() 182 183################### 184# Config generation 185################### 186 187include_directories($<TARGET_PROPERTY:kernel_Config,INTERFACE_INCLUDE_DIRECTORIES>) 188# The kernel expects to be able to include an 'autoconf.h' file at the moment. So lets 189# generate one for it to use 190# TODO: use the kernel_Config directly 191generate_autoconf(kernel_autoconf "kernel") 192include_directories($<TARGET_PROPERTY:kernel_autoconf,INTERFACE_INCLUDE_DIRECTORIES>) 193 194# Target for the config / autoconf headers. This is what all the other generated headers 195# can depend upon 196add_custom_target(kernel_config_headers 197 DEPENDS kernel_autoconf_Gen kernel_autoconf kernel_Config kernel_Gen 198) 199 200# Target for all generated headers. We start with just all the config / autoconf headers 201add_custom_target(kernel_headers DEPENDS kernel_config_headers 202) 203 204# Build up a list of generated files. needed for dependencies in custom commands 205get_generated_files(gen_files_list kernel_autoconf_Gen) 206get_generated_files(gen_files2 kernel_Gen) 207list(APPEND gen_files_list "${gen_files2}") 208 209##################### 210# C source generation 211##################### 212 213# Kernel compiles all C sources as a single C file, this provides 214# rules for doing the concatenation 215 216add_custom_command(OUTPUT kernel_all.c 217 COMMAND "${CPP_GEN_PATH}" ${c_sources} > kernel_all.c 218 DEPENDS "${CPP_GEN_PATH}" ${c_sources} 219 COMMENT "Concatenating C files" 220 VERBATIM 221) 222 223add_custom_target(kernel_all_c_wrapper 224 DEPENDS kernel_all.c 225) 226 227################### 228# Header Generation 229################### 230 231# Rules for generating invocation and syscall headers 232# Aside from generating file rules for dependencies this section will also produce a target 233# that can be depended upon (along with the desired files themselves) to control parallelism 234 235set(xml_headers "") 236set(header_dest "gen_headers/arch/api/invocation.h") 237gen_invocation_header( 238 OUTPUT ${header_dest} 239 XML ${CMAKE_CURRENT_SOURCE_DIR}/libsel4/arch_include/${KernelArch}/interfaces/sel4arch.xml 240 ARCH 241) 242list(APPEND xml_headers "${header_dest}") 243list(APPEND gen_files_list "${header_dest}") 244 245set(header_dest "gen_headers/arch/api/sel4_invocation.h") 246gen_invocation_header( 247 OUTPUT "${header_dest}" 248 XML "${CMAKE_CURRENT_SOURCE_DIR}/libsel4/sel4_arch_include/${KernelSel4Arch}/interfaces/sel4arch.xml" 249 SEL4ARCH 250) 251list(APPEND xml_headers "${header_dest}") 252list(APPEND gen_files_list "${header_dest}") 253 254set(header_dest "gen_headers/api/invocation.h") 255gen_invocation_header( 256 OUTPUT "${header_dest}" 257 XML "${CMAKE_CURRENT_SOURCE_DIR}/libsel4/include/interfaces/sel4.xml" 258) 259list(APPEND xml_headers "${header_dest}") 260list(APPEND gen_files_list "${header_dest}") 261 262set(syscall_xml_base "${CMAKE_CURRENT_SOURCE_DIR}/include/api") 263set(syscall_dest "gen_headers/arch/api/syscall.h") 264add_custom_command(OUTPUT ${syscall_dest} 265 COMMAND "${XMLLINT_PATH}" --noout --schema "${syscall_xml_base}/syscall.xsd" "${syscall_xml_base}/syscall.xml" 266 COMMAND ${CMAKE_COMMAND} -E remove -f "${syscall_dest}" 267 COMMAND ${PYTHON} "${SYSCALL_ID_GEN_PATH}" --xml "${syscall_xml_base}/syscall.xml" --kernel_header "${syscall_dest}" 268 DEPENDS "${XMLLINT_PATH}" "${SYSCALL_ID_GEN_PATH}" "${syscall_xml_base}/syscall.xsd" "${syscall_xml_base}/syscall.xml" 269 COMMENT "Generate syscall invocations" 270 VERBATIM 271) 272list(APPEND xml_headers "${syscall_dest}") 273list(APPEND gen_files_list "${syscall_dest}") 274# Construct target for just the xml headers 275add_custom_target(xml_headers_target DEPENDS ${xml_headers}) 276# Add the xml headers to all the kernel headers 277add_dependencies(kernel_headers xml_headers_target) 278include_directories("${CMAKE_CURRENT_BINARY_DIR}/gen_headers") 279 280####################### 281# Prune list generation 282####################### 283 284# When generating bitfield files we can pass multiple '--prune' parameters that are source 285# files that get searched for determing which bitfield functions are used. This allows the 286# bitfield generator to only generate functions that are used. Whilst irrelevant for 287# normal compilation, not generating unused functions has significant time savings for the 288# automated verification tools 289 290# To generate a prune file we 'build' the kernel (similar to the kernel_all_pp.c rule 291# below) but strictly WITHOUT the generated header directory where the bitfield generated 292# headers are. This means our preprocessed file will contain all the code used by the 293# normal compilation, just without the bitfield headers (which we generate dummy versions of). 294# If we allowed the bitfield headers to be included then we would have a circular 295# dependency. As a result this rule comes *before* the Bitfield header generation section 296 297set(dummy_headers "") 298foreach(bf_dec ${bf_declarations}) 299 string(REPLACE ":" ";" bf_dec ${bf_dec}) 300 list(GET bf_dec 0 bf_file) 301 list(GET bf_dec 1 bf_gen_dir) 302 get_filename_component(bf_name "${bf_file}" NAME) 303 string(REPLACE ".bf" "_gen.h" bf_target "${bf_name}") 304 list(APPEND dummy_headers "${CMAKE_CURRENT_BINARY_DIR}/generated_prune/${bf_gen_dir}/${bf_target}") 305endforeach() 306 307add_custom_command(OUTPUT ${dummy_headers} 308 COMMAND ${CMAKE_COMMAND} -E touch ${dummy_headers} 309 COMMENT "Generate dummy headers for prune compilation" 310) 311 312add_custom_target(dummy_header_wrapper 313 DEPENDS ${dummy_headers} 314) 315 316CPPFile(kernel_all_pp_prune.c kernel_all_pp_prune_wrapper kernel_all.c 317 EXTRA_FLAGS -CC "-I${CMAKE_CURRENT_BINARY_DIR}/generated_prune" 318 EXTRA_DEPS kernel_all_c_wrapper dummy_header_wrapper xml_headers_target kernel_config_headers ${gen_files_list} 319) 320 321############################ 322# Bitfield header generation 323############################ 324 325# Need to generate a bunch of unique targets, we'll do this with piano numbers 326set(bf_gen_target "kernel_bf_gen_target_1") 327 328foreach(bf_dec ${bf_declarations}) 329 string(REPLACE ":" ";" bf_dec ${bf_dec}) 330 list(GET bf_dec 0 bf_file) 331 list(GET bf_dec 1 bf_gen_dir) 332 get_filename_component(bf_name "${bf_file}" NAME) 333 string(REPLACE ".bf" "_gen.h" bf_target "${bf_name}") 334 string(REPLACE ".bf" "_defs.thy" defs_target "${bf_name}") 335 string(REPLACE ".bf" "_proofs.thy" proofs_target "${bf_name}") 336 set(pbf_name "generated/${bf_gen_dir}/${bf_name}.pbf") 337 set(pbf_target "${bf_gen_target}_pbf") 338 CPPFile("${pbf_name}" "${pbf_target}" "${bf_file}" 339 EXTRA_FLAGS -P 340 EXTRA_DEPS kernel_config_headers ${gen_files_list} 341 ) 342 GenHBFTarget("" ${bf_gen_target} "generated/${bf_gen_dir}/${bf_target}" "${pbf_name}" "${pbf_target}" 343 "kernel_all_pp_prune.c" "kernel_all_pp_prune_wrapper") 344 GenDefsBFTarget("${bf_gen_target}_def" "generated/${bf_gen_dir}/${defs_target}" "${pbf_name}" "${pbf_target}" 345 "kernel_all_pp_prune.c" "kernel_all_pp_prune_wrapper") 346 GenProofsBFTarget("${bf_gen_target}_proof" "generated/${bf_gen_dir}/${proofs_target}" "${pbf_name}" "${pbf_target}" 347 "kernel_all_pp_prune.c" "kernel_all_pp_prune_wrapper") 348 list(APPEND theories_deps 349 "${bf_gen_target}_def" "${CMAKE_CURRENT_BINARY_DIR}/generated/${bf_gen_dir}/${defs_target}" 350 "${bf_gen_target}_proof" "${CMAKE_CURRENT_BINARY_DIR}/generated/${bf_gen_dir}/${proofs_target}" 351 ) 352 add_dependencies(kernel_headers "${bf_gen_target}") 353 list(APPEND gen_files_list "${CMAKE_CURRENT_BINARY_DIR}/generated/${bf_gen_dir}/${bf_target}") 354 set(bf_gen_target "${bf_gen_target}1") 355endforeach() 356# At this point we have generated a bunch of headers into ${CMAKE_CURRENT_BINARY_DIR}/generated 357# but we do not pass this to include_directories, as that will cause it to be an include directory 358# for *all* targets in this file (including ones we defined earlier) and the prune generation 359# *must not* see this files and generate dependencies on them as this will result in nonsense. 360# As such we must manually add this as an include directory to future targets 361set(CPPExtraFlags "-I${CMAKE_CURRENT_BINARY_DIR}/generated") 362 363#################### 364# Kernel compilation 365#################### 366 367CPPFile(kernel_all.i kernel_i_wrapper kernel_all.c 368 EXTRA_DEPS kernel_all_c_wrapper kernel_headers ${gen_files_list} 369 EXTRA_FLAGS -CC "${CPPExtraFlags}" 370 # The circular_includes script relies upon parsing out exactly 'kernel_all_copy.c' as 371 # a special case so we must ask CPPFile to use this input name 372 EXACT_NAME kernel_all_copy.c 373) 374 375# Explain to cmake that our object file is actually a C input file 376set_property(SOURCE kernel_all.i PROPERTY LANGUAGE C) 377 378set(linker_source "src/plat/${KernelPlatform}/linker.lds") 379set(linker_lds_path "${CMAKE_CURRENT_BINARY_DIR}/linker.lds_pp") 380CPPFile("${linker_lds_path}" linker_ld_wrapper "${linker_source}" 381 EXTRA_DEPS kernel_headers ${gen_files_list} 382 EXTRA_FLAGS -CC -P "${CPPExtraFlags}" 383) 384 385add_custom_command(OUTPUT circular_includes_valid 386 COMMAND ${CIRCULAR_INCLUDES} --ignore kernel_all_copy.c < kernel_all.i 387 COMMAND touch circular_includes_valid 388 DEPENDS kernel_i_wrapper kernel_all.i 389) 390 391add_custom_target(circular_includes 392 DEPENDS circular_includes_valid 393) 394 395add_custom_command(OUTPUT kernel_all_pp.c 396 COMMAND ${CMAKE_COMMAND} -E copy kernel_all.i kernel_all_pp.c 397 DEPENDS kernel_i_wrapper kernel_all.i 398) 399add_custom_target(kernel_all_pp_wrapper DEPENDS kernel_all_pp.c) 400 401add_custom_target(kernel_theories 402 DEPENDS ${theories_deps} 403) 404 405# Declare final kernel output 406add_executable(kernel.elf EXCLUDE_FROM_ALL ${asm_sources} kernel_all.i) 407target_include_directories(kernel.elf PRIVATE ${config_dir}) 408target_include_directories(kernel.elf PRIVATE include) 409target_include_directories(kernel.elf PRIVATE "${CMAKE_CURRENT_BINARY_DIR}/generated") 410target_link_libraries(kernel.elf PRIVATE kernel_Config kernel_autoconf) 411set_property(TARGET kernel.elf APPEND_STRING PROPERTY LINK_FLAGS " -T ${linker_lds_path} ") 412add_dependencies(kernel.elf linker_ld_wrapper kernel_i_wrapper kernel_all_pp_wrapper circular_includes) 413