diff --git a/.gitignore b/.gitignore index 99f63da1..a006565c 100644 --- a/.gitignore +++ b/.gitignore @@ -12,10 +12,7 @@ tests/src/betree/target #=================== # Generated by dune #=================== -charon-ml/_build -charon-ml/name_matcher_parser/_build -charon/_build -charon/src/_build +_build #=================== # Generated by Charon diff --git a/Makefile b/Makefile index d1b62b0b..f8af4a31 100644 --- a/Makefile +++ b/Makefile @@ -64,7 +64,7 @@ charon-tests: # Run the Charon ML tests on the .ullbc and .llbc files generated by Charon .PHONY: charon-ml-tests -charon-ml-tests: build-charon-ml charon-tests +charon-ml-tests: build-charon-ml cd charon-ml && make tests # Generate some of the ml code automatically from the rust definitions. diff --git a/charon-ml/tests/Tests.ml b/charon-ml/tests/Tests.ml index 9d85127e..2b0a4bd0 100644 --- a/charon-ml/tests/Tests.ml +++ b/charon-ml/tests/Tests.ml @@ -12,8 +12,6 @@ let () = with Not_found -> log#set_level EL.Info (* Call the tests *) -let () = Test_Deserialize.run_tests "../../../tests/serialized" - -let () = - Test_NameMatcher.run_tests - "../../../tests/serialized/ml-name-matcher-tests.llbc" +(* llbc files are copied into the `_build` dir by the `(deps)` rule in `./dune`. *) +let () = Test_Deserialize.run_tests "./serialized" +let () = Test_NameMatcher.run_tests "./serialized/ml-name-matcher-tests.llbc" diff --git a/charon/src/bin/generate-ml/generated b/charon/src/bin/generate-ml/generated deleted file mode 120000 index 23f4fa79..00000000 --- a/charon/src/bin/generate-ml/generated +++ /dev/null @@ -1 +0,0 @@ -../../../../charon-ml/src \ No newline at end of file diff --git a/charon/src/bin/generate-ml/main.rs b/charon/src/bin/generate-ml/main.rs index d36e6588..b1c8c45a 100644 --- a/charon/src/bin/generate-ml/main.rs +++ b/charon/src/bin/generate-ml/main.rs @@ -974,10 +974,19 @@ fn main() -> Result<()> { CrateData::deserialize(deserializer)?.translated }; - generate_ml(crate_data, dir) + let output_dir = if std::env::var("IN_CI").as_deref() == Ok("1") { + dir.join("generated") + } else { + dir.join("../../../../charon-ml/src") + }; + generate_ml(crate_data, dir.join("templates"), output_dir) } -fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Result<()> { +fn generate_ml( + crate_data: TranslatedCrate, + template_dir: PathBuf, + output_dir: PathBuf, +) -> anyhow::Result<()> { let manual_type_impls = &[ // Hand-written because we replace the `FileId` with the corresponding file name. ( @@ -1244,8 +1253,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu #[rustfmt::skip] let generate_code_for = vec![ GenerateCodeFor { - template: output_dir.join("templates/GAst.ml"), - target: output_dir.join("generated/GAst.ml"), + template: template_dir.join("GAst.ml"), + target: output_dir.join("GAst.ml"), markers: ctx.markers_from_names(&[ (GenerationKind::TypeDecl(Some(DeriveVisitors { name: "statement_base", @@ -1275,8 +1284,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu ]), }, GenerateCodeFor { - template: output_dir.join("templates/Expressions.ml"), - target: output_dir.join("generated/Expressions.ml"), + template: template_dir.join("Expressions.ml"), + target: output_dir.join("Expressions.ml"), markers: ctx.markers_from_names(&[ (GenerationKind::TypeDecl(None), &[ "VarId", @@ -1316,8 +1325,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu ]), }, GenerateCodeFor { - template: output_dir.join("templates/Meta.ml"), - target: output_dir.join("generated/Meta.ml"), + template: template_dir.join("Meta.ml"), + target: output_dir.join("Meta.ml"), markers: ctx.markers_from_names(&[ (GenerationKind::TypeDecl(None), &[ "Loc", @@ -1332,8 +1341,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu ]), }, GenerateCodeFor { - template: output_dir.join("templates/Types.ml"), - target: output_dir.join("generated/Types.ml"), + template: template_dir.join("Types.ml"), + target: output_dir.join("Types.ml"), markers: ctx.markers_from_names(&[ (GenerationKind::TypeDecl(None), &[ "ConstGenericVarId", @@ -1420,8 +1429,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu ]), }, GenerateCodeFor { - template: output_dir.join("templates/Values.ml"), - target: output_dir.join("generated/Values.ml"), + template: template_dir.join("Values.ml"), + target: output_dir.join("Values.ml"), markers: ctx.markers_from_names(&[ (GenerationKind::TypeDecl(Some(DeriveVisitors { name: "literal", @@ -1441,8 +1450,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu ]), }, GenerateCodeFor { - template: output_dir.join("templates/LlbcAst.ml"), - target: output_dir.join("generated/LlbcAst.ml"), + template: template_dir.join("LlbcAst.ml"), + target: output_dir.join("LlbcAst.ml"), markers: vec![ (GenerationKind::TypeDecl(Some(DeriveVisitors { name: "statement", @@ -1453,8 +1462,8 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu ], }, GenerateCodeFor { - template: output_dir.join("templates/UllbcAst.ml"), - target: output_dir.join("generated/UllbcAst.ml"), + template: template_dir.join("UllbcAst.ml"), + target: output_dir.join("UllbcAst.ml"), markers: ctx.markers_from_names(&[ (GenerationKind::TypeDecl(Some(DeriveVisitors { name: "statement", @@ -1483,18 +1492,18 @@ fn generate_ml(crate_data: TranslatedCrate, output_dir: PathBuf) -> anyhow::Resu ]), }, GenerateCodeFor { - template: output_dir.join("templates/GAstOfJson.ml"), - target: output_dir.join("generated/GAstOfJson.ml"), + template: template_dir.join("GAstOfJson.ml"), + target: output_dir.join("GAstOfJson.ml"), markers: vec![(GenerationKind::OfJson, gast_types)], }, GenerateCodeFor { - template: output_dir.join("templates/LlbcOfJson.ml"), - target: output_dir.join("generated/LlbcOfJson.ml"), + template: template_dir.join("LlbcOfJson.ml"), + target: output_dir.join("LlbcOfJson.ml"), markers: vec![(GenerationKind::OfJson, llbc_types)], }, GenerateCodeFor { - template: output_dir.join("templates/UllbcOfJson.ml"), - target: output_dir.join("generated/UllbcOfJson.ml"), + template: template_dir.join("UllbcOfJson.ml"), + target: output_dir.join("UllbcOfJson.ml"), markers: vec![(GenerationKind::OfJson, ullbc_types)], }, ]; diff --git a/charon-ml/dune-project b/dune-project similarity index 100% rename from charon-ml/dune-project rename to dune-project diff --git a/flake.nix b/flake.nix index 42a4c422..4eead928 100644 --- a/flake.nix +++ b/flake.nix @@ -24,104 +24,20 @@ craneLib = (crane.mkLib pkgs).overrideToolchain rustToolchain; charon = pkgs.callPackage ./nix/charon.nix { inherit craneLib rustToolchain; }; + charon-ml = pkgs.callPackage ./nix/charon-ml.nix { inherit charon; }; # Check rust files are correctly formatted. charon-check-fmt = charon.passthru.check-fmt; # Check that the crate builds with the "rustc" feature off. charon-check-no-rustc = charon.passthru.check-no-rustc; - - # A utility that extracts the llbc of a crate using charon. This uses - # `crane` to handle dependencies and toolchain management. - extractCrateWithCharon = { name, src, charonFlags ? "", craneExtraArgs ? { } }: - craneLib.buildPackage ({ - inherit name; - src = pkgs.lib.cleanSourceWith { - inherit src; - filter = path: type: (craneLib.filterCargoSources path type); - }; - cargoArtifacts = craneLib.buildDepsOnly { inherit src; }; - buildPhase = '' - ${charon}/bin/charon ${charonFlags} --dest $out/llbc - ''; - dontInstall = true; - } // craneExtraArgs); + # Check ocaml files are correctly formatted. + charon-ml-check-fmt = charon-ml.charon-ml-check-fmt; + # Run ocaml tests + charon-ml-tests = charon-ml.charon-ml-tests; # Runs charon on the whole rustc ui test suite. rustc-tests = pkgs.callPackage ./nix/rustc-tests.nix { inherit charon rustToolchain; }; - ocamlPackages = pkgs.ocamlPackages; - easy_logging = ocamlPackages.buildDunePackage rec { - pname = "easy_logging"; - version = "0.8.2"; - src = pkgs.fetchFromGitHub { - owner = "sapristi"; - repo = "easy_logging"; - rev = "v${version}"; - sha256 = "sha256-Xy6Rfef7r2K8DTok7AYa/9m3ZEV07LlUeMQSRayLBco="; - }; - buildInputs = [ ocamlPackages.calendar ]; - }; - charon-name_matcher_parser = - ocamlPackages.buildDunePackage { - pname = "name_matcher_parser"; - version = "0.1.0"; - duneVersion = "3"; - nativeBuildInputs = with ocamlPackages; [ - menhir - ]; - propagatedBuildInputs = with ocamlPackages; [ - ppx_deriving - visitors - zarith - menhirLib - ]; - src = ./charon-ml; - }; - mk-charon-ml = doCheck: - ocamlPackages.buildDunePackage { - pname = "charon"; - version = "0.1.0"; - duneVersion = "3"; - OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. - preCheck = - if doCheck then '' - mkdir -p tests/serialized - cp ${charon}/tests-llbc/* tests/serialized - '' else - ""; - propagatedBuildInputs = with ocamlPackages; [ - core - ppx_deriving - visitors - easy_logging - zarith - yojson - calendar - charon-name_matcher_parser - ]; - src = ./charon-ml; - inherit doCheck; - }; - charon-ml = mk-charon-ml false; - charon-ml-tests = mk-charon-ml true; - - charon-ml-check-fmt = pkgs.stdenv.mkDerivation { - name = "charon-ml-check-fmt"; - src = ./charon-ml; - buildInputs = [ - ocamlPackages.dune_3 - ocamlPackages.ocaml - ocamlPackages.ocamlformat - ]; - buildPhase = '' - if ! dune build @fmt; then - echo 'ERROR: Ocaml code is not formatted. Run `make format` to format the project files'. - exit 1 - fi - ''; - installPhase = "touch $out"; - }; - # Check that the generated ocaml files match what is committed to the repo. check-generated-ml = pkgs.runCommand "check-generated-ml" { } '' mkdir generated @@ -150,6 +66,22 @@ fi touch $out ''; + + # A utility that extracts the llbc of a crate using charon. This uses + # `crane` to handle dependencies and toolchain management. + extractCrateWithCharon = { name, src, charonFlags ? "", craneExtraArgs ? { } }: + craneLib.buildPackage ({ + inherit name; + src = pkgs.lib.cleanSourceWith { + inherit src; + filter = path: type: (craneLib.filterCargoSources path type); + }; + cargoArtifacts = craneLib.buildDepsOnly { inherit src; }; + buildPhase = '' + ${charon}/bin/charon ${charonFlags} --dest $out/llbc + ''; + dontInstall = true; + } // craneExtraArgs); in { packages = { diff --git a/nix/charon-ml.nix b/nix/charon-ml.nix new file mode 100644 index 00000000..78abfeaa --- /dev/null +++ b/nix/charon-ml.nix @@ -0,0 +1,99 @@ +{ lib +, charon +, fetchFromGitHub +, ocamlPackages +, runCommand +, stdenv +}: +let + easy_logging = ocamlPackages.buildDunePackage rec { + pname = "easy_logging"; + version = "0.8.2"; + src = fetchFromGitHub { + owner = "sapristi"; + repo = "easy_logging"; + rev = "v${version}"; + sha256 = "sha256-Xy6Rfef7r2K8DTok7AYa/9m3ZEV07LlUeMQSRayLBco="; + }; + buildInputs = [ ocamlPackages.calendar ]; + }; + + # We need both `charon-ml` and the `dune-project` file. + src = lib.cleanSourceWith { + src = ./..; + filter = + path: type: + (lib.hasPrefix (toString ../charon-ml) path) + || (lib.hasPrefix (toString ../dune-project) path); + }; + + charon-name_matcher_parser = + ocamlPackages.buildDunePackage { + pname = "name_matcher_parser"; + version = "0.1.0"; + duneVersion = "3"; + inherit src; + + nativeBuildInputs = with ocamlPackages; [ + menhir + ]; + propagatedBuildInputs = with ocamlPackages; [ + ppx_deriving + visitors + zarith + menhirLib + ]; + }; + + charon-ml-check-fmt = stdenv.mkDerivation { + name = "charon-ml-check-fmt"; + inherit src; + + buildInputs = [ + ocamlPackages.dune_3 + ocamlPackages.ocaml + ocamlPackages.ocamlformat + ]; + buildPhase = '' + if ! dune build @fmt; then + echo 'ERROR: Ocaml code is not formatted. Run `make format` to format the project files'. + exit 1 + fi + ''; + installPhase = "touch $out"; + }; + + mk-charon-ml = doCheck: + ocamlPackages.buildDunePackage { + pname = "charon"; + version = "0.1.0"; + duneVersion = "3"; + inherit src; + + OCAMLPARAM = "_,warn-error=+A"; # Turn all warnings into errors. + preCheck = + if doCheck then '' + mkdir -p charon-ml/tests/serialized + cp ${charon}/tests-llbc/* charon-ml/tests/serialized + '' else + ""; + propagatedBuildInputs = with ocamlPackages; [ + core + ppx_deriving + visitors + easy_logging + zarith + yojson + calendar + charon-name_matcher_parser + ]; + inherit doCheck; + + passthru = { inherit charon-ml-tests charon-ml-check-fmt; }; + }; + + charon-ml = mk-charon-ml false; + charon-ml-tests = mk-charon-ml true; + +in +charon-ml diff --git a/nix/charon.nix b/nix/charon.nix index 99d5569a..affad103 100644 --- a/nix/charon.nix +++ b/nix/charon.nix @@ -40,12 +40,6 @@ craneLib.buildPackage ( nativeBuildInputs = lib.optionals (stdenv.isDarwin) [ bintools ]; # It's important to pass the same `RUSTFLAGS` to dependencies otherwise we'll have to rebuild them. cargoArtifacts = craneLib.buildDepsOnly craneArgs; - postPatch = '' - # This directory is a symlink outside of the charon directory. We remove - # it so that we regenerate fresh files in its place. - rm -f src/bin/generate-ml/generated - mkdir src/bin/generate-ml/generated - ''; # Make sure the toolchain is in $PATH so that `cargo` can work # properly. On mac we also have to tell `charon-driver` where to find # the rustc_driver dynamic library; this is done automatically on @@ -63,6 +57,7 @@ craneLib.buildPackage ( checkPhaseCargoCommand = '' CHARON_TOOLCHAIN_IS_IN_PATH=1 IN_CI=1 cargo test --profile release --locked # We also re-generate the ocaml files. + mkdir src/bin/generate-ml/generated CHARON_TOOLCHAIN_IS_IN_PATH=1 IN_CI=1 cargo run --release --locked --bin generate-ml # While running tests we also outputted llbc files. We export them for charon-ml tests.