Kconfig

#
# Copyright 2014, General Dynamics C4 Systems
#
# This software may be distributed and modified according to the terms of
# the GNU General Public License version 2. Note that NO WARRANTY is provided.
# See "LICENSE_GPLv2.txt" for details.
#
# @TAG(GD_GPL)
#

config KERNEL_PATH
    string
    option env="KERNEL_ROOT_PATH"

config ARCH_ARM_V6
    bool
    default n

config ARCH_ARM_V7A
    bool
    default n

config ARCH_ARM_V8A
    bool
    default n

config KERNEL_MASTER
    bool
    default y

# Native word size of the current platform. This is primarily intended for use
# in code generators that need to know, at generation-time, the word size of
# the target platform.
config WORD_SIZE
    int
    default 32 if ARCH_IA32 || ARCH_AARCH32

menu "seL4 System"

    choice
        prompt "Architecture Type"
        default ARCH_X86
        help
            Select the architecture seL4 will be running on.

        config ARCH_X86
            bool "x86"

        config ARCH_ARM
            bool "ARM"
    endchoice

    config ARCH_IA32
        bool
        default y if ARCH_X86

    config ARCH_AARCH32
        bool
        default y if ARCH_ARM

    # CPU values.

    config ARM1136JF_S
        bool
        default n

    config ARM_CORTEX_A7
        bool
        default n

    config ARM_CORTEX_A8 
        bool
        default n

    config ARM_CORTEX_A9
        bool
        default n

    config ARM_CORTEX_A15
        bool
        default n

    config ARM_CORTEX_A57
        bool
        default n

    config PLAT_EXYNOS54XX
       bool
       default n
       help
          Common flag for Exynos 5410 and 5422

    config PLAT_IMX6
       bool
       default n
       help
          Common flag for Sabre Lite and Wandboard Quad


    config PLAT_IMX7
        bool
        default n
            help
                Common flag for iMX7 SoC

    choice
        prompt "Platform Type"
        help
            Select the platform for the architecture

        config PLAT_KZM
            bool "KZM iMX.31 (ARMv6, ARM1136JF-S)"
            depends on ARCH_ARM
            select ARM1136JF_S
            select ARCH_ARM_V6
            help
                Support for the KZM platform

        config PLAT_OMAP3
            bool "OMAP3 (BeagleBoard, ARMv7a, Cortex A8)"
            depends on ARCH_ARM
            select ARM_CORTEX_A8
            select ARCH_ARM_V7A
            help
                Support for platforms based on OMAP3 SoCs.

        config PLAT_AM335X
            bool "AM335X (BeagleBone, ARMv7a, Cortex A8)"
            depends on ARCH_ARM
            select ARM_CORTEX_A8
            select ARCH_ARM_V7A
            help
                Support for AM335x platform (BeagleBone).

        config PLAT_EXYNOS4
            bool "EXYNOS4 (ODROID-X, ARMv7a, Cortex A9)"
            depends on ARCH_ARM
            select ARM_CORTEX_A9
            select ARCH_ARM_V7A
            help
                Support for EXYNOS4 platform (ODROID-X).

        config PLAT_EXYNOS5410
            bool "EXYNOS5410 (ODROID-XU, ARMv7a, Cortex A15)"
	    select PLAT_EXYNOS54XX
            depends on ARCH_ARM
            select ARM_CORTEX_A15
            select ARCH_ARM_V7A
            help
                Support for EXYNOS5410 platform (ODROID-XU).

        config PLAT_EXYNOS5422
            bool "EXYNOS5422 (ODROID-XU3, ARMv7a, Cortex A15)"
	    select PLAT_EXYNOS54XX
            depends on ARCH_ARM
            select ARM_CORTEX_A15
            select ARCH_ARM_V7A
            help
                Support for EXYNOS5422 platform (ODROID-XU3).

        config PLAT_EXYNOS5250
            bool "EXYNOS5250 (ARNDALE, ARMv7a, Cortex A15)"
            depends on ARCH_ARM
            select ARM_CORTEX_A15
            select ARCH_ARM_V7A
            help
                Support for EXYNOS5250 platform (ARNDALE).

        config PLAT_APQ8064
            bool "Qualcomm Snapdrogon S4 APQ8064 (Inforce IFC6410, ARMv7a, Cortex A15)"
            depends on ARCH_ARM
            select ARM_CORTEX_A15
            select ARCH_ARM_V7A
            help
                Support for Qualcomm Snapdragon S4 APQ8064 platforms (Inforce IFC6410).

        config PLAT_SABRE
            bool "iMX6 (Sabre Lite, ARMv7a, Cortex A9)"
            depends on ARCH_ARM
            select ARM_CORTEX_A9
            select ARCH_ARM_V7A
            select PLAT_IMX6
            help
                Support for iMX6 platform (Sabre Lite).

        config PLAT_WANDQ
            bool "iMX6 (Wandboard Quad, ARMv7a, Cortex A9)"
            depends on ARCH_ARM
            select ARM_CORTEX_A9
            select ARCH_ARM_V7A
            select PLAT_IMX6
            help
                Support for iMX6 platform (Wandboard Quad).

        config PLAT_IMX7_SABRE
            bool "iMX7 (Sabre, ARMv7a, Cortex A7)"
            depends on ARCH_ARM
            select ARM_CORTEX_A7
            select ARCH_ARM_V7A
            select PLAT_IMX7
            help
                Support for iMX7 Sabre Dual.

        config PLAT_ZYNQ7000
            bool "Zynq-7000 (Xilinx ZC706, ARMv7a, Cortex A9)"
            depends on ARCH_ARM
            select ARM_CORTEX_A9
            select ARCH_ARM_V7A
            help
                Support for Xilinx Zynq-7000 platforms.

        config PLAT_PC99
            bool "PC99"
            depends on ARCH_X86
            help
                Support for PC99 based platform

        config PLAT_ALLWINNERA20
            bool "ALLWINNERA20 (CUBIETRUCK, ARMv7a, Cortex A15)"
            depends on ARCH_ARM
            select ARM_CORTEX_A15
            select ARCH_ARM_V7A
            help
                Support for ALLWINNERA20 platform (CUBIETRUCK).

        config PLAT_TK1
            bool "Jetson (Tegra K1, ARMv7a, Cortex A15)"
            depends on ARCH_ARM
            select ARM_CORTEX_A15
            select ARCH_ARM_V7A
            help
                Support for Tegra K1 platform

        config PLAT_HIKEY
            bool "HiKey (ARMv8a, Cortex A57)"
            depends on ARCH_ARM
            select ARM_CORTEX_A57
            select ARCH_ARM_V8A
            help
                Support for HiKey platform.

    endchoice

    config ARM_HYPERVISOR_SUPPORT
        bool "Build as Hypervisor"
        depends on ARM_CORTEX_A15
        default n
        help
            Utilise ARM virtualisation extensions to build the kernel as a hypervisor

    config ARM_SMMU
        bool "Enable SystemMMU for Tegra K1 SoC"
        depends on PLAT_TK1
        default n
        help
            Support for TK1 SoC-specific SystemMMU

    config ARM_SMMU_VM_DEFAULT_MAPPING
        bool "Enable SystemMMU default mapping for guest VM"
        depends on PLAT_TK1 && ARM_SMMU && ARM_HYPERVISOR_SUPPORT
        default y
        help
            Enable the default translation for guest VM: all
            physical memory reserved for a VM is allowed to
            be accessed with read/write/nonsecure permissions.



