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
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
|
ifeq (3.81,$(MAKE_VERSION))
$(error You seem to be using the OSX antiquated Make version. Hint: brew \
install make, then invoke gmake instead of make)
endif
.PHONY: default
default: build
.PHONY: all
all: build-tests-verify nix
####################################
# Variables customizable by the user
####################################
# Paths to the executables we need for tests. They are overriden in CI.
AENEAS_EXE ?= $(PWD)/bin/aeneas
TEST_RUNNER_EXE ?= $(PWD)/bin/test_runner
CHARON_EXE ?= $(PWD)/charon/bin/charon
# The user can specify additional translation options for Aeneas.
AENEAS_OPTIONS ?=
CHARON_OPTIONS ?=
# The directory thta contains the rust source files for tests.
INPUTS_DIR ?= tests/src
# The directory where to look for the .llbc files.
LLBC_DIR ?= tests/llbc
# In CI, we enforce formatting and activate the (expensive) sanity checks.
IN_CI ?=
####################################
# The rules
####################################
# Never remove intermediate files
.SECONDARY:
# Build the compiler, after formatting the code
.PHONY: build
build: format build-dev
# Build the project, test it and verify the generated files
.PHONY: build-test-verify
build-test-verify: build test verify
# Build the project, without formatting the code
.PHONY: build-dev
ifdef IN_CI
build-dev:
@true
else
build-dev: build-bin build-lib build-bin-dir doc
endif
.PHONY: build-bin
build-bin: check-charon
cd compiler && dune build
.PHONY: build-lib
build-lib: check-charon
cd compiler && dune build aeneas.cmxs
.PHONY: build-runner
build-runner: check-charon
cd tests/test_runner && dune build
.PHONY: build-bin-dir
build-bin-dir: build-bin build-lib build-runner
mkdir -p bin
cp -f compiler/_build/default/main.exe bin/aeneas
cp -f compiler/_build/default/main.exe bin/aeneas.cmxs
cp -f tests/test_runner/_build/default/run_test.exe bin/test_runner
mkdir -p bin/backends/fstar
mkdir -p bin/backends/coq
cp -rf backends/fstar/*.fst* bin/backends/fstar/
cp -rf backends/coq/*.v bin/backends/coq/
.PHONY: doc
doc:
cd compiler && dune build @doc
# Fetches the latest commit from charon and updates `flake.lock` accordingly.
.PHONY: update-charon-pin
update-charon-pin:
nix flake lock --update-input charon
$(MAKE) charon-pin
# Keep the commit revision in `./charon-pin` as well so that non-nix users can
# know which commit to use.
./charon-pin: flake.lock
./scripts/update-charon-pin.sh >> ./charon-pin
# Checks that `./charon` contains a clone of charon at the required commit.
# Also checks that `./charon/bin/charon` exists.
.PHONY: check-charon
check-charon:
@echo "Checking the charon installation"
@./scripts/check-charon-install.sh
# Sets up the charon repository on the right commit.
.PHONY: setup-charon
setup-charon:
@./scripts/check-charon-install.sh --force
ifdef IN_CI
# In CI, error if formatting is not done.
format: RUSTFMT_FLAGS := --check
endif
# Reformat the project files
.PHONY: format
format:
@# `|| `true` because the command returns an error if it changed anything, which we don't care about.
cd compiler && dune fmt || true
cd tests/test_runner && dune fmt || true
rustfmt $(RUSTFMT_FLAGS) $(INPUTS_DIR)/*.rs
cd $(INPUTS_DIR)/betree && cargo fmt $(RUSTFMT_FLAGS)
.PHONY: clean
clean: clean-generated
cd compiler && dune clean
cd $(INPUTS_DIR)/betree && $(MAKE) clean
.PHONY: clean-generated
clean-generated: clean-generated-aeneas clean-generated-llbc
.PHONY: clean-generated-aeneas
clean-generated-aeneas:
@# We can't put this line in `tests/Makefile` otherwise it will detect itself.
@# FIXME: generation of hol4 files is deactivated so we don't delete those.
@# `|| true` to avoid failing if there are no generated files present.
grep -lR 'THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS' tests | grep -v '^tests/hol4' | xargs rm || true
.PHONY: clean-generated-llbc
clean-generated-llbc:
rm -rf $(LLBC_DIR)
# =============================================================================
# The tests.
# =============================================================================
# Test the project by translating test files to various backends.
.PHONY: test
test: build-dev test-all betree-tests
# This runs the rust tests of the betree crate.
.PHONY: betree-tests
betree-tests:
cd $(INPUTS_DIR)/betree && $(MAKE) test
# Verify the F* files generated by the translation
.PHONY: verify
verify:
cd tests && $(MAKE) all
# List the files and directories in `INPUTS_DIR`
INPUTS_LIST = $(wildcard $(INPUTS_DIR)/*)
# Remove the committed output files
INPUTS_LIST := $(filter-out %.out,$(INPUTS_LIST))
# Remove the directory prefix, replace with `test-`
INPUTS_LIST := $(subst $(INPUTS_DIR)/,test-,$(INPUTS_LIST))
# Run all the tests we found.
.PHONY: test-all
test-all: $(INPUTS_LIST)
ifdef IN_CI
# In CI we do extra sanity checks.
test-%: AENEAS_OPTIONS += -checks
endif
# Translate the given rust file to available backends. The test runner decides
# which backends to use and sets test-specific options.
# Note: the tests have the fulle file name: `test-arrays.rs`, `test-loops.rs`, `test-betree`.
.PHONY: test-%
test-%: build-dev
$(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(INPUTS_DIR)/"$*" $(AENEAS_OPTIONS)
echo "# Test $* done"
# =============================================================================
# Nix
# =============================================================================
# TODO: add the lean tests
.PHONY: nix
nix:
nix build && nix flake check
.PHONY: nix-aeneas-tests
nix-aeneas-tests:
nix build .#checks.x86_64-linux.aeneas-tests --show-trace -L
.PHONY: nix-aeneas-verify-fstar
nix-aeneas-verify-fstar:
nix build .#checks.x86_64-linux.aeneas-verify-fstar --show-trace -L
.PHONY: nix-aeneas-verify-fstar-split
nix-aeneas-verify-fstar-split:
nix build .#checks.x86_64-linux.aeneas-verify-fstar-split --show-trace -L
.PHONY: nix-aeneas-verify-coq
nix-aeneas-verify-coq:
nix build .#checks.x86_64-linux.aeneas-verify-coq --show-trace -L
.PHONY: nix-aeneas-verify-lean
nix-aeneas-verify-lean:
nix build .#checks.x86_64-linux.aeneas-verify-lean --show-trace -L
.PHONY: nix-aeneas-verify-hol4
nix-aeneas-verify-hol4:
nix build .#checks.x86_64-linux.aeneas-verify-hol4 --show-trace -L
|
