1#
2# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3#
4# SPDX-License-Identifier: BSD-2-Clause
5#
6
7# Makefile for building, decompiling & validating seL4.
8
9# n.b. doesn't track the dependencies of the custom tools
10# (e.g. standalone c-parser and decompiler) properly, so may not know to
11# rebuild if a custom tool is updated.
12
13ifndef CONFIG_OPTIMISATION_LEVEL
14  CONFIG_OPTIMISATION_LEVEL := -O1
15endif
16
17# FIXME: solver self-test is currently broken
18SKIP_SOLV_TEST := SKIP
19
20ifndef GREF_ROOT
21  GREF_ROOT := $(realpath $(dir $(lastword ${MAKEFILE_LIST}))..)
22endif
23
24ifndef HOL4_ROOT
25  HOL4_ROOT := $(realpath ${GREF_ROOT}/../HOL4)
26endif
27
28L4V_CONFIG := ${L4V_ARCH}$(if ${L4V_FEATURES},-${L4V_FEATURES},)
29TARGET_NAME := ${L4V_CONFIG}${CONFIG_OPTIMISATION_LEVEL}
30TARGET_DIR := target/${TARGET_NAME}
31
32# We build our own kernel locally, so we can store builds
33# according to their optimisation levels.
34KERNEL_BUILD_ROOT := ${TARGET_DIR}/build
35KERNEL_CMAKE_EXTRA_OPTIONS := -DKernelOptimisation=${CONFIG_OPTIMISATION_LEVEL}
36include ${GREF_ROOT}/../l4v/spec/cspec/c/kernel.mk
37
38# However, CFunctions.txt depends on l4v's kernel build.
39# FIXME: the l4v build directory should really depend on L4V_FEATURES.
40L4V_KERNEL_BUILD_DIR := build/${L4V_ARCH}
41L4V_KERNEL_BUILD_PATH := ${CSPEC_DIR}/c/${L4V_KERNEL_BUILD_DIR}
42
43DECOMP_DIR := ${HOL4_ROOT}/examples/machine-code/graph
44DECOMP_SCRIPT := $(shell PATH="${DECOMP_DIR}:${PATH}" sh -c "which decompile.py")
45
46# sanity test configuration
47
48$(if ${DECOMP_SCRIPT},,$(error decompile.py not executable in ${DECOMP_DIR}))
49
50$(if $(wildcard ${HOL4_ROOT}/bin/Holmake ${HOL4_ROOT}/bin/build),, \
51  $(error Holmake/build not found in ${HOL4_ROOT}/bin - first configure HOL4. \
52  See INSTALL in HOL4, but skip the bin/build step))
53
54SOLV=python ${GREF_ROOT}/solver.py
55
56SOLV_TEST_SUCC := 'Solver self-test succ'
57SOLV_TEST := $(shell $(if ${SKIP_SOLV_TEST}, echo ${SOLV_TEST_SUCC}, \
58    ${SOLV} testq) | grep ${SOLV_TEST_SUCC})
59$(if ${SOLV_TEST},,$(error Solver self-test failed (${SOLV} test)))
60
61# compile and decompile
62
63${TARGET_DIR}/summary.txt: ${TARGET_DIR}/kernel_all.c_pp
64	echo Summary > pre_summary.txt
65	bash mk_summ ${SOURCE_ROOT} >> pre_summary.txt
66	bash mk_summ ${L4V_REPO_PATH} >> pre_summary.txt
67	bash mk_summ ${HOL4_ROOT} >> pre_summary.txt
68	bash mk_summ . >> pre_summary.txt
69	mv pre_summary.txt summary.txt
70
71KERNEL_FILES := kernel.elf.rodata kernel.elf.txt kernel.elf.symtab kernel_all.c_pp kernel.sigs kernel.elf
72TARGET_FILES := target.py CFunctions.txt ASMFunctions.txt
73
74KERNEL_PATHS := $(patsubst %, $(TARGET_DIR)/%, $(KERNEL_FILES))
75TARGET_PATHS := $(patsubst %, $(TARGET_DIR)/%, $(TARGET_FILES))
76
77KERNEL_TGZ := ${TARGET_DIR}/kernel.tar.gz
78TARGET_TGZ := ${TARGET_DIR}/target.tar.gz
79
80${KERNEL_TGZ}: ${KERNEL_PATHS}
81	tar -czf $@ -C ${TARGET_DIR} ${KERNEL_FILES}
82
83${TARGET_TGZ}: ${KERNEL_PATHS} ${TARGET_PATHS}
84	tar -czf $@ -C ${TARGET_DIR} ${KERNEL_FILES} ${TARGET_FILES}
85
86tar: ${KERNEL_TGZ} ${TARGET_TGZ}
87
88${KERNEL_PATHS}: ${TARGET_DIR}/%: ${KERNEL_BUILD_ROOT}/%
89	@mkdir -p ${TARGET_DIR}
90	cp $< $@
91
92clean:
93	rm -rf build kernel.elf.* kernel_all* kernel.tar*
94
95.PHONY: clean tar
96
97H4PATH := $(realpath ${HOL4_ROOT}/bin):${PATH}
98
99IGNORES_ARM := restore_user_context,c_handle_fastpath_call,c_handle_fastpath_reply_recv
100IGNORES_RISCV64 := # TODO
101
102KERNEL_ALL_PP_FILES := ${L4V_KERNEL_BUILD_PATH}/kernel_all.c_pp ${KERNEL_BUILD_ROOT}/kernel_all.c_pp
103
104# FIXME: This should be a prerequisite of some other essential target,
105#        but for convenience during development, it is currently not.
106${TARGET_DIR}/.diff: ${KERNEL_ALL_PP_FILES}
107	diff -q --ignore-matching-lines='^#' ${KERNEL_ALL_PP_FILES}
108	@mkdir -p ${TARGET_DIR}
109	@touch $@
110
111diff: ${TARGET_DIR}/.diff
112.PHONY: diff
113
114${L4V_KERNEL_BUILD_PATH}/kernel_all.c_pp: ${KERNEL_DEPS} ${CONFIG_DOMAIN_SCHEDULE}
115	MAKEFILES= make -C ${CSPEC_DIR}/c ${L4V_KERNEL_BUILD_DIR}/kernel_all.c_pp
116
117${TARGET_DIR}/ASMFunctions.txt: ${TARGET_DIR}/kernel.elf.txt ${TARGET_DIR}/kernel.sigs
118	cd ${TARGET_DIR} && PATH=${H4PATH} ${DECOMP_SCRIPT} --fast ./kernel --ignore=${IGNORES_${L4V_CONFIG}}
119	mv ${TARGET_DIR}/kernel_mc_graph.txt ${TARGET_DIR}/ASMFunctions.txt
120
121${TARGET_DIR}/CFunctions.txt: ${L4V_KERNEL_BUILD_PATH}/kernel_all.c_pp ${L4V_REPO_PATH}/tools/asmrefine/*.thy
122	@mkdir -p ${TARGET_DIR}
123	MAKEFILES= make -C ${L4V_REPO_PATH}/proof/ SimplExport
124	# FIXME: the following path should really depend on L4V_FEATURES.
125	cp ${L4V_REPO_PATH}/proof/asmrefine/export/${L4V_ARCH}/CFunDump.txt $@
126
127${TARGET_DIR}/target.py: target.py
128	@mkdir -p ${TARGET_DIR}
129	cp target.py $@
130
131GRAPH_REFINE_INPUTS := \
132  ${TARGET_DIR}/kernel.elf.rodata \
133  ${TARGET_DIR}/kernel.elf.symtab \
134  ${TARGET_DIR}/ASMFunctions.txt \
135  ${TARGET_DIR}/CFunctions.txt \
136  ${TARGET_DIR}/target.py \
137  ${GREF_ROOT}/*.py
138
139GRAPH_REFINE := python ${GREF_ROOT}/graph-refine.py
140
141${TARGET_DIR}/StackBounds.txt: ${GRAPH_REFINE_INPUTS}
142	${GRAPH_REFINE} ${TARGET_DIR}
143
144${TARGET_DIR}/demo-report.txt: ${TARGET_DIR}/StackBounds.txt ${GRAPH_REFINE_INPUTS}
145	${GRAPH_REFINE} ${TARGET_DIR} trace-to:$@.partial deps:Kernel_C.cancelAllIPC
146	mv $@.partial $@
147
148${TARGET_DIR}/report.txt: ${TARGET_DIR}/StackBounds.txt ${GRAPH_REFINE_INPUTS}
149	${GRAPH_REFINE} ${TARGET_DIR} trace-to:$@.partial all
150	mv $@.partial $@
151
152${TARGET_DIR}/coverage.txt: ${TARGET_DIR}/StackBounds.txt ${GRAPH_REFINE_INPUTS}
153	${GRAPH_REFINE} ${TARGET_DIR} trace-to:$@.partial coverage
154	mv $@.partial $@
155
156report: ${TARGET_DIR}/report.txt
157coverage: ${TARGET_DIR}/coverage.txt
158StackBounds: ${TARGET_DIR}/StackBounds.txt
159
160.PHONY: report coverage StackBounds
161
162default: report
163
164.PHONY: .FORCE
165.FORCE:
166
167# WCET (worst-case execution time) targets
168
169GTG := ${GREF_ROOT}/graph-to-graph/
170TARGET_DIR_ABS := $(realpath TARGET_DIR)
171
172${TARGET_DIR}/loop_counts_1.py: ${TARGET_DIR}/StackBounds.txt ${GRAPH_REFINE_INPUTS}
173	cd ${GTG} && python graph_to_graph.py ${TARGET_DIR_ABS} handleSyscall --l
174	cp ${TARGET_DIR}/loop_counts.py $@
175
176${TARGET_DIR}/lb_reports/report_%.txt: ${TARGET_DIR}/loop_counts_1.py
177	@mkdir -p ${TARGET_DIR}/lb_reports
178	cd ${GTG} && python convert_loop_bounds.py --worker-id $* ${TARGET_DIR_ABS} &> ${TARGET_DIR_ABS}/lb_reports/pre-report_$*.txt
179	tail -n 500 ${TARGET_DIR}/lb_reports/pre-report_$*.txt > $@
180	rm ${TARGET_DIR}/lb_reports/pre-report_$*.txt
181
182ALL_LB_REPORTS := $(patsubst %, ${TARGET_DIR}/lb_reports/report_%.txt, 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 )
183
184${TARGET_DIR}/lb_reports/fin_report.txt: ${ALL_LB_REPORTS}
185	cd ${GTG} && python convert_loop_bounds.py $* ${TARGET_DIR_ABS} &> ${TARGET_DIR_ABS}/lb_reports/pre-freport.txt
186	mv ${TARGET_DIR}/lb_reports/pre-freport.txt $@
187
188lb: ${TARGET_DIR}/lb_reports/fin_report.txt
189