portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add a CMake based build system

Browse source 
This commit adds an alternate build system using CMake that operates indepenently of
the existing Kconfig+Kbuild+make based build system
This commit is contained in:
Adrian Danis 2017-03-17 09:42:18 +11:00
parent ac7216e528
commit 0b73072016
34 changed files with 2756 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

380
CMakeLists.txt Normal file
View file

@ -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)

245
config.cmake Normal file
View file

@ -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}")

26
configs/arm_verified.cmake Normal file
View file

@ -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 "")

34
gcc.cmake Normal file
View file

@ -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)

15
include/32/mode/config.cmake Normal file
View file

@ -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")

15
include/64/mode/config.cmake Normal file
View file

@ -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")

1
include/arch/arm/armv/armv7ve Symbolic link
View file

@ -0,0 +1 @@
armv7-a

152
libsel4/CMakeLists.txt Normal file
View file

@ -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)

37
src/arch/arm/32/config.cmake Normal file
View file

@ -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
)

32
src/arch/arm/64/config.cmake Normal file
View file

@ -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
)

24
src/arch/arm/armv/armv6/config.cmake Normal file
View file

@ -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
)

24
src/arch/arm/armv/armv7-a/config.cmake Normal file
View file

@ -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
)

24
src/arch/arm/armv/armv8-a/config.cmake Normal file
View file

@ -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
)

334
src/arch/arm/config.cmake Normal file
View file

@ -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)

32
src/arch/x86/32/config.cmake Normal file
View file

@ -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
)

32
src/arch/x86/64/config.cmake Normal file
View file

@ -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
)

262
src/arch/x86/config.cmake Normal file
View file

@ -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)

44
src/config.cmake Normal file
View file

@ -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
)

27
src/plat/am335x/config.cmake Normal file
View file

@ -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
)

29
src/plat/apq8064/config.cmake Normal file
View file

@ -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
)

29
src/plat/bcm2837/config.cmake Normal file
View file

@ -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
)

27
src/plat/exynos4/config.cmake Normal file
View file

@ -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
)

38
src/plat/exynos5/config.cmake Normal file
View file

@ -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
)

76
src/plat/hikey/config.cmake Normal file
View file

@ -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
)

27
src/plat/imx31/config.cmake Normal file
View file

@ -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
)

28
src/plat/imx6/config.cmake Normal file
View file

@ -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
)

28
src/plat/omap3/config.cmake Normal file
View file

@ -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
)

43
src/plat/pc99/config.cmake Normal file
View file

@ -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")

30
src/plat/tk1/config.cmake Normal file
View file

@ -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
)

29
src/plat/tx1/config.cmake Normal file
View file

@ -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
)

24
src/plat/zynq7000/config.cmake Normal file
View file

@ -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
)

21
tools/flags.cmake Normal file
View file

@ -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}")

488
tools/helpers.cmake Normal file
View file

@ -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)

99
tools/internal.cmake Normal file
View file

@ -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)