22// SPDX-License-Identifier: Apache-2.0 OR MIT
33use super :: cbmc:: goto_program:: { DatatypeComponent , Expr , Symbol , SymbolTable , Type } ;
44use super :: cbmc:: utils:: aggr_name;
5- use super :: metadata:: { GotocCtx , VTABLE_IS_WELL_FORMED_FIELD } ;
5+ use super :: metadata:: GotocCtx ;
66use crate :: btree_map;
77use rustc_ast:: ast:: Mutability ;
88use rustc_index:: vec:: IndexVec ;
@@ -11,8 +11,7 @@ use rustc_middle::ty::print::with_no_trimmed_paths;
1111use rustc_middle:: ty:: print:: FmtPrinter ;
1212use rustc_middle:: ty:: subst:: { InternalSubsts , SubstsRef } ;
1313use rustc_middle:: ty:: {
14- self , AdtDef , Binder , FloatTy , Instance , IntTy , PolyFnSig , TraitRef , Ty , TyS , UintTy ,
15- VariantDef ,
14+ self , AdtDef , FloatTy , Instance , IntTy , PolyFnSig , Ty , TyS , UintTy , VariantDef ,
1615} ;
1716use rustc_span;
1817use rustc_span:: def_id:: DefId ;
@@ -131,14 +130,13 @@ impl<'tcx> GotocCtx<'tcx> {
131130 // gives an Irep Pointer object for the signature
132131 let fnptr = self . codegen_dynamic_function_sig ( sig) . to_pointer ( ) ;
133132
134- //DSN For now, use the pretty name not the mangled name.
135- let _mangled_fname = self . symbol_name ( instance) ;
136- let pretty_fname = self . tcx . item_name ( def_id) . to_string ( ) ;
133+ // vtable field name, i.e., ::Shape::vol
134+ let vtable_field_name = self . vtable_field_name ( def_id) ;
137135
138136 let ins_ty = instance. ty ( self . tcx , ty:: ParamEnv :: reveal_all ( ) ) ;
139137 let _layout = self . layout_of ( ins_ty) ;
140138
141- Type :: datatype_component ( & pretty_fname , fnptr)
139+ Type :: datatype_component ( & vtable_field_name , fnptr)
142140 }
143141
144142 /// Generates a vtable that looks like this:
@@ -148,8 +146,6 @@ impl<'tcx> GotocCtx<'tcx> {
148146 /// size_t align;
149147 /// int (*f)(int) f1;
150148 /// ...
151- /// bool is_well_formed; //< TODO: this is a temporary RMC-only flag for issue #30
152- /// // <https://github.com/model-checking/rmc/issues/30>
153149 /// }
154150 /// Ensures that the vtable is added to the symbol table.
155151 fn codegen_trait_vtable_type ( & mut self , t : & ' tcx ty:: TyS < ' tcx > ) -> Type {
@@ -201,32 +197,12 @@ impl<'tcx> GotocCtx<'tcx> {
201197 Type :: datatype_component( "align" , Type :: size_t( ) ) ,
202198 ] ;
203199 vtable_base. append ( & mut flds) ;
204- // TODO: this is a temporary RMC-only flag for issue #30
205- // <https://github.com/model-checking/rmc/issues/30>
206- vtable_base. push ( Type :: datatype_component ( VTABLE_IS_WELL_FORMED_FIELD , Type :: c_bool ( ) ) ) ;
207200 vtable_base
208201 } else {
209202 unreachable ! ( "Expected to get a dynamic object here" ) ;
210203 }
211204 }
212205
213- /// Given a Binder<TraitRef>, gives back a normalized name for the dynamic type
214- /// For example, if we have a `Rectangle` that implements a `Shape`, this will give back
215- /// "<Rectangle as Shape>"
216- ///
217- /// This is used to generate the pretty name of trait methods when building the vtable.
218- /// Ideally, we would just use Instance::resolve() to get a defid for a vtable method.
219- /// Unfortunately, this doesn't currently work, so instead, we look at the pretty name of the method, and look by that.
220- /// As with vtable_name, we have both cases which have "&" and cases which don't.
221- /// e.g. "<Rectangle as Shape>" and "<&Rectangle as Shape>".
222- /// We solve this by normalizeing and removing the "&">::vol", but the inner type would be <&Rectangle as Vol>
223- pub fn normalized_name_of_dynamic_object_type (
224- & self ,
225- trait_ref_t : Binder < ' _ , TraitRef < ' tcx > > ,
226- ) -> String {
227- with_no_trimmed_paths ( || trait_ref_t. skip_binder ( ) . to_string ( ) . replace ( "&" , "" ) )
228- }
229-
230206 /// Gives the name for a trait.
231207 /// In some cases, we have &T, in other cases T, so normalize.
232208 pub fn normalized_trait_name ( & self , t : Ty < ' tcx > ) -> String {
0 commit comments