The seL4 microkernel https://sel4.systems/

CMakeLists.txt 16KB

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