feat(engine): keep track of parent items in spans

cli/subcommands/src/cargo_hax.rs

@@ -7,6 +7,7 @@ use hax_types::driver_api::*;
 use hax_types::engine_api::*;
 use is_terminal::IsTerminal;
 use serde_jsonlines::BufReadExt;
+use std::collections::HashMap;
 use std::fs;
 use std::io::BufRead;
 use std::io::Write;
@@ -188,7 +189,7 @@ impl HaxMessage {
                     format!("{}.{}", n / factor, n % factor)
                 }
                 let title = format!(
-                    "[profiling] {}: {}ms, memory={}, {} item{}{}",
+                    "hax[profiling]: {}: {}ms, memory={}, {} item{}{}",
                     data.context,
                     format_with_dot(6, data.time_ns),
                     data.memory,
@@ -202,6 +203,17 @@ impl HaxMessage {
                 );
                 eprintln!("{}", renderer.render(Level::Info.title(&title)));
             }
+            Self::Stats { errors_per_item } => {
+                let success_items = errors_per_item.iter().filter(|(_, n)| *n == 0).count();
+                let total = errors_per_item.len();
+                let title = format!(
+                    "hax: {}/{} items were successfully translated ({}% success rate)",
+                    success_items,
+                    total,
+                    (success_items * 100) / total
+                );
+                eprintln!("{}", renderer.render(Level::Info.title(&title)));
+            }
             Self::CargoBuildFailure => {
                 let title =
                     "hax: running `cargo build` was not successful, continuing anyway.".to_string();
@@ -285,6 +297,7 @@ fn run_engine(
         });
 
         let stdout = std::io::BufReader::new(engine_subprocess.stdout.take().unwrap());
+        let mut errors_per_item: HashMap<_, usize> = HashMap::new();
         for msg in stdout.json_lines() {
             let msg = msg.expect(
                 "Hax engine sent an invalid json value. \
@@ -299,6 +312,9 @@ fn run_engine(
                     if backend.dry_run {
                         output.diagnostics.push(diagnostic.clone())
                     }
+                    if let Some(owner_id) = &diagnostic.owner_id {
+                        *errors_per_item.entry(owner_id.clone()).or_default() += 1;
+                    }
                     HaxMessage::Diagnostic {
                         diagnostic,
                         working_dir: working_dir.clone(),
@@ -339,11 +355,22 @@ fn run_engine(
                 FromEngine::ProfilingData(profiling_data) => {
                     HaxMessage::ProfilingData(profiling_data).report(message_format, None)
                 }
+                FromEngine::ItemProcessed(items) => {
+                    for item in items {
+                        errors_per_item.insert(item, 0);
+                    }
+                }
                 FromEngine::Ping => {
                     send!(&ToEngine::Pong);
                 }
             }
         }
+        if backend.stats {
+            HaxMessage::Stats {
+                errors_per_item: errors_per_item.into_iter().collect(),
+            }
+            .report(message_format, None)
+        }
         drop(stdin);
     }
 

engine/bin/lib.ml

@@ -73,6 +73,8 @@ let import_thir_items (include_clauses : Types.inclusion_clause list)
         match Attrs.status i.attrs with Included _ -> true | _ -> false)
       items
   in
+  Hax_io.write
+    (ItemProcessed (List.filter_map ~f:(fun i -> Span.owner_hint i.span) items));
   let items = Deps.sort items in
   (* Extract error reports for the items we actually extract *)
   let reports =

engine/lib/diagnostics.ml

@@ -67,11 +67,26 @@ type thir_span = T.span [@@deriving show, eq]
 let compare_thir_span (a : thir_span) (b : thir_span) =
   [%compare: string] ([%show: thir_span] a) ([%show: thir_span] b)
 
