Ugly commit 29.13

prusti-contracts/prusti-contracts-proc-macros/src/lib.rs

@@ -53,6 +53,12 @@ pub fn panic_ensures(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
     tokens
 }
 
+#[cfg(not(feature = "prusti"))]
+#[proc_macro_attribute]
+pub fn structural_panic_ensures(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
+    tokens
+}
+
 #[cfg(not(feature = "prusti"))]
 #[proc_macro_attribute]
 pub fn structural_ensures(_attr: TokenStream, tokens: TokenStream) -> TokenStream {
@@ -479,6 +485,17 @@ pub fn structural_ensures(attr: TokenStream, tokens: TokenStream) -> TokenStream
     .into()
 }
 
+#[cfg(feature = "prusti")]
+#[proc_macro_attribute]
+pub fn structural_panic_ensures(attr: TokenStream, tokens: TokenStream) -> TokenStream {
+    rewrite_prusti_attributes(
+        SpecAttributeKind::StructuralPanicEnsures,
+        attr.into(),
+        tokens.into(),
+    )
+    .into()
+}
+
 /// FIXME: Remove.
 #[cfg(feature = "prusti")]
 #[proc_macro_attribute]

prusti-contracts/prusti-contracts/src/lib.rs

@@ -19,6 +19,9 @@ pub use prusti_contracts_proc_macros::panic_ensures;
 /// A macro for writing a structural postcondition on an unsafe function.
 pub use prusti_contracts_proc_macros::structural_ensures;
 
+/// A macro for writing a structural panic postcondition on an unsafe function.
+pub use prusti_contracts_proc_macros::structural_panic_ensures;
+
 /// A macro to indicate that the type invariant is not ensured by the function.
 /// FIXME: Remove
 pub use prusti_contracts_proc_macros::not_ensure;

prusti-contracts/prusti-specs/src/lib.rs

@@ -76,6 +76,7 @@ fn extract_prusti_attributes(
                     | SpecAttributeKind::Ensures
                     | SpecAttributeKind::PanicEnsures
                     | SpecAttributeKind::StructuralEnsures
+                    | SpecAttributeKind::StructuralPanicEnsures
                     | SpecAttributeKind::NotRequire
                     | SpecAttributeKind::NotEnsure
                     | SpecAttributeKind::AfterExpiry
@@ -180,6 +181,9 @@ fn generate_spec_and_assertions(
             SpecAttributeKind::StructuralEnsures => {
                 generate_for_structural_ensures(attr_tokens, item)
             }
+            SpecAttributeKind::StructuralPanicEnsures => {
+                generate_for_structural_panic_ensures(attr_tokens, item)
+            }
             SpecAttributeKind::NotRequire => generate_for_not_require(attr_tokens, item),
             SpecAttributeKind::NotEnsure => generate_for_not_ensure(attr_tokens, item),
             SpecAttributeKind::AfterExpiry => generate_for_after_expiry(attr_tokens, item),
@@ -314,6 +318,25 @@ fn generate_for_structural_ensures(
     ))
 }
 
