Merge pull request #1508 from cryspen/rengine-conform-engine-interface

Rust Engine: turn it into a hax-frontend compatible engine

Author: W95Psp

.github/workflows/test.yml

@@ -28,7 +28,7 @@ jobs:
       - uses: Swatinem/rust-cache@v2
 
       - name: Test
-        run: cargo test --workspace --exclude hax-engine-names-extract --verbose
+        run: cargo test --workspace --exclude hax-engine-names-extract --exclude hax-rust-engine --verbose
 
       - name: Test `hax-frontend-exporter` with feature `rustc` off
         run: cargo check -p hax-frontend-exporter --no-default-features --verbose

.utils/rebuild.sh

@@ -31,7 +31,7 @@ cd_rootwise () {
 
 rust () {
     cd_rootwise "cli"
-    for i in driver subcommands ../engine/names/extract; do
+    for i in driver subcommands ../engine/names/extract ../rust-engine; do
         CURRENT="rust/$i"
         cargo install --locked --quiet $OFFLINE_FLAG --debug --path $i
     done

Cargo.lock

@@ -24,7 +24,8 @@ 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,
+        hax_rust_engine::ocaml_engine::Query,
+        hax_rust_engine::ocaml_engine::Response,
     ));
     schema.schema.metadata.get_or_insert_default().id = Some(hax_types::HAX_VERSION.into());
     serde_json::to_writer(

cli/subcommands/build.rs

@@ -125,6 +125,25 @@ fn find_hax_engine(message_format: MessageFormat) -> process::Command {
         })
 }
 
+const RUST_ENGINE_BINARY_NAME: &str = "hax-rust-engine";
+const RUST_ENGINE_BINARY_NOT_FOUND: &str =
+    "The binary [hax-rust-engine] was not found in your [PATH].";
+
+#[allow(unused_variables, unreachable_code)]
+fn find_rust_hax_engine(message_format: MessageFormat) -> process::Command {
+    use which::which;
+
+    std::env::var("HAX_RUST_BINARY")
+        .ok()
+        .map(process::Command::new)
+        .or_else(|| {
+            which(RUST_ENGINE_BINARY_NAME)
+                .ok()
+                .map(process::Command::new)
+        })
+        .expect(RUST_ENGINE_BINARY_NOT_FOUND)
+}
+
 use hax_types::diagnostics::message::HaxMessage;
 use hax_types::diagnostics::report::ReportCtx;
 
@@ -245,7 +264,12 @@ fn run_engine(
         input: haxmeta.items,
         impl_infos: haxmeta.impl_infos,
     };
-    let mut engine_subprocess = find_hax_engine(message_format)
+    let mut hax_engine_command = if let Backend::Lean { .. } = &engine_options.backend.backend {
+        find_rust_hax_engine(message_format)
+    } else {
+        find_hax_engine(message_format)
+    };
+    let mut engine_subprocess = hax_engine_command
         .stdin(std::process::Stdio::piped())
         .stdout(std::process::Stdio::piped())
         .spawn()

cli/subcommands/src/cargo_hax.rs

@@ -140,7 +140,12 @@ let run (options : Types.engine_options) : Types.output =
         | Fstar opts -> run (module Fstar_backend) opts
         | Coq -> run (module Coq_backend) ()
         | Ssprove -> run (module Ssprove_backend) ()
