From 2b6be2efea6680b3cbe804f7b128620d787a846f Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 12 Jan 2022 15:06:57 -0800 Subject: [PATCH 1/4] Update rust toolchain version Fixes #747. --- src/rmc-compiler/rust-toolchain.toml | 2 +- .../rustc_codegen_rmc/src/codegen/rvalue.rs | 13 ------------- .../rustc_codegen_rmc/src/codegen/typ.rs | 6 +++--- 3 files changed, 4 insertions(+), 17 deletions(-) diff --git a/src/rmc-compiler/rust-toolchain.toml b/src/rmc-compiler/rust-toolchain.toml index d2f7ab63d7ea..042944dfeef7 100644 --- a/src/rmc-compiler/rust-toolchain.toml +++ b/src/rmc-compiler/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2021-12-27" +channel = "nightly-2022-01-11" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/rvalue.rs b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/rvalue.rs index 0eb7b93e7db1..759c32a701ab 100644 --- a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/rvalue.rs +++ b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/rvalue.rs @@ -381,24 +381,11 @@ impl<'tcx> GotocCtx<'tcx> { Rvalue::CheckedBinaryOp(op, box (ref e1, ref e2)) => { self.codegen_rvalue_checked_binary_op(op, e1, e2, res_ty) } - Rvalue::NullaryOp(NullOp::Box, t) => { - let t = self.monomorphize(*t); - let layout = self.layout_of(t); - let size = layout.size.bytes_usize(); - let box_ty = self.tcx.mk_box(t); - let box_ty = self.codegen_ty(box_ty); - let cbmc_t = self.codegen_ty(t); - let box_contents = BuiltinFn::Malloc - .call(vec![Expr::int_constant(size, Type::size_t())], Location::none()) - .cast_to(cbmc_t.to_pointer()); - self.box_value(box_contents, box_ty) - } Rvalue::NullaryOp(k, t) => { let t = self.monomorphize(*t); let layout = self.layout_of(t); match k { NullOp::SizeOf => Expr::int_constant(layout.size.bytes_usize(), Type::size_t()), - NullOp::Box => unreachable!("Should've matched previous expression"), NullOp::AlignOf => Expr::int_constant(layout.align.abi.bytes(), Type::size_t()), } } diff --git a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs index 149297b27a65..2a83ab6673e2 100644 --- a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs +++ b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs @@ -1297,15 +1297,15 @@ impl<'tcx> GotocCtx<'tcx> { pub fn use_thin_pointer(&self, mir_type: Ty<'tcx>) -> bool { // ptr_metadata_ty is not defined on all types, the projection of an associated type return !self.is_unsized(mir_type) - || mir_type.ptr_metadata_ty(self.tcx) == self.tcx.types.unit; + || mir_type.ptr_metadata_ty(self.tcx, |ty| ty) == self.tcx.types.unit; } /// A pointer to the mir type should be a slice fat pointer. pub fn use_slice_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool { - return mir_type.ptr_metadata_ty(self.tcx) == self.tcx.types.usize; + return mir_type.ptr_metadata_ty(self.tcx, |ty| ty) == self.tcx.types.usize; } /// A pointer to the mir type should be a vtable fat pointer. pub fn use_vtable_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool { - let metadata = mir_type.ptr_metadata_ty(self.tcx); + let metadata = mir_type.ptr_metadata_ty(self.tcx, |ty| ty); return metadata != self.tcx.types.unit && metadata != self.tcx.types.usize; } From 078c4acd1e8589510f2bf7d3d29f42453668abd9 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 13 Jan 2022 13:29:32 -0800 Subject: [PATCH 2/4] Update typ.rs Add a TODO and a link to the issue. --- src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs index 2a83ab6673e2..74788340751d 100644 --- a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs +++ b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs @@ -1296,6 +1296,8 @@ impl<'tcx> GotocCtx<'tcx> { /// A pointer to the mir type should be a thin pointer. pub fn use_thin_pointer(&self, mir_type: Ty<'tcx>) -> bool { // ptr_metadata_ty is not defined on all types, the projection of an associated type + // TODO: We should normalize the type projection here. For more details, see + // https://github.com/model-checking/rmc/issues/752 return !self.is_unsized(mir_type) || mir_type.ptr_metadata_ty(self.tcx, |ty| ty) == self.tcx.types.unit; } From 0a7905f40aa43d38bf872e25fa244cbe403b69e7 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 17 Jan 2022 10:35:23 -0800 Subject: [PATCH 3/4] Add a placeholder for type normalization function In order to make it easier to read and implement in the future. --- .../rustc_codegen_rmc/src/codegen/typ.rs | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs index 74788340751d..9e932b9d53a0 100644 --- a/src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs +++ b/src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs @@ -1292,22 +1292,28 @@ pub fn is_repr_c_adt(mir_type: Ty<'tcx>) -> bool { } } +/// This is a place holder function that should normalize the given type. +/// +/// TODO: We should normalize the type projection here. For more details, see +/// https://github.com/model-checking/rmc/issues/752 +fn normalize_type(ty: Ty<'tcx>) -> Ty<'tcx> { + ty +} + impl<'tcx> GotocCtx<'tcx> { /// A pointer to the mir type should be a thin pointer. pub fn use_thin_pointer(&self, mir_type: Ty<'tcx>) -> bool { // ptr_metadata_ty is not defined on all types, the projection of an associated type - // TODO: We should normalize the type projection here. For more details, see - // https://github.com/model-checking/rmc/issues/752 return !self.is_unsized(mir_type) - || mir_type.ptr_metadata_ty(self.tcx, |ty| ty) == self.tcx.types.unit; + || mir_type.ptr_metadata_ty(self.tcx, normalize_type) == self.tcx.types.unit; } /// A pointer to the mir type should be a slice fat pointer. pub fn use_slice_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool { - return mir_type.ptr_metadata_ty(self.tcx, |ty| ty) == self.tcx.types.usize; + return mir_type.ptr_metadata_ty(self.tcx, normalize_type) == self.tcx.types.usize; } /// A pointer to the mir type should be a vtable fat pointer. pub fn use_vtable_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool { - let metadata = mir_type.ptr_metadata_ty(self.tcx, |ty| ty); + let metadata = mir_type.ptr_metadata_ty(self.tcx, normalize_type); return metadata != self.tcx.types.unit && metadata != self.tcx.types.usize; } From 9d4a26de28ca0e7dae5003a9426227430e46e7ff Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 17 Jan 2022 10:53:21 -0800 Subject: [PATCH 4/4] Remove the LOC of the expected failure 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. --- .../src/tutorial/arbitrary-variables/unsafe_update.expected | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rmc-docs/src/tutorial/arbitrary-variables/unsafe_update.expected b/rmc-docs/src/tutorial/arbitrary-variables/unsafe_update.expected index 2b5fe7d7d56b..86776cb39a55 100644 --- a/rmc-docs/src/tutorial/arbitrary-variables/unsafe_update.expected +++ b/rmc-docs/src/tutorial/arbitrary-variables/unsafe_update.expected @@ -1,3 +1,3 @@ [inventory::verification::unsafe_update.assertion.1] line 61 assertion failed: inventory.get(&id).unwrap() == quantity: SUCCESS -[std::option::Option::::unwrap.assertion.1] line 759 called `Option::unwrap()` on a `None` value: FAILURE +called `Option::unwrap()` on a `None` value: FAILURE VERIFICATION FAILED