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=cgext2fs 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=ext2 21SRC=src/super.cogent 22TYPES=data/types.txt 23DEFNS=data/defns.txt 24PROOF_ID=Ext2 25 26# GCC version 27GCCVER:=$(shell gcc -dumpversion) 28# Standard Gum Directory 29LIBGUM:=$(COGENT_LIBGUM_DIR) 30ifeq ($(LIBGUM),) 31LIBGUM:=$(shell cogent --libgum-dir) 32endif 33 34COGENT_SOURCES := $(addprefix src/,\ 35 balloc.cogent bchain.cogent \ 36 dcommon.cogent debug.cogent \ 37 dread.cogent dwrite.cogent \ 38 ext2.cogent groupdesc.cogent \ 39 ialloc.cogent indirect.cogent \ 40 iread.cogent iwrite.cogent \ 41 path.cogent super.cogent \ 42 test.cogent util.cogent) 43C_SOURCES := $(addprefix plat/linux/, \ 44 adt.h \ 45 alloc.ac \ 46 inode.ac \ 47 module.c \ 48 vfs.ac \ 49 wrapper.h) 50 51# ADT headers required by Ext2fs 52AHFILES=$(wildcard $(LIBGUM)/gum/anti/abstract/*.ah) 53# ADT C files required by Ext2fs 54LINUX_ACFILES=$(addprefix $(LIBGUM)/gum/anti/, \ 55 common.ac \ 56 wordarray.ac \ 57 uarray.ac \ 58 array.ac \ 59 os.ac \ 60 ospage.ac \ 61 osbuffer.ac \ 62 iterator.ac \ 63 log.ac \ 64 dls.ac) \ 65 plat/linux/wrapper.ac 66 67COGENT_GUM := $(wildcard $(LIBGUM)/gum/*/*.cogent $(LIBGUM)/gum/kernel/linux/*.cogent) 68 69# ADT C files required by verification 70VERIF_ACFILES=plat/verification/wrapper.ac 71 72ifndef KERNELDIR 73KERNELDIR:= /lib/modules/$(shell uname -r)/build 74endif 75 76ifeq ($(KERNELRELEASE),) 77PWD:= $(shell pwd) 78endif 79 80ifneq ($(DEBUG),) 81EXTRA_CFLAGS+= -DEXT2FS_DEBUG 82# COGENT_FLAGS+= --debug 83endif 84 85# flags to ignores COGENT's compiler messy C code gen 86EXTRA_CFLAGS += -O2 -Wno-parentheses -Wno-declaration-after-statement -Wno-unused-variable -Wno-uninitialized 87 88CPPFLAGS.common := -I$(PWD) -I$(PWD)/src -I$(PWD)/lib -I$(PWD)/abstract -I$(LIBGUM) 89CPPFLAGS.linux := -I$(PWD)/plat/linux/ 90CPPFLAGS.verif := -I$(PWD)/plat/verification/ -DVERIFICATION 91 92# COGENT flags 93COGENT_FLAGS+= -Od --fno-static-inline --fno-fncall-as-macro \ 94 --ffunc-purity-attr --fno-pretty-errmsgs 95# end of configuration 96 97override COGENT_FLAGS+= -o$(OUTPUT) \ 98 --root-dir=$(ROOT_DIR) \ 99 --entry-funcs=$(DEFNS) \ 100 --ext-types=$(TYPES) \ 101 --infer-c-types="$(AHFILES)" \ 102 --abs-type-dir=$(PWD) \ 103 --cpp-args="-std=c99 \$$CPPIN -o \$$CPPOUT -E -P ${CFLAGS} ${EXTRA_CFLAGS} ${CPPFLAGS}" \ 104 --cogent-pp-args="${CPPFLAGS}" 105 106COUTPUT=$(addsuffix .c, $(OUTPUT)) 107HOUTPUT=$(addsuffix .h, $(OUTPUT)) 108NAME=$(MODULE) 109RTMPC=$(ACFILES:.ac=_pp_inferred.c) 110RTMPPPC=$(COUTPUT) $(ACFILES:.ac=_pp.ac) 111 112BUILDSRC=$(wildcard build/*.c) 113 114# Add C files with no antiquotation to OBJ. 115# Writing these functions in a .ac file would lead defining multiple 116# times the same symbol when parametric polymorphism gets expanded. 117# NOTE: A module.o is relevant only for the linux platform 118OBJ?=plat/linux/module.o 119 120 121########################### 122# TARGET-SPECIFIC VARIABLES 123########################### 124# ACFILES 125linux: ACFILES = $(LINUX_ACFILES) 126.c-gen: ACFILES = $(LINUX_ACFILES) 127verification: ACFILES = $(VERIF_ACFILES) 128.verif-gen: ACFILES = $(VERIF_ACFILES) 129# DISTDIR 130linux: DIST_DIR = plat/linux 131.c-gen: DIST_DIR = plat/linux 132verification: DIST_DIR = plat/verification 133.verif-gen: DIST_DIR = plat/verification 134# CPPFLAGS 135linux .c-gen: CPPFLAGS = ${CPPFLAGS.common} ${CPPFLAGS.linux} 136verification .verif-gen: CPPFLAGS = ${CPPFLAGS.common} ${CPPFLAGS.verif} 137 138 139# call from kernel build system 140ifneq ($(KERNELRELEASE),) 141 ccflags-y+=-I/usr/lib/gcc/x86_64-pc-linux-gnu/$(GCCVER)/include 142 obj-m+= $(MODULE).o 143 $(MODULE)-objs := $(OBJ) 144else 145 146PWD:= $(shell pwd) 147 148.PHONY: default cogent clean .c-gen .verif-gen verification 149 150default: linux 151 152all: .c-gen $(OBJ) 153 $(Q)$(CC) -o $(NAME) $(OBJ) 154 155%.c: 156 $(Q)$(CC) -c $@ 157 158# generate executable C code 159# NOTE: We run cpp with in c99 mode, as the default mode that cpp runs in is gnu99, 160# which has an issue when parsing. It replaces anything 'linux' with a '1'. 161# More details here: http://stackoverflow.com/questions/19210935/why-does-the-c-preprocessor-interpret-the-word-linux-as-the-constant-1 162# So we use c99 mode here and when building the generated C code(make modules), we 163# use `gnu99` mode. 164.c-gen: ${COGENT_SOURCES} ${C_SOURCES} ${LINUX_ACFILES} ${COGENT_GUM} 165 $(Q)cogent $(SRC) -g $(COGENT_FLAGS) \ 166 --dist-dir=$(DIST_DIR) \ 167 --infer-c-funcs="$(ACFILES)" 168 $(Q)touch $@ 169 170.verif-gen: ${COGENT_SOURCES} ${C_SOURCES} ${LINUX_ACFILES} ${COGENT_GUM} 171 $(Q)cogent $(SRC) -A $(COGENT_FLAGS) \ 172 --dist-dir=$(DIST_DIR) \ 173 --infer-c-funcs="$(ACFILES)" \ 174 --proof-name=$(PROOF_ID) \ 175 --proof-input-c="wrapper_pp_inferred.c" 176 $(Q)touch $@ 177 178# compile Linux kernel module for file system 179linux: .c-gen 180 $(Q)$(MAKE) OBJ="$(OBJ)" CFLAGS="${CFLAGS}" EXTRA_CFLAGS="-std=gnu99 ${EXTRA_CFLAGS} ${CPPFLAGS}" -C $(KERNELDIR) M=$(PWD) modules 181 182# generate verification-clean C code and proof scripts 183verification: .verif-gen 184 $(Q)mv $(DIST_DIR)/$(OUTPUT).table $(DIST_DIR)/wrapper_pp_inferred.table 185 186 187clean: 188 $(E) "Cleaning up.." 189 $(Q)rm -f $(HOUTPUT) 190 $(Q)rm -f $(OBJ) 191 $(Q)rm -f $(RTMPC) 192 $(Q)rm -f $(RTMPPPC) 193 $(Q)rm -f $(MODULE).mod.[co] $(MODULE).o $(MODULE).ko Module.symvers modules.order 194 $(Q)rm -f abstract/*.h 195 $(Q)rm -rf *.thy ROOT $(OUTPUT).table BUILD_INFO 196 $(Q)find . -name *.thy -exec rm -f {} \; 197 $(Q)find . -name ROOT -exec rm -f {} \; 198 $(Q)find . -name BUILD_INFO -exec rm -f {} \; 199 $(Q)find . -name *_pp* -exec rm -f {} \; 200 $(Q)find . -name $(OUTPUT).[ch] -exec rm -f {} \; 201 $(Q)find . -name *.cmd -exec rm -f {} \; 202 203TAGS: $(COGENT_SOURCES) $(C_SOURCES) $(LINUX_ACFILES) $(COGENT_GUM) Makefile 204 etags --regex='/^type *\([a^[b-zA-Z_][a-zA-Z0-9_]*\) .*= .*$$\|^\([a-zA-Z][a-zA-Z0-9_]*\) .*=.*$$/\1\2/' $(COGENT_SOURCES) $(COGENT_GUM) 205 etags --append $(filter %.c,$(C_SOURCES) $(LINUX_ACFILES)) 206 etags --append -l c --regex='/^\(\$$ty:(.*) *\)?\(\$$id:\)?\([A-Za-z_][A-Za-z0-9_]*\) *(.*$$/\3/' $(filter %.ac,$(C_SOURCES) $(LINUX_ACFILES)) 207 208help: 209 $(E) "** Cogent ext2fs build help **" 210 $(E) "Run 'make' to build the Linux ext2fs kernel module." 211 $(E) "" 212 $(E) "Please run 'make <target>' where target is one of the following:" 213 $(E) "* linux" 214 $(E) " Build the Linux kernel module(default)." 215 $(E) " This will build against the kernel headers of the current running kernel." 216 $(E) " Pass KERNELDIR=<path-to-kernel-headers> if you want to build against a different kernel version." 217 $(E) " eg.:" 218 $(E) " make linux" 219 $(E) " make linux KERNELDIR=/usr/src/linux-headers-4.3.0-1-amd64/" 220 $(E) "" 221 $(E) "* debug" 222 $(E) " Build the Linux kernel module with debugging enabled." 223 $(E) " This is equivalent to running 'make linux DEBUG=1'" 224 $(E) "" 225 $(E) "* verification" 226 $(E) " Generate verification table." 227 $(E) "" 228 $(E) "* clean" 229 $(E) " Cleanup." 230 $(E) "" 231 $(E) "* help" 232 $(E) " Print this help." 233endif 234