source "$KERNEL_PATH/src/arch/arm/Kconfig"
source "$KERNEL_PATH/src/plat/pc99/Kconfig"

endmenu


menu "seL4 System Parameters"

    config ROOT_CNODE_SIZE_BITS
        range 4 27
        int "Root CNode Size (2^n slots)"
        default 12
        help
            The acceptable range is 4-27, based on the kernel-supplied caps.
            The root CNode needs at least enough space to contain up to
            BI_CAP_DYN_START. Note that in practice your root CNode will need
            to be several bits larger than 4 to fit device frame caps and
            cannot be 27 bits as it won't fit in memory.

    config TIMER_TICK_MS
        int "Timer tick period in milliseconds"
        default 2
        help
            The number of milliseconds between timer ticks.


    config TIME_SLICE
        int "Time slice"
        default 5
        help
            Number of timer ticks until a thread is preempted.

    config RETYPE_FAN_OUT_LIMIT
        int "Retype fan out limit"
        default 256
        help
            Maximum number of objects that can be created in a single Retype()
            invocation.

    config MAX_NUM_WORK_UNITS_PER_PREEMPTION
        int "Max work units per preemption"
        default 100
        help
            Maximum number of work units (delete/revoke iterations) until
            the kernel checks for pending interrupts (and preempts the
            currently running syscall if interrupts are pending).

    config MAX_NUM_BOOTINFO_DEVICE_REGIONS
        int "Max number of bootinfo device regions"
        default 199

    config MAX_NUM_BOOTINFO_UNTYPED_CAPS
        int "Max number of bootinfo untyped caps"
        default 167

    config MAX_RMRR_ENTRIES
        int "Max number of RMRR entries to support finding in ACPI"
        depends on IOMMU
        default 32
        help
            Sets the maximum number of Reserved Memory Region Reporting
            structures we support recording from the ACPI tables

    config FASTPATH
        bool "Enable fastpath"
        default y
        help
            Enable IPC fastpath

      config NUM_DOMAINS
        int "Number of domains"
        default 1
        help
            The number of scheduler domains in the system

    config DOMAIN_SCHEDULE
        string "Domain schedule"
        help
            A C file providing the symbols ksDomSchedule and
            ksDomScheduleLength to be linked with the kernel as a scheduling
            configuration.

    config NUM_PRIORITIES
        int "Number of priority levels"
        default 256
        range 1 256
        help
            The number of priority levels per domain

