Encode unknown generic type parameters with (declare-forall-sort)

src/analyze/annot.rs

@@ -98,6 +98,14 @@ pub fn closure_model_path() -> [Symbol; 3] {
     ]
 }
 
+pub fn ghost_model_path() -> [Symbol; 3] {
+    [
+        Symbol::intern("thrust"),
+        Symbol::intern("def"),
+        Symbol::intern("ghost_model"),
+    ]
+}
+
 pub fn mut_model_new_path() -> [Symbol; 3] {
     [
         Symbol::intern("thrust"),

src/analyze/annot_fn.rs

@@ -1,12 +1,15 @@
 use std::collections::HashMap;
 
 use pretty::{termcolor, Pretty};
-use rustc_hir::{def_id::LocalDefId, HirId};
+use rustc_hir::{
+    def_id::{DefId, LocalDefId},
+    HirId,
+};
 use rustc_index::IndexVec;
-use rustc_middle::ty::{self as mir_ty, TyCtxt};
+use rustc_middle::ty::{self as mir_ty, TyCtxt, TypeFoldable};
 
 use crate::analyze::{self, did_cache::DefIdCache};
-use crate::chc;
+use crate::chc::{self};
 use crate::refine::{self, TypeBuilder};
 use crate::rty;
 
@@ -204,12 +207,20 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
         analyzer: &'a analyze::Analyzer<'tcx>,
         local_def_id: LocalDefId,
         generic_args: mir_ty::GenericArgsRef<'tcx>,
+        owner_fn_id: DefId,
     ) -> Self {
         let tcx = analyzer.tcx();
         let body = tcx.hir_body_owned_by(local_def_id);
         let typeck = tcx.typeck(local_def_id);
         let def_ids = analyzer.def_ids();
-        let type_builder = TypeBuilder::new(tcx, def_ids.clone(), local_def_id.to_def_id());
+        let type_builder = TypeBuilder::new(
+            tcx,
+            def_ids.clone(),
+            owner_fn_id,
+            analyzer.type_params.clone(),
+            analyzer.closure_type_params.clone(),
+            analyzer.system.clone(),
+        );
         let mut translator = Self {
             tcx,
             local_def_id,
@@ -227,11 +238,6 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
 
     pub fn with_def_id_cache(mut self, def_ids: DefIdCache<'tcx>) -> Self {
         self.def_ids = def_ids;
-        self.type_builder = TypeBuilder::new(
-            self.tcx,
-            self.def_ids.clone(),
-            self.local_def_id.to_def_id(),
-        );
         self
     }
 
@@ -386,29 +392,52 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
         }
     }
 
+    fn instantiate_generics<T>(
+        &self,
+        ty: T,
+        generic_args: mir_ty::GenericArgsRef<'tcx>,
+    ) -> Option<T>
+    where
+        T: TypeFoldable<TyCtxt<'tcx>>,
+    {
+        if !self.generic_args.is_empty() {
+            Some(mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, generic_args))
+        } else {
+            None
+        }
+    }
+
     fn expr_ty(&self, expr: &'tcx rustc_hir::Expr<'tcx>) -> mir_ty::Ty<'tcx> {
         let ty = self.typeck.expr_ty(expr);
-        let instantiated = mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, self.generic_args);
+        let instantiated = self
+            .instantiate_generics(ty, self.generic_args)
+            .unwrap_or(ty);
         let typing_env = mir_ty::TypingEnv::fully_monomorphized();
-        self.tcx.normalize_erasing_regions(typing_env, instantiated)
+        self.tcx
+            .try_normalize_erasing_regions(typing_env, instantiated)
+            .unwrap_or(instantiated)
     }
 
     fn pat_ty(&self, pat: &'tcx rustc_hir::Pat<'tcx>) -> mir_ty::Ty<'tcx> {
         let ty = self.typeck.pat_ty(pat);
-        let instantiated = mir_ty::EarlyBinder::bind(ty).instantiate(self.tcx, self.generic_args);
+        let instantiated = self
+            .instantiate_generics(ty, self.generic_args)
+            .unwrap_or(ty);
         let typing_env = mir_ty::TypingEnv::fully_monomorphized();
-        self.tcx.normalize_erasing_regions(typing_env, instantiated)
+        self.tcx
+            .try_normalize_erasing_regions(typing_env, instantiated)
+            .unwrap_or(instantiated)
     }
 
     pub fn to_formula_fn(&self) -> FormulaFn<'tcx> {
         let formula = self.to_formula(self.body.value);
-        let params = self
-            .tcx
-            .fn_sig(self.local_def_id.to_def_id())
-            .instantiate(self.tcx, self.generic_args)
-            .skip_binder()
-            .inputs()
-            .to_vec();
+        let fn_sig = self.tcx.fn_sig(self.local_def_id.to_def_id());
+        let binder = if self.generic_args.is_empty() {
+            fn_sig.skip_binder()
+        } else {
+            fn_sig.instantiate(self.tcx, self.generic_args)
+        };
+        let params = binder.skip_binder().inputs().to_vec();
         let param_idents = self
             .tcx
             .fn_arg_idents(self.local_def_id.to_def_id())
