Various improvements to trait clauses

charon-ml/src/CharonVersion.ml

@@ -1,3 +1,3 @@
 (* This is an automatically generated file, generated from `charon/Cargo.toml`. *)
 (* To re-generate this file, rune `make` in the root directory *)
-let supported_charon_version = "0.1.12"
+let supported_charon_version = "0.1.13"

charon-ml/src/GAstOfJson.ml

@@ -516,6 +516,7 @@ let trait_clause_of_json (id_to_file : id_to_file_map) (js : json) :
         [
           ("clause_id", clause_id);
           ("span", span);
+          ("origin", _);
           ("trait_id", trait_id);
           ("generics", generics);
         ] ->

charon/Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "charon"
-version = "0.1.12"
+version = "0.1.13"
 authors = ["Son Ho <[email protected]>"]
 edition = "2021"
 

charon/src/ast/names_utils.rs

@@ -5,6 +5,7 @@
 use crate::common::*;
 use crate::names::*;
 use crate::translate_ctx::*;
+use crate::types::PredicateOrigin;
 use hax_frontend_exporter as hax;
 use hax_frontend_exporter::SInto;
 use rustc_hir::{Item, ItemKind};
@@ -194,26 +195,28 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
                     // a body translation context.
                     let id = cur_id;
 
+                    // Translate from hax to LLBC
+                    let mut bt_ctx = BodyTransCtx::new(id, self);
+
                     // Translate to hax types
-                    let s1 = &hax::State::new_from_state_and_id(&self.hax_state, id);
-                    let substs =
-                        rustc_middle::ty::GenericArgs::identity_for_item(tcx, id).sinto(s1);
                     // TODO: use the bounds
-                    let _bounds: Vec<hax::Clause> = tcx
+                    let _bounds: Vec<hax::Clause> = bt_ctx
+                        .t_ctx
+                        .tcx
                         .predicates_of(id)
                         .predicates
                         .iter()
-                        .map(|(x, _)| x.sinto(s1))
+                        .map(|(x, _)| x.sinto(&bt_ctx.hax_state))
                         .collect();
-                    let ty = tcx.type_of(id).instantiate_identity().sinto(s1);
-
-                    // Translate from hax to LLBC
-                    let mut bt_ctx = BodyTransCtx::new(id, self);
+                    let ty = tcx
+                        .type_of(id)
+                        .instantiate_identity()
+                        .sinto(&bt_ctx.hax_state);
 
+                    bt_ctx.translate_generic_params(id).unwrap();
                     bt_ctx
-                        .translate_generic_params_from_hax(span, &substs)
+                        .translate_predicates_of(None, id, PredicateOrigin::WhereClauseOnImpl)
                         .unwrap();
-                    bt_ctx.translate_predicates_of(None, id).unwrap();
                     let erase_regions = false;
                     // Two cases, depending on whether the impl block is
                     // a "regular" impl block (`impl Foo { ... }`) or a trait
@@ -285,23 +288,6 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
         Ok(Name { name })
     }
 
-    pub(crate) fn make_hax_state_with_id(
-        &mut self,
-        def_id: DefId,
-    ) -> hax::State<hax::Base<'tcx>, (), (), DefId> {
-        hax::state::State {
-            thir: (),
-            mir: (),
-            owner_id: def_id,
-            base: hax::Base::new(
-                self.tcx,
-                hax::options::Options {
-                    inline_macro_calls: Vec::new(),
-                },
-            ),
-        }
-    }
-
     /// Returns an optional name for an HIR item.
     ///
     /// If the option is `None`, it means the item is to be ignored (example: it

charon/src/ast/types.rs

