Upgrade Rust toolchain to nightly-2024-03-29

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -725,7 +725,7 @@ impl<'tcx> GotocCtx<'tcx> {
                             .bytes(),
                         Type::size_t(),
                     ),
-                    NullOp::UbCheck(_) => Expr::c_false(),
+                    NullOp::UbChecks => Expr::c_false(),
                 }
             }
             Rvalue::ShallowInitBox(ref operand, content_ty) => {

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -570,7 +570,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // Note: This is not valid C but CBMC seems to be ok with it.
             ty::Slice(e) => self.codegen_ty(*e).flexible_array_of(),
             ty::Str => Type::unsigned_int(8).flexible_array_of(),
-            ty::Ref(_, t, _) | ty::RawPtr(ty::TypeAndMut { ty: t, .. }) => self.codegen_ty_ref(*t),
+            ty::Ref(_, t, _) | ty::RawPtr(t, _) => self.codegen_ty_ref(*t),
             ty::FnDef(def_id, args) => {
                 let instance =
                     Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
@@ -993,7 +993,7 @@ impl<'tcx> GotocCtx<'tcx> {
             | ty::Foreign(_)
             | ty::Coroutine(..)
             | ty::Int(_)
-            | ty::RawPtr(_)
+            | ty::RawPtr(_, _)
             | ty::Ref(..)
             | ty::Tuple(_)
             | ty::Uint(_) => self.codegen_ty(pointee_type).to_pointer(),
@@ -1352,10 +1352,7 @@ impl<'tcx> GotocCtx<'tcx> {
             // `F16` and `F128` are not yet handled.
             // Tracked here: <https://github.com/model-checking/kani/issues/3069>
             Primitive::F16 | Primitive::F128 => unimplemented!(),
-            Primitive::Pointer(_) => Ty::new_ptr(
-                self.tcx,
-                ty::TypeAndMut { ty: self.tcx.types.u8, mutbl: Mutability::Not },
-            ),
+            Primitive::Pointer(_) => Ty::new_ptr(self.tcx, self.tcx.types.u8, Mutability::Not),
         }
     }
 
@@ -1659,7 +1656,7 @@ fn common_vtable_fields(drop_in_place: Type) -> Vec<DatatypeComponent> {
 pub fn pointee_type(mir_type: Ty) -> Option<Ty> {
     match mir_type.kind() {
         ty::Ref(_, pointee_type, _) => Some(*pointee_type),
-        ty::RawPtr(ty::TypeAndMut { ty: pointee_type, .. }) => Some(*pointee_type),
+        ty::RawPtr(pointee_type, _) => Some(*pointee_type),
         _ => None,
     }
 }

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -23,7 +23,6 @@ use crate::kani_queries::QueryDb;
 use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type};
 use cbmc::utils::aggr_tag;
 use cbmc::{InternedString, MachineModel};
-use kani_metadata::HarnessMetadata;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::span_bug;
 use rustc_middle::ty::layout::{
@@ -61,8 +60,6 @@ pub struct GotocCtx<'tcx> {
     /// map from symbol identifier to string literal
     /// TODO: consider making the map from Expr to String instead
     pub str_literals: FxHashMap<InternedString, String>,
-    pub proof_harnesses: Vec<HarnessMetadata>,
-    pub test_harnesses: Vec<HarnessMetadata>,
     /// a global counter for generating unique IDs for checks
     pub global_checks_count: u64,
     /// A map of unsupported constructs that were found while codegen
@@ -98,8 +95,6 @@ impl<'tcx> GotocCtx<'tcx> {
             current_fn: None,
             type_map: FxHashMap::default(),
             str_literals: FxHashMap::default(),
-            proof_harnesses: vec![],
-            test_harnesses: vec![],
             global_checks_count: 0,
             unsupported_constructs: FxHashMap::default(),
             concurrent_constructs: FxHashMap::default(),

kani-compiler/src/kani_middle/mod.rs

@@ -22,7 +22,6 @@ use rustc_span::Span;
 use rustc_target::abi::call::FnAbi;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
 use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem};
-use stable_mir::mir::pretty::pretty_ty;
 use stable_mir::ty::{BoundVariableKind, FnDef, RigidTy, Span as SpanStable, Ty, TyKind};
 use stable_mir::visitor::{Visitable, Visitor as TypeVisitor};
 use stable_mir::{CrateDef, DefId};
@@ -48,7 +47,7 @@ pub mod transform;
 /// error was found.
 pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) {
     let krate = tcx.crate_name(LOCAL_CRATE);
-    for item in tcx.hir_crate_items(()).items() {
+    for item in tcx.hir().items() {
         let def_id = item.owner_id.def_id.to_def_id();
         KaniAttributes::for_item(tcx, def_id).check_attributes();
         if tcx.def_kind(def_id) == DefKind::GlobalAsm {
@@ -129,7 +128,7 @@ fn check_is_contract_safe(tcx: TyCtxt, instance: Instance) {
                 self.tcx.dcx().err(format!(
                     "{} contains a {}pointer ({}). This is prohibited for functions with contracts, \
                     as they cannot yet reason about the pointer behavior.", self.r#where, self.what,
-                    pretty_ty(ty.kind())));
+                    ty));
             }
 
             // Rust's type visitor only recurses into type arguments, (e.g.
@@ -227,20 +226,16 @@ pub fn dump_mir_items(tcx: TyCtxt, items: &[MonoItem], output: &Path) {
 pub struct SourceLocation {
     pub filename: String,
     pub start_line: usize,
-    pub start_col: usize,
     pub end_line: usize,
-    pub end_col: usize,
 }
 
 impl SourceLocation {
     pub fn new(span: SpanStable) -> Self {
         let loc = span.get_lines();
         let filename = span.get_filename().to_string();
         let start_line = loc.start_line;
-        let start_col = loc.start_col;
         let end_line = loc.end_line;
-        let end_col = loc.end_col;
-        SourceLocation { filename, start_line, start_col, end_line, end_col }
+        SourceLocation { filename, start_line, end_line }
     }
 }
 

kani-compiler/src/kani_middle/reachability.rs

@@ -25,7 +25,6 @@ use rustc_middle::ty::{TyCtxt, VtblEntry};
 use rustc_smir::rustc_internal;
 use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
 use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef};
-use stable_mir::mir::pretty::pretty_ty;
 use stable_mir::mir::{
     visit::Location, Body, CastKind, Constant, MirVisitor, PointerCoercion, Rvalue, Terminator,
     TerminatorKind,
@@ -433,7 +432,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
                                         `{}`. The function `{}` \
                                         cannot be stubbed by `{}` due to \
                                         generic bounds not being met. Callee: {}",
-                                        pretty_ty(receiver_ty.kind()),
+                                        receiver_ty,
                                         trait_,
                                         caller,
                                         self.tcx.def_path_str(stub),

kani-compiler/src/kani_middle/transform/body.rs

@@ -231,7 +231,7 @@ pub enum CheckType {
     /// This is used by default when the `kani` crate is available.
     Assert(Instance),
     /// When the `kani` crate is not available, we have to model the check as an `if { panic!() }`.
-    Panic(Instance),
+    Panic(),
     /// When building non-core crate, such as `rustc-std-workspace-core`, we cannot
     /// instrument code, but we can still compile them.
     NoCore,
@@ -246,8 +246,8 @@ impl CheckType {
     pub fn new(tcx: TyCtxt) -> CheckType {
         if let Some(instance) = find_instance(tcx, "KaniAssert") {
             CheckType::Assert(instance)
-        } else if let Some(instance) = find_instance(tcx, "panic_str") {
-            CheckType::Panic(instance)
+        } else if let Some(_) = find_instance(tcx, "panic_str") {
+            CheckType::Panic()
         } else {
             CheckType::NoCore
         }

kani-driver/src/call_cbmc.rs

@@ -11,7 +11,7 @@ use std::time::{Duration, Instant};
 
 use crate::args::{OutputFormat, VerificationArgs};
 use crate::cbmc_output_parser::{
-    extract_results, process_cbmc_output, CheckStatus, ParserItem, Property, VerificationOutput,
+    extract_results, process_cbmc_output, CheckStatus, Property, VerificationOutput,
 };
 use crate::cbmc_property_renderer::{format_coverage, format_result, kani_cbmc_output_filter};
 use crate::session::KaniSession;
@@ -45,9 +45,6 @@ pub struct VerificationResult {
     pub status: VerificationStatus,
     /// The compact representation for failed properties
     pub failed_properties: FailedProperties,
-    /// The parsed output, message by message, of CBMC. However, the `Result` message has been
-    /// removed and is available in `results` instead.
-    pub messages: Option<Vec<ParserItem>>,
     /// The `Result` properties in detail or the exit_status of CBMC.
     /// Note: CBMC process exit status is only potentially useful if `status` is `Failure`.
     /// Kani will see CBMC report "failure" that's actually success (interpreting "failed"
@@ -254,15 +251,14 @@ impl VerificationResult {
         start_time: Instant,
     ) -> VerificationResult {
         let runtime = start_time.elapsed();
-        let (items, results) = extract_results(output.processed_items);
+        let (_, results) = extract_results(output.processed_items);
 
         if let Some(results) = results {
             let (status, failed_properties) =
                 verification_outcome_from_properties(&results, should_panic);
             VerificationResult {
                 status,
                 failed_properties,
-                messages: Some(items),
                 results: Ok(results),
                 runtime,
                 generated_concrete_test: false,
@@ -272,7 +268,6 @@ impl VerificationResult {
             VerificationResult {
                 status: VerificationStatus::Failure,
                 failed_properties: FailedProperties::Other,
-                messages: Some(items),
                 results: Err(output.process_status),
                 runtime,
                 generated_concrete_test: false,
@@ -284,7 +279,6 @@ impl VerificationResult {
         VerificationResult {
             status: VerificationStatus::Success,
             failed_properties: FailedProperties::None,
-            messages: None,
             results: Ok(vec![]),
             runtime: Duration::from_secs(0),
             generated_concrete_test: false,
@@ -295,7 +289,6 @@ impl VerificationResult {
         VerificationResult {
             status: VerificationStatus::Failure,
             failed_properties: FailedProperties::Other,
-            messages: None,
             // on failure, exit codes in theory might be used,
             // but `mock_failure` should never be used in a context where they will,
             // so again use something weird:

kani-driver/src/cbmc_output_parser.rs

@@ -287,9 +287,7 @@ fn filepath(file: String) -> String {
 #[derive(Clone, Debug, Deserialize)]
 #[serde(rename_all = "camelCase")]
 pub struct TraceItem {
-    pub thread: u32,
     pub step_type: String,
-    pub hidden: bool,
     pub lhs: Option<String>,
     pub source_location: Option<SourceLocation>,
     pub value: Option<TraceValue>,
@@ -301,7 +299,6 @@ pub struct TraceItem {
 /// The fields included right now are relevant to primitive types.
 #[derive(Clone, Debug, Deserialize)]
 pub struct TraceValue {
-    pub name: String,
     pub binary: Option<String>,
     pub data: Option<TraceData>,
     pub width: Option<u32>,

kani-driver/src/concrete_playback/test_generator.rs

@@ -588,9 +588,7 @@ mod tests {
                 line: None,
             },
             trace: Some(vec![TraceItem {
-                thread: 0,
                 step_type: "assignment".to_string(),
-                hidden: false,
                 lhs: Some("goto_symex$$return_value".to_string()),
                 source_location: Some(SourceLocation {
                     column: None,
@@ -599,7 +597,6 @@ mod tests {
                     line: None,
                 }),
                 value: Some(TraceValue {
-                    name: "".to_string(),
                     binary: Some("0000001100000001".to_string()),
                     data: Some(TraceData::NonBool("385".to_string())),
                     width: Some(16),

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-03-21"
+channel = "nightly-2024-03-29"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]