From 72fd9f4fb541bda217ac42c0c8d639d63f640b46 Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Tue, 20 Feb 2024 11:03:06 -0800 Subject: [PATCH] Upgrade toolchain to 2024-02-14 (#3036) Upgrade toolchain to 2024-02-17. Relevant PRs: https://github.com/rust-lang/rust/pull/120872 https://github.com/rust-lang/rust/pull/120594 Resolves #3028 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- cprover_bindings/src/goto_program/builtin.rs | 12 ++++++----- cprover_bindings/src/goto_program/symbol.rs | 15 +++++++------- cprover_bindings/src/irep/irep_id.rs | 20 ++++++++++++------- .../codegen_cprover_gotoc/codegen/rvalue.rs | 1 + .../src/codegen_cprover_gotoc/codegen/typ.rs | 10 ++++++---- kani-compiler/src/kani_middle/attributes.rs | 2 +- rust-toolchain.toml | 2 +- .../playback_opts.expected | 2 +- 8 files changed, 38 insertions(+), 26 deletions(-) diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs index 438bc2eea1e9..a0c1f211b5e2 100644 --- a/cprover_bindings/src/goto_program/builtin.rs +++ b/cprover_bindings/src/goto_program/builtin.rs @@ -4,6 +4,8 @@ use self::BuiltinFn::*; use super::{Expr, Location, Symbol, Type}; +use std::fmt::Display; + #[derive(Debug, Clone, Copy)] pub enum BuiltinFn { Abort, @@ -67,9 +69,9 @@ pub enum BuiltinFn { Unlink, } -impl ToString for BuiltinFn { - fn to_string(&self) -> String { - match self { +impl Display for BuiltinFn { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let func = match self { Abort => "abort", Assert => "assert", CProverAssume => "__CPROVER_assume", @@ -129,8 +131,8 @@ impl ToString for BuiltinFn { Trunc => "trunc", Truncf => "truncf", Unlink => "unlink", - } - .to_string() + }; + write!(f, "{func}") } } diff --git a/cprover_bindings/src/goto_program/symbol.rs b/cprover_bindings/src/goto_program/symbol.rs index b1082a8f1f80..ad71b0f84346 100644 --- a/cprover_bindings/src/goto_program/symbol.rs +++ b/cprover_bindings/src/goto_program/symbol.rs @@ -4,6 +4,8 @@ use super::super::utils::aggr_tag; use super::{DatatypeComponent, Expr, Location, Parameter, Stmt, Type}; use crate::{InternStringOption, InternedString}; +use std::fmt::Display; + /// Based off the CBMC symbol implementation here: /// #[derive(Clone, Debug)] @@ -452,14 +454,13 @@ impl SymbolValues { } } -/// ToString - -impl ToString for SymbolModes { - fn to_string(&self) -> String { - match self { +/// Display +impl Display for SymbolModes { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let mode = match self { SymbolModes::C => "C", SymbolModes::Rust => "Rust", - } - .to_string() + }; + write!(f, "{mode}") } } diff --git a/cprover_bindings/src/irep/irep_id.rs b/cprover_bindings/src/irep/irep_id.rs index cad6eb563bf4..119aecb8887c 100644 --- a/cprover_bindings/src/irep/irep_id.rs +++ b/cprover_bindings/src/irep/irep_id.rs @@ -8,6 +8,8 @@ use crate::cbmc_string::InternedString; use crate::utils::NumUtils; use num::bigint::{BigInt, BigUint, Sign}; +use std::fmt::Display; + #[derive(PartialEq, Eq, PartialOrd, Ord, Clone, Debug)] pub enum IrepId { /// In addition to the standard enums defined below, CBMC also allows ids to be strings. @@ -872,15 +874,19 @@ impl IrepId { } } -impl ToString for IrepId { - fn to_string(&self) -> String { +impl Display for IrepId { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { - IrepId::FreeformString(s) => return s.to_string(), - IrepId::FreeformInteger(i) => return i.to_string(), + IrepId::FreeformString(s) => { + return write!(f, "{s}"); + } + IrepId::FreeformInteger(i) => { + return write!(f, "{i}"); + } IrepId::FreeformBitPattern(i) => { - return format!("{i:X}"); + return write!(f, "{i:X}"); } - _ => (), + _ => {} } let s = match self { @@ -1708,7 +1714,7 @@ impl ToString for IrepId { IrepId::VectorGt => "vector->", IrepId::VectorLt => "vector-<", }; - s.to_string() + write!(f, "{s}") } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index e7501df3aac4..3df6d807aaea 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -725,6 +725,7 @@ impl<'tcx> GotocCtx<'tcx> { .bytes(), Type::size_t(), ), + NullOp::DebugAssertions => Expr::c_false(), } } Rvalue::ShallowInitBox(ref operand, content_ty) => { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index c988636a390f..b0e3c115d597 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1714,8 +1714,10 @@ impl<'tcx> GotocCtx<'tcx> { /// metadata associated with it. 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 - let (metadata, _check_is_sized) = mir_type.ptr_metadata_ty(self.tcx, normalize_type); - !self.is_unsized(mir_type) || metadata == self.tcx.types.unit + let metadata = mir_type.ptr_metadata_ty_or_tail(self.tcx, normalize_type); + !self.is_unsized(mir_type) + || metadata.is_err() + || (metadata.unwrap() == self.tcx.types.unit) } /// We use fat pointer if not thin pointer. @@ -1726,14 +1728,14 @@ impl<'tcx> GotocCtx<'tcx> { /// A pointer to the mir type should be a slice fat pointer. /// We use a slice fat pointer if the metadata is the slice length (type usize). pub fn use_slice_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool { - let (metadata, _check_is_sized) = mir_type.ptr_metadata_ty(self.tcx, normalize_type); + let metadata = mir_type.ptr_metadata_ty(self.tcx, normalize_type); metadata == self.tcx.types.usize } /// A pointer to the mir type should be a vtable fat pointer. /// We use a vtable fat pointer if this is a fat pointer to anything that is not a slice ptr. /// I.e.: The metadata is not length (type usize). pub fn use_vtable_fat_pointer(&self, mir_type: Ty<'tcx>) -> bool { - let (metadata, _check_is_sized) = mir_type.ptr_metadata_ty(self.tcx, normalize_type); + let metadata = mir_type.ptr_metadata_ty(self.tcx, normalize_type); metadata != self.tcx.types.unit && metadata != self.tcx.types.usize } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 32425204d76a..621107acd13e 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -268,7 +268,7 @@ impl<'tcx> KaniAttributes<'tcx> { .hir_id() }; - let result = match hir_map.get_parent(hir_id) { + let result = match self.tcx.parent_hir_node(hir_id) { Node::Item(Item { kind, .. }) => match kind { ItemKind::Mod(m) => find_in_mod(m), ItemKind::Impl(imp) => { diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 9d93e7382952..42bd4779102f 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2024-02-09" +channel = "nightly-2024-02-14" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/script-based-pre/cargo_playback_opts/playback_opts.expected b/tests/script-based-pre/cargo_playback_opts/playback_opts.expected index 68b7daa3ee03..b68f0b355029 100644 --- a/tests/script-based-pre/cargo_playback_opts/playback_opts.expected +++ b/tests/script-based-pre/cargo_playback_opts/playback_opts.expected @@ -1,6 +1,6 @@ [TEST] Only codegen test... Executable unittests src/lib.rs [TEST] Only codegen test... - Finished test + Finished `test` [TEST] Executable debug/deps/sample_crate-