From 0b73072016e4898f6e08bd4a2c061c86bbaffc5f Mon Sep 17 00:00:00 2001
From: Adrian Danis <Adrian.Danis@data61.csiro.au>
Date: Fri, 17 Mar 2017 09:42:18 +1100
Subject: [PATCH] Add a CMake based build system
This commit adds an alternate build system using CMake that operates indepenently of
the existing Kconfig+Kbuild+make based build system
---
CMakeLists.txt | 380 +++++++++++++++++++
config.cmake | 245 +++++++++++++
configs/arm_verified.cmake | 26 ++
gcc.cmake | 34 ++
include/32/mode/config.cmake | 15 +
include/64/mode/config.cmake | 15 +
include/arch/arm/armv/armv7ve | 1 +
libsel4/CMakeLists.txt | 152 ++++++++
src/arch/arm/32/config.cmake | 37 ++
src/arch/arm/64/config.cmake | 32 ++
src/arch/arm/armv/armv6/config.cmake | 24 ++
src/arch/arm/armv/armv7-a/config.cmake | 24 ++
src/arch/arm/armv/armv8-a/config.cmake | 24 ++
src/arch/arm/config.cmake | 334 +++++++++++++++++
src/arch/x86/32/config.cmake | 32 ++
src/arch/x86/64/config.cmake | 32 ++
src/arch/x86/config.cmake | 262 +++++++++++++
src/config.cmake | 44 +++
src/plat/am335x/config.cmake | 27 ++
src/plat/apq8064/config.cmake | 29 ++
src/plat/bcm2837/config.cmake | 29 ++
src/plat/exynos4/config.cmake | 27 ++
src/plat/exynos5/config.cmake | 38 ++
src/plat/hikey/config.cmake | 76 ++++
src/plat/imx31/config.cmake | 27 ++
src/plat/imx6/config.cmake | 28 ++
src/plat/omap3/config.cmake | 28 ++
src/plat/pc99/config.cmake | 43 +++
src/plat/tk1/config.cmake | 30 ++
src/plat/tx1/config.cmake | 29 ++
src/plat/zynq7000/config.cmake | 24 ++
tools/flags.cmake | 21 ++
tools/helpers.cmake | 488 +++++++++++++++++++++++++
tools/internal.cmake | 99 +++++
34 files changed, 2756 insertions(+)
create mode 100644 CMakeLists.txt
create mode 100644 config.cmake
create mode 100644 configs/arm_verified.cmake
create mode 100644 gcc.cmake
create mode 100644 include/32/mode/config.cmake
create mode 100644 include/64/mode/config.cmake
create mode 120000 include/arch/arm/armv/armv7ve
create mode 100644 libsel4/CMakeLists.txt
create mode 100644 src/arch/arm/32/config.cmake
create mode 100644 src/arch/arm/64/config.cmake
create mode 100644 src/arch/arm/armv/armv6/config.cmake
create mode 100644 src/arch/arm/armv/armv7-a/config.cmake
create mode 100644 src/arch/arm/armv/armv8-a/config.cmake
create mode 100644 src/arch/arm/config.cmake
create mode 100644 src/arch/x86/32/config.cmake
create mode 100644 src/arch/x86/64/config.cmake
create mode 100644 src/arch/x86/config.cmake
create mode 100644 src/config.cmake
create mode 100644 src/plat/am335x/config.cmake
create mode 100644 src/plat/apq8064/config.cmake
create mode 100644 src/plat/bcm2837/config.cmake
create mode 100644 src/plat/exynos4/config.cmake
create mode 100644 src/plat/exynos5/config.cmake
create mode 100644 src/plat/hikey/config.cmake
create mode 100644 src/plat/imx31/config.cmake
create mode 100644 src/plat/imx6/config.cmake
create mode 100644 src/plat/omap3/config.cmake
create mode 100644 src/plat/pc99/config.cmake
create mode 100644 src/plat/tk1/config.cmake
create mode 100644 src/plat/tx1/config.cmake
create mode 100644 src/plat/zynq7000/config.cmake
create mode 100644 tools/flags.cmake
create mode 100644 tools/helpers.cmake
create mode 100644 tools/internal.cmake
diff --git a/CMakeLists.txt b/CMakeLists.txt
new file mode 100644
index 000000000..0edc2306d
--- /dev/null
+++ b/CMakeLists.txt
@@ -0,0 +1,380 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+project(seL4 C ASM)
+
+# First find our helpers
+find_file(KERNEL_HELPERS_PATH helpers.cmake PATHS tools CMAKE_FIND_ROOT_PATH_BOTH)
+mark_as_advanced(FORCE KERNEL_HELPERS_PATH)
+include(${KERNEL_HELPERS_PATH})
+
+function(RequireTool config file)
+ RequireFile("${config}" "${file}" PATHS tools)
+endfunction(RequireTool)
+
+RequireTool(KERNEL_FLAGS_PATH flags.cmake)
+
+if(CCACHEFOUND)
+ set(ccache "ccache")
+endif()
+
+include(tools/internal.cmake)
+
+# Process the configuration scripts
+include(config.cmake)
+
+# Define tools used by the kernel
+set(PYTHON "python" CACHE INTERNAL "")
+RequireTool(CPP_GEN_PATH cpp_gen.sh)
+RequireTool(CIRCULAR_INCLUDES circular_includes.py)
+RequireTool(BF_GEN_PATH bitfield_gen.py)
+RequireTool(INVOCATION_ID_GEN_PATH invocation_header_gen.py)
+RequireTool(SYSCALL_ID_GEN_PATH syscall_header_gen.py)
+RequireTool(XMLLINT_PATH xmllint.sh)
+
+# Define default global flag information so that users can compile with the same basic architecture
+# flags as the kernel
+if(KernelArchX86)
+ if(${KernelX86MicroArch} STREQUAL generic)
+ set(build_arch "-mtune=generic")
+ else()
+ set(build_arch "-march=${KernelX86MicroArch}")
+ endif()
+ if(Kernel64)
+ set(asm_common_flags "${asm_common_flags} -Wa,--64")
+ set(c_common_flags "${c_common_flags} -m64")
+ else()
+ set(asm_common_flags "${asm_common_flags} -Wa,--32")
+ set(c_common_flags "${c_common_flags} -m32")
+ endif()
+endif()
+if(KernelArchARM)
+ set(c_common_flags "${c_common_flags} -mcpu=${KernelArmCPU} -march=${KernelArmArmV}${KernelArmMachFeatureModifiers}")
+ set(asm_common_flags "${asm_common_flags} -Wa,-mcpu=${KernelArmCPU} -Wa,-march=${KernelArmArmV}${KernelArmMachFeatureModifiers}")
+endif()
+set(common_flags "${common_flags} ${build_arch}")
+if(Kernel64)
+ set(common_flags "${common_flags} -D__KERNEL_64__")
+else()
+ set(common_flags "${common_flags} -D__KERNEL_32__")
+endif()
+
+set(BASE_ASM_FLAGS "${asm_common_flags} ${common_flags}" CACHE INTERNAL "Default ASM flags for compilation \
+ (subset of flags used by the kernel build)"
+)
+set(BASE_C_FLAGS "${c_common_flags} ${common_flags}" CACHE INTERNAL "Default C flags for compilation \
+ (subset of flags used by the kernel)"
+)
+set(BASE_CXX_FLAGS "${cxx_common_flags} ${c_common_flags} ${common_flags}" CACHE INTERNAL
+ "Default CXX flags for compilation"
+)
+if(KernelArchX86)
+ if(Kernel64)
+ set(common_exe_flags "${common_exe_flags} -Wl,-m -Wl,elf_x86_64")
+ else()
+ set(common_exe_flags "${common_exe_flags} -Wl,-m -Wl,elf_i386")
+ endif()
+endif()
+set(BASE_EXE_LINKER_FLAGS "${common_flags} ${common_exe_flags} " CACHE INTERNAL
+ "Default flags for linker an elf binary application"
+)
+# Initializing the kernel build flags starting from the same base flags that the users will use
+include(${KERNEL_FLAGS_PATH})
+
+# Setup kernel specific flags
+set(kernel_common_flags "${kernel_common_flags} -nostdinc -nostdlib ${KernelOptimisation} -DHAVE_AUTOCONF")
+if(KernelFWholeProgram)
+ set(kernel_common_flags "${kernel_common_flags} -fwhole-program")
+endif()
+if(KernelDebugBuild)
+ set(kernel_common_flags "${kernel_common_flags} -DDEBUG -g -ggdb")
+ # Pretend to CMake that we're a release build with debug info. This is because
+ # we do actually allow CMake to do the final link step, so we'd like it not to
+ # strip our binary
+ set(CMAKE_BUILD_TYPE "RelWithDebInfo")
+else()
+ set(CMAKE_BUILD_TYPE "Release")
+endif()
+if(KernelArchX86 AND Kernel64)
+ set(kernel_common_flags "${kernel_common_flags} -mcmodel=kernel")
+endif()
+if(kernelArchARM)
+ set(kernel_common_flags "${kernel_common_flags} -mfloat-abi=soft")
+endif()
+set(kernel_common_flags "${kernel_common_flags} -fno-pic -fno-pie")
+set(CMAKE_ASM_FLAGS "${CMAKE_ASM_FLAGS} ${kernel_common_flags}")
+set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${kernel_common_flags} \
+ -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 ${KernelOptimisation} \
+ -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations \
+ -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding"
+)
+
+set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${kernel_common_flags} \
+ -ffreestanding -Wl,--build-id=none -static")
+
+set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-n")
+
+if(KernelArchX86)
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -mno-mmx -mno-sse -mno-sse2 -mno-3dnow")
+endif()
+
+# Sort the C sources to ensure a stable layout of the final C file
+list(SORT c_sources)
+# Add the domain schedule now that its sorted
+list(APPEND c_sources "${KernelDomainSchedule}")
+
+# 'c_arguments_deps' is a variable that will hold dependencies for any generated header paths added
+# to 'CMAKE_C/ASM_FLAGS'. This means whenever a command uses 'CMAKE_C/ASM_FLAGS' it should also
+# depends upon 'c_arguments_deps'
+# We define some macros for keeping these in sync
+macro(add_flags)
+ set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${ARGN}")
+ set(CMAKE_ASM_FLAGS "${CMAKE_ASM_FLAGS} ${ARGN}")
+endmacro(add_flags)
+macro(AddHeader header)
+ add_flags("-I${header}")
+endmacro(AddHeader)
+
+# Add static header includes
+AddHeader("${CMAKE_CURRENT_SOURCE_DIR}/include")
+AddHeader("${CMAKE_CURRENT_SOURCE_DIR}/include/arch/${KernelArch}")
+AddHeader("${CMAKE_CURRENT_SOURCE_DIR}/include/arch/${KernelArch}/arch/${KernelWordSize}/")
+AddHeader("${CMAKE_CURRENT_SOURCE_DIR}/include/plat/${KernelPlatform}/")
+AddHeader("${CMAKE_CURRENT_SOURCE_DIR}/include/plat/${KernelPlatform}/plat/${KernelWordSize}/")
+if(KernelArchARM)
+ AddHeader("${CMAKE_CURRENT_SOURCE_DIR}/include/arch/arm/armv/${KernelArmArmV}/")
+ AddHeader("${CMAKE_CURRENT_SOURCE_DIR}/include/arch/arm/armv/${KernelArmArmV}/${KernelWordSize}")
+endif()
+
+###################
+# Config generation
+###################
+
+# The kernel expects to be able to include an 'autoconf.h' file at the moment. So lets
+# generate one for it to use
+# TODO: use the kernel_Config directly
+generate_autoconf(kernel_autoconf "kernel")
+# When doing custom compilations we need to add the config header directories to our
+# include path, since we cannot get them automatically through link libraries. For
+# this purpose we have an additional variable for arguments that may have generator
+# expressions
+set(custom_command_c_flags "${custom_command_c_flags} -I$<JOIN:$<TARGET_PROPERTY:kernel_autoconf,INTERFACE_INCLUDE_DIRECTORIES>, -I>")
+
+# We also need to manually depend upon the targets and generated files
+get_generated_files(gen_files kernel_autoconf_Gen)
+list(APPEND c_arguments_deps kernel_autoconf_Gen
+ ${gen_files}
+)
+
+#####################
+# C source generation
+#####################
+
+# Kernel compiles all C sources as a single C file, this provides
+# rules for doing the concatenation
+
+add_custom_command(OUTPUT kernel_all.c
+ COMMAND "${CPP_GEN_PATH}" ${c_sources} > kernel_all.c
+ DEPENDS "${CPP_GEN_PATH}" ${c_sources} ${c_arguments_deps}
+ COMMENT "Concatenating C files"
+ VERBATIM
+)
+
+add_custom_target(kernel_all_c_wrapper
+ DEPENDS kernel_all.c
+)
+
+###################
+# Header Generation
+###################
+
+# Rules for generating invocation and syscall headers
+# Aside from generating file rules for dependencies this section will also produce a target
+# that can be depended upon (along with the desired files themselves) to control parallelism
+
+set(header_dest "gen_headers/arch/api/invocation.h")
+gen_invocation_header(
+ OUTPUT ${header_dest}
+ XML ${CMAKE_CURRENT_SOURCE_DIR}/libsel4/arch_include/${KernelArch}/interfaces/sel4arch.xml
+ ARCH
+)
+list(APPEND gen_headers_deps "${header_dest}")
+
+set(header_dest "gen_headers/arch/api/sel4_invocation.h")
+gen_invocation_header(
+ OUTPUT "${header_dest}"
+ XML "${CMAKE_CURRENT_SOURCE_DIR}/libsel4/sel4_arch_include/${KernelSel4Arch}/interfaces/sel4arch.xml"
+ SEL4ARCH
+)
+list(APPEND gen_headers_deps "${header_dest}")
+
+set(header_dest "gen_headers/api/invocation.h")
+gen_invocation_header(
+ OUTPUT "${header_dest}"
+ XML "${CMAKE_CURRENT_SOURCE_DIR}/libsel4/include/interfaces/sel4.xml"
+)
+list(APPEND gen_headers_deps "${header_dest}")
+
+set(syscall_xml_base "${CMAKE_CURRENT_SOURCE_DIR}/include/api")
+set(syscall_dest "gen_headers/arch/api/syscall.h")
+add_custom_command(OUTPUT ${syscall_dest}
+ COMMAND "${XMLLINT_PATH}" --noout --schema "${syscall_xml_base}/syscall.xsd" "${syscall_xml_base}/syscall.xml"
+ COMMAND rm -f "${syscall_dest}"
+ COMMAND "${SYSCALL_ID_GEN_PATH}" --xml "${syscall_xml_base}/syscall.xml" --kernel_header "${syscall_dest}"
+ DEPENDS "${XMLLINT_PATH}" "${SYSCALL_ID_GEN_PATH}" "${syscall_xml_base}/syscall.xsd" "${syscall_xml_base}/syscall.xml"
+ COMMENT "Generate syscall invocations"
+ VERBATIM
+)
+list(APPEND gen_headers_deps "${syscall_dest}")
+# Create a target for all the headers generation commands to control parallel builds
+add_custom_target(gen_headers_wrapper
+ DEPENDS ${gen_headers_deps}
+)
+AddHeader("${CMAKE_CURRENT_BINARY_DIR}/gen_headers")
+list(APPEND c_arguments_deps ${gen_headers_deps} gen_headers_wrapper)
+
+#######################
+# Prune list generation
+#######################
+
+# When generating bitfield files we can pass multiple '--prune' parameters that are source
+# files that get searched for determing which bitfield functions are used. This allows the
+# bitfield generator to only generate functions that are used. Whilst irrelevant for
+# normal compilation, not generating unused functions has significant time savings for the
+# automated verification tools
+
+# To generate a prune file we 'build' the kernel (similar to the kernel_all_pp.c rule
+# below) but strictly WITHOUT the generated header directory where the bitfield generated
+# headers are. This means our preprocessed file will contain all the code used by the
+# normal compilation, just without the bitfield headers (which we generate dummy versions of).
+# If we allowed the bitfield headers to be included then we would have a circular
+# dependency. As a result this rule comes *before* the Bitfield header generation section
+
+set(dummy_headers "")
+foreach(bf_dec ${bf_declarations})
+ string(REPLACE ":" ";" bf_dec ${bf_dec})
+ list(GET bf_dec 0 bf_file)
+ list(GET bf_dec 1 bf_gen_dir)
+ get_filename_component(bf_name "${bf_file}" NAME)
+ string(REPLACE ".bf" "_gen.h" bf_target "${bf_name}")
+ list(APPEND dummy_headers "${CMAKE_CURRENT_BINARY_DIR}/generated_prune/${bf_gen_dir}/${bf_target}")
+endforeach()
+
+add_custom_command(OUTPUT ${dummy_headers}
+ COMMAND touch ${dummy_headers}
+ COMMENT "Generate dummy headers for prune compilation"
+)
+
+add_custom_target(dummy_header_wrapper
+ DEPENDS ${dummy_headers}
+)
+
+GenCPPCommand(
+ kernel_all_pp_prune.c
+ kernel_all.c
+ EXTRA_FLAGS "${custom_command_c_flags} -CC -I${CMAKE_CURRENT_BINARY_DIR}/generated_prune"
+ TARGET kernel_all_pp_prune_wrapper
+ EXTRA_DEPS "kernel_all_c_wrapper;${c_arguments_deps};dummy_header_wrapper;${dummy_headers}"
+)
+
+############################
+# Bitfield header generation
+############################
+
+set(bf_gen_target "kernel_bf_gen_target")
+
+foreach(bf_dec ${bf_declarations})
+ string(REPLACE ":" ";" bf_dec ${bf_dec})
+ list(GET bf_dec 0 bf_file)
+ list(GET bf_dec 1 bf_gen_dir)
+ get_filename_component(bf_name "${bf_file}" NAME)
+ string(REPLACE ".bf" "_gen.h" bf_target "${bf_name}")
+ string(REPLACE ".bf" "_defs.thy" defs_target "${bf_name}")
+ string(REPLACE ".bf" "_proofs.thy" proofs_target "${bf_name}")
+ set(pbf_name "generated/${bf_gen_dir}/${bf_name}.pbf")
+ set(pbf_target "${bf_gen_target}_pbf")
+ GenCPPCommand(
+ "${pbf_name}"
+ "${bf_file}"
+ EXTRA_FLAGS "${custom_command_c_flags} -P"
+ TARGET "${pbf_target}"
+ EXTRA_DEPS "${c_arguments_deps}"
+ )
+ GenHBFTarget("" ${bf_gen_target} "generated/${bf_gen_dir}/${bf_target}" "${pbf_name}" "${pbf_target}"
+ "kernel_all_pp_prune.c" "kernel_all_pp_prune_wrapper")
+ GenDefsBFTarget("${bf_gen_target}_def" "generated/${bf_gen_dir}/${defs_target}" "${pbf_name}" "${pbf_target}"
+ "kernel_all_pp_prune.c" "kernel_all_pp_prune_wrapper")
+ GenProofsBFTarget("${bf_gen_target}_proof" "generated/${bf_gen_dir}/${proofs_target}" "${pbf_name}" "${pbf_target}"
+ "kernel_all_pp_prune.c" "kernel_all_pp_prune_wrapper")
+ list(APPEND theories_deps
+ "${bf_gen_target}_def" "${CMAKE_CURRENT_BINARY_DIR}/generated/${bf_gen_dir}/${defs_target}"
+ "${bf_gen_target}_proof" "${CMAKE_CURRENT_BINARY_DIR}/generated/${bf_gen_dir}/${proofs_target}"
+ )
+ list(APPEND c_arguments_deps "${bf_gen_target}")
+ set(bf_gen_target "${bf_gen_target}1")
+endforeach()
+
+AddHeader("${CMAKE_CURRENT_BINARY_DIR}/generated")
+
+####################
+# Kernel compilation
+####################
+
+GenCPPCommand(
+ kernel_all_pp.c
+ kernel_all.c
+ EXTRA_FLAGS "${custom_command_c_flags} -CC"
+ TARGET kernel_all_pp_wrapper
+ EXTRA_DEPS "kernel_all_c_wrapper;${c_arguments_deps}"
+)
+
+set(linker_lds_path "${CMAKE_CURRENT_BINARY_DIR}/linker.lds_pp")
+set(linker_source "src/plat/${KernelPlatform}/linker.lds")
+GenCPPCommand(
+ "${linker_lds_path}"
+ "${linker_source}"
+ EXTRA_FLAGS "${custom_command_c_flags} -P"
+ TARGET linker_ld_wrapper
+ EXTRA_DEPS "${c_arguments_deps}"
+)
+set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -T ${linker_lds_path}")
+
+# Need a custom build command as we need to not have our already pre-processed file get
+# processed again, which means either using a .ii file or explicitly saying -x cpp-output.
+# Unfortunately and cmake doesn't understand .ii files directly so we do the latter approach
+add_custom_command(OUTPUT kernel_all.o
+ # Take the opportunity to check for circular includes
+ COMMAND ${CIRCULAR_INCLUDES} < kernel_all_pp.c
+ COMMAND echo "${custom_command_c_flags}" "${CMAKE_C_FLAGS}" -x cpp-output kernel_all_pp.c |
+ xargs ${ccache} ${CMAKE_C_COMPILER} -ffreestanding -c -o kernel_all.o
+ # Cannot make the kernel.elf executable properly depend upon the linker script so depend upon it
+ # here
+ DEPENDS kernel_all_pp.c kernel_all_pp_wrapper ${c_arguments_deps} linker_ld_wrapper "${linker_lds_path}"
+ VERBATIM
+ COMMENT "Compiling concatenated kernel sources"
+)
+
+add_custom_target(kernel_all_wrapper
+ DEPENDS kernel_all.o
+)
+
+add_custom_target(kernel_theories
+ DEPENDS ${theories_deps}
+)
+
+# Declare final kernel output
+add_executable(kernel.elf EXCLUDE_FROM_ALL ${asm_sources} kernel_all.o)
+target_include_directories(kernel.elf PRIVATE ${config_dir})
+target_include_directories(kernel.elf PRIVATE include)
+target_link_libraries(kernel.elf PRIVATE kernel_Config kernel_autoconf)
+add_dependencies(kernel.elf kernel_all_wrapper)
diff --git a/config.cmake b/config.cmake
new file mode 100644
index 000000000..ce15f61c1
--- /dev/null
+++ b/config.cmake
@@ -0,0 +1,245 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+set(configure_string "")
+
+# Set kernel branch
+config_set(KernelIsMaster KERNEL_MASTER ON)
+
+# Proof based configuration variables
+find_path(CSPEC_DIR KernelState_C.thy CMAKE_FIND_ROOT_PATH_BOTH)
+set(SKIP_MODIFIES ON CACHE INTERNAL "")
+set(TOPLEVELTYPES "cte_C;tcb_C;endpoint_C;notification_C;asid_pool_C;pte_C;pde_C;user_data_C;user_data_device_C" CACHE INTERNAL "")
+set(SORRY_BITFIELD_PROOFS OFF CACHE INTERNAL "")
+find_file(UMM_TYPES umm_types.txt CMAKE_FIND_ROOT_PATH_BOTH)
+set(force FORCE)
+if(KernelVerificationBuild)
+ set(force CLEAR)
+endif()
+mark_as_advanced(${force} CSPEC_DIR SKIP_MODIFIES TOPLEVELTYPES SORRY_BITFIELD_PROOFS UMM_TYPES)
+
+########################
+# Architecture selection
+########################
+config_choice(KernelArch ARCH "Architecture to use when building the kernel"
+ "arm;KernelArchARM;ARCH_ARM"
+ "x86;KernelArchX86;ARCH_X86"
+)
+
+# Set defaults for common variables
+set(KernelHaveFPU OFF)
+
+include(src/arch/arm/config.cmake)
+include(src/arch/x86/config.cmake)
+
+include(include/32/mode/config.cmake)
+include(include/64/mode/config.cmake)
+include(src/config.cmake)
+
+# Enshrine common variables in the config
+config_set(KernelHaveFPU HAVE_FPU "${KernelHaveFPU}")
+
+# System parameters
+config_string(KernelRootCNodeSizeBits ROOT_CNODE_SIZE_BITS
+ "Root CNode Size (2^n slots) \
+ 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."
+ DEFAULT 12
+ UNQUOTE
+)
+
+config_string(KernelTimerTickMS TIMER_TICK_MS
+ "Timer tick period in milliseconds"
+ DEFAULT 2
+ UNQUOTE
+)
+config_string(KernelTimeSlice TIME_SLICE
+ "Number of timer ticks until a thread is preempted."
+ DEFAULT 5
+ UNQUOTE
+)
+config_string(KernelRetypeFanOutLimit RETYPE_FAN_OUT_LIMIT
+ "Maximum number of objects that can be created in a single Retype() invocation."
+ DEFAULT 256
+ UNQUOTE
+)
+config_string(KernelMaxNumWorkUnitsPerPreemption MAX_NUM_WORK_UNITS_PER_PREEMPTION
+ "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)."
+ DEFAULT 100
+ UNQUOTE
+)
+config_string(KernelMaxNumBootinfoUntypedCaps MAX_NUM_BOOTINFO_UNTYPED_CAPS
+ "Max number of bootinfo untyped caps"
+ DEFAULT 230
+ UNQUOTE
+)
+config_option(KernelFastpath FASTPATH "Enable IPC fastpath" DEFAULT ON)
+
+config_string(KernelNumDomains NUM_DOMAINS "The number of scheduler domains in the system" DEFAULT 1 UNQUOTE)
+
+find_file(KernelDomainSchedule default_domain.c PATHS src/config CMAKE_FIND_ROOT_PATH_BOTH
+ DOC "A C file providing the symbols ksDomSchedule and ksDomeScheudleLength \
+ to be linked with the kernel as a scheduling configuration."
+)
+
+config_string(KernelNumPriorities NUM_PRIORITIES
+ "The number of priority levels per domain. Valid range 1-256"
+ DEFAULT 256
+ UNQUOTE
+)
+
+config_string(KernelMaxNumNodes MAX_NUM_NODES "Max number of CPU cores to boot"
+ DEFAULT 1
+ DEPENDS "${KernelNumDomains} EQUAL 1"
+ UNQUOTE
+)
+
+config_string(KernelStackBits KERNEL_STACK_BITS
+ "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"
+ DEFAULT 12
+ UNQUOTE
+)
+
+config_string(KernelFPUMaxRestoresSinceSwitch FPU_MAX_RESTORES_SINCE_SWITCH
+ "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."
+ DEFAULT 64
+ DEPENDS "KernelHaveFPU" UNDEF_DISABLED
+ UNQUOTE
+)
+
+config_option(KernelVerificationBuild VERIFICATION_BUILD
+ "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."
+ DEFAULT ON
+)
+
+config_option(KernelDebugBuild DEBUG_BUILD
+ "Enable debug facilities (symbols and assertions) in the kernel"
+ DEFAULT ON
+ DEPENDS "NOT KernelVerificationBuild" DEFAULT_DISABLED OFF
+)
+
+config_option(HardwareDebugAPI HARDWARE_DEBUG_API
+ "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."
+ DEFAULT OFF
+ DEPENDS "NOT KernelVerificationBuild"
+)
+config_option(KernelPrinting PRINTING
+ "Allow the kernel to print out messages to the serial console during bootup and execution."
+ DEFAULT "${KernelDebugBuild}"
+ DEPENDS "NOT KernelVerificationBuild" DEFAULT_DISABLED OFF
+)
+config_choice(KernelBenchmarks KERNEL_BENCHMARK "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. \
+ none -> No Benchmarking features enabled. \
+ generic -> Enable global benchmarks config variable with no specific features. \
+ track_kernel_entries -> Log kernel entries information including timing, number of invocations and arguments for \
+ system calls, interrupts, user faults and VM faults. \
+ tracepoints -> Enable manually inserted tracepoints that the kernel will track time consumed between. \
+ track_utilisation -> Enable the kernel to track each thread's utilisation time."
+ "none;KernelBenchmarksNone;NO_BENCHMARKS"
+ "generic;KernelBenchmarksGeneric;BENCHMARK_GENERIC;NOT KernelVerificationBuild"
+ "track_kernel_entries;KernelBenchmarksTrackKernelEntries;BENCHMARK_TRACK_KERNEL_ENTRIES;NOT KernelVerificationBuild"
+ "tracepoints;KernelBenchmarksTracepoints;BENCHMARK_TRACEPOINTS;NOT KernelVerificationBuild"
+ "track_utilisation;KernelBenchmarksTrackUtilisation;BENCHMARK_TRACK_UTILISATION;NOT KernelVerificationBuild"
+)
+if(NOT (KernelBenchmarks STREQUAL "none"))
+ config_set(KernelEnableBenchmarks ENABLE_BENCHMARKS ON)
+else()
+ config_set(KernelEnableBenchmarks ENABLE_BENCHMARKS OFF)
+endif()
+config_string(KernelMaxNumTracePoints MAX_NUM_TRACE_POINTS
+ "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."
+ DEFAULT 1
+ DEPENDS "NOT KernelVerificationBuild;KernelBenchmarksTracepoints" DEFAULT_DISABLED 0
+ UNQUOTE
+)
+# TODO: this config has no business being in the build system, and should
+# be moved to C headers, but for now must be emulated here for compatibility
+if(KernelBenchmarksTrackKernelEntries OR KernelBenchmarksTracepoints)
+ config_set(KernelBenchmarkUseKernelLogBuffer BENCHMARK_USE_KERNEL_LOG_BUFFER ON)
+else()
+ config_set(KernelBenchmarkUseKernelLogBuffer BENCHMARK_USE_KERNEL_LOG_BUFFER OFF)
+endif()
+
+config_option(KernelIRQReporting IRQ_REPORTING
+ "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."
+ DEFAULT ON
+ DEPENDS "KernelPrinting" DEFAULT_DISABLED OFF
+)
+config_option(KernelColourPrinting COLOUR_PRINTING
+ "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."
+ DEFAULT ON
+ DEPENDS "KernelPrinting" DEFAULT_DISABLED OFF
+)
+config_string(KernelUserStackTraceLength USER_STACK_TRACE_LENGTH
+ "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."
+ DEFAULT 16
+ DEPENDS "KernelPrinting" DEFAULT_DISABLED 0
+ UNQUOTE
+)
+
+config_choice(KernelOptimisation KERNEL_OPT_LEVEL "Select the kernel optimisation level"
+ "-O2;KerenlOptimisationO2;KERNEL_OPT_LEVEL_O2"
+ "-Os;KerenlOptimisationOS;KERNEL_OPT_LEVEL_OS"
+ "-O1;KerenlOptimisationO1;KERNEL_OPT_LEVEL_O1"
+ "-O3;KerenlOptimisationO3;KERNEL_OPT_LEVEL_O3"
+)
+
+config_option(KernelFWholeProgram KERNEL_FWHOLE_PROGRAM
+ "Enable -fwhole-program when linking kernel. This should work modulo gcc bugs, which \
+ are not uncommon with -fwhole-program. Consider this feature experimental!"
+ DEFAULT OFF
+)
+
+
+config_option(KernelDangerousCodeInjection DANGEROUS_CODE_INJECTION
+ "Adds a system call that allows users to specify code to be run in kernel mode. \
+ Useful for profiling."
+ DEFAULT OFF
+ DEPENDS "NOT KernelARMHypervisorSupport;NOT KernelVerificationBuild"
+)
+
+config_option(KernelDebugDisablePrefetchers DEBUG_DISABLE_PREFETCHERS
+ "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."
+ DEFAULT OFF
+ DEPENDS "KernelArchX86 OR KernelPlatformHikey"
+)
+
+add_config_library(kernel "${configure_string}")
diff --git a/configs/arm_verified.cmake b/configs/arm_verified.cmake
new file mode 100644
index 000000000..aab81277f
--- /dev/null
+++ b/configs/arm_verified.cmake
@@ -0,0 +1,26 @@
+#
+# 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)
+#
+
+set(KernelARMPlatform "sabre" CACHE STRING "")
+set(KernelArch "arm" CACHE STRING "")
+set(KernelArmSel4Arch "aarch32" CACHE STRING "")
+set(KernelVerificationBuild ON CACHE BOOL "")
+set(KernelIPCBufferLocation "threadID_register" CACHE STRING "")
+set(KernelMaxNumNodes "1" CACHE STRING "")
+set(KernelOptimisation "-O2" CACHE STRING "")
+set(KernelRetypeFanOutLimit "256" CACHE STRING "")
+set(KernelBenchmarks "none" CACHE STRING "")
+set(KernelDangerousCodeInjection OFF CACHE BOOL "")
+set(KernelFastpath ON CACHE BOOL "")
+set(KernelPrinting OFF CACHE BOOL "")
+set(KernelNumDomains 16 CACHE STRING "")
+set(KernelMaxNumBootinfoUntypedCap 166 CACHE STRING "")
diff --git a/gcc.cmake b/gcc.cmake
new file mode 100644
index 000000000..898f69377
--- /dev/null
+++ b/gcc.cmake
@@ -0,0 +1,34 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+set(CMAKE_SYSTEM_NAME Generic)
+# For a generic system this is unused, so define it to something that will be
+# obvious if someone accidentally uses it
+set(CMAKE_SYSTEM_PROCESSOR seL4CPU)
+
+set(CMAKE_SYSROOT "${CMAKE_BINARY_DIR}")
+set(CMAKE_STAGING_PREFIX "${CMAKE_BINARY_DIR}/staging")
+
+set(CMAKE_C_COMPILER ${CROSS_COMPILER_PREFIX}gcc)
+set(CMAKE_ASM_COMPILER ${CROSS_COMPILER_PREFIX}gcc)
+set(CMAKE_CXX_COMPILER ${CROSS_COMPILER_PREFIX}g++)
+
+set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM NEVER)
+set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY ONLY)
+set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY)
+set(CMAKE_FIND_ROOT_PATH_MODE_PACKAGE ONLY)
+
+set(CMAKE_TRY_COMPILE_TARGET_TYPE STATIC_LIBRARY)
+
+mark_as_advanced(FORCE CMAKE_TOOLCHAIN_FILE)
diff --git a/include/32/mode/config.cmake b/include/32/mode/config.cmake
new file mode 100644
index 000000000..d03502054
--- /dev/null
+++ b/include/32/mode/config.cmake
@@ -0,0 +1,15 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+add_bf_source_old("Kernel32" "shared_types.bf" "include/32" "mode/api")
diff --git a/include/64/mode/config.cmake b/include/64/mode/config.cmake
new file mode 100644
index 000000000..eb0c95ef7
--- /dev/null
+++ b/include/64/mode/config.cmake
@@ -0,0 +1,15 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+add_bf_source_old("Kernel64" "shared_types.bf" "include/64" "mode/api")
diff --git a/include/arch/arm/armv/armv7ve b/include/arch/arm/armv/armv7ve
new file mode 120000
index 000000000..ef0887a29
--- /dev/null
+++ b/include/arch/arm/armv/armv7ve
@@ -0,0 +1 @@
+armv7-a
\ No newline at end of file
diff --git a/libsel4/CMakeLists.txt b/libsel4/CMakeLists.txt
new file mode 100644
index 000000000..44e6731b4
--- /dev/null
+++ b/libsel4/CMakeLists.txt
@@ -0,0 +1,152 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+project(libsel4 C)
+
+set(configure_string "")
+
+config_choice(LibSel4FunctionAttributes LIB_SEL4_FUNCTION_ATTRIBUTE "Function attributes \
+ default->Verification friendly default configuration. syscalls will be inlined, \
+ but generated functions will not. \
+ inline->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. \
+ public->When set to true will make all user facing functions available as \
+ public symbols, which can be convenient for some language bindings."
+ "inline;LibSel4FunctionAttributeInline;LIB_SEL4_INLINE_INVOCATIONS"
+ "default;LibSel4FunctionAttributeDefault;LIB_SEL4_DEFAULT_FUNCTION_ATTRIBUTES"
+ "public;LibSel4FunctionAttributePublic;LIB_SEL4_PUBLIC_SYMBOLS"
+)
+
+config_option(LibSel4StubsUseIPCBufferOnly LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY
+ "use only IPC buffer for syscalls. 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."
+ DEFAULT OFF
+)
+
+if(LibSel4StubsUseIPCBufferOnly)
+ set(buffer "--buffer")
+endif()
+
+RequireFile(SYSCALL_STUB_GEN_PATH syscall_stub_gen.py PATHS tools)
+
+add_config_library(sel4 "${configure_string}")
+
+# Currently we use autoconf.h, so generate one of those
+generate_autoconf(sel4_autoconf "kernel;sel4")
+
+gen_invocation_header(
+ OUTPUT include/sel4/invocation.h
+ XML include/interfaces/sel4.xml
+ LIBSEL4
+)
+
+gen_invocation_header(
+ OUTPUT sel4_arch_include/${KernelSel4Arch}/sel4/sel4_arch/invocation.h
+ XML "${CMAKE_CURRENT_SOURCE_DIR}/sel4_arch_include/${KernelSel4Arch}/interfaces/sel4arch.xml"
+ LIBSEL4 SEL4ARCH
+)
+
+gen_invocation_header(
+ OUTPUT arch_include/${KernelArch}/sel4/arch/invocation.h
+ XML "${CMAKE_CURRENT_SOURCE_DIR}/arch_include/${KernelArch}/interfaces/sel4arch.xml"
+ LIBSEL4 ARCH
+)
+
+set(source_header_dirs
+ "${CMAKE_CURRENT_SOURCE_DIR}/include"
+ "${CMAKE_CURRENT_SOURCE_DIR}/arch_include/${KernelArch}"
+ "${CMAKE_CURRENT_SOURCE_DIR}/sel4_arch_include/${KernelSel4Arch}"
+ "${CMAKE_CURRENT_SOURCE_DIR}/sel4_plat_include/${KernelPlatform}"
+)
+
+# Add the include directory of autoconf.h to the cflags for the bitfield generation
+set(extra_cflags "${extra_cflags} -I$<JOIN:$<TARGET_PROPERTY:sel4_autoconf,INTERFACE_INCLUDE_DIRECTORIES>;${source_header_dirs}, -I>")
+
+function(genbf target_prefix pbf_location bf_location header_output)
+ get_generated_files(gen_list sel4_autoconf_Gen)
+ GenCPPCommand(
+ "${pbf_location}" "${bf_location}"
+ EXTRA_FLAGS "${extra_cflags} -P"
+ TARGET ${target_prefix}_pbf
+ EXTRA_DEPS "sel4_autoconf_Gen;${gen_list}"
+ )
+ GenHBFTarget("libsel4" ${target_prefix}_h "${header_output}" "${pbf_location}" ${target_prefix}_pbf "" "")
+endfunction(genbf)
+
+genbf("libsel4_types_gen"
+ "${CMAKE_CURRENT_BINARY_DIR}/generated/types_gen/types.pbf"
+ "${CMAKE_CURRENT_SOURCE_DIR}/include/sel4/types_${KernelWordSize}.bf"
+ "${CMAKE_CURRENT_BINARY_DIR}/include/sel4/types_gen.h"
+)
+
+genbf("libsel4_shared_types_gen"
+ "${CMAKE_CURRENT_BINARY_DIR}/generated/shared_types_gen/shared_types.pbf"
+ "${CMAKE_CURRENT_SOURCE_DIR}/include/sel4/shared_types_${KernelWordSize}.bf"
+ "${CMAKE_CURRENT_BINARY_DIR}/include/sel4/shared_types_gen.h"
+)
+
+genbf("libsel4_sel4_arch_types_gen"
+ "${CMAKE_CURRENT_BINARY_DIR}/generated/sel4_arch_shared_types/types.pbf"
+ "${CMAKE_CURRENT_SOURCE_DIR}/sel4_arch_include/${KernelSel4Arch}/sel4/sel4_arch/types.bf"
+ "${CMAKE_CURRENT_BINARY_DIR}/sel4_arch_include/${KernelSel4Arch}/sel4/sel4_arch/types_gen.h"
+)
+
+add_custom_command(OUTPUT include/sel4/syscall.h
+ COMMAND rm -f include/sel4/syscall.h
+ COMMAND "${XMLLINT_PATH}" --noout --schema "${CMAKE_CURRENT_SOURCE_DIR}/include/api/syscall.xsd"
+ "${CMAKE_CURRENT_SOURCE_DIR}/include/api/syscall.xml"
+ COMMAND ${PYTHON} "${SYSCALL_ID_GEN_PATH}" --xml "${CMAKE_CURRENT_SOURCE_DIR}/include/api/syscall.xml"
+ --libsel4_header include/sel4/syscall.h
+ DEPENDS "${SYSCALL_ID_GEN_PATH}" "${CMAKE_CURRENT_SOURCE_DIR}/include/api/syscall.xsd" "${CMAKE_CURRENT_SOURCE_DIR}/include/api/syscall.xml"
+ COMMENT "Generate syscall.h"
+ VERBATIM
+)
+
+set(interface_xmls
+ "${CMAKE_CURRENT_SOURCE_DIR}/sel4_arch_include/${KernelSel4Arch}/interfaces/sel4arch.xml"
+ "${CMAKE_CURRENT_SOURCE_DIR}/arch_include/${KernelArch}/interfaces/sel4arch.xml"
+ "${CMAKE_CURRENT_SOURCE_DIR}/include/interfaces/sel4.xml"
+)
+add_custom_command(OUTPUT include/interfaces/sel4_client.h
+ COMMAND rm -f include/interfaces/sel4_client.h
+ COMMAND echo "CONFIG_WORD_SIZE=${KernelWordSize}" > config
+ COMMAND "${PYTHON}" "${SYSCALL_STUB_GEN_PATH}" ${buffer} -a "${KernelSel4Arch}" -c config
+ -o include/interfaces/sel4_client.h
+ ${interface_xmls}
+ DEPENDS "${SYSCALL_STUB_GEN_PATH}" ${interface_xmls}
+ BYPRODUCTS config
+ COMMENT "Generate sel4_client.h"
+ VERBATIM
+)
+
+add_custom_target(sel4_gen
+ DEPENDS
+ include/interfaces/sel4_client.h include/sel4/types_gen.h include/sel4/syscall.h
+ include/sel4/invocation.h arch_include/${KernelArch}/sel4/arch/invocation.h
+ include/sel4/shared_types_gen.h sel4_arch_include/${KernelSel4Arch}/sel4/sel4_arch/invocation.h
+ sel4_arch_include/${KernelSel4Arch}/sel4/sel4_arch/types_gen.h
+)
+
+add_library(sel4 src/sel4_bootinfo.c)
+target_link_libraries(sel4 PRIVATE kernel_Config sel4_Config sel4_autoconf)
+target_include_directories(sel4 PUBLIC
+ ${source_header_dirs}
+ "${CMAKE_CURRENT_BINARY_DIR}/include"
+ "${CMAKE_CURRENT_BINARY_DIR}/arch_include/${KernelArch}"
+ "${CMAKE_CURRENT_BINARY_DIR}/sel4_arch_include/${KernelSel4Arch}"
+)
+add_dependencies(sel4 sel4_gen)
diff --git a/src/arch/arm/32/config.cmake b/src/arch/arm/32/config.cmake
new file mode 100644
index 000000000..81dce72f7
--- /dev/null
+++ b/src/arch/arm/32/config.cmake
@@ -0,0 +1,37 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+add_sources(
+ DEP "KernelSel4ArchAarch32"
+ PREFIX src/arch/arm/32
+ CFILES
+ object/objecttype.c
+ machine/hardware.c
+ machine/registerset.c
+ machine/fpu.c
+ model/statedata.c
+ c_traps.c
+ idle.c
+ kernel/thread.c
+ kernel/vspace.c
+ ASMFILES
+ head.S
+ traps.S
+ hyp_traps.S
+)
+
+add_sources(
+ DEP "KernelSel4ArchAarch32;KernelDebugBuild"
+ CFILES src/arch/arm/32/machine/capdl.c
+)
diff --git a/src/arch/arm/64/config.cmake b/src/arch/arm/64/config.cmake
new file mode 100644
index 000000000..d85262ff8
--- /dev/null
+++ b/src/arch/arm/64/config.cmake
@@ -0,0 +1,32 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+add_sources(
+ DEP "KernelSel4ArchAarch64"
+ PREFIX src/arch/arm/64
+ CFILES
+ object/objecttype.c
+ machine/capdl.c
+ machine/hardware.c
+ machine/registerset.c
+ machine/fpu.c
+ model/statedata.c
+ c_traps.c
+ idle.c
+ kernel/thread.c
+ kernel/vspace.c
+ ASMFILES
+ head.S
+ traps.S
+)
diff --git a/src/arch/arm/armv/armv6/config.cmake b/src/arch/arm/armv/armv6/config.cmake
new file mode 100644
index 000000000..5d42ba496
--- /dev/null
+++ b/src/arch/arm/armv/armv6/config.cmake
@@ -0,0 +1,24 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+add_sources(
+ DEP "KernelArchArmV6"
+ PREFIX src/arch/arm/armv/armv6
+ CFILES
+ benchmark.c
+ cache.c
+ user_access.c
+ ASMFILES
+ machine_asm.S
+)
diff --git a/src/arch/arm/armv/armv7-a/config.cmake b/src/arch/arm/armv/armv7-a/config.cmake
new file mode 100644
index 000000000..b4e245678
--- /dev/null
+++ b/src/arch/arm/armv/armv7-a/config.cmake
@@ -0,0 +1,24 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+add_sources(
+ DEP "KernelArchArmV7a"
+ PREFIX src/arch/arm/armv/armv7-a
+ CFILES
+ benchmark.c
+ cache.c
+ user_access.c
+ ASMFILES
+ machine_asm.S
+)
diff --git a/src/arch/arm/armv/armv8-a/config.cmake b/src/arch/arm/armv/armv8-a/config.cmake
new file mode 100644
index 000000000..47594866a
--- /dev/null
+++ b/src/arch/arm/armv/armv8-a/config.cmake
@@ -0,0 +1,24 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+add_sources(
+ DEP "KernelArchArmV8a"
+ PREFIX src/arch/arm/armv/armv8-a/${KernelWordSize}
+ CFILES
+ benchmark.c
+ cache.c
+ user_access.c
+ ASMFILES
+ machine_asm.S
+)
diff --git a/src/arch/arm/config.cmake b/src/arch/arm/config.cmake
new file mode 100644
index 000000000..67bc3c309
--- /dev/null
+++ b/src/arch/arm/config.cmake
@@ -0,0 +1,334 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+config_choice(KernelArmSel4Arch ARM_SEL4_ARCH "Architecture mode for building the kernel"
+ "aarch32;KernelSel4ArchAarch32;ARCH_AARCH32;KernelArchARM"
+ "aarch64;KernelSel4ArchAarch64;ARCH_AARCH64;KernelArchARM"
+ "arm_hyp;KernelSel4ArchArmHyp;ARCH_ARM_HYP;KernelArchARM;KernelArmHypervisorSupport"
+)
+
+config_choice(KernelARMPlatform ARM_PLAT "Select the platform for the architecture"
+ "sabre;KernelPlatformSabre;PLAT_SABRE;KernelSel4ArchAarch32"
+ "kzm;KernelPlatformKZM;PLAT_KZM;KernelSel4ArchAarch32"
+ "omap3;KernelPlatformOMAP3;PLAT_OMAP3;KernelSel4ArchAarch32"
+ "am335x;KernelPlatformAM335X;PLAT_AM335X;KernelSel4ArchAarch32"
+ "exynos4;KernelPlatformExynos4;PLAT_EXYNOS4;KernelSel4ArchAarch32"
+ "exynos5410;KernelPlatformExynos5410;PLAT_EXYNOS5410;KernelSel4ArchAarch32 OR KernelSel4ArchArmHyp"
+ "exynos5422;KernelPlatformExynos5422;PLAT_EXYNOS5422;KernelSel4ArchAarch32"
+ "exynos5250;KernelPlatformExynos5250;PLAT_EXYNOS5250;KernelSel4ArchAarch32"
+ "apq8064;KernelPlatformAPQ8064;PLAT_APQ8064;KernelSel4ArchAarch32"
+ "wandq;KernelPlatformWandQ;PLAT_WANDQ;KernelSel4ArchAarch32"
+ "imx7sabre;KernelPlatformImx7Sabre;PLAT_IMX6_SABRE;KernelSel4ArchAarch32"
+ "zynq7000;KernelPlatformZynq7000;PLAT_ZYNQ7000;KernelSel4ArchAarch32"
+ "allwinnera20;KernelPlatformAllwinnerA20;PLAT_ALLWINNERA20;KernelSel4ArchAarch32"
+ "jetson;KernelPlatformJetson;PLAT_TK1;KernelSel4ArchAarch32 OR KernelSel4ArchArmHyp"
+ "hikey;KernelPlatformHikey;PLAT_HIKEY;KernelArchARM"
+ "rpi3;KernelPlatformRpi3;PLAT_BCM2837;KernelSel4ArchAarch32"
+ "tx1;KernelPlatformTx1;PLAT_TX1;KernelSel4ArchAarch64"
+)
+
+if(KernelArchARM)
+ config_set(KernelSel4Arch SEL4_ARCH "${KernelArmSel4Arch}")
+endif()
+
+# arm-hyp masquerades as an aarch32 build
+if(KernelSel4ArchArmHyp)
+ config_set(KernelSel4ArmHypAarch32 ARCH_AARCH32 ON)
+ set(KernelSel4ArchAarch32 ON CACHE INTERNAL "")
+else()
+ config_set(KernelSel4ArmHypAarch32 ARCH_AARCH32 OFF)
+endif()
+
+if(KernelSel4ArchAarch32 OR KernelSel4ArchArmHyp)
+ set_kernel_32()
+elseif(KernelSel4ArchAarch64)
+ set_kernel_64()
+endif()
+
+# Include all the platforms. For all of the common variables we set a default value here
+# and let the platforms override them.
+set(KernelArmMachFeatureModifiers "" CACHE INTERNAL "")
+set(KernelArmMach "" CACHE INTERNAL "")
+set(KernelArmCortexA8 OFF)
+set(KernelArmCortexA9 OFF)
+set(KernelArmCortexA15 OFF)
+set(KernelArmCortexA53 OFF)
+set(KernelArmCortexA57 OFF)
+set(KernelArchArmV6 OFF)
+set(KernelArchArmV7a OFF)
+set(KernelArchArmV7ve OFF)
+set(KernelArchArmV8a OFF)
+set(KernelArm1136JF_S OFF)
+include(src/plat/imx6/config.cmake)
+include(src/plat/imx31/config.cmake)
+include(src/plat/omap3/config.cmake)
+include(src/plat/exynos4/config.cmake)
+include(src/plat/exynos5/config.cmake)
+include(src/plat/am335x/config.cmake)
+include(src/plat/hikey/config.cmake)
+include(src/plat/apq8064/config.cmake)
+include(src/plat/bcm2837/config.cmake)
+include(src/plat/tk1/config.cmake)
+include(src/plat/tx1/config.cmake)
+include(src/plat/zynq7000/config.cmake)
+
+# Now enshrine all the common variables in the config
+config_set(KernelArmCortexA8 ARM_CORTEX_A8 "${KernelArmCortexA8}")
+config_set(KernelArmCortexA9 ARM_CORTEX_A9 "${KernelArmCortexA9}")
+config_set(KernelArmCortexA15 ARM_CORTEX_A15 "${KernelArmCortexA15}")
+config_set(KernelArmCortexA53 ARM_CORTEX_A53 "${KernelArmCortexA53}")
+config_set(KernelArmCortexA57 ARM_CORTEX_A57 "${KernelArmCortexA57}")
+config_set(KernelArm1136JF_S ARM1136JF_S "${KernelArm1136JF_S}")
+config_set(KernelArchArmV6 ARCH_ARM_V6 "${KernelArchArmV6}")
+config_set(KernelArchArmV7a ARCH_ARM_V7A "${KernelArchArmV7a}")
+config_set(KernelArchArmV7ve ARCH_ARM_V7VE "${KernelArchArmV7ve}")
+config_set(KernelArchArmV78a ARCH_ARM_V8A "${KernelArchArmV8a}")
+
+set(KernelArmCPU "" CACHE INTERNAL "")
+set(KernelArmArmV "" CACHE INTERNAL "")
+
+# Check for v7ve before v7a as v7ve is a superset and we want to set the
+# actual armv to that, but leave armv7a config enabled for anything that
+# checks directly against it
+if(KernelArchArmV7ve)
+ set(KernelArmArmV "armv7ve" CACHE INTERNAL "")
+elseif(KernelArchArmV7a)
+ set(KernelArmArmV "armv7-a" CACHE INTERNAL "")
+elseif(KernelArchArmV8a)
+ set(KernelArmArmV "armv8-a" CACHE INTERNAL "")
+elseif(KernelArchArmV6)
+ set(KernelArmArmV "armv6" CACHE INTERNAL "")
+endif()
+if(KernelArmCortexA8)
+ set(KernelArmCPU "cortex-a8" CACHE INTERNAL "")
+elseif(KernelArmCortexA9)
+ set(KernelArmCPU "cortex-a9" CACHE INTERNAL "")
+elseif(KernelArmCortexA15)
+ set(KernelArmCPU "cortex-a15" CACHE INTERNAL "")
+elseif(KernelArmCortexA53)
+ set(KernelArmCPU "cortex-a53" CACHE INTERNAL "")
+elseif(KernelArmCortexA57)
+ set(KernelArmCPU "cortex-a57" CACHE INTERNAL "")
+elseif(KernelArm1136JF_S)
+ set(KernelArmCPU "arm1136jf-s" CACHE INTERNAL "")
+endif()
+if(KernelArchARM)
+ config_set(KernelArmMach ARM_MACH "${KernelArmMach}")
+endif()
+
+include(src/arch/arm/armv/armv6/config.cmake)
+include(src/arch/arm/armv/armv7-a/config.cmake)
+include(src/arch/arm/armv/armv8-a/config.cmake)
+
+config_choice(KernelIPCBufferLocation KERNEL_IPC_BUFFER_LOCATION
+ "Controls how the location of the IPC buffer is provided to the user \
+ globals_frame-> Put the address of the IPC buffer in a dedicated frame that is \
+ read only at user level. This works on all ARM platforms \
+ threadID_register-> 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."
+ "threadID_register;KernelIPCBufferThreadID;IPC_BUF_TPIDRURW;KernelArchARM;NOT KernelArchArmV6"
+ "globals_frame;KernelIPCBufferGlobalsFrame;IPC_BUF_GLOBALS_FRAME;KernelSel4ArchAarch32"
+)
+
+config_option(KernelDangerousCodeInjectionOnUndefInstr DANGEROUS_CODE_INJECTION_ON_UNDEF_INSTR
+ "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."
+ DEFAULT OFF
+ DEPENDS "KernelArchARMV6;NOT KernelVerificationBuild"
+)
+
+config_option(KernelDebugDisableL2Cache DEBUG_DISABLE_L2_CACHE
+ "Do not enable the L2 cache on startup for debugging purposes."
+ DEFAULT OFF
+ DEPENDS "KernelArchARM"
+)
+config_option(KernelDebugDisableL1ICache DEBUG_DISABLE_L1_ICACHE
+ "Do not enable the L1 instruction cache on startup for debugging purposes."
+ DEFAULT OFF
+ DEPENDS "KernelArchARM;KernelDebugDisableL2Cache"
+)
+config_option(KernelDebugDisableL1DCache DEBUG_DISABLE_L1_DCACHE
+ "Do not enable the L1 data cache on startup for debugging purposes."
+ DEFAULT OFF
+ DEPENDS "KernelArchARM;KernelDebugDisableL2Cache"
+)
+config_option(KernelDebugDisableBranchPrediction DEBUG_DISABLE_BRANCH_PREDICTION
+ "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."
+ DEFAULT OFF
+ DEPENDS "KernelArchARM"
+)
+
+config_option(KernelArmHypervisorSupport ARM_HYPERVISOR_SUPPORT
+ "Build as Hypervisor. Utilise ARM virtualisation extensions to build the kernel as a hypervisor"
+ DEFAULT OFF
+ DEPENDS "KernelArmCortexA15"
+)
+
+config_option(KernelArmHypEnableVCPUCP14SaveAndRestore ARM_HYP_ENABLE_VCPU_CP14_SAVE_AND_RESTORE
+ "Trap, but don't save/restore VCPUs' CP14 accesses \
+ 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"
+ DEFAULT ON
+ DEPENDS "KernelArmHypervisorSupport;NOT KernelVerificationBuild" DEFAULT_DISABLED OFF
+)
+
+config_option(KernelArmErrata430973 ARM_ERRATA_430973
+ "Enable workaround for 430973 Cortex-A8 (r1p0..r1p2) erratum \
+ 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."
+ DEFAULT OFF
+ DEPENDS "KernelArchARM;KernelArmCortexA8"
+)
+
+config_option(KernelArmErrata773022 ARM_ERRATA_773022
+ "Enable workaround for 773022 Cortex-A15 (r0p0..r0p4) erratum \
+ 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"
+ DEFAULT ON
+ DEPENDS "KernelArchARM;KernelArmCortexA15" DEFAULT_DISABLED OFF
+)
+
+config_option(KernelArmSMMU ARM_SMMU
+ "Enable SystemMMU for the Tegra TK1 SoC"
+ DEFAULT OFF
+ DEPENDS "KernelPlatformJetson"
+)
+
+config_option(KernelArmEnableA9Prefetcher ENABLE_A9_PREFETCHER
+ "Enable Cortex-A9 prefetcher \
+ 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."
+ DEFAULT OFF
+ DEPENDS "KernelArmCortexA9"
+)
+
+config_option(KernelArmExportPMUUser EXPORT_PMU_USER
+ "PL0 access to PMU. \
+ Grant user access to Performance Monitoring Unit. \
+ WARNING: While useful for evaluating performance, \
+ this option opens timing and covert channels."
+ DEFAULT OFF
+ DEPENDS "KernelArchArmV7a OR KernelArchArmV8a"
+)
+
+config_option(KernelArmExportPCNTUser EXPORT_PCNT_USER
+ "PL0 access to generic timer CNTPCT and CNTFRQ. \
+ Grant user access to physical counter and counter \
+ frequency registers of the generic timer. \
+ WARNING: selecting this option opens a timing \
+ channel"
+ DEFAULT OFF
+ DEPENDS "KernelArmCortexA15"
+)
+
+config_option(KernelArmExportVCNTUser EXPORT_VCNT_USER
+ "PL0 access to generic timer CNTVCT and CNTFRQ. \
+ Grant user access to virtual counter and counter \
+ frequency registers of the generic timer. \
+ WARNING: selecting this option opens a timing \
+ channel"
+ DEFAULT OFF
+ DEPENDS "KernelArmCortexA15"
+)
+
+config_option(KernelARMSMMUInterruptEnable SMMU_INTERRUPT_ENABLE
+ "Enable SMMU interrupts. \
+ 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"
+ DEFAULT "${KernelDebugBuild}"
+ DEPENDS "KernelArmSMMU" DEFAULT_DISABLED OFF
+)
+
+config_option(KernelAArch32FPUEnableContextSwitch AARCH32_FPU_ENABLE_CONTEXT_SWITCH
+ "Enable hardware VFP and SIMD context switch \
+ 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)."
+ DEFAULT ON
+ DEPENDS "KernelSel4ArchAarch32;NOT KernelArchArmV6;NOT KernelVerificationBuild"
+ DEFAULT_DISABLED OFF
+)
+
+if(KernelAArch32FPUEnableContextSwitch)
+ set(HaveFPU ON)
+endif()
+
+# TODO: this config has no business being in the build system, and should
+# be moved to C headers, but for now must be emulated here for compatibility
+if(KernelBenchmarksTrackUtilisation AND KernelArchARM)
+ config_set(KernelArmEnablePMUOverflowInterrupt ARM_ENABLE_PMU_OVERFLOW_INTERRUPT ON)
+else()
+ config_set(KernelArmEnablePMUOverflowInterrupt ARM_ENABLE_PMU_OVERFLOW_INTERRUPT OFF)
+endif()
+
+
+add_sources(
+ DEP "KernelArchARM"
+ PREFIX src/arch/arm
+ CFILES
+ c_traps.c
+ api/faults.c
+ benchmark/benchmark.c
+ kernel/boot.c
+ machine/cache.c
+ machine/errata.c
+ machine/io.c
+ machine/debug.c
+ object/interrupt.c
+ object/tcb.c
+ object/iospace.c
+ object/vcpu.c
+ smp/ipi.c
+)
+
+add_sources(
+ DEP "KernelArmCortexA9"
+ CFILES src/arch/arm/machine/l2c_310.c
+)
+
+add_sources(
+ DEP "KernelArmCortexA9;NOT KernelPlatformExynos4"
+ CFILES src/arch/arm/machine/priv_timer.c
+)
+
+add_sources(
+ DEP "KernelArmCortexA15 OR KernelArmCortexA7 OR KernelArmCortexA57 OR KernelArmCortexA9 OR KernelPlatformHikey"
+ CFILES src/arch/arm/machine/gic_pl390.c
+)
+
+add_bf_source_old("KernelArchARM" "structures.bf" "include/arch/arm" "arch/object")
+add_bf_source_old("KernelArchARM" "hardware.bf" "include/plat/${KernelPlatform}" "plat/machine")
+
+include(src/arch/arm/32/config.cmake)
+include(src/arch/arm/64/config.cmake)
diff --git a/src/arch/x86/32/config.cmake b/src/arch/x86/32/config.cmake
new file mode 100644
index 000000000..cdcad8a31
--- /dev/null
+++ b/src/arch/x86/32/config.cmake
@@ -0,0 +1,32 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+add_sources(
+ DEP "KernelSel4ArchIA32"
+ PREFIX src/arch/x86/32
+ CFILES
+ c_traps.c
+ object/objecttype.c
+ kernel/thread.c
+ kernel/vspace.c
+ kernel/vspace_32paging.c
+ kernel/elf.c
+ model/statedata.c
+ machine/registerset.c
+ smp/ipi.c
+ ASMFILES
+ machine_asm.S
+ traps.S
+ head.S
+)
diff --git a/src/arch/x86/64/config.cmake b/src/arch/x86/64/config.cmake
new file mode 100644
index 000000000..a455feafe
--- /dev/null
+++ b/src/arch/x86/64/config.cmake
@@ -0,0 +1,32 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+add_sources(
+ DEP "KernelSel4ArchX86_64"
+ PREFIX src/arch/x86/64
+ CFILES
+ c_traps.c
+ object/objecttype.c
+ kernel/thread.c
+ kernel/vspace.c
+ kernel/elf.c
+ model/statedata.c
+ model/smp.c
+ machine/registerset.c
+ smp/ipi.c
+ ASMFILES
+ machine_asm.S
+ traps.S
+ head.S
+)
diff --git a/src/arch/x86/config.cmake b/src/arch/x86/config.cmake
new file mode 100644
index 000000000..4534de441
--- /dev/null
+++ b/src/arch/x86/config.cmake
@@ -0,0 +1,262 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+config_choice(KernelX86Sel4Arch X86_SEL4_ARCH "Architecture mode for building the kernel"
+ "x86_64;KernelSel4ArchX86_64;ARCH_X86_64;KernelArchX86"
+ "ia32;KernelSel4ArchIA32;ARCH_IA32;KernelArchX86"
+)
+
+if(KernelArchX86)
+ # Only one platform so just force it to be set
+ config_set(KernelPlatform PLAT "pc99")
+ config_set(KernelPlatPC99 PLAT_PC99 ON)
+ config_set(KernelSel4Arch SEL4_ARCH "${KernelX86Sel4Arch}")
+ # x86 always has an FPU
+ set(KernelHaveFPU ON)
+else()
+ config_set(KernelPlatPC99 PLAT_PC99 OFF)
+endif()
+
+if(KernelSel4ArchX86_64)
+ set_kernel_64()
+elseif(KernelSel4ArchIA32)
+ set_kernel_32()
+endif()
+
+config_choice(KernelX86MicroArch KERNEL_X86_MICRO_ARCH "Select the x86 micro architecture"
+ "nehalem;KernelX86MicroArchNehalem;ARCH_X86_NEHALEM;KernelArchX86"
+ "generic;KernelX86MicroArchGeneric;ARCH_X86_GENERIC;KernelArchX86"
+ "westmere;KernelX86MicroArchWestmere;ARCH_X86_WESTMERE;KernelArchX86"
+ "sandy;KernelX86MicroArchSandy;ARCH_X86_SANDY;KernelArchX86"
+ "ivy;KernelX86MicroArchIvy;ARCH_X86_IVY;KernelArchX86"
+ "haswell;KernelX86MicroArchHaswell;ARCH_X86_HASWELL;KernelArchX86"
+ "broadwell;KernelX86MicroArchBroadwell;ARCH_X86_BROADWELL;KernelArchX86"
+ "skylake;KernelX86MicroArchSkylake;ARCH_X86_SKYLAKE;KernelArchX86"
+)
+
+config_choice(KernelIRQController KERNEL_IRQ_CONTROLLER
+ "Select the IRQ controller seL4 will use. Code for others may still be included if \
+ needed to disable at run time. \
+ PIC -> Use the legacy PIC controller. \
+ IOAPIC -> Use one or more IOAPIC controllers"
+ "IOAPIC;KernelIRQControllerIOAPIC;IRQ_IOAPIC;KernelArchX86"
+ "PIC;KernelIRQControllerPIC;IRQ_PIC;KernelArchX86"
+)
+
+config_string(KernelMaxNumIOAPIC MAX_NUM_IOAPIC
+ "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."
+ DEFAULT 1
+ DEPENDS "KernelIRQControllerIOAPIC" DEFAULT_DISABLED 0
+ UNQUOTE
+)
+
+config_choice(KernelLAPICMode KERNEL_LAPIC_MODE
+ "Select the mode local APIC will use. Not all machines support X2APIC mode."
+ "XAPIC;KernelLAPICModeXPAIC;XAPIC;KernelArchX86"
+ "X2APIC;KernelLAPICModeX2APIC;X2APIC;KernelArchX86"
+)
+
+config_option(KernelUseLogcalIDs USE_LOGCAL_IDS
+ "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."
+ DEFAULT OFF
+ DEPENDS "NOT ${KernelMaxNumNodes} EQUAL 1;KernelArchX86"
+)
+
+config_string(KernelCacheLnSz CACHE_LN_SZ
+ "Define cache line size for the current architecture"
+ DEFAULT 64
+ DEPENDS "KernelArchX86" UNDEF_DISABLED
+ UNQUOTE
+)
+
+config_option(KernelVTX VTX
+ "VTX support"
+ DEFAULT OFF
+ DEPENDS "KernelArchX86;NOT KernelVerificationBuild"
+)
+
+config_string(KernelMaxVPIDs MAX_VPIDS
+ "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."
+ DEFAULT 1024
+ DEPENDS "KernelVTX" DEFAULT_DISABLED 0
+ UNQUOTE
+)
+
+config_option(KernelHugePage HUGE_PAGE
+ "Add support for 1GB huge page. Not all recent processor models support this feature."
+ DEFAULT ON
+ DEPENDS "KernelSel4ArchX86_64" DEFAULT_DISABLED OFF
+)
+config_option(KernelSupportPCID SUPPORT_PCID
+ "Add support for PCIDs (aka hardware ASIDs). Not all processor models support this feature."
+ DEFAULT ON
+ DEPENDS "KernelSel4ArchX86_64" DEFAULT_DISABLED OFF
+)
+
+config_choice(KernelSyscall KERNEL_X86_SYSCALL
+ "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"
+ "syscall;KernelX86SyscallSyscall;SYSCALL;KernelSel4ArchX86_64"
+ "sysenter;KernelX86SyscallSysenter;SYSENTER;KernelArchX86"
+)
+
+config_choice(KernelFPU KERNEL_X86_FPU "Choose the method that FPU state is stored in. This \
+ directly affects the method used to save and restore it. \
+ FXSAVE -> This chooses the legacy 512-byte region used by the fxsave and fxrstor functions \
+ XSAVE -> 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."
+ "XSAVE;KernelFPUXSave;XSAVE;KernelArchX86"
+ "FXSAVE;KernelFPUFXSave;FXSAVE;KernelArchX86"
+)
+
+config_choice(KernelXSave KERNEL_XSAVE "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. \
+ XSAVE -> Original XSAVE instruction. This is the only XSAVE instruction that is guaranteed to exist if \
+ XSAVE is present \
+ XSAVEC -> 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 \
+ XSAVEOPT -> Save state taking advantage of both the init optimization and modified optimization \
+ XSAVES -> 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."
+ "XSAVEOPT;KernelXSaveXsaveOpt;XSAVE_XSAVEOPT;KernelFPUXSave"
+ "XSAVE;KernelXSaveXsave;XSAVE_XSAVE;KernelFPUXSave"
+ "XSAVEC;KernelXSaveXSaveC;XSAVE_XSAVEC;KernelFPUXSave"
+)
+config_string(KernelXSaveFeatureSet XSAVE_FEATURE_SET
+ "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."
+ DEFAULT 3
+ DEPENDS "KernelFPUXSave" DEFAULT_DISABLED 0
+ UNQUOTE
+)
+
+if(KernelFPUXSave)
+ set(default_xsave_size 576)
+else()
+ set(default_xsave_size 512)
+endif()
+
+config_string(KernelXSaveSize XSAVE_SIZE
+ "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."
+ DEFAULT ${default_xsave_size}
+ DEPENDS "KernelArchX86" DEFAULT_DISABLED 0
+ UNQUOTE
+)
+
+config_choice(KernelFSGSBase KERNEL_FSGS_BASE
+ "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."
+ "inst;KernelFSGSBaseInst;FSGSBASE_INST;KernelSel4ArchX86_64"
+ "gdt;KernelFSGSBaseGDT;FSGSBASE_GDT;KernelSel4ArchIA32"
+ "msr;KernelFSGSBaseMSR;FSGSBASE_MSR;KernelSel4ArchX86_64"
+)
+
+config_choice(KernelMultibootGFXMode KERNEL_MUTLTIBOOT_GFX_MODE
+ "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"
+ "none;KernelMultibootGFXModeNone;MULTIBOOT_GRAPHICS_MODE_NONE;KernelArchX86"
+ "text;KernelMultibootGFXModeText;MULTIBOOT_GRAPHICS_MODE_TEXT;KernelArchX86"
+ "linear;KernelMultibootGFXModeLinear;MULTIBOOT_GRAPHICS_MODE_LINEAR;KernelArchX86"
+)
+
+config_string(KernelMultibootGFXDepth MULTIBOOT_GRAPHICS_MODE_DEPTH
+ "The bits per pixel of the linear graphics mode ot request. Value of zero indicates \
+ no preference."
+ DEFAULT 32
+ DEPENDS "KernelMultibootGFXModeLinear" UNDEF_DISABLED
+ UNQUOTE
+)
+
+config_string(KernelMultibootGFXWidth MULTIBOOT_GRAPHICS_MODE_WIDTH
+ "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."
+ DEFAULT 0
+ DEPENDS "KernelMultibootGFXModeText OR KernelMultibootGFXModeLinear" UNDEF_DISABLED
+ UNQUOTE
+)
+config_string(KernelMultibootGFXHeight MULTIBOOT_GRAPHICS_MODE_HEIGHT
+ "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."
+ DEFAULT 0
+ DEPENDS "KernelMultibootGFXModeText OR KernelMultibootGFXModeLinear" UNDEF_DISABLED
+ UNQUOTE
+)
+
+add_sources(
+ DEP "KernelArchX86"
+ PREFIX src/arch/x86
+ CFILES
+ c_traps.c
+ idle.c
+ api/faults.c
+ object/interrupt.c
+ object/ioport.c
+ object/objecttype.c
+ object/tcb.c
+ object/iospace.c
+ object/vcpu.c
+ 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
+ model/statedata.c
+ machine/hardware.c
+ machine/fpu.c
+ machine/cpu_identification.c
+ machine/breakpoint.c
+ machine/registerset.c
+ benchmark/benchmark.c
+ smp/ipi.c
+ ASMFILES
+ multiboot.S
+)
+
+add_sources(
+ DEP "KernelArchX86;KernelDebugBuild"
+ CFILES src/arch/x86/machine/capdl.c
+)
+
+add_bf_source_old("KernelArchX86" "structures.bf" "include/arch/x86" "arch/object")
+
+include(src/plat/pc99/config.cmake)
+
+include(src/arch/x86/32/config.cmake)
+include(src/arch/x86/64/config.cmake)
diff --git a/src/config.cmake b/src/config.cmake
new file mode 100644
index 000000000..cc91ba309
--- /dev/null
+++ b/src/config.cmake
@@ -0,0 +1,44 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+add_sources(CFILES
+ src/inlines.c
+ src/assert.c
+ src/util.c
+ src/string.c
+ src/fastpath/fastpath.c
+ src/api/syscall.c
+ src/api/faults.c
+ src/kernel/cspace.c
+ src/kernel/faulthandler.c
+ src/kernel/thread.c
+ src/kernel/boot.c
+ src/kernel/stack.c
+ 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
+ src/model/preemption.c
+ src/model/statedata.c
+ src/machine/io.c
+ src/machine/registerset.c
+ src/machine/fpu.c
+ src/benchmark/benchmark_track.c
+ src/benchmark/benchmark_utilisation.c
+ src/smp/lock.c
+ src/smp/ipi.c
+)
diff --git a/src/plat/am335x/config.cmake b/src/plat/am335x/config.cmake
new file mode 100644
index 000000000..b2984d942
--- /dev/null
+++ b/src/plat/am335x/config.cmake
@@ -0,0 +1,27 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+if(KernelPlatformAM335X)
+ set(KernelArmCortexA8 ON)
+ set(KernelArchArmV7a ON)
+ config_set(KernelPlatform PLAT "am335x")
+endif()
+
+add_sources(
+ DEP "KernelPlatformAM335X"
+ CFILES
+ src/plat/am335x/machine/hardware.c
+ src/plat/am335x/machine/io.c
+ src/plat/am335x/machine/l2cache.c
+)
diff --git a/src/plat/apq8064/config.cmake b/src/plat/apq8064/config.cmake
new file mode 100644
index 000000000..43f36e602
--- /dev/null
+++ b/src/plat/apq8064/config.cmake
@@ -0,0 +1,29 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+if(KernelPlatformAPQ8064)
+ set(KernelArmCortexA15 ON)
+ set(KernelArchArmV7a ON)
+ set(KernelArchArmV7ve ON)
+ config_set(KernelPlatform PLAT "apq8064")
+endif()
+
+add_sources(
+ DEP "KernelPlatformAPQ8064"
+ CFILES
+ src/plat/apq8064/machine/hardware.c
+ src/plat/apq8064/machine/l2cache.c
+ src/plat/apq8064/machine/io.c
+ src/plat/apq8064/machine/timer.c
+)
diff --git a/src/plat/bcm2837/config.cmake b/src/plat/bcm2837/config.cmake
new file mode 100644
index 000000000..ad7189233
--- /dev/null
+++ b/src/plat/bcm2837/config.cmake
@@ -0,0 +1,29 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+if(KernelPlatformRpi3)
+ set(KernelArmCortexA53 ON)
+ set(KernelArchArmV8a ON)
+ config_set(KernelPlatform PLAT "bcm2837")
+ set(KernelArmMachFeatureModifiers "+crc" CACHE INTERNAL "")
+endif()
+
+add_sources(
+ DEP "KernelPlatformRpi3"
+ CFILES
+ src/plat/bcm2837/machine/hardware.c
+ src/plat/bcm2837/machine/io.c
+ src/plat/bcm2837/machine/intc.c
+ src/plat/bcm2837/machine/l2cache.c
+)
diff --git a/src/plat/exynos4/config.cmake b/src/plat/exynos4/config.cmake
new file mode 100644
index 000000000..96955b9c0
--- /dev/null
+++ b/src/plat/exynos4/config.cmake
@@ -0,0 +1,27 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+if(KernelPlatformExynos4)
+ set(KernelArmCortexA9 ON)
+ set(KernelArchArmV7a ON)
+ config_set(KernelPlatform PLAT "exynos4")
+ config_set(KernelArmMach MACH "exynos")
+endif()
+
+add_sources(
+ DEP "KernelPlatformExynos4"
+ CFILES
+ src/plat/exynos_common/mct.c
+ src/plat/exynos_common/io.c
+)
diff --git a/src/plat/exynos5/config.cmake b/src/plat/exynos5/config.cmake
new file mode 100644
index 000000000..7d54eeac4
--- /dev/null
+++ b/src/plat/exynos5/config.cmake
@@ -0,0 +1,38 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+if(KernelPlatformExynos5250 OR KernelPlatformExynos5410 OR KernelPlatformExynos5422)
+ set(KernelArmCortexA15 ON)
+ set(KernelArchArmV7ve ON)
+ # v7ve is a superset of v7a, so we enable that as well
+ set(KernelArchArmV7a ON)
+ config_set(KernelPlatform PLAT "exynos5")
+ config_set(KernelArmMach MACH "exynos")
+ config_set(KernelPlatExynos5 PLAT_EXYNOS5 ON)
+ if (KernelPlatformExynos5410 OR KernelPlatformExynos5422)
+ config_set(KernelPlatExynos54xx PLAT_EXYNOS54XX ON)
+ endif()
+else()
+ config_set(KernelPlatExynos5 PLAT_EXYNOS5 OFF)
+ config_set(KernelPlatExynos54xx PLAT_EXYNOS54XX OFF)
+endif()
+
+add_sources(
+ DEP "KernelPlatExynos5"
+ CFILES
+ src/plat/exynos5/machine/hardware.c
+ src/plat/exynos5/machine/l2cache.c
+ src/plat/exynos_common/mct.c
+ src/plat/exynos_common/io.c
+)
diff --git a/src/plat/hikey/config.cmake b/src/plat/hikey/config.cmake
new file mode 100644
index 000000000..20a5a852f
--- /dev/null
+++ b/src/plat/hikey/config.cmake
@@ -0,0 +1,76 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+config_string(KernelArmHikeyOutstandingPrefetchers ARM_HIKEY_OUTSTANDING_PREFETCHERS
+ "Number of outstanding prefetch allowed \
+ 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."
+ DEFAULT 5
+ DEPENDS "KernelPlatformHikey;NOT KernelDebugDisablePrefetchers" DEFAULT_DISABLED 0
+ UNQUOTE
+)
+set_property(CACHE KernelArmHikeyOutstandingPrefetchers PROPERTY STRINGS "1;2;3;4;5;6;7")
+
+config_string(KernelArmHikeyPrefetcherStride ARM_HIKEY_PREFETCHER_STRIDE
+ "Number of strides before prefetcher is triggered \
+ Number of strides before prefetcher is triggered. \
+ Allowed values are 2 and 3. 2 is the reset value"
+ DEFAULT 2
+ DEPENDS "KernelPlatformHikey;NOT KernelDebugDisablePrefetchers" DEFAULT_DISABLED 0
+ UNQUOTE
+)
+set_property(CACHE KernelArmHikeyPrefetcherStride PROPERTY STRINGS "2;3")
+
+config_string(KernelArmHikeyPrefetcherNPFSTRM ARM_HIKEY_PREFETCHER_NPFSTRM
+ "Number of indepedent prefetch streams \
+ Number of indepedent prefetch streams. Allowed values are 1 to 4.\
+ 2 is the reset value"
+ DEFAULT 2
+ DEPENDS "KernelPlatformHikey;NOT KernelDebugDisablePrefetchers" DEFAULT_DISABLED 0
+ UNQUOTE
+)
+set_property(CACHE KernelArmHikeyPrefetcherNPFSTRM PROPERTY STRINGS "1;2;3;4")
+
+config_option(KernelArmHikeyPrefetcherSTBPFDIS ARM_HIKEY_PREFETCHER_STBPFDIS
+ "Enable prefetch streams initated by STB access \
+ Enable prefetch streams initated by STB access. Enabled is the reset value"
+ DEFAULT ON
+ DEPENDS "KernelPlatformHikey; NOT KernelDebugDisablePrefetchers" DEFAULT_DISABLED OFF
+)
+
+config_option(KernelArmHikeyPrefetcherSTBPFRS ARM_HIKEY_PREFETCHER_STBPFRS
+ "Prefetcher to initated on a ReadUnique or ReadShared \
+ Sets prefetcher to initated on a ReadUnique (n) or ReadShared (y) \
+ ReadUnique is the reset value"
+ DEFAULT OFF
+ DEPENDS "KernelPlatformHikey;NOT KernelDebugDisablePrefetchers"
+)
+
+if(KernelPlatformHikey)
+ set(KernelArmCortexA53 ON)
+ set(KernelArchArmV8a ON)
+ config_set(KernelPlatform PLAT "hikey")
+ set(KernelArmMachFeatureModifiers "+crc" CACHE INTERNAL "")
+ if(KernelSel4ArchAarch64)
+ set(KernelHaveFPU ON)
+ endif()
+endif()
+
+add_sources(
+ DEP "KernelPlatformHikey"
+ CFILES
+ src/plat/hikey/machine/hardware.c
+ src/plat/hikey/machine/io.c
+)
diff --git a/src/plat/imx31/config.cmake b/src/plat/imx31/config.cmake
new file mode 100644
index 000000000..c0f340d6c
--- /dev/null
+++ b/src/plat/imx31/config.cmake
@@ -0,0 +1,27 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+if(KernelPlatformKZM)
+ set(KernelArm1136JF_S ON)
+ set(KernelArchArmV6 ON)
+ config_set(KernelPlatform PLAT "imx31")
+ set(KernelArmMach "imx" CACHE INTERNAL "")
+endif()
+
+add_sources(
+ DEP "KernelPlatformKZM"
+ CFILES
+ src/plat/imx31/machine/io.c
+ src/plat/imx31/machine/hardware.c
+)
diff --git a/src/plat/imx6/config.cmake b/src/plat/imx6/config.cmake
new file mode 100644
index 000000000..1438fcdb6
--- /dev/null
+++ b/src/plat/imx6/config.cmake
@@ -0,0 +1,28 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+if(KernelPlatformWandQ OR KernelPlatformSabre)
+ set(KernelArmCortexA9 ON)
+ set(KernelArchArmV7a ON)
+ config_set(KernelPlatImx6 PLAT_IMX6 ON)
+ config_set(KernelPlatform PLAT "imx6")
+ set(KernelArmMach "imx" CACHE INTERNAL "")
+else()
+ config_set(KernelPlatImx6 PLAT_IMX6 OFF)
+endif()
+
+add_sources(
+ DEP "KernelPlatImx6"
+ CFILES src/plat/imx6/machine/io.c
+)
diff --git a/src/plat/omap3/config.cmake b/src/plat/omap3/config.cmake
new file mode 100644
index 000000000..6ca67899d
--- /dev/null
+++ b/src/plat/omap3/config.cmake
@@ -0,0 +1,28 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+if(KernelPlatformOMAP3)
+ set(KernelArmCortexA8 ON)
+ set(KernelArchArmV7a ON)
+ config_set(KernelPlatform PLAT "omap3")
+ config_set(KernelArmMach MACH "omap")
+endif()
+
+add_sources(
+ DEP "KernelPlatformOMAP3"
+ CFILES
+ src/plat/omap3/machine/hardware.c
+ src/plat/omap3/machine/io.c
+ src/plat/omap3/machine/l2cache.c
+)
diff --git a/src/plat/pc99/config.cmake b/src/plat/pc99/config.cmake
new file mode 100644
index 000000000..253a2f25b
--- /dev/null
+++ b/src/plat/pc99/config.cmake
@@ -0,0 +1,43 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+config_option(KernelIOMMU IOMMU
+ "IOMMU support for VT-d enabled chipset"
+ DEFAULT ON
+ DEPENDS "KernelPlatPC99; NOT KernelVerificationBuild" DEFAULT_DISABLED OFF
+)
+
+config_string(KernelMaxRMRREntries MAX_RMRR_ENTRIES
+ "Setsthe maximum number of Reserved Memory Region Reporting structures we support \
+ recording from the ACPI tables"
+ DEFAULT 32
+ DEPENDS "KernelIOMMU" DEFAULT_DISABLED 0
+ UNQUOTE
+)
+
+add_sources(
+ DEP "KernelPlatPC99"
+ PREFIX src/plat/pc99/machine
+ CFILES
+ acpi.c
+ hardware.c
+ pic.c
+ ioapic.c
+ pit.c
+ io.c
+ intel-vtd.c
+)
+
+add_bf_source_old("KernelSel4ArchX86_64" "hardware.bf" "include/plat/pc99/plat/64" "plat_mode/machine")
+add_bf_source_old("KernelSel4ArchIA32" "hardware.bf" "include/plat/pc99/plat/32" "plat_mode/machine")
diff --git a/src/plat/tk1/config.cmake b/src/plat/tk1/config.cmake
new file mode 100644
index 000000000..d28a296f5
--- /dev/null
+++ b/src/plat/tk1/config.cmake
@@ -0,0 +1,30 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+if(KernelPlatformJetson)
+ set(KernelArmCortexA15 ON)
+ set(KernelArchArmV7a ON)
+ set(KernelArchArmV7ve ON)
+ config_set(KernelPlatform PLAT "tk1")
+ config_set(KernelArmMach MACH "nvidia")
+endif()
+
+add_sources(
+ DEP "KernelPlatformJetson"
+ CFILES
+ src/plat/tk1/machine/hardware.c
+ src/plat/tk1/machine/io.c
+ src/plat/tk1/machine/l2cache.c
+ src/plat/tk1/machine/smmu.c
+)
diff --git a/src/plat/tx1/config.cmake b/src/plat/tx1/config.cmake
new file mode 100644
index 000000000..3341b2434
--- /dev/null
+++ b/src/plat/tx1/config.cmake
@@ -0,0 +1,29 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+if(KernelPlatformTx1)
+ set(KernelArmCortexA57 ON)
+ set(KernelArchArmV8a ON)
+ config_set(KernelPlatform PLAT "tx1")
+ config_set(KernelArmMach MACH "nvidia")
+ set(KernelHaveFPU ON)
+endif()
+
+add_sources(
+ DEP "KernelPlatformTx1"
+ CFILES
+ src/plat/tx1/machine/hardware.c
+ src/plat/tx1/machine/io.c
+ src/plat/tx1/machine/l2cache.c
+)
diff --git a/src/plat/zynq7000/config.cmake b/src/plat/zynq7000/config.cmake
new file mode 100644
index 000000000..ca3f788fd
--- /dev/null
+++ b/src/plat/zynq7000/config.cmake
@@ -0,0 +1,24 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+if(KernelPlatformZynq7000)
+ set(KernelArmCortexA9 ON)
+ set(KernelArchArmV7a ON)
+ config_set(KernelPlatform PLAT "zynq7000")
+endif()
+
+add_sources(
+ DEP "KernelPlatformZynq7000"
+ CFILES src/plat/zynq7000/machine/io.c
+)
diff --git a/tools/flags.cmake b/tools/flags.cmake
new file mode 100644
index 000000000..1481c9ad8
--- /dev/null
+++ b/tools/flags.cmake
@@ -0,0 +1,21 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+# Set the cmake compilation flags with kernel base flags
+# This allows, for example, user compilation to ensure they are building for the same
+# architecture / cpu as the kernel was compiled for
+set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} ${BASE_C_FLAGS}")
+set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${BASE_CXX_FLAGS}")
+set(CMAKE_ASM_FLAGS "${CMAKE_ASM_FLAGS} ${BASE_ASM_FLAGS}")
+set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${BASE_EXE_LINKER_FLAGS}")
diff --git a/tools/helpers.cmake b/tools/helpers.cmake
new file mode 100644
index 000000000..c8990189d
--- /dev/null
+++ b/tools/helpers.cmake
@@ -0,0 +1,488 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+include(CMakeDependentOption)
+
+# Wrapper function around find_file that generates a fatal error if it isn't found
+# Is equivalent to find_file except that it adds CMAKE_CURRENT_SOURCE_DIR as a path and sets
+# CMAKE_FIND_ROOT_PATH_BOTH
+function(RequireFile config_name file_name)
+ find_file(${config_name} "${file_name}" PATHS "${CMAKE_CURRENT_SOURCE_DIR}" CMAKE_FIND_ROOT_PATH_BOTH ${ARGV})
+ if("${${config_name}}" STREQUAL "${config_name}-NOTFOUND")
+ message(FATAL_ERROR "Failed to find required file ${file_name}")
+ endif()
+ mark_as_advanced(FORCE ${config_name})
+endfunction(RequireFile)
+
+# Helper macro for converting a filename to an absolute path. It first converts to
+# an absolute path based in the current source directory, and if the results in a file
+# that doesn't exist it returns an absolute path based from the binary directory
+# This file check is done at generation time and is considered safe as source files
+# should not be being added as part of the build step (except into the build directory)
+macro(get_absolute_source_or_binary output input)
+ get_filename_component(${output} "${input}" ABSOLUTE BASE_DIR "${CMAKE_CURRENT_SOURCE_DIR}")
+ if(NOT EXISTS "${${output}}")
+ get_filename_component(${output} "${input}" ABSOLUTE BASE_DIR "${CMAKE_CURRENT_BINARY_DIR}")
+ endif()
+endmacro(get_absolute_source_or_binary)
+
+# Generates a custom command that preprocesses an input file into an output file
+# Uses the current CMAKE_C_FLAGS as well as any EXTRA_FLAGS provided. Can also
+# be given any EXTRA_DEPS to depend upon
+# If TARGET is provided then an additional custom_target with that name will be generated
+# that just depends upon output
+# Output and input files will be converted to absolute paths based on the following rules
+# * Output is assumed to be in CMAKE_CURRENT_BINARY_DIR
+# * Input is assumed to be in CMAKE_CURRENT_SOURCE_DIR if it resolves to a file that exists
+# otherwise it is assumed to be in CMAKE_CURRENT_BINARY_DIR
+function(GenCPPCommand output input)
+ cmake_parse_arguments(PARSE_ARGV 2 "CPP" "" "EXTRA_DEPS;EXTRA_FLAGS;TARGET" "")
+ if(NOT "${CPP_UNPARSED_ARGUMENTS}" STREQUAL "")
+ message(FATAL_ERROR "Unknown arguments to GenCPPCommand")
+ endif()
+ # Get the absolute path of the output file so we can then get its path relative
+ # to the binary directory, which we need to do for correct dependency generation
+ get_filename_component(output_absolute "${output}" ABSOLUTE BASE_DIR "${CMAKE_CURRENT_BINARY_DIR}")
+ get_absolute_source_or_binary(input_absolute "${input}")
+ file(RELATIVE_PATH rel_target_path "${CMAKE_BINARY_DIR}" "${output_absolute}")
+ add_custom_command(OUTPUT "${output_absolute}" OUTPUT "${output_absolute}.d"
+ # Pipe are arguments through sed to turn lists from generator expressions into
+ # proper space separated argument lists. Note that lists from generator expressions
+ # will *not* be separated by the separate_arguments cmake command since separate_arguments
+ # is invoke during generation, not during building and hence generator expressions will
+ # not yet be filled in
+ COMMAND echo "${CPP_EXTRA_FLAGS}" "${CMAKE_C_FLAGS}" -x c ${input_absolute}
+ | xargs "${CMAKE_C_COMPILER}" -MMD -MT "${rel_target_path}"
+ -MF "${output_absolute}.d" -E -o "${output_absolute}"
+ DEPENDS "${input_absolute}" ${CPP_EXTRA_DEPS}
+ COMMENT "Preprocessing ${input} into ${output}"
+ DEPFILE "${output_absolute}.d"
+ VERBATIM
+ )
+ if(NOT "${CPP_TARGET}" STREQUAL "")
+ add_custom_target(${CPP_TARGET}
+ DEPENDS ${output}
+ )
+ endif()
+endfunction(GenCPPCommand)
+
+# Function to generate a custom command to process a bitfield file. The input
+# (pbf_path) is either a .bf file or, if you used pre-processor directives, a
+# pre-processed .bf file. As this invokes a python tool that places a file
+# in the current working directory a unqiue 'work_dir' needs to be provided
+# for this command to execute in
+# This function is not intended to be used directly, rather one of its wrappers
+# that is specialized to generate a specific kind of output should be used
+# These wrappers work by passing the additional 'args' that get passed on to
+# the bitfield generator
+function(GenBFCommand args target_name pbf_path pbf_target deps)
+ # Since we're going to change the working directory first convert any paths to absolute
+ get_filename_component(target_name_absolute "${target_name}" ABSOLUTE BASE_DIR "${CMAKE_CURRENT_BINARY_DIR}")
+ get_absolute_source_or_binary(pbf_path_absolute "${pbf_path}")
+ add_custom_command(OUTPUT "${target_name_absolute}"
+ COMMAND "${PYTHON}" "${BF_GEN_PATH}" ${args} "${pbf_path_absolute}" "${target_name_absolute}"
+ DEPENDS "${BF_GEN_PATH}" "${pbf_path_absolute}" "${pbf_target}" ${deps}
+ COMMENT "Generating from ${pbf_path}"
+ VERBATIM
+ )
+endfunction(GenBFCommand)
+
+# Wrapper function for generating both a target and command to process a bitfield file
+function(GenBFTarget args target_name target_file pbf_path pbf_target deps)
+ GenBFCommand("${args}" "${target_file}" "${pbf_path}" "${pbf_target}" "${deps}")
+ add_custom_target(${target_name}
+ DEPENDS "${target_file}"
+ )
+endfunction(GenBFTarget)
+
+# Wrapper around GenBFTarget for generating a C header file out of a bitfield specification
+# environment is empty for kernel generation and "libsel4" for generating non kernel headers
+# prunes is an optional list of files that will be passed as --prune options to the bitfield
+# generator
+function(GenHBFTarget environment target_name target_file pbf_path pbf_target prunes deps)
+ set(args "")
+ if(NOT "${environment}" STREQUAL "")
+ list(APPEND args --environment "${environment}")
+ endif()
+ foreach(prune IN LISTS prunes)
+ get_absolute_source_or_binary(prune_absolute "${prune}")
+ list(APPEND args "--prune" "${prune_absolute}")
+ endforeach()
+ list(APPEND deps ${prunes})
+ GenBFTarget("${args}" "${target_name}" "${target_file}" "${pbf_path}" "${pbf_target}" "${deps}")
+endfunction(GenHBFTarget)
+
+# Wrapper for generating different kinds of .thy files from bitfield specifications
+function(GenThyBFTarget args target_name target_file pbf_path pbf_target prunes deps)
+ get_filename_component(cspec_dir "${CSPEC_DIR}" REALPATH BASE_DIR)
+ list(APPEND args --cspec-dir "${cspec_dir}")
+ if(SKIP_MODIFIES)
+ list(APPEND args "--skip_modifies")
+ endif()
+ foreach(prune IN LISTS prunes)
+ list(APPEND args "--prune" "${prune}")
+ endforeach()
+ list(APPEND deps "${CSPEC_DIR}/Kernel_C.thy" ${prunes})
+ GenBFTarget("${args}" "${target_name}" "${target_file}" "${pbf_path}" "${pbf_target}" "${deps}")
+endfunction(GenThyBFTarget)
+
+# Generate hol definitions from a bitfield specification
+function(GenDefsBFTarget target_name target_file pbf_path pbf_target prunes deps)
+ set(args "")
+ list(APPEND args --hol_defs)
+ GenThyBFTarget("${args}" "${target_name}" "${target_file}" "${pbf_path}" "${pbf_target}" "${prunes}" "${deps}")
+endfunction(GenDefsBFTarget)
+
+# Generate proofs from a bitfield specification
+function(GenProofsBFTarget target_name target_file pbf_path pbf_target prunes deps)
+ set(args "")
+ # Get an absolute path to cspec_dir so that the final theory file is portable
+ list(APPEND args --hol_proofs --umm_types "${UMM_TYPES}")
+ if(SORRY_BITFIELD_PROOFS)
+ list(APPEND args "--sorry_lemmas")
+ endif()
+ foreach(type IN LISTS TOPLEVELTYPES)
+ list(APPEND args "--toplevel" "${type}")
+ endforeach()
+ list(APPEND deps "${UMM_TYPES}")
+ GenThyBFTarget("${args}" "${target_name}" "${target_file}" "${pbf_path}" "${pbf_target}" "${prunes}" "${deps}")
+endfunction(GenProofsBFTarget)
+
+# config_option(cmake_option_name c_config_name doc DEFAULT default [DEPENDS deps] [DEFAULT_DISABLE default_disabled])
+# Defines a toggleable configuration option that will be present in the cache and the
+# cmake-gui
+# optionname is the name of the cache variable that can be used directly in cmake scripts
+# to get the value of the option
+# configname is the name (prefixed with CONFIG_) that will appear in generated
+# C configuration headers
+# DEFAULT is the default value of the config that it should initially be set to
+# doc Help string to explain the option in the cmake-gui
+# An additional DEPENDS arguments may be passed, which is a list of conditions to evaluate and if true,
+# the option will exist. If the option doesn't exist it will be set to DEFAULT_DISABLED, or if
+# that wasn't provided then just DEFAULT
+# If the option is true it adds to the global configure_string variable (see add_config_library)
+function(config_option optionname configname doc)
+ cmake_parse_arguments(PARSE_ARGV 3 "CONFIG" "" "DEPENDS;DEFAULT_DISABLED;DEFAULT" "")
+ if(NOT "${CONFIG_UNPARSED_ARGUMENTS}" STREQUAL "")
+ message(FATAL_ERROR "Unknown arguments to config_option")
+ endif()
+ if("${CONFIG_DEFAULT_DISABLED}" STREQUAL "")
+ set(CONFIG_DEFAULT_DISABLED "${CONFIG_DEFAULT}")
+ endif()
+ if("${CONFIG_DEPENDS}" STREQUAL "")
+ option(${optionname} "${doc}" ${CONFIG_DEFAULT})
+ else()
+ cmake_dependent_option(${optionname} "${doc}" "${CONFIG_DEFAULT}" "${CONFIG_DEPENDS}" "${CONFIG_DEFAULT_DISABLED}")
+ endif()
+ set(local_config_string "${configure_string}")
+ if(${optionname})
+ list(APPEND local_config_string
+ "#define CONFIG_${configname} 1"
+ )
+ endif()
+ set(configure_string "${local_config_string}" PARENT_SCOPE)
+endfunction(config_option)
+
+# Set a configuration option to a particular value. This value will not appear in
+# the cmake-gui, but will produce an internal cmake cache variable and generated
+# configuration headers.
+# If the option is not OFF it adds to the global configure_string variable (see add_config_library)
+macro(config_set optionname configname value)
+ set(${optionname} "${value}" CACHE INTERNAL "")
+ if("${value}" STREQUAL "ON")
+ list(APPEND configure_string
+ "#define CONFIG_${configname} 1"
+ )
+ elseif("${value}" STREQUAL "OFF")
+ else()
+ list(APPEND configure_string
+ "#define CONFIG_${configname} ${value}"
+ )
+ endif()
+endmacro(config_set)
+
+# config_cmake_string(cmake_option_name c_config_name doc DEFAULT default [DEPENDS dep]
+# [DEFAULT_DISABLED default_disabled] [UNDEF_DISABLED] [QUOTE]
+# Defines a configuration option that is a user configurable string. Most parameters
+# are the same as config_option
+# UNQUOTE if specified says this is something with more semantics like a number or identifier
+# and should not be quoted in the output
+# [UNDEF_DISABLED] can be specified to explicitly disable generation of any output value when
+# the configuration dependencies are unmet
+# Adds to the global configure_string variable (see add_config_library)
+function(config_string optionname configname doc)
+ cmake_parse_arguments(PARSE_ARGV 3 "CONFIG" "UNQUOTE;UNDEF_DISABLED" "DEPENDS;DEFAULT_DISABLED;DEFAULT" "")
+ if(NOT "${CONFIG_UNPARSED_ARGUMENTS}" STREQUAL "")
+ message(FATAL_ERROR "Unknown arguments to config_option: ${CONFIG_UNPARSED_ARGUMENTS}")
+ endif()
+ if("${CONFIG_DEFAULT}" STREQUAL "")
+ message(FATAL_ERROR "No default specified for ${config_option}")
+ endif()
+ if("${CONFIG_DEFAULT_DISABLED}" STREQUAL "")
+ set(CONFIG_DEFAULT_DISABLED "${CONFIG_DEFAULT}")
+ endif()
+ set(valid ON)
+ set(local_config_string "${configure_string}")
+ if(NOT "${CONFIG_DEPENDS}" STREQUAL "")
+ # Check the passed in dependencies. This loop and logic is inspired by the
+ # actual cmake_dependent_option code
+ foreach(test ${CONFIG_DEPENDS})
+ string(REGEX REPLACE " +" ";" test "${test}")
+ if(NOT (${test}))
+ set(valid OFF)
+ break()
+ endif()
+ endforeach()
+ endif()
+ if(CONFIG_UNQUOTE)
+ set(quote "")
+ else()
+ set(quote "\"")
+ endif()
+ if(valid)
+ # See if we transitioned from disabled to enabled. We do this by having an
+ # _UNAVAILABLE variable. We want to ensure that if the option previously had
+ # unmet conditions that we reset its value to 'default'. This is needed
+ # because whilst the option had unmet conditions it still potentially had
+ # a value in the form of the optional disabled_value
+ set(force "")
+ if(${optionname}_UNAVAILABLE)
+ set(force "FORCE")
+ unset(${optionname}_UNAVAILABLE)
+ endif()
+ set(${optionname} "${CONFIG_DEFAULT}" CACHE STRING "${doc}" ${force})
+ list(APPEND local_config_string
+ "#define CONFIG_${configname} ${quote}@${optionname}@${quote}"
+ )
+ else()
+ if(CONFIG_UNDEF_DISABLED)
+ unset(${optionname})
+ else()
+ # Forcively change the value to its disabled_value
+ set(${optionname} "${CONFIG_DEFAULT_DISABLED}" CACHE INTERNAL "")
+ list(APPEND local_config_string
+ "#define CONFIG_${configname} ${quote}@${optionname}@${quote}"
+ )
+ endif()
+ # Sset _UNAVAILABLE so we can detect when the option because enabled again
+ set(${optionname}_UNAVAILABLE ON CACHE INTERNAL "")
+ endif()
+ set(configure_string "${local_config_string}" PARENT_SCOPE)
+endfunction(config_string)
+
+# Defines a multi choice / select configuration option
+# optionname is the name of the cache variable that can be used directly in cmake scripts
+# to get the value of the option
+# configname is the name (prefixed with CONFIG_) that will appear in generated
+# C configuration headers and is set to the string of the selected config
+# doc Help string to explain the option in the cmake-gui
+# Then any number of additional arguments may be supplied each describing one of the potential
+# configuration choices. Each additional argument is a list of (option_value, option_cache,
+# option_config, [condition]...)
+# option_value is the string that represents this option. this is what the user will see
+# in the cmake-gui and what configname will get defined to if this option is selected
+# option_cache is like optionname and is set to ON when this option is selected and OFF
+# if it is not
+# condition may be repeated as many times and all conditions must be true for this choice
+# to appear in the list
+# If no valid choices are given (either because none are given or the ones that were given
+# did not have their conditions met) then this option will be disabled and not appear in
+# the cmake-gui
+# Adds to the global configure_string variable (see add_config_library)
+function(config_choice optionname configname doc)
+ # Cannot use ARGN because each argument itself is a list
+ math(EXPR limit "${ARGC} - 1")
+ set(local_config_string "${configure_string}")
+ # force_default represents whether we need to force a new value or not. We would need
+ # to force a new value for example if we detect that the current selected choice is
+ # no longer (due to conditions) a valid choice
+ set(force_default "")
+ # Used to track the first time we see a valid enabled choice. The first valid choice
+ # becomes the default and if we never find a valid choice then we know to disable this config
+ set(first ON)
+ # This tracks whether or not the current selected choice is one of the ones that we
+ # have been passed. If we fail to find the currently selected choice then, similar to
+ # if the current choice is invalid to do an unment condition, we must switch to some
+ # valid default
+ set(found_current OFF)
+ foreach(i RANGE 3 ${limit})
+ set(option "${ARGV${i}}")
+ # Extract the constant parts of the choice information and just leave any
+ # conditional information
+ list(GET option 0 option_value)
+ list(GET option 1 option_cache)
+ list(GET option 2 option_config)
+ list(REMOVE_AT option 0 1 2)
+ # By default we assume is valid, we may change our mind after checking dependencies
+ # (if there are any). This loop is again based off the one in cmake_dependent_option
+ set(valid ON)
+ foreach(truth IN LISTS option)
+ string(REGEX REPLACE " +" ";" truth "${truth}")
+ if(NOT (${truth}))
+ # This choice isn't valid due to unmet conditions so we must check if we have
+ # currently selected this choice. If so trigger the force_default
+ if("${${optionname}}" STREQUAL "${option_value}")
+ set(force_default "FORCE")
+ endif()
+ set(valid OFF)
+ endif()
+ endforeach()
+ if(valid)
+ # Is a valid option, add to the strings list
+ list(APPEND strings "${option_value}")
+ if(first)
+ set(first OFF)
+ set(first_cache "${option_cache}")
+ set(first_config "${option_config}")
+ # Use the first valid option we find as the default. This default is will be
+ # used if there is no current value, or for some reason we need to override
+ # the current value (see force_default above)
+ set(default "${option_value}")
+ endif()
+ # Check if this option is the one that is currently set
+ if("${${optionname}}" STREQUAL "${option_value}")
+ set(${option_cache} ON CACHE INTERNAL "")
+ list(APPEND local_config_string
+ "#define CONFIG_${option_config} 1"
+ )
+ set(found_current ON)
+ else()
+ set(${option_cache} OFF CACHE INTERNAL "")
+ endif()
+ else()
+ # Remove this config as it's not valid
+ unset(${option_cache} CACHE)
+ endif()
+ endforeach()
+ if(NOT found_current)
+ # Currently selected option wasn't found so reset to a default that we know is valid
+ set(force_default "FORCE")
+ endif()
+ if(first)
+ # None of the choices were valid. Remove this option so its not visible
+ unset(${optionname} CACHE)
+ else()
+ list(APPEND local_config_string
+ "#define CONFIG_${configname} @${optionname}@"
+ )
+ set(configure_string "${local_config_string}" PARENT_SCOPE)
+ set(${optionname} "${default}" CACHE STRING "${doc}" ${force_default})
+ set_property(CACHE ${optionname} PROPERTY STRINGS ${strings})
+ if(NOT found_current)
+ # The option is actually enabled, but we didn't enable the correct
+ # choice earlier, since we didn't know we were going to revert to
+ # the default. So add the option setting here
+ set(${first_cache} ON CACHE INTERNAL "")
+ list(APPEND local_config_string
+ "#define CONFIG_${first_config} 1"
+ )
+ endif()
+ endif()
+ set(configure_string "${local_config_string}" PARENT_SCOPE)
+endfunction(config_choice)
+
+# Defines a target for a 'configuration' library, which generates a header based
+# upon current state of cache/variables and a provided template string. Additionally
+# the generated library gets added to a known global list of 'configuration' libraries
+# This list can be used if someone wants all the configurations
+# Whilst this function takes an explicit configure_template, generally this will always
+# be '${configure_string}' as that is the global variable automatically appended to
+# by the config_ helper macros and functions above
+# This generates a library that can be linked against with
+# target_link_library(<target> ${prefix}_Config)
+# Which will allow you to do #include <${prefix}/gen_config.h>
+function(add_config_library prefix configure_template)
+ set(config_dir "${CMAKE_CURRENT_BINARY_DIR}/gen_config")
+ set(config_file "${config_dir}/${prefix}/gen_config.h")
+ string(CONFIGURE "${configure_template}" config_header_contents)
+ add_custom_command(
+ OUTPUT "${config_file}"
+ COMMAND rm -f "${config_file}"
+ COMMAND echo "${config_header_contents}" | sed "s/;/\\n/g" > "${config_file}"
+ COMMENT "Generating config file for ${prefix}"
+ VERBATIM
+ )
+ add_custom_target(${prefix}_Gen DEPENDS "${config_file}")
+ add_library(${prefix}_Config INTERFACE)
+ target_include_directories(${prefix}_Config INTERFACE "${config_dir}")
+ add_dependencies(${prefix}_Config ${prefix}_Gen ${config_file})
+ set_property(GLOBAL APPEND PROPERTY CONFIG_LIBRARIES "${prefix}")
+ # Set a property on the library that is a list of the files we generated. This
+ # allows custom build commands to easily get a file dependency list so they can
+ # 'depend' upon this target easily
+ set_property(TARGET ${prefix}_Gen APPEND PROPERTY GENERATED_FILES "${config_file}")
+endfunction(add_config_library)
+
+macro(get_generated_files output target)
+ get_property(${output} TARGET ${target} PROPERTY GENERATED_FILES)
+endmacro(get_generated_files)
+
+# This rule tries to emulate an 'autoconf' header. autoconf generated headers
+# were previously used as configuration, so this rule provides a way for previous
+# applications and libraries to build without modification. The config_list
+# is a list of 'prefix' values that have been pssed to add_config_library
+# This generates a library with ${targetname} that when linked against
+# will allow code to simply #include <autoconf.h>
+function(generate_autoconf targetname config_list)
+ set(link_list "")
+ set(extra_deps_list "")
+ set(gen_list "")
+ set(include_list
+ "#ifndef AUTOCONF_${targetname}_H"
+ "#define AUTOCONF_${targetname}_H"
+ )
+ foreach(config IN LISTS config_list)
+ list(APPEND link_list "${config}_Config")
+ list(APPEND extrap_deps_list "${config}_Gen")
+ get_generated_files(gens ${config}_Gen)
+ list(APPEND gen_list ${gens})
+ list(APPEND include_list "#include <${config}/gen_config.h>")
+ endforeach()
+ list(APPEND include_list "#endif")
+ set(config_dir "${CMAKE_CURRENT_BINARY_DIR}/autoconf")
+ set(config_file "${config_dir}/autoconf.h")
+ add_custom_command(
+ OUTPUT "${config_file}"
+ DEPENDS ${extra_deps_list}
+ COMMAND rm -f "${config_file}"
+ COMMAND echo "#define AUTOCONF_INCLUDED;${include_list}" | sed "s/;/\\n/g" > "${config_file}"
+ COMMENT "Generating autoconf.h"
+ VERBATIM
+ )
+ add_custom_target(${targetname}_Gen DEPENDS "${config_file}")
+ add_library(${targetname} INTERFACE)
+ target_link_libraries(${targetname} INTERFACE ${link_list})
+ target_include_directories(${targetname} INTERFACE "${config_dir}")
+ add_dependencies(${targetname} ${targetname}_Gen ${config_file})
+ # Set our GENERATED_FILES property to include the GENERATED_FILES of all of our input
+ # configurations, as well as the files we generated
+ set_property(TARGET ${targetname}_Gen APPEND PROPERTY GENERATED_FILES "${config_file}" ${gen_list})
+endfunction(generate_autoconf)
+
+# Macro that allows for appending to a specified list only if all the supplied conditions are true
+macro(list_append_if list dep)
+ set(list_append_local_list ${${list}})
+ set(list_append_valid ON)
+ foreach(truth IN ITEMS ${dep})
+ string(REGEX REPLACE " +" ";" truth "${truth}")
+ if(NOT (${truth}))
+ set(list_append_valid OFF)
+ break()
+ endif()
+ endforeach()
+ if(list_append_valid)
+ list(APPEND list_append_local_list ${ARGN})
+ endif()
+ set(${list} ${list_append_local_list} PARENT_SCOPE)
+endmacro(list_append_if)
diff --git a/tools/internal.cmake b/tools/internal.cmake
new file mode 100644
index 000000000..64a717733
--- /dev/null
+++ b/tools/internal.cmake
@@ -0,0 +1,99 @@
+#
+# 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)
+#
+
+cmake_minimum_required(VERSION 3.7.2)
+
+# File for helpers that are very specific to the kernel
+
+function(gen_invocation_header)
+ cmake_parse_arguments(PARSE_ARGV 0 "GEN" "LIBSEL4;ARCH;SEL4ARCH" "OUTPUT;XML" "")
+ if (NOT "${GEN_UNPARSED_ARGUMENTS}" STREQUAL "")
+ message(FATAL_ERROR "Unknown arguments to gen_invocation_header: ${GEN_UNPARSED_ARGUMENTS}")
+ endif()
+ # Ensure only one of arch or sel4arch
+ if (GEN_ARCH AND GEN_SEL4ARCH)
+ message(FATAL_ERROR "Can only specify one of ARCH or SEL4ARCH")
+ endif()
+ # OUTPUT and XML are required
+ if (("${GEN_OUTPUT}" STREQUAL "") OR ("${GEN_XML}" STREQUAL ""))
+ message(FATAL_ERROR "OUTPUT and XML must both be specified")
+ endif()
+ set(arch_setting "")
+ if (GEN_ARCH)
+ set(arch_setting "--arch")
+ elseif (GEN_SEL4ARCH)
+ set(arch_setting "--sel4_arch")
+ endif()
+ set(libsel4_setting "")
+ if (GEN_LIBSEL4)
+ set(libsel4_setting "--libsel4")
+ endif()
+ # Turn the input xml into an absolute path as we build commands that may be
+ # be run with a working directory that is not the current source directory
+ get_absolute_source_or_binary(xml_absolute "${GEN_XML}")
+ add_custom_command(OUTPUT "${GEN_OUTPUT}"
+ COMMAND rm -f "${GEN_OUTPUT}"
+ COMMAND "${PYTHON}" "${INVOCATION_ID_GEN_PATH}" --xml "${xml_absolute}"
+ ${libsel4_setting} ${arch_setting} --dest "${GEN_OUTPUT}"
+ DEPENDS "${xml_absolute}" "${INVOCATION_ID_GEN_PATH}"
+ COMMENT "Generate invocation header ${GEN_OUTPUT}"
+ )
+endfunction(gen_invocation_header)
+
+# Adds files to the global sources list, but only if the supplied dependencies are met.
+# A dependency lists can be specified with DEP and CFILES are added to c_sources whilst
+# ASMFILES are added to asm_sources. An PREFIX can be given as path to prefix to each
+# C and ASM file given
+function(add_sources)
+ cmake_parse_arguments(PARSE_ARGV 0 "ADD" "" "DEP;PREFIX" "CFILES;ASMFILES")
+ if(NOT "${ADD_UNPARSED_ARGUMENTS}" STREQUAL "")
+ message(FATAL_ERROR "Unknown arguments to add_c_sources: ${ADD_UNPARSED_ARGUMENTS}")
+ endif()
+ # Need to prefix files with the CMAKE_CURRENT_SOURCE_DIR as we use these
+ # in custom commands whose working directory is not the source directory
+ # Also need to ensure that if an additional prefix wasn't specified by the
+ # caller, that we don't add an additional /, as this will screw up file sorting
+ if(NOT "${ADD_PREFIX}" STREQUAL "")
+ set(ADD_PREFIX "${ADD_PREFIX}/")
+ endif()
+ set(ADD_PREFIX "${CMAKE_CURRENT_SOURCE_DIR}/${ADD_PREFIX}")
+ foreach(file IN LISTS ADD_CFILES)
+ list(APPEND new_c_sources "${ADD_PREFIX}${file}")
+ endforeach()
+ foreach(file IN LISTS ADD_ASMFILES)
+ list(APPEND new_asm_sources "${ADD_PREFIX}${file}")
+ endforeach()
+ list_append_if(c_sources "${ADD_DEP}" ${new_c_sources})
+ list_append_if(asm_sources "${ADD_DEP}" ${new_asm_sources})
+endfunction(add_sources)
+
+# If the dependencies list in the 'dep' argument is true then a bf file is added
+# to the bf_declarations list. The format of file+prefix+path is used in order to
+# separate where the bf file is located in the source, versus where it will get
+# generated.
+function(add_bf_source_old dep file prefix path)
+ list_append_if(bf_declarations "${dep}" "${CMAKE_CURRENT_SOURCE_DIR}/${prefix}/${path}/${file}:${path}")
+endfunction(add_bf_source_old)
+
+# Macro for allowing different archs etc to set the kernel type to 32-bit
+macro(set_kernel_32)
+ config_set(KernelWordSize WORD_SIZE 32)
+ set(Kernel64 OFF CACHE INTERNAL "")
+ set(Kernel32 ON CACHE INTERNAL "")
+endmacro(set_kernel_32)
+
+# Macro for allowing different archs etc to set the kernel type to 64-bit
+macro(set_kernel_64)
+ config_set(KernelWordSize WORD_SIZE 64)
+ set(Kernel64 ON CACHE INTERNAL "")
+ set(Kernel32 OFF CACHE INTERNAL "")
+endmacro(set_kernel_64)
--
GitLab