From 88a2112b3561eff8b6996d740b5c0e1f62c2d9ee Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 10:56:17 +0200 Subject: Format `flake.nix` --- flake.nix | 74 +++++++++++++++++++++++++++++++++------------------------------ 1 file changed, 39 insertions(+), 35 deletions(-) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index 13b8795e..d380170a 100644 --- a/flake.nix +++ b/flake.nix @@ -52,21 +52,22 @@ version = "0.1.0"; duneVersion = "3"; src = ./compiler; - OCAMLPARAM="_,warn-error=+A"; # Turn all warnings into errors. + OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. propagatedBuildInputs = [ - easy_logging charon.packages.${system}.charon-ml - ] ++ (with ocamlPackages; [ - calendar - core_unix - ppx_deriving - visitors - yojson - zarith - ocamlgraph - unionFind - ]); + easy_logging + charon.packages.${system}.charon-ml + ] ++ (with ocamlPackages; [ + calendar + core_unix + ppx_deriving + visitors + yojson + zarith + ocamlgraph + unionFind + ]); afterBuild = '' - echo charon.packages.${system}.tests + echo charon.packages.${system}.tests ''; }; # Run the translation on various files. @@ -119,7 +120,7 @@ name = "aeneas_verify_fstar"; src = ./tests/fstar; FSTAR_EXE = "${hacl-nix.packages.${system}.fstar}/bin/fstar.exe"; - buildPhase= '' + buildPhase = '' make prepare-projects make verify -j $NIX_BUILD_CORES ''; @@ -131,7 +132,7 @@ name = "aeneas_verify_coq"; src = ./tests/coq; buildInputs = [ pkgs.coq ]; - buildPhase= '' + buildPhase = '' make prepare-projects make verify -j $NIX_BUILD_CORES ''; @@ -155,7 +156,7 @@ # || pkgs.lib.hasPrefix (toString ./tests/hol4) path; # }; buildInputs = [ pkgs.hol ]; - buildPhase= '' + buildPhase = '' cd ./tests/hol4 make prepare-projects make verify -j $NIX_BUILD_CORES @@ -164,21 +165,23 @@ installPhase = "touch $out"; }; - check-charon-pin = pkgs.runCommand "aeneas-check-charon-pin" { - buildInputs = [ pkgs.jq ]; - } '' - CHARON_REV_FROM_FLAKE="$(jq -r .nodes.charon.locked.rev ${./flake.lock})" - CHARON_REV_FROM_PIN="$(tail -1 ${./charon-pin})" - if [[ "$CHARON_REV_FROM_FLAKE" != "$CHARON_REV_FROM_PIN" ]]; then - echo 'ERROR: The charon version in `flacke.lock` differs from the one in `charon-pin`.' - echo ' In `flake.lock`: '"$CHARON_REV_FROM_FLAKE" - echo ' In `charon-pin`: '"$CHARON_REV_FROM_PIN" - echo 'Use `make charon-pin` to update the `./charon-pin` file.' - exit 1 - fi - touch $out + check-charon-pin = pkgs.runCommand "aeneas-check-charon-pin" + { + buildInputs = [ pkgs.jq ]; + } '' + CHARON_REV_FROM_FLAKE="$(jq -r .nodes.charon.locked.rev ${./flake.lock})" + CHARON_REV_FROM_PIN="$(tail -1 ${./charon-pin})" + if [[ "$CHARON_REV_FROM_FLAKE" != "$CHARON_REV_FROM_PIN" ]]; then + echo 'ERROR: The charon version in `flacke.lock` differs from the one in `charon-pin`.' + echo ' In `flake.lock`: '"$CHARON_REV_FROM_FLAKE" + echo ' In `charon-pin`: '"$CHARON_REV_FROM_PIN" + echo 'Use `make charon-pin` to update the `./charon-pin` file.' + exit 1 + fi + touch $out ''; - in { + in + { packages = { inherit aeneas; default = aeneas; @@ -198,10 +201,11 @@ }; checks = { inherit aeneas aeneas-tests - aeneas-verify-fstar - aeneas-verify-coq - aeneas-verify-hol4 - aeneas-check-tidiness - check-charon-pin; }; + aeneas-verify-fstar + aeneas-verify-coq + aeneas-verify-hol4 + aeneas-check-tidiness + check-charon-pin; + }; }); } -- cgit v1.2.3 From 6f14e8c699169aa11ea9c106f8cae1ba593569d0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 22 May 2024 15:11:28 +0200 Subject: Add simple test runner --- flake.nix | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index d380170a..7dd2b7c0 100644 --- a/flake.nix +++ b/flake.nix @@ -47,6 +47,7 @@ ''; installPhase = "touch $out"; }; + aeneas = ocamlPackages.buildDunePackage { pname = "aeneas"; version = "0.1.0"; @@ -70,6 +71,15 @@ echo charon.packages.${system}.tests ''; }; + + test_runner = ocamlPackages.buildDunePackage { + pname = "aeneas_test_runner"; + version = "0.1.0"; + duneVersion = "3"; + src = ./tests/test_runner; + OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. + }; + # Run the translation on various files. # Make sure we don't need to recompile the package whenever we make # unnecessary changes - we list the exact files and folders the package @@ -88,9 +98,8 @@ # We need to provide the paths to the Charon tests derivations export CHARON_TEST_DIR=${charon.checks.${system}.tests} - # Copy the Aeneas executable, and update the path to it - cp ${aeneas}/bin/aeneas aeneas - export AENEAS_EXE=./aeneas + export AENEAS_EXE=${aeneas}/bin/aeneas + export TEST_RUNNER_EXE=${test_runner}/bin/test_runner # Copy the tests cp -r tests tests-copy -- cgit v1.2.3 From 4ce3e9c7c11744abae52d7a3ae1a3962395784be Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 10:41:10 +0200 Subject: Import test suite from charon --- flake.nix | 35 ++++++++++++++++++++++++++++++----- 1 file changed, 30 insertions(+), 5 deletions(-) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index 7dd2b7c0..26689af0 100644 --- a/flake.nix +++ b/flake.nix @@ -80,6 +80,32 @@ OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. }; + betree-llbc = charon.extractCrateWithCharon.${system} { + name = "betree"; + src = ./tests/src/betree; + charonFlags = "--polonius --opaque=betree_utils --crate betree_main"; + craneExtraArgs.checkPhaseCargoCommand = '' + cargo rustc -- --test -Zpolonius + ./target/debug/betree + ''; + }; + input-llbcs = pkgs.runCommand "input-llbcs" + { + src = ./tests/src; + makefile = ./Makefile; + buildInputs = [ charon.packages.${system}.rustToolchain charon.packages.${system}.charon ]; + } '' + # Copy the betree output file + mkdir -p $out + cp ${betree-llbc}/llbc/betree_main.llbc $out + + mkdir tests + cp -r $src tests/src + cp $makefile Makefile + # Generate the llbc files + CHARON_EXE="charon" INPUTS_DIR="tests/src" LLBC_DIR="$out" make generate-llbc + ''; + # Run the translation on various files. # Make sure we don't need to recompile the package whenever we make # unnecessary changes - we list the exact files and folders the package @@ -95,9 +121,7 @@ || pkgs.lib.hasPrefix (toString ./tests) path; }; buildPhase = '' - # We need to provide the paths to the Charon tests derivations - export CHARON_TEST_DIR=${charon.checks.${system}.tests} - + export LLBC_DIR=${input-llbcs} export AENEAS_EXE=${aeneas}/bin/aeneas export TEST_RUNNER_EXE=${test_runner}/bin/test_runner @@ -106,8 +130,8 @@ # Run the tests with extra sanity checks enabled # Remark: we could remove the file - make clean-generated - OPTIONS=-checks make test-all -j $NIX_BUILD_CORES + make clean-generated-aeneas + IN_CI=1 make test-all -j $NIX_BUILD_CORES # Check that there are no differences between the generated tests # and the original tests @@ -124,6 +148,7 @@ # something, otherwise Nix will consider the build has failed. installPhase = "touch $out"; }; + # Replay the F* proofs. aeneas-verify-fstar = pkgs.stdenv.mkDerivation { name = "aeneas_verify_fstar"; -- cgit v1.2.3 From 3a380f990d0f202ee19bd163726ff5fc63181ae7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 14:38:50 +0200 Subject: Use runner to generate llbc --- flake.nix | 33 +++++++++++++-------------------- 1 file changed, 13 insertions(+), 20 deletions(-) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index 26689af0..9c918ff9 100644 --- a/flake.nix +++ b/flake.nix @@ -80,6 +80,9 @@ OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. }; + # This test is a full crate with dependencies. We generate the + # corresponding llbc file here; this function takes care of cargo + # dependencies for us. betree-llbc = charon.extractCrateWithCharon.${system} { name = "betree"; src = ./tests/src/betree; @@ -89,22 +92,6 @@ ./target/debug/betree ''; }; - input-llbcs = pkgs.runCommand "input-llbcs" - { - src = ./tests/src; - makefile = ./Makefile; - buildInputs = [ charon.packages.${system}.rustToolchain charon.packages.${system}.charon ]; - } '' - # Copy the betree output file - mkdir -p $out - cp ${betree-llbc}/llbc/betree_main.llbc $out - - mkdir tests - cp -r $src tests/src - cp $makefile Makefile - # Generate the llbc files - CHARON_EXE="charon" INPUTS_DIR="tests/src" LLBC_DIR="$out" make generate-llbc - ''; # Run the translation on various files. # Make sure we don't need to recompile the package whenever we make @@ -118,19 +105,25 @@ path == toString ./Makefile || pkgs.lib.hasPrefix (toString ./compiler) path || pkgs.lib.hasPrefix (toString ./backends) path - || pkgs.lib.hasPrefix (toString ./tests) path; + || (pkgs.lib.hasPrefix (toString ./tests) path + && !pkgs.lib.hasSuffix ".llbc" path); }; + buildInputs = [ charon.packages.${system}.rustToolchain ]; buildPhase = '' - export LLBC_DIR=${input-llbcs} export AENEAS_EXE=${aeneas}/bin/aeneas + export CHARON_EXE=${charon.packages.${system}.charon}/bin/charon export TEST_RUNNER_EXE=${test_runner}/bin/test_runner + mkdir llbc + export LLBC_DIR=llbc + # Copy over the llbc file we can't generate ourselves. + cp ${betree-llbc}/llbc/betree_main.llbc $LLBC_DIR + # Copy the tests cp -r tests tests-copy + make clean-generated-aeneas # Run the tests with extra sanity checks enabled - # Remark: we could remove the file - make clean-generated-aeneas IN_CI=1 make test-all -j $NIX_BUILD_CORES # Check that there are no differences between the generated tests -- cgit v1.2.3 From ca045d57b6cc3fc700efe07bfc257231edf814e5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 May 2024 15:37:01 +0200 Subject: Auto-detect test cases --- flake.nix | 3 +++ 1 file changed, 3 insertions(+) (limited to 'flake.nix') diff --git a/flake.nix b/flake.nix index 9c918ff9..caa29fae 100644 --- a/flake.nix +++ b/flake.nix @@ -78,6 +78,9 @@ duneVersion = "3"; src = ./tests/test_runner; OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. + propagatedBuildInputs = (with ocamlPackages; [ + core_unix + ]); }; # This test is a full crate with dependencies. We generate the -- cgit v1.2.3