Merge pull request #802 from hacspec/add-json-format-option

Add json format option

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

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::*;
@@ -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")
@@ -116,22 +116,76 @@ 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(message_format, 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(self, message_format: MessageFormat, rctx: Option<&mut ReportCtx>) {
+        match message_format {
+            MessageFormat::Json => println!("{}", 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 {
+            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`
@@ -140,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()
@@ -207,12 +262,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(message_format, Some(&mut rctx));
                 }
                 FromEngine::File(file) => {
                     if backend.dry_run {
@@ -221,8 +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();
-                        let title = format!("hax: wrote file {}", path.display());
-                        report(Level::Info.title(&title))
+                        HaxMessage::WroteFile { path }.report(message_format, None)
                     }
                 }
                 FromEngine::DebugString(debug) => {
@@ -252,12 +310,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);
     }
 
@@ -310,6 +365,11 @@ fn compute_haxmeta_files(options: &Options) -> (Vec<EmitHaxMetaMessage>, 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"));
@@ -355,8 +415,7 @@ fn compute_haxmeta_files(options: &Options) -> (Vec<EmitHaxMetaMessage>, 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(options.message_format, None);
         status.code().unwrap_or(254)
     } else {
         0
@@ -399,11 +458,10 @@ fn run_command(options: &Options, haxmeta_files: Vec<EmitHaxMetaMessage>) -> 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(options.message_format, None);
             }
 
             let mut error = false;
@@ -415,7 +473,14 @@ fn run_command(options: &Options, haxmeta_files: Vec<EmitHaxMetaMessage>) -> boo
             {
                 let haxmeta: HaxMeta<Body> = 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
         }

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;
 };

hax-types/src/cli_options.rs

@@ -433,12 +433,24 @@ 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.
     #[arg(long)]
     pub no_custom_target_directory: bool,
+
+    /// 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, Eq, PartialEq)]
+pub enum MessageFormat {
+    Human,
+    Json,
 }
 
 impl NormalizePaths for Command {

hax-types/src/diagnostics/message.rs

@@ -0,0 +1,39 @@
+use crate::cli_options::Backend;
+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,
+    } = 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()),
+        }
+    }
+}

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)]

hax-types/src/diagnostics/report.rs

@@ -10,7 +10,7 @@ pub struct ReportCtx {
     files: HashMap<PathBuf, Rc<String>>,
 }
 
-/// 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 {