From 72e675f1daac9e377ab48f1dd69dcbad125bc2bb Mon Sep 17 00:00:00 2001
From: Adam Felizzi <Adam.Felizzi@data61.csiro.au>
Date: Mon, 2 Jul 2018 15:55:12 +1000
Subject: [PATCH] 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.
---
Kconfig | 791 -----------------
Makefile | 802 ------------------
include/32/mode/Makefile | 15 -
include/64/mode/Makefile | 15 -
include/Makefile | 13 -
include/api/Makefile | 11 -
include/arch/arm/arch/Makefile | 11 -
include/arch/arm/arch/object/Makefile | 13 -
include/arch/riscv/arch/Makefile | 18 -
include/arch/riscv/arch/object/Makefile | 13 -
include/arch/x86/arch/Makefile | 11 -
include/arch/x86/arch/object/Makefile | 13 -
include/benchmark/Makefile | 13 -
include/plat/allwinnerA20/plat/Makefile | 11 -
.../plat/allwinnerA20/plat/machine/Makefile | 13 -
include/plat/am335x/plat/Makefile | 11 -
include/plat/am335x/plat/machine/Makefile | 13 -
include/plat/apq8064/plat/Makefile | 11 -
include/plat/apq8064/plat/machine/Makefile | 13 -
include/plat/bcm2837/plat/Makefile | 13 -
include/plat/bcm2837/plat/machine/Makefile | 15 -
include/plat/exynos4/plat/Makefile | 12 -
include/plat/exynos4/plat/machine/Makefile | 13 -
include/plat/exynos5/plat/Makefile | 12 -
include/plat/exynos5/plat/machine/Makefile | 13 -
include/plat/hikey/plat/Makefile | 11 -
include/plat/hikey/plat/machine/Makefile | 13 -
include/plat/imx31/plat/Makefile | 11 -
include/plat/imx31/plat/machine/Makefile | 13 -
include/plat/imx6/plat/Makefile | 11 -
include/plat/imx6/plat/machine/Makefile | 13 -
include/plat/imx7/plat/Makefile | 11 -
include/plat/imx7/plat/machine/Makefile | 13 -
include/plat/omap3/plat/Makefile | 11 -
include/plat/omap3/plat/machine/Makefile | 13 -
.../pc99/plat/32/plat_mode/machine/Makefile | 14 -
.../pc99/plat/64/plat_mode/machine/Makefile | 14 -
include/plat/pc99/plat/Makefile | 13 -
include/plat/pc99/plat/machine/Makefile | 11 -
include/plat/spike/plat/Makefile | 11 -
include/plat/spike/plat/machine/Makefile | 21 -
include/plat/tk1/plat/Makefile | 11 -
include/plat/tk1/plat/machine/Makefile | 13 -
include/plat/tx1/plat/Makefile | 13 -
include/plat/tx1/plat/machine/Makefile | 15 -
include/plat/zynq7000/plat/Makefile | 11 -
include/plat/zynq7000/plat/machine/Makefile | 13 -
include/plat/zynqmp/plat/Makefile | 13 -
include/plat/zynqmp/plat/machine/Makefile | 15 -
libsel4/Kbuild | 14 -
libsel4/Kconfig | 62 --
libsel4/Makefile | 139 ---
src/Makefile | 23 -
src/api/Makefile | 14 -
src/arch/arm/32/Makefile | 23 -
src/arch/arm/32/kernel/Makefile | 12 -
src/arch/arm/32/machine/Makefile | 17 -
src/arch/arm/32/model/Makefile | 11 -
src/arch/arm/32/object/Makefile | 11 -
src/arch/arm/64/Makefile | 24 -
src/arch/arm/64/kernel/Makefile | 14 -
src/arch/arm/64/machine/Makefile | 19 -
src/arch/arm/64/model/Makefile | 13 -
src/arch/arm/64/object/Makefile | 13 -
src/arch/arm/Kconfig | 96 ---
src/arch/arm/Makefile | 21 -
src/arch/arm/api/Makefile | 13 -
src/arch/arm/armv/armv6/Makefile | 18 -
src/arch/arm/armv/armv7-a/Makefile | 18 -
src/arch/arm/armv/armv8-a/Makefile | 18 -
src/arch/arm/benchmark/Makefile | 15 -
src/arch/arm/kernel/Makefile | 14 -
src/arch/arm/machine/Makefile | 43 -
src/arch/arm/object/Makefile | 13 -
src/arch/arm/smp/Makefile | 13 -
src/arch/riscv/Kconfig | 29 -
src/arch/riscv/Makefile | 28 -
src/arch/riscv/api/Makefile | 21 -
src/arch/riscv/kernel/Makefile | 23 -
src/arch/riscv/machine/Makefile | 21 -
src/arch/riscv/model/Makefile | 21 -
src/arch/riscv/object/Makefile | 21 -
src/arch/x86/32/Makefile | 22 -
src/arch/x86/32/kernel/Makefile | 14 -
src/arch/x86/32/machine/Makefile | 11 -
src/arch/x86/32/model/Makefile | 11 -
src/arch/x86/32/object/Makefile | 11 -
src/arch/x86/32/smp/Makefile | 13 -
src/arch/x86/64/Makefile | 24 -
src/arch/x86/64/kernel/Makefile | 15 -
src/arch/x86/64/machine/Makefile | 13 -
src/arch/x86/64/model/Makefile | 14 -
src/arch/x86/64/object/Makefile | 13 -
src/arch/x86/64/smp/Makefile | 13 -
src/arch/x86/Makefile | 23 -
src/arch/x86/api/Makefile | 13 -
src/arch/x86/benchmark/Makefile | 15 -
src/arch/x86/kernel/Makefile | 22 -
src/arch/x86/machine/Makefile | 21 -
src/arch/x86/model/Makefile | 13 -
src/arch/x86/object/Makefile | 19 -
src/arch/x86/smp/Makefile | 15 -
src/benchmark/Makefile | 16 -
src/fastpath/Makefile | 13 -
src/kernel/Makefile | 17 -
src/machine/Makefile | 15 -
src/model/Makefile | 15 -
src/object/Makefile | 16 -
src/plat/allwinnerA20/Makefile | 11 -
src/plat/allwinnerA20/machine/Makefile | 15 -
src/plat/am335x/Makefile | 11 -
src/plat/am335x/machine/Makefile | 15 -
src/plat/apq8064/Makefile | 11 -
src/plat/apq8064/machine/Makefile | 16 -
src/plat/bcm2837/Makefile | 13 -
src/plat/bcm2837/machine/Makefile | 18 -
src/plat/exynos4/Makefile | 11 -
src/plat/exynos4/machine/Makefile | 15 -
src/plat/exynos5/Makefile | 11 -
src/plat/exynos5/machine/Makefile | 17 -
src/plat/hikey/Makefile | 11 -
src/plat/hikey/machine/Makefile | 14 -
src/plat/imx31/Makefile | 11 -
src/plat/imx31/machine/Makefile | 13 -
src/plat/imx6/Makefile | 11 -
src/plat/imx6/machine/Makefile | 13 -
src/plat/imx7/Makefile | 11 -
src/plat/imx7/machine/Makefile | 14 -
src/plat/omap3/Makefile | 11 -
src/plat/omap3/machine/Makefile | 15 -
src/plat/pc99/Kconfig | 379 ---------
src/plat/pc99/Makefile | 11 -
src/plat/pc99/machine/Makefile | 19 -
src/plat/spike/Makefile | 19 -
src/plat/spike/machine/Makefile | 23 -
src/plat/tk1/Makefile | 11 -
src/plat/tk1/machine/Makefile | 16 -
src/plat/tx1/Makefile | 13 -
src/plat/tx1/machine/Makefile | 15 -
src/plat/zynq7000/Makefile | 11 -
src/plat/zynq7000/machine/Makefile | 11 -
src/plat/zynqmp/Makefile | 18 -
src/plat/zynqmp/machine/Makefile | 20 -
src/smp/Makefile | 16 -
144 files changed, 4329 deletions(-)
delete mode 100644 Kconfig
delete mode 100644 Makefile
delete mode 100644 include/32/mode/Makefile
delete mode 100644 include/64/mode/Makefile
delete mode 100644 include/Makefile
delete mode 100644 include/api/Makefile
delete mode 100644 include/arch/arm/arch/Makefile
delete mode 100644 include/arch/arm/arch/object/Makefile
delete mode 100644 include/arch/riscv/arch/Makefile
delete mode 100644 include/arch/riscv/arch/object/Makefile
delete mode 100644 include/arch/x86/arch/Makefile
delete mode 100644 include/arch/x86/arch/object/Makefile
delete mode 100644 include/benchmark/Makefile
delete mode 100755 include/plat/allwinnerA20/plat/Makefile
delete mode 100755 include/plat/allwinnerA20/plat/machine/Makefile
delete mode 100644 include/plat/am335x/plat/Makefile
delete mode 100644 include/plat/am335x/plat/machine/Makefile
delete mode 100644 include/plat/apq8064/plat/Makefile
delete mode 100644 include/plat/apq8064/plat/machine/Makefile
delete mode 100644 include/plat/bcm2837/plat/Makefile
delete mode 100644 include/plat/bcm2837/plat/machine/Makefile
delete mode 100644 include/plat/exynos4/plat/Makefile
delete mode 100644 include/plat/exynos4/plat/machine/Makefile
delete mode 100644 include/plat/exynos5/plat/Makefile
delete mode 100644 include/plat/exynos5/plat/machine/Makefile
delete mode 100755 include/plat/hikey/plat/Makefile
delete mode 100755 include/plat/hikey/plat/machine/Makefile
delete mode 100644 include/plat/imx31/plat/Makefile
delete mode 100644 include/plat/imx31/plat/machine/Makefile
delete mode 100644 include/plat/imx6/plat/Makefile
delete mode 100644 include/plat/imx6/plat/machine/Makefile
delete mode 100644 include/plat/imx7/plat/Makefile
delete mode 100644 include/plat/imx7/plat/machine/Makefile
delete mode 100644 include/plat/omap3/plat/Makefile
delete mode 100644 include/plat/omap3/plat/machine/Makefile
delete mode 100644 include/plat/pc99/plat/32/plat_mode/machine/Makefile
delete mode 100644 include/plat/pc99/plat/64/plat_mode/machine/Makefile
delete mode 100644 include/plat/pc99/plat/Makefile
delete mode 100644 include/plat/pc99/plat/machine/Makefile
delete mode 100644 include/plat/spike/plat/Makefile
delete mode 100644 include/plat/spike/plat/machine/Makefile
delete mode 100644 include/plat/tk1/plat/Makefile
delete mode 100644 include/plat/tk1/plat/machine/Makefile
delete mode 100644 include/plat/tx1/plat/Makefile
delete mode 100644 include/plat/tx1/plat/machine/Makefile
delete mode 100644 include/plat/zynq7000/plat/Makefile
delete mode 100644 include/plat/zynq7000/plat/machine/Makefile
delete mode 100644 include/plat/zynqmp/plat/Makefile
delete mode 100644 include/plat/zynqmp/plat/machine/Makefile
delete mode 100644 libsel4/Kbuild
delete mode 100644 libsel4/Kconfig
delete mode 100644 libsel4/Makefile
delete mode 100644 src/Makefile
delete mode 100644 src/api/Makefile
delete mode 100644 src/arch/arm/32/Makefile
delete mode 100644 src/arch/arm/32/kernel/Makefile
delete mode 100644 src/arch/arm/32/machine/Makefile
delete mode 100644 src/arch/arm/32/model/Makefile
delete mode 100644 src/arch/arm/32/object/Makefile
delete mode 100644 src/arch/arm/64/Makefile
delete mode 100644 src/arch/arm/64/kernel/Makefile
delete mode 100644 src/arch/arm/64/machine/Makefile
delete mode 100644 src/arch/arm/64/model/Makefile
delete mode 100644 src/arch/arm/64/object/Makefile
delete mode 100644 src/arch/arm/Kconfig
delete mode 100644 src/arch/arm/Makefile
delete mode 100644 src/arch/arm/api/Makefile
delete mode 100644 src/arch/arm/armv/armv6/Makefile
delete mode 100644 src/arch/arm/armv/armv7-a/Makefile
delete mode 100644 src/arch/arm/armv/armv8-a/Makefile
delete mode 100644 src/arch/arm/benchmark/Makefile
delete mode 100644 src/arch/arm/kernel/Makefile
delete mode 100644 src/arch/arm/machine/Makefile
delete mode 100644 src/arch/arm/object/Makefile
delete mode 100644 src/arch/arm/smp/Makefile
delete mode 100644 src/arch/riscv/Kconfig
delete mode 100644 src/arch/riscv/Makefile
delete mode 100644 src/arch/riscv/api/Makefile
delete mode 100644 src/arch/riscv/kernel/Makefile
delete mode 100644 src/arch/riscv/machine/Makefile
delete mode 100644 src/arch/riscv/model/Makefile
delete mode 100644 src/arch/riscv/object/Makefile
delete mode 100644 src/arch/x86/32/Makefile
delete mode 100644 src/arch/x86/32/kernel/Makefile
delete mode 100644 src/arch/x86/32/machine/Makefile
delete mode 100644 src/arch/x86/32/model/Makefile
delete mode 100644 src/arch/x86/32/object/Makefile
delete mode 100644 src/arch/x86/32/smp/Makefile
delete mode 100644 src/arch/x86/64/Makefile
delete mode 100644 src/arch/x86/64/kernel/Makefile
delete mode 100644 src/arch/x86/64/machine/Makefile
delete mode 100644 src/arch/x86/64/model/Makefile
delete mode 100644 src/arch/x86/64/object/Makefile
delete mode 100644 src/arch/x86/64/smp/Makefile
delete mode 100644 src/arch/x86/Makefile
delete mode 100644 src/arch/x86/api/Makefile
delete mode 100644 src/arch/x86/benchmark/Makefile
delete mode 100644 src/arch/x86/kernel/Makefile
delete mode 100644 src/arch/x86/machine/Makefile
delete mode 100644 src/arch/x86/model/Makefile
delete mode 100644 src/arch/x86/object/Makefile
delete mode 100644 src/arch/x86/smp/Makefile
delete mode 100644 src/benchmark/Makefile
delete mode 100644 src/fastpath/Makefile
delete mode 100644 src/kernel/Makefile
delete mode 100644 src/machine/Makefile
delete mode 100644 src/model/Makefile
delete mode 100644 src/object/Makefile
delete mode 100755 src/plat/allwinnerA20/Makefile
delete mode 100755 src/plat/allwinnerA20/machine/Makefile
delete mode 100644 src/plat/am335x/Makefile
delete mode 100644 src/plat/am335x/machine/Makefile
delete mode 100644 src/plat/apq8064/Makefile
delete mode 100644 src/plat/apq8064/machine/Makefile
delete mode 100644 src/plat/bcm2837/Makefile
delete mode 100644 src/plat/bcm2837/machine/Makefile
delete mode 100644 src/plat/exynos4/Makefile
delete mode 100644 src/plat/exynos4/machine/Makefile
delete mode 100644 src/plat/exynos5/Makefile
delete mode 100644 src/plat/exynos5/machine/Makefile
delete mode 100755 src/plat/hikey/Makefile
delete mode 100644 src/plat/hikey/machine/Makefile
delete mode 100644 src/plat/imx31/Makefile
delete mode 100644 src/plat/imx31/machine/Makefile
delete mode 100644 src/plat/imx6/Makefile
delete mode 100644 src/plat/imx6/machine/Makefile
delete mode 100644 src/plat/imx7/Makefile
delete mode 100644 src/plat/imx7/machine/Makefile
delete mode 100644 src/plat/omap3/Makefile
delete mode 100644 src/plat/omap3/machine/Makefile
delete mode 100644 src/plat/pc99/Kconfig
delete mode 100644 src/plat/pc99/Makefile
delete mode 100644 src/plat/pc99/machine/Makefile
delete mode 100644 src/plat/spike/Makefile
delete mode 100644 src/plat/spike/machine/Makefile
delete mode 100644 src/plat/tk1/Makefile
delete mode 100644 src/plat/tk1/machine/Makefile
delete mode 100644 src/plat/tx1/Makefile
delete mode 100644 src/plat/tx1/machine/Makefile
delete mode 100644 src/plat/zynq7000/Makefile
delete mode 100644 src/plat/zynq7000/machine/Makefile
delete mode 100755 src/plat/zynqmp/Makefile
delete mode 100644 src/plat/zynqmp/machine/Makefile
delete mode 100644 src/smp/Makefile
diff --git a/Kconfig b/Kconfig
deleted file mode 100644
index ea1ab25f0..000000000
--- a/Kconfig
+++ /dev/null
@@ -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
diff --git a/Makefile b/Makefile
deleted file mode 100644
index 37a6b0533..000000000
--- a/Makefile
+++ /dev/null
@@ -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
diff --git a/include/32/mode/Makefile b/include/32/mode/Makefile
deleted file mode 100644
index a0f6d8c23..000000000
--- a/include/32/mode/Makefile
+++ /dev/null
@@ -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
diff --git a/include/64/mode/Makefile b/include/64/mode/Makefile
deleted file mode 100644
index feba43e6c..000000000
--- a/include/64/mode/Makefile
+++ /dev/null
@@ -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
diff --git a/include/Makefile b/include/Makefile
deleted file mode 100644
index 444a244e3..000000000
--- a/include/Makefile
+++ /dev/null
@@ -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}
diff --git a/include/api/Makefile b/include/api/Makefile
deleted file mode 100644
index 3187ffb6a..000000000
--- a/include/api/Makefile
+++ /dev/null
@@ -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
diff --git a/include/arch/arm/arch/Makefile b/include/arch/arm/arch/Makefile
deleted file mode 100644
index 83ec1a4dc..000000000
--- a/include/arch/arm/arch/Makefile
+++ /dev/null
@@ -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
diff --git a/include/arch/arm/arch/object/Makefile b/include/arch/arm/arch/object/Makefile
deleted file mode 100644
index aebe5d31a..000000000
--- a/include/arch/arm/arch/object/Makefile
+++ /dev/null
@@ -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
diff --git a/include/arch/riscv/arch/Makefile b/include/arch/riscv/arch/Makefile
deleted file mode 100644
index ce3c265cc..000000000
--- a/include/arch/riscv/arch/Makefile
+++ /dev/null
@@ -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
diff --git a/include/arch/riscv/arch/object/Makefile b/include/arch/riscv/arch/object/Makefile
deleted file mode 100644
index aebe5d31a..000000000
--- a/include/arch/riscv/arch/object/Makefile
+++ /dev/null
@@ -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
diff --git a/include/arch/x86/arch/Makefile b/include/arch/x86/arch/Makefile
deleted file mode 100644
index ab5b5aeb8..000000000
--- a/include/arch/x86/arch/Makefile
+++ /dev/null
@@ -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
diff --git a/include/arch/x86/arch/object/Makefile b/include/arch/x86/arch/object/Makefile
deleted file mode 100644
index aebe5d31a..000000000
--- a/include/arch/x86/arch/object/Makefile
+++ /dev/null
@@ -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
diff --git a/include/benchmark/Makefile b/include/benchmark/Makefile
deleted file mode 100644
index 765e21c6e..000000000
--- a/include/benchmark/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/allwinnerA20/plat/Makefile b/include/plat/allwinnerA20/plat/Makefile
deleted file mode 100755
index c4af928dc..000000000
--- a/include/plat/allwinnerA20/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/allwinnerA20/plat/machine/Makefile b/include/plat/allwinnerA20/plat/machine/Makefile
deleted file mode 100755
index d53813681..000000000
--- a/include/plat/allwinnerA20/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/am335x/plat/Makefile b/include/plat/am335x/plat/Makefile
deleted file mode 100644
index 46c278954..000000000
--- a/include/plat/am335x/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/am335x/plat/machine/Makefile b/include/plat/am335x/plat/machine/Makefile
deleted file mode 100644
index 44c1a3f36..000000000
--- a/include/plat/am335x/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/apq8064/plat/Makefile b/include/plat/apq8064/plat/Makefile
deleted file mode 100644
index 46c278954..000000000
--- a/include/plat/apq8064/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/apq8064/plat/machine/Makefile b/include/plat/apq8064/plat/machine/Makefile
deleted file mode 100644
index 44c1a3f36..000000000
--- a/include/plat/apq8064/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/bcm2837/plat/Makefile b/include/plat/bcm2837/plat/Makefile
deleted file mode 100644
index d1f4f0aae..000000000
--- a/include/plat/bcm2837/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/bcm2837/plat/machine/Makefile b/include/plat/bcm2837/plat/machine/Makefile
deleted file mode 100644
index b6e917640..000000000
--- a/include/plat/bcm2837/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/exynos4/plat/Makefile b/include/plat/exynos4/plat/Makefile
deleted file mode 100644
index 56da6c6f8..000000000
--- a/include/plat/exynos4/plat/Makefile
+++ /dev/null
@@ -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/
diff --git a/include/plat/exynos4/plat/machine/Makefile b/include/plat/exynos4/plat/machine/Makefile
deleted file mode 100644
index 44c1a3f36..000000000
--- a/include/plat/exynos4/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/exynos5/plat/Makefile b/include/plat/exynos5/plat/Makefile
deleted file mode 100644
index 56da6c6f8..000000000
--- a/include/plat/exynos5/plat/Makefile
+++ /dev/null
@@ -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/
diff --git a/include/plat/exynos5/plat/machine/Makefile b/include/plat/exynos5/plat/machine/Makefile
deleted file mode 100644
index 44c1a3f36..000000000
--- a/include/plat/exynos5/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/hikey/plat/Makefile b/include/plat/hikey/plat/Makefile
deleted file mode 100755
index c4af928dc..000000000
--- a/include/plat/hikey/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/hikey/plat/machine/Makefile b/include/plat/hikey/plat/machine/Makefile
deleted file mode 100755
index d53813681..000000000
--- a/include/plat/hikey/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/imx31/plat/Makefile b/include/plat/imx31/plat/Makefile
deleted file mode 100644
index 46c278954..000000000
--- a/include/plat/imx31/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/imx31/plat/machine/Makefile b/include/plat/imx31/plat/machine/Makefile
deleted file mode 100644
index 44c1a3f36..000000000
--- a/include/plat/imx31/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/imx6/plat/Makefile b/include/plat/imx6/plat/Makefile
deleted file mode 100644
index 46c278954..000000000
--- a/include/plat/imx6/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/imx6/plat/machine/Makefile b/include/plat/imx6/plat/machine/Makefile
deleted file mode 100644
index 44c1a3f36..000000000
--- a/include/plat/imx6/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/imx7/plat/Makefile b/include/plat/imx7/plat/Makefile
deleted file mode 100644
index 46c278954..000000000
--- a/include/plat/imx7/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/imx7/plat/machine/Makefile b/include/plat/imx7/plat/machine/Makefile
deleted file mode 100644
index 44c1a3f36..000000000
--- a/include/plat/imx7/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/omap3/plat/Makefile b/include/plat/omap3/plat/Makefile
deleted file mode 100644
index 46c278954..000000000
--- a/include/plat/omap3/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/omap3/plat/machine/Makefile b/include/plat/omap3/plat/machine/Makefile
deleted file mode 100644
index 44c1a3f36..000000000
--- a/include/plat/omap3/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/pc99/plat/32/plat_mode/machine/Makefile b/include/plat/pc99/plat/32/plat_mode/machine/Makefile
deleted file mode 100644
index 5af7e826e..000000000
--- a/include/plat/pc99/plat/32/plat_mode/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/pc99/plat/64/plat_mode/machine/Makefile b/include/plat/pc99/plat/64/plat_mode/machine/Makefile
deleted file mode 100644
index ce9224c55..000000000
--- a/include/plat/pc99/plat/64/plat_mode/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/pc99/plat/Makefile b/include/plat/pc99/plat/Makefile
deleted file mode 100644
index c86f28a3e..000000000
--- a/include/plat/pc99/plat/Makefile
+++ /dev/null
@@ -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}
diff --git a/include/plat/pc99/plat/machine/Makefile b/include/plat/pc99/plat/machine/Makefile
deleted file mode 100644
index 2bc5516d0..000000000
--- a/include/plat/pc99/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/spike/plat/Makefile b/include/plat/spike/plat/Makefile
deleted file mode 100644
index 46c278954..000000000
--- a/include/plat/spike/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/spike/plat/machine/Makefile b/include/plat/spike/plat/machine/Makefile
deleted file mode 100644
index e12bb7865..000000000
--- a/include/plat/spike/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/tk1/plat/Makefile b/include/plat/tk1/plat/Makefile
deleted file mode 100644
index 0612070ab..000000000
--- a/include/plat/tk1/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/tk1/plat/machine/Makefile b/include/plat/tk1/plat/machine/Makefile
deleted file mode 100644
index 04583ad17..000000000
--- a/include/plat/tk1/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/tx1/plat/Makefile b/include/plat/tx1/plat/Makefile
deleted file mode 100644
index d1f4f0aae..000000000
--- a/include/plat/tx1/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/tx1/plat/machine/Makefile b/include/plat/tx1/plat/machine/Makefile
deleted file mode 100644
index b6e917640..000000000
--- a/include/plat/tx1/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/zynq7000/plat/Makefile b/include/plat/zynq7000/plat/Makefile
deleted file mode 100644
index 46c278954..000000000
--- a/include/plat/zynq7000/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/zynq7000/plat/machine/Makefile b/include/plat/zynq7000/plat/machine/Makefile
deleted file mode 100644
index 44c1a3f36..000000000
--- a/include/plat/zynq7000/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/zynqmp/plat/Makefile b/include/plat/zynqmp/plat/Makefile
deleted file mode 100644
index d1f4f0aae..000000000
--- a/include/plat/zynqmp/plat/Makefile
+++ /dev/null
@@ -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
diff --git a/include/plat/zynqmp/plat/machine/Makefile b/include/plat/zynqmp/plat/machine/Makefile
deleted file mode 100644
index b6e917640..000000000
--- a/include/plat/zynqmp/plat/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/libsel4/Kbuild b/libsel4/Kbuild
deleted file mode 100644
index 8afe1004e..000000000
--- a/libsel4/Kbuild
+++ /dev/null
@@ -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
diff --git a/libsel4/Kconfig b/libsel4/Kconfig
deleted file mode 100644
index 6b0aedebd..000000000
--- a/libsel4/Kconfig
+++ /dev/null
@@ -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
diff --git a/libsel4/Makefile b/libsel4/Makefile
deleted file mode 100644
index d6561f7db..000000000
--- a/libsel4/Makefile
+++ /dev/null
@@ -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 $@ $^
diff --git a/src/Makefile b/src/Makefile
deleted file mode 100644
index 3478df646..000000000
--- a/src/Makefile
+++ /dev/null
@@ -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
diff --git a/src/api/Makefile b/src/api/Makefile
deleted file mode 100644
index 3247d24aa..000000000
--- a/src/api/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/32/Makefile b/src/arch/arm/32/Makefile
deleted file mode 100644
index 6f1edf1af..000000000
--- a/src/arch/arm/32/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/32/kernel/Makefile b/src/arch/arm/32/kernel/Makefile
deleted file mode 100644
index 92dcac3fa..000000000
--- a/src/arch/arm/32/kernel/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/32/machine/Makefile b/src/arch/arm/32/machine/Makefile
deleted file mode 100644
index 6a38dbb09..000000000
--- a/src/arch/arm/32/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/32/model/Makefile b/src/arch/arm/32/model/Makefile
deleted file mode 100644
index b202ab2e7..000000000
--- a/src/arch/arm/32/model/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/32/object/Makefile b/src/arch/arm/32/object/Makefile
deleted file mode 100644
index 2b54c7bd9..000000000
--- a/src/arch/arm/32/object/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/64/Makefile b/src/arch/arm/64/Makefile
deleted file mode 100644
index a711273e0..000000000
--- a/src/arch/arm/64/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/64/kernel/Makefile b/src/arch/arm/64/kernel/Makefile
deleted file mode 100644
index b13353fe7..000000000
--- a/src/arch/arm/64/kernel/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/64/machine/Makefile b/src/arch/arm/64/machine/Makefile
deleted file mode 100644
index e1b4fab93..000000000
--- a/src/arch/arm/64/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/64/model/Makefile b/src/arch/arm/64/model/Makefile
deleted file mode 100644
index 5662bcfa5..000000000
--- a/src/arch/arm/64/model/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/64/object/Makefile b/src/arch/arm/64/object/Makefile
deleted file mode 100644
index 12ee152c5..000000000
--- a/src/arch/arm/64/object/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/Kconfig b/src/arch/arm/Kconfig
deleted file mode 100644
index 51d94a369..000000000
--- a/src/arch/arm/Kconfig
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/Makefile b/src/arch/arm/Makefile
deleted file mode 100644
index bf2433b90..000000000
--- a/src/arch/arm/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/api/Makefile b/src/arch/arm/api/Makefile
deleted file mode 100644
index a20c9391d..000000000
--- a/src/arch/arm/api/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/armv/armv6/Makefile b/src/arch/arm/armv/armv6/Makefile
deleted file mode 100644
index 0ee79a5c5..000000000
--- a/src/arch/arm/armv/armv6/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/armv/armv7-a/Makefile b/src/arch/arm/armv/armv7-a/Makefile
deleted file mode 100644
index 0ee79a5c5..000000000
--- a/src/arch/arm/armv/armv7-a/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/armv/armv8-a/Makefile b/src/arch/arm/armv/armv8-a/Makefile
deleted file mode 100644
index 8221b3b82..000000000
--- a/src/arch/arm/armv/armv8-a/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/benchmark/Makefile b/src/arch/arm/benchmark/Makefile
deleted file mode 100644
index e8cab5aad..000000000
--- a/src/arch/arm/benchmark/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/kernel/Makefile b/src/arch/arm/kernel/Makefile
deleted file mode 100644
index e64995124..000000000
--- a/src/arch/arm/kernel/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/machine/Makefile b/src/arch/arm/machine/Makefile
deleted file mode 100644
index 046232c73..000000000
--- a/src/arch/arm/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/object/Makefile b/src/arch/arm/object/Makefile
deleted file mode 100644
index 2dce17c98..000000000
--- a/src/arch/arm/object/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/arm/smp/Makefile b/src/arch/arm/smp/Makefile
deleted file mode 100644
index 34d387b2e..000000000
--- a/src/arch/arm/smp/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/riscv/Kconfig b/src/arch/riscv/Kconfig
deleted file mode 100644
index 28919143e..000000000
--- a/src/arch/riscv/Kconfig
+++ /dev/null
@@ -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.
diff --git a/src/arch/riscv/Makefile b/src/arch/riscv/Makefile
deleted file mode 100644
index 8dc5030e8..000000000
--- a/src/arch/riscv/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/riscv/api/Makefile b/src/arch/riscv/api/Makefile
deleted file mode 100644
index 10c11d064..000000000
--- a/src/arch/riscv/api/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/riscv/kernel/Makefile b/src/arch/riscv/kernel/Makefile
deleted file mode 100644
index 12ae7156d..000000000
--- a/src/arch/riscv/kernel/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/riscv/machine/Makefile b/src/arch/riscv/machine/Makefile
deleted file mode 100644
index 986200394..000000000
--- a/src/arch/riscv/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/riscv/model/Makefile b/src/arch/riscv/model/Makefile
deleted file mode 100644
index b2d206a16..000000000
--- a/src/arch/riscv/model/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/riscv/object/Makefile b/src/arch/riscv/object/Makefile
deleted file mode 100644
index 4c238fb6c..000000000
--- a/src/arch/riscv/object/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/32/Makefile b/src/arch/x86/32/Makefile
deleted file mode 100644
index abd46ff44..000000000
--- a/src/arch/x86/32/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/32/kernel/Makefile b/src/arch/x86/32/kernel/Makefile
deleted file mode 100644
index 67ac8f06f..000000000
--- a/src/arch/x86/32/kernel/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/32/machine/Makefile b/src/arch/x86/32/machine/Makefile
deleted file mode 100644
index 5121b7d26..000000000
--- a/src/arch/x86/32/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/32/model/Makefile b/src/arch/x86/32/model/Makefile
deleted file mode 100644
index b202ab2e7..000000000
--- a/src/arch/x86/32/model/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/32/object/Makefile b/src/arch/x86/32/object/Makefile
deleted file mode 100644
index 2b54c7bd9..000000000
--- a/src/arch/x86/32/object/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/32/smp/Makefile b/src/arch/x86/32/smp/Makefile
deleted file mode 100644
index e960ba5f0..000000000
--- a/src/arch/x86/32/smp/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/64/Makefile b/src/arch/x86/64/Makefile
deleted file mode 100644
index 6fc012612..000000000
--- a/src/arch/x86/64/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/64/kernel/Makefile b/src/arch/x86/64/kernel/Makefile
deleted file mode 100644
index acc336e23..000000000
--- a/src/arch/x86/64/kernel/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/64/machine/Makefile b/src/arch/x86/64/machine/Makefile
deleted file mode 100644
index b41a80806..000000000
--- a/src/arch/x86/64/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/64/model/Makefile b/src/arch/x86/64/model/Makefile
deleted file mode 100644
index a71e68d1f..000000000
--- a/src/arch/x86/64/model/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/64/object/Makefile b/src/arch/x86/64/object/Makefile
deleted file mode 100644
index 12ee152c5..000000000
--- a/src/arch/x86/64/object/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/64/smp/Makefile b/src/arch/x86/64/smp/Makefile
deleted file mode 100644
index 507b4d328..000000000
--- a/src/arch/x86/64/smp/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/Makefile b/src/arch/x86/Makefile
deleted file mode 100644
index 25335b1d8..000000000
--- a/src/arch/x86/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/api/Makefile b/src/arch/x86/api/Makefile
deleted file mode 100644
index 33e24d921..000000000
--- a/src/arch/x86/api/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/benchmark/Makefile b/src/arch/x86/benchmark/Makefile
deleted file mode 100644
index 0687da347..000000000
--- a/src/arch/x86/benchmark/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/kernel/Makefile b/src/arch/x86/kernel/Makefile
deleted file mode 100644
index f818ff657..000000000
--- a/src/arch/x86/kernel/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/machine/Makefile b/src/arch/x86/machine/Makefile
deleted file mode 100644
index 3bee19cd6..000000000
--- a/src/arch/x86/machine/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/model/Makefile b/src/arch/x86/model/Makefile
deleted file mode 100644
index c1efad616..000000000
--- a/src/arch/x86/model/Makefile
+++ /dev/null
@@ -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
diff --git a/src/arch/x86/object/Makefile b/src/arch/x86/object/Makefile
deleted file mode 100644
index 152663ffa..000000000
--- a/src/arch/x86/object/Makefile
+++ /dev/null
@@ -1,19 +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)/object
-
-ARCH_C_SOURCES += object/interrupt.c \
- object/ioport.c \
- object/objecttype.c \
- object/tcb.c
-
-ARCH_C_SOURCES += object/iospace.c \
- object/vcpu.c
diff --git a/src/arch/x86/smp/Makefile b/src/arch/x86/smp/Makefile
deleted file mode 100644
index 90d070933..000000000
--- a/src/arch/x86/smp/Makefile
+++ /dev/null
@@ -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)/smp
-
-ARCH_C_SOURCES += smp/ipi.c
diff --git a/src/benchmark/Makefile b/src/benchmark/Makefile
deleted file mode 100644
index 932f233fe..000000000
--- a/src/benchmark/Makefile
+++ /dev/null
@@ -1,16 +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/benchmark
-
-C_SOURCES += src/benchmark/benchmark_track.c
-C_SOURCES += src/benchmark/benchmark_utilisation.c
diff --git a/src/fastpath/Makefile b/src/fastpath/Makefile
deleted file mode 100644
index d077ab6b3..000000000
--- a/src/fastpath/Makefile
+++ /dev/null
@@ -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/fastpath
-
-C_SOURCES += src/fastpath/fastpath.c
diff --git a/src/kernel/Makefile b/src/kernel/Makefile
deleted file mode 100644
index 00314242a..000000000
--- a/src/kernel/Makefile
+++ /dev/null
@@ -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)
-#
-
-DIRECTORIES += src/kernel
-
-C_SOURCES += src/kernel/cspace.c \
- src/kernel/faulthandler.c \
- src/kernel/thread.c \
- src/kernel/boot.c \
- src/kernel/stack.c
diff --git a/src/machine/Makefile b/src/machine/Makefile
deleted file mode 100644
index 07abb2c0c..000000000
--- a/src/machine/Makefile
+++ /dev/null
@@ -1,15 +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/machine
-
-C_SOURCES += src/machine/io.c
-C_SOURCES += src/machine/registerset.c
-C_SOURCES += src/machine/fpu.c
diff --git a/src/model/Makefile b/src/model/Makefile
deleted file mode 100644
index d76ab03e3..000000000
--- a/src/model/Makefile
+++ /dev/null
@@ -1,15 +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/model
-
-C_SOURCES += src/model/preemption.c \
- src/model/statedata.c \
- src/model/smp.c
diff --git a/src/object/Makefile b/src/object/Makefile
deleted file mode 100644
index 59ef76fa0..000000000
--- a/src/object/Makefile
+++ /dev/null
@@ -1,16 +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/object
-
-C_SOURCES += src/object/notification.c src/object/cnode.c \
- src/object/endpoint.c src/object/interrupt.c \
- src/object/objecttype.c src/object/tcb.c \
- src/object/untyped.c
diff --git a/src/plat/allwinnerA20/Makefile b/src/plat/allwinnerA20/Makefile
deleted file mode 100755
index 417c13004..000000000
--- a/src/plat/allwinnerA20/Makefile
+++ /dev/null
@@ -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}/src/plat/allwinnerA20/machine/Makefile
diff --git a/src/plat/allwinnerA20/machine/Makefile b/src/plat/allwinnerA20/machine/Makefile
deleted file mode 100755
index 7bdeb6e7c..000000000
--- a/src/plat/allwinnerA20/machine/Makefile
+++ /dev/null
@@ -1,15 +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 += src/plat/allwinnerA20/machine
-
-PLAT_C_SOURCES += machine/hardware.c \
- machine/l2cache.c \
- machine/io.c
diff --git a/src/plat/am335x/Makefile b/src/plat/am335x/Makefile
deleted file mode 100644
index 8008d3509..000000000
--- a/src/plat/am335x/Makefile
+++ /dev/null
@@ -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}/src/plat/am335x/machine/Makefile
diff --git a/src/plat/am335x/machine/Makefile b/src/plat/am335x/machine/Makefile
deleted file mode 100644
index 45b6e3c2f..000000000
--- a/src/plat/am335x/machine/Makefile
+++ /dev/null
@@ -1,15 +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/plat/am335x/machine
-
-PLAT_C_SOURCES += machine/hardware.c \
- machine/l2cache.c \
- machine/io.c
diff --git a/src/plat/apq8064/Makefile b/src/plat/apq8064/Makefile
deleted file mode 100644
index b1c5c0719..000000000
--- a/src/plat/apq8064/Makefile
+++ /dev/null
@@ -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}/src/plat/${PLAT}/machine/Makefile
diff --git a/src/plat/apq8064/machine/Makefile b/src/plat/apq8064/machine/Makefile
deleted file mode 100644
index 7c2611d95..000000000
--- a/src/plat/apq8064/machine/Makefile
+++ /dev/null
@@ -1,16 +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/plat/${PLAT}/machine
-
-PLAT_C_SOURCES += machine/hardware.c \
- machine/timer.c \
- machine/l2cache.c \
- machine/io.c
diff --git a/src/plat/bcm2837/Makefile b/src/plat/bcm2837/Makefile
deleted file mode 100644
index 8e03fc034..000000000
--- a/src/plat/bcm2837/Makefile
+++ /dev/null
@@ -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}/src/plat/${PLAT}/machine/Makefile
diff --git a/src/plat/bcm2837/machine/Makefile b/src/plat/bcm2837/machine/Makefile
deleted file mode 100644
index fae765135..000000000
--- a/src/plat/bcm2837/machine/Makefile
+++ /dev/null
@@ -1,18 +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/plat/${PLAT}/machine
-
-PLAT_C_SOURCES += machine/hardware.c \
- machine/l2cache.c \
- machine/intc.c \
- machine/io.c
diff --git a/src/plat/exynos4/Makefile b/src/plat/exynos4/Makefile
deleted file mode 100644
index b1c5c0719..000000000
--- a/src/plat/exynos4/Makefile
+++ /dev/null
@@ -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}/src/plat/${PLAT}/machine/Makefile
diff --git a/src/plat/exynos4/machine/Makefile b/src/plat/exynos4/machine/Makefile
deleted file mode 100644
index aae4b314e..000000000
--- a/src/plat/exynos4/machine/Makefile
+++ /dev/null
@@ -1,15 +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/plat/${PLAT}/machine
-DIRECTORIES += src/plat/exynos_common
-
-PLAT_C_SOURCES += ../exynos_common/io.c
-PLAT_C_SOURCES += machine/hardware.c
diff --git a/src/plat/exynos5/Makefile b/src/plat/exynos5/Makefile
deleted file mode 100644
index b1c5c0719..000000000
--- a/src/plat/exynos5/Makefile
+++ /dev/null
@@ -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}/src/plat/${PLAT}/machine/Makefile
diff --git a/src/plat/exynos5/machine/Makefile b/src/plat/exynos5/machine/Makefile
deleted file mode 100644
index 4a9645123..000000000
--- a/src/plat/exynos5/machine/Makefile
+++ /dev/null
@@ -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)
-#
-
-DIRECTORIES += src/plat/${PLAT}/machine
-DIRECTORIES += src/plat/exynos_common
-
-PLAT_C_SOURCES += machine/hardware.c \
- machine/l2cache.c
-
-PLAT_C_SOURCES += ../exynos_common/io.c
diff --git a/src/plat/hikey/Makefile b/src/plat/hikey/Makefile
deleted file mode 100755
index 1a52eae9a..000000000
--- a/src/plat/hikey/Makefile
+++ /dev/null
@@ -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}/src/plat/${PLAT}/machine/Makefile
diff --git a/src/plat/hikey/machine/Makefile b/src/plat/hikey/machine/Makefile
deleted file mode 100644
index 46f1fceb5..000000000
--- a/src/plat/hikey/machine/Makefile
+++ /dev/null
@@ -1,14 +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 += src/plat/hikey/machine
-
-PLAT_C_SOURCES += machine/hardware.c machine/io.c
-
diff --git a/src/plat/imx31/Makefile b/src/plat/imx31/Makefile
deleted file mode 100644
index c8d706242..000000000
--- a/src/plat/imx31/Makefile
+++ /dev/null
@@ -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}/src/plat/imx31/machine/Makefile
diff --git a/src/plat/imx31/machine/Makefile b/src/plat/imx31/machine/Makefile
deleted file mode 100644
index d657a1467..000000000
--- a/src/plat/imx31/machine/Makefile
+++ /dev/null
@@ -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/plat/${PLAT}/machine
-
-PLAT_C_SOURCES += machine/hardware.c machine/io.c
diff --git a/src/plat/imx6/Makefile b/src/plat/imx6/Makefile
deleted file mode 100644
index b1c5c0719..000000000
--- a/src/plat/imx6/Makefile
+++ /dev/null
@@ -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}/src/plat/${PLAT}/machine/Makefile
diff --git a/src/plat/imx6/machine/Makefile b/src/plat/imx6/machine/Makefile
deleted file mode 100644
index eca30a028..000000000
--- a/src/plat/imx6/machine/Makefile
+++ /dev/null
@@ -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/plat/${PLAT}/machine
-
-PLAT_C_SOURCES += machine/io.c
diff --git a/src/plat/imx7/Makefile b/src/plat/imx7/Makefile
deleted file mode 100644
index b1c5c0719..000000000
--- a/src/plat/imx7/Makefile
+++ /dev/null
@@ -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}/src/plat/${PLAT}/machine/Makefile
diff --git a/src/plat/imx7/machine/Makefile b/src/plat/imx7/machine/Makefile
deleted file mode 100644
index 88c7afac7..000000000
--- a/src/plat/imx7/machine/Makefile
+++ /dev/null
@@ -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/plat/${PLAT}/machine
-
-PLAT_C_SOURCES += machine/hardware.c \
- machine/io.c
diff --git a/src/plat/omap3/Makefile b/src/plat/omap3/Makefile
deleted file mode 100644
index b5cfb4952..000000000
--- a/src/plat/omap3/Makefile
+++ /dev/null
@@ -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}/src/plat/omap3/machine/Makefile
diff --git a/src/plat/omap3/machine/Makefile b/src/plat/omap3/machine/Makefile
deleted file mode 100644
index 5657c1537..000000000
--- a/src/plat/omap3/machine/Makefile
+++ /dev/null
@@ -1,15 +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/plat/omap3/machine
-
-PLAT_C_SOURCES += machine/hardware.c \
- machine/l2cache.c \
- machine/io.c
diff --git a/src/plat/pc99/Kconfig b/src/plat/pc99/Kconfig
deleted file mode 100644
index 23fddb02f..000000000
--- a/src/plat/pc99/Kconfig
+++ /dev/null
@@ -1,379 +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)
-#
-
-menu "System Interrupt Management"
- depends on PLAT_PC99
- choice
- prompt "IRQ Controller"
- default IRQ_PIC if ARCH_IA32
- default IRQ_IOAPIC if ARCH_X86_64
- help
- Select the IRQ controller seL4 will use. Code for others may
- still be included if needed to disable at run time
- config IRQ_PIC
- bool "PIC"
- help
- Use the legacy PIC controller
- config IRQ_IOAPIC
- bool "IOAPIC"
- help
- Use one or more IOAPIC controllers
- endchoice
-
- config MAX_NUM_IOAPIC
- prompt "Max supported IOAPICs"
- depends on IRQ_IOAPIC
- int
- default 1
- help
- Configure the maximum number of IOAPIC controllers that can
- be supported. SeL4 will detect IOAPICs regardless of whether
- the IOAPIC will actually be used as the final IRQ controller
-
- choice
- prompt "Local APIC mode"
- default XAPIC if ARCH_IA32
- default X2APIC if ARCH_X86_64
- help
- Select the mode local APIC will use. Not all machines support
- X2APIC mode.
- config XAPIC
- bool "XAPIC"
- help
- Use XAPIC mode for local APIC
- config X2APIC
- bool "X2APIC"
- help
- Use X2APIC mode for local APIC
- endchoice
-
- config USE_LOGICAL_IDS
- bool "Use logical IDs for IPIs broadcasting"
- depends on MAX_NUM_NODES != 1
- default n
- help
- Use logical IDs to broadcast IPI between cores. Not all machines
- support logical IDs. In xAPIC mode only 8 cores can be addressed
- using logical IDs.
-endmenu
-
-config IOMMU
- bool "IOMMU support"
- depends on PLAT_PC99 && !VERIFICATION_BUILD
- default y
- help
- IOMMU support for VT-d enabled chipset
-
-config VTX
- bool "VTX support"
- depends on PLAT_PC99 && !VERIFICATION_BUILD
- default n
- help
- VTX support
-
-config MAX_VPIDS
- prompt "Max VPIDs to support"
- depends on VTX
- range 1 65535
- int
- default 1024
- help
- The kernel maintains a mapping of 16-bit VPIDs to VCPUs. This option
- should be sized as small as possible to save memory, but be at least
- the number of VCPUs that will be run for optimum performance
-
-config HUGE_PAGE
- bool "Use 1GB Huge Page"
- depends on ARCH_X86_64
- default y
- help
- Add support for 1GB huge page. Not all recent processor models support
- this feature.
-
-config SUPPORT_PCID
- bool "Support Process Context IDentifiers"
- depends on ARCH_X86_64
- default y
- help
- Add support for PCIDs (aka hardware ASIDs). Not all processor models
- support this feature
-
-choice
- prompt "Kernel syscall style"
- depends on ARCH_X86
- default SYSENTER if ARCH_IA32
- default SYSCALL if ARCH_X86_64
- help
- The kernel only ever supports one method of performing syscalls
- at a time. This config should be set to the most efficient one
- that is support by the hardware the system will run on
-
- config SYSENTER
- bool "sysenter+sysexit"
- config SYSCALL
- depends on ARCH_X86_64
- bool "syscall+sysret"
-endchoice
-
-choice
- prompt "FPU state implementation"
- depends on ARCH_X86
- default FXSAVE
- help
- Choose the method that FPU state is stored in. This directly
- affects the method used to save and rrestore it
- config FXSAVE
- bool "FXSAVE"
- help
- This chooses the legacy 512-byte region used by the
- fxsave and fxrstor functions
- config XSAVE
- bool "XSAVE"
- help
- This chooses the variable xsave region, and enables the
- ability to use any of the xsave variants to save and
- restore. The actual size of the region is dependent on
- the features enabled.
-endchoice
-
-choice
- prompt "XSAVE variant"
- depends on XSAVE
- default XSAVE_XSAVEOPT
- help
- The XSAVE area supports multiple instructions to save
- and restore to it. These instructions are dependent upon
- specific CPU support. See Chapter 13 of Volume 1 of the
- Intel Architectures SOftware Developers Manual for
- discussion on the init and modified optimizations
-
- config XSAVE_XSAVE
- bool "XSAVE"
- help
- Original XSAVE instruction. This is the only XSAVE
- instruction that is guaranteed to exist if XSAVE
- is present
- config XSAVE_XSAVEC
- bool "XSAVEC"
- help
- Save state with compaction. This compaction has
- to do with minimizing the total size of XSAVE buffer,
- if using non contiguous features, XSAVEC will attempt
- to use the init optimization when saving
- config XSAVE_XSAVEOPT
- bool "XSAVEOPT"
- help
- Save state taking advantage of both the init
- optimization and modified optimization
- config XSAVE_XSAVES
- bool "XSAVES"
- help
- Save state taking advantage of the modified
- optimization. This instruction is only
- available in OS code, and is the preferred
- save method if it exists
-endchoice
-
-config XSAVE_FEATURE_SET
- int "XSAVE feature set"
- depends on XSAVE
- default 3
- help
- XSAVE can save and restore the state for various
- features through the use of the feature mask. This
- config option represents the feature mask that we
- want to support. The CPU must support all bits
- in this feature mask. Current known bits are
- 0 - FPU
- 1 - SSE
- 2 - AVX
- FPU and SSE is guaranteed to exist if XSAVE exists
-
-config XSAVE_SIZE
- int "XSAVE region size"
- depends on ARCH_X86
- default 576 if XSAVE
- default 512 if !XSAVE
- help
- The size of the XSAVE region. This is dependent
- upon the features in XSAVE_FEATURE_SET that have
- been requested. Default is 576 for the FPU and
- SSE state, unless XSAVE is not in use then it
- should be 512 for the legacy FXSAVE region
-
-choice
- prompt "Setting FS/GS Base Addresses"
- depends on ARCH_X86
- default FSGSBASE_INST if ARCH_X86_64
- default FSGSBASE_GDT if ARCH_IA32
- help
- There are three ways to to set FS/GS base addresses:
- IA32_FS/GS_GDT, IA32_FS/GS_BASE_MSR, and fsgsbase instructions.
- IA32_FS/GS_GDT and IA32_FS/GS_BASE_MSR are availble for 32-bit.
- IA32_FS/GS_BASE_MSR and fsgsbase instructions are available for 64-bit.
-
- config FSGSBASE_GDT
- bool "IA32_FS/GS_GDT"
- depends on ARCH_IA32
- help
- Use GDT entries.
-
- config FSGSBASE_MSR
- bool "IA32_FS/GS_BASE MSRs"
- depends on ARCH_X86
- help
- Use MSRs to change base addresses.
-
- config FSGSBASE_INST
- bool "FSGSBASE Instructions"
- depends on ARCH_X86_64
- help
- Use rdfs/gsbase, wrfs/gsbase instructions to change base adddresses.
-endchoice
-
-menu "Multiboot options"
-depends on PLAT_PC99
- config MULTIBOOT1_HEADER
- bool "Insert multiboot1 compatible header"
- default y
- help
- When enabled inserts a header that indicates to the bootloader that the kernel
- supports a multiboot 1 boot header
- config MULTIBOOT2_HEADER
- bool "Insert multiboot2 compatible header"
- default y
- help
- When enabled inserts a header thatn indicates to the bootloader that the kernel
- supports a mutliboot 2 boot header. This is can be enabled together with a
- multiboot 1 header and the boot loader may use either one
- choice
- prompt "Multiboot graphics mode"
- help
- The type of graphics mode to request from the boot loader.
- This is encoded into the multiboot header and is merely a hint,
- the boot loader is free to ignore or set some other mode
- default MULTIBOOT_GRAPHICS_MODE_NONE
- config MULTIBOOT_GRAPHICS_MODE_NONE
- bool "None"
- help
- Request no graphics mode
- config MULTIBOOT_GRAPHICS_MODE_TEXT
- bool "Text"
- help
- Request a text mode
- config MULTIBOOT_GRAPHICS_MODE_LINEAR
- bool "Linear"
- help
- Request a linear graphics mode
- endchoice
- config MULTIBOOT_GRAPHICS_MODE_WIDTH
- int "Mode Width"
- depends on MULTIBOOT_GRAPHICS_MODE_TEXT || MULTIBOOT_GRAPHICS_MODE_LINEAR
- default 80 if MULTIBOOT_GRAPHICS_MODE_TEXT
- default 1024 if MULTIBOOT_GRAPHICS_MODE_LINEAR
- help
- The width of the graphics mode to request. For a linear graphics mode this
- is the number of pixels. For a text mode this is the number of characters.
- Value of zero indicates no preference
- config MULTIBOOT_GRAPHICS_MODE_HEIGHT
- int "Mode Height"
- depends on MULTIBOOT_GRAPHICS_MODE_TEXT || MULTIBOOT_GRAPHICS_MODE_LINEAR
- default 25 if MULTIBOOT_GRAPHICS_MODE_TEXT
- default 768 if MULTIBOOT_GRAPHICS_MODE_LINEAR
- help
- The height of the graphics mode to request. For a linear graphics mode this
- is the number of pixels. For a text mode this is the number of characters
- Value of zero indicates no preference
- config MULTIBOOT_GRAPHICS_MODE_DEPTH
- int "Mode Depth"
- depends on MULTIBOOT_GRAPHICS_MODE_LINEAR
- default 32
- help
- The bits per pixel of the linear graphics mode to request.
- Value of zero indicates no preference
-endmenu
-
-config KERNEL_SKIM_WINDOW
- bool "Kernel Static Kernel Image and Micro-state (SKIM) window"
- depends on ARCH_X86_64
- default y
- help
- Prevent against the Meltdown vulnerability by using a reduced Static Kernel
- Image and Micro-state window instead of having all kernel state in the kernel window.
- This only needs to be enabled if deploying to a vulnerable processor
-
-config EXPORT_PMC_USER
- bool "User access to PMC"
- depends on ARCH_X86 && !VERIFICATION_BUILD
- default n
- help
- Grant user access to the Performance Monitoring Counters.
- This allows the user to read performance counters, although
- not control what the counters are and whether or not they
- are counting. Nevertheless whilst this is useful for
- evalulating performance this option opens timing and covert
- channels.
-
-config KERNEL_X86_DANGEROUS_MSR
- bool "rdmsr/wrmsr kernel interface"
- depends on ARCH_X86 && !VERIFICATION_BUILD
- default n
- help
- Provides a syscall interface for reading and writing arbitrary MSRs.
- This is extremely dangerous as no checks are performed and exists
- to aid debugging and benchmarking
-
-choice
- prompt "Indirect Branch Restricted Speculation mode"
- help
- Used to prevent a user from manipulating the branch predictor to manipulate speculative
- execution of other processes. On current processors IBRS has a prohibitive performance
- penalty and it is recommended that it be disabled such that software mitigations are
- used instead. Software mitigation is done by disabling jump tables (the only form of
- indirect jump in seL4 except for 'ret') and flushing the RSB on vmexit. Flushing the RSB
- at other times is not needed as seL4 does not switch kernel stacks and so is not
- vulernable to RSB underflow. The STIBP is essentially software mitigation but enables
- the single thread isolation for branch predictions. This is only needed if attempting
- to protect user level process from each other in a multicore environment.
- default KERNEL_X86_IBRS_NONE
- config KERNEL_X86_IBRS_NONE
- bool "None"
- depends on ARCH_X86
- config KERNEL_X86_IBRS_STIBP
- bool "Only STIBP"
- depends on ARCH_X86 && MAX_NUM_NODES != 1
- config KERNEL_X86_IBRS_BASIC
- bool "Basic"
- depends on ARCH_X86
- config KERNEL_X86_IBRS_ALL
- bool "All"
- depends on ARCH_X86
-endchoice
-
-config KERNEL_X86_IBPB_ON_CONTEXT_SWITCH
- bool "Branch prediction barrier on context switch"
- depends on ARCH_X86
- default n
- help
- Performs a IBPB on every context switch to prevent Spectre attacks between user
- processes. This is extremely expensive and is recommended you only turn this on
- if absolutely necessary.
- Note that in a multicore environment you should also enable STIBP to prevent
- other cores retraining the branch predictor even after context switch.
-
-config KERNEL_X86_RSB_ON_CONTEXT_SWITCH
- bool "Flush RSB on context switch"
- depends on ARCH_X86
- default n
- help
- Flushes the RSB on context switch to prevent Spectre attacks between user processes.
- Whilst not nearly as expensive as an IBPB it is not enabled by default as it is
- largely pointless to flush the RSB without also doing an IBPB as the RSB is already
- a harder attack vector.
diff --git a/src/plat/pc99/Makefile b/src/plat/pc99/Makefile
deleted file mode 100644
index a1360de7c..000000000
--- a/src/plat/pc99/Makefile
+++ /dev/null
@@ -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}/src/plat/$(PLAT)/machine/Makefile
diff --git a/src/plat/pc99/machine/Makefile b/src/plat/pc99/machine/Makefile
deleted file mode 100644
index df9af3f8b..000000000
--- a/src/plat/pc99/machine/Makefile
+++ /dev/null
@@ -1,19 +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/plat/$(PLAT)/machine
-
-PLAT_C_SOURCES += machine/acpi.c \
- machine/hardware.c \
- machine/pic.c \
- machine/ioapic.c \
- machine/pit.c \
- machine/io.c \
- machine/intel-vtd.c
diff --git a/src/plat/spike/Makefile b/src/plat/spike/Makefile
deleted file mode 100644
index 1431469f4..000000000
--- a/src/plat/spike/Makefile
+++ /dev/null
@@ -1,19 +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}/src/plat/${PLAT}/machine/Makefile
diff --git a/src/plat/spike/machine/Makefile b/src/plat/spike/machine/Makefile
deleted file mode 100644
index 554d4755a..000000000
--- a/src/plat/spike/machine/Makefile
+++ /dev/null
@@ -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/plat/${PLAT}/machine
-
-PLAT_C_SOURCES += machine/hardware.c
-
-PLAT_C_SOURCES += machine/fdt.c
diff --git a/src/plat/tk1/Makefile b/src/plat/tk1/Makefile
deleted file mode 100644
index 9dd81efab..000000000
--- a/src/plat/tk1/Makefile
+++ /dev/null
@@ -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}/src/plat/$(PLAT)/machine/Makefile
diff --git a/src/plat/tk1/machine/Makefile b/src/plat/tk1/machine/Makefile
deleted file mode 100644
index c5cf608ff..000000000
--- a/src/plat/tk1/machine/Makefile
+++ /dev/null
@@ -1,16 +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 += src/plat/$(PLAT)/machine
-
-PLAT_C_SOURCES += machine/hardware.c \
- machine/l2cache.c \
- machine/smmu.c \
- machine/io.c
diff --git a/src/plat/tx1/Makefile b/src/plat/tx1/Makefile
deleted file mode 100644
index 8e03fc034..000000000
--- a/src/plat/tx1/Makefile
+++ /dev/null
@@ -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}/src/plat/${PLAT}/machine/Makefile
diff --git a/src/plat/tx1/machine/Makefile b/src/plat/tx1/machine/Makefile
deleted file mode 100644
index ceab09e1a..000000000
--- a/src/plat/tx1/machine/Makefile
+++ /dev/null
@@ -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/plat/hikey/machine
-
-PLAT_C_SOURCES += machine/hardware.c machine/io.c machine/l2cache.c
diff --git a/src/plat/zynq7000/Makefile b/src/plat/zynq7000/Makefile
deleted file mode 100644
index b1c5c0719..000000000
--- a/src/plat/zynq7000/Makefile
+++ /dev/null
@@ -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}/src/plat/${PLAT}/machine/Makefile
diff --git a/src/plat/zynq7000/machine/Makefile b/src/plat/zynq7000/machine/Makefile
deleted file mode 100644
index 36753b6ca..000000000
--- a/src/plat/zynq7000/machine/Makefile
+++ /dev/null
@@ -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)
-#
-
-PLAT_C_SOURCES += machine/io.c
diff --git a/src/plat/zynqmp/Makefile b/src/plat/zynqmp/Makefile
deleted file mode 100755
index 035063410..000000000
--- a/src/plat/zynqmp/Makefile
+++ /dev/null
@@ -1,18 +0,0 @@
-#
-# Copyright 2017, DornerWorks
-#
-# 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(DORNERWORKS_GPL)
-#
-
-#
-# This data was produced by DornerWorks, Ltd. of Grand Rapids, MI, USA under
-# a DARPA SBIR, Contract Number D16PC00107.
-#
-# Approved for Public Release, Distribution Unlimited.
-#
-
-include ${SOURCE_ROOT}/src/plat/${PLAT}/machine/Makefile
diff --git a/src/plat/zynqmp/machine/Makefile b/src/plat/zynqmp/machine/Makefile
deleted file mode 100644
index 21e1ac613..000000000
--- a/src/plat/zynqmp/machine/Makefile
+++ /dev/null
@@ -1,20 +0,0 @@
-#
-# Copyright 2017, DornerWorks
-#
-# 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(DORNERWORKS_GPL)
-#
-
-#
-# This data was produced by DornerWorks, Ltd. of Grand Rapids, MI, USA under
-# a DARPA SBIR, Contract Number D16PC00107.
-#
-# Approved for Public Release, Distribution Unlimited.
-#
-
-DIRECTORIES += src/plat/zynqmp/machine
-
-PLAT_C_SOURCES += machine/hardware.c machine/io.c
diff --git a/src/smp/Makefile b/src/smp/Makefile
deleted file mode 100644
index 04fe94290..000000000
--- a/src/smp/Makefile
+++ /dev/null
@@ -1,16 +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/smp
-
-C_SOURCES += src/smp/lock.c \
- src/smp/ipi.c
--
GitLab