Merge pull request #428 from hacspec/generalize-names-rs

Engine: generalize `names.rs` into a crate
cryspen · Jan 15, 2024 · f57c322 · f57c322
2 parents dde8c0f + c65f9b8
commit f57c322
Show file tree

Hide file tree

Showing 21 changed files with 424 additions and 78 deletions.
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -28,4 +28,4 @@ jobs:
       - uses: Swatinem/rust-cache@v2
 
       - name: Test
-        run: cargo test --workspace --verbose
+        run: cargo test --workspace --exclude hax-engine-names-extract --verbose
diff --git a/.utils/rebuild.sh b/.utils/rebuild.sh
@@ -31,7 +31,7 @@ cd_rootwise () {
 
 rust () {
     cd_rootwise "cli"
-    for i in driver subcommands; do
+    for i in driver subcommands ../engine/names/extract; do
         CURRENT="rust/$i"
         cargo install --quiet $OFFLINE_FLAG --debug --path $i
     done

diff --git a/Cargo.lock b/Cargo.lock
diff --git a/Cargo.toml b/Cargo.toml
@@ -14,9 +14,29 @@ members = [
      "hax-lib-macros",
      "hax-lib-macros/types",
      "hax-lib-protocol",
-     "hax-lib-protocol-macros"
+     "hax-lib-protocol-macros",
+     "engine/names",
+     "engine/names/extract",
 ]
 exclude = ["tests"]
+default-members = [
+     "frontend/exporter",
+     "frontend/exporter/options",
+     "frontend/diagnostics",
+     "frontend/lint",
+     "cli/options",
+     "cli/options/engine",
+     "cli/subcommands",
+     "cli/driver",
+     "test-harness",
+     "engine/utils/phase-debug-webapp",
+     "hax-lib",
+     "hax-lib-macros",
+     "hax-lib-macros/types",
+     "hax-lib-protocol",
+     "hax-lib-protocol-macros",
+     "engine/names",
+]
 resolver = "2"
 
 [workspace.package]
@@ -67,3 +87,4 @@ hax-diagnostics = { path = "frontend/diagnostics", version = "=0.1.0-pre.1" }
 hax-lint = { path = "frontend/lint", version = "=0.1.0-pre.1" }
 hax-phase-debug-webapp = { path = "engine/utils/phase-debug-webapp", version = "=0.1.0-pre.1" }
 hax-lib-macros-types = { path = "hax-lib-macros/types", version = "=0.1.0-pre.1" }
+hax-engine-names = { path = "engine/names", version = "=0.1.0-pre.1" }
diff --git a/cli/default.nix b/cli/default.nix
@@ -40,10 +40,13 @@
     // {
       pname = pname;
     });
-  hax = craneLib.buildPackage (commonArgs
+  hax = craneLib.buildPackage (
+    commonArgs
     // {
       inherit cargoArtifacts pname;
-    });
+      doInstallCargoArtifacts = true;
+    }
+  );
   frontend-docs = craneLib.cargoDoc (commonArgs // {inherit cargoArtifacts pname;});
   docs = stdenv.mkDerivation {
     name = "hax-docs";
@@ -103,6 +106,20 @@ in
     meta.mainProgram = "cargo-hax";
     passthru = {
       unwrapped = hax;
+      hax-engine-names-extract = craneLib.buildPackage (
+        commonArgs
+        // {
+          pname = "hax_engine_names_extract";
+          cargoLock = ../Cargo.lock;
+          cargoToml = ../engine/names/extract/Cargo.toml;
+          cargoArtifacts = hax;
+          nativeBuildInputs = [hax];
+          postUnpack = ''
+            cd $sourceRoot/engine/names/extract
+            sourceRoot="."
+          '';
+        }
+      );
       engine-docs = hax-engine.docs;
       inherit tests docs frontend-docs;
     };

diff --git a/cli/options/src/lib.rs b/cli/options/src/lib.rs
@@ -275,7 +275,8 @@ pub enum ExporterCommand {
         output_file: PathOrDash,
         /// Whether the bodies are exported as THIR, built MIR, const
         /// MIR, or a combination. Repeat this option to extract a
-        /// combination (e.g. `-k thir -k mir-built`).
+        /// combination (e.g. `-k thir -k mir-built`). Pass `--kind`
+        /// alone with no value to disable body extraction.
         #[arg(
             value_enum,
             short,

diff --git a/engine/bin/lib.ml b/engine/bin/lib.ml
@@ -62,7 +62,8 @@ let run (options : Types.engine_options) : Types.output =
       (module M : Backend.T with type BackendOptions.t = options_type)
       (backend_options : options_type) : Types.file list =
     let open M in
-    Concrete_ident.ImplInfoStore.init options.impl_infos;
+    Concrete_ident.ImplInfoStore.init
+      (Concrete_ident_generated.impl_infos @ options.impl_infos);
     let include_clauses =
       options.backend.translation_options.include_namespaces
     in

diff --git a/engine/default.nix b/engine/default.nix
@@ -2,6 +2,7 @@
   ocamlPackages,
   fetchzip,
   hax-rust-frontend,
+  hax-engine-names-extract,
   rustc,
   nodejs,
   jq,
@@ -81,6 +82,7 @@
     nativeBuildInputs = [
       rustc
       hax-rust-frontend
+      hax-engine-names-extract
       nodejs
       ocamlPackages.js_of_ocaml-compiler
       jq
@@ -89,9 +91,11 @@
     passthru = {
       docs = hax-engine.overrideAttrs (old: {
         name = "hax-engine-docs";
-        nativeBuildInputs = old.nativeBuildInputs ++ [
-          ocamlPackages.odoc
-        ];
+        nativeBuildInputs =
+          old.nativeBuildInputs
+          ++ [
+            ocamlPackages.odoc
+          ];
         buildPhase = ''dune build @doc'';
         installPhase = "cp -rf _build/default/_doc/_html $out";
       });