endmenu

menu "Build Options"
   
    config VERIFICATION_BUILD
        bool "Disable verification unfriendly features"
        default n
        help
            When enabled this configuration option prevents the usage of any other options that
            would compromise the verification story of the kernel. Enabling this option does NOT
            imply you are using a verified kernel.

    config DEBUG_BUILD
        bool "Enable debug facilities"
        depends on !VERIFICATION_BUILD
        default y
        help
            Enable debug facilities (symbols and assertions) in the kernel

    config PRINTING
        bool "Enable kernel printing"
        depends on !VERIFICATION_BUILD
        default y if DEBUG_BUILD
        help
            Allow the kernel to print out messages to the serial console during bootup and execution.

    config IRQ_REPORTING
        bool "Report spurious or undelivered IRQs"
        depends on PRINTING
        default y
        help
            seL4 does not properly check for and handle spurious interrupts
            This can result in unnecessary output from the kernel during
            debug builds. If you are CERTAIN these messages are benign
            then use this config to turn them off

    config COLOUR_PRINTING
        bool "Print error messages in colour"
        depends on PRINTING
        default y
        help
            In debug mode, seL4 prints diagnostic messages to its serial output
            describing, e.g., the cause of system call errors. This setting
            determines whether ANSI escape codes are applied to colour code
            these error messages. You may wish to disable this setting if your
            serial output is redirected to a file or pipe.

    config USER_STACK_TRACE_LENGTH
        int "Stack trace length"
        depends on PRINTING
        default 16
        help
            On a double fault the kernel can try and print out the users stack
            to aid debugging. This option determines how many words of stack
            should be printed

    choice
        prompt "Compiler optimisation flag"
        default OPTIMISATION_O2
        help
            Select the compiler optimisation level

        config OPTIMISATION_Os
            bool "-Os"
            help
                Compiler optimisations tuned for size

        config OPTIMISATION_O0
            bool "-O0"
            help
                No optimisation

        config OPTIMISATION_O1
            bool "-O1"
            help
                Basic compiler optimisations

        config OPTIMISATION_O2
            bool "-O2"
            help
                Aggressive compiler optimisations

        config OPTIMISATION_O3
            bool "-O3"
            help
                Enable all optimisations (may increase code size)

    endchoice

    config DANGEROUS_CODE_INJECTION
	    bool "Build kernel with support for executing arbitrary code in protected mode"
           depends on !ARM_HYPERVISOR_SUPPORT && !VERIFICATION_BUILD
        default n
        help
            Adds a system call that allows users to specify code to be run in kernel
            mode. Useful for profiling.

    config DANGEROUS_CODE_INJECTION_ON_UNDEF_INSTR
        bool "Make undefined instructions execute code in protected mode"
        depends on ARCH_ARM_V6 && !VERIFICATION_BUILD
        default n
        help
            Replaces the undefined instruction handler with a call to a function
            pointer in r8. This is an alternative mechanism to the code
            injection syscall. On ARMv6 the syscall interferes with the caches
            and branch predictor in such a way that it is unsuitable for
            benchmarking. This option has no effect on non-ARMv6 platforms.

    config DEBUG_DISABLE_L2_CACHE
        bool "Disable L2 cache"
        depends on ARCH_ARM
        default n
        help
            Do not enable the L2 cache on startup for debugging purposes.

    config DEBUG_DISABLE_L1_ICACHE
        bool "Disable L1 instruction cache"
        depends on ARCH_ARM && DEBUG_DISABLE_L2_CACHE
        default n
        help
            Do not enable the L1 instruction cache on startup for debugging purposes.

    config DEBUG_DISABLE_L1_DCACHE
        bool "Disable L1 data cache"
        depends on ARCH_ARM && DEBUG_DISABLE_L2_CACHE
        default n
        help
            Do not enable the L1 data cache on startup for debugging purposes.

    config DEBUG_DISABLE_BRANCH_PREDICTION
        bool "Disable branch prediction"
        depends on ARCH_ARM
        default n
        help
            Do not enable branch prediction (also called program flow control)
            on startup. This makes execution time more deterministic at the
            expense of dramatically decreasing performance. Primary use is for
            debugging.

    config DEBUG_DISABLE_PREFETCHERS
        bool "Disable prefetchers"
        depends on ARCH_IA32
        default n
        help
            On ia32 platforms, this option disables the L2 hardware prefetcher, the L2 
            adjacent cache line prefetcher, the DCU prefetcher and the DCU IP prefetcher.
            Currently unimplemented on other platforms.

    config ENABLE_BENCHMARKS
        bool
        default n

    config ARM_ENABLE_PMU_OVERFLOW_INTERRUPT
        bool
        depends on BENCHMARK_TRACK_UTILISATION && ARCH_ARM
        default y

    config BENCHMARK_USE_KERNEL_LOG_BUFFER
        bool
        depends on BENCHMARK_TRACK_KERNEL_ENTRIES || BENCHMARK_TRACEPOINTS
        default y

    choice
        prompt "Enable benchmarks"
        depends on !VERIFICATION_BUILD
        default NO_BENCHMARKS
        help
            Enable benchamrks including logging and tracing info.
            Setting this value > 1 enables a 1MB log buffer and functions for extracting data from it
            at user level.
            NOTE this is only tested on the sabre and will not work on platforms with < 512mb memory.
            This is not fully implemented for x86.


        config NO_BENCHMARKS
             bool "No benchmarking features enabled"

        config BENCHMARK_TRACK_KERNEL_ENTRIES
            bool "Keep track of kernel entries"
            select ENABLE_BENCHMARKS
            help
                Log kernel entries information including timing, number of invocations and arguments for
                system calls, interrupts, user faults and VM faults.

        config BENCHMARK_TRACEPOINTS
            bool "Use trace points"
            select ENABLE_BENCHMARKS
            help
                 Enable manually inserted tracepoints that the kernel will track time consumed between.

        config BENCHMARK_TRACK_UTILISATION
            bool "Track threads and kernel utilisation time"
            select ENABLE_BENCHMARKS
            help
                Enable the kernel to track each thread's utilisation time.

     endchoice

     config MAX_NUM_TRACE_POINTS
            int "Maximum number of tracepoints"
            depends on BENCHMARK_TRACEPOINTS
            default 1
            help
                Use TRACE_POINT_START(k) and TRACE_POINT_STOP(k) macros for recording data,
                where k is an integer between 0 and this value - 1.
                The maximum number of different trace point identifiers which can be used.


endmenu

menu "Errata"

    config ARM_ERRATA_430973
        bool "Enable workaround for 430973 Cortex-A8 (r1p0..r1p2) erratum"
        depends on ARCH_ARM
        depends on ARM_CORTEX_A8
        default n
        help
            Enables a workaround for the 430973 Cortex-A8 (r1p0..r1p2) erratum. Error occurs
            if code containing ARM/Thumb interworking branch is replaced by different code
            at the same virtual address.

    config ARM_ERRATA_773022
        bool "Enable workaround for 773022 Cortex-A15 (r0p0..r0p4) erratum"
        depends on ARCH_ARM
        depends on ARM_CORTEX_A15
        default y
        help
            Enables a workaround for the 773022 Cortex-A15 (r0p0..r0p4) erratum. Error occurs
            on rare sequences of instructions and results in the loop buffer delivering
            incorrect instructions. The work around is to disable the loop buffer

endmenu