-        | Easycrypt -> run (module Easycrypt_backend) ())
+        | Easycrypt -> run (module Easycrypt_backend) ()
+        | Lean ->
+            failwith
+              "The OCaml hax engine should never be called for lean. The Lean \
+               backend uses the newer rust engine. Please report this issue on \
+               our GitHub repository: https://github.com/cryspen/hax.")
   in
   {
     diagnostics = List.map ~f:Diagnostics.to_thir_diagnostic diagnostics;
@@ -181,34 +186,39 @@ let parse_id_table_node (json : Yojson.Safe.t) :
   in
   (table, value)
 
-let parse_options () =
+let load_table ?(check_version = true) : Yojson.Safe.t =
   let table, json =
     Hax_io.read_json () |> Option.value_exn |> parse_id_table_node
   in
-  let version =
-    try Yojson.Safe.Util.(member "hax_version" json |> to_string)
-    with _ -> "unknown"
-  in
-  if String.equal version Types.hax_version |> not then (
-    prerr_endline
-      [%string
-        {|
+  (if check_version then
+     let version =
+       try Yojson.Safe.Util.(member "hax_version" json |> to_string)
+       with _ -> "unknown"
+     in
+     if String.equal version Types.hax_version |> not then (
+       prerr_endline
+         [%string
+           {|
 The versions of `hax-engine` and of `cargo-hax` are different:
   - `hax-engine` version: %{Types.hax_version}
   - `cargo-hax`  version: %{version}
 
 Please reinstall hax.
 |}];
-    Stdlib.exit 1);
+       Stdlib.exit 1));
   table
   |> List.iter ~f:(fun (id, json) ->
          Hashtbl.add_exn Types.cache_map ~key:id ~data:(`JSON json));
+  json
+
+let parse_options () =
+  let json = load_table ~check_version:true in
   let options = [%of_yojson: Types.engine_options] json in
   Profiling.enabled := options.backend.profile;
   options
 
 (** Entrypoint of the engine. Assumes `Hax_io.init` was called. *)
-let main () =
+let engine () =
   let options = Profiling.profile (Other "parse_options") 1 parse_options in
   Printexc.record_backtrace true;
   let result =
@@ -240,3 +250,41 @@ let main () =
   | Error (exn, bt) ->
       Logs.info (fun m -> m "Exiting Hax engine (with an unexpected failure)");
       Printexc.raise_with_backtrace exn bt
+
+module ExportRustAst = Export_ast.Make (Features.Rust)
+module ExportFStarAst = Export_ast.Make (Fstar_backend.InputLanguage)
+
+(** Entry point for interacting with the Rust hax engine *)
+let driver_for_rust_engine () : unit =
+  let query : Rust_engine_types.query =
+    (* TODO: support for table *)
+    (* let json = load_table ~check_version:false in *)
+    let json = Hax_io.read_json () |> Option.value_exn in
+    [%of_yojson: Rust_engine_types.query] json
+  in
+  Concrete_ident.ImplInfoStore.init
+    (Concrete_ident_generated.impl_infos @ query.impl_infos);
+  match query.kind with
+  | Types.ImportThir { input } ->
+      let imported_items = import_thir_items [] input in
+      let imported_items =
+        (* TODO: this let binding is applying the phases from the F* backend *)
+        Fstar_backend.apply_phases
+          {
+            cli_extension = EmptyStructempty_args_extension;
+            fuel = Int64.zero;
+            ifuel = Int64.zero;
+            interfaces = [];
+            line_width = 80;
+            z3rlimit = Int64.zero;
+          }
+          imported_items
+      in
+      let rust_ast_items =
+        List.concat_map
+          ~f:(fun item -> ExportFStarAst.ditem item)
+          imported_items
+      in
+      let response = Rust_engine_types.ImportThir { output = rust_ast_items } in
+      Hax_io.write_json ([%yojson_of: Rust_engine_types.response] response);
+      Hax_io.write_json ([%yojson_of: Types.from_engine] Exit)

engine/bin/lib.ml

@@ -1 +1,2 @@
-val main : unit -> unit
+val engine : unit -> unit
+val driver_for_rust_engine : unit -> unit

engine/bin/lib.mli

@@ -20,4 +20,6 @@ let _ =
         output_char stdout '\n';
         flush stdout
     end);
-  Lib.main ()
+  match Sys.get_argv () with
+  | [| _; "driver_rust_engine" |] -> Lib.driver_for_rust_engine ()
+  | _ -> Lib.engine ()

engine/bin/native_driver.ml

@@ -347,7 +347,7 @@ module Make (FA : Features.T) = struct
     | String s -> B.String (Newtypesymbol s)
     | Char c -> B.Char c
     | Int { value; negative; kind } ->
-        B.Int { value; negative; kind = dint_kind kind }
+        B.Int { value = Newtypesymbol value; negative; kind = dint_kind kind }
     | Float { value; negative; kind } ->
         B.Float
           { value = Newtypesymbol value; negative; kind = dfloat_kind kind }

engine/lib/export_ast.ml

@@ -182,16 +182,20 @@ pub enum Backend<E: Extension> {
     Easycrypt,
     /// Use the ProVerif backend (warning: work in progress!)
     ProVerif(ProVerifOptions),
+    /// Use the Lean backend (warning: work in progress!)
+    #[clap(hide = true)]
+    Lean,
 }
 
 impl fmt::Display for Backend<()> {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
         match self {
-            Backend::Fstar(..) => write!(f, "fstar"),
-            Backend::Coq => write!(f, "coq"),
-            Backend::Ssprove => write!(f, "ssprove"),
-            Backend::Easycrypt => write!(f, "easycrypt"),
-            Backend::ProVerif(..) => write!(f, "proverif"),
+            Backend::Fstar { .. } => write!(f, "fstar"),
+            Backend::Coq { .. } => write!(f, "coq"),
+            Backend::Ssprove { .. } => write!(f, "ssprove"),
+            Backend::Easycrypt { .. } => write!(f, "easycrypt"),
+            Backend::ProVerif { .. } => write!(f, "proverif"),
+            Backend::Lean { .. } => write!(f, "lean"),
         }
     }
 }