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