Fix for duplicate vtable field names

compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs

@@ -653,13 +653,11 @@ impl Type {
     ///     f1.typ f1.data; ...
     /// }
     pub fn struct_type(name: &str, components: Vec<DatatypeComponent>) -> Self {
-        // TODO: turn this on after fixing issue #30
-        // <https://github.com/model-checking/rmc/issues/30>
-        //assert!(
-        //    Type::components_are_unique(&components),
-        //    "Components contain duplicates: {:?}",
-        //    components
-        //);
+        assert!(
+            Type::components_are_unique(&components),
+            "Components contain duplicates: {:?}",
+            components
+        );
         Struct { tag: name.to_string(), components }
     }
 

compiler/rustc_codegen_llvm/src/gotoc/metadata.rs

@@ -17,17 +17,13 @@ use rustc_middle::mir::interpret::Allocation;
 use rustc_middle::mir::{BasicBlock, Body, HasLocalDecls, Local, Operand, Place, Rvalue};
 use rustc_middle::ty::layout::{HasParamEnv, HasTyCtxt, TyAndLayout};
 use rustc_middle::ty::print::with_no_trimmed_paths;
-use rustc_middle::ty::{self, Binder, Instance, TraitRef, Ty, TyCtxt, TypeFoldable};
+use rustc_middle::ty::{self, Instance, Ty, TyCtxt, TypeFoldable};
 use rustc_target::abi::{HasDataLayout, LayoutOf, TargetDataLayout};
 use rustc_target::spec::Target;
 use std::iter;
 use std::path::Path;
 use tracing::debug;
 
-// TODO: this is a temporary RMC-only flag used in vtables for issue #30
-// <https://github.com/model-checking/rmc/issues/30>
-pub static VTABLE_IS_WELL_FORMED_FIELD: &str = "is_vtable_well_formed";
-
 // #[derive(RustcEncodable, RustcDecodable)]
 pub struct GotocCodegenResult {
     pub symtab: SymbolTable,
@@ -188,8 +184,7 @@ impl<'tcx> GotocCtx<'tcx> {
 
     /// Pretty name including crate path and trait information. For example:
     ///    boxtrait_fail::<Concrete as Trait>::increment
-    /// Generated from the fn instance to insert _into_ the symbol table.
-    /// Must match the format of pretty_name_from_dynamic_object.
+    /// Generated from the fn instance to insert into/lookup in the symbol table.
     /// TODO: internal unit tests https://github.com/model-checking/rmc/issues/172
     pub fn pretty_name_from_instance(&self, instance: Instance<'tcx>) -> String {
         format!(
@@ -199,22 +194,17 @@ impl<'tcx> GotocCtx<'tcx> {
         )
     }
 
-    /// Pretty name including crate path and trait information. For example:
-    ///    boxtrait_fail::<Concrete as Trait>::increment
-    /// Generated from the dynamic object type for _lookup_ from the symbol table.
-    /// Must match the format of pretty_name_from_instance.
-    pub fn pretty_name_from_dynamic_object(
-        &self,
-        def_id: DefId,
-        trait_ref_t: Binder<'_, TraitRef<'tcx>>,
-    ) -> String {
-        let normalized_object_type_name = self.normalized_name_of_dynamic_object_type(trait_ref_t);
-        format!(
-            "{}::{}::{}",
-            self.tcx.crate_name(def_id.krate),
-            normalized_object_type_name,
-            self.tcx.item_name(def_id)
-        )
+    /// For the vtable field name, we need exactly the dyn trait name and the function
+    /// name. The table itself already is scoped by the object type.
+    ///     Example: ::Shape::vol
+    /// Note: this is _not_ the same name for top-level entry into the symbol table,
+    /// which does need more crate and type information. For now, the symbol table
+    /// name is from the pretty_name_from_instance function above.
+    pub fn vtable_field_name(&self, def_id: DefId) -> String {
+        // `to_string_no_crate_verbose` is from Rust proper, we use it here because it
+        // always includes the dyn trait name and function name.
+        // Tracking a less brittle solution here: https://github.com/model-checking/rmc/issues/187
+        self.tcx.def_path(def_id).to_string_no_crate_verbose()
     }
 
     /// a human readable name in rust for reference

compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs

@@ -9,7 +9,7 @@ use super::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::btree_string_map;
 use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp};
 use rustc_middle::ty::adjustment::PointerCast;
-use rustc_middle::ty::{self, Binder, IntTy, TraitRef, Ty, UintTy};
+use rustc_middle::ty::{self, Binder, Instance, IntTy, TraitRef, Ty, UintTy};
 use rustc_span::def_id::DefId;
 use rustc_target::abi::{FieldsShape, LayoutOf, Primitive, TagEncoding, Variants};
 use tracing::{debug, warn};
@@ -671,15 +671,29 @@ impl<'tcx> GotocCtx<'tcx> {
         trait_ref_t: Binder<'_, TraitRef<'tcx>>,
         t: Ty<'tcx>,
     ) -> Expr {
-        let function_name = self.tcx.item_name(def_id).to_string();
+        let vtable_field_name = self.vtable_field_name(def_id);
         let vtable_type_name = aggr_name(&self.vtable_name(t));
         let field_type = self
             .symbol_table
-            .lookup_field_type(&vtable_type_name, &function_name)
+            .lookup_field_type(&vtable_type_name, &vtable_field_name)
             .cloned()
             .unwrap();
 
-        let pretty_function_name = self.pretty_name_from_dynamic_object(def_id, trait_ref_t);
+        // We use Instance::resolve to more closely match Rust proper behavior. The comment
+        // there says "used to find the precise code that will run for a trait method invocation"
+        // and it is used (in a more indirect way) to generate vtables.
+        let instance = Instance::resolve(
+            self.tcx,
+            ty::ParamEnv::reveal_all(),
+            def_id,
+            trait_ref_t.skip_binder().substs,
+        )
+        .unwrap()
+        .unwrap();
+
+        // TODO: stop using this pretty name here
+        // https://github.com/model-checking/rmc/issues/187
+        let pretty_function_name = self.pretty_name_from_instance(instance);
         let matching_symbols = self.symbol_table.find_by_pretty_name(&pretty_function_name); //("<path>::<Rectangle as Vol>::vol");
         match matching_symbols.len() {
             0 => {
@@ -809,14 +823,6 @@ impl<'tcx> GotocCtx<'tcx> {
                     binders.principal().unwrap().with_self_ty(ctx.tcx, src_mir_type);
                 let mut methods = ctx.codegen_vtable_methods(concrete_type, trait_type);
                 vtable_fields.append(&mut methods);
-                let fields = ctx
-                    .symbol_table
-                    .lookup_fields_in_type(&Type::struct_tag(&vtable_name))
-                    .unwrap();
-                // TODO: this is a temporary RMC-only flag for issue #30
-                // <https://github.com/model-checking/rmc/issues/30>
-                let is_well_formed = Expr::c_bool_constant(Type::components_are_unique(fields));
-                vtable_fields.push(is_well_formed);
                 let vtable = Expr::struct_expr_from_values(
                     Type::struct_tag(&vtable_name),
                     vtable_fields,

compiler/rustc_codegen_llvm/src/gotoc/statement.rs

@@ -281,48 +281,39 @@ impl<'tcx> GotocCtx<'tcx> {
                 // Mutable so that we can override it in case of a virtual function call
                 // TODO is there a better way to do this without needing the mut?
                 let mut funce = self.codegen_operand(func);
-
-                let mut stmts: Vec<Stmt> = vec![];
                 if let InstanceDef::Virtual(def_id, size) = instance.def {
                     debug!(
                         "Codegen a call through a virtual function. def_id: {:?} size: {:?}",
                         def_id, size
                     );
 
-                    //The first argument to a virtual function is a fat pointer for the trait
+                    // The first argument to a virtual function is a fat pointer for the trait
                     let trait_fat_ptr = fargs[0].to_owned();
-                    let vtable_field_name = self.tcx.item_name(def_id).to_string();
+                    let vtable_field_name = self.vtable_field_name(def_id);
 
-                    //now that we have all the stuff we need, we can actually build the dynamic call
+                    // Now that we have all the stuff we need, we can actually build the dynamic call
                     // If the original call was of the form
                     // f(arg0, arg1);
                     // The new call should be of the form
                     // arg0.vtable->f(arg0.data,arg1);
                     let vtable_ref = trait_fat_ptr.to_owned().member("vtable", &self.symbol_table);
                     let vtable = vtable_ref.dereference();
-                    let fn_ptr = vtable.clone().member(&vtable_field_name, &self.symbol_table);
+                    let fn_ptr = vtable.member(&vtable_field_name, &self.symbol_table);
                     funce = fn_ptr.dereference();
 
                     //Update the argument from arg0 to arg0.data
                     fargs[0] = trait_fat_ptr.to_owned().member("data", &self.symbol_table);
-
-                    // TODO: this is a temporary RMC-only flag for issue 30
-                    // <https://github.com/model-checking/rmc/issues/30>
-                    let is_well_formed = vtable
-                        .clone()
-                        .member(VTABLE_IS_WELL_FORMED_FIELD, &self.symbol_table)
-                        .cast_to(Type::bool());
-                    let assert_msg = format!("well formed vtable for type {:?}", &vtable.typ());
-                    let assert = Stmt::assert(is_well_formed, &assert_msg, loc.clone());
-                    stmts.push(assert);
                 }
 
                 // Actually generate the function call, and store the return value, if any.
-                stmts.append(&mut vec![
-                    self.codegen_expr_to_place(&p, funce.call(fargs)).with_location(loc.clone()),
-                    Stmt::goto(self.find_label(&target), loc.clone()),
-                ]);
-                Stmt::block(stmts, loc)
+                Stmt::block(
+                    vec![
+                        self.codegen_expr_to_place(&p, funce.call(fargs))
+                            .with_location(loc.clone()),
+                        Stmt::goto(self.find_label(&target), loc.clone()),
+                    ],
+                    loc,
+                )
             }
             ty::FnPtr(_) => {
                 let (p, target) = destination.unwrap();

compiler/rustc_codegen_llvm/src/gotoc/typ.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::cbmc::goto_program::{DatatypeComponent, Expr, Symbol, SymbolTable, Type};
 use super::cbmc::utils::aggr_name;
-use super::metadata::{GotocCtx, VTABLE_IS_WELL_FORMED_FIELD};
+use super::metadata::GotocCtx;
 use crate::btree_map;
 use rustc_ast::ast::Mutability;
 use rustc_index::vec::IndexVec;
@@ -11,8 +11,7 @@ use rustc_middle::ty::print::with_no_trimmed_paths;
 use rustc_middle::ty::print::FmtPrinter;
 use rustc_middle::ty::subst::{InternalSubsts, SubstsRef};
 use rustc_middle::ty::{
-    self, AdtDef, Binder, FloatTy, Instance, IntTy, PolyFnSig, TraitRef, Ty, TyS, UintTy,
-    VariantDef,
+    self, AdtDef, FloatTy, Instance, IntTy, PolyFnSig, Ty, TyS, UintTy, VariantDef,
 };
 use rustc_span;
 use rustc_span::def_id::DefId;
@@ -131,14 +130,13 @@ impl<'tcx> GotocCtx<'tcx> {
         // gives an Irep Pointer object for the signature
         let fnptr = self.codegen_dynamic_function_sig(sig).to_pointer();
 
-        //DSN For now, use the pretty name not the mangled name.
-        let _mangled_fname = self.symbol_name(instance);
-        let pretty_fname = self.tcx.item_name(def_id).to_string();
+        // vtable field name, i.e., ::Shape::vol
+        let vtable_field_name = self.vtable_field_name(def_id);
 
         let ins_ty = instance.ty(self.tcx, ty::ParamEnv::reveal_all());
         let _layout = self.layout_of(ins_ty);
 
-        Type::datatype_component(&pretty_fname, fnptr)
+        Type::datatype_component(&vtable_field_name, fnptr)
     }
 
     /// Generates a vtable that looks like this:
@@ -148,8 +146,6 @@ impl<'tcx> GotocCtx<'tcx> {
     ///      size_t align;
     ///      int (*f)(int) f1;
     ///      ...
-    ///      bool is_well_formed; //< TODO: this is a temporary RMC-only flag for issue #30
-    ///                           // <https://github.com/model-checking/rmc/issues/30>
     ///   }
     /// Ensures that the vtable is added to the symbol table.
     fn codegen_trait_vtable_type(&mut self, t: &'tcx ty::TyS<'tcx>) -> Type {
@@ -201,32 +197,12 @@ impl<'tcx> GotocCtx<'tcx> {
                 Type::datatype_component("align", Type::size_t()),
             ];
             vtable_base.append(&mut flds);
-            // TODO: this is a temporary RMC-only flag for issue #30
-            // <https://github.com/model-checking/rmc/issues/30>
-            vtable_base.push(Type::datatype_component(VTABLE_IS_WELL_FORMED_FIELD, Type::c_bool()));
             vtable_base
         } else {
             unreachable!("Expected to get a dynamic object here");
         }
     }
 
-    /// Given a Binder<TraitRef>, gives back a normalized name for the dynamic type
-    /// For example, if we have a `Rectangle` that implements a `Shape`, this will give back
-    /// "<Rectangle as Shape>"
-    ///
-    /// This is used to generate the pretty name of trait methods when building the vtable.
-    /// Ideally, we would just use Instance::resolve() to get a defid for a vtable method.
-    /// Unfortunately, this doesn't currently work, so instead, we look at the pretty name of the method, and look by that.
-    /// As with vtable_name, we have both cases which have "&" and cases which don't.
-    /// e.g. "<Rectangle as Shape>" and "<&Rectangle as Shape>".
-    /// We solve this by normalizeing and removing the "&">::vol", but the inner type would be <&Rectangle as Vol>
-    pub fn normalized_name_of_dynamic_object_type(
-        &self,
-        trait_ref_t: Binder<'_, TraitRef<'tcx>>,
-    ) -> String {
-        with_no_trimmed_paths(|| trait_ref_t.skip_binder().to_string().replace("&", ""))
-    }
-
     /// Gives the name for a trait.
     /// In some cases, we have &T, in other cases T, so normalize.
     pub fn normalized_trait_name(&self, t: Ty<'tcx>) -> String {

src/test/cbmc/DynTrait/different_crates.rs

@@ -0,0 +1,53 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test uses a trait defined in a different crate (the standard library)
+// and a test defined in the local crate. The goal is to test vtable resolution
+// of duplicate names across different crates.
+struct Counter {
+    count: usize,
+}
+
+// A custom impl for the standard library trait.
+impl std::iter::Iterator for Counter {
+    type Item = usize;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        // Increment our count. 
+        self.count += 1;
+        Some(self.count)
+    }
+}
+
+// An impl for our local trait, with an indentical name to the standard library
+trait Iterator {
+    fn next(&mut self) -> Option<usize>;
+}
+
+impl Iterator for Counter {
+    fn next(&mut self) -> Option<usize> {
+        Some(42)
+    }
+}
+
+trait Combined : Iterator + std::iter::Iterator<Item = usize> {}
+
+impl Combined for Counter {}
+
+fn std_count(c : &mut dyn std::iter::Iterator<Item = usize>) -> usize {
+    c.next().unwrap()
+}
+
+fn weird_count(c : &mut dyn Iterator) -> usize {
+    c.next().unwrap()
+}
+
+fn main() {
+    let counter : &mut Counter = &mut Counter { count: 0 };
+    assert!(std_count(counter as &mut dyn std::iter::Iterator<Item = usize>) == 1);
+    assert!(weird_count(counter as &mut dyn Iterator) == 42);
+
+    let counter_combined = counter as &mut dyn Combined;
+    assert!(std::iter::Iterator::next(counter_combined).unwrap() == 2);
+    assert!(Iterator::next(counter_combined).unwrap() == 42);
+}

src/test/cbmc/DynTrait/different_crates_fail.rs

@@ -0,0 +1,53 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test uses a trait defined in a different crate (the standard library)
+// and a test defined in the local crate. The goal is to test vtable resolution
+// of duplicate names across different crates.
+struct Counter {
+    count: usize,
+}
+
+// A custom impl for the standard library trait.
+impl std::iter::Iterator for Counter {
+    type Item = usize;
+
+    fn next(&mut self) -> Option<Self::Item> {
+        // Increment our count. 
+        self.count += 1;
+        Some(self.count)
+    }
+}
+
+// An impl for our local trait, with an indentical name to the standard library
+trait Iterator {
+    fn next(&mut self) -> Option<usize>;
+}
+
+impl Iterator for Counter {
+    fn next(&mut self) -> Option<usize> {
+        Some(42)
+    }
+}
+
+trait Combined : Iterator + std::iter::Iterator<Item = usize> {}
+
+impl Combined for Counter {}
+
+fn std_count(c : &mut dyn std::iter::Iterator<Item = usize>) -> usize {
+    c.next().unwrap()
+}
+
+fn weird_count(c : &mut dyn Iterator) -> usize {
+    c.next().unwrap()
+}
+
+fn main() {
+    let counter : &mut Counter = &mut Counter { count: 0 };
+    assert!(std_count(counter as &mut dyn std::iter::Iterator<Item = usize>) == 0); // Should be 1
+    assert!(weird_count(counter as &mut dyn Iterator) == 0); // Should be 42
+
+    let counter_combined = counter as &mut dyn Combined;
+    assert!(std::iter::Iterator::next(counter_combined).unwrap() == 0); // Should be 2
+    assert!(Iterator::next(counter_combined).unwrap() == 0); // Should be 42
+}