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