+/// Generate spec items and attributes to typecheck the and later retrieve
+/// "structural_ensures" annotations.
+fn generate_for_structural_panic_ensures(
+    attr: TokenStream,
+    item: &untyped::AnyFnItem,
+) -> GeneratedResult {
+    let mut rewriter = rewriter::AstRewriter::new();
+    let spec_id = rewriter.generate_spec_id();
+    let spec_id_str = spec_id.to_string();
+    let spec_item =
+        rewriter.process_assertion(rewriter::SpecItemType::Postcondition, spec_id, attr, item)?;
+    Ok((
+        vec![spec_item],
+        vec![parse_quote_spanned! {item.span()=>
+            #[prusti::post_structural_panic_spec_id_ref = #spec_id_str]
+        }],
+    ))
+}
+
 /// Generate spec items and attributes to typecheck and later retrieve
 /// "not_ensure" annotations.
 fn generate_for_not_ensure(attr: TokenStream, item: &untyped::AnyFnItem) -> GeneratedResult {
@@ -1100,6 +1123,9 @@ fn extract_prusti_attributes_for_types(
                     SpecAttributeKind::StructuralEnsures => {
                         unreachable!("structural ensures on type")
                     }
+                    SpecAttributeKind::StructuralPanicEnsures => {
+                        unreachable!("structural panic_ensures on type")
+                    }
                     SpecAttributeKind::AfterExpiry => unreachable!("after_expiry on type"),
                     SpecAttributeKind::AssertOnExpiry => unreachable!("assert_on_expiry on type"),
                     SpecAttributeKind::RefineSpec => unreachable!("refine_spec on type"),
@@ -1159,6 +1185,7 @@ fn generate_spec_and_assertions_for_types(
             SpecAttributeKind::Ensures => unreachable!(),
             SpecAttributeKind::PanicEnsures => unreachable!(),
             SpecAttributeKind::StructuralEnsures => unreachable!(),
+            SpecAttributeKind::StructuralPanicEnsures => unreachable!(),
             SpecAttributeKind::AfterExpiry => unreachable!(),
             SpecAttributeKind::AssertOnExpiry => unreachable!(),
             SpecAttributeKind::Pure => unreachable!(),

prusti-contracts/prusti-specs/src/spec_attribute_kind.rs

@@ -26,6 +26,7 @@ pub enum SpecAttributeKind {
     StructuralRequires = 18,
     StructuralEnsures = 19,
     PanicEnsures = 20,
+    StructuralPanicEnsures = 21,
 }
 
 impl TryFrom<String> for SpecAttributeKind {
@@ -38,6 +39,7 @@ impl TryFrom<String> for SpecAttributeKind {
             "ensures" => Ok(SpecAttributeKind::Ensures),
             "panic_ensures" => Ok(SpecAttributeKind::PanicEnsures),
             "structural_ensures" => Ok(SpecAttributeKind::StructuralEnsures),
+            "structural_panic_ensures" => Ok(SpecAttributeKind::StructuralPanicEnsures),
             "after_expiry" => Ok(SpecAttributeKind::AfterExpiry),
             "assert_on_expiry" => Ok(SpecAttributeKind::AssertOnExpiry),
             "pure" => Ok(SpecAttributeKind::Pure),

prusti-contracts/prusti-specs/src/specifications/common.rs

@@ -59,6 +59,7 @@ pub enum SpecIdRef {
     Postcondition(SpecificationId),
     PanicPostcondition(SpecificationId),
     StructuralPostcondition(SpecificationId),
+    StructuralPanicPostcondition(SpecificationId),
     BrokenPrecondition(SpecificationId),
     BrokenPostcondition(SpecificationId),
     Purity(SpecificationId),

prusti-interface/src/specs/mod.rs

@@ -189,6 +189,12 @@ impl<'a, 'tcx> SpecCollector<'a, 'tcx> {
                             self.env,
                         );
                     }
+                    SpecIdRef::StructuralPanicPostcondition(spec_id) => {
+                        spec.add_structural_panic_postcondition(
+                            *self.spec_functions.get(spec_id).unwrap(),
+                            self.env,
+                        );
+                    }
                     SpecIdRef::BrokenPrecondition(spec_id) => {
                         spec.add_broken_precondition(
                             self.spec_functions.get(spec_id).unwrap().to_def_id(),
@@ -527,6 +533,13 @@ fn get_procedure_spec_ids(def_id: DefId, attrs: &[ast::Attribute]) -> Option<Pro
                 SpecIdRef::StructuralPostcondition(parse_spec_id(raw_spec_id, def_id))
             }),
     );
+    spec_id_refs.extend(
+        read_prusti_attrs("post_structural_panic_spec_id_ref", attrs)
+            .into_iter()
+            .map(|raw_spec_id| {
+                SpecIdRef::StructuralPanicPostcondition(parse_spec_id(raw_spec_id, def_id))
+            }),
+    );
     spec_id_refs.extend(
         read_prusti_attrs("pre_broken_spec_id_ref", attrs)
             .into_iter()

prusti-interface/src/specs/typed.rs

@@ -114,6 +114,12 @@ impl DefSpecificationMap {
                 if let Some(posts) = spec.structural_posts.extract_with_selective_replacement() {
                     specs.extend(posts);
                 }
+                if let Some(posts) = spec
+                    .structural_panic_posts
+                    .extract_with_selective_replacement()
+                {
+                    specs.extend(posts);
+                }
                 if let Some(broken_pres) = spec.broken_pres.extract_with_selective_replacement() {
                     specs.extend(broken_pres);
                 }
@@ -266,6 +272,7 @@ pub struct ProcedureSpecification {
     pub posts: SpecificationItem<Vec<DefId>>,
     pub panic_posts: SpecificationItem<Vec<DefId>>,
     pub structural_posts: SpecificationItem<Vec<DefId>>,
+    pub structural_panic_posts: SpecificationItem<Vec<DefId>>,
     pub pledges: SpecificationItem<Vec<Pledge>>,
     pub trusted: SpecificationItem<bool>,
     pub non_verified_pure: SpecificationItem<bool>,
@@ -289,6 +296,7 @@ impl ProcedureSpecification {
             posts: SpecificationItem::Empty,
             panic_posts: SpecificationItem::Empty,
             structural_posts: SpecificationItem::Empty,
+            structural_panic_posts: SpecificationItem::Empty,
             broken_pres: SpecificationItem::Empty,
             broken_posts: SpecificationItem::Empty,
             pledges: SpecificationItem::Empty,
@@ -616,6 +624,32 @@ impl SpecGraph<ProcedureSpecification> {
         }
     }
 
+    /// Attaches the panic structural postcondition `structural_panic_post` to this
+    /// [SpecGraph].
+    ///
+    /// If this structural postcondition has a constraint it will be attached to
+    /// the corresponding constrained spec **and** the base spec, otherwise just
+    /// to the base spec.
+    pub fn add_structural_panic_postcondition<'tcx>(
+        &mut self,
+        post: LocalDefId,
+        env: &Environment<'tcx>,
+    ) {
+        match self.get_constraint(post, env) {
+            None => {
+                self.base_spec.structural_panic_posts.push(post.to_def_id());
+                self.specs_with_constraints
+                    .values_mut()
+                    .for_each(|s| s.structural_panic_posts.push(post.to_def_id()));
+            }
+            Some(obligation) => {
+                self.get_constrained_spec_mut(obligation)
+                    .structural_panic_posts
+                    .push(post.to_def_id());
+            }
+        }
+    }
+
     /// Sets the broken precondition for the base spec and all constrained specs.
     pub fn add_broken_precondition(&mut self, broken_precondition: DefId) {
         self.base_spec.broken_pres.push(broken_precondition);
@@ -986,6 +1020,9 @@ impl Refinable for ProcedureSpecification {
             structural_posts: self
                 .structural_posts
                 .refine(replace_empty(&EMPTYL, &other.structural_posts)),
+            structural_panic_posts: self
+                .structural_panic_posts
+                .refine(replace_empty(&EMPTYL, &other.structural_panic_posts)),
             broken_pres: self
                 .broken_pres
                 .refine(replace_empty(&EMPTYL, &other.broken_pres)),

prusti-viper/src/encoder/mir/contracts/contracts.rs

@@ -230,6 +230,14 @@ impl<L: fmt::Debug, P: fmt::Debug> ProcedureContractGeneric<L, P> {
         // }
     }
 
+    pub fn structural_panic_postcondition<'a, 'tcx>(
+        &'a self,
+        env: &'a Environment<'tcx>,
+        substs: SubstsRef<'tcx>,
+    ) -> Vec<(DefId, SubstsRef<'tcx>)> {
+        self.specification(&self.specification.structural_panic_posts, env, substs)
+    }
+
     pub fn functional_termination_measure<'a, 'tcx>(
         &'a self,
         env: &'a Environment<'tcx>,