Translate test attribute

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.236"
+let supported_charon_version = "0.1.237"

charon-ml/src/PrintFmt.ml

@@ -1101,6 +1101,106 @@ let pp_generic_params_single_line (env : fmt_env) (fmt : Format.formatter)
 let generic_params_to_string_single_line env generics =
   pp_to_string (fun fmt -> pp_generic_params_single_line env fmt generics)
 
+(** Print a built-in attribute the way it is written in the source. *)
+let pp_rustc_attribute_kind (fmt : Format.formatter)
+    (kind : rustc_attribute_kind) : unit =
+  match kind with
+  | RustcAttributeKindAutomaticallyDerived ->
+      pp_string fmt "automatically_derived"
+  | RustcAttributeKindCold -> pp_string fmt "cold"
+  | RustcAttributeKindDeprecated (deprecation, _) ->
+      pp_string fmt "deprecated";
+      let since =
+        match deprecation.since with
+        | RustcDeprecatedSinceRustcVersion v ->
+            Some (Printf.sprintf "%d.%d.%d" v.major v.minor v.patch)
+        | RustcDeprecatedSinceFuture -> Some "future"
+        | RustcDeprecatedSinceNonStandard since -> Some since
+        | RustcDeprecatedSinceUnspecified | RustcDeprecatedSinceErr -> None
+      in
+      let since = Option.map (fun since -> "since = \"" ^ since ^ "\"") since in
+      let note =
+        Option.map
+          (fun (note : rustc_ident) -> "note = \"" ^ note.name ^ "\"")
+          deprecation.note
+      in
+      let args = List.filter_map (fun x -> x) [ since; note ] in
+      if args <> [] then Format.fprintf fmt "(%s)" (String.concat ", " args)
+  | RustcAttributeKindFundamental -> pp_string fmt "fundamental"
+  | RustcAttributeKindIgnore (_, reason) ->
+      pp_string fmt "ignore";
+      Option.iter (fun reason -> Format.fprintf fmt " = \"%s\"" reason) reason
+  | RustcAttributeKindInline (inline, _) -> (
+      match inline with
+      | RustcInlineAttrNone -> pp_string fmt "inline"
+      | RustcInlineAttrHint -> pp_string fmt "inline(hint)"
+      | RustcInlineAttrAlways -> pp_string fmt "inline(always)"
+      | RustcInlineAttrNever -> pp_string fmt "inline(never)"
+      | RustcInlineAttrForce _ -> pp_string fmt "rustc_force_inline")
+  | RustcAttributeKindMayDangle _ -> pp_string fmt "may_dangle"
+  | RustcAttributeKindNaked _ -> pp_string fmt "naked"
+  | RustcAttributeKindNoLink -> pp_string fmt "no_link"
+  | RustcAttributeKindNoMangle _ -> pp_string fmt "no_mangle"
+  | RustcAttributeKindNonExhaustive _ -> pp_string fmt "non_exhaustive"
+  | RustcAttributeKindOptimize (optimize, _) -> (
+      match optimize with
+      | RustcOptimizeAttrDefault -> pp_string fmt "optimize(default)"
+      | RustcOptimizeAttrDoNotOptimize -> pp_string fmt "optimize(none)"
+      | RustcOptimizeAttrSpeed -> pp_string fmt "optimize(speed)"
+      | RustcOptimizeAttrSize -> pp_string fmt "optimize(size)")
+  | RustcAttributeKindRustcAlign (align, _) ->
+      Format.fprintf fmt "rustc_align(%d)" align
+  | RustcAttributeKindRustcIntrinsic -> pp_string fmt "rustc_intrinsic"
+  | RustcAttributeKindRustcTestEntrypointMarker ->
+      pp_string fmt "rustc_test_entrypoint_marker"
+  | RustcAttributeKindShouldPanic reason ->
+      pp_string fmt "should_panic";
+      Option.iter
+        (fun reason -> Format.fprintf fmt "(expected = \"%s\")" reason)
+        reason
+  | RustcAttributeKindTargetFeature (features, _, _) ->
+      let features = List.map (fun (feature, _) -> feature) features in
+      Format.fprintf fmt "target_feature(enable = \"%s\")"
+        (String.concat "," features)
+  | RustcAttributeKindTrackCaller _ -> pp_string fmt "track_caller"
+
+let pp_item_id (env : fmt_env) (fmt : Format.formatter) (id : item_id) : unit =
+  match find_short_name env id with
+  | Some name -> pp_name env fmt name
+  | None -> pp_string fmt (item_id_to_pretty_string id)
+
+let pp_attribute_unindented (env : fmt_env) (fmt : Format.formatter)
+    (attr : attribute) : unit =
+  match attr with
+  | AttrOpaque -> pp_string fmt "#[charon::opaque]"
+  | AttrExclude -> pp_string fmt "#[charon::exclude]"
+  | AttrRename name -> Format.fprintf fmt "#[charon::rename(\"%s\")]" name
+  | AttrVariantsPrefix prefix ->
+      Format.fprintf fmt "#[charon::variants_prefix(\"%s\")]" prefix
+  | AttrVariantsSuffix suffix ->
+      Format.fprintf fmt "#[charon::variants_suffix(\"%s\")]" suffix
+  | AttrTransparent -> pp_string fmt "#[charon::transparent]"
+  | AttrIsPrecondition id ->
+      Format.fprintf fmt "#[charon::precondition] // of %a" (pp_item_id env) id
+  | AttrIsPostcondition id ->
+      Format.fprintf fmt "#[charon::postcondition] // of %a" (pp_item_id env) id
+  | AttrHasPrecondition id ->
+      Format.fprintf fmt "// precondition: %a" (pp_item_id env) (IdFun id)
+  | AttrHasPostcondition id ->
+      Format.fprintf fmt "// postcondition: %a" (pp_item_id env) (IdFun id)
+  | AttrDocComment comment ->
+      let lines = String.split_on_char '\n' comment in
+      pp_sep_list "\n" pp_string fmt (List.map (fun line -> "///" ^ line) lines)
+  | AttrBuiltin kind -> Format.fprintf fmt "#[%a]" pp_rustc_attribute_kind kind
+  | AttrUnknown attr -> Format.fprintf fmt "#[%a]" pp_raw_attribute attr
+
+let pp_attribute (env : fmt_env) (indent : string) (fmt : Format.formatter)
+    (attr : attribute) : unit =
+  (* An attribute may span several lines: the caller indents the first line, we
+     indent the subsequent ones ourselves. *)
+  let attr = pp_to_string (fun fmt -> pp_attribute_unindented env fmt attr) in
+  pp_sep_list ("\n" ^ indent) pp_string fmt (String.split_on_char '\n' attr)
+
 let pp_item_intro (env : fmt_env) (indent : string) (keyword : string)
     (id : item_id) (fmt : Format.formatter) (meta : item_meta) : unit =
   let full_name = full_name_to_string env meta.name in
