1# * Copyright 2015, NICTA
2# *
3# * This software may be distributed and modified according to the terms of
4# * the BSD 2-Clause license. Note that NO WARRANTY is provided.
5# * See "LICENSE_BSD2.txt" for details.
6# *
7# * @TAG(NICTA_BSD)
8
9# makefile for building, decompiling & validating seL4.
10
11# n.b. doesn't track the dependencies of the custom tools
12# (e.g. standalone c-parser and decompiler) properly, so may not know to
13# rebuild if a custom tool is updated.
14
15# necessary configuration
16
17SOURCE_ROOT?=../../seL4
18
19L4V_ROOT?=../../l4v
20L4V_ARCH?=ARM
21PARSERPATH?=${L4V_ROOT}/tools/c-parser/standalone-parser
22CSPEC_PATH?=${L4V_ROOT}/spec/cspec/c
23
24HOL4_ROOT?=../../HOL4
25DECOMP_DIR?=${HOL4_ROOT}/examples/machine-code/graph
26
27GREF_ROOT?=..
28
29OBJDUMP?=${TOOLPREFIX}objdump
30
31# derived configuration
32
33TOOLPREFIX?=$(shell bash ${GREF_ROOT}/seL4-example/get_tool_prefix.sh)
34$(if ${TOOLPREFIX},,$(error failed to pick a toolset))
35
36CSPEC_BUILD_PREFIX=build/${L4V_ARCH}
37CSPEC_BUILD_PATH=${CSPEC_PATH}/${CSPEC_BUILD_PREFIX}
38CONFIG=${L4V_ARCH}_verified.cmake
39CONFIG_DOMAIN_SCHEDULE=${CSPEC_PATH}/config_sched.c
40
41# sanity test configuration
42
43OBJDUMP_PATH = $(shell which ${OBJDUMP})
44$(if ${OBJDUMP_PATH},,$(error objdump ${OBJDUMP} not executable))
45
46DECOMP_SCRIPT= $(shell PATH="${DECOMP_DIR}:${PATH}" sh -c "which decompile.py")
47$(if ${DECOMP_SCRIPT},,$(error decompile.py not executable in ${DECOMP_DIR}))
48
49$(if $(wildcard ${HOL4_ROOT}/bin/Holmake ${HOL4_ROOT}/bin/build),, \
50  $(error Holmake/build not found in ${HOL4_ROOT}/bin - first configure HOL4. \
51  See INSTALL in HOL4, but skip the bin/build step))
52
53SOLV=python ${GREF_ROOT}/solver.py
54
55SOLV_TEST_SUCC='Solver self-test succ'
56SOLV_TEST = $(shell $(if ${SKIP_SOLV_TEST}, echo ${SOLV_TEST_SUCC}, \
57    ${SOLV} testq) | grep ${SOLV_TEST_SUCC})
58$(if ${SOLV_TEST},,$(error Solver self-test failed (${SOLV} test)))
59
60# compile and decompile
61
62KERNEL_DEPS = $(shell find ${SOURCE_ROOT} -type f)
63
64${CSPEC_BUILD_PATH}/kernel_all.c_pp: ${KERNEL_DEPS} ${CONFIG_DOMAIN_SCHEDULE}
65	# have the l4v build system build its kernel source
66	cd ${CSPEC_PATH} && L4V_ARCH=${L4V_ARCH} make c-kernel-source
67
68kernel_all.c_pp: build/.cmake_done
69	cd build && ninja kernel_all_pp_wrapper
70	cp -a build/kernel_all_pp.c $@
71
72kernel.elf: build/.cmake_done kernel_all.c_pp
73	cd build && ninja kernel.elf
74	cp -a build/kernel.elf $@
75
76ABS_SOURCE_ROOT=$(realpath ${SOURCE_ROOT})
77
78build/.cmake_done: ${KERNEL_DEPS} ${CONFIG_DOMAIN_SCHEDULE}
79	# hack borrowed from l4v, create a new build dir each time
80	rm -rf build
81	mkdir -p build
82	cd build && cmake -DCROSS_COMPILER_PREFIX=${TOOLPREFIX} \
83		-DCMAKE_TOOLCHAIN_FILE=${ABS_SOURCE_ROOT}/gcc.cmake -C ${ABS_SOURCE_ROOT}/configs/${CONFIG} \
84		-DKernelDomainSchedule=$(realpath ${CONFIG_DOMAIN_SCHEDULE}) \
85		-G Ninja ${ABS_SOURCE_ROOT} \
86		-DKernelOptimisation=${CONFIG_OPTIMISATION_LEVEL}
87	touch build/.cmake_done
88
89kernel.elf.rodata: kernel.elf
90	${OBJDUMP} -z -D $^ > $@
91
92kernel.elf.txt: kernel.elf
93	${OBJDUMP} -dz $^ > $@
94
95kernel.elf.symtab: kernel.elf
96	${OBJDUMP} -t $^ > $@
97
98kernel.sigs: kernel_all.c_pp
99	MAKEFILES= make -C ${PARSERPATH} standalone-cparser
100	${PARSERPATH}/c-parser ${L4V_ARCH} --underscore_idents --mmbytes $^ > $@.tmp
101	mv $@.tmp $@
102
103summary.txt: kernel_all.c_pp 
104	echo Summary > pre_summary.txt
105	bash mk_summ ${SOURCE_ROOT} >> pre_summary.txt
106	bash mk_summ ${L4V_ROOT} >> pre_summary.txt
107	bash mk_summ ${HOL4_ROOT} >> pre_summary.txt
108	bash mk_summ . >> pre_summary.txt
109	mv pre_summary.txt summary.txt
110
111KERNEL_FILES= kernel.elf.rodata kernel.elf.txt kernel.elf.symtab \
112  kernel_all.c_pp kernel.sigs kernel.elf
113
114kernel.tar.gz: ${KERNEL_FILES}
115	tar -cvzf $@ $^
116
117target.tar.gz: ${KERNEL_FILES} target.py CFunctions.txt ASMFunctions.txt
118	tar -cvzf $@ $^
119
120tar: kernel.tar.gz
121
122clean:
123	rm -rf build kernel.elf.* kernel_all* kernel.tar*
124
125.PHONY: clean
126
127H4PATH=$(realpath ${HOL4_ROOT}/bin):${PATH}
128
129IGNORES= fastpath_restore,slowpath,fastpath_call,fastpath_reply_recv,restore_user_context,lockTLBEntry,lockTLBEntryCritical
130
131ASMFunctions.txt: kernel.elf.txt kernel.sigs
132	PATH=${H4PATH} ${DECOMP_SCRIPT} --fast ./kernel --ignore=${IGNORES}
133	# we move the output to a new location to get around a problem where
134	# the decompiler can fail leaving an incomplete output file.
135	mv kernel_mc_graph.txt ASMFunctions.txt
136
137KERNEL_ALL_FILES= kernel_all.c_pp ${CSPEC_BUILD_PATH}/kernel_all.c_pp
138
139CFunctions.txt: $(KERNEL_ALL_FILES) ${L4V_ROOT}/tools/asmrefine/*.thy
140	# it's important that the parser and compiler see the same source
141	diff -qs --ignore-matching-lines='^#' ${KERNEL_ALL_FILES}
142	MAKEFILES= make -C ${L4V_ROOT}/proof/ SimplExportOnly
143	cp ${L4V_ROOT}/proof/asmrefine/CFunDump.txt CFunctions.txt
144
145GRAPH_REFINE_INPUTS= kernel.elf.rodata kernel.elf.symtab ASMFunctions.txt \
146                CFunctions.txt target.py ${GREF_ROOT}/*.py
147
148GRAPH_REFINE=python ${GREF_ROOT}/graph-refine.py
149
150StackBounds.txt: ${GRAPH_REFINE_INPUTS}
151	${GRAPH_REFINE} .
152
153demo-report.txt: StackBounds.txt ${GRAPH_REFINE_INPUTS}
154	${GRAPH_REFINE} . trace-to:partial-$@ deps:Kernel_C.cancelAllIPC
155	mv partial-$@ $@
156
157report.txt: StackBounds.txt ${GRAPH_REFINE_INPUTS}
158	${GRAPH_REFINE} . trace-to:partial-$@ all
159	mv partial-$@ $@
160
161default: report.txt
162
163.PHONY: .FORCE
164.FORCE:
165
166# WCET (worst-case execution time) targets
167
168GTG=${GREF_ROOT}/graph-to-graph/
169HERE=$(shell pwd)
170
171loop_counts_1.py: StackBounds.txt ${GRAPH_REFINE_INPUTS}
172	cd ${GTG} ; python graph_to_graph.py ${HERE} handleSyscall --l
173	cp loop_counts.py $@
174
175lb_reports/report_%.txt : loop_counts_1.py
176	mkdir -p lb_reports
177	cd ${GTG} ; python convert_loop_bounds.py --worker-id $* ${HERE} &> ${HERE}/lb_reports/pre-report_$*.txt
178	tail -n 500 lb_reports/pre-report_$*.txt > $@
179	rm lb_reports/pre-report_$*.txt
180
181ALL_LB_REPORTS=$(patsubst %, 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 )
182
183lb_reports/fin_report.txt : ${ALL_LB_REPORTS}
184	cd ${GTG} ; python convert_loop_bounds.py $* ${HERE} &> ${HERE}/lb_reports/pre-freport.txt
185	mv lb_reports/pre-freport.txt $@
186
187lb: lb_reports/fin_report.txt
188
189