diff options
| -rw-r--r-- | Makefile | 92 | ||||
| -rw-r--r-- | README.md | 6 | ||||
| -rw-r--r-- | compiler/Driver.ml | 7 | ||||
| -rw-r--r-- | flake.nix | 29 | ||||
| -rw-r--r-- | fstar/Primitives.fst (renamed from compiler/fstar/Primitives.fst) | 0 |
5 files changed, 101 insertions, 33 deletions
@@ -3,27 +3,51 @@ ifeq (3.81,$(MAKE_VERSION)) install make, then invoke gmake instead of make) endif -all: build-tests-verify +all: build -CHARON_HOME = ../charon -DEST_DIR = tests +#################################### +# Variables customizable by the user +#################################### -# We use those variables, whose definition depends on the rule we apply -CHARON_TESTS_DIR = -CHARON_OPTIONS = -CHARON_TESTS_SRC = +# 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 paths to the test directories in Charon (Aeneas will look for the .llbc +# files in there). +CHARON_TESTS_REGULAR_DIR ?= $(CHARON_HOME)/tests +CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius AENEAS_DRIVER = driver.exe -# The user can specify additional translation options for Aeneas: -OPTIONS += -unfold-monads +# The path to the Aeneas executable to run the tests - we need the ability to +# change this path for the Nix package. +AENEAS_EXE ?= compiler/_build/default/$(AENEAS_DRIVER) -# Default translation options: +# The user can specify additional translation options for Aeneas. +# By default we do: +# - unfold all the monadic let bindings to matches (required by F*) # - insert calls to the normalizer in the translated code to test the # generated unit functions -TRANS_OPTIONS := -test-trans-units $(OPTIONS) +OPTIONS += -unfold-monads -test-trans-units + +# +# The rules use (and update) the following variables +# +# The Charon test directory where to look for the .llbc files +CHARON_TEST_DIR = +# The options with which to call Charon +CHARON_OPTIONS = +# The directory in which to extract the result of the translation SUBDIR := +#################################### +# The rules +#################################### + # Build the project, test it and verify the generated files .PHONY: build-test-verify build-tests-verify: build tests verify @@ -50,7 +74,7 @@ clean: # Test the project by translating test files to F* .PHONY: tests -tests: build trans-no_nested_borrows trans-paper \ +tests: trans-no_nested_borrows trans-paper \ trans-hashmap trans-hashmap_main \ trans-external trans-constants \ trans-polonius-betree_polonius trans-polonius-betree_main \ @@ -67,41 +91,45 @@ format: cd compiler && dune promote # The commands to run Charon to generate the .llbc files -CHARON_CMD = cd $(CHARON_HOME)/$(CHARON_TEST_SUBFOLDER) && NOT_ALL_TESTS=1 $(MAKE) test-$* +ifeq (, $(REGEN_LLBC)) +else +CHARON_CMD = cd $(CHARON_TEST_DIR) && NOT_ALL_TESTS=1 $(MAKE) test-$* +endif # The command to run Aeneas on the proper llbc file -AENEAS_CMD = cd compiler && dune exec -- ./$(AENEAS_DRIVER) ../$(CHARON_TESTS_DIR)/$(FILE).llbc -dest ../$(DEST_DIR)/$(SUBDIR) $(TRANS_OPTIONS) +AENEAS_CMD = $(AENEAS_EXE) $(CHARON_TEST_DIR)/llbc/$(FILE).llbc -dest ../tests/$(SUBDIR) $(OPTIONS) + # Add specific options to some tests trans-no_nested_borrows trans-paper: \ - TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses + OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses trans-no_nested_borrows trans-paper: SUBDIR:=misc -trans-hashmap: TRANS_OPTIONS += -template-clauses -no-state +trans-hashmap: OPTIONS += -template-clauses -no-state trans-hashmap: SUBDIR:=hashmap -trans-hashmap_main: TRANS_OPTIONS += -template-clauses +trans-hashmap_main: OPTIONS += -template-clauses trans-hashmap_main: SUBDIR:=hashmap_on_disk -trans-polonius-betree_polonius: TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses +trans-polonius-betree_polonius: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses trans-polonius-betree_polonius: SUBDIR:=misc -trans-constants: TRANS_OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses +trans-constants: OPTIONS += -test-units -test-trans-units -no-split-files -no-state -no-decreases-clauses trans-constants: SUBDIR:=misc -trans-external: TRANS_OPTIONS += +trans-external: OPTIONS += trans-external: SUBDIR:=misc BETREE_OPTIONS = -template-clauses -trans-polonius-betree_main: TRANS_OPTIONS += $(BETREE_OPTIONS) -backward-no-state-update +trans-polonius-betree_main: OPTIONS += $(BETREE_OPTIONS) -backward-no-state-update trans-polonius-betree_main: SUBDIR:=betree # Additional test on the betree: translate it without `-backward-no-state-update`. # This generates very ugly code, but is good to test the translation. test-trans-polonius-betree_main: trans-polonius-betree_main -test-trans-polonius-betree_main: TRANS_OPTIONS += $(BETREE_OPTIONS) +test-trans-polonius-betree_main: OPTIONS += $(BETREE_OPTIONS) test-trans-polonius-betree_main: SUBDIR:=betree_back_stateful -test-trans-polonius-betree_main: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc +test-trans-polonius-betree_main: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) test-trans-polonius-betree_main: FILE = betree_main test-trans-polonius-betree_main: $(AENEAS_CMD) @@ -110,21 +138,22 @@ test-trans-polonius-betree_main: # We use the rules in Charon's Makefile to generate the .llbc files: the options # vary with the test files. .PHONY: gen-llbc-polonius-% -gen-llbc-polonius-%: CHARON_TEST_SUBFOLDER = tests-polonius -gen-llbc-polonius-%: build +gen-llbc-polonius-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) +gen-llbc-polonius-%: $(CHARON_CMD) .PHONY: gen-llbc-% -gen-llbc-%: CHARON_TEST_SUBFOLDER = tests -gen-llbc-%: build +gen-llbc-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) +gen-llbc-%: $(CHARON_CMD) # Generic rule to test the translation of an LLBC file. # Note that the files requiring the Polonius borrow-checker are generated # in the tests-polonius subdirectory. .PHONY: trans-% -trans-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests/llbc -trans-polonius-%: CHARON_TESTS_DIR = $(CHARON_HOME)/tests-polonius/llbc +trans-%: +trans-polonius-%: CHARON_TEST_DIR = $(CHARON_TESTS_POLONIUS_DIR) +trans-%: CHARON_TEST_DIR = $(CHARON_TESTS_REGULAR_DIR) trans-polonius-%: FILE = $* trans-polonius-%: gen-llbc-polonius-% @@ -133,3 +162,8 @@ trans-polonius-%: gen-llbc-polonius-% trans-%: FILE = $* trans-%: gen-llbc-% $(AENEAS_CMD) + +# Nix +.PHONY: nix +nix: + nix build .#checks.x86_64-linux.aeneas-tests --show-trace -L @@ -63,6 +63,12 @@ if [ -e charon ]; then echo "valid"; else echo "invalid"; fi Finally, building the project simply requires to run `make` in the top directory. +You can also use `make tests` and `make verify` to run the tests, and check +the generated files. As `make tests` will run tests which use the Charon tests, +you will need to regenerate the `.llbc` files. You have the following options: +- run `make tests` in the Charon repository +- run `REGEN_LLBC=1 make tests` in the Aeneas repository + ## Documentation If you run `make`, you will generate a documentation accessible from [`doc.html`](./doc.html). diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 304d0f2f..3059ec2f 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -140,17 +140,18 @@ let () = pure_micro_passes_log#set_level EL.Info; pure_to_extract_log#set_level EL.Info; translate_log#set_level EL.Info; + let log = main_log in (* Load the module *) let json = Yojson.Basic.from_file filename in match crate_of_json json with | Error s -> - main_log#error "error: %s\n" s; + log#error "error: %s\n" s; exit 1 | Ok m -> (* Logging *) - main_log#linfo (lazy ("Imported: " ^ filename)); - main_log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n")); + log#linfo (lazy ("Imported: " ^ filename)); + log#ldebug (lazy ("\n" ^ Print.Crate.crate_to_string m ^ "\n")); (* Apply the pre-passes *) let m = PrePasses.apply_passes m in @@ -26,7 +26,7 @@ aeneas = ocamlPackages.buildDunePackage { pname = "aeneas"; version = "0.1.0"; - src = ./.; + src = ./compiler; buildInputs = [ easy_logging charon.packages.${system}.charon-ml ] ++ (with ocamlPackages; [ calendar @@ -36,11 +36,38 @@ yojson zarith ]); + afterBuild = '' + echo charon.packages.${system}.tests + ''; + }; + # Make sure we don't need to recompile the package whenever we make + # unnecessary changes - we list the exact files and folders the package + # depends upon. + aeneas-tests = pkgs.stdenv.mkDerivation { + name = "aeneas_tests"; + src = pkgs.lib.cleanSourceWith { + src = ./.; + filter = path: type: + path == toString ./Makefile + || pkgs.lib.hasPrefix (toString ./compiler) path + || pkgs.lib.hasPrefix (toString ./fstar) path + || pkgs.lib.hasPrefix (toString ./tests) path; + }; + buildPhase = '' + export CHARON_TESTS_REGULAR_DIR=${charon.checks.${system}.tests} + export CHARON_TESTS_POLONIUS_DIR=${charon.checks.${system}.tests-polonius} + export AENEAS_EXE=${aeneas}/bin/aeneas_driver + + make tests + ''; + installPhase = "touch $out"; }; in { packages = { inherit aeneas; default = aeneas; }; + checks = { inherit aeneas aeneas-tests; }; + hydraJobs = { inherit aeneas aeneas-tests; }; }); } diff --git a/compiler/fstar/Primitives.fst b/fstar/Primitives.fst index 96138e46..96138e46 100644 --- a/compiler/fstar/Primitives.fst +++ b/fstar/Primitives.fst |