Skip to content

Commit 7820fa5

Browse files
avanhattavanhatt
authored
Add option to restrict vtable function pointers (model-checking#536)
Add vtable restriction option, need CBMC PR to use
1 parent 601b2f8 commit 7820fa5

File tree

27 files changed

+754
-70
lines changed

27 files changed

+754
-70
lines changed

‎Cargo.lock‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3342,6 +3342,25 @@ dependencies = [
33423342
name = "rmc"
33433343
version = "0.1.0"
33443344

3345+
[[package]]
3346+
name = "rmc-link-restrictions"
3347+
version = "0.1.0"
3348+
dependencies = [
3349+
"rmc_restrictions",
3350+
"rustc_data_structures",
3351+
"serde",
3352+
"serde_json",
3353+
]
3354+
3355+
[[package]]
3356+
name = "rmc_restrictions"
3357+
version = "0.1.0"
3358+
dependencies = [
3359+
"cbmc",
3360+
"rustc_data_structures",
3361+
"serde",
3362+
]
3363+
33453364
[[package]]
33463365
name = "rust-demangler"
33473366
version = "0.0.1"
@@ -3884,6 +3903,7 @@ dependencies = [
38843903
"libc",
38853904
"measureme 9.1.2",
38863905
"num",
3906+
"rmc_restrictions",
38873907
"rustc-demangle",
38883908
"rustc_arena",
38893909
"rustc_ast",

‎Cargo.toml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ members = [
55
"library/std",
66
"library/test",
77
"library/rmc",
8+
"library/rmc_restrictions",
89
"src/rustdoc-json-types",
910
"src/tools/cargotest",
1011
"src/tools/clippy",
@@ -21,6 +22,7 @@ members = [
2122
"src/tools/build-manifest",
2223
"src/tools/remote-test-client",
2324
"src/tools/remote-test-server",
25+
"src/tools/rmc-link-restrictions",
2426
"src/tools/rust-installer",
2527
"src/tools/rust-demangler",
2628
"src/tools/cargo",

‎compiler/cbmc/src/irep/serialize.rs‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,32 @@ impl Serialize for InternedString {
9898
}
9999
}
100100

101+
struct InternedStringVisitor;
102+
103+
impl<'de> serde::Deserialize<'de> for InternedString {
104+
fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
105+
where
106+
D: serde::Deserializer<'de>,
107+
{
108+
deserializer.deserialize_str(InternedStringVisitor)
109+
}
110+
}
111+
112+
impl<'de> serde::de::Visitor<'de> for InternedStringVisitor {
113+
type Value = InternedString;
114+
115+
fn expecting(&self, formatter: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
116+
formatter.write_str("a String like thing")
117+
}
118+
119+
fn visit_str<E>(self, v: &str) -> Result<Self::Value, E>
120+
where
121+
E: serde::de::Error,
122+
{
123+
Ok(v.into())
124+
}
125+
}
126+
101127
impl Serialize for Symbol {
102128
fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
103129
where

‎compiler/rustc_codegen_rmc/Cargo.toml‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ serde = "1"
2121
serde_json = "1"
2222
snap = "1"
2323
tracing = "0.1"
24+
rmc_restrictions = { path = "../../library/rmc_restrictions" }
2425
rustc_middle = { path = "../rustc_middle" }
2526
rustc-demangle = "0.1.21"
2627
rustc_arena = { path = "../rustc_arena" }

‎compiler/rustc_codegen_rmc/src/codegen/assumptions.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -178,7 +178,7 @@ impl<'tcx> GotocCtx<'tcx> {
178178
self.find_function(fname)
179179
}
180180
}
181-
ty::Dynamic(_, _) => unimplemented!(),
181+
ty::Dynamic(_, _) => None,
182182
ty::Projection(_) | ty::Opaque(_, _) => {
183183
let normalized = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), t);
184184
self.codegen_assumption_ref_ptr(fname, t, normalized, is_ref)

‎compiler/rustc_codegen_rmc/src/codegen/rvalue.rs‎

Lines changed: 51 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
use super::typ::{is_pointer, pointee_type, TypeExt};
44
use crate::utils::{dynamic_fat_ptr, slice_fat_ptr};
5-
use crate::GotocCtx;
5+
use crate::{GotocCtx, VtableCtx};
66
use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type};
77
use cbmc::utils::{aggr_tag, BUG_REPORT_URL};
88
use cbmc::MachineModel;
@@ -722,7 +722,17 @@ impl<'tcx> GotocCtx<'tcx> {
722722

723723
// Lookup in the symbol table using the full symbol table name/key
724724
let fn_name = self.symbol_name(instance);
725+
725726
if let Some(fn_symbol) = self.symbol_table.lookup(&fn_name) {
727+
if self.vtable_ctx.emit_vtable_restrictions {
728+
// Add to the possible method names for this trait type
729+
self.vtable_ctx.add_possible_method(
730+
self.normalized_trait_name(t).into(),
731+
idx,
732+
fn_name.into(),
733+
);
734+
}
735+
726736
// Create a pointer to the method
727737
// Note that the method takes a self* as the first argument, but the vtable field type has a void* as the first arg.
728738
// So we need to cast it at the end.
@@ -746,13 +756,22 @@ impl<'tcx> GotocCtx<'tcx> {
746756
trait_ty: &'tcx ty::TyS<'tcx>,
747757
) -> Expr {
748758
let drop_instance = Instance::resolve_drop_in_place(self.tcx, ty).polymorphize(self.tcx);
749-
let drop_sym_name = self.symbol_name(drop_instance);
759+
let drop_sym_name: InternedString = self.symbol_name(drop_instance).into();
750760

751761
// The drop instance has the concrete object type, for consistency with
752762
// type codegen we need the trait type for the function parameter.
753763
let trait_fn_ty = self.trait_vtable_drop_type(trait_ty);
754764

755-
if let Some(drop_sym) = self.symbol_table.lookup(&drop_sym_name) {
765+
if let Some(drop_sym) = self.symbol_table.lookup(drop_sym_name) {
766+
if self.vtable_ctx.emit_vtable_restrictions {
767+
// Add to the possible method names for this trait type
768+
self.vtable_ctx.add_possible_method(
769+
self.normalized_trait_name(trait_ty).into(),
770+
VtableCtx::drop_index(),
771+
drop_sym_name,
772+
);
773+
}
774+
756775
Expr::symbol_expression(drop_sym_name, drop_sym.clone().typ)
757776
.address_of()
758777
.cast_to(trait_fn_ty)
@@ -761,37 +780,37 @@ impl<'tcx> GotocCtx<'tcx> {
761780
// for it. Build and insert a function that just calls an unimplemented block
762781
// to maintain soundness.
763782
let drop_sym_name = format!("{}_unimplemented", self.symbol_name(drop_instance));
764-
765-
// Function body
766-
let unimplemented = self
767-
.codegen_unimplemented(
768-
format!("drop_in_place for {}", drop_sym_name).as_str(),
769-
Type::empty(),
783+
let drop_sym = self.ensure(&drop_sym_name, |ctx, name| {
784+
// Function body
785+
let unimplemented = ctx
786+
.codegen_unimplemented(
787+
format!("drop_in_place for {}", drop_sym_name).as_str(),
788+
Type::empty(),
789+
Location::none(),
790+
"https://github.com/model-checking/rmc/issues/281",
791+
)
792+
.as_stmt(Location::none());
793+
794+
// Declare symbol for the single, self parameter
795+
let param_name = format!("{}::1::var{:?}", drop_sym_name, 0);
796+
let param_sym = Symbol::variable(
797+
param_name.clone(),
798+
param_name,
799+
ctx.codegen_ty(trait_ty).to_pointer(),
800+
Location::none(),
801+
);
802+
ctx.symbol_table.insert(param_sym.clone());
803+
804+
// Build and insert the function itself
805+
Symbol::function(
806+
name,
807+
Type::code(vec![param_sym.to_function_parameter()], Type::empty()),
808+
Some(Stmt::block(vec![unimplemented], Location::none())),
809+
NO_PRETTY_NAME,
770810
Location::none(),
771-
"https://github.com/model-checking/rmc/issues/281",
772811
)
773-
.as_stmt(Location::none());
774-
775-
// Declare symbol for the single, self parameter
776-
let param_name = format!("{}::1::var{:?}", drop_sym_name, 0);
777-
let param_sym = Symbol::variable(
778-
param_name.clone(),
779-
param_name,
780-
self.codegen_ty(trait_ty).to_pointer(),
781-
Location::none(),
782-
);
783-
self.symbol_table.insert(param_sym.clone());
784-
785-
// Build and insert the function itself
786-
let sym = Symbol::function(
787-
&drop_sym_name,
788-
Type::code(vec![param_sym.to_function_parameter()], Type::empty()),
789-
Some(Stmt::block(vec![unimplemented], Location::none())),
790-
NO_PRETTY_NAME,
791-
Location::none(),
792-
);
793-
self.symbol_table.insert(sym.clone());
794-
Expr::symbol_expression(drop_sym_name, sym.typ).address_of().cast_to(trait_fn_ty)
812+
});
813+
drop_sym.to_expr().address_of().cast_to(trait_fn_ty)
795814
}
796815
}
797816

‎compiler/rustc_codegen_rmc/src/codegen/statement.rs‎

Lines changed: 23 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
use super::typ::TypeExt;
44
use super::typ::FN_RETURN_VOID_VAR_NAME;
5-
use crate::GotocCtx;
5+
use crate::{GotocCtx, VtableCtx};
66
use cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Type};
77
use rustc_hir::def_id::DefId;
88
use rustc_middle::mir;
@@ -143,8 +143,17 @@ impl<'tcx> GotocCtx<'tcx> {
143143
let self_ref =
144144
self_ref.cast_to(trait_fat_ptr.typ().clone().to_pointer());
145145

146-
let func_exp: Expr = fn_ptr.dereference();
147-
func_exp.call(vec![self_ref]).as_stmt(Location::none())
146+
let call = if self.vtable_ctx.emit_vtable_restrictions {
147+
self.virtual_call_with_restricted_fn_ptr(
148+
trait_fat_ptr.typ().clone(),
149+
VtableCtx::drop_index(),
150+
fn_ptr,
151+
vec![self_ref],
152+
)
153+
} else {
154+
fn_ptr.dereference().call(vec![self_ref])
155+
};
156+
call.as_stmt(Location::none())
148157
}
149158
_ => {
150159
// Non-virtual, direct drop call
@@ -449,12 +458,17 @@ impl<'tcx> GotocCtx<'tcx> {
449458
let assert_nonnull = Stmt::assert(call_is_nonnull, &assert_msg, loc.clone());
450459

451460
// Virtual function call and corresponding nonnull assertion.
452-
let func_exp: Expr = fn_ptr.dereference();
453-
vec![
454-
assert_nonnull,
455-
self.codegen_expr_to_place(place, func_exp.call(fargs.to_vec()))
456-
.with_location(loc.clone()),
457-
]
461+
let call = if self.vtable_ctx.emit_vtable_restrictions {
462+
self.virtual_call_with_restricted_fn_ptr(
463+
trait_fat_ptr.typ().clone(),
464+
idx,
465+
fn_ptr,
466+
fargs.to_vec(),
467+
)
468+
} else {
469+
fn_ptr.dereference().call(fargs.to_vec())
470+
};
471+
vec![assert_nonnull, self.codegen_expr_to_place(place, call).with_location(loc.clone())]
458472
}
459473

460474
/// 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‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -486,8 +486,8 @@ impl<'tcx> GotocCtx<'tcx> {
486486
pub fn codegen_ty(&mut self, ty: Ty<'tcx>) -> Type {
487487
let goto_typ = self.codegen_ty_inner(ty);
488488
if let Some(tag) = goto_typ.tag() {
489-
if !self.type_map.contains_key(&tag.to_string()) {
490-
self.type_map.insert(tag.to_string(), ty);
489+
if !self.type_map.contains_key(&tag) {
490+
self.type_map.insert(tag, ty);
491491
}
492492
}
493493
goto_typ

‎compiler/rustc_codegen_rmc/src/compiler_interface.rs‎

Lines changed: 20 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ use crate::GotocCtx;
88
use bitflags::_core::any::Any;
99
use cbmc::goto_program::symtab_transformer;
1010
use cbmc::goto_program::SymbolTable;
11+
use cbmc::InternedString;
12+
use rmc_restrictions::VtableCtxResults;
1113
use rustc_codegen_ssa::traits::CodegenBackend;
1214
use rustc_data_structures::fx::FxHashMap;
1315
use rustc_errors::ErrorReported;
@@ -27,9 +29,10 @@ use tracing::{debug, warn};
2729

2830
// #[derive(RustcEncodable, RustcDecodable)]
2931
pub struct GotocCodegenResult {
30-
pub type_map: BTreeMap<String, String>,
32+
pub type_map: BTreeMap<InternedString, InternedString>,
3133
pub symtab: SymbolTable,
3234
pub crate_name: rustc_span::Symbol,
35+
pub vtable_restrictions: Option<VtableCtxResults>,
3336
}
3437

3538
#[derive(Clone)]
@@ -130,12 +133,22 @@ impl CodegenBackend for GotocCodegenBackend {
130133
&tcx.sess.opts.debugging_opts.symbol_table_passes,
131134
);
132135

133-
let type_map = BTreeMap::from_iter(c.type_map.into_iter().map(|(k, v)| (k, v.to_string())));
136+
// Map MIR types to GotoC types
137+
let type_map =
138+
BTreeMap::from_iter(c.type_map.into_iter().map(|(k, v)| (k, v.to_string().into())));
139+
140+
// Get the vtable function pointer restrictions if requested
141+
let vtable_restrictions = if c.vtable_ctx.emit_vtable_restrictions {
142+
Some(c.vtable_ctx.get_virtual_function_restrictions())
143+
} else {
144+
None
145+
};
134146

135147
Box::new(GotocCodegenResult {
136148
type_map,
137149
symtab: symbol_table,
138150
crate_name: tcx.crate_name(LOCAL_CRATE) as rustc_span::Symbol,
151+
vtable_restrictions: vtable_restrictions,
139152
})
140153
}
141154

@@ -163,6 +176,11 @@ impl CodegenBackend for GotocCodegenBackend {
163176
let base_filename = outputs.path(OutputType::Object);
164177
write_file(&base_filename, "symtab.json", &result.symtab);
165178
write_file(&base_filename, "type_map.json", &result.type_map);
179+
180+
// If they exist, write out vtable virtual call function pointer restrictions
181+
if let Some(restrictions) = result.vtable_restrictions {
182+
write_file(&base_filename, "restrictions.json", &restrictions);
183+
}
166184
}
167185

168186
Ok(())

‎compiler/rustc_codegen_rmc/src/context/current_fn.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ use rustc_middle::ty::Instance;
99
use rustc_middle::ty::PolyFnSig;
1010

1111
/// This structure represents useful data about the function we are currently compiling.
12+
#[derive(Debug)]
1213
pub struct CurrentFnCtx<'tcx> {
1314
/// The GOTO block we are compiling into
1415
block: Vec<Stmt>,

0 commit comments

Comments
 (0)