Skip to content

Commit

Permalink
Structural check for Rust types instead of name based (rust-lang#499)
Browse files Browse the repository at this point in the history
  • Loading branch information
danielsn authored and tedinski committed Sep 22, 2021
1 parent c2430cc commit 45b5589
Show file tree
Hide file tree
Showing 3 changed files with 88 additions and 33 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -84,11 +84,18 @@ impl SymbolTable {
self.symbol_table.get(name)
}

pub fn lookup_components(&self, aggr_name: &str) -> Option<&Vec<DatatypeComponent>> {
self.lookup(aggr_name).and_then(|x| x.typ.components())
}

pub fn lookup_components_in_type(&self, base_type: &Type) -> Option<&Vec<DatatypeComponent>> {
base_type.type_name().and_then(|aggr_name| self.lookup_components(&aggr_name))
}

/// If aggr_name.field_name exists in the symbol table, return Some(field_type),
/// otherwise, return none.
pub fn lookup_field_type(&self, aggr_name: &str, field_name: &str) -> Option<&Type> {
self.lookup(aggr_name)
.and_then(|x| x.typ.components())
self.lookup_components(aggr_name)
.and_then(|fields| fields.iter().find(|&field| field.name() == field_name))
.and_then(|field| field.field_typ())
}
Expand Down
20 changes: 17 additions & 3 deletions compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -387,6 +387,13 @@ impl Type {
}
}

pub fn is_flexible_array(&self) -> bool {
match self {
FlexibleArray { .. } => true,
_ => false,
}
}

