Switch --restrict-vtable to use CBMC labels instead of wrapper functions (rust-lang#767)

tedinski · avanhatt · tedinski · commit eca2c52e2b8e · 2022-03-04T11:07:40.000-06:00
Co-authored-by: Alexa VanHattum &lt;amv94@cornell.edu&gt;
diff --git a/library/kani_restrictions/src/lib.rs b/library/kani_restrictions/src/lib.rs
@@ -19,6 +19,7 @@ pub struct TraitDefinedMethod {
 pub struct CallSite {
     pub trait_method: TraitDefinedMethod,
     pub function_name: InternedString,
+    pub label: InternedString,
 }
 
 #[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]
diff --git a/src/kani-compiler/rustc_codegen_kani/src/codegen/statement.rs b/src/kani-compiler/rustc_codegen_kani/src/codegen/statement.rs
@@ -139,17 +139,17 @@ impl<'tcx> GotocCtx<'tcx> {
                             let self_ref =
                                 self_ref.cast_to(trait_fat_ptr.typ().clone().to_pointer());
 
-                            let call = if self.vtable_ctx.emit_vtable_restrictions {
+                            let call =
+                                fn_ptr.dereference().call(vec![self_ref]).as_stmt(Location::none());
+                            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],
+                                    call,
                                 )
                             } else {
-                                fn_ptr.dereference().call(vec![self_ref])
-                            };
-                            call.as_stmt(Location::none())
+                                call
+                            }
                         }
                         _ => {
                             // Non-virtual, direct drop call
@@ -436,17 +436,14 @@ impl<'tcx> GotocCtx<'tcx> {
         let assert_nonnull = Stmt::assert(call_is_nonnull, &assert_msg, loc.clone());
 
         // Virtual function call and corresponding nonnull assertion.
-        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(),
-            )
+        let call = fn_ptr.dereference().call(fargs.to_vec());
+        let call_stmt = self.codegen_expr_to_place(place, call).with_location(loc.clone());
+        let call_stmt = if self.vtable_ctx.emit_vtable_restrictions {
+            self.virtual_call_with_restricted_fn_ptr(trait_fat_ptr.typ().clone(), idx, call_stmt)
         } else {
-            fn_ptr.dereference().call(fargs.to_vec())
+            call_stmt
         };
-        vec![assert_nonnull, self.codegen_expr_to_place(place, call).with_location(loc.clone())]
+        vec![assert_nonnull, call_stmt]
     }
 
     /// 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.
diff --git a/src/kani-compiler/rustc_codegen_kani/src/context/vtable_ctx.rs b/src/kani-compiler/rustc_codegen_kani/src/context/vtable_ctx.rs
@@ -16,9 +16,8 @@
 /// For the current CBMC implementation of function restrictions, see:
 ///     http://cprover.diffblue.com/md__home_travis_build_diffblue_cbmc_doc_architectural_restrict-function-pointer.html
 use crate::GotocCtx;
-use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type};
+use cbmc::goto_program::{Stmt, Type};
 use cbmc::InternedString;
-use cbmc::NO_PRETTY_NAME;
 use kani_restrictions::{CallSite, PossibleMethodEntry, TraitDefinedMethod, VtableCtxResults};
 use rustc_data_structures::stable_map::FxHashMap;
 use tracing::debug;
