Merge branch 'main' into fstar-lib-additions

engine/backends/fstar/fstar_backend.ml

@@ -796,14 +796,35 @@ struct
         in
         F.mk_e_app effect (if is_lemma then args else typ :: args)
 
+  (** Prints doc comments out of a list of attributes *)
+  let pdoc_comments attrs =
+    attrs
+    |> List.filter_map ~f:(fun (attr : attr) ->
+           match attr.kind with
+           | DocComment { kind; body } -> Some (kind, body)
+           | _ -> None)
+    |> List.map ~f:(fun (kind, string) ->
+           match kind with
+           | DCKLine ->
+               String.split_lines string
+               |> List.map ~f:(fun s -> "///" ^ s)
+               |> String.concat_lines
+           | DCKBlock -> "(**" ^ string ^ "*)")
+    |> List.map ~f:(fun s -> `VerbatimIntf (s, `NoNewline))
+
   let rec pitem (e : item) :
       [> `Impl of F.AST.decl
       | `Intf of F.AST.decl
-      | `VerbatimImpl of string
-      | `VerbatimIntf of string
+      | `VerbatimImpl of string * [ `NoNewline | `Newline ]
+      | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
-    try pitem_unwrapped e
+    try
+      match pitem_unwrapped e with
+      | [] -> []
+      | printed_items ->
+          (* Print comments only for items that are being printed *)
+          pdoc_comments e.attrs @ printed_items
     with Diagnostics.SpanFreeError.Exn error ->
       let error = Diagnostics.SpanFreeError.payload error in
       let error = [%show: Diagnostics.Context.t * Diagnostics.kind] error in
@@ -816,8 +837,8 @@ struct
   and pitem_unwrapped (e : item) :
       [> `Impl of F.AST.decl
       | `Intf of F.AST.decl
-      | `VerbatimImpl of string
-      | `VerbatimIntf of string
+      | `VerbatimImpl of string * [ `NoNewline | `Newline ]
+      | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
     match e.v with
@@ -1283,10 +1304,13 @@ struct
                    "Malformed `Quote` item: could not find a ItemQuote payload")
           |> Option.value ~default:Types.{ intf = true; impl = false }
         in
-        (if fstar_opts.intf then [ `VerbatimIntf (pquote e.span quote) ]
+        (if fstar_opts.intf then
+         [ `VerbatimIntf (pquote e.span quote, `Newline) ]
         else [])
         @
-        if fstar_opts.impl then [ `VerbatimImpl (pquote e.span quote) ] else []
+        if fstar_opts.impl then
+          [ `VerbatimImpl (pquote e.span quote, `Newline) ]
+        else []
     | HaxError details ->
         [
           `Comment
@@ -1302,8 +1326,8 @@ module type S = sig
     item ->
     [> `Impl of F.AST.decl
     | `Intf of F.AST.decl
-    | `VerbatimImpl of string
-    | `VerbatimIntf of string
+    | `VerbatimImpl of string * [ `NoNewline | `Newline ]
+    | `VerbatimIntf of string * [ `NoNewline | `Newline ]
     | `Comment of string ]
     list
 end
@@ -1316,7 +1340,8 @@ let make (module M : Attrs.WITH_ITEMS) ctx =
             end) : S)
 
 let strings_of_item ~signature_only (bo : BackendOptions.t) m items
