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