Fix mono errors

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

@@ -245,12 +245,16 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         let Some(kind) = self.base_kind_for_item(def_id) else {
             return;
         };
-        let item_src = if self.options.monomorphize_with_hax
-            && let Ok(def) = self.poly_hax_def(def_id)
-            && !def.has_any_generics()
-        {
-            // Monomorphize this item and the items it depends on.
-            TransItemSource::monomorphic(def.this(), kind)
+        let item_src = if self.options.monomorphize_with_hax {
+            if let Ok(def) = self.poly_hax_def(def_id)
+                && !def.has_any_generics()
+            {
+                // Monomorphize this item and the items it depends on.
+                TransItemSource::monomorphic(def.this(), kind)
+            } else {
+                // Skip polymorphic items and items that cause errors.
+                return;
+            }
         } else {
             TransItemSource::polymorphic(def_id, kind)
         };

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

@@ -133,7 +133,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx> {
         let def_id = item.def_id();
         let span = self.def_span(def_id);
         if let RustcItem::Mono(item_ref) = item
-            && item_ref.has_param
+            && item_ref.has_non_lt_param
         {
             raise_error!(self, span, "Item is not monomorphic: {item:?}")
         }

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

@@ -680,6 +680,8 @@ impl ItemTransCtx<'_, '_> {
                     let ty = self.translate_ty(item_span, ty)?;
                     consts.push((item_name.clone(), ty));
                 }
+                // Monomorphic traits have no associated types.
+                hax::FullDefKind::AssocTy { .. } if self.monomorphize() => continue,
                 hax::FullDefKind::AssocTy { param_env, .. }
                     if !param_env.generics.params.is_empty() =>
                 {
@@ -890,6 +892,8 @@ impl ItemTransCtx<'_, '_> {
                     };
                     consts.push((name, gref));
                 }
+                // Monomorphic traits have no associated types.
+                hax::FullDefKind::AssocTy { .. } if self.monomorphize() => continue,
                 hax::FullDefKind::AssocTy { param_env, .. }
                     if !param_env.generics.params.is_empty() =>
                 {
@@ -1057,17 +1061,20 @@ impl ItemTransCtx<'_, '_> {
 
         let mut types = vec![];
         let mut type_clauses = vec![];
-        let type_items = trait_items.iter().filter(|assoc| match assoc.kind {
-            hax::AssocKind::Type { .. } => true,
-            _ => false,
-        });
-        for ((ty, impl_exprs), assoc) in vimpl.types.iter().zip(type_items) {
-            let name = self.t_ctx.translate_trait_item_name(&assoc.def_id)?;
-            let ty = self.translate_ty(span, ty)?;
-            types.push((name.clone(), ty.clone()));
-            if !self.monomorphize() {
-                let trait_refs = self.translate_trait_impl_exprs(span, impl_exprs)?;
-                type_clauses.push((name.clone(), trait_refs));
+        // Monomorphic traits have no associated types.
+        if !self.monomorphize() {
+            let type_items = trait_items.iter().filter(|assoc| match assoc.kind {
+                hax::AssocKind::Type { .. } => true,
+                _ => false,
+            });
+            for ((ty, impl_exprs), assoc) in vimpl.types.iter().zip(type_items) {
+                let name = self.t_ctx.translate_trait_item_name(&assoc.def_id)?;
+                let ty = self.translate_ty(span, ty)?;
+                types.push((name.clone(), ty.clone()));
+                if !self.monomorphize() {
+                    let trait_refs = self.translate_trait_impl_exprs(span, impl_exprs)?;
+                    type_clauses.push((name.clone(), trait_refs));
+                }
             }
         }
 

charon/src/errors.rs

@@ -10,6 +10,8 @@ use petgraph::prelude::DiGraphMap;
 use std::cmp::{Ord, PartialOrd};
 use std::collections::{HashMap, HashSet};
 
+const BACKTRACE_ON_ERR: bool = false;
+
 #[macro_export]
 macro_rules! register_error {
     ($ctx:expr, crate($krate:expr), $span: expr, $($fmt:tt)*) => {{
@@ -231,6 +233,10 @@ impl ErrorCtx {
     ) -> Error {
         let error = Error { span, msg };
         anstream::eprintln!("{}\n", error.render(krate, level));
+        if BACKTRACE_ON_ERR {
+            let backtrace = std::backtrace::Backtrace::force_capture();
+            eprintln!("{backtrace}\n");
+        }
         error
     }
 

charon/tests/ui/dyn-with-diamond-supertraits.out

@@ -0,0 +1,11 @@
+
+thread 'rustc' panicked at src/bin/charon-driver/translate/translate_trait_objects.rs:426:14:
+trait should be dyn-compatible
+note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
+error: Thread panicked when extracting item `test_crate::{impl#4}`.
+  --> tests/ui/dyn-with-diamond-supertraits.rs:47:1
+   |
+47 | impl Join<i32> for i32 {
+   | ^^^^^^^^^^^^^^^^^^^^^^
+
+ERROR Charon failed to translate this code (1 errors)

charon/tests/ui/dyn-with-diamond-supertraits.rs

@@ -0,0 +1,56 @@
+//@ known-failure
+/// This tests `dyn` with a diamond hierarchy between supertraits. Fails for now because we don't
+/// support dyn with associated types.
+
+trait Super<T> {
+    fn super_method(&self, arg: T) -> i32;
+}
+trait Internal {
+    type Internal;
+    fn internal_method(&self) -> Self::Internal;
+}
+trait Left: Internal {
+    type Left;
+    fn left_method(&self) -> Self::Left;
+}
+trait Right<T>: Internal + Super<T> {
+    type Right;
+    fn right_method(&self) -> Self::Right;
+}
+trait Join<T>: Left + Right<T> {
+    fn join_method(&self) -> (Self::Left, Self::Right);
+}
+
+impl Super<i32> for i32 {
+    fn super_method(&self, arg: i32) -> i32 {
+        self + arg
+    }
+}
+impl Internal for i32 {
+    type Internal = i32;
+    fn internal_method(&self) -> Self::Internal {
+        *self + 1
+    }
+}
+impl Left for i32 {
+    type Left = i32;
+    fn left_method(&self) -> Self::Left {
+        *self + 2
+    }
+}
+impl Right<i32> for i32 {
+    type Right = i32;
+    fn right_method(&self) -> Self::Right {
+        *self + 3 + self.internal_method() + self.super_method(10)
+    }
+}
+impl Join<i32> for i32 {
+    fn join_method(&self) -> (Self::Left, Self::Right) {
+        (self.left_method(), self.right_method())
+    }
+}
+
+fn main() {
+    let v: &dyn Join<i32, Internal = i32, Left = i32, Right = i32> = &97;
+    let (_, _) = v.join_method();
+}

charon/tests/ui/monomorphization/bound_lifetime.out

@@ -0,0 +1,63 @@
+# Final LLBC before serialization:
+
+// Full name: core::marker::MetaSized::<&'_ (u32)>
+#[lang_item("meta_sized")]
+pub trait MetaSized::<&'_ (u32)>
+
+// Full name: core::marker::Sized::<&'_ (u32)>
+#[lang_item("sized")]
+pub trait Sized::<&'_ (u32)>
+{
+    parent_clause0 : [@TraitClause0]: MetaSized::<&'_ (u32)>
+    non-dyn-compatible
+}
+
+// Full name: core::option::Option::<&'_ (u32)>
+#[lang_item("Option")]
+pub enum Option::<&'_ (u32)> {
+  None,
+  Some(&'_ (u32)),
+}
+
+// Full name: test_crate::foo
+fn foo<'_0>(@1: &'_0 (u32)) -> Option::<&'_ (u32)>
+{
+    let @0: Option::<&'_ (u32)>; // return
+    let x@1: &'_ (u32); // arg #1
+    let @2: &'_ (u32); // anonymous local
+
+    storage_live(@2)
+    @2 := &*(x@1)
+    @0 := Option::<&'_ (u32)>::Some { 0: move (@2) }
+    storage_dead(@2)
+    return
+}
+
+// Full name: test_crate::main
+fn main()
+{
+    let @0: (); // return
+    let @1: Option::<&'_ (u32)>; // anonymous local
+    let @2: &'_ (u32); // anonymous local
+    let @3: &'_ (u32); // anonymous local
+    let @4: u32; // anonymous local
+
+    storage_live(@1)
+    storage_live(@2)
+    storage_live(@3)
+    storage_live(@4)
+    @4 := const (42 : u32)
+    @3 := &@4
+    @2 := &*(@3)
+    @1 := foo<'_>(move (@2))
+    storage_dead(@2)
+    storage_dead(@4)
+    storage_dead(@3)
+    storage_dead(@1)
+    @0 := ()
+    @0 := ()
+    return
+}
+
+
+

charon/tests/ui/monomorphization/bound_lifetime.rs

@@ -0,0 +1,9 @@
+//@ charon-args=--monomorphize
+/// Reproducer for a bug whereby a bound lifetime was not allowed in monomorphic context.
+fn foo(x: &u32) -> Option<&u32> {
+    Some(x)
+}
+
+fn main() {
+    let _ = foo(&42);
+}

charon/tests/ui/monomorphization/closure-fn.out

@@ -57,7 +57,6 @@ pub trait FnOnce::<closure<'_, '_>, (u8, u8)>
     parent_clause0 : [@TraitClause0]: MetaSized::<closure<'_, '_>>
     parent_clause1 : [@TraitClause1]: Sized::<(u8, u8)>
     parent_clause2 : [@TraitClause2]: Tuple::<(u8, u8)>
-    type Output
     fn call_once = core::ops::function::FnOnce::call_once::<closure<'_, '_>, (u8, u8)>
     non-dyn-compatible
 }
@@ -311,7 +310,6 @@ impl<'_0, '_1> FnOnce::<closure<'_, '_>, (u8, u8)> {
     parent_clause0 = MetaSized::<closure<'_, '_>>
     parent_clause1 = Sized::<(u8, u8)>
     parent_clause2 = Tuple::<(u8, u8)>
-    type Output = u8
     fn call_once = {impl FnOnce::<closure<'_, '_>, (u8, u8)>}::call_once<'_0, '_1>
     non-dyn-compatible
 }

charon/tests/ui/monomorphization/closure-fnonce.out

@@ -73,7 +73,6 @@ pub trait FnOnce::<closure, (u8)>
     parent_clause0 : [@TraitClause0]: MetaSized::<closure>
     parent_clause1 : [@TraitClause1]: Sized::<(u8)>
     parent_clause2 : [@TraitClause2]: Tuple::<(u8)>
-    type Output
     fn call_once = core::ops::function::FnOnce::call_once::<closure, (u8)>
     non-dyn-compatible
 }
@@ -157,7 +156,6 @@ impl FnOnce::<closure, (u8)> {
     parent_clause0 = MetaSized::<closure>
     parent_clause1 = Sized::<(u8)>
     parent_clause2 = Tuple::<(u8)>
-    type Output = u8
     fn call_once = {impl FnOnce::<closure, (u8)>}::call_once
     non-dyn-compatible
 }

charon/tests/ui/monomorphization/closures.out

@@ -126,7 +126,6 @@ pub trait FnOnce::<test_crate::main::closure<'_>, (u8)>
     parent_clause0 : [@TraitClause0]: MetaSized::<test_crate::main::closure<'_>>
     parent_clause1 : [@TraitClause1]: Sized::<(u8)>
     parent_clause2 : [@TraitClause2]: Tuple::<(u8)>
-    type Output
     fn call_once = core::ops::function::FnOnce::call_once::<test_crate::main::closure<'_>, (u8)>
     non-dyn-compatible
 }
@@ -166,7 +165,6 @@ pub trait FnOnce::<test_crate::main::closure#1<'_>, (u8)>
     parent_clause0 : [@TraitClause0]: MetaSized::<test_crate::main::closure#1<'_>>
     parent_clause1 : [@TraitClause1]: Sized::<(u8)>
     parent_clause2 : [@TraitClause2]: Tuple::<(u8)>
-    type Output
     fn call_once = core::ops::function::FnOnce::call_once::<test_crate::main::closure#1<'_>, (u8)>
     non-dyn-compatible
 }
@@ -198,7 +196,6 @@ pub trait FnOnce::<test_crate::main::closure#2, (u8)>
     parent_clause0 : [@TraitClause0]: MetaSized::<test_crate::main::closure#2>
     parent_clause1 : [@TraitClause1]: Sized::<(u8)>
     parent_clause2 : [@TraitClause2]: Tuple::<(u8)>
-    type Output
     fn call_once = core::ops::function::FnOnce::call_once::<test_crate::main::closure#2, (u8)>
     non-dyn-compatible
 }
@@ -439,7 +436,6 @@ impl<'_0> FnOnce::<test_crate::main::closure<'_>, (u8)> {
     parent_clause0 = MetaSized::<test_crate::main::closure<'_>>
     parent_clause1 = Sized::<(u8)>
     parent_clause2 = Tuple::<(u8)>
-    type Output = u8
     fn call_once = {impl FnOnce::<test_crate::main::closure<'_>, (u8)>}::call_once<'_0>
     non-dyn-compatible
 }
@@ -484,7 +480,6 @@ impl<'_0> FnOnce::<test_crate::main::closure#1<'_>, (u8)> {
     parent_clause0 = MetaSized::<test_crate::main::closure#1<'_>>
     parent_clause1 = Sized::<(u8)>
     parent_clause2 = Tuple::<(u8)>
-    type Output = u8
     fn call_once = {impl FnOnce::<test_crate::main::closure#1<'_>, (u8)>}::call_once<'_0>
     non-dyn-compatible
 }
@@ -504,7 +499,6 @@ impl FnOnce::<test_crate::main::closure#2, (u8)> {
     parent_clause0 = MetaSized::<test_crate::main::closure#2>
     parent_clause1 = Sized::<(u8)>
     parent_clause2 = Tuple::<(u8)>
-    type Output = u8
     fn call_once = {impl FnOnce::<test_crate::main::closure#2, (u8)>}::call_once
     non-dyn-compatible
 }

charon/tests/ui/monomorphization/closures.rs

@@ -1,5 +1,6 @@
 //@ charon-args=--monomorphize
 //@ charon-args=--start-from=crate::main
+//@ charon-args=--remove-associated-types *
 // Ensures closures are monomorphized and replaced with static function calls
 
 struct Thing;