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 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 backend sub-directory in which to generate the files
BACKEND_SUBDIR :=
# The directory in which to extract the result of the translation
SUBDIR :=

####################################
# 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-bin-dir
build-bin-dir: build-bin build-lib
	mkdir -p bin
	cp -f compiler/_build/default/main.exe bin/aeneas
	cp -f compiler/_build/default/main.exe bin/aeneas.cmxs
	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-no_nested_borrows test-paper \
	test-hashmap test-hashmap_main \
	test-external test-constants \
	test-polonius_list test-betree_main \
	ctest-test-betree_main \
	test-loops \
	test-arrays test-traits test-bitwise test-demo

.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

# 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 = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest tests/$(BACKEND_SUBDIR)/$(SUBDIR) $(OPTIONS)


# Add specific options to some tests
test-no_nested_borrows test-paper: \
	OPTIONS += -test-trans-units
test-no_nested_borrows test-paper: SUBDIR := misc
tfstar-no_nested_borrows tfstar-paper:
tlean-no_nested_borrows: SUBDIR :=
tlean-paper: SUBDIR :=
thol4-no_nested_borrows: SUBDIR := misc-no_nested_borrows
thol4-paper: SUBDIR := misc-paper

test-arrays: OPTIONS +=
test-arrays: SUBDIR := arrays
tfstar-arrays: OPTIONS += -decreases-clauses -template-clauses -split-files
tcoq-arrays: OPTIONS += -use-fuel
tlean-arrays: SUBDIR :=
tlean-arrays: OPTIONS +=
thol4-arrays: OPTIONS +=

test-traits: OPTIONS +=
test-traits: SUBDIR := traits
tfstar-traits: OPTIONS += -decreases-clauses -template-clauses
tcoq-traits: OPTIONS +=
tlean-traits: SUBDIR :=
tlean-traits: OPTIONS +=
thol4-traits: OPTIONS +=

test-loops: OPTIONS +=
test-loops: SUBDIR := misc
tfstar-loops: OPTIONS += -decreases-clauses -template-clauses -split-files
tcoq-loops: OPTIONS += -use-fuel
tlean-loops: SUBDIR :=
thol4-loops: SUBDIR := misc-loops

test-demo: OPTIONS +=
test-demo: SUBDIR := demo
tfstar-demo: OPTIONS += -use-fuel
tcoq-demo: OPTIONS += -use-fuel
tlean-demo: SUBDIR := Demo
thol4-demo: OPTIONS +=

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

# TODO: reactivate -test-trans-units
test-hashmap_main: OPTIONS += -state -split-files
test-hashmap_main: SUBDIR := hashmap_on_disk
tfstar-hashmap_main: OPTIONS += -decreases-clauses -template-clauses
tcoq-hashmap_main: OPTIONS += -use-fuel
tlean-hashmap_main: SUBDIR :=
thol4-hashmap_main: OPTIONS +=

test-polonius_list: OPTIONS += -test-trans-units
test-polonius_list: SUBDIR := misc
tfstar-polonius_list: OPTIONS +=
tcoq-polonius_list: OPTIONS +=
tlean-polonius_list: SUBDIR :=
tlean-polonius_list: OPTIONS +=
thol4-polonius_list: SUBDIR := misc-polonius_list
thol4-polonius_list: OPTIONS +=

test-constants: OPTIONS += -test-trans-units
test-constants: SUBDIR := misc
tfstar-constants: OPTIONS +=
tcoq-constants: OPTIONS +=
tlean-constants: SUBDIR :=
tlean-constants: OPTIONS +=
thol4-constants: SUBDIR := misc-constants
thol4-constants: OPTIONS +=

test-external: OPTIONS += -test-trans-units -state -split-files
test-external: SUBDIR := misc
tfstar-external: OPTIONS +=
tcoq-external: OPTIONS +=
tlean-external: SUBDIR :=
tlean-external: OPTIONS +=
thol4-external: SUBDIR := misc-external
thol4-external: OPTIONS +=

test-bitwise: OPTIONS += -test-trans-units
test-bitwise: SUBDIR := misc
tfstar-bitwise: OPTIONS +=
tcoq-bitwise: OPTIONS +=
tlean-bitwise: SUBDIR :=
tlean-bitwise: OPTIONS +=
thol4-bitwise: SUBDIR := misc-bitwise
thol4-bitwise: OPTIONS +=

BETREE_FSTAR_OPTIONS = -decreases-clauses -template-clauses
test-betree_main: OPTIONS += -backward-no-state-update -test-trans-units -state -split-files
test-betree_main: SUBDIR:=betree
tfstar-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
tcoq-betree_main: OPTIONS += -use-fuel
tlean-betree_main: SUBDIR :=
tlean-betree_main: OPTIONS +=
thol4-betree_main: OPTIONS +=

# 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: OPTIONS += -backend fstar -test-trans-units -state -split-files
ctest-test-betree_main: OPTIONS += $(BETREE_FSTAR_OPTIONS)
ctest-test-betree_main: BACKEND_SUBDIR := "fstar"
ctest-test-betree_main: SUBDIR:=betree_back_stateful
ctest-test-betree_main: FILE = betree_main
ctest-test-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-%
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-%: OPTIONS += -backend fstar
tfstar-%: BACKEND_SUBDIR := fstar
tfstar-%:
	$(AENEAS_CMD)

.PHONY: tcoq-%
tcoq-%: OPTIONS += -backend coq
tcoq-%: BACKEND_SUBDIR := coq
tcoq-%:
	$(AENEAS_CMD)

.PHONY: tlean-%
tlean-%: OPTIONS += -backend lean
tlean-%: BACKEND_SUBDIR := lean
tlean-%:
	$(AENEAS_CMD)

# TODO: reactivate HOL4 once traits are parameterized by their associated types
.PHONY: thol4-%
thol4-%: OPTIONS += -backend hol4
thol4-%: BACKEND_SUBDIR := hol4
thol4-%:
	echo Ignoring the $* test for HOL4

#thol4-%:
#	$(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