@@ -92,98 +91,44 @@ impl VtableCtx {
         trait_name: InternedString,
         method: usize,
         function_name: InternedString,
+        label: InternedString,
     ) {
         assert!(self.emit_vtable_restrictions);
         let site = CallSite {
             trait_method: TraitDefinedMethod { trait_name, vtable_idx: method },
             function_name: function_name,
+            label: label,
         };
         self.call_sites.push(site);
     }
 }
 
 impl<'tcx> GotocCtx<'tcx> {
-    /// Wrap a virtual call through a function pointer and restrict the
-    /// possible targets.
-    ///
-    /// We need to wrap because for the current implemention, CBMC employs
-    /// a hard-to-get-right naming scheme for restrictions: the call site is
-    /// named for its index in  a given function. We don't have a good way to
-    /// track _all_ function pointers within the function, so wrapping the call
-    /// to a function that makes a single virtual function pointer call makes
-    /// the naming unambiguous.
-    ///
-    /// This can be simplified if CBMC implemented label-based restrictions.
-    /// Kani tracking: https://github.com/model-checking/kani/issues/651
-    /// CBMC tracking: https://github.com/diffblue/cbmc/issues/6464
+    /// Create a label to the virtual call site
     pub fn virtual_call_with_restricted_fn_ptr(
         &mut self,
         trait_ty: Type,
         vtable_idx: usize,
-        fn_ptr: Expr,
-        args: Vec<Expr>,
-    ) -> Expr {
+        body: Stmt,
+    ) -> Stmt {
         assert!(self.vtable_ctx.emit_vtable_restrictions);
 
-        // Crate-based naming scheme for wrappers
-        let full_crate_name = self.full_crate_name().to_string().replace("::", "_");
-        let wrapper_name: InternedString = format!(
-            "restricted_call_{}_{}",
-            full_crate_name,
-            self.vtable_ctx.get_call_site_global_idx()
-        )
-        .into();
+        let label: InternedString =
+            format!("restricted_call_label_{}", self.vtable_ctx.get_call_site_global_idx()).into();
 
         // We only have the Gotoc type, we need to normalize to match the MIR type.
         assert!(trait_ty.is_struct_tag());
         let mir_name =
             self.normalized_trait_name(*self.type_map.get(&trait_ty.tag().unwrap()).unwrap());
-        self.vtable_ctx.add_call_site(mir_name.into(), vtable_idx, wrapper_name);
-
-        // Declare the wrapper's parameters
-        let func_exp: Expr = fn_ptr.dereference();
-        let fn_type = func_exp.typ().clone();
-        let parameters: Vec<Symbol> = fn_type
-            .parameters()
-            .unwrap()
-            .iter()
-            .enumerate()
-            .map(|(i, parameter)| {
-                let name = format!("{}_{}", wrapper_name, i);
-                let param =
-                    Symbol::variable(name.clone(), name, parameter.typ().clone(), Location::none());
-                self.symbol_table.insert(param.clone());
-                param
-            })
-            .collect();
-
-        // Finish constructing the wrapper type
-        let ret_typ = fn_type.return_type().unwrap().clone();
-        let param_typs = parameters.clone().iter().map(|p| p.to_function_parameter()).collect();
-        let new_typ = if fn_type.is_code() {
-            Type::code(param_typs, ret_typ.clone())
-        } else if fn_type.is_variadic_code() {
-            Type::variadic_code(param_typs, ret_typ.clone())
-        } else {
-            unreachable!("Function type must be Code or VariadicCode")
-        };
 
-        // Build the body: call the original function pointer
-        let body = func_exp
-            .clone()
-            .call(parameters.iter().map(|p| p.to_expr()).collect())
-            .ret(Location::none());
-
-        // Build and insert the wrapper function itself
-        let sym = Symbol::function(
-            wrapper_name,
-            new_typ,
-            Some(Stmt::block(vec![body], Location::none())),
-            NO_PRETTY_NAME,
-            Location::none(),
+        // Label
+        self.vtable_ctx.add_call_site(
+            mir_name.into(),
+            vtable_idx,
+            self.current_fn().name().into(),
+            label,
         );
-        self.symbol_table.insert(sym.clone());
-        sym.to_expr().call(args.to_vec())
+        body.with_label(label)
     }
 }
 
diff --git a/tests/kani/DynTrait/any_cast_int.rs b/tests/kani/DynTrait/any_cast_int.rs
@@ -1,6 +1,10 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+// kani-flags: --no-restrict-vtable
+// Tracking issue for the need for this flag:
+// https://github.com/model-checking/kani/issues/802
+
 use std::any::Any;
 
 // Cast one dynamic trait object type to another, which is legal because Send
diff --git a/tests/kani/DynTrait/any_cast_int_fail.rs b/tests/kani/DynTrait/any_cast_int_fail.rs
@@ -1,6 +1,10 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+// kani-flags: --no-restrict-vtable
+// Tracking issue for the need for this flag:
+// https://github.com/model-checking/kani/issues/802
+
 use std::any::Any;
 
 // Cast one dynamic trait object type to another, which is legal because Send
diff --git a/tools/kani-link-restrictions/src/main.rs b/tools/kani-link-restrictions/src/main.rs
@@ -23,10 +23,9 @@ fn link_function_pointer_restrictions(data_per_crate: Vec<VtableCtxResults>) ->
     // Iterate call sites
     for crate_data in data_per_crate {
         for call_site in crate_data.call_sites {
-            // CBMC index is 1-indexed:
-            // http://cprover.diffblue.com/md__home_travis_build_diffblue_cbmc_doc_architectural_restrict-function-pointer.html
-            let cbmc_call_site_name =
-                format!("{}.function_pointer_call.1", call_site.function_name);
+            // CBMC Now supports referencing callsites by label:
+            // https://github.com/diffblue/cbmc/pull/6508
+            let cbmc_call_site_name = format!("{}.{}", call_site.function_name, call_site.label);
             let trait_def = call_site.trait_method;
 
             // Look up all possibilities, defaulting to the empty set

Original file line number	Diff line number	Diff line change
`@@ -19,6 +19,7 @@ pub struct TraitDefinedMethod {`
`19`	`19`	`pub struct CallSite {`
`20`	`20`	`pub trait_method: TraitDefinedMethod,`
`21`	`21`	`pub function_name: InternedString,`
	`22`	`+ pub label: InternedString,`
`22`	`23`	`}`
`23`	`24`
`24`	`25`	`#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)]`