@@ -222,15 +222,7 @@ pub enum TraitInstanceId {
     /// is useful to give priority to the local clauses when solving the trait
     /// obligations which are fullfilled by the trait parameters.
     SelfId,
-    /// Clause which hasn't been solved yet.
-    /// This happens when we register clauses in the context: solving some
-    /// trait obligations/references might require to refer to clauses which
-    /// haven't been registered yet. This variant is purely internal: after we
-    /// finished solving the trait obligations, all the remaining unsolved
-    /// clauses (in case we don't fail hard on error) are converted to [Unknown].
-    Unsolved(TraitDeclId, GenericArgs),
     /// For error reporting.
-    /// Can appear only if the option [CliOpts::continue_on_failure] is used.
     Unknown(String),
 }
 
@@ -343,6 +335,7 @@ generate_index_type!(TraitClauseId, "TraitClause");
 generate_index_type!(TraitDeclId, "TraitDecl");
 generate_index_type!(TraitImplId, "TraitImpl");
 
+/// A predicate of the form `Type: Trait<Args>`.
 #[derive(Debug, Clone, Serialize, Deserialize, Derivative, Drive, DriveMut)]
 #[derivative(PartialEq)]
 pub struct TraitClause {
@@ -352,13 +345,62 @@ pub struct TraitClause {
     pub clause_id: TraitClauseId,
     #[derivative(PartialEq = "ignore")]
     pub span: Option<Span>,
+    /// Where the predicate was written, relative to the item that requires it.
+    #[derivative(PartialEq = "ignore")]
+    pub origin: PredicateOrigin,
+    /// The trait that is implemented.
     pub trait_id: TraitDeclId,
+    /// The generics applied to the trait. Note: this includes the `Self` type.
     /// Remark: the trait refs list in the [generics] field should be empty.
     pub generics: GenericArgs,
 }
 
 impl Eq for TraitClause {}
 
+/// Where a given predicate came from.
+#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize, Derivative, Drive, DriveMut)]
+pub enum PredicateOrigin {
+    // Note: we use this for globals too, but that's only available with an unstable feature.
+    // ```
+    // fn function<T: Clone>() {}
+    // fn function<T>() where T: Clone {}
+    // const NONE<T: Copy>: Option<T> = None;
+    // ```
+    WhereClauseOnFn,
+    // ```
+    // struct Struct<T: Clone> {}
+    // struct Struct<T> where T: Clone {}
+    // type TypeAlias<T: Clone> = ...;
+    // ```
+    WhereClauseOnType,
+    // Note: this is both trait impls and inherent impl blocks.
+    // ```
+    // impl<T: Clone> Type<T> {}
+    // impl<T> Type<T> where T: Clone {}
+    // impl<T> Trait for Type<T> where T: Clone {}
+    // ```
+    WhereClauseOnImpl,
+    // The special `Self: Trait` clause which is in scope inside the definition of `Foo` or an
+    // implementation of it.
+    // ```
+    // trait Trait {}
+    // ```
+    TraitSelf,
+    // Note: this also includes supertrait constraings.
+    // ```
+    // trait Trait<T: Clone> {}
+    // trait Trait<T> where T: Clone {}
+    // trait Trait: Clone {}
+    // ```
+    WhereClauseOnTrait,
+    // ```
+    // trait Trait {
+    //     type AssocType: Clone;
+    // }
+    // ```
+    TraitItem(TraitItemName),
+}
+
 /// A type declaration.
 ///
 /// Types can be opaque or transparent.

charon/src/pretty/fmt_with_ctx.rs

@@ -1188,13 +1188,6 @@ impl<C: AstFormatter> FmtWithCtx<C> for TraitInstanceId {
             TraitInstanceId::TraitImpl(id) => ctx.format_object(*id),
             TraitInstanceId::Clause(id) => ctx.format_object(*id),
             TraitInstanceId::BuiltinOrAuto(id) => ctx.format_object(*id),
-            TraitInstanceId::Unsolved(trait_id, generics) => {
-                format!(
-                    "Unsolved({}{})",
-                    ctx.format_object(*trait_id),
-                    generics.fmt_with_ctx(ctx),
-                )
-            }
             TraitInstanceId::Unknown(msg) => format!("UNKNOWN({msg})"),
         }
     }

