blob: c4ec50efb39354489b44886708556c5b25bd6afe (
plain)
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-test-verify nix
####################################
# Variables customizable by the user
####################################
# Set this variable to any value to call Charon to regenerate the .llbc source
# files before running the tests
REGEN_LLBC ?=
# The path to Charon
CHARON_HOME ?= ../charon
# The paths to the test directories in Charon (Aeneas will look for the .llbc
# files in there).
CHARON_TESTS_REGULAR_DIR ?= $(CHARON_HOME)/tests
CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius
# The path to the Aeneas executable to run the tests - we need the ability to
# change this path for the Nix package.
AENEAS_EXE ?= bin/aeneas.exe
# The user can specify additional translation options for Aeneas.
# By default we do:
# - unfold all the monadic let bindings to matches (required by F*)
# - insert calls to the normalizer in the translated code to test the
# generated unit functions
OPTIONS +=
#
# The rules use (and update) the following variables
#
# The Charon test directory where to look for the .llbc files
CHARON_TEST_DIR =
# The options with which to call Charon
CHARON_OPTIONS =
# The backend sub-directory in which to generate the files
BACKEND_SUBDIR :=
# The directory in which to extract the result of the translation
SUBDIR :=
####################################
# The rules
####################################
# Build the project, test it and verify the generated files
.PHONY: build-test-verify
build-tests-verify: build tests verify
# Build the project
.PHONY: build
build: build-driver build-lib build-bin-dir doc
.PHONY: build-driver
build-driver:
cd compiler && dune build $(AENEAS_DRIVER)
.PHONY: build-lib
build-lib:
cd compiler && dune build aeneas.cmxs
.PHONY: build-bin-dir
build-bin-dir: build-driver build-lib
mkdir -p bin
cp -f compiler/_build/default/driver.exe bin/aeneas.exe
cp -f compiler/_build/default/driver.exe bin/aeneas.cmxs
cp -rf backends bin
.PHONY: doc
doc:
cd compiler && dune build @doc
.PHONY: clean
clean:
cd compiler && dune clean
# Test the project by translating test files to F*
.PHONY: tests
tests: trans-no_nested_borrows trans-paper \
trans-hashmap trans-hashmap_main \
trans-external trans-constants \
transp-polonius_list transp-betree_main \
test-transp-betree_main
# Verify the F* files generated by the translation
.PHONY: verify
verify:
cd tests && $(MAKE) all
# Reformat the project
.PHONY: format
format:
cd compiler && dune promote
# The commands to run Charon to generate the .llbc files
ifeq (, $(REGEN_LLBC))
else
CHARON_CMD = cd $(CHARON_TEST_DIR) && NOT_ALL_TESTS=1 $(MAKE) test-$*
endif
# The command to run Aeneas on the proper llbc file
AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BACKEND_SUBDIR)/$(SUBDIR) $(OPTIONS)
# Add specific options to some tests
trans-no_nested_borrows trans-paper: \
OPTIONS += -test-units -test-trans-units -no-split-files -no-state
trans-no_nested_borrows trans-paper: SUBDIR:=misc
tfstar-no_nested_borrows tfstar-paper:
trans-hashmap: OPTIONS += -no-state
trans-hashmap: SUBDIR:=hashmap
tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
trans-hashmap_main: OPTIONS +=
trans-hashmap_main: SUBDIR:=hashmap_on_disk
tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
transp-polonius_list: OPTIONS += -test-units -test-trans-units -no-split-files -no-state
transp-polonius_list: SUBDIR:=misc
tfstarp-polonius_list: OPTIONS +=
trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state
trans-constants: SUBDIR:=misc
tfstar-constants: OPTIONS +=
trans-external: OPTIONS +=
trans-external: SUBDIR:=misc
tfstar-external: OPTIONS +=
BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
transp-betree_main: OPTIONS += -backward-no-state-update
transp-betree_main: SUBDIR:=betree
tfstarp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
# Additional test on the betree: translate it without `-backward-no-state-update`.
# This generates very ugly code, but is good to test the translation.
.PHONY: test-transp-betree_main
test-transp-betree_main: transp-betree_main
test-transp-betree_main: OPTIONS += -backend fstar -unfold-monads -test-trans-units
test-transp-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
test-transp-betree_main: BACKEND_SUBDIR := "fstar"
test-transp-betree_main: SUBDIR:=betree_back_stateful
test-transp-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
test-transp-betree_main: FILE = betree_main
test-transp-betree_main:
$(AENEAS_CMD)
# Generic rules to extract the LLBC from a rust file
# We use the rules in Charon's Makefile to generate the .llbc files: the options
# vary with the test files.
.PHONY: gen-llbc-%
gen-llbc-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
gen-llbc-%:
$(CHARON_CMD)
# "p" stands for "Polonius"
.PHONY: gen-llbcp-%
gen-llbcp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
gen-llbcp-%:
$(CHARON_CMD)
# Generic rules to test the translation of an LLBC file.
# Note that the files requiring the Polonius borrow-checker are generated
# in the tests-polonius subdirectory.
.PHONY: trans-%
trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR)
trans-%: FILE = $*
trans-%: gen-llbc-% tfstar-% tcoq-%
echo "# Test $* done"
# "p" stands for "Polonius"
.PHONY: transp-%
transp-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR)
transp-%: FILE = $*
transp-%: gen-llbcp-% tfstarp-%
echo "# Test $* done"
.PHONY: tfstar-%
tfstar-%: OPTIONS += -backend fstar -unfold-monads -test-trans-units
tfstar-%: BACKEND_SUBDIR := fstar
tfstar-%:
$(AENEAS_CMD)
# "p" stands for "Polonius"
.PHONY: tfstarp-%
tfstarp-%: OPTIONS += -backend fstar -unfold-monads -test-trans-units
tfstarp-%: BACKEND_SUBDIR := fstar
tfstarp-%:
$(AENEAS_CMD)
# TODO: -test-trans-units
# It doesn't work on vec_push_fwd, I don't understand why.
.PHONY: tcoq-%
tcoq-%: OPTIONS += -backend coq -decompose-monads
tcoq-%: BACKEND_SUBDIR := coq
tcoq-%:
$(AENEAS_CMD)
# Nix
.PHONY: nix
nix:
nix build .#checks.x86_64-linux.aeneas-tests --show-trace -L
|
