From 44339ccba9d3444b715d7a6dccfa933c10a1de44 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Tue, 8 Jun 2021 15:40:52 -0400 Subject: [PATCH 01/11] Use dyn trait name (+ function) in vtable field --- compiler/rustc_codegen_llvm/src/gotoc/metadata.rs | 10 ++++++++++ compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs | 4 ++-- compiler/rustc_codegen_llvm/src/gotoc/statement.rs | 6 +++--- compiler/rustc_codegen_llvm/src/gotoc/typ.rs | 7 +++---- ...cate_fields_fixme.rs => vtable_duplicate_fields.rs} | 0 5 files changed, 18 insertions(+), 9 deletions(-) rename src/test/cbmc/DynTrait/{vtable_duplicate_fields_fixme.rs => vtable_duplicate_fields.rs} (100%) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs index be3dea1c103a..87bb60e5bd28 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs @@ -217,6 +217,16 @@ impl<'tcx> GotocCtx<'tcx> { ) } + /// 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_* functions above. + pub fn vtable_fild_name(&self, def_id: DefId) -> String { + self.tcx.def_path(def_id).to_string_no_crate_verbose() + } + /// a human readable name in rust for reference pub fn instance_name(&self, instance: Instance<'tcx>) -> String { with_no_trimmed_paths(|| self.tcx.def_path_str(instance.def_id())) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index 497fd5c69886..a6c3ea9b2bb0 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -671,11 +671,11 @@ 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_fild_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(); diff --git a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs index a03fb5a68d2e..72f4f6f6d2e1 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs @@ -289,11 +289,11 @@ impl<'tcx> GotocCtx<'tcx> { 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_fild_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 diff --git a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs index 19a5a553e653..d92ee212920a 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs @@ -131,14 +131,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_fild_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: 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 From ca70d0d4cb02929b134d280d347798fa209575b1 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Tue, 8 Jun 2021 15:44:58 -0400 Subject: [PATCH 02/11] Remove is_vtable_well_formed flag and turn on assert for unique components --- .../src/gotoc/cbmc/goto_program/typ.rs | 12 +++++------- compiler/rustc_codegen_llvm/src/gotoc/metadata.rs | 4 ---- compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs | 4 ---- compiler/rustc_codegen_llvm/src/gotoc/statement.rs | 10 ---------- compiler/rustc_codegen_llvm/src/gotoc/typ.rs | 7 +------ 5 files changed, 6 insertions(+), 31 deletions(-) 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 87bb60e5bd28..1f7c41565084 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs @@ -24,10 +24,6 @@ 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, diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index a6c3ea9b2bb0..82f054b48c34 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -813,10 +813,6 @@ impl<'tcx> GotocCtx<'tcx> { .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 72f4f6f6d2e1..56ff1b1309fd 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs @@ -305,16 +305,6 @@ impl<'tcx> GotocCtx<'tcx> { //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. diff --git a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs index d92ee212920a..3fd368a9ed17 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; @@ -147,8 +147,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 { @@ -200,9 +198,6 @@ 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"); From db057dddc274a473120b20d2d81a866362384b4b Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Tue, 8 Jun 2021 15:59:29 -0400 Subject: [PATCH 03/11] Additional duplicate test with override --- .../vtable_duplicate_field_override.rs | 56 +++++++++++++++++++ 1 file changed, 56 insertions(+) create mode 100644 src/test/cbmc/DynTrait/vtable_duplicate_field_override.rs 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); +} From 25c63d99dcb494c002bdc37ed05c175d6fb090b1 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Tue, 8 Jun 2021 16:25:58 -0400 Subject: [PATCH 04/11] Use the instance for dyn trait object pretty names, too, which fixes the new test that otherwise breaks --- .../rustc_codegen_llvm/src/gotoc/metadata.rs | 23 ++----------------- .../rustc_codegen_llvm/src/gotoc/rvalue.rs | 12 ++++++++-- 2 files changed, 12 insertions(+), 23 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs index 1f7c41565084..a4b8f2813c0e 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs @@ -17,7 +17,7 @@ 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, Ty, TyCtxt, TypeFoldable}; use rustc_target::abi::{HasDataLayout, LayoutOf, TargetDataLayout}; use rustc_target::spec::Target; use std::iter; @@ -184,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!( @@ -195,24 +194,6 @@ 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 diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index 82f054b48c34..791856b171f8 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}; @@ -678,8 +678,16 @@ impl<'tcx> GotocCtx<'tcx> { .lookup_field_type(&vtable_type_name, &vtable_field_name) .cloned() .unwrap(); + let instance = Instance::resolve( + self.tcx, + ty::ParamEnv::reveal_all(), + def_id, + trait_ref_t.skip_binder().substs, + ) + .unwrap() + .unwrap(); - let pretty_function_name = self.pretty_name_from_dynamic_object(def_id, trait_ref_t); + 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 => { From 6bec91727a306cb51c6469c31f2b970fd650cec4 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Tue, 8 Jun 2021 17:03:17 -0400 Subject: [PATCH 05/11] Fix import, remove stale dead code --- .../rustc_codegen_llvm/src/gotoc/metadata.rs | 2 +- compiler/rustc_codegen_llvm/src/gotoc/typ.rs | 17 ----------------- 2 files changed, 1 insertion(+), 18 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs index a4b8f2813c0e..79da1c58db51 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs @@ -17,7 +17,7 @@ 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, 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; diff --git a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs index 3fd368a9ed17..14e28834b3a5 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs @@ -204,23 +204,6 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// 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 { From 2313681de1cba1f765118e314af337a0dc1ac2ab Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Tue, 8 Jun 2021 17:32:11 -0400 Subject: [PATCH 06/11] fix typo --- compiler/rustc_codegen_llvm/src/gotoc/metadata.rs | 4 ++-- compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs | 2 +- compiler/rustc_codegen_llvm/src/gotoc/statement.rs | 2 +- compiler/rustc_codegen_llvm/src/gotoc/typ.rs | 2 +- 4 files changed, 5 insertions(+), 5 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs index 79da1c58db51..041448d1a53e 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs @@ -199,8 +199,8 @@ impl<'tcx> GotocCtx<'tcx> { /// 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_* functions above. - pub fn vtable_fild_name(&self, def_id: DefId) -> String { + /// name is from the pretty_name_from_instance function above. + pub fn vtable_field_name(&self, def_id: DefId) -> String { self.tcx.def_path(def_id).to_string_no_crate_verbose() } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index 791856b171f8..ed8d1204d111 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -671,7 +671,7 @@ impl<'tcx> GotocCtx<'tcx> { trait_ref_t: Binder<'_, TraitRef<'tcx>>, t: Ty<'tcx>, ) -> Expr { - let vtable_field_name = self.vtable_fild_name(def_id); + 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 diff --git a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs index 56ff1b1309fd..3b73a9e8fcb0 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs @@ -291,7 +291,7 @@ impl<'tcx> GotocCtx<'tcx> { // 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.vtable_fild_name(def_id); + 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 // If the original call was of the form diff --git a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs index 14e28834b3a5..8578cc191b9d 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs @@ -132,7 +132,7 @@ impl<'tcx> GotocCtx<'tcx> { let fnptr = self.codegen_dynamic_function_sig(sig).to_pointer(); // vtable field name, i.e., ::Shape::vol - let vtable_field_name = self.vtable_fild_name(def_id); + 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); From b6b761c55512eaaa84795576d9f4a6b8e0d81574 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Tue, 8 Jun 2021 20:32:33 -0400 Subject: [PATCH 07/11] Create std_lib_add_duplicate.rs --- .../cbmc/DynTrait/std_lib_add_duplicate.rs | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 src/test/cbmc/DynTrait/std_lib_add_duplicate.rs 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); +} From e5f93e13c025e1bbd01b10041bad17b272e8ea6a Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Wed, 9 Jun 2021 13:48:56 -0400 Subject: [PATCH 08/11] Add test for duplicates across crates --- src/test/cbmc/DynTrait/different_crates.rs | 51 +++++++++++++++++++ .../cbmc/DynTrait/different_crates_fail.rs | 51 +++++++++++++++++++ 2 files changed, 102 insertions(+) create mode 100644 src/test/cbmc/DynTrait/different_crates.rs create mode 100644 src/test/cbmc/DynTrait/different_crates_fail.rs diff --git a/src/test/cbmc/DynTrait/different_crates.rs b/src/test/cbmc/DynTrait/different_crates.rs new file mode 100644 index 000000000000..bf4facd73d6c --- /dev/null +++ b/src/test/cbmc/DynTrait/different_crates.rs @@ -0,0 +1,51 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +struct Counter { + count: usize, +} + +impl std::iter::Iterator for Counter { + type Item = usize; + + fn next(&mut self) -> Option { + // Increment our count. + self.count += 1; + Some(self.count) + } +} + +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..aaa37802d833 --- /dev/null +++ b/src/test/cbmc/DynTrait/different_crates_fail.rs @@ -0,0 +1,51 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +struct Counter { + count: usize, +} + +impl std::iter::Iterator for Counter { + type Item = usize; + + fn next(&mut self) -> Option { + // Increment our count. + self.count += 1; + Some(self.count) + } +} + +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 From 1acc6487d34af26a1cf433b17e1c1f825f061db2 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Wed, 9 Jun 2021 14:01:23 -0400 Subject: [PATCH 09/11] More comment documentation of choices --- compiler/rustc_codegen_llvm/src/gotoc/metadata.rs | 3 +++ compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs | 6 ++++++ src/test/cbmc/DynTrait/different_crates.rs | 4 +--- src/test/cbmc/DynTrait/different_crates_fail.rs | 4 +--- 4 files changed, 11 insertions(+), 6 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs index 041448d1a53e..8397cb7462a2 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs @@ -201,6 +201,9 @@ impl<'tcx> GotocCtx<'tcx> { /// 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() } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index ed8d1204d111..dc94f1ec2e37 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -678,6 +678,10 @@ impl<'tcx> GotocCtx<'tcx> { .lookup_field_type(&vtable_type_name, &vtable_field_name) .cloned() .unwrap(); + + // 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(), @@ -687,6 +691,8 @@ impl<'tcx> GotocCtx<'tcx> { .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() { diff --git a/src/test/cbmc/DynTrait/different_crates.rs b/src/test/cbmc/DynTrait/different_crates.rs index bf4facd73d6c..a7583c3163a8 100644 --- a/src/test/cbmc/DynTrait/different_crates.rs +++ b/src/test/cbmc/DynTrait/different_crates.rs @@ -27,9 +27,7 @@ impl Iterator for Counter { trait Combined : Iterator + std::iter::Iterator {} -impl Combined for Counter { - -} +impl Combined for Counter {} fn std_count(c : &mut dyn std::iter::Iterator) -> usize { c.next().unwrap() diff --git a/src/test/cbmc/DynTrait/different_crates_fail.rs b/src/test/cbmc/DynTrait/different_crates_fail.rs index aaa37802d833..5b2bce5c0844 100644 --- a/src/test/cbmc/DynTrait/different_crates_fail.rs +++ b/src/test/cbmc/DynTrait/different_crates_fail.rs @@ -27,9 +27,7 @@ impl Iterator for Counter { trait Combined : Iterator + std::iter::Iterator {} -impl Combined for Counter { - -} +impl Combined for Counter {} fn std_count(c : &mut dyn std::iter::Iterator) -> usize { c.next().unwrap() From 25fa389e7df2062fb7fe4c27f1d2b5f6b1095308 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Wed, 9 Jun 2021 14:26:34 -0400 Subject: [PATCH 10/11] Cleanup: remove stale mut, unused var/imports --- compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs | 4 ---- .../rustc_codegen_llvm/src/gotoc/statement.rs | 17 +++++++++-------- compiler/rustc_codegen_llvm/src/gotoc/typ.rs | 3 +-- 3 files changed, 10 insertions(+), 14 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index dc94f1ec2e37..b39b5980bb26 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -823,10 +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(); 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 3b73a9e8fcb0..186e714dd8f6 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs @@ -281,8 +281,6 @@ 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: {:?}", @@ -300,7 +298,7 @@ impl<'tcx> GotocCtx<'tcx> { // 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 @@ -308,11 +306,14 @@ impl<'tcx> GotocCtx<'tcx> { } // 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 8578cc191b9d..e8490bd6fdd6 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/typ.rs @@ -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; From 776f3e47c839d9f488675aba893ec026a7229c9b Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Wed, 9 Jun 2021 15:55:44 -0400 Subject: [PATCH 11/11] Better comments for multiple crate tests --- src/test/cbmc/DynTrait/different_crates.rs | 6 +++++- src/test/cbmc/DynTrait/different_crates_fail.rs | 6 +++++- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/src/test/cbmc/DynTrait/different_crates.rs b/src/test/cbmc/DynTrait/different_crates.rs index a7583c3163a8..a007860ea0f7 100644 --- a/src/test/cbmc/DynTrait/different_crates.rs +++ b/src/test/cbmc/DynTrait/different_crates.rs @@ -1,10 +1,14 @@ // 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; @@ -15,6 +19,7 @@ impl std::iter::Iterator for Counter { } } +// An impl for our local trait, with an indentical name to the standard library trait Iterator { fn next(&mut self) -> Option; } @@ -37,7 +42,6 @@ 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); diff --git a/src/test/cbmc/DynTrait/different_crates_fail.rs b/src/test/cbmc/DynTrait/different_crates_fail.rs index 5b2bce5c0844..ea51fddb21be 100644 --- a/src/test/cbmc/DynTrait/different_crates_fail.rs +++ b/src/test/cbmc/DynTrait/different_crates_fail.rs @@ -1,10 +1,14 @@ // 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; @@ -15,6 +19,7 @@ impl std::iter::Iterator for Counter { } } +// An impl for our local trait, with an indentical name to the standard library trait Iterator { fn next(&mut self) -> Option; } @@ -37,7 +42,6 @@ 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