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