From c1e9ba57ccb3367a37732b922e94d42be6c766dc Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Thu, 10 Jun 2021 22:24:03 -0400 Subject: [PATCH] Remove slow find_by_pretty_name vtable search (#193) * Replace slower lookup by pretty name with symbol name * Add nonnull fn call assertion (with new utility fn) * Kill pretty_name_from_instance * Remove fixme from boxmuttrait test that now works * Pipe pretty_name through Symbol::function constructor * Don't pass non-specific pretty names --- .../src/gotoc/assumptions.rs | 9 ++-- .../src/gotoc/cbmc/goto_program/expr.rs | 7 +++ .../src/gotoc/cbmc/goto_program/symbol.rs | 12 +++-- .../gotoc/cbmc/goto_program/symbol_table.rs | 13 ------ .../rustc_codegen_llvm/src/gotoc/hooks.rs | 1 + .../rustc_codegen_llvm/src/gotoc/metadata.rs | 31 +++++-------- compiler/rustc_codegen_llvm/src/gotoc/mod.rs | 9 +++- .../rustc_codegen_llvm/src/gotoc/operand.rs | 13 +++++- .../rustc_codegen_llvm/src/gotoc/rvalue.rs | 42 +++++++----------- .../rustc_codegen_llvm/src/gotoc/statement.rs | 44 +++++++++++++------ ...oxmuttrait_fail.rs => boxmuttrait_fail.rs} | 0 11 files changed, 97 insertions(+), 84 deletions(-) rename src/test/cbmc/FatPointers/{fixme_boxmuttrait_fail.rs => boxmuttrait_fail.rs} (100%) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs b/compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs index c4001d3ede81a..759a716c6d982 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/assumptions.rs @@ -215,7 +215,7 @@ impl<'tcx> GotocCtx<'tcx> { let len = sl.member("len", &tcx.symbol_table); let mut invariants = vec![]; if is_ref { - invariants.push(data.clone().neq(data.typ().null())); + invariants.push(data.clone().is_nonnull()); } if let Some(f) = f { //CHECKME: why is this 2? @@ -224,7 +224,7 @@ impl<'tcx> GotocCtx<'tcx> { let lbody = Stmt::block( vec![ data.clone() - .neq(data.typ().null()) + .is_nonnull() .implies(f.call(vec![data.plus(idx.clone())])) .not() .if_then_else( @@ -262,10 +262,10 @@ impl<'tcx> GotocCtx<'tcx> { let x = ptr.dereference(); let mut invarints = vec![]; if is_ref { - invarints.push(x.clone().neq(x.typ().null())); + invarints.push(x.clone().is_nonnull()); } if let Some(f) = f { - invarints.push(x.clone().neq(x.typ().null()).implies(f.call(vec![x]))); + invarints.push(x.clone().is_nonnull().implies(f.call(vec![x]))); } body.push(fold_invariants(invarints).ret(Location::none())); }) @@ -586,6 +586,7 @@ impl<'tcx> GotocCtx<'tcx> { fname, Type::code(vec![var.to_function_parameter()], Type::bool()), Some(body), + None, Location::none(), ) } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs index fc3b8760b6586..645c29afef8e3 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs @@ -1105,6 +1105,13 @@ impl Expr { self.lt(typ.zero()) } + /// `self != NULL` + pub fn is_nonnull(self) -> Self { + assert!(self.typ.is_pointer()); + let nullptr = self.typ().null(); + self.neq(nullptr) + } + /// `ArithmeticOverflowResult r; >>>r.overflowed = builtin_add_overflow(self, e, &r.result)<<<` pub fn add_overflow(self, e: Expr) -> ArithmeticOverflowResult { let result = self.clone().plus(e.clone()); diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symbol.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symbol.rs index 47ba3c226a1c2..0957a7dcebeef 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symbol.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symbol.rs @@ -113,6 +113,7 @@ impl Symbol { name, Type::code_with_unnamed_parameters(param_types, return_type), None, + None, Location::builtin_function(name, None), ) } @@ -135,15 +136,20 @@ impl Symbol { .with_is_static_lifetime(true) //TODO with thread local was also true?? } - pub fn function(name: &str, typ: Type, body: Option, loc: Location) -> Symbol { - // TODO should take pretty name + pub fn function( + name: &str, + typ: Type, + body: Option, + pretty_name: Option, + loc: Location, + ) -> Symbol { Symbol::new( name.to_string(), loc, typ, body.map_or(SymbolValues::None, |x| SymbolValues::Stmt(x)), Some(name.to_string()), - None, + pretty_name, ) .with_is_lvalue(true) } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symbol_table.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symbol_table.rs index 4c8556ef4678a..974ba137221a2 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symbol_table.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symbol_table.rs @@ -76,19 +76,6 @@ impl SymbolTable { self.symbol_table.contains_key(name) } - //TODO DSN - // https://github.com/model-checking/rmc/issues/4 - // This is SUPER DUMB AND SLOW. We should just keep a second map. But for now, this is good enough - pub fn find_by_pretty_name(&self, pretty_name: &str) -> Vec<&Symbol> { - let mut rval = Vec::new(); - for (_name, symbol) in &self.symbol_table { - if symbol.pretty_name.as_ref().map_or(false, |x| x == pretty_name) { - rval.push(symbol); - } - } - rval - } - pub fn iter(&self) -> std::collections::btree_map::Iter<'_, String, Symbol> { self.symbol_table.iter() } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs b/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs index e94321388cf0b..fa08872ddfe4f 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs @@ -328,6 +328,7 @@ impl<'tcx> GotocHook<'tcx> for MemSwap { Type::empty(), ), Some(Stmt::block(block, loc.clone())), + None, Location::none(), ) }); diff --git a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs index 8397cb7462a2e..b9a94b4b99774 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/metadata.rs @@ -182,24 +182,11 @@ 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/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!( - "{}::{}", - self.tcx.crate_name(instance.def_id().krate), - with_no_trimmed_paths(|| instance.to_string()) - ) - } - /// 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. + /// which does need more crate/type information and uses the full symbol_name(...) 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. @@ -207,27 +194,28 @@ impl<'tcx> GotocCtx<'tcx> { 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 { + /// A human readable name in Rust for reference, should not be used as a key. + pub fn readable_instance_name(&self, instance: Instance<'tcx>) -> String { with_no_trimmed_paths(|| self.tcx.def_path_str(instance.def_id())) } - /// the actual function name used in the symbol table + /// The actual function name used in the symbol table pub fn symbol_name(&self, instance: Instance<'tcx>) -> String { let llvm_mangled = self.tcx.symbol_name(instance).name.to_string(); debug!( "finding function name for instance: {}, debug: {:?}, name: {}, symbol: {}, demangle: {}", instance, instance, - self.instance_name(instance), + self.readable_instance_name(instance), llvm_mangled, rustc_demangle::demangle(&llvm_mangled).to_string() ); - let pretty = self.pretty_name_from_instance(instance); + let pretty = self.readable_instance_name(instance); - // make main function a special case for easy CBMC entry - if pretty.ends_with("::main") { + // Make main function a special case for easy CBMC entry + // TODO: probably need to edit for https://github.com/model-checking/rmc/issues/169 + if pretty == "main" { "main".to_string() } else { // TODO: llvm mangled string is not very readable. one way to tackle this is to @@ -460,6 +448,7 @@ impl<'tcx> GotocCtx<'tcx> { &fn_name, Type::code(vec![], Type::constructor()), Some(Stmt::block(vec![body], Location::none())), //TODO is this block needed? + None, Location::none(), ) .with_is_file_local(true) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mod.rs b/compiler/rustc_codegen_llvm/src/gotoc/mod.rs index a2c5478c764d1..c69db57ef5b4c 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mod.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mod.rs @@ -165,8 +165,13 @@ impl<'tcx> GotocCtx<'tcx> { self.set_current_fn(instance); 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_from_instance(instance)) + Symbol::function( + fname, + ctx.fn_typ(), + None, + Some(ctx.readable_instance_name(instance)), + ctx.codegen_span2(&mir.span), + ) }); self.reset_current_fn(); } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/operand.rs b/compiler/rustc_codegen_llvm/src/gotoc/operand.rs index 60d99481412ee..17143dbaf9dcf 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/operand.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/operand.rs @@ -282,6 +282,7 @@ impl<'tcx> GotocCtx<'tcx> { &func_name, Type::code(vec![param.to_function_parameter()], cgt), Some(Stmt::block(body, Location::none())), + None, Location::none(), ) }); @@ -538,6 +539,7 @@ impl<'tcx> GotocCtx<'tcx> { &fname, Type::code(vec![param.to_function_parameter()], cgt), Some(Stmt::block(body, Location::none())), + None, Location::none(), ) }); @@ -548,8 +550,15 @@ impl<'tcx> GotocCtx<'tcx> { let func = self.symbol_name(instance); let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance)); // make sure the functions imported from other modules are in the symbol table - self.ensure(&func, |_, _| { - Symbol::function(&func, funct.clone(), None, Location::none()).with_is_extern(true) + self.ensure(&func, |ctx, _| { + Symbol::function( + &func, + funct.clone(), + None, + Some(ctx.readable_instance_name(instance)), + Location::none(), + ) + .with_is_extern(true) }); Expr::symbol_expression(func, funct).with_location(self.codegen_span_option2(span.cloned())) } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs index b39b5980bb26b..8e94a0ed03f89 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/rvalue.rs @@ -203,6 +203,7 @@ impl<'tcx> GotocCtx<'tcx> { &func_name, Type::code(vec![inp.to_function_parameter()], res_t), Some(Stmt::block(body, Location::none())), + None, Location::none(), ) }); @@ -691,31 +692,22 @@ 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() { - 0 => { - warn!( - "Unable to find vtable symbol for {}. Using NULL instead", - &pretty_function_name - ); - field_type.null() - } - 1 => { - let fn_symbol = matching_symbols[0]; - // create a pointer to the method - // Note that the method takes a self* as the first argument, but the vtable field type has a void* as the first arg. - // So we need to cast it at the end. - Expr::symbol_expression(fn_symbol.name.clone(), fn_symbol.typ.clone()) - .address_of() - .cast_to(field_type) - } - _ => unreachable!( - "Too many options when trying to build vtable for {} {:?}", - pretty_function_name, matching_symbols - ), + // Lookup in the symbol table using the full symbol table name/key + let fn_name = self.symbol_name(instance); + if let Some(fn_symbol) = self.symbol_table.lookup(&fn_name) { + // Create a pointer to the method + // Note that the method takes a self* as the first argument, but the vtable field type has a void* as the first arg. + // So we need to cast it at the end. + Expr::symbol_expression(fn_symbol.name.clone(), fn_symbol.typ.clone()) + .address_of() + .cast_to(field_type) + } else { + warn!( + "Unable to find vtable symbol for virtual function {}, attempted lookup for symbol name: {}", + self.readable_instance_name(instance), + fn_name, + ); + field_type.null() } } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs index 186e714dd8f61..732243afb6c9b 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/statement.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/statement.rs @@ -278,10 +278,8 @@ impl<'tcx> GotocCtx<'tcx> { return Stmt::goto(self.find_label(&target), Location::none()); } - // 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); - if let InstanceDef::Virtual(def_id, size) = instance.def { + // Handle the case of a virtual function call via vtable lookup. + let mut stmts = if let InstanceDef::Virtual(def_id, size) = instance.def { debug!( "Codegen a call through a virtual function. def_id: {:?} size: {:?}", def_id, size @@ -299,21 +297,39 @@ impl<'tcx> GotocCtx<'tcx> { let vtable_ref = trait_fat_ptr.to_owned().member("vtable", &self.symbol_table); let vtable = vtable_ref.dereference(); let fn_ptr = vtable.member(&vtable_field_name, &self.symbol_table); - funce = fn_ptr.dereference(); - //Update the argument from arg0 to arg0.data + // Update the argument from arg0 to arg0.data fargs[0] = trait_fat_ptr.to_owned().member("data", &self.symbol_table); - } - // Actually generate the function call, and store the return value, if any. - Stmt::block( + // For soundness, add an assertion that the vtable function call is not null. + // Otherwise, CBMC might treat this as an assert(0) and later user-added assertions + // could be vacuously true. + let call_is_nonnull = fn_ptr.clone().is_nonnull(); + let assert_msg = + format!("Non-null virtual function call for {:?}", vtable_field_name); + let assert_nonnull = Stmt::assert(call_is_nonnull, &assert_msg, loc.clone()); + + // Virtual function call and corresponding nonnull assertion. + let func_exp: Expr = fn_ptr.dereference(); vec![ - self.codegen_expr_to_place(&p, funce.call(fargs)) + assert_nonnull, + self.codegen_expr_to_place(&p, func_exp.call(fargs)) .with_location(loc.clone()), - Stmt::goto(self.find_label(&target), loc.clone()), - ], - loc, - ) + ] + } else { + // Non-virtual function call. + let func_exp = self.codegen_operand(func); + vec![ + self.codegen_expr_to_place(&p, func_exp.call(fargs)) + .with_location(loc.clone()), + ] + }; + + // Add return jump. + stmts.push(Stmt::goto(self.find_label(&target), loc.clone())); + + // Produce the full function call block. + Stmt::block(stmts, loc) } ty::FnPtr(_) => { let (p, target) = destination.unwrap(); diff --git a/src/test/cbmc/FatPointers/fixme_boxmuttrait_fail.rs b/src/test/cbmc/FatPointers/boxmuttrait_fail.rs similarity index 100% rename from src/test/cbmc/FatPointers/fixme_boxmuttrait_fail.rs rename to src/test/cbmc/FatPointers/boxmuttrait_fail.rs