From c25fc217e4652f2d1d499138db6c265d58f7520f Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 24 Jul 2024 14:56:23 +0200 Subject: [PATCH 1/8] feat(engine/ocaml_of_json_schema): add `val` to keyword list `val` is not a keyword in Rust, but is in OCaml, so it should be renamed by the script that generates OCaml types, parsers and serializers. This PR adds an exhaustive list of OCaml keywords to the list of words that shoudl get rewritten. --- .../ocaml_of_json_schema/ocaml_of_json_schema.js | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js b/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js index 13e3b94c9..f3de435db 100644 --- a/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js +++ b/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js @@ -76,7 +76,16 @@ let variantNameOf = s => { }; let typeNameOf = s => s.replace(/[A-Z]/g, (l, i) => `${i?'_':''}${l.toLowerCase()}`); let fieldNameOf = s => { - if (['then', 'if', 'end', 'open', 'include', 'begin', 'fun', 'initializer'].includes(s)) + let ocaml_keywords = [ "and", "as", "assert", "asr", "begin", "class", "constraint", + "do", "done", "downto", "else", "end", "exception", "external", + "false", "for", "fun", "function", "functor", "if", "in", + "include", "inherit", "initializer", "land", "lazy", "let", + "lor", "lsl", "lsr", "lxor", "match", "method", "mod", "module", + "mutable", "new", "nonrec", "object", "of", "open", "or", + "private", "rec", "sig", "struct", "then", "to", "true", "try", + "type", "val", "virtual", "when", "while", "with" + ]; + if (ocaml_keywords.includes(s)) return s + "'"; return s; }; From e379c0b11acf86e476ae6ded4a74070b363fed03 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 25 Jul 2024 09:00:52 +0200 Subject: [PATCH 2/8] refactor: add enum `HaxMessage`, use as a base for reporting --- cli/subcommands/Cargo.toml | 1 + cli/subcommands/src/cargo_hax.rs | 108 +++++++++++++++++++-------- hax-types/src/diagnostics/message.rs | 24 ++++++ hax-types/src/diagnostics/mod.rs | 1 + hax-types/src/diagnostics/report.rs | 2 +- 5 files changed, 104 insertions(+), 32 deletions(-) create mode 100644 hax-types/src/diagnostics/message.rs diff --git a/cli/subcommands/Cargo.toml b/cli/subcommands/Cargo.toml index 93b44cb86..7efc93be4 100644 --- a/cli/subcommands/Cargo.toml +++ b/cli/subcommands/Cargo.toml @@ -42,6 +42,7 @@ serde-jsonlines = "0.5.0" prettyplease = "0.2.20" syn = { version = "2.*", features = ["full"] } cargo_metadata.workspace = true +extension-traits = "1.0.1" [build-dependencies] serde.workspace = true diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs index dbe58d133..a4ad36a55 100644 --- a/cli/subcommands/src/cargo_hax.rs +++ b/cli/subcommands/src/cargo_hax.rs @@ -1,4 +1,4 @@ -use annotate_snippets::{Level, Message, Renderer}; +use annotate_snippets::{Level, Renderer}; use clap::Parser; use colored::Colorize; use hax_types::cli_options::*; @@ -116,22 +116,70 @@ fn find_hax_engine() -> process::Command { fn is_opam_setup_correctly() -> bool { std::env::var("OPAM_SWITCH_PREFIX").is_ok() } - use colored::Colorize; - let message = format!("hax: {}\n{}\n\n{} {}\n", - &ENGINE_BINARY_NOT_FOUND, - "Please make sure the engine is installed and is in PATH!", - "Hint: With OPAM, `eval $(opam env)` is necessary for OPAM binaries to be in PATH: make sure to run `eval $(opam env)` before running `cargo hax`.".bright_black(), - format!("(diagnostics: {})", if is_opam_setup_correctly() { "opam seems okay ✓" } else {"opam seems not okay ❌"}).bright_black() - ); - report(Level::Error.title(&message)); + HaxMessage::EngineNotFound { + is_opam_setup_correctly: is_opam_setup_correctly(), + } + .report_styled(None); std::process::exit(2); }) } -/// Report an `annotate_snippets::Message` now -fn report(message: Message) { - let renderer = Renderer::styled(); - eprintln!("{}", renderer.render(message)) +use hax_types::diagnostics::message::HaxMessage; +use hax_types::diagnostics::report::ReportCtx; + +#[extension_traits::extension(trait ExtHaxMessage)] +impl HaxMessage { + fn report_styled(self, rctx: Option<&mut ReportCtx>) { + let renderer = Renderer::styled(); + match self { + Self::Diagnostic { + diagnostic, + working_dir, + } => { + let mut _rctx = None; + let rctx = rctx.unwrap_or_else(|| _rctx.get_or_insert(ReportCtx::default())); + diagnostic.with_message(rctx, &working_dir, Level::Error, |msg| { + eprintln!("{}", renderer.render(msg)) + }); + } + Self::EngineNotFound { + is_opam_setup_correctly, + } => { + use colored::Colorize; + let message = format!("hax: {}\n{}\n\n{} {}\n", + &ENGINE_BINARY_NOT_FOUND, + "Please make sure the engine is installed and is in PATH!", + "Hint: With OPAM, `eval $(opam env)` is necessary for OPAM binaries to be in PATH: make sure to run `eval $(opam env)` before running `cargo hax`.".bright_black(), + format!("(diagnostics: {})", if is_opam_setup_correctly { "opam seems okay ✓" } else {"opam seems not okay ❌"}).bright_black() + ); + let message = Level::Error.title(&message); + eprintln!("{}", renderer.render(message)) + } + Self::WroteFile { path } => { + let title = format!("hax: wrote file {}", path.display()); + eprintln!("{}", renderer.render(Level::Info.title(&title))) + } + Self::HaxEngineFailure { exit_code } => { + let title = format!( + "hax: {} exited with non-zero code {}", + ENGINE_BINARY_NAME, exit_code, + ); + eprintln!("{}", renderer.render(Level::Error.title(&title))); + } + Self::CargoBuildFailure => { + let title = + format!("hax: running `cargo build` was not successful, continuing anyway."); + eprintln!("{}", renderer.render(Level::Warning.title(&title))); + } + Self::WarnExperimentalBackend { backend } => { + let title = format!( + "hax: Experimental backend \"{}\" is work in progress.", + backend + ); + eprintln!("{}", renderer.render(Level::Warning.title(&title))); + } + } + } } /// Runs `hax-engine` @@ -207,12 +255,16 @@ fn run_engine( use protocol::*; match msg { FromEngine::Exit => break, - FromEngine::Diagnostic(diag) => { + FromEngine::Diagnostic(diagnostic) => { error = true; if backend.dry_run { - output.diagnostics.push(diag.clone()) + output.diagnostics.push(diagnostic.clone()) } - diag.with_message(&mut rctx, &working_dir, Level::Error, report); + HaxMessage::Diagnostic { + diagnostic, + working_dir: working_dir.clone(), + } + .report_styled(Some(&mut rctx)); } FromEngine::File(file) => { if backend.dry_run { @@ -221,8 +273,7 @@ fn run_engine( let path = out_dir.join(&file.path); std::fs::create_dir_all(&path.parent().unwrap()).unwrap(); std::fs::write(&path, file.contents).unwrap(); - let title = format!("hax: wrote file {}", path.display()); - report(Level::Info.title(&title)) + HaxMessage::WroteFile { path }.report_styled(None) } } FromEngine::DebugString(debug) => { @@ -252,12 +303,9 @@ fn run_engine( let exit_status = engine_subprocess.wait().unwrap(); if !exit_status.success() { - let title = format!( - "hax: {} exited with non-zero code {}", - ENGINE_BINARY_NAME, - exit_status.code().unwrap_or(-1), - ); - report(Level::Error.title(&title)); + HaxMessage::HaxEngineFailure { + exit_code: exit_status.code().unwrap_or(-1), + }; std::process::exit(1); } @@ -355,8 +403,7 @@ fn compute_haxmeta_files(options: &Options) -> (Vec, i32) { .expect("`driver-hax-frontend-exporter`: could not start?"); let exit_code = if !status.success() { - let title = format!("hax: running `cargo build` was not successful, continuing anyway."); - report(Level::Warning.title(&title)); + HaxMessage::CargoBuildFailure.report_styled(None); status.code().unwrap_or(254) } else { 0 @@ -399,11 +446,10 @@ fn run_command(options: &Options, haxmeta_files: Vec) -> boo use Backend; if matches!(backend.backend, Backend::Easycrypt | Backend::ProVerif(..)) { - let title = format!( - "hax: Experimental backend \"{}\" is work in progress.", - backend.backend - ); - report(Level::Warning.title(&title)) + HaxMessage::WarnExperimentalBackend { + backend: backend.backend.clone(), + } + .report_styled(None); } let mut error = false; diff --git a/hax-types/src/diagnostics/message.rs b/hax-types/src/diagnostics/message.rs new file mode 100644 index 000000000..e333aa4d2 --- /dev/null +++ b/hax-types/src/diagnostics/message.rs @@ -0,0 +1,24 @@ +use crate::cli_options::Backend; +use crate::prelude::*; + +#[derive_group(Serializers)] +#[derive(Debug, Clone, JsonSchema)] +pub enum HaxMessage { + Diagnostic { + diagnostic: super::Diagnostics, + working_dir: PathBuf, + }, + EngineNotFound { + is_opam_setup_correctly: bool, + }, + WroteFile { + path: PathBuf, + }, + HaxEngineFailure { + exit_code: i32, + }, + CargoBuildFailure, + WarnExperimentalBackend { + backend: Backend, + }, +} diff --git a/hax-types/src/diagnostics/mod.rs b/hax-types/src/diagnostics/mod.rs index 096c9a237..d9e57b492 100644 --- a/hax-types/src/diagnostics/mod.rs +++ b/hax-types/src/diagnostics/mod.rs @@ -1,6 +1,7 @@ use crate::prelude::*; use colored::Colorize; +pub mod message; pub mod report; #[derive_group(Serializers)] diff --git a/hax-types/src/diagnostics/report.rs b/hax-types/src/diagnostics/report.rs index d875d58f3..3faba540d 100644 --- a/hax-types/src/diagnostics/report.rs +++ b/hax-types/src/diagnostics/report.rs @@ -10,7 +10,7 @@ pub struct ReportCtx { files: HashMap>, } -/// Translates ae line and column position into an absolute offset +/// Translates a line and column position into an absolute offset fn compute_offset(src: &str, mut line: usize, col: usize) -> usize { let mut chars = src.chars().enumerate(); while line > 1 { From f3d548c4d0e5852e12c85929635a462e4f32b610 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 25 Jul 2024 09:21:31 +0200 Subject: [PATCH 3/8] feat: add `message_format` --- cli/subcommands/src/cargo_hax.rs | 30 ++++++++++++++++++++++-------- hax-types/src/cli_options.rs | 11 +++++++++++ 2 files changed, 33 insertions(+), 8 deletions(-) diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs index a4ad36a55..8e088def8 100644 --- a/cli/subcommands/src/cargo_hax.rs +++ b/cli/subcommands/src/cargo_hax.rs @@ -82,7 +82,7 @@ const ENGINE_BINARY_NOT_FOUND: &str = "The binary [hax-engine] was not found in /// found, detect whether nodejs is available, download the JS-compiled /// engine and use it. #[allow(unused_variables, unreachable_code)] -fn find_hax_engine() -> process::Command { +fn find_hax_engine(message_format: MessageFormat) -> process::Command { use which::which; std::env::var("HAX_ENGINE_BINARY") @@ -119,7 +119,7 @@ fn find_hax_engine() -> process::Command { HaxMessage::EngineNotFound { is_opam_setup_correctly: is_opam_setup_correctly(), } - .report_styled(None); + .report(message_format, None); std::process::exit(2); }) } @@ -129,6 +129,12 @@ use hax_types::diagnostics::report::ReportCtx; #[extension_traits::extension(trait ExtHaxMessage)] impl HaxMessage { + fn report(self, message_format: MessageFormat, rctx: Option<&mut ReportCtx>) { + match message_format { + MessageFormat::Json => eprintln!("{}", serde_json::to_string(&self).unwrap()), + MessageFormat::Human => self.report_styled(rctx), + } + } fn report_styled(self, rctx: Option<&mut ReportCtx>) { let renderer = Renderer::styled(); match self { @@ -188,13 +194,14 @@ fn run_engine( working_dir: PathBuf, manifest_dir: PathBuf, backend: &BackendOptions, + message_format: MessageFormat, ) -> bool { let engine_options = EngineOptions { backend: backend.clone(), input: haxmeta.items, impl_infos: haxmeta.impl_infos, }; - let mut engine_subprocess = find_hax_engine() + let mut engine_subprocess = find_hax_engine(message_format) .stdin(std::process::Stdio::piped()) .stdout(std::process::Stdio::piped()) .spawn() @@ -264,7 +271,7 @@ fn run_engine( diagnostic, working_dir: working_dir.clone(), } - .report_styled(Some(&mut rctx)); + .report(message_format, Some(&mut rctx)); } FromEngine::File(file) => { if backend.dry_run { @@ -273,7 +280,7 @@ fn run_engine( let path = out_dir.join(&file.path); std::fs::create_dir_all(&path.parent().unwrap()).unwrap(); std::fs::write(&path, file.contents).unwrap(); - HaxMessage::WroteFile { path }.report_styled(None) + HaxMessage::WroteFile { path }.report(message_format, None) } } FromEngine::DebugString(debug) => { @@ -403,7 +410,7 @@ fn compute_haxmeta_files(options: &Options) -> (Vec, i32) { .expect("`driver-hax-frontend-exporter`: could not start?"); let exit_code = if !status.success() { - HaxMessage::CargoBuildFailure.report_styled(None); + HaxMessage::CargoBuildFailure.report(options.message_format, None); status.code().unwrap_or(254) } else { 0 @@ -449,7 +456,7 @@ fn run_command(options: &Options, haxmeta_files: Vec) -> boo HaxMessage::WarnExperimentalBackend { backend: backend.backend.clone(), } - .report_styled(None); + .report(options.message_format, None); } let mut error = false; @@ -461,7 +468,14 @@ fn run_command(options: &Options, haxmeta_files: Vec) -> boo { let haxmeta: HaxMeta = HaxMeta::read(fs::File::open(&path).unwrap()); - error = error || run_engine(haxmeta, working_dir, manifest_dir, &backend); + error = error + || run_engine( + haxmeta, + working_dir, + manifest_dir, + &backend, + options.message_format, + ); } error } diff --git a/hax-types/src/cli_options.rs b/hax-types/src/cli_options.rs index 2338ae979..afe56acc2 100644 --- a/hax-types/src/cli_options.rs +++ b/hax-types/src/cli_options.rs @@ -439,6 +439,17 @@ pub struct Options { /// this behavior. #[arg(long)] pub no_custom_target_directory: bool, + + /// Diagnostic format. + #[arg(long, default_value = "human")] + pub message_format: MessageFormat, +} + +#[derive_group(Serializers)] +#[derive(JsonSchema, ValueEnum, Debug, Clone, Copy)] +pub enum MessageFormat { + Human, + Json, } impl NormalizePaths for Command { From 588ed4fdcacf563245831a2b97e31bbe9ea657e0 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 25 Jul 2024 09:21:41 +0200 Subject: [PATCH 4/8] chore: minor typo --- hax-types/src/cli_options.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hax-types/src/cli_options.rs b/hax-types/src/cli_options.rs index afe56acc2..80cb3e5a8 100644 --- a/hax-types/src/cli_options.rs +++ b/hax-types/src/cli_options.rs @@ -433,7 +433,7 @@ pub struct Options { #[arg(long = "deps")] pub deps: bool, - /// By default, hax use `$CARGO_TARGET_DIR/hax` as target folder, + /// By default, hax uses `$CARGO_TARGET_DIR/hax` as target folder, /// to avoid recompilation when working both with `cargo hax` and /// `cargo build` (or, e.g. `rust-analyzer`). This option disables /// this behavior. From 9b756ab7de3e8dc4877038bc90363c0d6abc976b Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 25 Jul 2024 09:27:54 +0200 Subject: [PATCH 5/8] feat(diagnostics): `HaxMessage`: add `code()` function --- hax-types/src/diagnostics/message.rs | 27 +++++++++++++++++++++------ 1 file changed, 21 insertions(+), 6 deletions(-) diff --git a/hax-types/src/diagnostics/message.rs b/hax-types/src/diagnostics/message.rs index e333aa4d2..47ad79a43 100644 --- a/hax-types/src/diagnostics/message.rs +++ b/hax-types/src/diagnostics/message.rs @@ -3,22 +3,37 @@ use crate::prelude::*; #[derive_group(Serializers)] #[derive(Debug, Clone, JsonSchema)] +#[repr(u8)] pub enum HaxMessage { Diagnostic { diagnostic: super::Diagnostics, working_dir: PathBuf, - }, + } = 254, EngineNotFound { is_opam_setup_correctly: bool, - }, + } = 0, WroteFile { path: PathBuf, - }, + } = 1, HaxEngineFailure { exit_code: i32, - }, - CargoBuildFailure, + } = 2, + CargoBuildFailure = 3, WarnExperimentalBackend { backend: Backend, - }, + } = 4, +} + +impl HaxMessage { + // https://doc.rust-lang.org/reference/items/enumerations.html#pointer-casting + pub fn discriminant(&self) -> u16 { + unsafe { *(self as *const Self as *const u16) } + } + + pub fn code(&self) -> String { + match self { + HaxMessage::Diagnostic { diagnostic, .. } => diagnostic.kind.code(), + _ => format!("CARGOHAX{:0>4}", self.discriminant()), + } + } } From 9de338014174de94c2548a46730e8ee6b4128ba8 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 25 Jul 2024 09:46:53 +0200 Subject: [PATCH 6/8] feat(cli): propagate message format --- cli/subcommands/src/cargo_hax.rs | 5 +++++ hax-types/src/cli_options.rs | 5 +++-- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs index 8e088def8..85883b24c 100644 --- a/cli/subcommands/src/cargo_hax.rs +++ b/cli/subcommands/src/cargo_hax.rs @@ -365,6 +365,11 @@ fn compute_haxmeta_files(options: &Options) -> (Vec, i32) { if !explicit_color_flag && std::io::stderr().is_terminal() { cmd.args([COLOR_FLAG, "always"]); } + const MSG_FMT_FLAG: &str = "--message-format"; + let explicit_msg_fmt_flag = options.cargo_flags.iter().any(|flag| flag == MSG_FMT_FLAG); + if !explicit_msg_fmt_flag && options.message_format == MessageFormat::Json { + cmd.args([MSG_FMT_FLAG, "json"]); + } cmd.stderr(std::process::Stdio::piped()); if !options.no_custom_target_directory { cmd.env("CARGO_TARGET_DIR", target_dir("hax")); diff --git a/hax-types/src/cli_options.rs b/hax-types/src/cli_options.rs index 80cb3e5a8..c63c866c5 100644 --- a/hax-types/src/cli_options.rs +++ b/hax-types/src/cli_options.rs @@ -440,13 +440,14 @@ pub struct Options { #[arg(long)] pub no_custom_target_directory: bool, - /// Diagnostic format. + /// Diagnostic format. Sets `cargo`'s `--message-format` as well, + /// if not present. #[arg(long, default_value = "human")] pub message_format: MessageFormat, } #[derive_group(Serializers)] -#[derive(JsonSchema, ValueEnum, Debug, Clone, Copy)] +#[derive(JsonSchema, ValueEnum, Debug, Clone, Copy, Eq, PartialEq)] pub enum MessageFormat { Human, Json, From 1dc5c1dddec96a5503a199185ccd2c117c7011b5 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 25 Jul 2024 09:57:13 +0200 Subject: [PATCH 7/8] fix(cli): JSON diagnostics should be on stdout, not stderr --- cli/subcommands/src/cargo_hax.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/cli/subcommands/src/cargo_hax.rs b/cli/subcommands/src/cargo_hax.rs index 85883b24c..6c3b52a6c 100644 --- a/cli/subcommands/src/cargo_hax.rs +++ b/cli/subcommands/src/cargo_hax.rs @@ -131,7 +131,7 @@ use hax_types::diagnostics::report::ReportCtx; impl HaxMessage { fn report(self, message_format: MessageFormat, rctx: Option<&mut ReportCtx>) { match message_format { - MessageFormat::Json => eprintln!("{}", serde_json::to_string(&self).unwrap()), + MessageFormat::Json => println!("{}", serde_json::to_string(&self).unwrap()), MessageFormat::Human => self.report_styled(rctx), } } From 4e1a614a2edac9d4e81188d60d0c14770ff0c862 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 25 Jul 2024 09:58:27 +0200 Subject: [PATCH 8/8] chore: lock `Cargo.lock` --- Cargo.lock | 1 + 1 file changed, 1 insertion(+) diff --git a/Cargo.lock b/Cargo.lock index 41873af81..9a09e2844 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -161,6 +161,7 @@ dependencies = [ "cargo_metadata", "clap", "colored", + "extension-traits", "hax-frontend-exporter", "hax-frontend-exporter-options", "hax-lib-macros-types",