@@ -1110,6 +1210,20 @@ let pp_item_intro (env : fmt_env) (indent : string) (keyword : string)
         (name_to_string env short_name, "// Full name: " ^ full_name ^ "\n")
     | None -> (full_name, "")
   in
+  let attributes =
+    List.filter_map
+      (fun attr ->
+        (* Doc-comments are long and don't affect the semantics; skip them. *)
+        match attr with
+        | AttrDocComment _ -> None
+        | _ ->
+            Some
+              (indent
+              ^ pp_to_string (fun fmt -> pp_attribute env indent fmt attr)
+              ^ "\n"))
+      meta.attr_info.attributes
+    |> String.concat ""
+  in
   let lang_item =
     match meta.lang_item with
     | None -> ""
@@ -1130,7 +1244,7 @@ let pp_item_intro (env : fmt_env) (indent : string) (keyword : string)
     | Some id -> indent ^ "#[diagnostic_item(\"" ^ id ^ "\")]\n"
   in
   let public = if meta.attr_info.public then "pub " else "" in
-  Format.fprintf fmt "%s%s%s%s%s%s %s" full_name_comment lang_item
+  Format.fprintf fmt "%s%s%s%s%s%s%s %s" full_name_comment attributes lang_item
     diagnostic_item indent public keyword name
 
 let item_intro_to_string env indent keyword id meta =

charon-ml/src/generated/Generated_Meta.ml

@@ -205,9 +205,9 @@ and rustc_attribute_kind =
           Fields:
           - [align]
           - [span] *)
