adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

cspec: provide mechanism for adding dts overlays (#591) 

Add mechanism for adding overlay.dts files to the l4v build for all
architectures apart from X64 (which does not use dts files).

For example, place a file `overlays/ARM/overlay.dts` into the tree and
the build will pick it up as custom overlay file with the correct proof
session dependencies.

If no file is provided, an empty default overlay file is used.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-03-07 14:35:53 +11:00 committed by GitHub
parent c2a9ec60a8
commit 42c4e78e9f
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
8 changed files with 83 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

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

3
spec/cspec/README.md
View File

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

41
spec/cspec/c/kernel.mk
View File

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

6
spec/cspec/c/overlays/AARCH64/default-overlay.dts Normal file
View File

@ -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. */

6
spec/cspec/c/overlays/ARM/default-overlay.dts Normal file
View File

@ -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. */

6
spec/cspec/c/overlays/ARM_HYP/default-overlay.dts Normal file
View File

@ -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. */

22
spec/cspec/c/overlays/README.md Normal file
View File

@ -0,0 +1,22 @@
<!--
Copyright 2024, Proofcraft Pty Ltd
SPDX-License-Identifier: CC-BY-SA-4.0
-->
# 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.

6
spec/cspec/c/overlays/RISCV64/default-overlay.dts Normal file
View File

@ -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. */