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