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