Upgrade toolchain to 2024-02-14

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}")
     }
 }
 

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:
 /// <https://github.com/diffblue/cbmc/blob/develop/src/util/symbol.h>
 #[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}")
     }
 }

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}")
     }
 }
 

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) => {

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
     }
 

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) => {

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"]

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-