-  | RustcAttributeKindRustcDiagnosticItem of string
-      (** Represents [#[rustc_diagnostic_item]] *)
   | RustcAttributeKindRustcIntrinsic  (** Represents [#[rustc_intrinsic]] *)
+  | RustcAttributeKindRustcTestEntrypointMarker
+      (** Represents [#[rustc_test_entrypoint_marker]] *)
   | RustcAttributeKindShouldPanic of string option
       (** Represents [#[should_panic]]
 

charon-ml/src/generated/Generated_OfJson.ml

@@ -2079,10 +2079,9 @@ and rustc_attribute_kind_of_json (ctx : of_json_ctx) (js : json) :
         let* align = int_of_json ctx align in
         let* span = span_of_json ctx span in
         Ok (RustcAttributeKindRustcAlign (align, span))
-    | `Assoc [ ("RustcDiagnosticItem", _0) ] ->
-        let* _0 = string_of_json ctx _0 in
-        Ok (RustcAttributeKindRustcDiagnosticItem _0)
     | `String "RustcIntrinsic" -> Ok RustcAttributeKindRustcIntrinsic
+    | `String "RustcTestEntrypointMarker" ->
+        Ok RustcAttributeKindRustcTestEntrypointMarker
     | `Assoc [ ("ShouldPanic", `Assoc [ ("reason", reason) ]) ] ->
         let* reason = option_of_json string_of_json ctx reason in
         Ok (RustcAttributeKindShouldPanic reason)

charon-ml/src/generated/Generated_OfPostcard.ml

@@ -1818,10 +1818,8 @@ and rustc_attribute_kind_of_postcard (ctx : of_postcard_ctx)
          let* align = u64_of_postcard ctx st in
          let* span = span_of_postcard ctx st in
          Ok (RustcAttributeKindRustcAlign (align, span))
-     | 13 ->
-         let* _0 = string_of_postcard ctx st in
-         Ok (RustcAttributeKindRustcDiagnosticItem _0)
-     | 14 -> Ok RustcAttributeKindRustcIntrinsic
+     | 13 -> Ok RustcAttributeKindRustcIntrinsic
+     | 14 -> Ok RustcAttributeKindRustcTestEntrypointMarker
      | 15 ->
          let* reason = option_of_postcard string_of_postcard ctx st in
          Ok (RustcAttributeKindShouldPanic reason)

charon/Cargo.toml

@@ -26,7 +26,7 @@ tracing = { version = "0.1", features = ["max_level_trace"] }
 
 [package]
 name = "charon"
-version = "0.1.236"
+version = "0.1.237"
 authors.workspace = true
 edition.workspace = true
 license.workspace = true

charon/src/ast/from_rustc.rs

@@ -104,10 +104,10 @@ pub enum AttributeKind {
     Optimize(OptimizeAttr, Span),
     /// Represents `#[align(N)]`.
     RustcAlign { align: u64, span: Span },
-    /// Represents `#[rustc_diagnostic_item]`
-    RustcDiagnosticItem(Ustr),
     /// Represents `#[rustc_intrinsic]`
     RustcIntrinsic,
+    /// Represents `#[rustc_test_entrypoint_marker]`
+    RustcTestEntrypointMarker,
     /// Represents `#[should_panic]`
     ShouldPanic { reason: Option<Ustr> },
     /// Represents `#[target_feature(enable = "...")]` and

charon/src/bin/charon-driver/translate/translate_from_rustc.rs

@@ -82,10 +82,10 @@ impl<'tcx> TranslateCtx<'tcx> {
                     span: self.translate_span(span),
                 })
             }
-            AttributeKind::RustcDiagnosticItem(_0) => Ok(
-                from_rustc::AttributeKind::RustcDiagnosticItem((_0).to_string().into()),
-            ),
             AttributeKind::RustcIntrinsic => Ok(from_rustc::AttributeKind::RustcIntrinsic),
+            AttributeKind::RustcTestEntrypointMarker => {
+                Ok(from_rustc::AttributeKind::RustcTestEntrypointMarker)
+            }
             AttributeKind::ShouldPanic { reason } => Ok(from_rustc::AttributeKind::ShouldPanic {
                 reason: (reason)
                     .as_ref()

charon/src/bin/generate-asts/generate_rust.rs

@@ -73,8 +73,8 @@ impl RustcDatatypes {
                     "NonExhaustive",
                     "Optimize",
                     "RustcAlign",
-                    "RustcDiagnosticItem",
                     "RustcIntrinsic",
+                    "RustcTestEntrypointMarker",
                     "ShouldPanic",
                     "TargetFeature",
                     "TrackCaller",

charon/src/pretty/fmt_with_ctx.rs

@@ -1143,6 +1143,13 @@ impl ItemMeta {
             writeln!(f, "// Full name: {}", self.name.full_name(ctx))?;
         }
 
+        for attr in &self.attr_info.attributes {
+            // Doc-comments are long and don't affect the semantics; skip them.
+            if attr.is_doc_comment() {
+                continue;
+            }
+            writeln!(f, "{tab}{}", attr.with_ctx(ctx))?;
+        }
         if let Some(id) = &self.lang_item {
             writeln!(f, "{tab}#[lang_item({id:?})]")?;
         }
@@ -1429,6 +1436,133 @@ impl PolyTraitDeclRef {
     }
 }
 
+impl<C: AstFormatter> FmtWithCtx<C> for Attribute {
+    fn fmt_with_ctx(&self, ctx: &C, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        let mut attr = String::new();
+        self.fmt_unindented(ctx, &mut attr)?;
+        let sep = format!("\n{}", ctx.indent());
+        write!(f, "{}", attr.lines().format(sep.as_str()))
+    }
+}
+
+impl Attribute {
+    fn fmt_unindented<C: AstFormatter>(&self, ctx: &C, f: &mut impl fmt::Write) -> fmt::Result {
+        match self {
+            Attribute::Opaque => write!(f, "#[charon::opaque]"),
+            Attribute::Exclude => write!(f, "#[charon::exclude]"),
+            Attribute::Rename(name) => write!(f, "#[charon::rename(\"{name}\")]"),
+            Attribute::VariantsPrefix(prefix) => {
+                write!(f, "#[charon::variants_prefix(\"{prefix}\")]")
+            }
+            Attribute::VariantsSuffix(suffix) => {
+                write!(f, "#[charon::variants_suffix(\"{suffix}\")]")
+            }
+            Attribute::Transparent => write!(f, "#[charon::transparent]"),
+            Attribute::IsPrecondition(id) => {
+                write!(f, "#[charon::precondition] // of {}", id.with_ctx(ctx))
+            }
+            Attribute::IsPostcondition(id) => {
+                write!(f, "#[charon::postcondition] // of {}", id.with_ctx(ctx))
+            }
+            Attribute::HasPrecondition(id) => {
+                let id = ItemId::Fun(*id);
+                write!(f, "// precondition: {}", id.with_ctx(ctx))
+            }
+            Attribute::HasPostcondition(id) => {
+                let id = ItemId::Fun(*id);
+                write!(f, "// postcondition: {}", id.with_ctx(ctx))
+            }
+            Attribute::DocComment(comment) => {
+                write!(
+                    f,
+                    "{}",
+                    comment
+                        .lines()
+                        .map(|line| format!("///{line}"))
+                        .format("\n")
+                )
+            }
+            Attribute::Builtin(kind) => write!(f, "#[{kind}]"),
+            Attribute::Unknown(attr) => write!(f, "#[{attr}]"),
+        }
+    }
+}
+
+/// Print a built-in attribute the way it is written in the source.
+impl Display for from_rustc::AttributeKind {
+    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+        use from_rustc::AttributeKind;
+        match self {
+            AttributeKind::AutomaticallyDerived => write!(f, "automatically_derived"),
+            AttributeKind::Cold => write!(f, "cold"),
+            AttributeKind::Deprecated { deprecation, .. } => {
+                write!(f, "deprecated")?;
+                let since = match &deprecation.since {
+                    from_rustc::DeprecatedSince::RustcVersion(v) => {
+                        Some(format!("{}.{}.{}", v.major, v.minor, v.patch))
+                    }
+                    from_rustc::DeprecatedSince::Future => Some("future".to_owned()),
+                    from_rustc::DeprecatedSince::NonStandard(since) => Some(since.to_string()),
+                    from_rustc::DeprecatedSince::Unspecified | from_rustc::DeprecatedSince::Err => {
+                        None
+                    }
+                };
+                let since = since.map(|since| format!("since = \"{since}\""));
+                let note = deprecation
+                    .note
+                    .as_ref()
+                    .map(|note| format!("note = \"{}\"", note.name));
+                let args = since.into_iter().chain(note).format(", ").to_string();
+                if !args.is_empty() {
+                    write!(f, "({args})")?;
+                }
+                Ok(())
+            }
+            AttributeKind::Fundamental => write!(f, "fundamental"),
+            AttributeKind::Ignore { reason, .. } => {
+                write!(f, "ignore")?;
+                if let Some(reason) = reason {
+                    write!(f, " = \"{reason}\"")?;
+                }
+                Ok(())
+            }
+            AttributeKind::Inline(inline, _) => match inline {
+                from_rustc::InlineAttr::None => write!(f, "inline"),
+                from_rustc::InlineAttr::Hint => write!(f, "inline(hint)"),
+                from_rustc::InlineAttr::Always => write!(f, "inline(always)"),
+                from_rustc::InlineAttr::Never => write!(f, "inline(never)"),
+                from_rustc::InlineAttr::Force { .. } => write!(f, "rustc_force_inline"),
+            },
+            AttributeKind::MayDangle(_) => write!(f, "may_dangle"),
+            AttributeKind::Naked(_) => write!(f, "naked"),
+            AttributeKind::NoLink => write!(f, "no_link"),
+            AttributeKind::NoMangle(_) => write!(f, "no_mangle"),
+            AttributeKind::NonExhaustive(_) => write!(f, "non_exhaustive"),
+            AttributeKind::Optimize(optimize, _) => match optimize {
+                from_rustc::OptimizeAttr::Default => write!(f, "optimize(default)"),
+                from_rustc::OptimizeAttr::DoNotOptimize => write!(f, "optimize(none)"),
+                from_rustc::OptimizeAttr::Speed => write!(f, "optimize(speed)"),
+                from_rustc::OptimizeAttr::Size => write!(f, "optimize(size)"),
+            },
+            AttributeKind::RustcAlign { align, .. } => write!(f, "rustc_align({align})"),
+            AttributeKind::RustcIntrinsic => write!(f, "rustc_intrinsic"),
+            AttributeKind::RustcTestEntrypointMarker => write!(f, "rustc_test_entrypoint_marker"),
+            AttributeKind::ShouldPanic { reason } => {
+                write!(f, "should_panic")?;
+                if let Some(reason) = reason {
+                    write!(f, "(expected = \"{reason}\")")?;
+                }
+                Ok(())
+            }
+            AttributeKind::TargetFeature { features, .. } => {
+                let features = features.iter().map(|(feature, _)| feature).format(",");
+                write!(f, "target_feature(enable = \"{features}\")")
+            }
+            AttributeKind::TrackCaller(_) => write!(f, "track_caller"),
+        }
+    }
+}
+
 impl Display for RawAttribute {
     fn fmt(&self, f: &mut fmt::Formatter<'_>) -> std::result::Result<(), fmt::Error> {
         write!(f, "{}", self.path)?;

charon/tests/cargo.rs

@@ -234,6 +234,13 @@ fn main() -> Result<(), Box<dyn Error>> {
             Success,
         ),
         issue_1298,
+        mktest(
+            "test-attributes",
+            root.join("test-attributes"),
+            &[],
+            &["--tests".to_owned()],
+            Success,
+        ),
     ];
 
     let args = libtest_mimic::Arguments::from_args();