Solve trait refs in two phases

charon/src/ast/types.rs

@@ -2,6 +2,7 @@ use crate::ast::*;
 use crate::ids::Vector;
 use derivative::Derivative;
 use derive_visitor::{Drive, DriveMut, Event, Visitor, VisitorMut};
+use hax_frontend_exporter as hax;
 use macros::{EnumAsGetters, EnumIsA, EnumToGetters, VariantIndexArity, VariantName};
 use serde::{Deserialize, Serialize};
 
@@ -220,6 +221,12 @@ pub enum TraitRefKind {
     /// The automatically-generated implementation for `dyn Trait`.
     Dyn(TraitDeclRef),
 
+    /// The trait ref could not be resolved, likely because the corresponding clause had not been
+    /// registered yet. We will try resolving it again once all clauses are registered.
+    #[charon::opaque]
+    #[drive(skip)]
+    Unsolved(hax::TraitRef),
+
     /// For error reporting.
     #[charon::rename("UnknownTrait")]
     Unknown(String),

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

@@ -6,7 +6,10 @@ use charon_lib::formatter::{FmtCtx, IntoFormatter};
 use charon_lib::ids::{MapGenerator, Vector};
 use charon_lib::name_matcher::NamePattern;
 use charon_lib::options::CliOpts;
+use charon_lib::pretty::FmtWithCtx;
 use charon_lib::ullbc_ast as ast;
+use derive_visitor::visitor_enter_fn_mut;
+use derive_visitor::DriveMut;
 use hax_frontend_exporter as hax;
 use hax_frontend_exporter::SInto;
 use itertools::Itertools;
@@ -1101,7 +1104,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             .iter()
             .enumerate()
             .all(|(i, c)| c.clause_id.index() == i));
-        let generic_params = GenericParams {
+        let mut generic_params = GenericParams {
             regions: self.region_vars[0].clone(),
             types: self.type_vars.clone(),
             const_generics: self.const_generic_vars.clone(),
@@ -1110,6 +1113,52 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             types_outlive: self.types_outlive.clone(),
             trait_type_constraints: self.trait_type_constraints.clone(),
         };
+        // Solve trait refs now that all clauses have been registered.
+        generic_params.drive_mut(&mut visitor_enter_fn_mut(|tref_kind: &mut TraitRefKind| {
+            if let TraitRefKind::Unsolved(hax_trait_ref) = tref_kind {
+                let new_kind = self.find_trait_clause_for_param(hax_trait_ref);
+                *tref_kind = if let TraitRefKind::Unsolved(_) = new_kind {
+                    // Could not find a clause.
+                    // Check if we are in the registration process, otherwise report an error.
+                    let fmt_ctx = self.into_fmt();
+                    let trait_ref = format!("{:?}", hax_trait_ref);
+                    let clauses: Vec<String> = self
+                        .trait_clauses
+                        .values()
+                        .flat_map(|x| x)
+                        .map(|x| x.fmt_with_ctx(&fmt_ctx))
+                        .collect();
+
+                    if !self.t_ctx.continue_on_failure() {
+                        let clauses = clauses.join("\n");
+                        unreachable!(
+                            "Could not find a clause for parameter:\n- target param: {}\n\
+                            - available clauses:\n{}\n- context: {:?}",
+                            trait_ref, clauses, self.def_id
+                        );
+                    } else {
+                        // Return the UNKNOWN clause
+                        tracing::warn!(
+                            "Could not find a clause for parameter:\n- target param: {}\n\
+                            - available clauses:\n{}\n- context: {:?}",
+                            trait_ref,
+                            clauses.join("\n"),
+                            self.def_id
+                        );
+                        TraitRefKind::Unknown(format!(
+                            "Could not find a clause for parameter: {} \
+                            (available clauses: {}) (context: {:?})",
+                            trait_ref,
+                            clauses.join("; "),
+                            self.def_id
+                        ))
+                    }
+                } else {
+                    new_kind
+                }
+            }
+        }));
+
         trace!("Translated generics: {generic_params:?}");
         generic_params
     }

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

