From d59f84ce01d8381d7df014df1b098f448d28f29c Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 23 Apr 2024 10:13:43 +0200 Subject: [PATCH] feat: add support for `#[doc="..."]` attributes --- engine/backends/fstar/fstar_backend.ml | 77 ++++++++++++++----- engine/lib/import_thir.ml | 27 ++++--- frontend/exporter/src/types/copied.rs | 30 +++++++- .../toolchain__attributes into-fstar.snap | 6 ++ .../toolchain__generics into-fstar.snap | 1 + .../toolchain__include-flag into-fstar.snap | 3 + .../toolchain__interface-only into-fstar.snap | 9 +++ .../toolchain__naming into-fstar.snap | 14 ++++ .../toolchain__side-effects into-fstar.snap | 10 ++- tests/attributes/src/lib.rs | 6 ++ 10 files changed, 151 insertions(+), 32 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index cb365d4e1..ec91d8bb5 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -799,8 +799,8 @@ struct 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 @@ -816,10 +816,27 @@ 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 = + let doc_comments = + e.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)) + in + doc_comments + @ match e.v with | Alias { name; item } -> let pat = @@ -1272,10 +1289,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 @@ -1291,8 +1311,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 @@ -1305,7 +1325,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) -> @@ -1342,26 +1363,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) ) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 376a1c87a..5d1db99fc 100644 --- a/engine/lib/import_thir.ml +++ b/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 diff --git a/frontend/exporter/src/types/copied.rs b/frontend/exporter/src/types/copied.rs index d9488b389..60a2aba72 100644 --- a/frontend/exporter/src/types/copied.rs +++ b/frontend/exporter/src/types/copied.rs @@ -2008,9 +2008,35 @@ 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), +} + +/// 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, + pub kind: LitKind, + pub span: Span, } /// Reflects [`rustc_ast::ast::AttrItem`] diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index bfeaf0a6c..6998ed94e 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/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) diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index eee521479..6892c3613 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap @@ -63,6 +63,7 @@ let impl_Foo_for_usize: t_Foo usize = f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N } +/// Test defaults types and constants let dup (#v_T: Type) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T) (x: v_T) : (v_T & v_T) = Core.Clone.f_clone x, Core.Clone.f_clone x <: (v_T & v_T) diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap index 86e4eb07f..759bc8f1d 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap +++ b/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 diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap index 9d392ab5e..b3a95740d 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -35,6 +35,11 @@ module Interface_only open Core open FStar.Mul +/// This item contains unsafe blocks and raw references, two features +/// not supported by hax. Thanks to the `-i` flag and the `+:` +/// modifier, `f` is still extractable as an interface. +/// Expressions within type are still extracted, as well as pre- and +/// post-conditions. val f (x: u8) : Prims.Pure (t_Array u8 (sz 4)) (requires x <. 254uy) @@ -45,6 +50,9 @@ val f (x: u8) type t_Bar = | Bar : t_Bar +/// Non-inherent implementations are extracted, their bodies are not +/// dropped. This might be a bit surprising: see +/// https://github.com/hacspec/hax/issues/616. [@@ FStar.Tactics.Typeclasses.tcinstance] let impl: Core.Convert.t_From t_Bar Prims.unit = { @@ -55,6 +63,7 @@ let impl: Core.Convert.t_From t_Bar Prims.unit = val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True) +/// If you need to drop the body of a method, please hoist it: [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_1: Core.Convert.t_From t_Bar u8 = { diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index abfe8b043..b679b28e8 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -32,6 +32,8 @@ module Naming.Ambiguous_names open Core open FStar.Mul +/// This macro surround a given expression with a let binding for +/// an identifier `a` and a print of that `a`. let debug (label value: u32) : Prims.unit = let _:Prims.unit = Std.Io.Stdio.v__print (Core.Fmt.impl_2__new_v1 (Rust_primitives.unsize (let list = @@ -56,6 +58,7 @@ let debug (label value: u32) : Prims.unit = in () +/// `f` stacks mutliple let bindings declaring different `a`s. let f (_: Prims.unit) : Prims.unit = let a_1_:u32 = 104ul in let a_2_:u32 = 205ul in @@ -66,6 +69,13 @@ let f (_: Prims.unit) : Prims.unit = let _:Prims.unit = debug 1ul a_1_ in debug 4ul a +/// `f` is expanded into `f_expand` below, while the execution of `f` gives: +/// ```plaintext +/// [3] a=306 +/// [2] a=205 +/// [1] a=104 +/// [last] a=123 +/// ``` let ff_expand (_: Prims.unit) : Prims.unit = let a:i32 = 104l in let a:i32 = 205l in @@ -117,6 +127,10 @@ class t_T3_e_for_a (v_Self: Type) = { __marker_trait_t_T3_e_for_a:Prims.unit } [@@ FStar.Tactics.Typeclasses.tcinstance] let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () } +/// Test for ambiguous local names renaming: when two local vars are +/// ambiguous by name but not by their internal IDs. +/// Such situation can occur playing with *hygenic* macros. +/// Also, this happens with some internal Rustc rewrite. (e.g. assignment of tuples) let v_INHERENT_CONSTANT: usize = sz 3 let constants diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap index 5ae7f9b1a..ee3c46e86 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -1,6 +1,5 @@ --- source: test-harness/src/harness.rs -assertion_line: 214 expression: snapshot info: kind: @@ -36,15 +35,18 @@ module Side_effects open Core open FStar.Mul +/// Helper function let add3 (x y z: u32) : u32 = Core.Num.impl__u32__wrapping_add (Core.Num.impl__u32__wrapping_add x y <: u32) z +/// Question mark without error coercion let direct_result_question_mark (y: Core.Result.t_Result Prims.unit u32) : Core.Result.t_Result i8 u32 = match y with | Core.Result.Result_Ok _ -> Core.Result.Result_Ok 0y <: Core.Result.t_Result i8 u32 | Core.Result.Result_Err err -> Core.Result.Result_Err err <: Core.Result.t_Result i8 u32 +/// Question mark with an error coercion let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16) : Core.Result.t_Result i8 u32 = match y with @@ -52,6 +54,7 @@ let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16) | Core.Result.Result_Err err -> Core.Result.Result_Err (Core.Convert.f_from err) <: Core.Result.t_Result i8 u32 +/// Exercise early returns with control flow and loops let early_returns (x: u32) : u32 = Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! _:Prims.unit = if x >. 3ul @@ -104,6 +107,7 @@ let early_returns (x: u32) : u32 = <: Core.Ops.Control_flow.t_ControlFlow u32 u32) +/// Exercise local mutation with control flow and loops let local_mutation (x: u32) : u32 = let y:u32 = 0ul in let x:u32 = Core.Num.impl__u32__wrapping_add x 1ul in @@ -144,6 +148,7 @@ let local_mutation (x: u32) : u32 = let x:u32 = hoist15 in Core.Num.impl__u32__wrapping_add x y +/// Test question mark on `Option`s with some control flow let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core.Option.t_Option u8 = Rust_primitives.Hax.Control_flow_monad.Mexception.run (match x with | Core.Option.Option_Some hoist19 -> @@ -249,6 +254,7 @@ let options (x y: Core.Option.t_Option u8) (z: Core.Option.t_Option u64) : Core. <: Core.Ops.Control_flow.t_ControlFlow (Core.Option.t_Option u8) (Core.Option.t_Option u8)) +/// Test question mark on `Result`s with local mutation let question_mark (x: u32) : Core.Result.t_Result u32 u32 = Rust_primitives.Hax.Control_flow_monad.Mexception.run (let! x:u32 = if x >. 40ul @@ -300,6 +306,7 @@ type t_Bar = { f_b:(t_Array (bool & bool) (sz 6) & bool) } +/// Combine `?` and early return let monad_lifting (x: u8) : Core.Result.t_Result t_A t_B = Rust_primitives.Hax.Control_flow_monad.Mexception.run (if x >. 123uy <: bool then @@ -336,6 +343,7 @@ type t_Foo = { f_bar:t_Bar } +/// Test assignation on non-trivial places let assign_non_trivial_lhs (foo: t_Foo) : t_Foo = let foo:t_Foo = { foo with f_x = true } <: t_Foo in let foo:t_Foo = { foo with f_bar = { foo.f_bar with f_a = true } <: t_Bar } <: t_Foo in diff --git a/tests/attributes/src/lib.rs b/tests/attributes/src/lib.rs index cab615b18..76a05cd69 100644 --- a/tests/attributes/src/lib.rs +++ b/tests/attributes/src/lib.rs @@ -3,6 +3,8 @@ use hax_lib as hax; // dummy max value const u32_max: u32 = 90000; +/// A doc comment on `add3` +#[doc = "another doc comment on add3"] #[hax::requires(x > 10 && y > 10 && z > 10 && x + y + z < u32_max)] #[hax::ensures(|result| hax_lib::implies(true, || result > 32))] fn add3(x: u32, y: u32, z: u32) -> u32 { @@ -84,6 +86,10 @@ mod refined_indexes { } } + /// Triple dash comment + /** Multiline double star comment Maecenas blandit accumsan feugiat. + Done vitae ullamcorper est. + Curabitur id dui eget sem viverra interdum. */ fn mutation_example( use_generic_update_at: &mut MyArray, use_specialized_update_at: &mut [u8],