Cargo hax: improve error reports

CHANGELOG.md

@@ -32,6 +32,7 @@ Changes to hax-lib:
 
 Miscellaneous:
  - A lean tutorial has been added to the hax website (#1626)
+ - Diagnostics reporting were improved (#1692)
 
 ## 0.3.4
 

cli/subcommands/src/cargo_hax.rs

@@ -150,6 +150,17 @@ use hax_types::diagnostics::report::ReportCtx;
 #[extension_traits::extension(trait ExtHaxMessage)]
 impl HaxMessage {
     fn report(self, message_format: MessageFormat, rctx: Option<&mut ReportCtx>) {
+        let rctx = if let Some(rctx) = rctx {
+            if let HaxMessage::Diagnostic { diagnostic, .. } = &self
+                && rctx.seen_already(diagnostic.clone())
+            {
+                return;
+            } else {
+                Some(rctx)
+            }
+        } else {
+            None
+        };
         match message_format {
             MessageFormat::Json => println!("{}", serde_json::to_string(&self).unwrap()),
             MessageFormat::Human => self.report_styled(rctx),

engine/lib/backend.ml

@@ -55,7 +55,8 @@ module Make (InputLanguage : Features.T) (M : BackendMetadata) = struct
       let context = Diagnostics.Context.Backend M.backend in
       let kind = err.kind in
       let span = Span.to_thir err.span in
-      Diagnostics.SpanFreeError.raise ~span context kind
+      Diagnostics.SpanFreeError.raise ~span (Span.owner_hint err.span) context
+        kind
 
     let unimplemented ?issue_id ?details span =
       raise

engine/lib/deprecated_generic_printer/deprecated_generic_printer_base.ml

@@ -130,7 +130,9 @@ module Make (F : Features.T) = struct
           let span = Span.to_thir current_span in
           let kind = Types.AssertionFailure { details } in
           let ctx = Diagnostics.Context.GenericPrinter print#printer_name in
-          Diagnostics.SpanFreeError.raise ~span ctx kind
+          Diagnostics.SpanFreeError.raise ~span
+            (Span.owner_hint current_span)
+            ctx kind
 
       method set_current_namespace ns = current_namespace <- ns
       method get_current_namespace () = current_namespace

engine/lib/diagnostics.ml

@@ -147,7 +147,9 @@ module SpanFreeError : sig
   exception Exn of t
 
   val payload : t -> Context.t * kind
-  val raise : ?span:T.span list -> Context.t -> kind -> 'a
+
+  val raise :
+    ?span:T.span list -> Types.def_id option -> Context.t -> kind -> 'a
 end = struct
   type t = Data of Context.t * kind [@@deriving show]
 
@@ -158,7 +160,8 @@ end = struct
   let raise_without_reporting (ctx : Context.t) (kind : kind) =
     raise (Exn (Data (ctx, kind)))
 
-  let raise ?(span = []) (ctx : Context.t) (kind : kind) =
-    report { span; kind; context = ctx; owner_id = None };
+  let raise ?(span = []) (owner_id : Types.def_id option) (ctx : Context.t)
+      (kind : kind) =
+    report { span; kind; context = ctx; owner_id };
     raise_without_reporting ctx kind
 end

engine/lib/feature_gate.ml

@@ -43,14 +43,15 @@ struct
             =
           try f span x
           with S0.E err ->
-            let span = Span.to_thir span in
+            let thir_span = Span.to_thir span in
             let kind : Diagnostics.kind =
               ExplicitRejection { reason = S0.explain err feature_kind }
             in
             let context : Diagnostics.Context.t =
               Phase S0.metadata.current_phase
             in
-            Diagnostics.SpanFreeError.raise ~span context kind
+            Diagnostics.SpanFreeError.raise ~span:thir_span
+              (Span.owner_hint span) context kind
       end)
 
   include Subtype.Make (FA) (FB) (S)

engine/lib/generic_printer/generic_printer.ml

@@ -198,7 +198,9 @@ module Make (F : Features.T) = struct
           let span = Span.to_thir self#current_span in
           let kind = Types.AssertionFailure { details } in
           let ctx = Diagnostics.Context.GenericPrinter self#printer_name in
-          Diagnostics.SpanFreeError.raise ~span ctx kind
+          Diagnostics.SpanFreeError.raise ~span
+            (Span.owner_hint self#current_span)
+            ctx kind
       (** An assertion failed *)
 
       method unreachable : 'any. unit -> 'any =

engine/lib/import_thir.ml

@@ -20,7 +20,9 @@ open Diagnostics
 
 let assertion_failure (span : Thir.span list) (details : string) =
   let kind = T.AssertionFailure { details } in
-  Diagnostics.SpanFreeError.raise ~span ThirImport kind
+  Diagnostics.SpanFreeError.raise ~span
+    (Span.dummy () |> Span.owner_hint)
+    ThirImport kind
 
 let unimplemented ~issue_id (span : Thir.span list) (details : string) =
   let kind =
@@ -30,7 +32,9 @@ let unimplemented ~issue_id (span : Thir.span list) (details : string) =
         details = String.(if details = "" then None else Some details);
       }
   in
-  Diagnostics.SpanFreeError.raise ~span ThirImport kind
+  Diagnostics.SpanFreeError.raise ~span
+    (Span.dummy () |> Span.owner_hint)
+    ThirImport kind
 
 module Ast = struct
   include Ast

engine/lib/phase_utils.ml

@@ -113,7 +113,8 @@ end) : ERROR = struct
 
   let raise err =
     let span = Span.to_thir err.span in
-    Diagnostics.SpanFreeError.raise ~span Ctx.ctx err.kind
+    Diagnostics.SpanFreeError.raise ~span (Span.owner_hint err.span) Ctx.ctx
+      err.kind
 
   let unimplemented ?issue_id ?details span =
     raise

engine/lib/span.ml

@@ -150,7 +150,8 @@ let default = { id = 0; data = []; owner_hint = None }
 
 let owner_hint span =
   span.owner_hint
-  |> Option.bind ~f:(fun (OwnerId id) -> List.nth !owner_id_list id)
+  |> Option.map ~f:(fun (OwnerId id) ->
+         Option.value_exn (List.nth !owner_id_list id))
 
 let to_span2 span : Types.span2 =
   {

hax-types/src/diagnostics/mod.rs

@@ -5,7 +5,7 @@ pub mod message;
 pub mod report;
 
 #[derive_group(Serializers)]
-#[derive(Debug, Clone, JsonSchema)]
+#[derive(Debug, Clone, JsonSchema, Eq, PartialEq, Hash)]
 pub struct Diagnostics {
     pub kind: Kind,
     pub span: Vec<hax_frontend_exporter::Span>,
@@ -15,7 +15,6 @@ pub struct Diagnostics {
 
 impl std::fmt::Display for Diagnostics {
     fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
-        write!(f, "({}) ", self.context)?;
         match &self.kind {
             Kind::Unimplemented { issue_id, details } => write!(
                 f,
@@ -31,7 +30,7 @@ impl std::fmt::Display for Diagnostics {
             ),
             Kind::UnsupportedMacro { id } => write!(
                 f,
-                "The unexpanded macro {} it is not supported by this backend. Please verify the option you passed the {} (or {}) option.",
+                "The unexpanded macro {} it is not supported by this backend.\nPlease verify the option you passed the {} (or {}) option.",
                 id.bold(),
                 "--inline-macro-call".bold(), "-i".bold()
             ),
@@ -49,10 +48,9 @@ impl std::fmt::Display for Diagnostics {
             ),
             Kind::ExpectedMutRef => write!(
                 f,
-                "At this position, Hax was expecting an expression of the shape `&mut _`. Hax forbids `f(x)` (where `f` expects a mutable reference as input) when `x` is not a {}{} or when it is a dereference expression.
+                "At this position, Hax was expecting an expression of the shape `&mut _`.\nHax forbids `f(x)` (where `f` expects a mutable reference as input) when `x` is not a {}{} or when it is a dereference expression.
 
-{}
-",
+{}",
                 "place expression".bold(),
                 "[1]".bright_black(),
                 "[1]: https://doc.rust-lang.org/reference/expressions.html#place-expressions-and-value-expressions"
@@ -62,15 +60,53 @@ impl std::fmt::Display for Diagnostics {
                 "The bindings {:?} cannot be mutated here: they don't belong to the closure scope, and this is not allowed.",
                 bindings
             ),
-            Kind::ArbitraryLHS => write!(f, "Assignation of an arbitrary left-hand side is not supported. `lhs = e` is fine only when `lhs` is a combination of local identifiers, field accessors and index accessors."),
+            Kind::ArbitraryLHS => write!(f, "Assignation of an arbitrary left-hand side is not supported.\n`lhs = e` is fine only when `lhs` is a combination of local identifiers, field accessors and index accessors."),
 
             Kind::AttributeRejected {reason} => write!(f, "Here, this attribute cannot be used: {reason}."),
 
-            Kind::NonTrivialAndMutFnInput => write!(f, "The support in hax of function with one or more inputs of type `&mut _` is limited. Onlu trivial patterns are allowed there: `fn f(x: &mut (T, U)) ...` is allowed while `f((x, y): &mut (T, U))` is rejected."),
+            Kind::NonTrivialAndMutFnInput => write!(f, "The support in hax of function with one or more inputs of type `&mut _` is limited.\nOnly trivial patterns are allowed there: `fn f(x: &mut (T, U)) ...` is allowed while `f((x, y): &mut (T, U))` is rejected."),
 
             Kind::FStarParseError { fstar_snippet, details: _ } => write!(f, "The following code snippet could not be parsed as valid F*:\n```\n{fstar_snippet}\n```"),
 
             _ => write!(f, "{:?}", self.kind),
+        }?;
+        write!(f, "\n\n")?;
+        if let Some(issue) = self.kind.issue_number() {
+            write!(
+                f,
+                "This is discussed in issue https://github.com/hacspec/hax/issues/{issue}.\nPlease upvote or comment this issue if you see this error message."
+            )?;
+        }
+        write!(
+            f,
+            "{}",
+            format!(
+                "\nNote: the error was labeled with context `{}`.\n",
+                self.context
+            )
+            .bright_black()
+        )?;
+        Ok(())
+    }
+}
+
+impl Kind {
+    fn issue_number(&self) -> Option<u32> {
+        match self {
+            Kind::UnsafeBlock => None,
+            Kind::Unimplemented { issue_id, .. } => issue_id.clone(),
+            Kind::AssertionFailure { .. } => None,
+            Kind::UnallowedMutRef => Some(420),
+            Kind::UnsupportedMacro { .. } => None,
+            Kind::ErrorParsingMacroInvocation { .. } => None,
+            Kind::ClosureMutatesParentBindings { .. } => Some(1060),
+            Kind::ArbitraryLHS => None,
+            Kind::ExplicitRejection { .. } => None,
+            Kind::UnsupportedTupleSize { .. } => None,
+            Kind::ExpectedMutRef => Some(420),
+            Kind::NonTrivialAndMutFnInput => Some(1405),
+            Kind::AttributeRejected { .. } => None,
+            Kind::FStarParseError { .. } => todo!(),
         }
     }
 }

hax-types/src/diagnostics/report.rs

@@ -1,14 +1,15 @@
 use super::Diagnostics;
 use annotate_snippets::*;
 use miette::SourceOffset;
-use std::collections::HashMap;
+use std::collections::{HashMap, HashSet};
 use std::path::{Path, PathBuf};
 use std::rc::Rc;
 
 /// A context for reporting diagnostics
 #[derive(Clone, Debug, Default)]
 pub struct ReportCtx {
     files: HashMap<PathBuf, Rc<String>>,
+    seen: HashSet<Diagnostics>,
 }
 
 /// Translates a line and column position into an absolute offset
@@ -28,6 +29,11 @@ impl ReportCtx {
             })
             .clone()
     }
+
+    /// Check if `diagnostic` have been seen already, and mark `diagnostic` as seen.
+    pub fn seen_already(&mut self, diagnostic: Diagnostics) -> bool {
+        !self.seen.insert(diagnostic)
+    }
 }
 
 impl Diagnostics {

rustc-coverage-tests/snapshots/fstar/Coverage.Attr.Trait_impl_inherit.fst

@@ -3,7 +3,11 @@ module Coverage.Attr.Trait_impl_inherit
 open Core
 open FStar.Mul
 
-(* item error backend: (reject_TraitItemDefault) ExplicitRejection { reason: "a node of kind [Trait_item_default] have been found in the AST" }
+(* item error backend: ExplicitRejection { reason: "a node of kind [Trait_item_default] have been found in the AST" }
+
+
+Note: the error was labeled with context `reject_TraitItemDefault`.
+
 Last available AST for this item:
 
 #[<cfg>(any(feature = "json"))]#[feature(coverage_attribute)]#[<cfg>(any(feature = "json", feature = "lean", feature = "fstar", feature =

rustc-coverage-tests/snapshots/fstar/Coverage.Color.fst

@@ -4,7 +4,7 @@ open Core
 open FStar.Mul
 
 let main (_: Prims.unit) : (Prims.unit & Prims.unit) =
-  Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+  Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
     "{\n for _i in (core::iter::traits::collect::f_into_iter(core::ops::range::Range {\n f_start: 0,\n f_end: 0,\n })) {\n Tuple0\n }\n }"
   ,
   ()

rustc-coverage-tests/snapshots/fstar/Coverage.If_not.fst

@@ -58,11 +58,11 @@ let if_not (cond: bool) : Prims.unit =
 
 let main (_: Prims.unit) : (Prims.unit & Prims.unit) =
   let _:Prims.unit =
-    Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+    Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
       "{\n for _ in (core::iter::traits::collect::f_into_iter(core::ops::range::Range {\n f_start: 0,\n f_end: 8,\n })) {\n coverage::if_not::if_not(core::hint::black_box::<bool>(true))\n }\n }"
 
   in
-  Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+  Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
     "{\n for _ in (core::iter::traits::collect::f_into_iter(core::ops::range::Range {\n f_start: 0,\n f_end: 4,\n })) {\n coverage::if_not::if_not(core::hint::black_box::<bool>(false))\n }\n }"
   ,
   ()

rustc-coverage-tests/snapshots/fstar/Coverage.Inline.fst

@@ -24,7 +24,7 @@ let display
       (xs: t_Slice v_T)
     : Prims.unit =
   let _:Prims.unit =
-    Rust_primitives.Hax.failure "(FunctionalizeLoops) something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation"
+    Rust_primitives.Hax.failure "something is not implemented yet.This is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nLoop without mutation\n\nThis is discussed in issue https://github.com/hacspec/hax/issues/405.\nPlease upvote or comment this issue if you see this error message.\nNote: the error was labeled with context `FunctionalizeLoops`.\n"
       "{\n for x in (core::iter::traits::collect::f_into_iter(xs)) {\n {\n let args: [core::fmt::rt::t_Argument; 1] = {\n [core::fmt::rt::impl__new_display::<T>(x)]\n };\n {\n let _: tuple0 = {\n std::io::stdio::e_p..."
 
   in

rustc-coverage-tests/snapshots/fstar/Coverage.Inner_items.fst

@@ -35,7 +35,11 @@ type main__t_InStruct = { main__f_in_struct_field:u32 }
 
 let main__v_IN_CONST: u32 = mk_u32 1234
 
-(* item error backend: (reject_TraitItemDefault) ExplicitRejection { reason: "a node of kind [Trait_item_default] have been found in the AST" }
+(* item error backend: ExplicitRejection { reason: "a node of kind [Trait_item_default] have been found in the AST" }
+
+
+Note: the error was labeled with context `reject_TraitItemDefault`.
+
 Last available AST for this item:
 
 #[<cfg>(any(feature = "json", feature = "lean"))]#[allow(unused_assignments, unused_variables, dead_code)]#[feature(coverage_attribute)]#[allow(unused_attributes)]#[allow(dead_code)]#[allow(unreachable_code)]#[feature(register_tool)]#[register_tool(_hax)]trait main__t_InTrait<Self_>{#[_hax::json("\"TraitMethodNoPrePost\"")]fn main__f_trait_func_pre(_: Self,_: int) -> bool;