1# 2# Copyright 2014, General Dynamics C4 Systems 3# 4# This software may be distributed and modified according to the terms of 5# the GNU General Public License version 2. Note that NO WARRANTY is provided. 6# See "LICENSE_GPLv2.txt" for details. 7# 8# @TAG(GD_GPL) 9# 10 11PWD = $(shell pwd) 12SOURCE_ROOT=${PWD}/../../../../seL4 13PARSERPATH=${PWD}/../../../tools/c-parser/standalone-parser 14PATH:=${PARSERPATH}:${PATH} 15export PATH 16SHELL=bash 17BUILDROOT=${PWD}/build/${L4V_ARCH} 18CONFIG=${L4V_ARCH}_verified.cmake 19UMM_TYPES=${BUILDROOT}/umm_types.txt 20 21CONFIG_DOMAIN_SCHEDULE=${PWD}/config_sched.c 22 23ifeq ($(findstring ARM, ${L4V_ARCH}),ARM) 24 TOOLPREFIX ?= arm-none-eabi- 25endif 26 27ifeq (${L4V_ARCH},RISCV64) 28 TOOLPREFIX ?= riscv64-unknown-elf- 29endif 30 31SORRY_BITFIELD_PROOFS?=FALSE 32 33ifeq ($(shell which ${TOOLPREFIX}cpp),) 34 ifeq ($(shell which cpp),) 35 $(error C Preprocessor '${TOOLPREFIX}cpp' not found) 36 else 37 $(warning C Preprocessor '${TOOLPREFIX}cpp' not found; defaulting to native cpp) 38 TOOLPREFIX := 39 endif 40endif 41 42# modifies are produced by the parser 43SKIP_MODIFIES=ON 44FASTPATH=yes 45CSPEC_DIR=${PWD}/.. 46 47# Build a list of every file in the kernel directory. We use this as the dependency basis 48# for working out when we should rebuild the kernel 49KERNEL_DEPS = $(shell find ${SOURCE_ROOT} -type f) 50 51# Top level rule for rebuilding kernel_all.c_pp 52${BUILDROOT}/kernel_all.c_pp: ${BUILDROOT}/.cmake_done 53 cd ${BUILDROOT} && ninja kernel_all_pp_wrapper 54 cp -a ${BUILDROOT}/kernel_all_pp.c $@ 55 56# Initialize the CMake build. We purge the build directory and start again 57# whenever any of the kernel sources change, so that we can reliably pick up 58# changes to the build config. 59# This step also generates a large number of files, so we create a dummy file 60# .cmake_done to represent overall completion for make's dependency tracking. 61${BUILDROOT}/.cmake_done: ${SOURCE_ROOT}/gcc.cmake ${SOURCE_ROOT}/configs/${CONFIG} ${KERNEL_DEPS} ${CONFIG_DOMAIN_SCHEDULE} 62 rm -rf ${BUILDROOT} 63 mkdir -p ${BUILDROOT} 64 cd ${BUILDROOT} && \ 65 cmake -DCROSS_COMPILER_PREFIX=${TOOLPREFIX} \ 66 -DCMAKE_TOOLCHAIN_FILE=${SOURCE_ROOT}/gcc.cmake -C ${SOURCE_ROOT}/configs/${CONFIG} \ 67 -DCSPEC_DIR=${CSPEC_DIR} \ 68 -DSKIP_MODIFIES=${SKIP_MODIFIES} \ 69 -DUMM_TYPES=${UMM_TYPES} \ 70 -DSORRY_BITFIELD_PROOFS=${SORRY_BITFIELD_PROOFS} \ 71 -DKernelDomainSchedule=${CONFIG_DOMAIN_SCHEDULE} -G Ninja ${SOURCE_ROOT} 72 touch ${BUILDROOT}/.cmake_done 73 74# called by graph-refine's seL4-example/Makefile.common 75c-kernel-source: ${BUILDROOT}/kernel_all.c_pp 76 77# called by ../spec/Makefile 78cspec: ${UMM_TYPES} ${BUILDROOT}/kernel_all.c_pp 79 cd ${BUILDROOT} && ninja kernel_theories 80 81${UMM_TYPES}: ${BUILDROOT}/kernel_all.c_pp 82 python ../mk_umm_types.py --root $(L4V_REPO_PATH) ${BUILDROOT}/kernel_all.c_pp $@ 83 84clean: 85 rm -rf build 86 rm -f ${UMM_TYPES} 87 88.PHONY: clean 89