@@ -492,10 +521,41 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
     fn receiver_closure_fn_type(&self, receiver_ty: mir_ty::Ty<'tcx>) -> Option<rty::FunctionType> {
         let closure_ty = self.receiver_closure_ty(receiver_ty)?;
         let mir_ty::TyKind::Closure(def_id, args) = closure_ty.kind() else {
+            if let mir_ty::TyKind::Param(ty) = closure_ty.kind() {
+                tracing::debug!("ParamTy is found: {ty:?}");
+                let closure_fun_ty = self.type_builder.build_closure_type_for_param(
+                    *ty,
+                    self.local_def_id,
+                    self.generic_args,
+                );
+                tracing::debug!(
+                    "the obtained FunctionType for the closure {ty:?}: {closure_fun_ty:#?}"
+                );
+                if let Some(closure_fun_ty) = closure_fun_ty.clone() {
+                    self.type_builder.register_closure_type_param(
+                        analyze::TypeParam::GenericType {
+                            param_def_id: self.type_builder.param_def_id(ty),
+                            local_idx: self.type_builder.param_local_idx(ty),
+                        },
+                        closure_fun_ty,
+                    );
+                };
+                return closure_fun_ty;
+            }
             return None;
         };
+        self.analyzer.known_function_ty_with_args(
+            *def_id,
+            self.tcx.mk_args(args.as_closure().parent_args()),
+            self.type_builder.owner_fn_id(),
+        )
+    }
+
+    fn register_forall_pred(&self, forall_pred: chc::ForallPred) {
         self.analyzer
-            .known_function_ty_with_args(*def_id, self.tcx.mk_args(args.as_closure().parent_args()))
+            .system
+            .borrow_mut()
+            .register_forall_pred(forall_pred.clone());
     }
 
     /// Extracts the logical argument terms passed to `closure_precondition`/
@@ -574,9 +634,11 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
     }
 
     fn node_arg_type_at(&self, hir_id: HirId, idx: usize) -> rty::Type<rty::Closed> {
-        let generic_args = self.typeck.node_args(hir_id);
-        let generic_args =
-            mir_ty::EarlyBinder::bind(generic_args).instantiate(self.tcx, self.generic_args);
+        let mut generic_args = self.typeck.node_args(hir_id);
+        if !self.generic_args.is_empty() {
+            generic_args =
+                mir_ty::EarlyBinder::bind(generic_args).instantiate(self.tcx, self.generic_args);
+        }
         let elem_ty = generic_args.type_at(idx);
         self.type_builder.build(elem_ty)
     }
@@ -978,7 +1040,10 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                             .next()
                             .is_some()
                         {
-                            let typing_env = mir_ty::TypingEnv::fully_monomorphized();
+                            let typing_env = mir_ty::TypingEnv::post_analysis(
+                                self.tcx,
+                                self.type_builder.owner_fn_id(),
+                            );
                             let generic_args = self.typeck.node_args(func_expr.hir_id);
                             tracing::debug!(
                                 lhs = ?def_id,
@@ -987,23 +1052,57 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                                 outer_generic_args = ?self.generic_args,
                                 "resolving predicate call in formula"
                             );
-                            let generic_args = mir_ty::EarlyBinder::bind(generic_args)
-                                .instantiate(self.tcx, self.generic_args);
+                            // `self.generic_args` is empty only when the owner has no generics,
+                            // so the predicate's own args are already concrete and there is
+                            // nothing to instantiate. In both cases `Instance::try_resolve`
+                            // decides the routing: it resolves a call on a concrete type to the
+                            // impl's predicate, and returns `None` for a call that still
+                            // depends on the owner's type parameters (an `ImplSource::Param`),
+                            // which is the only case that needs the forall predicate.
+                            let generic_args = self
+                                .instantiate_generics(generic_args, self.generic_args)
+                                .unwrap_or(generic_args);
+
                             let instance = mir_ty::Instance::try_resolve(
                                 self.tcx,
                                 typing_env,
                                 def_id,
                                 generic_args,
                             )
                             .unwrap();
-                            let pred_def_id = if let Some(instance) = instance {
-                                instance.def_id()
+                            let (is_unresolved_args, pred_def_id) = match instance {
+                                Some(instance) => (false, instance.def_id()),
+                                None => (true, def_id),
+                            };
+
+                            let pred = if is_unresolved_args {
+                                tracing::debug!(?self.local_def_id, ?generic_args, "owner_fn_id={:?}", self.type_builder.owner_fn_id());
+                                let type_params = generic_args
+                                    .types()
+                                    .map(|ty| self.type_builder.build(ty).to_sort())
+                                    .collect();
+
+                                let params = args
+                                    .iter()
+                                    .map(|expr| {
+                                        self.type_builder.build(self.expr_ty(expr)).to_sort()
+                                    })
+                                    .collect();
+
+                                let pred = refine::trait_forall_pred(
+                                    self.tcx,
+                                    pred_def_id,
+                                    type_params,
+                                    params,
+                                );
+                                self.register_forall_pred(pred.clone());
+                                pred.into()
                             } else {
-                                def_id
+                                refine::user_defined_pred(self.tcx, pred_def_id).into()
                             };
-                            let pred = refine::user_defined_pred(self.tcx, pred_def_id);
+                            tracing::debug!("resolved predicate call in formula: {:?}", pred);
                             let arg_terms = args.iter().map(|e| self.to_term(e)).collect();
-                            let atom = chc::Atom::new(pred.into(), arg_terms);
+                            let atom = chc::Atom::new(pred, arg_terms);
                             return FormulaOrTerm::Formula(chc::Formula::Atom(atom));
                         }
                     }