-type t = { context : Context.t; kind : kind; span : thir_span list }
+type thir_def_id = T.def_id [@@deriving show, eq]
+
+let compare_thir_def_id (a : thir_def_id) (b : thir_def_id) =
+  [%compare: string] ([%show: thir_def_id] a) ([%show: thir_def_id] b)
+
+type t = {
+  context : Context.t;
+  kind : kind;
+  span : thir_span list;
+  owner_id : thir_def_id option;
+}
 [@@deriving show, eq, compare]
 
 let to_thir_diagnostic (d : t) : Types.diagnostics =
-  { kind = d.kind; context = Context.display d.context; span = d.span }
+  {
+    kind = d.kind;
+    context = Context.display d.context;
+    span = d.span;
+    owner_id = d.owner_id;
+  }
 
 (** Ask `cargo-hax` to pretty print a diagnostic *)
 let ask_diagnostic_pretty_print diag : string =
@@ -86,7 +101,7 @@ let pretty_print : t -> string =
 let pretty_print_context_kind : Context.t -> kind -> string =
  fun context kind ->
   let span = Span.to_thir (Span.dummy ()) in
-  pretty_print { context; kind; span }
+  pretty_print { context; kind; span; owner_id = None }
 
 module Core : sig
   val raise_fatal_error : 'never. t -> 'never
@@ -122,7 +137,8 @@ end
 include Core
 
 let failure ~context ~span kind =
-  Core.raise_fatal_error { context; kind; span = Span.to_thir span }
+  Core.raise_fatal_error
+    { context; kind; span = Span.to_thir span; owner_id = Span.owner_hint span }
 
 module SpanFreeError : sig
   type t = private Data of Context.t * kind [@@deriving show]
@@ -142,6 +158,6 @@ end = struct
     raise (Exn (Data (ctx, kind)))
 
   let raise ?(span = []) (ctx : Context.t) (kind : kind) =
-    report { span; kind; context = ctx };
+    report { span; kind; context = ctx; owner_id = None };
     raise_without_reporting ctx kind
 end

engine/lib/import_thir.ml

@@ -1441,7 +1441,9 @@ let cast_of_enum typ_name generics typ thir_span
   { v; span; ident; attrs = [] }
 
 let rec c_item ~ident ~drop_body (item : Thir.item) : item list =
-  try c_item_unwrapped ~ident ~drop_body item
+  try
+    Span.with_owner_hint item.owner_id (fun _ ->
+        c_item_unwrapped ~ident ~drop_body item)
   with Diagnostics.SpanFreeError.Exn payload ->
     let context, kind = Diagnostics.SpanFreeError.payload payload in
     let error = Diagnostics.pretty_print_context_kind context kind in

engine/lib/print_rust.ml

@@ -140,6 +140,7 @@ module Raw = struct
                      ident";
                 };
             span = Span.to_thir span;
+            owner_id = Span.owner_hint span;
           };
         "print_rust_last_of_global_ident_error"
 

engine/lib/span.ml

@@ -93,26 +93,61 @@ module Imported = struct
     "<" ^ file ^ " " ^ display_loc s.lo ^ "→" ^ display_loc s.hi ^ ">"
 end
 
-type t = { id : int; data : Imported.span list }
+type owner_id = OwnerId of int
 [@@deriving show, yojson, sexp, compare, eq, hash]
 
-let display { id = _; data } =
+let owner_id_list = ref []
+
+let fresh_owner_id (owner : Types.def_id) : owner_id =
+  let next_id = OwnerId (List.length !owner_id_list) in
+  owner_id_list := owner :: !owner_id_list;
+  next_id
+
+(** This state changes the behavior of `of_thir`: the hint placed into
+this state will be inserted automatically by `of_thir`. The field
+`owner_hint` shall be used solely for reporting to the user, not for
+any logic within the engine. *)
+let state_owner_hint : owner_id option ref = ref None
+
+let with_owner_hint (type t) (owner : Types.def_id) (f : unit -> t) : t =
+  let previous = !state_owner_hint in
+  state_owner_hint := Some (fresh_owner_id owner);
+  let result = f () in
+  state_owner_hint := previous;
+  result
+
+type t = { id : int; data : Imported.span list; owner_hint : owner_id option }
+[@@deriving show, yojson, sexp, compare, eq, hash]
+
+let display { id = _; data; _ } =
   match data with
   | [] -> "<dummy>"
   | [ span ] -> Imported.display_span span
   | spans -> List.map ~f:Imported.display_span spans |> String.concat ~sep:"∪"
 
 let of_thir span =
