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