path: root/Makefile

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-tests-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 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

# The path to our test runner.
TEST_RUNNER_EXE ?= bin/test_runner

# The user can specify additional translation options for Aeneas.
# By default we activate the (expensive) sanity checks.
OPTIONS ?=

# The rules use (and update) the following variables
#
# The Charon test directory where to look for the .llbc files
CHARON_TEST_DIR ?= $(CHARON_HOME)/tests
# The options with which to call Charon
CHARON_OPTIONS =

####################################
# The rules
####################################

# Build the compiler, after formatting the code
.PHONY: build
build: format build-dev

# Build the project, test it and verify the generated files
.PHONY: build-test-verify
build-test-verify: build test verify

# Build the project, without formatting the code
.PHONY: build-dev
build-dev: build-bin build-lib build-bin-dir doc

.PHONY: build-bin
build-bin: check-charon
	cd compiler && dune build

.PHONY: build-lib
build-lib: check-charon
	cd compiler && dune build aeneas.cmxs

.PHONY: build-runner
build-runner: check-charon
	cd tests/test_runner && dune build

.PHONY: build-bin-dir
build-bin-dir: build-bin build-lib build-runner
	mkdir -p bin
	cp -f compiler/_build/default/main.exe bin/aeneas
	cp -f compiler/_build/default/main.exe bin/aeneas.cmxs
	cp -f tests/test_runner/_build/default/run_test.exe bin/test_runner
	mkdir -p bin/backends/fstar
	mkdir -p bin/backends/coq
	cp -rf backends/fstar/*.fst* bin/backends/fstar/
	cp -rf backends/coq/*.v bin/backends/coq/

.PHONY: doc
doc:
	cd compiler && dune build @doc

# Fetches the latest commit from charon and updates `flake.lock` accordingly.
.PHONY: update-charon-pin
update-charon-pin:
	nix flake lock --update-input charon
	$(MAKE) charon-pin

# Keep the commit revision in `./charon-pin` as well so that non-nix users can
# know which commit to use.
./charon-pin: flake.lock
	nix-shell -p jq --run './scripts/update-charon-pin.sh' >> ./charon-pin

# Checks that `./charon` contains a clone of charon at the required commit.
# Also checks that `./charon/bin/charon` exists.
.PHONY: check-charon
check-charon:
	@echo "Checking the charon installation"
	@./scripts/check-charon-install.sh

# Sets up the charon repository on the right commit.
.PHONY: setup-charon
setup-charon:
	@./scripts/check-charon-install.sh --force


.PHONY: clean
clean: clean-generated
	cd compiler && dune clean

# Test the project by translating test files to F*
.PHONY: test
test: build-dev test-all

.PHONY: test-all
test-all: \
	test-arrays \
	test-betree_main \
	ctest-test-betree_main \
	test-bitwise \
	test-constants \
	test-demo \
	test-external \
	test-hashmap \
	test-hashmap_main \
	test-loops \
	test-no_nested_borrows \
	test-paper \
	test-polonius_list \
	test-traits

.PHONY: clean-generated
clean-generated:
	# We can't put this line in `tests/Makefile` otherwise it will detect itself.
	# FIXME: generation of hol4 files is deactivated so we don't delete those.
	grep -lR 'THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS' tests | grep -v '^tests/hol4' | xargs rm

# Verify the F* files generated by the translation
.PHONY: verify
verify:
	cd tests && $(MAKE) all

# Reformat the project
.PHONY: format
format:
	@# `|| `true` because the command returns an error if it changed anything, which we don't care about.
	cd compiler && dune fmt || true
	cd tests/test_runner && dune fmt || true

# The commands to run Charon to generate the .llbc files
ifeq (, $(REGEN_LLBC))
else
CHARON_CMD = cd $(CHARON_TEST_DIR) && $(MAKE) test-$*
endif

# The command to run Aeneas on the proper llbc file
AENEAS_CMD = $(TEST_RUNNER_EXE) $(AENEAS_EXE) $(CHARON_TEST_DIR) $(FILE) $(BACKEND) $(OPTIONS)

# Add specific options to some tests
# TODO: reactivate -test-trans-units for hashmap and hashmap_main
tfstar-arrays: OPTIONS += -decreases-clauses -template-clauses -split-files
tcoq-arrays: OPTIONS += -use-fuel

test-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
tfstar-betree_main: OPTIONS += -decreases-clauses -template-clauses
tcoq-betree_main: OPTIONS += -use-fuel

ctest-test-betree_main: OPTIONS += -test-trans-units -state -split-files
ctest-test-betree_main: OPTIONS += -decreases-clauses -template-clauses

test-bitwise: OPTIONS += -test-trans-units

test-constants: OPTIONS += -test-trans-units

tfstar-demo: OPTIONS += -use-fuel
tcoq-demo: OPTIONS += -use-fuel

test-external: OPTIONS += -test-trans-units -state -split-files

test-hashmap: OPTIONS += -split-files
tfstar-hashmap: OPTIONS += -decreases-clauses -template-clauses
tcoq-hashmap: OPTIONS += -use-fuel
tlean-hashmap: OPTIONS += -no-gen-lib-entry # We add a custom import in the Hashmap.lean file: we do not want to overwrite it

test-hashmap_main: OPTIONS += -state -split-files
tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
tcoq-hashmap_main: OPTIONS += -use-fuel

tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files
tcoq-loops: OPTIONS += -use-fuel

test-no_nested_borrows: OPTIONS += -test-trans-units

test-paper: OPTIONS += -test-trans-units

test-polonius_list: OPTIONS += -test-trans-units

tfstar-traits: OPTIONS += -decreases-clauses -template-clauses

# 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_CMD)

# Generic rules to test the translation of an LLBC file.
.PHONY: test-%
test-%: FILE = $*
test-%: gen-llbc-% tfstar-% tcoq-% tlean-% thol4-%
	echo "# Test $* done"

.PHONY: tfstar-%
tfstar-%: BACKEND := fstar
tfstar-%:
	$(AENEAS_CMD)

.PHONY: tcoq-%
tcoq-%: BACKEND := coq
tcoq-%:
	$(AENEAS_CMD)

.PHONY: tlean-%
tlean-%: BACKEND := lean
tlean-%:
	$(AENEAS_CMD)

# TODO: reactivate HOL4 once traits are parameterized by their associated types
.PHONY: thol4-%
thol4-%: BACKEND := hol4
thol4-%:
	echo Ignoring the $* test for HOL4
#	$(AENEAS_CMD)

# Additional, *c*ustom test on the betree: translate it without `-backward-no-state-update`.
# This generates very ugly code, but is good to test the translation.
.PHONY: ctest-test-betree_main
ctest-test-betree_main: test-betree_main
ctest-test-betree_main: FILE = betree_main-special
ctest-test-betree_main: BACKEND := fstar
ctest-test-betree_main:
	$(AENEAS_CMD)

# Nix - TODO: add the lean tests
.PHONY: nix
nix:
	nix build && nix flake check

.PHONY: nix-aeneas-tests
nix-aeneas-tests:
	nix build .#checks.x86_64-linux.aeneas-tests --show-trace -L

.PHONY: nix-aeneas-verify-fstar
nix-aeneas-verify-fstar:
	nix build .#checks.x86_64-linux.aeneas-verify-fstar --show-trace -L

.PHONY: nix-aeneas-verify-fstar-split
nix-aeneas-verify-fstar-split:
	nix build .#checks.x86_64-linux.aeneas-verify-fstar-split --show-trace -L

.PHONY: nix-aeneas-verify-coq
nix-aeneas-verify-coq:
	nix build .#checks.x86_64-linux.aeneas-verify-coq --show-trace -L

.PHONY: nix-aeneas-verify-lean
nix-aeneas-verify-lean:
	nix build .#checks.x86_64-linux.aeneas-verify-lean --show-trace -L

.PHONY: nix-aeneas-verify-hol4
nix-aeneas-verify-hol4:
	nix build .#checks.x86_64-linux.aeneas-verify-hol4 --show-trace -L