Update synstructure version

Author: Chris-Hawblitzel

source/Cargo.lock

@@ -16,7 +16,7 @@ proc-macro = true
 [dependencies]
 proc-macro2 = "1.0.39"
 quote = "1.0"
-synstructure = { git = "https://github.com/mystor/synstructure.git", rev = "1079497eb2bea252433dac53afe41291d8779641" }
+synstructure = "0.13.2"
 syn = { version = "2.0", features = ["full", "visit", "visit-mut", "extra-traits"] }
 verus_syn = { version = "2.0.96", path="../../dependencies/syn", features = ["full", "visit", "visit-mut", "extra-traits"] }
 verus_prettyplease = { version = "0.2.29", path="../../dependencies/prettyplease" }

source/builtin_macros/Cargo.toml

@@ -13,12 +13,10 @@ pub fn derive_structural_mut(s: &mut synstructure::Structure) -> proc_macro2::To
         })
         .collect::<proc_macro2::TokenStream>();
 
-    // TODO: this feature has disappeared in the latest version of synstructure
-    // (this is why we still use a specific commit of synstructure)
-    // see 'path.segments.iter().find(|s| s.starts_with("_DERIVE_builtin_Structural_FOR_")).is_some()' in rust_to_vir
-    s.underscore_const(false);
-
-    s.gen_impl(quote_spanned_builtin! { verus_builtin, s.ast().span() =>
+    let mut tokens1 = quote::quote_spanned!(s.ast().span() =>
+        #[verus::internal(structural_const_wrapper)]
+    );
+    let tokens2 = s.gen_impl(quote_spanned_builtin! { verus_builtin, s.ast().span() =>
         #[automatically_derived]
         #[allow(non_local_definitions)]
         gen unsafe impl #verus_builtin::Structural for @Self {
@@ -28,7 +26,9 @@ pub fn derive_structural_mut(s: &mut synstructure::Structure) -> proc_macro2::To
                 #assert_receiver_is_structural_body
             }
         }
-    })
+    });
+    tokens1.extend(tokens2.into_iter());
+    tokens1
 }
 
 pub fn derive_structural(mut s: synstructure::Structure) -> proc_macro2::TokenStream {

source/builtin_macros/src/structural.rs

@@ -344,6 +344,8 @@ pub(crate) enum Attr {
     UsesUnerasedProxy,
     EncodedConst,
     EncodedStatic,
+    // The "const _: () = { ... }" generated by synstructure for #[derive(Structural)]
+    StructuralConstWrapper,
 }
 
 fn get_trigger_arg(span: Span, attr_tree: &AttrTree) -> Result<u64, VirErr> {
@@ -778,6 +780,9 @@ pub(crate) fn parse_attrs(
                     AttrTree::Fun(_, arg, None) if arg == "encoded_static" => {
                         v.push(Attr::EncodedStatic)
                     }
+                    AttrTree::Fun(_, arg, None) if arg == "structural_const_wrapper" => {
+                        v.push(Attr::StructuralConstWrapper)
+                    }
                     _ => {
                         return err_span(span, "unrecognized internal attribute");
                     }
@@ -966,6 +971,7 @@ pub(crate) struct ExternalAttrs {
     pub(crate) internal_get_field_many_variants: bool,
     pub(crate) external_auto_derives: AutoDerivesAttr,
     pub(crate) uses_unerased_proxy: bool,
+    pub(crate) structural_const_wrapper: bool,
 }
 
 #[derive(Debug)]
@@ -1026,6 +1032,7 @@ pub(crate) struct VerifierAttrs {
     pub(crate) unerased_proxy: bool,
     pub(crate) encoded_const: bool,
     pub(crate) encoded_static: bool,
+    pub(crate) structural_const_wrapper: bool,
 }
 
 // Check for the `get_field_many_variants` attribute
@@ -1085,6 +1092,7 @@ pub(crate) fn get_external_attrs(
         internal_get_field_many_variants: false,
         external_auto_derives: AutoDerivesAttr::Regular,
         uses_unerased_proxy: false,
+        structural_const_wrapper: false,
     };
 
     for attr in parse_attrs(attrs, diagnostics)? {
@@ -1108,6 +1116,7 @@ pub(crate) fn get_external_attrs(
                 es.external_auto_derives = AutoDerivesAttr::SomeExternal(external_auto_derives)
             }
             Attr::UsesUnerasedProxy => es.uses_unerased_proxy = true,
+            Attr::StructuralConstWrapper => es.structural_const_wrapper = true,
             Attr::UnsupportedRustcAttr(..) => {}
             _ => {
                 es.any_other_verus_specific_attribute = true;
@@ -1193,6 +1202,7 @@ pub(crate) fn get_verifier_attrs_maybe_check(
         unerased_proxy: false,
         encoded_const: false,
         encoded_static: false,
+        structural_const_wrapper: false,
     };
     let mut unsupported_rustc_attr: Option<(String, Span)> = None;
     for attr in parse_attrs(attrs, diagnostics)? {
@@ -1269,6 +1279,7 @@ pub(crate) fn get_verifier_attrs_maybe_check(
             Attr::UnerasedProxy => vs.unerased_proxy = true,
             Attr::EncodedConst => vs.encoded_const = true,
             Attr::EncodedStatic => vs.encoded_static = true,
+            Attr::StructuralConstWrapper => vs.structural_const_wrapper = true,
             Attr::UsesUnerasedProxy => {}
             _ => {}
         }

source/rust_verify/src/attributes.rs

@@ -384,13 +384,7 @@ impl<'a, 'tcx> VisitMod<'a, 'tcx> {
                     });
                 }
                 ItemKind::Const(_ident, _ty, _generics, _body_id) => {
-                    let path = def_id_to_vir_path(self.ctxt.tcx, &self.ctxt.verus_items, def_id);
-                    if path
-                        .segments
-                        .iter()
-                        .find(|s| s.starts_with("_DERIVE_builtin_Structural_FOR_"))
-                        .is_some()
-                    {
+                    if eattrs.structural_const_wrapper {
                         self.state = VerifState::Verify;
                     }
                 }

source/rust_verify/src/external.rs

@@ -67,7 +67,6 @@ fn check_item<'tcx>(
 
     let mut handle_const_or_static = |body_id: &rustc_hir::BodyId| {
         let def_id = body_id.hir_id.owner.to_def_id();
-        let path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, def_id);
         if vattrs.size_of_global {
             return Ok(()); // handled earlier
         }
@@ -150,8 +149,7 @@ fn check_item<'tcx>(
 
             return Ok(());
         }
-        if path.segments.iter().find(|s| s.starts_with("_DERIVE_builtin_Structural_FOR_")).is_some()
-        {
+        if vattrs.structural_const_wrapper {
             ctxt.erasure_info
                 .borrow_mut()
                 .ignored_functions