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