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=cogent-vfat
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=vfat
21SRC=src/super.cogent
22TYPES=data/types.txt
23DEFNS=data/defns.txt
24PROOF_ID=Vfat
25
26# GCC version
27GCCVER=$(shell gcc -dumpversion)
28
29# Standard Gum Directory
30LIBGUM=$(shell cogent --libgum-dir)
31# ADT headers required by vfat
32# AHFILES=$(wildcard $(LIBGUM)/gum/anti/abstract/*.ah)
33AHFILES=
34# ADT C files required by vfat
35LINUX_ACFILES=plat/linux/wrapper.ac
36
37# ADT C files required by verification
38VERIF_ACFILES=plat/verification/wrapper.ac
39
40ifndef KERNELDIR
41KERNELDIR:= /lib/modules/$(shell uname -r)/build
42endif
43
44ifeq ($(KERNELRELEASE),)
45PWD:= $(shell pwd)
46endif
47
48ifneq ($(DEBUG),)
49EXTRA_CFLAGS+= -DSKELFS_DEBUG -g #TODO: FIX THIS
50COGENT_FLAGS+= --debug
51endif
52
53# flags to ignores COGENT's compiler messy C code gen
54COMMON_CFLAGS := -O2 -Wno-parentheses -Wno-declaration-after-statement -Wno-unused-variable -Wno-uninitialized
55LINUX_EXTRA_CFLAGS := -I$(PWD)/plat/linux/ -I$(PWD) -I$(PWD)/src -I$(PWD)/lib -I$(PWD)/abstract $(COMMON_CFLAGS) -I$(LIBGUM)
56VERIF_EXTRA_CFLAGS := -I$(PWD)/plat/verification/ -I$(PWD) -I$(PWD)/src -I$(PWD)/lib -I$(PWD)/abstract -I$(LIBGUM) $(COMMON_CFLAGS)
57
58# COGENT flags
59COGENT_FLAGS+= -Od --fno-static-inline --fno-fncall-as-macro --ffunc-purity-attr
60# end of configuration
61
62override COGENT_FLAGS+= -o$(OUTPUT) \
63			--root-dir=$(ROOT_DIR) \
64			--entry-funcs=$(DEFNS) \
65			--ext-types=$(TYPES) \
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
77# Add C files with no antiquotation to OBJ.
78# Writing these functions in a .ac file would lead defining multiple
79# times the same symbol when parametric polymorphism gets expanded.
80# NOTE: A module.o is relevant only for the linux platform
81OBJ?=plat/linux/module.o
82
83
84###########################
85# TARGET-SPECIFIC VARIABLES
86###########################
87# ACFILES
88linux: ACFILES = $(LINUX_ACFILES)
89.c-gen: ACFILES = $(LINUX_ACFILES)
90verification: ACFILES = $(VERIF_ACFILES)
91.verif-gen: ACFILES = $(VERIF_ACFILES)
92# DISTDIR
93linux: DIST_DIR = plat/linux
94.c-gen: 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)
100verification: EXTRA_CFLAGS = $(VERIF_EXTRA_CFLAGS)
101.verif-gen: EXTRA_CFLAGS = $(VERIF_EXTRA_CFLAGS)
102
103
104# call from kernel build system
105ifneq ($(KERNELRELEASE),)
106	ccflags-y+=-I/usr/lib/gcc/x86_64-pc-linux-gnu/$(GCCVER)/include
107	obj-m+= cogent-fat.o
108	obj-m+= $(MODULE).o
109
110#$(MODULE)-objs := $(OBJ)
111	cogent-fat-y := plat/linux/cache.o plat/linux/dir.o plat/linux/fatent.o plat/linux/file.o plat/linux/inode.o plat/linux/misc.o plat/linux/nfs.o
112	$(MODULE)-y := plat/linux/module.o
113else
114
115PWD:= $(shell pwd)
116
117.PHONY: default cogent clean .c-gen .verif-gen verification
118
119default: linux
120
121all: .c-gen $(OBJ)
122	$(Q)$(CC) -o $(NAME) $(OBJ)
123
124%.c:
125	$(Q)$(CC) -c $@
126
127# generate executable C cod
128# NOTE: We run cpp with in c99 mode, as the default mode that cpp runs in is gnu99,
129#       which has an issue when parsing. It replaces anything 'linux' with a '1'.
130#       More details here: http://stackoverflow.com/questions/19210935/why-does-the-c-preprocessor-interpret-the-word-linux-as-the-constant-1
131#       So we use c99 mode here and when building the generated C code(make modules), we
132#       use `gnu99` mode.
133.c-gen:
134	$(Q)cogent $(SRC) -g $(COGENT_FLAGS) \
135		--cpp-args="-std=c99 \$$CPPIN -o \$$CPPOUT -E -P $(EXTRA_CFLAGS)" \
136		--dist-dir=$(DIST_DIR) \
137		--infer-c-funcs="$(ACFILES)"
138
139.verif-gen:
140	$(Q)cogent $(SRC) -A $(COGENT_FLAGS) \
141		--cpp-args="-std=c99 \$$CPPIN -o \$$CPPOUT -E -P $(EXTRA_CFLAGS)" \
142		--dist-dir=$(DIST_DIR) \
143		--infer-c-funcs="$(ACFILES)" \
144		--proof-name=$(PROOF_ID) \
145		--proof-input-c="wrapper_pp_inferred.c"
146
147# compile Linux kernel module for file system
148linux: .c-gen
149	make -C  $(KERNELDIR) CFLAGS="$(CFLAGS)" EXTRA_CFLAGS="-std=gnu99 $(EXTRA_CFLAGS)" M=$(PWD) modules
150	#$(Q) $(MAKE) OBJ="$(OBJ)" CFLAGS="$(CFLAGS)" EXTRA_CFLAGS="$(EXTRA_CFLAGS)" -C $(KERNELDIR) M=$(PWD) modules
151# generate verification-clean C code and proof scripts
152verification: .verif-gen
153	$(Q)mv $(DIST_DIR)/$(OUTPUT).table $(DIST_DIR)/wrapper_pp_inferred.table
154
155
156clean:
157	$(E) "Cleaning up..."
158	$(Q) make -C $(KERNELDIR) M=$(PWD) clean
159	$(Q) rm -f $(HOUTPUT)
160	$(Q) rm -f $(OBJ)
161	$(Q) rm -f $(RTMPC)
162	$(Q) rm -f $(RTMPPPC)
163	$(Q) rm -f $(MODULE).mod.[co] $(MODULE).o $(MODULE).ko Module.symvers modules.order
164	$(Q) rm -f abstract/*.h
165	$(Q) rm -rf *.thy ROOT $(OUTPUT).table BUILD_INFO
166	$(Q) find . -name *.thy -exec rm -f {} \;
167	$(Q) find . -name ROOT -exec rm -f {} \;
168	$(Q) find . -name BUILD_INFO -exec rm -f {} \;
169	$(Q) find . -name *_pp* -exec rm -f {} \;
170	$(Q) find . -name $(OUTPUT).* -exec rm -f {} \;
171	$(Q)find . -name *.cmd -exec rm -f {} \;
172
173help:
174	$(E) "** Cogent vfat build help **"
175	$(E) "Run 'make' to build the Linux vfat kernel module."
176	$(E) ""
177	$(E) "Please run 'make <target>' where target is one of the following:"
178	$(E) "* linux"
179	$(E) "  Build the Linux kernel module(default)."
180	$(E) "  This will build against the kernel headers of the current running kernel."
181	$(E) "  Pass KERNELDIR=<path-to-kernel-headers> if you want to build against a different kernel version."
182	$(E) "  eg.:"
183	$(E) "     make linux"
184	$(E) "     make linux KERNELDIR=/usr/src/linux-headers-4.3.0-1-amd64/"
185	$(E) ""
186	$(E) "* debug"
187	$(E) "  Build the Linux kernel module with debugging enabled."
188	$(E) "  This is equivalent to running 'make linux DEBUG=1'"
189	$(E) ""
190	$(E) "* verification"
191	$(E) "  Generate verification table."
192	$(E) ""
193	$(E) "* clean"
194	$(E) "  Cleanup."
195	$(E) ""
196	$(E) "* help"
197	$(E) "  Print this help."
198
199endif
200