Skip to content

Update rust toolchain version #750

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Jan 17, 2022
Merged

Update rust toolchain version #750

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
2b6be2e
Update rust toolchain version
celinval Jan 12, 2022
078c4ac
Update typ.rs
celinval Jan 13, 2022
0a7905f
Add a placeholder for type normalization function
celinval Jan 17, 2022
9d4a26d
Remove the LOC of the expected failure
celinval Jan 17, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion rmc-docs/src/tutorial/arbitrary-variables/unsafe_update.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
[inventory::verification::unsafe_update.assertion.1] line 61 assertion failed: inventory.get(&id).unwrap() == quantity: SUCCESS
[std::option::Option::<T>::unwrap.assertion.1] line 759 called `Option::unwrap()` on a `None` value: FAILURE
called `Option::unwrap()` on a `None` value: FAILURE
VERIFICATION FAILED
2 changes: 1 addition & 1 deletion src/rmc-compiler/rust-toolchain.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"]
13 changes: 0 additions & 13 deletions src/rmc-compiler/rustc_codegen_rmc/src/codegen/rvalue.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
}
Comment on lines -384 to -395
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why this change?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This NullOp::Box had deprecated and replaced by ShallowInitBox. So they finally removed it.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

rust-lang/rust@57a4f4a

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()),
}
}
Expand Down
14 changes: 11 additions & 3 deletions src/rmc-compiler/rustc_codegen_rmc/src/codegen/typ.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1292,20 +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
return !self.is_unsized(mir_type)
|| mir_type.ptr_metadata_ty(self.tcx) == 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) == 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);
let metadata = mir_type.ptr_metadata_ty(self.tcx, normalize_type);
return metadata != self.tcx.types.unit && metadata != self.tcx.types.usize;
}

Expand Down