diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs index 6d1eee2602ef..0340ff41a5e0 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs +++ b/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) -> Self { - // TODO: turn this on after fixing issue #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 } } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs index be3dea1c103a..8397cb7462a2 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs +++ b/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 -// -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::::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::::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 diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index 497fd5c69886..b39b5980bb26 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/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); //("::::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 - // - 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, diff --git a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs index a03fb5a68d2e..186e714dd8f6 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs +++ b/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 = 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 - // - 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(); diff --git a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs index 19a5a553e653..e8490bd6fdd6 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs +++ b/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 - /// // /// } /// 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 - // - 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, gives back a normalized name for the dynamic type - /// For example, if we have a `Rectangle` that implements a `Shape`, this will give back - /// "" - /// - /// 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. "" 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 { diff --git a/src/test/cbmc/DynTrait/different_crates.rs b/src/test/cbmc/DynTrait/different_crates.rs new file mode 100644 index 000000000000..a007860ea0f7 --- /dev/null +++ b/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 { + // 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; +} + +impl Iterator for Counter { + fn next(&mut self) -> Option { + Some(42) + } +} + +trait Combined : Iterator + std::iter::Iterator {} + +impl Combined for Counter {} + +fn std_count(c : &mut dyn std::iter::Iterator) -> 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) == 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); +} \ No newline at end of file diff --git a/src/test/cbmc/DynTrait/different_crates_fail.rs b/src/test/cbmc/DynTrait/different_crates_fail.rs new file mode 100644 index 000000000000..ea51fddb21be --- /dev/null +++ b/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 { + // 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; +} + +impl Iterator for Counter { + fn next(&mut self) -> Option { + Some(42) + } +} + +trait Combined : Iterator + std::iter::Iterator {} + +impl Combined for Counter {} + +fn std_count(c : &mut dyn std::iter::Iterator) -> 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) == 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 +} \ No newline at end of file diff --git a/src/test/cbmc/DynTrait/std_lib_add_duplicate.rs b/src/test/cbmc/DynTrait/std_lib_add_duplicate.rs new file mode 100644 index 000000000000..37293b5d7178 --- /dev/null +++ b/src/test/cbmc/DynTrait/std_lib_add_duplicate.rs @@ -0,0 +1,29 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +trait WeirdAdd { + fn add(&self, rhs: i32) -> i32; +} + +impl WeirdAdd for i32 { + fn add(&self, other: i32) -> i32 { + self/2 + other/2 + } +} + +fn std_add(x: i32, y: i32) -> i32 { + x + y +} + +fn weird_add(x: &dyn WeirdAdd, y: i32) -> i32 { + x.add(y) +} + +fn main() { + let x = 2; + let y = 4; + + let std_add = std_add(x, y); + assert!(std_add == 6); + let weird_add = weird_add(&x as &dyn WeirdAdd, y); + assert!(weird_add == 3); +} diff --git a/src/test/cbmc/DynTrait/vtable_duplicate_field_override.rs b/src/test/cbmc/DynTrait/vtable_duplicate_field_override.rs new file mode 100644 index 000000000000..2ca65f1aaa20 --- /dev/null +++ b/src/test/cbmc/DynTrait/vtable_duplicate_field_override.rs @@ -0,0 +1,56 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT +trait A { + fn foo(&self) -> i32; +} + +trait B { + fn foo(&self) -> i32; +} + +trait T: A + B { + fn foo(&self) -> i32; +} + +struct S { + x: i32, + y: i32, + z: i32, +} + +impl S { + fn new(a: i32, b: i32, c: i32) -> S { + S { x: a, y: b, z: c } + } + fn new_box(a: i32, b: i32, c: i32) -> Box { + Box::new(S::new(a, b, c)) + } +} + +impl A for S { + fn foo(&self) -> i32 { + self.x + } +} + +impl B for S { + fn foo(&self) -> i32 { + self.y + } +} + +impl T for S { + fn foo(&self) -> i32 { + self.z + } +} + +fn main() { + let t = S::new_box(1, 2, 3); + let a = ::foo(&*t); + assert!(a == 1); + let b = ::foo(&*t); + assert!(b == 2); + let t_value = T::foo(&*t); + assert!(t_value == 3); +} diff --git a/src/test/cbmc/DynTrait/vtable_duplicate_fields_fixme.rs b/src/test/cbmc/DynTrait/vtable_duplicate_fields.rs similarity index 100% rename from src/test/cbmc/DynTrait/vtable_duplicate_fields_fixme.rs rename to src/test/cbmc/DynTrait/vtable_duplicate_fields.rs