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