Skip to content

Commit 7fa93b2

Browse files
celinvaltedinski
authored andcommitted
Update rust toolchain version (model-checking#750)
Fixes model-checking#747. * Update typ.rs. Add a placeholder for type normalization function to make it easier to read and implement in the future. * Remove the LOC of expected failure on std function. This exact line where the assertion is may change whenever we update the rust toolchain, which makes this test unreliable. We still ensure that the assertion fails. Note that this may still fail if the message or the check gets updated, but this shouldn't happen frequently.
1 parent 84b8314 commit 7fa93b2

File tree

4 files changed

+13
-18
lines changed

4 files changed

+13
-18
lines changed
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
11
[inventory::verification::unsafe_update.assertion.1] line 61 assertion failed: inventory.get(&id).unwrap() == quantity: SUCCESS
2-
[std::option::Option::<T>::unwrap.assertion.1] line 759 called `Option::unwrap()` on a `None` value: FAILURE
2+
called `Option::unwrap()` on a `None` value: FAILURE
33
VERIFICATION FAILED

src/rmc-compiler/rust-toolchain.toml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,5 +2,5 @@
22
# SPDX-License-Identifier: Apache-2.0 OR MIT
33

44
[toolchain]
5-
channel = "nightly-2021-12-27"
5+
channel = "nightly-2022-01-11"
66
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

src/rmc-compiler/rustc_codegen_rmc/src/codegen/rvalue.rs

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -381,24 +381,11 @@ impl<'tcx> GotocCtx<'tcx> {
381381
Rvalue::CheckedBinaryOp(op, box (ref e1, ref e2)) => {
382382
self.codegen_rvalue_checked_binary_op(op, e1, e2, res_ty)
383383
}
384-
Rvalue::NullaryOp(NullOp::Box, t) => {
385-
let t = self.monomorphize(*t);
386-
let layout = self.layout_of(t);
387-
let size = layout.size.bytes_usize();
388-
let box_ty = self.tcx.mk_box(t);
389-
let box_ty = self.codegen_ty(box_ty);
390-
let cbmc_t = self.codegen_ty(t);
391-
let box_contents = BuiltinFn::Malloc
392-
.call(vec![Expr::int_constant(size, Type::size_t())], Location::none())
393-
.cast_to(cbmc_t.to_pointer());
394-
self.box_value(box_contents, box_ty)
395-
}
396384
Rvalue::NullaryOp(k, t) => {
397385
let t = self.monomorphize(*t);
398386
let layout = self.layout_of(t);
399387
match k {
400388
NullOp::SizeOf => Expr::int_constant(layout.size.bytes_usize(), Type::size_t()),
401-
NullOp::Box => unreachable!("Should've matched previous expression"),
402389
NullOp::AlignOf => Expr::int_constant(layout.align.abi.bytes(), Type::size_t()),
403390
}
404391
}

src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1292,20 +1292,28 @@ pub fn is_repr_c_adt(mir_type: Ty<'tcx>) -> bool {
12921292
}
12931293
}
12941294

1295+
/// This is a place holder function that should normalize the given type.
1296+
///
1297+
/// TODO: We should normalize the type projection here. For more details, see
1298+
/// https://github.com/model-checking/rmc/issues/752
1299+
fn normalize_type(ty: Ty<'tcx>) -> Ty<'tcx> {
1300+
ty
1301+
}
1302+
12951303
impl<'tcx> GotocCtx<'tcx> {
12961304
/// A pointer to the mir type should be a thin pointer.
12971305
pub fn use_thin_pointer(&self, mir_type: Ty<'tcx>) -> bool {
12981306
// ptr_metadata_ty is not defined on all types, the projection of an associated type
12991307
return !self.is_unsized(mir_type)
1300-
|| mir_type.ptr_metadata_ty(self.tcx) == self.tcx.types.unit;
1308+
|| mir_type.ptr_metadata_ty(self.tcx, normalize_type) == self.tcx.types.unit;
13011309
}
13021310
/// A pointer to the mir type should be a slice fat pointer.
13031311
pub fn use_slice_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool {
1304-
return mir_type.ptr_metadata_ty(self.tcx) == self.tcx.types.usize;
1312+
return mir_type.ptr_metadata_ty(self.tcx, normalize_type) == self.tcx.types.usize;
13051313
}
13061314
/// A pointer to the mir type should be a vtable fat pointer.
13071315
pub fn use_vtable_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool {
1308-
let metadata = mir_type.ptr_metadata_ty(self.tcx);
1316+
let metadata = mir_type.ptr_metadata_ty(self.tcx, normalize_type);
13091317
return metadata != self.tcx.types.unit && metadata != self.tcx.types.usize;
13101318
}
13111319

0 commit comments

Comments
 (0)