1#
2# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3#
4# SPDX-License-Identifier: GPL-2.0-only
5#
6
7# This file contains parts of the l4v C kernel build that are reused by binary verification.
8# It allows building the C kernel in locations other than the default one used by l4v,
9# and assumes that KERNEL_BUILD_ROOT has already been set to specify the build location.
10
11ifndef L4V_REPO_PATH
12  L4V_REPO_PATH := $(realpath $(dir $(lastword ${MAKEFILE_LIST}))../../..)
13endif
14
15ifndef SOURCE_ROOT
16  SOURCE_ROOT := $(realpath ${L4V_REPO_PATH}/../seL4)
17endif
18
19CSPEC_DIR := ${L4V_REPO_PATH}/spec/cspec
20PARSERPATH := ${L4V_REPO_PATH}/tools/c-parser/standalone-parser
21
22ifndef L4V_ARCH
23  $(error L4V_ARCH is not set)
24endif
25
26ifndef CONFIG
27  CONFIG := ${SOURCE_ROOT}/configs/${L4V_ARCH}_$(if ${L4V_FEATURES},${L4V_FEATURES}_,)verified.cmake
28endif
29
30ifndef CONFIG_DOMAIN_SCHEDULE
31  CONFIG_DOMAIN_SCHEDULE := ${CSPEC_DIR}/c/config_sched.c
32endif
33
34ifndef TOOLPREFIX
35  ifndef TRY_TOOLPREFIX
36    ifeq ($(findstring ARM, ${L4V_ARCH}),ARM)
37      TRY_TOOLPREFIX := arm-none-eabi-
38    else ifeq (${L4V_ARCH},RISCV64)
39      TRY_TOOLPREFIX := riscv64-unknown-linux-gnu- riscv64-linux-gnu-
40    endif
41  endif
42  ifdef TRY_TOOLPREFIX
43    TOOLPREFIX := $(firstword $(strip $(foreach TRY,${TRY_TOOLPREFIX},$(if $(shell which ${TRY}gcc),${TRY},))))
44    ifeq (,${TOOLPREFIX})
45      $(error No gcc cross-compiler found for this L4V_ARCH)
46    endif
47  endif
48endif
49
50ifndef OBJDUMP
51  OBJDUMP := ${TOOLPREFIX}objdump
52endif
53
54ifndef UMM_TYPES
55  UMM_TYPES := ${KERNEL_BUILD_ROOT}/umm_types.txt
56endif
57
58# This duplicates parts of isa-common.mk necessary for mk_umm_types.py
59ifndef ISABELLE_HOME
60  export ISABELLE_HOME:=${L4V_REPO_PATH}/isabelle
61endif
62ifndef ISABELLE_TOOL
63  export ISABELLE_TOOL:=${ISABELLE_HOME}/bin/isabelle
64endif
65ifndef ISABELLE_PROCESS
66  export ISABELLE_PROCESS:=${ISABELLE_HOME}/bin/isabelle-process
67endif
68
69# __pycache__ directories are the only in-tree products of the kernel build.
70# But since they are generated after the cmake setup, they would cause unnecessary
71# kernel rebuilds if we treated them as dependencies of the kernel build.
72# We avoid this by excluding __pycache__ directories from the kernel dependencies.
73KERNEL_DEPS := $(shell find ${SOURCE_ROOT} -name .git -prune -o -name __pycache__ -prune -o -type f -print)
74
75# Top level rule for rebuilding kernel_all.c_pp
76${KERNEL_BUILD_ROOT}/kernel_all.c_pp: ${KERNEL_BUILD_ROOT}/.cmake_done
77	cd ${KERNEL_BUILD_ROOT} && ninja kernel_all_pp_wrapper
78	cp -a ${KERNEL_BUILD_ROOT}/kernel_all_pp.c $@
79
80# Various targets useful for binary verification.
81${KERNEL_BUILD_ROOT}/kernel.elf: ${KERNEL_BUILD_ROOT}/kernel_all.c_pp
82	cd ${KERNEL_BUILD_ROOT} && ninja kernel.elf
83
84${KERNEL_BUILD_ROOT}/kernel.elf.rodata: ${KERNEL_BUILD_ROOT}/kernel.elf
85	${OBJDUMP} -z -D $^ > $@
86
87${KERNEL_BUILD_ROOT}/kernel.elf.txt: ${KERNEL_BUILD_ROOT}/kernel.elf
88	${OBJDUMP} -dz $^ > $@
89
90${KERNEL_BUILD_ROOT}/kernel.elf.symtab: ${KERNEL_BUILD_ROOT}/kernel.elf
91	${OBJDUMP} -t $^ > $@
92
93${KERNEL_BUILD_ROOT}/kernel.sigs: ${KERNEL_BUILD_ROOT}/kernel_all.c_pp
94	MAKEFILES= make -C ${PARSERPATH} standalone-cparser
95	${PARSERPATH}/c-parser ${L4V_ARCH} --underscore_idents --mmbytes $^ > $@.tmp
96	mv $@.tmp $@
97
98# Initialize the CMake build. We purge the build directory and start again
99# whenever any of the kernel sources change, so that we can reliably pick up
100# changes to the build config.
101# This step also generates a large number of files, so we create a dummy file
102# .cmake_done to represent overall completion for make's dependency tracking.
103${KERNEL_BUILD_ROOT}/.cmake_done: ${KERNEL_DEPS} ${CONFIG_DOMAIN_SCHEDULE}
104	rm -rf ${KERNEL_BUILD_ROOT}
105	mkdir -p ${KERNEL_BUILD_ROOT}
106	cd ${KERNEL_BUILD_ROOT} && \
107	cmake -C ${CONFIG} \
108		-DCROSS_COMPILER_PREFIX=${TOOLPREFIX} \
109		-DCMAKE_TOOLCHAIN_FILE=${SOURCE_ROOT}/gcc.cmake \
110		-DKernelDomainSchedule=${CONFIG_DOMAIN_SCHEDULE} \
111		-DUMM_TYPES=$(abspath ${UMM_TYPES}) \
112		-DCSPEC_DIR=${CSPEC_DIR} ${KERNEL_CMAKE_EXTRA_OPTIONS} \
113		-G Ninja ${SOURCE_ROOT}
114	touch ${KERNEL_BUILD_ROOT}/.cmake_done
115
116${UMM_TYPES}: ${KERNEL_BUILD_ROOT}/kernel_all.c_pp
117	${CSPEC_DIR}/mk_umm_types.py --root $(L4V_REPO_PATH) ${KERNEL_BUILD_ROOT}/kernel_all.c_pp $@
118