pub fn is_float(&self) -> bool {
match self {
Float => true,
Expand Down Expand Up @@ -453,10 +460,9 @@ impl Type {
}
}

/// This is a union (and not an incomplete union or union tag)
pub fn is_union(&self) -> bool {
pub fn is_struct_like(&self) -> bool {
match self {
Union { .. } => true,
IncompleteStruct { .. } | Struct { .. } | StructTag(_) => true,
_ => false,
}
}
Expand All @@ -469,6 +475,14 @@ impl Type {
}
}

/// This is a union (and not an incomplete union or union tag)
pub fn is_union(&self) -> bool {
match self {
Union { .. } => true,
_ => false,
}
}

/// This is a union tag
pub fn is_union_tag(&self) -> bool {
match self {
Expand Down
90 changes: 62 additions & 28 deletions compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/utils/utils.rs
Original file line number Diff line number Diff line change
Expand Up @@ -85,28 +85,20 @@ impl<'tcx> GotocCtx<'tcx> {
// };
// ```
// And notice that its `.pointer` field is exactly what we want.
assert!(e.typ().is_rust_box(), "expected rust box {:?}", e);
let unique_ptr_typ =
self.symbol_table.lookup_field_type_in_type(e.typ(), "0").unwrap().clone();
assert!(
unique_ptr_typ.is_rust_unique_pointer(),
"{:?}\n\t{}",
unique_ptr_typ,
self.current_fn().readable_name()
);
self.assert_is_rust_box_like(e.typ());
e.member("0", &self.symbol_table).member("pointer", &self.symbol_table)
}

/// Box<T> initializer
/// `boxed_type the_box = >>> { .0=nondet(), .1={ ._marker=nondet(), .pointer=boxed_value } } <<<`
/// `boxed_type` is the type of the resulting expression
pub fn box_value(&self, boxed_value: Expr, boxed_type: Type) -> Expr {
assert!(boxed_type.is_rust_box(), "expected rust box {:?}", boxed_type);
self.assert_is_rust_box_like(&boxed_type);
let get_field_type = |struct_typ, field| {
self.symbol_table.lookup_field_type_in_type(struct_typ, field).unwrap().clone()
};
let unique_ptr_typ = get_field_type(&boxed_type, "0");
assert!(unique_ptr_typ.is_rust_unique_pointer());
self.assert_is_rust_unique_pointer_like(&unique_ptr_typ);
let unique_ptr_pointer_typ = get_field_type(&unique_ptr_typ, "pointer");
assert_eq!(&unique_ptr_pointer_typ, boxed_value.typ());
let unique_ptr_val = Expr::struct_expr_with_nondet_fields(
Expand All @@ -121,29 +113,71 @@ impl<'tcx> GotocCtx<'tcx> {
);
boxed_val
}
}

impl Type {
/// Best effort check if the struct represents a rust "std::alloc::Global".
pub fn assert_is_rust_global_alloc_like(&self, t: &Type) {
// TODO: A std::alloc::Global appears to be an empty struct, in the cases we've seen.
// Is there something smarter we can do here?
assert!(t.is_struct_like());
let components = self.symbol_table.lookup_components_in_type(t).unwrap();
assert_eq!(components.len(), 0);
}

/// Best effort check if the struct represents a rust "std::marker::PhantomData".
pub fn assert_is_rust_phantom_data_like(&self, t: &Type) {
// TODO: A std::marker::PhantomData appears to be an empty struct, in the cases we've seen.
// Is there something smarter we can do here?
assert!(t.is_struct_like());
let components = self.symbol_table.lookup_components_in_type(t).unwrap();
assert_eq!(components.len(), 0);
}

/// Best effort check if the struct represents a Rust "Box". May return false positives.
pub fn is_rust_box(&self) -> bool {
// We have seen variants on the name, including
// tag-std::boxed::Box, tag-core::boxed::Box, tag-boxed::Box.
// If we match on exact names, we're playing whack-a-mole trying to keep track of how this
// can be reimported.
// If we don't, we spuriously fail. https://github.com/model-checking/rmc/issues/113
// TODO: find a better way of checking this https://github.com/model-checking/rmc/issues/152
self.type_name().map_or(false, |name| name.contains("boxed::Box"))
pub fn assert_is_rust_box_like(&self, t: &Type) {
// struct std::boxed::Box<[u8; 8]>::15334369982748499855
// {
// // 1
// struct std::alloc::Global::13633191317886109837 1;
// // 0
// struct std::ptr::Unique<[u8; 8]>::14713681870393313245 0;
// };
assert!(t.is_struct_like());
let components = self.symbol_table.lookup_components_in_type(t).unwrap();
assert_eq!(components.len(), 2);
for c in components {
match c.name() {
"0" => self.assert_is_rust_unique_pointer_like(&c.typ()),
"1" => self.assert_is_rust_global_alloc_like(&c.typ()),
_ => panic!("Unexpected component {} in {:?}", c.name(), t),
}
}
}

/// Checks if the struct represents a Rust "Unique"
pub fn is_rust_unique_pointer(&self) -> bool {
self.type_name().map_or(false, |name| {
name.starts_with("tag-std::ptr::Unique")
|| name.starts_with("tag-core::ptr::Unique")
|| name.starts_with("tag-rustc_std_workspace_core::ptr::Unique")
})
/// Checks if the struct represents a Rust "std::ptr::Unique"
pub fn assert_is_rust_unique_pointer_like(&self, t: &Type) {
// struct std::ptr::Unique<[u8; 8]>::14713681870393313245
// {
// // _marker
// struct std::marker::PhantomData<[u8; 8]>::18073278521438838603 _marker;
// // pointer
// struct [u8::16712579856250238426; 8] *pointer;
// };
assert!(t.is_struct_like());
let components = self.symbol_table.lookup_components_in_type(t).unwrap();
assert_eq!(components.len(), 2);
for c in components {
match c.name() {
"_marker" => self.assert_is_rust_phantom_data_like(&c.typ()),
"pointer" => {
assert!(c.typ().is_pointer() || c.typ().is_rust_fat_ptr(&self.symbol_table))
}
_ => panic!("Unexpected component {} in {:?}", c.name(), t),
}
}
}
}

impl Type {
pub fn is_rust_slice_fat_ptr(&self, st: &SymbolTable) -> bool {
match self {
Type::Struct { components, .. } => {
Expand Down

0 comments on commit 45b5589

Please sign in to comment.