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