Remove slow find_by_pretty_name vtable search

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(),
         )
     }

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());

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<Stmt>, loc: Location) -> Symbol {
-        // TODO should take pretty name
+    pub fn function(
+        name: &str,
+        typ: Type,
+        body: Option<Stmt>,
+        pretty_name: Option<String>,
+        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)
     }

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()
     }

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(),
             )
         });

compiler/rustc_codegen_llvm/src/gotoc/metadata.rs

@@ -182,52 +182,40 @@ 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::<Concrete as Trait>::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.
         // 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
-    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)

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();
     }

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()))
     }

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); //("<path>::<Rectangle as Vol>::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()
         }
     }
 

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();