@@ -1,11 +1,11 @@
 use super::translate_ctx::*;
 use super::translate_traits::PredicateLocation;
+use charon_lib::common::*;
 use charon_lib::formatter::AstFormatter;
 use charon_lib::gast::*;
 use charon_lib::ids::Vector;
 use charon_lib::pretty::FmtWithCtx;
 use charon_lib::types::*;
-use charon_lib::{common::*, formatter::IntoFormatter};
 use hax_frontend_exporter as hax;
 use macros::{EnumAsGetters, EnumIsA, EnumToGetters};
 use rustc_hir::def_id::DefId;
@@ -38,6 +38,25 @@ pub(crate) struct NonLocalTraitClause {
     pub trait_ref_kind: TraitRefKind,
 }
 
+impl NonLocalTraitClause {
+    fn matches(&self, hax_trait_ref: &hax::TraitRef) -> bool {
+        // We ignore regions.
+        let skip_lifetimes = |arg: &&hax::GenericArg| match arg {
+            hax::GenericArg::Lifetime(_) => false,
+            _ => true,
+        };
+        hax_trait_ref
+            .generic_args
+            .iter()
+            .filter(skip_lifetimes)
+            .eq(self
+                .hax_trait_ref
+                .generic_args
+                .iter()
+                .filter(skip_lifetimes))
+    }
+}
+
 impl<C: AstFormatter> FmtWithCtx<C> for NonLocalTraitClause {
     fn fmt_with_ctx(&self, ctx: &C) -> String {
         let clause_id = self.trait_ref_kind.fmt_with_ctx(ctx);
@@ -527,7 +546,10 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
     /// Find the trait instance fullfilling a trait obligation.
     /// TODO: having to do this is very annoying. Isn't there a better way?
     #[tracing::instrument(skip(self))]
-    fn find_trait_clause_for_param(&self, hax_trait_ref: &hax::TraitRef) -> TraitRefKind {
+    pub(crate) fn find_trait_clause_for_param(
+        &self,
+        hax_trait_ref: &hax::TraitRef,
+    ) -> TraitRefKind {
         trace!(
             "Inside context of: {:?}\nSpan: {:?}",
             self.def_id,
@@ -539,58 +561,13 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         if let Some(clauses_for_this_trait) = self.trait_clauses.get(&OrdRustId::TraitDecl(def_id))
         {
             for trait_clause in clauses_for_this_trait {
-                // We ignore regions.
-                if hax_trait_ref
-                    .generic_args
-                    .iter()
-                    .filter(|arg| match arg {
-                        hax::GenericArg::Lifetime(_) => false,
-                        _ => true,
-                    })
-                    .eq(trait_clause
-                        .hax_trait_ref
-                        .generic_args
-                        .iter()
-                        .filter(|arg| match arg {
-                            hax::GenericArg::Lifetime(_) => false,
-                            _ => true,
-                        }))
-                {
+                if trait_clause.matches(hax_trait_ref) {
                     return trait_clause.trait_ref_kind.clone();
                 }
             }
         };
 
-        // Could not find a clause.
-        // Check if we are in the registration process, otherwise report an error.
-        // TODO: we might be registering a where clause.
-        let fmt_ctx = self.into_fmt();
-        let trait_ref = format!("{:?}", hax_trait_ref);
-        let clauses: Vec<String> = self
-            .trait_clauses
-            .values()
-            .flat_map(|x| x)
-            .map(|x| x.fmt_with_ctx(&fmt_ctx))
-            .collect();
-
-        if !self.t_ctx.continue_on_failure() {
-            let clauses = clauses.join("\n");
-            unreachable!(
-                "Could not find a clause for parameter:\n- target param: {}\n- available clauses:\n{}\n- context: {:?}",
-                trait_ref, clauses, self.def_id
-            );
-        } else {
-            // Return the UNKNOWN clause
-            tracing::warn!(
-                "Could not find a clause for parameter:\n- target param: {}\n- available clauses:\n{}\n- context: {:?}",
-                trait_ref, clauses.join("\n"), self.def_id
-            );
-            TraitRefKind::Unknown(format!(
-                "Could not find a clause for parameter: {} (available clauses: {}) (context: {:?})",
-                trait_ref,
-                clauses.join("; "),
-                self.def_id
-            ))
-        }
+        // Try solving it again later, when more clauses are registered.
+        TraitRefKind::Unsolved(hax_trait_ref.clone())
     }
 }

charon/src/pretty/fmt_with_ctx.rs

@@ -1304,6 +1304,7 @@ impl<C: AstFormatter> FmtWithCtx<C> for TraitRefKind {
             }
             TraitRefKind::Clause(id) => ctx.format_object(*id),
             TraitRefKind::BuiltinOrAuto(tr) | TraitRefKind::Dyn(tr) => tr.fmt_with_ctx(ctx),
+            TraitRefKind::Unsolved(tref) => format!("Unsolved({tref:?})"),
             TraitRefKind::Unknown(msg) => format!("UNKNOWN({msg})"),
         }
     }

charon/src/transform/check_generics.rs

@@ -111,6 +111,7 @@ impl CheckGenericsVisitor<'_, '_> {
             | TraitRefKind::ParentClause(..)
             | TraitRefKind::ItemClause(..)
             | TraitRefKind::SelfId
+            | TraitRefKind::Unsolved(_)
             | TraitRefKind::Unknown(_) => {}
         }
     }

charon/tests/ui/find-sized-clause.out

@@ -1,18 +1,13 @@
-thread 'rustc' panicked at src/bin/charon-driver/translate/translate_predicates.rs:578:13:
-internal error: entered unreachable code: Could not find a clause for parameter:
-- target param: TraitRef { def_id: core::marker::Sized, generic_args: [Type(Param(ParamTy { index: 0, name: "T" }))] }
-- available clauses:
+# Final LLBC before serialization:
+
+trait test_crate::Trait<Self>
+
+enum core::option::Option<T> =
+|  None()
+|  Some(T)
+
+
+impl<T> test_crate::{impl test_crate::Trait for core::option::Option<T>}<T> : test_crate::Trait<core::option::Option<T>>
 
-- context: test_crate::{impl#0}
-note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
-error: Thread panicked when extracting item `test_crate::{impl#0}`.
- --> tests/ui/find-sized-clause.rs:5:1
-  |
-5 | impl<T> Trait for Option<T> {}
-  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^
 
-thread 'rustc' panicked at src/bin/charon-driver/translate/translate_crate_to_ullbc.rs:284:25:
-Thread panicked when extracting item `test_crate::{impl#0}`.
-error: aborting due to 1 previous error
 
-Error: Charon driver exited with code 101

charon/tests/ui/find-sized-clause.rs

@@ -1,5 +1,3 @@
-//@ known-failure
 //@ charon-args=--abort-on-error
-
 trait Trait {}
 impl<T> Trait for Option<T> {}

charon/tests/ui/trait-instance-id.rs

@@ -1,5 +1,5 @@
 //@ charon-args=--errors-as-warnings
-// This (for now) produces `TraitInstanceId::Unsolved`; it's a regressiontest because we used to
+// This (for now) produces `TraitRefKind::Unknown`; it's a regression test because we used to
 // not parse this in `charon-ml`.
 fn main() {
     let a = [0, 1, 2, 3, 4, 5, 6];

charon/tests/ui/unsupported/advanced-const-generics.out

@@ -1,4 +1,4 @@
-thread 'rustc' panicked at src/ast/types.rs:644:5:
+thread 'rustc' panicked at src/ast/types.rs:651:5:
 internal error: entered unreachable code: Ty::to_literal: Not the proper variant
 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
 error: Thread panicked when extracting item `test_crate::foo`.