Skip to content

Commit 632fda6

Browse files
celinvaldanielsn
celinval
and
danielsn
authored
Late toolchain upgrade to use nightly-2022-08-02 (#1522)
* 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>
1 parent 131c073 commit 632fda6

File tree

15 files changed

+262
-128
lines changed

15 files changed

+262
-128
lines changed

‎cprover_bindings/src/goto_program/expr.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -484,7 +484,7 @@ impl Expr {
484484

485485
/// `(typ) self`.
486486
pub fn cast_to(self, typ: Type) -> Self {
487-
assert!(self.can_cast_to(&typ), "Can't cast\n\n{:?}\n\n{:?}", self, typ);
487+
assert!(self.can_cast_to(&typ), "Can't cast\n\n{:?} ({:?})\n\n{:?}", self, self.typ, typ);
488488
if self.typ == typ {
489489
self
490490
} else if typ.is_bool() {

‎kani-compiler/src/codegen_cprover_gotoc/archive.rs

Lines changed: 27 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ use std::fs::File;
2020
use std::io::{self, Read, Seek};
2121
use std::path::{Path, PathBuf};
2222

23-
use rustc_codegen_ssa::back::archive::ArchiveBuilder;
23+
use rustc_codegen_ssa::back::archive::{ArchiveBuilder, ArchiveBuilderBuilder};
2424
use rustc_session::Session;
2525

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

3535
pub(crate) struct ArArchiveBuilder<'a> {
3636
sess: &'a Session,
37-
dst: PathBuf,
3837
use_gnu_style_archive: bool,
3938

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

4645
impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
47-
fn new(sess: &'a Session, output: &Path) -> Self {
48-
ArArchiveBuilder {
49-
sess,
50-
dst: output.to_path_buf(),
51-
use_gnu_style_archive: sess.target.archive_format == "gnu",
52-
src_archives: vec![],
53-
entries: vec![],
54-
}
55-
}
56-
5746
fn add_file(&mut self, file: &Path) {
5847
self.entries.push((
5948
file.file_name().unwrap().to_str().unwrap().to_string().into_bytes(),
6049
ArchiveEntry::File(file.to_owned()),
6150
));
6251
}
6352

64-
fn add_archive<F>(&mut self, archive_path: &Path, mut skip: F) -> std::io::Result<()>
65-
where
66-
F: FnMut(&str) -> bool + 'static,
67-
{
53+
fn add_archive(
54+
&mut self,
55+
archive_path: &Path,
56+
mut skip: Box<dyn FnMut(&str) -> bool + 'static>,
57+
) -> std::io::Result<()> {
6858
let read_cache = ReadCache::new(std::fs::File::open(&archive_path)?);
6959
let archive = ArchiveFile::parse(&read_cache).unwrap();
7060
let archive_index = self.src_archives.len();
@@ -85,7 +75,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
8575
Ok(())
8676
}
8777

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

123113
let mut builder = if self.use_gnu_style_archive {
124114
BuilderKind::Gnu(ar::GnuBuilder::new(
125-
File::create(&self.dst).unwrap_or_else(|err| {
115+
File::create(&output).unwrap_or_else(|err| {
126116
sess.fatal(&format!(
127117
"error opening destination during archive building: {}",
128118
err
@@ -131,7 +121,7 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
131121
entries.iter().map(|(name, _)| name.clone()).collect(),
132122
))
133123
} else {
134-
BuilderKind::Bsd(ar::Builder::new(File::create(&self.dst).unwrap_or_else(|err| {
124+
BuilderKind::Bsd(ar::Builder::new(File::create(&output).unwrap_or_else(|err| {
135125
sess.fatal(&format!("error opening destination during archive building: {}", err));
136126
})))
137127
};
@@ -150,13 +140,27 @@ impl<'a> ArchiveBuilder<'a> for ArArchiveBuilder<'a> {
150140
std::mem::drop(builder);
151141
any_members
152142
}
143+
}
153144

154-
fn inject_dll_import_lib(
155-
&mut self,
145+
pub(crate) struct ArArchiveBuilderBuilder;
146+
147+
impl ArchiveBuilderBuilder for ArArchiveBuilderBuilder {
148+
fn new_archive_builder<'a>(&self, sess: &'a Session) -> Box<dyn ArchiveBuilder<'a> + 'a> {
149+
Box::new(ArArchiveBuilder {
150+
sess,
151+
use_gnu_style_archive: sess.target.archive_format == "gnu",
152+
src_archives: vec![],
153+
entries: vec![],
154+
})
155+
}
156+
157+
fn create_dll_import_lib(
158+
&self,
159+
_sess: &Session,
156160
_lib_name: &str,
157161
_dll_imports: &[rustc_session::cstore::DllImport],
158-
_tmpdir: &rustc_data_structures::temp_dir::MaybeTempDir,
159-
) {
162+
_tmpdir: &Path,
163+
) -> PathBuf {
160164
unimplemented!("injecting dll imports is not supported");
161165
}
162166
}

‎kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

Lines changed: 28 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
// Copyright Kani Contributors
22
// SPDX-License-Identifier: Apache-2.0 OR MIT
33
//! this module handles intrinsics
4-
use super::typ::pointee_type;
4+
use super::typ::{self, pointee_type};
55
use super::PropertyClass;
66
use crate::codegen_cprover_gotoc::GotocCtx;
77
use cbmc::goto_program::{
@@ -35,6 +35,11 @@ struct SizeAlign {
3535
align: Expr,
3636
}
3737

38+
enum VTableInfo {
39+
Size,
40+
Align,
41+
}
42+
3843
impl<'tcx> GotocCtx<'tcx> {
3944
fn binop<F: FnOnce(Expr, Expr) -> Expr>(
4045
&mut self,
@@ -703,6 +708,8 @@ impl<'tcx> GotocCtx<'tcx> {
703708
assert!(self.place_ty(p).is_unit());
704709
self.codegen_volatile_store(fargs, farg_types, loc)
705710
}
711+
"vtable_size" => self.vtable_info(VTableInfo::Size, fargs, p, loc),
712+
"vtable_align" => self.vtable_info(VTableInfo::Align, fargs, p, loc),
706713
"wrapping_add" => codegen_wrapping_op!(plus),
707714
"wrapping_mul" => codegen_wrapping_op!(mul),
708715
"wrapping_sub" => codegen_wrapping_op!(sub),
@@ -1201,6 +1208,26 @@ impl<'tcx> GotocCtx<'tcx> {
12011208
self.codegen_expr_to_place(p, e)
12021209
}
12031210

1211+
fn vtable_info(
1212+
&mut self,
1213+
info: VTableInfo,
1214+
mut fargs: Vec<Expr>,
1215+
place: &Place<'tcx>,
1216+
_loc: Location,
1217+
) -> Stmt {
1218+
assert_eq!(fargs.len(), 1, "vtable intrinsics expects one raw pointer argument");
1219+
let vtable_obj = fargs
1220+
.pop()
1221+
.unwrap()
1222+
.cast_to(self.codegen_ty_common_vtable().to_pointer())
1223+
.dereference();
1224+
let expr = match info {
1225+
VTableInfo::Size => vtable_obj.member(typ::VTABLE_SIZE_FIELD, &self.symbol_table),
1226+
VTableInfo::Align => vtable_obj.member(typ::VTABLE_ALIGN_FIELD, &self.symbol_table),
1227+
};
1228+
self.codegen_expr_to_place(place, expr)
1229+
}
1230+
12041231
/// This function computes the size and alignment of a dynamically-sized type.
12051232
/// The implementations follows closely the SSA implementation found in
12061233
/// rustc_codegen_ssa::glue::size_and_align_of_dst.

‎kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -379,6 +379,14 @@ impl<'tcx> GotocCtx<'tcx> {
379379
let name = format!("{}::{:?}", self.full_crate_name(), alloc_id);
380380
self.codegen_allocation(alloc.inner(), |_| name.clone(), Some(name.clone()))
381381
}
382+
GlobalAlloc::VTable(ty, trait_ref) => {
383+
// This is similar to GlobalAlloc::Memory but the type is opaque to rust and it
384+
// requires a bit more logic to get information about the allocation.
385+
let alloc_id = self.tcx.vtable_allocation((ty, trait_ref));
386+
let alloc = self.tcx.global_alloc(alloc_id).unwrap_memory();
387+
let name = format!("{}::{:?}", self.full_crate_name(), alloc_id);
388+
self.codegen_allocation(alloc.inner(), |_| name.clone(), Some(name.clone()))
389+
}
382390
};
383391
assert!(res_t.is_pointer() || res_t.is_transparent_type(&self.symbol_table));
384392
let offset_addr = base_addr

‎kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

Lines changed: 15 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
//! in [GotocCtx::codegen_place] below.
77
88
use super::typ::TypeExt;
9+
use crate::codegen_cprover_gotoc::codegen::typ::{pointee_type, std_pointee_type};
910
use crate::codegen_cprover_gotoc::utils::slice_fat_ptr;
1011
use crate::codegen_cprover_gotoc::GotocCtx;
1112
use cbmc::goto_program::{Expr, Location, Type};
@@ -360,31 +361,30 @@ impl<'tcx> GotocCtx<'tcx> {
360361
before.goto_expr
361362
};
362363

363-
let inner_mir_typ_and_mut = base_type.builtin_deref(true).unwrap();
364-
let fat_ptr_mir_typ = if self.is_box_of_unsized(base_type) {
365-
// If we have a box, its fat pointer typ is a pointer to the boxes inner type.
366-
Some(self.tcx.mk_ptr(inner_mir_typ_and_mut))
367-
} else if self.is_ref_of_unsized(base_type) {
368-
Some(before.mir_typ_or_variant.expect_type())
364+
let inner_mir_typ = std_pointee_type(base_type).unwrap();
365+
let (fat_ptr_mir_typ, fat_ptr_goto_expr) = if self.use_thin_pointer(inner_mir_typ) {
366+
(before.fat_ptr_mir_typ, before.fat_ptr_goto_expr)
369367
} else {
370-
before.fat_ptr_mir_typ
368+
(Some(before.mir_typ_or_variant.expect_type()), Some(inner_goto_expr.clone()))
371369
};
372-
let fat_ptr_goto_expr =
373-
if self.is_box_of_unsized(base_type) || self.is_ref_of_unsized(base_type) {
374-
Some(inner_goto_expr.clone())
375-
} else {
376-
before.fat_ptr_goto_expr
377-
};
378370

379371
// Check that we have a valid trait or slice fat pointer
380372
if let Some(fat_ptr) = fat_ptr_goto_expr.clone() {
381373
assert!(
382374
fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table)
383-
|| fat_ptr.typ().is_rust_slice_fat_ptr(&self.symbol_table)
375+
|| fat_ptr.typ().is_rust_slice_fat_ptr(&self.symbol_table),
376+
"Unexpected type: {:?} -- {:?}",
377+
fat_ptr.typ(),
378+
pointee_type(fat_ptr_mir_typ.unwrap()).unwrap().kind(),
379+
);
380+
assert!(
381+
self.use_fat_pointer(pointee_type(fat_ptr_mir_typ.unwrap()).unwrap()),
382+
"Unexpected type: {:?} -- {:?}",
383+
fat_ptr.typ(),
384+
fat_ptr_mir_typ,
384385
);
385386
};
386387

387-
let inner_mir_typ = inner_mir_typ_and_mut.ty;
388388
let expr = match inner_mir_typ.kind() {
389389
ty::Slice(_) | ty::Str | ty::Dynamic(..) => {
390390
inner_goto_expr.member("data", &self.symbol_table)
@@ -547,13 +547,6 @@ impl<'tcx> GotocCtx<'tcx> {
547547
self,
548548
)
549549
}
550-
ProjectionElem::OpaqueCast(ty) => ProjectedPlace::try_new(
551-
before.goto_expr.cast_to(self.codegen_ty(ty)),
552-
TypeOrVariant::Type(ty),
553-
before.fat_ptr_goto_expr,
554-
before.fat_ptr_mir_typ,
555-
self,
556-
),
557550
}
558551
}
559552

‎kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

Lines changed: 22 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ impl<'tcx> GotocCtx<'tcx> {
4343
let left_typ = self.operand_ty(left_op);
4444
let right_typ = self.operand_ty(left_op);
4545
assert_eq!(left_typ, right_typ, "Cannot compare pointers of different types");
46-
assert!(self.is_ref_of_unsized(left_typ));
46+
assert!(self.is_fat_pointer(left_typ));
4747

4848
if self.is_vtable_fat_pointer(left_typ) {
4949
// Codegen an assertion failure since vtable comparison is not stable.
@@ -334,7 +334,7 @@ impl<'tcx> GotocCtx<'tcx> {
334334
self.codegen_unchecked_scalar_binop(op, e1, e2)
335335
}
336336
BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => {
337-
if self.is_ref_of_unsized(self.operand_ty(e1)) {
337+
if self.is_fat_pointer(self.operand_ty(e1)) {
338338
self.codegen_comparison_fat_ptr(op, e1, e2, loc)
339339
} else {
340340
self.codegen_comparison(op, e1, e2)
@@ -628,11 +628,11 @@ impl<'tcx> GotocCtx<'tcx> {
628628
}
629629

630630
// Cast between fat pointers
631-
if self.is_ref_of_unsized(src_t) && self.is_ref_of_unsized(dst_t) {
631+
if self.is_fat_pointer(src_t) && self.is_fat_pointer(dst_t) {
632632
return self.codegen_fat_ptr_to_fat_ptr_cast(src, dst_t);
633633
}
634634

635-
if self.is_ref_of_unsized(src_t) && self.is_ref_of_sized(dst_t) {
635+
if self.is_fat_pointer(src_t) && !self.is_fat_pointer(dst_t) {
636636
return self.codegen_fat_ptr_to_thin_ptr_cast(src, dst_t);
637637
}
638638

@@ -760,14 +760,9 @@ impl<'tcx> GotocCtx<'tcx> {
760760
dst_mir_type,
761761
)
762762
} else {
763-
// Check that the source is either not a pointer, or a thin or a slice pointer
764-
assert!(
765-
pointee_type(src_mir_type)
766-
.map_or(true, |p| self.use_thin_pointer(p) || self.use_slice_fat_pointer(p))
767-
);
768-
769-
// Sized to unsized cast
770-
self.cast_sized_expr_to_unsized_expr(src_goto_expr, src_mir_type, dst_mir_type)
763+
// Recursively cast the source expression into an unsized expression.
764+
// This will include thin pointers, slices, and Adt.
765+
self.cast_expr_to_unsized_expr(src_goto_expr, src_mir_type, dst_mir_type)
771766
}
772767
}
773768

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

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

1057-
// The src type will be sized, but the dst type may not be unsized. If
1058-
// the dst is an adt containing a pointer to a trait object nested
1059-
// within the adt, the trait object will be unsized and the pointer will
1060-
// be a fat pointer, but the adt (containing the fat pointer) will
1061-
// itself be sized.
1062-
assert!(
1063-
src_mir_type.is_sized(self.tcx.at(rustc_span::DUMMY_SP), ty::ParamEnv::reveal_all())
1064-
);
1065-
1066-
// The src type cannot be a pointer to a dynamic trait object, otherwise
1067-
// we should have called cast_unsized_dyn_trait_to_unsized_dyn_trait
1068-
assert!(!self.is_vtable_fat_pointer(src_mir_type));
1069-
10701051
match (src_mir_type.kind(), dst_mir_type.kind()) {
10711052
(ty::Ref(..), ty::Ref(..)) => {
10721053
self.cast_sized_pointer_to_fat_pointer(src_goto_expr, src_mir_type, dst_mir_type)
@@ -1081,7 +1062,7 @@ impl<'tcx> GotocCtx<'tcx> {
10811062
self.cast_sized_pointer_to_fat_pointer(src_goto_expr, src_mir_type, dst_mir_type)
10821063
}
10831064
(ty::Adt(..), ty::Adt(..)) => {
1084-
self.cast_sized_adt_to_unsized_adt(src_goto_expr, src_mir_type, dst_mir_type)
1065+
self.cast_adt_to_unsized_adt(src_goto_expr, src_mir_type, dst_mir_type)
10851066
}
10861067
(src_kind, dst_kind) => {
10871068
unreachable!(
@@ -1095,6 +1076,11 @@ impl<'tcx> GotocCtx<'tcx> {
10951076
/// Cast a pointer to a sized object to a fat pointer to an unsized object.
10961077
/// Return the result of the cast as Some(expr) and return None if no cast
10971078
/// was required.
1079+
/// Note: This seems conceptually wrong. If we are converting sized to unsized, how come
1080+
/// source and destination can have the same type? Also, how come destination can be a thin
1081+
/// pointer?
1082+
/// TODO: Fix the cast code structure:
1083+
/// <https://github.com/model-checking/kani/issues/1531>
10981084
fn cast_sized_pointer_to_fat_pointer(
10991085
&mut self,
11001086
src_goto_expr: Expr,
@@ -1106,6 +1092,10 @@ impl<'tcx> GotocCtx<'tcx> {
11061092
return None;
11071093
};
11081094

1095+
// The src type cannot be a pointer to a dynamic trait object, otherwise
1096+
// we should have called cast_unsized_dyn_trait_to_unsized_dyn_trait
1097+
assert!(!self.is_vtable_fat_pointer(src_mir_type));
1098+
11091099
// extract pointee types from pointer types, panic if type is not a
11101100
// pointer type.
11111101
let src_pointee_type = pointee_type(src_mir_type).unwrap();
@@ -1192,10 +1182,10 @@ impl<'tcx> GotocCtx<'tcx> {
11921182
}
11931183
}
11941184

1195-
/// Cast a sized ADT to an unsized ADT (an ADT with a nested fat pointer).
1185+
/// Cast an ADT (sized or unsized) to an unsized ADT (an ADT with a nested fat pointer).
11961186
/// Return the result of the cast as Some(expr) and return None if no cast
11971187
/// was required.
1198-
fn cast_sized_adt_to_unsized_adt(
1188+
fn cast_adt_to_unsized_adt(
11991189
&mut self,
12001190
src_goto_expr: Expr,
12011191
src_mir_type: Ty<'tcx>,

‎kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -595,7 +595,7 @@ impl<'tcx> GotocCtx<'tcx> {
595595
| InstanceDef::DropGlue(_, Some(_))
596596
| InstanceDef::Intrinsic(..)
597597
| InstanceDef::FnPtrShim(..)
598-
| InstanceDef::VtableShim(..)
598+
| InstanceDef::VTableShim(..)
599599
| InstanceDef::ReifyShim(..)
600600
| InstanceDef::ClosureOnceShim { .. }
601601
| InstanceDef::CloneShim(..) => {

0 commit comments

Comments
 (0)