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