forked from AeneasVerif/charon
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Makefile
118 lines (96 loc) · 3.26 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
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-charon-rust
.PHONY: all
all: build test nix
.PHONY: format
format:
cd charon && $(MAKE) format
cd charon-ml && $(MAKE) format
# Take the version written in `Cargo.toml` and export it to a ml variable, so
# that charon-ml can error if it is ever given a llbc file with an incompatible
# version.
charon-ml/src/CharonVersion.ml: charon/Cargo.toml
echo '(* This is an automatically generated file, generated from `charon/Cargo.toml`. *)' > "$@"
echo '(* To re-generate this file, rune `make` in the root directory *)' >> "$@"
printf 'let supported_charon_version = ' >> "$@"
grep '^version =' charon/Cargo.toml | head -1 | sed 's/^version = \(".*"\)/\1/' >> "$@"
# Build the project in release mode, after formatting the code
.PHONY: build
build: build-charon-rust build-charon-ml
# Build in debug mode, without formatting the code
.PHONY: build-dev
build-dev: build-dev-charon-rust build-dev-charon-ml
.PHONY: build-charon-rust
build-charon-rust:
cd charon && $(MAKE)
mkdir -p bin
cp -f charon/target/release/charon bin
cp -f charon/target/release/charon-driver bin
.PHONY: build-dev-charon-rust
build-dev-charon-rust:
cd charon && cargo build
mkdir -p bin
cp -f charon/target/debug/charon bin
cp -f charon/target/debug/charon-driver bin
.PHONY: build-charon-ml
build-charon-ml: charon-ml/src/CharonVersion.ml
cd charon-ml && $(MAKE)
.PHONY: build-dev-charon-ml
build-dev-charon-ml: charon-ml/src/CharonVersion.ml
cd charon-ml && $(MAKE) build-dev
# Build and run the tests
.PHONY: test
test: build-dev charon-tests charon-ml-tests
# Run Charon on various test files
.PHONY: charon-tests
charon-tests:
cd charon && make test
# Run the Charon ML tests on the .ullbc and .llbc files generated by Charon
.PHONY: charon-ml-tests
charon-ml-tests: build-charon-ml charon-tests
cd charon-ml && make tests
# Generate some of the ml code automatically from the rust definitions.
.PHONY: generate-ml
generate-ml:
cd charon && cargo run --bin generate-ml
cd charon-ml && make format 2> /dev/null
# Same as `generate-ml` but don't re-run charon on itself. Useful when developping.
.PHONY: generate-ml-keep-llbc
generate-ml-keep-llbc:
CHARON_ML_REUSE_LLBC=1 $(MAKE) generate-ml
# Run Charon on rustc's ui test suite
.PHONY: rustc-tests
rustc-tests:
nix build -L '.#rustc-tests'
@echo "Summary of the results:"
@cat result/charon-results | cut -d' ' -f 2 | sort | uniq -c
# Prints a summary of the most common test errors.
.PHONY: analyze-rustc-tests
analyze-rustc-tests: rustc-tests
find result/ -name '*.charon-output' \
| xargs cat \
| grep '^error: ' \
| sed 's/^error: \([^:]*\).*/\1/' \
| grep -v 'aborting due to .* error' \
| sort | uniq -c | sort -h
.PHONY: clean-generated
clean-generated:
cd charon && make clean-generated
.PHONY: clean
clean: clean-generated
cd charon/attributes && cargo clean
cd charon && cargo clean
cd charon/macros && cargo clean
# Build the Nix packages
.PHONY: nix
nix: nix-charon nix-ml
.PHONY: nix-charon
nix-charon:
nix build .#packages.x86_64-linux.charon --show-trace -L
.PHONY: nix-ml
nix-ml:
nix build .#checks.x86_64-linux.charon-ml-tests --show-trace -L