-
Notifications
You must be signed in to change notification settings - Fork 23
/
Makefile
126 lines (84 loc) · 3.64 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
.PHONY: all \
test test-execution test-simple test-prove \
test-conformance test-conformance-parse test-conformance-supported \
media presentations reports
all: build
# Building Definition
# -------------------
ifneq ($(NIX),1)
POETRY := poetry -C pykwasm
POETRY_RUN := $(POETRY) run --
KDIST := $(POETRY_RUN) kdist
endif
.PHONY: pykwasm
pykwasm:
$(POETRY) install
.PHONY: build
build: pykwasm
$(KDIST) -v build -j3
.PHONY: clean
clean: pykwasm
$(KDIST) clean
# Testing
# -------
TEST := $(POETRY_RUN) kwasm
CHECK := git --no-pager diff --no-index --ignore-all-space -R
TEST_CONCRETE_BACKEND := llvm
TEST_SYMBOLIC_BACKEND := haskell
test: test-execution test-prove
# Generic Test Harnesses
tests/%.run: tests/%
$(TEST) run $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out
$(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out tests/success-$(TEST_CONCRETE_BACKEND).out
rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
tests/%.run-term: tests/%
$(TEST) run $< > tests/$*.$(TEST_CONCRETE_BACKEND)-out
grep --after-context=2 "<instrs>" tests/$*.$(TEST_CONCRETE_BACKEND)-out > tests/$*.$(TEST_CONCRETE_BACKEND)-out-term
$(CHECK) tests/$*.$(TEST_CONCRETE_BACKEND)-out-term tests/success-k.out
rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out
rm -rf tests/$*.$(TEST_CONCRETE_BACKEND)-out-term
tests/%.parse: tests/%
K_OPTS='-Xmx16G -Xss512m' $(TEST) kast --output kore $< > $@-out
rm -rf $@-out
tests/%.prove: tests/%
$(eval SOURCE_DIR := $(shell $(KDIST) which wasm-semantics.source))
$(TEST) prove $< kwasm-lemmas -I $(SOURCE_DIR)/wasm-semantics -w2e
tests/proofs/wrc20-spec.k.prove: tests/proofs/wrc20-spec.k
$(eval SOURCE_DIR := $(shell $(KDIST) which wasm-semantics.source))
$(TEST) prove $< wrc20 -I $(SOURCE_DIR)/wasm-semantics -w2e --haskell-backend-command "kore-exec --smt-timeout 500"
### Execution Tests
test-execution: test-simple
simple_tests := $(wildcard tests/simple/*.wast)
simple_tests_failing := $(shell cat tests/failing.simple)
simple_tests_passing := $(filter-out $(simple_tests_failing), $(simple_tests))
test-simple: $(simple_tests_passing:=.run)
### Conformance Tests
conformance_tests:=$(wildcard tests/wasm-tests/test/core/*.wast)
unsupported_conformance_tests:=$(patsubst %, tests/wasm-tests/test/core/%, $(shell cat tests/conformance/unsupported-$(TEST_CONCRETE_BACKEND).txt))
unparseable_conformance_tests:=$(patsubst %, tests/wasm-tests/test/core/%, $(shell cat tests/conformance/unparseable.txt))
parseable_conformance_tests:=$(filter-out $(unparseable_conformance_tests), $(conformance_tests))
supported_conformance_tests:=$(filter-out $(unsupported_conformance_tests), $(parseable_conformance_tests))
test-conformance-parse: $(parseable_conformance_tests:=.parse)
test-conformance-supported: $(supported_conformance_tests:=.run-term)
test-conformance: test-conformance-parse test-conformance-supported
### Proof Tests
proof_tests:=$(wildcard tests/proofs/*-spec.k)
test-prove: $(proof_tests:=.prove)
# Analysis
# --------
json_build := $(haskell_dir)/parsed.json
$(json_build):
$(MAKE) build-haskell -B KOMPILE_OPTS="--emit-json"
graph-imports: $(json_build)
kpyk $(haskell_dir) graph-imports
# Presentation
# ------------
media: presentations reports
media/%.pdf: TO_FORMAT=beamer
presentations: $(patsubst %.md, %.pdf, $(wildcard media/*-presentation-*.md))
media/201903-report-chalmers.pdf: TO_FORMAT=latex
reports: media/201903-report-chalmers.pdf
media/%.pdf: media/%.md media/citations.md
cat $^ | pandoc --from markdown-latex_macros --to $(TO_FORMAT) --filter pandoc-citeproc --output $@
media-clean:
rm media/*.pdf