Add option to restrict vtable function pointers

Cargo.lock

@@ -3342,6 +3342,25 @@ dependencies = [
 name = "rmc"
 version = "0.1.0"
 
+[[package]]
+name = "rmc-link-restrictions"
+version = "0.1.0"
+dependencies = [
+ "rmc_restrictions",
+ "rustc_data_structures",
+ "serde",
+ "serde_json",
+]
+
+[[package]]
+name = "rmc_restrictions"
+version = "0.1.0"
+dependencies = [
+ "cbmc",
+ "rustc_data_structures",
+ "serde",
+]
+
 [[package]]
 name = "rust-demangler"
 version = "0.0.1"
@@ -3884,6 +3903,7 @@ dependencies = [
  "libc",
  "measureme 9.1.2",
  "num",
+ "rmc_restrictions",
  "rustc-demangle",
  "rustc_arena",
  "rustc_ast",

Cargo.toml

@@ -5,6 +5,7 @@ members = [
   "library/std",
   "library/test",
   "library/rmc",
+  "library/rmc_restrictions",
   "src/rustdoc-json-types",
   "src/tools/cargotest",
   "src/tools/clippy",
@@ -21,6 +22,7 @@ members = [
   "src/tools/build-manifest",
   "src/tools/remote-test-client",
   "src/tools/remote-test-server",
+  "src/tools/rmc-link-restrictions",
   "src/tools/rust-installer",
   "src/tools/rust-demangler",
   "src/tools/cargo",

compiler/cbmc/src/irep/serialize.rs

@@ -98,6 +98,32 @@ impl Serialize for InternedString {
     }
 }
 
+struct InternedStringVisitor;
+
+impl<'de> serde::Deserialize<'de> for InternedString {
+    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
+    where
+        D: serde::Deserializer<'de>,
+    {
+        deserializer.deserialize_str(InternedStringVisitor)
+    }
+}
+
+impl<'de> serde::de::Visitor<'de> for InternedStringVisitor {
+    type Value = InternedString;
+
+    fn expecting(&self, formatter: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        formatter.write_str("a String like thing")
+    }
+
+    fn visit_str<E>(self, v: &str) -> Result<Self::Value, E>
+    where
+        E: serde::de::Error,
+    {
+        Ok(v.into())
+    }
+}
+
 impl Serialize for Symbol {
     fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
     where

compiler/rustc_codegen_rmc/Cargo.toml

@@ -21,6 +21,7 @@ serde = "1"
 serde_json = "1"
 snap = "1"
 tracing = "0.1"
+rmc_restrictions = { path = "../../library/rmc_restrictions" }
 rustc_middle = { path = "../rustc_middle" }
 rustc-demangle = "0.1.21"
 rustc_arena = { path = "../rustc_arena" }

compiler/rustc_codegen_rmc/src/codegen/assumptions.rs

@@ -178,7 +178,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     self.find_function(fname)
                 }
             }
-            ty::Dynamic(_, _) => unimplemented!(),
+            ty::Dynamic(_, _) => None,
             ty::Projection(_) | ty::Opaque(_, _) => {
                 let normalized = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), t);
                 self.codegen_assumption_ref_ptr(fname, t, normalized, is_ref)

compiler/rustc_codegen_rmc/src/codegen/rvalue.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::typ::{is_pointer, pointee_type, TypeExt};
 use crate::utils::{dynamic_fat_ptr, slice_fat_ptr};
-use crate::GotocCtx;
+use crate::{GotocCtx, VtableCtx};
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
 use cbmc::utils::{aggr_tag, BUG_REPORT_URL};
 use cbmc::MachineModel;
@@ -722,7 +722,17 @@ impl<'tcx> GotocCtx<'tcx> {
 
         // 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) {
+            if self.vtable_ctx.emit_vtable_restrictions {
+                // Add to the possible method names for this trait type
+                self.vtable_ctx.add_possible_method(
+                    self.normalized_trait_name(t).into(),
+                    idx,
+                    fn_name.into(),
+                );
+            }
+
             // 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.
@@ -746,13 +756,22 @@ impl<'tcx> GotocCtx<'tcx> {
         trait_ty: &'tcx ty::TyS<'tcx>,
     ) -> Expr {
         let drop_instance = Instance::resolve_drop_in_place(self.tcx, ty).polymorphize(self.tcx);
-        let drop_sym_name = self.symbol_name(drop_instance);
+        let drop_sym_name: InternedString = self.symbol_name(drop_instance).into();
 
         // The drop instance has the concrete object type, for consistency with
         // type codegen we need the trait type for the function parameter.
         let trait_fn_ty = self.trait_vtable_drop_type(trait_ty);
 
-        if let Some(drop_sym) = self.symbol_table.lookup(&drop_sym_name) {
+        if let Some(drop_sym) = self.symbol_table.lookup(drop_sym_name) {
+            if self.vtable_ctx.emit_vtable_restrictions {
+                // Add to the possible method names for this trait type
+                self.vtable_ctx.add_possible_method(
+                    self.normalized_trait_name(trait_ty).into(),
+                    VtableCtx::drop_index(),
+                    drop_sym_name,
+                );
+            }
+
             Expr::symbol_expression(drop_sym_name, drop_sym.clone().typ)
                 .address_of()
                 .cast_to(trait_fn_ty)
@@ -761,37 +780,37 @@ impl<'tcx> GotocCtx<'tcx> {
             // for it. Build and insert a function that just calls an unimplemented block
             // to maintain soundness.
             let drop_sym_name = format!("{}_unimplemented", self.symbol_name(drop_instance));
-
-            // Function body
-            let unimplemented = self
-                .codegen_unimplemented(
-                    format!("drop_in_place for {}", drop_sym_name).as_str(),
-                    Type::empty(),
+            let drop_sym = self.ensure(&drop_sym_name, |ctx, name| {
+                // Function body
+                let unimplemented = ctx
+                    .codegen_unimplemented(
+                        format!("drop_in_place for {}", drop_sym_name).as_str(),
+                        Type::empty(),
+                        Location::none(),
+                        "https://github.com/model-checking/rmc/issues/281",
+                    )
+                    .as_stmt(Location::none());
+
+                // Declare symbol for the single, self parameter
+                let param_name = format!("{}::1::var{:?}", drop_sym_name, 0);
+                let param_sym = Symbol::variable(
+                    param_name.clone(),
+                    param_name,
+                    ctx.codegen_ty(trait_ty).to_pointer(),
+                    Location::none(),
+                );
+                ctx.symbol_table.insert(param_sym.clone());
+
+                // Build and insert the function itself
+                Symbol::function(
+                    name,
+                    Type::code(vec![param_sym.to_function_parameter()], Type::empty()),
+                    Some(Stmt::block(vec![unimplemented], Location::none())),
+                    NO_PRETTY_NAME,
                     Location::none(),
-                    "https://github.com/model-checking/rmc/issues/281",
                 )
-                .as_stmt(Location::none());
-
-            // Declare symbol for the single, self parameter
-            let param_name = format!("{}::1::var{:?}", drop_sym_name, 0);
-            let param_sym = Symbol::variable(
-                param_name.clone(),
-                param_name,
-                self.codegen_ty(trait_ty).to_pointer(),
-                Location::none(),
-            );
-            self.symbol_table.insert(param_sym.clone());
-
-            // Build and insert the function itself
-            let sym = Symbol::function(
-                &drop_sym_name,
-                Type::code(vec![param_sym.to_function_parameter()], Type::empty()),
-                Some(Stmt::block(vec![unimplemented], Location::none())),
-                NO_PRETTY_NAME,
-                Location::none(),
-            );
-            self.symbol_table.insert(sym.clone());
-            Expr::symbol_expression(drop_sym_name, sym.typ).address_of().cast_to(trait_fn_ty)
+            });
+            drop_sym.to_expr().address_of().cast_to(trait_fn_ty)
         }
     }
 

compiler/rustc_codegen_rmc/src/codegen/statement.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::typ::TypeExt;
 use super::typ::FN_RETURN_VOID_VAR_NAME;
-use crate::GotocCtx;
+use crate::{GotocCtx, VtableCtx};
 use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir;
@@ -143,8 +143,17 @@ impl<'tcx> GotocCtx<'tcx> {
                             let self_ref =
                                 self_ref.cast_to(trait_fat_ptr.typ().clone().to_pointer());
 
-                            let func_exp: Expr = fn_ptr.dereference();
-                            func_exp.call(vec![self_ref]).as_stmt(Location::none())
+                            let call = if self.vtable_ctx.emit_vtable_restrictions {
+                                self.virtual_call_with_restricted_fn_ptr(
+                                    trait_fat_ptr.typ().clone(),
+                                    VtableCtx::drop_index(),
+                                    fn_ptr,
+                                    vec![self_ref],
+                                )
+                            } else {
+                                fn_ptr.dereference().call(vec![self_ref])
+                            };
+                            call.as_stmt(Location::none())
                         }
                         _ => {
                             // Non-virtual, direct drop call
@@ -449,12 +458,17 @@ impl<'tcx> GotocCtx<'tcx> {
         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![
-            assert_nonnull,
-            self.codegen_expr_to_place(place, func_exp.call(fargs.to_vec()))
-                .with_location(loc.clone()),
-        ]
+        let call = if self.vtable_ctx.emit_vtable_restrictions {
+            self.virtual_call_with_restricted_fn_ptr(
+                trait_fat_ptr.typ().clone(),
+                idx,
+                fn_ptr,
+                fargs.to_vec(),
+            )
+        } else {
+            fn_ptr.dereference().call(fargs.to_vec())
+        };
+        vec![assert_nonnull, self.codegen_expr_to_place(place, call).with_location(loc.clone())]
     }
 
     /// A place is similar to the C idea of a LHS. For example, the returned value of a function call is stored to a place.

compiler/rustc_codegen_rmc/src/codegen/typ.rs

@@ -486,8 +486,8 @@ impl<'tcx> GotocCtx<'tcx> {
     pub fn codegen_ty(&mut self, ty: Ty<'tcx>) -> Type {
         let goto_typ = self.codegen_ty_inner(ty);
         if let Some(tag) = goto_typ.tag() {
-            if !self.type_map.contains_key(&tag.to_string()) {
-                self.type_map.insert(tag.to_string(), ty);
+            if !self.type_map.contains_key(&tag) {
+                self.type_map.insert(tag, ty);
             }
         }
         goto_typ

compiler/rustc_codegen_rmc/src/compiler_interface.rs

@@ -8,6 +8,8 @@ use crate::GotocCtx;
 use bitflags::_core::any::Any;
 use cbmc::goto_program::symtab_transformer;
 use cbmc::goto_program::SymbolTable;
+use cbmc::InternedString;
+use rmc_restrictions::VtableCtxResults;
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_errors::ErrorReported;
@@ -27,9 +29,10 @@ use tracing::{debug, warn};
 
 // #[derive(RustcEncodable, RustcDecodable)]
 pub struct GotocCodegenResult {
-    pub type_map: BTreeMap<String, String>,
+    pub type_map: BTreeMap<InternedString, InternedString>,
     pub symtab: SymbolTable,
     pub crate_name: rustc_span::Symbol,
+    pub vtable_restrictions: Option<VtableCtxResults>,
 }
 
 #[derive(Clone)]
@@ -130,12 +133,22 @@ impl CodegenBackend for GotocCodegenBackend {
             &tcx.sess.opts.debugging_opts.symbol_table_passes,
         );
 
-        let type_map = BTreeMap::from_iter(c.type_map.into_iter().map(|(k, v)| (k, v.to_string())));
+        // Map MIR types to GotoC types
+        let type_map =
+            BTreeMap::from_iter(c.type_map.into_iter().map(|(k, v)| (k, v.to_string().into())));
+
+        // Get the vtable function pointer restrictions if requested
+        let vtable_restrictions = if c.vtable_ctx.emit_vtable_restrictions {
+            Some(c.vtable_ctx.get_virtual_function_restrictions())
+        } else {
+            None
+        };
 
         Box::new(GotocCodegenResult {
             type_map,
             symtab: symbol_table,
             crate_name: tcx.crate_name(LOCAL_CRATE) as rustc_span::Symbol,
+            vtable_restrictions: vtable_restrictions,
         })
     }
 
@@ -163,6 +176,11 @@ impl CodegenBackend for GotocCodegenBackend {
             let base_filename = outputs.path(OutputType::Object);
             write_file(&base_filename, "symtab.json", &result.symtab);
             write_file(&base_filename, "type_map.json", &result.type_map);
+
+            // If they exist, write out vtable virtual call function pointer restrictions
+            if let Some(restrictions) = result.vtable_restrictions {
+                write_file(&base_filename, "restrictions.json", &restrictions);
+            }
         }
 
         Ok(())

compiler/rustc_codegen_rmc/src/context/current_fn.rs

@@ -9,6 +9,7 @@ use rustc_middle::ty::Instance;
 use rustc_middle::ty::PolyFnSig;
 
 /// This structure represents useful data about the function we are currently compiling.
+#[derive(Debug)]
 pub struct CurrentFnCtx<'tcx> {
     /// The GOTO block we are compiling into
     block: Vec<Stmt>,

compiler/rustc_codegen_rmc/src/context/goto_ctx.rs

@@ -14,6 +14,7 @@
 //! Any MIR specific functionality (e.g. codegen etc) should live in specialized files that use
 //! this structure as input.
 use super::current_fn::CurrentFnCtx;
+use super::vtable_ctx::VtableCtx;
 use crate::overrides::{fn_hooks, GotocHooks};
 use crate::utils::full_crate_name;
 use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type};
@@ -48,8 +49,10 @@ pub struct GotocCtx<'tcx> {
     pub global_var_count: u64,
     /// map a global allocation to a name in the symbol table
     pub alloc_map: FxHashMap<&'tcx Allocation, String>,
+    /// map (trait, method) pairs to possible implementations
+    pub vtable_ctx: VtableCtx,
     pub current_fn: Option<CurrentFnCtx<'tcx>>,
-    pub type_map: FxHashMap<String, Ty<'tcx>>,
+    pub type_map: FxHashMap<InternedString, Ty<'tcx>>,
 }
 
 /// Constructor
@@ -58,13 +61,15 @@ impl<'tcx> GotocCtx<'tcx> {
         let fhks = fn_hooks();
         let mm = machine_model_from_session(tcx.sess);
         let symbol_table = SymbolTable::new(mm);
+        let emit_vtable_restrictions = tcx.sess.opts.debugging_opts.emit_vtable_restrictions;
         GotocCtx {
             tcx,
             symbol_table,
             hooks: fhks,
             full_crate_name: full_crate_name(tcx),
             global_var_count: 0,
             alloc_map: FxHashMap::default(),
+            vtable_ctx: VtableCtx::new(emit_vtable_restrictions),
             current_fn: None,
             type_map: FxHashMap::default(),
         }

compiler/rustc_codegen_rmc/src/context/mod.rs

@@ -8,5 +8,7 @@
 
 mod current_fn;
 mod goto_ctx;
+mod vtable_ctx;
 
 pub use goto_ctx::GotocCtx;
+pub use vtable_ctx::VtableCtx;