Upgrade Rust toolchain to nightly-2024-06-17

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

@@ -53,7 +53,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
             }
             Operand::Constant(constant) => {
-                self.codegen_const(&constant.literal, self.codegen_span_stable(constant.span))
+                self.codegen_const(&constant.const_, self.codegen_span_stable(constant.span))
             }
         }
     }

kani-compiler/src/kani_middle/reachability.rs

@@ -26,7 +26,7 @@ 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::{
-    visit::Location, Body, CastKind, Constant, MirVisitor, PointerCoercion, Rvalue, Terminator,
+    visit::Location, Body, CastKind, ConstOperand, MirVisitor, PointerCoercion, Rvalue, Terminator,
     TerminatorKind,
 };
 use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind};
@@ -375,9 +375,9 @@ impl<'a, 'tcx> MirVisitor for MonoItemsFnCollector<'a, 'tcx> {
     }
 
     /// Collect constants that are represented as static variables.
-    fn visit_constant(&mut self, constant: &Constant, location: Location) {
-        debug!(?constant, ?location, literal=?constant.literal, "visit_constant");
-        let allocation = match constant.literal.kind() {
+    fn visit_const_operand(&mut self, constant: &ConstOperand, location: Location) {
+        debug!(?constant, ?location, literal=?constant.const_, "visit_constant");
+        let allocation = match constant.const_.kind() {
             ConstantKind::Allocated(allocation) => allocation,
             ConstantKind::Unevaluated(_) => {
                 unreachable!("Instance with polymorphic constant: `{constant:?}`")

kani-compiler/src/kani_middle/stubbing/mod.rs

@@ -16,7 +16,7 @@ use rustc_middle::ty::{self, EarlyBinder, ParamEnv, TyCtxt, TypeFoldable};
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::visit::{Location, MirVisitor};
-use stable_mir::mir::Constant;
+use stable_mir::mir::ConstOperand;
 use stable_mir::ty::{FnDef, RigidTy, TyKind};
 use stable_mir::{CrateDef, CrateItem};
 
@@ -185,8 +185,8 @@ impl<'tcx> StubConstChecker<'tcx> {
 
 impl<'tcx> MirVisitor for StubConstChecker<'tcx> {
     /// Collect constants that are represented as static variables.
-    fn visit_constant(&mut self, constant: &Constant, location: Location) {
-        let const_ = self.monomorphize(rustc_internal::internal(self.tcx, &constant.literal));
+    fn visit_const_operand(&mut self, constant: &ConstOperand, location: Location) {
+        let const_ = self.monomorphize(rustc_internal::internal(self.tcx, &constant.const_));
         debug!(?constant, ?location, ?const_, "visit_constant");
         match const_ {
             Const::Val(..) | Const::Ty(..) => {}

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

@@ -81,12 +81,12 @@ impl MutableBody {
 
     pub fn new_str_operand(&mut self, msg: &str, span: Span) -> Operand {
         let literal = MirConst::from_str(msg);
-        Operand::Constant(Constant { span, user_ty: None, literal })
+        Operand::Constant(ConstOperand { span, user_ty: None, const_: literal })
     }
 
     pub fn new_const_operand(&mut self, val: u128, uint_ty: UintTy, span: Span) -> Operand {
         let literal = MirConst::try_from_uint(val, uint_ty).unwrap();
-        Operand::Constant(Constant { span, user_ty: None, literal })
+        Operand::Constant(ConstOperand { span, user_ty: None, const_: literal })
     }
 
     /// Create a raw pointer of `*mut type` and return a new local where that value is stored.

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

@@ -24,7 +24,7 @@ use stable_mir::abi::{FieldsShape, Scalar, TagEncoding, ValueAbi, VariantsShape,
 use stable_mir::mir::mono::{Instance, InstanceKind};
 use stable_mir::mir::visit::{Location, PlaceContext, PlaceRef};
 use stable_mir::mir::{
-    AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, Constant, FieldIdx, Local, LocalDecl,
+    AggregateKind, BasicBlockIdx, BinOp, Body, CastKind, ConstOperand, FieldIdx, Local, LocalDecl,
     MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place, ProjectionElem, Rvalue,
     Statement, StatementKind, Terminator, TerminatorKind,
 };
@@ -118,8 +118,8 @@ impl ValidValuePass {
         reason: &str,
     ) {
         let span = source.span(body.blocks());
-        let rvalue = Rvalue::Use(Operand::Constant(Constant {
-            literal: MirConst::from_bool(false),
+        let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
+            const_: MirConst::from_bool(false),
             span,
             user_ty: None,
         }));

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

@@ -10,7 +10,7 @@ use cbmc::{InternString, InternedString};
 use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
-use stable_mir::mir::{Body, Constant, Operand, TerminatorKind};
+use stable_mir::mir::{Body, ConstOperand, Operand, TerminatorKind};
 use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
 use stable_mir::{CrateDef, DefId};
 use std::collections::HashSet;
@@ -113,7 +113,7 @@ impl AnyModifiesPass {
                 let instance = Instance::resolve(self.kani_any.unwrap(), &instance_args).unwrap();
                 let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap();
                 let span = bb.terminator.span;
-                let new_func = Constant { span, user_ty: None, literal };
+                let new_func = ConstOperand { span, user_ty: None, const_: literal };
                 *func = Operand::Constant(new_func);
                 changed = true;
             }

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

@@ -15,7 +15,7 @@ use crate::kani_queries::QueryDb;
 use rustc_middle::ty::TyCtxt;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
-    BinOp, Body, Constant, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL,
+    BinOp, Body, ConstOperand, Operand, Place, Rvalue, Statement, StatementKind, RETURN_LOCAL,
 };
 use stable_mir::target::MachineInfo;
 use stable_mir::ty::{MirConst, RigidTy, TyKind};
@@ -79,10 +79,10 @@ impl IntrinsicGeneratorPass {
         let span = new_body.locals()[ret_var].span;
         let assign = StatementKind::Assign(
             Place::from(ret_var),
-            Rvalue::Use(Operand::Constant(Constant {
+            Rvalue::Use(Operand::Constant(ConstOperand {
                 span,
                 user_ty: None,
-                literal: MirConst::from_bool(true),
+                const_: MirConst::from_bool(true),
             })),
         );
         let stmt = Statement { kind: assign, span };
@@ -115,8 +115,8 @@ impl IntrinsicGeneratorPass {
             }
             Err(msg) => {
                 // We failed to retrieve all the valid ranges.
-                let rvalue = Rvalue::Use(Operand::Constant(Constant {
-                    literal: MirConst::from_bool(false),
+                let rvalue = Rvalue::Use(Operand::Constant(ConstOperand {
+                    const_: MirConst::from_bool(false),
                     span,
                     user_ty: None,
                 }));

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

@@ -11,7 +11,7 @@ use rustc_middle::ty::TyCtxt;
 use rustc_smir::rustc_internal;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::visit::{Location, MirVisitor};
-use stable_mir::mir::{Body, Constant, LocalDecl, Operand, Terminator, TerminatorKind};
+use stable_mir::mir::{Body, ConstOperand, LocalDecl, Operand, Terminator, TerminatorKind};
 use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind};
 use stable_mir::CrateDef;
 use std::collections::HashMap;
@@ -199,7 +199,7 @@ impl<'a> MutMirVisitor for ExternFnStubVisitor<'a> {
                     let instance = Instance::resolve(*new_def, &args).unwrap();
                     let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap();
                     let span = term.span;
-                    let new_func = Constant { span, user_ty: None, literal };
+                    let new_func = ConstOperand { span, user_ty: None, const_: literal };
                     *func = Operand::Constant(new_func);
                     self.changed = true;
                 }
@@ -212,12 +212,12 @@ impl<'a> MutMirVisitor for ExternFnStubVisitor<'a> {
         let func_ty = operand.ty(&self.locals).unwrap();
         if let TyKind::RigidTy(RigidTy::FnDef(orig_def, args)) = func_ty.kind() {
             if let Some(new_def) = self.stubs.get(&orig_def) {
-                let Operand::Constant(Constant { span, .. }) = operand else {
+                let Operand::Constant(ConstOperand { span, .. }) = operand else {
                     unreachable!();
                 };
                 let instance = Instance::resolve_for_fn_ptr(*new_def, &args).unwrap();
                 let literal = MirConst::try_new_zero_sized(instance.ty()).unwrap();
-                let new_func = Constant { span: *span, user_ty: None, literal };
+                let new_func = ConstOperand { span: *span, user_ty: None, const_: literal };
                 *operand = Operand::Constant(new_func);
                 self.changed = true;
             }

kani-driver/src/call_single_file.rs

@@ -184,6 +184,10 @@ impl KaniSession {
             }
         }
 
+        if self.args.coverage {
+            flags.push("-Zmir-enable-passes=-SingleUseConsts".into());
+        }
+
         // This argument will select the Kani flavour of the compiler. It will be removed before
         // rustc driver is invoked.
         flags.push("--kani-compiler".into());

rust-toolchain.toml

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

scripts/kani-regression.sh

@@ -33,8 +33,8 @@ check_kissat_version.sh
 # Formatting check
 ${SCRIPT_DIR}/kani-fmt.sh --check
 
-# Build all packages in the workspace and ensure no warning is emitted.
-RUSTFLAGS="-D warnings" cargo build-dev
+# Build kani
+cargo build-dev
 
 # Unit tests
 cargo test -p cprover_bindings
@@ -102,6 +102,13 @@ FEATURES_MANIFEST_PATH="$KANI_DIR/tests/cargo-kani/cargo-features-flag/Cargo.tom
 cargo kani --manifest-path "$FEATURES_MANIFEST_PATH" --harness trivial_success
 cargo clean --manifest-path "$FEATURES_MANIFEST_PATH"
 
+# Build all packages in the workspace and ensure no warning is emitted.
+# Please don't replace `cargo build-dev` above with this command.
+# Setting RUSTFLAGS like this always resets cargo's build cache resulting in
+# all tests to be re-run. I.e., cannot keep re-runing the regression from where
+# we stopped.
+RUSTFLAGS="-D warnings" cargo build --target-dir /tmp/kani_build_warnings
+
 echo
 echo "All Kani regression tests completed successfully."
 echo