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=wa_example 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=wa 21SRC=wa.cogent 22DEFNS=defns.txt 23 24# Standard Gum Directory 25LIBGUM=$(COGENT_LIBGUM_DIR) 26# ADT headers required by BilbyFs 27AHFILES=$(addprefix $(LIBGUM)/gum/anti/abstract/, \ 28 WordArray.ah) 29# ADT C files required by BilbyFs 30LINUX_ACFILES=wa_wrapper.ac 31# ADT C files required by verification 32LINUX_TYPES=types.txt 33 34ifeq ($(KERNELRELEASE),) 35PWD:= $(shell pwd) 36endif 37ifneq ($(DEBUG),) 38EXTRA_CFLAGS+= -DBILBYFS_DEBUG 39COGENT_FLAGS+= --debug 40endif 41 42# flags to ignores COGENT's compiler messy C code gen 43COMMON_CFLAGS := -O2 -Wno-parentheses -Wno-declaration-after-statement -Wno-unused-variable -Wno-uninitialized 44LINUX_EXTRA_CFLAGS := -I$(PWD) -I$(PWD)/build -I$(PWD)/abstract $(COMMON_CFLAGS) -I$(LIBGUM) 45 46# COGENT flags 47COGENT_FLAGS+= -Od --fno-static-inline --fno-fncall-as-macro --fnormalisation=knf --ffunc-purity-attr --fffi-c-functions 48# end of configuration 49 50override COGENT_FLAGS+= -o$(OUTPUT) \ 51 --root-dir=$(ROOT_DIR) \ 52 --entry-funcs=$(DEFNS) \ 53 --infer-c-types="$(AHFILES)" \ 54 --abs-type-dir=$(PWD) 55 56COUTPUT=$(addsuffix .c, $(OUTPUT)) 57HOUTPUT=$(addsuffix .h, $(OUTPUT)) 58NAME=$(MODULE) 59RTMPC=$(ACFILES:.ac=_pp_inferred.c) 60RTMPPPC=$(COUTPUT) $(ACFILES:.ac=_pp.ac) 61 62BUILDSRC=$(wildcard build/*.c) 63# Add C files with no antiquotation to OBJ. 64# Writing these functions in a .ac file would lead defining multiple 65# times the same symbol when parametric polymorphism gets expanded. 66 67 68# ACFILES 69ACFILES = $(LINUX_ACFILES) 70# DISTDIR 71DIST_DIR = build 72# EXTRA_CFLAGS 73EXTRA_CFLAGS = $(LINUX_EXTRA_CFLAGS) 74EXTRA_CFLAGS += -D BUG_ON(x)= -D printk=printf 75 76# call from kernel build system 77ifneq ($(KERNELRELEASE),) 78 obj-m += $(MODULE).o 79 $(MODULE)-objs := $(OBJ) 80else 81 82PWD:= $(shell pwd) 83 84.PHONY: default all clean c-gen o-gen hs-gen 85 86 87default: c-gen o-gen 88all: c-gen o-gen 89 90# generate executable C code 91# NOTE: We run cpp with in c99 mode, as the default mode that cpp runs in is gnu99, 92# which has an issue when parsing. It replaces anything 'linux' with a '1'. 93# More details here: http://stackoverflow.com/questions/19210935/why-does-the-c-preprocessor-interpret-the-word-linux-as-the-constant-1 94# So we use c99 mode here and when building the generated C code(make modules), we 95# use `gnu99` mode. 96c-gen: 97 $(Q)cogent $(SRC) -Q $(COGENT_FLAGS) \ 98 --cpp-args="-std=c99 \$$CPPIN -o \$$CPPOUT -E -P $(EXTRA_CFLAGS)" \ 99 --dist-dir=$(DIST_DIR) \ 100 --infer-c-funcs="$(ACFILES)" \ 101 --ext-types="$(LINUX_TYPES)" 102 103o-gen: 104 $(Q)$(CC) -c $(DIST_DIR)/wa_wrapper_pp_inferred.c -o $(DIST_DIR)/wa.o -I$(DIST_DIR) -I$(PWD) -fPIC 105 106hs-gen: 107 $(Q)cogent $(SRC) --hs-shallow-desugar $(COGENT_FLAGS) \ 108 --dist-dir=$(DIST_DIR) 109 110clean: 111 $(E) "Cleaning up.." 112 $(Q)rm -f abstract/*.h 113 $(Q)rm -rf $(DIST_DIR) 114 115endif 116