-  { data = [ Imported.span_of_thir span ]; id = FreshId.make () }
+  {
+    data = [ Imported.span_of_thir span ];
+    id = FreshId.make ();
+    owner_hint = !state_owner_hint;
+  }
 
 let to_thir { data; _ } = List.map ~f:Imported.span_to_thir data
 
 let union_list spans =
   let data = List.concat_map ~f:(fun { data; _ } -> data) spans in
-  { data; id = FreshId.make () }
+  let owner_hint = List.hd spans |> Option.bind ~f:(fun s -> s.owner_hint) in
+  { data; id = FreshId.make (); owner_hint }
 
 let union x y = union_list [ x; y ]
-let dummy () = { id = FreshId.make (); data = [] }
+
+let dummy () =
+  { id = FreshId.make (); data = []; owner_hint = !state_owner_hint }
+
 let id_of { id; _ } = id
 let refresh_id span = { span with id = FreshId.make () }
-let default = { id = 0; data = [] }
+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)

engine/lib/span.mli

@@ -1,12 +1,36 @@
-(* type loc [@@deriving show, yojson, sexp, compare, eq, hash] *)
 type t [@@deriving show, yojson, sexp, compare, eq, hash]
 
 val display : t -> string
+
 val of_thir : Types.span -> t
+(** Imports a THIR span as a hax span *)
+
 val to_thir : t -> Types.span list
+(** Exports a hax span to THIR spans (a hax span might be a collection of spans) *)
+
 val union_list : t list -> t
 val union : t -> t -> t
+
 val dummy : unit -> t
+(** Generates a dummy span: this should be avoided at all cost. *)
+
 val id_of : t -> int
+(** Lookup the internal unique identifier of a span. *)
+
 val refresh_id : t -> t
+(** Replaces the internal identifier by a fresh one. This can be useful for debugging. *)
+
 val default : t
