Skip to content

Commit

Permalink
Late toolchain upgrade to use nightly-2022-08-02 (#1522)
Browse files Browse the repository at this point in the history
* Fix compilation errors

Regression is still failing. Related changes:

- rust-lang/rust#99420
- rust-lang/rust#99495
- rust-lang/rust#99844
- rust-lang/rust#99058

* Change test to expect compilation failure

The compiler has reverted their fix to Opaque types due to performance
degradation.

* Fix VTable handling now that it has an Opaque type

 - Add an implementation for vtable_size and vtable_align intrinsics.
 - Change how we handled Foreign types. Even though they are unsized, a
   pointer to foreign types is a thin pointer.

Co-authored-by: Daniel Schwartz-Narbonne <danielsn@users.noreply.github.com>
  • Loading branch information
celinval and danielsn authored Aug 17, 2022
1 parent 131c073 commit 632fda6
Show file tree
Hide file tree
Showing 15 changed files with 262 additions and 128 deletions.
2 changes: 1 addition & 1 deletion cprover_bindings/src/goto_program/expr.rs
Original file line number Diff line number Diff line change
Expand Up @@ -484,7 +484,7 @@ impl Expr {

/// `(typ) self`.
pub fn cast_to(self, typ: Type) -> Self {
assert!(self.can_cast_to(&typ), "Can't cast\n\n{:?}\n\n{:?}", self, typ);
assert!(self.can_cast_to(&typ), "Can't cast\n\n{:?} ({:?})\n\n{:?}", self, self.typ, typ);
if self.typ == typ {
self
} else if typ.is_bool() {
Expand Down
50 changes: 27 additions & 23 deletions kani-compiler/src/codegen_cprover_gotoc/archive.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ use std::fs::File;
use std::io::{self, Read, Seek};
use std::path::{Path, PathBuf};

use rustc_codegen_ssa::back::archive::ArchiveBuilder;
use rustc_codegen_ssa::back::archive::{ArchiveBuilder, ArchiveBuilderBuilder};
use rustc_session::Session;

use object::read::archive::ArchiveFile;
Expand All @@ -34,7 +34,6 @@ enum ArchiveEntry {

pub(crate) struct ArArchiveBuilder<'a> {
sess: &'a Session,
dst: PathBuf,
use_gnu_style_archive: bool,

src_archives: Vec<File>,
Expand All @@ -44,27 +43,18 @@ pub(crate) struct ArArchiveBuilder<'a> {
}

impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
fn new(sess: &'a Session, output: &Path) -> Self {
ArArchiveBuilder {
sess,
dst: output.to_path_buf(),
use_gnu_style_archive: sess.target.archive_format == "gnu",
src_archives: vec![],
entries: vec![],
}
}

fn add_file(&mut self, file: &Path) {
self.entries.push((
file.file_name().unwrap().to_str().unwrap().to_string().into_bytes(),
ArchiveEntry::File(file.to_owned()),
));
}

fn add_archive<F>(&mut self, archive_path: &Path, mut skip: F) -> std::io::Result<()>
where
F: FnMut(&str) -> bool + 'static,
{
fn add_archive(
&mut self,
archive_path: &Path,
mut skip: Box<dyn FnMut(&str) -> bool + 'static>,
) -> std::io::Result<()> {
let read_cache = ReadCache::new(std::fs::File::open(&archive_path)?);
let archive = ArchiveFile::parse(&read_cache).unwrap();
let archive_index = self.src_archives.len();
Expand All @@ -85,7 +75,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
Ok(())
}

fn build(mut self) -> bool {
fn build(mut self: Box<Self>, output: &Path) -> bool {
enum BuilderKind {
Bsd(ar::Builder<File>),
Gnu(ar::GnuBuilder<File>),
Expand Down Expand Up @@ -122,7 +112,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {

let mut builder = if self.use_gnu_style_archive {
BuilderKind::Gnu(ar::GnuBuilder::new(
File::create(&self.dst).unwrap_or_else(|err| {
File::create(&output).unwrap_or_else(|err| {
sess.fatal(&format!(
"error opening destination during archive building: {}",
err
Expand All @@ -131,7 +121,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
entries.iter().map(|(name, _)| name.clone()).collect(),
))
} else {
BuilderKind::Bsd(ar::Builder::new(File::create(&self.dst).unwrap_or_else(|err| {
BuilderKind::Bsd(ar::Builder::new(File::create(&output).unwrap_or_else(|err| {
sess.fatal(&format!("error opening destination during archive building: {}", err));
})))
};
Expand All @@ -150,13 +140,27 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
std::mem::drop(builder);
any_members
}
}

fn inject_dll_import_lib(
&mut self,
pub(crate) struct ArArchiveBuilderBuilder;

impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder {
fn new_archive_builder<'a>(&self, sess: &'a Session) -> Box<dyn ArchiveBuilder<'a> + 'a> {
Box::new(ArArchiveBuilder {
sess,
use_gnu_style_archive: sess.target.archive_format == "gnu",
src_archives: vec![],
entries: vec![],
})
}

fn create_dll_import_lib(
&self,
_sess: &Session,
_lib_name: &str,
_dll_imports: &[rustc_session::cstore::DllImport],
_tmpdir: &rustc_data_structures::temp_dir::MaybeTempDir,
) {
_tmpdir: &Path,
) -> PathBuf {
unimplemented!("injecting dll imports is not supported");
}
}
29 changes: 28 additions & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
//! this module handles intrinsics
use super::typ::pointee_type;
use super::typ::{self, pointee_type};
use super::PropertyClass;
use crate::codegen_cprover_gotoc::GotocCtx;
use cbmc::goto_program::{
Expand Down Expand Up @@ -35,6 +35,11 @@ struct SizeAlign {
align: Expr,
}

enum VTableInfo {
Size,
Align,
}

impl<'tcx> GotocCtx<'tcx> {
fn binop<F: FnOnce(Expr, Expr) -> Expr>(
&mut self,
Expand Down Expand Up @@ -703,6 +708,8 @@ impl<'tcx> GotocCtx<'tcx> {
assert!(self.place_ty(p).is_unit());
self.codegen_volatile_store(fargs, farg_types, loc)
}
"vtable_size" => self.vtable_info(VTableInfo::Size, fargs, p, loc),
"vtable_align" => self.vtable_info(VTableInfo::Align, fargs, p, loc),
"wrapping_add" => codegen_wrapping_op!(plus),
"wrapping_mul" => codegen_wrapping_op!(mul),
"wrapping_sub" => codegen_wrapping_op!(sub),
Expand Down Expand Up @@ -1201,6 +1208,26 @@ impl<'tcx> GotocCtx<'tcx> {
self.codegen_expr_to_place(p, e)
}

fn vtable_info(
&mut self,
info: VTableInfo,
mut fargs: Vec<Expr>,
place: &Place<'tcx>,
_loc: Location,
) -> Stmt {
assert_eq!(fargs.len(), 1, "vtable intrinsics expects one raw pointer argument");
let vtable_obj = fargs
.pop()
.unwrap()
.cast_to(self.codegen_ty_common_vtable().to_pointer())
.dereference();
let expr = match info {
VTableInfo::Size => vtable_obj.member(typ::VTABLE_SIZE_FIELD, &self.symbol_table),
VTableInfo::Align => vtable_obj.member(typ::VTABLE_ALIGN_FIELD, &self.symbol_table),
};
self.codegen_expr_to_place(place, expr)
}

/// This function computes the size and alignment of a dynamically-sized type.
/// The implementations follows closely the SSA implementation found in
/// rustc_codegen_ssa::glue::size_and_align_of_dst.
Expand Down
8 changes: 8 additions & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -379,6 +379,14 @@ impl<'tcx> GotocCtx<'tcx> {
let name = format!("{}::{:?}", self.full_crate_name(), alloc_id);
self.codegen_allocation(alloc.inner(), |_| name.clone(), Some(name.clone()))
}
GlobalAlloc::VTable(ty, trait_ref) => {
// This is similar to GlobalAlloc::Memory but the type is opaque to rust and it
// requires a bit more logic to get information about the allocation.
let alloc_id = self.tcx.vtable_allocation((ty, trait_ref));
let alloc = self.tcx.global_alloc(alloc_id).unwrap_memory();
let name = format!("{}::{:?}", self.full_crate_name(), alloc_id);
self.codegen_allocation(alloc.inner(), |_| name.clone(), Some(name.clone()))
}
};
assert!(res_t.is_pointer() || res_t.is_transparent_type(&self.symbol_table));
let offset_addr = base_addr
Expand Down
37 changes: 15 additions & 22 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
//! in [GotocCtx::codegen_place] below.
use super::typ::TypeExt;
use crate::codegen_cprover_gotoc::codegen::typ::{pointee_type, std_pointee_type};
use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
use crate::codegen_cprover_gotoc::GotocCtx;
use cbmc::goto_program::{Expr, Location, Type};
Expand Down Expand Up @@ -360,31 +361,30 @@ impl<'tcx> GotocCtx<'tcx> {
before.goto_expr
};

let inner_mir_typ_and_mut = base_type.builtin_deref(true).unwrap();
let fat_ptr_mir_typ = if self.is_box_of_unsized(base_type) {
// If we have a box, its fat pointer typ is a pointer to the boxes inner type.
Some(self.tcx.mk_ptr(inner_mir_typ_and_mut))
} else if self.is_ref_of_unsized(base_type) {
Some(before.mir_typ_or_variant.expect_type())
let inner_mir_typ = std_pointee_type(base_type).unwrap();
let (fat_ptr_mir_typ, fat_ptr_goto_expr) = if self.use_thin_pointer(inner_mir_typ) {
(before.fat_ptr_mir_typ, before.fat_ptr_goto_expr)
} else {
before.fat_ptr_mir_typ
(Some(before.mir_typ_or_variant.expect_type()), Some(inner_goto_expr.clone()))
};
let fat_ptr_goto_expr =
if self.is_box_of_unsized(base_type) || self.is_ref_of_unsized(base_type) {
Some(inner_goto_expr.clone())
} else {
before.fat_ptr_goto_expr
};

// Check that we have a valid trait or slice fat pointer
if let Some(fat_ptr) = fat_ptr_goto_expr.clone() {
assert!(
fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table)
|| fat_ptr.typ().is_rust_slice_fat_ptr(&self.symbol_table)
|| fat_ptr.typ().is_rust_slice_fat_ptr(&self.symbol_table),
"Unexpected type: {:?} -- {:?}",
fat_ptr.typ(),
pointee_type(fat_ptr_mir_typ.unwrap()).unwrap().kind(),
);
assert!(
self.use_fat_pointer(pointee_type(fat_ptr_mir_typ.unwrap()).unwrap()),
"Unexpected type: {:?} -- {:?}",
fat_ptr.typ(),
fat_ptr_mir_typ,
);
};

let inner_mir_typ = inner_mir_typ_and_mut.ty;
let expr = match inner_mir_typ.kind() {
ty::Slice(_) | ty::Str | ty::Dynamic(..) => {
inner_goto_expr.member("data", &self.symbol_table)
Expand Down Expand Up @@ -547,13 +547,6 @@ impl<'tcx> GotocCtx<'tcx> {
self,
)
}
ProjectionElem::OpaqueCast(ty) => ProjectedPlace::try_new(
before.goto_expr.cast_to(self.codegen_ty(ty)),
TypeOrVariant::Type(ty),
before.fat_ptr_goto_expr,
before.fat_ptr_mir_typ,
self,
),
}
}

Expand Down
54 changes: 22 additions & 32 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,7 @@ impl<'tcx> GotocCtx<'tcx> {
let left_typ = self.operand_ty(left_op);
let right_typ = self.operand_ty(left_op);
assert_eq!(left_typ, right_typ, "Cannot compare pointers of different types");
assert!(self.is_ref_of_unsized(left_typ));
assert!(self.is_fat_pointer(left_typ));

if self.is_vtable_fat_pointer(left_typ) {
// Codegen an assertion failure since vtable comparison is not stable.
Expand Down Expand Up @@ -334,7 +334,7 @@ impl<'tcx> GotocCtx<'tcx> {
self.codegen_unchecked_scalar_binop(op, e1, e2)
}
BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => {
if self.is_ref_of_unsized(self.operand_ty(e1)) {
if self.is_fat_pointer(self.operand_ty(e1)) {
self.codegen_comparison_fat_ptr(op, e1, e2, loc)
} else {
self.codegen_comparison(op, e1, e2)
Expand Down Expand Up @@ -628,11 +628,11 @@ impl<'tcx> GotocCtx<'tcx> {
}

// Cast between fat pointers
if self.is_ref_of_unsized(src_t) && self.is_ref_of_unsized(dst_t) {
if self.is_fat_pointer(src_t) && self.is_fat_pointer(dst_t) {
return self.codegen_fat_ptr_to_fat_ptr_cast(src, dst_t);
}

if self.is_ref_of_unsized(src_t) && self.is_ref_of_sized(dst_t) {
if self.is_fat_pointer(src_t) && !self.is_fat_pointer(dst_t) {
return self.codegen_fat_ptr_to_thin_ptr_cast(src, dst_t);
}

Expand Down Expand Up @@ -760,14 +760,9 @@ impl<'tcx> GotocCtx<'tcx> {
dst_mir_type,
)
} else {
// Check that the source is either not a pointer, or a thin or a slice pointer
assert!(
pointee_type(src_mir_type)
.map_or(true, |p| self.use_thin_pointer(p) || self.use_slice_fat_pointer(p))
);

// Sized to unsized cast
self.cast_sized_expr_to_unsized_expr(src_goto_expr, src_mir_type, dst_mir_type)
// Recursively cast the source expression into an unsized expression.
// This will include thin pointers, slices, and Adt.
self.cast_expr_to_unsized_expr(src_goto_expr, src_mir_type, dst_mir_type)
}
}

Expand Down Expand Up @@ -1041,10 +1036,9 @@ impl<'tcx> GotocCtx<'tcx> {
Some(dynamic_fat_ptr(dst_goto_type, data, vtable, &self.symbol_table))
}

/// Cast a sized object to an unsized object: the result of the cast will be
/// a fat pointer or an ADT with a nested fat pointer. Return the result of
/// the cast as Some(expr) and return None if no cast was required.
fn cast_sized_expr_to_unsized_expr(
/// Cast an object / thin pointer to a fat pointer or an ADT with a nested fat pointer.
/// Return the result of the cast as Some(expr) and return None if no cast was required.
fn cast_expr_to_unsized_expr(
&mut self,
src_goto_expr: Expr,
src_mir_type: Ty<'tcx>,
Expand All @@ -1054,19 +1048,6 @@ impl<'tcx> GotocCtx<'tcx> {
return None; // no cast required, nothing to do
}

// The src type will be sized, but the dst type may not be unsized. If
// the dst is an adt containing a pointer to a trait object nested
// within the adt, the trait object will be unsized and the pointer will
// be a fat pointer, but the adt (containing the fat pointer) will
// itself be sized.
assert!(
src_mir_type.is_sized(self.tcx.at(rustc_span::DUMMY_SP), ty::ParamEnv::reveal_all())
);

// The src type cannot be a pointer to a dynamic trait object, otherwise
// we should have called cast_unsized_dyn_trait_to_unsized_dyn_trait
assert!(!self.is_vtable_fat_pointer(src_mir_type));

match (src_mir_type.kind(), dst_mir_type.kind()) {
(ty::Ref(..), ty::Ref(..)) => {
self.cast_sized_pointer_to_fat_pointer(src_goto_expr, src_mir_type, dst_mir_type)
Expand All @@ -1081,7 +1062,7 @@ impl<'tcx> GotocCtx<'tcx> {
self.cast_sized_pointer_to_fat_pointer(src_goto_expr, src_mir_type, dst_mir_type)
}
(ty::Adt(..), ty::Adt(..)) => {
self.cast_sized_adt_to_unsized_adt(src_goto_expr, src_mir_type, dst_mir_type)
self.cast_adt_to_unsized_adt(src_goto_expr, src_mir_type, dst_mir_type)
}
(src_kind, dst_kind) => {
unreachable!(
Expand All @@ -1095,6 +1076,11 @@ impl<'tcx> GotocCtx<'tcx> {
/// Cast a pointer to a sized object to a fat pointer to an unsized object.
/// Return the result of the cast as Some(expr) and return None if no cast
/// was required.
/// Note: This seems conceptually wrong. If we are converting sized to unsized, how come
/// source and destination can have the same type? Also, how come destination can be a thin
/// pointer?
/// TODO: Fix the cast code structure:
/// <https://github.com/model-checking/kani/issues/1531>
fn cast_sized_pointer_to_fat_pointer(
&mut self,
src_goto_expr: Expr,
Expand All @@ -1106,6 +1092,10 @@ impl<'tcx> GotocCtx<'tcx> {
return None;
};

// The src type cannot be a pointer to a dynamic trait object, otherwise
// we should have called cast_unsized_dyn_trait_to_unsized_dyn_trait
assert!(!self.is_vtable_fat_pointer(src_mir_type));

// extract pointee types from pointer types, panic if type is not a
// pointer type.
let src_pointee_type = pointee_type(src_mir_type).unwrap();
Expand Down Expand Up @@ -1192,10 +1182,10 @@ impl<'tcx> GotocCtx<'tcx> {
}
}

/// Cast a sized ADT to an unsized ADT (an ADT with a nested fat pointer).
/// Cast an ADT (sized or unsized) to an unsized ADT (an ADT with a nested fat pointer).
/// Return the result of the cast as Some(expr) and return None if no cast
/// was required.
fn cast_sized_adt_to_unsized_adt(
fn cast_adt_to_unsized_adt(
&mut self,
src_goto_expr: Expr,
src_mir_type: Ty<'tcx>,
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -595,7 +595,7 @@ impl<'tcx> GotocCtx<'tcx> {
| InstanceDef::DropGlue(_, Some(_))
| InstanceDef::Intrinsic(..)
| InstanceDef::FnPtrShim(..)
| InstanceDef::VtableShim(..)
| InstanceDef::VTableShim(..)
| InstanceDef::ReifyShim(..)
| InstanceDef::ClosureOnceShim { .. }
| InstanceDef::CloneShim(..) => {
Expand Down
Loading

0 comments on commit 632fda6

Please sign in to comment.