Permalink
Fetching contributors…
Cannot retrieve contributors at this time
89 lines (73 sloc) 2.75 KB
#
# Copyright 2014, General Dynamics C4 Systems
#
# This software may be distributed and modified according to the terms of
# the GNU General Public License version 2. Note that NO WARRANTY is provided.
# See "LICENSE_GPLv2.txt" for details.
#
# @TAG(GD_GPL)
#
PWD = $(shell pwd)
SOURCE_ROOT=${PWD}/../../../../seL4
PARSERPATH=${PWD}/../../../tools/c-parser/standalone-parser
PATH:=${PARSERPATH}:${PATH}
export PATH
SHELL=bash
BUILDROOT=${PWD}/build/${L4V_ARCH}
CONFIG=${L4V_ARCH}_verified.cmake
UMM_TYPES=${BUILDROOT}/umm_types.txt
CONFIG_DOMAIN_SCHEDULE=${PWD}/config_sched.c
ifeq ($(findstring ARM, ${L4V_ARCH}),ARM)
TOOLPREFIX ?= arm-none-eabi-
endif
ifeq (${L4V_ARCH},RISCV64)
TOOLPREFIX ?= riscv64-unknown-elf-
endif
SORRY_BITFIELD_PROOFS?=FALSE
ifeq ($(shell which ${TOOLPREFIX}cpp),)
ifeq ($(shell which cpp),)
$(error C Preprocessor '${TOOLPREFIX}cpp' not found)
else
$(warning C Preprocessor '${TOOLPREFIX}cpp' not found; defaulting to native cpp)
TOOLPREFIX :=
endif
endif
# modifies are produced by the parser
SKIP_MODIFIES=ON
FASTPATH=yes
CSPEC_DIR=${PWD}/..
# Build a list of every file in the kernel directory. We use this as the dependency basis
# for working out when we should rebuild the kernel
KERNEL_DEPS = $(shell find ${SOURCE_ROOT} -type f)
# Top level rule for rebuilding kernel_all.c_pp
${BUILDROOT}/kernel_all.c_pp: ${BUILDROOT}/.cmake_done
cd ${BUILDROOT} && ninja kernel_all_pp_wrapper
cp -a ${BUILDROOT}/kernel_all_pp.c $@
# 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.
${BUILDROOT}/.cmake_done: ${SOURCE_ROOT}/gcc.cmake ${SOURCE_ROOT}/configs/${CONFIG} ${KERNEL_DEPS} ${CONFIG_DOMAIN_SCHEDULE}
rm -rf ${BUILDROOT}
mkdir -p ${BUILDROOT}
cd ${BUILDROOT} && \
cmake -DCROSS_COMPILER_PREFIX=${TOOLPREFIX} \
-DCMAKE_TOOLCHAIN_FILE=${SOURCE_ROOT}/gcc.cmake -C ${SOURCE_ROOT}/configs/${CONFIG} \
-DCSPEC_DIR=${CSPEC_DIR} \
-DSKIP_MODIFIES=${SKIP_MODIFIES} \
-DUMM_TYPES=${UMM_TYPES} \
-DSORRY_BITFIELD_PROOFS=${SORRY_BITFIELD_PROOFS} \
-DKernelDomainSchedule=${CONFIG_DOMAIN_SCHEDULE} -G Ninja ${SOURCE_ROOT}
touch ${BUILDROOT}/.cmake_done
# called by graph-refine's seL4-example/Makefile.common
c-kernel-source: ${BUILDROOT}/kernel_all.c_pp
# called by ../spec/Makefile
cspec: ${UMM_TYPES} ${BUILDROOT}/kernel_all.c_pp
cd ${BUILDROOT} && ninja kernel_theories
${UMM_TYPES}: ${BUILDROOT}/kernel_all.c_pp
python ../mk_umm_types.py --root $(L4V_REPO_PATH) ${BUILDROOT}/kernel_all.c_pp $@
clean:
rm -rf build
rm -f ${UMM_TYPES}
.PHONY: clean