add: reference trait-side definitions for require/ensure annotations of

functions in impl blocks

Author: coeff-aij

src/analyze/local_def.rs

@@ -53,13 +53,13 @@ pub struct Analyzer<'tcx, 'ctx> {
 }
 
 impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
-    fn extract_require_annot<T>(&self, resolver: T) -> Option<AnnotFormula<T::Output>>
+    fn extract_require_annot<T>(&self, def_id: DefId, resolver: T) -> Option<AnnotFormula<T::Output>>
     where
         T: annot::Resolver,
     {
         let mut require_annot = None;
         for attrs in self.tcx.get_attrs_by_path(
-            self.local_def_id.to_def_id(),
+            def_id,
             &analyze::annot::requires_path(),
         ) {
             if require_annot.is_some() {
@@ -72,13 +72,13 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
         require_annot
     }
 
-    fn extract_ensure_annot<T>(&self, resolver: T) -> Option<AnnotFormula<T::Output>>
+    fn extract_ensure_annot<T>(&self, def_id: DefId, resolver: T) -> Option<AnnotFormula<T::Output>>
     where
         T: annot::Resolver,
     {
         let mut ensure_annot = None;
         for attrs in self.tcx.get_attrs_by_path(
-            self.local_def_id.to_def_id(),
+            def_id,
             &analyze::annot::ensures_path(),
         ) {
             if ensure_annot.is_some() {
@@ -252,6 +252,14 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             || (all_params_annotated && has_ret)
     }
 
+    pub fn get_trait_item(&mut self) -> Option<LocalDefId>
+    {
+        let impl_item_assoc = self.tcx.opt_associated_item(self.local_def_id.to_def_id())?;
+        let trait_item_id = impl_item_assoc.trait_item_def_id.and_then(|id| id.as_local())?;
+
+        Some(trait_item_id)
+    }
+
     pub fn expected_ty(&mut self) -> rty::RefinedType {
         let sig = self
             .ctx
@@ -268,14 +276,26 @@ impl<'tcx, 'ctx> Analyzer<'tcx, 'ctx> {
             param_resolver.push_param(input_ident.name, input_ty.to_sort());
         }
 
-        let mut require_annot = self.extract_require_annot(&param_resolver);
-        let mut ensure_annot = {
-            let output_ty = self.type_builder.build(sig.output());
-            let resolver = annot::StackedResolver::default()
-                .resolver(analyze::annot::ResultResolver::new(output_ty.to_sort()))
-                .resolver((&param_resolver).map(rty::RefinedTypeVar::Free));
-            self.extract_ensure_annot(resolver)
-        };
+        let mut require_annot = self.extract_require_annot(self.local_def_id.to_def_id(), &param_resolver);
+        
+        let output_ty = self.type_builder.build(sig.output());
+        let result_param_resolver = annot::StackedResolver::default()
+            .resolver(analyze::annot::ResultResolver::new(output_ty.to_sort()))
+            .resolver((&param_resolver).map(rty::RefinedTypeVar::Free));
+        let mut ensure_annot = self.extract_ensure_annot(self.local_def_id.to_def_id(), &result_param_resolver);
+
+        if let Some(trait_item_id) = self.get_trait_item(){
+            tracing::info!("trait item fonud: {}", self.tcx.item_name(trait_item_id.into()).to_string());
+            let trait_require_annot = self.extract_require_annot(trait_item_id.into(), &param_resolver);
+            let trait_ensure_annot = self.extract_ensure_annot(trait_item_id.into(), &result_param_resolver);
+        
+            assert!(require_annot.is_none() || trait_require_annot.is_none());
+            require_annot = require_annot.or(trait_require_annot);
+
+            assert!(ensure_annot.is_none() || trait_ensure_annot.is_none());
+            ensure_annot = ensure_annot.or(trait_ensure_annot);
+        }
+
         let param_annots = self.extract_param_annots(&param_resolver);
         let ret_annot = self.extract_ret_annot(&param_resolver);