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