charon/src/transform/ullbc_to_llbc.rs

@@ -1411,7 +1411,6 @@ fn compute_loop_switch_exits(cfg_info: &CfgInfo) -> ExitInfo {
     exit_info
 }
 
-// FIXME: don't fold
 fn combine_statements_and_statement(
     statements: Vec<tgt::Statement>,
     next: Option<tgt::Statement>,

charon/src/translate/translate_crate_to_ullbc.rs

@@ -3,62 +3,16 @@ use crate::common::*;
 use crate::get_mir::{extract_constants_at_top_level, MirLevel};
 use crate::transform::TransformCtx;
 use crate::translate_ctx::*;
-use crate::translate_functions_to_ullbc;
 
 use hax_frontend_exporter as hax;
 use hax_frontend_exporter::SInto;
 use rustc_hir::def_id::DefId;
-use rustc_hir::{Defaultness, ForeignItemKind, ImplItem, ImplItemKind, Item, ItemKind};
+use rustc_hir::{ForeignItemKind, ImplItemKind, Item, ItemKind};
 use rustc_middle::ty::TyCtxt;
 use rustc_session::Session;
 use std::collections::{HashMap, HashSet};
 
 impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
-    fn register_local_hir_impl_item(&mut self, _top_item: bool, impl_item: &ImplItem) {
-        // TODO: make a proper error message
-        assert!(impl_item.defaultness == Defaultness::Final);
-
-        let def_id = impl_item.owner_id.to_def_id();
-
-        // Match on the impl item kind
-        match &impl_item.kind {
-            ImplItemKind::Const(_, _) => {
-                // Can happen in traits:
-                // ```
-                // trait Foo {
-                //   const C : usize;
-                // }
-                //
-                // impl Foo for Bar {
-                //   const C = 32; // HERE
-                // }
-                // ```
-                let _ = self.register_global_decl_id(&None, def_id);
-            }
-            ImplItemKind::Type(_) => {
-                // Trait type:
-                // ```
-                // trait Foo {
-                //   type T;
-                // }
-                //
-                // impl Foo for Bar {
-                //   type T = bool; // HERE
-                // }
-                // ```
-                //
-                // Do nothing for now: we won't generate a top-level definition
-                // for this, and handle it when translating the trait implementation
-                // this item belongs to.
-                let tcx = self.tcx;
-                assert!(tcx.associated_item(def_id).trait_item_def_id.is_some());
-            }
-            ImplItemKind::Fn(_, _) => {
-                let _ = self.register_fun_decl_id(&None, def_id);
-            }
-        }
-    }
-
     /// General function to register a MIR item. It is called on all the top-level
     /// items. This includes: crate inclusions and `use` instructions (which are
     /// ignored), but also type and functions declarations.
@@ -146,8 +100,18 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
 
             ItemKind::Impl(impl_block) => {
                 trace!("impl");
-                // Sanity checks - TODO: remove?
-                translate_functions_to_ullbc::check_impl_item(impl_block);
+                // Sanity checks
+                // TODO: make proper error messages
+                use rustc_hir::{Defaultness, ImplPolarity, Unsafety};
+                assert!(impl_block.unsafety == Unsafety::Normal);
+                // About polarity:
+                // [https://doc.rust-lang.org/beta/unstable-book/language-features/negative-impls.html]
+                // Not sure about what I should do about it. Should I do anything, actually?
+                // This seems useful to enforce some discipline on the user-side, but not
+                // necessary for analysis purposes.
+                assert!(impl_block.polarity == ImplPolarity::Positive);
+                // Not sure what this is about
+                assert!(impl_block.defaultness == Defaultness::Final);
 
                 // If this is a trait implementation, register it
                 if self.tcx.trait_id_of_impl(def_id).is_some() {
@@ -161,7 +125,48 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
                     // we need to look it up
                     let impl_item = hir_map.impl_item(impl_item_ref.id);
 
-                    self.register_local_hir_impl_item(false, impl_item);
+                    // TODO: make a proper error message
+                    assert!(impl_item.defaultness == Defaultness::Final);
+
+                    let def_id = impl_item.owner_id.to_def_id();
+
+                    // Match on the impl item kind
+                    match &impl_item.kind {
+                        ImplItemKind::Const(_, _) => {
+                            // Can happen in traits:
+                            // ```
+                            // trait Foo {
+                            //   const C : usize;
+                            // }
+                            //
+                            // impl Foo for Bar {
+                            //   const C = 32; // HERE
+                            // }
+                            // ```
+                            let _ = self.register_global_decl_id(&None, def_id);
+                        }
+                        ImplItemKind::Type(_) => {
+                            // Trait type:
+                            // ```
+                            // trait Foo {
+                            //   type T;
+                            // }
+                            //
+                            // impl Foo for Bar {
+                            //   type T = bool; // HERE
+                            // }
+                            // ```
+                            //
+                            // Do nothing for now: we won't generate a top-level definition
+                            // for this, and handle it when translating the trait implementation
+                            // this item belongs to.
+                            let tcx = self.tcx;
+                            assert!(tcx.associated_item(def_id).trait_item_def_id.is_some());
+                        }
+                        ImplItemKind::Fn(_, _) => {
+                            let _ = self.register_fun_decl_id(&None, def_id);
+                        }
+                    }
                 }
                 Ok(())
             }

charon/src/translate/translate_ctx.rs

@@ -310,13 +310,7 @@ pub(crate) struct BodyTransCtx<'tcx, 'ctx, 'ctx1> {
     /// `ImplExprAtom::LocalBound`, we use this to recover the specific trait reference it
     /// corresponds to.
     /// FIXME: hax should take care of this matching up.
-    pub trait_clauses: HashMap<TraitDeclId, Vec<NonLocalTraitClause>>,
-    /// If [true] it means we are currently registering trait clauses in the
-    /// local context. As a consequence, we allow not solving all the trait
-    /// obligations, because the obligations for some clauses may be solved
-    /// by other clauses which have not been registered yet.
-    /// For this reason, we do the resolution in several passes.
-    pub registering_trait_clauses: bool,
+    pub trait_clauses: BTreeMap<TraitDeclId, Vec<NonLocalTraitClause>>,
     ///
     pub types_outlive: Vec<TypeOutlives>,
     ///
@@ -817,7 +811,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
 impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
     /// Create a new `ExecContext`.
     pub(crate) fn new(def_id: DefId, t_ctx: &'ctx mut TranslateCtx<'tcx, 'ctx1>) -> Self {
-        let hax_state = t_ctx.make_hax_state_with_id(def_id);
+        let hax_state = hax::State::new_from_state_and_id(&t_ctx.hax_state, def_id);
         BodyTransCtx {
             def_id,
             t_ctx,
@@ -833,7 +827,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
             const_generic_vars_map: MapGenerator::new(),
             clause_translation_context: Default::default(),
             trait_clauses: Default::default(),
-            registering_trait_clauses: false,
             regions_outlive: Vec::new(),
             types_outlive: Vec::new(),
             trait_type_constraints: Vec::new(),
@@ -1068,19 +1061,6 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         (out, new_ctx)
     }
 
-    /// Set [registering_trait_clauses] to [true], call the continuation, and
-    /// reset it to [false]
-    pub(crate) fn while_registering_trait_clauses<F, T>(&mut self, f: F) -> T
-    where
-        F: FnOnce(&mut Self) -> T,
-    {
-        assert!(!self.registering_trait_clauses);
-        self.registering_trait_clauses = true;
-        let out = f(self);
-        self.registering_trait_clauses = false;
-        out
-    }
-
     pub(crate) fn make_dep_source(&self, span: rustc_span::Span) -> Option<DepSource> {
         DepSource::make(self.def_id, span)
     }