charon/Makefile at main · maximebuyse/charon · GitHub

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
.PHONY: all
all: build

.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 test --no-run
	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

# Generate documentation
.PHONY: doc
doc:
	cd charon && $(MAKE) doc
	cd charon-ml && $(MAKE) doc

# Build and run the tests
.PHONY: test
test: charon-ml/src/CharonVersion.ml clean-generated build-dev charon-tests charon-ml-tests

# Run Charon on various test files
.PHONY: charon-tests
charon-tests:
	cd charon && $(MAKE) test-noclippy

.PHONY: clippy
clippy:
	cd charon && $(MAKE) clippy

# Run the Charon ML tests on the .ullbc and .llbc files generated by Charon
.PHONY: charon-ml-tests
charon-ml-tests: build-charon-ml
	cd charon-ml && $(MAKE) tests

# Debug the ocaml tests in `ocamldebug`
.PHONY: debug-ml-tests
debug-ml-tests: build-charon-ml charon-tests
	cd charon-ml && $(MAKE) copy-tests
	rlwrap ocamldebug -cd _build/default/charon-ml/tests/ Tests.bc

# Generate some of the ml code automatically from the rust definitions.
.PHONY: generate-ml
generate-ml:
	cd charon && cargo build --release && cargo run --release --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

.PHONY: toolchain-commit
toolchain-commit:
	@rustc -vV | awk '/^commit-hash/ { print $$2 }'

# 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-summary

# 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 && cargo clean
	cd charon/macros && cargo clean
	dune 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