-
Notifications
You must be signed in to change notification settings - Fork 26
Expand file tree
/
Copy pathMakefile
More file actions
373 lines (254 loc) · 9.52 KB
/
Copy pathMakefile
File metadata and controls
373 lines (254 loc) · 9.52 KB
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
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
#NOTE: if you want to add global F* options, you need to do the following:
# 1. Add them to FSTAR_OPTIONS in src/fstar.Makefile
# 2. Add them to fstar_args0 in src/3d/ocaml/Batch.ml
all: package-subset asn1 cbor
.PHONY: all
package-subset: quackyducky lowparse 3d
.PHONY: package-subset
clean_rules += clean-3d clean-lowparse clean-quackyducky clean-cbor-verify clean-cddl clean-bin clean-cose-test clean-asn1 clean-tests clean-3d-tests clean-doc
other_clean_rules += distclean
include nofstar.Makefile
include deps.Makefile
ifneq ($(OS),Windows_NT)
package-subset: cddl
endif
# Disable COSE on MacOS because we don't know how to link with OpenSSL
ifneq ($(OS),Darwin)
all: cose
endif
ifeq (,$(NO_PULSE))
all: cddl cbor-interface
endif
EVERPARSE_SRC_PATH := $(realpath src)
ALREADY_CACHED := *,-LowParse,-EverParse3d,-ASN1,-CBOR,-CDDL,
SRC_DIRS += src/lowparse src/ASN1 src/3d/prelude src/cbor/spec src/cbor/spec/raw src/cbor/spec/raw/everparse src/cddl/spec
ifeq (,$(NO_PULSE))
SRC_DIRS += src/lowparse/pulse src/cbor/pulse src/cbor/pulse/raw src/cbor/pulse/raw/everparse src/cddl/pulse src/cddl/tool
endif
include $(EVERPARSE_SRC_PATH)/karamel.Makefile
ifeq (,$(NO_PULSE))
include $(EVERPARSE_SRC_PATH)/pulse.Makefile
endif
include $(EVERPARSE_SRC_PATH)/common.Makefile
$(FSTAR_DEP_FILE): $(NEED_FSTAR) $(NEED_KRML) $(NEED_PULSE)
$(ALL_CHECKED_FILES): %.checked: $(NEED_FSTAR) $(NEED_Z3) $(NEED_KRML) $(NEED_PULSE)
ifeq (1,$(ADMIT_LOWPARSE))
$(filter src/lowparse/%,$(ALL_CHECKED_FILES)): ADMIT := 1
endif
ifeq (1,$(ADMIT_CBOR_CDDL))
$(filter src/cbor/% src/cddl/%,$(ALL_CHECKED_FILES)): ADMIT := 1
endif
lowparse: $(filter-out src/lowparse/pulse/%,$(filter src/lowparse/%,$(ALL_CHECKED_FILES)))
ifeq (,$(NO_PULSE))
lowparse: $(filter src/lowparse/pulse/%,$(ALL_CHECKED_FILES))
endif
# lowparse needed because of .fst behind .fsti for extraction
3d-prelude-verify: $(filter src/3d/prelude/%,$(ALL_CHECKED_FILES)) $(filter-out src/lowparse/LowParse.SLow.% src/lowparse/pulse/%,$(filter src/lowparse/%,$(ALL_CHECKED_FILES)))
.PHONY: 3d-prelude-verify
3d-prelude: 3d-prelude-verify
+$(MAKE) -C src/3d/prelude
.PHONY: 3d-prelude
3d-exe: $(NEED_Z3)
+$(MAKE) -C src/3d 3d
.PHONY: 3d-exe
3d: 3d-prelude 3d-exe
# filter-out comes from NOT_INCLUDED in src/ASN1/Makefile
asn1: $(filter-out $(addprefix src/ASN1/,$(addsuffix .checked,ASN1.Tmp.fst ASN1.Test.Interpreter.fst ASN1.Low.% ASN1Test.fst ASN1.bak%)),$(filter src/ASN1/%,$(ALL_CHECKED_FILES)))
quackyducky: qd-exe lowparse
qd-exe: $(NEED_OPAM)
+$(MAKE) -C src/qd
.PHONY: qd-exe
lowparse-unit-test: lowparse
+$(MAKE) -C tests/lowparse
3d-unit-test: 3d $(NEED_Z3_TESTGEN)
+$(MAKE) -C src/3d test
3d-doc-test: 3d $(NEED_Z3_TESTGEN)
+$(MAKE) -C doc 3d-test
3d-test: 3d-unit-test 3d-doc-test
asn1-test: asn1
+$(MAKE) -C src/ASN1 test
lowparse-bitfields-test: lowparse
+$(MAKE) -C tests/bitfields
ifeq (,$(NO_PULSE))
lowparse-pulse-test: lowparse
+$(MAKE) -C share/everparse/tests/lowparse
# +$(MAKE) -C tests/pulse # TODO: move it into `share/everparse/tests/lowparse` and re-enable it
else
lowparse-pulse-test:
endif
.PHONY: lowparse-pulse-test
lowparse-test: lowparse-unit-test lowparse-bitfields-test lowparse-pulse-test
quackyducky-lowstar-test: quackyducky
+$(MAKE) -C tests
.PHONY: quackyducky-lowstar-test
quackyducky-pulse-test: quackyducky
+$(MAKE) -C share/everparse/tests/qd
.PHONY: quackyducky-pulse-test
quackyducky-test: quackyducky-lowstar-test quackyducky-pulse-test
test: all lowparse-test quackyducky-test asn1-test cbor-test cddl-test
# Disable 3d-unit-test on MacOS because there is a loop in Makefiles
# Disable 3d-doc-test on MacOS because sphinx is not available
ifneq ($(OS),Darwin)
test: 3d-test
endif
# Disable COSE tests on MacOS because we don't know how to link with OpenSSL
ifneq ($(OS),Darwin)
test: cose-test
endif
submodules:
$(MAKE) -C $(EVERPARSE_OPT_PATH) submodules
.PHONY: submodules
cbor-interface: $(filter-out src/cbor/spec/raw/%,$(filter src/cbor/spec/%,$(ALL_CHECKED_FILES)))
ifeq (,$(NO_PULSE))
cbor-interface: $(filter-out src/cbor/pulse/raw/%,$(filter src/cbor/pulse/%,$(ALL_CHECKED_FILES)))
endif
.PHONY: cbor-interface
ifeq (,$(NO_PULSE))
cbor-det-c-vertest: cbor cbor-interface
+$(MAKE) -C src/cbor/pulse/det/vertest/c
else
cbor-det-c-vertest:
endif
.PHONY: cbor-det-c-vertest
ifeq (,$(NO_PULSE))
cbor-det-common-vertest: cbor cbor-interface
+$(MAKE) -C src/cbor/pulse/det/vertest/common
else
cbor-det-common-vertest:
endif
.PHONY: cbor-det-common-vertest
cbor-verify-aux: $(filter src/cbor/spec/%,$(ALL_CHECKED_FILES))
ifeq (,$(NO_PULSE))
cbor-verify-aux: $(filter src/cbor/pulse/%,$(ALL_CHECKED_FILES))
endif
.PHONY: cbor-verify-aux
# The byte_slice seam (CBOR.Pulse.Raw.Slice) has two backend implementations,
# slice-c and slice-rust, that share a module name and so cannot be checked in a
# single dependency scan; each lives in its own directory with its own Makefile
# (mirroring src/cbor/pulse/raw) and is excluded from SRC_DIRS and the global
# checked-file cache. `cbor-verify` is the full verification rule: cbor-verify-aux
# (the whole CBOR closure, including the shared CBOR.Pulse.Raw.Slice.fsti.checked)
# plus each backend's CBOR.Pulse.Raw.Slice.fst.checked, built by delegating to the
# per-directory Makefile. Delegating lets each slice directory name its own target
# locally (the relative CBOR.Pulse.Raw.Slice.fst.checked) instead of threading its
# absolute path to a sub-make.
#
# Each backend build depends on cbor-verify-aux: the local Makefile checks only the
# backend .fst against the already-built shared .fsti.checked and CBOR closure, so
# that closure must exist first (otherwise, under `make -j`, the local check races
# cbor-verify-aux and fails, e.g. Error 317 "Expected CBOR.Pulse.Raw.Compare.Base
# to be already checked"). Given that ordering the two backends touch only their own
# directories and merely read the up-to-date shared .fsti.checked, so they are
# independent targets and may run in parallel with each other under -j.
ifeq (,$(NO_PULSE))
cbor-verify-slice-c: cbor-verify-aux
+$(MAKE) -C src/cbor/pulse/raw/slice-c
cbor-verify-slice-rust: cbor-verify-aux
+$(MAKE) -C src/cbor/pulse/raw/slice-rust
cbor-verify: cbor-verify-aux cbor-verify-slice-c cbor-verify-slice-rust
else
cbor-verify: cbor-verify-aux
endif
.PHONY: cbor-verify cbor-verify-slice-c cbor-verify-slice-rust
# lowparse needed for extraction because of .fst files behind .fsti
ifeq (,$(NO_PULSE))
cbor-extract-pre: cbor-verify $(filter-out src/lowparse/LowParse.SLow.% src/lowparse/LowParse.Low.%,$(filter src/lowparse/%,$(ALL_CHECKED_FILES)))
.PHONY: cbor-extract-pre
cbor-extract-krml: cbor-extract-pre
+$(MAKE) -C src/cbor extract-krml
.PHONY: cbor-extract-krml
cbor-test-snapshot: cbor-extract-krml
+$(MAKE) -C src/cbor test-snapshot
else
cbor-test-snapshot: cbor-verify
endif
.PHONY: cbor-test-snapshot
# This rule is incompatible with `cbor` and `cbor-test-snapshot`
ifeq (,$(NO_PULSE))
cbor-snapshot: cbor-extract-krml
+$(MAKE) -C src/cbor snapshot
else
cbor-snapshot:
endif
.PHONY: cbor-snapshot
cbor-test-verified: cbor-det-c-vertest cbor-det-common-vertest
.PHONY: cbor-test-verified
cbor-test-extracted: cbor-test-unverified cbor-test-verified
.PHONY: cbor-test-extracted
cbor-test: cbor-test-extracted cbor-test-snapshot
cddl-spec: $(filter src/cddl/spec/%,$(ALL_CHECKED_FILES))
ifeq (,$(NO_PULSE))
cddl-pulse: cddl-spec $(filter src/cddl/pulse/%,$(ALL_CHECKED_FILES))
# cbor-extract-pre needed because Rust extraction extracts CBOR and COSE altogether
cddl-tool: cddl-pulse $(filter src/cddl/tool/%,$(ALL_CHECKED_FILES)) cbor-extract-pre
+$(MAKE) -C src/cddl/tool
else
cddl-tool:
endif
cddl: cbor cbor-interface cddl-spec cddl-tool
.PHONY: cddl-spec cddl-tool
.PHONY: cbor-det-c-test cbor-det-rust-test cbor-test cddl
ifeq (,$(NO_PULSE))
cddl-unit-tests: cddl
+$(MAKE) -C src/cddl test
else
cddl-unit-tests:
endif
.PHONY: cddl-unit-tests
ifeq (,$(NO_PULSE))
cose-extract-krml: cddl-tool
+$(MAKE) -C src/cose extract-krml
cose-extract-test: cose-extract-krml cbor
+$(MAKE) -C src/cose test-extract
# This rule is incompatible with cose-extract-test
cose-snapshot: cose-extract-krml cbor
+$(MAKE) -C src/cose snapshot
else
cose-extract-krml:
cose-extract-test:
cose-snapshot:
endif
.PHONY: cose-extract-krml cose-extract-test cose-snapshot
cose-test: cose-extract-test cose-extracted-test
.PHONY: cose-test
cddl-test: cddl cddl-unit-tests
.PHONY: cddl-test
3d-doc-snapshot: 3d $(NEED_Z3_TESTGEN)
+$(MAKE) -C doc 3d-snapshot
.PHONY: 3d-doc-snapshot
clean-asn1:
+$(MAKE) -C src/ASN1 clean
.PHONY: clean-asn1
clean-3d:
+$(MAKE) -C src/3d clean
clean-lowparse:
+$(MAKE) -C src/lowparse clean
clean-quackyducky:
+$(MAKE) -C src/qd clean
clean-cbor-verify:
+$(MAKE) -C src/cbor clean-verify
clean-cddl:
+$(MAKE) -C src/cddl clean
.PHONY: clean-cbor-verify
clean-bin:
rm -rf bin lib
.PHONY: clean-bin
clean-cose-test:
+$(MAKE) -C src/cose clean-extract
.PHONY: clean-cose-test
clean-tests:
+$(MAKE) -C tests clean
.PHONY: clean-tests
clean-3d-tests:
+$(MAKE) -C src/3d/tests clean
.PHONY: clean-3d-tests
clean-doc:
+$(MAKE) -C doc clean
.PHONY: clean-doc
clean: $(clean_rules)
.PHONY: all gen verify test gen-test clean quackyducky lowparse lowparse-test lowparse-fstar-test package 3d 3d-test lowparse-unit-test lowparse-bitfields-test release everparse 3d-unit-test 3d-doc-test ci clean-3d clean-lowparse clean-quackyducky asn1 asn1-test
release package package-noversion nuget-noversion everparse:
+$(MAKE) -f package.Makefile $@
# For F* testing purposes, cf. FStarLang/FStar@fc30456a163c749843c50ee5f86fa22de7f8ad7a
lowparse-fstar-test:
+$(MAKE) -C src/lowparse fstar-test