diff --git a/.gitignore b/.gitignore index ca7ae5934..c8bb96531 100644 --- a/.gitignore +++ b/.gitignore @@ -16,6 +16,7 @@ /spec/cspec/c/build /spec/cspec/c/config-build /spec/cspec/c/export +/spec/cspec/c/overlays/*/overlay.dts /spec/haskell/stack.yaml.lock /spec/haskell/doc/**/*.aux diff --git a/spec/cspec/README.md b/spec/cspec/README.md index f4fc56c6b..2bd48ff01 100644 --- a/spec/cspec/README.md +++ b/spec/cspec/README.md @@ -52,6 +52,9 @@ indicating the architecture-specific definitions and proofs to use. The default architecture is `ARM` and will be selected if none is provided. See `l4v/spec/cspec/c/Makefile` for seL4 configuration details. +The build process has an option for providing a device tree overlay file if +desired, which can customise the memory regions available to the kernel. See +the [README](c/overlays/README.md) file in `c/overlays/` for more details. Remarks ------- diff --git a/spec/cspec/c/kernel.mk b/spec/cspec/c/kernel.mk index ecc7931e5..f7e44406b 100644 --- a/spec/cspec/c/kernel.mk +++ b/spec/cspec/c/kernel.mk @@ -92,14 +92,23 @@ ${KERNEL_BUILD_ROOT}/kernel_all.c_pp: ${KERNEL_BUILD_ROOT}/.cmake_done cd ${KERNEL_BUILD_ROOT} && ninja kernel_all_pp_wrapper cp -a ${KERNEL_BUILD_ROOT}/kernel_all_pp.c $@ +ifneq ($(L4V_ARCH),X64) +OVERLAY := overlays/$(L4V_ARCH)/overlay.dts +OVERLAY_OPT := -DKernelCustomDTSOverlay=../../${OVERLAY} +DEFAULT_OVERLAY := overlays/$(L4V_ARCH)/default-overlay.dts + +${OVERLAY}: overlays/$(L4V_ARCH)/default-overlay.dts + @cp $< $@ +endif + # Initialize the CMake build. We purge the build directory and start again # whenever any of the kernel sources change, so that we can reliably pick up # changes to the build config. # This step also generates a large number of files, so we create a dummy file # .cmake_done to represent overall completion for make's dependency tracking. -${KERNEL_BUILD_ROOT}/.cmake_done: ${KERNEL_DEPS} ${CONFIG_DOMAIN_SCHEDULE} - rm -rf ${KERNEL_BUILD_ROOT} - mkdir -p ${KERNEL_BUILD_ROOT} +${KERNEL_BUILD_ROOT}/.cmake_done: ${KERNEL_DEPS} ${CONFIG_DOMAIN_SCHEDULE} ${OVERLAY} + @rm -rf ${KERNEL_BUILD_ROOT} + @mkdir -p ${KERNEL_BUILD_ROOT} cd ${KERNEL_BUILD_ROOT} && \ cmake -C ${CONFIG} \ -DCROSS_COMPILER_PREFIX=${TOOLPREFIX} \ @@ -107,8 +116,16 @@ ${KERNEL_BUILD_ROOT}/.cmake_done: ${KERNEL_DEPS} ${CONFIG_DOMAIN_SCHEDULE} -DKernelDomainSchedule=${CONFIG_DOMAIN_SCHEDULE} \ -DUMM_TYPES=$(abspath ${UMM_TYPES}) -DCSPEC_DIR=${CSPEC_DIR} \ ${KERNEL_CMAKE_OPTIMISATION} ${KERNEL_CMAKE_EXTRA_OPTIONS} \ + ${OVERLAY_OPT} \ -G Ninja ${SOURCE_ROOT} - touch ${KERNEL_BUILD_ROOT}/.cmake_done + @touch ${KERNEL_BUILD_ROOT}/.cmake_done +ifneq ($(L4V_ARCH),X64) + @if [ "$$(diff -q ${OVERLAY} ${DEFAULT_OVERLAY})" ]; then \ + echo "++ Used custom overlay for $(L4V_ARCH)"; \ + else \ + echo "-- Used default overlay for $(L4V_ARCH)"; \ + fi +endif ${UMM_TYPES}: ${KERNEL_BUILD_ROOT}/kernel_all.c_pp ${CSPEC_DIR}/mk_umm_types.py --root $(L4V_REPO_PATH) ${KERNEL_BUILD_ROOT}/kernel_all.c_pp $@ @@ -116,16 +133,24 @@ ${UMM_TYPES}: ${KERNEL_BUILD_ROOT}/kernel_all.c_pp # This target generates config files and headers only. It does not invoke # the C tool chain or preprocessor. We force CMake to skip tests for these, # so that ASpec and ExecSpec can be built with fewer dependencies. -${KERNEL_CONFIG_ROOT}/.cmake_done: ${KERNEL_DEPS} gen-config-thy.py - rm -rf ${KERNEL_CONFIG_ROOT} - mkdir -p ${KERNEL_CONFIG_ROOT} +${KERNEL_CONFIG_ROOT}/.cmake_done: ${KERNEL_DEPS} gen-config-thy.py ${OVERLAY} + @rm -rf ${KERNEL_CONFIG_ROOT} + @mkdir -p ${KERNEL_CONFIG_ROOT} cd ${KERNEL_CONFIG_ROOT} && \ cmake -C ${CONFIG} \ -DCMAKE_TOOLCHAIN_FILE=${CSPEC_DIR}/c/no-compiler.cmake \ ${KERNEL_CMAKE_OPTIMISATION} ${KERNEL_CMAKE_EXTRA_OPTIONS} \ + ${OVERLAY_OPT} \ -G Ninja ${SOURCE_ROOT} cd ${KERNEL_CONFIG_ROOT} && ninja gen_config/kernel/gen_config.json - touch ${KERNEL_CONFIG_ROOT}/.cmake_done + @touch ${KERNEL_CONFIG_ROOT}/.cmake_done +ifneq ($(L4V_ARCH),X64) + @if [ "$$(diff -q ${OVERLAY} ${DEFAULT_OVERLAY})" ]; then \ + echo "++ Used custom overlay for $(L4V_ARCH)"; \ + else \ + echo "-- Used default overlay for $(L4V_ARCH)"; \ + fi +endif # Various targets useful for binary verification. ${KERNEL_BUILD_ROOT}/kernel.elf: ${KERNEL_BUILD_ROOT}/kernel_all.c_pp diff --git a/spec/cspec/c/overlays/AARCH64/default-overlay.dts b/spec/cspec/c/overlays/AARCH64/default-overlay.dts new file mode 100644 index 000000000..f01d7c177 --- /dev/null +++ b/spec/cspec/c/overlays/AARCH64/default-overlay.dts @@ -0,0 +1,6 @@ +/* + * Copyright 2023, Proofcraft Pty Ltd + * SPDX-License-Identifier: GPL-2.0-only + */ + +/* Empty overlay file that will be used if no custom `overlay.dts` exists. */ diff --git a/spec/cspec/c/overlays/ARM/default-overlay.dts b/spec/cspec/c/overlays/ARM/default-overlay.dts new file mode 100644 index 000000000..f01d7c177 --- /dev/null +++ b/spec/cspec/c/overlays/ARM/default-overlay.dts @@ -0,0 +1,6 @@ +/* + * Copyright 2023, Proofcraft Pty Ltd + * SPDX-License-Identifier: GPL-2.0-only + */ + +/* Empty overlay file that will be used if no custom `overlay.dts` exists. */ diff --git a/spec/cspec/c/overlays/ARM_HYP/default-overlay.dts b/spec/cspec/c/overlays/ARM_HYP/default-overlay.dts new file mode 100644 index 000000000..f01d7c177 --- /dev/null +++ b/spec/cspec/c/overlays/ARM_HYP/default-overlay.dts @@ -0,0 +1,6 @@ +/* + * Copyright 2023, Proofcraft Pty Ltd + * SPDX-License-Identifier: GPL-2.0-only + */ + +/* Empty overlay file that will be used if no custom `overlay.dts` exists. */ diff --git a/spec/cspec/c/overlays/README.md b/spec/cspec/c/overlays/README.md new file mode 100644 index 000000000..9e97ad946 --- /dev/null +++ b/spec/cspec/c/overlays/README.md @@ -0,0 +1,22 @@ + + +# DTS Overlays + +This directory contains device tree overlay files that can be used to override +default platform parameters such as available memory regions. + +The default files in the repository are all empty. + +To provide an override, place a file `overlay.dts` into the respective +architecture directory, e.g. `ARM/overlay.dts`. + +The l4v build system will pick up this overlay file when it generates the +kernel configuration data and preprocessed kernel code. It will rebuild proof +sessions according to their dependencies. + +The `X64` build does not support overlays, and therefore does not provide a +default. diff --git a/spec/cspec/c/overlays/RISCV64/default-overlay.dts b/spec/cspec/c/overlays/RISCV64/default-overlay.dts new file mode 100644 index 000000000..f01d7c177 --- /dev/null +++ b/spec/cspec/c/overlays/RISCV64/default-overlay.dts @@ -0,0 +1,6 @@ +/* + * Copyright 2023, Proofcraft Pty Ltd + * SPDX-License-Identifier: GPL-2.0-only + */ + +/* Empty overlay file that will be used if no custom `overlay.dts` exists. */