-
Notifications
You must be signed in to change notification settings - Fork 6
/
Copy pathMakefile
175 lines (127 loc) · 4.96 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
168
169
170
171
172
173
174
175
.PHONY: all clean distclean deps deps-polkadot \
build \
polkadot-runtime-source polkadot-runtime-loaded \
prove-specs defn-specs kompile-specs \
test test-python-config test-search
# Settings
# --------
BUILD_DIR := .build
DEPS_DIR := deps
DEFN_DIR := $(BUILD_DIR)/defn
KWASM_SUBMODULE := $(DEPS_DIR)/wasm-semantics
K_SUBMODULE := $(KWASM_SUBMODULE)/deps/k
ifneq (,$(wildcard $(K_SUBMODULE)/k-distribution/target/release/k/bin/*))
K_RELEASE ?= $(abspath $(K_SUBMODULE)/k-distribution/target/release/k)
else
K_RELEASE ?= $(dir $(shell which kompile))..
endif
K_BIN := $(K_RELEASE)/bin
K_LIB := $(K_RELEASE)/lib/kframework
export K_RELEASE
KWASM_DIR := .
KWASM_MAKE := make --directory $(KWASM_SUBMODULE) BUILD_DIR=../../$(BUILD_DIR) RELEASE=$(RELEASE)
export KWASM_DIR
PATH := $(K_BIN):$(CURDIR)/$(KWASM_SUBMODULE):$(PATH)
export PATH
PYTHONPATH := $(K_LIB)
export PYTHONPATH
PANDOC_TANGLE_SUBMODULE := $(abspath $(DEPS_DIR)/pandoc-tangle)
TANGLER := $(PANDOC_TANGLE_SUBMODULE)/tangle.lua
LUA_PATH := $(PANDOC_TANGLE_SUBMODULE)/?.lua;;
export TANGLER
export LUA_PATH
KPOL := ./kpol
all: build
clean:
rm -rf $(DEFN_DIR) tests/*.out
distclean: clean
rm -rf $(BUILD_DIR)
deps:
$(KWASM_MAKE) deps
# Polkadot Setup
# --------------
POLKADOT_SUBMODULE := $(DEPS_DIR)/substrate
POLKADOT_RUNTIME_WASM := $(POLKADOT_SUBMODULE)/target/release/wbuild/node-template-runtime/node_template_runtime.compact.wasm
# Useful Builds
# -------------
KOMPILE_OPTS := --emit-json
MAIN_MODULE := KWASM-POLKADOT-HOST
MAIN_SYNTAX_MODULE := KWASM-POLKADOT-HOST-SYNTAX
MAIN_DEFN_FILE := kwasm-polkadot-host
ifeq (coverage,$(BUILD))
KOMPILE_OPTS += --coverage
SUBDEFN := coverage
else
SUBDEFN := kwasm
endif
export SUBDEFN
build: build-llvm build-haskell
# Semantics Build
# ---------------
build-%: $(KWASM_SUBMODULE)/$(MAIN_DEFN_FILE).md
$(KWASM_MAKE) build-$* \
DEFN_DIR=../../$(DEFN_DIR)/$(SUBDEFN) \
llvm_main_module=$(MAIN_MODULE) \
llvm_syntax_module=$(MAIN_SYNTAX_MODULE) \
llvm_main_file=$(MAIN_DEFN_FILE) \
haskell_main_module=$(MAIN_MODULE) \
haskell_syntax_module=$(MAIN_SYNTAX_MODULE) \
haskell_main_file=$(MAIN_DEFN_FILE) \
EXTRA_SOURCE_FILES=$(MAIN_DEFN_FILE).md \
KOMPILE_OPTS="$(KOMPILE_OPTS)"
$(KWASM_SUBMODULE)/$(MAIN_DEFN_FILE).md: $(MAIN_DEFN_FILE).md
cp $< $@
# Verification Source Build
# -------------------------
CONCRETE_BACKEND := llvm
SYMBOLIC_BACKEND := haskell
POLKADOT_RUNTIME_WAT := src/polkadot-runtime.wat
POLKADOT_RUNTIME_ENV_WAT := src/polkadot-runtime.env.wat
POLKADOT_RUNTIME_JSON := src/polkadot-runtime.wat.json
POLKADOT_RUNTIME_LOADED_JSON := src/polkadot-runtime.loaded.json
polkadot-runtime-source: $(POLKADOT_RUNTIME_WAT)
polkadot-runtime-loaded: $(POLKADOT_RUNTIME_LOADED_JSON)
$(POLKADOT_RUNTIME_WASM):
cd $(POLKADOT_SUBMODULE) && cargo build --package node-template --release
$(POLKADOT_RUNTIME_WAT): $(POLKADOT_RUNTIME_WASM)
@mkdir -p src
wasm2wat $< | sed 's/(elem/;; (elem/' > $@
$(POLKADOT_RUNTIME_ENV_WAT): $(POLKADOT_RUNTIME_WAT)
./build-runtime-host.sh $< > $@
$(POLKADOT_RUNTIME_LOADED_JSON): $(POLKADOT_RUNTIME_JSON)
$(KPOL) run --backend $(CONCRETE_BACKEND) $< --parser cat --output json > $@
$(POLKADOT_RUNTIME_JSON): $(POLKADOT_RUNTIME_ENV_WAT) $(POLKADOT_RUNTIME_WAT)
cat $^ | $(KPOL) kast --backend $(CONCRETE_BACKEND) - json > $@
# Specification Build
# -------------------
SPEC_NAMES := set-balance
SPECS_DIR := $(BUILD_DIR)/specs
SPECS_SOURCE := $(patsubst %, %.md, $(SPEC_NAMES))
SPECS_PROOFS := $(patsubst %, $(SPECS_DIR)/%-spec.k, $(SPEC_NAMES))
SPECS_KOMPILED := $(patsubst %, $(SPECS_DIR)/%-kompiled/definition.kore, $(SPEC_NAMES))
defn-specs: $(SPECS_SOURCE)
kompile-specs: $(SPECS_KOMPILED)
prove-specs: $(SPECS_PROOFS:=.prove)
$(SPECS_DIR)/%-kompiled/definition.kore: %.md
kompile --backend $(SYMBOLIC_BACKEND) -I $(CURDIR) \
--main-module $(shell echo $* | tr '[:lower:]' '[:upper:]') \
--syntax-module $(shell echo $* | tr '[:lower:]' '[:upper:]') \
--directory $(SPECS_DIR) \
$<
$(SPECS_DIR)/%-spec.k.prove: $(SPECS_DIR)/%-spec.k $(SPECS_DIR)/%-kompiled/definition.kore
kprove --directory $(SPECS_DIR) $(SPECS_DIR)/$*-spec.k --def-module VERIFICATION
$(SPECS_DIR)/%-spec.k: %-spec.md $(TANGLER)
@mkdir -p $(dir $@)
pandoc --from markdown --to $(TANGLER) --metadata=code:.k $< > $@
# Testing
# -------
CHECK := git --no-pager diff --no-index --ignore-all-space
test: prove-specs test-python-config test-search
# Search Through Executions
# -------------------------
test-search:
python3 search.py summary
# Python Configuration Build
# --------------------------
test-python-config:
python3 pykWasm.py