@@ -10,7 +10,8 @@ use crate::btree_string_map;
10
10
use num:: bigint:: BigInt ;
11
11
use rustc_middle:: mir:: { AggregateKind , BinOp , CastKind , NullOp , Operand , Place , Rvalue , UnOp } ;
12
12
use rustc_middle:: ty:: adjustment:: PointerCast ;
13
- use rustc_middle:: ty:: { self , Binder , Instance , IntTy , TraitRef , Ty , UintTy } ;
13
+ use rustc_middle:: ty:: subst:: InternalSubsts ;
14
+ use rustc_middle:: ty:: { self , Binder , GenericParamDefKind , Instance , IntTy , TraitRef , Ty , UintTy } ;
14
15
use rustc_span:: def_id:: DefId ;
15
16
use rustc_target:: abi:: { FieldsShape , LayoutOf , Primitive , TagEncoding , Variants } ;
16
17
use tracing:: { debug, warn} ;
@@ -689,7 +690,7 @@ impl<'tcx> GotocCtx<'tcx> {
689
690
& mut self ,
690
691
def_id : DefId ,
691
692
_substs : ty:: subst:: SubstsRef < ' tcx > ,
692
- trait_ref_t : Binder < ' _ , TraitRef < ' tcx > > ,
693
+ trait_ref_t : Binder < ' tcx , TraitRef < ' tcx > > ,
693
694
t : Ty < ' tcx > ,
694
695
) -> Expr {
695
696
let vtable_field_name = self . vtable_field_name ( def_id) ;
@@ -700,17 +701,33 @@ impl<'tcx> GotocCtx<'tcx> {
700
701
. cloned ( )
701
702
. unwrap ( ) ;
702
703
704
+ ///////////////////////////////////////////////////////////////////////
705
+ // Copied from rustc impl:
706
+ // compiler/rustc_trait_selection/src/traits/mod.rs
707
+ //
708
+ // The method may have some early-bound lifetimes; add regions for those.
709
+ let substs = trait_ref_t. map_bound ( |trait_ref| {
710
+ InternalSubsts :: for_item ( self . tcx , def_id, |param, _| match param. kind {
711
+ GenericParamDefKind :: Lifetime => self . tcx . lifetimes . re_erased . into ( ) ,
712
+ GenericParamDefKind :: Type { .. } | GenericParamDefKind :: Const { .. } => {
713
+ trait_ref. substs [ param. index as usize ]
714
+ }
715
+ } )
716
+ } ) ;
717
+
718
+ // The trait type may have higher-ranked lifetimes in it;
719
+ // erase them if they appear, so that we get the type
720
+ // at some particular call site.
721
+ let substs =
722
+ self . tcx . normalize_erasing_late_bound_regions ( ty:: ParamEnv :: reveal_all ( ) , substs) ;
723
+ ///////////////////////////////////////////////////////////////////////
724
+
703
725
// We use Instance::resolve to more closely match Rust proper behavior. The comment
704
726
// there says "used to find the precise code that will run for a trait method invocation"
705
727
// and it is used (in a more indirect way) to generate vtables.
706
- let instance = Instance :: resolve (
707
- self . tcx ,
708
- ty:: ParamEnv :: reveal_all ( ) ,
709
- def_id,
710
- trait_ref_t. skip_binder ( ) . substs ,
711
- )
712
- . unwrap ( )
713
- . unwrap ( ) ;
728
+ let instance = Instance :: resolve ( self . tcx , ty:: ParamEnv :: reveal_all ( ) , def_id, substs)
729
+ . unwrap ( )
730
+ . unwrap ( ) ;
714
731
715
732
// Lookup in the symbol table using the full symbol table name/key
716
733
let fn_name = self . symbol_name ( instance) ;
@@ -739,15 +756,25 @@ impl<'tcx> GotocCtx<'tcx> {
739
756
) -> Expr {
740
757
let drop_instance = Instance :: resolve_drop_in_place ( self . tcx , ty) ;
741
758
let drop_sym_name = self . symbol_name ( drop_instance) ;
742
- let drop_sym = self . symbol_table . lookup ( & drop_sym_name ) . unwrap ( ) . clone ( ) ;
759
+ let param_types = vec ! [ self . codegen_ty ( trait_ty ) ] ;
743
760
744
761
// The drop instance has the concrete object type, for consistency with
745
762
// type codegen we need the trait type for the function parameter.
746
763
let trait_fn_ty =
747
- Type :: code_with_unnamed_parameters ( vec ! [ self . codegen_ty( trait_ty) ] , Type :: unit ( ) )
748
- . to_pointer ( ) ;
764
+ Type :: code_with_unnamed_parameters ( param_types, Type :: unit ( ) ) . to_pointer ( ) ;
749
765
750
- Expr :: symbol_expression ( drop_sym_name, drop_sym. typ ) . address_of ( ) . cast_to ( trait_fn_ty)
766
+ if let Some ( drop_sym) = self . symbol_table . lookup ( & drop_sym_name) {
767
+ Expr :: symbol_expression ( drop_sym_name, drop_sym. clone ( ) . typ )
768
+ . address_of ( )
769
+ . cast_to ( trait_fn_ty)
770
+ } else {
771
+ // TODO: check why in https://github.com/model-checking/rmc/issues/66
772
+ debug ! (
773
+ "WARNING: drop_in_place not found for {:?}" ,
774
+ self . readable_instance_name( drop_instance) ,
775
+ ) ;
776
+ Type :: void_pointer ( ) . null ( ) . cast_to ( trait_fn_ty)
777
+ }
751
778
}
752
779
753
780
fn codegen_vtable_methods (
0 commit comments