Skip to content

Commit

Permalink
Upgrade toolchain to 2024-02-14 (rust-lang#3036)
Browse files Browse the repository at this point in the history
Upgrade toolchain to 2024-02-17. Relevant PRs:

rust-lang#120872

rust-lang#120594

Resolves rust-lang#3028 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
  • Loading branch information
zhassan-aws authored Feb 20, 2024
1 parent 9fae67a commit 72fd9f4
Show file tree
Hide file tree
Showing 8 changed files with 38 additions and 26 deletions.
12 changes: 7 additions & 5 deletions cprover_bindings/src/goto_program/builtin.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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",
Expand Down Expand Up @@ -129,8 +131,8 @@ impl ToString for BuiltinFn {
Trunc => "trunc",
Truncf => "truncf",
Unlink => "unlink",
}
.to_string()
};
write!(f, "{func}")
}
}

Expand Down
15 changes: 8 additions & 7 deletions cprover_bindings/src/goto_program/symbol.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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:
/// <https://github.com/diffblue/cbmc/blob/develop/src/util/symbol.h>
#[derive(Clone, Debug)]
Expand Down Expand Up @@ -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}")
}
}
20 changes: 13 additions & 7 deletions cprover_bindings/src/irep/irep_id.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -1708,7 +1714,7 @@ impl ToString for IrepId {
IrepId::VectorGt => "vector->",
IrepId::VectorLt => "vector-<",
};
s.to_string()
write!(f, "{s}")
}
}

Expand Down
1 change: 1 addition & 0 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
Original file line number Diff line number Diff line change
Expand Up @@ -725,6 +725,7 @@ impl<'tcx> GotocCtx<'tcx> {
.bytes(),
Type::size_t(),
),
NullOp::DebugAssertions => Expr::c_false(),
}
}
Rvalue::ShallowInitBox(ref operand, content_ty) => {
Expand Down
10 changes: 6 additions & 4 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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
}

Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/kani_middle/attributes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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) => {
Expand Down
2 changes: 1 addition & 1 deletion rust-toolchain.toml
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-2024-02-09"
channel = "nightly-2024-02-14"
components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
Original file line number Diff line number Diff line change
@@ -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-

0 comments on commit 72fd9f4

Please sign in to comment.