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