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