Upgrade Rust toolchain to nightly-2024-03-29

docs/src/rust-feature-support/intrinsics.md

@@ -220,6 +220,7 @@ truncf64 | Yes | |
 try | No | [#267](https://github.com/model-checking/kani/issues/267) |
 type_id | Yes | |
 type_name | Yes | |
+typed_swap | Yes | |
 unaligned_volatile_load | No | See [Notes - Concurrency](#concurrency) |
 unaligned_volatile_store | No | See [Notes - Concurrency](#concurrency) |
 unchecked_add | Yes | |

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

@@ -580,6 +580,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "truncf64" => codegen_simple_intrinsic!(Trunc),
             "type_id" => codegen_intrinsic_const!(),
             "type_name" => codegen_intrinsic_const!(),
+            "typed_swap" => self.codegen_swap(fargs, farg_types, loc),
             "unaligned_volatile_load" => {
                 unstable_codegen!(
                     self.codegen_expr_to_place_stable(place, fargs.remove(0).dereference())
@@ -1943,6 +1944,47 @@ impl<'tcx> GotocCtx<'tcx> {
         let zero = Type::size_t().zero();
         cast_ptr.rem(align).eq(zero)
     }
+
+    /// Swaps the memory contents pointed to by arguments `x` and `y`, respectively, which is
+    /// required for the `typed_swap` intrinsic.
+    ///
+    /// The standard library API requires that `x` and `y` are readable and writable as their
+    /// (common) type (which auto-generated checks for dereferencing will take care of), and the
+    /// memory regions pointed to must be non-overlapping.
+    pub fn codegen_swap(&mut self, mut fargs: Vec<Expr>, farg_types: &[Ty], loc: Location) -> Stmt {
+        // two parameters, and both must be raw pointers with the same base type
+        assert!(fargs.len() == 2);
+        assert!(farg_types[0].kind().is_raw_ptr());
+        assert!(farg_types[0] == farg_types[1]);
+
+        let x = fargs.remove(0);
+        let y = fargs.remove(0);
+
+        // if(same_object(x, y)) {
+        //   assert(x + 1 <= y || y + 1 <= x);
+        //   assume(x + 1 <= y || y + 1 <= x);
+        // }
+        let one = Expr::int_constant(1, Type::c_int());
+        let non_overlapping =
+            x.clone().plus(one.clone()).le(y.clone()).or(y.clone().plus(one.clone()).le(x.clone()));
+        let non_overlapping_check = self.codegen_assert_assume(
+            non_overlapping,
+            PropertyClass::SafetyCheck,
+            "memory regions pointed to by `x` and `y` must not overlap",
+            loc,
+        );
+        let non_overlapping_stmt =
+            Stmt::if_then_else(x.clone().same_object(y.clone()), non_overlapping_check, None, loc);
+
+        // T t = *y; *y = *x; *x = t;
+        let deref_y = y.clone().dereference();
+        let (temp_var, assign_to_t) =
+            self.decl_temp_variable(deref_y.typ().clone(), Some(deref_y), loc);
+        let assign_to_y = y.dereference().assign(x.clone().dereference(), loc);
+        let assign_to_x = x.dereference().assign(temp_var, loc);
+
+        Stmt::block(vec![non_overlapping_stmt, assign_to_t, assign_to_y, assign_to_x], loc)
+    }
 }
 
 fn instance_args(instance: &Instance) -> GenericArgs {

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

@@ -46,7 +46,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 {
@@ -127,9 +127,11 @@ 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,
+    #[allow(dead_code)]
+    pub start_col: usize, // set, but not currently used in Goto output
     pub end_line: usize,
-    pub end_col: usize,
+    #[allow(dead_code)]
+    pub end_col: usize, // set, but not currently used in Goto output
 }
 
 impl SourceLocation {

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,
@@ -434,7 +433,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),
@@ -453,10 +452,7 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
                                         objects in the modifies clause (including return types) \
                                         implement `{}`.\nThis is a strict condition to use \
                                         function contracts as verified stubs.",
-                                        pretty_ty(receiver_ty.kind()),
-                                        trait_,
-                                        callee,
-                                        trait_,
+                                        receiver_ty, trait_, callee, trait_,
                                     ),
                                 );
                             } else {

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

@@ -173,7 +173,7 @@ impl MutableBody {
                 let terminator = Terminator { kind, span };
                 self.split_bb(source, terminator);
             }
-            CheckType::Panic(..) | CheckType::NoCore => {
+            CheckType::Panic | CheckType::NoCore => {
                 tcx.sess
                     .dcx()
                     .struct_err("Failed to instrument the code. Cannot find `kani::assert`")
@@ -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 find_instance(tcx, "panic_str").is_some() {
+            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"]

tests/kani/Intrinsics/typed_swap.rs

@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Check that `typed_swap` yields the expected results.
+// https://doc.rust-lang.org/nightly/std/intrinsics/fn.typed_swap.html
+
+#![feature(core_intrinsics)]
+#![allow(internal_features)]
+
+#[kani::proof]
+fn test_typed_swap_u32() {
+    let mut a: u32 = kani::any();
+    let a_before = a;
+    let mut b: u32 = kani::any();
+    let b_before = b;
+    unsafe {
+        std::intrinsics::typed_swap(&mut a, &mut b);
+    }
+    assert!(b == a_before);
+    assert!(a == b_before);
+}