From 30895d2d4d3f5ddf8c72b423d22e32b089fc2b64 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Thu, 3 Jun 2021 16:50:41 -0400 Subject: [PATCH 1/3] Refactor pretty name to restore passable dyn trait functionality --- .../rustc_codegen_llvm/src/gotoc/metadata.rs | 38 +++++++++++++++---- compiler/rustc_codegen_llvm/src/gotoc/mod.rs | 2 +- .../rustc_codegen_llvm/src/gotoc/rvalue.rs | 5 +-- .../{fixme_main_fail.rs => main_fail.rs} | 0 ...ixme_boxtrait_fail.rs => boxtrait_fail.rs} | 0 .../{fixme_trait1_fail.rs => trait1_fail.rs} | 0 .../{fixme_trait2_fail.rs => trait2_fail.rs} | 0 .../{fixme_trait3_fail.rs => trait3_fail.rs} | 0 8 files changed, 34 insertions(+), 11 deletions(-) rename rust-tests/cbmc-reg/DynTrait/{fixme_main_fail.rs => main_fail.rs} (100%) rename rust-tests/cbmc-reg/FatPointers/{fixme_boxtrait_fail.rs => boxtrait_fail.rs} (100%) rename rust-tests/cbmc-reg/FatPointers/{fixme_trait1_fail.rs => trait1_fail.rs} (100%) rename rust-tests/cbmc-reg/FatPointers/{fixme_trait2_fail.rs => trait2_fail.rs} (100%) rename rust-tests/cbmc-reg/FatPointers/{fixme_trait3_fail.rs => trait3_fail.rs} (100%) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs index 22955a3f2237..b0b8c3def4dc 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, Instance, Ty, TyCtxt, TypeFoldable}; +use rustc_middle::ty::{self, Binder, Instance, TraitRef, Ty, TyCtxt, TypeFoldable}; use rustc_target::abi::{HasDataLayout, LayoutOf, TargetDataLayout}; use rustc_target::spec::Target; use std::iter; @@ -186,10 +186,34 @@ impl<'tcx> GotocCtx<'tcx> { self.current_fn.as_ref().map(|x| self.symbol_name(x.instance)) } - /// a path to the def id. the difference from [instance_name] is that it does not consider generics. - pub fn pretty_name(&self, did: DefId) -> String { - let def_path = self.tcx.def_path(did); - format!("{}{}", self.tcx.crate_name(did.krate), def_path.to_string_no_crate_verbose()) + // 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. + pub fn pretty_name_from_instance(&self, instance: Instance<'tcx>) -> String { + format!( + "{}::{}", + self.tcx.crate_name(instance.def_id().krate), + with_no_trimmed_paths(|| instance.to_string()) + ) + } + + // 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) + ) } /// a human readable name in rust for reference @@ -208,8 +232,8 @@ impl<'tcx> GotocCtx<'tcx> { llvm_mangled, rustc_demangle::demangle(&llvm_mangled).to_string() ); - let did = instance.def.def_id(); - let pretty = self.pretty_name(did); + + let pretty = self.pretty_name_from_instance(instance); // make main function a special case for easy CBMC entry if pretty.ends_with("::main") { diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mod.rs b/compiler/rustc_codegen_llvm/src/gotoc/mod.rs index 62859df6f68a..a2c5478c764d 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mod.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mod.rs @@ -166,7 +166,7 @@ impl<'tcx> GotocCtx<'tcx> { self.ensure(&self.fname(), |ctx, fname| { let mir = ctx.mir(); Symbol::function(fname, ctx.fn_typ(), None, ctx.codegen_span2(&mir.span)) - .with_pretty_name(&ctx.pretty_name(instance.def_id())) + .with_pretty_name(&ctx.pretty_name_from_instance(instance)) }); self.reset_current_fn(); } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index 358f57aef75d..b06ef4dc3401 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -680,9 +680,8 @@ impl<'tcx> GotocCtx<'tcx> { .unwrap(); // TODO: this name lookup does not work with rust-tests/cbmc-reg/DynTrait/main.rs - let normalized_object_type_name = self.normalized_name_of_dynamic_object_type(trait_ref_t); - let pretty_function_name = format!("{}::{}", normalized_object_type_name, function_name); - let matching_symbols = self.symbol_table.find_by_pretty_name(&pretty_function_name); //("::vol"); + let pretty_function_name = self.pretty_name_from_dynamic_object(def_id, trait_ref_t); + let matching_symbols = self.symbol_table.find_by_pretty_name(&pretty_function_name); //("::::vol"); match matching_symbols.len() { 0 => { warn!( diff --git a/rust-tests/cbmc-reg/DynTrait/fixme_main_fail.rs b/rust-tests/cbmc-reg/DynTrait/main_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/DynTrait/fixme_main_fail.rs rename to rust-tests/cbmc-reg/DynTrait/main_fail.rs diff --git a/rust-tests/cbmc-reg/FatPointers/fixme_boxtrait_fail.rs b/rust-tests/cbmc-reg/FatPointers/boxtrait_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/fixme_boxtrait_fail.rs rename to rust-tests/cbmc-reg/FatPointers/boxtrait_fail.rs diff --git a/rust-tests/cbmc-reg/FatPointers/fixme_trait1_fail.rs b/rust-tests/cbmc-reg/FatPointers/trait1_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/fixme_trait1_fail.rs rename to rust-tests/cbmc-reg/FatPointers/trait1_fail.rs diff --git a/rust-tests/cbmc-reg/FatPointers/fixme_trait2_fail.rs b/rust-tests/cbmc-reg/FatPointers/trait2_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/fixme_trait2_fail.rs rename to rust-tests/cbmc-reg/FatPointers/trait2_fail.rs diff --git a/rust-tests/cbmc-reg/FatPointers/fixme_trait3_fail.rs b/rust-tests/cbmc-reg/FatPointers/trait3_fail.rs similarity index 100% rename from rust-tests/cbmc-reg/FatPointers/fixme_trait3_fail.rs rename to rust-tests/cbmc-reg/FatPointers/trait3_fail.rs From e7e357c3292c7d35581e28117f84cc4ea68e7199 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Thu, 3 Jun 2021 18:19:12 -0400 Subject: [PATCH 2/3] Doc comments, remove stale TODO --- .../rustc_codegen_llvm/src/gotoc/metadata.rs | 16 ++++++++-------- compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs | 1 - 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs index b0b8c3def4dc..0fdbb4593d7d 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs @@ -186,10 +186,10 @@ impl<'tcx> GotocCtx<'tcx> { self.current_fn.as_ref().map(|x| self.symbol_name(x.instance)) } - // 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. + /// 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. pub fn pretty_name_from_instance(&self, instance: Instance<'tcx>) -> String { format!( "{}::{}", @@ -198,10 +198,10 @@ 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. + /// 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, diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index b06ef4dc3401..497fd5c69886 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -679,7 +679,6 @@ impl<'tcx> GotocCtx<'tcx> { .cloned() .unwrap(); - // TODO: this name lookup does not work with rust-tests/cbmc-reg/DynTrait/main.rs let pretty_function_name = self.pretty_name_from_dynamic_object(def_id, trait_ref_t); let matching_symbols = self.symbol_table.find_by_pretty_name(&pretty_function_name); //("::::vol"); match matching_symbols.len() { From 58a5f677449c1b7075c50857294c4616851befab Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Fri, 4 Jun 2021 08:34:13 -0400 Subject: [PATCH 3/3] Add unit testing issue --- compiler/rustc_codegen_llvm/src/gotoc/metadata.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs index 0fdbb4593d7d..be3dea1c103a 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs @@ -190,6 +190,7 @@ impl<'tcx> GotocCtx<'tcx> { /// boxtrait_fail::::increment /// Generated from the fn instance to insert _into_ the symbol table. /// Must match the format of pretty_name_from_dynamic_object. + /// TODO: internal unit tests https://github.com/model-checking/rmc/issues/172 pub fn pretty_name_from_instance(&self, instance: Instance<'tcx>) -> String { format!( "{}::{}",