blob: 1d6d4b7d80c7c139f0dc413d89041231627827b7 (
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
|
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
all: build-tests-verify
CHARON_HOME = ../charon
CHARON_EXEC = $(CHARON_HOME)/charon
DEST_DIR = tests
# We use those variables, whose definition depends on the rule we apply
CHARON_TESTS_DIR =
CHARON_OPTIONS =
CHARON_TESTS_SRC =
AENEAS_DRIVER = driver.exe
# The user can specify additional translation options for Aeneas:
OPTIONS += -unfold-monads
# Default translation options:
# - insert calls to the normalizer in the translated code to test the
# generated unit functions
TRANS_OPTIONS := -test-trans-units $(OPTIONS)
SUBDIR :=
# 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 doc
.PHONY: build-driver
build-driver:
cd compiler && dune build $(AENEAS_DRIVER)
.PHONY: build-lib
build-lib:
cd compiler && dune build aeneas.cmxs
.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: build trans-no_nested_borrows trans-paper \
trans-hashmap trans-hashmap_main \
trans-external trans-constants \
trans-polonius-betree_polonius trans-polonius-betree_main \
test-trans-polonius-betree_main
# Verify the F* files generated by the translation
.PHONY: verify
verify: build tests
cd tests && $(MAKE) all
# Reformat the project
.PHONY: format
format:
cd compiler && dune promote
# The commands to run Charon to generate the .llbc files
CHARON_CMD = cd $(CHARON_HOME)/$(CHARON_TEST_SUBFOLDER) && NOT_ALL_TESTS=1 $(MAKE) test-$*
# The command to run Aeneas on the proper llbc file
AENEAS_CMD = cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DIR)/$(FILE).llbc -dest ../$(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS)
# Add specific options to some tests
trans-no_nested_borrows trans-paper: \
TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
trans-no_nested_borrows trans-paper: SUBDIR:=misc
trans-hashmap: TRANS_OPTIONS += -template-clauses -no-state
trans-hashmap: SUBDIR:=hashmap
trans-hashmap_main: TRANS_OPTIONS += -template-clauses
trans-hashmap_main: SUBDIR:=hashmap_on_disk
trans-polonius-betree_polonius: TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
trans-polonius-betree_polonius: SUBDIR:=misc
trans-constants: TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses
trans-constants: SUBDIR:=misc
trans-external: TRANS_OPTIONS +=
trans-external: SUBDIR:=misc
BETREE_OPTIONS = -template-clauses
trans-polonius-betree_main: TRANS_OPTIONS += $(BETREE_OPTIONS) -backward-no-state-update
trans-polonius-betree_main: SUBDIR:=betree
# Additional test on the betree: translate it without `-backward-no-state-update`.
# This generates very ugly code, but is good to test the translation.
test-trans-polonius-betree_main: trans-polonius-betree_main
test-trans-polonius-betree_main: TRANS_OPTIONS += $(BETREE_OPTIONS)
test-trans-polonius-betree_main: SUBDIR:=betree_back_stateful
test-trans-polonius-betree_main: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
test-trans-polonius-betree_main: FILE = betree_main
test-trans-polonius-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-polonius-%
gen-llbc-polonius-%: CHARON_TEST_SUBFOLDER = tests-polonius
gen-llbc-polonius-%: build
$(CHARON_CMD)
.PHONY: gen-llbc-%
gen-llbc-%: CHARON_TEST_SUBFOLDER = tests
gen-llbc-%: build
$(CHARON_CMD)
# Generic rule 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_TESTS_DIR = $(CHARON_HOME)/tests/llbc
trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc
trans-polonius-%: FILE = $*
trans-polonius-%: gen-llbc-polonius-%
$(AENEAS_CMD)
trans-%: FILE = $*
trans-%: gen-llbc-%
$(AENEAS_CMD)
|
