Merge pull request #1506 from cryspen/ocaml-spans-reviewable

Rust engine: Add spans to the Rust AST.

Author: W95Psp

engine/lib/export_ast.ml

@@ -241,7 +241,7 @@ module Make (FA : Features.T) = struct
             sub_pat = Option.map ~f:(fun (p, _) -> dpat p) subpat;
           }
 
-  and dspan (_span : span) : B.span = EmptyStructspan2
+  and dspan : span -> B.span = Span.to_span2
 
   and dbinding_mode (binding_mode : A.binding_mode) : B.binding_mode =
     match binding_mode with
@@ -458,12 +458,8 @@ module Make (FA : Features.T) = struct
     {
       attributes = List.map ~f:dattr p.attrs;
       pat = dpat p.pat;
-      ty =
-        {
-          ty = dty p.typ;
-          span =
-            EmptyStructspan2 (* Should use dspan, but what if option is None*);
-        };
+      ty = dty p.typ;
+      ty_span = Option.map ~f:dspan p.typ_span;
     }
 
   let dvariant (v : A.variant) : B.variant =
@@ -513,7 +509,7 @@ module Make (FA : Features.T) = struct
       meta = dmetadata ~attrs:ii.ii_attrs ii.ii_span;
     }
 
-  let ditem' (item : A.item') : B.item_kind =
+  let ditem' (item : A.item') (span : Types.span2) : B.item_kind =
     match item with
     | A.Fn { name; generics; body; params; safety } ->
         B.Fn
@@ -578,7 +574,7 @@ module Make (FA : Features.T) = struct
     | A.HaxError s ->
         let node : Types.fragment = Unknown "HaxError" in
         let info : B.diagnostic_info =
-          { context = Import; kind = Custom s; span = EmptyStructspan2 }
+          { context = Import; kind = Custom s; span }
         in
         Error { node; info }
     | A.NotImplementedYet -> B.NotImplementedYet
@@ -587,7 +583,7 @@ module Make (FA : Features.T) = struct
     [
       {
         ident = dconcrete_ident i.ident;
-        kind = ditem' i.v;
+        kind = ditem' i.v (dspan i.span);
         meta = dmetadata ~attrs:i.attrs i.span;
       };
     ]

engine/lib/span.ml

@@ -151,3 +151,13 @@ 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)
+
+let to_span2 span : Types.span2 =
+  {
+    data = List.map ~f:Imported.span_to_thir span.data;
+    id = Int.to_string span.id;
+    owner_hint =
+      Option.map
+        ~f:(fun (OwnerId n) -> Types.Newtypeowner_id (Int.to_string n))
+        span.owner_hint;
+  }

engine/lib/span.mli

@@ -34,3 +34,6 @@ 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. *)
+
+val to_span2 : t -> Types.span2
+(** Converts this span to a span2 for export to the Rust engine. *)

rust-printer/src/ast.rs

@@ -1173,7 +1173,9 @@ pub struct Param {
     /// The pattern part (left-hand side) of a parameter (`(mut x, y)` in the example).
     pub pat: Pat,
     /// The type part (right-rand side) of a parameter (`(T, u8)` in the example).
-    pub ty: SpannedTy,
+    pub ty: Ty,
+    /// The span of the type part (if available).
+    pub ty_span: Option<Span>,
     /// Optionally, some attributes present on the parameter.
     pub attributes: Attributes,
 }
@@ -1421,7 +1423,7 @@ pub mod traits {
     }
     impl<T: HasMetadata> HasSpan for T {
         fn span(&self) -> Span {
-            self.metadata().span
+            self.metadata().span.clone()
         }
     }
 
@@ -1474,7 +1476,7 @@ pub mod traits {
 
     impl HasSpan for SpannedTy {
         fn span(&self) -> Span {
-            self.span
+            self.span.clone()
         }
     }
 

rust-printer/src/ast/span.rs

@@ -2,15 +2,41 @@
 
 use hax_rust_engine_macros::*;
 
-// TODO: implement, interned (statically -- bumpalo or something)
-/// Position in the source code
+/// Creates a fresh identifier for a span.
+fn fresh_id() -> usize {
+    use std::sync::atomic::{AtomicUsize, Ordering};
+    static CURRENT_ID: AtomicUsize = AtomicUsize::new(0);
+    CURRENT_ID.fetch_add(1, Ordering::Relaxed)
+}
+
+/// Identifier used to track the origin Rust item of a span
 #[derive_group_for_ast]
-#[derive(Copy)]
-pub struct Span(());
+pub struct OwnerId(usize);
+
+/// Position of a Rust source
+#[derive_group_for_ast]
+pub struct Span {
+    /// A vector of spans as defined by the frontend.
+    /// This is useful for supporting in a trivial way union of spans.
+    data: Vec<hax_frontend_exporter::Span>,
+    /// A unique identifier. Since we store spans almost for every node of the
+    /// AST, having a unique identifier for spans gives us a fine-grained way of
+    /// refering to sub-nodes in debugging context. This id is indeed mostly
+    /// used by the web debugger.
+    id: usize,
+    /// A reference to the item in which this span lives. This information is
+    /// used for debugging and profiling purposes, e.g. for `cargo hax into
+    /// --stats backend`.
+    owner_hint: Option<OwnerId>,
+}
 
 impl From<hax_frontend_exporter::Span> for Span {
-    fn from(_span: hax_frontend_exporter::Span) -> Self {
-        Self(())
+    fn from(span: hax_frontend_exporter::Span) -> Self {
+        Self {
+            data: vec![span],
+            id: fresh_id(),
+            owner_hint: None, // TODO: this will be defined properly while addressing issue #1524
+        }
     }
 }