1# 2# Copyright 2014, General Dynamics C4 Systems 3# 4# This software may be distributed and modified according to the terms of 5# the GNU General Public License version 2. Note that NO WARRANTY is provided. 6# See "LICENSE_GPLv2.txt" for details. 7# 8# @TAG(GD_GPL) 9# 10 11SHELL=bash 12SEL4_VERSION=../../seL4/VERSION 13 14# default to primary verification platform 15L4V_ARCH?=ARM 16 17## Targets 18images: ASpec CKernel 19default: images test 20all: images test 21report-regression: 22 @echo ASpec ExecSpec DSpec TakeGrant CKernel CSpec \ 23 binary-verification-input 24 25# 26# Setup heaps. 27# 28 29# Spec heaps. 30HEAPS += ASpec ASpecDoc ExecSpec DSpec CKernel CSpec TakeGrant ASepSpec 31 32# Additional dependencies 33 34CKernel CSpec: c-kernel design-spec 35 36# NOTE: The abstract spec imports Events from Haskell hence the dependency 37 38ASpec ExecSpec DSpec : design-spec 39 40ASPEC_DOC_GITREV_FILE=abstract/document/gitrev.tex 41ASPEC_DOC_VERSION_FILE=abstract/document/VERSION 42 43ASpecDoc: design-spec $(ASPEC_DOC_VERSION_FILE) $(ASPEC_DOC_GITREV_FILE) 44 45$(ASPEC_DOC_VERSION_FILE): $(SEL4_VERSION) 46 cp $< $@ 47 48$(ASPEC_DOC_GITREV_FILE): .FORCE 49 git rev-parse --short=15 HEAD > $@ || echo unknown > $@ 50 git diff --no-ext-diff --quiet || echo "*" >> $@ 51 git diff --no-ext-diff --quiet --cached || echo "+" >> $@ 52 perl -p -i -e "s/\n//" $@ 53 54# NOTE: the install_C_file in Kernel_C.thy invocation generates a spurious 55# umm_types.txt file in this folder. This file is never used nor 56# depended on. 57 58# Preprocess the kernel's source code and bitfield theory files. 59c-kernel: c-parser .FORCE 60 cd cspec/c && L4V_REPO_PATH=$(L4V_REPO_PATH) L4V_ARCH=$(L4V_ARCH) $(MAKE) cspec 61.PHONY: c-kernel 62 63# Run the haskell translator 64design-spec: .FORCE 65 cd design/ && L4V_REPO_PATH=$(L4V_REPO_PATH) $(MAKE) design 66.PHONY: design-spec 67 68# Sets up the c-parser grammar files 69c-parser: .FORCE 70 cd ../tools/c-parser && make c-parser-deps 71.PHONY: c-parser 72 73# Produce the input data for the binary verification problem at -O1 74binary-verification-input: c-kernel 75 $(ISABELLE_TOOL) build -d .. -v SimplExport 76 echo 'Built CFunDump.txt, md5sums of relevance are:' 77 md5sum cspec/CFunDump.txt cspec/c/kernel_all.c_pp 78 79# Clean 80clean: 81 rm -rf abstract/generated 82 cd cspec/c && L4V_ARCH=$(L4V_ARCH) $(MAKE) clean SKIP_PATH_CHECKS=1 83 rm -f umm_types.txt 84.PHONY: clean 85 86include ../misc/isa-common.mk 87