-    (item : item) : [> `Impl of string | `Intf of string ] list =
+    (item : item) :
+    ([> `Impl of string | `Intf of string ] * [ `NoNewline | `Newline ]) list =
   let interface_mode' : Types.inclusion_kind =
     List.rev bo.interfaces
     |> List.find ~f:(fun (clause : Types.inclusion_clause) ->
@@ -1353,26 +1378,44 @@ let strings_of_item ~signature_only (bo : BackendOptions.t) m items
   Print.pitem item
   |> List.filter ~f:(function `Impl _ when no_impl -> false | _ -> true)
   |> List.concat_map ~f:(function
-       | `Impl i -> [ mk_impl (decl_to_string i) ]
-       | `Intf i -> [ mk_intf (decl_to_string i) ]
-       | `VerbatimIntf s -> if interface_mode then [ `Intf s ] else [ `Impl s ]
-       | `VerbatimImpl s -> if interface_mode then [ `Impl s ] else [ `Impl s ]
+       | `Impl i -> [ (mk_impl (decl_to_string i), `Newline) ]
+       | `Intf i -> [ (mk_intf (decl_to_string i), `Newline) ]
+       | `VerbatimIntf (s, nl) ->
+           [ ((if interface_mode then `Intf s else `Impl s), nl) ]
+       | `VerbatimImpl (s, nl) ->
+           [ ((if interface_mode then `Impl s else `Impl s), nl) ]
        | `Comment s ->
            let s = "(* " ^ s ^ " *)" in
-           if interface_mode then [ `Impl s; `Intf s ] else [ `Impl s ])
+           if interface_mode then [ (`Impl s, `Newline); (`Intf s, `Newline) ]
+           else [ (`Impl s, `Newline) ])
 
 let string_of_items ~signature_only (bo : BackendOptions.t) m items :
     string * string =
   let strings =
     List.concat_map ~f:(strings_of_item ~signature_only bo m items) items
-    |> List.map ~f:(function
-         | `Impl s -> `Impl (String.strip s)
-         | `Intf s -> `Intf (String.strip s))
+    |> List.map
+         ~f:
+           ((function
+              | `Impl s -> `Impl (String.strip s)
+              | `Intf s -> `Intf (String.strip s))
+           *** Fn.id)
     |> List.filter
-         ~f:((function `Impl s | `Intf s -> String.is_empty s) >> not)
+         ~f:(fst >> (function `Impl s | `Intf s -> String.is_empty s) >> not)
   in
   let string_for filter =
-    List.filter_map ~f:filter strings |> String.concat ~sep:"\n\n"
+    let l =
+      List.filter_map
+        ~f:(fun (s, space) ->
+          let* s = filter s in
+          Some (s, space))
+        strings
+    in
+    let n = List.length l - 1 in
+    List.mapi
+      ~f:(fun i (s, space) ->
+        s ^ if [%matches? `NoNewline] space || [%eq: int] i n then "" else "\n")
+      l
+    |> String.concat ~sep:"\n"
   in
   ( string_for (function `Impl s -> Some s | _ -> None),
     string_for (function `Intf s -> Some s | _ -> None) )

engine/lib/import_thir.ml

@@ -101,6 +101,19 @@ let c_logical_op : Thir.logical_op -> logical_op = function
 let c_attr (attr : Thir.attribute) : attr =
   let kind =
     match attr.kind with
+    | DocComment (kind, body) ->
+        let kind =
+          match kind with Thir.Line -> DCKLine | Thir.Block -> DCKBlock
+        in
+        DocComment { kind; body }
+    | Normal
+        {
+          item =
+            { args = Eq (_, Hir { symbol; _ }); path = "doc"; tokens = None };
+          tokens = None;
+        } ->
+        DocComment { kind = DCKLine; body = symbol }
+        (* Looks for `#[doc = "something"]` *)
     | Normal { item = { args; path; tokens = subtokens }; tokens } ->
         let args_tokens =
           match args with Delimited { tokens; _ } -> Some tokens | _ -> None
@@ -110,11 +123,6 @@ let c_attr (attr : Thir.attribute) : attr =
           Option.value ~default:"" (args_tokens || tokens || subtokens)
         in
         Tool { path; tokens }
-    | DocComment (kind, body) ->
-        let kind =
-          match kind with Thir.Line -> DCKLine | Thir.Block -> DCKBlock
-        in
-        DocComment { kind; body }
   in
   { kind; span = Span.of_thir attr.span }
 
@@ -125,15 +133,14 @@ let c_item_attrs (attrs : Thir.item_attributes) : attrs =
      that parent/self structure in our AST. See
      https://github.com/hacspec/hax/issues/123. *)
   let self = c_attrs attrs.attributes in
-  let parent = c_attrs attrs.parent_attributes in
   let parent =
-    (* Repeating associateditem or uid is harmful *)
-    List.filter
-      ~f:(fun payload ->
+    c_attrs attrs.parent_attributes
+    |> List.filter ~f:([%matches? ({ kind = DocComment _; _ } : attr)] >> not)
+    |> (* Repeating associateditem or uid is harmful, same for comments *)
+    List.filter ~f:(fun payload ->
         match Attr_payloads.payloads [ payload ] with
         | [ ((Uid _ | AssociatedItem _), _) ] -> false
         | _ -> true)
-      parent
   in
   self @ parent
 

engine/names/extract/build.rs

@@ -123,7 +123,8 @@ fn target_dir(suffix: &str) -> camino::Utf8PathBuf {
 }
 
 fn get_json() -> String {
-    let mut cmd = Command::new("cargo-hax");
+    let mut cmd =
+        Command::new(std::env::var("HAX_CARGO_COMMAND_PATH").unwrap_or("cargo-hax".to_string()));
     cmd.args([
         "hax",
         "-C",

frontend/exporter/src/traits.rs

@@ -492,7 +492,7 @@ pub fn select_trait_candidate<'tcx, S: UnderOwnerState<'tcx>>(
         Ok(selection) => selection,
         Err(error) => fatal!(
             s,
-            "Cannot hanlde error `{:?}` selecting `{:?}`",
+            "Cannot handle error `{:?}` selecting `{:?}`",
             error,
             trait_ref
         ),

frontend/exporter/src/types/copied.rs

@@ -290,7 +290,7 @@ impl<'tcx, S: BaseState<'tcx>> SInto<S, DefId> for rustc_hir::hir_id::OwnerId {
 #[derive(
     AdtInto, Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
-#[args(<'tcx, S: UnderOwnerState<'tcx> + HasThir<'tcx>>, from: rustc_ast::ast::LitFloatType, state: S as gstate)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::LitFloatType, state: S as gstate)]
 pub enum LitFloatType {
     Suffixed(FloatTy),
     Unsuffixed,
@@ -660,7 +660,7 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto<S, Vec<GenericArg>>
 
 /// Reflects both [`rustc_middle::ty::subst::GenericArg`] and [`rustc_middle::ty::subst::GenericArgKind`]
 #[derive(AdtInto)]
-#[args(<'tcx, S: UnderOwnerState<'tcx> + HasThir<'tcx>>, from: rustc_ast::ast::LitIntType, state: S as gstate)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::LitIntType, state: S as gstate)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -1948,7 +1948,7 @@ pub enum StrStyle {
 
 /// Reflects [`rustc_ast::ast::LitKind`]
 #[derive(AdtInto)]
-#[args(<'tcx, S: UnderOwnerState<'tcx> + HasThir<'tcx>>, from: rustc_ast::ast::LitKind, state: S as gstate)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::LitKind, state: S as gstate)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -2000,22 +2000,48 @@ pub enum CommentKind {
 
 /// Reflects [`rustc_ast::ast::AttrArgs`]
 #[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::ast::AttrArgs, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrArgs, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
 pub enum AttrArgs {
     Empty,
     Delimited(DelimArgs),
 
+    Eq(Span, AttrArgsEq),
+    // #[todo]
+    // Todo(String),
+}
+
+/// Reflects [`rustc_ast::ast::AttrArgsEq`]
+#[derive(AdtInto)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrArgsEq, state: S as tcx)]
+#[derive(
+    Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
+)]
+pub enum AttrArgsEq {
+    Hir(MetaItemLit),
     #[todo]
-    Todo(String),
-    // Eq(Span, AttrArgsEq),
+    Ast(String),
+    // Ast(P<Expr>),
+}
+
+/// Reflects [`rustc_ast::ast::MetaItemLit`]
+#[derive(AdtInto)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::MetaItemLit, state: S as tcx)]
+#[derive(
+    Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
+)]
+pub struct MetaItemLit {
+    pub symbol: Symbol,
+    pub suffix: Option<Symbol>,
+    pub kind: LitKind,
+    pub span: Span,
 }
 
 /// Reflects [`rustc_ast::ast::AttrItem`]
 #[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::ast::AttrItem, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::AttrItem, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -2034,7 +2060,7 @@ impl<S> SInto<S, String> for rustc_ast::tokenstream::LazyAttrTokenStream {
 
 /// Reflects [`rustc_ast::ast::NormalAttr`]
 #[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::ast::NormalAttr, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::ast::NormalAttr, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]
@@ -2045,7 +2071,7 @@ pub struct NormalAttr {
 
 /// Reflects [`rustc_ast::AttrKind`]
 #[derive(AdtInto)]
-#[args(<S>, from: rustc_ast::AttrKind, state: S as tcx)]
+#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_ast::AttrKind, state: S as tcx)]
 #[derive(
     Clone, Debug, Serialize, Deserialize, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord,
 )]

test-harness/src/command_hax_ext.rs

@@ -33,9 +33,23 @@ impl CommandHaxExt for Command {
                 let root = std::env::current_dir().unwrap();
                 let root = root.parent().unwrap();
                 let engine_dir = root.join("engine");
-                // Make sure binaries are built
+                // Make sure binaries are built. Note this doesn't
+                // include `hax-engine-names-extract`: its build
+                // script requires the driver and CLI of `hax` to be
+                // available.
                 assert!(Command::new("cargo")
-                        .args(&["build", "--workspace", "--bins"])
+                            .args(&["build", "--bins"])
+                            .status()
+                            .unwrap()
+                            .success());
+                let cargo_hax = cargo_bin(CARGO_HAX);
+                let driver = cargo_bin("driver-hax-frontend-exporter");
+                // Now the driver & CLI are installed, call `cargo
+                // build` injecting their paths
+                assert!(Command::new("cargo")
+                        .args(&["build", "--workspace", "--bin", "hax-engine-names-extract"])
+                        .env("HAX_CARGO_COMMAND_PATH", &cargo_hax)
+                        .env("HAX_RUSTC_DRIVER_BINARY", &driver)
                         .status()
                         .unwrap()
                         .success());
@@ -49,8 +63,8 @@ impl CommandHaxExt for Command {
                         .unwrap()
                         .success());
                 Some(Paths {
-                    driver: cargo_bin("driver-hax-frontend-exporter"),
-                    cargo_hax: cargo_bin(CARGO_HAX),
+                    driver,
+                    cargo_hax,
                     engine: engine_dir.join("_build/install/default/bin/hax-engine"),
                 })
             };

test-harness/src/snapshots/toolchain__attributes into-fstar.snap

@@ -108,6 +108,10 @@ let v_MAX: usize = sz 10
 
 type t_MyArray = | MyArray : t_Array u8 (sz 10) -> t_MyArray
 
+/// Triple dash comment
+(** Multiline double star comment Maecenas blandit accumsan feugiat.
+    Done vitae ullamcorper est.
+    Curabitur id dui eget sem viverra interdum. *)
 let mutation_example
       (use_generic_update_at: t_MyArray)
       (use_specialized_update_at: t_Slice u8)
@@ -153,6 +157,8 @@ let u32_max: u32 = 90000ul
 
 unfold let some_function _ = "hello from F*"
 
+/// A doc comment on `add3`
+///another doc comment on add3
 let add3 (x y z: u32)
     : Prims.Pure u32
       (requires x >. 10ul && y >. 10ul && z >. 10ul && ((x +! y <: u32) +! z <: u32) <. u32_max)

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

@@ -34,12 +34,14 @@ open FStar.Mul
 
 class t_Trait (v_Self: Type) = { __marker_trait_t_Trait:Prims.unit }
 
+/// Indirect dependencies
 let main_a_a (_: Prims.unit) : Prims.unit = ()
 
 let main_a_b (_: Prims.unit) : Prims.unit = ()
 
 let main_a_c (_: Prims.unit) : Prims.unit = ()
 
+/// Direct dependencies
 let main_a (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T)
     : Prims.unit =
   let _:Prims.unit = main_a_a () in
@@ -76,6 +78,7 @@ type t_Foo = | Foo : t_Foo
 [@@ FStar.Tactics.Typeclasses.tcinstance]
 let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () }
 
+/// Entrypoint
 let main (_: Prims.unit) : Prims.unit =
   let _:Prims.unit = main_a (Foo <: t_Foo) in
   let _:Prims.unit = main_b () in