+(** A default span can be useful when a span is required in some
+computation that never reports error and when we know the span will go
+away. Using this should be avoided. *)
+
+val with_owner_hint : Types.def_id -> (unit -> 't) -> 't
+(** Inserts a hint about the fact that, in function `f`, we're
+translating spans that are "owned" by an item `owner`. This should be
+used only in `import_thir`, also, the hint shall be used only to
+enhance user reporting, not for any logic within the engine. *)
+
+val owner_hint : t -> Types.def_id option
+(** Looks up the owner hint for a span. This should be used for user
+reports only. *)

engine/names/extract/build.rs

@@ -18,7 +18,7 @@ mod id_table {
     #[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Serialize, Deserialize)]
     pub struct Node<T> {
         value: Arc<T>,
-        cache_id: u32,
+        id: u32,
     }
 
     impl<T> std::ops::Deref for Node<T> {

engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js

@@ -582,11 +582,11 @@ let parse_table_id_node (type t) (name: string) (encode: t -> map_types) (decode
     let label = "parse_table_id_node:" ^ name ^ ": " in
     match o with
     | \`Assoc alist -> begin
-          let id = match List.assoc_opt "cache_id" alist with
+          let id = match List.assoc_opt "id" alist with
             | Some (\`Int id) -> Base.Int.to_int64 id
             | Some (\`Intlit lit) -> (try Base.Int64.of_string lit with | _ -> failwith (label ^ "Base.Int64.of_string failed for " ^ lit))
             | Some bad_json -> failwith (label ^ "id was expected to be an int, got: " ^ Yojson.Safe.pretty_to_string bad_json ^ "\n\n\nfull json: " ^ Yojson.Safe.pretty_to_string o)
-            | None -> failwith (label ^ " could not find the key 'cache_id' in the following json: " ^ Yojson.Safe.pretty_to_string o)
+            | None -> failwith (label ^ " could not find the key 'id' in the following json: " ^ Yojson.Safe.pretty_to_string o)
           in
           let decode v = decode v |> Base.Option.value_exn ~message:(label ^ "could not decode value (wrong type)") in
           match List.assoc_opt "value" alist with

frontend/exporter/src/id_table.rs

@@ -272,7 +272,7 @@ mod serde_repr {
 
     #[derive(Serialize, Deserialize, JsonSchema, Debug)]
     pub(super) struct NodeRepr<T> {
-        cache_id: Id,
+        id: Id,
         value: Option<Arc<T>>,
     }
 
@@ -290,8 +290,8 @@ mod serde_repr {
             } else {
                 Some(self.value.clone())
             };
-            let cache_id = self.id;
-            NodeRepr { value, cache_id }
+            let id = self.id;
+            NodeRepr { value, id }
         }
     }
 
@@ -301,7 +301,7 @@ mod serde_repr {
         fn try_from(cached: NodeRepr<T>) -> Result<Self, Self::Error> {
             use serde::de::Error;
             let table = DESERIALIZATION_STATE.lock().unwrap();
-            let id = cached.cache_id;
+            let id = cached.id;
             let kind = if let Some(kind) = cached.value {
                 kind
             } else {

hax-types/src/cli_options/mod.rs

@@ -308,8 +308,14 @@ pub struct BackendOptions<E: Extension> {
     #[arg(short, long, action = clap::ArgAction::Count)]
     pub verbose: u8,
 
-    /// Enables profiling for the engine
-    #[arg(short, long)]
+    /// Prints statistics about how many items have been translated
+    /// successfully by the engine.
+    #[arg(long)]
+    pub stats: bool,
+
+    /// Enables profiling for the engine: for each phase of the
+    /// engine, time and memory usage are recorded and reported.
+    #[arg(long)]
     pub profile: bool,
 
     /// Enable engine debugging: dumps the AST at each phase.

hax-types/src/diagnostics/message.rs

@@ -24,6 +24,9 @@ pub enum HaxMessage {
         backend: Backend<()>,
     } = 4,
     ProfilingData(crate::engine_api::ProfilingData) = 5,
+    Stats {
+        errors_per_item: Vec<(hax_frontend_exporter::DefId, usize)>,
+    } = 6,
 }
 
 impl HaxMessage {

hax-types/src/diagnostics/mod.rs

@@ -10,6 +10,7 @@ pub struct Diagnostics {
     pub kind: Kind,
     pub span: Vec<hax_frontend_exporter::Span>,
     pub context: String,
+    pub owner_id: Option<hax_frontend_exporter::DefId>,
 }
 
 impl std::fmt::Display for Diagnostics {

hax-types/src/engine_api.rs

@@ -79,6 +79,7 @@ pub struct ProfilingData {
 
 pub mod protocol {
     use super::*;
+
     #[derive_group(Serializers)]
     #[derive(JsonSchema, Debug, Clone)]
     pub enum FromEngine {
@@ -88,6 +89,8 @@ pub mod protocol {
         PrettyPrintRust(String),
         DebugString(String),
         ProfilingData(ProfilingData),
+        /// Declares a list of items that will be processed by the engine
+        ItemProcessed(Vec<hax_frontend_exporter::DefId>),
         Exit,
         Ping,
     }

test-harness/src/snapshots/toolchain__include-flag into-coq.snap

@@ -56,7 +56,7 @@ Class t_Trait `{v_Self : Type} : Type :=
 Arguments t_Trait:clear implicits.
 Arguments t_Trait (_).
 
-Instance t_Trait_187936720 : t_Trait ((t_Foo)) :=
+Instance t_Trait_254780795 : t_Trait ((t_Foo)) :=
   {
   }.