-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathMakefile
168 lines (124 loc) · 5.26 KB
/
Makefile
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
BUILD_DIR := .build
BUILD_LOCAL := $(abspath $(BUILD_DIR)/local)
LOCAL_LIB := $(BUILD_LOCAL)/lib
DEPS_DIR := ext
K_SUBMODULE := $(abspath $(DEPS_DIR)/k)
PLUGIN_SUBMODULE := $(abspath $(DEPS_DIR)/blockchain-k-plugin)
K_RELEASE ?= $(K_SUBMODULE)/k-distribution/target/release/k
K_BIN := $(K_RELEASE)/bin
K_LIB := $(K_RELEASE)/lib
export K_RELEASE
PATH := $(K_BIN):$(PATH)
export PATH
.PHONY: all clean distclean \
deps k-deps \
build \
tests \
all: build
# K Dependencies
# --------------
deps : repo-deps
repo-deps : k-deps plugin-deps
k-deps : $(K_SUBMODULE)/make.timestamp
plugin-deps: $(PLUGIN_SUBMODULE)/make.timestamp
$(K_SUBMODULE)/make.timestamp:
git submodule update --init --recursive -- $(K_SUBMODULE)
cd $(K_SUBMODULE) && mvn package -DskipTests -U -Dproject.build.type=FastBuild
touch $(K_SUBMODULE)/make.timestamp
$(PLUGIN_SUBMODULE)/make.timestamp:
git submodule update --init --recursive -- $(PLUGIN_SUBMODULE)
touch $(PLUGIN_SUBMODULE)/make.timestamp
# Building
# --------
MAIN_MODULE := MEDIK
SYNTAX_MODULE := MEDIK-SYNTAX
export MAIN_DEFN_FILE := medik
COMMON_FILES :=
EXTRA_K_FILES += $(MAIN_DEFN_FILE).md
ALL_K_FILES := $(COMMON_FILES) $(EXTRA_K_FILES)
build: build-execution build-model-check build-symbolic
COMMON_OPTS := -w all -Wno unused-symbol --gen-glr-bison-parser
# LLVM-Build Pipeline
# ===================
# Concrete Execution
# ------------------
LLVM_EXEC_BUILD_DIR := $(BUILD_DIR)/llvm-exec
LLVM_EXEC_KOMPILED_DIR := $(LLVM_EXEC_BUILD_DIR)/$(MAIN_DEFN_FILE)-llvm-kompiled
build-execution: $(LLVM_EXEC_KOMPILED_DIR)/make.timestamp
PLUGIN_FILES := $(PLUGIN_SUBMODULE)/plugin-c/json.cpp $(PLUGIN_SUBMODULE)/plugin-c/k.cpp
CPP_FILES := $(PLUGIN_FILES)
LLVM_OPTS := --hook-namespaces JSON
LLVM_KOMPILE_OPTS := $(COMMON_OPTS) $(LLVM_OPTS)
LLVM_CC_OPTS := -L$(LOCAL_LIB) -I$(K_RELEASE)/include/kllvm \
-I$(PLUGIN_SUBMODULE)/plugin-c \
$(abspath $(CPP_FILES)) \
-Wall -g -Wno-return-type-c-linkage #TODO: Fix disabled warning
$(LLVM_EXEC_KOMPILED_DIR)/make.timestamp: $(ALL_K_FILES) $(CPP_FILES)
mkdir -p $(LLVM_EXEC_BUILD_DIR)
kompile --output-definition $(LLVM_EXEC_KOMPILED_DIR) \
--md-selector 'k|concrete' \
$(LLVM_KOMPILE_OPTS) \
$(addprefix -ccopt , $(LLVM_CC_OPTS)) \
--main-module $(MAIN_MODULE) --syntax-module $(SYNTAX_MODULE) $(MAIN_DEFN_FILE).md
@touch $@
# Model Checking
# --------------
LLVM_MCHECK_BUILD_DIR := $(BUILD_DIR)/llvm-mcheck
LLVM_MCHECK_KOMPILED_DIR := $(LLVM_MCHECK_BUILD_DIR)/$(MAIN_DEFN_FILE)-llvm-kompiled
build-model-check: $(LLVM_MCHECK_KOMPILED_DIR)/make.timestamp
LLVM_MCHECK_OPTS := $(COMMON_OPTS) --enable-search \
$(LLVM_MCHECK_KOMPILED_DIR)/make.timestamp: $(ALL_K_FILES)
mkdir -p $(LLVM_MCHECK_BUILD_DIR)
kompile --output-definition $(LLVM_MCHECK_KOMPILED_DIR) \
--md-selector 'k|mcheck' \
$(LLVM_MCHECK_OPTS) \
--main-module $(MAIN_MODULE) --syntax-module $(SYNTAX_MODULE) $(MAIN_DEFN_FILE).md
@touch $@
# Haskell-Build Pipeline
# ----------------------
HASKELL_BUILD_DIR := $(BUILD_DIR)/haskell-symbolic
HASKELL_KOMPILED_DIR := $(HASKELL_BUILD_DIR)/$(MAIN_DEFN_FILE)-haskell-kompiled
HASKELL_OPTS :=
HASKELL_KOMPILE_OPTS := $(COMMON_OPTS) $(HASKELL_OPTS)
build-symbolic: $(HASKELL_KOMPILED_DIR)/make.timestamp
$(HASKELL_KOMPILED_DIR)/make.timestamp: $(ALL_K_FILES)
mkdir -p $(HASKELL_BUILD_DIR)
kompile --output-definition $(HASKELL_KOMPILED_DIR) \
--backend haskell \
--md-selector 'k|symbolic' \
$(HASKELL_KOMPILE_OPTS) \
--main-module $(MAIN_MODULE) --syntax-module $(SYNTAX_MODULE) $(MAIN_DEFN_FILE).md
@touch $@
# Tests
# -----
COMPARE := git --no-pager diff --no-index --ignore-all-space -R
GREEN := \033[0;32m
RESET := \033[0m
# Regular Medik Tests
# -------------------
TEST_EXECUTION_FILES := $(wildcard tests/execution/*.medik)
tests-execution: $(patsubst tests/execution/%.medik, tests/execution/%.medik.run, $(TEST_EXECUTION_FILES))
tests/execution/%.medik.run: tests/execution/%.medik tests/execution/%.medik.expected $(LLVM_EXEC_KOMPILED_DIR)/make.timestamp
@printf '%-45s %s' "$< " "... "
@if [ -f tests/execution/$*.medik.in ]; then \
./medik -in tests/execution/$*.medik.in $< > $@; \
else ./medik $< > $@; fi
@$(COMPARE) $@ $(word 2, $^)
@printf "${GREEN}OK ${RESET}\n"
# Model Checking Tests
# --------------------
TEST_MODEL_CHECK_FILES := $(wildcard tests/model-check/*.medik)
KRUN_MCHECK := krun --definition $(LLVM_MCHECK_KOMPILED_DIR) --search
tests-model-check: $(patsubst tests/model-check/%.medik, tests/model-check/%.medik.run, $(TEST_MODEL_CHECK_FILES))
tests/model-check/%.medik.run: tests/model-check/%.medik tests/model-check/%.medik.expected $(LLVM_MCHECK_KOMPILED_DIR)/make.timestamp
@printf '%-45s %s' "$< " "... "
@$(KRUN_MCHECK) --pattern "$$(cat tests/model-check/$*.medik.pattern)" $< > $@
@$(COMPARE) $@ $(word 2, $^)
@printf "${GREEN}OK ${RESET}\n"
# Complete Tests Suite
# --------------------
tests: tests-execution tests-model-check
# Cleaning
# --------
clean:
rm -rf .build tests/*.tmp