1# 2# Copyright 2016, NICTA 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(NICTA_GPL) 9# 10 11MODULE=cgbilbyfs 12 13ROOT_DIR=../../../../ 14 15ifeq ($(KERNELRELEASE),) 16# this include won't make sense inside the kernel tree 17include $(ROOT_DIR)build-env.mk 18endif 19 20OUTPUT=bilbyfs 21SRC=src/fsop.cogent 22DEFNS=data/defns.txt 23PROOF_ID=BilbyFs 24 25# GCC version 26GCCVER=$(shell gcc -dumpversion) 27 28# Standard Gum Directory 29LIBGUM=$(COGENT_LIBGUM_DIR) 30ifeq ($(LIBGUM),) 31LIBGUM=$(shell cogent --libgum-dir) 32endif 33# ADT headers required by BilbyFs 34AHFILES=$(wildcard $(LIBGUM)/gum/anti/abstract/*.ah) 35# ADT C files required by BilbyFs 36LINUX_ACFILES=plat/linux/wrapper.ac 37# ADT C files required by verification 38VERIF_ACFILES=plat/verification/wrapper.ac 39LINUX_TYPES=plat/linux/data/types.txt 40VERIF_TYPES=plat/verification/data/types.txt 41 42ifndef KERNELDIR 43KERNELDIR:= /lib/modules/$(shell uname -r)/build 44endif 45 46ifeq ($(KERNELRELEASE),) 47PWD:= $(shell pwd) 48endif 49ifneq ($(DEBUG),) 50EXTRA_CFLAGS+= -DBILBYFS_DEBUG 51COGENT_FLAGS+= --cogent-pp-args=-DDEBUG=1 52endif 53 54# flags to ignores COGENT's compiler messy C code gen 55COMMON_CFLAGS := -O2 -Wno-parentheses -Wno-declaration-after-statement -Wno-unused-variable -Wno-uninitialized 56LINUX_EXTRA_CFLAGS := -I$(PWD)/plat/linux/ -I$(PWD) -I$(PWD)/src -I$(PWD)/lib -I$(PWD)/abstract $(COMMON_CFLAGS) -I$(LIBGUM) 57VERIF_EXTRA_CFLAGS := -I$(PWD)/plat/verification/ -I$(PWD) -I$(PWD)/src -I$(PWD)/lib -I$(PWD)/abstract -I$(LIBGUM) $(COMMON_CFLAGS) 58 59# COGENT flags 60COGENT_FLAGS+= -Od --fno-static-inline --fno-fncall-as-macro --fnormalisation=knf --ffunc-purity-attr 61# end of configuration 62 63override COGENT_FLAGS+= -o$(OUTPUT) \ 64 --root-dir=$(ROOT_DIR) \ 65 --entry-funcs=$(DEFNS) \ 66 --infer-c-types="$(AHFILES)" \ 67 --abs-type-dir=$(PWD) 68 69COUTPUT=$(addsuffix .c, $(OUTPUT)) 70HOUTPUT=$(addsuffix .h, $(OUTPUT)) 71NAME=$(MODULE) 72RTMPC=$(ACFILES:.ac=_pp_inferred.c) 73RTMPPPC=$(COUTPUT) $(ACFILES:.ac=_pp.ac) 74 75BUILDSRC=$(wildcard build/*.c) 76# Add C files with no antiquotation to OBJ. 77# Writing these functions in a .ac file would lead defining multiple 78# times the same symbol when parametric polymorphism gets expanded. 79OBJ?=plat/linux/module.o plat/linux/rbt.o 80 81 82########################### 83# TARGET-SPECIFIC VARIABLES 84########################### 85# ACFILES 86linux: ACFILES = $(LINUX_ACFILES) 87.c-gen: ACFILES = $(LINUX_ACFILES) 88hs: ACFILES = $(LINUX_ACFILES) 89verification: ACFILES = $(VERIF_ACFILES) 90.verif-gen: ACFILES = $(VERIF_ACFILES) 91# DISTDIR 92linux: DIST_DIR = plat/linux 93.c-gen: DIST_DIR = plat/linux 94hs: DIST_DIR = plat/linux 95verification: DIST_DIR = plat/verification 96.verif-gen: DIST_DIR = plat/verification 97# EXTRA_CFLAGS 98linux: EXTRA_CFLAGS = $(LINUX_EXTRA_CFLAGS) 99.c-gen: EXTRA_CFLAGS = $(LINUX_EXTRA_CFLAGS) 100hs: EXTRA_CFLAGS = $(LINUX_EXTRA_CFLAGS) 101verification: EXTRA_CFLAGS = $(VERIF_EXTRA_CFLAGS) 102.verif-gen: EXTRA_CFLAGS = $(VERIF_EXTRA_CFLAGS) 103 104 105# call from kernel build system 106ifneq ($(KERNELRELEASE),) 107 ccflags-y+=-I/usr/lib/gcc/x86_64-pc-linux-gnu/$(GCCVER)/include 108 obj-m+= $(MODULE).o 109 $(MODULE)-objs := $(OBJ) 110else 111 112PWD:= $(shell pwd) 113 114.PHONY: default cogent clean .c-gen .verif-gen verification 115 116 117default: linux 118 119all: .c-gen $(OBJ) 120 $(Q)$(CC) -o $(NAME) $(OBJ) 121 122%.c: 123 $(Q)$(CC) -c $@ 124 125# generate executable C code 126# NOTE: We run cpp with in c99 mode, as the default mode that cpp runs in is gnu99, 127# which has an issue when parsing. It replaces anything 'linux' with a '1'. 128# More details here: http://stackoverflow.com/questions/19210935/why-does-the-c-preprocessor-interpret-the-word-linux-as-the-constant-1 129# So we use c99 mode here and when building the generated C code(make modules), we 130# use `gnu99` mode. 131.c-gen: 132 $(Q)cogent $(SRC) -g $(COGENT_FLAGS) \ 133 --cpp-args="-std=c99 \$$CPPIN -o \$$CPPOUT -E -P $(EXTRA_CFLAGS)" \ 134 --dist-dir=$(DIST_DIR) \ 135 --infer-c-funcs="$(ACFILES)" \ 136 --ext-types="$(LINUX_TYPES)" 137 138hs: 139 $(Q)cogent $(SRC) --hs-shallow-desugar-tuples $(COGENT_FLAGS) \ 140 --cpp-args="-std=c99 \$$CPPIN -o \$$CPPOUT -E -P $(EXTRA_CFLAGS)" \ 141 --proof-name=$(PROOF_ID) \ 142 --dist-dir=$(DIST_DIR) \ 143 --infer-c-funcs="$(ACFILES)" \ 144 --ext-types="$(LINUX_TYPES)" 145 146 147.verif-gen: 148 $(Q)cogent $(SRC) -A $(COGENT_FLAGS) \ 149 --cpp-args="-std=c99 \$$CPPIN -o \$$CPPOUT -E -P $(EXTRA_CFLAGS)" \ 150 --dist-dir=$(DIST_DIR) \ 151 --infer-c-funcs="$(ACFILES)" \ 152 --ext-types="$(VERIF_TYPES)" \ 153 --proof-name=$(PROOF_ID) \ 154 --proof-input-c="wrapper_pp_inferred.c" 155 156 157# compile Linux kernel module for file system 158linux: .c-gen 159 $(Q)$(MAKE) OBJ="$(OBJ)" CFLAGS="$(CFLAGS)" EXTRA_CFLAGS="-std=gnu99 $(EXTRA_CFLAGS)" -C $(KERNELDIR) M=$(PWD) modules 160 161# generate verification-clean C code and proof scripts 162verification: .verif-gen 163 $(Q)mv $(DIST_DIR)/$(OUTPUT).table $(DIST_DIR)/wrapper_pp_inferred.table 164 165typeproof: 166 sed -i -e 's/^session BilbyFs_TypeProof = BilbyFs_ACInstall +$$/session BilbyFs_TypeProof = "HOL-Word" +/' plat/verification/ROOT 167 $(Q)isabelle build -d $(AC_DIR) -d ../../../../cogent/isa -d plat/verification -c -v BilbyFs_TypeProof 168 169corresproof: 170 sed -i -e 's/^session BilbyFs_CorresProof = BilbyFs_CorresSetup +$$/session BilbyFs_CorresProof = AutoCorres +/' plat/verification/ROOT 171 $(Q)isabelle build -d $(AC_DIR) -d ../../../../cogent/isa -d plat/verification -v BilbyFs_CorresProof 172 173allrefine: 174 sed -i -e 's/^session BilbyFs_AllRefine = BilbyFs_CorresProof +$$/session BilbyFs_AllRefine = AutoCorres +/' plat/verification/ROOT 175 $(Q)isabelle build -d $(AC_DIR) -d ../../../../cogent/isa -d plat/verification -v BilbyFs_AllRefine 176 177shallownormal: 178 echo 'session BilbyFs_Shallow_Normal = AutoCorres +' >> plat/verification/ROOT 179 echo ' theories [quick_and_dirty] "BilbyFs_Shallow_Normal"' >> plat/verification/ROOT 180 $(Q)isabelle build -d $(AC_DIR) -d ../../../../cogent/isa -d plat/verification -v BilbyFs_Shallow_Normal 181 182clean: 183 $(E) "Cleaning up.." 184 $(Q)rm -f $(HOUTPUT) 185 $(Q)rm -f $(OBJ) 186 $(Q)rm -f $(RTMPC) 187 $(Q)rm -f $(RTMPPPC) 188 $(Q)rm -f $(MODULE).mod.[co] $(MODULE).o $(MODULE).ko Module.symvers modules.order 189 $(Q)rm -f abstract/*.h 190 $(Q)rm -rf *.thy ROOT $(OUTPUT).table BUILD_INFO 191 $(Q)find . -name *.thy -exec rm -f {} \; 192 $(Q)find . -name ROOT -exec rm -f {} \; 193 $(Q)find . -name BUILD_INFO -exec rm -f {} \; 194 $(Q)find . -name *_pp* -exec rm -f {} \; 195 $(Q)find . -name $(OUTPUT).[ch] -exec rm -f {} \; 196 $(Q)find . -name *.cmd -exec rm -f {} \; 197 198help: 199 $(E) "** Cogent bilbyfs build help **" 200 $(E) "Run 'make' to build the Linux bilbyfs kernel module." 201 $(E) "" 202 $(E) "Please run 'make <target>' where target is one of the following:" 203 $(E) "* linux" 204 $(E) " Build the Linux kernel module(default)." 205 $(E) " This will build against the kernel headers of the current running kernel." 206 $(E) " Pass KERNELDIR=<path-to-kernel-headers> if you want to build against a different kernel version." 207 $(E) " eg.:" 208 $(E) " make linux" 209 $(E) " make linux KERNELDIR=/usr/src/linux-headers-4.3.0-1-amd64/" 210 $(E) "" 211 $(E) "* debug" 212 $(E) " Build the Linux kernel module with debugging enabled." 213 $(E) " This is equivalent to running 'make linux DEBUG=1'" 214 $(E) "" 215 $(E) "* verification" 216 $(E) " Generate verification table." 217 $(E) "" 218 $(E) "* clean" 219 $(E) " Cleanup." 220 $(E) "" 221 $(E) "* help" 222 $(E) " Print this help." 223 224endif 225