Kbuild: Removed Kbuild

Removed all Kbuild/Kconfig/Makefiles from the kernel as we migrate to a CMake only build system. Kbuild is no longer supported.
2018-07-02 15:55:12 +10:00 · 2018-07-02 15:55:12 +10:00 · 72e675f1da
commit 72e675f1da
parent 4c265f369e
144 changed files with 0 additions and 4329 deletions
--- a/791
+++ b/791
@ -1,791 +0,0 @@
-#
-# 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 HAVE_FPU
-    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 || ARCH_RISCV_RV32
-    default 64 if ARCH_X86_64 || ARCH_AARCH64 || ARCH_RISCV_RV64
-
-menu "seL4 System"
-
-    choice
-        prompt "Architecture Type"
-        default ARCH_X86
-        help
-            Select the architecture seL4 will be running on.
-
-        config ARCH_X86
-            select HAVE_FPU
-            bool "x86"
-
-        config ARCH_ARM
-            bool "ARM"
-
-        config ARCH_RISCV
-            bool "RISCV"
-
-    endchoice
-
-    config ARCH_X86_64
-        bool "64-bit kernel"
-        default n
-        depends on ARCH_X86
-
-    config ARCH_AARCH64
-        bool "64-bit kernel"
-        default n
-        depends on ARCH_ARM
-
-    config ARCH_IA32
-        bool
-        default y if !ARCH_X86_64 && ARCH_X86
-
-    config ARCH_AARCH32
-        bool
-        default y if !ARCH_AARCH64 && 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_A53
-        bool
-        default n
-
-    config ARM_CORTEX_A57
-        bool
-        default n
-
-    config PLAT_EXYNOS5
-        bool
-        default n
-        help
-            Common flag for Exynos5 platforms
-
-    choice
-       prompt "RISC-V CPU selection"
-       depends on ARCH_RISCV
-       default ARCH_RISCV_RV64
-       help
-            Select the RISC-V CPU Implementation
-
-        config ARCH_RISCV_RV64
-            bool "RISCV RV64"
-            help
-                Support for RV64 (RISC-V 64-bit)
-
-        config ARCH_RISCV_RV32
-            bool "RISCV RV32"
-            depends on PT_LEVELS = 2
-            help
-                Support for RV32 (RISC-V 32-bit). Only 2 levels PT is supported
-                for RV32
-    endchoice
-
-    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_AARCH32
-            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_AARCH32
-            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_AARCH32
-            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_AARCH32
-            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)"
-            depends on ARCH_AARCH32
-            select PLAT_EXYNOS54XX
-            select PLAT_EXYNOS5
-            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)"
-            depends on ARCH_AARCH32
-            select PLAT_EXYNOS54XX
-            select PLAT_EXYNOS5
-            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_AARCH32
-            select PLAT_EXYNOS5
-            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_AARCH32
-            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_AARCH32
-            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_AARCH32
-            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_AARCH32
-            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_AARCH32
-            select ARM_CORTEX_A9
-            select ARCH_ARM_V7A
-            help
-                Support for Xilinx Zynq-7000 platforms.
-
-        config PLAT_ZYNQMP
-            bool "Zynq UltraScale+ MPSoC (Xilinx ZCU102, ARMv8a, Cortex A53)"
-            depends on ARCH_ARM
-            select ARM_CORTEX_A53
-            select ARCH_ARM_V8A
-            select HAVE_FPU if ARCH_AARCH64
-            help
-                Support for Xilinx Zynq UltraScale+ MPSoC 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_AARCH32
-            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_AARCH32
-            select ARM_CORTEX_A15
-            select ARCH_ARM_V7A
-            help
-                Support for Tegra K1 platform
-
-        config PLAT_HIKEY
-            bool "HiKey (Hi6220, ARMv8a, Cortex A53)"
-            depends on ARCH_ARM
-            select ARM_CORTEX_A53
-            select ARCH_ARM_V8A
-            select HAVE_FPU if ARCH_AARCH64
-            help
-                Support for HiKey platform.
-
-        config PLAT_BCM2837
-            bool "Raspberry Pi 3 (BCM2837, ARMv8a, Cortex A53)"
-            depends on ARCH_AARCH32
-            select ARM_CORTEX_A53
-            select ARCH_ARM_V8A
-            help
-                Support for Raspberry PI 3 platform.
-
-        config PLAT_TX1
-            bool "Jetson (Tegra X1, ARMv8a, Cortex A57)"
-            depends on ARCH_AARCH64
-            select ARM_CORTEX_A57
-            select ARCH_ARM_V8A
-            select HAVE_FPU
-            help
-                Support for Tegra X1 platform
-
-        config PLAT_SPIKE
-            bool "PLAT_SPIKE"
-            depends on ARCH_RISCV
-            help
-                Support for spike 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
-
-source "$KERNEL_PATH/src/arch/riscv/Kconfig"
-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 untyped 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 RESET_CHUNK_BITS
-        int "Max chunks to reset when clearing memory"
-        default 8
-        help
-            Maximum size in bits of chunks of memory to zero before checking a preemption point.
-
-    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
-
-    config MAX_NUM_NODES
-        int "Max number of CPU nodes"
-        depends on NUM_DOMAINS = 1 && !ARCH_RISCV
-        range 1 256
-        default 1
-        help
-            The number of CPU cores to boot
-    config MAX_NUM_NODES
-        depends on ARCH_RISCV
-        default 1
-
-    config CACHE_LN_SZ
-        int "Cache line size"
-        depends on ARCH_X86
-        default 64
-        help
-            Define cache line size for the current architecture
-
-    config KERNEL_STACK_BITS
-        int "Kernel stack size bits"
-        default 12
-        help
-            This describes the log2 size of the kernel stack. Great care should
-            be taken as there is no guard below the stack so setting this too
-            small will cause random memory corruption
-
-config AARCH32_FPU_ENABLE_CONTEXT_SWITCH
-    bool "Enable hardware VFP and SIMD context switch"
-    depends on ARCH_AARCH32 && !ARCH_ARM_V6 && !VERIFICATION_BUILD 
-    select HAVE_FPU
-    default y
-    help
-        This enables the VFP and SIMD context switch on platforms with
-        hardware support, allowing the user to execute hardware VFP and SIMD
-        operations in a multithreading environment, instead of relying on
-        software emulation of FPU/VFP from the C library (e.g. mfloat-abi=soft).
-
-config RISCV_FPU_ENABLE_CONTEXT_SWITCH
-    bool "Enable hardware FPU"
-    depends on ARCH_RISCV
-    select HAVE_FPU
-    default n
-    help
-        This enables FPU, if HW supports it
-
-config FPU_MAX_RESTORES_SINCE_SWITCH
-    int "Max thread restores without switching FPU"
-    depends on HAVE_FPU
-    default 64
-    help
-        This option is a heuristic to attempt to detect when the FPU is no
-        longer in use, allowing the kernel to save the FPU state out so that
-        the FPU does not have to be enabled/disabled every thread swith. Every
-        time we restore a thread and there is active FPU state, we increment
-        this setting and if it exceeds this threshold we switch to the NULL
-        state.
-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 HARDWARE_DEBUG_API
-        bool "Enable hardware breakpoint and single-stepping API"
-        depends on !VERIFICATION_BUILD
-        default n
-        help
-            Builds the kernel with support for a userspace debug API, which can
-            allows userspace processes to set breakpoints, watchpoints and to
-            single-step through thread execution.
-
-    config ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE
-        bool "Trap, but don't save/restore VCPUs' CP14 accesses"
-        depends on ARM_HYPERVISOR_SUPPORT && !VERIFICATION_BUILD
-        default y
-        help
-            This allows us to turn off the save and restore of VCPU threads' CP14
-            context for performance (or other) reasons, we can just turn them off
-            and trap them instead, and have the VCPUs' accesses to CP14
-            intercepted and delivered to the VM Monitor as fault messages.
-
-    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 && !PLAT_HIKEY && !KERNEL_SKIM_WINDOW
-        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 && !HAVE_FPU
-        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_X86 || PLAT_HIKEY
-        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.
-            On the cortex a53 this disables the L1 Data prefetcher.
-
-    config ARM_HIKEY_OUTSTANDING_PREFETCHERS
-        int "Number of outstanding prefetch allowed"
-        default 5
-        range 1 7
-        depends on PLAT_HIKEY && !DEBUG_DISABLE_PREFETCHERS
-        help
-            Cortex A53 has an L1 Data prefetcher. This config options allows 
-            the number of outstanding prefetcher to be set from a number from
-            1 to 7. Note that a setting of 7 maps to 8 and 5 is the reset value.
-
-    config ARM_HIKEY_PREFETCHER_STRIDE
-        int "Number of strides before prefetcher is triggered"
-        default 2
-        range 2 3
-        depends on PLAT_HIKEY && !DEBUG_DISABLE_PREFETCHERS
-        help
-            Number of strides before prefetcher is triggered.
-            Allowed values are 2 and 3. 2 is the reset value
-
-    config ARM_HIKEY_PREFETCHER_NPFSTRM
-        int "Number of indepedent prefetch streams"
-        default 2
-        range 1 4
-        depends on PLAT_HIKEY && !DEBUG_DISABLE_PREFETCHERS
-        help
-            Number of indepedent prefetch streams. Allowed values are 1 to 4.
-            2 is the reset value
-
-    config ARM_HIKEY_PREFETCHER_STBPFDIS
-        bool "Enable prefetch streams initated by STB access"
-        default y
-        depends on PLAT_HIKEY && !DEBUG_DISABLE_PREFETCHERS
-        help
-            Enable prefetch streams initated by STB access. Enabled is the reset value
-
-    config ARM_HIKEY_PREFETCHER_STBPFRS
-        bool "Prefetcher to initated on a ReadUnique or ReadShared"
-        default n
-        depends on PLAT_HIKEY && !DEBUG_DISABLE_PREFETCHERS
-        help
-            Sets prefetcher to initated on a ReadUnique (n) or ReadShared (y)
-            ReadUnique is the reset value
-
-    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_GENERIC
-            bool "Enable generic benchmarks"
-            select ENABLE_BENCHMARKS
-            help
-                Enable global benchmarks config variable with no specific features
-
-        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
--- a/802
+++ b/802
@ -1,802 +0,0 @@
-#
-# 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)
-#
-
-# Disable built-in rules.
-.SUFFIXES:
-
-############################################################
-### Build parameters
-############################################################
-
-SEL4_ARCH_LIST:=aarch32 aarch64 ia32 x86_64 riscv32 riscv64
-ARCH_LIST:=arm x86 riscv
-CPU_LIST:=arm1136jf-s ixp420 cortex-a7 cortex-a8 cortex-a9 cortex-a15 cortex-a53 cortex-a57
-PLAT_LIST:=imx31 pc99 ixp420 omap3 am335x exynos4 exynos5 imx6 imx7 apq8064 zynq7000 zynqmp allwinnerA20 tk1 hikey bcm2837 tx1 spike
-ARMV_LIST:=armv6 armv7-a armv8-a
-
-ifndef SOURCE_ROOT
-    # Assume we're in the source directory if not specified.
-    SOURCE_ROOT=.
-    export SOURCE_ROOT
-endif
-
-# The if statements below check to see if the make target doesn't require
-# values for the ARCH, PLAT, or SEL4_ARCH variables.
-ifneq (${MAKECMDGOALS},)
-ifeq (${MAKECMDGOALS}, $(filter ${MAKECMDGOALS}, style astyle xmllint pylint))
-# Pick an arbitrary value for ARCH, PLAT, and SEL4_ARCH to placate
-# other rules that depend on them being defined.
-ARCH:=x86
-PLAT:=pc99
-SEL4_ARCH:=ia32
-endif
-endif
-
-# we do need them if we want to build anything else
-$(if $(filter ${ARCH},${ARCH_LIST}),, \
-	$(error ARCH ${ARCH} invalid or undefined, should be one of [${ARCH_LIST}]))
-
-$(if $(filter ${PLAT},${PLAT_LIST}),, \
-	$(error PLAT ${PLAT} invalid or undefined, should be one of [${PLAT_LIST}]))
-
-ifeq (${ARCH}, riscv)
-ifeq (${KERNEL_32}, y)
-TYPE_SUFFIX:=32
-SEL4_ARCH:=riscv32
-else
-TYPE_SUFFIX:=64
-SEL4_ARCH:=riscv64
-endif
-endif
-
-ifeq (${ARCH}, arm)
-$(if $(filter ${CPU},${CPU_LIST}),, \
-	$(error CPU ${CPU} invalid or undefined, should be one of [${CPU_LIST}]))
-
-$(if $(filter ${ARMV},${ARMV_LIST}),, \
-	$(error ARMV ${ARMV} invalid or undefined, should be one of [${ARMV_LIST}]))
-ifneq (${SEL4_ARCH}, aarch64)
-SEL4_ARCH:=aarch32
-endif
-endif
-
-$(if $(filter ${SEL4_ARCH},${SEL4_ARCH_LIST}),, \
-    $(error SEL4_ARCH ${SEL4_ARCH} invalid or undefined, should be one of [${SEL4_ARCH_LIST}]))
-
-# If no domain configuration file was specified, use a default
-# configuration of just a single domain.
-ifeq (${CONFIG_DOMAIN_SCHEDULE},)
-DOMAIN_CONFIG_FILE=${SOURCE_ROOT}/src/config/default_domain.c
-else
-DOMAIN_CONFIG_FILE=$(wildcard ${CONFIG_DOMAIN_SCHEDULE})
-ifeq ($(DOMAIN_CONFIG_FILE),)
-$(error Domain schedule, ${CONFIG_DOMAIN_SCHEDULE}, does not exist)
-endif
-endif
-
-### Verbose building
-########################################
-
-# Set V=1 for verbose building, this can be passed in on the command line
-# Set V=2 to have make echo out commands before executing them
-
-ifeq ($V, 1)
-	BUILD_VERBOSE = 1
-	MAKE_SILENT = -s
-	quiet = 
-	Q =
-else
-ifeq ($V, 2)
-	BUILD_VERBOSE = 1
-	MAKE_SILENT =
-	quiet =
-	Q =
-else
-ifeq ($V, 3)
-	BUILD_VERBOSE = 1
-	MAKE_SILENT =
-	quiet =
-	Q =
-else
-	MAKE_SILENT = -s
-	quiet = quiet_
-	Q = @
-endif
-endif
-endif
-
-### Benchmarking parameters
-########################################
-
-CONFIG_DEFS=
-
-ifdef BENCHMARK_PROFILER
-CONFIG_DEFS += PROFILER
-ifdef CHECKPOINT_PROFILER
-CONFIG_DEFS += CHECKPOINT_PROFILER
-endif # CHECKPOINT_PROFILER
-else
-CONFIG_DEFS = CYCLE_COUNTER
-endif # BENCHMARK_PROFILER
-
-ifdef BENCHMARK_ICACHE
-CONFIG_DEFS += PERF_COUNTER=ARM_INSTRUCTION_CACHE_MISS
-else
-ifdef BENCHMARK_DCACHE
-CONFIG_DEFS += PERF_COUNTER=ARM_DATA_CACHE_MISS
-else
-CONFIG_DEFS += PERF_COUNTER=CYCLE_COUNTER
-endif # BENCHMARK_DCACHE
-endif # BENCHMARK_ICACHE
-
-ifdef IOMMU
-CONFIG_DEFS += CONFIG_IOMMU
-endif
-
-CONFIG_DEFS += $(strip $(foreach var, \
-  CONFIG_ROOT_CNODE_SIZE_BITS \
-  CONFIG_TIME_SLICE \
-  CONFIG_NUM_DOMAINS \
-  CONFIG_NUM_PRIORITIES \
-  CONFIG_RETYPE_FAN_OUT_LIMIT \
-  CONFIG_MAX_NUM_WORK_UNITS_PER_PREEMPTION \
-  CONFIG_MAX_NUM_BOOTINFO_DEVICE_REGIONS \
-  CONFIG_MAX_NUM_BOOTINFO_UNTYPED_CAPS \
-  CONFIG_TIMER_TICK_MS, \
-  $(if $(value ${var}), ${var}=$(value ${var}), )))
-
-ifdef BUILD_VERBOSE
-$(info seL4 build options:)
-$(info ===================)
-$(info ARCH          = ${ARCH})
-$(info PLAT          = ${PLAT})
-$(info CPU           = ${CPU})
-$(info TOOLPREFIX    = ${TOOLPREFIX})
-$(info PATH          = ${PATH})
-$(info DEBUG         = ${DEBUG})
-$(info ASSERT        = ${ASSERT})
-$(info CONFIG_DEFS   = ${CONFIG_DEFS})
-$(info DANGEROUS_CODE_INJECTION = ${DANGEROUS_CODE_INJECTION})
-endif
-
-.PHONY: all default clean preprocess validate
-
-default: all
-
-############################################################
-### Tool setup
-############################################################
-
-PATH := ${SOURCE_ROOT}/tools:${PATH}
-export PATH
-
-PARSER = c-parser
-
-CC =
-# Allow manually specifying a compiler.
-ifdef CONFIG_KERNEL_COMPILER
-ifneq (${CONFIG_KERNEL_COMPILER},)
-ifneq (${CONFIG_KERNEL_COMPILER},"")
-CC = ${CONFIG_KERNEL_COMPILER}
-# Assume that this is a non-GNU compiler.
-CPPFLAGS += -U__GNUC__
-endif
-endif
-endif
-ifeq (${CC},)
-CC = ${TOOLPREFIX}gcc
-endif
-
-ifeq (${PYTHON},)
-PYTHON = python
-# Suppress python bytecode (pyc) files for build thread safety
-export PYTHONDONTWRITEBYTECODE = true
-endif
-
-# Allow manually appending CPP flags.
-ifneq (${CONFIG_KERNEL_EXTRA_CPPFLAGS},)
-ifneq (${CONFIG_KERNEL_EXTRA_CPPFLAGS},"")
-CPPFLAGS += ${CONFIG_KERNEL_EXTRA_CPPFLAGS}
-endif
-endif
-
-CPP = ${TOOLPREFIX}cpp
-AS = ${TOOLPREFIX}as
-LD = ${TOOLPREFIX}ld
-STRIP = ${TOOLPREFIX}strip
-BF_GEN_PATH = ${SOURCE_ROOT}/tools/bitfield_gen.py
-CHANGED = ${SOURCE_ROOT}/tools/changed.sh
-CPP_GEN = ${SOURCE_ROOT}/tools/cpp_gen.sh
-SYSCALL_ID_GEN_PATH = ${SOURCE_ROOT}/tools/syscall_header_gen.py
-INVOCATION_ID_GEN_PATH = ${SOURCE_ROOT}/tools/invocation_header_gen.py
-XMLLINT = xmllint.sh
-CIRCULAR_INCLUDES = ${SOURCE_ROOT}/tools/circular_includes.py
-
-########################################
-## Check tools
-########################################
-
-ifdef BUILD_VERBOSE
-$(info CC            = ${CC})
-$(info CC_PATH       = ${CC_PATH})
-$(info CPP           = ${CPP})
-$(info CPP_PATH      = ${CPP_PATH})
-$(info AS            = ${AS})
-$(info AS_PATH       = ${AS_PATH})
-$(info LD            = ${LD})
-$(info LD_PATH       = ${LD_PATH})
-$(info PARSER        = ${PARSER})
-$(info PARSER_PATH   = ${PARSER_PATH})
-$(info BF_GEN_PATH   = ${BF_GEN_PATH})
-$(info SYSCALL_ID_GEN_PATH = ${SYSCALL_ID_GEN_PATH})
-$(info INVOCATION_ID_GEN_PATH = ${INVOCATION_ID_GEN_PATH})
-$(info XMLLINT_PATH  = ${XMLLINT_PATH})
-$(info XMLLINT       = ${XMLLINT})
-endif
-
-ifndef SKIP_PATH_CHECKS
-
-CC_PATH = $(shell PATH=${PATH} sh -c "which ${CC}")
-$(if ${CC_PATH},,$(error ${CC} not in PATH or not executable))
-
-CPP_PATH = $(shell PATH=${PATH} sh -c "which ${CPP}")
-$(if ${CPP_PATH},,$(error ${CPP} not in PATH or not executable))
-
-AS_PATH = $(shell PATH=${PATH} sh -c "which ${AS}")
-$(if ${AS_PATH},,$(error ${AS} not in PATH or not executable))
-
-LD_PATH = $(shell PATH=${PATH} sh -c "which ${LD}")
-$(if ${LD_PATH},,$(error ${LD} not in PATH or not executable))
-
-STRIP_PATH = $(shell PATH=${PATH} sh -c "which ${STRIP}")
-$(if ${STRIP_PATH},,$(error ${STRIP} not in PATH or not executable))
-
-PYTHON_PATH = $(shell PATH=${PATH} sh -c "which ${PYTHON}")
-$(if ${PYTHON_PATH},,$(error ${PYTHON} not in PATH or not executable))
-
-XMLLINT_PATH = $(shell PATH=${PATH} sh -c "which ${XMLLINT}")
-$(if ${XMLLINT_PATH},,$(error ${XMLLINT} not in PATH or not executable))
-endif
-
-ifeq ($(SORRY_BITFIELD_PROOFS),1)
-    SORRY_ARG:=--sorry_lemmas
-else
-    SORRY_ARG:=
-endif
-
-# If a parent Makefile has passed us DEFINES, assume they will be missing -D.
-DEFINES := ${DEFINES:%=-D%}
-
-INCLUDES = ${INCLUDE_DIRS:%=-I%}
-DEFINES += ${CONFIG_DEFS:%=-D%}
-
-ifdef DEBUG
-DEFINES += -DDEBUG
-CFLAGS  += -ggdb -g3
-endif
-
-ifdef DANGEROUS_CODE_INJECTION
-DEFINES += -DDANGEROUS_CODE_INJECTION
-endif
-
-ifdef ASSERT
-DEFINES += -DASSERT
-endif
-
-ifdef FASTPATH
-DEFINES += -DFASTPATH
-endif
-
-# Only set CFLAGS if we're building standalone.
-# common/Makefile.Flags sets NK_CFLAGS  in Kbuild environments.
-ifndef NK_CFLAGS
-STATICHEADERS += ${SOURCE_ROOT}/configs/$(PLAT)/autoconf.h
-INCLUDES += "-I${SOURCE_ROOT}/configs/$(PLAT)"
-DEFINES += -DHAVE_AUTOCONF
-ifdef DEBUG
-DEFINES += -DCONFIG_DEBUG_BUILD
-DEFINE  += -DCONFIG_PRINTING
-DEFINES += -DCONFIG_USER_STACK_TRACE_LENGTH=1
-endif
-ifeq (${ARCH}, arm)
-CFLAGS += -mtune=${CPU} -marm -march=${ARMV}
-ASFLAGS += -Wa,-mcpu=${CPU} -Wa,-march=${ARMV}
-DEFINES += -D$(shell echo ${ARMV}|tr [:lower:] [:upper:]|tr - _)
-DEFINES += -DARCH_ARM
-ifeq (${SEL4_ARCH}, aarch32)
-DEFINES += -D__KERNEL_32__ -DAARCH32
-TYPE_SUFFIX:=32
-export __ARM_32__ = y
-ifeq (${CPU},cortex-a7)
-DEFINES += -DARM_CORTEX_A7
-endif
-ifeq (${CPU},cortex-a8)
-DEFINES += -DARM_CORTEX_A8
-endif
-ifeq (${CPU},cortex-a9)
-DEFINES += -DARM_CORTEX_A9
-endif
-ifeq (${CPU},cortex-a15)
-DEFINES += -DARM_CORTEX_A15
-endif
-ifeq ($(PLAT),imx6)
-DEFINES += -DIMX6
-endif
-ifeq ($(PLAT),imx7)
-DEFINES += -DIMX7
-endif
-ifeq ($(PLAT),imx31)
-DEFINES += -DIMX31
-endif
-ifeq ($(PLAT),pc99)
-DEFINES += -DPC99
-endif
-ifeq ($(PLAT),ixp420)
-DEFINES += -DIXP420
-endif
-ifeq ($(PLAT),omap3)
-DEFINES += -DOMAP3
-endif
-ifeq ($(PLAT),am335x)
-DEFINES += -DAM335X
-endif
-ifeq ($(PLAT),exynos4)
-DEFINES += -DEXYNOS4
-endif
-ifeq ($(PLAT),exynos5)
-DEFINES += -DEXYNOS5
-endif
-ifeq ($(PLAT),apq8064)
-DEFINES += -DAPQ8064
-endif
-ifeq ($(PLAT),zynq7000)
-DEFINES += -DZYNQ7000
-endif
-ifeq ($(PLAT),zynqmp)
-DEFINES += -DZYNQMP
-endif
-ifeq ($(PLAT),allwinnerA20)
-DEFINES += -DALLWINNERA20
-endif
-ifeq ($(PLAT),bcm2837)
-DEFINES += -DBCM2837
-endif
-endif # SEL4_ARCH=aarch32
-ifeq (${SEL4_ARCH}, aarch64)
-DEFINES += -D__KERNEL_64__ -DAARCH64
-TYPE_SUFFIX:=64
-export __ARM_64__ = y
-endif # SEL4_ARCH=aarch64
-ifeq (${CPU},cortex-a53)
-DEFINES += -DARM_CORTEX_A53
-endif
-ifeq ($(PLAT),hikey)
-DEFINES += -DHIKEY
-endif
-endif # ARCH=arm
-ifeq (${SEL4_ARCH}, x86_64)
-CFLAGS += -m64 -fno-asynchronous-unwind-tables
-ASFLAGS += -Wa,--64
-DEFINES += -DARCH_X86 -DX86_64 -DCONFIG_X86_64=y -D__KERNEL_64__ -DKERNEL_64=y -D__X86_64__=y
-export __X86_64__ = y
-TYPE_SUFFIX:=64
-endif
-ifeq (${SEL4_ARCH}, ia32)
-CFLAGS += -m32
-ASFLAGS += -Wa,--32
-DEFINES += -DARCH_IA32 -DARCH_X86 -DX86_32 -D__KERNEL_32__
-LDFLAGS += -Wl,-m,elf_i386
-TYPE_SUFFIX:=32
-export __X86_32__ = y
-endif
-else # NK_CFLAGS
-# Require autoconf to be provided if larger build
-$(if ${HAVE_AUTOCONF},,$(error autoconf.h not provided))
-STATICHEADERS += $(srctree)/include/generated/autoconf.h
-endif # NK_CFLAGS
-
-ifeq (${SEL4_ARCH}, ia32)
-INCLUDES += "-I${SOURCE_ROOT}/include/arch/$(ARCH)/arch/32"
-INCLUDES += "-I${SOURCE_ROOT}/include/plat/$(PLAT)/plat/32"
-else
-ifeq ($(SEL4_ARCH), x86_64)
-INCLUDES += "-I${SOURCE_ROOT}/include/arch/$(ARCH)/arch/64"
-INCLUDES += "-I${SOURCE_ROOT}/include/plat/$(PLAT)/plat/64"
-endif
-endif
-
-ifeq ($(SEL4_ARCH), aarch32)
-INCLUDES += "-I${SOURCE_ROOT}/include/arch/$(ARCH)/arch/32"
-INCLUDES += "-I${SOURCE_ROOT}/include/plat/$(PLAT)/plat/32"
-else
-ifeq ($(SEL4_ARCH), aarch64)
-INCLUDES += "-I${SOURCE_ROOT}/include/arch/$(ARCH)/arch/64"
-INCLUDES += "-I${SOURCE_ROOT}/include/plat/$(PLAT)/plat/64"
-endif
-ifeq ($(ARCH), riscv)
-INCLUDES += "-I${SOURCE_ROOT}/include/arch/$(ARCH)/arch/$(TYPE_SUFFIX)"
-INCLUDES += "-I${SOURCE_ROOT}/include/plat/$(PLAT)/plat/$(TYPE_SUFFIX)"
-endif
-endif
-
-ifeq (${CPU}, arm1136jf-s)
-DEFINES += -DARM1136_WORKAROUND
-# Add definition for verified platform to support standalone kernel builds
-DEFINES += -DCONFIG_ARM1136JF_S
-endif
-
-WARNINGS = all error strict-prototypes missing-prototypes nested-externs \
-	missing-declarations undef pointer-arith no-nonnull
-
-CFLAGS += --std=c99 -nostdlib -nostdinc -ffreestanding \
-	${WARNINGS:%=-W%} ${INCLUDES} -fno-pic
-CPPFLAGS += -nostdinc
-LDFLAGS += -nostdlib -nostdinc -static
-LDFLAGS += -Wl,--build-id=none
-ASFLAGS += ${INCLUDES}
-
-# As the kernel has no function pointers or other indirect jumps except those
-# as generated by the compiler through switch statements we can disable jump
-# tables in order to prevent Spectre Variant 2 style attacks. Note that some
-# architectures treat certain kinds of function returns as indirect jumps and
-# this needs other mitigations
-CFLAGS += -fno-jump-tables
-
-# Compiler optimisation level. Note that you can't build the kernel with
-# GCC -Os without linking against libgcc.
-ifeq (${CONFIG_OPTIMISATION_Os},y)
-CFLAGS += -Os
-LDFLAGS += -Os
-else
-ifeq (${CONFIG_OPTIMISATION_O0},y)
-CFLAGS += -O0
-LDFLAGS += -O0
-else
-ifeq (${CONFIG_OPTIMISATION_O1},y)
-CFLAGS += -O1
-LDFLAGS += -O1
-else
-ifeq (${CONFIG_OPTIMISATION_O3},y)
-CFLAGS += -O3
-LDFLAGS += -O3
-else # Make -O2 the default for kernel builds.
-CFLAGS += -O2
-LDFLAGS += -O2
-endif # CONFIG_OPTIMISATION_O3
-endif # CONFIG_OPTIMISATION_O1
-endif # CONFIG_OPTIMISATION_O0
-endif # CONFIG_OPTIMISATION_Os
-
-# Attempt to enable -fwhole-program if it was requested. Considered harmful
-ifeq (${CONFIG_WHOLE_PROGRAM_OPTIMISATIONS_KERNEL}, y)
-    CFLAGS += -fwhole-program
-endif
-
-# Set kernel build specific flags for the different x86 variants
-# These are set here and not by the common build system as they
-# only apply to building the kernel, and nothing else
-ifeq (${ARCH}, x86)
-CFLAGS += -mno-mmx -mno-sse -mno-sse2 -mno-3dnow
-endif
-ifeq (${SEL4_ARCH}, x86_64)
-CFLAGS += -mcmodel=kernel
-endif
-ifeq (${SEL4_ARCH}, aarch64)
-CFLAGS += -mgeneral-regs-only
-endif
-ifeq (${SEL4_ARCH}, aarch32)
-CFLAGS += -mfloat-abi=soft
-endif
-ifeq (${ARCH}, riscv)
-CFLAGS += -mcmodel=medany
-endif
-
-# Allow overriding of the CFLAGS. Use with caution.
-ifdef CONFIG_KERNEL_CFLAGS
-ifneq (${CONFIG_KERNEL_CFLAGS},)
-ifneq (${CONFIG_KERNEL_CFLAGS},"")
-CFLAGS := ${CONFIG_KERNEL_CFLAGS}
-endif
-endif
-endif
-
-CFLAGS += ${DEFINES}
-CPPFLAGS += ${DEFINES} ${INCLUDES}
-
-ifdef BUILD_VERBOSE
-$(info CFLAGS   = ${CFLAGS})
-$(info ASFLAGS  = ${ASFLAGS})
-$(info CPPFLAGS = ${CPPFLAGS})
-$(info LDFLAGS  = ${LDFLAGS})
-endif
-
-############################################################
-### Paths
-############################################################
-
-PYTHONPATH := ${PYTHONPATH}:${SOURCE_ROOT}/tools
-export PYTHONPATH
-
-vpath %.c   ${SOURCE_ROOT}
-vpath %.S   ${SOURCE_ROOT}
-vpath %.h   ${SOURCE_ROOT}
-vpath %.bf  ${SOURCE_ROOT}/include \
-            ${SOURCE_ROOT}/include/arch/${ARCH} \
-            ${SOURCE_ROOT}/include/plat/${PLAT}
-vpath %.lds ${SOURCE_ROOT}
-
-INCLUDE_DIRS = ${SOURCE_ROOT}/include ${SOURCE_ROOT}/include/arch/${ARCH} \
-               ${SOURCE_ROOT}/include/plat/${PLAT} .
-
-############################################################
-### Sub-makefiles
-############################################################
-
-include ${SOURCE_ROOT}/include/arch/${ARCH}/arch/Makefile
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/Makefile
-include ${SOURCE_ROOT}/src/arch/${ARCH}/Makefile
-include ${SOURCE_ROOT}/src/plat/${PLAT}/Makefile
-include ${SOURCE_ROOT}/include/Makefile
-include ${SOURCE_ROOT}/src/Makefile
-
-DIRECTORIES += arch plat src arch/api
-
-############################################################
-### Sources and targets
-############################################################
-
-C_SOURCES += $(patsubst %, src/arch/${ARCH}/%, ${ARCH_C_SOURCES})
-ASM_SOURCES += $(patsubst %, src/arch/${ARCH}/%, ${ARCH_ASM_SOURCES})
-
-C_SOURCES += $(patsubst %, src/plat/${PLAT}/%, ${PLAT_C_SOURCES})
-ASM_SOURCES += $(patsubst %, src/plat/${PLAT}/%, ${PLAT_ASM_SOURCES})
-
-GENHEADERS = $(patsubst %.bf, %.pbf, ${BF_SOURCES}) \
-  $(patsubst %.bf, %_gen.h, ${BF_SOURCES})
-
-GENHEADERS += arch/api/invocation.h arch/api/sel4_invocation.h api/invocation.h arch/api/syscall.h
-
-DEFTHEORIES = $(patsubst %.bf, %_defs.thy, ${BF_SOURCES})
-PROOFTHEORIES = $(patsubst %.bf, %_proofs.thy, ${BF_SOURCES})
-THEORIES = ${DEFTHEORIES} ${PROOFTHEORIES}
-
-C_SOURCES_WITH_PARSE = $(sort ${C_SOURCES})
-
-STATICHEADERS := $(shell find ${SOURCE_ROOT}/include/ -name "*.h" \
-                              ! -regex ".*include/arch.*" \
-                              ! -regex ".*include/plat.*") \
-                 $(shell find ${SOURCE_ROOT}/include/arch/${ARCH} -name "*.h") \
-                 $(shell find ${SOURCE_ROOT}/include/plat/${PLAT} -name "*.h")
-
-ifeq (${HAVE_AUTOCONF}, 1)
-	STATICHEADERS += $(srctree)/include/generated/autoconf.h
-endif
-
-STATICSOURCES = $(foreach file,${C_SOURCES_WITH_PARSE} ${ASM_SOURCES}, \
-                          ${SOURCE_ROOT}/${file})
-
-OBJECTS = ${ASM_SOURCES:.S=.o} kernel.o
-
-MAKEFILES := $(shell find ${SOURCE_ROOT} -name "Makefile")
-
-############################################################
-### Top-level targets
-############################################################
-
-all: kernel.elf kernel.elf.strip
-
-theories: ${THEORIES}
-
-preprocess: ${PPFILES}
-
-.PHONY: style astyle xmllint pylint
-
-# Combine style-checking rules into a single rule
-style: astyle xmllint pylint
-
-astyle: $(shell find ${SOURCE_ROOT}/src ${SOURCE_ROOT}/include ${SOURCE_ROOT}/libsel4 -name '*.[ch]')
-	@echo " [Checking C style]"
-	$(Q)astyle --max-instatement-indent=120 --style=otbs --pad-header --indent=spaces=4 --pad-oper $^
-
-API_DTD = libsel4/tools/sel4_idl.dtd
-
-xmllint: libsel4/include/interfaces/sel4.xml $(wildcard ${SOURCE_ROOT}/libsel4/arch_include/*/interfaces/sel4arch.xml) \
-                                             $(wildcard ${SOURCE_ROOT}/libsel4/sel4_arch_include/*/interfaces/sel4arch.xml)
-	@echo " [Checking XML API descriptions against $(API_DTD)]"
-	$(Q)xmllint --dtdvalid $(API_DTD) --noout $^
-
-pylint: $(shell find ${SOURCE_ROOT}/tools ${SOURCE_ROOT}/manual/tools ${SOURCE_ROOT}/libsel4/tools -name '*.py')
-	@echo " [Checking for errors in python scripts]"
-	$(Q)pylint --errors-only --rcfile=tools/pylintrc $^
-
-validate: c-parser.log
-
-c-parser.log: kernel_all.c_pp
-	@echo " [VALIDATE] $<"
-	$(Q)${PARSER} $^ 2>&1 | tee $@.errors
-	$(Q)mv $@.errors $@
-
-# The list of sources is a variable, not a file, so there is no sane way to ask make to depend
-# upon it. This rule exists to touch a file to force the regeneration of kernel_all.c if we
-# suspect that anything has changed that may have caused the sources list to change.
-# Depend upon STATICHEADERS for autoconf/config related changes. Then try and depend upon
-# any Makefiles. If you change environment variables (such as debug or fastpath in cases where
-# not using autoconf) then you should make clean yourself. These dependencies really should
-# just be on the kernel_all.c rule, but there is some magic in the usage of the $^ variable
-# which has had the prerequsites located in the VPATH, and doing this ourselves from the
-# C_SOURCES_WITH_PARSE variable is more trouble than this horrible intermediate file.
-sources_list_updated: ${STATICHEADERS} ${MAKEFILES}
-	@echo " [TOUCH] $@"
-	$(Q)touch $@
-
-kernel_all.c: sources_list_updated ${C_SOURCES_WITH_PARSE} ${DOMAIN_CONFIG_FILE}
-	@echo " [CPP_GEN] $@"
-	$(Q)${CPP_GEN} $(wordlist 2, $(words $^), $^) > $@
-
-kernel.o: kernel_final.s
-	@echo " [AS] $@"
-	# Clear any .arch directive from the .s file in case we are assembling
-	# for a different architecture. This happens when the compiler supports
-	# a subset architecture compared to the assembler. For example where the
-	# compiler only supports armv7-a, where the assembler supports armv7ve
-	$(Q)sed -i 's/^[ \t]*\.arch .*$$//' $<
-	$(Q)${CC} ${ASFLAGS} -o $@ -c $<
-
-kernel_final.s: kernel_final.c
-	@echo " [CC] $@"
-	$(Q)${CC} ${CFLAGS} -S -o $@ $<
-
-# Awkward rule to get around passing -x to CC and having a .c input file.
-kernel_final.c: kernel_all.c_pp
-	@echo " [Circular includes] $<"
-	$(Q)${CIRCULAR_INCLUDES} < $<
-	@echo " [CP] $@"
-	$(Q)cp -a $< $@
-
-LINKER_SCRIPT = src/plat/${PLAT}/linker.lds
-
-linker.lds_pp: ${LINKER_SCRIPT}
-	@echo " [CPP] $@"
-	$(Q)${CPP} ${CPPFLAGS} -P -E -o $@ -x c $<
-
-kernel.elf: ${OBJECTS} linker.lds_pp
-	@echo " [LD] $@"
-	$(Q)${CHANGED} $@ ${CC} ${LDFLAGS} -T linker.lds_pp -Wl,-n \
-	     -o $@ ${OBJECTS}
-
-############################################################
-### Pattern rules
-############################################################
-
-%.elf.strip: %.elf | ${DIRECTORIES}
-	@echo " [STRIP] $@"
-	$(Q)${STRIP} -o $@ $<
-
-%.o: %.s_pp | ${DIRECTORIES}
-	@echo " [AS] $@"
-	$(Q)${CC} ${ASFLAGS} -x assembler -c $< -o $@
-
-###################
-# Header generation
-###################
-
-arch/api/invocation.h: ${SOURCE_ROOT}/libsel4/arch_include/${ARCH}/interfaces/sel4arch.xml ${INVOCATION_ID_GEN_PATH} | ${DIRECTORIES}
-	$(Q)rm -f ${SOURCE_ROOT}/include/arch/${ARCH}/arch/api/invocation.h
-	$(Q)${INVOCATION_ID_GEN_PATH} --arch --xml $< \
-		--dest $@
-
-arch/api/sel4_invocation.h: ${SOURCE_ROOT}/libsel4/sel4_arch_include/${SEL4_ARCH}/interfaces/sel4arch.xml ${INVOCATION_ID_GEN_PATH} | ${DIRECTORIES}
-	$(Q)rm -f ${SOURCE_ROOT}/include/arch/${ARCH}/arch/api/sel4_invocation.h
-	$(Q)${INVOCATION_ID_GEN_PATH} --sel4_arch --xml $< \
-		--dest $@
-
-
-api/invocation.h: ${SOURCE_ROOT}/libsel4/include/interfaces/sel4.xml ${INVOCATION_ID_GEN_PATH} | ${DIRECTORIES}
-	$(Q)rm -f ${SOURCE_ROOT}/include/api/invocation.h
-	$(Q)${INVOCATION_ID_GEN_PATH} --xml $< \
-		--dest $@
-
-arch/api/syscall.h: ${SOURCE_ROOT}/include/api/syscall.xsd ${SOURCE_ROOT}/include/api/syscall.xml | ${DIRECTORIES} ${SYSCALL_ID_GEN_PATH}
-	$(Q)${XMLLINT_PATH} --noout --schema $^
-	$(Q)rm -f ${SOURCE_ROOT}/include/arch/${ARCH}/arch/api/syscall.h
-	$(Q)${SYSCALL_ID_GEN_PATH} --xml $(word 2, $^) \
-		--kernel_header $@
-
-####################
-# Bitfield generation
-####################
-
-PRUNES = $(foreach file,${STATICSOURCES} ${STATICHEADERS}, \
-           --prune ${file} )
-
-TOPLEVELTYPES=cte_C tcb_C endpoint_C notification_C asid_pool_C pte_C \
-              pde_C user_data_C user_data_device_C
-TOPTYPES = $(foreach tp,${TOPLEVELTYPES}, \
-           --toplevel ${tp} )
-
-%.pbf: %.bf ${STATICHEADERS} | ${DIRECTORIES}
-	@echo " [PBF_GEN] $@"
-	$(Q)${CPP} ${CPPFLAGS} -P $< > $@
-
-%_gen.h: %.pbf ${STATICSOURCES} ${STATICHEADERS} ${BF_GEN_PATH} | ${DIRECTORIES}
-	@echo " [BF_GEN] $@"
-	$(Q)${PYTHON} ${BF_GEN_PATH} $< $@ ${PRUNES}
-
-ifdef SKIP_MODIFIES
-  SM_ARG=--skip_modifies
-else
-  SM_ARG=
-endif
-
-${DEFTHEORIES}: %_defs.thy: %.pbf ${BF_GEN_PATH} ${STATICSOURCES} \
-                ${STATICHEADERS} ${SOURCE_ROOT}/Makefile | ${DIRECTORIES}
-	@echo " [BF_DEFS] $@"
-	$(Q)${PYTHON} ${BF_GEN_PATH} --cspec-dir ${CSPEC_DIR} --hol_defs $< $@ ${PRUNES} ${SM_ARG}
-
-${PROOFTHEORIES}: %_proofs.thy: %.pbf ${BF_GEN_PATH} ${STATICSOURCES} \
-                  ${STATICHEADERS} ${SOURCE_ROOT}/Makefile ${UMM_TYPES} | ${DIRECTORIES}
-	@echo " [BF_PROOFS] $@"
-	@$(if ${UMM_TYPES}, , echo "UMM_TYPES unset" ; false)
-	$(Q)${PYTHON} ${BF_GEN_PATH} --cspec-dir ${CSPEC_DIR} --hol_proofs ${SORRY_ARG} $< $@ ${TOPTYPES} \
-	           --umm_types ${UMM_TYPES} ${PRUNES} ${SM_ARG}
-
-###########################
-# Preprocessed source files
-###########################
-
-%.s_pp: %.S ${GENHEADERS} ${STATICHEADERS} | ${DIRECTORIES}
-	@echo " [CPP] $@"
-	$(Q)${CPP} ${CPPFLAGS} -CC -E -o $@ $<
-
-%.c_pp: %.c ${GENHEADERS} ${STATICHEADERS} | ${DIRECTORIES}
-	@echo " [CPP] $@"
-ifdef NO_PRESERVE_TIMESTAMP
-    # Preserving the timestamp can cause repeated rebuilding if a file is touched
-    # with trivial modifications such that it has a future timestamp, but every time
-    # we rebuild we restore this timestamp back into the past. This results in partial
-    # rebuilds all the time. This flag allows you to stop this happening if you find it upsetting.
-	$(Q)${CPP} ${CPPFLAGS} -CC -E -o $@ $<
-else
-	$(Q)${CHANGED} $@ ${CPP} ${CPPFLAGS} -CC -E -o $@ $<
-endif
-
-%.h_pp: %.h ${GENHEADERS} ${STATICHEADERS} | ${DIRECTORIES}
-	@echo " [CPP] $@"
-	$(Q)${CPP} ${CPPFLAGS} -CC -E -o $@ $<
-
-############################################################
-### Utility targets
-############################################################
-
-CLEANTARGETS = kernel.elf kernel.elf.strip ${GENHEADERS} ${OBJECTS} autoconf.h \
-  parser.out parsetab.py \
-  kernel_final.s kernel_final.c kernel_all.c kernel_all.c_pp \
-  ${PPFILES} ${THEORIES} c-parser.log c-parser-all.log \
-  arch api plat ${ASM_SOURCES:.S=.s_pp} linker.lds_pp
-
-clean:
-	@echo " [CLEAN]"
-	rm -f ${SOURCE_ROOT}/include/arch/${ARCH}/arch/api/invocation.h
-	rm -f ${SOURCE_ROOT}/include/api/invocation.h
-	rm -f ${SOURCE_ROOT}/include/arch/${ARCH}/arch/api/syscall.h
-	rm -Rf ${CLEANTARGETS}
-
-.PHONY: distclean
-distclean: clean
-	@echo " [CLEAN]"
-	$(Q)rm -f tools/*.pyc
-
-${DIRECTORIES}:
-	@echo " [MKDIR] $@"
-	$(Q)mkdir -p ${DIRECTORIES}
-
-.FORCE:
-
-.PHONY: .FORCE
--- a/include/32/mode/Makefile
+++ b/include/32/mode/Makefile
@ -1,15 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += 32/mode/api
-BF_SOURCES += 32/mode/api/shared_types.bf
-INCLUDE_DIRS += 32
--- a/include/64/mode/Makefile
+++ b/include/64/mode/Makefile
@ -1,15 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += 64/mode/api
-BF_SOURCES += 64/mode/api/shared_types.bf
-INCLUDE_DIRS += 64
--- a/include/Makefile
+++ b/include/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/api/Makefile
-include ${SOURCE_ROOT}/include/${TYPE_SUFFIX}/mode/Makefile
-INCLUDE_DIRS += ${SOURCE_ROOT}/include/${TYPE_SUFFIX}
--- a/include/api/Makefile
+++ b/include/api/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += api
--- a/include/arch/arm/arch/Makefile
+++ b/include/arch/arm/arch/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/arch/arm/arch/object/Makefile
--- a/include/arch/arm/arch/object/Makefile
+++ b/include/arch/arm/arch/object/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += arch/object
-
-BF_SOURCES += arch/object/structures.bf
--- a/include/arch/riscv/arch/Makefile
+++ b/include/arch/riscv/arch/Makefile
@ -1,18 +0,0 @@
-#
-# Copyright 2018, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-#
-#
-# Copyright 2016, 2017 Hesham Almatary, Data61/CSIRO <hesham.almatary@data61.csiro.au>
-# Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
-#
-include ${SOURCE_ROOT}/include/arch/riscv/arch/object/Makefile
--- a/include/arch/riscv/arch/object/Makefile
+++ b/include/arch/riscv/arch/object/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += arch/object
-
-BF_SOURCES += arch/object/structures.bf
--- a/include/arch/x86/arch/Makefile
+++ b/include/arch/x86/arch/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/arch/$(ARCH)/arch/object/Makefile
--- a/include/arch/x86/arch/object/Makefile
+++ b/include/arch/x86/arch/object/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += arch/object
-
-BF_SOURCES += arch/object/structures.bf
--- a/include/benchmark/Makefile
+++ b/include/benchmark/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += benchmark
--- a/include/plat/allwinnerA20/plat/Makefile
+++ b/include/plat/allwinnerA20/plat/Makefile
@ -1,11 +0,0 @@
-#
-# Copyright 2015, DornerWorks, Ltd.
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/allwinnerA20/plat/machine/Makefile
+++ b/include/plat/allwinnerA20/plat/machine/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2015, DornerWorks, Ltd.
-#
-# 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)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/am335x/plat/Makefile
+++ b/include/plat/am335x/plat/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/am335x/plat/machine/Makefile
+++ b/include/plat/am335x/plat/machine/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/apq8064/plat/Makefile
+++ b/include/plat/apq8064/plat/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/apq8064/plat/machine/Makefile
+++ b/include/plat/apq8064/plat/machine/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/bcm2837/plat/Makefile
+++ b/include/plat/bcm2837/plat/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/bcm2837/plat/machine/Makefile
+++ b/include/plat/bcm2837/plat/machine/Makefile
@ -1,15 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/exynos4/plat/Makefile
+++ b/include/plat/exynos4/plat/Makefile
@ -1,12 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
-INCLUDE_DIRS += ${SOURCE_ROOT}/include/plat/exynos_common/
--- a/include/plat/exynos4/plat/machine/Makefile
+++ b/include/plat/exynos4/plat/machine/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/exynos5/plat/Makefile
+++ b/include/plat/exynos5/plat/Makefile
@ -1,12 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
-INCLUDE_DIRS += ${SOURCE_ROOT}/include/plat/exynos_common/
--- a/include/plat/exynos5/plat/machine/Makefile
+++ b/include/plat/exynos5/plat/machine/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/hikey/plat/Makefile
+++ b/include/plat/hikey/plat/Makefile
@ -1,11 +0,0 @@
-#
-# Copyright 2015, DornerWorks, Ltd.
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/hikey/plat/machine/Makefile
+++ b/include/plat/hikey/plat/machine/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2015, DornerWorks, Ltd.
-#
-# 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)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/imx31/plat/Makefile
+++ b/include/plat/imx31/plat/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/imx31/plat/machine/Makefile
+++ b/include/plat/imx31/plat/machine/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/imx6/plat/Makefile
+++ b/include/plat/imx6/plat/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/imx6/plat/machine/Makefile
+++ b/include/plat/imx6/plat/machine/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/imx7/plat/Makefile
+++ b/include/plat/imx7/plat/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/imx7/plat/machine/Makefile
+++ b/include/plat/imx7/plat/machine/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/omap3/plat/Makefile
+++ b/include/plat/omap3/plat/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/omap3/plat/machine/Makefile
+++ b/include/plat/omap3/plat/machine/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/pc99/plat/32/plat_mode/machine/Makefile
+++ b/include/plat/pc99/plat/32/plat_mode/machine/Makefile
@ -1,14 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += plat/32/plat_mode/machine
-BF_SOURCES += plat/32/plat_mode/machine/hardware.bf
--- a/include/plat/pc99/plat/64/plat_mode/machine/Makefile
+++ b/include/plat/pc99/plat/64/plat_mode/machine/Makefile
@ -1,14 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += plat/64/plat_mode/machine
-BF_SOURCES += plat/64/plat_mode/machine/hardware.bf
--- a/include/plat/pc99/plat/Makefile
+++ b/include/plat/pc99/plat/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/${TYPE_SUFFIX}/plat_mode/machine/Makefile
-INCLUDE_DIRS += plat/${TYPE_SUFFIX}
--- a/include/plat/pc99/plat/machine/Makefile
+++ b/include/plat/pc99/plat/machine/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += plat/machine
--- a/include/plat/spike/plat/Makefile
+++ b/include/plat/spike/plat/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/spike/plat/machine/Makefile
+++ b/include/plat/spike/plat/machine/Makefile
@ -1,21 +0,0 @@
-#
-# Copyright 2018, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-#
-#
-# Copyright 2016, 2017 Hesham Almatary, Data61/CSIRO <hesham.almatary@data61.csiro.au>
-# Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/tk1/plat/Makefile
+++ b/include/plat/tk1/plat/Makefile
@ -1,11 +0,0 @@
-#
-# Copyright 2016, 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/tk1/plat/machine/Makefile
+++ b/include/plat/tk1/plat/machine/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2016, 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)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/tx1/plat/Makefile
+++ b/include/plat/tx1/plat/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/tx1/plat/machine/Makefile
+++ b/include/plat/tx1/plat/machine/Makefile
@ -1,15 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/zynq7000/plat/Makefile
+++ b/include/plat/zynq7000/plat/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/zynq7000/plat/machine/Makefile
+++ b/include/plat/zynq7000/plat/machine/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/include/plat/zynqmp/plat/Makefile
+++ b/include/plat/zynqmp/plat/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-include ${SOURCE_ROOT}/include/plat/${PLAT}/plat/machine/Makefile
--- a/include/plat/zynqmp/plat/machine/Makefile
+++ b/include/plat/zynqmp/plat/machine/Makefile
@ -1,15 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += plat/machine
-
-BF_SOURCES +=  plat/machine/hardware.bf
--- a/libsel4/Kbuild
+++ b/libsel4/Kbuild
@ -1,14 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# This software may be distributed and modified according to the terms of
-# the BSD 2-Clause license. Note that NO WARRANTY is provided.
-# See "LICENSE_BSD2.txt" for details.
-#
-# @TAG(DATA61_BSD)
-#
-
-libs-$(CONFIG_LIB_SEL4) += libsel4
-libsel4: common
--- a/libsel4/Kconfig
+++ b/libsel4/Kconfig
@ -1,62 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# This software may be distributed and modified according to the terms of
-# the BSD 2-Clause license. Note that NO WARRANTY is provided.
-# See "LICENSE_BSD2.txt" for details.
-#
-# @TAG(DATA61_BSD)
-#
-
-menu "libsel4"
-    config LIB_SEL4
-        bool "libsel4"
-        default y
-        select HAVE_LIB_SEL4
-        help
-            seL4 API library
-
-choice
-    prompt "Function attributes"
-    default LIB_SEL4_INLINE_INVOCATIONS
-
-config LIB_SEL4_DEFAULT_FUNCTION_ATTRIBUTES
-    bool "Default"
-    depends on LIB_SEL4
-    help
-        Verification friendly default configuration. syscalls will be inlined,
-        but generated functions will not.
-
-config LIB_SEL4_INLINE_INVOCATIONS
-    bool "Inline generated syscall invocations"
-    depends on LIB_SEL4
-    help
-        When set to true will mark generated functions as 'inline', allowing
-        them to be inlined by the callee user code. This may be undesirable
-        for verification, so setting to 'n' will forcibly prevent the function
-        from being inlined.
-
-config LIB_SEL4_PUBLIC_SYMBOLS
-    bool "Public symbols for all external interfaces"
-    depends on LIB_SEL4
-    help
-        When set to true will make all user facing functions available as
-        public symbols, which can be convenient for some language bindings.
-
-endchoice
-
-config LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY
-    bool "use only IPC buffer for syscalls"
-    depends on LIB_SEL4
-    default n
-    help
-        When generating syscall wrappers, only use the IPC buffer for
-        marshalling and unmarshalling arguments. Without this option set,
-        arguments will be passed in registers where possible for better
-        performance.
-
-config HAVE_LIB_SEL4
-    bool
-endmenu
--- a/libsel4/Makefile
+++ b/libsel4/Makefile
@ -1,139 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# This software may be distributed and modified according to the terms of
-# the BSD 2-Clause license. Note that NO WARRANTY is provided.
-# See "LICENSE_BSD2.txt" for details.
-#
-# @TAG(DATA61_BSD)
-#
-
-# Tools
-BF_GEN_PATH := ${SOURCE_DIR}/tools/bitfield_gen.py
-SYSCALL_ID_GEN_PATH := ${SOURCE_DIR}/tools/syscall_header_gen.py
-INVOCATION_ID_GEN_PATH := ${SOURCE_DIR}/tools/invocation_header_gen.py
-XMLLINT_PATH := ${SOURCE_DIR}/tools/xmllint.sh
-CHANGED_PATH := ${SOURCE_DIR}/tools/changed.sh
-
-ifeq (${PYTHON},)
-PYTHON = python
-# Suppress python bytecode (pyc) files for build thread safety
-export PYTHONDONTWRITEBYTECODE = true
-endif
-
-ifeq (${KERNEL_32}, y)
-TYPE_SUFFIX:=32
-else
-ifeq (${KERNEL_64}, y)
-TYPE_SUFFIX:=64
-else
-$(error Cannot determine TYPE_SUFFIX)
-endif
-endif
-
-# Targets
-PRIORITY_TARGETS := include/interfaces/sel4_client.h include/sel4/syscall.h \
-					include/sel4/invocation.h arch_include/${ARCH}/sel4/arch/invocation.h \
-					include/sel4/shared_types_gen.h sel4_arch_include/${SEL4_ARCH}/sel4/sel4_arch/invocation.h \
-					sel4_arch_include/${SEL4_ARCH}/sel4/sel4_arch/types_gen.h
-TARGETS          := libsel4.a
-
-# Source files required to build the target
-CFILES := \
-	$(patsubst $(SOURCE_DIR)/%,%,$(wildcard $(SOURCE_DIR)/src/*.c))
-
-# Header files/directories this library provides
-# Note: sel4_client.h may not have been built at the time this is evaluated.
-HDRFILES := \
-	$(wildcard $(SOURCE_DIR)/include/*) \
-	$(wildcard $(SOURCE_DIR)/arch_include/$(ARCH)/*) \
-	$(wildcard $(SOURCE_DIR)/sel4_arch_include/$(SEL4_ARCH)/*) \
-	$(wildcard $(SOURCE_DIR)/sel4_plat_include/$(PLAT)/*) \
-	$(wildcard $(SOURCE_DIR)/mode_include/$(TYPE_SUFFIX)/*) \
-	$(BUILD_DIR)/include/sel4 \
-	$(BUILD_DIR)/include/interfaces \
-	$(BUILD_DIR)/arch_include/${ARCH}/* \
-    $(BUILD_DIR)/sel4_arch_include/$(SEL4_ARCH)/*
-#TODO proper prefix instruction
-
-.DEFAULT_GOAL := default
-
-install-headers: ${PRIORITY_TARGETS}
-
-include $(SEL4_COMMON)/common.mk
-
-# For all the autogenerated headers we use the 'changed' script which will
-# only update the timestamp of the target if the file actually changed
-# This prevents anything that depends upon the target from being rebuilt
-# if the file did not really change. This is neccessary because these
-# targets get called forcively as a result of install-headers being a
-# PHONY target. The downside to this 'trick' is if one of our prerequisites
-# has its timestamp updated then make will get confused and always think
-# this build step needs to be redone. But since it is phony and gets redone
-# anyway, who cares!
-include/sel4/invocation.h: ${SOURCE_DIR}/include/interfaces/sel4.xml
-	@echo " [GEN] $@"
-	@mkdir -p $(dir $@)
-	@${CHANGED_PATH} $@ ${PYTHON} ${INVOCATION_ID_GEN_PATH} \
-		--xml $< --libsel4 --dest $@
-
-sel4_arch_include/${SEL4_ARCH}/sel4/sel4_arch/invocation.h: ${SOURCE_DIR}/sel4_arch_include/${SEL4_ARCH}/interfaces/sel4arch.xml
-	@echo " [GEN] $@"
-	@mkdir -p $(dir $@)
-	@${CHANGED_PATH} $@ ${PYTHON} ${INVOCATION_ID_GEN_PATH} \
-		--xml $< --libsel4 --sel4_arch --dest $@
-
-arch_include/${ARCH}/sel4/arch/invocation.h: ${SOURCE_DIR}/arch_include/${ARCH}/interfaces/sel4arch.xml
-	@echo " [GEN] $@"
-	@mkdir -p $(dir $@)
-	@${CHANGED_PATH} $@ ${PYTHON} ${INVOCATION_ID_GEN_PATH} \
-		--xml $< --libsel4 --arch --dest $@
-
-# Header generator
-include/sel4/syscall.h: ${SOURCE_DIR}/include/api/syscall.xsd \
-						${SOURCE_DIR}/include/api/syscall.xml
-	@echo " [GEN] $@"
-	@mkdir -p $(dir $@)
-	@${XMLLINT_PATH} --noout --schema $^
-	@${CHANGED_PATH} $@ ${PYTHON} ${SYSCALL_ID_GEN_PATH} \
-	--xml ${SOURCE_DIR}/include/api/syscall.xml \
-	--libsel4_header $@
-
-include/sel4/%.pbf: ${SOURCE_DIR}/include/sel4/%.bf $(srctree)/include/generated/autoconf.h
-	@echo " [PBF_GEN] $@"
-	@mkdir -p $(dir $@)
-	$(Q)${CPP} ${CPPFLAGS} -P $< > $@
-
-include/sel4/sel4_arch/%.pbf: ${SOURCE_DIR}/sel4_arch_include/${SEL4_ARCH}/sel4/sel4_arch/types.bf $(srctree)/include/generated/autoconf.h
-	@echo " [PBF_GEN] $@"
-	@mkdir -p $(dir $@)
-	$(Q)${CPP} ${CPPFLAGS} -I${SOURCE_DIR}/arch_include/${ARCH}/ -P $< > $@
-
-# Bitfield generator
-include/sel4/shared_types_gen.h: \
-		include/sel4/shared_types_${TYPE_SUFFIX}.pbf \
-		${BF_GEN_PATH}
-	@echo " [GEN] $@"
-	@mkdir -p $(dir $@)
-	@${CHANGED_PATH} $@ ${PYTHON} ${BF_GEN_PATH} --environment libsel4 $< include/sel4/shared_types_gen.h
-
-sel4_arch_include/${SEL4_ARCH}/sel4/sel4_arch/types_gen.h: \
-		include/sel4/sel4_arch/types.pbf \
-		${BF_GEN_PATH}
-	@echo " [GEN] $@"
-	@mkdir -p $(dir $@)
-	@${CHANGED_PATH} $@ python ${BF_GEN_PATH} --environment libsel4 $< sel4_arch_include/${SEL4_ARCH}/sel4/sel4_arch/types_gen.h
-
-# Stub generator
-include/interfaces/sel4_client.h: \
-		${SOURCE_DIR}/sel4_arch_include/${SEL4_ARCH}/interfaces/sel4arch.xml \
-        ${SOURCE_DIR}/arch_include/${ARCH}/interfaces/sel4arch.xml \
-		${SOURCE_DIR}/include/interfaces/sel4.xml
-	@echo " [GEN] $@"
-	@mkdir -p $(dir $@)
-	@${CHANGED_PATH} $@ \
-        ${PYTHON} ${SOURCE_DIR}/tools/syscall_stub_gen.py \
-        $(if ${CONFIG_LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY},--buffer,) \
-        -a $(SEL4_ARCH) -c ${srctree}/.config -o $@ $^
--- a/src/Makefile
+++ b/src/Makefile
@ -1,23 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/src/fastpath/Makefile
-include ${SOURCE_ROOT}/src/api/Makefile
-include ${SOURCE_ROOT}/src/kernel/Makefile
-include ${SOURCE_ROOT}/src/object/Makefile
-include ${SOURCE_ROOT}/src/model/Makefile
-include ${SOURCE_ROOT}/src/machine/Makefile
-include ${SOURCE_ROOT}/src/benchmark/Makefile
-include ${SOURCE_ROOT}/src/smp/Makefile
-
-C_SOURCES += src/inlines.c \
-             src/assert.c \
-             src/util.c \
-             src/string.c
--- a/src/api/Makefile
+++ b/src/api/Makefile
@ -1,14 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += src/api
-
-C_SOURCES += src/api/syscall.c
-C_SOURCES += src/api/faults.c
--- a/src/arch/arm/32/Makefile
+++ b/src/arch/arm/32/Makefile
@ -1,23 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += src/arch/$(ARCH)/32
-
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/32/object/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/32/kernel/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/32/model/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/32/machine/Makefile
-
-ARCH_C_SOURCES   += 32/c_traps.c \
-                    32/idle.c
-
-ARCH_ASM_SOURCES += 32/head.S \
-                    32/traps.S \
-                    32/hyp_traps.S
--- a/src/arch/arm/32/kernel/Makefile
+++ b/src/arch/arm/32/kernel/Makefile
@ -1,12 +0,0 @@
-#
-# 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)
-#
-
-ARCH_C_SOURCES += 32/kernel/thread.c \
-                  32/kernel/vspace.c
--- a/src/arch/arm/32/machine/Makefile
+++ b/src/arch/arm/32/machine/Makefile
@ -1,17 +0,0 @@
-#
-# 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)
-#
-
-ARCH_C_SOURCES += 32/machine/hardware.c \
-                  32/machine/registerset.c \
-                  32/machine/fpu.c
-
-ifdef DEBUG
-    ARCH_C_SOURCES += 32/machine/capdl.c
-endif
--- a/src/arch/arm/32/model/Makefile
+++ b/src/arch/arm/32/model/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-ARCH_C_SOURCES += 32/model/statedata.c
--- a/src/arch/arm/32/object/Makefile
+++ b/src/arch/arm/32/object/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-ARCH_C_SOURCES += 32/object/objecttype.c
--- a/src/arch/arm/64/Makefile
+++ b/src/arch/arm/64/Makefile
@ -1,24 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += src/arch/$(ARCH)/64
-
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/64/object/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/64/kernel/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/64/model/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/64/machine/Makefile
-
-ARCH_C_SOURCES   += 64/c_traps.c \
-                    64/idle.c
-
-ARCH_ASM_SOURCES += 64/head.S \
-                    64/traps.S
--- a/src/arch/arm/64/kernel/Makefile
+++ b/src/arch/arm/64/kernel/Makefile
@ -1,14 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-ARCH_C_SOURCES += 64/kernel/thread.c \
-                  64/kernel/vspace.c
--- a/src/arch/arm/64/machine/Makefile
+++ b/src/arch/arm/64/machine/Makefile
@ -1,19 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-ARCH_C_SOURCES += 64/machine/hardware.c \
-                  64/machine/registerset.c \
-                  64/machine/fpu.c
-
-ifdef DEBUG
-    ARCH_C_SOURCES += 64/machine/capdl.c
-endif
--- a/src/arch/arm/64/model/Makefile
+++ b/src/arch/arm/64/model/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-ARCH_C_SOURCES += 64/model/statedata.c
--- a/src/arch/arm/64/object/Makefile
+++ b/src/arch/arm/64/object/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-ARCH_C_SOURCES += 64/object/objecttype.c
--- a/src/arch/arm/Kconfig
+++ b/src/arch/arm/Kconfig
@ -1,96 +0,0 @@
-#
-# 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 HAVE_ARCH_TIMER
-    bool
-    default y
-    depends on ARM_CORTEX_A15
-
-config ENABLE_A9_PREFETCHER
-    bool "Enable Cortex-A9 prefetcher"
-    default n
-    depends on ARM_CORTEX_A9
-    help
-        Cortex-A9 has an L1 and L2 prefetcher. By default
-        they are disabled. This config options allows
-        them to be turned on. Enabling the prefetchers
-        requires that the kernel be in secure mode. ARM
-        documents indicate that as of r4p1 version of
-        Cortex-A9 the bits used to enable the prefetchers
-        no longer exist, it is not clear if this is just
-        a document error or not.
-
-config EXPORT_PMU_USER
-    bool "PL0 access to PMU"
-    default n
-    depends on (ARCH_ARM_V7A || ARCH_ARM_V8A) && !ARM_CORTEX_A8
-    help
-        Grant user access to Performance Monitoring Unit.
-        WARNING: While useful for evaluating performance,
-        this option opens timing and covert channels.
-
-config EXPORT_PCNT_USER
-    bool "PL0 access to generic timer CNTPCT and CNTFRQ"
-    default y
-    depends on HAVE_ARCH_TIMER
-    help
-        Grant user access to physical counter and counter
-        frequency registers of the generic timer.
-        WARNING: selecting this option opens a timing
-        channel
-
-config EXPORT_VCNT_USER
-    bool "PL0 access to generic timer CNTVCT and CNTFRQ"
-    default y
-    depends on HAVE_ARCH_TIMER
-    help
-        Grant user access to virtual counter and counter
-        frequency registers of the generic timer.
-        WARNING: selecting this option opens a timing
-        channel
-
-choice
-    prompt "IPC Buffer location"
-    default IPC_BUF_TPIDRURW if !ARCH_ARM_V6
-    default IPC_BUF_GLOBALS_FRAME if ARCH_ARM_V6
-    depends on ARCH_AARCH32
-    help
-        Controls how the location of the IPC buffer is
-        provided to the user
-
-    config IPC_BUF_GLOBALS_FRAME
-        bool "Globals frame"
-        depends on ARCH_AARCH32 && (MAX_NUM_NODES = 1)
-        help
-            Put the address of the IPC buffer in a dedicated
-            frame that is read only at user level. This works
-            on all ARM platforms
-    config IPC_BUF_TPIDRURW
-        bool "ThreadID register"
-        depends on !ARCH_ARM_V6
-        help
-            Put the address of the IPC buffer in the user
-            readable/writeable ThreadID register. When enabled
-            this has the result of the kernel overwriting
-            any value the user writes to this register.
-endchoice
-
-config SMMU_INTERRUPT_ENABLE
-    bool "Enable SMMU interrupts"
-    default y if DEBUG_BUILD
-    default n if !DEBUG_BUILD
-    depends on ARM_SMMU
-    help
-        SMMU interrupts currently only serve a debug purpose as
-        they are not forwarded to user level. Enabling this will
-        cause some fault types to print out a message in the kernel.
-        WARNING: Printing fault information is slow and rapid faults
-        can result in all time spent in the kernel printing fault
-        messages
--- a/src/arch/arm/Makefile
+++ b/src/arch/arm/Makefile
@ -1,21 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/src/arch/arm/api/Makefile
-include ${SOURCE_ROOT}/src/arch/arm/object/Makefile
-include ${SOURCE_ROOT}/src/arch/arm/kernel/Makefile
-include ${SOURCE_ROOT}/src/arch/arm/machine/Makefile
-include ${SOURCE_ROOT}/src/arch/arm/benchmark/Makefile
-include ${SOURCE_ROOT}/src/arch/arm/smp/Makefile
-include ${SOURCE_ROOT}/src/arch/arm/armv/$(ARMV)/Makefile
-
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/${TYPE_SUFFIX}/Makefile
-
-ARCH_C_SOURCES += c_traps.c
--- a/src/arch/arm/api/Makefile
+++ b/src/arch/arm/api/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += src/arch/arm/api
-
-ARCH_C_SOURCES += api/faults.c
--- a/src/arch/arm/armv/armv6/Makefile
+++ b/src/arch/arm/armv/armv6/Makefile
@ -1,18 +0,0 @@
-#
-# 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)
-#
-DIRECTORIES += src/arch/arm/armv/${ARMV}
-
-INCLUDE_DIRS += ${SOURCE_ROOT}/include/arch/arm/armv/${ARMV}
-
-ARCH_ASM_SOURCES += armv/${ARMV}/machine_asm.S
-
-ARCH_C_SOURCES += armv/${ARMV}/benchmark.c
-ARCH_C_SOURCES += armv/${ARMV}/user_access.c
-ARCH_C_SOURCES += armv/${ARMV}/cache.c
--- a/src/arch/arm/armv/armv7-a/Makefile
+++ b/src/arch/arm/armv/armv7-a/Makefile
@ -1,18 +0,0 @@
-#
-# 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)
-#
-DIRECTORIES += src/arch/arm/armv/${ARMV}
-
-INCLUDE_DIRS += ${SOURCE_ROOT}/include/arch/arm/armv/${ARMV}
-
-ARCH_ASM_SOURCES += armv/${ARMV}/machine_asm.S
-
-ARCH_C_SOURCES += armv/${ARMV}/benchmark.c
-ARCH_C_SOURCES += armv/${ARMV}/user_access.c
-ARCH_C_SOURCES += armv/${ARMV}/cache.c
--- a/src/arch/arm/armv/armv8-a/Makefile
+++ b/src/arch/arm/armv/armv8-a/Makefile
@ -1,18 +0,0 @@
-#
-# 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)
-#
-DIRECTORIES += src/arch/arm/armv/${ARMV}/$(TYPE_SUFFIX)
-
-INCLUDE_DIRS += ${SOURCE_ROOT}/include/arch/arm/armv/${ARMV}/$(TYPE_SUFFIX)
-
-ARCH_ASM_SOURCES += armv/${ARMV}/$(TYPE_SUFFIX)/machine_asm.S
-
-ARCH_C_SOURCES += armv/${ARMV}/$(TYPE_SUFFIX)/benchmark.c
-ARCH_C_SOURCES += armv/${ARMV}/$(TYPE_SUFFIX)/user_access.c
-ARCH_C_SOURCES += armv/${ARMV}/$(TYPE_SUFFIX)/cache.c
--- a/src/arch/arm/benchmark/Makefile
+++ b/src/arch/arm/benchmark/Makefile
@ -1,15 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += src/arch/arm/benchmark
-
-ARCH_C_SOURCES += benchmark/benchmark.c
--- a/src/arch/arm/kernel/Makefile
+++ b/src/arch/arm/kernel/Makefile
@ -1,14 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += src/arch/arm/kernel
-
-C_SOURCES += src/arch/arm/kernel/boot.c \
-             src/arch/arm/kernel/thread.c
--- a/src/arch/arm/machine/Makefile
+++ b/src/arch/arm/machine/Makefile
@ -1,43 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += src/arch/arm/machine
-
-ARCH_C_SOURCES += machine/cache.c \
-                  machine/errata.c \
-                  machine/io.c \
-                  machine/debug.c
-
-ifeq ($(CPU), cortex-a9)
-    ARCH_C_SOURCES += machine/gic_pl390.c
-    ARCH_C_SOURCES += machine/l2c_310.c
-
-ifeq ($(PLAT), exynos4)
-    # if exynos4412 has MPCORE peripherals, then
-    # samsung has NOT documented their location
-else
-    ARCH_C_SOURCES += machine/priv_timer.c
-endif
-
-endif
-
-# platforms that use the generic timer
-ifeq ($(PLAT), $(filter $(PLAT), exynos5 bcm2837 hikey tk1 tx1 zynqmp imx7))
-	ARCH_C_SOURCES += machine/generic_timer.c
-endif
-
-ifeq ($(CPU), $(filter $(CPU), cortex-a15 cortex-a7 cortex-a57))
-    # A15 uses the gic_pl400 which is an extention of pl390
-    ARCH_C_SOURCES += machine/gic_pl390.c
-endif
-
-ifeq ($(PLAT), $(filter $(PLAT), zynqmp hikey))
-    ARCH_C_SOURCES += machine/gic_pl390.c
-endif
--- a/src/arch/arm/object/Makefile
+++ b/src/arch/arm/object/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += src/arch/arm/object
-
-ARCH_C_SOURCES += object/interrupt.c object/tcb.c object/iospace.c object/vcpu.c
--- a/src/arch/arm/smp/Makefile
+++ b/src/arch/arm/smp/Makefile
@ -1,13 +0,0 @@
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-DIRECTORIES += src/arch/arm/smp
-
-C_SOURCES += src/arch/arm/smp/ipi.c
--- a/src/arch/riscv/Kconfig
+++ b/src/arch/riscv/Kconfig
@ -1,29 +0,0 @@
-#
-# Copyright 2018, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-#
-#
-# Copyright 2016, 2017 Hesham Almatary, Data61/CSIRO <hesham.almatary@data61.csiro.au>
-# Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
-#
-
-config HAVE_ARCH_TIMER
-    bool
-    default y
-
-config PT_LEVELS
-    int "Number of page table levels"
-    default 3
-    help
-        Number of page tables levels for RISC-V depends on the mode. For
-        example there are: 2, 3 and 4 levels on Sv32, Sv39, Sv48 RISC-V paging
-        modes respectively.
--- a/src/arch/riscv/Makefile
+++ b/src/arch/riscv/Makefile
@ -1,28 +0,0 @@
-#
-# Copyright 2018, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-#
-#
-# Copyright 2016, 2017 Hesham Almatary, Data61/CSIRO <hesham.almatary@data61.csiro.au>
-# Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
-#
-
-DIRECTORIES += src/arch/riscv/
-
-include ${SOURCE_ROOT}/src/arch/riscv/object/Makefile
-include ${SOURCE_ROOT}/src/arch/riscv/api/Makefile
-include ${SOURCE_ROOT}/src/arch/riscv/kernel/Makefile
-include ${SOURCE_ROOT}/src/arch/riscv/model/Makefile
-include ${SOURCE_ROOT}/src/arch/riscv/machine/Makefile
-
-ARCH_ASM_SOURCES += head.S traps.S
-ARCH_C_SOURCES += c_traps.c idle.c
--- a/src/arch/riscv/api/Makefile
+++ b/src/arch/riscv/api/Makefile
@ -1,21 +0,0 @@
-#
-# Copyright 2018, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-#
-#
-# Copyright 2016, 2017 Hesham Almatary, Data61/CSIRO <hesham.almatary@data61.csiro.au>
-# Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
-#
-
-DIRECTORIES += src/arch/riscv/api
-
-ARCH_C_SOURCES += api/faults.c
--- a/src/arch/riscv/kernel/Makefile
+++ b/src/arch/riscv/kernel/Makefile
@ -1,23 +0,0 @@
-#
-# Copyright 2018, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-#
-#
-# Copyright 2016, 2017 Hesham Almatary, Data61/CSIRO <hesham.almatary@data61.csiro.au>
-# Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
-#
-
-DIRECTORIES += src/arch/riscv/kernel
-
-C_SOURCES += src/arch/riscv/kernel/thread.c \
-             src/arch/riscv/kernel/vspace.c \
-             src/arch/riscv/kernel/boot.c
--- a/src/arch/riscv/machine/Makefile
+++ b/src/arch/riscv/machine/Makefile
@ -1,21 +0,0 @@
-#
-# Copyright 2018, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += src/arch/riscv/machine
-
-ARCH_C_SOURCES += machine/registerset.c \
-    machine/hardware.c \
-	machine/io.c
-
-ifdef DEBUG
-    ARCH_C_SOURCES += machine/capdl.c
-endif
--- a/src/arch/riscv/model/Makefile
+++ b/src/arch/riscv/model/Makefile
@ -1,21 +0,0 @@
-#
-# Copyright 2018, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-#
-#
-# Copyright 2016, 2017 Hesham Almatary, Data61/CSIRO <hesham.almatary@data61.csiro.au>
-# Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
-#
-
-DIRECTORIES += src/arch/riscv/model
-
-ARCH_C_SOURCES += model/statedata.c
--- a/src/arch/riscv/object/Makefile
+++ b/src/arch/riscv/object/Makefile
@ -1,21 +0,0 @@
-#
-# Copyright 2018, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-#
-#
-# Copyright 2016, 2017 Hesham Almatary, Data61/CSIRO <hesham.almatary@data61.csiro.au>
-# Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
-#
-
-DIRECTORIES += src/arch/riscv/object
-
-ARCH_C_SOURCES += object/tcb.c object/interrupt.c object/objecttype.c
--- a/src/arch/x86/32/Makefile
+++ b/src/arch/x86/32/Makefile
@ -1,22 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += src/arch/$(ARCH)/32
-
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/32/object/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/32/kernel/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/32/model/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/32/machine/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/32/smp/Makefile
-
-ARCH_C_SOURCES += 32/c_traps.c
-ARCH_ASM_SOURCES += 32/machine_asm.S \
-                    32/traps.S \
-                    32/head.S
--- a/src/arch/x86/32/kernel/Makefile
+++ b/src/arch/x86/32/kernel/Makefile
@ -1,14 +0,0 @@
-#
-# 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)
-#
-
-ARCH_C_SOURCES += 32/kernel/vspace_32paging.c \
-                  32/kernel/thread.c \
-                  32/kernel/vspace.c \
-                  32/kernel/elf.c
--- a/src/arch/x86/32/machine/Makefile
+++ b/src/arch/x86/32/machine/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-ARCH_C_SOURCES += 32/machine/registerset.c
--- a/src/arch/x86/32/model/Makefile
+++ b/src/arch/x86/32/model/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-ARCH_C_SOURCES += 32/model/statedata.c
--- a/src/arch/x86/32/object/Makefile
+++ b/src/arch/x86/32/object/Makefile
@ -1,11 +0,0 @@
-#
-# 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)
-#
-
-ARCH_C_SOURCES += 32/object/objecttype.c
--- a/src/arch/x86/32/smp/Makefile
+++ b/src/arch/x86/32/smp/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-ARCH_C_SOURCES += 32/smp/ipi.c
--- a/src/arch/x86/64/Makefile
+++ b/src/arch/x86/64/Makefile
@ -1,24 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += src/arch/$(ARCH)/64
-
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/64/object/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/64/kernel/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/64/model/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/64/machine/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/64/smp/Makefile
-
-ARCH_C_SOURCES += 64/c_traps.c
-ARCH_ASM_SOURCES += 64/machine_asm.S \
-                    64/traps.S \
-                    64/head.S
--- a/src/arch/x86/64/kernel/Makefile
+++ b/src/arch/x86/64/kernel/Makefile
@ -1,15 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-ARCH_C_SOURCES += 64/kernel/thread.c \
-                  64/kernel/vspace.c \
-                  64/kernel/elf.c
--- a/src/arch/x86/64/machine/Makefile
+++ b/src/arch/x86/64/machine/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-ARCH_C_SOURCES += 64/machine/registerset.c
--- a/src/arch/x86/64/model/Makefile
+++ b/src/arch/x86/64/model/Makefile
@ -1,14 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-ARCH_C_SOURCES += 64/model/statedata.c \
-                  64/model/smp.c
--- a/src/arch/x86/64/object/Makefile
+++ b/src/arch/x86/64/object/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-ARCH_C_SOURCES += 64/object/objecttype.c
--- a/src/arch/x86/64/smp/Makefile
+++ b/src/arch/x86/64/smp/Makefile
@ -1,13 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-ARCH_C_SOURCES += 64/smp/ipi.c
--- a/src/arch/x86/Makefile
+++ b/src/arch/x86/Makefile
@ -1,23 +0,0 @@
-#
-# 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)
-#
-
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/api/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/object/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/kernel/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/model/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/machine/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/benchmark/Makefile
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/smp/Makefile
-
-include ${SOURCE_ROOT}/src/arch/$(ARCH)/${TYPE_SUFFIX}/Makefile
-
-ARCH_ASM_SOURCES += multiboot.S
-ARCH_C_SOURCES += c_traps.c \
-                  idle.c
--- a/src/arch/x86/api/Makefile
+++ b/src/arch/x86/api/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += src/arch/$(ARCH)/api
-
-ARCH_C_SOURCES += api/faults.c
--- a/src/arch/x86/benchmark/Makefile
+++ b/src/arch/x86/benchmark/Makefile
@ -1,15 +0,0 @@
-#
-# Copyright 2017, Data61
-# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
-# ABN 41 687 119 230.
-#
-# 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(DATA61_GPL)
-#
-
-DIRECTORIES += src/arch/$(ARCH)/benchmark
-
-ARCH_C_SOURCES += benchmark/benchmark.c
--- a/src/arch/x86/kernel/Makefile
+++ b/src/arch/x86/kernel/Makefile
@ -1,22 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += src/arch/$(ARCH)/kernel
-
-ARCH_C_SOURCES += kernel/vspace.c \
-                  kernel/apic.c \
-                  kernel/xapic.c \
-                  kernel/x2apic.c \
-                  kernel/boot_sys.c \
-                  kernel/smp_sys.c \
-                  kernel/boot.c \
-                  kernel/cmdline.c \
-                  kernel/ept.c  \
-                  kernel/thread.c
--- a/src/arch/x86/machine/Makefile
+++ b/src/arch/x86/machine/Makefile
@ -1,21 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += src/arch/$(ARCH)/machine
-
-ARCH_C_SOURCES += machine/hardware.c \
-                  machine/fpu.c \
-                  machine/cpu_identification.c \
-                  machine/breakpoint.c \
-                  machine/registerset.c
-
-ifdef DEBUG
-    ARCH_C_SOURCES += machine/capdl.c
-endif
--- a/src/arch/x86/model/Makefile
+++ b/src/arch/x86/model/Makefile
@ -1,13 +0,0 @@
-#
-# 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)
-#
-
-DIRECTORIES += src/arch/$(ARCH)/model
-
-ARCH_C_SOURCES += model/statedata.c
--- a/Show more
+++ b/Show more