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