Mention name of missing decls in the pretty output

AeneasVerif · Aug 21, 2024 · cdd8b4f · cdd8b4f
1 parent f48d1e5
commit cdd8b4f
Show file tree

Hide file tree

Showing 4 changed files with 42 additions and 48 deletions.
diff --git a/charon/src/pretty/fmt_with_ctx.rs b/charon/src/pretty/fmt_with_ctx.rs
@@ -54,6 +54,18 @@ impl<C: AstFormatter> FmtWithCtx<C> for AbortKind {
     }
 }
 
+impl<C: AstFormatter> FmtWithCtx<C> for AnyTransItem<'_> {
+    fn fmt_with_ctx(&self, ctx: &C) -> String {
+        match self {
+            AnyTransItem::Type(d) => d.fmt_with_ctx(ctx),
+            AnyTransItem::Fun(d) => d.fmt_with_ctx(ctx),
+            AnyTransItem::Global(d) => d.fmt_with_ctx(ctx),
+            AnyTransItem::TraitDecl(d) => d.fmt_with_ctx(ctx),
+            AnyTransItem::TraitImpl(d) => d.fmt_with_ctx(ctx),
+        }
+    }
+}
+
 impl<C: AstFormatter> FmtWithCtx<C> for BlockData {
     fn fmt_with_ctx_and_indent(&self, tab: &str, ctx: &C) -> String {
         let mut out: Vec<String> = Vec::new();

diff --git a/charon/src/pretty/formatter.rs b/charon/src/pretty/formatter.rs
@@ -221,6 +221,28 @@ impl<'a> FmtCtx<'a> {
             AnyTransId::TraitImpl(id) => self.format_decl(id),
         }
     }
+
+    pub fn get_item(&self, id: AnyTransId) -> Result<AnyTransItem<'_>, Option<&Name>> {
+        let Some(translated) = &self.translated else {
+            return Err(None);
+        };
+        translated
+            .get_item(id)
+            .ok_or_else(|| translated.item_names.get(&id))
+    }
+
+    fn format_any_decl(&self, id: AnyTransId) -> String {
+        match self.get_item(id) {
+            Ok(d) => d.fmt_with_ctx(self),
+            Err(opt_name) => {
+                let opt_name = opt_name
+                    .map(|n| n.fmt_with_ctx(self))
+                    .map(|n| format!(" ({n})"))
+                    .unwrap_or_default();
+                format!("Missing decl: {id:?}{opt_name}")
+            }
+        }
+    }
 }
 
 impl<'a> Formatter<TypeDeclId> for FmtCtx<'a> {
@@ -585,70 +607,30 @@ impl<'a> Formatter<&gast::TraitImpl> for FmtCtx<'a> {
 
 impl<'a> DeclFormatter<TypeDeclId> for FmtCtx<'a> {
     fn format_decl(&self, id: TypeDeclId) -> String {
-        match &self.translated {
-            None => format!("Unknown decl: {:?}", id),
-            Some(translated) => match translated.type_decls.get(id) {
-                None => {
-                    format!("Unknown decl: {:?}", id)
-                }
-                Some(d) => d.fmt_with_ctx(self),
-            },
-        }
+        self.format_any_decl(id.into())
     }
 }
 
 impl<'a> DeclFormatter<GlobalDeclId> for FmtCtx<'a> {
     fn format_decl(&self, id: GlobalDeclId) -> String {
-        match &self.translated {
-            None => format!("Unknown decl: {:?}", id),
-            Some(translated) => match translated.global_decls.get(id) {
-                None => {
-                    format!("Unknown decl: {:?}", id)
-                }
-                Some(d) => d.fmt_with_ctx(self),
-            },
-        }
+        self.format_any_decl(id.into())
     }
 }
 
 impl<'a> DeclFormatter<FunDeclId> for FmtCtx<'a> {
     fn format_decl(&self, id: FunDeclId) -> String {
-        match &self.translated {
-            None => format!("Unknown decl: {:?}", id),
-            Some(translated) => match translated.fun_decls.get(id) {
-                None => {
-                    format!("Unknown decl: {:?}", id)
-                }
-                Some(d) => d.fmt_with_ctx(self),
-            },
-        }
+        self.format_any_decl(id.into())
     }
 }
 
 impl<'a> DeclFormatter<TraitDeclId> for FmtCtx<'a> {
     fn format_decl(&self, id: TraitDeclId) -> String {
-        match &self.translated {
-            None => format!("Unknown decl: {:?}", id),
-            Some(translated) => match translated.trait_decls.get(id) {
-                None => {
-                    format!("Unknown decl: {:?}", id)
-                }
-                Some(d) => d.fmt_with_ctx(self),
-            },
-        }
+        self.format_any_decl(id.into())
     }
 }
 
 impl<'a> DeclFormatter<TraitImplId> for FmtCtx<'a> {
     fn format_decl(&self, id: TraitImplId) -> String {
-        match &self.translated {
-            None => format!("Unknown impl: {:?}", id),
-            Some(translated) => match translated.trait_impls.get(id) {
-                None => {
-                    format!("Unknown impl: {:?}", id)
-                }
-                Some(d) => d.fmt_with_ctx(self),
-            },
-        }
+        self.format_any_decl(id.into())
     }
 }
diff --git a/charon/tests/ui/opacity.out b/charon/tests/ui/opacity.out
@@ -68,7 +68,7 @@ impl core::convert::num::{impl core::convert::From<u32> for u64}#72 : core::conv
 
 fn core::convert::Into::into<Self, T>(@1: Self) -> T
 
-Unknown decl: 4
+Missing decl: Fun(4) (core::slice::raw::from_ref)
 
 fn test_crate::foo()
 {

diff --git a/charon/tests/ui/trait-instance-id.out b/charon/tests/ui/trait-instance-id.out
@@ -296,7 +296,7 @@ where
     [@TraitClause0]: core::ops::function::FnMut<F, (&'_ (T))>,
     (parents(UNKNOWN(Could not find a clause for parameter: core::ops::function::FnMut<F, (core::slice::iter::{impl core::iter::traits::iterator::Iterator for @Adt2<'a, T>}#182<'_, T>::Item)> (available clauses: [Self]: core::iter::traits::iterator::Iterator<@Adt2<'a, T>>; [@TraitClause0]: core::ops::function::FnMut<F, (&'_ (T))>) (context: core::slice::iter::{impl#182}::any)))::[@TraitClause0])::Output = bool,
 
-Unknown decl: 39
+Missing decl: Fun(39) (core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::find)
 
 fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::find_map<'a, '_1, T, B, F>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: F) -> core::option::Option<B>
 where
@@ -335,7 +335,7 @@ where
 
 unsafe fn core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::__iterator_get_unchecked<'a, '_1, T>(@1: &'_1 mut (core::slice::iter::Iter<'a, T>), @2: usize) -> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182<'_, T>::Item
 
-Unknown decl: 44
+Missing decl: Fun(44) (core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182::is_sorted_by)
 
 impl<'a, T> core::slice::iter::{impl core::iter::traits::iterator::Iterator for core::slice::iter::Iter<'a, T>}#182<'a, T> : core::iter::traits::iterator::Iterator<core::slice::iter::Iter<'a, T>>
 {