Merge branch 'main' into main

Author: W95Psp

.github/workflows/clippy_rust_engine.yml

@@ -15,4 +15,4 @@ jobs:
     - uses: actions/checkout@v4
     - name: Run clippy
       run: |
-        cargo clippy -p rust-printer -- --no-deps
+        cargo clippy -p hax-rust-engine -- --no-deps

Cargo.lock

@@ -14,10 +14,10 @@ members = [
      "engine/names",
      "engine/names/extract",
      "hax-types",
-     "rust-printer",
-     "rust-printer/macros",
+     "rust-engine",
+     "rust-engine/macros",
 ]
-exclude = ["tests", "rustc-coverage-tests", "rust-printer/tests"]
+exclude = ["tests", "rustc-coverage-tests", "rust-engine/tests"]
 default-members = [
      "frontend/exporter",
      "frontend/exporter/options",
@@ -81,6 +81,7 @@ hax-lib-macros-types = { path = "hax-lib/macros/types", version = "=0.3.1" }
 hax-lib = { path = "hax-lib", version = "=0.3.1" }
 hax-engine-names = { path = "engine/names", version = "=0.3.1" }
 hax-types = { path = "hax-types", version = "=0.3.1" }
+hax-rust-engine = { path = "rust-engine" }
 
 [workspace.metadata.release]
 owners = ["github:cryspen:tools"]

Cargo.toml

@@ -48,14 +48,21 @@ extension-traits = "1.0.1"
 serde.workspace = true
 serde_json.workspace = true
 hax-types.workspace = true
+hax-rust-engine.workspace = true
 schemars.workspace = true
 hax-frontend-exporter.workspace = true
-hax-lib-macros-types = {workspace = true, features = ["schemars"]}
+hax-lib-macros-types = { workspace = true, features = ["schemars"] }
 version_check = "0.9"
 toml = "0.8"
 
 [package.metadata.release]
-pre-release-hook = ["dune", "build", "--root", "../../engine", "hax-engine.opam"]
+pre-release-hook = [
+    "dune",
+    "build",
+    "--root",
+    "../../engine",
+    "hax-engine.opam",
+]
 
 [[package.metadata.release.pre-release-replacements]]
 file = "../../engine/dune-project"

cli/subcommands/Cargo.toml

@@ -24,6 +24,7 @@ fn json_schema_static_asset() {
         hax_types::engine_api::protocol::FromEngine,
         hax_types::engine_api::protocol::ToEngine,
         hax_lib_macros_types::AttrPayload,
+        hax_rust_engine::ast::Item,
     ));
     schema.schema.metadata.get_or_insert_default().id = Some(hax_types::HAX_VERSION.into());
     serde_json::to_writer(

cli/subcommands/build.rs

@@ -149,12 +149,12 @@ These tests aim at increasing the confidence in the ability of hax frontend to h
 
 ### Rust printer testing
 
-This method aims at testing the quality of hax frontend's output. It uses a tool that is under development that we call the Rust printer.
+This method aims at testing the quality of hax frontend's output. It uses the Rust hax engine.
 
 This tool (written in Rust) takes the output of hax frontend (a json file describing the content of a Rust crate), it imports it as an AST (similar to the hax engine AST), and then prints this AST in Rust syntax. 
 
 If the Rust code we get out of this tool is equivalent to the Rust code it was given as input, then this means hax frontend correctly extracted the input code without losing or altering any information.
 
 There is no easy way of testing the full input/output equivalence so the methodology here is to test that the resulting code behaves the same as the input code with respect to relevant test cases.
 
-This work is available in the `rust-printer` folder. In the `tests` subfolder, an input file is available with tests for all Rust constructs supported by the printer (currently functions and expressions). For now these tests pass after extracting and printing the file with hax frontend and the Rust printer. This means that for the Rust constructs covered by the printer and the test file, hax frontend's extraction is correct. However this still needs to be extended to test more Rust constructs.
+This work is available in the `hax-rust-engine` folder. In the `tests` subfolder, an input file is available with tests for all Rust constructs supported by the printer (currently functions and expressions). For now these tests pass after extracting and printing the file with hax frontend and the Rust printer. This means that for the Rust constructs covered by the printer and the test file, hax frontend's extraction is correct. However this still needs to be extended to test more Rust constructs.

docs/frontend/evaluation.md

@@ -27,6 +27,9 @@ module Fresh_module : sig
 
   val to_mod_path : t -> View.ModPath.t
   (** Compute a module path for a fresh module. *)
+
+  val to_rust_ast : t -> Rust_engine_types.fresh_module
+  val from_rust_ast : Rust_engine_types.fresh_module -> t
 end = struct
   open View
 
@@ -111,6 +114,21 @@ end = struct
     |> snd |> Option.value_exn
 
   let get_path_hints { hints; _ } = hints
+
+  let to_rust_ast ({ id; hints; label } : t) : Rust_engine_types.fresh_module =
+    {
+      id = Int.to_string id;
+      hints = List.map ~f:Explicit_def_id.to_rust_ast hints;
+      label;
+    }
+
+  let from_rust_ast ({ id; hints; label } : Rust_engine_types.fresh_module) : t
+      =
+    {
+      id = Int.of_string id;
+      hints = List.map ~f:Explicit_def_id.from_rust_ast hints;
+      label;
+    }
 end
 
 type reserved_suffix = [ `Cast | `Pre | `Post ]
@@ -743,3 +761,27 @@ let matches_namespace (ns : Types.namespace) (did : t) : bool =
     | _ -> false
   in
   aux ns.chunks path
+
+let to_rust_ast ({ def_id; moved; suffix } : t) : Rust_engine_types.concrete_id
+    =
+  let moved = Option.map ~f:Fresh_module.to_rust_ast moved in
+  let suffix =
+    Option.map
+      ~f:(fun s ->
+        match s with
+        | `Cast -> Rust_engine_types.Cast
+        | `Pre -> Rust_engine_types.Pre
+        | `Post -> Rust_engine_types.Post)
+      suffix
+  in
+  { def_id = Explicit_def_id.to_rust_ast def_id; moved; suffix }
+
+let from_rust_ast ({ def_id; moved; suffix } : Rust_engine_types.concrete_id) :
+    t =
+  let moved = Option.map ~f:Fresh_module.from_rust_ast moved in
+  let suffix =
+    Option.map
+      ~f:(fun s -> match s with Cast -> `Cast | Pre -> `Pre | Post -> `Post)
+      suffix
+  in
+  { def_id = Explicit_def_id.from_rust_ast def_id; moved; suffix }

engine/lib/concrete_ident/concrete_ident.ml

@@ -104,3 +104,5 @@ module ImplInfoStore : sig
 end
 
 val matches_namespace : Types.namespace -> t -> bool
+val to_rust_ast : t -> Rust_engine_types.concrete_id
+val from_rust_ast : Rust_engine_types.concrete_id -> t

engine/lib/concrete_ident/concrete_ident.mli

@@ -125,3 +125,46 @@ module ImplInfoStore = struct
   let lookup_raw (impl_def_id : t) : Types.impl_infos option =
     find (to_def_id impl_def_id)
 end
+
+module ToRustAST = struct
+  module A = Types
+  module B = Rust_engine_types
+
+  let rec def_id_contents_to_rust_ast
+      ({ krate; path; parent; kind; _ } : A.def_id_contents) : B.def_id =
+    let f (o : A.def_id) = def_id_contents_to_rust_ast o.contents.value in
+    let parent = Option.map ~f parent in
+    { krate; path; parent; kind }
+
+  let to_rust_ast ({ is_constructor; def_id } : t) : B.explicit_def_id =
+    { is_constructor; def_id = def_id_contents_to_rust_ast def_id }
+end
+
+module FromRustAST = struct
+  module A = Rust_engine_types
+  module B = Types
+
+  let rec def_id_contents_to_rust_ast
+      ({ krate; path; parent; kind; _ } : A.def_id) : B.def_id_contents =
+    let f (o : A.def_id) : B.def_id =
+      let contents : B.node_for__def_id_contents =
+        { value = def_id_contents_to_rust_ast o; id = Int64.of_int (-1) }
+      in
+      { contents }
+    in
+    let parent = Option.map ~f parent in
+    {
+      krate;
+      path;
+      parent;
+      kind;
+      index = (Int64.of_int (-1), Int64.of_int (-1), None);
+      is_local = false;
+    }
+
+  let to_rust_ast ({ is_constructor; def_id } : A.explicit_def_id) : t =
+    { is_constructor; def_id = def_id_contents_to_rust_ast def_id }
+end
+
+let to_rust_ast = ToRustAST.to_rust_ast
+let from_rust_ast = FromRustAST.to_rust_ast

engine/lib/concrete_ident/explicit_def_id.ml

@@ -81,3 +81,6 @@ module ImplInfoStore : sig
   engine, this function may return [None] even though the supplied
   identifier points to an [Impl] block. *)
 end
+
+val to_rust_ast : t -> Rust_engine_types.explicit_def_id
+val from_rust_ast : Rust_engine_types.explicit_def_id -> t