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